src/Provers/IsaPlanner/zipper.ML
author wenzelm
Mon Jun 12 21:19:00 2006 +0200 (2006-06-12)
changeset 19861 620d90091788
parent 19853 cb73c3c367db
child 19871 88e8f6173bab
permissions -rw-r--r--
tuned Seq/Envir/Unify interfaces;
dixon@19835
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
dixon@19835
     2
(*  Title:      Pure/IsaPlanner/zipper.ML
dixon@19835
     3
    ID:		$Id$
dixon@19835
     4
    Author:     Lucas Dixon, University of Edinburgh
dixon@19835
     5
                lucas.dixon@ed.ac.uk
dixon@19835
     6
    Created:    24 Mar 2006
dixon@19835
     7
*)
dixon@19835
     8
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
dixon@19835
     9
(*  DESCRIPTION:
dixon@19835
    10
    A notion roughly based on Huet's Zippers for Isabelle terms.
dixon@19835
    11
*)   
dixon@19835
    12
dixon@19835
    13
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
dixon@19835
    14
dixon@19835
    15
(* abstract term for no more than pattern matching *)
dixon@19835
    16
signature ABSTRACT_TRM = 
dixon@19835
    17
sig
dixon@19835
    18
type typ   (* types *)
dixon@19835
    19
type aname (* abstraction names *)
dixon@19835
    20
type fname (* parameter/free variable names *)
dixon@19835
    21
type cname (* constant names *)
dixon@19835
    22
type vname (* meta variable names *)
dixon@19835
    23
type bname (* bound var name *)
dixon@19835
    24
datatype term = Const of (cname * typ)
dixon@19835
    25
           | Abs of (aname * typ * term)
dixon@19835
    26
           | Free of (fname * typ)
dixon@19835
    27
           | Var of (vname * typ)
dixon@19835
    28
           | Bound of bname
dixon@19835
    29
           | $ of term * term;
dixon@19835
    30
type T = term;
dixon@19835
    31
end;
dixon@19835
    32
dixon@19835
    33
structure IsabelleTrmWrap : ABSTRACT_TRM= 
dixon@19835
    34
struct 
dixon@19835
    35
open Term;
dixon@19835
    36
type typ   = Term.typ; (* types *)
dixon@19835
    37
type aname = string; (* abstraction names *)
dixon@19835
    38
type fname = string; (* parameter/free variable names *)
dixon@19835
    39
type cname = string; (* constant names *)
dixon@19835
    40
type vname = string * int; (* meta variable names *)
dixon@19835
    41
type bname = int; (* bound var name *)
dixon@19835
    42
type T = term;
dixon@19835
    43
end;
dixon@19835
    44
dixon@19835
    45
(* Concrete version for the Trm structure *)
dixon@19835
    46
signature TRM_CTXT_DATA = 
dixon@19835
    47
sig
dixon@19835
    48
dixon@19835
    49
  structure Trm : ABSTRACT_TRM
dixon@19835
    50
  datatype dtrm = Abs of Trm.aname * Trm.typ
dixon@19835
    51
                | AppL of Trm.T
dixon@19835
    52
                | AppR of Trm.T;
dixon@19835
    53
  val apply : dtrm -> Trm.T -> Trm.T
dixon@19835
    54
  val eq_pos : dtrm * dtrm -> bool
dixon@19835
    55
end;
dixon@19835
    56
dixon@19835
    57
(* A trm context = list of derivatives *)
dixon@19835
    58
signature TRM_CTXT =
dixon@19835
    59
sig
dixon@19835
    60
  structure D : TRM_CTXT_DATA
dixon@19835
    61
  type T = D.dtrm list
dixon@19835
    62
dixon@19835
    63
  val empty : T
dixon@19835
    64
  val is_empty : T -> bool
dixon@19835
    65
dixon@19835
    66
  val eq_path : T * T -> bool
dixon@19835
    67
dixon@19835
    68
  val add_outerctxt : T -> T -> T
dixon@19835
    69
dixon@19835
    70
  val apply : T -> D.Trm.T -> D.Trm.T
dixon@19835
    71
dixon@19835
    72
  val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list;
dixon@19835
    73
  val ty_ctxt : T -> D.Trm.typ list;
dixon@19835
    74
dixon@19835
    75
  val depth : T -> int;
