List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
in
C.Var (uri,exp_named_subst')
- | C.Meta _ -> assert false
+ | C.Meta (i,l) ->
+ let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
+ C.Meta (i,l)
| C.Sort _
| C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
*)
;;
-let typecheck uri ugraph =
+let typecheck_obj0 ~logger uri 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
+ ("the type of the body is not the one expected"))
+ 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,_,_) ->
+ 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 (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
+ ("the body is not the one expected"))
+ else
+ ugraph
+ )
+ | (C.InductiveDefinition _ as obj) ->
+ check_mutual_inductive_defs ~logger uri obj ugraph
+
+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 ugraph 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);*)
cobj,ugraph'
(* let's typecheck the uncooked object *)
logger#log (`Start_type_checking uri) ;
(* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
- let ugraph1 =
- (match uobj with
- C.Constant (_,Some te,ty,_,_) ->
- let _,ugraph1 = type_of ~logger ty ugraph in
- let ty_te,ugraph2 = type_of ~logger te ugraph1 in
- let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in
- if not b then
- raise (TypeCheckerFailure
- ("Unknown constant:" ^ U.string_of_uri uri))
- else
- ugraph3
- | C.Constant (_,None,ty,_,_) ->
- (* only to check that ty is well-typed *)
- let _,ugraph1 = type_of ~logger ty ugraph in
- ugraph1
- | C.CurrentProof (_,conjs,te,ty,_,_) ->
- let _,ugraph1 =
- List.fold_left
- (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
- let _,ugraph1 =
- type_of_aux' ~logger metasenv context ty ugraph
- in
- metasenv @ [conj],ugraph1
- ) ([],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
- if not b 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"
- (U.string_of_uri uri) (CicPp.ppterm type_of_te)
- (CicPp.ppterm ty)))
- else
- ugraph4
- | C.Variable (_,bo,ty,_,_) ->
- (* only to check that ty is well-typed *)
- let _,ugraph1 = type_of ~logger ty ugraph in
- (match bo with
- None -> ugraph1
- | Some bo ->
- let ty_bo,ugraph2 = type_of ~logger bo ugraph1 in
- let b,ugraph3 = R.are_convertible [] ty_bo ty ugraph2 in
- if not b then
- raise (TypeCheckerFailure
- ("Unknown variable:" ^ U.string_of_uri uri))
- else
- ugraph3
- )
- | C.InductiveDefinition _ ->
- check_mutual_inductive_defs ~logger uri uobj ugraph
- ) in
+ let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
try
CicEnvironment.set_type_checking_info uri;
logger#log (`Type_checking_completed uri);
*)
Invalid_argument s ->
(*debug_print s;*)
- uobj,ugraph1
+ 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)
+
(** wrappers which instantiate fresh loggers *)
let type_of_aux' ?(subst = []) metasenv context t ugraph =
let logger = new CicLogger.logger in
type_of_aux' ~logger ~subst metasenv context t ugraph
-let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
- let logger = new CicLogger.logger in
- typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno)
-
+let typecheck_obj uri obj =
+ let logger = new CicLogger.logger in
+ typecheck_obj ~logger uri obj
projects / helm.git / blobdiff