summaryrefslogtreecommitdiff
path: root/pretyping/inductiveops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/inductiveops.ml')
-rw-r--r--pretyping/inductiveops.ml357
1 files changed, 254 insertions, 103 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 5bfc57bf..654f914b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -1,47 +1,52 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Errors
open Util
open Names
open Univ
open Term
+open Vars
+open Context
open Termops
-open Namegen
-open Sign
open Declarations
+open Declareops
open Environ
open Reductionops
+open Inductive
(* The following three functions are similar to the ones defined in
Inductive, but they expect an env *)
-let type_of_inductive env ind =
- let specif = Inductive.lookup_mind_specif env ind in
- Inductive.type_of_inductive env specif
+let type_of_inductive env (ind,u) =
+ let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+ Typeops.check_hyps_inclusion env (mkInd ind) mib.mind_hyps;
+ Inductive.type_of_inductive env (specif,u)
(* Return type as quoted by the user *)
-let type_of_constructor env cstr =
- let specif =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Inductive.type_of_constructor cstr specif
+let type_of_constructor env (cstr,u) =
+ let (mib,_ as specif) =
+ Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+ Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps;
+ Inductive.type_of_constructor (cstr,u) specif
(* Return constructor types in user form *)
-let type_of_constructors env ind =
+let type_of_constructors env (ind,u as indu) =
let specif = Inductive.lookup_mind_specif env ind in
- Inductive.type_of_constructors ind specif
+ Inductive.type_of_constructors indu specif
(* Return constructor types in normal form *)
-let arities_of_constructors env ind =
+let arities_of_constructors env (ind,u as indu) =
let specif = Inductive.lookup_mind_specif env ind in
- Inductive.arities_of_constructors ind specif
+ Inductive.arities_of_constructors indu specif
(* [inductive_family] = [inductive_instance] applied to global parameters *)
-type inductive_family = inductive * constr list
+type inductive_family = pinductive * constr list
let make_ind_family (mis, params) = (mis,params)
let dest_ind_family (mis,params) = (mis,params)
@@ -68,88 +73,224 @@ let lift_inductive_type n = liftn_inductive_type n 1
let substnl_ind_type l n = map_inductive_type (substnl l n)
let mkAppliedInd (IndType ((ind,params), realargs)) =
- applist (mkInd ind,params@realargs)
+ applist (mkIndU ind,params@realargs)
(* Does not consider imbricated or mutually recursive types *)
let mis_is_recursive_subset listind rarg =
- let rec one_is_rec rvec =
+ let one_is_rec rvec =
List.exists
(fun ra ->
match dest_recarg ra with
- | Mrec (_,i) -> List.mem i listind
+ | Mrec (_,i) -> Int.List.mem i listind
| _ -> false) rvec
in
- array_exists one_is_rec (dest_subterms rarg)
+ Array.exists one_is_rec (dest_subterms rarg)
let mis_is_recursive (ind,mib,mip) =
- mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1))
+ mis_is_recursive_subset (List.interval 0 (mib.mind_ntypes - 1))
mip.mind_recargs
-let mis_nf_constructor_type (ind,mib,mip) j =
+let mis_nf_constructor_type ((ind,u),mib,mip) j =
let specif = mip.mind_nf_lc
and ntypes = mib.mind_ntypes
and nconstr = Array.length mip.mind_consnames in
- let make_Ik k = mkInd ((fst ind),ntypes-k-1) in
+ let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
if j > nconstr then error "Not enough constructors in the type.";
- substl (list_tabulate make_Ik ntypes) specif.(j-1)
+ substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
+
+(* Number of constructors *)
+
+let nconstructors ind =
+ let (_,mip) = Global.lookup_inductive ind in
+ Array.length mip.mind_consnames
+
+let nconstructors_env env ind =
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ Array.length mip.mind_consnames
+
+(* Arity of constructors excluding parameters, excluding local defs *)
+
+let constructors_nrealargs ind =
+ let (_,mip) = Global.lookup_inductive ind in
+ mip.mind_consnrealargs
+
+let constructors_nrealargs_env env ind =
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ mip.mind_consnrealargs
+
+(* Arity of constructors excluding parameters, including local defs *)
+
+let constructors_nrealdecls ind =
+ let (_,mip) = Global.lookup_inductive ind in
+ mip.mind_consnrealdecls
+
+let constructors_nrealdecls_env env ind =
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ mip.mind_consnrealdecls
-(* Arity of constructors excluding parameters and local defs *)
+(* Arity of constructors including parameters, excluding local defs *)
-let mis_constr_nargs indsp =
+let constructor_nallargs (indsp,j) =
let (mib,mip) = Global.lookup_inductive indsp in
- let recargs = dest_subterms mip.mind_recargs in
- Array.map List.length recargs
+ mip.mind_consnrealargs.(j-1) + mib.mind_nparams
-let mis_constr_nargs_env env (kn,i) =
+let constructor_nallargs_env env ((kn,i),j) =
let mib = Environ.lookup_mind kn env in
let mip = mib.mind_packets.(i) in
- let recargs = dest_subterms mip.mind_recargs in
- Array.map List.length recargs
+ mip.mind_consnrealargs.(j-1) + mib.mind_nparams
-let mis_constructor_nargs_env env ((kn,i),j) =
+(* Arity of constructors including params, including local defs *)
+
+let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *)
+ let (mib,mip) = Global.lookup_inductive indsp in
+ mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+
+let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *)
let mib = Environ.lookup_mind kn env in
let mip = mib.mind_packets.(i) in
- recarg_length mip.mind_recargs j + mib.mind_nparams
+ mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+
+(* Arity of constructors excluding params, excluding local defs *)
-let constructor_nrealargs env (ind,j) =
+let constructor_nrealargs (ind,j) =
+ let (_,mip) = Global.lookup_inductive ind in
+ mip.mind_consnrealargs.(j-1)
+
+let constructor_nrealargs_env env (ind,j) =
let (_,mip) = Inductive.lookup_mind_specif env ind in
- recarg_length mip.mind_recargs j
+ mip.mind_consnrealargs.(j-1)
-let constructor_nrealhyps env (ind,j) =
- let (mib,mip) = Inductive.lookup_mind_specif env ind in
+(* Arity of constructors excluding params, including local defs *)
+
+let constructor_nrealdecls (ind,j) = (* TOCHANGE en decls *)
+ let (_,mip) = Global.lookup_inductive ind in
mip.mind_consnrealdecls.(j-1)
-let get_full_arity_sign env ind =
- let (mib,mip) = Inductive.lookup_mind_specif env ind in
- mip.mind_arity_ctxt
+let constructor_nrealdecls_env env (ind,j) = (* TOCHANGE en decls *)
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ mip.mind_consnrealdecls.(j-1)
-let nconstructors ind =
- let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
- Array.length mip.mind_consnames
+(* Length of arity, excluding params, excluding local defs *)
+
+let inductive_nrealargs ind =
+ let (_,mip) = Global.lookup_inductive ind in
+ mip.mind_nrealargs
+
+let inductive_nrealargs_env env ind =
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ mip.mind_nrealargs
+
+(* Length of arity, excluding params, including local defs *)
+
+let inductive_nrealdecls ind =
+ let (_,mip) = Global.lookup_inductive ind in
+ mip.mind_nrealdecls
+
+let inductive_nrealdecls_env env ind =
+ let (_,mip) = Inductive.lookup_mind_specif env ind in
+ mip.mind_nrealdecls
+
+(* Full length of arity (w/o local defs) *)
+
+let inductive_nallargs ind =
+ let (mib,mip) = Global.lookup_inductive ind in
+ mib.mind_nparams + mip.mind_nrealargs
+
+let inductive_nallargs_env env ind =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ mib.mind_nparams + mip.mind_nrealargs
(* Length of arity (w/o local defs) *)
-let inductive_nargs env ind =
+let inductive_nparams ind =
+ let (mib,mip) = Global.lookup_inductive ind in
+ mib.mind_nparams
+
+let inductive_nparams_env env ind =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ mib.mind_nparams
+
+(* Length of arity (with local defs) *)
+
+let inductive_nparamdecls ind =
+ let (mib,mip) = Global.lookup_inductive ind in
+ rel_context_length mib.mind_params_ctxt
+
+let inductive_nparamdecls_env env ind =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ rel_context_length mib.mind_params_ctxt
+
+(* Full length of arity (with local defs) *)
+
+let inductive_nalldecls ind =
+ let (mib,mip) = Global.lookup_inductive ind in
+ rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+
+let inductive_nalldecls_env env ind =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt)
+ rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+
+(* Others *)
+
+let inductive_paramdecls (ind,u) =
+ let (mib,mip) = Global.lookup_inductive ind in
+ Inductive.inductive_paramdecls (mib,u)
+
+let inductive_paramdecls_env env (ind,u) =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ Inductive.inductive_paramdecls (mib,u)
+
+let inductive_alldecls (ind,u) =
+ let (mib,mip) = Global.lookup_inductive ind in
+ Vars.subst_instance_context u mip.mind_arity_ctxt
+
+let inductive_alldecls_env env (ind,u) =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ Vars.subst_instance_context u mip.mind_arity_ctxt
+
+let constructor_has_local_defs (indsp,j) =
+ let (mib,mip) = Global.lookup_inductive indsp in
+ let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in
+ let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
+ not (Int.equal l1 l2)
+
+let inductive_has_local_defs ind =
+ let (mib,mip) = Global.lookup_inductive ind in
+ let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls in
+ let l2 = mib.mind_nparams + mip.mind_nrealargs in
+ not (Int.equal l1 l2)
let allowed_sorts env (kn,i as ind) =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
mip.mind_kelim
+let projection_nparams_env env p =
+ let pb = lookup_projection p env in
+ pb.proj_npars
+
+let projection_nparams p = projection_nparams_env (Global.env ()) p
+
(* Annotation for cases *)
let make_case_info env ind style =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in
+ let ind_tags =
+ rel_context_tags (List.firstn mip.mind_nrealargs mip.mind_arity_ctxt) in
+ let cstr_tags =
+ Array.map2 (fun c n ->
+ let d,_ = decompose_prod_assum c in
+ rel_context_tags (List.firstn n d))
+ mip.mind_nf_lc mip.mind_consnrealdecls in
+ let print_info = { ind_tags; cstr_tags; style } in
{ ci_ind = ind;
ci_npar = mib.mind_nparams;
ci_cstr_ndecls = mip.mind_consnrealdecls;
+ ci_cstr_nargs = mip.mind_consnrealargs;
ci_pp_info = print_info }
(*s Useful functions *)
type constructor_summary = {
- cs_cstr : constructor;
+ cs_cstr : pconstructor;
cs_params : constr list;
cs_nargs : int;
cs_args : rel_context;
@@ -170,33 +311,39 @@ let instantiate_params t args sign =
| ((_,None,_)::ctxt,a::args) ->
(match kind_of_term t with
| Prod(_,_,t) -> inst (a::s) t (ctxt,args)
- | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+ | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch"))
| ((_,(Some b),_)::ctxt,args) ->
(match kind_of_term t with
| LetIn(_,_,_,t) -> inst ((substl s b)::s) t (ctxt,args)
- | _ -> anomaly"instantiate_params: type, ctxt and args mismatch")
+ | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch"))
| _, [] -> substl s t
- | _ -> anomaly"instantiate_params: type, ctxt and args mismatch"
+ | _ -> anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch")
in inst [] t (List.rev sign,args)
-let get_constructor (ind,mib,mip,params) j =
+let get_constructor ((ind,u as indu),mib,mip,params) j =
assert (j <= Array.length mip.mind_consnames);
- let typi = mis_nf_constructor_type (ind,mib,mip) j in
+ let typi = mis_nf_constructor_type (indu,mib,mip) j in
let typi = instantiate_params typi params mib.mind_params_ctxt in
let (args,ccl) = decompose_prod_assum typi in
let (_,allargs) = decompose_app ccl in
- let vargs = list_skipn (List.length params) allargs in
- { cs_cstr = ith_constructor_of_inductive ind j;
+ let vargs = List.skipn (List.length params) allargs in
+ { cs_cstr = (ith_constructor_of_inductive ind j,u);
cs_params = params;
cs_nargs = rel_context_length args;
cs_args = args;
cs_concl_realargs = Array.of_list vargs }
let get_constructors env (ind,params) =
- let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
Array.init (Array.length mip.mind_consnames)
(fun j -> get_constructor (ind,mib,mip,params) (j+1))
+let get_projections env (ind,params) =
+ let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
+ match mib.mind_record with
+ | Some (Some (id, projs, pbs)) -> Some projs
+ | _ -> None
+
(* substitution in a signature *)
let substnl_rel_context subst n sign =
@@ -207,15 +354,15 @@ let substnl_rel_context subst n sign =
let substl_rel_context subst = substnl_rel_context subst 0
-let rec instantiate_context sign args =
+let instantiate_context sign args =
let rec aux subst = function
| (_,None,_)::sign, a::args -> aux (a::subst) (sign,args)
| (_,Some b,_)::sign, args -> aux (substl subst b::subst) (sign,args)
| [], [] -> subst
- | _ -> anomaly "Signature/instance mismatch in inductive family"
+ | _ -> anomaly (Pp.str "Signature/instance mismatch in inductive family")
in aux [] (List.rev sign,args)
-let get_arity env (ind,params) =
+let get_arity env ((ind,u),params) =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let parsign =
(* Dynamically detect if called with an instance of recursively
@@ -223,19 +370,21 @@ let get_arity env (ind,params) =
parameters *)
let parsign = mib.mind_params_ctxt in
let nnonrecparams = mib.mind_nparams - mib.mind_nparams_rec in
- if List.length params = rel_context_nhyps parsign - nnonrecparams then
- snd (list_chop nnonrecparams mib.mind_params_ctxt)
+ if Int.equal (List.length params) (rel_context_nhyps parsign - nnonrecparams) then
+ snd (List.chop nnonrecparams mib.mind_params_ctxt)
else
parsign in
+ let parsign = Vars.subst_instance_context u parsign in
let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in
- let arsign,_ = list_chop arproperlength mip.mind_arity_ctxt in
+ let arsign,_ = List.chop arproperlength mip.mind_arity_ctxt in
let subst = instantiate_context parsign params in
+ let arsign = Vars.subst_instance_context u arsign in
(substl_rel_context subst arsign, Inductive.inductive_sort_family mip)
(* Functions to build standard types related to inductive *)
let build_dependent_constructor cs =
applist
- (mkConstruct cs.cs_cstr,
+ (mkConstructU cs.cs_cstr,
(List.map (lift cs.cs_nargs) cs.cs_params)
@(extended_rel_list 0 cs.cs_args))
@@ -243,7 +392,7 @@ let build_dependent_inductive env ((ind, params) as indf) =
let arsign,_ = get_arity env indf in
let nrealargs = List.length arsign in
applist
- (mkInd ind,
+ (mkIndU ind,
(List.map (lift nrealargs) params)@(extended_rel_list 0 arsign))
(* builds the arity of an elimination predicate in sort [s] *)
@@ -252,7 +401,7 @@ let make_arity_signature env dep indf =
let (arsign,_) = get_arity env indf in
if dep then
(* We need names everywhere *)
- name_context env
+ Namegen.name_context env
((Anonymous,None,build_dependent_inductive env indf)::arsign)
(* Costly: would be better to name once for all at definition time *)
else
@@ -265,7 +414,7 @@ let make_arity env dep indf s = mkArity (make_arity_signature env dep indf, s)
let build_branch_type env dep p cs =
let base = appvect (lift cs.cs_nargs p, cs.cs_concl_realargs) in
if dep then
- it_mkProd_or_LetIn_name env
+ Namegen.it_mkProd_or_LetIn_name env
(applist (base,[build_dependent_constructor cs]))
cs.cs_args
else
@@ -288,18 +437,18 @@ let find_mrectype env sigma c =
let find_rectype env sigma c =
let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
match kind_of_term t with
- | Ind ind ->
+ | Ind (ind,u as indu) ->
let (mib,mip) = Inductive.lookup_mind_specif env ind in
if mib.mind_nparams > List.length l then raise Not_found;
- let (par,rargs) = list_chop mib.mind_nparams l in
- IndType((ind, par),rargs)
+ let (par,rargs) = List.chop mib.mind_nparams l in
+ IndType((indu, par),rargs)
| _ -> raise Not_found
let find_inductive env sigma c =
let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
match kind_of_term t with
| Ind ind
- when (fst (Inductive.lookup_mind_specif env ind)).mind_finite ->
+ when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite ->
(ind, l)
| _ -> raise Not_found
@@ -307,7 +456,7 @@ let find_coinductive env sigma c =
let (t, l) = decompose_app (whd_betadeltaiota env sigma c) in
match kind_of_term t with
| Ind ind
- when not (fst (Inductive.lookup_mind_specif env ind)).mind_finite ->
+ when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite ->
(ind, l)
| _ -> raise Not_found
@@ -322,7 +471,7 @@ let is_predicate_explicitly_dep env pred arsign =
match kind_of_term pv', arsign with
| Lambda (na,t,b), (_,None,_)::arsign ->
srec (push_rel_assum (na,t) env) b arsign
- | Lambda (na,_,_), _ ->
+ | Lambda (na,_,t), _ ->
(* The following code has an impact on the introduction names
given by the tactics "case" and "inversion": when the
@@ -341,13 +490,15 @@ let is_predicate_explicitly_dep env pred arsign =
dependency status (of course, Anonymous implies non
dependent, but not conversely).
- At the end, this is only to preserve the compatibility: a
- check whether the predicate is actually dependent or not
- would indeed be more natural! *)
+ From Coq > 8.2, using or not the the effective dependency of
+ the predicate is parametrable! *)
- na <> Anonymous
+ begin match na with
+ | Anonymous -> false
+ | Name _ -> true
+ end
- | _ -> anomaly "Non eta-expanded dep-expanded \"match\" predicate"
+ | _ -> anomaly (Pp.str "Non eta-expanded dep-expanded \"match\" predicate")
in
srec env pred arsign
@@ -357,7 +508,7 @@ let is_elim_predicate_explicitly_dependent env pred indf =
let set_names env n brty =
let (ctxt,cl) = decompose_prod_n_assum n brty in
- it_mkProd_or_LetIn_name env cl ctxt
+ Namegen.it_mkProd_or_LetIn_name env cl ctxt
let set_pattern_names env ind brv =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
@@ -367,19 +518,19 @@ let set_pattern_names env ind brv =
rel_context_length ((prod_assum c)) -
mib.mind_nparams)
mip.mind_nf_lc in
- array_map2 (set_names env) arities brv
+ Array.map2 (set_names env) arities brv
let type_case_branches_with_names env indspec p c =
let (ind,args) = indspec in
- let (mib,mip as specif) = Inductive.lookup_mind_specif env ind in
+ let (mib,mip as specif) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
- let (params,realargs) = list_chop nparams args in
+ let (params,realargs) = List.chop nparams args in
let lbrty = Inductive.build_branches_type ind specif params p in
(* Build case type *)
let conclty = Reduction.beta_appvect p (Array.of_list (realargs@[c])) in
(* Adjust names *)
if is_elim_predicate_explicitly_dependent env p (ind,params) then
- (set_pattern_names env ind lbrty, conclty)
+ (set_pattern_names env (fst ind) lbrty, conclty)
else (lbrty, conclty)
(* Type of Case predicates *)
@@ -393,40 +544,44 @@ let arity_of_case_predicate env (ind,params) dep k =
(* Inferring the sort of parameters of a polymorphic inductive type
knowing the sort of the conclusion *)
+
(* Compute the inductive argument types: replace the sorts
that appear in the type of the inductive by the sort of the
conclusion, and the other ones by fresh universes. *)
-let rec instantiate_universes env scl is = function
+let rec instantiate_universes env evdref scl is = function
| (_,Some _,_ as d)::sign, exp ->
- d :: instantiate_universes env scl is (sign, exp)
+ d :: instantiate_universes env evdref scl is (sign, exp)
| d::sign, None::exp ->
- d :: instantiate_universes env scl is (sign, exp)
- | (na,None,ty)::sign, Some u::exp ->
+ d :: instantiate_universes env evdref scl is (sign, exp)
+ | (na,None,ty)::sign, Some l::exp ->
let ctx,_ = Reduction.dest_arity env ty in
+ let u = Univ.Universe.make l in
let s =
(* Does the sort of parameter [u] appear in (or equal)
the sort of inductive [is] ? *)
- if univ_depends u is then
+ if univ_level_mem l is then
scl (* constrained sort: replace by scl *)
else
- (* unconstriained sort: replace by fresh universe *)
- new_Type_sort() in
- (na,None,mkArity(ctx,s)):: instantiate_universes env scl is (sign, exp)
+ (* unconstrained sort: replace by fresh universe *)
+ let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
+ let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
+ evdref := evm; s
+ in
+ (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp)
| sign, [] -> sign (* Uniform parameters are exhausted *)
| [], _ -> assert false
-(* Does not deal with universes, but only with Set/Type distinction *)
-let type_of_inductive_knowing_conclusion env mip conclty =
+let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
match mip.mind_arity with
- | Monomorphic s ->
- s.mind_user_arity
- | Polymorphic ar ->
- let _,scl = Reduction.dest_arity env conclty in
- let ctx = List.rev mip.mind_arity_ctxt in
- let ctx =
- instantiate_universes
- env scl ar.poly_level (ctx,ar.poly_param_levels) in
- mkArity (List.rev ctx,scl)
+ | RegularArity s -> sigma, subst_instance_constr u s.mind_user_arity
+ | TemplateArity ar ->
+ let _,scl = Reduction.dest_arity env conclty in
+ let ctx = List.rev mip.mind_arity_ctxt in
+ let evdref = ref sigma in
+ let ctx =
+ instantiate_universes
+ env evdref scl ar.template_level (ctx,ar.template_param_levels) in
+ !evdref, mkArity (List.rev ctx,scl)
(***********************************************)
(* Guard condition *)
@@ -447,7 +602,3 @@ let control_only_guard env c =
iter_constr_with_full_binders push_rel iter env c
in
iter env c
-
-let subst_inductive subst (kn,i as ind) =
- let kn' = Mod_subst.subst_ind subst kn in
- if kn == kn' then ind else (kn',i)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 07:22:43 +0000