X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=dc26794a1a096cb4f9575e93cf9e826cbe83989a;hb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;hp=d7635fe8860ef409efa5534aa255d3ba263562dc;hpb=62f476a05884d451bfb90d845ea2b1c0a1c77f96;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index d7635fe88..dc26794a1 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -22,15 +22,23 @@ let map_term_fold_a g k f a = function | C.Rel _ as t -> a,t | C.Appl [] | C.Appl [_] -> assert false | C.Appl l as orig -> + let fire_beta, upto = + match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 + in let a,l1 = (* sharing fold? *) List.fold_right (fun t (a,l) -> let a,t = f k a t in a, t :: l) l (a,[]) in - a, if l1 == l then orig else (match l1 with - | C.Appl l :: tl -> C.Appl (l@tl) - | _ -> C.Appl l1) + a, if l1 == l then orig else + let t = + match l1 with + | C.Appl l :: tl -> C.Appl (l@tl) + | _ -> C.Appl l1 + in + if fire_beta then NCicReduction.head_beta_reduce ~upto t + else t | C.Prod (n,s,t) as orig -> let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1) @@ -87,3 +95,156 @@ let mk_appl he args = | NCic.Appl l -> NCic.Appl (l@args) | _ -> NCic.Appl (he::args) ;; + +let map_obj_kind ?(skip_body=false) f = + let do_bo f x = if skip_body then x else f x in + function + NCic.Constant (relev,name,bo,ty,attrs) -> + NCic.Constant (relev,name,do_bo (HExtlib.map_option f) bo, f ty,attrs) + | NCic.Fixpoint (ind,fl,attrs) -> + let fl = + List.map + (function (relevance,name,recno,ty,bo) -> + relevance,name,recno,f ty,do_bo f bo) + fl + in + NCic.Fixpoint (ind,fl,attrs) + | NCic.Inductive (is_ind,lno,itl,attrs) -> + let itl = + List.map + (fun (relevance,name,ty,cl) -> + let cl = + List.map (fun (relevance, name, ty) -> + relevance, name, f ty) + cl + in + relevance, name, f ty, cl) + itl + in + NCic.Inductive (is_ind,lno,itl,attrs) +;; + +exception Occurr;; + +let clean_or_fix_dependent_abstrations ctx t = + let occurrs_1 t = + let rec aux n _ = function + | NCic.Meta _ -> () + | NCic.Rel i when i = n + 1 -> raise Occurr + | t -> NCicUtils.fold (fun _ k -> k + 1) n aux () t + in + try aux 0 () t; false + with Occurr -> true + in + let fresh ctx name = + if not (List.mem name ctx) then name + else + let rec aux i = + let attempt = name ^ string_of_int i in + if List.mem attempt ctx then aux (i+1) + else attempt + in + aux 0 + in + let rec aux ctx = function + | NCic.Meta _ as t -> t + | NCic.Prod (name,s,t) when name.[0] = '#' && occurrs_1 t -> + let name = fresh ctx (String.sub name 1 (String.length name-1)) in + NCic.Prod (name,aux ctx s, aux (name::ctx) t) + | NCic.Prod (name,s,t) when name.[0] = '#' && not (occurrs_1 t) -> + NCic.Prod ("_",aux ctx s,aux ("_"::ctx) t) + | NCic.Prod ("_",s,t) -> NCic.Prod("_",aux ctx s,aux ("_"::ctx) t) + | NCic.Prod (name,s,t) when name.[0] <> '_' && not (occurrs_1 t) -> + let name = fresh ctx ("_"^name) in + NCic.Prod (name, aux ctx s, aux (name::ctx) t) + | NCic.Prod (name,s,t) when List.mem name ctx -> + let name = fresh ctx name in + NCic.Prod (name, aux ctx s, aux (name::ctx) t) + | NCic.Lambda (name,s,t) when List.mem name ctx -> + let name = fresh ctx name in + NCic.Lambda (name, aux ctx s, aux (name::ctx) t) + | t -> NCicUtils.map (fun (e,_) ctx -> e::ctx) ctx aux t + in + aux (List.map fst ctx) t +;; + +let apply_subst subst context t = + let rec apply_subst subst () = + function + NCic.Meta (i,lc) -> + (try + let _,_,t,_ = NCicUtils.lookup_subst i subst in + let t = NCicSubstitution.subst_meta lc t in + apply_subst subst () t + with + Not_found -> + match lc with + _,NCic.Irl _ -> NCic.Meta (i,lc) + | n,NCic.Ctx l -> + NCic.Meta + (i,(0,NCic.Ctx + (List.map (fun t -> + apply_subst subst () (NCicSubstitution.lift n t)) l)))) + | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t + in + clean_or_fix_dependent_abstrations context (apply_subst subst () t) +;; + +let apply_subst_context subst context = + let rec aux c = function + | [] -> [] + | (name,NCic.Decl t as e) :: tl -> + (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl + | (name,NCic.Def (t1,t2) as e) :: tl -> + (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) :: + aux (e::c) tl + in + List.rev (aux [] (List.rev context)) +;; + +let rec apply_subst_metasenv subst = function + | [] -> [] + | (i,_) :: _ when List.mem_assoc i subst -> assert false + | (i,(name,ctx,ty)) :: tl -> + (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) :: + apply_subst_metasenv subst tl +;; + +let height_of_term tl = + let h = ref 0 in + let get_height (NReference.Ref (uri,_)) = + let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in + height in + let rec aux = + function + NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l + | NCic.Meta _ -> () + | NCic.Rel _ + | NCic.Sort _ -> () + | NCic.Implicit _ -> assert false + | NCic.Const nref -> h := max !h (get_height nref) + | NCic.Prod (_,t1,t2) + | NCic.Lambda (_,t1,t2) -> aux t1; aux t2 + | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t + | NCic.Appl l -> List.iter aux l + | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl + in + List.iter aux tl; + 1 + !h +;; + +let height_of_obj_kind uri = + function + NCic.Inductive _ + | NCic.Constant (_,_,None,_,_) + | NCic.Fixpoint (false,_,_) -> 0 + | NCic.Fixpoint (true,ifl,_) -> + let iflno = List.length ifl in + height_of_term + (List.fold_left + (fun l (_,_,_,ty,bo) -> + let bo = NCicTypeChecker.debruijn uri iflno [] bo in + ty::bo::l + ) [] ifl) + | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty] +;;