dtlc

commit 795ed7b03d11afeb39e89d07dbface2f7d2ff9f7
parent 89fa2d5bb5b1e8fb745e6321a4ff9b39e7537592
Author: Robert Russell <robertrussell.72001@gmail.com>
Date:   Fri, 15 Dec 2023 14:47:28 -0800

It works!

Diffstat:
M
Makefile
 | 
2
+-
M
concrete.ml
 | 
26
--------------------------
M
core.ml
 | 
28
++++++++++++++++++----------
M
elab.ml
 | 
212
+++++++++++++++++++++++++++++++++++++++++++++++++------------------------------
D
elab2.ml
 | 
136
-------------------------------------------------------------------------------
M
eval.ml
 | 
15
+++++----------
M
main.ml
 | 
12
++++++++----
M
parser.mly
 | 
8
+++++---
D
surf.ml
 | 
40
----------------------------------------

9 files changed, 170 insertions(+), 309 deletions(-)
diff --git a/Makefile b/Makefile
@@ -1,4 +1,4 @@
-main: common.ml concrete.ml parser.ml lexer.ml abstract.ml conctoabs.ml
+main: common.ml concrete.ml parser.ml lexer.ml abstract.ml conctoabs.ml core.ml value.ml eval.ml elab.ml main.ml
 	ocamlfind ocamlopt -o $@ -g -linkpkg -package zarith $^
 
 lexer.ml: lexer.mll
diff --git a/concrete.ml b/concrete.ml
@@ -26,29 +26,3 @@ type expr =
 | Underscore
 | Ident of ident
 and case = Case of {patt: expr; guard: expr option; body: expr}
-
-(*
-let rec string_of_expr m e =
-	let sp = string_of_patt in
-	let se = string_of_expr in
-	let (c, s) = match e with
-	| Let (p, a, b) -> (0, "let " ^ sp 0 p ^ " = " ^ se 1 a ^ "; " ^ se 0 b)
-	| If (c, t, f) -> (0, "if " ^ se 1 c ^ " then " ^ se 1 t ^ " else " ^ se 1 f)
-	| Fn (p, e) -> (1, "@(" ^ sp 0 p ^ ") -> " ^ se 1 e)
-	| Pi (p, e) -> (1, "#(" ^ sp 0 p ^ ") -> " ^ se 1 e)
-	| Hint (a, b) -> (1, se 2 a ^ " : " ^ se 1 b)
-	| Plus (a, b) -> (2, se 2 a ^ " + " ^ se 3 b)
-	| Asterisk (a, b) -> (3, se 3 a ^ " * " ^ se 4 b)
-	| Apposition (a, b) -> (4, se 4 a ^ " " ^ se 5 b)
-	| Var x -> (5, x)
-	| Int z -> (5, Z.to_string z) in
-	if c < m then "(" ^ s ^ ")" else s
-
-and string_of_patt m p =
-	let sp = string_of_patt in
-	let se = string_of_expr in
-	let (c, s) = match p with
-	| Annot (p, e) -> (0, sp 1 p ^ " : " ^ se 1 e)
-	| Wild x -> (1, x) in
-	if c < m then "(" ^ s ^ ")" else s
-*)
diff --git a/core.ml b/core.ml
@@ -21,13 +21,21 @@ and patt_discriminant =
 | PattDiscFalse
 | PattDiscData of ident * int
 
