1 files changed, 115 insertions, 0 deletions
diff --git a/compiler/InterpreterProjectors.mli b/compiler/InterpreterProjectors.mli
new file mode 100644
index 00000000..a6d8bd5c
--- /dev/null
+++ b/compiler/InterpreterProjectors.mli
@@ -0,0 +1,115 @@
+module T = Types
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+open InterpreterBorrowsCore
+
+(** Auxiliary function.
+
+    Apply a proj_borrows on a shared borrow.
+    Note that when projecting over shared values, we generate
+    {!V.abstract_shared_borrows}, not {!V.avalue}s.
+*)
+val apply_proj_loans_on_symbolic_expansion :
+  T.RegionId.Set.t -> V.symbolic_expansion -> T.rty -> V.typed_avalue
+
+(** Convert a symbolic expansion *which is not a borrow* to a value *)
+val symbolic_expansion_non_borrow_to_value :
+  V.symbolic_value -> V.symbolic_expansion -> V.typed_value
+
+(** Convert a symbolic expansion *which is not a shared borrow* to a value.
+
+    If the expansion is a mutable reference expansion, it converts it to a borrow.
+    This function is meant to be used when reducing projectors over borrows,
+    during a symbolic expansion.
+  *)
+val symbolic_expansion_non_shared_borrow_to_value :
+  V.symbolic_value -> V.symbolic_expansion -> V.typed_value
+
+(** Auxiliary function to prepare reborrowing operations (used when
+    applying projectors).
+
+    Returns two functions:
+    - a function to generate fresh re-borrow ids, and register the reborrows
+    - a function to apply the reborrows in a context
+    Those functions are of course stateful.
+
+    Parameters:
+    - [config]
+    - [allow_reborrows]
+ *)
+val prepare_reborrows :
+  C.config ->
+  bool ->
+  (V.BorrowId.id -> V.BorrowId.id) * (C.eval_ctx -> C.eval_ctx)
+
+(** Apply (and reduce) a projector over borrows to a value.
+
+    Parameters:
+    - [check_symbolic_no_ended]: controls whether we check or not whether
+      symbolic values don't contain already ended regions.
+      This check is activated when applying projectors upon calling a function
+      (because we need to check that function arguments don't contain ⊥),
+      but deactivated when expanding symbolic values:
+      {[
+        fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
+
+        let p = f(&mut x, &mut y); // p -> @s0
+        assert(x == ...); // end 'a
+        let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
+      ]}
+    - [ctx]
+
+    - [fresh_reborrow]: a function which generates fresh ids for reborrows, and
+      registers the reborrows (to be applied later to the context).
+
+      When applying projections on shared values, we need to apply
+      reborrows. This is a bit annoying because, with the way we compute
+      the projection on borrows, we can't update the context immediately.
+      Instead, we remember the list of borrows we have to insert in the
+      context *afterwards*.
+
+      See {!prepare_reborrows}
+
+    - [regions]: the regions to project
+    - [ancestor_regions]
+    - [v]: the value on which to apply the projection
+
+    - [ty]: the projection type (is used to map borrows to regions, or in other
+      words to interpret the borrows as belonging to some regions). Remember that
+      [v] doesn't contain region information.
+      For instance, if we have:
+      [v <: ty] where:
+      - [v = mut_borrow l ...]
+      - [ty = Ref (r, ...)]
+      then we interpret the borrow [l] as belonging to region [r]
+*)
+val apply_proj_borrows :
+  bool ->
+  C.eval_ctx ->
+  (V.BorrowId.id -> V.BorrowId.id) ->
+  T.RegionId.Set.t ->
+  T.RegionId.Set.t ->
+  V.typed_value ->
+  T.rty ->
+  V.typed_avalue
+
+(** Parameters:
+    - [config]
+    - [ctx]
+    - [regions]: the regions to project
+    - [ancestors_regions]
+    - [v]: the value on which to apply the projection
+    - [ty]: the type (with regions) to use for the projection
+
+ *)
+val apply_proj_borrows_on_input_value :
+  C.config ->
+  C.eval_ctx ->
+  T.RegionId.Set.t ->
+  T.RegionId.Set.t ->
+  V.typed_value ->
+  T.rty ->
+  C.eval_ctx * V.typed_avalue