diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 3 | ||||
| -rw-r--r-- | vernac/assumptions.mli | 2 | ||||
| -rw-r--r-- | vernac/attributes.ml | 9 | ||||
| -rw-r--r-- | vernac/attributes.mli | 10 | ||||
| -rw-r--r-- | vernac/classes.ml | 26 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 4 | ||||
| -rw-r--r-- | vernac/comFixpoint.ml | 15 | ||||
| -rw-r--r-- | vernac/comFixpoint.mli | 2 | ||||
| -rw-r--r-- | vernac/comInductive.ml | 8 | ||||
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 18 | ||||
| -rw-r--r-- | vernac/declareDef.ml | 6 | ||||
| -rw-r--r-- | vernac/egramml.mli | 4 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 9 | ||||
| -rw-r--r-- | vernac/himsg.ml | 23 | ||||
| -rw-r--r-- | vernac/lemmas.ml | 80 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 4 | ||||
| -rw-r--r-- | vernac/obligations.ml | 108 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/pvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 36 | ||||
| -rw-r--r-- | vernac/record.mli | 1 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 233 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 47 | ||||
| -rw-r--r-- | vernac/vernacexpr.ml | 79 | ||||
| -rw-r--r-- | vernac/vernacextend.ml | 250 | ||||
| -rw-r--r-- | vernac/vernacextend.mli | 118 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml | 77 | ||||
| -rw-r--r-- | vernac/vernacinterp.mli | 21 |
29 files changed, 648 insertions, 555 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 6beac2032d..3ca2a4ad6b 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -294,7 +294,6 @@ let traverse current t = let type_of_constant cb = cb.Declarations.const_type let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = - let (idts, knst) = st in (** Only keep the transitive dependencies *) let (_, graph, ax2ty) = traverse (label_of gr) t in let fold obj _ accu = match obj with @@ -316,7 +315,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let t = type_of_constant cb in let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (Constant kn,l)) t accu - else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then + else if add_opaque && (Declareops.is_opaque cb || not (TransparentState.is_transparent_constant st kn)) then let t = type_of_constant cb in ContextObjectMap.add (Opaque kn) t accu else if add_transparent then diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index aead345d8c..536185f4aa 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -28,5 +28,5 @@ val traverse : on which a term relies (together with their type). The above warning of {!traverse} also applies. *) val assumptions : - ?add_opaque:bool -> ?add_transparent:bool -> transparent_state -> + ?add_opaque:bool -> ?add_transparent:bool -> TransparentState.t -> GlobRef.t -> constr -> types ContextObjectMap.t diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 88638b295b..bc0b0310b3 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -9,7 +9,14 @@ (************************************************************************) open CErrors -open Vernacexpr + +(** The type of parsing attribute data *) +type vernac_flags = vernac_flag list +and vernac_flag = string * vernac_flag_value +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags let unsupported_attributes = function | [] -> () diff --git a/vernac/attributes.mli b/vernac/attributes.mli index c81082d5ad..c2dde4cbcc 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -8,7 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Vernacexpr +(** The type of parsing attribute data *) +type vernac_flags = vernac_flag list +and vernac_flag = string * vernac_flag_value +and vernac_flag_value = + | VernacFlagEmpty + | VernacFlagLeaf of string + | VernacFlagList of vernac_flags type +'a attribute (** The type of attributes. When parsing attributes if an ['a @@ -80,7 +86,7 @@ val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a (** * Defining attributes. *) -type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a +type 'a key_parser = 'a option -> vernac_flag_value -> 'a (** A parser for some key in an attribute. It is given a nonempty ['a option] when the attribute is multiply set for some command. diff --git a/vernac/classes.ml b/vernac/classes.ml index f4b0015851..95e46b252b 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -146,7 +146,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps ?hook (ConstRef cst); id -let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = +let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if program_mode then let hook _ _ vis gr = @@ -188,11 +188,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id ] in ignore (Pfedit.by init_refine) - else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + else ignore (Pfedit.by (Tactics.auto_intros_tac ids)); (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () -let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len = +let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -275,7 +274,7 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype else if program_mode || refine || Option.is_empty term then - declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype + declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining."); id @@ -341,7 +340,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id else do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode - cty k u ctx ctx' pri decl imps subst id props len + cty k u ctx ctx' pri decl imps subst id props let named_of_rel_context l = let open Vars in @@ -370,25 +369,24 @@ let context poly l = user_err Pp.(str "Anonymous variables not allowed in contexts.") in let univs = - let uctx = Evd.universe_context_set sigma in match ctx with | [] -> assert false - | [_] -> - if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) - else Monomorphic_const_entry uctx + | [_] -> Evd.const_univ_entry ~poly sigma | _::_::_ -> + (** TODO: explain this little belly dance *) if Lib.sections_are_opened () then begin + let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - if poly then Polymorphic_const_entry Univ.UContext.empty + if poly then Polymorphic_const_entry ([||], Univ.UContext.empty) else Monomorphic_const_entry Univ.ContextSet.empty end - else if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else if poly then + Evd.const_univ_entry ~poly sigma else begin + let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; Monomorphic_const_entry Univ.ContextSet.empty end diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e990f0cd15..8707121306 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -47,7 +47,7 @@ match local with | Discharge when Lib.sections_are_opened () -> let ctx = match ctx with | Monomorphic_const_entry ctx -> ctx - | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx + | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx in let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in @@ -79,7 +79,7 @@ match local with let () = if do_instance then Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with - | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx | Monomorphic_const_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 138696e3a7..a9c499b192 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -99,7 +99,7 @@ let check_mutuality env evd isfix fixl = let names = List.map fst fixl in let preorder = List.map (fun (id,def) -> - (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names)) + (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names)) fixl in let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with @@ -227,25 +227,28 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in let sigma = Evd.minimize_universes sigma in - (* XXX: We still have evars here in Program *) - let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in - let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in (* Build the fix declaration block *) (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env evd (Evd.from_env env); if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env evd isfix (List.combine fixnames fixdefs) end +let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) = + check_evars_are_solved env evd (Evd.from_env env); + let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in + let fixtypes = List.map EConstr.(to_constr evd) fixtypes in + Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes) + let interp_fixpoint ~cofix l ntns = let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in check_recursive true env evd fix; - (fix,pl,Evd.evar_universe_context evd,info) + let uctx,fix = ground_fixpoint env evd fix in + (fix,pl,uctx,info) let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b1a9c8a5a3..f4569ed3e2 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -51,7 +51,7 @@ val interp_recursive : (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) - (Id.t list * Constr.constr option list * Constr.types list) * + (Id.t list * EConstr.constr option list * EConstr.types list) * (* ctx per mutual def / implicits / struct annotations *) (EConstr.rel_context * Impargs.manual_explicitation list * int option) list diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 5ff3032ec4..f405c4d5a9 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -450,10 +450,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not in let univs = match uctx with - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (nas, uctx) -> if cum then - Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx) - else Polymorphic_ind_entry uctx + Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx) + else Polymorphic_ind_entry (nas, uctx) | Monomorphic_const_entry uctx -> Monomorphic_ind_entry uctx in @@ -535,11 +535,11 @@ let declare_mutual_inductive_with_eliminations mie pl impls = 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 + Declare.declare_univ_binders (IndRef (mind,0)) pl; List.iteri (fun i (indimpls, constrimpls) -> let ind = (mind,i) in let gr = IndRef ind in maybe_declare_manual_implicits false gr indimpls; - Declare.declare_univ_binders gr pl; List.iteri (fun j impls -> maybe_declare_manual_implicits false diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3d3d825bd0..ebedfb1e0d 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Pp open CErrors open Util @@ -204,7 +214,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in - let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in @@ -252,10 +261,10 @@ let do_program_recursive local poly fixkind fixl ntns = let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) and typ = (* Worrying... *) - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = @@ -269,6 +278,9 @@ let do_program_recursive local poly fixkind fixl ntns = let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in let () = if not cofix then begin let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in + (* XXX: are we allowed to have evars here? *) + let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in + let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), Array.of_list fixtypes, Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 35fb18e292..2fe03a8ec5 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -43,9 +43,11 @@ let declare_definition ident (local, p, k) ce pl imps hook = | Discharge | Local | Global -> let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in - ConstRef kn in + let gr = ConstRef kn in + let () = Declare.declare_univ_binders gr pl in + gr + in let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in let () = definition_message ident in Lemmas.call_hook fix_exn hook local gr; gr diff --git a/vernac/egramml.mli b/vernac/egramml.mli index a90ef97e7d..3689f60383 100644 --- a/vernac/egramml.mli +++ b/vernac/egramml.mli @@ -21,10 +21,10 @@ type 's grammar_prod_item = ('s, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> vernac_expr Pcoq.Entry.t option -> + extend_name -> vernac_expr Pcoq.Entry.t option -> vernac_expr grammar_prod_item list -> unit -val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list +val get_extend_vernac_rule : extend_name -> vernac_expr grammar_prod_item list val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1d0a5ab0a3..3cdf81ced0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -30,6 +30,7 @@ open Pcoq.Prim open Pcoq.Constr open Pcoq.Module open Pvernac.Vernac_ +open Attributes let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ] let _ = List.iter CLexer.add_keyword vernac_kw @@ -989,8 +990,9 @@ GRAMMAR EXTEND Gram | IDENT "Scope"; s = IDENT -> { PrintScope s } | IDENT "Visibility"; s = OPT IDENT -> { PrintVisibility s } | IDENT "Implicit"; qid = smart_global -> { PrintImplicit qid } - | IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (false, fopt) } - | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> { PrintUniverses (true, fopt) } + | b = [ IDENT "Sorted" -> { true } | -> { false } ]; IDENT "Universes"; + g = OPT printunivs_subgraph; fopt = OPT ne_string -> + { PrintUniverses (b, g, fopt) } | IDENT "Assumptions"; qid = smart_global -> { PrintAssumptions (false, false, qid) } | IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (true, false, qid) } | IDENT "Transparent"; IDENT "Dependencies"; qid = smart_global -> { PrintAssumptions (false, true, qid) } @@ -1000,6 +1002,9 @@ GRAMMAR EXTEND Gram | IDENT "Registered" -> { PrintRegistered } ] ] ; + printunivs_subgraph: + [ [ IDENT "Subgraph"; "("; l = LIST0 reference; ")" -> { l } ] ] + ; class_rawexpr: [ [ IDENT "Funclass" -> { FunClass } | IDENT "Sortclass" -> { SortClass } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index ba31f73030..6c7117b513 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -884,8 +884,6 @@ let explain_not_match_error = function let status b = if b then str"polymorphic" else str"monomorphic" in str "a " ++ status b ++ str" declaration was expected, but a " ++ status (not b) ++ str" declaration was found" - | IncompatibleInstances -> - str"polymorphic universe instances do not match" | IncompatibleUniverses incon -> str"the universe constraints are inconsistent: " ++ Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon @@ -894,11 +892,22 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++ str "compared to " ++ spc () ++ quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) - | IncompatibleConstraints cst -> - str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in - (** FIXME: provide a proper naming for the bound variables *) - quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) + | IncompatibleConstraints { got; expect } -> + let open Univ in + let pr_auctx auctx = + let sigma = Evd.from_ctx + (UState.of_binders + (UnivNames.universe_binders_with_opt_names auctx None)) + in + let uctx = AUContext.repr auctx in + Printer.pr_universe_instance_constraints sigma + (UContext.instance uctx) + (UContext.constraints uctx) + in + str "incompatible polymorphic binders: got" ++ spc () ++ h 0 (pr_auctx got) ++ spc() ++ + str "but expected" ++ spc() ++ h 0 (pr_auctx expect) ++ + (if not (Int.equal (AUContext.size got) (AUContext.size expect)) then mt() else + fnl() ++ str "(incompatible constraints)") let explain_signature_mismatch l spec why = str "Signature components for label " ++ Label.print l ++ diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 8aa459729c..de020926f6 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -197,10 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in - ConstRef kn + let gr = ConstRef kn in + Declare.declare_univ_binders gr (UState.universe_binders uctx); + gr in definition_message id; - Declare.declare_univ_binders r (UState.universe_binders uctx); call_hook (fun exn -> exn) hook locality r with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -228,7 +229,7 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_, | Discharge -> let impl = false in (* copy values from Vernacentries *) let univs = match univs with - | Polymorphic_const_entry univs -> + | Polymorphic_const_entry (_, univs) -> (* What is going on here? *) Univ.ContextSet.of_context univs | Monomorphic_const_entry univs -> univs @@ -305,17 +306,18 @@ let universe_proof_terminator compute_guard hook = | Admitted (id,k,pe,ctx) -> admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) (); Feedback.feedback Feedback.AddedAxiom - | Proved (opaque,idopt,proof) -> - let is_opaque, export_seff = match opaque with - | Transparent -> false, true - | Opaque -> true, false - in - let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in - let const = {const with const_entry_opaque = is_opaque} in - let id = match idopt with - | None -> id - | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in - save ~export_seff id const univs compute_guard persistence (hook (Some univs)) + | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) -> + let is_opaque, export_seff = match opaque with + | Transparent -> false, true + | Opaque -> true, false + in + let const = {const with const_entry_opaque = is_opaque} in + let id = match idopt with + | None -> id + | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in + save ~export_seff id const universes compute_guard persistence (hook (Some universes)) + | Proved (opaque,idopt, _ ) -> + CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term") end let standard_proof_terminator compute_guard hook = @@ -329,7 +331,7 @@ let initialize_named_context_for_proof () = let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in Environ.push_named_context_val d signv) sign Environ.empty_named_context_val -let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let terminator = match terminator with | None -> standard_proof_terminator compute_guard hook | Some terminator -> terminator compute_guard hook @@ -339,19 +341,21 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard= | Some sign -> sign | None -> initialize_named_context_for_proof () in - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator + let goals = [ Global.env_of_context sign , c ] in + Proof_global.start_proof sigma id ?pl kind goals terminator -let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook = +let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?(compute_guard=[]) hook = let terminator = match terminator with | None -> universe_proof_terminator compute_guard hook | Some terminator -> terminator compute_guard hook in - let sign = + let sign = match sign with | Some sign -> sign | None -> initialize_named_context_for_proof () in - Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator + let goals = [ Global.env_of_context sign , c ] in + Proof_global.start_proof sigma id ?pl kind goals terminator let rec_tac_initializer finite guard thms snl = if finite then @@ -368,28 +372,20 @@ let rec_tac_initializer finite guard thms snl = | _ -> assert false let start_proof_with_initialization kind sigma decl recguard thms snl hook = - let intro_tac (_, (_, (ids, _))) = - Tacticals.New.tclMAP (function - | Name id -> Tactics.intro_mustbe_force id - | Anonymous -> Tactics.intro) (List.rev ids) in + let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> - let rec_tac = rec_tac_initializer finite guard thms snl in - Some (match init_tac with - | None -> - if Flags.is_auto_intros () then - Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) - else - rec_tac + let rec_tac = rec_tac_initializer finite guard thms snl in + Some (match init_tac with + | None -> + Tacticals.New.tclTHENS rec_tac (List.map intro_tac thms) | Some tacl -> - Tacticals.New.tclTHENS rec_tac - (if Flags.is_auto_intros () then - List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms - else - tacl)),guard + Tacticals.New.tclTHENS rec_tac + List.(map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms) + ),guard | None -> - let () = match thms with [_] -> () | _ -> assert false in - (if Flags.is_auto_intros () then Some (intro_tac (List.hd thms)) else None), [] in + let () = match thms with [_] -> () | _ -> assert false in + Some (intro_tac (List.hd thms)), [] in match thms with | [] -> anomaly (Pp.str "No proof to start.") | (id,(t,(_,imps)))::other_thms -> @@ -410,7 +406,11 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook = List.iter (fun (strength,ref,imps) -> maybe_declare_manual_implicits false ref imps; call_hook (fun exn -> exn) hook strength ref) thms_data in - start_proof_univs id ~pl:decl kind sigma t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard + start_proof_univs id ~pl:decl kind sigma t (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard; + ignore (Proof_global.with_current_proof (fun _ p -> + match init_tac with + | None -> p,(true,[]) + | Some tac -> Proof.run_tactic Global.(env ()) tac p)) let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in @@ -420,8 +420,8 @@ let start_proof_com ?inference_hook kind thms hook = let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in let flags = all_and_fail_flags in - let flags = { flags with use_hook = inference_hook } in - let evd = solve_remaining_evars flags env evd Evd.empty in + let hook = inference_hook in + let evd = solve_remaining_evars ?hook flags env evd Evd.empty in let ids = List.map RelDecl.get_name ctx in check_name_freshness (pi1 kind) id; (* XXX: The nf_evar is critical !! *) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index 195fcbf4ca..246d8cbe6d 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -18,13 +18,13 @@ val call_hook : Future.fix_exn -> declaration_hook -> Decl_kinds.locality -> Glo val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + ?compute_guard:Proof_global.lemma_possible_guards -> declaration_hook -> unit val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> + ?compute_guard:Proof_global.lemma_possible_guards -> (UState.t option -> declaration_hook) -> unit val start_proof_com : diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 97ed43c5f4..8baf391c70 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -667,7 +667,7 @@ let declare_obligation prg obl body ty uctx = if not opaque then add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; let body = match uctx with - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (_, uctx) -> Some (DefinedObl (constant, Univ.UContext.instance uctx)) | Monomorphic_const_entry _ -> Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) @@ -826,26 +826,41 @@ let rec string_of_list sep f = function | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl (* Solve an obligation using tactics, return the corresponding proof term *) +let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err -> + Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl (); + str "This will become an error in the future"]) -let solve_by_tac name evi t poly ctx = +let solve_by_tac ?loc name evi t poly ctx = let id = name in (* spiwack: the status is dropped. *) - let (entry,_,ctx') = Pfedit.build_constant_by_tactic - id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in - let env = Global.env () in - let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, () = Future.force entry.const_entry_body 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)); - (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' + try + let (entry,_,ctx') = + Pfedit.build_constant_by_tactic + id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in + let env = Global.env () in + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, () = Future.force entry.const_entry_body 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.const_entry_type, Evd.evar_universe_context ctx') + with + | Refiner.FailError (_, s) as exn -> + let _ = CErrors.push exn in + user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) + (* If the proof is open we absorb the error and leave the obligation open *) + | Proof.OpenProof _ -> + None + | e when CErrors.noncritical e -> + let err = CErrors.print e in + warn_solve_errored ?loc err; + None let obligation_terminator name num guard hook auto pf = let open Proof_global in let term = Lemmas.universe_proof_terminator guard hook in match pf with | Admitted _ -> apply_terminator term pf - | Proved (opq, id, proof) -> - let (_, (entry, uctx, _)) = Pfedit.cook_this_proof proof in + | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in @@ -904,6 +919,9 @@ let obligation_terminator name num guard hook auto pf = with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) + end + | Proved (_, _, _ ) -> + CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term") let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in @@ -987,44 +1005,34 @@ and solve_obligation_by_tac prg obls i tac = match obl.obl_body with | Some _ -> None | None -> - try - if List.is_empty (deps_remaining obls obl.obl_deps) then - let obl = subst_deps_obl obls obl in - let tac = - match tac with - | Some t -> t - | None -> - match obl.obl_tac with - | Some t -> t - | None -> !default_tactic - in - let evd = Evd.from_ctx prg.prg_ctx in - let evd = Evd.update_sigma_env evd (Global.env ()) in - let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = if pi2 prg.prg_kind - then Polymorphic_const_entry (UState.context ctx) - else Monomorphic_const_entry (UState.context_set ctx) - in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; - if def && not (pi2 prg.prg_kind) then ( - (* Declare the term constraints with the first obligation only *) - let evd = Evd.from_env (Global.env ()) in - let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in - let ctx' = Evd.evar_universe_context evd in - Some {prg with prg_ctx = ctx'}) - else Some prg - else None - with e when CErrors.noncritical e -> - let (e, _) = CErrors.push e in - match e with - | Refiner.FailError (_, s) -> - user_err ?loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s) - | e -> None (* FIXME really ? *) + if List.is_empty (deps_remaining obls obl.obl_deps) then + let obl = subst_deps_obl obls obl in + let tac = + match tac with + | Some t -> t + | None -> + match obl.obl_tac with + | Some t -> t + | None -> !default_tactic + in + let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in + match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with + | None -> None + | Some (t, ty, ctx) -> + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in + Some {prg with prg_ctx = ctx'}) + else Some prg + else None and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 1c1faca599..2ddd210365 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -492,12 +492,13 @@ open Pputils keyword "Print Hint *" | PrintHintDbName s -> keyword "Print HintDb" ++ spc () ++ str s - | PrintUniverses (b, fopt) -> + | PrintUniverses (b, g, fopt) -> let cmd = if b then "Print Sorted Universes" else "Print Universes" in - keyword cmd ++ pr_opt str fopt + let pr_subgraph = prlist_with_sep spc pr_qualid in + keyword cmd ++ pr_opt pr_subgraph g ++ pr_opt str fopt | PrintName (qid,udecl) -> keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl | PrintModuleType qid -> @@ -1213,6 +1214,7 @@ open Pputils let rec pr_vernac_flag (k, v) = let k = keyword k in + let open Attributes in match v with | VernacFlagEmpty -> k | VernacFlagLeaf v -> k ++ str " = " ++ qs v diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index b2fa8ec99f..4761e4bbc2 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -42,7 +42,7 @@ module Vernac_ = let command_entry_ref = ref noedit_mode let command_entry = Gram.Entry.of_parser "command_entry" - (fun strm -> Gram.Entry.parse_token !command_entry_ref strm) + (fun strm -> Gram.Entry.parse_token_stream !command_entry_ref strm) end diff --git a/vernac/record.ml b/vernac/record.ml index 7a4c38e972..ac84003266 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -277,12 +277,12 @@ let warn_non_primitive_record = strbrk" could not be defined as a primitive record"))) (* We build projections *) -let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in let u = match ctx with - | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx | Monomorphic_const_entry ctx -> Univ.Instance.empty in let paramdecls = Inductive.inductive_paramdecls (mib, u) in @@ -324,7 +324,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u (** Already defined by declare_mind silently *) let kn = Projection.Repr.constant p in Declare.definition_message fid; - UnivNames.register_universe_binders (ConstRef kn) ubinders; kn, mkProj (Projection.make p false,mkRel 1) else let ccl = subst_projection fid subst ti in @@ -360,7 +359,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u applist (mkConstU (kn,u),proj_args) in Declare.definition_message fid; - UnivNames.register_universe_binders (ConstRef kn) ubinders; kn, constr_fip with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) @@ -389,10 +387,10 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St match univs with | Monomorphic_ind_entry ctx -> false, Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry ctx -> - true, Polymorphic_const_entry ctx - | Cumulative_ind_entry cumi -> - true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) + | Polymorphic_ind_entry (nas, ctx) -> + true, Polymorphic_const_entry (nas, ctx) + | Cumulative_ind_entry (nas, cumi) -> + true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi) in let binder_name = match name with @@ -443,7 +441,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St let map i (_, _, _, fieldimpls, fields, is_coe, coers) = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in @@ -480,7 +478,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari (DefinitionEntry class_entry, IsDefinition Definition) in let inst, univs = match univs with - | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs + | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty in let cstu = (cst, inst) in @@ -496,9 +494,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref [paramimpls]; - UnivNames.register_universe_binders cref ubinders; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - UnivNames.register_universe_binders (ConstRef proj_cst) ubinders; Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = match List.hd coers with | Some b -> Some ((if b then Backward else Forward), List.hd priorities) @@ -508,11 +504,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | _ -> let univs = match univs with - | Polymorphic_const_entry univs -> + | Polymorphic_const_entry (nas, univs) -> if cum then - Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) + Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) else - Polymorphic_ind_entry univs + Polymorphic_ind_entry (nas, univs) | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in @@ -541,8 +537,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari in let univs, ctx_context, fields = match univs with - | Polymorphic_const_entry univs -> - let usubst, auctx = Univ.abstract_universes univs in + | Polymorphic_const_entry (nas, univs) -> + let usubst, auctx = Univ.abstract_universes nas univs in let usubst = Univ.make_instance_subst usubst in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in @@ -682,11 +678,11 @@ let definition_structure udecl kind ~template cum poly finite records = let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let univs = match univs with - | Polymorphic_const_entry univs -> + | Polymorphic_const_entry (nas, univs) -> if cum then - Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) + Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) else - Polymorphic_ind_entry univs + Polymorphic_ind_entry (nas, univs) | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in diff --git a/vernac/record.mli b/vernac/record.mli index 953d5ec3b6..04984030f7 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -20,7 +20,6 @@ val declare_projections : ?kind:Decl_kinds.definition_object_kind -> Id.t -> bool list -> - UnivNames.universe_binders -> Impargs.manual_implicits list -> Constr.rel_context -> (Name.t * bool) list * Constant.t option list diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 30fae756e9..ce93a8baaf 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -8,7 +8,7 @@ Himsg ExplainErr Locality Egramml -Vernacinterp +Vernacextend Ppvernac Proof_using Lemmas diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 74423d482e..a78329ad1d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -30,7 +30,6 @@ open Constrexpr open Redexpr open Lemmas open Locality -open Vernacinterp open Attributes module NamedDecl = Context.Named.Declaration @@ -320,7 +319,7 @@ let print_registered () = hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ()) -let dump_universes_gen g s = +let dump_universes_gen prl g s = let output = open_out s in let output_constraint, close = if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin @@ -345,10 +344,12 @@ let dump_universes_gen g s = | Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=" - in Printf.fprintf output "%s %s %s ;\n" left kind right + in + Printf.fprintf output "%s %s %s ;\n" left kind right end, (fun () -> close_out output) end in + let output_constraint k l r = output_constraint k (prl l) (prl r) in try UGraph.dump_universes output_constraint g; close (); @@ -358,6 +359,36 @@ let dump_universes_gen g s = close (); iraise reraise +let universe_subgraph ?loc g univ = + let open Univ in + let sigma = Evd.from_env (Global.env()) in + let univs_of q = + let q = Glob_term.(GType (UNamed q)) in + (* this function has a nice error message for not found univs *) + LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q) + in + let univs = List.fold_left (fun univs q -> LSet.union univs (univs_of q)) LSet.empty g in + let csts = UGraph.constraints_for ~kept:(LSet.add Level.prop (LSet.add Level.set univs)) univ in + let univ = LSet.fold UGraph.add_universe_unconstrained univs UGraph.initial_universes in + UGraph.merge_constraints csts univ + +let print_universes ?loc ~sort ~subgraph dst = + let univ = Global.universes () in + let univ = match subgraph with + | None -> univ + | Some g -> universe_subgraph ?loc g univ + in + let univ = if sort then UGraph.sort_universes univ else univ in + let pr_remaining = + if Global.is_joined_environment () then mt () + else str"There may remain asynchronous universe constraints" + in + let prl = UnivNames.pr_with_global_universes in + begin match dst with + | None -> UGraph.pr_universes prl univ ++ pr_remaining + | Some s -> dump_universes_gen (fun u -> Pp.string_of_ppcmds (prl u)) univ s + end + (*********************) (* "Locate" commands *) @@ -458,8 +489,7 @@ let start_proof_and_print k l hook = Evarutil.is_ground_term sigma concl) then raise Exit; let c, _, ctx = - Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) - concl (Tacticals.New.tclCOMPLETE tac) + Pfedit.build_by_tactic 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 \ @@ -1065,15 +1095,30 @@ let vernac_restore_state file = (* Commands *) let vernac_create_hintdb ~module_local id b = - Hints.create_hint_db module_local id full_transparent_state b - -let vernac_remove_hints ~module_local dbs ids = - Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids) + Hints.create_hint_db module_local id TransparentState.full b + +let warn_implicit_core_hint_db = + CWarnings.create ~name:"implicit-core-hint-db" ~category:"deprecated" + (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. " + ++ strbrk"Please specify a hint database.") + +let vernac_remove_hints ~module_local dbnames ids = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in + Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids) -let vernac_hints ~atts lb h = +let vernac_hints ~atts dbnames h = + let dbnames = + if List.is_empty dbnames then + (warn_implicit_core_hint_db (); ["core"]) + else dbnames + in let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_module_locality local in - Hints.add_hints ~local lb (Hints.interp_hints poly h) + Hints.add_hints ~local dbnames (Hints.interp_hints poly h) let vernac_syntactic_definition ~module_local lid x y = Dumpglob.dump_definition lid false "syndef"; @@ -1422,14 +1467,6 @@ let _ = let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic introduction of variables"; - optkey = ["Automatic";"Introduction"]; - optread = Flags.is_auto_intros; - optwrite = Flags.make_auto_intros } - -let _ = - declare_bool_option { optdepr = false; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; @@ -1827,17 +1864,7 @@ let vernac_print ~atts env sigma = | PrintCoercionPaths (cls,clt) -> Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt) | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma - | PrintUniverses (b, dst) -> - let univ = Global.universes () in - let univ = if b then UGraph.sort_universes univ else univ in - let pr_remaining = - if Global.is_joined_environment () then mt () - else str"There may remain asynchronous universe constraints" - in - begin match dst with - | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining - | Some s -> dump_universes_gen univ s - end + | PrintUniverses (sort, subgraph, dst) -> print_universes ~sort ~subgraph dst | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) | PrintHintGoal -> Hints.pr_applicable_hint () | PrintHintDbName s -> Hints.pr_hint_db_by_name env sigma s @@ -2268,7 +2295,7 @@ let interp ?proof ~atts ~st c = (* Extensions *) | VernacExtend (opn,args) -> (* XXX: Here we are returning the state! :) *) - let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in + let _st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in () (** A global default timeout, controlled by option "Set Default Timeout n". @@ -2400,147 +2427,3 @@ let interp ?verbosely ?proof ~st cmd = let exn = CErrors.push exn in Vernacstate.invalidate_cache (); iraise exn - -(** VERNAC EXTEND registering *) - -open Genarg -open Extend - -type classifier = Genarg.raw_generic_argument list -> vernac_classification - -type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig -| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig -| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig - -type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml - -let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") - -let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function -| TyNil -> fun f args -> - begin match args with - | [] -> f - | _ :: _ -> type_error () - end -| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args -| TyNonTerminal (tu, ty) -> fun f args -> - begin match args with - | [] -> type_error () - | Genarg.GenArg (Rawwit tag, v) :: args -> - match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with - | None -> type_error () - | Some Refl -> untype_classifier ty (f v) args - end - -(** Stupid GADTs forces us to duplicate the definition just for typing *) -let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function -| TyNil -> fun f args -> - begin match args with - | [] -> f - | _ :: _ -> type_error () - end -| TyTerminal (_, ty) -> fun f args -> untype_command ty f args -| TyNonTerminal (tu, ty) -> fun f args -> - begin match args with - | [] -> type_error () - | Genarg.GenArg (Rawwit tag, v) :: args -> - match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with - | None -> type_error () - | Some Refl -> untype_command ty (f v) args - end - -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function -| TUlist1 l -> Alist1 (untype_user_symbol l) -| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUlist0 l -> Alist0 (untype_user_symbol l) -| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUopt o -> Aopt (untype_user_symbol o) -| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a)) -| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i) - -let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function -| TyNil -> [] -| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty -| TyNonTerminal (tu, ty) -> - let t = rawwit (Egramml.proj_symbol tu) in - let symb = untype_user_symbol tu in - Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty - -let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol - -let classifiers : classifier array String.Map.t ref = ref String.Map.empty - -let get_vernac_classifier (name, i) args = - (String.Map.find name !classifiers).(i) args - -let declare_vernac_classifier name f = - classifiers := String.Map.add name f !classifiers - -let vernac_extend ~command ?classifier ?entry ext = - let get_classifier (TyML (_, ty, _, cl)) = match cl with - | Some cl -> untype_classifier ty cl - | None -> - match classifier with - | Some cl -> fun _ -> cl command - | None -> - let e = match entry with - | None -> "COMMAND" - | Some e -> Pcoq.Gram.Entry.name e - in - let msg = Printf.sprintf "\ - Vernac entry \"%s\" misses a classifier. \ - A classifier is a function that returns an expression \ - of type vernac_classification (see Vernacexpr). You can: \n\ - - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \ - new vernacular command does not alter the system state;\n\ - - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \ - new vernacular command alters the system state but not the \ - parser nor it starts a proof or ends one;\n\ - - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \ - a global function f. The function f will be called passing\ - \"%s\" as the only argument;\n\ - - Add a specific classifier in each clause using the syntax:\n\ - '[...] => [ f ] -> [...]'.\n\ - Specific classifiers have precedence over global \ - classifiers. Only one classifier is called." - command e e e command - in - CErrors.user_err (Pp.strbrk msg) - in - let cl = Array.map_of_list get_classifier ext in - let iter i (TyML (depr, ty, f, _)) = - let f = untype_command ty f in - let r = untype_grammar ty in - let () = vinterp_add depr (command, i) f in - Egramml.extend_vernac_command_grammar (command, i) entry r - in - let () = declare_vernac_classifier command cl in - List.iteri iter ext - -(** VERNAC ARGUMENT EXTEND registering *) - -type 'a argument_rule = -| Arg_alias of 'a Pcoq.Entry.t -| Arg_rules of 'a Extend.production_rule list - -type 'a vernac_argument = { - arg_printer : 'a -> Pp.t; - arg_parsing : 'a argument_rule; -} - -let vernac_argument_extend ~name arg = - let wit = Genarg.create_arg name in - let entry = match arg.arg_parsing with - | Arg_alias e -> - let () = Pcoq.register_grammar wit e in - e - | Arg_rules rules -> - let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in - e - in - let pr = arg.arg_printer in - let pr x = Genprint.PrinterBasic (fun () -> pr x) in - let () = Genprint.register_vernac_print0 wit pr in - (wit, entry) diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 8ccd121b8f..8d8d7cfcf0 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -36,50 +36,3 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t - -(** {5 VERNAC EXTEND} *) - -type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification - -type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig -| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig -| TyNonTerminal : - ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> - ('a -> 'r, 'a -> 's) ty_sig - -type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml - -(** Wrapper to dynamically extend vernacular commands. *) -val vernac_extend : - command:string -> - ?classifier:(string -> Vernacexpr.vernac_classification) -> - ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> - ty_ml list -> unit - -(** {5 VERNAC ARGUMENT EXTEND} *) - -type 'a argument_rule = -| Arg_alias of 'a Pcoq.Entry.t - (** This is used because CAMLP5 parser can be dumb about rule factorization, - which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Extend.production_rule list - (** There is a discrepancy here as we use directly extension rules and thus - entries instead of ty_user_symbol and thus arguments as roots. *) - -type 'a vernac_argument = { - arg_printer : 'a -> Pp.t; - arg_parsing : 'a argument_rule; -} - -val vernac_argument_extend : name:string -> 'a vernac_argument -> - ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t - -(** {5 STM classifiers} *) - -val get_vernac_classifier : - Vernacexpr.extend_name -> classifier - -(** Low-level API, not for casual user. *) -val declare_vernac_classifier : - string -> classifier array -> unit diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 594e9eca48..122005e011 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -45,7 +45,7 @@ type printable = | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions - | PrintUniverses of bool * string option + | PrintUniverses of bool * qualid list option * string option | PrintHint of qualid or_by_notation | PrintHintGoal | PrintHintDbName of string @@ -219,13 +219,6 @@ type section_subset_expr = {b ("ExtractionBlacklist", 0)} indicates {b Extraction Blacklist {i ident{_1}} ... {i ident{_n}}} command. *) -type extend_name = - (** Name of the vernac entry where the tactic is defined, typically found - after the VERNAC EXTEND statement in the source. *) - string * - (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch - is given an offset, starting from zero. *) - int (* This type allows registering the inlining of constants in native compiler. It will be extended with primitive inductive types and operators *) @@ -253,6 +246,14 @@ type vernac_argument_status = { implicit_status : vernac_implicit_status; } +type extend_name = + (** Name of the vernac entry where the tactic is defined, typically found + after the VERNAC EXTEND statement in the source. *) + string * + (** Index of the extension in the VERNAC EXTEND statement. Each parsing branch + is given an offset, starting from zero. *) + int + type nonrec vernac_expr = | VernacLoad of verbose_flag * string @@ -395,71 +396,11 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_flags = vernac_flag list -and vernac_flag = string * vernac_flag_value -and vernac_flag_value = - | VernacFlagEmpty - | VernacFlagLeaf of string - | VernacFlagList of vernac_flags - type vernac_control = - | VernacExpr of vernac_flags * vernac_expr + | VernacExpr of Attributes.vernac_flags * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) | VernacTime of bool * vernac_control CAst.t | VernacRedirect of string * vernac_control CAst.t | VernacTimeout of int * vernac_control | VernacFail of vernac_control - -(* A vernac classifier provides information about the exectuion of a - command: - - - vernac_when: encodes if the vernac may alter the parser [thus - forcing immediate execution], or if indeed it is pure and parsing - can continue without its execution. - - - vernac_type: if it is starts, ends, continues a proof or - alters the global state or is a control command like BackTo or is - a query like Check. - - The classification works on the assumption that we have 3 states: - parsing, execution (global enviroment, etc...), and proof - state. For example, commands that only alter the proof state are - considered safe to delegate to a worker. - -*) -type vernac_type = - (* Start of a proof *) - | VtStartProof of vernac_start - (* Command altering the global state, bad for parallel - processing. *) - | VtSideff of vernac_sideff_type - (* End of a proof *) - | VtQed of vernac_qed_type - (* A proof step *) - | VtProofStep of proof_step - (* To be removed *) - | VtProofMode of string - (* Queries are commands assumed to be "pure", that is to say, they - don't modify the interpretation state. *) - | VtQuery - (* To be removed *) - | VtMeta - | VtUnknown -and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) -and vernac_start = string * opacity_guarantee * Id.t list -and vernac_sideff_type = Id.t list -and opacity_guarantee = - | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) - | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) -and proof_step = { (* TODO: inline with OCaml 4.03 *) - parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; - proof_block_detection : proof_block_name option -} -and solving_tac = bool (* a terminator *) -and anon_abstracting_tac = bool (* abstracting anonymously its result *) -and proof_block_name = string (* open type of delimiters *) -type vernac_when = - | VtNow - | VtLater -type vernac_classification = vernac_type * vernac_when diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml new file mode 100644 index 0000000000..3a321ecdb4 --- /dev/null +++ b/vernac/vernacextend.ml @@ -0,0 +1,250 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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 Util +open Pp +open CErrors + +type vernac_type = + (* Start of a proof *) + | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) + | VtSideff of vernac_sideff_type + (* End of a proof *) + | VtQed of vernac_qed_type + (* A proof step *) + | VtProofStep of { + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option + } + (* To be removed *) + | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) + | VtQuery + (* To be removed *) + | VtMeta + | VtUnknown +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) +and vernac_start = string * opacity_guarantee * Names.Id.t list +and vernac_sideff_type = Names.Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and solving_tac = bool (** a terminator *) +and anon_abstracting_tac = bool (** abstracting anonymously its result *) +and proof_block_name = string (** open type of delimiters *) + +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when + +type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list + +(* Table of vernac entries *) +let vernac_tab = + (Hashtbl.create 211 : + (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) + +let vinterp_add depr s f = + try + Hashtbl.add vernac_tab s (depr, f) + with Failure _ -> + user_err ~hdr:"vinterp_add" + (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") + +let vinterp_map s = + try + Hashtbl.find vernac_tab s + with Failure _ | Not_found -> + user_err ~hdr:"Vernac Interpreter" + (str"Cannot find vernac command " ++ str (fst s) ++ str".") + +let warn_deprecated_command = + let open CWarnings in + create ~name:"deprecated-command" ~category:"deprecated" + (fun pr -> str "Deprecated vernacular command: " ++ pr) + +(* Interpretation of a vernac command *) + +let call opn converted_args ~atts ~st = + let phase = ref "Looking up command" in + try + let depr, callback = vinterp_map opn in + let () = if depr then + let rules = Egramml.get_extend_vernac_rule opn in + let pr_gram = function + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" + in + let pr = pr_sequence pr_gram rules in + warn_deprecated_command pr; + in + phase := "Checking arguments"; + let hunk = callback converted_args in + phase := "Executing command"; + hunk ~atts ~st + with + | reraise -> + let reraise = CErrors.push reraise in + if !Flags.debug then + Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); + iraise reraise + +(** VERNAC EXTEND registering *) + +type classifier = Genarg.raw_generic_argument list -> vernac_classification + +(** Classifiers *) +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let classify_as_query = VtQuery, VtLater +let classify_as_sideeff = VtSideff [], VtLater +let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater + +type (_, _) ty_sig = +| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") + +let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args +| TyNonTerminal (tu, ty) -> fun f args -> + let open Genarg in + begin match args with + | [] -> type_error () + | GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_classifier ty (f v) args + end + +(** Stupid GADTs forces us to duplicate the definition just for typing *) +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_command ty f args +| TyNonTerminal (tu, ty) -> fun f args -> + let open Genarg in + begin match args with + | [] -> type_error () + | GenArg (Rawwit tag, v) :: args -> + match genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_command ty (f v) args + end + +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = + let open Extend in function +| TUlist1 l -> Alist1 (untype_user_symbol l) +| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUlist0 l -> Alist0 (untype_user_symbol l) +| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUopt o -> Aopt (untype_user_symbol o) +| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a)) +| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i) + +let rec untype_grammar : type r s. (r, s) ty_sig -> 'a Egramml.grammar_prod_item list = function +| TyNil -> [] +| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty +| TyNonTerminal (tu, ty) -> + let t = Genarg.rawwit (Egramml.proj_symbol tu) in + let symb = untype_user_symbol tu in + Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty + +let vernac_extend ~command ?classifier ?entry ext = + let get_classifier (TyML (_, ty, _, cl)) = match cl with + | Some cl -> untype_classifier ty cl + | None -> + match classifier with + | Some cl -> fun _ -> cl command + | None -> + let e = match entry with + | None -> "COMMAND" + | Some e -> Pcoq.Gram.Entry.name e + in + let msg = Printf.sprintf "\ + Vernac entry \"%s\" misses a classifier. \ + A classifier is a function that returns an expression \ + of type vernac_classification (see Vernacexpr). You can: \n\ + - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \ + new vernacular command does not alter the system state;\n\ + - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \ + new vernacular command alters the system state but not the \ + parser nor it starts a proof or ends one;\n\ + - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \ + a global function f. The function f will be called passing\ + \"%s\" as the only argument;\n\ + - Add a specific classifier in each clause using the syntax:\n\ + '[...] => [ f ] -> [...]'.\n\ + Specific classifiers have precedence over global \ + classifiers. Only one classifier is called." + command e e e command + in + CErrors.user_err (Pp.strbrk msg) + in + let cl = Array.map_of_list get_classifier ext in + let iter i (TyML (depr, ty, f, _)) = + let f = untype_command ty f in + let r = untype_grammar ty in + let () = vinterp_add depr (command, i) f in + Egramml.extend_vernac_command_grammar (command, i) entry r + in + let () = declare_vernac_classifier command cl in + List.iteri iter ext + +(** VERNAC ARGUMENT EXTEND registering *) + +type 'a argument_rule = +| Arg_alias of 'a Pcoq.Entry.t +| Arg_rules of 'a Extend.production_rule list + +type 'a vernac_argument = { + arg_printer : 'a -> Pp.t; + arg_parsing : 'a argument_rule; +} + +let vernac_argument_extend ~name arg = + let wit = Genarg.create_arg name in + let entry = match arg.arg_parsing with + | Arg_alias e -> + let () = Pcoq.register_grammar wit e in + e + | Arg_rules rules -> + let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in + let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + e + in + let pr = arg.arg_printer in + let pr x = Genprint.PrinterBasic (fun () -> pr x) in + let () = Genprint.register_vernac_print0 wit pr in + (wit, entry) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli new file mode 100644 index 0000000000..7feaccd9a3 --- /dev/null +++ b/vernac/vernacextend.mli @@ -0,0 +1,118 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <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) *) +(************************************************************************) + +(** Vernacular Extension data *) + +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or + alters the global state or is a control command like BackTo or is + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) +type vernac_type = + (* Start of a proof *) + | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) + | VtSideff of vernac_sideff_type + (* End of a proof *) + | VtQed of vernac_qed_type + (* A proof step *) + | VtProofStep of { + parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; + proof_block_detection : proof_block_name option + } + (* To be removed *) + | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) + | VtQuery + (* To be removed *) + | VtMeta + | VtUnknown +and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) +and vernac_start = string * opacity_guarantee * Names.Id.t list +and vernac_sideff_type = Names.Id.t list +and opacity_guarantee = + | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) + | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) +and solving_tac = bool (** a terminator *) +and anon_abstracting_tac = bool (** abstracting anonymously its result *) +and proof_block_name = string (** open type of delimiters *) + +type vernac_when = + | VtNow + | VtLater +type vernac_classification = vernac_type * vernac_when + +(** Interpretation of extended vernac phrases. *) + +type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list + +val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +(** {5 VERNAC EXTEND} *) + +type classifier = Genarg.raw_generic_argument list -> vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> + ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +(** Wrapper to dynamically extend vernacular commands. *) +val vernac_extend : + command:string -> + ?classifier:(string -> vernac_classification) -> + ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> + ty_ml list -> unit + +(** {5 VERNAC ARGUMENT EXTEND} *) + +type 'a argument_rule = +| Arg_alias of 'a Pcoq.Entry.t + (** This is used because CAMLP5 parser can be dumb about rule factorization, + which sometimes requires two entries to be the same. *) +| Arg_rules of 'a Extend.production_rule list + (** There is a discrepancy here as we use directly extension rules and thus + entries instead of ty_user_symbol and thus arguments as roots. *) + +type 'a vernac_argument = { + arg_printer : 'a -> Pp.t; + arg_parsing : 'a argument_rule; +} + +val vernac_argument_extend : name:string -> 'a vernac_argument -> + ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t + +(** {5 STM classifiers} *) +val get_vernac_classifier : Vernacexpr.extend_name -> classifier + +(** Standard constant classifiers *) +val classify_as_query : vernac_classification +val classify_as_sideeff : vernac_classification +val classify_as_proofstep : vernac_classification diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml deleted file mode 100644 index eb4282705e..0000000000 --- a/vernac/vernacinterp.ml +++ /dev/null @@ -1,77 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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 Util -open Pp -open CErrors - -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t - -type plugin_args = Genarg.raw_generic_argument list - -(* Table of vernac entries *) -let vernac_tab = - (Hashtbl.create 211 : - (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) - -let vinterp_add depr s f = - try - Hashtbl.add vernac_tab s (depr, f) - with Failure _ -> - user_err ~hdr:"vinterp_add" - (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") - -let overwriting_vinterp_add s f = - begin - try - let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s - with Not_found -> () - end; - Hashtbl.add vernac_tab s (false, f) - -let vinterp_map s = - try - Hashtbl.find vernac_tab s - with Failure _ | Not_found -> - user_err ~hdr:"Vernac Interpreter" - (str"Cannot find vernac command " ++ str (fst s) ++ str".") - -let vinterp_init () = Hashtbl.clear vernac_tab - -let warn_deprecated_command = - let open CWarnings in - create ~name:"deprecated-command" ~category:"deprecated" - (fun pr -> str "Deprecated vernacular command: " ++ pr) - -(* Interpretation of a vernac command *) - -let call opn converted_args ~atts ~st = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then - let rules = Egramml.get_extend_vernac_rule opn in - let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" - in - let pr = pr_sequence pr_gram rules in - warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts ~st - with - | reraise -> - let reraise = CErrors.push reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - iraise reraise diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli deleted file mode 100644 index 0fc02c6915..0000000000 --- a/vernac/vernacinterp.mli +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <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) *) -(************************************************************************) - -(** Interpretation of extended vernac phrases. *) - -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t - -type plugin_args = Genarg.raw_generic_argument list - -val vinterp_init : unit -> unit -val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit -val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit - -val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t |