Work on pretty names

9 files changed, 152 insertions, 101 deletions

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 065a39b9..89dfb274 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1202,12 +1202,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
           ^ aborrow_content_to_string ctx bc));
       let ctx =
         match bc with
-        | V.AMutBorrow (mv, bid, av) ->
+        | V.AMutBorrow (_mv, bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
             let sv = convert_avalue_to_given_back_value abs.kind av in
             (* Replace the mut borrow to register the fact that we ended
              * it and store with it the freshly generated given back value *)
-            let ended_borrow = V.ABorrow (V.AEndedMutBorrow (mv, sv, av)) in
+            let ended_borrow = V.ABorrow (V.AEndedMutBorrow (sv, av)) in
             let ctx = update_aborrow ek_all bid ended_borrow ctx in
             (* Give the value back *)
             let sv = mk_typed_value_from_symbolic_value sv in
@@ -1256,9 +1256,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
       (* Generate a fresh symbolic value *)
       let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
-      let ended_borrow =
-        V.AEndedProjBorrows { original = sv; given_back = nsv }
-      in
+      let ended_borrow = V.AEndedProjBorrows nsv in
       let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
diff --git a/src/Print.ml b/src/Print.ml
index 69379bf9..5ccba517 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -457,7 +457,7 @@ module Values = struct
         ^ ", "
         ^ typed_avalue_to_string fmt av
         ^ ")"
-    | AEndedMutBorrow (_mv, _msv, child) ->
+    | AEndedMutBorrow (_mv, child) ->
         "@ended_mut_borrow(" ^ typed_avalue_to_string fmt child ^ ")"
     | AEndedIgnoredMutBorrow
         { child; given_back_loans_proj; given_back_meta = _ } ->
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 9ca0c064..e962c27c 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -318,15 +318,10 @@ let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string
 
 let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string =
   match v with
-  | Var (v, { place = None; from_rvalue = None }) ->
-      var_to_string (ast_to_type_formatter fmt) v
-  | Var (v, { place; from_rvalue }) ->
-      let dest = Print.option_to_string (mplace_to_string fmt) place in
-      let from_rvalue =
-        Print.option_to_string (typed_rvalue_to_string fmt) from_rvalue
-      in
-      "(" ^ var_to_varname v ^ " @meta[@dest=" ^ dest ^ ", from_rvalue="
-      ^ from_rvalue ^ "] : "
+  | Var (v, None) -> var_to_string (ast_to_type_formatter fmt) v
+  | Var (v, Some mp) ->
+      let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in
+      "(" ^ var_to_varname v ^ " " ^ mp ^ " : "
       ^ ty_to_string (ast_to_type_formatter fmt) v.ty
       ^ ")"
   | Dummy -> "_"
diff --git a/src/Pure.ml b/src/Pure.ml
index dbc6421c..f0e43115 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -12,6 +12,16 @@ 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.) *)
@@ -283,14 +293,14 @@ and typed_rvalue = { value : rvalue; ty : ty }
         polymorphic = false;
       }]
 
