diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Ast.ml | 16 | ||||
| -rw-r--r-- | lib/Domain.ml | 27 | ||||
| -rw-r--r-- | lib/Eval.ml | 55 | ||||
| -rw-r--r-- | lib/Eval.mli | 1 | ||||
| -rw-r--r-- | lib/Lexer.mll | 8 | ||||
| -rw-r--r-- | lib/Parser.mly | 21 | ||||
| -rw-r--r-- | lib/Syntax.ml | 19 |
7 files changed, 125 insertions, 22 deletions
@@ -6,6 +6,14 @@ and arg = raw_arg Asai.Range.located and raw_expr = | Var of raw_ident + | Pi of arg * expr + | Lam of ident * expr + | App of expr * expr + | Sg of arg * expr + | Pair of expr * expr + | Fst of expr + | Snd of expr + | Type | Bool | True | False @@ -16,14 +24,6 @@ and raw_expr = false_case : expr; scrut : expr; } - | Pi of arg * expr - | Lam of ident * expr - | App of expr * expr - | Sg of arg * expr - | Pair of expr * expr - | Fst of expr - | Snd of expr - | Type and expr = raw_expr Asai.Range.located diff --git a/lib/Domain.ml b/lib/Domain.ml new file mode 100644 index 0000000..cf07a4b --- /dev/null +++ b/lib/Domain.ml @@ -0,0 +1,27 @@ +open Bwd + +type value = + | Neutral of ne + | Pi of value * clos + | Lam of clos + | Sg of value * clos + | Pair of value * value + | Type + | Bool + | True + | False + +and ne = ne_head * frame bwd +and ne_head = Var of int (* De Bruijn levels *) +and frame = + | BoolElim of { + cmot: clos; + vtrue: value; + vfalse: value; + } + | App of value + | Fst + | Snd + +and env = value bwd +and clos = Clos of { body : Syntax.tm; env : env } diff --git a/lib/Eval.ml b/lib/Eval.ml new file mode 100644 index 0000000..29ede14 --- /dev/null +++ b/lib/Eval.ml @@ -0,0 +1,55 @@ +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_clos body = D.Clos { body; env = Eff.read() } + + let rec inst_clos (D.Clos { 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.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 cmot vtrue vfalse = function + | D.True -> vtrue + | D.False -> vfalse + | D.Neutral (hd, frms) -> D.Neutral (hd, frms <: D.BoolElim { cmot; vtrue; vfalse }) + | _ -> invalid_arg "Eval.bool_elim" + + and eval = function + | S.Var i -> BwdLabels.nth (Eff.read()) i + | S.Pi (base, fam) -> D.Pi (eval base, make_clos fam) + | S.Lam body -> D.Lam (make_clos body) + | S.App (a, b) -> app (eval a) (eval b) + | S.Sg (base, fam) -> D.Sg (eval base, make_clos 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; true_case; false_case; scrut } -> + bool_elim (make_clos motive) (eval true_case) (eval false_case) (eval scrut) +end + +let eval ~env tm = Internal.Eff.run ~env (fun () -> Internal.eval tm) diff --git a/lib/Eval.mli b/lib/Eval.mli new file mode 100644 index 0000000..aaa8977 --- /dev/null +++ b/lib/Eval.mli @@ -0,0 +1 @@ +val eval : env:Domain.env -> Syntax.tm -> Domain.value diff --git a/lib/Lexer.mll b/lib/Lexer.mll index a8410d0..3f178f5 100644 --- a/lib/Lexer.mll +++ b/lib/Lexer.mll @@ -20,13 +20,13 @@ rule lex = | "," { COMMA } | "." { DOT } | "=>" { FATARROW } - | "bool" { BOOL } - | "true" { TRUE } - | "false" { FALSE } - | "bool-elim" { BOOL_ELIM } | "at" { AT } | "fst" { FST } | "snd" { SND } | "type" { TYPE } + | "bool" { BOOL } + | "true" { TRUE } + | "false" { FALSE } + | "bool-elim" { BOOL_ELIM } | ident { IDENT (Lexing.lexeme lexbuf) } | eof { EOF } diff --git a/lib/Parser.mly b/lib/Parser.mly index 5c587b2..d0395ac 100644 --- a/lib/Parser.mly +++ b/lib/Parser.mly @@ -12,7 +12,7 @@ open Ast %token EOF %right ARROW ASTERISK -%left IDENT LPR APP BACKSLASH FST SND BOOL TRUE FALSE BOOL_ELIM +%left IDENT LPR APP BACKSLASH FST SND TYPE BOOL TRUE FALSE BOOL_ELIM %start <Ast.expr> parse @@ -35,15 +35,6 @@ raw_expr: { Var name } | LPR; e = raw_expr; RPR { e } - | BOOL - { Bool } - | TRUE - { True } - | FALSE - { False } - | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr; - LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR - { BoolElim { motive_var; motive_body; true_case; false_case; scrut } } | a = arg; ARROW; b = expr { Pi (a, b) } @@ -64,6 +55,16 @@ raw_expr: | TYPE { Type } + | BOOL + { Bool } + | TRUE + { True } + | FALSE + { False } + | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr; + LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR + { BoolElim { motive_var; motive_body; true_case; false_case; scrut } } + %inline expr: e = locate(raw_expr) { e } diff --git a/lib/Syntax.ml b/lib/Syntax.ml new file mode 100644 index 0000000..6cd988a --- /dev/null +++ b/lib/Syntax.ml @@ -0,0 +1,19 @@ +type tm = + | Var of int + | Pi of tm * (* BINDS *) tm + | Lam of (* BINDS *) tm + | App of tm * tm + | Sg of tm * (* BINDS *) tm + | Pair of tm * tm + | Fst of tm + | Snd of tm + | Type + | Bool + | True + | False + | BoolElim of { + motive : (* BINDS *) tm; + true_case : tm; + false_case : tm; + scrut : tm; + } |