author | obua |
Fri, 03 Jun 2005 01:08:07 +0200 | |
changeset 16198 | cfd070a2cc4d |
parent 16177 | 1af9f5c69745 |
child 16308 | 636a1a84977a |
permissions | -rw-r--r-- |
16108
cf468b93a02e
Implement cycle-free 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 cycle-free 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 cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
4 |
|
cf468b93a02e
Implement cycle-free 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 cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
7 |
"Cycle-free Overloading in Isabelle", Steven Obua, technical report, to be written :-) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
8 |
*) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
9 |
|
cf468b93a02e
Implement cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
11 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
12 |
type graph |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
13 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
14 |
exception DEFS of string |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
15 |
exception CIRCULAR of (typ * string * string) list |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
16 |
exception INFINITE_CHAIN of (typ * string * string) list |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
17 |
exception FINAL of string * typ |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
18 |
exception CLASH of string * string * string |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
19 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
20 |
val empty : graph |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
21 |
val declare : graph -> string * typ -> graph (* exception DEFS *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
22 |
val define : graph -> string * typ -> string -> (string * typ) list -> graph |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
23 |
(* exception DEFS, CIRCULAR, INFINITE_CHAIN, CLASH, FINAL *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
24 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
25 |
val finalize : graph -> string * typ -> graph (* exception DEFS *) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
26 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
27 |
val finals : graph -> (typ list) Symtab.table |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
28 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
29 |
(* the first argument should be the smaller graph *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
30 |
val merge : graph -> graph -> graph (* exception CIRCULAR, INFINITE_CHAIN, CLASH *) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
31 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
32 |
end |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
33 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
34 |
structure Defs :> DEFS = struct |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
35 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
36 |
type tyenv = Type.tyenv |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
37 |
type edgelabel = (int * typ * typ * (typ * string * string) list) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
38 |
type noderef = string |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
39 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
40 |
datatype node = Node of |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
41 |
string (* name of constant *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
42 |
* typ (* most general type of constant *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
43 |
* defnode Symtab.table (* a table of defnodes, each corresponding to 1 definition of the |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
44 |
constant for a particular type, indexed by axiom name *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
45 |
* backref Symtab.table (* a table of all back references to this node, indexed by node name *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
46 |
* typ list (* a list of all finalized types *) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
47 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
48 |
and defnode = Defnode of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
49 |
typ (* type of the constant in this particular definition *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
50 |
* ((noderef * (string option * edgelabel list) list) Symtab.table) (* The edges, grouped by nodes. *) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
51 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
52 |
and backref = Backref of |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
53 |
noderef (* the name of the node that has defnodes which reference a certain node A *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
54 |
* (unit Symtab.table) (* the names of the defnodes that DIRECTLY reference A. *) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
55 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
56 |
fun getnode graph noderef = the (Symtab.lookup (graph, noderef)) |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
57 |
fun get_nodename (Node (n, _, _ ,_, _)) = n |
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
58 |
fun get_nodedefs (Node (_, _, defs, _, _)) = defs |
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
59 |
fun get_defnode (Node (_, _, defs, _, _)) defname = Symtab.lookup (defs, defname) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
60 |
fun get_defnode' graph noderef defname = Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname) |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
61 |
fun get_nodename (Node (n, _, _ , _, _)) = n |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
62 |
|
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
63 |
datatype graphaction = Declare of string * typ |
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
64 |
| Define of string * typ * string * (string * typ) list |
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
65 |
| Finalize of string * typ |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
66 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
67 |
type graph = (graphaction list) * (node Symtab.table) |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
68 |
|
16108
cf468b93a02e
Implement cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
70 |
|
cf468b93a02e
Implement cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
72 |
exception CIRCULAR of (typ * string * string) list; |
16113
692fe6595755
Infinite chains in definitions are now detected, too.
obua
parents:
16108
diff
changeset
|
73 |
exception INFINITE_CHAIN of (typ * string * string) list; |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
74 |
exception CLASH of string * string * string; |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
75 |
exception FINAL of string * typ; |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
76 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
77 |
fun def_err s = raise (DEFS s) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
78 |
|
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
79 |
fun declare (actions, g) (cty as (name, ty)) = |
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
80 |
((Declare cty)::actions, |
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
81 |
Symtab.update_new ((name, Node (name, Type.varifyT(Type.strip_sorts ty), Symtab.empty, Symtab.empty, [])), g)) |
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
82 |
handle Symtab.DUP _ => def_err "constant is already declared" |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
83 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
84 |
fun rename ty1 ty2 = incr_tvar ((maxidx_of_typ ty1)+1) ty2; |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
85 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
86 |
fun subst_incr_tvar inc t = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
87 |
if (inc > 0) then |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
88 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
89 |
val tv = typ_tvars t |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
90 |
val t' = incr_tvar inc t |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
91 |
fun update_subst (((n,i), _), s) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
92 |
Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
93 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
94 |
(t',List.foldl update_subst Vartab.empty tv) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
95 |
end |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
96 |
else |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
97 |
(t, Vartab.empty) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
98 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
99 |
(* Rename tys2 so that tys2 and tys1 do not have any variables in common any more. |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
100 |
As a result, return the renamed tys2' and the substitution that takes tys2 to tys2'. *) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
101 |
fun subst_rename max1 ty2 = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
102 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
103 |
val max2 = (maxidx_of_typ ty2) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
104 |
val (ty2', s) = subst_incr_tvar (max1 + 1) ty2 |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
105 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
106 |
(ty2', s, max1 + max2 + 1) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
107 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
108 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
109 |
fun subst s ty = Envir.norm_type s ty |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
110 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
111 |
fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
112 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
113 |
fun is_instance instance_ty general_ty = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
114 |
Type.typ_instance Type.empty_tsig (instance_ty, general_ty) |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
115 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
116 |
fun is_instance_r instance_ty general_ty = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
117 |
is_instance instance_ty (rename instance_ty general_ty) |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
118 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
119 |
fun unify ty1 ty2 = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
120 |
SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2))) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
121 |
handle Type.TUNIFY => NONE |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
122 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
123 |
(* |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
124 |
Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and so that they |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
125 |
are different. All indices in ty1 and ty2 are supposed to be less than or equal to max. |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
126 |
Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than all |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
127 |
indices in s1, s2, ty1, ty2. |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
128 |
*) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
129 |
fun unify_r max ty1 ty2 = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
130 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
131 |
val max = Int.max(max, 0) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
132 |
val max1 = max (* >= maxidx_of_typ ty1 *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
133 |
val max2 = max (* >= maxidx_of_typ ty2 *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
134 |
val max = Int.max(max, Int.max (max1, max2)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
135 |
val (ty1, s1) = subst_incr_tvar (max+1) ty1 |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
136 |
val (ty2, s2) = subst_incr_tvar (max+max1+2) ty2 |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
137 |
val max = max+max1+max2+2 |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
138 |
fun merge a b = Vartab.merge (fn _ => false) (a, b) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
139 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
140 |
case unify ty1 ty2 of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
141 |
NONE => NONE |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
142 |
| SOME s => SOME (max, merge s1 s, merge s2 s) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
143 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
144 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
145 |
fun can_be_unified_r ty1 ty2 = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
146 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
147 |
val ty2 = rename ty1 ty2 |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
148 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
149 |
case unify ty1 ty2 of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
150 |
NONE => false |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
151 |
| _ => true |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
152 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
153 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
154 |
fun can_be_unified ty1 ty2 = |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
155 |
case unify ty1 ty2 of |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
156 |
NONE => false |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
157 |
| _ => true |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
158 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
159 |
fun checkT (Type (a, Ts)) = Type (a, map checkT Ts) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
160 |
| checkT (TVar ((a, 0), _)) = TVar ((a, 0), []) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
161 |
| checkT (TVar ((a, i), _)) = def_err "type is not clean" |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
162 |
| checkT (TFree (a, _)) = TVar ((a, 0), []) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
163 |
|
cf468b93a02e
Implement cycle-free 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 cycle-free 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 cycle-free 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 cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
168 |
|
cf468b93a02e
Implement cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
170 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
171 |
val t1 = u1 --> v1 |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
172 |
val t2 = u2 --> v2 |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
173 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
174 |
if (is_instance_r t1 t2) then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
175 |
(if is_instance_r t2 t1 then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
176 |
SOME (int_ord (length history2, length history1)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
177 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
178 |
SOME LESS) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
179 |
else if (is_instance_r t2 t1) then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
180 |
SOME GREATER |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
181 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
182 |
NONE |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
183 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
184 |
|
16108
cf468b93a02e
Implement cycle-free 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 cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
187 |
(case compare_edges x y of |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
188 |
SOME LESS => (y::ys) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
189 |
| SOME EQUAL => (y::ys) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
190 |
| SOME GREATER => merge_edges_1 (x, ys) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
191 |
| NONE => y::(merge_edges_1 (x, ys))) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
192 |
|
16108
cf468b93a02e
Implement cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
194 |
|
cf468b93a02e
Implement cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
196 |
|
cf468b93a02e
Implement cycle-free 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 cycle-free 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 cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
200 |
(case label_ord l1 l2 of |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
201 |
LESS => (l1, e1)::(merge_labelled_edges es1 ((l2, e2)::es2)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
202 |
| GREATER => (l2, e2)::(merge_labelled_edges ((l1, e1)::es1) es2) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
203 |
| EQUAL => (l1, merge_edges e1 e2)::(merge_labelled_edges es1 es2)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
204 |
|
16108
cf468b93a02e
Implement cycle-free 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 cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
206 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
207 |
val (Defnode (ty, def_edges)) = defnode |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
208 |
fun g (b, (_, (n, labelled_edges))) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
209 |
foldl (fn ((s, edges), b') => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
210 |
(foldl (fn (e, b'') => f ty n s e b'') b' edges)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
211 |
b |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
212 |
labelled_edges |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
213 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
214 |
Symtab.foldl g (a, def_edges) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
215 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
216 |
|
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
217 |
fun define (actions, graph) (name, ty) axname body = |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
218 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
219 |
val ty = checkT ty |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
220 |
val body = map (fn (n,t) => (n, checkT t)) body |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
221 |
val mainref = name |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
222 |
val mainnode = (case Symtab.lookup (graph, mainref) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
223 |
NONE => def_err ("constant "^mainref^" is not declared") |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
224 |
| SOME n => n) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
225 |
val (Node (n, gty, defs, backs, finals)) = mainnode |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
226 |
val _ = (if is_instance_r ty gty then () else def_err "type of constant does not match declared type") |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
227 |
fun check_def (s, Defnode (ty', _)) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
228 |
(if can_be_unified_r ty ty' then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
229 |
raise (CLASH (mainref, axname, s)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
230 |
else if s = axname then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
231 |
def_err "name of axiom is already used for another definition of this constant" |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
232 |
else false) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
233 |
val _ = Symtab.exists check_def defs |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
234 |
fun check_final finalty = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
235 |
(if can_be_unified_r finalty ty then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
236 |
raise (FINAL (mainref, finalty)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
237 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
238 |
true) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
239 |
val _ = forall check_final finals |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
240 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
241 |
(* now we know that the only thing that can prevent acceptance of the definition is a cyclic dependency *) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
242 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
243 |
(* body contains the constants that this constant definition depends on. For each element of body, |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
244 |
the function make_edges_to calculates a group of edges that connect this constant with |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
245 |
the constant that is denoted by the element of the body *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
246 |
fun make_edges_to (bodyn, bodyty) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
247 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
248 |
val bnode = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
249 |
(case Symtab.lookup (graph, bodyn) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
250 |
NONE => def_err "body of constant definition references undeclared constant" |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
251 |
| SOME x => x) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
252 |
val (Node (_, general_btyp, bdefs, bbacks, bfinals)) = bnode |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
253 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
254 |
case unify_r 0 bodyty general_btyp of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
255 |
NONE => NONE |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
256 |
| SOME (maxidx, sigma1, sigma2) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
257 |
SOME ( |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
258 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
259 |
(* For each definition of the constant in the body, |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
260 |
check if the definition unifies with the type of the constant in the body. *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
261 |
fun make_edges ((swallowed, l),(def_name, Defnode (def_ty, _))) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
262 |
if swallowed then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
263 |
(swallowed, l) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
264 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
265 |
(case unify_r 0 bodyty def_ty of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
266 |
NONE => (swallowed, l) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
267 |
| SOME (maxidx, sigma1, sigma2) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
268 |
(is_instance_r bodyty def_ty, |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
269 |
merge_labelled_edges l [(SOME def_name,[(maxidx, subst sigma1 ty, subst sigma2 def_ty, [])])])) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
270 |
val swallowed = exists (is_instance_r bodyty) bfinals |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
271 |
val (swallowed, edges) = Symtab.foldl make_edges ((swallowed, []), bdefs) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
272 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
273 |
if swallowed then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
274 |
(bodyn, edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
275 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
276 |
(bodyn, [(NONE, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])])]@edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
277 |
end) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
278 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
279 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
280 |
fun update_edges (b as (bodyn, bodyty), edges) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
281 |
(case make_edges_to b of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
282 |
NONE => edges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
283 |
| SOME m => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
284 |
(case Symtab.lookup (edges, bodyn) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
285 |
NONE => Symtab.update ((bodyn, m), edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
286 |
| SOME (_, es') => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
287 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
288 |
val (_, es) = m |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
289 |
val es = merge_labelled_edges es es' |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
290 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
291 |
Symtab.update ((bodyn, (bodyn, es)), edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
292 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
293 |
) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
294 |
) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
295 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
296 |
val edges = foldl update_edges Symtab.empty body |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
297 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
298 |
fun insert_edge edges (nodename, (defname_opt, edge)) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
299 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
300 |
val newlink = [(defname_opt, [edge])] |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
301 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
302 |
case Symtab.lookup (edges, nodename) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
303 |
NONE => Symtab.update ((nodename, (nodename, newlink)), edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
304 |
| SOME (_, links) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
305 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
306 |
val links' = merge_labelled_edges links newlink |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
307 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
308 |
Symtab.update ((nodename, (nodename, links')), edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
309 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
310 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
311 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
312 |
(* We constructed all direct edges that this defnode has. |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
313 |
Now we have to construct the transitive hull by going a single step further. *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
314 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
315 |
val thisDefnode = Defnode (ty, edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
316 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
317 |
fun make_trans_edges _ noderef defname_opt (max1, alpha1, beta1, history1) edges = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
318 |
case defname_opt of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
319 |
NONE => edges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
320 |
| SOME defname => |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
321 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
322 |
val defnode = the (get_defnode' graph noderef defname) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
323 |
fun make_trans_edge _ noderef2 defname_opt2 (max2, alpha2, beta2, history2) edges = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
324 |
case unify_r (Int.max (max1, max2)) beta1 alpha2 of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
325 |
NONE => edges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
326 |
| SOME (max, sleft, sright) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
327 |
insert_edge edges (noderef2, |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
328 |
(defname_opt2, |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
329 |
(max, subst sleft alpha1, subst sright beta2, |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
330 |
(subst_history sleft history1)@ |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
331 |
((subst sleft beta1, noderef, defname):: |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
332 |
(subst_history sright history2))))) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
333 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
334 |
defnode_edges_foldl make_trans_edge edges defnode |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
335 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
336 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
337 |
val edges = defnode_edges_foldl make_trans_edges edges thisDefnode |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
338 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
339 |
val thisDefnode = Defnode (ty, edges) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
340 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
341 |
(* We also have to add the backreferences that this new defnode induces. *) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
342 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
343 |
fun hasNONElink ((NONE, _)::_) = true |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
344 |
| hasNONElink _ = false |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
345 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
346 |
fun install_backref graph noderef pointingnoderef pointingdefname = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
347 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
348 |
val (Node (pname, _, _, _, _)) = getnode graph pointingnoderef |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
349 |
val (Node (name, ty, defs, backs, finals)) = getnode graph noderef |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
350 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
351 |
case Symtab.lookup (backs, pname) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
352 |
NONE => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
353 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
354 |
val defnames = Symtab.update ((pointingdefname, ()), Symtab.empty) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
355 |
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
356 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
357 |
Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
358 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
359 |
| SOME (Backref (pointingnoderef, defnames)) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
360 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
361 |
val defnames = Symtab.update_new ((pointingdefname, ()), defnames) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
362 |
val backs = Symtab.update ((pname, Backref (pointingnoderef, defnames)), backs) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
363 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
364 |
Symtab.update ((name, Node (name, ty, defs, backs, finals)), graph) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
365 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
366 |
handle Symtab.DUP _ => graph |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
367 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
368 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
369 |
fun install_backrefs (graph, (_, (noderef, labelled_edges))) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
370 |
if hasNONElink labelled_edges then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
371 |
install_backref graph noderef mainref axname |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
372 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
373 |
graph |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
374 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
375 |
val graph = Symtab.foldl install_backrefs (graph, edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
376 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
377 |
val (Node (_, _, _, backs, _)) = getnode graph mainref |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
378 |
val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update_new |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
379 |
((axname, thisDefnode), defs), backs, finals)), graph) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
380 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
381 |
(* Now we have to check all backreferences to this node and inform them about the new defnode. |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
382 |
In this section we also check for circularity. *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
383 |
fun update_backrefs ((backs, newedges), (nodename, Backref (noderef, defnames))) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
384 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
385 |
val node = getnode graph noderef |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
386 |
fun update_defs ((defnames, newedges),(defname, _)) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
387 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
388 |
val (Defnode (_, defnode_edges)) = the (get_defnode node defname) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
389 |
val (_, labelled_edges) = the (Symtab.lookup (defnode_edges, n)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
390 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
391 |
(* the type of thisDefnode is ty *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
392 |
fun update (e as (max, alpha, beta, history), (none_edges, this_edges)) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
393 |
case unify_r max beta ty of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
394 |
NONE => (e::none_edges, this_edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
395 |
| SOME (max', s_beta, s_ty) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
396 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
397 |
val alpha' = subst s_beta alpha |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
398 |
val ty' = subst s_ty ty |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
399 |
val _ = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
400 |
if noderef = mainref andalso defname = axname then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
401 |
(case unify alpha' ty' of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
402 |
NONE => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
403 |
if (is_instance_r ty' alpha') then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
404 |
raise (INFINITE_CHAIN ( |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
405 |
(alpha', mainref, axname):: |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
406 |
(subst_history s_beta history)@ |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
407 |
[(ty', mainref, axname)])) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
408 |
else () |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
409 |
| SOME s => raise (CIRCULAR ( |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
410 |
(subst s alpha', mainref, axname):: |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
411 |
(subst_history s (subst_history s_beta history))@ |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
412 |
[(subst s ty', mainref, axname)]))) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
413 |
else () |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
414 |
val edge = (max', alpha', ty', subst_history s_beta history) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
415 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
416 |
if is_instance_r beta ty then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
417 |
(none_edges, edge::this_edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
418 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
419 |
(e::none_edges, edge::this_edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
420 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
421 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
422 |
case labelled_edges of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
423 |
((NONE, edges)::_) => |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
424 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
425 |
val (none_edges, this_edges) = foldl update ([], []) edges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
426 |
val defnames = if none_edges = [] then defnames else Symtab.update_new ((defname, ()), defnames) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
427 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
428 |
(defnames, (defname, none_edges, this_edges)::newedges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
429 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
430 |
| _ => sys_error "define: update_defs, internal error, corrupt backrefs" |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
431 |
end |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
432 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
433 |
val (defnames, newedges') = Symtab.foldl update_defs ((Symtab.empty, []), defnames) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
434 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
435 |
if Symtab.is_empty defnames then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
436 |
(backs, (noderef, newedges')::newedges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
437 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
438 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
439 |
val backs = Symtab.update_new ((nodename, Backref (noderef, defnames)), backs) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
440 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
441 |
(backs, newedges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
442 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
443 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
444 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
445 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
446 |
val (backs, newedges) = Symtab.foldl update_backrefs ((Symtab.empty, []), backs) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
447 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
448 |
(* If a Circular exception is thrown then we never reach this point. *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
449 |
(* Ok, the definition is consistent, let's update this node. *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
450 |
val graph = Symtab.update ((mainref, Node (n, gty, Symtab.update |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
451 |
((axname, thisDefnode), defs), backs, finals)), graph) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
452 |
|
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
453 |
(* Furthermore, update all the other nodes that backreference this node. *) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
454 |
fun final_update_backrefs graph noderef defname none_edges this_edges = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
455 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
456 |
val node = getnode graph noderef |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
457 |
val (Node (nodename, nodety, defs, backs, finals)) = node |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
458 |
val (Defnode (defnode_ty, defnode_edges)) = the (get_defnode node defname) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
459 |
val (_, defnode_links) = the (Symtab.lookup (defnode_edges, n)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
460 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
461 |
fun update edges none_edges this_edges = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
462 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
463 |
val u = merge_labelled_edges edges [(SOME axname, pack_edges this_edges)] |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
464 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
465 |
if none_edges = [] then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
466 |
u |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
467 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
468 |
(NONE, pack_edges none_edges)::u |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
469 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
470 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
471 |
val defnode_links' = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
472 |
case defnode_links of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
473 |
((NONE, _) :: edges) => update edges none_edges this_edges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
474 |
| edges => update edges none_edges this_edges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
475 |
val defnode_edges' = Symtab.update ((n, (mainref, defnode_links')), defnode_edges) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
476 |
val defs' = Symtab.update ((defname, Defnode (defnode_ty, defnode_edges')), defs) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
477 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
478 |
Symtab.update ((nodename, Node (nodename, nodety, defs', backs, finals)), graph) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
479 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
480 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
481 |
val graph = foldl (fn ((noderef, newedges),graph) => foldl (fn ((defname, none_edges, this_edges), graph) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
482 |
final_update_backrefs graph noderef defname none_edges this_edges) graph newedges) graph newedges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
483 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
484 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
485 |
((Define (name, ty, axname, body))::actions, graph) |
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
486 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
487 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
488 |
fun finalize (history, graph) (c, ty) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
489 |
case Symtab.lookup (graph, c) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
490 |
NONE => def_err ("cannot finalize constant "^c^"; it is not declared") |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
491 |
| SOME (Node (noderef, nodety, defs, backs, finals)) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
492 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
493 |
val ty = checkT ty |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
494 |
val _ = if (not (is_instance_r ty nodety)) then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
495 |
def_err ("only type instances of the declared constant "^c^" can be finalized") |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
496 |
else () |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
497 |
val _ = Symtab.exists (fn (def_name, Defnode (def_ty, _)) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
498 |
if can_be_unified_r ty def_ty then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
499 |
def_err ("cannot finalize constant "^c^"; clash with definition "^def_name) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
500 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
501 |
false) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
502 |
defs |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
503 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
504 |
fun update_finals [] = SOME [ty] |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
505 |
| update_finals (final_ty::finals) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
506 |
(if is_instance_r ty final_ty then NONE |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
507 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
508 |
case update_finals finals of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
509 |
NONE => NONE |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
510 |
| (r as SOME finals) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
511 |
if (is_instance_r final_ty ty) then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
512 |
r |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
513 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
514 |
SOME (final_ty :: finals)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
515 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
516 |
case update_finals finals of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
517 |
NONE => (history, graph) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
518 |
| SOME finals => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
519 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
520 |
val graph = Symtab.update ((noderef, Node(noderef, nodety, defs, backs, finals)), graph) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
521 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
522 |
fun update_backref ((graph, backs), (backrefname, Backref (_, backdefnames))) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
523 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
524 |
fun update_backdef ((graph, defnames), (backdefname, _)) = |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
525 |
let |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
526 |
val (backnode as Node (_, backty, backdefs, backbacks, backfinals)) = getnode graph backrefname |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
527 |
val (Defnode (def_ty, all_edges)) = the (get_defnode backnode backdefname) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
528 |
val (defnames', all_edges') = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
529 |
case Symtab.lookup (all_edges, noderef) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
530 |
NONE => sys_error "finalize: corrupt backref" |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
531 |
| SOME (_, (NONE, edges)::rest) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
532 |
let |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
533 |
val edges' = List.filter (fn (_, _, beta, _) => not (is_instance_r beta ty)) edges |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
534 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
535 |
if edges' = [] then |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
536 |
(defnames, Symtab.update ((noderef, (noderef, rest)), all_edges)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
537 |
else |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
538 |
(Symtab.update ((backdefname, ()), defnames), |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
539 |
Symtab.update ((noderef, (noderef, (NONE, edges')::rest)), all_edges)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
540 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
541 |
val defnode' = Defnode (def_ty, all_edges') |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
542 |
val backnode' = Node (backrefname, backty, Symtab.update ((backdefname, defnode'), backdefs), |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
543 |
backbacks, backfinals) |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
544 |
in |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
545 |
(Symtab.update ((backrefname, backnode'), graph), defnames') |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
546 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
547 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
548 |
val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
549 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
550 |
(graph', if Symtab.is_empty defnames' then backs |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
551 |
else Symtab.update ((backrefname, Backref (backrefname, defnames')), backs)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
552 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
553 |
val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
554 |
val Node (_, _, defs, _, _) = getnode graph' noderef |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
555 |
in |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
556 |
((Finalize (c, ty)) :: history, Symtab.update ((noderef, Node (noderef, nodety, defs, backs', finals)), graph')) |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
557 |
end |
16198
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
558 |
end |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
559 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
560 |
fun merge' (Declare cty, g) = (declare g cty handle _ => g) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
561 |
| merge' (Define (name, ty, axname, body), g as (_, graph)) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
562 |
(case Symtab.lookup (graph, name) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
563 |
NONE => define g (name, ty) axname body |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
564 |
| SOME (Node (_, _, defs, _, _)) => |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
565 |
(case Symtab.lookup (defs, axname) of |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
566 |
NONE => define g (name, ty) axname body |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
567 |
| SOME _ => g)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
568 |
| merge' (Finalize finals, g) = finalize g finals |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
569 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
570 |
fun merge (actions, _) g = foldr merge' g actions |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
571 |
|
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
572 |
fun finals (history, graph) = |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
573 |
Symtab.foldl |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
574 |
(fn (finals, (_, Node(name, _, _, _, ftys))) => Symtab.update_new ((name, ftys), finals)) |
cfd070a2cc4d
Integrates cycle detection in definitions with finalconsts
obua
parents:
16177
diff
changeset
|
575 |
(Symtab.empty, graph) |
16158
2c3565b74b7a
Removed final_consts from theory data. Now const_deps deals with final
obua
parents:
16113
diff
changeset
|
576 |
|
16108
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
577 |
end; |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
578 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
579 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
580 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
581 |
(*fun tvar name = TVar ((name, 0), []) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
582 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
583 |
val bool = Type ("bool", []) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
584 |
val int = Type ("int", []) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
585 |
val alpha = tvar "'a" |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
586 |
val beta = tvar "'b" |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
587 |
val gamma = tvar "'c" |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
588 |
fun pair a b = Type ("pair", [a,b]) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
589 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
590 |
val _ = print "make empty" |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
591 |
val g = Defs.empty |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
592 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
593 |
val _ = print "declare" |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
594 |
val g = Defs.declare g "M" (alpha --> bool) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
595 |
val g = Defs.declare g "N" (beta --> bool) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
596 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
597 |
val _ = print "define" |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
598 |
val g = Defs.define g "N" (alpha --> bool) "defN" [("M", alpha --> bool)] |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
599 |
val g = Defs.define g "M" (alpha --> bool) "defM" [("N", int --> alpha)] |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
600 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
601 |
val g = Defs.declare g "0" alpha |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
602 |
val g = Defs.define g "0" (pair alpha beta) "zp" [("0", alpha), ("0", beta)]*) |
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
603 |
|
cf468b93a02e
Implement cycle-free overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset
|
604 |