One more optimization for guard checking of cofixpoints.

In check_one_cofix, we now avoid calling dest_subterms each time we meet a
constructor by storing both the current tree (needed for the new criterion)
and a precomputed array of trees for subterms.

1 files changed, 12 insertions, 11 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a69a2d7ca1..802e232c7a 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1113,7 +1113,7 @@ let rec codomain_is_coind env c =
 	  raise (CoFixGuardError (env, CodomainNotInductiveType b)))
 
 let check_one_cofix env nbfix def deftype =
-  let rec check_rec_call env alreadygrd n vlra  t =
+  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_betadeltaiota env t) in
       match kind_of_term c with
@@ -1125,7 +1125,7 @@ let check_one_cofix env nbfix def deftype =
             else if not(List.for_all (noccur_with_meta n nbfix) args) then
 	      raise (CoFixGuardError (env,NestedRecursiveOccurrences))
 	| Construct ((_,i as cstr_kn),u)  ->
-            let lra = (dest_subterms vlra).(i-1) in
+            let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
             let realargs = List.skipn mib.mind_nparams args in
@@ -1137,7 +1137,7 @@ let check_one_cofix env nbfix def deftype =
                     else raise (CoFixGuardError
 		                 (env,RecCallInNonRecArgOfConstructor t))
                   else begin
-                      check_rec_call env true n rar t;
+                      check_rec_call env true n rar (dest_subterms rar) t;
                       process_args_of_constr (lr, lrar)
 		    end
               | [],_ -> ()
@@ -1148,7 +1148,7 @@ let check_one_cofix env nbfix def deftype =
 	    let () = assert (List.is_empty args) in
             if noccur_with_meta n nbfix a then
               let env' = push_rel (x, None, a) env in
-              check_rec_call env' alreadygrd (n+1) vlra b
+              check_rec_call env' alreadygrd (n+1) tree vlra b
             else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
 
@@ -1158,8 +1158,8 @@ let check_one_cofix env nbfix def deftype =
 	      if Array.for_all (noccur_with_meta n nbfix) varit then
 		let nbfix = Array.length vdefs in
 		let env' = push_rec_types recdef env in
-		(Array.iter (check_rec_call env' alreadygrd (n+nbfix) vlra) vdefs;
-		 List.iter (check_rec_call env alreadygrd n vlra) args)
+		(Array.iter (check_rec_call env' alreadygrd (n+nbfix) tree vlra) vdefs;
+		 List.iter (check_rec_call env alreadygrd n tree vlra) args)
               else
 		raise (CoFixGuardError (env,RecCallInTypeOfDef c))
 	    else
@@ -1167,15 +1167,16 @@ let check_one_cofix env nbfix def deftype =
 
 	| Case (_,p,tm,vrest) ->
 	   begin
-	     let vlra = match restrict_spec env (Subterm (Strict, vlra)) p with
+	     let tree = match restrict_spec env (Subterm (Strict, tree)) p with
 	     | Dead_code -> assert false
-	     | Subterm (_, vlra') -> vlra'
+	     | Subterm (_, tree') -> tree'
 	     | _ -> raise (CoFixGuardError (env, ReturnPredicateNotCoInductive c))
 	     in
                if (noccur_with_meta n nbfix p) then
 		 if (noccur_with_meta n nbfix tm) then
 		   if (List.for_all (noccur_with_meta n nbfix) args) then
-		     Array.iter (check_rec_call env alreadygrd n vlra) vrest
+		     let vlra = dest_subterms tree in
+		     Array.iter (check_rec_call env alreadygrd n tree vlra) vrest
 		   else
 		     raise (CoFixGuardError (env,RecCallInCaseFun c))
 		 else
@@ -1186,13 +1187,13 @@ let check_one_cofix env nbfix def deftype =
 
 	| Meta _ -> ()
         | Evar _ ->
-	    List.iter (check_rec_call env alreadygrd n vlra) args
+	    List.iter (check_rec_call env alreadygrd n tree vlra) args
 
 	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in
 
   let ((mind, _),_) = codomain_is_coind env deftype in
   let vlra = lookup_subterms env mind in
-  check_rec_call env false 1 vlra def
+  check_rec_call env false 1 vlra (dest_subterms vlra) def
 
 (* The  function which checks that the whole block of definitions
    satisfies the guarded condition *)