aboutsummaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r--kernel/inductive.ml169
1 files changed, 85 insertions, 84 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e3fb472be1..4d13a5fcb8 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1,16 +1,18 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open CErrors
open Util
open Names
open Univ
-open Term
+open Constr
open Vars
open Declarations
open Declareops
@@ -30,22 +32,22 @@ let lookup_mind_specif env (kn,tyi) =
let find_rectype env c =
let (t, l) = decompose_app (whd_all env c) in
- match kind_of_term t with
+ match kind t with
| Ind ind -> (ind, l)
| _ -> raise Not_found
let find_inductive env c =
let (t, l) = decompose_app (whd_all env c) in
- match kind_of_term t with
+ match kind t with
| Ind ind
- when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l)
+ when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> CoFinite -> (ind, l)
| _ -> raise Not_found
let find_coinductive env c =
let (t, l) = decompose_app (whd_all env c) in
- match kind_of_term t with
+ match kind t with
| Ind ind
- when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l)
+ when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == CoFinite -> (ind, l)
| _ -> raise Not_found
let inductive_params (mib,_) = mib.mind_nparams
@@ -54,9 +56,7 @@ let inductive_paramdecls (mib,u) =
Vars.subst_instance_context u mib.mind_params_ctxt
let instantiate_inductive_constraints mib u =
- let process auctx =
- Univ.UContext.constraints (Univ.subst_instance_context u auctx)
- in
+ let process auctx = Univ.AUContext.instantiate u auctx in
match mib.mind_universes with
| Monomorphic_ind _ -> Univ.Constraint.empty
| Polymorphic_ind auctx -> process auctx
@@ -83,7 +83,7 @@ let instantiate_params full t u args sign =
let (rem_args, subs, ty) =
Context.Rel.fold_outside
(fun decl (largs,subs,ty) ->
- match (decl, largs, kind_of_term ty) with
+ match (decl, largs, kind ty) with
| (LocalAssum _, a::args, Prod(_,_,t)) -> (args, a::subs, t)
| (LocalDef (_,b,_), _, LetIn(_,_,_,t)) ->
(largs, (substl subs (subst_instance_constr u b))::subs, t)
@@ -96,9 +96,9 @@ let instantiate_params full t u args sign =
substl subs ty
let full_inductive_instantiate mib u params sign =
- let dummy = prop_sort in
- let t = mkArity (Vars.subst_instance_context u sign,dummy) in
- fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+ let dummy = Sorts.prop in
+ let t = Term.mkArity (Vars.subst_instance_context u sign,dummy) in
+ fst (Term.destArity (instantiate_params true t u params mib.mind_params_ctxt))
let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
let inst_ind = constructor_instantiate mind u mib t in
@@ -130,11 +130,6 @@ where
Remark: Set (predicative) is encoded as Type(0)
*)
-let sort_as_univ = function
-| Type u -> u
-| Prop Null -> Universe.type0m
-| Prop Pos -> Universe.type0
-
(* Template polymorphism *)
(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
@@ -168,7 +163,7 @@ let make_subst env =
(* arity is a global level which, at typing time, will be enforce *)
(* to be greater than the level of the argument; this is probably *)
(* a useless extra constraint *)
- let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+ let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in
make (cons_subst u s subst) (sign, exp, args)
| LocalAssum (na,t) :: sign, Some u::exp, [] ->
(* No more argument here: we add the remaining universes to the *)
@@ -194,11 +189,11 @@ let instantiate_universes env ctx ar argsorts =
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
- if is_type0m_univ level then prop_sort
+ if is_type0m_univ level then Sorts.prop
(* Non singleton type not containing types are interpretable in Set *)
- else if is_type0_univ level then set_sort
+ else if is_type0_univ level then Sorts.set
(* This is a Type with constraints *)
- else Type level
+ else Sorts.Type level
in
(ctx, ty)
@@ -213,9 +208,9 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
(* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
the situation where a non-Prop singleton inductive becomes Prop
when applied to Prop params *)
- if not polyprop && not (is_type0m_univ ar.template_level) && is_prop_sort s
+ if not polyprop && not (is_type0m_univ ar.template_level) && Sorts.is_prop s
then raise (SingletonInductiveBecomesProp mip.mind_typename);
- mkArity (List.rev ctx,s)
+ Term.mkArity (List.rev ctx,s)
let type_of_inductive env pind =
type_of_inductive_gen env pind [||]
@@ -235,9 +230,9 @@ let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
(* The max of an array of universes *)
-let cumulate_constructor_univ u = function
- | Prop Null -> u
- | Prop Pos -> Universe.sup Universe.type0 u
+let cumulate_constructor_univ u = let open Sorts in function
+ | Prop -> u
+ | Set -> Universe.sup Universe.type0 u
| Type u' -> Universe.sup u u'
let max_inductive_sort =
@@ -278,8 +273,8 @@ let type_of_constructors (ind,u) (mib,mip) =
let inductive_sort_family mip =
match mip.mind_arity with
- | RegularArity s -> family_of_sort s.mind_sort
- | TemplateArity _ -> InType
+ | RegularArity s -> Sorts.family s.mind_sort
+ | TemplateArity _ -> Sorts.InType
let mind_arity mip =
mip.mind_arity_ctxt, inductive_sort_family mip
@@ -293,24 +288,25 @@ let elim_sorts (_,mip) = mip.mind_kelim
let is_private (mib,_) = mib.mind_private = Some true
let is_primitive_record (mib,_) =
match mib.mind_record with
- | Some (Some _) -> true
- | _ -> false
+ | PrimRecord _ -> true
+ | NotRecord | FakeRecord -> false
let build_dependent_inductive ind (_,mip) params =
let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
- applist
+ Term.applist
(mkIndU ind,
List.map (lift mip.mind_nrealdecls) params
@ Context.Rel.to_extended_list mkRel 0 realargs)
(* This exception is local *)
-exception LocalArity of (sorts_family * sorts_family * arity_error) option
+exception LocalArity of (Sorts.family * Sorts.family * arity_error) option
let check_allowed_sort ksort specif =
+ let open Sorts in
let eq_ksort s = match ksort, s with
| InProp, InProp | InSet, InSet | InType, InType -> true
| _ -> false in
- if not (List.exists eq_ksort (elim_sorts specif)) then
+ if not (CList.exists eq_ksort (elim_sorts specif)) then
let s = inductive_sort_family (snd specif) in
raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
@@ -318,7 +314,7 @@ let is_correct_arity env c pj ind specif params =
let arsign,_ = get_instantiated_arity ind specif params in
let rec srec env pt ar =
let pt' = whd_all env pt in
- match kind_of_term pt', ar with
+ match kind pt', ar with
| Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
let () =
try conv env a1 a1'
@@ -327,8 +323,8 @@ let is_correct_arity env c pj ind specif params =
(* 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_of_term (whd_all env' a2) with
- | Sort s -> family_of_sort s
+ 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 _ =
@@ -353,22 +349,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 (cstrsign,ccl) = decompose_prod_assum typi in
+ let (cstrsign,ccl) = Term.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@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in
+ let dep_cstr = Term.applist (mkConstructU (cstr,u),lparams@(Context.Rel.to_extended_list mkRel 0 cstrsign)) in
vargs @ [dep_cstr] 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
+ let base = Term.lambda_appvect_assum (mip.mind_nrealdecls+1) (lift nargs p) (Array.of_list cargs) in
+ Term.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 (lambda_appvect_assum (n+1) p (Array.of_list (realargs@[c])))
+ 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
@@ -591,7 +587,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
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
@@ -623,7 +619,7 @@ compute the number of recursive arguments. *)
let get_recargs_approx env tree ind args =
let rec build_recargs (env, ra_env as ienv) tree 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) ->
assert (List.is_empty largs);
build_recargs (ienv_push_var ienv (na, b, mk_norec)) tree d
@@ -682,7 +678,7 @@ let get_recargs_approx env tree ind args =
and build_recargs_constructors ienv trees c =
let rec recargs_constr_rec (env,ra_env as ienv) trees 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
@@ -711,7 +707,7 @@ let restrict_spec env spec p =
let arctx, s = dest_prod_assum env ar in
let env = push_rel_context arctx env in
let i,args = decompose_app (whd_all env s) in
- match kind_of_term i with
+ match kind i with
| Ind i ->
begin match spec with
| Dead_code -> spec
@@ -732,7 +728,7 @@ let restrict_spec env spec p =
let rec subterm_specif renv stack t =
(* maybe reduction is not always necessary! *)
let f,l = decompose_app (whd_all renv.env t) in
- match kind_of_term f with
+ match kind f with
| Rel k -> subterm_var k renv
| Case (ci,p,c,lbr) ->
let stack' = push_stack_closures renv l stack in
@@ -775,7 +771,7 @@ let rec subterm_specif renv stack t =
let decrArg = recindxs.(i) in
let theBody = bodies.(i) in
let nbOfAbst = decrArg+1 in
- let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
+ let sign,strippedBody = Term.decompose_lam_n_assum nbOfAbst theBody in
(* pushing the fix parameters *)
let stack' = push_stack_closures renv l stack in
let renv'' = push_ctxt_renv renv' sign in
@@ -789,7 +785,7 @@ let rec subterm_specif renv stack t =
| Lambda (x,a,b) ->
let () = assert (List.is_empty l) in
- let spec,stack' = extract_stack renv a stack in
+ let spec,stack' = extract_stack stack in
subterm_specif (push_var renv (x,a,spec)) stack' b
(* Metas and evars are considered OK *)
@@ -797,21 +793,21 @@ let rec subterm_specif renv stack t =
| Proj (p, c) ->
let subt = subterm_specif renv stack c in
- (match subt with
- | Subterm (s, wf) ->
- (* We take the subterm specs of the constructor of the record *)
- let wf_args = (dest_subterms wf).(0) in
- (* We extract the tree of the projected argument *)
- let kn = Projection.constant p in
- let cb = lookup_constant kn renv.env in
- let pb = Option.get cb.const_proj in
- let n = pb.proj_arg in
- Subterm (Strict, List.nth wf_args n)
- | Dead_code -> Dead_code
- | Not_subterm -> Not_subterm)
+ (match subt with
+ | Subterm (s, wf) ->
+ (* We take the subterm specs of the constructor of the record *)
+ let wf_args = (dest_subterms wf).(0) in
+ (* We extract the tree of the projected argument *)
+ let n = Projection.arg p in
+ spec_of_tree (List.nth wf_args n)
+ | Dead_code -> Dead_code
+ | Not_subterm -> Not_subterm)
+
+ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _ | Ind _
+ | Construct _ | CoFix _ -> Not_subterm
+
(* Other terms are not subterms *)
- | _ -> Not_subterm
and lazy_subterm_specif renv stack t =
lazy (subterm_specif renv stack t)
@@ -820,7 +816,7 @@ and stack_element_specif = function
|SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
|SArg x -> x
-and extract_stack renv a = function
+and extract_stack = function
| [] -> Lazy.from_val Not_subterm , []
| h::t -> stack_element_specif h, t
@@ -851,7 +847,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) =
let error_partial_apply renv fx =
raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
-let filter_stack_domain env ci p stack =
+let filter_stack_domain env 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. *)
@@ -859,11 +855,13 @@ let filter_stack_domain env ci p stack =
else let env = push_rel_context absctx env in
let rec filter_stack env ar stack =
let t = whd_all env ar in
- match stack, kind_of_term t with
+ match stack, kind t with
| elt :: stack', Prod (n,a,c0) ->
let d = LocalAssum (n,a) in
+ let ctx, a = dest_prod_assum env a in
+ let env = push_rel_context ctx env in
let ty, args = decompose_app (whd_all env a) in
- let elt = match kind_of_term ty with
+ let elt = match kind ty with
| Ind ind ->
let spec' = stack_element_specif elt in
(match (Lazy.force spec') with
@@ -894,7 +892,7 @@ let check_one_fix renv recpos trees def =
if noccur_with_meta renv.rel_min nfi t then ()
else
let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
- match kind_of_term f with
+ match kind f with
| Rel p ->
(* Test if [p] is a fixpoint (recursive call) *)
if renv.rel_min <= p && p < renv.rel_min+nfi then
@@ -924,7 +922,7 @@ let check_one_fix renv recpos trees def =
| LocalDef (_,c,_) ->
try List.iter (check_rec_call renv []) l
with FixGuardError _ ->
- check_rec_call renv stack (applist(lift p c,l))
+ check_rec_call renv stack (Term.applist(lift p c,l))
end
| Case (ci,p,c_0,lrest) ->
@@ -934,7 +932,7 @@ let check_one_fix renv recpos trees def =
let case_spec = branches_specif renv
(lazy_subterm_specif renv [] c_0) ci in
let stack' = push_stack_closures renv l stack in
- let stack' = filter_stack_domain renv.env ci p stack' in
+ let stack' = filter_stack_domain renv.env p stack' in
Array.iteri (fun k br' ->
let stack_br = push_stack_args case_spec.(k) stack' in
check_rec_call renv stack_br br') lrest
@@ -970,14 +968,14 @@ let check_one_fix renv recpos trees def =
if evaluable_constant kn renv.env then
try List.iter (check_rec_call renv []) l
with (FixGuardError _ ) ->
- let value = (applist(constant_value_in renv.env cu, l)) in
+ let value = (Term.applist(constant_value_in renv.env cu, l)) in
check_rec_call renv stack value
else List.iter (check_rec_call renv []) l
| Lambda (x,a,b) ->
let () = assert (List.is_empty l) in
check_rec_call renv [] a ;
- let spec, stack' = extract_stack renv a stack in
+ let spec, stack' = extract_stack stack in
check_rec_call (push_var renv (x,a,spec)) stack' b
| Prod (x,a,b) ->
@@ -1007,7 +1005,7 @@ let check_one_fix renv recpos trees def =
| LocalDef (_,c,_) ->
try List.iter (check_rec_call renv []) l
with (FixGuardError _) ->
- check_rec_call renv stack (applist(c,l))
+ check_rec_call renv stack (Term.applist(c,l))
end
| Sort _ ->
@@ -1022,7 +1020,7 @@ let check_one_fix renv recpos trees def =
if Int.equal decr 0 then
check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
else
- match kind_of_term body with
+ match kind body with
| Lambda (x,a,b) ->
check_rec_call renv [] a;
let renv' = push_var_renv renv (x,a) in
@@ -1053,7 +1051,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
(* check fi does not appear in the k+1 first abstractions,
gives the type of the k+1-eme abstraction (must be an inductive) *)
let rec check_occur env n def =
- match kind_of_term (whd_all env def) with
+ match kind (whd_all env def) with
| Lambda (x,a,b) ->
if noccur_with_meta n nbfix a then
let env' = push_rel (LocalAssum (x,a)) env in
@@ -1063,6 +1061,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
try find_inductive env a
with Not_found ->
raise_err env i (RecursionNotOnInductiveType a) in
+ let mib,_ = lookup_mind_specif env (out_punivs mind) in
+ if mib.mind_finite != Finite then
+ raise_err env i (RecursionNotOnInductiveType a);
(mind, (env', b))
else check_occur env' (n+1) b
else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.")
@@ -1094,8 +1095,8 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
()
(*
-let cfkey = Profile.declare_profile "check_fix";;
-let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
+let cfkey = CProfile.declare_profile "check_fix";;
+let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
*)
(************************************************************************)
@@ -1108,7 +1109,7 @@ let anomaly_ill_typed () =
let rec codomain_is_coind env c =
let b = whd_all env c in
- match kind_of_term b with
+ match kind b with
| Prod (x,a,b) ->
codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
| _ ->
@@ -1120,7 +1121,7 @@ let check_one_cofix env nbfix def deftype =
let rec check_rec_call env alreadygrd n tree vlra t =
if not (noccur_with_meta n nbfix t) then
let c,args = decompose_app (whd_all env t) in
- match kind_of_term c with
+ match kind c with
| Rel p when n <= p && p < n+nbfix ->
(* recursive call: must be guarded and no nested recursive
call allowed *)
@@ -1192,8 +1193,8 @@ let check_one_cofix env nbfix def deftype =
| Meta _ -> ()
| Evar _ ->
List.iter (check_rec_call env alreadygrd n tree vlra) args
-
- | _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
+ | Rel _ | Var _ | Sort _ | Cast _ | Prod _ | LetIn _ | App _ | Const _
+ | Ind _ | Fix _ | Proj _ -> raise (CoFixGuardError (env,NotGuardedForm t)) in
let ((mind, _),_) = codomain_is_coind env deftype in
let vlra = lookup_subterms env mind in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 12:34:37 +0000