diff options
| -rw-r--r-- | vernac/ppvernac.ml | 7 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 150 |
2 files changed, 92 insertions, 65 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f91983d31c..5cffc39839 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1083,7 +1083,12 @@ let string_of_definition_object_kind = let open Decls in function match n, nbidi, l with | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l | _, Some 0, l -> spc () ++ str"|" ++ print_arguments n None l - | _, _, [] -> mt() + | None, None, [] -> mt() + | _, _, [] -> + let dummy = {name=Anonymous; recarg_like=false; + notation_scope=None; implicit_status=Impargs.NotImplicit} + in + print_arguments n nbidi [dummy] | n, nbidi, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index fa534a0936..358c40bdb0 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -17,7 +17,6 @@ open CErrors open Util open CAst open Names -open Nameops open Termops open Declarations open Environ @@ -30,7 +29,7 @@ open Printer open Printmod open Context.Rel.Declaration -(* module RelDecl = Context.Rel.Declaration *) +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { @@ -138,11 +137,6 @@ let print_impargs_list prefix l = then print_one_impargs_list imps else [str "No implicit arguments"]))])]) l) -let print_renames_list prefix l = - if List.is_empty l then [] else - [add_colon prefix ++ str "Arguments are renamed to " ++ - hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] - let need_expansion impl ref = let typ, _ = Typeops.type_of_global_in_context (Global.env ()) ref in let ctx = Term.prod_assum typ in @@ -163,19 +157,6 @@ let print_impargs ref = else [str "No implicit arguments"])) (*********************) -(** Printing Scopes *) - -let print_argument_scopes prefix = function - | [Some sc] -> - [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] - | l when not (List.for_all Option.is_empty l) -> - [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ - pr_sequence (function Some sc -> str sc | None -> str "_") l ++ - str "]")] - | _ -> [] - -(*********************) (** Printing Opacity *) type opacity = @@ -260,13 +241,85 @@ let print_primitive ref = print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record | _ -> [] -let print_name_infos ref = - let impls = implicits_of_global ref in +let needs_extra_scopes ref scopes = + let open Constr in + let rec aux env t = function + | [] -> false + | _::scopes -> match kind (Reduction.whd_all env t) with + | Prod (na,dom,codom) -> aux (push_rel (RelDecl.LocalAssum (na,dom)) env) codom scopes + | _ -> true + in + let env = Global.env() in + let ty, _ctx = Typeops.type_of_global_in_context env ref in + aux env ty scopes + +let implicit_kind_of_status = function + | None -> Anonymous, NotImplicit + | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit + +let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit + +let rec main_implicits i renames recargs scopes impls = + if renames = [] && recargs = [] && scopes = [] && impls = [] then [] + else + let recarg_like, recargs = match recargs with + | j :: recargs when i = j -> true, recargs + | _ -> false, recargs + in + let (name, implicit_status) = + match renames, impls with + | _, (Some _ as i) :: _ -> implicit_kind_of_status i + | name::_, _ -> (name,NotImplicit) + | [], (None::_ | []) -> (Anonymous, NotImplicit) + in + let notation_scope = match scopes with + | scope :: _ -> Option.map CAst.make scope + | [] -> None + in + let status = {Vernacexpr.implicit_status; name; recarg_like; notation_scope} in + let tl = function [] -> [] | _::tl -> tl in + (* recargs is special -> tl handled above *) + let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in + if is_dummy status && rest = [] + then [] (* we may have a trail of dummies due to eg "clear scopes" *) + else status :: rest + +let print_arguments ref = + let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in + let flags, recargs, nargs_for_red = + let open Reductionops.ReductionBehaviour in + match get ref with + | None -> [], [], None + | Some NeverUnfold -> [`ReductionNeverUnfold], [], None + | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs + | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs + in + let flags, renames = match Arguments_renaming.arguments_names ref with + | exception Not_found -> flags, [] + | [] -> flags, [] + | renames -> `Rename::flags, renames + in let scopes = Notation.find_arguments_scope ref in - let renames = - try Arguments_renaming.arguments_names ref with Not_found -> [] in + let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in + let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in + let impls, moreimpls = match impls with + | (_, impls) :: rest -> impls, rest + | [] -> assert false + in + let impls = main_implicits 0 renames recargs scopes impls in + let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in + let bidi = Pretyping.get_bidirectionality_hint ref in + if impls = [] && moreimpls = [] && nargs_for_red = None && bidi = None && flags = [] then [] + else + let open Constrexpr in + let open Vernacexpr in + [Ppvernac.pr_vernac_expr + (VernacArguments (CAst.make (AN qid), impls, moreimpls, nargs_for_red, bidi, flags))] + +let print_name_infos ref = let type_info_for_implicit = - if need_expansion (select_impargs_size 0 impls) ref then + if need_expansion (select_impargs_size 0 (implicits_of_global ref)) ref then (* Need to reduce since implicits are computed with products flattened *) [str "Expanded type for implicit arguments"; print_ref true ref None; blankline] @@ -275,42 +328,15 @@ let print_name_infos ref = print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ - print_renames_list (mt()) renames @ - print_impargs_list (mt()) impls @ - print_argument_scopes (mt()) scopes @ + print_arguments ref @ print_if_is_coercion ref -let print_id_args_data test pr id l = - if List.exists test l then - pr (str "For " ++ Id.print id) l - else - [] - -let print_args_data_of_inductive_ids get test pr sp mipv = - List.flatten (Array.to_list (Array.mapi - (fun i mip -> - print_id_args_data test pr mip.mind_typename (get (GlobRef.IndRef (sp,i))) @ - List.flatten (Array.to_list (Array.mapi - (fun j idc -> - print_id_args_data test pr idc (get (GlobRef.ConstructRef ((sp,i),j+1)))) - mip.mind_consnames))) - mipv)) - -let print_inductive_implicit_args = - print_args_data_of_inductive_ids - implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l))) - print_impargs_list - -let print_inductive_renames = - print_args_data_of_inductive_ids - (fun r -> - try Arguments_renaming.arguments_names r with Not_found -> []) - ((!=) Anonymous) - print_renames_list - -let print_inductive_argument_scopes = - print_args_data_of_inductive_ids - Notation.find_arguments_scope (Option.has_some) print_argument_scopes +let print_inductive_args sp mipv = + let flatmapi f v = List.flatten (Array.to_list (Array.mapi f v)) in + flatmapi + (fun i mip -> print_arguments (GlobRef.IndRef (sp,i)) @ + flatmapi (fun j _ -> print_arguments (GlobRef.ConstructRef ((sp,i),j+1))) + mip.mind_consnames) mipv let print_bidi_hints gr = match Pretyping.get_bidirectionality_hint gr with @@ -536,9 +562,7 @@ let gallina_print_inductive sp udecl = pr_mutual_inductive_body env sp mib udecl ++ with_line_skip (print_primitive_record mib.mind_finite mipv mib.mind_record @ - print_inductive_renames sp mipv @ - print_inductive_implicit_args sp mipv @ - print_inductive_argument_scopes sp mipv) + print_inductive_args sp mipv) let print_named_decl env sigma id = gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () @@ -860,13 +884,11 @@ let print_about_any ?loc env sigma k udecl = maybe_error_reject_univ_decl k udecl; match k with | Term ref -> - let rb = Reductionops.ReductionBehaviour.print ref in Dumpglob.add_glob ?loc ref; pr_infos_list (print_ref false ref udecl :: blankline :: print_polymorphism ref @ print_name_infos ref @ - (if Pp.ismt rb then [] else [rb]) @ print_opacity ref @ print_bidi_hints ref @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) |