diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.mli | 31 |
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 |