-type mdplace = { place : mplace option; from_rvalue : typed_rvalue option }
-[@@deriving show]
-(** "Meta" destination place.
+(** Meta destination place.
 
     Meta information for places used as assignment destinations.
-    This is useful for the values given back by the backward functions: in such
-    situations, we link the output variables to the input arguments, to derive
-    names for the output variables from the input variables.
+    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.:
     ====
@@ -302,17 +312,21 @@ type mdplace = { place : mplace option; from_rvalue : typed_rvalue option }
     ```
     gets translated to:
     ```
-    let y = f_fwd x in
+    let y = f_fwd xv in
     ...
-    let s = f_back x y_i in // we want the introduced variable to be name "x1"
+    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. This is why we link the output variables to the input arguments:
-    it allows us to propagate such naming constraints "across" function calls.
+    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 =
@@ -348,7 +362,7 @@ class virtual ['self] mapreduce_var_or_dummy_base =
   end
 
 type var_or_dummy =
-  | Var of var * mdplace
+  | Var of var * mplace option
       (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections).
 
           We use [mplace] because it leads to a more uniform treatment of the meta
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index abdeb41e..ceaaa129 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -85,7 +85,9 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
   (* Find the max id in the input variables - some of them may have been
    * filtered from the body *)
   let min_input_id =
-    List.fold_left (fun id var -> VarId.max id var.id) VarId.zero body.inputs
+    List.fold_left
+      (fun id (var : var) -> VarId.max id var.id)
+      VarId.zero body.inputs
   in
   let obj =
     object
@@ -119,9 +121,12 @@ type pn_ctx = string VarId.Map.t
     - 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)
       
     Something important is that, for every variable we find, the name of this
-    variable is influenced by the information we find *below* in the AST.
+    variable can be influenced by the information we find *below* in the AST.
 
     For instance, the following situations happen:
     
@@ -139,8 +144,8 @@ type pn_ctx = string VarId.Map.t
       tmp := discriminant(ls);
       switch tmp {
         0 => {
-          x := (ls as Cons).0;
-          hd := (ls as Cons).1;
+          x := (ls as Cons).0; // (i)
+          hd := (ls as Cons).1; // (ii)
           ...
         }
       }
@@ -149,8 +154,10 @@ type pn_ctx = string VarId.Map.t
       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:
+      The assigments at (i) and (ii) lead to the following binding in the
+      evaluation context:
       ```
       x -> s1
       hd -> s2
@@ -165,7 +172,44 @@ type pn_ctx = string VarId.Map.t
       | Cons x hd -> ...
       | ...
       ```
+   - Given back values (introduced by backward functions):
+     Let's say we have the following Rust code:
+     ```
+     let py = id(&mut x);
+     *py = 2;
+     assert!(x == 2);
+     ```
+     
+     After desugaring, we get the following MIR:
+     ```
+     ^0 = &mut x; // anonymous variable
+     py = id(move ^0);
+     *py += 2;
+     assert!(x == 2);
+     ```
+     
+     We want this to be translated as:
+     ```
+     let py = id_fwd x in
+     let py1 = py + 2 in
+     let x1 = id_back x py1 in // <-- x1 is "given back": doesn't appear in the original MIR
+     assert(x1 = 2);
+     ```
+
+     We want to notice that the value given back by `id_back` is given back for "x",
+     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.
+
+     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 =
   (* Small helpers *)
@@ -217,6 +261,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   in
 
   let add_constraint (mp : mplace) (var_id : VarId.id) (ctx : pn_ctx) : pn_ctx =
+    (* Update the variable name *)
     match (mp.name, mp.projection) with
     | Some name, [] ->
         (* Check if the variable already has a name - if not: insert the new name *)
@@ -242,19 +287,39 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
 
         method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ())
 
-        method! visit_Var _ v mdp () =
+        method! visit_Var _ v mp () =
           (* Register the variable *)
           let ctx = add_var (self#zero ()) v in
           (* Register the mplace information if there is such information *)
-          match mdp.place with
-          | None -> ctx
-          | Some mp -> add_constraint mp v.id ctx
+          match mp with Some mp -> add_constraint mp v.id ctx | None -> ctx
       end
     in
     let ctx1 = obj#visit_typed_lvalue () lv () in
     merge_ctxs ctx ctx1
   in
 
+  (* This is used to propagate constraint information about places in case of
+   * assignments *)
+  let add_left_right_constraint (lv : typed_lvalue) (re : texpression)
+      (ctx : pn_ctx) : pn_ctx =
+    (* We propagate constraints across variable reassignments: `^0 = x` *)
+    match (lv.value, re.e) with
+    | ( 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
+    | ( 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
+
   (* *)
   let rec update_texpression (e : texpression) (ctx : pn_ctx) :
       pn_ctx * texpression =
@@ -286,6 +351,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
   and update_let (monadic : bool) (lv : typed_lvalue) (re : texpression)
       (e : texpression) (ctx : pn_ctx) : pn_ctx * expression =
     let ctx = add_left_constraint lv ctx in
+    let ctx = add_left_right_constraint lv re ctx in
     let ctx, re = update_texpression re ctx in
     let ctx, e = update_texpression e ctx in
     let lv = update_typed_lvalue ctx lv in
@@ -822,7 +888,7 @@ let to_monadic (config : config) (def : fun_decl) : fun_decl =
             let id, _ = VarId.fresh var_cnt in
             let var = { id; basename = None; ty = unit_ty } in
             let inputs = [ var ] in
-            let input_lv = mk_typed_lvalue_from_var var None None in
+            let input_lv = mk_typed_lvalue_from_var var None in
             let inputs_lvs = [ input_lv ] in
             Some { body with inputs; inputs_lvs }
       in
@@ -980,7 +1046,7 @@ let decompose_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) :
                    * monadic binding *)
                   let vid = fresh_id () in
                   let tmp : var = { id = vid; basename = None; ty = lv.ty } in
-                  let ltmp = mk_typed_lvalue_from_var tmp None None in
+                  let ltmp = mk_typed_lvalue_from_var tmp None in
                   let rtmp = mk_typed_rvalue_from_var tmp in
                   let rtmp = mk_value_expression rtmp None in
                   (* Visit the next expression *)
@@ -1058,9 +1124,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
                 in
                 (* The `Success` branch introduces a fresh state variable *)
                 let state_var = fresh_state_var () in
-                let state_value =
-                  mk_typed_lvalue_from_var state_var None None
-                in
+                let state_value = mk_typed_lvalue_from_var state_var None in
                 let success_pat =
                   mk_result_return_lvalue
                     (mk_simpl_tuple_lvalue [ state_value; lv ])
@@ -1131,7 +1195,7 @@ let unfold_monadic_let_bindings (config : config) (_ctx : trans_ctx)
           let sg = { sg with inputs = sg_inputs; outputs = sg_outputs } in
           (* Update the inputs list *)
           let inputs = body.inputs @ [ input_state_var ] in
-          let input_lv = mk_typed_lvalue_from_var input_state_var None None in
+          let input_lv = mk_typed_lvalue_from_var input_state_var None in
           let inputs_lvs = body.inputs_lvs @ [ input_lv ] in
           (* Update the body *)
           let body = { body with inputs; inputs_lvs } in
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 78ddf8aa..23bffa1d 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -64,10 +64,8 @@ let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
   let ty = v.ty in
   { value; ty }
 
-let mk_typed_lvalue_from_var (v : var) (mp : mplace option)
-    (mfrom_rvalue : typed_rvalue option) : typed_lvalue =
-  let mdplace = { place = mp; from_rvalue = mfrom_rvalue } in
-  let value = LvVar (Var (v, mdplace)) in
+let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue =
+  let value = LvVar (Var (v, mp)) in
   let ty = v.ty in
   { value; ty }
 
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 87e86e69..163ddde8 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -736,7 +736,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
   match bc with
   | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
       failwith "Unreachable"
-  | AEndedMutBorrow (_, _, _) ->
+  | AEndedMutBorrow (_, _) ->
       (* We collect consumed values: ignore *)
       None
   | AEndedIgnoredMutBorrow _ ->
@@ -804,9 +804,6 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
     
     [mp]: it is possible to provide some meta-place information, to guide
     the heuristics which later find pretty names for the variables.
-
-    TODO:
-    
  *)
 let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
     (ctx : bs_ctx) : bs_ctx * typed_lvalue option =
@@ -878,13 +875,10 @@ and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content)
   match bc with
   | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
       failwith "Unreachable"
