diff options
Diffstat (limited to 'vernac')
32 files changed, 2192 insertions, 679 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index cb034bdff6..dacef1cb18 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -135,11 +135,13 @@ let lookup_constant_in_impl cst fallback = | None -> anomaly (str "Print Assumption: unknown constant " ++ Constant.print cst ++ str ".") let lookup_constant cst = - try - let cb = Global.lookup_constant cst in + let env = Global.env() in + if not (Environ.mem_constant cst env) + then lookup_constant_in_impl cst None + else + let cb = Environ.lookup_constant cst env in if Declareops.constant_has_body cb then cb else lookup_constant_in_impl cst (Some cb) - with Not_found -> lookup_constant_in_impl cst None let lookup_mind_in_impl mind = try @@ -150,8 +152,9 @@ let lookup_mind_in_impl mind = anomaly (str "Print Assumption: unknown inductive " ++ MutInd.print mind ++ str ".") let lookup_mind mind = - try Global.lookup_mind mind - with Not_found -> lookup_mind_in_impl mind + let env = Global.env() in + if Environ.mem_mind mind env then Environ.lookup_mind mind env + else lookup_mind_in_impl mind (** Graph traversal of an object, collecting on the way the dependencies of traversed objects *) diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 6af454eee5..b7a3b002bd 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -18,13 +18,17 @@ and vernac_flag_value = | VernacFlagLeaf of string | VernacFlagList of vernac_flags +let warn_unsupported_attributes = + CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError + (fun atts -> + let keys = List.map fst atts in + let keys = List.sort_uniq String.compare keys in + let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in + Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")) + let unsupported_attributes = function | [] -> () - | atts -> - let keys = List.map fst atts in - let keys = List.sort_uniq String.compare keys in - let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in - user_err Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".") + | atts -> warn_unsupported_attributes atts type 'a key_parser = 'a option -> vernac_flag_value -> 'a diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 98fe436a22..5822a1a586 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -248,6 +248,7 @@ let build_beq_scheme mode kn = | Meta _ -> raise (EqUnknown "meta-variable") | Evar _ -> raise (EqUnknown "existential variable") | Int _ -> raise (EqUnknown "int") + | Float _ -> raise (EqUnknown "float") in aux t in diff --git a/vernac/classes.ml b/vernac/classes.ml index 0a8c4e6b0f..e9a0ed7c34 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -47,7 +47,7 @@ let add_instance_hint inst path local info poly = in Flags.silently (fun () -> Hints.add_hints ~local [typeclasses_db] - (Hints.HintsResolveEntry + (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst'])) () let is_local_for_hint i = @@ -210,7 +210,7 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in try let info = abs_context cl in - let ctx = info.Lib.abstr_ctx in + let ctx = info.Section.abstr_ctx in let ctx, subst = rel_of_variable_context ctx in let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in let context = discharge_context ctx (subst, usubst) cl.cl_context in @@ -287,7 +287,7 @@ let type_ctx_instance ~program_mode env sigma ctx inst subst = decl :: ctx -> let t' = substl subst (RelDecl.get_type decl) in let (sigma, c'), l = - match decl with + match decl with | LocalAssum _ -> interp_casted_constr_evars ~program_mode env sigma (List.hd l) t', List.tl l | LocalDef (_,b,_) -> (sigma, substl subst b), l in @@ -301,8 +301,8 @@ let id_of_class cl = match cl.cl_impl with | ConstRef kn -> Label.to_id @@ Constant.label kn | IndRef (kn,i) -> - let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in - mip.(0).Declarations.mind_typename + let mip = (Environ.lookup_mind kn (Global.env ())).Declarations.mind_packets in + mip.(0).Declarations.mind_typename | _ -> assert false let instance_hook info global imps ?hook cst = @@ -314,18 +314,12 @@ let instance_hook info global imps ?hook cst = (match hook with Some h -> h cst | None -> ()) let declare_instance_constant info global imps ?hook name decl poly sigma term termtype = - (* XXX: Duplication of the declare_constant path *) - let sigma = - let levels = Univ.LSet.union (CVars.universes_of_constr termtype) - (CVars.universes_of_constr term) in - Evd.restrict_universe_context sigma levels - in - let uctx = Evd.check_univ_decl ~poly sigma decl in let kind = Decls.(IsDefinition Instance) in - let entry = Declare.definition_entry ~types:termtype ~univs:uctx term in + let sigma, entry = DeclareDef.prepare_definition + ~allow_evars:false ~poly sigma decl ~types:(Some termtype) ~body:term in let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in Declare.definition_message name; - Declare.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma); instance_hook info global imps ?hook (GlobRef.ConstRef kn) let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst name = @@ -338,10 +332,10 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst nam let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~name ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in - Declare.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma); instance_hook pri global imps (GlobRef.ConstRef cst) -let declare_instance_program env sigma ~global ~poly id pri imps decl term termtype = +let declare_instance_program env sigma ~global ~poly name pri imps univdecl term termtype = let hook { DeclareDef.Hook.S.scope; dref; _ } = let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in Impargs.declare_manual_implicits false dref imps; @@ -350,19 +344,13 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt let sigma = Evd.from_env env in declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst) in - let obls, constr, typ = - match term with - | Some t -> - let termtype = EConstr.of_constr termtype in - let obls, _, constr, typ = - Obligations.eterm_obligations env id sigma 0 t termtype - in obls, Some constr, typ - | None -> [||], None, termtype - in + let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in let hook = DeclareDef.Hook.make hook in let ctx = Evd.evar_universe_context sigma in - ignore(Obligations.add_definition ~name:id ?term:constr - ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Decls.Instance ~hook typ ctx obls) + let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in + let _ : DeclareObl.progress = + Obligations.add_definition ~name ~term ~univdecl ~scope ~poly ~kind ~hook typ ctx obls + in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype = (* spiwack: it is hard to reorder the actions to do @@ -374,20 +362,24 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t let kind = Decls.(IsDefinition Instance) in let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in let info = Lemmas.Info.make ~hook ~kind () in - let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in + (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! + This is due to a bug in proof_global :( *) + let termtype = Evarutil.nf_evar sigma termtype in + let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = - if not (Option.is_empty term) then + match term with + | Some term -> let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); + Refine.refine ~typecheck:false (fun sigma -> sigma, term); Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); Tactics.New.reduce_after_refine; ] in let lemma, _ = Lemmas.by init_refine lemma in lemma - else + | None -> let lemma, _ = Lemmas.by (Tactics.auto_intros_tac ids) lemma in lemma in @@ -419,7 +411,6 @@ let do_instance_resolve_TC term termtype sigma env = let sigma = Evd.minimize_universes sigma in (* Check that the type is free of evars now. *) Pretyping.check_evars env (Evd.from_env env) sigma termtype; - let termtype = to_constr sigma termtype in termtype, sigma let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = @@ -459,9 +450,9 @@ let do_instance_type_ctx_instance props k env' ctx' sigma ~program_mode subst = let do_instance_interactive env sigma ?hook ~tac ~global ~poly cty k u ctx ctx' pri decl imps subst id = let term, termtype = if List.is_empty k.cl_props then - let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - Some term, termtype + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + Some term, termtype else None, it_mkProd_or_LetIn cty ctx in let termtype, sigma = do_instance_resolve_TC term termtype sigma env in @@ -489,7 +480,6 @@ let do_instance env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imp if Evd.has_undefined sigma then CErrors.user_err Pp.(str "Unsolved obligations remaining.") else - let term = to_constr sigma term in declare_instance_constant pri global imps ?hook id decl poly sigma term termtype let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri decl imps subst id opt_props = @@ -499,24 +489,23 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri check_duplicate ?loc fs; let subst, sigma = do_instance_type_ctx_instance fs k env' ctx' sigma ~program_mode:true subst in - let term, termtype = - do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - Some term, termtype, sigma + let term, termtype = + do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in + term, termtype, sigma | Some (_, term) -> let sigma, def = interp_casted_constr_evars ~program_mode:true env' sigma term cty in let termtype = it_mkProd_or_LetIn cty ctx in let term = it_mkLambda_or_LetIn def ctx in - Some term, termtype, sigma + term, termtype, sigma | None -> let subst, sigma = do_instance_type_ctx_instance [] k env' ctx' sigma ~program_mode:true subst in let term, termtype = do_instance_subst_constructor_and_ty subst k u (ctx' @ ctx) in - Some term, termtype, sigma in + term, termtype, sigma in let termtype, sigma = do_instance_resolve_TC term termtype sigma env in if not (Evd.has_undefined sigma) && not (Option.is_empty opt_props) then - let term = to_constr sigma (Option.get term) in declare_instance_constant pri global imps ?hook id decl poly sigma term termtype else declare_instance_program env sigma ~global ~poly id pri imps decl term termtype 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/comAssumption.ml b/vernac/comAssumption.ml index a0b0dcf4c8..e5db6146ca 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -69,7 +69,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name let kn = Declare.declare_constant ~name ~local ~kind decl in let gr = GlobRef.ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in + let () = DeclareUniv.declare_univ_binders gr pl in let () = Declare.assumption_message name in let env = Global.env () in let sigma = Evd.from_env env in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 98b869d72e..36aa7a37a2 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -15,18 +15,15 @@ open Util open Constr open Context open Environ -open Declare open Names open Libnames open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Impargs open Reductionops open Type_errors open Pretyping -open Indschemes open Context.Rel.Declaration open Entries @@ -80,12 +77,6 @@ type structured_one_inductive_expr = { ind_lc : (Id.t * constr_expr) list } -let minductive_message = function - | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (Id.print x ++ str " is defined") - | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++ - spc () ++ str "are defined") - let check_all_names_different indl = let ind_names = List.map (fun ind -> ind.ind_name) indl in let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in @@ -363,6 +354,67 @@ let restrict_inductive_universes sigma ctx_params arities constructors = let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in Evd.restrict_universe_context sigma uvars +let interp_mutual_inductive_constr ~env0 ~sigma ~template ~udecl ~env_ar ~env_params ~ctx_params ~indnames ~arities ~arityconcl ~constructors ~env_ar_params ~cumulative ~poly ~private_ind ~finite = + (* Compute renewed arities *) + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in + let constructors = List.map (on_pi2 (List.map nf)) constructors in + let arities = List.map EConstr.(to_constr sigma) arities in + let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in + let sigma, arities = inductive_levels env_ar_params sigma arities constructors in + let sigma = Evd.minimize_universes sigma in + let nf = Evarutil.nf_evars_universes sigma in + let arities = List.map (on_snd nf) arities in + let constructors = List.map (on_pi2 (List.map nf)) constructors in + let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in + let arityconcl = List.map (Option.map (fun (_anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in + let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in + let uctx = Evd.check_univ_decl ~poly sigma udecl in + List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities; + Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; + List.iter (fun (_,ctyps,_) -> + List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) + constructors; + + (* Build the inductive entries *) + let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes,cimpls) -> + let template_candidate () = + templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in + let template = match template with + | Some template -> + if poly && template then user_err + Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); + if template && not (template_candidate ()) then + user_err Pp.(strbrk "Inductive " ++ Id.print indname ++ + str" cannot be made template polymorphic."); + template + | None -> + should_auto_template indname (template_candidate ()) + in + { mind_entry_typename = indname; + mind_entry_arity = arity; + mind_entry_template = template; + mind_entry_consnames = cnames; + mind_entry_lc = ctypes + }) + indnames arities arityconcl constructors + in + let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in + (* Build the mutual inductive entry *) + let mind_ent = + { mind_entry_params = ctx_params; + mind_entry_record = None; + mind_entry_finite = finite; + mind_entry_inds = entries; + mind_entry_private = if private_ind then Some false else None; + mind_entry_universes = uctx; + mind_entry_variance = variance; + } + in + (if poly && cumulative then + InferCumulativity.infer_inductive env_ar mind_ent + else mind_ent), Evd.universe_binders sigma + let interp_params env udecl uparamsl paramsl = let sigma, udecl = interp_univ_decl_opt env udecl in let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) = @@ -441,73 +493,16 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_uparams) fullarities in let env_ar = push_types env0 indnames relevances fullarities in let env_ar_params = EConstr.push_rel_context ctx_params env_ar in - (* Try further to solve evars, and instantiate them *) let sigma = solve_remaining_evars all_and_fail_flags env_params sigma in - (* Compute renewed arities *) - let sigma = Evd.minimize_universes sigma in - let nf = Evarutil.nf_evars_universes sigma in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in - let arities = List.map EConstr.(to_constr sigma) arities in - let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in - let sigma, arities = inductive_levels env_ar_params sigma arities constructors in - let sigma = Evd.minimize_universes sigma in - let nf = Evarutil.nf_evars_universes sigma in - let arities = List.map (fun (template, arity) -> template, nf arity) arities in - let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in - let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in - let arityconcl = List.map (Option.map (fun (anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in - let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in - let uctx = Evd.check_univ_decl ~poly sigma udecl in - List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities; - Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params; - List.iter (fun (_,ctyps,_) -> - List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps) - constructors; - - (* Build the inductive entries *) - let entries = List.map4 (fun ind (templatearity, arity) concl (cnames,ctypes,cimpls) -> - let template_candidate () = - templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in - let template = match template with - | Some template -> - if poly && template then user_err - Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible."); - if template && not (template_candidate ()) then - user_err Pp.(strbrk "Inductive " ++ Id.print ind.ind_name ++ - str" cannot be made template polymorphic."); - template - | None -> - should_auto_template ind.ind_name (template_candidate ()) - in - { mind_entry_typename = ind.ind_name; - mind_entry_arity = arity; - mind_entry_template = template; - mind_entry_consnames = cnames; - mind_entry_lc = ctypes - }) - indl arities arityconcl constructors - in let impls = - List.map2 (fun indimpls (_,_,cimpls) -> + List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> - userimpls @ impls) cimpls) indimpls constructors - in - let variance = if poly && cumulative then Some (InferCumulativity.dummy_variance uctx) else None in - (* Build the mutual inductive entry *) - let mind_ent = - { mind_entry_params = ctx_params; - mind_entry_record = None; - mind_entry_finite = finite; - mind_entry_inds = entries; - mind_entry_private = if private_ind then Some false else None; - mind_entry_universes = uctx; - mind_entry_variance = variance; - } + userimpls @ impls) cimpls) indimpls constructors in - (if poly && cumulative then - InferCumulativity.infer_inductive env_ar mind_ent - else mind_ent), Evd.universe_binders sigma, impls + let mie, pl = interp_mutual_inductive_constr ~env0 ~template ~sigma ~env_params ~env_ar ~ctx_params ~udecl ~arities ~arityconcl ~constructors ~env_ar_params ~poly ~finite ~cumulative ~private_ind ~indnames in + (mie, pl, impls) + (* Very syntactical equality *) let eq_local_binders bl1 bl2 = @@ -541,62 +536,6 @@ let extract_mutual_inductive_declaration_components indl = let indl = extract_inductive indl in (params,indl), coes, List.flatten ntnl -let is_recursive mie = - let rec is_recursive_constructor lift typ = - match Constr.kind typ with - | Prod (_,arg,rest) -> - not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || - is_recursive_constructor (lift+1) rest - | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest - | _ -> false - in - match mie.mind_entry_inds with - | [ind] -> - let nparams = List.length mie.mind_entry_params in - List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc - | _ -> false - -let warn_non_primitive_record = - CWarnings.create ~name:"non-primitive-record" ~category:"record" - (fun indsp -> - (hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ - strbrk" could not be defined as a primitive record"))) - -let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = - (* spiwack: raises an error if the structure is supposed to be non-recursive, - but isn't *) - begin match mie.mind_entry_finite with - | Declarations.BiFinite when is_recursive mie -> - if Option.has_some mie.mind_entry_record then - user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") - else - user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) - | _ -> () - end; - let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in - let (_, kn), prim = declare_mind mie in - let mind = Global.mind_of_delta_kn kn in - if primitive_expected && not prim then warn_non_primitive_record (mind,0); - Declare.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; - List.iteri (fun i (indimpls, constrimpls) -> - let ind = (mind,i) in - let gr = GlobRef.IndRef ind in - maybe_declare_manual_implicits false gr indimpls; - List.iteri - (fun j impls -> - maybe_declare_manual_implicits false - (GlobRef.ConstructRef (ind, succ j)) impls) - constrimpls) - impls; - Flags.if_verbose Feedback.msg_info (minductive_message names); - if mie.mind_entry_private == None - then declare_default_schemes mind; - mind - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - type uniform_inductive_flag = | UniformParameters | NonUniformParameters @@ -607,7 +546,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in (* Declare the mutual inductive block with its associated schemes *) - ignore (declare_mutual_inductive_with_eliminations mie pl impls); + ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls); (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) @@ -652,3 +591,5 @@ let make_cases ind = let consref = GlobRef.ConstructRef (ith_constructor_of_inductive ind (i + 1)) in (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l) mip.mind_nf_lc [] + +let declare_mutual_inductive_with_eliminations = DeclareInd.declare_mutual_inductive_with_eliminations diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index 7587bd165f..45e539b1e4 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Entries open Vernacexpr open Constrexpr @@ -42,22 +41,37 @@ val do_mutual_inductive val make_cases : Names.inductive -> string list list +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> DeclareInd.one_inductive_impls list + -> Names.MutInd.t + [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"] + +val interp_mutual_inductive_constr : + env0:Environ.env -> + sigma:Evd.evar_map -> + template:bool option -> + udecl:UState.universe_decl -> + env_ar:Environ.env -> + env_params:Environ.env -> + ctx_params:(EConstr.t, EConstr.t) Context.Rel.Declaration.pt list -> + indnames:Names.Id.t list -> + arities:EConstr.t list -> + arityconcl:(bool * EConstr.ESorts.t) option list -> + constructors:(Names.Id.t list * Constr.constr list * 'a list list) list -> + env_ar_params:Environ.env -> + cumulative:bool -> + poly:bool -> + private_ind:bool -> + finite:Declarations.recursivity_kind -> + Entries.mutual_inductive_entry * UnivNames.universe_binders + (************************************************************************) (** Internal API, exported for Record *) (************************************************************************) -(** Registering a mutual inductive definition together with its - associated schemes *) - -type one_inductive_impls = - Impargs.manual_implicits (* for inds *) * - Impargs.manual_implicits list (* for constrs *) - -val declare_mutual_inductive_with_eliminations : - ?primitive_expected:bool -> - mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list -> - MutInd.t - val should_auto_template : Id.t -> bool -> bool (** [should_auto_template x b] is [true] when [b] is [true] and we automatically use template polymorphism. [x] is the name of the @@ -72,7 +86,3 @@ val template_polymorphism_candidate : can be made parametric in its conclusion sort, if one is given. If the [Template Check] flag is false we just check that the conclusion sort is not small. *) - -val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t -(** [sign_level env sigma ctx] computes the universe level of the context [ctx] - as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 67733c95a1..e57c324c9a 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -44,7 +44,7 @@ end (* Locality stuff *) let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = - let fix_exn = Future.fix_exn_of ce.proof_entry_body in + let fix_exn = Declare.Internal.get_fix_exn ce in let gr = match scope with | Discharge -> let () = @@ -54,7 +54,7 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps = | Global local -> let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in let gr = Names.GlobRef.ConstRef kn in - let () = Declare.declare_univ_binders gr udecl in + let () = DeclareUniv.declare_univ_binders gr udecl in gr in let () = maybe_declare_manual_implicits false gr imps in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index d6001f5970..1bb6620886 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -62,11 +62,16 @@ val declare_fix -> Impargs.manual_implicits -> GlobRef.t -val prepare_definition : allow_evars:bool -> - ?opaque:bool -> ?inline:bool -> poly:bool -> - Evd.evar_map -> UState.universe_decl -> - types:EConstr.t option -> body:EConstr.t -> - Evd.evar_map * Evd.side_effects Declare.proof_entry +val prepare_definition + : allow_evars:bool + -> ?opaque:bool + -> ?inline:bool + -> poly:bool + -> Evd.evar_map + -> UState.universe_decl + -> types:EConstr.t option + -> body:EConstr.t + -> Evd.evar_map * Evd.side_effects Declare.proof_entry val prepare_parameter : allow_evars:bool -> poly:bool -> Evd.evar_map -> UState.universe_decl -> EConstr.types -> diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml new file mode 100644 index 0000000000..2375028541 --- /dev/null +++ b/vernac/declareInd.ml @@ -0,0 +1,214 @@ +(************************************************************************) +(* * 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 Entries + +(** Declaration of inductive blocks *) +let declare_inductive_argument_scopes kn mie = + List.iteri (fun i {mind_entry_consnames=lc} -> + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.IndRef (kn,i)); + for j=1 to List.length lc do + Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstructRef ((kn,i),j)); + done) mie.mind_entry_inds + +type inductive_obj = { + ind_names : (Id.t * Id.t list) list + (* For each block, name of the type + name of constructors *) +} + +let inductive_names sp kn obj = + let (dp,_) = Libnames.repr_path sp in + let kn = Global.mind_of_delta_kn kn in + let names, _ = + List.fold_left + (fun (names, n) (typename, consnames) -> + let ind_p = (kn,n) in + let names, _ = + List.fold_left + (fun (names, p) l -> + let sp = + Libnames.make_path dp l + in + ((sp, GlobRef.ConstructRef (ind_p,p)) :: names, p+1)) + (names, 1) consnames in + let sp = Libnames.make_path dp typename + in + ((sp, GlobRef.IndRef ind_p) :: names, n+1)) + ([], 0) obj.ind_names + in names + +let load_inductive i ((sp, kn), names) = + let names = inductive_names sp kn names in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names + +let open_inductive i ((sp, kn), names) = + let names = inductive_names sp kn names in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names + +let cache_inductive ((sp, kn), names) = + let names = inductive_names sp kn names in + List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names + +let discharge_inductive ((sp, kn), names) = + Some names + +let inInductive : inductive_obj -> Libobject.obj = + let open Libobject in + declare_object {(default_object "INDUCTIVE") with + cache_function = cache_inductive; + load_function = load_inductive; + open_function = open_inductive; + classify_function = (fun a -> Substitute a); + subst_function = ident_subst_function; + discharge_function = discharge_inductive; + } + + +let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c + +let load_prim _ p = cache_prim p + +let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c + +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) + +let inPrim : (Projection.Repr.t * Constant.t) -> Libobject.obj = + let open Libobject in + declare_object { + (default_object "PRIMPROJS") with + cache_function = cache_prim ; + load_function = load_prim; + subst_function = subst_prim; + classify_function = (fun x -> Substitute x); + discharge_function = discharge_prim } + +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) + +let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = + let name = Label.to_id label in + let univs, u = match univs with + | Monomorphic_entry _ -> + (* Global constraints already defined through the inductive *) + Monomorphic_entry Univ.ContextSet.empty, Univ.Instance.empty + | Polymorphic_entry (nas, ctx) -> + Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx + in + let term = Vars.subst_instance_constr u term in + let types = Vars.subst_instance_constr u types in + let entry = Declare.definition_entry ~types ~univs term in + let cst = Declare.declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (Declare.DefinitionEntry entry) in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + declare_primitive_projection p cst + +let declare_projections univs mind = + let env = Global.env () in + let mib = Environ.lookup_mind mind env in + let open Declarations in + match mib.mind_record with + | PrimRecord info -> + let iter_ind i (_, labs, _, _) = + let ind = (mind, i) in + let projs = Inductiveops.compute_projections env ind in + CArray.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs + in + let () = Array.iteri iter_ind info in + true + | FakeRecord -> false + | NotRecord -> false + +let feedback_axiom () = Feedback.(feedback AddedAxiom) + +let is_unsafe_typing_flags () = + let open Declarations in + let flags = Environ.typing_flags (Global.env()) in + not (flags.check_universes && flags.check_guarded && flags.check_positive) + +(* for initial declaration *) +let declare_mind mie = + let id = match mie.mind_entry_inds with + | ind::_ -> ind.mind_entry_typename + | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in + let map_names mip = (mip.mind_entry_typename, mip.mind_entry_consnames) in + let names = List.map map_names mie.mind_entry_inds in + List.iter (fun (typ, cons) -> + Declare.check_exists typ; + List.iter Declare.check_exists cons) names; + let _kn' = Global.add_mind id mie in + let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in + if is_unsafe_typing_flags() then feedback_axiom (); + let mind = Global.mind_of_delta_kn kn in + let isprim = declare_projections mie.mind_entry_universes mind in + Impargs.declare_mib_implicits mind; + declare_inductive_argument_scopes mind mie; + oname, isprim + +let is_recursive mie = + let open Constr in + let rec is_recursive_constructor lift typ = + match Constr.kind typ with + | Prod (_,arg,rest) -> + not (EConstr.Vars.noccurn Evd.empty (* FIXME *) lift (EConstr.of_constr arg)) || + is_recursive_constructor (lift+1) rest + | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest + | _ -> false + in + match mie.mind_entry_inds with + | [ind] -> + let nparams = List.length mie.mind_entry_params in + List.exists (fun t -> is_recursive_constructor (nparams+1) t) ind.mind_entry_lc + | _ -> false + +let warn_non_primitive_record = + CWarnings.create ~name:"non-primitive-record" ~category:"record" + (fun indsp -> + Pp.(hov 0 (str "The record " ++ Nametab.pr_global_env Id.Set.empty (GlobRef.IndRef indsp) ++ + strbrk" could not be defined as a primitive record"))) + +let minductive_message = function + | [] -> CErrors.user_err Pp.(str "No inductive definition.") + | [x] -> Pp.(Id.print x ++ str " is defined") + | l -> Pp.(hov 0 (prlist_with_sep pr_comma Id.print l ++ + spc () ++ str "are defined")) + +type one_inductive_impls = + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) + +let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls = + (* spiwack: raises an error if the structure is supposed to be non-recursive, + but isn't *) + begin match mie.mind_entry_finite with + | Declarations.BiFinite when is_recursive mie -> + if Option.has_some mie.mind_entry_record then + CErrors.user_err Pp.(str "Records declared with the keywords Record or Structure cannot be recursive. You can, however, define recursive records using the Inductive or CoInductive command.") + else + CErrors.user_err Pp.(str ("Types declared with the keyword Variant cannot be recursive. Recursive types are defined with the Inductive and CoInductive command.")) + | _ -> () + end; + let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in + let (_, kn), prim = declare_mind mie in + let mind = Global.mind_of_delta_kn kn in + if primitive_expected && not prim then warn_non_primitive_record (mind,0); + DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl; + List.iteri (fun i (indimpls, constrimpls) -> + let ind = (mind,i) in + let gr = GlobRef.IndRef ind in + Impargs.maybe_declare_manual_implicits false gr indimpls; + List.iteri + (fun j impls -> + Impargs.maybe_declare_manual_implicits false + (GlobRef.ConstructRef (ind, succ j)) impls) + constrimpls) + impls; + Flags.if_verbose Feedback.msg_info (minductive_message names); + if mie.mind_entry_private == None + then Indschemes.declare_default_schemes mind; + mind diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli new file mode 100644 index 0000000000..df8895a999 --- /dev/null +++ b/vernac/declareInd.mli @@ -0,0 +1,23 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** Registering a mutual inductive definition together with its + associated schemes *) + +type one_inductive_impls = + Impargs.manual_implicits (* for inds *) * + Impargs.manual_implicits list (* for constrs *) + +val declare_mutual_inductive_with_eliminations + : ?primitive_expected:bool + -> Entries.mutual_inductive_entry + -> UnivNames.universe_binders + -> one_inductive_impls list + -> Names.MutInd.t diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 2c56f707f1..b56b9c8ce2 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -490,10 +490,8 @@ let obligation_terminator entries uctx { name; num; auto } = | [entry] -> let env = Global.env () in let ty = entry.Declare.proof_entry_type in - let body, eff = Future.force entry.Declare.proof_entry_body in - let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in + let body, uctx = Declare.inline_private_constants ~univs:uctx env entry in let sigma = Evd.from_ctx uctx in - let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); (* Declare the obligation ourselves and drop the hook *) let prg = CEphemeron.get (ProgMap.find name !from_prg) in diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml new file mode 100644 index 0000000000..69ba9d76ec --- /dev/null +++ b/vernac/declareUniv.ml @@ -0,0 +1,110 @@ +(************************************************************************) +(* * 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 + +type universe_source = + | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) + | QualifiedUniv of Id.t (* global universe introduced by some global value *) + | UnqualifiedUniv (* other global universe *) + +type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list + +let check_exists_universe sp = + if Nametab.exists_universe sp then + raise (Declare.AlreadyDeclared (Some "Universe", Libnames.basename sp)) + else () + +let qualify_univ i dp src id = + match src with + | BoundUniv | UnqualifiedUniv -> + i, Libnames.make_path dp id + | QualifiedUniv l -> + let dp = DirPath.repr dp in + Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id + +let do_univ_name ~check i dp src (id,univ) = + let i, sp = qualify_univ i dp src id in + if check then check_exists_universe sp; + Nametab.push_universe i sp univ + +let cache_univ_names ((sp, _), (src, univs)) = + let depth = Lib.sections_depth () in + let dp = Libnames.pop_dirpath_n depth (Libnames.dirpath sp) in + List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs + +let load_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Until i) (Libnames.dirpath sp) src) univs + +let open_univ_names i ((sp, _), (src, univs)) = + List.iter (do_univ_name ~check:false (Nametab.Exactly i) (Libnames.dirpath sp) src) univs + +let discharge_univ_names = function + | _, (BoundUniv, _) -> None + | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x + +let input_univ_names : universe_name_decl -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Global universe name state") with + cache_function = cache_univ_names; + load_function = load_univ_names; + open_function = open_univ_names; + discharge_function = discharge_univ_names; + subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); + classify_function = (fun a -> Substitute a) } + +let declare_univ_binders gr pl = + if Global.is_polymorphic gr then + () + else + let l = let open GlobRef in match gr with + | ConstRef c -> Label.to_id @@ Constant.label c + | IndRef (c, _) -> Label.to_id @@ MutInd.label c + | VarRef id -> + CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") + | ConstructRef _ -> + CErrors.anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on an constructor reference") + in + let univs = Id.Map.fold (fun id univ univs -> + match Univ.Level.name univ with + | None -> assert false (* having Prop/Set/Var as binders is nonsense *) + | Some univ -> (id,univ)::univs) pl [] + in + Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) + +let do_universe ~poly l = + let in_section = Global.sections_are_opened () in + let () = + if poly && not in_section then + CErrors.user_err ~hdr:"Constraint" + (Pp.str"Cannot declare polymorphic universes outside sections") + in + let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in + let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) + Univ.LSet.empty l, Univ.Constraint.empty + in + let src = if poly then BoundUniv else UnqualifiedUniv in + let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in + Declare.declare_universe_context ~poly ctx + +let do_constraint ~poly l = + let open Univ in + let u_of_id x = + Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x + in + let constraints = List.fold_left (fun acc (l, d, r) -> + let lu = u_of_id l and ru = u_of_id r in + Constraint.add (lu, d, ru) acc) + Constraint.empty l + in + let uctx = ContextSet.add_constraints constraints ContextSet.empty in + Declare.declare_universe_context ~poly uctx diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli new file mode 100644 index 0000000000..ce2a6e225c --- /dev/null +++ b/vernac/declareUniv.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* * 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 + +(** Global universe contexts, names and constraints *) +val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit + +val do_universe : poly:bool -> lident list -> unit +val do_constraint : poly:bool -> Glob_term.glob_constraint 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/g_vernac.mlg b/vernac/g_vernac.mlg index efcb2635be..b4c0a33585 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -244,7 +244,8 @@ GRAMMAR EXTEND Gram ; register_type_token: - [ [ "#int63_type" -> { CPrimitives.PT_int63 } ] ] + [ [ "#int63_type" -> { CPrimitives.PT_int63 } + | "#float64_type" -> { CPrimitives.PT_float64 } ] ] ; register_prim_token: @@ -272,6 +273,24 @@ GRAMMAR EXTEND Gram | "#int63_lt" -> { CPrimitives.Int63lt } | "#int63_le" -> { CPrimitives.Int63le } | "#int63_compare" -> { CPrimitives.Int63compare } + | "#float64_opp" -> { CPrimitives.Float64opp } + | "#float64_abs" -> { CPrimitives.Float64abs } + | "#float64_eq" -> { CPrimitives.Float64eq } + | "#float64_lt" -> { CPrimitives.Float64lt } + | "#float64_le" -> { CPrimitives.Float64le } + | "#float64_compare" -> { CPrimitives.Float64compare } + | "#float64_classify" -> { CPrimitives.Float64classify } + | "#float64_add" -> { CPrimitives.Float64add } + | "#float64_sub" -> { CPrimitives.Float64sub } + | "#float64_mul" -> { CPrimitives.Float64mul } + | "#float64_div" -> { CPrimitives.Float64div } + | "#float64_sqrt" -> { CPrimitives.Float64sqrt } + | "#float64_of_int63" -> { CPrimitives.Float64ofInt63 } + | "#float64_normfr_mantissa" -> { CPrimitives.Float64normfr_mantissa } + | "#float64_frshiftexp" -> { CPrimitives.Float64frshiftexp } + | "#float64_ldshiftexp" -> { CPrimitives.Float64ldshiftexp } + | "#float64_next_up" -> { CPrimitives.Float64next_up } + | "#float64_next_down" -> { CPrimitives.Float64next_down } ] ] ; @@ -418,19 +437,19 @@ GRAMMAR EXTEND Gram rec_definition: [ [ id_decl = ident_decl; bl = binders_fixannot; - rtype = type_cstr; + rtype = rec_type_cstr; body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> { let binders, rec_order = bl in {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} } ] ] ; corec_definition: - [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + [ [ id_decl = ident_decl; binders = binders; rtype = rec_type_cstr; body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} } ]] ; - type_cstr: + rec_type_cstr: [ [ ":"; c=lconstr -> { c } | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ] ; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index e49277c51b..865eded545 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -17,15 +17,10 @@ open Pp open Names open Constr open Declareops -open Entries open Nameops open Pretyping -open Termops -open Reductionops -open Constrintern open Impargs -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* Support for terminators and proofs with an associated constant @@ -113,13 +108,6 @@ let by tac pf = (* Creating a lemma-like constant *) (************************************************************************) -let check_name_freshness locality {CAst.loc;v=id} : unit = - (* We check existence here: it's a bit late at Qed time *) - if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || - locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) - then - user_err ?loc (Id.print id ++ str " already exists.") - let initialize_named_context_for_proof () = let sign = Global.named_context () in List.fold_right @@ -193,41 +181,6 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua | None -> p | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma -let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms = - let env0 = Global.env () in - let decl = fst (List.hd thms) in - let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in - let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> - let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in - let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in - let flags = { all_and_fail_flags with program_mode } in - let hook = inference_hook in - let evd = solve_remaining_evars ?hook flags env evd in - let ids = List.map RelDecl.get_name ctx in - check_name_freshness scope id; - (* XXX: The nf_evar is critical !! *) - evd, (id.CAst.v, - (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), - (ids, imps @ imps')))) - evd thms in - let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in - let evd = Evd.minimize_universes evd in - (* XXX: This nf_evar is critical too!! We are normalizing twice if - you look at the previous lines... *) - let thms = List.map (fun (name, (typ, (args, impargs))) -> - { Recthm.name; typ = nf_evar evd typ; args; impargs} ) thms in - let () = - let open UState in - if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then - ignore (Evd.check_univ_decl ~poly evd udecl) - in - let evd = - if poly then evd - else (* We fix the variables to ensure they won't be lowered to Set *) - Evd.fix_undefined_variables evd - in - start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl - (************************************************************************) (* Commom constant saving path, for both Qed and Admitted *) (************************************************************************) @@ -258,17 +211,9 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect let open DeclareDef in (match scope with | Discharge -> - let impl = Glob_term.Explicit in - let univs = match univs with - | Polymorphic_entry (_, univs) -> - (* What is going on here? *) - Univ.ContextSet.of_context univs - | Monomorphic_entry univs -> univs - in - let () = Declare.declare_universe_context ~poly univs in - let c = Declare.SectionLocalAssum {typ=t_i; impl} in - let () = Declare.declare_variable ~name ~kind c in - GlobRef.VarRef name, impargs + (* Let Fixpoint + Admitted gets turned into axiom so scope is Global, + see finish_admitted *) + assert false | Global local -> let kind = Decls.(IsAssumption Conjectural) in let decl = Declare.ParameterEntry (None,(t_i,univs),None) in @@ -335,7 +280,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe in let kn = Declare.declare_constant ~name ~local ~kind:Decls.(IsAssumption Conjectural) (Declare.ParameterEntry pe) in let () = Declare.assumption_message name in - Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); + DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx); (* This takes care of the implicits and hook for the current constant*) process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms @@ -350,16 +295,18 @@ let save_lemma_admitted ~(lemma : t) : unit = | _ -> CErrors.anomaly ~label:"Lemmas.save_proof" (Pp.str "more than one statement.") in let typ = EConstr.Unsafe.to_constr typ in - (* This will warn if the proof is complete *) - let pproofs, _univs = Proof_global.return_proof ~allow_partial:true lemma.proof in + let proof = Proof_global.get_proof lemma.proof in + let pproofs = Proof.partial_proof proof in let sec_vars = if not (get_keep_admitted_vars ()) then None else match Proof_global.get_used_variables lemma.proof, pproofs with | Some _ as x, _ -> x - | None, (pproof, _) :: _ -> + | None, pproof :: _ -> let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in - let ids_def = Environ.global_vars_set env pproof in + (* [pproof] is evar-normalized by [partial_proof]. We don't + count variables appearing only in the type of evars. *) + let ids_def = Environ.global_vars_set env (EConstr.Unsafe.to_constr pproof) in Some (Environ.really_needed env (Id.Set.union ids_typ ids_def)) | _ -> None in let universes = Proof_global.get_initial_euctx lemma.proof in @@ -384,17 +331,14 @@ let adjust_guardness_conditions const = function | possible_indexes -> (* Try all combinations... not optimal *) let env = Global.env() in - { const with - Declare.proof_entry_body = - Future.chain const.Declare.proof_entry_body - (fun ((body, ctx), eff) -> - match Constr.kind body with - | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> - let env = Safe_typing.push_private_constants env eff.Evd.seff_private in - let indexes = search_guard env possible_indexes fixdecls in - (mkFix ((indexes,0),fixdecls), ctx), eff - | _ -> (body, ctx), eff) - } + Declare.Internal.map_entry_body const + ~f:(fun ((body, ctx), eff) -> + match Constr.kind body with + | Fix ((nv,0),(_,_,fixdefs as fixdecls)) -> + let env = Safe_typing.push_private_constants env eff.Evd.seff_private in + let indexes = search_guard env possible_indexes fixdecls in + (mkFix ((indexes,0),fixdecls), ctx), eff + | _ -> (body, ctx), eff) let finish_proved env sigma idopt po info = let open Proof_global in @@ -404,7 +348,7 @@ let finish_proved env sigma idopt po info = let name = match idopt with | None -> name | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in - let fix_exn = Future.fix_exn_of const.Declare.proof_entry_body in + let fix_exn = Declare.Internal.get_fix_exn const in let () = try let const = adjust_guardness_conditions const compute_guard in let should_suggest = const.Declare.proof_entry_opaque && @@ -425,7 +369,7 @@ let finish_proved env sigma idopt po info = then Proof_using.suggest_constant (Global.env ()) kn in let gr = GlobRef.ConstRef kn in - Declare.declare_univ_binders gr (UState.universe_binders universes); + DeclareUniv.declare_univ_binders gr (UState.universe_binders universes); gr in Declare.definition_message name; @@ -452,7 +396,7 @@ let finish_derived ~f ~name ~idopt ~entries = in (* The opacity of [f_def] is adjusted to be [false], as it must. Then [f] is declared in the global environment. *) - let f_def = { f_def with Declare.proof_entry_opaque = false } in + let f_def = Declare.Internal.set_opacity ~opaque:false f_def in let f_kind = Decls.(IsDefinition Definition) in let f_def = Declare.DefinitionEntry f_def in let f_kn = Declare.declare_constant ~name:f ~kind:f_kind f_def in @@ -463,20 +407,15 @@ let finish_derived ~f ~name ~idopt ~entries = performs this precise action. *) let substf c = Vars.replace_vars [f,f_kn_term] c in (* Extracts the type of the proof of [suchthat]. *) - let lemma_pretype = - match lemma_def.Declare.proof_entry_type with - | Some t -> t + let lemma_pretype typ = + match typ with + | Some t -> Some (substf t) | None -> assert false (* Proof_global always sets type here. *) in (* The references of [f] are subsituted appropriately. *) - let lemma_type = substf lemma_pretype in + let lemma_def = Declare.Internal.map_entry_type lemma_def ~f:lemma_pretype in (* The same is done in the body of the proof. *) - let lemma_body = Future.chain lemma_def.Declare.proof_entry_body (fun ((b,ctx),fx) -> (substf b, ctx), fx) in - let lemma_def = - { lemma_def with - Declare.proof_entry_body = lemma_body; - proof_entry_type = Some lemma_type } - in + let lemma_def = Declare.Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in let lemma_def = Declare.DefinitionEntry lemma_def in let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in () @@ -491,7 +430,7 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 = | Some id -> id | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n) in - let entry, args = Abstract.shrink_entry local_context entry in + let entry, args = Declare.Internal.shrink_entry local_context entry in let cst = Declare.declare_constant ~name:id ~kind (Declare.DefinitionEntry entry) in let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index fbf91b3ad4..e790c39022 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -110,17 +110,6 @@ val start_lemma_with_initialization val default_thm_id : Names.Id.t -(** Main [Lemma foo args : type.] command *) -val start_lemma_com - : program_mode:bool - -> poly:bool - -> scope:DeclareDef.locality - -> kind:Decls.logical_kind - -> ?inference_hook:Pretyping.inference_hook - -> ?hook:DeclareDef.Hook.t - -> Vernacexpr.proof_expr list - -> t - (** {4 Saving proofs} *) val save_lemma_admitted : lemma:t -> unit diff --git a/vernac/library.ml b/vernac/library.ml index 8125c3de35..244424de6b 100644 --- a/vernac/library.ml +++ b/vernac/library.ml @@ -430,23 +430,33 @@ let error_recursively_dependent_library dir = (* Security weakness: file might have been changed on disk between writing the content and computing the checksum... *) -let save_library_to ?todo ~output_native_objects dir f otab = - let except = match todo with - | None -> - (* XXX *) - (* assert(!Flags.compilation_mode = Flags.BuildVo); *) - assert(Filename.check_suffix f ".vo"); - Future.UUIDSet.empty - | Some (l,_) -> - assert(Filename.check_suffix f ".vio"); - List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) - Future.UUIDSet.empty l in +type ('document,'counters) todo_proofs = + | ProofsTodoNone (* for .vo *) + | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + +let save_library_to todo_proofs ~output_native_objects dir f otab = + assert( + let expected_extension = match todo_proofs with + | ProofsTodoNone -> ".vo" + | ProofsTodoSomeEmpty _ -> ".vos" + | ProofsTodoSome _ -> ".vio" + in + Filename.check_suffix f expected_extension); + let except = match todo_proofs with + | ProofsTodoNone -> Future.UUIDSet.empty + | ProofsTodoSomeEmpty except -> except + | ProofsTodoSome (except,l,_) -> except + in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in let opaque_table, f2t_map = Opaqueproof.dump ~except otab in let tasks, utab = - match todo with - | None -> None, None - | Some (tasks, rcbackup) -> + match todo_proofs with + | ProofsTodoNone -> None, None + | ProofsTodoSomeEmpty _except -> + None, + Some (Univ.ContextSet.empty,false) + | ProofsTodoSome (_except, tasks, rcbackup) -> let tasks = List.map Stateid.(fun (r,b) -> try { r with uuid = Future.UUIDMap.find r.uuid f2t_map }, b diff --git a/vernac/library.mli b/vernac/library.mli index 6a32413248..ec485e6408 100644 --- a/vernac/library.mli +++ b/vernac/library.mli @@ -36,10 +36,18 @@ type seg_univ = (* all_cst, finished? *) Univ.ContextSet.t * bool type seg_proofs = Opaqueproof.opaque_proofterm array -(** End the compilation of a library and save it to a ".vo" file. +(** End the compilation of a library and save it to a ".vo" file, + a ".vio" file, or a ".vos" file, depending on the todo_proofs + argument. [output_native_objects]: when producing vo objects, also compile the native-code version. *) + +type ('document,'counters) todo_proofs = + | ProofsTodoNone (* for .vo *) + | ProofsTodoSomeEmpty of Future.UUIDSet.t (* for .vos *) + | ProofsTodoSome of Future.UUIDSet.t * ((Future.UUID.t,'document) Stateid.request * bool) list * 'counters (* for .vio *) + val save_library_to : - ?todo:(((Future.UUID.t,'document) Stateid.request * bool) list * 'counters) -> + ('document,'counters) todo_proofs -> output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml index bea0c943c3..b3dc254a63 100644 --- a/vernac/loadpath.ml +++ b/vernac/loadpath.ml @@ -138,6 +138,18 @@ let select_vo_file ~warn loadpath base = System.where_in_path ~warn loadpath name in Some (lpath, file) with Not_found -> None in + if !Flags.load_vos_libraries then begin + (* If the .vos file exists and is not empty, it describes the library. + If the .vos file exists and is empty, then load the .vo file. + If the .vos file is missing, then fail. *) + match find ".vos" with + | None -> Error LibNotFound + | Some (_, vos as resvos) -> + if (Unix.stat vos).Unix.st_size > 0 then Ok resvos else + match find ".vo" with + | None -> Error LibNotFound + | Some resvo -> Ok resvo + end else match find ".vo", find ".vio" with | None, None -> Error LibNotFound @@ -189,8 +201,10 @@ let error_unmapped_dir qid = ]) let error_lib_not_found qid = + let vos = !Flags.load_vos_libraries in + let vos_msg = if vos then [Pp.str " (while searching for a .vos file)"] else [] in CErrors.user_err ~hdr:"load_absolute_library_from" - Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]) + Pp.(seq ([ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]@vos_msg)) let try_locate_absolute_library dir = match locate_absolute_library dir with diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c8cede1f84..4ea34e2b60 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -423,11 +423,9 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic ~name ~poly ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let (body, eff) = Future.force entry.Declare.proof_entry_body in - let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in - let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - Some (fst body, entry.Declare.proof_entry_type, Evd.evar_universe_context ctx') + let body, ctx' = Declare.inline_private_constants ~univs:ctx' env entry in + Inductiveops.control_only_guard env (Evd.from_ctx ctx') (EConstr.of_constr body); + Some (body, entry.Declare.proof_entry_type, ctx') with | Refiner.FailError (_, s) as exn -> let _ = CErrors.push exn in 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/record.ml b/vernac/record.ml index 831fb53549..b60bfdfa22 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -466,7 +466,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa in let mie = InferCumulativity.infer_inductive (Global.env ()) mie in let impls = List.map (fun _ -> paramimpls, []) record_data in - let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls + let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls ~primitive_expected:!primitive_flag in let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) = diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index afc701edbc..5226c2ba65 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -13,11 +13,13 @@ Ppvernac Proof_using Egramcoq Metasyntax +DeclareUniv DeclareDef DeclareObl Canonical RecLemmas Library +Prettyp Lemmas Class Auto_ind_decl @@ -28,6 +30,7 @@ ComDefinition Classes ComPrimitive ComAssumption +DeclareInd ComInductive ComFixpoint ComProgramFixpoint @@ -36,6 +39,7 @@ Assumptions Mltop Topfmt Loadpath +ComArguments Vernacentries Vernacstate Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 430cee62c2..6dfba02ae9 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) @@ -407,8 +406,10 @@ let err_notfound_library ?from qid = | Some from -> str " with prefix " ++ DirPath.print from ++ str "." in + let bonus = + if !Flags.load_vos_libraries then " (While searching for a .vos file.)" else "" in user_err ?loc:qid.CAst.loc ~hdr:"locate_library" - (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) + (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix ++ str bonus) let print_located_library qid = let open Loadpath in @@ -448,9 +449,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()) @@ -465,29 +463,64 @@ let vernac_custom_entry ~module_local s = (***********) (* Gallina *) -let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = - let inference_hook = - if program_mode then - let hook env sigma ev = - let tac = !Obligations.default_tactic in - let evi = Evd.find sigma ev in - let evi = Evarutil.nf_evar_info sigma evi in - let env = Evd.evar_filtered_env evi in - try - let concl = evi.Evd.evar_concl in - if not (Evarutil.is_ground_env sigma env && - Evarutil.is_ground_term sigma concl) - then raise Exit; - let c, _, ctx = - Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac - in Evd.set_universe_context sigma ctx, EConstr.of_constr c - with Logic_monad.TacticFailure e when Logic.catchable_exception e -> - user_err Pp.(str "The statement obligations could not be resolved \ - automatically, write a statement definition first.") - in Some hook - else None +let check_name_freshness locality {CAst.loc;v=id} : unit = + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id || + locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id) + then + user_err ?loc (Id.print id ++ str " already exists.") + +let program_inference_hook env sigma ev = + let tac = !Obligations.default_tactic in + let evi = Evd.find sigma ev in + let evi = Evarutil.nf_evar_info sigma evi in + let env = Evd.evar_filtered_env evi in + try + let concl = evi.Evd.evar_concl in + if not (Evarutil.is_ground_env sigma env && + Evarutil.is_ground_term sigma concl) + then raise Exit; + let c, _, ctx = + Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac + in Evd.set_universe_context sigma ctx, EConstr.of_constr c + with Logic_monad.TacticFailure e when Logic.catchable_exception e -> + user_err Pp.(str "The statement obligations could not be resolved \ + automatically, write a statement definition first.") + +let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = + let env0 = Global.env () in + let decl = fst (List.hd thms) in + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in + let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) -> + let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in + let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in + let flags = Pretyping.{ all_and_fail_flags with program_mode } in + let inference_hook = if program_mode then Some program_inference_hook else None in + let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in + let ids = List.map Context.Rel.Declaration.get_name ctx in + check_name_freshness scope id; + (* XXX: The nf_evar is critical !! *) + evd, (id.CAst.v, + (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), + (ids, imps @ imps')))) + evd thms in + let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in + let evd = Evd.minimize_universes evd in + (* XXX: This nf_evar is critical too!! We are normalizing twice if + you look at the previous lines... *) + let thms = List.map (fun (name, (typ, (args, impargs))) -> + { Recthm.name; typ = Evarutil.nf_evar evd typ; args; impargs} ) thms in + let () = + let open UState in + if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then + ignore (Evd.check_univ_decl ~poly evd udecl) + in + let evd = + if poly then evd + else (* We fix the variables to ensure they won't be lowered to Set *) + Evd.fix_undefined_variables evd in - start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l + start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl let vernac_definition_hook ~poly = let open Decls in function | Coercion -> @@ -522,7 +555,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] + start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in @@ -545,7 +578,7 @@ let vernac_start_proof ~atts kind l = let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l + start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l let vernac_end_proof ~lemma = let open Vernacexpr in function | Admitted -> @@ -620,7 +653,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 @@ -799,7 +832,7 @@ let vernac_scheme l = Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid; match s with | InductionScheme (_, r, _) - | CaseScheme (_, r, _) + | CaseScheme (_, r, _) | EqualityScheme r -> dump_global r) l; Indschemes.do_scheme l @@ -814,14 +847,14 @@ let vernac_universe ~poly l = user_err ~hdr:"vernac_universe" (str"Polymorphic universes can only be declared inside sections, " ++ str "use Monomorphic Universe instead"); - Declare.do_universe ~poly l + DeclareUniv.do_universe ~poly l let vernac_constraint ~poly l = if poly && not (Global.sections_are_opened ()) then user_err ~hdr:"vernac_constraint" (str"Polymorphic universe constraints can only be declared" ++ str " inside sections, use Monomorphic Constraint instead"); - Declare.do_constraint ~poly l + DeclareUniv.do_constraint ~poly l (**********************) (* Modules *) @@ -1178,292 +1211,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; @@ -1927,29 +1674,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() @@ -2100,11 +1844,13 @@ let vernac_register qid r = if DirPath.equal (dirpath_of_string "kernel") ns then begin if Global.sections_are_opened () then user_err Pp.(str "Registering a kernel type is not allowed in sections"); - let pind = match Id.to_string id with - | "ind_bool" -> CPrimitives.PIT_bool - | "ind_carry" -> CPrimitives.PIT_carry - | "ind_pair" -> CPrimitives.PIT_pair - | "ind_cmp" -> CPrimitives.PIT_cmp + let CPrimitives.PIE pind = match Id.to_string id with + | "ind_bool" -> CPrimitives.(PIE PIT_bool) + | "ind_carry" -> CPrimitives.(PIE PIT_carry) + | "ind_pair" -> CPrimitives.(PIE PIT_pair) + | "ind_cmp" -> CPrimitives.(PIE PIT_cmp) + | "ind_f_cmp" -> CPrimitives.(PIE PIT_f_cmp) + | "ind_f_class" -> CPrimitives.(PIE PIT_f_class) | k -> CErrors.user_err Pp.(str "Register: unknown identifier “" ++ str k ++ str "” in the “kernel” namespace") in match gr with @@ -2418,7 +2164,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) |