dixon@19835
    76
  val map : (D.dtrm -> D.dtrm) -> T -> T
dixon@19835
    77
  val fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
dixon@19835
    78
dixon@19835
    79
end;
dixon@19835
    80
dixon@19835
    81
(* A zipper = a term looked at, at a particular point in the term *)
dixon@19835
    82
signature ZIPPER =
dixon@19835
    83
sig
dixon@19835
    84
  structure C : TRM_CTXT
dixon@19835
    85
  type T
dixon@19835
    86
dixon@19835
    87
  val mktop : C.D.Trm.T -> T
dixon@19835
    88
  val goto_top : T -> T
dixon@19835
    89
  val at_top : T -> bool
dixon@19835
    90
  val mk : (C.D.Trm.T * C.T) -> T
dixon@19835
    91
  val set_trm : C.D.Trm.T -> T -> T
dixon@19835
    92
  val set_ctxt : C.T -> T -> T
dixon@19835
    93
dixon@19835
    94
  val split : T -> T * C.T
dixon@19835
    95
  val add_outerctxt : C.T -> T -> T
dixon@19835
    96
dixon@19835
    97
  val ctxt : T -> C.T
dixon@19835
    98
  val trm : T -> C.D.Trm.T
dixon@19835
    99
dixon@19835
   100
  val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
dixon@19835
   101
  val ty_ctxt : T -> C.D.Trm.typ list;
dixon@19835
   102
dixon@19835
   103
  val depth_of_ctxt : T -> int;
dixon@19835
   104
  val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T
dixon@19835
   105
  val fold_on_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
dixon@19835
   106
dixon@19835
   107
  (* searching through a zipper *)
dixon@19835
   108
  datatype zsearch = Here of T | LookIn of T;
dixon@19835
   109
  (* lazily search through the zipper *)
dixon@19835
   110
  val lzy_search : (T -> zsearch list) -> T -> T Seq.seq
dixon@19835
   111
  (* lazy search with folded data *)
dixon@19835
   112
  val pf_lzy_search : ('a -> T -> ('a * zsearch list)) 
dixon@19835
   113
                      -> 'a -> T -> T Seq.seq
dixon@19835
   114
  (* zsearch list is or-choices *)
dixon@19835
   115
  val searchfold : ('a -> T -> (('a * zsearch) list)) 
dixon@19835
   116
                      -> 'a -> T -> ('a * T) Seq.seq
dixon@19835
   117
  (* limit function to the current focus of the zipper, 
dixon@19835
   118
     but give function the zipper's context *)
dixon@19835
   119
  val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq) 
dixon@19835
   120
                      -> T -> ('a * T) Seq.seq
dixon@19835
   121
  val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq
dixon@19835
   122
  val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq
dixon@19835
   123
dixon@19835
   124
  (* moving around zippers with option types *)
dixon@19835
   125
  val omove_up : T -> T option
dixon@19835
   126
  val omove_up_abs : T -> T option
dixon@19835
   127
  val omove_up_app : T -> T option
dixon@19835
   128
  val omove_up_left : T -> T option
dixon@19835
   129
  val omove_up_right : T -> T option
dixon@19835
   130
  val omove_up_left_or_abs : T -> T option
dixon@19835
   131
  val omove_up_right_or_abs : T -> T option
dixon@19835
   132
  val omove_down_abs : T -> T option
dixon@19835
   133
  val omove_down_left : T -> T option
dixon@19835
   134
  val omove_down_right : T -> T option
dixon@19835
   135
  val omove_down_app : T -> (T * T) option
dixon@19835
   136
dixon@19835
   137
  (* moving around zippers, raising exceptions *)
dixon@19835
   138
  exception move of string * T
dixon@19835
   139
  val move_up : T -> T
dixon@19835
   140
  val move_up_abs : T -> T
dixon@19835
   141
  val move_up_app : T -> T
dixon@19835
   142
  val move_up_left : T -> T
dixon@19835
   143
  val move_up_right : T -> T
dixon@19835
   144
  val move_up_left_or_abs : T -> T
dixon@19835
   145
  val move_up_right_or_abs : T -> T
dixon@19835
   146
  val move_down_abs : T -> T
dixon@19835
   147
  val move_down_left : T -> T
dixon@19835
   148
  val move_down_right : T -> T
dixon@19835
   149
  val move_down_app : T -> T * T
dixon@19835
   150
dixon@19835
   151
end;
dixon@19835
   152
dixon@19835
   153
dixon@19835
   154
(* Zipper data for an generic trm *)
dixon@19835
   155
functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM) 
dixon@19835
   156
