From c2f06e61a58f3830f96086a8cc3b51d8cc68f34f Mon Sep 17 00:00:00 2001 From: Tagada14 Date: Wed, 31 Jan 2024 13:03:55 +0100 Subject: [PATCH] Improve error messages --- .ocamlformat | 2 + TestFile.neon | 7 ++- bin/dune | 2 +- bin/main.ml | 17 ++++--- lib/ast/ast.ml | 66 ++------------------------- lib/env/dune | 3 ++ lib/env/env.ml | 71 +++++++++++++++++++++++++++++ lib/errors/errors.ml | 26 +++++------ lib/lexer/dune | 6 +-- lib/parser/dune | 4 +- lib/parser/parser.ml | 45 +++++++++--------- lib/parserAst/parserAst.ml | 40 +++++++--------- lib/prettyPrinter/dune | 5 +- lib/prettyPrinter/prettyPrinter.ml | 62 +++++++++++++++---------- lib/prettyPrinter/prettyPrinter.mli | 2 +- lib/typeChecker/dune | 2 +- lib/typeChecker/typeChecker.ml | 70 ++++++++++++++++------------ lib/typeChecker/typeChecker.mli | 3 +- lib/yaccParser/dune | 6 +-- 19 files changed, 235 insertions(+), 204 deletions(-) create mode 100644 .ocamlformat create mode 100644 lib/env/dune create mode 100644 lib/env/env.ml diff --git a/.ocamlformat b/.ocamlformat new file mode 100644 index 0000000..7df62da --- /dev/null +++ b/.ocamlformat @@ -0,0 +1,2 @@ +profile = default +version = 0.26.1 \ No newline at end of file diff --git a/TestFile.neon b/TestFile.neon index cd4f626..c78e830 100644 --- a/TestFile.neon +++ b/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) => diff --git a/bin/dune b/bin/dune index 65caf19..6ca7349 100644 --- a/bin/dune +++ b/bin/dune @@ -1,4 +1,4 @@ (executable (public_name neon) (name main) - (libraries ast parser typeChecker prettyPrinter)) + (libraries ast env parser typeChecker prettyPrinter)) diff --git a/bin/main.ml b/bin/main.ml index b9b5fbf..ffe9c7b 100644 --- a/bin/main.ml +++ b/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) *) \ No newline at end of file + let term_s = PrettyPrinter.term_to_string term + let tp_s = PrettyPrinter.term_to_string tp + let _ = print_endline (term_s ^ ": " ^ tp_s) *) diff --git a/lib/ast/ast.ml b/lib/ast/ast.ml index 1430ae0..c0a76ba 100644 --- a/lib/ast/ast.ml +++ b/lib/ast/ast.ml @@ -1,7 +1,7 @@ (* TERMS *) type var = int -type term = +type term = | Type | Kind | Triangle @@ -9,68 +9,8 @@ type term = | 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 diff --git a/lib/env/dune b/lib/env/dune new file mode 100644 index 0000000..22c4950 --- /dev/null +++ b/lib/env/dune @@ -0,0 +1,3 @@ +(library + (name env) + (libraries prettyPrinter ast)) diff --git a/lib/env/env.ml b/lib/env/env.ml new file mode 100644 index 0000000..5e65740 --- /dev/null +++ b/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 *) \ No newline at end of file diff --git a/lib/errors/errors.ml b/lib/errors/errors.ml index 091b920..d5e10a7 100644 --- a/lib/errors/errors.ml +++ b/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 \ No newline at end of file +exception Type_error of type_checker_reason diff --git a/lib/lexer/dune b/lib/lexer/dune index 446cde0..dc34acb 100644 --- a/lib/lexer/dune +++ b/lib/lexer/dune @@ -1,5 +1,5 @@ (library - (name lexer) - (libraries parserAst yaccParser errors)) + (name lexer) + (libraries parserAst yaccParser errors)) -(ocamllex lexer) \ No newline at end of file +(ocamllex lexer) diff --git a/lib/parser/dune b/lib/parser/dune index 593b5ca..6307a19 100644 --- a/lib/parser/dune +++ b/lib/parser/dune @@ -1,3 +1,3 @@ (library - (name parser) - (libraries parserAst errors lexer yaccParser)) \ No newline at end of file + (name parser) + (libraries parserAst errors lexer yaccParser)) diff --git a/lib/parser/parser.ml b/lib/parser/parser.ml index 25a1045..1d6d202 100644 --- a/lib/parser/parser.ml +++ b/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 }) diff --git a/lib/parserAst/parserAst.ml b/lib/parserAst/parserAst.ml index 0e14c1e..70d8701 100644 --- a/lib/parserAst/parserAst.ml +++ b/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 - - diff --git a/lib/prettyPrinter/dune b/lib/prettyPrinter/dune index 0a80267..dfe55d9 100644 --- a/lib/prettyPrinter/dune +++ b/lib/prettyPrinter/dune @@ -1,4 +1,5 @@ (library (name prettyPrinter) - (flags (-warn-error -A)) -(libraries ast parserAst)) \ No newline at end of file + (flags + (-warn-error -A)) + (libraries ast parserAst)) diff --git a/lib/prettyPrinter/prettyPrinter.ml b/lib/prettyPrinter/prettyPrinter.ml index e8e5c1b..caff402 100644 --- a/lib/prettyPrinter/prettyPrinter.ml +++ b/lib/prettyPrinter/prettyPrinter.ml @@ -6,30 +6,42 @@ let rec term_to_string (t : term) : string = | Type -> "Type" | Kind -> "Kind" | Var (nm, _) -> nm - | Lambda (nm, _, tp_x, body) -> "(λ" ^ nm ^ ":" ^ (term_to_string tp_x) ^ " => " ^ (term_to_string body) ^ ")" - | Product (nm, _, tp_x, body) -> "(Π" ^ nm ^ ":" ^ (term_to_string tp_x) ^ " => " ^ (term_to_string body) ^ ")" - | App (t1, t2) -> "(" ^ (term_to_string t1) ^ ") (" ^ (term_to_string t2) ^ ")" - | Let (nm, _, t1, tp_t1, t2) -> "(let " ^ nm ^ "=" ^ (term_to_string t1) ^ ":" ^ (term_to_string tp_t1) ^ " in\n\t" ^ (term_to_string t2) - | Hole (nm, tp) -> nm ^ ":" ^ (term_to_string tp) - | TypeArrow (tp1, tp2) -> "(" ^ (term_to_string tp1) ^ " -> " ^ (term_to_string tp2) ^ ")" + | Lambda (nm, _, tp_x, body) -> + "(λ" ^ nm ^ ":" ^ term_to_string tp_x ^ " => " ^ term_to_string body ^ ")" + | Product (nm, _, tp_x, body) -> + "(Π" ^ nm ^ ":" ^ term_to_string tp_x ^ " => " ^ term_to_string body ^ ")" + | App (t1, t2) -> "(" ^ term_to_string t1 ^ ") (" ^ term_to_string t2 ^ ")" + | Let (nm, _, t1, tp_t1, t2) -> + "(let " ^ nm ^ "=" ^ term_to_string t1 ^ ":" ^ term_to_string tp_t1 + ^ " in\n\t" ^ term_to_string t2 + | Hole (nm, tp) -> nm ^ ":" ^ term_to_string tp + | TypeArrow (tp1, tp2) -> + "(" ^ term_to_string tp1 ^ " -> " ^ term_to_string tp2 ^ ")" | Triangle -> "Idk how u got here" - let rec uterm_to_string ({pos; data = t}: uTerm) : string = - match t with - | Type -> "Type" - | Kind -> "Kind" - | Var nm -> nm - | Lambda (nm, tp_x, body) -> - begin match tp_x with - | Some tp_x -> "(λ" ^ nm ^ ":" ^ (uterm_to_string tp_x) ^ " => " ^ (uterm_to_string body) ^ ")" - | None -> "(λ" ^ nm ^ " => " ^ (uterm_to_string body) ^ ")" - end - | Product (nm, tp_x, body) -> "(Π" ^ nm ^ ":" ^ (uterm_to_string tp_x) ^ " => " ^ (uterm_to_string body) ^ ")" - | App (t1, t2) -> "(" ^ (uterm_to_string t1) ^ ") (" ^ (uterm_to_string t2) ^ ")" - | Let (nm, t1, t2) -> "(let " ^ nm ^ "=" ^ (uterm_to_string t1) ^ " in\n\t" ^ (uterm_to_string t2) - | LetDef (nm, t1) -> "(let " ^ nm ^ "=" ^ (uterm_to_string t1) - | Lemma (nm, t1, t2) -> "(lemma " ^ nm ^ "=" ^ (uterm_to_string t1) ^ " in\n\t" ^ (uterm_to_string t2) - | LemmaDef (nm, t1) -> "(lemmaDef " ^ nm ^ "=" ^ (uterm_to_string t1) - | Hole nm -> nm - | TypeArrow (tp1, tp2) -> "(" ^ (uterm_to_string tp1) ^ " -> " ^ (uterm_to_string tp2) ^ ")" - | TermWithTypeAnno (t1, t2) -> "(" ^ (uterm_to_string t1) ^ " : " ^ (uterm_to_string t2) ^ ")" +let rec uterm_to_string ({ pos; data = t } : uTerm) : string = + match t with + | Type -> "Type" + | Kind -> "Kind" + | Var nm -> nm + | Lambda (nm, tp_x, body) -> ( + match tp_x with + | Some tp_x -> + "(λ" ^ nm ^ ":" ^ uterm_to_string tp_x ^ " => " ^ uterm_to_string body + ^ ")" + | None -> "(λ" ^ nm ^ " => " ^ uterm_to_string body ^ ")") + | Product (nm, tp_x, body) -> + "(Π" ^ nm ^ ":" ^ uterm_to_string tp_x ^ " => " ^ uterm_to_string body + ^ ")" + | App (t1, t2) -> "(" ^ uterm_to_string t1 ^ ") (" ^ uterm_to_string t2 ^ ")" + | Let (nm, t1, t2) -> + "(let " ^ nm ^ "=" ^ uterm_to_string t1 ^ " in\n\t" ^ uterm_to_string t2 + | LetDef (nm, t1) -> "(let " ^ nm ^ "=" ^ uterm_to_string t1 + | Lemma (nm, t1, t2) -> + "(lemma " ^ nm ^ "=" ^ uterm_to_string t1 ^ " in\n\t" ^ uterm_to_string t2 + | LemmaDef (nm, t1) -> "(lemmaDef " ^ nm ^ "=" ^ uterm_to_string t1 + | Hole nm -> nm + | TypeArrow (tp1, tp2) -> + "(" ^ uterm_to_string tp1 ^ " -> " ^ uterm_to_string tp2 ^ ")" + | TermWithTypeAnno (t1, t2) -> + "(" ^ uterm_to_string t1 ^ " : " ^ uterm_to_string t2 ^ ")" diff --git a/lib/prettyPrinter/prettyPrinter.mli b/lib/prettyPrinter/prettyPrinter.mli index dc06417..1464daa 100644 --- a/lib/prettyPrinter/prettyPrinter.mli +++ b/lib/prettyPrinter/prettyPrinter.mli @@ -2,4 +2,4 @@ open Ast open ParserAst val term_to_string : term -> string -val uterm_to_string : uTerm -> string \ No newline at end of file +val uterm_to_string : uTerm -> string diff --git a/lib/typeChecker/dune b/lib/typeChecker/dune index d70af86..02fc744 100644 --- a/lib/typeChecker/dune +++ b/lib/typeChecker/dune @@ -1,3 +1,3 @@ (library (name typeChecker) - (libraries ast parserAst prettyPrinter errors)) + (libraries ast env parserAst prettyPrinter errors)) diff --git a/lib/typeChecker/typeChecker.ml b/lib/typeChecker/typeChecker.ml index 756401f..bf900b0 100644 --- a/lib/typeChecker/typeChecker.ml +++ b/lib/typeChecker/typeChecker.ml @@ -1,5 +1,6 @@ open Ast open PrettyPrinter +open Env module VarMap = Map.Make(Int) type sub_map = term VarMap.t @@ -14,10 +15,17 @@ type whnf = | Lambda of var * tp * term | Product of var * tp * tp -let create_infer_type_error (pos : ParserAst.position) (error_msg: string) (term: ParserAst.uTerm) (env: env) : string = - "Error at " ^ (Int.to_string pos.start.pos_lnum) ^ ":" ^ (Int.to_string pos.start.pos_bol) ^ "\n" ^ - "While infering the type of term: " ^ uterm_to_string(term) ^ "\n The following error accured:\n" ^ error_msg ^ "\n" - ^ "The state of the environment at that moment:\n" +let create_infer_type_error (pos : ParserAst.position) (error_msg: string) (term: ParserAst.uTerm) (env: env) : 'a = + let _ = print_endline ("While infering the type of term: " ^ uterm_to_string(term) ^ + "\n\n The following error accured:\n\t" ^ error_msg ^ "\n" + ^ "\nThe state of the environment at that moment:\n" ^ env_to_string env) in + failwith ("Error at line " ^ (Int.to_string pos.start.pos_lnum) ^ ":" ^ (Int.to_string (pos.start.pos_cnum - pos.start.pos_bol))) + +let create_check_type_error (pos : ParserAst.position) (error_msg: string) (term: ParserAst.uTerm) (tp: tp) (env: env) : 'a = +let _ = print_endline ("While checking the type of term: " ^ uterm_to_string(term) ^ "\nwith expected type: " ^ + term_to_string tp ^"\n\nThe following error accured:\n\t" ^ error_msg ^ "\n" + ^ "\nThe state of the environment at that moment:\n" ^ env_to_string env) in + failwith ("Error at line " ^ (Int.to_string pos.start.pos_lnum) ^ ":" ^ (Int.to_string (pos.start.pos_cnum - pos.start.pos_bol))) let rec substitute (t: term) (sub: sub_map) : term = begin match t with @@ -65,15 +73,15 @@ let rec to_whnf (t: term) (env: termEnv) : whnf = | Product (_, x, x_tp, body) -> Product (x, x_tp, body) | TypeArrow (tp1, tp2) -> Product(-1, tp1, tp2) | App (t1, t2) -> - let _ = print_endline (term_to_string t1) in - let _ = print_endline (term_to_string t2) in + (* let _ = print_endline (term_to_string t1) in *) + (* let _ = print_endline (term_to_string t2) in *) begin match to_whnf t1 env with | Neu (x, ts) -> - let _ = print_endline "Dupa" in + (* let _ = print_endline "Dupa" in *) Neu (x, (t2 :: ts)) | Neu_with_Hole (x, tp, ts) -> Neu_with_Hole (x, tp, (t2 :: ts)) | Lambda (x, _, body) -> - let _ = print_endline "Dupa" in + (* let _ = print_endline "Dupa" in *) to_whnf (substitute body (VarMap.singleton x t2)) env | _ -> failwith ("Expected Neu or Lambda when reducing Application " ^ term_to_string t1 ^ " with whnf " ^ term_to_string t2) end @@ -129,16 +137,16 @@ let rec equiv (t1: term) (t2: term) (env: termEnv): bool = | (_, Neu_with_Hole (nm, _, _)) -> failwith ("Hole " ^ nm ^ " is expected to be equal to " ^ (term_to_string t1)) | _ -> false -let rec infer_type ((_, termEnv) as env : env) ({pos; data = t}: ParserAst.uTerm) : (term * term) = +let rec infer_type ((_, termEnv) as env : env) ({pos; data = t} as term: ParserAst.uTerm) : (term * term) = match t with | Type -> (Type, Kind) - | Kind -> (Kind, Triangle) + | Kind -> create_infer_type_error pos "Can't infer the type of Kind" term env | Var x -> begin match find_opt_in_env env x with | Some (y, (Opaque tp | (Transparent (_, tp)))) -> (Var (x, y), tp) - | None -> failwith (create_type_checker_error pos ("Variable " ^ x ^ " not found")) + | None -> (create_infer_type_error pos ("Variable " ^ x ^ " not found") term env) end - | Lambda (_, None, _) -> failwith (create_type_checker_error pos "Can't infer the type of lambda with omitted argument type") + | Lambda (_, None, _) -> (create_infer_type_error pos "Can't infer the type of lambda with omitted argument type" term env) | Lambda (x, Some tp, t) -> let (tp, tp_of_tp) = infer_type env tp in begin match tp_of_tp with @@ -147,7 +155,7 @@ let rec infer_type ((_, termEnv) as env : env) ({pos; data = t}: ParserAst.uTerm let (body, body_tp) = infer_type env t in let _ = rm_from_env env x in (Lambda (x, fresh_var, tp, body) , Product (x, fresh_var, tp, body_tp)) - | _ -> failwith (create_type_checker_error pos "The type of Lambda argument type must be either Type or Kind") + | _ -> (create_infer_type_error pos "The type of Lambda argument type must be either Type or Kind" term env) end | Product (x, tp, t) -> let (tp, tp_of_tp) = infer_type env tp in @@ -159,9 +167,9 @@ let rec infer_type ((_, termEnv) as env : env) ({pos; data = t}: ParserAst.uTerm begin match body_tp with | Type | Kind -> (Product (x, fresh_var, tp, body) , body_tp) - | _ -> failwith (create_type_checker_error pos "The type of Product body type must be either Type or Kind") + | _ -> (create_infer_type_error pos "The type of Product body type must be either Type or Kind" term env) end - | _ -> failwith (create_type_checker_error pos "The type of Product argument type must be either Type or Kind") + | _ -> (create_infer_type_error pos "The type of Product argument type must be either Type or Kind" term env) end | TypeArrow (tp1, tp2) -> let (tp1, tp_of_tp1) = infer_type env tp1 in @@ -171,9 +179,9 @@ let rec infer_type ((_, termEnv) as env : env) ({pos; data = t}: ParserAst.uTerm begin match tp_of_tp2 with | Type | Kind -> (TypeArrow (tp1, tp2) , tp_of_tp2) - | _ -> failwith (create_type_checker_error pos "The type of Type Arrow body type must be either Type or Kind") + | _ -> (create_infer_type_error pos "The type of Type Arrow body type must be either Type or Kind" term env) end - | _ -> failwith (create_type_checker_error pos "The type of Type Arrow argument type must be either Type or Kind") + | _ -> (create_infer_type_error pos "The type of Type Arrow argument type must be either Type or Kind" term env) end | App (t1, t2) -> let (t1, t1_tp) = infer_type env t1 in @@ -181,13 +189,13 @@ let rec infer_type ((_, termEnv) as env : env) ({pos; data = t}: ParserAst.uTerm | Product (x, x_tp, tp_body) -> let t2 = check_type env t2 x_tp in (App (t1, t2), substitute tp_body (VarMap.singleton x t2)) - | _ -> failwith (create_type_checker_error pos "The type of Application's first argument must be a Product") + | _ -> (create_infer_type_error pos "The type of Application's first argument must be a Product" term env) end | TermWithTypeAnno (t, tp) -> let (tp, tp_of_tp) = infer_type env tp in begin match tp_of_tp with | Type | Kind -> (check_type env t tp, tp) - | _ -> failwith (create_type_checker_error pos "Type annotation must be a Type or Kind") + | _ -> (create_infer_type_error pos "Type annotation must be a Type or Kind" term env) end | Let (x, t1, t2) -> let (t1, tp_t1) = infer_type env t1 in @@ -209,39 +217,41 @@ let rec infer_type ((_, termEnv) as env : env) ({pos; data = t}: ParserAst.uTerm let (t1, tp_t1) = infer_type env t1 in let _ = add_to_env env x (Opaque tp_t1) in t1, tp_t1 - | Hole x -> failwith (create_type_checker_error pos "Trying to infer the type of a Hole " ^ x) + | Hole x -> (create_infer_type_error pos ("Trying to infer the type of a Hole " ^ x) term env) and check_type ((_, termEnv) as env : env) ({pos; data = t} as term: ParserAst.uTerm) (tp: term) : term = match t with | Type | Var _ | App _ | Product _ | TermWithTypeAnno _ | TypeArrow _ -> let (t, t_tp) = infer_type env term in - if equiv tp t_tp termEnv then t else failwith (create_type_checker_error pos (create_type_checker_error pos "Type mismatch")) + if equiv tp t_tp termEnv then t else (create_check_type_error pos ("The expected type was: " ^ term_to_string t_tp) term tp env) | Lambda (x, None, body) -> begin match to_whnf tp termEnv with | Product (y, y_tp, body_tp) -> let fresh_var = add_to_env env x (Opaque y_tp) in let _ = add_to_termEnv termEnv y (Opaque y_tp) in - let _ = print_endline (x ^ " " ^ Int.to_string y) in + (* let _ = print_endline (x ^ " " ^ Int.to_string y) in *) (* Ask PPO, why substitue y_tp for y in body_tp *) (* let body' = check_type env body (substitute body_tp (VarMap.singleton y y_tp)) in *) let body' = check_type env body body_tp in let _ = rm_from_env env x in Lambda (x, fresh_var, y_tp, body') - | _ -> failwith (create_type_checker_error pos "The type of Lambda must be a Product") + | _ -> (create_check_type_error pos "The type of Lambda must be a Product" term tp env) end | Lambda (x, Some x_tp, body) -> - let _ = print_endline ((uterm_to_string term) ^ " : " ^ term_to_string tp) in + (* let _ = print_endline ((uterm_to_string term) ^ " : " ^ term_to_string tp) in *) begin match (check_type env {pos = pos; data = (Lambda (x, None, body))} tp) with | Lambda (_, _, arg_tp, _) as lambda -> - let _ = print_endline ((term_to_string lambda)) in + (* let _ = print_endline ((term_to_string lambda)) in *) let (x_tp, _) = infer_type env x_tp in - let _ = print_endline ((term_to_string x_tp)) in - let _ = print_endline ((term_to_string arg_tp)) in - if equiv x_tp arg_tp termEnv then lambda else failwith "Type mismatch" - | _ -> failwith (create_type_checker_error pos "Lambda must be lambda lolz") + (* let _ = print_endline ((term_to_string x_tp)) in *) + (* let _ = print_endline ((term_to_string arg_tp)) in *) + if equiv x_tp arg_tp termEnv then lambda else + (create_check_type_error pos + ("Got: " ^ term_to_string x_tp ^ "\nThe expected type of lambda argument was: " ^ term_to_string arg_tp) term tp env) + | _ -> (create_check_type_error pos "Lambda must be lambda lolz" term tp env) end - | Kind -> failwith (create_type_checker_error pos "Kind doesn't have a type") + | Kind -> (create_check_type_error pos "Kind doesn't have a type" term tp env) | Let (x, t1, t2) -> let (t1, tp_t1) = infer_type env t1 in let fresh_var = add_to_env env x (Transparent (t1, tp_t1)) in diff --git a/lib/typeChecker/typeChecker.mli b/lib/typeChecker/typeChecker.mli index 501d340..12dbe12 100644 --- a/lib/typeChecker/typeChecker.mli +++ b/lib/typeChecker/typeChecker.mli @@ -1,5 +1,6 @@ open Ast +open Env open ParserAst val infer_type : env -> uTerm -> term * term -val check_type : env -> uTerm -> term -> term \ No newline at end of file +val check_type : env -> uTerm -> term -> term diff --git a/lib/yaccParser/dune b/lib/yaccParser/dune index 067fdd6..a068bd7 100644 --- a/lib/yaccParser/dune +++ b/lib/yaccParser/dune @@ -1,5 +1,5 @@ (library - (name yaccParser) - (libraries parserAst)) + (name yaccParser) + (libraries parserAst)) -(ocamlyacc yaccParser) \ No newline at end of file +(ocamlyacc yaccParser)