1 (* Title: Pure/General/defs.ML |
1 (* Title: Pure/defs.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Steven Obua, TU Muenchen |
3 Author: Makarius |
4 |
4 |
5 Checks if definitions preserve consistency of logic by enforcing that |
5 Global well-formedness checks for constant definitions. Dependencies |
6 there are no cyclic definitions. The algorithm is described in "An |
6 are only tracked for non-overloaded definitions! |
7 Algorithm for Determining Definitional Cycles in Higher-Order Logic |
|
8 with Overloading", Steven Obua, technical report, to be written :-) |
|
9 |
|
10 ATTENTION: |
|
11 Currently this implementation of the cycle test contains a bug of which the author is fully aware. |
|
12 This bug makes it possible to introduce inconsistent definitional cycles in Isabelle. |
|
13 *) |
7 *) |
14 |
8 |
15 signature DEFS = |
9 signature DEFS = |
16 sig |
10 sig |
17 (*true: record the full chain of definitions that lead to a circularity*) |
11 type T |
18 val chain_history: bool ref |
12 val monomorphic: T -> string -> bool |
19 type graph |
13 val define: string -> string * typ -> (string * typ) list -> T -> T |
20 val empty: graph |
14 val empty: T |
21 val declare: theory -> string * typ -> graph -> graph |
15 val merge: Pretty.pp -> T * T -> T |
22 val define: theory -> string * typ -> string -> (string * typ) list -> graph -> graph |
|
23 val finalize: theory -> string * typ -> graph -> graph |
|
24 val merge: Pretty.pp -> graph -> graph -> graph |
|
25 val finals: graph -> typ list Symtab.table |
|
26 datatype overloadingstate = Open | Closed | Final |
|
27 val overloading_info: graph -> string -> (typ * (string*typ) list * overloadingstate) option |
|
28 val monomorphic: graph -> string -> bool |
|
29 end |
16 end |
30 |
17 |
31 structure Defs :> DEFS = struct |
18 structure Defs (* FIXME : DEFS *) = |
|
19 struct |
32 |
20 |
33 type tyenv = Type.tyenv |
21 (** datatype T **) |
34 type edgelabel = (int * typ * typ * (typ * string * string) list) |
|
35 |
22 |
36 datatype overloadingstate = Open | Closed | Final |
23 datatype T = Defs of |
|
24 {consts: typ Graph.T, (*constant declarations and dependencies*) |
|
25 specified: (string * typ) Inttab.table Symtab.table, (*specification name and const type*) |
|
26 monomorphic: unit Symtab.table}; (*constants having monomorphic specs*) |
37 |
27 |
38 datatype node = Node of |
28 fun rep_defs (Defs args) = args; |
39 typ (* most general type of constant *) |
|
40 * defnode Symtab.table |
|
41 (* a table of defnodes, each corresponding to 1 definition of the |
|
42 constant for a particular type, indexed by axiom name *) |
|
43 * (unit Symtab.table) Symtab.table |
|
44 (* a table of all back referencing defnodes to this node, |
|
45 indexed by node name of the defnodes *) |
|
46 * typ list (* a list of all finalized types *) |
|
47 * overloadingstate |
|
48 |
29 |
49 and defnode = Defnode of |
30 fun make_defs (consts, specified, monomorphic) = |
50 typ (* type of the constant in this particular definition *) |
31 Defs {consts = consts, specified = specified, monomorphic = monomorphic}; |
51 * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *) |
|
52 |
32 |
53 fun getnode graph = the o Symtab.lookup graph |
33 fun map_defs f (Defs {consts, specified, monomorphic}) = |
54 fun get_nodedefs (Node (_, defs, _, _, _)) = defs |
34 make_defs (f (consts, specified, monomorphic)); |
55 fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup defs defname |
|
56 fun get_defnode' graph noderef = |
|
57 Symtab.lookup (get_nodedefs (the (Symtab.lookup graph noderef))) |
|
58 |
|
59 fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0; |
|
60 |
|
61 datatype graphaction = |
|
62 Declare of string * typ |
|
63 | Define of string * typ * string * string * (string * typ) list |
|
64 | Finalize of string * typ |
|
65 |
|
66 type graph = int * string Symtab.table * graphaction list * node Symtab.table |
|
67 |
|
68 val chain_history = ref true |
|
69 |
|
70 val empty = (0, Symtab.empty, [], Symtab.empty) |
|
71 |
|
72 exception DEFS of string; |
|
73 exception CIRCULAR of (typ * string * string) list; |
|
74 exception INFINITE_CHAIN of (typ * string * string) list; |
|
75 exception CLASH of string * string * string; |
|
76 exception FINAL of string * typ; |
|
77 |
|
78 fun def_err s = raise (DEFS s) |
|
79 |
|
80 fun no_forwards defs = |
|
81 Symtab.foldl |
|
82 (fn (closed, (_, Defnode (_, edges))) => |
|
83 if not closed then false else Symtab.is_empty edges) |
|
84 (true, defs) |
|
85 |
|
86 fun checkT' (Type (a, Ts)) = Type (a, map checkT' Ts) |
|
87 | checkT' (TFree (a, _)) = TVar ((a, 0), []) |
|
88 | checkT' (TVar ((a, 0), _)) = TVar ((a, 0), []) |
|
89 | checkT' (T as TVar _) = raise TYPE ("Illegal schematic type variable encountered", [T], []); |
|
90 |
|
91 fun checkT thy = Compress.typ thy o checkT'; |
|
92 |
|
93 fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2; |
|
94 |
|
95 fun subst_incr_tvar inc t = |
|
96 if inc > 0 then |
|
97 let |
|
98 val tv = typ_tvars t |
|
99 val t' = Logic.incr_tvar inc t |
|
100 fun update_subst ((n, i), _) = |
|
101 Vartab.update ((n, i), ([], TVar ((n, i + inc), []))); |
|
102 in |
|
103 (t', fold update_subst tv Vartab.empty) |
|
104 end |
|
105 else |
|
106 (t, Vartab.empty) |
|
107 |
|
108 fun subst s ty = Envir.norm_type s ty |
|
109 |
|
110 fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history |
|
111 |
|
112 fun is_instance instance_ty general_ty = |
|
113 Type.raw_instance (instance_ty, general_ty) |
|
114 |
|
115 fun is_instance_r instance_ty general_ty = |
|
116 is_instance instance_ty (rename instance_ty general_ty) |
|
117 |
|
118 fun unify ty1 ty2 = |
|
119 SOME (Type.raw_unify (ty1, ty2) Vartab.empty) |
|
120 handle Type.TUNIFY => NONE |
|
121 |
|
122 (* |
|
123 Unifies ty1 and ty2, renaming ty1 and ty2 so that they have greater indices than max and |
|
124 so that they are different. All indices in ty1 and ty2 are supposed to be less than or |
|
125 equal to max. |
|
126 Returns SOME (max', s1, s2), so that s1(ty1) = s2(ty2) and max' is greater or equal than |
|
127 all indices in s1, s2, ty1, ty2. |
|
128 *) |
|
129 fun unify_r max ty1 ty2 = |
|
130 let |
|
131 val max = Int.max(max, 0) |
|
132 val max1 = max (* >= maxidx_of_typ ty1 *) |
|
133 val max2 = max (* >= maxidx_of_typ ty2 *) |
|
134 val max = Int.max(max, Int.max (max1, max2)) |
|
135 val (ty1, s1) = subst_incr_tvar (max + 1) ty1 |
|
136 val (ty2, s2) = subst_incr_tvar (max + max1 + 2) ty2 |
|
137 val max = max + max1 + max2 + 2 |
|
138 fun merge a b = Vartab.merge (fn _ => false) (a, b) |
|
139 in |
|
140 case unify ty1 ty2 of |
|
141 NONE => NONE |
|
142 | SOME s => SOME (max, merge s1 s, merge s2 s) |
|
143 end |
|
144 |
|
145 fun can_be_unified_r ty1 ty2 = is_some (unify ty1 (rename ty1 ty2)) |
|
146 fun can_be_unified ty1 ty2 = is_some (unify ty1 ty2) |
|
147 |
|
148 fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) = |
|
149 if maxidx <= 1000000 then edge else |
|
150 let |
|
151 |
|
152 fun idxlist idx extract_ty inject_ty (tab, max) ts = |
|
153 foldr |
|
154 (fn (e, ((tab, max), ts)) => |
|
155 let |
|
156 val ((tab, max), ty) = idx (tab, max) (extract_ty e) |
|
157 val e = inject_ty (ty, e) |
|
158 in |
|
159 ((tab, max), e::ts) |
|
160 end) |
|
161 ((tab,max), []) ts |
|
162 |
|
163 fun idx (tab,max) (TVar ((a,i),_)) = |
|
164 (case Inttab.lookup tab i of |
|
165 SOME j => ((tab, max), TVar ((a,j),[])) |
|
166 | NONE => ((Inttab.update (i, max) tab, max + 1), TVar ((a,max),[]))) |
|
167 | idx (tab,max) (Type (t, ts)) = |
|
168 let |
|
169 val ((tab, max), ts) = idxlist idx I fst (tab, max) ts |
|
170 in |
|
171 ((tab,max), Type (t, ts)) |
|
172 end |
|
173 | idx (tab, max) ty = ((tab, max), ty) |
|
174 |
|
175 val ((tab,max), u1) = idx (Inttab.empty, 0) u1 |
|
176 val ((tab,max), v1) = idx (tab, max) v1 |
|
177 val ((tab,max), history) = |
|
178 idxlist idx |
|
179 (fn (ty,_,_) => ty) |
|
180 (fn (ty, (_, s1, s2)) => (ty, s1, s2)) |
|
181 (tab, max) history |
|
182 in |
|
183 (max, u1, v1, history) |
|
184 end |
|
185 |
|
186 fun compare_edges (e1 as (maxidx1, u1, v1, history1)) (e2 as (maxidx2, u2, v2, history2)) = |
|
187 let |
|
188 val t1 = u1 --> v1 |
|
189 val t2 = Logic.incr_tvar (maxidx1+1) (u2 --> v2) |
|
190 in |
|
191 if (is_instance t1 t2) then |
|
192 (if is_instance t2 t1 then |
|
193 SOME (int_ord (length history2, length history1)) |
|
194 else |
|
195 SOME LESS) |
|
196 else if (is_instance t2 t1) then |
|
197 SOME GREATER |
|
198 else |
|
199 NONE |
|
200 end |
|
201 |
|
202 fun merge_edges_1 (x, []) = [x] |
|
203 | merge_edges_1 (x, (y::ys)) = |
|
204 (case compare_edges x y of |
|
205 SOME LESS => (y::ys) |
|
206 | SOME EQUAL => (y::ys) |
|
207 | SOME GREATER => merge_edges_1 (x, ys) |
|
208 | NONE => y::(merge_edges_1 (x, ys))) |
|
209 |
|
210 fun merge_edges xs ys = foldl merge_edges_1 xs ys |
|
211 |
|
212 fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = |
|
213 (cost, axmap, (Declare cty)::actions, |
|
214 Symtab.update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph) |
|
215 handle Symtab.DUP _ => |
|
216 let |
|
217 val (Node (gty, _, _, _, _)) = the (Symtab.lookup graph name) |
|
218 in |
|
219 if is_instance_r ty gty andalso is_instance_r gty ty then |
|
220 g |
|
221 else |
|
222 def_err "constant is already declared with different type" |
|
223 end |
|
224 |
|
225 fun declare'' thy g (name, ty) = declare' g (name, checkT thy ty) |
|
226 |
|
227 val axcounter = ref (IntInf.fromInt 0) |
|
228 fun newaxname axmap axname = |
|
229 let |
|
230 val c = !axcounter |
|
231 val _ = axcounter := c+1 |
|
232 val axname' = axname^"_"^(IntInf.toString c) |
|
233 in |
|
234 (Symtab.update (axname', axname) axmap, axname') |
|
235 end |
|
236 |
|
237 fun translate_ex axmap x = |
|
238 let |
|
239 fun translate (ty, nodename, axname) = |
|
240 (ty, nodename, the (Symtab.lookup axmap axname)) |
|
241 in |
|
242 case x of |
|
243 INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain)) |
|
244 | CIRCULAR cycle => raise (CIRCULAR (map translate cycle)) |
|
245 | _ => raise x |
|
246 end |
|
247 |
|
248 fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body = |
|
249 let |
|
250 val mainnode = (case Symtab.lookup graph mainref of |
|
251 NONE => def_err ("constant "^mainref^" is not declared") |
|
252 | SOME n => n) |
|
253 val (Node (gty, defs, backs, finals, _)) = mainnode |
|
254 val _ = (if is_instance_r ty gty then () |
|
255 else def_err "type of constant does not match declared type") |
|
256 fun check_def (s, Defnode (ty', _)) = |
|
257 (if can_be_unified_r ty ty' then |
|
258 raise (CLASH (mainref, axname, s)) |
|
259 else if s = axname then |
|
260 def_err "name of axiom is already used for another definition of this constant" |
|
261 else false) |
|
262 val _ = Symtab.exists check_def defs |
|
263 fun check_final finalty = |
|
264 (if can_be_unified_r finalty ty then |
|
265 raise (FINAL (mainref, finalty)) |
|
266 else |
|
267 true) |
|
268 val _ = forall check_final finals |
|
269 |
|
270 (* now we know that the only thing that can prevent acceptance of the definition |
|
271 is a cyclic dependency *) |
|
272 |
|
273 fun insert_edges edges (nodename, links) = |
|
274 (if links = [] then |
|
275 edges |
|
276 else |
|
277 let |
|
278 val links = map normalize_edge_idx links |
|
279 in |
|
280 Symtab.update (nodename, |
|
281 case Symtab.lookup edges nodename of |
|
282 NONE => links |
|
283 | SOME links' => merge_edges links' links) edges |
|
284 end) |
|
285 |
|
286 fun make_edges ((bodyn, bodyty), edges) = |
|
287 let |
|
288 val bnode = |
|
289 (case Symtab.lookup graph bodyn of |
|
290 NONE => def_err "body of constant definition references undeclared constant" |
|
291 | SOME x => x) |
|
292 val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode |
|
293 in |
|
294 if closed = Final then edges else |
|
295 case unify_r 0 bodyty general_btyp of |
|
296 NONE => edges |
|
297 | SOME (maxidx, sigma1, sigma2) => |
|
298 if exists (is_instance_r bodyty) bfinals then |
|
299 edges |
|
300 else |
|
301 let |
|
302 fun insert_trans_edges ((step1, edges), (nodename, links)) = |
|
303 let |
|
304 val (maxidx1, alpha1, beta1, defname) = step1 |
|
305 fun connect (maxidx2, alpha2, beta2, history) = |
|
306 case unify_r (Int.max (maxidx1, maxidx2)) beta1 alpha2 of |
|
307 NONE => NONE |
|
308 | SOME (max, sleft, sright) => |
|
309 SOME (max, subst sleft alpha1, subst sright beta2, |
|
310 if !chain_history then |
|
311 ((subst sleft beta1, bodyn, defname):: |
|
312 (subst_history sright history)) |
|
313 else []) |
|
314 val links' = List.mapPartial connect links |
|
315 in |
|
316 (step1, insert_edges edges (nodename, links')) |
|
317 end |
|
318 |
|
319 fun make_edges' ((swallowed, edges), |
|
320 (def_name, Defnode (def_ty, def_edges))) = |
|
321 if swallowed then |
|
322 (swallowed, edges) |
|
323 else |
|
324 (case unify_r 0 bodyty def_ty of |
|
325 NONE => (swallowed, edges) |
|
326 | SOME (maxidx, sigma1, sigma2) => |
|
327 (is_instance_r bodyty def_ty, |
|
328 snd (Symtab.foldl insert_trans_edges |
|
329 (((maxidx, subst sigma1 ty, subst sigma2 def_ty, def_name), |
|
330 edges), def_edges)))) |
|
331 val (swallowed, edges) = Symtab.foldl make_edges' ((false, edges), bdefs) |
|
332 in |
|
333 if swallowed then |
|
334 edges |
|
335 else |
|
336 insert_edges edges |
|
337 (bodyn, [(maxidx, subst sigma1 ty, subst sigma2 general_btyp,[])]) |
|
338 end |
|
339 end |
|
340 |
|
341 val edges = foldl make_edges Symtab.empty body |
|
342 |
|
343 (* We also have to add the backreferences that this new defnode induces. *) |
|
344 fun install_backrefs (graph, (noderef, links)) = |
|
345 if links <> [] then |
|
346 let |
|
347 val (Node (ty, defs, backs, finals, closed)) = getnode graph noderef |
|
348 val _ = if closed = Final then |
|
349 sys_error ("install_backrefs: closed node cannot be updated") |
|
350 else () |
|
351 val defnames = |
|
352 (case Symtab.lookup backs mainref of |
|
353 NONE => Symtab.empty |
|
354 | SOME s => s) |
|
355 val defnames' = Symtab.update_new (axname, ()) defnames |
|
356 val backs' = Symtab.update (mainref, defnames') backs |
|
357 in |
|
358 Symtab.update (noderef, Node (ty, defs, backs', finals, closed)) graph |
|
359 end |
|
360 else |
|
361 graph |
|
362 |
|
363 val graph = Symtab.foldl install_backrefs (graph, edges) |
|
364 |
|
365 val (Node (_, _, backs, _, closed)) = getnode graph mainref |
|
366 val closed = |
|
367 if closed = Final then sys_error "define: closed node" |
|
368 else if closed = Open andalso is_instance_r gty ty then Closed else closed |
|
369 |
|
370 val thisDefnode = Defnode (ty, edges) |
|
371 val graph = Symtab.update (mainref, Node (gty, Symtab.update_new |
|
372 (axname, thisDefnode) defs, backs, finals, closed)) graph |
|
373 |
|
374 (* Now we have to check all backreferences to this node and inform them about |
|
375 the new defnode. In this section we also check for circularity. *) |
|
376 fun update_backrefs ((backs, graph), (noderef, defnames)) = |
|
377 let |
|
378 fun update_defs ((defnames, graph),(defname, _)) = |
|
379 let |
|
380 val (Node (nodety, nodedefs, nodebacks, nodefinals, closed)) = |
|
381 getnode graph noderef |
|
382 val _ = if closed = Final then sys_error "update_defs: closed node" else () |
|
383 val (Defnode (def_ty, defnode_edges)) = |
|
384 the (Symtab.lookup nodedefs defname) |
|
385 val edges = the (Symtab.lookup defnode_edges mainref) |
|
386 val refclosed = ref false |
|
387 |
|
388 (* the type of thisDefnode is ty *) |
|
389 fun update (e as (max, alpha, beta, history), (changed, edges)) = |
|
390 case unify_r max beta ty of |
|
391 NONE => (changed, e::edges) |
|
392 | SOME (max', s_beta, s_ty) => |
|
393 let |
|
394 val alpha' = subst s_beta alpha |
|
395 val ty' = subst s_ty ty |
|
396 val _ = |
|
397 if noderef = mainref andalso defname = axname then |
|
398 (case unify alpha' ty' of |
|
399 NONE => |
|
400 if (is_instance_r ty' alpha') then |
|
401 raise (INFINITE_CHAIN ( |
|
402 (alpha', mainref, axname):: |
|
403 (subst_history s_beta history)@ |
|
404 [(ty', mainref, axname)])) |
|
405 else () |
|
406 | SOME s => |
|
407 raise (CIRCULAR ( |
|
408 (subst s alpha', mainref, axname):: |
|
409 (subst_history s (subst_history s_beta history))@ |
|
410 [(subst s ty', mainref, axname)]))) |
|
411 else () |
|
412 in |
|
413 if is_instance_r beta ty then |
|
414 (true, edges) |
|
415 else |
|
416 (changed, e::edges) |
|
417 end |
|
418 |
|
419 val (changed, edges') = foldl update (false, []) edges |
|
420 val defnames' = if edges' = [] then |
|
421 defnames |
|
422 else |
|
423 Symtab.update (defname, ()) defnames |
|
424 in |
|
425 if changed then |
|
426 let |
|
427 val defnode_edges' = |
|
428 if edges' = [] then |
|
429 Symtab.delete mainref defnode_edges |
|
430 else |
|
431 Symtab.update (mainref, edges') defnode_edges |
|
432 val defnode' = Defnode (def_ty, defnode_edges') |
|
433 val nodedefs' = Symtab.update (defname, defnode') nodedefs |
|
434 val closed = if closed = Closed andalso Symtab.is_empty defnode_edges' |
|
435 andalso no_forwards nodedefs' |
|
436 then Final else closed |
|
437 val graph' = |
|
438 Symtab.update |
|
439 (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph |
|
440 in |
|
441 (defnames', graph') |
|
442 end |
|
443 else |
|
444 (defnames', graph) |
|
445 end |
|
446 |
|
447 val (defnames', graph') = Symtab.foldl update_defs |
|
448 ((Symtab.empty, graph), defnames) |
|
449 in |
|
450 if Symtab.is_empty defnames' then |
|
451 (backs, graph') |
|
452 else |
|
453 let |
|
454 val backs' = Symtab.update_new (noderef, defnames') backs |
|
455 in |
|
456 (backs', graph') |
|
457 end |
|
458 end |
|
459 |
|
460 val (backs, graph) = Symtab.foldl update_backrefs ((Symtab.empty, graph), backs) |
|
461 |
|
462 (* If a Circular exception is thrown then we never reach this point. *) |
|
463 val (Node (gty, defs, _, finals, closed)) = getnode graph mainref |
|
464 val closed = if closed = Closed andalso no_forwards defs then Final else closed |
|
465 val graph = Symtab.update (mainref, Node (gty, defs, backs, finals, closed)) graph |
|
466 val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions |
|
467 in |
|
468 (cost+3, axmap, actions', graph) |
|
469 end handle ex => translate_ex axmap ex |
|
470 |
|
471 fun define'' thy (g as (cost, axmap, actions, graph)) (mainref, ty) orig_axname body = |
|
472 let |
|
473 val ty = checkT thy ty |
|
474 fun checkbody (n, t) = |
|
475 let |
|
476 val (Node (_, _, _,_, closed)) = getnode graph n |
|
477 in |
|
478 case closed of |
|
479 Final => NONE |
|
480 | _ => SOME (n, checkT thy t) |
|
481 end |
|
482 val body = distinct (List.mapPartial checkbody body) |
|
483 val (axmap, axname) = newaxname axmap orig_axname |
|
484 in |
|
485 define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body |
|
486 end |
|
487 |
|
488 fun finalize' (cost, axmap, history, graph) (noderef, ty) = |
|
489 case Symtab.lookup graph noderef of |
|
490 NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") |
|
491 | SOME (Node (nodety, defs, backs, finals, closed)) => |
|
492 let |
|
493 val _ = |
|
494 if (not (is_instance_r ty nodety)) then |
|
495 def_err ("only type instances of the declared constant "^ |
|
496 noderef^" can be finalized") |
|
497 else () |
|
498 val _ = Symtab.exists |
|
499 (fn (def_name, Defnode (def_ty, _)) => |
|
500 if can_be_unified_r ty def_ty then |
|
501 def_err ("cannot finalize constant "^noderef^ |
|
502 "; clash with definition "^def_name) |
|
503 else |
|
504 false) |
|
505 defs |
|
506 |
|
507 fun update_finals [] = SOME [ty] |
|
508 | update_finals (final_ty::finals) = |
|
509 (if is_instance_r ty final_ty then NONE |
|
510 else |
|
511 case update_finals finals of |
|
512 NONE => NONE |
|
513 | (r as SOME finals) => |
|
514 if (is_instance_r final_ty ty) then |
|
515 r |
|
516 else |
|
517 SOME (final_ty :: finals)) |
|
518 in |
|
519 case update_finals finals of |
|
520 NONE => (cost, axmap, history, graph) |
|
521 | SOME finals => |
|
522 let |
|
523 val closed = if closed = Open andalso is_instance_r nodety ty then |
|
524 Closed else |
|
525 closed |
|
526 val graph = Symtab.update (noderef, Node (nodety, defs, backs, finals, closed)) graph |
|
527 |
|
528 fun update_backref ((graph, backs), (backrefname, backdefnames)) = |
|
529 let |
|
530 fun update_backdef ((graph, defnames), (backdefname, _)) = |
|
531 let |
|
532 val (backnode as Node (backty, backdefs, backbacks, |
|
533 backfinals, backclosed)) = |
|
534 getnode graph backrefname |
|
535 val (Defnode (def_ty, all_edges)) = |
|
536 the (get_defnode backnode backdefname) |
|
537 |
|
538 val (defnames', all_edges') = |
|
539 case Symtab.lookup all_edges noderef of |
|
540 NONE => sys_error "finalize: corrupt backref" |
|
541 | SOME edges => |
|
542 let |
|
543 val edges' = List.filter (fn (_, _, beta, _) => |
|
544 not (is_instance_r beta ty)) edges |
|
545 in |
|
546 if edges' = [] then |
|
547 (defnames, Symtab.delete noderef all_edges) |
|
548 else |
|
549 (Symtab.update (backdefname, ()) defnames, |
|
550 Symtab.update (noderef, edges') all_edges) |
|
551 end |
|
552 val defnode' = Defnode (def_ty, all_edges') |
|
553 val backdefs' = Symtab.update (backdefname, defnode') backdefs |
|
554 val backclosed' = if backclosed = Closed andalso |
|
555 Symtab.is_empty all_edges' |
|
556 andalso no_forwards backdefs' |
|
557 then Final else backclosed |
|
558 val backnode' = |
|
559 Node (backty, backdefs', backbacks, backfinals, backclosed') |
|
560 in |
|
561 (Symtab.update (backrefname, backnode') graph, defnames') |
|
562 end |
|
563 |
|
564 val (graph', defnames') = |
|
565 Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) |
|
566 in |
|
567 (graph', if Symtab.is_empty defnames' then backs |
|
568 else Symtab.update (backrefname, defnames') backs) |
|
569 end |
|
570 val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) |
|
571 val Node ( _, defs, _, _, closed) = getnode graph' noderef |
|
572 val closed = if closed = Closed andalso no_forwards defs then Final else closed |
|
573 val graph' = Symtab.update (noderef, Node (nodety, defs, backs', |
|
574 finals, closed)) graph' |
|
575 val history' = (Finalize (noderef, ty)) :: history |
|
576 in |
|
577 (cost+1, axmap, history', graph') |
|
578 end |
|
579 end |
|
580 |
|
581 fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty) |
|
582 |
|
583 fun update_axname ax orig_ax (cost, axmap, history, graph) = |
|
584 (cost, Symtab.update (ax, orig_ax) axmap, history, graph) |
|
585 |
|
586 fun merge' (Declare cty, g) = declare' g cty |
|
587 | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = |
|
588 (case Symtab.lookup graph name of |
|
589 NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body |
|
590 | SOME (Node (_, defs, _, _, _)) => |
|
591 (case Symtab.lookup defs axname of |
|
592 NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body |
|
593 | SOME _ => g)) |
|
594 | merge' (Finalize finals, g) = finalize' g finals |
|
595 |
|
596 fun merge'' (g1 as (cost1, _, actions1, _)) (g2 as (cost2, _, actions2, _)) = |
|
597 if cost1 < cost2 then |
|
598 foldr merge' g2 actions1 |
|
599 else |
|
600 foldr merge' g1 actions2 |
|
601 |
|
602 fun finals (_, _, history, graph) = |
|
603 Symtab.foldl |
|
604 (fn (finals, (name, Node(_, _, _, ftys, _))) => |
|
605 Symtab.update_new (name, ftys) finals) |
|
606 (Symtab.empty, graph) |
|
607 |
|
608 fun overloading_info (_, axmap, _, graph) c = |
|
609 let |
|
610 fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup axmap ax), ty) |
|
611 in |
|
612 case Symtab.lookup graph c of |
|
613 NONE => NONE |
|
614 | SOME (Node (ty, defnodes, _, _, state)) => |
|
615 SOME (ty, map translate (Symtab.dest defnodes), state) |
|
616 end |
|
617 |
35 |
618 |
36 |
619 (* monomorphic consts -- neither parametric nor ad-hoc polymorphism *) |
37 (* specified consts *) |
620 |
38 |
621 fun monomorphicT (Type (_, Ts)) = forall monomorphicT Ts |
39 fun disjoint_types T U = |
622 | monomorphicT _ = false |
40 (Type.raw_unify (T, Logic.incr_tvar (maxidx_of_typ T + 1) U) Vartab.empty; false) |
|
41 handle Type.TUNIFY => true; |
623 |
42 |
624 fun monomorphic (_, _, _, graph) c = |
43 fun check_specified c specified = |
625 (case Symtab.lookup graph c of |
44 specified |> Inttab.forall (fn (i, (a, T)) => |
626 NONE => true |
45 specified |> Inttab.forall (fn (j, (b, U)) => |
627 | SOME (Node (ty, defnodes, _, _, _)) => |
46 i = j orelse disjoint_types T U orelse |
628 Symtab.min_key defnodes = Symtab.max_key defnodes andalso |
47 error ("Type clash in specifications " ^ quote a ^ " and " ^ quote b ^ |
629 monomorphicT ty); |
48 " for constant " ^ quote c))); |
630 |
49 |
631 |
50 |
|
51 (* monomorphic constants *) |
632 |
52 |
633 (** diagnostics **) |
53 val monomorphic = Symtab.defined o #monomorphic o rep_defs; |
634 |
54 |
635 fun pretty_const pp (c, T) = |
55 fun update_monomorphic specified c = |
636 [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
56 let |
637 Pretty.quote (Pretty.typ pp (Type.freeze_type (Term.zero_var_indexesT T)))]; |
57 val specs = the_default Inttab.empty (Symtab.lookup specified c); |
638 |
58 fun is_monoT (Type (_, Ts)) = forall is_monoT Ts |
639 fun pretty_path pp path = fold_rev (fn (T, c, def) => |
59 | is_monoT _ = false; |
640 fn [] => [Pretty.block (pretty_const pp (c, T))] |
60 val is_mono = |
641 | prts => Pretty.block (pretty_const pp (c, T) @ |
61 Inttab.is_empty specs orelse |
642 [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path []; |
62 Inttab.min_key specs = Inttab.max_key specs andalso |
643 |
63 is_monoT (snd (the (Inttab.lookup specs (the (Inttab.min_key specs))))); |
644 fun defs_circular pp path = |
64 in if is_mono then Symtab.update (c, ()) else Symtab.remove (K true) (c, ()) end; |
645 Pretty.str "Cyclic dependency of definitions: " :: pretty_path pp path |
|
646 |> Pretty.chunks |> Pretty.string_of; |
|
647 |
|
648 fun defs_infinite_chain pp path = |
|
649 Pretty.str "Infinite chain of definitions: " :: pretty_path pp path |
|
650 |> Pretty.chunks |> Pretty.string_of; |
|
651 |
|
652 fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2; |
|
653 |
|
654 fun defs_final pp const = |
|
655 (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const) |
|
656 |> Pretty.block |> Pretty.string_of; |
|
657 |
65 |
658 |
66 |
659 (* external interfaces *) |
67 (* define consts *) |
660 |
68 |
661 fun declare thy const defs = |
69 fun err_cyclic cycles = |
662 if_none (try (declare'' thy defs) const) defs; |
70 error ("Cyclic dependency of constants:\n" ^ |
|
71 cat_lines (map (space_implode " -> " o map quote o rev) cycles)); |
663 |
72 |
664 fun define thy const name rhs defs = |
73 fun define const_type name lhs rhs = map_defs (fn (consts, specified, monomorphic) => |
665 define'' thy defs const name rhs |
74 let |
666 handle DEFS msg => sys_error msg |
75 fun declare (a, _) = Graph.default_node (a, const_type a); |
667 | CIRCULAR path => error (defs_circular (Sign.pp thy) path) |
76 fun add_deps (a, bs) G = Graph.add_deps_acyclic (a, bs) G |
668 | INFINITE_CHAIN path => error (defs_infinite_chain (Sign.pp thy) path) |
77 handle Graph.CYCLES cycles => err_cyclic cycles; |
669 | CLASH (_, def1, def2) => error (defs_clash def1 def2) |
|
670 | FINAL const => error (defs_final (Sign.pp thy) const); |
|
671 |
78 |
672 fun finalize thy const defs = |
79 val (c, T) = lhs; |
673 finalize'' thy defs const handle DEFS msg => sys_error msg; |
80 val no_overloading = Type.raw_instance (const_type c, T); |
674 |
81 |
675 fun merge pp defs1 defs2 = |
82 val consts' = |
676 merge'' defs1 defs2 |
83 consts |> declare lhs |> fold declare rhs |
677 handle CIRCULAR namess => error (defs_circular pp namess) |
84 |> K no_overloading ? add_deps (c, map #1 rhs); |
678 | INFINITE_CHAIN namess => error (defs_infinite_chain pp namess); |
85 val specified' = |
|
86 specified |> Symtab.default (c, Inttab.empty) |
|
87 |> Symtab.map_entry c (Inttab.update (serial (), (name, T)) #> tap (check_specified c)); |
|
88 val monomorphic' = monomorphic |> update_monomorphic specified' c; |
|
89 in (consts', specified', monomorphic') end); |
|
90 |
|
91 |
|
92 (* empty and merge *) |
|
93 |
|
94 val empty = make_defs (Graph.empty, Symtab.empty, Symtab.empty); |
|
95 |
|
96 fun merge pp |
|
97 (Defs {consts = consts1, specified = specified1, monomorphic}, |
|
98 Defs {consts = consts2, specified = specified2, ...}) = |
|
99 let |
|
100 val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true) |
|
101 handle Graph.CYCLES cycles => err_cyclic cycles; |
|
102 val specified' = (specified1, specified2) |
|
103 |> Symtab.join (fn c => Inttab.merge (K true) #> tap (check_specified c) #> SOME); |
|
104 val monomorphic' = monomorphic |
|
105 |> Symtab.fold (update_monomorphic specified' o #1) specified'; |
|
106 in make_defs (consts', specified', monomorphic') end; |
679 |
107 |
680 end; |
108 end; |
681 |
|
682 (* |
|
683 |
|
684 fun tvar name = TVar ((name, 0), []) |
|
685 |
|
686 val bool = Type ("bool", []) |
|
687 val int = Type ("int", []) |
|
688 val lam = Type("lam", []) |
|
689 val alpha = tvar "'a" |
|
690 val beta = tvar "'b" |
|
691 val gamma = tvar "'c" |
|
692 fun pair a b = Type ("pair", [a,b]) |
|
693 fun prm a = Type ("prm", [a]) |
|
694 val name = Type ("name", []) |
|
695 |
|
696 val _ = print "make empty" |
|
697 val g = Defs.empty |
|
698 |
|
699 val _ = print "declare perm" |
|
700 val g = Defs.declare g ("perm", prm alpha --> beta --> beta) |
|
701 |
|
702 val _ = print "declare permF" |
|
703 val g = Defs.declare g ("permF", prm alpha --> lam --> lam) |
|
704 |
|
705 val _ = print "define perm (1)" |
|
706 val g = Defs.define g ("perm", prm alpha --> (beta --> gamma) --> (beta --> gamma)) "perm_fun" |
|
707 [("perm", prm alpha --> gamma --> gamma), ("perm", prm alpha --> beta --> beta)] |
|
708 |
|
709 val _ = print "define permF (1)" |
|
710 val g = Defs.define g ("permF", prm alpha --> lam --> lam) "permF_app" |
|
711 ([("perm", prm alpha --> lam --> lam), |
|
712 ("perm", prm alpha --> lam --> lam), |
|
713 ("perm", prm alpha --> lam --> lam), |
|
714 ("perm", prm alpha --> name --> name)]) |
|
715 |
|
716 val _ = print "define perm (2)" |
|
717 val g = Defs.define g ("perm", prm alpha --> lam --> lam) "perm_lam" |
|
718 [("permF", (prm alpha --> lam --> lam))] |
|
719 |
|
720 *) |
|