File ‹~~/src/Tools/Metis/metis.ML›

(*
   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 = 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,...}) =
    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;

(* ------------------------------------------------------------------------- *)
(* Mapping tree values.                                                      *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Merge is the basic operation for joining two trees. Note that the merged  *)
(* key is always the one from the second map.                                *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A union operation on trees.                                               *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* An intersect operation on trees.                                          *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A union operation on trees which simply chooses the second value.         *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* An intersect operation on trees which simply chooses the second value.    *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A difference operation on trees.                                          *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A subset operation on trees.                                              *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Picking an arbitrary key/value pair from a tree.                          *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Removing an arbitrary key/value pair from a tree.                         *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Finding the nth smallest key/value (counting from 0).                     *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Removing the nth smallest key/value (counting from 0).                    *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Iterators.                                                                *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A type of finite maps.                                                    *)
(* ------------------------------------------------------------------------- *)

datatype ('key,'value) map =
    Metis_Map of ('key * 'key -> order) * ('key,'value) tree;

(* ------------------------------------------------------------------------- *)
(* Metis_Map debugging functions.                                                  *)
(* ------------------------------------------------------------------------- *)

(*BasicDebug
fun checkInvariants s m =
    let
      val Metis_Map (compareKey,tree) = m

      val _ = treeCheckInvariants compareKey tree
    in
      m
    end
    handle Bug bug => raise Bug (s ^ "\n" ^ "Metis_Map.checkInvariants: " ^ bug);
*)

(* ------------------------------------------------------------------------- *)
(* Constructors.                                                             *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Metis_Map size.                                                                 *)
(* ------------------------------------------------------------------------- *)

fun size (Metis_Map (_,tree)) = treeSize tree;

fun null m = size m = 0;

(* ------------------------------------------------------------------------- *)
(* Querying.                                                                 *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Adding.                                                                   *)
(* ------------------------------------------------------------------------- *)

fun insert (Metis_Map (compareKey,tree)) key_value =
    let
      val tree = treeInsert compareKey key_value tree
    in
      Metis_Map (compareKey,tree)
    end;

(*BasicDebug
val insert = fn m => fn kv =>
    checkInvariants "Metis_Map.insert: result"
      (insert (checkInvariants "Metis_Map.insert: input" m) kv);
*)

fun insertList m =
    let
      fun ins (key_value,acc) = insert acc key_value
    in
      List.foldl ins m
    end;

(* ------------------------------------------------------------------------- *)
(* Removing.                                                                 *)
(* ------------------------------------------------------------------------- *)

fun delete (Metis_Map (compareKey,tree)) dkey =
    let
      val tree = treeDelete compareKey dkey tree
    in
      Metis_Map (compareKey,tree)
    end;

(*BasicDebug
val delete = fn m => fn k =>
    checkInvariants "Metis_Map.delete: result"
      (delete (checkInvariants "Metis_Map.delete: input" m) k);
*)

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;

(*BasicDebug
val deletePick = fn m =>
    let
      val (kv,m) = deletePick (checkInvariants "Metis_Map.deletePick: input" m)
    in
      (kv, checkInvariants "Metis_Map.deletePick: result" m)
    end;
*)

fun deleteNth (Metis_Map (compareKey,tree)) n =
    let
      val (key_value,tree) = treeDeleteNth n tree
    in
      (key_value, Metis_Map (compareKey,tree))
    end;

