# HG changeset patch # User haftmann # Date 1125473832 -7200 # Node ID 0cfbf76ed31359365b1b51aafb18979e1b3d8257 # Parent ae9901f856aabcf2aff1688bb7f4fd11ee5f262f introduced AList.* diff -r ae9901f856aa -r 0cfbf76ed313 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Aug 31 09:01:45 2005 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Aug 31 09:37:12 2005 +0200 @@ -60,7 +60,7 @@ (used for expanding chain list)*) fun connected_with _ [] relatives = relatives | connected_with chains (root :: roots) relatives = - let val branches = (assocs chains root) \\ relatives; + let val branches = these (AList.lookup (op =) chains root) \\ relatives; in connected_with chains (branches @ roots) (branches @ relatives) end; (* convert productions to grammar; @@ -74,9 +74,9 @@ (*store chain if it does not already exist*) val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from => - let val old_tos = assocs chains from in + let val old_tos = these (AList.lookup (op =) chains from) in if lhs mem old_tos then (NONE, chains) - else (SOME from, overwrite (chains, (from, lhs ins old_tos))) + else (SOME from, AList.update (op =) (from, lhs ins old_tos) chains) end; (*propagate new chain in lookahead and lambda lists; @@ -160,10 +160,12 @@ (*associate production with new starting tokens*) fun copy [] nt_prods = nt_prods | copy (tk :: tks) nt_prods = - let val old_prods = assocs nt_prods tk; + let val old_prods = these (AList.lookup (op =) nt_prods tk); val prods' = p :: old_prods; - in copy tks (overwrite (nt_prods, (tk, prods'))) + in nt_prods + |> AList.update (op =) (tk, prods') + |> copy tks end; val nt_prods' = @@ -189,7 +191,7 @@ (*existing productions whose lookahead may depend on l*) val tk_prods = - assocs nt_prods + (these o AList.lookup (op =) nt_prods) (SOME (hd l_starts handle Empty => UnknownStart)); (*add_lambda is true if an existing production of the nt @@ -265,7 +267,7 @@ Option.map (fn x => x+1) prod_count else prod_count, is_new) | store (tk :: tks) prods is_new = - let val tk_prods = assocs prods tk; + let val tk_prods = (these o AList.lookup (op =) prods) tk; (*if prod_count = NONE then we can assume that grammar does not contain new production already*) @@ -275,9 +277,8 @@ else (new_prod :: tk_prods, true) else (new_prod :: tk_prods, true); - val prods' = if is_new' then - overwrite (prods, (tk, tk_prods')) - else prods; + val prods' = prods + |> K is_new' ? AList.update (op =) (tk, tk_prods'); in store tks prods' (is_new orelse is_new') end; val (nt_prods', prod_count', changed) = @@ -331,15 +332,17 @@ fun copy [] nt_prods = nt_prods | copy (tk :: tks) nt_prods = let - val tk_prods = assocs nt_prods (SOME tk); + val tk_prods = (these o AList.lookup (op =) nt_prods) (SOME tk); val tk_prods' = if not lambda then p :: tk_prods else p ins tk_prods; (*if production depends on lambda NT we have to look for duplicates*) - in copy tks - (overwrite (nt_prods, (SOME tk, tk_prods'))) + in + nt_prods + |> AList.update (op =) (SOME tk, tk_prods') + |> copy tks end; val result = if update then @@ -356,16 +359,15 @@ val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt); - val tk_prods = assocs nt_prods key; + val tk_prods = (these o AList.lookup (op =) nt_prods) key; (*associate productions with new lookahead tokens*) val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods); val nt_prods' = - if key = SOME UnknownStart then - overwrite (nt_prods', (key, tk_prods')) - else nt_prods'; + nt_prods' + |> (K (key = SOME UnknownStart)) ? AList.update (op =) (key, tk_prods') val added_tks = gen_rems matching_tokens (new_tks, old_tks); @@ -413,7 +415,7 @@ val nt_prods = Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @ - map prod_of_chain (assocs chains tag); + map prod_of_chain ((these o AList.lookup (op =) chains) tag); in map (pretty_prod name) nt_prods end; in List.concat (map pretty_nt taglist) end; @@ -432,8 +434,8 @@ | inverse_chains ((root, branches) :: cs) result = let fun add [] result = result | add (id :: ids) result = - let val old = assocs result id; - in add ids (overwrite (result, (id, root :: old))) end; + let val old = (these o AList.lookup (op =) result) id; + in add ids (AList.update (op =) (id, root :: old) result) end; in inverse_chains cs (add branches result) end; @@ -833,7 +835,7 @@ val (_, nt_prods) = Array.sub (prods, nt); val chained = map (fn nt => (nt, minPrec)) - (assocs chains nt); + ((these o AList.lookup (op =) chains) nt); in get_starts (chained @ nts) ((get nt_prods []) union result) end; diff -r ae9901f856aa -r 0cfbf76ed313 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Wed Aug 31 09:01:45 2005 +0200 +++ b/src/Pure/Syntax/printer.ML Wed Aug 31 09:37:12 2005 +0200 @@ -246,7 +246,7 @@ let val fmts = List.mapPartial xprod_to_fmt xprods; val tab = fold f fmts (mode_tab prtabs mode); - in overwrite (prtabs, (mode, tab)) end; + in AList.update (op =) (mode, tab) prtabs end; fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m; fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m; diff -r ae9901f856aa -r 0cfbf76ed313 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Aug 31 09:01:45 2005 +0200 +++ b/src/Pure/Syntax/syntax.ML Wed Aug 31 09:37:12 2005 +0200 @@ -108,7 +108,8 @@ (** tables of token translation functions **) fun lookup_tokentr tabs modes = - let val trs = gen_distinct eq_fst (List.concat (map (assocs tabs) (modes @ [""]))) + let val trs = gen_distinct eq_fst + (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""]))) in fn c => Option.map fst (assoc (trs, c)) end; fun merge_tokentrtabs tabs1 tabs2 = @@ -119,8 +120,8 @@ fun merge mode = let - val trs1 = assocs tabs1 mode; - val trs2 = assocs tabs2 mode; + val trs1 = (these o AList.lookup (op =) tabs1) mode; + val trs2 = (these o AList.lookup (op =) tabs2) mode; val trs = gen_distinct eq_tr (trs1 @ trs2); in (case gen_duplicates eq_fst trs of @@ -135,7 +136,7 @@ fun extend_tokentrtab tokentrs tabs = let fun ins_tokentr (m, c, f) ts = - overwrite (ts, (m, ("_" ^ c, (f, stamp ())) :: assocs ts m)); + AList.map_entry (op =) m (cons ("_" ^ c, (f, stamp ()))) ts; in merge_tokentrtabs tabs (fold ins_tokentr tokentrs []) end; diff -r ae9901f856aa -r 0cfbf76ed313 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Aug 31 09:01:45 2005 +0200 +++ b/src/Pure/Thy/thy_info.ML Wed Aug 31 09:37:12 2005 +0200 @@ -252,7 +252,7 @@ (if exists (equal path o #1) files then () else warning (loader_msg "undeclared dependency of theory" [name] ^ " on file: " ^ quote (Path.pack path)); - SOME (make_deps present outdated master (overwrite (files, (path, SOME info))))) + SOME (make_deps present outdated master (AList.update (op =) (path, SOME info) files))) | provide _ _ _ NONE = NONE; fun run_file path =