From 253493355a71c0673b0c10b06e7eb9f0fd0242a9 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 17 Nov 2016 16:01:29 +0100 Subject: Add missing label. Fixes broken ref. --- doc/refman/Classes.tex | 1 + 1 file changed, 1 insertion(+) 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: -- cgit v1.2.3 From 27190db7f119bc9b50150be6dff889986c747e38 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 15:05:26 -0500 Subject: (v8.6) Add example in dev/doc/changes involving Tacmach.project --- dev/doc/changes.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f9..e92667469 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -244,6 +244,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. -- cgit v1.2.3 From 8572140c30629cfcc6b7e68d450487c64922a6b9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 16:01:34 -0500 Subject: (v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes --- dev/doc/changes.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f9..12c0163b9 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -218,6 +218,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. -- cgit v1.2.3 From 59dee24e5dfe3dfe20c2a4a2843192d797c89155 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 17:03:22 -0500 Subject: (v8.6) Update dev/doc/changes with things about mem_named_context --- dev/doc/changes.txt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f9..156f38c45 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -256,7 +256,10 @@ 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` +- `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 ** -- cgit v1.2.3 From bfa2ac5fc5578d9bcf2ea1183deeaa6329c29b9b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 21 Nov 2016 17:11:45 -0500 Subject: (v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes --- dev/doc/changes.txt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d052468f9..134a6a25e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -256,7 +256,8 @@ 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)` ** Search API ** -- cgit v1.2.3 From 17559d528cf7ff92a089d1b966c500424ba45099 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Nov 2016 13:24:39 +0100 Subject: Slightly more efficient [Univ.super] implem --- kernel/univ.ml | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/kernel/univ.ml b/kernel/univ.ml index 9224ec48d..c863fac0e 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -471,12 +471,17 @@ struct 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 Inl (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 -> Inl false + | Prop, _ -> Inl true + | _, Prop -> Inl false + | _, _ -> Inr cmp) + | _, _ -> Inr cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v -- cgit v1.2.3 From 25c82d55497db43bf2cd131f10d2ef366758bbe1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 18 Nov 2016 13:25:05 +0100 Subject: Fix UGraph.check_eq! Universes are kept in normal form w.r.t. equality but not the <= relation, so the previous check worked almost always but was actually too strict! In cases like (max(Set,u) = u) when u is declared >= Set it was failing to find an equality. Applying the KISS principle: u = v <-> u <= v /\ v <= u. Fix invariant breakage that triggered the discovery of the check_eq bug as well. No algebraic universes should appear in a term position (on the left of a colon in a typing judgment), this was not the case when an algebraic universe instantiated an evar that appeared in the term. We force their universe variable status to change in refresh_universes to avoid this. Fix ind sort inference: Use syntactic universe equality for inductive sort inference instead of check_leq (which now correctly takes constraints into account) and simplify code --- engine/evd.ml | 7 ++ engine/evd.mli | 3 +- kernel/uGraph.ml | 21 ++-- pretyping/cases.ml | 11 +- pretyping/cases.mli | 5 +- pretyping/evarsolve.ml | 41 ++++---- test-suite/bugs/closed/5208.v | 222 +++++++++++++++++++++++++++++++++++++++++ test-suite/success/Inductive.v | 21 ++++ toplevel/command.ml | 8 +- 9 files changed, 294 insertions(+), 45 deletions(-) create mode 100644 test-suite/bugs/closed/5208.v diff --git a/engine/evd.ml b/engine/evd.ml index aa91fc522..a6b6f742b 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 b47b389d1..89dcd92ce 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -514,7 +514,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/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/pretyping/cases.ml b/pretyping/cases.ml index aa24733d9..27c1dd031 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1934,14 +1934,19 @@ 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 = + 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 +1957,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 ba566f374..ee4148de6 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 f0aa9b564..02e10d7fc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,33 +42,34 @@ 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) -> + let refresh_sort status dir s = let s' = evd_comb0 (new_sort_variable status) evdref in let evd = if dir then set_leq_sort env !evdref s' s else 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 dir t = + match kind_of_term t with + | Sort (Type u as s) -> + (match Univ.universe_level u with + | None -> refresh_sort status dir s + | Some l -> + (match Evd.universe_rigidity evd l with + | UnivRigid -> if not onlyalg then refresh_sort status dir 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 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' + refresh_sort status dir s | Prod (na,u,v) -> - mkProd (na,u,refresh status dir v) + mkProd (na, u, refresh onlyalg status dir v) | _ -> t (** Refresh the types of evars under template polymorphic references *) and refresh_term_evars onevars top t = @@ -81,7 +82,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 true evi.evar_concl in if !modified then evdref := Evd.add !evdref ev {evi with evar_concl = ty'} else () @@ -101,9 +102,9 @@ 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 -> refresh true univ_flexible false t + | Some dir -> refresh onlyalg status dir t else (refresh_term_evars false true t; t) in if !modified then !evdref, t' else !evdref, t 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/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/toplevel/command.ml b/toplevel/command.ml index 7ffe680e5..ed3eac51b 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -537,11 +537,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 -- cgit v1.2.3 From d06211803146dec998b414d215d4d93190e2001f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Nov 2016 18:36:10 +0100 Subject: Univs: fix bug #5180 In the kernel's generic conversion, backtrack on UniverseInconsistency for the unfolding heuristic (single backtracking point in reduction). This exception can be raised in the univ_compare structure to produce better error messages when the generic conversion function is called from higher level code in reductionops.ml, which itself is called during unification in evarconv.ml. Inside the kernel, the infer and check variants of conversion never raise UniverseInconsistency though, so this does not change the behavior of the kernel. --- kernel/reduction.ml | 2 +- kernel/reduction.mli | 8 +++++- pretyping/reductionops.ml | 2 +- test-suite/bugs/closed/5180.v | 64 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 73 insertions(+), 3 deletions(-) create mode 100644 test-suite/bugs/closed/5180.v 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/pretyping/reductionops.ml b/pretyping/reductionops.ml index 332d4e0b2..297f0a1a8 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1262,7 +1262,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/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 -- cgit v1.2.3 From 1099b748bb080d449037fbd06199c012fa3ce387 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 30 Nov 2016 16:23:38 +0100 Subject: Fix bug #5232: proper globalization of hints paths --- ltac/g_auto.ml4 | 24 ++++++++++++++++----- tactics/hints.ml | 62 +++++++++++++++++++++++++++++++++++++++---------------- tactics/hints.mli | 25 +++++++++++++++------- 3 files changed, 80 insertions(+), 31 deletions(-) diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 22a2d7fc2..c561ecf60 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -171,18 +171,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 ] @@ -203,7 +217,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/tactics/hints.ml b/tactics/hints.ml index d91ea8079..9a96b7389 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -100,18 +100,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 @@ -393,21 +400,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 42a2896ed..1be3e0c52 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -42,11 +42,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 { @@ -67,20 +68,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 -- cgit v1.2.3 From 823f0ab9c34f99d9171a5332a535c20d9f0f315c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 30 Nov 2016 15:00:13 +0100 Subject: Fix typeclasses eauto shelving. A file in the test-suite had to be modified. It was supposed to reproduce a behavior in intuistionistic-nuprl but it did not really. This commit is not supposed to break intuistionistic-nuprl. --- tactics/class_tactics.ml | 4 ++-- test-suite/success/Typeclasses.v | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index e44ace425..b47d8af56 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1129,7 +1129,7 @@ module Search = struct 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,7 +1147,7 @@ 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, goals = List.partition (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 Feedback.msg_debug 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. -- cgit v1.2.3 From 910a1aec499b304006f2a9291811087ca3c4c7a1 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 28 Nov 2016 16:06:06 +0100 Subject: Fix shelving order in typeclasses eauto. Before this fix, unshelve typeclasses eauto would produce sub-goals in the reverse order compared to when they were first shelved. --- tactics/class_tactics.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b47d8af56..b416bc657 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1124,7 +1124,7 @@ 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 @@ -1148,8 +1148,8 @@ module Search = struct (* Some existentials produced by the original tactic were not solved in the subgoals, turn them into subgoals now. *) let shelved, goals = List.partition (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 = 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 -- cgit v1.2.3 From f35eb5737fcdc1430eb45372d5bb99109d0216a2 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 28 Jun 2016 16:51:59 +0200 Subject: [merlin] Adjust merlin for ide. --- .merlin | 2 ++ ide/.merlin | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.merlin b/.merlin index 7ae642233..24226a918 100644 --- a/.merlin +++ b/.merlin @@ -2,6 +2,8 @@ FLG -rectypes -thread S config B config +S ide +B ide S lib B lib S intf 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 -- cgit v1.2.3 From 17c3f8e2d339e5b6f60c89ad17e578d786d2b9ca Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 15:14:23 +0100 Subject: More on fixing #5098 (preserving printing of "in hyp"). --- printing/pptactic.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 6e40e03f5..4b86381b4 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -630,7 +630,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 "<- " -- cgit v1.2.3 From 4e551415f20ad696c319b32b349e4499c2505388 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 17:58:07 +0100 Subject: Protect printing of ltac's "context [...]" from possible collision with user-level notations by inserting spaces. --- printing/pptactic.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 4b86381b4..fedc62f44 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -219,7 +219,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 -> @@ -676,9 +676,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) -> -- cgit v1.2.3 From 1c5e311d6a92deb66ba412c56516a4b71a513e01 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 15:35:05 +0100 Subject: Fixing printing of "only parsing" in abbreviations. --- printing/ppvernac.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3494ad006..be1587918 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1015,7 +1015,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 ( -- cgit v1.2.3 From 00f1839a2cee1cb1fa4dc207391c4a5bb588f71a Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 15:40:40 +0100 Subject: Fixing space in printing several list of implicit arguments. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index be1587918..75271e21e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1060,7 +1060,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 -- cgit v1.2.3 From a4db30e1cd6c21a466549835a86d61f95db36c82 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Apr 2016 22:24:59 +0200 Subject: Fixing printers for pr_auto_using and pr_firstorder_using. --- ltac/g_auto.ml4 | 10 +++++++--- plugins/firstorder/g_ground.ml4 | 6 +++--- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index c561ecf60..6a8fa8d69 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 @@ -206,8 +212,6 @@ GLOB_PRINTED BY pr_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 diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 95095b09c..43fac8ad8 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" -- cgit v1.2.3 From edb7a97487cb5e38bb284472eacfd1b58fa97f84 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Nov 2016 07:00:31 +0100 Subject: Fixing space in printing "Context". --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 75271e21e..953383321 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -913,7 +913,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 -> -- cgit v1.2.3 From ab3b0de5902082f7e692901979aa8330394c2f26 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 21 Nov 2016 12:58:02 +0100 Subject: Fixing printing of "Set Warnings Append". --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 953383321..5d6d36d56 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1131,7 +1131,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 ( -- cgit v1.2.3 From 0ea7bdc2e315da9a0a8338e5099dfcaad0bac9ef Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 2 Dec 2016 15:48:30 +0100 Subject: Fix #5242 - Dubious unsilenceable warning on invalid identifier We make this warning configurable and disabled by default. --- kernel/names.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/kernel/names.ml b/kernel/names.ml index 9267a64d6..1eb9a3175 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) -- cgit v1.2.3 From af58f731322527af1d81233beade4c98fbb2d7bd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Nov 2016 19:05:23 +0100 Subject: Univs: fix bug #5188 Parameter was implemented the wrong way trying to separate the universes of the telescope. --- test-suite/bugs/closed/5188.v | 5 +++++ toplevel/command.ml | 15 +++++++-------- 2 files changed, 12 insertions(+), 8 deletions(-) create mode 100644 test-suite/bugs/closed/5188.v 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/toplevel/command.ml b/toplevel/command.ml index 7ffe680e5..f6172a4b8 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -261,10 +261,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, _ = @@ -290,25 +287,27 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = else l in 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 + 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, Univ.ContextSet.empty)) ([],true,ctx) l) let do_assumptions_bound_univs coe kind nl id pl c = let env = Global.env () in -- cgit v1.2.3 From f492ddb3f9949993ad9072688e9e2cac7cfcbce0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 Dec 2016 16:46:05 +0100 Subject: Comment on universe handling in Parameters --- toplevel/command.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/toplevel/command.ml b/toplevel/command.ml index f6172a4b8..8b527ebd6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -286,6 +286,7 @@ 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,imps = interp_assumption evdref env ienv [] c in let env = @@ -297,6 +298,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = (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 @@ -307,7 +309,9 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l = (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u))) idl refs in - (subst'@subst, status' && status, Univ.ContextSet.empty)) ([],true,ctx) 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 -- cgit v1.2.3 From afab44873b7861d542cc0146d2bb8099d513f008 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 15:34:39 +0100 Subject: Fixing printing of "ltac:" in tactics after surrounding parentheses became mandatory. --- printing/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fedc62f44..fcc30d702 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1217,7 +1217,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 -- cgit v1.2.3 From 7e8434765ca1289aeb3a5200e791c9ced0acfde4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 20 Nov 2016 15:54:55 +0100 Subject: Fixing lexing of strings in comments for beautifier. Was a bug introduced in 0ad6edc1. --- parsing/cLexer.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index d570f015e..aec6a3264 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 -- cgit v1.2.3 From b8c0f76e507dc0c5dbae3ea7a89d78f16b4a7acb Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 2 Dec 2016 18:00:18 +0100 Subject: Document changes --- engine/evd.mli | 12 ++++++++++- kernel/univ.ml | 54 +++++++++++++++++++++++++++++++------------------- pretyping/cases.ml | 3 +++ pretyping/evarsolve.ml | 29 +++++++++++++++++---------- 4 files changed, 66 insertions(+), 32 deletions(-) diff --git a/engine/evd.mli b/engine/evd.mli index 89dcd92ce..86887f3dc 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 diff --git a/kernel/univ.ml b/kernel/univ.ml index c863fac0e..09f884ecd 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -468,20 +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 Inl (n < n') + 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 -> Inl false - | Prop, _ -> Inl true - | _, Prop -> Inl false - | _, _ -> Inr cmp) - | _, _ -> Inr cmp + | 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 @@ -603,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/pretyping/cases.ml b/pretyping/cases.ml index 27c1dd031..6e4d72705 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1935,6 +1935,9 @@ 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 diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 02e10d7fc..4fd030845 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -46,30 +46,35 @@ 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 refresh_sort status dir 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' in - let rec refresh onlyalg status dir t = + 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 dir s + | None -> refresh_sort status ~direction s | Some l -> (match Evd.universe_rigidity evd l with - | UnivRigid -> if not onlyalg then refresh_sort status dir s else t + | 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 dir -> - refresh_sort status dir s + | 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 onlyalg 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 = @@ -82,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 onlyalg 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 () @@ -103,8 +108,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let t' = if isArity t then match pbty with - | None -> refresh true univ_flexible false t - | Some dir -> refresh onlyalg status dir t + | 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 -- cgit v1.2.3 From f4818831f8661cab43ec0261d78140b0693d1381 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 2 Dec 2016 18:18:21 +0100 Subject: Fix test-suite after change in "context" printing. --- test-suite/output/Tactics.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3 From 7aa2c39387a9781bf406c763c538859f24b8b7f3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 5 Dec 2016 10:58:04 +0100 Subject: Compute dependency of C files only in kernel/byterun. Some C files included in build scripts (in dev/build) were triggering errors or warnings on non-win32 platforms. Note that ide/ide_win32_stubs.c was already handled through an ad-hoc rule in Makefile. If you add a new C file outside of kernel/byterun, please extend the CFILES variable. --- Makefile | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 6649542c8..1dd4efca2 100644 --- a/Makefile +++ b/Makefile @@ -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 -- cgit v1.2.3 From 436782a98f9f8d452f9b60cb27cd90a7bcf33253 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 5 Dec 2016 13:29:17 +0100 Subject: ssrmatching: handle primite projections (fix: #5247) --- plugins/ssrmatching/ssrmatching.ml4 | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index ef04bef8e..11f45d5d8 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -434,7 +434,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 @@ -486,6 +486,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 @@ -566,6 +567,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 @@ -576,7 +581,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 -- cgit v1.2.3 From 08c6e4c3dbe2ae851ef3097cc44618ea82717974 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 5 Dec 2016 17:26:55 -0500 Subject: the -byte option is deprecated --- doc/refman/RefMan-com.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index c1e552a5d..784c9ccbb 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -26,8 +26,8 @@ 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 -- cgit v1.2.3 From 2125949733b631426e955e722d6ca4e1b2eb5b60 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 5 Dec 2016 17:55:15 -0500 Subject: Change module for Coq loop --- doc/refman/RefMan-com.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 784c9ccbb..bef0a1686 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -32,7 +32,7 @@ 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 -- cgit v1.2.3 From 227ff6a46ad511ff2ab0ba1ffb9017bdb0291a58 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 6 Dec 2016 17:52:26 +0100 Subject: Update documentation (bugs #5246 and #5251). --- doc/refman/RefMan-gal.tex | 6 +++--- doc/refman/RefMan-tac.tex | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) 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..4b0652031 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -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} -- cgit v1.2.3 From 7af1b3e08452c3bbced6ca7eece2c91c6bf29137 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 6 Dec 2016 18:53:22 +0100 Subject: Fix broken documentation in presence of \zeroone{... \tt ...}. The way \zeroone was defined, the \tt modifier was leaked outside the brackets, thus messing with the following text. There are a bunch of occurrences of this issue in the manual, so rather than turning all the \tt into \texttt, the definition of \zeroone is made more robust. Unfortunately, there is one single occurrence of \zeroone that does not support the more robust version. (Note that this specific usage of \zeroone is morally a bug, since it goes against all the LaTeX conventions.) So the commit also keeps the old leaky version of \zeroone around as \zeroonelax so that it can be used there. --- doc/common/macros.tex | 3 ++- doc/refman/RefMan-tac.tex | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) 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/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 4b0652031..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}}}\\ -- cgit v1.2.3 From 40cffd816b7adbf8f136f62f6f891fb5be9b96a6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 6 Dec 2016 16:56:42 +0100 Subject: Fix #5248 - test-suite fails in 8.6beta1 This was yet another bug in the VM long multiplication, that I unfortunately introduced in ebc509ed2. It was impacting only 32-bit architectures. In the future, I'll try to make sure that 1) we provide unit tests for integer arithmetic (my int63 branch ships with such tests) 2) our continuous testing infrastructure runs the test suite on a 32-bit architecture. I tried to set up such an instance, but failed. Waiting for support reply. --- kernel/byterun/coq_interp.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 */ -- cgit v1.2.3