diff options
34 files changed, 750 insertions, 163 deletions
@@ -1,4 +1,4 @@ -Changes from V8.5beta2 to ... +Changes from V8.5beta2 to V8.5beta3 =================================== Vernacular commands @@ -8,6 +8,7 @@ Vernacular commands - New option "Strict Universe Declaration", set by default. It enforces the declaration of all polymorphic universes appearing in a definition when introducing it. +- New command "Show id" to show goal named id. Tactics @@ -42,7 +43,8 @@ solved by the automatic tactic. of incompatibilities). - Hints costs are now correctly taken into account (potential source of incompatibilities). - +- Documented the Hint Cut command that allows control of the + proof-search during typeclass resolution (see reference manual). API diff --git a/checker/check.ml b/checker/check.ml index 2bc470aea..21c8f1c5b 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -46,7 +46,7 @@ type library_t = { library_opaques : Cic.opaque_table; library_deps : Cic.library_deps; library_digest : Cic.vodigest; - library_extra_univs : Univ.constraints } + library_extra_univs : Univ.ContextSet.t } module LibraryOrdered = struct @@ -97,7 +97,7 @@ let access_opaque_univ_table dp i = let t = LibraryMap.find dp !opaque_univ_tables in assert (i < Array.length t); Future.force t.(i) - with Not_found -> Univ.empty_constraint + with Not_found -> Univ.ContextSet.empty let _ = Declarations.indirect_opaque_access := access_opaque_table @@ -347,9 +347,8 @@ let intern_from_file (dir, f) = LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) opaque_csts; let extra_cst = - Option.default Univ.empty_constraint - (Option.map (fun (_,cs,_) -> - Univ.ContextSet.constraints cs) opaque_csts) in + Option.default Univ.ContextSet.empty + (Option.map (fun (_,cs,_) -> cs) opaque_csts) in mk_library sd md f table digest extra_cst let get_deps (dir, f) = diff --git a/checker/declarations.ml b/checker/declarations.ml index 36e6a7cab..32d1713a8 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -426,7 +426,7 @@ let subst_lazy_constr sub = function let indirect_opaque_access = ref ((fun dp i -> assert false) : DirPath.t -> int -> constr) let indirect_opaque_univ_access = - ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints) + ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.ContextSet.t) let force_lazy_constr = function | Indirect (l,dp,i) -> @@ -435,7 +435,7 @@ let force_lazy_constr = function let force_lazy_constr_univs = function | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i - | _ -> Univ.empty_constraint + | _ -> Univ.ContextSet.empty let subst_constant_def sub = function | Undef inl -> Undef inl @@ -457,6 +457,8 @@ let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Def _ | Undef _ -> false +let opaque_univ_context cb = force_lazy_constr_univs cb.const_body + let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in let t' = subst_mps sub t in diff --git a/checker/declarations.mli b/checker/declarations.mli index 3c6db6ab7..456df8369 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -2,17 +2,18 @@ open Names open Cic val force_constr : constr_substituted -> constr -val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints +val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t val from_val : constr -> constr_substituted val indirect_opaque_access : (DirPath.t -> int -> constr) ref -val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref +val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref (** Constant_body *) val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool val is_opaque : constant_body -> bool +val opaque_univ_context : constant_body -> Univ.ContextSet.t (* Mutual inductives *) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index d3bc8373a..81a3cc035 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -28,7 +28,7 @@ let set_engagement c = let full_add_module dp mb univs digest = let env = !genv in let env = push_context_set ~strict:true mb.mod_constraints env in - let env = add_constraints univs env in + let env = push_context_set ~strict:true univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest @@ -83,7 +83,7 @@ let import file clib univs digest = check_engagement env clib.comp_enga; let mb = clib.comp_mod in Mod_checking.check_module - (add_constraints univs + (push_context_set ~strict:true univs (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb; stamp_library file digest; full_add_module clib.comp_name mb univs digest diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index e16e64e6a..892a8d2cc 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -15,6 +15,6 @@ val get_env : unit -> env val set_engagement : engagement -> unit val import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit val unsafe_import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 67ce7e8cd..fae0bd5e5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3788,12 +3788,47 @@ Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. -info_auto with eqdec. +Info 1 auto with eqdec. \end{coq_example} \begin{coq_eval} Abort. \end{coq_eval} +\item \texttt{Cut} {\textit{regexp}} +\label{HintCut} +\comindex{Hint Cut} + + \textit{Warning:} these hints currently only apply to typeclass proof search and + the \texttt{typeclasses eauto} tactic. + + This command can be used to cut the proof-search tree according to a + regular expression matching paths to be cut. The grammar for regular + expressions is the following: +\[\begin{array}{lcll} + e & ::= & \ident & \text{ hint or instance identifier } \\ + & & \texttt{*} & \text{ any hint } \\ + & & e | e' & \text{ disjunction } \\ + & & e ; e' & \text{ sequence } \\ + & & ! e & \text{ Kleene star } \\ + & & \texttt{emp} & \text{ empty } \\ + & & \texttt{eps} & \text{ epsilon } \\ + & & \texttt{(} e \texttt{)} & +\end{array}\] + +The \texttt{emp} regexp does not match any search path while +\texttt{eps} matches the empty path. During proof search, the path of +successive successful hints on a search branch is recorded, as a list of +identifiers for the hints (note \texttt{Hint Extern}'s do not have an +associated identitier). Before applying any hint $\ident$ the current +path $p$ extended with $\ident$ is matched against the current cut +expression $c$ associated to the hint database. If matching succeeds, +the hint is \emph{not} applied. The semantics of \texttt{Hint Cut} $e$ +is to set the cut expression to $c | e$, the initial cut expression +being \texttt{emp}. + + + + \end{itemize} \Rem One can use an \texttt{Extern} hint with no pattern to do diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index cd8222269..f47973601 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -7,9 +7,7 @@ \asection{General Presentation} \begin{flushleft} - \em The status of Universe Polymorphism is experimental. Some features - are not compatible with it (yet): bytecode compilation does not handle - polymorphic definitions, it treats them as opaque constants. + \em The status of Universe Polymorphism is experimental. \end{flushleft} This section describes the universe polymorphic extension of Coq. @@ -65,7 +63,7 @@ Now \texttt{pidentity} is used at two different levels: at the head of the application it is instantiated at \texttt{Top.3} while in the argument position it is instantiated at \texttt{Top.4}. This definition is only valid as long as \texttt{Top.4} is strictly smaller than -\texttt{Top.3}, as show by the constraints. Not that this definition is +\texttt{Top.3}, as show by the constraints. Note that this definition is monomorphic (not universe polymorphic), so in turn the two universes are actually global levels. @@ -119,18 +117,28 @@ producing global universe constraints, one can use the \begin{itemize} \item \texttt{Lemma}, \texttt{Axiom}, and all the other ``definition'' keywords support polymorphism. -\item \texttt{Variables}, \texttt{Context} in a section support polymorphism. - This means that the - variables are discharged polymorphically over definitions that use - them. In other words, two definitions in the section sharing a common - variable will both get parameterized by the universes produced by the - variable declaration. This is in contrast to a ``mononorphic'' variable - which introduces global universes, making the two definitions depend on - the \emph{same} global universes associated to the variable. +\item \texttt{Variables}, \texttt{Context}, \texttt{Universe} and + \texttt{Constraint} in a section support polymorphism. This means + that the universe variables (and associated constraints) are + discharged polymorphically over definitions that use them. In other + words, two definitions in the section sharing a common variable will + both get parameterized by the universes produced by the variable + declaration. This is in contrast to a ``mononorphic'' variable which + introduces global universes and constraints, making the two + definitions depend on the \emph{same} global universes associated to + the variable. \item \texttt{Hint \{Resolve, Rewrite\}} will use the auto/rewrite hint polymorphically, not at a single instance. \end{itemize} +\asection{Global and local universes} + +Each universe is declared in a global or local environment before it can +be used. To ensure compatibility, every \emph{global} universe is set to +be strictly greater than \Set~when it is introduced, while every +\emph{local} (i.e. polymorphically quantified) universe is introduced as +greater or equal to \Set. + \asection{Conversion and unification} The semantics of conversion and unification have to be modified a little @@ -173,23 +181,48 @@ This definition is elaborated by minimizing the universe of id to level generated at the application of id and a constraint that $\Set \le i$. This minimization process is applied only to fresh universe variables. It simply adds an equation between the variable and its lower -bound if it is an atomic universe (i.e. not an algebraic max()). +bound if it is an atomic universe (i.e. not an algebraic \texttt{max()} +universe). -\asection{Explicit Universes} +The option \texttt{Unset Universe Minimization ToSet} disallows +minimization to the sort $\Set$ and only collapses floating universes +between themselves. -\begin{flushleft} - \em The design and implementation of explicit universes is very - experimental and is likely to change in future versions. -\end{flushleft} +\asection{Explicit Universes} The syntax has been extended to allow users to explicitly bind names to -universes and explicitly instantiate polymorphic -definitions. Currently, binding is implicit at the first occurrence of a -universe name. For example, i and j below are introduced by the -annotations attached to Types. +universes and explicitly instantiate polymorphic definitions. + +\subsection{\tt Universe {\ident}. + \comindex{Universe} + \label{UniverseCmd}} + +In the monorphic case, this command declare a new global universe named +{\ident}. It supports the polymorphic flag only in sections, meaning the +universe quantification will be discharged on each section definition +independently. + +\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}. + \comindex{Constraint} + \label{ConstraintCmd}} + +This command declare a new constraint between named universes. +The order relation can be one of $<$, $\le$ or $=$. If consistent, +the constraint is then enforced in the global environment. Like +\texttt{Universe}, it can be used with the \texttt{Polymorphic} prefix +in sections only to declare constraints discharged at section closing time. + +\begin{ErrMsgs} +\item \errindex{Undeclared universe {\ident}}. +\item \errindex{Universe inconsistency} +\end{ErrMsgs} + +\subsection{Polymorphic definitions} +For polymorphic definitions, the declaration of (all) universe levels +introduced by a definition uses the following syntax: \begin{coq_example*} -Polymorphic Definition le (A : Type@{i}) : Type@{j} := A. +Polymorphic Definition le@{i j} (A : Type@{i}) : Type@{j} := A. \end{coq_example*} \begin{coq_example} Print le. @@ -197,40 +230,32 @@ Print le. During refinement we find that $j$ must be larger or equal than $i$, as we are using $A : Type@{i} <= Type@{j}$, hence the generated -constraint. Note that the names here are not bound in the final -definition, they just allow to specify locally what relations should -hold. In the term and in general in proof mode, universe names -introduced in the types can be referred to in terms. +constraint. At the end of a definition or proof, we check that the only +remaining universes are the ones declared. In the term and in general in +proof mode, introduced universe names can be referred to in +terms. Note that local universe names shadow global universe names. +During a proof, one can use \texttt{Show Universes} to display +the current context of universes. Definitions can also be instantiated explicitly, giving their full instance: \begin{coq_example} Check (pidentity@{Set}). -Check (le@{i j}). +Universes k l. +Check (le@{k l}). \end{coq_example} User-named universes are considered rigid for unification and are never minimized. -Finally, two commands allow to name \emph{global} universes and constraints. - -\subsection{\tt Universe {\ident}. - \comindex{Universe} - \label{UniverseCmd}} +\subsection{\tt Unset Strict Universe Declaration. + \optindex{StrictUniverseDeclaration} + \label{StrictUniverseDeclaration}} -This command declare a new global universe named {\ident}. - -\subsection{\tt Constraint {\ident} {\textit{ord}} {\ident}. - \comindex{Constraint} - \label{ConstraintCmd}} - -This command declare a new constraint between named universes. -The order relation can be one of $<$, $<=$ or $=$. If consistent, -the constraint is then enforced in the global environment. - -\begin{ErrMsgs} -\item \errindex{Undeclared universe {\ident}}. -\item \errindex{Universe inconsistency} -\end{ErrMsgs} +The command \texttt{Unset Strict Universe Declaration} allows one to +freely use identifiers for universes without declaring them first, with +the semantics that the first use declares it. In this mode, the universe +names are not associated with the definition or proof once it has been +defined. This is meant mainly for debugging purposes. %%% Local Variables: %%% mode: latex diff --git a/engine/evd.ml b/engine/evd.ml index 40409fe7f..60239ebfe 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -945,7 +945,7 @@ let update_sigma_env evd env = (* Conversion w.r.t. an evar map and its local universes. *) -let conversion_gen env evd pb t u = +let test_conversion_gen env evd pb t u = match pb with | Reduction.CONV -> Reduction.trans_conv_universes @@ -955,14 +955,8 @@ let conversion_gen env evd pb t u = full_transparent_state ~evars:(existential_opt_value evd) env (UState.ugraph evd.universes) t u -(* let conversion_gen_key = Profile.declare_profile "conversion_gen" *) -(* let conversion_gen = Profile.profile5 conversion_gen_key conversion_gen *) - -let conversion env d pb t u = - conversion_gen env d pb t u; d - let test_conversion env d pb t u = - try conversion_gen env d pb t u; true + try test_conversion_gen env d pb t u; true with _ -> false exception UniversesDiffer = UState.UniversesDiffer diff --git a/engine/evd.mli b/engine/evd.mli index 3a95b77f0..25d8a8c3d 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -571,14 +571,11 @@ val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** - Conversion w.r.t. an evar map: might generate universe unifications - that are kept in the evarmap. - Raises [NotConvertible]. *) - -val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map + Conversion w.r.t. an evar map, not unifying universes. See + [Reductionops.infer_conv] for conversion up-to universes. *) val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool -(** This one forgets about the assignemts of universes. *) +(** WARNING: This does not allow unification of universes *) val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool (** Syntactic equality up to universes, recording the associated constraints *) diff --git a/engine/uState.ml b/engine/uState.ml index 0901d81e9..a00d9ccd1 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -32,9 +32,8 @@ type t = uctx_univ_variables : Universes.universe_opt_subst; (** The local universes that are unification variables *) uctx_univ_algebraic : Univ.universe_set; - (** The subset of unification variables that - can be instantiated with algebraic universes as they appear in types - and universe instances only. *) + (** The subset of unification variables that can be instantiated with + algebraic universes as they appear in inferred types only. *) uctx_universes : UGraph.t; (** The current graph extended with the local constraints *) uctx_initial_universes : UGraph.t; (** The graph at the creation of the evar_map *) } diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index f89f076b5..99264dbe0 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -40,7 +40,8 @@ type scope_name = string type goal_reference = | OpenSubgoals | NthGoal of int - | GoalId of goal_identifier + | GoalId of Id.t + | GoalUid of goal_identifier type printable = | PrintTables diff --git a/kernel/univ.ml b/kernel/univ.ml index b303a1a5a..4cc34e41e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -991,7 +991,7 @@ struct let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) + h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) @@ -1065,7 +1065,7 @@ struct let pr prl (univs, cst as ctx) = if is_empty ctx then mt() else - LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst) + h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) let constraints (univs, cst) = cst let levels (univs, cst) = univs diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 7f5459bfa..017f0ea50 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -73,8 +73,10 @@ GEXTEND Gram | IDENT "Unfocused" -> VernacUnfocused | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals) | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n)) + | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id)) + | IDENT "Show"; IDENT "Goal" -> VernacShow (ShowGoal (GoalId (Names.Id.of_string "Goal"))) | IDENT "Show"; IDENT "Goal"; n = string -> - VernacShow (ShowGoal (GoalId n)) + VernacShow (ShowGoal (GoalUid n)) | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural -> VernacShow (ShowGoalImplicitly n) | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index f06207c3b..35bc1de59 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,21 +42,20 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -(** - forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed - hd ?A (l : list t) -> A = t +let refresh_level evd s = + match Evd.is_sort_variable evd s with + | None -> true + | Some l -> not (Evd.is_flexible_level evd l) -*) let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in - let rec refresh dir t = + let rec refresh status dir t = match kind_of_term t with | Sort (Type u as s) when (match Univ.universe_level u with - | None -> true - | Some l -> not onlyalg && Option.is_empty (Evd.is_sort_variable evd s)) -> - let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in + | None -> true + | Some l -> not onlyalg && refresh_level evd s) -> let s' = evd_comb0 (new_sort_variable status) evdref in let evd = if dir then set_leq_sort env !evdref s' s @@ -64,11 +63,11 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = in modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> - mkProd (na,u,refresh dir v) + mkProd (na,u,refresh status dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = - match kind_of_term t with + match kind_of_term (whd_evar !evdref t) with | App (f, args) when is_template_polymorphic env f -> let pos = get_polymorphic_positions f in refresh_polymorphic_positions args pos @@ -77,7 +76,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh true evi.evar_concl in + let ty' = refresh univ_flexible true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -99,7 +98,7 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t = if isArity t then (match pbty with | None -> t - | Some dir -> refresh dir t) + | Some dir -> refresh univ_rigid dir t) else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t @@ -1275,7 +1274,10 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = | [c,evd] -> (* solve_candidates might have been called recursively in the mean *) (* time and the evar been solved by the filtering process *) - if Evd.is_undefined evd evk then Evd.define evk c evd else evd + if Evd.is_undefined evd evk then + let evd' = Evd.define evk c evd in + check_evar_instance evd' evk c conv_algo + else evd | l when List.length l < List.length l' -> let candidates = List.map fst l in restrict_evar evd evk None (UpdateWith candidates) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index bc9f08331..508b9e802 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -715,7 +715,8 @@ let define_pure_evar_as_product evd evk = let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in let concl = whd_betadeltaiota evenv evd evi.evar_concl in let s = destSort concl in - let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in + let evd1,(dom,u1) = + new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in let evd2,rng = let newenv = push_named (id, None, dom) evenv in let src = evar_source evk evd1 in @@ -724,8 +725,9 @@ let define_pure_evar_as_product evd evk = (* Impredicative product, conclusion must fall in [Prop]. *) new_evar_unsafe newenv evd1 concl ~src ~filter else + let status = univ_flexible_alg in let evd3, (rng, srng) = - new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in + new_type_evar newenv evd1 status ~src ~filter in let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in evd3, rng diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c2cf1f83d..3f9ac87a6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -118,7 +118,7 @@ let _ = { optsync = true; optdepr = false; optname = "minimization to Set"; - optkey = ["Universe";"set";"Minimization"]; + optkey = ["Universe";"Minimization";"ToSet"]; optread = Universes.is_set_minimization; optwrite = (:=) Universes.set_minimization }) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 00c276bdb..72b9cafe3 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -594,7 +594,8 @@ module Make let pr_goal_reference = function | OpenSubgoals -> mt () | NthGoal n -> spc () ++ int n - | GoalId n -> spc () ++ str n in + | GoalId id -> spc () ++ pr_id id + | GoalUid n -> spc () ++ str n in let pr_showable = function | ShowGoal n -> keyword "Show" ++ pr_goal_reference n | ShowGoalImplicitly n -> keyword "Show Implicit Arguments" ++ pr_opt int n diff --git a/printing/printer.ml b/printing/printer.ml index 202b4f2bc..2e112f9ac 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -455,14 +455,17 @@ let pr_ne_evar_set hd tl sigma l = else mt () +let pr_selected_subgoal name sigma g = + let pg = default_pr_goal { sigma=sigma ; it=g; } in + v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g + ++ str " is:" ++ cut () ++ pg) + let default_pr_subgoal n sigma = let rec prrec p = function | [] -> error "No such goal." | g::rest -> if Int.equal p 1 then - let pg = default_pr_goal { sigma=sigma ; it=g; } in - v 0 (str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g - ++ str " is:" ++ cut () ++ pg) + pr_selected_subgoal (int n) sigma g else prrec (p-1) rest in @@ -652,9 +655,17 @@ let pr_nth_open_subgoal n = let pr_goal_by_id id = let p = Proof_global.give_me_the_proof () in - let g = Goal.get_by_uid id in + try + Proof.in_proof p (fun sigma -> + let g = Evd.evar_key id sigma in + pr_selected_subgoal (pr_id id) sigma g) + with Not_found -> error "No such goal." + +let pr_goal_by_uid uid = + let p = Proof_global.give_me_the_proof () in + let g = Goal.get_by_uid uid in let pr gs = - v 0 (str "goal / evar " ++ str id ++ str " is:" ++ cut () + v 0 (str "goal / evar " ++ str uid ++ str " is:" ++ cut () ++ pr_goal gs) in try diff --git a/printing/printer.mli b/printing/printer.mli index 0a44e4f10..5c60b8936 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -176,7 +176,8 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> Term.types ContextObjectMap.t -> std_ppcmds -val pr_goal_by_id : string -> std_ppcmds +val pr_goal_by_id : Id.t -> std_ppcmds +val pr_goal_by_uid : string -> std_ppcmds type printer_pr = { pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; diff --git a/proofs/logic.ml b/proofs/logic.ml index 7d101b4c7..a38a36bdc 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -356,9 +356,11 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = if is_template_polymorphic env f then - let sigma, ty = + let ty = (* Template sort-polymorphism of definition and inductive types *) - type_of_global_reference_knowing_conclusion env sigma f conclty + let firstmeta = Array.findi (fun i x -> occur_meta x) l in + let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in + type_of_global_reference_knowing_parameters env sigma f args in goalacc, ty, sigma, f else diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 96ba88233..d69b5b421 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -387,20 +387,23 @@ let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t let tclFOCUSID id t = let open Proof in Pv.get >>= fun initial -> - let rec aux n = function - | [] -> tclZERO (NoSuchGoals 1) - | g::l -> - if Names.Id.equal (Evd.evar_ident g initial.solution) id then - let (focused,context) = focus n n initial in - Pv.set focused >> - t >>= fun result -> - Pv.modify (fun next -> unfocus context next) >> - return result - else - aux (n+1) l in - aux 1 initial.comb - - + try + let ev = Evd.evar_key id initial.solution in + try + let n = CList.index Evar.equal ev initial.comb in + (* goal is already under focus *) + let (focused,context) = focus n n initial in + Pv.set focused >> + t >>= fun result -> + Pv.modify (fun next -> unfocus context next) >> + return result + with Not_found -> + (* otherwise, save current focus and work purely on the shelve *) + Comb.set [ev] >> + t >>= fun result -> + Comb.set initial.comb >> + return result + with Not_found -> tclZERO (NoSuchGoals 1) (** {7 Dispatching on goals} *) diff --git a/stm/stm.ml b/stm/stm.ml index 0c0bdc827..623629745 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2317,6 +2317,17 @@ let edit_at id = | { step = `Fork _ } -> false | { next } -> aux next in aux (VCS.get_branch_pos (VCS.current_branch ())) in + let rec is_pure_aux id = + let view = VCS.visit id in + match view.step with + | `Cmd _ -> is_pure_aux view.next + | `Fork _ -> true + | _ -> false in + let is_pure id = + match (VCS.visit id).step with + | `Qed (_,last_step) -> is_pure_aux last_step + | _ -> assert false + in let is_ancestor_of_cur_branch id = Vcs_.NodeSet.mem id (VCS.reachable (VCS.get_branch_pos (VCS.current_branch ()))) in @@ -2327,7 +2338,9 @@ let edit_at id = let rec master_for_br root tip = if Stateid.equal tip Stateid.initial then tip else match VCS.visit tip with - | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip + | { step = (`Fork _ | `Qed _) } -> tip + | { step = `Sideff (`Ast(_,id)) } -> id + | { step = `Sideff _ } -> tip | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = @@ -2377,7 +2390,7 @@ let edit_at id = | _, Some _, None -> assert false | false, Some (qed_id,start), Some(mode,bn) -> let tip = VCS.cur_tip () in - if has_failed qed_id && not !Flags.async_proofs_never_reopen_branch + if has_failed qed_id && is_pure qed_id && not !Flags.async_proofs_never_reopen_branch then reopen_branch start id mode qed_id tip bn else backto id (Some bn) | true, Some (qed_id,_), Some(mode,bn) -> diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 0d24b7138..0c8440fe5 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -641,12 +641,7 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ convert_concl_no_check x DEFAULTcast ] END - -let pr_hints_path_atom prc _ _ a = - match a with - | PathAny -> str"." - | PathHints grs -> - pr_sequence Printer.pr_global grs +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom ARGUMENT EXTEND hints_path_atom TYPED AS hints_path_atom @@ -655,15 +650,7 @@ ARGUMENT EXTEND hints_path_atom | [ "*" ] -> [ PathAny ] END -let pr_hints_path prc prx pry c = - let rec aux = function - | PathAtom a -> pr_hints_path_atom prc prx pry a - | PathStar p -> str"(" ++ aux p ++ str")*" - | PathSeq (p, p') -> aux p ++ spc () ++ aux p' - | PathOr (p, p') -> str "(" ++ aux p ++ str"|" ++ aux p' ++ str")" - | PathEmpty -> str"ø" - | PathEpsilon -> str"ε" - in aux c +let pr_hints_path prc prx pry c = Hints.pp_hints_path c ARGUMENT EXTEND hints_path TYPED AS hints_path diff --git a/tactics/hints.ml b/tactics/hints.ml index 4ba9adafe..5630d20b5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -382,15 +382,19 @@ let rec normalize_path h = let path_derivate hp hint = normalize_path (path_derivate hp hint) +let pp_hints_path_atom a = + match a with + | PathAny -> str"*" + | PathHints grs -> pr_sequence pr_global grs + let rec pp_hints_path = function - | PathAtom (PathAny) -> str"." - | PathAtom (PathHints grs) -> pr_sequence pr_global grs - | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" + | PathAtom pa -> pp_hints_path_atom pa + | PathStar p -> str "!(" ++ pp_hints_path p ++ str")" | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p' | PathOr (p, p') -> str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")" - | PathEmpty -> str"Ø" - | PathEpsilon -> str"ε" + | PathEmpty -> str"emp" + | PathEpsilon -> str"eps" let subst_path_atom subst p = match p with diff --git a/tactics/hints.mli b/tactics/hints.mli index af4d3d1f6..3a0521f66 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -70,6 +70,7 @@ type hints_path = val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool val path_derivate : hints_path -> hints_path_atom -> hints_path +val pp_hints_path_atom : hints_path_atom -> Pp.std_ppcmds val pp_hints_path : hints_path -> Pp.std_ppcmds module Hint_db : diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fc453cfaf..bb97c80be 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -242,8 +242,9 @@ let convert_hyp_no_check = convert_hyp ~check:false let convert_gen pb x y = Proofview.Goal.enter { enter = begin fun gl -> try - let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in - Proofview.Unsafe.tclEVARS sigma + let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in + if b then Proofview.Unsafe.tclEVARS sigma + else Tacticals.New.tclFAIL 0 (str "Not convertible") with (* Reduction.NotConvertible *) _ -> (** FIXME: Sometimes an anomaly is raised from conversion *) Tacticals.New.tclFAIL 0 (str "Not convertible") @@ -3300,7 +3301,7 @@ let is_defined_variable env id = match lookup_named id env with | (_, Some _, _) -> true let abstract_args gl generalize_vars dep id defined f args = - let sigma = Tacmach.project gl in + let sigma = ref (Tacmach.project gl) in let env = Tacmach.pf_env gl in let concl = Tacmach.pf_concl gl in let dep = dep || dependent (mkVar id) concl in @@ -3317,11 +3318,12 @@ let abstract_args gl generalize_vars dep id defined f args = *) let aux (prod, ctx, ctxenv, c, args, eqs, refls, nongenvars, vars, env) arg = let (name, _, ty), arity = - let rel, c = Reductionops.splay_prod_n env sigma 1 prod in + let rel, c = Reductionops.splay_prod_n env !sigma 1 prod in List.hd rel, c in let argty = Tacmach.pf_unsafe_type_of gl arg in - let ty = (* refresh_universes_strict *) ty in + let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma ty in + let () = sigma := sigma' in let lenctx = List.length ctx in let liftargty = lift lenctx argty in let leq = constr_cmp Reduction.CUMUL liftargty ty in @@ -3360,8 +3362,9 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then + let tyf' = Tacmach.pf_unsafe_type_of gl f' in let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (Tacmach.pf_unsafe_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' + Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = @@ -3370,9 +3373,12 @@ let abstract_args gl generalize_vars dep id defined f args = hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars else [] in - let body, c' = if defined then Some c', Retyping.get_type_of ctxenv Evd.empty c' else None, c' in - Some (make_abstract_generalize gl id concl dep ctx body c' eqs args refls, - dep, succ (List.length ctx), vars) + let body, c' = + if defined then Some c', Retyping.get_type_of ctxenv !sigma c' + else None, c' + in + let term = make_abstract_generalize {gl with sigma = !sigma} id concl dep ctx body c' eqs args refls in + Some (term, !sigma, dep, succ (List.length ctx), vars) else None let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = @@ -3394,20 +3400,26 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = let newc = Tacmach.New.of_old (fun gl -> abstract_args gl generalize_vars force_dep id def f args) gl in match newc with | None -> Proofview.tclUNIT () - | Some (newc, dep, n, vars) -> + | Some (newc, sigma, dep, n, vars) -> let tac = if dep then - Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; - Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] - else - Tacticals.New.tclTHENLIST [Proofview.V82.tactic (refine newc); Proofview.V82.tactic (clear [id]); Tacticals.New.tclDO n intro] + Tacticals.New.tclTHENLIST + [Proofview.Unsafe.tclEVARS sigma; + Proofview.V82.tactic (refine newc); + rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; + Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] + else Tacticals.New.tclTHENLIST + [Proofview.Unsafe.tclEVARS sigma; + Proofview.V82.tactic (refine newc); + Proofview.V82.tactic (clear [id]); + Tacticals.New.tclDO n intro] in if List.is_empty vars then tac else Tacticals.New.tclTHEN tac (Tacticals.New.tclFIRST [revert vars ; Proofview.V82.tactic (fun gl -> tclMAP (fun id -> - tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) + tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) end } let rec compare_upto_variables x y = diff --git a/test-suite/bugs/closed/4151.v b/test-suite/bugs/closed/4151.v new file mode 100644 index 000000000..fec64555f --- /dev/null +++ b/test-suite/bugs/closed/4151.v @@ -0,0 +1,403 @@ +Lemma foo (H : forall A, A) : forall A, A. + Show Universes. + eexact H. +Qed. + +(* File reduced by coq-bug-finder from original input, then from 6390 lines to 397 lines *) +(* coqc version 8.5beta1 (March 2015) compiled on Mar 17 2015 12:34:25 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (1b3759e78f227eb85a128c58b8ce8c11509dd8c3) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.SetoidList. +Require Export Coq.Program.Program. + +Global Set Implicit Arguments. +Global Set Asymmetric Patterns. + +Fixpoint combine_sig_helper {T} {P : T -> Prop} (ls : list T) : (forall x, In x ls -> P x) -> list (sig P). + admit. +Defined. + +Lemma Forall_forall1_transparent_helper_1 {A P} {x : A} {xs : list A} {l : list A} + (H : Forall P l) (H' : x::xs = l) +: P x. + admit. +Defined. +Lemma Forall_forall1_transparent_helper_2 {A P} {x : A} {xs : list A} {l : list A} + (H : Forall P l) (H' : x::xs = l) +: Forall P xs. + admit. +Defined. + +Fixpoint Forall_forall1_transparent {A} (P : A -> Prop) (l : list A) {struct l} +: Forall P l -> forall x, In x l -> P x + := match l as l return Forall P l -> forall x, In x l -> P x with + | nil => fun _ _ f => match f : False with end + | x::xs => fun H x' H' => + match H' with + | or_introl H'' => eq_rect x + P + (Forall_forall1_transparent_helper_1 H eq_refl) + _ + H'' + | or_intror H'' => @Forall_forall1_transparent A P xs (Forall_forall1_transparent_helper_2 H eq_refl) _ H'' + end + end. + +Definition combine_sig {T P ls} (H : List.Forall P ls) : list (@sig T P) + := combine_sig_helper ls (@Forall_forall1_transparent T P ls H). +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Record string_like (CharType : Type) := + { + String :> Type; + Singleton : CharType -> String where "[ x ]" := (Singleton x); + Empty : String; + Concat : String -> String -> String where "x ++ y" := (Concat x y); + bool_eq : String -> String -> bool; + bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y; + Length : String -> nat; + Associativity : forall x y z, (x ++ y) ++ z = x ++ (y ++ z); + LeftId : forall x, Empty ++ x = x; + RightId : forall x, x ++ Empty = x; + Singleton_Length : forall x, Length (Singleton x) = 1; + Length_correct : forall s1 s2, Length s1 + Length s2 = Length (s1 ++ s2); + Length_Empty : Length Empty = 0; + Empty_Length : forall s1, Length s1 = 0 -> s1 = Empty; + Not_Singleton_Empty : forall x, Singleton x <> Empty; + SplitAt : nat -> String -> String * String; + SplitAt_correct : forall n s, fst (SplitAt n s) ++ snd (SplitAt n s) = s; + SplitAt_concat_correct : forall s1 s2, SplitAt (Length s1) (s1 ++ s2) = (s1, s2); + SplitAtLength_correct : forall n s, Length (fst (SplitAt n s)) = min (Length s) n + }. + +Delimit Scope string_like_scope with string_like. +Bind Scope string_like_scope with String. +Arguments Length {_%type_scope _} _%string_like. +Notation "[[ x ]]" := (@Singleton _ _ x) : string_like_scope. +Infix "++" := (@Concat _ _) : string_like_scope. +Infix "=s" := (@bool_eq _ _) (at level 70, right associativity) : string_like_scope. + +Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String) + := Length s1 < Length s2 \/ s1 = s2. +Infix "≤s" := str_le (at level 70, right associativity). + +Record StringWithSplitState {CharType} (String : string_like CharType) (split_stateT : String -> Type) := + { string_val :> String; + state_val : split_stateT string_val }. + +Module Export ContextFreeGrammar. + Require Import Coq.Strings.String. + + Section cfg. + Variable CharType : Type. + + Section definitions. + + Inductive item := + | Terminal (_ : CharType) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + End cfg. + +End ContextFreeGrammar. +Module Export BaseTypes. + Import Coq.Strings.String. + + Local Open Scope string_like_scope. + + Inductive any_grammar CharType := + | include_item (_ : item CharType) + | include_production (_ : production CharType) + | include_productions (_ : productions CharType) + | include_nonterminal (_ : string). + Global Coercion include_item : item >-> any_grammar. + Global Coercion include_production : production >-> any_grammar. + + Section recursive_descent_parser. + Context {CharType : Type} + {String : string_like CharType} + {G : grammar CharType}. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> string -> bool; + remove_nonterminal : nonterminals_listT -> string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal = true + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_computational_types_dataT := + { predata :> parser_computational_predataT; + split_stateT : String -> nonterminals_listT -> any_grammar CharType -> String -> Type }. + + Class parser_computational_dataT' `{parser_computational_types_dataT} := + { split_string_for_production + : forall (str0 : String) (valid : nonterminals_listT) (it : item CharType) (its : production CharType) (str : StringWithSplitState String (split_stateT str0 valid (it::its : production CharType))), + list (StringWithSplitState String (split_stateT str0 valid it) + * StringWithSplitState String (split_stateT str0 valid its)); + split_string_for_production_correct + : forall str0 valid it its str, + let P f := List.Forall f (@split_string_for_production str0 valid it its str) in + P (fun s1s2 => (fst s1s2 ++ snd s1s2 =s str) = true) }. + End recursive_descent_parser. + +End BaseTypes. +Import Coq.Strings.String. + +Section cfg. + Context CharType (String : string_like CharType) (G : grammar CharType). + Context (names_listT : Type) + (initial_names_data : names_listT) + (is_valid_name : names_listT -> string -> bool) + (remove_name : names_listT -> string -> names_listT) + (names_listT_R : names_listT -> names_listT -> Prop) + (remove_name_dec : forall ls name, + is_valid_name ls name = true + -> names_listT_R (remove_name ls name) ls) + (remove_name_1 + : forall ls ps ps', + is_valid_name (remove_name ls ps) ps' = true + -> is_valid_name ls ps' = true) + (remove_name_2 + : forall ls ps ps', + is_valid_name (remove_name ls ps) ps' = false + <-> is_valid_name ls ps' = false \/ ps = ps') + (ntl_wf : well_founded names_listT_R). + + Inductive minimal_parse_of + : forall (str0 : String) (valid : names_listT) + (str : String), + productions CharType -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : names_listT) + (str : String), + production CharType -> Type := + | MinParseProductionNil : forall str0 valid, + @minimal_parse_of_production str0 valid (Empty _) nil + | MinParseProductionCons : forall str0 valid str strs pat pats, + str ++ strs ≤s str0 + -> @minimal_parse_of_item str0 valid str pat + -> @minimal_parse_of_production str0 valid strs pats + -> @minimal_parse_of_production str0 valid (str ++ strs) (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : names_listT) + (str : String), + item CharType -> Type := + | MinParseTerminal : forall str0 valid x, + @minimal_parse_of_item str0 valid [[ x ]]%string_like (Terminal x) + | MinParseNonTerminal + : forall str0 valid str name, + @minimal_parse_of_name str0 valid str name + -> @minimal_parse_of_item str0 valid str (NonTerminal CharType name) + with minimal_parse_of_name + : forall (str0 : String) (valid : names_listT) + (str : String), + string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid name str, + Length str < Length str0 + -> is_valid_name initial_names_data name = true + -> @minimal_parse_of str initial_names_data str (Lookup G name) + -> @minimal_parse_of_name str0 valid str name + | MinParseNonTerminalStrEq + : forall str valid name, + is_valid_name initial_names_data name = true + -> is_valid_name valid name = true + -> @minimal_parse_of str (remove_name valid name) str (Lookup G name) + -> @minimal_parse_of_name str valid str name. +End cfg. + +Local Coercion is_true : bool >-> Sortclass. + +Local Open Scope string_like_scope. + +Section general. + Context {CharType} {String : string_like CharType} {G : grammar CharType}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_stateT : String -> Type; + data' :> _ := {| BaseTypes.predata := predata ; BaseTypes.split_stateT := fun _ _ _ => split_stateT |}; + split_string_for_production + : forall it its, + StringWithSplitState String split_stateT + -> list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT); + split_string_for_production_correct + : forall it its (str : StringWithSplitState String split_stateT), + let P f := List.Forall f (split_string_for_production it its str) in + P (fun s1s2 => + (fst s1s2 ++ snd s1s2 =s str) = true); + premethods :> parser_computational_dataT' + := @Build_parser_computational_dataT' + _ String data' + (fun _ _ => split_string_for_production) + (fun _ _ => split_string_for_production_correct) }. + + Definition split_list_completeT `{data : boolean_parser_dataT} + {str0 valid} + (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) + (split_list : list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT)) + (it : item CharType) (its : production CharType) + := ({ s1s2 : String * String + & (fst s1s2 ++ snd s1s2 =s str) + * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) + * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type) + -> ({ s1s2 : StringWithSplitState String split_stateT * StringWithSplitState String split_stateT + & (In s1s2 split_list) + * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) + * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type). +End general. + +Section recursive_descent_parser. + Context {CharType} + {String : string_like CharType} + {G : grammar CharType}. + Context `{data : @boolean_parser_dataT _ String}. + + Section bool. + Section parts. + Definition parse_item + (str_matches_nonterminal : string -> bool) + (str : StringWithSplitState String split_stateT) + (it : item CharType) + : bool + := match it with + | Terminal ch => [[ ch ]] =s str + | NonTerminal nt => str_matches_nonterminal nt + end. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Fixpoint parse_production + (str : StringWithSplitState String split_stateT) + (pf : str ≤s str0) + (prod : production CharType) + : bool. + Proof. + refine + match prod with + | nil => + + str =s Empty _ + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (let mapF f := map f (combine_sig (split_string_for_production_correct it its str)) in + mapF (fun s1s2p => + (parse_item + (parse_nonterminal (fst (proj1_sig s1s2p)) _) + (fst (proj1_sig s1s2p)) + it) + && parse_production' (snd (proj1_sig s1s2p)) _)%bool) + end; + revert pf; clear; intros; admit. + Defined. + End production. + + End parts. + End bool. +End recursive_descent_parser. + +Section sound. + Context CharType (String : string_like CharType) (G : grammar CharType). + Context `{data : @boolean_parser_dataT CharType String}. + + Section production. + Context (str0 : String) + (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Definition parse_nonterminal_completeT P + := forall valid (str : StringWithSplitState String split_stateT) pf nonterminal (H_sub : P str0 valid nonterminal), + minimal_parse_of_name _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal + -> @parse_nonterminal str pf nonterminal = true. + + Lemma parse_production_complete + valid Pv + (parse_nonterminal_complete : parse_nonterminal_completeT Pv) + (Hinit : forall str (pf : str ≤s str0) nonterminal, + minimal_parse_of_name String G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal + -> Pv str0 valid nonterminal) + (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) + (prod : production CharType) + (split_string_for_production_complete' + : forall str0 valid str pf, + Forall_tails + (fun prod' => + match prod' return Type with + | nil => True + | it::its => split_list_completeT (G := G) (valid := valid) (str0 := str0) str pf (split_string_for_production it its str) it its + end) + prod) + : minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str prod + -> parse_production parse_nonterminal str pf prod = true. + admit. + Defined. + End production. + Context (str0 : String) + (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Goal forall (a : production CharType), + (forall (str1 : String) (valid : nonterminals_listT) + (str : StringWithSplitState String split_stateT) + (pf : str ≤s str1), + Forall_tails + (fun prod' : list (item CharType) => + match prod' with + | [] => True + | it :: its => + split_list_completeT (G := G) (valid := valid) str pf + (split_string_for_production it its str) it its + end) a) -> + forall (str : String) (pf : str ≤s str0) (st : split_stateT str), + parse_production parse_nonterminal + {| string_val := str; state_val := st |} pf a = true. + Proof. + intros a X **. + eapply parse_production_complete. + Focus 3. + exact X. + Undo. + assumption. + Undo. + eassumption. (* no applicable tactic *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v new file mode 100644 index 000000000..60c935459 --- /dev/null +++ b/test-suite/bugs/closed/4394.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) + +Require Import Equality List. +Inductive Foo (I : Type -> Type) (A : Type) : Type := +| foo (B : Type) : A -> I B -> Foo I A. +Definition Family := Type -> Type. +Definition FooToo : Family -> Family := Foo. +Definition optionize (I : Type -> Type) (A : Type) := option (I A). +Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A. +Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. +Definition barRec : Rec (optionize id) := {| rec := bar id |}. +Inductive Empty {T} : T -> Prop := . +Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) : + Empty (a, b) -> False. +Proof. + intro e. + dependent induction e. +Qed. + diff --git a/test-suite/bugs/closed/4397.v b/test-suite/bugs/closed/4397.v new file mode 100644 index 000000000..3566353d8 --- /dev/null +++ b/test-suite/bugs/closed/4397.v @@ -0,0 +1,3 @@ +Require Import Equality. +Theorem foo (u : unit) (H : u = u) : True. +dependent destruction H. diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v index ae3e50d7e..223a98de1 100644 --- a/test-suite/bugs/closed/HoTT_coq_014.v +++ b/test-suite/bugs/closed/HoTT_coq_014.v @@ -3,9 +3,9 @@ Set Implicit Arguments. Generalizable All Variables. Set Universe Polymorphism. -Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' { - Object :> _ := obj; - Morphism' : obj -> obj -> Type; +Polymorphic Record SpecializedCategory@{l k} (obj : Type@{l}) := Build_SpecializedCategory' { + Object :> Type@{l} := obj; + Morphism' : obj -> obj -> Type@{k}; Identity' : forall o, Morphism' o o; Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d' diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index cc8cec470..f934a5c74 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -62,3 +62,47 @@ Axiom cast_coalesce : ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2). Hint Rewrite cast_coalesce : ltamer. + +Require Import Program. +Module HintCut. +Class A (f : nat -> nat) := a : True. +Class B (f : nat -> nat) := b : True. +Class C (f : nat -> nat) := c : True. +Class D (f : nat -> nat) := d : True. +Class E (f : nat -> nat) := e : True. + +Instance a_is_b f : A f -> B f. +Proof. easy. Qed. +Instance b_is_c f : B f -> C f. +Proof. easy. Qed. +Instance c_is_d f : C f -> D f. +Proof. easy. Qed. +Instance d_is_e f : D f -> E f. +Proof. easy. Qed. + +Instance a_compose f g : A f -> A g -> A (compose f g). +Proof. easy. Qed. +Instance b_compose f g : B f -> B g -> B (compose f g). +Proof. easy. Qed. +Instance c_compose f g : C f -> C g -> C (compose f g). +Proof. easy. Qed. +Instance d_compose f g : D f -> D g -> D (compose f g). +Proof. easy. Qed. +Instance e_compose f g : E f -> E g -> E (compose f g). +Proof. easy. Qed. + +Instance a_id : A id. +Proof. easy. Qed. + +Instance foo f : + E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ + id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id). +Proof. + Fail Timeout 1 apply _. (* 3.7s *) + +Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ; + (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. + + Timeout 1 Fail apply _. (* 0.06s *) +Abort. +End HintCut.
\ No newline at end of file diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 83016976e..b04d5168f 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -34,6 +34,27 @@ Tactic Notation "constructor" := constructor_84. Tactic Notation "constructor" int_or_var(n) := constructor_84_n n. Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac. +(** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *) +Tactic Notation "reflexivity" := reflexivity. +Tactic Notation "assumption" := assumption. +Tactic Notation "etransitivity" := etransitivity. +Tactic Notation "cut" constr(c) := cut c. +Tactic Notation "exact_no_check" constr(c) := exact_no_check c. +Tactic Notation "vm_cast_no_check" constr(c) := vm_cast_no_check c. +Tactic Notation "casetype" constr(c) := casetype c. +Tactic Notation "elimtype" constr(c) := elimtype c. +Tactic Notation "lapply" constr(c) := lapply c. +Tactic Notation "transitivity" constr(c) := transitivity c. +Tactic Notation "left" := left. +Tactic Notation "eleft" := eleft. +Tactic Notation "right" := right. +Tactic Notation "eright" := eright. +Tactic Notation "constructor" := constructor. +Tactic Notation "econstructor" := econstructor. +Tactic Notation "symmetry" := symmetry. +Tactic Notation "split" := split. +Tactic Notation "esplit" := esplit. + Global Set Regular Subst Tactic. (** Some names have changed in the standard library, so we add aliases. *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index bf090384d..4a44ad52e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1786,6 +1786,7 @@ let vernac_show = function | OpenSubgoals -> pr_open_subgoals () | NthGoal n -> pr_nth_open_subgoal n | GoalId id -> pr_goal_by_id id + | GoalUid id -> pr_goal_by_uid id in msg_notice info | ShowGoalImplicitly None -> |