exception CicEnvironmentError;;
-let rec type_of_constant uri =
+let rec type_of_constant ~logger uri =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
- CicLogger.log (`Start_type_checking uri) ;
+ logger#log (`Start_type_checking uri) ;
CicUniv.directly_to_env_begin ();
(* let's typecheck the uncooked obj *)
(match uobj with
C.Constant (_,Some te,ty,_) ->
- let _ = type_of ty in
- let type_of_te = type_of te in
+ let _ = type_of ~logger ty in
+ let type_of_te = type_of ~logger te in
if not (R.are_convertible [] type_of_te ty) then
raise (TypeCheckerFailure (sprintf
"the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
let _ =
List.fold_left
(fun metasenv ((_,context,ty) as conj) ->
- ignore (type_of_aux' metasenv context ty) ;
+ ignore (type_of_aux' ~logger metasenv context ty) ;
metasenv @ [conj]
) [] conjs
in
- let _ = type_of_aux' conjs [] ty in
- let type_of_te = type_of_aux' conjs [] te in
+ let _ = type_of_aux' ~logger conjs [] ty in
+ let type_of_te = type_of_aux' ~logger conjs [] te in
if not (R.are_convertible [] type_of_te ty) then
raise (TypeCheckerFailure (sprintf
"the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
);
CicEnvironment.set_type_checking_info uri ;
CicUniv.directly_to_env_end ();
- CicLogger.log (`Type_checking_completed uri) ;
+ logger#log (`Type_checking_completed uri) ;
match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
| _ ->
raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
-and type_of_variable uri =
+and type_of_variable ~logger uri =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
| CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
- CicLogger.log (`Start_type_checking uri) ;
+ logger#log (`Start_type_checking uri) ;
CicUniv.directly_to_env_begin ();
(* only to check that ty is well-typed *)
let _ = type_of ty in
(match bo with
None -> ()
| Some bo ->
- if not (R.are_convertible [] (type_of bo) ty) then
+ if not (R.are_convertible [] (type_of ~logger bo) ty) then
raise (TypeCheckerFailure
("Unknown variable:" ^ U.string_of_uri uri))
) ;
CicEnvironment.set_type_checking_info uri ;
CicUniv.directly_to_env_end ();
- CicLogger.log (`Type_checking_completed uri) ;
+ logger#log (`Type_checking_completed uri) ;
ty
| _ ->
raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
(* Main function to checks the correctness of a mutual *)
(* inductive block definition. This is the function *)
(* exported to the proof-engine. *)
-and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
+and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) =
let module U = UriManager in
(* let's check if the arity of the inductive types are well *)
(* formed *)
- List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
+ List.iter (fun (_,_,x,_) -> let _ = type_of ~logger x in ()) itl ;
(* let's check if the types of the inductive constructors *)
(* are well formed. *)
raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
UriManager.string_of_uri uri))
-and type_of_mutual_inductive_defs uri i =
+and type_of_mutual_inductive_defs ~logger uri i =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
- CicLogger.log (`Start_type_checking uri) ;
+ logger#log (`Start_type_checking uri) ;
CicUniv.directly_to_env_begin ();
- check_mutual_inductive_defs uri uobj ;
+ check_mutual_inductive_defs ~logger uri uobj ;
CicEnvironment.set_type_checking_info uri ;
CicUniv.directly_to_env_end ();
- CicLogger.log (`Type_checking_completed uri) ;
+ logger#log (`Type_checking_completed uri) ;
(match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
U.string_of_uri uri))
-and type_of_mutual_inductive_constr uri i j =
+and type_of_mutual_inductive_constr ~logger uri i j =
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
- CicLogger.log (`Start_type_checking uri) ;
+ logger#log (`Start_type_checking uri) ;
(*CicUniv.directly_to_env_begin ();*)
- check_mutual_inductive_defs uri uobj ;
+ check_mutual_inductive_defs ~logger uri uobj ;
CicEnvironment.set_type_checking_info uri ;
(*CicUniv.directly_to_env_end ();*)
- CicLogger.log (`Type_checking_completed uri) ;
+ logger#log (`Type_checking_completed uri) ;
(match CicEnvironment.is_type_checked ~trust:false uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
args coInductiveTypeURI
) fl true
-and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
+and check_allowed_sort_elimination ~logger context uri i need_dummy ind arity1 arity2 =
let module C = Cic in
let module U = UriManager in
match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
(C.Prod (_,so1,de1), C.Prod (_,so2,de2))
when CicReduction.are_convertible context so1 so2 ->
- check_allowed_sort_elimination context uri i need_dummy
+ check_allowed_sort_elimination ~logger context uri i need_dummy
(C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
| (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
| (C.Sort C.Prop, C.Sort C.Set)
in
let (_,_,_,cl) = List.nth itl i in
List.fold_right
- (fun (_,x) i -> i && is_small tys paramsno x) cl true
+ (fun (_,x) i -> i && is_small ~logger tys paramsno x) cl true
| _ ->
raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
UriManager.string_of_uri uri))
(fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
in
List.fold_right
- (fun (_,x) i -> i && is_small tys paramsno x) cl true
+ (fun (_,x) i -> i && is_small ~logger tys paramsno x) cl true
| _ ->
raise (TypeCheckerFailure
("Unknown mutual inductive definition:" ^
metavariable is consitent - up to relocation via the relocation list l -
with the actual context *)
-and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l =
+and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
+ canonical_context l
+=
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
"Not well typed metavariable local context: expected a term convertible with %s, found %s"
(CicPp.ppterm ct) (CicPp.ppterm t)))
| Some t,Some (_,C.Decl ct) ->
- let type_t = type_of_aux' ~subst metasenv context t in
+ let type_t = type_of_aux' ~logger ~subst metasenv context t in
if not (R.are_convertible ~subst ~metasenv context type_t ct) then
(* debug *)
raise (TypeCheckerFailure (sprintf
) l lifted_canonical_context
(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-and type_of_aux' ?(subst = []) metasenv context t =
- let rec type_of_aux context =
+and type_of_aux' ~logger ?(subst = []) metasenv context t =
+ let rec type_of_aux ~logger context =
let module C = Cic in
let module R = CicReduction in
let module S = CicSubstitution in
| Some (_,C.Def (_,Some ty)) -> S.lift n ty
| Some (_,C.Def (bo,None)) ->
debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
- type_of_aux context (S.lift n bo)
+ type_of_aux ~logger context (S.lift n bo)
| None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
with
_ ->
)
| C.Var (uri,exp_named_subst) ->
incr fdebug ;
- check_exp_named_subst ~subst context exp_named_subst ;
+ check_exp_named_subst ~logger ~subst context exp_named_subst ;
let ty =
- CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
+ CicSubstitution.subst_vars exp_named_subst (type_of_variable ~logger uri)
in
decr fdebug ;
ty
| C.Meta (n,l) ->
(try
let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
- check_metasenv_consistency
+ check_metasenv_consistency ~logger
~subst metasenv context canonical_context l;
(* assuming subst is well typed !!!!! *)
CicSubstitution.lift_meta l ty
(* type_of_aux context (CicSubstitution.lift_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
- check_metasenv_consistency
+ check_metasenv_consistency ~logger
~subst metasenv context canonical_context l;
CicSubstitution.lift_meta l ty)
(* TASSI: CONSTRAINTS *)
| C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
| C.Implicit _ -> raise (AssertFailure "21")
| C.Cast (te,ty) as t ->
- let _ = type_of_aux context ty in
- if R.are_convertible ~subst ~metasenv context (type_of_aux context te) ty then
+ let _ = type_of_aux ~logger context ty in
+ if R.are_convertible ~subst ~metasenv context (type_of_aux ~logger context te) ty then
ty
else
raise (TypeCheckerFailure
(sprintf "Invalid cast %s" (CicPp.ppterm t)))
| C.Prod (name,s,t) ->
- let sort1 = type_of_aux context s
- and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
+ let sort1 = type_of_aux ~logger context s
+ and sort2 = type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t in
let res = sort_of_prod ~subst context (name,s) (sort1,sort2) in
res
| C.Lambda (n,s,t) ->
- let sort1 = type_of_aux context s in
+ let sort1 = type_of_aux ~logger context s in
(match R.whd ~subst context sort1 with
C.Meta _
| C.Sort _ -> ()
type; instead it is a term of type %s" (CicPp.ppterm s)
(CicPp.ppterm sort1)))
) ;
- let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
+ let type2 = type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t in
C.Prod (n,s,type2)
| C.LetIn (n,s,t) ->
(* only to check if s is well-typed *)
- let ty = type_of_aux context s in
+ let ty = type_of_aux ~logger context s in
(* The type of a LetIn is a LetIn. Extremely slow since the computed
LetIn is later reduced and maybe also re-checked.
(C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
(* One-step LetIn reduction. Even faster than the previous solution.
Moreover the inferred type is closer to the expected one. *)
(CicSubstitution.subst s
- (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
+ (type_of_aux ~logger ((Some (n,(C.Def (s,Some ty))))::context) t))
| C.Appl (he::tl) when List.length tl > 0 ->
- let hetype = type_of_aux context he in
- let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
+ let hetype = type_of_aux ~logger context he in
+ let tlbody_and_type = List.map (fun x -> (x, type_of_aux ~logger context x)) tl in
eat_prods ~subst context hetype tlbody_and_type
| C.Appl _ -> raise (AssertFailure "Appl: no arguments")
| C.Const (uri,exp_named_subst) ->
incr fdebug ;
- check_exp_named_subst ~subst context exp_named_subst ;
+ check_exp_named_subst ~logger ~subst context exp_named_subst ;
let cty =
- CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
+ CicSubstitution.subst_vars exp_named_subst (type_of_constant ~logger uri)
in
decr fdebug ;
cty
| C.MutInd (uri,i,exp_named_subst) ->
incr fdebug ;
- check_exp_named_subst ~subst context exp_named_subst ;
+ check_exp_named_subst ~logger ~subst context exp_named_subst ;
let cty =
CicSubstitution.subst_vars exp_named_subst
- (type_of_mutual_inductive_defs uri i)
+ (type_of_mutual_inductive_defs ~logger uri i)
in
decr fdebug ;
cty
| C.MutConstruct (uri,i,j,exp_named_subst) ->
- check_exp_named_subst ~subst context exp_named_subst ;
+ check_exp_named_subst ~logger ~subst context exp_named_subst ;
let cty =
CicSubstitution.subst_vars exp_named_subst
- (type_of_mutual_inductive_constr uri i j)
+ (type_of_mutual_inductive_constr ~logger uri i j)
in
cty
| C.MutCase (uri,i,outtype,term,pl) ->
- let outsort = type_of_aux context outtype in
+ let outsort = type_of_aux ~logger context outtype in
let (need_dummy, k) =
let rec guess_args context t =
let outtype = CicReduction.whd ~subst context t in
let (b, k) = guess_args context outsort in
if not b then (b, k - 1) else (b, k) in
let (parameters, arguments, exp_named_subst) =
- match R.whd ~subst context (type_of_aux context term) with
+ match R.whd ~subst context (type_of_aux ~logger context term) with
C.MutInd (uri',i',exp_named_subst) as typ ->
if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
else raise
else
C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in
if not
- (check_allowed_sort_elimination context uri i need_dummy
- sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
+ (check_allowed_sort_elimination ~logger context uri i need_dummy
+ sort_of_ind_type (type_of_aux ~logger context sort_of_ind_type) outsort)
then
raise
(TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
let res =
b &&
R.are_convertible
- ~subst ~metasenv context (type_of_aux context p)
+ ~subst ~metasenv context (type_of_aux ~logger context p)
(type_of_branch context parsno need_dummy outtype cons
- (type_of_aux context cons)) in
+ (type_of_aux ~logger context cons)) in
if not res then
- debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
+ debug_print ("#### " ^ CicPp.ppterm (type_of_aux ~logger context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux ~logger context cons))) ; res
)
) (1,true) pl
in
List.rev
(List.map
(fun (n,k,ty,_) ->
- let _ = type_of_aux context ty in
+ let _ = type_of_aux ~logger context ty in
(Some (C.Name n,(C.Decl ty)),k)) fl)
in
let (types,kl) = List.split types_times_kl in
(fun (name,x,ty,bo) ->
if
(R.are_convertible
- ~subst ~metasenv (types@context) (type_of_aux (types@context) bo)
+ ~subst ~metasenv (types@context) (type_of_aux ~logger (types@context) bo)
(CicSubstitution.lift len ty))
then
begin
List.rev
(List.map
(fun (n,ty,_) ->
- let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
+ let _ = type_of_aux ~logger context ty in Some (C.Name n,(C.Decl ty))) fl)
in
let len = List.length types in
List.iter
if
(R.are_convertible
~subst ~metasenv (types @ context)
- (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
+ (type_of_aux ~logger (types @ context) bo) (CicSubstitution.lift len ty))
then
begin
(* let's control that the returned type is coinductive *)
let (_,ty,_) = List.nth fl i in
ty
- and check_exp_named_subst ?(subst = []) context =
- let rec check_exp_named_subst_aux esubsts =
+ and check_exp_named_subst ~logger ?(subst = []) context =
+ let rec check_exp_named_subst_aux ~logger esubsts =
function
[] -> ()
| ((uri,t) as item)::tl ->
let typeofvar =
- CicSubstitution.subst_vars esubsts (type_of_variable uri) in
- let typeoft = type_of_aux context t in
+ CicSubstitution.subst_vars esubsts (type_of_variable ~logger uri) in
+ let typeoft = type_of_aux ~logger context t in
if CicReduction.are_convertible
~subst ~metasenv context typeoft typeofvar then
- check_exp_named_subst_aux (esubsts@[item]) tl
+ check_exp_named_subst_aux ~logger (esubsts@[item]) tl
else
begin
CicReduction.fdebug := 0 ;
raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
end
in
- check_exp_named_subst_aux []
+ check_exp_named_subst_aux ~logger []
and sort_of_prod ?(subst = []) context (name,s) (t1, t2) =
let module C = Cic in
debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
let res =
*)
- type_of_aux context t
+ type_of_aux ~logger context t
(*
in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
*)
(* is a small constructor? *)
(*CSC: ottimizzare calcolando staticamente *)
-and is_small context paramsno c =
- let rec is_small_aux context c =
+and is_small ~logger context paramsno c =
+ let rec is_small_aux ~logger context c =
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 = type_of_aux' [] context so in
+ let s = type_of_aux' ~logger [] context so in
(s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
- is_small_aux ((Some (n,(C.Decl so)))::context) de
+ is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de
| _ -> true (*CSC: we trust the type-checker *)
in
let (context',dx) = split_prods context paramsno c in
- is_small_aux context' dx
+ is_small_aux ~logger context' dx
-and type_of t =
+and type_of ~logger t =
(*CSC
debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
let res =
*)
- type_of_aux' [] [] t
+ type_of_aux' ~logger [] [] t
(*CSC
in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
*)
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
+ let logger = new CicLogger.logger in
(*match CicEnvironment.is_type_checked ~trust:false uri with*)
match CicEnvironment.is_type_checked ~trust:true uri with
CicEnvironment.CheckedObj cobj -> cobj
| CicEnvironment.UncheckedObj uobj ->
(* let's typecheck the uncooked object *)
- CicLogger.log (`Start_type_checking uri) ;
+ logger#log (`Start_type_checking uri) ;
CicUniv.directly_to_env_begin ();
(match uobj with
C.Constant (_,Some te,ty,_) ->
- let _ = type_of ty in
- if not (R.are_convertible [] (type_of te ) ty) then
+ let _ = type_of ~logger ty in
+ if not (R.are_convertible [] (type_of ~logger te ) ty) then
raise (TypeCheckerFailure
("Unknown constant:" ^ U.string_of_uri uri))
| C.Constant (_,None,ty,_) ->
(* only to check that ty is well-typed *)
- let _ = type_of ty in ()
+ let _ = type_of ~logger ty in ()
| C.CurrentProof (_,conjs,te,ty,_) ->
let _ =
List.fold_left
(fun metasenv ((_,context,ty) as conj) ->
- ignore (type_of_aux' metasenv context ty) ;
+ ignore (type_of_aux' ~logger metasenv context ty) ;
metasenv @ [conj]
) [] conjs
in
- let _ = type_of_aux' conjs [] ty in
- let type_of_te = type_of_aux' conjs [] te in
+ let _ = type_of_aux' ~logger conjs [] ty in
+ let type_of_te = type_of_aux' ~logger conjs [] te in
if not (R.are_convertible [] type_of_te ty)
then
raise (TypeCheckerFailure (sprintf
(CicPp.ppterm ty)))
| C.Variable (_,bo,ty,_) ->
(* only to check that ty is well-typed *)
- let _ = type_of ty in
+ let _ = type_of ~logger ty in
(match bo with
None -> ()
| Some bo ->
- if not (R.are_convertible [] (type_of bo) ty) then
+ if not (R.are_convertible [] (type_of ~logger bo) ty) then
raise (TypeCheckerFailure
("Unknown variable:" ^ U.string_of_uri uri))
)
| C.InductiveDefinition _ ->
- check_mutual_inductive_defs uri uobj
+ check_mutual_inductive_defs ~logger uri uobj
) ;
CicEnvironment.set_type_checking_info uri ;
CicUniv.directly_to_env_end ();
- CicLogger.log (`Type_checking_completed uri);
+ logger#log (`Type_checking_completed uri);
uobj
;;
+
+(** wrappers which instantiate fresh loggers *)
+
+let type_of_aux' ?(subst = []) metasenv context t =
+ let logger = new CicLogger.logger in
+ type_of_aux' ~logger metasenv context t
+
+let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
+ let logger = new CicLogger.logger in
+ typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno)
+
projects / helm.git / commitdiff