-(*
-TODO:
-1. copy over elab code
-2. test
-3. add support for constants
-4. add support for ADTs
-5. staging
-6. ...
-7. quantities (0, ω)
-*)
+let rec to_string m e =
+	let s = to_string in
+	let (c, s) = match e with
+	| Let _ -> failwith "no impl: let"
+	| Case _ -> failwith "no impl: case"
+	| App (f, args) -> (6, String.concat " " (List.map (s 7) (f :: args)))
+	| Fn (arity, body) -> (1, "fn " ^ string_of_int arity ^ " => " ^ s 1 body)
+	| FnType (_, doms, cod) ->
+		let sdoms = match doms with
+		| dom :: [] -> s 4 dom
+		| doms -> "(" ^ String.concat ", " (List.map (s 1) doms) ^ ")" in
+		(3, sdoms ^ " -> " ^ s 3 cod)
+	| Nat n -> (8, Z.to_string n)
+	| Var i -> (8, "?" ^ string_of_int i)
+	| Intrin Type -> (8, "`Type")
+	| Intrin NatType -> (8, "`Nat")
+	| Intrin NatOpAdd -> (8, "`+") in
+	if c < m then "(" ^ s ^ ")" else s
diff --git a/elab.ml b/elab.ml
@@ -1,99 +1,153 @@
 open Common
-module S = Surf
+open Eval
+module A = Abstract
 module C = Core
 module V = Value
 
 type context = {
-	env: V.environ;
-	free: (ident * V.value) list;
+	len: int;
+	names: ident option list;
+	values: V.value list;
+	types: V.value list;
 }
 
