| _ -> 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)
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) ->
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 ->
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;;
+
projects / helm.git / blobdiff