From 1b6fc912bfad5a2b0e047835f6778137e4aabe5b Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Sun, 30 Jun 2024 21:31:53 +0200 Subject: improve error messages --- src/bin/main.ml | 2 +- src/elaborator/Elaborator.ml | 40 +++++++++++++++++++++------------------- src/error/Error.ml | 27 +++++++++++++++++---------- 3 files changed, 39 insertions(+), 30 deletions(-) (limited to 'src') diff --git a/src/bin/main.ml b/src/bin/main.ml index 1c466ea..e1be039 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -11,7 +11,7 @@ let ep input = let rec repl () = match LNoise.linenoise "toytt> " with | Some input -> - Error.run ~emit:Term.display ~fatal:Term.display (fun () -> ep input); + Error.run ~emit:(Term.display ~show_backtrace:false) ~fatal:(Term.display ~show_backtrace:false) (fun () -> ep input); let _ = LNoise.history_add input in repl () | None -> repl () diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml index ba1da02..f40076d 100644 --- a/src/elaborator/Elaborator.ml +++ b/src/elaborator/Elaborator.ml @@ -5,8 +5,6 @@ module A = Ast module S = NbE.Syntax module D = NbE.Domain -(* TODO: REALLY improve error messages *) - (* invariant: `tps`, `tms` and `names` all have length `size` *) type env = { tps : D.env; @@ -48,19 +46,23 @@ let eval tm = NbE.eval ~env:(Eff.read()).tms tm (* TODO: this is kind of inelegant, can we do better? *) let eval_at arg = NbE.eval ~env:((Eff.read()).tms <: arg) -let quote v = NbE.quote ~size:(Eff.read()).size v - (** Pretty-printing helpers *) -let pp () = let names = (Eff.read()).names in fun fmt tm -> - Pretty.pp ~names fmt tm +let pp_tm () = + let names = (Eff.read()).names in + fun fmt tm -> Pretty.pp ~names fmt tm + +let pp_val () = + let size = (Eff.read()).size in + let pp_tm = pp_tm () in + fun fmt v -> pp_tm fmt (NbE.quote ~size v) (** Main algorithm *) type connective = [ `Pi | `Sigma ] let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = - Error.tracef ?loc:tm.loc "when checking against the type @[%a@]" (pp()) (quote tp) @@ fun () -> + Error.tracef ?loc:tm.loc "when checking against the type @[%a@]" (pp_val()) tp @@ fun () -> match tm.value with | A.Pi ((name, base), fam) -> check_connective `Pi ~name:name.value ~base ~fam ~tp | A.Fun (base, fam) -> check_connective `Pi ~name:None ~base ~fam ~tp @@ -70,7 +72,7 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = let fib = NbE.inst_clo fam arg in check ~tm:body ~tp:fib in S.Lam (name.value, body) - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" (pp()) (quote tp) + | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "a Pi type" end | A.Sg ((name, base), fam) -> check_connective `Sigma ~name:name.value ~base ~fam ~tp | A.Prod (base, fam) -> check_connective `Sigma ~name:None ~base ~fam ~tp @@ -80,28 +82,28 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = let fib = NbE.inst_clo fam (eval fst) in let snd = check ~tm:snd ~tp:fib in S.Pair (fst, snd) - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (pp()) (quote tp) + | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "a Sigma type" end | A.Type -> begin match tp with (* TODO type-in-type *) | D.Type -> S.Type - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) + | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type" end | A.Bool -> begin match tp with | D.Type -> S.Bool - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) + | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type" end | A.True -> begin match tp with | D.Bool -> S.True - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp) + | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "bool" end | A.False -> begin match tp with | D.Bool -> S.False - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp) + | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "bool" end | _ -> let (inferred_tp, tm) = infer tm in begin try NbE.equate ~size:((Eff.read()).size) inferred_tp tp with | NbE.Unequal -> - Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" (pp()) (quote tp) (pp()) (quote inferred_tp) + Error.type_mismatch (pp_val()) tp (pp_val()) inferred_tp end; tm @@ -114,7 +116,7 @@ and check_connective connective ~(name : Ident.local) ~(base : A.expr) ~(fam : A | `Pi -> S.Pi (name, base, fam) | `Sigma -> S.Sg (name, base, fam) end - | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) + | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type" and infer (tm : A.expr) : D.t * S.t = Error.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> @@ -130,18 +132,18 @@ and infer (tm : A.expr) : D.t * S.t = let tp = NbE.inst_clo fam (eval arg) in let tm = S.App (fn, arg) in (tp, tm) - | _ -> Error.fatalf Error.Message.IllTyped "cannot apply this term because it is not a function" + | (tp, _) -> Error.type_mismatch ?loc:fn.loc Fmt.string "a Pi type" (pp_val()) tp end | A.Fst p -> begin match infer p with | (D.Sg (_, base, _), p) -> (base, S.Fst p) - | _ -> Error.fatalf Error.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type" + | (tp, _) -> Error.type_mismatch ?loc:p.loc Fmt.string "a Sigma type" (pp_val()) tp end | A.Snd p -> begin match infer p with | (D.Sg (_, _, fam), p) -> let tp = NbE.inst_clo fam (eval (S.Fst p)) in let tm = S.Snd p in (tp, tm) - | _ -> Error.fatalf Error.Message.IllTyped "cannot apply second projection to this term because it is of sigma type" + | (tp, _) -> Error.type_mismatch ?loc:p.loc Fmt.string "a Sigma type" (pp_val()) tp end | A.BoolElim { motive_var; motive_body; true_case; false_case; scrut } -> let scrut = check ~tm:scrut ~tp:D.Bool in @@ -154,7 +156,7 @@ and infer (tm : A.expr) : D.t * S.t = let false_case = check ~tm:false_case ~tp:motive_false in let tm = S.BoolElim { motive_var = motive_var.value; motive; true_case; false_case; scrut } in (motive_scrut, tm) - | _ -> Error.fatalf Error.Message.CannotInferType "cannot infer type" + | _ -> Error.not_inferable () let empty_env : env = { tps = Emp; diff --git a/src/error/Error.ml b/src/error/Error.ml index ee04c23..555d41c 100644 --- a/src/error/Error.ml +++ b/src/error/Error.ml @@ -4,8 +4,8 @@ struct | IllegalCharacter | SyntaxError | UnboundVariable - | IllTyped - | CannotInferType + | TypeMismatch + | NotInferable | Bug let default_severity : t -> Asai.Diagnostic.severity = @@ -13,8 +13,8 @@ struct | IllegalCharacter -> Error | SyntaxError -> Error | UnboundVariable -> Error - | IllTyped -> Error - | CannotInferType -> Error + | TypeMismatch -> Error + | NotInferable -> Error | Bug -> Bug let short_code : t -> string = @@ -24,17 +24,24 @@ struct | SyntaxError -> "E102" (* elaboration errors *) | UnboundVariable -> "E201" - | IllTyped -> "E202" - | CannotInferType -> "E202" + | TypeMismatch -> "E202" + | NotInferable -> "E203" (* misc *) | Bug -> "E900" end include Asai.Reporter.Make(Message) -let illegal_character ~loc char = fatalf ~loc IllegalCharacter "illegal character '%s'" (Char.escaped char) -let syntax_error ~loc = fatalf ~loc SyntaxError "syntax error" -let unbound_variable id = fatalf UnboundVariable "unbound variable '%a'" Ident.pp id -let expected_universe fmt x = fatalf IllTyped "expected a universe but got %a" fmt x +let illegal_character ~loc char = fatalf ~loc IllegalCharacter + "illegal character '%s'" (Char.escaped char) +let syntax_error ~loc = fatalf ~loc SyntaxError + "syntax error" +let unbound_variable id = fatalf UnboundVariable + "unbound variable '%a'" Ident.pp id +let type_mismatch ?loc fmt_expected expected fmt_found found = fatalf ?loc TypeMismatch + "@[type mismatch:@,expected: @[%a@]@, found: @[%a@]@]" + fmt_expected expected fmt_found found +let not_inferable () = fatalf NotInferable + "cannot infer type" let bug msg = fatalf Bug msg -- cgit 1.4.1