author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24792  fd4655e57168 
child 29606  fedb8be05f24 
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 

19692  5 
Global wellformedness checks for constant definitions. Covers plain 
19701  6 
definitions and simple substructural overloading. 
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 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

11 
val pretty_const: Pretty.pp > string * typ list > Pretty.T 
19701  12 
val plain_args: typ list > bool 
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset

13 
type T 
24199  14 
val specifications_of: T > string > {is_def: bool, name: string, 
15 
lhs: typ list, rhs: (string * typ list) list} list 

16 
val all_specifications_of: T > (string * {is_def: bool, name: string, 

17 
lhs: typ list, rhs: (string * typ list) list} list) list 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

18 
val dest: T > 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

19 
{restricts: ((string * typ list) * string) list, 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

20 
reducts: ((string * typ list) * (string * typ list) list) list} 
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset

21 
val empty: T 
19692  22 
val merge: Pretty.pp > T * T > T 
24199  23 
val define: Pretty.pp > bool > bool > string > 
19727  24 
string * typ list > (string * typ list) list > 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

25 
end 
cf468b93a02e
Implement cyclefree overloading, so that definitions cannot harm consistency any more (except of course via interaction with axioms).
obua
parents:
diff
changeset

26 

17711  27 
structure Defs: DEFS = 
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset

28 
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

29 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

30 
(* type arguments *) 
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset

31 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

32 
type args = typ list; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

33 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

34 
fun pretty_const pp (c, args) = 
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset

35 
let 
19692  36 
val prt_args = 
37 
if null args then [] 

19806  38 
else [Pretty.list "(" ")" (map (Pretty.typ pp o Logic.unvarifyT) args)]; 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

39 
in Pretty.block (Pretty.str c :: prt_args) end; 
19624  40 

19707  41 
fun plain_args args = 
42 
forall Term.is_TVar args andalso not (has_duplicates (op =) args); 

43 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

44 
fun disjoint_args (Ts, Us) = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

45 
not (Type.could_unifys (Ts, Us)) orelse 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

46 
((Type.raw_unifys (Ts, map (Logic.incr_tvar (maxidx_of_typs Ts + 1)) Us) Vartab.empty; false) 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

47 
handle Type.TUNIFY => true); 
19692  48 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

49 
fun match_args (Ts, Us) = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

50 
Option.map Envir.typ_subst_TVars 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

51 
(SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE); 
19692  52 

53 

54 
(* datatype defs *) 

55 

24199  56 
type spec = {is_def: bool, name: string, lhs: args, rhs: (string * args) list}; 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

57 

19692  58 
type def = 
19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

59 
{specs: spec Inttab.table, (*source specifications*) 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

60 
restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

61 
reducts: (args * (string * args) list) list}; (*specifications as reduction system*) 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

62 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

63 
fun make_def (specs, restricts, reducts) = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

64 
{specs = specs, restricts = restricts, reducts = reducts}: def; 
19692  65 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

66 
fun map_def c f = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

67 
Symtab.default (c, make_def (Inttab.empty, [], [])) #> 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

68 
Symtab.map_entry c (fn {specs, restricts, reducts}: def => 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

69 
make_def (f (specs, restricts, reducts))); 
19692  70 

71 

72 
datatype T = Defs of def Symtab.table; 

73 

19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

74 
fun lookup_list which defs c = 
19692  75 
(case Symtab.lookup defs c of 
19713  76 
SOME (def: def) => which def 
19692  77 
 NONE => []); 
78 

24199  79 
fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs; 
80 
fun all_specifications_of (Defs defs) = 

