summaryrefslogtreecommitdiff
path: root/checker/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/inductive.ml')
-rw-r--r--checker/inductive.ml352
1 files changed, 174 insertions, 178 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index b9964fe6..7a04cbfa 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductive.ml 10172 2007-10-04 13:02:03Z herbelin $ *)
-
open Util
open Names
open Univ
@@ -83,8 +81,6 @@ let instantiate_params full t args sign =
if rem_args <> [] then fail();
substl subs ty
-let instantiate_partial_params = instantiate_params false
-
let full_inductive_instantiate mib params sign =
let dummy = Prop Null in
let t = mkArity (sign,dummy) in
@@ -100,10 +96,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) =
(* Functions to build standard types related to inductive *)
-
-let number_of_inductives mib = Array.length mib.mind_packets
-let number_of_constructors mip = Array.length mip.mind_consnames
-
(*
Computing the actual sort of an applied or partially applied inductive type:
@@ -346,14 +338,14 @@ let type_case_branches env (ind,largs) (p,pj) c =
(************************************************************************)
-(* Checking the case annotation is relevent *)
+(* Checking the case annotation is relevant *)
let check_case_info env indsp ci =
let (mib,mip) = lookup_mind_specif env indsp in
if
not (eq_ind indsp ci.ci_ind) or
(mib.mind_nparams <> ci.ci_npar) or
- (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
+ (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls)
then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
(************************************************************************)
@@ -404,8 +396,10 @@ type subterm_spec =
| Dead_code
| Not_subterm
-let spec_of_tree t =
- if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
+let spec_of_tree t = lazy
+ (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec
+ then Not_subterm
+ else Subterm(Strict,Lazy.force t))
let subterm_spec_glb =
let glb2 s1 s2 =
@@ -440,7 +434,7 @@ let make_renv env minds recarg (kn,tyi) =
rel_min = recarg+2;
inds = minds;
recvec = mind_recvec;
- genv = [Lazy.lazy_from_val (Subterm(Large,mind_recvec.(tyi)))] }
+ genv = [Lazy.lazy_from_val(Subterm(Large,mind_recvec.(tyi)))] }
let push_var renv (x,ty,spec) =
{ renv with
@@ -459,10 +453,6 @@ 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,lazy (spec_of_tree (Lazy.force spec)))
-
let push_ctxt_renv renv ctxt =
let n = rel_context_length ctxt in
{ renv with
@@ -478,6 +468,15 @@ let push_fix_renv renv (_,v,_ as recdef) =
genv = iterate (fun ge -> Lazy.lazy_from_val 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
+
+let push_stack_closures renv l stack =
+ List.fold_right (fun h b -> (SClosure (renv,h))::b) l stack
+
+let push_stack_args l stack =
+ List.fold_right (fun h b -> (SArg h)::b) l stack
+
(******************************)
(* Computing the recursive subterms of a term (propagation of size
information through Cases). *)
@@ -497,60 +496,38 @@ let lookup_subterms env ind =
let (_,mip) = lookup_mind_specif env ind in
mip.mind_recargs
-(*********************************)
-
-let match_trees t1 t2 =
- let v1 = dest_subterms t1 in
- let v2 = dest_subterms t2 in
- array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) v1 v2
+let match_inductive ind ra =
+ match ra with
+ | (Mrec i | Imbr i) -> eq_ind ind i
+ | Norec -> false
-(* In {match c as z in ind y_s return P with |C_i x_s => t end}
- [branches_specif renv c_spec ind] returns an array of x_s specs given
- c_spec the spec of c. *)
-let branches_specif renv c_spec ind =
- let (_,mip) = lookup_mind_specif renv.env ind in
+(* 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 =
(* We fetch the regular tree associated to the inductive of the match.
This is just to get the number of constructors (and constructor
arities) that fit the match branches without forcing c_spec.
Note that c_spec might be more precise than [v] below, because of
nested inductive types. *)
+ 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
Array.mapi
(fun i nca -> (* i+1-th cstructor has arity nca *)
let lvra = lazy
(match Lazy.force c_spec with
- Subterm (_,t) when match_trees mip.mind_recargs t ->
+ Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
let vra = Array.of_list (dest_subterms t).(i) in
assert (nca = Array.length vra);
- Array.map spec_of_tree vra
+ Array.map
+ (fun t -> Lazy.force (spec_of_tree (lazy t)))
+ vra
| Dead_code -> Array.create nca Dead_code
| _ -> Array.create nca Not_subterm) in
list_tabulate (fun j -> lazy (Lazy.force lvra).(j)) nca)
- car
-
-(* 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 ind lbr =
- let vlrec = branches_specif renv c_spec ind in
- let rec push_branch_args renv lrec c =
- match lrec with
- ra::lr ->
- let c' = whd_betadeltaiota renv.env c in
- (match 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
- assert (Array.length vlrec = Array.length lbr);
- array_map2 (push_branch_args renv) vlrec 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
@@ -558,78 +535,88 @@ let case_branches_specif renv c_spec ind 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 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.lazy_from_val (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.ci_ind lbr
-
-(* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c =
- match subterm_specif renv c with
+ match 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 -> stack_element_specif h, t
+
+
+(* Check size x is a correct size for recursive calls. *)
+let check_is_subterm x =
+ match Lazy.force x with
Subterm (Strict,_) | Dead_code -> true
| _ -> false
@@ -637,7 +624,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 ->
@@ -647,7 +634,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))
@@ -659,48 +647,57 @@ 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 =
+ 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
- let (f,l) = decompose_app (whd_betaiotazeta renv.env t) in
+ let (f,l) = decompose_app (whd_betaiotazeta t) in
match f with
| Rel p ->
(* 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
- 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(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 :
- if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
+ if - g = fix g (y1:T1)...(yp:Tp) {struct yp} := e &
- f is guarded with respect to the set of pattern variables S
in a1 ... am &
- f is guarded with respect to the set of pattern variables S
@@ -710,81 +707,80 @@ let check_one_fix renv recpos def =
S+{yp} in e
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 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 inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 17:17:15 +0000