summaryrefslogtreecommitdiff
path: root/checker/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/inductive.ml')
-rw-r--r--checker/inductive.ml93
1 files changed, 61 insertions, 32 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml
index a300af79..fcd69f26 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -429,7 +429,7 @@ type guard_env =
(* the recarg information of inductive family *)
recvec : wf_paths array;
(* dB of variables denoting subterms *)
- genv : subterm_spec list;
+ genv : subterm_spec Lazy.t list;
}
let make_renv env minds recarg (kn,tyi) =
@@ -440,7 +440,7 @@ let make_renv env minds recarg (kn,tyi) =
rel_min = recarg+2;
inds = minds;
recvec = mind_recvec;
- genv = [Subterm(Large,mind_recvec.(tyi))] }
+ genv = [Lazy.lazy_from_val (Subterm(Large,mind_recvec.(tyi)))] }
let push_var renv (x,ty,spec) =
{ renv with
@@ -452,30 +452,30 @@ let assign_var_spec renv (i,spec) =
{ renv with genv = list_assign renv.genv (i-1) spec }
let push_var_renv renv (x,ty) =
- push_var renv (x,ty,Not_subterm)
+ push_var renv (x,ty,Lazy.lazy_from_val Not_subterm)
(* Fetch recursive information about a variable p *)
let subterm_var p renv =
- try List.nth renv.genv (p-1)
+ 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)
+ 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
env = push_rel_context ctxt renv.env;
rel_min = renv.rel_min+n;
- genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+ genv = iterate (fun ge -> Lazy.lazy_from_val 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;
rel_min = renv.rel_min+n;
- genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
+ genv = iterate (fun ge -> Lazy.lazy_from_val Not_subterm::ge) n renv.genv }
(******************************)
@@ -499,12 +499,44 @@ let lookup_subterms env ind =
(*********************************)
+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
+
+(* 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
+ 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 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 ->
+ let vra = Array.of_list (dest_subterms t).(i) in
+ assert (nca = Array.length vra);
+ Array.map spec_of_tree 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 ->
@@ -516,17 +548,9 @@ let case_branches_specif renv c_spec ind lbr =
| _ -> (* branch not in eta-long form: cannot perform rec. calls *)
(renv,c'))
| [] -> (renv, c) in
- match c_spec with
- Subterm (_,t) ->
- let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
- assert (Array.length sub_spec = Array.length lbr);
- array_map2 (push_branch_args renv) sub_spec lbr
- | Dead_code ->
- let t = dest_subterms (lookup_subterms renv.env ind) in
- let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
- assert (Array.length sub_spec = Array.length lbr);
- array_map2 (push_branch_args renv) sub_spec lbr
- | Not_subterm -> Array.map (fun c -> (renv,c)) lbr
+ assert (Array.length vlrec = Array.length lbr);
+ array_map2 (push_branch_args renv) vlrec lbr
+
(* [subterm_specif renv t] computes the recursive structure of [t] and
compare its size with the size of the initial recursive argument of
@@ -541,14 +565,11 @@ let rec subterm_specif renv t =
| Rel k -> subterm_var k renv
| Case (ci,_,c,lbr) ->
- if Array.length lbr = 0 then Dead_code
- else
- let c_spec = subterm_specif renv c in
- let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in
- let stl =
- Array.map (fun (renv',br') -> subterm_specif renv' br')
- lbr_spec in
- subterm_spec_glb stl
+ 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
@@ -571,7 +592,8 @@ let rec subterm_specif renv t =
let renv' =
(* Why Strict here ? To be general, it could also be
Large... *)
- assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
+ 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
@@ -582,7 +604,7 @@ let rec subterm_specif renv t =
if List.length l < nbOfAbst then renv''
else
let theDecrArg = List.nth l decrArg in
- let arg_spec = subterm_specif renv theDecrArg in
+ let arg_spec = lazy_subterm_specif renv theDecrArg in
assign_var_spec renv'' (1, arg_spec) in
subterm_specif renv'' strippedBody)
@@ -596,7 +618,15 @@ let rec subterm_specif renv t =
(* 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
@@ -611,7 +641,7 @@ let error_illegal_rec_call renv fx arg =
let (_,le_vars,lt_vars) =
List.fold_left
(fun (i,le,lt) sbt ->
- match sbt with
+ match Lazy.force sbt with
(Subterm(Strict,_) | Dead_code) -> (i+1, le, i::lt)
| (Subterm(Large,_)) -> (i+1, i::le, lt)
| _ -> (i+1, le ,lt))
@@ -665,8 +695,7 @@ let check_one_fix renv recpos def =
List.iter (check_rec_call renv) (c_0::p::l);
(* compute the recarg information for the arguments of
each branch *)
- let c_spec = subterm_specif renv c_0 in
- let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in
+ let lbr = case_subterm_specif renv ci c_0 lrest in
Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
(* Enables to traverse Fixpoint definitions in a more intelligent
@@ -694,7 +723,7 @@ let check_one_fix renv recpos def =
(fun j body ->
if i=j then
let theDecrArg = List.nth l decrArg in
- let arg_spec = subterm_specif renv theDecrArg 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)
bodies
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-17 11:12:46 +0000