Update `switch` to have a specific treatment of ADTs

1 files changed, 39 insertions, 1 deletions

diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli
index c610e939..2ea3c6df 100644
--- a/compiler/InterpreterExpressions.mli
+++ b/compiler/InterpreterExpressions.mli
@@ -11,6 +11,41 @@ module S = SynthesizeSymbolic
 open Cps
 open InterpreterPaths
 
+(** Read a place (CPS-style function).
+
+    We also check that the value *doesn't contain bottoms or reserved
+    borrows*.
+
+    This function doesn't reorganize the context to make sure we can read
+    the place. If needs be, you should call {!update_ctx_along_read_place} first.
+ *)
+val read_place :
+  C.config -> access_kind -> E.place -> (V.typed_value -> m_fun) -> m_fun
+
+(** Auxiliary function.
+
+    Prepare the access to a place in a right-value (typically an operand) by
+    reorganizing the environment.
+
+    We reorganize the environment so that:
+    - we can access the place (we prepare *along* the path)
+    - the value at the place itself doesn't contain loans (the [access_kind]
+      controls whether we only end mutable loans, or also shared loans).
+
+    We also check, after the reorganization, that the value at the place
+    *doesn't contain any bottom nor reserved borrows*.
+
+    [expand_prim_copy]: if [true], expand the symbolic values which are
+    primitively copyable and contain borrows.
+ *)
+val access_rplace_reorganize_and_read :
+  C.config ->
+  bool ->
+  access_kind ->
+  E.place ->
+  (V.typed_value -> m_fun) ->
+  m_fun
+
 (** Evaluate an operand.
 
     Reorganize the context, then evaluate the operand.
@@ -26,9 +61,12 @@ val eval_operand : C.config -> E.operand -> (V.typed_value -> m_fun) -> m_fun
 val eval_operands :
   C.config -> E.operand list -> (V.typed_value list -> m_fun) -> m_fun
 
-(** Evaluate an rvalue which is not a global.
+(** Evaluate an rvalue which is not a global (globals are handled elsewhere).
 
     Transmits the computed rvalue to the received continuation.
+
+    Note that this function fails on {!E.Discriminant}: discriminant reads should
+    have been eliminated from the AST.
  *)
 val eval_rvalue_not_global :
   C.config -> E.rvalue -> ((V.typed_value, eval_error) result -> m_fun) -> m_fun