summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/SymbolicToPure.ml26
-rw-r--r--src/Translate.ml18
2 files changed, 12 insertions, 32 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 66f4d608..83c045df 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -101,12 +101,8 @@ type bs_ctx = {
fun_context : fun_context;
fun_decl : A.fun_decl;
bid : T.RegionGroupId.id option; (** TODO: rename *)
- output_ty : ty;
- (** The output type - we use it to translate `Panic`.
-
- This should be the directly translated output type (i.e., no state,
- no result).
- *)
+ sg : fun_sig;
+ (** The function signature - useful in particular to translate `Panic` *)
sv_to_var : var V.SymbolicValueId.Map.t;
(** Whenever we encounter a new symbolic value (introduced because of
a symbolic expansion or upon ending an abstraction, for instance)
@@ -1070,29 +1066,25 @@ let rec translate_expression (config : config) (e : S.expression) (ctx : bs_ctx)
: texpression =
match e with
| S.Return opt_v -> translate_return config opt_v ctx
- | Panic -> translate_panic config ctx
+ | Panic -> translate_panic ctx
| FunCall (call, e) -> translate_function_call config call e ctx
| EndAbstraction (abs, e) -> translate_end_abstraction config abs e ctx
| Expansion (p, sv, exp) -> translate_expansion config p sv exp ctx
| Meta (meta, e) -> translate_meta config meta e ctx
-and translate_panic (config : config) (ctx : bs_ctx) : texpression =
+and translate_panic (ctx : bs_ctx) : texpression =
(* Here we use the function return type - note that it is ok because
* we don't match on panics which happen inside the function body -
* but it won't be true anymore once we translate individual blocks *)
(* If we use a state monad, we need to add a lambda for the state variable *)
(* Note that only forward functions return a state *)
- if config.use_state_monad && ctx.bid <> None then
+ let output_ty = mk_simpl_tuple_ty ctx.sg.doutputs in
+ if ctx.sg.info.output_state then
(* Create the `Fail` value *)
- let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; ctx.output_ty ] in
+ let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
let ret_v = mk_result_fail_texpression ret_ty in
- (* Add the lambda *)
- let _, state_var =
- fresh_var (Some ConstStrings.state_basename) mk_state_ty ctx
- in
- let state_pattern = mk_typed_pattern_from_var state_var None in
- mk_abs state_pattern ret_v
- else mk_result_fail_texpression ctx.output_ty
+ ret_v
+ else mk_result_fail_texpression output_ty
and translate_return (config : config) (opt_v : V.typed_value option)
(ctx : bs_ctx) : texpression =
diff --git a/src/Translate.ml b/src/Translate.ml
index 92261dba..a264a121 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -122,11 +122,6 @@ let translate_function_to_pure (config : C.partial_config)
(* Initialize the context *)
let forward_sig = RegularFunIdMap.find (A.Regular def_id, None) fun_sigs in
- let forward_output_ty =
- match forward_sig.sg.doutputs with
- | [ ty ] -> ty
- | _ -> failwith "Unreachable"
- in
let sv_to_var = V.SymbolicValueId.Map.empty in
let var_counter = Pure.VarId.generator_zero in
let state_var, var_counter = Pure.VarId.fresh var_counter in
@@ -146,7 +141,7 @@ let translate_function_to_pure (config : C.partial_config)
{
SymbolicToPure.bid = None;
(* Dummy for now *)
- output_ty = forward_output_ty;
+ sg = forward_sig.sg;
(* Will need to be updated for the backward functions *)
sv_to_var;
var_counter;
@@ -216,10 +211,7 @@ let translate_function_to_pure (config : C.partial_config)
let backward_sg =
RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
in
- let backward_output_ty = mk_simpl_tuple_ty backward_sg.sg.doutputs in
- let ctx =
- { ctx with bid = Some back_id; output_ty = backward_output_ty }
- in
+ let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in
(* Translate *)
SymbolicToPure.translate_fun_decl sp_config ctx None
@@ -255,10 +247,6 @@ let translate_function_to_pure (config : C.partial_config)
let ctx, backward_outputs =
SymbolicToPure.fresh_vars backward_outputs ctx
in
- let backward_output_tys =
- List.map (fun (v : Pure.var) -> v.ty) backward_outputs
- in
- let backward_output_ty = mk_simpl_tuple_ty backward_output_tys in
let backward_inputs =
T.RegionGroupId.Map.singleton back_id backward_inputs
in
@@ -271,7 +259,7 @@ let translate_function_to_pure (config : C.partial_config)
{
ctx with
bid = Some back_id;
- output_ty = backward_output_ty;
+ sg = backward_sg.sg;
backward_inputs;
backward_outputs;
}