-  | AEndedMutBorrow (consumed_mv, msv, _) ->
-      (* We use the originally consumed value (which is stored as a meta-value)
-       * to help with propagating naming constraints. *)
-      let consumed = typed_value_to_rvalue ctx consumed_mv in
+  | AEndedMutBorrow (msv, _) ->
       (* Return the meta-symbolic-value *)
       let ctx, var = fresh_var_for_symbolic_value msv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var mp (Some consumed)))
+      (ctx, Some (mk_typed_lvalue_from_var var mp))
   | AEndedIgnoredMutBorrow _ ->
       (* This happens with nested borrows: we need to dive in *)
       raise Unimplemented
@@ -903,15 +897,10 @@ and aproj_to_given_back (mp : mplace option) (aproj : V.aproj) (ctx : bs_ctx) :
           (fun (_, aproj) -> aproj = V.AIgnoredProjBorrows)
           child_projs);
       (ctx, None)
-  | AEndedProjBorrows { original; given_back = mv } ->
-      (* We use the original symbolic value to help propagate the naming constraints *)
-      let original =
-        InterpreterUtils.mk_typed_value_from_symbolic_value original
-      in
-      let original = typed_value_to_rvalue ctx original in
+  | AEndedProjBorrows mv ->
       (* Return the meta-value *)
       let ctx, var = fresh_var_for_symbolic_value mv ctx in
-      (ctx, Some (mk_typed_lvalue_from_var var mp (Some original)))
+      (ctx, Some (mk_typed_lvalue_from_var var mp))
   | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
       failwith "Unreachable"
 
@@ -1050,7 +1039,7 @@ and translate_function_call (config : config) (call : S.call) (e : S.expression)
       (fun (arg, mp) -> mk_value_expression arg mp)
       (List.combine args args_mplaces)
   in
-  let dest_v = mk_typed_lvalue_from_var dest dest_mplace None in
+  let dest_v = mk_typed_lvalue_from_var dest dest_mplace in
   let call = { func; type_params; args } in
   let call = Call call in
   let call_ty = if monadic then mk_result_ty dest_v.ty else dest_v.ty in
@@ -1115,7 +1104,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       List.fold_right
         (fun (var, value) (e : texpression) ->
           mk_let monadic
-            (mk_typed_lvalue_from_var var None None)
+            (mk_typed_lvalue_from_var var None)
             (mk_value_expression value None)
             e)
         variables_values next_e
