From 3cf472b13c9b329b711a5c254fc6f89268a99eda Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Mon, 8 Jul 2024 23:59:31 +0200
Subject: implement argument lists for top-level definitions

---
 src/elaborator/Elaborator.ml | 27 ++++++++++++++++++++++++---
 1 file changed, 24 insertions(+), 3 deletions(-)

(limited to 'src/elaborator/Elaborator.ml')

diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml
index d15a7f3..6fa44ff 100644
--- a/src/elaborator/Elaborator.ml
+++ b/src/elaborator/Elaborator.ml
@@ -128,14 +128,14 @@ and check_connective connective ~(name : Name.local) ~(base : A.expr) ~(fam : A.
     end
   | _ -> Error.type_mismatch (pp_val()) tp Fmt.string "type"
 
-and check_tp (tp : A.expr) = eval @@ check ~tp:D.Type ~tm:tp
+and check_tp (tp : A.expr) = check ~tp:D.Type ~tm:tp
 
 and infer (tm : A.expr) : D.t * S.t =
   Error.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
   match tm.value with
   | A.Var name -> lookup name
   | A.Check (tm, tp) ->
-    let tp = check_tp tp in
+    let tp = eval @@ check_tp tp in
     let tm = check ~tp ~tm in
     (tp, tm)
   | A.App (fn, arg) -> begin match infer fn with
@@ -170,6 +170,24 @@ and infer (tm : A.expr) : D.t * S.t =
     (motive_scrut, tm)
   | _ -> Error.not_inferable ()
 
+(* elaborating definitions *)
+
+let check_def ~(args : A.arg list) ~(tp : A.expr) ~(tm : A.expr) : S.t * S.t =
+  let check_arg ((arg_name, arg_tp) : A.arg) cont () =
+    let arg_tp = check_tp arg_tp in
+    bind ~name:arg_name.value ~tp:(eval arg_tp) @@ fun _ ->
+    let (tp, tm) = cont () in
+    let tp = S.Pi (arg_name.value, arg_tp, tp) in
+    let tm = S.Lam (arg_name.value, tm) in
+    (tp, tm)
+  in
+  let check_rhs () =
+    let tp = check_tp tp in
+    let tm = check ~tp:(eval tp) ~tm in
+    (tp, tm)
+  in
+  List.fold_right check_arg args check_rhs ()
+
 (* interface *)
 
 let initial_env toplvl : env = {
@@ -187,4 +205,7 @@ let check_tp_toplevel ~(toplvl : TopLevel.t) (tp : A.expr) =
   Eff.run ~env:(initial_env toplvl) @@ fun () -> check_tp tp
 
 let infer_toplevel ~(toplvl : TopLevel.t) (tm : A.expr) =
-  Eff.run ~env:(initial_env toplvl) @@ fun () -> infer tm
\ No newline at end of file
+  Eff.run ~env:(initial_env toplvl) @@ fun () -> infer tm
+
+let check_def_toplevel ~(toplvl : TopLevel.t) ~(args : A.arg list) ~(tp : A.expr) ~(tm : A.expr) =
+  Eff.run ~env:(initial_env toplvl) @@ fun () -> check_def ~args ~tp ~tm
\ No newline at end of file
-- 
cgit 1.4.1