diff options
37 files changed, 610 insertions, 157 deletions
@@ -4,6 +4,8 @@ S ltac B ltac S config B config +S ide +B ide S lib B lib S intf @@ -59,6 +59,10 @@ define find $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||') endef +define findindir + $(shell find $(1) $(FIND_VCS_CLAUSE) '(' -name $(2) ')' -print | sed 's|^\./||') +endef + define findx $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||') endef @@ -68,7 +72,7 @@ endef LEXFILES := $(call find, '*.mll') export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') -export CFILES := $(call find, '*.c') +export CFILES := $(call findindir, 'kernel/byterun', '*.c') # NB: The lists of currently existing .ml and .mli files will change # before and after a build or a make clean. Hence we do not export diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 5fe88bf33..f54f3fcc8 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -270,6 +270,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id for constructing compound entries still works over this scheme. Note that in the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound in the parsing rules, so beware of recursive calls. + + For example, to get "wit_constr" you must "open Constrarg" at the top of the file. - Evarutil was split in two parts. The new Evardefine file exposes functions define_evar_* mostly used internally in the unification engine. @@ -296,6 +298,10 @@ define_evar_* mostly used internally in the unification engine. ... let Sigma (xn, sigma, pn) = ... in Sigma (ans, sigma, p1 +> ... +> pn) + + Examples of `Sigma.Unsafe.of_evar_map` include: + + Evarutil.new_evar env (Tacmach.project goal) ty ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty - The Proofview.Goal.*enter family of functions now takes a polymorphic continuation given as a record as an argument. @@ -308,7 +314,11 @@ define_evar_* mostly used internally in the unification engine. Proofview.Goal.enter { enter = begin fun gl -> ... end } -- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` +- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c` +- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)` +- `Pretyping.Termops.mem_named_context` ---> `Engine.Termops.mem_named_context_val` + (`Global.named_context` ---> `Global.named_context_val`) + (`Context.Named.lookup` ---> `Environ.lookup_named_val`) ** Search API ** diff --git a/doc/common/macros.tex b/doc/common/macros.tex index df5ee405f..5abdecfc1 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -72,7 +72,8 @@ %\newcommand{\spec}[1]{\{\,#1\,\}} % Building regular expressions -\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}} +\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}} +\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}} %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*} %\newcommand{\onemany}[1]{$\{$#1$\}$+} \newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}} diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index bd8ee450e..acfc4bea9 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -380,6 +380,7 @@ use implicit generalization (see \ref{SectionContext}). \asubsection{\tt typeclasses eauto} \tacindex{typeclasses eauto} +\label{typeclasseseauto} The {\tt typeclasses eauto} tactic uses a different resolution engine than {\tt eauto} and {\tt auto}. The main differences are the following: diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index c1e552a5d..bef0a1686 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -26,13 +26,13 @@ run by the command {\tt coqtop}. They are two different binary images of \Coq: the byte-code one and the native-code one (if {\ocaml} provides a native-code compiler for your platform, which is supposed in the following). By default, -\verb!coqc! executes the native-code version; this can be overridden -using the \verb!-byte! option. +\verb!coqtop! executes the native-code version; run \verb!coqtop.byte! to +get the byte-code version. The byte-code toplevel is based on an {\ocaml} toplevel (to allow the dynamic link of tactics). You can switch to the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the -\Coq~toplevel with the command \verb!Toplevel.loop();;!. +\Coq~toplevel with the command \verb!Coqloop.loop();;!. \section{Batch compilation ({\tt coqc})} The {\tt coqc} command takes a name {\em file} as argument. Then it diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 99eee44e0..3814e4403 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -713,9 +713,9 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\ & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\ & & \\ -{\inductivebody} & ::= & - {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\ - && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\ +{\inductivebody} & ::= & + {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\ + && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\ & & \\ %% TODO: where ... %% Fixpoints {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\ diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 01dc1dec9..3f1241186 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -114,7 +114,7 @@ following syntax: \begin{tabular}{lcl} {\occclause} & ::= & {\tt in} {\occgoalset} \\ {\occgoalset} & ::= & - \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\ + \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\ & & {\dots} {\tt ,}\\ & & {\ident$_m$} \zeroone{\atoccurrences}}\\ & & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\ @@ -302,7 +302,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}. \begin{ErrMsgs} -\item \errindex{Impossible to unify \dots\ with \dots} +\item \errindex{Unable to unify \dots\ with \dots} The {\tt apply} tactic failed to match the conclusion of {\term} and the current goal. @@ -4621,7 +4621,7 @@ It is equivalent to {\tt apply refl\_equal}. \begin{ErrMsgs} \item \errindex{The conclusion is not a substitutive equation} -\item \errindex{Impossible to unify \dots\ with \dots} +\item \errindex{Unable to unify \dots\ with \dots} \end{ErrMsgs} \subsection{\tt symmetry} diff --git a/engine/evd.ml b/engine/evd.ml index d8a658e3e..bffb40727 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -854,6 +854,13 @@ let is_eq_sort s1 s2 = if Univ.Universe.equal u1 u2 then None else Some (u1, u2) +(* Precondition: l is not defined in the substitution *) +let universe_rigidity evd l = + let uctx = evd.universes in + if Univ.LSet.mem l (Univ.ContextSet.levels (UState.context_set uctx)) then + UnivFlexible (Univ.LSet.mem l (UState.algebraics uctx)) + else UnivRigid + let normalize_universe evd = let vars = ref (UState.subst evd.universes) in let normalize = Universes.normalize_universe_opt_subst vars in diff --git a/engine/evd.mli b/engine/evd.mli index 5c9effd4b..993ed300b 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -467,7 +467,17 @@ val retract_coercible_metas : evar_map -> metabinding list * evar_map (********************************************************* Sort/universe variables *) -(** Rigid or flexible universe variables *) +(** Rigid or flexible universe variables. + + [UnivRigid] variables are user-provided or come from an explicit + [Type] in the source, we do not minimize them or unify them eagerly. + + [UnivFlexible alg] variables are fresh universe variables of + polymorphic constants or generated during refinement, sometimes in + algebraic position (i.e. not appearing in the term at the moment of + creation). They are the candidates for minimization (if alg, to an + algebraic universe) and unified eagerly in the first-order + unification heurstic. *) type rigid = UState.rigid = | UnivRigid @@ -514,7 +524,8 @@ val new_univ_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_ val new_sort_variable : ?loc:Loc.t -> ?name:string -> rigid -> evar_map -> evar_map * sorts val add_global_univ : evar_map -> Univ.Level.t -> evar_map - + +val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map val is_sort_variable : evar_map -> sorts -> Univ.universe_level option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is diff --git a/ide/.merlin b/ide/.merlin index 3f3d9d275..953b5dce4 100644 --- a/ide/.merlin +++ b/ide/.merlin @@ -1,4 +1,4 @@ -PKG lablgtk2.sourceview2 +PKG unix laglgtk2 lablgtk2.sourceview2 S utils B utils diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 47df22807..5dec3b785 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,9 +23,9 @@ #include "coq_values.h" /* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) ((uint32_t)(val) >> 1) -#define value_of_uint32(i) ((value)(((uint32_t)(i) << 1) | 1)) -#define UI64_of_uint32(lo) ((uint64_t)(lo)) +#define uint32_of_value(val) (((uint32_t)(val)) >> 1) +#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1)) +#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo))) #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) /* /spiwack */ diff --git a/kernel/names.ml b/kernel/names.ml index d928d300f..1f138581c 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,9 +34,15 @@ struct let hash = String.hash + let warn_invalid_identifier = + CWarnings.create ~name:"invalid-identifier" ~category:"parsing" + ~default:CWarnings.Disabled + (fun s -> str s) + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x) + if fatal then CErrors.error x else + if warn then warn_invalid_identifier x in Option.iter iter (Unicode.ident_refutation x) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6c664f791..1ae89347a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let cuniv = conv_table_key infos fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with NotConvertible -> + with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9812c45f7..8a2b2469d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,7 +36,7 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = - { (* Might raise NotConvertible *) + { (* Might raise NotConvertible or UnivInconsistency *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -56,9 +56,12 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(** These two never raise UnivInconsistency, inferred_universes + just gathers the constraints. *) val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare +(** These two functions can only raise NotConvertible *) val conv : constr extended_conversion_function val conv_leq : types extended_conversion_function @@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function +(** Depending on the universe state functions, this might raise + [UniverseInconsistency] in addition to [NotConvertible] (for better error + messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e2712615b..4884d0deb 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -638,19 +638,6 @@ let check_smaller g strict u v = type 'a check_function = universes -> 'a -> 'a -> bool -let check_equal_expr g x y = - x == y || (let (u, n) = x and (v, m) = y in - Int.equal n m && check_equal g u v) - -let check_eq_univs g l1 l2 = - let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in - Universe.for_all (fun x1 -> exists x1 l2) l1 - && Universe.for_all (fun x2 -> exists x2 l1) l2 - -let check_eq g u v = - Universe.equal u v || check_eq_univs g u v - let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with @@ -669,7 +656,13 @@ let real_check_leq g u v = let check_leq g u v = Universe.equal u v || is_type0m_univ u || - check_eq_univs g u v || real_check_leq g u v + real_check_leq g u v + +let check_eq_univs g l1 l2 = + real_check_leq g l1 l2 && real_check_leq g l2 l1 + +let check_eq g u v = + Universe.equal u v || check_eq_univs g u v (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 9224ec48d..09f884ecd 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -468,15 +468,32 @@ struct else if Level.is_prop u then hcons (Level.set,n+k) else hcons (u,n+k) - + + type super_result = + SuperSame of bool + (* The level expressions are in cumulativity relation. boolean + indicates if left is smaller than right? *) + | SuperDiff of int + (* The level expressions are unrelated, the comparison result + is canonical *) + + (** [super u v] compares two level expressions, + returning [SuperSame] if they refer to the same level at potentially different + increments or [SuperDiff] if they are different. The booleans indicate if the + left expression is "smaller" than the right one in both cases. *) let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in - if Int.equal cmp 0 then - if n < n' then Inl true - else Inl false - else if is_prop x then Inl true - else if is_prop y then Inl false - else Inr cmp + if Int.equal cmp 0 then SuperSame (n < n') + else + match x, y with + | (l,0), (l',0) -> + let open RawLevel in + (match Level.data l, Level.data l' with + | Prop, Prop -> SuperSame false + | Prop, _ -> SuperSame true + | _, Prop -> SuperSame false + | _, _ -> SuperDiff cmp) + | _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -598,24 +615,26 @@ struct | Nil, _ -> l2 | _, Nil -> l1 | Cons (h1, _, t1), Cons (h2, _, t2) -> - (match Expr.super h1 h2 with - | Inl true (* h1 < h2 *) -> merge_univs t1 l2 - | Inl false -> merge_univs l1 t2 - | Inr c -> - if c <= 0 (* h1 < h2 is name order *) - then cons h1 (merge_univs t1 l2) - else cons h2 (merge_univs l1 t2)) + let open Expr in + (match super h1 h2 with + | SuperSame true (* h1 < h2 *) -> merge_univs t1 l2 + | SuperSame false -> merge_univs l1 t2 + | SuperDiff c -> + if c <= 0 (* h1 < h2 is name order *) + then cons h1 (merge_univs t1 l2) + else cons h2 (merge_univs l1 t2)) let sort u = let rec aux a l = match l with | Cons (b, _, l') -> - (match Expr.super a b with - | Inl false -> aux a l' - | Inl true -> l - | Inr c -> - if c <= 0 then cons a l - else cons b (aux a l')) + let open Expr in + (match super a b with + | SuperSame false -> aux a l' + | SuperSame true -> l + | SuperDiff c -> + if c <= 0 then cons a l + else cons b (aux a l')) | Nil -> cons a l in fold (fun a acc -> aux a acc) u nil diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 03ef3e5c9..a37cf306e 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -50,11 +50,17 @@ let eval_uconstrs ist cs = } in List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs -let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ()) +let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using Printer.pr_closed_glob ARGUMENT EXTEND auto_using TYPED AS uconstr_list PRINTED BY pr_auto_using + RAW_TYPED AS uconstr_list + RAW_PRINTED BY pr_auto_using_raw + GLOB_TYPED AS uconstr_list + GLOB_PRINTED BY pr_auto_using_glob | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] | [ ] -> [ [] ] END @@ -171,18 +177,32 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ] END -let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global +let glob_hints_path_atom ist = Hints.glob_hints_path_atom ARGUMENT EXTEND hints_path_atom PRINTED BY pr_hints_path_atom -| [ ne_global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ] + + GLOBALIZED BY glob_hints_path_atom + + RAW_PRINTED BY pr_pre_hints_path_atom + GLOB_PRINTED BY pr_hints_path_atom +| [ ne_global_list(g) ] -> [ Hints.PathHints g ] | [ "_" ] -> [ Hints.PathAny ] END let pr_hints_path prc prx pry c = Hints.pp_hints_path c - +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let glob_hints_path ist = Hints.glob_hints_path + ARGUMENT EXTEND hints_path - PRINTED BY pr_hints_path +PRINTED BY pr_hints_path + +GLOBALIZED BY glob_hints_path +RAW_PRINTED BY pr_pre_hints_path +GLOB_PRINTED BY pr_hints_path + | [ "(" hints_path(p) ")" ] -> [ p ] | [ hints_path(p) "*" ] -> [ Hints.PathStar p ] | [ "emp" ] -> [ Hints.PathEmpty ] @@ -192,8 +212,6 @@ ARGUMENT EXTEND hints_path | [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ] END -let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases - ARGUMENT EXTEND opthints TYPED AS preident_list_opt PRINTED BY pr_hintbases @@ -203,7 +221,7 @@ END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - let entry = Hints.HintsCutEntry p in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ())) (match dbnames with None -> ["core"] | Some l -> l) entry ] END diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml index 85740f187..b1a6fa63d 100644 --- a/ltac/pptactic.ml +++ b/ltac/pptactic.ml @@ -136,7 +136,7 @@ module Make | ConstrContext ((_,id),c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ - str "[" ++ prlc c ++ str "]") + str "[ " ++ prlc c ++ str " ]") | ConstrTypeOf c -> hov 1 (keyword "type of" ++ spc() ++ prc c) | ConstrTerm c when test c -> @@ -497,7 +497,8 @@ module Make | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,()) in pr_in - (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) + (prlist_with_sep (fun () -> str",") + (fun id -> spc () ++ pr_hyp_location pr_id id) l ++ pr_occs) let pr_orient b = if b then mt () else str "<- " @@ -542,9 +543,9 @@ module Make | Subterm (b,None,a) -> (** ppedrot: we don't make difference between [appcontext] and [context] anymore, and the interpretation is governed by a flag instead. *) - keyword "context" ++ str" [" ++ pr_pat a ++ str "]" + keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" | Subterm (b,Some id,a) -> - keyword "context" ++ spc () ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]" + keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function | Hyp (nal,mp) -> @@ -1083,7 +1084,7 @@ module Make | TacNumgoals -> keyword "numgoals" | (TacCall _|Tacexp _ | TacGeneric _) as a -> - str "ltac:(" ++ pr_tac (1,Any) (TacArg (Loc.ghost,a)) ++ str ")" + hov 0 (keyword "ltac:" ++ surround (pr_tac ltop (TacArg (Loc.ghost,a)))) in pr_tac diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 003fb6789..02a720d2d 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -419,8 +419,8 @@ let rec comment loc bp = parser bp2 | [< '')' >] -> push_string "*)"; loc | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc | [< ''"'; s >] -> - let loc = fst (string loc ~comm_level:(Some 0) bp2 0 s) - in + let loc, len = string loc ~comm_level:(Some 0) bp2 0 s in + push_string "\""; push_string (get_buff len); push_string "\""; comment loc bp s | [< _ = Stream.empty >] ep -> let loc = set_loc_pos loc bp ep in diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 344a04a6a..260e86ad6 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -116,9 +116,9 @@ open Pp open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_reference l -let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l -let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l +let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference +let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) +let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global let warn_deprecated_syntax = CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a688fc065..0d4be72d9 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -435,7 +435,7 @@ let proj_nparams c = try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 let isFixed c = match kind_of_term c with - | Var _ | Ind _ | Construct _ | Const _ -> true + | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true | _ -> false let isRigid c = match kind_of_term c with @@ -487,6 +487,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let np = proj_nparams p in if np = 0 || np > List.length a then KpatConst, f, a else let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2 + | Proj (p,arg) -> KpatProj (Projection.constant p), f, a | Var _ | Ind _ | Construct _ -> KpatFixed, f, a | Evar (k, _) -> if Evd.mem sigma0 k then KpatEvar k, f, a else @@ -567,6 +568,10 @@ let filter_upat i0 f n u fpats = if np < na then fpats else let () = if !i0 < np then i0 := n in (u, np) :: fpats +let eq_prim_proj c t = match kind_of_term t with + | Proj(p,_) -> Constant.equal (Projection.constant p) c + | _ -> false + let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else @@ -577,7 +582,7 @@ let filter_upat_FO i0 f n u fpats = | KpatLet -> isLetIn f | KpatLam -> isLambda f | KpatRigid -> isRigid f - | KpatProj pc -> Term.eq_constr f (mkConst pc) + | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f | KpatFlex -> i0 := n; true in if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d5b125135..468446982 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1934,14 +1934,22 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = *) let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = + let refresh_tycon sigma t = + (** If we put the typing constraint in the term, it has to be + refreshed to preserve the invariant that no algebraic universe + can appear in the term. *) + refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true) + env sigma t + in let preds = match pred, tycon with (* No return clause *) | None, Some t when not (noccur_with_meta 0 max_int t) -> (* If the tycon is not closed w.r.t real variables, we try *) (* two different strategies *) - (* First strategy: we abstract the tycon wrt to the dependencies *) - let p1 = + (* First strategy: we abstract the tycon wrt to the dependencies *) + let sigma, t = refresh_tycon sigma t in + let p1 = prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in (* Second strategy: we build an "inversion" predicate *) let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in @@ -1952,7 +1960,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = (* No dependent type constraint, or no constraints at all: *) (* we use two strategies *) let sigma,t = match tycon with - | Some t -> sigma,t + | Some t -> refresh_tycon sigma t | None -> let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((t, _), sigma, _) = diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 6bc61f6dd..d8fad1687 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -114,10 +114,11 @@ val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment val prepare_predicate : Loc.t -> (Evarutil.type_constraint -> - Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) -> + Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) -> Environ.env -> Evd.evar_map -> (Term.types * tomatch_type) list -> Context.Rel.t list -> Constr.constr option -> - 'a option -> (Evd.evar_map * Names.name list * Term.constr) list + glob_constr option -> + (Evd.evar_map * Names.name list * Term.constr) list diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 1ae5532be..92662f07d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,33 +42,39 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -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 ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = let evdref = ref evd in let modified = ref false in - 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 && refresh_level evd s) -> + (* direction: true for fresh universes lower than the existing ones *) + let refresh_sort status ~direction s = let s' = evd_comb0 (new_sort_variable status) evdref in let evd = - if dir then set_leq_sort env !evdref s' s + if direction then set_leq_sort env !evdref s' s else set_leq_sort env !evdref s s' in - modified := true; evdref := evd; mkSort s' - | Sort (Prop Pos as s) when refreshset && not dir -> - let s' = evd_comb0 (new_sort_variable status) evdref in - let evd = set_leq_sort env !evdref s s' in - modified := true; evdref := evd; mkSort s' + modified := true; evdref := evd; mkSort s' + in + let rec refresh ~onlyalg status ~direction t = + match kind_of_term t with + | Sort (Type u as s) -> + (match Univ.universe_level u with + | None -> refresh_sort status ~direction s + | Some l -> + (match Evd.universe_rigidity evd l with + | UnivRigid -> + if not onlyalg then refresh_sort status ~direction s + else t + | UnivFlexible alg -> + if onlyalg && alg then + (evdref := Evd.make_flexible_variable !evdref false l; t) + else t)) + | Sort (Prop Pos as s) when refreshset && not direction -> + (* Cannot make a universe "lower" than "Set", + only refreshing when we want higher universes. *) + refresh_sort status ~direction s | Prod (na,u,v) -> - mkProd (na,u,refresh status dir v) + mkProd (na, u, refresh ~onlyalg status ~direction v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = @@ -81,7 +87,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) Array.iter (refresh_term_evars onevars false) args | Evar (ev, a) when onevars -> let evi = Evd.find !evdref ev in - let ty' = refresh univ_flexible true evi.evar_concl in + let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -101,9 +107,11 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) in let t' = if isArity t then - (match pbty with - | None -> t - | Some dir -> refresh status dir t) + match pbty with + | None -> + (* No cumulativity needed, but we still need to refresh the algebraics *) + refresh ~onlyalg:true univ_flexible ~direction:false t + | Some direction -> refresh ~onlyalg status ~direction t else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a85e493ea..1fdbbb412 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1266,7 +1266,7 @@ let sigma_compare_sorts env pb s0 s1 sigma = match pb with | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1 | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1 - + let sigma_compare_instances ~flex i0 i1 sigma = try Evd.set_eq_instances ~flex sigma i0 i1 with Evd.UniversesDiffer diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5d1964a0a..ff72be90c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -911,7 +911,7 @@ module Make | VernacContext l -> return ( hov 1 ( - keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) + keyword "Context" ++ pr_and_type_binders_arg l) ) | VernacDeclareInstances insts -> @@ -1013,7 +1013,10 @@ module Make (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++ pr_syntax_modifiers - (match compat with None -> [] | Some v -> [SetCompatVersion v])) + (match compat with + | None -> [] + | Some Flags.Current -> [SetOnlyParsing] + | Some v -> [SetCompatVersion v])) ) | VernacDeclareImplicits (q,[]) -> return ( @@ -1055,7 +1058,7 @@ module Make in print_arguments nargs args ++ if not (List.is_empty more_implicits) then - str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits + prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ (if not (List.is_empty mods) then str" : " else str"") ++ prlist_with_sep (fun () -> str", " ++ spc()) (function @@ -1126,7 +1129,7 @@ module Make | VernacSetAppendOption (na,v) -> return ( hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++ - spc() ++ keyword "Append" ++ spc() ++ str v) + spc() ++ keyword "Append" ++ spc() ++ qs v) ) | VernacAddOption (na,l) -> return ( diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9fc3232fd..0abfd342d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1124,12 +1124,12 @@ module Search = struct else tclDISPATCH (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) in - let finish sigma = + let finish nestedshelf sigma = let filter ev = try let evi = Evd.find_undefined sigma ev in if info.search_only_classes then - Some (ev, is_class_type sigma (Evd.evar_concl evi)) + Some (ev, not (is_class_type sigma (Evd.evar_concl evi))) else Some (ev, true) with Not_found -> None in @@ -1147,9 +1147,9 @@ module Search = struct begin (* Some existentials produced by the original tactic were not solved in the subgoals, turn them into subgoals now. *) - let shelved, goals = List.split_when (fun (ev, s) -> s) remaining in - let shelved = List.map fst shelved and goals = List.map fst goals in - if !typeclasses_debug > 1 && not (List.is_empty goals) then + let shelved, goals = List.partition (fun (ev, s) -> s) remaining in + let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in + if !typeclasses_debug > 1 && not (List.is_empty shelved && List.is_empty goals) then Feedback.msg_debug (str"Adding shelved subgoals to the search: " ++ prlist_with_sep spc (pr_ev sigma) goals ++ @@ -1162,7 +1162,8 @@ module Search = struct with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS goals) >>= fun s -> result s i (Some (Option.default 0 k + j))) end - in res <*> tclEVARMAP >>= finish + in with_shelf res >>= fun (sh, ()) -> + tclEVARMAP >>= finish sh in if path_matches derivs [] then aux e tl else diff --git a/tactics/hints.ml b/tactics/hints.ml index edb4d3d6a..59d015fa2 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -104,18 +104,25 @@ type 'a hint_ast = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Genarg.glob_generic_argument (* Hint Extern *) -type hints_path_atom = - | PathHints of global_reference list + +type 'a hints_path_atom_gen = + | PathHints of 'a list + (* For forward hints, their names is the list of projections *) | PathAny -type hints_path = - | PathAtom of hints_path_atom - | PathStar of hints_path - | PathSeq of hints_path * hints_path - | PathOr of hints_path * hints_path +type hints_path_atom = global_reference hints_path_atom_gen + +type 'a hints_path_gen = + | PathAtom of 'a hints_path_atom_gen + | PathStar of 'a hints_path_gen + | PathSeq of 'a hints_path_gen * 'a hints_path_gen + | PathOr of 'a hints_path_gen * 'a hints_path_gen | PathEmpty | PathEpsilon +type pre_hints_path = Libnames.reference hints_path_gen +type hints_path = global_reference hints_path_gen + type hint_term = | IsGlobRef of global_reference | IsConstr of constr * Univ.universe_context_set @@ -397,21 +404,40 @@ let rec normalize_path h = let path_derivate hp hint = normalize_path (path_derivate hp hint) -let pp_hints_path_atom a = +let pp_hints_path_atom prg a = match a with | PathAny -> str"_" - | PathHints grs -> pr_sequence pr_global grs - -let rec pp_hints_path = function - | PathAtom pa -> pp_hints_path_atom pa - | PathStar (PathAtom PathAny) -> str"_*" - | PathStar p -> str "(" ++ pp_hints_path p ++ str")*" - | PathSeq (p, p') -> pp_hints_path p ++ spc () ++ pp_hints_path p' - | PathOr (p, p') -> - str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ cut () ++ spc () ++ - pp_hints_path p' ++ str ")" + | PathHints grs -> pr_sequence prg grs + +let pp_hints_path_gen prg = + let rec aux = function + | PathAtom pa -> pp_hints_path_atom prg pa + | PathStar (PathAtom PathAny) -> str"_*" + | PathStar p -> str "(" ++ aux p ++ str")*" + | PathSeq (p, p') -> aux p ++ spc () ++ aux p' + | PathOr (p, p') -> + str "(" ++ aux p ++ spc () ++ str"|" ++ cut () ++ spc () ++ + aux p' ++ str ")" | PathEmpty -> str"emp" | PathEpsilon -> str"eps" + in aux + +let pp_hints_path = pp_hints_path_gen pr_global + +let glob_hints_path_atom p = + match p with + | PathHints g -> PathHints (List.map Nametab.global g) + | PathAny -> PathAny + +let glob_hints_path = + let rec aux = function + | PathAtom pa -> PathAtom (glob_hints_path_atom pa) + | PathStar p -> PathStar (aux p) + | PathSeq (p, p') -> PathSeq (aux p, aux p') + | PathOr (p, p') -> PathOr (aux p, aux p') + | PathEmpty -> PathEmpty + | PathEpsilon -> PathEpsilon + in aux let subst_path_atom subst p = match p with diff --git a/tactics/hints.mli b/tactics/hints.mli index 73cafbefd..05d41adfe 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -45,11 +45,12 @@ type 'a hint_ast = type hint type raw_hint = constr * types * Univ.universe_context_set -type hints_path_atom = - | PathHints of global_reference list +type 'a hints_path_atom_gen = + | PathHints of 'a list (* For forward hints, their names is the list of projections *) | PathAny +type hints_path_atom = global_reference hints_path_atom_gen type hint_db_name = string type 'a with_metadata = private { @@ -70,20 +71,28 @@ type search_entry type hint_entry -type hints_path = - | PathAtom of hints_path_atom - | PathStar of hints_path - | PathSeq of hints_path * hints_path - | PathOr of hints_path * hints_path +type 'a hints_path_gen = + | PathAtom of 'a hints_path_atom_gen + | PathStar of 'a hints_path_gen + | PathSeq of 'a hints_path_gen * 'a hints_path_gen + | PathOr of 'a hints_path_gen * 'a hints_path_gen | PathEmpty | PathEpsilon +type pre_hints_path = Libnames.reference hints_path_gen +type hints_path = global_reference hints_path_gen + 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_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds +val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds val pp_hints_path : hints_path -> Pp.std_ppcmds val pp_hint_mode : hint_mode -> Pp.std_ppcmds +val glob_hints_path_atom : + Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen +val glob_hints_path : + Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen module Hint_db : sig diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v new file mode 100644 index 000000000..261092ee6 --- /dev/null +++ b/test-suite/bugs/closed/5180.v @@ -0,0 +1,64 @@ +Universes a b c ω ω'. +Definition Typeω := Type@{ω}. +Definition Type2 : Typeω := Type@{c}. +Definition Type1 : Type2 := Type@{b}. +Definition Type0 : Type1 := Type@{a}. + +Set Universe Polymorphism. +Set Printing Universes. + +Definition Typei' (n : nat) + := match n return Type@{ω'} with + | 0 => Type0 + | 1 => Type1 + | 2 => Type2 + | _ => Typeω + end. +Definition TypeOfTypei' {n} (x : Typei' n) : Type@{ω'} + := match n return Typei' n -> Type@{ω'} with + | 0 | 1 | 2 | _ => fun x => x + end x. +Definition Typei (n : nat) : Typei' (S n) + := match n return Typei' (S n) with + | 0 => Type0 + | 1 => Type1 + | _ => Type2 + end. +Definition TypeOfTypei {n} (x : TypeOfTypei' (Typei n)) : Type@{ω'} + := match n return TypeOfTypei' (Typei n) -> Type@{ω'} with + | 0 | 1 | _ => fun x => x + end x. +Check Typei 0 : Typei 1. +Check Typei 1 : Typei 2. + +Definition lift' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) + := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with + | 0 | 1 | 2 | _ => fun x => (x : Type) + end. +Definition lift'' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) + := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with + | 0 | 1 | 2 | _ => fun x => x + end. (* The command has indeed failed with message: +In environment +n : nat +x : TypeOfTypei' (Typei 0) +The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type + "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because a < b). + *) +Check (fun x : TypeOfTypei' (Typei 0) => TypeOfTypei' (Typei 1)). + +Definition lift''' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)). + refine match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with + | 0 | 1 | 2 | _ => fun x => _ + end. + exact x. + Undo. + (* The command has indeed failed with message: +In environment +n : nat +x : TypeOfTypei' (Typei 0) +The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type + "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because a < b). + *) + all:compute in *. + all:exact x.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5188.v b/test-suite/bugs/closed/5188.v new file mode 100644 index 000000000..e29ebfb4e --- /dev/null +++ b/test-suite/bugs/closed/5188.v @@ -0,0 +1,5 @@ +Set Printing All. +Axiom relation : forall (T : Type), Set. +Axiom T : forall A (R : relation A), Set. +Set Printing Universes. +Parameter (A:_) (R:_) (e:@T A R). diff --git a/test-suite/bugs/closed/5208.v b/test-suite/bugs/closed/5208.v new file mode 100644 index 000000000..b7a684a27 --- /dev/null +++ b/test-suite/bugs/closed/5208.v @@ -0,0 +1,222 @@ +Require Import Program. + +Require Import Coq.Strings.String. +Require Import Coq.Strings.Ascii. +Require Import Coq.Numbers.BinNums. + +Set Implicit Arguments. +Set Strict Implicit. +Set Universe Polymorphism. +Set Printing Universes. + +Local Open Scope positive. + +Definition field : Type := positive. + +Section poly. + Universe U. + + Inductive fields : Type := + | pm_Leaf : fields + | pm_Branch : fields -> option Type@{U} -> fields -> fields. + + Definition fields_left (f : fields) : fields := + match f with + | pm_Leaf => pm_Leaf + | pm_Branch l _ _ => l + end. + + Definition fields_right (f : fields) : fields := + match f with + | pm_Leaf => pm_Leaf + | pm_Branch _ _ r => r + end. + + Definition fields_here (f : fields) : option Type@{U} := + match f with + | pm_Leaf => None + | pm_Branch _ s _ => s + end. + + Fixpoint fields_get (p : field) (m : fields) {struct p} : option Type@{U} := + match p with + | xH => match m with + | pm_Leaf => None + | pm_Branch _ x _ => x + end + | xO p' => fields_get p' match m with + | pm_Leaf => pm_Leaf + | pm_Branch L _ _ => L + end + | xI p' => fields_get p' match m with + | pm_Leaf => pm_Leaf + | pm_Branch _ _ R => R + end + end. + + Definition fields_leaf : fields := pm_Leaf. + + Inductive member (val : Type@{U}) : fields -> Type := + | pmm_H : forall L R, member val (pm_Branch L (Some val) R) + | pmm_L : forall (V : option Type@{U}) L R, member val L -> member val (pm_Branch L V R) + | pmm_R : forall (V : option Type@{U}) L R, member val R -> member val (pm_Branch L V R). + Arguments pmm_H {_ _ _}. + Arguments pmm_L {_ _ _ _} _. + Arguments pmm_R {_ _ _ _} _. + + Fixpoint get_member (val : Type@{U}) p {struct p} + : forall m, fields_get p m = @Some Type@{U} val -> member val m := + match p as p return forall m, fields_get p m = @Some Type@{U} val -> member@{U} val m with + | xH => fun m => + match m as m return fields_get xH m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : None = @Some Type@{U} _ => + match pf in _ = Z return match Z with + | Some _ => _ + | None => unit + end + with + | eq_refl => tt + end + | pm_Branch _ None _ => fun pf : None = @Some Type@{U} _ => + match pf in _ = Z return match Z with + | Some _ => _ + | None => unit + end + with + | eq_refl => tt + end + | pm_Branch _ (Some x) _ => fun pf : @Some Type@{U} x = @Some Type@{U} val => + match eq_sym pf in _ = Z return member@{U} val (pm_Branch _ Z _) with + | eq_refl => pmm_H + end + end + | xO p' => fun m => + match m as m return fields_get (xO p') m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val => + @get_member _ p' pm_Leaf pf + | pm_Branch l _ _ => fun pf : fields_get p' l = @Some Type@{U} val => + @pmm_L _ _ _ _ (@get_member _ p' l pf) + end + | xI p' => fun m => + match m as m return fields_get (xI p') m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val => + @get_member _ p' pm_Leaf pf + | pm_Branch l _ r => fun pf : fields_get p' r = @Some Type@{U} val => + @pmm_R _ _ _ _ (@get_member _ p' r pf) + end + end. + + Inductive record : fields -> Type := + | pr_Leaf : record pm_Leaf + | pr_Branch : forall L R (V : option Type@{U}), + record L -> + match V return Type@{U} with + | None => unit + | Some t => t + end -> + record R -> + record (pm_Branch L V R). + + + Definition record_left {L} {V : option Type@{U}} {R} + (r : record (pm_Branch L V R)) : record L := + match r in record z + return match z with + | pm_Branch L _ _ => record L + | _ => unit + end + with + | pr_Branch _ l _ _ => l + | pr_Leaf => tt + end. +Set Printing All. + Definition record_at {L} {V : option Type@{U}} {R} (r : record (pm_Branch L V R)) + : match V return Type@{U} with + | None => unit + | Some t => t + end := + match r in record z + return match z (* return ?X *) with + | pm_Branch _ V _ => match V return Type@{U} with + | None => unit + | Some t => t + end + | _ => unit + end + with + | pr_Branch _ _ v _ => v + | pr_Leaf => tt + end. + + Definition record_here {L : fields} (v : Type@{U}) {R : fields} + (r : record (pm_Branch L (@Some Type@{U} v) R)) : v := + match r in record z + return match z return Type@{U} with + | pm_Branch _ (Some v) _ => v + | _ => unit + end + with + | pr_Branch _ _ v _ => v + | pr_Leaf => tt + end. + + Definition record_right {L V R} (r : record (pm_Branch L V R)) : record R := + match r in record z return match z with + | pm_Branch _ _ R => record R + | _ => unit + end + with + | pr_Branch _ _ _ r => r + | pr_Leaf => tt + end. + + Fixpoint record_get {val : Type@{U}} {pm : fields} (m : member val pm) : record pm -> val := + match m in member _ pm return record pm -> val with + | pmm_H => fun r => record_here r + | pmm_L m' => fun r => record_get m' (record_left r) + | pmm_R m' => fun r => record_get m' (record_right r) + end. + + Fixpoint record_set {val : Type@{U}} {pm : fields} (m : member val pm) (x : val) {struct m} + : record pm -> record pm := + match m in member _ pm return record pm -> record pm with + | pmm_H => fun r => + pr_Branch (Some _) + (record_left r) + x + (record_right r) + | pmm_L m' => fun r => + pr_Branch _ + (record_set m' x (record_left r)) + (record_at r) + (record_right r) + | pmm_R m' => fun r => + pr_Branch _ (record_left r) + (record_at r) + (record_set m' x (record_right r)) + end. +End poly. +Axiom cheat : forall {A}, A. +Lemma record_get_record_set_different: + forall (T: Type) (vars: fields) + (pmr pmw: member T vars) + (diff: pmr <> pmw) + (r: record vars) (val: T), + record_get pmr (record_set pmw val r) = record_get pmr r. +Proof. + intros. + revert pmr diff r val. + induction pmw; simpl; intros. + - dependent destruction pmr. + + congruence. + + auto. + + auto. + - dependent destruction pmr. + + auto. + + simpl. apply IHpmw. congruence. + + auto. + - dependent destruction pmr. + + auto. + + auto. + + simpl. apply IHpmw. congruence. +Qed. diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out index 9949658c4..239edd1da 100644 --- a/test-suite/output/Tactics.out +++ b/test-suite/output/Tactics.out @@ -1,4 +1,4 @@ Ltac f H := split; [ a H | e H ] Ltac g := match goal with - | |- context [if ?X then _ else _] => case X + | |- context [ if ?X then _ else _ ] => case X end diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 9661b3bfa..f746def5c 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A. hit the Inductiveops.get_arity bug mentioned above (see #3491) *) Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. + + +Module TemplateProp. + + (** Check lowering of a template universe polymorphic inductive to Prop *) + + Inductive Foo (A : Type) : Type := foo : A -> Foo A. + + Check Foo True : Prop. + +End TemplateProp. + +Module PolyNoLowerProp. + + (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *) + + Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A. + + Fail Check Foo True : Prop. + +End PolyNoLowerProp. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index f62427ef4..6b1f0315b 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -98,7 +98,7 @@ Goal exists R, @Refl nat R. solve [typeclasses eauto with foo]. Qed. -(* Set Typeclasses Compatibility "8.5". *) +Set Typeclasses Compatibility "8.5". Parameter f : nat -> Prop. Parameter g : nat -> nat -> Prop. Parameter h : nat -> nat -> nat -> Prop. @@ -108,8 +108,7 @@ Axiom c : forall x y z, h x y z -> f x -> f y. Hint Resolve a b c : mybase. Goal forall x y z, h x y z -> f x -> f y. intros. - Set Typeclasses Debug. - typeclasses eauto with mybase. + Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *) Unshelve. Abort. End bt. @@ -138,7 +137,8 @@ Notation "'return' t" := (unit t). Class A `(e: T) := { a := True }. Class B `(e_: T) := { e := e_; sg_ass :> A e }. -Set Typeclasses Debug. +(* Set Typeclasses Debug. *) +(* Set Typeclasses Debug Verbosity 2. *) Goal forall `{B T}, Prop. intros. apply a. diff --git a/toplevel/command.ml b/toplevel/command.ml index a8cd52ae8..049f58aa2 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -263,10 +263,7 @@ match local with let interp_assumption evdref env impls bl c = let c = prod_constr_expr c bl in - let ty, impls = interp_type_evars_impls env evdref ~impls c in - let evd, nf = nf_evars_and_universes !evdref in - let ctx = Evd.universe_context_set evd in - ((nf ty, ctx), impls) + interp_type_evars_impls env evdref ~impls c let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl = let refs, status, _ = @@ -291,26 +288,32 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = l [] else l in + (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) let _,l = List.fold_map (fun (env,ienv) (is_coe,(idl,c)) -> - let (t,ctx),imps = interp_assumption evdref env ienv [] c in + let t,imps = interp_assumption evdref env ienv [] c in let env = push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in let ienv = List.fold_right (fun (_,id) ienv -> let impls = compute_internalization_data env Variable t imps in Id.Map.add id impls ienv) idl ienv in - ((env,ienv),((is_coe,idl),t,(ctx,imps)))) + ((env,ienv),((is_coe,idl),t,imps))) (env,empty_internalization_env) l in let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in + (* The universe constraints come from the whole telescope. *) + let evd = Evd.nf_constraints evd in + let ctx = Evd.universe_context_set evd in let l = List.map (on_pi2 (nf_evar evd)) l in - snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> + pi2 (List.fold_left (fun (subst,status,ctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in let subst' = List.map2 (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs in - (subst'@subst, status' && status)) ([],true) l) + (subst'@subst, status' && status, + (* The universe constraints are declared with the first declaration only. *) + Univ.ContextSet.empty)) ([],true,ctx) l) let do_assumptions_bound_univs coe kind nl id pl c = let env = Global.env () in @@ -539,11 +542,9 @@ let inductive_levels env evdref poly arities inds = in let duu = Sorts.univ_of_sort du in let evd = - if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then - if is_flexible_sort evd duu then - if Evd.check_leq evd Univ.type0_univ duu then - evd - else Evd.set_eq_sort env evd (Prop Null) du + if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then + if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then + Evd.set_eq_sort env evd (Prop Null) du else evd else Evd.set_eq_sort env evd (Type cu) du in |