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