+let relocate status destination (source,t as orig) =
+ pp(lazy("relocate:\n" ^ ppterm_and_context status orig));
+ pp(lazy("relocate in:\n" ^ ppcontext status destination));
+ let rc =
+ if source == destination then status, orig else
+ let _, _, metasenv, subst, _ = status#obj in
+ let rec compute_ops ctx = function (* destination, source *)
+ | (n1, NCic.Decl t1 as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
+ if n1 = n2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
+ compute_ops (e::ctx) (cl1,cl2)
+ else
+ [ `Delift ctx; `Lift (List.rev ex) ]
+ | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Def (b2,t2))::cl2 ->
+ if n1 = n2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv b1 b2 then
+ compute_ops (e::ctx) (cl1,cl2)
+ else
+ [ `Delift ctx; `Lift (List.rev ex) ]
+ | (n1, NCic.Def (b1,t1) as e)::cl1 as ex, (n2, NCic.Decl t2)::cl2 ->
+ if n1 = n2 &&
+ NCicReduction.are_convertible ctx ~subst ~metasenv t1 t2 then
+ compute_ops (e::ctx) (cl1,cl2)
+ else
+ [ `Delift ctx; `Lift (List.rev ex) ]
+ | (n1, NCic.Decl _)::cl1 as ex, (n2, NCic.Def _)::cl2 ->
+ [ `Delift ctx; `Lift (List.rev ex) ]
+ | _::_ as ex, [] -> [ `Lift (List.rev ex) ]
+ | [], _::_ -> [ `Delift ctx ]
+ | [],[] -> []
+ in
+ 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
+ in
+ pp(lazy("relocated: " ^ ppterm (fst rc) (snd rc)));
+ rc
+;;
+let relocate a b c = wrap "relocate" (relocate a b) c;;