diff options
| -rw-r--r-- | src/Assumed.ml | 5 | ||||
| -rw-r--r-- | src/PureUtils.ml | 2 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 12 | ||||
| -rw-r--r-- | src/Translate.ml | 32 | ||||
| -rw-r--r-- | src/main.ml | 2 |
5 files changed, 24 insertions, 29 deletions
diff --git a/src/Assumed.ml b/src/Assumed.ml index 8ce518c9..2cd83db5 100644 --- a/src/Assumed.ml +++ b/src/Assumed.ml @@ -232,8 +232,7 @@ type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name (** The list of assumed functions and all their information: - their signature - - a boolean indicating whether they are monadic or not (i.e., if they - can fail or not) + - a boolean indicating whether the function can fail or not - their name Rk.: following what is written above, we don't include `Box::free`. @@ -282,6 +281,6 @@ let get_assumed_name (id : A.assumed_fun_id) : fun_name = let _, _, _, name = get_assumed_info id in name -let assumed_is_monadic (id : A.assumed_fun_id) : bool = +let assumed_can_fail (id : A.assumed_fun_id) : bool = let _, _, b, _ = get_assumed_info id in b diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 7d298f13..032d65d0 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -485,7 +485,7 @@ let get_fun_effect_info (use_state : bool) (fun_id : A.fun_id) { can_fail = true; input_state; output_state } | A.Assumed aid -> { - can_fail = Assumed.assumed_is_monadic aid; + can_fail = Assumed.assumed_can_fail aid; input_state = false; output_state = false; } diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 01cc37eb..a9bf0a9d 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -38,11 +38,9 @@ type config = { Note that we later filter the useless *forward* calls in the micro-passes, where it is more natural to do. *) - use_state_monad : bool; - (** If `true`, use a state-error monad. - If `false`, only use an error monad. - - Using a state-error monad is necessary when modelling I/O, for instance. + use_state : bool; + (** Controls whether we need to use a state to model the external world + (I/O, for instance). *) } @@ -477,7 +475,7 @@ let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : (** Small utility. *) let get_fun_effect_info (config : config) (fun_id : A.fun_id) (gid : T.RegionGroupId.id option) : fun_effect_info = - PureUtils.get_fun_effect_info config.use_state_monad fun_id gid + PureUtils.get_fun_effect_info config.use_state fun_id gid (** Translate a function signature. @@ -1081,7 +1079,7 @@ and translate_return (config : config) (opt_v : V.typed_value option) * - error-monad: Return x * - state-error: Return (state, x) * *) - if config.use_state_monad then + if config.use_state then let state_var = { id = ctx.state_var; diff --git a/src/Translate.ml b/src/Translate.ml index d5505894..2390dd69 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -15,11 +15,9 @@ let log = TranslateCore.log type config = { eval_config : Contexts.partial_config; mp_config : Micro.config; - use_state_monad : bool; - (** If `true`, use a state-error monad. - If `false`, only use an error monad. - - Using a state-error monad is necessary when modelling I/O, for instance. + use_state : bool; + (** Controls whether we need to use a state to model the external world + (I/O, for instance). *) split_files : bool; (** Controls whether we split the generated definitions between different @@ -98,7 +96,7 @@ let translate_function_to_symbolics (config : C.partial_config) TODO: maybe we should introduce a record for this. *) let translate_function_to_pure (config : C.partial_config) - (mp_config : Micro.config) (use_state_monad : bool) (trans_ctx : trans_ctx) + (mp_config : Micro.config) (use_state : bool) (trans_ctx : trans_ctx) (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t) (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl) : pure_fun_translation = @@ -182,7 +180,7 @@ let translate_function_to_pure (config : C.partial_config) { SymbolicToPure.filter_useless_back_calls = mp_config.filter_useless_monadic_calls; - use_state_monad; + use_state; } in @@ -227,7 +225,7 @@ let translate_function_to_pure (config : C.partial_config) (* We need to ignore the forward inputs, and the state input (if there is) *) let _, backward_inputs = Collections.List.split_at backward_sg.sg.inputs - (num_forward_inputs + if use_state_monad then 1 else 0) + (num_forward_inputs + if use_state then 1 else 0) in (* As we forbid nested borrows, the additional inputs for the backward * functions come from the borrows in the return value of the rust function: @@ -276,7 +274,7 @@ let translate_function_to_pure (config : C.partial_config) (pure_forward, pure_backwards) let translate_module_to_pure (config : C.partial_config) - (mp_config : Micro.config) (use_state_monad : bool) (m : M.llbc_module) : + (mp_config : Micro.config) (use_state : bool) (m : M.llbc_module) : trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list = (* Debug *) log#ldebug (lazy "translate_module_to_pure"); @@ -320,7 +318,7 @@ let translate_module_to_pure (config : C.partial_config) { SymbolicToPure.filter_useless_back_calls = mp_config.filter_useless_monadic_calls; - use_state_monad; + use_state; } in let fun_sigs = @@ -331,8 +329,8 @@ let translate_module_to_pure (config : C.partial_config) (* Translate all the *transparent* functions *) let pure_translations = List.map - (translate_function_to_pure config mp_config use_state_monad trans_ctx - fun_sigs type_decls_map) + (translate_function_to_pure config mp_config use_state trans_ctx fun_sigs + type_decls_map) m.functions in @@ -357,7 +355,7 @@ type gen_ctx = { type gen_config = { mp_config : Micro.config; - use_state_monad : bool; + use_state : bool; extract_types : bool; extract_decreases_clauses : bool; extract_template_decreases_clauses : bool; @@ -603,7 +601,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) (* Translate the module to the pure AST *) let trans_ctx, trans_types, trans_funs = translate_module_to_pure config.eval_config config.mp_config - config.use_state_monad m + config.use_state m in (* Initialize the extraction context - for now we extract only to F* *) @@ -715,14 +713,14 @@ let translate_module (filename : string) (dest_dir : string) (config : config) } in - let use_state = config.use_state_monad in + let use_state = config.use_state in (* Extract one or several files, depending on the configuration *) if config.split_files then ( let base_gen_config = { mp_config = config.mp_config; - use_state_monad = use_state; + use_state; extract_types = false; extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = false; @@ -812,7 +810,7 @@ let translate_module (filename : string) (dest_dir : string) (config : config) let gen_config = { mp_config = config.mp_config; - use_state_monad = use_state; + use_state; extract_types = true; extract_decreases_clauses = config.extract_decreases_clauses; extract_template_decreases_clauses = diff --git a/src/main.ml b/src/main.ml index 8afbc0cd..3fb162f3 100644 --- a/src/main.ml +++ b/src/main.ml @@ -188,7 +188,7 @@ let () = test_unit_functions; extract_decreases_clauses = not !no_decreases_clauses; extract_template_decreases_clauses = !template_decreases_clauses; - use_state_monad = not !no_state; + use_state = not !no_state; } in Translate.translate_module filename dest_dir trans_config m |