From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sun, 21 May 2017 14:46:30 +0200 Subject: Squashed commit of the following: Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints. --- API/API.ml | 1 + API/API.mli | 7 +++- dev/include | 1 + dev/top_printers.ml | 1 + engine/termops.ml | 3 ++ engine/uState.ml | 2 +- engine/universes.ml | 30 -------------- engine/universes.mli | 4 -- kernel/declareops.ml | 21 ++++++---- kernel/kernel.mllib | 1 + kernel/reduction.ml | 70 +++++++++++++++++++++---------- kernel/subtyping.ml | 5 +++ kernel/univ.ml | 3 ++ kernel/univ.mli | 3 ++ kernel/univops.ml | 70 +++++++++++++++++++++++++++++++ kernel/univops.mli | 17 ++++++++ plugins/setoid_ring/newring.ml | 4 +- pretyping/evarconv.ml | 94 ++++++++++++++++++++++++++++++------------ pretyping/reductionops.ml | 4 +- proofs/proof_global.ml | 8 ++-- tactics/elimschemes.ml | 30 +++++++------- vernac/classes.ml | 10 +++-- vernac/command.ml | 12 +++--- 23 files changed, 276 insertions(+), 125 deletions(-) create mode 100644 kernel/univops.ml create mode 100644 kernel/univops.mli diff --git a/API/API.ml b/API/API.ml index 2b7bbd561..515b152e4 100644 --- a/API/API.ml +++ b/API/API.ml @@ -138,6 +138,7 @@ module Typeclasses = Typeclasses module Pretype_errors = Pretype_errors module Notation = Notation module Declarations = Declarations +module Univops = Univops module Declareops = Declareops module Globnames = Globnames module Environ = Environ diff --git a/API/API.mli b/API/API.mli index cea879ba3..a4ae6347c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1124,6 +1124,11 @@ sig | SFBmodtype of module_type_body end +module Univops : sig + val universes_of_constr : Term.constr -> Univ.LSet.t + val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t +end + module Environ : sig type env = Prelude.env @@ -2651,8 +2656,6 @@ sig val new_Type : Names.DirPath.t -> Term.types val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr - val universes_of_constr : Term.constr -> Univ.LSet.t - val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t diff --git a/dev/include b/dev/include index 0f43f0072..4835b360d 100644 --- a/dev/include +++ b/dev/include @@ -41,6 +41,7 @@ #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 info *) ppuniverse_info;; #install_printer (* univ set *) ppuniverse_set;; #install_printer (* univ instance *) ppuniverse_instance;; #install_printer (* univ subst *) ppuniverse_subst;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6ae5125f6..e902da0b1 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -215,6 +215,7 @@ let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = let ctx = Future.force c in ppuniverse_context ctx +let ppuniverse_info c = pp (Univ.pr_universe_info_ind Univ.Level.pr c) let ppuniverses u = pp (UGraph.pr_universes Level.pr u) let ppnamedcontextval e = pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e)) diff --git a/engine/termops.ml b/engine/termops.ml index 92016d4af..3eef71b2d 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1173,6 +1173,9 @@ let compare_constr_univ sigma f cv_pb t1 t2 = Sort s1, Sort s2 -> base_sort_cmp cv_pb (ESorts.kind sigma s1) (ESorts.kind sigma s2) | Prod (_,t1,c1), Prod (_,t2,c2) -> f Reduction.CONV t1 t2 && f cv_pb c1 c2 + | Const (c, u), Const (c', u') -> Constant.equal c c' + | Ind (i, _), Ind (i', _) -> eq_ind i i' + | Construct (i, _), Construct (i', _) -> eq_constructor i i' | _ -> EConstr.compare_constr sigma (fun t1 t2 -> f Reduction.CONV t1 t2) t1 t2 let constr_cmp sigma cv_pb t1 t2 = diff --git a/engine/uState.ml b/engine/uState.ml index acef90143..0973ca457 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -284,7 +284,7 @@ let universe_context ?names ctx = in map, ctx let restrict ctx vars = - let uctx' = Universes.restrict_universe_context ctx.uctx_local vars in + let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } type rigid = diff --git a/engine/universes.ml b/engine/universes.ml index 51957e00a..a12b42ab1 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -976,36 +976,6 @@ let normalize_context_set ctx us algs = (* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) (* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) -let universes_of_constr c = - let rec aux s c = - match kind_of_term c with - | Const (_, u) | Ind (_, u) | Construct (_, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> fold_constr aux s c - in aux LSet.empty c - -let restrict_universe_context (univs,csts) s = - (* Universes that are not necessary to typecheck the term. - E.g. univs introduced by tactics and not used in the proof term. *) - let diff = LSet.diff univs s in - let rec aux diff candid univs ness = - let (diff', candid', univs', ness') = - Constraint.fold - (fun (l, d, r as c) (diff, candid, univs, csts) -> - if not (LSet.mem l diff) then - (LSet.remove r diff, candid, univs, Constraint.add c csts) - else if not (LSet.mem r diff) then - (LSet.remove l diff, candid, univs, Constraint.add c csts) - else (diff, Constraint.add c candid, univs, csts)) - candid (diff, Constraint.empty, univs, ness) - in - if ness' == ness then (LSet.diff univs diff', ness) - else aux diff' candid' univs' ness' - in aux diff csts univs Constraint.empty - let simplify_universe_context (univs,csts) = let uf = UF.create () in let noneqs = diff --git a/engine/universes.mli b/engine/universes.mli index 1b9703c7b..c600f4af6 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -210,10 +210,6 @@ val unsafe_type_of_global : Globnames.global_reference -> types val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr -(** Shrink a universe context to a restricted set of variables *) - -val universes_of_constr : constr -> universe_set -val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst diff --git a/kernel/declareops.ml b/kernel/declareops.ml index cdea468ad..883896652 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -49,6 +49,11 @@ let instantiate cb c = Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c else c +let instantiate_constraints cb cst = + if cb.const_polymorphic then + Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst + else cst + let body_of_constant otab cb = match cb.const_body with | Undef _ -> None | Def c -> Some (instantiate cb (force_constr c)) @@ -61,13 +66,15 @@ let type_of_constant cb = if t' == t then x else RegularArity t' | TemplateArity _ as x -> x -let constraints_of_constant otab cb = Univ.Constraint.union - (Univ.UContext.constraints cb.const_universes) - (match cb.const_body with - | Undef _ -> Univ.empty_constraint - | Def c -> Univ.empty_constraint - | OpaqueDef o -> - Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) +let constraints_of_constant otab cb = + let cst = Univ.Constraint.union + (Univ.UContext.constraints cb.const_universes) + (match cb.const_body with + | Undef _ -> Univ.empty_constraint + | Def c -> Univ.empty_constraint + | OpaqueDef o -> + Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o)) + in instantiate_constraints cb cst let universes_of_constant otab cb = match cb.const_body with diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 2f49982ce..8132d6685 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,3 +43,4 @@ Vm Csymtable Vconv Declarations +Univops diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c8fad60eb..a872a103a 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -489,8 +489,8 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1), FInd (ind2,u2)) -> - if eq_ind ind1 ind2 - then + if eq_ind ind1 ind2 + then begin let fall_back () = let cuniv = convert_instances ~flex:false u1 u2 cuniv in @@ -498,31 +498,54 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = in let mind = Environ.lookup_mind (fst ind1) env in if mind.Declarations.mind_polymorphic then - begin - let num_param_arity = - Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt) - in - if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then - fall_back () - else begin - let uinfind = mind.Declarations.mind_universes in - let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in - let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + let num_param_arity = + Context.Rel.length (mind.Declarations.mind_packets.(snd ind1).Declarations.mind_arity_ctxt) + in + if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then + fall_back () + else + begin + let uinfind = mind.Declarations.mind_universes in + let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in + let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + end end - end else fall_back () end - else raise NotConvertible + else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> - if Int.equal j1 j2 && eq_ind ind1 ind2 - then - (let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv) - else raise NotConvertible + if Int.equal j1 j2 && eq_ind ind1 ind2 + then + begin + let fall_back () = + let cuniv = convert_instances ~flex:false u1 u2 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + in + let mind = Environ.lookup_mind (fst ind1) env in + if mind.Declarations.mind_polymorphic then + begin + let num_cnstr_args = + let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in + nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1) + in + if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then + fall_back () + else + begin (* we don't consider subtyping for constructors. *) + let uinfind = mind.Declarations.mind_universes in + let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in + let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv + end + end + else + fall_back () + end + else raise NotConvertible (* Eta expansion of records *) | (FConstruct ((ind1,j1),u1), _) -> @@ -688,7 +711,12 @@ let infer_cmp_universes env pb s0 s1 univs = else univs let infer_convert_instances ~flex u u' (univs,cstrs) = - (univs, Univ.enforce_eq_instances u u' cstrs) + let cstrs' = + if flex then + if UGraph.check_eq_instances univs u u' then cstrs + else raise NotConvertible + else Univ.enforce_eq_instances u u' cstrs + in (univs, cstrs') let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index f779f68be..60cd77f40 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -90,6 +90,7 @@ let check_conv_error error why cst poly u f env a1 a2 = else error (IncompatiblePolymorphism (env, a1, a2)) else Constraint.union cst cst' with NotConvertible -> error why + | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e) (* for now we do not allow reorderings *) @@ -302,6 +303,10 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let ctx2 = Univ.instantiate_univ_context cb2.const_universes in let inst1, ctx1 = Univ.UContext.dest ctx1 in let inst2, ctx2 = Univ.UContext.dest ctx2 in + output_string stderr "\ninst1:\n"; + output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst1)); + output_string stderr "\ninst2:\n"; + output_string stderr (Pp.string_of_ppcmds (Univ.Instance.pr Univ.Level.pr inst2)); flush stderr; if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then error IncompatibleInstances else diff --git a/kernel/univ.ml b/kernel/univ.ml index 4a4cf1baa..5de45cf2b 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -725,8 +725,11 @@ struct pp_std ++ prl u1 ++ pr_constraint_type op ++ prl u2 ++ fnl () ) c (str "") + let universes_of c = + fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end +let universes_of_constraints = Constraint.universes_of let empty_constraint = Constraint.empty let union_constraint = Constraint.union let eq_constraint = Constraint.equal diff --git a/kernel/univ.mli b/kernel/univ.mli index f139a8b33..114193329 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -462,3 +462,6 @@ val eq_levels : universe_level -> universe_level -> bool (** deprecated: Equality of formal universe expressions. *) val equal_universes : universe -> universe -> bool + +(** Universes of constraints *) +val universes_of_constraints : constraints -> universe_set diff --git a/kernel/univops.ml b/kernel/univops.ml new file mode 100644 index 000000000..e9383c6d9 --- /dev/null +++ b/kernel/univops.ml @@ -0,0 +1,70 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + LSet.fold LSet.add (Instance.levels u) s + | Sort u when not (Sorts.is_small u) -> + let u = univ_of_sort u in + LSet.fold LSet.add (Universe.levels u) s + | _ -> fold_constr aux s c + in aux LSet.empty c + +let universes_of_inductive mind = + if mind.mind_polymorphic then + begin + let u = Univ.UContext.instance (Univ.UInfoInd.univ_context mind.mind_universes) in + let univ_of_one_ind oind = + let arity_univs = + Context.Rel.fold_outside + (fun decl unvs -> + Univ.LSet.union + (Context.Rel.Declaration.fold_constr + (fun cnstr unvs -> + let cnstr = Vars.subst_instance_constr u cnstr in + Univ.LSet.union + (universes_of_constr cnstr) unvs) + decl Univ.LSet.empty) unvs) + oind.mind_arity_ctxt ~init:Univ.LSet.empty + in + Array.fold_left (fun unvs cns -> + let cns = Vars.subst_instance_constr u cns in + Univ.LSet.union (universes_of_constr cns) unvs) arity_univs + oind.mind_nf_lc + in + let univs = Array.fold_left (fun unvs pk -> Univ.LSet.union (univ_of_one_ind pk) unvs) Univ.LSet.empty mind.mind_packets in + let mindcnt = Univ.UContext.constraints (Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mind.mind_universes)) in + let univs = Univ.LSet.union univs (Univ.universes_of_constraints mindcnt) in + univs + end + else LSet.empty + +let restrict_universe_context (univs,csts) s = + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let rec aux diff candid univs ness = + let (diff', candid', univs', ness') = + Constraint.fold + (fun (l, d, r as c) (diff, candid, univs, csts) -> + if not (LSet.mem l diff) then + (LSet.remove r diff, candid, univs, Constraint.add c csts) + else if not (LSet.mem r diff) then + (LSet.remove l diff, candid, univs, Constraint.add c csts) + else (diff, Constraint.add c candid, univs, csts)) + candid (diff, Constraint.empty, univs, ness) + in + if ness' == ness then (LSet.diff univs diff', ness) + else aux diff' candid' univs' ness' + in aux diff csts univs Constraint.empty diff --git a/kernel/univops.mli b/kernel/univops.mli new file mode 100644 index 000000000..5b499c75b --- /dev/null +++ b/kernel/univops.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* universe_set +val universes_of_inductive : mutual_inductive_body -> universe_set +val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index ee75d2908..da21f64ab 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -153,8 +153,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na ctx c = let open Term in - let vars = Universes.universes_of_constr c in - let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in + let vars = Univops.universes_of_constr c in + let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in mkConst(declare_constant (Id.of_string na) (DefinitionEntry (definition_entry ~opaque:true ~univs:(Univ.ContextSet.to_context ctx) c), diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 882ea61a9..eb8a0c85a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -454,48 +454,88 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else evar_eqappr_x ts env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = - let fall_back () = + let check_strict () = let univs = EConstr.eq_constr_universes evd term term' in + match univs with + | Some univs -> + begin + let cstrs = Universes.to_constraints (Evd.universes evd) univs in + try Success (Evd.add_constraints evd cstrs) + with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + end + | None -> + UnifFailure (evd, NotSameHead) + in + let first_try_strict_check cond u u' try_subtyping_constraints = + if cond then + let univs = EConstr.eq_constr_universes evd term term' in match univs with | Some univs -> begin let cstrs = Universes.to_constraints (Evd.universes evd) univs in try Success (Evd.add_constraints evd cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) + with Univ.UniverseInconsistency p -> try_subtyping_constraints () end | None -> UnifFailure (evd, NotSameHead) + else + UnifFailure (evd, NotSameHead) in let compare_heads evd = match EConstr.kind evd term, EConstr.kind evd term' with | Const (c, u), Const (c', u') -> - fall_back () + check_strict () | Ind (ind, u), Ind (ind', u') -> - let nparamsaplied = Stack.args_size sk in - let nparamsaplied' = Stack.args_size sk' in - if Names.eq_ind ind ind' then - begin - let mind = Environ.lookup_mind (fst ind) env in - if mind.Declarations.mind_polymorphic then - begin - let num_param_arity = - Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) - in - if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then - fall_back () - else - begin - let uinfind = mind.Declarations.mind_universes in - let evd' = check_leq_inductives evd uinfind u u' in - Success (check_leq_inductives evd' uinfind u' u) - end - end - else - fall_back () - end - else UnifFailure (evd, NotSameHead) + let check_subtyping_constraints () = + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + begin + let mind = Environ.lookup_mind (fst ind) env in + if mind.Declarations.mind_polymorphic then + begin + let num_param_arity = + Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) + in + if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let uinfind = mind.Declarations.mind_universes in + let evd' = check_leq_inductives evd uinfind u u' in + Success (check_leq_inductives evd' uinfind u' u) + end + end + else + UnifFailure (evd, NotSameHead) + end + in + first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints | Construct (cons, u), Construct (cons', u') -> - fall_back () + let check_subtyping_constraints () = + let ind, ind' = fst cons, fst cons' in + let j, j' = snd cons, snd cons' in + let nparamsaplied = Stack.args_size sk in + let nparamsaplied' = Stack.args_size sk' in + let mind = Environ.lookup_mind (fst ind) env in + if mind.Declarations.mind_polymorphic then + begin + let num_cnstr_args = + let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in + nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1) + in + if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let uinfind = mind.Declarations.mind_universes in + let evd' = check_leq_inductives evd uinfind u u' in + Success (check_leq_inductives evd' uinfind u' u) + end + end + else + UnifFailure (evd, NotSameHead) + in + first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints | _, _ -> anomaly (Pp.str "") in ise_and evd [(fun i -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 971ad78e6..e374f7b3b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1313,8 +1313,8 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let report_anomaly _ = - let e = UserError (None, Pp.str "Conversion test raised an anomaly") in +let report_anomaly e = + let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in let e = CErrors.push e in iraise e diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 5ec34a638..f5664aed0 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -343,8 +343,8 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now nf t else t in - let used_univs_body = Universes.universes_of_constr body in - let used_univs_typ = Universes.universes_of_constr typ in + let used_univs_body = Univops.universes_of_constr body in + let used_univs_typ = Univops.universes_of_constr typ in if keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in @@ -353,7 +353,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now * complement the univ constraints of the typ with the ones of * the body. So we keep the two sets distinct. *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx_body = restrict_universe_context ctx used_univs in + let ctx_body = Univops.restrict_universe_context ctx used_univs in (initunivs, typ), ((body, ctx_body), eff) else let initunivs = Univ.UContext.empty in @@ -362,7 +362,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now * constraints in which we merge the ones for the body and the ones * for the typ *) let used_univs = Univ.LSet.union used_univs_body used_univs_typ in - let ctx = restrict_universe_context ctx used_univs in + let ctx = Univops.restrict_universe_context ctx used_univs in let univs = Univ.ContextSet.to_context ctx in (univs, typ), ((body, Univ.ContextSet.empty), eff) in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 466b1350d..8d8e19811 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -80,30 +80,30 @@ let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) -let ind_scheme_kind_from_type = - declare_individual_scheme_object "_ind_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) - -let ind_scheme_kind_from_prop = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" - (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp) - -let ind_dep_scheme_kind_from_type = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) -let rec_scheme_kind_from_type = - declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) - let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) +let ind_scheme_kind_from_type = + declare_individual_scheme_object "_ind_nodep" + (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp) + +let ind_dep_scheme_kind_from_type = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" + (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp) + +let ind_scheme_kind_from_prop = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" + (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp) + (* Case analysis *) let build_case_analysis_scheme_in_type dep sort ind = diff --git a/vernac/classes.ml b/vernac/classes.ml index aba61146c..007b70bc0 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -114,8 +114,8 @@ let instance_hook k info global imps ?hook cst = let declare_instance_constant k info global imps ?hook id pl poly evm term termtype = let kind = IsDefinition Instance in let evm = - let levels = Univ.LSet.union (Universes.universes_of_constr termtype) - (Universes.universes_of_constr term) in + let levels = Univ.LSet.union (Univops.universes_of_constr termtype) + (Univops.universes_of_constr term) in Evd.restrict_universe_context evm levels in let pl, uctx = Evd.universe_context ?names:pl evm in @@ -420,6 +420,8 @@ let context poly l = let _ = Command.declare_definition id decl entry [] [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in - let () = uctx := Univ.ContextSet.empty in status && nstatus - in List.fold_left fn true (List.rev ctx) + in + if Lib.sections_are_opened () then + Declare.declare_universe_context poly !uctx; + List.fold_left fn true (List.rev ctx) diff --git a/vernac/command.ml b/vernac/command.ml index 2d4f05134..116a7aee1 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -106,7 +106,7 @@ let interp_definition pl bl p red_option c ctypopt = let c = EConstr.Unsafe.to_constr c in let nf,subst = Evarutil.e_nf_evars_and_universes evdref in let body = nf (it_mkLambda_or_LetIn c ctx) in - let vars = Universes.universes_of_constr body in + let vars = Univops.universes_of_constr body in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in imps1@(Impargs.lift_implicits nb_args imps2), pl, @@ -131,8 +131,8 @@ let interp_definition pl bl p red_option c ctypopt = in if not (try List.for_all chk imps2 with Not_found -> false) then warn_implicits_in_term (); - let vars = Univ.LSet.union (Universes.universes_of_constr body) - (Universes.universes_of_constr typ) in + let vars = Univ.LSet.union (Univops.universes_of_constr body) + (Univops.universes_of_constr typ) in let ctx = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl ctx in imps1@(Impargs.lift_implicits nb_args impsty), pl, @@ -329,7 +329,7 @@ let do_assumptions_bound_univs coe kind nl id pl c = let nf, subst = Evarutil.e_nf_evars_and_universes evdref in let ty = EConstr.Unsafe.to_constr ty in let ty = nf ty in - let vars = Universes.universes_of_constr ty in + let vars = Univops.universes_of_constr ty in let evd = Evd.restrict_universe_context !evdref vars in let pl, uctx = Evd.universe_context ?names:pl evd in let uctx = Univ.ContextSet.of_context uctx in @@ -1213,7 +1213,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind let env = Global.env() in let indexes = search_guard env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in - let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in + let vars = Univops.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in @@ -1245,7 +1245,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let vars = Universes.universes_of_constr (List.hd fixdecls) in + let vars = Univops.universes_of_constr (List.hd fixdecls) in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in -- cgit v1.2.3