Fix pretty-printing of function clauses with wildcards for Lem

Before, wildcards sometimes ended up in the arguments to the function call on
the RHS, in particular when using vector patterns (which implicitly introduce
wildcards for the order and index parameters).

1 files changed, 22 insertions, 2 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 673c286b..f3fe13cb 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -270,6 +270,17 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w
       | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats))
      | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*)
 
+let rec pat_has_wildcard (P_aux (p,_)) = match p with
+  | P_app (_, pats) -> List.exists pat_has_wildcard pats
+  | P_lit _ -> false
+  | P_wild -> true
+  | P_id _ -> false
+  | P_as (pat,_) -> pat_has_wildcard pat
+  | P_typ (_,pat) -> pat_has_wildcard pat
+  | P_vector pats -> true (* Vector patterns are pretty-printed with underscores for order and index *)
+  | P_vector_concat pats -> true
+  | P_tup pats -> List.exists pat_has_wildcard pats
+
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
@@ -1068,12 +1079,21 @@ let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot))
                let auxiliary_functions = 
                   auxiliary_functions ^^ hardline ^^ hardline ^^
                     doc_fundef_lem regtypes (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in
+               let bind_wild_pats idx (P_aux (p,a)) =
+                 if pat_has_wildcard (P_aux (p,a))
+                 then P_aux (P_as (P_aux (p,a), Id_aux (Id ("arg" ^ string_of_int idx),l)),a)
+                 else P_aux (p,a) in
+               let bound_argspat = List.mapi bind_wild_pats argspat in
+               let bound_pat = P_aux (P_app (Id_aux (Id ctor,l),bound_argspat),pannot) in
+               let argsexp = List.map (fun (P_aux (p,a)) -> match p with
+                 | P_as (p,id) -> P_aux (P_id id,a)
+                 | _ -> P_aux (p,a)) bound_argspat in
                let clauses =
                  clauses ^^ (break 1) ^^
                    (separate space
-                      [pipe;doc_pat_lem regtypes false pat;arrow;
+                      [pipe;doc_pat_lem regtypes false bound_pat;arrow;
                        string aux_fname;
-                       doc_pat_lem regtypes true (P_aux (P_tup argspat, pannot))]) in
+                       doc_pat_lem regtypes true (P_aux (P_tup argsexp, pannot))]) in
                (already_used_fnames,auxiliary_functions,clauses)
           ) (StringSet.empty,empty,empty) fcls in