From 458d0fc95ae3f3a20bd91e3e29ddeb92a009d0fa Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 Apr 2003 14:19:43 +0000 Subject: [PATCH] * Removed several try .... with _ -> (which make thread killing impossible ;-(( * The CicTypeChecker module now uses just a single TypeCheckerFailure exception --- .../cic_proof_checking/cicTypeChecker.ml | 319 ++++++++++++------ .../cic_proof_checking/cicTypeChecker.mli | 23 +- 2 files changed, 227 insertions(+), 115 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index b07c6e4a0..48d8b2ea9 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -23,17 +23,21 @@ * http://cs.unibo.it/helm/. *) -exception Impossible of int;; -exception NotWellTyped of string;; -exception WrongUriToConstant of string;; -exception WrongUriToVariable of string;; -exception WrongUriToMutualInductiveDefinitions of string;; -exception ListTooShort;; -exception NotPositiveOccurrences of string;; -exception NotWellFormedTypeOfInductiveConstructor of string;; -exception WrongRequiredArgument of string;; -exception RelToHiddenHypothesis;; -exception MetasenvInconsistency;; +type type_checker_exn = + Impossible of int + | NotWellTyped of string + | WrongUriToConstant of string + | WrongUriToVariable of string + | WrongUriToMutualInductiveDefinitions of string + | ListTooShort + | NotPositiveOccurrences of string + | NotWellFormedTypeOfInductiveConstructor of string + | WrongRequiredArgument of string + | RelToHiddenHypothesis + | MetasenvInconsistency;; + +(* This is the only exception that will be raised *) +exception TypeCheckerFailure of type_checker_exn;; let fdebug = ref 0;; let debug t context = @@ -43,7 +47,9 @@ let debug t context = CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i in if !fdebug = 0 then - raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) "")) + raise + (TypeCheckerFailure + (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) ""))) (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*) ;; @@ -51,7 +57,7 @@ let rec split l n = match (l,n) with (l,0) -> ([], l) | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) - | (_,_) -> raise ListTooShort + | (_,_) -> raise (TypeCheckerFailure ListTooShort) ;; let debrujin_constructor uri number_of_types = @@ -60,7 +66,7 @@ let debrujin_constructor uri number_of_types = function C.Rel n as t when n <= k -> t | C.Rel _ -> - raise (NotWellTyped ("Debrujin: open term found")) + raise (TypeCheckerFailure (NotWellTyped ("Debrujin: open term found"))) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst @@ -82,9 +88,10 @@ let debrujin_constructor uri number_of_types = | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' -> if exp_named_subst != [] then raise - (NotWellTyped - ("Debrujin: a non-empty explicit named substitution is applied to " ^ - "a mutual inductive type which is being defined")) ; + (TypeCheckerFailure + (NotWellTyped + ("Debrujin: a non-empty explicit named substitution is applied to "^ + "a mutual inductive type which is being defined"))) ; C.Rel (k + number_of_types - tyno) ; | C.MutInd (uri',tyno,exp_named_subst) -> let exp_named_subst' = @@ -135,7 +142,9 @@ let rec type_of_constant uri = C.Constant (_,Some te,ty,_) -> let _ = type_of ty in if not (R.are_convertible [] (type_of te) ty) then - raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) + raise + (TypeCheckerFailure + (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))) | C.Constant (_,None,ty,_) -> (* only to check that ty is well-typed *) let _ = type_of ty in () @@ -150,8 +159,11 @@ let rec type_of_constant uri = let _ = type_of_aux' conjs [] ty in if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then - raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) - | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) + raise + (TypeCheckerFailure + (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))) + | _ -> + raise (TypeCheckerFailure (WrongUriToConstant (U.string_of_uri uri))) ) ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; @@ -162,7 +174,7 @@ let rec type_of_constant uri = match cobj with C.Constant (_,_,ty,_) -> ty | C.CurrentProof (_,_,_,ty,_) -> ty - | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) + | _ -> raise (TypeCheckerFailure (WrongUriToConstant (U.string_of_uri uri))) and type_of_variable uri = let module C = Cic in @@ -179,12 +191,16 @@ and type_of_variable uri = None -> () | Some bo -> if not (R.are_convertible [] (type_of bo) ty) then - raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri))) + raise + (TypeCheckerFailure + (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))) ) ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; ty - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + | _ -> + raise + (TypeCheckerFailure (WrongUriToVariable (UriManager.string_of_uri uri))) and does_not_occur context n nn te = let module C = Cic in @@ -327,7 +343,11 @@ and weakly_positive context n nn uri te = (subst_inductive_type_with_dummy_mutind source)&& weakly_positive ((Some (name,(C.Decl source)))::context) (n + 1) (nn + 1) uri dest - | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)")) + | _ -> + raise + (TypeCheckerFailure + (NotWellFormedTypeOfInductiveConstructor + ("Guess where the error is ;-)"))) (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) @@ -339,7 +359,7 @@ and instantiate_parameters params c = instantiate_parameters tl (CicSubstitution.subst he ta) | (C.Cast (te,_), _) -> instantiate_parameters params te - | (t,l) -> raise (Impossible 1) + | (t,l) -> raise (TypeCheckerFailure (Impossible 1)) and strictly_positive context n nn te = let module C = Cic in @@ -360,7 +380,10 @@ and strictly_positive context n nn te = C.InductiveDefinition (tl,_,paramsno) -> let (name,_,ity,cl) = List.nth tl i in (List.length tl = 1, paramsno, ity, cl, name) - | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + | _ -> + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))) in let (params,arguments) = split tl paramsno in let lifted_params = List.map (CicSubstitution.lift 1) params in @@ -399,18 +422,25 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = else match CicReduction.whd context x with C.Rel m when m = n - (indparamsno - k) -> k - 1 - | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri)) + | _ -> + raise + (TypeCheckerFailure + (WrongRequiredArgument (UriManager.string_of_uri uri))) ) indparamsno tl in if last = 0 then List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true else - raise (WrongRequiredArgument (UriManager.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongRequiredArgument (UriManager.string_of_uri uri))) | C.Rel m when m = i -> if indparamsno = 0 then true else - raise (WrongRequiredArgument (UriManager.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongRequiredArgument (UriManager.string_of_uri uri))) | C.Prod (C.Anonymous,source,dest) -> strictly_positive context n nn source && are_all_occurrences_positive @@ -427,7 +457,10 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = does_not_occur context n nn source && are_all_occurrences_positive ((Some (name,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest - | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri)) + | _ -> + raise + (TypeCheckerFailure + (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))) (* Main function to checks the correctness of a mutual *) (* inductive block definition. This is the function *) @@ -464,7 +497,9 @@ and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) = (are_all_occurrences_positive tys uri indparamsno i 0 len debrujinedte) then - raise (NotPositiveOccurrences (U.string_of_uri uri)) + raise + (TypeCheckerFailure + (NotPositiveOccurrences (U.string_of_uri uri))) ) cl ; (i + 1) ) itl 1 @@ -478,7 +513,9 @@ and check_mutual_inductive_defs uri = Cic.InductiveDefinition (itl, params, indparamsno) -> typecheck_mutual_inductive_defs uri (itl,params,indparamsno) | _ -> - raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri))) and type_of_mutual_inductive_defs uri i = let module C = Cic in @@ -501,7 +538,10 @@ and type_of_mutual_inductive_defs uri i = C.InductiveDefinition (dl,_,_) -> let (_,_,arity,_) = List.nth dl i in arity - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + | _ -> + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))) and type_of_mutual_inductive_constr uri i j = let module C = Cic in @@ -525,7 +565,10 @@ and type_of_mutual_inductive_constr uri i j = let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + | _ -> + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))) and recursive_args context n nn te = let module C = Cic in @@ -535,19 +578,22 @@ and recursive_args context n nn te = | C.Meta _ | C.Sort _ | C.Implicit - | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *) + | C.Cast _ (*CSC ??? *) -> + raise (TypeCheckerFailure (Impossible 3)) (* due to type-checking *) | C.Prod (name,so,de) -> (not (does_not_occur context n nn so)) :: (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de) | C.Lambda _ - | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *) + | C.LetIn _ -> + raise (TypeCheckerFailure (Impossible 4)) (* due to type-checking *) | C.Appl _ -> [] - | C.Const _ -> raise (Impossible 5) + | C.Const _ -> raise (TypeCheckerFailure (Impossible 5)) | C.MutInd _ | C.MutConstruct _ | C.MutCase _ | C.Fix _ - | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *) + | C.CoFix _ -> + raise (TypeCheckerFailure (Impossible 6)) (* due to type-checking *) and get_new_safes context p c rl safes n nn x = let module C = Cic in @@ -575,7 +621,7 @@ and get_new_safes context p c rl safes n nn x = (* CSC: as a branch of a case whose type is a Prod. In *) (* CSC: particular, this means that a new (C.Prod, x,_) case *) (* CSC: must be considered in this match. (e.g. x = MutCase) *) - raise (Impossible 7) + raise (TypeCheckerFailure (Impossible 7)) and split_prods context n te = let module C = Cic in @@ -584,7 +630,7 @@ and split_prods context n te = (0, _) -> context,te | (n, C.Prod (name,so,ta)) when n > 0 -> split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta - | (_, _) -> raise (Impossible 8) + | (_, _) -> raise (TypeCheckerFailure (Impossible 8)) and eat_lambdas context n te = let module C = Cic in @@ -596,7 +642,7 @@ and eat_lambdas context n te = eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta in (te, k + 1, context') - | (_, _) -> raise (Impossible 9) + | (_, _) -> raise (TypeCheckerFailure (Impossible 9)) (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) and check_is_really_smaller_arg context n nn kl x safes te = @@ -619,7 +665,7 @@ and check_is_really_smaller_arg context 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 10) + | C.Prod _ -> raise (TypeCheckerFailure (Impossible 10)) | C.Lambda (name,so,ta) -> check_is_really_smaller_arg context n nn kl x safes so && check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context) @@ -632,9 +678,9 @@ and check_is_really_smaller_arg context 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 context n nn kl x safes he - | C.Appl [] -> raise (Impossible 11) + | C.Appl [] -> raise (TypeCheckerFailure (Impossible 11)) | C.Const _ - | C.MutInd _ -> raise (Impossible 12) + | C.MutInd _ -> raise (TypeCheckerFailure (Impossible 12)) | C.MutConstruct _ -> false | C.MutCase (uri,i,outtype,term,pl) -> (match term with @@ -653,7 +699,9 @@ and check_is_really_smaller_arg context n nn kl x safes te = in (tys,List.length tl,isinductive,paramsno,cl') | _ -> - raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))) in if not isinductive then List.fold_right @@ -688,7 +736,9 @@ and check_is_really_smaller_arg context n nn kl x safes te = in (tys,List.length tl,isinductive,paramsno,cl') | _ -> - raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))) in if not isinductive then List.fold_right @@ -752,7 +802,7 @@ and guarded_by_destructors context n nn kl x safes = (match List.nth context (n-1) with Some (_,C.Decl _) -> true | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo - | None -> raise RelToHiddenHypothesis + | None -> raise (TypeCheckerFailure RelToHiddenHypothesis) ) | C.Meta _ | C.Sort _ @@ -809,7 +859,9 @@ and guarded_by_destructors context n nn kl x safes = in (tys,List.length tl,isinductive,paramsno,cl') | _ -> - raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))) in if not isinductive then guarded_by_destructors context n nn kl x safes outtype && @@ -849,7 +901,9 @@ and guarded_by_destructors context n nn kl x safes = in (tys,List.length tl,isinductive,paramsno,cl') | _ -> - raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))) in if not isinductive then guarded_by_destructors context n nn kl x safes outtype && @@ -932,7 +986,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Cast _ | C.Prod _ | C.LetIn _ -> - raise (Impossible 17) (* the term has just been type-checked *) + (* the term has just been type-checked *) + raise (TypeCheckerFailure (Impossible 17)) | C.Lambda (name,so,de) -> does_not_occur context n nn so && guarded_by_constructors ((Some (name,(C.Decl so)))::context) @@ -948,22 +1003,26 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = let (_,cons) = List.nth cl (j - 1) in CicSubstitution.subst_vars exp_named_subst cons | _ -> - raise (WrongUriToMutualInductiveDefinitions - (UriManager.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri))) in let rec analyse_branch context ty te = match CicReduction.whd context ty with - C.Meta _ -> raise (Impossible 34) + C.Meta _ -> raise (TypeCheckerFailure (Impossible 34)) | C.Rel _ | C.Var _ | C.Sort _ -> does_not_occur context n nn te | C.Implicit - | C.Cast _ -> raise (Impossible 24) (* due to type-checking *) + | C.Cast _ -> + raise (TypeCheckerFailure (Impossible 24))(* due to type-checking *) | C.Prod (name,so,de) -> analyse_branch ((Some (name,(C.Decl so)))::context) de te | C.Lambda _ - | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *) + | C.LetIn _ -> + raise (TypeCheckerFailure (Impossible 25))(* due to type-checking *) | C.Appl ((C.MutInd (uri,_,_))::_) as ty when uri == coInductiveTypeURI -> guarded_by_constructors context n nn true te [] coInductiveTypeURI @@ -971,17 +1030,18 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = guarded_by_constructors context n nn true te tl coInductiveTypeURI | C.Appl _ -> does_not_occur context n nn te - | C.Const _ -> raise (Impossible 26) + | C.Const _ -> raise (TypeCheckerFailure (Impossible 26)) | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> guarded_by_constructors context n nn true te [] coInductiveTypeURI | C.MutInd _ -> does_not_occur context n nn te - | C.MutConstruct _ -> raise (Impossible 27) + | C.MutConstruct _ -> raise (TypeCheckerFailure (Impossible 27)) (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) (*CSC: in head position. *) | C.MutCase _ | C.Fix _ - | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *) + | C.CoFix _ -> + raise (TypeCheckerFailure (Impossible 28))(* due to type-checking *) in let rec analyse_instantiated_type context ty l = match CicReduction.whd context ty with @@ -990,7 +1050,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | C.Meta _ | C.Sort _ | C.Implicit - | C.Cast _ -> raise (Impossible 29) (* due to type-checking *) + | C.Cast _ -> + raise (TypeCheckerFailure (Impossible 29))(* due to type-checking *) | C.Prod (name,so,de) -> begin match l with @@ -1001,20 +1062,22 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = de tl end | C.Lambda _ - | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *) + | C.LetIn _ -> + raise (TypeCheckerFailure (Impossible 30))(* due to type-checking *) | C.Appl _ -> List.fold_left (fun i x -> i && does_not_occur context n nn x) true l - | C.Const _ -> raise (Impossible 31) + | C.Const _ -> raise (TypeCheckerFailure (Impossible 31)) | C.MutInd _ -> List.fold_left (fun i x -> i && does_not_occur context n nn x) true l - | C.MutConstruct _ -> raise (Impossible 32) + | C.MutConstruct _ -> raise (TypeCheckerFailure (Impossible 32)) (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) (*CSC: in head position. *) | C.MutCase _ | C.Fix _ - | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *) + | C.CoFix _ -> + raise (TypeCheckerFailure (Impossible 33))(* due to type-checking *) in let rec instantiate_type args consty = function @@ -1033,7 +1096,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = | _ -> (*CSC:We do not consider backbones with a MutCase, a *) (*CSC:FixPoint, a CoFixPoint and so on in head position.*) - raise (Impossible 23) + raise (TypeCheckerFailure (Impossible 23)) end | [] -> analyse_instantiated_type context consty' l (* These are all the other cases *) @@ -1121,7 +1184,9 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = (* is a singleton definition or the empty proposition? *) List.length cl = 1 || List.length cl = 0 | _ -> - raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))) ) | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true @@ -1135,7 +1200,9 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = List.fold_right (fun (_,x) i -> i && is_small tys paramsno x) cl true | _ -> - raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))) ) | (C.Sort C.Type, C.Sort _) when need_dummy -> true | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy -> @@ -1151,8 +1218,9 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = (* is a singleton definition? *) List.length cl = 1 | _ -> - raise (WrongUriToMutualInductiveDefinitions - (U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))) ) | _ -> false ) @@ -1174,10 +1242,11 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = List.fold_right (fun (_,x) i -> i && is_small tys paramsno x) cl true | _ -> - raise (WrongUriToMutualInductiveDefinitions - (U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))) ) - | _ -> raise (Impossible 19) + | _ -> raise (TypeCheckerFailure (Impossible 19)) ) | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy -> CicReduction.are_convertible context so ind @@ -1208,7 +1277,7 @@ and type_of_branch context argsno need_dummy outtype term constype = C.Prod (C.Anonymous,so,type_of_branch ((Some (name,(C.Decl so)))::context) argsno need_dummy (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (Impossible 20) + | _ -> raise (TypeCheckerFailure (Impossible 20)) (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -1241,7 +1310,7 @@ and check_metasenv_consistency metasenv context canonical_context l = R.are_convertible context (type_of_aux' metasenv context t) ct | _, _ -> false in - if not res then raise MetasenvInconsistency + if not res then raise (TypeCheckerFailure MetasenvInconsistency) ) l lifted_canonical_context (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -1257,9 +1326,9 @@ and type_of_aux' metasenv context t = match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo) - | None -> raise RelToHiddenHypothesis + | None -> raise (TypeCheckerFailure RelToHiddenHypothesis) with - _ -> raise (NotWellTyped "Not a close term") + _ -> raise (TypeCheckerFailure (NotWellTyped "Not a close term")) ) | C.Var (uri,exp_named_subst) -> incr fdebug ; @@ -1276,11 +1345,11 @@ and type_of_aux' metasenv context t = check_metasenv_consistency metasenv context canonical_context l; CicSubstitution.lift_meta l ty | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) - | C.Implicit -> raise (Impossible 21) + | C.Implicit -> raise (TypeCheckerFailure (Impossible 21)) | C.Cast (te,ty) -> let _ = type_of_aux context ty in if R.are_convertible context (type_of_aux context te) ty then ty - else raise (NotWellTyped "Cast") + else raise (TypeCheckerFailure (NotWellTyped "Cast")) | C.Prod (name,s,t) -> let sort1 = type_of_aux context s and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in @@ -1313,7 +1382,7 @@ and type_of_aux' metasenv context t = let hetype = type_of_aux context he and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in eat_prods context hetype tlbody_and_type - | C.Appl _ -> raise (NotWellTyped "Appl: no arguments") + | C.Appl _ -> raise (TypeCheckerFailure (NotWellTyped "Appl: no arguments")) | C.Const (uri,exp_named_subst) -> incr fdebug ; check_exp_named_subst context exp_named_subst ; @@ -1358,7 +1427,9 @@ and type_of_aux' metasenv context t = | _ -> (true, 1) else (b, n + 1) - | _ -> raise (NotWellTyped "MutCase: outtype ill-formed") + | _ -> + raise + (TypeCheckerFailure (NotWellTyped "MutCase: outtype ill-formed")) in (*CSC whd non serve dopo type_of_aux ? *) let (b, k) = guess_args context outsort in @@ -1372,20 +1443,23 @@ and type_of_aux' metasenv context t = (*CSC: Hint: nella DTD servono per gli stylesheet. *) C.MutInd (uri',i',exp_named_subst) as typ -> if U.eq uri uri' && i = i' then ([],[],exp_named_subst) - else raise (NotWellTyped ("MutCase: the term is of type " ^ + else raise (TypeCheckerFailure + (NotWellTyped ("MutCase: the term is of type " ^ CicPp.ppterm typ ^ " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^ - string_of_int i ^ "{_}")) + string_of_int i ^ "{_}"))) | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) -> if U.eq uri uri' && i = i' then let params,args = split tl (List.length tl - k) in params,args,exp_named_subst - else raise (NotWellTyped ("MutCase: the term is of type " ^ + else raise (TypeCheckerFailure (NotWellTyped + ("MutCase: the term is of type " ^ CicPp.ppterm typ ^ " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^ - string_of_int i ^ "{_}")) - | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one") + string_of_int i ^ "{_}"))) + | _ -> raise (TypeCheckerFailure + (NotWellTyped "MutCase: the term is not an inductive one")) in (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *) let sort_of_ind_type = @@ -1397,14 +1471,18 @@ and type_of_aux' metasenv context t = if not (check_allowed_sort_elimination context uri i need_dummy sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort) then - raise (NotWellTyped "MutCase: not allowed sort elimination") ; + raise + (TypeCheckerFailure + (NotWellTyped "MutCase: not allowed sort elimination")) ; (* let's check if the type of branches are right *) let parsno = match CicEnvironment.get_cooked_obj ~trust:false uri with C.InductiveDefinition (_,_,parsno) -> parsno | _ -> - raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))) in let (_,branches_ok) = List.fold_left @@ -1428,7 +1506,9 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) ) (1,true) pl in if not branches_ok then - raise (NotWellTyped "MutCase: wrong type of a branch") ; + raise + (TypeCheckerFailure + (NotWellTyped "MutCase: wrong type of a branch")) ; if not need_dummy then C.Appl ((outtype::arguments)@[term]) @@ -1461,10 +1541,12 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) not (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m) then - raise (NotWellTyped "Fix: not guarded by destructors") + raise + (TypeCheckerFailure + (NotWellTyped "Fix: not guarded by destructors")) end else - raise (NotWellTyped "Fix: ill-typed bodies") + raise (TypeCheckerFailure (NotWellTyped "Fix: ill-typed bodies")) ) fl ; (*CSC: controlli mancanti solo su D{f,k,x,M} *) @@ -1488,7 +1570,9 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) (* let's control that the returned type is coinductive *) match returns_a_coinductive context ty with None -> - raise(NotWellTyped "CoFix: does not return a coinductive type") + raise + (TypeCheckerFailure + (NotWellTyped "CoFix: does not return a coinductive type")) | Some uri -> (*let's control the guarded by constructors conditions C{f,M}*) if @@ -1496,10 +1580,14 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) (guarded_by_constructors (types @ context) 0 len false bo [] uri) then - raise (NotWellTyped "CoFix: not guarded by constructors") + raise + (TypeCheckerFailure + (NotWellTyped "CoFix: not guarded by constructors")) end else - raise (NotWellTyped "CoFix: ill-typed bodies") + raise + (TypeCheckerFailure + (NotWellTyped "CoFix: ill-typed bodies")) ) fl ; let (_,ty,_) = List.nth fl i in @@ -1515,10 +1603,14 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise - (NotWellTyped - "A variable with a body can not be explicit substituted") + (TypeCheckerFailure + (NotWellTyped + "A variable with a body can not be explicit substituted")) | Cic.Variable (_,None,_,_) -> () - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + | _ -> + raise + (TypeCheckerFailure + (WrongUriToVariable (UriManager.string_of_uri uri))) ) ; let typeoft = type_of_aux context t in if CicReduction.are_convertible context typeoft typeofvar then @@ -1529,7 +1621,9 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) ignore (CicReduction.are_convertible context typeoft typeofvar) ; fdebug := 0 ; debug typeoft [typeofvar] ; - raise (NotWellTyped "Wrong Explicit Named Substitution") + raise + (TypeCheckerFailure + (NotWellTyped "Wrong Explicit Named Substitution")) end in check_exp_named_subst_aux [] @@ -1545,8 +1639,9 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) | (_,_) -> raise - (NotWellTyped - ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2')) + (TypeCheckerFailure + (NotWellTyped + ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= "^ CicPp.ppterm t2'))) and eat_prods context hetype = (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) @@ -1566,9 +1661,10 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) ignore (CicReduction.are_convertible context s hety) ; fdebug := 0 ; debug s [hety] ; - raise (NotWellTyped "Appl: wrong parameter-type") + raise + (TypeCheckerFailure (NotWellTyped "Appl: wrong parameter-type")) end - | _ -> raise (NotWellTyped "Appl: wrong Prod-type") + | _ -> raise (TypeCheckerFailure (NotWellTyped "Appl: wrong Prod-type")) ) and returns_a_coinductive context ty = @@ -1581,8 +1677,9 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) | _ -> - raise (WrongUriToMutualInductiveDefinitions - (UriManager.string_of_uri uri)) + raise + (TypeCheckerFailure (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri))) ) | C.Appl ((C.MutInd (uri,i,_))::_) -> (match CicEnvironment.get_obj uri with @@ -1590,8 +1687,10 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) | _ -> - raise (WrongUriToMutualInductiveDefinitions - (UriManager.string_of_uri uri)) + raise + (TypeCheckerFailure + (WrongUriToMutualInductiveDefinitions + (UriManager.string_of_uri uri))) ) | C.Prod (n,so,de) -> returns_a_coinductive ((Some (n,C.Decl so))::context) de @@ -1647,7 +1746,9 @@ let typecheck uri = C.Constant (_,Some te,ty,_) -> let _ = type_of ty in if not (R.are_convertible [] (type_of te ) ty) then - raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri))) + raise + (TypeCheckerFailure + (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))) | C.Constant (_,None,ty,_) -> (* only to check that ty is well-typed *) let _ = type_of ty in () @@ -1662,7 +1763,9 @@ let typecheck uri = let _ = type_of_aux' conjs [] ty in if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then - raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) + raise + (TypeCheckerFailure + (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))) | C.Variable (_,bo,ty,_) -> (* only to check that ty is well-typed *) let _ = type_of ty in @@ -1670,7 +1773,9 @@ let typecheck uri = None -> () | Some bo -> if not (R.are_convertible [] (type_of bo) ty) then - raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri))) + raise + (TypeCheckerFailure + (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))) ) | C.InductiveDefinition _ -> check_mutual_inductive_defs uri uobj diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 4a7fe8db0..1dbcc11c8 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -23,14 +23,21 @@ * http://cs.unibo.it/helm/. *) -exception NotWellTyped of string -exception WrongUriToConstant of string -exception WrongUriToVariable of string -exception WrongUriToMutualInductiveDefinitions of string -exception ListTooShort -exception NotPositiveOccurrences of string -exception NotWellFormedTypeOfInductiveConstructor of string -exception WrongRequiredArgument of string +type type_checker_exn = + Impossible of int + | NotWellTyped of string + | WrongUriToConstant of string + | WrongUriToVariable of string + | WrongUriToMutualInductiveDefinitions of string + | ListTooShort + | NotPositiveOccurrences of string + | NotWellFormedTypeOfInductiveConstructor of string + | WrongRequiredArgument of string + | RelToHiddenHypothesis + | MetasenvInconsistency;; + +(* This is the only exception that will be raised *) +exception TypeCheckerFailure of type_checker_exn;; val typecheck : UriManager.uri -> unit -- 2.39.2