diff options
author | Son Ho | 2022-01-27 22:16:44 +0100 |
---|---|---|
committer | Son Ho | 2022-01-27 22:16:44 +0100 |
commit | d15d71ca9f903883fcbfa515aa1e0637074ab78d (patch) | |
tree | 4bae16226021e901e7764f500114c2912720116c /src/PureMicroPasses.ml | |
parent | 6070002cbc97a46b8c060a8ac58c0602a1fbf660 (diff) |
Make minor modifications and create PureMicroPasses.ml
Diffstat (limited to '')
-rw-r--r-- | src/PureMicroPasses.ml | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml new file mode 100644 index 00000000..f35ee2d6 --- /dev/null +++ b/src/PureMicroPasses.ml @@ -0,0 +1,43 @@ +(** 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 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`! Still, + the subsequent assignments actually give us the naming information we + were looking for. + *) +let compute_pretty_names () = () |