From: Enrico Tassi Date: Wed, 2 Apr 2008 13:15:27 +0000 (+0000) Subject: added slim version of does_not_occur X-Git-Tag: make_still_working~5467 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=507636cbb473500f40d0969a30e7afc7ddd88f2d;p=helm.git added slim version of does_not_occur --- diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index ecc63445c..fd7e756ce 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -89,90 +89,6 @@ let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types = exception CicEnvironmentError;; -and does_not_occur ?(subst=[]) context n nn te = - let module C = Cic in - match te with - C.Rel m when m > n && m <= nn -> false - | C.Rel m -> - (try - (match List.nth context (m-1) with - Some (_,C.Def (bo,_)) -> - does_not_occur ~subst context n nn (CicSubstitution.lift m bo) - | _ -> true) - with - Failure _ -> assert false) - | C.Sort _ - | C.Implicit _ -> true - | C.Meta (_,l) -> - List.fold_right - (fun x i -> - match x with - None -> i - | Some x -> i && does_not_occur ~subst context n nn x) l true && - (try - let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in - does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term) - with - CicUtil.Subst_not_found _ -> true) - | C.Cast (te,ty) -> - does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty - | C.Prod (name,so,dest) -> - does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) - (nn + 1) dest - | C.Lambda (name,so,dest) -> - does_not_occur ~subst context n nn so && - does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) - dest - | C.LetIn (name,so,ty,dest) -> - does_not_occur ~subst context n nn so && - does_not_occur ~subst context n nn ty && - does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context) - (n + 1) (nn + 1) dest - | C.Appl l -> - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) - | C.MutInd (_,_,exp_named_subst) - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x) - exp_named_subst true - | C.MutCase (_,_,out,te,pl) -> - does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te && - List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true - | C.Fix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let nn_plus_len = nn + len in - let tys,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo - ) fl true - | C.CoFix (_,fl) -> - let len = List.length fl in - let n_plus_len = n + len in - let nn_plus_len = nn + len in - let tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - List.fold_right - (fun (_,ty,bo) i -> - i && does_not_occur ~subst context n nn ty && - 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 *) @@ -1293,6 +1209,30 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty = aux ty_he args_with_ty ;; +exception DoesOccur;; + +let does_not_occur ~subst context n nn t = + let rec aux (context,n,nn as k) _ = function + | C.Rel m when m > n && m <= nn -> raise DoesOccur + | C.Rel m -> + (try (match List.nth context (m-1) with + | _,C.Def (bo,_) -> aux k () (S.lift m bo) + | _ -> ()) + with Failure _ -> assert false) + | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) () + | C.Meta (mno,(s,l)) -> + (try + let _,_,term,_ = U.lookup_subst mno subst in + aux (context,n+s,nn+s) () (S.subst_meta (0,l) term) + with CicUtil.Subst_not_found _ -> match l with + | C.Irl len -> if not (n >= s+len || s > nn) then raise DoesOccur + | C.Ctx lc -> List.iter (aux (context,n+s,nn+s) ()) lc) + | t -> U.fold (fun e (ctx,n,nn) -> (e::ctx,n+1,nn+1)) k aux () t + in + try aux (context,n,nn) () t; true + with DoesOccur -> false +;; + let rec typeof ~subst ~metasenv context term = let rec typeof_aux context = function | C.Rel n -> @@ -1307,10 +1247,10 @@ let rec typeof ~subst ~metasenv context term = | C.Meta (n,l) as t -> let canonical_context,ty = try - let _,c,_,ty = NCicUtils.lookup_subst n subst in c,ty - with NCicUtils.Subst_not_found _ -> try - let _,_,c,ty = NCicUtils.lookup_meta n metasenv in c,ty - with NCicUtils.Meta_not_found _ -> + let _,c,_,ty = U.lookup_subst n subst in c,ty + with U.Subst_not_found _ -> try + let _,_,c,ty = U.lookup_meta n metasenv in c,ty + with U.Meta_not_found _ -> raise (AssertFailure (lazy (Printf.sprintf "%s not found" (NCicPp.ppterm t)))) in @@ -1475,7 +1415,7 @@ let rec typeof ~subst ~metasenv context term = S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl) in lift_metas 1 canonical_context in - let l = NCicUtils.expand_local_context lc_kind in + let l = U.expand_local_context lc_kind in try List.iter2 (fun t ct -> @@ -1643,8 +1583,7 @@ and typecheck_obj0 (uri,height,metasenv,subst,kind) = in List.iter (fun (_,name,x,ty,bo) -> let ty_bo = typeof ~subst ~metasenv types bo in - if not (R.are_convertible ~subst ~metasenv types ty_bo - (S.lift len ty)) + if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty)) then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) else if inductive then begin