summaryrefslogtreecommitdiff
path: root/compiler/Contexts.ml
diff options
context:
space:
mode:
authorSon Ho2024-01-25 11:25:47 +0100
committerSon Ho2024-01-25 11:25:47 +0100
commit8703639a324b9cd398133388a85d8d997d353b9c (patch)
treef46487c9e6daa9290e4d9fb5c5996ead1cac4a5b /compiler/Contexts.ml
parent15a7d7b7322a1cd0ebeb328fde214060e23fa8b4 (diff)
Fix a minor issue when values are moved in the loops
Diffstat (limited to 'compiler/Contexts.ml')
-rw-r--r--compiler/Contexts.ml19
1 files changed, 19 insertions, 0 deletions
diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 5d646a61..b1dd9553 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -153,6 +153,7 @@ and env_elem =
and env = env_elem list
[@@deriving
show,
+ ord,
visitors
{
name = "iter_env";
@@ -170,6 +171,17 @@ and env = env_elem list
concrete = true;
}]
+module OrderedBinder : Collections.OrderedType with type t = binder = struct
+ type t = binder
+
+ let compare x y = compare_binder x y
+ let to_string x = show_binder x
+ let pp_t fmt x = Format.pp_print_string fmt (show_binder x)
+ let show_t x = show_binder x
+end
+
+module BinderMap = Collections.MakeMap (OrderedBinder)
+
type interpreter_mode = ConcreteMode | SymbolicMode [@@deriving show]
type config = {
@@ -394,6 +406,13 @@ let ctx_push_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) (v : typed_value)
: eval_ctx =
{ ctx with env = EBinding (BDummy vid, v) :: ctx.env }
+let ctx_push_fresh_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx =
+ ctx_push_dummy_var ctx (fresh_dummy_var_id ()) v
+
+let ctx_push_fresh_dummy_vars (ctx : eval_ctx) (vl : typed_value list) :
+ eval_ctx =
+ List.fold_left (fun ctx v -> ctx_push_fresh_dummy_var ctx v) ctx vl
+
(** Remove a dummy variable from a context's environment. *)
let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
eval_ctx * typed_value =