From: Enrico Tassi Date: Fri, 11 Apr 2008 16:45:29 +0000 (+0000) Subject: quinck and untested implementation of positivity conditions check X-Git-Tag: make_still_working~5348 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=574819cdf8dedfbef960ec71ef73e67ca8f9a0a0;p=helm.git quinck and untested implementation of positivity conditions check --- diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 9de1f0f5c..a77b293c1 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -28,217 +28,9 @@ let shift_k e (c,rf,x,safes) = (* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *) -(* -exception CicEnvironmentError;; -(*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 = - 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,[]) - in - (*CSC: mettere in cicSubstitution *) - let rec subst_inductive_type_with_dummy_mutind = - function - C.MutInd (uri',0,_) when UriManager.eq uri' uri -> - dummy_mutind - | 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 - | C.Prod (name,so,ta) -> - C.Prod (name, subst_inductive_type_with_dummy_mutind so, - subst_inductive_type_with_dummy_mutind ta) - | C.Lambda (name,so,ta) -> - C.Lambda (name, subst_inductive_type_with_dummy_mutind so, - subst_inductive_type_with_dummy_mutind ta) - | C.Appl tl -> - C.Appl (List.map subst_inductive_type_with_dummy_mutind 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) - | 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) - | 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) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map - (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t)) - exp_named_subst - in - C.Const (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)) - 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)) - 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 (C.Anonymous,source,dest) -> - strictly_positive context n nn - (subst_inductive_type_with_dummy_mutind source) && - weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context) - (n + 1) (nn + 1) uri dest - | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n 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")) - -(* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) -(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) -and instantiate_parameters params c = - let module C = Cic in - match (c,params) with - (c,[]) -> c - | (C.Prod (_,_,ta), he::tl) -> - instantiate_parameters tl - (CicSubstitution.subst he ta) - | (C.Cast (te,_), _) -> instantiate_parameters params te - | (t,l) -> raise (AssertFailure (lazy "1")) - -and strictly_positive context n nn 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.Cast (te,ty) -> - (*CSC: bisogna controllare ty????*) - strictly_positive context n nn 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 -> - 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))::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) - (* (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 - ok && - List.fold_right - (fun x i -> i && does_not_occur context n nn x) - arguments true && - (*CSC: MEGAPATCH3 (sara' quella giusta?)*) - List.fold_right - (fun x i -> - i && - weakly_positive - ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri - x - ) cl' true - | 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 - 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.Rel m when m = i -> - if indparamsno = 0 then - true - else - raise (TypeCheckerFailure - (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ - UriManager.string_of_uri uri))) - | C.Prod (C.Anonymous,source,dest) -> - 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 - | C.Prod (name,source,dest) when - does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest -> - (* dummy abstraction, so we behave as in the anonimous case *) - strictly_positive context n nn source && - are_all_occurrences_positive - ((Some (name,(C.Decl source)))::context) uri indparamsno - (i+1) (n + 1) (nn + 1) dest - | C.Prod (name,source,dest) -> - does_not_occur context n nn source && - are_all_occurrences_positive ((Some (name,(C.Decl source)))::context) - uri indparamsno (i+1) (n + 1) (nn + 1) dest - | _ -> - raise - (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^ - (UriManager.string_of_uri uri)))) +(* (* 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. *) @@ -618,6 +410,116 @@ let does_not_occur ~subst context n nn t = with DoesOccur -> false ;; +(*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 ;-) *) +let rec weakly_positive ~subst context n nn uri te = +(*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*) + let dummy_mutind = C.Implicit `Hole in + (*CSC: mettere in cicSubstitution *) + let rec subst_inductive_type_with_dummy_mutind _ = function + | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy_mutind + | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) when NUri.eq uri' uri -> + dummy_mutind + | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy_mutind t + in + match R.whd context te with + | C.Const (Ref.Ref (_,uri',Ref.Ind _)) + | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true + | C.Prod (name,source,dest) when + does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest -> + (* dummy abstraction, so we behave as in the anonimous case *) + strictly_positive ~subst context n nn + (subst_inductive_type_with_dummy_mutind () source) && + weakly_positive ~subst ((name,C.Decl source)::context) + (n + 1) (nn + 1) uri dest + | C.Prod (name,source,dest) -> + does_not_occur ~subst context n nn + (subst_inductive_type_with_dummy_mutind () source)&& + weakly_positive ~subst ((name,C.Decl source)::context) + (n + 1) (nn + 1) uri dest + | _ -> + raise (TypeCheckerFailure (lazy "Malformed inductive constructor type")) + +(* instantiate_parameters ps (x1:T1)...(xn:Tn)C *) +(* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *) +and instantiate_parameters params c = + match c, params with + | c,[] -> c + | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta) + | t,l -> raise (AssertFailure (lazy "1")) + +and strictly_positive ~subst context n nn te = + match R.whd context te with + | t when does_not_occur ~subst context n nn t -> true + | C.Rel _ -> true + | C.Prod (name,so,ta) -> + does_not_occur ~subst context n nn so && + strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta + | C.Appl ((C.Rel m)::tl) when m > n && m <= nn -> + List.for_all (does_not_occur ~subst context n nn) tl + | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) -> + let _,paramsno,tyl,_,i = E.get_checked_indtys r in + let _,name,ity,cl = List.nth tyl i in + let ok = List.length tyl = 1 in + let params, arguments = HExtlib.split_nth paramsno tl in + let lifted_params = List.map (S.lift 1) params in + let cl = + List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl + in + ok && + List.for_all (does_not_occur ~subst context n nn) arguments && + List.for_all + (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl + | _ -> false + +(* the inductive type indexes are s.t. n < x <= nn *) +and are_all_occurrences_positive ~subst context uri indparamsno i n nn te = + match R.whd context te with + | C.Appl ((C.Rel m)::tl) when m = i -> + let last = + List.fold_left + (fun k x -> + if k = 0 then 0 + else + match R.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]" ^ + NUri.string_of_uri uri)))) + indparamsno tl + in + if last = 0 then + List.for_all (does_not_occur ~subst context n nn) tl + else + raise (TypeCheckerFailure + (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^ + NUri.string_of_uri uri))) + | C.Rel m when m = i -> + if indparamsno = 0 then + true + else + raise (TypeCheckerFailure + (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^ + NUri.string_of_uri uri))) + | C.Prod (name,source,dest) when + does_not_occur ~subst ((name,C.Decl source)::context) 0 n dest -> + strictly_positive ~subst context n nn source && + are_all_occurrences_positive ~subst + ((name,C.Decl source)::context) uri indparamsno + (i+1) (n + 1) (nn + 1) dest + | C.Prod (name,source,dest) -> + does_not_occur ~subst context n nn source && + are_all_occurrences_positive ~subst ((name,C.Decl source)::context) + uri indparamsno (i+1) (n + 1) (nn + 1) dest + | _ -> + raise + (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^ + (NUri.string_of_uri uri)))) +;; + exception NotGuarded of string Lazy.t;; let rec typeof ~subst ~metasenv context term = @@ -960,10 +862,10 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = let debruijnedte = debruijn uri len te in ignore (typeof ~subst ~metasenv tys debruijnedte); (* let's check also the positivity conditions *) - if false (* + if not - (are_all_occurrences_positive tys uri indparamsno i 0 len - debruijnedte) *) + (are_all_occurrences_positive ~subst tys uri leftno i 0 len + debruijnedte) then raise (TypeCheckerFailure