diff options
Diffstat (limited to 'compiler/InterpreterExpressions.mli')
-rw-r--r-- | compiler/InterpreterExpressions.mli | 40 |
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 |