diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Pure.ml | 13 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 25 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 3 |
3 files changed, 40 insertions, 1 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 96c7d211..bdcb35f8 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -34,6 +34,9 @@ type integer_type = T.integer_type [@@deriving show, ord] *) type assumed_ty = State | Result | Vec | Option [@@deriving show, ord] +(* TODO: we should never directly manipulate `Return` and `Fail`, but rather + * the monadic functions `return` and `fail` (makes treatment of error and + * state-error monads more uniform) *) let result_return_id = VariantId.of_int 0 let result_fail_id = VariantId.of_int 1 @@ -375,7 +378,15 @@ type unop = Not | Neg of integer_type [@@deriving show, ord] type fun_id = | Regular of A.fun_id * T.RegionGroupId.id option (** Backward id: `Some` if the function is a backward function, `None` - if it is a forward function *) + if it is a forward function. + + TODO: we need to redefine A.fun_id here, to add `fail` and + `return` (important to get a unified treatment of the state-error + monad). For now, when using the state-error monad: extraction + works only if we unfold all the monadic let-bindings, and we + then replace the content of the occurrences of `Return` to also + return the state (which is really super ugly). + *) | Unop of unop | Binop of E.binop * integer_type [@@deriving show, ord] diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 61d247ea..6c61b9dc 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -1008,6 +1008,31 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx) let switch_body = Match [ fail_branch; success_branch ] in let e = Switch (re, switch_body) in self#visit_expression state_var e + + method! visit_Value state_var rv mp = + if config.use_state_monad then + match rv.ty with + | Adt (Assumed Result, _) -> ( + match rv.value with + | RvAdt av -> + (* We only need to replace the content of `Return ...` *) + (* TODO: type checking is completely broken at this point... *) + let variant_id = Option.get av.variant_id in + if variant_id = result_return_id then + let res_v = Collections.List.to_cons_nil av.field_values in + let state_value = mk_typed_rvalue_from_var state_var in + let res = mk_simpl_tuple_rvalue [ state_value; res_v ] in + let res = mk_result_return_rvalue res in + (mk_value_expression res None).e + else super#visit_Value state_var rv mp + | _ -> raise (Failure "Unrechable")) + | _ -> super#visit_Value state_var rv mp + else super#visit_Value state_var rv mp + (** We also need to update values, in case this value is `Return ...`. + + TODO: this is super ugly... We need to use the monadic functions + `fail` and `return` instead. + *) end in (* Update the body *) diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index f2ed1053..5709ce23 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -972,6 +972,9 @@ and translate_return (_config : config) (opt_v : V.typed_value option) (* Forward function *) let v = Option.get opt_v in let v = typed_value_to_rvalue ctx v in + (* TODO: we need to use a `return` function (otherwise we have problems + * with the state-error monad). We also need to update the type when using + * a state-error monad. *) let v = mk_result_return_rvalue v in let e = Value (v, None) in let ty = v.ty in |