# HG changeset patch # User wenzelm # Date 1282050649 -7200 # Node ID 62d16c415019463d0137bcefbb78e3e7b52a485d # Parent f55e77f623ab3f6f2ee42b535d345f455d80aee9 added functor Linear_Set, based on former adhoc structures in document.ML; Linear_Set.delete_after (ML): actually delete table entries; Scala Linear_Set: clarified exceptions, according to ML version; simplified Document.node using Linear_Set; ML Document.edit: refer to start via NONE instead of no_id, according to Scala version; diff -r f55e77f623ab -r 62d16c415019 src/Pure/General/linear_set.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/linear_set.ML Tue Aug 17 15:10:49 2010 +0200 @@ -0,0 +1,142 @@ +(* Title: Pure/General/linear_set.ML + Author: Makarius + +Sets with canonical linear order, or immutable linked-lists. +*) + +signature LINEAR_SET = +sig + type key + type 'a T + exception DUPLICATE of key + exception UNDEFINED of key + exception NEXT_UNDEFINED of key option + val empty: 'a T + val is_empty: 'a T -> bool + val defined: 'a T -> key -> bool + val lookup: 'a T -> key -> 'a option + val update: key * 'a -> 'a T -> 'a T + val fold: key option -> + ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b + val get_first: key option -> + ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option + val get_after: 'a T -> key option -> key option + val insert_after: key option -> key * 'a -> 'a T -> 'a T + val delete_after: key option -> 'a T -> 'a T +end; + +functor Linear_Set(Key: KEY): LINEAR_SET = +struct + +(* type key *) + +type key = Key.key; +structure Table = Table(Key); + +exception DUPLICATE of key; +exception UNDEFINED of key; +exception NEXT_UNDEFINED of key option; + + +(* raw entries *) + +fun the_entry entries key = + (case Table.lookup entries key of + NONE => raise UNDEFINED key + | SOME entry => entry); + +fun next_entry entries key = snd (the_entry entries key); + +fun put_entry entry entries = Table.update entry entries; + +fun new_entry entry entries = Table.update_new entry entries + handle Table.DUP key => raise DUPLICATE key; + +fun del_entry key entries = Table.delete_safe key entries; + + +(* set representation and basic operations *) + +datatype 'a T = Set of {start: key option, entries: ('a * key option) Table.table}; + +fun make_set (start, entries) = Set {start = start, entries = entries}; +fun map_set f (Set {start, entries}) = make_set (f (start, entries)); + +fun start_of (Set {start, ...}) = start; +fun entries_of (Set {entries, ...}) = entries; + +val empty = Set {start = NONE, entries = Table.empty}; +fun is_empty set = is_none (start_of set); + +fun defined set key = Table.defined (entries_of set) key; + +fun lookup set key = Option.map fst (Table.lookup (entries_of set) key); + +fun update (key, x) = map_set (fn (start, entries) => + (start, put_entry (key, (x, next_entry entries key)) entries)); + + +(* iterate entries *) + +fun optional_start set NONE = start_of set + | optional_start _ some = some; + +fun fold opt_start f set = + let + val entries = entries_of set; + fun apply _ NONE y = y + | apply prev (SOME key) y = + let + val (x, next) = the_entry entries key; + val item = ((prev, key), x); + in apply (SOME key) next (f item y) end; + in apply NONE (optional_start set opt_start) end; + +fun get_first opt_start P set = + let + val entries = entries_of set; + fun first _ NONE = NONE + | first prev (SOME key) = + let + val (x, next) = the_entry entries key; + val item = ((prev, key), x); + in if P item then SOME item else first (SOME key) next end; + in first NONE (optional_start set opt_start) end; + + +(* relative addressing *) + +fun get_after set hook = + (case hook of + NONE => start_of set + | SOME key => next_entry (entries_of set) key); + +fun insert_after hook (key, x) = map_set (fn (start, entries) => + (case hook of + NONE => (SOME key, new_entry (key, (x, start)) entries) + | SOME key1 => + let + val (x1, next) = the_entry entries key1; + val entries' = entries + |> put_entry (key1, (x1, SOME key)) + |> new_entry (key, (x, next)); + in (start, entries') end)); + +fun delete_after hook set = set |> map_set (fn (start, entries) => + (case hook of + NONE => + (case start of + NONE => raise NEXT_UNDEFINED NONE + | SOME key1 => (next_entry entries key1, del_entry key1 entries)) + | SOME key1 => + (case the_entry entries key1 of + (_, NONE) => raise NEXT_UNDEFINED (SOME key1) + | (x1, SOME key2) => + let + val entries' = entries + |> put_entry (key1, (x1, next_entry entries key2)) + |> del_entry key2; + in (start, entries') end))); + +end; + diff -r f55e77f623ab -r 62d16c415019 src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Mon Aug 16 22:56:28 2010 +0200 +++ b/src/Pure/General/linear_set.scala Tue Aug 17 15:10:49 2010 +0200 @@ -25,8 +25,9 @@ implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A] override def empty[A] = new Linear_Set[A] - class Duplicate(s: String) extends Exception(s) - class Undefined(s: String) extends Exception(s) + class Duplicate[A](x: A) extends Exception + class Undefined[A](x: A) extends Exception + class Next_Undefined[A](x: Option[A]) extends Exception } @@ -43,19 +44,22 @@ protected val rep = Linear_Set.empty_rep[A] - /* auxiliary operations */ + /* relative addressing */ + // FIXME check definedness?? def next(elem: A): Option[A] = rep.nexts.get(elem) def prev(elem: A): Option[A] = rep.prevs.get(elem) def get_after(hook: Option[A]): Option[A] = hook match { case None => rep.start - case Some(elem) => next(elem) + case Some(elem) => + if (!contains(elem)) throw new Linear_Set.Undefined(elem) + next(elem) } def insert_after(hook: Option[A], elem: A): Linear_Set[A] = - if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString) + if (contains(elem)) throw new Linear_Set.Duplicate(elem) else hook match { case None => @@ -66,7 +70,7 @@ rep.nexts + (elem -> elem1), rep.prevs + (elem1 -> elem)) } case Some(elem1) => - if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString) + if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) else rep.nexts.get(elem1) match { case None => @@ -83,7 +87,7 @@ hook match { case None => rep.start match { - case None => throw new Linear_Set.Undefined("") + case None => throw new Linear_Set.Next_Undefined[A](None) case Some(elem1) => rep.nexts.get(elem1) match { case None => empty @@ -92,10 +96,10 @@ } } case Some(elem1) => - if (!contains(elem1)) throw new Linear_Set.Undefined(elem1.toString) + if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) else rep.nexts.get(elem1) match { - case None => throw new Linear_Set.Undefined("") + case None => throw new Linear_Set.Next_Undefined(Some(elem1)) case Some(elem2) => rep.nexts.get(elem2) match { case None => @@ -153,15 +157,15 @@ def iterator(elem: A): Iterator[A] = if (contains(elem)) make_iterator(Some(elem), rep.nexts) - else throw new Linear_Set.Undefined(elem.toString) + else throw new Linear_Set.Undefined(elem) def reverse_iterator(elem: A): Iterator[A] = if (contains(elem)) make_iterator(Some(elem), rep.prevs) - else throw new Linear_Set.Undefined(elem.toString) + else throw new Linear_Set.Undefined(elem) def + (elem: A): Linear_Set[A] = insert_after(rep.end, elem) def - (elem: A): Linear_Set[A] = - if (!contains(elem)) throw new Linear_Set.Undefined(elem.toString) + if (!contains(elem)) throw new Linear_Set.Undefined(elem) else delete_after(prev(elem)) } \ No newline at end of file diff -r f55e77f623ab -r 62d16c415019 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Aug 16 22:56:28 2010 +0200 +++ b/src/Pure/IsaMakefile Tue Aug 17 15:10:49 2010 +0200 @@ -80,6 +80,7 @@ General/graph.ML \ General/heap.ML \ General/integer.ML \ + General/linear_set.ML \ General/long_name.ML \ General/markup.ML \ General/name_space.ML \ diff -r f55e77f623ab -r 62d16c415019 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Mon Aug 16 22:56:28 2010 +0200 +++ b/src/Pure/PIDE/document.ML Tue Aug 17 15:10:49 2010 +0200 @@ -15,7 +15,7 @@ val new_id: unit -> id val parse_id: string -> id val print_id: id -> string - type edit = string * ((command_id * command_id option) list) option + type edit = string * ((command_id option * command_id option) list) option type state val init_state: state val define_command: command_id -> string -> state -> state @@ -55,82 +55,43 @@ (** document structure **) -abstype entry = Entry of {next: command_id option, exec: exec_id option} - and node = Node of entry Inttab.table (*unique entries indexed by command_id, start with no_id*) +structure Entries = Linear_Set(type key = command_id val ord = int_ord); + +abstype node = Node of exec_id option Entries.T (*command entries with excecutions*) and version = Version of node Graph.T (*development graph wrt. static imports*) with - -(* command entries *) - -fun make_entry next exec = Entry {next = next, exec = exec}; - -fun the_entry (Node entries) (id: command_id) = - (case Inttab.lookup entries id of - NONE => err_undef "command entry" id - | SOME (Entry entry) => entry); +val empty_node = Node Entries.empty; +val empty_version = Version Graph.empty; -fun put_entry (id: command_id, entry: entry) (Node entries) = - Node (Inttab.update (id, entry) entries); - -fun put_entry_exec (id: command_id) exec node = - let val {next, ...} = the_entry node id - in put_entry (id, make_entry next exec) node end; - -fun reset_entry_exec id = put_entry_exec id NONE; -fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id); +fun fold_entries start f (Node entries) = Entries.fold start f entries; +fun first_entry start P (Node entries) = Entries.get_first start P entries; -(* iterate entries *) - -fun fold_entries id0 f (node as Node entries) = - let - fun apply NONE x = x - | apply (SOME id) x = - let val entry = the_entry node id - in apply (#next entry) (f (id, entry) x) end; - in if Inttab.defined entries id0 then apply (SOME id0) else I end; - -fun first_entry P node = - let - fun first _ NONE = NONE - | first prev (SOME id) = - let val entry = the_entry node id - in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end; - in first NONE (SOME no_id) end; - - -(* modify entries *) - -fun insert_after (id: command_id) (id2: command_id) node = - let val {next, exec} = the_entry node id in - node - |> put_entry (id, make_entry (SOME id2) exec) - |> put_entry (id2, make_entry next NONE) - end; - -fun delete_after (id: command_id) node = - let val {next, exec} = the_entry node id in - (case next of - NONE => error ("No next entry to delete: " ^ print_id id) - | SOME id2 => - node |> - (case #next (the_entry node id2) of - NONE => put_entry (id, make_entry NONE exec) - | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3)) - end; - - -(* node edits *) +(* node edits and associated executions *) type edit = - string * (*node name*) - ((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*) + string * + (*NONE: remove node, SOME: insert/remove commands*) + ((command_id option * command_id option) list) option; + +fun the_entry (Node entries) id = + (case Entries.lookup entries id of + NONE => err_undef "command entry" id + | SOME entry => entry); -val empty_node = Node (Inttab.make [(no_id, make_entry NONE (SOME no_id))]); +fun update_entry (id, exec_id) (Node entries) = + Node (Entries.update (id, SOME exec_id) entries); -fun edit_node (id, SOME id2) = insert_after id id2 - | edit_node (id, NONE) = delete_after id; +fun reset_after id entries = + (case Entries.get_after entries id of + NONE => entries + | SOME next => Entries.update (next, NONE) entries); + +fun edit_node (hook, SOME id2) (Node entries) = + Node (Entries.insert_after hook (id2, NONE) entries) + | edit_node (hook, NONE) (Node entries) = + Node (entries |> Entries.delete_after hook |> reset_after hook); (* version operations *) @@ -138,16 +99,15 @@ fun nodes_of (Version nodes) = nodes; val node_names_of = Graph.keys o nodes_of; +fun get_node version name = Graph.get_node (nodes_of version) name + handle Graph.UNDEF _ => empty_node; + fun edit_nodes (name, SOME edits) (Version nodes) = Version (nodes |> Graph.default_node (name, empty_node) |> Graph.map_node name (fold edit_node edits)) - | edit_nodes (name, NONE) (Version nodes) = Version (Graph.del_node name nodes); - -val empty_version = Version Graph.empty; - -fun the_node version name = - Graph.get_node (nodes_of version) name handle Graph.UNDEF _ => empty_node; + | edit_nodes (name, NONE) (Version nodes) = + Version (Graph.del_node name nodes); (* FIXME Graph.UNDEF !? *) fun put_node name node (Version nodes) = Version (Graph.map_node name (K node) nodes); (* FIXME Graph.UNDEF !? *) @@ -173,8 +133,8 @@ val init_state = make_state (Inttab.make [(no_id, empty_version)], - Inttab.make [(no_id, Future.value Toplevel.empty)], - Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))], + Inttab.make [(no_id, Future.value Toplevel.empty)], (* FIXME no_id !?? *) + Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))], (* FIXME no_id !?? *) []); @@ -238,10 +198,10 @@ local -fun is_changed node' (id, {next = _, exec}) = +fun is_changed node' ((_, id), exec) = (case try (the_entry node') id of NONE => true - | SOME {next = _, exec = exec'} => exec' <> exec); + | SOME exec' => exec' <> exec); fun new_exec name (id: command_id) (exec_id, updates, state) = let @@ -266,15 +226,18 @@ val new_version = fold edit_nodes edits old_version; fun update_node name (rev_updates, version, st) = - let val node = the_node version name in - (case first_entry (is_changed (the_node old_version name)) node of + let val node = get_node version name in + (case first_entry NONE (is_changed (get_node old_version name)) node of NONE => (rev_updates, version, st) - | SOME (prev, id, _) => + | SOME ((prev, id), _) => let - val prev_exec = the (#exec (the_entry node (the prev))); + val prev_exec = + (case prev of + NONE => no_id + | SOME prev_id => the_default no_id (the_entry node prev_id)); val (_, rev_upds, st') = - fold_entries id (new_exec name o #1) node (prev_exec, [], st); - val node' = fold set_entry_exec rev_upds node; + fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st); + val node' = fold update_entry rev_upds node; in (rev_upds @ rev_updates, put_node name node' version, st') end) end; @@ -306,8 +269,8 @@ node_names_of version |> map (fn name => Future.fork_pri 1 (fn () => (await_cancellation (); - fold_entries no_id (fn (_, {exec, ...}) => fn () => force_exec exec) - (the_node version name) ()))); + fold_entries NONE (fn (_, exec) => fn () => force_exec exec) + (get_node version name) ()))); in (versions, commands, execs, execution') end); end; diff -r f55e77f623ab -r 62d16c415019 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Aug 16 22:56:28 2010 +0200 +++ b/src/Pure/ROOT.ML Tue Aug 17 15:10:49 2010 +0200 @@ -42,6 +42,7 @@ use "General/ord_list.ML"; use "General/balanced_tree.ML"; use "General/graph.ML"; +use "General/linear_set.ML"; use "General/long_name.ML"; use "General/binding.ML"; use "General/name_space.ML"; diff -r f55e77f623ab -r 62d16c415019 src/Pure/System/isar_document.ML --- a/src/Pure/System/isar_document.ML Mon Aug 16 22:56:28 2010 +0200 +++ b/src/Pure/System/isar_document.ML Tue Aug 17 15:10:49 2010 +0200 @@ -21,10 +21,14 @@ val old_id = Document.parse_id old_id_string; val new_id = Document.parse_id new_id_string; val edits = - XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string - (XML_Data.dest_option (XML_Data.dest_list - (XML_Data.dest_pair XML_Data.dest_int - (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); + XML_Data.dest_list + (XML_Data.dest_pair + XML_Data.dest_string + (XML_Data.dest_option + (XML_Data.dest_list + (XML_Data.dest_pair + (XML_Data.dest_option XML_Data.dest_int) + (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml); val (updates, state') = Document.edit old_id new_id edits state; val _ = diff -r f55e77f623ab -r 62d16c415019 src/Pure/System/isar_document.scala --- a/src/Pure/System/isar_document.scala Mon Aug 16 22:56:28 2010 +0200 +++ b/src/Pure/System/isar_document.scala Tue Aug 17 15:10:49 2010 +0200 @@ -51,14 +51,13 @@ def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID, edits: List[Document.Edit[Document.Command_ID]]) { - def make_id1(id1: Option[Document.Command_ID]): XML.Body = - XML_Data.make_long(id1 getOrElse Document.NO_ID) - val arg = XML_Data.make_list( XML_Data.make_pair(XML_Data.make_string)( XML_Data.make_option(XML_Data.make_list( - XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits) + XML_Data.make_pair( + XML_Data.make_option(XML_Data.make_long))( + XML_Data.make_option(XML_Data.make_long))))))(edits) input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))