(*BasicDebug
val deleteNth = fn m => fn n =>
    let
      val (kv,m) = deleteNth (checkInvariants "Metis_Map.deleteNth: input" m) n
    in
      (kv, checkInvariants "Metis_Map.deleteNth: result" m)
    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;

(* ------------------------------------------------------------------------- *)
(* Joining (all join operations prefer keys in the second map).              *)
(* ------------------------------------------------------------------------- *)

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;

(*BasicDebug
val merge = fn f => fn m1 => fn m2 =>
    checkInvariants "Metis_Map.merge: result"
      (merge f
         (checkInvariants "Metis_Map.merge: input 1" m1)
         (checkInvariants "Metis_Map.merge: input 2" m2));
*)

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;

(*BasicDebug
val union = fn f => fn m1 => fn m2 =>
    checkInvariants "Metis_Map.union: result"
      (union f
         (checkInvariants "Metis_Map.union: input 1" m1)
         (checkInvariants "Metis_Map.union: input 2" m2));
*)

fun intersect f (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
    let
      val tree = treeIntersect compareKey f tree1 tree2
    in
      Metis_Map (compareKey,tree)
    end;

(*BasicDebug
val intersect = fn f => fn m1 => fn m2 =>
    checkInvariants "Metis_Map.intersect: result"
      (intersect f
         (checkInvariants "Metis_Map.intersect: input 1" m1)
         (checkInvariants "Metis_Map.intersect: input 2" m2));
*)

(* ------------------------------------------------------------------------- *)
(* Iterators over maps.                                                      *)
(* ------------------------------------------------------------------------- *)

fun mkIterator (Metis_Map (_,tree)) = treeMkIterator tree;

fun mkRevIterator (Metis_Map (_,tree)) = treeMkRevIterator tree;

(* ------------------------------------------------------------------------- *)
(* Mapping and folding.                                                      *)
(* ------------------------------------------------------------------------- *)

fun mapPartial f (Metis_Map (compareKey,tree)) =
    let
      val tree = treeMapPartial f tree
    in
      Metis_Map (compareKey,tree)
    end;

(*BasicDebug
val mapPartial = fn f => fn m =>
    checkInvariants "Metis_Map.mapPartial: result"
      (mapPartial f (checkInvariants "Metis_Map.mapPartial: input" m));
*)

fun map f (Metis_Map (compareKey,tree)) =
    let
      val tree = treeMap f tree
    in
      Metis_Map (compareKey,tree)
    end;

(*BasicDebug
val map = fn f => fn m =>
    checkInvariants "Metis_Map.map: result"
      (map f (checkInvariants "Metis_Map.map: input" m));
*)

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;

(* ------------------------------------------------------------------------- *)
(* Searching.                                                                *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Comparing.                                                                *)
(* ------------------------------------------------------------------------- *)

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

(* ------------------------------------------------------------------------- *)
(* Metis_Set operations on the domain.                                             *)
(* ------------------------------------------------------------------------- *)

fun unionDomain (Metis_Map (compareKey,tree1)) (Metis_Map (_,tree2)) =
    let
      val tree = treeUnionDomain compareKey tree1 tree2
    in
      Metis_Map (compareKey,tree)
    end;

(*BasicDebug
val unionDomain = fn m1 => fn m2 =>
    checkInvariants "Metis_Map.unionDomain: result"
      (unionDomain
         (checkInvariants "Metis_Map.unionDomain: input 1" m1)
         (checkInvariants "Metis_Map.unionDomain: input 2" m2));
*)

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;

(*BasicDebug
val intersectDomain = fn m1 => fn m2 =>
    checkInvariants "Metis_Map.intersectDomain: result"
      (intersectDomain
         (checkInvariants "Metis_Map.intersectDomain: input 1" m1)
         (checkInvariants "Metis_Map.intersectDomain: input 2" m2));
*)

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;

(*BasicDebug
val differenceDomain = fn m1 => fn m2 =>
    checkInvariants "Metis_Map.differenceDomain: result"
      (differenceDomain
         (checkInvariants "Metis_Map.differenceDomain: input 1" m1)
         (checkInvariants "Metis_Map.differenceDomain: input 2" m2));
*)

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

(* ------------------------------------------------------------------------- *)
(* Converting to and from lists.                                             *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Pretty-printing.                                                          *)
(* ------------------------------------------------------------------------- *)

fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";

end

(**** Original file: src/KeyMap.sig ****)

(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

signature Metis_KeyMap =
sig

(* ------------------------------------------------------------------------- *)
(* A type of map keys.                                                       *)
(* ------------------------------------------------------------------------- *)

type key

val compareKey : key * key -> order

val equalKey : key -> key -> bool

(* ------------------------------------------------------------------------- *)
(* A type of finite maps.                                                    *)
(* ------------------------------------------------------------------------- *)

type 'a map

(* ------------------------------------------------------------------------- *)
(* Constructors.                                                             *)
(* ------------------------------------------------------------------------- *)

val new : unit -> 'a map

val singleton : key * 'a -> 'a map

(* ------------------------------------------------------------------------- *)
(* Metis_Map size.                                                                 *)
(* ------------------------------------------------------------------------- *)

val null : 'a map -> bool

val size : 'a map -> int

(* ------------------------------------------------------------------------- *)
(* Querying.                                                                 *)
(* ------------------------------------------------------------------------- *)

val peekKey : 'a map -> key -> (key * 'a) option

val peek : 'a map -> key -> 'a option

val get : 'a map -> key -> 'a  (* raises Error *)

val pick : 'a map -> key * 'a  (* an arbitrary key/value pair *)

val nth : 'a map -> int -> key * 'a  (* in the range [0,size-1] *)

val random : 'a map -> key * 'a

(* ------------------------------------------------------------------------- *)
(* Adding.                                                                   *)
(* ------------------------------------------------------------------------- *)

val insert : 'a map -> key * 'a -> 'a map

val insertList : 'a map -> (key * 'a) list -> 'a map

(* ------------------------------------------------------------------------- *)
(* Removing.                                                                 *)
(* ------------------------------------------------------------------------- *)

val delete : 'a map -> key -> 'a map  (* must be present *)

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

(* ------------------------------------------------------------------------- *)
(* 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} ->
    '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

(* ------------------------------------------------------------------------- *)
(* Metis_Set operations on the domain.                                             *)
(* ------------------------------------------------------------------------- *)

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

(* ------------------------------------------------------------------------- *)
(* Mapping and folding.                                                      *)
(* ------------------------------------------------------------------------- *)

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

(* ------------------------------------------------------------------------- *)
(* Searching.                                                                *)
(* ------------------------------------------------------------------------- *)

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

(* ------------------------------------------------------------------------- *)
(* Comparing.                                                                *)
(* ------------------------------------------------------------------------- *)

val compare : ('a * 'a -> order) -> 'a map * 'a map -> order

val equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool

(* ------------------------------------------------------------------------- *)
(* Converting to and from lists.                                             *)
(* ------------------------------------------------------------------------- *)

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

(* ------------------------------------------------------------------------- *)
(* Pretty-printing.                                                          *)
(* ------------------------------------------------------------------------- *)

val toString : 'a map -> string

(* ------------------------------------------------------------------------- *)
(* Iterators over maps.                                                      *)
(* ------------------------------------------------------------------------- *)

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

(**** Original file: src/KeyMap.sml ****)

(* ========================================================================= *)
(* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
(* Copyright (c) 2004 Joe Leslie-Hurd, distributed under the BSD License     *)
(* ========================================================================= *)

functor Metis_KeyMap (Key : Metis_Ordered) :> Metis_KeyMap where type key = Key.t =
struct

(* ------------------------------------------------------------------------- *)
(* Importing from the input signature.                                       *)
(* ------------------------------------------------------------------------- *)

type key = Key.t;

val compareKey = Key.compare;

(* ------------------------------------------------------------------------- *)
(* 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 key1 key2 = compareKey (key1,key2) = EQUAL;

(* ------------------------------------------------------------------------- *)
(* Priorities.                                                               *)
(* ------------------------------------------------------------------------- *)

type priority = Word.word;

val randomPriority = randomWord;

val comparePriority = Word.compare;

(* ------------------------------------------------------------------------- *)
(* Priority search trees.                                                    *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* 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 x tree =
      case tree of
        E => x
      | T (Node {left,key,right,...}) =>
        let
          val x = checkSorted 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 x right
        end;

  fun checkPriorities tree =
      case tree of
        E => NONE
      | T node =>
        let
          val Node {left,right,...} = node

          val () =
              case checkPriorities left of
                NONE => ()
              | SOME lnode =>
                if not (lowerPriorityNode node lnode) then ()
                else raise Bug "left child has greater priority"

          val () =
              case checkPriorities 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 tree =
      let
        val _ = checkSizes tree

        val _ = checkSorted NONE tree

        val _ = checkPriorities 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 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;

(* ------------------------------------------------------------------------- *)
(* Tree paths.                                                               *)
(* ------------------------------------------------------------------------- *)

(* Generating a path by searching a tree for a key/value pair *)

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;

(* 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 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;

(* ------------------------------------------------------------------------- *)
(* Searching a tree for a key/value pair.                                    *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Inserting new key/values into the tree.                                   *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Deleting key/value pairs: it raises an exception if the supplied key is   *)
(* not present.                                                              *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* 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,...}) =
    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;

(* ------------------------------------------------------------------------- *)
(* Mapping tree values.                                                      *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Merge is the basic operation for joining two trees. Note that the merged  *)
(* key is always the one from the second map.                                *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A union operation on trees.                                               *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* An intersect operation on trees.                                          *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A union operation on trees which simply chooses the second value.         *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* An intersect operation on trees which simply chooses the second value.    *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A difference operation on trees.                                          *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A subset operation on trees.                                              *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Picking an arbitrary key/value pair from a tree.                          *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Removing an arbitrary key/value pair from a tree.                         *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Finding the nth smallest key/value (counting from 0).                     *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Removing the nth smallest key/value (counting from 0).                    *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Iterators.                                                                *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* A type of finite maps.                                                    *)
(* ------------------------------------------------------------------------- *)

datatype 'value map =
    Metis_Map of 'value tree;

(* ------------------------------------------------------------------------- *)
(* Metis_Map debugging functions.                                                  *)
(* ------------------------------------------------------------------------- *)

(*BasicDebug
fun checkInvariants s m =
    let
      val Metis_Map tree = m

      val _ = treeCheckInvariants tree
    in
      m
    end
    handle Bug bug => raise Bug (s ^ "\n" ^ "Metis_KeyMap.checkInvariants: " ^ bug);
*)

(* ------------------------------------------------------------------------- *)
(* Constructors.                                                             *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Metis_Map size.                                                                 *)
(* ------------------------------------------------------------------------- *)

fun size (Metis_Map tree) = treeSize tree;

fun null m = size m = 0;

(* ------------------------------------------------------------------------- *)
(* Querying.                                                                 *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Adding.                                                                   *)
(* ------------------------------------------------------------------------- *)

fun insert (Metis_Map tree) key_value =
    let
      val tree = treeInsert key_value tree
    in
      Metis_Map tree
    end;

(*BasicDebug
val insert = fn m => fn kv =>
    checkInvariants "Metis_KeyMap.insert: result"
      (insert (checkInvariants "Metis_KeyMap.insert: input" m) kv);
*)

fun insertList m =
    let
      fun ins (key_value,acc) = insert acc key_value
    in
      List.foldl ins m
    end;

(* ------------------------------------------------------------------------- *)
(* Removing.                                                                 *)
(* ------------------------------------------------------------------------- *)

fun delete (Metis_Map tree) dkey =
    let
      val tree = treeDelete dkey tree
    in
      Metis_Map tree
    end;

(*BasicDebug
val delete = fn m => fn k =>
    checkInvariants "Metis_KeyMap.delete: result"
      (delete (checkInvariants "Metis_KeyMap.delete: input" m) k);
*)

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;

(*BasicDebug
val deletePick = fn m =>
    let
      val (kv,m) = deletePick (checkInvariants "Metis_KeyMap.deletePick: input" m)
    in
      (kv, checkInvariants "Metis_KeyMap.deletePick: result" m)
    end;
*)

fun deleteNth (Metis_Map tree) n =
    let
      val (key_value,tree) = treeDeleteNth n tree
    in
      (key_value, Metis_Map tree)
    end;

(*BasicDebug
val deleteNth = fn m => fn n =>
    let
      val (kv,m) = deleteNth (checkInvariants "Metis_KeyMap.deleteNth: input" m) n
    in
      (kv, checkInvariants "Metis_KeyMap.deleteNth: result" m)
    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;

(* ------------------------------------------------------------------------- *)
(* Joining (all join operations prefer keys in the second map).              *)
(* ------------------------------------------------------------------------- *)

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;

(*BasicDebug
val merge = fn f => fn m1 => fn m2 =>
    checkInvariants "Metis_KeyMap.merge: result"
      (merge f
         (checkInvariants "Metis_KeyMap.merge: input 1" m1)
         (checkInvariants "Metis_KeyMap.merge: input 2" m2));
*)

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;

(*BasicDebug
val union = fn f => fn m1 => fn m2 =>
    checkInvariants "Metis_KeyMap.union: result"
      (union f
         (checkInvariants "Metis_KeyMap.union: input 1" m1)
         (checkInvariants "Metis_KeyMap.union: input 2" m2));
*)

fun intersect f (Metis_Map tree1) (Metis_Map tree2) =
    let
      val tree = treeIntersect f tree1 tree2
    in
      Metis_Map tree
    end;

(*BasicDebug
val intersect = fn f => fn m1 => fn m2 =>
    checkInvariants "Metis_KeyMap.intersect: result"
      (intersect f
         (checkInvariants "Metis_KeyMap.intersect: input 1" m1)
         (checkInvariants "Metis_KeyMap.intersect: input 2" m2));
*)

(* ------------------------------------------------------------------------- *)
(* Iterators over maps.                                                      *)
(* ------------------------------------------------------------------------- *)

fun mkIterator (Metis_Map tree) = treeMkIterator tree;

fun mkRevIterator (Metis_Map tree) = treeMkRevIterator tree;

(* ------------------------------------------------------------------------- *)
(* Mapping and folding.                                                      *)
(* ------------------------------------------------------------------------- *)

fun mapPartial f (Metis_Map tree) =
    let
      val tree = treeMapPartial f tree
    in
      Metis_Map tree
    end;

(*BasicDebug
val mapPartial = fn f => fn m =>
    checkInvariants "Metis_KeyMap.mapPartial: result"
      (mapPartial f (checkInvariants "Metis_KeyMap.mapPartial: input" m));
*)

fun map f (Metis_Map tree) =
    let
      val tree = treeMap f tree
    in
      Metis_Map tree
    end;

(*BasicDebug
val map = fn f => fn m =>
    checkInvariants "Metis_KeyMap.map: result"
      (map f (checkInvariants "Metis_KeyMap.map: input" m));
*)

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;

(* ------------------------------------------------------------------------- *)
(* Searching.                                                                *)
(* ------------------------------------------------------------------------- *)

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;

(* ------------------------------------------------------------------------- *)
(* Comparing.                                                                *)
(* ------------------------------------------------------------------------- *)

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

(* ------------------------------------------------------------------------- *)
(* Metis_Set operations on the domain.                                             *)
(* ------------------------------------------------------------------------- *)

fun unionDomain (Metis_Map tree1) (Metis_Map tree2) =
    let
      v