author  obua 
Tue, 27 Sep 2005 14:41:41 +0200  
changeset 17670  bf4f2c1b26cc 
parent 17669  94dbbffbf94b 
child 17707  bc0270e9d27f 
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 

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

7 
Algorithm for Determining Definitional Cycles in HigherOrder Logic 

8 
with Overloading", Steven Obua, technical report, to be written :) 

17669  9 

10 
ATTENTION: 

17670  11 
Currently this implementation of the cycle test contains a bug of which the author is fully aware. 
17669  12 
This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

14 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

15 
signature DEFS = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

16 
sig 
16982  17 
(*true: record the full chain of definitions that lead to a circularity*) 
18 
val chain_history: bool ref 

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

19 
type graph 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

20 
val empty: graph 
16982  21 
val declare: theory > string * typ > graph > graph 
22 
val define: theory > string * typ > string > (string * typ) list > graph > graph 

23 
val finalize: theory > string * typ > graph > graph 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

24 
val merge: Pretty.pp > graph > graph > graph 
16982  25 
val finals: graph > typ list Symtab.table 
16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

26 
datatype overloadingstate = Open  Closed  Final 
16982  27 
val overloading_info: graph > string > (typ * (string*typ) list * overloadingstate) option 
28 
val monomorphic: graph > string > bool 

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

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

30 

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

31 
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

32 

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

33 
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

34 
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

35 

16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

36 
datatype overloadingstate = Open  Closed  Final 
16361  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 
datatype node = Node of 
16308  39 
typ (* most general type of constant *) 
16361  40 
* defnode Symtab.table 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

41 
(* a table of defnodes, each corresponding to 1 definition of the 
16308  42 
constant for a particular type, indexed by axiom name *) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

43 
* (unit Symtab.table) Symtab.table 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

44 
(* a table of all back referencing defnodes to this node, 
16308  45 
indexed by node name of the defnodes *) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

46 
* typ list (* a list of all finalized types *) 
16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

47 
* overloadingstate 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

48 

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

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

50 
typ (* type of the constant in this particular definition *) 
16308  51 
* (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

52 

17412  53 
fun getnode graph = the o Symtab.lookup graph 
16361  54 
fun get_nodedefs (Node (_, defs, _, _, _)) = defs 
17412  55 
fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup defs defname 
17223  56 
fun get_defnode' graph noderef = 
17412  57 
Symtab.lookup (get_nodedefs (the (Symtab.lookup graph noderef))) 
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 

17223  59 
fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0; 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

60 

16982  61 
datatype graphaction = 
62 
Declare of string * typ 

63 
 Define of string * typ * string * string * (string * typ) list 

64 
 Finalize of string * typ 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

65 

16982  66 
type graph = int * string Symtab.table * graphaction list * node Symtab.table 
16308  67 

16982  68 
val chain_history = ref true 
16308  69 

16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

70 
val empty = (0, Symtab.empty, [], 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

71 

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

72 
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

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

74 
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

75 
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

76 
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

77 

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

78 
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

79 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

80 
fun no_forwards defs = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

81 
Symtab.foldl 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

82 
(fn (closed, (_, Defnode (_, edges))) => 
16361  83 
if not closed then false else Symtab.is_empty edges) 
84 
(true, defs) 

85 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

86 
fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts) 
17669  87 
 checkT' (TFree (a, _)) = TVar ((a, 0), []) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

88 
 checkT' (TVar ((a, 0), _)) = TVar ((a, 0), []) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

89 
 checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []); 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

90 

16982  91 
fun checkT thy = Compress.typ thy o checkT'; 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

92 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

93 
fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) 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

94 

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

95 
fun subst_incr_tvar inc t = 
17223  96 
if inc > 0 then 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

97 
let 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

98 
val tv = typ_tvars t 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

99 
val t' = Logic.incr_tvar inc t 
17223  100 
fun update_subst ((n, i), _) = 
17412  101 
Vartab.update ((n, i), ([], TVar ((n, i + inc), []))); 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

