- prerr_endline (NCicPp.ppobj status.istatus.pstatus)
-;;
-
-let pp_lowtac_status status =
- prerr_endline "--------------------------------------------";
- prerr_endline (NCicPp.ppobj status.pstatus)
-;;
-
-type cic_term = NCic.conjecture (* name, context, term *)
-let ctx_of (_,c,_) = c ;;
-
-let relocate status destination (name,source,t as orig) =
- if source == destination then status, orig else
- let rec lcp j i = function
- | (n1, t1)::cl1, (n2, t2)::cl2 ->
- if n1 = n2 && t1 = t2 then
- NCic.Rel i :: lcp (j-1) (i-1) (cl1,cl2)
- else
- HExtlib.mk_list (NCic.Appl
- [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
- | _::_, [] ->
- HExtlib.mk_list (NCic.Appl
- [NCic.Sort NCic.Prop; NCic.Sort NCic.Prop]) j
- | _ -> []
- in
- let lc =
- lcp (List.length destination) (List.length source)
- (List.rev destination, List.rev source)
- in
- let lc = (0,NCic.Ctx (List.rev lc)) in
- let u, d, metasenv, subst, o = status.pstatus in
- let db = NCicUnifHint.db () in (* XXX fixme *)
- let (metasenv, subst), t =
- NCicMetaSubst.delift
- ~unify:(fun m s c t1 t2 ->
- try Some (NCicUnification.unify db m s c t1 t2)
- with
- | NCicUnification.UnificationFailure _
- | NCicUnification.Uncertain _ -> None)
- metasenv subst source 0 lc t
- in
- let status = { status with pstatus = u, d, metasenv, subst, o } in
- status, (name, destination, t)
+ prerr_endline (NCicPp.ppobj status#obj);
+ prerr_endline ("STACK:\n" ^ Continuationals.Stack.pp status#stack)
+;;
+
+type cic_term = NCic.context * NCic.term
+let ctx_of (c,_) = c ;;
+let mk_cic_term c t = c,t ;;
+
+let ppterm status t =
+ let uri,height,metasenv,subst,obj = status#obj in
+ let context,t = t in
+ NCicPp.ppterm ~metasenv ~subst ~context t
+;;
+
+let ppcontext status c =
+ let uri,height,metasenv,subst,obj = status#obj in
+ NCicPp.ppcontext ~metasenv ~subst c
+;;
+
+let ppterm_and_context status t =
+ let uri,height,metasenv,subst,obj = status#obj in
+ let context,t = t in
+ NCicPp.ppcontext ~metasenv ~subst context ^ "\n ⊢ "^
+ NCicPp.ppterm ~metasenv ~subst ~context t
+;;
+
+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