author  wenzelm 
Thu, 29 Sep 2005 01:09:39 +0200  
changeset 17711  c16cbe73798c 
parent 17707  bc0270e9d27f 
child 17712  46c2091e5187 
permissions  rwrr 
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 cyclefree 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 cyclefree 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 wellformedness 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 nonoverloaded definitions! 
16108
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

7 
*) 
cf468b93a02e
Implement cyclefree 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 
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset

13 
val define: string > string * typ > (string * typ) list > T > T 
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 cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

16 
end 
cf468b93a02e
Implement cyclefree 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 cyclefree 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 cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

108 
end; 