[kernel] termination checking backtracks on stuck case

The strategy is to backtrack when a constant is in head
position: we first try to see if the arguments are guarded,
if not we unfold.

Since `Case` is represented as a head (rather than as a context
as the reduction machine does) we did not backtrack there
and reduce (including delta) the scrutinized in order to
fire the iota redex.

This commit adds a choice point in that specific case, and
reduces eagerly (not step by step) the scrutinized in case
of failure.

1 files changed, 24 insertions, 10 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 848ae65c51..cbdb393bd7 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -921,16 +921,30 @@ let check_one_fix renv recpos trees def =
               end
 		
         | Case (ci,p,c_0,lrest) ->
-            List.iter (check_rec_call renv []) (c_0::p::l);
-            (* compute the recarg information for the arguments of
-               each branch *)
-            let case_spec = branches_specif renv 
-	      (lazy_subterm_specif renv [] c_0) ci in
-	    let stack' = push_stack_closures renv l stack in
-            let stack' = filter_stack_domain renv.env p 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
+            begin try
+              List.iter (check_rec_call renv []) (c_0::p::l);
+              (* compute the recarg info for the arguments of each branch *)
+              let case_spec =
+                branches_specif renv (lazy_subterm_specif renv [] c_0) ci in
+              let stack' = push_stack_closures renv l stack in
+              let stack' = filter_stack_domain renv.env p stack' in
+              lrest |> Array.iteri (fun k br' ->
+                let stack_br = push_stack_args case_spec.(k) stack' in
+                check_rec_call renv stack_br br')
+            with (FixGuardError _ as exn) ->
+              let exn = CErrors.push exn in
+              (* we try hard to reduce the match away by looking for a
+                 constructor in c_0 (we unfold definitions too) *)
+              let c_0 = whd_all renv.env c_0 in
+              let hd, _ = decompose_app c_0 in
+              match kind hd with
+              | Construct _ ->
+                  (* the call to whd_betaiotazeta will reduce the
+                     apparent iota redex away *)
+                  check_rec_call renv []
+                    (Term.applist (mkCase (ci,p,c_0,lrest), l))
+              | _ -> Exninfo.iraise exn
+            end
 
         (* Enables to traverse Fixpoint definitions in a more intelligent
            way, ie, the rule :