Improve error messages

.ocamlformat

@@ -0,0 +1,2 @@
+profile = default
+version = 0.26.1

TestFile.neon

@@ -5,16 +5,15 @@ let eq =
     fun A: type        => 
     fun x: A           => 
     fun y: A           => 
-    fun  P: (A -> type) => P(x) -> P(y)
+    pi  P: (A -> type) => P(x) -> P(y)
 
 
 let refl_type = 
     pi A: type         =>
     pi a: A            =>
-    pi P : (A -> type) =>
-    eq(A)(a)(a)(P)
+    eq(A)(a)(a)
 
-let refl : refl_type = 
+let refl = 
     fun A:  type         =>
     fun x:  A            =>
     fun P:  (A -> type)  =>

bin/dune

@@ -1,4 +1,4 @@
 (executable
  (public_name neon)
  (name main)
- (libraries ast parser typeChecker prettyPrinter))
+ (libraries ast env parser typeChecker prettyPrinter))

bin/main.ml

@@ -1,9 +1,14 @@
-let env = Ast.create_env ()
-let print (term, tp) = print_endline (PrettyPrinter.term_to_string term ^ ": " ^ PrettyPrinter.term_to_string tp) 
-let _ = List.iter print (List.map (TypeChecker.infer_type env) (Parser.parse_file "TestFile.neon"))
+let env = Env.create_env ()
 
+let print (term, tp) =
+  print_endline
+    (PrettyPrinter.term_to_string term ^ ": " ^ PrettyPrinter.term_to_string tp)
+
+let _ =
+  List.iter print
+    (List.map (TypeChecker.infer_type env) (Parser.parse_file "TestFile.neon"))
 
 (* let term, tp = TypeChecker.infer_type env (List.hd (Parser.parse_file "TestFile.neon"))
-let term_s = PrettyPrinter.term_to_string term
-let tp_s = PrettyPrinter.term_to_string tp
-let _ = print_endline (term_s ^ ": " ^ tp_s) *)
+   let term_s = PrettyPrinter.term_to_string term
+   let tp_s = PrettyPrinter.term_to_string tp
+   let _ = print_endline (term_s ^ ": " ^ tp_s) *)

lib/ast/ast.ml

@@ -1,76 +1,16 @@
 (* TERMS *)
 type var = int
 
-type term = 
+type term =
   | Type
   | Kind
   | Triangle
   | Var of string * var
   | Lambda of string * var * tp * term
   | Product of string * var * tp * tp
   | App of term * term
-  | Hole of string * tp 
+  | Hole of string * tp
   | Let of string * var * term * tp * term
   | TypeArrow of tp * tp
-and tp = term
-
-
-(* ENV *)
-module UTermEnvHashtbl = Hashtbl.Make(String)
-module TermEnvHashtbl = Hashtbl.Make(Int)
-
-type env_var = 
-  | Opaque of tp
-  | Transparent of term * tp
-
-type uTermEnv = var UTermEnvHashtbl.t 
-type termEnv =  env_var TermEnvHashtbl.t
-type env = uTermEnv * termEnv
-
-let counter = ref 0
-
-let fresh_var () : int =
-  let fresh_var = !counter in
-  let _ = counter := !counter + 1 in
-  fresh_var
-
-
-
-let create_env () : env =
-  UTermEnvHashtbl.create 10, TermEnvHashtbl.create 10
-
-let add_to_env (uTermEnv, termEnv: env) (nm : string) (var : env_var) : var =
-  let y = fresh_var () in
-  let _ = UTermEnvHashtbl.add uTermEnv nm y in
-  let _ = TermEnvHashtbl.add termEnv y var in
-  y
-
-let add_to_termEnv (termEnv: termEnv) (var: var) (env_var : env_var) : unit =
-  TermEnvHashtbl.add termEnv var env_var
-
-let rm_from_env (uTermEnv, termEnv: env) (nm : string) : unit =
-  let y = UTermEnvHashtbl.find uTermEnv nm in
-  let _ = UTermEnvHashtbl.remove uTermEnv nm in
-  TermEnvHashtbl.remove termEnv y
-
-let rm_from_termEnv (termEnv: termEnv) (var: var) : unit =
-  TermEnvHashtbl.remove termEnv var
-
-let find_opt_in_env (uTermEnv, termEnv: env) (nm: string) : (var * env_var) option =
-  match UTermEnvHashtbl.find_opt uTermEnv nm with
-  | None -> None
-  | Some var -> 
-    match TermEnvHashtbl.find_opt termEnv var with
-    | None -> None
-    | Some env_var -> Some (var, env_var)
-
-let find_opt_in_termEnv (termEnv: termEnv) (var : var) : env_var option =
-  match TermEnvHashtbl.find_opt termEnv var with
-  | None -> None
-  | Some env_var -> Some env_var
-
-let print_env (uTermEnv, termEnv: env) : string =
-  UTermEnvHashtbl.iter (fun key val -> Printf.sprintf ("%s ->" ^^ " %s\n") key val) uTermEnv
-
-  (* "x" -> num -> term*)
 
