From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- pretyping/typeclasses.ml | 2 +- pretyping/vnorm.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d7b4842810..152ccb0798 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -123,7 +123,7 @@ let typeclass_univ_instance (cl,u') = 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 + if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) else Univ.Instance.empty | _ -> Univ.Instance.empty in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b08666483e..074b7373c7 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -174,7 +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 + if mib.mind_polymorphic then Univ.UContext.size (Univ.UInfoInd.univ_context mib.mind_universes) else 0 in let mk u = -- cgit v1.2.3 From bef2e53ae2286d0a7c61697f7a7a71bfdc0a3c99 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 5 Apr 2017 14:49:13 +0200 Subject: Subtyping inference for inductoves and records Also reinferred after sections discharge --- pretyping/inductiveops.ml | 65 ++++++++++++++++++++++++++++++++++++++++++++++ pretyping/inductiveops.mli | 5 ++++ 2 files changed, 70 insertions(+) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index d8252ea9bb..1f8600dc2c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -655,3 +655,68 @@ 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 = + 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 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' + 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 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_inds = entries; + Entries.mind_entry_polymorphic = poly; + Entries.mind_entry_universes = ground_uinfind; + } = mind_ent + in + let uinfind = + if poly then + begin + let uctx = Univ.UInfoInd.univ_context ground_uinfind in + let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind 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 ctxs' = infer_inductive_subtyping_arity_constructor + ctxs dosubst indentry.Entries.mind_entry_arity true + in + List.fold_left + (fun ctxs cons -> + infer_inductive_subtyping_arity_constructor ctxs dosubst cons false) + ctxs' indentry.Entries.mind_entry_lc + ) (env', evd', Univ.Constraint.empty) entries + in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, + Univ.UContext.make + (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), + subtyp_constraints)) + end + else ground_uinfind + in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index bdb6f996b9..7d89b1b2bd 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,3 +199,8 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit + +(* inference of subtyping condition for inductive types *) + +val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry -- cgit v1.2.3 From ab86b9b3999f3860bdb69824f585b9cf461ff295 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 7 Apr 2017 12:44:12 +0200 Subject: Use inductive subtyping for conv/cumul --- pretyping/reductionops.ml | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index c2a6483012..971ad78e67 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1361,9 +1361,24 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible +let sigma_leq_inductives ~flex uinfind i0 i1 sigma = + let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in + let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length i0) && + (Univ.Instance.length ind_instance = Univ.Instance.length i1)) then + anomaly (Pp.str "Invalid inductive subtyping encountered!") + else + let comp_subst = (Univ.Instance.append i0 i1) in + let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances } + Reduction.compare_instances = sigma_compare_instances; + Reduction.leq_inductives = sigma_leq_inductives } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = -- cgit v1.2.3 From 4385872b2d82fbad2be84f2423802e00e9d9575f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 8 Apr 2017 22:01:30 +0200 Subject: Make unification use subtyping info of inductives --- pretyping/evarconv.ml | 74 ++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 64 insertions(+), 10 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3757ba7e6d..882ea61a9d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -350,6 +350,21 @@ 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 uinfind u u' = + let u = EConstr.EInstance.kind evd u in + let u' = EConstr.EInstance.kind evd u' in + let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in + let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.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.subst_instance_constraints 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 +454,55 @@ 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 fall_back () = + 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 compare_heads evd = + match EConstr.kind evd term, EConstr.kind evd term' with + | Const (c, u), Const (c', u') -> + fall_back () + | 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) + | Construct (cons, u), Construct (cons', u') -> + fall_back () + | _, _ -> 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')] +(* >>>>>>> Make unification use subtyping info of inductives *) 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 -- cgit v1.2.3 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. --- pretyping/evarconv.ml | 94 +++++++++++++++++++++++++++++++++-------------- pretyping/reductionops.ml | 4 +- 2 files changed, 69 insertions(+), 29 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 882ea61a9d..eb8a0c85a0 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 971ad78e67..e374f7b3bb 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 -- cgit v1.2.3 From 7b5fcef8a0fb3b97a3980f10596137234061990f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 26 Apr 2017 15:24:35 +0200 Subject: Fix bugs --- pretyping/evarconv.ml | 6 ++++-- pretyping/inductiveops.ml | 41 ++++++++++++++++++++++++++--------------- pretyping/inductiveops.mli | 4 ++++ 3 files changed, 34 insertions(+), 17 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index eb8a0c85a0..ea22c3708f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -494,7 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_param_arity = - Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) + 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) @@ -520,7 +520,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_cnstr_args = - let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in + 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 diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1f8600dc2c..ebfb1f8a7c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -659,14 +659,22 @@ let control_only_guard 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 = + (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 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' + 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 @@ -680,12 +688,14 @@ let infer_inductive_subtyping_arity_constructor end | _ -> anomaly (Pp.str "") in - let typs, codom = Reduction.dest_prod env arcn 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_inds = entries; + let { Entries.mind_entry_params = params; + Entries.mind_entry_inds = entries; Entries.mind_entry_polymorphic = poly; Entries.mind_entry_universes = ground_uinfind; } = mind_ent @@ -704,15 +714,16 @@ let infer_inductive_subtyping env evd mind_ent = 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 ctxs' = infer_inductive_subtyping_arity_constructor - ctxs dosubst indentry.Entries.mind_entry_arity true - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor ctxs dosubst cons false) - ctxs' indentry.Entries.mind_entry_lc - ) (env', evd', Univ.Constraint.empty) entries + (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 Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, Univ.UContext.make (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7d89b1b2bd..811f47f39a 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -201,6 +201,10 @@ 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 -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- pretyping/evarconv.ml | 2 ++ pretyping/reductionops.ml | 64 +++++++++++++++++++++++++++++++++++++++-------- 2 files changed, 56 insertions(+), 10 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index ea22c3708f..be2fd81290 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -494,6 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_param_arity = + (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *) 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 @@ -521,6 +522,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty begin let num_cnstr_args = let nparamsctxt = + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) 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) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e374f7b3bb..2040acba79 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1361,24 +1361,68 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_leq_inductives ~flex uinfind i0 i1 sigma = +let sigma_check_inductive_instances cv_pb uinfind u u' sigma = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length i0) && - (Univ.Instance.length ind_instance = Univ.Instance.length i1)) then + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - let comp_subst = (Univ.Instance.append i0 i1) in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.subst_instance_constraints comp_subst ind_sbcst + in + let comp_cst = + match cv_pb with + Reduction.CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) 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 -> + if mind.Declarations.mind_polymorphic then + 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 + let uinfind = mind.Declarations.mind_universes in + sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma + else raise Reduction.NotConvertible + +let sigma_conv_constructors + (mind, ind, cns) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + if mind.Declarations.mind_polymorphic then + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) 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 + let uinfind = mind.Declarations.mind_universes in + sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma + else raise Reduction.NotConvertible let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances; - Reduction.leq_inductives = sigma_leq_inductives } + 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 = -- cgit v1.2.3 From fece24ec8aa88950477ccfed70b511f05b438718 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Fri, 28 Apr 2017 12:49:38 +0200 Subject: Fix a bug Incorrect environment was used when checking subtyping information of inductive types. --- pretyping/inductiveops.ml | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ebfb1f8a7c..1ef4a9f5e7 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -697,11 +697,12 @@ let infer_inductive_subtyping env evd mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; Entries.mind_entry_polymorphic = poly; + Entries.mind_entry_cumulative = cum; Entries.mind_entry_universes = ground_uinfind; } = mind_ent in let uinfind = - if poly then + if poly && cum then begin let uctx = Univ.UInfoInd.univ_context ground_uinfind in let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind in @@ -709,9 +710,9 @@ let infer_inductive_subtyping env evd mind_ent = 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 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 -> @@ -723,7 +724,7 @@ let infer_inductive_subtyping env evd mind_ent = (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 + ) (env, evd, Univ.Constraint.empty) entries in Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, Univ.UContext.make (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- pretyping/arguments_renaming.ml | 2 +- pretyping/evarconv.ml | 55 ++++++++++++++++------------- pretyping/inductiveops.ml | 77 ++++++++++++++++++++++++----------------- pretyping/recordops.ml | 5 ++- pretyping/reductionops.ml | 45 +++++++++++++++--------- pretyping/typeclasses.ml | 8 ++--- pretyping/vnorm.ml | 6 ++-- 7 files changed, 112 insertions(+), 86 deletions(-) (limited to 'pretyping') diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 1bd03491a7..c7b37aba5c 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -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/evarconv.ml b/pretyping/evarconv.ml index be2fd81290..b15dde5d79 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -350,18 +350,22 @@ 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 uinfind u u' = +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 ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + in + let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.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.subst_instance_constraints comp_subst ind_sbcst in + let comp_cst = + Univ.UContext.constraints (Univ.subst_instance_context comp_subst ind_sbcst) + in Evd.add_constraints evd comp_cst end @@ -491,23 +495,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let nparamsaplied' = Stack.args_size sk' in begin let mind = Environ.lookup_mind (fst ind) env in - if mind.Declarations.mind_polymorphic then + match mind.Declarations.mind_universes with + | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> + UnifFailure (evd, NotSameHead) + | Declarations.Cumulative_ind cumi -> begin let num_param_arity = - (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *) - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + 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 + 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) + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi u' u) end end - else - UnifFailure (evd, NotSameHead) end in first_try_strict_check (Names.eq_ind ind ind') u u' check_subtyping_constraints @@ -518,26 +523,29 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty 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 + 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 = - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs + 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) + nparamsctxt + + mind.Declarations.mind_packets.(snd ind). + Declarations.mind_consnrealargs.(j - 1) in - if not (num_cnstr_args = nparamsaplied && num_cnstr_args = nparamsaplied') then + 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) + let evd' = check_leq_inductives evd cumi u u' in + Success (check_leq_inductives evd' cumi 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 "") @@ -546,7 +554,6 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty 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')] -(* >>>>>>> Make unification use subtyping info of inductives *) 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/inductiveops.ml b/pretyping/inductiveops.ml index 1ef4a9f5e7..2ae7c0f809 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -696,39 +696,52 @@ let infer_inductive_subtyping_arity_constructor let infer_inductive_subtyping env evd mind_ent = let { Entries.mind_entry_params = params; Entries.mind_entry_inds = entries; - Entries.mind_entry_polymorphic = poly; - Entries.mind_entry_cumulative = cum; - Entries.mind_entry_universes = ground_uinfind; + Entries.mind_entry_universes = ground_univs; } = mind_ent in let uinfind = - if poly && cum then - begin - let uctx = Univ.UInfoInd.univ_context ground_uinfind in - let sbsubst = Univ.UInfoInd.subtyping_susbst ground_uinfind 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 Univ.UInfoInd.make (Univ.UInfoInd.univ_context ground_uinfind, - Univ.UContext.make - (Univ.UContext.instance (Univ.UInfoInd.subtyp_context ground_uinfind), - subtyp_constraints)) - end - else ground_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/recordops.ml b/pretyping/recordops.ml index bc9e3a1f46..283a1dcd18 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -197,7 +197,7 @@ let warn_projection_no_head_constant = (* 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 ctx = Environ.constant_context env con in let u = Univ.UContext.instance ctx in let v = (mkConstU (con,u)) in let ctx = Univ.ContextSet.of_context ctx in @@ -298,8 +298,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 = Environ.constant_instance 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/reductionops.ml b/pretyping/reductionops.ml index 2040acba79..123c610166 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1362,21 +1362,25 @@ let sigma_compare_instances ~flex i0 i1 sigma = raise Reduction.NotConvertible let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in - let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in + let ind_instance = + Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context uinfind) + in + let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_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.subst_instance_constraints comp_subst ind_sbcst + Univ.UContext.constraints (Univ.subst_instance_context 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.subst_instance_constraints comp_subst ind_sbcst) in + let comp_cst' = + Univ.UContext.constraints(Univ.subst_instance_context comp_subst ind_sbctx) + in Univ.Constraint.union comp_cst comp_cst' | Reduction.CUMUL -> comp_cst in @@ -1389,34 +1393,43 @@ 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 -> - if mind.Declarations.mind_polymorphic then + 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 + 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 - let uinfind = mind.Declarations.mind_universes in - sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma - else raise Reduction.NotConvertible + 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 -> - if mind.Declarations.mind_polymorphic then + 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 - (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in - nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + 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 - let uinfind = mind.Declarations.mind_universes in - sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma - else raise Reduction.NotConvertible + sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 152ccb0798..f883e647b5 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -111,20 +111,16 @@ 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 + Declareops.constant_polymorphic_instance cb | IndRef c -> let mib,oib = Global.lookup_inductive c in - if mib.mind_polymorphic then Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes) - else Univ.Instance.empty + Declareops.inductive_polymorphic_instance mib | _ -> 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') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 074b7373c7..9e151fea25 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -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 (Univ.UInfoInd.univ_context mib.mind_universes) - else 0 + Univ.Instance.length (Declareops.inductive_polymorphic_instance 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.Instance.length (Declareops.constant_polymorphic_instance cbody) in let mk u = let pcst = (cst, u) in (mkConstU pcst, Typeops.type_of_constant_in env pcst) -- cgit v1.2.3 From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 15 Jun 2017 16:50:05 +0200 Subject: Fix a bug in cumulativity --- pretyping/evarconv.ml | 9 +++++---- pretyping/reductionops.mli | 1 - 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b15dde5d79..d84363089d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -353,12 +353,13 @@ let exact_ise_stack2 env evd f sk1 sk2 = 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 ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) + let length_ind_instance = + Univ.Instance.length + (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)) in let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + 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 diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index af4ea3ac53..a4da19de75 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -66,7 +66,6 @@ module Cst_stack : sig val pr : t -> Pp.std_ppcmds end - module Stack : sig type 'a app_node -- cgit v1.2.3