diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | TODO.md | 5 | ||||
| -rw-r--r-- | src/Pure.ml | 13 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 25 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 3 |
5 files changed, 43 insertions, 5 deletions
@@ -30,7 +30,7 @@ test: build translate-no_nested_borrows translate-hashmap translate-paper # Add specific options to some tests translate-no_nested_borrows translate-paper: \ - TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-decreases-clauses + TRANS_OPTIONS:=$(TRANS_OPTIONS) -test-units -no-split-files -no-state -no-decreases-clauses translate-no_nested_borrows translate-paper: SUBDIR:=misc translate-hashmap: TRANS_OPTIONS:=$(TRANS_OPTIONS) -template-clauses -no-state translate-hashmap: SUBDIR:=hashmap @@ -1,8 +1,7 @@ # TODO -0. borrows which are never ended? Drop locals in *symbolic* modes upon return - -0. improve variable names generation: "hash_map" -> "hm" (and not just "h") +0. Improve treatments of error and state error monads. In particular, introduce + `return` and `fail`, and remove `Return` and `Fail`. 0. replace all the `failwith` with `raise (Failure ...)`: in CPS, it messes up with provenance tracking 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 |