commit ef23c70fab3f52ab642184b3dd7fe3c26b9c36e7
parent 54013f815d85edede36ea27876f82d5de84ee46e
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Mon, 13 May 2024 15:58:39 -0700
Stuff
Diffstat:
2 files changed, 8 insertions(+), 0 deletions(-)
diff --git a/elab.ml b/elab.ml
@@ -356,6 +356,8 @@ and infer_definers'
(* Single non-recursive definer. These are handled specially, because
* the type annotation on the lhs is optional. *)
+ (* TODO: Maybe we should make this distinction in internal syntax (maybe
+ * abstract syntax as well). I.e., Let vs LetRec. *)
| [|{loc; data = {recursive = false; lhs; rhs}}|] ->
let (names, rhs, vtyp) =
(* First try to infer from lhs (and check rhs). *)
@@ -390,6 +392,9 @@ and infer_definers'
* assignments. We later set the active flag to false on assignments
* for non-recusive definers, so that the rhs of non-recursive definers
* can not access their own assignment. *)
+ (* TODO: Actually, we should allow definer types to depend on each
+ * other in a well-ordered fashion, because this allows
+ * induction-recursion. *)
let ctx_with_asns = ref ctx in
let name_set = ref Name.Var.Set.empty in
let namess = Array.make ndefiners garbage in
diff --git a/eval.ml b/eval.ml
@@ -95,6 +95,9 @@ and do_match
let clo = Env.bind clo vars in
let clo = Env.define clo var scrutinee in
let clo = define_data_args clo scrutinee patt in
+ (* TODO: "Unify" the scrutinee with the pattern. E.g., if the scrutinee
+ * is a variable, then it gets defined to the "term-version" of the
+ * pattern, which can make some values require further reduction. *)
eval clo body
| None -> V.NeutralMatch {scrutinee; cases_clo = (clo, cases); switch}
end
