src/Provers/IsaPlanner/zipper.ML

 sig
   structure C : TRM_CTXT
   type T
 
   val mktop : C.D.Trm.T -> T
-  val goto_top : T -> T
+  val mk : (C.D.Trm.T * C.T) -> T
+
+  val goto_top : T -> T 
   val at_top : T -> bool
-  val mk : (C.D.Trm.T * C.T) -> T
+
+  val split : T -> T * C.T
+  val add_outerctxt : C.T -> T -> T
+
   val set_trm : C.D.Trm.T -> T -> T
   val set_ctxt : C.T -> T -> T
 
-  val split : T -> T * C.T
-  val add_outerctxt : C.T -> T -> T
-
   val ctxt : T -> C.T
   val trm : T -> C.D.Trm.T
+  val top_trm : T -> C.D.Trm.T
+
+  val zipto : C.T -> T -> T (* follow context down *)
 
   val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
   val ty_ctxt : T -> C.D.Trm.typ list;
 
   val depth_of_ctxt : T -> int;

   fun split (t,c) = ((t,C.empty) : T, c : C.T) 
   fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T
 
   val ctxt = snd;
   val trm = fst;
+  val top_trm = trm o goto_top;
 
   fun nty_ctxt x = C.nty_ctxt (ctxt x);
   fun ty_ctxt x = C.ty_ctxt (ctxt x);
 
   fun depth_of_ctxt x = C.depth (ctxt x);

     | move_down_right z = raise move ("move_down_right",z);
   fun move_down_app (Trm.$(l,r),c) = 
       ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
     | move_down_app z = raise move ("move_down_app",z);
 
+  (* follow the given path down the given zipper *)
+  (* implicit arguments: C.D.dtrm list, then T *)
+  val zipto = 
+      C.fold (fn C.D.Abs _ => move_down_abs 
+               | C.D.AppL _ => move_down_left
+               | C.D.AppR _ => move_down_right) 
 
   (* Note: interpretted as being examined depth first *)
   datatype zsearch = Here of T | LookIn of T;
 
+  (* lazy search *)
   fun lzy_search fsearch = 
       let 
         fun lzyl [] () = NONE
           | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
           | lzyl ((LookIn z) :: more) () =