102 
in 
17223  103 
(t', fold update_subst tv Vartab.empty) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

104 
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

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

106 
(t, Vartab.empty) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

107 

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

108 
fun subst s ty = Envir.norm_type s ty 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

109 

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

110 
fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

111 

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

112 
fun is_instance instance_ty general_ty = 
16936
93772bd33871
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
wenzelm
parents:
16877
diff
changeset

113 
Type.raw_instance (instance_ty, general_ty) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

114 

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

115 
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

116 
is_instance instance_ty (rename instance_ty general_ty) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

117 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

118 
fun unify ty1 ty2 = 
16936
93772bd33871
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
wenzelm
parents:
16877
diff
changeset

119 
SOME (Type.raw_unify (ty1, ty2) Vartab.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

120 
handle Type.TUNIFY => NONE 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

121 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

122 
(* 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

123 
Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

124 
so that they are different. All indices in ty1 and ty2 are supposed to be less than or 
16308  125 
equal to max. 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

126 
Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than 
16308  127 
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

128 
*) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

129 
fun unify_r max 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

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

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

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

134 
val max = Int.max(max, Int.max (max1, max2)) 
16308  135 
val (ty1, s1) = subst_incr_tvar (max + 1) ty1 
136 
val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

137 
val max = max + max1 + max2 + 2 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

138 
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

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

140 
case unify ty1 ty2 of 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

142 
 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

143 
end 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

144 

16982  145 
fun can_be_unified_r ty1 ty2 = is_some (unify ty1 (rename ty1 ty2)) 
146 
fun can_be_unified ty1 ty2 = is_some (unify ty1 ty2) 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

147 

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

150 
let 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

151 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

152 
fun idxlist idx extract_ty inject_ty (tab, max) ts = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

153 
foldr 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

154 
(fn (e, ((tab, max), ts)) => 
16308  155 
let 
156 
val ((tab, max), ty) = idx (tab, max) (extract_ty e) 

157 
val e = inject_ty (ty, e) 

158 
in 

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

160 
end) 

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

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

162 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

163 
fun idx (tab,max) (TVar ((a,i),_)) = 
17412  164 
(case Inttab.lookup tab i of 
16308  165 
SOME j => ((tab, max), TVar ((a,j),[])) 
17412  166 
 NONE => ((Inttab.update (i, max) tab, max + 1), TVar ((a,max),[]))) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

167 
 idx (tab,max) (Type (t, ts)) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

168 
let 
16308  169 
val ((tab, max), ts) = idxlist idx I fst (tab, max) ts 
170 
in 

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

172 
end 

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

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

174 

16308  175 
val ((tab,max), u1) = idx (Inttab.empty, 0) u1 
176 
val ((tab,max), v1) = idx (tab, max) v1 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

177 
val ((tab,max), history) = 
16308  178 
idxlist idx 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

179 
(fn (ty,_,_) => ty) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

180 
(fn (ty, (_, s1, s2)) => (ty, s1, s2)) 
16308  181 
(tab, max) history 
182 
in 

183 
(max, u1, v1, history) 

184 
end 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

185 

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

186 
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

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

188 
val t1 = u1 > v1 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

189 
val t2 = Logic.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

190 
in 
16308  191 
if (is_instance t1 t2) then 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

192 
(if is_instance t2 t1 then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

193 
SOME (int_ord (length history2, length history1)) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

194 
else 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

195 
SOME LESS) 
16308  196 
else if (is_instance t2 t1) then 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

198 
else 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

199 
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

200 
end 
16308  201 

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

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

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

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

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

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

208 
 NONE => y::(merge_edges_1 (x, ys))) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

211 

16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

212 
fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

213 
(cost, axmap, (Declare cty)::actions, 
17412  214 
Symtab.update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

215 
handle Symtab.DUP _ => 
16361  216 
let 
17412  217 
val (Node (gty, _, _, _, _)) = the (Symtab.lookup graph name) 
16361  218 
in 
219 
if is_instance_r ty gty andalso is_instance_r gty ty then 

220 
g 

221 
else 

222 
def_err "constant is already declared with different type" 

223 
end 

224 

16982  225 
fun declare'' thy g (name, ty) = declare' g (name, checkT thy ty) 
16361  226 

16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

227 
val axcounter = ref (IntInf.fromInt 0) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

228 
fun newaxname axmap axname = 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

229 
let 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

230 
val c = !axcounter 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

231 
val _ = axcounter := c+1 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

232 
val axname' = axname^"_"^(IntInf.toString c) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

233 
in 
17412  234 
(Symtab.update (axname', axname) axmap, axname') 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

235 
end 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

236 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

237 
fun translate_ex axmap x = 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

238 
let 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

239 
fun translate (ty, nodename, axname) = 
17412  240 
(ty, nodename, the (Symtab.lookup axmap axname)) 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

241 
in 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

242 
case x of 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

243 
INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain)) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

244 
 CIRCULAR cycle => raise (CIRCULAR (map translate cycle)) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

245 
 _ => raise x 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

246 
end 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

247 

16826  248 
fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_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

249 
let 
17412  250 
val mainnode = (case Symtab.lookup graph mainref of 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

251 
NONE => def_err ("constant "^mainref^" is not declared") 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

252 
 SOME n => n) 
16361  253 
val (Node (gty, defs, backs, finals, _)) = mainnode 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

254 
val _ = (if is_instance_r ty gty then () 
16308  255 
else def_err "type of constant does not match declared type") 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

256 
fun check_def (s, Defnode (ty', _)) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

257 
(if can_be_unified_r ty ty' then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

258 
raise (CLASH (mainref, axname, s)) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

259 
else if s = axname then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

260 
def_err "name of axiom is already used for another definition of this constant" 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

262 
val _ = Symtab.exists check_def defs 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

263 
fun check_final finalty = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

264 
(if can_be_unified_r finalty ty then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

265 
raise (FINAL (mainref, finalty)) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

266 
else 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

268 
val _ = forall check_final finals 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

269 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

270 
(* now we know that the only thing that can prevent acceptance of the definition 
16308  271 
is a cyclic dependency *) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

272 

16308  273 
fun insert_edges edges (nodename, links) = 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

274 
(if links = [] then 
16308  275 
edges 
276 
else 

277 
let 

278 
val links = map normalize_edge_idx links 

279 
in 

17412  280 
Symtab.update (nodename, 
281 
case Symtab.lookup edges nodename of 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

282 
NONE => links 
17223  283 
 SOME links' => merge_edges links' links) edges 
16308  284 
end) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

285 

16308  286 
fun make_edges ((bodyn, bodyty), edges) = 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

287 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

288 
val bnode = 
17412  289 
(case Symtab.lookup graph bodyn of 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

290 
NONE => def_err "body of constant definition references undeclared constant" 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

291 
 SOME x => x) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

292 
val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

293 
in 
16361  294 
if closed = Final then edges else 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

295 
case unify_r 0 bodyty general_btyp of 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

296 
NONE => edges 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

297 
 SOME (maxidx, sigma1, sigma2) => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

298 
if exists (is_instance_r bodyty) bfinals then 
16308  299 
edges 
300 
else 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

301 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

302 
fun insert_trans_edges ((step1, edges), (nodename, links)) = 
16308  303 
let 
304 
val (maxidx1, alpha1, beta1, defname) = step1 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

305 
fun connect (maxidx2, alpha2, beta2, history) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

306 
case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

307 
NONE => NONE 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

308 
 SOME (max, sleft, sright) => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

309 
SOME (max, subst sleft alpha1, subst sright beta2, 
16982  310 
if !chain_history then 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

311 
((subst sleft beta1, bodyn, defname):: 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

312 
(subst_history sright history)) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

313 
else []) 
16308  314 
val links' = List.mapPartial connect links 
315 
in 

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

317 
end 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

318 

16308  319 
fun make_edges' ((swallowed, edges), 
320 
(def_name, Defnode (def_ty, def_edges))) = 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

321 
if swallowed then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

322 
(swallowed, edges) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

323 
else 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

324 
(case unify_r 0 bodyty def_ty of 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

325 
NONE => (swallowed, edges) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

326 
 SOME (maxidx, sigma1, sigma2) => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

327 
(is_instance_r bodyty def_ty, 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

328 
snd (Symtab.foldl insert_trans_edges 
16308  329 
(((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name), 
330 
edges), def_edges)))) 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

331 
val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

332 
in 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

333 
if swallowed then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

334 
edges 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

335 
else 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

336 
insert_edges edges 
16308  337 
(bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])]) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

338 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

339 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

340 

16308  341 
val edges = foldl make_edges Symtab.empty body 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

342 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

343 
(* We also have to add the backreferences that this new defnode induces. *) 
16308  344 
fun install_backrefs (graph, (noderef, links)) = 
345 
if links <> [] then 

346 
let 

16361  347 
val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

348 
val _ = if closed = Final then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

349 
sys_error ("install_backrefs: closed node cannot be updated") 
16361  350 
else () 
16308  351 
val defnames = 
17412  352 
(case Symtab.lookup backs mainref of 
16308  353 
NONE => Symtab.empty 
354 
 SOME s => s) 

17412  355 
val defnames' = Symtab.update_new (axname, ()) defnames 
356 
val backs' = Symtab.update (mainref, defnames') backs 

