From 641ab7e5aa7dbfa352028d7bba95def7234cc3f1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 13 Oct 2009 13:36:32 +0000 Subject: [PATCH] relocate is hopefully fixed once and for-all! --- .../components/ng_tactics/nTacStatus.ml | 77 +++++++++++-------- 1 file changed, 43 insertions(+), 34 deletions(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 70ddfeaa9..8d47439c0 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -73,51 +73,60 @@ let relocate status destination (source,t as orig) = pp(lazy("relocate in:\n" ^ ppcontext status destination)); let rc = if source == destination then status, orig else - let u, d, metasenv, subst, o = status#obj in - let cons x (a,b) = a, x::b in - let rec lcp ctx j i = function - | (n1, NCic.Decl t1 as e)::cl1, (n2, NCic.Decl t2)::cl2 -> + 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 - cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2)) + compute_ops (e::ctx) (cl1,cl2) else - j, [] - | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Def (b2,t2))::cl2 -> + [ `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 - cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2)) + compute_ops (e::ctx) (cl1,cl2) else - j, [] - | (n1, NCic.Def (b1,t1) as e)::cl1, (n2, NCic.Decl t2)::cl2 -> + [ `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 - cons (NCic.Rel i) (lcp (e::ctx)(j-1) (i-1) (cl1,cl2)) + compute_ops (e::ctx) (cl1,cl2) else - j, [] - | (n1, NCic.Decl _)::cl1, (n2, NCic.Def _)::cl2 -> assert false - | _::_, [] -> j, [] - | _ -> 0, [] + [ `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 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 in pp(lazy("relocated: " ^ ppterm (fst rc) (snd rc))); rc -- 2.39.2