author  obua 
Mon, 13 Jun 2005 21:28:57 +0200  
changeset 16384  90c51c932154 
parent 16361  cb31cb768a6c 
child 16743  21dbff595bf6 
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 

16361  45 
datatype forwardstate = Open  Closed  Final 
46 

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

47 
datatype node = Node of 
16308  48 
typ (* most general type of constant *) 
16361  49 
* defnode Symtab.table 
16308  50 
(* a table of defnodes, each corresponding to 1 definition of the 
51 
constant for a particular type, indexed by axiom name *) 

52 
* (unit Symtab.table) Symtab.table 

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

54 
indexed by node name of the defnodes *) 

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

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

57 

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

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

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

61 

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

62 
fun getnode graph noderef = the (Symtab.lookup (graph, noderef)) 
16361  63 
fun get_nodedefs (Node (_, defs, _, _, _)) = defs 
64 
fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname) 

16308  65 
fun get_defnode' graph noderef defname = 
66 
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

67 

16361  68 
fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table) 
69 

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

71 
 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

72 
 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

73 

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

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

75 

16308  76 
val CHAIN_HISTORY = 
77 
let 

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

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

80 
in 

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

82 
end 

83 

84 
fun set_chain_history b = CHAIN_HISTORY := b 

85 
fun chain_history () = !CHAIN_HISTORY 

86 

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

87 
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

88 

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

89 
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

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

91 
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

92 
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

93 
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

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

96 

16361  97 
fun no_forwards defs = 
98 
Symtab.foldl 

99 
(fn (closed, (_, Defnode (_, edges))) => 

100 
if not closed then false else Symtab.is_empty edges) 

101 
(true, defs) 

102 

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

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

104 

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

105 
fun map_nc f list = 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

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

107 
val changed = ref false 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

108 
fun f' x = 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

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

110 
val x' = f x 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

111 
val _ = changed := true 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

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

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

114 
end handle No_Change => x 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

115 
val list' = map f' list 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

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

117 
if !changed then list' else raise No_Change 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

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

119 

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

120 
fun checkT' (t as (Type (a, Ts))) = (Type (a, map_nc checkT' Ts) handle No_Change => t) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

121 
 checkT' (t as (TVar ((a, 0), []))) = raise No_Change 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

122 
 checkT' (t as (TVar ((a, 0), _))) = TVar ((a, 0), []) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

123 
 checkT' (t as (TFree (a, _))) = TVar ((a, 0), []) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

124 
 checkT' _ = def_err "type is not clean" 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

125 

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

126 
fun checkT t = Term.compress_type (checkT' t handle No_Change => t) 
16308  127 

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

129 

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

130 
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

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

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

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

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

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

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

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

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

139 
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

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

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

142 

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 
fun subst s ty = Envir.norm_type s ty 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

144 

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

145 
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

146 

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

147 
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

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

149 

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

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

152 

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

153 
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

154 
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

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

156 

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

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

160 
equal to max. 

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

162 
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

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

164 
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

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

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

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

169 
val max = Int.max(max, Int.max (max1, max2)) 
16308  170 
val (ty1, s1) = subst_incr_tvar (max + 1) ty1 
171 
val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2 

172 
val max = max + max1 + max2 + 2 

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

173 
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

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

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

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

177 
 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

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

179 

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

180 
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

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

182 
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

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

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

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

186 
 _ => 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

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

188 

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

189 
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

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

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

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

193 

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

195 

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

198 
let 

199 

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

201 
foldr 

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

203 
let 

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

205 
val e = inject_ty (ty, e) 

206 
in 

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

208 
end) 

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

210 

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

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

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

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

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

216 
let 

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

218 
in 

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

220 
end 

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

222 

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

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

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

226 
idxlist idx 

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

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

229 
(tab, max) history 

230 
in 

231 
(max, u1, v1, history) 

232 
end 

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

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

236 
val t1 = u1 > v1 
16308  237 
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

238 
in 
16308  239 
if (is_instance t1 t2) then 
240 
(if is_instance t2 t1 then 

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

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

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

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

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

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

247 
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

248 
end 
16308  249 

250 
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

251 
 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

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

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

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

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

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

257 

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

258 
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

259 

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

260 
fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

261 
(cost, axmap, (Declare cty)::actions, 
16361  262 
Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph)) 
263 
handle Symtab.DUP _ => 

264 
let 

265 
val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name)) 

266 
in 

267 
if is_instance_r ty gty andalso is_instance_r gty ty then 

268 
g 

269 
else 

270 
def_err "constant is already declared with different type" 

271 
end 

272 

273 
fun declare g (name, ty) = declare' g (name, checkT ty) 

274 

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

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

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

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

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

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

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

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

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

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

284 

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

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

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

