From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 11 Sep 2015 18:07:39 +0200 Subject: Universes: enforce Set <= i for all Type occurrences. --- Makefile.build | 2 +- kernel/indtypes.ml | 5 ++- kernel/univ.ml | 71 +++++++++++++++++++++++++++---------------- kernel/univ.mli | 10 ++++-- library/universes.ml | 41 +++++++++++++++++-------- pretyping/evd.ml | 41 ++++++++++++++++--------- pretyping/evd.mli | 6 ++-- theories/Classes/CMorphisms.v | 3 +- theories/Init/Logic.v | 2 +- toplevel/command.ml | 21 +++++++------ 10 files changed, 128 insertions(+), 74 deletions(-) diff --git a/Makefile.build b/Makefile.build index 30b93a0e8..0455a247b 100644 --- a/Makefile.build +++ b/Makefile.build @@ -69,7 +69,7 @@ TIMED= # non-empty will activate a default time command TIMECMD= # if you prefer a specific time command instead of $(STDTIME) # e.g. "'time -p'" - +CAMLFLAGS:=${CAMLFLAGS} -w -3 # NB: if you want to collect compilation timings of .v and import them # in a spreadsheet, I suggest something like: # make TIMED=1 2> timings.csv diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8c89abe94..9c065101a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -286,7 +286,10 @@ let typecheck_inductive env mie = let defu = Term.univ_of_sort def_level in let is_natural = type_in_type env || (check_leq (universes env') infu defu && - not (is_type0m_univ defu && not is_unit)) + not (is_type0m_univ defu && not is_unit) + (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *) + + ) in let _ = (** Impredicative sort, always allow *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 336cdb653..040e9bc27 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -270,8 +270,10 @@ module Level = struct let is_small x = match data x with | Level _ -> false - | _ -> true - + | Var _ -> false + | Prop -> true + | Set -> true + let is_prop x = match data x with | Prop -> true @@ -670,7 +672,7 @@ let arc_is_lt arc = match arc.status with | Unset | SetLe -> false | SetLt -> true -let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset} +let terminal ?(predicative=false) u = {univ=u; lt=[]; le=[]; rank=0; predicative; status = Unset} module UMap : sig @@ -720,6 +722,16 @@ let enter_arc ca g = (* Every Level.t has a unique canonical arc representative *) +(** The graph always contains nodes for Prop and Set. *) + +let terminal_lt u v = + {(terminal u) with lt=[v]} + +let empty_universes = + let g = enter_arc (terminal ~predicative:true Level.set) UMap.empty in + let g = enter_arc (terminal_lt Level.prop Level.set) g in + g + (* repr : universes -> Level.t -> canonical_arc *) (* canonical representative : we follow the Equiv links *) @@ -733,6 +745,22 @@ let rec repr g u = | Equiv v -> repr g v | Canonical arc -> arc +let get_prop_arc g = repr g Level.prop +let get_set_arc g = repr g Level.set +let is_set_arc u = Level.is_set u.univ +let is_prop_arc u = Level.is_prop u.univ + +let add_universe vlev ~predicative g = + let v = terminal ~predicative vlev in + let arc = + let arc = + if predicative then get_set_arc g else get_prop_arc g + in + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* [safe_repr] also search for the canonical representative, but if the graph doesn't contain the searched universe, we add it. *) @@ -745,6 +773,8 @@ let safe_repr g u = try g, safe_repr_rec g u with Not_found -> let can = terminal u in + let setarc = get_set_arc g in + let g = enter_arc {setarc with le=u::setarc.le} g in enter_arc can g, can (* reprleq : canonical_arc -> canonical_arc list *) @@ -789,7 +819,6 @@ let between g arcu arcv = in let good,_,_ = explore ([arcv],[],false) arcu in good - (* We assume compare(u,v) = LE with v canonical (see compare below). In this case List.hd(between g u v) = repr u Otherwise, between g u v = [] @@ -900,8 +929,9 @@ let get_explanation strict g arcu arcv = in find [] arc.lt in + let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in try - let (to_revert, c) = cmp [] [] [] [(arcu, [])] in + let (to_revert, c) = cmp start [] [] [(arcu, [])] in (** Reset all the touched arcs. *) let () = List.iter (fun arc -> arc.status <- Unset) to_revert in List.rev c @@ -972,7 +1002,6 @@ let fast_compare_neq strict g arcu arcv = else process_le c to_revert (arc :: lt_todo) le_todo lt le in - try let (to_revert, c) = cmp FastNLE [] [] [arcu] in (** Reset all the touched arcs. *) @@ -1021,10 +1050,6 @@ let check_equal g u v = let check_eq_level g u v = u == v || check_equal g u v -let is_set_arc u = Level.is_set u.univ -let is_prop_arc u = Level.is_prop u.univ -let get_prop_arc g = snd (safe_repr g Level.prop) - let check_smaller g strict u v = let g, arcu = safe_repr g u in let g, arcv = safe_repr g v in @@ -1120,7 +1145,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 Level.is_small arc.univ || arc.rank >= max_rank + if arc.rank >= max_rank && not (Level.is_small best_arc.univ) then (arc.rank, max_rank, arc, best_arc::rest) else (max_rank, old_max_rank, best_arc, arc::rest) in @@ -1150,7 +1175,7 @@ let merge g arcu arcv = (* we assume compare(u,v) = compare(v,u) = NLE *) (* merge_disc u v forces u ~ v with repr u as canonical repr *) let merge_disc g arc1 arc2 = - let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in + let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in let arcu, g = if not (Int.equal arc1.rank arc2.rank) then arcu, g else @@ -1173,8 +1198,8 @@ exception UniverseInconsistency of univ_inconsistency let error_inconsistency o u v (p:explanation option) = raise (UniverseInconsistency (o,make u,make v,p)) -(* enforc_univ_eq : Level.t -> Level.t -> unit *) -(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) +(* enforce_univ_eq : Level.t -> Level.t -> unit *) +(* enforce_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 @@ -1225,18 +1250,10 @@ let enforce_univ_lt u v g = let p = get_explanation false g arcv arcu in error_inconsistency Lt u v p -let empty_universes = UMap.empty - (* Prop = Set is forbidden here. *) -let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty +let initial_universes = empty_universes let is_initial_universes g = UMap.equal (==) g initial_universes - -let add_universe vlev g = - let v = terminal vlev in - let proparc = get_prop_arc g in - enter_arc {proparc with le=vlev::proparc.le} - (enter_arc v g) (* Constraints and sets of constraints. *) @@ -1370,10 +1387,12 @@ let check_univ_leq u v = let enforce_leq u v c = let open Universe.Huniv in + let rec aux acc v = match v with - | Cons (v, _, Nil) -> - fold (fun u -> constraint_add_leq u v) u c - | _ -> anomaly (Pp.str"A universe bound can only be a variable") + | Cons (v, _, l) -> + aux (fold (fun u -> constraint_add_leq u v) u c) l + | Nil -> acc + in aux c v let enforce_leq u v c = if check_univ_leq u v then c diff --git a/kernel/univ.mli b/kernel/univ.mli index 7aaf2ffe6..76453cbb0 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -20,7 +20,11 @@ sig val is_small : t -> bool (** Is the universe set or prop? *) - + + val is_prop : t -> bool + val is_set : t -> bool + (** Is it specifically Prop or Set *) + val compare : t -> t -> int (** Comparison function *) @@ -159,8 +163,8 @@ val is_initial_universes : universes -> bool val sort_universes : universes -> universes -(** Adds a universe to the graph, ensuring it is >= Prop. *) -val add_universe : universe_level -> universes -> universes +(** Adds a universe to the graph, ensuring it is >= Prop or Set. *) +val add_universe : universe_level -> predicative:bool -> universes -> universes (** {6 Constraints. } *) diff --git a/library/universes.ml b/library/universes.ml index 1c8a5ad77..c67371e3b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -182,10 +182,13 @@ let leq_constr_univs_infer univs m n = if Sorts.equal s1 s2 then true else let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - if Univ.check_leq univs u1 u2 then true - else - (cstrs := Constraints.add (u1, ULe, u2) !cstrs; - true) + if Univ.check_leq univs u1 u2 then + ((if Univ.is_small_univ u1 then + cstrs := Constraints.add (u1, ULe, u2) !cstrs); + true) + else + (cstrs := Constraints.add (u1, ULe, u2) !cstrs; + true) in let rec eq_constr' m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n @@ -820,10 +823,18 @@ let minimize_univ_variables ctx us algs left right cstrs = if v == None then fst (aux acc u) else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) us (ctx, us, algs, lbounds, cstrs) - + let normalize_context_set ctx us algs = let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in let uf = UF.create () in + (** Keep the Prop/Set <= i constraints separate for minimization *) + let smallles, csts = + Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> + if d == Le && Univ.Level.is_small l then + (Constraint.add cstr smallles, noneqs) + else (smallles, Constraint.add cstr noneqs)) + csts (Constraint.empty, Constraint.empty) + in let csts = (* We first put constraints in a normal-form: all self-loops are collapsed to equalities. *) @@ -831,11 +842,15 @@ let normalize_context_set ctx us algs = Univ.constraints_of_universes g in let noneqs = - Constraint.fold (fun (l,d,r) noneqs -> - if d == Eq then (UF.union l r uf; noneqs) - else Constraint.add (l,d,r) noneqs) - csts Constraint.empty + Constraint.fold (fun (l,d,r as cstr) noneqs -> + if d == Eq then (UF.union l r uf; noneqs) + else (* We ignore the trivial Prop/Set <= i constraints. *) + if d == Le && Univ.Level.is_small l then + noneqs + else Constraint.add cstr noneqs) + csts Constraint.empty in + let noneqs = Constraint.union noneqs smallles in let partition = UF.partition uf in let flex x = LMap.mem x us in let ctx, subst, eqs = List.fold_left (fun (ctx, subst, cstrs) s -> @@ -941,12 +956,12 @@ let simplify_universe_context (univs,csts) = let csts' = subst_univs_level_constraints subst csts' in (univs', csts'), subst -let is_small_leq (l,d,r) = - Level.is_small l && d == Univ.Le +let is_trivial_leq (l,d,r) = + Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r)) (* Prop < i <-> Set+1 <= i <-> Set < i *) let translate_cstr (l,d,r as cstr) = - if Level.equal Level.prop l && d == Univ.Lt then + if Level.equal Level.prop l && d == Univ.Lt && not (Level.equal Level.set r) then (Level.set, d, r) else cstr @@ -954,7 +969,7 @@ let refresh_constraints univs (ctx, cstrs) = let cstrs', univs' = Univ.Constraint.fold (fun c (cstrs', univs as acc) -> let c = translate_cstr c in - if Univ.check_constraint univs c && not (is_small_leq c) then acc + if is_trivial_leq c then acc else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) cstrs (Univ.Constraint.empty, univs) in ((ctx, cstrs'), univs') diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 632611291..fe5f12dd8 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -453,7 +453,7 @@ let add_constraints_context ctx cstrs = in { ctx with uctx_local = (univs, Univ.Constraint.union local local'); uctx_univ_variables = vars; - uctx_universes = Univ.merge_constraints cstrs ctx.uctx_universes } + uctx_universes = Univ.merge_constraints local' ctx.uctx_universes } (* let addconstrkey = Profile.declare_profile "add_constraints_context";; *) (* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *) @@ -1058,36 +1058,49 @@ let with_context_set rigid d (a, ctx) = let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) -let uctx_new_univ_variable rigid name +let uctx_new_univ_variable rigid name predicative ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = let u = Universes.new_univ_level (Global.current_dirpath ()) in let ctx' = Univ.ContextSet.add_universe u ctx in - let uctx' = + let uctx', pred = match rigid with - | UnivRigid -> uctx + | UnivRigid -> uctx, true | UnivFlexible b -> let uvars' = Univ.LMap.add u None uvars in if b then {uctx with uctx_univ_variables = uvars'; - uctx_univ_algebraic = Univ.LSet.add u avars} - else {uctx with uctx_univ_variables = Univ.LMap.add u None uvars} in + uctx_univ_algebraic = Univ.LSet.add u avars}, false + else {uctx with uctx_univ_variables = uvars'}, false + in + (* let ctx' = *) + (* if pred then *) + (* Univ.ContextSet.add_constraints *) + (* (Univ.Constraint.singleton (Univ.Level.set, Univ.Le, u)) ctx' *) + (* else ctx' *) + (* in *) let names = match name with | Some n -> add_uctx_names n u uctx.uctx_names | None -> uctx.uctx_names in + let initial = + Univ.add_universe u pred uctx.uctx_initial_universes + in + let uctx' = {uctx' with uctx_names = names; uctx_local = ctx'; - uctx_universes = Univ.add_universe u uctx.uctx_universes}, u - -let new_univ_level_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in + uctx_universes = Univ.add_universe u pred uctx.uctx_universes; + uctx_initial_universes = initial} + in uctx', u + +let new_univ_level_variable ?name ?(predicative=true) rigid evd = + let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in ({evd with universes = uctx'}, u) -let new_univ_variable ?name rigid evd = - let uctx', u = uctx_new_univ_variable rigid name evd.universes in +let new_univ_variable ?name ?(predicative=true) rigid evd = + let uctx', u = uctx_new_univ_variable rigid name predicative evd.universes in ({evd with universes = uctx'}, Univ.Universe.make u) -let new_sort_variable ?name rigid d = - let (d', u) = new_univ_variable rigid ?name d in +let new_sort_variable ?name ?(predicative=true) rigid d = + let (d', u) = new_univ_variable rigid ?name ~predicative d in (d', Type u) let make_flexible_variable evd b u = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 94d9d5f66..c2ccc6d21 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -505,9 +505,9 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts +val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level +val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe +val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts 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/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 048faa916..9d3952e64 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -267,10 +267,9 @@ Section GenericInstances. Qed. (** The complement of a crelation conserves its proper elements. *) - Program Definition complement_proper `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Proper (RA ==> RA ==> iff) (complement R) := _. + Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _. Next Obligation. Proof. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 50f853f0e..375495c88 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -370,7 +370,7 @@ Module EqNotations. End EqNotations. Import EqNotations. - +Set Printing Universes. Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a. Proof. intros. diff --git a/toplevel/command.ml b/toplevel/command.ml index e2e5d8704..d397eed61 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -467,16 +467,17 @@ let inductive_levels env evdref poly arities inds = Evd.set_leq_sort env evd (Prop Pos) du else evd in - (* let arity = it_mkProd_or_LetIn (mkType cu) ctx 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 - Evd.set_eq_sort env evd (Prop Null) du - else evd - else Evd.set_eq_sort env evd (Type cu) du - in - (evd, arity :: arities)) + 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 + else evd + else Evd.set_eq_sort env evd (Type cu) du + in + (evd, arity :: arities)) (!evdref,[]) (Array.to_list levels') destarities sizes in evdref := evd; List.rev arities -- cgit v1.2.3