+and tp = term

lib/env/dune

@@ -0,0 +1,3 @@
+(library
+ (name env)
+ (libraries prettyPrinter ast))

lib/env/env.ml

@@ -0,0 +1,71 @@
+open Ast
+
+(* ENV *)
+module UTermEnvHashtbl = Hashtbl.Make(String)
+module TermEnvHashtbl = Hashtbl.Make(Int)
+
+type env_var = 
+  | Opaque of tp
+  | Transparent of term * tp
+
+type uTermEnv = var UTermEnvHashtbl.t 
+type termEnv =  env_var TermEnvHashtbl.t
+type env = uTermEnv * termEnv
+
+let counter = ref 0
+
+let fresh_var () : int =
+  let fresh_var = !counter in
+  let _ = counter := !counter + 1 in
+  fresh_var
+
+
+
+let create_env () : env =
+  UTermEnvHashtbl.create 10, TermEnvHashtbl.create 10
+
+let add_to_env (uTermEnv, termEnv: env) (nm : string) (var : env_var) : var =
+  let y = fresh_var () in
+  let _ = UTermEnvHashtbl.add uTermEnv nm y in
+  let _ = TermEnvHashtbl.add termEnv y var in
+  y
+
+let add_to_termEnv (termEnv: termEnv) (var: var) (env_var : env_var) : unit =
+  TermEnvHashtbl.add termEnv var env_var
+
+let rm_from_env (uTermEnv, termEnv: env) (nm : string) : unit =
+  let y = UTermEnvHashtbl.find uTermEnv nm in
+  let _ = UTermEnvHashtbl.remove uTermEnv nm in
+  TermEnvHashtbl.remove termEnv y
+
+let rm_from_termEnv (termEnv: termEnv) (var: var) : unit =
+  TermEnvHashtbl.remove termEnv var
+
+let find_opt_in_env (uTermEnv, termEnv: env) (nm: string) : (var * env_var) option =
+  match UTermEnvHashtbl.find_opt uTermEnv nm with
+  | None -> None
+  | Some var -> 
+    match TermEnvHashtbl.find_opt termEnv var with
+    | None -> None
+    | Some env_var -> Some (var, env_var)
+
+let find_opt_in_termEnv (termEnv: termEnv) (var : var) : env_var option =
+  match TermEnvHashtbl.find_opt termEnv var with
+  | None -> None
+  | Some env_var -> Some env_var
+
+let env_var_to_string (env_var : env_var option) : string =
+  match env_var with
+  | None -> "Not found"
+  | Some Opaque tp -> PrettyPrinter.term_to_string tp
+  | Some Transparent (term, tp) -> PrettyPrinter.term_to_string term ^ " : " ^ PrettyPrinter.term_to_string tp
+
+let env_to_string (uTermEnv, termEnv: env) : string =
+  (UTermEnvHashtbl.fold (fun key v acc -> acc ^ Printf.sprintf ("%s -> %d -> %s\n") key v
+   (env_var_to_string (TermEnvHashtbl.find_opt termEnv v))) uTermEnv "\n") ^ "\n"
+
+let termEnv_to_string (termEnv: termEnv) : string = 
+  (TermEnvHashtbl.fold (fun key v acc -> acc ^ Printf.sprintf ("%d -> %s\n") key
+  (env_var_to_string (Some v))) termEnv "\n") ^ "\n"
+
+  (* "x" -> num -> term  *)

lib/errors/errors.ml

@@ -1,20 +1,16 @@
 type parser_reason =
-| EofInComment
-| InvalidNumber   of string
-| InvalidChar     of char
-| UnexpectedToken of string
+  | EofInComment
+  | InvalidNumber of string
+  | InvalidChar of char
+  | UnexpectedToken of string
 
 exception Parse_error of ParserAst.position * parser_reason
+exception Cannot_open_file of { fname : string; message : string }
 
