author  wenzelm 
Fri, 17 Nov 2000 18:49:29 +0100  
changeset 10485  f1576723371f 
parent 8407  d522ad1809e9 
child 11513  2f6fe5b01521 
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} 
10485  14 
val genvars: string > env * typ list > env * term list 
15 
val genvar: string > env * typ > env * term 

16 
val lookup: env * indexname > term option 

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

18 
val empty: int > env 

19 
val is_empty: env > bool 

20 
val above: int * env > bool 

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

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

23 
val norm_term: env > term > term 

24 
val beta_norm: term > term 

0  25 
end; 
26 

1500  27 
structure Envir : ENVIR = 
0  28 
struct 
29 

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

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

32 
*) 

33 
datatype env = Envir of 

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

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

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

36 
iTs: typ Vartab.table} (*table of assignments to TVars*) 
0  37 

38 

39 
(*Generate a list of distinct variables. 

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

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

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

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

44 
 genvs (n, T::Ts) = 

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

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

46 
:: genvs(n+1,Ts) 
0  47 
in (Envir{maxidx=maxidx+1, asol=asol, iTs=iTs}, genvs (0,Ts)) end; 
48 

49 
(*Generate a variable.*) 

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

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

51 
let val (env',[v]) = genvars name (env,[T]) 
0  52 
in (env',v) end; 
53 

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

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

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

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

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

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

60 
fun empty m = Envir{maxidx=m, asol=Vartab.empty, iTs=Vartab.empty}; 
0  61 

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

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

63 
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

64 

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

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

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

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

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

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

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

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

72 

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

75 
Var(name',T) => 

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

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

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

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

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

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

81 
else update((a,t), env) 
0  82 
 _ => update((a,t), env); 
83 

84 

85 
(*Convert environment to alist*) 

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

86 
fun alist_of (Envir{asol,...}) = Vartab.dest asol; 
0  87 

88 

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

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

92 

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

94 
exception SAME; 

0  95 

1500  96 
fun norm_term1 (asol,t) : term = 
97 
let fun norm (Var (w,T)) = 

10485  98 
(case Vartab.lookup (asol, w) of 
99 
Some u => (norm u handle SAME => u) 

100 
 None => raise SAME) 

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

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

103 
 norm (f $ t) = 

104 
((case norm f of 

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

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

107 
handle SAME => f $ norm t) 

108 
 norm _ = raise SAME 

2191  109 
and normh t = norm t handle SAME => t 
1500  110 
in normh t end 
0  111 

1500  112 
and norm_term2(asol,iTs,t) : term = 
113 
let fun normT(Type(a,Ts)) = Type(a, normTs Ts) 

10485  114 
 normT(TFree _) = raise SAME 
115 
 normT(TVar(v,_)) = (case Vartab.lookup (iTs, v) of 

116 
Some(U) => normTh U 

117 
 None => raise SAME) 

1500  118 
and normTh T = ((normT T) handle SAME => T) 
119 
and normTs([]) = raise SAME 

10485  120 
 normTs(T::Ts) = ((normT T :: (normTs Ts handle SAME => Ts)) 
121 
handle SAME => T :: normTs Ts) 

1500  122 
and norm(Const(a,T)) = Const(a, normT T) 
10485  123 
 norm(Free(a,T)) = Free(a, normT T) 
124 
 norm(Var (w,T)) = 

125 
(case Vartab.lookup (asol, w) of 

126 
Some u => normh u 

127 
 None => Var(w,normT T)) 

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

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

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

131 
 norm(f $ t) = 

132 
((case norm f of 

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

134 
 nf => nf $ normh t) 

135 
handle SAME => f $ norm t) 

136 
 norm _ = raise SAME 

1500  137 
and normh t = (norm t) handle SAME => t 
138 
in normh t end; 

0  139 

140 
fun norm_term (env as Envir{asol,iTs,...}) t : term = 

10485  141 
if Vartab.is_empty iTs then norm_term1(asol, t) else norm_term2(asol,iTs, t) 
142 

143 
val beta_norm = norm_term (empty 0); 

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

144 

0  145 
end; 