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
(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 =
(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 = []) () =
module Trivial =
struct
- exception Ambiguous_term of string
+ exception Ambiguous_term of string Lazy.t
exception Exit
module Callbacks =
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
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
open DisambiguateTypes
exception Invalid_choice
-exception Choice_not_found of string
+exception Choice_not_found of string Lazy.t
let num_choices = ref []
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,
(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)))
(** {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
open Printf
-exception Elim_failure of string
+exception Elim_failure of string Lazy.t
exception Can_t_eliminate
let debug_print = fun _ -> ()
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))
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
;;
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;;
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
(* *)
(****************************************************************************)
-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,
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 =
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 _ -> () ;;
(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 =
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
| 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' =
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,_,_) ->
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;
(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
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
(*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
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|} *)
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
(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
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
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 *)
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
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
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
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
| 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
(* 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
(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
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 =
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)
(*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
(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
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 ->
(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
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 *)
| 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 _
(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 &&
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? *)
(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 &&
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? *)
| 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)
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 []
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
| 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
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
| _ ->
(*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 *)
(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
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 *)
(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)))
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 *)
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 -
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) ->
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
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 ;
(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
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 =
| 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
(* 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 =
| _ ->
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 =
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
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
([],[],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
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:
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,_ =
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
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
(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
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
(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
~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
| (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 *)
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 =
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
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
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,_,_) ->
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,_,_) ->
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
)
*)
(* 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
-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 _ -> ()
(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
@ 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);
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' =
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 *)
(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
* 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 *)
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 _ -> ()
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)
;;
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 =
| 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
| _ ->
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
| _ ->
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
| _ ->
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 *)
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 =
(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 =
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
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
| 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... *)
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))))
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
| _ ->
raise
(RefineFailure
- (Reason ("Unkown mutual inductive definition " ^
+ (lazy ("Unkown mutual inductive definition " ^
U.string_of_uri uri)))
in
let rec count_prod t =
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
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) ->
(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))))
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))))
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 " ^
| _,_ ->
raise
(RefineFailure
- (Reason
+ (lazy
(sprintf
("Two sorts were expected, found %s " ^^
"(that reduces to %s) and %s (that reduces to %s)")
| 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
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 =
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
(* 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
* 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], *)
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."
(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
| 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
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
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 =
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
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."
(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."
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!!!!
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 =
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)
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)
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)
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
) (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)
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)
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) ->
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
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)
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 *)
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
* 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]. *)
*)
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 []
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
(** 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
| 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 ()
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 =
| 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
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
)
| _, 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 =
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 *)
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);;
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");
open Printf
-exception Error of string
-
-let fail msg = raise (Error msg)
+exception Error of string Lazy.t
module type Engine =
sig
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
| 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
| 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 =
| 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) ->
(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,
* http://helm.cs.unibo.it/
*)
-exception Error of string
+exception Error of string Lazy.t
module type Engine =
sig
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)))
(* 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)
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
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
)
])
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)
;;
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
~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
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
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) ->
(*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
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
~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
;;
[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)
;;
let tcl_fail a (proof,goal) =
match a with
- 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+ 1 -> raise (ProofEngineTypes.Fail (lazy "fail-tactical"))
| _ -> (proof,[goal])
;;
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 *******************************************************)
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)
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)
;;
~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
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
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 =
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)
(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)
* 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 []
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
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)
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].
| 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
* 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. *)
| _,_ ->
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 ->
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
_ ->
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
_ ->
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
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
) 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
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))))
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
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
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
(**
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
try
ring_tac status
with GoalUnringable ->
- raise (Fail "goal unringable")
+ raise (Fail (lazy "goal unringable"))
let ring_tac = ProofEngineTypes.mk_tactic ring_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
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)
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
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)
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
projects / helm.git / commitdiff