aboutsummaryrefslogtreecommitdiff
path: root/lib/Elab.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Elab.ml')
-rw-r--r--lib/Elab.ml163
1 files changed, 163 insertions, 0 deletions
diff --git a/lib/Elab.ml b/lib/Elab.ml
new file mode 100644
index 0000000..5bda770
--- /dev/null
+++ b/lib/Elab.ml
@@ -0,0 +1,163 @@
+open Bwd
+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;
+ size : int;
+}
+
+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 define ~(name : A.raw_ident) ~(tp : D.t) ~(tm : D.t) f =
+ let update env = {
+ tps = env.tps <: tp;
+ tms = env.tms <: tm;
+ names = env.names <: Some 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)
+
+(** NbE helpers *)
+
+let eval tm = Eval.eval ~env:(Eff.read()).tms tm
+
+(** Evaluate under the current environment augmented by `arg` *)
+(* TODO: this is kind of inelegant, can we do better? *)
+let eval_at arg = Eval.eval ~env:((Eff.read()).tms <: arg)
+
+let quote v = Quote.quote ~size:(Eff.read()).size v
+
+(** 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 () ->
+ 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
+ | A.Lam (name, body) -> begin match tp with
+ | 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)
+ 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
+ | A.Pair (fst, snd) -> begin match tp with
+ | 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ 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)
+ end;
+ tm
+
+and infer (tm : A.expr) : D.t * S.t =
+ R.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
+ match tm.value with
+ | A.Var name -> lookup_name 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) ->
+ 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"
+ 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"
+ end
+ | A.Snd p -> begin match infer p with
+ | (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"
+ end
+ | A.BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
+ let scrut = check ~tm:scrut ~tp:D.Bool in
+ let motive = bind ~name:motive_var.value ~tp:D.Bool @@ fun _ ->
+ check ~tm:motive_body ~tp:D.Type in
+ let motive_true = eval_at D.True motive in
+ let motive_false = eval_at D.False motive in
+ 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
+ (motive_scrut, tm)
+ | _ -> R.fatalf R.Message.CannotInferType "cannot infer type"
+
+let empty_env : env = {
+ tps = Emp;
+ tms = Emp;
+ names = Emp;
+ size = 0;
+}
+
+let infer_toplevel (tm : A.expr) = Eff.run ~env:empty_env @@ fun () -> infer tm \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-20 09:01:39 +0000