Tentative fix for the commutative cut subterm rule.

Some fixpoints are now rejected in the standard library, but that's probably
because we compare trees for equality instead of intersecting them.

1 files changed, 35 insertions, 7 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 7698eed0f..24763b79e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -611,16 +611,14 @@ let check_inductive_codomain env p =
   isInd i
 
 let get_codomain_tree env p =
-  let absctx, ar = dest_lam_assum env p in
-  let arctx, s = dest_prod_assum env ar in
+  let absctx, ar = dest_lam_assum env p in (* TODO: reduce or preserve lets? *)
+  let arctx, s = dest_prod_assum env ar in (* TODO: check number of prods *)
   let i,l' = decompose_app (whd_betadeltaiota env s) in
   match kind_of_term i with
   | Ind i ->
     let (_,mip) = lookup_mind_specif env i in Subterm(Strict,mip.mind_recargs)
   | _ -> Not_subterm
 
-
-
 (* [subterm_specif renv t] computes the recursive structure of [t] and
    compare its size with the size of the initial recursive argument of
    the fixpoint we are checking. [renv] collects such information
@@ -650,6 +648,7 @@ let rec subterm_specif renv stack t =
 	 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
       *)
+           (* TODO: is this necessary? *)
     if not (check_inductive_codomain renv.env typarray.(i)) then Not_subterm
     else 
       let (ctxt,clfix) = dest_prod renv.env typarray.(i) in	    
@@ -686,7 +685,7 @@ let rec subterm_specif renv stack t =
 
     | Lambda (x,a,b) ->
       let () = assert (List.is_empty l) in
-      let spec,stack' = extract_stack renv a stack in
+      let spec,stack' = extract_stack stack in
 	subterm_specif (push_var renv (x,a,spec)) stack' b
 
       (* Metas and evars are considered OK *)
@@ -702,7 +701,7 @@ and stack_element_specif = function
   |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
   |SArg x -> x
 
-and extract_stack renv a = function
+and extract_stack = function
   | [] -> Lazy.lazy_from_val Not_subterm , []
   | h::t -> stack_element_specif h, t
 
@@ -732,6 +731,34 @@ let error_illegal_rec_call renv fx (arg_renv,arg) =
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
 
+let filter_stack_domain env ci p stack =
+  let absctx, ar = dest_lam_assum env p in
+  let env = push_rel_context absctx env in
+  let rec filter_stack env ar stack =
+    let t = whd_betadeltaiota env ar in
+    match stack, kind_of_term t with
+    | elt :: stack', Prod (n,a,c0) ->
+      let d = (n,None,a) in
+      let ty, _ = decompose_app a in (* TODO: reduce a? *)
+      let elt = match kind_of_term ty with
+      | Ind i -> 
+        let (_,mip) = lookup_mind_specif env i in
+        let spec' = stack_element_specif elt in (* TODO: this is recomputed
+        each time*)
+        (match (Lazy.force spec') with (* TODO: are we forcing too much? *)
+        | Not_subterm -> elt
+        | Subterm(_,path) ->
+            if eq_wf_paths path mip.mind_recargs then elt
+            else (SArg (lazy Not_subterm))) (* TODO: intersection *)
+            (* TODO: not really an SArg *)
+      | _ -> (SArg (lazy Not_subterm))
+      in
+      elt :: filter_stack (push_rel d env) c0 stack'
+    | _,_ -> List.fold_right (fun _ l -> SArg (lazy Not_subterm) :: l) stack []
+             (* TODO: is it correct to empty the stack instead? *)
+  in
+  filter_stack env ar stack
+
 (* Check if [def] is a guarded fixpoint body with decreasing arg.
    given [recpos], the decreasing arguments of each mutually defined
    fixpoint. *)
@@ -786,6 +813,7 @@ let check_one_fix renv recpos def =
             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 ci 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
@@ -828,7 +856,7 @@ let check_one_fix renv recpos def =
         | Lambda (x,a,b) ->
             let () = assert (List.is_empty l) in
 	    check_rec_call renv [] a ;
-	    let spec, stack' = extract_stack renv a stack in
+	    let spec, stack' = extract_stack stack in
 	    check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->