commit 8e0a0d1522a4cca7ee6d239085e9e7f05a48d14b
parent 5bb93471b62efc8ce1f7cc6cd9b9e0c10e34c93a
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Wed, 24 Jan 2024 19:45:08 -0800
Dependent pattern matching works! (At least a little.)
Diffstat:
| M | elab.ml | | | 32 | +++++++------------------------- |
| M | error.ml | | | 14 | ++++++++++++-- |
| M | eval.ml | | | 88 | +++++++++++++++++++++++++++++++++++++++---------------------------------------- |
| M | main.ml | | | 4 | ++-- |
| M | quote.ml | | | 26 | -------------------------- |
5 files changed, 64 insertions(+), 100 deletions(-)
diff --git a/elab.ml b/elab.ml
@@ -39,21 +39,6 @@ let add_name'
else
(Name.Var.Set.add name name_set, name)
-(*
-let ensure_distinct'
-: Name.Var.t node array -> Name.Var.t array
-= fun names ->
- let nnames = Array.length names in
- let name_set = ref Name.Var.Set.empty in
- let names' = Array.make nnames garbage in
- for i = 0 to nnames - 1 do
- let {loc; data = name} = names.(i) in
- name_set := add_name' loc !name_set name;
- names'.(i) <- names.(i).data
- done;
- names'
-*)
-
let rec assign_patt
: context -> I.patt -> V.value -> Uniq.uniq -> context
= fun ctx {names; disc} vtyp var ->
@@ -78,15 +63,15 @@ let rec assign_patt
(* Assign each subpattern in type-dependency order, because that's the
* order that check_disc' elaborates subpatterns in. The order matters
* here, because assign_patt binds variables. *)
- let ctx = ref ctx in
+ let ctx' = ref ctx in
for i = 0 to arity - 1 do
let j = order.(i) in
let subtyp = I.disc_type binders.(j).patt.disc in
- let vsubtyp = eval !ctx.env subtyp in
- ctx := assign_patt !ctx subpatts.(j) vsubtyp (Uniq.get subvars j)
+ let vsubtyp = eval ctx.env subtyp in
+ ctx' := assign_patt !ctx' subpatts.(j) vsubtyp (Uniq.get subvars j)
done;
- !ctx
+ !ctx'
(* Elaborate explicits to Some and implicits to None. *)
let elaborate_args'
@@ -429,6 +414,8 @@ and elaborate_match'
: context -> Loc.t -> A.term -> A.case array -> V.value -> I.term
= fun ctx loc scrutinee cases body_vtyp ->
let (scrutinee, scrutinee_vtyp) = infer' ctx scrutinee in
+ let vars = Uniq.fresh 1 in
+ let var = Uniq.get vars 0 in
let ncases = Array.length cases in
let cases' = Array.make ncases garbage in
@@ -438,8 +425,6 @@ and elaborate_match'
let (_, patt) = check_patt'
ctx Name.Var.Set.empty patt scrutinee_vtyp in
- let vars = Uniq.fresh 1 in
- let var = Uniq.get vars 0 in
let ctx = Ctx.bind ctx vars in
let ctx = assign_patt ctx patt scrutinee_vtyp var in
let body = check' ctx body body_vtyp in
@@ -447,9 +432,6 @@ and elaborate_match'
cases'.(i) <- {I.patt; I.body}
done;
- let vars = Uniq.fresh 1 in
- let var = Uniq.get vars 0 in
-
let to_clause
: int -> I.case -> clause
= fun casei case ->
@@ -799,7 +781,7 @@ and check_disc'
let vtyp = eval clo typ in
let (name_set', subpatt') = match subpatts.(j) with
| Some patt -> check_patt' !ctx !name_set patt vtyp
- | None -> no_impl "implict args" in
+ | None -> no_impl "implicit args" in
name_set := name_set';
subpatts'.(j) <- subpatt';
(* XXX: I think this is a quadratic time algorithm. We should
diff --git a/error.ml b/error.ml
@@ -1,6 +1,7 @@
module F = Format
open Node
module I = Internal
+module P = Pretty
type error = error' node
and error' =
@@ -37,7 +38,7 @@ and error' =
(*| ElabExpectedFnType of I.term*)
let rec pp_print ppf {loc; data = e} =
- F.fprintf ppf "[%a] %a"
+ F.fprintf ppf "@[<v>[%a] %a@]"
Loc.pp_print loc
pp_print' e
@@ -69,9 +70,18 @@ and pp_print' ppf = function
(Pretty.pp_print_term 0) typ
| ElabNonInferablePatt ->
F.pp_print_string ppf "non-inferable pattern"
+| ElabUnifyFail (expected, inferred) ->
+ F.fprintf ppf
+ "\
+ expected type@;<0 4>\
+ %a@,\
+ does not unify with inferred type@;<0 4>\
+ %a@,\
+ "
+ (P.pp_print_term 0) expected
+ (P.pp_print_term 0) inferred
(* TODO *)
-| ElabUnifyFail _ -> F.pp_print_string ppf "ErrUnifyFail"
| ElabCantInferData -> F.pp_print_string ppf "ErrCantInferData"
| ElabNoLetAnnot _ -> F.pp_print_string ppf "ErrNoLetAnnot"
| ElabNoBinderAnnot _ -> F.pp_print_string ppf "ErrNoBinderAnnot"
diff --git a/eval.ml b/eval.ml
@@ -6,33 +6,41 @@ module V = Value
* cases? *)
(* TODO: Lazily evaluate args? *)
-(*
let rec define_data_args
: V.environment -> V.value -> I.patt -> V.environment
= fun env value {disc; _} -> match value, disc with
-| value, I.DWild -> env
-| V.Data {tagi = data_tagi; args; _}, I.DData {tagi = disc_tagi; subpatts; _} ->
- begin if data_tagi <> disc_tagi then
- impossible "Eval.define_along_patt: value and disc have different tag"
+| value, I.DWild _ -> env
+| V.Data v, I.DData d ->
+ begin if v.tagi <> d.tagi then
+ impossible "Eval.define_data_args: value and disc have different tag"
end;
+ let tagi = v.tagi in
- let arity = Array.length args in
- begin if arity <> Array.length subpatts then
- impossible "Eval.define_along_patt: value and disc have different arity"
+ begin if Array.length v.args <> Array.length d.subpatts then
+ impossible "Eval.define_data_args: value and disc have different arity"
end;
+ let arity = Array.length v.args in
let subvars = Uniq.fresh arity in
let env = Env.bind env subvars in
let env = ref env in
for i = 0 to arity - 1 do
- env := Env.define !env (Uniq.get subvars i) args.(i);
- env := define_data_args !env args.(i) subpatts.(i)
+ let (_, {I.ctors; _}) = v.datatype_clo in
+ let vorder = ctors.(tagi).order in
+ let dorder = d.datatype.ctors.(tagi).order in
+ begin if vorder.(i) <> dorder.(i) then
+ impossible "Eval.define_data_args: value and disc have different order"
+ end;
+ let j = vorder.(i) in
+
+ let subvar = Uniq.get subvars j in
+ env := Env.define !env subvar v.args.(j);
+ env := define_data_args !env v.args.(j) d.subpatts.(j)
done;
!env
| _, I.DData _ ->
- impossible "Eval.define_along_patt: value is not data, but disc is"
-*)
+ impossible "Eval.define_data_args: value is not data, but disc is"
let rec eval
: V.environment -> I.term -> V.value
@@ -47,33 +55,11 @@ let rec eval
env := Env.define !env (Uniq.get vars i) vrhs
done;
eval !env body
-
| I.Match {scrutinee; cases; switch} ->
- no_impl "eval match"
-(*
- let scrutinee = eval env scrutinee in
- let vars = Uniq.fresh 1 in
- let var = Uniq.get vars 0 in
- let switch_env = Env.bind Env.empty vars in
- let switch_env = Env.define switch_env var scrutinee in
- begin match do_switch switch_env (Index.Of (0, 0)) switch with
- | Some casei ->
- let {I.patt; I.body} = cases.(casei) in
- let vars = Uniq.fresh 1 in
- let env = Env.bind env vars in
- let env = Env.define env (Uniq.get vars 0) scrutinee in
- let env = define_data_args env scrutinee patt in
- eval env body
- | None -> V.Match {scrutinee; clo = env; cases; switch}
- end
-*)
-
+ do_match (eval env scrutinee) (env, cases) switch
| 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; tagi; args; datatype} ->
V.Data {
tag;
@@ -81,23 +67,34 @@ let rec eval
args = Array.map (eval env) args;
datatype_clo = (env, datatype);
}
-
| 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
-(*
+and do_match
+: V.value -> I.case array V.closure -> I.switch -> V.value
+= fun scrutinee (clo, cases) switch ->
+ let vars = Uniq.fresh 1 in
+ let var = Uniq.get vars 0 in
+ let switch_env = Env.bind Env.empty vars in
+ let switch_env = Env.define switch_env var scrutinee in
+ begin match do_switch switch_env (Index.Of (0, 0)) switch with
+ | Some casei ->
+ let {I.patt; I.body} = cases.(casei) in
+ let clo = Env.bind clo vars in
+ let clo = Env.define clo var scrutinee in
+ let clo = define_data_args clo scrutinee patt in
+ eval clo body
+ | None -> V.NeutralMatch {scrutinee; cases_clo = (clo, cases); switch}
+ end
+
and do_switch env ij = function
| Switch {index = ij'; subswitches; _} ->
let var = Env.index env ij in
@@ -116,7 +113,6 @@ and do_switch env ij = function
| None -> impossible "Eval.switch: undefined variable"
end
| Goto casei -> Some casei
-*)
and apply
: V.value -> V.value array -> V.value
@@ -142,14 +138,16 @@ and force
: V.environment -> V.value -> V.value
= fun env -> function
| V.RefClo (env', t) -> force env (eval !env' t)
-| V.NeutralMatch _ -> no_impl "force neutral match"
+| V.NeutralMatch {scrutinee; cases_clo; switch} ->
+ do_match (force env scrutinee) cases_clo switch
(* XXX: There's no reason to force the arguments for "CbNeed redexes" (i.e.,
* when fn is a lambda), but we do need to force args in a "CbValue redex"
* (i.e., when fn is a builtin with builtin reduction rules). *)
-| V.NeutralApp (fn, args) -> apply (force env fn) (Array.map (force env) args)
+| V.NeutralApp (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
+ | None -> V.Arb var
end
| v -> v
diff --git a/main.ml b/main.ml
@@ -2,6 +2,7 @@ open Node
module I = Internal
module V = Value
+(*
let buf = Lexing.from_string "\
N := [A: Type, A, A -> A] -> A;\n\
add: [N, N] -> N := fn m, n => fn A, z, s => m A (n A z s) s;\n\
@@ -10,8 +11,8 @@ let buf = Lexing.from_string "\
five := add two three;\n\
five Nat 0 (fn n => n + 1)\n\
"
+*)
-(*
let buf = Lexing.from_string "\
Bool := #{@false; @true};\n\
T := #(b: Bool, (if b then Nat else Type));\n\
@@ -20,7 +21,6 @@ let buf = Lexing.from_string "\
(@false, _) => 2,\n\
}): Nat\n\
"
-*)
(*
let buf = Lexing.from_string "\
diff --git a/quote.ml b/quote.ml
@@ -3,32 +3,6 @@ open Eval
module I = Internal
module V = Value
-(*
-let rec bind_and_define_subpatts
-: V.environment -> Uniq.uniq -> I.patt -> V.environment
-= fun env var {disc; _} -> match disc with
-| I.DWild -> env
-| I.DData {tag; tagi; subpatts; datatype} ->
- let arity = Array.length subpatts in
- let subvars = Uniq.fresh arity in
- let data = V.Data {
- tag;
- tagi;
- args = Array.init arity (fun i -> V.Arb (Uniq.get subvars i));
- datatype_clo = (env, datatype);
- } in
- let env = Env.bind env subvars in
- let env = Env.define env var data in
-
- let env = ref env in
- for i = 0 to arity - 1 do
- let subvar = Uniq.get subvars i in
- env := bind_and_define_subpatts !env subvar subpatts.(i)
- done;
-
- !env
-*)
-
let rec bind_patt_twice
: V.environment * V.environment -> I.patt -> V.environment * V.environment
= fun (env0, env1) {disc; _} ->
