author | wenzelm |
Thu, 27 Apr 2006 15:06:35 +0200 | |
changeset 19482 | 9f11af8f7ef9 |
parent 19339 | 59f08f67ed3f |
child 19569 | 1c23356a8ea8 |
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 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
5 |
Global well-formedness checks for constant definitions. Dependencies |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
6 |
are only tracked for non-overloaded definitions! |
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 |
19135 | 12 |
val define: (string -> typ) -> (bool * string) * string |
13 |
-> string * typ -> (string * typ) list -> T -> T |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
14 |
val empty: T |
19339 | 15 |
val specifications_of: T -> string -> (typ * (string * string)) list |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
16 |
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
|
17 |
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
|
18 |
|
17711 | 19 |
structure Defs: DEFS = |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
20 |
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
|
21 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
22 |
(** datatype T **) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
23 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
24 |
datatype T = Defs of |
19135 | 25 |
{consts: typ Graph.T, |
26 |
(*constant declarations and dependencies*) |
|
27 |
specified: (bool * string * string * typ) Inttab.table Symtab.table}; |
|
28 |
(*is proper definition?, theory name, specification name and const type*) |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
29 |
|
17994 | 30 |
fun make_defs (consts, specified) = Defs {consts = consts, specified = specified}; |
31 |
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
|
32 |
|
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
33 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
34 |
(* specified consts *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
35 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
36 |
fun disjoint_types T U = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
37 |
(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
|
38 |
handle Type.TUNIFY => true; |
16308 | 39 |
|
19135 | 40 |
fun check_specified c (i, (_, a, _, T)) = Inttab.forall (fn (j, (_, b, _, U)) => |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
41 |
i = j orelse not (Type.could_unify (T, U)) orelse disjoint_types T U orelse |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
42 |
error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
43 |
" for constant " ^ quote c)); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
44 |
|
16982 | 45 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
46 |
(* define consts *) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
47 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
48 |
fun err_cyclic cycles = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
49 |
error ("Cyclic dependency of constants:\n" ^ |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
50 |
cat_lines (map (space_implode " -> " o map quote o rev) cycles)); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
51 |
|
19135 | 52 |
fun define const_type ((is_def, thyname), 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
|
53 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
54 |
fun declare (a, _) = Graph.default_node (a, const_type a); |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
55 |
fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
56 |
handle Graph.CYCLES cycles => err_cyclic cycles; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
57 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
58 |
val (c, T) = lhs; |
19135 | 59 |
val spec = (serial (), (is_def, name, thyname, T)); |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
60 |
val no_overloading = Type.raw_instance (const_type c, T); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
61 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
62 |
val consts' = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
63 |
consts |> declare lhs |> fold declare rhs |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
64 |
|> K no_overloading ? add_deps (c, map #1 rhs); |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
65 |
val specified' = specified |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
66 |
|> Symtab.default (c, Inttab.empty) |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
67 |
|> Symtab.map_entry c (fn specs => |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
68 |
(check_specified c spec specs; Inttab.update spec specs)); |
17994 | 69 |
in (consts', specified') end); |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
70 |
|
19050 | 71 |
fun specifications_of (Defs {specified, ...}) c = |
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19339
diff
changeset
|
72 |
(map_filter |
19135 | 73 |
(fn (_, (false, _, _, _)) => NONE |
19339 | 74 |
| (_, (true, specname, thyname, ty)) => SOME (ty, (specname, thyname))) o Inttab.dest |
19135 | 75 |
o the_default Inttab.empty o Symtab.lookup specified) c; |
19050 | 76 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
77 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
78 |
(* empty and merge *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
79 |
|
17994 | 80 |
val empty = make_defs (Graph.empty, Symtab.empty); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
81 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
82 |
fun merge pp |
17994 | 83 |
(Defs {consts = consts1, specified = specified1}, |
84 |
Defs {consts = consts2, specified = specified2}) = |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
85 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
86 |
val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
87 |
handle Graph.CYCLES cycles => err_cyclic cycles; |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
88 |
val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) => |
19025 | 89 |
Inttab.fold (fn spec2 => fn specs1 => |
90 |
(check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1); |
|
17994 | 91 |
in make_defs (consts', specified') end; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
92 |
|
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
|
93 |
end; |