commit 54b7bd3a98514dfd174af3d9cc56a6951ecd4b31
parent 008e2cfcb987935ecfd7e9ba10446aa38b529807
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Tue, 5 Dec 2023 23:47:08 -0800
Save progress, because I'm about to change a bunch of stuff
Diffstat:
| A | .gitignore | | | 3 | +++ |
| A | common.ml | | | 6 | ++++++ |
| A | core.ml | | | 20 | ++++++++++++++++++++ |
| A | elab.ml | | | 99 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| A | eval.ml | | | 34 | ++++++++++++++++++++++++++++++++++ |
| A | parser.ml | | | 415 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| M | parser.mly | | | 11 | +++++++---- |
| M | surf.ml | | | 8 | ++++---- |
| A | value.ml | | | 12 | ++++++++++++ |
9 files changed, 600 insertions(+), 8 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -0,0 +1,3 @@
+*.cm*
+*.mli
+test
diff --git a/common.ml b/common.ml
@@ -0,0 +1,6 @@
+type ident = string
+type index = int
+type level = int
+
+(* Readable helper function for creating closures. *)
+let capture env body = (env, body)
diff --git a/core.ml b/core.ml
@@ -0,0 +1,20 @@
+open Common
+
+type term =
+| Let of ident * term * term
+| Fn of ident * term
+| Pi of ident * term * term
+| App of term * term
+| Var of index
+| Int of Z.t
+
+(*
+TODO:
+1. copy over elab code
+2. test
+3. add support for constants
+4. add support for ADTs
+5. staging
+6. ...
+7. quantities (0, ω)
+*)
diff --git a/elab.ml b/elab.ml
@@ -0,0 +1,99 @@
+open Common
+module S = Surf
+module C = Core
+module V = Value
+
+type context = {
+ env: V.environ;
+ free: (ident * V.value) list;
+}
+
+let let_bind ctx x t v = {
+ env = v :: ctx.env;
+ free = (x, t) :: ctx.free;
+}
+
+let var_bind ctx x t = let_bind ctx x t (V.Var (List.length ctx.env))
+
+let rec check ctx a t = match a, t with
+| S.Let (p, a, b), t ->
+ let (ca, ta, x) = infer_with_patt ctx a p in
+ let va = eval ctx.env ca in
+ let cb = check (let_bind ctx x ta va) sb t in
+ C.Let (x, ca, cb)
+| S.Fn (p, a), V.Pi (_, dom, cod) ->
+ let x = check_patt ctx p dom in
+ let ca = check (var_bind ctx x dom) a (apply cod (V.Var (List.length ctx.env))) in
+ C.Fn (x, ca)
+| a, t ->
+ let (ca, u) = infer ctx a in
+ if conv (List.length ctx.env) t u then ca else failwith "type error"
+
+and infer ctx a = match a with
+| S.Let (p, a, b) ->
+ let (ca, ta, x) = infer_with_patt ctx a p in
+ let va = eval ctx.env ca in
+ let (cb, tb) = infer (let_bind ctx x ta va) sb in
+ (C.Let (x, ca, cb), tb)
+| S.Fn (p, a) ->
+ let (x, t) = infer_patt ctx p in
+ let (ca, u) = infer (var_bind ctx x t) a in
+ (C.Fn (x, ca), V.Pi ("α", t, capture ctx.env (quote (List.length ctx.env) u)))
+| S.Pi (x, dom, cod) ->
+ let cdom = check ctx dom V.Type in
+ let vdom = eval ctx.env cdom in
+ let ccod = check (var_bind ctx x vdom) cod V.Type in
+ (C.Pi (x, cdom, ccod), V.Type)
+| S.Hint (a, b) ->
+ let cb = check ctx b V.Type in
+ let vb = eval ctx.env cb in
+ let ca = check ctx a vb in
+ (ca, vb)
+| S.Plus (a, b) -> infer ctx (App ())
+ let c0 = check ctx s0 VNat in
+ let c1 = check ctx s1 VNat in
+ (CAdd (c0, c1), VNat)
+
+| SVar x ->
+ let rec go i = function
+ | [] -> failwith ("variable '" ^ x ^ "' out of scope")
+ | (y, v) :: rest -> if x = y then (CVar i, v) else go (i + 1) rest in
+ go 0 ctx.free
+| SType -> (CType, VType)
+| SApp (s0, s1) ->
+ let (c0, t0) = infer ctx s0 in
+ begin match t0 with
+ | VPi (dom, cod) ->
+ let c1 = check ctx s1 dom in
+ (CApp (c0, c1), apply cod (eval ctx.env c1))
+ | _ -> failwith "expected function type in application"
+ end
+| SNat -> (CNat, VType)
+| SLit n -> (CLit n, VNat)
+
+and infer_with_patt ctx a p = match p with
+| S.Annot (p, b) ->
+ let cb = check ctx b V.Type in
+ let vb = eval ctx.env cb in
+ let x = check_patt ctx p vb in
+ let ca = check ctx a vb in
+ (ca, vb, x)
+| S.Wild x -> let (ca, t) = infer ctx a in (ca, t, x)
+
+and check_patt ctx p t = match p with
+| S.Annot (p, a) ->
+ let ca = check ctx a V.Type in
+ let va = eval ctx.env ca in
+ if conv (List.length ctx.env) t va then
+ check_patt ctx p t
+ else
+ failwith "patt_check fail"
+| S.Wild x -> x
+
+and infer_patt ctx p = match p with
+| S.Annot (p, a) ->
+ let ca = check ctx a V.Type in
+ let va = eval ctx.env ca in
+ let x = check_patt ctx p va in
+ (x, va)
+| S.Wild _ -> failwith "can not infer type for wild pattern"
diff --git a/eval.ml b/eval.ml
@@ -0,0 +1,34 @@
+open Common
+module C = Core
+module V = Value
+
+let rec eval env = function
+| C.Let (_, a, b) -> eval (eval env a :: env) b
+| C.Fn (x, body) -> V.Fn (x, capture env body)
+| C.Pi (x, dom, cod) -> V.Pi (x, eval env dom, capture env cod)
+| C.App (f, a) ->
+ begin match eval env f, eval env a with
+ | V.Fn (_, fclo), va -> apply fclo va
+ | vf, va -> V.App (vf, va)
+ end
+| C.Var i -> List.nth env i
+| C.Int n -> V.Int n
+
+and apply (env, a) v = eval (v :: env) a
+
+let rec quote l = function
+| V.Fn (x, clo) -> C.Fn (x, quote (l + 1) (apply clo (V.Var l)))
+| V.Pi (x, dom, cod) -> C.Pi (x, quote l dom, quote (l + 1) (apply cod (V.Var l)))
+| V.App (f, a) -> C.App (quote l f, quote l a)
+| V.Var k -> C.Var (l - k - 1)
+| V.Int z -> C.Int z
+
+let rec conv l a b = match a, b with
+(* no η for fn *)
+| V.Fn (_, aclo), V.Fn(_, bclo) -> conv (l + 1) (apply aclo (V.Var l)) (apply bclo (V.Var l))
+| V.Pi (_, dom0, cod0), V.Pi (_, dom1, cod1) -> conv l dom0 dom1
+ && conv (l + 1) (apply cod0 (V.Var l)) (apply cod1 (V.Var l))
+| V.App (a0, a1), V.App (b0, b1) -> conv l a0 b0 && conv l a1 b1
+| V.Var x, V.Var y -> x = y
+| V.Int n, V.Int m -> Z.equal n m
+| _, _ -> false
diff --git a/parser.ml b/parser.ml
@@ -0,0 +1,415 @@
+type token =
+ | EOF
+ | COLON
+ | EQ
+ | SEMICOLON
+ | SINGLE_ARROW
+ | DOUBLE_ARROW
+ | AT_LPAREN
+ | HASH_LPAREN
+ | LPAREN
+ | RPAREN
+ | LBRACK
+ | RBRACK
+ | LBRACE
+ | RBRACE
+ | PLUS
+ | ASTERISK
+ | LET
+ | IF
+ | THEN
+ | ELSE
+ | IDENT of (
+# 16 "parser.mly"
+ Surf.ident
+# 26 "parser.ml"
+)
+ | INT of (
+# 17 "parser.mly"
+ Z.t
+# 31 "parser.ml"
+)
+
+open Parsing
+let _ = parse_error;;
+# 2 "parser.mly"
+open Surf
+# 38 "parser.ml"
+let yytransl_const = [|
+ 0 (* EOF *);
+ 257 (* COLON *);
+ 258 (* EQ *);
+ 259 (* SEMICOLON *);
+ 260 (* SINGLE_ARROW *);
+ 261 (* DOUBLE_ARROW *);
+ 262 (* AT_LPAREN *);
+ 263 (* HASH_LPAREN *);
+ 264 (* LPAREN *);
+ 265 (* RPAREN *);
+ 266 (* LBRACK *);
+ 267 (* RBRACK *);
+ 268 (* LBRACE *);
+ 269 (* RBRACE *);
+ 270 (* PLUS *);
+ 271 (* ASTERISK *);
+ 272 (* LET *);
+ 273 (* IF *);
+ 274 (* THEN *);
+ 275 (* ELSE *);
+ 0|]
+
+let yytransl_block = [|
+ 276 (* IDENT *);
+ 277 (* INT *);
+ 0|]
+
+let yylhs = "\255\255\
+\001\000\001\000\001\000\003\000\003\000\003\000\004\000\004\000\
+\004\000\005\000\005\000\006\000\006\000\007\000\007\000\008\000\
+\008\000\008\000\002\000\002\000\009\000\009\000\000\000"
+
+let yylen = "\002\000\
+\006\000\006\000\001\000\005\000\003\000\001\000\007\000\005\000\
+\001\000\003\000\001\000\003\000\001\000\002\000\001\000\001\000\
+\001\000\003\000\003\000\001\000\001\000\003\000\002\000"
+
+let yydefred = "\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\016\000\
+\017\000\023\000\003\000\000\000\000\000\000\000\000\000\015\000\
+\000\000\021\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\014\000\000\000\000\000\000\000\
+\000\000\000\000\018\000\000\000\000\000\005\000\000\000\000\000\
+\022\000\000\000\019\000\000\000\000\000\000\000\000\000\004\000\
+\000\000\008\000\000\000\000\000\000\000\001\000\002\000\007\000"
+
+let yydgoto = "\002\000\
+\010\000\019\000\011\000\012\000\013\000\014\000\015\000\016\000\
+\020\000"
+
+let yysindex = "\006\000\
+\005\255\000\000\254\254\036\255\005\255\254\254\031\255\000\000\
+\000\000\000\000\000\000\009\255\000\255\012\255\252\254\000\000\
+\254\254\000\000\006\255\032\255\052\255\023\255\045\255\056\255\
+\037\255\031\255\252\254\252\254\000\000\054\255\060\255\031\255\
+\031\255\061\255\000\000\031\255\031\255\000\000\012\255\252\254\
+\000\000\031\255\000\000\057\255\039\255\066\255\051\255\000\000\
+\067\255\000\000\005\255\031\255\039\255\000\000\000\000\000\000"
+
+let yyrindex = "\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\009\000\045\000\023\000\001\000\000\000\
+\000\000\000\000\000\000\027\255\053\255\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\042\000\020\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000"
+
+let yygindex = "\000\000\
+\253\255\002\000\254\255\252\255\000\000\048\000\044\000\244\255\
+\000\000"
+
+let yytablesize = 320
+let yytable = "\022\000\
+\013\000\023\000\029\000\005\000\025\000\017\000\001\000\024\000\
+\006\000\026\000\003\000\004\000\005\000\027\000\031\000\008\000\
+\009\000\018\000\030\000\012\000\006\000\007\000\011\000\038\000\
+\008\000\009\000\028\000\029\000\020\000\043\000\044\000\034\000\
+\032\000\046\000\047\000\020\000\003\000\004\000\005\000\048\000\
+\050\000\010\000\004\000\005\000\009\000\004\000\005\000\054\000\
+\056\000\055\000\008\000\009\000\033\000\035\000\037\000\021\000\
+\009\000\036\000\008\000\009\000\016\000\016\000\041\000\042\000\
+\045\000\049\000\016\000\016\000\051\000\052\000\053\000\040\000\
+\016\000\016\000\039\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\
+\000\000\013\000\013\000\013\000\000\000\000\000\000\000\000\000\
+\000\000\013\000\006\000\006\000\000\000\000\000\013\000\013\000\
+\000\000\006\000\013\000\013\000\012\000\012\000\012\000\011\000\
+\011\000\011\000\006\000\006\000\012\000\000\000\000\000\011\000\
+\000\000\012\000\012\000\000\000\011\000\012\000\012\000\000\000\
+\011\000\011\000\010\000\010\000\010\000\009\000\009\000\009\000\
+\000\000\000\000\010\000\000\000\000\000\009\000\000\000\010\000\
+\000\000\000\000\000\000\010\000\010\000\000\000\009\000\009\000"
+
+let yycheck = "\004\000\
+\000\000\005\000\015\000\008\001\007\000\008\001\001\000\006\000\
+\000\000\001\001\006\001\007\001\008\001\014\001\009\001\020\001\
+\021\001\020\001\017\000\000\000\016\001\017\001\000\000\026\000\
+\020\001\021\001\015\001\040\000\002\001\032\000\033\000\009\001\
+\001\001\036\000\037\000\009\001\006\001\007\001\008\001\042\000\
+\045\000\000\000\007\001\008\001\000\000\007\001\008\001\051\000\
+\053\000\052\000\020\001\021\001\001\001\009\001\018\001\020\001\
+\021\001\002\001\020\001\021\001\008\001\009\001\009\001\004\001\
+\004\001\009\001\014\001\015\001\003\001\019\001\004\001\028\000\
+\020\001\021\001\027\000\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\
+\255\255\001\001\002\001\003\001\255\255\255\255\255\255\255\255\
+\255\255\009\001\002\001\003\001\255\255\255\255\014\001\015\001\
+\255\255\009\001\018\001\019\001\001\001\002\001\003\001\001\001\
+\002\001\003\001\018\001\019\001\009\001\255\255\255\255\009\001\
+\255\255\014\001\015\001\255\255\014\001\018\001\019\001\255\255\
+\018\001\019\001\001\001\002\001\003\001\001\001\002\001\003\001\
+\255\255\255\255\009\001\255\255\255\255\009\001\255\255\014\001\
+\255\255\255\255\255\255\018\001\019\001\255\255\018\001\019\001"
+
+let yynames_const = "\
+ EOF\000\
+ COLON\000\
+ EQ\000\
+ SEMICOLON\000\
+ SINGLE_ARROW\000\
+ DOUBLE_ARROW\000\
+ AT_LPAREN\000\
+ HASH_LPAREN\000\
+ LPAREN\000\
+ RPAREN\000\
+ LBRACK\000\
+ RBRACK\000\
+ LBRACE\000\
+ RBRACE\000\
+ PLUS\000\
+ ASTERISK\000\
+ LET\000\
+ IF\000\
+ THEN\000\
+ ELSE\000\
+ "
+
+let yynames_block = "\
+ IDENT\000\
+ INT\000\
+ "
+
+let yyact = [|
+ (fun _ -> failwith "parser")
+; (fun __caml_parser_env ->
+ let _2 = (Parsing.peek_val __caml_parser_env 4 : 'patt0) in
+ let _4 = (Parsing.peek_val __caml_parser_env 2 : 'expr1) in
+ let _6 = (Parsing.peek_val __caml_parser_env 0 : Surf.expr) in
+ Obj.repr(
+# 25 "parser.mly"
+ ( Let (_2, _4, _6) )
+# 234 "parser.ml"
+ : Surf.expr))
+; (fun __caml_parser_env ->
+ let _2 = (Parsing.peek_val __caml_parser_env 4 : 'expr1) in
+ let _4 = (Parsing.peek_val __caml_parser_env 2 : 'expr1) in
+ let _6 = (Parsing.peek_val __caml_parser_env 0 : 'expr1) in
+ Obj.repr(
+# 26 "parser.mly"
+ ( If (_2, _4, _6) )
+# 243 "parser.ml"
+ : Surf.expr))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'expr1) in
+ Obj.repr(
+# 27 "parser.mly"
+ ( _1 )
+# 250 "parser.ml"
+ : Surf.expr))
+; (fun __caml_parser_env ->
+ let _2 = (Parsing.peek_val __caml_parser_env 3 : 'patt0) in
+ let _5 = (Parsing.peek_val __caml_parser_env 0 : 'expr1) in
+ Obj.repr(
+# 29 "parser.mly"
+ ( Fn (_2, _5) )
+# 258 "parser.ml"
+ : 'expr1))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 2 : 'expr2) in
+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'expr1) in
+ Obj.repr(
+# 30 "parser.mly"
+ ( Hint (_1, _3) )
+# 266 "parser.ml"
+ : 'expr1))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'expr2) in
+ Obj.repr(
+# 31 "parser.mly"
+ ( _1 )
+# 273 "parser.ml"
+ : 'expr1))
+; (fun __caml_parser_env ->
+ let _2 = (Parsing.peek_val __caml_parser_env 5 : Surf.ident) in
+ let _4 = (Parsing.peek_val __caml_parser_env 3 : 'expr1) in
+ let _7 = (Parsing.peek_val __caml_parser_env 0 : 'expr2) in
+ Obj.repr(
+# 33 "parser.mly"
+ ( Pi (Some _2, _4, _7) )
+# 282 "parser.ml"
+ : 'expr2))
+; (fun __caml_parser_env ->
+ let _2 = (Parsing.peek_val __caml_parser_env 3 : 'expr2) in
+ let _5 = (Parsing.peek_val __caml_parser_env 0 : 'expr2) in
+ Obj.repr(
+# 34 "parser.mly"
+ ( Pi (None, _2, _5) )
+# 290 "parser.ml"
+ : 'expr2))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'expr3) in
+ Obj.repr(
+# 35 "parser.mly"
+ ( _1 )
+# 297 "parser.ml"
+ : 'expr2))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 2 : 'expr3) in
+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'expr4) in
+ Obj.repr(
+# 37 "parser.mly"
+ ( Plus (_1, _3) )
+# 305 "parser.ml"
+ : 'expr3))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'expr4) in
+ Obj.repr(
+# 38 "parser.mly"
+ ( _1 )
+# 312 "parser.ml"
+ : 'expr3))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 2 : 'expr4) in
+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'expr5) in
+ Obj.repr(
+# 40 "parser.mly"
+ ( Asterisk (_1, _3) )
+# 320 "parser.ml"
+ : 'expr4))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'expr5) in
+ Obj.repr(
+# 41 "parser.mly"
+ ( _1 )
+# 327 "parser.ml"
+ : 'expr4))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 1 : 'expr5) in
+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'expr6) in
+ Obj.repr(
+# 43 "parser.mly"
+ ( Apposition (_1, _2) )
+# 335 "parser.ml"
+ : 'expr5))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'expr6) in
+ Obj.repr(
+# 44 "parser.mly"
+ ( _1 )
+# 342 "parser.ml"
+ : 'expr5))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : Surf.ident) in
+ Obj.repr(
+# 46 "parser.mly"
+ ( Var _1 )
+# 349 "parser.ml"
+ : 'expr6))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : Z.t) in
+ Obj.repr(
+# 47 "parser.mly"
+ ( Int _1 )
+# 356 "parser.ml"
+ : 'expr6))
+; (fun __caml_parser_env ->
+ let _2 = (Parsing.peek_val __caml_parser_env 1 : Surf.expr) in
+ Obj.repr(
+# 48 "parser.mly"
+ ( _2 )
+# 363 "parser.ml"
+ : 'expr6))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 2 : 'patt1) in
+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'expr1) in
+ Obj.repr(
+# 51 "parser.mly"
+ ( Annot (_1, _3) )
+# 371 "parser.ml"
+ : 'patt0))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'patt1) in
+ Obj.repr(
+# 52 "parser.mly"
+ ( _1 )
+# 378 "parser.ml"
+ : 'patt0))
+; (fun __caml_parser_env ->
+ let _1 = (Parsing.peek_val __caml_parser_env 0 : Surf.ident) in
+ Obj.repr(
+# 54 "parser.mly"
+ ( Wild _1 )
+# 385 "parser.ml"
+ : 'patt1))
+; (fun __caml_parser_env ->
+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'patt0) in
+ Obj.repr(
+# 55 "parser.mly"
+ ( _2 )
+# 392 "parser.ml"
+ : 'patt1))
+(* Entry expr0 *)
+; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))
+|]
+let yytables =
+ { Parsing.actions=yyact;
+ Parsing.transl_const=yytransl_const;
+ Parsing.transl_block=yytransl_block;
+ Parsing.lhs=yylhs;
+ Parsing.len=yylen;
+ Parsing.defred=yydefred;
+ Parsing.dgoto=yydgoto;
+ Parsing.sindex=yysindex;
+ Parsing.rindex=yyrindex;
+ Parsing.gindex=yygindex;
+ Parsing.tablesize=yytablesize;
+ Parsing.table=yytable;
+ Parsing.check=yycheck;
+ Parsing.error_function=parse_error;
+ Parsing.names_const=yynames_const;
+ Parsing.names_block=yynames_block }
+let expr0 (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =
+ (Parsing.yyparse yytables 1 lexfun lexbuf : Surf.expr)
+;;
diff --git a/parser.mly b/parser.mly
@@ -27,19 +27,22 @@ expr0:
| expr1 { $1 }
expr1:
| AT_LPAREN patt0 RPAREN SINGLE_ARROW expr1 { Fn ($2, $5) }
- | HASH_LPAREN patt0 RPAREN SINGLE_ARROW expr1 { Pi ($2, $5) }
| expr2 COLON expr1 { Hint ($1, $3) }
| expr2 { $1 }
expr2:
- | expr2 PLUS expr3 { Plus ($1, $3) }
+ | HASH_LPAREN IDENT COLON expr1 RPAREN SINGLE_ARROW expr2 { Pi (Some $2, $4, $7) }
+ | HASH_LPAREN expr2 RPAREN SINGLE_ARROW expr2 { Pi (None, $2, $5) }
| expr3 { $1 }
expr3:
- | expr3 ASTERISK expr4 { Asterisk ($1, $3) }
+ | expr3 PLUS expr4 { Plus ($1, $3) }
| expr4 { $1 }
expr4:
- | expr4 expr5 { Apply ($1, $2) }
+ | expr4 ASTERISK expr5 { Asterisk ($1, $3) }
| expr5 { $1 }
expr5:
+ | expr5 expr6 { Apposition ($1, $2) }
+ | expr6 { $1 }
+expr6:
| IDENT { Var $1 }
| INT { Int $1 }
| LPAREN expr0 RPAREN { $2 }
diff --git a/surf.ml b/surf.ml
@@ -1,14 +1,14 @@
-type ident = string
+open Common
type expr =
| Let of patt * expr * expr
| If of expr * expr * expr
| Fn of patt * expr
-| Pi of patt * expr
+| Pi of ident * expr * expr
| Hint of expr * expr
| Plus of expr * expr
| Asterisk of expr * expr
-| Apply of expr * expr
+| Apposition of expr * expr
| Var of ident
| Int of Z.t
and patt =
@@ -26,7 +26,7 @@ let rec string_of_expr m e =
| Hint (a, b) -> (1, se 2 a ^ " : " ^ se 1 b)
| Plus (a, b) -> (2, se 2 a ^ " + " ^ se 3 b)
| Asterisk (a, b) -> (3, se 3 a ^ " * " ^ se 4 b)
- | Apply (a, b) -> (4, se 4 a ^ " " ^ se 5 b)
+ | Apposition (a, b) -> (4, se 4 a ^ " " ^ se 5 b)
| Var x -> (5, x)
| Int z -> (5, Z.to_string z) in
if c < m then "(" ^ s ^ ")" else s
diff --git a/value.ml b/value.ml
@@ -0,0 +1,12 @@
+open Common
+
+type value =
+| Type
+| Fn of ident * closure
+| Pi of ident * value * closure
+| App of value * value
+| Var of level (* TODO: rename this to "generic" or something? *)
+| Nat
+| Int of Z.t
+and closure = environ * Core.term
+and environ = value list
