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