author  obua 
Sun, 29 May 2005 12:39:12 +0200  
changeset 16108  cf468b93a02e 
child 16113  692fe6595755 
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 

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

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

13 

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

14 
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

15 
exception CIRCULAR of (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

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

17 

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

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

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

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

21 

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

22 
(* the first argument should be the smaller graph *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

24 

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

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

26 

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

27 
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

28 

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

29 
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

30 
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

31 
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

32 

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

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

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

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

36 
* defnode Symtab.table (* a table of defnodes, each corresponding to 1 definition of the constant for a particular type, 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

38 
* backref Symtab.table (* a table of all back references to this node, indexed by node name *) 
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 
and defnode = Defnode of 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

41 
typ (* type of the constant in this particular definition *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

42 
* ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

43 

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

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

45 
noderef (* a reference to the node that has defnodes which reference a certain node A *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

47 

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

48 
fun getnode graph noderef = the (Symtab.lookup (graph, noderef)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

51 
fun get_defnode (Node (_, _, defs, _)) defname = Symtab.lookup (defs, defname) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

52 
fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

54 

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 t2list t = rev (Symtab.foldl (fn (l, d) => d::l) ([], t)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

57 
fun tmap f t = map (fn (a,b) => (a, f b)) t 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

58 
fun defnode2data (Defnode (typ, table)) = ("Defnode", typ, t2list table) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

59 
fun backref2data (Backref (noderef, table)) = ("Backref", noderef, map fst (t2list table)) 
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 node2data (Node (s, t, defs, backs)) = ("Node", ("nodename", s), ("nodetyp", t), 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

61 
("defs", tmap defnode2data (t2list defs)), ("backs", tmap backref2data (t2list backs))) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

62 
fun graph2data g = ("Graph", tmap node2data (t2list g)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

64 

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

65 
datatype graphaction = Declare of string * typ  Define of string * typ * string * (string * typ) list 
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) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

68 

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; 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

74 

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

75 
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

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 declare (actions, g) name ty = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

79 
Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty)), g)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

81 

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

82 
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

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

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

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

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

88 
val t' = 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

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

90 
Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

92 
(t',List.foldl update_subst Vartab.empty tv) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

96 

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

97 
(* 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

98 
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

99 
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

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

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

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

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

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

106 

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

107 
fun subst s ty = Envir.norm_type s ty 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

108 

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_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

110 

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

112 
Type.typ_instance Type.empty_tsig (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

113 

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

114 
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

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

116 

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

117 
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

118 
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

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

120 

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

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

122 
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

123 
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

124 
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

125 
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

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

127 
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

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

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

130 
val max1 = max (* >= maxidx_of_typ ty1 *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

131 
val max2 = max (* >= maxidx_of_typ ty2 *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

133 
val (ty1, s1) = subst_incr_tvar (max+1) ty1 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

134 
val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

135 
val max = max+max1+max2+2 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

136 
fun merge a b = Vartab.merge (fn _ => false) (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

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

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

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

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

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

142 

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

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

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

145 
val ty2 = rename 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 
in 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

151 

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

152 
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

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

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

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

156 

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

157 
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

158 
 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

159 
 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

160 
 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

161 

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

162 
fun forall_table P tab = Symtab.foldl (fn (true, e) => P e  (b, _) => b) (true, tab); 
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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

172 
val t2 = u2 > v2 
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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

178 
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

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

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

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

182 
NONE 
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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

184 

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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

188 
SOME LESS => (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

189 
 SOME EQUAL => (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

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

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

192 

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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

201 
LESS => (l1, e1)::(merge_labelled_edges 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

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

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

204 

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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

209 
foldl (fn ((s, edges), b') => 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

210 
(foldl (fn (e, b'') => f ty n s e b'') b' edges)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

212 
labelled_edges 
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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

214 
Symtab.foldl g (a, def_edges) 
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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

216 

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

217 
fun define (actions, graph) name ty axname body = 
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 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

220 
val body = map (fn (n,t) => (n, checkT t)) body 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

222 
val mainnode = (case Symtab.lookup (graph, mainref) of 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

223 
NONE => def_err ("constant "^(quote mainref)^" is not declared") 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

225 
val (Node (n, gty, defs, backs)) = mainnode 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

226 
val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type") 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

227 
fun check_def (s, Defnode (ty', _)) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

231 
def_err "name of axiom is already used for another definition of this constant" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

235 

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

236 
(* body contains the constants that this constant definition depends on. For each element of body, 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

237 
the function make_edges_to calculates a group of edges that connect this constant with 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

238 
the constant that is denoted by the element of the body *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

243 
NONE => def_err "body of constant definition references undeclared constant" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

245 
val (Node (_, general_btyp, bdefs, bbacks)) = bnode 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

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

252 
(* For each definition of the constant in the body, 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

253 
check if the definition unifies with the type of the constant in the body. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

254 
fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

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

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

262 
merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])])) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

263 
val (swallowed, edges) = Symtab.foldl make_edges ((false, []), bdefs) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

268 
(bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

271 

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

272 
fun update_edges (b as (bodyn, bodyty), edges) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

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

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

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

281 
val es = 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

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

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

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

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

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

287 

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

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

289 

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

290 
fun insert_edge edges (nodename, (defname_opt, edge)) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

303 

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

304 
(* We constructed all direct edges that this defnode has. 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

305 
Now we have to construct the transitive hull by going a single step further. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

306 

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

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

308 

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

309 
fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

314 
val defnode = the (get_defnode' graph noderef defname) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

315 
fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

316 
case unify_r (Int.max (max1, max2)) beta1 alpha2 of 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

328 

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

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

330 

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

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

332 

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

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

334 

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

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

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

337 

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

338 
fun install_backref graph noderef pointingnoderef pointingdefname = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

340 
val (Node (pname, _, _, _)) = getnode graph pointingnoderef 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

341 
val (Node (name, ty, defs, backs)) = getnode graph noderef 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

346 
val defnames = Symtab.update ((pointingdefname, ()), 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

347 
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

349 
Symtab.update ((name, Node (name, ty, defs, backs)), graph) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

354 
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

356 
Symtab.update ((name, Node (name, ty, defs, backs)), graph) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

358 
handle Symtab.DUP _ => graph 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

360 

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

361 
fun install_backrefs (graph, (_, (noderef, labelled_edges))) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

366 

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

367 
val graph = Symtab.foldl install_backrefs (graph, edges) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

368 

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

369 
val (Node (_, _, _, backs)) = getnode graph mainref 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

370 
val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new ((axname, thisDefnode), defs), backs)), graph) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

371 

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

372 
(* Now we have to check all backreferences to this node and inform them about the new defnode. 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

373 
In this section we also check for circularity. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

374 
fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

377 
fun update_defs ((defnames, newedges),(defname, _)) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

379 
val (Defnode (_, defnode_edges)) = the (get_defnode node defname) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

380 
val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

381 

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

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

383 
fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

386 
 SOME (max', s_beta, s_ty) => 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

391 
if noderef = mainref andalso defname = axname then 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

397 
[(subst s ty', mainref, axname)]))) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

399 
val edge = (max', alpha', ty', subst_history s_beta history) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

410 
val (none_edges, this_edges) = foldl update ([], []) edges 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

415 
 _ => def_err "update_defs, internal error, corrupt backrefs" 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

417 

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

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

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

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

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

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

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

424 
val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

429 

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

430 

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

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

432 

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

433 
(* If a Circular exception is thrown then we never reach this point. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

434 
(* Ok, the definition is consistent, let's update this node. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

435 
val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update ((axname, thisDefnode), defs), backs)), graph) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

436 

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

437 
(* Furthermore, update all the other nodes that backreference this node. *) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

438 
fun final_update_backrefs graph noderef defname none_edges this_edges = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

441 
val (Node (nodename, nodety, defs, backs)) = node 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

442 
val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

443 
val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n)) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

444 

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

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

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

447 
val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)] 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

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

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

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

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

454 

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

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

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

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

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

459 
val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

460 
val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

462 
Symtab.update ((nodename, Node (nodename, nodety, defs', backs)), graph) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

464 

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

465 
val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) => 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

466 
final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

467 

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

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

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

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

471 

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

472 

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

473 
fun merge' (Declare (name, ty), g) = (declare g name ty handle _ => g) 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

474 
 merge' (Define (name, ty, axname, body), g as (_, graph)) = 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

476 
NONE => define g name ty axname body 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

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

479 
NONE => define g name ty axname body 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

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

481 

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

482 
fun merge (actions, _) g = foldr merge' g actions 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

483 

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

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

485 

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

486 

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

487 

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

488 
(*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

489 

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

490 
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

491 
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

492 
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

493 
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

494 
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

495 
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

496 

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

497 
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

498 
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

499 

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

500 
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

501 
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

502 
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

503 

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

504 
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

505 
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

506 
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

507 

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

508 
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

509 
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

510 

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

511 