tuned;
authorwenzelm
Sun Apr 17 19:39:11 2005 +0200 (2005-04-17)
changeset 15759144c9f9a8ade
parent 15758 07e382399a96
child 15760 1ca99038c847
tuned;
src/Pure/General/graph.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/General/graph.ML	Sun Apr 17 19:38:53 2005 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Sun Apr 17 19:39:11 2005 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (*  Title:      Pure/General/graph.ML
     1.5      ID:         $Id$
     1.6 -    Author:     Markus Wenzel, TU Muenchen
     1.7 +    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
     1.8  
     1.9  Directed graphs.
    1.10  *)
    1.11 @@ -18,7 +18,7 @@
    1.12    val minimals: 'a T -> key list
    1.13    val maximals: 'a T -> key list
    1.14    val map_nodes: ('a -> 'b) -> 'a T -> 'b T
    1.15 -  val get_node: 'a T -> key -> 'a (* UNDEF *)
    1.16 +  val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    1.17    val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    1.18    val imm_preds: 'a T -> key -> key list
    1.19    val imm_succs: 'a T -> key -> key list
    1.20 @@ -26,18 +26,18 @@
    1.21    val all_succs: 'a T -> key list -> key list
    1.22    val strong_conn: 'a T -> key list list
    1.23    val find_paths: 'a T -> key * key -> key list list
    1.24 -  val new_node: key * 'a -> 'a T -> 'a T (* DUP *)
    1.25 -  val del_nodes: key list -> 'a T -> 'a T
    1.26 +  val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    1.27 +  val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
    1.28    val is_edge: 'a T -> key * key -> bool
    1.29    val add_edge: key * key -> 'a T -> 'a T
    1.30    val del_edge: key * key -> 'a T -> 'a T
    1.31 -  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    1.32 +  val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUPS*)
    1.33    exception CYCLES of key list list
    1.34 -  val add_edge_acyclic: key * key -> 'a T -> 'a T
    1.35 -  val add_deps_acyclic: key * key list -> 'a T -> 'a T
    1.36 -  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    1.37 -  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T
    1.38 -  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T
    1.39 +  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
    1.40 +  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
    1.41 +  val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
    1.42 +  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
    1.43 +  val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    1.44  end;
    1.45  
    1.46  functor GraphFun(Key: KEY): GRAPH =
    1.47 @@ -52,11 +52,7 @@
    1.48  infix mem_key;
    1.49  val op mem_key = gen_mem eq_key;
    1.50  
    1.51 -infix ins_key;
    1.52 -val op ins_key = gen_ins eq_key;
    1.53 -
    1.54 -infix del_key;
    1.55 -fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
    1.56 +val remove_key = remove eq_key;
    1.57  
    1.58  
    1.59  (* tables and sets of keys *)
    1.60 @@ -70,7 +66,7 @@
    1.61  fun x mem_keys tab = isSome (Table.lookup (tab: keys, x));
    1.62  
    1.63  infix ins_keys;
    1.64 -fun x ins_keys tab = if x mem_keys tab then tab else Table.update ((x, ()), tab);
    1.65 +fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
    1.66  
    1.67  
    1.68  (* graphs *)
    1.69 @@ -146,17 +142,14 @@
    1.70  
    1.71  (* nodes *)
    1.72  
    1.73 -exception DUPLICATE of key;
    1.74 -
    1.75  fun new_node (x, info) (Graph tab) =
    1.76    Graph (Table.update_new ((x, (info, ([], []))), tab));
    1.77  
    1.78  fun del_nodes xs (Graph tab) =
    1.79 -  let
    1.80 -    fun del (x, (i, (preds, succs))) =
    1.81 -      if x mem_key xs then NONE
    1.82 -      else SOME (x, (i, (Library.foldl op del_key (preds, xs), Library.foldl op del_key (succs, xs))));
    1.83 -  in Graph (Table.make (List.mapPartial del (Table.dest tab))) end;
    1.84 +  Graph (tab
    1.85 +    |> fold Table.delete xs
    1.86 +    |> Table.map (fn (i, (preds, succs)) =>
    1.87 +      (i, (fold remove_key xs preds, fold remove_key xs succs))));
    1.88  
    1.89  
    1.90  (* edges *)
    1.91 @@ -171,8 +164,8 @@
    1.92  
    1.93  fun del_edge (x, y) G =
    1.94    if is_edge G (x, y) then
    1.95 -    G |> map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)))
    1.96 -      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y)))
    1.97 +    G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
    1.98 +      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
    1.99    else G;
   1.100  
   1.101  fun diff_edges G1 G2 =
   1.102 @@ -204,8 +197,7 @@
   1.103        [] => add_edge (x, y) G
   1.104      | cycles => raise CYCLES (map (cons x) cycles));
   1.105  
   1.106 -fun add_deps_acyclic (y, xs) G =
   1.107 -  Library.foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);
   1.108 +fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
   1.109  
   1.110  fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
   1.111  
     2.1 --- a/src/Pure/Syntax/printer.ML	Sun Apr 17 19:38:53 2005 +0200
     2.2 +++ b/src/Pure/Syntax/printer.ML	Sun Apr 17 19:39:11 2005 +0200
     2.3 @@ -250,7 +250,7 @@
     2.4    in overwrite (prtabs, (mode, tab)) end;
     2.5  
     2.6  fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m;
     2.7 -fun remove_prtabs m = change_prtabs (fn (c, prnp) => Symtab.map_entry c (remove prnp)) m;
     2.8 +fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m;
     2.9  
    2.10  fun merge_prtabs prtabs1 prtabs2 =
    2.11    let
     3.1 --- a/src/Pure/Syntax/syntax.ML	Sun Apr 17 19:38:53 2005 +0200
     3.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Apr 17 19:39:11 2005 +0200
     3.3 @@ -87,10 +87,7 @@
     3.4  fun extend_trtab name trfuns tab = Symtab.extend (tab, trfuns)
     3.5    handle Symtab.DUPS cs => err_dup_trfuns name cs;
     3.6  
     3.7 -fun remove_trtab trfuns = trfuns |> fold (fn (c, (_, s: stamp)) => fn tab =>
     3.8 -  if Option.map snd (Symtab.lookup (tab, c)) = SOME s
     3.9 -  then Symtab.delete c tab
    3.10 -  else tab);
    3.11 +fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
    3.12  
    3.13  fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
    3.14    handle Symtab.DUPS cs => err_dup_trfuns name cs;
    3.15 @@ -99,12 +96,8 @@
    3.16  (* print (ast) translations *)
    3.17  
    3.18  fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
    3.19 -
    3.20 -fun extend_tr'tab trfuns tab = foldr Symtab.update_multi tab trfuns;
    3.21 -
    3.22 -fun remove_tr'tab trfuns = trfuns |> fold (fn (c, tr) =>
    3.23 -  Symtab.map_entry c (gen_remove SynExt.eq_trfun tr));
    3.24 -
    3.25 +fun extend_tr'tab trfuns = fold_rev (curry Symtab.update_multi) trfuns;
    3.26 +fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
    3.27  fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
    3.28  
    3.29  
    3.30 @@ -138,11 +131,9 @@
    3.31  
    3.32  fun extend_tokentrtab tokentrs tabs =
    3.33    let
    3.34 -    fun ins_tokentr (ts, (m, c, f)) =
    3.35 +    fun ins_tokentr (m, c, f) ts =
    3.36        overwrite (ts, (m, ("_" ^ c, (f, stamp ())) :: assocs ts m));
    3.37 -  in
    3.38 -    merge_tokentrtabs tabs (Library.foldl ins_tokentr ([], tokentrs))
    3.39 -  end;
    3.40 +  in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end;
    3.41  
    3.42  
    3.43  
    3.44 @@ -156,10 +147,10 @@
    3.45  
    3.46  (* empty, extend, merge ruletabs *)
    3.47  
    3.48 -fun extend_ruletab rules tab =
    3.49 -  foldr Symtab.update_multi tab (map (fn r => (Ast.head_of_rule r, r)) rules);
    3.50 +val extend_ruletab =
    3.51 +  fold_rev (fn r => fn tab => Symtab.update_multi ((Ast.head_of_rule r, r), tab));
    3.52  
    3.53 -val remove_ruletab = fold (fn r => Symtab.map_entry (Ast.head_of_rule r) (remove r));
    3.54 +val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
    3.55  
    3.56  fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
    3.57  
    3.58 @@ -246,7 +237,7 @@
    3.59      val {input, lexicon, gram, consts, prmodes,
    3.60        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
    3.61        print_ast_trtab, tokentrtab, prtabs} = tabs;
    3.62 -    val input' = if inout then fold remove xprods input else input;
    3.63 +    val input' = if inout then fold (remove (op =)) xprods input else input;
    3.64    in
    3.65      Syntax {
    3.66        input = input',
    3.67 @@ -306,15 +297,14 @@
    3.68  
    3.69  
    3.70  
    3.71 -(** inspect syntax **)
    3.72 +(** print syntax **)
    3.73 +
    3.74 +local
    3.75  
    3.76  fun pretty_strs_qs name strs =
    3.77    Pretty.strs (name :: map Library.quote (sort_strings strs));
    3.78  
    3.79 -
    3.80 -(* print_gram *)
    3.81 -
    3.82 -fun print_gram (Syntax tabs) =
    3.83 +fun pretty_gram (Syntax tabs) =
    3.84    let
    3.85      val {lexicon, prmodes, gram, prtabs, ...} = tabs;
    3.86      val prmodes' = sort_strings (filter_out (equal "") prmodes);
    3.87 @@ -322,13 +312,9 @@
    3.88      [pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon),
    3.89        Pretty.big_list "prods:" (Parser.pretty_gram gram),
    3.90        pretty_strs_qs "print modes:" prmodes']
    3.91 -    |> Pretty.chunks |> Pretty.writeln
    3.92    end;
    3.93  
    3.94 -
    3.95 -(* print_trans *)
    3.96 -
    3.97 -fun print_trans (Syntax tabs) =
    3.98 +fun pretty_trans (Syntax tabs) =
    3.99    let
   3.100      fun pretty_trtab name tab =
   3.101        pretty_strs_qs name (Symtab.keys tab);
   3.102 @@ -349,13 +335,15 @@
   3.103        pretty_ruletab "print_rules:" print_ruletab,
   3.104        pretty_trtab "print_ast_translation:" print_ast_trtab,
   3.105        Pretty.big_list "token_translation:" (map pretty_tokentr tokentrtab)]
   3.106 -    |> Pretty.chunks |> Pretty.writeln
   3.107    end;
   3.108  
   3.109 +in
   3.110  
   3.111 -(* print_syntax *)
   3.112 +fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
   3.113 +fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
   3.114 +fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
   3.115  
   3.116 -fun print_syntax syn = (print_gram syn; print_trans syn);
   3.117 +end;
   3.118  
   3.119  
   3.120