From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/InterpreterStatements.mli | 35 ++++++++++++++--------------------- 1 file changed, 14 insertions(+), 21 deletions(-) (limited to 'compiler/InterpreterStatements.mli') diff --git a/compiler/InterpreterStatements.mli b/compiler/InterpreterStatements.mli index e65758ae..d84e8be6 100644 --- a/compiler/InterpreterStatements.mli +++ b/compiler/InterpreterStatements.mli @@ -1,15 +1,8 @@ -module T = Types -module PV = PrimitiveValues -module V = Values -module E = Expressions -module C = Contexts -module Subst = Substitute -module A = LlbcAst -module L = Logging -module Inv = Invariants -module S = SynthesizeSymbolic +open Types +open Values +open Contexts +open LlbcAst open Cps -open InterpreterExpressions (** Pop the current frame. @@ -17,13 +10,13 @@ open InterpreterExpressions dummy variables, after ending the proper borrows of course) but the return variable, move the return value out of the return variable, remove all the local variables (but preserve the abstractions!), remove the - {!constructor:C.env_elem.Frame} indicator delimiting the current frame and + {!constructor:env_elem.Frame} indicator delimiting the current frame and handle the return value to the continuation. If the boolean is false, we don't move the return value, and call the continuation with [None]. *) -val pop_frame : C.config -> bool -> (V.typed_value option -> m_fun) -> m_fun +val pop_frame : config -> bool -> (typed_value option -> m_fun) -> m_fun (** Helper. @@ -44,15 +37,15 @@ val pop_frame : C.config -> bool -> (V.typed_value option -> m_fun) -> m_fun - [ctx] *) val create_push_abstractions_from_abs_region_groups : - (T.RegionGroupId.id -> V.abs_kind) -> - LA.abs_region_group list -> - (T.RegionGroupId.id -> bool) -> - (V.abs -> C.eval_ctx -> C.eval_ctx * V.typed_avalue list) -> - C.eval_ctx -> - C.eval_ctx + (RegionGroupId.id -> abs_kind) -> + abs_region_group list -> + (RegionGroupId.id -> bool) -> + (abs -> eval_ctx -> eval_ctx * typed_avalue list) -> + eval_ctx -> + eval_ctx (** Evaluate a statement *) -val eval_statement : C.config -> LA.statement -> st_cm_fun +val eval_statement : config -> statement -> st_cm_fun (** Evaluate a statement seen as a function body *) -val eval_function_body : C.config -> LA.statement -> st_cm_fun +val eval_function_body : config -> statement -> st_cm_fun -- cgit v1.2.3