From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 30 Nov 2001 17:15:59 +0000 (+0000)
Subject: Exception management improved.
X-Git-Tag: mlminidom_0_2_2~40
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d841c3bfd62e3f1547bf1e25cad7c998d52d7c2d;p=helm.git

Exception management improved.
---

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 2ccc1e743..f2cd6265e 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -24,7 +24,7 @@
  *)
 
 exception NotImplemented;;
-exception Impossible;;
+exception Impossible of int;;
 exception NotWellTyped of string;;
 exception WrongUriToConstant of string;;
 exception WrongUriToVariable of string;;
@@ -273,7 +273,7 @@ and instantiate_parameters params c =
        instantiate_parameters tl
         (CicSubstitution.subst he ta)
    | (C.Cast (te,_), _) -> instantiate_parameters params te
-   | (t,l) -> raise Impossible
+   | (t,l) -> raise (Impossible 1)
 
 and strictly_positive n nn te =
  let module C = Cic in
@@ -391,7 +391,7 @@ and cooked_mutual_inductive_defs uri =
                  raise (NotPositiveOccurrences (U.string_of_uri uri))
                 else
                  match !r with
-                    Some _ -> raise Impossible
+                    Some _ -> raise (Impossible 2)
                   | None -> r := Some (recursive_args 0 len te)
             ) cl ;
            (i + 1)
@@ -456,19 +456,19 @@ and recursive_args n nn te =
    | C.Meta _
    | C.Sort _
    | C.Implicit
-   | C.Cast _ (*CSC ??? *) -> raise Impossible (* due to type-checking *)
+   | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
    | C.Prod (_,so,de) ->
       (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
-   | C.Lambda _ -> raise Impossible (* due to type-checking *)
+   | C.Lambda _ -> raise (Impossible 4) (* due to type-checking *)
    | C.LetIn _ -> raise NotImplemented
    | C.Appl _ -> []
    | C.Const _
-   | C.Abst _ -> raise Impossible
+   | C.Abst _ -> raise (Impossible 5)
    | C.MutInd _
    | C.MutConstruct _
    | C.MutCase _
    | C.Fix _
-   | C.CoFix _ -> raise Impossible (* due to type-checking *)
+   | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
 
 and get_new_safes p c rl safes n nn x =
  let module C = Cic in
@@ -487,7 +487,7 @@ and get_new_safes p c rl safes n nn x =
          get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
    | (C.MutInd _, e, []) -> (e,safes,n,nn,x)
    | (C.Appl _, e, []) -> (e,safes,n,nn,x)
-   | (_,_,_) -> raise Impossible
+   | (_,_,_) -> raise (Impossible 7)
 
 and eat_prods n te =
  let module C = Cic in
@@ -495,7 +495,7 @@ and eat_prods n te =
   match (n, R.whd te) with
      (0, _) -> te
    | (n, C.Prod (_,_,ta)) when n > 0 -> eat_prods (n - 1) ta
-   | (_, _) -> raise Impossible
+   | (_, _) -> raise (Impossible 8)
 
 and eat_lambdas n te =
  let module C = Cic in
@@ -505,7 +505,7 @@ and eat_lambdas n te =
    | (n, C.Lambda (_,_,ta)) when n > 0 ->
       let (te, k) = eat_lambdas (n - 1) ta in
        (te, k + 1)
-   | (_, _) -> raise Impossible
+   | (_, _) -> raise (Impossible 9)
 
 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 and check_is_really_smaller_arg n nn kl x safes te =
@@ -528,7 +528,7 @@ and check_is_really_smaller_arg n nn kl x safes te =
       check_is_really_smaller_arg n nn kl x safes so &&
        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta*)
-   | C.Prod _ -> raise Impossible
+   | C.Prod _ -> raise (Impossible 10)
    | C.Lambda (_,so,ta) ->
       check_is_really_smaller_arg n nn kl x safes so &&
        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
