diff options
author | Son Ho | 2022-01-28 14:54:51 +0100 |
---|---|---|
committer | Son Ho | 2022-01-28 14:54:51 +0100 |
commit | 057c6cc1f445449022b953b08f691e3f83386634 (patch) | |
tree | 42a4ae74cae2b13606051ca75311f4729c98054c /src/PureMicroPasses.ml | |
parent | c6eedd0ebe3c4f986cdea36ecec468ae1cadb537 (diff) |
Finish implementing to_monadic
Diffstat (limited to '')
-rw-r--r-- | src/PureMicroPasses.ml | 54 |
1 files changed, 41 insertions, 13 deletions
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 |