diff options
Diffstat (limited to 'lib/Eval.ml')
| -rw-r--r-- | lib/Eval.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/lib/Eval.ml b/lib/Eval.ml index 8f6722b..033ee8c 100644 --- a/lib/Eval.ml +++ b/lib/Eval.ml @@ -8,14 +8,14 @@ module Internal = struct module Eff = Algaeff.Reader.Make (struct type nonrec t = D.env end) - let make_clos body = D.Clos { body; env = Eff.read() } + let make_clo body = D.Clo { body; env = Eff.read() } - let rec inst_clos (D.Clos { body; env }) arg = + 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 clos -> inst_clos clos w + | D.Lam clo -> inst_clo clo w | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.App w) | _ -> invalid_arg "Eval.app" @@ -37,10 +37,10 @@ struct and eval = function | S.Var i -> Bwd.nth (Eff.read()) i - | S.Pi (base, fam) -> D.Pi (eval base, make_clos fam) - | S.Lam body -> D.Lam (make_clos body) + | S.Pi (base, fam) -> D.Pi (eval base, make_clo fam) + | S.Lam body -> D.Lam (make_clo body) | S.App (a, b) -> app (eval a) (eval b) - | S.Sg (base, fam) -> D.Sg (eval base, make_clos fam) + | S.Sg (base, fam) -> D.Sg (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) @@ -49,8 +49,8 @@ struct | S.True -> D.True | S.False -> D.False | S.BoolElim { motive; true_case; false_case; scrut } -> - bool_elim (make_clos motive) (eval true_case) (eval false_case) (eval scrut) + bool_elim (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_clos = Internal.inst_clos +let eval ~env tm = Internal.Eff.run ~env @@ fun () -> Internal.eval tm +let inst_clo = Internal.inst_clo |