author | wenzelm |
Fri, 17 Jul 2009 21:33:00 +0200 | |
changeset 32031 | e2e6b0691264 |
parent 32018 | 3370cea95387 |
child 32034 | 70c0bcd0adfb |
permissions | -rw-r--r-- |
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
1 |
(* Title: Pure/envir.ML |
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
10485 | 3 |
|
32031 | 4 |
Free-form environments. The type of a term variable / sort of a type variable is |
5 |
part of its name. The lookup function must apply type substitutions, |
|
15797 | 6 |
since they may change the identity of a variable. |
0 | 7 |
*) |
8 |
||
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
9 |
signature ENVIR = |
0 | 10 |
sig |
32018 | 11 |
type tenv = (typ * term) Vartab.table |
32031 | 12 |
datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv} |
13 |
val maxidx_of: env -> int |
|
14 |
val term_env: env -> tenv |
|
15797 | 15 |
val type_env: env -> Type.tyenv |
32031 | 16 |
val is_empty: env -> bool |
17 |
val empty: int -> env |
|
18 |
val merge: env * env -> env |
|
26638 | 19 |
val insert_sorts: env -> sort list -> sort list |
10485 | 20 |
val genvars: string -> env * typ list -> env * term list |
21 |
val genvar: string -> env * typ -> env * term |
|
15797 | 22 |
val lookup: env * (indexname * typ) -> term option |
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
23 |
val lookup': tenv * (indexname * typ) -> term option |
15797 | 24 |
val update: ((indexname * typ) * term) * env -> env |
19861 | 25 |
val above: env -> int -> bool |
15797 | 26 |
val vupdate: ((indexname * typ) * term) * env -> env |
32018 | 27 |
val norm_type_same: Type.tyenv -> typ Same.operation |
28 |
val norm_types_same: Type.tyenv -> typ list Same.operation |
|
15797 | 29 |
val norm_type: Type.tyenv -> typ -> typ |
32018 | 30 |
val norm_term_same: env -> term Same.operation |
31 |
val norm_term: env -> term -> term |
|
10485 | 32 |
val beta_norm: term -> term |
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
33 |
val head_norm: env -> term -> term |
18937 | 34 |
val eta_contract: term -> term |
35 |
val beta_eta_contract: term -> term |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
36 |
val fastype: env -> typ list -> term -> typ |
15797 | 37 |
val typ_subst_TVars: Type.tyenv -> typ -> typ |
38 |
val subst_TVars: Type.tyenv -> term -> term |
|
39 |
val subst_Vars: tenv -> term -> term |
|
40 |
val subst_vars: Type.tyenv * tenv -> term -> term |
|
19422 | 41 |
val expand_atom: typ -> typ * term -> term |
21695 | 42 |
val expand_term: (term -> (typ * term) option) -> term -> term |
21795 | 43 |
val expand_term_frees: ((string * typ) * term) list -> term -> term |
0 | 44 |
end; |
45 |
||
32031 | 46 |
structure Envir: ENVIR = |
0 | 47 |
struct |
48 |
||
32031 | 49 |
(** datatype env **) |
50 |
||
51 |
(*Updating can destroy environment in 2 ways! |
|
52 |
(1) variables out of range |
|
53 |
(2) circular assignments |
|
0 | 54 |
*) |
32031 | 55 |
|
32018 | 56 |
type tenv = (typ * term) Vartab.table; |
15797 | 57 |
|
0 | 58 |
datatype env = Envir of |
32031 | 59 |
{maxidx: int, (*upper bound of maximum index of vars*) |
60 |
tenv: tenv, (*assignments to Vars*) |
|
61 |
tyenv: Type.tyenv}; (*assignments to TVars*) |
|
62 |
||
63 |
fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv}; |
|
64 |
fun map_env f (Envir {maxidx, tenv, tyenv}) = make_env (f (maxidx, tenv, tyenv)); |
|
65 |
||
66 |
fun maxidx_of (Envir {maxidx, ...}) = maxidx; |
|
67 |
fun term_env (Envir {tenv, ...}) = tenv; |
|
68 |
fun type_env (Envir {tyenv, ...}) = tyenv; |
|
69 |
||
70 |
fun is_empty env = |
|
71 |
Vartab.is_empty (term_env env) andalso |
|
72 |
Vartab.is_empty (type_env env); |
|
0 | 73 |
|
32031 | 74 |
|
75 |
(* build env *) |
|
76 |
||
77 |
fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty); |
|
0 | 78 |
|
32031 | 79 |
fun merge |
80 |
(Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1}, |
|
81 |
Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) = |
|
82 |
make_env (Int.max (maxidx1, maxidx2), |
|
83 |
Vartab.merge (op =) (tenv1, tenv2), |
|
84 |
Vartab.merge (op =) (tyenv1, tyenv2)); |
|
85 |
||
86 |
||
87 |
(*NB: type unification may invent new sorts*) (* FIXME tenv!? *) |
|
26638 | 88 |
val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env; |
89 |
||
0 | 90 |
(*Generate a list of distinct variables. |
91 |
Increments index to make them distinct from ALL present variables. *) |
|
32031 | 92 |
fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list = |
32018 | 93 |
let |
94 |
fun genvs (_, [] : typ list) : term list = [] |
|
95 |
| genvs (n, [T]) = [Var ((name, maxidx + 1), T)] |
|
96 |
| genvs (n, T :: Ts) = |
|
97 |
Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T) |
|
98 |
:: genvs (n + 1, Ts); |
|
32031 | 99 |
in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end; |
0 | 100 |
|
101 |
(*Generate a variable.*) |
|
32018 | 102 |
fun genvar name (env, T) : env * term = |
103 |
let val (env', [v]) = genvars name (env, [T]) |
|
104 |
in (env', v) end; |
|
0 | 105 |
|
32031 | 106 |
fun var_clash xi T T' = |
107 |
raise TYPE ("Variable " ^ quote (Term.string_of_vname xi) ^ " has two distinct types", |
|
32018 | 108 |
[T', T], []); |
0 | 109 |
|
32031 | 110 |
fun lookup_check check tenv (xi, T) = |
111 |
(case Vartab.lookup tenv xi of |
|
32018 | 112 |
NONE => NONE |
32031 | 113 |
| SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U); |
15797 | 114 |
|
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
115 |
(* When dealing with environments produced by matching instead *) |
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
116 |
(* of unification, there is no need to chase assigned TVars. *) |
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
117 |
(* In this case, we can simply ignore the type substitution *) |
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
118 |
(* and use = instead of eq_type. *) |
15797 | 119 |
|
32031 | 120 |
fun lookup' (tenv, p) = lookup_check (op =) tenv p; |
15797 | 121 |
|
32031 | 122 |
fun lookup2 (tyenv, tenv) = |
123 |
lookup_check (Type.eq_type tyenv) tenv; |
|
15797 | 124 |
|
32031 | 125 |
fun lookup (Envir {tenv, tyenv, ...}, p) = lookup2 (tyenv, tenv) p; |
0 | 126 |
|
32031 | 127 |
fun update (((xi, T), t), Envir {maxidx, tenv, tyenv}) = |
128 |
Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv}; |
|
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
129 |
|
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset
|
130 |
(*Determine if the least index updated exceeds lim*) |
32031 | 131 |
fun above (Envir {tenv, tyenv, ...}) lim = |
132 |
(case Vartab.min_key tenv of SOME (_, i) => i > lim | NONE => true) andalso |
|
133 |
(case Vartab.min_key tyenv of SOME (_, i) => i > lim | NONE => true); |
|
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
134 |
|
0 | 135 |
(*Update, checking Var-Var assignments: try to suppress higher indexes*) |
32031 | 136 |
fun vupdate ((aU as (a, U), t), env as Envir {tyenv, ...}) = |
137 |
(case t of |
|
138 |
Var (nT as (name', T)) => |
|
139 |
if a = name' then env (*cycle!*) |
|
140 |
else if TermOrd.indexname_ord (a, name') = LESS then |
|
141 |
(case lookup (env, nT) of (*if already assigned, chase*) |
|
142 |
NONE => update ((nT, Var (a, T)), env) |
|
143 |
| SOME u => vupdate ((aU, u), env)) |
|
144 |
else update ((aU, t), env) |
|
145 |
| _ => update ((aU, t), env)); |
|
0 | 146 |
|
147 |
||
148 |
||
32031 | 149 |
(** beta normalization wrt. environment **) |
0 | 150 |
|
32031 | 151 |
(*Chases variables in env. Does not exploit sharing of variable bindings |
152 |
Does not check types, so could loop.*) |
|
1500 | 153 |
|
32018 | 154 |
local |
155 |
||
32031 | 156 |
fun norm_type0 tyenv : typ Same.operation = |
32018 | 157 |
let |
158 |
fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts) |
|
159 |
| norm (TFree _) = raise Same.SAME |
|
160 |
| norm (TVar v) = |
|
32031 | 161 |
(case Type.lookup tyenv v of |
32018 | 162 |
SOME U => Same.commit norm U |
163 |
| NONE => raise Same.SAME); |
|
164 |
in norm end; |
|
0 | 165 |
|
32031 | 166 |
fun norm_term1 tenv : term Same.operation = |
32018 | 167 |
let |
168 |
fun norm (Var v) = |
|
32031 | 169 |
(case lookup' (tenv, v) of |
32018 | 170 |
SOME u => Same.commit norm u |
171 |
| NONE => raise Same.SAME) |
|
32031 | 172 |
| norm (Abs (a, T, body)) = Abs (a, T, norm body) |
32018 | 173 |
| norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) |
174 |
| norm (f $ t) = |
|
175 |
((case norm f of |
|
176 |
Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) |
|
177 |
| nf => nf $ Same.commit norm t) |
|
178 |
handle Same.SAME => f $ norm t) |
|
179 |
| norm _ = raise Same.SAME; |
|
180 |
in norm end; |
|
0 | 181 |
|
32031 | 182 |
fun norm_term2 tenv tyenv : term Same.operation = |
32018 | 183 |
let |
32031 | 184 |
val normT = norm_type0 tyenv; |
32018 | 185 |
fun norm (Const (a, T)) = Const (a, normT T) |
186 |
| norm (Free (a, T)) = Free (a, normT T) |
|
187 |
| norm (Var (xi, T)) = |
|
32031 | 188 |
(case lookup2 (tyenv, tenv) (xi, T) of |
32018 | 189 |
SOME u => Same.commit norm u |
190 |
| NONE => Var (xi, normT T)) |
|
191 |
| norm (Abs (a, T, body)) = |
|
192 |
(Abs (a, normT T, Same.commit norm body) |
|
193 |
handle Same.SAME => Abs (a, T, norm body)) |
|
194 |
| norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) |
|
195 |
| norm (f $ t) = |
|
196 |
((case norm f of |
|
197 |
Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) |
|
198 |
| nf => nf $ Same.commit norm t) |
|
199 |
handle Same.SAME => f $ norm t) |
|
200 |
| norm _ = raise Same.SAME; |
|
201 |
in norm end; |
|
11513 | 202 |
|
32018 | 203 |
in |
204 |
||
32031 | 205 |
fun norm_type_same tyenv T = |
206 |
if Vartab.is_empty tyenv then raise Same.SAME |
|
207 |
else norm_type0 tyenv T; |
|
0 | 208 |
|
32031 | 209 |
fun norm_types_same tyenv Ts = |
210 |
if Vartab.is_empty tyenv then raise Same.SAME |
|
211 |
else Same.map (norm_type0 tyenv) Ts; |
|
32018 | 212 |
|
32031 | 213 |
fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T; |
11513 | 214 |
|
32031 | 215 |
fun norm_term_same (Envir {tenv, tyenv, ...}) = |
216 |
if Vartab.is_empty tyenv then norm_term1 tenv |
|
217 |
else norm_term2 tenv tyenv; |
|
10485 | 218 |
|
32018 | 219 |
fun norm_term envir t = norm_term_same envir t handle Same.SAME => t; |
25471
ca009b7ce693
Optimized beta_norm: only tries to normalize term when it contains
berghofe
parents:
24670
diff
changeset
|
220 |
fun beta_norm t = if Term.has_abs t then norm_term (empty 0) t else t; |
719
e3e1d1a6d408
Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents:
247
diff
changeset
|
221 |
|
32018 | 222 |
end; |
11513 | 223 |
|
224 |
||
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
225 |
(*Put a term into head normal form for unification.*) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
226 |
|
32018 | 227 |
fun head_norm env = |
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
228 |
let |
32018 | 229 |
fun norm (Var v) = |
230 |
(case lookup (env, v) of |
|
15531 | 231 |
SOME u => head_norm env u |
32018 | 232 |
| NONE => raise Same.SAME) |
233 |
| norm (Abs (a, T, body)) = Abs (a, T, norm body) |
|
234 |
| norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) |
|
235 |
| norm (f $ t) = |
|
236 |
(case norm f of |
|
237 |
Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) |
|
238 |
| nf => nf $ t) |
|
239 |
| norm _ = raise Same.SAME; |
|
240 |
in Same.commit norm end; |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
241 |
|
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
242 |
|
18937 | 243 |
(*Eta-contract a term (fully)*) |
244 |
||
22174 | 245 |
local |
246 |
||
32018 | 247 |
fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME |
22174 | 248 |
| decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body) |
32018 | 249 |
| decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u) |
250 |
| decr _ _ = raise Same.SAME |
|
251 |
and decrh lev t = (decr lev t handle Same.SAME => t); |
|
20670 | 252 |
|
22174 | 253 |
fun eta (Abs (a, T, body)) = |
254 |
((case eta body of |
|
255 |
body' as (f $ Bound 0) => |
|
256 |
if loose_bvar1 (f, 0) then Abs (a, T, body') |
|
257 |
else decrh 0 f |
|
32018 | 258 |
| body' => Abs (a, T, body')) handle Same.SAME => |
22174 | 259 |
(case body of |
260 |
f $ Bound 0 => |
|
32018 | 261 |
if loose_bvar1 (f, 0) then raise Same.SAME |
22174 | 262 |
else decrh 0 f |
32018 | 263 |
| _ => raise Same.SAME)) |
264 |
| eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u) |
|
265 |
| eta _ = raise Same.SAME; |
|
22174 | 266 |
|
267 |
in |
|
268 |
||
269 |
fun eta_contract t = |
|
32018 | 270 |
if Term.has_abs t then Same.commit eta t else t; |
18937 | 271 |
|
272 |
val beta_eta_contract = eta_contract o beta_norm; |
|
273 |
||
22174 | 274 |
end; |
275 |
||
18937 | 276 |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
277 |
(*finds type of term without checking that combinations are consistent |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
278 |
Ts holds types of bound variables*) |
32031 | 279 |
fun fastype (Envir {tyenv, ...}) = |
280 |
let |
|
281 |
val funerr = "fastype: expected function type"; |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
282 |
fun fast Ts (f $ u) = |
32031 | 283 |
(case fast Ts f of |
284 |
Type ("fun", [_, T]) => T |
|
285 |
| TVar v => |
|
286 |
(case Type.lookup tyenv v of |
|
287 |
SOME (Type ("fun", [_, T])) => T |
|
288 |
| _ => raise TERM (funerr, [f $ u])) |
|
289 |
| _ => raise TERM (funerr, [f $ u])) |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
290 |
| fast Ts (Const (_, T)) = T |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
291 |
| fast Ts (Free (_, T)) = T |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
292 |
| fast Ts (Bound i) = |
32031 | 293 |
(nth Ts i handle Subscript => raise TERM ("fastype: Bound", [Bound i])) |
20670 | 294 |
| fast Ts (Var (_, T)) = T |
32031 | 295 |
| fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u; |
296 |
in fast end; |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
297 |
|
15797 | 298 |
|
299 |
(*Substitute for type Vars in a type*) |
|
32031 | 300 |
fun typ_subst_TVars tyenv T = |
301 |
if Vartab.is_empty tyenv then T |
|
302 |
else |
|
303 |
let |
|
304 |
fun subst (Type (a, Ts)) = Type (a, map subst Ts) |
|
305 |
| subst (T as TFree _) = T |
|
306 |
| subst (T as TVar v) = (case Type.lookup tyenv v of NONE => T | SOME U => U); |
|
307 |
in subst T end; |
|
15797 | 308 |
|
309 |
(*Substitute for type Vars in a term*) |
|
20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20098
diff
changeset
|
310 |
val subst_TVars = map_types o typ_subst_TVars; |
15797 | 311 |
|
312 |
(*Substitute for Vars in a term *) |
|
32031 | 313 |
fun subst_Vars tenv tm = |
314 |
if Vartab.is_empty tenv then tm |
|
315 |
else |
|
316 |
let |
|
317 |
fun subst (t as Var v) = the_default t (lookup' (tenv, v)) |
|
15797 | 318 |
| subst (Abs (a, T, t)) = Abs (a, T, subst t) |
32031 | 319 |
| subst (t $ u) = subst t $ subst u |
320 |
| subst t = t; |
|
321 |
in subst tm end; |
|
15797 | 322 |
|
323 |
(*Substitute for type/term Vars in a term *) |
|
32031 | 324 |
fun subst_vars (tyenv, tenv) = |
325 |
if Vartab.is_empty tyenv then subst_Vars tenv |
|
326 |
else |
|
327 |
let |
|
328 |
fun subst (Const (a, T)) = Const (a, typ_subst_TVars tyenv T) |
|
329 |
| subst (Free (a, T)) = Free (a, typ_subst_TVars tyenv T) |
|
330 |
| subst (Var (xi, T)) = |
|
331 |
(case lookup' (tenv, (xi, T)) of |
|
332 |
NONE => Var (xi, typ_subst_TVars tyenv T) |
|
333 |
| SOME t => t) |
|
334 |
| subst (t as Bound _) = t |
|
335 |
| subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars tyenv T, subst t) |
|
336 |
| subst (t $ u) = subst t $ subst u; |
|
337 |
in subst end; |
|
15797 | 338 |
|
18937 | 339 |
|
21795 | 340 |
(* expand defined atoms -- with local beta reduction *) |
18937 | 341 |
|
19422 | 342 |
fun expand_atom T (U, u) = |
343 |
subst_TVars (Type.raw_match (U, T) Vartab.empty) u |
|
32031 | 344 |
handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]); |
18937 | 345 |
|
21795 | 346 |
fun expand_term get = |
21695 | 347 |
let |
348 |
fun expand tm = |
|
349 |
let |
|
350 |
val (head, args) = Term.strip_comb tm; |
|
351 |
val args' = map expand args; |
|
352 |
fun comb head' = Term.list_comb (head', args'); |
|
353 |
in |
|
354 |
(case head of |
|
355 |
Abs (x, T, t) => comb (Abs (x, T, expand t)) |
|
356 |
| _ => |
|
32031 | 357 |
(case get head of |
358 |
SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args') |
|
359 |
| NONE => comb head)) |
|
21695 | 360 |
end; |
361 |
in expand end; |
|
362 |
||
21795 | 363 |
fun expand_term_frees defs = |
364 |
let |
|
365 |
val eqs = map (fn ((x, U), u) => (x, (U, u))) defs; |
|
366 |
val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE; |
|
367 |
in expand_term get end; |
|
368 |
||
0 | 369 |
end; |