diff options
| -rw-r--r-- | src/pretty_print_lem.ml | 24 |
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 |