diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/constr.ml | 47 | ||||
| -rw-r--r-- | kernel/constr.mli | 23 | ||||
| -rw-r--r-- | kernel/inductive.ml | 67 |
3 files changed, 39 insertions, 98 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 3157ec9f57..bbaf95c9df 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -624,30 +624,6 @@ let map_branches_with_binders g f l ci bl = let map_return_predicate_with_binders g f l ci p = map_under_context_with_binders g f l (List.length ci.ci_pp_info.ind_tags) p -let rec map_under_context_with_full_binders g f l n d = - if n = 0 then f l d else - match kind d with - | LetIn (na,b,t,c) -> - let b' = f l b in - let t' = f l t in - let c' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalDef (na,b,t)) l) (n-1) c in - if b' == b && t' == t && c' == c then d - else mkLetIn (na,b',t',c') - | Lambda (na,t,b) -> - let t' = f l t in - let b' = map_under_context_with_full_binders g f (g (Context.Rel.Declaration.LocalAssum (na,t)) l) (n-1) b in - if t' == t && b' == b then d - else mkLambda (na,t',b') - | _ -> CErrors.anomaly (Pp.str "Ill-formed context") - -let map_branches_with_full_binders g f l ci bl = - let tags = Array.map List.length ci.ci_pp_info.cstr_tags in - let bl' = Array.map2 (map_under_context_with_full_binders g f l) tags bl in - if Array.for_all2 (==) bl' bl then bl else bl' - -let map_return_predicate_with_full_binders g f l ci p = - map_under_context_with_full_binders g f l (List.length ci.ci_pp_info.ind_tags) p - let map_invert f = function | NoInvert -> NoInvert | CaseInvert {univs;args;} as orig -> @@ -886,29 +862,6 @@ let liftn n k c = let lift n = liftn n 1 -let fold_with_full_binders g f n acc c = - let open Context.Rel.Declaration in - match kind c with - | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _ -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (_,c) -> f n acc c - | Evar (_,l) -> List.fold_left (f n) acc l - | Case (_,p,iv,c,bl) -> Array.fold_left (f n) (f n (fold_invert (f n) (f n acc p) iv) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | Array(_u,t,def,ty) -> f n (f n (Array.fold_left (f n) acc t) def) ty - - type 'univs instance_compare_fn = (GlobRef.t * int) option -> 'univs -> 'univs -> bool diff --git a/kernel/constr.mli b/kernel/constr.mli index 62f2555a7e..ed63ac507c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -478,25 +478,6 @@ val map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> val map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr -(** [map_under_context_with_full_binders g f n l c] is similar to - [map_under_context_with_binders] except that [g] takes also a full - binder as argument and that only the number of binders (and not - their signature) is required *) - -val map_under_context_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> int -> constr -> constr - -(** [map_branches_with_full_binders g f l br] is equivalent to - [map_branches_with_binders] but using - [map_under_context_with_full_binders] *) - -val map_branches_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr array -> constr array - -(** [map_return_predicate_with_full_binders g f l p] is equivalent to - [map_return_predicate_with_binders] but using - [map_under_context_with_full_binders] *) - -val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Declaration.pt -> 'a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_info -> constr -> constr - (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] @@ -505,10 +486,6 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a -val fold_with_full_binders : - (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> - 'a -> 'b -> constr -> 'b - val fold_invert : ('a -> 'b -> 'a) -> 'a -> ('b, 'c) case_invert -> 'a (** [map f c] maps [f] on the immediate subterms of [c]; it is diff --git a/kernel/inductive.ml b/kernel/inductive.ml index e34b3c0b47..ce12d65614 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -330,33 +330,45 @@ let check_allowed_sort ksort specif = let s = inductive_sort_family (snd specif) in raise (LocalArity (Some(elim_sort specif, ksort,s,error_elim_explain ksort s))) -let is_correct_arity env c pj ind specif params = +let check_correct_arity env c pj ind specif params = + (* We use l2r:true for compat with old versions which used CONV + instead of CUMUL called with arguments flipped. It is relevant + for performance eg in bedrock / Kami. *) let arsign,_ = get_instantiated_arity ind specif params in - let rec srec env pt ar = + let rec srec env ar pt = let pt' = whd_all env pt in - match kind pt', ar with - | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - let () = - try conv env a1 a1' - with NotConvertible -> raise (LocalArity None) in - srec (push_rel (LocalAssum (na1,a1)) env) t ar' - (* The last Prod domain is the type of the scrutinee *) - | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (LocalAssum (na1,a1)) env in - let ksort = match kind (whd_all env' a2) with - | Sort s -> Sorts.family s - | _ -> raise (LocalArity None) in - let dep_ind = build_dependent_inductive ind specif params in - let _ = - try conv env a1 dep_ind - with NotConvertible -> raise (LocalArity None) in - check_allowed_sort ksort specif - | _, (LocalDef _ as d)::ar' -> - srec (push_rel d env) (lift 1 pt') ar' - | _ -> - raise (LocalArity None) + match ar, kind pt' with + | (LocalAssum (_,a1))::ar', Prod (na1,a1',t) -> + let () = + try conv_leq ~l2r:true env a1 a1' + with NotConvertible -> raise (LocalArity None) in + srec (push_rel (LocalAssum (na1,a1)) env) ar' t + (* The last Prod domain is the type of the scrutinee *) + | [], Prod (na1,a1',a2) -> + let env' = push_rel (LocalAssum (na1,a1')) env in + let ksort = match kind (whd_all env' a2) with + | Sort s -> Sorts.family s + | _ -> raise (LocalArity None) + in + let dep_ind = build_dependent_inductive ind specif params in + let () = + (* This ensures that the type of the scrutinee is <= the + inductive type declared in the predicate. *) + try conv_leq ~l2r:true env dep_ind a1' + with NotConvertible -> raise (LocalArity None) + in + let () = check_allowed_sort ksort specif in + (* We return the "higher" inductive universe instance from the predicate, + the branches must be typeable using these universes. + The find_rectype call cannot fail due to the cumulativity check above. *) + let (pind, _args) = find_rectype env a1' in + pind + | (LocalDef _ as d)::ar', _ -> + srec (push_rel d env) ar' (lift 1 pt') + | _ -> + raise (LocalArity None) in - try srec env pj.uj_type (List.rev arsign) + try srec env (List.rev arsign) pj.uj_type with LocalArity kinds -> error_elim_arity env ind c pj kinds @@ -387,17 +399,16 @@ let build_branches_type (ind,u) (_,mip as specif) params p = let build_case_type env n p c realargs = whd_betaiota env (Term.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 +let type_case_branches env ((ind, _ as pind),largs) pj c = + let specif = lookup_mind_specif env ind in let nparams = inductive_params specif in let (params,realargs) = List.chop nparams largs in let p = pj.uj_val in - let () = is_correct_arity env c pj pind specif params in + let pind = check_correct_arity env c pj pind specif params in let lc = build_branches_type pind specif params p in let ty = build_case_type env (snd specif).mind_nrealdecls p c realargs in (lc, ty) - (************************************************************************) (* Checking the case annotation is relevant *) |