diff options
| -rw-r--r-- | kernel/inductive.ml | 71 | ||||
| -rw-r--r-- | kernel/inductive.mli | 4 | ||||
| -rw-r--r-- | test-suite/complexity/guard.v | 17 |
3 files changed, 60 insertions, 32 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8b5649dfb..d806c39a0 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -418,14 +418,16 @@ 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 = - match s1,s2 with - _, Dead_code -> s1 - | Dead_code, _ -> s2 + let glb2 s1 s2 = + match s1, s2 with + s1, Dead_code -> s1 + | Dead_code, s2 -> s2 | Not_subterm, _ -> Not_subterm | _, Not_subterm -> Not_subterm | Subterm (a1,t1), Subterm (a2,t2) -> @@ -443,7 +445,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) = @@ -454,7 +456,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 @@ -466,11 +468,11 @@ 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 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]. *) @@ -482,14 +484,14 @@ let push_ctxt_renv renv ctxt = { 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 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 Not_subterm::ge) n renv.genv } (******************************) @@ -518,7 +520,8 @@ let lookup_subterms env ind = 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 case_branches_specif renv c_spec ci lbr = + let ind = ci.ci_ind in let rec push_branch_args renv lrec c = match lrec with ra::lr -> @@ -530,17 +533,21 @@ 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 + + let sub_spec = + Array.mapi + (fun i nca -> (* i+1-th cstructor has arity nca *) + let cs = lazy + (match Lazy.force c_spec with + Subterm (_,t) -> + Array.map (fun t -> spec_of_tree (lazy t)) + (Array.of_list (dest_subterms t).(i)) + | 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) + ci.ci_cstr_nargs in + assert (Array.length sub_spec = Array.length lbr); + array_map2 (push_branch_args renv) sub_spec lbr (* [subterm_specif renv t] computes the recursive structure of [t] and compare its size with the size of the initial recursive argument of @@ -582,7 +589,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 (Subterm(Strict,recargs))) in let decrArg = recindxs.(i) in let theBody = bodies.(i) in let nbOfAbst = decrArg+1 in @@ -593,7 +601,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) @@ -607,11 +615,14 @@ 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 = subterm_specif renv c in - case_branches_specif renv c_spec ci.ci_ind lbr + let c_spec = lazy_subterm_specif renv c in + case_branches_specif renv c_spec ci lbr (* Check term c can be applied to one of the mutual fixpoints. *) let check_is_subterm renv c = @@ -627,7 +638,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)) @@ -709,7 +720,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 diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 9f8d10900..8fe8eb11f 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -109,9 +109,9 @@ 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; } val subterm_specif : guard_env -> constr -> subterm_spec -val case_branches_specif : guard_env -> subterm_spec -> inductive -> +val case_branches_specif : guard_env -> subterm_spec Lazy.t -> case_info -> constr array -> (guard_env * constr) array diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v new file mode 100644 index 000000000..f64ffc259 --- /dev/null +++ b/test-suite/complexity/guard.v @@ -0,0 +1,17 @@ +(* Examples to check that the guard condition does not unfold + irrelevant subterms *) +(* Expected time < 1s *) +Require Import Bool. + +Fixpoint slow n := + match n with + | 0 => true + | S k => andb (slow k) (slow k) + end. + +Timeout 5 Time Fixpoint F n := + match n with + | 0 => 0 + | S k => + if slow 100 then F k else 0 + end. |