about summary refs log tree commit diff
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-pink 1.4.1 (git 2.36.1) at 2024-09-27 17:18:16 +0000