(*
This file was generated by the "make_metis" script. The BSD License is used
with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010
email written by him:
I hereby give permission to the Isabelle team to release Metis as part
of Isabelle, with the Metis code covered under the Isabelle BSD
license.
*)
(******************************************************************)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)
(**** Original file: src/Random.sig ****)
(* Title: Tools/random_word.ML
Author: Makarius
Simple generator for pseudo-random numbers, using unboxed word
arithmetic only. Unprotected concurrency introduces some true
randomness.
*)
signature Metis_Random =
sig
val nextWord : unit -> word
val nextBool : unit ->
bool
val nextInt : int -> int
(* k -> [0,k) *)
val nextReal : unit -> real
(* () -> [0,1) *)
end;
(**** Original file: src/Random.sml ****)
(* Title: Tools/random_word.ML
Author: Makarius
Simple generator for pseudo-random numbers, using unboxed word
arithmetic only. Unprotected concurrency introduces some true
randomness.
*)
structure Metis_Random :> Metis_Random =
struct
(* random words: 0w0 <= result <= max_word *)
(*minimum length of unboxed words on all supported ML platforms*)
val _ = Word.wordSize >= 30
orelse
raise Fail (
"Bad platform word size");
val max_word = 0wx3FFFFFFF;
val top_bit = 0wx20000000;
(*multiplier according to Borosh and Niederreiter (for modulus = 2^30),
see http://random.mat.sbg.ac.at/~charly/server/server.html*)
val a = 0w777138309;
fun step x = Word.andb (a * x + 0w1, max_word);
fun change r f = r := f (!r);
local
val rand =
(*Unsynchronized.*)Unsynchronized.ref 0w1
in fun nextWord () = (
(*Unsynchronized.*)change rand step; ! rand) end;
(*NB: higher bits are more random than lower ones*)
fun nextBool () = Word.andb (nextWord (), top_bit) = 0w0;
(* random integers: 0 <= result < k *)
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));
(* random reals: 0.0 <= result < 1.0 *)
val scaling = real max_int + 1.0;
fun nextReal () = real (Word.toInt (nextWord ())) / scaling;
end;
(**** Original file: src/Portable.sig ****)
(* ========================================================================= *)
(* ML COMPILER SPECIFIC FUNCTIONS *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Portable =
sig
(* ------------------------------------------------------------------------- *)
(* The ML implementation. *)
(* ------------------------------------------------------------------------- *)
val ml :
string
(* ------------------------------------------------------------------------- *)
(* Pointer equality using the run-time system. *)
(* ------------------------------------------------------------------------- *)
val pointerEqual :
'a * 'a ->
bool
(* ------------------------------------------------------------------------- *)
(* Marking critical sections of code. *)
(* ------------------------------------------------------------------------- *)
val critical : (unit ->
'a) -> unit -> 'a
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
val randomBool : unit ->
bool
val randomInt : int -> int
(* n |-> [0,n) *)
val randomReal : unit -> real
(* () |-> [0,1] *)
val randomWord : unit -> Word.word
(* ------------------------------------------------------------------------- *)
(* Timing function applications. *)
(* ------------------------------------------------------------------------- *)
val time : (
'a -> 'b) ->
'a -> 'b
end
(**** Original file: PortableIsabelle.sml ****)
(* Title: Tools/Metis/PortableIsabelle.sml
Author: Jasmin Blanchette, TU Muenchen
Copyright 2010
Isabelle-specific setup for Metis. Based on "src/PortablePolyml.sml".
*)
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
(* dummy *)
end
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a
(**** Original file: src/Useful.sig ****)
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Useful =
sig
(* ------------------------------------------------------------------------- *)
(* Exceptions. *)
(* ------------------------------------------------------------------------- *)
exception Error
of string
exception Bug
of string
val total : (
'a -> 'b) ->
'a -> 'b
option
val can : (
'a -> 'b) ->
'a -> bool
(* ------------------------------------------------------------------------- *)
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
val tracePrint : (
string -> unit) Unsynchronized.
ref
val trace :
string -> unit
(* ------------------------------------------------------------------------- *)
(* Combinators. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Pairs. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* State transformers. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Equality. *)
(* ------------------------------------------------------------------------- *)
val equal :
''a ->
''a ->
bool
val notEqual :
''a ->
''a ->
bool
val listEqual : (
'a -> 'a ->
bool) ->
'a list -> 'a
list ->
bool
(* ------------------------------------------------------------------------- *)
(* Comparisons. *)
(* ------------------------------------------------------------------------- *)
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
(* false < true *)
(* ------------------------------------------------------------------------- *)
(* Lists: note we count elements from 0. *)
(* ------------------------------------------------------------------------- *)
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 (* Subscript *)
val revDivide :
'a list -> int -> 'a
list *
'a list (* Subscript *)
val updateNth : int *
'a -> 'a
list ->
'a list (* Subscript *)
val deleteNth : int ->
'a list -> 'a
list (* Subscript *)
(* ------------------------------------------------------------------------- *)
(* Sets implemented with lists. *)
(* ------------------------------------------------------------------------- *)
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 (* removes duplicates *)
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
(* ------------------------------------------------------------------------- *)
(* Sorting and searching. *)
(* ------------------------------------------------------------------------- *)
val minimum : (
'a * 'a -> order) ->
'a list -> 'a *
'a list (* Empty *)
val maximum : (
'a * 'a -> order) ->
'a list -> 'a *
'a list (* Empty *)
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
(* ------------------------------------------------------------------------- *)
(* Integers. *)
(* ------------------------------------------------------------------------- *)
val interval : int -> int -> int
list
val divides : int -> int ->
bool
val gcd : int -> int -> int
(* Primes *)
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
(* ------------------------------------------------------------------------- *)
(* Strings. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Tables. *)
(* ------------------------------------------------------------------------- *)
type columnAlignment = {leftAlign :
bool, padChar : char}
val alignColumn : columnAlignment ->
string list ->
string list ->
string list
val alignTable : columnAlignment
list ->
string list list ->
string list
(* ------------------------------------------------------------------------- *)
(* Reals. *)
(* ------------------------------------------------------------------------- *)
val percentToString : real ->
string
val pos : real -> real
val log2 : real -> real
(* Domain *)
(* ------------------------------------------------------------------------- *)
(* Sum datatype. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Metis_Useful impure features. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* The environment. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Profiling and error reporting. *)
(* ------------------------------------------------------------------------- *)
val try : (
'a -> 'b) ->
'a -> 'b
val chat :
string -> unit
(* stdout *)
val chide :
string -> unit
(* stderr *)
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
(* Wall clock execution time *)
end
(**** Original file: src/Useful.sml ****)
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
(* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Useful :> Metis_Useful =
struct
(* ------------------------------------------------------------------------- *)
(* Exceptions. *)
(* ------------------------------------------------------------------------- *)
exception Error
of string;
exception Bug
of string;
fun errorToStringOption err =
case err
of
Error message => SOME (
"Error: " ^ message)
| _ => NONE;
(*mlton
val () = MLton.Exn.addExnMessager errorToStringOption;
*)
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;
(*mlton
val () = MLton.Exn.addExnMessager bugToStringOption;
*)
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;
(* ------------------------------------------------------------------------- *)
(* Tracing. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Combinators. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Pairs. *)
(* ------------------------------------------------------------------------- *)
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);
(* ------------------------------------------------------------------------- *)
(* State transformers. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Equality. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Comparisons. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Lists. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Sets implemented with lists. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Sorting and searching. *)
(* ------------------------------------------------------------------------- *)
(* Finding the minimum and maximum element of a list, wrt some order. *)
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);
(* Merge (for the following merge-sort, but generally useful too). *)
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;
(* Merge sort (stable). *)
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;
(* ------------------------------------------------------------------------- *)
(* Integers. *)
(* ------------------------------------------------------------------------- *)
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;
(* Primes *)
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;
(* ------------------------------------------------------------------------- *)
(* Strings. *)
(* ------------------------------------------------------------------------- *)
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));
(* ------------------------------------------------------------------------- *)
(* Tables. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Reals. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Sums. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Metis_Useful impure features. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Environment. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Profiling and error reporting. *)
(* ------------------------------------------------------------------------- *)
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
(**** Original file: src/Lazy.sig ****)
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
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
(**** Original file: src/Lazy.sml ****)
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
(* Copyright (c) 2007 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
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
(**** Original file: src/Ordered.sig ****)
(* ========================================================================= *)
(* ORDERED TYPES *)
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Ordered =
sig
type t
val compare : t * t -> order
(*
PROVIDES
!x : t. compare (x,x) = EQUAL
!x y : t. compare (x,y) = LESS <=> compare (y,x) = GREATER
!x y : t. compare (x,y) = EQUAL ==> compare (y,x) = EQUAL
!x y z : t. compare (x,y) = EQUAL ==> compare (x,z) = compare (y,z)
!x y z : t.
compare (x,y) = LESS andalso compare (y,z) = LESS ==>
compare (x,z) = LESS
!x y z : t.
compare (x,y) = GREATER andalso compare (y,z) = GREATER ==>
compare (x,z) = GREATER
*)
end
(**** Original file: src/Ordered.sml ****)
(* ========================================================================= *)
(* ORDERED TYPES *)
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
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;
(**** Original file: src/Map.sig ****)
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Metis_Map =
sig
(* ------------------------------------------------------------------------- *)
(* A type of finite maps. *)
(* ------------------------------------------------------------------------- *)
type (
'key,'a)
map
(* ------------------------------------------------------------------------- *)
(* Constructors. *)
(* ------------------------------------------------------------------------- *)
val new : (
'key * 'key -> order) -> (
'key,'a)
map
val singleton : (
'key * 'key -> order) ->
'key * 'a -> (
'key,'a)
map
(* ------------------------------------------------------------------------- *)
(* Metis_Map size. *)
(* ------------------------------------------------------------------------- *)
val null : (
'key,'a)
map ->
bool
val size : (
'key,'a)
map -> int
(* ------------------------------------------------------------------------- *)
(* Querying. *)
(* ------------------------------------------------------------------------- *)
val peekKey : (
'key,'a)
map ->
'key -> ('key *
'a) option
val peek : (
'key,'a)
map ->
'key -> 'a
option
val get : (
'key,'a)
map ->
'key -> 'a
(* raises Error *)
val pick : (
'key,'a)
map ->
'key * 'a
(* an arbitrary key/value pair *)
val nth : (
'key,'a)
map -> int ->
'key * 'a
(* in the range [0,size-1] *)
val random : (
'key,'a)
map ->
'key * 'a
(* ------------------------------------------------------------------------- *)
(* Adding. *)
(* ------------------------------------------------------------------------- *)
val insert : (
'key,'a)
map ->
'key * 'a -> (
'key,'a)
map
val insertList : (
'key,'a)
map -> (
'key * 'a)
list -> (
'key,'a)
map
(* ------------------------------------------------------------------------- *)
(* Removing. *)
(* ------------------------------------------------------------------------- *)
val delete : (
'key,'a)
map ->
'key -> ('key,
'a) map (* must be present *)
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
(* ------------------------------------------------------------------------- *)
(* Joining (all join operations prefer keys in the second 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
(* ------------------------------------------------------------------------- *)
(* Metis_Set operations on the domain. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Mapping and folding. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Searching. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Comparing. *)
(* ------------------------------------------------------------------------- *)
val compare : (
'a * 'a -> order) -> (
'key,'a)
map * (
'key,'a)
map -> order
val equal : (
'a -> 'a ->
bool) -> (
'key,'a)
map -> (
'key,'a)
map ->
bool
(* ------------------------------------------------------------------------- *)
(* Converting to and from lists. *)
(* ------------------------------------------------------------------------- *)
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
(* ------------------------------------------------------------------------- *)
(* Pretty-printing. *)
(* ------------------------------------------------------------------------- *)
val toString : (
'key,'a)
map ->
string
(* ------------------------------------------------------------------------- *)
(* Iterators over maps. *)
(* ------------------------------------------------------------------------- *)
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
(**** Original file: src/Map.sml ****)
(* ========================================================================= *)
(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Metis_Map :> Metis_Map =
struct
(* ------------------------------------------------------------------------- *)
(* Importing useful functionality. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Converting a comparison function to an equality function. *)
(* ------------------------------------------------------------------------- *)
fun equalKey compareKey key1 key2 = compareKey (key1,key2) = EQUAL;
(* ------------------------------------------------------------------------- *)
(* Priorities. *)
(* ------------------------------------------------------------------------- *)
type priority = Word.word;
val randomPriority = randomWord;
val comparePriority = Word.compare;
(* ------------------------------------------------------------------------- *)
(* Priority search trees. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Tree debugging functions. *)
(* ------------------------------------------------------------------------- *)
(*BasicDebug
local
fun checkSizes tree =
case tree of
E => 0
| T (Node {size,left,right,...}) =>
let
val l = checkSizes left
and r = checkSizes right
val () = if l + 1 + r = size then () else raise Bug "wrong size"
in
size
end;
fun checkSorted compareKey x tree =
case tree of
E => x
| T (Node {left,key,right,...}) =>
let
val x = checkSorted compareKey x left
val () =
case x of
NONE => ()
| SOME k =>
case compareKey (k,key) of
LESS => ()
| EQUAL => raise Bug "duplicate keys"
| GREATER => raise Bug "unsorted"
val x = SOME key
in
checkSorted compareKey x right
end;
fun checkPriorities compareKey tree =
case tree of
E => NONE
| T node =>
let
val Node {left,right,...} = node
val () =
case checkPriorities compareKey left of
NONE => ()
| SOME lnode =>
if not (lowerPriorityNode node lnode) then ()
else raise Bug "left child has greater priority"
val () =
case checkPriorities compareKey right of
NONE => ()
| SOME rnode =>
if not (lowerPriorityNode node rnode) then ()
else raise Bug "right child has greater priority"
in
SOME node
end;
in
fun treeCheckInvariants compareKey tree =
let
val _ = checkSizes tree
val _ = checkSorted compareKey NONE tree
val _ = checkPriorities compareKey tree
in
tree
end
handle Error err => raise Bug err;
end;
*)
(* ------------------------------------------------------------------------- *)
(* Tree operations. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Extracting the left and right spines of a tree. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Singleton trees. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Appending two trees, where every element of the first tree is less than *)
(* every element of the second tree. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Appending two trees and a node, where every element of the first tree is *)
(* less than the node, which in turn is less than every element of the *)
(* second tree. *)
(* ------------------------------------------------------------------------- *)
fun treeCombine left node right =
let
val left_node = treeAppend left (T node)
in
treeAppend left_node right
end;
(* ------------------------------------------------------------------------- *)
(* Searching a tree for a value. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Tree paths. *)
(* ------------------------------------------------------------------------- *)
(* Generating a path by searching a tree for a key/value pair *)
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;
(* A path splits a tree into left/right components *)
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;
(* Updating the subtree at a 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;
(* Inserting a new node at a path position *)
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;
(* ------------------------------------------------------------------------- *)
(* Using a key to split a node into three components: the keys comparing *)
(* less than the supplied key, an optional equal key, and the keys comparing *)
(* greater. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Searching a tree for a key/value pair. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Inserting new key/values into the tree. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Deleting key/value pairs: it raises an exception if the supplied key is *)
(* not present. *)
(* ------------------------------------------------------------------------- *)
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;
(* ------------------------------------------------------------------------- *)
(* Partial map is the basic operation for preserving tree structure. *)
(* It applies its argument function to the elements *in order*. *)
(* ------------------------------------------------------------------------- *)
fun treeMapPartial f tree =
case tree
of
E => E
| T node => nodeMapPartial f node
and nodeMapPartial f (Node {priority,left,key,value,right,...}) =
--> --------------------
--> maximum size reached
--> --------------------
