author | wenzelm |
Thu, 02 Jun 2005 09:11:32 +0200 | |
changeset 16179 | fa7e70be26b0 |
parent 15814 | d65f461c8672 |
child 17044 | 94d38d9fac40 |
permissions | -rw-r--r-- |
15481 | 1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
16179 | 2 |
(* Title: Pure/IsaPlanner/focus_term_lib.ML |
3 |
ID: $Id$ |
|
15481 | 4 |
Author: Lucas Dixon, University of Edinburgh |
5 |
lucasd@dai.ed.ac.uk |
|
6 |
Date: 16 April 2003 |
|
7 |
*) |
|
8 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
9 |
(* DESCRIPTION: |
|
10 |
||
11 |
Generic Foucs terms (like Zippers), which allows modification and |
|
12 |
manipulation of term keeping track of how we got to the position |
|
13 |
in the term. We provide a signature for terms, ie any kind of |
|
14 |
lamda calculus with abs and application, and some notion of types |
|
15 |
and naming of abstracted vars. |
|
16 |
||
17 |
FIXME: at some point in the future make a library to work simply |
|
18 |
with polymorphic upterms - that way if I want to use them without |
|
19 |
the focus part, then I don't need to include all the focus stuff. |
|
20 |
||
21 |
*) |
|
22 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
23 |
||
24 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
25 |
||
26 |
(* to endoce and decode general terms into the type needed by focus |
|
27 |
term, this is an easy thing to write, but needs to be done for each |
|
28 |
type that is going to be used with focus terms. *) |
|
29 |
||
30 |
signature F_ENCODE_TERM_SIG = |
|
31 |
sig |
|
32 |
||
33 |
type term (* type of term to be encoded into TermT for focus term manip *) |
|
34 |
type TypeT (* type annotation for abstractions *) |
|
35 |
type LeafT (* type for other leaf types in term sturcture *) |
|
36 |
||
37 |
(* the type to be encoded into *) |
|
15632
bb178a7a69c1
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
gagern
parents:
15531
diff
changeset
|
38 |
datatype TermT = op $ of TermT * TermT |
15481 | 39 |
| Abs of string * TypeT * TermT |
40 |
| lf of LeafT |
|
41 |
||
42 |
(* the encode and decode functions *) |
|
43 |
val fakebounds : string * TypeT -> term -> term |
|
44 |
val encode : term -> TermT |
|
45 |
val decode : TermT -> term |
|
46 |
||
47 |
end; |
|
48 |
||
49 |
||
50 |
||
51 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
52 |
signature FOCUS_TERM_SIG = |
|
53 |
sig |
|
54 |
structure MinTermS : F_ENCODE_TERM_SIG |
|
55 |
||
56 |
exception focus_term_exp of string; |
|
57 |
exception out_of_term_exception of string; |
|
58 |
||
59 |
type Term = MinTermS.TermT; |
|
60 |
type Type = MinTermS.TypeT; |
|
61 |
||
62 |
type UpTerm = (Term,Type) UpTermLib.T; |
|
63 |
||
64 |
(* datatype |
|
65 |
UpTerm = |
|
66 |
abs of string * Type * UpTerm |
|
67 |
| appl of Term * UpTerm |
|
68 |
| appr of Term * UpTerm |
|
69 |
| root *) |
|
70 |
||
71 |
datatype FcTerm = focus of Term * UpTerm |
|
72 |
||
73 |
(* translating *) |
|
74 |
val fcterm_of_term : MinTermS.term -> FcTerm |
|
75 |
val term_of_fcterm : FcTerm -> MinTermS.term |
|
76 |
||
77 |
(* editing/constrution *) |
|
78 |
val enc_appl : (MinTermS.term * UpTerm) -> UpTerm |
|
79 |
val enc_appr : (MinTermS.term * UpTerm) -> UpTerm |
|
80 |
||
81 |
(* upterm creatioin *) |
|
82 |
val upterm_of : FcTerm -> UpTerm |
|
83 |
val add_upterm : UpTerm -> FcTerm -> FcTerm |
|
84 |
val mk_term_of_upterm : (MinTermS.term * UpTerm) -> MinTermS.term |
|
85 |
val mk_termf_of_upterm : UpTerm -> |
|
86 |
(((string * Type) list) * |
|
87 |
(MinTermS.term -> MinTermS.term)) |
|
88 |
val pure_mk_termf_of_upterm : (MinTermS.term, Type) UpTermLib.T -> |
|
89 |
(((string * Type) list) * |
|
90 |
(MinTermS.term -> MinTermS.term)) |
|
91 |
||
92 |
(* focusing, throws exceptions *) |
|
93 |
val focus_bot_left_leaf : FcTerm -> FcTerm |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
94 |
val focus_bot_left_nonabs_leaf : FcTerm -> FcTerm |
15481 | 95 |
val focus_left : FcTerm -> FcTerm |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
96 |
val focus_strict_left : FcTerm -> FcTerm |
15481 | 97 |
val focus_right : FcTerm -> FcTerm |
98 |
val focus_abs : FcTerm -> FcTerm |
|
99 |
val focus_fake_abs : FcTerm -> FcTerm |
|
100 |
val focus_to_top : FcTerm -> FcTerm |
|
101 |
val focus_up : FcTerm -> FcTerm |
|
102 |
val focus_up_right : FcTerm -> FcTerm |
|
103 |
val focus_up_right1 : FcTerm -> FcTerm |
|
104 |
||
105 |
(* optional focus changes *) |
|
106 |
val focus_up_abs : FcTerm -> FcTerm option |
|
107 |
val focus_up_appr : FcTerm -> FcTerm option |
|
108 |
val focus_up_appl : FcTerm -> FcTerm option |
|
109 |
val focus_up_abs_or_appr : FcTerm -> FcTerm option |
|
110 |
||
111 |
val tyenv_of_focus : FcTerm -> (string * Type) list |
|
112 |
val tyenv_of_focus' : FcTerm -> Type list |
|
113 |
||
114 |
(* set/get the focus term *) |
|
115 |
val set_focus_of_fcterm : FcTerm -> MinTermS.term -> FcTerm |
|
116 |
val focus_of_fcterm : FcTerm -> MinTermS.term |
|
117 |
||
118 |
(* leaf navigation *) |
|
119 |
val leaf_seq_of_fcterm : FcTerm -> FcTerm Seq.seq |
|
120 |
val next_leaf_fcterm : FcTerm -> FcTerm |
|
121 |
val next_leaf_of_fcterm_seq : FcTerm -> FcTerm Seq.seq |
|
122 |
||
123 |
(* analysis *) |
|
124 |
val upsize_of_fcterm : FcTerm -> int |
|
125 |
val pretty_fcterm : FcTerm -> Pretty.T |
|
126 |
end; |
|
127 |
||
128 |
||
129 |
||
130 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
131 |
(* |
|
132 |
||
133 |
NOTE!!! I think this can be done in a purely functional way with a |
|
134 |
pair of a term (the focus) and a function, that when applied |
|
135 |
unfocuses one level... maybe think about this as it would be a very |
|
136 |
nice generic consrtuction, without the need for encoding/decoding |
|
137 |
strutcures. |
|
138 |
||
139 |
*) |
|
140 |
functor FocusTermFUN(structure EncodeTerm : F_ENCODE_TERM_SIG) |
|
141 |
: FOCUS_TERM_SIG = |
|
142 |
struct |
|
143 |
||
144 |
structure MinTermS = EncodeTerm; |
|
145 |
||
146 |
local open MinTermS open UpTermLib in |
|
147 |
||
148 |
type Term = MinTermS.TermT; |
|
149 |
type Type = MinTermS.TypeT; |
|
150 |
||
151 |
exception focus_term_exp of string; |
|
152 |
exception out_of_term_exception of string; |
|
153 |
||
154 |
infix 9 $ |
|
155 |
||
156 |
(* datatype to hold a term tree and the path to where you are in the term *) |
|
157 |
(* datatype UpTerm = root |
|
158 |
| appl of (Term * UpTerm) |
|
159 |
| appr of (Term * UpTerm) |
|
160 |
| abs of (string * Type * UpTerm); *) |
|
161 |
||
162 |
type UpTerm = (Term,Type) UpTermLib.T; |
|
163 |
||
164 |
fun enc_appl (t,u) = appl((MinTermS.encode t),u); |
|
165 |
fun enc_appr (t,u) = appr((MinTermS.encode t),u); |
|
166 |
||
167 |
datatype FcTerm = focus of (Term * UpTerm); |
|
168 |
||
169 |
(* the the term of the upterm *) |
|
170 |
fun mk_term_of_upt_aux (t, root) = MinTermS.decode t |
|
171 |
| mk_term_of_upt_aux (t, appl (l,m)) = mk_term_of_upt_aux(l$t, m) |
|
172 |
| mk_term_of_upt_aux (t, appr (r,m)) = mk_term_of_upt_aux(t$r, m) |
|
173 |
| mk_term_of_upt_aux (t, abs (s,ty,m)) = mk_term_of_upt_aux(Abs(s,ty,t),m); |
|
174 |
||
175 |
fun mk_term_of_upterm (t, ut) = mk_term_of_upt_aux (MinTermS.encode t, ut); |
|
176 |
||
177 |
(* a function version of the above, given an upterm it returns: |
|
178 |
a function on that given a term puts it in the context of the upterm, |
|
179 |
and a list of bound variables that are in the upterm, added as |
|
180 |
we go up - so in reverse order from that typiclaly used by top-down |
|
181 |
parsing of terms. *) |
|
182 |
fun mk_termf_of_upt_aux (f, bs, root) = |
|
183 |
(bs, fn t => MinTermS.decode (f t)) |
|
184 |
| mk_termf_of_upt_aux (f, bs, appl (l,m)) = |
|
185 |
mk_termf_of_upt_aux (fn t => l $ (f t), bs, m) |
|
186 |
| mk_termf_of_upt_aux (f, bs, appr (r,m)) = |
|
187 |
mk_termf_of_upt_aux (fn t => (f t) $ r, bs, m) |
|
188 |
| mk_termf_of_upt_aux (f, bs, abs (s,ty,m)) = |
|
189 |
mk_termf_of_upt_aux (fn t => Abs(s,ty,(f t)), (s,ty)::bs, m); |
|
190 |
||
191 |
fun mk_termf_of_upterm ut = mk_termf_of_upt_aux (MinTermS.encode, [], ut); |
|
192 |
||
193 |
||
194 |
fun upterm_of (focus(t, u)) = u; |
|
195 |
||
196 |
(* put a new upterm at the start of our current term *) |
|
197 |
fun add_upterm u2 (focus(t, u)) = focus(t, UpTermLib.apply u2 u); |
|
198 |
||
199 |
||
200 |
(* As above but work on the pure originial upterm type *) |
|
201 |
fun pure_mk_termf_of_upterm ut = |
|
202 |
mk_termf_of_upt_aux |
|
203 |
(encode, [], (map_to_upterm_parts (encode, I) ut)); |
|
204 |
||
205 |
fun fcterm_of_term t = focus(encode t, root); |
|
206 |
||
207 |
fun term_of_fcterm (focus (t, m)) = mk_term_of_upt_aux (t, m); |
|
208 |
||
209 |
(* fun term_of_fcterm (focus (t, root)) = mk_term_of_upt_aux (t, root) |
|
210 |
| term_of_fcterm _ = raise focus_term_exp "term_of_fcterm: something bad has happened here."; *) |
|
211 |
||
212 |
fun focus_of_fcterm (focus(t, _)) = MinTermS.decode t; |
|
213 |
||
214 |
(* replace the focus term with a new term... *) |
|
215 |
fun set_focus_of_fcterm (focus(_, m)) nt = focus(MinTermS.encode nt, m); |
|
216 |
||
217 |
fun focus_left (focus(a $ b, m)) = focus(a, appr(b, m)) |
|
218 |
| focus_left (focus(Abs(s,ty,t), m)) = focus_left (focus(t, abs(s,ty,m))) |
|
219 |
| focus_left (focus(l, m)) = raise out_of_term_exception "focus_left"; |
|
220 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
221 |
fun focus_strict_left (focus(a $ b, m)) = focus(a, appr(b, m)) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
222 |
| focus_strict_left (focus(l, m)) = raise out_of_term_exception "focus_left"; |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
223 |
|
15481 | 224 |
(* Note: ":" is standard for faked bound vars... see: EQStepTacTermTools *) |
225 |
fun focus_fake_abs (focus(Abs(s,ty,t), m)) = |
|
226 |
let val t' = MinTermS.encode (fakebounds (s,ty) (MinTermS.decode t)) |
|
227 |
in focus(t', abs(s,ty,m)) end |
|
228 |
| focus_fake_abs (focus(l, m)) = raise out_of_term_exception "focus_fake_abs"; |
|
229 |
||
230 |
fun focus_abs (focus(Abs(s,ty,t), m)) = focus(t, abs(s,ty,m)) |
|
231 |
| focus_abs (focus(l, m)) = raise out_of_term_exception "focus_abs"; |
|
232 |
||
233 |
||
234 |
fun focus_right (focus(a $ b, m)) = focus(b, appl(a, m)) |
|
235 |
| focus_right (focus(Abs(s,ty,t), m)) = focus_right (focus(t, abs(s,ty,m))) |
|
236 |
| focus_right (focus(l, m)) = raise out_of_term_exception "focus_right"; |
|
237 |
||
238 |
fun focus_up (focus(t, appl(l,m))) = focus(l$t, m) |
|
239 |
| focus_up (focus(t, appr(r,m))) = focus(t$r, m) |
|
240 |
| focus_up (focus(t, abs(s,ty,m))) = focus_up (focus(Abs(s,ty,t), m)) |
|
241 |
| focus_up (focus(t, root)) = raise out_of_term_exception "focus_up"; |
|
242 |
||
243 |
fun focus_to_top t = |
|
244 |
focus_to_top (focus_up t) handle out_of_term_exception _ => t; |
|
245 |
||
246 |
(* focus up until you can move right, and then do so *) |
|
247 |
fun focus_up_right (focus(t, appl(l,m))) = |
|
248 |
focus_up_right (focus(l$t, m)) |
|
249 |
| focus_up_right (focus(t, appr(r,m))) = |
|
250 |
focus(r, appl(t,m)) |
|
251 |
| focus_up_right (focus(t, abs(s,ty,m))) = |
|
252 |
focus_up_right (focus(Abs(s,ty,t), m)) |
|
253 |
| focus_up_right (focus(t, root)) = |
|
254 |
raise out_of_term_exception "focus_up_right"; |
|
255 |
||
256 |
(* as above, but do not move up over a left application *) |
|
257 |
fun focus_up_right1 (focus(t, appl(l,m))) = |
|
258 |
raise out_of_term_exception "focus_up_right1" |
|
259 |
| focus_up_right1 (focus(t, appr(r,m))) = |
|
260 |
focus(r, appl(t,m)) |
|
261 |
| focus_up_right1 (focus(t, abs(s,ty,m))) = |
|
262 |
focus_up_right (focus(Abs(s,ty,t), m)) |
|
263 |
| focus_up_right1 (focus(t, root)) = |
|
264 |
raise out_of_term_exception "focus_up_right1"; |
|
265 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
266 |
(* move focus to the bottom left through abstractions *) |
15481 | 267 |
fun focus_bot_left_leaf (ft as focus(t, _)) = |
268 |
focus_bot_left_leaf (focus_left ft) |
|
269 |
handle out_of_term_exception _=> ft; |
|
270 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
271 |
(* move focus to the bottom left, but not into abstractions *) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
272 |
fun focus_bot_left_nonabs_leaf (ft as focus(t, _)) = |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
273 |
focus_bot_left_nonabs_leaf (focus_strict_left ft) |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
274 |
handle out_of_term_exception _=> ft; |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15632
diff
changeset
|
275 |
|
15481 | 276 |
(* focus tools for working directly with the focus representation *) |
15531 | 277 |
fun focus_up_appr (focus(t, appl(l,m))) = NONE |
278 |
| focus_up_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m)) |
|
279 |
| focus_up_appr (focus(t, abs(s,ty,m))) = NONE |
|
280 |
| focus_up_appr (focus(t, root)) = NONE; |
|
15481 | 281 |
|
15531 | 282 |
fun focus_up_appl (focus(t, appl(l,m))) = SOME (focus(l$t, m)) |
283 |
| focus_up_appl (focus(t, appr(r,m))) = NONE |
|
284 |
| focus_up_appl (focus(t, abs(s,ty,m))) = NONE |
|
285 |
| focus_up_appl (focus(t, root)) = NONE; |
|
15481 | 286 |
|
15531 | 287 |
fun focus_up_abs (focus(t, appl(l,m))) = NONE |
288 |
| focus_up_abs (focus(t, appr(r,m))) = NONE |
|
15481 | 289 |
| focus_up_abs (focus(t, abs(s,ty,m))) = |
15531 | 290 |
SOME (focus_up (focus(Abs(s,ty,t), m))) |
291 |
| focus_up_abs (focus(t, root)) = NONE; |
|
15481 | 292 |
|
15531 | 293 |
fun focus_up_abs_or_appr (focus(t, appl(l,m))) = NONE |
294 |
| focus_up_abs_or_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m)) |
|
15481 | 295 |
| focus_up_abs_or_appr (focus(t, abs(s,ty,m))) = |
15531 | 296 |
SOME (focus_up (focus(Abs(s,ty,t), m))) |
297 |
| focus_up_abs_or_appr (focus(t, root)) = NONE; |
|
15481 | 298 |
|
299 |
||
300 |
fun tyenv_of_focus (focus(t, u)) = tyenv_of_upterm u; |
|
301 |
fun tyenv_of_focus' (focus(t, u)) = tyenv_of_upterm' u; |
|
302 |
||
303 |
(* return the Term.type of the focus term, computes bound vars type, |
|
304 |
does a quick check only. *) |
|
305 |
(* fun fastype_of_focus (focus(t, m)) = |
|
306 |
let |
|
307 |
fun boundtypes_of_upterm (abs(s,ty,m)) = |
|
308 |
ty::(boundtypes_of_upterm m) |
|
309 |
| boundtypes_of_upterm (appl(t,m)) = |
|
310 |
boundtypes_of_upterm m |
|
311 |
| boundtypes_of_upterm (appr(t,m)) = |
|
312 |
boundtypes_of_upterm m |
|
313 |
| boundtypes_of_upterm (root) = [] |
|
314 |
in |
|
315 |
fastype_of1 ((boundtypes_of_upterm m), t) |
|
316 |
end; *) |
|
317 |
||
318 |
(* gets the next left hand side term, or throws an exception *) |
|
319 |
fun next_leaf_fcterm ft = focus_bot_left_leaf (focus_up_right ft); |
|
320 |
||
321 |
fun next_leaf_of_fcterm_seq_aux t () = |
|
322 |
let val nextt = next_leaf_fcterm t |
|
323 |
in |
|
15531 | 324 |
SOME (nextt, Seq.make (next_leaf_of_fcterm_seq_aux nextt)) |
325 |
end handle out_of_term_exception _ => NONE; |
|
15481 | 326 |
|
327 |
(* sequence of next upterms from start upterm... |
|
328 |
ie a sequence of all leafs after this one*) |
|
329 |
fun next_leaf_of_fcterm_seq in_t = |
|
330 |
Seq.make (next_leaf_of_fcterm_seq_aux in_t); |
|
331 |
||
332 |
(* returns a sequence of all leaf up terms from term, ie DFS on |
|
333 |
leafs of term, ie uses time O(n), n = sizeof term. *) |
|
334 |
fun leaf_seq_of_fcterm in_t = |
|
335 |
let |
|
336 |
val botleft = (focus_bot_left_leaf in_t) |
|
337 |
in |
|
338 |
Seq.cons (botleft, (Seq.make (next_leaf_of_fcterm_seq_aux botleft)) ) |
|
339 |
end; |
|
340 |
||
341 |
||
342 |
fun upsize_of_fcterm (focus(t, ut)) = upsize_of_upterm ut; |
|
343 |
||
344 |
fun pretty_fcterm ft = Pretty.str "no yet implemented"; |
|
345 |
||
346 |
end; (* local *) |
|
347 |
||
348 |
end; (* functor *) |
|
349 |
||
350 |
||
351 |
||
352 |
||
353 |
||
354 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
355 |
(* focus term encoding sturcture for isabelle terms *) |
|
356 |
structure EncodeIsaFTerm : F_ENCODE_TERM_SIG = |
|
357 |
struct |
|
358 |
infix 9 $; |
|
359 |
||
360 |
type term = Term.term; |
|
361 |
||
362 |
type TypeT = Term.typ; |
|
363 |
||
364 |
datatype LeafT = lConst of string * Term.typ |
|
365 |
| lVar of ((string * int) * Term.typ) |
|
366 |
| lFree of (string * Term.typ) |
|
367 |
| lBound of int; |
|
368 |
||
369 |
datatype TermT = op $ of TermT * TermT |
|
370 |
| Abs of string * TypeT * TermT |
|
371 |
| lf of LeafT; |
|
372 |
||
373 |
fun fakebounds (s, ty) t = subst_bound (Free(":" ^ s, ty), t); |
|
374 |
||
375 |
fun encode (Term.$(a,b)) = (encode a) $ (encode b) |
|
376 |
| encode (Term.Abs(s,ty,t)) = Abs(s,ty,(encode t)) |
|
377 |
| encode (Term.Const(s,ty)) = lf(lConst(s,ty)) |
|
378 |
| encode (Term.Var((s,i),ty)) = lf(lVar((s,i),ty)) |
|
379 |
| encode (Term.Free(s,ty)) = lf(lFree(s,ty)) |
|
380 |
| encode (Term.Bound i) = lf(lBound i); |
|
381 |
||
382 |
fun decode (a $ b) = Term.$(decode a, decode b) |
|
383 |
| decode (Abs(s,ty,t)) = (Term.Abs(s,ty,decode t)) |
|
384 |
| decode (lf(lConst(s,ty))) = Term.Const(s,ty) |
|
385 |
| decode (lf(lVar((s,i),ty))) = Term.Var((s,i),ty) |
|
386 |
| decode (lf(lFree(s,ty))) = (Term.Free(s,ty)) |
|
387 |
| decode (lf(lBound i)) = (Term.Bound i); |
|
388 |
||
389 |
end; |
|
390 |