aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declarations.mli2
-rw-r--r--kernel/indtypes.ml15
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/inductive.ml353
-rw-r--r--kernel/inductive.mli11
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/term_typing.ml2
-rw-r--r--kernel/term_typing.mli2
-rw-r--r--kernel/type_errors.ml2
-rw-r--r--kernel/type_errors.mli2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml2
-rw-r--r--pretyping/indrec.ml4
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--toplevel/himsg.ml4
16 files changed, 203 insertions, 208 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 4f98bb8b0..c7f808742 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -71,7 +71,7 @@ let subst_rel_context sub = list_smartmap (subst_rel_declaration sub)
type recarg =
| Norec
- | Mrec of int
+ | Mrec of inductive
| Imbr of inductive
let subst_recarg sub r = match r with
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 15c5350b0..3e8de34c4 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -51,7 +51,7 @@ val subst_const_body : substitution -> constant_body -> constant_body
type recarg =
| Norec
- | Mrec of int
+ | Mrec of inductive
| Imbr of inductive
val subst_recarg : substitution -> recarg -> recarg
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index a9f8fa7c6..c3d79ee4a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -402,7 +402,7 @@ let array_min nmr a = if nmr = 0 then 0 else
(* The recursive function that checks positivity and builds the list
of recursive arguments *)
-let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
+let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
let lparams = rel_context_length hyps in
let nmr = rel_context_nhyps hyps in
(* Checking the (strict) positivity of a constructor argument type [c] *)
@@ -446,6 +446,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
with Failure _ -> raise (IllFormedInd (LocalNonPos n)) in
(* If the inductive appears in the args (non params) then the
definition is not positive. *)
+
if not (List.for_all (noccur_between n ntypes) auxlargs) then
failwith_non_pos_list n ntypes auxlargs;
(* We do not deal with imbricated mutual inductive types *)
@@ -511,11 +512,11 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i nargs lcnames indlc =
in
let irecargs = Array.map snd irecargs_nmr
and nmr' = array_min nmr irecargs_nmr
- in (nmr', mk_paths (Mrec i) irecargs)
+ in (nmr', mk_paths (Mrec ind) irecargs)
-let check_positivity env_ar params inds =
+let check_positivity kn env_ar params inds =
let ntypes = Array.length inds in
- let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+ let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
let lra_ind = List.rev (Array.to_list rc) in
let lparams = rel_context_length params in
let nmr = rel_context_nhyps params in
@@ -524,7 +525,7 @@ let check_positivity env_ar params inds =
list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
let nargs = rel_context_nhyps sign - nmr in
- check_positivity_one ienv params i nargs lcnames lc
+ check_positivity_one ienv params (kn,i) nargs lcnames lc
in
let irecargs_nmr = Array.mapi check_one inds in
let irecargs = Array.map snd irecargs_nmr
@@ -655,11 +656,11 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
(************************************************************************)
(************************************************************************)
-let check_inductive env mie =
+let check_inductive env kn mie =
(* First type-check the inductive definition *)
let (env_ar, params, inds, cst) = typecheck_inductive env mie in
(* Then check positivity conditions *)
- let (nmr,recargs) = check_positivity env_ar params inds in
+ let (nmr,recargs) = check_positivity kn env_ar params inds in
(* Build the inductive packets *)
build_inductive env env_ar params mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs cst
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index a3867c6b8..40d6912c4 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -37,4 +37,4 @@ exception InductiveError of inductive_error
(** The following function does checks on inductive declarations. *)
val check_inductive :
- env -> mutual_inductive_entry -> mutual_inductive_body
+ env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9215ac0c6..f3f0e2217 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -438,27 +438,20 @@ type guard_env =
{ env : env;
(* dB of last fixpoint *)
rel_min : int;
- (* inductive of recarg of each fixpoint *)
- inds : inductive array;
- (* the recarg information of inductive family *)
- recvec : wf_paths array;
(* dB of variables denoting subterms *)
genv : subterm_spec Lazy.t list;
}
-let make_renv env minds recarg (kn,tyi) =
+let make_renv env recarg (kn,tyi) =
let mib = Environ.lookup_mind kn env in
let mind_recvec =
Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in
{ env = env;
rel_min = recarg+2;
- inds = minds;
- recvec = mind_recvec;
genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] }
let push_var renv (x,ty,spec) =
- { renv with
- env = push_rel (x,None,ty) renv.env;
+ { env = push_rel (x,None,ty) renv.env;
rel_min = renv.rel_min+1;
genv = spec:: renv.genv }
@@ -473,69 +466,43 @@ let subterm_var p renv =
try Lazy.force (List.nth renv.genv (p-1))
with Failure _ | Invalid_argument _ -> Not_subterm
-(* Add a variable and mark it as strictly smaller with information [spec]. *)
-let add_subterm renv (x,a,spec) =
- push_var renv (x,a,spec_of_tree spec)
-
let push_ctxt_renv renv ctxt =
let n = rel_context_length ctxt in
- { renv with
- env = push_rel_context ctxt renv.env;
+ { env = push_rel_context ctxt renv.env;
rel_min = renv.rel_min+n;
genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv }
let push_fix_renv renv (_,v,_ as recdef) =
let n = Array.length v in
- { renv with
- env = push_rec_types recdef renv.env;
+ { env = push_rec_types recdef renv.env;
rel_min = renv.rel_min+n;
genv = iterate (fun ge -> lazy Not_subterm::ge) n renv.genv }
+(* Definition and manipulation of the stack *)
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
-(******************************)
-(* Computing the recursive subterms of a term (propagation of size
- information through Cases). *)
+let push_stack_closures renv l stack =
+ List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack
-(*
- c is a branch of an inductive definition corresponding to the spec
- lrec. mind_recvec is the recursive spec of the inductive
- definition of the decreasing argument n.
-
- case_branches_specif renv lrec lc will pass the lambdas
- of c corresponding to pattern variables and collect possibly new
- subterms variables and returns the bodies of the branches with the
- correct envs and decreasing args.
-*)
+let push_stack_args l stack =
+ List.fold_right (fun h b -> (SArg h)::b) l stack
+
+(******************************)
+(* {6 Computing the recursive subterms of a term (propagation of size
+ information through Cases).} *)
let lookup_subterms env ind =
let (_,mip) = lookup_mind_specif env ind in
mip.mind_recargs
-(*********************************)
-
-(* Propagation of size information through Cases: if the matched
- object is a recursive subterm then compute the information
- associated to its own subterms.
- Rq: if branch is not eta-long, then the recursive information
- is not propagated to the missing abstractions *)
-let case_branches_specif renv c_spec ci lbr =
- let car =
+(* In {match c as z in ci y_s return P with |C_i x_s => t end}
+ [branches_specif renv c_spec ci] returns an array of x_s specs knowing
+ c_spec. *)
+let branches_specif renv c_spec ci =
+ let car =
let (_,mip) = lookup_mind_specif renv.env ci.ci_ind in
let v = dest_subterms mip.mind_recargs in
- Array.map List.length v in
- let rec push_branch_args renv lrec c =
- match lrec with
- ra::lr ->
- let c' = whd_betadeltaiota renv.env c in
- (match kind_of_term c' with
- Lambda(x,a,b) ->
- let renv' = push_var renv (x,a,ra) in
- push_branch_args renv' lr b
- | _ -> (* branch not in eta-long form: cannot perform rec. calls *)
- (renv,c'))
- | [] -> (renv, c) in
-
- let sub_spec =
+ Array.map List.length v in
Array.mapi
(fun i nca -> (* i+1-th cstructor has arity nca *)
let cs = lazy
@@ -546,9 +513,7 @@ let case_branches_specif renv c_spec ci lbr =
| Dead_code -> Array.create nca (lazy Dead_code)
| Not_subterm -> Array.create nca (lazy Not_subterm)) in
list_tabulate (fun j -> (Lazy.force cs).(j)) nca)
- car in
- assert (Array.length sub_spec = Array.length lbr);
- array_map2 (push_branch_args renv) sub_spec lbr
+ car
(* [subterm_specif renv t] computes the recursive structure of [t] and
compare its size with the size of the initial recursive argument of
@@ -556,78 +521,98 @@ let case_branches_specif renv c_spec ci lbr =
about variables.
*)
-let rec subterm_specif renv t =
+let rec subterm_specif renv stack t =
(* maybe reduction is not always necessary! *)
let f,l = decompose_app (whd_betadeltaiota renv.env t) in
- match kind_of_term f with
- | Rel k -> subterm_var k renv
-
- | Case (ci,_,c,lbr) ->
- let lbr_spec = case_subterm_specif renv ci c lbr in
- let stl =
- Array.map (fun (renv',br') -> subterm_specif renv' br')
- lbr_spec in
- subterm_spec_glb stl
-
- | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
-(* when proving that the fixpoint f(x)=e is less than n, it is enough
- to prove that e is less than n assuming f is less than n
- furthermore when f is applied to a term which is strictly less than
- n, one may assume that x itself is strictly less than n
-*)
- let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
- let oind =
- let env' = push_rel_context ctxt renv.env in
- try Some(fst(find_inductive env' clfix))
- with Not_found -> None in
- (match oind with
- None -> Not_subterm (* happens if fix is polymorphic *)
- | Some ind ->
- let nbfix = Array.length typarray in
- let recargs = lookup_subterms renv.env ind in
- (* pushing the fixpoints *)
- let renv' = push_fix_renv renv recdef in
- let renv' =
- (* Why Strict here ? To be general, it could also be
- Large... *)
- assign_var_spec renv'
- (nbfix-i, lazy (Subterm(Strict,recargs))) in
- 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
- (* pushing the fix parameters *)
- let renv'' = push_ctxt_renv renv' sign in
- let renv'' =
- if List.length l < nbOfAbst then renv''
- else
- let theDecrArg = List.nth l decrArg in
- let arg_spec = lazy_subterm_specif renv theDecrArg in
- assign_var_spec renv'' (1, arg_spec) in
- subterm_specif renv'' strippedBody)
-
- | Lambda (x,a,b) ->
- assert (l=[]);
- subterm_specif (push_var_renv renv (x,a)) b
-
- (* Metas and evars are considered OK *)
- | (Meta _|Evar _) -> Dead_code
-
- (* Other terms are not subterms *)
- | _ -> Not_subterm
-
-and lazy_subterm_specif renv t =
- lazy (subterm_specif renv t)
-
-and case_subterm_specif renv ci c lbr =
- if Array.length lbr = 0 then [||]
- else
- let c_spec = lazy_subterm_specif renv c in
- case_branches_specif renv c_spec ci lbr
-
+ match kind_of_term f with
+ | Rel k -> subterm_var k renv
+
+ | Case (ci,_,c,lbr) ->
+ let stack' = push_stack_closures renv l stack in
+ let cases_spec = branches_specif renv
+ (lazy_subterm_specif renv [] c) ci in
+ let stl =
+ Array.mapi (fun i br' ->
+ let stack_br = push_stack_args (cases_spec.(i)) stack' in
+ subterm_specif renv stack_br br')
+ lbr in
+ subterm_spec_glb stl
+
+ | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
+ (* when proving that the fixpoint f(x)=e is less than n, it is enough
+ to prove that e is less than n assuming f is less than n
+ furthermore when f is applied to a term which is strictly less than
+ n, one may assume that x itself is strictly less than n
+ *)
+ let (ctxt,clfix) = dest_prod renv.env typarray.(i) in
+ let oind =
+ let env' = push_rel_context ctxt renv.env in
+ try Some(fst(find_inductive env' clfix))
+ with Not_found -> None in
+ (match oind with
+ None -> Not_subterm (* happens if fix is polymorphic *)
+ | Some ind ->
+ let nbfix = Array.length typarray in
+ let recargs = lookup_subterms renv.env ind in
+ (* pushing the fixpoints *)
+ let renv' = push_fix_renv renv recdef in
+ let renv' =
+ (* Why Strict here ? To be general, it could also be
+ Large... *)
+ assign_var_spec renv'
+ (nbfix-i, lazy (Subterm(Strict,recargs))) in
+ 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
+ (* pushing the fix parameters *)
+ let stack' = push_stack_closures renv l stack in
+ let renv'' = push_ctxt_renv renv' sign in
+ let renv'' =
+ if List.length stack' < nbOfAbst then renv''
+ else
+ let decrArg = List.nth stack' decrArg in
+ let arg_spec = stack_element_specif decrArg in
+ assign_var_spec renv'' (1, arg_spec) in
+ subterm_specif renv'' [] strippedBody)
+
+ | Lambda (x,a,b) ->
+ assert (l=[]);
+ let spec,stack' = extract_stack renv a stack in
+ subterm_specif (push_var renv (x,a,spec)) stack' b
+
+ (* Metas and evars are considered OK *)
+ | (Meta _|Evar _) -> Dead_code
+
+ (* Other terms are not subterms *)
+ | _ -> Not_subterm
+
+and lazy_subterm_specif renv stack t =
+ lazy (subterm_specif renv stack t)
+
+and stack_element_specif = function
+ |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
+ |SArg x -> x
+
+and extract_stack renv a = function
+ |[] -> Lazy.lazy_from_val Not_subterm , []
+ |h::t -> lazy ((* because commutavive cuts are not compatible with typing,
+ arg_spec must carry the good wf_path *)
+ match Lazy.force (stack_element_specif h) with
+ |Subterm(k,wpath) as spec -> begin
+ try let (inda,_) = find_inductive renv.env a in
+ match fst (Rtree.dest_node wpath) with
+ |Norec -> assert false
+ |(Mrec ind | Imbr ind) -> if inda = ind then spec else Dead_code
+ with |Not_found -> Dead_code
+ (* Something not of inductive type cannot be used as
+ fixpoint recursive argument *)
+ end
+ |_ as spec -> spec) , t
+
(* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c =
- match subterm_specif renv c with
+let check_is_subterm x =
+ match Lazy.force x with
Subterm (Strict,_) | Dead_code -> true
| _ -> false
@@ -635,7 +620,7 @@ let check_is_subterm renv c =
exception FixGuardError of env * guard_error
-let error_illegal_rec_call renv fx arg =
+let error_illegal_rec_call renv fx (arg_renv,arg) =
let (_,le_vars,lt_vars) =
List.fold_left
(fun (i,le,lt) sbt ->
@@ -645,7 +630,8 @@ let error_illegal_rec_call renv fx arg =
| _ -> (i+1, le ,lt))
(1,[],[]) renv.genv in
raise (FixGuardError (renv.env,
- RecursionOnIllegalTerm(fx,arg,le_vars,lt_vars)))
+ RecursionOnIllegalTerm(fx,(arg_renv.env, arg),
+ le_vars,lt_vars)))
let error_partial_apply renv fx =
raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
@@ -656,8 +642,11 @@ let error_partial_apply renv fx =
let check_one_fix renv recpos def =
let nfi = Array.length recpos in
- (* Checks if [t] only make valid recursive calls *)
- let rec check_rec_call renv t =
+ (* Checks if [t] only make valid recursive calls
+ [stack] is the list of constructor's argument specification and
+ arguments than will be applied after reduction.
+ example u in t where we have (match .. with |.. => t end) u *)
+ let rec check_rec_call renv stack t =
(* if [t] does not make recursive calls, it is guarded: *)
if noccur_with_meta renv.rel_min nfi t then ()
else
@@ -667,35 +656,43 @@ let check_one_fix renv recpos def =
(* Test if [p] is a fixpoint (recursive call) *)
if renv.rel_min <= p & p < renv.rel_min+nfi then
begin
- List.iter (check_rec_call renv) l;
+ List.iter (check_rec_call renv []) l;
(* the position of the invoked fixpoint: *)
let glob = renv.rel_min+nfi-1-p in
(* the decreasing arg of the rec call: *)
let np = recpos.(glob) in
- if List.length l <= np then error_partial_apply renv glob
+ let stack' = push_stack_closures renv l stack in
+ if List.length stack' <= np then error_partial_apply renv glob
else
(* Check the decreasing arg is smaller *)
- let z = List.nth l np in
- if not (check_is_subterm renv z) then
- error_illegal_rec_call renv glob z
+ let z = List.nth stack' np in
+ if not (check_is_subterm (stack_element_specif z)) then
+ begin match z with
+ |SClosure (z,z') -> error_illegal_rec_call renv glob (z,z')
+ |SArg _ -> error_partial_apply renv glob
+ end
end
else
begin
match pi2 (lookup_rel p renv.env) with
| None ->
- List.iter (check_rec_call renv) l
+ List.iter (check_rec_call renv []) l
| Some c ->
- try List.iter (check_rec_call renv) l
+ try List.iter (check_rec_call renv []) l
with FixGuardError _ ->
- check_rec_call renv (applist(lift p c,l))
+ check_rec_call renv stack (applist(lift p c,l))
end
-
+
| Case (ci,p,c_0,lrest) ->
- List.iter (check_rec_call renv) (c_0::p::l);
+ List.iter (check_rec_call renv []) (c_0::p::l);
(* compute the recarg information for the arguments of
each branch *)
- let lbr = case_subterm_specif renv ci c_0 lrest in
- Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
+ let case_spec = branches_specif renv
+ (lazy_subterm_specif renv [] c_0) ci in
+ let stack' = push_stack_closures renv l 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
(* Enables to traverse Fixpoint definitions in a more intelligent
way, ie, the rule :
@@ -710,79 +707,79 @@ let check_one_fix renv recpos def =
then f is guarded with respect to S in (g a1 ... am).
Eduardo 7/9/98 *)
| Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
- List.iter (check_rec_call renv) l;
- Array.iter (check_rec_call renv) typarray;
+ List.iter (check_rec_call renv []) l;
+ Array.iter (check_rec_call renv []) typarray;
let decrArg = recindxs.(i) in
let renv' = push_fix_renv renv recdef in
- if (List.length l < (decrArg+1)) then
- Array.iter (check_rec_call renv') bodies
- else
+ let stack' = push_stack_closures renv l stack in
Array.iteri
(fun j body ->
- if i=j then
- let theDecrArg = List.nth l decrArg in
- let arg_spec = lazy_subterm_specif renv theDecrArg in
- check_nested_fix_body renv' (decrArg+1) arg_spec body
- else check_rec_call renv' body)
+ if i=j && (List.length stack' > decrArg) then
+ let recArg = List.nth stack' decrArg in
+ let arg_sp = stack_element_specif recArg in
+ check_nested_fix_body renv' (decrArg+1) arg_sp body
+ else check_rec_call renv' [] body)
bodies
| Const kn ->
if evaluable_constant kn renv.env then
- try List.iter (check_rec_call renv) l
+ try List.iter (check_rec_call renv []) l
with (FixGuardError _ ) ->
- check_rec_call renv(applist(constant_value renv.env kn, l))
- else List.iter (check_rec_call renv) l
-
- (* The cases below simply check recursively the condition on the
- subterms *)
- | Cast (a,_, b) ->
- List.iter (check_rec_call renv) (a::b::l)
+ let value = (applist(constant_value renv.env kn, l)) in
+ check_rec_call renv stack value
+ else List.iter (check_rec_call renv []) l
| Lambda (x,a,b) ->
- List.iter (check_rec_call renv) (a::l);
- check_rec_call (push_var_renv renv (x,a)) b
+ assert (l = []);
+ check_rec_call renv [] a ;
+ let spec, stack' = extract_stack renv a stack in
+ check_rec_call (push_var renv (x,a,spec)) stack' b
| Prod (x,a,b) ->
- List.iter (check_rec_call renv) (a::l);
- check_rec_call (push_var_renv renv (x,a)) b
+ assert (l = [] && stack = []);
+ check_rec_call renv [] a;
+ check_rec_call (push_var_renv renv (x,a)) [] b
| CoFix (i,(_,typarray,bodies as recdef)) ->
- List.iter (check_rec_call renv) l;
- Array.iter (check_rec_call renv) typarray;
+ List.iter (check_rec_call renv []) l;
+ Array.iter (check_rec_call renv []) typarray;
let renv' = push_fix_renv renv recdef in
- Array.iter (check_rec_call renv') bodies
+ Array.iter (check_rec_call renv' []) bodies
- | (Ind _ | Construct _ | Sort _) ->
- List.iter (check_rec_call renv) l
+ | (Ind _ | Construct _) ->
+ List.iter (check_rec_call renv []) l
| Var id ->
begin
match pi2 (lookup_named id renv.env) with
| None ->
- List.iter (check_rec_call renv) l
+ List.iter (check_rec_call renv []) l
| Some c ->
- try List.iter (check_rec_call renv) l
- with (FixGuardError _) -> check_rec_call renv (applist(c,l))
+ try List.iter (check_rec_call renv []) l
+ with (FixGuardError _) ->
+ check_rec_call renv stack (applist(c,l))
end
+ | Sort _ -> assert (l = [])
+
(* l is not checked because it is considered as the meta's context *)
| (Evar _ | Meta _) -> ()
- | (App _ | LetIn _) -> assert false (* beta zeta reduction *)
+ | (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
and check_nested_fix_body renv decr recArgsDecrArg body =
if decr = 0 then
- check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) body
+ check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
else
match kind_of_term body with
| Lambda (x,a,b) ->
- check_rec_call renv a;
+ check_rec_call renv [] a;
let renv' = push_var_renv renv (x,a) in
- check_nested_fix_body renv' (decr-1) recArgsDecrArg b
+ check_nested_fix_body renv' (decr-1) recArgsDecrArg b
| _ -> anomaly "Not enough abstractions in fix body"
-
+
in
- check_rec_call renv def
+ check_rec_call renv [] def
let judgment_of_fixpoint (_, types, bodies) =
array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
@@ -829,7 +826,7 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
let (minds, rdef) = inductive_of_mutfix env fix in
for i = 0 to Array.length bodies - 1 do
let (fenv,body) = rdef.(i) in
- let renv = make_renv fenv minds nvect.(i) minds.(i) in
+ let renv = make_renv fenv nvect.(i) minds.(i) in
try check_one_fix renv nvect body
with FixGuardError (fixenv,err) ->
error_ill_formed_rec_body fixenv err names i
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3212b8eed..202b1aa4c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -101,14 +101,11 @@ type guard_env =
{ env : env;
(** dB of last fixpoint *)
rel_min : int;
- (** inductive of recarg of each fixpoint *)
- inds : inductive array;
- (** the recarg information of inductive family *)
- recvec : wf_paths array;
(** dB of variables denoting subterms *)
genv : subterm_spec Lazy.t list;
}
-val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec Lazy.t -> case_info ->
- constr array -> (guard_env * constr) array
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+
+val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
+
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6a18f72d5..7e910c360 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -294,9 +294,9 @@ let add_mind dir l mie senv =
check_label l senv.labset;
(* TODO: when we will allow reorderings we will have to verify
all labels *)
- let mib = translate_mind senv.env mie in
- let senv' = add_constraints mib.mind_constraints senv in
let kn = make_mind senv.modinfo.modpath dir l in
+ let mib = translate_mind senv.env kn mie in
+ let senv' = add_constraints mib.mind_constraints senv in
let env'' = Environ.add_mind kn mib senv'.env in
kn, { old = senv'.old;
env = env'';
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index da3393065..2189db264 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -138,4 +138,4 @@ let translate_recipe env kn r =
(* Insertion of inductive types. *)
-let translate_mind env mie = check_inductive env mie
+let translate_mind env kn mie = check_inductive env kn mie
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 49463e75a..dbf479a0c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -31,7 +31,7 @@ val build_constant_declaration : env -> 'a ->
val translate_constant : env -> constant -> constant_entry -> constant_body
val translate_mind :
- env -> mutual_inductive_entry -> mutual_inductive_body
+ env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
val translate_recipe :
env -> constant -> Cooking.recipe -> constant_body
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 77b69bb88..c9f9fe7ad 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -18,7 +18,7 @@ type guard_error =
(* Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of constr
- | RecursionOnIllegalTerm of int * constr * int list * int list
+ | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(* CoFixpoints *)
| CodomainNotInductiveType of constr
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index dabff8360..3a6ad4bb1 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -18,7 +18,7 @@ type guard_error =
(** Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of constr
- | RecursionOnIllegalTerm of int * constr * int list * int list
+ | RecursionOnIllegalTerm of int * (env * constr) * int list * int list
| NotEnoughArgumentsForFixCall of int
(** CoFixpoints *)
| CodomainNotInductiveType of constr
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 97a56cabe..aadd04547 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -806,7 +806,7 @@ let is_rec_pos (main_ind,wft) =
None -> false
| Some index ->
match fst (Rtree.dest_node wft) with
- Mrec i when i = index -> true
+ Mrec (_,i) when i = index -> true
| _ -> false
let rec constr_trees (main_ind,wft) ind =
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 1daae0236..a6f5a729a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -153,7 +153,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
| [] -> None,[]
| ra::rest ->
(match dest_recarg ra with
- | Mrec j when is_rec -> (depPvect.(j),rest)
+ | Mrec (_,j) when is_rec -> (depPvect.(j),rest)
| Imbr _ ->
Flags.if_verbose warning "Ignoring recursive call";
(None,rest)
@@ -223,7 +223,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
match dest_recarg recarg with
| Norec -> None
| Imbr _ -> None
- | Mrec i -> fvect.(i)
+ | Mrec (_,i) -> fvect.(i)
in
(match optionpos with
| None ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 07447c540..1a5882f4f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -76,7 +76,7 @@ let mis_is_recursive_subset listind rarg =
List.exists
(fun ra ->
match dest_recarg ra with
- | Mrec i -> List.mem i listind
+ | Mrec (_,i) -> List.mem i listind
| _ -> false) rvec
in
array_exists one_is_rec (dest_subterms rarg)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 1ff67bffe..7878b5154 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -290,7 +290,7 @@ let compute_construtor_signatures isrec (_,k as ity) =
| Prod (_,_,c), recarg::rest ->
let b = match dest_recarg recarg with
| Norec | Imbr _ -> false
- | Mrec j -> isrec & j=k
+ | Mrec (_,j) -> isrec & j=k
in b :: (analrec c rest)
| LetIn (_,_,_,c), rest -> false :: (analrec c rest)
| _, [] -> []
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 6c8847ff9..8fcf15608 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -227,7 +227,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
| RecursionNotOnInductiveType c ->
str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++
str "which should be an inductive type"
- | RecursionOnIllegalTerm(j,arg,le,lt) ->
+ | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) ->
let called =
match names.(j) with
Name id -> pr_id id
@@ -245,7 +245,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
prlist_with_sep pr_spc pr_db lt in
str "Recursive call to " ++ called ++ spc () ++
strbrk "has principal argument equal to" ++ spc () ++
- pr_lconstr_env env arg ++ strbrk " instead of " ++ vars
+ pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars
| NotEnoughArgumentsForFixCall j ->
let called =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 16:28:46 +0000