diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comArguments.ml | 306 | ||||
| -rw-r--r-- | vernac/comArguments.mli | 19 | ||||
| -rw-r--r-- | vernac/declaremods.ml | 6 | ||||
| -rw-r--r-- | vernac/declaremods.mli | 2 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 9 | ||||
| -rw-r--r-- | vernac/prettyp.ml | 1012 | ||||
| -rw-r--r-- | vernac/prettyp.mli | 109 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 316 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 23 |
10 files changed, 1492 insertions, 312 deletions
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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open CAst +open Util +open Names +open Vernacexpr + +let smart_global r = + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob ?loc:r.loc gr; + gr + +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' = 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 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val vernac_arguments + : section_local:bool + -> 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/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/ppvernac.ml b/vernac/ppvernac.ml index f91983d31c..3dbf7afb78 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1082,8 +1082,13 @@ 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 - | _, _, [] -> mt() + | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l + | 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 new file mode 100644 index 0000000000..5ebc89892c --- /dev/null +++ b/vernac/prettyp.ml @@ -0,0 +1,1012 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu> + * on May-June 2006 for implementation of abstraction of pretty-printing of objects. + *) + +open Pp +open CErrors +open Util +open CAst +open Names +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 : 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 : 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 : 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 ~mod_ops:Declaremods.mod_ops +let gallina_print_modtype = print_modtype ~mod_ops:Declaremods.mod_ops + + + +(**************) +(** 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 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 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 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 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 (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] + else + [] in + print_type_in_type ref @ + print_primitive ref @ + type_info_for_implicit @ + print_arguments ref @ + print_if_is_coercion ref + +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 + | 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_args 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"<no body>") + +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 with_values sep sp udecl = + let cb = Global.lookup_constant sp 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 + 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 Library.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 sp udecl = + print_constant 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 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 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 with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) + | ModuleTypeObject _ -> + let (mp,l) = KerName.repr kn in + Some (print_modtype ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) + | _ -> None + +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 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 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 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 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 + +(******************************************) +(**** 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 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 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.indirect_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 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 (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 env sigma sec = + print_context env sigma true 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 + 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 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 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 (printable_body obj_dir) obj_mp + | Dir _ -> mt () + | 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 *) + 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 env sigma na udecl = + match na with + | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> + 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 env sigma (locate_any_name ref) udecl + +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 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 env sigma depth = + print_context 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..dc4280f286 --- /dev/null +++ b/vernac/prettyp.mli @@ -0,0 +1,109 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Environ +open Reductionops +open Libnames + +(** A Pretty-Printer for the Calculus of Inductive Constructions. *) + +val assumptions_for_print : Name.t list -> Termops.names_context + +val print_closed_sections : bool ref +val print_context + : env + -> Evd.evar_map + -> bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry + : env + -> Evd.evar_map + -> 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 : 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 : 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 + +(** 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 : 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 : 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 : 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 : 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; +} + +val set_object_pr : object_pr -> unit +val default_object_pr : object_pr diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 956b56e256..5226c2ba65 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -19,6 +19,7 @@ DeclareObl Canonical RecLemmas Library +Prettyp Lemmas Class Auto_ind_decl @@ -38,6 +39,7 @@ Assumptions Mltop Topfmt Loadpath +ComArguments Vernacentries Vernacstate Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 684d8a3d90..edff80af00 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 @@ -176,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) @@ -184,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) @@ -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; @@ -1962,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() @@ -2453,7 +2160,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) |