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