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