aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--README.md2
-rw-r--r--src/bin/main.ml2
-rw-r--r--src/elaborator/Elaborator.ml40
-rw-r--r--src/error/Error.ml27
4 files changed, 40 insertions, 31 deletions
diff --git a/README.md b/README.md
index 40bfde5..80cc8ba 100644
--- a/README.md
+++ b/README.md
@@ -29,7 +29,7 @@ not-function applied to `false` (which evaluates to `true`).
- [x] figure out how to recover variable names in pretty-printing so we don't
have to print de bruijn indices all the time
- [x] build a better repl
-- [ ] improve error messages
+- [x] improve error messages
- [ ] implement top-level definitions
- [x] implement less aggrevating syntax for non-dependent function & pair types
- [ ] add a type of natural numbers
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
+ "@[<v>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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 13:59:26 +0000