author  wenzelm 
Wed, 24 May 2006 22:04:06 +0200  
changeset 19713  69c71d40f8a8 
parent 19712  3ae3cc4b1eac 
child 19727  f5895f998402 
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 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

14 
val specifications_of: T > string > (serial * {is_def: bool, module: string, name: string, 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

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

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

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

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

19 
val empty: T 
19692  20 
val merge: Pretty.pp > T * T > T 
21 
val define: Pretty.pp > Consts.T > 

19628  22 
bool > bool > string > string > string * typ > (string * typ) 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

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

24 

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

26 
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

27 

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

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

29 

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

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

31 

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

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

33 
let 
19692  34 
val prt_args = 
35 
if null args then [] 

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

36 
else [Pretty.list "(" ")" (map (Pretty.typ pp o Type.freeze_type) args)]; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

37 
in Pretty.block (Pretty.str c :: prt_args) end; 
19624  38 

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

41 

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

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

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

44 
((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

45 
handle Type.TUNIFY => true); 
19692  46 

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

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

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

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

51 

52 
(* datatype defs *) 

53 

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

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

55 

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

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

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

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

60 

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

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

62 
{specs = specs, restricts = restricts, reducts = reducts}: def; 
19692  63 

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

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

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

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

67 
make_def (f (specs, restricts, reducts))); 
19692  68 

69 

70 
datatype T = Defs of def Symtab.table; 

71 

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

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

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

77 
fun specifications_of (Defs defs) = lookup_list (Inttab.dest o #specs) defs; 
19692  78 
val restricts_of = lookup_list #restricts; 
79 
val reducts_of = lookup_list #reducts; 

80 

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

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

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

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

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

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

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

87 
in {restricts = restricts, reducts = reducts} end; 
19692  88 

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

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

90 

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

91 

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

92 
(* specifications *) 
19692  93 

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

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

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

96 
i = j orelse disjoint_args (Ts, Us) orelse 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

97 
error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

98 
" for constant " ^ quote c)); 
19692  99 

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

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

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

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

103 
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

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

105 

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

106 
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

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

108 

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

109 

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

111 

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

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

113 

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

114 
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

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

116 

19701  117 
fun wellformed pp defs (c, args) (d, Us) = 
19692  118 
let 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

119 
val prt = Pretty.string_of o pretty_const pp; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

120 
fun err s1 s2 = 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

121 
error (s1 ^ " dependency of constant " ^ prt (c, args) ^ " > " ^ prt (d, Us) ^ s2); 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

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

123 
exists (fn U => exists (contained U) args) Us orelse 
19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

124 
(c <> d andalso forall is_TVar Us) orelse 
19701  125 
(if c = d andalso is_some (match_args (args, Us)) then err "Circular" "" else 
126 
(case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of 

127 
SOME (Ts, name) => 

128 
is_some (match_args (Ts, Us)) orelse 

129 
err "Malformed" ("\n(restriction " ^ prt (d, Ts) ^ " from " ^ quote name ^ ")") 

130 
 NONE => true)) 

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

131 
end; 
19692  132 

19701  133 
fun reduction pp defs const deps = 
19692  134 
let 
19701  135 
fun reduct Us (Ts, rhs) = 
136 
(case match_args (Ts, Us) of 

137 
NONE => NONE 

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

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

140 

141 
fun add (NONE, dp) = insert (op =) dp 

142 
 add (SOME dps, _) = fold (insert (op =)) dps; 

143 
val reds = map (`reducts) deps; 

144 
val deps' = 

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

146 
else SOME (fold_rev add reds []); 

147 
val _ = forall (wellformed pp defs const) (the_default deps deps'); 

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

148 
in deps' end; 
19692  149 

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

150 
fun normalize pp = 
19692  151 
let 
19701  152 
fun norm_update (c, {reducts, ...}: def) (changed, defs) = 
153 
let 

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

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

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

156 
in 
19701  157 
if reducts = reducts' then (changed, defs) 
158 
else (true, defs > map_def c (fn (specs, restricts, reducts) => 

159 
(specs, restricts, reducts'))) 

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

160 
end; 
19701  161 
fun norm_all defs = 
162 
(case Symtab.fold norm_update defs (false, defs) of 

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

164 
 (false, _) => defs); 

165 
in norm_all end; 

166 

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

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

168 

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

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

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

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

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

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

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

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

176 

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

177 
end; 
19692  178 

179 

19624  180 
(* merge *) 
181 

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

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

184 
fun add_deps (c, args) restr deps defs = 
19692  185 
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

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

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

188 
fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; 
19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset

189 
in Defs (Symtab.join join_specs (defs1, defs2) > Symtab.fold add_def defs2) end; 
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset

190 

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

191 

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

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

193 

19692  194 
fun define pp consts unchecked is_def module name lhs rhs (Defs defs) = 
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset

195 
let 
19692  196 
fun typargs const = (#1 const, Consts.typargs consts const); 
197 
val (c, args) = typargs lhs; 

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

198 
val deps = map typargs rhs; 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

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

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

201 
(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

202 
then [] else [(args, name)]; 
19692  203 
val spec = 
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

204 
(serial (), {is_def = is_def, module = module, name = name, lhs = args, rhs = deps}); 
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset

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

206 
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

207 

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

208 
end; 