diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Ast.ml | 12 | ||||
| -rw-r--r-- | lib/Conversion.ml | 75 | ||||
| -rw-r--r-- | lib/Data.ml | 51 | ||||
| -rw-r--r-- | lib/Domain.ml | 34 | ||||
| -rw-r--r-- | lib/Elab.ml | 163 | ||||
| -rw-r--r-- | lib/Eval.ml | 18 | ||||
| -rw-r--r-- | lib/Eval.mli | 4 | ||||
| -rw-r--r-- | lib/Lexer.mll | 1 | ||||
| -rw-r--r-- | lib/Parser.mly | 17 | ||||
| -rw-r--r-- | lib/ParserEff.ml | 1 | ||||
| -rw-r--r-- | lib/Quote.ml | 14 | ||||
| -rw-r--r-- | lib/Quote.mli | 4 | ||||
| -rw-r--r-- | lib/Reporter.ml | 28 | ||||
| -rw-r--r-- | lib/Syntax.ml | 114 | ||||
| -rw-r--r-- | lib/dune | 2 |
15 files changed, 473 insertions, 65 deletions
@@ -1,11 +1,11 @@ type raw_ident = Yuujinchou.Trie.path type ident = raw_ident Asai.Range.located -type raw_arg = { name : ident; ty : expr } -and arg = raw_arg Asai.Range.located +type arg = ident * expr and raw_expr = | Var of raw_ident + | Check of expr * expr | Pi of arg * expr | Lam of ident * expr | App of expr * expr @@ -27,18 +27,18 @@ and raw_expr = and expr = raw_expr Asai.Range.located +(* TODO this is the same as Syntax.pretty.pp_name *) let dump_raw_ident fmt (id : raw_ident) = Format.pp_print_list ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.') Format.pp_print_string fmt id let dump_ident fmt ({ value; _ } : ident) = dump_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 - -and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value +let rec dump_arg fmt ((name, tp) : arg) = + Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr tp and dump_raw_expr fmt = function | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id + | Check (tm, tp) -> Format.fprintf fmt "@[%a@] : @[%a@]" dump_expr tm dump_expr tp | Bool -> Format.pp_print_string fmt "Bool" | True -> Format.pp_print_string fmt "True" | False -> Format.pp_print_string fmt "False" diff --git a/lib/Conversion.ml b/lib/Conversion.ml new file mode 100644 index 0000000..b70a070 --- /dev/null +++ b/lib/Conversion.ml @@ -0,0 +1,75 @@ +open Bwd +open Bwd.Infix + +module D = Domain + +exception Unequal + +module Internal = +struct + (** Context size *) + type env = int + + module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) + + let bind f = + let arg = D.var (Eff.read()) in + Eff.scope (fun size -> size + 1) (fun () -> f arg) + + let rec equate v1 v2 = match v1, v2 with + | D.Neutral ne, v | v, D.Neutral ne -> equate_ne ne v + | D.Pi (base1, fam1), D.Pi (base2, fam2) -> + equate base1 base2; + equate_clo fam1 fam2 + | D.Lam clo1, D.Lam clo2 -> equate_clo clo1 clo2 + | D.Sg (base1, fam1), D.Sg (base2, fam2) -> + equate base1 base2; + equate_clo fam1 fam2 + | D.Pair (fst1, snd1), D.Pair (fst2, snd2) -> + equate fst1 fst2; + equate snd1 snd2 + | Type, Type -> () + | Bool, Bool -> () + | True, True -> () + | False, False -> () + | _ -> raise Unequal + + and equate_clo clo1 clo2 = bind @@ fun arg -> + equate (Eval.inst_clo clo1 arg) (Eval.inst_clo clo2 arg) + + and equate_ne_head (D.Var lvl1) (D.Var lvl2) = + if lvl1 = lvl2 then () else raise Unequal + + and equate_frm frm1 frm2 = match frm1, frm2 with + | D.App arg1, D.App arg2 -> equate arg1 arg2 + | D.Fst, D.Fst -> () + | D.Snd, D.Snd -> () + | D.BoolElim { cmot = mot1; vtrue = t1; vfalse = f1 }, + D.BoolElim { cmot = mot2; vtrue = t2; vfalse = f2 } -> + equate_clo mot1 mot2; + equate t1 t2; + equate f1 f2; + | _ -> raise Unequal + + and equate_spine sp1 sp2 = match sp1, sp2 with + | Emp, Emp -> () + | Snoc (sp1, frm1), Snoc (sp2, frm2) -> + equate_frm frm1 frm2; + equate_spine sp1 sp2 + | _ -> raise Unequal + + and equate_ne (hd, sp) v = match v with + | D.Neutral (hd2, sp2) -> + equate_ne_head hd hd2; + equate_spine sp sp2 + (* eta expansion *) + | D.Lam clo -> bind @@ fun arg -> + equate_ne (hd, sp <: D.App arg) (Eval.inst_clo clo arg) + | D.Pair (fst, snd) -> + equate_ne (hd, sp <: D.Fst) fst; + equate_ne (hd, sp <: D.Snd) snd + | _ -> raise Unequal +end + +let equate ~size v1 v2 = Internal.Eff.run ~env:size @@ fun () -> + Internal.equate v1 v2 diff --git a/lib/Data.ml b/lib/Data.ml new file mode 100644 index 0000000..19ca67d --- /dev/null +++ b/lib/Data.ml @@ -0,0 +1,51 @@ +open Bwd + +(** Syntactic terms *) + +type syn = + | Var of int + | Pi of syn * (* BINDS *) syn + | Lam of (* BINDS *) syn + | App of syn * syn + | Sg of syn * (* BINDS *) syn + | Pair of syn * syn + | Fst of syn + | Snd of syn + | Type + | Bool + | True + | False + | BoolElim of { + motive : (* BINDS *) syn; + true_case : syn; + false_case : syn; + scrut : syn; + } + +(** Semantic domain *) + +type value = + | Neutral of ne + | Pi of value * clo + | Lam of clo + | Sg of value * clo + | Pair of value * value + | Type + | Bool + | True + | False + +and ne = ne_head * frm bwd +and ne_head = Var of int (* De Bruijn levels *) +and frm = + | App of value + | Fst + | Snd + | BoolElim of { + cmot: clo; + vtrue: value; + vfalse: value; + } + +and env = value bwd +and clo = Clo of { body : syn; env : env } diff --git a/lib/Domain.ml b/lib/Domain.ml index 88560c2..67ac4ae 100644 --- a/lib/Domain.ml +++ b/lib/Domain.ml @@ -1,31 +1,29 @@ open Bwd -type value = +type t = Data.value = | Neutral of ne - | Pi of value * clos - | Lam of clos - | Sg of value * clos - | Pair of value * value + | Pi of t * clo + | Lam of clo + | Sg of t * clo + | Pair of t * t | Type | Bool | True | False -and ne = ne_head * frame bwd -and ne_head = Var of int (* De Bruijn levels *) -and frame = - | BoolElim of { - cmot: clos; - vtrue: value; - vfalse: value; - } - | App of value +and ne = Data.ne +and ne_head = Data.ne_head = Var of int (* De Bruijn levels *) +and frm = Data.frm = + | App of t | Fst | Snd + | BoolElim of { + cmot: clo; + vtrue: t; + vfalse: t; + } -and env = value bwd -and clos = Clos of { body : Syntax.tm; env : env } - -type cell = { tm : value; tp : value } +and env = Data.env +and clo = Data.clo = Clo of { body : Data.syn; env : env } let var i = Neutral (Var i, Bwd.Emp) diff --git a/lib/Elab.ml b/lib/Elab.ml new file mode 100644 index 0000000..5bda770 --- /dev/null +++ b/lib/Elab.ml @@ -0,0 +1,163 @@ +open Bwd +open Bwd.Infix + +module A = Ast +module S = Syntax +module D = Domain +module R = Reporter + +(* TODO: REALLY improve error messages *) + +(* `None` means that an underscore was used in the binder *) +(* TODO: actually implement this *) +type local_name = Yuujinchou.Trie.path option + +(* invariant: `tps`, `tms` and `names` all have length `size` *) +type env = { + tps : D.env; + tms : D.env; + names : local_name bwd; + size : int; +} + +module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) + +(** General helpers *) + +let lookup_name name : D.t * S.t = + let env = Eff.read() in + match Bwd.find_index ((=) (Some name)) env.names with + | Some ix -> + let tp = Bwd.nth env.tps ix in + let tm = Quote.quote ~size:env.size (Bwd.nth env.tms ix) in + (tp, tm) + | None -> R.fatalf R.Message.UnboundVariable + "unbound variable @[%a@]" S.Pretty.pp_name name + +let define ~(name : A.raw_ident) ~(tp : D.t) ~(tm : D.t) f = + let update env = { + tps = env.tps <: tp; + tms = env.tms <: tm; + names = env.names <: Some name; + size = env.size + 1; + } in + Eff.scope update f + +let bind ~(name : A.raw_ident) ~(tp : D.t) f = + let arg = D.var (Eff.read()).size in + define ~name ~tp ~tm:arg (fun () -> f arg) + +(** NbE helpers *) + +let eval tm = Eval.eval ~env:(Eff.read()).tms tm + +(** Evaluate under the current environment augmented by `arg` *) +(* TODO: this is kind of inelegant, can we do better? *) +let eval_at arg = Eval.eval ~env:((Eff.read()).tms <: arg) + +let quote v = Quote.quote ~size:(Eff.read()).size v + +(** Main algorithm *) + +let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = + R.tracef ?loc:tm.loc "when checking against the type @[%a@]" Syntax.Pretty.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 (base, fam) + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end + | A.Lam (name, body) -> begin match tp with + | D.Pi (base, fam) -> + let body = bind ~name:name.value ~tp:base @@ fun arg -> + let fib = Eval.inst_clo fam arg in + check ~tm:body ~tp:fib in + S.Lam body + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Pi type" Syntax.Pretty.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 (base, fam) + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) end + | A.Pair (fst, snd) -> begin match tp with + | D.Sg (base, fam) -> + let fst = check ~tm:fst ~tp:base in + let fib = Eval.inst_clo fam (eval fst) in + let snd = check ~tm:snd ~tp:fib in + S.Pair (fst, snd) + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" Syntax.Pretty.pp (quote tp) + end + | A.Type -> begin match tp with (* TODO type-in-type *) + | D.Type -> S.Type + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) + end + | A.Bool -> begin match tp with + | D.Type -> S.Bool + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" Syntax.Pretty.pp (quote tp) + end + | A.True -> begin match tp with + | D.Bool -> S.True + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.pp (quote tp) + end + | A.False -> begin match tp with + | D.Bool -> S.False + | _ -> R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" Syntax.Pretty.pp (quote tp) + end + | _ -> let (inferred_tp, tm) = infer tm in begin + try Conversion.equate ~size:((Eff.read()).size) inferred_tp tp with + | Conversion.Unequal -> + R.fatalf R.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" Syntax.Pretty.pp (quote tp) Syntax.Pretty.pp (quote inferred_tp) + end; + tm + +and infer (tm : A.expr) : D.t * S.t = + R.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> + match tm.value with + | A.Var name -> lookup_name name + | A.Check (tm, tp) -> + let tp = eval @@ check ~tp:D.Type ~tm:tp in + let tm = check ~tp ~tm in + (tp, tm) + | A.App (fn, arg) -> begin match infer fn with + | (D.Pi (base, fam), fn) -> + let arg = check ~tm:arg ~tp:base in + let tp = Eval.inst_clo fam (eval arg) in + let tm = S.App (fn, arg) in + (tp, tm) + | _ -> R.fatalf R.Message.IllTyped "cannot apply this term because it is not a function" + end + | A.Fst p -> begin match infer p with + | (D.Sg (base, _), p) -> (base, S.Fst p) + | _ -> R.fatalf R.Message.IllTyped "cannot apply first projection to this term because it is not of sigma type" + end + | A.Snd p -> begin match infer p with + | (D.Sg (_, fam), p) -> + let tp = Eval.inst_clo fam (eval (S.Fst p)) in + let tm = S.Snd p in + (tp, tm) + | _ -> R.fatalf R.Message.IllTyped "cannot apply second projection to this term because it is of sigma type" + end + | A.BoolElim { motive_var; motive_body; true_case; false_case; scrut } -> + let scrut = check ~tm:scrut ~tp:D.Bool in + let motive = bind ~name:motive_var.value ~tp:D.Bool @@ fun _ -> + check ~tm:motive_body ~tp:D.Type in + let motive_true = eval_at D.True motive in + let motive_false = eval_at D.False motive in + let motive_scrut = eval_at (eval scrut) motive in + let true_case = check ~tm:true_case ~tp:motive_true in + let false_case = check ~tm:false_case ~tp:motive_false in + let tm = S.BoolElim { motive; true_case; false_case; scrut } in + (motive_scrut, tm) + | _ -> R.fatalf R.Message.CannotInferType "cannot infer type" + +let empty_env : env = { + tps = Emp; + tms = Emp; + names = Emp; + size = 0; +} + +let infer_toplevel (tm : A.expr) = Eff.run ~env:empty_env @@ fun () -> infer tm
\ No newline at end of file diff --git a/lib/Eval.ml b/lib/Eval.ml index 8f6722b..033ee8c 100644 --- a/lib/Eval.ml +++ b/lib/Eval.ml @@ -8,14 +8,14 @@ module Internal = struct module Eff = Algaeff.Reader.Make (struct type nonrec t = D.env end) - let make_clos body = D.Clos { body; env = Eff.read() } + let make_clo body = D.Clo { body; env = Eff.read() } - let rec inst_clos (D.Clos { body; env }) arg = + let rec inst_clo (D.Clo { body; env }) arg = let env = env <: arg in Eff.run ~env @@ fun () -> eval body and app v w = match v with - | D.Lam clos -> inst_clos clos w + | D.Lam clo -> inst_clo clo w | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w) | _ -> invalid_arg "Eval.app" @@ -37,10 +37,10 @@ struct and eval = function | S.Var i -> Bwd.nth (Eff.read()) i - | S.Pi (base, fam) -> D.Pi (eval base, make_clos fam) - | S.Lam body -> D.Lam (make_clos body) + | S.Pi (base, fam) -> D.Pi (eval base, make_clo fam) + | S.Lam body -> D.Lam (make_clo body) | S.App (a, b) -> app (eval a) (eval b) - | S.Sg (base, fam) -> D.Sg (eval base, make_clos fam) + | S.Sg (base, fam) -> D.Sg (eval base, make_clo fam) | S.Pair (a, b) -> D.Pair (eval a, eval b) | S.Fst a -> fst (eval a) | S.Snd a -> snd (eval a) @@ -49,8 +49,8 @@ struct | S.True -> D.True | S.False -> D.False | S.BoolElim { motive; true_case; false_case; scrut } -> - bool_elim (make_clos motive) (eval true_case) (eval false_case) (eval scrut) + bool_elim (make_clo motive) (eval true_case) (eval false_case) (eval scrut) end -let eval ~env tm = Internal.Eff.run ~env (fun () -> Internal.eval tm) -let inst_clos = Internal.inst_clos +let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm +let inst_clo = Internal.inst_clo diff --git a/lib/Eval.mli b/lib/Eval.mli index 24fa87d..63c49cf 100644 --- a/lib/Eval.mli +++ b/lib/Eval.mli @@ -1,2 +1,2 @@ -val eval : env:Domain.env -> Syntax.tm -> Domain.value -val inst_clos : Domain.clos -> Domain.value -> Domain.value +val eval : env:Domain.env -> Syntax.t -> Domain.t +val inst_clo : Domain.clo -> Domain.t -> Domain.t diff --git a/lib/Lexer.mll b/lib/Lexer.mll index 3f178f5..c33acae 100644 --- a/lib/Lexer.mll +++ b/lib/Lexer.mll @@ -16,6 +16,7 @@ rule lex = | "->" { ARROW } | "*" { ASTERISK } | "\\" { BACKSLASH } + | "::" { DOUBLE_COLON } | ":" { COLON } | "," { COMMA } | "." { DOT } diff --git a/lib/Parser.mly b/lib/Parser.mly index 0390b3c..fc82d1a 100644 --- a/lib/Parser.mly +++ b/lib/Parser.mly @@ -5,13 +5,15 @@ open Ast %token <string> IDENT %token LPR RPR %token LBR RBR -%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW +%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW %token BOOL TRUE FALSE BOOL_ELIM AT %token FST SND %token TYPE %token EOF -%right ARROW ASTERISK +%nonassoc DOUBLE_COLON +%right ARROW +%right ASTERISK %left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM %start <Ast.expr> parse @@ -19,24 +21,23 @@ open Ast %% %inline -locate(X): e = X { Asai.Range.locate_lex $loc e } +locate(X): e = X { Asai.Range.locate_lex ~source:(ParserEff.Eff.read()) $loc e } raw_ident: id = separated_nonempty_list(DOT, IDENT) { id } %inline ident: id = locate(raw_ident) { id } -raw_arg: LPR; name = ident; COLON; ty = expr; RPR - { { name; ty } } - -%inline -arg: a = locate(raw_arg) { a } +arg: LPR; name = ident; COLON; tp = expr; RPR + { (name, tp) } raw_expr: | name = raw_ident { Var name } | LPR; e = raw_expr; RPR { e } + | tm = expr; DOUBLE_COLON; tp = expr + { Check (tm, tp) } | a = arg; ARROW; b = expr { Pi (a, b) } diff --git a/lib/ParserEff.ml b/lib/ParserEff.ml new file mode 100644 index 0000000..84c0de8 --- /dev/null +++ b/lib/ParserEff.ml @@ -0,0 +1 @@ +module Eff = Algaeff.Reader.Make (struct type nonrec t = Asai.Range.source end) diff --git a/lib/Quote.ml b/lib/Quote.ml index 5989870..611843a 100644 --- a/lib/Quote.ml +++ b/lib/Quote.ml @@ -15,28 +15,28 @@ struct let rec quote = function | D.Neutral ne -> quote_ne ne - | D.Pi (base, fam) -> S.Pi (quote base, quote_clos fam) - | D.Lam clos -> S.Lam (quote_clos clos) - | D.Sg (base, fam) -> S.Sg (quote base, quote_clos fam) + | D.Pi (base, fam) -> S.Pi (quote base, quote_clo fam) + | D.Lam clo -> S.Lam (quote_clo clo) + | D.Sg (base, fam) -> S.Sg (quote base, quote_clo fam) | D.Pair (v, w) -> S.Pair (quote v, quote w) | D.Type -> S.Type | D.Bool -> S.Bool | D.True -> S.True | D.False -> S.False - and quote_clos clos = bind @@ fun arg -> quote (Eval.inst_clos clos arg) + and quote_clo clo = bind @@ fun arg -> quote (Eval.inst_clo clo arg) - and quote_ne (hd, frms) = Bwd.fold_left quote_frame (quote_ne_head hd) frms + and quote_ne (hd, frms) = Bwd.fold_left quote_frm (quote_ne_head hd) frms and quote_ne_head (D.Var i) = S.Var (Eff.read() - i - 1) (* converting from levels to indices *) - and quote_frame hd = function + and quote_frm hd = function | D.App v -> S.App (hd, quote v) | D.Fst -> S.Fst hd | D.Snd -> S.Snd hd | D.BoolElim { cmot; vtrue; vfalse } -> S.BoolElim { - motive = quote_clos cmot; + motive = quote_clo cmot; true_case = quote vtrue; false_case = quote vfalse; scrut = hd; diff --git a/lib/Quote.mli b/lib/Quote.mli index c55aa8b..193b0b0 100644 --- a/lib/Quote.mli +++ b/lib/Quote.mli @@ -1,2 +1,2 @@ -val quote : size:int -> Domain.value -> Syntax.tm -val quote_ne : size:int -> Domain.ne -> Syntax.tm +val quote : size:int -> Domain.t -> Syntax.t +val quote_ne : size:int -> Domain.ne -> Syntax.t diff --git a/lib/Reporter.ml b/lib/Reporter.ml new file mode 100644 index 0000000..c86a04a --- /dev/null +++ b/lib/Reporter.ml @@ -0,0 +1,28 @@ +module Message = +struct + type t = + | SyntaxError + | IllTyped + | UnboundVariable + | CannotInferType + + let default_severity : t -> Asai.Diagnostic.severity = + function + | SyntaxError -> Error + | IllTyped -> Error + | UnboundVariable -> Error + | CannotInferType -> Error + + let short_code : t -> string = + function + | SyntaxError -> "E0001" + | IllTyped -> "E0002" + | UnboundVariable -> "E0003" + | CannotInferType -> "E0004" +end + +include Asai.Reporter.Make(Message) + +let invalid_local_name (name : Ast.raw_ident) = fatalf SyntaxError "invalid local variable name `%a`" Ast.dump_raw_ident name + +let expected_universe fmt x = fatalf IllTyped "expected a universe but got %a" fmt x
\ No newline at end of file diff --git a/lib/Syntax.ml b/lib/Syntax.ml index 6cd988a..c4cf80d 100644 --- a/lib/Syntax.ml +++ b/lib/Syntax.ml @@ -1,19 +1,109 @@ -type tm = +open Bwd + +type t = Data.syn = | Var of int - | Pi of tm * (* BINDS *) tm - | Lam of (* BINDS *) tm - | App of tm * tm - | Sg of tm * (* BINDS *) tm - | Pair of tm * tm - | Fst of tm - | Snd of tm + | Pi of t * (* BINDS *) t + | Lam of (* BINDS *) t + | App of t * t + | Sg of t * (* BINDS *) t + | Pair of t * t + | Fst of t + | Snd of t | Type | Bool | True | False | BoolElim of { - motive : (* BINDS *) tm; - true_case : tm; - false_case : tm; - scrut : tm; + motive : (* BINDS *) t; + true_case : t; + false_case : t; + scrut : t; } + +module Pretty = +struct + type local_names = Yuujinchou.Trie.path option bwd + type tm_with_names = t * local_names + + let pp_name fmt (id : Yuujinchou.Trie.path) = Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.') + Format.pp_print_string fmt id + + module Internal = + struct + type env = { + prec : int; + } + + module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) + + let with_prec (prec : int) (inner : 'a Fmt.t) (fmt : Format.formatter) (v : 'a) = + Eff.scope (fun _ -> { prec; }) (fun () -> inner fmt v) + + let delimited inner = with_prec 0 inner + + let parenthesize (prec : int) : 'a Fmt.t -> 'a Fmt.t = + if (Eff.read()).prec > prec then + Fmt.parens + else + Fun.id + + let lassoc (prec : int) + ?(pre = "") + (pp_left : 'l Fmt.t) + ?(middle = " ") + (pp_right : 'r Fmt.t) + ?(post = "") : ('l * 'r) Fmt.t = + parenthesize prec @@ fun fmt v -> + Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" + pre + (with_prec prec pp_left) (fst v) + middle + (with_prec (prec + 1) pp_right) (snd v) + post + + let rassoc (prec : int) + ?(pre = "") + (pp_left : 'l Fmt.t) + ?(middle = " ") + (pp_right : 'r Fmt.t) + ?(post = "") : ('l * 'r) Fmt.t = + parenthesize prec @@ fun fmt v -> + Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" + pre + (with_prec (prec + 1) pp_left) (fst v) + middle + (with_prec prec pp_right) (snd v) + post + + let pp_var ix fmt = Fmt.pf fmt "%@%d" ix + + let rec pp_pair fmt = (delimited @@ fun fmt (a, b) -> Fmt.pf fmt "@[(@[%a@], @[%a@])@]" pp a pp b) fmt + + and pp_bool_elim fmt = + (delimited @@ fun fmt (motive, true_case, false_case, scrut) -> Fmt.pf fmt + "@[bool-elim @[%a@] at _ -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]" + pp scrut pp motive pp true_case pp false_case + ) fmt + + (* TODO: improve indentation *) + and pp fmt = function + | Var ix -> pp_var ix fmt + | Pi (base, fam) -> rassoc 1 ~pre:"(_ : " pp ~middle:") -> " pp fmt (base, fam) + | Lam body -> Fmt.pf fmt "@[\\_ -> @[%a@]@]" pp body + | Sg (base, fam) -> rassoc 2 ~pre:"(_ : " pp ~middle:") * " pp fmt (base, fam) + | App (a, b) -> lassoc 3 pp pp fmt (a, b) + | Pair (a, b) -> pp_pair fmt (a, b) + | Fst a -> lassoc 3 Fmt.string pp fmt ("fst", a) + | Snd a -> lassoc 3 Fmt.string pp fmt ("snd", a) + | Type -> Fmt.string fmt "type" + | Bool -> Fmt.string fmt "bool" + | True -> Fmt.string fmt "true" + | False -> Fmt.string fmt "false" + | BoolElim { motive; true_case; false_case; scrut } -> pp_bool_elim fmt (motive, true_case, false_case, scrut) + end + + let pp fmt tm = + let env : Internal.env = { prec = 0; } in + Internal.Eff.run ~env (fun () -> Internal.pp fmt tm) +end @@ -6,5 +6,5 @@ (library (name toytt) - (libraries asai yuujinchou) + (libraries asai fmt yuujinchou) (preprocess (pps ppx_deriving.std))) |