about summary refs log tree commit diff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/ast/Ast.ml67
-rw-r--r--src/ast/dune4
-rw-r--r--src/bin/dune11
-rw-r--r--src/bin/main.ml19
-rw-r--r--src/elaborator/Elaborator.ml161
-rw-r--r--src/elaborator/dune11
-rw-r--r--src/ident/Ident.ml9
-rw-r--r--src/ident/dune4
-rw-r--r--src/nbe/Conversion.ml75
-rw-r--r--src/nbe/Data.ml53
-rw-r--r--src/nbe/Domain.ml30
-rw-r--r--src/nbe/Eval.ml56
-rw-r--r--src/nbe/NbE.ml10
-rw-r--r--src/nbe/Quote.ml47
-rw-r--r--src/nbe/Syntax.ml20
-rw-r--r--src/nbe/dune4
-rw-r--r--src/parser/Eff.ml1
-rw-r--r--src/parser/Grammar.mly80
-rw-r--r--src/parser/Lexer.mll37
-rw-r--r--src/parser/Parser.ml13
-rw-r--r--src/parser/dune13
-rw-r--r--src/pretty/Pretty.ml93
-rw-r--r--src/pretty/dune9
-rw-r--r--src/reporter/Reporter.ml40
-rw-r--r--src/reporter/dune4
25 files changed, 871 insertions, 0 deletions
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 <string> 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 <Ast.expr> 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))
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-27 19:27:12 +0000