commit 5377553a6de6ea89292b8f5ea8199d249ee25e9d
parent 0f8ed905de3ec4f365268a8b523933f55945185c
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Mon, 8 Jan 2024 23:09:47 -0800
Get (mutual) recursion working
Diffstat:
| M | ctx.ml | | | 71 | +++++++---------------------------------------------------------------- |
| M | desugar.ml | | | 2 | +- |
| M | elab.ml | | | 85 | +++++++++++++++++++++++++++++++++++++++++++++++++++---------------------------- |
| M | env.ml | | | 3 | --- |
| M | eval.ml | | | 36 | +++++++++++++++++++----------------- |
| M | main.ml | | | 18 | +++++++++++------- |
| M | value.ml | | | 2 | +- |
7 files changed, 94 insertions(+), 123 deletions(-)
diff --git a/ctx.ml b/ctx.ml
@@ -11,18 +11,14 @@ type 'a assignment = {
type 'a context = {
assignments: 'a assignment tsil Name.Map.t; (* XXX: tsil! Yuck! *)
- bindings: Index.UniqTsil.t;
- definitions: 'a Uniq.Map.t;
+ env: 'a Env.environment;
}
let empty = {
assignments = Name.Map.empty;
- bindings = Index.UniqTsil.lin;
- definitions = Uniq.Map.empty;
+ env = Env.empty;
}
-let to_env {bindings; definitions; _} = {Env.bindings; Env.definitions}
-
let assign ctx names typ value =
let asn = {typ; value; active = true} in
let shadow ctx name =
@@ -33,11 +29,9 @@ let assign ctx names typ value =
{ctx with assignments} in
(Array.fold_left shadow ctx names, asn)
-let bind ctx vars =
- {ctx with bindings = Index.UniqTsil.snoc ctx.bindings vars}
+let bind ctx vars = {ctx with env = Env.bind ctx.env vars}
-let define ctx var value =
- {ctx with definitions = Uniq.Map.add var value ctx.definitions}
+let define ctx var value = {ctx with env = Env.define ctx.env var value}
let lookup ctx name i =
match Name.Map.find_opt name ctx.assignments with
@@ -50,59 +44,8 @@ let lookup ctx name i =
go i t
| None -> None
-let index ctx ij = Index.UniqTsil.var_of ctx.bindings ij
-
-let quote ctx var = Index.UniqTsil.index_of ctx.bindings var
-
-let eval ctx var = Uniq.Map.find_opt var ctx.definitions
-
-
-
-
-
-
-
-(*
-type 'a assignee = {
- names: Name.t array;
- typ: 'a;
-}
-*)
-
-(*
-let extend_and_bind_one ctx preb =
- let (ctx, vars) = extend_fresh ctx 1 in
- let (ctx, postb) = bind_one ctx preb vars.(0) in
- (ctx, postb)
-
-let extend_and_bind_all ctx prebs =
- let n = Array.length prebs in
- let postbs = Array.make n garbage in
- let (ctx, vars) = extend_fresh ctx n in
- let ctx = ref ctx in
- for i = 0 to n - 1 do
- let (ctx', postb) = bind_one !ctx prebs.(i) vars.(i) in
- ctx := ctx';
- postbs.(i) <- postb
- done;
- (!ctx, postbs)
-*)
+let index ctx ij = Env.index ctx.env ij
-(*
-let extend_fresh ctx n =
- let vars = Uniq.fresh_array n in
- (extend ctx vars, vars)
-*)
+let quote ctx var = Env.quote ctx.env var
-(*
-let bind_one ctx {names; vtyp} var =
- let postb = {var; vtyp; active = true} in
- let ctx = ref ctx in
- for i = 0 to Array.length names - 1 do
- let shadow = function
- | None -> Some (Snoc (Lin, postb))
- | Some l -> Some (Snoc (l, postb)) in
- ctx := {!ctx with names = Name.Map.update names.(i) shadow !ctx.names}
- done;
- (!ctx, postb)
-*)
+let eval ctx var = Env.eval ctx.env var
diff --git a/desugar.ml b/desugar.ml
@@ -64,7 +64,7 @@ and term' loc = function
and definer d = Node.map definer' d
and definer' = function
| C.Definer (lhs, rhs) -> {recursive = false; lhs = patt lhs; rhs = term rhs}
-| C.RecDefiner (lhs, rhs) -> {recursive = false; lhs = patt lhs; rhs = term rhs}
+| C.RecDefiner (lhs, rhs) -> {recursive = true; lhs = patt lhs; rhs = term rhs}
and case c = Node.map case' c
and case' (C.Case (p, t)) = A.Case (patt p, term t)
diff --git a/elab.ml b/elab.ml
@@ -25,6 +25,26 @@ and error' =
| ErrFnPlicityMismatch
| ErrUnexpectedCtor of Tag.t
+let rec string_of_error {loc; data = e} =
+ Loc.to_string loc ^ " " ^ string_of_error' e
+and string_of_error' = function
+| ErrNonInferablePatt _ -> "ErrNonInferablePatt"
+| ErrCantInferData -> "ErrCantInferData"
+| ErrNoLetAnnot _ -> "ErrNoLetAnnot"
+| ErrNoBinderAnnot _ -> "ErrNoBinderAnnot"
+| ErrUnannotImplicitIsType _ -> "ErrUnannotImplicitIsType"
+| ErrApplyNonFunction _ -> "ErrApplyNonFunction"
+| ErrUnifyFail _ -> "ErrUnifyFail"
+| ErrDataPattRefutable -> "ErrDataPattRefutable"
+| ErrBinderCycle _ -> "ErrBinderCycle"
+| ErrArityMismatch -> "ErrArityMismatch"
+| ErrUnboundVar _ -> "ErrUnboundVar"
+| ErrExpectedFnType _ -> "ErrExpectedFnType"
+| ErrExpectedDataType _ -> "ErrExpectedDataType"
+| ErrFnArityMismatch -> "ErrFnArityMismatch"
+| ErrFnPlicityMismatch -> "ErrFnPlicityMismatch"
+| ErrUnexpectedCtor _ -> "ErrUnexpectedCtor"
+
exception Exn of error
let abort e = raise (Exn e)
@@ -39,7 +59,7 @@ exception BlockedOnFuture of Uniq.t * int * Name.t
let rec infer ctx t =
try Ok (infer' ctx t) with
| Exn e -> Error e
-and infer' ctx {loc; data = t} = match t with
+and infer' (ctx: 'a Ctx.context) {loc; data = t} = match t with
| A.Let (definers, body) ->
let (ctx, definers) = infer_definers' ctx definers in
let (body, vtyp) = infer' ctx body in
@@ -49,13 +69,13 @@ and infer' ctx {loc; data = t} = match t with
| A.Annot (t, a) ->
let a = check' ctx a V.Type in
- let va = eval (Ctx.to_env ctx) a in
+ let va = eval ctx.env a in
let t = check' ctx t va in
(t, va)
| A.App (fn, explicit_args) ->
let (fn, va) = infer' ctx fn in
- begin match force (Ctx.to_env ctx) va with
+ begin match force ctx.env va with
| V.FnTypeClosure (clo, {binders; codomain}) ->
let (args, clo) = check_args' ctx loc explicit_args clo binders in
let vcodomain = eval clo codomain in
@@ -66,9 +86,9 @@ and infer' ctx {loc; data = t} = match t with
| A.Fn (params, body) ->
let (ctx', binders) = infer_binders' ctx loc params in
let (body, vcodomain) = infer' ctx' body in
- let codomain = quote (Ctx.to_env ctx') vcodomain in
+ let codomain = quote ctx'.env vcodomain in
let fn = I.Fn {binders; body; codomain} in
- let vfntype = V.FnTypeClosure (Ctx.to_env ctx, {binders; codomain}) in
+ let vfntype = V.FnTypeClosure (ctx.env, {binders; codomain}) in
(fn, vfntype)
| A.FnType (domains, codomain) ->
@@ -87,7 +107,7 @@ and infer' ctx {loc; data = t} = match t with
| A.Var (name, i) ->
begin match Ctx.lookup ctx name i with
| Some {typ = V.Future (id, j); _} -> raise (BlockedOnFuture (id, j, name))
- | Some {typ; value; _} -> (quote (Ctx.to_env ctx) value, typ)
+ | Some {typ; value; _} -> (quote ctx.env value, typ)
| None -> abort (loc @$ ErrUnboundVar (name, i))
end
@@ -96,7 +116,7 @@ and infer' ctx {loc; data = t} = match t with
and check ctx t vtyp =
try Ok (check' ctx t vtyp) with
| Exn e -> Error e
-and check' ctx ({loc; data = t} as node) vtyp = match t, force (Ctx.to_env ctx) vtyp with
+and check' ctx ({loc; data = t} as node) vtyp = match t, force ctx.env vtyp with
| A.Let (definers, body), vtyp ->
let (ctx, definers) = infer_definers' ctx definers in
let body = check' ctx body vtyp in
@@ -133,7 +153,7 @@ and check' ctx ({loc; data = t} as node) vtyp = match t, force (Ctx.to_env ctx)
let plicity = param.plicity in
let vtyp = eval clo domain.typ in
- let typ = quote (Ctx.to_env !ctx) vtyp in
+ let typ = quote !ctx.env vtyp in
let names = check_irrefutable_patt' !ctx param.patt vtyp in
(* Assign the names in ctx. The other params may refer to them. *)
@@ -143,7 +163,7 @@ and check' ctx ({loc; data = t} as node) vtyp = match t, force (Ctx.to_env ctx)
done;
let vcodomain = eval clo codomain in
- let codomain = quote (Ctx.to_env !ctx) vcodomain in
+ let codomain = quote !ctx.env vcodomain in
let body = check' !ctx body vcodomain in
I.Fn {binders = {binders = params'; order}; body; codomain}
@@ -163,7 +183,7 @@ and check' ctx ({loc; data = t} as node) vtyp = match t, force (Ctx.to_env ctx)
| (A.Annot _ | A.App _ | A.FnType _ | A.DataType _ | A.Nat _ | A.Var _ | A.Type), vexpected ->
let (t, vinferred) = infer' ctx node in
- if conv (Ctx.to_env ctx) vexpected vinferred then
+ if conv ctx.env vexpected vinferred then
t
else
abort (loc @$ ErrUnifyFail (vexpected, vinferred))
@@ -207,7 +227,7 @@ and check_args' ctx loc explicit_args clo {binders; order} =
let (arg, varg) = match args.(j) with
| Some arg ->
let arg = check' ctx arg vtyp in
- let varg = eval (Ctx.to_env ctx) arg in
+ let varg = eval ctx.env arg in
(arg, varg)
| None -> no_impl "implict args" in
args'.(j) <- arg;
@@ -248,9 +268,11 @@ and infer_definers' ctx definers =
let names = check_irrefutable_patt' ctx lhs vtyp in
(names, rhs, vtyp)
| Error e -> abort e in
- let typ = quote (Ctx.to_env ctx) vtyp in
+ let typ = quote ctx.env vtyp in
+ (* XXX: vrhs doesn't need to be a Rec. We could eagerly evaluate it, or
+ * add some other mechanism for laziness (like glued eval). *)
+ let vrhs = V.Rec {env = ref ctx.env; rhs} in
let (ctx, _) = Ctx.assign ctx names vtyp (V.Arb vars.(0)) in
- let vrhs = lazy_eval (Ctx.to_env ctx) rhs in
let ctx = Ctx.define ctx vars.(0) vrhs in
(ctx, [|{rhs; typ}|])
@@ -261,7 +283,7 @@ and infer_definers' ctx definers =
* to avoid meta-variables/unification, because they're unpredictable;
* inference should only rely on local information. *)
| definers ->
- (* Infer each definer (in the original context, because definitions are
+ (* Infer each lhs (in the original context, because definitions are
* not allowed to have mutually dependent types), and make all
* assignments. We later set the active flag to false on assignments
* for non-recusive definers, so that the rhs of non-recursive definers
@@ -277,16 +299,18 @@ and infer_definers' ctx definers =
let ctx = !ctx_with_asns in
(* Check each rhs with the appropriate assignments active, but not any
- * definitions. This avoids any non-terminating mutual recursion during
- * elaboration. It also means that each definition is "opaque" during
- * the elaboration of each rhs, i.e., the let-bound variables behave
- * like fn-bound variables. *)
- let ctx_with_defs = ref ctx in
+ * definitions. This means that each definition is "opaque" during the
+ * elaboration of each rhs, i.e., the let-bound variables behave like
+ * fn-bound variables. It's hard to get around this. It might be useful
+ * to elaborate each rhs with every other rhs defined in context, but
+ * that would require every rhs to already be elaborated! *)
+ let env = ref ctx.env in
let definers' = Array.make ndefiners garbage in
for i = 0 to ndefiners - 1 do
- let rhs = definers.(i).data.rhs in
let vtyp = asns.(i).typ in
+ let typ = quote ctx.env vtyp in
+ let rhs = definers.(i).data.rhs in
let rhs =
if definers.(i).data.recursive then
check' ctx rhs vtyp
@@ -298,15 +322,16 @@ and infer_definers' ctx definers =
asns.(i).active <- true;
rhs
end in
+ let vrhs = V.Rec {env; rhs} in
- let vrhs = lazy_eval (Ctx.to_env ctx) rhs in
- ctx_with_defs := Ctx.define !ctx_with_defs vars.(i) vrhs;
-
- let typ = quote (Ctx.to_env ctx) vtyp in
+ env := Env.define !env vars.(i) vrhs;
definers'.(i) <- {I.rhs; I.typ}
done;
- (!ctx_with_defs, definers')
+ (* TODO: For this situation, it might be nice to abstract the surface
+ * name assignment map from contexts. Then we can say a context is an
+ * environment + a surface name assignment. *)
+ ({ctx with env = !env}, definers')
and infer_lhs' ctx {loc; data = {lhs; _}} =
match infer_irrefutable_patt ctx lhs with
@@ -443,7 +468,7 @@ and infer_binders' ctx loc binders =
for i = 0 to arity - 1 do
match states.(i) with
| Elaborated j ->
- let typ = quote (Ctx.to_env ctx) asns.(i).typ in
+ let typ = quote ctx.env asns.(i).typ in
binders'.(i) <- {I.plicity = binders.(i).data.plicity; I.typ};
order.(j) <- i
| Pending _ ->
@@ -455,7 +480,7 @@ and infer_binders' ctx loc binders =
and infer_binder' ctx {loc; data = {plicity; patt; typ}} = match typ with
| Some a ->
let a = check' ctx a V.Type in
- let va = eval (Ctx.to_env ctx) a in
+ let va = eval ctx.env a in
let _ = check_irrefutable_patt' ctx patt va in
va
| None ->
@@ -482,7 +507,7 @@ and infer_irrefutable_patt' ctx ({loc; data = patt} as node) = match patt with
| A.PBind _ -> abort (loc @$ ErrNonInferablePatt node)
| A.PAnnot (patt, typ) ->
let typ = check' ctx typ V.Type in
- let vtyp = eval (Ctx.to_env ctx) typ in
+ let vtyp = eval ctx.env typ in
let names = check_irrefutable_patt' ctx patt vtyp in
(names, vtyp)
| A.PData _ -> abort (loc @$ ErrDataPattRefutable)
@@ -495,8 +520,8 @@ and check_irrefutable_patt' ctx {loc; data = patt} vtyp = match patt with
| A.PBind name -> [|name|]
| A.PAnnot (patt, typ') ->
let typ' = check' ctx typ' V.Type in
- let vtyp' = eval (Ctx.to_env ctx) typ' in
- if conv (Ctx.to_env ctx) vtyp vtyp' then
+ let vtyp' = eval ctx.env typ' in
+ if conv ctx.env vtyp vtyp' then
check_irrefutable_patt' ctx patt vtyp
else
abort (loc @$ ErrUnifyFail (vtyp, vtyp'))
diff --git a/env.ml b/env.ml
@@ -1,8 +1,5 @@
open Global
-(* TODO: Smarter use modules to avoid redundancy between Env and Ctx. Or just
- * store an env on each ctx instead of duplicating fields. *)
-
type 'a environment = {
bindings: Index.UniqTsil.t;
definitions: 'a Uniq.Map.t;
diff --git a/eval.ml b/eval.ml
@@ -9,40 +9,42 @@ module V = Value
let rec eval env = function
| I.Let (definers, body) ->
let ndefiners = Array.length definers in
+
let vars = Uniq.fresh ndefiners in
let env = Env.bind env vars in
- let env' = ref env in
+
+ let env = ref env in
for i = 0 to ndefiners - 1 do
- (* In typical programs, most definitions will not appear inside a type
- * and hence won't be tested for conversion. Thus, it's important that
- * we only lazily evaluate each rhs. *)
- let vrhs = lazy_eval env definers.(i).rhs in
- env' := Env.define !env' vars.(i) vrhs
+ let vrhs = V.Rec {env; rhs = definers.(i).rhs} in
+ env := Env.define !env vars.(i) vrhs
done;
- eval !env' body
+ eval !env body
+
| I.App (fn, args) -> apply (eval env fn) (Array.map (eval env) args)
+
| I.Fn fn -> V.FnClosure (env, fn)
+
| I.FnType fntype -> V.FnTypeClosure (env, fntype)
+
| I.Data (tag, args) -> V.Data (tag, Array.map (eval env) args)
+
| I.DataType datatype -> V.DataTypeClosure (env, datatype)
+
| I.Nat n -> V.Nat n
+
| I.Var ij ->
let var = Env.index env ij in
begin match Env.eval env var with
| Some v -> v
| None -> Arb var
end
+
| I.Type -> V.Type
-| I.Builtin b -> V.Builtin b
-(* TODO: Optimization: Change `Lazy of value lazy` to `Lazy of env * term`,
- * so that when later forcing/reevaluating a lazy value, we can just change the
- * "values" field of the environment (but not the "indices" field, because that
- * is sensitive to term structure) and call eval. *)
-and lazy_eval env t = V.Lazy (lazy (eval env t))
+| I.Builtin b -> V.Builtin b
and apply fn args = match fn, args with
-| V.Lazy fn, args -> V.Lazy (lazy (apply (Lazy.force fn) args))
+| V.Rec {env; rhs}, args -> apply (eval !env rhs) args
| V.FnClosure (clo, {binders = {binders; _}; body; _}), args ->
let arity = Array.length binders in
let vars = Uniq.fresh arity in
@@ -57,16 +59,17 @@ and apply fn args = match fn, args with
* stuck variables to the outside of neutral terms so we can force them without
* needing to recurse. *)
and force env = function
+| V.Rec {env = env'; rhs} -> force env (eval !env' rhs)
| V.App (fn, args) -> apply (force env fn) (Array.map (force env) args)
| V.Arb var ->
begin match Env.eval env var with
| Some v -> force env v
| None -> Arb var
end
-| V.Lazy l -> force env (Lazy.force l)
| v -> v
let rec quote env = function
+| V.Rec {env = env'; rhs} -> quote env (eval !env' rhs)
| V.App (fn, args) -> I.App (quote env fn, Array.map (quote env) args)
| V.FnClosure (clo, {binders; body; codomain}) ->
let (env, clo, binders) = quote_binders env clo binders in
@@ -87,11 +90,10 @@ let rec quote env = function
| V.Arb var ->
begin match Env.quote env var with
| Some ij -> I.Var ij
- | None -> impossible () (* XXX: Is it? *)
+ | None -> impossible ()
end
| V.Type -> I.Type
| V.Builtin b -> I.Builtin b
-| V.Lazy l -> quote env (Lazy.force l)
| V.Future _ -> impossible ()
and quote_binders env clo {binders; order} =
diff --git a/main.ml b/main.ml
@@ -11,8 +11,16 @@ let buf = Lexing.from_string "\
five Nat 0 (fn n => n + 1)\n\
"
*)
+
+(*
+let buf = Lexing.from_string "T := #{@a Nat; @b #()}; @a 3 : T"
+*)
+
let buf = Lexing.from_string "\
-T := #{@a Nat; @b #()}; @a 3 : T"
+ fact: Nat -> Nat := rec fn n =>\n\
+ if eq n 0 then 1 else n * fact (n + 1);\n\
+ fact 3\n\
+"
let concrete =
try Parser.start Lexer.token buf with
@@ -38,16 +46,12 @@ let ctx =
let (ctx, _) = Ctx.assign ctx [|Name.Of "`*"|] nat_op_typ (V.Builtin I.NatOpMul) in
ctx
-(*
let (internal, ty) =
match Elab.infer ctx abstract with
| Ok r -> r
- | Error e -> print_endline "elab error"; exit 1
-*)
-let (internal, ty) = Elab.infer' ctx abstract
+ | Error e -> print_endline (Elab.string_of_error e); exit 1
-let env = Ctx.to_env ctx
-let internal' = Eval.quote env (Eval.eval env internal)
+let internal' = Eval.quote ctx.env (Eval.eval ctx.env internal)
let () = print_endline (I.to_string internal)
let () = print_endline (I.to_string internal')
diff --git a/value.ml b/value.ml
@@ -2,6 +2,7 @@ open Global
module I = Internal
type value =
+| Rec of {env: value Env.environment ref; rhs: I.term}
(*| Switch of ...*)
| App of value * value array
| FnClosure of value Env.environment * I.fn
@@ -13,7 +14,6 @@ type value =
(*| Meta of Uniq.t*)
| Type
| Builtin of I.builtin
-| Lazy of value Lazy.t (* TODO: See comment in eval.ml about optimization. *)
| Future of Uniq.t * int
(*
