split code into smaller libraries and make a better repl

1 files changed, 0 insertions, 56 deletions

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