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;
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph_dust
in
match cobj,ugraph with
(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
| CicEnvironment.CheckedObj _
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*debug_print s;*)
+ (*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 context n nn te =
+and does_not_occur ?(subst=[]) context n nn te =
let module C = Cic in
(*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
(*CSC: venga mangiata durante la whd sembra presentare problemi di *)
(*CSC: universi *)
- match CicReduction.whd context te with
+ match CicReduction.whd ~subst context te with
C.Rel m when m > n && m <= nn -> false
| C.Rel _
- | C.Meta _ (* CSC: Are we sure? No recursion?*)
| C.Sort _
| C.Implicit _ -> true
+ | C.Meta (_,l) ->
+ List.fold_right
+ (fun x i ->
+ match x with
+ None -> i
+ | Some x -> i && does_not_occur ~subst context n nn x) l true
| C.Cast (te,ty) ->
- does_not_occur context n nn te && does_not_occur context n nn ty
+ does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
| C.Prod (name,so,dest) ->
- does_not_occur context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
- dest
+ does_not_occur ~subst context n nn so &&
+ does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
+ (nn + 1) dest
| C.Lambda (name,so,dest) ->
- does_not_occur context n nn so &&
- does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+ does_not_occur ~subst context n nn so &&
+ does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
dest
| C.LetIn (name,so,dest) ->
- does_not_occur context n nn so &&
- does_not_occur ((Some (name,(C.Def (so,None))))::context)
+ does_not_occur ~subst context n nn so &&
+ does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context)
(n + 1) (nn + 1) dest
| C.Appl l ->
- List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
+ List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
| C.Var (_,exp_named_subst)
| C.Const (_,exp_named_subst)
| C.MutInd (_,_,exp_named_subst)
| C.MutConstruct (_,_,_,exp_named_subst) ->
- List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
+ List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
exp_named_subst true
| C.MutCase (_,_,out,te,pl) ->
- does_not_occur context n nn out && does_not_occur context n nn te &&
- List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
+ does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
+ List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
| C.Fix (_,fl) ->
let len = List.length fl in
let n_plus_len = n + len in
in
List.fold_right
(fun (_,_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- does_not_occur (tys @ context) n_plus_len nn_plus_len bo
+ i && does_not_occur ~subst context n nn ty &&
+ does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
) fl true
| C.CoFix (_,fl) ->
let len = List.length fl in
in
List.fold_right
(fun (_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- does_not_occur (tys @ context) n_plus_len nn_plus_len bo
+ i && does_not_occur ~subst context n nn ty &&
+ does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
) fl true
(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
let dummy_mutind =
C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
in
- (*CSC mettere in cicSubstitution *)
+ (*CSC: mettere in cicSubstitution *)
let rec subst_inductive_type_with_dummy_mutind =
function
C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
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
) cl' true
| t -> does_not_occur context n nn t
-(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
+(* the inductive type indexes are s.t. n < x <= nn *)
and are_all_occurrences_positive context uri indparamsno i n nn te =
let module C = Cic in
match CicReduction.whd context te with
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
)
with
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph1_dust
in
match cobj with
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
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph1_dust
in
match cobj with
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 =
+and get_new_safes ~subst context p c rl safes n nn x =
let module C = Cic in
let module U = UriManager in
let module R = CicReduction 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 =
+and split_prods ~subst context n te =
let module C = Cic in
let module R = CicReduction in
- match (n, R.whd context te) with
+ match (n, R.whd ~subst context te) with
(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 =
+and eat_lambdas ~subst context n te =
let module C = Cic in
let module R = CicReduction in
match (n, R.whd ~subst context te) with
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 =
+and check_is_really_smaller_arg ~subst context n nn kl x safes te =
(*CSC: forse la whd si puo' fare solo quando serve veramente. *)
(*CSC: cfr guarded_by_destructors *)
let module C = Cic in
let module U = UriManager in
- match CicReduction.whd context te with
+ match CicReduction.whd ~subst context te with
C.Rel m when List.mem m safes -> true
| C.Rel _ -> false
| C.Var _
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
i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure (lazy "not enough patterns"))
+ in
List.fold_right
(fun (p,(_,c)) i ->
let rl' =
in
i &&
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(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
i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure (lazy "not enough patterns"))
+ in
(*CSC: supponiamo come prima che nessun controllo sia necessario*)
(*CSC: sugli argomenti di una applicazione *)
List.fold_right
recursive_args tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
- get_new_safes context p c rl' safes n nn x
+ get_new_safes ~subst context p c rl' safes n nn x
in
i &&
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| _ ->
List.fold_right
(fun p i ->
x_plus_len safes' bo
) fl true
-and guarded_by_destructors ?(subst = []) context n nn kl x safes =
+and guarded_by_destructors ~subst context n nn kl x safes =
let module C = Cic in
let module U = UriManager in
function
(match List.nth context (n-1) with
Some (_,C.Decl _) -> true
| Some (_,C.Def (bo,_)) ->
- guarded_by_destructors context m nn kl x safes
+ 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 _
| C.Implicit _ -> true
| C.Cast (te,ty) ->
- guarded_by_destructors context n nn kl x safes te &&
- guarded_by_destructors context n nn kl x safes ty
+ guarded_by_destructors ~subst context n nn kl x safes te &&
+ guarded_by_destructors ~subst context n nn kl x safes ty
| C.Prod (name,so,ta) ->
- guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Decl so)))::context)
+ guarded_by_destructors ~subst context n nn kl x safes so &&
+ guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Lambda (name,so,ta) ->
- guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Decl so)))::context)
+ guarded_by_destructors ~subst context n nn kl x safes so &&
+ guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.LetIn (name,so,ta) ->
- guarded_by_destructors context n nn kl x safes so &&
- guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
+ guarded_by_destructors ~subst context n nn kl x safes so &&
+ guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context)
(n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
let k = List.nth kl (m - n - 1) in
else
List.fold_right
(fun param i ->
- i && guarded_by_destructors context n nn kl x safes param
+ i && guarded_by_destructors ~subst context n nn kl x safes param
) tl true &&
check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
| C.Appl tl ->
List.fold_right
- (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
+ (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
tl true
| C.Var (_,exp_named_subst)
| C.Const (_,exp_named_subst)
| C.MutInd (_,_,exp_named_subst)
| C.MutConstruct (_,_,_,exp_named_subst) ->
List.fold_right
- (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
+ (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
exp_named_subst true
| C.MutCase (uri,i,outtype,term,pl) ->
- (match CicReduction.whd context term with
+ (match CicReduction.whd ~subst context term with
C.Rel m when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(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 context n nn kl x safes outtype &&
- guarded_by_destructors context n nn kl x safes term &&
+ guarded_by_destructors ~subst context n nn kl x safes outtype &&
+ guarded_by_destructors ~subst context n nn kl x safes term &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
(fun p i ->
- i && guarded_by_destructors context n nn kl x safes p)
+ i && guarded_by_destructors ~subst context n nn kl x safes p)
pl true
else
- guarded_by_destructors context n nn kl x safes outtype &&
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ 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? *)
List.fold_right
(fun (p,(_,c,brujinedc)) i ->
let rl' = recursive_args tys 0 len brujinedc in
let (e,safes',n',nn',x',context') =
- get_new_safes context p c rl' safes n nn x
+ get_new_safes ~subst context p c rl' safes n nn x
in
i &&
- guarded_by_destructors context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ guarded_by_destructors ~subst context' n' nn' kl x' safes' e
+ ) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
(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 context n nn kl x safes outtype &&
- guarded_by_destructors context n nn kl x safes term &&
+ guarded_by_destructors ~subst context n nn kl x safes outtype &&
+ guarded_by_destructors ~subst context n nn kl x safes term &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
(fun p i ->
- i && guarded_by_destructors context n nn kl x safes p)
+ i && guarded_by_destructors ~subst context n nn kl x safes p)
pl true
else
- guarded_by_destructors context n nn kl x safes outtype &&
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ 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? *)
List.fold_right
(fun t i ->
- i && guarded_by_destructors context n nn kl x safes t)
+ i && guarded_by_destructors ~subst context n nn kl x safes t)
tl true &&
List.fold_right
(fun (p,(_,c)) i ->
recursive_args tys 0 len debrujinedte
in
let (e, safes',n',nn',x',context') =
- get_new_safes context p c rl' safes n nn x
+ get_new_safes ~subst context p c rl' safes n nn x
in
i &&
- guarded_by_destructors context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ guarded_by_destructors ~subst context' n' nn' kl x' safes' e
+ ) pl_and_cl true
| _ ->
- guarded_by_destructors context n nn kl x safes outtype &&
- guarded_by_destructors context n nn kl x safes term &&
+ guarded_by_destructors ~subst context n nn kl x safes outtype &&
+ guarded_by_destructors ~subst context n nn kl x safes term &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
- (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
+ (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
pl true
)
| C.Fix (_, fl) ->
and safes' = List.map (fun x -> x + len) safes in
List.fold_right
(fun (_,_,ty,bo) i ->
- i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
- guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
+ i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
+ guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
x_plus_len safes' bo
) fl true
| C.CoFix (_, fl) ->
List.fold_right
(fun (_,ty,bo) i ->
i &&
- guarded_by_destructors context n nn kl x_plus_len safes' ty &&
- guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
+ guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
+ guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
x_plus_len safes' bo
) fl true
(* the boolean h means already protected *)
(* args is the list of arguments the type of the constructor that may be *)
(* found in head position must be applied to. *)
-(*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
-and guarded_by_constructors context n nn h te args coInductiveTypeURI =
+and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
let module C = Cic in
(*CSC: There is a lot of code replication between the cases X and *)
(*CSC: (C.Appl X tl). Maybe it will be better to define a function *)
(*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
- match CicReduction.whd context te with
+ match CicReduction.whd ~subst context te with
C.Rel m when m > n && m <= nn -> h
| C.Rel _ -> true
| C.Meta _
| 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 context n nn so &&
- guarded_by_constructors ((Some (name,(C.Decl so)))::context)
+ does_not_occur ~subst context n nn so &&
+ guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
(n + 1) (nn + 1) h de args coInductiveTypeURI
| C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
h &&
- List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
+ List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
| C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
let consty =
let obj,_ =
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 context ty with
- C.Meta _ -> raise (AssertFailure "34")
+ match CicReduction.whd ~subst context ty with
+ C.Meta _ -> raise (AssertFailure (lazy "34"))
| C.Rel _
| C.Var _
| C.Sort _ ->
- does_not_occur context n nn te
+ 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 context n nn true te [] coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn true te []
+ coInductiveTypeURI
| C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
- guarded_by_constructors context n nn true te tl coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn true te tl
+ coInductiveTypeURI
| C.Appl _ ->
- does_not_occur context n nn te
- | C.Const _ -> raise (AssertFailure "26")
+ does_not_occur ~subst context n nn te
+ | C.Const _ -> raise (AssertFailure (lazy "26"))
| C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
- guarded_by_constructors context n nn true te [] coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn true te []
+ coInductiveTypeURI
| C.MutInd _ ->
- does_not_occur context n nn te
- | C.MutConstruct _ -> raise (AssertFailure "27")
+ does_not_occur ~subst context n nn te
+ | 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 context ty with
+ match CicReduction.whd ~subst context ty with
C.Rel _
| C.Var _
| 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 context n nn x) true l
- | C.Const _ -> raise (AssertFailure "31")
+ (fun i x -> i && does_not_occur ~subst context n nn x) true l
+ | C.Const _ -> raise (AssertFailure (lazy "31"))
| C.MutInd _ ->
List.fold_left
- (fun i x -> i && does_not_occur context n nn x) true l
- | C.MutConstruct _ -> raise (AssertFailure "32")
+ (fun i x -> i && does_not_occur ~subst context n nn x) true l
+ | 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
[] -> true
| tlhe::tltl as l ->
- let consty' = CicReduction.whd context consty in
+ let consty' = CicReduction.whd ~subst context consty in
match args with
he::tl ->
begin
C.Prod (_,_,de) ->
let instantiated_de = CicSubstitution.subst he de in
(*CSC: siamo sicuri che non sia troppo forte? *)
- does_not_occur context n nn tlhe &
+ does_not_occur ~subst context n nn tlhe &
instantiate_type tl instantiated_de tltl
| _ ->
(*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 *)
in
instantiate_type args consty tl
| C.Appl ((C.CoFix (_,fl))::tl) ->
- List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
+ List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
let len = List.length fl in
let n_plus_len = n + len
and nn_plus_len = nn + len
and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
- args coInductiveTypeURI
+ i && does_not_occur ~subst context n nn ty &&
+ guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
+ h bo args coInductiveTypeURI
) fl true
| C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
- List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
- does_not_occur context n nn out &&
- does_not_occur context n nn te &&
+ List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
+ does_not_occur ~subst context n nn out &&
+ does_not_occur ~subst context n nn te &&
List.fold_right
(fun x i ->
i &&
- guarded_by_constructors context n nn h x args coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn h x args
+ coInductiveTypeURI
) pl true
| C.Appl l ->
- List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
+ List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
| C.Var (_,exp_named_subst)
| C.Const (_,exp_named_subst) ->
List.fold_right
- (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
+ (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
| C.MutInd _ -> assert false
| C.MutConstruct (_,_,_,exp_named_subst) ->
List.fold_right
- (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
+ (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
| C.MutCase (_,_,out,te,pl) ->
- does_not_occur context n nn out &&
- does_not_occur context n nn te &&
+ does_not_occur ~subst context n nn out &&
+ does_not_occur ~subst context n nn te &&
List.fold_right
(fun x i ->
i &&
- guarded_by_constructors context n nn h x args coInductiveTypeURI
+ guarded_by_constructors ~subst context n nn h x args
+ coInductiveTypeURI
) pl true
| C.Fix (_,fl) ->
let len = List.length fl in
and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- does_not_occur (tys@context) n_plus_len nn_plus_len bo
+ i && does_not_occur ~subst context n nn ty &&
+ does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
) fl true
| C.CoFix (_,fl) ->
let len = List.length fl in
and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
List.fold_right
(fun (_,ty,bo) i ->
- i && does_not_occur context n nn ty &&
- guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
+ i && does_not_occur ~subst context n nn ty &&
+ guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
+ h bo
args coInductiveTypeURI
) fl true
-and check_allowed_sort_elimination ~logger context uri i need_dummy ind
- arity1 arity2 ugraph =
+and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+ need_dummy ind arity1 arity2 ugraph =
let module C = Cic in
let module U = UriManager in
- match (CicReduction.whd context arity1, CicReduction.whd 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 context so1 so2 ugraph in
+ let b,ugraph1 =
+ CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
if b then
- check_allowed_sort_elimination ~logger context uri i need_dummy
- (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
+ check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+ need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
+ 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 context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ((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 context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ((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 context so ind ugraph
| (_,_) -> false,ugraph
+ in
+ check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
-and type_of_branch context argsno need_dummy outtype term constype =
+and type_of_branch ~subst context argsno need_dummy outtype term constype =
let module C = Cic in
let module R = CicReduction in
- match R.whd context constype with
+ match R.whd ~subst context constype with
C.MutInd (_,_,_) ->
if need_dummy then
outtype
C.Appl l -> C.Appl (l@[C.Rel 1])
| t -> C.Appl [t ; C.Rel 1]
in
- C.Prod (C.Anonymous,so,type_of_branch
+ 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 -
with the actual context *)
-and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
+and check_metasenv_consistency ~logger ~subst metasenv context
canonical_context l ugraph
=
let module C = Cic in
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
Some (_,C.Decl t) -> S.lift n t,ugraph
| Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
| Some (_,C.Def (bo,None)) ->
- debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
+ 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
(* The type of the LetIn is reduced. Much faster than the previous
solution. Moreover the inferred type is probably very different
from the expected one.
- (CicReduction.whd context
+ (CicReduction.whd ~subst context
(C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
*)
(* One-step LetIn reduction. Even faster than the previous solution.
(* 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 =
let ty,ugraph2 = type_of_aux context term ugraph1 in
- match R.whd context ty with
+ match R.whd ~subst context ty with
(*CSC manca il caso dei CAST *)
(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *)
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:
let type_of_sort_of_ind_ty,ugraph3 =
type_of_aux ~logger context sort_of_ind_type ugraph2 in
let b,ugraph4 =
- check_allowed_sort_elimination ~logger context uri i need_dummy
- sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
+ check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
+ need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
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
let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
(* 2 is skipped *)
let ty_branch =
- type_of_branch context parsno need_dummy outtype cons
+ type_of_branch ~subst context parsno need_dummy outtype cons
ty_cons in
let b1,ugraph4 =
R.are_convertible
~subst ~metasenv context ty_p ty_branch ugraph3
in
if not b1 then
- debug_print
+ debug_print (lazy
("#### " ^ CicPp.ppterm ty_p ^
- " <==> " ^ CicPp.ppterm ty_branch);
+ " <==> " ^ CicPp.ppterm ty_branch));
(j + 1,b1,ugraph4)
else
(j,false,ugraph)
in
if not branches_ok then
raise
- (TypeCheckerFailure "Case analysys: wrong branch type");
- let arguments =
+ (TypeCheckerFailure (lazy "Case analysys: wrong branch type"));
+ let arguments' =
if not need_dummy then outtype::arguments@[term]
else outtype::arguments in
let outtype =
- if arguments = [] then outtype
- else CicReduction.head_beta_reduce (C.Appl arguments)
+ if need_dummy && arguments = [] then outtype
+ else CicReduction.head_beta_reduce (C.Appl arguments')
in
outtype,ugraph5
| C.Fix (i,fl) ->
let's control the guarded by
destructors conditions D{f,k,x,M}
*)
- if not (guarded_by_destructors context' eaten
+ if not (guarded_by_destructors ~subst context' eaten
(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
if b then
begin
(* let's control that the returned type is coinductive *)
- match returns_a_coinductive context ty with
+ match returns_a_coinductive ~subst context ty with
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
conditions C{f,M}
*)
- if not (guarded_by_constructors (types @ context)
- 0 len false bo [] uri) then
+ if not (guarded_by_constructors ~subst
+ (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
ty,ugraph2
- and check_exp_named_subst ~logger ?(subst = []) context ugraph =
+ and check_exp_named_subst ~logger ~subst context ugraph =
let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
match l with
[] -> ugraph
~subst ~metasenv context typeoft typeofvar ugraph2) ;
fdebug := 0 ;
debug typeoft [typeofvar] ;
- raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
+ raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
end
in
check_exp_named_subst_aux ~logger [] ugraph
- and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
+ and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
let module C = Cic in
let t1' = CicReduction.whd ~subst context t1 in
let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
| (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 =
+ and eat_prods ~subst context hetype l ugraph =
(*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
(*CSC: cucinati *)
match l with
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 context ty =
+ and returns_a_coinductive ~subst context ty =
let module C = Cic in
- match CicReduction.whd context ty with
+ match CicReduction.whd ~subst context ty with
C.MutInd (uri,i,_) ->
(*CSC: definire una funzioncina per questo codice sempre replicato *)
let obj,_ =
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 ((Some (n,C.Decl so))::context) de
+ returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
| _ -> None
in
(*CSC
-debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
+debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ;
let res =
*)
type_of_aux ~logger context t ugraph
(*
-in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
+in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
*)
(* 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) ->
- (*CSC: [] is an empty metasenv. Is it correct? *)
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 context paramsno c in
- is_small_aux ~logger context' dx ugraph
+ let (context',dx) = split_prods ~subst:[] context paramsno c in
+ 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
-debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
+debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ;
let res =
*)
type_of_aux' ~logger [] [] t ugraph
(*CSC
-in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
+in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
*)
;;
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
)
(* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') ->
- (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+ (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
cobj,ugraph'
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
logger#log (`Start_type_checking uri) ;
- (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
+ (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
try
CicEnvironment.set_type_checking_info uri;
object.
*)
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph
;;
let typecheck_obj ~logger uri obj =
let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
- CicEnvironment.add_type_checked_obj uri (obj,ugraph)
+ let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
+ CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
(** wrappers which instantiate fresh loggers *)
let typecheck_obj uri obj =
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