raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
;;
+(* XXX: bug *)
+let ugraph_convertibility ug1 ug2 ul2 = true;;
+
+let check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj =
+ match unchecked_ugraph with
+ | Some (ug,ul) ->
+ if not (ugraph_convertibility inferred_ugraph ug ul) then
+ raise (TypeCheckerFailure (lazy
+ ("inferred univ graph not equal with declared ugraph")))
+ else
+ ug,ul,obj
+ | None ->
+ CicUnivUtils.clean_and_fill uri obj inferred_ugraph
+;;
+
let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
let rec aux k t =
let module C = Cic in
let cobj,ugraph =
match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
- | CicEnvironment.UncheckedObj uobj ->
+ | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
logger#log (`Start_type_checking uri) ;
(* let's typecheck the uncooked obj *)
-
-(****************************************************************
- TASSI: FIXME qui e' inutile ricordarselo,
- tanto poi lo richiediamo alla cache che da quello su disco
-*****************************************************************)
-
- let ugraph_dust =
- (match uobj with
+ let inferred_ugraph =
+ match uobj with
C.Constant (_,Some te,ty,_,_) ->
let _,ugraph = type_of ~logger ty ugraph in
- 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
+ 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 (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))))
else
- ugraph'
+ ugraph
| C.Constant (_,None,ty,_,_) ->
(* only to check that ty is well-typed *)
- let _,ugraph' = type_of ~logger ty ugraph in
- ugraph'
+ let _,ugraph = type_of ~logger ty ugraph in
+ ugraph
| C.CurrentProof (_,conjs,te,ty,_,_) ->
- let _,ugraph1 =
+ let _,ugraph =
List.fold_left
(fun (metasenv,ugraph) ((_,context,ty) as conj) ->
- let _,ugraph' =
+ let _,ugraph =
type_of_aux' ~logger metasenv context ty ugraph
in
- (metasenv @ [conj],ugraph')
+ (metasenv @ [conj],ugraph)
) ([],ugraph) conjs
in
- let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
- let type_of_te,ugraph3 =
- type_of_aux' ~logger conjs [] te ugraph2
- in
- let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
+ let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
+ let type_of_te,ugraph = type_of_aux' ~logger conjs [] te ugraph in
+ let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
if not b then
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))))
else
- ugraph4
+ ugraph
| _ ->
raise
- (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))))
+ (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
in
- try
- CicEnvironment.set_type_checking_info uri;
- logger#log (`Type_checking_completed uri) ;
- match CicEnvironment.is_type_checked ~trust:false ugraph uri with
- CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
- | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
- with Invalid_argument s ->
- (*debug_print (lazy s);*)
- uobj,ugraph_dust
+ let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+ CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+ logger#log (`Type_checking_completed uri) ;
+ match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
in
match cobj,ugraph with
(C.Constant (_,_,ty,_,_)),g -> ty,g
(* 0 because a variable is never cooked => no partial cooking at one level *)
match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
- | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
+ | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph) ->
logger#log (`Start_type_checking uri) ;
(* only to check that ty is well-typed *)
- let _,ugraph1 = type_of ~logger ty ugraph in
- let ugraph2 =
- (match bo with
+ let _,ugraph = type_of ~logger ty ugraph in
+ let inferred_ugraph =
+ match bo with
None -> ugraph
| Some bo ->
- let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
- let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
+ let ty_bo,ugraph = type_of ~logger bo ugraph in
+ let b,ugraph = R.are_convertible [] ty_bo ty ugraph in
if not b then
raise (TypeCheckerFailure
(lazy ("Unknown variable:" ^ U.string_of_uri uri)))
else
- ugraph'')
+ ugraph
in
- (try
- CicEnvironment.set_type_checking_info uri ;
- logger#log (`Type_checking_completed uri) ;
- match CicEnvironment.is_type_checked ~trust:false ugraph uri with
- CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
- ty,ugraph'
- | CicEnvironment.CheckedObj _
- | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
- with Invalid_argument s ->
- (*debug_print (lazy s);*)
- ty,ugraph2)
+ let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+ CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+ logger#log (`Type_checking_completed uri) ;
+ (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ CicEnvironment.CheckedObj((C.Variable(_,_,ty,_,_)),ugraph)->ty,ugraph
+ | CicEnvironment.CheckedObj _
+ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
| _ ->
raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
let cobj,ugraph1 =
match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
- | CicEnvironment.UncheckedObj uobj ->
+ | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
logger#log (`Start_type_checking uri) ;
- let ugraph1_dust =
- check_mutual_inductive_defs ~logger uri uobj ugraph
- in
- (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
- try
- CicEnvironment.set_type_checking_info uri ;
- logger#log (`Type_checking_completed uri) ;
- (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
- CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
- | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
- )
- with
- Invalid_argument s ->
- (*debug_print (lazy s);*)
- uobj,ugraph1_dust
+ let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj ugraph in
+ let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+ CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
+ logger#log (`Type_checking_completed uri) ;
+ (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
+ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
+ )
in
match cobj with
C.InductiveDefinition (dl,_,_,_) ->
let cobj,ugraph1 =
match CicEnvironment.is_type_checked ~trust:true ugraph uri with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
- | CicEnvironment.UncheckedObj uobj ->
+ | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
logger#log (`Start_type_checking uri) ;
- let ugraph1_dust =
+ let inferred_ugraph =
check_mutual_inductive_defs ~logger uri uobj ugraph
in
- (* check ugraph1 validity ??? == ugraph' *)
- try
- CicEnvironment.set_type_checking_info uri ;
- logger#log (`Type_checking_completed uri) ;
- (match
- CicEnvironment.is_type_checked ~trust:false ugraph uri
- with
+ let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
+ CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
+ logger#log (`Type_checking_completed uri) ;
+ (match
+ CicEnvironment.is_type_checked ~trust:false ugraph uri
+ with
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ ->
raise CicEnvironmentError)
- with
- Invalid_argument s ->
- (*debug_print (lazy s);*)
- uobj,ugraph1_dust
in
match cobj with
C.InductiveDefinition (dl,_,_,_) ->
*)
;;
-let typecheck_obj0 ~logger uri ugraph =
+let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) =
let module C = Cic in
- function
- C.Constant (_,Some te,ty,_,_) ->
- let _,ugraph = type_of ~logger ty ugraph in
- let ty_te,ugraph = type_of ~logger te ugraph in
- let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
- if not b then
- raise (TypeCheckerFailure
- (lazy
- ("the type of the body is not the one expected:\n" ^
- CicPp.ppterm ty_te ^ "\nvs\n" ^
- CicPp.ppterm ty)))
- else
- ugraph
- | C.Constant (_,None,ty,_,_) ->
- (* only to check that ty is well-typed *)
- let _,ugraph = type_of ~logger ty ugraph in
- ugraph
- | C.CurrentProof (_,conjs,te,ty,_,_) ->
- (* this block is broken since the metasenv should
- * be topologically sorted before typing metas *)
- ignore(assert false);
- let _,ugraph =
- List.fold_left
- (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
- let _,ugraph =
- type_of_aux' ~logger metasenv context ty ugraph
- in
- metasenv @ [conj],ugraph
- ) ([],ugraph) conjs
- in
- let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
- let type_of_te,ugraph =
- type_of_aux' ~logger conjs [] te ugraph
- in
- let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
- if not b then
- 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))))
- else
+ let ugraph = CicUniv.empty_ugraph in
+ let inferred_ugraph =
+ match obj with
+ | C.Constant (_,Some te,ty,_,_) ->
+ let _,ugraph = type_of ~logger ty ugraph in
+ let ty_te,ugraph = type_of ~logger te ugraph in
+ let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
+ if not b then
+ raise (TypeCheckerFailure
+ (lazy
+ ("the type of the body is not the one expected:\n" ^
+ CicPp.ppterm ty_te ^ "\nvs\n" ^
+ CicPp.ppterm ty)))
+ else
+ ugraph
+ | C.Constant (_,None,ty,_,_) ->
+ (* only to check that ty is well-typed *)
+ let _,ugraph = type_of ~logger ty ugraph in
ugraph
- | C.Variable (_,bo,ty,_,_) ->
- (* only to check that ty is well-typed *)
- let _,ugraph = type_of ~logger ty ugraph in
- (match bo with
- None -> ugraph
- | Some bo ->
- let ty_bo,ugraph = type_of ~logger bo ugraph in
- let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
- if not b then
- raise (TypeCheckerFailure
- (lazy "the body is not the one expected"))
- else
- ugraph
- )
- | (C.InductiveDefinition _ as obj) ->
- check_mutual_inductive_defs ~logger uri obj ugraph
+ | C.CurrentProof (_,conjs,te,ty,_,_) ->
+ (* this block is broken since the metasenv should
+ * be topologically sorted before typing metas *)
+ ignore(assert false);
+ let _,ugraph =
+ List.fold_left
+ (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
+ let _,ugraph =
+ type_of_aux' ~logger metasenv context ty ugraph
+ in
+ metasenv @ [conj],ugraph
+ ) ([],ugraph) conjs
+ in
+ let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
+ let type_of_te,ugraph =
+ type_of_aux' ~logger conjs [] te ugraph
+ in
+ let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
+ if not b then
+ 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))))
+ else
+ ugraph
+ | C.Variable (_,bo,ty,_,_) ->
+ (* only to check that ty is well-typed *)
+ let _,ugraph = type_of ~logger ty ugraph in
+ (match bo with
+ None -> ugraph
+ | Some bo ->
+ let ty_bo,ugraph = type_of ~logger bo ugraph in
+ let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
+ if not b then
+ raise (TypeCheckerFailure
+ (lazy "the body is not the one expected"))
+ else
+ ugraph
+ )
+ | (C.InductiveDefinition _ as obj) ->
+ check_mutual_inductive_defs ~logger uri obj ugraph
+ in
+ check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
+;;
let typecheck uri =
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:true uri with ???? *)
match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
- CicEnvironment.CheckedObj (cobj,ugraph') ->
- (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
- cobj,ugraph'
- | CicEnvironment.UncheckedObj uobj ->
+ | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+ | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
(* let's typecheck the uncooked object *)
logger#log (`Start_type_checking 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;
- logger#log (`Type_checking_completed uri);
- match CicEnvironment.is_type_checked ~trust:false ugraph uri with
- CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
- | _ -> raise CicEnvironmentError
- with
- (*
- this is raised if set_type_checking_info is called on an object
- that has no associated universe file. If we are in univ_maker
- phase this is OK since univ_maker will properly commit the
- object.
- *)
- Invalid_argument s ->
- (*debug_print (lazy s);*)
- uobj,ugraph
+ let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
+ CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
+ logger#log (`Type_checking_completed uri);
+ match CicEnvironment.is_type_checked ~trust:false ugraph uri with
+ | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
+ | _ -> raise CicEnvironmentError
;;
let typecheck_obj ~logger uri obj =
- let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
- let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
- CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
+ let ugraph,univlist,obj = typecheck_obj0 ~logger uri (obj,None) in
+ CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
(** wrappers which instantiate fresh loggers *)
projects / helm.git / blobdiff