author | wenzelm |
Fri, 07 Oct 2005 23:29:00 +0200 | |
changeset 17789 | ccba4e900023 |
parent 17412 | e26cb20ef0cc |
child 18937 | 0eb35519f0f3 |
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 |
0 | 2 |
ID: $Id$ |
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1988 University of Cambridge |
10485 | 5 |
|
15797 | 6 |
Environments. The type of a term variable / sort of a type variable is |
7 |
part of its name. The lookup function must apply type substitutions, |
|
8 |
since they may change the identity of a variable. |
|
0 | 9 |
*) |
10 |
||
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
11 |
signature ENVIR = |
0 | 12 |
sig |
15797 | 13 |
type tenv |
14 |
datatype env = Envir of {asol: tenv, iTs: Type.tyenv, maxidx: int} |
|
15 |
val type_env: env -> Type.tyenv |
|
11513 | 16 |
exception SAME |
10485 | 17 |
val genvars: string -> env * typ list -> env * term list |
18 |
val genvar: string -> env * typ -> env * term |
|
15797 | 19 |
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
|
20 |
val lookup': tenv * (indexname * typ) -> term option |
15797 | 21 |
val update: ((indexname * typ) * term) * env -> env |
10485 | 22 |
val empty: int -> env |
23 |
val is_empty: env -> bool |
|
24 |
val above: int * env -> bool |
|
15797 | 25 |
val vupdate: ((indexname * typ) * term) * env -> env |
26 |
val alist_of: env -> (indexname * (typ * term)) list |
|
10485 | 27 |
val norm_term: env -> term -> term |
11513 | 28 |
val norm_term_same: env -> term -> term |
15797 | 29 |
val norm_type: Type.tyenv -> typ -> typ |
30 |
val norm_type_same: Type.tyenv -> typ -> typ |
|
31 |
val norm_types_same: Type.tyenv -> typ list -> typ list |
|
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 |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
34 |
val fastype: env -> typ list -> term -> typ |
15797 | 35 |
val typ_subst_TVars: Type.tyenv -> typ -> typ |
36 |
val subst_TVars: Type.tyenv -> term -> term |
|
37 |
val subst_Vars: tenv -> term -> term |
|
38 |
val subst_vars: Type.tyenv * tenv -> term -> term |
|
0 | 39 |
end; |
40 |
||
1500 | 41 |
structure Envir : ENVIR = |
0 | 42 |
struct |
43 |
||
44 |
(*updating can destroy environment in 2 ways!! |
|
45 |
(1) variables out of range (2) circular assignments |
|
46 |
*) |
|
15797 | 47 |
type tenv = (typ * term) Vartab.table |
48 |
||
0 | 49 |
datatype env = Envir of |
15797 | 50 |
{maxidx: int, (*maximum index of vars*) |
51 |
asol: tenv, (*table of assignments to Vars*) |
|
52 |
iTs: Type.tyenv} (*table of assignments to TVars*) |
|
0 | 53 |
|
12496 | 54 |
fun type_env (Envir {iTs, ...}) = iTs; |
0 | 55 |
|
56 |
(*Generate a list of distinct variables. |
|
57 |
Increments index to make them distinct from ALL present variables. *) |
|
58 |
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list = |
|
59 |
let fun genvs (_, [] : typ list) : term list = [] |
|
60 |
| genvs (n, [T]) = [ Var((name, maxidx+1), T) ] |
|
61 |
| genvs (n, T::Ts) = |
|
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
62 |
Var((name ^ radixstring(26,"a",n), maxidx+1), T) |
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
63 |
:: genvs(n+1,Ts) |
0 | 64 |
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end; |
65 |
||
66 |
(*Generate a variable.*) |
|
67 |
fun genvar name (env,T) : env * term = |
|
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
68 |
let val (env',[v]) = genvars name (env,[T]) |
0 | 69 |
in (env',v) end; |
70 |
||
15797 | 71 |
fun var_clash ixn T T' = raise TYPE ("Variable " ^ |
72 |
quote (Syntax.string_of_vname ixn) ^ " has two distinct types", |
|
73 |
[T', T], []); |
|
0 | 74 |
|
15797 | 75 |
fun gen_lookup f asol (xname, T) = |
17412 | 76 |
(case Vartab.lookup asol xname of |
15797 | 77 |
NONE => NONE |
78 |
| SOME (U, t) => if f (T, U) then SOME t |
|
79 |
else var_clash xname T U); |
|
80 |
||
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
81 |
(* 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
|
82 |
(* 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
|
83 |
(* 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
|
84 |
(* and use = instead of eq_type. *) |
15797 | 85 |
|
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
86 |
fun lookup' (asol, p) = gen_lookup op = asol p; |
15797 | 87 |
|
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
88 |
fun lookup2 (iTs, asol) p = |
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
89 |
if Vartab.is_empty iTs then lookup' (asol, p) |
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
90 |
else gen_lookup (Type.eq_type iTs) asol p; |
15797 | 91 |
|
92 |
fun lookup (Envir {asol, iTs, ...}, p) = lookup2 (iTs, asol) p; |
|
93 |
||
94 |
fun update (((xname, T), t), Envir {maxidx, asol, iTs}) = |
|
17412 | 95 |
Envir{maxidx=maxidx, asol=Vartab.update_new (xname, (T, t)) asol, iTs=iTs}; |
0 | 96 |
|
5289 | 97 |
(*The empty environment. New variables will start with the given index+1.*) |
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset
|
98 |
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty}; |
0 | 99 |
|
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset
|
100 |
(*Test for empty environment*) |
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset
|
101 |
fun is_empty (Envir {asol, iTs, ...}) = Vartab.is_empty asol andalso Vartab.is_empty iTs; |
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
102 |
|
2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset
|
103 |
(*Determine if the least index updated exceeds lim*) |
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset
|
104 |
fun above (lim, Envir {asol, iTs, ...}) = |
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset
|
105 |
(case (Vartab.min_key asol, Vartab.min_key iTs) of |
15531 | 106 |
(NONE, NONE) => true |
107 |
| (SOME (_, i), NONE) => i > lim |
|
108 |
| (NONE, SOME (_, i')) => i' > lim |
|
109 |
| (SOME (_, i), SOME (_, i')) => i > lim andalso i' > lim); |
|
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
110 |
|
0 | 111 |
(*Update, checking Var-Var assignments: try to suppress higher indexes*) |
15797 | 112 |
fun vupdate ((aU as (a, U), t), env as Envir {iTs, ...}) = case t of |
113 |
Var (nT as (name', T)) => |
|
114 |
if a = name' then env (*cycle!*) |
|
247
bc10568855ee
added is_empty: env -> bool, minidx: env -> int option;
wenzelm
parents:
0
diff
changeset
|
115 |
else if xless(a, name') then |
15797 | 116 |
(case lookup (env, nT) of (*if already assigned, chase*) |
117 |
NONE => update ((nT, Var (a, T)), env) |
|
118 |
| SOME u => vupdate ((aU, u), env)) |
|
119 |
else update ((aU, t), env) |
|
120 |
| _ => update ((aU, t), env); |
|
0 | 121 |
|
122 |
||
123 |
(*Convert environment to alist*) |
|
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset
|
124 |
fun alist_of (Envir{asol,...}) = Vartab.dest asol; |
0 | 125 |
|
126 |
||
1500 | 127 |
(*** Beta normal form for terms (not eta normal form). |
128 |
Chases variables in env; Does not exploit sharing of variable bindings |
|
129 |
Does not check types, so could loop. ***) |
|
130 |
||
131 |
(*raised when norm has no effect on a term, to do sharing instead of copying*) |
|
132 |
exception SAME; |
|
0 | 133 |
|
11513 | 134 |
fun norm_term1 same (asol,t) : term = |
15797 | 135 |
let fun norm (Var wT) = |
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
136 |
(case lookup' (asol, wT) of |
15531 | 137 |
SOME u => (norm u handle SAME => u) |
138 |
| NONE => raise SAME) |
|
10485 | 139 |
| norm (Abs(a,T,body)) = Abs(a, T, norm body) |
140 |
| norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body)) |
|
141 |
| norm (f $ t) = |
|
142 |
((case norm f of |
|
143 |
Abs(_,_,body) => normh(subst_bound (t, body)) |
|
144 |
| nf => nf $ (norm t handle SAME => t)) |
|
145 |
handle SAME => f $ norm t) |
|
146 |
| norm _ = raise SAME |
|
2191 | 147 |
and normh t = norm t handle SAME => t |
11513 | 148 |
in (if same then norm else normh) t end |
0 | 149 |
|
11513 | 150 |
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts) |
151 |
| normT iTs (TFree _) = raise SAME |
|
15797 | 152 |
| normT iTs (TVar vS) = (case Type.lookup (iTs, vS) of |
15531 | 153 |
SOME U => normTh iTs U |
154 |
| NONE => raise SAME) |
|
11513 | 155 |
and normTh iTs T = ((normT iTs T) handle SAME => T) |
156 |
and normTs iTs [] = raise SAME |
|
157 |
| normTs iTs (T :: Ts) = |
|
158 |
((normT iTs T :: (normTs iTs Ts handle SAME => Ts)) |
|
159 |
handle SAME => T :: normTs iTs Ts); |
|
160 |
||
161 |
fun norm_term2 same (asol, iTs, t) : term = |
|
162 |
let fun norm (Const (a, T)) = Const(a, normT iTs T) |
|
163 |
| norm (Free (a, T)) = Free(a, normT iTs T) |
|
164 |
| norm (Var (w, T)) = |
|
15797 | 165 |
(case lookup2 (iTs, asol) (w, T) of |
15531 | 166 |
SOME u => normh u |
167 |
| NONE => Var(w, normT iTs T)) |
|
11513 | 168 |
| norm (Abs (a, T, body)) = |
169 |
(Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body)) |
|
170 |
| norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body)) |
|
171 |
| norm (f $ t) = |
|
10485 | 172 |
((case norm f of |
11513 | 173 |
Abs(_, _, body) => normh (subst_bound (t, body)) |
10485 | 174 |
| nf => nf $ normh t) |
175 |
handle SAME => f $ norm t) |
|
176 |
| norm _ = raise SAME |
|
1500 | 177 |
and normh t = (norm t) handle SAME => t |
11513 | 178 |
in (if same then norm else normh) t end; |
0 | 179 |
|
11513 | 180 |
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term = |
181 |
if Vartab.is_empty iTs then norm_term1 same (asol, t) |
|
182 |
else norm_term2 same (asol, iTs, t); |
|
183 |
||
184 |
val norm_term = gen_norm_term false; |
|
185 |
val norm_term_same = gen_norm_term true; |
|
10485 | 186 |
|
187 |
val beta_norm = norm_term (empty 0); |
|
719
e3e1d1a6d408
Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents:
247
diff
changeset
|
188 |
|
12496 | 189 |
fun norm_type iTs = normTh iTs; |
190 |
fun norm_type_same iTs = |
|
11513 | 191 |
if Vartab.is_empty iTs then raise SAME else normT iTs; |
192 |
||
12496 | 193 |
fun norm_types_same iTs = |
11513 | 194 |
if Vartab.is_empty iTs then raise SAME else normTs iTs; |
195 |
||
196 |
||
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
197 |
(*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
|
198 |
|
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
199 |
fun head_norm env t = |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
200 |
let |
15797 | 201 |
fun hnorm (Var vT) = (case lookup (env, vT) of |
15531 | 202 |
SOME u => head_norm env u |
203 |
| NONE => raise SAME) |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
204 |
| hnorm (Abs (a, T, body)) = Abs (a, T, hnorm body) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
205 |
| hnorm (Abs (_, _, body) $ t) = |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
206 |
head_norm env (subst_bound (t, body)) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
207 |
| hnorm (f $ t) = (case hnorm f of |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
208 |
Abs (_, _, body) => head_norm env (subst_bound (t, body)) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
209 |
| nf => nf $ t) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
210 |
| hnorm _ = raise SAME |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
211 |
in hnorm t handle SAME => t end; |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
212 |
|
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
213 |
|
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
214 |
(*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
|
215 |
Ts holds types of bound variables*) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
216 |
fun fastype (Envir {iTs, ...}) = |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
217 |
let val funerr = "fastype: expected function type"; |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
218 |
fun fast Ts (f $ u) = |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
219 |
(case fast Ts f of |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
220 |
Type ("fun", [_, T]) => T |
15797 | 221 |
| TVar ixnS => |
222 |
(case Type.lookup (iTs, ixnS) of |
|
15531 | 223 |
SOME (Type ("fun", [_, T])) => T |
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
224 |
| _ => raise TERM (funerr, [f $ u])) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
225 |
| _ => raise TERM (funerr, [f $ u])) |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
226 |
| fast Ts (Const (_, T)) = T |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
227 |
| fast Ts (Free (_, T)) = T |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
228 |
| fast Ts (Bound i) = |
15570 | 229 |
(List.nth (Ts, i) |
230 |
handle Subscript => raise TERM ("fastype: Bound", [Bound i])) |
|
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
231 |
| fast Ts (Var (_, T)) = T |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
232 |
| fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
233 |
in fast end; |
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset
|
234 |
|
15797 | 235 |
|
236 |
(*Substitute for type Vars in a type*) |
|
237 |
fun typ_subst_TVars iTs T = if Vartab.is_empty iTs then T else |
|
238 |
let fun subst(Type(a, Ts)) = Type(a, map subst Ts) |
|
239 |
| subst(T as TFree _) = T |
|
240 |
| subst(T as TVar ixnS) = |
|
241 |
(case Type.lookup (iTs, ixnS) of NONE => T | SOME(U) => U) |
|
242 |
in subst T end; |
|
243 |
||
244 |
(*Substitute for type Vars in a term*) |
|
245 |
val subst_TVars = map_term_types o typ_subst_TVars; |
|
246 |
||
247 |
(*Substitute for Vars in a term *) |
|
248 |
fun subst_Vars itms t = if Vartab.is_empty itms then t else |
|
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
249 |
let fun subst (v as Var ixnT) = getOpt (lookup' (itms, ixnT), v) |
15797 | 250 |
| subst (Abs (a, T, t)) = Abs (a, T, subst t) |
251 |
| subst (f $ t) = subst f $ subst t |
|
252 |
| subst t = t |
|
253 |
in subst t end; |
|
254 |
||
255 |
(*Substitute for type/term Vars in a term *) |
|
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
256 |
fun subst_vars (iTs, itms) = |
15797 | 257 |
if Vartab.is_empty iTs then subst_Vars itms else |
258 |
let fun subst (Const (a, T)) = Const(a, typ_subst_TVars iTs T) |
|
259 |
| subst (Free (a, T)) = Free (a, typ_subst_TVars iTs T) |
|
16652
4ecf94235ec7
Fixed bug: lookup' must use = instead of eq_type to compare types of
berghofe
parents:
15797
diff
changeset
|
260 |
| subst (Var (ixn, T)) = (case lookup' (itms, (ixn, T)) of |
15797 | 261 |
NONE => Var (ixn, typ_subst_TVars iTs T) |
262 |
| SOME t => t) |
|
263 |
| subst (b as Bound _) = b |
|
264 |
| subst (Abs (a, T, t)) = Abs(a, typ_subst_TVars iTs T, subst t) |
|
265 |
| subst (f $ t) = subst f $ subst t |
|
266 |
in subst end; |
|
267 |
||
0 | 268 |
end; |