From fab70aaf2947ff1369757355fbf11437c6db35ff Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Sun, 30 Jun 2024 15:07:02 +0200
Subject: implement syntax for non-dependent function and pair types

---
 src/ast/Ast.ml               |  6 ++++++
 src/elaborator/Elaborator.ml | 31 ++++++++++++++++++-------------
 src/parser/Grammar.mly       |  4 ++++
 src/pretty/Pretty.ml         |  5 +++--
 4 files changed, 31 insertions(+), 15 deletions(-)

(limited to 'src')

diff --git a/src/ast/Ast.ml b/src/ast/Ast.ml
index 1a1d4c5..3a6fac6 100644
--- a/src/ast/Ast.ml
+++ b/src/ast/Ast.ml
@@ -7,9 +7,11 @@ and raw_expr =
   | Var of Ident.t
   | Check of expr * expr
   | Pi of arg * expr
+  | Fun of expr * expr
   | Lam of local_name * expr
   | App of expr * expr
   | Sg of arg * expr
+  | Prod of expr * expr
   | Pair of expr * expr
   | Fst of expr
   | Snd of expr
@@ -52,12 +54,16 @@ and dump_raw_expr fmt = function
       dump_expr scrut
   | Pi (dom, cod) ->
     Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod
+  | Fun (dom, cod) ->
+    Format.fprintf fmt "@[<5>Fun (@[%a@],@ @[%a@])@]" dump_expr dom dump_expr cod
   | Lam (var, body) ->
     Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_local_name var dump_expr body
   | App (fn, arg) ->
     Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg
   | Sg (fst, snd) ->
     Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd
+  | Prod (fst, snd) ->
+    Format.fprintf fmt "@[<6>Prod (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd
   | Pair (fst, snd) ->
     Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr snd
   | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p
diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml
index df2a358..ba1da02 100644
--- a/src/elaborator/Elaborator.ml
+++ b/src/elaborator/Elaborator.ml
@@ -53,19 +53,17 @@ let quote v = NbE.quote ~size:(Eff.read()).size v
 (** Pretty-printing helpers *)
 
 let pp () = let names = (Eff.read()).names in fun fmt tm -> 
-  Pretty.pp ~names fmt tm
+    Pretty.pp ~names fmt tm
 
 (** Main algorithm *)
 
+type connective = [ `Pi | `Sigma ]
+
 let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
   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)
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
+  | A.Pi ((name, base), fam) -> check_connective `Pi ~name:name.value ~base ~fam ~tp
+  | A.Fun (base, fam) -> check_connective `Pi ~name:None ~base ~fam ~tp
   | A.Lam (name, body) -> begin match tp with
       | D.Pi (_, base, fam) -> 
         let body = bind ~name:name.value ~tp:base @@ fun arg ->
@@ -74,12 +72,8 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
         S.Lam (name.value, body)
       | _ -> 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)
-      | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end
+  | A.Sg ((name, base), fam) -> check_connective `Sigma ~name:name.value ~base ~fam ~tp
+  | A.Prod (base, fam) -> check_connective `Sigma ~name:None ~base ~fam ~tp
   | A.Pair (fst, snd) -> begin match tp with
       | D.Sg (_, base, fam) -> 
         let fst = check ~tm:fst ~tp:base in
@@ -111,6 +105,17 @@ let rec check ~(tm : A.expr) ~(tp : D.t) : S.t =
     end;
     tm
 
+and check_connective connective ~(name : Ident.local) ~(base : A.expr) ~(fam : A.expr) ~(tp : D.t) =
+  match tp with
+  | D.Type ->
+    let base = check ~tm:base ~tp in
+    let fam = bind ~name:name ~tp:(eval base) @@ fun _ -> check ~tm:fam ~tp in
+    begin match connective with
+      | `Pi -> S.Pi (name, base, fam)
+      | `Sigma -> S.Sg (name, base, fam)
+    end
+  | _ -> Error.fatalf Error.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp)
+
 and infer (tm : A.expr) : D.t * S.t =
   Error.tracef ?loc:tm.loc "when inferring the type" @@ fun () ->
   match tm.value with
diff --git a/src/parser/Grammar.mly b/src/parser/Grammar.mly
index bb98029..d8e9ee0 100644
--- a/src/parser/Grammar.mly
+++ b/src/parser/Grammar.mly
@@ -47,6 +47,8 @@ raw_expr:
 
   | a = arg; ARROW; b = expr
 	{ Pi (a, b) }
+  | a = expr; ARROW; b = expr
+    { Fun (a, b) }
   | BACKSLASH; a = local_name; ARROW; b = expr
 	{ Lam (a, b) }
   | a = expr; b = expr %prec APP
@@ -54,6 +56,8 @@ raw_expr:
 
   | a = arg; ASTERISK; b = expr
 	{ Sg (a, b) }
+  | a = expr; ASTERISK; b = expr
+	{ Prod (a, b) }
   | LPR; a = expr; COMMA; b = expr; RPR
 	{ Pair (a, b) }
   | FST; p = expr
diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml
index ba78881..8b7ad1a 100644
--- a/src/pretty/Pretty.ml
+++ b/src/pretty/Pretty.ml
@@ -67,8 +67,9 @@ struct
        pp scrut pp_local_name motive_var (bind motive_var pp) motive pp true_case pp false_case
     ) fmt
 
-  and pp_arg fmt (name, tp) =
-    Fmt.pf fmt "(@[%a@] : @[%a@])" pp_local_name name pp tp
+  and pp_arg fmt (name, tp) = match name with
+    | Some name -> (delimited @@ fun fmt (name, tp) -> Fmt.pf fmt "(@[%s@] : @[%a@])" name pp tp) fmt (name, tp)
+    | None -> pp fmt tp
 
   (* TODO: improve indentation *)
   and pp fmt = function
-- 
cgit 1.4.1