From 8d40541003736d5319ec981278338e8c8c66daf6 Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Sun, 23 Jun 2024 01:36:48 +0200 Subject: keep track of bound names everywhere to be able to output names instead of de bruijn indices --- lib/Elab.ml | 94 ++++++++++++++++++++++++++++++------------------------------- 1 file changed, 46 insertions(+), 48 deletions(-) (limited to 'lib/Elab.ml') diff --git a/lib/Elab.ml b/lib/Elab.ml index 5bda770..d911b9f 100644 --- a/lib/Elab.ml +++ b/lib/Elab.ml @@ -4,19 +4,14 @@ open Bwd.Infix module A = Ast module S = Syntax module D = Domain -module R = Reporter (* TODO: REALLY improve error messages *) -(* `None` means that an underscore was used in the binder *) -(* TODO: actually implement this *) -type local_name = Yuujinchou.Trie.path option - (* invariant: `tps`, `tms` and `names` all have length `size` *) type env = { tps : D.env; tms : D.env; - names : local_name bwd; + names : Ident.local bwd; size : int; } @@ -24,28 +19,26 @@ module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) (** General helpers *) -let lookup_name name : D.t * S.t = - let env = Eff.read() in - match Bwd.find_index ((=) (Some name)) env.names with - | Some ix -> - let tp = Bwd.nth env.tps ix in - let tm = Quote.quote ~size:env.size (Bwd.nth env.tms ix) in - (tp, tm) - | None -> R.fatalf R.Message.UnboundVariable - "unbound variable @[%a@]" S.Pretty.pp_name name +let lookup (id : Ident.t) : D.t * S.t = match Ident.to_local id with + | Some name -> begin + let env = Eff.read() in + match Bwd.find_index ((=) name) env.names with + | Some ix -> + let tp = Bwd.nth env.tps ix in + (tp, S.Var ix) + | None -> Reporter.unbound_variable id + end + | None -> Reporter.unbound_variable id -let define ~(name : A.raw_ident) ~(tp : D.t) ~(tm : D.t) f = +let bind ~(name : Ident.local) ~(tp : D.t) f = + let arg = D.var (Eff.read()).size in let update env = { tps = env.tps <: tp; - tms = env.tms <: tm; - names = env.names <: Some name; + tms = env.tms <: arg; + names = env.names <: name; size = env.size + 1; } in - Eff.scope update f - -let bind ~(name : A.raw_ident) ~(tp : D.t) f = - let arg = D.var (Eff.read()).size in - define ~name ~tp ~tm:arg (fun () -> f arg) + Eff.scope update (fun () -> f arg) (** NbE helpers *) @@ -57,88 +50,93 @@ let eval_at arg = Eval.eval ~env:((Eff.read()).tms <: arg) let quote v = Quote.quote ~size:(Eff.read()).size v +(** Pretty-printing helpers *) + +let pp () = let names = (Eff.read()).names in fun fmt tm -> + Syntax.Pretty.pp fmt (tm, names) + (** Main algorithm *) let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = - R.tracef ?loc:tm.loc "when checking against the type @[%a@]" Syntax.Pretty.pp (quote tp) @@ fun () -> + Reporter.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 (base, fam) - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end + 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 | A.Lam (name, body) -> begin match tp with - | D.Pi (base, fam) -> + | D.Pi (_, base, fam) -> let body = bind ~name:name.value ~tp:base @@ fun arg -> let fib = Eval.inst_clo fam arg in check ~tm:body ~tp:fib in - S.Lam body - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" Syntax.Pretty.pp (quote tp) + 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) 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 (base, fam) - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end + 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 | A.Pair (fst, snd) -> begin match tp with - | D.Sg (base, fam) -> + | D.Sg (_, base, fam) -> let fst = check ~tm:fst ~tp:base in let fib = Eval.inst_clo fam (eval fst) in let snd = check ~tm:snd ~tp:fib in S.Pair (fst, snd) - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" Syntax.Pretty.pp (quote tp) + | _ -> Reporter.fatalf Reporter.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 - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) + | _ -> Reporter.fatalf Reporter.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 - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) + | _ -> Reporter.fatalf Reporter.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 - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.pp (quote tp) + | _ -> Reporter.fatalf Reporter.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 - | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.pp (quote tp) + | _ -> Reporter.fatalf Reporter.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 Conversion.equate ~size:((Eff.read()).size) inferred_tp tp with | Conversion.Unequal -> - R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" Syntax.Pretty.pp (quote tp) Syntax.Pretty.pp (quote inferred_tp) + 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) end; tm and infer (tm : A.expr) : D.t * S.t = - R.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> + Reporter.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> match tm.value with - | A.Var name -> lookup_name name + | A.Var name -> lookup name | A.Check (tm, tp) -> let tp = eval @@ check ~tp:D.Type ~tm:tp in let tm = check ~tp ~tm in (tp, tm) | A.App (fn, arg) -> begin match infer fn with - | (D.Pi (base, fam), fn) -> + | (D.Pi (_, base, fam), fn) -> let arg = check ~tm:arg ~tp:base in let tp = Eval.inst_clo fam (eval arg) in let tm = S.App (fn, arg) in (tp, tm) - | _ -> R.fatalf R.Message.IllTyped "cannot apply this term because it is not a function" + | _ -> Reporter.fatalf Reporter.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) - | _ -> R.fatalf R.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type" + | (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" end | A.Snd p -> begin match infer p with - | (D.Sg (_, fam), p) -> + | (D.Sg (_, _, fam), p) -> let tp = Eval.inst_clo fam (eval (S.Fst p)) in let tm = S.Snd p in (tp, tm) - | _ -> R.fatalf R.Message.IllTyped "cannot apply second projection to this term because it is of sigma type" + | _ -> Reporter.fatalf Reporter.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,9 +147,9 @@ and infer (tm : A.expr) : D.t * S.t = let motive_scrut = eval_at (eval scrut) motive in let true_case = check ~tm:true_case ~tp:motive_true in let false_case = check ~tm:false_case ~tp:motive_false in - let tm = S.BoolElim { motive; true_case; false_case; scrut } in + let tm = S.BoolElim { motive_var = motive_var.value; motive; true_case; false_case; scrut } in (motive_scrut, tm) - | _ -> R.fatalf R.Message.CannotInferType "cannot infer type" + | _ -> Reporter.fatalf Reporter.Message.CannotInferType "cannot infer type" let empty_env : env = { tps = Emp; -- cgit 1.4.1