: TRM_CTXT_DATA 
dixon@19835
   157
= struct
dixon@19835
   158
  
dixon@19835
   159
  structure Trm = Trm;
dixon@19835
   160
dixon@19835
   161
  (* a dtrm is, in McBridge-speak, a differentiated term. It represents
dixon@19835
   162
  the different ways a term can occur within its datatype constructors *)
dixon@19835
   163
  datatype dtrm = Abs of Trm.aname * Trm.typ
dixon@19835
   164
                | AppL of Trm.T
dixon@19835
   165
                | AppR of Trm.T;
dixon@19835
   166
dixon@19835
   167
  (* apply a dtrm to a term, ie put the dtrm above it, building context *)
dixon@19835
   168
  fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)
dixon@19835
   169
    | apply (AppL tl) tr = Trm.$ (tl, tr)
dixon@19835
   170
    | apply (AppR tr) tl = Trm.$ (tl, tr);
dixon@19835
   171
dixon@19835
   172
  fun eq_pos (Abs _, Abs _) = true
dixon@19835
   173
    | eq_pos (AppL _, AppL _) = true
dixon@19835
   174
    | eq_pos (AppR _, AppR _) = true
dixon@19835
   175
    | eq_pos _ = false;
dixon@19835
   176
dixon@19835
   177
end;
dixon@19835
   178
dixon@19835
   179
dixon@19835
   180
(* functor for making term contexts given term data *)
dixon@19835
   181
functor TrmCtxtFUN(D : TRM_CTXT_DATA) 
dixon@19835
   182
 : TRM_CTXT =
dixon@19835
   183
struct 
dixon@19835
   184
  structure D = D;
dixon@19835
   185
dixon@19835
   186
  type T = D.dtrm list;
dixon@19835
   187
dixon@19835
   188
  val empty = [];
dixon@19835
   189
  val is_empty = List.null;
dixon@19835
   190
dixon@19835
   191
  fun eq_path ([], []) = true
dixon@19835
   192
    | eq_path ([], _::_) = false
dixon@19835
   193
    | eq_path ( _::_, []) = false
dixon@19835
   194
    | eq_path (h::t, h2::t2) = 
dixon@19835
   195
      D.eq_pos(h,h2) andalso eq_path (t, t2);
dixon@19835
   196
dixon@19835
   197
  (* add context to outside of existing context *) 
dixon@19835
   198
  fun add_outerctxt ctop cbottom = cbottom @ ctop; 
dixon@19835
   199
dixon@19835
   200
  (* mkterm : zipper -> trm -> trm *)
dixon@19835
   201
  val apply = Library.fold D.apply;
dixon@19835
   202
  
dixon@19835
   203
  (* named type context *)
dixon@19835
   204
  val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
dixon@19835
   205
                             | (_,ntys) => ntys) [];
dixon@19835
   206
  (* type context *)
dixon@19835
   207
  val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys
dixon@19835
   208
                           | (_,tys) => tys) [];
dixon@19835
   209
dixon@19835
   210
  val depth = length : T -> int;
dixon@19835
   211
dixon@19835
   212
  val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
dixon@19835
   213
dixon@19835
   214
  val fold = Library.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
dixon@19835
   215
dixon@19835
   216
end;
dixon@19835
   217
dixon@19835
   218
(* zippers in terms of term contexts *)
dixon@19835
   219
functor ZipperFUN(C : TRM_CTXT) 
dixon@19835
   220
 : ZIPPER
dixon@19835
   221
= struct 
dixon@19835
   222
dixon@19835
   223
  structure C = C;
dixon@19835
   224
  structure D = C.D;
dixon@19835
   225
  structure Trm = D.Trm;
dixon@19835
   226
dixon@19835
   227
  type T = C.D.Trm.T * C.T;
dixon@19835
   228
dixon@19835
   229
  fun mktop t = (t, C.empty) : T
dixon@19835
   230
dixon@19835
   231
  val mk = I;
wenzelm@19853
   232
  fun set_trm x = apfst (K x);
