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/ast/Ast.ml               |  1 +
 src/driver/Driver.ml         | 11 +++++++----
 src/elaborator/Elaborator.ml | 27 ++++++++++++++++++++++++---
 src/parser/Grammar.mly       |  4 ++--
 test/bool.toytt              | 21 +++++++++++----------
 5 files changed, 45 insertions(+), 19 deletions(-)

diff --git a/src/ast/Ast.ml b/src/ast/Ast.ml
index 5952977..bbf3e93 100644
--- a/src/ast/Ast.ml
+++ b/src/ast/Ast.ml
@@ -32,6 +32,7 @@ and expr = raw_expr Asai.Range.located
 type item =
   | Def of {
       name : ident;
+      args : arg List.t;
       tp : expr;
       tm : expr;
     }
diff --git a/src/driver/Driver.ml b/src/driver/Driver.ml
index a2c4364..57eec82 100644
--- a/src/driver/Driver.ml
+++ b/src/driver/Driver.ml
@@ -1,9 +1,12 @@
 let process_item (toplvl : TopLevel.t) (item : Ast.item) : TopLevel.t =
   let (name, item) = match item with
-    | Ast.Def { name; tp; tm } ->
-      let tp = Elaborator.check_tp_toplevel ~toplvl tp in
-      let tm = Elaborator.check_toplevel ~toplvl ~tm ~tp in
-      (name, TopLevel.Def { tp; tm = lazy (NbE.eval_toplevel tm) })
+    | Ast.Def { name; args; tp; tm } ->
+      let (tp, tm) = Elaborator.check_def_toplevel ~toplvl ~args ~tp ~tm in
+      let item = TopLevel.Def {
+          tp = NbE.eval_toplevel tp;
+          tm = lazy (NbE.eval_toplevel tm);
+        } in
+      (name, item)
   in
   Yuujinchou.Trie.update_singleton name.value (fun _ -> Some (item, ())) toplvl
 
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
diff --git a/src/parser/Grammar.mly b/src/parser/Grammar.mly
index d49c050..5e4886e 100644
--- a/src/parser/Grammar.mly
+++ b/src/parser/Grammar.mly
@@ -84,8 +84,8 @@ raw_expr:
 expr: e = locate(raw_expr) { e }
 
 item:
-  | DEF; name = ident; COLON; tp = expr; ASSIGN; tm = expr
-    { Def { name; tp; tm } }
+  | DEF; name = ident; args = list(arg); COLON; tp = expr; ASSIGN; tm = expr
+    { Def { name; args; tp; tm } }
 
 file: items = list(item) { items }
 
diff --git a/test/bool.toytt b/test/bool.toytt
index c8e62fd..5f16d20 100644
--- a/test/bool.toytt
+++ b/test/bool.toytt
@@ -1,11 +1,13 @@
-def not : bool -> bool :=
-  \x -> bool-elim x at _ -> bool [
+def id (A : type) (x : A) : A := x
+
+def not (x : bool) : bool :=
+  bool-elim x at _ -> bool [
     true => false,
     false => true
   ]
 
-def and : bool -> bool -> bool :=
-  \x -> \y -> bool-elim x at _ -> bool [
+def and (x : bool) (y : bool) : bool :=
+  bool-elim x at _ -> bool [
     true => bool-elim y at _ -> bool [
       true => true,
       false => false
@@ -13,8 +15,8 @@ def and : bool -> bool -> bool :=
     false => false
   ]
 
-def or : bool -> bool -> bool :=
-  \x -> \y -> bool-elim x at _ -> bool [
+def or (x : bool) (y : bool) : bool :=
+  bool-elim x at _ -> bool [
     true => true,
     false => bool-elim y at _ -> bool [
       true => true,
@@ -22,7 +24,6 @@ def or : bool -> bool -> bool :=
     ]
   ]
 
-def xor : bool -> bool -> bool :=
-  \x -> \y -> or
-    (and x (not y))
-	(and (not x) y)
+def xor (x : bool) (y : bool) : bool :=
+  or (and x (not y))
+     (and (not x) y)
-- 
cgit 1.4.1