From d841c3bfd62e3f1547bf1e25cad7c998d52d7c2d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 30 Nov 2001 17:15:59 +0000 Subject: [PATCH] Exception management improved. --- .../cic_proof_checking/cicTypeChecker.ml | 46 +++++++++---------- 1 file changed, 23 insertions(+), 23 deletions(-) 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 -- 2.39.2