wenzelm@19853
   233
  fun set_ctxt x = apsnd (K x);
dixon@19835
   234
dixon@19835
   235
  fun goto_top (z as (t,c)) = 
dixon@19835
   236
      if C.is_empty c then z else (C.apply c t, C.empty);
dixon@19835
   237
dixon@19835
   238
  fun at_top (_,c) = C.is_empty c;
dixon@19835
   239
dixon@19835
   240
  fun split (t,c) = ((t,C.empty) : T, c : C.T) 
dixon@19835
   241
  fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T
dixon@19835
   242
dixon@19835
   243
  val ctxt = snd;
dixon@19835
   244
  val trm = fst;
dixon@19835
   245
wenzelm@19853
   246
  fun nty_ctxt x = C.nty_ctxt (ctxt x);
wenzelm@19853
   247
  fun ty_ctxt x = C.ty_ctxt (ctxt x);
dixon@19835
   248
wenzelm@19853
   249
  fun depth_of_ctxt x = C.depth (ctxt x);
wenzelm@19853
   250
  fun map_on_ctxt x = apsnd (C.map x);
dixon@19835
   251
  fun fold_on_ctxt f = C.fold f o ctxt;
dixon@19835
   252
dixon@19835
   253
  fun omove_up (t,(d::c)) = SOME (D.apply d t, c)
dixon@19835
   254
    | omove_up (z as (_,[])) = NONE;
dixon@19835
   255
  fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)
dixon@19835
   256
    | omove_up_abs z = NONE;
dixon@19835
   257
  fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
dixon@19835
   258
    | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
dixon@19835
   259
    | omove_up_app z = NONE;
dixon@19835
   260
  fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
dixon@19835
   261
    | omove_up_left z = NONE;
dixon@19835
   262
  fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
dixon@19835
   263
    | omove_up_right _ = NONE;
dixon@19835
   264
  fun omove_up_left_or_abs (t,(D.AppL tl)::c) = 
dixon@19835
   265
      SOME (Trm.$(tl,t), c)
dixon@19835
   266
    | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) = 
dixon@19835
   267
      SOME (Trm.Abs(n,ty,t), c)
dixon@19835
   268
    | omove_up_left_or_abs z = NONE;
dixon@19835
   269
  fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) = 
dixon@19835
   270
      SOME (Trm.Abs(n,ty,t), c) 
dixon@19835
   271
    | omove_up_right_or_abs (t,(D.AppR tr)::c) = 
dixon@19835
   272
      SOME (Trm.$(t,tr), c)
dixon@19835
   273
    | omove_up_right_or_abs _ = NONE;
dixon@19835
   274
  fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)
dixon@19835
   275
    | omove_down_abs _ = NONE;
dixon@19835
   276
  fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)
dixon@19835
   277
    | omove_down_left _ = NONE;
dixon@19835
   278
  fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)
dixon@19835
   279
    | omove_down_right _ = NONE;
dixon@19835
   280
  fun omove_down_app (Trm.$(l,r),c) = 
dixon@19835
   281
      SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
dixon@19835
   282
    | omove_down_app _ = NONE;
dixon@19835
   283
dixon@19835
   284
  exception move of string * T
dixon@19835
   285
  fun move_up (t,(d::c)) = (D.apply d t, c)
dixon@19835
   286
    | move_up (z as (_,[])) = raise move ("move_up",z);
dixon@19835
   287
  fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)
dixon@19835
   288
    | move_up_abs z = raise move ("move_up_abs",z);
dixon@19835
   289
  fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
dixon@19835
   290
    | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
dixon@19835
   291
    | move_up_app z = raise move ("move_up_app",z);
dixon@19835
   292
  fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)
dixon@19835
   293
    | move_up_left z = raise move ("move_up_left",z);
dixon@19835
   294
  fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
dixon@19835
   295
    | move_up_right z = raise move ("move_up_right",z);
dixon@19835
   296
  fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
dixon@19835
   297
    | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
dixon@19835
   298
    | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);
dixon@19835
   299
  fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c) 
dixon@19835
   300
    | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
dixon@19835
   301
    | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);
dixon@19835
   302
  fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)
dixon@19835
   303
    | move_down_abs z = raise move ("move_down_abs",z);
dixon@19835
   304
  fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)
