--- a/src/HOL/Tools/inductive.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Mar 12 12:18:41 2014 +0100
@@ -230,7 +230,7 @@
[Pretty.block
(Pretty.breaks
(Pretty.str "(co)inductives:" ::
- map (Pretty.mark_str o #1) (Name_Space.extern_table' ctxt space infos))),
+ map (Pretty.mark_str o #1) (Name_Space.markup_entries ctxt space (Symtab.dest infos)))),
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
end |> Pretty.chunks |> Pretty.writeln;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/change_table.ML Wed Mar 12 12:18:41 2014 +0100
@@ -0,0 +1,146 @@
+(* Title: Pure/General/change_table.ML
+ Author: Makarius
+
+Generic tables with extra bookkeeping of changes relative to some
+common base version, subject to implicit block structure. Support for
+efficient join/merge of big global tables with small local updates.
+*)
+
+signature CHANGE_TABLE =
+sig
+ structure Table: TABLE
+ type key = Table.key
+ exception DUP of key
+ exception SAME
+ type 'a T
+ val table_of: 'a T -> 'a Table.table
+ val empty: 'a T
+ val is_empty: 'a T -> bool
+ val change_base: bool -> 'a T -> 'a T
+ val join: (key -> 'a * 'a -> 'a) (*exception SAME*) -> 'a T * 'a T -> 'a T (*exception DUP*)
+ val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*)
+ val fold: (key * 'b -> 'a -> 'a) -> 'b T -> 'a -> 'a
+ val dest: 'a T -> (key * 'a) list
+ val lookup_key: 'a T -> key -> (key * 'a) option
+ val lookup: 'a T -> key -> 'a option
+ val defined: 'a T -> key -> bool
+ val update: key * 'a -> 'a T -> 'a T
+ val update_new: key * 'a -> 'a T -> 'a T (*exception DUP*)
+ val map_entry: key -> ('a -> 'a) -> 'a T -> 'a T
+ val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T
+ val delete_safe: key -> 'a T -> 'a T
+end;
+
+functor Change_Table(Key: KEY): CHANGE_TABLE =
+struct
+
+structure Table = Table(Key);
+type key = Table.key;
+
+exception SAME = Table.SAME;
+exception DUP = Table.DUP;
+
+
+(* optional change *)
+
+datatype change = Change of {base: serial, depth: int, changes: Table.set};
+
+fun some_change base depth changes =
+ SOME (Change {base = base, depth = depth, changes = changes});
+
+fun base_change true NONE =
+ some_change (serial ()) 0 Table.empty
+ | base_change true (SOME (Change {base, depth, changes})) =
+ some_change base (depth + 1) changes
+ | base_change false (SOME (Change {base, depth, changes})) =
+ if depth = 0 then NONE else some_change base (depth - 1) changes
+ | base_change false NONE = raise Fail "Unbalanced block structure of change table";
+
+fun update_change _ NONE = NONE
+ | update_change key (SOME (Change {base, depth, changes})) =
+ some_change base depth (Table.insert (K true) (key, ()) changes);
+
+fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base";
+
+fun merge_change (NONE, NONE) = NONE
+ | merge_change (SOME (Change change1), SOME (Change change2)) =
+ let
+ val {base = base1, depth = depth1, changes = changes1} = change1;
+ val {base = base2, depth = depth2, changes = changes2} = change2;
+ in
+ if base1 = base1 andalso depth1 = depth2 then
+ SOME ((changes2, some_change base1 depth1 (Table.merge (K true) (changes1, changes2))))
+ else cannot_merge ()
+ end
+ | merge_change _ = cannot_merge ();
+
+
+(* table with changes *)
+
+datatype 'a T = Change_Table of {change: change option, table: 'a Table.table};
+
+fun table_of (Change_Table {table, ...}) = table;
+
+val empty = Change_Table {change = NONE, table = Table.empty};
+fun is_empty (Change_Table {change, table}) = is_none change andalso Table.is_empty table;
+
+fun make_change_table (change, table) = Change_Table {change = change, table = table};
+fun map_change_table f (Change_Table {change, table}) = make_change_table (f (change, table));
+
+fun change_base begin = (map_change_table o apfst) (base_change begin);
+
+
+(* join and merge *)
+
+fun join f (arg1, arg2) =
+ let
+ val Change_Table {change = change1, table = table1} = arg1;
+ val Change_Table {change = change2, table = table2} = arg2;
+ in
+ if pointer_eq (change1, change2) andalso pointer_eq (table1, table2) then arg1
+ else if is_empty arg2 then arg1
+ else if is_empty arg1 then arg2
+ else
+ (case merge_change (change1, change2) of
+ NONE => make_change_table (NONE, Table.join f (table1, table2))
+ | SOME (changes2, change') =>
+ let
+ fun update key table =
+ (case Table.lookup table2 key of
+ NONE => table
+ | SOME y =>
+ (case Table.lookup table key of
+ NONE => Table.update (key, y) table
+ | SOME x =>
+ (case (SOME (f key (x, y)) handle Table.SAME => NONE) of
+ NONE => table
+ | SOME z => Table.update (key, z) table)));
+ val table' = Table.fold (update o #1) changes2 table1;
+ in make_change_table (change', table') end)
+ end;
+
+fun merge eq =
+ join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key);
+
+
+(* derived operations *)
+
+fun fold f arg = Table.fold f (table_of arg);
+fun dest arg = Table.dest (table_of arg);
+fun lookup_key arg = Table.lookup_key (table_of arg);
+fun lookup arg = Table.lookup (table_of arg);
+fun defined arg = Table.defined (table_of arg);
+
+fun change_table key f =
+ map_change_table (fn (change, table) => (update_change key change, f table));
+
+fun update (key, x) = change_table key (Table.update (key, x));
+fun update_new (key, x) = change_table key (Table.update_new (key, x));
+fun map_entry key f = change_table key (Table.map_entry key f);
+fun map_default (key, x) f = change_table key (Table.map_default (key, x) f);
+fun delete_safe key = change_table key (Table.delete_safe key);
+
+end;
+
+structure Change_Table = Change_Table(type key = string val ord = fast_string_ord);
+
--- a/src/Pure/General/name_space.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/General/name_space.ML Wed Mar 12 12:18:41 2014 +0100
@@ -55,6 +55,7 @@
val map_naming: (naming -> naming) -> Context.generic -> Context.generic
val declare: Context.generic -> bool -> binding -> T -> string * T
type 'a table
+ val change_base: bool -> 'a table -> 'a table
val space_of_table: 'a table -> T
val check_reports: Context.generic -> 'a table ->
xstring * Position.T list -> (string * Position.report list) * 'a
@@ -69,12 +70,12 @@
val fold_table: (string * 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
val empty_table: string -> 'a table
val merge_tables: 'a table * 'a table -> 'a table
- val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
+ val join_tables: (string -> 'a * 'a -> 'a) (*exception Change_Table.SAME*) ->
'a table * 'a table -> 'a table
- val dest_table': Proof.context -> T -> 'a Symtab.table -> ((string * xstring) * 'a) list
- val dest_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
- val extern_table': Proof.context -> T -> 'a Symtab.table -> ((Markup.T * xstring) * 'a) list
- val extern_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
+ val extern_entries: Proof.context -> T -> (string * 'a) list -> ((string * xstring) * 'a) list
+ val markup_entries: Proof.context -> T -> (string * 'a) list -> ((Markup.T * xstring) * 'a) list
+ val extern_table: Proof.context -> 'a table -> ((string * xstring) * 'a) list
+ val markup_table: Proof.context -> 'a table -> ((Markup.T * xstring) * 'a) list
end;
structure Name_Space: NAME_SPACE =
@@ -110,8 +111,8 @@
datatype T =
Name_Space of
{kind: string,
- internals: (string list * string list) Symtab.table, (*visible, hidden*)
- entries: (xstring list * entry) Symtab.table}; (*externals, entry*)
+ internals: (string list * string list) Change_Table.T, (*visible, hidden*)
+ entries: (xstring list * entry) Change_Table.T}; (*externals, entry*)
fun make_name_space (kind, internals, entries) =
Name_Space {kind = kind, internals = internals, entries = entries};
@@ -119,25 +120,28 @@
fun map_name_space f (Name_Space {kind = kind, internals = internals, entries = entries}) =
make_name_space (f (kind, internals, entries));
+fun change_base_space begin = map_name_space (fn (kind, internals, entries) =>
+ (kind, Change_Table.change_base begin internals, Change_Table.change_base begin entries));
+
fun map_internals f xname = map_name_space (fn (kind, internals, entries) =>
- (kind, Symtab.map_default (xname, ([], [])) f internals, entries));
+ (kind, Change_Table.map_default (xname, ([], [])) f internals, entries));
-fun empty kind = make_name_space (kind, Symtab.empty, Symtab.empty);
+fun empty kind = make_name_space (kind, Change_Table.empty, Change_Table.empty);
fun kind_of (Name_Space {kind, ...}) = kind;
-fun defined_entry (Name_Space {entries, ...}) = Symtab.defined entries;
+fun defined_entry (Name_Space {entries, ...}) = Change_Table.defined entries;
fun the_entry (Name_Space {kind, entries, ...}) name =
- (case Symtab.lookup entries name of
+ (case Change_Table.lookup entries name of
NONE => error (undefined kind name)
| SOME (_, entry) => entry);
fun entry_ord space = int_ord o pairself (#id o the_entry space);
fun markup (Name_Space {kind, entries, ...}) name =
- (case Symtab.lookup entries name of
+ (case Change_Table.lookup entries name of
NONE => Markup.intensify
| SOME (_, entry) => entry_markup false kind (name, entry));
@@ -147,7 +151,7 @@
(* name accesses *)
fun lookup (Name_Space {internals, ...}) xname =
- (case Symtab.lookup internals xname of
+ (case Change_Table.lookup internals xname of
NONE => (xname, true)
| SOME ([], []) => (xname, true)
| SOME ([name], _) => (name, true)
@@ -155,12 +159,12 @@
| SOME ([], name' :: _) => (Long_Name.hidden name', true));
fun get_accesses (Name_Space {entries, ...}) name =
- (case Symtab.lookup entries name of
+ (case Change_Table.lookup entries name of
NONE => [name]
| SOME (externals, _) => externals);
fun valid_accesses (Name_Space {internals, ...}) name =
- Symtab.fold (fn (xname, (names, _)) =>
+ Change_Table.fold (fn (xname, (names, _)) =>
if not (null names) andalso hd names = name then cons xname else I) internals [];
@@ -224,7 +228,7 @@
val Name_Space {kind, internals, ...} = space;
val ext = extern_shortest (Context.proof_of context) space;
val names =
- Symtab.fold
+ Change_Table.fold
(fn (a, (name :: _, _)) =>
if String.isPrefix x a andalso not (is_concealed space name)
then
@@ -273,14 +277,14 @@
if kind1 = kind2 then kind1
else error ("Attempt to merge different kinds of name spaces " ^
quote kind1 ^ " vs. " ^ quote kind2);
- val internals' = (internals1, internals2) |> Symtab.join
+ val internals' = (internals1, internals2) |> Change_Table.join
(K (fn ((names1, names1'), (names2, names2')) =>
if pointer_eq (names1, names2) andalso pointer_eq (names1', names2')
- then raise Symtab.SAME
+ then raise Change_Table.SAME
else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
- val entries' = (entries1, entries2) |> Symtab.join
+ val entries' = (entries1, entries2) |> Change_Table.join
(fn name => fn ((_, entry1), (_, entry2)) =>
- if #id entry1 = #id entry2 then raise Symtab.SAME
+ if #id entry1 = #id entry2 then raise Change_Table.SAME
else err_dup kind' (name, entry1) (name, entry2) Position.none);
in make_name_space (kind', internals', entries') end;
@@ -390,9 +394,9 @@
|> fold (add_name name) accs
|> map_name_space (fn (kind, internals, entries) =>
let
- val _ = Symtab.defined entries name orelse error (undefined kind name);
+ val _ = Change_Table.defined entries name orelse error (undefined kind name);
val entries' = entries
- |> Symtab.map_entry name (fn (externals, entry) =>
+ |> Change_Table.map_entry name (fn (externals, entry) =>
(Library.merge (op =) (externals, accs'), entry))
in (kind, internals, entries') end);
in space' end;
@@ -429,9 +433,10 @@
map_name_space (fn (kind, internals, entries) =>
let
val entries' =
- (if strict then Symtab.update_new else Symtab.update) (name, (externals, entry)) entries
- handle Symtab.DUP dup =>
- err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry) (#pos entry);
+ (if strict then Change_Table.update_new else Change_Table.update)
+ (name, (externals, entry)) entries
+ handle Change_Table.DUP dup =>
+ err_dup kind (dup, #2 (the (Change_Table.lookup entries dup))) (name, entry) (#pos entry);
in (kind, internals, entries') end);
fun declare context strict binding space =
@@ -464,13 +469,16 @@
(* definition in symbol table *)
-datatype 'a table = Table of T * 'a Symtab.table;
+datatype 'a table = Table of T * 'a Change_Table.T;
+
+fun change_base begin (Table (space, tab)) =
+ Table (change_base_space begin space, Change_Table.change_base begin tab);
fun space_of_table (Table (space, _)) = space;
fun check_reports context (Table (space, tab)) (xname, ps) =
let val name = intern space xname in
- (case Symtab.lookup tab name of
+ (case Change_Table.lookup tab name of
SOME x =>
let
val reports =
@@ -492,7 +500,7 @@
val _ = Position.reports reports;
in (name, x) end;
-fun lookup_key (Table (_, tab)) name = Symtab.lookup_key tab name;
+fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
fun get table name =
(case lookup_key table name of
@@ -502,7 +510,7 @@
fun define context strict (binding, x) (Table (space, tab)) =
let
val (name, space') = declare context strict binding space;
- val tab' = Symtab.update (name, x) tab;
+ val tab' = Change_Table.update (name, x) tab;
in (name, Table (space', tab')) end;
@@ -517,36 +525,35 @@
fun del_table name (Table (space, tab)) =
let
val space' = hide true name space handle ERROR _ => space;
- val tab' = Symtab.delete_safe name tab;
+ val tab' = Change_Table.delete_safe name tab;
in Table (space', tab') end;
fun map_table_entry name f (Table (space, tab)) =
- Table (space, Symtab.map_entry name f tab);
+ Table (space, Change_Table.map_entry name f tab);
-fun fold_table f (Table (_, tab)) = Symtab.fold f tab;
+fun fold_table f (Table (_, tab)) = Change_Table.fold f tab;
-fun empty_table kind = Table (empty kind, Symtab.empty);
+fun empty_table kind = Table (empty kind, Change_Table.empty);
fun merge_tables (Table (space1, tab1), Table (space2, tab2)) =
- Table (merge (space1, space2), Symtab.merge (K true) (tab1, tab2));
+ Table (merge (space1, space2), Change_Table.merge (K true) (tab1, tab2));
fun join_tables f (Table (space1, tab1), Table (space2, tab2)) =
- Table (merge (space1, space2), Symtab.join f (tab1, tab2));
+ Table (merge (space1, space2), Change_Table.join f (tab1, tab2));
(* present table content *)
-fun dest_table' ctxt space tab =
- Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
+fun extern_entries ctxt space entries =
+ fold (fn (name, x) => cons ((name, extern ctxt space name), x)) entries []
|> Library.sort_wrt (#2 o #1);
-fun dest_table ctxt (Table (space, tab)) = dest_table' ctxt space tab;
-
-fun extern_table' ctxt space tab =
- dest_table' ctxt space tab
+fun markup_entries ctxt space entries =
+ extern_entries ctxt space entries
|> map (fn ((name, xname), x) => ((markup space name, xname), x));
-fun extern_table ctxt (Table (space, tab)) = extern_table' ctxt space tab;
+fun extern_table ctxt (Table (space, tab)) = extern_entries ctxt space (Change_Table.dest tab);
+fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Change_Table.dest tab);
end;
--- a/src/Pure/General/table.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/General/table.ML Wed Mar 12 12:18:41 2014 +0100
@@ -36,10 +36,10 @@
val update: key * 'a -> 'a table -> 'a table
val update_new: key * 'a -> 'a table -> 'a table (*exception DUP*)
val default: key * 'a -> 'a table -> 'a table
- val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
+ val map_entry: key -> ('a -> 'a) (*exception SAME*) -> 'a table -> 'a table
val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
val make: (key * 'a) list -> 'a table (*exception DUP*)
- val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
+ val join: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
'a table * 'a table -> 'a table (*exception DUP*)
val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception DUP*)
val delete: key -> 'a table -> 'a table (*exception UNDEF*)
--- a/src/Pure/Isar/attrib.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Mar 12 12:18:41 2014 +0100
@@ -104,7 +104,7 @@
Pretty.block
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
- [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
+ [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table ctxt attribs))]
|> Pretty.chunks |> Pretty.writeln
end;
@@ -337,7 +337,9 @@
Pretty.brk 1, Pretty.str (Config.print_value value)]
end;
val space = attribute_space ctxt;
- val configs = Name_Space.extern_table' ctxt space (Configs.get (Proof_Context.theory_of ctxt));
+ val configs =
+ Name_Space.markup_entries ctxt space
+ (Symtab.dest (Configs.get (Proof_Context.theory_of ctxt)));
in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
--- a/src/Pure/Isar/bundle.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/bundle.ML Wed Mar 12 12:18:41 2014 +0100
@@ -133,7 +133,7 @@
Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
in
- map prt_bundle (Name_Space.extern_table ctxt (get_bundles ctxt))
+ map prt_bundle (Name_Space.markup_table ctxt (get_bundles ctxt))
end |> Pretty.chunks |> Pretty.writeln;
end;
--- a/src/Pure/Isar/class.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/class.ML Wed Mar 12 12:18:41 2014 +0100
@@ -571,6 +571,7 @@
| NONE => NONE);
in
thy
+ |> Sign.change_begin
|> Proof_Context.init_global
|> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
|> fold (Variable.declare_typ o TFree) vs
@@ -586,7 +587,7 @@
abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
declaration = K Generic_Target.theory_declaration,
pretty = pretty,
- exit = Local_Theory.target_of o conclude}
+ exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
end;
fun instantiation_cmd arities thy =
--- a/src/Pure/Isar/expression.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/expression.ML Wed Mar 12 12:18:41 2014 +0100
@@ -944,9 +944,16 @@
fun gen_sublocale_global prep_loc prep_interpretation
before_exit raw_locale expression raw_eqns thy =
- thy
- |> Named_Target.init before_exit (prep_loc thy raw_locale)
- |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns;
+ let
+ val lthy = Named_Target.init before_exit (prep_loc thy raw_locale) thy;
+ fun setup_proof after_qed =
+ Element.witness_proof_eqs
+ (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
+ in
+ lthy |>
+ generic_interpretation prep_interpretation setup_proof
+ Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_eqns
+ end;
in
--- a/src/Pure/Isar/local_theory.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Mar 12 12:18:41 2014 +0100
@@ -313,6 +313,7 @@
mark_brittle #> activate_nonbrittle dep_morph mixin export;
+
(** init and exit **)
(* init *)
--- a/src/Pure/Isar/locale.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/locale.ML Wed Mar 12 12:18:41 2014 +0100
@@ -635,7 +635,7 @@
(Pretty.breaks
(Pretty.str "locales:" ::
map (Pretty.mark_str o #1)
- (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy))))
+ (Name_Space.markup_table (Proof_Context.init_global thy) (Locales.get thy))))
|> Pretty.writeln;
fun pretty_locale thy show_facts name =
--- a/src/Pure/Isar/method.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/method.ML Wed Mar 12 12:18:41 2014 +0100
@@ -328,7 +328,7 @@
Pretty.block
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
in
- [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
+ [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table ctxt meths))]
|> Pretty.chunks |> Pretty.writeln
end;
--- a/src/Pure/Isar/named_target.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/named_target.ML Wed Mar 12 12:18:41 2014 +0100
@@ -175,6 +175,7 @@
|> Name_Space.mandatory_path (Long_Name.base_name target);
in
thy
+ |> Sign.change_begin
|> init_context ta
|> Data.put (SOME ta)
|> Local_Theory.init naming
@@ -183,7 +184,7 @@
abbrev = Generic_Target.abbrev (target_abbrev ta),
declaration = target_declaration ta,
pretty = pretty ta,
- exit = Local_Theory.target_of o before_exit}
+ exit = before_exit #> Local_Theory.target_of #> Sign.change_end_local}
end;
val theory_init = init I "";
--- a/src/Pure/Isar/overloading.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/overloading.ML Wed Mar 12 12:18:41 2014 +0100
@@ -194,6 +194,7 @@
(Term.dest_Const (prep_const ctxt const), (v, checked)));
in
thy
+ |> Sign.change_begin
|> Proof_Context.init_global
|> Data.put overloading
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
@@ -205,7 +206,7 @@
abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
declaration = K Generic_Target.theory_declaration,
pretty = pretty,
- exit = Local_Theory.target_of o conclude}
+ exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
end;
val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
--- a/src/Pure/Isar/proof_context.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Mar 12 12:18:41 2014 +0100
@@ -1236,7 +1236,7 @@
if not show_globals andalso Symtab.defined globals c then I
else cons (c, Logic.mk_equals (Const (c, T), t));
val abbrevs =
- Name_Space.extern_table' ctxt space (Symtab.make (Symtab.fold add_abbr constants []));
+ Name_Space.markup_entries ctxt space (Symtab.fold add_abbr constants []);
in
if null abbrevs then []
else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
--- a/src/Pure/Isar/toplevel.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Mar 12 12:18:41 2014 +0100
@@ -534,7 +534,7 @@
fun theory_to_proof f = begin_proof
(fn _ => fn gthy =>
- (Context.Theory o Sign.reset_group o Proof_Context.theory_of,
+ (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of,
(case gthy of
Context.Theory thy => f (Sign.new_group thy)
| _ => raise UNDEF)));
--- a/src/Pure/ROOT Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/ROOT Wed Mar 12 12:18:41 2014 +0100
@@ -71,6 +71,7 @@
"General/basics.ML"
"General/binding.ML"
"General/buffer.ML"
+ "General/change_table.ML"
"General/completion.ML"
"General/file.ML"
"General/graph.ML"
--- a/src/Pure/ROOT.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/ROOT.ML Wed Mar 12 12:18:41 2014 +0100
@@ -64,6 +64,7 @@
use "PIDE/xml.ML";
use "PIDE/yxml.ML";
+use "General/change_table.ML";
use "General/graph.ML";
use "System/options.ML";
--- a/src/Pure/Thy/thy_output.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Mar 12 12:18:41 2014 +0100
@@ -104,8 +104,8 @@
fun print_antiquotations ctxt =
let
val (commands, options) = get_antiquotations ctxt;
- val command_names = map #1 (Name_Space.extern_table ctxt commands);
- val option_names = map #1 (Name_Space.extern_table ctxt options);
+ val command_names = map #1 (Name_Space.markup_table ctxt commands);
+ val option_names = map #1 (Name_Space.markup_table ctxt options);
in
[Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
--- a/src/Pure/consts.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/consts.ML Wed Mar 12 12:18:41 2014 +0100
@@ -9,6 +9,7 @@
sig
type T
val eq_consts: T * T -> bool
+ val change_base: bool -> T -> T
val retrieve_abbrevs: T -> string list -> term -> (term * term) list
val dest: T ->
{const_space: Name_Space.T,
@@ -65,6 +66,9 @@
fun map_consts f (Consts {decls, constraints, rev_abbrevs}) =
make_consts (f (decls, constraints, rev_abbrevs));
+fun change_base begin = map_consts (fn (decls, constraints, rev_abbrevs) =>
+ (Name_Space.change_base begin decls, constraints, rev_abbrevs));
+
(* reverted abbrevs *)
--- a/src/Pure/defs.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/defs.ML Wed Mar 12 12:18:41 2014 +0100
@@ -50,8 +50,10 @@
handle Type.TUNIFY => true);
fun match_args (Ts, Us) =
- Option.map Envir.subst_type
- (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE);
+ if Type.could_matches (Ts, Us) then
+ Option.map Envir.subst_type
+ (SOME (Type.raw_matches (Ts, Us) Vartab.empty) handle Type.TYPE_MATCH => NONE)
+ else NONE;
(* datatype defs *)
--- a/src/Pure/display.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/display.ML Wed Mar 12 12:18:41 2014 +0100
@@ -157,22 +157,24 @@
val arities = Sorts.arities_of class_algebra;
val clsses =
- Name_Space.dest_table' ctxt class_space
- (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)))
+ Name_Space.extern_entries ctxt class_space
+ (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
|> map (apfst #1);
- val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1);
- val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1);
+ val tdecls = Name_Space.extern_table ctxt types |> map (apfst #1);
+ val arties =
+ Name_Space.extern_entries ctxt (Type.type_space tsig) (Symtab.dest arities)
+ |> map (apfst #1);
fun prune_const c = not verbose andalso Consts.is_concealed consts c;
val cnsts =
- Name_Space.extern_table' ctxt const_space
- (Symtab.make (filter_out (prune_const o fst) (Symtab.dest constants)));
+ Name_Space.markup_entries ctxt const_space
+ (filter_out (prune_const o fst) (Symtab.dest constants));
val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
- val cnstrs = Name_Space.extern_table' ctxt const_space constraints;
+ val cnstrs = Name_Space.markup_entries ctxt const_space (Symtab.dest constraints);
- val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy);
+ val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
|> map (fn (lhs, rhs) =>
--- a/src/Pure/sign.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/sign.ML Wed Mar 12 12:18:41 2014 +0100
@@ -7,6 +7,10 @@
signature SIGN =
sig
+ val change_begin: theory -> theory
+ val change_end: theory -> theory
+ val change_end_local: Proof.context -> Proof.context
+ val change_check: theory -> theory
val syn_of: theory -> Syntax.syntax
val tsig_of: theory -> Type.tsig
val classes_of: theory -> Sorts.algebra
@@ -151,6 +155,22 @@
fun map_consts f = map_sign (fn (syn, tsig, consts) => (syn, tsig, f consts));
+(* linear change discipline *)
+
+fun change_base begin = map_sign (fn (syn, tsig, consts) =>
+ (syn, Type.change_base begin tsig, Consts.change_base begin consts));
+
+val change_begin = change_base true;
+val change_end = change_base false;
+
+fun change_end_local ctxt =
+ Context.raw_transfer (change_end (Proof_Context.theory_of ctxt)) ctxt;
+
+fun change_check thy =
+ if can change_end thy
+ then raise Fail "Unfinished linear change of theory content" else thy;
+
+
(* syntax *)
val syn_of = #syn o rep_sg;
--- a/src/Pure/theory.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/theory.ML Wed Mar 12 12:18:41 2014 +0100
@@ -175,7 +175,10 @@
end;
fun end_theory thy =
- thy |> apply_wrappers (end_wrappers thy) |> Context.finish_thy;
+ thy
+ |> apply_wrappers (end_wrappers thy)
+ |> Sign.change_check
+ |> Context.finish_thy;
--- a/src/Pure/thm.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/thm.ML Wed Mar 12 12:18:41 2014 +0100
@@ -1743,7 +1743,7 @@
);
fun extern_oracles ctxt =
- map #1 (Name_Space.extern_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
+ map #1 (Name_Space.markup_table ctxt (Oracles.get (Proof_Context.theory_of ctxt)));
fun add_oracle (b, oracle) thy =
let
--- a/src/Pure/type.ML Tue Mar 11 17:18:42 2014 +0100
+++ b/src/Pure/type.ML Wed Mar 12 12:18:41 2014 +0100
@@ -25,6 +25,7 @@
default: sort,
types: decl Name_Space.table,
log_types: string list}
+ val change_base: bool -> tsig -> tsig
val empty_tsig: tsig
val class_space: tsig -> Name_Space.T
val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
@@ -76,6 +77,8 @@
val typ_instance: tsig -> typ * typ -> bool
val raw_match: typ * typ -> tyenv -> tyenv
val raw_matches: typ list * typ list -> tyenv -> tyenv
+ val could_match: typ * typ -> bool
+ val could_matches: typ list * typ list -> bool
val raw_instance: typ * typ -> bool
exception TUNIFY
val unify: tsig -> typ * typ -> tyenv * int -> tyenv * int
@@ -174,6 +177,9 @@
fun make_tsig (classes, default, types, log_types) =
TSig {classes = classes, default = default, types = types, log_types = log_types};
+fun change_base begin (TSig {classes, default, types, log_types}) =
+ make_tsig (classes, default, Name_Space.change_base begin types, log_types);
+
fun build_tsig (classes, default, types) =
let
val log_types =
@@ -461,8 +467,19 @@
| raw_matches ([], []) subs = subs
| raw_matches _ _ = raise TYPE_MATCH;
+(*fast matching filter*)
+fun could_match (Type (a, Ts), Type (b, Us)) = a = b andalso could_matches (Ts, Us)
+ | could_match (TFree (a, _), TFree (b, _)) = a = b
+ | could_match (TVar _, _) = true
+ | could_match _ = false
+and could_matches (T :: Ts, U :: Us) = could_match (T, U) andalso could_matches (Ts, Us)
+ | could_matches ([], []) = true
+ | could_matches _ = false;
+
fun raw_instance (T, U) =
- (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false;
+ if could_match (U, T) then
+ (raw_match (U, T) Vartab.empty; true) handle TYPE_MATCH => false
+ else false;
(* unification *)