287 
fun translate (ty, nodename, axname) = 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

288 
(ty, nodename, the (Symtab.lookup (axmap, axname))) 
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

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

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

291 
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

292 
 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

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

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

295 

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

296 
fun define' (cost, axmap, 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

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

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

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

300 
 SOME n => n) 
16361  301 
val (Node (gty, defs, backs, finals, _)) = mainnode 
16308  302 
val _ = (if is_instance_r ty gty then () 
303 
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

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

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

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

308 
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

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

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

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

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

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

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

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

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

317 

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

16361  320 

16308  321 
fun insert_edges edges (nodename, links) = 
322 
(if links = [] then 

323 
edges 

324 
else 

325 
let 

326 
val links = map normalize_edge_idx links 

327 
in 

328 
Symtab.update ((nodename, 

329 
case Symtab.lookup (edges, nodename) of 

330 
NONE => links 

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

332 
edges) 

333 
end) 

334 

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

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

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

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

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

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

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

342 
in 
16361  343 
if closed = Final then edges else 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

346 
 SOME (maxidx, sigma1, sigma2) => 
16308  347 
if exists (is_instance_r bodyty) bfinals then 
348 
edges 

349 
else 

350 
let 

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

352 
let 

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

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

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

356 
NONE => NONE 

357 
 SOME (max, sleft, sright) => 

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

359 
if !CHAIN_HISTORY then 

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

361 
(subst_history sright history)) 

362 
else []) 

363 
val links' = List.mapPartial connect links 

364 
in 

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

366 
end 

367 

368 
fun make_edges' ((swallowed, edges), 

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

370 
if swallowed then 

371 
(swallowed, edges) 

372 
else 

373 
(case unify_r 0 bodyty def_ty of 

374 
NONE => (swallowed, edges) 

375 
 SOME (maxidx, sigma1, sigma2) => 

376 
(is_instance_r bodyty def_ty, 

377 
snd (Symtab.foldl insert_trans_edges 

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

379 
edges), def_edges)))) 

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

381 
in 

382 
if swallowed then 

383 
edges 

384 
else 

385 
insert_edges edges 

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

387 
end 

16361  388 
end 
389 

16308  390 
val edges = foldl make_edges Symtab.empty body 
391 

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

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

394 
if links <> [] then 

395 
let 

16361  396 
val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef 
397 
val _ = if closed = Final then 

398 
sys_error ("install_backrefs: closed node cannot be updated") 

399 
else () 

16308  400 
val defnames = 
401 
(case Symtab.lookup (backs, mainref) of 

402 
NONE => Symtab.empty 

403 
 SOME s => s) 

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

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

406 
in 

16361  407 
Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph) 
16308  408 
end 
409 
else 

410 
graph 

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

411 

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

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

413 

16361  414 
val (Node (_, _, backs, _, closed)) = getnode graph mainref 
415 
val closed = 

416 
if closed = Final then sys_error "define: closed node" 

417 
else if closed = Open andalso is_instance_r gty ty then Closed else closed 

418 

16308  419 
val thisDefnode = Defnode (ty, edges) 
420 
val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new 

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

422 

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

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

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

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

428 
let 
16361  429 
val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = 
430 
getnode graph noderef 

431 
val _ = if closed = Final then sys_error "update_defs: closed node" else () 

16308  432 
val (Defnode (def_ty, defnode_edges)) = 
433 
the (Symtab.lookup (nodedefs, defname)) 

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

16361  435 
val refclosed = ref false 
16308  436 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

454 
else () 
16308  455 
 SOME s => 
