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) [1]" ^
+ 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) [2]"^
+ 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) [3]"^
+ 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 *)
need_dummy ind arity1 arity2 ugraph =
let module C = Cic in
let module U = UriManager in
- match (CicReduction.whd ~subst context arity1, CicReduction.whd ~subst context arity2) with
+ let arity1 = CicReduction.whd ~subst context arity1 in
+ let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
+ match arity1, CicReduction.whd ~subst context arity2 with
(C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
let b,ugraph1 =
CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
ugraph1
else
false,ugraph1
+ | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy ->
+ let b,ugraph1 =
+ CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
+ if not b then
+ false,ugraph1
+ else
+ check_allowed_sort_elimination_aux ugraph1
+ ((Some (name,C.Decl so))::context) ta true
| (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
| (C.Sort C.Prop, C.Sort C.Set)
| (C.Sort C.Prop, C.Sort C.CProp)
| (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
- (* TASSI: da verificare *)
-(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,_,_,cl) = List.nth itl i in
- (* is a singleton definition or the empty proposition? *)
- (List.length cl = 1 || List.length cl = 0) , ugraph
+ C.InductiveDefinition (itl,_,paramsno,_) ->
+ let itl_len = List.length itl in
+ let (name,_,ty,cl) = List.nth itl i in
+ let cl_len = List.length cl in
+ if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
+ let non_informative,ugraph =
+ if cl_len = 0 then true,ugraph
+ else
+ is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
+ paramsno (snd (List.nth cl 0)) ugraph
+ in
+ (* is it a singleton or empty non recursive and non informative
+ definition? *)
+ non_informative, ugraph
+ else
+ false,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
| (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
| (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
| ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
- (* TASSI: da verificare *)
when need_dummy ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
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 *)
- | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
- let b,ugraph1 =
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop -> true,ugraph1
- | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,_,_,cl) = List.nth itl i in
- (* is a singleton definition or the empty proposition? *)
- (List.length cl = 1 || List.length cl = 0),ugraph1
- | _ ->
- raise (TypeCheckerFailure
- ("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)))
- when not need_dummy ->
- let b,ugraph1 =
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop
- | C.Sort C.Set -> true,ugraph1
- | C.Sort C.CProp -> true,ugraph1
- | C.Sort (C.Type _) ->
- (* TASSI: da verificare *)
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,paramsno,_) ->
- let (_,_,_,cl) = List.nth itl i in
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
- in
- (List.fold_right
- (fun (_,x) (i,ugraph) ->
- if i then
- is_small ~logger tys paramsno x ugraph
- else
- false,ugraph
- ) cl (true,ugraph1))
- | _ ->
- raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri))
- )
- | _ -> raise (AssertFailure "19")
- )
- | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
- (* TASSI: da verificare *)
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph
| (_,_) -> false,ugraph
+ in
+ check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
and type_of_branch ~subst context argsno need_dummy outtype term constype =
let module C = Cic in
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
(* is a small constructor? *)
(*CSC: ottimizzare calcolando staticamente *)
-and is_small ~logger context paramsno c ugraph =
- let rec is_small_aux ~logger context c ugraph =
+and is_small_or_non_informative ~condition ~logger context paramsno c ugraph =
+ let rec is_small_or_non_informative_aux ~logger context c ugraph =
let module C = Cic in
match CicReduction.whd context c with
C.Prod (n,so,de) ->
let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
- let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
+ let b = condition s in
if b then
- is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
+ is_small_or_non_informative_aux
+ ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
else
false,ugraph1
| _ -> true,ugraph (*CSC: we trust the type-checker *)
in
let (context',dx) = split_prods ~subst:[] context paramsno c in
- is_small_aux ~logger context' dx ugraph
+ is_small_or_non_informative_aux ~logger context' dx ugraph
+
+and is_small ~logger =
+ is_small_or_non_informative
+ ~condition:(fun s -> s=Cic.Sort Cic.Prop || s=Cic.Sort Cic.Set)
+ ~logger
+
+and is_non_informative ~logger =
+ is_small_or_non_informative
+ ~condition:(fun s -> s=Cic.Sort Cic.Prop)
+ ~logger
and type_of ~logger t ugraph =
(*CSC
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
)
let logger = new CicLogger.logger in
typecheck_obj ~logger uri obj
+(* check_allowed_sort_elimination uri i s1 s2
+ This function is used outside the kernel to determine in advance whether
+ a MutCase will be allowed or not.
+ [uri,i] is the type of the term to match
+ [s1] is the sort of the term to eliminate (i.e. the head of the arity
+ of the inductive type [uri,i])
+ [s2] is the sort of the goal (i.e. the head of the type of the outtype
+ of the MutCase) *)
+let check_allowed_sort_elimination uri i s1 s2 =
+ fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
+ ~logger:(new CicLogger.logger) [] uri i true
+ (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
+ CicUniv.empty_ugraph)
projects / helm.git / blobdiff