raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
;;
-let debug_print = prerr_endline ;;
+let debug_print = fun _ -> () ;;
let rec split l n =
match (l,n) with
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)
CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph_dust
in
match cobj,ugraph with
| CicEnvironment.CheckedObj _
| CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
with Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
ty,ugraph2)
| _ ->
raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print 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 ->
(fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
exp_named_subst true
| C.MutCase (uri,i,outtype,term,pl) ->
- (match term with
+ (match CicReduction.whd 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
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 ->
function
[] -> []
| (Some (n,C.Decl t))::tl ->
- (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+ (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
| (Some (n,C.Def (t,None)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
| None::tl -> None::(aux (i+1) tl)
| (Some (n,C.Def (t,Some ty)))::tl ->
- (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
+ (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
in
aux 1 canonical_context
in
~subst metasenv context canonical_context l ugraph
in
(* assuming subst is well typed !!!!! *)
- ((CicSubstitution.lift_meta l ty), ugraph1)
- (* type_of_aux context (CicSubstitution.lift_meta l term) *)
+ ((CicSubstitution.subst_meta l ty), ugraph1)
+ (* type_of_aux context (CicSubstitution.subst_meta l term) *)
with CicUtil.Subst_not_found _ ->
let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
let ugraph1 =
check_metasenv_consistency ~logger
~subst metasenv context canonical_context l ugraph
in
- ((CicSubstitution.lift_meta l ty),ugraph1))
+ ((CicSubstitution.subst_meta l ty),ugraph1))
(* TASSI: CONSTRAINTS *)
| C.Sort (C.Type t) ->
let t' = CicUniv.fresh() in
else raise
(TypeCheckerFailure
(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))
+ ("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))
| 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
- "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))
+ ("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))
| _ ->
raise
(TypeCheckerFailure
if not branches_ok then
raise
(TypeCheckerFailure "Case analysys: wrong branch type");
- if not need_dummy then
- (C.Appl ((outtype::arguments)@[term])),ugraph5
- else if arguments = [] then
- outtype,ugraph5
- else
- (C.Appl (outtype::arguments)),ugraph5
+ let arguments' =
+ if not need_dummy then outtype::arguments@[term]
+ else outtype::arguments in
+ let outtype =
+ if need_dummy && arguments = [] then outtype
+ else CicReduction.head_beta_reduce (C.Appl arguments')
+ in
+ outtype,ugraph5
| C.Fix (i,fl) ->
let types_times_kl,ugraph1 =
(* WAS: list rev list map *)
*)
;;
-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') ->
- (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
+ (* debug_print ("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) ;
- (* prerr_endline ("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
+ (* debug_print ("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);
object.
*)
Invalid_argument s ->
- (*prerr_endline s;*)
- uobj,ugraph1
+ (*debug_print s;*)
+ uobj,ugraph
;;
-(** wrappers which instantiate fresh loggers *)
+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 type_of_aux' ?(subst = []) metasenv context t =
- let logger = new CicLogger.logger in
- type_of_aux' ~logger ~subst metasenv context t
+(** wrappers which instantiate fresh loggers *)
-let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
+let type_of_aux' ?(subst = []) metasenv context t ugraph =
let logger = new CicLogger.logger in
- typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno)
+ type_of_aux' ~logger ~subst metasenv context t ugraph
+let typecheck_obj uri obj =
+ let logger = new CicLogger.logger in
+ typecheck_obj ~logger uri obj
projects / helm.git / blobdiff