aux (List.map fst ctx) t
;;
-let rec fire_projection_redex () = function
+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 = List.map (fire_projection_redex ()) ol in
+ 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 () =
- let l' = HExtlib.sharing_map (fire_projection_redex ()) l in
- if l == l' then t else C.Appl l'
+ 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 ()
+ if pragma <> `Projection || List.length args <= rno then conclude ()
else
(match List.nth args rno with
| C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
(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
- NCicReduction.head_beta_reduce
- ~delta:max_int (C.Appl (pat :: kargs))
+ 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
- NCicReduction.head_beta_reduce
- ~delta:max_int (C.Appl (pat :: kargs @ args))
+ fire_projection_redex false
+ (NCicReduction.head_beta_reduce
+ ~delta:max_int (C.Appl (pat :: kargs @ args)))
| _ -> conclude ())
| _ -> conclude ())
- | t -> NCicUtils.map (fun _ _ -> ()) () fire_projection_redex t
+ | 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 =
apply_subst subst () (NCicSubstitution.lift n t)) l))))
| t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
in
- (if fix_projections then fire_projection_redex () else fun x -> x)
+ (if fix_projections then fire_projection_redex true else fun x -> x)
(clean_or_fix_dependent_abstrations context (apply_subst subst () t))
;;