diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 46 |
1 files changed, 23 insertions, 23 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e248436ec4..8e9b606a58 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -11,6 +11,7 @@ open Util open Names open Univ open Term +open Constr open Vars open Declarations open Declareops @@ -130,11 +131,11 @@ let is_unit constrsinfos = let infos_and_sort env t = let rec aux env t max = let t = whd_all env t in - match kind_of_term t with + match kind t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in let env1 = Environ.push_rel (LocalAssum (name,varj.utj_val)) env in - let max = Universe.sup max (univ_of_sort varj.utj_type) in + let max = Universe.sup max (Sorts.univ_of_sort varj.utj_type) in aux env1 c2 max | _ when is_constructor_head t -> max | _ -> (* don't fail if not positive, it is tested later *) max @@ -168,7 +169,7 @@ let infer_constructor_packet env_ar_par params lc = let jlc = List.map (infer_type env_ar_par) lc in let jlc = Array.of_list jlc in (* generalize the constructor over the parameters *) - let lc'' = Array.map (fun j -> it_mkProd_or_LetIn j.utj_val params) jlc in + let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) let levels = List.map (infos_and_sort env_ar_par) lc in let isunit = is_unit levels in @@ -183,7 +184,7 @@ let cumulate_arity_large_levels env sign = match d with | LocalAssum (_,t) -> let tj = infer_type env t in - let u = univ_of_sort tj.utj_type in + let u = Sorts.univ_of_sort tj.utj_type in (Universe.sup u lev, push_rel d env) | LocalDef _ -> lev, push_rel d env) @@ -199,8 +200,8 @@ let is_impredicative env u = let param_ccls paramsctxt = let fold acc = function | (LocalAssum (_, p)) -> - (let c = strip_prod_assum p in - match kind_of_term c with + (let c = Term.strip_prod_assum p in + match kind c with | Sort (Type u) -> Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc @@ -208,7 +209,7 @@ let param_ccls paramsctxt = List.fold_left fold [] paramsctxt (* Check arities and constructors *) -let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) numparams is_arity = +let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : types) numparams is_arity = let numchecked = ref 0 in let basic_check ev tp = if !numchecked < numparams then () else conv_leq ev tp (subst tp); @@ -264,13 +265,12 @@ let typecheck_inductive env mie = (* Check unicity of names *) mind_check_names mie; (* Params are typed-checked here *) - let univctx = + let env' = match mie.mind_entry_universes with - | Monomorphic_ind_entry ctx -> ctx - | Polymorphic_ind_entry ctx -> ctx - | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi + | Monomorphic_ind_entry ctx -> push_context_set ctx env + | Polymorphic_ind_entry ctx -> push_context ctx env + | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env in - let env' = push_context univctx env in let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in (* We first type arity of each inductive definition *) (* This allows building the environment of arities and to share *) @@ -288,7 +288,7 @@ let typecheck_inductive env mie = (** We have an algebraic universe as the conclusion of the arity, typecheck the dummy Π ctx, Prop and do a special case for the conclusion. *) - let proparity = infer_type env_params (mkArity (ctx, prop_sort)) in + let proparity = infer_type env_params (mkArity (ctx, Sorts.prop)) in let (cctx, _) = destArity proparity.utj_val in (* Any universe is well-formed, we don't need to check [s] here *) mkArity (cctx, s) @@ -350,7 +350,7 @@ let typecheck_inductive env mie = | None -> clev in let full_polymorphic () = - let defu = Term.univ_of_sort def_level in + let defu = Sorts.univ_of_sort def_level in let is_natural = type_in_type env || (UGraph.check_leq (universes env') infu defu) in @@ -468,7 +468,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = | LocalDef _ :: paramdecls -> check param_index (paramdecl_index+1) paramdecls | _::paramdecls -> - match kind_of_term (whd_all env params.(param_index)) with + match kind (whd_all env params.(param_index)) with | Rel w when Int.equal w paramdecl_index -> check (param_index-1) (paramdecl_index+1) paramdecls | _ -> @@ -495,7 +495,7 @@ if Int.equal nmr 0 then 0 else | (_,[]) -> assert false (* |paramsctxt|>=nmr *) | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt) | (p::lp,_::paramsctxt) -> - ( match kind_of_term (whd_all env p) with + ( match kind (whd_all env p) with | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt) | _ -> k) in find 0 (n-1) (lpar,List.rev paramsctxt) @@ -526,7 +526,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else let c' = whd_all env c in - match kind_of_term c' with + match kind c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in ienv_decompose_prod ienv' (n-1) b @@ -555,7 +555,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in (** If one of the inductives of the mutually inductive @@ -663,7 +663,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_all env c) in - match kind_of_term x with + match kind x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -746,7 +746,7 @@ let allowed_sorts is_smashed s = as well. *) all_sorts else - match family_of_sort s with + match Sorts.family s with (* Type: all elimination allowed: above and below *) | InType -> all_sorts (* Smashed Set is necessarily impredicative: forbids large elimination *) @@ -787,7 +787,7 @@ exception UndefinableExpansion a substitution of the form [params, x : ind params] *) let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params mind_consnrealdecls mind_consnrealargs paramslet ctx = - let mp, dp, l = repr_mind kn in + let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) @@ -915,11 +915,11 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r let ar = {template_param_levels = paramlevs; template_level = lev} in TemplateArity ar, all_sorts | RegularArity (info,ar,defs) -> - let s = sort_of_univ defs in + let s = Sorts.sort_of_univ defs in let kelim = allowed_sorts info s in let ar = RegularArity { mind_user_arity = Vars.subst_univs_level_constr substunivs ar; - mind_sort = sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in + mind_sort = Sorts.sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in ar, kelim in (* Assigning VM tags to constructors *) let nconst, nblock = ref 0, ref 0 in |