Improve the generation of pretty names by correctly using the

left constraints

4 files changed, 30 insertions, 23 deletions

diff --git a/src/Print.ml b/src/Print.ml
index 24945298..5ccba517 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -1072,9 +1072,8 @@ module LlbcAst = struct
      * (we have access to a body) *)
     match def.body with
     | None ->
-        (* Arguments - we need to ignore the first input type which is actually
-         * the return type... TODO: fix that *)
-        let input_tys = List.tl sg.inputs in
+        (* Arguments *)
+        let input_tys = sg.inputs in
         let args = List.map sty_to_string input_tys in
         let args = String.concat ", " args in
 
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 1ad37a5b..09194d85 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -191,19 +191,15 @@ let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string =
       "enum " ^ name ^ params ^ " =\n" ^ variants
   | Opaque -> "opaque type " ^ name ^ params
 
+let var_to_varname (v : var) : string =
+  match v.basename with
+  | Some name -> name ^ "^" ^ VarId.to_string v.id
+  | None -> "^" ^ VarId.to_string v.id
+
 let var_to_string (fmt : type_formatter) (v : var) : string =
-  let varname =
-    match v.basename with
-    | Some name -> name ^ "^" ^ VarId.to_string v.id
-    | None -> "^" ^ VarId.to_string v.id
-  in
+  let varname = var_to_varname v in
   "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")"
 
-let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string =
-  match v with
-  | Var (v, _) -> var_to_string (value_to_type_formatter fmt) v
-  | Dummy -> "_"
-
 let rec projection_to_string (fmt : ast_formatter) (inside : string)
     (p : projection) : string =
   match p with
@@ -228,6 +224,20 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
               let variant_name = fmt.adt_variant_to_string adt_id variant_id in
               "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
 
+let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
+  let name = match p.name with None -> "_" | Some name -> name in
+  projection_to_string fmt name p.projection
+
+let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string =
+  match v with
+  | Var (v, Some { name = Some name; projection }) ->
+      assert (projection = []);
+      let fmt = value_to_type_formatter fmt in
+      "(" ^ var_to_varname v ^ " @meta[@dest=" ^ name ^ "] : "
+      ^ ty_to_string fmt v.ty ^ ")"
+  | Var (v, _) -> var_to_string (value_to_type_formatter fmt) v
+  | Dummy -> "_"
+
 let place_to_string (fmt : ast_formatter) (p : place) : string =
   (* TODO: improve that *)
   let var = fmt.var_id_to_string p.var in
@@ -394,10 +404,6 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string =
   | Binop (binop, int_ty) ->
       binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">"
 
-let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
-  let name = match p.name with None -> "_" | Some name -> name in
-  projection_to_string fmt name p.projection
-
 let meta_to_string (fmt : ast_formatter) (meta : meta) : string =
   let meta =
     match meta with
@@ -444,10 +450,9 @@ and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string)
     (monadic : bool) (lv : typed_lvalue) (re : texpression) (e : texpression) :
     string =
   let indent1 = indent ^ indent_incr in
-  let val_fmt = ast_to_value_formatter fmt in
   let re = texpression_to_string fmt indent1 indent_incr re in
   let e = texpression_to_string fmt indent indent_incr e in
-  let lv = typed_lvalue_to_string val_fmt lv in
+  let lv = typed_lvalue_to_string (ast_to_value_formatter fmt) lv in
   if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e
   else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e
 
@@ -466,9 +471,8 @@ and switch_to_string (fmt : ast_formatter) (indent : string)
       "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent ^ e_true ^ "\n" ^ indent
       ^ "else\n" ^ indent ^ e_false
   | Match branches ->
-      let val_fmt = ast_to_value_formatter fmt in
       let branch_to_string (b : match_branch) : string =
-        let pat = typed_lvalue_to_string val_fmt b.pat in
+        let pat = typed_lvalue_to_string (ast_to_value_formatter fmt) b.pat in
         indent ^ "| " ^ pat ^ " ->\n" ^ indent1
         ^ texpression_to_string fmt indent1 indent_incr b.branch
       in
diff --git a/src/Pure.ml b/src/Pure.ml
index 9efab912..58ee0b98 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -236,7 +236,7 @@ class virtual ['self] mapreduce_value_base =
   end
 
 type var_or_dummy =
-  | Var of var * mplace option
+  | Var of var * mplace option (* TODO: the mplace is actually always a variable *)
   | Dummy  (** Ignored value: `_`. *)
 [@@deriving
   show,
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 7b34ad76..06fd3d69 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -242,7 +242,11 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
 
         method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ())
 
-        method! visit_var _ v () = add_var (self#zero ()) v
+        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 mp with None -> ctx | Some mp -> add_constraint mp v.id ctx
       end
     in
     let ctx1 = obj#visit_typed_lvalue () lv () in