Revert "Propagate size info through pattern matching in predicates, for the"

This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea.

Apply again if this kind of dependently typed programming idioms are needed.

1 files changed, 10 insertions, 23 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bce56d6170..8962fa9a92 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -763,6 +763,7 @@ let get_codomain_spec env p =
        let env' = push_rel_context pctx env in
        if is_arity env' pr then
 	 let specs = Array.map (family_codomain_spec env) lbr in
+	 (* What if the specs correspond to different inductive families? *)
 	 Array.fold_left family_spec_glb (None, Dead_code) specs
        else None, Not_subterm
     | _ -> None, Not_subterm
@@ -882,50 +883,36 @@ let error_illegal_rec_call renv fx (arg_renv,arg) =
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
 
-let rec filter_stack_domain env p stack =
-  let reset_stack stack =
-    (* TODO: is it correct to empty the stack instead? *)
-    List.fold_right (fun _ l -> (None, SArg (lazy Not_subterm)) :: l) stack []
-  in
+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
-    | (oind,elt) :: stack', Prod (n,a,c0) ->
+    | elt :: stack', Prod (n,a,c0) ->
       let d = (n,None,a) in
       let ty, args = decompose_app a in (* TODO: reduce a? *)
       let elt = match kind_of_term ty with
-      | Ind ind when oind = None || Option.equal eq_ind (Some ind) oind ->
+      | Ind ind -> 
         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 -> (Some ind, elt)
+        | Not_subterm -> elt
         | Subterm(s,path) ->
             let recargs = get_recargs_approx env ind args in
             let path = inter_wf_paths path recargs in
-            (Some ind, SArg (lazy (Subterm(s,path)))))
+            SArg (lazy (Subterm(s,path))))
             (* TODO: not really an SArg *)
             (* TODO: what if Dead_code above? *)
-      | _ -> (None, SArg (lazy Not_subterm)) (* We could accept match here too *)
+      | _ -> (SArg (lazy Not_subterm))
       in
       elt :: filter_stack (push_rel d env) c0 stack'
-    | _, Case (ci,p,c,lbr) ->
-      let pctx, pr = dest_lam_assum env p in
-      let env' = push_rel_context pctx env in
-      if is_arity env' pr then
-	Array.fold_left (fun stack ar -> filter_stack_domain env ar stack) stack lbr
-	(* What if the specs correspond to different inductive families? *)
-      else reset_stack stack
     | [], _ -> [] (* TODO: remove after debugging *)
-    | _,_ -> reset_stack 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
 
-let filter_stack_domain env p stack =
-  let stack = List.map (fun spec -> (None, spec)) stack in
-  List.map snd (filter_stack_domain env p stack)
-
 (* Check if [def] is a guarded fixpoint body with decreasing arg.
    given [recpos], the decreasing arguments of each mutually defined
    fixpoint. *)
@@ -981,7 +968,7 @@ let check_one_fix renv recpos trees 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 p 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