author  berghofe 
Mon, 19 Nov 2001 17:32:49 +0100  
changeset 12231  4a25f04bea61 
parent 11513  2f6fe5b01521 
child 12496  0a9bd5034e05 
permissions  rwrr 
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 

6 
Environments. They don't take account that typ is part of variable 

7 
name. Therefore we check elsewhere that two variables with same names 

8 
and different types cannot occur. 

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 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

13 
datatype env = Envir of {asol: term Vartab.table, iTs: typ Vartab.table, maxidx: int} 
11513  14 
exception SAME 
10485  15 
val genvars: string > env * typ list > env * term list 
16 
val genvar: string > env * typ > env * term 

17 
val lookup: env * indexname > term option 

18 
val update: (indexname * term) * env > env 

19 
val empty: int > env 

20 
val is_empty: env > bool 

21 
val above: int * env > bool 

22 
val vupdate: (indexname * term) * env > env 

23 
val alist_of: env > (indexname * term) list 

24 
val norm_term: env > term > term 

11513  25 
val norm_term_same: env > term > term 
26 
val norm_type: env > typ > typ 

27 
val norm_type_same: env > typ > typ 

28 
val norm_types_same: env > typ list > typ list 

10485  29 
val beta_norm: term > term 
12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

30 
val head_norm: env > term > term 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

31 
val fastype: env > typ list > term > typ 
0  32 
end; 
33 

1500  34 
structure Envir : ENVIR = 
0  35 
struct 
36 

37 
(*updating can destroy environment in 2 ways!! 

38 
(1) variables out of range (2) circular assignments 

39 
*) 

40 
datatype env = Envir of 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

41 
{maxidx: int, (*maximum index of vars*) 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

42 
asol: term Vartab.table, (*table of assignments to Vars*) 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

43 
iTs: typ Vartab.table} (*table of assignments to TVars*) 
0  44 

45 

46 
(*Generate a list of distinct variables. 

47 
Increments index to make them distinct from ALL present variables. *) 

48 
fun genvars name (Envir{maxidx, asol, iTs}, Ts) : env * term list = 

49 
let fun genvs (_, [] : typ list) : term list = [] 

50 
 genvs (n, [T]) = [ Var((name, maxidx+1), T) ] 

51 
 genvs (n, T::Ts) = 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

52 
Var((name ^ radixstring(26,"a",n), maxidx+1), T) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

53 
:: genvs(n+1,Ts) 
0  54 
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end; 
55 

56 
(*Generate a variable.*) 

57 
fun genvar name (env,T) : env * term = 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