@@ -541,10 +541,10 @@ and check_is_really_smaller_arg n nn kl x safes te =
       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
       (*CSC: solo perche' non abbiamo trovato controesempi            *)
       check_is_really_smaller_arg n nn kl x safes he
-   | C.Appl [] -> raise Impossible
+   | C.Appl [] -> raise (Impossible 11)
    | C.Const _
    | C.Abst _
-   | C.MutInd _ -> raise Impossible
+   | C.MutInd _ -> raise (Impossible 12)
    | C.MutConstruct _ -> false
    | C.MutCase (uri,_,i,outtype,term,pl) ->
       (match term with
@@ -572,7 +572,7 @@ and check_is_really_smaller_arg n nn kl x safes te =
                      Some rl' ->
                       let (_,rl'') = split rl' paramsno in
                        rl''
-                   | None -> raise Impossible
+                   | None -> raise (Impossible 13)
                  in
                   let (e,safes',n',nn',x') =
                    get_new_safes p c rl' safes n nn x
@@ -606,7 +606,7 @@ and check_is_really_smaller_arg n nn kl x safes te =
                      Some rl' ->
                       let (_,rl'') = split rl' paramsno in
                        rl''
-                   | None -> raise Impossible
+                   | None -> raise (Impossible 14)
                  in
                   let (e, safes',n',nn',x') =
                    get_new_safes p c rl' safes n nn x
@@ -716,7 +716,7 @@ and guarded_by_destructors n nn kl x safes =
                      Some rl' ->
                       let (_,rl'') = split rl' paramsno in
                        rl''
-                   | None -> raise Impossible
+                   | None -> raise (Impossible 15)
                  in
                   let (e,safes',n',nn',x') =
                    get_new_safes p c rl' safes n nn x
@@ -756,7 +756,7 @@ and guarded_by_destructors n nn kl x safes =
                      Some rl' ->
                       let (_,rl'') = split rl' paramsno in
                        rl''
-                   | None -> raise Impossible
+                   | None -> raise (Impossible 16)
                  in
                   let (e, safes',n',nn',x') =
                    get_new_safes p c rl' safes n nn x
@@ -813,7 +813,7 @@ and guarded_by_constructors n nn h =
       guarded_by_constructors n nn h te &&
        guarded_by_constructors n nn h ty
    | C.Prod (_,so,de) ->
-      raise Impossible (* the term has just been type-checked *)
+      raise (Impossible 17) (* the term has just been type-checked *)
    | C.Lambda (_,so,de) ->
       does_not_occur n nn so &&
        guarded_by_constructors (n + 1) (nn + 1) h de
@@ -830,7 +830,7 @@ and guarded_by_constructors n nn h =
            let (_,is_inductive,_,cl) = List.nth itl i in
             let (_,cons,rrec_args) = List.nth cl (j - 1) in
              (match !rrec_args with
-                 None -> raise Impossible
+                 None -> raise (Impossible 18)
                | Some rec_args -> (not is_inductive, rec_args)
              )
         | _ ->
@@ -989,7 +989,7 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
                  raise (WrongUriToMutualInductiveDefinitions
                   (U.string_of_uri uri))
              )
-          | _ -> raise Impossible
+          | _ -> raise (Impossible 19)
         )
    | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
        CicReduction.are_convertible so ind
@@ -1015,7 +1015,7 @@ and type_of_branch argsno need_dummy outtype term constype =
       C.Prod (C.Name "pippo",so,type_of_branch argsno need_dummy 
        (CicSubstitution.lift 1 outtype)
        (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
-  | _ -> raise Impossible
+  | _ -> raise (Impossible 20)
        
  
 and type_of t =
@@ -1033,7 +1033,7 @@ and type_of t =
        ty
     | C.Meta n -> raise NotImplemented
     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
-    | C.Implicit -> raise Impossible
+    | C.Implicit -> raise (Impossible 21)
     | C.Cast (te,ty) ->
        let _ = type_of ty in
         if R.are_convertible (type_of_aux env te) ty then ty
@@ -1065,7 +1065,7 @@ and type_of t =
       let cty = cooked_type_of_constant uri cookingsno in
        decr fdebug ;
        cty
-   | C.Abst _ -> raise Impossible
+   | C.Abst _ -> raise (Impossible 22)
    | C.MutInd (uri,cookingsno,i) ->
       incr fdebug ;
       let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in