diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 51 |
1 files changed, 35 insertions, 16 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index ffe376e0..8d9dd881 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -537,9 +537,9 @@ let doc_typquant_items ctx delimit (TypQ_aux (tq,_)) = let doc_typquant_items_separate ctx delimit (TypQ_aux (tq,_)) = match tq with | TypQ_tq qis -> - separate_opt space (doc_quant_item_id ctx delimit) qis, - separate_opt space (doc_quant_item_constr ctx delimit) qis - | TypQ_no_forall -> empty, empty + Util.map_filter (doc_quant_item_id ctx delimit) qis, + Util.map_filter (doc_quant_item_constr ctx delimit) qis + | TypQ_no_forall -> [], [] let doc_typquant ctx (TypQ_aux(tq,_)) typ = match tq with | TypQ_tq ((_ :: _) as qs) -> @@ -1485,14 +1485,6 @@ let merge_kids_atoms pats = let gone,map,_ = List.fold_left try_eliminate (KidSet.empty, KBindings.empty, KidSet.empty) pats in gone,map -let doc_binder ctxt (P_aux (p,ann) as pat, typ) = - let env = env_of_annot ann in - let exp_typ = Env.expand_synonyms env typ in - match p with - | P_id id - | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) -> - parens (separate space [doc_id id; colon; doc_typ ctxt typ]) - | _ -> squote ^^ parens (separate space [doc_pat ctxt true (pat, exp_typ); colon; doc_typ ctxt typ]) let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in @@ -1516,22 +1508,48 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = been replaced by one of the term-level arguments is bound. *) let quantspp, constrspp = doc_typquant_items_separate ctxt braces tq in let exp = List.fold_left (fun body f -> f body) (bind exp) binds in - let patspp = separate_map space (doc_binder ctxt) pats in - let atom_constr_pp = separate_opt space (atom_constraint ctxt) pats in + let used_a_pattern = ref false in + let doc_binder (P_aux (p,ann) as pat, typ) = + let env = env_of_annot ann in + let exp_typ = Env.expand_synonyms env typ in + match p with + | P_id id + | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) -> + parens (separate space [doc_id id; colon; doc_typ ctxt typ]) + | _ -> + (used_a_pattern := true; + squote ^^ parens (separate space [doc_pat ctxt true (pat, exp_typ); colon; doc_typ ctxt typ])) + in + let patspp = separate_map space doc_binder pats in + let atom_constrs = Util.map_filter (atom_constraint ctxt) pats in + let atom_constr_pp = separate space atom_constrs in let retpp = if effectful eff then string "M" ^^ space ^^ parens (doc_typ ctxt ret_typ) else doc_typ ctxt ret_typ in + let idpp = doc_id id in + (* Work around Coq bug 7975 about pattern binders followed by implicit arguments *) + let implicitargs = + if !used_a_pattern && List.length constrspp + List.length atom_constrs > 0 then + separate space + ([string "Arguments"; idpp;] @ + List.map (fun _ -> string "{_}") quantspp @ + List.map (fun _ -> string "_") pats @ + List.map (fun _ -> string "{_}") constrspp @ + List.map (fun _ -> string "{_}") atom_constrs) + ^^ dot + else empty + in let _ = match guard with | None -> () | _ -> raise (Reporting_basic.err_unreachable l "guarded pattern expression should have been rewritten before pretty-printing") in group (prefix 3 1 - (separate space [doc_id id; quantspp; patspp; constrspp; atom_constr_pp] ^/^ + (separate space ([idpp] @ quantspp @ [patspp] @ constrspp @ [atom_constr_pp]) ^/^ colon ^^ space ^^ retpp ^^ coloneq) - (doc_fun_body ctxt exp ^^ dot)) + (doc_fun_body ctxt exp ^^ dot)) ^/^ implicitargs let get_id = function | [] -> failwith "FD_function with empty list" @@ -1660,7 +1678,8 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) = let arg_typs_pp = separate space (List.map doc_typ' typs) in let ret_typ_pp = doc_typ empty_ctxt ret_ty in let tyvars_pp, constrs_pp = doc_typquant_items_separate empty_ctxt braces tqs in - string "forall" ^/^ tyvars_pp ^/^ arg_typs_pp ^/^ constrs_pp ^^ comma ^/^ ret_typ_pp + string "forall" ^/^ separate space tyvars_pp ^/^ + arg_typs_pp ^/^ separate space constrs_pp ^^ comma ^/^ ret_typ_pp | _ -> doc_typschm empty_ctxt true ts let doc_val_spec unimplemented (VS_aux (VS_val_spec(tys,id,_,_),ann)) = |