16308  357 
in 
17412  358 
Symtab.update (noderef, Node (ty, defs, backs', finals, closed)) graph 
16308  359 
end 
360 
else 

361 
graph 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

362 

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

363 
val graph = Symtab.foldl install_backrefs (graph, edges) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

364 

16361  365 
val (Node (_, _, backs, _, closed)) = getnode graph mainref 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

366 
val closed = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

367 
if closed = Final then sys_error "define: closed node" 
16361  368 
else if closed = Open andalso is_instance_r gty ty then Closed else closed 
369 

16308  370 
val thisDefnode = Defnode (ty, edges) 
17412  371 
val graph = Symtab.update (mainref, Node (gty, Symtab.update_new 
17223  372 
(axname, thisDefnode) defs, backs, finals, closed)) graph 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

373 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

374 
(* Now we have to check all backreferences to this node and inform them about 
16308  375 
the new defnode. In this section we also check for circularity. *) 
376 
fun update_backrefs ((backs, graph), (noderef, defnames)) = 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

377 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

378 
fun update_defs ((defnames, graph),(defname, _)) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

379 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

380 
val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = 
16361  381 
getnode graph noderef 
382 
val _ = if closed = Final then sys_error "update_defs: closed node" else () 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

383 
val (Defnode (def_ty, defnode_edges)) = 
17412  384 
the (Symtab.lookup nodedefs defname) 
385 
val edges = the (Symtab.lookup defnode_edges mainref) 

16361  386 
val refclosed = ref false 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

387 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

388 
(* the type of thisDefnode is ty *) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

389 
fun update (e as (max, alpha, beta, history), (changed, edges)) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

390 
case unify_r max beta ty of 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

391 
NONE => (changed, e::edges) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

392 
 SOME (max', s_beta, s_ty) => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

393 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

394 
val alpha' = subst s_beta alpha 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

395 
val ty' = subst s_ty ty 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

396 
val _ = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

397 
if noderef = mainref andalso defname = axname then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

398 
(case unify alpha' ty' of 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

399 
NONE => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

400 
if (is_instance_r ty' alpha') then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

401 
raise (INFINITE_CHAIN ( 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

402 
(alpha', mainref, axname):: 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

403 
(subst_history s_beta history)@ 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

404 
[(ty', mainref, axname)])) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

405 
else () 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

406 
 SOME s => 
16308  407 
raise (CIRCULAR ( 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

408 
(subst s alpha', mainref, axname):: 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

409 
(subst_history s (subst_history s_beta history))@ 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

410 
[(subst s ty', mainref, axname)]))) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

411 
else () 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

412 
in 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

413 
if is_instance_r beta ty then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

414 
(true, edges) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

415 
else 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

416 
(changed, e::edges) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

417 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

418 

16308  419 
val (changed, edges') = foldl update (false, []) edges 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

420 
val defnames' = if edges' = [] then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

421 
defnames 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

422 
else 
17412  423 
Symtab.update (defname, ()) defnames 
16308  424 
in 
425 
if changed then 

426 
let 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

427 
val defnode_edges' = 
16308  428 
if edges' = [] then 
429 
Symtab.delete mainref defnode_edges 

430 
else 

17412  431 
Symtab.update (mainref, edges') defnode_edges 
16308  432 
val defnode' = Defnode (def_ty, defnode_edges') 
17412  433 
val nodedefs' = Symtab.update (defname, defnode') nodedefs 
16361  434 
val closed = if closed = Closed andalso Symtab.is_empty defnode_edges' 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

435 
andalso no_forwards nodedefs' 
16361  436 
then Final else closed 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

437 
val graph' = 
17412  438 
Symtab.update 
17223  439 
(noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph 
16308  440 
in 
441 
(defnames', graph') 

442 
end 

443 
else 

444 
(defnames', graph) 

445 
end 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

446 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

447 
val (defnames', graph') = Symtab.foldl update_defs 
16308  448 
((Symtab.empty, graph), defnames) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

449 
in 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

450 
if Symtab.is_empty defnames' then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

451 
(backs, graph') 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

452 
else 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

453 
let 
17412  454 
val backs' = Symtab.update_new (noderef, defnames') backs 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

455 
in 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

456 
(backs', graph') 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

457 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

458 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

459 

16308  460 
val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

461 

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

462 
(* If a Circular exception is thrown then we never reach this point. *) 
16361  463 
val (Node (gty, defs, _, finals, closed)) = getnode graph mainref 
464 
val closed = if closed = Closed andalso no_forwards defs then Final else closed 

17412  465 
val graph = Symtab.update (mainref, Node (gty, defs, backs, finals, closed)) graph 
16826  466 
val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

467 
in 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

468 
(cost+3, axmap, actions', graph) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

469 
end handle ex => translate_ex axmap ex 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

470 

16982  471 
fun define'' thy (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body = 
16308  472 
let 
16982  473 
val ty = checkT thy ty 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

474 
fun checkbody (n, t) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

475 
let 
16361  476 
val (Node (_, _, _,_, closed)) = getnode graph n 
477 
in 

478 
case closed of 

479 
Final => NONE 

16982  480 
 _ => SOME (n, checkT thy t) 
16361  481 
end 
482 
val body = distinct (List.mapPartial checkbody body) 

16826  483 
val (axmap, axname) = newaxname axmap orig_axname 
16308  484 
in 
16826  485 
define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body 
16308  486 
end 
487 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

488 
fun finalize' (cost, axmap, history, graph) (noderef, ty) = 
17412  489 
case Symtab.lookup graph noderef of 
16308  490 
NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") 
16361  491 
 SOME (Node (nodety, defs, backs, finals, closed)) => 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

492 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

493 
val _ = 
16308  494 
if (not (is_instance_r ty nodety)) then 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

495 
def_err ("only type instances of the declared constant "^ 
16308  496 
noderef^" can be finalized") 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

497 
else () 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

498 
val _ = Symtab.exists 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

499 
(fn (def_name, Defnode (def_ty, _)) => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

500 
if can_be_unified_r ty def_ty then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

501 
def_err ("cannot finalize constant "^noderef^ 
16308  502 
"; clash with definition "^def_name) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

503 
else 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

504 
false) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

505 
defs 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

506 

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

507 
fun update_finals [] = SOME [ty] 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

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

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

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

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

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

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

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

516 
else 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

517 
SOME (final_ty :: finals)) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

519 
case update_finals finals of 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

520 
NONE => (cost, axmap, history, graph) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

521 
 SOME finals => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

522 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

523 
val closed = if closed = Open andalso is_instance_r nodety ty then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

524 
Closed else 
16361  525 
closed 
17412  526 
val graph = Symtab.update (noderef, Node (nodety, defs, backs, finals, closed)) graph 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

527 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

528 
fun update_backref ((graph, backs), (backrefname, backdefnames)) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

529 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

530 
fun update_backdef ((graph, defnames), (backdefname, _)) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

531 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

532 
val (backnode as Node (backty, backdefs, backbacks, 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

533 
backfinals, backclosed)) = 
16308  534 
getnode graph backrefname 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

535 
val (Defnode (def_ty, all_edges)) = 
16308  536 
the (get_defnode backnode backdefname) 
537 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

538 
val (defnames', all_edges') = 
17412  539 
case Symtab.lookup all_edges noderef of 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

540 
NONE => sys_error "finalize: corrupt backref" 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

541 
 SOME edges => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

542 
let 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

543 
val edges' = List.filter (fn (_, _, beta, _) => 
16308  544 
not (is_instance_r beta ty)) edges 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

545 
in 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

546 
if edges' = [] then 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

547 
(defnames, Symtab.delete noderef all_edges) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

548 
else 
17412  549 
(Symtab.update (backdefname, ()) defnames, 
550 
Symtab.update (noderef, edges') all_edges) 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

551 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

552 
val defnode' = Defnode (def_ty, all_edges') 
17412  553 
val backdefs' = Symtab.update (backdefname, defnode') backdefs 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

554 
val backclosed' = if backclosed = Closed andalso 
16361  555 
Symtab.is_empty all_edges' 
556 
andalso no_forwards backdefs' 

557 
then Final else backclosed 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

558 
val backnode' = 
16361  559 
Node (backty, backdefs', backbacks, backfinals, backclosed') 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

560 
in 
17412  561 
(Symtab.update (backrefname, backnode') graph, defnames') 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

562 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

563 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

564 
val (graph', defnames') = 
16308  565 
Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

566 
in 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

567 
(graph', if Symtab.is_empty defnames' then backs 
17412  568 
else Symtab.update (backrefname, defnames') backs) 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

569 
end 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

570 
val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

571 
val Node ( _, defs, _, _, closed) = getnode graph' noderef 
16361  572 
val closed = if closed = Closed andalso no_forwards defs then Final else closed 
17412  573 
val graph' = Symtab.update (noderef, Node (nodety, defs, backs', 
17223  574 
finals, closed)) graph' 
16361  575 
val history' = (Finalize (noderef, ty)) :: history 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

576 
in 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

577 
(cost+1, axmap, history', graph') 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

579 
end 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

580 

16982  581 
fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty) 
16308  582 

16826  583 
fun update_axname ax orig_ax (cost, axmap, history, graph) = 
17412  584 
(cost, Symtab.update (ax, orig_ax) axmap, history, graph) 
16826  585 

16361  586 
fun merge' (Declare cty, g) = declare' g cty 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

587 
 merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = 
17412  588 
(case Symtab.lookup graph name of 
16826  589 
NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

590 
 SOME (Node (_, defs, _, _, _)) => 
17412  591 
(case Symtab.lookup defs axname of 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

592 
NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

593 
 SOME _ => g)) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

594 
 merge' (Finalize finals, g) = finalize' g finals 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

595 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

596 
fun merge'' (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) = 
16308  597 
if cost1 < cost2 then 
598 
foldr merge' g2 actions1 

599 
else 

600 
foldr merge' g1 actions2 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

601 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

602 
fun finals (_, _, history, graph) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

603 
Symtab.foldl 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

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

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

607 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

608 
fun overloading_info (_, axmap, _, graph) c = 
16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

609 
let 
17412  610 
fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup axmap ax), ty) 
16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

611 
in 
17412  612 
case Symtab.lookup graph c of 
16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

613 
NONE => NONE 
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

614 
 SOME (Node (ty, defnodes, _, _, state)) => 
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

615 
SOME (ty, map translate (Symtab.dest defnodes), state) 
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

616 
end 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

617 

16982  618 

619 
(* monomorphic consts  neither parametric nor adhoc polymorphism *) 

620 

621 
fun monomorphicT (Type (_, Ts)) = forall monomorphicT Ts 

622 
 monomorphicT _ = false 

623 

624 
fun monomorphic (_, _, _, graph) c = 

17412  625 
(case Symtab.lookup graph c of 
16982  626 
NONE => true 
627 
 SOME (Node (ty, defnodes, _, _, _)) => 

628 
Symtab.min_key defnodes = Symtab.max_key defnodes andalso 

629 
monomorphicT ty); 

16743
21dbff595bf6
1) all theorems in Orderings can now be given as a parameter
obua
parents:
16384
diff
changeset

630 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

631 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

632 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

633 
(** diagnostics **) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

634 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

635 
fun pretty_const pp (c, T) = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

636 
[Pretty.str c, Pretty.str " ::", Pretty.brk 1, 
16936
93772bd33871
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
wenzelm
parents:
16877
diff
changeset

637 
Pretty.quote (Pretty.typ pp (Type.freeze_type (Term.zero_var_indexesT T)))]; 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

638 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

639 
fun pretty_path pp path = fold_rev (fn (T, c, def) => 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

640 
fn [] => [Pretty.block (pretty_const pp (c, T))] 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

641 
 prts => Pretty.block (pretty_const pp (c, T) @ 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

642 
[Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path []; 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

643 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

644 
fun defs_circular pp path = 
16982  645 
Pretty.str "Cyclic dependency of definitions: " :: pretty_path pp path 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

646 
> Pretty.chunks > Pretty.string_of; 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

647 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

648 
fun defs_infinite_chain pp path = 
16982  649 
Pretty.str "Infinite chain of definitions: " :: pretty_path pp path 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

650 
> Pretty.chunks > Pretty.string_of; 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

651 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

652 
fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2; 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

653 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

654 
fun defs_final pp const = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

655 
(Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

656 
> Pretty.block > Pretty.string_of; 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

657 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

658 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

659 
(* external interfaces *) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

660 

16982  661 
fun declare thy const defs = 
662 
if_none (try (declare'' thy defs) const) defs; 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

663 

16982  664 
fun define thy const name rhs defs = 
665 
define'' thy defs const name rhs 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

666 
handle DEFS msg => sys_error msg 
16982  667 
 CIRCULAR path => error (defs_circular (Sign.pp thy) path) 
668 
 INFINITE_CHAIN path => error (defs_infinite_chain (Sign.pp thy) path) 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

669 
 CLASH (_, def1, def2) => error (defs_clash def1 def2) 
16982  670 
 FINAL const => error (defs_final (Sign.pp thy) const); 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

671 

16982  672 
fun finalize thy const defs = 
673 
finalize'' thy defs const handle DEFS msg => sys_error msg; 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

674 

e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

675 
fun merge pp defs1 defs2 = 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

676 
merge'' defs1 defs2 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

677 
handle CIRCULAR namess => error (defs_circular pp namess) 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

678 
 INFINITE_CHAIN namess => error (defs_infinite_chain pp namess); 
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

679 

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

680 
end; 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

681 

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

683 

16308  684 
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

685 

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

686 
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

687 
val int = Type ("int", []) 
16308  688 
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

689 
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

690 
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

691 
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

692 
fun pair a b = Type ("pair", [a,b]) 
16308  693 
fun prm a = Type ("prm", [a]) 
694 
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

695 

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

696 
val _ = print "make empty" 
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

697 
val g = Defs.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

698 

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

701 

702 
val _ = print "declare permF" 

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

704 

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

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

706 
val g = Defs.define g ("perm", prm alpha > (beta > gamma) > (beta > gamma)) "perm_fun" 
16308  707 
[("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

708 

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

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

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

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

714 
("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

715 

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

718 
[("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

719 

16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset

720 
*) 