]> matita.cs.unibo.it Git - helm.git/commitdiff
Every exception that used to have type string is now a string Lazy.t.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 12:37:37 +0000 (12:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 25 Oct 2005 12:37:37 +0000 (12:37 +0000)
43 files changed:
helm/matita/matitaEngine.ml
helm/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_disambiguation/disambiguate.mli
helm/ocaml/cic_disambiguation/disambiguateChoices.ml
helm/ocaml/cic_disambiguation/disambiguateChoices.mli
helm/ocaml/cic_proof_checking/cicElim.ml
helm/ocaml/cic_proof_checking/cicElim.mli
helm/ocaml/cic_proof_checking/cicEnvironment.ml
helm/ocaml/cic_proof_checking/cicEnvironment.mli
helm/ocaml/cic_proof_checking/cicTypeChecker.ml
helm/ocaml/cic_proof_checking/cicTypeChecker.mli
helm/ocaml/cic_unification/cicMetaSubst.ml
helm/ocaml/cic_unification/cicMetaSubst.mli
helm/ocaml/cic_unification/cicRefine.ml
helm/ocaml/cic_unification/cicRefine.mli
helm/ocaml/cic_unification/cicUnification.ml
helm/ocaml/cic_unification/cicUnification.mli
helm/ocaml/cic_unification/coercDb.ml
helm/ocaml/cic_unification/coercDb.mli
helm/ocaml/cic_unification/coercGraph.ml
helm/ocaml/cic_unification/coercGraph.mli
helm/ocaml/paramodulation/inference.ml
helm/ocaml/paramodulation/saturation.ml
helm/ocaml/tactics/autoTactic.ml
helm/ocaml/tactics/continuationals.ml
helm/ocaml/tactics/continuationals.mli
helm/ocaml/tactics/discriminationTactics.ml
helm/ocaml/tactics/eliminationTactics.ml
helm/ocaml/tactics/equalityTactics.ml
helm/ocaml/tactics/fourierR.ml
helm/ocaml/tactics/fwdSimplTactic.ml
helm/ocaml/tactics/introductionTactics.ml
helm/ocaml/tactics/negationTactics.ml
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tactics/proofEngineHelpers.ml
helm/ocaml/tactics/proofEngineHelpers.mli
helm/ocaml/tactics/proofEngineReduction.ml
helm/ocaml/tactics/proofEngineStructuralRules.ml
helm/ocaml/tactics/proofEngineTypes.ml
helm/ocaml/tactics/proofEngineTypes.mli
helm/ocaml/tactics/ring.ml
helm/ocaml/tactics/tacticals.ml
helm/ocaml/tactics/variousTactics.ml

index 20fee8c181b3e2b2835942a3f4f6555a8e30f755..cffb9cf449c30d72cd71741e108d03248209b6a7 100644 (file)
@@ -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
index 51c124a9b5d83824d0f5ba128460d2bc0ef49e6c..7e0996f4f59ef693050b9aef47d03b941c56934a 100644 (file)
@@ -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
 
index 356b5e117274f570634e15167c07ad810d76d2d5..5b0e0da1e24fc0e380dbb395bffce7f73cde1efb 100644 (file)
@@ -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
index 9f3c554c6ec626ae5f4c2a7d3ea28c43940a6540..99f8fca91634c9acb057c8d83beae1d247f6efeb 100644 (file)
@@ -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)))
 
index 74dfaaa58bec3dc215ca1c38631a65bb4b406a5a..0ad498106456a50d50ed4962a530e597b7d1a08f 100644 (file)
@@ -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
index fb568613c943c8b3b7389d9d09d039d8e88b8046..60cf5af2e60031a37579b791985b287a63576a98 100644 (file)
@@ -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))
index 0d81b7a60b9198d8f4374431e58a7581231623d4..a00ebff423c98276e37fefb24a133edb86597284 100644 (file)
@@ -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
index c6201ce458e48b8e03d49924603c19f23231ef22..2849bc38a7f09c33d2c4b3c6789aba69a73b8c66 100644 (file)
@@ -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
index 93075425791fc008e433551051a12cdf0df0a4d4..55566a614493de9ae8b872a0a9347d2cf6a37073 100644 (file)
@@ -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,
index 007962097e03b95c2f8318937e8f93f30f61e4b9..605b9676e2d5befe11e590de052ed9651d4dac9f 100644 (file)
@@ -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
             )
index 5cbda28d638100874cf69a8836492947c996e56b..675b548dc0e169421ac79ca841a47cd01c393813 100644 (file)
@@ -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
 
index 614faf6df15f50d6af219ac90ccacf502afd04fb..dfa47e469bbd97d12ddbf6e83ce39935bd90c526 100644 (file)
@@ -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
index 7d78cec5cd9047210680839e5a2a9d5a89980f2d..890a347b006b879660f9908569c5a0a2de7c83f1 100644 (file)
@@ -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 *)
index e3392bf05ff949b9778aa96eccbe43d56b598aa7..120fdceaa1b5a08452ff30c4398a0d0cad76bebd 100644 (file)
 
 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
index 24a6c276f1757804c9be4d7fadf9bb49ad92a8bc..ef089cabf1a433023d01749a884b7808ef3018e4 100644 (file)
  * 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],  *)