@@ -1287,7 +1276,7 @@ and translate_expansion (config : config) (p : S.mplace option)
           let next_e = translate_expression config e ctx in
           let monadic = false in
           mk_let monadic
-            (mk_typed_lvalue_from_var var None None)
+            (mk_typed_lvalue_from_var var None)
             (mk_value_expression scrutinee scrutinee_mplace)
             next_e
       | SeAdt _ ->
@@ -1311,7 +1300,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                 (* This is an enumeration: introduce an [ExpandEnum] let-binding *)
                 let variant_id = Option.get variant_id in
                 let lvars =
-                  List.map (fun v -> mk_typed_lvalue_from_var v None None) vars
+                  List.map (fun v -> mk_typed_lvalue_from_var v None) vars
                 in
                 let lv = mk_adt_lvalue scrutinee.ty variant_id lvars in
                 let monadic = false in
@@ -1340,13 +1329,13 @@ and translate_expansion (config : config) (p : S.mplace option)
                   (fun (fid, var) e ->
                     let field_proj = gen_field_proj fid var in
                     mk_let monadic
-                      (mk_typed_lvalue_from_var var None None)
+                      (mk_typed_lvalue_from_var var None)
                       (mk_value_expression field_proj None)
                       e)
                   id_var_pairs branch
           | T.Tuple ->
               let vars =
-                List.map (fun x -> mk_typed_lvalue_from_var x None None) vars
+                List.map (fun x -> mk_typed_lvalue_from_var x None) vars
               in
               let monadic = false in
               mk_let monadic
@@ -1362,7 +1351,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                * identity when extracted (`box a == a`) *)
               let monadic = false in
               mk_let monadic
-                (mk_typed_lvalue_from_var var None None)
+                (mk_typed_lvalue_from_var var None)
                 (mk_value_expression scrutinee scrutinee_mplace)
                 branch
           | T.Assumed T.Vec ->
@@ -1383,7 +1372,7 @@ and translate_expansion (config : config) (p : S.mplace option)
             let variant_id = Option.get variant_id in
             let ctx, vars = fresh_vars_for_symbolic_values svl ctx in
             let vars =
-              List.map (fun x -> mk_typed_lvalue_from_var x None None) vars
+              List.map (fun x -> mk_typed_lvalue_from_var x None) vars
             in
             let pat_ty = scrutinee.ty in
             let pat = mk_adt_lvalue pat_ty variant_id vars in
@@ -1456,6 +1445,9 @@ 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
   log#ldebug
@@ -1492,7 +1484,7 @@ let translate_fun_decl (config : config) (ctx : bs_ctx)
         in
         let inputs = List.append ctx.forward_inputs backward_inputs in
         let inputs_lvs =
-          List.map (fun v -> mk_typed_lvalue_from_var v None None) inputs
+          List.map (fun v -> mk_typed_lvalue_from_var v None) inputs
         in
         (* Sanity check *)
         assert (
diff --git a/src/Values.ml b/src/Values.ml
index a3dfb84a..3314defb 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -329,16 +329,10 @@ type aproj =
           
           Note that we keep the original symbolic value as a meta-value.
        *)
-  | AEndedProjBorrows of {
-      original : msymbolic_value;
-      given_back : msymbolic_value;
-    }
+  | AEndedProjBorrows of msymbolic_value
       (** The only purpose of [AEndedProjBorrows] is to store, for synthesis
-          purposes, the symbolic value which was originally in the borrow projection,
-          and the symbolic value which was generated and given back upon ending the borrow.
-       
-          The given back value is necessary for the synthesis. The orignal value is
-          useful to propagate naming constraints.
+          purposes, the symbolic value which was generated and given back upon
+          ending the borrow.
        *)
   | AIgnoredProjBorrows
 [@@deriving
@@ -681,13 +675,9 @@ and aborrow_content =
             abstraction so that we can properly call the backward functions
             when generating the pure translation.
        *)
-  | AEndedMutBorrow of mvalue * msymbolic_value * typed_avalue
+  | AEndedMutBorrow of msymbolic_value * typed_avalue
       (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value
-          that we gave back as a meta-value, to help with the synthesis, together
-          with the initial consumed value (also as a meta-value).
-
-          The given back value is necessary for the synthesis. The orignal consumed
-          value is useful to propagate naming constraints.
+          that we gave back as a meta-value, to help with the synthesis.
 
           We also remember the child [avalue] because this structural information
           is useful for the synthesis (but not for the symbolic execution):
diff --git a/src/main.ml b/src/main.ml
index 00693890..943689be 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.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;
+  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;
   (* Load the module *)
   let json = Yojson.Basic.from_file filename in
   match llbc_module_of_json json with