dixon@19835
   305
    | move_down_left z = raise move ("move_down_left",z);
dixon@19835
   306
  fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)
dixon@19835
   307
    | move_down_right z = raise move ("move_down_right",z);
dixon@19835
   308
  fun move_down_app (Trm.$(l,r),c) = 
dixon@19835
   309
      ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
dixon@19835
   310
    | move_down_app z = raise move ("move_down_app",z);
dixon@19835
   311
dixon@19835
   312
dixon@19835
   313
  (* Note: interpretted as being examined depth first *)
dixon@19835
   314
  datatype zsearch = Here of T | LookIn of T;
dixon@19835
   315
dixon@19835
   316
  fun lzy_search fsearch = 
dixon@19835
   317
      let 
dixon@19835
   318
        fun lzyl [] () = NONE
dixon@19835
   319
          | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
dixon@19835
   320
          | lzyl ((LookIn z) :: more) () =
dixon@19835
   321
            (case lzy z
dixon@19835
   322
              of NONE => NONE
dixon@19835
   323
               | SOME (hz,mz) => 
wenzelm@19861
   324
                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
dixon@19835
   325
        and lzy z = lzyl (fsearch z) ()
dixon@19835
   326
      in Seq.make o lzyl o fsearch end;
dixon@19835
   327
dixon@19835
   328
  (* path folded lazy search - the search list is defined in terms of
dixon@19835
   329
  the path passed through: the data a is updated with every zipper
dixon@19835
   330
  considered *)
dixon@19835
   331
  fun pf_lzy_search fsearch a0 z = 
dixon@19835
   332
      let 
dixon@19835
   333
        fun lzyl a [] () = NONE
dixon@19835
   334
          | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
dixon@19835
   335
          | lzyl a ((LookIn z) :: more) () =
dixon@19835
   336
            (case lzy a z
dixon@19835
   337
              of NONE => lzyl a more ()
wenzelm@19861
   338
               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
dixon@19835
   339
        and lzy a z = 
dixon@19835
   340
            let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
dixon@19835
   341
dixon@19835
   342
        val (a,slist) = fsearch a0 z
dixon@19835
   343
      in Seq.make (lzyl a slist) end;
dixon@19835
   344
dixon@19835
   345
  (* Note: depth first over zsearch results *)
dixon@19835
   346
  fun searchfold fsearch a0 z = 
dixon@19835
   347
      let 
dixon@19835
   348
        fun lzyl [] () = NONE
dixon@19835
   349
          | lzyl ((a, Here z) :: more) () = 
dixon@19835
   350
            SOME((a,z), Seq.make (lzyl more))
dixon@19835
   351
          | lzyl ((a, LookIn z) :: more) () =
dixon@19835
   352
            (case lzyl (fsearch a z) () of 
dixon@19835
   353
               NONE => lzyl more ()
wenzelm@19861
   354
             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
dixon@19835
   355
      in Seq.make (lzyl (fsearch a0 z)) end;
dixon@19835
   356
dixon@19835
   357
dixon@19835
   358
  fun limit_pcapply f z = 
dixon@19835
   359
      let val (z2,c) = split z
dixon@19835
   360
      in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;
dixon@19835
   361
  fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) = 
dixon@19835
   362
      let val ((z2 : T),(c : C.T)) = split z
dixon@19835
   363
      in Seq.map (add_outerctxt c) (f c z2) end
dixon@19835
   364
dixon@19835
   365
  val limit_apply = limit_capply o K;
dixon@19835
   366
dixon@19835
   367
end;
dixon@19835
   368
dixon@19835
   369
(* now build these for Isabelle terms *)
dixon@19835
   370
structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);
dixon@19835
   371
structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);
dixon@19835
   372
structure Zipper = ZipperFUN(TrmCtxt);
dixon@19835
   373
dixon@19835
   374
dixon@19835
   375
dixon@19835
   376
(* For searching through Zippers below the current focus...
dixon@19835
   377
   KEY for naming scheme:    
dixon@19835
   378
dixon@19835
   379
   td = starting at the top down
dixon@19835
   380
   lr = going from left to right
dixon@19835
   381
   rl = going from right to left
dixon@19835
   382
dixon@19835
   383
   bl = starting at the bottom left
dixon@19835
   384
   br = starting at the bottom right
dixon@19835
   385
   ul = going up then left
dixon@19835
   386
   ur = going up then right
dixon@19835
   387
   ru = going right then up
dixon@19835
   388
   lu = going left then up
dixon@19835
   389
*)
dixon@19835
   390
