+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 =