# HG changeset patch
# User wenzelm
# Date 1113759551 -7200
# Node ID 144c9f9a8ade44287eefb2015bb574229514aef5
# Parent  07e382399a9682abaaeae7d5e7efbbdececdba15
tuned;

diff -r 07e382399a96 -r 144c9f9a8ade src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sun Apr 17 19:38:53 2005 +0200
+++ b/src/Pure/General/graph.ML	Sun Apr 17 19:39:11 2005 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/General/graph.ML
     ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Directed graphs.
 *)
@@ -18,7 +18,7 @@
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
-  val get_node: 'a T -> key -> 'a (* UNDEF *)
+  val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
   val imm_preds: 'a T -> key -> key list
   val imm_succs: 'a T -> key -> key list
@@ -26,18 +26,18 @@
   val all_succs: 'a T -> key list -> key list
   val strong_conn: 'a T -> key list list
   val find_paths: 'a T -> key * key -> key list list
-  val new_node: key * 'a -> 'a T -> 'a T (* DUP *)
-  val del_nodes: key list -> 'a T -> 'a T
+  val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
+  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T
   val del_edge: key * key -> 'a T -> 'a T
-  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
+  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
   exception CYCLES of key list list
-  val add_edge_acyclic: key * key -> 'a T -> 'a T
-  val add_deps_acyclic: key * key list -> 'a T -> 'a T
-  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
-  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T
-  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
+  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
+  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
+  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
+  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
+  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
@@ -52,11 +52,7 @@
 infix mem_key;
 val op mem_key = gen_mem eq_key;
 
-infix ins_key;
-val op ins_key = gen_ins eq_key;
-
-infix del_key;
-fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
+val remove_key = remove eq_key;
 
 
 (* tables and sets of keys *)
@@ -70,7 +66,7 @@
 fun x mem_keys tab = isSome (Table.lookup (tab: keys, x));
 
 infix ins_keys;
-fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab);
+fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
 
 
 (* graphs *)
@@ -146,17 +142,14 @@
 
 (* nodes *)
 
-exception DUPLICATE of key;
-
 fun new_node (x, info) (Graph tab) =
   Graph (Table.update_new ((x, (info, ([], []))), tab));
 
 fun del_nodes xs (Graph tab) =
-  let
-    fun del (x, (i, (preds, succs))) =
-      if x mem_key xs then NONE
-      else SOME (x, (i, (Library.foldl op del_key (preds, xs), Library.foldl op del_key (succs, xs))));
-  in Graph (Table.make (List.mapPartial del (Table.dest tab))) end;
+  Graph (tab
+    |> fold Table.delete xs
+    |> Table.map (fn (i, (preds, succs)) =>
+      (i, (fold remove_key xs preds, fold remove_key xs succs))));
 
 
 (* edges *)
@@ -171,8 +164,8 @@
 
 fun del_edge (x, y) G =
   if is_edge G (x, y) then
-    G |> map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)))
-      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y)))
+    G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
+      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
   else G;
 
 fun diff_edges G1 G2 =
@@ -204,8 +197,7 @@
       [] => add_edge (x, y) G
     | cycles => raise CYCLES (map (cons x) cycles));
 
-fun add_deps_acyclic (y, xs) G =
-  Library.foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
+fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
 
 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
 
diff -r 07e382399a96 -r 144c9f9a8ade src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Apr 17 19:38:53 2005 +0200
+++ b/src/Pure/Syntax/printer.ML	Sun Apr 17 19:39:11 2005 +0200
@@ -250,7 +250,7 @@
   in overwrite (prtabs, (mode, tab)) end;
 
 fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m;
-fun remove_prtabs m = change_prtabs (fn (c, prnp) => Symtab.map_entry c (remove prnp)) m;
+fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m;
 
 fun merge_prtabs prtabs1 prtabs2 =
   let