index d8a078997a04ca3e9a1d8de75db88d4da96b90e2..a2a98bd0d8213739796d81de2492cb1446b4242d 100644 (file)
 
 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 
index 5887f004d858d8d6e7c11a49d8dd733c262ab131..e1a6c2899e446026f352c91b33ad4e6c53f13f73 100644 (file)
  * 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]. *)
index e636f87596a8e9e86729bc2c5e0c99e072151b21..969d482c1601de65c62355fda02ed77afc1afb87 100644 (file)
@@ -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
index 7b0e6c5317c15c8c69a99c2ff23419a732c492eb..2d7a11cae0123d31367f18f9b500addc40c85da7 100644 (file)
@@ -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
index 469e334a7358e0b7dcbb03ea32607690a0d32fe5..2e69c648657646867879bebbdafd49148ea7212c 100644 (file)
@@ -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 =
index dfba8f5dc758a8198868f58ca2cbc4867f5e5912..fcbed3497313fd840b81d36000d5e3eef7d3dd6a 100644 (file)
@@ -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
index 003fb958430cf9597bc46909e06867c33db6018a..b9f165edb2d3c83ef3506357631d3228d0b49726 100644 (file)
@@ -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 =
index fe3cf09f14c5e02e047ddb18e839c3f76a3dbf43..c0a7ec61180450d9e1633f4001bac144d7fbdc38 100644 (file)
@@ -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 *)
index 9b716637a9ed8c0c1c4ba2736034595365b461b3..b232d9894c444fb1ea2b431ff3811908e033930f 100644 (file)
@@ -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");
index 5b1bbce3daf9850c4c1a41ff284dab396d3a5b93..f4f9e34f665be5d106c4b2f68031fa18f23223fe 100644 (file)
@@ -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,
index e89e2e51d17e6734d31cefe93dc9d1cf5f2a297c..109dbaf99790e71ee2682ead2547e218aa62aa28 100644 (file)
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-exception Error of string
+exception Error of string Lazy.t
 
 module type Engine =
 sig
index b807728273f82e730102acfb292718dd41a24f6c..c9feaaee68da093fd97a49df693886a463fc5931 100644 (file)
@@ -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
index 0aa33c2db5dd2082e5557b9212cb30cc2c51c380..bb269411ede2ec4749dba9a456d8dbc020a7fc56 100644 (file)
@@ -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
 
index c56d3de2d75af9c4566d19a98ff568104c4d4699..5a091b7ad895cb196243c9d96c0394e8330fe1f3 100644 (file)
@@ -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)
 ;;
index f586455a24d41a606204f445409cdfda6fac2c4c..13dd9f410af6c74b2019842158a4a1b1a96a25c0 100644 (file)
@@ -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])
 ;;
 
index bd2ac9fdeb7d85861cb6f130879ba61ced2d9bd5..16510a7cd9e456d5b25eaa9becf71e4d1f48613d 100644 (file)
@@ -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 *******************************************************)
 
index f6283cf680644e6bb9db6413d1d3bf746a7fe816..6bf8ab6c1e37d339c37ac5afaef982fe148c3ea1 100644 (file)
@@ -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)
index e4cd7389813df6c35cdea841187be0c57a255208..8f05ae436bc450d4697cf4afc69e652b1db8c2dd 100644 (file)
@@ -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
index 74a9f63f2548290bb22e136e58cf9ae2f9ee06f2..d26221d3951bac5c6e82bf3437ffbaf3fba6477c 100644 (file)
@@ -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)
 
index 51405f5fdfa7269f58c3b780b16484eb7b67e85d..9f7fb42f4945a547d839878f158a3b8d3e8f8ca8 100644 (file)
@@ -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
index a7603d3a528bd54d978768892725aa1178ad279b..e28e1425d8fd69270ba896bcf1c703a1cc2f0b58 100644 (file)
@@ -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.                       *)
index f8782b7aec13db70083d025a44258d1416d0cf21..fc3bfd3b8a66991101daa4dd029d07b039565171 100644 (file)
@@ -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
index 99c37f8017832625f838c4128fb47cfd046e0bc3..2c641fd84f9ee3e48d625951bc970d35a61ed4e2 100644 (file)
@@ -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))))
index ed4a491e1d98d2ed14c55e1a585365e56c0d2f18..58dafd1a674441e25a8a933dc82a031fef1a5fea 100644 (file)
@@ -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 
index f45d681c198b216cf65564f95368b81597d70c48..40a9e6c80067ffd81d34cdb4c8a771d89eacd8f8 100644 (file)
@@ -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
   
index 8f6369d512f601ead6358e03fb9d9773a0eafcb8..1d7cc10e6bfad0a0a16fe9b7ad2b74bc0dc6d078 100644 (file)
@@ -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
 
index 94b5d379d19837cbaa96dd2f722771d13eeb48fc..3d5626afa4a0a6017346e08537706d3e998adcfe 100644 (file)
@@ -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)
index 51f28b3c9e7b6a29c634128afc87a7a37014d147..927552f0a60219c558dc35a38368541f90586ed7 100644 (file)
@@ -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