diff options
| -rw-r--r-- | README.md | 17 | ||||
| -rw-r--r-- | bin/main.ml | 2 | ||||
| -rw-r--r-- | lib/Ast.ml | 30 | ||||
| -rw-r--r-- | lib/Conversion.ml | 12 | ||||
| -rw-r--r-- | lib/Data.ml | 20 | ||||
| -rw-r--r-- | lib/Domain.ml | 13 | ||||
| -rw-r--r-- | lib/Elab.ml | 94 | ||||
| -rw-r--r-- | lib/Eval.ml | 20 | ||||
| -rw-r--r-- | lib/Ident.ml | 9 | ||||
| -rw-r--r-- | lib/Lexer.mll | 1 | ||||
| -rw-r--r-- | lib/Parser.mly | 14 | ||||
| -rw-r--r-- | lib/Quote.ml | 15 | ||||
| -rw-r--r-- | lib/Reporter.ml | 18 | ||||
| -rw-r--r-- | lib/Syntax.ml | 82 |
14 files changed, 188 insertions, 159 deletions
@@ -26,15 +26,16 @@ not-function applied to `false` (which evaluates to `true`). ## todo list (in descending order of importance and/or realizability) -- figure out how to recover variable names in pretty-printing so we don't +- [x] figure out how to recover variable names in pretty-printing so we don't have to print de bruijn indices all the time -- implement top-level definitions -- implement less aggrevating syntax for non-dependent function & pair types -- add a type of natural numbers -- replace type-in-type with a proper (cumulative?) hierarchy of universes +- [ ] improve error messages and build a better repl +- [ ] implement top-level definitions +- [ ] implement less aggrevating syntax for non-dependent function & pair types +- [ ] add a type of natural numbers +- [ ] replace type-in-type with a proper (cumulative?) hierarchy of universes -> maybe use the mugen library or figure out typical ambiguity? -- implement inductive types/families -- implement axioms (probably easy) -- do HoTT stuff (maybe implement a form of cubical type theory? or stick with +- [ ] implement inductive types/families +- [ ] implement axioms (probably easy) +- [ ] do HoTT stuff (maybe implement a form of cubical type theory? or stick with book HoTT, which is probably much easier) - ... diff --git a/bin/main.ml b/bin/main.ml index ec5c4d2..afae47c 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -18,7 +18,7 @@ let rec repl () = let ast = parse input in let (tp, tm) = Elab.infer_toplevel ast in let value = Eval.eval ~env:Emp tm in - Format.printf "%a : %a\n%!" Syntax.Pretty.pp (Quote.quote ~size:0 value) Syntax.Pretty.pp (Quote.quote ~size:0 tp); + Format.printf "%a : %a\n%!" Syntax.Pretty.pp (Quote.quote ~size:0 value, Emp) Syntax.Pretty.pp (Quote.quote ~size:0 tp, Emp); repl () let () = @@ -1,13 +1,13 @@ -type raw_ident = Yuujinchou.Trie.path -type ident = raw_ident Asai.Range.located +type ident = Ident.t Asai.Range.located +type local_name = Ident.local Asai.Range.located -type arg = ident * expr +type arg = local_name * expr and raw_expr = - | Var of raw_ident + | Var of Ident.t | Check of expr * expr | Pi of arg * expr - | Lam of ident * expr + | Lam of local_name * expr | App of expr * expr | Sg of arg * expr | Pair of expr * expr @@ -18,7 +18,7 @@ and raw_expr = | True | False | BoolElim of { - motive_var : ident; + motive_var : local_name; motive_body : expr; true_case : expr; false_case : expr; @@ -27,17 +27,17 @@ 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 dump_ident fmt ({ value; _ } : ident) = Ident.pp fmt value + +let dump_local_name fmt ({ value; _ } : local_name) = match value with + | Some name -> Format.pp_print_string fmt name + | None -> Format.pp_print_char fmt '_' let rec dump_arg fmt ((name, tp) : arg) = - Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr tp + Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_local_name name dump_expr tp and dump_raw_expr fmt = function - | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id + | Var id -> Format.fprintf fmt "Var @[%a@]" Ident.pp 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" @@ -45,7 +45,7 @@ and dump_raw_expr fmt = function | 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_local_name motive_var dump_expr motive_body dump_expr true_case dump_expr false_case @@ -53,7 +53,7 @@ and dump_raw_expr fmt = function | Pi (dom, cod) -> Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod | Lam (var, body) -> - Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr 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) -> diff --git a/lib/Conversion.ml b/lib/Conversion.ml index b70a070..00bc942 100644 --- a/lib/Conversion.ml +++ b/lib/Conversion.ml @@ -18,11 +18,11 @@ struct 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) -> + | 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) -> + | 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) -> @@ -44,8 +44,8 @@ struct | 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 } -> + | D.BoolElim { motive = mot1; true_case = t1; false_case = f1; _ }, + D.BoolElim { motive = mot2; true_case = t2; false_case = f2; _ } -> equate_clo mot1 mot2; equate t1 t2; equate f1 f2; @@ -63,7 +63,7 @@ struct equate_ne_head hd hd2; equate_spine sp sp2 (* eta expansion *) - | D.Lam clo -> bind @@ fun arg -> + | 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; diff --git a/lib/Data.ml b/lib/Data.ml index 19ca67d..d2f94d3 100644 --- a/lib/Data.ml +++ b/lib/Data.ml @@ -4,10 +4,10 @@ open Bwd type syn = | Var of int - | Pi of syn * (* BINDS *) syn - | Lam of (* BINDS *) syn + | Pi of Ident.local * syn * (* BINDS *) syn + | Lam of Ident.local * (* BINDS *) syn | App of syn * syn - | Sg of syn * (* BINDS *) syn + | Sg of Ident.local * syn * (* BINDS *) syn | Pair of syn * syn | Fst of syn | Snd of syn @@ -16,6 +16,7 @@ type syn = | True | False | BoolElim of { + motive_var : Ident.local; motive : (* BINDS *) syn; true_case : syn; false_case : syn; @@ -26,9 +27,9 @@ type syn = type value = | Neutral of ne - | Pi of value * clo - | Lam of clo - | Sg of value * clo + | Pi of Ident.local * value * clo + | Lam of Ident.local * clo + | Sg of Ident.local * value * clo | Pair of value * value | Type | Bool @@ -42,9 +43,10 @@ and frm = | Fst | Snd | BoolElim of { - cmot: clo; - vtrue: value; - vfalse: value; + motive_var : Ident.local; + motive: clo; + true_case: value; + false_case: value; } and env = value bwd diff --git a/lib/Domain.ml b/lib/Domain.ml index 67ac4ae..6f5e11c 100644 --- a/lib/Domain.ml +++ b/lib/Domain.ml @@ -2,9 +2,9 @@ open Bwd type t = Data.value = | Neutral of ne - | Pi of t * clo - | Lam of clo - | Sg of t * clo + | Pi of Ident.local * t * clo + | Lam of Ident.local * clo + | Sg of Ident.local * t * clo | Pair of t * t | Type | Bool @@ -18,9 +18,10 @@ and frm = Data.frm = | Fst | Snd | BoolElim of { - cmot: clo; - vtrue: t; - vfalse: t; + motive_var : Ident.local; + motive : clo; + true_case : t; + false_case: t; } and env = Data.env diff --git a/lib/Elab.ml b/lib/Elab.ml index 5bda770..d911b9f 100644 --- a/lib/Elab.ml +++ b/lib/Elab.ml @@ -4,19 +4,14 @@ 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; + names : Ident.local bwd; size : int; } @@ -24,28 +19,26 @@ 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 lookup (id : Ident.t) : D.t * S.t = match Ident.to_local id with + | Some name -> begin + let env = Eff.read() in + match Bwd.find_index ((=) name) env.names with + | Some ix -> + let tp = Bwd.nth env.tps ix in + (tp, S.Var ix) + | None -> Reporter.unbound_variable id + end + | None -> Reporter.unbound_variable id -let define ~(name : A.raw_ident) ~(tp : D.t) ~(tm : D.t) f = +let bind ~(name : Ident.local) ~(tp : D.t) f = + let arg = D.var (Eff.read()).size in let update env = { tps = env.tps <: tp; - tms = env.tms <: tm; - names = env.names <: Some name; + tms = env.tms <: arg; + names = env.names <: 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) + Eff.scope update (fun () -> f arg) (** NbE helpers *) @@ -57,88 +50,93 @@ let eval_at arg = Eval.eval ~env:((Eff.read()).tms <: arg) let quote v = Quote.quote ~size:(Eff.read()).size v +(** Pretty-printing helpers *) + +let pp () = let names = (Eff.read()).names in fun fmt tm -> + Syntax.Pretty.pp fmt (tm, names) + (** 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 () -> + Reporter.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 (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 + S.Pi (name.value, base, fam) + | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end | A.Lam (name, body) -> begin match tp with - | D.Pi (base, fam) -> + | 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) + S.Lam (name.value, body) + | _ -> Reporter.fatalf Reporter.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 (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 + S.Sg (name.value, base, fam) + | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (pp()) (quote tp) end | A.Pair (fst, snd) -> begin match tp with - | D.Sg (base, fam) -> + | 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) + | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a Sigma type" (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) + | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (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) + | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of a universe" (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) + | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (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) + | _ -> Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type Bool" (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) + Reporter.fatalf Reporter.Message.IllTyped "expected an element of type @[%a@], but found an element of type @[%a@]" (pp()) (quote tp) (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 () -> + Reporter.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> match tm.value with - | A.Var name -> lookup_name name + | A.Var name -> lookup 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) -> + | (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" + | _ -> Reporter.fatalf Reporter.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" + | (D.Sg (_, base, _), p) -> (base, S.Fst p) + | _ -> Reporter.fatalf Reporter.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) -> + | (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" + | _ -> Reporter.fatalf Reporter.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 @@ -149,9 +147,9 @@ and infer (tm : A.expr) : D.t * S.t = 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 + let tm = S.BoolElim { motive_var = motive_var.value; motive; true_case; false_case; scrut } in (motive_scrut, tm) - | _ -> R.fatalf R.Message.CannotInferType "cannot infer type" + | _ -> Reporter.fatalf Reporter.Message.CannotInferType "cannot infer type" let empty_env : env = { tps = Emp; diff --git a/lib/Eval.ml b/lib/Eval.ml index 033ee8c..bd8326e 100644 --- a/lib/Eval.ml +++ b/lib/Eval.ml @@ -15,7 +15,7 @@ struct Eff.run ~env @@ fun () -> eval body and app v w = match v with - | D.Lam clo -> inst_clo clo w + | D.Lam (_, clo) -> inst_clo clo w | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w) | _ -> invalid_arg "Eval.app" @@ -29,18 +29,18 @@ struct | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Snd) | _ -> invalid_arg "Eval.snd" - and bool_elim cmot vtrue vfalse = function - | D.True -> vtrue - | D.False -> vfalse - | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.BoolElim { cmot; vtrue; vfalse }) + and bool_elim motive_var motive true_case false_case = function + | D.True -> true_case + | D.False -> false_case + | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.BoolElim { motive_var; motive; true_case; false_case }) | _ -> invalid_arg "Eval.bool_elim" and eval = function | S.Var i -> Bwd.nth (Eff.read()) i - | S.Pi (base, fam) -> D.Pi (eval base, make_clo fam) - | S.Lam body -> D.Lam (make_clo body) + | S.Pi (name, base, fam) -> D.Pi (name, eval base, make_clo fam) + | S.Lam (name, body) -> D.Lam (name, make_clo body) | S.App (a, b) -> app (eval a) (eval b) - | S.Sg (base, fam) -> D.Sg (eval base, make_clo fam) + | S.Sg (name, base, fam) -> D.Sg (name, 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) @@ -48,8 +48,8 @@ struct | S.Bool -> D.Bool | S.True -> D.True | S.False -> D.False - | S.BoolElim { motive; true_case; false_case; scrut } -> - bool_elim (make_clo motive) (eval true_case) (eval false_case) (eval scrut) + | S.BoolElim { motive_var; motive; true_case; false_case; scrut } -> + bool_elim motive_var (make_clo motive) (eval true_case) (eval false_case) (eval scrut) end let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm diff --git a/lib/Ident.ml b/lib/Ident.ml new file mode 100644 index 0000000..81c6575 --- /dev/null +++ b/lib/Ident.ml @@ -0,0 +1,9 @@ +type t = Yuujinchou.Trie.path + +type local = string option + +let to_local : t -> local option = function + | name :: [] -> Some (Some name) + | _ -> None + +let pp = Fmt.list ~sep:(Fmt.const Fmt.char '.') Fmt.string diff --git a/lib/Lexer.mll b/lib/Lexer.mll index c33acae..98d1d6b 100644 --- a/lib/Lexer.mll +++ b/lib/Lexer.mll @@ -21,6 +21,7 @@ rule lex = | "," { COMMA } | "." { DOT } | "=>" { FATARROW } + | "_" { UNDERSCORE } | "at" { AT } | "fst" { FST } | "snd" { SND } diff --git a/lib/Parser.mly b/lib/Parser.mly index fc82d1a..8588b56 100644 --- a/lib/Parser.mly +++ b/lib/Parser.mly @@ -5,7 +5,7 @@ open Ast %token <string> IDENT %token LPR RPR %token LBR RBR -%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW +%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE %token BOOL TRUE FALSE BOOL_ELIM AT %token FST SND %token TYPE @@ -28,7 +28,13 @@ raw_ident: id = separated_nonempty_list(DOT, IDENT) { id } %inline ident: id = locate(raw_ident) { id } -arg: LPR; name = ident; COLON; tp = expr; RPR +raw_local_name: + | name = IDENT { Some name } + | UNDERSCORE { None } + +local_name: name = locate(raw_local_name) { name } + +arg: LPR; name = local_name; COLON; tp = expr; RPR { (name, tp) } raw_expr: @@ -41,7 +47,7 @@ raw_expr: | a = arg; ARROW; b = expr { Pi (a, b) } - | BACKSLASH; a = ident; ARROW; b = expr + | BACKSLASH; a = local_name; ARROW; b = expr { Lam (a, b) } | a = expr; b = expr %prec APP { App (a, b) } @@ -64,7 +70,7 @@ raw_expr: { True } | FALSE { False } - | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr; + | BOOL_ELIM; scrut = expr; AT; motive_var = local_name; ARROW; motive_body = expr; LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR { BoolElim { motive_var; motive_body; true_case; false_case; scrut } } diff --git a/lib/Quote.ml b/lib/Quote.ml index 611843a..4b88e91 100644 --- a/lib/Quote.ml +++ b/lib/Quote.ml @@ -15,9 +15,9 @@ struct let rec quote = function | D.Neutral ne -> quote_ne ne - | 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.Pi (name, base, fam) -> S.Pi (name, quote base, quote_clo fam) + | D.Lam (name, clo) -> S.Lam (name, quote_clo clo) + | D.Sg (name, base, fam) -> S.Sg (name, quote base, quote_clo fam) | D.Pair (v, w) -> S.Pair (quote v, quote w) | D.Type -> S.Type | D.Bool -> S.Bool @@ -34,11 +34,12 @@ struct | D.App v -> S.App (hd, quote v) | D.Fst -> S.Fst hd | D.Snd -> S.Snd hd - | D.BoolElim { cmot; vtrue; vfalse } -> + | D.BoolElim { motive_var; motive; true_case; false_case } -> S.BoolElim { - motive = quote_clo cmot; - true_case = quote vtrue; - false_case = quote vfalse; + motive_var; + motive = quote_clo motive; + true_case = quote true_case; + false_case = quote false_case; scrut = hd; } end diff --git a/lib/Reporter.ml b/lib/Reporter.ml index c86a04a..a90966c 100644 --- a/lib/Reporter.ml +++ b/lib/Reporter.ml @@ -1,10 +1,11 @@ module Message = struct - type t = + type t = | SyntaxError | IllTyped | UnboundVariable | CannotInferType + | Bug let default_severity : t -> Asai.Diagnostic.severity = function @@ -12,17 +13,20 @@ struct | IllTyped -> Error | UnboundVariable -> Error | CannotInferType -> Error + | Bug -> Bug let short_code : t -> string = function - | SyntaxError -> "E0001" - | IllTyped -> "E0002" - | UnboundVariable -> "E0003" - | CannotInferType -> "E0004" + | SyntaxError -> "E001" + | IllTyped -> "E002" + | UnboundVariable -> "E003" + | CannotInferType -> "E004" + | Bug -> "BUG" 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 unbound_variable id = fatalf UnboundVariable "unbound variable %a" Ident.pp id +let expected_universe fmt x = fatalf IllTyped "expected a universe but got %a" fmt x -let expected_universe fmt x = fatalf IllTyped "expected a universe but got %a" fmt x
\ No newline at end of file +let bug msg = fatalf Bug msg diff --git a/lib/Syntax.ml b/lib/Syntax.ml index c4cf80d..fc58353 100644 --- a/lib/Syntax.ml +++ b/lib/Syntax.ml @@ -1,11 +1,12 @@ open Bwd +open Bwd.Infix type t = Data.syn = | Var of int - | Pi of t * (* BINDS *) t - | Lam of (* BINDS *) t + | Pi of Ident.local * t * (* BINDS *) t + | Lam of Ident.local * (* BINDS *) t | App of t * t - | Sg of t * (* BINDS *) t + | Sg of Ident.local * t * (* BINDS *) t | Pair of t * t | Fst of t | Snd of t @@ -14,6 +15,7 @@ type t = Data.syn = | True | False | BoolElim of { + motive_var : Ident.local; motive : (* BINDS *) t; true_case : t; false_case : t; @@ -22,23 +24,21 @@ type t = Data.syn = 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 = { + names : Ident.local bwd; prec : int; } module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) + let bind (name : Ident.local) f fmt x = + let update env = { env with names = env.names <: name } in + Eff.scope update (fun () -> f fmt x) + let with_prec (prec : int) (inner : 'a Fmt.t) (fmt : Format.formatter) (v : 'a) = - Eff.scope (fun _ -> { prec; }) (fun () -> inner fmt v) + Eff.scope (fun env -> { env with prec; }) (fun () -> inner fmt v) let delimited inner = with_prec 0 inner @@ -49,49 +49,54 @@ struct Fun.id let lassoc (prec : int) - ?(pre = "") (pp_left : 'l Fmt.t) - ?(middle = " ") - (pp_right : 'r Fmt.t) - ?(post = "") : ('l * 'r) Fmt.t = + ?(sep = " ") + (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = parenthesize prec @@ fun fmt v -> - Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" - pre + Fmt.pf fmt "@[%a@]%s@[%a@]" (with_prec prec pp_left) (fst v) - middle + sep (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 = + ?(sep = " ") + (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = parenthesize prec @@ fun fmt v -> - Fmt.pf fmt "%s@[%a@]%s@[%a@]%s" - pre + Fmt.pf fmt "@[%a@]%s@[%a@]" (with_prec (prec + 1) pp_left) (fst v) - middle + sep (with_prec prec pp_right) (snd v) - post - let pp_var ix fmt = Fmt.pf fmt "%@%d" ix + let pp_local_name fmt name = + Fmt.string fmt @@ Option.value ~default:"_" name + + let pp_var fmt ix = + let names = (Eff.read()).names in + match Bwd.nth_opt names ix with + (* the variable has a bound name which has not been shadowed *) + | Some ((Some name) as id) when Bwd.find_index ((=) id) names = Some ix -> Fmt.string fmt name + (* the variable does not have a bound name or its bound name has been shadowed *) + | Some _ -> Fmt.pf fmt "%@%d" ix + | None -> Reporter.bug "index out of range in pp_var" 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 + (delimited @@ fun fmt (motive_var, motive, true_case, false_case, scrut) -> Fmt.pf fmt + "@[bool-elim @[%a@] at @[%a@] -> @[%a@] [ true => @[%a@], false => @[%a@] ]@]" + 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 + (* 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) + | Var ix -> pp_var fmt ix + | Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam) + | Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body + | Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, 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) @@ -100,10 +105,11 @@ struct | 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) + | BoolElim { motive_var; motive; true_case; false_case; scrut } + -> pp_bool_elim fmt (motive_var, motive, true_case, false_case, scrut) end - let pp fmt tm = - let env : Internal.env = { prec = 0; } in + let pp fmt (tm, names) = + let env : Internal.env = { names; prec = 0; } in Internal.Eff.run ~env (fun () -> Internal.pp fmt tm) end |