From 169ff6c0d196246e28c4413b43895ad5a377a2e5 Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Fri, 16 Feb 2024 16:18:32 +0100
Subject: add type universe to grammar

---
 bin/main.ml    |  2 +-
 lib/Ast.ml     | 38 ++++++++++++++++++++------------------
 lib/Lexer.mll  |  1 +
 lib/Parser.mly |  4 ++++
 4 files changed, 26 insertions(+), 19 deletions(-)

diff --git a/bin/main.ml b/bin/main.ml
index 1607ec4..6c62764 100644
--- a/bin/main.ml
+++ b/bin/main.ml
@@ -8,7 +8,7 @@ let parse (s : string) : Ast.expr =
 let rec repl () =
   let input = read_line () in
   let ast = parse input in
-  Format.printf "%a\n%!" Ast.dump_expr ast;
+  Format.printf "%a\n%!" Ast.pp_expr ast;
   repl ()
 
 let () = repl ()
diff --git a/lib/Ast.ml b/lib/Ast.ml
index 002dfff..f7c90dd 100644
--- a/lib/Ast.ml
+++ b/lib/Ast.ml
@@ -23,40 +23,42 @@ and raw_expr =
   | Pair of expr * expr
   | Fst of expr
   | Snd of expr
+  | Type
 
 and expr = raw_expr Asai.Range.located
 
-let dump_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id
-let dump_ident fmt ({ value; _ } : ident) = dump_raw_ident fmt value
+let pp_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id
+let pp_ident fmt ({ value; _ } : ident) = pp_raw_ident fmt value
 
-let rec dump_raw_arg fmt ({ name; ty } : raw_arg) =
-  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr ty
+let rec pp_raw_arg fmt ({ name; ty } : raw_arg) =
+  Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" pp_ident name pp_expr ty
 
-and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value
+and pp_arg fmt ({ value; _ } : arg) = pp_raw_arg fmt value
 
-and dump_raw_expr fmt = function
-  | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id
+and pp_raw_expr fmt = function
+  | Var id -> Format.fprintf fmt "Var @[%a@]" pp_raw_ident id
   | Bool -> Format.pp_print_string fmt "Bool"
   | True -> Format.pp_print_string fmt "True"
   | False -> Format.pp_print_string fmt "False"
   | BoolElim { motive_var; motive_body; true_case; false_case; scrut } ->
       Format.fprintf fmt
-        "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]" dump_ident
-        motive_var dump_expr motive_body dump_expr true_case dump_expr
-        false_case dump_expr scrut
+        "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]" pp_ident
+        motive_var pp_expr motive_body pp_expr true_case pp_expr
+        false_case pp_expr scrut
   | Pi (dom, cod) ->
-      Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod
+      Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" pp_arg dom pp_expr cod
   | Lam (var, body) ->
-      Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr
+      Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" pp_ident var pp_expr
         body
   | App (fn, arg) ->
-      Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg
+      Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" pp_expr fn pp_expr arg
   | Sg (fst, snd) ->
-      Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd
+      Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" pp_arg fst pp_expr snd
   | Pair (fst, snd) ->
-      Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr
+      Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" pp_expr fst pp_expr
         snd
-  | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p
-  | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p
+  | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" pp_expr p
+  | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" pp_expr p
+  | Type -> Format.pp_print_string fmt "Type"
 
-and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value
+and pp_expr fmt ({ value; _ } : expr) = pp_raw_expr fmt value
diff --git a/lib/Lexer.mll b/lib/Lexer.mll
index 55a22c2..a8410d0 100644
--- a/lib/Lexer.mll
+++ b/lib/Lexer.mll
@@ -27,5 +27,6 @@ rule lex =
   | "at" { AT }
   | "fst" { FST }
   | "snd" { SND }
+  | "type" { TYPE }
   | ident { IDENT (Lexing.lexeme lexbuf) }
   | eof { EOF }
diff --git a/lib/Parser.mly b/lib/Parser.mly
index db2a9e2..5c587b2 100644
--- a/lib/Parser.mly
+++ b/lib/Parser.mly
@@ -8,6 +8,7 @@ open Ast
 %token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW
 %token BOOL TRUE FALSE BOOL_ELIM AT
 %token FST SND
+%token TYPE
 %token EOF
 
 %right ARROW ASTERISK
@@ -60,6 +61,9 @@ raw_expr:
   | SND; p = expr
 	{ Snd p }
 
+  | TYPE
+	{ Type }
+
 %inline
 expr: e = locate(raw_expr) { e }
 
-- 
cgit 1.4.1