-exception Cannot_open_file of
-  { fname   : string
-  ; message : string
-  }
+type type_checker_reason =
+  | InferTypeError of string
+  | CheckTypeError of string
+  | EqualityError of string
+  | WhnfError of string
 
-type type_checker_reason = 
-| InferTypeError of string * ParserAst.position
-| CheckTypeError of string * ParserAst.position
-| EqualityError of string
-| WhnfError of string
-
-exception Type_error of type_checker_reason
+exception Type_error of type_checker_reason

lib/lexer/dune

@@ -1,5 +1,5 @@
 (library
-  (name lexer)
-  (libraries parserAst yaccParser errors))
+ (name lexer)
+ (libraries parserAst yaccParser errors))
 
-(ocamllex lexer)
+(ocamllex lexer)

lib/parser/dune

@@ -1,3 +1,3 @@
 (library
-  (name parser)
-  (libraries parserAst errors lexer yaccParser))
+ (name parser)
+ (libraries parserAst errors lexer yaccParser))

lib/parser/parser.ml

@@ -1,31 +1,30 @@
 type fname = string
 
 let run_parser parse (lexbuf : Lexing.lexbuf) =
-  try parse Lexer.token lexbuf with
-  | Parsing.Parse_error ->
+  try parse Lexer.token lexbuf
+  with Parsing.Parse_error ->
     let pos =
-      { ParserAst.start  = lexbuf.lex_start_p
-      ; ParserAst.length = lexbuf.lex_curr_p.pos_cnum - lexbuf.lex_start_p.pos_cnum
-      } in
-    raise (Errors.Parse_error(pos, UnexpectedToken (Lexing.lexeme lexbuf)))
+      {
+        ParserAst.start = lexbuf.lex_start_p;
+        ParserAst.length =
+          lexbuf.lex_curr_p.pos_cnum - lexbuf.lex_start_p.pos_cnum;
+      }
+    in
+    raise (Errors.Parse_error (pos, UnexpectedToken (Lexing.lexeme lexbuf)))
 
 let parse_file fname =
   match open_in fname with
-  | chan ->
-    begin match
-      let lexbuf = Lexing.from_channel chan in
-      lexbuf.lex_curr_p <-
-        { lexbuf.lex_curr_p with
-          pos_fname = fname
-        };
-      run_parser YaccParser.program lexbuf
-    with
-    | result ->
-      close_in chan;
-      result
-    | exception exn ->
-      close_in_noerr chan;
-      raise exn
-    end
+  | chan -> (
+      match
+        let lexbuf = Lexing.from_channel chan in
+        lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fname };
+        run_parser YaccParser.program lexbuf
+      with
+      | result ->
+          close_in chan;
+          result
+      | exception exn ->
+          close_in_noerr chan;
+          raise exn)
   | exception Sys_error message ->
-    raise (Errors.Cannot_open_file { fname; message })
+      raise (Errors.Cannot_open_file { fname; message })

lib/parserAst/parserAst.ml

@@ -1,29 +1,21 @@
-type position =
-  { start  : Lexing.position
-  ; length : int
-  }
-
-type 'a node =
-  { pos  : position
-  ; data : 'a
-  }
+type position = { start : Lexing.position; length : int }
+type 'a node = { pos : position; data : 'a }
 
 type uTerm = term_data node
+
 and term_data =
-| Type
-| Kind
-| Var of string
-| Lambda of string * uTerm option * uTerm
-| Product of string * uTerm * uTerm
-| App of uTerm * uTerm
-| TermWithTypeAnno of uTerm * uTerm
-| Let of string * uTerm * uTerm
-| LetDef of string * uTerm
-| Lemma of string * uTerm * uTerm
-| LemmaDef of string * uTerm
-| Hole of string
-| TypeArrow of uTerm * uTerm
+  | Type
+  | Kind
+  | Var of string
+  | Lambda of string * uTerm option * uTerm
+  | Product of string * uTerm * uTerm
+  | App of uTerm * uTerm
+  | TermWithTypeAnno of uTerm * uTerm
+  | Let of string * uTerm * uTerm
+  | LetDef of string * uTerm
+  | Lemma of string * uTerm * uTerm
+  | LemmaDef of string * uTerm
+  | Hole of string
+  | TypeArrow of uTerm * uTerm
 
 type program = uTerm list
-
-

lib/prettyPrinter/dune

@@ -1,4 +1,5 @@
 (library
  (name prettyPrinter)
- (flags (-warn-error -A))
-(libraries ast parserAst))
+ (flags
+  (-warn-error -A))
+ (libraries ast parserAst))