From 5e5d161f094982275ce39dbb4780c106e4475b37 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 Jul 2008 16:09:17 +0000 Subject: [PATCH] positivity check fixed, some subterms were erroneously skipped --- .../cic_proof_checking/cicTypeChecker.ml | 98 +++++++++---------- 1 file changed, 49 insertions(+), 49 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 289ef4b76..f450dcd89 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -337,92 +337,95 @@ and does_not_occur ?(subst=[]) context n nn te = and weakly_positive context n nn uri 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,[]) + let leftno = + match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with + | Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno + | _ -> assert false in + let dummy = Cic.Sort Cic.Prop in (*CSC: mettere in cicSubstitution *) - let rec subst_inductive_type_with_dummy_mutind = + 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")) + 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 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 source && + weakly_positive ((Some (name,(C.Decl source)))::context) + (n + 1) (nn + 1) uri 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|} *) @@ -592,12 +595,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 -- 2.39.2