# HG changeset patch # User wenzelm # Date 1394623121 -3600 # Node ID cd9ce893f2d6fc2063c64a9a2125b94f90556a01 # Parent c6a15aa64e36c0ae153aa650eb2458fa3b56d41a# Parent ad6bd8030d88efdfd3cd55280dcc8fb363a9d8b2 merged diff -r c6a15aa64e36 -r cd9ce893f2d6 src/HOL/Tools/inductive.ML --- 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; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/General/change_table.ML --- /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); + diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/General/name_space.ML --- 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; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/General/table.ML --- 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*) diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/attrib.ML --- 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; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/bundle.ML --- 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; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/class.ML --- 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 = diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/expression.ML --- 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 diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/local_theory.ML --- 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 *) diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/locale.ML --- 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 = diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/method.ML --- 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; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/named_target.ML --- 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 ""; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/overloading.ML --- 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); diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/proof_context.ML --- 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)] diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Isar/toplevel.ML --- 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))); diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/ROOT --- 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" diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/ROOT.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"; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/Thy/thy_output.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)] diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/consts.ML --- 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 *) diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/defs.ML --- 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 *) diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/display.ML --- 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) => diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/sign.ML --- 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; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/theory.ML --- 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; diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/thm.ML --- 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 diff -r c6a15aa64e36 -r cd9ce893f2d6 src/Pure/type.ML --- 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 *)