From 5d227bcd0055d02e1d49a3dcd27e80a756923d5b Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Sun, 23 Jun 2024 23:31:59 +0200 Subject: split code into smaller libraries and make a better repl --- README.md | 3 +- bin/dune | 5 -- bin/main.ml | 25 ------- dune-project | 1 + lib/Ast.ml | 67 ------------------ lib/Conversion.ml | 75 -------------------- lib/Data.ml | 53 -------------- lib/Domain.ml | 30 -------- lib/Elab.ml | 161 ------------------------------------------- lib/Eval.ml | 56 --------------- lib/Eval.mli | 2 - lib/Ident.ml | 9 --- lib/Lexer.mll | 34 --------- lib/Parser.mly | 80 --------------------- lib/ParserEff.ml | 1 - lib/Quote.ml | 48 ------------- lib/Quote.mli | 2 - lib/Reporter.ml | 32 --------- lib/Syntax.ml | 115 ------------------------------- lib/dune | 10 --- src/ast/Ast.ml | 67 ++++++++++++++++++ src/ast/dune | 4 ++ src/bin/dune | 11 +++ src/bin/main.ml | 19 +++++ src/elaborator/Elaborator.ml | 161 +++++++++++++++++++++++++++++++++++++++++++ src/elaborator/dune | 11 +++ src/ident/Ident.ml | 9 +++ src/ident/dune | 4 ++ src/nbe/Conversion.ml | 75 ++++++++++++++++++++ src/nbe/Data.ml | 53 ++++++++++++++ src/nbe/Domain.ml | 30 ++++++++ src/nbe/Eval.ml | 56 +++++++++++++++ src/nbe/NbE.ml | 10 +++ src/nbe/Quote.ml | 47 +++++++++++++ src/nbe/Syntax.ml | 20 ++++++ src/nbe/dune | 4 ++ src/parser/Eff.ml | 1 + src/parser/Grammar.mly | 80 +++++++++++++++++++++ src/parser/Lexer.mll | 37 ++++++++++ src/parser/Parser.ml | 13 ++++ src/parser/dune | 13 ++++ src/pretty/Pretty.ml | 93 +++++++++++++++++++++++++ src/pretty/dune | 9 +++ src/reporter/Reporter.ml | 40 +++++++++++ src/reporter/dune | 4 ++ toytt.opam | 1 + 46 files changed, 875 insertions(+), 806 deletions(-) delete mode 100644 bin/dune delete mode 100644 bin/main.ml delete mode 100644 lib/Ast.ml delete mode 100644 lib/Conversion.ml delete mode 100644 lib/Data.ml delete mode 100644 lib/Domain.ml delete mode 100644 lib/Elab.ml delete mode 100644 lib/Eval.ml delete mode 100644 lib/Eval.mli delete mode 100644 lib/Ident.ml delete mode 100644 lib/Lexer.mll delete mode 100644 lib/Parser.mly delete mode 100644 lib/ParserEff.ml delete mode 100644 lib/Quote.ml delete mode 100644 lib/Quote.mli delete mode 100644 lib/Reporter.ml delete mode 100644 lib/Syntax.ml delete mode 100644 lib/dune create mode 100644 src/ast/Ast.ml create mode 100644 src/ast/dune create mode 100644 src/bin/dune create mode 100644 src/bin/main.ml create mode 100644 src/elaborator/Elaborator.ml create mode 100644 src/elaborator/dune create mode 100644 src/ident/Ident.ml create mode 100644 src/ident/dune create mode 100644 src/nbe/Conversion.ml create mode 100644 src/nbe/Data.ml create mode 100644 src/nbe/Domain.ml create mode 100644 src/nbe/Eval.ml create mode 100644 src/nbe/NbE.ml create mode 100644 src/nbe/Quote.ml create mode 100644 src/nbe/Syntax.ml create mode 100644 src/nbe/dune create mode 100644 src/parser/Eff.ml create mode 100644 src/parser/Grammar.mly create mode 100644 src/parser/Lexer.mll create mode 100644 src/parser/Parser.ml create mode 100644 src/parser/dune create mode 100644 src/pretty/Pretty.ml create mode 100644 src/pretty/dune create mode 100644 src/reporter/Reporter.ml create mode 100644 src/reporter/dune diff --git a/README.md b/README.md index 1d67821..ce6c1f8 100644 --- a/README.md +++ b/README.md @@ -28,7 +28,8 @@ not-function applied to `false` (which evaluates to `true`). - [x] figure out how to recover variable names in pretty-printing so we don't have to print de bruijn indices all the time -- [ ] improve error messages and build a better repl +- [x] build a better repl +- [ ] improve error messages - [ ] implement top-level definitions - [ ] implement less aggrevating syntax for non-dependent function & pair types - [ ] add a type of natural numbers diff --git a/bin/dune b/bin/dune deleted file mode 100644 index 2e2f594..0000000 --- a/bin/dune +++ /dev/null @@ -1,5 +0,0 @@ -(executable - (public_name toytt) - (name main) - (libraries toytt) - (modes byte exe)) diff --git a/bin/main.ml b/bin/main.ml deleted file mode 100644 index afae47c..0000000 --- a/bin/main.ml +++ /dev/null @@ -1,25 +0,0 @@ -open Toytt - -module Term = Asai.Tty.Make(Reporter.Message) - -let parse (s : string) : Ast.expr = - let lexbuf = Lexing.from_string s in - let string_source : Asai.Range.string_source = { - title = None; - content = s; - } in - let source = `String string_source in - ParserEff.Eff.run ~env:source @@ fun () -> - let ast = Parser.parse Lexer.lex lexbuf in - ast - -let rec repl () = - let input = read_line () in - 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, Emp) Syntax.Pretty.pp (Quote.quote ~size:0 tp, Emp); - repl () - -let () = - Reporter.run ~emit:Term.display ~fatal:Term.display @@ fun () -> repl () diff --git a/dune-project b/dune-project index 0fa4b03..f3993f2 100644 --- a/dune-project +++ b/dune-project @@ -24,6 +24,7 @@ asai bwd fmt + linenoise yuujinchou ) (tags diff --git a/lib/Ast.ml b/lib/Ast.ml deleted file mode 100644 index 1a1d4c5..0000000 --- a/lib/Ast.ml +++ /dev/null @@ -1,67 +0,0 @@ -type ident = Ident.t Asai.Range.located -type local_name = Ident.local Asai.Range.located - -type arg = local_name * expr - -and raw_expr = - | Var of Ident.t - | Check of expr * expr - | Pi of arg * expr - | Lam of local_name * expr - | App of expr * expr - | Sg of arg * expr - | Pair of expr * expr - | Fst of expr - | Snd of expr - | Type - | Bool - | True - | False - | BoolElim of { - motive_var : local_name; - motive_body : expr; - true_case : expr; - false_case : expr; - scrut : expr; - } - -and expr = raw_expr Asai.Range.located - -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_local_name name dump_expr tp - -and dump_raw_expr fmt = function - | 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" - | 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_local_name motive_var - dump_expr motive_body - dump_expr true_case - dump_expr false_case - dump_expr scrut - | 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_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 - | 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 - | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p - | Type -> Format.pp_print_string fmt "Type" - -and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value diff --git a/lib/Conversion.ml b/lib/Conversion.ml deleted file mode 100644 index 00bc942..0000000 --- a/lib/Conversion.ml +++ /dev/null @@ -1,75 +0,0 @@ -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 { 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; - | _ -> 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 deleted file mode 100644 index d2f94d3..0000000 --- a/lib/Data.ml +++ /dev/null @@ -1,53 +0,0 @@ -open Bwd - -(** Syntactic terms *) - -type syn = - | Var of int - | Pi of Ident.local * syn * (* BINDS *) syn - | Lam of Ident.local * (* BINDS *) syn - | App of syn * syn - | Sg of Ident.local * syn * (* BINDS *) syn - | Pair of syn * syn - | Fst of syn - | Snd of syn - | Type - | Bool - | True - | False - | BoolElim of { - motive_var : Ident.local; - motive : (* BINDS *) syn; - true_case : syn; - false_case : syn; - scrut : syn; - } - -(** Semantic domain *) - -type value = - | Neutral of ne - | Pi of Ident.local * value * clo - | Lam of Ident.local * clo - | Sg of Ident.local * 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 { - motive_var : Ident.local; - motive: clo; - true_case: value; - false_case: value; - } - -and env = value bwd -and clo = Clo of { body : syn; env : env } diff --git a/lib/Domain.ml b/lib/Domain.ml deleted file mode 100644 index 6f5e11c..0000000 --- a/lib/Domain.ml +++ /dev/null @@ -1,30 +0,0 @@ -open Bwd - -type t = Data.value = - | Neutral of ne - | Pi of Ident.local * t * clo - | Lam of Ident.local * clo - | Sg of Ident.local * t * clo - | Pair of t * t - | Type - | Bool - | True - | False - -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 { - motive_var : Ident.local; - motive : clo; - true_case : t; - false_case: t; - } - -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 deleted file mode 100644 index d911b9f..0000000 --- a/lib/Elab.ml +++ /dev/null @@ -1,161 +0,0 @@ -open Bwd -open Bwd.Infix - -module A = Ast -module S = Syntax -module D = Domain - -(* TODO: REALLY improve error messages *) - -(* invariant: `tps`, `tms` and `names` all have length `size` *) -type env = { - tps : D.env; - tms : D.env; - names : Ident.local bwd; - size : int; -} - -module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) - -(** General helpers *) - -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 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 <: arg; - names = env.names <: name; - size = env.size + 1; - } in - Eff.scope update (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 - -(** 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 = - 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 (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) -> - 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 (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 (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) -> - 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) - | _ -> 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 - | _ -> 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 - | _ -> 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 - | _ -> 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 - | _ -> 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 -> - 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 = - Reporter.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> - match tm.value with - | 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) -> - 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) - | _ -> 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) - | _ -> 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) -> - let tp = Eval.inst_clo fam (eval (S.Fst p)) in - let tm = S.Snd p in - (tp, tm) - | _ -> 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 - 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_var = motive_var.value; motive; true_case; false_case; scrut } in - (motive_scrut, tm) - | _ -> Reporter.fatalf Reporter.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 deleted file mode 100644 index bd8326e..0000000 --- a/lib/Eval.ml +++ /dev/null @@ -1,56 +0,0 @@ -open Bwd -open Bwd.Infix - -module S = Syntax -module D = Domain - -module Internal = -struct - module Eff = Algaeff.Reader.Make (struct type nonrec t = D.env end) - - let make_clo body = D.Clo { body; env = Eff.read() } - - 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 (_, clo) -> inst_clo clo w - | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w) - | _ -> invalid_arg "Eval.app" - - and fst = function - | D.Pair (v, _) -> v - | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Fst) - | _ -> invalid_arg "Eval.fst" - - and snd = function - | D.Pair (_, v) -> v - | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Snd) - | _ -> invalid_arg "Eval.snd" - - 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 (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 (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) - | S.Type -> D.Type - | S.Bool -> D.Bool - | S.True -> D.True - | S.False -> D.False - | 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 -let inst_clo = Internal.inst_clo diff --git a/lib/Eval.mli b/lib/Eval.mli deleted file mode 100644 index 63c49cf..0000000 --- a/lib/Eval.mli +++ /dev/null @@ -1,2 +0,0 @@ -val eval : env:Domain.env -> Syntax.t -> Domain.t -val inst_clo : Domain.clo -> Domain.t -> Domain.t diff --git a/lib/Ident.ml b/lib/Ident.ml deleted file mode 100644 index 81c6575..0000000 --- a/lib/Ident.ml +++ /dev/null @@ -1,9 +0,0 @@ -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 deleted file mode 100644 index 98d1d6b..0000000 --- a/lib/Lexer.mll +++ /dev/null @@ -1,34 +0,0 @@ -{ -open Parser -} - -let whitespace = [' ' '\t' '\r' '\n']+ -let letter = ['a'-'z' 'A'-'Z'] -let ident = letter+ - -rule lex = - parse - | whitespace { lex lexbuf } - | "(" { LPR } - | ")" { RPR } - | "[" { LBR } - | "]" { RBR } - | "->" { ARROW } - | "*" { ASTERISK } - | "\\" { BACKSLASH } - | "::" { DOUBLE_COLON } - | ":" { COLON } - | "," { COMMA } - | "." { DOT } - | "=>" { FATARROW } - | "_" { UNDERSCORE } - | "at" { AT } - | "fst" { FST } - | "snd" { SND } - | "type" { TYPE } - | "bool" { BOOL } - | "true" { TRUE } - | "false" { FALSE } - | "bool-elim" { BOOL_ELIM } - | ident { IDENT (Lexing.lexeme lexbuf) } - | eof { EOF } diff --git a/lib/Parser.mly b/lib/Parser.mly deleted file mode 100644 index 8588b56..0000000 --- a/lib/Parser.mly +++ /dev/null @@ -1,80 +0,0 @@ -%{ -open Ast -%} - -%token IDENT -%token LPR RPR -%token LBR RBR -%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE -%token BOOL TRUE FALSE BOOL_ELIM AT -%token FST SND -%token TYPE -%token EOF - -%nonassoc DOUBLE_COLON -%right ARROW -%right ASTERISK -%left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM - -%start parse - -%% - -%inline -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_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: - | 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) } - | BACKSLASH; a = local_name; ARROW; b = expr - { Lam (a, b) } - | a = expr; b = expr %prec APP - { App (a, b) } - - | a = arg; ASTERISK; b = expr - { Sg (a, b) } - | LPR; a = expr; COMMA; b = expr; RPR - { Pair (a, b) } - | FST; p = expr - { Fst p } - | SND; p = expr - { Snd p } - - | TYPE - { Type } - - | BOOL - { Bool } - | TRUE - { True } - | FALSE - { False } - | 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 } } - -%inline -expr: e = locate(raw_expr) { e } - -parse: e = expr; EOF { e } diff --git a/lib/ParserEff.ml b/lib/ParserEff.ml deleted file mode 100644 index 84c0de8..0000000 --- a/lib/ParserEff.ml +++ /dev/null @@ -1 +0,0 @@ -module Eff = Algaeff.Reader.Make (struct type nonrec t = Asai.Range.source end) diff --git a/lib/Quote.ml b/lib/Quote.ml deleted file mode 100644 index 4b88e91..0000000 --- a/lib/Quote.ml +++ /dev/null @@ -1,48 +0,0 @@ -open Bwd - -module S = Syntax -module D = Domain - -module Internal = -struct - (* keeping track of the context size *) - module Eff = Algaeff.Reader.Make (struct type t = int end) - - let bind f = - let arg = D.var (Eff.read()) in - Eff.scope (fun size -> size + 1) @@ fun () -> - f arg - - let rec quote = function - | D.Neutral ne -> quote_ne ne - | 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 - | D.True -> S.True - | D.False -> S.False - - and quote_clo clo = bind @@ fun arg -> quote (Eval.inst_clo clo arg) - - 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_frm hd = function - | D.App v -> S.App (hd, quote v) - | D.Fst -> S.Fst hd - | D.Snd -> S.Snd hd - | D.BoolElim { motive_var; motive; true_case; false_case } -> - S.BoolElim { - motive_var; - motive = quote_clo motive; - true_case = quote true_case; - false_case = quote false_case; - scrut = hd; - } -end - -let quote ~size v = Internal.Eff.run ~env:size (fun () -> Internal.quote v) -let quote_ne ~size ne = Internal.Eff.run ~env:size (fun () -> Internal.quote_ne ne) diff --git a/lib/Quote.mli b/lib/Quote.mli deleted file mode 100644 index 193b0b0..0000000 --- a/lib/Quote.mli +++ /dev/null @@ -1,2 +0,0 @@ -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 deleted file mode 100644 index a90966c..0000000 --- a/lib/Reporter.ml +++ /dev/null @@ -1,32 +0,0 @@ -module Message = -struct - type t = - | SyntaxError - | IllTyped - | UnboundVariable - | CannotInferType - | Bug - - let default_severity : t -> Asai.Diagnostic.severity = - function - | SyntaxError -> Error - | IllTyped -> Error - | UnboundVariable -> Error - | CannotInferType -> Error - | Bug -> Bug - - let short_code : t -> string = - function - | SyntaxError -> "E001" - | IllTyped -> "E002" - | UnboundVariable -> "E003" - | CannotInferType -> "E004" - | Bug -> "BUG" -end - -include Asai.Reporter.Make(Message) - -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 bug msg = fatalf Bug msg diff --git a/lib/Syntax.ml b/lib/Syntax.ml deleted file mode 100644 index fc58353..0000000 --- a/lib/Syntax.ml +++ /dev/null @@ -1,115 +0,0 @@ -open Bwd -open Bwd.Infix - -type t = Data.syn = - | Var of int - | Pi of Ident.local * t * (* BINDS *) t - | Lam of Ident.local * (* BINDS *) t - | App of t * t - | Sg of Ident.local * t * (* BINDS *) t - | Pair of t * t - | Fst of t - | Snd of t - | Type - | Bool - | True - | False - | BoolElim of { - motive_var : Ident.local; - motive : (* BINDS *) t; - true_case : t; - false_case : t; - scrut : t; - } - -module Pretty = -struct - 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 env -> { env with 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) - (pp_left : 'l Fmt.t) - ?(sep = " ") - (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = - parenthesize prec @@ fun fmt v -> - Fmt.pf fmt "@[%a@]%s@[%a@]" - (with_prec prec pp_left) (fst v) - sep - (with_prec (prec + 1) pp_right) (snd v) - - let rassoc (prec : int) - (pp_left : 'l Fmt.t) - ?(sep = " ") - (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = - parenthesize prec @@ fun fmt v -> - Fmt.pf fmt "@[%a@]%s@[%a@]" - (with_prec (prec + 1) pp_left) (fst v) - sep - (with_prec prec pp_right) (snd v) - - 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_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 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) - | 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_var; motive; true_case; false_case; scrut } - -> pp_bool_elim fmt (motive_var, motive, true_case, false_case, scrut) - end - - let pp fmt (tm, names) = - let env : Internal.env = { names; prec = 0; } in - Internal.Eff.run ~env (fun () -> Internal.pp fmt tm) -end diff --git a/lib/dune b/lib/dune deleted file mode 100644 index 3d2f366..0000000 --- a/lib/dune +++ /dev/null @@ -1,10 +0,0 @@ -(menhir - (explain true) - (modules Parser)) - -(ocamllex Lexer) - -(library - (name toytt) - (libraries asai fmt yuujinchou) - (preprocess (pps ppx_deriving.std))) diff --git a/src/ast/Ast.ml b/src/ast/Ast.ml new file mode 100644 index 0000000..1a1d4c5 --- /dev/null +++ b/src/ast/Ast.ml @@ -0,0 +1,67 @@ +type ident = Ident.t Asai.Range.located +type local_name = Ident.local Asai.Range.located + +type arg = local_name * expr + +and raw_expr = + | Var of Ident.t + | Check of expr * expr + | Pi of arg * expr + | Lam of local_name * expr + | App of expr * expr + | Sg of arg * expr + | Pair of expr * expr + | Fst of expr + | Snd of expr + | Type + | Bool + | True + | False + | BoolElim of { + motive_var : local_name; + motive_body : expr; + true_case : expr; + false_case : expr; + scrut : expr; + } + +and expr = raw_expr Asai.Range.located + +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_local_name name dump_expr tp + +and dump_raw_expr fmt = function + | 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" + | 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_local_name motive_var + dump_expr motive_body + dump_expr true_case + dump_expr false_case + dump_expr scrut + | 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_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 + | 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 + | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p + | Type -> Format.pp_print_string fmt "Type" + +and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value diff --git a/src/ast/dune b/src/ast/dune new file mode 100644 index 0000000..072fe89 --- /dev/null +++ b/src/ast/dune @@ -0,0 +1,4 @@ +(library + (name Ast) + (public_name toytt.ast) + (libraries asai toytt.ident)) diff --git a/src/bin/dune b/src/bin/dune new file mode 100644 index 0000000..980d799 --- /dev/null +++ b/src/bin/dune @@ -0,0 +1,11 @@ +(executable + (public_name toytt) + (name main) + (libraries + asai + linenoise + toytt.elaborator + toytt.nbe + toytt.parser + toytt.reporter + )) diff --git a/src/bin/main.ml b/src/bin/main.ml new file mode 100644 index 0000000..f762d26 --- /dev/null +++ b/src/bin/main.ml @@ -0,0 +1,19 @@ +module Term = Asai.Tty.Make(Reporter.Message) + +let ep input = + let ast = Parser.parse_expr input in + let (tp, tm) = Elaborator.infer_toplevel ast in + let value = NbE.eval ~env:Emp tm in + Format.printf "%a : %a\n%!" + (Pretty.pp ~names:Emp) (NbE.quote ~size:0 value) + (Pretty.pp ~names:Emp) (NbE.quote ~size:0 tp) + +let rec repl () = + match LNoise.linenoise "toytt> " with + | Some input -> + Reporter.run ~emit:Term.display ~fatal:Term.display (fun () -> ep input); + let _ = LNoise.history_add input in + repl () + | None -> repl () + +let () = repl (); diff --git a/src/elaborator/Elaborator.ml b/src/elaborator/Elaborator.ml new file mode 100644 index 0000000..0f72f24 --- /dev/null +++ b/src/elaborator/Elaborator.ml @@ -0,0 +1,161 @@ +open Bwd +open Bwd.Infix + +module A = Ast +module S = NbE.Syntax +module D = NbE.Domain + +(* TODO: REALLY improve error messages *) + +(* invariant: `tps`, `tms` and `names` all have length `size` *) +type env = { + tps : D.env; + tms : D.env; + names : Ident.local bwd; + size : int; +} + +module Eff = Algaeff.Reader.Make (struct type nonrec t = env end) + +(** General helpers *) + +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 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 <: arg; + names = env.names <: name; + size = env.size + 1; + } in + Eff.scope update (fun () -> f arg) + +(** NbE helpers *) + +let eval tm = NbE.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 = NbE.eval ~env:((Eff.read()).tms <: arg) + +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 + +(** Main algorithm *) + +let rec check ~(tm : A.expr) ~(tp : D.t) : S.t = + 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 (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) -> + let body = bind ~name:name.value ~tp:base @@ fun arg -> + let fib = NbE.inst_clo fam arg in + check ~tm:body ~tp:fib in + 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 (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) -> + let fst = check ~tm:fst ~tp:base in + let fib = NbE.inst_clo fam (eval fst) in + let snd = check ~tm:snd ~tp:fib in + S.Pair (fst, snd) + | _ -> 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 + | _ -> 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 + | _ -> 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 + | _ -> 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 + | _ -> 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 NbE.equate ~size:((Eff.read()).size) inferred_tp tp with + | NbE.Unequal -> + 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 = + Reporter.tracef ?loc:tm.loc "when inferring the type" @@ fun () -> + match tm.value with + | 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) -> + let arg = check ~tm:arg ~tp:base in + let tp = NbE.inst_clo fam (eval arg) in + let tm = S.App (fn, arg) in + (tp, tm) + | _ -> 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) + | _ -> 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) -> + let tp = NbE.inst_clo fam (eval (S.Fst p)) in + let tm = S.Snd p in + (tp, tm) + | _ -> 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 + 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_var = motive_var.value; motive; true_case; false_case; scrut } in + (motive_scrut, tm) + | _ -> Reporter.fatalf Reporter.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/src/elaborator/dune b/src/elaborator/dune new file mode 100644 index 0000000..46227f0 --- /dev/null +++ b/src/elaborator/dune @@ -0,0 +1,11 @@ +(library + (name Elaborator) + (public_name toytt.elaborator) + (libraries + algaeff + bwd + toytt.ast + toytt.ident + toytt.nbe + toytt.pretty + toytt.reporter)) diff --git a/src/ident/Ident.ml b/src/ident/Ident.ml new file mode 100644 index 0000000..81c6575 --- /dev/null +++ b/src/ident/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/src/ident/dune b/src/ident/dune new file mode 100644 index 0000000..732a2c7 --- /dev/null +++ b/src/ident/dune @@ -0,0 +1,4 @@ +(library + (name Ident) + (public_name toytt.ident) + (libraries fmt yuujinchou)) diff --git a/src/nbe/Conversion.ml b/src/nbe/Conversion.ml new file mode 100644 index 0000000..00bc942 --- /dev/null +++ b/src/nbe/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 { 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; + | _ -> 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/src/nbe/Data.ml b/src/nbe/Data.ml new file mode 100644 index 0000000..d2f94d3 --- /dev/null +++ b/src/nbe/Data.ml @@ -0,0 +1,53 @@ +open Bwd + +(** Syntactic terms *) + +type syn = + | Var of int + | Pi of Ident.local * syn * (* BINDS *) syn + | Lam of Ident.local * (* BINDS *) syn + | App of syn * syn + | Sg of Ident.local * syn * (* BINDS *) syn + | Pair of syn * syn + | Fst of syn + | Snd of syn + | Type + | Bool + | True + | False + | BoolElim of { + motive_var : Ident.local; + motive : (* BINDS *) syn; + true_case : syn; + false_case : syn; + scrut : syn; + } + +(** Semantic domain *) + +type value = + | Neutral of ne + | Pi of Ident.local * value * clo + | Lam of Ident.local * clo + | Sg of Ident.local * 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 { + motive_var : Ident.local; + motive: clo; + true_case: value; + false_case: value; + } + +and env = value bwd +and clo = Clo of { body : syn; env : env } diff --git a/src/nbe/Domain.ml b/src/nbe/Domain.ml new file mode 100644 index 0000000..6f5e11c --- /dev/null +++ b/src/nbe/Domain.ml @@ -0,0 +1,30 @@ +open Bwd + +type t = Data.value = + | Neutral of ne + | Pi of Ident.local * t * clo + | Lam of Ident.local * clo + | Sg of Ident.local * t * clo + | Pair of t * t + | Type + | Bool + | True + | False + +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 { + motive_var : Ident.local; + motive : clo; + true_case : t; + false_case: t; + } + +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/src/nbe/Eval.ml b/src/nbe/Eval.ml new file mode 100644 index 0000000..bd8326e --- /dev/null +++ b/src/nbe/Eval.ml @@ -0,0 +1,56 @@ +open Bwd +open Bwd.Infix + +module S = Syntax +module D = Domain + +module Internal = +struct + module Eff = Algaeff.Reader.Make (struct type nonrec t = D.env end) + + let make_clo body = D.Clo { body; env = Eff.read() } + + 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 (_, clo) -> inst_clo clo w + | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w) + | _ -> invalid_arg "Eval.app" + + and fst = function + | D.Pair (v, _) -> v + | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Fst) + | _ -> invalid_arg "Eval.fst" + + and snd = function + | D.Pair (_, v) -> v + | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.Snd) + | _ -> invalid_arg "Eval.snd" + + 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 (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 (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) + | S.Type -> D.Type + | S.Bool -> D.Bool + | S.True -> D.True + | S.False -> D.False + | 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 +let inst_clo = Internal.inst_clo diff --git a/src/nbe/NbE.ml b/src/nbe/NbE.ml new file mode 100644 index 0000000..3ec1f6d --- /dev/null +++ b/src/nbe/NbE.ml @@ -0,0 +1,10 @@ +module Syntax = Syntax +module Domain = Domain + +let eval = Eval.eval +let inst_clo = Eval.inst_clo + +let quote = Quote.quote + +exception Unequal = Conversion.Unequal +let equate = Conversion.equate diff --git a/src/nbe/Quote.ml b/src/nbe/Quote.ml new file mode 100644 index 0000000..cc5a81e --- /dev/null +++ b/src/nbe/Quote.ml @@ -0,0 +1,47 @@ +open Bwd + +module S = Syntax +module D = Domain + +module Internal = +struct + (* keeping track of the context size *) + module Eff = Algaeff.Reader.Make (struct type t = int end) + + let bind f = + let arg = D.var (Eff.read()) in + Eff.scope (fun size -> size + 1) @@ fun () -> + f arg + + let rec quote = function + | D.Neutral ne -> quote_ne ne + | 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 + | D.True -> S.True + | D.False -> S.False + + and quote_clo clo = bind @@ fun arg -> quote (Eval.inst_clo clo arg) + + 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_frm hd = function + | D.App v -> S.App (hd, quote v) + | D.Fst -> S.Fst hd + | D.Snd -> S.Snd hd + | D.BoolElim { motive_var; motive; true_case; false_case } -> + S.BoolElim { + motive_var; + motive = quote_clo motive; + true_case = quote true_case; + false_case = quote false_case; + scrut = hd; + } +end + +let quote ~size v = Internal.Eff.run ~env:size (fun () -> Internal.quote v) diff --git a/src/nbe/Syntax.ml b/src/nbe/Syntax.ml new file mode 100644 index 0000000..dd690fb --- /dev/null +++ b/src/nbe/Syntax.ml @@ -0,0 +1,20 @@ +type t = Data.syn = + | Var of int + | Pi of Ident.local * t * (* BINDS *) t + | Lam of Ident.local * (* BINDS *) t + | App of t * t + | Sg of Ident.local * t * (* BINDS *) t + | Pair of t * t + | Fst of t + | Snd of t + | Type + | Bool + | True + | False + | BoolElim of { + motive_var : Ident.local; + motive : (* BINDS *) t; + true_case : t; + false_case : t; + scrut : t; + } diff --git a/src/nbe/dune b/src/nbe/dune new file mode 100644 index 0000000..b7c9bed --- /dev/null +++ b/src/nbe/dune @@ -0,0 +1,4 @@ +(library + (name NbE) + (public_name toytt.nbe) + (libraries algaeff bwd toytt.ident toytt.reporter)) diff --git a/src/parser/Eff.ml b/src/parser/Eff.ml new file mode 100644 index 0000000..45887b8 --- /dev/null +++ b/src/parser/Eff.ml @@ -0,0 +1 @@ +include Algaeff.Reader.Make (struct type nonrec t = Asai.Range.source end) \ No newline at end of file diff --git a/src/parser/Grammar.mly b/src/parser/Grammar.mly new file mode 100644 index 0000000..bb98029 --- /dev/null +++ b/src/parser/Grammar.mly @@ -0,0 +1,80 @@ +%{ +open Ast +%} + +%token IDENT +%token LPR RPR +%token LBR RBR +%token ARROW ASTERISK BACKSLASH COLON DOUBLE_COLON COMMA DOT FATARROW UNDERSCORE +%token BOOL TRUE FALSE BOOL_ELIM AT +%token FST SND +%token TYPE +%token EOF + +%nonassoc DOUBLE_COLON +%right ARROW +%right ASTERISK +%left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM + +%start start_expr + +%% + +%inline +locate(X): e = X { Asai.Range.locate_lex ~source:(Eff.read()) $loc e } + +raw_ident: id = separated_nonempty_list(DOT, IDENT) { id } + +%inline +ident: id = locate(raw_ident) { id } + +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: + | 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) } + | BACKSLASH; a = local_name; ARROW; b = expr + { Lam (a, b) } + | a = expr; b = expr %prec APP + { App (a, b) } + + | a = arg; ASTERISK; b = expr + { Sg (a, b) } + | LPR; a = expr; COMMA; b = expr; RPR + { Pair (a, b) } + | FST; p = expr + { Fst p } + | SND; p = expr + { Snd p } + + | TYPE + { Type } + + | BOOL + { Bool } + | TRUE + { True } + | FALSE + { False } + | 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 } } + +%inline +expr: e = locate(raw_expr) { e } + +start_expr: e = expr; EOF { e } diff --git a/src/parser/Lexer.mll b/src/parser/Lexer.mll new file mode 100644 index 0000000..708bb64 --- /dev/null +++ b/src/parser/Lexer.mll @@ -0,0 +1,37 @@ +{ +open Grammar + +exception IllegalCharacter of char +} + +let whitespace = [' ' '\t' '\r' '\n']+ +let letter = ['a'-'z' 'A'-'Z'] +let ident = letter+ + +rule token = + parse + | whitespace { token lexbuf } + | "(" { LPR } + | ")" { RPR } + | "[" { LBR } + | "]" { RBR } + | "->" { ARROW } + | "*" { ASTERISK } + | "\\" { BACKSLASH } + | "::" { DOUBLE_COLON } + | ":" { COLON } + | "," { COMMA } + | "." { DOT } + | "=>" { FATARROW } + | "_" { UNDERSCORE } + | "at" { AT } + | "fst" { FST } + | "snd" { SND } + | "type" { TYPE } + | "bool" { BOOL } + | "true" { TRUE } + | "false" { FALSE } + | "bool-elim" { BOOL_ELIM } + | ident { IDENT (Lexing.lexeme lexbuf) } + | eof { EOF } + | (_ as illegal_char) { raise (IllegalCharacter illegal_char) } diff --git a/src/parser/Parser.ml b/src/parser/Parser.ml new file mode 100644 index 0000000..4593d82 --- /dev/null +++ b/src/parser/Parser.ml @@ -0,0 +1,13 @@ +let parse_expr (s : string) : Ast.expr = + let lexbuf = Lexing.from_string s in + let string_source : Asai.Range.string_source = { + title = None; + content = s; + } in + let source = `String string_source in + Eff.run ~env:source @@ fun () -> + try Grammar.start_expr Lexer.token lexbuf with + | Lexer.IllegalCharacter illegal_char -> + Reporter.illegal_character ~loc:(Asai.Range.of_lexbuf ~source lexbuf) illegal_char + | Grammar.Error -> + Reporter.syntax_error ~loc:(Asai.Range.of_lexbuf ~source lexbuf) diff --git a/src/parser/dune b/src/parser/dune new file mode 100644 index 0000000..fd4aae7 --- /dev/null +++ b/src/parser/dune @@ -0,0 +1,13 @@ +(menhir + (explain true) + (modules Grammar)) + +(ocamllex Lexer) + +(library + (name Parser) + (public_name toytt.parser) + (libraries + asai + toytt.ast + toytt.reporter)) diff --git a/src/pretty/Pretty.ml b/src/pretty/Pretty.ml new file mode 100644 index 0000000..66d6159 --- /dev/null +++ b/src/pretty/Pretty.ml @@ -0,0 +1,93 @@ +open Bwd +open Bwd.Infix + +module S = NbE.Syntax + +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 env -> { env with 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) + (pp_left : 'l Fmt.t) + ?(sep = " ") + (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = + parenthesize prec @@ fun fmt v -> + Fmt.pf fmt "@[%a@]%s@[%a@]" + (with_prec prec pp_left) (fst v) + sep + (with_prec (prec + 1) pp_right) (snd v) + + let rassoc (prec : int) + (pp_left : 'l Fmt.t) + ?(sep = " ") + (pp_right : 'r Fmt.t) : ('l * 'r) Fmt.t = + parenthesize prec @@ fun fmt v -> + Fmt.pf fmt "@[%a@]%s@[%a@]" + (with_prec (prec + 1) pp_left) (fst v) + sep + (with_prec prec pp_right) (snd v) + + 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_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 + | S.Var ix -> pp_var fmt ix + | S.Pi (name, base, fam) -> rassoc 1 pp_arg ~sep:" -> " (bind name pp) fmt ((name, base), fam) + | S.Lam (name, body) -> Fmt.pf fmt "@[\\@[%a@] -> @[%a@]@]" pp_local_name name (bind name pp) body + | S.Sg (name, base, fam) -> rassoc 2 pp_arg ~sep:" * " (bind name pp) fmt ((name, base), fam) + | S.App (a, b) -> lassoc 3 pp pp fmt (a, b) + | S.Pair (a, b) -> pp_pair fmt (a, b) + | S.Fst a -> lassoc 3 Fmt.string pp fmt ("fst", a) + | S.Snd a -> lassoc 3 Fmt.string pp fmt ("snd", a) + | S.Type -> Fmt.string fmt "type" + | S.Bool -> Fmt.string fmt "bool" + | S.True -> Fmt.string fmt "true" + | S.False -> Fmt.string fmt "false" + | S.BoolElim { motive_var; motive; true_case; false_case; scrut } + -> pp_bool_elim fmt (motive_var, motive, true_case, false_case, scrut) +end + +let pp ~names fmt tm = + let env : Internal.env = { names; prec = 0; } in + Internal.Eff.run ~env (fun () -> Internal.pp fmt tm) diff --git a/src/pretty/dune b/src/pretty/dune new file mode 100644 index 0000000..df46822 --- /dev/null +++ b/src/pretty/dune @@ -0,0 +1,9 @@ +(library + (name Pretty) + (public_name toytt.pretty) + (libraries + bwd + fmt + toytt.ident + toytt.nbe + toytt.reporter)) diff --git a/src/reporter/Reporter.ml b/src/reporter/Reporter.ml new file mode 100644 index 0000000..ee04c23 --- /dev/null +++ b/src/reporter/Reporter.ml @@ -0,0 +1,40 @@ +module Message = +struct + type t = + | IllegalCharacter + | SyntaxError + | UnboundVariable + | IllTyped + | CannotInferType + | Bug + + let default_severity : t -> Asai.Diagnostic.severity = + function + | IllegalCharacter -> Error + | SyntaxError -> Error + | UnboundVariable -> Error + | IllTyped -> Error + | CannotInferType -> Error + | Bug -> Bug + + let short_code : t -> string = + function + (* parser errors *) + | IllegalCharacter -> "E101" + | SyntaxError -> "E102" + (* elaboration errors *) + | UnboundVariable -> "E201" + | IllTyped -> "E202" + | CannotInferType -> "E202" + (* misc *) + | Bug -> "E900" +end + +include Asai.Reporter.Make(Message) + +let illegal_character ~loc char = fatalf ~loc IllegalCharacter "illegal character '%s'" (Char.escaped char) +let syntax_error ~loc = fatalf ~loc SyntaxError "syntax error" +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 bug msg = fatalf Bug msg diff --git a/src/reporter/dune b/src/reporter/dune new file mode 100644 index 0000000..ab0f04a --- /dev/null +++ b/src/reporter/dune @@ -0,0 +1,4 @@ +(library + (name Reporter) + (public_name toytt.reporter) + (libraries asai toytt.ident)) diff --git a/toytt.opam b/toytt.opam index a10e9c7..ed17cae 100644 --- a/toytt.opam +++ b/toytt.opam @@ -18,6 +18,7 @@ depends: [ "asai" "bwd" "fmt" + "linenoise" "yuujinchou" "odoc" {with-doc} ] -- cgit 1.4.1