diff options
| -rw-r--r-- | src/Pure.ml | 5 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 54 | ||||
| -rw-r--r-- | src/SymbolicToPure.ml | 2 |
3 files changed, 48 insertions, 13 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 30d4a0a8..90f6dc26 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -468,6 +468,8 @@ type fun_sig = { outputs : ty list; (** The list of outputs. + Immediately after the translation from symbolic to pure we have this + the following: In case of a forward function, the list will have length = 1. However, in case of backward function, the list may have length > 1. If the length is > 1, it gets extracted to a tuple type. Followingly, @@ -475,6 +477,9 @@ type fun_sig = { want to account for the fact that we immediately deconstruct the tuple upon calling the backward function (because the backward function is called to update a set of values in the environment). + + After the "to monadic" pass, the list has size exactly one (and we + use the `Result` type). *) } diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 3b91eaa5..efe26bc4 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -307,18 +307,40 @@ let to_monadic (def : fun_def) : fun_def = let body = obj#visit_expression () def.body in let def = { def with body } in - (* Update the signature *) - if def.inputs = [] then ( - assert (def.signature.inputs = []); - let signature = - { def.signature with inputs = [ SymbolicToPure.unit_ty ] } - in - let var_cnt = get_expression_min_var_counter def.body in - let id, _ = VarId.fresh var_cnt in - let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in - let inputs = [ var ] in - { def with signature; inputs }) - else def + (* Update the signature: first the input types *) + let def = + if def.inputs = [] then ( + assert (def.signature.inputs = []); + let signature = + { def.signature with inputs = [ SymbolicToPure.unit_ty ] } + in + let var_cnt = get_expression_min_var_counter def.body in + let id, _ = VarId.fresh var_cnt in + let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in + let inputs = [ var ] in + { def with signature; inputs }) + else def + in + (* Then the output type *) + let output_ty = + match (def.back_id, def.signature.outputs) with + | None, [ out_ty ] -> + (* Forward function: there is always exactly one output *) + SymbolicToPure.mk_result_ty out_ty + | Some _, outputs -> + (* Backward function: we have to group them *) + SymbolicToPure.mk_result_ty (SymbolicToPure.mk_tuple_ty outputs) + | _ -> failwith "Unreachable" + in + let outputs = [ output_ty ] in + let signature = { def.signature with outputs } in + { def with signature } + +(** Convert the unit variables to `()` if they are used as right-values or + `_` if they are used as left values. *) +let unit_vars_to_unit (def : fun_def) : fun_def = + (* TODO *) + def (** Apply all the micro-passes to a function. @@ -349,10 +371,16 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def = (* Add unit arguments for functions with no arguments, and change their return type. * **Rk.**: from now onwards, the types in the AST are correct (until now, - * functions had return type `t` where they should have return type `result t`) *) + * functions had return type `t` where they should have return type `result t`). + * Also, from now onwards, the outputs list has length 1. x*) let def = to_monadic def in log#ldebug (lazy ("to_monadic:\n" ^ fun_def_to_string ctx def)); + (* Convert the unit variables to `()` if they are used as right-values or + * `_` if they are used as left values. *) + let def = unit_vars_to_unit def in + log#ldebug (lazy ("unit_vars_to_unit:\n" ^ fun_def_to_string ctx def)); + (* Inline the useless variable reassignments *) let def = inline_useless_var_reassignments def in log#ldebug diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 30142639..345555e7 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -75,6 +75,8 @@ let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue = in { value; ty } +let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) + (** Type substitution *) let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty = let obj = |