blob: cd64a2880c80d41a8952e39cb69f19a6659c8d8d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
(** The following module defines micro-passes which operate on the pure AST *)
open Pure
(** This function computes pretty names for the variables in the pure AST. It
relies on the "meta"-place information in the AST to generate naming
constraints.
The way it works is as follows:
- we only modify the names of the unnamed variables
- whenever we see an rvalue/lvalue which is exactly an unnamed variable,
and this value is linked to some meta-place information which contains
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>) {
List::Cons(x, hd) => {
...
}
}
```
Actually, in MIR, we get:
```
tmp = discriminant(ls);
switch tmp {
0 => {
x = (ls as Cons).0;
hd = (ls as Cons).1;
...
}
}
```
If `ls` maps to a symbolic value `s0` upon evaluating the match in symbolic
mode, we expand this value upon evaluating `tmp = discriminant(ls)`.
However, at this point, we don't know which should be the names of
the symbolic values we introduce for the fields of `Cons`!
Let's imagine we have (for the `Cons` branch): `s0 ~~> Cons s1 s2`.
The assigments lead to the following binding in the evaluation context:
```
x -> s1
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.
*)
let compute_pretty_names () = ()
|
