From 407a2a4a0a440c41adc19fbe8b67283b7b7c65ab Mon Sep 17 00:00:00 2001 From: Malte Voos Date: Mon, 19 Feb 2024 12:57:26 +0100 Subject: core syntax, semantic domain, evaluation --- dune-project | 2 +- flake.nix | 2 +- lib/Ast.ml | 16 ++++++++-------- lib/Domain.ml | 27 +++++++++++++++++++++++++++ lib/Eval.ml | 55 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/Eval.mli | 1 + lib/Lexer.mll | 8 ++++---- lib/Parser.mly | 21 +++++++++++---------- lib/Syntax.ml | 19 +++++++++++++++++++ toytt.opam | 3 +++ 10 files changed, 130 insertions(+), 24 deletions(-) create mode 100644 lib/Domain.ml create mode 100644 lib/Eval.ml create mode 100644 lib/Eval.mli create mode 100644 lib/Syntax.ml diff --git a/dune-project b/dune-project index ede6aa8..61494e3 100644 --- a/dune-project +++ b/dune-project @@ -15,7 +15,7 @@ (name toytt) (synopsis "A short synopsis") (description "A longer description") - (depends ocaml dune ppx_deriving asai) + (depends ocaml dune menhir ppx_deriving algaeff asai bwd) (tags (topics "to describe" your project))) diff --git a/flake.nix b/flake.nix index 6be9e8b..0b8acde 100644 --- a/flake.nix +++ b/flake.nix @@ -24,7 +24,7 @@ (on.listRepo (on.makeOpamRepo ./.)); devPackagesQuery = { ocaml-lsp-server = "*"; - ocamlformat = "*"; + ocp-indent = "*"; }; query = devPackagesQuery // { ocaml-base-compiler = "*"; diff --git a/lib/Ast.ml b/lib/Ast.ml index f7c90dd..d26cc0f 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -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 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; + } diff --git a/toytt.opam b/toytt.opam index 1a4a45c..c2dd3f6 100644 --- a/toytt.opam +++ b/toytt.opam @@ -12,8 +12,11 @@ bug-reports: "https://github.com/username/reponame/issues" depends: [ "ocaml" "dune" {>= "3.13"} + "menhir" "ppx_deriving" + "algaeff" "asai" + "bwd" "odoc" {with-doc} ] build: [ -- cgit 1.4.1