From 5a36b1b03d95c5021e803df9a3ff24084a27db3d Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves@strub.nu>
Date: Wed, 25 Sep 2024 08:04:35 +0200
Subject: [PATCH] pretty-printer/parser: improve reparsability of the
 pretty-printer output

---
 src/ecParser.mly   |  4 ++--
 src/ecParsetree.ml |  2 +-
 src/ecPrinting.ml  | 21 +++++++++++++--------
 src/ecTyping.ml    |  5 +++--
 4 files changed, 19 insertions(+), 13 deletions(-)

diff --git a/src/ecParser.mly b/src/ecParser.mly
index 55277b088..6c7b11a10 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -1440,10 +1440,10 @@ lvalue_u:
 | LPAREN p=plist2(qident, COMMA) RPAREN
    { PLvTuple p }
 
-| x=loc(fident) DLBRACKET ti=tvars_app? e=expr RBRACKET
+| x=loc(fident) DLBRACKET ti=tvars_app? es=plist1(expr, COMMA) RBRACKET
    { match lqident_of_fident x.pl_desc with
      | None   -> parse_error x.pl_loc None
-     | Some v -> PLvMap (mk_loc x.pl_loc v, ti, e) }
+     | Some v -> PLvMap (mk_loc x.pl_loc v, ti, es) }
 
 %inline lvalue:
 | x=loc(lvalue_u) { x }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 593b1a200..fa20ee80e 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -96,7 +96,7 @@ and 'a rfield = {
 type plvalue_r =
   | PLvSymbol of pqsymbol
   | PLvTuple  of pqsymbol list
-  | PLvMap    of pqsymbol * ptyannot option * pexpr
+  | PLvMap    of pqsymbol * ptyannot option * pexpr list
 
 and plvalue = plvalue_r located
 
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index f002a157c..c342b5828 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -3028,11 +3028,14 @@ let pp_ovdecl ppe fmt ov =
 let pp_pvdecl ppe fmt v =
   Format.fprintf fmt "%s : %a" v.v_name (pp_type ppe) v.v_type
 
-let pp_funsig ppe fmt fs =
-  Format.fprintf fmt "@[<hov 2>proc %s(%a) :@ %a@]"
-    fs.fs_name
-    (pp_list ", " (pp_ovdecl ppe)) fs.fs_anames
-    (pp_type ppe) fs.fs_ret
+let pp_funsig ?(with_sig = true) ppe fmt fs =
+  if with_sig then
+    Format.fprintf fmt "@[<hov 2>proc %s(%a) :@ %a@]"
+      fs.fs_name
+      (pp_list ", " (pp_ovdecl ppe)) fs.fs_anames
+      (pp_type ppe) fs.fs_ret
+  else
+    Format.fprintf fmt "@[<hov 2>proc %s@]" fs.fs_name
 
 let pp_sigitem moi_opt ppe fmt (Tys_function fs) =
   Format.fprintf fmt "@[<hov 2>%a@ %t@]"
@@ -3189,6 +3192,10 @@ and pp_moditem ppe fmt (p, i) =
           Format.fprintf fmt "@[<hov 2>return@ @[%a@];@]" (pp_expr ppe) e
     in
 
+    let pp_funsig ppe fmt fun_ =
+      let with_sig = match fun_.f_def with FBalias _ -> false | _ -> true in
+      Format.fprintf fmt "%a" (pp_funsig ~with_sig ppe) fun_.f_sig in
+
     let pp_fundef ppe fmt fun_ =
       match fun_.f_def with
       | (FBdef def) ->
@@ -3210,9 +3217,7 @@ and pp_moditem ppe fmt (p, i) =
           Format.fprintf fmt "?ABSTRACT?"
     in
 
-    Format.fprintf fmt "@[<v>%a = %a@]"
-      (pp_funsig ppe) f.f_sig
-      (pp_fundef ppe) f
+    Format.fprintf fmt "@[<v>%a = %a@]" (pp_funsig ppe) f (pp_fundef ppe) f
 
 let pp_modexp ppe fmt (mp, me) =
   Format.fprintf fmt "%a." (pp_modexp ppe) (mp, me)
diff --git a/src/ecTyping.ml b/src/ecTyping.ml
index 3c4541537..a5511aefa 100644
--- a/src/ecTyping.ml
+++ b/src/ecTyping.ml
@@ -2709,11 +2709,12 @@ and translvalue ue (env : EcEnv.env) lvalue =
       let ty = ttuple (List.map snd xs) in
       Lval (LvTuple xs), ty
 
-  | PLvMap (x, tvi, e) ->
+  | PLvMap (x, tvi, es) ->
       let tvi = tvi |> omap (transtvi env ue) in
       let codomty = UE.fresh ue in
       let pv, xty = trans_pv env x in
-      let e, ety = transexp env `InProc ue e in
+      let e, ety = List.split (List.map (transexp env `InProc ue) es) in
+      let e, ety = e_tuple e, ttuple ety in
       let name = ([], EcCoreLib.s_set) in
       let esig = [xty; ety; codomty] in
       let ops = select_exp_op env `InProc None name ue tvi esig in