diff options
Diffstat (limited to 'pretyping')
62 files changed, 405 insertions, 139 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 1bd03491a7..ea33f1c0d6 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,7 +43,7 @@ let section_segment_of_reference = function | ConstRef con -> Lib.section_segment_of_constant con | IndRef (kn,_) | ConstructRef ((kn,_),_) -> Lib.section_segment_of_mutual_inductive kn - | _ -> [], Univ.LMap.empty, Univ.UContext.empty + | _ -> [], Univ.LMap.empty, Univ.AUContext.empty let discharge_rename_args = function | _, (ReqGlobal (c, names), _ as req) -> diff --git a/pretyping/arguments_renaming.mli b/pretyping/arguments_renaming.mli index e123e77862..804e38216c 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b88532e1b9..49f073d663 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 4b1fde25a8..428f64b999 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 6c2086f3e0..19d61a64db 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index eb25994bef..3ee7bebf08 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 8d87f6e99c..078990a8c1 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -403,7 +403,7 @@ type coercion = { (* Computation of the class arity *) let reference_arity_length ref = - let t = Universes.unsafe_type_of_global ref in + let t, _ = Global.type_of_global_in_context (Global.env ()) ref in List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *) let projection_arity_length p = diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c4238e8b0d..2e5ce30f35 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 1282e3cb86..535a62046a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index ab1f6c110f..a8c07d2efa 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 2cb837ba03..886cfd880f 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 4734c90a87..1d7019d09f 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c93b1e568c..f830d4be3f 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index da287ae9f0..ffd67299d5 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3757ba7e6d..cb76df4e8a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -205,7 +205,8 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = else match (Stack.strip_n_app (l_us-1) sk2_effective) with | None -> raise Not_found | Some (l',el,s') -> (l'@Stack.append_app [|el|] Stack.empty,s') in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let u, ctx' = Universes.fresh_instance_from ctx None in + let subst = Univ.make_inverse_instance_subst u in let c = EConstr.of_constr c in let c' = subst_univs_level_constr subst c in let t' = EConstr.of_constr t' in @@ -350,6 +351,23 @@ let exact_ise_stack2 env evd f sk1 sk2 = ise_stack2 evd (List.rev sk1) (List.rev sk2) else UnifFailure (evd, (* Dummy *) NotSameHead) +let check_leq_inductives evd cumi u u' = + let u = EConstr.EInstance.kind evd u in + let u' = EConstr.EInstance.kind evd u' in + let length_ind_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in + if not ((length_ind_instance = Univ.Instance.length u) && + (length_ind_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + begin + let comp_subst = (Univ.Instance.append u u') in + let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in + Evd.add_constraints evd comp_cst + end + let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in @@ -439,16 +457,102 @@ 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 univs = EConstr.eq_constr_universes evd term term' in - match univs with - | Some univs -> - ise_and evd [(fun i -> - let cstrs = Universes.to_constraints (Evd.universes i) univs in - try Success (Evd.add_constraints i cstrs) - with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] - | None -> - UnifFailure (evd,NotSameHead) + 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 -> 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') -> + check_strict () + | Ind (ind, u), Ind (ind', u') -> + 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 + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> + begin + let num_param_arity = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + in + if not (num_param_arity = nparamsaplied + && num_param_arity = nparamsaplied') then + UnifFailure (evd, NotSameHead) + else + begin + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) + end + end + end + in + first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints + | Construct (cons, u), Construct (cons', u') -> + 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 + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> + begin + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + 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 evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) + end + end + in + first_try_strict_check (Names.eq_constructor cons cons') u u' check_subtyping_constraints + | _, _ -> anomaly (Pp.str "") + in + ise_and evd [(fun i -> + try compare_heads i + with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); + (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] in let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = let switch f a b = if on_left then f a b else f b a in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 45857df2ae..c30d1d26bf 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 2d86daadb6..7f5a780f9c 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index b8134a28c5..c727332c79 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ff0aeff75d..9f48297613 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -70,7 +70,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) else t | UnivFlexible alg -> if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref false l; t) + (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) else t)) | Prop Pos when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 02b5c59d26..811b4dc18f 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 3fc569fc4a..9e7652da64 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index d22f94e4e5..e77d8ff645 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9c09396ccc..b94228e75e 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 6bb421e732..bd9e111f5c 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 97aec1814f..aced42f839 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index a22470ae8c..2825c4d83a 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d8252ea9bb..88ca9b5ca8 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -655,3 +655,93 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c + +(* inference of subtyping condition for inductive types *) + +let infer_inductive_subtyping_arity_constructor + (env, evd, csts) (subst : constr -> constr) (arcn : Term.types) is_arity (params : Context.Rel.t) = + let numchecked = ref 0 in + let numparams = Context.Rel.nhyps params in + let update_contexts (env, evd, csts) csts' = + (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') + in + let basic_check (env, evd, csts) tp = + let result = + if !numchecked >= numparams then + let csts' = + Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) + in update_contexts (env, evd, csts) csts' + else + (env, evd, csts) + in + numchecked := !numchecked + 1; result + in + let infer_typ typ ctxs = + match typ with + | LocalAssum (_, typ') -> + begin + try + let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) + with Reduction.NotConvertible -> + anomaly ~label:"inference of record/inductive subtyping relation failed" + (Pp.str "Can't infer subtyping for record/inductive type") + end + | _ -> anomaly (Pp.str "") + in + let arcn' = Term.it_mkProd_or_LetIn arcn params in + let typs, codom = Reduction.dest_prod env arcn' in + let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in + if not is_arity then basic_check last_contexts codom else last_contexts + +let infer_inductive_subtyping env evd mind_ent = + let { Entries.mind_entry_params = params; + Entries.mind_entry_inds = entries; + Entries.mind_entry_universes = ground_univs; + } = mind_ent + in + let uinfind = + match ground_univs with + | Entries.Monomorphic_ind_entry _ + | Entries.Polymorphic_ind_entry _ -> ground_univs + | Entries.Cumulative_ind_entry cumi -> + begin + let uctx = Univ.CumulativityInfo.univ_context cumi in + let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in + let dosubst = subst_univs_level_constr sbsubst in + let instance_other = + Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) + in + let constraints_other = + Univ.subst_univs_level_constraints + sbsubst (Univ.UContext.constraints uctx) + in + let uctx_other = Univ.UContext.make (instance_other, constraints_other) in + let env = Environ.push_context uctx env in + let env = Environ.push_context uctx_other env in + let evd = + Evd.merge_universe_context + evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) + in + let (_, _, subtyp_constraints) = + List.fold_left + (fun ctxs indentry -> + let _, params = Typeops.infer_local_decls env params in + let ctxs' = infer_inductive_subtyping_arity_constructor + ctxs dosubst indentry.Entries.mind_entry_arity true params + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor + ctxs dosubst cons false params + ) + ctxs' indentry.Entries.mind_entry_lc + ) (env, evd, Univ.Constraint.empty) entries + in + Entries.Cumulative_ind_entry + (Univ.CumulativityInfo.make + (Univ.CumulativityInfo.univ_context cumi, + Univ.UContext.make + (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), + subtyp_constraints))) + end + in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index bdb6f996b9..aa38d3b47d 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -199,3 +199,12 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit + +(* inference of subtyping condition for inductive types *) +(* for debugging purposes only to be removed *) +val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> +(Term.constr -> Term.constr) -> +Term.types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t + +val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index e555742bca..86bc471323 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index c7661239e3..718d074cf4 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 69bc2d11ff..bc563b46dc 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index f30dc1a4b6..dae29208ed 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 61118cf777..5142af3567 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index c899340c8c..4e7f2110dd 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index c36542aebc..5826cc1355 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 791fd74ed3..3a1faf1c77 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index d7c04b08b0..54b477bed9 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index c303d5d949..124fa6e06c 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 7488f35bfe..bfc6bf5cff 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -511,8 +511,8 @@ let pretype_global ?loc rigid env evd gr us = match us with | None -> evd, None | Some l -> - let _, ctx = Universes.unsafe_constr_of_global gr in - let len = Univ.UContext.size ctx in + let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in + let len = Univ.AUContext.size ctx in interp_instance ?loc evd ~len l in let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index e17468ef83..6e533f1784 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/program.ml b/pretyping/program.ml index f9be82024a..bdc34bc532 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/program.mli b/pretyping/program.mli index 8439b9528c..70ab97e83e 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bc9e3a1f46..a23579609a 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -134,7 +134,7 @@ let find_projection = function type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (* position of trivial argument if any *) o_TABS : constr list; (* ordered *) o_TPARAMS : constr list; (* ordered *) @@ -189,22 +189,26 @@ let cs_pattern_of_constr t = let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" - (fun (t,con_pp,proji_sp_pp) -> + (fun (sign,env,t,con,proji_sp) -> + let sign = List.map (on_snd EConstr.Unsafe.to_constr) sign in + let env = Termops.push_rels_assum sign env in + let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in + let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in + let term_pp = Termops.print_constr_env env Evd.empty (EConstr.of_constr t) in strbrk "Projection value has no head constant: " - ++ Termops.print_constr (EConstr.of_constr t) ++ strbrk " in canonical instance " + ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) let compute_canonical_projections warn (con,ind) = let env = Global.env () in - let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in - let u = Univ.UContext.instance ctx in + let ctx = Environ.constant_context env con in + let u = Univ.make_abstract_instance ctx in let v = (mkConstU (con,u)) in - let ctx = Univ.ContextSet.of_context ctx in let c = Environ.constant_value_in env (con,u) in - let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in + let sign,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in let t = EConstr.Unsafe.to_constr t in - let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in + let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) sign in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in @@ -221,9 +225,7 @@ let compute_canonical_projections warn (con,ind) = let patt, n , args = cs_pattern_of_constr t in ((ConstRef proji_sp, patt, t, n, args) :: l) with Not_found -> - let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) - and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + if warn then warn_projection_no_head_constant (sign,env,t,con,proji_sp); l end | _ -> l) @@ -298,8 +300,7 @@ let error_not_structure ref = let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in let env = Global.env () in - let ctx = Environ.constant_context env sp in - let u = Univ.UContext.instance ctx in + let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc | None -> error_not_structure ref in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 7c0d0ec6d4..de09edcdcb 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,7 +57,7 @@ type cs_pattern = type obj_typ = { o_DEF : constr; - o_CTX : Univ.ContextSet.t; + o_CTX : Univ.AUContext.t; o_INJ : int option; (** position of trivial argument *) o_TABS : constr list; (** ordered *) o_TPARAMS : constr list; (** ordered *) diff --git a/pretyping/redops.ml b/pretyping/redops.ml index 8e190f40b9..b5e4a7acbf 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/redops.mli b/pretyping/redops.mli index f6d4d80862..435b25091e 100644 --- a/pretyping/redops.mli +++ b/pretyping/redops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c2a6483012..1d75fecb15 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,7 +29,7 @@ exception Elimconst let refolding_in_reduction = ref false let _ = Goptions.declare_bool_option { - Goptions.optdepr = false; + Goptions.optdepr = true; (* remove in 8.8 *) Goptions.optname = "Perform refolding of fixpoints/constants like cbn during reductions"; Goptions.optkey = ["Refolding";"Reduction"]; @@ -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 @@ -1361,9 +1361,79 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible +let sigma_check_inductive_instances cv_pb uinfind u u' sigma = + let len_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) + in + let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in + if not ((len_instance = Univ.Instance.length u) && + (len_instance = Univ.Instance.length u')) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.AUContext.instantiate comp_subst ind_sbctx + in + let comp_cst = + match cv_pb with + Reduction.CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in + Univ.Constraint.union comp_cst comp_cst' + | Reduction.CUMUL -> comp_cst + in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + +let sigma_conv_inductives + cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> + let num_param_arity = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + raise Reduction.NotConvertible + else + sigma_check_inductive_instances cv_pb cumi u1 u2 sigma + +let sigma_conv_constructors + (mind, ind, cns) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Polymorphic_ind _ -> + raise Reduction.NotConvertible + | Declarations.Cumulative_ind cumi -> + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + nparamsctxt + + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + raise Reduction.NotConvertible + else + sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma + let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances } + Reduction.compare_instances = sigma_compare_instances; + Reduction.conv_inductives = sigma_conv_inductives; + Reduction.conv_constructors = sigma_conv_constructors} let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index af4ea3ac53..db407b6c9b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -66,7 +66,6 @@ module Cst_stack : sig val pr : t -> Pp.std_ppcmds end - module Stack : sig type 'a app_node diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a1d0977f5a..e0f9bfcb72 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 25129db1c9..163d3975af 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 62737b65e0..76f35f76f5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index c31212e26a..91726e8c6d 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d7b4842810..d4fa266c02 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -57,6 +57,9 @@ type direction = Forward | Backward (* This module defines type-classes *) type typeclass = { + (* Universe quantification *) + cl_univs : Univ.AUContext.t; + (* The class implementation *) cl_impl : global_reference; @@ -111,27 +114,11 @@ let new_instance cl info glob poly impl = let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes" let instances : instances ref = Summary.ref Refmap.empty ~name:"instances" -open Declarations - -let typeclass_univ_instance (cl,u') = - let subst = - let u = - match cl.cl_impl with - | ConstRef c -> - let cb = Global.lookup_constant c in - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes - else Univ.Instance.empty - | IndRef c -> - let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes - else Univ.Instance.empty - | _ -> Univ.Instance.empty - in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) - Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u') - in - let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in - { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context); - cl_props = subst_ctx cl.cl_props}, u' +let typeclass_univ_instance (cl, u) = + assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u); + let subst_ctx c = Context.Rel.map (subst_instance_constr u) c in + { cl with cl_context = on_snd subst_ctx cl.cl_context; + cl_props = subst_ctx cl.cl_props} let class_info c = try Refmap.find c !classes @@ -189,7 +176,8 @@ let subst_class (subst,cl) = do_subst_ctx ctx in let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in - { cl_impl = do_subst_gr cl.cl_impl; + { cl_univs = cl.cl_univs; + cl_impl = do_subst_gr cl.cl_impl; cl_context = do_subst_context cl.cl_context; cl_props = do_subst_ctx cl.cl_props; cl_projs = do_subst_projs cl.cl_projs; @@ -203,15 +191,14 @@ let discharge_class (_,cl) = let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in (decl' :: ctx', NamedDecl.get_id decl :: subst) ) ctx ([], []) in - let discharge_rel_context subst n rel = + let discharge_rel_context (subst, usubst) n rel = let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in - let ctx, _ = - List.fold_right - (fun decl (ctx, k) -> - RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k - ) - rel ([], n) - in ctx + let fold decl (ctx, k) = + let map c = subst_univs_level_constr usubst (substn_vars k subst c) in + RelDecl.map_constr map decl :: ctx, succ k + in + let ctx, _ = List.fold_right fold rel ([], n) in + ctx in let abs_context cl = match cl.cl_impl with @@ -231,12 +218,14 @@ let discharge_class (_,cl) = in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in if cl_impl' == cl.cl_impl then cl else - let ctx, usubst, uctx = abs_context cl in + let ctx, _, _ as info = abs_context cl in let ctx, subst = rel_of_variable_context ctx in - let context = discharge_context ctx subst cl.cl_context in - let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in + let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in + let context = discharge_context ctx (subst, usubst) cl.cl_context in + let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in let discharge_proj (x, y, z) = x, y, Option.smartmap Lib.discharge_con z in - { cl_impl = cl_impl'; + { cl_univs = cl_univs'; + cl_impl = cl_impl'; cl_context = context; cl_props = props; cl_projs = List.smartmap discharge_proj cl.cl_projs; @@ -283,8 +272,10 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in let ty, ctx = Global.type_of_global_in_context env glob in + let inst, ctx = Universes.fresh_instance_from ctx None in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in - let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in let rec aux pri c ty path = match class_of_constr sigma ty with | None -> [] @@ -321,7 +312,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in + let term = Universes.constr_of_global_univ (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] @@ -409,7 +400,7 @@ let remove_instance i = remove_instance_hint i.is_impl let declare_instance info local glob = - let ty = Global.type_of_global_unsafe glob in + let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 8d1c0b94ca..99cdbd3a36 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,6 +16,10 @@ type direction = Forward | Backward (** This module defines type-classes *) type typeclass = { + (** The toplevel universe quantification in which the typeclass lives. In + particular, [cl_props] and [cl_context] are quantified over it. *) + cl_univs : Univ.AUContext.t; + (** The class implementation: a record parameterized by the context with defs in it or a definition if the class is a singleton. This acts as the class' global identifier. *) cl_impl : global_reference; @@ -64,7 +68,7 @@ val class_info : global_reference -> typeclass (** raises a UserError if not a c val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.EInstance.t) * constr list (** Get the instantiated typeclass structure for a given universe instance. *) -val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses +val typeclass_univ_instance : typeclass puniverses -> typeclass (** Just return None if not a class *) val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 754dacd193..dc8ff2e208 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 558575ccce..557aa3c9f9 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7ad988ad0b..1bb0035751 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1f3ba34e51..1e20788268 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 67c8b07e78..f090921e5c 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 0d90ab1584..fce17d5641 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b08666483e..66cc42cb61 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -174,8 +174,7 @@ and nf_whd env sigma whd typ = | Vatom_stk(Aind ((mi,i) as ind), stk) -> let mib = Environ.lookup_mind mi env in let nb_univs = - if mib.mind_polymorphic then Univ.UContext.size mib.mind_universes - else 0 + Univ.AUContext.size (Declareops.inductive_polymorphic_context mib) in let mk u = let pind = (ind, u) in (mkIndU pind, type_of_ind env pind) @@ -204,8 +203,7 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk = | ConstKey cst -> let cbody = Environ.lookup_constant cst env in let nb_univs = - if cbody.const_polymorphic then Univ.UContext.size cbody.const_universes - else 0 + Univ.AUContext.size (Declareops.constant_polymorphic_context cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index 8a4202c887..d1a996a34b 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |