summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoopsMatchCtxs.mli
diff options
context:
space:
mode:
authorSon Ho2024-02-13 00:31:39 +0100
committerSon Ho2024-03-08 16:53:29 +0100
commit7733752dd8c153c48263609087794f5199ef37d2 (patch)
treecafce4bf7c2ba9991224936bb230dbe6c4fae4c9 /compiler/InterpreterLoopsMatchCtxs.mli
parentc7b4286af6f1668308c166906479de851d722466 (diff)
Fix some issues with the loops
Diffstat (limited to 'compiler/InterpreterLoopsMatchCtxs.mli')
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.mli15
1 files changed, 15 insertions, 0 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 5f69b8d3..d6f89ed6 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -137,6 +137,21 @@ val match_ctxs :
*)
val ctxs_are_equivalent : ids_sets -> eval_ctx -> eval_ctx -> bool
+(** Reorganize a target context so that we can match it with a source context
+ (remember that the source context is generally the fixed point context,
+ which results from joins during which we ended the loans which
+ were introduced during the loop iterations).
+
+ **Parameters**:
+ - [config]
+ - [loop_id]
+ - [fixed_ids]
+ - [src_ctx]
+
+ *)
+val prepare_match_ctx_with_target :
+ config -> LoopId.id -> ids_sets -> eval_ctx -> cm_fun
+
(** Match a context with a target context.
This is used to compute application of loop translations: we use this