| _ -> 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 apply_subst 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
+ 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
+;;