1 files changed, 105 insertions, 0 deletions
diff --git a/compiler/InterpreterPaths.mli b/compiler/InterpreterPaths.mli
new file mode 100644
index 00000000..ed00b7c5
--- /dev/null
+++ b/compiler/InterpreterPaths.mli
@@ -0,0 +1,105 @@
+module T = Types
+module V = Values
+module E = Expressions
+module C = Contexts
+module Subst = Substitute
+module L = Logging
+open Cps
+open InterpreterExpansion
+module Synth = SynthesizeSymbolic
+
+type access_kind = Read | Write | Move
+
+(** Update the environment to be able to read a place.
+
+    When reading a place, we may be stuck along the way because some value
+    is borrowed, we reach a symbolic value, etc. This function repeatedly
+    updates the environment (by ending borrows, expanding symbolic values, etc.)
+    until it manages to fully access the provided place.
+ *)
+val update_ctx_along_read_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Update the environment to be able to write to a place.
+
+    See {!update_ctx_along_read_place}.
+*)
+val update_ctx_along_write_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Read the value at a given place.
+
+    Note that we only access the value at the place, and do not check that
+    the value is "well-formed" (for instance that it doesn't contain bottoms).
+ *)
+val read_place :
+  C.config -> access_kind -> E.place -> C.eval_ctx -> V.typed_value
+
+(** Update the value at a given place.
+
+    This function is an auxiliary function and is not safe: it will not check if
+    the overwritten value contains borrows, loans, etc. and will simply
+    overwrite it.
+ *)
+val write_place :
+  C.config ->
+  access_kind ->
+  E.place ->
+  V.typed_value ->
+  C.eval_ctx ->
+  C.eval_ctx
+
+(** Compute an expanded tuple ⊥ value.
+
+    [compute_expanded_bottom_tuple_value [ty0, ..., tyn]] returns
+    [(⊥:ty0, ..., ⊥:tyn)]
+ *)
+val compute_expanded_bottom_tuple_value : T.ety list -> V.typed_value
+
+(** Compute an expanded ADT ⊥ value *)
+val compute_expanded_bottom_adt_value :
+  T.type_decl T.TypeDeclId.Map.t ->
+  T.TypeDeclId.id ->
+  T.VariantId.id option ->
+  T.erased_region list ->
+  T.ety list ->
+  V.typed_value
+
+(** Compute an expanded [Option] ⊥ value *)
+val compute_expanded_bottom_option_value :
+  T.VariantId.id -> T.ety -> V.typed_value
+
+(** Drop (end) outer loans at a given place, which should be seen as an l-value
+    (we will write to it later, but need to drop the loans before writing).
+
+    This is used to drop values when evaluating the drop statement or before
+    writing to a place.
+
+    Note that we don't do what is defined in the formalization: we move the
+    value to a temporary dummy value, then explore this value and end the outer
+    loans which are inside as long as we find some, then move the resulting
+    value back to where it was. This shouldn't make any difference, really (note
+    that the place is *inside* a borrow, if we end the borrow, we won't be able
+    to reinsert the value back).
+ *)
+val drop_outer_loans_at_lplace : C.config -> E.place -> cm_fun
+
+(** End the loans at a given place: read the value, if it contains a loan,
+    end this loan, repeat.
+
+    This is used when reading or borrowing values. We typically
+    first call {!update_ctx_along_read_place} or {!update_ctx_along_write_place}
+    to get access to the value, then call this function to "prepare" the value:
+    when moving values, we can't move a value which contains loans and thus need
+    to end them, etc.
+ *)
+val end_loans_at_place : C.config -> access_kind -> E.place -> cm_fun
+
+(** Small utility.
+
+    Prepare a place which is to be used as the destination of an assignment:
+    update the environment along the paths, end the outer loans at this place, etc.
+
+    Return the updated context and the (updated) value at the end of the
+    place. This value should not contain any outer loan (and we check it is the
+    case). Note that this value is very likely to contain ⊥ subvalues.
+  *)
+val prepare_lplace : C.config -> E.place -> (V.typed_value -> m_fun) -> m_fun