src/Provers/IsaPlanner/zipper.ML
changeset 23171 861f63a35d31
parent 23170 94e9413bd7fc
child 23172 f1ae6a8648ef
     1.1 --- a/src/Provers/IsaPlanner/zipper.ML	Thu May 31 19:11:19 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,491 +0,0 @@
     1.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      Pure/IsaPlanner/zipper.ML
     1.6 -    ID:		$Id$
     1.7 -    Author:     Lucas Dixon, University of Edinburgh
     1.8 -                lucas.dixon@ed.ac.uk
     1.9 -    Created:    24 Mar 2006
    1.10 -*)
    1.11 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.12 -(*  DESCRIPTION:
    1.13 -    A notion roughly based on Huet's Zippers for Isabelle terms.
    1.14 -*)   
    1.15 -
    1.16 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    1.17 -
    1.18 -(* abstract term for no more than pattern matching *)
    1.19 -signature ABSTRACT_TRM = 
    1.20 -sig
    1.21 -type typ   (* types *)
    1.22 -type aname (* abstraction names *)
    1.23 -type fname (* parameter/free variable names *)
    1.24 -type cname (* constant names *)
    1.25 -type vname (* meta variable names *)
    1.26 -type bname (* bound var name *)
    1.27 -datatype term = Const of cname * typ
    1.28 -           | Abs of aname * typ * term
    1.29 -           | Free of fname * typ
    1.30 -           | Var of vname * typ
    1.31 -           | Bound of bname
    1.32 -           | $ of term * term;
    1.33 -type T = term;
    1.34 -end;
    1.35 -
    1.36 -structure IsabelleTrmWrap : ABSTRACT_TRM= 
    1.37 -struct 
    1.38 -open Term;
    1.39 -type typ   = Term.typ; (* types *)
    1.40 -type aname = string; (* abstraction names *)
    1.41 -type fname = string; (* parameter/free variable names *)
    1.42 -type cname = string; (* constant names *)
    1.43 -type vname = string * int; (* meta variable names *)
    1.44 -type bname = int; (* bound var name *)
    1.45 -type T = term;
    1.46 -end;
    1.47 -
    1.48 -(* Concrete version for the Trm structure *)
    1.49 -signature TRM_CTXT_DATA = 
    1.50 -sig
    1.51 -
    1.52 -  structure Trm : ABSTRACT_TRM
    1.53 -  datatype dtrm = Abs of Trm.aname * Trm.typ
    1.54 -                | AppL of Trm.T
    1.55 -                | AppR of Trm.T;
    1.56 -  val apply : dtrm -> Trm.T -> Trm.T
    1.57 -  val eq_pos : dtrm * dtrm -> bool
    1.58 -end;
    1.59 -
    1.60 -(* A trm context = list of derivatives *)
    1.61 -signature TRM_CTXT =
    1.62 -sig
    1.63 -  structure D : TRM_CTXT_DATA
    1.64 -  type T = D.dtrm list;
    1.65 -
    1.66 -  val empty : T;
    1.67 -  val is_empty : T -> bool;
    1.68 -
    1.69 -  val add_abs : D.Trm.aname * D.Trm.typ -> T -> T;
    1.70 -  val add_appl : D.Trm.T -> T -> T;
    1.71 -  val add_appr : D.Trm.T -> T -> T;
    1.72 -
    1.73 -  val add_dtrm : D.dtrm -> T -> T;
    1.74 -
    1.75 -  val eq_path : T * T -> bool
    1.76 -
    1.77 -  val add_outerctxt : T -> T -> T
    1.78 -
    1.79 -  val apply : T -> D.Trm.T -> D.Trm.T
    1.80 -
    1.81 -  val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list;
    1.82 -  val ty_ctxt : T -> D.Trm.typ list;
    1.83 -
    1.84 -  val depth : T -> int;
    1.85 -  val map : (D.dtrm -> D.dtrm) -> T -> T
    1.86 -  val fold_up : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
    1.87 -  val fold_down : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
    1.88 -
    1.89 -end;
    1.90 -
    1.91 -(* A zipper = a term looked at, at a particular point in the term *)
    1.92 -signature ZIPPER =
    1.93 -sig
    1.94 -  structure C : TRM_CTXT
    1.95 -  type T
    1.96 -
    1.97 -  val mktop : C.D.Trm.T -> T
    1.98 -  val mk : (C.D.Trm.T * C.T) -> T
    1.99 -
   1.100 -  val goto_top : T -> T 
   1.101 -  val at_top : T -> bool
   1.102 -
   1.103 -  val split : T -> T * C.T
   1.104 -  val add_outerctxt : C.T -> T -> T
   1.105 -
   1.106 -  val set_trm : C.D.Trm.T -> T -> T
   1.107 -  val set_ctxt : C.T -> T -> T
   1.108 -
   1.109 -  val ctxt : T -> C.T
   1.110 -  val trm : T -> C.D.Trm.T
   1.111 -  val top_trm : T -> C.D.Trm.T
   1.112 -
   1.113 -  val zipto : C.T -> T -> T (* follow context down *)
   1.114 -
   1.115 -  val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
   1.116 -  val ty_ctxt : T -> C.D.Trm.typ list;
   1.117 -
   1.118 -  val depth_of_ctxt : T -> int;
   1.119 -  val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T
   1.120 -  val fold_up_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
   1.121 -  val fold_down_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
   1.122 -
   1.123 -  (* searching through a zipper *)
   1.124 -  datatype zsearch = Here of T | LookIn of T;
   1.125 -  (* lazily search through the zipper *)
   1.126 -  val lzy_search : (T -> zsearch list) -> T -> T Seq.seq
   1.127 -  (* lazy search with folded data *)
   1.128 -  val pf_lzy_search : ('a -> T -> ('a * zsearch list)) 
   1.129 -                      -> 'a -> T -> T Seq.seq
   1.130 -  (* zsearch list is or-choices *)
   1.131 -  val searchfold : ('a -> T -> (('a * zsearch) list)) 
   1.132 -                      -> 'a -> T -> ('a * T) Seq.seq
   1.133 -  (* limit function to the current focus of the zipper, 
   1.134 -     but give function the zipper's context *)
   1.135 -  val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq) 
   1.136 -                      -> T -> ('a * T) Seq.seq
   1.137 -  val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq
   1.138 -  val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq
   1.139 -
   1.140 -  (* moving around zippers with option types *)
   1.141 -  val omove_up : T -> T option
   1.142 -  val omove_up_abs : T -> T option
   1.143 -  val omove_up_app : T -> T option
   1.144 -  val omove_up_left : T -> T option
   1.145 -  val omove_up_right : T -> T option
   1.146 -  val omove_up_left_or_abs : T -> T option
   1.147 -  val omove_up_right_or_abs : T -> T option
   1.148 -  val omove_down_abs : T -> T option
   1.149 -  val omove_down_left : T -> T option
   1.150 -  val omove_down_right : T -> T option
   1.151 -  val omove_down_app : T -> (T * T) option
   1.152 -
   1.153 -  (* moving around zippers, raising exceptions *)
   1.154 -  exception move of string * T
   1.155 -  val move_up : T -> T
   1.156 -  val move_up_abs : T -> T
   1.157 -  val move_up_app : T -> T
   1.158 -  val move_up_left : T -> T
   1.159 -  val move_up_right : T -> T
   1.160 -  val move_up_left_or_abs : T -> T
   1.161 -  val move_up_right_or_abs : T -> T
   1.162 -  val move_down_abs : T -> T
   1.163 -  val move_down_left : T -> T
   1.164 -  val move_down_right : T -> T
   1.165 -  val move_down_app : T -> T * T
   1.166 -
   1.167 -end;
   1.168 -
   1.169 -
   1.170 -(* Zipper data for an generic trm *)
   1.171 -functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM) 
   1.172 -: TRM_CTXT_DATA 
   1.173 -= struct
   1.174 -  
   1.175 -  structure Trm = Trm;
   1.176 -
   1.177 -  (* a dtrm is, in McBridge-speak, a differentiated term. It represents
   1.178 -  the different ways a term can occur within its datatype constructors *)
   1.179 -  datatype dtrm = Abs of Trm.aname * Trm.typ
   1.180 -                | AppL of Trm.T
   1.181 -                | AppR of Trm.T;
   1.182 -
   1.183 -  (* apply a dtrm to a term, ie put the dtrm above it, building context *)
   1.184 -  fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)
   1.185 -    | apply (AppL tl) tr = Trm.$ (tl, tr)
   1.186 -    | apply (AppR tr) tl = Trm.$ (tl, tr);
   1.187 -
   1.188 -  fun eq_pos (Abs _, Abs _) = true
   1.189 -    | eq_pos (AppL _, AppL _) = true
   1.190 -    | eq_pos (AppR _, AppR _) = true
   1.191 -    | eq_pos _ = false;
   1.192 -
   1.193 -end;
   1.194 -
   1.195 -
   1.196 -(* functor for making term contexts given term data *)
   1.197 -functor TrmCtxtFUN(D : TRM_CTXT_DATA) 
   1.198 - : TRM_CTXT =
   1.199 -struct 
   1.200 -  structure D = D;
   1.201 -
   1.202 -  type T = D.dtrm list;
   1.203 -
   1.204 -  val empty = [];
   1.205 -  val is_empty = List.null;
   1.206 -
   1.207 -  fun add_abs d l = (D.Abs d) :: l;
   1.208 -  fun add_appl d l = (D.AppL d) :: l;
   1.209 -  fun add_appr d l = (D.AppR d) :: l;
   1.210 -
   1.211 -  fun add_dtrm d l = d::l;
   1.212 -
   1.213 -  fun eq_path ([], []) = true
   1.214 -    | eq_path ([], _::_) = false
   1.215 -    | eq_path ( _::_, []) = false
   1.216 -    | eq_path (h::t, h2::t2) = 
   1.217 -      D.eq_pos(h,h2) andalso eq_path (t, t2);
   1.218 -
   1.219 -  (* add context to outside of existing context *) 
   1.220 -  fun add_outerctxt ctop cbottom = cbottom @ ctop; 
   1.221 -
   1.222 -  (* mkterm : zipper -> trm -> trm *)
   1.223 -  val apply = Basics.fold D.apply;
   1.224 -  
   1.225 -  (* named type context *)
   1.226 -  val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
   1.227 -                             | (_,ntys) => ntys) [];
   1.228 -  (* type context *)
   1.229 -  val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys
   1.230 -                           | (_,tys) => tys) [];
   1.231 -
   1.232 -  val depth = length : T -> int;
   1.233 -
   1.234 -  val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
   1.235 -
   1.236 -  val fold_up = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
   1.237 -  val fold_down = Basics.fold_rev : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
   1.238 -
   1.239 -end;
   1.240 -
   1.241 -(* zippers in terms of term contexts *)
   1.242 -functor ZipperFUN(C : TRM_CTXT) 
   1.243 - : ZIPPER
   1.244 -= struct 
   1.245 -
   1.246 -  structure C = C;
   1.247 -  structure D = C.D;
   1.248 -  structure Trm = D.Trm;
   1.249 -
   1.250 -  type T = C.D.Trm.T * C.T;
   1.251 -
   1.252 -  fun mktop t = (t, C.empty) : T
   1.253 -
   1.254 -  val mk = I;
   1.255 -  fun set_trm x = apfst (K x);
   1.256 -  fun set_ctxt x = apsnd (K x);
   1.257 -
   1.258 -  fun goto_top (z as (t,c)) = 
   1.259 -      if C.is_empty c then z else (C.apply c t, C.empty);
   1.260 -
   1.261 -  fun at_top (_,c) = C.is_empty c;
   1.262 -
   1.263 -  fun split (t,c) = ((t,C.empty) : T, c : C.T) 
   1.264 -  fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T
   1.265 -
   1.266 -  val ctxt = snd;
   1.267 -  val trm = fst;
   1.268 -  val top_trm = trm o goto_top;
   1.269 -
   1.270 -  fun nty_ctxt x = C.nty_ctxt (ctxt x);
   1.271 -  fun ty_ctxt x = C.ty_ctxt (ctxt x);
   1.272 -
   1.273 -  fun depth_of_ctxt x = C.depth (ctxt x);
   1.274 -  fun map_on_ctxt x = apsnd (C.map x);
   1.275 -  fun fold_up_ctxt f = C.fold_up f o ctxt;
   1.276 -  fun fold_down_ctxt f = C.fold_down f o ctxt;
   1.277 -
   1.278 -  fun omove_up (t,(d::c)) = SOME (D.apply d t, c)
   1.279 -    | omove_up (z as (_,[])) = NONE;
   1.280 -  fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)
   1.281 -    | omove_up_abs z = NONE;
   1.282 -  fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
   1.283 -    | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
   1.284 -    | omove_up_app z = NONE;
   1.285 -  fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
   1.286 -    | omove_up_left z = NONE;
   1.287 -  fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
   1.288 -    | omove_up_right _ = NONE;
   1.289 -  fun omove_up_left_or_abs (t,(D.AppL tl)::c) = 
   1.290 -      SOME (Trm.$(tl,t), c)
   1.291 -    | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) = 
   1.292 -      SOME (Trm.Abs(n,ty,t), c)
   1.293 -    | omove_up_left_or_abs z = NONE;
   1.294 -  fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) = 
   1.295 -      SOME (Trm.Abs(n,ty,t), c) 
   1.296 -    | omove_up_right_or_abs (t,(D.AppR tr)::c) = 
   1.297 -      SOME (Trm.$(t,tr), c)
   1.298 -    | omove_up_right_or_abs _ = NONE;
   1.299 -  fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)
   1.300 -    | omove_down_abs _ = NONE;
   1.301 -  fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)
   1.302 -    | omove_down_left _ = NONE;
   1.303 -  fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)
   1.304 -    | omove_down_right _ = NONE;
   1.305 -  fun omove_down_app (Trm.$(l,r),c) = 
   1.306 -      SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
   1.307 -    | omove_down_app _ = NONE;
   1.308 -
   1.309 -  exception move of string * T
   1.310 -  fun move_up (t,(d::c)) = (D.apply d t, c)
   1.311 -    | move_up (z as (_,[])) = raise move ("move_up",z);
   1.312 -  fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)
   1.313 -    | move_up_abs z = raise move ("move_up_abs",z);
   1.314 -  fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
   1.315 -    | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
   1.316 -    | move_up_app z = raise move ("move_up_app",z);
   1.317 -  fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)
   1.318 -    | move_up_left z = raise move ("move_up_left",z);
   1.319 -  fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
   1.320 -    | move_up_right z = raise move ("move_up_right",z);
   1.321 -  fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
   1.322 -    | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
   1.323 -    | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);
   1.324 -  fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c) 
   1.325 -    | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
   1.326 -    | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);
   1.327 -  fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)
   1.328 -    | move_down_abs z = raise move ("move_down_abs",z);
   1.329 -  fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)
   1.330 -    | move_down_left z = raise move ("move_down_left",z);
   1.331 -  fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)
   1.332 -    | move_down_right z = raise move ("move_down_right",z);
   1.333 -  fun move_down_app (Trm.$(l,r),c) = 
   1.334 -      ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
   1.335 -    | move_down_app z = raise move ("move_down_app",z);
   1.336 -
   1.337 -  (* follow the given path down the given zipper *)
   1.338 -  (* implicit arguments: C.D.dtrm list, then T *)
   1.339 -  val zipto = C.fold_down 
   1.340 -                (fn C.D.Abs _ => move_down_abs 
   1.341 -                  | C.D.AppL _ => move_down_right
   1.342 -                  | C.D.AppR _ => move_down_left); 
   1.343 -
   1.344 -  (* Note: interpretted as being examined depth first *)
   1.345 -  datatype zsearch = Here of T | LookIn of T;
   1.346 -
   1.347 -  (* lazy search *)
   1.348 -  fun lzy_search fsearch = 
   1.349 -      let 
   1.350 -        fun lzyl [] () = NONE
   1.351 -          | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
   1.352 -          | lzyl ((LookIn z) :: more) () =
   1.353 -            (case lzy z
   1.354 -              of NONE => NONE
   1.355 -               | SOME (hz,mz) => 
   1.356 -                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
   1.357 -        and lzy z = lzyl (fsearch z) ()
   1.358 -      in Seq.make o lzyl o fsearch end;
   1.359 -
   1.360 -  (* path folded lazy search - the search list is defined in terms of
   1.361 -  the path passed through: the data a is updated with every zipper
   1.362 -  considered *)
   1.363 -  fun pf_lzy_search fsearch a0 z = 
   1.364 -      let 
   1.365 -        fun lzyl a [] () = NONE
   1.366 -          | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
   1.367 -          | lzyl a ((LookIn z) :: more) () =
   1.368 -            (case lzy a z
   1.369 -              of NONE => lzyl a more ()
   1.370 -               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
   1.371 -        and lzy a z = 
   1.372 -            let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
   1.373 -
   1.374 -        val (a,slist) = fsearch a0 z
   1.375 -      in Seq.make (lzyl a slist) end;
   1.376 -
   1.377 -  (* Note: depth first over zsearch results *)
   1.378 -  fun searchfold fsearch a0 z = 
   1.379 -      let 
   1.380 -        fun lzyl [] () = NONE
   1.381 -          | lzyl ((a, Here z) :: more) () = 
   1.382 -            SOME((a,z), Seq.make (lzyl more))
   1.383 -          | lzyl ((a, LookIn z) :: more) () =
   1.384 -            (case lzyl (fsearch a z) () of 
   1.385 -               NONE => lzyl more ()
   1.386 -             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
   1.387 -      in Seq.make (lzyl (fsearch a0 z)) end;
   1.388 -
   1.389 -
   1.390 -  fun limit_pcapply f z = 
   1.391 -      let val (z2,c) = split z
   1.392 -      in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;
   1.393 -  fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) = 
   1.394 -      let val ((z2 : T),(c : C.T)) = split z
   1.395 -      in Seq.map (add_outerctxt c) (f c z2) end
   1.396 -
   1.397 -  val limit_apply = limit_capply o K;
   1.398 -
   1.399 -end;
   1.400 -
   1.401 -(* now build these for Isabelle terms *)
   1.402 -structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);
   1.403 -structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);
   1.404 -structure Zipper = ZipperFUN(TrmCtxt);
   1.405 -
   1.406 -
   1.407 -
   1.408 -(* For searching through Zippers below the current focus...
   1.409 -   KEY for naming scheme:    
   1.410 -
   1.411 -   td = starting at the top down
   1.412 -   lr = going from left to right
   1.413 -   rl = going from right to left
   1.414 -
   1.415 -   bl = starting at the bottom left
   1.416 -   br = starting at the bottom right
   1.417 -   ul = going up then left
   1.418 -   ur = going up then right
   1.419 -   ru = going right then up
   1.420 -   lu = going left then up
   1.421 -*)
   1.422 -signature ZIPPER_SEARCH =
   1.423 -sig
   1.424 -  structure Z : ZIPPER;
   1.425 -  
   1.426 -  val leaves_lr : Z.T -> Z.T Seq.seq
   1.427 -  val leaves_rl : Z.T -> Z.T Seq.seq
   1.428 -
   1.429 -  val all_bl_ru : Z.T -> Z.T Seq.seq
   1.430 -  val all_bl_ur : Z.T -> Z.T Seq.seq
   1.431 -  val all_td_lr : Z.T -> Z.T Seq.seq
   1.432 -  val all_td_rl : Z.T -> Z.T Seq.seq
   1.433 -  
   1.434 -end;
   1.435 -
   1.436 -functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH
   1.437 -= struct
   1.438 -
   1.439 -structure Z = Zipper;
   1.440 -structure C = Z.C;
   1.441 -structure D = C.D; 
   1.442 -structure Trm = D.Trm; 
   1.443 -
   1.444 -fun sf_leaves_lr z = 
   1.445 -    case Z.trm z 
   1.446 -     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
   1.447 -                    Z.LookIn (Z.move_down_right z)]
   1.448 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
   1.449 -      | _ => [Z.Here z];
   1.450 -fun sf_leaves_rl z = 
   1.451 -    case Z.trm z 
   1.452 -     of Trm.$ _ => [Z.LookIn (Z.move_down_right z),
   1.453 -                    Z.LookIn (Z.move_down_left z)]
   1.454 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
   1.455 -      | _ => [Z.Here z];
   1.456 -val leaves_lr = Z.lzy_search sf_leaves_lr;
   1.457 -val leaves_rl = Z.lzy_search sf_leaves_rl;
   1.458 -
   1.459 -
   1.460 -fun sf_all_td_lr z = 
   1.461 -    case Z.trm z 
   1.462 -     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),
   1.463 -                    Z.LookIn (Z.move_down_right z)]
   1.464 -      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
   1.465 -      | _ => [Z.Here z];
   1.466 -fun sf_all_td_rl z = 
   1.467 -    case Z.trm z 
   1.468 -     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),
   1.469 -                    Z.LookIn (Z.move_down_left z)]
   1.470 -      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
   1.471 -      | _ => [Z.Here z];
   1.472 -fun sf_all_bl_ur z = 
   1.473 -    case Z.trm z 
   1.474 -     of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,
   1.475 -                    Z.LookIn (Z.move_down_right z)]
   1.476 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),
   1.477 -                      Z.Here z]
   1.478 -      | _ => [Z.Here z];
   1.479 -fun sf_all_bl_ru z = 
   1.480 -    case Z.trm z 
   1.481 -     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
   1.482 -                    Z.LookIn (Z.move_down_right z), Z.Here z]
   1.483 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]
   1.484 -      | _ => [Z.Here z];
   1.485 -
   1.486 -val all_td_lr = Z.lzy_search sf_all_td_lr;
   1.487 -val all_td_rl = Z.lzy_search sf_all_td_rl;
   1.488 -val all_bl_ur = Z.lzy_search sf_all_bl_ru;
   1.489 -val all_bl_ru = Z.lzy_search sf_all_bl_ur;
   1.490 -
   1.491 -end;
   1.492 -
   1.493 -
   1.494 -structure ZipperSearch = ZipperSearchFUN(Zipper);