author | wenzelm |
Tue, 22 Nov 2005 19:34:48 +0100 | |
changeset 18228 | 628c11780077 |
parent 17994 | 6a1a49cba5b3 |
child 19025 | 596fb1eb7856 |
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 |
17712 | 12 |
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
|
13 |
val empty: T |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
14 |
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
|
15 |
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
|
16 |
|
17711 | 17 |
structure Defs: DEFS = |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
18 |
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
|
19 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
20 |
(** datatype T **) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
21 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
22 |
datatype T = Defs of |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
23 |
{consts: typ Graph.T, (*constant declarations and dependencies*) |
17994 | 24 |
specified: (string * typ) Inttab.table Symtab.table}; (*specification name and const type*) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
25 |
|
17994 | 26 |
fun make_defs (consts, specified) = Defs {consts = consts, specified = specified}; |
27 |
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
|
28 |
|
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 |
(* specified consts *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
31 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
32 |
fun disjoint_types T U = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
33 |
(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
|
34 |
handle Type.TUNIFY => true; |
16308 | 35 |
|
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
36 |
fun check_specified c (i, (a, T)) = Inttab.forall (fn (j, (b, U)) => |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
37 |
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
|
38 |
error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
39 |
" for constant " ^ quote c)); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
40 |
|
16982 | 41 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
42 |
(* define consts *) |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
43 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
44 |
fun err_cyclic cycles = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
45 |
error ("Cyclic dependency of constants:\n" ^ |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
46 |
cat_lines (map (space_implode " -> " o map quote o rev) cycles)); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
47 |
|
17994 | 48 |
fun define const_type 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
|
49 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
50 |
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
|
51 |
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
|
52 |
handle Graph.CYCLES cycles => err_cyclic cycles; |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
53 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
54 |
val (c, T) = lhs; |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
55 |
val spec = (serial (), (name, T)); |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
56 |
val no_overloading = Type.raw_instance (const_type c, T); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
57 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
58 |
val consts' = |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
59 |
consts |> declare lhs |> fold declare rhs |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
60 |
|> K no_overloading ? add_deps (c, map #1 rhs); |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
61 |
val specified' = specified |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
62 |
|> Symtab.default (c, Inttab.empty) |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
63 |
|> Symtab.map_entry c (fn specs => |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
64 |
(check_specified c spec specs; Inttab.update spec specs)); |
17994 | 65 |
in (consts', specified') end); |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
66 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
67 |
|
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
68 |
(* empty and merge *) |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
69 |
|
17994 | 70 |
val empty = make_defs (Graph.empty, Symtab.empty); |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
71 |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
72 |
fun merge pp |
17994 | 73 |
(Defs {consts = consts1, specified = specified1}, |
74 |
Defs {consts = consts2, specified = specified2}) = |
|
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
75 |
let |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
76 |
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
|
77 |
handle Graph.CYCLES cycles => err_cyclic cycles; |
17803
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
78 |
val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) => |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
79 |
SOME (Inttab.fold (fn spec2 => fn specs1 => |
e235a57651a1
more efficient check_specified, much less invocations;
wenzelm
parents:
17712
diff
changeset
|
80 |
(check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1)); |
17994 | 81 |
in make_defs (consts', specified') end; |
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
82 |
|
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 |
end; |