author | wenzelm |
Fri, 07 Oct 2005 23:29:00 +0200 | |
changeset 17789 | ccba4e900023 |
parent 17712 | 46c2091e5187 |
child 17803 | e235a57651a1 |
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 |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
12 |
val monomorphic: T -> string -> bool |
17712 | 13 |
val define: (string -> typ) -> string -> 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 |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
15 |
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
|
16 |
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
|
17 |
|
17711 | 18 |
structure Defs: DEFS = |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
19 |
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
|
20 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
21 |
(** datatype T **) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
22 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
23 |
datatype T = Defs of |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
24 |
{consts: typ Graph.T, (*constant declarations and dependencies*) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
25 |
specified: (string * typ) Inttab.table Symtab.table, (*specification name and const type*) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
26 |
monomorphic: unit Symtab.table}; (*constants having monomorphic specs*) |
16384
90c51c932154
internalize axiom names in Defs.define; compress types via Term.compress_type
obua
parents:
16361
diff
changeset
|
27 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
28 |
fun rep_defs (Defs args) = args; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
29 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
30 |
fun make_defs (consts, specified, monomorphic) = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
31 |
Defs {consts = consts, specified = specified, monomorphic = monomorphic}; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
32 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
33 |
fun map_defs f (Defs {consts, specified, monomorphic}) = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
34 |
make_defs (f (consts, specified, monomorphic)); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
35 |
|
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
36 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
37 |
(* specified consts *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
38 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
39 |
fun disjoint_types T U = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
40 |
(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
|
41 |
handle Type.TUNIFY => true; |
16308 | 42 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
43 |
fun check_specified c specified = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
44 |
specified |> Inttab.forall (fn (i, (a, T)) => |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
45 |
specified |> Inttab.forall (fn (j, (b, U)) => |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
46 |
i = j orelse disjoint_types T U orelse |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
47 |
error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
48 |
" for constant " ^ quote c))); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
49 |
|
16982 | 50 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
51 |
(* monomorphic constants *) |
16982 | 52 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
53 |
val monomorphic = Symtab.defined o #monomorphic o rep_defs; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
54 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
55 |
fun update_monomorphic specified c = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
56 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
57 |
val specs = the_default Inttab.empty (Symtab.lookup specified c); |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
58 |
fun is_monoT (Type (_, Ts)) = forall is_monoT Ts |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
59 |
| is_monoT _ = false; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
60 |
val is_mono = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
61 |
Inttab.is_empty specs orelse |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
62 |
Inttab.min_key specs = Inttab.max_key specs andalso |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
63 |
is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs))))); |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
64 |
in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
65 |
|
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
66 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
67 |
(* define consts *) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
68 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
69 |
fun err_cyclic cycles = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
70 |
error ("Cyclic dependency of constants:\n" ^ |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
71 |
cat_lines (map (space_implode " -> " o map quote o rev) cycles)); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
72 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
73 |
fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) => |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
74 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
75 |
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
|
76 |
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
|
77 |
handle Graph.CYCLES cycles => err_cyclic cycles; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
78 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
79 |
val (c, T) = lhs; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
80 |
val no_overloading = Type.raw_instance (const_type c, T); |
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 |
val consts' = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
83 |
consts |> declare lhs |> fold declare rhs |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
84 |
|> K no_overloading ? add_deps (c, map #1 rhs); |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
85 |
val specified' = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
86 |
specified |> Symtab.default (c, Inttab.empty) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
87 |
|> Symtab.map_entry c (Inttab.update (serial (), (name, T)) #> tap (check_specified c)); |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
88 |
val monomorphic' = monomorphic |> update_monomorphic specified' c; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
89 |
in (consts', specified', monomorphic') end); |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
90 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
91 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
92 |
(* empty and 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 |
val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
95 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
96 |
fun merge pp |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
97 |
(Defs {consts = consts1, specified = specified1, monomorphic}, |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
98 |
Defs {consts = consts2, specified = specified2, ...}) = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
99 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
100 |
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
|
101 |
handle Graph.CYCLES cycles => err_cyclic cycles; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
102 |
val specified' = (specified1, specified2) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
103 |
|> Symtab.join (fn c => Inttab.merge (K true) #> tap (check_specified c) #> SOME); |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
104 |
val monomorphic' = monomorphic |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
105 |
|> Symtab.fold (update_monomorphic specified' o #1) specified'; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
106 |
in make_defs (consts', specified', monomorphic') end; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
107 |
|
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
|
108 |
end; |