Cleanup and update comments

5 files changed, 75 insertions, 130 deletions

diff --git a/src/Pure.ml b/src/Pure.ml
index 02b821ef..e7721b41 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -12,16 +12,6 @@ module FieldId = T.FieldId
 module SymbolicValueId = V.SymbolicValueId
 module FunDeclId = A.FunDeclId
 
-module MPlaceId = IdGen ()
-(** A meta-place identifier. See [mplace]. *)
-
-(** Some global counters - TODO: remove *)
-
-let mplace_id_counter, fresh_mplace_id = MPlaceId.fresh_stateful_generator ()
-
-(** Reset the mplace counter *)
-let reset_pure_counters () = mplace_id_counter := MPlaceId.generator_zero
-
 module SynthPhaseId = IdGen ()
 (** We give an identifier to every phase of the synthesis (forward, backward
     for group of regions 0, etc.) *)
@@ -297,74 +287,6 @@ and typed_rvalue = { value : rvalue; ty : ty }
         polymorphic = false;
       }]
 
-(** Meta destination place.
-
-    Meta information for places used as assignment destinations.
-    Either a regular mplace, or an mplace derived from another mplace.
-    
-    The second case is used for values given back by backward function: we
-    remember the identifier of the place from which the input argument was
-    taken from.
-
-    Ex.:
-    ====
-    ```
-    let y = f<'a>(&mut x);
-    ...
-    // end 'a
-    ...
-    ```
-    gets translated to:
-    ```
-    let y = f_fwd xv in
-    ...
-    let s = f_back xv y_i in // we want the introduced variable to be name "x"
-    ...
-    ```
-    In order to compute a proper name for the variable introduced by the backward
-    call, we need to link `s` to `x`. However, because of desugaring, it may happen
-    that the fact `f` takes `x` as argument may have to be computed by propagating
-    naming information. We use place identifiers to link the output variables to the
-    input arguments: it allows us to propagate naming constraints "across" function
-    calls.
-
-    The full details are given in [PureMicroPasses.compute_pretty_names]
- *)
-type mdplace = Regular of mplace | From of MPlaceId.id [@@deriving show]
-
-(** Ancestor for [iter_var_or_dummy] visitor *)
-class ['self] iter_var_or_dummy_base =
-  object (_self : 'self)
-    inherit [_] iter_typed_rvalue
-
-    method visit_mdplace : 'env -> mdplace -> unit = fun _ _ -> ()
-  end
-
-(** Ancestor for [map_var_or_dummy] visitor *)
-class ['self] map_var_or_dummy_base =
-  object (_self : 'self)
-    inherit [_] map_typed_rvalue
-
-    method visit_mdplace : 'env -> mdplace -> mdplace = fun _ x -> x
-  end
-
-(** Ancestor for [reduce_var_or_dummy] visitor *)
-class virtual ['self] reduce_var_or_dummy_base =
-  object (self : 'self)
-    inherit [_] reduce_typed_rvalue
-
-    method visit_mdplace : 'env -> mdplace -> 'a = fun _ _ -> self#zero
-  end
-
-(** Ancestor for [mapreduce_var_or_dummy] visitor *)
-class virtual ['self] mapreduce_var_or_dummy_base =
-  object (self : 'self)
-    inherit [_] mapreduce_typed_rvalue
-
-    method visit_mdplace : 'env -> mdplace -> mdplace * 'a =
-      fun _ x -> (x, self#zero)
-  end
-
 type var_or_dummy =
   | Var of var * mplace option
       (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections).
@@ -379,7 +301,7 @@ type var_or_dummy =
       {
         name = "iter_var_or_dummy";
         variety = "iter";
-        ancestors = [ "iter_var_or_dummy_base" ];
+        ancestors = [ "iter_typed_rvalue" ];
         nude = true (* Don't inherit [VisitorsRuntime.iter] *);
         concrete = true;
         polymorphic = false;
@@ -388,7 +310,7 @@ type var_or_dummy =
       {
         name = "map_var_or_dummy";
         variety = "map";
-        ancestors = [ "map_var_or_dummy_base" ];
+        ancestors = [ "map_typed_rvalue" ];
         nude = true (* Don't inherit [VisitorsRuntime.map] *);
         concrete = true;
         polymorphic = false;
@@ -397,7 +319,7 @@ type var_or_dummy =
       {
         name = "reduce_var_or_dummy";
         variety = "reduce";
-        ancestors = [ "reduce_var_or_dummy_base" ];
+        ancestors = [ "reduce_typed_rvalue" ];
         nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
         polymorphic = false;
       },
@@ -405,7 +327,7 @@ type var_or_dummy =
       {
         name = "mapreduce_var_or_dummy";
         variety = "mapreduce";
-        ancestors = [ "mapreduce_var_or_dummy_base" ];
+        ancestors = [ "mapreduce_typed_rvalue" ];
         nude = true (* Don't inherit [VisitorsRuntime.reduce] *);
         polymorphic = false;
       }]
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index a963e628..bc4cdc3c 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -112,7 +112,9 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
 
 type pn_ctx = {
   pure_vars : string VarId.Map.t;
+      (** Information about the pure variables used in the synthesized program *)
   llbc_vars : string V.VarId.Map.t;
+      (** Information about the LLBC variables used in the original program *)
 }
 (** "pretty-name context": see [compute_pretty_names] *)
 
@@ -125,9 +127,10 @@ type pn_ctx = {
     - 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 the values given back by backward functions, we link the given back
-      values to the places (identified by unique indices) where the input
-      arguments come from (see examples below)
+    - we try to propagate naming constraints on the pure variables use in the
+      synthesized programs, and also on the LLBC variables from the original
+      program (information about the LLBC variables is stored in the meta-places)
+      
       
     Something important is that, for every variable we find, the name of this
     variable can be influenced by the information we find *below* in the AST.
@@ -176,6 +179,13 @@ type pn_ctx = {
       | Cons x hd -> ...
       | ...
       ```
+   - Assignments:
+     `let x [@mplace=lp] = v [@mplace = rp} in ...`
+     
+     We propagate naming information across the assignments. This is important
+     because many reassignments using temporary, anonymous variables are
+     introduced during desugaring.
+   
    - Given back values (introduced by backward functions):
      Let's say we have the following Rust code:
      ```
@@ -204,15 +214,13 @@ type pn_ctx = {
      so we should use "x" as the basename (hence the resulting name "x1"). However,
      this is non-trivial, because after desugaring the input argument given to `id`
      is not `&mut x` but `move ^0` (i.e., it comes from a temporary, anonymous
-     variable). For this reason, we give unique identifiers to places, link
-     given back values to the places where the input arguments come from, and
-     propagate naming information between the places.
+     variable). For this reason, we use the meta-place "&mut x" as the meta-place
+     for the given back value (this is done during the synthesis), and propagate
+     naming information *also* on the LLBC variables (which are referenced by the
+     meta-places).
 
      This way, because of `^0 = &mut x`, we can propagate the name "x" to the place
      `^0`, then to the given back variable across the function call.
-
-   - TODO: inputs and end abstraction...
-   
    
  *)
 let compute_pretty_names (def : fun_decl) : fun_decl =
@@ -252,7 +260,20 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     List.fold_left (fun ctx0 ctx1 -> merge_ctxs ctx0 ctx1) empty_ctx ctxs
   in
 
-  let add_var (ctx : pn_ctx) (v : var) : pn_ctx =
+  (*
+   * The way we do is as follows:
+   * - we explore the expressions
+   * - we register the variables introduced by the let-bindings
+   * - we use the naming information we find (through the variables and the
+   *   meta-places) to update our context (i.e., maps from variable ids to
+   *   names)
+   * - we use this information to update the names of the variables used in the
+   *   expressions
+   *)
+
+  (* Register a variable for constraints propagation - used when an variable is
+   * introduced (left-hand side of a left binding) *)
+  let register_var (ctx : pn_ctx) (v : var) : pn_ctx =
     assert (not (VarId.Map.mem v.id ctx.pure_vars));
     match v.basename with
     | None -> ctx
@@ -260,6 +281,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
         let pure_vars = VarId.Map.add v.id name ctx.pure_vars in
         { ctx with pure_vars }
   in
+  (* Update a variable - used to update an expression after we computed constraints *)
   let update_var (ctx : pn_ctx) (v : var) (mp : mplace option) : var =
     match v.basename with
     | Some _ -> v
@@ -275,6 +297,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
               | Some basename -> { v with basename = Some basename }
             else v)
   in
+  (* Update an lvalue - used to update an expression after we computed constraints *)
   let update_typed_lvalue ctx (lv : typed_lvalue) : typed_lvalue =
     let obj =
       object
@@ -286,6 +309,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     obj#visit_typed_lvalue () lv
   in
 
+  (* Register an mplace the first time we find one *)
   let register_mplace (mp : mplace) (ctx : pn_ctx) : pn_ctx =
     match (V.VarId.Map.find_opt mp.var_id ctx.llbc_vars, mp.name) with
     | None, Some name ->
@@ -294,6 +318,8 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     | _ -> ctx
   in
 
+  (* Register the fact that [name] can be used for the pure variable identified
+   * by [var_id] (will add this name in the map if the variable is anonymous) *)
   let add_pure_var_constraint (var_id : VarId.id) (name : string) (ctx : pn_ctx)
       : pn_ctx =
     let pure_vars =
@@ -302,6 +328,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     in
     { ctx with pure_vars }
   in
+  (* Similar to [add_pure_var_constraint], but for LLBC variables *)
   let add_llbc_var_constraint (var_id : V.VarId.id) (name : string)
       (ctx : pn_ctx) : pn_ctx =
     let llbc_vars =
@@ -310,6 +337,8 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     in
     { ctx with llbc_vars }
   in
+  (* Add a constraint: given a variable id and an associated meta-place, try to
+   * extract naming information from the meta-place and save it *)
   let add_constraint (mp : mplace) (var_id : VarId.id) (ctx : pn_ctx) : pn_ctx =
     (* Register the place *)
     let ctx = register_mplace mp ctx in
@@ -322,6 +351,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
         ctx
     | _ -> ctx
   in
+  (* Specific case of constraint on rvalues *)
   let add_right_constraint (mp : mplace) (rv : typed_rvalue) (ctx : pn_ctx) :
       pn_ctx =
     (* Register the place *)
@@ -333,6 +363,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       (ctx : pn_ctx) : pn_ctx =
     match mp with None -> ctx | Some mp -> add_right_constraint mp rv ctx
   in
+  (* Specific case of constraint on left values *)
   let add_left_constraint (lv : typed_lvalue) (ctx : pn_ctx) : pn_ctx =
     let obj =
       object (self)
@@ -344,7 +375,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
 
         method! visit_Var _ v mp () =
           (* Register the variable *)
-          let ctx = add_var (self#zero ()) v in
+          let ctx = register_var (self#zero ()) v in
           (* Register the mplace information if there is such information *)
           match mp with Some mp -> add_constraint mp v.id ctx | None -> ctx
       end
@@ -354,7 +385,8 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   in
 
   (* This is used to propagate constraint information about places in case of
-   * assignments *)
+   * variable reassignments: we try to propagate the information from the
+   * rvalue to the left *)
   let add_left_right_constraint (lv : typed_lvalue) (re : texpression)
       (ctx : pn_ctx) : pn_ctx =
     (* We propagate constraints across variable reassignments: `^0 = x`,
@@ -403,23 +435,6 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
               ctx
           | _ -> ctx)
     | _ -> ctx
-    (* match (lv.value, re.e) with
-       (* Case 1: *)
-       | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))),
-           Value (_, Some ({ name = Some _; projection = [] } as rmp)) ) ->
-           (* Use the meta-information on the right *)
-           add_constraint rmp lvar.id ctx
-       (* Case 2: *)
-       | ( LvVar (Var (lvar, (Some { name = None; projection = [] } | None))),
-           Value ({ value = RvPlace { var = rvar_id; projection = [] }; ty = _ }, _)
-         ) -> (
-           (* Use the variable name *)
-           match
-             (VarId.Map.find_opt lvar.id ctx, VarId.Map.find_opt rvar_id ctx)
-           with
-           | None, Some name -> VarId.Map.add lvar.id name ctx
-           | _ -> ctx)
-         | _ -> (* Nothing to propagate *) ctx *)
   in
 
   (* *)
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 65bdcf9c..e32e28d6 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -640,7 +640,7 @@ let rec typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) : typed_rvalue
             (translate mv).value
         | V.InactivatedMutBorrow (mv, _) ->
             (* Same as for shared borrows. However, note that we use inactivated borrows
-             * only in meta-data: a value actually used in the translation can't come
+             * only in meta-data: a value actually *used in the translation* can't come
              * from an unpromoted inactivated borrow *)
             (translate mv).value
         | V.MutBorrow (_, v) ->
@@ -1451,8 +1451,6 @@ and translate_meta (config : config) (meta : S.meta) (e : S.expression)
 
 let translate_fun_decl (config : config) (ctx : bs_ctx)
     (body : S.expression option) : fun_decl =
-  (* Reset the counters *)
-  reset_pure_counters ();
   (* Translate *)
   let def = ctx.fun_decl in
   let bid = ctx.bid in
diff --git a/src/Values.ml b/src/Values.ml
index 3f1fc0bd..4799f3b9 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -173,6 +173,16 @@ and borrow_content =
           The meta-value is used for the same purposes as with shared borrows,
           at the exception that in case of inactivated borrows it is not
           *necessary* for the synthesis: we keep it only as meta-information.
+          To be more precise:
+          - when generating the synthesized program, we may need to convert
+            shared borrows to pure values
+          - we never need to do so for inactivated borrows: such borrows must
+            be activated at the moment we use them (meaning we convert a *mutable*
+            borrow to a pure value). However, we save meta-data about the assignments,
+            which is used to make the code cleaner: when generating this meta-data,
+            we may need to convert inactivated borrows to pure values, in which
+            situation we convert the meta-value we stored in the inactivated
+            borrow.
        *)
 
 and loan_content =
diff --git a/src/main.ml b/src/main.ml
index 943689be..00693890 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -122,22 +122,22 @@ let () =
 
   (* Set up the logging - for now we use default values - TODO: use the
    * command-line arguments *)
-  Easy_logging.Handlers.set_level main_logger_handler EL.Debug;
-  main_log#set_level EL.Debug;
-  llbc_of_json_logger#set_level EL.Debug;
-  pre_passes_log#set_level EL.Debug;
-  interpreter_log#set_level EL.Debug;
-  statements_log#set_level EL.Debug;
-  paths_log#set_level EL.Debug;
-  expressions_log#set_level EL.Debug;
-  expansion_log#set_level EL.Debug;
-  borrows_log#set_level EL.Debug;
-  invariants_log#set_level EL.Debug;
-  pure_utils_log#set_level EL.Debug;
-  symbolic_to_pure_log#set_level EL.Debug;
-  pure_micro_passes_log#set_level EL.Debug;
-  pure_to_extract_log#set_level EL.Debug;
-  translate_log#set_level EL.Debug;
+  Easy_logging.Handlers.set_level main_logger_handler EL.Info;
+  main_log#set_level EL.Info;
+  llbc_of_json_logger#set_level EL.Info;
+  pre_passes_log#set_level EL.Info;
+  interpreter_log#set_level EL.Info;
+  statements_log#set_level EL.Info;
+  paths_log#set_level EL.Info;
+  expressions_log#set_level EL.Info;
+  expansion_log#set_level EL.Info;
+  borrows_log#set_level EL.Info;
+  invariants_log#set_level EL.Info;
+  pure_utils_log#set_level EL.Info;
+  symbolic_to_pure_log#set_level EL.Info;
+  pure_micro_passes_log#set_level EL.Info;
+  pure_to_extract_log#set_level EL.Info;
+  translate_log#set_level EL.Info;
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match llbc_module_of_json json with