author  obua 
Tue, 07 Jun 2005 06:39:39 +0200  
changeset 16308  636a1a84977a 
parent 16198  cfd070a2cc4d 
child 16361  cb31cb768a6c 
permissions  rwrr 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

1 
(* Title: Pure/General/defs.ML 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

2 
ID: $Id$ 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

3 
Author: Steven Obua, TU Muenchen 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

4 

16308  5 
Checks if definitions preserve consistency of logic by enforcing 
6 
that there are no cyclic definitions. The algorithm is described in 

7 
"An Algorithm for Determining Definitional Cycles in HigherOrder Logic with Overloading", 

8 
Steven Obua, technical report, to be written :) 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

9 
*) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

10 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

11 
signature DEFS = sig 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

12 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

13 
type graph 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

14 

cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

15 
exception DEFS of string 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

16 
exception CIRCULAR of (typ * string * string) list 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

17 
exception INFINITE_CHAIN of (typ * string * string) list 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

18 
exception FINAL of string * typ 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

19 
exception CLASH of string * string * string 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

20 

cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

21 
val empty : graph 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

22 
val declare : graph > string * typ > graph (* exception DEFS *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

23 
val define : graph > string * typ > string > (string * typ) list > graph 
16308  24 
(* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *) 
25 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

26 
val finalize : graph > string * typ > graph (* exception DEFS *) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

27 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

28 
val finals : graph > (typ list) Symtab.table 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

29 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

30 
val merge : graph > graph > graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

31 

16308  32 
(* If set to true then the exceptions CIRCULAR and INFINITE_CHAIN return the full 
33 
chain of definitions that lead to the exception. In the beginning, chain_history 

34 
is initialized with the Isabelle environment variable DEFS_CHAIN_HISTORY. *) 

35 
val set_chain_history : bool > unit 

36 
val chain_history : unit > bool 

37 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

38 
end 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

39 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

40 
structure Defs :> DEFS = struct 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

41 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

42 
type tyenv = Type.tyenv 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

43 
type edgelabel = (int * typ * typ * (typ * string * string) list) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

44 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

45 
datatype node = Node of 
16308  46 
typ (* most general type of constant *) 
47 
* defnode Symtab.table 

48 
(* a table of defnodes, each corresponding to 1 definition of the 

49 
constant for a particular type, indexed by axiom name *) 

50 
* (unit Symtab.table) Symtab.table 

51 
(* a table of all back referencing defnodes to this node, 

52 
indexed by node name of the defnodes *) 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

53 
* typ list (* a list of all finalized types *) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

54 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

55 
and defnode = Defnode of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

56 
typ (* type of the constant in this particular definition *) 
16308  57 
* (edgelabel list) Symtab.table (* The edges, grouped by nodes. *) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

58 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

59 
fun getnode graph noderef = the (Symtab.lookup (graph, noderef)) 
16308  60 
fun get_nodedefs (Node (_, defs, _, _)) = defs 
61 
fun get_defnode (Node (_, defs, _, _)) defname = Symtab.lookup (defs, defname) 

62 
fun get_defnode' graph noderef defname = 

63 
Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname) 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

64 

16308  65 
datatype graphaction = Declare of string * typ 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

66 
 Define of string * typ * string * (string * typ) list 
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

67 
 Finalize of string * typ 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

68 

16308  69 
type graph = int * (graphaction list) * (node Symtab.table) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

70 

16308  71 
val CHAIN_HISTORY = 
72 
let 

73 
fun f c = if Char.isSpace c then "" else String.str (Char.toUpper c) 

74 
val env = String.translate f (getenv "DEFS_CHAIN_HISTORY") 

75 
in 

76 
ref (env = "ON" orelse env = "TRUE") 

77 
end 

78 

79 
fun set_chain_history b = CHAIN_HISTORY := b 

80 
fun chain_history () = !CHAIN_HISTORY 

81 

82 
val empty = (0, [], Symtab.empty) 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

83 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

84 
exception DEFS of string; 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

85 
exception CIRCULAR of (typ * string * string) list; 
16113
692fe6595755
Infinite chains in definitions are now detected, too.
obua
parents:
16108
diff
changeset

86 
exception INFINITE_CHAIN of (typ * string * string) list; 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

