commit 89fa2d5bb5b1e8fb745e6321a4ff9b39e7537592
parent 3642f1d0bec1614bc4fa1e9d6a146e3e784e2c05
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Fri, 15 Dec 2023 13:50:38 -0800
Wip
Diffstat:
| M | abstract.ml | | | 2 | ++ |
| M | common.ml | | | 9 | +++++---- |
| M | core.ml | | | 12 | ++++++++---- |
| M | elab2.ml | | | 94 | ++++++++++++++++++++++++++++++++++++++----------------------------------------- |
| M | eval.ml | | | 110 | ++++++++++++++++++++++++++++++++++++++----------------------------------------- |
| M | parser.mly | | | 9 | +++++++++ |
| M | value.ml | | | 15 | +++------------ |
7 files changed, 125 insertions(+), 126 deletions(-)
diff --git a/abstract.ml b/abstract.ml
@@ -1,5 +1,7 @@
open Common
+(* TODO: Here (and elsewhere) we should be using arrays instead of lists. *)
+
type term =
| Match of term * case list
| Annot of term * term
diff --git a/common.ml b/common.ml
@@ -2,7 +2,8 @@ type ident = string
type index = int
type level = int
-(* Readable helper function for creating closures. *)
-let capture env body = (env, body)
-
-let all = List.fold_left (&&) true
+(* Short-circuiting AND fold_left. *)
+let rec all2 f xs ys = match xs, ys with
+| x :: xs, y :: ys -> f x y && all2 f xs ys
+| [], [] -> true
+| _, _ -> invalid_arg "all2: lists have different length"
diff --git a/core.ml b/core.ml
@@ -1,15 +1,19 @@
open Common
+type intrin =
+| Type
+| NatType
+| NatOpAdd
+
type term =
| Let of term * term
| Case of term * case list
| App of term * term list
-| Fn of fn
-| FnType of fn_type
+| Fn of int * term
+| FnType of int * term list * term
| Nat of Z.t
| Var of index
-and fn = int * term
-and fn_type = int * term list * term
+| Intrin of intrin
and case = patt * term
and patt = patt_discriminant list
and patt_discriminant =
diff --git a/elab2.ml b/elab2.ml
@@ -1,4 +1,5 @@
open Common
+open Eval
module A = Abstract
module C = Core
module V = Value
@@ -10,6 +11,7 @@ type context = {
types: V.value list;
}
+(* Add `x := v : t` to ctx. *)
let bind_def ctx x v t = {
len = 1 + ctx.len;
names = x :: ctx.names;
@@ -17,6 +19,7 @@ let bind_def ctx x v t = {
types = t :: ctx.types;
}
+(* Add `x : t` to ctx. *)
let bind_arb ctx x t = bind_def ctx x (V.Arb ctx.len) t
let rec bind_arb_telescope ctx xs ts = match xs, ts with
@@ -24,29 +27,28 @@ let rec bind_arb_telescope ctx xs ts = match xs, ts with
| [], [] -> ctx
| _, _ -> failwith "impossible"
-let rec quote_telescope l = function
-| t :: ts -> quote l t :: quote_telescope (l + 1) ts
-| [] -> []
-
-let rec check ctx t u = match t, u with
-(* TODO: Match, Fn, Data *)
-| t, u ->
- let (ct, v) = infer ctx t in
- if conv ctx.len u v then ct else failwith "type error"
-
-and infer ctx = function
+let rec infer ctx = function
| A.Match _ -> failwith "no impl: match"
-| A.Annot (a, b) ->
- let cb = check ctx b V.Type in
- let vb = eval ctx.values cb in
- let ca = check ctx a vb in
- (ca, vb)
+| A.Annot (a, t) ->
+ let ct = check ctx t (V.Intrin C.Type) in
+ let vt = eval ctx.values ct in
+ let ca = check ctx a vt in
+ (ca, vt)
| A.App (f, args) ->
let (cf, tf) = infer ctx f in
begin match tf with
- | V.FnType (env, (arity, doms, cod)) ->
+ | V.FnType (env, arity, doms, cod) ->
if List.length args <> arity then failwith "arity mismatch" else
- let (cargs, vcod) = check_app ctx args env doms cod in
+ let rec go env args doms = match args, doms with
+ | arg :: args, dom :: doms ->
+ let vdom = eval env dom in
+ let carg = check ctx arg vdom in
+ let varg = eval ctx.values carg in
+ let (cargs, vcod) = go (varg :: env) args doms in
+ (carg :: cargs, vcod)
+ | [], [] -> ([], eval env cod)
+ | _, _ -> failwith "impossible" in
+ let (cargs, vcod) in go env args doms in
(C.App (cf, cargs), vcod)
| _ -> failwith "expected function type in application"
end
@@ -54,20 +56,27 @@ and infer ctx = function
| A.Index _ -> failwith "no impl: index"
| A.Deref _ -> failwith "no impl: deref"
| A.Fn (ps, body) ->
- let (xs, ts) = infer_patt_telescope ctx ps in
+ let (xs, vdoms) = infer_patt_telescope ctx ps in
let arity = List.length xs in
- let (cbody, u) = infer (bind_arb_telescope ctx xs ts) body in
- let f = C.Fn (arity, cbody) in
- let ft = V.FnType (ctx.values, (arity, quote_telescope ctx.len ts)) in
- (f, ft)
-| A.FnType (doms, cod) ->
- let arity = List.length doms in
- let (xs, cdoms, vdoms) = check_annots ctx doms in
- let ccod = check (bind_arb_telescope ctx xs vdoms) cod V.Type in
- (C.FnType (arity, cdoms, ccod), V.Type)
+ let (cbody, vcod) = infer (bind_arb_telescope ctx xs vdoms) body in
+ let cdoms = quote_telescope ctx.len vdoms in
+ let ccod = quote (ctx.len + arity) vcod in
+ (C.Fn (arity, cbody), V.FnType (ctx.values, arity, cdoms, ccod))
+| A.FnType (anns, cod) ->
+ let arity = List.length anns in
+ let rec go ctx = function
+ | A.Annot (p, dom) :: anns ->
+ let cdom = check ctx dom (V.Intrin C.Type) in
+ let vdom = eval ctx.values cdom in
+ let x = check_patt ctx p vdom in
+ let (cdoms, ccod) = go (bind_arb ctx x vdom) anns in
+ (cdom :: cdoms, ccod)
+ | [] -> check ctx cod (V.Intrin C.Type) in
+ let (cdoms, ccod) = go ctx anns in
+ (C.FnType (arity, cdoms, ccod), V.Intrin C.Type)
| A.Data _ -> failwith "no impl: data"
| A.DataType _ -> failwith "no impl: data type"
-| A.Nat n -> (C.Nat n, V.Nat)
+| A.Nat n -> (C.Nat n, V.Intrin C.NatType)
| A.Ident x ->
let rec go ys vs ts = match ys, vs, ts with
| y :: ys, v :: vs, t :: ts -> if x = y then (v, t) else go ys vs ts
@@ -75,22 +84,18 @@ and infer ctx = function
| _, _, _ -> failwith "impossible" in
go ctx.names ctx.values ctx.types
-and check_app ctx args env doms cod = match args, doms with
-| arg :: args, dom :: doms ->
- let vdom = eval env dom in
- let carg = check ctx arg vdom in
- let varg = eval ctx.values carg in
- let (cargs, vcod) = check_app ctx args (varg :: env) doms cod in
- (carg :: cargs, vcod)
-| [], [] -> ([], eval env cod)
-| _, _ -> failwith "impossible"
+and check ctx a t = match a, t with
+(* TODO: Match, Fn, Data *)
+| a, t ->
+ let (ca, ta) = infer ctx a in
+ if conv ctx.len t ta then ca else failwith "type error"
and infer_patt ctx = function
| A.PWild -> failwith "can not infer type for wild pattern"
| A.PBind _ -> failwith "can not infer type for bind pattern"
| A.PAssign _ -> failwith "no impl: assign pattern"
| A.PAnnot (A.Annot (p, t)) ->
- let ct = check ctx t V.Type in
+ let ct = check ctx t (V.Intrin C.Type) in
let vt = eval ctx.values ct in
let x = check_patt ctx p vt in
(x, vt)
@@ -111,7 +116,7 @@ and check_patt ctx p t = match p with
| A.PBind x -> Some x
| A.PAssign _ -> failwith "no impl: assign pattern"
| A.PAnnot (A.Annot (p, u)) ->
- let cu = check ctx u V.Type in
+ let cu = check ctx u (V.Intrin C.Type) in
let vu = eval ctx.values cu in
if conv ctx.len vu t then
check_patt ctx p t
@@ -129,12 +134,3 @@ and check_patt_telescope ctx ps ts = match ps, ts with
x :: xs
| [], [] -> []
| _, _ -> failwith "impossible"
-
-and check_annots ctx = function
-| Annot (p, t) :: anns ->
- let ct = check ctx t V.Type in
- let vt = eval ctx.values ct in
- let x = check_patt ctx p vt in
- let (xs, cts, vts) = check_annots (bind_arb ctx x vt) anns in
- (x :: xs, ct :: cts, vt :: vts)
-| [] -> ([], [], [])
diff --git a/eval.ml b/eval.ml
@@ -2,81 +2,77 @@ open Common
module C = Core
module V = Value
+(* Extend env with values Arb l, Arb (l+1), ..., Arb (l+n-1). *)
+let weaken env l n =
+ let rec go env i =
+ if i < l + n then go (V.Arb i :: env) (i + 1) else env in
+ go env l
+
let rec eval env = function
-| C.Let (_, t, u) -> eval (eval env t :: env) u
+| C.Let _ -> failwith "no impl: let"
+| C.Case _ -> failwith "no impl: case"
| C.App (f, args) ->
let vargs = List.map (eval env) args in
begin match eval env f with
- | V.Clo (cap, C.Fn (_, body)) -> eval (vargs @ cap) body
- | V.Add ->
+ (* β-reduction *)
+ | V.Fn (cap, _, body) ->
+ eval (List.rev_append vargs cap) body
+ | V.Intrin C.NatOpAdd ->
begin match vargs with
| [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
| _ -> failwith "impossible"
end
+ (* neutral application *)
| vf -> V.App (vf, vargs)
end
-| C.Fn _ as t -> V.Clo (env, t)
-| C.FnType _ as t -> V.Clo (env, t)
+| C.Fn (arity, body) -> V.Fn (env, arity, body)
+| C.FnType (arity, doms, cod) -> V.FnType (env, arity, doms, cod)
| C.Nat n -> V.Nat n
| C.Var i -> List.nth env i
+| C.Intrin a -> V.Intrin a
+(* TODO: quote of eval normalizes terms; in some cases below, we probabaly
+ * don't need to eval before quoting *)
let rec quote l = function
+| V.Case _ -> failwith "no impl: case"
| V.App (f, args) -> C.App (quote l f, List.map (quote l) args)
-| V.Clo (env, C.Fn (xs, body)) -> C.Fn
-| V.Nat of Z.t
-| V.Var of level
-| V.Type
-| V.Nat
-| V.Add
+| V.Fn (env, arity, body) ->
+ let vbody = eval (weaken env l arity) body in
+ C.Fn (arity, quote (l + arity) vbody)
+| V.FnType (env, arity, doms, cod) ->
+ let rec go l env = function
+ | dom :: doms ->
+ let cdom = quote l (eval env dom) in
+ let (cdoms, ccod) = go (l + 1) (V.Arb l :: env) doms in
+ (cdom :: cdoms, ccod)
+ | [] -> ([], quote l (eval env cod)) in
+ C.FnType (arity, cdoms, ccod)
+| V.Nat n -> C.Nat n
+| V.Arb i -> C.Var (l - i - 1)
+| V.Intrin a -> C.Intrin a
+
+let rec quote_telescope l = function
+| t :: ts -> quote l t :: quote_telescope (l + 1) ts
+| [] -> []
let rec conv l a b = match a, b with
+(* TODO: η-equality? *)
+(* TODO: Case *)
| V.App (af, aargs), V.App (bf, bargs) ->
- conv l af bf && all (List.map2 (conv l) aargs bargs)
-| V.Clo (e)
+ conv l af bf && all2 (conv l) aargs bargs
+| V.Fn (aenv, arity, abody), V.Fn (benv, _, bbody) ->
+ let vabody = eval (weaken aenv l arity) abody in
+ let vbbody = eval (weaken benv l arity) bbody in
+ conv (l + arity) vabody vbbody
+| V.FnType (aenv, arity, adoms, acod), V.FnType (benv, _, bdoms, bcod) ->
+ let rec go l aenv adoms benv bdoms = match adoms, bdoms with
+ | adom :: adoms, bdom :: bdoms ->
+ conv l (eval aenv adom) (eval benv bdom)
+ && go (l + 1) (V.Arb l :: aenv) adoms (V.Arb l :: benv) bdoms
+ | [], [] -> conv l (eval aenv acod) (eval benv bcod)
+ | _, _ -> failwith "impossible" in
+ go l aenv adoms benv bdoms
| V.Nat n, V.Nat m -> Z.equal n m
| V.Arb i, V.Arb j -> i = j
-| V.Type, V.Type -> true
-| V.Nat, V.Nat -> true
-| V.Add, V.Add -> true
-| _, _ -> false
-
-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
-
-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
+| V.Intrin a, V.Intrin b -> a = b
| _, _ -> false
diff --git a/parser.mly b/parser.mly
@@ -25,6 +25,15 @@ open Concrete
%%
+(* Syntax idea for mutual recursion:
+ * Anonymous functions (no recursion support):
+ * fn x -> ...
+ * Named functions ((mutual) recursion support)):
+ * f := func x -> ...;
+ * g := func y -> ...;
+ * (Think of ":= func" as being one symbol).
+ * We can make a similar distinction for types with "ty" vs "type". *)
+
expr0: (* Sequencing *)
| expr1 COLON_EQ expr1 SEMICOLON expr0 { Let ($1, $3, $5) }
| expr1 SEMICOLON expr0 { Seq ($1, $3) }
diff --git a/value.ml b/value.ml
@@ -4,18 +4,9 @@ module C = Core
type value =
| Case of value * environ * C.case list
| App of value * value list
-| Fn of environ * C.fn
-| FnType of environ * C.fn_type
+| Fn of environ * int * C.term
+| FnType of environ * int * C.term list * C.term
| Nat of Z.t
| Arb of level
-| Type
-| PtrType
-| PtrOp of ptr_op
-| NatType
-| NatOp of nat_op
+| Intrin of C.intrin
and environ = value list
-and ptr_op =
-| PtrOpRead
-| PtrOpWrite
-and nat_op =
-| NatOpAdd
