diff options
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 3 | ||||
| -rw-r--r-- | library/universes.ml | 33 | ||||
| -rw-r--r-- | library/universes.mli | 4 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 11 | ||||
| -rw-r--r-- | theories/Classes/CRelationClasses.v | 15 |
6 files changed, 53 insertions, 14 deletions
diff --git a/dev/include b/dev/include index 58fff078b..a8c4e1d49 100644 --- a/dev/include +++ b/dev/include @@ -38,6 +38,7 @@ #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; +#install_printer (* univ context future *) ppuniverse_context_future;; #install_printer (* univ context set *) ppuniverse_context_set;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 857a989dc..ec7716356 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -192,6 +192,9 @@ let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) let ppconstraints_map c = pp (Universes.pr_constraints_map c) let ppconstraints c = pp (pr_constraints c) let ppuniverseconstraints c = pp (UniverseConstraints.pr c) +let ppuniverse_context_future c = + let ctx = Future.force c in + ppuniverse_context ctx let ppenv e = pp (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ diff --git a/library/universes.ml b/library/universes.ml index d8fa563a0..2b42e3fe8 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -251,7 +251,7 @@ type universe_full_subst = (universe_level * universe) list (** Precondition: flexible <= ctx *) let choose_canonical ctx flexible algs s = let global = LSet.diff s ctx in - let flexible, rigid = LSet.partition (fun x -> LMap.mem x flexible) (LSet.inter s ctx) in + let flexible, rigid = LSet.partition flexible (LSet.inter s ctx) in (** If there is a global universe in the set, choose it *) if not (LSet.is_empty global) then let canon = LSet.choose global in @@ -589,8 +589,9 @@ let normalize_context_set ctx us algs = csts Constraint.empty in let partition = UF.partition uf in + let flex x = LMap.mem x us in let subst, eqs = List.fold_left (fun (subst, cstrs) s -> - let canon, (global, rigid, flexible) = choose_canonical ctx us algs s in + let canon, (global, rigid, flexible) = choose_canonical ctx flex algs s in (* Add equalities for globals which can't be merged anymore. *) let cstrs = LSet.fold (fun g cst -> Constraint.add (canon, Univ.Eq, g) cst) global cstrs @@ -675,6 +676,34 @@ let restrict_universe_context (univs,csts) s = csts Constraint.empty in (univs', csts') +let simplify_universe_context (univs,csts) s = + let uf = UF.create () in + let noneqs = + Constraint.fold (fun (l,d,r) noneqs -> + if d == Eq && (LSet.mem l univs || LSet.mem r univs) then + (UF.union l r uf; noneqs) + else Constraint.add (l,d,r) noneqs) + csts Constraint.empty + in + let partition = UF.partition uf in + let flex x = LSet.mem x univs in + let subst, univs', csts' = List.fold_left (fun (subst, univs, cstrs) s -> + let canon, (global, rigid, flexible) = choose_canonical univs flex LSet.empty s in + (* Add equalities for globals which can't be merged anymore. *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) (LSet.union global rigid) + cstrs + in + let subst = LSet.fold (fun f -> LMap.add f canon) + flexible subst + in (subst, LSet.diff univs flexible, cstrs)) + (LMap.empty, univs, noneqs) partition + in + (* Noneqs is now in canonical form w.r.t. equality constraints, + and contains only inequality constraints. *) + 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 diff --git a/library/universes.mli b/library/universes.mli index a41b07362..150686d73 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -78,7 +78,7 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn val subst_opt_univs_constr : universe_opt_subst -> constr -> constr -val choose_canonical : universe_set -> universe_opt_subst -> universe_set -> universe_set -> +val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> universe_level * (universe_set * universe_set * universe_set) val instantiate_with_lbound : @@ -171,6 +171,8 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds val universes_of_constr : constr -> universe_set val shrink_universe_context : universe_context_set -> universe_set -> universe_context_set val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set +val simplify_universe_context : universe_context_set -> universe_set -> + universe_context_set * universe_level_subst val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f2da99c13..29810eb9a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -274,7 +274,7 @@ let close_proof ?feedback_id ~now fpl = let () = if poly || now then ignore (Future.compute univs) in let entries = Future.map2 (fun p (c, (t, octx)) -> let compute_univs (usubst, uctx) = - let nf = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst in + let nf x = Universes.nf_evars_and_universes_opt_subst (fun _ -> None) usubst x in let compute_c_t (c, eff) = let c, t = if not now then nf c, nf t @@ -283,9 +283,12 @@ let close_proof ?feedback_id ~now fpl = let univs = Univ.LSet.union (Universes.universes_of_constr c) (Universes.universes_of_constr t) - in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context uctx) univs in - (c, eff), t, Univ.ContextSet.to_context ctx + in + let ctx, subst = + Universes.simplify_universe_context (Univ.ContextSet.of_context uctx) univs + in + let nf x = Vars.subst_univs_level_constr subst x in + (nf c, eff), nf t, Univ.ContextSet.to_context ctx in Future.chain ~pure:true p compute_c_t in diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index ca38ac5b4..5e04671ba 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -341,13 +341,14 @@ Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : type (** The partial order defined by subrelation and crelation equivalence. *) -Program Instance subrelation_partial_order : - ! PartialOrder (crelation A) relation_equivalence subrelation. - -Next Obligation. -Proof. - unfold relation_equivalence in *. compute; firstorder. -Qed. +(* Program Instance subrelation_partial_order : *) +(* ! PartialOrder (crelation A) relation_equivalence subrelation. *) +(* Obligation Tactic := idtac. *) + +(* Next Obligation. *) +(* Proof. *) +(* intros x. refine (fun x => x). *) +(* Qed. *) Typeclasses Opaque relation_equivalence. |