X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicTypeChecker.ml;h=ca76827068c7b893326369800910c27676ebf1e0;hb=987627a48b2a3c2345d1af2c2a6b1ab78aa90b58;hp=289ef4b76dc91d5d1c89593c628b29f7e463094e;hpb=0b15dfdee3357a626c77d30599e87a83ab34e471;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 289ef4b76..ca7682706 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 @@ -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,19 +461,21 @@ 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 -> @@ -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 @@ -592,12 +598,9 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (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 + (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) else ugraph ) ugraph cl in @@ -1132,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 @@ -1171,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? *) @@ -1327,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 @@ -1419,7 +1446,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = 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