diff options
author | Son Ho | 2024-05-24 16:32:59 +0200 |
---|---|---|
committer | Son Ho | 2024-05-24 16:32:59 +0200 |
commit | 321263384bb1e6e8bfd08806f35164bdba387d74 (patch) | |
tree | 04d90b72b7591e380079614a4335e9ca7fe11268 /compiler/InterpreterExpressions.mli | |
parent | 765cb792916c1c69f864a6cf59a49c504ad603a2 (diff) | |
parent | 0baa0519cf477fe1fa447417585960fc811bcae9 (diff) |
Merge branch 'main' into afromher/recursive_projectors
Diffstat (limited to '')
-rw-r--r-- | compiler/InterpreterExpressions.mli | 45 |
1 files changed, 20 insertions, 25 deletions
diff --git a/compiler/InterpreterExpressions.mli b/compiler/InterpreterExpressions.mli index 0fb12180..feb641d1 100644 --- a/compiler/InterpreterExpressions.mli +++ b/compiler/InterpreterExpressions.mli @@ -4,41 +4,28 @@ open Contexts 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 {!InterpreterPaths.update_ctx_along_read_place} first. - *) -val read_place : - Meta.meta -> access_kind -> place -> (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. + Prepare the access to a place in a right-value (typically an operand) by reorganizing + the environment to end outer loans, then read the value and check that this value + *doesn't contain any bottom nor reserved borrows*. 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 : config -> - Meta.meta -> + Meta.span -> bool -> access_kind -> place -> - (typed_value -> m_fun) -> - m_fun + eval_ctx -> + typed_value * eval_ctx * (eval_result -> eval_result) (** Evaluate an operand. @@ -50,11 +37,19 @@ val access_rplace_reorganize_and_read : Use {!eval_operands} instead. *) val eval_operand : - config -> Meta.meta -> operand -> (typed_value -> m_fun) -> m_fun + config -> + Meta.span -> + operand -> + eval_ctx -> + typed_value * eval_ctx * (eval_result -> eval_result) (** Evaluate several operands at once. *) val eval_operands : - config -> Meta.meta -> operand list -> (typed_value list -> m_fun) -> m_fun + config -> + Meta.span -> + operand list -> + eval_ctx -> + typed_value list * eval_ctx * (eval_result -> eval_result) (** Evaluate an rvalue which is not a global (globals are handled elsewhere). @@ -65,10 +60,10 @@ val eval_operands : *) val eval_rvalue_not_global : config -> - Meta.meta -> + Meta.span -> rvalue -> - ((typed_value, eval_error) result -> m_fun) -> - m_fun + eval_ctx -> + (typed_value, eval_error) result * eval_ctx * (eval_result -> eval_result) (** Evaluate a fake read (update the context so that we can read a place) *) -val eval_fake_read : config -> Meta.meta -> place -> cm_fun +val eval_fake_read : config -> Meta.span -> place -> cm_fun |