author | wenzelm |
Fri, 12 May 2006 01:01:08 +0200 | |
changeset 19620 | ccd6de95f4a6 |
parent 19613 | 9bf274ec94cf |
child 19624 | 3b6629701a79 |
permissions | -rw-r--r-- |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
1 |
(* Title: Pure/defs.ML |
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
|
2 |
ID: $Id$ |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
3 |
Author: Makarius |
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
|
4 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
5 |
Global well-formedness checks for constant definitions. Covers |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
6 |
dependencies of simple sub-structural overloading, where type |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
7 |
arguments are approximated by the outermost type constructor. |
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
|
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 |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
10 |
signature DEFS = |
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
11 |
sig |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
12 |
type T |
19569 | 13 |
val specifications_of: T -> string -> |
14 |
(serial * {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}) list |
|
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
15 |
val empty: T |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
16 |
val merge: T * T -> T |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
17 |
val define: (string * typ -> typ list) -> |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
18 |
bool -> string -> string -> string * typ -> (string * typ) list -> T -> T |
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
|
19 |
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
|
20 |
|
17711 | 21 |
structure Defs: DEFS = |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
22 |
struct |
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
|
23 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
24 |
(* dependency items *) |
19569 | 25 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
26 |
(* |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
27 |
Constant c covers all instances of c |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
28 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
29 |
Instance (c, a) covers all instances of applications (c, [Type (a, _)]) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
30 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
31 |
Different Constant/Constant or Instance/Instance items represent |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
32 |
disjoint sets of instances. The set Constant c subsumes any |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
33 |
Instance (c, a) -- dependencies are propagated accordingly. |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
34 |
*) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
35 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
36 |
datatype item = |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
37 |
Constant of string | |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
38 |
Instance of string * string; |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
39 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
40 |
fun make_item (c, [Type (a, _)]) = Instance (c, a) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
41 |
| make_item (c, _) = Constant c; |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
42 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
43 |
fun pretty_item (Constant c) = Pretty.str (quote c) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
44 |
| pretty_item (Instance (c, a)) = Pretty.str (quote c ^ " (type " ^ quote a ^ ")"); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
45 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
46 |
fun item_ord (Constant c, Constant c') = fast_string_ord (c, c') |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
47 |
| item_ord (Instance ca, Instance ca') = prod_ord fast_string_ord fast_string_ord (ca, ca') |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
48 |
| item_ord (Constant _, Instance _) = LESS |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
49 |
| item_ord (Instance _, Constant _) = GREATER; |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
50 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
51 |
structure Items = GraphFun(type key = item val ord = item_ord); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
52 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
53 |
fun declare_edge (i, j) = |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
54 |
Items.default_node (i, ()) #> |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
55 |
Items.default_node (j, ()) #> |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
56 |
Items.add_edge_acyclic (i, j); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
57 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
58 |
fun propagate_deps insts deps = |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
59 |
let |
19620 | 60 |
fun inst_item (Constant c) = Symtab.lookup_list insts c |
61 |
| inst_item (Instance _) = []; |
|
62 |
fun inst_edge i j = |
|
63 |
fold declare_edge (tl (product (i :: inst_item i) (j :: inst_item j))); |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
64 |
in Items.fold (fn (i, (_, (_, js))) => fold (inst_edge i) js) deps deps end; |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
65 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
66 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
67 |
(* specifications *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
68 |
|
19569 | 69 |
type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}; |
70 |
||
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
71 |
datatype T = Defs of |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
72 |
{specs: (bool * spec Inttab.table) Symtab.table, |
19620 | 73 |
insts: item list Symtab.table, |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
74 |
deps: unit Items.T}; |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
75 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
76 |
fun no_overloading_of (Defs {specs, ...}) c = |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
77 |
(case Symtab.lookup specs c of |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
78 |
SOME (b, _) => b |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
79 |
| NONE => false); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
80 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
81 |
fun specifications_of (Defs {specs, ...}) c = |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
82 |
(case Symtab.lookup specs c of |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
83 |
SOME (_, sps) => Inttab.dest sps |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
84 |
| NONE => []); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
85 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
86 |
fun make_defs (specs, insts, deps) = Defs {specs = specs, insts = insts, deps = deps}; |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
87 |
fun map_defs f (Defs {specs, insts, deps}) = make_defs (f (specs, insts, deps)); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
88 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
89 |
val empty = make_defs (Symtab.empty, Symtab.empty, Items.empty); |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
90 |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
91 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
92 |
(* merge *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
93 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
94 |
fun disjoint_types T U = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
95 |
(Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
96 |
handle Type.TUNIFY => true; |
16308 | 97 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
98 |
fun disjoint_specs c (i, {lhs = T, name = a, ...}: spec) = |
19569 | 99 |
Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) => |
100 |
i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse |
|
101 |
error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ |
|
102 |
" for constant " ^ quote c)); |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
103 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
104 |
fun cycle_msg css = |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
105 |
let |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
106 |
fun prt_cycle items = Pretty.block (flat |
19620 | 107 |
(separate [Pretty.str " ->", Pretty.brk 1] (map (single o pretty_item) items))); |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
108 |
in Pretty.string_of (Pretty.big_list "Cyclic dependency of constants:" (map prt_cycle css)) end; |
16982 | 109 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
110 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
111 |
fun merge |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
112 |
(Defs {specs = specs1, insts = insts1, deps = deps1}, |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
113 |
Defs {specs = specs2, insts = insts2, deps = deps2}) = |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
114 |
let |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
115 |
val specs' = (specs1, specs2) |> Symtab.join (fn c => fn ((b, sps1), (_, sps2)) => |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
116 |
(b, Inttab.fold (fn sp2 => (disjoint_specs c sp2 sps1; Inttab.update sp2)) sps2 sps1)); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
117 |
val insts' = Symtab.merge_list (op =) (insts1, insts2); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
118 |
val items' = propagate_deps insts' (Items.merge_acyclic (K true) (deps1, deps2)) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
119 |
handle Items.CYCLES cycles => error (cycle_msg cycles); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
120 |
in make_defs (specs', insts', items') end; |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
121 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
122 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
123 |
(* define *) |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
124 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
125 |
fun define const_typargs is_def module name lhs rhs defs = defs |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
126 |
|> map_defs (fn (specs, insts, deps) => |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
127 |
let |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
128 |
val (c, T) = lhs; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
129 |
val args = const_typargs lhs; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
130 |
val no_overloading = forall Term.is_TVar args andalso not (has_duplicates (op =) args); |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
131 |
|
19569 | 132 |
val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs}); |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
133 |
val specs' = specs |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
134 |
|> Symtab.default (c, (false, Inttab.empty)) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
135 |
|> Symtab.map_entry c (fn (_, sps) => |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
136 |
(disjoint_specs c spec sps; (no_overloading, Inttab.update spec sps))); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
137 |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
138 |
val lhs' = make_item (c, if no_overloading then [] else args); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
139 |
val rhs' = rhs |> map_filter (fn (c', T') => |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
140 |
let val args' = const_typargs (c', T') in |
19620 | 141 |
if forall Term.is_TVar args' then NONE |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
142 |
else SOME (make_item (c', if no_overloading_of defs c' then [] else args')) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
143 |
end); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
144 |
|
19620 | 145 |
val insts' = insts |> fold (fn i as Instance (c, _) => |
146 |
Symtab.insert_list (op =) (c, i) | _ => I) (lhs' :: rhs'); |
|
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
147 |
val deps' = deps |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
148 |
|> fold (fn r => declare_edge (r, lhs')) rhs' |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
149 |
|> propagate_deps insts' |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
150 |
handle Items.CYCLES cycles => |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
151 |
if no_overloading then error (cycle_msg cycles) |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
152 |
else (warning (cycle_msg cycles ^ "\nUnchecked overloaded specification: " ^ name); deps); |
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
153 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
154 |
in (specs', insts', deps') end); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
155 |
|
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
|
156 |
end; |