# 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;