author | wenzelm |
Mon, 08 May 2006 17:40:06 +0200 | |
changeset 19590 | 12af4942923d |
parent 19569 | 1c23356a8ea8 |
child 19613 | 9bf274ec94cf |
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 |
|
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
5 |
Global well-formedness checks for constant definitions -- covers |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
6 |
dependencies of simple sub-structural overloading. |
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
|
7 |
*) |
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 |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
9 |
signature DEFS = |
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
10 |
sig |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
11 |
type T |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
12 |
val define: (string * typ -> typ list) -> |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
13 |
bool -> string -> string -> string * typ -> (string * typ) list -> T -> T |
19569 | 14 |
val specifications_of: T -> string -> |
15 |
(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
|
16 |
val empty: T |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
17 |
val merge: Pretty.pp -> T * 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
|
18 |
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
|
19 |
|
17711 | 20 |
structure Defs: DEFS = |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
21 |
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
|
22 |
|
19569 | 23 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
24 |
(** datatype T **) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
25 |
|
19569 | 26 |
type spec = {is_def: bool, module: string, name: string, lhs: typ, rhs: (string * typ) list}; |
27 |
||
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
28 |
datatype T = Defs of |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
29 |
{consts: unit Graph.T, |
19569 | 30 |
specified: spec Inttab.table Symtab.table}; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
31 |
|
17994 | 32 |
fun make_defs (consts, specified) = Defs {consts = consts, specified = specified}; |
33 |
fun map_defs f (Defs {consts, specified}) = make_defs (f (consts, specified)); |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
34 |
|
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
35 |
fun cyclic cycles = |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
36 |
"Cyclic dependency of constants:\n" ^ |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
37 |
cat_lines (map (space_implode " -> " o map quote o rev) cycles); |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
38 |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
39 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
40 |
(* specified consts *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
41 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
42 |
fun disjoint_types T U = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
43 |
(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
|
44 |
handle Type.TUNIFY => true; |
16308 | 45 |
|
19569 | 46 |
fun check_specified c (i, {lhs = T, name = a, ...}: spec) = |
47 |
Inttab.forall (fn (j, {lhs = U, name = b, ...}: spec) => |
|
48 |
i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse |
|
49 |
error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ |
|
50 |
" for constant " ^ quote c)); |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
51 |
|
16982 | 52 |
|
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
53 |
(* substructural type arguments *) |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
54 |
|
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
55 |
fun struct_less T (Type (_, Us)) = exists (struct_le T) Us |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
56 |
| struct_less _ _ = false |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
57 |
and struct_le T U = T = U orelse struct_less T U; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
58 |
|
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
59 |
fun structs_le Ts Us = forall (fn U => exists (fn T => struct_le T U) Ts) Us; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
60 |
fun structs_less Ts Us = Ts <> Us andalso structs_le Ts Us; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
61 |
|
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
62 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
63 |
(* define consts *) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
64 |
|
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
65 |
fun define const_typargs is_def module name lhs rhs = map_defs (fn (consts, specified) => |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
66 |
let |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
67 |
val (c, T) = lhs; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
68 |
val args = const_typargs lhs; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
69 |
val deps = rhs |> map_filter (fn d => |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
70 |
if structs_less (const_typargs d) args then NONE else SOME (#1 d)); |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
71 |
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
|
72 |
|
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
73 |
val consts' = fold (fn (a, _) => Graph.default_node (a, ())) (lhs :: rhs) consts; |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
74 |
val consts'' = Graph.add_deps_acyclic (c, deps) consts' handle Graph.CYCLES cycles => |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
75 |
if no_overloading then error (cyclic cycles) |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
76 |
else (warning (cyclic cycles ^ "\nUnchecked overloaded specification: " ^ name); consts'); |
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
77 |
|
19569 | 78 |
val spec = (serial (), {is_def = is_def, module = module, name = name, lhs = T, rhs = rhs}); |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
79 |
val specified' = specified |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
80 |
|> Symtab.default (c, Inttab.empty) |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
81 |
|> Symtab.map_entry c (fn specs => (check_specified c spec specs; Inttab.update spec specs)); |
17994 | 82 |
in (consts', specified') end); |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
83 |
|
19050 | 84 |
fun specifications_of (Defs {specified, ...}) c = |
19569 | 85 |
Inttab.dest (the_default Inttab.empty (Symtab.lookup specified c)); |
19050 | 86 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
87 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
88 |
(* empty and merge *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
89 |
|
17994 | 90 |
val empty = make_defs (Graph.empty, Symtab.empty); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
91 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
92 |
fun merge pp |
17994 | 93 |
(Defs {consts = consts1, specified = specified1}, |
94 |
Defs {consts = consts2, specified = specified2}) = |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
95 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
96 |
val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true) |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
97 |
handle Graph.CYCLES cycles => error (cyclic cycles); |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
98 |
val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) => |
19025 | 99 |
Inttab.fold (fn spec2 => fn specs1 => |
100 |
(check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1); |
|
17994 | 101 |
in make_defs (consts', specified') end; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
102 |
|
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
|
103 |
end; |