From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 11:44:28 +0000 (+0000)
Subject: Bug fixed: Invalid_argument was raised by List.combine in place of a typing
X-Git-Tag: V_0_1_2_1~108
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2d2783d78eadbaec5f43252d420018667a3ddf8;p=helm.git

Bug fixed: Invalid_argument was raised by List.combine in place of a typing
error. A similar thing occurred during pretty-printing.
---

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 776532852..93d7d0a04 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -141,9 +141,21 @@ let rec pp t l =
           | _ -> raise CicPpInternalError
         )
        in
+        let connames_and_patterns =
+         let rec combine =
+            function
+               [],[] -> []
+             | [],l -> List.map (fun x -> "???",Some x) l
+             | l,[] -> List.map (fun x -> x,None) l
+             | x::tlx,y::tly -> (x,Some y)::(combine (tlx,tly))
+         in
+          combine (connames,patterns)
+        in
         "\n<" ^ pp ty l ^ ">Cases " ^ pp te l ^ " of " ^
-          List.fold_right (fun (x,y) i -> "\n " ^ x ^ " => " ^ pp y l ^ i)
-           (List.combine connames patterns) "" ^
+          List.fold_right
+           (fun (x,y) i -> "\n " ^ x ^ " => " ^
+             (match y with None -> "" | Some y -> pp y l) ^ i)
+           connames_and_patterns "" ^
           "\nend"
     | C.Fix (no, funs) ->
        let snames = List.map (fun (name,_,_,_) -> name) funs in
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 6d26f8848..f2c0ebbcc 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -767,6 +767,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                  i && check_is_really_smaller_arg ~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 "not enough patterns")
+             in
               List.fold_right
                (fun (p,(_,c)) i ->
                  let rl' =
@@ -778,7 +785,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                   in
                    i &&
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -806,6 +813,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                  i && check_is_really_smaller_arg ~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 "not enough patterns")
+             in
               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
               (*CSC: sugli argomenti di una applicazione                      *)
               List.fold_right
@@ -819,7 +833,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
                   in
                    i &&
                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | _ ->
           List.fold_right
            (fun p i ->
@@ -940,6 +954,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                  i && guarded_by_destructors context n nn kl x safes p)
                pl true
             else
+             let pl_and_cl =
+              try
+               List.combine pl cl
+              with
+               Invalid_argument _ ->
+                raise (TypeCheckerFailure "not enough patterns")
+             in
              guarded_by_destructors context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
@@ -950,7 +971,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                   in
                    i &&
                    guarded_by_destructors context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
 	    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
@@ -981,6 +1002,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                  i && guarded_by_destructors context n nn kl x safes p)
                pl true
             else
+             let pl_and_cl =
+              try
+               List.combine pl cl
+              with
+               Invalid_argument _ ->
+                raise (TypeCheckerFailure "not enough patterns")
+             in
              guarded_by_destructors context n nn kl x safes outtype &&
               (*CSC: manca ??? il controllo sul tipo di term? *)
               List.fold_right
@@ -998,7 +1026,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes =
                   in
                    i &&
                    guarded_by_destructors context' n' nn' kl x' safes' e
-               ) (List.combine pl cl) true
+               ) pl_and_cl true
         | _ ->
           guarded_by_destructors context n nn kl x safes outtype &&
            guarded_by_destructors context n nn kl x safes term &&