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
)
projects / helm.git / blobdiff