aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/bin/dune2
-rw-r--r--src/bin/main.ml4
-rw-r--r--src/elaborator/Elaborator.ml34
-rw-r--r--src/elaborator/dune2
-rw-r--r--src/error/Error.ml (renamed from src/reporter/Reporter.ml)0
-rw-r--r--src/error/dune4
-rw-r--r--src/nbe/dune2
-rw-r--r--src/parser/Parser.ml4
-rw-r--r--src/parser/dune2
-rw-r--r--src/pretty/Pretty.ml2
-rw-r--r--src/pretty/dune2
-rw-r--r--src/reporter/dune4
12 files changed, 31 insertions, 31 deletions
diff --git a/src/bin/dune b/src/bin/dune
index 980d799..f11979a 100644
--- a/src/bin/dune
+++ b/src/bin/dune
@@ -7,5 +7,5 @@
toytt.elaborator
toytt.nbe
toytt.parser
- toytt.reporter
+ toytt.error
))
diff --git a/src/bin/main.ml b/src/bin/main.ml
index f762d26..1c466ea 100644
--- a/src/bin/main.ml
+++ b/src/bin/main.ml
@@ -1,4 +1,4 @@
-module Term = Asai.Tty.Make(Reporter.Message)
+module Term = Asai.Tty.Make(Error.Message)
let ep input =
let ast = Parser.parse_expr input in
@@ -11,7 +11,7 @@ let ep input =
let rec repl () =
match LNoise.linenoise "toytt> " with
| Some input ->
- Reporter.run ~emit:Term.display ~fatal:Term.display (fun () -> ep input);
+ Error.run ~emit:Term.display ~fatal:Term.display (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 0f72f24..df2a358 100644
--- a/src/elaborator/Elaborator.ml
+++ b/src/elaborator/Elaborator.ml
@@ -26,9 +26,9 @@ let lookup (id : Ident.t) : D.t * S.t = match Ident.to_local id with
| Some ix ->
let tp = Bwd.nth env.tps ix in
(tp, S.Var ix)
- | None -> Reporter.unbound_variable id
+ | None -> Error.unbound_variable id
end
- | None -> Reporter.unbound_variable id
+ | None -> Error.unbound_variable id
let bind ~(name : Ident.local) ~(tp : D.t) f =
let arg = D.var (Eff.read()).size in
@@ -58,61 +58,61 @@ let pp () = let names = (Eff.read()).names in fun fmt tm ->
(** Main algorithm *)
let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
- Reporter.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()) (quote tp) @@ fun () ->
match tm.value with
| A.Pi ((name, base), fam) -> begin match tp with
| D.Type ->
let base = check ~tm:base ~tp in
let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in
S.Pi (name.value, base, fam)
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
| A.Lam (name, body) -> begin match tp with
| D.Pi (_, base, fam) ->
let body = bind ~name:name.value ~tp:base @@ fun arg ->
let fib = NbE.inst_clo fam arg in
check ~tm:body ~tp:fib in
S.Lam (name.value, body)
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" (pp()) (quote tp)
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" (pp()) (quote tp)
end
| A.Sg ((name, base), fam) -> begin match tp with
| D.Type ->
let base = check ~tm:base ~tp in
let fam = bind ~name:name.value ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in
S.Sg (name.value, base, fam)
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
| A.Pair (fst, snd) -> begin match tp with
| D.Sg (_, base, fam) ->
let fst = check ~tm:fst ~tp:base in
let fib = NbE.inst_clo fam (eval fst) in
let snd = check ~tm:snd ~tp:fib in
S.Pair (fst, snd)
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (pp()) (quote tp)
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (pp()) (quote tp)
end
| A.Type -> begin match tp with (* TODO type-in-type *)
| D.Type -> S.Type
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
end
| A.Bool -> begin match tp with
| D.Type -> S.Bool
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
end
| A.True -> begin match tp with
| D.Bool -> S.True
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
end
| A.False -> begin match tp with
| D.Bool -> S.False
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
+ | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (pp()) (quote tp)
end
| _ -> let (inferred_tp, tm) = infer tm in begin
try NbE.equate ~size:((Eff.read()).size) inferred_tp tp with
| NbE.Unequal ->
- Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" (pp()) (quote tp) (pp()) (quote inferred_tp)
+ 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)
end;
tm
and infer (tm : A.expr) : D.t * S.t =
- Reporter.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
+ Error.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
match tm.value with
| A.Var name -> lookup name
| A.Check (tm, tp) ->
@@ -125,18 +125,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)
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "cannot apply this term because it is not a function"
+ | _ -> Error.fatalf Error.Message.IllTyped "cannot apply this term because it is not a function"
end
| A.Fst p -> begin match infer p with
| (D.Sg (_, base, _), p) -> (base, S.Fst p)
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type"
+ | _ -> Error.fatalf Error.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type"
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)
- | _ -> Reporter.fatalf Reporter.Message.IllTyped "cannot apply second projection to this term because it is of sigma type"
+ | _ -> Error.fatalf Error.Message.IllTyped "cannot apply second projection to this term because it is of sigma type"
end
| A.BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
let scrut = check ~tm:scrut ~tp:D.Bool in
@@ -149,7 +149,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)
- | _ -> Reporter.fatalf Reporter.Message.CannotInferType "cannot infer type"
+ | _ -> Error.fatalf Error.Message.CannotInferType "cannot infer type"
let empty_env : env = {
tps = Emp;
diff --git a/src/elaborator/dune b/src/elaborator/dune
index 46227f0..941027a 100644
--- a/src/elaborator/dune
+++ b/src/elaborator/dune
@@ -8,4 +8,4 @@
toytt.ident
toytt.nbe
toytt.pretty
- toytt.reporter))
+ toytt.error))
diff --git a/src/reporter/Reporter.ml b/src/error/Error.ml
index ee04c23..ee04c23 100644
--- a/src/reporter/Reporter.ml
+++ b/src/error/Error.ml
diff --git a/src/error/dune b/src/error/dune
new file mode 100644
index 0000000..857f7bc
--- /dev/null
+++ b/src/error/dune
@@ -0,0 +1,4 @@
+(library
+ (name Error)
+ (public_name toytt.error)
+ (libraries asai toytt.ident))
diff --git a/src/nbe/dune b/src/nbe/dune
index b7c9bed..3e62347 100644
--- a/src/nbe/dune
+++ b/src/nbe/dune
@@ -1,4 +1,4 @@
(library
(name NbE)
(public_name toytt.nbe)
- (libraries algaeff bwd toytt.ident toytt.reporter))
+ (libraries algaeff bwd toytt.ident toytt.error))
diff --git a/src/parser/Parser.ml b/src/parser/Parser.ml
index 4593d82..88448c9 100644
--- a/src/parser/Parser.ml
+++ b/src/parser/Parser.ml
@@ -8,6 +8,6 @@ let parse_expr (s : string) : Ast.expr =
Eff.run ~env:source @@ fun () ->
try Grammar.start_expr Lexer.token lexbuf with
| Lexer.IllegalCharacter illegal_char ->
- Reporter.illegal_character ~loc:(Asai.Range.of_lexbuf ~source lexbuf) illegal_char
+ Error.illegal_character ~loc:(Asai.Range.of_lexbuf ~source lexbuf) illegal_char
| Grammar.Error ->
- Reporter.syntax_error ~loc:(Asai.Range.of_lexbuf ~source lexbuf)
+ Error.syntax_error ~loc:(Asai.Range.of_lexbuf ~source lexbuf)
diff --git a/src/parser/dune b/src/parser/dune
index fd4aae7..7a1b290 100644
--- a/src/parser/dune
+++ b/src/parser/dune
@@ -10,4 +10,4 @@
(libraries
asai
toytt.ast
- toytt.reporter))
+ toytt.error))
diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml
index 66d6159..ba78881 100644
--- a/src/pretty/Pretty.ml
+++ b/src/pretty/Pretty.ml
@@ -57,7 +57,7 @@ struct
| Some ((Some name) as id) when Bwd.find_index ((=) id) names = Some ix -> Fmt.string fmt name
(* the variable does not have a bound name or its bound name has been shadowed *)
| Some _ -> Fmt.pf fmt "%@%d" ix
- | None -> Reporter.bug "index out of range in pp_var"
+ | None -> Error.bug "index out of range in pp_var"
let rec pp_pair fmt = (delimited @@ fun fmt (a, b) -> Fmt.pf fmt "@[(@[%a@], @[%a@])@]" pp a pp b) fmt
diff --git a/src/pretty/dune b/src/pretty/dune
index df46822..ee17573 100644
--- a/src/pretty/dune
+++ b/src/pretty/dune
@@ -6,4 +6,4 @@
fmt
toytt.ident
toytt.nbe
- toytt.reporter))
+ toytt.error))
diff --git a/src/reporter/dune b/src/reporter/dune
deleted file mode 100644
index ab0f04a..0000000
--- a/src/reporter/dune
+++ /dev/null
@@ -1,4 +0,0 @@
-(library
- (name Reporter)
- (public_name toytt.reporter)
- (libraries asai toytt.ident))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 13:15:46 +0000