--- a/src/Pure/Isar/locale.ML Mon Sep 24 23:27:01 2018 +0200
+++ b/src/Pure/Isar/locale.ML Mon Sep 24 23:49:43 2018 +0200
@@ -75,24 +75,26 @@
val intro_locales_tac: {strict: bool, eager: bool} -> Proof.context -> thm list -> tactic
(* Registrations and dependencies *)
- type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
+ type registration = {inst: string * morphism, mixin: (morphism * bool) option, export: morphism}
val amend_registration: registration -> Context.generic -> Context.generic
val add_registration: registration -> Context.generic -> Context.generic
val add_registration_theory: registration -> theory -> theory
val add_registration_proof: registration -> Proof.context -> Proof.context
val add_registration_local_theory: registration -> local_theory -> local_theory
- val activate_fragment: registration -> local_theory -> local_theory
val registrations_of: Context.generic -> string -> (string * morphism) list
val add_dependency: string -> registration -> theory -> theory
(* Diagnostic *)
val get_locales: theory -> string list
- val print_locales: bool -> theory -> unit
- val print_locale: theory -> bool -> xstring * Position.T -> unit
- val print_registrations: Proof.context -> xstring * Position.T -> unit
- val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
- val pretty_locale: theory -> bool -> string -> Pretty.T list
+ val pretty_locales: theory -> bool -> Pretty.T
+ val pretty_locale: theory -> bool -> string -> Pretty.T
+ val pretty_registrations: Proof.context -> string -> Pretty.T
+ val pretty_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> Pretty.T
val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
+ type locale_dependency =
+ {source: string, target: string, prefix: (string * bool) list, morphism: morphism,
+ pos: Position.T, serial: serial}
+ val dest_dependencies: theory list -> theory -> locale_dependency list
end;
structure Locale: LOCALE =
@@ -103,23 +105,30 @@
(*** Locales ***)
-type mixins = (((morphism * bool) * serial) list) Inttab.table;
- (* table of mixin lists, per list mixins in reverse order of declaration;
- lists indexed by registration/dependency serial,
- entries for empty lists may be omitted *)
+type dep = {name: string, morphisms: morphism * morphism, pos: Position.T, serial: serial};
+fun eq_dep (dep1: dep, dep2: dep) = #serial dep1 = #serial dep2;
+
+fun make_dep (name, morphisms) : dep =
+ {name = name, morphisms = morphisms, pos = Position.thread_data (), serial = serial ()};
-fun lookup_mixins serial' mixins = Inttab.lookup_list mixins serial';
-
-fun merge_mixins mixs : mixins = Inttab.merge_list (eq_snd op =) mixs;
+(*table of mixin lists, per list mixins in reverse order of declaration;
+ lists indexed by registration/dependency serial,
+ entries for empty lists may be omitted*)
+type mixin = (morphism * bool) * serial;
+type mixins = mixin list Inttab.table;
-fun insert_mixin serial' mixin = Inttab.cons_list (serial', (mixin, serial ()));
+fun lookup_mixins (mixins: mixins) serial' = Inttab.lookup_list mixins serial';
+
+val merge_mixins: mixins * mixins -> mixins = Inttab.merge_list (eq_snd op =);
+
+fun insert_mixin serial' mixin : mixins -> mixins = Inttab.cons_list (serial', (mixin, serial ()));
-fun rename_mixin (old, new) mix =
- (case Inttab.lookup mix old of
- NONE => mix
- | SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs));
+fun rename_mixin (old, new) (mixins: mixins) =
+ (case Inttab.lookup mixins old of
+ NONE => mixins
+ | SOME mixin => Inttab.delete old mixins |> Inttab.update_new (new, mixin));
-fun compose_mixins mixins =
+fun compose_mixins (mixins: mixin list) =
fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
datatype locale = Loc of {
@@ -141,7 +150,7 @@
(*theorem declarations*)
notes: ((string * Attrib.fact list) * serial) list,
(*locale dependencies (sublocale relation) in reverse order*)
- dependencies: ((string * (morphism * morphism)) * serial) list,
+ dependencies: dep list,
(*mixin part of dependencies*)
mixins: mixins
};
@@ -164,7 +173,7 @@
((parameters, spec, intros, axioms, hyp_spec),
((merge (eq_snd op =) (syntax_decls, syntax_decls'),
merge (eq_snd op =) (notes, notes')),
- (merge (eq_snd op =) (dependencies, dependencies'),
+ (merge eq_dep (dependencies, dependencies'),
(merge_mixins (mixins, mixins')))));
structure Locales = Theory_Data
@@ -195,13 +204,14 @@
SOME (Loc loc) => loc
| NONE => error ("Unknown locale " ^ quote name));
-fun register_locale binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy =
+fun register_locale
+ binding parameters spec intros axioms hyp_spec syntax_decls notes dependencies thy =
thy |> Locales.map (Name_Space.define (Context.Theory thy) true
(binding,
mk_locale ((parameters, spec, (apply2 o Option.map) Thm.trim_context intros,
map Thm.trim_context axioms, hyp_spec),
((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
- (map (fn d => (d |> apsnd (rpair Morphism.identity), serial ())) dependencies,
+ (map (fn (name, morph) => make_dep (name, (morph, Morphism.identity))) dependencies,
Inttab.empty)))) #> snd);
(* FIXME Morphism.identity *)
@@ -227,20 +237,13 @@
fun dependencies_of thy = #dependencies o the_locale thy;
-fun mixins_of thy name serial = the_locale thy name |>
- #mixins |> lookup_mixins serial;
+fun mixins_of thy name serial = lookup_mixins (#mixins (the_locale thy name)) serial;
-(* FIXME unused!? *)
-fun identity_on thy name morph =
- let val mk_instance = instance_of thy name
- in ListPair.all Term.aconv_untyped (mk_instance Morphism.identity, mk_instance morph) end;
(* Print instance and qualifiers *)
-fun pretty_reg ctxt export (name, morph) =
+fun pretty_reg_inst ctxt qs (name, ts) =
let
- val thy = Proof_Context.theory_of ctxt;
- val morph' = morph $> export;
fun print_qual (qual, mandatory) = qual ^ (if mandatory then "" else "?");
fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs));
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
@@ -251,15 +254,20 @@
else prt_term t;
fun prt_inst ts =
Pretty.block (Pretty.breaks (pretty_name ctxt name :: map prt_term' ts));
-
- val qs = Binding.name "x" |> Morphism.binding morph' |> Binding.prefix_of;
- val ts = instance_of thy name morph';
in
(case qs of
[] => prt_inst ts
| qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
end;
+fun pretty_reg ctxt export (name, morph) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val morph' = morph $> export;
+ val qs = Morphism.binding_prefix morph';
+ val ts = instance_of thy name morph';
+ in pretty_reg_inst ctxt qs (name, ts) end;
+
(*** Identifiers: activated locales in theory or proof context ***)
@@ -297,17 +305,15 @@
if redundant_ident thy marked (name, instance) then (deps, marked)
else
let
- (* no inheritance of mixins, regardless of requests by clients *)
- val dependencies = dependencies_of thy name |>
- map (fn ((name', (morph', export')), serial') =>
- (name', morph' $> export' $> compose_mixins (mixins_of thy name serial')));
+ (*no inheritance of mixins, regardless of requests by clients*)
+ val dependencies =
+ dependencies_of thy name |> map (fn dep as {morphisms = (morph', export'), ...} =>
+ (#name dep, morph' $> export' $> compose_mixins (mixins_of thy name (#serial dep))));
val marked' = insert_idents (name, instance) marked;
val (deps', marked'') =
fold_rev (add thy (depth + 1) (morph $> stem) export) dependencies
([], marked');
- in
- ((name, morph $> stem) :: deps' @ deps, marked'')
- end
+ in ((name, morph $> stem) :: deps' @ deps, marked'') end
end;
in
@@ -334,52 +340,80 @@
(*** Registrations: interpretations in theories or proof contexts ***)
val total_ident_ord = prod_ord fast_string_ord (list_ord Term_Ord.fast_term_ord);
-
structure Idtab = Table(type key = string * term list val ord = total_ident_ord);
-structure Registrations = Generic_Data
+type reg = {morphisms: morphism * morphism, pos: Position.T, serial: serial};
+type regs = reg Idtab.table;
+
+val join_regs : regs * regs -> regs =
+ Idtab.join (fn id => fn (reg1, reg2) =>
+ if #serial reg1 = #serial reg2 then raise Idtab.SAME else raise Idtab.DUP id);
+
+(* FIXME consolidate with locale dependencies, consider one data slot only *)
+structure Global_Registrations = Theory_Data'
(
- type T = ((morphism * morphism) * serial) Idtab.table * mixins;
- (* registrations, indexed by locale name and instance;
- unique registration serial points to mixin list *)
- val empty = (Idtab.empty, Inttab.empty);
+ (*registrations, indexed by locale name and instance;
+ unique registration serial points to mixin list*)
+ type T = regs * mixins;
+ val empty: T = (Idtab.empty, Inttab.empty);
val extend = I;
- fun merge ((reg1, mix1), (reg2, mix2)) : T =
- (Idtab.join (fn id => fn ((_, s1), (_, s2)) =>
- if s1 = s2 then raise Idtab.SAME else raise Idtab.DUP id) (reg1, reg2),
- merge_mixins (mix1, mix2))
- handle Idtab.DUP id =>
- (* distinct interpretations with same base: merge their mixins *)
- let
- val (_, s1) = Idtab.lookup reg1 id |> the;
- val (morph2, s2) = Idtab.lookup reg2 id |> the;
- val reg2' = Idtab.update (id, (morph2, s1)) reg2;
- val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
- (* FIXME print interpretations,
- which is not straightforward without theory context *)
- in merge ((reg1, mix1), (reg2', rename_mixin (s2, s1) mix2)) end;
- (* FIXME consolidate with dependencies, consider one data slot only *)
+ fun merge old_thys =
+ let
+ fun recursive_merge ((regs1, mixins1), (regs2, mixins2)) : T =
+ (join_regs (regs1, regs2), merge_mixins (mixins1, mixins2))
+ handle Idtab.DUP id =>
+ (*distinct interpretations with same base: merge their mixins*)
+ let
+ val reg1 = Idtab.lookup regs1 id |> the;
+ val reg2 = Idtab.lookup regs2 id |> the;
+ val reg2' =
+ {morphisms = #morphisms reg2,
+ pos = Position.thread_data (),
+ serial = #serial reg1};
+ val regs2' = Idtab.update (id, reg2') regs2;
+ val mixins2' = rename_mixin (#serial reg2, #serial reg1) mixins2;
+ val _ =
+ warning ("Removed duplicate interpretation after retrieving its mixins" ^
+ Position.here_list [#pos reg1, #pos reg2] ^ ":\n " ^
+ Pretty.string_of (pretty_reg_inst (Syntax.init_pretty_global (#1 old_thys)) [] id));
+ in recursive_merge ((regs1, mixins1), (regs2', mixins2')) end;
+ in recursive_merge end;
);
+structure Local_Registrations = Proof_Data
+(
+ type T = Global_Registrations.T;
+ val init = Global_Registrations.get;
+);
+
+val get_registrations = Context.cases Global_Registrations.get Local_Registrations.get;
+
+fun map_registrations f (Context.Theory thy) = Context.Theory (Global_Registrations.map f thy)
+ | map_registrations f (Context.Proof ctxt) = Context.Proof (Local_Registrations.map f ctxt);
+
(* Primitive operations *)
fun add_reg thy export (name, morph) =
- Registrations.map (apfst (Idtab.insert (K false)
- ((name, instance_of thy name (morph $> export)), ((morph, export), serial ()))));
+ let
+ val reg = {morphisms = (morph, export), pos = Position.thread_data (), serial = serial ()};
+ val id = (name, instance_of thy name (morph $> export));
+ in (map_registrations o apfst) (Idtab.insert (K false) (id, reg)) end;
fun add_mixin serial' mixin =
(* registration to be amended identified by its serial id *)
- Registrations.map (apsnd (insert_mixin serial' mixin));
+ (map_registrations o apsnd) (insert_mixin serial' mixin);
+
+val get_regs = #1 o get_registrations;
fun get_mixins context (name, morph) =
let
val thy = Context.theory_of context;
- val (regs, mixins) = Registrations.get context;
+ val (regs, mixins) = get_registrations context;
in
(case Idtab.lookup regs (name, instance_of thy name morph) of
NONE => []
- | SOME (_, serial) => lookup_mixins serial mixins)
+ | SOME {serial, ...} => lookup_mixins mixins serial)
end;
fun collect_mixins context (name, morph) =
@@ -394,13 +428,6 @@
|> compose_mixins
end;
-fun registrations_of context loc =
- Idtab.fold_rev (fn ((name, _), (reg, _)) => name = loc ? cons (name, reg))
- (#1 (Registrations.get context)) []
- (* with inherited mixins *)
- |> map (fn (name, (base, export)) =>
- (name, base $> (collect_mixins context (name, base $> export)) $> export));
-
(*** Activate context elements of locale ***)
@@ -521,12 +548,12 @@
type registration = Locale.registration;
fun amend_registration {mixin = NONE, ...} context = context
- | amend_registration {dep = (name, morph), mixin = SOME mixin, export} context =
+ | amend_registration {inst = (name, morph), mixin = SOME mixin, export} context =
let
val thy = Context.theory_of context;
val ctxt = Context.proof_of context;
- val regs = Registrations.get context |> fst;
+ val regs = get_regs context;
val base = instance_of thy name (morph $> export);
val serial' =
(case Idtab.lookup regs (name, base) of
@@ -535,7 +562,7 @@
" with\nparameter instantiation " ^
space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
" available")
- | SOME (_, serial') => serial');
+ | SOME {serial = serial', ...} => serial');
in
add_mixin serial' mixin context
end;
@@ -543,7 +570,7 @@
(* Note that a registration that would be subsumed by an existing one will not be
generated, and it will not be possible to amend it. *)
-fun add_registration {dep = (name, base_morph), mixin, export} context =
+fun add_registration {inst = (name, base_morph), mixin, export} context =
let
val thy = Context.theory_of context;
val pos_morph = Morphism.binding_morphism "position" (Binding.set_pos (Position.thread_data ()));
@@ -557,7 +584,7 @@
(* add new registrations with inherited mixins *)
|> roundup thy (add_reg thy export) export (name, mix_morph) |> #2
(* add mixin *)
- |> amend_registration {dep = (name, mix_morph), mixin = mixin, export = export}
+ |> amend_registration {inst = (name, mix_morph), mixin = mixin, export = export}
(* activate import hierarchy as far as not already active *)
|> activate_facts (SOME export) (name, mix_morph $> pos_morph)
end;
@@ -576,44 +603,30 @@
end;
-(* locale fragments within local theory *)
-
-fun activate_fragment registration =
- Local_Theory.mark_brittle #> add_registration_local_theory registration;
-
-
(*** Dependencies ***)
-(* FIXME dead code!?
-fun amend_dependency loc (name, morph) mixin export thy =
+fun registrations_of context loc =
+ Idtab.fold_rev (fn ((name, _), {morphisms, ...}) =>
+ name = loc ? cons (name, morphisms)) (get_regs context) []
+ (*with inherited mixins*)
+ |> map (fn (name, (base, export)) =>
+ (name, base $> (collect_mixins context (name, base $> export)) $> export));
+
+fun add_dependency loc {inst = (name, morph), mixin, export} thy =
let
- val deps = dependencies_of thy loc;
- in
- case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) =>
- total_ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of
- NONE => error ("Locale " ^
- quote (extern thy name) ^ " with\parameter instantiation " ^
- space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^
- " not a sublocale of " ^ quote (extern thy loc))
- | SOME (_, serial') => change_locale ...
- end;
-*)
-
-fun add_dependency loc {dep = (name, morph), mixin, export} thy =
- let
- val serial' = serial ();
- val thy' = thy |>
- (change_locale loc o apsnd)
- (apfst (cons ((name, (morph, export)), serial')) #>
- apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin));
+ val dep = make_dep (name, (morph, export));
+ val add_dep =
+ apfst (cons dep) #>
+ apsnd (case mixin of NONE => I | SOME mixin => insert_mixin (#serial dep) mixin);
+ val thy' = change_locale loc (apsnd add_dep) thy;
val context' = Context.Theory thy';
val (_, regs) =
fold_rev (roundup thy' cons export)
(registrations_of context' loc) (Idents.get context', []);
in
- thy'
- |> fold_rev (fn dep => add_registration_theory {dep = dep, mixin = NONE, export = export}) regs
+ fold_rev (fn inst => add_registration_theory {inst = inst, mixin = NONE, export = export})
+ regs thy'
end;
@@ -698,13 +711,12 @@
fun get_locales thy = map #1 (Name_Space.dest_table (Locales.get thy));
-fun print_locales verbose thy =
+fun pretty_locales thy verbose =
Pretty.block
(Pretty.breaks
(Pretty.str "locales:" ::
map (Pretty.mark_str o #1)
- (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy))))
- |> Pretty.writeln;
+ (Name_Space.markup_table verbose (Proof_Context.init_global thy) (Locales.get thy))));
fun pretty_locale thy show_facts name =
let
@@ -718,24 +730,16 @@
|> tap consolidate_notes
|> map force_notes;
in
- Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
- maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems
+ Pretty.block (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
+ maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems)
end;
-fun print_locale thy show_facts raw_name =
- Pretty.writeln (Pretty.block (pretty_locale thy show_facts (check thy raw_name)));
+fun pretty_registrations ctxt name =
+ (case registrations_of (Context.Proof ctxt) name of
+ [] => Pretty.str "no interpretations"
+ | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs)));
-fun print_registrations ctxt raw_name =
- let
- val thy = Proof_Context.theory_of ctxt;
- val name = check thy raw_name;
- in
- (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
- [] => Pretty.str "no interpretations"
- | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt Morphism.identity) (rev regs)))
- end |> Pretty.writeln;
-
-fun print_dependencies ctxt clean export insts =
+fun pretty_dependencies ctxt clean export insts =
let
val thy = Proof_Context.theory_of ctxt;
val idents = if clean then empty_idents else Idents.get (Context.Proof ctxt);
@@ -743,15 +747,43 @@
(case fold (roundup thy cons export) insts (idents, []) |> snd of
[] => Pretty.str "no dependencies"
| deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt export) (rev deps)))
- end |> Pretty.writeln;
+ end;
fun pretty_locale_deps thy =
let
fun make_node name =
{name = name,
- parents = map (fst o fst) (dependencies_of thy name),
- body = Pretty.block (pretty_locale thy false name)};
+ parents = map #name (dependencies_of thy name),
+ body = pretty_locale thy false name};
val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []);
in map make_node names end;
+type locale_dependency =
+ {source: string, target: string, prefix: (string * bool) list, morphism: morphism,
+ pos: Position.T, serial: serial};
+
+fun dest_dependencies prev_thys thy =
+ let
+ fun remove_prev loc prev_thy deps =
+ (case get_locale prev_thy loc of
+ NONE => deps
+ | SOME (Loc {dependencies = prev_deps, ...}) =>
+ if eq_list eq_dep (prev_deps, deps) then []
+ else subtract eq_dep prev_deps deps);
+ fun result loc (dep: dep) =
+ let val morphism = op $> (#morphisms dep) in
+ {source = #name dep,
+ target = loc,
+ prefix = Morphism.binding_prefix morphism,
+ morphism = morphism,
+ pos = #pos dep,
+ serial = #serial dep}
+ end;
+ fun add (loc, Loc {dependencies = deps, ...}) =
+ fold (cons o result loc) (fold (remove_prev loc) prev_thys deps);
+ in
+ Name_Space.fold_table add (Locales.get thy) []
+ |> sort (int_ord o apply2 #serial)
+ end;
+
end;