author | wenzelm |
Tue, 22 Sep 2015 20:21:53 +0200 | |
changeset 61253 | 63875746d82d |
parent 61249 | 8611f408ec13 |
child 61254 | 4918c6e52a02 |
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 |
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
2 |
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
|
3 |
|
19692 | 4 |
Global well-formedness checks for constant definitions. Covers plain |
19701 | 5 |
definitions and simple sub-structural overloading. |
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
|
6 |
*) |
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 |
|
16877
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
8 |
signature DEFS = |
e92cba1d4842
tuned interfaces declare, define, finalize, merge:
wenzelm
parents:
16838
diff
changeset
|
9 |
sig |
61249 | 10 |
datatype item_kind = Constant | Type |
11 |
type item = item_kind * string |
|
12 |
val item_ord: item * item -> order |
|
61253 | 13 |
val pretty_args: Proof.context -> typ list -> Pretty.T list |
19701 | 14 |
val plain_args: typ list -> bool |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
15 |
type T |
33712 | 16 |
type spec = |
55544 | 17 |
{def: string option, |
18 |
description: string, |
|
19 |
pos: Position.T, |
|
20 |
lhs: typ list, |
|
61249 | 21 |
rhs: (item * typ list) list} |
22 |
val all_specifications_of: T -> (item * spec list) list |
|
23 |
val specifications_of: T -> item -> spec list |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
24 |
val dest: T -> |
61249 | 25 |
{restricts: ((item * typ list) * string) list, |
26 |
reducts: ((item * typ list) * (item * typ list) list) list} |
|
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
27 |
val empty: T |
42389 | 28 |
val merge: Proof.context -> T * T -> T |
42384 | 29 |
val define: Proof.context -> bool -> string option -> string -> |
61249 | 30 |
item * typ list -> (item * typ list) list -> T -> T |
31 |
end; |
|
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59050
diff
changeset
|
32 |
|
17711 | 33 |
structure Defs: DEFS = |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
34 |
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
|
35 |
|
61249 | 36 |
(* specification items *) |
37 |
||
38 |
datatype item_kind = Constant | Type; |
|
39 |
type item = item_kind * string; |
|
40 |
||
41 |
fun item_kind_ord (Constant, Type) = LESS |
|
42 |
| item_kind_ord (Type, Constant) = GREATER |
|
43 |
| item_kind_ord _ = EQUAL; |
|
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59050
diff
changeset
|
44 |
|
61249 | 45 |
val item_ord = prod_ord item_kind_ord string_ord; |
46 |
val fast_item_ord = prod_ord item_kind_ord fast_string_ord; |
|
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59050
diff
changeset
|
47 |
|
61253 | 48 |
fun print_item (k, s) = if k = Constant then s else "type " ^ s; |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59050
diff
changeset
|
49 |
|
61249 | 50 |
structure Itemtab = Table(type key = item val ord = fast_item_ord); |
51 |
||
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59050
diff
changeset
|
52 |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
53 |
(* type arguments *) |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
54 |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
55 |
type args = typ list; |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
56 |
|
61253 | 57 |
fun pretty_args ctxt args = |
58 |
if null args then [] |
|
59 |
else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)]; |
|
60 |
||
61 |
fun pretty_entry ctxt (c, args) = |
|
62 |
Pretty.block (Pretty.str (print_item c) :: pretty_args ctxt args); |
|
19624 | 63 |
|
19707 | 64 |
fun plain_args args = |
65 |
forall Term.is_TVar args andalso not (has_duplicates (op =) args); |
|
66 |
||
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
67 |
fun disjoint_args (Ts, Us) = |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
68 |
not (Type.could_unifys (Ts, Us)) orelse |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
69 |
((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
|
70 |
handle Type.TUNIFY => true); |
19692 | 71 |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
72 |
fun match_args (Ts, Us) = |
56050
fdccbb97915a
minor performance tuning via fast matching filter;
wenzelm
parents:
55544
diff
changeset
|
73 |
if Type.could_matches (Ts, Us) then |
fdccbb97915a
minor performance tuning via fast matching filter;
wenzelm
parents:
55544
diff
changeset
|
74 |
Option.map Envir.subst_type |
fdccbb97915a
minor performance tuning via fast matching filter;
wenzelm
parents:
55544
diff
changeset
|
75 |
(SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE) |
fdccbb97915a
minor performance tuning via fast matching filter;
wenzelm
parents:
55544
diff
changeset
|
76 |
else NONE; |
19692 | 77 |
|
78 |
||
79 |
(* datatype defs *) |
|
80 |
||
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
32785
diff
changeset
|
81 |
type spec = |
55544 | 82 |
{def: string option, |
83 |
description: string, |
|
84 |
pos: Position.T, |
|
85 |
lhs: args, |
|
61249 | 86 |
rhs: (item * args) list}; |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
87 |
|
19692 | 88 |
type def = |
55544 | 89 |
{specs: spec Inttab.table, (*source specifications*) |
90 |
restricts: (args * string) list, (*global restrictions imposed by incomplete patterns*) |
|
61249 | 91 |
reducts: (args * (item * args) list) list}; (*specifications as reduction system*) |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
92 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
93 |
fun make_def (specs, restricts, reducts) = |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
94 |
{specs = specs, restricts = restricts, reducts = reducts}: def; |
19692 | 95 |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
96 |
fun map_def c f = |
61249 | 97 |
Itemtab.default (c, make_def (Inttab.empty, [], [])) #> |
98 |
Itemtab.map_entry c (fn {specs, restricts, reducts}: def => |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
99 |
make_def (f (specs, restricts, reducts))); |
19692 | 100 |
|
101 |
||
61249 | 102 |
datatype T = Defs of def Itemtab.table; |
19692 | 103 |
|
19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset
|
104 |
fun lookup_list which defs c = |
61249 | 105 |
(case Itemtab.lookup defs c of |
19713 | 106 |
SOME (def: def) => which def |
19692 | 107 |
| NONE => []); |
108 |
||
32050 | 109 |
fun all_specifications_of (Defs defs) = |
61249 | 110 |
(map o apsnd) (map snd o Inttab.dest o #specs) (Itemtab.dest defs); |
32050 | 111 |
|
24199 | 112 |
fun specifications_of (Defs defs) = lookup_list (map snd o Inttab.dest o #specs) defs; |
32050 | 113 |
|
19692 | 114 |
val restricts_of = lookup_list #restricts; |
115 |
val reducts_of = lookup_list #reducts; |
|
116 |
||
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
117 |
fun dest (Defs defs) = |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
118 |
let |
61249 | 119 |
val restricts = Itemtab.fold (fn (c, {restricts, ...}) => |
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
32785
diff
changeset
|
120 |
fold (fn (args, description) => cons ((c, args), description)) restricts) defs []; |
61249 | 121 |
val reducts = Itemtab.fold (fn (c, {reducts, ...}) => |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
122 |
fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs []; |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
123 |
in {restricts = restricts, reducts = reducts} end; |
19692 | 124 |
|
61249 | 125 |
val empty = Defs Itemtab.empty; |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
126 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
127 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
128 |
(* specifications *) |
19692 | 129 |
|
55544 | 130 |
fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = |
131 |
Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
132 |
i = j orelse disjoint_args (Ts, Us) orelse |
61249 | 133 |
error ("Clash of specifications for " ^ print_item c ^ ":\n" ^ |
55544 | 134 |
" " ^ quote a ^ Position.here pos_a ^ "\n" ^ |
135 |
" " ^ quote b ^ Position.here pos_b)); |
|
19692 | 136 |
|
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
137 |
fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
138 |
let |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
139 |
val specs' = |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
140 |
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
|
141 |
in make_def (specs', restricts, reducts) end; |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
142 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
143 |
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
|
144 |
(disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts))); |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
145 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
146 |
|
19701 | 147 |
(* normalized dependencies: reduction with well-formedness check *) |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
148 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
149 |
local |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
150 |
|
61253 | 151 |
val prt = Pretty.string_of oo pretty_entry; |
42384 | 152 |
fun err ctxt (c, args) (d, Us) s1 s2 = |
61246
077b88f9ec16
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
wenzelm
parents:
59050
diff
changeset
|
153 |
error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2); |
19729 | 154 |
|
42384 | 155 |
fun acyclic ctxt (c, args) (d, Us) = |
19729 | 156 |
c <> d orelse |
157 |
is_none (match_args (args, Us)) orelse |
|
42384 | 158 |
err ctxt (c, args) (d, Us) "Circular" ""; |
19729 | 159 |
|
42384 | 160 |
fun wellformed ctxt defs (c, args) (d, Us) = |
57520
3ad1b289f21b
proper plain_args to ensure that multi-argument overloading cannot escape pattern restriction (despite more liberal structural containment before 3ae3cc4b1eac);
wenzelm
parents:
56050
diff
changeset
|
161 |
plain_args Us orelse |
19729 | 162 |
(case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of |
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
32785
diff
changeset
|
163 |
SOME (Ts, description) => |
42384 | 164 |
err ctxt (c, args) (d, Us) "Malformed" |
165 |
("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")") |
|
19729 | 166 |
| NONE => true); |
19692 | 167 |
|
42384 | 168 |
fun reduction ctxt defs const deps = |
19692 | 169 |
let |
19701 | 170 |
fun reduct Us (Ts, rhs) = |
171 |
(case match_args (Ts, Us) of |
|
172 |
NONE => NONE |
|
173 |
| SOME subst => SOME (map (apsnd (map subst)) rhs)); |
|
174 |
fun reducts (d, Us) = get_first (reduct Us) (reducts_of defs d); |
|
175 |
||
176 |
val reds = map (`reducts) deps; |
|
177 |
val deps' = |
|
178 |
if forall (is_none o #1) reds then NONE |
|
20668 | 179 |
else SOME (fold_rev |
180 |
(fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []); |
|
42384 | 181 |
val _ = forall (acyclic ctxt const) (the_default deps deps'); |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
182 |
in deps' end; |
19692 | 183 |
|
19760 | 184 |
in |
185 |
||
42384 | 186 |
fun normalize ctxt = |
19692 | 187 |
let |
19701 | 188 |
fun norm_update (c, {reducts, ...}: def) (changed, defs) = |
189 |
let |
|
190 |
val reducts' = reducts |> map (fn (args, deps) => |
|
42384 | 191 |
(args, perhaps (reduction ctxt defs (c, args)) deps)); |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
192 |
in |
19701 | 193 |
if reducts = reducts' then (changed, defs) |
32785 | 194 |
else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts'))) |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
195 |
end; |
19701 | 196 |
fun norm_all defs = |
61249 | 197 |
(case Itemtab.fold norm_update defs (false, defs) of |
19701 | 198 |
(true, defs') => norm_all defs' |
199 |
| (false, _) => defs); |
|
19729 | 200 |
fun check defs (c, {reducts, ...}: def) = |
42384 | 201 |
reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps); |
61249 | 202 |
in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end; |
19701 | 203 |
|
42384 | 204 |
fun dependencies ctxt (c, args) restr deps = |
19712
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset
|
205 |
map_def c (fn (specs, restricts, reducts) => |
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset
|
206 |
let |
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset
|
207 |
val restricts' = Library.merge (op =) (restricts, restr); |
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset
|
208 |
val reducts' = insert (op =) (args, deps) reducts; |
3ae3cc4b1eac
wellformed: be less ambitious about structural containment;
wenzelm
parents:
19707
diff
changeset
|
209 |
in (specs, restricts', reducts') end) |
42384 | 210 |
#> normalize ctxt; |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
211 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
212 |
end; |
19692 | 213 |
|
214 |
||
19624 | 215 |
(* merge *) |
216 |
||
42389 | 217 |
fun merge ctxt (Defs defs1, Defs defs2) = |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
218 |
let |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
219 |
fun add_deps (c, args) restr deps defs = |
19692 | 220 |
if AList.defined (op =) (reducts_of defs c) args then defs |
42384 | 221 |
else dependencies ctxt (c, args) restr deps defs; |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
222 |
fun add_def (c, {restricts, reducts, ...}: def) = |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
223 |
fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; |
19760 | 224 |
in |
61249 | 225 |
Defs (Itemtab.join join_specs (defs1, defs2) |
226 |
|> normalize ctxt |> Itemtab.fold add_def defs2) |
|
19760 | 227 |
end; |
19613
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
228 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
229 |
|
9bf274ec94cf
allow dependencies of disjoint collections of instances;
wenzelm
parents:
19590
diff
changeset
|
230 |
(* define *) |
19590
12af4942923d
simple substructure test for typargs (independent type constructors);
wenzelm
parents:
19569
diff
changeset
|
231 |
|
42384 | 232 |
fun define ctxt unchecked def description (c, args) deps (Defs defs) = |
17707
bc0270e9d27f
back to simple 'defs' (cf. revision 1.79 of theory.ML);
wenzelm
parents:
17670
diff
changeset
|
233 |
let |
55544 | 234 |
val pos = Position.thread_data (); |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
235 |
val restr = |
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
236 |
if plain_args args orelse |
61249 | 237 |
(case args of [Term.Type (_, rec_args)] => plain_args rec_args | _ => false) |
33701
9dd1079cec3a
primitive defs: clarified def (axiom name) vs. description;
wenzelm
parents:
32785
diff
changeset
|
238 |
then [] else [(args, description)]; |
19692 | 239 |
val spec = |
55544 | 240 |
(serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps}); |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
241 |
val defs' = defs |> update_specs c spec; |
42384 | 242 |
in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end; |
19697
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
243 |
|
423af2e013b8
specifications_of: lhs/rhs represented as typargs;
wenzelm
parents:
19695
diff
changeset
|
244 |
end; |