-let let_bind ctx x t v = {
-	env = v :: ctx.env;
-	free = (x, t) :: ctx.free;
+let default_ctx = {
+	len = 3;
+	names = [Some "`+"; Some "Nat"; Some "Type"];
+	values = [V.Intrin C.NatOpAdd; V.Intrin C.NatType; V.Intrin C.Type];
+	types =
+		let nat_op_add_type = V.FnType (
+			[],
+			2,
+			[C.Intrin C.NatType; C.Intrin C.NatType],
+			C.Intrin C.NatType
+		) in
+		[nat_op_add_type; V.Intrin C.Type; V.Intrin C.Type];
 }
 
-let var_bind ctx x t = let_bind ctx x t (V.Var (List.length ctx.env))
+(* Add `x := v : t` to ctx. *)
+let bind_def ctx x v t = {
+	len = 1 + ctx.len;
+	names = x :: ctx.names;
+	values = v :: ctx.values;
+	types = t :: ctx.types;
+}
 
-let rec check ctx a t = match a, t with
-| S.Let (p, a, b), t ->
-	let (ca, ta, x) = infer_with_patt ctx a p in
-	let va = eval ctx.env ca in
-	let cb = check (let_bind ctx x ta va) sb t in
-	C.Let (x, ca, cb)
-| S.Fn (p, a), V.Pi (_, dom, cod) ->
-	let x = check_patt ctx p dom in
-	let ca = check (var_bind ctx x dom) a (apply cod (V.Var (List.length ctx.env))) in
-	C.Fn (x, ca)
-| a, t ->
-	let (ca, u) = infer ctx a in
-	if conv (List.length ctx.env) t u then ca else failwith "type error"
+(* Add `x : t` to ctx. *)
+let bind_arb ctx x t = bind_def ctx x (V.Arb ctx.len) t
 
-and infer ctx a = match a with
-| S.Let (p, a, b) ->
-	let (ca, ta, x) = infer_with_patt ctx a p in
-	let va = eval ctx.env ca in
-	let (cb, tb) = infer (let_bind ctx x ta va) sb in
-	(C.Let (x, ca, cb), tb)
-| S.Fn (p, a) ->
-	let (x, t) = infer_patt ctx p in
-	let (ca, u) = infer (var_bind ctx x t) a in
-	(C.Fn (x, ca), V.Pi ("α", t, capture ctx.env (quote (List.length ctx.env) u)))
-| S.Pi (x, dom, cod) ->
-	let cdom = check ctx dom V.Type in
-	let vdom = eval ctx.env cdom in
-	let ccod = check (var_bind ctx x vdom) cod V.Type in
-	(C.Pi (x, cdom, ccod), V.Type)
-| S.Hint (a, b) ->
-	let cb = check ctx b V.Type in
-	let vb = eval ctx.env cb in
-	let ca = check ctx a vb in
-	(ca, vb)
-| S.Plus (a, b) -> infer ctx (App ())
-	let c0 = check ctx s0 VNat in
-	let c1 = check ctx s1 VNat in
-	(CAdd (c0, c1), VNat)
+let rec bind_arb_telescope ctx xs ts = match xs, ts with
+| x :: xs, t :: ts -> bind_arb_telescope (bind_arb ctx x t) xs ts
+| [], [] -> ctx
+| _, _ -> failwith "impossible"
 
-| SVar x ->
-	let rec go i = function
-	| [] -> failwith ("variable '" ^ x ^ "' out of scope")
-	| (y, v) :: rest -> if x = y then (CVar i, v) else go (i + 1) rest in
-	go 0 ctx.free
-| SType -> (CType, VType)
-| SApp (s0, s1) ->
-	let (c0, t0) = infer ctx s0 in
-	begin match t0 with
-	| VPi (dom, cod) ->
-		let c1 = check ctx s1 dom in
-		(CApp (c0, c1), apply cod (eval ctx.env c1))
+let rec infer ctx = function
+| A.Match _ -> failwith "no impl: match"
+| A.Annot (a, t) ->
+	let ct = check ctx t (V.Intrin C.Type) in
+	let vt = eval ctx.values ct in
+	let ca = check ctx a vt in
+	(ca, vt)
+| A.App (f, args) ->
+	let (cf, tf) = infer ctx f in
+	begin match tf with
+	| V.FnType (env, arity, doms, cod) ->
+		if List.length args <> arity then failwith "arity mismatch" else
+		let rec go env args doms = match args, doms with
+		| arg :: args, dom :: doms ->
+			let vdom = eval env dom in
+			let carg = check ctx arg vdom in
+			let varg = eval ctx.values carg in
+			let (cargs, vcod) = go (varg :: env) args doms in
+			(carg :: cargs, vcod)
+		| [], [] -> ([], eval env cod)
+		| _, _ -> failwith "impossible" in
+		let (cargs, vcod) = go env args doms in
+		(C.App (cf, cargs), vcod)
 	| _ -> failwith "expected function type in application"
 	end
-| SNat -> (CNat, VType)
-| SLit n -> (CLit n, VNat)
+| A.Access _ -> failwith "no impl: access"
+| A.Index _ -> failwith "no impl: index"
+| A.Deref _ -> failwith "no impl: deref"
+| A.Fn (ps, body) ->
+	let (xs, vdoms) = infer_patt_telescope ctx ps in
+	let arity = List.length xs in
+	let (cbody, vcod) = infer (bind_arb_telescope ctx xs vdoms) body in
+	let cdoms = quote_telescope ctx.len vdoms in
+	let ccod = quote (ctx.len + arity) vcod in
+	(C.Fn (arity, cbody), V.FnType (ctx.values, arity, cdoms, ccod))
+| A.FnType (anns, cod) ->
+	let arity = List.length anns in
+	let rec go ctx = function
+	| A.Annot (p, dom) :: anns ->
+		let cdom = check ctx dom (V.Intrin C.Type) in
+		let vdom = eval ctx.values cdom in
+		let x = check_patt ctx p vdom in
+		let (cdoms, ccod) = go (bind_arb ctx x vdom) anns in
+		(cdom :: cdoms, ccod)
+	| [] -> ([], check ctx cod (V.Intrin C.Type)) in
+	let (cdoms, ccod) = go ctx anns in
+	(C.FnType (arity, cdoms, ccod), V.Intrin C.Type)
+| A.Data _ -> failwith "no impl: data"
+| A.DataType _ -> failwith "no impl: data type"
+| A.Nat n -> (C.Nat n, V.Intrin C.NatType)
+| A.Ident x ->
+	let rec go i ys ts = match ys, ts with
+	| Some y :: ys, t :: ts -> if x = y then (C.Var i, t) else go (i + 1) ys ts
+	| None :: ys, _ :: ts -> go (i + 1) ys ts
+	| [], [] -> failwith ("unbound identifier: " ^ x)
+	| _, _ -> failwith "impossible" in
+	go 0 ctx.names ctx.types
 
-and infer_with_patt ctx a p = match p with
-| S.Annot (p, b) ->
-	let cb = check ctx b V.Type in
-	let vb = eval ctx.env cb in
-	let x = check_patt ctx p vb in
-	let ca = check ctx a vb in
-	(ca, vb, x)
-| S.Wild x -> let (ca, t) = infer ctx a in (ca, t, x)
+and check ctx a t = match a, t with
+(* TODO: Match, Fn, Data *)
+| a, t ->
+	let (ca, ta) = infer ctx a in
+	if conv ctx.len t ta then ca else failwith "type error"
+
+and infer_patt ctx = function
+| A.PWild -> failwith "can not infer type for wild pattern"
+| A.PBind _ -> failwith "can not infer type for bind pattern"
+| A.PAssign _ -> failwith "no impl: assign pattern"
+| A.PAnnot (A.Annot (p, t)) ->
+	let ct = check ctx t (V.Intrin C.Type) in
+	let vt = eval ctx.values ct in
+	let x = check_patt ctx p vt in
+	(x, vt)
+| A.PData _ -> failwith "no impl: data pattern"
+| A.PNat _ -> failwith "no impl: nat pattern"
+| A.PAnd _ -> failwith "no impl: and pattern"
+| A.POr _ -> failwith "no impl: or pattern"
+
+and infer_patt_telescope ctx = function
+| p :: ps ->
+	let (x, t) = infer_patt ctx p in
+	let (xs, ts) = infer_patt_telescope (bind_arb ctx x t) ps in
+	(x :: xs, t :: ts)
+| [] -> ([], [])
 
 and check_patt ctx p t = match p with
-| S.Annot (p, a) ->
-	let ca = check ctx a V.Type in
-	let va = eval ctx.env ca in
-	if conv (List.length ctx.env) t va then
+| A.PWild -> None
+| A.PBind x -> Some x
+| A.PAssign _ -> failwith "no impl: assign pattern"
+| A.PAnnot (A.Annot (p, u)) ->
+	let cu = check ctx u (V.Intrin C.Type) in
+	let vu = eval ctx.values cu in
+	if conv ctx.len vu t then
 		check_patt ctx p t
 	else
-		failwith "patt_check fail"
-| S.Wild x -> x
+		failwith "pattern does not unify with inferred type"
+| A.PData _ -> failwith "no impl: data pattern"
+| A.PNat _ -> failwith "no impl: nat pattern"
+| A.PAnd _ -> failwith "no impl: and pattern"
+| A.POr _ -> failwith "no impl: or pattern"
 
-and infer_patt ctx p = match p with
-| S.Annot (p, a) ->
-	let ca = check ctx a V.Type in
-	let va = eval ctx.env ca in
-	let x = check_patt ctx p va in
-	(x, va)
-| S.Wild _ -> failwith "can not infer type for wild pattern"
+(*
+and check_patt_telescope ctx ps ts = match ps, ts with
+| p :: ps, t :: ts ->
+	let x = check_patt ctx p t in
+	let xs = check_patt_telescope (bind_arb ctx x t) ps ts in
+	x :: xs
+| [], [] -> []
+| _, _ -> failwith "impossible"
+*)
diff --git a/elab2.ml b/elab2.ml
@@ -1,136 +0,0 @@
-open Common
-open Eval
-module A = Abstract
-module C = Core
-module V = Value
-
-type context = {
-	len: int;
-	names: ident list;
-	values: V.value list;
-	types: V.value list;
-}
-
-(* Add `x := v : t` to ctx. *)
-let bind_def ctx x v t = {
-	len = 1 + ctx.len;
-	names = x :: ctx.names;
-	values = v :: ctx.values;
-	types = t :: ctx.types;
-}
-
-(* Add `x : t` to ctx. *)
-let bind_arb ctx x t = bind_def ctx x (V.Arb ctx.len) t
-
-let rec bind_arb_telescope ctx xs ts = match xs, ts with
-| x :: xs, t :: ts -> bind_arb_telescope (bind_arb ctx x t) xs ts
-| [], [] -> ctx
-| _, _ -> failwith "impossible"
-
-let rec infer ctx = function
-| A.Match _ -> failwith "no impl: match"
-| A.Annot (a, t) ->
-	let ct = check ctx t (V.Intrin C.Type) in
-	let vt = eval ctx.values ct in
-	let ca = check ctx a vt in
-	(ca, vt)
-| A.App (f, args) ->
-	let (cf, tf) = infer ctx f in
-	begin match tf with
-	| V.FnType (env, arity, doms, cod) ->
-		if List.length args <> arity then failwith "arity mismatch" else
-		let rec go env args doms = match args, doms with
-		| arg :: args, dom :: doms ->
-			let vdom = eval env dom in
-			let carg = check ctx arg vdom in
-			let varg = eval ctx.values carg in
-			let (cargs, vcod) = go (varg :: env) args doms in
-			(carg :: cargs, vcod)
-		| [], [] -> ([], eval env cod)
-		| _, _ -> failwith "impossible" in
-		let (cargs, vcod) in go env args doms in
-		(C.App (cf, cargs), vcod)
-	| _ -> failwith "expected function type in application"
-	end
-| A.Access _ -> failwith "no impl: access"
-| A.Index _ -> failwith "no impl: index"
-| A.Deref _ -> failwith "no impl: deref"
-| A.Fn (ps, body) ->
-	let (xs, vdoms) = infer_patt_telescope ctx ps in
-	let arity = List.length xs in
-	let (cbody, vcod) = infer (bind_arb_telescope ctx xs vdoms) body in
-	let cdoms = quote_telescope ctx.len vdoms in
-	let ccod = quote (ctx.len + arity) vcod in
-	(C.Fn (arity, cbody), V.FnType (ctx.values, arity, cdoms, ccod))
-| A.FnType (anns, cod) ->
-	let arity = List.length anns in
-	let rec go ctx = function
-	| A.Annot (p, dom) :: anns ->
-		let cdom = check ctx dom (V.Intrin C.Type) in
-		let vdom = eval ctx.values cdom in
-		let x = check_patt ctx p vdom in
-		let (cdoms, ccod) = go (bind_arb ctx x vdom) anns in
-		(cdom :: cdoms, ccod)
-	| [] -> check ctx cod (V.Intrin C.Type) in
-	let (cdoms, ccod) = go ctx anns in
-	(C.FnType (arity, cdoms, ccod), V.Intrin C.Type)
-| A.Data _ -> failwith "no impl: data"
-| A.DataType _ -> failwith "no impl: data type"
-| A.Nat n -> (C.Nat n, V.Intrin C.NatType)
-| A.Ident x ->
-	let rec go ys vs ts = match ys, vs, ts with
-	| y :: ys, v :: vs, t :: ts -> if x = y then (v, t) else go ys vs ts
-	| [], [], [] -> failwith ("unbound identifier: " ^ x)
-	| _, _, _ -> failwith "impossible" in
-	go ctx.names ctx.values ctx.types
-
-and check ctx a t = match a, t with
-(* TODO: Match, Fn, Data *)
-| a, t ->
-	let (ca, ta) = infer ctx a in
-	if conv ctx.len t ta then ca else failwith "type error"
-
-and infer_patt ctx = function
-| A.PWild -> failwith "can not infer type for wild pattern"
-| A.PBind _ -> failwith "can not infer type for bind pattern"
-| A.PAssign _ -> failwith "no impl: assign pattern"
-| A.PAnnot (A.Annot (p, t)) ->
-	let ct = check ctx t (V.Intrin C.Type) in
-	let vt = eval ctx.values ct in
-	let x = check_patt ctx p vt in
-	(x, vt)
-| A.PData _ -> failwith "no impl: data pattern"
-| A.PNat _ -> failwith "no impl: nat pattern"
-| A.PAnd _ -> failwith "no impl: and pattern"
-| A.POr _ -> failwith "no impl: or pattern"
-
-and infer_patt_telescope ctx = function
-| p :: ps ->
-	let (x, t) = infer_patt ctx p in
-	let (xs, ts) = infer_patt_telescope (bind_arb ctx x t) ps in
-	(x :: xs, t :: ts)
-| [] -> ([], [])
-
-and check_patt ctx p t = match p with
-| A.PWild -> None
-| A.PBind x -> Some x
-| A.PAssign _ -> failwith "no impl: assign pattern"
-| A.PAnnot (A.Annot (p, u)) ->
-	let cu = check ctx u (V.Intrin C.Type) in
-	let vu = eval ctx.values cu in
-	if conv ctx.len vu t then
-		check_patt ctx p t
-	else
-		failwith "pattern does not unify with inferred type"
-| A.PData _ -> failwith "no impl: data pattern"
-| A.PNat _ -> failwith "no impl: nat pattern"
-| A.PAnd _ -> failwith "no impl: and pattern"
-| A.POr _ -> failwith "no impl: or pattern"
-
-and check_patt_telescope ctx ps ts = match ps, ts with
-| p :: ps, t :: ts ->
-	let x = check_patt ctx p t in
-	let xs = check_patt_telescope (bind_arb ctx x t) ps ts in
-	x :: xs
-| [], [] -> []
-| _, _ -> failwith "impossible"
diff --git a/eval.ml b/eval.ml
@@ -12,18 +12,12 @@ let rec eval env = function
 | C.Let _ -> failwith "no impl: let"
 | C.Case _ -> failwith "no impl: case"
 | C.App (f, args) ->
-	let vargs = List.map (eval env) args in
-	begin match eval env f with
+	begin match eval env f, List.map (eval env) args with
 	(* β-reduction *)
-	| V.Fn (cap, _, body) ->
-		eval (List.rev_append vargs cap) body
-	| V.Intrin C.NatOpAdd ->
-		begin match vargs with
-		| [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
-		| _ -> failwith "impossible"
-		end
+	| V.Fn (cap, _, body), vargs -> eval (List.rev_append vargs cap) body
+	| V.Intrin C.NatOpAdd, [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
 	(* neutral application *)
-	| vf -> V.App (vf, vargs)
+	| vf, vargs -> V.App (vf, vargs)
 	end
 | C.Fn (arity, body) -> V.Fn (env, arity, body)
 | C.FnType (arity, doms, cod) -> V.FnType (env, arity, doms, cod)
@@ -46,6 +40,7 @@ let rec quote l = function
 		let (cdoms, ccod) = go (l + 1) (V.Arb l :: env) doms in
 		(cdom :: cdoms, ccod)
 	| [] -> ([], quote l (eval env cod)) in
+	let (cdoms, ccod) = go l env doms in
 	C.FnType (arity, cdoms, ccod)
 | V.Nat n -> C.Nat n
 | V.Arb i -> C.Var (l - i - 1)
diff --git a/main.ml b/main.ml
@@ -1,3 +1,8 @@
-let buf = Lexing.from_string "let f = @(n) -> 2 * n : Nat; f 7"
-let e = Parser.expr0 Lexer.token buf
-let () = print_endline (Surf.string_of_expr 0 e)
-\ No newline at end of file
+let buf = Lexing.from_string "(fn x:Nat, y:Nat => x + y) 1 2"
+let concrete = Parser.start Lexer.token buf
+let abstract = Conctoabs.term concrete
+let ctx = Elab.default_ctx
+let (core, core_type) = Elab.infer ctx abstract
+let norm = Eval.quote ctx.len (Eval.eval ctx.values core)
+let () = print_endline (Core.to_string 0 core)
+let () = print_endline (Core.to_string 0 norm)
diff --git a/parser.mly b/parser.mly
@@ -16,8 +16,8 @@ open Concrete
 %token <Common.ident> IDENT
 %token <Z.t> NAT
 
-%start expr0
-%type <Concrete.expr> expr0
+%start start
+%type <Concrete.expr> start
 
 %nonassoc PREC_EXPR4
 %nonassoc PREC_TUPLE
@@ -34,6 +34,8 @@ open Concrete
  *     (Think of ":= func" as being one symbol).
  * We can make a similar distinction for types with "ty" vs "type". *)
 
+start: expr0 EOF { $1 }
+
 expr0: (* Sequencing *)
 	| expr1 COLON_EQ expr1 SEMICOLON expr0 { Let ($1, $3, $5) }
 	| expr1 SEMICOLON expr0 { Seq ($1, $3) }
@@ -42,7 +44,7 @@ expr1: (* Control flow *)
 	| expr2 MATCH LBRACE cases RBRACE { Match($1, $4) }
 	| IF expr1 THEN expr1 ELSE expr1 { If ($2, $4, $6) }
 	| IFF expr1 DO expr1 { Iff ($2, $4) }
-	| FN annot_list SINGLE_ARROW expr1 { Fn ($2, $4) }
+	| FN annot_list DOUBLE_ARROW expr1 { Fn ($2, $4) }
 	| expr2 { $1 }
 expr2: (* Type annotations (right-associative); lowest prec for patterns *)
 	| expr3 COLON expr2 { Annot($1, $3) }
diff --git a/surf.ml b/surf.ml
@@ -1,40 +0,0 @@
-open Common
-
-type expr =
-| Let of patt * expr * expr
-| If of expr * expr * expr
-| Fn of patt * expr
-| Pi of ident * expr * expr
-| Hint of expr * expr
-| Plus of expr * expr
-| Asterisk of expr * expr
-| Apposition of expr * expr
-| Var of ident
-| Int of Z.t
-and patt =
-| Annot of patt * expr
-| Wild of ident
-
-let rec string_of_expr m e =
-	let sp = string_of_patt in
-	let se = string_of_expr in
-	let (c, s) = match e with
-	| Let (p, a, b) -> (0, "let " ^ sp 0 p ^ " = " ^ se 1 a ^ "; " ^ se 0 b)
-	| If (c, t, f) -> (0, "if " ^ se 1 c ^ " then " ^ se 1 t ^ " else " ^ se 1 f)
-	| Fn (p, e) -> (1, "@(" ^ sp 0 p ^ ") -> " ^ se 1 e)
-	| Pi (p, e) -> (1, "#(" ^ sp 0 p ^ ") -> " ^ se 1 e)
-	| Hint (a, b) -> (1, se 2 a ^ " : " ^ se 1 b)
-	| Plus (a, b) -> (2, se 2 a ^ " + " ^ se 3 b)
-	| Asterisk (a, b) -> (3, se 3 a ^ " * " ^ se 4 b)
-	| Apposition (a, b) -> (4, se 4 a ^ " " ^ se 5 b)
-	| Var x -> (5, x)
-	| Int z -> (5, Z.to_string z) in
-	if c < m then "(" ^ s ^ ")" else s
-
-and string_of_patt m p =
-	let sp = string_of_patt in
-	let se = string_of_expr in
-	let (c, s) = match p with
-	| Annot (p, e) -> (0, sp 1 p ^ " : " ^ se 1 e)
-	| Wild x -> (1, x) in
-	if c < m then "(" ^ s ^ ")" else s