Implement visitors for Pure.expression and make minor modifications

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