diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 45 |
1 files changed, 12 insertions, 33 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 80dc690422..dd49c4a1b7 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Vars -open Context open Declarations open Declareops open Environ @@ -77,7 +76,7 @@ let instantiate_params full t u args sign = let fail () = anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in let (rem_args, subs, ty) = - Context.fold_rel_context + Context.Rel.fold_outside (fun (_,copt,_) (largs,subs,ty) -> match (copt, largs, kind_of_term ty) with | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t) @@ -151,7 +150,7 @@ let remember_subst u subst = (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = +let make_subst env = let rec make subst = function | (_,Some _,_)::sign, exp, args -> make subst (sign, exp, args) @@ -270,18 +269,6 @@ let type_of_constructors (ind,u) (mib,mip) = (* Type of case predicates *) -let local_rels ctxt = - let (rels,_) = - Context.fold_rel_context_reverse - (fun (rels,n) (_,copt,_) -> - match copt with - None -> (mkRel n :: rels, n+1) - | Some _ -> (rels, n+1)) - ~init:([],1) - ctxt - in - rels - (* Get type of inductive, with parameters instantiated *) let inductive_sort_family mip = @@ -304,20 +291,12 @@ let is_primitive_record (mib,_) = | Some (Some _) -> true | _ -> false -let extended_rel_list n hyps = - let rec reln l p = function - | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps - | (_,Some _,_) :: hyps -> reln l (p+1) hyps - | [] -> l - in - reln [] 1 hyps - let build_dependent_inductive ind (_,mip) params = let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (mkIndU ind, List.map (lift mip.mind_nrealdecls) params - @ extended_rel_list 0 realargs) + @ Context.Rel.to_extended_list 0 realargs) (* This exception is local *) exception LocalArity of (sorts_family * sorts_family * arity_error) option @@ -369,22 +348,22 @@ let is_correct_arity env c pj ind specif params = let build_branches_type (ind,u) (_,mip as specif) params p = let build_one_branch i cty = let typi = full_constructor_instantiate (ind,u,specif,params) cty in - let (args,ccl) = decompose_prod_assum typi in - let nargs = rel_context_length args in + let (cstrsign,ccl) = decompose_prod_assum typi in + let nargs = Context.Rel.length cstrsign in let (_,allargs) = decompose_app ccl in let (lparams,vargs) = List.chop (inductive_params specif) allargs in let cargs = let cstr = ith_constructor_of_inductive ind (i+1) in - let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in + let dep_cstr = applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list 0 cstrsign)) in vargs @ [dep_cstr] in - let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in - it_mkProd_or_LetIn base args in + let base = lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in + it_mkProd_or_LetIn base cstrsign in Array.mapi build_one_branch mip.mind_nf_lc (* [p] is the predicate, [c] is the match object, [realargs] is the list of real args of the inductive type *) let build_case_type env n p c realargs = - whd_betaiota env (betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) + whd_betaiota env (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c]))) let type_case_branches env (pind,largs) pj c = let specif = lookup_mind_specif env (fst pind) in @@ -519,7 +498,7 @@ let subterm_var p renv = with Failure _ | Invalid_argument _ -> Not_subterm let push_ctxt_renv renv ctxt = - let n = rel_context_length ctxt in + let n = Context.Rel.length ctxt in { env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv } @@ -721,7 +700,7 @@ let restrict_spec env spec p = else let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) - if noccur_with_meta 1 (rel_context_length absctx) ar then spec + if noccur_with_meta 1 (Context.Rel.length absctx) ar then spec else let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in @@ -863,7 +842,7 @@ let filter_stack_domain env ci p stack = let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) - if noccur_with_meta 1 (rel_context_length absctx) ar then stack + if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = let t = whd_betadeltaiota env ar in |