diff options
| -rw-r--r-- | src/Pure.ml | 67 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 71 |
2 files changed, 121 insertions, 17 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 7e5aca47..4e0768cd 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -203,6 +203,55 @@ type let_bindings = (** Meta-information stored in the AST *) type meta = Assignment of mplace * typed_rvalue +(** Ancestor for [iter_expression] iter visitor *) +class ['self] iter_expression_base = + object (_self : 'self) + inherit [_] VisitorsRuntime.iter + + method visit_typed_rvalue : 'env -> typed_rvalue -> unit = fun _ _ -> () + + method visit_let_bindings : 'env -> let_bindings -> unit = fun _ _ -> () + + method visit_mplace : 'env -> mplace -> unit = fun _ _ -> () + + method visit_meta : 'env -> meta -> unit = fun _ _ -> () + + method visit_integer_type : 'env -> T.integer_type -> unit = fun _ _ -> () + + method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> () + + method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> () + + method visit_var_or_dummy : 'env -> var_or_dummy -> unit = fun _ _ -> () + end + +(** Ancestor for [map_expression] map visitor *) +class ['self] map_expression_base = + object (_self : 'self) + inherit [_] VisitorsRuntime.map + + method visit_typed_rvalue : 'env -> typed_rvalue -> typed_rvalue = + fun _ x -> x + + method visit_let_bindings : 'env -> let_bindings -> let_bindings = + fun _ x -> x + + method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x + + method visit_meta : 'env -> meta -> meta = fun _ x -> x + + method visit_integer_type : 'env -> T.integer_type -> T.integer_type = + fun _ x -> x + + method visit_scalar_value : 'env -> scalar_value -> scalar_value = + fun _ x -> x + + method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x + + method visit_var_or_dummy : 'env -> var_or_dummy -> var_or_dummy = + fun _ x -> x + end + (** **Rk.:** here, [expression] is not at all equivalent to the expressions used in CFIM. They are lambda-calculus expressions, and are thus actually more general than the CFIM statements, in a sense. @@ -230,6 +279,24 @@ and match_branch = { vars : var_or_dummy list; branch : expression; } +[@@deriving + visitors + { + name = "iter_expression"; + variety = "iter"; + ancestors = [ "iter_expression_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + }, + visitors + { + name = "map_expression"; + variety = "map"; + ancestors = [ "map_expression_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + }] +(** "Regular" typed value (we map variables to typed values) *) type fun_sig = { type_params : type_var list; diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index cd64a288..634537c2 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -1,5 +1,6 @@ (** The following module defines micro-passes which operate on the pure AST *) +open Errors open Pure (** This function computes pretty names for the variables in the pure AST. It @@ -13,6 +14,7 @@ open Pure a name and an empty path, we consider we should use this name For instance, the following situations happen: + - let's say we evaluate: ``` match (ls : List<T>) { @@ -24,11 +26,11 @@ open Pure Actually, in MIR, we get: ``` - tmp = discriminant(ls); + tmp := discriminant(ls); switch tmp { 0 => { - x = (ls as Cons).0; - hd = (ls as Cons).1; + x := (ls as Cons).0; + hd := (ls as Cons).1; ... } } @@ -44,19 +46,54 @@ open Pure hd -> s2 ``` - If at any moment we use `x` (as an operand to a function, to return, - etc.) we ... - TODO: finish explanations - TODO: meta-information for: - - unop - - binop - - assignments - - discriminant - - ... - - the subsequent assignments actually give us the naming information we - were looking for. - - TODO: temporaries for binops which can fail/have preconditions - - TODO: reborrows just before calling functions. + When generating the symbolic AST, we save as meta-information that we + assign `s1` to the place `x` and `s2` to the place `hd`. This way, + we learn we can use the names `x` and `hd` for the variables which are + introduced by the match: + ``` + match ls with + | Cons x hd -> ... + | ... + ``` + - If we write the following in Rust: + ``` + let x = y + z; + ``` + + We get the following MIR: + ``` + let tmp = y + z; + ``` + TODO: finish... + - If we write the following in Rust: + ``` + let px = &mut x; + f(px); + ``` + + Rustc generates the following MIR: + ``` + px := &mut x; + tmp := &mut ( *px ); // "tmp" is actually an anonymous variable + f(move tmp); + ``` + + As borrows and dereferencements are ignored in the pure paths we generate + (because they are extracted to the identity), we save as meta-data that + at some point we assign the value of `px` to `tmp`. + + TODO: actually useless, because `tmp` later gets inlined. + - TODO: inputs and end abstraction... *) let compute_pretty_names () = () + +(** Remove the meta-information *) +let remove_meta (e : expression) : expression = + let obj = + object + inherit [_] map_expression as super + + method! visit_Meta env meta e = super#visit_expression env e + end + in + obj#visit_expression () e |