diff options
Diffstat (limited to '')
| -rw-r--r-- | src/PureMicroPasses.ml | 71 |
1 files changed, 54 insertions, 17 deletions
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 |