From c67847189601cf360e9ee565ef3c1f096abd5fed Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Oct 2019 15:46:45 +0100 Subject: Move Arguments implementation to its own file (from vernacentries) --- vernac/comArguments.ml | 306 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/comArguments.mli | 19 +++ vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 295 +--------------------------------------------- vernac/vernacexpr.ml | 23 +++- 5 files changed, 346 insertions(+), 298 deletions(-) create mode 100644 vernac/comArguments.ml create mode 100644 vernac/comArguments.mli diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml new file mode 100644 index 0000000000..737e0427ec --- /dev/null +++ b/vernac/comArguments.ml @@ -0,0 +1,306 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Pretyping.clear_bidirectionality_hint gr + | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs + +let load_bidi_hints _ r = + cache_bidi_hints r + +let subst_bidi_hints (subst, (gr, ohint as orig)) = + let gr' = Globnames.subst_global_reference subst gr in + if gr == gr' then orig else (gr', ohint) + +let discharge_bidi_hints (_name, (gr, ohint)) = + if Globnames.isVarRef gr && Lib.is_in_section gr then None + else + let vars = Lib.variable_section_segment_of_reference gr in + let n = List.length vars in + Some (gr, Option.map ((+) n) ohint) + +let inBidiHints = + let open Libobject in + declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with + load_function = load_bidi_hints; + cache_function = cache_bidi_hints; + classify_function = (fun o -> Substitute o); + subst_function = subst_bidi_hints; + discharge_function = discharge_bidi_hints; + } + + +let warn_arguments_assert = + CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + Pp.(fun sr -> + strbrk "This command is just asserting the names of arguments of " ++ + Printer.pr_global sr ++ strbrk". If this is what you want add " ++ + strbrk "': assert' to silence the warning. If you want " ++ + strbrk "to clear implicit arguments add ': clear implicits'. " ++ + strbrk "If you want to clear notation scopes add ': clear scopes'") + +(* [nargs_for_red] is the number of arguments required to trigger reduction, + [args] is the main list of arguments statuses, + [more_implicits] is a list of extra lists of implicit statuses *) +let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags = + let env = Global.env () in + let sigma = Evd.from_env env in + let assert_flag = List.mem `Assert flags in + let rename_flag = List.mem `Rename flags in + let clear_scopes_flag = List.mem `ClearScopes flags in + let extra_scopes_flag = List.mem `ExtraScopes flags in + let clear_implicits_flag = List.mem `ClearImplicits flags in + let default_implicits_flag = List.mem `DefaultImplicits flags in + let never_unfold_flag = List.mem `ReductionNeverUnfold flags in + let nomatch_flag = List.mem `ReductionDontExposeCase flags in + let clear_bidi_hint = List.mem `ClearBidiHint flags in + + let err_incompat x y = + CErrors.user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in + + if assert_flag && rename_flag then + err_incompat "assert" "rename"; + if clear_scopes_flag && extra_scopes_flag then + err_incompat "clear scopes" "extra scopes"; + if clear_implicits_flag && default_implicits_flag then + err_incompat "clear implicits" "default implicits"; + + let sr = smart_global reference in + let inf_names = + let ty, _ = Typeops.type_of_global_in_context env sr in + Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) + in + let prev_names = + try Arguments_renaming.arguments_names sr with Not_found -> inf_names + in + let num_args = List.length inf_names in + assert (Int.equal num_args (List.length prev_names)); + + let names_of args = List.map (fun a -> a.name) args in + + (* Checks *) + + let err_extra_args names = + CErrors.user_err ~hdr:"vernac_declare_arguments" + Pp.(strbrk "Extra arguments: " ++ + prlist_with_sep pr_comma Name.print names ++ str ".") + in + let err_missing_args names = + CErrors.user_err ~hdr:"vernac_declare_arguments" + Pp.(strbrk "The following arguments are not declared: " ++ + prlist_with_sep pr_comma Name.print names ++ str ".") + in + + let rec check_extra_args extra_args = + match extra_args with + | [] -> () + | { notation_scope = None } :: _ -> + CErrors.user_err Pp.(str"Extra arguments should specify a scope.") + | { notation_scope = Some _ } :: args -> check_extra_args args + in + + let args, scopes = + let scopes = List.map (fun { notation_scope = s } -> s) args in + if List.length args > num_args then + let args, extra_args = List.chop num_args args in + if extra_scopes_flag then + (check_extra_args extra_args; (args, scopes)) + else err_extra_args (names_of extra_args) + else args, scopes + in + + if Option.cata (fun n -> n > num_args) false nargs_for_red then + CErrors.user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); + + if Option.cata (fun n -> n > num_args) false nargs_before_bidi then + CErrors.user_err Pp.(str "The \"&\" modifier should be put before any extra scope."); + + let scopes_specified = List.exists Option.has_some scopes in + + if scopes_specified && clear_scopes_flag then + CErrors.user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); + + let names = List.map (fun { name } -> name) args in + let names = names :: List.map (List.map fst) more_implicits in + + let rename_flag_required = ref false in + let example_renaming = ref None in + let save_example_renaming renaming = + rename_flag_required := !rename_flag_required + || not (Name.equal (fst renaming) Anonymous); + if Option.is_empty !example_renaming then + example_renaming := Some renaming + in + + let rec names_union names1 names2 = + match names1, names2 with + | [], [] -> [] + | _ :: _, [] -> names1 + | [], _ :: _ -> names2 + | (Name _ as name) :: names1, Anonymous :: names2 + | Anonymous :: names1, (Name _ as name) :: names2 -> + name :: names_union names1 names2 + | name1 :: names1, name2 :: names2 -> + if Name.equal name1 name2 then + name1 :: names_union names1 names2 + else CErrors.user_err Pp.(str "Argument lists should agree on the names they provide.") + in + + let names = List.fold_left names_union [] names in + + let rec rename prev_names names = + match prev_names, names with + | [], [] -> [] + | [], _ :: _ -> err_extra_args names + | _ :: _, [] when assert_flag -> + (* Error messages are expressed in terms of original names, not + renamed ones. *) + err_missing_args (List.lastn (List.length prev_names) inf_names) + | _ :: _, [] -> prev_names + | prev :: prev_names, Anonymous :: names -> + prev :: rename prev_names names + | prev :: prev_names, (Name id as name) :: names -> + if not (Name.equal prev name) then save_example_renaming (prev,name); + name :: rename prev_names names + in + + let names = rename prev_names names in + let renaming_specified = Option.has_some !example_renaming in + + if !rename_flag_required && not rename_flag then begin + let msg = let open Pp in + match !example_renaming with + | None -> + strbrk "To rename arguments the \"rename\" flag must be specified." + | Some (o,n) -> + strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ + strbrk " into " ++ Name.print n ++ str "." + in CErrors.user_err ~hdr:"vernac_declare_arguments" msg + end; + + let duplicate_names = + List.duplicates Name.equal (List.filter ((!=) Anonymous) names) + in + if not (List.is_empty duplicate_names) then begin + CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++ + prlist_with_sep pr_comma Name.print duplicate_names) + end; + + let implicits = + List.map (fun { name; implicit_status = i } -> (name,i)) args + in + let implicits = implicits :: more_implicits in + + let implicits = List.map (List.map snd) implicits in + let implicits_specified = match implicits with + | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l + | _ -> true in + + if implicits_specified && clear_implicits_flag then + CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); + + if implicits_specified && default_implicits_flag then + CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); + + let rargs = + Util.List.map_filter (function (n, true) -> Some n | _ -> None) + (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) + in + + let red_behavior = + let open Reductionops.ReductionBehaviour in + match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with + | true, false, [], None -> Some NeverUnfold + | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" + | true, _, _::_, _ -> err_incompat "simpl never" "!" + | true, _, _, Some _ -> err_incompat "simpl never" "/" + | false, false, [], None -> None + | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; + recargs = rargs; + }) + | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; + recargs = rargs; + }) + in + + + let red_modifiers_specified = Option.has_some red_behavior in + + let bidi_hint_specified = Option.has_some nargs_before_bidi in + + if bidi_hint_specified && clear_bidi_hint then + err_incompat "clear bidirectionality hint" "&"; + + + (* Actions *) + + if renaming_specified then begin + Arguments_renaming.rename_arguments section_local sr names + end; + + if scopes_specified || clear_scopes_flag then begin + let scopes = List.map (Option.map (fun {loc;v=k} -> + try ignore (Notation.find_scope k); k + with CErrors.UserError _ -> + Notation.find_delimiters_scope ?loc k)) scopes + in + Notation.declare_arguments_scope section_local (smart_global reference) scopes + end; + + if implicits_specified || clear_implicits_flag then + Impargs.set_implicits section_local (smart_global reference) implicits; + + if default_implicits_flag then + Impargs.declare_implicits section_local (smart_global reference); + + if red_modifiers_specified then begin + match sr with + | GlobRef.ConstRef _ -> + Reductionops.ReductionBehaviour.set + ~local:section_local sr (Option.get red_behavior) + + | _ -> + CErrors.user_err + Pp.(strbrk "Modifiers of the behavior of the simpl tactic "++ + strbrk "are relevant for constants only.") + end; + + if bidi_hint_specified then begin + let n = Option.get nargs_before_bidi in + if section_local then + Pretyping.add_bidirectionality_hint sr n + else + Lib.add_anonymous_leaf (inBidiHints (sr, Some n)) + end; + + if clear_bidi_hint then begin + if section_local then + Pretyping.clear_bidirectionality_hint sr + else + Lib.add_anonymous_leaf (inBidiHints (sr, None)) + end; + + if not (renaming_specified || + implicits_specified || + scopes_specified || + red_modifiers_specified || + bidi_hint_specified) && (List.is_empty flags) then + warn_arguments_assert sr diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli new file mode 100644 index 0000000000..f78e01a11f --- /dev/null +++ b/vernac/comArguments.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Libnames.qualid Constrexpr.or_by_notation + -> Vernacexpr.vernac_argument_status list + -> (Names.Name.t * Impargs.implicit_kind) list list + -> int option + -> int option + -> Vernacexpr.arguments_modifier list + -> unit diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 956b56e256..102da20257 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -38,6 +38,7 @@ Assumptions Mltop Topfmt Loadpath +ComArguments Vernacentries Vernacstate Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 684d8a3d90..4c7332f011 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -15,7 +15,6 @@ open CErrors open CAst open Util open Names -open Nameops open Tacmach open Constrintern open Prettyp @@ -448,9 +447,6 @@ let vernac_bind_scope ~module_local sc cll = let vernac_open_close_scope ~section_local (b,s) = Notation.open_close_scope (section_local,b,s) -let vernac_arguments_scope ~section_local r scl = - Notation.declare_arguments_scope section_local (smart_global r) scl - let vernac_infix ~atts = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in Metasyntax.add_infix ~local:module_local deprecation (Global.env()) @@ -655,7 +651,7 @@ let vernac_record ~template udecl cum k poly finite records = let cumulative = should_treat_as_cumulative cum poly in let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with - | None -> add_prefix "Build_" id.v + | None -> Nameops.add_prefix "Build_" id.v | Some lid -> let () = Dumpglob.dump_definition lid false "constr" in lid.v @@ -1213,292 +1209,6 @@ let vernac_syntactic_definition ~atts lid x compat = Dumpglob.dump_definition lid false "syndef"; Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat -let cache_bidi_hints (_name, (gr, ohint)) = - match ohint with - | None -> Pretyping.clear_bidirectionality_hint gr - | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs - -let load_bidi_hints _ r = - cache_bidi_hints r - -let subst_bidi_hints (subst, (gr, ohint as orig)) = - let gr' = subst_global_reference subst gr in - if gr == gr' then orig else (gr', ohint) - -let discharge_bidi_hints (_name, (gr, ohint)) = - if isVarRef gr && Lib.is_in_section gr then None - else - let vars = Lib.variable_section_segment_of_reference gr in - let n = List.length vars in - Some (gr, Option.map ((+) n) ohint) - -let inBidiHints = - let open Libobject in - declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with - load_function = load_bidi_hints; - cache_function = cache_bidi_hints; - classify_function = (fun o -> Substitute o); - subst_function = subst_bidi_hints; - discharge_function = discharge_bidi_hints; - } - - -let warn_arguments_assert = - CWarnings.create ~name:"arguments-assert" ~category:"vernacular" - (fun sr -> - strbrk "This command is just asserting the names of arguments of " ++ - pr_global sr ++ strbrk". If this is what you want add " ++ - strbrk "': assert' to silence the warning. If you want " ++ - strbrk "to clear implicit arguments add ': clear implicits'. " ++ - strbrk "If you want to clear notation scopes add ': clear scopes'") - -(* [nargs_for_red] is the number of arguments required to trigger reduction, - [args] is the main list of arguments statuses, - [more_implicits] is a list of extra lists of implicit statuses *) -let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags = - let env = Global.env () in - let sigma = Evd.from_env env in - let assert_flag = List.mem `Assert flags in - let rename_flag = List.mem `Rename flags in - let clear_scopes_flag = List.mem `ClearScopes flags in - let extra_scopes_flag = List.mem `ExtraScopes flags in - let clear_implicits_flag = List.mem `ClearImplicits flags in - let default_implicits_flag = List.mem `DefaultImplicits flags in - let never_unfold_flag = List.mem `ReductionNeverUnfold flags in - let nomatch_flag = List.mem `ReductionDontExposeCase flags in - let clear_bidi_hint = List.mem `ClearBidiHint flags in - - let err_incompat x y = - user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in - - if assert_flag && rename_flag then - err_incompat "assert" "rename"; - if clear_scopes_flag && extra_scopes_flag then - err_incompat "clear scopes" "extra scopes"; - if clear_implicits_flag && default_implicits_flag then - err_incompat "clear implicits" "default implicits"; - - let sr = smart_global reference in - let inf_names = - let ty, _ = Typeops.type_of_global_in_context env sr in - Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) - in - let prev_names = - try Arguments_renaming.arguments_names sr with Not_found -> inf_names - in - let num_args = List.length inf_names in - assert (Int.equal num_args (List.length prev_names)); - - let names_of args = List.map (fun a -> a.name) args in - - (* Checks *) - - let err_extra_args names = - user_err ~hdr:"vernac_declare_arguments" - (strbrk "Extra arguments: " ++ - prlist_with_sep pr_comma Name.print names ++ str ".") - in - let err_missing_args names = - user_err ~hdr:"vernac_declare_arguments" - (strbrk "The following arguments are not declared: " ++ - prlist_with_sep pr_comma Name.print names ++ str ".") - in - - let rec check_extra_args extra_args = - match extra_args with - | [] -> () - | { notation_scope = None } :: _ -> - user_err Pp.(str"Extra arguments should specify a scope.") - | { notation_scope = Some _ } :: args -> check_extra_args args - in - - let args, scopes = - let scopes = List.map (fun { notation_scope = s } -> s) args in - if List.length args > num_args then - let args, extra_args = List.chop num_args args in - if extra_scopes_flag then - (check_extra_args extra_args; (args, scopes)) - else err_extra_args (names_of extra_args) - else args, scopes - in - - if Option.cata (fun n -> n > num_args) false nargs_for_red then - user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); - - if Option.cata (fun n -> n > num_args) false nargs_before_bidi then - user_err Pp.(str "The \"&\" modifier should be put before any extra scope."); - - let scopes_specified = List.exists Option.has_some scopes in - - if scopes_specified && clear_scopes_flag then - user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); - - let names = List.map (fun { name } -> name) args in - let names = names :: List.map (List.map fst) more_implicits in - - let rename_flag_required = ref false in - let example_renaming = ref None in - let save_example_renaming renaming = - rename_flag_required := !rename_flag_required - || not (Name.equal (fst renaming) Anonymous); - if Option.is_empty !example_renaming then - example_renaming := Some renaming - in - - let rec names_union names1 names2 = - match names1, names2 with - | [], [] -> [] - | _ :: _, [] -> names1 - | [], _ :: _ -> names2 - | (Name _ as name) :: names1, Anonymous :: names2 - | Anonymous :: names1, (Name _ as name) :: names2 -> - name :: names_union names1 names2 - | name1 :: names1, name2 :: names2 -> - if Name.equal name1 name2 then - name1 :: names_union names1 names2 - else user_err Pp.(str "Argument lists should agree on the names they provide.") - in - - let names = List.fold_left names_union [] names in - - let rec rename prev_names names = - match prev_names, names with - | [], [] -> [] - | [], _ :: _ -> err_extra_args names - | _ :: _, [] when assert_flag -> - (* Error messages are expressed in terms of original names, not - renamed ones. *) - err_missing_args (List.lastn (List.length prev_names) inf_names) - | _ :: _, [] -> prev_names - | prev :: prev_names, Anonymous :: names -> - prev :: rename prev_names names - | prev :: prev_names, (Name id as name) :: names -> - if not (Name.equal prev name) then save_example_renaming (prev,name); - name :: rename prev_names names - in - - let names = rename prev_names names in - let renaming_specified = Option.has_some !example_renaming in - - if !rename_flag_required && not rename_flag then begin - let msg = - match !example_renaming with - | None -> - strbrk "To rename arguments the \"rename\" flag must be specified." - | Some (o,n) -> - strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ - strbrk " into " ++ Name.print n ++ str "." - in user_err ~hdr:"vernac_declare_arguments" msg - end; - - let duplicate_names = - List.duplicates Name.equal (List.filter ((!=) Anonymous) names) - in - if not (List.is_empty duplicate_names) then begin - let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in - user_err (strbrk "Some argument names are duplicated: " ++ duplicates) - end; - - let implicits = - List.map (fun { name; implicit_status = i } -> (name,i)) args - in - let implicits = implicits :: more_implicits in - - let implicits = List.map (List.map snd) implicits in - let implicits_specified = match implicits with - | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l - | _ -> true in - - if implicits_specified && clear_implicits_flag then - user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); - - if implicits_specified && default_implicits_flag then - user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); - - let rargs = - Util.List.map_filter (function (n, true) -> Some n | _ -> None) - (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) - in - - let red_behavior = - let open Reductionops.ReductionBehaviour in - match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with - | true, false, [], None -> Some NeverUnfold - | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" - | true, _, _::_, _ -> err_incompat "simpl never" "!" - | true, _, _, Some _ -> err_incompat "simpl never" "/" - | false, false, [], None -> None - | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; - recargs = rargs; - }) - | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; - recargs = rargs; - }) - in - - - let red_modifiers_specified = Option.has_some red_behavior in - - let bidi_hint_specified = Option.has_some nargs_before_bidi in - - if bidi_hint_specified && clear_bidi_hint then - err_incompat "clear bidirectionality hint" "&"; - - - (* Actions *) - - if renaming_specified then begin - Arguments_renaming.rename_arguments section_local sr names - end; - - if scopes_specified || clear_scopes_flag then begin - let scopes = List.map (Option.map (fun {loc;v=k} -> - try ignore (Notation.find_scope k); k - with UserError _ -> - Notation.find_delimiters_scope ?loc k)) scopes - in - vernac_arguments_scope ~section_local reference scopes - end; - - if implicits_specified || clear_implicits_flag then - Impargs.set_implicits section_local (smart_global reference) implicits; - - if default_implicits_flag then - Impargs.declare_implicits section_local (smart_global reference); - - if red_modifiers_specified then begin - match sr with - | GlobRef.ConstRef _ as c -> - Reductionops.ReductionBehaviour.set - ~local:section_local c (Option.get red_behavior) - - | _ -> user_err - (strbrk "Modifiers of the behavior of the simpl tactic "++ - strbrk "are relevant for constants only.") - end; - - if bidi_hint_specified then begin - let n = Option.get nargs_before_bidi in - if section_local then - Pretyping.add_bidirectionality_hint sr n - else - Lib.add_anonymous_leaf (inBidiHints (sr, Some n)) - end; - - if clear_bidi_hint then begin - if section_local then - Pretyping.clear_bidirectionality_hint sr - else - Lib.add_anonymous_leaf (inBidiHints (sr, None)) - end; - - if not (renaming_specified || - implicits_specified || - scopes_specified || - red_modifiers_specified || - bidi_hint_specified) && (List.is_empty flags) then - warn_arguments_assert sr - let default_env () = { Notation_term.ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -2453,7 +2163,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> VtDefault(fun () -> - with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) + with_section_locality ~atts + (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags)) | VernacReserve bl -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b712d7e264..564c55670d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -257,6 +257,17 @@ type vernac_argument_status = { implicit_status : Impargs.implicit_kind; } +type arguments_modifier = + [ `Assert + | `ClearBidiHint + | `ClearImplicits + | `ClearScopes + | `DefaultImplicits + | `ExtraScopes + | `ReductionDontExposeCase + | `ReductionNeverUnfold + | `Rename ] + type extend_name = (* Name of the vernac entry where the tactic is defined, typically found after the VERNAC EXTEND statement in the source. *) @@ -365,16 +376,16 @@ type nonrec vernac_expr = | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * qualid list | VernacHints of string list * Hints.hints_expr - | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * + | VernacSyntacticDefinition of + lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacArguments of qualid or_by_notation * + | VernacArguments of + qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * - (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * + (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * int option (* Number of args to trigger reduction *) * int option (* Number of args before bidirectional typing *) * - [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `ClearBidiHint | - `DefaultImplicits ] list + arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) -- cgit v1.2.3 From ae1eb22a1365a6f477fc328eabf821fd346b5f0b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Oct 2019 16:02:51 +0100 Subject: Doc: index command Arguments with assert --- doc/sphinx/language/gallina-extensions.rst | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f477bf239d..f50cf9340c 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1927,9 +1927,11 @@ Renaming implicit arguments This command is used to redefine the names of implicit arguments. -With the assert flag, ``Arguments`` can be used to assert that a given -object has the expected number of arguments and that these arguments -are named as expected. +.. cmd:: Arguments @qualid {* @name} : assert + :name: Arguments (assert) + + This command is used to assert that a given object has the expected + number of arguments and that these arguments are named as expected. .. example:: (continued) -- cgit v1.2.3 From 215b7e43cba768bfc82914718b159a22797f9d2b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Oct 2019 16:48:21 +0100 Subject: Move prettyp (Print implementation) to vernac/ --- printing/prettyp.ml | 984 ------------------------------------------------ printing/prettyp.mli | 129 ------- printing/printing.mllib | 1 - vernac/prettyp.ml | 984 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/prettyp.mli | 129 +++++++ vernac/vernac.mllib | 1 + 6 files changed, 1114 insertions(+), 1114 deletions(-) delete mode 100644 printing/prettyp.ml delete mode 100644 printing/prettyp.mli create mode 100644 vernac/prettyp.ml create mode 100644 vernac/prettyp.mli diff --git a/printing/prettyp.ml b/printing/prettyp.ml deleted file mode 100644 index c995887f31..0000000000 --- a/printing/prettyp.ml +++ /dev/null @@ -1,984 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* - * on May-June 2006 for implementation of abstraction of pretty-printing of objects. - *) - -open Pp -open CErrors -open Util -open CAst -open Names -open Nameops -open Termops -open Declarations -open Environ -open Impargs -open Libobject -open Libnames -open Globnames -open Recordops -open Printer -open Printmod -open Context.Rel.Declaration - -(* module RelDecl = Context.Rel.Declaration *) -module NamedDecl = Context.Named.Declaration - -type object_pr = { - print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; - print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; - print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; -} - -let gallina_print_module = print_module -let gallina_print_modtype = print_modtype - -(**************) -(** Utilities *) - -let print_closed_sections = ref false - -let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) - -let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l - -let blankline = mt() (* add a blank sentence in the list of infos *) - -let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": " - -let int_or_no n = if Int.equal n 0 then str "no" else int n - -(*******************) -(** Basic printing *) - -let print_basename sp = pr_global (GlobRef.ConstRef sp) - -let print_ref reduce ref udecl = - let env = Global.env () in - let typ, univs = Typeops.type_of_global_in_context env ref in - let inst = Univ.make_abstract_instance univs in - let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in - let sigma = Evd.from_ctx (UState.of_binders bl) in - let typ = EConstr.of_constr typ in - let typ = - if reduce then - let ctx,ccl = Reductionops.splay_prod_assum env sigma typ - in EConstr.it_mkProd_or_LetIn ccl ctx - else typ in - let variance = let open GlobRef in match ref with - | VarRef _ | ConstRef _ -> None - | IndRef (ind,_) | ConstructRef ((ind,_),_) -> - let mind = Environ.lookup_mind ind env in - mind.Declarations.mind_variance - in - let inst = - if Global.is_polymorphic ref - then Printer.pr_universe_instance sigma inst - else mt () - in - let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) - -(********************************) -(** Printing implicit arguments *) - -let pr_impl_name imp = Id.print (name_of_implicit imp) - -let print_impargs_by_name max = function - | [] -> [] - | impls -> - let n = List.length impls in - [hov 0 (str (String.plural n "Argument") ++ spc() ++ - prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ - str (String.conjugate_verb_to_be n) ++ str" implicit" ++ - (if max then strbrk " and maximally inserted" else mt()))] - -let print_one_impargs_list l = - let imps = List.filter is_status_implicit l in - let maximps = List.filter Impargs.maximal_insertion_of imps in - let nonmaximps = List.subtract (=) imps maximps in (* FIXME *) - print_impargs_by_name false nonmaximps @ - print_impargs_by_name true maximps - -let print_impargs_list prefix l = - let l = extract_impargs_data l in - List.flatten (List.map (fun (cond,imps) -> - match cond with - | None -> - List.map (fun pp -> add_colon prefix ++ pp) - (print_one_impargs_list imps) - | Some (n1,n2) -> - [v 2 (prlist_with_sep cut (fun x -> x) - [(if ismt prefix then str "When" else prefix ++ str ", when") ++ - str " applied to " ++ - (if Int.equal n1 n2 then int_or_no n2 else - if Int.equal n1 0 then str "no more than " ++ int n2 - else int n1 ++ str " to " ++ int_or_no n2) ++ - str (String.plural n2 " argument") ++ str ":"; - v 0 (prlist_with_sep cut (fun x -> x) - (if List.exists is_status_implicit imps - 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 - let nprods = List.count is_local_assum ctx in - not (List.is_empty impl) && List.length impl >= nprods && - let _,lastimpl = List.chop nprods impl in - List.exists is_status_implicit lastimpl - -let print_impargs ref = - let ref = Smartlocate.smart_global ref in - let impl = implicits_of_global ref in - let has_impl = not (List.is_empty impl) in - (* Need to reduce since implicits are computed with products flattened *) - pr_infos_list - ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref None; - blankline ] @ - (if has_impl then print_impargs_list (mt()) impl - 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 = - | FullyOpaque - | TransparentMaybeOpacified of Conv_oracle.level - -let opacity env = - function - | GlobRef.VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> - Some(TransparentMaybeOpacified - (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) - | GlobRef.ConstRef cst -> - let cb = Environ.lookup_constant cst env in - (match cb.const_body with - | Undef _ | Primitive _ -> None - | OpaqueDef _ -> Some FullyOpaque - | Def _ -> Some - (TransparentMaybeOpacified - (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) - | _ -> None - -let print_opacity ref = - match opacity (Global.env()) ref with - | None -> [] - | Some s -> - [pr_global ref ++ str " is " ++ - match s with - | FullyOpaque -> str "opaque" - | TransparentMaybeOpacified Conv_oracle.Opaque -> - str "basically transparent but considered opaque for reduction" - | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> - str "transparent" - | TransparentMaybeOpacified (Conv_oracle.Level n) -> - str "transparent (with expansion weight " ++ int n ++ str ")" - | TransparentMaybeOpacified Conv_oracle.Expand -> - str "transparent (with minimal expansion weight)"] - -(*******************) - -let print_if_is_coercion ref = - if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] - -(*******************) -(* *) - -let pr_template_variables = function - | [] -> mt () - | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars - -let print_polymorphism ref = - let poly = Global.is_polymorphic ref in - let template_poly = Global.is_template_polymorphic ref in - let template_checked = Global.is_template_checked ref in - let template_variables = Global.get_template_polymorphic_variables ref in - [ pr_global ref ++ str " is " ++ - (if poly then str "universe polymorphic" - else if template_poly then - (if not template_checked then str "assumed " else mt()) ++ - str "template universe polymorphic " - ++ h 0 (pr_template_variables template_variables) - else str "not universe polymorphic") ] - -let print_type_in_type ref = - let unsafe = Global.is_type_in_type ref in - if unsafe then - [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] - else [] - -let print_primitive_record recflag mipv = function - | PrimRecord _ -> - let eta = match recflag with - | CoFinite | Finite -> str" without eta conversion" - | BiFinite -> str " with eta conversion" - in - [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] - | FakeRecord | NotRecord -> [] - -let print_primitive ref = - match ref with - | GlobRef.IndRef ind -> - let mib,_ = Global.lookup_inductive ind in - 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 scopes = Notation.find_arguments_scope ref in - let renames = - try Arguments_renaming.arguments_names ref with Not_found -> [] in - let type_info_for_implicit = - if need_expansion (select_impargs_size 0 impls) ref then - (* Need to reduce since implicits are computed with products flattened *) - [str "Expanded type for implicit arguments"; - print_ref true ref None; blankline] - else - [] in - 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_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_bidi_hints gr = - match Pretyping.get_bidirectionality_hint gr with - | None -> [] - | Some nargs -> - [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"] - -(*********************) -(* "Locate" commands *) - -type 'a locatable_info = { - locate : qualid -> 'a option; - locate_all : qualid -> 'a list; - shortest_qualid : 'a -> qualid; - name : 'a -> Pp.t; - print : 'a -> Pp.t; - about : 'a -> Pp.t; -} - -type locatable = Locatable : 'a locatable_info -> locatable - -type logical_name = - | Term of GlobRef.t - | Dir of Nametab.GlobDirRef.t - | Syntactic of KerName.t - | ModuleType of ModPath.t - | Other : 'a * 'a locatable_info -> logical_name - | Undefined of qualid - -(** Generic table for objects that are accessible through a name. *) -let locatable_map : locatable String.Map.t ref = ref String.Map.empty - -let register_locatable name f = - locatable_map := String.Map.add name (Locatable f) !locatable_map - -exception ObjFound of logical_name - -let locate_any_name qid = - try Term (Nametab.locate qid) - with Not_found -> - try Syntactic (Nametab.locate_syndef qid) - with Not_found -> - try Dir (Nametab.locate_dir qid) - with Not_found -> - try ModuleType (Nametab.locate_modtype qid) - with Not_found -> - let iter _ (Locatable info) = match info.locate qid with - | None -> () - | Some ans -> raise (ObjFound (Other (ans, info))) - in - try String.Map.iter iter !locatable_map; Undefined qid - with ObjFound obj -> obj - -let pr_located_qualid = function - | Term ref -> - let ref_str = let open GlobRef in match ref with - ConstRef _ -> "Constant" - | IndRef _ -> "Inductive" - | ConstructRef _ -> "Constructor" - | VarRef _ -> "Variable" in - str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) - | Syntactic kn -> - str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) - | Dir dir -> - let s,dir = - let open Nametab in - let open GlobDirRef in match dir with - | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir - | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir - | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir - | DirModule { obj_dir ; _ } -> "Module", obj_dir - in - str s ++ spc () ++ DirPath.print dir - | ModuleType mp -> - str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) - | Other (obj, info) -> info.name obj - | Undefined qid -> - pr_qualid qid ++ spc () ++ str "not a defined object." - -let canonize_ref = let open GlobRef in function - | ConstRef c -> - let kn = Constant.canonical c in - if KerName.equal (Constant.user c) kn then None - else Some (ConstRef (Constant.make1 kn)) - | IndRef (ind,i) -> - let kn = MutInd.canonical ind in - if KerName.equal (MutInd.user ind) kn then None - else Some (IndRef (MutInd.make1 kn, i)) - | ConstructRef ((ind,i),j) -> - let kn = MutInd.canonical ind in - if KerName.equal (MutInd.user ind) kn then None - else Some (ConstructRef ((MutInd.make1 kn, i),j)) - | VarRef _ -> None - -let display_alias = function - | Term r -> - begin match canonize_ref r with - | None -> mt () - | Some r' -> - let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in - spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")" - end - | _ -> mt () - -let locate_term qid = - let expand = function - | TrueGlobal ref -> - Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref - | SynDef kn -> - Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn - in - List.map expand (Nametab.locate_extended_all qid) - -let locate_module qid = - let all = Nametab.locate_extended_all_dir qid in - let map dir = let open Nametab.GlobDirRef in match dir with - | DirModule { Nametab.obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp) - | DirOpenModule _ -> Some (Dir dir, qid) - | _ -> None - in - List.map_filter map all - -let locate_modtype qid = - let all = Nametab.locate_extended_all_modtype qid in - let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in - let modtypes = List.map map all in - (* Don't forget the opened module types: they are not part of the same name tab. *) - let all = Nametab.locate_extended_all_dir qid in - let map dir = let open Nametab.GlobDirRef in match dir with - | DirOpenModtype _ -> Some (Dir dir, qid) - | _ -> None - in - modtypes @ List.map_filter map all - -let locate_other s qid = - let Locatable info = String.Map.find s !locatable_map in - let ans = info.locate_all qid in - let map obj = (Other (obj, info), info.shortest_qualid obj) in - List.map map ans - -type locatable_kind = -| LocTerm -| LocModule -| LocOther of string -| LocAny - -let print_located_qualid name flags qid = - let located = match flags with - | LocTerm -> locate_term qid - | LocModule -> locate_modtype qid @ locate_module qid - | LocOther s -> locate_other s qid - | LocAny -> - locate_term qid @ - locate_modtype qid @ - locate_module qid @ - String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map [] - in - match located with - | [] -> - let (dir,id) = repr_qualid qid in - if DirPath.is_empty dir then - str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id - else - str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid - | l -> - prlist_with_sep fnl - (fun (o,oqid) -> - hov 2 (pr_located_qualid o ++ - (if not (qualid_eq oqid qid) then - spc() ++ str "(shorter name to refer to it in current context is " - ++ pr_qualid oqid ++ str")" - else mt ()) ++ - display_alias o)) l - -let print_located_term ref = print_located_qualid "term" LocTerm ref -let print_located_other s ref = print_located_qualid s (LocOther s) ref -let print_located_module ref = print_located_qualid "module" LocModule ref -let print_located_qualid ref = print_located_qualid "object" LocAny ref - -(******************************************) -(**** Printing declarations and judgments *) -(**** Gallina layer *****) - -let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_leconstr_env env sigma trm ++ fnl () ++ - str " : " ++ pr_letype_env env sigma typ) - -(* To be improved; the type should be used to provide the types in the - abstractions. This should be done recursively inside pr_lconstr, so that - the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) - synthesizes the type nat of the abstraction on u *) - -let print_named_def env sigma name body typ = - let pbody = pr_lconstr_env env sigma body in - let ptyp = pr_ltype_env env sigma typ in - let pbody = if Constr.isCast body then surround pbody else pbody in - (str "*** [" ++ str name ++ str " " ++ - hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ - str ":" ++ brk (1,2) ++ ptyp) ++ - str "]") - -let print_named_assum env sigma name typ = - str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" - -let gallina_print_named_decl env sigma = - let open Context.Named.Declaration in - function - | LocalAssum (id, typ) -> - print_named_assum env sigma (Id.to_string id.Context.binder_name) typ - | LocalDef (id, body, typ) -> - print_named_def env sigma (Id.to_string id.Context.binder_name) body typ - -let assumptions_for_print lna = - List.fold_right (fun na env -> add_name na env) lna empty_names_context - -(*********************) -(* *) - -let gallina_print_inductive sp udecl = - let env = Global.env() in - let mib = Environ.lookup_mind sp env in - let mipv = mib.mind_packets in - 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) - -let print_named_decl env sigma id = - gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () - -let gallina_print_section_variable env sigma id = - print_named_decl env sigma id ++ - with_line_skip (print_name_infos (GlobRef.VarRef id)) - -let print_body env evd = function - | Some c -> pr_lconstr_env env evd c - | None -> (str"") - -let print_typed_body env evd (val_0,typ) = - (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) - -let print_instance sigma cb = - if Declareops.constant_is_polymorphic cb then - let univs = Declareops.constant_polymorphic_context cb in - let inst = Univ.make_abstract_instance univs in - pr_universe_instance sigma inst - else mt() - -let print_constant indirect_accessor with_values sep sp udecl = - let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body indirect_accessor cb in - let typ = cb.const_type in - let univs = - let open Univ in - let otab = Global.opaque_tables () in - match cb.const_body with - | Undef _ | Def _ | Primitive _ -> cb.const_universes - | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in - match cb.const_universes with - | Monomorphic ctx -> - Monomorphic (ContextSet.union body_uctxs ctx) - | Polymorphic ctx -> - assert(ContextSet.is_empty body_uctxs); - Polymorphic ctx - in - let ctx = - UState.of_binders - (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) - in - let env = Global.env () and sigma = Evd.from_ctx ctx in - let pr_ltype = pr_ltype_env env sigma in - hov 0 ( - match val_0 with - | None -> - str"*** [ " ++ - print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ - str" ]" ++ - Printer.pr_universes sigma univs - | Some (c, priv, ctx) -> - let priv = match priv with - | Opaqueproof.PrivateMonomorphic () -> None - | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx - in - print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ - Printer.pr_universes sigma univs ?priv) - -let gallina_print_constant_with_infos indirect_accessor sp udecl = - print_constant indirect_accessor true " = " sp udecl ++ - with_line_skip (print_name_infos (GlobRef.ConstRef sp)) - -let gallina_print_syntactic_def env kn = - let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn - and (vars,a) = Syntax_def.search_syntactic_definition kn in - let c = Notation_ops.glob_constr_of_notation_constr a in - hov 2 - (hov 4 - (str "Notation " ++ pr_qualid qid ++ - prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++ - spc () ++ str ":=") ++ - spc () ++ - Constrextern.without_specific_symbols - [Notation.SynDefRule kn] (pr_glob_constr_env env) c) - -let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = - let sep = if with_values then " = " else " : " in - match lobj with - | AtomicObject o -> - let tag = object_tag o in - begin match (oname,tag) with - | (_,"VARIABLE") -> - (* Outside sections, VARIABLES still exist but only with universes - constraints *) - (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) - | (_,"CONSTANT") -> - Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) - | (_,"INDUCTIVE") -> - Some (gallina_print_inductive (MutInd.make1 kn) None) - | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| - "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None - (* To deal with forgotten cases... *) - | (_,s) -> None - end - | ModuleObject _ -> - let (mp,l) = KerName.repr kn in - Some (print_module ~mod_ops with_values (MPdot (mp,l))) - | ModuleTypeObject _ -> - let (mp,l) = KerName.repr kn in - Some (print_modtype ~mod_ops (MPdot (mp,l))) - | _ -> None - -let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = - let pr_name (sp,_) = Id.print (basename sp) in - match ent with - | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) - | (oname,Lib.OpenedSection (dir,_)) -> - Some (str " >>>>>>> Section " ++ pr_name oname) - | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> - Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) - | (oname,Lib.OpenedModule _) -> - Some (str " >>>>>>> Module " ++ pr_name oname) - -let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = - let rec prec n = function - | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with - | None -> prec n rest - | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) - | _ -> mt () - in - prec - -let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = - let ntrm = red_fun env sigma trm in - (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) - -(******************************************) -(**** Printing abstraction layer *) - -let default_object_pr = { - print_inductive = gallina_print_inductive; - print_constant_with_infos = gallina_print_constant_with_infos; - print_section_variable = gallina_print_section_variable; - print_syntactic_def = gallina_print_syntactic_def; - print_module = gallina_print_module; - print_modtype = gallina_print_modtype; - print_named_decl = gallina_print_named_decl; - print_library_entry = gallina_print_library_entry; - print_context = gallina_print_context; - print_typed_value_in_env = gallina_print_typed_value_in_env; - print_eval = gallina_print_eval; -} - -let object_pr = ref default_object_pr -let set_object_pr = (:=) object_pr - -let print_inductive x = !object_pr.print_inductive x -let print_constant_with_infos c = !object_pr.print_constant_with_infos c -let print_section_variable c = !object_pr.print_section_variable c -let print_syntactic_def x = !object_pr.print_syntactic_def x -let print_module x = !object_pr.print_module x -let print_modtype x = !object_pr.print_modtype x -let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x -let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x -let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x -let print_eval x = !object_pr.print_eval x - -(******************************************) -(**** Printing declarations and judgments *) -(**** Abstract layer *****) - -let print_judgment env sigma {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env sigma (trm, typ) - -let print_safe_judgment env sigma j = - let trm = Safe_typing.j_val j in - let typ = Safe_typing.j_type j in - let trm = EConstr.of_constr trm in - let typ = EConstr.of_constr typ in - print_typed_value_in_env env sigma (trm, typ) - -(*********************) -(* *) - -let print_full_context ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) - -let print_full_pure_context ~mod_ops ~library_accessor env sigma = - let rec prec = function - | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> - let pp = match object_tag lobj with - | "CONSTANT" -> - let con = Global.constant_of_delta_kn kn in - let cb = Global.lookup_constant con in - let typ = cb.const_type in - hov 0 ( - match cb.const_body with - | Undef _ -> - str "Parameter " ++ - print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ - | OpaqueDef lc -> - str "Theorem " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) - | Def c -> - str "Definition " ++ print_basename con ++ cut () ++ - str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ - pr_lconstr_env env sigma (Mod_subst.force_constr c) - | Primitive _ -> - str "Primitive " ++ - print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) - ++ str "." ++ fnl () ++ fnl () - | "INDUCTIVE" -> - let mind = Global.mind_of_delta_kn kn in - let mib = Global.lookup_mind mind in - pr_mutual_inductive_body (Global.env()) mind mib None ++ - str "." ++ fnl () ++ fnl () - | _ -> mt () in - prec rest ++ pp - | ((_,kn),Lib.Leaf ModuleObject _)::rest -> - (* TODO: make it reparsable *) - let (mp,l) = KerName.repr kn in - prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () - | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> - (* TODO: make it reparsable *) - let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () - | _::rest -> prec rest - | _ -> mt () in - prec (Lib.contents ()) - -(* For printing an inductive definition with - its constructors and elimination, - assume that the declaration of constructors and eliminations - follows the definition of the inductive type *) - -(* This is designed to print the contents of an opened section *) -let read_sec_context qid = - let dir = - try Nametab.locate_section qid - with Not_found -> - user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in - let rec get_cxt in_cxt = function - | (_,Lib.OpenedSection ({Nametab.obj_dir;_},_) as hd)::rest -> - if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest - | [] -> [] - | hd::rest -> get_cxt (hd::in_cxt) rest - in - let cxt = Lib.contents () in - List.rev (get_cxt [] cxt) - -let print_sec_context ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) - -let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) - -let maybe_error_reject_univ_decl na udecl = - let open GlobRef in - match na, udecl with - | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> () - | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl -> - (* TODO Print na somehow *) - user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") - -let print_any_name ~mod_ops indirect_accessor env sigma na udecl = - maybe_error_reject_univ_decl na udecl; - let open GlobRef in - match na with - | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl - | Term (IndRef (sp,_)) -> print_inductive sp udecl - | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl - | Term (VarRef sp) -> print_section_variable env sigma sp - | Syntactic kn -> print_syntactic_def env kn - | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> - print_module ~mod_ops (printable_body obj_dir) obj_mp - | Dir _ -> mt () - | ModuleType mp -> print_modtype ~mod_ops mp - | Other (obj, info) -> info.print obj - | Undefined qid -> - try (* Var locale de but, pas var de section... donc pas d'implicits *) - let dir,str = repr_qualid qid in - if not (DirPath.is_empty dir) then raise Not_found; - str |> Global.lookup_named |> print_named_decl env sigma - - with Not_found -> - user_err - ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") - -let print_name ~mod_ops indirect_accessor env sigma na udecl = - match na with - | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name ~mod_ops indirect_accessor env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) - ntn sc)) - udecl - | {loc; v=Constrexpr.AN ref} -> - print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl - -let print_opaque_name indirect_accessor env sigma qid = - let open GlobRef in - match Nametab.global qid with - | ConstRef cst -> - let cb = Global.lookup_constant cst in - if Declareops.constant_has_body cb then - print_constant_with_infos indirect_accessor cst None - else - user_err Pp.(str "Not a defined constant.") - | IndRef (sp,_) -> - print_inductive sp None - | ConstructRef cstr as gr -> - let ty, ctx = Typeops.type_of_global_in_context env gr in - let ty = EConstr.of_constr ty in - let open EConstr in - print_typed_value_in_env env sigma (mkConstruct cstr, ty) - | VarRef id -> - env |> lookup_named id |> print_named_decl env sigma - -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)]) - | Syntactic kn -> - let () = match Syntax_def.search_syntactic_definition kn with - | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref - | _ -> () in - v 0 ( - print_syntactic_def env kn ++ fnl () ++ - hov 0 (str "Expands to: " ++ pr_located_qualid k)) - | Dir _ | ModuleType _ | Undefined _ -> - hov 0 (pr_located_qualid k) - | Other (obj, info) -> hov 0 (info.about obj) - -let print_about env sigma na udecl = - match na with - | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> - print_about_any ?loc env sigma - (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) - ntn sc)) udecl - | {loc;v=Constrexpr.AN ref} -> - print_about_any ?loc env sigma (locate_any_name ref) udecl - -(* for debug *) -let inspect ~mod_ops indirect_accessor env sigma depth = - print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) - -(*************************************************************************) -(* Pretty-printing functions coming from classops.ml *) - -open Classops - -let print_coercion_value v = Printer.pr_global v.coe_value - -let print_class i = - let cl,_ = class_info_from_index i in - pr_class cl - -let print_path ((i,j),p) = - hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ - str"] : ") ++ - print_class i ++ str" >-> " ++ print_class j - -let _ = Classops.install_path_printer print_path - -let print_graph () = - prlist_with_sep fnl print_path (inheritance_graph()) - -let print_classes () = - pr_sequence pr_class (classes()) - -let print_coercions () = - pr_sequence print_coercion_value (coercions()) - -let index_of_class cl = - try - fst (class_info cl) - with Not_found -> - user_err ~hdr:"index_of_class" - (pr_class cl ++ spc() ++ str "not a defined class.") - -let print_path_between cls clt = - let i = index_of_class cls in - let j = index_of_class clt in - let p = - try - lookup_path_between_class (i,j) - with Not_found -> - user_err ~hdr:"index_cl_of_id" - (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt - ++ str ".") - in - print_path ((i,j),p) - -let print_canonical_projections env sigma = - prlist_with_sep fnl - (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ - str " <- " ++ - pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )") - (canonical_projections ()) - -(*************************************************************************) - -(*************************************************************************) -(* Pretty-printing functions for type classes *) - -open Typeclasses - -let pr_typeclass env t = - print_ref false t.cl_impl None - -let print_typeclasses () = - let env = Global.env () in - prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) - -let pr_instance env i = - (* gallina_print_constant_with_infos i.is_impl *) - (* lighter *) - print_ref false (instance_impl i) None ++ - begin match hint_priority i with - | None -> mt () - | Some i -> spc () ++ str "|" ++ spc () ++ int i - end - -let print_all_instances () = - let env = Global.env () in - let inst = all_instances () in - prlist_with_sep fnl (pr_instance env) inst - -let print_instances r = - let env = Global.env () in - let sigma = Evd.from_env env in - let inst = instances env sigma r in - prlist_with_sep fnl (pr_instance env) inst diff --git a/printing/prettyp.mli b/printing/prettyp.mli deleted file mode 100644 index c8b361d95b..0000000000 --- a/printing/prettyp.mli +++ /dev/null @@ -1,129 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* Termops.names_context - -val print_closed_sections : bool ref -val print_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t -val print_full_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t - -val print_full_pure_context - : mod_ops:Printmod.mod_ops - -> library_accessor:Opaqueproof.indirect_accessor - -> env - -> Evd.evar_map - -> Pp.t - -val print_sec_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t -val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t -val print_eval : - reduction_function -> env -> Evd.evar_map -> - Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t - -val print_name - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation - -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> - UnivNames.univ_name_list option -> Pp.t -val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t - -(** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> Pp.t -val print_classes : unit -> Pp.t -val print_coercions : unit -> Pp.t -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t -val print_canonical_projections : env -> Evd.evar_map -> Pp.t - -(** Pretty-printing functions for type classes and instances *) -val print_typeclasses : unit -> Pp.t -val print_instances : GlobRef.t -> Pp.t -val print_all_instances : unit -> Pp.t - -val inspect - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> int -> Pp.t - -(** {5 Locate} *) - -type 'a locatable_info = { - locate : qualid -> 'a option; - (** Locate the most precise object with the provided name if any. *) - locate_all : qualid -> 'a list; - (** Locate all objects whose name is a suffix of the provided name *) - shortest_qualid : 'a -> qualid; - (** Return the shortest name in the current context *) - name : 'a -> Pp.t; - (** Data as printed by the Locate command *) - print : 'a -> Pp.t; - (** Data as printed by the Print command *) - about : 'a -> Pp.t; - (** Data as printed by the About command *) -} -(** Generic data structure representing locatable objects. *) - -val register_locatable : string -> 'a locatable_info -> unit -(** Define a new type of locatable objects that can be reached via the - corresponding generic vernacular commands. The string should be a unique - name describing the kind of objects considered and that is added as a - grammar command prefix for vernacular commands Locate. *) - -val print_located_qualid : qualid -> Pp.t -val print_located_term : qualid -> Pp.t -val print_located_module : qualid -> Pp.t -val print_located_other : string -> qualid -> Pp.t - -type object_pr = { - print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; - print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; - print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; -} - -val set_object_pr : object_pr -> unit -val default_object_pr : object_pr diff --git a/printing/printing.mllib b/printing/printing.mllib index deb52ad270..5b5b6590a4 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -4,4 +4,3 @@ Ppconstr Proof_diffs Printer Printmod -Prettyp diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml new file mode 100644 index 0000000000..fa534a0936 --- /dev/null +++ b/vernac/prettyp.ml @@ -0,0 +1,984 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* + * on May-June 2006 for implementation of abstraction of pretty-printing of objects. + *) + +open Pp +open CErrors +open Util +open CAst +open Names +open Nameops +open Termops +open Declarations +open Environ +open Impargs +open Libobject +open Libnames +open Globnames +open Recordops +open Printer +open Printmod +open Context.Rel.Declaration + +(* module RelDecl = Context.Rel.Declaration *) +module NamedDecl = Context.Named.Declaration + +type object_pr = { + print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; + print_syntactic_def : env -> KerName.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; +} + +let gallina_print_module = print_module +let gallina_print_modtype = print_modtype + +(**************) +(** Utilities *) + +let print_closed_sections = ref false + +let pr_infos_list l = v 0 (prlist_with_sep cut (fun x -> x) l) + +let with_line_skip l = if List.is_empty l then mt() else fnl() ++ fnl () ++ pr_infos_list l + +let blankline = mt() (* add a blank sentence in the list of infos *) + +let add_colon prefix = if ismt prefix then mt () else prefix ++ str ": " + +let int_or_no n = if Int.equal n 0 then str "no" else int n + +(*******************) +(** Basic printing *) + +let print_basename sp = pr_global (GlobRef.ConstRef sp) + +let print_ref reduce ref udecl = + let env = Global.env () in + let typ, univs = Typeops.type_of_global_in_context env ref in + let inst = Univ.make_abstract_instance univs in + let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in + let sigma = Evd.from_ctx (UState.of_binders bl) in + let typ = EConstr.of_constr typ in + let typ = + if reduce then + let ctx,ccl = Reductionops.splay_prod_assum env sigma typ + in EConstr.it_mkProd_or_LetIn ccl ctx + else typ in + let variance = let open GlobRef in match ref with + | VarRef _ | ConstRef _ -> None + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> + let mind = Environ.lookup_mind ind env in + mind.Declarations.mind_variance + in + let inst = + if Global.is_polymorphic ref + then Printer.pr_universe_instance sigma inst + else mt () + in + let priv = None in (* We deliberately don't print private univs in About. *) + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) + +(********************************) +(** Printing implicit arguments *) + +let pr_impl_name imp = Id.print (name_of_implicit imp) + +let print_impargs_by_name max = function + | [] -> [] + | impls -> + let n = List.length impls in + [hov 0 (str (String.plural n "Argument") ++ spc() ++ + prlist_with_sep pr_comma pr_impl_name impls ++ spc() ++ + str (String.conjugate_verb_to_be n) ++ str" implicit" ++ + (if max then strbrk " and maximally inserted" else mt()))] + +let print_one_impargs_list l = + let imps = List.filter is_status_implicit l in + let maximps = List.filter Impargs.maximal_insertion_of imps in + let nonmaximps = List.subtract (=) imps maximps in (* FIXME *) + print_impargs_by_name false nonmaximps @ + print_impargs_by_name true maximps + +let print_impargs_list prefix l = + let l = extract_impargs_data l in + List.flatten (List.map (fun (cond,imps) -> + match cond with + | None -> + List.map (fun pp -> add_colon prefix ++ pp) + (print_one_impargs_list imps) + | Some (n1,n2) -> + [v 2 (prlist_with_sep cut (fun x -> x) + [(if ismt prefix then str "When" else prefix ++ str ", when") ++ + str " applied to " ++ + (if Int.equal n1 n2 then int_or_no n2 else + if Int.equal n1 0 then str "no more than " ++ int n2 + else int n1 ++ str " to " ++ int_or_no n2) ++ + str (String.plural n2 " argument") ++ str ":"; + v 0 (prlist_with_sep cut (fun x -> x) + (if List.exists is_status_implicit imps + 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 + let nprods = List.count is_local_assum ctx in + not (List.is_empty impl) && List.length impl >= nprods && + let _,lastimpl = List.chop nprods impl in + List.exists is_status_implicit lastimpl + +let print_impargs ref = + let ref = Smartlocate.smart_global ref in + let impl = implicits_of_global ref in + let has_impl = not (List.is_empty impl) in + (* Need to reduce since implicits are computed with products flattened *) + pr_infos_list + ([ print_ref (need_expansion (select_impargs_size 0 impl) ref) ref None; + blankline ] @ + (if has_impl then print_impargs_list (mt()) impl + 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 = + | FullyOpaque + | TransparentMaybeOpacified of Conv_oracle.level + +let opacity env = + function + | GlobRef.VarRef v when NamedDecl.is_local_def (Environ.lookup_named v env) -> + Some(TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (VarKey v))) + | GlobRef.ConstRef cst -> + let cb = Environ.lookup_constant cst env in + (match cb.const_body with + | Undef _ | Primitive _ -> None + | OpaqueDef _ -> Some FullyOpaque + | Def _ -> Some + (TransparentMaybeOpacified + (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) + | _ -> None + +let print_opacity ref = + match opacity (Global.env()) ref with + | None -> [] + | Some s -> + [pr_global ref ++ str " is " ++ + match s with + | FullyOpaque -> str "opaque" + | TransparentMaybeOpacified Conv_oracle.Opaque -> + str "basically transparent but considered opaque for reduction" + | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev -> + str "transparent" + | TransparentMaybeOpacified (Conv_oracle.Level n) -> + str "transparent (with expansion weight " ++ int n ++ str ")" + | TransparentMaybeOpacified Conv_oracle.Expand -> + str "transparent (with minimal expansion weight)"] + +(*******************) + +let print_if_is_coercion ref = + if Classops.coercion_exists ref then [pr_global ref ++ str " is a coercion"] else [] + +(*******************) +(* *) + +let pr_template_variables = function + | [] -> mt () + | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars + +let print_polymorphism ref = + let poly = Global.is_polymorphic ref in + let template_poly = Global.is_template_polymorphic ref in + let template_checked = Global.is_template_checked ref in + let template_variables = Global.get_template_polymorphic_variables ref in + [ pr_global ref ++ str " is " ++ + (if poly then str "universe polymorphic" + else if template_poly then + (if not template_checked then str "assumed " else mt()) ++ + str "template universe polymorphic " + ++ h 0 (pr_template_variables template_variables) + else str "not universe polymorphic") ] + +let print_type_in_type ref = + let unsafe = Global.is_type_in_type ref in + if unsafe then + [ pr_global ref ++ str " relies on an unsafe universe hierarchy"] + else [] + +let print_primitive_record recflag mipv = function + | PrimRecord _ -> + let eta = match recflag with + | CoFinite | Finite -> str" without eta conversion" + | BiFinite -> str " with eta conversion" + in + [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] + | FakeRecord | NotRecord -> [] + +let print_primitive ref = + match ref with + | GlobRef.IndRef ind -> + let mib,_ = Global.lookup_inductive ind in + 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 scopes = Notation.find_arguments_scope ref in + let renames = + try Arguments_renaming.arguments_names ref with Not_found -> [] in + let type_info_for_implicit = + if need_expansion (select_impargs_size 0 impls) ref then + (* Need to reduce since implicits are computed with products flattened *) + [str "Expanded type for implicit arguments"; + print_ref true ref None; blankline] + else + [] in + 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_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_bidi_hints gr = + match Pretyping.get_bidirectionality_hint gr with + | None -> [] + | Some nargs -> + [str "Using typing information from context after typing the " ++ int nargs ++ str " first arguments"] + +(*********************) +(* "Locate" commands *) + +type 'a locatable_info = { + locate : qualid -> 'a option; + locate_all : qualid -> 'a list; + shortest_qualid : 'a -> qualid; + name : 'a -> Pp.t; + print : 'a -> Pp.t; + about : 'a -> Pp.t; +} + +type locatable = Locatable : 'a locatable_info -> locatable + +type logical_name = + | Term of GlobRef.t + | Dir of Nametab.GlobDirRef.t + | Syntactic of KerName.t + | ModuleType of ModPath.t + | Other : 'a * 'a locatable_info -> logical_name + | Undefined of qualid + +(** Generic table for objects that are accessible through a name. *) +let locatable_map : locatable String.Map.t ref = ref String.Map.empty + +let register_locatable name f = + locatable_map := String.Map.add name (Locatable f) !locatable_map + +exception ObjFound of logical_name + +let locate_any_name qid = + try Term (Nametab.locate qid) + with Not_found -> + try Syntactic (Nametab.locate_syndef qid) + with Not_found -> + try Dir (Nametab.locate_dir qid) + with Not_found -> + try ModuleType (Nametab.locate_modtype qid) + with Not_found -> + let iter _ (Locatable info) = match info.locate qid with + | None -> () + | Some ans -> raise (ObjFound (Other (ans, info))) + in + try String.Map.iter iter !locatable_map; Undefined qid + with ObjFound obj -> obj + +let pr_located_qualid = function + | Term ref -> + let ref_str = let open GlobRef in match ref with + ConstRef _ -> "Constant" + | IndRef _ -> "Inductive" + | ConstructRef _ -> "Constructor" + | VarRef _ -> "Variable" in + str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) + | Syntactic kn -> + str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) + | Dir dir -> + let s,dir = + let open Nametab in + let open GlobDirRef in match dir with + | DirOpenModule { obj_dir ; _ } -> "Open Module", obj_dir + | DirOpenModtype { obj_dir ; _ } -> "Open Module Type", obj_dir + | DirOpenSection { obj_dir ; _ } -> "Open Section", obj_dir + | DirModule { obj_dir ; _ } -> "Module", obj_dir + in + str s ++ spc () ++ DirPath.print dir + | ModuleType mp -> + str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) + | Other (obj, info) -> info.name obj + | Undefined qid -> + pr_qualid qid ++ spc () ++ str "not a defined object." + +let canonize_ref = let open GlobRef in function + | ConstRef c -> + let kn = Constant.canonical c in + if KerName.equal (Constant.user c) kn then None + else Some (ConstRef (Constant.make1 kn)) + | IndRef (ind,i) -> + let kn = MutInd.canonical ind in + if KerName.equal (MutInd.user ind) kn then None + else Some (IndRef (MutInd.make1 kn, i)) + | ConstructRef ((ind,i),j) -> + let kn = MutInd.canonical ind in + if KerName.equal (MutInd.user ind) kn then None + else Some (ConstructRef ((MutInd.make1 kn, i),j)) + | VarRef _ -> None + +let display_alias = function + | Term r -> + begin match canonize_ref r with + | None -> mt () + | Some r' -> + let q' = Nametab.shortest_qualid_of_global Id.Set.empty r' in + spc () ++ str "(alias of " ++ pr_qualid q' ++ str ")" + end + | _ -> mt () + +let locate_term qid = + let expand = function + | TrueGlobal ref -> + Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref + | SynDef kn -> + Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn + in + List.map expand (Nametab.locate_extended_all qid) + +let locate_module qid = + let all = Nametab.locate_extended_all_dir qid in + let map dir = let open Nametab.GlobDirRef in match dir with + | DirModule { Nametab.obj_mp ; _ } -> Some (Dir dir, Nametab.shortest_qualid_of_module obj_mp) + | DirOpenModule _ -> Some (Dir dir, qid) + | _ -> None + in + List.map_filter map all + +let locate_modtype qid = + let all = Nametab.locate_extended_all_modtype qid in + let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in + let modtypes = List.map map all in + (* Don't forget the opened module types: they are not part of the same name tab. *) + let all = Nametab.locate_extended_all_dir qid in + let map dir = let open Nametab.GlobDirRef in match dir with + | DirOpenModtype _ -> Some (Dir dir, qid) + | _ -> None + in + modtypes @ List.map_filter map all + +let locate_other s qid = + let Locatable info = String.Map.find s !locatable_map in + let ans = info.locate_all qid in + let map obj = (Other (obj, info), info.shortest_qualid obj) in + List.map map ans + +type locatable_kind = +| LocTerm +| LocModule +| LocOther of string +| LocAny + +let print_located_qualid name flags qid = + let located = match flags with + | LocTerm -> locate_term qid + | LocModule -> locate_modtype qid @ locate_module qid + | LocOther s -> locate_other s qid + | LocAny -> + locate_term qid @ + locate_modtype qid @ + locate_module qid @ + String.Map.fold (fun s _ accu -> locate_other s qid @ accu) !locatable_map [] + in + match located with + | [] -> + let (dir,id) = repr_qualid qid in + if DirPath.is_empty dir then + str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id + else + str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid + | l -> + prlist_with_sep fnl + (fun (o,oqid) -> + hov 2 (pr_located_qualid o ++ + (if not (qualid_eq oqid qid) then + spc() ++ str "(shorter name to refer to it in current context is " + ++ pr_qualid oqid ++ str")" + else mt ()) ++ + display_alias o)) l + +let print_located_term ref = print_located_qualid "term" LocTerm ref +let print_located_other s ref = print_located_qualid s (LocOther s) ref +let print_located_module ref = print_located_qualid "module" LocModule ref +let print_located_qualid ref = print_located_qualid "object" LocAny ref + +(******************************************) +(**** Printing declarations and judgments *) +(**** Gallina layer *****) + +let gallina_print_typed_value_in_env env sigma (trm,typ) = + (pr_leconstr_env env sigma trm ++ fnl () ++ + str " : " ++ pr_letype_env env sigma typ) + +(* To be improved; the type should be used to provide the types in the + abstractions. This should be done recursively inside pr_lconstr, so that + the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u) + synthesizes the type nat of the abstraction on u *) + +let print_named_def env sigma name body typ = + let pbody = pr_lconstr_env env sigma body in + let ptyp = pr_ltype_env env sigma typ in + let pbody = if Constr.isCast body then surround pbody else pbody in + (str "*** [" ++ str name ++ str " " ++ + hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ + str ":" ++ brk (1,2) ++ ptyp) ++ + str "]") + +let print_named_assum env sigma name typ = + str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" + +let gallina_print_named_decl env sigma = + let open Context.Named.Declaration in + function + | LocalAssum (id, typ) -> + print_named_assum env sigma (Id.to_string id.Context.binder_name) typ + | LocalDef (id, body, typ) -> + print_named_def env sigma (Id.to_string id.Context.binder_name) body typ + +let assumptions_for_print lna = + List.fold_right (fun na env -> add_name na env) lna empty_names_context + +(*********************) +(* *) + +let gallina_print_inductive sp udecl = + let env = Global.env() in + let mib = Environ.lookup_mind sp env in + let mipv = mib.mind_packets in + 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) + +let print_named_decl env sigma id = + gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () + +let gallina_print_section_variable env sigma id = + print_named_decl env sigma id ++ + with_line_skip (print_name_infos (GlobRef.VarRef id)) + +let print_body env evd = function + | Some c -> pr_lconstr_env env evd c + | None -> (str"") + +let print_typed_body env evd (val_0,typ) = + (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) + +let print_instance sigma cb = + if Declareops.constant_is_polymorphic cb then + let univs = Declareops.constant_polymorphic_context cb in + let inst = Univ.make_abstract_instance univs in + pr_universe_instance sigma inst + else mt() + +let print_constant indirect_accessor with_values sep sp udecl = + let cb = Global.lookup_constant sp in + let val_0 = Global.body_of_constant_body indirect_accessor cb in + let typ = cb.const_type in + let univs = + let open Univ in + let otab = Global.opaque_tables () in + match cb.const_body with + | Undef _ | Def _ | Primitive _ -> cb.const_universes + | OpaqueDef o -> + let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in + match cb.const_universes with + | Monomorphic ctx -> + Monomorphic (ContextSet.union body_uctxs ctx) + | Polymorphic ctx -> + assert(ContextSet.is_empty body_uctxs); + Polymorphic ctx + in + let ctx = + UState.of_binders + (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) + in + let env = Global.env () and sigma = Evd.from_ctx ctx in + let pr_ltype = pr_ltype_env env sigma in + hov 0 ( + match val_0 with + | None -> + str"*** [ " ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ + str" ]" ++ + Printer.pr_universes sigma univs + | Some (c, priv, ctx) -> + let priv = match priv with + | Opaqueproof.PrivateMonomorphic () -> None + | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx + in + print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ + (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ + Printer.pr_universes sigma univs ?priv) + +let gallina_print_constant_with_infos indirect_accessor sp udecl = + print_constant indirect_accessor true " = " sp udecl ++ + with_line_skip (print_name_infos (GlobRef.ConstRef sp)) + +let gallina_print_syntactic_def env kn = + let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn + and (vars,a) = Syntax_def.search_syntactic_definition kn in + let c = Notation_ops.glob_constr_of_notation_constr a in + hov 2 + (hov 4 + (str "Notation " ++ pr_qualid qid ++ + prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++ + spc () ++ str ":=") ++ + spc () ++ + Constrextern.without_specific_symbols + [Notation.SynDefRule kn] (pr_glob_constr_env env) c) + +let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = + let sep = if with_values then " = " else " : " in + match lobj with + | AtomicObject o -> + let tag = object_tag o in + begin match (oname,tag) with + | (_,"VARIABLE") -> + (* Outside sections, VARIABLES still exist but only with universes + constraints *) + (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) + | (_,"CONSTANT") -> + Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) + | (_,"INDUCTIVE") -> + Some (gallina_print_inductive (MutInd.make1 kn) None) + | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| + "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None + (* To deal with forgotten cases... *) + | (_,s) -> None + end + | ModuleObject _ -> + let (mp,l) = KerName.repr kn in + Some (print_module ~mod_ops with_values (MPdot (mp,l))) + | ModuleTypeObject _ -> + let (mp,l) = KerName.repr kn in + Some (print_modtype ~mod_ops (MPdot (mp,l))) + | _ -> None + +let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = + let pr_name (sp,_) = Id.print (basename sp) in + match ent with + | (oname,Lib.Leaf lobj) -> + gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) + | (oname,Lib.OpenedSection (dir,_)) -> + Some (str " >>>>>>> Section " ++ pr_name oname) + | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> + Some (str " >>>>>>> Library " ++ DirPath.print obj_dir) + | (oname,Lib.OpenedModule _) -> + Some (str " >>>>>>> Module " ++ pr_name oname) + +let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = + let rec prec n = function + | h::rest when Option.is_empty n || Option.get n > 0 -> + (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with + | None -> prec n rest + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) + | _ -> mt () + in + prec + +let gallina_print_eval red_fun env sigma _ {uj_val=trm;uj_type=typ} = + let ntrm = red_fun env sigma trm in + (str " = " ++ gallina_print_typed_value_in_env env sigma (ntrm,typ)) + +(******************************************) +(**** Printing abstraction layer *) + +let default_object_pr = { + print_inductive = gallina_print_inductive; + print_constant_with_infos = gallina_print_constant_with_infos; + print_section_variable = gallina_print_section_variable; + print_syntactic_def = gallina_print_syntactic_def; + print_module = gallina_print_module; + print_modtype = gallina_print_modtype; + print_named_decl = gallina_print_named_decl; + print_library_entry = gallina_print_library_entry; + print_context = gallina_print_context; + print_typed_value_in_env = gallina_print_typed_value_in_env; + print_eval = gallina_print_eval; +} + +let object_pr = ref default_object_pr +let set_object_pr = (:=) object_pr + +let print_inductive x = !object_pr.print_inductive x +let print_constant_with_infos c = !object_pr.print_constant_with_infos c +let print_section_variable c = !object_pr.print_section_variable c +let print_syntactic_def x = !object_pr.print_syntactic_def x +let print_module x = !object_pr.print_module x +let print_modtype x = !object_pr.print_modtype x +let print_named_decl x = !object_pr.print_named_decl x +let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x +let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x +let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x +let print_eval x = !object_pr.print_eval x + +(******************************************) +(**** Printing declarations and judgments *) +(**** Abstract layer *****) + +let print_judgment env sigma {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env sigma (trm, typ) + +let print_safe_judgment env sigma j = + let trm = Safe_typing.j_val j in + let typ = Safe_typing.j_type j in + let trm = EConstr.of_constr trm in + let typ = EConstr.of_constr typ in + print_typed_value_in_env env sigma (trm, typ) + +(*********************) +(* *) + +let print_full_context ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) +let print_full_context_typ ~mod_ops indirect_accessor env sigma = + print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) + +let print_full_pure_context ~mod_ops ~library_accessor env sigma = + let rec prec = function + | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> + let pp = match object_tag lobj with + | "CONSTANT" -> + let con = Global.constant_of_delta_kn kn in + let cb = Global.lookup_constant con in + let typ = cb.const_type in + hov 0 ( + match cb.const_body with + | Undef _ -> + str "Parameter " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ + | OpaqueDef lc -> + str "Theorem " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ + str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + | Def c -> + str "Definition " ++ print_basename con ++ cut () ++ + str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ + pr_lconstr_env env sigma (Mod_subst.force_constr c) + | Primitive _ -> + str "Primitive " ++ + print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) + ++ str "." ++ fnl () ++ fnl () + | "INDUCTIVE" -> + let mind = Global.mind_of_delta_kn kn in + let mib = Global.lookup_mind mind in + pr_mutual_inductive_body (Global.env()) mind mib None ++ + str "." ++ fnl () ++ fnl () + | _ -> mt () in + prec rest ++ pp + | ((_,kn),Lib.Leaf ModuleObject _)::rest -> + (* TODO: make it reparsable *) + let (mp,l) = KerName.repr kn in + prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> + (* TODO: make it reparsable *) + let (mp,l) = KerName.repr kn in + prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + | _::rest -> prec rest + | _ -> mt () in + prec (Lib.contents ()) + +(* For printing an inductive definition with + its constructors and elimination, + assume that the declaration of constructors and eliminations + follows the definition of the inductive type *) + +(* This is designed to print the contents of an opened section *) +let read_sec_context qid = + let dir = + try Nametab.locate_section qid + with Not_found -> + user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in + let rec get_cxt in_cxt = function + | (_,Lib.OpenedSection ({Nametab.obj_dir;_},_) as hd)::rest -> + if DirPath.equal dir obj_dir then (hd::in_cxt) else get_cxt (hd::in_cxt) rest + | [] -> [] + | hd::rest -> get_cxt (hd::in_cxt) rest + in + let cxt = Lib.contents () in + List.rev (get_cxt [] cxt) + +let print_sec_context ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) + +let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = + print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) + +let maybe_error_reject_univ_decl na udecl = + let open GlobRef in + match na, udecl with + | _, None | Term (ConstRef _ | IndRef _ | ConstructRef _), Some _ -> () + | (Term (VarRef _) | Syntactic _ | Dir _ | ModuleType _ | Other _ | Undefined _), Some udecl -> + (* TODO Print na somehow *) + user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") + +let print_any_name ~mod_ops indirect_accessor env sigma na udecl = + maybe_error_reject_univ_decl na udecl; + let open GlobRef in + match na with + | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl + | Term (IndRef (sp,_)) -> print_inductive sp udecl + | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl + | Term (VarRef sp) -> print_section_variable env sigma sp + | Syntactic kn -> print_syntactic_def env kn + | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> + print_module ~mod_ops (printable_body obj_dir) obj_mp + | Dir _ -> mt () + | ModuleType mp -> print_modtype ~mod_ops mp + | Other (obj, info) -> info.print obj + | Undefined qid -> + try (* Var locale de but, pas var de section... donc pas d'implicits *) + let dir,str = repr_qualid qid in + if not (DirPath.is_empty dir) then raise Not_found; + str |> Global.lookup_named |> print_named_decl env sigma + + with Not_found -> + user_err + ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") + +let print_name ~mod_ops indirect_accessor env sigma na udecl = + match na with + | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> + print_any_name ~mod_ops indirect_accessor env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + ntn sc)) + udecl + | {loc; v=Constrexpr.AN ref} -> + print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl + +let print_opaque_name indirect_accessor env sigma qid = + let open GlobRef in + match Nametab.global qid with + | ConstRef cst -> + let cb = Global.lookup_constant cst in + if Declareops.constant_has_body cb then + print_constant_with_infos indirect_accessor cst None + else + user_err Pp.(str "Not a defined constant.") + | IndRef (sp,_) -> + print_inductive sp None + | ConstructRef cstr as gr -> + let ty, ctx = Typeops.type_of_global_in_context env gr in + let ty = EConstr.of_constr ty in + let open EConstr in + print_typed_value_in_env env sigma (mkConstruct cstr, ty) + | VarRef id -> + env |> lookup_named id |> print_named_decl env sigma + +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)]) + | Syntactic kn -> + let () = match Syntax_def.search_syntactic_definition kn with + | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref + | _ -> () in + v 0 ( + print_syntactic_def env kn ++ fnl () ++ + hov 0 (str "Expands to: " ++ pr_located_qualid k)) + | Dir _ | ModuleType _ | Undefined _ -> + hov 0 (pr_located_qualid k) + | Other (obj, info) -> hov 0 (info.about obj) + +let print_about env sigma na udecl = + match na with + | {loc;v=Constrexpr.ByNotation (ntn,sc)} -> + print_about_any ?loc env sigma + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) + ntn sc)) udecl + | {loc;v=Constrexpr.AN ref} -> + print_about_any ?loc env sigma (locate_any_name ref) udecl + +(* for debug *) +let inspect ~mod_ops indirect_accessor env sigma depth = + print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) + +(*************************************************************************) +(* Pretty-printing functions coming from classops.ml *) + +open Classops + +let print_coercion_value v = Printer.pr_global v.coe_value + +let print_class i = + let cl,_ = class_info_from_index i in + pr_class cl + +let print_path ((i,j),p) = + hov 2 ( + str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ + str"] : ") ++ + print_class i ++ str" >-> " ++ print_class j + +let _ = Classops.install_path_printer print_path + +let print_graph () = + prlist_with_sep fnl print_path (inheritance_graph()) + +let print_classes () = + pr_sequence pr_class (classes()) + +let print_coercions () = + pr_sequence print_coercion_value (coercions()) + +let index_of_class cl = + try + fst (class_info cl) + with Not_found -> + user_err ~hdr:"index_of_class" + (pr_class cl ++ spc() ++ str "not a defined class.") + +let print_path_between cls clt = + let i = index_of_class cls in + let j = index_of_class clt in + let p = + try + lookup_path_between_class (i,j) + with Not_found -> + user_err ~hdr:"index_cl_of_id" + (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt + ++ str ".") + in + print_path ((i,j),p) + +let print_canonical_projections env sigma = + prlist_with_sep fnl + (fun ((r1,r2),o) -> pr_cs_pattern r2 ++ + str " <- " ++ + pr_global r1 ++ str " ( " ++ pr_lconstr_env env sigma o.o_DEF ++ str " )") + (canonical_projections ()) + +(*************************************************************************) + +(*************************************************************************) +(* Pretty-printing functions for type classes *) + +open Typeclasses + +let pr_typeclass env t = + print_ref false t.cl_impl None + +let print_typeclasses () = + let env = Global.env () in + prlist_with_sep fnl (pr_typeclass env) (typeclasses ()) + +let pr_instance env i = + (* gallina_print_constant_with_infos i.is_impl *) + (* lighter *) + print_ref false (instance_impl i) None ++ + begin match hint_priority i with + | None -> mt () + | Some i -> spc () ++ str "|" ++ spc () ++ int i + end + +let print_all_instances () = + let env = Global.env () in + let inst = all_instances () in + prlist_with_sep fnl (pr_instance env) inst + +let print_instances r = + let env = Global.env () in + let sigma = Evd.from_env env in + let inst = instances env sigma r in + prlist_with_sep fnl (pr_instance env) inst diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli new file mode 100644 index 0000000000..c8b361d95b --- /dev/null +++ b/vernac/prettyp.mli @@ -0,0 +1,129 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* Termops.names_context + +val print_closed_sections : bool ref +val print_context + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t +val print_full_context_typ + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t + +val print_full_pure_context + : mod_ops:Printmod.mod_ops + -> library_accessor:Opaqueproof.indirect_accessor + -> env + -> Evd.evar_map + -> Pp.t + +val print_sec_context + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t +val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t +val print_eval : + reduction_function -> env -> Evd.evar_map -> + Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t + +val print_name + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option -> Pp.t +val print_opaque_name + : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> + UnivNames.univ_name_list option -> Pp.t +val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t + +(** Pretty-printing functions for classes and coercions *) +val print_graph : unit -> Pp.t +val print_classes : unit -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_canonical_projections : env -> Evd.evar_map -> Pp.t + +(** Pretty-printing functions for type classes and instances *) +val print_typeclasses : unit -> Pp.t +val print_instances : GlobRef.t -> Pp.t +val print_all_instances : unit -> Pp.t + +val inspect + : mod_ops:Printmod.mod_ops + -> Opaqueproof.indirect_accessor + -> env -> Evd.evar_map -> int -> Pp.t + +(** {5 Locate} *) + +type 'a locatable_info = { + locate : qualid -> 'a option; + (** Locate the most precise object with the provided name if any. *) + locate_all : qualid -> 'a list; + (** Locate all objects whose name is a suffix of the provided name *) + shortest_qualid : 'a -> qualid; + (** Return the shortest name in the current context *) + name : 'a -> Pp.t; + (** Data as printed by the Locate command *) + print : 'a -> Pp.t; + (** Data as printed by the Print command *) + about : 'a -> Pp.t; + (** Data as printed by the About command *) +} +(** Generic data structure representing locatable objects. *) + +val register_locatable : string -> 'a locatable_info -> unit +(** Define a new type of locatable objects that can be reached via the + corresponding generic vernacular commands. The string should be a unique + name describing the kind of objects considered and that is added as a + grammar command prefix for vernacular commands Locate. *) + +val print_located_qualid : qualid -> Pp.t +val print_located_term : qualid -> Pp.t +val print_located_module : qualid -> Pp.t +val print_located_other : string -> qualid -> Pp.t + +type object_pr = { + print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; + print_syntactic_def : env -> KerName.t -> Pp.t; + print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; + print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; + print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; +} + +val set_object_pr : object_pr -> unit +val default_object_pr : object_pr diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 102da20257..7563b4a5d5 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -10,6 +10,7 @@ Locality Egramml Vernacextend Ppvernac +Prettyp Proof_using Egramcoq Metasyntax -- cgit v1.2.3 From 82bdd64c97f45510044a9ccd9b5b87effcd034d1 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Oct 2019 17:55:23 +0100 Subject: Print argument info as an Arguments command in About Close #10961 --- vernac/ppvernac.ml | 7 ++- 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 @@ -162,19 +156,6 @@ let print_impargs ref = (if has_impl then print_impargs_list (mt()) impl 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 *) @@ -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)]) -- cgit v1.2.3 From b16ae82270be36e6578b36737d57a3792ae25f71 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Oct 2019 18:26:22 +0100 Subject: ppvernac: bidi hints use & not | --- vernac/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 5cffc39839..3dbf7afb78 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1082,7 +1082,7 @@ let string_of_definition_object_kind = let open Decls in function let rec print_arguments n nbidi l = 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 + | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l | None, None, [] -> mt() | _, _, [] -> let dummy = {name=Anonymous; recarg_like=false; -- cgit v1.2.3 From b6e50de7f52a24aeeca0df0175fe5e5b327bfb90 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 28 Oct 2019 19:29:48 +0100 Subject: Fix output tests --- test-suite/output/Arguments.out | 55 ++++++++---------------------- test-suite/output/ArgumentsScope.out | 10 +++--- test-suite/output/Arguments_renaming.out | 57 ++++++++------------------------ test-suite/output/Cases.out | 10 +++--- test-suite/output/Implicit.out | 3 +- test-suite/output/Inductive.out | 4 +-- test-suite/output/InitSyntax.out | 7 ++-- test-suite/output/Notations3.out | 2 +- test-suite/output/PatternsInBinders.out | 5 ++- test-suite/output/PrintInfos.out | 51 +++++++++------------------- test-suite/output/StringSyntax.out | 6 ++-- test-suite/output/UnivBinders.out | 35 ++++++++++---------- 12 files changed, 81 insertions(+), 164 deletions(-) diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 3c1e27ba9d..7bfb2fc210 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,41 +1,31 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold Nat.sub but avoid exposing match constructs +Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold Nat.sub when applied to 1 argument - but avoid exposing match constructs +Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold Nat.sub - when the 1st argument evaluates to a constructor and - when applied to 1 argument but avoid exposing match constructs +Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor and when applied to 2 arguments +Arguments Nat.sub !_%nat_scope !_%nat_scope / Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] -The reduction tactics unfold Nat.sub when the 1st and - 2nd arguments evaluate to a constructor +Arguments Nat.sub !_%nat_scope !_%nat_scope Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : @@ -43,57 +33,43 @@ forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments D2, C2 are implicit -Arguments D1, C1 are implicit and maximally inserted -Argument scopes are [foo_scope type_scope _ _ _ _ _] -The reduction tactics never unfold pf +Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never pf is transparent Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic -Arguments A, B, C are implicit and maximally inserted -Argument scopes are [type_scope type_scope type_scope _ _ _] -The reduction tactics unfold fcomp when applied to 6 arguments +Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat volatile is not universe polymorphic -Argument scope is [nat_scope] -The reduction tactics always unfold volatile +Arguments volatile / _%nat_scope volatile is transparent Expands to: Constant Arguments.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] +Arguments f _ _ _%nat_scope _ _%nat_scope f is transparent Expands to: Constant Arguments.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] -The reduction tactics unfold f when the 3rd, 4th and - 5th arguments evaluate to a constructor +Arguments f _ _ !_%nat_scope !_ !_%nat_scope f is transparent Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument T2 is implicit -Argument scopes are [type_scope _ _ nat_scope _ nat_scope] -The reduction tactics unfold f when the 4th, 5th and - 6th arguments evaluate to a constructor +Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope f is transparent Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments T1, T2 are implicit -Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] -The reduction tactics unfold f when the 5th, 6th and - 7th arguments evaluate to a constructor +Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope f is transparent Expands to: Constant Arguments.f = forall v : unit, f 0 0 5 v 3 = 2 @@ -103,8 +79,7 @@ Expands to: Constant Arguments.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -The reduction tactics unfold f when the 5th, 6th and - 7th arguments evaluate to a constructor +Arguments f _ _ _ _ !_ !_ !_ f is transparent Expands to: Constant Arguments.f forall w : r, w 3 true = tt @@ -118,9 +93,7 @@ Extra arguments: _, _. volatilematch : nat -> nat volatilematch is not universe polymorphic -Argument scope is [nat_scope] -The reduction tactics always unfold volatilematch - but avoid exposing match constructs +Arguments volatilematch / _%nat_scope : simpl nomatch volatilematch is transparent Expands to: Constant Arguments.volatilematch = fun n : nat => volatilematch n diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 69ba329ff1..7b25fd40f8 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,29 +1,29 @@ a : bool -> bool a is not universe polymorphic -Argument scope is [bool_scope] +Arguments a _%bool_scope Expands to: Variable a b : bool -> bool b is not universe polymorphic -Argument scope is [bool_scope] +Arguments b _%bool_scope Expands to: Variable b negb'' : bool -> bool negb'' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb'' _%bool_scope negb'' is transparent Expands to: Constant ArgumentsScope.A.B.negb'' negb' : bool -> bool negb' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb' _%bool_scope negb' is transparent Expands to: Constant ArgumentsScope.A.negb' negb : bool -> bool negb is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb _%bool_scope negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 65c902202d..e025c167e3 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,36 +13,21 @@ where ?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -For eq_refl: Arguments are renamed to B, y -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments B, y are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument B is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {B%type_scope} {y}, [B] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -Arguments are renamed to B, y -When applied to no arguments: - Arguments B, y are implicit and maximally inserted -When applied to 1 argument: - Argument B is implicit -Argument scopes are [type_scope _] +Arguments eq_refl {B%type_scope} {y}, [B] _ Expands to: Constructor Coq.Init.Logic.eq_refl Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x -For myrefl: Arguments are renamed to C, x, _ -For myrefl: Argument C is implicit and maximally inserted -For myEq: Argument scopes are [type_scope _ _] -For myrefl: Argument scopes are [type_scope _ _] +Arguments myEq _%type_scope +Arguments myrefl {C%type_scope} x : rename myrefl : forall (B : Type) (x : A), B -> myEq B x x myrefl is not universe polymorphic -Arguments are renamed to C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope _ _] +Arguments myrefl {C%type_scope} x : rename Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -52,17 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] -The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus @@ -70,16 +49,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x -For myrefl: Arguments are renamed to A, C, x, _ -For myrefl: Argument C is implicit and maximally inserted -For myEq: Argument scopes are [type_scope type_scope _ _] -For myrefl: Argument scopes are [type_scope type_scope _ _] +Arguments myEq _%type_scope _%type_scope +Arguments myrefl A%type_scope {C%type_scope} x : rename myrefl : forall (A B : Type) (x : A), B -> myEq A B x x myrefl is not universe polymorphic -Arguments are renamed to A, C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope type_scope _ _] +Arguments myrefl A%type_scope {C%type_scope} x : rename Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -91,17 +66,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] -The reduction tactics unfold myplus when the 2nd and - 3rd arguments evaluate to a constructor +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus is transparent Expands to: Constant Arguments_renaming.myplus @myplus diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index cb835ab48d..7489b8987e 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -Argument scopes are [function_scope function_scope _] +Arguments t_rect _%function_scope _%function_scope = fun d : TT => match d with | {| f3 := b |} => b end @@ -26,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Argument scopes are [nat_scope nat_scope function_scope _ _] +Arguments proj _%nat_scope _%nat_scope _%function_scope foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with @@ -36,14 +36,14 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -Argument scopes are [type_scope list_scope] +Arguments foo _%type_scope _%list_scope uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end : forall A : Type, I A -> A -Argument scopes are [type_scope _] +Arguments uncast _%type_scope foo' = if A 0 then true else false : bool f = @@ -82,7 +82,7 @@ lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k -Argument scope is [bool_scope] +Arguments lem2 _%bool_scope lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c29..d65d2a8f55 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,8 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments x, x0 are implicit -Argument scopes are [nat_scope nat_scope _] +Arguments d2 [x%nat_scope] [x0%nat_scope] map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index af202ea01c..8ff571ae55 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -3,5 +3,5 @@ Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x -For foo: Argument scopes are [type_scope _] -For Foo: Argument scopes are [type_scope _] +Arguments foo _%type_scope +Arguments Foo _%type_scope diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index c17c63e724..ce058a6d34 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,11 +1,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} -For sig2: Argument A is implicit -For exist2: Argument A is implicit -For sig2: Argument scopes are [type_scope type_scope type_scope] -For exist2: Argument scopes are [type_scope function_scope function_scope _ _ - _] +Arguments sig2 [A%type_scope] _%type_scope _%type_scope +Arguments exist2 [A%type_scope] _%function_scope _%function_scope exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index d32cf67e28..abada44da7 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -230,7 +230,7 @@ fun l : list nat => match l with end : list nat -> list nat -Argument scope is [list_scope] +Arguments foo _%list_scope Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation) diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 8a6d94c732..2952b6d94b 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,8 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments A, B are implicit and maximally inserted -Argument scopes are [type_scope type_scope _] +Arguments swap {A%type_scope} {B%type_scope} fun (A B : Type) '(x, y) => swap (x, y) = (y, x) : forall A B : Type, A * B -> Prop forall (A B : Type) '(x, y), swap (x, y) = (y, x) @@ -42,6 +41,6 @@ fun (pat : nat) '(x, y) => x + y = pat f = fun x : nat => x + x : nat -> nat -Argument scope is [nat_scope] +Arguments f _%nat_scope fun x : nat => x + x : nat -> nat diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index e788977fb7..7d0d81a3e8 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,36 +1,24 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 -Argument A is implicit -Argument scopes are [type_scope function_scope _ _] +Arguments existT [A%type_scope] _%function_scope Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} -For sigT: Argument A is implicit -For existT: Argument A is implicit -For sigT: Argument scopes are [type_scope type_scope] -For existT: Argument scopes are [type_scope function_scope _ _] +Arguments sigT [A%type_scope] _%type_scope +Arguments existT [A%type_scope] _%function_scope existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {A%type_scope} {x}, [A] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -When applied to no arguments: - Arguments A, x are implicit and maximally inserted -When applied to 1 argument: - Argument A is implicit -Argument scopes are [type_scope _] +Arguments eq_refl {A%type_scope} {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall (A : Type) (x : A), x = x @@ -46,11 +34,11 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add : nat -> nat -> nat Nat.add is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add is transparent Expands to: Constant Coq.Init.Nat.add Nat.add : nat -> nat -> nat @@ -58,17 +46,15 @@ Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 plus_n_O is not universe polymorphic -Argument scope is [nat_scope] +Arguments plus_n_O _%nat_scope plus_n_O is opaque Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m -For le_S: Argument m is implicit -For le_S: Argument n is implicit and maximally inserted -For le: Argument scopes are [nat_scope nat_scope] -For le_n: Argument scope is [nat_scope] -For le_S: Argument scopes are [nat_scope nat_scope _] +Arguments le _%nat_scope _%nat_scope +Arguments le_n _%nat_scope +Arguments le_S {n%nat_scope} [m%nat_scope] comparison : Set comparison is not universe polymorphic @@ -81,26 +67,21 @@ bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Module Coq.Init.Peano Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit and maximally inserted -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +Arguments eq {A%type_scope} +Arguments eq_refl {A%type_scope} {x}, {A} _ n:nat Hypothesis of the goal context. diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index 9366113c0c..e9cf4282dc 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -433,7 +433,7 @@ end P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rect _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope byte_rec = fun P : byte -> Set => byte_rect P : forall P : byte -> Set, @@ -607,7 +607,7 @@ fun P : byte -> Set => byte_rect P P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rec _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope byte_ind = fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") @@ -1043,7 +1043,7 @@ end P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope "000" : byte "a" diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d48d8b900f..298a0789c4 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -4,37 +4,36 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } (* u |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +Arguments PWrap _%type_scope +Arguments pwrap _%type_scope punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } (* u |= *) -For RWrap: Argument scope is [type_scope] -For rwrap: Argument scopes are [type_scope _] +Arguments RWrap _%type_scope +Arguments rwrap _%type_scope runwrap@{u} = fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) -Argument scopes are [type_scope _] +Arguments runwrap _%type_scope Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) -Argument scope is [type_scope] +Arguments Wrap _%type_scope wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) -Arguments A, Wrap are implicit and maximally inserted -Argument scopes are [type_scope _] +Arguments wrap {A%type_scope} {Wrap} bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) @@ -87,13 +86,13 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } (* E |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +Arguments PWrap _%type_scope +Arguments pwrap _%type_scope punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A (* K |= *) punwrap is universe polymorphic -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope punwrap is transparent Expands to: Constant UnivBinders.punwrap The command has indeed failed with message: @@ -118,7 +117,7 @@ Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} (* k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) @@ -126,7 +125,7 @@ Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} (* u k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec2@{u} = Prop : Type@{Set+1} (* u |= *) @@ -148,24 +147,24 @@ Type@{UnivBinders.59} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axfoo is universe polymorphic -Argument scope is [type_scope] +Arguments axfoo _%type_scope Expands to: Constant UnivBinders.axfoo axbar@{i UnivBinders.59 UnivBinders.60} : Type@{UnivBinders.60} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axbar is universe polymorphic -Argument scope is [type_scope] +Arguments axbar _%type_scope Expands to: Constant UnivBinders.axbar axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axfoo' is not universe polymorphic -Argument scope is [type_scope] +Arguments axfoo' _%type_scope Expands to: Constant UnivBinders.axfoo' axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axbar' is not universe polymorphic -Argument scope is [type_scope] +Arguments axbar' _%type_scope Expands to: Constant UnivBinders.axbar' The command has indeed failed with message: When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). -- cgit v1.2.3 From d9892ecc6cc647ffc8803b17350f46ce6b901410 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Oct 2019 13:14:50 +0100 Subject: changelog for #10985 --- doc/changelog/02-specification-language/10985-about-arguments.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/02-specification-language/10985-about-arguments.rst diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst new file mode 100644 index 0000000000..1e05b0b0fe --- /dev/null +++ b/doc/changelog/02-specification-language/10985-about-arguments.rst @@ -0,0 +1,5 @@ +- The output of the :cmd:`Print` and :cmd:`About` commands has + changed. Arguments meta-data is now displayed as the corresponding + :cmd:`Arguments ` command instead of the + human-targeted prose used in previous Coq versions. (`#10985 + `_, by Gaëtan Gilbert). -- cgit v1.2.3 From 777109f0068d524ca2a82d405416da273fec3d7f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 30 Oct 2019 16:30:26 +0100 Subject: restore red behaviour printing --- test-suite/output/Arguments.out | 23 +++++++++++++++++++++++ test-suite/output/Arguments_renaming.out | 4 ++++ vernac/prettyp.ml | 2 ++ 3 files changed, 29 insertions(+) diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 7bfb2fc210..6704337f80 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -2,30 +2,40 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch +The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch +The reduction tactics unfold Nat.sub when applied to 1 argument + but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch +The reduction tactics unfold Nat.sub + when the 1st argument evaluates to a constructor and + when applied to 1 argument but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Arguments Nat.sub !_%nat_scope !_%nat_scope / +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic Arguments Nat.sub !_%nat_scope !_%nat_scope +The reduction tactics unfold Nat.sub when the 1st and + 2nd arguments evaluate to a constructor Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub pf : @@ -34,18 +44,21 @@ forall D1 C1 : Type, pf is not universe polymorphic Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never +The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / +The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat volatile is not universe polymorphic Arguments volatile / _%nat_scope +The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Arguments.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat @@ -58,18 +71,24 @@ f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f _ _ !_%nat_scope !_ !_%nat_scope +The reduction tactics unfold f when the 3rd, 4th and + 5th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +The reduction tactics unfold f when the 4th, 5th and + 6th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f = forall v : unit, f 0 0 5 v 3 = 2 @@ -80,6 +99,8 @@ f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic Arguments f _ _ _ _ !_ !_ !_ +The reduction tactics unfold f when the 5th, 6th and + 7th arguments evaluate to a constructor f is transparent Expands to: Constant Arguments.f forall w : r, w 3 true = tt @@ -94,6 +115,8 @@ volatilematch : nat -> nat volatilematch is not universe polymorphic Arguments volatilematch / _%nat_scope : simpl nomatch +The reduction tactics always unfold volatilematch + but avoid exposing match constructs volatilematch is transparent Expands to: Constant Arguments.volatilematch = fun n : nat => volatilematch n diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e025c167e3..53d5624f6f 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -42,6 +42,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.Test1.myplus @myplus @@ -71,6 +73,8 @@ myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +The reduction tactics unfold myplus when the 2nd and + 3rd arguments evaluate to a constructor myplus is transparent Expands to: Constant Arguments_renaming.myplus @myplus diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 358c40bdb0..b03ff7b2ae 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -884,11 +884,13 @@ 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)]) -- cgit v1.2.3 From 85905b38c15c3d2bb73e878e6e7db180b73d468e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 31 Oct 2019 14:55:05 +0100 Subject: [prettyp] remove `mod_ops` and `indirect_accessor` parameters `Prettyp` is now late enough in linking to refer to them. --- toplevel/coqc.ml | 6 +--- vernac/declaremods.ml | 6 ++++ vernac/declaremods.mli | 2 ++ vernac/prettyp.ml | 94 ++++++++++++++++++++++++++----------------------- vernac/prettyp.mli | 62 +++++++++++--------------------- vernac/vernac.mllib | 2 +- vernac/vernacentries.ml | 21 +++++------ 7 files changed, 89 insertions(+), 104 deletions(-) diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 642dc94ab2..98206fb341 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -53,11 +53,7 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in - let library_accessor = Library.indirect_accessor in - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index c7b68d18c2..65cd4cd6a4 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -1068,3 +1068,9 @@ let debug_print_modtab _ = in let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in hov 0 modules + + +let mod_ops = { + Printmod.import_module = import_module; + process_module_binding = process_module_binding; +} diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index ae84704656..23f25bc597 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -126,3 +126,5 @@ val debug_print_modtab : unit -> Pp.t val process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + +val mod_ops : Printmod.mod_ops diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index b03ff7b2ae..5ebc89892c 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -34,20 +34,22 @@ module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } -let gallina_print_module = print_module -let gallina_print_modtype = print_modtype +let gallina_print_module = print_module ~mod_ops:Declaremods.mod_ops +let gallina_print_modtype = print_modtype ~mod_ops:Declaremods.mod_ops + + (**************) (** Utilities *) @@ -585,9 +587,9 @@ let print_instance sigma cb = pr_universe_instance sigma inst else mt() -let print_constant indirect_accessor with_values sep sp udecl = +let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body indirect_accessor cb in + let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -595,7 +597,7 @@ let print_constant indirect_accessor with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in + let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -625,8 +627,8 @@ let print_constant indirect_accessor with_values sep sp udecl = (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universes sigma univs ?priv) -let gallina_print_constant_with_infos indirect_accessor sp udecl = - print_constant indirect_accessor true " = " sp udecl ++ +let gallina_print_constant_with_infos sp udecl = + print_constant true " = " sp udecl ++ with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = @@ -642,7 +644,7 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> @@ -653,7 +655,7 @@ let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (( constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) + Some (print_constant with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| @@ -663,17 +665,17 @@ let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (( end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module ~mod_ops with_values (MPdot (mp,l))) + Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype ~mod_ops (MPdot (mp,l))) + Some (print_modtype ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = +let gallina_print_library_entry env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) + gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> @@ -681,10 +683,10 @@ let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = +let gallina_print_context env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with + (match gallina_print_library_entry env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -722,8 +724,8 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x -let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x +let print_library_entry x = !object_pr.print_library_entry x +let print_context x = !object_pr.print_context x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x let print_eval x = !object_pr.print_eval x @@ -744,12 +746,12 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) +let print_full_context env sigma = + print_context env sigma true None (Lib.contents ()) +let print_full_context_typ env sigma = + print_context env sigma false None (Lib.contents ()) -let print_full_pure_context ~mod_ops ~library_accessor env sigma = +let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with @@ -765,7 +767,9 @@ let print_full_pure_context ~mod_ops ~library_accessor env sigma = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + str "Proof " ++ pr_lconstr_env env sigma + (fst (Opaqueproof.force_proof Library.indirect_accessor + (Global.opaque_tables ()) lc)) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ @@ -784,11 +788,11 @@ let print_full_pure_context ~mod_ops ~library_accessor env sigma = | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -813,11 +817,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) +let print_sec_context env sigma sec = + print_context env sigma true None (read_sec_context sec) -let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) +let print_sec_context_typ env sigma sec = + print_context env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -827,19 +831,19 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name ~mod_ops indirect_accessor env sigma na udecl = +let print_any_name env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with - | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl + | Term (ConstRef sp) -> print_constant_with_infos sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> - print_module ~mod_ops (printable_body obj_dir) obj_mp + print_module (printable_body obj_dir) obj_mp | Dir _ -> mt () - | ModuleType mp -> print_modtype ~mod_ops mp + | ModuleType mp -> print_modtype mp | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) @@ -851,23 +855,23 @@ let print_any_name ~mod_ops indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name ~mod_ops indirect_accessor env sigma na udecl = +let print_name env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name ~mod_ops indirect_accessor env sigma + print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl + print_any_name env sigma (locate_any_name ref) udecl -let print_opaque_name indirect_accessor env sigma qid = +let print_opaque_name env sigma qid = let open GlobRef in match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in if Declareops.constant_has_body cb then - print_constant_with_infos indirect_accessor cst None + print_constant_with_infos cst None else user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> @@ -915,8 +919,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect ~mod_ops indirect_accessor env sigma depth = - print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) +let inspect env sigma depth = + print_context env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) diff --git a/vernac/prettyp.mli b/vernac/prettyp.mli index c8b361d95b..dc4280f286 100644 --- a/vernac/prettyp.mli +++ b/vernac/prettyp.mli @@ -19,48 +19,31 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map + : env + -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t -val print_full_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t - -val print_full_pure_context - : mod_ops:Printmod.mod_ops - -> library_accessor:Opaqueproof.indirect_accessor - -> env + : env -> Evd.evar_map - -> Pp.t + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context : env -> Evd.evar_map -> Pp.t +val print_full_context_typ : env -> Evd.evar_map -> Pp.t + +val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation - -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_name : env -> Evd.evar_map + -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option + -> Pp.t +val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t @@ -77,10 +60,7 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> int -> Pp.t +val inspect : env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -113,14 +93,14 @@ val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7563b4a5d5..5226c2ba65 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -10,7 +10,6 @@ Locality Egramml Vernacextend Ppvernac -Prettyp Proof_using Egramcoq Metasyntax @@ -20,6 +19,7 @@ DeclareObl Canonical RecLemmas Library +Prettyp Lemmas Class Auto_ind_decl diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4c7332f011..edff80af00 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -175,7 +175,7 @@ let print_module qid = let globdir = Nametab.locate_dir qid in match globdir with DirModule Nametab.{ obj_dir; obj_mp; _ } -> - Printmod.print_module (Printmod.printable_body obj_dir) obj_mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) @@ -183,12 +183,12 @@ let print_module qid = let print_modtype qid = try let kn = Nametab.locate_modtype qid in - Printmod.print_modtype kn + Printmod.print_modtype ~mod_ops:Declaremods.mod_ops kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Printmod.print_module false mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) @@ -1672,29 +1672,26 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ env sigma + | PrintSectionContext qid -> print_sec_context_typ env sigma qid + | PrintInspect n -> inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module ~mod_ops qid - | PrintModuleType qid -> print_modtype ~mod_ops qid + | PrintModule qid -> print_module qid + | PrintModuleType qid -> print_modtype qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name ~mod_ops Library.indirect_accessor env sigma qid udecl + print_name env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() -- cgit v1.2.3