456 
raise (CIRCULAR ( 

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

458 
(subst_history s (subst_history s_beta history))@ 

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

460 
else () 

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

461 
in 
16308  462 
if is_instance_r beta ty then 
463 
(true, edges) 

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

464 
else 
16308  465 
(changed, e::edges) 
466 
end 

467 

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

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

470 
defnames 

471 
else 

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

473 
in 

474 
if changed then 

475 
let 

476 
val defnode_edges' = 

477 
if edges' = [] then 

478 
Symtab.delete mainref defnode_edges 

479 
else 

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

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

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

16361  483 
val closed = if closed = Closed andalso Symtab.is_empty defnode_edges' 
484 
andalso no_forwards nodedefs' 

485 
then Final else closed 

16308  486 
val graph' = 
487 
Symtab.update 

16361  488 
((noderef, 
489 
Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph) 

16308  490 
in 
491 
(defnames', graph') 

492 
end 

493 
else 

494 
(defnames', graph) 

495 
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

496 

16308  497 
val (defnames', graph') = Symtab.foldl update_defs 
498 
((Symtab.empty, graph), defnames) 

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

499 
in 
16308  500 
if Symtab.is_empty defnames' then 
501 
(backs, graph') 

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

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

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

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

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

508 
end 
16308  509 

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

511 

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

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

515 
val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) 

516 
val actions' = (Define (mainref, ty, axname, body))::actions 

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

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

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

519 
end handle ex => translate_ex axmap ex 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

520 

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

521 
fun define (g as (cost, axmap, actions, graph)) (mainref, ty) axname body = 
16308  522 
let 
523 
val ty = checkT ty 

16361  524 
fun checkbody (n, t) = 
525 
let 

526 
val (Node (_, _, _,_, closed)) = getnode graph n 

527 
in 

528 
case closed of 

529 
Final => NONE 

530 
 _ => SOME (n, checkT t) 

531 
end 

532 
val body = distinct (List.mapPartial checkbody body) 

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

533 
val (axmap, axname) = newaxname axmap axname 
16308  534 
in 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

535 
define' (cost, axmap, actions, graph) (mainref, ty) axname body 
16308  536 
end 
537 

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

538 
fun finalize' (cost, axmap, history, graph) (noderef, ty) = 
16308  539 
case Symtab.lookup (graph, noderef) of 
540 
NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") 

16361  541 
 SOME (Node (nodety, defs, backs, finals, closed)) => 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

542 
let 
16308  543 
val _ = 
544 
if (not (is_instance_r ty nodety)) then 

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

546 
noderef^" can be finalized") 

547 
else () 

548 
val _ = Symtab.exists 

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

550 
if can_be_unified_r ty def_ty then 

551 
def_err ("cannot finalize constant "^noderef^ 

552 
"; clash with definition "^def_name) 

553 
else 

554 
false) 

555 
defs 

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

556 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

570 
NONE => (cost, axmap, history, graph) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

572 
let 
16361  573 
val closed = if closed = Open andalso is_instance_r nodety ty then 
574 
Closed else 

575 
closed 

576 
val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)), 

16308  577 
graph) 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

578 

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

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

581 
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

582 
let 
16361  583 
val (backnode as Node (backty, backdefs, backbacks, 
584 
backfinals, backclosed)) = 

16308  585 
getnode graph backrefname 
586 
val (Defnode (def_ty, all_edges)) = 

587 
the (get_defnode backnode backdefname) 

588 

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

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

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

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

593 
let 
16308  594 
val edges' = List.filter (fn (_, _, beta, _) => 
595 
not (is_instance_r beta ty)) edges 

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

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

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

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

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

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

603 
val defnode' = Defnode (def_ty, all_edges') 
16361  604 
val backdefs' = Symtab.update ((backdefname, defnode'), backdefs) 
605 
val backclosed' = if backclosed = Closed andalso 

606 
Symtab.is_empty all_edges' 

607 
andalso no_forwards backdefs' 

608 
then Final else backclosed 

16308  609 
val backnode' = 
16361  610 
Node (backty, backdefs', backbacks, backfinals, backclosed') 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

611 
in 
16308  612 
(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

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

614 

16308  615 
val (graph', defnames') = 
616 
Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) 

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

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

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

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

621 
val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) 
16361  622 
val Node ( _, defs, _, _, closed) = getnode graph' noderef 
623 
val closed = if closed = Closed andalso no_forwards defs then Final else closed 

624 
val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', 

625 
finals, closed)), graph') 

626 
val history' = (Finalize (noderef, ty)) :: history 

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

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

628 
(cost+1, axmap, history', graph') 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

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

630 
end 
16308  631 

16361  632 
fun finalize g (noderef, ty) = finalize' g (noderef, checkT ty) 
16308  633 

16361  634 
fun merge' (Declare cty, g) = declare' g cty 
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset

635 
 merge' (Define (name, ty, axname, body), g as (_,_, _, graph)) = 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

636 
(case Symtab.lookup (graph, name) of 
16308  637 
NONE => define' g (name, ty) axname body 
16361  638 
 SOME (Node (_, defs, _, _, _)) => 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

643 

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

644 
fun merge (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) = 
16308  645 
if cost1 < cost2 then 
646 
foldr merge' g2 actions1 

647 
else 

648 
foldr merge' g1 actions2 

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

649 

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

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

651 
Symtab.foldl 
16361  652 
(fn (finals, (name, Node(_, _, _, ftys, _))) => 
653 
Symtab.update_new ((name, ftys), finals)) 

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

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

655 

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

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

657 

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

659 

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

661 

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

662 
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

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

665 
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

666 
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

667 
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

668 
fun pair a b = Type ("pair", [a,b]) 
16308  669 
fun prm a = Type ("prm", [a]) 
670 
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

671 

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

672 
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

673 
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

674 

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

677 

678 
val _ = print "declare permF" 

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

680 

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

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

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

684 

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

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

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

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

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

691 

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

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

695 

16308  696 
*) 