From d15d71ca9f903883fcbfa515aa1e0637074ab78d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 27 Jan 2022 22:16:44 +0100
Subject: Make minor modifications and create PureMicroPasses.ml

---
 src/PrintPure.ml       |  2 +-
 src/PureMicroPasses.ml | 43 +++++++++++++++++++++++++++++++++++++++++++
 src/Translate.ml       |  1 +
 3 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 src/PureMicroPasses.ml

(limited to 'src')

diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index e5b58b9f..532278ea 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -227,7 +227,7 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
 
 let place_to_string (fmt : ast_formatter) (p : place) : string =
   (* TODO: improve that *)
-  let var = "@" ^ fmt.var_id_to_string p.var in
+  let var = fmt.var_id_to_string p.var in
   projection_to_string fmt var p.projection
 
 let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string
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 () = ()
diff --git a/src/Translate.ml b/src/Translate.ml
index 9de07519..e3f7bbb2 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -5,6 +5,7 @@ module T = Types
 module A = CfimAst
 module M = Modules
 module SA = SymbolicAst
+module Micro = PureMicroPasses
 
 (** The local logger *)
 let log = L.translate_log
-- 
cgit v1.2.3