diff options
| author | Son HO | 2024-05-24 14:16:37 +0200 |
|---|---|---|
| committer | GitHub | 2024-05-24 14:16:37 +0200 |
| commit | c6c9e351546a723e62cc21579b2359dba3bfb56f (patch) | |
| tree | 74ed652b8862d1dde24ccd65b6c29503ea3db35c /compiler/InterpreterProjectors.mli | |
| parent | e669de58b71fd68642cfacf1a2e3cbd1c5b2f4fe (diff) | |
| parent | 69ff150ede10b7d24f9777298e8ca3de163c33e1 (diff) | |
Merge pull request #175 from AeneasVerif/afromher/meta
Rename meta into span
Diffstat (limited to '')
| -rw-r--r-- | compiler/InterpreterProjectors.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli index 17569ac8..43cdc09d 100644 --- a/compiler/InterpreterProjectors.mli +++ b/compiler/InterpreterProjectors.mli @@ -15,7 +15,7 @@ open Contexts [original_sv_ty]: shouldn't have erased regions *) val apply_proj_loans_on_symbolic_expansion : - Meta.meta -> + Meta.span -> RegionId.Set.t -> RegionId.Set.t -> symbolic_expansion -> @@ -24,7 +24,7 @@ val apply_proj_loans_on_symbolic_expansion : (** Convert a symbolic expansion *which is not a borrow* to a value *) val symbolic_expansion_non_borrow_to_value : - Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value + Meta.span -> symbolic_value -> symbolic_expansion -> typed_value (** Convert a symbolic expansion *which is not a shared borrow* to a value. @@ -33,7 +33,7 @@ val symbolic_expansion_non_borrow_to_value : during a symbolic expansion. *) val symbolic_expansion_non_shared_borrow_to_value : - Meta.meta -> symbolic_value -> symbolic_expansion -> typed_value + Meta.span -> symbolic_value -> symbolic_expansion -> typed_value (** Auxiliary function to prepare reborrowing operations (used when applying projectors). @@ -49,7 +49,7 @@ val symbolic_expansion_non_shared_borrow_to_value : *) val prepare_reborrows : config -> - Meta.meta -> + Meta.span -> bool -> (BorrowId.id -> BorrowId.id) * (eval_ctx -> eval_ctx) @@ -104,7 +104,7 @@ val prepare_reborrows : then we interpret the borrow [l] as belonging to region [r] *) val apply_proj_borrows : - Meta.meta -> + Meta.span -> bool -> eval_ctx -> (BorrowId.id -> BorrowId.id) -> @@ -125,7 +125,7 @@ val apply_proj_borrows : *) val apply_proj_borrows_on_input_value : config -> - Meta.meta -> + Meta.span -> eval_ctx -> RegionId.Set.t -> RegionId.Set.t -> |