X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=f2c0ebbcc5d44555932c0fd715db21ddfe1622be;hb=b66e2a4ea05a9a53b1c4c1d7051de0419ccc441b;hp=1db82a99fb48eeddcf63adb96c4a31575e2ca5e6;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 1db82a99f..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 &&
@@ -1299,21 +1327,19 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind
 	 false,ugraph1
        else
          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
-           C.Sort C.Prop -> true,ugraph1
-         | (C.Sort C.Set | C.Sort C.CProp) ->
-             (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-	       match o with
-               C.InductiveDefinition (itl,_,_,_) ->
-                   let (_,_,_,cl) = List.nth itl i in
-                   (* is a singleton definition? *)
-                   List.length cl = 1,ugraph1
-             | _ ->
-                 raise (TypeCheckerFailure
-			  ("Unknown mutual inductive definition:" ^
-			   UriManager.string_of_uri uri))
-             )
-         | _ -> false,ugraph1
-         )
+              C.Sort C.Prop -> true,ugraph1
+           | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
+               (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                 match o with
+                    C.InductiveDefinition (itl,_,_,_) ->
+                     let (_,_,_,cl) = List.nth itl i in
+                     (* is a singleton definition or the empty proposition? *)
+                     (List.length cl = 1 || List.length cl = 0),ugraph1
+                  | _ ->
+                   raise (TypeCheckerFailure
+                    ("Unknown mutual inductive definition:" ^
+                       UriManager.string_of_uri uri)))
+           | _ -> false,ugraph1)
    | ((C.Sort C.Set, C.Prod (name,so,ta)) 
    | (C.Sort C.CProp, C.Prod (name,so,ta)))
      when not need_dummy ->
@@ -1768,12 +1794,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           if not branches_ok then
            raise
             (TypeCheckerFailure "Case analysys: wrong branch type");
-          let arguments =
+          let arguments' =
            if not need_dummy then outtype::arguments@[term]
            else outtype::arguments in
           let outtype =
-           if arguments = [] then outtype
-           else CicReduction.head_beta_reduce (C.Appl arguments)
+           if need_dummy && arguments = [] then outtype
+           else CicReduction.head_beta_reduce (C.Appl arguments')
           in
            outtype,ugraph5
    | C.Fix (i,fl) ->