X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=35015e541202d36fe82a245ddd167e7322fc2c1c;hb=ebb2f4bda5f7c5c7fc26d3aa1e17312f8900da4a;hp=ffb53c236a3f4faefd8ce1ddb72d1f6c8f528e82;hpb=9f66cc89caf70d20a0e4c0d55796da6082d60976;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index ffb53c236..35015e541 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 = @@ -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 @@ -264,14 +269,15 @@ and does_not_occur ?(subst=[]) context n nn te = 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,ty,dest) -> does_not_occur ~subst context n nn so && @@ -279,16 +285,17 @@ and does_not_occur ?(subst=[]) context n nn te = 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 @@ -557,7 +564,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = let ugraph'' = List.fold_left (fun ugraph (name,te) -> - let debrujinedte = debrujin_constructor uri len te in + 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)) @@ -595,65 +602,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,_,_,_) -> @@ -666,58 +663,45 @@ 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 @@ -741,158 +725,91 @@ 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,ty,ta) -> - check_is_really_smaller_arg ~subst context n nn kl x safes so && - check_is_really_smaller_arg ~subst context n nn kl x safes ty && - check_is_really_smaller_arg ~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 (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 - (lefts@tys,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 - (lefts@tys,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 @@ -906,41 +823,30 @@ and check_is_really_smaller_arg ~subst context n nn kl x safes te = 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 - 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.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 t = +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 - match CicReduction.whd ~subst context t with + 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 (m-1) with Some (_,C.Decl _) -> true | Some (_,C.Def (bo,_)) -> - guarded_by_destructors ~subst context n 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")) ) @@ -948,162 +854,84 @@ and guarded_by_destructors ~subst context n nn kl x safes t = | 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) + 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 ~subst context n nn kl x safes so && - guarded_by_destructors ~subst context n nn kl x safes ty && - guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::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 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) + 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 - (lefts@tys,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 -> - 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 - 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 - (lefts@tys,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.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t-> @@ -1120,29 +948,30 @@ and guarded_by_destructors ~subst context n nn kl x safes t = ) ([],0) fl in let safes' = List.map (fun x -> x + len) safes in List.for_all - (guarded_by_destructors ~subst context n nn kl x safes) l && + (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 ~subst context n nn kl x_plus_len safes' ty && + 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 ~subst context n nn kl x safes - (List.nth l recno) + 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 ~subst context (n_plus_len+recno+1) + 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 ~subst (tys@context) n_plus_len nn_plus_len + 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) -> @@ -1160,236 +989,132 @@ and guarded_by_destructors ~subst context n nn kl x safes t = 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 ~subst context n nn kl x safes t) + (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 *) - 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 *) + let rec_params = + let c = + debrujin_constructor ~check_exp_named_subst:false + indURI len_tys context consty 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.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 -> - 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.fold_left (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) 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 + 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.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl + 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 -> - 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 + 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 = @@ -1960,12 +1685,33 @@ 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:"^CicPp.ppterm t))) @@ -2011,8 +1757,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")) @@ -2208,103 +1954,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,_,_) -> - (* 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 + 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 *) @@ -2336,21 +2071,16 @@ let check_allowed_sort_elimination uri i s1 s2 = Deannotate.type_of_aux' := fun context t -> - (*CSC: we need to type-check the context to avoid Not_found in - get_cooked_obj in CicReduction. However, this implementation may - be very inefficient, since we may type-check the same context - O(n^2) times. On the other hand, type-checking the context in Deannotate - would be a cost to pay not only for Coq objects. *) ignore ( List.fold_right (fun el context -> (match el with None -> () | Some (_,Cic.Decl ty) -> - ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph) + ignore (type_of_aux' [] context ty CicUniv.empty_ugraph) | Some (_,Cic.Def (bo,ty)) -> - ignore (type_of_aux' [] context ty CicUniv.oblivion_ugraph); - ignore (type_of_aux' [] context bo CicUniv.oblivion_ugraph)); + 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.oblivion_ugraph);; + fst (type_of_aux' [] context t CicUniv.empty_ugraph);;