From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 17 Apr 2008 14:39:30 +0000 (+0000)
Subject: Two similar cases packed together
X-Git-Tag: make_still_working~5329
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=998a7855d00bcb55525a82138a3bfb4183d99014;p=helm.git

Two similar cases packed together
---

diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 5f1c933f2..68bbe416a 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -875,70 +875,17 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
    | C.Const (_,exp_named_subst)
    | C.MutInd (_,_,exp_named_subst)
    | C.MutConstruct (_,_,_,exp_named_subst) ->
-      List.fold_right
-       (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
-       exp_named_subst true
+      List.for_all
+       (fun (_,t) -> guarded_by_destructors ~subst context n nn kl x safes t)
+       exp_named_subst 
    | C.MutCase (uri,i,outtype,term,pl) ->
       (match CicReduction.whd ~subst context term with
-          C.Rel m when List.mem m safes || m = x ->
-           let (lefts_and_tys,len,isinductive,paramsno,cl) =
-	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-            match o with
-               C.InductiveDefinition (tl,_,paramsno,_) ->
-                let len = List.length tl in
-                 let (_,isinductive,_,cl) = List.nth tl i in
-                  let tys =
-                   List.map (fun (n,_,ty,_) ->
-                    Some(Cic.Name n,(Cic.Decl ty))) tl
-                  in
-                   let cl' =
-                    List.map
-                     (fun (id,ty) ->
-                      let debrujinedty = debrujin_constructor uri len ty in
-                       (id, snd (split_prods ~subst tys paramsno ty),
-                        snd (split_prods ~subst tys paramsno debrujinedty)
-                       )) cl in
-                   let lefts =
-                    match tl with
-                       [] -> assert false
-                     | (_,_,ty,_)::_ ->
-                        fst (split_prods ~subst [] paramsno ty)
-                   in
-                    (lefts@tys,len,isinductive,paramsno,cl')
-             | _ ->
-                raise (TypeCheckerFailure
-                  (lazy ("Unknown mutual inductive definition:" ^
-                  UriManager.string_of_uri uri)))
-           in
-            if not isinductive then
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              guarded_by_destructors ~subst context n nn kl x safes term &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun p i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes p)
-               pl true
-            else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
-             guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun (p,(name,c,brujinedc)) i ->
-                   i &&
-                 let rl' = recursive_args 
-                   lefts_and_tys paramsno (len+paramsno) brujinedc in
-                  let (e,safes',n',nn',x',context') =
-                   get_new_safes ~subst context p c rl' safes n nn x
-                  in
-                   guarded_by_destructors ~subst context' n' nn' kl x' safes' e
-               ) pl_and_cl true
-        | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
+        | C.Rel m 
+        | C.Appl ((C.Rel m)::_) as t when List.mem m safes || m = x ->
+           let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
+           List.for_all
+             (guarded_by_destructors ~subst context n nn kl x safes)
+             tl &&
            let (lefts_and_tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
             match o with
@@ -967,27 +914,13 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
             if not isinductive then
              guarded_by_destructors ~subst context n nn kl x safes outtype &&
               guarded_by_destructors ~subst context n nn kl x safes term &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun p i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes p)
-               pl true
+              List.for_all
+               (guarded_by_destructors ~subst context n nn kl x safes)
+               pl
             else
-             let pl_and_cl =
-              try
-               List.combine pl cl
-              with
-               Invalid_argument _ ->
-                raise (TypeCheckerFailure (lazy "not enough patterns"))
-             in
              guarded_by_destructors ~subst context n nn kl x safes outtype &&
-              (*CSC: manca ??? il controllo sul tipo di term? *)
-              List.fold_right
-               (fun t i ->
-                 i && guarded_by_destructors ~subst context n nn kl x safes t)
-               tl true &&
-              List.fold_right
-               (fun (p,(_,c)) i ->
+             List.for_all2
+               (fun p (_,c) ->
                  let rl' =
                   let debrujinedte = debrujin_constructor uri len c in
                    recursive_args lefts_and_tys paramsno 
@@ -996,9 +929,8 @@ and guarded_by_destructors ~subst context n nn kl x safes t =
                   let (e, safes',n',nn',x',context') =
                    get_new_safes ~subst context p c rl' safes n nn x
                   in
-                   i &&
                    guarded_by_destructors ~subst context' n' nn' kl x' safes' e
-               ) pl_and_cl true
+               ) pl cl
         | _ ->
           guarded_by_destructors ~subst context n nn kl x safes outtype &&
            guarded_by_destructors ~subst context n nn kl x safes term &&