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
| 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))
)
with
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph1_dust
in
match cobj with
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*debug_print s;*)
+ (*debug_print (lazy s);*)
uobj,ugraph1_dust
in
match cobj with
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 "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
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 "not enough patterns")
+ in
(*CSC: supponiamo come prima che nessun controllo sia necessario*)
(*CSC: sugli argomenti di una applicazione *)
List.fold_right
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 ->
i && guarded_by_destructors context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
in
i &&
guarded_by_destructors 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
i && guarded_by_destructors context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
in
i &&
guarded_by_destructors context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| _ ->
guarded_by_destructors context n nn kl x safes outtype &&
guarded_by_destructors context n nn kl x safes term &&
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) ->
- (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? *)
- List.length cl = 1,ugraph1
- | _ ->
- raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri))
- )
- | _ -> false,ugraph1
- )
+ 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 ->
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")
~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)
if not branches_ok then
raise
(TypeCheckerFailure "Case analysys: wrong branch type");
- let arguments =
+ 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) ->
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? *)
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
*)
;;
(* ??? 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 = 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
+
projects / helm.git / blobdiff