author  obua 
Fri, 03 Jun 2005 01:08:07 +0200  
changeset 16198  cfd070a2cc4d 
parent 16177  1af9f5c69745 
child 16308  636a1a84977a 
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 

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

5 
Checks if definitions preserve consistency of logic by enforcing that there are no cyclic definitions. 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

7 
"Cyclefree Overloading in Isabelle", Steven Obua, technical report, to be written :) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

8 
*) 
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 
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

11 

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

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

13 

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

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

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

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

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

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

19 

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

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

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

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

23 
(* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

24 

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

25 
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

26 

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

27 
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

28 

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

29 
(* the first argument should be the smaller graph *) 
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 

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

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

33 

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

34 
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

35 

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

36 
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

37 
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

38 
type noderef = string 
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 
datatype node = Node of 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

41 
string (* name of constant *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

42 
* typ (* most general type of constant *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

43 
* defnode Symtab.table (* a table of defnodes, each corresponding to 1 definition of the 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

44 
constant for a particular type, indexed by axiom name *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

45 
* backref Symtab.table (* a table of all back references to this node, indexed by node name *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

47 

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

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

49 
typ (* type of the constant in this particular definition *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

50 
* ((noderef * (string option * edgelabel list) 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

51 

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

52 
and backref = Backref of 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

53 
noderef (* the name of the node that has defnodes which reference a certain node A *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

54 
* (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

55 

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

56 
fun getnode graph noderef = the (Symtab.lookup (graph, noderef)) 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

57 
fun get_nodename (Node (n, _, _ ,_, _)) = n 
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

58 
fun get_nodedefs (Node (_, _, defs, _, _)) = defs 
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

59 
fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, 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

60 
fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname) 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

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

62 

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

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

64 
 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

65 
 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

66 

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

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

68 

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

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

70 

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

71 
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

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

73 
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

74 
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

75 
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

76 

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

77 
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

78 

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

79 
fun declare (actions, g) (cty as (name, ty)) = 
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

80 
((Declare cty)::actions, 
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

81 
Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g)) 
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

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

83 

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

84 
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

85 

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

86 
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

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

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

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

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

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

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

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

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

95 
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

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

97 
(t, 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

98 

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

99 
(* Rename tys2 so that tys2 and tys1 do not have any variables in common any more. 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

100 
As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

104 
val (ty2', s) = subst_incr_tvar (max1 + 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

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

106 
(ty2', s, max1 + max2 + 1) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

108 

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

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

110 

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

111 
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

112 

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

113 
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

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

115 

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

116 
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

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

118 

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

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

120 
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

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

122 

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

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

124 
Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

125 
are different. All indices in ty1 and ty2 are supposed to be less than or equal to max. 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

126 
Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

127 
indices in s1, s2, 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

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

129 
fun unify_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

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

131 
val max = Int.max(max, 0) 
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)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

135 
val (ty1, s1) = subst_incr_tvar (max+1) ty1 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

136 
val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

137 
val max = max+max1+max2+2 
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 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

141 
NONE => NONE 
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 
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 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

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

147 
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

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

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

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

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

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

153 

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

154 
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

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

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

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

158 

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

159 
fun checkT (Type (a, Ts)) = Type (a, map checkT Ts) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

160 
 checkT (TVar ((a, 0), _)) = TVar ((a, 0), []) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

161 
 checkT (TVar ((a, i), _)) = def_err "type is not clean" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

162 
 checkT (TFree (a, _)) = TVar ((a, 0), []) 
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 label_ord NONE NONE = EQUAL 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

168 

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

169 
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

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

171 
val t1 = u1 > v1 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

172 
val t2 = 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

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

174 
if (is_instance_r t1 t2) then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

175 
(if is_instance_r t2 t1 then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

178 
SOME LESS) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

179 
else if (is_instance_r t2 t1) then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

182 
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

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

184 

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

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

186 
 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

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

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

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

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

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

192 

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

193 
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

194 

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

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

196 

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

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

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

199 
 merge_labelled_edges ((l1,e1)::es1) ((l2,e2)::es2) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

200 
(case label_ord l1 l2 of 
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

201 
LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

202 
 GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

203 
 EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

204 

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

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

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

207 
val (Defnode (ty, def_edges)) = defnode 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

208 
fun g (b, (_, (n, labelled_edges))) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

209 
foldl (fn ((s, edges), b') => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

210 
(foldl (fn (e, b'') => f ty n s e b'') b' edges)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

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

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

216 

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

217 
fun define (actions, graph) (name, 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

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

219 
val ty = checkT ty 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

220 
val body = map (fn (n,t) => (n, checkT t)) body 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

221 
val mainref = name 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

224 
 SOME n => n) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

225 
val (Node (n, gty, defs, backs, finals)) = mainnode 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

226 
val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type") 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

227 
fun check_def (s, Defnode (ty', _)) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

231 
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

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

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

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

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

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

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

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

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

240 

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

241 
(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

242 

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

243 
(* body contains the constants that this constant definition depends on. For each element of body, 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

244 
the function make_edges_to calculates a group of edges that connect this constant with 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

245 
the constant that is denoted by the element of the body *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

246 
fun make_edges_to (bodyn, bodyty) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

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

251 
 SOME x => x) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

252 
val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

254 
case unify_r 0 bodyty general_btyp of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

256 
 SOME (maxidx, sigma1, sigma2) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

259 
(* For each definition of the constant in the body, 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

260 
check if the definition unifies with the type of the constant in the body. *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

261 
fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

262 
if swallowed then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

263 
(swallowed, l) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

265 
(case unify_r 0 bodyty def_ty of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

266 
NONE => (swallowed, l) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

267 
 SOME (maxidx, sigma1, sigma2) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

268 
(is_instance_r bodyty def_ty, 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

269 
merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])])) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

270 
val swallowed = exists (is_instance_r bodyty) bfinals 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

271 
val (swallowed, edges) = Symtab.foldl make_edges ((swallowed, []), bdefs) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

273 
if swallowed then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

274 
(bodyn, edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

276 
(bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

279 

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

280 
fun update_edges (b as (bodyn, bodyty), edges) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

281 
(case make_edges_to b of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

285 
NONE => Symtab.update ((bodyn, m), edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

286 
 SOME (_, es') => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

288 
val (_, es) = m 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

289 
val es = merge_labelled_edges es es' 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

291 
Symtab.update ((bodyn, (bodyn, es)), edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

295 

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

296 
val edges = foldl update_edges Symtab.empty body 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

297 

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

298 
fun insert_edge edges (nodename, (defname_opt, edge)) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

300 
val newlink = [(defname_opt, [edge])] 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

302 
case Symtab.lookup (edges, nodename) of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

303 
NONE => Symtab.update ((nodename, (nodename, newlink)), edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

304 
 SOME (_, links) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

306 
val links' = merge_labelled_edges links newlink 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

308 
Symtab.update ((nodename, (nodename, links')), edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

311 

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

312 
(* We constructed all direct edges that this defnode has. 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

313 
Now we have to construct the transitive hull by going a single step further. *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

314 

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

315 
val thisDefnode = Defnode (ty, edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

316 

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

317 
fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

318 
case defname_opt of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

322 
val defnode = the (get_defnode' graph noderef defname) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

323 
fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

324 
case unify_r (Int.max (max1, max2)) beta1 alpha2 of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

326 
 SOME (max, sleft, sright) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

327 
insert_edge edges (noderef2, 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

328 
(defname_opt2, 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

329 
(max, subst sleft alpha1, subst sright beta2, 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

330 
(subst_history sleft history1)@ 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

331 
((subst sleft beta1, noderef, defname):: 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

334 
defnode_edges_foldl make_trans_edge edges defnode 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

336 

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

337 
val edges = defnode_edges_foldl make_trans_edges edges thisDefnode 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

338 

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

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

340 

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

341 
(* We also have to add the backreferences that this new defnode induces. *) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

342 

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

343 
fun hasNONElink ((NONE, _)::_) = true 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

344 
 hasNONElink _ = false 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

345 

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

346 
fun install_backref graph noderef pointingnoderef pointingdefname = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

348 
val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

349 
val (Node (name, ty, defs, backs, finals)) = getnode graph noderef 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

351 
case Symtab.lookup (backs, pname) of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

354 
val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

355 
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

357 
Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

359 
 SOME (Backref (pointingnoderef, defnames)) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

361 
val defnames = Symtab.update_new ((pointingdefname, ()), defnames) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

362 
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

364 
Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

366 
handle Symtab.DUP _ => graph 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

368 

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

369 
fun install_backrefs (graph, (_, (noderef, labelled_edges))) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

370 
if hasNONElink labelled_edges then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

371 
install_backref graph noderef mainref axname 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

374 

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

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

376 

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

377 
val (Node (_, _, _, backs, _)) = getnode graph mainref 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

378 
val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

380 

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

381 
(* Now we have to check all backreferences to this node and inform them about the new defnode. 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

382 
In this section we also check for circularity. *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

383 
fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

385 
val node = getnode graph noderef 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

386 
fun update_defs ((defnames, newedges),(defname, _)) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

388 
val (Defnode (_, defnode_edges)) = the (get_defnode node defname) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

389 
val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

390 

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

391 
(* the type of thisDefnode is ty *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

392 
fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

393 
case unify_r max beta ty of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

394 
NONE => (e::none_edges, this_edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

409 
 SOME s => raise (CIRCULAR ( 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

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

414 
val edge = (max', alpha', ty', subst_history s_beta history) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

416 
if is_instance_r beta ty then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

417 
(none_edges, edge::this_edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

419 
(e::none_edges, edge::this_edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

422 
case labelled_edges of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

425 
val (none_edges, this_edges) = foldl update ([], []) edges 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

426 
val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

428 
(defnames, (defname, none_edges, this_edges)::newedges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

430 
 _ => sys_error "define: update_defs, internal error, corrupt backrefs" 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

431 
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

432 

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

433 
val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

435 
if Symtab.is_empty defnames then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

436 
(backs, (noderef, newedges')::newedges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

439 
val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

441 
(backs, newedges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

444 

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

445 

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

446 
val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

447 

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

448 
(* If a Circular exception is thrown then we never reach this point. *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

449 
(* Ok, the definition is consistent, let's update this node. *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

450 
val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

452 

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

453 
(* Furthermore, update all the other nodes that backreference this node. *) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

454 
fun final_update_backrefs graph noderef defname none_edges this_edges = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

456 
val node = getnode graph noderef 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

457 
val (Node (nodename, nodety, defs, backs, finals)) = node 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

458 
val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

459 
val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

460 

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

461 
fun update edges none_edges this_edges = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

463 
val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)] 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

465 
if none_edges = [] then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

468 
(NONE, pack_edges none_edges)::u 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

470 

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

471 
val defnode_links' = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

472 
case defnode_links of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

473 
((NONE, _) :: edges) => update edges none_edges this_edges 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

474 
 edges => update edges none_edges this_edges 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

475 
val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

476 
val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

478 
Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

480 

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

481 
val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

482 
final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

483 

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

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

485 
((Define (name, ty, axname, body))::actions, graph) 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

487 

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

488 
fun finalize (history, graph) (c, ty) = 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

490 
NONE => def_err ("cannot finalize constant "^c^"; it is not declared") 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

493 
val ty = checkT ty 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

494 
val _ = if (not (is_instance_r ty nodety)) then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

495 
def_err ("only type instances of the declared constant "^c^" can be finalized") 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

497 
val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

498 
if can_be_unified_r ty def_ty then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

499 
def_err ("cannot finalize constant "^c^"; clash with definition "^def_name) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

503 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

520 
val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

521 

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

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

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

524 
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

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

526 
val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

527 
val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

530 
NONE => sys_error "finalize: corrupt backref" 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

531 
 SOME (_, (NONE, edges)::rest) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

533 
val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

535 
if edges' = [] then 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

536 
(defnames, Symtab.update ((noderef, (noderef, rest)), all_edges)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

538 
(Symtab.update ((backdefname, ()), defnames), 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

539 
Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

541 
val defnode' = Defnode (def_ty, all_edges') 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

542 
val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

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

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

547 

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

548 
val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

550 
(graph', if Symtab.is_empty defnames' then backs 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

551 
else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

553 
val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

554 
val Node (_, _, defs, _, _) = getnode graph' noderef 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

556 
((Finalize (c, ty)) :: history, Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')) 
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset

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

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

559 

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

560 
fun merge' (Declare cty, g) = (declare g cty handle _ => g) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

563 
NONE => define g (name, ty) axname body 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

564 
 SOME (Node (_, _, defs, _, _)) => 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

565 
(case Symtab.lookup (defs, axname) of 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

566 
NONE => define g (name, ty) axname body 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

567 
 SOME _ => g)) 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

568 
 merge' (Finalize finals, g) = finalize g finals 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

569 

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

570 
fun merge (actions, _) g = foldr merge' g actions 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

571 

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

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

573 
Symtab.foldl 
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset

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

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

576 

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

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

578 

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

579 

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

580 

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

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

582 

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

583 
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

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

585 
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

586 
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

587 
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

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

589 

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

590 
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

591 
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

592 

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

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

594 
val g = Defs.declare g "M" (alpha > bool) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

595 
val g = Defs.declare g "N" (beta > bool) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

596 

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

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

598 
val g = Defs.define g "N" (alpha > bool) "defN" [("M", alpha > bool)] 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

599 
val g = Defs.define g "M" (alpha > bool) "defM" [("N", int > alpha)] 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

600 

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

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

602 
val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

603 

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

604 