summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 06 Feb 2006 11:00:06 +0100 | |

changeset 18926 | 4227b1510552 |

parent 18925 | 2e3d508ba8dc |

child 18927 | 2e5b0f3f1418 |

clarified semantics of merge

--- a/src/Pure/General/alist.ML Sat Feb 04 03:14:32 2006 +0100 +++ b/src/Pure/General/alist.ML Mon Feb 06 11:00:06 2006 +0100 @@ -35,12 +35,12 @@ fun find_index eq xs key = let - fun find [] _ = 0 + fun find [] _ = ~1 | find ((key', value)::xs) i = if eq (key, key') then i else find xs (i+1); - in find xs 1 end; + in find xs 0 end; fun lookup _ [] _ = NONE | lookup eq ((key, value)::xs) key' = @@ -54,9 +54,9 @@ fun update eq (x as (key, value)) xs = let val i = find_index eq xs key; - fun upd 1 (_::xs) = (x::xs) + fun upd 0 (_::xs) = x :: xs | upd i (x::xs) = x :: upd (i-1) xs; - in if i = 0 then x::xs else upd i xs end; + in if i = ~1 then x::xs else upd i xs end; fun default eq (key, value) xs = if defined eq xs key then xs else (key, value)::xs; @@ -64,51 +64,43 @@ fun delete eq key xs = let val i = find_index eq xs key; - fun del 1 (_::xs) = xs + fun del 0 (_::xs) = xs | del i (x::xs) = x :: del (i-1) xs; - in if i = 0 then xs else del i xs end; + in if i = ~1 then xs else del i xs end; fun map_entry eq key f xs = let val i = find_index eq xs key; - fun mapp 1 ((x as (key, value))::xs) = (key, f value) :: xs + fun mapp 0 ((x as (key, value))::xs) = (key, f value) :: xs | mapp i (x::xs) = x :: mapp (i-1) xs; - in if i = 0 then xs else mapp i xs end; + in if i = ~1 then xs else mapp i xs end; fun map_entry_yield eq key f xs = let val i = find_index eq xs key; - fun mapp 1 ((x as (key, value))::xs) = + fun mapp 0 ((x as (key, value))::xs) = let val (r, value') = f value in (SOME r, (key, value') :: xs) end | mapp i (x::xs) = let val (r, xs') = mapp (i-1) xs in (r, x::xs') end; - in if i = 0 then (NONE, xs) else mapp i xs end; + in if i = ~1 then (NONE, xs) else mapp i xs end; exception DUP; fun join eq f (xs, ys) = let - fun add (key, x) xs = + fun add (y as (key, value)) xs = (case lookup eq xs key of - NONE => update eq (key, x) xs - | SOME y => - (case f key (y, x) of - SOME z => update eq (key, z) xs + NONE => cons y xs + | SOME value' => + (case f key (value', value) of + SOME value'' => update eq (key, value'') xs | NONE => raise DUP)); - in fold_rev add xs ys end; + in fold_rev add ys xs end; -fun merge eq_key eq_val (xs, ys) = - let - fun add (x as (key, value)) ys = - case lookup eq_key ys key - of NONE => update eq_key x ys - | SOME value' => - if eq_val (value, value') - then ys - else raise DUP; - in fold_rev add xs ys end; +fun merge eq_key eq_val = + join eq_key (K (fn (yx as (_, x)) => if eq_val yx then SOME x else NONE)); fun make keyfun = let fun keypair x = (x, keyfun x)