58 
let val (env',[v]) = genvars name (env,[T]) 
0  59 
in (env',v) end; 
60 

8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

61 
fun lookup (Envir{asol,...}, xname) : term option = Vartab.lookup (asol, xname); 
0  62 

63 
fun update ((xname, t), Envir{maxidx, asol, iTs}) = 

8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

64 
Envir{maxidx=maxidx, asol=Vartab.update_new ((xname,t), asol), iTs=iTs}; 
0  65 

5289  66 
(*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

67 
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty}; 
0  68 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

69 
(*Test for empty environment*) 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

70 
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

71 

2142
20f208ff085d
Deleted Olist constructor. Replaced minidx by "above" function
paulson
parents:
1500
diff
changeset

72 
(*Determine if the least index updated exceeds lim*) 
8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

73 
fun above (lim, Envir {asol, iTs, ...}) = 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

74 
(case (Vartab.min_key asol, Vartab.min_key iTs) of 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

75 
(None, None) => true 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

76 
 (Some (_, i), None) => i > lim 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

77 
 (None, Some (_, i')) => i' > lim 
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

78 
 (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

79 

0  80 
(*Update, checking VarVar assignments: try to suppress higher indexes*) 
81 
fun vupdate((a,t), env) = case t of 

82 
Var(name',T) => 

247
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

83 
if a=name' then env (*cycle!*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

84 
else if xless(a, name') then 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

85 
(case lookup(env,name') of (*if already assigned, chase*) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

86 
None => update((name', Var(a,T)), env) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

87 
 Some u => vupdate((a,u), env)) 
bc10568855ee
added is_empty: env > bool, minidx: env > int option;
wenzelm
parents:
0
diff
changeset

88 
else update((a,t), env) 
0  89 
 _ => update((a,t), env); 
90 

91 

92 
(*Convert environment to alist*) 

8407
d522ad1809e9
Envir now uses Vartab instead of association lists.
berghofe
parents:
5289
diff
changeset

93 
fun alist_of (Envir{asol,...}) = Vartab.dest asol; 
0  94 

95 

1500  96 
(*** Beta normal form for terms (not eta normal form). 
97 
Chases variables in env; Does not exploit sharing of variable bindings 

98 
Does not check types, so could loop. ***) 

99 

100 
(*raised when norm has no effect on a term, to do sharing instead of copying*) 

101 
exception SAME; 

0  102 

11513  103 
fun norm_term1 same (asol,t) : term = 
1500  104 
let fun norm (Var (w,T)) = 
10485  105 
(case Vartab.lookup (asol, w) of 
106 
Some u => (norm u handle SAME => u) 

107 
 None => raise SAME) 

108 
 norm (Abs(a,T,body)) = Abs(a, T, norm body) 

109 
 norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body)) 

110 
 norm (f $ t) = 

111 
((case norm f of 

112 
Abs(_,_,body) => normh(subst_bound (t, body)) 

113 
 nf => nf $ (norm t handle SAME => t)) 

114 
handle SAME => f $ norm t) 

115 
 norm _ = raise SAME 

2191  116 
and normh t = norm t handle SAME => t 
11513  117 
in (if same then norm else normh) t end 
0  118 

11513  119 
fun normT iTs (Type (a, Ts)) = Type (a, normTs iTs Ts) 
120 
 normT iTs (TFree _) = raise SAME 

121 
 normT iTs (TVar(v, _)) = (case Vartab.lookup (iTs, v) of 

122 
Some U => normTh iTs U 

123 
 None => raise SAME) 

124 
and normTh iTs T = ((normT iTs T) handle SAME => T) 

125 
and normTs iTs [] = raise SAME 

126 
 normTs iTs (T :: Ts) = 

127 
((normT iTs T :: (normTs iTs Ts handle SAME => Ts)) 

128 
handle SAME => T :: normTs iTs Ts); 

129 

130 
fun norm_term2 same (asol, iTs, t) : term = 

131 
let fun norm (Const (a, T)) = Const(a, normT iTs T) 

132 
 norm (Free (a, T)) = Free(a, normT iTs T) 

133 
 norm (Var (w, T)) = 

10485  134 
(case Vartab.lookup (asol, w) of 
135 
Some u => normh u 

11513  136 
 None => Var(w, normT iTs T)) 
137 
 norm (Abs (a, T, body)) = 

138 
(Abs (a, normT iTs T, normh body) handle SAME => Abs (a, T, norm body)) 

139 
 norm (Abs(_, _, body) $ t) = normh (subst_bound (t, body)) 

140 
 norm (f $ t) = 

10485  141 
((case norm f of 
11513  142 
Abs(_, _, body) => normh (subst_bound (t, body)) 
10485  143 
 nf => nf $ normh t) 
144 
handle SAME => f $ norm t) 

145 
 norm _ = raise SAME 

1500  146 
and normh t = (norm t) handle SAME => t 
11513  147 
in (if same then norm else normh) t end; 
0  148 

11513  149 
fun gen_norm_term same (env as Envir{asol,iTs,...}) t : term = 
150 
if Vartab.is_empty iTs then norm_term1 same (asol, t) 

151 
else norm_term2 same (asol, iTs, t); 

152 

153 
val norm_term = gen_norm_term false; 

154 
val norm_term_same = gen_norm_term true; 

10485  155 

156 
val beta_norm = norm_term (empty 0); 

719
e3e1d1a6d408
Pure/envir/norm_term: replaced equality test for [] by null
lcp
parents:
247
diff
changeset

157 

11513  158 
fun norm_type (Envir {iTs, ...}) = normTh iTs; 
159 
fun norm_type_same (Envir {iTs, ...}) = 

160 
if Vartab.is_empty iTs then raise SAME else normT iTs; 

161 

162 
fun norm_types_same (Envir {iTs, ...}) = 

163 
if Vartab.is_empty iTs then raise SAME else normTs iTs; 

164 

165 

12231
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

166 
(*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

167 

4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

168 
fun head_norm env t = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

169 
let 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

170 
fun hnorm (Var (v, T)) = (case lookup (env, v) of 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

171 
Some u => head_norm env u 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

172 
 None => raise SAME) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

173 
 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

174 
 hnorm (Abs (_, _, body) $ t) = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

175 
head_norm env (subst_bound (t, body)) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

176 
 hnorm (f $ t) = (case hnorm f of 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

177 
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

178 
 nf => nf $ t) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

179 
 hnorm _ = raise SAME 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

180 
in hnorm t handle SAME => t end; 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

181 

4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

182 

4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

183 
(*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

184 
Ts holds types of bound variables*) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

185 
fun fastype (Envir {iTs, ...}) = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

186 
let val funerr = "fastype: expected function type"; 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

187 
fun fast Ts (f $ u) = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

188 
(case fast Ts f of 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

189 
Type ("fun", [_, T]) => T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

190 
 TVar(ixn, _) => 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

191 
(case Vartab.lookup (iTs, ixn) of 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

192 
Some (Type ("fun", [_, T])) => T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

193 
 _ => raise TERM (funerr, [f $ u])) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

194 
 _ => raise TERM (funerr, [f $ u])) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

195 
 fast Ts (Const (_, T)) = T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

196 
 fast Ts (Free (_, T)) = T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

197 
 fast Ts (Bound i) = 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

198 
(nth_elem (i, Ts) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

199 
handle LIST _=> raise TERM ("fastype: Bound", [Bound i])) 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

200 
 fast Ts (Var (_, T)) = T 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

201 
 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

202 
in fast end; 
4a25f04bea61
Moved head_norm and fastype from unify.ML to envir.ML
berghofe
parents:
11513
diff
changeset

203 

0  204 
end; 