signature ZIPPER_SEARCH =
dixon@19835
   391
sig
dixon@19835
   392
  structure Z : ZIPPER;
dixon@19835
   393
  
dixon@19835
   394
  val leaves_lr : Z.T -> Z.T Seq.seq
dixon@19835
   395
  val leaves_rl : Z.T -> Z.T Seq.seq
dixon@19835
   396
dixon@19835
   397
  val all_bl_ru : Z.T -> Z.T Seq.seq
dixon@19835
   398
  val all_bl_ur : Z.T -> Z.T Seq.seq
dixon@19835
   399
  val all_td_lr : Z.T -> Z.T Seq.seq
dixon@19835
   400
  val all_td_rl : Z.T -> Z.T Seq.seq
dixon@19835
   401
  
dixon@19835
   402
end;
dixon@19835
   403
dixon@19835
   404
functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH
dixon@19835
   405
= struct
dixon@19835
   406
dixon@19835
   407
structure Z = Zipper;
dixon@19835
   408
structure C = Z.C;
dixon@19835
   409
structure D = C.D; 
dixon@19835
   410
structure Trm = D.Trm; 
dixon@19835
   411
dixon@19835
   412
fun sf_leaves_lr z = 
dixon@19835
   413
    case Z.trm z 
dixon@19835
   414
     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
dixon@19835
   415
                    Z.LookIn (Z.move_down_right z)]
dixon@19835
   416
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
dixon@19835
   417
      | _ => [Z.Here z];
dixon@19835
   418
fun sf_leaves_rl z = 
dixon@19835
   419
    case Z.trm z 
dixon@19835
   420
     of Trm.$ _ => [Z.LookIn (Z.move_down_right z),
dixon@19835
   421
                    Z.LookIn (Z.move_down_left z)]
dixon@19835
   422
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
dixon@19835
   423
      | _ => [Z.Here z];
dixon@19835
   424
val leaves_lr = Z.lzy_search sf_leaves_lr;
dixon@19835
   425
val leaves_rl = Z.lzy_search sf_leaves_rl;
dixon@19835
   426
dixon@19835
   427
dixon@19835
   428
fun sf_all_td_lr z = 
dixon@19835
   429
    case Z.trm z 
dixon@19835
   430
     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),
dixon@19835
   431
                    Z.LookIn (Z.move_down_right z)]
dixon@19835
   432
      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
dixon@19835
   433
      | _ => [Z.Here z];
dixon@19835
   434
fun sf_all_td_rl z = 
dixon@19835
   435
    case Z.trm z 
dixon@19835
   436
     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),
dixon@19835
   437
                    Z.LookIn (Z.move_down_left z)]
dixon@19835
   438
      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
dixon@19835
   439
      | _ => [Z.Here z];
dixon@19835
   440
fun sf_all_bl_ur z = 
dixon@19835
   441
    case Z.trm z 
dixon@19835
   442
     of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,
dixon@19835
   443
                    Z.LookIn (Z.move_down_right z)]
dixon@19835
   444
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),
dixon@19835
   445
                      Z.Here z]
dixon@19835
   446
      | _ => [Z.Here z];
dixon@19835
   447
fun sf_all_bl_ru z = 
dixon@19835
   448
    case Z.trm z 
dixon@19835
   449
     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
dixon@19835
   450
                    Z.LookIn (Z.move_down_right z), Z.Here z]
dixon@19835
   451
      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]
dixon@19835
   452
      | _ => [Z.Here z];
dixon@19835
   453
dixon@19835
   454
val all_td_lr = Z.lzy_search sf_all_td_lr;
dixon@19835
   455
val all_td_rl = Z.lzy_search sf_all_td_lr;
dixon@19835
   456
val all_bl_ur = Z.lzy_search sf_all_bl_ru;
dixon@19835
   457
val all_bl_ru = Z.lzy_search sf_all_bl_ur;
dixon@19835
   458
dixon@19835
   459
end;
dixon@19835
   460
dixon@19835
   461
dixon@19835
   462
structure ZipperSearch = ZipperSearchFUN(Zipper);