aboutsummaryrefslogtreecommitdiff
path: root/src/nbe
diff options
context:
space:
mode:
Diffstat (limited to 'src/nbe')
-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
8 files changed, 295 insertions, 0 deletions
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))
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-14 07:52:33 +0000