From 5d227bcd0055d02e1d49a3dcd27e80a756923d5b Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Sun, 23 Jun 2024 23:31:59 +0200 Subject: split code into smaller libraries and make a better repl --- src/nbe/Conversion.ml | 75 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/nbe/Data.ml | 53 ++++++++++++++++++++++++++++++++++++ src/nbe/Domain.ml | 30 +++++++++++++++++++++ src/nbe/Eval.ml | 56 ++++++++++++++++++++++++++++++++++++++ src/nbe/NbE.ml | 10 +++++++ src/nbe/Quote.ml | 47 ++++++++++++++++++++++++++++++++ src/nbe/Syntax.ml | 20 ++++++++++++++ src/nbe/dune | 4 +++ 8 files changed, 295 insertions(+) create mode 100644 src/nbe/Conversion.ml create mode 100644 src/nbe/Data.ml create mode 100644 src/nbe/Domain.ml create mode 100644 src/nbe/Eval.ml create mode 100644 src/nbe/NbE.ml create mode 100644 src/nbe/Quote.ml create mode 100644 src/nbe/Syntax.ml create mode 100644 src/nbe/dune (limited to 'src/nbe') 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)) -- cgit 1.4.1