diff options
author | Son HO | 2023-11-22 15:06:43 +0100 |
---|---|---|
committer | GitHub | 2023-11-22 15:06:43 +0100 |
commit | bacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (patch) | |
tree | 9953d7af1fe406cdc750030a43a5e4d6245cd763 /compiler/InterpreterLoopsMatchCtxs.mli | |
parent | 587f1ebc0178acb19029d3fc9a729c197082aba7 (diff) | |
parent | 01cfd899119174ef7c5941c99dd251711f4ee701 (diff) |
Merge pull request #45 from AeneasVerif/son_merge_types
Big cleanup
Diffstat (limited to 'compiler/InterpreterLoopsMatchCtxs.mli')
-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 |