summaryrefslogtreecommitdiff
path: root/compiler/InterpreterLoopsMatchCtxs.mli
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/InterpreterLoopsMatchCtxs.mli31
1 files changed, 12 insertions, 19 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli
index 20b997ce..bf29af79 100644
--- a/compiler/InterpreterLoopsMatchCtxs.mli
+++ b/compiler/InterpreterLoopsMatchCtxs.mli
@@ -4,15 +4,8 @@
to check if two contexts are equivalent (modulo conversion).
*)
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module A = LlbcAst
-module Inv = Invariants
-module S = SynthesizeSymbolic
+open Values
+open Contexts
open Cps
open InterpreterUtils
open InterpreterLoopsCore
@@ -26,7 +19,7 @@ open InterpreterLoopsCore
- [env]
*)
val compute_abs_borrows_loans_maps :
- bool -> (V.abs -> bool) -> C.env -> abs_borrows_loans_maps
+ bool -> (abs -> bool) -> env -> abs_borrows_loans_maps
(** Generic functor to implement matching functions between values, environments,
etc.
@@ -100,10 +93,10 @@ module MakeCheckEquivMatcher : functor (_ : MatchCheckEquivState) ->
val match_ctxs :
bool ->
ids_sets ->
- (V.loan_id -> V.typed_value) ->
- (V.loan_id -> V.typed_value) ->
- C.eval_ctx ->
- C.eval_ctx ->
+ (loan_id -> typed_value) ->
+ (loan_id -> typed_value) ->
+ eval_ctx ->
+ eval_ctx ->
ids_maps option
(** Compute whether two contexts are equivalent modulo an identifier substitution.
@@ -142,7 +135,7 @@ val match_ctxs :
- [ctx0]
- [ctx1]
*)
-val ctxs_are_equivalent : ids_sets -> C.eval_ctx -> C.eval_ctx -> bool
+val ctxs_are_equivalent : ids_sets -> eval_ctx -> eval_ctx -> bool
(** Match a context with a target context.
@@ -291,11 +284,11 @@ val ctxs_are_equivalent : ids_sets -> C.eval_ctx -> C.eval_ctx -> bool
- [src_ctx]
*)
val match_ctx_with_target :
- C.config ->
- V.loop_id ->
+ config ->
+ loop_id ->
bool ->
borrow_loan_corresp ->
- V.symbolic_value_id list ->
+ symbolic_value_id list ->
ids_sets ->
- C.eval_ctx ->
+ eval_ctx ->
st_cm_fun