diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Pure.ml | 17 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 51 |
2 files changed, 59 insertions, 9 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index fc6cbad1..aeb02fe2 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -196,6 +196,23 @@ class virtual ['self] reduce_value_base = method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero end +(*(** Ancestor for [mapreduce_var_or_dummy] visitor *) + class virtual ['self] mapreduce_value_base = + object (self : 'self) + inherit [_] VisitorsRuntime.mapreduce + + method visit_constant_value : 'env -> constant_value -> constant_vlaue * 'a = + fun _ _ -> self#zero + + method visit_var : 'env -> var -> va * 'a = fun _ _ -> self#zero + + method visit_place : 'env -> place -> place * 'a = fun _ _ -> self#zero + + method visit_mplace : 'env -> mplace -> mplace * 'a = fun _ _ -> self#zero + + method visit_ty : 'env -> ty -> ty * 'a = fun _ _ -> self#zero + end*) + type var_or_dummy = | Var of var * mplace option | Dummy (** Ignored value: `_`. *) diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 74796e22..2bc5d7aa 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -21,16 +21,15 @@ let get_expression_min_var_counter (e : expression) : VarId.generator = object inherit [_] reduce_expression - method zero _ _ = VarId.zero + method zero _ = VarId.zero - (* TODO: why 2 parameters??? I don't understand what's going on... *) - method plus id0 id1 _ _ = VarId.max (id0 () ()) (id1 () ()) + method plus id0 id1 _ = VarId.max (id0 ()) (id1 ()) (* Get the maximum *) - method! visit_var _ v _ () = v.id + method! visit_var _ v _ = v.id end in - let id = obj#visit_expression () e () () in + let id = obj#visit_expression () e () in VarId.generator_from_incr_id id type pn_ctx = string VarId.Map.t @@ -337,11 +336,45 @@ let inline_useless_var_reassignments (inline_named : bool) (def : fun_def) : let body = obj#visit_expression VarId.Map.empty def.body in { def with body } +(** Given a forward or backward function call, is there, for every execution + path, a child backward function called later with exactly the same input + list prefix? We use this to filter useless function calls: if there are + such child calls, we can remove this one (in case its outputs are not + used). + We do this check because we can't simply remove function calls whose + outputs are not used, as they might fail. However, if a function fails, + its children backward functions then fail on the same inputs (ignoring + the additional inputs those receive). + + For instance, if we have: + ``` + fn f<'a>(x : &'a mut T); + ``` + + We often have things like this in the synthesized code: + ``` + _ <-- f x; + ... + nx <-- f@back'a x y; + ... + ``` + + In this situation, we can remove the call `f x`. + *) +let expression_contains_child_call_in_all_paths (ctx : trans_ctx) (call : call) + (e : expression) : bool = + raise Unimplemented + (** Filter the unused assignments (removes the unused variables, filters the function calls) *) -let filter_unused_assignments (def : fun_def) : fun_def = - (* TODO *) - def +let filter_unused_assignments (ctx : trans_ctx) (def : fun_def) : fun_def = + (* let add_used_vars = () in + let filter_in_expr (e : expression) : VarId.Set.t = + match e with + | Value (v, _ ) -> let ctx = add_used_vars v ctx + | Call call -> + in*) + raise Unimplemented (** Add unit arguments for functions with no arguments, and change their return type. *) let to_monadic (def : fun_def) : fun_def = @@ -464,7 +497,7 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def = (* Filter the unused assignments (removes the unused variables, filters * the function calls) *) - let def = filter_unused_assignments def in + let def = filter_unused_assignments ctx def in log#ldebug (lazy ("filter_unused_assignments:\n\n" ^ fun_def_to_string ctx def ^ "\n")); |