Diagnostic command to show locale dependencies.
1 (* Title: Pure/Isar/locale.ML
2 Author: Clemens Ballarin, TU Muenchen
4 Locales -- managed Isar proof contexts, based on Pure predicates.
6 Draws basic ideas from Florian Kammueller's original version of
7 locales, but uses the richer infrastructure of Isar instead of the raw
8 meta-logic. Furthermore, structured import of contexts (with merge
9 and rename operations) are provided, as well as type-inference of the
10 signature parts, and predicate definitions of the specification text.
12 Interpretation enables the reuse of theorems of locales in other
13 contexts, namely those defined by theories, structured proofs and
18 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
19 In Stefano Berardi et al., Types for Proofs and Programs: International
20 Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
21 [2] Clemens Ballarin. Interpretation of Locales in Isabelle: Managing
22 Dependencies between Locales. Technical Report TUM-I0607, Technische
23 Universitaet Muenchen, 2006.
24 [3] Clemens Ballarin. Interpretation of Locales in Isabelle: Theories and
25 Proof Contexts. In J.M. Borwein and W.M. Farmer, MKM 2006, LNAI 4108,
31 (* Locale specification *)
32 val register_locale: binding ->
33 (string * sort) list * ((string * typ) * mixfix) list ->
34 term option * term list ->
35 thm option * thm option -> thm list ->
37 (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list ->
38 (string * morphism) list -> theory -> theory
39 val intern: theory -> xstring -> string
40 val extern: theory -> string -> xstring
41 val defined: theory -> string -> bool
42 val params_of: theory -> string -> ((string * typ) * mixfix) list
43 val intros_of: theory -> string -> thm option * thm option
44 val axioms_of: theory -> string -> thm list
45 val instance_of: theory -> string -> morphism -> term list
46 val specification_of: theory -> string -> term option * term list
49 val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
50 Proof.context -> Proof.context
51 val add_declaration: string -> declaration -> Proof.context -> Proof.context
52 val add_syntax_declaration: string -> declaration -> Proof.context -> Proof.context
55 val activate_declarations: string * morphism -> Proof.context -> Proof.context
56 val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
57 val init: string -> theory -> Proof.context
59 (* Reasoning about locales *)
60 val get_witnesses: Proof.context -> thm list
61 val get_intros: Proof.context -> thm list
62 val get_unfolds: Proof.context -> thm list
63 val witness_add: attribute
64 val intro_add: attribute
65 val unfold_add: attribute
66 val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
68 (* Registrations and dependencies *)
69 val add_registration: string * morphism -> (morphism * bool) option ->
70 morphism -> Context.generic -> Context.generic
71 val amend_registration: string * morphism -> morphism * bool ->
72 morphism -> Context.generic -> Context.generic
73 val registrations_of: Context.generic -> string -> (string * morphism) list
74 val add_dependency: string -> string * morphism -> (morphism * bool) option ->
75 morphism -> theory -> theory
78 val all_locales: theory -> string list
79 val print_locales: theory -> unit
80 val print_locale: theory -> bool -> xstring -> unit
81 val print_registrations: Proof.context -> string -> unit
82 val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
83 val locale_deps: theory ->
84 {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
85 * term list list Symtab.table Symtab.table
88 structure Locale: LOCALE =
91 datatype ctxt = datatype Element.ctxt;
96 type mixins = (((morphism * bool) * serial) list) Inttab.table;
97 (* table of mixin lists, per list mixins in reverse order of declaration;
98 lists indexed by registration/dependency serial,
99 entries for empty lists may be omitted *)
101 fun lookup_mixins serial' mixins = the_default [] (Inttab.lookup mixins serial');
103 fun merge_mixins (mix1, mix2) = Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2);
105 fun insert_mixin serial' mixin =
106 Inttab.map_default (serial', []) (cons (mixin, serial ()));
108 fun rename_mixin (old, new) mix =
109 case Inttab.lookup mix old of
111 SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs);
113 fun compose_mixins mixins =
114 fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
116 datatype locale = Loc of {
118 parameters: (string * sort) list * ((string * typ) * mixfix) list,
119 (* type and term parameters *)
120 spec: term option * term list,
121 (* assumptions (as a single predicate expression) and defines *)
122 intros: thm option * thm option,
125 syntax_decls: (declaration * serial) list,
126 (* syntax declarations *)
127 notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
128 (* theorem declarations *)
129 dependencies: ((string * (morphism * morphism)) * serial) list
130 (* locale dependencies (sublocale relation) in reverse order *),
132 (* mixin part of dependencies *)
135 fun mk_locale ((parameters, spec, intros, axioms),
136 ((syntax_decls, notes), (dependencies, mixins))) =
137 Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
138 syntax_decls = syntax_decls, notes = notes, dependencies = dependencies, mixins = mixins};
140 fun map_locale f (Loc {parameters, spec, intros, axioms,
141 syntax_decls, notes, dependencies, mixins}) =
142 mk_locale (f ((parameters, spec, intros, axioms),
143 ((syntax_decls, notes), (dependencies, mixins))));
146 (Loc {parameters, spec, intros, axioms, syntax_decls, notes, dependencies, mixins},
147 Loc {syntax_decls = syntax_decls', notes = notes',
148 dependencies = dependencies', mixins = mixins', ...}) =
150 ((parameters, spec, intros, axioms),
151 ((merge (eq_snd op =) (syntax_decls, syntax_decls'),
152 merge (eq_snd op =) (notes, notes')),
153 (merge (eq_snd op =) (dependencies, dependencies'),
154 (merge_mixins (mixins, mixins')))));
156 structure Locales = Theory_Data
158 type T = locale Name_Space.table;
159 val empty : T = Name_Space.empty_table "locale";
161 val merge = Name_Space.join_tables (K merge_locale);
164 val intern = Name_Space.intern o #1 o Locales.get;
165 val extern = Name_Space.extern o #1 o Locales.get;
167 val get_locale = Symtab.lookup o #2 o Locales.get;
168 val defined = Symtab.defined o #2 o Locales.get;
170 fun the_locale thy name =
171 (case get_locale thy name of
172 SOME (Loc loc) => loc
173 | NONE => error ("Unknown locale " ^ quote name));
175 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
176 thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
178 mk_locale ((parameters, spec, intros, axioms),
179 ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
180 (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies,
181 Inttab.empty)))) #> snd);
182 (* FIXME Morphism.identity *)
184 fun change_locale name =
185 Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
188 (** Primitive operations **)
190 fun params_of thy = snd o #parameters o the_locale thy;
192 fun intros_of thy = #intros o the_locale thy;
194 fun axioms_of thy = #axioms o the_locale thy;
196 fun instance_of thy name morph = params_of thy name |>
197 map (Morphism.term morph o Free o #1);
199 fun specification_of thy = #spec o the_locale thy;
201 fun dependencies_of thy name = the_locale thy name |>
204 fun mixins_of thy name serial = the_locale thy name |>
205 #mixins |> lookup_mixins serial;
208 fun identity_on thy name morph =
209 let val mk_instance = instance_of thy name
211 forall2 (curry Term.aconv_untyped) (mk_instance Morphism.identity) (mk_instance morph)
214 (* Print instance and qualifiers *)
216 fun pretty_reg ctxt (name, morph) =
218 val thy = ProofContext.theory_of ctxt;
219 val name' = extern thy name;
220 fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
221 fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
222 val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
224 if Config.get ctxt show_types
225 then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
226 Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
229 Pretty.block (Pretty.breaks (Pretty.str name' :: map prt_term' ts));
231 val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
232 val ts = instance_of thy name morph;
236 | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
240 (*** Identifiers: activated locales in theory or proof context ***)
243 fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
244 (* smaller term is more general *)
247 fun ident_ord ((n: string, ts), (m, ss)) =
248 (case fast_string_ord (m, n) of
249 EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
254 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
256 structure Identifiers = Generic_Data
258 type T = (string * term list) list delayed;
259 val empty = Ready [];
264 fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2)
265 | finish _ (Ready ids) = ids;
267 val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy =>
268 (case Identifiers.get (Context.Theory thy) of
270 | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
274 val get_idents = (fn Ready ids => ids) o Identifiers.get;
275 val put_idents = Identifiers.put o Ready;
280 (** Resolve locale dependencies in a depth-first fashion **)
284 val roundup_bound = 120;
286 fun add thy depth stem export (name, morph, mixins) (deps, marked) =
287 if depth > roundup_bound
288 then error "Roundup bound exceeded (sublocale relation probably not terminating)."
291 val instance = instance_of thy name (morph $> stem $> export);
293 if member (ident_le thy) marked (name, instance)
297 val full_morph = morph $> compose_mixins mixins $> stem;
298 (* no inheritance of mixins, regardless of requests by clients *)
299 val dependencies = dependencies_of thy name |>
300 map (fn ((name', (morph', export')), serial') =>
301 (name', morph' $> export', mixins_of thy name serial'));
302 val marked' = (name, instance) :: marked;
303 val (deps', marked'') =
304 fold_rev (add thy (depth + 1) full_morph export) dependencies
307 ((name, full_morph) :: deps' @ deps, marked'')
313 (* Note that while identifiers always have the external (exported) view, activate_dep
314 is presented with the internal view. *)
316 fun roundup thy activate_dep export (name, morph) (marked, input) =
318 (* Find all dependencies including new ones (which are dependencies enriching
319 existing registrations). *)
320 val (dependencies, marked') =
321 add thy 0 Morphism.identity export (name, morph, []) ([], []);
322 (* Filter out fragments from marked; these won't be activated. *)
323 val dependencies' = filter_out (fn (name, morph) =>
324 member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies;
326 (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
332 (*** Registrations: interpretations in theories or proof contexts ***)
334 structure Idtab = Table(type key = string * term list val ord = ident_ord);
336 structure Registrations = Generic_Data
338 type T = ((morphism * morphism) * serial) Idtab.table * mixins;
339 (* registrations, indexed by locale name and instance;
340 unique registration serial points to mixin list *)
341 val empty = (Idtab.empty, Inttab.empty);
343 fun merge ((reg1, mix1), (reg2, mix2)) : T =
344 (Idtab.join (fn id => fn (r1 as (_, s1), r2 as (_, s2)) =>
345 if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
346 merge_mixins (mix1, mix2))
347 handle Idtab.DUP id =>
348 (* distinct interpretations with same base: merge their mixins *)
350 val (_, s1) = Idtab.lookup reg1 id |> the;
351 val (morph2, s2) = Idtab.lookup reg2 id |> the;
352 val reg2' = Idtab.update (id, (morph2, s1)) reg2;
353 val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
354 (* FIXME print interpretations,
355 which is not straightforward without theory context *)
356 in merge ((reg1, mix1), (reg2', rename_mixin (s2, s1) mix2)) end;
357 (* FIXME consolidate with dependencies, consider one data slot only *)
361 (* Primitive operations *)
363 fun add_reg thy export (name, morph) =
364 Registrations.map (apfst (Idtab.insert (K false)
365 ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
367 fun add_mixin serial' mixin =
368 (* registration to be amended identified by its serial id *)
369 Registrations.map (apsnd (insert_mixin serial' mixin));
371 fun get_mixins context (name, morph) =
373 val thy = Context.theory_of context;
374 val (regs, mixins) = Registrations.get context;
376 (case Idtab.lookup regs (name, instance_of thy name morph) of
378 | SOME (_, serial) => lookup_mixins serial mixins)
381 fun collect_mixins context (name, morph) =
383 val thy = Context.theory_of context;
385 roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
386 Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
387 |> snd |> filter (snd o fst) (* only inheritable mixins *)
388 |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
392 fun get_registrations context select = Registrations.get context
393 |>> Idtab.dest |>> select
394 (* with inherited mixins *)
395 |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
396 (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
398 fun registrations_of context name =
399 get_registrations context (filter (curry (op =) name o fst o fst));
401 fun all_registrations context = get_registrations context I;
404 (*** Activate context elements of locale ***)
406 (* Declarations, facts and entire locale content *)
408 fun activate_syntax_decls (name, morph) context =
410 val thy = Context.theory_of context;
411 val {syntax_decls, ...} = the_locale thy name;
414 |> fold_rev (fn (decl, _) => decl morph) syntax_decls
417 fun activate_notes activ_elem transfer context export' (name, morph) input =
419 val thy = Context.theory_of context;
420 val {notes, ...} = the_locale thy name;
421 fun activate ((kind, facts), _) input =
425 NONE => Morphism.identity
426 | SOME export => collect_mixins context (name, morph $> export) $> export);
428 |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
429 in activ_elem (Notes (kind, facts')) input end;
431 fold_rev activate notes input
434 fun activate_all name thy activ_elem transfer (marked, input) =
436 val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
437 val input' = input |>
439 activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
440 (* FIXME type parameters *)
441 (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
443 activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
444 val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
446 roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
450 (** Public activation functions **)
452 fun activate_declarations dep = Context.proof_map (fn context =>
454 val thy = Context.theory_of context;
456 roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
460 fun activate_facts export dep context =
462 val thy = Context.theory_of context;
463 val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
465 roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
466 dep (get_idents context, context)
471 activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
472 ([], Context.Proof (ProofContext.init_global thy)) |-> put_idents |> Context.proof_of;
475 (*** Add and extend registrations ***)
477 fun amend_registration (name, morph) mixin export context =
479 val thy = Context.theory_of context;
480 val regs = Registrations.get context |> fst;
481 val base = instance_of thy name (morph $> export);
483 (case Idtab.lookup regs (name, base) of
485 error ("No interpretation of locale " ^
486 quote (extern thy name) ^ " with\nparameter instantiation " ^
487 space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
489 | SOME (_, serial') => add_mixin serial' mixin context)
492 (* Note that a registration that would be subsumed by an existing one will not be
493 generated, and it will not be possible to amend it. *)
495 fun add_registration (name, base_morph) mixin export context =
497 val thy = Context.theory_of context;
498 val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
499 val morph = base_morph $> mix;
500 val inst = instance_of thy name morph;
502 if member (ident_le thy) (get_idents context) (name, inst)
503 then context (* FIXME amend mixins? *)
505 (get_idents context, context)
506 (* add new registrations with inherited mixins *)
507 |> roundup thy (add_reg thy export) export (name, morph)
513 | SOME mixin => amend_registration (name, morph) mixin export)
514 (* activate import hierarchy as far as not already active *)
515 |> activate_facts (SOME export) (name, morph)
519 (*** Dependencies ***)
522 fun amend_dependency loc (name, morph) mixin export thy =
524 val deps = dependencies_of thy loc;
526 case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) =>
527 ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
528 NONE => error ("Locale " ^
529 quote (extern thy name) ^ " with\parameter instantiation " ^
530 space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^
531 " not a sublocale of " ^ quote (extern thy loc))
532 | SOME (_, serial') => change_locale ...
536 fun add_dependency loc (name, morph) mixin export thy =
538 val serial' = serial ();
540 (change_locale loc o apsnd)
541 (apfst (cons ((name, (morph, export)), serial')) #>
542 apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
543 val context' = Context.Theory thy';
544 val (_, regs) = fold_rev (roundup thy' cons export)
545 (registrations_of context' loc) (get_idents (context'), []);
548 |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
552 (*** Storing results ***)
556 fun add_thmss loc kind args ctxt =
558 val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
559 val ctxt'' = ctxt' |> ProofContext.background_theory
560 ((change_locale loc o apfst o apsnd) (cons (args', serial ()))
563 (fn thy => fold_rev (fn (_, morph) =>
565 val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
566 Attrib.map_facts (Attrib.attribute_i thy)
567 in Global_Theory.note_thmss kind args'' #> snd end)
568 (registrations_of (Context.Theory thy) loc) thy))
574 fun add_declaration loc decl =
576 [((Binding.conceal Binding.empty,
577 [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
578 [([Drule.dummy_thm], [])])];
580 fun add_syntax_declaration loc decl =
581 ProofContext.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
582 #> add_declaration loc decl;
585 (*** Reasoning about locales ***)
587 (* Storage for witnesses, intro and unfold rules *)
589 structure Thms = Generic_Data
591 type T = thm list * thm list * thm list;
592 val empty = ([], [], []);
594 fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
595 (Thm.merge_thms (witnesses1, witnesses2),
596 Thm.merge_thms (intros1, intros2),
597 Thm.merge_thms (unfolds1, unfolds2));
600 val get_witnesses = #1 o Thms.get o Context.Proof;
601 val get_intros = #2 o Thms.get o Context.Proof;
602 val get_unfolds = #3 o Thms.get o Context.Proof;
605 Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (Thm.add_thm th x, y, z)));
607 Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, Thm.add_thm th y, z)));
609 Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
614 fun gen_intro_locales_tac intros_tac eager ctxt =
616 (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
618 val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
619 val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
621 val _ = Context.>> (Context.map_theory
622 (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
623 "back-chain introduction rules of locales without unfolding predicates" #>
624 Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
625 "back-chain all introduction rules of locales"));
628 (*** diagnostic commands and interfaces ***)
630 val all_locales = Symtab.keys o snd o Locales.get;
632 fun print_locales thy =
633 Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
636 fun print_locale thy show_facts raw_name =
638 val name = intern thy raw_name;
639 val ctxt = init name thy;
640 fun cons_elem (elem as Notes _) = show_facts ? cons elem
641 | cons_elem elem = cons elem;
643 activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
646 Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
650 fun print_registrations ctxt raw_name =
652 val thy = ProofContext.theory_of ctxt;
653 val name = intern thy raw_name;
654 val _ = the_locale thy name; (* error if locale unknown *)
656 (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
657 [] => Pretty.str ("no interpretations")
658 | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs)))
659 end |> Pretty.writeln;
661 fun print_dependencies ctxt clean export insts =
663 val thy = ProofContext.theory_of ctxt;
664 val idents = if clean then [] else get_idents (Context.Proof ctxt);
666 (case fold (roundup thy cons export) insts (idents, []) |> snd of
667 [] => Pretty.str ("no dependencies")
668 | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
669 end |> Pretty.writeln;
671 fun locale_deps thy =
673 val names = all_locales thy
674 fun add_locale_node name =
676 val params = params_of thy name;
678 these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
680 map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
682 Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
684 fun add_locale_deps name =
687 (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name |> map fst);
689 fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
690 deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
695 |> fold add_locale_node names
696 |> rpair Symtab.empty
697 |> fold add_locale_deps names