diff -r 07e382399a96 -r 144c9f9a8ade src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Apr 17 19:38:53 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Apr 17 19:39:11 2005 +0200
@@ -87,10 +87,7 @@
 fun extend_trtab name trfuns tab = Symtab.extend (tab, trfuns)
   handle Symtab.DUPS cs => err_dup_trfuns name cs;
 
-fun remove_trtab trfuns = trfuns |> fold (fn (c, (_, s: stamp)) => fn tab =>
-  if Option.map snd (Symtab.lookup (tab, c)) = SOME s
-  then Symtab.delete c tab
-  else tab);
+fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
 
 fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
   handle Symtab.DUPS cs => err_dup_trfuns name cs;
@@ -99,12 +96,8 @@
 (* print (ast) translations *)
 
 fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
-
-fun extend_tr'tab trfuns tab = foldr Symtab.update_multi tab trfuns;
-
-fun remove_tr'tab trfuns = trfuns |> fold (fn (c, tr) =>
-  Symtab.map_entry c (gen_remove SynExt.eq_trfun tr));
-
+fun extend_tr'tab trfuns = fold_rev (curry Symtab.update_multi) trfuns;
+fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
 fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
 
 
@@ -138,11 +131,9 @@
 
 fun extend_tokentrtab tokentrs tabs =
   let
-    fun ins_tokentr (ts, (m, c, f)) =
+    fun ins_tokentr (m, c, f) ts =
       overwrite (ts, (m, ("_" ^ c, (f, stamp ())) :: assocs ts m));
-  in
-    merge_tokentrtabs tabs (Library.foldl ins_tokentr ([], tokentrs))
-  end;
+  in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end;
 
 
 
@@ -156,10 +147,10 @@
 
 (* empty, extend, merge ruletabs *)
 
-fun extend_ruletab rules tab =
-  foldr Symtab.update_multi tab (map (fn r => (Ast.head_of_rule r, r)) rules);
+val extend_ruletab =
+  fold_rev (fn r => fn tab => Symtab.update_multi ((Ast.head_of_rule r, r), tab));
 
-val remove_ruletab = fold (fn r => Symtab.map_entry (Ast.head_of_rule r) (remove r));
+val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
 
 fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
 
@@ -246,7 +237,7 @@
     val {input, lexicon, gram, consts, prmodes,
       parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
       print_ast_trtab, tokentrtab, prtabs} = tabs;
-    val input' = if inout then fold remove xprods input else input;
+    val input' = if inout then fold (remove (op =)) xprods input else input;
   in
     Syntax {
       input = input',
@@ -306,15 +297,14 @@
 
 
 
-(** inspect syntax **)
+(** print syntax **)
+
+local
 
 fun pretty_strs_qs name strs =
   Pretty.strs (name :: map Library.quote (sort_strings strs));
 
-
-(* print_gram *)
-
-fun print_gram (Syntax tabs) =
+fun pretty_gram (Syntax tabs) =
   let
     val {lexicon, prmodes, gram, prtabs, ...} = tabs;
     val prmodes' = sort_strings (filter_out (equal "") prmodes);
@@ -322,13 +312,9 @@
     [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
       Pretty.big_list "prods:" (Parser.pretty_gram gram),
       pretty_strs_qs "print modes:" prmodes']
-    |> Pretty.chunks |> Pretty.writeln
   end;
 
-
-(* print_trans *)
-
-fun print_trans (Syntax tabs) =
+fun pretty_trans (Syntax tabs) =
   let
     fun pretty_trtab name tab =
       pretty_strs_qs name (Symtab.keys tab);
@@ -349,13 +335,15 @@
       pretty_ruletab "print_rules:" print_ruletab,
       pretty_trtab "print_ast_translation:" print_ast_trtab,
       Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
-    |> Pretty.chunks |> Pretty.writeln
   end;
 
+in
 
-(* print_syntax *)
+fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
+fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
+fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
 
-fun print_syntax syn = (print_gram syn; print_trans syn);
+end;