X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=c38c15b931cdea943fda830e4097790503ef5501;hb=1b70a1f66be53f76e475383e86d63c2b5c1fbcaa;hp=4dfe783012ed0fffe914037d30f8048c465b0f26;hpb=2b10614120e86ec755f4826c6e78a654434bc7f8;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 4dfe78301..c38c15b93 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -141,6 +141,27 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri n exception CicEnvironmentError;; +let check_homogeneous_call context indparamsno n uri reduct tl = + let last = + List.fold_left + (fun k x -> + if k = 0 then 0 + else + match CicReduction.whd context x with + | Cic.Rel m when m = n - (indparamsno - k) -> k - 1 + | _ -> raise (TypeCheckerFailure (lazy + ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^ + string_of_int indparamsno ^ " fixed) is not homogeneous in "^ + "appl:\n"^ CicPp.ppterm reduct)))) + indparamsno tl + in + if last <> 0 then + raise (TypeCheckerFailure + (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ + UriManager.string_of_uri uri))) +;; + + let rec type_of_constant ~logger uri orig_ugraph = let module C = Cic in let module R = CicReduction in @@ -173,8 +194,8 @@ let rec type_of_constant ~logger uri orig_ugraph = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> let _,ugraph = - type_of_aux' ~logger metasenv context ty ugraph - in + type_of_aux' ~logger metasenv context ty ugraph + in (metasenv @ [conj],ugraph) ) ([],CicUniv.empty_ugraph) conjs in @@ -222,13 +243,13 @@ and type_of_variable ~logger uri orig_ugraph = match bo with None -> ugraph | Some bo -> - let ty_bo,ugraph = type_of ~logger bo ugraph in + let ty_bo,ugraph = type_of ~logger bo ugraph in let b,ugraph = R.are_convertible [] ty_bo ty ugraph in if not b then raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri))) - else - ugraph + else + ugraph in let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj @@ -240,7 +261,7 @@ and type_of_variable ~logger uri orig_ugraph = | CicEnvironment.CheckedObj _ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError) | _ -> - raise (TypeCheckerFailure (lazy + raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri))) and does_not_occur ?(subst=[]) context n nn te = @@ -305,7 +326,7 @@ and does_not_occur ?(subst=[]) context n nn te = (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 -> @@ -321,7 +342,7 @@ and does_not_occur ?(subst=[]) context n nn te = (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 -> @@ -329,100 +350,104 @@ and does_not_occur ?(subst=[]) context n nn te = does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo ) fl true -(*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *) -(*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *) -(*CSC dei controlli leggermente diversi. Viene invocata solamente dalla *) -(*CSC strictly_positive *) -(*CSC definizione (giusta???) tratta dalla mail di Hugo ;-) *) -and weakly_positive context n nn uri te = +(* Inductive types being checked for positivity have *) +(* indexes x s.t. n < x <= nn. *) +and weakly_positive context n nn uri indparamsno posuri te = let module C = Cic in -(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) - let dummy_mutind = - C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[]) + (*CSC: Not very nice. *) + let leftno = + match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with + | Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno + | _ -> assert false in - (*CSC: mettere in cicSubstitution *) - let rec subst_inductive_type_with_dummy_mutind = + let dummy = Cic.Sort Cic.Prop in + (*CSC: to be moved in cicSubstitution? *) + let rec subst_inductive_type_with_dummy = function C.MutInd (uri',0,_) when UriManager.eq uri' uri -> - dummy_mutind + dummy | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> - dummy_mutind - | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te + let _, rargs = HExtlib.split_nth leftno tl in + if rargs = [] then dummy else Cic.Appl (dummy :: rargs) + | C.Cast (te,ty) -> subst_inductive_type_with_dummy te | C.Prod (name,so,ta) -> - C.Prod (name, subst_inductive_type_with_dummy_mutind so, - subst_inductive_type_with_dummy_mutind ta) + C.Prod (name, subst_inductive_type_with_dummy so, + subst_inductive_type_with_dummy ta) | C.Lambda (name,so,ta) -> - C.Lambda (name, subst_inductive_type_with_dummy_mutind so, - subst_inductive_type_with_dummy_mutind ta) + C.Lambda (name, subst_inductive_type_with_dummy so, + subst_inductive_type_with_dummy ta) | C.LetIn (name,so,ty,ta) -> - C.LetIn (name, subst_inductive_type_with_dummy_mutind so, - subst_inductive_type_with_dummy_mutind ty, - subst_inductive_type_with_dummy_mutind ta) + C.LetIn (name, subst_inductive_type_with_dummy so, + subst_inductive_type_with_dummy ty, + subst_inductive_type_with_dummy ta) | C.Appl tl -> - C.Appl (List.map subst_inductive_type_with_dummy_mutind tl) + C.Appl (List.map subst_inductive_type_with_dummy tl) | C.MutCase (uri,i,outtype,term,pl) -> C.MutCase (uri,i, - subst_inductive_type_with_dummy_mutind outtype, - subst_inductive_type_with_dummy_mutind term, - List.map subst_inductive_type_with_dummy_mutind pl) + subst_inductive_type_with_dummy outtype, + subst_inductive_type_with_dummy term, + List.map subst_inductive_type_with_dummy pl) | C.Fix (i,fl) -> C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i, - subst_inductive_type_with_dummy_mutind ty, - subst_inductive_type_with_dummy_mutind bo)) fl) + subst_inductive_type_with_dummy ty, + subst_inductive_type_with_dummy bo)) fl) | C.CoFix (i,fl) -> C.CoFix (i,List.map (fun (name,ty,bo) -> (name, - subst_inductive_type_with_dummy_mutind ty, - subst_inductive_type_with_dummy_mutind bo)) fl) + subst_inductive_type_with_dummy ty, + subst_inductive_type_with_dummy bo)) fl) | C.Const (uri,exp_named_subst) -> let exp_named_subst' = List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) exp_named_subst in C.Const (uri,exp_named_subst') | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) exp_named_subst in C.Var (uri,exp_named_subst') | C.MutInd (uri,typeno,exp_named_subst) -> let exp_named_subst' = List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) exp_named_subst in C.MutInd (uri,typeno,exp_named_subst') | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> let exp_named_subst' = List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) + (function (uri,t) -> (uri,subst_inductive_type_with_dummy t)) exp_named_subst in C.MutConstruct (uri,typeno,consno,exp_named_subst') | t -> t in - match CicReduction.whd context te with -(* - C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true -*) - C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true - | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true - | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> - (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive context n nn - (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (name,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest - | C.Prod (name,source,dest) -> - does_not_occur context n nn - (subst_inductive_type_with_dummy_mutind source)&& - weakly_positive ((Some (name,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest - | _ -> - raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) + (* this function has the same semantics of are_all_occurrences_positive + but the i-th context entry role is played by dummy and some checks + are skipped because we already know that are_all_occurrences_positive + of uri in te. *) + let rec aux context n nn te = + match CicReduction.whd context te with + | C.Appl (C.Sort C.Prop::tl) -> + List.for_all (does_not_occur context n nn) tl + | C.Sort C.Prop -> true + | C.Prod (name,source,dest) when + does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> + (* dummy abstraction, so we behave as in the anonimous case *) + strictly_positive context n nn indparamsno posuri source && + aux ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) dest + | C.Prod (name,source,dest) -> + does_not_occur context n nn source && + aux ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) dest + | _ -> + raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) + in + aux context n nn (subst_inductive_type_with_dummy te) (* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) @@ -436,34 +461,36 @@ and instantiate_parameters params c = | (C.Cast (te,_), _) -> instantiate_parameters params te | (t,l) -> raise (AssertFailure (lazy "1")) -and strictly_positive context n nn te = +and strictly_positive context n nn indparamsno posuri te = let module C = Cic in let module U = UriManager in match CicReduction.whd context te with | t when does_not_occur context n nn t -> true - | C.Rel _ -> true + | C.Rel _ when indparamsno = 0 -> true | C.Cast (te,ty) -> (*CSC: bisogna controllare ty????*) - strictly_positive context n nn te + strictly_positive context n nn indparamsno posuri te | C.Prod (name,so,ta) -> does_not_occur context n nn so && - strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta - | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> + strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) + indparamsno posuri ta + | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn -> + check_homogeneous_call context indparamsno n posuri reduct tl; List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_) | (C.MutInd (uri,i,exp_named_subst)) as t -> let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in let (ok,paramsno,ity,cl,name) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with C.InductiveDefinition (tl,_,paramsno,_) -> - let (name,_,ity,cl) = List.nth tl i in + let (name,_,ity,cl) = List.nth tl i in (List.length tl = 1, paramsno, ity, cl, name) (* (true, paramsno, ity, cl, name) *) | _ -> - raise - (TypeCheckerFailure - (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) + raise + (TypeCheckerFailure + (lazy ("Unknown inductive type:" ^ U.string_of_uri uri))) in let (params,arguments) = split tl paramsno in let lifted_params = List.map (CicSubstitution.lift 1) params in @@ -482,8 +509,8 @@ and strictly_positive context n nn te = (fun x i -> i && weakly_positive - ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri - x + ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri + indparamsno posuri x ) cl' true | t -> false @@ -491,30 +518,9 @@ and strictly_positive context n nn te = and are_all_occurrences_positive context uri indparamsno i n nn te = let module C = Cic in match CicReduction.whd context te with - C.Appl ((C.Rel m)::tl) when m = i -> - (*CSC: riscrivere fermandosi a 0 *) - (* let's check if the inductive type is applied at least to *) - (* indparamsno parameters *) - let last = - List.fold_left - (fun k x -> - if k = 0 then 0 - else - match CicReduction.whd context x with - C.Rel m when m = n - (indparamsno - k) -> k - 1 - | _ -> - raise (TypeCheckerFailure - (lazy - ("Non-positive occurence in mutual inductive definition(s) [1]" ^ - UriManager.string_of_uri uri))) - ) indparamsno tl - in - if last = 0 then - List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true - else - raise (TypeCheckerFailure - (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ - UriManager.string_of_uri uri))) + C.Appl ((C.Rel m)::tl) as reduct when m = i -> + check_homogeneous_call context indparamsno n uri reduct tl; + List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Rel m when m = i -> if indparamsno = 0 then true @@ -525,7 +531,7 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = | C.Prod (name,source,dest) when does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest -> (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive context n nn source && + strictly_positive context n nn indparamsno uri source && are_all_occurrences_positive ((Some (name,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest @@ -562,7 +568,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = List.fold_right (fun (_,_,ty,cl) (i,ugraph) -> let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in - let ugraph'' = + let ugraph'' = List.fold_left (fun ugraph (name,te) -> let te = debrujin_constructor uri len [] te in @@ -572,11 +578,14 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = match CicReduction.whd context con_sort, CicReduction.whd [] ty_sort with - Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) -> + Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2) + | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2) + | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2) + | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) -> CicUniv.add_ge u2 u1 ugraph | Cic.Sort _, Cic.Sort Cic.Prop + | Cic.Sort _, Cic.Sort Cic.CProp _ | Cic.Sort _, Cic.Sort Cic.Set - | Cic.Sort Cic.CProp, Cic.Sort Cic.CProp | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph | a,b -> raise @@ -585,20 +594,17 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) in (* let's check also the positivity conditions *) if - not - (are_all_occurrences_positive context uri indparamsno + not + (are_all_occurrences_positive context uri indparamsno (i+indparamsno) indparamsno (len+indparamsno) te) then - begin - prerr_endline (UriManager.string_of_uri uri); - prerr_endline (string_of_int (List.length tys)); - raise - (TypeCheckerFailure - (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end + raise + (TypeCheckerFailure + (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) else - ugraph + ugraph ) ugraph cl in - (i + 1),ugraph'' + (i + 1),ugraph'' ) itl (1,ugrap1) in ugraph2 @@ -608,11 +614,11 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = and check_mutual_inductive_defs uri obj ugraph = match obj with Cic.InductiveDefinition (itl, params, indparamsno, _) -> - typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph + typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph | _ -> - raise (TypeCheckerFailure ( - lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + raise (TypeCheckerFailure ( + lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = let module C = Cic in @@ -622,17 +628,17 @@ and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> - logger#log (`Start_type_checking uri) ; - let inferred_ugraph = + logger#log (`Start_type_checking uri) ; + let inferred_ugraph = check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph in let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in - CicEnvironment.set_type_checking_info uri (obj,ugraph,ul); - logger#log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph') - | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError - ) + 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,_,_,_) -> @@ -641,36 +647,36 @@ and type_of_mutual_inductive_defs ~logger uri i orig_ugraph = | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri))) - + and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph = let module C = Cic in let module R = CicReduction in let module U = UriManager in let cobj,ugraph1 = match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with - CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> - logger#log (`Start_type_checking uri) ; - let inferred_ugraph = - check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph - in + logger#log (`Start_type_checking uri) ; + let inferred_ugraph = + check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph + in let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in - CicEnvironment.set_type_checking_info uri (obj, ugraph, ul); - logger#log (`Type_checking_completed uri) ; - (match + CicEnvironment.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) + CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' + | CicEnvironment.UncheckedObj _ -> + raise CicEnvironmentError) in match cobj with - C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cl) = List.nth dl i in + C.InductiveDefinition (dl,_,_,_) -> + let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,ugraph1 | _ -> - raise (TypeCheckerFailure + raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) and recursive_args context n nn te = @@ -834,7 +840,7 @@ and check_is_really_smaller_arg (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.for_all (fun (_,_,_,bo) -> @@ -958,7 +964,7 @@ and guarded_by_destructors (fun (types,len) (n,_,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl in + ) ([],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 && @@ -997,7 +1003,7 @@ and guarded_by_destructors (fun (types,len) (n,ty,_) -> (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1) - ) ([],0) fl + ) ([],0) fl and safes' = List.map (fun x -> x + len) safes in List.fold_right (fun (_,ty,bo) i -> @@ -1129,6 +1135,21 @@ and guarded_by_constructors ~logger ~subst ~metasenv indURI = in aux +and is_non_recursive ctx paramsno t uri = + let t = debrujin_constructor uri 1 [] t in +(* let ctx, t = split_prods ~subst:[] ctx paramsno t in *) + let len = List.length ctx in + let rec aux ctx n nn t = + match CicReduction.whd ctx t with + | Cic.Prod (name,src,tgt) -> + does_not_occur ctx n nn src && + aux (Some (name,Cic.Decl src) :: ctx) (n+1) (nn+1) tgt + | (Cic.Rel k) + | Cic.Appl (Cic.Rel k :: _) when k = nn -> true + | t -> assert false + in + aux ctx (len-1) len t + and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy ind arity1 arity2 ugraph = let module C = Cic in @@ -1140,26 +1161,26 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in if b then - check_allowed_sort_elimination ~subst ~metasenv ~logger + check_allowed_sort_elimination ~subst ~metasenv ~logger ((Some (name,C.Decl so1))::context) uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1 else - false,ugraph1 + false,ugraph1 | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy -> let b,ugraph1 = CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in if not b then - false,ugraph1 + false,ugraph1 else check_allowed_sort_elimination_aux ugraph1 ((Some (name,C.Decl so))::context) ta true | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph | (C.Sort C.Prop, C.Sort C.Set) - | (C.Sort C.Prop, C.Sort C.CProp) + | (C.Sort C.Prop, C.Sort (C.CProp _)) | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,paramsno,_) -> let itl_len = List.length itl in let (name,_,ty,cl) = List.nth itl i in @@ -1168,8 +1189,13 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let non_informative,ugraph = if cl_len = 0 then true,ugraph else - is_non_informative ~logger [Some (C.Name name,C.Decl ty)] - paramsno (snd (List.nth cl 0)) ugraph + let b, ug = + is_non_informative ~logger [Some (C.Name name,C.Decl ty)] + paramsno (snd (List.nth cl 0)) ugraph + in + b && + is_non_recursive [Some (C.Name name,C.Decl ty)] + paramsno (snd (List.nth cl 0)) uri, ug in (* is it a singleton or empty non recursive and non informative definition? *) @@ -1178,19 +1204,16 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i false,ugraph | _ -> raise (TypeCheckerFailure - (lazy ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri))) + (lazy ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) ) | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph - | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph - | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _))) + | (C.Sort C.Set, C.Sort (C.Type _)) + | (C.Sort C.Set, C.Sort (C.CProp _)) when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,paramsno,_) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl @@ -1198,21 +1221,22 @@ and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i let (_,_,_,cl) = List.nth itl i in (List.fold_right (fun (_,x) (i,ugraph) -> - if i then - is_small ~logger tys paramsno x ugraph - else - false,ugraph - ) cl (true,ugraph)) + if i then + is_small ~logger tys paramsno x ugraph + else + false,ugraph + ) cl (true,ugraph)) | _ -> raise (TypeCheckerFailure (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri))) ) | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph + | (C.Sort (C.CProp _), C.Sort _) when need_dummy -> true , ugraph | (_,_) -> false,ugraph in check_allowed_sort_elimination_aux ugraph context arity2 need_dummy - + and type_of_branch ~subst context argsno need_dummy outtype term constype = let module C = Cic in let module R = CicReduction in @@ -1285,33 +1309,33 @@ and check_metasenv_consistency ~logger ~subst metasenv context in (*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!" else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*) - let b,ugraph1 = - R.are_convertible ~subst ~metasenv context optimized_t ct ugraph - in - if not b then - raise - (TypeCheckerFailure - (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))) - else - ugraph1 + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context optimized_t ct ugraph + in + if not b then + raise + (TypeCheckerFailure + (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))) + else + ugraph1 | Some t,Some (_,C.Decl ct) -> let type_t,ugraph1 = - type_of_aux' ~logger ~subst metasenv context t ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv context type_t ct ugraph1 - in + type_of_aux' ~logger ~subst metasenv context t ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv context type_t ct ugraph1 + in if not b then raise (TypeCheckerFailure - (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" - (CicPp.ppterm ct) (CicPp.ppterm t) - (CicPp.ppterm type_t)))) - else - ugraph2 + (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s" + (CicPp.ppterm ct) (CicPp.ppterm t) + (CicPp.ppterm type_t)))) + else + ugraph2 | None, _ -> raise (TypeCheckerFailure - (lazy ("Not well typed metavariable local context: "^ - "an hypothesis, that is not hidden, is not instantiated"))) + (lazy ("Not well typed metavariable local context: "^ + "an hypothesis, that is not hidden, is not instantiated"))) ) ugraph l lifted_canonical_context @@ -1326,6 +1350,10 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let module R = CicReduction in let module S = CicSubstitution in let module U = UriManager in +(* FG: DEBUG ONLY + prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context); + prerr_endline ("TC: term :\n" ^ CicPp.ppterm ~metasenv t ^ "\n"); +*) match t with C.Rel n -> (try @@ -1333,38 +1361,45 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = Some (_,C.Decl t) -> S.lift n t,ugraph | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph | None -> raise - (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) + (TypeCheckerFailure (lazy "Reference to deleted hypothesis")) with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")) ) | C.Var (uri,exp_named_subst) -> incr fdebug ; - let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph - in - let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in - let ty1 = CicSubstitution.subst_vars exp_named_subst ty in - decr fdebug ; - ty1,ugraph2 + let ugraph1 = + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + in + let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in + let ty1 = CicSubstitution.subst_vars exp_named_subst ty in + decr fdebug ; + ty1,ugraph2 | C.Meta (n,l) -> (try let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in let ugraph1 = - check_metasenv_consistency ~logger - ~subst metasenv context canonical_context l ugraph - in + check_metasenv_consistency ~logger + ~subst metasenv context canonical_context l ugraph + in (* assuming subst is well typed !!!!! *) ((CicSubstitution.subst_meta l ty), ugraph1) (* type_of_aux context (CicSubstitution.subst_meta l term) *) - with CicUtil.Subst_not_found _ -> - let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in + with CicUtil.Subst_not_found _ -> + let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let ugraph1 = - check_metasenv_consistency ~logger - ~subst metasenv context canonical_context l ugraph - in + check_metasenv_consistency ~logger + ~subst metasenv context canonical_context l ugraph + in ((CicSubstitution.subst_meta l ty),ugraph1)) (* TASSI: CONSTRAINTS *) + | C.Sort (C.CProp t) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_gt t' t ugraph in + (C.Sort (C.Type t')),ugraph1 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in (try @@ -1372,23 +1407,23 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (C.Sort (C.Type t')),ugraph1 with CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) - | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph + | C.Sort (C.Prop|C.Set) -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found")) | C.Cast (te,ty) as t -> let _,ugraph1 = type_of_aux ~logger context ty ugraph in let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in let b,ugraph3 = - R.are_convertible ~subst ~metasenv context ty_te ty ugraph2 + R.are_convertible ~subst ~metasenv context ty_te ty ugraph2 in - if b then + if b then ty,ugraph3 - else + else raise (TypeCheckerFailure - (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t)))) + (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t)))) | C.Prod (name,s,t) -> let sort1,ugraph1 = type_of_aux ~logger context s ugraph in let sort2,ugraph2 = - type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1 + type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t ugraph1 in sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2 | C.Lambda (n,s,t) -> @@ -1403,15 +1438,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (CicPp.ppterm sort1)))) ) ; let type2,ugraph2 = - type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 + type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1 in - (C.Prod (n,s,type2)),ugraph2 + (C.Prod (n,s,type2)),ugraph2 | C.LetIn (n,s,ty,t) -> (* only to check if s is well-typed *) let ty',ugraph1 = type_of_aux ~logger context s ugraph in let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in let b,ugraph1 = - R.are_convertible ~subst ~metasenv context ty ty' ugraph1 + R.are_convertible ~subst ~metasenv context ty' ty ugraph1 in if not b then raise @@ -1433,57 +1468,57 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) let ty1,ugraph2 = - type_of_aux ~logger - ((Some (n,(C.Def (s,ty))))::context) t ugraph1 + type_of_aux ~logger + ((Some (n,(C.Def (s,ty))))::context) t ugraph1 in (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2 | C.Appl (he::tl) when List.length tl > 0 -> let hetype,ugraph1 = type_of_aux ~logger context he ugraph in let tlbody_and_type,ugraph2 = - List.fold_right ( - fun x (l,ugraph) -> - let ty,ugraph1 = type_of_aux ~logger context x ugraph in - (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) - ((x,ty)::l,ugraph1)) - tl ([],ugraph1) + List.fold_right ( + fun x (l,ugraph) -> + let ty,ugraph1 = type_of_aux ~logger context x ugraph in + (*let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in*) + ((x,ty)::l,ugraph1)) + tl ([],ugraph1) in - (* TASSI: questa c'era nel mio... ma non nel CVS... *) - (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) - eat_prods ~subst context hetype tlbody_and_type ugraph2 + (* TASSI: questa c'era nel mio... ma non nel CVS... *) + (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *) + eat_prods ~subst context hetype tlbody_and_type ugraph2 | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments")) | C.Const (uri,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in let cty1 = - CicSubstitution.subst_vars exp_named_subst cty + CicSubstitution.subst_vars exp_named_subst cty in - decr fdebug ; - cty1,ugraph2 + decr fdebug ; + cty1,ugraph2 | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in let cty = - CicSubstitution.subst_vars exp_named_subst mty + CicSubstitution.subst_vars exp_named_subst mty in - decr fdebug ; - cty,ugraph2 + decr fdebug ; + cty,ugraph2 | C.MutConstruct (uri,i,j,exp_named_subst) -> let ugraph1 = - check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph + check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph in let mty,ugraph2 = - type_of_mutual_inductive_constr ~logger uri i j ugraph1 + type_of_mutual_inductive_constr ~logger uri i j ugraph1 in let cty = - CicSubstitution.subst_vars exp_named_subst mty + CicSubstitution.subst_vars exp_named_subst mty in - cty,ugraph2 + cty,ugraph2 | C.MutCase (uri,i,outtype,term,pl) -> let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in let (need_dummy, k) = @@ -1492,100 +1527,100 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = match outtype with C.Sort _ -> (true, 0) | C.Prod (name, s, t) -> - let (b, n) = - guess_args ((Some (name,(C.Decl s)))::context) t in - if n = 0 then - (* last prod before sort *) - match CicReduction.whd ~subst context s with + let (b, n) = + guess_args ((Some (name,(C.Decl s)))::context) t in + if n = 0 then + (* last prod before sort *) + match CicReduction.whd ~subst context s with (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> - (false, 1) + C.MutInd (uri',i',_) when U.eq uri' uri && i' = i -> + (false, 1) (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *) - | C.Appl ((C.MutInd (uri',i',_)) :: _) - when U.eq uri' uri && i' = i -> (false, 1) - | _ -> (true, 1) - else - (b, n + 1) + | C.Appl ((C.MutInd (uri',i',_)) :: _) + when U.eq uri' uri && i' = i -> (false, 1) + | _ -> (true, 1) + else + (b, n + 1) | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - "Malformed case analasys' output type %s" - (CicPp.ppterm outtype)))) + raise + (TypeCheckerFailure + (lazy (sprintf + "Malformed case analasys' output type %s" + (CicPp.ppterm outtype)))) in (* let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux context term ugraph1 in + let ty,ugraph2 = type_of_aux context term ugraph1 in match R.whd ~subst context ty with (*CSC manca il caso dei CAST *) (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *) (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo? *) (*CSC: Hint: nella DTD servono per gli stylesheet. *) C.MutInd (uri',i',exp_named_subst) as typ -> - if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri) i))) + if U.eq uri uri' && i = i' then + ([],[],exp_named_subst),ugraph2 + else + raise + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri) i))) | C.Appl - ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> - if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 - else - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s, "^ - "but is expected to be (an application of) "^ - "%s#1/%d{_}") - (CicPp.ppterm typ') (U.string_of_uri uri) i))) + ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> + if U.eq uri uri' && i = i' then + let params,args = + split tl (List.length tl - k) + in (params,args,exp_named_subst),ugraph2 + else + raise + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s, "^ + "but is expected to be (an application of) "^ + "%s#1/%d{_}") + (CicPp.ppterm typ') (U.string_of_uri uri) i))) | _ -> - raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysis: "^ - "analysed term %s is not an inductive one") - (CicPp.ppterm term)))) + raise + (TypeCheckerFailure + (lazy (sprintf + ("Case analysis: "^ + "analysed term %s is not an inductive one") + (CicPp.ppterm term)))) *) let (b, k) = guess_args context outsort in - if not b then (b, k - 1) else (b, k) in + if not b then (b, k - 1) else (b, k) in let (parameters, arguments, exp_named_subst),ugraph2 = - let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in + let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in match R.whd ~subst context ty with C.MutInd (uri',i',exp_named_subst) as typ -> if U.eq uri uri' && i = i' then - ([],[],exp_named_subst),ugraph2 + ([],[],exp_named_subst),ugraph2 else raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) -> if U.eq uri uri' && i = i' then - let params,args = - split tl (List.length tl - k) - in (params,args,exp_named_subst),ugraph2 + let params,args = + split tl (List.length tl - k) + in (params,args,exp_named_subst),ugraph2 else raise - (TypeCheckerFailure - (lazy (sprintf - ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) + (TypeCheckerFailure + (lazy (sprintf + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))) | _ -> raise - (TypeCheckerFailure - (lazy (sprintf - "Case analysis: analysed term %s is not an inductive one" + (TypeCheckerFailure + (lazy (sprintf + "Case analysis: analysed term %s is not an inductive one" (CicPp.ppterm term)))) in - (* - let's control if the sort elimination is allowed: - [(I q1 ... qr)|B] - *) + (* + let's control if the sort elimination is allowed: + [(I q1 ... qr)|B] + *) let sort_of_ind_type = if parameters = [] then C.MutInd (uri,i,exp_named_subst) @@ -1593,12 +1628,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in let type_of_sort_of_ind_ty,ugraph3 = - type_of_aux ~logger context sort_of_ind_type ugraph2 in + type_of_aux ~logger context sort_of_ind_type ugraph2 in let b,ugraph4 = - check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i + check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3 in - if not b then + if not b then raise (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed"))); (* let's check if the type of branches are right *) @@ -1625,24 +1660,24 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = let (_,branches_ok,ugraph5) = List.fold_left (fun (j,b,ugraph) p -> - if b then + if b then let cons = - if parameters = [] then - (C.MutConstruct (uri,i,j,exp_named_subst)) - else - (C.Appl - (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) + if parameters = [] then + (C.MutConstruct (uri,i,j,exp_named_subst)) + else + (C.Appl + (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in - let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in - let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in - (* 2 is skipped *) - let ty_branch = - type_of_branch ~subst context parsno need_dummy outtype cons - ty_cons in - let b1,ugraph4 = - R.are_convertible - ~subst ~metasenv context ty_p ty_branch ugraph3 - in + let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in + let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in + (* 2 is skipped *) + let ty_branch = + type_of_branch ~subst context parsno need_dummy outtype cons + ty_cons in + let b1,ugraph4 = + R.are_convertible + ~subst ~metasenv context ty_p ty_branch ugraph3 + in (* Debugging code if not b1 then begin @@ -1652,13 +1687,13 @@ prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons); prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch); end; *) - if not b1 then - debug_print (lazy - ("#### " ^ CicPp.ppterm ty_p ^ - " <==> " ^ CicPp.ppterm ty_branch)); - (j + 1,b1,ugraph4) - else - (j,false,ugraph) + if not b1 then + debug_print (lazy + ("#### " ^ CicPp.ppterm ty_p ^ + " <==> " ^ CicPp.ppterm ty_branch)); + (j + 1,b1,ugraph4) + else + (j,false,ugraph) ) (1,true,ugraph4) pl in if not branches_ok then @@ -1679,22 +1714,22 @@ end; let _,ugraph1 = type_of_aux ~logger context ty ugraph in (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, k::kl,ugraph1,len+1) - ) ([],[],ugraph,0) fl + ) ([],[],ugraph,0) fl in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (name,x,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types@context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types@context) - ty_bo (CicSubstitution.lift len ty) ugraph1 in - if b then - begin - let (m, eaten, context') = - eat_lambdas ~subst (types @ context) (x + 1) bo - in + let ty_bo,ugraph1 = + type_of_aux ~logger (types@context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types@context) + ty_bo (CicSubstitution.lift len ty) ugraph1 in + if b then + begin + let (m, eaten, context') = + eat_lambdas ~subst (types @ context) (x + 1) bo + in let rec_uri, rec_uri_len = let he = match List.hd context' with @@ -1714,74 +1749,74 @@ end; | _ -> assert false) | _ -> assert false in - (* - let's control the guarded by - destructors conditions D{f,k,x,M} - *) - if not (guarded_by_destructors ~logger ~metasenv ~subst + (* + let's control the guarded by + destructors conditions D{f,k,x,M} + *) + if not (guarded_by_destructors ~logger ~metasenv ~subst rec_uri rec_uri_len context' eaten (len + eaten) kl 1 [] m) then - raise - (TypeCheckerFailure - (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) - else - ugraph2 - end + raise + (TypeCheckerFailure + (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t))) + else + ugraph2 + end else - raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) + raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies"))) ) ugraph1 fl in - (*CSC: controlli mancanti solo su D{f,k,x,M} *) + (*CSC: controlli mancanti solo su D{f,k,x,M} *) let (_,_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 | C.CoFix (i,fl) -> let types,ugraph1,len = - List.fold_left - (fun (l,ugraph,len) (n,ty,_) -> + List.fold_left + (fun (l,ugraph,len) (n,ty,_) -> let _,ugraph1 = - type_of_aux ~logger context ty ugraph in - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, + type_of_aux ~logger context ty ugraph in + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l, ugraph1,len+1) - ) ([],ugraph,0) fl + ) ([],ugraph,0) fl in let ugraph2 = - List.fold_left + List.fold_left (fun ugraph (_,ty,bo) -> - let ty_bo,ugraph1 = - type_of_aux ~logger (types @ context) bo ugraph - in - let b,ugraph2 = - R.are_convertible ~subst ~metasenv (types @ context) ty_bo - (CicSubstitution.lift len ty) ugraph1 - in - if b then - begin - (* let's control that the returned type is coinductive *) - match returns_a_coinductive ~subst context ty with - None -> - raise - (TypeCheckerFailure - (lazy "CoFix: does not return a coinductive type")) - | Some uri -> - (* - let's control the guarded by constructors - conditions C{f,M} - *) - if not (guarded_by_constructors ~logger ~subst ~metasenv uri + let ty_bo,ugraph1 = + type_of_aux ~logger (types @ context) bo ugraph + in + let b,ugraph2 = + R.are_convertible ~subst ~metasenv (types @ context) ty_bo + (CicSubstitution.lift len ty) ugraph1 + in + if b then + begin + (* let's control that the returned type is coinductive *) + match returns_a_coinductive ~subst context ty with + None -> + raise + (TypeCheckerFailure + (lazy "CoFix: does not return a coinductive type")) + | Some uri -> + (* + let's control the guarded by constructors + conditions C{f,M} + *) + if not (guarded_by_constructors ~logger ~subst ~metasenv uri (types @ context) 0 len false bo) then - raise - (TypeCheckerFailure - (lazy "CoFix: not guarded by constructors")) - else - ugraph2 - end - else - raise - (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) + raise + (TypeCheckerFailure + (lazy "CoFix: not guarded by constructors")) + else + ugraph2 + end + else + raise + (TypeCheckerFailure (lazy "CoFix: ill-typed bodies")) ) ugraph1 fl in let (_,ty,_) = List.nth fl i in - ty,ugraph2 + ty,ugraph2 and check_exp_named_subst uri ~logger ~subst context ens ugraph = let params = @@ -1803,27 +1838,27 @@ end; in let rec check_exp_named_subst_aux ~logger esubsts l ugraph = match l with - [] -> ugraph + [] -> ugraph | ((uri,t) as item)::tl -> - let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in - let typeofvar = + let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in + let typeofvar = CicSubstitution.subst_vars esubsts ty_uri in - let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in - let b,ugraph3 = + let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in + let b,ugraph3 = CicReduction.are_convertible ~subst ~metasenv - context typeoft typeofvar ugraph2 - in - if b then + context typeoft typeofvar ugraph2 + in + if b then check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3 else begin - CicReduction.fdebug := 0 ; - ignore - (CicReduction.are_convertible - ~subst ~metasenv context typeoft typeofvar ugraph2) ; - fdebug := 0 ; - debug typeoft [typeofvar] ; - raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) + CicReduction.fdebug := 0 ; + ignore + (CicReduction.are_convertible + ~subst ~metasenv context typeoft typeofvar ugraph2) ; + fdebug := 0 ; + debug typeoft [typeofvar] ; + raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution")) end in check_same_order params ens ; @@ -1837,9 +1872,7 @@ end; | (C.Sort s1, C.Sort (C.Prop | C.Set)) -> (* different from Coq manual!!! *) t2',ugraph - | (C.Sort (C.Prop | C.Set | C.CProp), C.Sort C.CProp ) -> t2', ugraph - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) + | (C.Sort (C.Type t1 | C.CProp t1), C.Sort (C.Type t2)) -> let t' = CicUniv.fresh() in (try let ugraph1 = CicUniv.add_ge t' t1 ugraph in @@ -1847,10 +1880,16 @@ end; C.Sort (C.Type t'),ugraph2 with CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) - | (C.Sort _,C.Sort (C.Type t1)) - | (C.Sort (C.Type t1), C.Sort C.CProp) -> - (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *) - C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *) + | (C.Sort (C.CProp t1 | C.Type t1), C.Sort (C.CProp t2)) -> + let t' = CicUniv.fresh() in + (try + let ugraph1 = CicUniv.add_ge t' t1 ugraph in + let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in + C.Sort (C.CProp t'),ugraph2 + with + CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg)) + | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph + | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph | (C.Meta _, C.Sort _) -> t2',ugraph | (C.Meta _, (C.Meta (_,_) as t)) | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t -> @@ -1865,39 +1904,39 @@ end; match l with [] -> hetype,ugraph | (hete, hety)::tl -> - (match (CicReduction.whd ~subst context hetype) with + (match (CicReduction.whd ~subst context hetype) with Cic.Prod (n,s,t) -> - let b,ugraph1 = + let b,ugraph1 = (*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then( prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*) - CicReduction.are_convertible - ~subst ~metasenv context hety s ugraph - in - if b then - begin - CicReduction.fdebug := -1 ; - eat_prods ~subst context - (CicSubstitution.subst ~avoid_beta_redexes:true hete t) + CicReduction.are_convertible + ~subst ~metasenv context hety s ugraph + in + if b then + begin + CicReduction.fdebug := -1 ; + eat_prods ~subst context + (CicSubstitution.subst ~avoid_beta_redexes:true hete t) tl ugraph1 - (*TASSI: not sure *) - end - else - begin - CicReduction.fdebug := 0 ; - ignore (CicReduction.are_convertible - ~subst ~metasenv context s hety ugraph) ; - fdebug := 0 ; - debug s [hety] ; - raise - (TypeCheckerFailure - (lazy (sprintf - ("Appl: wrong parameter-type, expected %s, found %s") - (CicPp.ppterm hetype) (CicPp.ppterm s)))) - end - | _ -> - raise (TypeCheckerFailure - (lazy "Appl: this is not a function, it cannot be applied")) - ) + (*TASSI: not sure *) + end + else + begin + CicReduction.fdebug := 0 ; + ignore (CicReduction.are_convertible + ~subst ~metasenv context s hety ugraph) ; + fdebug := 0 ; + debug s [hety] ; + raise + (TypeCheckerFailure + (lazy (sprintf + ("Appl: wrong parameter-type, expected %s, found %s") + (CicPp.ppterm hetype) (CicPp.ppterm s)))) + end + | _ -> + raise (TypeCheckerFailure + (lazy "Appl: this is not a function, it cannot be applied")) + ) and returns_a_coinductive ~subst context ty = let module C = Cic in @@ -1920,7 +1959,7 @@ prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> ) | C.Appl ((C.MutInd (uri,i,_))::_) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with + match o with C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) @@ -1956,7 +1995,7 @@ and is_small_or_non_informative ~condition ~logger context paramsno c ugraph = is_small_or_non_informative_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1 else - false,ugraph1 + false,ugraph1 | _ -> true,ugraph (*CSC: we trust the type-checker *) in let (context',dx) = split_prods ~subst:[] context paramsno c in @@ -2035,7 +2074,7 @@ let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) = 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 + 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")) @@ -2048,12 +2087,12 @@ let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj ;; -let typecheck uri = +let typecheck ?(trust=true) uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in let logger = new CicLogger.logger in - match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with + match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) -> (* let's typecheck the uncooked object *) @@ -2061,7 +2100,7 @@ let typecheck uri = 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 + match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | _ -> raise CicEnvironmentError ;;