87 
exception CLASH of string * string * string; 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

88 
exception FINAL of string * typ; 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

89 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

90 
fun def_err s = raise (DEFS s) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

91 

16308  92 
fun checkT (Type (a, Ts)) = Type (a, map checkT Ts) 
93 
 checkT (TVar ((a, 0), _)) = TVar ((a, 0), []) 

94 
 checkT (TVar ((a, i), _)) = def_err "type is not clean" 

95 
 checkT (TFree (a, _)) = TVar ((a, 0), []) 

96 

97 
fun declare' (cost, actions, g) (cty as (name, ty)) = 

98 
(cost, (Declare cty)::actions, 

99 
Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [])), g)) 

16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

100 
handle Symtab.DUP _ => def_err "constant is already declared" 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

101 

16308  102 
fun declare g (name, ty) = declare' g (name, checkT ty) 
103 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

104 
fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2; 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

105 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

106 
fun subst_incr_tvar inc t = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

107 
if (inc > 0) then 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

108 
let 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

109 
val tv = typ_tvars t 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

110 
val t' = incr_tvar inc t 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

111 
fun update_subst (((n,i), _), s) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

112 
Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

113 
in 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

114 
(t',List.foldl update_subst Vartab.empty tv) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

115 
end 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

116 
else 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

117 
(t, Vartab.empty) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

118 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

119 
fun subst s ty = Envir.norm_type s ty 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

120 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

121 
fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

122 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

123 
fun is_instance instance_ty general_ty = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

124 
Type.typ_instance Type.empty_tsig (instance_ty, general_ty) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

125 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

126 
fun is_instance_r instance_ty general_ty = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

127 
is_instance instance_ty (rename instance_ty general_ty) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

128 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

129 
fun unify ty1 ty2 = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

130 
SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2))) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

131 
handle Type.TUNIFY => NONE 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

132 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

133 
(* 
16308  134 
Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and 
135 
so that they are different. All indices in ty1 and ty2 are supposed to be less than or 

136 
equal to max. 

137 
Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than 

138 
all indices in s1, s2, ty1, ty2. 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

139 
*) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

140 
fun unify_r max ty1 ty2 = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

141 
let 
16308  142 
val max = Int.max(max, 0) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

143 
val max1 = max (* >= maxidx_of_typ ty1 *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

144 
val max2 = max (* >= maxidx_of_typ ty2 *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

145 
val max = Int.max(max, Int.max (max1, max2)) 
16308  146 
val (ty1, s1) = subst_incr_tvar (max + 1) ty1 
147 
val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2 

148 
val max = max + max1 + max2 + 2 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

149 
fun merge a b = Vartab.merge (fn _ => false) (a, b) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

150 
in 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

151 
case unify ty1 ty2 of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

152 
NONE => NONE 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

153 
 SOME s => SOME (max, merge s1 s, merge s2 s) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

154 
end 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

155 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

156 
fun can_be_unified_r ty1 ty2 = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

157 
let 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

158 
val ty2 = rename ty1 ty2 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

159 
in 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

160 
case unify ty1 ty2 of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

161 
NONE => false 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

162 
 _ => true 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

163 
end 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

164 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

165 
fun can_be_unified ty1 ty2 = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

166 
case unify ty1 ty2 of 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

167 
NONE => false 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

168 
 _ => true 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

169 

16308  170 
structure Inttab = TableFun(type key = int val ord = int_ord); 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

171 

16308  172 
fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) = 
173 
if maxidx <= 1000000 then edge else 

174 
let 

175 

176 
fun idxlist idx extract_ty inject_ty (tab, max) ts = 

177 
foldr 

178 
(fn (e, ((tab, max), ts)) => 

179 
let 

180 
val ((tab, max), ty) = idx (tab, max) (extract_ty e) 

181 
val e = inject_ty (ty, e) 

182 
in 

183 
((tab, max), e::ts) 

184 
end) 

185 
((tab,max), []) ts 

186 

187 
fun idx (tab,max) (TVar ((a,i),_)) = 

188 
(case Inttab.lookup (tab, i) of 

189 
SOME j => ((tab, max), TVar ((a,j),[])) 

190 
 NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[]))) 

191 
 idx (tab,max) (Type (t, ts)) = 

192 
let 

