X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=c38c15b931cdea943fda830e4097790503ef5501;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=7e2715d0a8b592d9367652688817a3c651567c44;hpb=dd19b00878e9a29118141e8b178be6839c900ce9;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 7e2715d0a..c38c15b93 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -54,7 +54,22 @@ let rec split l n = raise (TypeCheckerFailure (lazy "Parameters number < left parameters number")) ;; -let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = +(* 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 res = @@ -75,7 +90,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t) + | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t) | C.Appl l -> C.Appl (List.map (aux k) l) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = @@ -83,7 +98,7 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = in C.Const (uri,exp_named_subst') | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' -> - if exp_named_subst != [] then + if check_exp_named_subst && exp_named_subst != [] then raise (TypeCheckerFailure (lazy ("non-empty explicit named substitution is applied to "^ "a mutual inductive type which is being defined"))) ; @@ -121,79 +136,89 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = cb t res; res in - aux 0 + aux (List.length context) ;; exception CicEnvironmentError;; -let rec type_of_constant ~logger uri ugraph = +let check_homogeneous_call context indparamsno n uri reduct tl = + let last = + List.fold_left + (fun k x -> + if k = 0 then 0 + else + match CicReduction.whd context x with + | Cic.Rel m when m = n - (indparamsno - k) -> k - 1 + | _ -> raise (TypeCheckerFailure (lazy + ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^ + string_of_int indparamsno ^ " fixed) is not homogeneous in "^ + "appl:\n"^ CicPp.ppterm reduct)))) + indparamsno tl + in + if last <> 0 then + raise (TypeCheckerFailure + (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ + UriManager.string_of_uri uri))) +;; + + +let rec type_of_constant ~logger uri orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph = - match CicEnvironment.is_type_checked ~trust:true ugraph uri with + match CicEnvironment.is_type_checked ~trust:true orig_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 _,ugraph = type_of ~logger ty CicUniv.empty_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 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 CicUniv.empty_ugraph in + ugraph | C.CurrentProof (_,conjs,te,ty,_,_) -> - let _,ugraph1 = + 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 + let _,ugraph = + type_of_aux' ~logger metasenv context ty ugraph + in + (metasenv @ [conj],ugraph) + ) ([],CicUniv.empty_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 orig_ugraph uri with + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError in match cobj,ugraph with (C.Constant (_,_,ty,_,_)),g -> ty,g @@ -201,42 +226,43 @@ let rec type_of_constant ~logger uri ugraph = | _ -> raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))) -and type_of_variable ~logger uri ugraph = +and type_of_variable ~logger uri orig_ugraph = let module C = Cic in let module R = CicReduction in 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,_,_)) -> + match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with + | CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph' + | 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 CicUniv.empty_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'') + else + 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 orig_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))) + raise (TypeCheckerFailure (lazy + ("Unknown variable:" ^ U.string_of_uri uri))) and does_not_occur ?(subst=[]) context n nn te = let module C = Cic in @@ -252,48 +278,55 @@ and does_not_occur ?(subst=[]) context n nn te = Failure _ -> assert false) | C.Sort _ | C.Implicit _ -> true - | C.Meta (_,l) -> + | C.Meta (mno,l) -> List.fold_right (fun x i -> match x with None -> i | Some x -> i && does_not_occur ~subst context n nn x) l true && (try - let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in + let (canonical_context,term,ty) = CicUtil.lookup_subst mno subst in does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term) with CicUtil.Subst_not_found _ -> true) | C.Cast (te,ty) -> - does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty + does_not_occur ~subst context n nn te && + does_not_occur ~subst context n nn ty | C.Prod (name,so,dest) -> does_not_occur ~subst context n nn so && does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest | C.Lambda (name,so,dest) -> does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) + does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) dest - | C.LetIn (name,so,dest) -> + | C.LetIn (name,so,ty,dest) -> does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Def (so,None))))::context) - (n + 1) (nn + 1) dest + does_not_occur ~subst context n nn ty && + does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context) + (n + 1) (nn + 1) dest | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true + List.for_all (does_not_occur ~subst context n nn) l | C.Var (_,exp_named_subst) | C.Const (_,exp_named_subst) | C.MutInd (_,_,exp_named_subst) | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x) - exp_named_subst true + List.for_all (fun (_,x) -> does_not_occur ~subst context n nn x) + exp_named_subst | C.MutCase (_,_,out,te,pl) -> - does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true + does_not_occur ~subst context n nn out && + does_not_occur ~subst context n nn te && + List.for_all (does_not_occur ~subst context n nn) pl | C.Fix (_,fl) -> let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = - List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,_,ty,bo) i -> @@ -304,8 +337,12 @@ and does_not_occur ?(subst=[]) context n nn te = let len = List.length fl in let n_plus_len = n + len in let nn_plus_len = nn + len in - let tys = - List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in List.fold_right (fun (_,ty,bo) i -> @@ -313,94 +350,104 @@ and does_not_occur ?(subst=[]) context n nn te = does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo ) fl true -(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) -(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *) -(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *) -(*CSC strictly_positive *) -(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *) -and weakly_positive context n nn uri te = +(* Inductive types being checked for positivity have *) +(* indexes x s.t. n < x <= nn. *) +and weakly_positive context n nn uri indparamsno posuri te = let module C = Cic in -(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) - let dummy_mutind = - C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[]) + (*CSC: Not very nice. *) + let leftno = + match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with + | Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno + | _ -> assert false in - (*CSC: mettere in cicSubstitution *) - let rec subst_inductive_type_with_dummy_mutind = + let dummy = Cic.Sort Cic.Prop in + (*CSC: to be moved in cicSubstitution? *) + let rec subst_inductive_type_with_dummy = function C.MutInd (uri',0,_) when UriManager.eq uri' uri -> - dummy_mutind + dummy | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> - dummy_mutind - | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te + let _, rargs = HExtlib.split_nth leftno tl in + if rargs = [] then dummy else Cic.Appl (dummy :: rargs) + | C.Cast (te,ty) -> subst_inductive_type_with_dummy te | C.Prod (name,so,ta) -> - C.Prod (name, subst_inductive_type_with_dummy_mutind so, - subst_inductive_type_with_dummy_mutind ta) + C.Prod (name, subst_inductive_type_with_dummy so, + subst_inductive_type_with_dummy ta) | C.Lambda (name,so,ta) -> - C.Lambda (name, subst_inductive_type_with_dummy_mutind so, - subst_inductive_type_with_dummy_mutind ta) + C.Lambda (name, subst_inductive_type_with_dummy so, + subst_inductive_type_with_dummy ta) + | C.LetIn (name,so,ty,ta) -> + C.LetIn (name, subst_inductive_type_with_dummy so, + subst_inductive_type_with_dummy ty, + subst_inductive_type_with_dummy ta) | C.Appl tl -> - C.Appl (List.map subst_inductive_type_with_dummy_mutind tl) + C.Appl (List.map subst_inductive_type_with_dummy tl) | C.MutCase (uri,i,outtype,term,pl) -> C.MutCase (uri,i, - subst_inductive_type_with_dummy_mutind outtype, - subst_inductive_type_with_dummy_mutind term, - List.map subst_inductive_type_with_dummy_mutind pl) + subst_inductive_type_with_dummy outtype, + subst_inductive_type_with_dummy term, + List.map subst_inductive_type_with_dummy pl) | C.Fix (i,fl) -> C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i, - subst_inductive_type_with_dummy_mutind ty, - subst_inductive_type_with_dummy_mutind bo)) fl) + subst_inductive_type_with_dummy ty, + subst_inductive_type_with_dummy bo)) fl) | C.CoFix (i,fl) -> C.CoFix (i,List.map (fun (name,ty,bo) -> (name, - subst_inductive_type_with_dummy_mutind ty, - subst_inductive_type_with_dummy_mutind bo)) fl) + subst_inductive_type_with_dummy ty, + subst_inductive_type_with_dummy bo)) fl) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) exp_named_subst in C.Const (uri,exp_named_subst') + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) + exp_named_subst + in + C.Var (uri,exp_named_subst') | C.MutInd (uri,typeno,exp_named_subst) -> let exp_named_subst' = List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) exp_named_subst in C.MutInd (uri,typeno,exp_named_subst') | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> let exp_named_subst' = List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) exp_named_subst in C.MutConstruct (uri,typeno,consno,exp_named_subst') | t -> t in - match CicReduction.whd context te with -(* - C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true -*) - C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true - | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true - | C.Prod (C.Anonymous,source,dest) -> - strictly_positive context n nn - (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest - | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> - (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive context n nn - (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (name,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest - | C.Prod (name,source,dest) -> - does_not_occur context n nn - (subst_inductive_type_with_dummy_mutind source)&& - weakly_positive ((Some (name,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest - | _ -> - raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) + (* this function has the same semantics of are_all_occurrences_positive + but the i-th context entry role is played by dummy and some checks + are skipped because we already know that are_all_occurrences_positive + of uri in te. *) + let rec aux context n nn te = + match CicReduction.whd context te with + | C.Appl (C.Sort C.Prop::tl) -> + List.for_all (does_not_occur context n nn) tl + | C.Sort C.Prop -> true + | C.Prod (name,source,dest) when + does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> + (* dummy abstraction, so we behave as in the anonimous case *) + strictly_positive context n nn indparamsno posuri source && + aux ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) dest + | C.Prod (name,source,dest) -> + does_not_occur context n nn source && + aux ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) dest + | _ -> + raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) + in + aux context n nn (subst_inductive_type_with_dummy te) (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) @@ -414,32 +461,36 @@ and instantiate_parameters params c = | (C.Cast (te,_), _) -> instantiate_parameters params te | (t,l) -> raise (AssertFailure (lazy "1")) -and strictly_positive context n nn te = +and strictly_positive context n nn indparamsno posuri te = let module C = Cic in let module U = UriManager in match CicReduction.whd context te with | t when does_not_occur context n nn t -> true - | C.Rel _ -> true + | C.Rel _ when indparamsno = 0 -> true | C.Cast (te,ty) -> (*CSC: bisogna controllare ty????*) - strictly_positive context n nn te + strictly_positive context n nn indparamsno posuri te | C.Prod (name,so,ta) -> does_not_occur context n nn so && - strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta - | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> + strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) + indparamsno posuri ta + | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn -> + check_homogeneous_call context indparamsno n posuri reduct tl; List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true - | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> + | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) + | (C.MutInd (uri,i,exp_named_subst)) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in let (ok,paramsno,ity,cl,name) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with C.InductiveDefinition (tl,_,paramsno,_) -> - let (name,_,ity,cl) = List.nth tl i in + let (name,_,ity,cl) = List.nth tl i in (List.length tl = 1, paramsno, ity, cl, name) (* (true, paramsno, ity, cl, name) *) | _ -> - raise - (TypeCheckerFailure - (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) + raise + (TypeCheckerFailure + (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) in let (params,arguments) = split tl paramsno in let lifted_params = List.map (CicSubstitution.lift 1) params in @@ -454,13 +505,12 @@ and strictly_positive context n nn te = List.fold_right (fun x i -> i && does_not_occur context n nn x) arguments true && - (*CSC: MEGAPATCH3 (sara' quella giusta?)*) List.fold_right (fun x i -> i && weakly_positive - ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri - x + ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri + indparamsno posuri x ) cl' true | t -> false @@ -468,30 +518,9 @@ and strictly_positive context n nn te = and are_all_occurrences_positive context uri indparamsno i n nn te = let module C = Cic in match CicReduction.whd context te with - C.Appl ((C.Rel m)::tl) when m = i -> - (*CSC: riscrivere fermandosi a 0 *) - (* let's check if the inductive type is applied at least to *) - (* indparamsno parameters *) - let last = - List.fold_left - (fun k x -> - if k = 0 then 0 - else - match CicReduction.whd context x with - C.Rel m when m = n - (indparamsno - k) -> k - 1 - | _ -> - raise (TypeCheckerFailure - (lazy - ("Non-positive occurence in mutual inductive definition(s) [1]" ^ - UriManager.string_of_uri uri))) - ) indparamsno tl - in - if last = 0 then - List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true - else - raise (TypeCheckerFailure - (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ - UriManager.string_of_uri uri))) + C.Appl ((C.Rel m)::tl) as reduct when m = i -> + check_homogeneous_call context indparamsno n uri reduct tl; + List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Rel m when m = i -> if indparamsno = 0 then true @@ -499,16 +528,10 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = raise (TypeCheckerFailure (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ UriManager.string_of_uri uri))) - | C.Prod (C.Anonymous,source,dest) -> - let b = strictly_positive context n nn source in - b && - are_all_occurrences_positive - ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno - (i+1) (n + 1) (nn + 1) dest | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> + does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive context n nn source && + strictly_positive context n nn indparamsno uri source && are_all_occurrences_positive ((Some (name,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest @@ -540,36 +563,48 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (* constructors using Prods *) let len = List.length itl in let tys = - List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in + List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in let _,ugraph2 = List.fold_right - (fun (_,_,_,cl) (i,ugraph) -> - let ugraph'' = + (fun (_,_,ty,cl) (i,ugraph) -> + let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in + let ugraph'' = List.fold_left (fun ugraph (name,te) -> - let debrujinedte = debrujin_constructor uri len te in - let augmented_term = - List.fold_right - (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i)) - itl debrujinedte - in - let _,ugraph' = type_of ~logger augmented_term ugraph in + let te = debrujin_constructor uri len [] te in + let context,te = split_prods ~subst:[] tys indparamsno te in + let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in + let ugraph = + match + CicReduction.whd context con_sort, CicReduction.whd [] ty_sort + with + Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) + | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2) + | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2) + | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) -> + CicUniv.add_ge u2 u1 ugraph + | Cic.Sort _, Cic.Sort Cic.Prop + | Cic.Sort _, Cic.Sort Cic.CProp _ + | Cic.Sort _, Cic.Sort Cic.Set + | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph + | a,b -> + raise + (TypeCheckerFailure + (lazy ("Wrong constructor or inductive arity shape: "^ + CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) in (* let's check also the positivity conditions *) if - not - (are_all_occurrences_positive tys uri indparamsno i 0 len - debrujinedte) + not + (are_all_occurrences_positive context uri indparamsno + (i+indparamsno) indparamsno (len+indparamsno) te) then - begin - prerr_endline (UriManager.string_of_uri uri); - prerr_endline (string_of_int (List.length tys)); - raise - (TypeCheckerFailure - (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end + raise + (TypeCheckerFailure + (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) else - ugraph' + ugraph ) ugraph cl in - (i + 1),ugraph'' + (i + 1),ugraph'' ) itl (1,ugrap1) in ugraph2 @@ -579,142 +614,120 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = and check_mutual_inductive_defs uri obj ugraph = match obj with Cic.InductiveDefinition (itl, params, indparamsno, _) -> - typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph + typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph | _ -> - raise (TypeCheckerFailure ( - lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + raise (TypeCheckerFailure ( + lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) -and type_of_mutual_inductive_defs ~logger uri i ugraph = +and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = - match CicEnvironment.is_type_checked ~trust:true ugraph uri with + match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' - | CicEnvironment.UncheckedObj uobj -> - 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 + | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> + logger#log (`Start_type_checking uri) ; + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_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 orig_ugraph uri with + CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') + | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError + ) in - match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,arity,_) = List.nth dl i in - arity,ugraph1 - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) - -and type_of_mutual_inductive_constr ~logger uri i j ugraph = + match cobj with + | C.InductiveDefinition (dl,_,_,_) -> + let (_,_,arity,_) = List.nth dl i in + arity,ugraph1 + | _ -> + raise (TypeCheckerFailure + (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) + +and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = - match CicEnvironment.is_type_checked ~trust:true ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' - | CicEnvironment.UncheckedObj uobj -> - logger#log (`Start_type_checking uri) ; - let ugraph1_dust = - 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 - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' - | CicEnvironment.UncheckedObj _ -> - raise CicEnvironmentError) - with - Invalid_argument s -> - (*debug_print (lazy s);*) - uobj,ugraph1_dust + match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> + logger#log (`Start_type_checking uri) ; + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_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 orig_ugraph uri + with + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj _ -> + raise CicEnvironmentError) in match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cl) = List.nth dl i in + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,ugraph1 | _ -> - raise (TypeCheckerFailure + raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) and recursive_args context n nn te = let module C = Cic in - match CicReduction.whd context te with - C.Rel _ -> [] - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ (*CSC ??? *) -> - raise (AssertFailure (lazy "3")) (* due to type-checking *) - | C.Prod (name,so,de) -> - (not (does_not_occur context n nn so)) :: - (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de) - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "4")) (* due to type-checking *) - | C.Appl _ -> [] - | C.Const _ -> raise (AssertFailure (lazy "5")) - | C.MutInd _ - | C.MutConstruct _ - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *) + match CicReduction.whd context te with + C.Rel _ + | C.MutInd _ -> [] + | C.Var _ + | C.Meta _ + | C.Sort _ + | C.Implicit _ + | C.Cast _ (*CSC ??? *) -> + raise (AssertFailure (lazy "3")) (* due to type-checking *) + | C.Prod (name,so,de) -> + (not (does_not_occur context n nn so)) :: + (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de) + | C.Lambda _ + | C.LetIn _ -> + raise (AssertFailure (lazy "4")) (* due to type-checking *) + | C.Appl _ -> [] + | C.Const _ -> raise (AssertFailure (lazy "5")) + | C.MutConstruct _ + | C.MutCase _ + | C.Fix _ + | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *) -and get_new_safes ~subst context p c rl safes n nn x = +and get_new_safes ~subst context p rl safes n nn x = let module C = Cic in let module U = UriManager in let module R = CicReduction in - match (R.whd ~subst context c, R.whd ~subst context p, rl) with - (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) -> - (* we are sure that the two sources are convertible because we *) - (* have just checked this. So let's go along ... *) - let safes' = - List.map (fun x -> x + 1) safes - in - let safes'' = - if b then 1::safes' else safes' - in - get_new_safes ~subst ((Some (name,(C.Decl so)))::context) - ta2 ta1 tl safes'' (n+1) (nn+1) (x+1) - | (C.Prod _, (C.MutConstruct _ as e), _) - | (C.Prod _, (C.Rel _ as e), _) - | (C.MutInd _, e, []) - | (C.Appl _, e, []) -> (e,safes,n,nn,x,context) - | (c,p,l) -> - (* CSC: If the next exception is raised, it just means that *) - (* CSC: the proof-assistant allows to use very strange things *) - (* CSC: as a branch of a case whose type is a Prod. In *) - (* CSC: particular, this means that a new (C.Prod, x,_) case *) - (* CSC: must be considered in this match. (e.g. x = MutCase) *) + match R.whd ~subst context p, rl with + | C.Lambda (name,so,ta), b::tl -> + let safes = List.map (fun x -> x + 1) safes in + let safes = if b then 1::safes else safes in + get_new_safes ~subst ((Some (name,(C.Decl so)))::context) + ta tl safes (n+1) (nn+1) (x+1) + | C.MutConstruct _ as e, _ + | (C.Rel _ as e), _ + | e, [] -> (e,safes,n,nn,x,context) + | p,_::_ -> raise (AssertFailure (lazy - (Printf.sprintf "Get New Safes: c=%s ; p=%s" - (CicPp.ppterm c) (CicPp.ppterm p)))) + (Printf.sprintf "Get New Safes: p=%s" (CicPp.ppterm p)))) and split_prods ~subst context n te = let module C = Cic in let module R = CicReduction in match (n, R.whd ~subst context te) with (0, _) -> context,te - | (n, C.Prod (name,so,ta)) when n > 0 -> + | (n, C.Sort _) when n <= 0 -> context,te + | (n, C.Prod (name,so,ta)) -> split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta | (_, _) -> raise (AssertFailure (lazy "8")) @@ -731,193 +744,128 @@ and eat_lambdas ~subst context n te = | (n, te) -> raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))) -(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) -and check_is_really_smaller_arg ~subst context n nn kl x safes te = - (*CSC: forse la whd si puo' fare solo quando serve veramente. *) - (*CSC: cfr guarded_by_destructors *) +and specialize_inductive_type ~logger ~subst ~metasenv context t = + let ty,_= type_of_aux' ~logger ~subst metasenv context t CicUniv.oblivion_ugraph in + match CicReduction.whd ~subst context ty with + | Cic.MutInd (uri,_,exp) + | Cic.Appl (Cic.MutInd (uri,_,exp) :: _) as ty -> + let args = match ty with Cic.Appl (_::tl) -> tl | _ -> [] in + let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + (match o with + | Cic.InductiveDefinition (tl,_,paramsno,_) -> + let left_args,_ = HExtlib.split_nth paramsno args in + List.map (fun (name, isind, arity, cl) -> + let arity = CicSubstitution.subst_vars exp arity in + let arity = instantiate_parameters left_args arity in + let cl = + List.map + (fun (id,ty) -> + let ty = CicSubstitution.subst_vars exp ty in + id, instantiate_parameters left_args ty) + cl + in + name, isind, arity, cl) + tl, paramsno + | _ -> assert false) + | _ -> assert false + +and check_is_really_smaller_arg + ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes te += let module C = Cic in let module U = UriManager in + (*CSC: we could perform beta-iota(-zeta?) immediately, and + delta only on-demand when it fails without *) match CicReduction.whd ~subst context te with C.Rel m when List.mem m safes -> true - | C.Rel _ -> false - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ -(* | C.Cast (te,ty) -> - check_is_really_smaller_arg ~subst n nn kl x safes te && - check_is_really_smaller_arg ~subst n nn kl x safes ty*) -(* | C.Prod (_,so,ta) -> - check_is_really_smaller_arg ~subst n nn kl x safes so && - check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1) - (List.map (fun x -> x + 1) safes) ta*) - | C.Prod _ -> raise (AssertFailure (lazy "10")) - | C.Lambda (name,so,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.Appl (he::_) -> - (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *) - (*CSC: solo perche' non abbiamo trovato controesempi *) - check_is_really_smaller_arg ~subst context n nn kl x safes he - | C.Appl [] -> raise (AssertFailure (lazy "11")) + | C.Rel _ + | C.MutConstruct _ | C.Const _ - | C.MutInd _ -> raise (AssertFailure (lazy "12")) - | C.MutConstruct _ -> false + | C.Var _ -> false + | C.Appl (he::_) -> + check_is_really_smaller_arg rec_uri rec_uri_len + ~logger ~metasenv ~subst context n nn kl x safes he + | C.Lambda (name,ty,ta) -> + check_is_really_smaller_arg rec_uri rec_uri_len + ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context) + (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta | C.MutCase (uri,i,outtype,term,pl) -> (match term with - C.Rel m when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let tys = - List.map - (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl - in - let (_,isinductive,_,cl) = List.nth tl i in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,List.length tl,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - in - if not isinductive then - List.fold_right - (fun p i -> - 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 (lazy "not enough patterns")) - in - List.fold_right - (fun (p,(_,c)) i -> - let rl' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args lefts_and_tys 0 len debrujinedte - in - let (e,safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true - | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let (_,isinductive,_,cl) = List.nth tl i in - let tys = - List.map (fun (n,_,ty,_) -> - Some(Cic.Name n,(Cic.Decl ty))) tl - in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,List.length tl,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) - in - if not isinductive then - List.fold_right - (fun p i -> - 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 (lazy "not enough patterns")) - in - (*CSC: supponiamo come prima che nessun controllo sia necessario*) - (*CSC: sugli argomenti di una applicazione *) - List.fold_right - (fun (p,(_,c)) i -> - let rl' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args lefts_and_tys 0 len debrujinedte - in - let (e, safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true + | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x -> + let tys,_ = + specialize_inductive_type ~logger ~subst ~metasenv context term + in + let tys_ctx,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ([],0) tys + in + let _,isinductive,_,cl = List.nth tys i in + if not isinductive then + List.for_all + (check_is_really_smaller_arg rec_uri rec_uri_len + ~logger ~metasenv ~subst context n nn kl x safes) + pl + else + List.for_all2 + (fun p (_,c) -> + let rec_params = + let c = + debrujin_constructor ~check_exp_named_subst:false + rec_uri rec_uri_len context c in + let len_ctx = List.length context in + recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c + in + let (e, safes',n',nn',x',context') = + get_new_safes ~subst context p rec_params safes n nn x + in + check_is_really_smaller_arg rec_uri rec_uri_len + ~logger ~metasenv ~subst context' n' nn' kl x' safes' e + ) pl cl | _ -> - List.fold_right - (fun p i -> - i && check_is_really_smaller_arg ~subst context n nn kl x safes p - ) pl true + List.for_all + (check_is_really_smaller_arg + rec_uri rec_uri_len ~logger ~metasenv ~subst + context n nn kl x safes) pl ) | C.Fix (_, fl) -> let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl - and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,_,ty,bo) i -> - i && - check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true - | C.CoFix (_, fl) -> - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,ty,bo) i -> - i && - check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl + List.for_all + (fun (_,_,_,bo) -> + check_is_really_smaller_arg + rec_uri rec_uri_len ~logger ~metasenv ~subst + (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo - ) fl true + ) fl + | t -> + raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t))) -and guarded_by_destructors ~subst context n nn kl x safes = +and guarded_by_destructors + ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes t += let module C = Cic in let module U = UriManager in - function + let t = CicReduction.whd ~delta:false ~subst context t in + let res = + match t with C.Rel m when m > n && m <= nn -> false | C.Rel m -> - (match List.nth context (n-1) with + (match List.nth context (m-1) with Some (_,C.Decl _) -> true | Some (_,C.Def (bo,_)) -> - guarded_by_destructors ~subst context m nn kl x safes + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes (CicSubstitution.lift m bo) | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) ) @@ -925,398 +873,282 @@ and guarded_by_destructors ~subst context n nn kl x safes = | C.Sort _ | C.Implicit _ -> true | C.Cast (te,ty) -> - guarded_by_destructors ~subst context n nn kl x safes te && - guarded_by_destructors ~subst context n nn kl x safes ty + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes te && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty | C.Prod (name,so,ta) -> - guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Lambda (name,so,ta) -> - guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context) - (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta - | C.LetIn (name,so,ta) -> - guarded_by_destructors ~subst context n nn kl x safes so && - guarded_by_destructors ~subst ((Some (name,(C.Def (so,None))))::context) + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta + | C.LetIn (name,so,ty,ta) -> + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Def (so,ty))))::context) + (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> let k = List.nth kl (m - n - 1) in if not (List.length tl > k) then false else - List.fold_right - (fun param i -> - i && guarded_by_destructors ~subst context n nn kl x safes param - ) tl true && - check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k) - | C.Appl tl -> - List.fold_right - (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t) - tl true + List.for_all + (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) tl && + check_is_really_smaller_arg + rec_uri rec_uri_len + ~logger ~metasenv ~subst context n nn kl x safes (List.nth tl k) | C.Var (_,exp_named_subst) | C.Const (_,exp_named_subst) | C.MutInd (_,_,exp_named_subst) | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right - (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t) - exp_named_subst true + List.for_all + (fun (_,t) -> guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t) + exp_named_subst | C.MutCase (uri,i,outtype,term,pl) -> (match CicReduction.whd ~subst context term with - C.Rel m when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let len = List.length tl in - let (_,isinductive,_,cl) = List.nth tl i in - let tys = - List.map (fun (n,_,ty,_) -> - Some(Cic.Name n,(Cic.Decl ty))) tl - in - let cl' = - List.map - (fun (id,ty) -> - let debrujinedty = debrujin_constructor uri len ty in - (id, snd (split_prods ~subst tys paramsno ty), - snd (split_prods ~subst tys paramsno debrujinedty) - )) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,len,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + | C.Rel m + | C.Appl ((C.Rel m)::_) as t when List.mem m safes || m = x -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + List.for_all + (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) + tl && + let tys,_ = + specialize_inductive_type ~logger ~subst ~metasenv context t in - if not isinductive then - guarded_by_destructors ~subst context n nn kl x safes outtype && - guarded_by_destructors ~subst context n nn kl x safes term && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun p i -> - i && guarded_by_destructors ~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 (lazy "not enough patterns")) - in - guarded_by_destructors ~subst context n nn kl x safes outtype && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun (p,(_,c,brujinedc)) i -> - let rl' = recursive_args lefts_and_tys 0 len brujinedc in - let (e,safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - guarded_by_destructors ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true - | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> - let (lefts_and_tys,len,isinductive,paramsno,cl) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (tl,_,paramsno,_) -> - let (_,isinductive,_,cl) = List.nth tl i in - let tys = - List.map - (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl - in - let cl' = - List.map - (fun (id,ty) -> - (id, snd (split_prods ~subst tys paramsno ty))) cl in - let lefts = - match tl with - [] -> assert false - | (_,_,ty,_)::_ -> - fst (split_prods ~subst [] paramsno ty) - in - (tys@lefts,List.length tl,isinductive,paramsno,cl') - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + let tys_ctx,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ([],0) tys in + let _,isinductive,_,cl = List.nth tys i in if not isinductive then - guarded_by_destructors ~subst context n nn kl x safes outtype && - guarded_by_destructors ~subst context n nn kl x safes term && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun p i -> - i && guarded_by_destructors ~subst context n nn kl x safes p) - pl true + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term && + List.for_all + (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) + pl else - let pl_and_cl = - try - List.combine pl cl - with - Invalid_argument _ -> - raise (TypeCheckerFailure (lazy "not enough patterns")) - in - guarded_by_destructors ~subst context n nn kl x safes outtype && - (*CSC: manca ??? il controllo sul tipo di term? *) - List.fold_right - (fun t i -> - i && guarded_by_destructors ~subst context n nn kl x safes t) - tl true && - List.fold_right - (fun (p,(_,c)) i -> - let rl' = - let debrujinedte = debrujin_constructor uri len c in - recursive_args lefts_and_tys 0 len debrujinedte - in - let (e, safes',n',nn',x',context') = - get_new_safes ~subst context p c rl' safes n nn x - in - i && - guarded_by_destructors ~subst context' n' nn' kl x' safes' e - ) pl_and_cl true + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype && + List.for_all2 + (fun p (_,c) -> + let rec_params = + let c = + debrujin_constructor ~check_exp_named_subst:false + rec_uri rec_uri_len context c in + let len_ctx = List.length context in + recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c + in + let (e, safes',n',nn',x',context') = + get_new_safes ~subst context p rec_params safes n nn x + in + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context' n' nn' kl x' safes' e + ) pl cl | _ -> - guarded_by_destructors ~subst context n nn kl x safes outtype && - guarded_by_destructors ~subst context n nn kl x safes term && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right - (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p) + (fun p i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes p) pl true ) - | C.Fix (_, fl) -> + | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t-> + let l = match t with C.Appl (_::tl) -> tl | _ -> [] in let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - and x_plus_len = x + len - and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl - and safes' = List.map (fun x -> x + len) safes in - List.fold_right - (fun (_,_,ty,bo) i -> - i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && - guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl - x_plus_len safes' bo - ) fl true + let n_plus_len = n + len in + let nn_plus_len = nn + len in + let x_plus_len = x + len in + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl in + let safes' = List.map (fun x -> x + len) safes in + List.for_all + (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) l && + snd (List.fold_left + (fun (fixno',i) (_,recno,ty,bo) -> + fixno'+1, + i && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty && + if + fixno' = fixno && + List.length l > recno && + (*case where the recursive argument is already really_smaller *) + check_is_really_smaller_arg + rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes + (List.nth l recno) + then + let bo_without_lambdas,_,context = + eat_lambdas ~subst (tys@context) (recno+1) bo + in + (* we assume the formal argument to be safe *) + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context (n_plus_len+recno+1) + (nn_plus_len+recno+1) kl (x_plus_len+recno+1) + (1::List.map (fun x -> x+recno+1) safes') + bo_without_lambdas + else + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len + kl x_plus_len safes' bo + ) (0,true) fl) | C.CoFix (_, fl) -> let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len and x_plus_len = x + len - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> i && - guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty && - guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty && + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len kl x_plus_len safes' bo ) fl true + | C.Appl tl -> + List.fold_right + (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t) + tl true + in + if res then res + else + let t' = CicReduction.whd ~subst context t in + if t = t' then + false + else + guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t' (* the boolean h means already protected *) (* args is the list of arguments the type of the constructor that may be *) (* found in head position must be applied to. *) -and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI = +and guarded_by_constructors ~logger ~subst ~metasenv indURI = let module C = Cic in - (*CSC: There is a lot of code replication between the cases X and *) - (*CSC: (C.Appl X tl). Maybe it will be better to define a function *) - (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *) + let rec aux context n nn h te = match CicReduction.whd ~subst context te with - C.Rel m when m > n && m <= nn -> h - | C.Rel _ -> true - | C.Meta _ + | C.Rel m when m > n && m <= nn -> h + | C.Rel _ + | C.Meta _ -> true | C.Sort _ | C.Implicit _ | C.Cast _ | C.Prod _ - | C.LetIn _ -> - (* the term has just been type-checked *) - raise (AssertFailure (lazy "17")) + | C.MutInd _ + | C.LetIn _ -> raise (AssertFailure (lazy "17")) | C.Lambda (name,so,de) -> does_not_occur ~subst context n nn so && - guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context) - (n + 1) (nn + 1) h de args coInductiveTypeURI + aux ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) h de | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> - h && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true - | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) -> - let consty = - let obj,_ = - try - CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri - with Not_found -> assert false - in - match obj with - 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 - | _ -> - raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) + h && List.for_all (does_not_occur ~subst context n nn) tl + | C.MutConstruct (_,_,_,exp_named_subst) -> + List.for_all + (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst + | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) as t -> + List.for_all + (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst && + let consty, len_tys, tys_ctx, paramsno = + let tys, paramsno = + specialize_inductive_type ~logger ~subst ~metasenv context t in + let _,_,_,cl = List.nth tys i in + let _,ty = List.nth cl (j-1) in + ty, List.length tys, + fst(List.fold_left + (fun (types,len) (n,_,ty,_) -> + Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) + ([],0) tys), paramsno in - let rec analyse_branch context ty te = - match CicReduction.whd ~subst context ty with - C.Meta _ -> raise (AssertFailure (lazy "34")) - | C.Rel _ - | C.Var _ - | C.Sort _ -> - does_not_occur ~subst context n nn te - | C.Implicit _ - | C.Cast _ -> - raise (AssertFailure (lazy "24"))(* due to type-checking *) - | C.Prod (name,so,de) -> - analyse_branch ((Some (name,(C.Decl so)))::context) de te - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "25"))(* due to type-checking *) - | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.Appl ((C.MutInd (uri,_,_))::_) -> - guarded_by_constructors ~subst context n nn true te tl - coInductiveTypeURI - | C.Appl _ -> - does_not_occur ~subst context n nn te - | C.Const _ -> raise (AssertFailure (lazy "26")) - | C.MutInd (uri,_,_) when uri == coInductiveTypeURI -> - guarded_by_constructors ~subst context n nn true te [] - coInductiveTypeURI - | C.MutInd _ -> - does_not_occur ~subst context n nn te - | C.MutConstruct _ -> raise (AssertFailure (lazy "27")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "28"))(* due to type-checking *) + let rec_params = + let c = + debrujin_constructor ~check_exp_named_subst:false + indURI len_tys context consty in - let rec analyse_instantiated_type context ty l = - match CicReduction.whd ~subst context ty with - C.Rel _ - | C.Var _ - | C.Meta _ - | C.Sort _ - | C.Implicit _ - | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *) - | C.Prod (name,so,de) -> - begin - match l with - [] -> true - | he::tl -> - analyse_branch context so he && - analyse_instantiated_type - ((Some (name,(C.Decl so)))::context) de tl - end - | C.Lambda _ - | C.LetIn _ -> - raise (AssertFailure (lazy "30"))(* due to type-checking *) - | C.Appl _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.Const _ -> raise (AssertFailure (lazy "31")) - | C.MutInd _ -> - List.fold_left - (fun i x -> i && does_not_occur ~subst context n nn x) true l - | C.MutConstruct _ -> raise (AssertFailure (lazy "32")) - (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *) - (*CSC: in head position. *) - | C.MutCase _ - | C.Fix _ - | C.CoFix _ -> - raise (AssertFailure (lazy "33"))(* due to type-checking *) - in - let rec instantiate_type args consty = - function - [] -> true - | tlhe::tltl as l -> - let consty' = CicReduction.whd ~subst context consty in - match args with - he::tl -> - begin - match consty' with - C.Prod (_,_,de) -> - let instantiated_de = CicSubstitution.subst he de in - (*CSC: siamo sicuri che non sia troppo forte? *) - does_not_occur ~subst context n nn tlhe & - instantiate_type tl instantiated_de tltl - | _ -> - (*CSC:We do not consider backbones with a MutCase, a *) - (*CSC:FixPoint, a CoFixPoint and so on in head position.*) - raise (AssertFailure (lazy "23")) - end - | [] -> analyse_instantiated_type context consty' l - (* These are all the other cases *) - in - instantiate_type args consty tl - | C.Appl ((C.CoFix (_,fl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - let len = List.length fl in - let n_plus_len = n + len - and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo args coInductiveTypeURI - ) fl true - | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) -> - List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl && - does_not_occur ~subst context n nn out && - does_not_occur ~subst context n nn te && - List.fold_right - (fun x i -> - i && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) -> - List.fold_right - (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true - | C.MutInd _ -> assert false - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right - (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true - | C.MutCase (_,_,out,te,pl) -> + let len_ctx = List.length context in + recursive_args (context@tys_ctx) len_ctx (len_ctx+len_tys) c + in + let rec analyse_instantiated_type rec_spec args = + match rec_spec, args with + | h::rec_spec, he::args -> + aux context n nn h he && + analyse_instantiated_type rec_spec args + | _,[] -> true + | _ -> raise (AssertFailure (lazy + ("Too many args for constructor: " ^ String.concat " " + (List.map (fun x-> CicPp.ppterm x) args)))) + in + let left, args = HExtlib.split_nth paramsno tl in + List.for_all (does_not_occur ~subst context n nn) left && + analyse_instantiated_type rec_params args + | C.Appl ((C.MutCase (_,_,out,te,pl))::_) + | C.MutCase (_,_,out,te,pl) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + List.for_all (does_not_occur ~subst context n nn) tl && does_not_occur ~subst context n nn out && - does_not_occur ~subst context n nn te && - List.fold_right - (fun x i -> - i && - guarded_by_constructors ~subst context n nn h x args - coInductiveTypeURI - ) pl true - | C.Fix (_,fl) -> + does_not_occur ~subst context n nn te && + List.for_all (aux context n nn h ) pl + | C.Fix (_,fl) + | C.Appl (C.Fix (_,fl)::_) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in - List.fold_right - (fun (_,_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo - ) fl true - | C.CoFix (_,fl) -> - let len = List.length fl in + and tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in + List.for_all (does_not_occur ~subst context n nn) tl && + List.for_all + (fun (_,_,ty,bo) -> + does_not_occur ~subst context n nn ty && + aux (tys@context) n_plus_len nn_plus_len h bo) + fl + | C.Appl ((C.CoFix (_,fl))::_) + | C.CoFix (_,fl) as t -> + let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in + let len = List.length fl in let n_plus_len = n + len and nn_plus_len = nn + len - (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *) - and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len - h bo - args coInductiveTypeURI - ) fl true + and tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl + in + List.for_all (does_not_occur ~subst context n nn) tl && + List.for_all + (fun (_,ty,bo) -> + does_not_occur ~subst context n nn ty && + aux (tys@context) n_plus_len nn_plus_len h bo) + fl + | C.Var _ + | C.Const _ + | C.Appl _ as t -> does_not_occur ~subst context n nn t + in + aux + +and is_non_recursive ctx paramsno t uri = + let t = debrujin_constructor uri 1 [] t in +(* let ctx, t = split_prods ~subst:[] ctx paramsno t in *) + let len = List.length ctx in + let rec aux ctx n nn t = + match CicReduction.whd ctx t with + | Cic.Prod (name,src,tgt) -> + does_not_occur ctx n nn src && + aux (Some (name,Cic.Decl src) :: ctx) (n+1) (nn+1) tgt + | (Cic.Rel k) + | Cic.Appl (Cic.Rel k :: _) when k = nn -> true + | t -> assert false + in + aux ctx (len-1) len t and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy ind arity1 arity2 ugraph = @@ -1325,29 +1157,30 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let arity1 = CicReduction.whd ~subst context arity1 in let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy = match arity1, CicReduction.whd ~subst context arity2 with - (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) -> + (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) -> let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in if b then - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + check_allowed_sort_elimination ~subst ~metasenv ~logger + ((Some (name,C.Decl so1))::context) uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1 else - false,ugraph1 + false,ugraph1 | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy -> let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in if not b then - false,ugraph1 + false,ugraph1 else check_allowed_sort_elimination_aux ugraph1 ((Some (name,C.Decl so))::context) ta true | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph | (C.Sort C.Prop, C.Sort C.Set) - | (C.Sort C.Prop, C.Sort C.CProp) + | (C.Sort C.Prop, C.Sort (C.CProp _)) | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,paramsno,_) -> let itl_len = List.length itl in let (name,_,ty,cl) = List.nth itl i in @@ -1356,8 +1189,13 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let non_informative,ugraph = if cl_len = 0 then true,ugraph else - is_non_informative ~logger [Some (C.Name name,C.Decl ty)] - paramsno (snd (List.nth cl 0)) ugraph + let b, ug = + is_non_informative ~logger [Some (C.Name name,C.Decl ty)] + paramsno (snd (List.nth cl 0)) ugraph + in + b && + is_non_recursive [Some (C.Name name,C.Decl ty)] + paramsno (snd (List.nth cl 0)) uri, ug in (* is it a singleton or empty non recursive and non informative definition? *) @@ -1366,19 +1204,16 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i false,ugraph | _ -> raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) ) | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph - | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _))) + | (C.Sort C.Set, C.Sort (C.Type _)) + | (C.Sort C.Set, C.Sort (C.CProp _)) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,paramsno,_) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl @@ -1386,21 +1221,22 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let (_,_,_,cl) = List.nth itl i in (List.fold_right (fun (_,x) (i,ugraph) -> - if i then - is_small ~logger tys paramsno x ugraph - else - false,ugraph - ) cl (true,ugraph)) + if i then + is_small ~logger tys paramsno x ugraph + else + false,ugraph + ) cl (true,ugraph)) | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) ) | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph + | (C.Sort (C.CProp _), C.Sort _) when need_dummy -> true , ugraph | (_,_) -> false,ugraph in check_allowed_sort_elimination_aux ugraph context arity2 need_dummy - + and type_of_branch ~subst context argsno need_dummy outtype term constype = let module C = Cic in let module R = CicReduction in @@ -1445,11 +1281,9 @@ and check_metasenv_consistency ~logger ~subst metasenv context [] -> [] | (Some (n,C.Decl t))::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.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.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl) + | (Some (n,C.Def (t,ty)))::tl -> + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1458,33 +1292,50 @@ and check_metasenv_consistency ~logger ~subst metasenv context match (t,ct) with | _,None -> ugraph | Some t,Some (_,C.Def (ct,_)) -> - let b,ugraph1 = - R.are_convertible ~subst ~metasenv context t ct ugraph - in - if not b then - raise - (TypeCheckerFailure - (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))) - else - ugraph1 + (*CSC: the following optimization is to avoid a possibly expensive + reduction that can be easily avoided and that is quite + frequent. However, this is better handled using levels to + control reduction *) + let optimized_t = + match t with + Cic.Rel n -> + (try + match List.nth context (n - 1) with + Some (_,C.Def (te,_)) -> S.lift n te + | _ -> t + with + Failure _ -> t) + | _ -> t + in +(*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!" +else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*) + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context optimized_t ct ugraph + in + if not b then + raise + (TypeCheckerFailure + (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))) + else + ugraph1 | Some t,Some (_,C.Decl ct) -> let type_t,ugraph1 = - type_of_aux' ~logger ~subst metasenv context t ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv context type_t ct ugraph1 - in + type_of_aux' ~logger ~subst metasenv context t ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv context type_t ct ugraph1 + in if not b then raise (TypeCheckerFailure - (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" - (CicPp.ppterm ct) (CicPp.ppterm t) - (CicPp.ppterm type_t)))) - else - ugraph2 + (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" + (CicPp.ppterm ct) (CicPp.ppterm t) + (CicPp.ppterm type_t)))) + else + ugraph2 | None, _ -> raise (TypeCheckerFailure - (lazy ("Not well typed metavariable local context: "^ - "an hypothesis, that is not hidden, is not instantiated"))) + (lazy ("Not well typed metavariable local context: "^ + "an hypothesis, that is not hidden, is not instantiated"))) ) ugraph l lifted_canonical_context @@ -1499,70 +1350,80 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let module R = CicReduction in let module S = CicSubstitution in let module U = UriManager in +(* FG: DEBUG ONLY + prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context); + prerr_endline ("TC: term :\n" ^ CicPp.ppterm ~metasenv t ^ "\n"); +*) match t with C.Rel n -> (try match List.nth context (n - 1) with Some (_,C.Decl t) -> S.lift n t,ugraph - | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph - | Some (_,C.Def (bo,None)) -> - debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ; - type_of_aux ~logger context (S.lift n bo) ugraph + | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph | None -> raise - (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) + (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")) ) | C.Var (uri,exp_named_subst) -> incr fdebug ; - let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph - in - let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in - let ty1 = CicSubstitution.subst_vars exp_named_subst ty in - decr fdebug ; - ty1,ugraph2 + let ugraph1 = + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + in + let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in + let ty1 = CicSubstitution.subst_vars exp_named_subst ty in + decr fdebug ; + ty1,ugraph2 | C.Meta (n,l) -> (try let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in let ugraph1 = - check_metasenv_consistency ~logger - ~subst metasenv context canonical_context l ugraph - in + check_metasenv_consistency ~logger + ~subst metasenv context canonical_context l ugraph + in (* assuming subst is well typed !!!!! *) ((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 + 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 + check_metasenv_consistency ~logger + ~subst metasenv context canonical_context l ugraph + in ((CicSubstitution.subst_meta l ty),ugraph1)) (* TASSI: CONSTRAINTS *) + | C.Sort (C.CProp t) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_gt t' t ugraph in + (C.Sort (C.Type t')),ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_gt t' t ugraph in - (C.Sort (C.Type t')),ugraph1 - (* TASSI: CONSTRAINTS *) - | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph - | C.Implicit _ -> raise (AssertFailure (lazy "21")) + (try + let ugraph1 = CicUniv.add_gt t' t ugraph in + (C.Sort (C.Type t')),ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) + | C.Sort (C.Prop|C.Set) -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph + | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Cast (te,ty) as t -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in let b,ugraph3 = - R.are_convertible ~subst ~metasenv context ty_te ty ugraph2 + R.are_convertible ~subst ~metasenv context ty_te ty ugraph2 in - if b then + if b then ty,ugraph3 - else + else raise (TypeCheckerFailure - (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t)))) + (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t)))) | C.Prod (name,s,t) -> let sort1,ugraph1 = type_of_aux ~logger context s ugraph in let sort2,ugraph2 = - type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1 + type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1 in sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2 | C.Lambda (n,s,t) -> @@ -1577,12 +1438,23 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (CicPp.ppterm sort1)))) ) ; let type2,ugraph2 = - type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 + type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 in - (C.Prod (n,s,type2)),ugraph2 - | C.LetIn (n,s,t) -> + (C.Prod (n,s,type2)),ugraph2 + | C.LetIn (n,s,ty,t) -> (* only to check if s is well-typed *) - let ty,ugraph1 = type_of_aux ~logger context s ugraph in + let ty',ugraph1 = type_of_aux ~logger context s ugraph in + let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context ty' ty ugraph1 + in + if not b then + raise + (TypeCheckerFailure + (lazy (sprintf + "The type of %s is %s but it is expected to be %s" + (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty)))) + else (* 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)) @@ -1596,60 +1468,57 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) let ty1,ugraph2 = - type_of_aux ~logger - ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1 + type_of_aux ~logger + ((Some (n,(C.Def (s,ty))))::context) t ugraph1 in (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2 | C.Appl (he::tl) when List.length tl > 0 -> let hetype,ugraph1 = type_of_aux ~logger context he ugraph in let tlbody_and_type,ugraph2 = - List.fold_right ( - fun x (l,ugraph) -> - let ty,ugraph1 = type_of_aux ~logger context x ugraph in - let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in - ((x,ty)::l,ugraph1)) - tl ([],ugraph1) + List.fold_right ( + fun x (l,ugraph) -> + let ty,ugraph1 = type_of_aux ~logger context x ugraph in + (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) + ((x,ty)::l,ugraph1)) + tl ([],ugraph1) in - (* TASSI: questa c'era nel mio... ma non nel CVS... *) - (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) - eat_prods ~subst context hetype tlbody_and_type ugraph2 + (* TASSI: questa c'era nel mio... ma non nel CVS... *) + (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) + eat_prods ~subst context hetype tlbody_and_type ugraph2 | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments")) | C.Const (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in let cty1 = - CicSubstitution.subst_vars exp_named_subst cty + CicSubstitution.subst_vars exp_named_subst cty in - decr fdebug ; - cty1,ugraph2 + decr fdebug ; + cty1,ugraph2 | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in - (* TASSI: da me c'era anche questa, ma in CVS no *) let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in - (* fine parte dubbia *) let cty = - CicSubstitution.subst_vars exp_named_subst mty + CicSubstitution.subst_vars exp_named_subst mty in - decr fdebug ; - cty,ugraph2 + decr fdebug ; + cty,ugraph2 | C.MutConstruct (uri,i,j,exp_named_subst) -> let ugraph1 = - check_exp_named_subst ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in - (* TASSI: idem come sopra *) let mty,ugraph2 = - type_of_mutual_inductive_constr ~logger uri i j ugraph1 + type_of_mutual_inductive_constr ~logger uri i j ugraph1 in let cty = - CicSubstitution.subst_vars exp_named_subst mty + CicSubstitution.subst_vars exp_named_subst mty in - cty,ugraph2 + cty,ugraph2 | C.MutCase (uri,i,outtype,term,pl) -> let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in let (need_dummy, k) = @@ -1658,100 +1527,100 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = match outtype with C.Sort _ -> (true, 0) | C.Prod (name, s, t) -> - let (b, n) = - guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd ~subst context s with + let (b, n) = + guess_args ((Some (name,(C.Decl s)))::context) t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd ~subst context s with (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> - (false, 1) + C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> + (false, 1) (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - | C.Appl ((C.MutInd (uri',i',_)) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) + | C.Appl ((C.MutInd (uri',i',_)) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - "Malformed case analasys' output type %s" - (CicPp.ppterm outtype)))) + raise + (TypeCheckerFailure + (lazy (sprintf + "Malformed case analasys' output type %s" + (CicPp.ppterm outtype)))) in (* let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux context term ugraph1 in + let ty,ugraph2 = type_of_aux context term ugraph1 in match R.whd ~subst context ty with (*CSC manca il caso dei CAST *) (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *) (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *) (*CSC: Hint: nella DTD servono per gli stylesheet. *) C.MutInd (uri',i',exp_named_subst) as typ -> - if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (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))) + if U.eq uri uri' && i = i' then + ([],[],exp_named_subst),ugraph2 + else + raise + (TypeCheckerFailure + (lazy (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))) | C.Appl - ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> - if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (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))) + ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> + if U.eq uri uri' && i = i' then + let params,args = + split tl (List.length tl - k) + in (params,args,exp_named_subst),ugraph2 + else + raise + (TypeCheckerFailure + (lazy (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))) | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysis: "^ - "analysed term %s is not an inductive one") - (CicPp.ppterm term)))) + raise + (TypeCheckerFailure + (lazy (sprintf + ("Case analysis: "^ + "analysed term %s is not an inductive one") + (CicPp.ppterm term)))) *) let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) in + if not b then (b, k - 1) else (b, k) in let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in + let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in match R.whd ~subst context ty with C.MutInd (uri',i',exp_named_subst) as typ -> if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 + ([],[],exp_named_subst),ugraph2 else raise - (TypeCheckerFailure - (lazy (sprintf - ("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))) + (TypeCheckerFailure + (lazy (sprintf + ("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) -> if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 + let params,args = + split tl (List.length tl - k) + in (params,args,exp_named_subst),ugraph2 else raise - (TypeCheckerFailure - (lazy (sprintf - ("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))) + (TypeCheckerFailure + (lazy (sprintf + ("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 - (lazy (sprintf - "Case analysis: analysed term %s is not an inductive one" + (TypeCheckerFailure + (lazy (sprintf + "Case analysis: analysed term %s is not an inductive one" (CicPp.ppterm term)))) in - (* - let's control if the sort elimination is allowed: - [(I q1 ... qr)|B] - *) + (* + let's control if the sort elimination is allowed: + [(I q1 ... qr)|B] + *) let sort_of_ind_type = if parameters = [] then C.MutInd (uri,i,exp_named_subst) @@ -1759,49 +1628,56 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in let type_of_sort_of_ind_ty,ugraph3 = - type_of_aux ~logger context sort_of_ind_type ugraph2 in + type_of_aux ~logger context sort_of_ind_type ugraph2 in let b,ugraph4 = - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 in - if not b then + if not b then raise - (TypeCheckerFailure (lazy ("Case analasys: sort elimination not allowed"))); + (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed"))); (* let's check if the type of branches are right *) - let parsno = + let parsno,constructorsno = let obj,_ = try CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri with Not_found -> assert false in match obj with - C.InductiveDefinition (_,_,parsno,_) -> parsno + C.InductiveDefinition (il,_,parsno,_) -> + let _,_,_,cl = + try List.nth il i with Failure _ -> assert false + in + parsno, List.length cl | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) - in + in + if List.length pl <> constructorsno then + raise (TypeCheckerFailure + (lazy ("Wrong number of cases in case analysis"))) ; let (_,branches_ok,ugraph5) = List.fold_left (fun (j,b,ugraph) p -> - if b then + if b then let cons = - if parameters = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl - (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) + if parameters = [] then + (C.MutConstruct (uri,i,j,exp_named_subst)) + else + (C.Appl + (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in - let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in - let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in - (* 2 is skipped *) - let ty_branch = - type_of_branch ~subst context parsno need_dummy outtype cons - ty_cons in - let b1,ugraph4 = - R.are_convertible - ~subst ~metasenv context ty_p ty_branch ugraph3 - in + let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in + let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in + (* 2 is skipped *) + let ty_branch = + type_of_branch ~subst context parsno need_dummy outtype cons + ty_cons in + let b1,ugraph4 = + R.are_convertible + ~subst ~metasenv context ty_p ty_branch ugraph3 + in (* Debugging code if not b1 then begin @@ -1811,13 +1687,13 @@ prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons); prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch); end; *) - if not b1 then - debug_print (lazy - ("#### " ^ CicPp.ppterm ty_p ^ - " <==> " ^ CicPp.ppterm ty_branch)); - (j + 1,b1,ugraph4) - else - (j,false,ugraph) + if not b1 then + debug_print (lazy + ("#### " ^ CicPp.ppterm ty_p ^ + " <==> " ^ CicPp.ppterm ty_branch)); + (j + 1,b1,ugraph4) + else + (j,false,ugraph) ) (1,true,ugraph4) pl in if not branches_ok then @@ -1832,143 +1708,188 @@ end; in outtype,ugraph5 | C.Fix (i,fl) -> - let types_times_kl,ugraph1 = - (* WAS: list rev list map *) + let types,kl,ugraph1,len = List.fold_left - (fun (l,ugraph) (n,k,ty,_) -> + (fun (types,kl,ugraph,len) (n,k,ty,_) -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in - ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1) - ) ([],ugraph) fl + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + k::kl,ugraph1,len+1) + ) ([],[],ugraph,0) fl in - let (types,kl) = List.split types_times_kl in - let len = List.length types in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (name,x,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types@context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types@context) - ty_bo (CicSubstitution.lift len ty) ugraph1 in - if b then - begin - let (m, eaten, context') = - eat_lambdas ~subst (types @ context) (x + 1) bo - in - (* - let's control the guarded by - destructors conditions D{f,k,x,M} - *) - if not (guarded_by_destructors ~subst context' eaten - (len + eaten) kl 1 [] m) then - raise - (TypeCheckerFailure - (lazy ("Fix: not guarded by destructors"))) - else - ugraph2 - end + let ty_bo,ugraph1 = + type_of_aux ~logger (types@context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types@context) + ty_bo (CicSubstitution.lift len ty) ugraph1 in + if b then + begin + let (m, eaten, context') = + eat_lambdas ~subst (types @ context) (x + 1) bo + in + let rec_uri, rec_uri_len = + let he = + match List.hd context' with + Some (_,Cic.Decl he) -> he + | _ -> assert false + in + match CicReduction.whd ~subst (List.tl context') he with + | Cic.MutInd (uri,_,_) + | Cic.Appl (Cic.MutInd (uri,_,_)::_) -> + uri, + (match + CicEnvironment.get_obj + CicUniv.oblivion_ugraph uri + with + | Cic.InductiveDefinition (tl,_,_,_), _ -> + List.length tl + | _ -> assert false) + | _ -> assert false + in + (* + let's control the guarded by + destructors conditions D{f,k,x,M} + *) + if not (guarded_by_destructors ~logger ~metasenv ~subst + rec_uri rec_uri_len context' eaten (len + eaten) kl + 1 [] m) + then + raise + (TypeCheckerFailure + (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) + else + ugraph2 + end else - raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) + raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) ) ugraph1 fl in - (*CSC: controlli mancanti solo su D{f,k,x,M} *) + (*CSC: controlli mancanti solo su D{f,k,x,M} *) let (_,_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 | C.CoFix (i,fl) -> - let types,ugraph1 = - List.fold_left - (fun (l,ugraph) (n,ty,_) -> + let types,ugraph1,len = + List.fold_left + (fun (l,ugraph,len) (n,ty,_) -> let _,ugraph1 = - type_of_aux ~logger context ty ugraph in - (Some (C.Name n,(C.Decl ty))::l,ugraph1) - ) ([],ugraph) fl + type_of_aux ~logger context ty ugraph in + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, + ugraph1,len+1) + ) ([],ugraph,0) fl in - let len = List.length types in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (_,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types @ context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types @ context) ty_bo - (CicSubstitution.lift len ty) ugraph1 - in - if b then - begin - (* let's control that the returned type is coinductive *) - match returns_a_coinductive ~subst context ty with - None -> - raise - (TypeCheckerFailure - (lazy "CoFix: does not return a coinductive type")) - | Some uri -> - (* - let's control the guarded by constructors - conditions C{f,M} - *) - if not (guarded_by_constructors ~subst - (types @ context) 0 len false bo [] uri) then - raise - (TypeCheckerFailure - (lazy "CoFix: not guarded by constructors")) - else - ugraph2 - end - else - raise - (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) + let ty_bo,ugraph1 = + type_of_aux ~logger (types @ context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types @ context) ty_bo + (CicSubstitution.lift len ty) ugraph1 + in + if b then + begin + (* let's control that the returned type is coinductive *) + match returns_a_coinductive ~subst context ty with + None -> + raise + (TypeCheckerFailure + (lazy "CoFix: does not return a coinductive type")) + | Some uri -> + (* + let's control the guarded by constructors + conditions C{f,M} + *) + if not (guarded_by_constructors ~logger ~subst ~metasenv uri + (types @ context) 0 len false bo) then + raise + (TypeCheckerFailure + (lazy "CoFix: not guarded by constructors")) + else + ugraph2 + end + else + raise + (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) ) ugraph1 fl in let (_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 - and check_exp_named_subst ~logger ~subst context ugraph = + and check_exp_named_subst uri ~logger ~subst context ens ugraph = + let params = + let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + (match obj with + Cic.Constant (_,_,_,params,_) -> params + | Cic.Variable (_,_,_,params,_) -> params + | Cic.CurrentProof (_,_,_,_,params,_) -> params + | Cic.InductiveDefinition (_,params,_,_) -> params + ) in + let rec check_same_order params ens = + match params,ens with + | _,[] -> () + | [],_::_ -> + raise (TypeCheckerFailure (lazy "Bad explicit named substitution")) + | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' -> + check_same_order tl tl' + | _::tl,l -> check_same_order tl l + in let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with - [] -> ugraph + [] -> ugraph | ((uri,t) as item)::tl -> - let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in - let typeofvar = + let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in + let typeofvar = CicSubstitution.subst_vars esubsts ty_uri in - let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in - let b,ugraph3 = + let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in + let b,ugraph3 = CicReduction.are_convertible ~subst ~metasenv - context typeoft typeofvar ugraph2 - in - if b then + context typeoft typeofvar ugraph2 + in + if b then check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3 else begin - CicReduction.fdebug := 0 ; - ignore - (CicReduction.are_convertible - ~subst ~metasenv context typeoft typeofvar ugraph2) ; - fdebug := 0 ; - debug typeoft [typeofvar] ; - raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) + CicReduction.fdebug := 0 ; + ignore + (CicReduction.are_convertible + ~subst ~metasenv context typeoft typeofvar ugraph2) ; + fdebug := 0 ; + debug typeoft [typeofvar] ; + raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in - check_exp_named_subst_aux ~logger [] ugraph + check_same_order params ens ; + check_exp_named_subst_aux ~logger [] ens ugraph and sort_of_prod ~subst context (name,s) (t1, t2) ugraph = let module C = Cic in let t1' = CicReduction.whd ~subst context t1 in let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in match (t1', t2') with - (C.Sort s1, C.Sort s2) - when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> + | (C.Sort s1, C.Sort (C.Prop | C.Set)) -> (* different from Coq manual!!! *) - C.Sort s2,ugraph - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) + t2',ugraph + | (C.Sort (C.Type t1 | C.CProp t1), C.Sort (C.Type t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.Type t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) + | (C.Sort (C.CProp t1 | C.Type t1), C.Sort (C.CProp t2)) -> let t' = CicUniv.fresh() in - let ugraph1 = CicUniv.add_ge t' t1 ugraph in - let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in - C.Sort (C.Type t'),ugraph2 - | (C.Sort _,C.Sort (C.Type t1)) -> - (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) - C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *) + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) + | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph + | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph | (C.Meta _, C.Sort _) -> t2',ugraph | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> @@ -1983,37 +1904,39 @@ end; match l with [] -> hetype,ugraph | (hete, hety)::tl -> - (match (CicReduction.whd ~subst context hetype) with + (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> - let b,ugraph1 = - CicReduction.are_convertible - ~subst ~metasenv context hety s ugraph - in - if b then - begin - CicReduction.fdebug := -1 ; - eat_prods ~subst context - (CicSubstitution.subst ~avoid_beta_redexes:true hete t) + let b,ugraph1 = +(*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then( +prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*) + CicReduction.are_convertible + ~subst ~metasenv context hety s ugraph + in + if b then + begin + CicReduction.fdebug := -1 ; + eat_prods ~subst context + (CicSubstitution.subst ~avoid_beta_redexes:true hete t) tl ugraph1 - (*TASSI: not sure *) - end - else - begin - CicReduction.fdebug := 0 ; - ignore (CicReduction.are_convertible - ~subst ~metasenv context s hety ugraph) ; - fdebug := 0 ; - debug s [hety] ; - raise - (TypeCheckerFailure - (lazy (sprintf - ("Appl: wrong parameter-type, expected %s, found %s") - (CicPp.ppterm hetype) (CicPp.ppterm s)))) - end - | _ -> - raise (TypeCheckerFailure - (lazy "Appl: this is not a function, it cannot be applied")) - ) + (*TASSI: not sure *) + end + else + begin + CicReduction.fdebug := 0 ; + ignore (CicReduction.are_convertible + ~subst ~metasenv context s hety ugraph) ; + fdebug := 0 ; + debug s [hety] ; + raise + (TypeCheckerFailure + (lazy (sprintf + ("Appl: wrong parameter-type, expected %s, found %s") + (CicPp.ppterm hetype) (CicPp.ppterm s)))) + end + | _ -> + raise (TypeCheckerFailure + (lazy "Appl: this is not a function, it cannot be applied")) + ) and returns_a_coinductive ~subst context ty = let module C = Cic in @@ -2036,7 +1959,7 @@ end; ) | C.Appl ((C.MutInd (uri,i,_))::_) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) @@ -2072,7 +1995,7 @@ and is_small_or_non_informative ~condition ~logger context paramsno c ugraph = is_small_or_non_informative_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1 else - false,ugraph1 + false,ugraph1 | _ -> true,ugraph (*CSC: we trust the type-checker *) in let (context',dx) = split_prods ~subst:[] context paramsno c in @@ -2099,100 +2022,92 @@ in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res *) ;; -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,_,_) -> - 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 typecheck ?(trust=true) 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 -> + match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with + | 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 CicUniv.empty_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 *) @@ -2220,3 +2135,20 @@ let check_allowed_sort_elimination uri i s1 s2 = ~logger:(new CicLogger.logger) [] uri i true (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2) CicUniv.empty_ugraph) +;; + +Deannotate.type_of_aux' := + fun context t -> + ignore ( + List.fold_right + (fun el context -> + (match el with + None -> () + | Some (_,Cic.Decl ty) -> + ignore (type_of_aux' [] context ty CicUniv.empty_ugraph) + | Some (_,Cic.Def (bo,ty)) -> + ignore (type_of_aux' [] context ty CicUniv.empty_ugraph); + ignore (type_of_aux' [] context bo CicUniv.empty_ugraph)); + el::context + ) context []); + fst (type_of_aux' [] context t CicUniv.empty_ugraph);;