X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=771568018b0d44ca99c61580e27152d2f1befad1;hb=da0c52aa34feaacdcefdf67df433ebbc367fdbc2;hp=95f40da5368ff06fe99991f33dc372c3d67f6d57;hpb=1bd6b7d2637d765f11ddbd1218d63474e9d0c63b;p=helm.git diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 95f40da53..771568018 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -96,14 +96,16 @@ let mk_appl he args = | _ -> NCic.Appl (he::args) ;; -let map_obj_kind f = +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,HExtlib.map_option f bo, f 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,f bo) + (function (relevance,name,recno,ty,bo) -> + relevance,name,recno,f ty,do_bo f bo) fl in NCic.Fixpoint (ind,fl,attrs) @@ -122,7 +124,87 @@ let map_obj_kind f = NCic.Inductive (is_ind,lno,itl,attrs) ;; -let apply_subst subst t = +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 rec fire_projection_redex on_args = function + | C.Meta _ as t -> t + | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot-> + let l= if on_args then List.map (fire_projection_redex true) ol else ol in + let t = if l == ol then ot else C.Appl l in + let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in + let conclude () = + if on_args then + let l' = HExtlib.sharing_map (fire_projection_redex true) l in + if l == l' then t else C.Appl l' + else + t (* ot is the same *) + in + if pragma <> `Projection || List.length args <= rno then conclude () + else + (match List.nth args rno with + | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) -> + let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *) + let t = C.Appl (fbody::args) in + (match NCicReduction.head_beta_reduce ~delta:max_int t with + | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])-> + let _,kargs = HExtlib.split_nth leftno kargs in + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs))) + | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) -> + let _,kargs = HExtlib.split_nth leftno kargs in + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs @ args))) + | _ -> conclude ()) + | _ -> conclude ()) + | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t + | t -> t +;; + +let apply_subst ?(fix_projections=false) subst context t = let rec apply_subst subst () = function NCic.Meta (i,lc) -> @@ -131,7 +213,7 @@ let apply_subst subst t = let t = NCicSubstitution.subst_meta lc t in apply_subst subst () t with - Not_found -> + NCicUtils.Subst_not_found j when j = i -> match lc with _,NCic.Irl _ -> NCic.Meta (i,lc) | n,NCic.Ctx l -> @@ -141,6 +223,32 @@ let apply_subst subst t = apply_subst subst () (NCicSubstitution.lift n t)) l)))) | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t in - apply_subst subst () t + (if fix_projections then fire_projection_redex true else fun x -> x) + (clean_or_fix_dependent_abstrations context (apply_subst subst () t)) +;; + +let apply_subst_context ~fix_projections subst context = + let apply_subst = apply_subst ~fix_projections in + 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 ~fix_projections:true subst ctx, + apply_subst ~fix_projections:true subst ctx ty)) :: + apply_subst_metasenv subst tl ;; +(* hide optional arg *) +let apply_subst s c t = apply_subst s c t;; +