81 
((map o apsnd) (map snd o Inttab.dest o #specs) o Symtab.dest) defs; 

19692  82 
val restricts_of = lookup_list #restricts; 
83 
val reducts_of = lookup_list #reducts; 

84 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

85 
fun dest (Defs defs) = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

86 
let 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

87 
val restricts = Symtab.fold (fn (c, {restricts, ...}) => 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

88 
fold (fn (args, name) => cons ((c, args), name)) restricts) defs []; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

89 
val reducts = Symtab.fold (fn (c, {reducts, ...}) => 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

90 
fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs []; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

91 
in {restricts = restricts, reducts = reducts} end; 
19692  92 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

93 
val empty = Defs Symtab.empty; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

94 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

95 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

96 
(* specifications *) 
19692  97 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

98 
fun disjoint_specs c (i, {lhs = Ts, name = a, ...}: spec) = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

99 
Inttab.forall (fn (j, {lhs = Us, name = b, ...}: spec) => 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

100 
i = j orelse disjoint_args (Ts, Us) orelse 
24792  101 
error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^ 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

102 
" for constant " ^ quote c)); 
19692  103 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

104 
fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

105 
let 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

106 
val specs' = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

107 
Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

108 
in make_def (specs', restricts, reducts) end; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

109 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

110 
fun update_specs c spec = map_def c (fn (specs, restricts, reducts) => 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

111 
(disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts))); 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

112 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

113 

19701  114 
(* normalized dependencies: reduction with wellformedness check *) 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

115 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

116 
local 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

117 

19729  118 
val prt = Pretty.string_of oo pretty_const; 
119 
fun err pp (c, args) (d, Us) s1 s2 = 

120 
error (s1 ^ " dependency of constant " ^ prt pp (c, args) ^ " > " ^ prt pp (d, Us) ^ s2); 

121 

19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

122 
fun contained (U as TVar _) (Type (_, Ts)) = exists (fn T => T = U orelse contained U T) Ts 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

123 
 contained _ _ = false; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

124 

19729  125 
fun acyclic pp defs (c, args) (d, Us) = 
126 
c <> d orelse 

127 
exists (fn U => exists (contained U) args) Us orelse 

128 
is_none (match_args (args, Us)) orelse 

129 
err pp (c, args) (d, Us) "Circular" ""; 

130 

19701  131 
fun wellformed pp defs (c, args) (d, Us) = 
19729  132 
forall is_TVar Us orelse 
133 
(case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of 

134 
SOME (Ts, name) => 

135 
err pp (c, args) (d, Us) "Malformed" 

136 
("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote name ^ ")") 

137 
 NONE => true); 

19692  138 

19701  139 
fun reduction pp defs const deps = 
19692  140 
let 
19701  141 
fun reduct Us (Ts, rhs) = 
142 
(case match_args (Ts, Us) of 

143 
NONE => NONE 

144 
 SOME subst => SOME (map (apsnd (map subst)) rhs)); 

145 
fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d); 

146 

147 
val reds = map (`reducts) deps; 

148 
val deps' = 

149 
if forall (is_none o #1) reds then NONE 

20668  150 
else SOME (fold_rev 
151 
(fn (NONE, dp) => insert (op =) dp  (SOME dps, _) => fold (insert (op =)) dps) reds []); 

19729  152 
val _ = forall (acyclic pp defs const) (the_default deps deps'); 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

153 
in deps' end; 
19692  154 

19760  155 
in 
156 

19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

157 
fun normalize pp = 
19692  158 
let 
19701  159 
fun norm_update (c, {reducts, ...}: def) (changed, defs) = 
160 
let 

161 
val reducts' = reducts > map (fn (args, deps) => 

19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

162 
(args, perhaps (reduction pp defs (c, args)) deps)); 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

163 
in 
19701  164 
if reducts = reducts' then (changed, defs) 
165 
else (true, defs > map_def c (fn (specs, restricts, reducts) => 

166 
(specs, restricts, reducts'))) 

19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

167 
end; 
19701  168 
fun norm_all defs = 
169 
(case Symtab.fold norm_update defs (false, defs) of 

170 
(true, defs') => norm_all defs' 

171 
 (false, _) => defs); 

19729  172 
fun check defs (c, {reducts, ...}: def) = 
173 
reducts > forall (fn (args, deps) => forall (wellformed pp defs (c, args)) deps); 

174 
in norm_all #> (fn defs => tap (Symtab.forall (check defs)) defs) end; 

19701  175 

19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

176 
fun dependencies pp (c, args) restr deps = 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

177 
map_def c (fn (specs, restricts, reducts) => 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

178 
let 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

179 
val restricts' = Library.merge (op =) (restricts, restr); 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

180 
val reducts' = insert (op =) (args, deps) reducts; 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

181 
in (specs, restricts', reducts') end) 
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

182 
#> normalize pp; 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

183 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

184 
end; 
19692  185 

186 

19624  187 
(* merge *) 
188 

19692  189 
fun merge pp (Defs defs1, Defs defs2) = 
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset

190 
let 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

191 
fun add_deps (c, args) restr deps defs = 
19692  192 
if AList.defined (op =) (reducts_of defs c) args then defs 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

193 
else dependencies pp (c, args) restr deps defs; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

194 
fun add_def (c, {restricts, reducts, ...}: def) = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

195 
fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; 
19760  196 
in 
197 
Defs (Symtab.join join_specs (defs1, defs2) 

198 
> normalize pp > Symtab.fold add_def defs2) 

199 
end; 

19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset

200 

9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset

201 

9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset

202 
(* define *) 
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset

203 

24199  204 
fun define pp unchecked is_def name (c, args) deps (Defs defs) = 
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset

205 
let 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

206 
val restr = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

207 
if plain_args args orelse 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

208 
(case args of [Type (a, rec_args)] => plain_args rec_args  _ => false) 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

209 
then [] else [(args, name)]; 
19692  210 
val spec = 
24199  211 
(serial (), {is_def = is_def, name = name, lhs = args, rhs = deps}); 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

212 
val defs' = defs > update_specs c spec; 
19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

213 
in Defs (defs' > (if unchecked then I else dependencies pp (c, args) restr deps)) end; 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

214 

423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

215 
end; 