From 8b55faddb06e3c4b0a13839210bb49170939b33e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 25 Oct 2005 12:37:37 +0000 Subject: [PATCH] Every exception that used to have type string is now a string Lazy.t. --- helm/matita/matitaEngine.ml | 2 +- helm/ocaml/cic_disambiguation/disambiguate.ml | 12 +- .../ocaml/cic_disambiguation/disambiguate.mli | 2 +- .../cic_disambiguation/disambiguateChoices.ml | 6 +- .../disambiguateChoices.mli | 2 +- helm/ocaml/cic_proof_checking/cicElim.ml | 6 +- helm/ocaml/cic_proof_checking/cicElim.mli | 2 +- .../cic_proof_checking/cicEnvironment.ml | 4 +- .../cic_proof_checking/cicEnvironment.mli | 2 +- .../cic_proof_checking/cicTypeChecker.ml | 268 +++++++++--------- .../cic_proof_checking/cicTypeChecker.mli | 4 +- helm/ocaml/cic_unification/cicMetaSubst.ml | 28 +- helm/ocaml/cic_unification/cicMetaSubst.mli | 6 +- helm/ocaml/cic_unification/cicRefine.ml | 69 ++--- helm/ocaml/cic_unification/cicRefine.mli | 9 +- helm/ocaml/cic_unification/cicUnification.ml | 118 ++++---- helm/ocaml/cic_unification/cicUnification.mli | 11 +- helm/ocaml/cic_unification/coercDb.ml | 6 +- helm/ocaml/cic_unification/coercDb.mli | 2 +- helm/ocaml/cic_unification/coercGraph.ml | 4 +- helm/ocaml/cic_unification/coercGraph.mli | 2 +- helm/ocaml/paramodulation/inference.ml | 12 +- helm/ocaml/paramodulation/saturation.ml | 4 +- helm/ocaml/tactics/autoTactic.ml | 4 +- helm/ocaml/tactics/continuationals.ml | 22 +- helm/ocaml/tactics/continuationals.mli | 2 +- helm/ocaml/tactics/discriminationTactics.ml | 16 +- helm/ocaml/tactics/eliminationTactics.ml | 2 +- helm/ocaml/tactics/equalityTactics.ml | 12 +- helm/ocaml/tactics/fourierR.ml | 2 +- helm/ocaml/tactics/fwdSimplTactic.ml | 2 +- helm/ocaml/tactics/introductionTactics.ml | 2 +- helm/ocaml/tactics/negationTactics.ml | 4 +- helm/ocaml/tactics/primitiveTactics.ml | 18 +- helm/ocaml/tactics/proofEngineHelpers.ml | 12 +- helm/ocaml/tactics/proofEngineHelpers.mli | 2 +- helm/ocaml/tactics/proofEngineReduction.ml | 6 +- .../tactics/proofEngineStructuralRules.ml | 18 +- helm/ocaml/tactics/proofEngineTypes.ml | 2 +- helm/ocaml/tactics/proofEngineTypes.mli | 2 +- helm/ocaml/tactics/ring.ml | 6 +- helm/ocaml/tactics/tacticals.ml | 10 +- helm/ocaml/tactics/variousTactics.ml | 2 +- 43 files changed, 355 insertions(+), 372 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 20fee8c18..cffb9cf44 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -617,7 +617,7 @@ let generate_projections uri fields status = with CicTypeChecker.TypeCheckerFailure s -> MatitaLog.message - ("Unable to create projection " ^ name ^ " cause: " ^ s); + ("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force s)); status | CicEnvironment.Object_not_found uri -> let depend = UriManager.name_of_uri uri in diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 51c124a9b..7e0996f4f 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -71,11 +71,11 @@ let refine_term metasenv context uri term ugraph = (Ok (term', metasenv')),ugraph1 with | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppterm term)) ; + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppterm term)) ; Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppterm term) (CicRefine.explain_error msg))); + (CicPp.ppterm term) (Lazy.force msg))); Ko,ugraph let refine_obj metasenv context uri obj ugraph = @@ -87,11 +87,11 @@ let refine_obj metasenv context uri obj ugraph = (Ok (obj', metasenv)),ugraph with | CicRefine.Uncertain s -> - debug_print (lazy ("UNCERTAIN!!! [" ^ s ^ "] " ^ CicPp.ppobj obj)) ; + debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force s) ^ "] " ^ CicPp.ppobj obj)) ; Uncertain,ugraph | CicRefine.RefineFailure msg -> debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s" - (CicPp.ppobj obj) (CicRefine.explain_error msg))) ; + (CicPp.ppobj obj) (Lazy.force msg))) ; Ko,ugraph let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () = @@ -921,7 +921,7 @@ in refine_profiler.HExtlib.profile foo () module Trivial = struct - exception Ambiguous_term of string + exception Ambiguous_term of string Lazy.t exception Exit module Callbacks = struct @@ -941,6 +941,6 @@ struct try fst (Disambiguator.disambiguate_term ~dbd ~context ~metasenv ast ?initial_ugraph ~aliases ~universe:None) - with Exit -> raise (Ambiguous_term term) + with Exit -> raise (Ambiguous_term (lazy term)) end diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli index 356b5e117..5b0e0da1e 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.mli +++ b/helm/ocaml/cic_disambiguation/disambiguate.mli @@ -71,7 +71,7 @@ module Make (C : DisambiguateTypes.Callbacks) : Disambiguator module Trivial: sig - exception Ambiguous_term of string + exception Ambiguous_term of string Lazy.t (** disambiguate an _unanmbiguous_ term using dummy callbacks which fail if a * choice from the user is needed to disambiguate the term diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml index 9f3c554c6..99f8fca91 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.ml @@ -28,7 +28,7 @@ open Printf open DisambiguateTypes exception Invalid_choice -exception Choice_not_found of string +exception Choice_not_found of string Lazy.t let num_choices = ref [] @@ -41,7 +41,7 @@ let lookup_num_choices () = !num_choices let lookup_num_by_dsc dsc = try List.find (has_description dsc) !num_choices - with Not_found -> raise (Choice_not_found ("Num with dsc " ^ dsc)) + with Not_found -> raise (Choice_not_found (lazy ("Num with dsc " ^ dsc))) let mk_choice (dsc, args, appl_pattern) = dsc, @@ -63,5 +63,5 @@ let lookup_symbol_by_dsc symbol dsc = (fun (dsc', _, _) -> dsc = dsc') (CicNotationRew.lookup_interpretations symbol)) with CicNotationRew.Interpretation_not_found | Not_found -> - raise (Choice_not_found (sprintf "Symbol %s, dsc %s" symbol dsc)) + raise (Choice_not_found (lazy (sprintf "Symbol %s, dsc %s" symbol dsc))) diff --git a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli index 74dfaaa58..0ad498106 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateChoices.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateChoices.mli @@ -28,7 +28,7 @@ open DisambiguateTypes (** {2 Choice registration low-level interface} *) (** raised by lookup_XXXX below *) -exception Choice_not_found of string +exception Choice_not_found of string Lazy.t (** register a new number choice *) val add_num_choice: codomain_item -> unit diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index fb568613c..60cf5af2e 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -25,7 +25,7 @@ open Printf -exception Elim_failure of string +exception Elim_failure of string Lazy.t exception Can_t_eliminate let debug_print = fun _ -> () @@ -382,9 +382,9 @@ debug_print (lazy (CicPp.ppterm eliminator_body)); try CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph with CicTypeChecker.TypeCheckerFailure msg -> - raise (Elim_failure (sprintf + raise (Elim_failure (lazy (sprintf "type checker failure while type checking:\n%s\nerror:\n%s" - (CicPp.ppterm eliminator_body) msg)) + (CicPp.ppterm eliminator_body) (Lazy.force msg)))) in if not (fst (CicReduction.are_convertible [] eliminator_type computed_type ugraph)) diff --git a/helm/ocaml/cic_proof_checking/cicElim.mli b/helm/ocaml/cic_proof_checking/cicElim.mli index 0d81b7a60..a00ebff42 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.mli +++ b/helm/ocaml/cic_proof_checking/cicElim.mli @@ -28,7 +28,7 @@ exception Can_t_eliminate (** internal error while generating elimination principle *) -exception Elim_failure of string +exception Elim_failure of string Lazy.t (** @param sort target sort, defaults to Type * @param uri inductive type uri diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index c6201ce45..2849bc38a 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -56,7 +56,7 @@ type type_checked_obj = ;; exception AlreadyCooked of string;; -exception CircularDependency of string;; +exception CircularDependency of string Lazy.t;; exception CouldNotFreeze of string;; exception CouldNotUnfreeze of string;; exception Object_not_found of UriManager.uri;; @@ -356,7 +356,7 @@ module Cache : let univ = if o = None then "NO_UNIV" else "" in print_endline (su^" "^univ)) !frozen_list; - raise (CircularDependency (UriManager.string_of_uri uri)) + raise (CircularDependency (lazy (UriManager.string_of_uri uri))) end else if HT.mem cacheOfCookedObjects uri then diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 930754257..55566a614 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -36,7 +36,7 @@ (* *) (****************************************************************************) -exception CircularDependency of string;; +exception CircularDependency of string Lazy.t;; exception Object_not_found of UriManager.uri;; (* as the get cooked, but if not present the object is only fetched, diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 007962097..605b9676e 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -28,8 +28,8 @@ open Printf -exception AssertFailure of string;; -exception TypeCheckerFailure of string;; +exception AssertFailure of string Lazy.t;; +exception TypeCheckerFailure of string Lazy.t;; let fdebug = ref 0;; let debug t context = @@ -39,7 +39,7 @@ let debug t context = CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i in if !fdebug = 0 then - raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) "")) + raise (TypeCheckerFailure (lazy (List.fold_right debug_aux (t::context) ""))) ;; let debug_print = fun _ -> () ;; @@ -49,7 +49,7 @@ let rec split l n = (l,0) -> ([], l) | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) | (_,_) -> - raise (TypeCheckerFailure "Parameters number < left parameters number") + raise (TypeCheckerFailure (lazy "Parameters number < left parameters number")) ;; let debrujin_constructor uri number_of_types = @@ -58,7 +58,7 @@ let debrujin_constructor uri number_of_types = function C.Rel n as t when n <= k -> t | C.Rel _ -> - raise (TypeCheckerFailure "unbound variable found in constructor type") + raise (TypeCheckerFailure (lazy "unbound variable found in constructor type")) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst @@ -82,8 +82,8 @@ 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 (TypeCheckerFailure - ("non-empty explicit named substitution is applied to "^ - "a mutual inductive type which is being defined")) ; + (lazy ("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' = @@ -143,10 +143,10 @@ let rec type_of_constant ~logger uri ugraph = let type_of_te,ugraph' = type_of ~logger te ugraph in let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in if not b' then - raise (TypeCheckerFailure (sprintf + raise (TypeCheckerFailure (lazy (sprintf "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s" (U.string_of_uri uri) (CicPp.ppterm type_of_te) - (CicPp.ppterm ty))) + (CicPp.ppterm ty)))) else ugraph' | C.Constant (_,None,ty,_,_) -> @@ -169,15 +169,15 @@ let rec type_of_constant ~logger uri ugraph = in let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in if not b then - raise (TypeCheckerFailure (sprintf + raise (TypeCheckerFailure (lazy (sprintf "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s" (U.string_of_uri uri) (CicPp.ppterm type_of_te) - (CicPp.ppterm ty))) + (CicPp.ppterm ty)))) else ugraph4 | _ -> - raise (TypeCheckerFailure - ("Unknown constant:" ^ U.string_of_uri uri))) + raise + (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))) in try CicEnvironment.set_type_checking_info uri; @@ -193,7 +193,7 @@ let rec type_of_constant ~logger uri ugraph = (C.Constant (_,_,ty,_,_)),g -> ty,g | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g | _ -> - raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri)) + raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))) and type_of_variable ~logger uri ugraph = let module C = Cic in @@ -214,7 +214,7 @@ and type_of_variable ~logger uri ugraph = let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in if not b then raise (TypeCheckerFailure - ("Unknown variable:" ^ U.string_of_uri uri)) + (lazy ("Unknown variable:" ^ U.string_of_uri uri))) else ugraph'') in @@ -230,7 +230,7 @@ and type_of_variable ~logger uri ugraph = (*debug_print (lazy s);*) ty,ugraph2) | _ -> - raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) + raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri))) and does_not_occur ?(subst=[]) context n nn te = let module C = Cic in @@ -382,7 +382,7 @@ and weakly_positive context n nn uri te = weakly_positive ((Some (name,(C.Decl source)))::context) (n + 1) (nn + 1) uri dest | _ -> - raise (TypeCheckerFailure "Malformed inductive constructor type") + raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) @@ -394,7 +394,7 @@ and instantiate_parameters params c = instantiate_parameters tl (CicSubstitution.subst he ta) | (C.Cast (te,_), _) -> instantiate_parameters params te - | (t,l) -> raise (AssertFailure "1") + | (t,l) -> raise (AssertFailure (lazy "1")) and strictly_positive context n nn te = let module C = Cic in @@ -418,7 +418,7 @@ and strictly_positive context n nn te = (List.length tl = 1, paramsno, ity, cl, name) | _ -> raise (TypeCheckerFailure - ("Unknown inductive type:" ^ U.string_of_uri uri)) + (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) in let (params,arguments) = split tl paramsno in let lifted_params = List.map (CicSubstitution.lift 1) params in @@ -460,23 +460,23 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = C.Rel m when m = n - (indparamsno - k) -> k - 1 | _ -> raise (TypeCheckerFailure - ("Non-positive occurence in mutual inductive definition(s) " ^ - UriManager.string_of_uri uri)) + (lazy ("Non-positive occurence in mutual inductive definition(s) " ^ + 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 (TypeCheckerFailure - ("Non-positive occurence in mutual inductive definition(s) " ^ - UriManager.string_of_uri uri)) + (lazy ("Non-positive occurence in mutual inductive definition(s) " ^ + UriManager.string_of_uri uri))) | C.Rel m when m = i -> if indparamsno = 0 then true else raise (TypeCheckerFailure - ("Non-positive occurence in mutual inductive definition(s) " ^ - UriManager.string_of_uri uri)) + (lazy ("Non-positive occurence in mutual inductive definition(s) " ^ + UriManager.string_of_uri uri))) | C.Prod (C.Anonymous,source,dest) -> strictly_positive context n nn source && are_all_occurrences_positive @@ -495,8 +495,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = uri indparamsno (i+1) (n + 1) (nn + 1) dest | _ -> raise - (TypeCheckerFailure ("Malformed inductive constructor type " ^ - (UriManager.string_of_uri uri))) + (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^ + (UriManager.string_of_uri uri)))) (* Main function to checks the correctness of a mutual *) (* inductive block definition. This is the function *) @@ -538,8 +538,8 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = debrujinedte) then raise - (TypeCheckerFailure ("Non positive occurence in " ^ - U.string_of_uri uri)) + (TypeCheckerFailure + (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) else ugraph' ) ugraph cl in @@ -556,8 +556,8 @@ and check_mutual_inductive_defs uri obj ugraph = typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph | _ -> raise (TypeCheckerFailure ( - "Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) and type_of_mutual_inductive_defs ~logger uri i ugraph = let module C = Cic in @@ -589,8 +589,8 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph = let (_,_,arity,_) = List.nth dl i in arity,ugraph1 | _ -> - raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ - U.string_of_uri uri)) + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) and type_of_mutual_inductive_constr ~logger uri i j ugraph = let module C = Cic in @@ -625,8 +625,8 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = let (_,ty) = List.nth cl (j-1) in ty,ugraph1 | _ -> - raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) and recursive_args context n nn te = let module C = Cic in @@ -637,20 +637,20 @@ and recursive_args context n nn te = | C.Sort _ | C.Implicit _ | C.Cast _ (*CSC ??? *) -> - raise (AssertFailure "3") (* due to type-checking *) + raise (AssertFailure (lazy "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 (AssertFailure "4") (* due to type-checking *) + raise (AssertFailure (lazy "4")) (* due to type-checking *) | C.Appl _ -> [] - | C.Const _ -> raise (AssertFailure "5") + | C.Const _ -> raise (AssertFailure (lazy "5")) | C.MutInd _ | C.MutConstruct _ | C.MutCase _ | C.Fix _ - | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *) + | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *) and get_new_safes ~subst context p c rl safes n nn x = let module C = Cic in @@ -679,9 +679,9 @@ and get_new_safes ~subst context p c rl safes n nn x = (* CSC: particular, this means that a new (C.Prod, x,_) case *) (* CSC: must be considered in this match. (e.g. x = MutCase) *) raise - (AssertFailure + (AssertFailure (lazy (Printf.sprintf "Get New Safes: c=%s ; p=%s" - (CicPp.ppterm c) (CicPp.ppterm p))) + (CicPp.ppterm c) (CicPp.ppterm p)))) and split_prods ~subst context n te = let module C = Cic in @@ -690,7 +690,7 @@ and split_prods ~subst context n te = (0, _) -> context,te | (n, C.Prod (name,so,ta)) when n > 0 -> split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta - | (_, _) -> raise (AssertFailure "8") + | (_, _) -> raise (AssertFailure (lazy "8")) and eat_lambdas ~subst context n te = let module C = Cic in @@ -703,7 +703,7 @@ and eat_lambdas ~subst context n te = in (te, k + 1, context') | (n, te) -> - raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te))) + raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))) (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) and check_is_really_smaller_arg ~subst context n nn kl x safes te = @@ -726,7 +726,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = check_is_really_smaller_arg ~subst n nn kl x safes so && check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta*) - | C.Prod _ -> raise (AssertFailure "10") + | C.Prod _ -> raise (AssertFailure (lazy "10")) | C.Lambda (name,so,ta) -> check_is_really_smaller_arg ~subst context n nn kl x safes so && check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context) @@ -739,9 +739,9 @@ and check_is_really_smaller_arg ~subst 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 ~subst context n nn kl x safes he - | C.Appl [] -> raise (AssertFailure "11") + | C.Appl [] -> raise (AssertFailure (lazy "11")) | C.Const _ - | C.MutInd _ -> raise (AssertFailure "12") + | C.MutInd _ -> raise (AssertFailure (lazy "12")) | C.MutConstruct _ -> false | C.MutCase (uri,i,outtype,term,pl) -> (match term with @@ -763,8 +763,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) in if not isinductive then List.fold_right @@ -777,7 +777,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = List.combine pl cl with Invalid_argument _ -> - raise (TypeCheckerFailure "not enough patterns") + raise (TypeCheckerFailure (lazy "not enough patterns")) in List.fold_right (fun (p,(_,c)) i -> @@ -809,8 +809,8 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = (tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) in if not isinductive then List.fold_right @@ -823,7 +823,7 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = List.combine pl cl with Invalid_argument _ -> - raise (TypeCheckerFailure "not enough patterns") + raise (TypeCheckerFailure (lazy "not enough patterns")) in (*CSC: supponiamo come prima che nessun controllo sia necessario*) (*CSC: sugli argomenti di una applicazione *) @@ -883,7 +883,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = | Some (_,C.Def (bo,_)) -> guarded_by_destructors ~subst context m nn kl x safes (CicSubstitution.lift m bo) - | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") + | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) ) | C.Meta _ | C.Sort _ @@ -947,8 +947,8 @@ and guarded_by_destructors ~subst context n nn kl x safes = (tys,len,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) in if not isinductive then guarded_by_destructors ~subst context n nn kl x safes outtype && @@ -964,7 +964,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = List.combine pl cl with Invalid_argument _ -> - raise (TypeCheckerFailure "not enough patterns") + raise (TypeCheckerFailure (lazy "not enough patterns")) in guarded_by_destructors ~subst context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) @@ -995,8 +995,8 @@ and guarded_by_destructors ~subst context n nn kl x safes = (tys,List.length tl,isinductive,paramsno,cl') | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) in if not isinductive then guarded_by_destructors ~subst context n nn kl x safes outtype && @@ -1012,7 +1012,7 @@ and guarded_by_destructors ~subst context n nn kl x safes = List.combine pl cl with Invalid_argument _ -> - raise (TypeCheckerFailure "not enough patterns") + raise (TypeCheckerFailure (lazy "not enough patterns")) in guarded_by_destructors ~subst context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) @@ -1086,7 +1086,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = | C.Prod _ | C.LetIn _ -> (* the term has just been type-checked *) - raise (AssertFailure "17") + raise (AssertFailure (lazy "17")) | C.Lambda (name,so,de) -> does_not_occur ~subst context n nn so && guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context) @@ -1107,24 +1107,24 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = let (_,cons) = List.nth cl (j - 1) in CicSubstitution.subst_vars exp_named_subst cons | _ -> - raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) in let rec analyse_branch context ty te = match CicReduction.whd ~subst context ty with - C.Meta _ -> raise (AssertFailure "34") + C.Meta _ -> raise (AssertFailure (lazy "34")) | C.Rel _ | C.Var _ | C.Sort _ -> does_not_occur ~subst context n nn te | C.Implicit _ | C.Cast _ -> - raise (AssertFailure "24")(* due to type-checking *) + raise (AssertFailure (lazy "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 (AssertFailure "25")(* due to type-checking *) + raise (AssertFailure (lazy "25"))(* due to type-checking *) | C.Appl ((C.MutInd (uri,_,_))::_) as ty when uri == coInductiveTypeURI -> guarded_by_constructors ~subst context n nn true te [] @@ -1134,19 +1134,19 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = coInductiveTypeURI | C.Appl _ -> does_not_occur ~subst context n nn te - | C.Const _ -> raise (AssertFailure "26") + | C.Const _ -> raise (AssertFailure (lazy "26")) | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> guarded_by_constructors ~subst context n nn true te [] coInductiveTypeURI | C.MutInd _ -> does_not_occur ~subst context n nn te - | C.MutConstruct _ -> raise (AssertFailure "27") + | C.MutConstruct _ -> raise (AssertFailure (lazy "27")) (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) (*CSC: in head position. *) | C.MutCase _ | C.Fix _ | C.CoFix _ -> - raise (AssertFailure "28")(* due to type-checking *) + raise (AssertFailure (lazy "28"))(* due to type-checking *) in let rec analyse_instantiated_type context ty l = match CicReduction.whd ~subst context ty with @@ -1155,7 +1155,7 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = | C.Meta _ | C.Sort _ | C.Implicit _ - | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *) + | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *) | C.Prod (name,so,de) -> begin match l with @@ -1167,21 +1167,21 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = end | C.Lambda _ | C.LetIn _ -> - raise (AssertFailure "30")(* due to type-checking *) + raise (AssertFailure (lazy "30"))(* due to type-checking *) | C.Appl _ -> List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.Const _ -> raise (AssertFailure "31") + | C.Const _ -> raise (AssertFailure (lazy "31")) | C.MutInd _ -> List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.MutConstruct _ -> raise (AssertFailure "32") + | C.MutConstruct _ -> raise (AssertFailure (lazy "32")) (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) (*CSC: in head position. *) | C.MutCase _ | C.Fix _ | C.CoFix _ -> - raise (AssertFailure "33")(* due to type-checking *) + raise (AssertFailure (lazy "33"))(* due to type-checking *) in let rec instantiate_type args consty = function @@ -1200,7 +1200,7 @@ and guarded_by_constructors ~subst 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 (AssertFailure "23") + raise (AssertFailure (lazy "23")) end | [] -> analyse_instantiated_type context consty' l (* These are all the other cases *) @@ -1301,8 +1301,8 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i (List.length cl = 1 || List.length cl = 0) , ugraph | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) ) | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph @@ -1328,8 +1328,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i false,ugraph ) cl (true,ugraph)) | _ -> - raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) ) | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph (* TASSI: da verificare *) @@ -1350,8 +1351,9 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i (List.length cl = 1 || List.length cl = 0),ugraph1 | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + (lazy + ("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))) @@ -1383,11 +1385,11 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i false,ugraph ) cl (true,ugraph1)) | _ -> - raise (TypeCheckerFailure + raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + UriManager.string_of_uri uri))) ) - | _ -> raise (AssertFailure "19") + | _ -> raise (AssertFailure (lazy "19")) ) | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy -> (* TASSI: da verificare *) @@ -1419,7 +1421,7 @@ and type_of_branch ~subst context argsno need_dummy outtype term constype = C.Prod (C.Anonymous,so,type_of_branch ~subst ((Some (name,(C.Decl so)))::context) argsno need_dummy (CicSubstitution.lift 1 outtype) term' de) - | _ -> raise (AssertFailure "20") + | _ -> raise (AssertFailure (lazy "20")) (* check_metasenv_consistency checks that the "canonical" context of a metavariable is consitent - up to relocation via the relocation list l - @@ -1457,7 +1459,7 @@ and check_metasenv_consistency ~logger ~subst metasenv context if not b then raise (TypeCheckerFailure - (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t))) + (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))) else ugraph1 | Some t,Some (_,C.Decl ct) -> @@ -1469,15 +1471,15 @@ and check_metasenv_consistency ~logger ~subst metasenv context in if not b then raise (TypeCheckerFailure - (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" + (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" (CicPp.ppterm ct) (CicPp.ppterm t) - (CicPp.ppterm type_t))) + (CicPp.ppterm type_t)))) else ugraph2 | None, _ -> raise (TypeCheckerFailure - ("Not well typed metavariable local context: "^ - "an hypothesis, that is not hidden, is not instantiated")) + (lazy ("Not well typed metavariable local context: "^ + "an hypothesis, that is not hidden, is not instantiated"))) ) ugraph l lifted_canonical_context @@ -1502,10 +1504,10 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ; type_of_aux ~logger context (S.lift n bo) ugraph | None -> raise - (TypeCheckerFailure "Reference to deleted hypothesis") + (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) with _ -> - raise (TypeCheckerFailure "unbound variable") + raise (TypeCheckerFailure (lazy "unbound variable")) ) | C.Var (uri,exp_named_subst) -> incr fdebug ; @@ -1540,7 +1542,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (C.Sort (C.Type t')),ugraph1 (* TASSI: CONSTRAINTS *) | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph - | C.Implicit _ -> raise (AssertFailure "21") + | C.Implicit _ -> raise (AssertFailure (lazy "21")) | C.Cast (te,ty) as t -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in @@ -1551,7 +1553,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ty,ugraph3 else raise (TypeCheckerFailure - (sprintf "Invalid cast %s" (CicPp.ppterm t))) + (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t)))) | C.Prod (name,s,t) -> let sort1,ugraph1 = type_of_aux ~logger context s ugraph in let sort2,ugraph2 = @@ -1565,9 +1567,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Sort _ -> () | _ -> raise - (TypeCheckerFailure (sprintf + (TypeCheckerFailure (lazy (sprintf "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) - (CicPp.ppterm sort1))) + (CicPp.ppterm sort1)))) ) ; let type2,ugraph2 = type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 @@ -1606,7 +1608,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* TASSI: questa c'era nel mio... ma non nel CVS... *) (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) eat_prods ~subst context hetype tlbody_and_type ugraph2 - | C.Appl _ -> raise (AssertFailure "Appl: no arguments") + | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments")) | C.Const (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = @@ -1668,9 +1670,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | _ -> raise (TypeCheckerFailure - (sprintf + (lazy (sprintf "Malformed case analasys' output type %s" - (CicPp.ppterm outtype))) + (CicPp.ppterm outtype)))) in (* let (parameters, arguments, exp_named_subst),ugraph2 = @@ -1686,9 +1688,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = else raise (TypeCheckerFailure - (sprintf + (lazy (sprintf ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri) i)) + (CicPp.ppterm typ) (U.string_of_uri uri) i))) | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> if U.eq uri uri' && i = i' then @@ -1698,18 +1700,18 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = else raise (TypeCheckerFailure - (sprintf + (lazy (sprintf ("Case analysys: analysed term type is %s, "^ "but is expected to be (an application of) "^ "%s#1/%d{_}") - (CicPp.ppterm typ') (U.string_of_uri uri) i)) + (CicPp.ppterm typ') (U.string_of_uri uri) i))) | _ -> raise (TypeCheckerFailure - (sprintf + (lazy (sprintf ("Case analysis: "^ "analysed term %s is not an inductive one") - (CicPp.ppterm term))) + (CicPp.ppterm term)))) *) let (b, k) = guess_args context outsort in if not b then (b, k - 1) else (b, k) in @@ -1721,9 +1723,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ([],[],exp_named_subst),ugraph2 else raise (TypeCheckerFailure - (sprintf + (lazy (sprintf ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)) + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> if U.eq uri uri' && i = i' then @@ -1732,15 +1734,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in (params,args,exp_named_subst),ugraph2 else raise (TypeCheckerFailure - (sprintf + (lazy (sprintf ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)) + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) | _ -> raise (TypeCheckerFailure - (sprintf + (lazy (sprintf "Case analysis: analysed term %s is not an inductive one" - (CicPp.ppterm term))) + (CicPp.ppterm term)))) in (* let's control if the sort elimination is allowed: @@ -1760,7 +1762,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in if not b then raise - (TypeCheckerFailure ("Case analasys: sort elimination not allowed")); + (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed"))); (* let's check if the type of branches are right *) let parsno = let obj,_ = @@ -1772,8 +1774,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = C.InductiveDefinition (_,_,parsno,_) -> parsno | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) in let (_,branches_ok,ugraph5) = List.fold_left @@ -1807,7 +1809,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in if not branches_ok then raise - (TypeCheckerFailure "Case analysys: wrong branch type"); + (TypeCheckerFailure (lazy "Case analysys: wrong branch type")); let arguments' = if not need_dummy then outtype::arguments@[term] else outtype::arguments in @@ -1849,12 +1851,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (len + eaten) kl 1 [] m) then raise (TypeCheckerFailure - ("Fix: not guarded by destructors")) + (lazy ("Fix: not guarded by destructors"))) else ugraph2 end else - raise (TypeCheckerFailure ("Fix: ill-typed bodies")) + raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) ) ugraph1 fl in (*CSC: controlli mancanti solo su D{f,k,x,M} *) let (_,_,ty,_) = List.nth fl i in @@ -1886,7 +1888,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = None -> raise (TypeCheckerFailure - ("CoFix: does not return a coinductive type")) + (lazy "CoFix: does not return a coinductive type")) | Some uri -> (* let's control the guarded by constructors @@ -1896,13 +1898,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (types @ context) 0 len false bo [] uri) then raise (TypeCheckerFailure - ("CoFix: not guarded by constructors")) + (lazy "CoFix: not guarded by constructors")) else ugraph2 end else raise - (TypeCheckerFailure ("CoFix: ill-typed bodies")) + (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) ) ugraph1 fl in let (_,ty,_) = List.nth fl i in @@ -1931,7 +1933,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ~subst ~metasenv context typeoft typeofvar ugraph2) ; fdebug := 0 ; debug typeoft [typeofvar] ; - raise (TypeCheckerFailure "Wrong Explicit Named Substitution") + raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in check_exp_named_subst_aux ~logger [] ugraph @@ -1958,9 +1960,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> t2',ugraph - | (_,_) -> raise (TypeCheckerFailure (sprintf + | (_,_) -> raise (TypeCheckerFailure (lazy (sprintf "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1') - (CicPp.ppterm t2'))) + (CicPp.ppterm t2')))) and eat_prods ~subst context hetype l ugraph = (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) @@ -1990,13 +1992,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = debug s [hety] ; raise (TypeCheckerFailure - (sprintf + (lazy (sprintf ("Appl: wrong parameter-type, expected %s, found %s") - (CicPp.ppterm hetype) (CicPp.ppterm s))) + (CicPp.ppterm hetype) (CicPp.ppterm s)))) end | _ -> raise (TypeCheckerFailure - "Appl: this is not a function, it cannot be applied") + (lazy "Appl: this is not a function, it cannot be applied")) ) and returns_a_coinductive ~subst context ty = @@ -2015,8 +2017,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = if is_inductive then None else (Some uri) | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) ) | C.Appl ((C.MutInd (uri,i,_))::_) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in @@ -2026,8 +2028,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = if is_inductive then None else (Some uri) | _ -> raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) ) | C.Prod (n,so,de) -> returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de @@ -2081,7 +2083,7 @@ let typecheck_obj0 ~logger uri ugraph = let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in if not b then raise (TypeCheckerFailure - ("the type of the body is not the one expected")) + (lazy "the type of the body is not the one expected")) else ugraph | C.Constant (_,None,ty,_,_) -> @@ -2104,9 +2106,9 @@ let typecheck_obj0 ~logger uri ugraph = in let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in if not b then - raise (TypeCheckerFailure (sprintf + raise (TypeCheckerFailure (lazy (sprintf "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s" - (CicPp.ppterm type_of_te) (CicPp.ppterm ty))) + (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))) else ugraph | C.Variable (_,bo,ty,_,_) -> @@ -2119,7 +2121,7 @@ let typecheck_obj0 ~logger uri ugraph = let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in if not b then raise (TypeCheckerFailure - ("the body is not the one expected")) + (lazy "the body is not the one expected")) else ugraph ) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index 5cbda28d6..675b548dc 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -24,8 +24,8 @@ *) (* These are the only exceptions that will be raised *) -exception TypeCheckerFailure of string -exception AssertFailure of string +exception TypeCheckerFailure of string Lazy.t +exception AssertFailure of string Lazy.t val debrujin_constructor : UriManager.uri -> int -> Cic.term -> Cic.term diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 614faf6df..dfa47e469 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -68,9 +68,9 @@ context length: %d (avg = %.2f) -exception MetaSubstFailure of string -exception Uncertain of string -exception AssertFailure of string +exception MetaSubstFailure of string Lazy.t +exception Uncertain of string Lazy.t +exception AssertFailure of string Lazy.t exception DeliftingARelWouldCaptureAFreeVariable;; let debug_print = fun _ -> () @@ -536,10 +536,10 @@ let rec restrict subst to_be_restricted metasenv = (more @ more_to_be_restricted @ more_to_be_restricted', metasenv') with Occur -> - raise (MetaSubstFailure (sprintf + raise (MetaSubstFailure (lazy (sprintf "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" - n (names_of_context_indexes context to_be_restricted)))) - metasenv ([], []) + n (names_of_context_indexes context to_be_restricted))))) + metasenv ([], []) in let (more_to_be_restricted', subst) = (* restrict subst *) List.fold_right @@ -567,10 +567,10 @@ let rec restrict subst to_be_restricted metasenv = @ more_to_be_restricted'@more_to_be_restricted'' in (more, subst') with Occur -> - let error_msg = sprintf + let error_msg = lazy (sprintf "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" n (names_of_context_indexes context to_be_restricted) n - (ppterm subst term) + (ppterm subst term)) in (* DEBUG debug_print (lazy error_msg); @@ -623,10 +623,10 @@ let delift n subst context metasenv l t = deliftaux k (S.lift m t) | Some (_,C.Decl t) -> C.Rel ((position (m-k) l) + k) - | None -> raise (MetaSubstFailure "RelToHiddenHypothesis") + | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) with Failure _ -> - raise (MetaSubstFailure "Unbound variable found in deliftaux") + raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) ) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = @@ -640,9 +640,9 @@ let delift n subst context metasenv l t = with CicUtil.Subst_not_found _ -> (* see the top level invariant *) if (i = n) then - raise (MetaSubstFailure (sprintf + raise (MetaSubstFailure (lazy (sprintf "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" - i (ppterm subst t))) + i (ppterm subst t)))) else begin (* I do not consider the term associated to ?i in subst since *) @@ -724,13 +724,13 @@ debug_print(lazy (sprintf (List.map (function Some t -> ppterm subst t | None -> "_") l )))); *) - raise (Uncertain (sprintf + raise (Uncertain (lazy (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) (String.concat "; " (List.map (function Some t -> ppterm subst t | None -> "_") - l)))) + l))))) in let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 7d78cec5c..890a347b0 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -23,9 +23,9 @@ * http://helm.cs.unibo.it/ *) -exception MetaSubstFailure of string -exception Uncertain of string -exception AssertFailure of string +exception MetaSubstFailure of string Lazy.t +exception Uncertain of string Lazy.t +exception AssertFailure of string Lazy.t exception DeliftingARelWouldCaptureAFreeVariable;; (* The entry (i,t) in a substitution means that *) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index e3392bf05..120fdceaa 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -25,18 +25,9 @@ open Printf -type failure_msg = - Reason of string - | UnificationFailure of CicUnification.failure_msg - -let explain_error = - function - Reason msg -> msg - | UnificationFailure msg -> CicUnification.explain_error msg - -exception RefineFailure of failure_msg;; -exception Uncertain of string;; -exception AssertFailure of string;; +exception RefineFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; let debug_print = fun _ -> () @@ -48,7 +39,7 @@ let foo () = CicUnification.fo_unif_subst subst context metasenv t1 t2 ugraph in profiler.HExtlib.profile foo () with - (CicUnification.UnificationFailure msg) -> raise (RefineFailure (UnificationFailure msg)) + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; @@ -56,7 +47,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 (AssertFailure "split: list too short") + | (_,_) -> raise (AssertFailure (lazy "split: list too short")) ;; let rec type_of_constant uri ugraph = @@ -74,7 +65,7 @@ let rec type_of_constant uri ugraph = | C.CurrentProof (_,_,_,ty,_,_) -> ty,u | _ -> raise - (RefineFailure (Reason ("Unknown constant definition " ^ U.string_of_uri uri))) + (RefineFailure (lazy ("Unknown constant definition " ^ U.string_of_uri uri))) and type_of_variable uri ugraph = let module C = Cic in @@ -91,7 +82,7 @@ and type_of_variable uri ugraph = | _ -> raise (RefineFailure - (Reason ("Unknown variable definition " ^ UriManager.string_of_uri uri))) + (lazy ("Unknown variable definition " ^ UriManager.string_of_uri uri))) and type_of_mutual_inductive_defs uri i ugraph = let module C = Cic in @@ -110,7 +101,7 @@ and type_of_mutual_inductive_defs uri i ugraph = | _ -> raise (RefineFailure - (Reason ("Unknown mutual inductive definition " ^ U.string_of_uri uri))) + (lazy ("Unknown mutual inductive definition " ^ U.string_of_uri uri))) and type_of_mutual_inductive_constr uri i j ugraph = let module C = Cic in @@ -130,7 +121,7 @@ and type_of_mutual_inductive_constr uri i j ugraph = | _ -> raise (RefineFailure - (Reason ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) + (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -169,8 +160,8 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de ugraph1 - | _ -> raise (AssertFailure "Wrong number of arguments")) - | _ -> raise (AssertFailure "Prod or MutInd expected") + | _ -> raise (AssertFailure (lazy "Wrong number of arguments"))) + | _ -> raise (AssertFailure (lazy "Prod or MutInd expected")) and type_of_aux' metasenv context t ugraph = let rec type_of_aux subst metasenv context t ugraph = @@ -193,9 +184,9 @@ and type_of_aux' metasenv context t ugraph = (S.lift n bo) ugraph in t,ty,subst,metasenv,ugraph - | None -> raise (RefineFailure (Reason "Rel to hidden hypothesis")) + | None -> raise (RefineFailure (lazy "Rel to hidden hypothesis")) with - _ -> raise (RefineFailure (Reason "Not a close term")) + _ -> raise (RefineFailure (lazy "Not a close term")) ) | C.Var (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = @@ -235,7 +226,7 @@ and type_of_aux' metasenv context t ugraph = t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1 | C.Sort _ -> t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph - | C.Implicit _ -> raise (AssertFailure "21") + | C.Implicit _ -> raise (AssertFailure (lazy "21")) | C.Cast (te,ty) -> let ty',_,subst',metasenv',ugraph1 = type_of_aux subst metasenv context ty ugraph @@ -250,7 +241,7 @@ and type_of_aux' metasenv context t ugraph = in C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 with - _ -> raise (RefineFailure (Reason "Cast"))) + _ -> raise (RefineFailure (lazy "Cast"))) | C.Prod (name,s,t) -> let s',sort1,subst',metasenv',ugraph1 = type_of_aux subst metasenv context s ugraph @@ -284,7 +275,7 @@ and type_of_aux' metasenv context t ugraph = | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> raise exn | CoercGraph.NotMetaClosed -> - raise (Uncertain "Coercions on metas") + raise (Uncertain (lazy "Coercions on metas")) | CoercGraph.SomeCoercion c -> Cic.Appl [c;t]) in (* this is probably not the best... *) @@ -322,7 +313,7 @@ and type_of_aux' metasenv context t ugraph = C.Meta _ | C.Sort _ -> () | _ -> - raise (RefineFailure (Reason (sprintf + raise (RefineFailure (lazy (sprintf "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1)))) @@ -366,7 +357,7 @@ and type_of_aux' metasenv context t ugraph = hetype tlbody_and_type ugraph2 in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 - | C.Appl _ -> raise (RefineFailure (Reason "Appl: no arguments")) + | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) | C.Const (uri,exp_named_subst) -> let exp_named_subst',subst',metasenv',ugraph1 = check_exp_named_subst subst metasenv context @@ -410,7 +401,7 @@ and type_of_aux' metasenv context t ugraph = | _ -> raise (RefineFailure - (Reason ("Unkown mutual inductive definition " ^ + (lazy ("Unkown mutual inductive definition " ^ U.string_of_uri uri))) in let rec count_prod t = @@ -613,7 +604,7 @@ and type_of_aux' metasenv context t ugraph = None,ugraph4,metasenv,subst in match candidate with - | None -> raise (Uncertain "can't solve an higher order unification problem") + | None -> raise (Uncertain (lazy "can't solve an higher order unification problem")) | Some candidate -> let subst,metasenv,ugraph = fo_unif_subst subst context metasenv @@ -769,7 +760,7 @@ and type_of_aux' metasenv context t ugraph = let subst',metasenv',ugraph' = (try fo_unif_subst subst context metasenv t ct ugraph - with e -> raise (RefineFailure (Reason (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t],subst',metasenv',ugraph' | Some t,Some (_,C.Decl ct) -> @@ -780,11 +771,11 @@ and type_of_aux' metasenv context t ugraph = (try fo_unif_subst subst' context metasenv' inferredty ct ugraph1 - with e -> raise (RefineFailure (Reason (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e)))))) + with e -> raise (RefineFailure (lazy (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> Lazy.force msg | _ -> (Printexc.to_string e)))))) in l @ [Some t'], subst'',metasenv'',ugraph2 | None, Some _ -> - raise (RefineFailure (Reason (sprintf + raise (RefineFailure (lazy (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context)))) @@ -793,7 +784,7 @@ and type_of_aux' metasenv context t ugraph = Invalid_argument _ -> raise (RefineFailure - (Reason (sprintf + (lazy (sprintf "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context)))) @@ -827,7 +818,7 @@ and type_of_aux' metasenv context t ugraph = fo_unif_subst metasubst' context metasenv' typeoft typeofvar ugraph2 with _ -> - raise (RefineFailure (Reason + raise (RefineFailure (lazy ("Wrong Explicit Named Substitution: " ^ CicMetaSubst.ppterm metasubst' typeoft ^ " not unifiable with " ^ @@ -877,7 +868,7 @@ and type_of_aux' metasenv context t ugraph = | _,_ -> raise (RefineFailure - (Reason + (lazy (sprintf ("Two sorts were expected, found %s " ^^ "(that reduces to %s) and %s (that reduces to %s)") @@ -965,7 +956,7 @@ and type_of_aux' metasenv context t ugraph = | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> raise exn | CoercGraph.NotMetaClosed -> - raise (Uncertain "Coercions on meta") + raise (Uncertain (lazy "Coercions on meta")) | CoercGraph.SomeCoercion c -> (Cic.Appl [ c ; hete ]), subst, metasenv, ugraph in @@ -1035,7 +1026,7 @@ let type_of_aux' metasenv context term ugraph = try type_of_aux' metasenv context term ugraph with - CicUniv.UniverseInconsistency msg -> raise (RefineFailure (Reason msg)) + CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg)) (*CSC: this is a very very rough approximation; to be finished *) let are_all_occurrences_positive uri = @@ -1045,7 +1036,7 @@ let are_all_occurrences_positive uri = Cic.Appl (Cic.MutInd (uri',_,_)::_) when uri = uri' -> () | Cic.MutInd (uri',_,_) when uri = uri' -> () | Cic.Prod (_,_,t) -> aux t - | _ -> raise (RefineFailure (Reason "not well formed constructor type")) + | _ -> raise (RefineFailure (lazy "not well formed constructor type")) in aux @@ -1074,7 +1065,7 @@ let typecheck metasenv uri obj = (* instead of raising Uncertain, let's hope that the meta will become a sort *) | Cic.Meta _ -> () - | _ -> raise (RefineFailure (Reason "The term provided is not a type")) + | _ -> raise (RefineFailure (lazy "The term provided is not a type")) end; let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in let bo' = CicMetaSubst.apply_subst subst bo' in diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index 24a6c276f..ef089cabf 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -23,12 +23,9 @@ * http://cs.unibo.it/helm/. *) -type failure_msg -exception RefineFailure of failure_msg;; -exception Uncertain of string;; -exception AssertFailure of string;; - -val explain_error: failure_msg -> string +exception RefineFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; (* type_of_aux' metasenv context term graph *) (* refines [term] and returns the refined form of [term], *) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index d8a078997..a2a98bd0d 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,25 +25,25 @@ open Printf -type failure_msg = - Reason of string - | Enriched of string * Cic.substitution * Cic.context * Cic.metasenv * - Cic.term * Cic.term * CicUniv.universe_graph - -let failure_msg_of_string msg = Reason msg - -exception UnificationFailure of failure_msg;; -exception Uncertain of string;; -exception AssertFailure of failure_msg;; +exception UnificationFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; let debug_print = fun _ -> () +let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'" +let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand" +let profiler_deref = HExtlib.profile "fo_unif_subst.deref'" +let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible" + let type_of_aux' metasenv subst context term ugraph = +let foo () = try CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph with CicTypeChecker.TypeCheckerFailure msg -> let msg = + lazy (sprintf "Kernel Type checking error: %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." @@ -51,8 +51,10 @@ let type_of_aux' metasenv subst context term ugraph = (CicMetaSubst.ppterm [] term) (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) msg) in - raise (AssertFailure (Reason msg));; + (CicMetaSubst.ppsubst subst) (Lazy.force msg)) in + raise (AssertFailure msg) +in profiler_toa.HExtlib.profile foo () +;; let exists_a_meta l = List.exists (function Cic.Meta _ -> true | _ -> false) l @@ -77,6 +79,10 @@ let rec deref subst t = | t -> t ;; +let deref subst t = + let foo () = deref subst t + in profiler_deref.HExtlib.profile foo () + exception WrongShape;; let eta_reduce after_beta_expansion after_beta_expansion_body before_beta_expansion @@ -112,6 +118,7 @@ let eta_reduce after_beta_expansion after_beta_expansion_body let rec beta_expand test_equality_only metasenv subst context t arg ugraph = let module S = CicSubstitution in let module C = Cic in +let foo () = let rec aux metasenv subst n context t' ugraph = try @@ -256,6 +263,7 @@ let rec beta_expand test_equality_only metasenv subst context t arg ugraph = let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in subst, metasenv, t'', ugraph2 +in profiler_beta_expand.HExtlib.profile foo () and beta_expand_many test_equality_only metasenv subst context t args ugraph = @@ -288,7 +296,9 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = let t1 = deref subst t1 in let t2 = deref subst t2 in let b,ugraph = +let foo () = R.are_convertible ~subst ~metasenv context t1 t2 ugraph +in profiler_are_convertible.HExtlib.profile foo () in if b then subst, metasenv, ugraph @@ -332,7 +342,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ with Exit -> raise - (UnificationFailure (Reason "1")) + (UnificationFailure (lazy "1")) (* (sprintf "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." @@ -340,7 +350,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (CicMetaSubst.ppterm subst t2))) *) | Invalid_argument _ -> raise - (UnificationFailure (Reason "2"))) + (UnificationFailure (lazy "2"))) (* (sprintf "Error trying to unify %s with %s: the lengths of the two local contexts do not match." @@ -375,8 +385,8 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with - UnificationFailure msg ->raise (UnificationFailure msg) - | Uncertain msg -> raise (UnificationFailure (Reason msg)) + UnificationFailure _ as e -> raise e + | Uncertain msg -> raise (UnificationFailure msg) | AssertFailure _ -> debug_print (lazy "siamo allo huge hack"); (* TODO huge hack!!!! @@ -392,7 +402,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ CicMetaSubst.delift n subst context metasenv l t with (CicMetaSubst.MetaSubstFailure msg)-> - raise (UnificationFailure (Reason msg)) + raise (UnificationFailure msg) | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in let t'',ugraph2 = @@ -426,7 +436,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ fo_unif_subst_exp_named_subst test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (Reason "3")) + raise (UnificationFailure (lazy "3")) (* (sprintf "Can't unify %s with %s due to different constants" (CicMetaSubst.ppterm subst t1) @@ -437,7 +447,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (Reason "4")) + raise (UnificationFailure (lazy "4")) (* (sprintf "Can't unify %s with %s due to different inductive principles" (CicMetaSubst.ppterm subst t1) @@ -449,7 +459,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv exp_named_subst1 exp_named_subst2 ugraph else - raise (UnificationFailure (Reason "5")) + raise (UnificationFailure (lazy "5")) (* (sprintf "Can't unify %s with %s due to different inductive constructors" (CicMetaSubst.ppterm subst t1) @@ -487,7 +497,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ test_equality_only subst context metasenv t1 t2 ugraph) (subst,metasenv,ugraph) l1 l2 with (Invalid_argument msg) -> - raise (UnificationFailure (Reason msg))) + raise (UnificationFailure (lazy msg))) | C.Meta (i,l)::args, _ when not(exists_a_meta args) -> (* we verify that none of the args is a Meta, since beta expanding with respoect to a metavariable @@ -564,7 +574,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ ) (subst'',metasenv'',ugraph2) pl1 pl2 with Invalid_argument _ -> - raise (UnificationFailure (Reason "6"))) + raise (UnificationFailure (lazy "6"))) (* (sprintf "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) @@ -573,7 +583,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ if t1 = t2 then subst, metasenv,ugraph else - raise (UnificationFailure (Reason "6")) + raise (UnificationFailure (lazy "6")) (* (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) @@ -607,9 +617,9 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ if b then subst, metasenv, ugraph1 else - raise (* (UnificationFailure "7") *) - (UnificationFailure (Reason (sprintf - "7: Can't unify %s with %s because they are not convertible" + raise + (UnificationFailure (lazy (sprintf + "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) | (C.Prod _, t2) -> @@ -618,7 +628,7 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ C.Prod _ -> fo_unif_subst test_equality_only subst context metasenv t1 t2' ugraph - | _ -> raise (UnificationFailure (Reason "8"))) + | _ -> raise (UnificationFailure (lazy "8"))) | (t1, C.Prod _) -> let t1' = R.whd ~subst context t1 in (match t1' with @@ -627,12 +637,12 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ subst context metasenv t1' t2 ugraph | _ -> (* raise (UnificationFailure "9")) *) raise - (UnificationFailure (Reason (sprintf - "9: Can't unify %s with %s because they are not convertible" + (UnificationFailure (lazy (sprintf + "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))) | (_,_) -> - raise (UnificationFailure (Reason "10")) + raise (UnificationFailure (lazy "10")) (* (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) @@ -656,7 +666,7 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t) ) ens) in - raise (UnificationFailure (Reason (sprintf + raise (UnificationFailure (lazy (sprintf "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2)))) (* A substitution is a (int * Cic.term) list that associates a *) @@ -669,33 +679,29 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv let fo_unif metasenv context t1 t2 ugraph = fo_unif_subst false [] context metasenv t1 t2 ugraph ;; +let enrich_msg msg subst context metasenv t1 t2 ugraph = + lazy + (sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" + (CicMetaSubst.ppterm subst t1) + (try + let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in + CicPp.ppterm ty_t1 + with _ -> "MALFORMED") + (CicMetaSubst.ppterm subst t2) + (try + let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in + CicPp.ppterm ty_t2 + with _ -> "MALFORMED") + (CicMetaSubst.ppcontext subst context) + (CicMetaSubst.ppmetasenv subst metasenv) + (CicMetaSubst.ppsubst subst) (Lazy.force msg)) + let fo_unif_subst subst context metasenv t1 t2 ugraph = try fo_unif_subst false subst context metasenv t1 t2 ugraph with - | AssertFailure (Enriched _ as msg) -> assert false - | AssertFailure (Reason msg) -> - raise (AssertFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph))) - | UnificationFailure (Enriched _ as msg) -> assert false - | UnificationFailure (Reason msg) -> - raise (UnificationFailure (Enriched (msg,subst,context,metasenv,t1,t2,ugraph))) + | AssertFailure msg -> + raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) + | UnificationFailure msg -> + raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph)) ;; - -let explain_error = - function - Reason msg -> msg - | Enriched (msg,subst,context,metasenv,t1,t2,ugraph) -> - sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" - (CicMetaSubst.ppterm subst t1) - (try - let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in - CicPp.ppterm ty_t1 - with _ -> "MALFORMED") - (CicMetaSubst.ppterm subst t2) - (try - let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in - CicPp.ppterm ty_t2 - with _ -> "MALFORMED") - (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv subst metasenv) - (CicMetaSubst.ppsubst subst) msg diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 5887f004d..e1a6c2899 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -23,14 +23,9 @@ * http://cs.unibo.it/helm/. *) -type failure_msg - -exception UnificationFailure of failure_msg;; -exception Uncertain of string;; -exception AssertFailure of failure_msg;; - -val failure_msg_of_string: string -> failure_msg -val explain_error: failure_msg -> string +exception UnificationFailure of string Lazy.t;; +exception Uncertain of string Lazy.t;; +exception AssertFailure of string Lazy.t;; (* fo_unif metasenv context t1 t2 *) (* unifies [t1] and [t2] in a context [context]. *) diff --git a/helm/ocaml/cic_unification/coercDb.ml b/helm/ocaml/cic_unification/coercDb.ml index e636f8759..969d482c1 100644 --- a/helm/ocaml/cic_unification/coercDb.ml +++ b/helm/ocaml/cic_unification/coercDb.ml @@ -24,7 +24,7 @@ *) type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term -exception EqCarrNotImplemented of string +exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed let db = ref [] @@ -48,8 +48,8 @@ let eq_carr src tgt = CicUtil.is_meta_closed t1 && CicUtil.is_meta_closed t2 -> raise (EqCarrNotImplemented - ("Unsupported carr for coercions: " ^ - CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2)) + (lazy ("Unsupported carr for coercions: " ^ + CicPp.ppterm t1 ^ " or " ^ CicPp.ppterm t2))) | _ -> raise EqCarrOnNonMetaClosed let name_of_carr = function diff --git a/helm/ocaml/cic_unification/coercDb.mli b/helm/ocaml/cic_unification/coercDb.mli index 7b0e6c531..2d7a11cae 100644 --- a/helm/ocaml/cic_unification/coercDb.mli +++ b/helm/ocaml/cic_unification/coercDb.mli @@ -25,7 +25,7 @@ (** XXX WARNING: non-reentrant *) type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term -exception EqCarrNotImplemented of string +exception EqCarrNotImplemented of string Lazy.t exception EqCarrOnNonMetaClosed val eq_carr: coerc_carr -> coerc_carr -> bool val coerc_carr_of_term: Cic.term -> coerc_carr diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index 469e334a7..2e69c6486 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -29,7 +29,7 @@ type coercion_search_result = | SomeCoercion of Cic.term | NoCoercion | NotMetaClosed - | NotHandled of string + | NotHandled of string Lazy.t let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () @@ -115,7 +115,7 @@ let generate_composite_closure c1 c2 univ = CicTypeChecker.type_of_aux' [] [] c univ with CicTypeChecker.TypeCheckerFailure s as exn -> debug_print (lazy (sprintf "Generated composite coercion:\n%s\n%s" - (CicPp.ppterm c) s)); + (CicPp.ppterm c) (Lazy.force s))); raise exn in let cleaned_ty = diff --git a/helm/ocaml/cic_unification/coercGraph.mli b/helm/ocaml/cic_unification/coercGraph.mli index dfba8f5dc..fcbed3497 100644 --- a/helm/ocaml/cic_unification/coercGraph.mli +++ b/helm/ocaml/cic_unification/coercGraph.mli @@ -27,7 +27,7 @@ type coercion_search_result = | SomeCoercion of Cic.term | NoCoercion | NotMetaClosed - | NotHandled of string + | NotHandled of string Lazy.t val look_for_coercion : Cic.term -> Cic.term -> coercion_search_result diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 003fb9584..b9f165edb 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -378,8 +378,7 @@ let unification_simple metasenv context t1 t2 ugraph = unif subst menv t s | C.Meta _, t when occurs_check subst s t -> raise - (U.UnificationFailure - (U.failure_msg_of_string "Inference.unification.unif")) + (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Meta (i, l), t -> ( try let _, _, ty = CicUtil.lookup_meta i menv in @@ -400,20 +399,17 @@ let unification_simple metasenv context t1 t2 ugraph = ) | _, C.Meta _ -> unif subst menv t s | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> - raise (U.UnificationFailure - (U.failure_msg_of_string "Inference.unification.unif")) + raise (U.UnificationFailure (lazy "Inference.unification.unif")) | C.Appl (hds::tls), C.Appl (hdt::tlt) -> ( try List.fold_left2 (fun (subst', menv) s t -> unif subst' menv s t) (subst, menv) tls tlt with Invalid_argument _ -> - raise (U.UnificationFailure - (U.failure_msg_of_string "Inference.unification.unif")) + raise (U.UnificationFailure (lazy "Inference.unification.unif")) ) | _, _ -> - raise (U.UnificationFailure - (U.failure_msg_of_string "Inference.unification.unif")) + raise (U.UnificationFailure (lazy "Inference.unification.unif")) in let subst, menv = unif [] metasenv t1 t2 in let menv = diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index fe3cf09f1..c0a7ec611 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -2051,12 +2051,12 @@ let saturate debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!"); debug_print (lazy (CicPp.pp proof names)); raise (ProofEngineTypes.Fail - "Found a proof, but it doesn't typecheck") + (lazy "Found a proof, but it doesn't typecheck")) in debug_print (lazy (Printf.sprintf "\nTIME NEEDED: %.9f" time)); newstatus | _ -> - raise (ProofEngineTypes.Fail "NO proof found") + raise (ProofEngineTypes.Fail (lazy "NO proof found")) ;; (* dummy function called within matita to trigger linkage *) diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml index 9b716637a..b232d9894 100644 --- a/helm/ocaml/tactics/autoTactic.ml +++ b/helm/ocaml/tactics/autoTactic.ml @@ -306,7 +306,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd) let paramodulation_tactic = ref (fun dbd ?full ?depth ?width status -> - raise (ProofEngineTypes.Fail "Not Ready yet..."));; + raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));; let term_is_equality = ref (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);; @@ -325,7 +325,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] with [] -> debug_print(lazy "Auto failed"); - raise (ProofEngineTypes.Fail "No Applicable theorem") + raise (ProofEngineTypes.Fail (lazy "No Applicable theorem")) | (_,(proof,[],_))::_ -> let t2 = Unix.gettimeofday () in debug_print (lazy "AUTO_TAC HA FINITO"); diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml index 5b1bbce3d..f4f9e34f6 100644 --- a/helm/ocaml/tactics/continuationals.ml +++ b/helm/ocaml/tactics/continuationals.ml @@ -25,9 +25,7 @@ open Printf -exception Error of string - -let fail msg = raise (Error msg) +exception Error of string Lazy.t module type Engine = sig @@ -157,8 +155,8 @@ struct match tactical, switch with | Tactic tac, Open n -> E.apply_tactic tac proof n | Skip, Closed n -> proof, [], [n] - | Tactic _, Closed _ -> fail "can't apply tactic to a closed goal" - | Skip, Open _ -> fail "can't skip an open goal" + | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal")) + | Skip, Open _ -> raise (Error (lazy "can't skip an open goal")) let eval continuational status = match continuational, status with @@ -191,7 +189,7 @@ struct | Dot, (proof, (env, todo, left, tag)::tail) -> let env, left = match List.filter is_open env, left with - | [], [] -> fail "There is nothig to do for '.'" + | [], [] -> raise (Error (lazy "There is nothig to do for '.'")) | g::env,left -> [g], union (List.map goal_of env) left | [], g::left -> [dummy_pos, Open g], left in @@ -199,7 +197,7 @@ struct | Branch, (proof, (g1::tl, todo, left, tag)::tail) -> assert (List.length tl >= 1); proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail - | Branch, (_, _) -> fail "can't branch on a singleton context" + | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context")) | Shift opt_pos, (proof, (leftopen, t, l,BranchTag):: (goals, todo, left,tag)::tail) -> let next_goal, rem_goals = @@ -208,19 +206,19 @@ struct | Some pos, _ -> (try list_assoc_extract pos goals - with Not_found -> fail (sprintf "position %d not found" pos)) - | None, [] -> fail "no more goals to shift" + with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos)))) + | None, [] -> raise (Error (lazy "no more goals to shift")) in let t = union t (union (List.map goal_of (List.filter is_open leftopen)) l) in proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail - | Shift _, (_, _) -> fail "no more goals to shift" + | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift")) | Select gl, (proof, stack) -> List.iter (fun g -> if E.is_goal_closed g proof then - fail "you can't select a closed goal") + raise (Error (lazy "you can't select a closed goal"))) gl; (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack) | End, (proof, stack) -> @@ -233,7 +231,7 @@ struct (union not_processed (List.filter is_open leftopen)))) in proof, (env,todo,left,tag)::tail - | _ -> fail "can't end here") + | _ -> raise (Error (lazy "can't end here"))) let init proof = proof, diff --git a/helm/ocaml/tactics/continuationals.mli b/helm/ocaml/tactics/continuationals.mli index e89e2e51d..109dbaf99 100644 --- a/helm/ocaml/tactics/continuationals.mli +++ b/helm/ocaml/tactics/continuationals.mli @@ -23,7 +23,7 @@ * http://helm.cs.unibo.it/ *) -exception Error of string +exception Error of string Lazy.t module type Engine = sig diff --git a/helm/ocaml/tactics/discriminationTactics.ml b/helm/ocaml/tactics/discriminationTactics.ml index b80772827..c9feaaee6 100644 --- a/helm/ocaml/tactics/discriminationTactics.ml +++ b/helm/ocaml/tactics/discriminationTactics.ml @@ -59,7 +59,7 @@ let rec injection_tac ~term = T.then_ ~start:(injection1_tac ~i ~term) ~continuation:(traverse_list (i+1) tl1 tl2) - | _ -> raise (ProofEngineTypes.Fail "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???") ; T.id_tac + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) ; T.id_tac in traverse_list 1 applist1 applist2 | ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)), (C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2))) @@ -73,9 +73,9 @@ let rec injection_tac ~term = (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality but a discriminable one") ; *) T.id_tac | _ -> (* raise (ProofEngineTypes.Fail "Injection: not a projectable equality") ; *) T.id_tac ) - | _ -> raise (ProofEngineTypes.Fail "Injection: not a projectable equality") + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not a projectable equality")) ) - | _ -> raise (ProofEngineTypes.Fail "Injection: not an equation") + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: not an equation")) ) status in ProofEngineTypes.mk_tactic (injection_tac ~term) @@ -138,7 +138,7 @@ and injection1_tac ~term ~i = in aux reduced_cty 1 ) constructor_list - | _ -> raise (ProofEngineTypes.Fail "Discriminate: object is not an Inductive Definition: it's imposible") + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible")) in ProofEngineTypes.apply_tactic (T.thens @@ -158,7 +158,7 @@ and injection1_tac ~term ~i = match gty with (C.Appl (C.MutInd (_,_,_)::arglist)) -> List.nth arglist 1 - | _ -> raise (ProofEngineTypes.Fail "Injection: goal after cut is not correct") + | _ -> raise (ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct")) in ProofEngineTypes.apply_tactic (ReductionTactics.change_tac @@ -187,9 +187,9 @@ and injection1_tac ~term ~i = ) ]) status - | _ -> raise (ProofEngineTypes.Fail "Discriminate: not a discriminable equality") + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not a discriminable equality")) ) - | _ -> raise (ProofEngineTypes.Fail "Discriminate: not an equality") + | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: not an equality")) in ProofEngineTypes.mk_tactic (injection1_tac ~term ~i) ;; @@ -204,7 +204,7 @@ let discriminate'_tac ~term = let module U = UriManager in let module P = PrimitiveTactics in let module T = Tacticals in - let fail msg = raise (ProofEngineTypes.Fail ("Discriminate: " ^ msg)) in + let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in let find_discriminating_consno t1 t2 = let rec aux t1 t2 = match t1, t2 with diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml index 0aa33c2db..bb269411e 100644 --- a/helm/ocaml/tactics/eliminationTactics.ml +++ b/helm/ocaml/tactics/eliminationTactics.ml @@ -97,7 +97,7 @@ let elim_clear_tac ~mk_fresh_name_callback ~types ~what = ~continuation:(S.clear what) in E.apply_tactic tac status - else raise (E.Fail "unexported elim_clear: not an eliminable type") + else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type")) in E.mk_tactic elim_clear_tac diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index c56d3de2d..5a091b7ad 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -62,7 +62,7 @@ let rewrite_tac ~direction ~pattern equality = in let eq_ind = C.Const (ind_uri uri,[]) in if_right_to_left (eq_ind, ty, t2, t1) (eq_ind, ty, t1, t2) - | _ -> raise (PET.Fail "Rewrite: argument is not a proof of an equality") in + | _ -> raise (PET.Fail (lazy "Rewrite: argument is not a proof of an equality")) in (* now we always do as if direction was `LeftToRight *) let fresh_name = FreshNamesGenerator.mk_fresh_name @@ -152,7 +152,7 @@ let replace_tac ~pattern ~with_what = metasenv context with_what CicUniv.empty_ugraph in let whats = match selected_terms_with_context with - [] -> raise (ProofEngineTypes.Fail "Replace: no term selected") + [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected")) | l -> List.map (fun (context_of_t,t) -> @@ -173,7 +173,7 @@ let replace_tac ~pattern ~with_what = (*CSC: we could implement something stronger by completely changing the semantics of the tactic *) raise (ProofEngineTypes.Fail - "Replace: one of the selected terms is not closed") in + (lazy "Replace: one of the selected terms is not closed")) in let ty_of_t_in_context,u = (* TASSI: FIXME *) CicTypeChecker.type_of_aux' metasenv context t_in_context CicUniv.empty_ugraph in @@ -186,7 +186,7 @@ let replace_tac ~pattern ~with_what = else raise (ProofEngineTypes.Fail - "Replace: one of the selected terms and the term to be replaced with have not convertible types") + (lazy "Replace: one of the selected terms and the term to be replaced with have not convertible types")) ) l in let rec aux n whats status = match whats with @@ -255,7 +255,7 @@ let symmetry_tac = ~term: (C.Const (LibraryObjects.sym_eq_URI uri, []))) (proof,goal) - | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") + | _ -> raise (ProofEngineTypes.Fail (lazy "Symmetry failed")) in ProofEngineTypes.mk_tactic symmetry_tac ;; @@ -280,7 +280,7 @@ let transitivity_tac ~term = [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]) status - | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") + | _ -> raise (ProofEngineTypes.Fail (lazy "Transitivity failed")) in ProofEngineTypes.mk_tactic (transitivity_tac ~term) ;; diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml index f586455a2..13dd9f410 100644 --- a/helm/ocaml/tactics/fourierR.ml +++ b/helm/ocaml/tactics/fourierR.ml @@ -900,7 +900,7 @@ let equality_replace a b = let tcl_fail a (proof,goal) = match a with - 1 -> raise (ProofEngineTypes.Fail "fail-tactical") + 1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical")) | _ -> (proof,[goal]) ;; diff --git a/helm/ocaml/tactics/fwdSimplTactic.ml b/helm/ocaml/tactics/fwdSimplTactic.ml index bd2ac9fde..16510a7cd 100644 --- a/helm/ocaml/tactics/fwdSimplTactic.ml +++ b/helm/ocaml/tactics/fwdSimplTactic.ml @@ -38,7 +38,7 @@ module PESR = ProofEngineStructuralRules let fail_msg0 = "unexported clearbody: invalid argument" let fail_msg2 = "fwd: no applicable simplification" -let error msg = raise (PET.Fail msg) +let error msg = raise (PET.Fail (lazy msg)) (* unexported tactics *******************************************************) diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml index f6283cf68..6bf8ab6c1 100644 --- a/helm/ocaml/tactics/introductionTactics.ml +++ b/helm/ocaml/tactics/introductionTactics.ml @@ -35,7 +35,7 @@ let fake_constructor_tac ~n (proof, goal) = PrimitiveTactics.apply_tac ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))) (proof, goal) - | _ -> raise (ProofEngineTypes.Fail "Constructor: failed") + | _ -> raise (ProofEngineTypes.Fail (lazy "Constructor: failed")) ;; let constructor_tac ~n = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n) diff --git a/helm/ocaml/tactics/negationTactics.ml b/helm/ocaml/tactics/negationTactics.ml index e4cd73898..8f05ae436 100644 --- a/helm/ocaml/tactics/negationTactics.ml +++ b/helm/ocaml/tactics/negationTactics.ml @@ -41,7 +41,7 @@ let absurd_tac ~term = term ; ty]) ) status - else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition") + else raise (ProofEngineTypes.Fail (lazy "Absurd: Not a Proposition")) in ProofEngineTypes.mk_tactic (absurd_tac ~term) ;; @@ -65,7 +65,7 @@ let contradiction_tac = ~continuation: VariousTactics.assumption_tac)) status with - (ProofEngineTypes.Fail "Assumption: No such assumption") -> raise (ProofEngineTypes.Fail "Contradiction: No such assumption") + ProofEngineTypes.Fail msg when Lazy.force msg = "Assumption: No such assumption" -> raise (ProofEngineTypes.Fail (lazy "Contradiction: No such assumption")) (* sarebbe piu' elegante se Assumtion sollevasse un'eccezione tutta sua che questa cattura, magari con l'aiuto di try_tactics *) in ProofEngineTypes.mk_tactic contradiction_tac diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 74a9f63f2..d26221d39 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -67,7 +67,7 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = in context, t, (C.Meta (newmeta,irl)) else - raise (Fail "intro(s): not enough products or let-ins") + raise (Fail (lazy "intro(s): not enough products or let-ins")) in collect_context context howmany ty @@ -325,10 +325,9 @@ let apply_tac_verbose_with_subst ~term status = apply_tac_verbose_with_subst ~term status (* TODO cacciare anche altre eccezioni? *) with - | CicUnification.UnificationFailure msg -> - raise (Fail (CicUnification.explain_error msg)) - | CicTypeChecker.TypeCheckerFailure _ as e -> - raise (Fail (Printexc.to_string e)) + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (Fail msg) (* ALB *) let apply_tac_verbose ~term status = @@ -345,10 +344,9 @@ let apply_tac ~term = apply_tac ~term status (* TODO cacciare anche altre eccezioni? *) with - | CicUnification.UnificationFailure msg -> - raise (Fail (CicUnification.explain_error msg)) - | CicTypeChecker.TypeCheckerFailure _ as e -> - raise (Fail (Printexc.to_string e)) + | CicUnification.UnificationFailure msg + | CicTypeChecker.TypeCheckerFailure msg -> + raise (Fail msg) in mk_tactic (apply_tac ~term) @@ -453,7 +451,7 @@ let exact_tac ~term = (newproof, []) end else - raise (Fail "The type of the provided term is not the one expected.") + raise (Fail (lazy "The type of the provided term is not the one expected.")) in mk_tactic (exact_tac ~term) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 51405f5fd..9f7fb42f4 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception Bad_pattern of string +exception Bad_pattern of string Lazy.t let new_meta_of_proof ~proof:(_, metasenv, _, _) = CicMkImplicit.new_meta metasenv [] @@ -231,7 +231,7 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = try List.map2 f l1 l2 with - | Invalid_argument _ -> raise (Bad_pattern error_msg) + | Invalid_argument _ -> raise (Bad_pattern (lazy error_msg)) in let rec aux context where term = match (where, term) with @@ -292,9 +292,9 @@ let select_in_term ~metasenv ~context ~ugraph ~term ~pattern:(wanted,where) = funs1 funs2) | x,y -> raise (Bad_pattern - (Printf.sprintf "Pattern %s versus term %s" + (lazy (Printf.sprintf "Pattern %s versus term %s" (CicPp.ppterm x) - (CicPp.ppterm y))) + (CicPp.ppterm y)))) and auxs context terms1 terms2 = (* as aux for list of terms *) List.concat (map2 "wrong number of arguments in application" (fun t1 t2 -> aux context t1 t2) terms1 terms2) @@ -455,7 +455,7 @@ let pattern_of ?(equality=(==)) ~term terms = in snd (aux term) -exception Fail of string +exception Fail of string Lazy.t (** select metasenv conjecture pattern * select all subterms of [conjecture] matching [pattern]. @@ -678,6 +678,6 @@ let lookup_type metasenv context hyp = | Some (Cic.Name name, Cic.Def (u, _)) :: tail when name = hyp -> p, fst (CicTypeChecker.type_of_aux' metasenv tail u CicUniv.empty_ugraph) | _ :: tail -> aux (succ p) tail - | [] -> raise (ProofEngineTypes.Fail "lookup_type: not premise in the current goal") + | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal")) in aux 1 context diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index a7603d3a5..e28e1425d 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -exception Bad_pattern of string +exception Bad_pattern of string Lazy.t (* Returns the first meta whose number is above the *) (* number of the higher meta. *) diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index f8782b7ae..fc3bfd3b8 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -909,14 +909,14 @@ let unfold ?what context where = | _,_ -> raise (ProofEngineTypes.Fail - "The term to unfold is not a constant, a variable or a bound variable ") + (lazy "The term to unfold is not a constant, a variable or a bound variable ")) in let appl he tl = if tl = [] then he else Cic.Appl (he::tl) in let cannot_delta_expand t = raise (ProofEngineTypes.Fail - ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded")) in + (lazy ("The term " ^ CicPp.ppterm t ^ " cannot be delta-expanded"))) in let rec hd_delta_beta context tl = function Cic.Rel n as t -> @@ -967,7 +967,7 @@ let unfold ?what context where = if res = [] then raise (ProofEngineTypes.Fail - ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where)) + (lazy ("Term "^ CicPp.ppterm what ^ " not found in " ^ CicPp.ppterm where))) else res in diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml index 99c37f801..2c641fd84 100644 --- a/helm/ocaml/tactics/proofEngineStructuralRules.ml +++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml @@ -67,10 +67,10 @@ let clearbody ~hyp = _ -> raise (Fail - ("The correctness of hypothesis " ^ + (lazy ("The correctness of hypothesis " ^ string_of_name n ^ " relies on the body of " ^ hyp) - ) + )) in entry::context | Some (_,Cic.Def (_,Some _)) -> assert false @@ -84,8 +84,8 @@ let clearbody ~hyp = _ -> raise (Fail - ("The correctness of the goal relies on the body of " ^ - hyp)) + (lazy ("The correctness of the goal relies on the body of " ^ + hyp))) in m,canonical_context',ty | t -> t @@ -129,8 +129,8 @@ let clear ~hyp = with _ -> raise (Fail - ("Hypothesis " ^ string_of_name n ^ - " uses hypothesis " ^ hyp)) + (lazy ("Hypothesis " ^ string_of_name n ^ + " uses hypothesis " ^ hyp))) in (b, entry::context) else @@ -138,13 +138,13 @@ let clear ~hyp = ) canonical_context (false, []) in if not context_changed then - raise (Fail ("Hypothesis " ^ hyp ^ " does not exist")); + raise (Fail (lazy ("Hypothesis " ^ hyp ^ " does not exist"))); let _,_ = try CicTypeChecker.type_of_aux' metasenv canonical_context' ty CicUniv.empty_ugraph with _ -> - raise (Fail ("Hypothesis " ^ hyp ^ " occurs in the goal")) + raise (Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal"))) in m,canonical_context',ty | t -> t @@ -161,4 +161,4 @@ let set_goal n = if CicUtil.exists_meta n metasenv then (proof, [n]) else - raise (ProofEngineTypes.Fail ("no such meta: " ^ string_of_int n))) + raise (ProofEngineTypes.Fail (lazy ("no such meta: " ^ string_of_int n)))) diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index ed4a491e1..58dafd1a6 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -83,7 +83,7 @@ let conclusion_pattern t = t',[],Cic.Implicit (Some `Hole) (** tactic failure *) -exception Fail of string +exception Fail of string Lazy.t (** calls the opaque tactic on the status, restoring the original diff --git a/helm/ocaml/tactics/proofEngineTypes.mli b/helm/ocaml/tactics/proofEngineTypes.mli index f45d681c1..40a9e6c80 100644 --- a/helm/ocaml/tactics/proofEngineTypes.mli +++ b/helm/ocaml/tactics/proofEngineTypes.mli @@ -65,7 +65,7 @@ type pattern = lazy_term option * (string * Cic.term) list * Cic.term val conclusion_pattern : Cic.term option -> pattern (** tactic failure *) -exception Fail of string +exception Fail of string Lazy.t val apply_tactic: tactic -> status -> proof * goal list diff --git a/helm/ocaml/tactics/ring.ml b/helm/ocaml/tactics/ring.ml index 8f6369d51..1d7cc10e6 100644 --- a/helm/ocaml/tactics/ring.ml +++ b/helm/ocaml/tactics/ring.ml @@ -366,7 +366,7 @@ let status_of_single_goal_tactic_result = function proof,[goal] -> proof,goal | _ -> - raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal") + raise (Fail (lazy "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")) (* Galla: spostata in variousTactics.ml (** @@ -577,7 +577,7 @@ let ring_tac status = status'')]) status with (Fail s) -> - raise (Fail ("Ring failure: " ^ s)) + raise (Fail (lazy ("Ring failure: " ^ Lazy.force s))) end | _ -> (* impossible: we are applying ring exacty to 2 terms *) assert false @@ -588,7 +588,7 @@ let ring_tac status = try ring_tac status with GoalUnringable -> - raise (Fail "goal unringable") + raise (Fail (lazy "goal unringable")) let ring_tac = ProofEngineTypes.mk_tactic ring_tac diff --git a/helm/ocaml/tactics/tacticals.ml b/helm/ocaml/tactics/tacticals.ml index 94b5d379d..3d5626afa 100644 --- a/helm/ocaml/tactics/tacticals.ml +++ b/helm/ocaml/tactics/tacticals.ml @@ -48,7 +48,7 @@ let fail_tac = let fail_tac (proof,goal) = let _, metasenv, _, _ = proof in let _, _, _ = CicUtil.lookup_meta goal metasenv in - raise (Fail "fail tactical") + raise (Fail (lazy "fail tactical")) in mk_tactic fail_tac @@ -118,7 +118,7 @@ let first ~tactics = first ~tactics status | _ -> raise e (* [e] must not be caught ; let's re-raise it *) ) - | [] -> raise (Fail "first: no tactics left") + | [] -> raise (Fail (lazy "first: no tactics left")) in S.mk_tactic (first ~tactics) @@ -140,8 +140,8 @@ let thens ~start ~continuations = S.set_goals output_status goals with Invalid_argument _ -> - let debug = Printf.sprintf "thens: expected %i new goals, found %i" - (List.length continuations) (List.length new_goals) + let debug = lazy (Printf.sprintf "thens: expected %i new goals, found %i" + (List.length continuations) (List.length new_goals)) in raise (Fail debug) in @@ -272,7 +272,7 @@ let solve_tactics ~tactics = Printexc.to_string e)); solve_tactics ~tactics status ) - | [] -> raise (Fail "solve_tactics cannot solve the goal"); + | [] -> raise (Fail (lazy "solve_tactics cannot solve the goal")); S.apply_tactic S.id_tac status in S.mk_tactic (solve_tactics ~tactics) diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 51f28b3c9..927552f0a 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -55,7 +55,7 @@ let assumption_tac = if b then n else find (n+1) tl | _ -> find (n+1) tl ) - | [] -> raise (PET.Fail "Assumption: No such assumption") + | [] -> raise (PET.Fail (lazy "Assumption: No such assumption")) in PET.apply_tactic (PT.apply_tac ~term:(C.Rel (find 1 context))) status in PET.mk_tactic assumption_tac -- 2.39.2