about summary refs log tree commit diff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/Ast.ml67
-rw-r--r--lib/Conversion.ml75
-rw-r--r--lib/Data.ml53
-rw-r--r--lib/Domain.ml30
-rw-r--r--lib/Elab.ml161
-rw-r--r--lib/Eval.ml56
-rw-r--r--lib/Eval.mli2
-rw-r--r--lib/Ident.ml9
-rw-r--r--lib/Lexer.mll34
-rw-r--r--lib/Parser.mly80
-rw-r--r--lib/ParserEff.ml1
-rw-r--r--lib/Quote.ml48
-rw-r--r--lib/Quote.mli2
-rw-r--r--lib/Reporter.ml32
-rw-r--r--lib/Syntax.ml115
-rw-r--r--lib/dune10
16 files changed, 0 insertions, 775 deletions
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 <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> 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)))
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-09-27 17:15:38 +0000