193 
val ((tab, max), ts) = idxlist idx I fst (tab, max) ts 

194 
in 

195 
((tab,max), Type (t, ts)) 

196 
end 

197 
 idx (tab, max) ty = ((tab, max), ty) 

198 

199 
val ((tab,max), u1) = idx (Inttab.empty, 0) u1 

200 
val ((tab,max), v1) = idx (tab, max) v1 

201 
val ((tab,max), history) = 

202 
idxlist idx 

203 
(fn (ty,_,_) => ty) 

204 
(fn (ty, (_, s1, s2)) => (ty, s1, s2)) 

205 
(tab, max) history 

206 
in 

207 
(max, u1, v1, history) 

208 
end 

209 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

210 
fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

211 
let 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

212 
val t1 = u1 > v1 
16308  213 
val t2 = incr_tvar (maxidx1+1) (u2 > v2) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

214 
in 
16308  215 
if (is_instance t1 t2) then 
216 
(if is_instance t2 t1 then 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

217 
SOME (int_ord (length history2, length history1)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

218 
else 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

219 
SOME LESS) 
16308  220 
else if (is_instance t2 t1) then 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

221 
SOME GREATER 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

222 
else 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

223 
NONE 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

224 
end 
16308  225 

226 
fun merge_edges_1 (x, []) = [x] 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

227 
 merge_edges_1 (x, (y::ys)) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

228 
(case compare_edges x y of 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

229 
SOME LESS => (y::ys) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

230 
 SOME EQUAL => (y::ys) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

231 
 SOME GREATER => merge_edges_1 (x, ys) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

232 
 NONE => y::(merge_edges_1 (x, ys))) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

233 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

234 
fun merge_edges xs ys = foldl merge_edges_1 xs ys 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

235 

16308  236 
fun define' (cost, actions, graph) (mainref, ty) axname body = 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

237 
let 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

238 
val mainnode = (case Symtab.lookup (graph, mainref) of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

239 
NONE => def_err ("constant "^mainref^" is not declared") 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

240 
 SOME n => n) 
16308  241 
val (Node (gty, defs, backs, finals)) = mainnode 
242 
val _ = (if is_instance_r ty gty then () 

243 
else def_err "type of constant does not match declared type") 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

244 
fun check_def (s, Defnode (ty', _)) = 
16308  245 
(if can_be_unified_r ty ty' then 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

246 
raise (CLASH (mainref, axname, s)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

247 
else if s = axname then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

248 
def_err "name of axiom is already used for another definition of this constant" 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

249 
else false) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

250 
val _ = Symtab.exists check_def defs 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

251 
fun check_final finalty = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

252 
(if can_be_unified_r finalty ty then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

253 
raise (FINAL (mainref, finalty)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

254 
else 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

255 
true) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

256 
val _ = forall check_final finals 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

257 

16308  258 
(* now we know that the only thing that can prevent acceptance of the definition 
259 
is a cyclic dependency *) 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

260 

16308  261 
fun insert_edges edges (nodename, links) = 
262 
(if links = [] then 

263 
edges 

264 
else 

265 
let 

266 
val links = map normalize_edge_idx links 

267 
in 

268 
Symtab.update ((nodename, 

269 
case Symtab.lookup (edges, nodename) of 

270 
NONE => links 

271 
 SOME links' => merge_edges links' links), 

272 
edges) 

273 
end) 

274 

275 
fun make_edges ((bodyn, bodyty), edges) = 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

276 
let 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

277 
val bnode = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

278 
(case Symtab.lookup (graph, bodyn) of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

279 
NONE => def_err "body of constant definition references undeclared constant" 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

280 
 SOME x => x) 
16308  281 
val (Node (general_btyp, bdefs, bbacks, bfinals)) = bnode 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

282 
in 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

283 
case unify_r 0 bodyty general_btyp of 
16308  284 
NONE => edges 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

285 
 SOME (maxidx, sigma1, sigma2) => 
16308  286 
if exists (is_instance_r bodyty) bfinals then 
287 
edges 

288 
else 

289 
let 

290 
fun insert_trans_edges ((step1, edges), (nodename, links)) = 

291 
let 

292 
val (maxidx1, alpha1, beta1, defname) = step1 

293 
fun connect (maxidx2, alpha2, beta2, history) = 

294 
case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of 

295 
NONE => NONE 

296 
 SOME (max, sleft, sright) => 

297 
SOME (max, subst sleft alpha1, subst sright beta2, 

298 
if !CHAIN_HISTORY then 

299 
((subst sleft beta1, bodyn, defname):: 

300 
(subst_history sright history)) 

301 
else []) 

302 
val links' = List.mapPartial connect links 

303 
in 

304 
(step1, insert_edges edges (nodename, links')) 

305 
end 

306 

307 
fun make_edges' ((swallowed, edges), 

308 
(def_name, Defnode (def_ty, def_edges))) = 

309 
if swallowed then 

310 
(swallowed, edges) 

311 
else 

312 
(case unify_r 0 bodyty def_ty of 

313 
NONE => (swallowed, edges) 

314 
 SOME (maxidx, sigma1, sigma2) => 

315 
(is_instance_r bodyty def_ty, 

316 
snd (Symtab.foldl insert_trans_edges 

317 
(((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name), 

318 
edges), def_edges)))) 

319 
val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs) 

320 
in 

321 
if swallowed then 

322 
edges 

323 
else 

324 
insert_edges edges 

325 
(bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])]) 

326 
end 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

327 
end 
16308  328 

329 
val edges = foldl make_edges Symtab.empty body 

330 

331 
(* We also have to add the backreferences that this new defnode induces. *) 

332 
fun install_backrefs (graph, (noderef, links)) = 

333 
if links <> [] then 

334 
let 

335 
val (Node (ty, defs, backs, finals)) = getnode graph noderef 

336 
val defnames = 

337 
(case Symtab.lookup (backs, mainref) of 

338 
NONE => Symtab.empty 

339 
 SOME s => s) 

340 
val defnames' = Symtab.update_new ((axname, ()), defnames) 

341 
val backs' = Symtab.update ((mainref,defnames'), backs) 

