diff options
| -rw-r--r-- | dev/base_include | 1 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | kernel/reduction.ml | 58 | ||||
| -rw-r--r-- | kernel/univ.ml | 47 | ||||
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 12 | ||||
| -rw-r--r-- | stm/lemmas.ml | 19 | ||||
| -rw-r--r-- | stm/lemmas.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 22 | ||||
| -rw-r--r-- | theories/Classes/CEquivalence.v | 4 | ||||
| -rw-r--r-- | theories/Classes/CMorphisms.v | 43 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 9 |
14 files changed, 94 insertions, 133 deletions
diff --git a/dev/base_include b/dev/base_include index fa6add7d3..6e10dac3f 100644 --- a/dev/base_include +++ b/dev/base_include @@ -155,7 +155,6 @@ open Command open Indschemes open Ind_tables open Auto_ind_decl -(* open Lemmas *) open Coqinit open Coqtop open Discharge diff --git a/dev/printers.mllib b/dev/printers.mllib index 5a9acb6dd..2eae9d598 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -194,4 +194,3 @@ Discharge Declare Ind_tables Top_printers - diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8773f4f34..a820e337e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -221,47 +221,23 @@ type conv_pb = let is_cumul = function CUMUL -> true | CONV -> false let is_pos = function Pos -> true | Null -> false -(* let sort_cmp env pb s0 s1 cuniv = *) -(* match (s0,s1) with *) -(* | (Prop c1, Prop c2) when is_cumul pb -> *) -(* begin match c1, c2 with *) -(* | Null, _ | _, Pos -> cuniv (\* Prop <= Set *\) *) -(* | _ -> raise NotConvertible *) -(* end *) -(* | (Prop c1, Prop c2) -> *) -(* if c1 == c2 then cuniv else raise NotConvertible *) -(* | (Prop c1, Type u) when is_cumul pb -> *) -(* enforce_leq (if is_pos c1 then Universe.type0 else Universe.type0m) u cuniv *) -(* | (Type u, Prop c) when is_cumul pb -> *) -(* enforce_leq u (if is_pos c then Universe.type0 else Universe.type0m) cuniv *) -(* | (Type u1, Type u2) -> *) -(* (match pb with *) -(* | CONV -> Univ.enforce_eq u1 u2 cuniv *) -(* | CUMUL -> enforce_leq u1 u2 cuniv) *) -(* | (_, _) -> raise NotConvertible *) - -(* let conv_sort env s0 s1 = sort_cmp CONV s0 s1 Constraint.empty *) -(* let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty *) - let check_eq (univs, cstrs as cuniv) u u' = match cstrs with | None -> if check_eq univs u u' then cuniv else raise NotConvertible | Some cstrs -> univs, Some (Univ.enforce_eq u u' cstrs) - (* let cstr = Univ.enforce_eq u u' Univ.Constraint.empty in *) - (* try let univs' = Univ.enforce_constraint cstr univs in *) - (* univs', Some (Univ.enforce_eq u u' cstrs) *) - (* with UniverseInconsistency _ -> raise NotConvertible *) -let check_leq (univs, cstrs as cuniv) u u' = +let check_leq ?(record=false) (univs, cstrs as cuniv) u u' = match cstrs with | None -> if check_leq univs u u' then cuniv else raise NotConvertible | Some cstrs -> - univs, Some (Univ.enforce_leq u u' cstrs) - (* let cstr = Univ.enforce_leq u u' Univ.Constraint.empty in *) - (* try let univs' = Univ.enforce_constraint cstr univs in *) - (* univs', Some (Univ.enforce_leq u u' cstrs) *) - (* with UniverseInconsistency _ -> raise NotConvertible *) + let cstrs' = Univ.enforce_leq u u' cstrs in + let cstrs' = if record then + Univ.Constraint.add (Option.get (Univ.Universe.level u),Univ.Le, + Option.get (Univ.Universe.level u')) cstrs' + else cstrs' + in + univs, Some cstrs' let sort_cmp_universes pb s0 s1 univs = match (s0,s1) with @@ -274,23 +250,14 @@ let sort_cmp_universes pb s0 s1 univs = | (Prop c1, Type u) -> let u0 = univ_of_sort s0 in (match pb with - | CUMUL -> check_leq univs u0 u + | CUMUL -> check_leq ~record:true univs u0 u | CONV -> check_eq univs u0 u) - | (Type u, Prop c) -> - let u1 = univ_of_sort s1 in - (match pb with - | CUMUL -> check_leq univs u u1 - | CONV -> check_eq univs u u1) + | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> (match pb with | CUMUL -> check_leq univs u1 u2 | CONV -> check_eq univs u1 u2) -(* let sort_cmp _ _ _ cuniv = cuniv *) - -(* let conv_sort env s0 s1 = sort_cmp CONV s0 s1 empty_constraint *) -(* let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 empty_constraint *) - let rec no_arg_available = function | [] -> true | Zupdate _ :: stk -> no_arg_available stk @@ -594,7 +561,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = compare_stacks - (fun (l1,t1) (l2,t2) c -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) + (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) (eq_ind) lft1 stk1 lft2 stk2 cuniv @@ -665,7 +632,8 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2 else Constr.eq_constr_univs_infer univs t1 t2 in - if b && Univ.check_constraints cstrs univs then cstrs + if b && (try ignore(Univ.merge_constraints cstrs univs); true with _ -> false) then + cstrs else let (u, cstrs) = clos_fconv reds cv_pb l2r evars env (univs, Some Constraint.empty) t1 t2 diff --git a/kernel/univ.ml b/kernel/univ.ml index 8a48eb5db..7ab0aa93c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1341,7 +1341,7 @@ let merge g arcu arcv = (* we find the arc with the biggest rank, and we redirect all others to it *) let arcu, g, v = let best_ranked (max_rank, old_max_rank, best_arc, rest) arc = - if arc.rank >= max_rank + if Level.is_small arc.univ || arc.rank >= max_rank then (arc.rank, max_rank, arc, best_arc::rest) else (max_rank, old_max_rank, best_arc, arc::rest) in @@ -1394,27 +1394,13 @@ exception UniverseInconsistency of univ_inconsistency let error_inconsistency o u v (p:explanation) = raise (UniverseInconsistency (o,make u,make v,p)) -(* enforce_univ_leq : Level.t -> Level.t -> unit *) -(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) -let enforce_univ_leq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in - if is_leq g arcu arcv then g - else match fast_compare g arcv arcu with - | FastLT -> - (match compare g arcv arcu with - | LT p -> error_inconsistency Le u v (List.rev (Lazy.force p)) - | _ -> anomaly (Pp.str "Univ.fast_compare")) - | FastLE -> merge g arcv arcu - | FastNLE -> fst (setleq g arcu arcv) - | FastEQ -> anomaly (Pp.str "Univ.compare") - (* enforc_univ_eq : Level.t -> Level.t -> unit *) (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) + let enforce_univ_eq u v g = let g,arcu = safe_repr g u in let g,arcv = safe_repr g v in - match fast_compare g arcu arcv with + match fast_compare g arcu arcv with | FastEQ -> g | FastLT -> (match compare g arcu arcv with @@ -1431,11 +1417,27 @@ let enforce_univ_eq u v g = | FastNLE -> merge_disc g arcu arcv | FastEQ -> anomaly (Pp.str "Univ.compare")) +(* enforce_univ_leq : Level.t -> Level.t -> unit *) +(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) +let enforce_univ_leq u v g = + let g,arcu = safe_repr g u in + let g,arcv = safe_repr g v in + if is_leq g arcu arcv then g + else + match fast_compare g arcv arcu with + | FastLT -> + (match compare g arcv arcu with + | LT p -> error_inconsistency Le u v (List.rev (Lazy.force p)) + | _ -> anomaly (Pp.str "Univ.fast_compare")) + | FastLE -> merge g arcv arcu + | FastNLE -> fst (setleq g arcu arcv) + | FastEQ -> anomaly (Pp.str "Univ.compare") + (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *) let enforce_univ_lt u v g = let g,arcu = safe_repr g u in let g,arcv = safe_repr g v in - match fast_compare g arcu arcv with + match fast_compare g arcu arcv with | FastLT -> g | FastLE -> fst (setlt g arcu arcv) | FastEQ -> @@ -1452,7 +1454,10 @@ let enforce_univ_lt u v g = | _ -> anomaly (Pp.str "Univ.fast_compare")) let empty_universes = LMap.empty -let initial_universes = enforce_univ_leq Level.prop Level.set LMap.empty + +(* Prop = Set is forbidden here. *) +let initial_universes = enforce_univ_lt Level.prop Level.set LMap.empty + let is_initial_universes g = LMap.equal (==) g initial_universes (* Constraints and sets of constraints. *) @@ -2176,7 +2181,7 @@ let normalize_universes g = univ = v; lt = LSet.elements lt; le = LSet.elements le; - rank = rank + rank = rank; } in LMap.mapi canonicalize g @@ -2321,7 +2326,7 @@ let sort_universes orig = let fold i accu u = if 0 < i then let pred = types.(i - 1) in - let arc = {univ = u; lt = [pred]; le = []; rank = 0; } in + let arc = {univ = u; lt = [pred]; le = []; rank = 0} in LMap.add u (Canonical arc) accu else accu in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1f462197c..940a54128 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1132,6 +1132,8 @@ let set_leq_sort evd s1 s2 = | Prop c, Prop c' -> if c == Null && c' == Pos then evd else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, []))) + | Type _, Prop _ -> + raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) | _, _ -> add_universe_constraints evd (Univ.UniverseConstraints.singleton (u1,Univ.ULe,u2)) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 7b6fb262a..1b2afd19a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -33,7 +33,6 @@ let occur_meta_or_undefined_evar evd c = | Evar_defined c -> occrec c; Array.iter occrec args | Evar_empty -> raise Occur) - (* | Sort (Type _) (\* FIXME could be finer *\) -> raise Occur *) | Const (_, i) (* | Ind (_, i) | Construct (_, i) *) when not (Univ.Instance.is_empty i) -> raise Occur | _ -> iter_constr occrec c @@ -749,7 +748,8 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag with Invalid_argument "Reductionops.Stack.fold2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - in + in + let res = if occur_meta_or_undefined_evar sigma m || occur_meta_or_undefined_evar sigma n || subterm_restriction conv_at_top flags then None diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 091ab29ae..89939b864 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -285,19 +285,19 @@ let close_proof ?feedback_id ~now fpl = let univsubst = (subst, Univ.ContextSet.to_context ctx) in univsubst, nf in - let make_body nf t _octx ((c, ctx), eff) = + let make_body nf ctx t _octx ((c, _ctx), eff) = let body = nf c and typ = nf t in let used_univs = Univ.LSet.union (Universes.universes_of_constr body) (Universes.universes_of_constr typ) in - let ctx = Universes.restrict_universe_context ctx used_univs in + let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) used_univs in let p = (body, Univ.ContextSet.empty),eff in let univs = Univ.ContextSet.to_context ctx in (univs, typ), p in - let make_body nf t octx p = - Future.split2 (Future.chain ~pure:true p (make_body nf t octx)) + let make_body nf ctx t octx p = + Future.split2 (Future.chain ~pure:true p (make_body nf ctx t octx)) in let univsubst = Future.chain ~pure:true univs make_usubst @@ -310,13 +310,13 @@ let close_proof ?feedback_id ~now fpl = in let univs = Univ.ContextSet.to_context ctx in let univsubst = (Univ.LMap.empty, univs) in - let make_body nf t octx p = Future.from_val (univs, t), p in + let make_body nf ctx t octx p = Future.from_val (univs, t), p in Future.from_val (univsubst, fun x -> x), make_body in let univsubst, nf = Future.force univsubst in let entries = Future.map2 (fun p (c, (t, octx)) -> - let univstyp, body = make_body nf t octx p in + let univstyp, body = make_body nf (snd univsubst) t octx p in let univs, typ = Future.force univstyp in { Entries. const_entry_body = body; diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 9cbd89e8b..0668af2c5 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -170,8 +170,6 @@ let look_for_possibly_mutual_statements = function let save id const cstrs do_guard (locality,poly,kind) hook = let const = adjust_guardness_conditions const do_guard in let k = Kindops.logical_kind_of_goal_kind kind in - (* Add global constraints necessary to check the type of the proof *) - let () = Global.push_context (snd cstrs) in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let c = SectionLocalDef const in @@ -316,13 +314,14 @@ let standard_proof_terminator compute_guard hook = save_anonymous_with_strength proof kind id end -let standard_proof_terminator compute_guard hook = +let universe_proof_terminator compute_guard hook = let open Proof_global in function | Admitted -> - admit hook (); + admit (hook (Univ.LMap.empty, Univ.UContext.empty)) (); Pp.feedback Interface.AddedAxiom | Proved (is_opaque,idopt,proof) -> - let proof = get_proof proof compute_guard hook is_opaque in + let proof = get_proof proof compute_guard + (hook proof.Proof_global.universes) is_opaque in begin match idopt with | None -> save_named proof | Some ((_,id),None) -> save_anonymous proof id @@ -340,6 +339,16 @@ let start_proof id kind ?sign c ?init_tac ?(compute_guard=[]) hook = !start_hook (fst c); Pfedit.start_proof id kind sign c ?init_tac terminator +let start_proof_univs id kind ?sign c ?init_tac ?(compute_guard=[]) hook = + let terminator = universe_proof_terminator compute_guard hook in + let sign = + match sign with + | Some sign -> sign + | None -> initialize_named_context_for_proof () + in + !start_hook (fst c); + Pfedit.start_proof id kind sign c ?init_tac terminator + (* FIXME: forgetting about the universes here *) let rec_tac_initializer finite guard thms snl = diff --git a/stm/lemmas.mli b/stm/lemmas.mli index f8694a096..8f5c75976 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -21,6 +21,10 @@ val start_proof : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> unit declaration_hook -> unit +val start_proof_univs : Id.t -> goal_kind -> ?sign:Environ.named_context_val -> types Univ.in_universe_context_set -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + (Proof_global.proof_universes -> unit declaration_hook) -> unit + val start_proof_com : goal_kind -> (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list -> unit declaration_hook -> unit diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8ed8f1856..8fe0a6893 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1286,7 +1286,6 @@ let specialize (c,lbind) g = let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in - let nargs = List.length tstack in let rec chk = function | [] -> [] | t::l -> if occur_meta t then [] else t :: chk l diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 1ef2713e4..99284eb54 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -211,7 +211,27 @@ Polymorphic Definition id {A : Type} (a : A) : A := a. Definition typeid := (@id Type). +Fail Check (Prop : Set). +Fail Check (Set : Set). +Check (Set : Type). +Check (Prop : Type). +Definition setType := $(let t := type of Set in exact t)$. +Definition foo (A : Prop) := A. + +Fail Check foo Set. +Check fun A => foo A. +Fail Check fun A : Type => foo A. +Check fun A : Prop => foo A. +Fail Definition bar := fun A : Set => foo A. + +Fail Check (let A := Type in foo (id A)). + +Definition fooS (A : Set) := A. + +Check (let A := nat in fooS (id A)). +Fail Check (let A := Set in fooS (id A)). +Fail Check (let A := Prop in fooS (id A)). (* Some tests of sort-polymorphisme *) Section S. @@ -227,7 +247,7 @@ End S. (* Check f nat nat : Set. *) -Definition foo:= I nat nat : Set. +Definition foo' := I nat nat. Print Universes. Print foo. Set Printing Universes. Print foo. (* Polymorphic axioms: *) diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index b540feabf..8610f18c3 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -107,11 +107,11 @@ Section Respecting. Definition respecting `(eqa : Equivalence A (R : crelation A), eqb : Equivalence B (R' : crelation B)) : Type := - { morph : A -> B | respectful R R' morph morph }. + { morph : A -> B & respectful R R' morph morph }. Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') : Equivalence (fun (f g : respecting eqa eqb) => - forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). + forall (x y : A), R x y -> R' (projT1 f x) (projT1 g y)). Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 4b031f949..b1c2842f7 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -192,10 +192,6 @@ Section Relations. intros. apply sub. apply mor. Qed. - Global Instance proper_subrelation_proper : - Proper (subrelation ++> eq ==> impl) (@Proper A). - Proof. reduce. subst. firstorder. Qed. - Global Instance proper_subrelation_proper_arrow : Proper (subrelation ++> eq ==> arrow) (@Proper A). Proof. reduce. subst. firstorder. Qed. @@ -301,16 +297,6 @@ Section GenericInstances. contravariant in the first argument, covariant in the second. *) Global Program - Instance trans_contra_co_morphism - `(Transitive A R) : Proper (R --> R ++> impl) R. - - Next Obligation. - Proof with auto. - transitivity x... - transitivity x0... - Qed. - - Global Program Instance trans_contra_co_type_morphism `(Transitive A R) : Proper (R --> R ++> arrow) R. @@ -323,15 +309,6 @@ Section GenericInstances. (** Proper declarations for partial applications. *) Global Program - Instance trans_contra_inv_impl_morphism - `(Transitive A R) : Proper (R --> flip impl) (R x) | 3. - - Next Obligation. - Proof with auto. - transitivity y... - Qed. - - Global Program Instance trans_contra_inv_impl_type_morphism `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3. @@ -380,15 +357,6 @@ Section GenericInstances. (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) Global Program - Instance trans_co_eq_inv_impl_morphism - `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2. - - Next Obligation. - Proof with auto. - transitivity y... - Qed. - - Global Program Instance trans_co_eq_inv_arrow_morphism `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2. @@ -669,17 +637,6 @@ Qed. (** A [PartialOrder] is compatible with its underlying equivalence. *) Require Import Relation_Definitions. -Instance PartialOrder_proper `(PartialOrder A eqA (R : crelation A)) : - Proper (eqA==>eqA==>iff) R. -Proof. -intros. -apply proper_sym_impl_iff_2; auto with *. -intros x x' Hx y y' Hy Hr. -transitivity x. -generalize (partial_order_equivalence x x'); compute; intuition. -transitivity y; auto. -generalize (partial_order_equivalence y y'); compute; intuition. -Qed. Instance PartialOrder_proper_type `(PartialOrder A eqA R) : Proper (eqA==>eqA==>iffT) R. diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index cce5242ec..91c58e60d 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -831,9 +831,9 @@ let rec solve_obligation prg num tac = let ctx = prg.prg_ctx in let obl = subst_deps_obl prg.prg_subst obls obl in let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in - Lemmas.start_proof obl.obl_name kind + Lemmas.start_proof_univs obl.obl_name kind (Universes.subst_opt_univs_constr prg.prg_subst obl.obl_type, ctx) - (fun strength gr -> + (fun (subst, ctx) strength gr -> let cst = match gr with ConstRef cst -> cst | _ -> assert false in let obl = let transparent = evaluable_constant cst (Global.env ()) in @@ -853,13 +853,12 @@ let rec solve_obligation prg num tac = in let obls = Array.copy obls in let _ = obls.(num) <- obl in -(* let ctx = Univ.ContextSet.of_context ctx in *) - let subst = Univ.LMap.empty (** FIXME *) in + let ctx = Univ.ContextSet.of_context ctx in let res = try update_obls {prg with prg_body = Universes.subst_opt_univs_constr subst prg.prg_body; prg_type = Universes.subst_opt_univs_constr subst prg.prg_type; - prg_ctx = ctx; + prg_ctx = Univ.ContextSet.union prg.prg_ctx ctx; prg_subst = Univ.LMap.union prg.prg_subst subst} obls (pred rem) with e when Errors.noncritical e -> |