From 6df971c040176977f74ee5b2b7913b4fda23bb63 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 4 Sep 2006 11:21:26 +0000 Subject: [PATCH] Bug fixing. If the inductive types do not occur in t, t is strictly positive. --- .../cic_proof_checking/cicTypeChecker.ml | 74 +++++++++++-------- 1 file changed, 42 insertions(+), 32 deletions(-) diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml index 531705a3c..c0e90a5c6 100644 --- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml +++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml @@ -377,7 +377,10 @@ and weakly_positive context n nn uri te = | 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 (C.Anonymous,source,dest) -> strictly_positive context n nn @@ -389,13 +392,13 @@ and weakly_positive context n nn uri te = (* 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) + 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 + 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")) @@ -415,7 +418,8 @@ and strictly_positive context n nn te = let module C = Cic in let module U = UriManager in match CicReduction.whd context te with - C.Rel _ -> true + | t when does_not_occur context n nn t -> true + | C.Rel _ -> true | C.Cast (te,ty) -> (*CSC: bisogna controllare ty????*) strictly_positive context n nn te @@ -427,37 +431,39 @@ and strictly_positive context n nn te = | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) -> let (ok,paramsno,ity,cl,name) = 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 - (List.length tl = 1, paramsno, ity, cl, name) - | _ -> - 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 - let cl' = + match o with + C.InductiveDefinition (tl,_,paramsno,_) -> + 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))) + in + let (params,arguments) = split tl paramsno in + let lifted_params = List.map (CicSubstitution.lift 1) params in + let cl' = List.map - (fun (_,te) -> - instantiate_parameters lifted_params - (CicSubstitution.subst_vars exp_named_subst te) - ) cl - in + (fun (_,te) -> + instantiate_parameters lifted_params + (CicSubstitution.subst_vars exp_named_subst te) + ) cl + in ok && - List.fold_right + List.fold_right (fun x i -> i && does_not_occur context n nn x) arguments true && (*CSC: MEGAPATCH3 (sara' quella giusta?)*) - List.fold_right + List.fold_right (fun x i -> - i && - weakly_positive - ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri - x + i && + weakly_positive + ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri + x ) cl' true - | t -> does_not_occur context n nn t - + | t -> false + (* the inductive type indexes are s.t. n < x <= nn *) and are_all_occurrences_positive context uri indparamsno i n nn te = let module C = Cic in @@ -494,7 +500,8 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ UriManager.string_of_uri uri))) | C.Prod (C.Anonymous,source,dest) -> - strictly_positive context n nn source && + let b = strictly_positive context n nn source in + b && are_all_occurrences_positive ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno (i+1) (n + 1) (nn + 1) dest @@ -553,9 +560,12 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (are_all_occurrences_positive tys uri indparamsno i 0 len debrujinedte) 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))) + (lazy ("Non positive occurence in " ^ U.string_of_uri uri))) end else ugraph' ) ugraph cl in -- 2.39.2