From b34ebf3fe3ecaf292be873d231dd54c80f16ad07 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 24 Jun 2024 00:24:24 +0200 Subject: rename: Reporter -> Error --- src/bin/dune | 2 +- src/bin/main.ml | 4 ++-- src/elaborator/Elaborator.ml | 34 +++++++++++++++++----------------- src/elaborator/dune | 2 +- src/error/Error.ml | 40 ++++++++++++++++++++++++++++++++++++++++ src/error/dune | 4 ++++ src/nbe/dune | 2 +- src/parser/Parser.ml | 4 ++-- src/parser/dune | 2 +- src/pretty/Pretty.ml | 2 +- src/pretty/dune | 2 +- src/reporter/Reporter.ml | 40 ---------------------------------------- src/reporter/dune | 4 ---- 13 files changed, 71 insertions(+), 71 deletions(-) create mode 100644 src/error/Error.ml create mode 100644 src/error/dune delete mode 100644 src/reporter/Reporter.ml delete mode 100644 src/reporter/dune (limited to 'src') 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/error/Error.ml b/src/error/Error.ml new file mode 100644 index 0000000..ee04c23 --- /dev/null +++ b/src/error/Error.ml @@ -0,0 +1,40 @@ +module Message = +struct + type t = + | IllegalCharacter + | SyntaxError + | UnboundVariable + | IllTyped + | CannotInferType + | Bug + + let default_severity : t -> Asai.Diagnostic.severity = + function + | IllegalCharacter -> Error + | SyntaxError -> Error + | UnboundVariable -> Error + | IllTyped -> Error + | CannotInferType -> Error + | Bug -> Bug + + let short_code : t -> string = + function + (* parser errors *) + | IllegalCharacter -> "E101" + | SyntaxError -> "E102" + (* elaboration errors *) + | UnboundVariable -> "E201" + | IllTyped -> "E202" + | CannotInferType -> "E202" + (* 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 bug msg = fatalf Bug msg 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/Reporter.ml b/src/reporter/Reporter.ml deleted file mode 100644 index ee04c23..0000000 --- a/src/reporter/Reporter.ml +++ /dev/null @@ -1,40 +0,0 @@ -module Message = -struct - type t = - | IllegalCharacter - | SyntaxError - | UnboundVariable - | IllTyped - | CannotInferType - | Bug - - let default_severity : t -> Asai.Diagnostic.severity = - function - | IllegalCharacter -> Error - | SyntaxError -> Error - | UnboundVariable -> Error - | IllTyped -> Error - | CannotInferType -> Error - | Bug -> Bug - - let short_code : t -> string = - function - (* parser errors *) - | IllegalCharacter -> "E101" - | SyntaxError -> "E102" - (* elaboration errors *) - | UnboundVariable -> "E201" - | IllTyped -> "E202" - | CannotInferType -> "E202" - (* 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 bug msg = fatalf Bug msg 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)) -- cgit 1.4.1