diff options
| author | Son HO | 2024-06-04 14:05:44 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-04 14:05:44 +0200 |
| commit | afc4e62ce7a584da0bb0a7350533e321388be545 (patch) | |
| tree | 89f3b6999e1697595f1c3fbb2d9c4d8c60a69e49 /compiler/InterpreterLoopsMatchCtxs.mli | |
| parent | 4a31acdff7a5dfdc26bf25ad25bb8266b790f891 (diff) | |
| parent | 3ad6c4712fd41efec55f29af5ccc31f68a0e12cf (diff) | |
Merge pull request #228 from AeneasVerif/son/loops2
Add support for projection markers when joining environments
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.mli | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli index ab585220..cd807358 100644 --- a/compiler/InterpreterLoopsMatchCtxs.mli +++ b/compiler/InterpreterLoopsMatchCtxs.mli @@ -13,13 +13,11 @@ open InterpreterLoopsCore (** Compute various maps linking the abstractions and the borrows/loans they contain. Parameters: - - [no_duplicates]: checks that borrows/loans are not referenced more than once - (see the documentation for {!type:InterpreterLoopsCore.abs_borrows_loans_maps}). - [explore]: this function is used to filter abstractions. - [env] *) val compute_abs_borrows_loans_maps : - Meta.span -> bool -> (abs -> bool) -> env -> abs_borrows_loans_maps + Meta.span -> (abs -> bool) -> env -> abs_borrows_loans_maps (** Generic functor to implement matching functions between values, environments, etc. @@ -188,7 +186,7 @@ val prepare_match_ctx_with_target : We want to introduce an abstraction [abs@2], which has the same shape as [abs@fp] above (the fixed-point abstraction), and which is actually the identity. If we do so, - we get an environment which is actually also a fixed point (we can collapse + we get an environment which is actually also a fixed point (we can reduce the dummy variables and [abs@1] to actually retrieve the fixed point we computed, and we use the fact that those values and abstractions can't be *directly* manipulated unless we end this newly introduced [abs@2], which we |