dtlc

commit 98a4af8e5798785f07f05471de0c031beb111085
parent 680d5ffc27c92e9f504ced9ebd714f403d9174a6
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Wed, 20 Dec 2023 13:38:18 -0800

Test error handling

Diffstat:
M
elab.ml
 | 
4
++--
M
lexer.mll
 | 
4
++--
M
main.ml
 | 
29
+++++++++++++++++++++--------

3 files changed, 25 insertions(+), 12 deletions(-)
diff --git a/elab.ml b/elab.ml
@@ -4,9 +4,9 @@ module A = Abstract
 module I = Internal
 module V = Value
 
-exception ElabError of Loc.t * string
+exception Error of Loc.t * string
 
-let error loc msg = raise (ElabError (loc, msg))
+let error loc msg = raise (Error (loc, msg))
 
 (* TODO: use a hashtable or map for ident -> level lookups *)
 type context = {
diff --git a/lexer.mll b/lexer.mll
@@ -2,11 +2,11 @@
 open Common
 open Parser
 
-exception LexerError of Loc.t * string
+exception Error of Loc.t * string
 
 let error lexbuf msg =
 	let loc = Loc.of_position (Lexing.lexeme_start_p lexbuf) in
-	raise (LexerError (loc, msg))
+	raise (Error (loc, msg))
 }
 
 let dnumeral = ['0'-'9']
diff --git a/main.ml b/main.ml
@@ -1,17 +1,30 @@
 (*let buf = Lexing.from_string "(fn A: Nat -> Type, f: (A 0, A 1) -> A 2, x: A 0, y: A 1 => f x y) (fn _: Nat => Nat) (fn x: Nat, y: Nat => x + y) 3 4 : Nat"*)
 (*let buf = Lexing.from_string "N := (A: Type, A, A -> A) -> A; ((fn m: N, n: N => fn A: Type, z: A, s: A -> A => m A (n A z s) s) (fn A: Type, z: A, s: A -> A => s (s z)) (fn A: Type, z: A, s: A -> A => s (s (s z)))) Nat 0 (fn n: Nat => n + 1)"*)
 let buf = Lexing.from_string "\
-	N := (A: Type, A, A -> A) -> A;\
-	add: (N, N) -> N := fn m, n => fn A, z, s => m A (n A z s) s;\
-	two: N := fn A, z, s => s (s z);\
-	three: N := fn A, z, s => s (s (s z));\
-	five := add two three;\
-	five Nat 0 (fn n => n + 1)\
+	N := (A: Type, A, A -> A) -> A;\n\
+	add: (N, N) -> N := fn m, n => fn A, z, s => m A (n A z s) s;\n\
+	two: N := fn A, z, s => s (s z);\n\
+	three: N := fn A, z, s => s (s (s z));\n\
+	five := add two three;\n\
+	five Nat 0 (fn n => n + 1)\n\
 "
-let concrete = Parser.start Lexer.token buf
+
+let concrete =
+	try Parser.start Lexer.token buf with
+	| Lexer.Error (loc, msg) ->
+		let () = print_endline ("[" ^ Loc.to_string loc ^ "] " ^ msg) in
+		exit 1
+
 let abstract = Cnctoabs.term concrete
+
 let ctx = Elab.default_ctx
-let (internal, ty) = Elab.infer ctx abstract
+let (internal, ty) =
+	try Elab.infer ctx abstract with
+	| Elab.Error (loc, msg) ->
+		let () = print_endline ("[" ^ Loc.to_string loc ^ "] " ^ msg) in
+		exit 1
+
 let internal' = Eval.quote ctx.len (Eval.eval ctx.values internal)
+
 let () = print_endline (Internal.to_string 0 internal)
 let () = print_endline (Internal.to_string 0 internal')