- let shift, lc =
- lcp [] (List.length destination) (List.length source)
- (List.rev destination, List.rev source)
- in
- let lc = (shift,NCic.Ctx (List.rev lc)) in
- pp(lazy("delifting as " ^
- NCicPp.ppterm ~metasenv ~subst ~context:source
- (NCic.Meta (0,lc))));
- let (metasenv, subst), t =
- NCicMetaSubst.delift
- ~unify:(fun m s c t1 t2 ->
- try Some (NCicUnification.unify status m s c t1 t2)
- with
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _ -> None)
- metasenv subst source 0 lc t
- in
- let status = status#set_obj (u, d, metasenv, subst, o) in
- status, (destination, t)
+ let ops = compute_ops [] (List.rev destination, List.rev source) in
+ let rec mk_irl i j = if i > j then [] else NCic.Rel i :: mk_irl (i+1) j in
+ List.fold_left
+ (fun (status, (source,t)) -> function
+ | `Lift extra_ctx ->
+ let len = List.length extra_ctx in
+ status, (extra_ctx@source, NCicSubstitution.lift len t)
+ | `Delift ctx ->
+ let len_ctx = List.length ctx in
+ let irl = mk_irl 1 (List.length ctx) in
+ let lc = List.length source - len_ctx, NCic.Ctx irl in
+ let u, d, metasenv, subst, o = status#obj in
+ pp(lazy("delifting as " ^
+ NCicPp.ppterm ~metasenv ~subst ~context:source
+ (NCic.Meta (0,lc))));
+ let (metasenv, subst), t =
+ NCicMetaSubst.delift
+ ~unify:(fun m s c t1 t2 ->
+ try Some (NCicUnification.unify status m s c t1 t2)
+ with
+ | NCicUnification.UnificationFailure _
+ | NCicUnification.Uncertain _ -> None)
+ metasenv subst source 0 lc t
+ in
+ let status = status#set_obj (u, d, metasenv, subst, o) in
+ status, (ctx,t))
+ (status,orig) ops