X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=6cbb44f8044432db90ae2cd361d2831cb132be8d;hb=d025518bc5930796c748704b069a2719b34b00d3;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..6cbb44f80 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,68 @@ 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 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 + let _,ugraph = + type_of_aux' ~logger metasenv context ty ugraph in - (metasenv @ [conj],ugraph') - ) ([],ugraph) conjs + (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 +205,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'') + 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 +257,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 +316,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 -> @@ -338,6 +354,10 @@ and weakly_positive context n nn uri te = | C.Lambda (name,so,ta) -> C.Lambda (name, subst_inductive_type_with_dummy_mutind so, subst_inductive_type_with_dummy_mutind ta) + | C.LetIn (name,so,ty,ta) -> + C.LetIn (name, subst_inductive_type_with_dummy_mutind so, + subst_inductive_type_with_dummy_mutind ty, + subst_inductive_type_with_dummy_mutind ta) | C.Appl tl -> C.Appl (List.map subst_inductive_type_with_dummy_mutind tl) | C.MutCase (uri,i,outtype,term,pl) -> @@ -360,6 +380,13 @@ and weakly_positive context n nn uri te = 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_mutind t)) + exp_named_subst + in + C.Var (uri,exp_named_subst') | C.MutInd (uri,typeno,exp_named_subst) -> let exp_named_subst' = List.map @@ -382,13 +409,8 @@ and weakly_positive context n nn uri te = *) 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 -> + 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 (subst_inductive_type_with_dummy_mutind source) && @@ -428,7 +450,9 @@ and strictly_positive context n nn te = strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> 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 @@ -454,7 +478,6 @@ 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 && @@ -499,14 +522,8 @@ 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 && are_all_occurrences_positive @@ -540,25 +557,35 @@ 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) -> + (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) -> + CicUniv.add_ge u2 u1 ugraph + | Cic.Sort _, Cic.Sort Cic.Prop + | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp + | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph + | _, _ -> + raise + (TypeCheckerFailure + (lazy ("Wrong constructor or inductive arity shape"))) in (* let's check also the positivity conditions *) if not - (are_all_occurrences_positive tys uri indparamsno i 0 len - debrujinedte) + (are_all_occurrences_positive context uri indparamsno + (i+indparamsno) indparamsno (len+indparamsno) te) then begin prerr_endline (UriManager.string_of_uri uri); @@ -567,7 +594,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (TypeCheckerFailure (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end else - ugraph' + ugraph ) ugraph cl in (i + 1),ugraph'' ) itl (1,ugrap1) @@ -585,65 +612,55 @@ and check_mutual_inductive_defs uri obj ugraph = 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 -> + | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> logger#log (`Start_type_checking uri) ; - let ugraph1_dust = - check_mutual_inductive_defs ~logger uri uobj ugraph - in - (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *) - try - CicEnvironment.set_type_checking_info uri ; - logger#log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked ~trust:false ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') - | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError - ) - with - Invalid_argument s -> - (*debug_print (lazy s);*) - uobj,ugraph1_dust + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj 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))) + 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 = +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 + 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 ugraph1_dust = - check_mutual_inductive_defs ~logger uri uobj ugraph + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph in - (* check ugraph1 validity ??? == ugraph' *) - try - CicEnvironment.set_type_checking_info uri ; - logger#log (`Type_checking_completed uri) ; - (match - CicEnvironment.is_type_checked ~trust:false ugraph uri - with + let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in + CicEnvironment.set_type_checking_info uri (obj, ugraph, ul); + logger#log (`Type_checking_completed uri) ; + (match + CicEnvironment.is_type_checked ~trust:false orig_ugraph uri + with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError) - with - Invalid_argument s -> - (*debug_print (lazy s);*) - uobj,ugraph1_dust in match cobj with C.InductiveDefinition (dl,_,_,_) -> @@ -656,65 +673,53 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = 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 +736,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 +865,267 @@ 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 *) - 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 *) + let rec_params = + let c = + debrujin_constructor ~check_exp_named_subst:false + indURI len_tys context consty 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 check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy ind arity1 arity2 ugraph = @@ -1325,11 +1134,12 @@ 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 @@ -1445,11 +1255,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,8 +1266,25 @@ and check_metasenv_consistency ~logger ~subst metasenv context match (t,ct) with | _,None -> ugraph | Some t,Some (_,C.Def (ct,_)) -> + (*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 t ct ugraph + R.are_convertible ~subst ~metasenv context optimized_t ct ugraph in if not b then raise @@ -1504,10 +1329,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (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")) with @@ -1517,7 +1339,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Var (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 ty,ugraph2 = type_of_variable ~logger uri ugraph1 in let ty1 = CicSubstitution.subst_vars exp_named_subst ty in @@ -1543,11 +1365,13 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* TASSI: CONSTRAINTS *) | 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 *) + (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 s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph - | C.Implicit _ -> raise (AssertFailure (lazy "21")) + | 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 @@ -1580,9 +1404,20 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = 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.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)) @@ -1597,7 +1432,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = 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 + ((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 -> @@ -1606,7 +1441,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = 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 + (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) ((x,ty)::l,ugraph1)) tl ([],ugraph1) in @@ -1617,7 +1452,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | 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 = @@ -1628,11 +1463,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | 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 in @@ -1640,9 +1473,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = 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 in @@ -1766,21 +1598,28 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in 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 -> @@ -1832,16 +1671,14 @@ 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 (fun ugraph (name,x,ty,bo) -> @@ -1856,15 +1693,36 @@ end; 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 ~subst context' eaten - (len + eaten) kl 1 [] m) then + 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"))) + (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) else ugraph2 end @@ -1875,15 +1733,15 @@ end; let (_,_,ty,_) = List.nth fl i in ty,ugraph2 | C.CoFix (i,fl) -> - let types,ugraph1 = + let types,ugraph1,len = List.fold_left - (fun (l,ugraph) (n,ty,_) -> + (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 + (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 (fun ugraph (_,ty,bo) -> @@ -1907,8 +1765,8 @@ end; 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 + if not (guarded_by_constructors ~logger ~subst ~metasenv uri + (types @ context) 0 len false bo) then raise (TypeCheckerFailure (lazy "CoFix: not guarded by constructors")) @@ -1923,7 +1781,24 @@ end; let (_,ty,_) = List.nth fl i in 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 @@ -1949,7 +1824,8 @@ end; 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 @@ -1963,9 +1839,12 @@ end; | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) 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 + (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.Sort (C.Type t1)) -> (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *) @@ -1986,6 +1865,8 @@ end; (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,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 @@ -2099,100 +1980,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 module C = Cic in let module R = CicReduction in let module U = UriManager in let logger = new CicLogger.logger in - (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *) match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> - (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*) - cobj,ugraph' - | CicEnvironment.UncheckedObj uobj -> + | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> (* let's typecheck the uncooked object *) logger#log (`Start_type_checking uri) ; - (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *) - let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in - try - CicEnvironment.set_type_checking_info uri; - logger#log (`Type_checking_completed uri); - match CicEnvironment.is_type_checked ~trust:false ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' - | _ -> raise CicEnvironmentError - with - (* - this is raised if set_type_checking_info is called on an object - that has no associated universe file. If we are in univ_maker - phase this is OK since univ_maker will properly commit the - object. - *) - Invalid_argument s -> - (*debug_print (lazy s);*) - uobj,ugraph + let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in + CicEnvironment.set_type_checking_info uri (obj,ugraph,ul); + logger#log (`Type_checking_completed uri); + match CicEnvironment.is_type_checked ~trust:false 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 +2093,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);;