# HG changeset patch # User wenzelm # Date 1394727982 -3600 # Node ID b7add947a6effcc9ce75e737b936a678159ea675 # Parent f42de6d8ed8ed5a4247021ff122002bf935d4f56 more frugal recording of changes: join merely requires information from one side; tuned; diff -r f42de6d8ed8e -r b7add947a6ef src/Pure/General/change_table.ML --- a/src/Pure/General/change_table.ML Thu Mar 13 15:05:56 2014 +0100 +++ b/src/Pure/General/change_table.ML Thu Mar 13 17:26:22 2014 +0100 @@ -17,6 +17,7 @@ val empty: 'a T val is_empty: 'a T -> bool val change_base: bool -> 'a T -> 'a T + val change_ignore: '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 @@ -43,35 +44,42 @@ (* optional change *) -datatype change = No_Change | Change of {base: serial, depth: int, changes: Table.set}; +datatype change = + No_Change | Change of {base: serial, depth: int, changes: Table.set option}; fun make_change base depth changes = Change {base = base, depth = depth, changes = changes}; +fun ignore_change (Change {base, depth, changes = SOME _}) = + make_change base depth NONE + | ignore_change change = change; + +fun update_change key (Change {base, depth, changes = SOME ch}) = + make_change base depth (SOME (Table.insert (K true) (key, ()) ch)) + | update_change _ change = change; + fun base_change true No_Change = - make_change (serial ()) 0 Table.empty + make_change (serial ()) 0 (SOME Table.empty) | base_change true (Change {base, depth, changes}) = make_change base (depth + 1) changes | base_change false (Change {base, depth, changes}) = if depth = 0 then No_Change else make_change base (depth - 1) changes - | base_change false No_Change = raise Fail "Unbalanced block structure of change table"; + | base_change false No_Change = raise Fail "Unbalanced change structure"; -fun update_change _ No_Change = No_Change - | update_change key (Change {base, depth, changes}) = - make_change base depth (Table.insert (K true) (key, ()) changes); - -fun cannot_merge () = raise Fail "Attempt to merge tables with incompatible change base"; +fun cannot_merge () = raise Fail "Cannot merge: incompatible change structure"; fun merge_change (No_Change, No_Change) = NONE | merge_change (Change change1, Change change2) = let val {base = base1, depth = depth1, changes = changes1} = change1; val {base = base2, depth = depth2, changes = changes2} = change2; - in - if base1 = base2 andalso depth1 = depth2 then - SOME ((changes2, make_change base1 depth1 (Table.merge (K true) (changes1, changes2)))) - else cannot_merge () - end + val _ = if base1 = base2 andalso depth1 = depth2 then () else cannot_merge (); + val (swapped, ch2) = + (case (changes1, changes2) of + (_, SOME ch2) => (false, ch2) + | (SOME ch1, _) => (true, ch1) + | _ => cannot_merge ()); + in SOME (swapped, ch2, make_change base1 depth1 NONE) end | merge_change _ = cannot_merge (); @@ -90,6 +98,7 @@ 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); +fun change_ignore arg = (map_change_table o apfst) ignore_change arg; (* join and merge *) @@ -105,20 +114,21 @@ else (case merge_change (change1, change2) of NONE => make_change_table (No_Change, Table.join f (table1, table2)) - | SOME (changes2, change') => + | SOME (swapped, ch2, change') => let - fun update key table = - (case Table.lookup table2 key of - NONE => table + fun maybe_swap (x, y) = if swapped then (y, x) else (x, y); + val (tab1, tab2) = maybe_swap (table1, table2); + fun update key tab = + (case Table.lookup tab2 key of + NONE => tab | SOME y => - (case Table.lookup table key of - NONE => Table.update (key, y) table + (case Table.lookup tab key of + NONE => Table.update (key, y) tab | 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) + (case (SOME (f key (maybe_swap (x, y))) handle Table.SAME => NONE) of + NONE => tab + | SOME z => Table.update (key, z) tab))); + in make_change_table (change', Table.fold (update o #1) ch2 tab1) end) end; fun merge eq = diff -r f42de6d8ed8e -r b7add947a6ef src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Thu Mar 13 15:05:56 2014 +0100 +++ b/src/Pure/General/name_space.ML Thu Mar 13 17:26:22 2014 +0100 @@ -56,6 +56,7 @@ val declare: Context.generic -> bool -> binding -> T -> string * T type 'a table val change_base: bool -> 'a table -> 'a table + val change_ignore: '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 @@ -123,6 +124,9 @@ 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)); +val change_ignore_space = map_name_space (fn (kind, internals, entries) => + (kind, Change_Table.change_ignore internals, Change_Table.change_ignore entries)); + fun map_internals f xname = map_name_space (fn (kind, internals, entries) => (kind, Change_Table.map_default (xname, ([], [])) f internals, entries)); @@ -474,6 +478,9 @@ fun change_base begin (Table (space, tab)) = Table (change_base_space begin space, Change_Table.change_base begin tab); +fun change_ignore (Table (space, tab)) = + Table (change_ignore_space space, Change_Table.change_ignore tab); + fun space_of_table (Table (space, _)) = space; fun check_reports context (Table (space, tab)) (xname, ps) = diff -r f42de6d8ed8e -r b7add947a6ef src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Mar 13 15:05:56 2014 +0100 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 13 17:26:22 2014 +0100 @@ -219,9 +219,12 @@ ( type T = data; fun init thy = - make_data (mode_default, Local_Syntax.init thy, - (Sign.tsig_of thy, Sign.tsig_of thy), - (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases); + make_data (mode_default, + Local_Syntax.init thy, + (Type.change_ignore (Sign.tsig_of thy), Sign.tsig_of thy), + (Consts.change_ignore (Sign.consts_of thy), Sign.consts_of thy), + Facts.empty, + empty_cases); ); fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep); diff -r f42de6d8ed8e -r b7add947a6ef src/Pure/consts.ML --- a/src/Pure/consts.ML Thu Mar 13 15:05:56 2014 +0100 +++ b/src/Pure/consts.ML Thu Mar 13 17:26:22 2014 +0100 @@ -10,6 +10,7 @@ type T val eq_consts: T * T -> bool val change_base: bool -> T -> T + val change_ignore: T -> T val retrieve_abbrevs: T -> string list -> term -> (term * term) list val dest: T -> {const_space: Name_Space.T, @@ -69,6 +70,9 @@ fun change_base begin = map_consts (fn (decls, constraints, rev_abbrevs) => (Name_Space.change_base begin decls, constraints, rev_abbrevs)); +val change_ignore = map_consts (fn (decls, constraints, rev_abbrevs) => + (Name_Space.change_ignore decls, constraints, rev_abbrevs)); + (* reverted abbrevs *) diff -r f42de6d8ed8e -r b7add947a6ef src/Pure/type.ML --- a/src/Pure/type.ML Thu Mar 13 15:05:56 2014 +0100 +++ b/src/Pure/type.ML Thu Mar 13 17:26:22 2014 +0100 @@ -26,6 +26,7 @@ types: decl Name_Space.table, log_types: string list} val change_base: bool -> tsig -> tsig + val change_ignore: tsig -> tsig val empty_tsig: tsig val class_space: tsig -> Name_Space.T val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig @@ -180,6 +181,9 @@ fun change_base begin (TSig {classes, default, types, log_types}) = make_tsig (classes, default, Name_Space.change_base begin types, log_types); +fun change_ignore (TSig {classes, default, types, log_types}) = + make_tsig (classes, default, Name_Space.change_ignore types, log_types); + fun build_tsig (classes, default, types) = let val log_types =