342 
in 

343 
Symtab.update ((noderef, Node (ty, defs, backs', finals)), graph) 

344 
end 

345 
else 

346 
graph 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

347 

cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

348 
val graph = Symtab.foldl install_backrefs (graph, edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

349 

16308  350 
val (Node (_, _, backs, _)) = getnode graph mainref 
351 
val thisDefnode = Defnode (ty, edges) 

352 
val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

353 
((axname, thisDefnode), defs), backs, finals)), graph) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

354 

16308  355 
(* Now we have to check all backreferences to this node and inform them about 
356 
the new defnode. In this section we also check for circularity. *) 

357 
fun update_backrefs ((backs, graph), (noderef, defnames)) = 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

358 
let 
16308  359 
fun update_defs ((defnames, graph),(defname, _)) = 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

360 
let 
16308  361 
val (Node (nodety, nodedefs, nodebacks, nodefinals)) = getnode graph noderef 
362 
val (Defnode (def_ty, defnode_edges)) = 

363 
the (Symtab.lookup (nodedefs, defname)) 

364 
val edges = the (Symtab.lookup (defnode_edges, mainref)) 

365 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

366 
(* the type of thisDefnode is ty *) 
16308  367 
fun update (e as (max, alpha, beta, history), (changed, edges)) = 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

368 
case unify_r max beta ty of 
16308  369 
NONE => (changed, e::edges) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

370 
 SOME (max', s_beta, s_ty) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

371 
let 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

372 
val alpha' = subst s_beta alpha 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

373 
val ty' = subst s_ty ty 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

374 
val _ = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

375 
if noderef = mainref andalso defname = axname then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

376 
(case unify alpha' ty' of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

377 
NONE => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

378 
if (is_instance_r ty' alpha') then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

379 
raise (INFINITE_CHAIN ( 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

380 
(alpha', mainref, axname):: 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

381 
(subst_history s_beta history)@ 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

382 
[(ty', mainref, axname)])) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

383 
else () 
16308  384 
 SOME s => 
385 
raise (CIRCULAR ( 

386 
(subst s alpha', mainref, axname):: 

387 
(subst_history s (subst_history s_beta history))@ 

388 
[(subst s ty', mainref, axname)]))) 

389 
else () 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

390 
in 
16308  391 
if is_instance_r beta ty then 
392 
(true, edges) 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

393 
else 
16308  394 
(changed, e::edges) 
395 
end 

396 

397 
val (changed, edges') = foldl update (false, []) edges 

398 
val defnames' = if edges' = [] then 

399 
defnames 

400 
else 

401 
Symtab.update ((defname, ()), defnames) 

402 
in 

403 
if changed then 

404 
let 

405 
val defnode_edges' = 

406 
if edges' = [] then 

407 
Symtab.delete mainref defnode_edges 

408 
else 

409 
Symtab.update ((mainref, edges'), defnode_edges) 

410 
val defnode' = Defnode (def_ty, defnode_edges') 

411 
val nodedefs' = Symtab.update ((defname, defnode'), nodedefs) 

412 
val graph' = 

413 
Symtab.update 

414 
((noderef, Node (nodety, nodedefs', nodebacks, nodefinals)),graph) 

415 
in 

416 
(defnames', graph') 

417 
end 

418 
else 

419 
(defnames', graph) 

420 
end 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

421 

16308  422 
val (defnames', graph') = Symtab.foldl update_defs 
423 
((Symtab.empty, graph), defnames) 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

424 
in 
16308  425 
if Symtab.is_empty defnames' then 
426 
(backs, graph') 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

427 
else 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

428 
let 
16308  429 
val backs' = Symtab.update_new ((noderef, defnames'), backs) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

430 
in 
16308  431 
(backs', graph') 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

432 
end 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

433 
end 
16308  434 

435 
val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs) 

436 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

437 
(* If a Circular exception is thrown then we never reach this point. *) 
16308  438 
val (Node (gty, defs, _, finals)) = getnode graph mainref 
439 
val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals)), graph) 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

440 
in 
16308  441 
(cost+3,(Define (mainref, ty, axname, body))::actions, graph) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

442 
end 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

443 

16308  444 
fun define g (mainref, ty) axname body = 
445 
let 

446 
val ty = checkT ty 

447 
val body = distinct (map (fn (n,t) => (n, checkT t)) body) 

448 
in 

449 
define' g (mainref, ty) axname body 

450 
end 

451 

452 
fun finalize' (cost, history, graph) (noderef, ty) = 

453 
case Symtab.lookup (graph, noderef) of 

454 
NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") 

455 
 SOME (Node (nodety, defs, backs, finals)) => 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

456 
let 
16308  457 
val _ = 
458 
if (not (is_instance_r ty nodety)) then 

459 
def_err ("only type instances of the declared constant "^ 

460 
noderef^" can be finalized") 

461 
else () 

462 
val _ = Symtab.exists 

463 
(fn (def_name, Defnode (def_ty, _)) => 

464 
if can_be_unified_r ty def_ty then 

465 
def_err ("cannot finalize constant "^noderef^ 

466 
"; clash with definition "^def_name) 

467 
else 

468 
false) 

469 
defs 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

470 

cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

471 
fun update_finals [] = SOME [ty] 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

472 
 update_finals (final_ty::finals) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

473 
(if is_instance_r ty final_ty then NONE 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

474 
else 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

475 
case update_finals finals of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

476 
NONE => NONE 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

477 
 (r as SOME finals) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

478 
if (is_instance_r final_ty ty) then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

479 
r 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

480 
else 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

481 
SOME (final_ty :: finals)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

482 
in 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

483 
case update_finals finals of 
16308  484 
NONE => (cost, history, graph) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

485 
 SOME finals => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

486 
let 
16308  487 
val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals)), 
488 
graph) 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

489 

16308  490 
fun update_backref ((graph, backs), (backrefname, backdefnames)) = 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

491 
let 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

492 
fun update_backdef ((graph, defnames), (backdefname, _)) = 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

493 
let 
16308  494 
val (backnode as Node (backty, backdefs, backbacks, backfinals)) = 
495 
getnode graph backrefname 

496 
val (Defnode (def_ty, all_edges)) = 

497 
the (get_defnode backnode backdefname) 

498 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

499 
val (defnames', all_edges') = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

500 
case Symtab.lookup (all_edges, noderef) of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

501 
NONE => sys_error "finalize: corrupt backref" 
16308  502 
 SOME edges => 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

503 
let 
16308  504 
val edges' = List.filter (fn (_, _, beta, _) => 
505 
not (is_instance_r beta ty)) edges 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

506 
in 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

507 
if edges' = [] then 
16308  508 
(defnames, Symtab.delete noderef all_edges) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

509 
else 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

510 
(Symtab.update ((backdefname, ()), defnames), 
16308  511 
Symtab.update ((noderef, edges'), all_edges)) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

512 
end 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

513 
val defnode' = Defnode (def_ty, all_edges') 
16308  514 
val backnode' = 
515 
Node (backty, 

516 
Symtab.update ((backdefname, defnode'), backdefs), 

517 
backbacks, backfinals) 

16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

518 
in 
16308  519 
(Symtab.update ((backrefname, backnode'), graph), defnames') 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

520 
end 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

521 

16308  522 
val (graph', defnames') = 
523 
Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

524 
in 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

525 
(graph', if Symtab.is_empty defnames' then backs 
16308  526 
else Symtab.update ((backrefname, defnames'), backs)) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

527 
end 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

528 
val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) 
16308  529 
val Node ( _, defs, _, _) = getnode graph' noderef 
530 
val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', finals)), graph') 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

531 
in 
16308  532 
(cost+1,(Finalize (noderef, ty)) :: history, graph') 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

533 
end 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

534 
end 
16308  535 

536 
fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) 

537 

538 
fun merge' (Declare cty, g) = (declare' g cty handle _ => g) 

539 
 merge' (Define (name, ty, axname, body), g as (_,_, graph)) = 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

540 
(case Symtab.lookup (graph, name) of 
16308  541 
NONE => define' g (name, ty) axname body 
542 
 SOME (Node (_, defs, _, _)) => 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

543 
(case Symtab.lookup (defs, axname) of 
16308  544 
NONE => define' g (name, ty) axname body 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

545 
 SOME _ => g)) 
16308  546 
 merge' (Finalize finals, g) = finalize' g finals 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

547 

16308  548 
fun merge (g1 as (cost1, actions1, _)) (g2 as (cost2, actions2, _)) = 
549 
if cost1 < cost2 then 

550 
foldr merge' g2 actions1 

551 
else 

552 
foldr merge' g1 actions2 

16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

553 

16308  554 
fun finals (cost, history, graph) = 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

555 
Symtab.foldl 
16308  556 
(fn (finals, (name, Node(_, _, _, ftys))) => Symtab.update_new ((name, ftys), finals)) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

557 
(Symtab.empty, graph) 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

558 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

559 
end; 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

560 

16308  561 
(* 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

562 

16308  563 
fun tvar name = TVar ((name, 0), []) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

564 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

565 
val bool = Type ("bool", []) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

566 
val int = Type ("int", []) 
16308  567 
val lam = Type("lam", []) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

568 
val alpha = tvar "'a" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

569 
val beta = tvar "'b" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

570 
val gamma = tvar "'c" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

571 
fun pair a b = Type ("pair", [a,b]) 
16308  572 
fun prm a = Type ("prm", [a]) 
573 
val name = Type ("name", []) 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

574 

cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

575 
val _ = print "make empty" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

576 
val g = Defs.empty 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

577 

16308  578 
val _ = print "declare perm" 
579 
val g = Defs.declare g ("perm", prm alpha > beta > beta) 

580 

581 
val _ = print "declare permF" 

582 
val g = Defs.declare g ("permF", prm alpha > lam > lam) 

583 

584 
val _ = print "define perm (1)" 

585 
val g = Defs.define g ("perm", prm alpha > (beta > gamma) > (beta > gamma)) "perm_fun" 

586 
[("perm", prm alpha > gamma > gamma), ("perm", prm alpha > beta > beta)] 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

587 

16308  588 
val _ = print "define permF (1)" 
589 
val g = Defs.define g ("permF", prm alpha > lam > lam) "permF_app" 

590 
([("perm", prm alpha > lam > lam), 

591 
("perm", prm alpha > lam > lam), 

592 
("perm", prm alpha > lam > lam), 

593 
("perm", prm alpha > name > name)]) 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

594 

16308  595 
val _ = print "define perm (2)" 
596 
val g = Defs.define g ("perm", prm alpha > lam > lam) "perm_lam" 

597 
[("permF", (prm alpha > lam > lam))] 

16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

598 

16308  599 
*) 