File ‹~~/src/Tools/Metis/metis.ML›
signature Metis_Random =
sig
val nextWord : unit -> word
val nextBool : unit -> bool
val nextInt : int -> int
val nextReal : unit -> real
end;
structure Metis_Random :> Metis_Random =
struct
val _ = Word.wordSize >= 30
orelse raise Fail ("Bad platform word size");
val max_word = 0wx3FFFFFFF;
val top_bit = 0wx20000000;
val a = 0w777138309;
fun step x = Word.andb (a * x + 0w1, max_word);
fun change r f = r := f (!r);
local val rand = Unsynchronized.ref 0w1
in fun nextWord () = (change rand step; ! rand) end;
fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;
val max_int = Word.toInt max_word;
fun nextInt k =
if k <= 0 orelse k > max_int then raise Fail ("next_int: out of range")
else if k = max_int then Word.toInt (nextWord ())
else Word.toInt (Word.mod (nextWord (), Word.fromInt k));
val scaling = real max_int + 1.0;
fun nextReal () = real (Word.toInt (nextWord ())) / scaling;
end;
signature Metis_Portable =
sig
val ml : string
val pointerEqual : 'a * 'a -> bool
val critical : (unit -> 'a) -> unit -> 'a
val randomBool : unit -> bool
val randomInt : int -> int
val randomReal : unit -> real
val randomWord : unit -> Word.word
val time : ('a -> 'b) -> 'a -> 'b
end
structure Metis_Portable :> Metis_Portable =
struct
val ml = "isabelle"
fun pointerEqual (x : 'a, y : 'a) = pointer_eq (x, y)
local
val lock = Thread.Mutex.mutex ();
in
fun critical e () = Multithreading.synchronized "metis" lock e
end;
val randomWord = Metis_Random.nextWord
val randomBool = Metis_Random.nextBool
val randomInt = Metis_Random.nextInt
val randomReal = Metis_Random.nextReal
fun time f x = f x
end
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a
signature Metis_Useful =
sig
exception Error of string
exception Bug of string
val total : ('a -> 'b) -> 'a -> 'b option
val can : ('a -> 'b) -> 'a -> bool
val tracePrint : (string -> unit) Unsynchronized.ref
val trace : string -> unit
val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
val I : 'a -> 'a
val K : 'a -> 'b -> 'a
val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
val W : ('a -> 'a -> 'b) -> 'a -> 'b
val funpow : int -> ('a -> 'a) -> 'a -> 'a
val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a
val fst : 'a * 'b -> 'a
val snd : 'a * 'b -> 'b
val pair : 'a -> 'b -> 'a * 'b
val swap : 'a * 'b -> 'b * 'a
val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
val ## : ('a -> 'c) * ('b -> 'd) -> 'a * 'b -> 'c * 'd
val unit : 'a -> 's -> 'a * 's
val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's
val mmap : ('a -> 'b) -> ('s -> 'a * 's) -> 's -> 'b * 's
val mjoin : ('s -> ('s -> 'a * 's) * 's) -> 's -> 'a * 's
val mwhile : ('a -> bool) -> ('a -> 's -> 'a * 's) -> 'a -> 's -> 'a * 's
val equal : ''a -> ''a -> bool
val notEqual : ''a -> ''a -> bool
val listEqual : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
val mapCompare : ('a -> 'b) -> ('b * 'b -> order) -> 'a * 'a -> order
val revCompare : ('a * 'a -> order) -> 'a * 'a -> order
val prodCompare :
('a * 'a -> order) -> ('b * 'b -> order) -> ('a * 'b) * ('a * 'b) -> order
val lexCompare : ('a * 'a -> order) -> 'a list * 'a list -> order
val optionCompare : ('a * 'a -> order) -> 'a option * 'a option -> order
val boolCompare : bool * bool -> order
val cons : 'a -> 'a list -> 'a list
val hdTl : 'a list -> 'a * 'a list
val append : 'a list -> 'a list -> 'a list
val singleton : 'a -> 'a list
val first : ('a -> 'b option) -> 'a list -> 'b option
val maps : ('a -> 's -> 'b * 's) -> 'a list -> 's -> 'b list * 's
val mapsPartial : ('a -> 's -> 'b option * 's) -> 'a list -> 's -> 'b list * 's
val zipWith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val zip : 'a list -> 'b list -> ('a * 'b) list
val unzip : ('a * 'b) list -> 'a list * 'b list
val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val cart : 'a list -> 'b list -> ('a * 'b) list
val takeWhile : ('a -> bool) -> 'a list -> 'a list
val dropWhile : ('a -> bool) -> 'a list -> 'a list
val divideWhile : ('a -> bool) -> 'a list -> 'a list * 'a list
val groups : ('a * 's -> bool * 's) -> 's -> 'a list -> 'a list list
val groupsBy : ('a * 'a -> bool) -> 'a list -> 'a list list
val groupsByFst : (''a * 'b) list -> (''a * 'b list) list
val groupsOf : int -> 'a list -> 'a list list
val index : ('a -> bool) -> 'a list -> int option
val enumerate : 'a list -> (int * 'a) list
val divide : 'a list -> int -> 'a list * 'a list
val revDivide : 'a list -> int -> 'a list * 'a list
val updateNth : int * 'a -> 'a list -> 'a list
val deleteNth : int -> 'a list -> 'a list
val mem : ''a -> ''a list -> bool
val insert : ''a -> ''a list -> ''a list
val delete : ''a -> ''a list -> ''a list
val setify : ''a list -> ''a list
val union : ''a list -> ''a list -> ''a list
val intersect : ''a list -> ''a list -> ''a list
val difference : ''a list -> ''a list -> ''a list
val subset : ''a list -> ''a list -> bool
val distinct : ''a list -> bool
val minimum : ('a * 'a -> order) -> 'a list -> 'a * 'a list
val maximum : ('a * 'a -> order) -> 'a list -> 'a * 'a list
val merge : ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
val sort : ('a * 'a -> order) -> 'a list -> 'a list
val sortMap : ('a -> 'b) -> ('b * 'b -> order) -> 'a list -> 'a list
val interval : int -> int -> int list
val divides : int -> int -> bool
val gcd : int -> int -> int
type sieve
val initSieve : sieve
val maxSieve : sieve -> int
val primesSieve : sieve -> int list
val incSieve : sieve -> bool * sieve
val nextSieve : sieve -> int * sieve
val primes : int -> int list
val primesUpTo : int -> int list
val rot : int -> char -> char
val charToInt : char -> int option
val charFromInt : int -> char option
val nChars : char -> int -> string
val chomp : string -> string
val trim : string -> string
val join : string -> string list -> string
val split : string -> string -> string list
val capitalize : string -> string
val mkPrefix : string -> string -> string
val destPrefix : string -> string -> string
val isPrefix : string -> string -> bool
val stripPrefix : (char -> bool) -> string -> string
val mkSuffix : string -> string -> string
val destSuffix : string -> string -> string
val isSuffix : string -> string -> bool
val stripSuffix : (char -> bool) -> string -> string
type columnAlignment = {leftAlign : bool, padChar : char}
val alignColumn : columnAlignment -> string list -> string list -> string list
val alignTable : columnAlignment list -> string list list -> string list
val percentToString : real -> string
val pos : real -> real
val log2 : real -> real
datatype ('a,'b) sum = Left of 'a | Right of 'b
val destLeft : ('a,'b) sum -> 'a
val isLeft : ('a,'b) sum -> bool
val destRight : ('a,'b) sum -> 'b
val isRight : ('a,'b) sum -> bool
val newInt : unit -> int
val newInts : int -> int list
val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b
val cloneArray : 'a Array.array -> 'a Array.array
val host : unit -> string
val time : unit -> string
val date : unit -> string
val readDirectory : {directory : string} -> {filename : string} list
val readTextFile : {filename : string} -> string
val writeTextFile : {contents : string, filename : string} -> unit
val try : ('a -> 'b) -> 'a -> 'b
val chat : string -> unit
val chide : string -> unit
val warn : string -> unit
val die : string -> 'exit
val timed : ('a -> 'b) -> 'a -> real * 'b
val timedMany : ('a -> 'b) -> 'a -> real * 'b
val executionTime : unit -> real
end
structure Metis_Useful :> Metis_Useful =
struct
exception Error of string;
exception Bug of string;
fun errorToStringOption err =
case err of
Error message => SOME ("Error: " ^ message)
| _ => NONE;
fun errorToString err =
case errorToStringOption err of
SOME s => "\n" ^ s ^ "\n"
| NONE => raise Bug "errorToString: not an Error exception";
fun bugToStringOption err =
case err of
Bug message => SOME ("Bug: " ^ message)
| _ => NONE;
fun bugToString err =
case bugToStringOption err of
SOME s => "\n" ^ s ^ "\n"
| NONE => raise Bug "bugToString: not a Bug exception";
fun total f x = SOME (f x) handle Error _ => NONE;
fun can f = Option.isSome o total f;
local
val traceOut = TextIO.stdOut;
fun tracePrintFn mesg =
let
val () = TextIO.output (traceOut,mesg)
val () = TextIO.flushOut traceOut
in
()
end;
in
val tracePrint = Unsynchronized.ref tracePrintFn;
end;
fun trace mesg = !tracePrint mesg;
fun C f x y = f y x;
fun I x = x;
fun K x y = x;
fun S f g x = f x (g x);
fun W f x = f x x;
fun funpow 0 _ x = x
| funpow n f x = funpow (n - 1) f (f x);
fun exp m =
let
fun f _ 0 z = z
| f x y z = f (m (x,x)) (y div 2) (if y mod 2 = 0 then z else m (z,x))
in
f
end;
fun fst (x,_) = x;
fun snd (_,y) = y;
fun pair x y = (x,y);
fun swap (x,y) = (y,x);
fun curry f x y = f (x,y);
fun uncurry f (x,y) = f x y;
val op## = fn (f,g) => fn (x,y) => (f x, g y);
val unit : 'a -> 's -> 'a * 's = pair;
fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f;
fun mmap f (m : 's -> 'a * 's) = bind m (unit o f);
fun mjoin (f : 's -> ('s -> 'a * 's) * 's) = bind f I;
fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end;
val equal = fn x => fn y => x = y;
val notEqual = fn x => fn y => x <> y;
fun listEqual xEq =
let
fun xsEq [] [] = true
| xsEq (x1 :: xs1) (x2 :: xs2) = xEq x1 x2 andalso xsEq xs1 xs2
| xsEq _ _ = false
in
xsEq
end;
fun mapCompare f cmp (a,b) = cmp (f a, f b);
fun revCompare cmp x_y =
case cmp x_y of LESS => GREATER | EQUAL => EQUAL | GREATER => LESS;
fun prodCompare xCmp yCmp ((x1,y1),(x2,y2)) =
case xCmp (x1,x2) of
LESS => LESS
| EQUAL => yCmp (y1,y2)
| GREATER => GREATER;
fun lexCompare cmp =
let
fun lex ([],[]) = EQUAL
| lex ([], _ :: _) = LESS
| lex (_ :: _, []) = GREATER
| lex (x :: xs, y :: ys) =
case cmp (x,y) of
LESS => LESS
| EQUAL => lex (xs,ys)
| GREATER => GREATER
in
lex
end;
fun optionCompare _ (NONE,NONE) = EQUAL
| optionCompare _ (NONE,_) = LESS
| optionCompare _ (_,NONE) = GREATER
| optionCompare cmp (SOME x, SOME y) = cmp (x,y);
fun boolCompare (false,true) = LESS
| boolCompare (true,false) = GREATER
| boolCompare _ = EQUAL;
fun cons x y = x :: y;
fun hdTl l = (hd l, tl l);
fun append xs ys = xs @ ys;
fun singleton a = [a];
fun first f [] = NONE
| first f (x :: xs) = (case f x of NONE => first f xs | s => s);
fun maps (_ : 'a -> 's -> 'b * 's) [] = unit []
| maps f (x :: xs) =
bind (f x) (fn y => bind (maps f xs) (fn ys => unit (y :: ys)));
fun mapsPartial (_ : 'a -> 's -> 'b option * 's) [] = unit []
| mapsPartial f (x :: xs) =
bind
(f x)
(fn yo =>
bind
(mapsPartial f xs)
(fn ys => unit (case yo of NONE => ys | SOME y => y :: ys)));
fun zipWith f =
let
fun z l [] [] = l
| z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
| z _ _ _ = raise Error "zipWith: lists different lengths";
in
fn xs => fn ys => List.rev (z [] xs ys)
end;
fun zip xs ys = zipWith pair xs ys;
local
fun inc ((x,y),(xs,ys)) = (x :: xs, y :: ys);
in
fun unzip ab = List.foldl inc ([],[]) (List.rev ab);
end;
fun cartwith f =
let
fun aux _ res _ [] = res
| aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt
| aux xsCopy res (x :: xt) (ys as y :: _) =
aux xsCopy (f x y :: res) xt ys
in
fn xs => fn ys =>
let val xs' = List.rev xs in aux xs' [] xs' (List.rev ys) end
end;
fun cart xs ys = cartwith pair xs ys;
fun takeWhile p =
let
fun f acc [] = List.rev acc
| f acc (x :: xs) = if p x then f (x :: acc) xs else List.rev acc
in
f []
end;
fun dropWhile p =
let
fun f [] = []
| f (l as x :: xs) = if p x then f xs else l
in
f
end;
fun divideWhile p =
let
fun f acc [] = (List.rev acc, [])
| f acc (l as x :: xs) = if p x then f (x :: acc) xs else (List.rev acc, l)
in
f []
end;
fun groups f =
let
fun group acc row x l =
case l of
[] =>
let
val acc = if List.null row then acc else List.rev row :: acc
in
List.rev acc
end
| h :: t =>
let
val (eor,x) = f (h,x)
in
if eor then group (List.rev row :: acc) [h] x t
else group acc (h :: row) x t
end
in
group [] []
end;
fun groupsBy eq =
let
fun f (x_y as (x,_)) = (not (eq x_y), x)
in
fn [] => []
| h :: t =>
case groups f h t of
[] => [[h]]
| hs :: ts => (h :: hs) :: ts
end;
local
fun fstEq ((x,_),(y,_)) = x = y;
fun collapse l = (fst (hd l), List.map snd l);
in
fun groupsByFst l = List.map collapse (groupsBy fstEq l);
end;
fun groupsOf n =
let
fun f (_,i) = if i = 1 then (true,n) else (false, i - 1)
in
groups f (n + 1)
end;
fun index p =
let
fun idx _ [] = NONE
| idx n (x :: xs) = if p x then SOME n else idx (n + 1) xs
in
idx 0
end;
fun enumerate l = fst (maps (fn x => fn m => ((m, x), m + 1)) l 0);
local
fun revDiv acc l 0 = (acc,l)
| revDiv _ [] _ = raise Subscript
| revDiv acc (h :: t) n = revDiv (h :: acc) t (n - 1);
in
fun revDivide l = revDiv [] l;
end;
fun divide l n = let val (a,b) = revDivide l n in (List.rev a, b) end;
fun updateNth (n,x) l =
let
val (a,b) = revDivide l n
in
case b of [] => raise Subscript | _ :: t => List.revAppend (a, x :: t)
end;
fun deleteNth n l =
let
val (a,b) = revDivide l n
in
case b of [] => raise Subscript | _ :: t => List.revAppend (a,t)
end;
fun mem x = List.exists (equal x);
fun insert x s = if mem x s then s else x :: s;
fun delete x s = List.filter (not o equal x) s;
local
fun inc (v,x) = if mem v x then x else v :: x;
in
fun setify s = List.rev (List.foldl inc [] s);
end;
fun union s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
List.foldl inc t (List.rev s)
end;
fun intersect s t =
let
fun inc (v,x) = if mem v t then v :: x else x
in
List.foldl inc [] (List.rev s)
end;
fun difference s t =
let
fun inc (v,x) = if mem v t then x else v :: x
in
List.foldl inc [] (List.rev s)
end;
fun subset s t = List.all (fn x => mem x t) s;
fun distinct [] = true
| distinct (x :: rest) = not (mem x rest) andalso distinct rest;
fun minimum cmp =
let
fun min (l,m,r) _ [] = (m, List.revAppend (l,r))
| min (best as (_,m,_)) l (x :: r) =
min (case cmp (x,m) of LESS => (l,x,r) | _ => best) (x :: l) r
in
fn [] => raise Empty
| h :: t => min ([],h,t) [h] t
end;
fun maximum cmp = minimum (revCompare cmp);
fun merge cmp =
let
fun mrg acc [] ys = List.revAppend (acc,ys)
| mrg acc xs [] = List.revAppend (acc,xs)
| mrg acc (xs as x :: xt) (ys as y :: yt) =
(case cmp (x,y) of
GREATER => mrg (y :: acc) xs yt
| _ => mrg (x :: acc) xt ys)
in
mrg []
end;
fun sort cmp =
let
fun findRuns acc r rs [] = List.rev (List.rev (r :: rs) :: acc)
| findRuns acc r rs (x :: xs) =
case cmp (r,x) of
GREATER => findRuns (List.rev (r :: rs) :: acc) x [] xs
| _ => findRuns acc x (r :: rs) xs
fun mergeAdj acc [] = List.rev acc
| mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
| mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
fun mergePairs [xs] = xs
| mergePairs l = mergePairs (mergeAdj [] l)
in
fn [] => []
| l as [_] => l
| h :: t => mergePairs (findRuns [] h [] t)
end;
fun sortMap _ _ [] = []
| sortMap _ _ (l as [_]) = l
| sortMap f cmp xs =
let
fun ncmp ((m,_),(n,_)) = cmp (m,n)
val nxs = List.map (fn x => (f x, x)) xs
val nys = sort ncmp nxs
in
List.map snd nys
end;
fun interval m 0 = []
| interval m len = m :: interval (m + 1) (len - 1);
fun divides _ 0 = true
| divides 0 _ = false
| divides a b = b mod (Int.abs a) = 0;
local
fun hcf 0 n = n
| hcf 1 _ = 1
| hcf m n = hcf (n mod m) m;
in
fun gcd m n =
let
val m = Int.abs m
and n = Int.abs n
in
if m < n then hcf m n else hcf n m
end;
end;
datatype sieve =
Sieve of
{max : int,
primes : (int * (int * int)) list};
val initSieve =
let
val n = 1
and ps = []
in
Sieve
{max = n,
primes = ps}
end;
fun maxSieve (Sieve {max = n, ...}) = n;
fun primesSieve (Sieve {primes = ps, ...}) = List.map fst ps;
fun incSieve sieve =
let
val n = maxSieve sieve + 1
fun add i ps =
case ps of
[] => (true,[(n,(0,0))])
| (p,(k,j)) :: ps =>
let
val k = (k + i) mod p
val j = j + i
in
if k = 0 then (false, (p,(k,j)) :: ps)
else
let
val (b,ps) = add j ps
in
(b, (p,(k,0)) :: ps)
end
end
val Sieve {primes = ps, ...} = sieve
val (b,ps) = add 1 ps
val sieve =
Sieve
{max = n,
primes = ps}
in
(b,sieve)
end;
fun nextSieve sieve =
let
val (b,sieve) = incSieve sieve
in
if b then (maxSieve sieve, sieve)
else nextSieve sieve
end;
local
fun inc s =
let
val (_,s) = incSieve s
in
s
end;
in
fun primesUpTo m =
if m <= 1 then []
else primesSieve (funpow (m - 1) inc initSieve);
end;
val primes =
let
fun next s n =
if n <= 0 then []
else
let
val (p,s) = nextSieve s
val n = n - 1
val ps = next s n
in
p :: ps
end
in
next initSieve
end;
local
fun len l = (length l, l)
val upper = len (String.explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
val lower = len (String.explode "abcdefghijklmnopqrstuvwxyz");
fun rotate (n,l) c k =
List.nth (l, (k + Option.valOf (index (equal c) l)) mod n);
in
fun rot k c =
if Char.isLower c then rotate lower c k
else if Char.isUpper c then rotate upper c k
else c;
end;
fun charToInt #"0" = SOME 0
| charToInt #"1" = SOME 1
| charToInt #"2" = SOME 2
| charToInt #"3" = SOME 3
| charToInt #"4" = SOME 4
| charToInt #"5" = SOME 5
| charToInt #"6" = SOME 6
| charToInt #"7" = SOME 7
| charToInt #"8" = SOME 8
| charToInt #"9" = SOME 9
| charToInt _ = NONE;
fun charFromInt 0 = SOME #"0"
| charFromInt 1 = SOME #"1"
| charFromInt 2 = SOME #"2"
| charFromInt 3 = SOME #"3"
| charFromInt 4 = SOME #"4"
| charFromInt 5 = SOME #"5"
| charFromInt 6 = SOME #"6"
| charFromInt 7 = SOME #"7"
| charFromInt 8 = SOME #"8"
| charFromInt 9 = SOME #"9"
| charFromInt _ = NONE;
fun nChars x =
let
fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
in
fn n => String.implode (dup n [])
end;
fun chomp s =
let
val n = size s
in
if n = 0 orelse String.sub (s, n - 1) <> #"\n" then s
else String.substring (s, 0, n - 1)
end;
local
fun chop l =
case l of
[] => []
| h :: t => if Char.isSpace h then chop t else l;
in
val trim = String.implode o chop o List.rev o chop o List.rev o String.explode;
end;
val join = String.concatWith;
local
fun match [] l = SOME l
| match _ [] = NONE
| match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
fun stringify acc [] = acc
| stringify acc (h :: t) = stringify (String.implode h :: acc) t;
in
fun split sep =
let
val pat = String.explode sep
fun div1 prev recent [] = stringify [] (List.rev recent :: prev)
| div1 prev recent (l as h :: t) =
case match pat l of
NONE => div1 prev (h :: recent) t
| SOME rest => div1 (List.rev recent :: prev) [] rest
in
fn s => div1 [] [] (String.explode s)
end;
end;
fun capitalize s =
if s = "" then s
else str (Char.toUpper (String.sub (s,0))) ^ String.extract (s,1,NONE);
fun mkPrefix p s = p ^ s;
fun destPrefix p =
let
fun check s =
if String.isPrefix p s then ()
else raise Error "destPrefix"
val sizeP = size p
in
fn s =>
let
val () = check s
in
String.extract (s,sizeP,NONE)
end
end;
fun isPrefix p = can (destPrefix p);
fun stripPrefix pred s =
Substring.string (Substring.dropl pred (Substring.full s));
fun mkSuffix p s = s ^ p;
fun destSuffix p =
let
fun check s =
if String.isSuffix p s then ()
else raise Error "destSuffix"
val sizeP = size p
in
fn s =>
let
val () = check s
val sizeS = size s
in
String.substring (s, 0, sizeS - sizeP)
end
end;
fun isSuffix p = can (destSuffix p);
fun stripSuffix pred s =
Substring.string (Substring.dropr pred (Substring.full s));
type columnAlignment = {leftAlign : bool, padChar : char}
fun alignColumn {leftAlign,padChar} column =
let
val (n,_) = maximum Int.compare (List.map size column)
fun pad entry row =
let
val padding = nChars padChar (n - size entry)
in
if leftAlign then entry ^ padding ^ row
else padding ^ entry ^ row
end
in
zipWith pad column
end;
local
fun alignTab aligns rows =
case aligns of
[] => List.map (K "") rows
| [{leftAlign = true, padChar = #" "}] => List.map hd rows
| align :: aligns =>
let
val col = List.map hd rows
and cols = alignTab aligns (List.map tl rows)
in
alignColumn align col cols
end;
in
fun alignTable aligns rows =
if List.null rows then [] else alignTab aligns rows;
end;
val realToString = Real.toString;
fun percentToString x = Int.toString (Real.round (100.0 * x)) ^ "%";
fun pos r = Real.max (r,0.0);
local
val invLn2 = 1.0 / Math.ln 2.0;
in
fun log2 x = invLn2 * Math.ln x;
end;
datatype ('a,'b) sum = Left of 'a | Right of 'b
fun destLeft (Left l) = l
| destLeft _ = raise Error "destLeft";
fun isLeft (Left _) = true
| isLeft (Right _) = false;
fun destRight (Right r) = r
| destRight _ = raise Error "destRight";
fun isRight (Left _) = false
| isRight (Right _) = true;
local
val generator = Unsynchronized.ref 0
fun newIntThunk () =
let
val n = !generator
val () = generator := n + 1
in
n
end;
fun newIntsThunk k () =
let
val n = !generator
val () = generator := n + k
in
interval n k
end;
in
fun newInt () = Metis_Portable.critical newIntThunk ();
fun newInts k =
if k <= 0 then []
else Metis_Portable.critical (newIntsThunk k) ();
end;
fun withRef (r,new) f x =
let
val old = !r
val () = r := new
val y = f x handle e => (r := old; raise e)
val () = r := old
in
y
end;
fun cloneArray a =
let
fun index i = Array.sub (a,i)
in
Array.tabulate (Array.length a, index)
end;
fun host () = Option.getOpt (OS.Process.getEnv "HOSTNAME", "unknown");
fun time () = Date.fmt "%H:%M:%S" (Date.fromTimeLocal (Time.now ()));
fun date () = Date.fmt "%d/%m/%Y" (Date.fromTimeLocal (Time.now ()));
fun readDirectory {directory = dir} =
let
val dirStrm = OS.FileSys.openDir dir
fun readAll acc =
case OS.FileSys.readDir dirStrm of
NONE => acc
| SOME file =>
let
val filename = OS.Path.joinDirFile {dir = dir, file = file}
val acc = {filename = filename} :: acc
in
readAll acc
end
val filenames = readAll []
val () = OS.FileSys.closeDir dirStrm
in
List.rev filenames
end;
fun readTextFile {filename} =
let
open TextIO
val h = openIn filename
val contents = inputAll h
val () = closeIn h
in
contents
end;
fun writeTextFile {contents,filename} =
let
open TextIO
val h = openOut filename
val () = output (h,contents)
val () = closeOut h
in
()
end;
fun chat s = TextIO.output (TextIO.stdOut, s ^ "\n");
fun chide s = TextIO.output (TextIO.stdErr, s ^ "\n");
local
fun err x s = chide (x ^ ": " ^ s);
in
fun try f x = f x
handle e as Error _ => (err "try" (errorToString e); raise e)
| e as Bug _ => (err "try" (bugToString e); raise e)
| e => (err "try" "strange exception raised"; raise e);
val warn = err "WARNING";
fun die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure);
end;
fun timed f a =
let
val tmr = Timer.startCPUTimer ()
val res = f a
val {usr,sys,...} = Timer.checkCPUTimer tmr
in
(Time.toReal usr + Time.toReal sys, res)
end;
local
val MIN = 1.0;
fun several n t f a =
let
val (t',res) = timed f a
val t = t + t'
val n = n + 1
in
if t > MIN then (t / Real.fromInt n, res) else several n t f a
end;
in
fun timedMany f a = several 0 0.0 f a
end;
val executionTime =
let
val startTime = Time.toReal (Time.now ())
in
fn () => Time.toReal (Time.now ()) - startTime
end;
end
signature Metis_Lazy =
sig
type 'a lazy
val quickly : 'a -> 'a lazy
val delay : (unit -> 'a) -> 'a lazy
val force : 'a lazy -> 'a
val memoize : (unit -> 'a) -> unit -> 'a
end
structure Metis_Lazy :> Metis_Lazy =
struct
datatype 'a thunk =
Value of 'a
| Thunk of unit -> 'a;
datatype 'a lazy = Metis_Lazy of 'a thunk Unsynchronized.ref;
fun quickly v = Metis_Lazy (Unsynchronized.ref (Value v));
fun delay f = Metis_Lazy (Unsynchronized.ref (Thunk f));
fun force (Metis_Lazy s) =
case !s of
Value v => v
| Thunk f =>
let
val v = f ()
val () = s := Value v
in
v
end;
fun memoize f =
let
val t = delay f
in
fn () => force t
end;
end
signature Metis_Ordered =
sig
type t
val compare : t * t -> order
end
structure Metis_IntOrdered =
struct type t = int val compare = Int.compare end;
structure Metis_IntPairOrdered =
struct
type t = int * int;
fun compare ((i1,j1),(i2,j2)) =
case Int.compare (i1,i2) of
LESS => LESS
| EQUAL => Int.compare (j1,j2)
| GREATER => GREATER;
end;
structure Metis_StringOrdered =
struct type t = string val compare = String.compare end;
signature Metis_Map =
sig
type ('key,'a) map
val new : ('key * 'key -> order) -> ('key,'a) map
val singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map
val null : ('key,'a) map -> bool
val size : ('key,'a) map -> int
val peekKey : ('key,'a) map -> 'key -> ('key * 'a) option
val peek : ('key,'a) map -> 'key -> 'a option
val get : ('key,'a) map -> 'key -> 'a
val pick : ('key,'a) map -> 'key * 'a
val nth : ('key,'a) map -> int -> 'key * 'a
val random : ('key,'a) map -> 'key * 'a
val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map
val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map
val delete : ('key,'a) map -> 'key -> ('key,'a) map
val remove : ('key,'a) map -> 'key -> ('key,'a) map
val deletePick : ('key,'a) map -> ('key * 'a) * ('key,'a) map
val deleteNth : ('key,'a) map -> int -> ('key * 'a) * ('key,'a) map
val deleteRandom : ('key,'a) map -> ('key * 'a) * ('key,'a) map
val merge :
{first : 'key * 'a -> 'c option,
second : 'key * 'b -> 'c option,
both : ('key * 'a) * ('key * 'b) -> 'c option} ->
('key,'a) map -> ('key,'b) map -> ('key,'c) map
val union :
(('key * 'a) * ('key * 'a) -> 'a option) ->
('key,'a) map -> ('key,'a) map -> ('key,'a) map
val intersect :
(('key * 'a) * ('key * 'b) -> 'c option) ->
('key,'a) map -> ('key,'b) map -> ('key,'c) map
val inDomain : 'key -> ('key,'a) map -> bool
val unionDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
val unionListDomain : ('key,'a) map list -> ('key,'a) map
val intersectDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
val intersectListDomain : ('key,'a) map list -> ('key,'a) map
val differenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
val symmetricDifferenceDomain : ('key,'a) map -> ('key,'a) map -> ('key,'a) map
val equalDomain : ('key,'a) map -> ('key,'a) map -> bool
val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool
val disjointDomain : ('key,'a) map -> ('key,'a) map -> bool
val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map
val map : ('key * 'a -> 'b) -> ('key,'a) map -> ('key,'b) map
val app : ('key * 'a -> unit) -> ('key,'a) map -> unit
val transform : ('a -> 'b) -> ('key,'a) map -> ('key,'b) map
val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map
val partition :
('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map * ('key,'a) map
val foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
val findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
val firstl : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
val firstr : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool
val all : ('key * 'a -> bool) -> ('key,'a) map -> bool
val count : ('key * 'a -> bool) -> ('key,'a) map -> int
val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order
val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
val keys : ('key,'a) map -> 'key list
val values : ('key,'a) map -> 'a list
val toList : ('key,'a) map -> ('key * 'a) list
val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map
val toString : ('key,'a) map -> string
type ('key,'a) iterator
val mkIterator : ('key,'a) map -> ('key,'a) iterator option
val mkRevIterator : ('key,'a) map -> ('key,'a) iterator option
val readIterator : ('key,'a) iterator -> 'key * 'a
val advanceIterator : ('key,'a) iterator -> ('key,'a) iterator option
end
structure Metis_Map :> Metis_Map =
struct
exception Bug = Metis_Useful.Bug;
exception Error = Metis_Useful.Error;
val pointerEqual = Metis_Portable.pointerEqual;
val K = Metis_Useful.K;
val randomInt = Metis_Portable.randomInt;
val randomWord = Metis_Portable.randomWord;
fun equalKey compareKey key1 key2 = compareKey (key1,key2) = EQUAL;
type priority = Word.word;
val randomPriority = randomWord;
val comparePriority = Word.compare;
datatype ('key,'value) tree =
E
| T of ('key,'value) node
and ('key,'value) node =
Node of
{size : int,
priority : priority,
left : ('key,'value) tree,
key : 'key,
value : 'value,
right : ('key,'value) tree};
fun lowerPriorityNode node1 node2 =
let
val Node {priority = p1, ...} = node1
and Node {priority = p2, ...} = node2
in
comparePriority (p1,p2) = LESS
end;
fun treeNew () = E;
fun nodeSize (Node {size = x, ...}) = x;
fun treeSize tree =
case tree of
E => 0
| T x => nodeSize x;
fun mkNode priority left key value right =
let
val size = treeSize left + 1 + treeSize right
in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
end;
fun mkTree priority left key value right =
let
val node = mkNode priority left key value right
in
T node
end;
fun treeLeftSpine acc tree =
case tree of
E => acc
| T node => nodeLeftSpine acc node
and nodeLeftSpine acc node =
let
val Node {left,...} = node
in
treeLeftSpine (node :: acc) left
end;
fun treeRightSpine acc tree =
case tree of
E => acc
| T node => nodeRightSpine acc node
and nodeRightSpine acc node =
let
val Node {right,...} = node
in
treeRightSpine (node :: acc) right
end;
fun mkNodeSingleton priority key value =
let
val size = 1
and left = E
and right = E
in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
end;
fun nodeSingleton (key,value) =
let
val priority = randomPriority ()
in
mkNodeSingleton priority key value
end;
fun treeSingleton key_value =
let
val node = nodeSingleton key_value
in
T node
end;
fun treeAppend tree1 tree2 =
case tree1 of
E => tree2
| T node1 =>
case tree2 of
E => tree1
| T node2 =>
if lowerPriorityNode node1 node2 then
let
val Node {priority,left,key,value,right,...} = node2
val left = treeAppend tree1 left
in
mkTree priority left key value right
end
else
let
val Node {priority,left,key,value,right,...} = node1
val right = treeAppend right tree2
in
mkTree priority left key value right
end;
fun treeCombine left node right =
let
val left_node = treeAppend left (T node)
in
treeAppend left_node right
end;
fun treePeek compareKey pkey tree =
case tree of
E => NONE
| T node => nodePeek compareKey pkey node
and nodePeek compareKey pkey node =
let
val Node {left,key,value,right,...} = node
in
case compareKey (pkey,key) of
LESS => treePeek compareKey pkey left
| EQUAL => SOME value
| GREATER => treePeek compareKey pkey right
end;
fun treePeekPath compareKey pkey path tree =
case tree of
E => (path,NONE)
| T node => nodePeekPath compareKey pkey path node
and nodePeekPath compareKey pkey path node =
let
val Node {left,key,right,...} = node
in
case compareKey (pkey,key) of
LESS => treePeekPath compareKey pkey ((true,node) :: path) left
| EQUAL => (path, SOME node)
| GREATER => treePeekPath compareKey pkey ((false,node) :: path) right
end;
fun addSidePath ((wentLeft,node),(leftTree,rightTree)) =
let
val Node {priority,left,key,value,right,...} = node
in
if wentLeft then (leftTree, mkTree priority rightTree key value right)
else (mkTree priority left key value leftTree, rightTree)
end;
fun addSidesPath left_right = List.foldl addSidePath left_right;
fun mkSidesPath path = addSidesPath (E,E) path;
local
fun updateTree ((wentLeft,node),tree) =
let
val Node {priority,left,key,value,right,...} = node
in
if wentLeft then mkTree priority tree key value right
else mkTree priority left key value tree
end;
in
fun updateTreePath tree = List.foldl updateTree tree;
end;
fun insertNodePath node =
let
fun insert left_right path =
case path of
[] =>
let
val (left,right) = left_right
in
treeCombine left node right
end
| (step as (_,snode)) :: rest =>
if lowerPriorityNode snode node then
let
val left_right = addSidePath (step,left_right)
in
insert left_right rest
end
else
let
val (left,right) = left_right
val tree = treeCombine left node right
in
updateTreePath tree path
end
in
insert (E,E)
end;
fun nodePartition compareKey pkey node =
let
val (path,pnode) = nodePeekPath compareKey pkey [] node
in
case pnode of
NONE =>
let
val (left,right) = mkSidesPath path
in
(left,NONE,right)
end
| SOME node =>
let
val Node {left,key,value,right,...} = node
val (left,right) = addSidesPath (left,right) path
in
(left, SOME (key,value), right)
end
end;
fun treePeekKey compareKey pkey tree =
case tree of
E => NONE
| T node => nodePeekKey compareKey pkey node
and nodePeekKey compareKey pkey node =
let
val Node {left,key,value,right,...} = node
in
case compareKey (pkey,key) of
LESS => treePeekKey compareKey pkey left
| EQUAL => SOME (key,value)
| GREATER => treePeekKey compareKey pkey right
end;
fun treeInsert compareKey key_value tree =
let
val (key,value) = key_value
val (path,inode) = treePeekPath compareKey key [] tree
in
case inode of
NONE =>
let
val node = nodeSingleton (key,value)
in
insertNodePath node path
end
| SOME node =>
let
val Node {size,priority,left,right,...} = node
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
updateTreePath (T node) path
end
end;
fun treeDelete compareKey dkey tree =
case tree of
E => raise Bug "Metis_Map.delete: element not found"
| T node => nodeDelete compareKey dkey node
and nodeDelete compareKey dkey node =
let
val Node {size,priority,left,key,value,right} = node
in
case compareKey (dkey,key) of
LESS =>
let
val size = size - 1
and left = treeDelete compareKey dkey left
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
T node
end
| EQUAL => treeAppend left right
| GREATER =>
let
val size = size - 1
and right = treeDelete compareKey dkey right
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
T node
end
end;
fun treeMapPartial f tree =
case tree of
E => E
| T node => nodeMapPartial f node
and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
let
val left = treeMapPartial f left
and vo = f (key,value)
and right = treeMapPartial f right
in
case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right
end;
fun treeMap f tree =
case tree of
E => E
| T node => T (nodeMap f node)
and nodeMap f node =
let
val Node {size,priority,left,key,value,right} = node
val left = treeMap f left
and value = f (key,value)
and right = treeMap f right
in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
end;
fun treeMerge compareKey f1 f2 fb tree1 tree2 =
case tree1 of
E => treeMapPartial f2 tree2
| T node1 =>
case tree2 of
E => treeMapPartial f1 tree1
| T node2 => nodeMerge compareKey f1 f2 fb node1 node2
and nodeMerge compareKey f1 f2 fb node1 node2 =
let
val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition compareKey key node1
val left = treeMerge compareKey f1 f2 fb l left
and right = treeMerge compareKey f1 f2 fb r right
val vo =
case kvo of
NONE => f2 (key,value)
| SOME kv => fb (kv,(key,value))
in
case vo of
NONE => treeAppend left right
| SOME value =>
let
val node = mkNodeSingleton priority key value
in
treeCombine left node right
end
end;
fun treeUnion compareKey f f2 tree1 tree2 =
case tree1 of
E => tree2
| T node1 =>
case tree2 of
E => tree1
| T node2 => nodeUnion compareKey f f2 node1 node2
and nodeUnion compareKey f f2 node1 node2 =
if pointerEqual (node1,node2) then nodeMapPartial f2 node1
else
let
val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition compareKey key node1
val left = treeUnion compareKey f f2 l left
and right = treeUnion compareKey f f2 r right
val vo =
case kvo of
NONE => SOME value
| SOME kv => f (kv,(key,value))
in
case vo of
NONE => treeAppend left right
| SOME value =>
let
val node = mkNodeSingleton priority key value
in
treeCombine left node right
end
end;
fun treeIntersect compareKey f t1 t2 =
case t1 of
E => E
| T n1 =>
case t2 of
E => E
| T n2 => nodeIntersect compareKey f n1 n2
and nodeIntersect compareKey f n1 n2 =
let
val Node {priority,left,key,value,right,...} = n2
val (l,kvo,r) = nodePartition compareKey key n1
val left = treeIntersect compareKey f l left
and right = treeIntersect compareKey f r right
val vo =
case kvo of
NONE => NONE
| SOME kv => f (kv,(key,value))
in
case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right
end;
fun treeUnionDomain compareKey tree1 tree2 =
case tree1 of
E => tree2
| T node1 =>
case tree2 of
E => tree1
| T node2 =>
if pointerEqual (node1,node2) then tree2
else nodeUnionDomain compareKey node1 node2
and nodeUnionDomain compareKey node1 node2 =
let
val Node {priority,left,key,value,right,...} = node2
val (l,_,r) = nodePartition compareKey key node1
val left = treeUnionDomain compareKey l left
and right = treeUnionDomain compareKey r right
val node = mkNodeSingleton priority key value
in
treeCombine left node right
end;
fun treeIntersectDomain compareKey tree1 tree2 =
case tree1 of
E => E
| T node1 =>
case tree2 of
E => E
| T node2 =>
if pointerEqual (node1,node2) then tree2
else nodeIntersectDomain compareKey node1 node2
and nodeIntersectDomain compareKey node1 node2 =
let
val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition compareKey key node1
val left = treeIntersectDomain compareKey l left
and right = treeIntersectDomain compareKey r right
in
if Option.isSome kvo then mkTree priority left key value right
else treeAppend left right
end;
fun treeDifferenceDomain compareKey t1 t2 =
case t1 of
E => E
| T n1 =>
case t2 of
E => t1
| T n2 => nodeDifferenceDomain compareKey n1 n2
and nodeDifferenceDomain compareKey n1 n2 =
if pointerEqual (n1,n2) then E
else
let
val Node {priority,left,key,value,right,...} = n1
val (l,kvo,r) = nodePartition compareKey key n2
val left = treeDifferenceDomain compareKey left l
and right = treeDifferenceDomain compareKey right r
in
if Option.isSome kvo then treeAppend left right
else mkTree priority left key value right
end;
fun treeSubsetDomain compareKey tree1 tree2 =
case tree1 of
E => true
| T node1 =>
case tree2 of
E => false
| T node2 => nodeSubsetDomain compareKey node1 node2
and nodeSubsetDomain compareKey node1 node2 =
pointerEqual (node1,node2) orelse
let
val Node {size,left,key,right,...} = node1
in
size <= nodeSize node2 andalso
let
val (l,kvo,r) = nodePartition compareKey key node2
in
Option.isSome kvo andalso
treeSubsetDomain compareKey left l andalso
treeSubsetDomain compareKey right r
end
end;
fun nodePick node =
let
val Node {key,value,...} = node
in
(key,value)
end;
fun treePick tree =
case tree of
E => raise Bug "Metis_Map.treePick"
| T node => nodePick node;
fun nodeDeletePick node =
let
val Node {left,key,value,right,...} = node
in
((key,value), treeAppend left right)
end;
fun treeDeletePick tree =
case tree of
E => raise Bug "Metis_Map.treeDeletePick"
| T node => nodeDeletePick node;
fun treeNth n tree =
case tree of
E => raise Bug "Metis_Map.treeNth"
| T node => nodeNth n node
and nodeNth n node =
let
val Node {left,key,value,right,...} = node
val k = treeSize left
in
if n = k then (key,value)
else if n < k then treeNth n left
else treeNth (n - (k + 1)) right
end;
fun treeDeleteNth n tree =
case tree of
E => raise Bug "Metis_Map.treeDeleteNth"
| T node => nodeDeleteNth n node
and nodeDeleteNth n node =
let
val Node {size,priority,left,key,value,right} = node
val k = treeSize left
in
if n = k then ((key,value), treeAppend left right)
else if n < k then
let
val (key_value,left) = treeDeleteNth n left
val size = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
(key_value, T node)
end
else
let
val n = n - (k + 1)
val (key_value,right) = treeDeleteNth n right
val size = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
(key_value, T node)
end
end;
datatype ('key,'value) iterator =
LeftToRightIterator of
('key * 'value) * ('key,'value) tree * ('key,'value) node list
| RightToLeftIterator of
('key * 'value) * ('key,'value) tree * ('key,'value) node list;
fun fromSpineLeftToRightIterator nodes =
case nodes of
[] => NONE
| Node {key,value,right,...} :: nodes =>
SOME (LeftToRightIterator ((key,value),right,nodes));
fun fromSpineRightToLeftIterator nodes =
case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
SOME (RightToLeftIterator ((key,value),left,nodes));
fun addLeftToRightIterator nodes tree = fromSpineLeftToRightIterator (treeLeftSpine nodes tree);
fun addRightToLeftIterator nodes tree = fromSpineRightToLeftIterator (treeRightSpine nodes tree);
fun treeMkIterator tree = addLeftToRightIterator [] tree;
fun treeMkRevIterator tree = addRightToLeftIterator [] tree;
fun readIterator iter =
case iter of
LeftToRightIterator (key_value,_,_) => key_value
| RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter =
case iter of
LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
| RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io =
case io of
NONE => acc
| SOME iter =>
let
val (key,value) = readIterator iter
in
foldIterator f (f (key,value,acc)) (advanceIterator iter)
end;
fun findIterator pred io =
case io of
NONE => NONE
| SOME iter =>
let
val key_value = readIterator iter
in
if pred key_value then SOME key_value
else findIterator pred (advanceIterator iter)
end;
fun firstIterator f io =
case io of
NONE => NONE
| SOME iter =>
let
val key_value = readIterator iter
in
case f key_value of
NONE => firstIterator f (advanceIterator iter)
| s => s
end;
fun compareIterator compareKey compareValue io1 io2 =
case (io1,io2) of
(NONE,NONE) => EQUAL
| (NONE, SOME _) => LESS
| (SOME _, NONE) => GREATER
| (SOME i1, SOME i2) =>
let
val (k1,v1) = readIterator i1
and (k2,v2) = readIterator i2
in
case compareKey (k1,k2) of
LESS => LESS
| EQUAL =>
(case compareValue (v1,v2) of
LESS => LESS
| EQUAL =>
let
val io1 = advanceIterator i1
and io2 = advanceIterator i2
in
compareIterator compareKey compareValue io1 io2
end
| GREATER => GREATER)
| GREATER => GREATER
end;
fun equalIterator equalKey equalValue io1 io2 =
case (io1,io2) of
(NONE,NONE) => true
| (NONE, SOME _) => false
| (SOME _, NONE) => false
| (SOME i1, SOME i2) =>
let
val (k1,v1) = readIterator i1
and (k2,v2) = readIterator i2
in
equalKey k1 k2 andalso
equalValue v1 v2 andalso
let
val io1 = advanceIterator i1
and io2 = advanceIterator i2
in
equalIterator equalKey equalValue io1 io2
end
end;
datatype ('key,'value) map =
Metis_Map of ('key * 'key -> order) * ('key,'value) tree;
fun new compareKey =
let
val tree = treeNew ()
in
Metis_Map (compareKey,tree)
end;
fun singleton compareKey key_value =
let
val tree = treeSingleton key_value
in
Metis_Map (compareKey,tree)
end;
fun size (Metis_Map (_,tree)) = treeSize tree;
fun null m = size m = 0;
fun peekKey (Metis_Map (compareKey,tree)) key = treePeekKey compareKey key tree;
fun peek (Metis_Map (compareKey,tree)) key = treePeek compareKey key tree;
fun inDomain key m = Option.isSome (peek m key);
fun get m key =
case peek m key of
NONE => raise Error "Metis_Map.get: element not found"
| SOME value => value;
fun pick (Metis_Map (_,tree)) = treePick tree;
fun nth (Metis_Map (_,tree)) n = treeNth n tree;
fun random m =
let
val n = size m
in
if n = 0 then raise Bug "Metis_Map.random: empty"
else nth m (randomInt n)
end;
fun insert (Metis_Map (compareKey,tree)) key_value =
let
val tree = treeInsert compareKey key_value tree
in
Metis_Map (compareKey,tree)
end;
fun insertList m =
let
fun ins (key_value,acc) = insert acc key_value
in
List.foldl ins m
end;
fun delete (Metis_Map (compareKey,tree)) dkey =
let
val tree = treeDelete compareKey dkey tree
in
Metis_Map (compareKey,tree)
end;
fun remove m key = if inDomain key m then delete m key else m;
fun deletePick (Metis_Map (compareKey,tree)) =
let
val (key_value,tree) = treeDeletePick tree
in
(key_value, Metis_Map (compareKey,tree))
end;
fun deleteNth (Metis_Map (compareKey,tree)) n =
let
val (key_value,tree) = treeDeleteNth n tree
in
(key_value, Metis_Map (compareKey,tree))
end;
fun deleteRandom m =
let
val n = size m
in
if n = 0 then raise Bug "Metis_Map.deleteRandom: empty"
else deleteNth m (randomInt n)
end;
fun merge {first,second,both} (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
let
val tree = treeMerge compareKey first second both tree1 tree2
in
Metis_Map (compareKey,tree)
end;
fun union f (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
let
fun f2 kv = f (kv,kv)
val tree = treeUnion compareKey f f2 tree1 tree2
in
Metis_Map (compareKey,tree)
end;
fun intersect f (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
let
val tree = treeIntersect compareKey f tree1 tree2
in
Metis_Map (compareKey,tree)
end;
fun mkIterator (Metis_Map (_,tree)) = treeMkIterator tree;
fun mkRevIterator (Metis_Map (_,tree)) = treeMkRevIterator tree;
fun mapPartial f (Metis_Map (compareKey,tree)) =
let
val tree = treeMapPartial f tree
in
Metis_Map (compareKey,tree)
end;
fun map f (Metis_Map (compareKey,tree)) =
let
val tree = treeMap f tree
in
Metis_Map (compareKey,tree)
end;
fun transform f = map (fn (_,value) => f value);
fun filter pred =
let
fun f (key_value as (_,value)) =
if pred key_value then SOME value else NONE
in
mapPartial f
end;
fun partition p =
let
fun np x = not (p x)
in
fn m => (filter p m, filter np m)
end;
fun foldl f b m = foldIterator f b (mkIterator m);
fun foldr f b m = foldIterator f b (mkRevIterator m);
fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
fun findl p m = findIterator p (mkIterator m);
fun findr p m = findIterator p (mkRevIterator m);
fun firstl f m = firstIterator f (mkIterator m);
fun firstr f m = firstIterator f (mkRevIterator m);
fun exists p m = Option.isSome (findl p m);
fun all p =
let
fun np x = not (p x)
in
fn m => not (exists np m)
end;
fun count pred =
let
fun f (k,v,acc) = if pred (k,v) then acc + 1 else acc
in
foldl f 0
end;
fun compare compareValue (m1,m2) =
if pointerEqual (m1,m2) then EQUAL
else
case Int.compare (size m1, size m2) of
LESS => LESS
| EQUAL =>
let
val Metis_Map (compareKey,_) = m1
val io1 = mkIterator m1
and io2 = mkIterator m2
in
compareIterator compareKey compareValue io1 io2
end
| GREATER => GREATER;
fun equal equalValue m1 m2 =
pointerEqual (m1,m2) orelse
(size m1 = size m2 andalso
let
val Metis_Map (compareKey,_) = m1
val io1 = mkIterator m1
and io2 = mkIterator m2
in
equalIterator (equalKey compareKey) equalValue io1 io2
end);
fun unionDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
let
val tree = treeUnionDomain compareKey tree1 tree2
in
Metis_Map (compareKey,tree)
end;
local
fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
in
fun unionListDomain ms =
case ms of
[] => raise Bug "Metis_Map.unionListDomain: no sets"
| m :: ms => List.foldl uncurriedUnionDomain m ms;
end;
fun intersectDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
let
val tree = treeIntersectDomain compareKey tree1 tree2
in
Metis_Map (compareKey,tree)
end;
local
fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
in
fun intersectListDomain ms =
case ms of
[] => raise Bug "Metis_Map.intersectListDomain: no sets"
| m :: ms => List.foldl uncurriedIntersectDomain m ms;
end;
fun differenceDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
let
val tree = treeDifferenceDomain compareKey tree1 tree2
in
Metis_Map (compareKey,tree)
end;
fun symmetricDifferenceDomain m1 m2 =
unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);
fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
fun subsetDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
treeSubsetDomain compareKey tree1 tree2;
fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
fun values m = foldr (fn (_,value,l) => value :: l) [] m;
fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
fun fromList compareKey l =
let
val m = new compareKey
in
insertList m l
end;
fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
end
signature Metis_KeyMap =
sig
type key
val compareKey : key * key -> order
val equalKey : key -> key -> bool
type 'a map
val new : unit -> 'a map
val singleton : key * 'a -> 'a map
val null : 'a map -> bool
val size : 'a map -> int
val peekKey : 'a map -> key -> (key * 'a) option
val peek : 'a map -> key -> 'a option
val get : 'a map -> key -> 'a
val pick : 'a map -> key * 'a
val nth : 'a map -> int -> key * 'a
val random : 'a map -> key * 'a
val insert : 'a map -> key * 'a -> 'a map
val insertList : 'a map -> (key * 'a) list -> 'a map
val delete : 'a map -> key -> 'a map
val remove : 'a map -> key -> 'a map
val deletePick : 'a map -> (key * 'a) * 'a map
val deleteNth : 'a map -> int -> (key * 'a) * 'a map
val deleteRandom : 'a map -> (key * 'a) * 'a map
val merge :
{first : key * 'a -> 'c option,
second : key * 'b -> 'c option,
both : (key * 'a) * (key * 'b) -> 'c option} ->
'a map -> 'b map -> 'c map
val union :
((key * 'a) * (key * 'a) -> 'a option) ->
'a map -> 'a map -> 'a map
val intersect :
((key * 'a) * (key * 'b) -> 'c option) ->
'a map -> 'b map -> 'c map
val inDomain : key -> 'a map -> bool
val unionDomain : 'a map -> 'a map -> 'a map
val unionListDomain : 'a map list -> 'a map
val intersectDomain : 'a map -> 'a map -> 'a map
val intersectListDomain : 'a map list -> 'a map
val differenceDomain : 'a map -> 'a map -> 'a map
val symmetricDifferenceDomain : 'a map -> 'a map -> 'a map
val equalDomain : 'a map -> 'a map -> bool
val subsetDomain : 'a map -> 'a map -> bool
val disjointDomain : 'a map -> 'a map -> bool
val mapPartial : (key * 'a -> 'b option) -> 'a map -> 'b map
val map : (key * 'a -> 'b) -> 'a map -> 'b map
val app : (key * 'a -> unit) -> 'a map -> unit
val transform : ('a -> 'b) -> 'a map -> 'b map
val filter : (key * 'a -> bool) -> 'a map -> 'a map
val partition :
(key * 'a -> bool) -> 'a map -> 'a map * 'a map
val foldl : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
val foldr : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
val findl : (key * 'a -> bool) -> 'a map -> (key * 'a) option
val findr : (key * 'a -> bool) -> 'a map -> (key * 'a) option
val firstl : (key * 'a -> 'b option) -> 'a map -> 'b option
val firstr : (key * 'a -> 'b option) -> 'a map -> 'b option
val exists : (key * 'a -> bool) -> 'a map -> bool
val all : (key * 'a -> bool) -> 'a map -> bool
val count : (key * 'a -> bool) -> 'a map -> int
val compare : ('a * 'a -> order) -> 'a map * 'a map -> order
val equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
val keys : 'a map -> key list
val values : 'a map -> 'a list
val toList : 'a map -> (key * 'a) list
val fromList : (key * 'a) list -> 'a map
val toString : 'a map -> string
type 'a iterator
val mkIterator : 'a map -> 'a iterator option
val mkRevIterator : 'a map -> 'a iterator option
val readIterator : 'a iterator -> key * 'a
val advanceIterator : 'a iterator -> 'a iterator option
end
functor Metis_KeyMap (Key : Metis_Ordered) :> Metis_KeyMap where type key = Key.t =
struct
type key = Key.t;
val compareKey = Key.compare;
exception Bug = Metis_Useful.Bug;
exception Error = Metis_Useful.Error;
val pointerEqual = Metis_Portable.pointerEqual;
val K = Metis_Useful.K;
val randomInt = Metis_Portable.randomInt;
val randomWord = Metis_Portable.randomWord;
fun equalKey key1 key2 = compareKey (key1,key2) = EQUAL;
type priority = Word.word;
val randomPriority = randomWord;
val comparePriority = Word.compare;
datatype 'value tree =
E
| T of 'value node
and 'value node =
Node of
{size : int,
priority : priority,
left : 'value tree,
key : key,
value : 'value,
right : 'value tree};
fun lowerPriorityNode node1 node2 =
let
val Node {priority = p1, ...} = node1
and Node {priority = p2, ...} = node2
in
comparePriority (p1,p2) = LESS
end;
fun treeNew () = E;
fun nodeSize (Node {size = x, ...}) = x;
fun treeSize tree =
case tree of
E => 0
| T x => nodeSize x;
fun mkNode priority left key value right =
let
val size = treeSize left + 1 + treeSize right
in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
end;
fun mkTree priority left key value right =
let
val node = mkNode priority left key value right
in
T node
end;
fun treeLeftSpine acc tree =
case tree of
E => acc
| T node => nodeLeftSpine acc node
and nodeLeftSpine acc node =
let
val Node {left,...} = node
in
treeLeftSpine (node :: acc) left
end;
fun treeRightSpine acc tree =
case tree of
E => acc
| T node => nodeRightSpine acc node
and nodeRightSpine acc node =
let
val Node {right,...} = node
in
treeRightSpine (node :: acc) right
end;
fun mkNodeSingleton priority key value =
let
val size = 1
and left = E
and right = E
in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
end;
fun nodeSingleton (key,value) =
let
val priority = randomPriority ()
in
mkNodeSingleton priority key value
end;
fun treeSingleton key_value =
let
val node = nodeSingleton key_value
in
T node
end;
fun treeAppend tree1 tree2 =
case tree1 of
E => tree2
| T node1 =>
case tree2 of
E => tree1
| T node2 =>
if lowerPriorityNode node1 node2 then
let
val Node {priority,left,key,value,right,...} = node2
val left = treeAppend tree1 left
in
mkTree priority left key value right
end
else
let
val Node {priority,left,key,value,right,...} = node1
val right = treeAppend right tree2
in
mkTree priority left key value right
end;
fun treeCombine left node right =
let
val left_node = treeAppend left (T node)
in
treeAppend left_node right
end;
fun treePeek pkey tree =
case tree of
E => NONE
| T node => nodePeek pkey node
and nodePeek pkey node =
let
val Node {left,key,value,right,...} = node
in
case compareKey (pkey,key) of
LESS => treePeek pkey left
| EQUAL => SOME value
| GREATER => treePeek pkey right
end;
fun treePeekPath pkey path tree =
case tree of
E => (path,NONE)
| T node => nodePeekPath pkey path node
and nodePeekPath pkey path node =
let
val Node {left,key,right,...} = node
in
case compareKey (pkey,key) of
LESS => treePeekPath pkey ((true,node) :: path) left
| EQUAL => (path, SOME node)
| GREATER => treePeekPath pkey ((false,node) :: path) right
end;
fun addSidePath ((wentLeft,node),(leftTree,rightTree)) =
let
val Node {priority,left,key,value,right,...} = node
in
if wentLeft then (leftTree, mkTree priority rightTree key value right)
else (mkTree priority left key value leftTree, rightTree)
end;
fun addSidesPath left_right = List.foldl addSidePath left_right;
fun mkSidesPath path = addSidesPath (E,E) path;
local
fun updateTree ((wentLeft,node),tree) =
let
val Node {priority,left,key,value,right,...} = node
in
if wentLeft then mkTree priority tree key value right
else mkTree priority left key value tree
end;
in
fun updateTreePath tree = List.foldl updateTree tree;
end;
fun insertNodePath node =
let
fun insert left_right path =
case path of
[] =>
let
val (left,right) = left_right
in
treeCombine left node right
end
| (step as (_,snode)) :: rest =>
if lowerPriorityNode snode node then
let
val left_right = addSidePath (step,left_right)
in
insert left_right rest
end
else
let
val (left,right) = left_right
val tree = treeCombine left node right
in
updateTreePath tree path
end
in
insert (E,E)
end;
fun nodePartition pkey node =
let
val (path,pnode) = nodePeekPath pkey [] node
in
case pnode of
NONE =>
let
val (left,right) = mkSidesPath path
in
(left,NONE,right)
end
| SOME node =>
let
val Node {left,key,value,right,...} = node
val (left,right) = addSidesPath (left,right) path
in
(left, SOME (key,value), right)
end
end;
fun treePeekKey pkey tree =
case tree of
E => NONE
| T node => nodePeekKey pkey node
and nodePeekKey pkey node =
let
val Node {left,key,value,right,...} = node
in
case compareKey (pkey,key) of
LESS => treePeekKey pkey left
| EQUAL => SOME (key,value)
| GREATER => treePeekKey pkey right
end;
fun treeInsert key_value tree =
let
val (key,value) = key_value
val (path,inode) = treePeekPath key [] tree
in
case inode of
NONE =>
let
val node = nodeSingleton (key,value)
in
insertNodePath node path
end
| SOME node =>
let
val Node {size,priority,left,right,...} = node
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
updateTreePath (T node) path
end
end;
fun treeDelete dkey tree =
case tree of
E => raise Bug "Metis_KeyMap.delete: element not found"
| T node => nodeDelete dkey node
and nodeDelete dkey node =
let
val Node {size,priority,left,key,value,right} = node
in
case compareKey (dkey,key) of
LESS =>
let
val size = size - 1
and left = treeDelete dkey left
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
T node
end
| EQUAL => treeAppend left right
| GREATER =>
let
val size = size - 1
and right = treeDelete dkey right
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
T node
end
end;
fun treeMapPartial f tree =
case tree of
E => E
| T node => nodeMapPartial f node
and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
let
val left = treeMapPartial f left
and vo = f (key,value)
and right = treeMapPartial f right
in
case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right
end;
fun treeMap f tree =
case tree of
E => E
| T node => T (nodeMap f node)
and nodeMap f node =
let
val Node {size,priority,left,key,value,right} = node
val left = treeMap f left
and value = f (key,value)
and right = treeMap f right
in
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
end;
fun treeMerge f1 f2 fb tree1 tree2 =
case tree1 of
E => treeMapPartial f2 tree2
| T node1 =>
case tree2 of
E => treeMapPartial f1 tree1
| T node2 => nodeMerge f1 f2 fb node1 node2
and nodeMerge f1 f2 fb node1 node2 =
let
val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition key node1
val left = treeMerge f1 f2 fb l left
and right = treeMerge f1 f2 fb r right
val vo =
case kvo of
NONE => f2 (key,value)
| SOME kv => fb (kv,(key,value))
in
case vo of
NONE => treeAppend left right
| SOME value =>
let
val node = mkNodeSingleton priority key value
in
treeCombine left node right
end
end;
fun treeUnion f f2 tree1 tree2 =
case tree1 of
E => tree2
| T node1 =>
case tree2 of
E => tree1
| T node2 => nodeUnion f f2 node1 node2
and nodeUnion f f2 node1 node2 =
if pointerEqual (node1,node2) then nodeMapPartial f2 node1
else
let
val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition key node1
val left = treeUnion f f2 l left
and right = treeUnion f f2 r right
val vo =
case kvo of
NONE => SOME value
| SOME kv => f (kv,(key,value))
in
case vo of
NONE => treeAppend left right
| SOME value =>
let
val node = mkNodeSingleton priority key value
in
treeCombine left node right
end
end;
fun treeIntersect f t1 t2 =
case t1 of
E => E
| T n1 =>
case t2 of
E => E
| T n2 => nodeIntersect f n1 n2
and nodeIntersect f n1 n2 =
let
val Node {priority,left,key,value,right,...} = n2
val (l,kvo,r) = nodePartition key n1
val left = treeIntersect f l left
and right = treeIntersect f r right
val vo =
case kvo of
NONE => NONE
| SOME kv => f (kv,(key,value))
in
case vo of
NONE => treeAppend left right
| SOME value => mkTree priority left key value right
end;
fun treeUnionDomain tree1 tree2 =
case tree1 of
E => tree2
| T node1 =>
case tree2 of
E => tree1
| T node2 =>
if pointerEqual (node1,node2) then tree2
else nodeUnionDomain node1 node2
and nodeUnionDomain node1 node2 =
let
val Node {priority,left,key,value,right,...} = node2
val (l,_,r) = nodePartition key node1
val left = treeUnionDomain l left
and right = treeUnionDomain r right
val node = mkNodeSingleton priority key value
in
treeCombine left node right
end;
fun treeIntersectDomain tree1 tree2 =
case tree1 of
E => E
| T node1 =>
case tree2 of
E => E
| T node2 =>
if pointerEqual (node1,node2) then tree2
else nodeIntersectDomain node1 node2
and nodeIntersectDomain node1 node2 =
let
val Node {priority,left,key,value,right,...} = node2
val (l,kvo,r) = nodePartition key node1
val left = treeIntersectDomain l left
and right = treeIntersectDomain r right
in
if Option.isSome kvo then mkTree priority left key value right
else treeAppend left right
end;
fun treeDifferenceDomain t1 t2 =
case t1 of
E => E
| T n1 =>
case t2 of
E => t1
| T n2 => nodeDifferenceDomain n1 n2
and nodeDifferenceDomain n1 n2 =
if pointerEqual (n1,n2) then E
else
let
val Node {priority,left,key,value,right,...} = n1
val (l,kvo,r) = nodePartition key n2
val left = treeDifferenceDomain left l
and right = treeDifferenceDomain right r
in
if Option.isSome kvo then treeAppend left right
else mkTree priority left key value right
end;
fun treeSubsetDomain tree1 tree2 =
case tree1 of
E => true
| T node1 =>
case tree2 of
E => false
| T node2 => nodeSubsetDomain node1 node2
and nodeSubsetDomain node1 node2 =
pointerEqual (node1,node2) orelse
let
val Node {size,left,key,right,...} = node1
in
size <= nodeSize node2 andalso
let
val (l,kvo,r) = nodePartition key node2
in
Option.isSome kvo andalso
treeSubsetDomain left l andalso
treeSubsetDomain right r
end
end;
fun nodePick node =
let
val Node {key,value,...} = node
in
(key,value)
end;
fun treePick tree =
case tree of
E => raise Bug "Metis_KeyMap.treePick"
| T node => nodePick node;
fun nodeDeletePick node =
let
val Node {left,key,value,right,...} = node
in
((key,value), treeAppend left right)
end;
fun treeDeletePick tree =
case tree of
E => raise Bug "Metis_KeyMap.treeDeletePick"
| T node => nodeDeletePick node;
fun treeNth n tree =
case tree of
E => raise Bug "Metis_KeyMap.treeNth"
| T node => nodeNth n node
and nodeNth n node =
let
val Node {left,key,value,right,...} = node
val k = treeSize left
in
if n = k then (key,value)
else if n < k then treeNth n left
else treeNth (n - (k + 1)) right
end;
fun treeDeleteNth n tree =
case tree of
E => raise Bug "Metis_KeyMap.treeDeleteNth"
| T node => nodeDeleteNth n node
and nodeDeleteNth n node =
let
val Node {size,priority,left,key,value,right} = node
val k = treeSize left
in
if n = k then ((key,value), treeAppend left right)
else if n < k then
let
val (key_value,left) = treeDeleteNth n left
val size = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
(key_value, T node)
end
else
let
val n = n - (k + 1)
val (key_value,right) = treeDeleteNth n right
val size = size - 1
val node =
Node
{size = size,
priority = priority,
left = left,
key = key,
value = value,
right = right}
in
(key_value, T node)
end
end;
datatype 'value iterator =
LeftToRightIterator of
(key * 'value) * 'value tree * 'value node list
| RightToLeftIterator of
(key * 'value) * 'value tree * 'value node list;
fun fromSpineLeftToRightIterator nodes =
case nodes of
[] => NONE
| Node {key,value,right,...} :: nodes =>
SOME (LeftToRightIterator ((key,value),right,nodes));
fun fromSpineRightToLeftIterator nodes =
case nodes of
[] => NONE
| Node {key,value,left,...} :: nodes =>
SOME (RightToLeftIterator ((key,value),left,nodes));
fun addLeftToRightIterator nodes tree = fromSpineLeftToRightIterator (treeLeftSpine nodes tree);
fun addRightToLeftIterator nodes tree = fromSpineRightToLeftIterator (treeRightSpine nodes tree);
fun treeMkIterator tree = addLeftToRightIterator [] tree;
fun treeMkRevIterator tree = addRightToLeftIterator [] tree;
fun readIterator iter =
case iter of
LeftToRightIterator (key_value,_,_) => key_value
| RightToLeftIterator (key_value,_,_) => key_value;
fun advanceIterator iter =
case iter of
LeftToRightIterator (_,tree,nodes) => addLeftToRightIterator nodes tree
| RightToLeftIterator (_,tree,nodes) => addRightToLeftIterator nodes tree;
fun foldIterator f acc io =
case io of
NONE => acc
| SOME iter =>
let
val (key,value) = readIterator iter
in
foldIterator f (f (key,value,acc)) (advanceIterator iter)
end;
fun findIterator pred io =
case io of
NONE => NONE
| SOME iter =>
let
val key_value = readIterator iter
in
if pred key_value then SOME key_value
else findIterator pred (advanceIterator iter)
end;
fun firstIterator f io =
case io of
NONE => NONE
| SOME iter =>
let
val key_value = readIterator iter
in
case f key_value of
NONE => firstIterator f (advanceIterator iter)
| s => s
end;
fun compareIterator compareValue io1 io2 =
case (io1,io2) of
(NONE,NONE) => EQUAL
| (NONE, SOME _) => LESS
| (SOME _, NONE) => GREATER
| (SOME i1, SOME i2) =>
let
val (k1,v1) = readIterator i1
and (k2,v2) = readIterator i2
in
case compareKey (k1,k2) of
LESS => LESS
| EQUAL =>
(case compareValue (v1,v2) of
LESS => LESS
| EQUAL =>
let
val io1 = advanceIterator i1
and io2 = advanceIterator i2
in
compareIterator compareValue io1 io2
end
| GREATER => GREATER)
| GREATER => GREATER
end;
fun equalIterator equalValue io1 io2 =
case (io1,io2) of
(NONE,NONE) => true
| (NONE, SOME _) => false
| (SOME _, NONE) => false
| (SOME i1, SOME i2) =>
let
val (k1,v1) = readIterator i1
and (k2,v2) = readIterator i2
in
equalKey k1 k2 andalso
equalValue v1 v2 andalso
let
val io1 = advanceIterator i1
and io2 = advanceIterator i2
in
equalIterator equalValue io1 io2
end
end;
datatype 'value map =
Metis_Map of 'value tree;
fun new () =
let
val tree = treeNew ()
in
Metis_Map tree
end;
fun singleton key_value =
let
val tree = treeSingleton key_value
in
Metis_Map tree
end;
fun size (Metis_Map tree) = treeSize tree;
fun null m = size m = 0;
fun peekKey (Metis_Map tree) key = treePeekKey key tree;
fun peek (Metis_Map tree) key = treePeek key tree;
fun inDomain key m = Option.isSome (peek m key);
fun get m key =
case peek m key of
NONE => raise Error "Metis_KeyMap.get: element not found"
| SOME value => value;
fun pick (Metis_Map tree) = treePick tree;
fun nth (Metis_Map tree) n = treeNth n tree;
fun random m =
let
val n = size m
in
if n = 0 then raise Bug "Metis_KeyMap.random: empty"
else nth m (randomInt n)
end;
fun insert (Metis_Map tree) key_value =
let
val tree = treeInsert key_value tree
in
Metis_Map tree
end;
fun insertList m =
let
fun ins (key_value,acc) = insert acc key_value
in
List.foldl ins m
end;
fun delete (Metis_Map tree) dkey =
let
val tree = treeDelete dkey tree
in
Metis_Map tree
end;
fun remove m key = if inDomain key m then delete m key else m;
fun deletePick (Metis_Map tree) =
let
val (key_value,tree) = treeDeletePick tree
in
(key_value, Metis_Map tree)
end;
fun deleteNth (Metis_Map tree) n =
let
val (key_value,tree) = treeDeleteNth n tree
in
(key_value, Metis_Map tree)
end;
fun deleteRandom m =
let
val n = size m
in
if n = 0 then raise Bug "Metis_KeyMap.deleteRandom: empty"
else deleteNth m (randomInt n)
end;
fun merge {first,second,both} (Metis_Map tree1) (Metis_Map tree2) =
let
val tree = treeMerge first second both tree1 tree2
in
Metis_Map tree
end;
fun union f (Metis_Map tree1) (Metis_Map tree2) =
let
fun f2 kv = f (kv,kv)
val tree = treeUnion f f2 tree1 tree2
in
Metis_Map tree
end;
fun intersect f (Metis_Map tree1) (Metis_Map tree2) =
let
val tree = treeIntersect f tree1 tree2
in
Metis_Map tree
end;
fun mkIterator (Metis_Map tree) = treeMkIterator tree;
fun mkRevIterator (Metis_Map tree) = treeMkRevIterator tree;
fun mapPartial f (Metis_Map tree) =
let
val tree = treeMapPartial f tree
in
Metis_Map tree
end;
fun map f (Metis_Map tree) =
let
val tree = treeMap f tree
in
Metis_Map tree
end;
fun transform f = map (fn (_,value) => f value);
fun filter pred =
let
fun f (key_value as (_,value)) =
if pred key_value then SOME value else NONE
in
mapPartial f
end;
fun partition p =
let
fun np x = not (p x)
in
fn m => (filter p m, filter np m)
end;
fun foldl f b m = foldIterator f b (mkIterator m);
fun foldr f b m = foldIterator f b (mkRevIterator m);
fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
fun findl p m = findIterator p (mkIterator m);
fun findr p m = findIterator p (mkRevIterator m);
fun firstl f m = firstIterator f (mkIterator m);
fun firstr f m = firstIterator f (mkRevIterator m);
fun exists p m = Option.isSome (findl p m);
fun all p =
let
fun np x = not (p x)
in
fn m => not (exists np m)
end;
fun count pred =
let
fun f (k,v,acc) = if pred (k,v) then acc + 1 else acc
in
foldl f 0
end;
fun compare compareValue (m1,m2) =
if pointerEqual (m1,m2) then EQUAL
else
case Int.compare (size m1, size m2) of
LESS => LESS
| EQUAL =>
let
val Metis_Map _ = m1
val io1 = mkIterator m1
and io2 = mkIterator m2
in
compareIterator compareValue io1 io2
end
| GREATER => GREATER;
fun equal equalValue m1 m2 =
pointerEqual (m1,m2) orelse
(size m1 = size m2 andalso
let
val Metis_Map _ = m1
val io1 = mkIterator m1
and io2 = mkIterator m2
in
equalIterator equalValue io1 io2
end);
fun unionDomain (Metis_Map tree1) (Metis_Map tree2) =
let
val tree = treeUnionDomain tree1 tree2
in
Metis_Map tree
end;
local
fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
in
fun unionListDomain ms =
case ms of
[] => raise Bug "Metis_KeyMap.unionListDomain: no sets"
| m :: ms => List.foldl uncurriedUnionDomain m ms;
end;
fun intersectDomain (Metis_Map tree1) (Metis_Map tree2) =
let
val tree = treeIntersectDomain tree1 tree2
in
Metis_Map tree
end;
local
fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
in
fun intersectListDomain ms =
case ms of
[] => raise Bug "Metis_KeyMap.intersectListDomain: no sets"
| m :: ms => List.foldl uncurriedIntersectDomain m ms;
end;
fun differenceDomain (Metis_Map tree1) (Metis_Map tree2) =
let
val tree = treeDifferenceDomain tree1 tree2
in
Metis_Map tree
end;
fun symmetricDifferenceDomain m1 m2 =
unionDomain (differenceDomain m1 m2) (differenceDomain m2 m1);
fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
fun subsetDomain (Metis_Map tree1) (Metis_Map tree2) =
treeSubsetDomain tree1 tree2;
fun disjointDomain m1 m2 = null (intersectDomain m1 m2);
fun keys m = foldr (fn (key,_,l) => key :: l) [] m;
fun values m = foldr (fn (_,value,l) => value :: l) [] m;
fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
fun fromList l =
let
val m = new