let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+ CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
in
if !fdebug = 0 then
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)
let ugraph_dust =
(match uobj with
- C.Constant (_,Some te,ty,_) ->
+ 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
(CicPp.ppterm ty)))
else
ugraph'
- | C.Constant (_,None,ty,_) ->
+ | 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,_) ->
+ | C.CurrentProof (_,conjs,te,ty,_,_) ->
let _,ugraph1 =
List.fold_left
(fun (metasenv,ugraph) ((_,context,ty) as conj) ->
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
- (C.Constant (_,_,ty,_)),g -> ty,g
- | (C.CurrentProof (_,_,_,ty,_)),g -> ty,g
+ (C.Constant (_,_,ty,_,_)),g -> ty,g
+ | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
| _ ->
raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
let module U = UriManager in
(* 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.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
+ | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
logger#log (`Start_type_checking uri) ;
(* only to check that ty is well-typed *)
let _,ugraph1 = type_of ~logger ty ugraph in
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') ->
+ CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
ty,ugraph'
| 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))
let (ok,paramsno,ity,cl,name) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let (name,_,ity,cl) = List.nth tl i in
(List.length tl = 1, paramsno, ity, cl, name)
| _ ->
(* inductive block definition. *)
and check_mutual_inductive_defs uri obj ugraph =
match obj with
- Cic.InductiveDefinition (itl, params, indparamsno) ->
+ Cic.InductiveDefinition (itl, params, indparamsno, _) ->
typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
| _ ->
raise (TypeCheckerFailure (
)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
- C.InductiveDefinition (dl,_,_) ->
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,arity,_) = List.nth dl i in
arity,ugraph1
| _ ->
raise CicEnvironmentError)
with
Invalid_argument s ->
- (*prerr_endline s;*)
+ (*debug_print s;*)
uobj,ugraph1_dust
in
match cobj with
- C.InductiveDefinition (dl,_,_) ->
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,_,cl) = List.nth dl i in
let (_,ty) = List.nth cl (j-1) in
ty,ugraph1
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let tys =
List.map
(fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
List.map (fun (n,_,ty,_) ->
(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
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let len = List.length tl in
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (tl,_,paramsno) ->
+ C.InductiveDefinition (tl,_,paramsno,_) ->
let (_,isinductive,_,cl) = List.nth tl i in
let tys =
List.map
with Not_found -> assert false
in
match obj with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,_,_) ->
let (_,_,_,cl) = List.nth itl i in
let (_,cons) = List.nth cl (j - 1) in
CicSubstitution.subst_vars exp_named_subst cons
(*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,_) ->
+ 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) , ugraph
when need_dummy ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,paramsno) ->
+ C.InductiveDefinition (itl,_,paramsno,_) ->
let tys =
List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
in
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 ->
(* TASSI: da verificare *)
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,paramsno) ->
+ C.InductiveDefinition (itl,_,paramsno,_) ->
let (_,_,_,cl) = List.nth itl i in
let tys =
List.map
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
with Not_found -> assert false
in
match obj with
- C.InductiveDefinition (_,_,parsno) -> parsno
+ C.InductiveDefinition (_,_,parsno,_) -> parsno
| _ ->
raise (TypeCheckerFailure
("Unknown mutual inductive definition:" ^
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 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 *)
with Not_found -> assert false
in
(match obj with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,_,_) ->
let (_,is_inductive,_,_) = List.nth itl i in
if is_inductive then None else (Some uri)
| _ ->
| C.Appl ((C.MutInd (uri,i,_))::_) ->
(let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match o with
- C.InductiveDefinition (itl,_,_) ->
+ C.InductiveDefinition (itl,_,_,_) ->
let (_,is_inductive,_,_) = List.nth itl i in
if is_inductive then None else (Some uri)
| _ ->
*)
;;
-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