--- a/src/Tools/Metis/metis.ML Mon Sep 13 21:19:13 2010 +0200
+++ b/src/Tools/Metis/metis.ML Mon Sep 13 21:21:45 2010 +0200
@@ -1,3 +1,19 @@
+(*
+ This file was generated by the "make-metis" script. A few changes were done
+ manually on the script's output; these are marked as follows:
+
+ MODIFIED by Jasmin Blanchette
+
+ Some of these changes are needed so that the ML files compiles at all. Others
+ are old tweaks by Lawrence C. Paulson that are needed, if nothing else, for
+ backward compatibility. The BSD License is used with Joe Hurd's kind
+ permission. Extract from a September 13, 2010 email written by Joe Hurd:
+
+ 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 *)
@@ -8,11 +24,95 @@
structure Metis = struct structure Word = Word structure Array = Array end;
+(**** Original file: 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 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: Random.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
+(* 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 Random :> 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;
+end;
+
(**** Original file: Portable.sig ****)
(* ========================================================================= *)
(* ML SPECIFIC FUNCTIONS *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Portable =
@@ -37,12 +137,6 @@
val time : ('a -> 'b) -> 'a -> 'b
(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-val CRITICAL: (unit -> 'a) -> 'a
-
-(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
@@ -56,11 +150,11 @@
end
-(**** Original file: PortableIsabelle.sml ****)
+(**** Original file: PortablePolyml.sml ****)
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
+nonfix ++ -- RL;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -68,7 +162,8 @@
val foldr = List.foldr;
(* ========================================================================= *)
-(* Isabelle ML SPECIFIC FUNCTIONS *)
+(* POLY/ML SPECIFIC FUNCTIONS *)
+(* Copyright (c) 2008 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Portable :> Portable =
@@ -78,36 +173,65 @@
(* The ML implementation. *)
(* ------------------------------------------------------------------------- *)
-val ml = ml_system;
+val ml = "polyml";
(* ------------------------------------------------------------------------- *)
(* Pointer equality using the run-time system. *)
(* ------------------------------------------------------------------------- *)
-val pointerEqual = pointer_eq;
-
-(* ------------------------------------------------------------------------- *)
-(* Timing function applications a la Mosml.time. *)
-(* ------------------------------------------------------------------------- *)
-
-val time = timeap;
-
-(* ------------------------------------------------------------------------- *)
-(* Critical section markup (multiprocessing) *)
-(* ------------------------------------------------------------------------- *)
-
-fun CRITICAL e = NAMED_CRITICAL "metis" e;
+fun pointerEqual (x : 'a, y : 'a) = PolyML.pointerEq(x,y);
+
+(* ------------------------------------------------------------------------- *)
+(* Timing function applications. *)
+(* ------------------------------------------------------------------------- *)
+
+fun time f x =
+ let
+ fun p t =
+ let
+ val s = Time.fmt 3 t
+ in
+ case size (List.last (String.fields (fn x => x = #".") s)) of
+ 3 => s
+ | 2 => s ^ "0"
+ | 1 => s ^ "00"
+ | _ => raise Fail "Portable.time"
+ end
+
+ val c = Timer.startCPUTimer ()
+
+ val r = Timer.startRealTimer ()
+
+ fun pt () =
+ let
+ val {usr,sys} = Timer.checkCPUTimer c
+ val real = Timer.checkRealTimer r
+ in
+ print
+ ("User: " ^ p usr ^ " System: " ^ p sys ^
+ " Real: " ^ p real ^ "\n")
+ end
+
+ val y = f x handle e => (pt (); raise e)
+
+ val () = pt ()
+ in
+ y
+ end;
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
-val randomWord = Random_Word.next_word;
-val randomBool = Random_Word.next_bool;
-fun randomInt n = Random_Word.next_int 0 (n - 1);
-val randomReal = Random_Word.next_real;
-
-end;
+val randomWord = Random.nextWord;
+
+val randomBool = Random.nextBool;
+
+val randomInt = Random.nextInt;
+
+val randomReal = Random.nextReal;
+
+end
(* ------------------------------------------------------------------------- *)
(* Quotations a la Moscow ML. *)
@@ -116,868 +240,11 @@
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a;
end;
-(**** Original file: PP.sig ****)
-
-(* ========================================================================= *)
-(* PP -- pretty-printing -- from the SML/NJ library *)
-(* *)
-(* Modified for Moscow ML from SML/NJ Library version 0.2 *)
-(* *)
-(* COPYRIGHT (c) 1992 by AT&T Bell Laboratories. *)
-(* *)
-(* STANDARD ML OF NEW JERSEY COPYRIGHT NOTICE, LICENSE AND DISCLAIMER. *)
-(* *)
-(* Permission to use, copy, modify, and distribute this software and its *)
-(* documentation for any purpose and without fee is hereby granted, *)
-(* provided that the above copyright notice appear in all copies and that *)
-(* both the copyright notice and this permission notice and warranty *)
-(* disclaimer appear in supporting documentation, and that the name of *)
-(* AT&T Bell Laboratories or any AT&T entity not be used in advertising *)
-(* or publicity pertaining to distribution of the software without *)
-(* specific, written prior permission. *)
-(* *)
-(* AT&T disclaims all warranties with regard to this software, including *)
-(* all implied warranties of merchantability and fitness. In no event *)
-(* shall AT&T be liable for any special, indirect or consequential *)
-(* damages or any damages whatsoever resulting from loss of use, data or *)
-(* profits, whether in an action of contract, negligence or other *)
-(* tortious action, arising out of or in connection with the use or *)
-(* performance of this software. *)
-(* ========================================================================= *)
-
-signature PP =
-sig
-
- type ppstream
-
- type ppconsumer =
- {consumer : string -> unit,
- linewidth : int,
- flush : unit -> unit}
-
- datatype break_style =
- CONSISTENT
- | INCONSISTENT
-
- val mk_ppstream : ppconsumer -> ppstream
-
- val dest_ppstream : ppstream -> ppconsumer
-
- val add_break : ppstream -> int * int -> unit
-
- val add_newline : ppstream -> unit
-
- val add_string : ppstream -> string -> unit
-
- val begin_block : ppstream -> break_style -> int -> unit
-
- val end_block : ppstream -> unit
-
- val clear_ppstream : ppstream -> unit
-
- val flush_ppstream : ppstream -> unit
-
- val with_pp : ppconsumer -> (ppstream -> unit) -> unit
-
- val pp_to_string : int -> (ppstream -> 'a -> unit) -> 'a -> string
-
-end
-
-(*
- This structure provides tools for creating customized Oppen-style
- pretty-printers, based on the type ppstream. A ppstream is an
- output stream that contains prettyprinting commands. The commands
- are placed in the stream by various function calls listed below.
-
- There following primitives add commands to the stream:
- begin_block, end_block, add_string, add_break, and add_newline.
- All calls to add_string, add_break, and add_newline must happen
- between a pair of calls to begin_block and end_block must be
- properly nested dynamically. All calls to begin_block and
- end_block must be properly nested (dynamically).
-
- [ppconsumer] is the type of sinks for pretty-printing. A value of
- type ppconsumer is a record
- { consumer : string -> unit,
- linewidth : int,
- flush : unit -> unit }
- of a string consumer, a specified linewidth, and a flush function
- which is called whenever flush_ppstream is called.
-
- A prettyprinter can be called outright to print a value. In
- addition, a prettyprinter for a base type or nullary datatype ty
- can be installed in the top-level system. Then the installed
- prettyprinter will be invoked automatically whenever a value of
- type ty is to be printed.
-
- [break_style] is the type of line break styles for blocks:
-
- [CONSISTENT] specifies that if any line break occurs inside the
- block, then all indicated line breaks occur.
-
- [INCONSISTENT] specifies that breaks will be inserted to only to
- avoid overfull lines.
-
- [mk_ppstream {consumer, linewidth, flush}] creates a new ppstream
- which invokes the consumer to output text, putting at most
- linewidth characters on each line.
-
- [dest_ppstream ppstrm] extracts the linewidth, flush function, and
- consumer from a ppstream.
-
- [add_break ppstrm (size, offset)] notifies the pretty-printer that
- a line break is possible at this point.
- * When the current block style is CONSISTENT:
- ** if the entire block fits on the remainder of the line, then
- output size spaces; else
- ** increase the current indentation by the block offset;
- further indent every item of the block by offset, and add
- one newline at every add_break in the block.
- * When the current block style is INCONSISTENT:
- ** if the next component of the block fits on the remainder of
- the line, then output size spaces; else
- ** issue a newline and indent to the current indentation level
- plus the block offset plus the offset.
-
- [add_newline ppstrm] issues a newline.
-
- [add_string ppstrm str] outputs the string str to the ppstream.
-
- [begin_block ppstrm style blockoffset] begins a new block and
- level of indentation, with the given style and block offset.
-
- [end_block ppstrm] closes the current block.
-
- [clear_ppstream ppstrm] restarts the stream, without affecting the
- underlying consumer.
-
- [flush_ppstream ppstrm] executes any remaining commands in the
- ppstream (that is, flushes currently accumulated output to the
- consumer associated with ppstrm); executes the flush function
- associated with the consumer; and calls clear_ppstream.
-
- [with_pp consumer f] makes a new ppstream from the consumer and
- applies f (which can be thought of as a producer) to that
- ppstream, then flushed the ppstream and returns the value of f.
-
- [pp_to_string linewidth printit x] constructs a new ppstream
- ppstrm whose consumer accumulates the output in a string s. Then
- evaluates (printit ppstrm x) and finally returns the string s.
-
-
- Example 1: A simple prettyprinter for Booleans:
-
- load "PP";
- fun ppbool pps d =
- let open PP
- in
- begin_block pps INCONSISTENT 6;
- add_string pps (if d then "right" else "wrong");
- end_block pps
- end;
-
- Now one may define a ppstream to print to, and exercise it:
-
- val ppstrm = Metis.PP.mk_ppstream {consumer =
- fn s => Metis.TextIO.output(Metis.TextIO.stdOut, s),
- linewidth = 72,
- flush =
- fn () => Metis.TextIO.flushOut Metis.TextIO.stdOut};
-
- fun ppb b = (ppbool ppstrm b; Metis.PP.flush_ppstream ppstrm);
-
- - ppb false;
- wrong> val it = () : unit
-
- The prettyprinter may also be installed in the toplevel system;
- then it will be used to print all expressions of type bool
- subsequently computed:
-
- - installPP ppbool;
- > val it = () : unit
- - 1=0;
- > val it = wrong : bool
- - 1=1;
- > val it = right : bool
-
- See library Meta for a description of installPP.
-
-
- Example 2: Prettyprinting simple expressions (examples/pretty/Metis.ppexpr.sml):
-
- datatype expr =
- Cst of int
- | Neg of expr
- | Plus of expr * expr
-
- fun ppexpr pps e0 =
- let open PP
- fun ppe (Cst i) = add_string pps (Metis.Int.toString i)
- | ppe (Neg e) = (add_string pps "~"; ppe e)
- | ppe (Plus(e1, e2)) = (begin_block pps CONSISTENT 0;
- add_string pps "(";
- ppe e1;
- add_string pps " + ";
- add_break pps (0, 1);
- ppe e2;
- add_string pps ")";
- end_block pps)
- in
- begin_block pps INCONSISTENT 0;
- ppe e0;
- end_block pps
- end
-
- val _ = installPP ppexpr;
-
- (* Some example values: *)
-
- val e1 = Cst 1;
- val e2 = Cst 2;
- val e3 = Plus(e1, Neg e2);
- val e4 = Plus(Neg e3, e3);
- val e5 = Plus(Neg e4, e4);
- val e6 = Plus(e5, e5);
- val e7 = Plus(e6, e6);
- val e8 =
- Plus(e3, Plus(e3, Plus(e3, Plus(e3, Plus(e3, Plus(e3, e7))))));
-*)
-
-(**** Original file: PP.sml ****)
-
-structure Metis = struct open Metis
-(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;
-val foldl = List.foldl;
-val foldr = List.foldr;
-
-(* ========================================================================= *)
-(* PP -- pretty-printing -- from the SML/NJ library *)
-(* *)
-(* Modified for Moscow ML from SML/NJ Library version 0.2 *)
-(* *)
-(* COPYRIGHT (c) 1992 by AT&T Bell Laboratories. *)
-(* *)
-(* STANDARD ML OF NEW JERSEY COPYRIGHT NOTICE, LICENSE AND DISCLAIMER. *)
-(* *)
-(* Permission to use, copy, modify, and distribute this software and its *)
-(* documentation for any purpose and without fee is hereby granted, *)
-(* provided that the above copyright notice appear in all copies and that *)
-(* both the copyright notice and this permission notice and warranty *)
-(* disclaimer appear in supporting documentation, and that the name of *)
-(* AT&T Bell Laboratories or any AT&T entity not be used in advertising *)
-(* or publicity pertaining to distribution of the software without *)
-(* specific, written prior permission. *)
-(* *)
-(* AT&T disclaims all warranties with regard to this software, including *)
-(* all implied warranties of merchantability and fitness. In no event *)
-(* shall AT&T be liable for any special, indirect or consequential *)
-(* damages or any damages whatsoever resulting from loss of use, data or *)
-(* profits, whether in an action of contract, negligence or other *)
-(* tortious action, arising out of or in connection with the use or *)
-(* performance of this software. *)
-(* ========================================================================= *)
-
-structure PP :> PP =
-struct
-
-open Array
-infix 9 sub
-
-(* the queue library, formerly in unit Ppqueue *)
-
-datatype Qend = Qback | Qfront
-
-exception QUEUE_FULL
-exception QUEUE_EMPTY
-exception REQUESTED_QUEUE_SIZE_TOO_SMALL
-
-local
- fun ++ i n = (i + 1) mod n
- fun -- i n = (i - 1) mod n
-in
-
-abstype 'a queue = QUEUE of {elems: 'a array, (* the contents *)
- front: int Unsynchronized.ref,
- back: int Unsynchronized.ref,
- size: int} (* fixed size of element array *)
-with
-
- fun is_empty (QUEUE{front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1,...}) = true
- | is_empty _ = false
-
- fun mk_queue n init_val =
- if (n < 2)
- then raise REQUESTED_QUEUE_SIZE_TOO_SMALL
- else QUEUE{elems=array(n, init_val), front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1, size=n}
-
- fun clear_queue (QUEUE{front,back,...}) = (front := ~1; back := ~1)
-
- fun queue_at Qfront (QUEUE{elems,front,...}) = elems sub !front
- | queue_at Qback (QUEUE{elems,back,...}) = elems sub !back
-
- fun en_queue Qfront item (Q as QUEUE{elems,front,back,size}) =
- if (is_empty Q)
- then (front := 0; back := 0;
- update(elems,0,item))
- else let val i = --(!front) size
- in if (i = !back)
- then raise QUEUE_FULL
- else (update(elems,i,item); front := i)
- end
- | en_queue Qback item (Q as QUEUE{elems,front,back,size}) =
- if (is_empty Q)
- then (front := 0; back := 0;
- update(elems,0,item))
- else let val i = ++(!back) size
- in if (i = !front)
- then raise QUEUE_FULL
- else (update(elems,i,item); back := i)
- end
-
- fun de_queue Qfront (Q as QUEUE{front,back,size,...}) =
- if (!front = !back) (* unitary queue *)
- then clear_queue Q
- else front := ++(!front) size
- | de_queue Qback (Q as QUEUE{front,back,size,...}) =
- if (!front = !back)
- then clear_queue Q
- else back := --(!back) size
-
-end (* abstype queue *)
-end (* local *)
-
-
-val magic: 'a -> 'a = fn x => x
-
-(* exception PP_FAIL of string *)
-
-datatype break_style = CONSISTENT | INCONSISTENT
-
-datatype break_info
- = FITS
- | PACK_ONTO_LINE of int
- | ONE_PER_LINE of int
-
-(* Some global values *)
-val INFINITY = 999999
-
-abstype indent_stack = Istack of break_info list Unsynchronized.ref
-with
- fun mk_indent_stack() = Istack (Unsynchronized.ref([]:break_info list))
- fun clear_indent_stack (Istack stk) = (stk := ([]:break_info list))
- fun top (Istack stk) =
- case !stk
- of nil => raise Fail "PP-error: top: badly formed block"
- | x::_ => x
- fun push (x,(Istack stk)) = stk := x::(!stk)
- fun pop (Istack stk) =
- case !stk
- of nil => raise Fail "PP-error: pop: badly formed block"
- | _::rest => stk := rest
-end
-
-(* The delim_stack is used to compute the size of blocks. It is
- a stack of indices into the token buffer. The indices only point to
- BBs, Es, and BRs. We push BBs and Es onto the stack until a BR
- is encountered. Then we compute sizes and pop. When we encounter
- a BR in the middle of a block, we compute the Distance_to_next_break
- of the previous BR in the block, if there was one.
-
- We need to be able to delete from the bottom of the delim_stack, so
- we use a queue, treated with a stack discipline, i.e., we only add
- items at the head of the queue, but can delete from the front or
- back of the queue.
-*)
-abstype delim_stack = Dstack of int queue
-with
- fun new_delim_stack i = Dstack(mk_queue i ~1)
- fun reset_delim_stack (Dstack q) = clear_queue q
-
- fun pop_delim_stack (Dstack d) = de_queue Qfront d
- fun pop_bottom_delim_stack (Dstack d) = de_queue Qback d
-
- fun push_delim_stack(i,Dstack d) = en_queue Qfront i d
- fun top_delim_stack (Dstack d) = queue_at Qfront d
- fun bottom_delim_stack (Dstack d) = queue_at Qback d
- fun delim_stack_is_empty (Dstack d) = is_empty d
-end
-
-
-type block_info = { Block_size : int Unsynchronized.ref,
- Block_offset : int,
- How_to_indent : break_style }
-
-
-(* Distance_to_next_break includes Number_of_blanks. Break_offset is
- a local offset for the break. BB represents a sequence of contiguous
- Begins. E represents a sequence of contiguous Ends.
-*)
-datatype pp_token
- = S of {String : string, Length : int}
- | BB of {Pblocks : block_info list Unsynchronized.ref, (* Processed *)
- Ublocks : block_info list Unsynchronized.ref} (* Unprocessed *)
- | E of {Pend : int Unsynchronized.ref, Uend : int Unsynchronized.ref}
- | BR of {Distance_to_next_break : int Unsynchronized.ref,
- Number_of_blanks : int,
- Break_offset : int}
-
-
-(* The initial values in the token buffer *)
-val initial_token_value = S{String = "", Length = 0}
-
-(* type ppstream = General.ppstream; *)
-datatype ppstream_ =
- PPS of
- {consumer : string -> unit,
- linewidth : int,
- flush : unit -> unit,
- the_token_buffer : pp_token array,
- the_delim_stack : delim_stack,
- the_indent_stack : indent_stack,
- ++ : int Unsynchronized.ref -> unit, (* increment circular buffer index *)
- space_left : int Unsynchronized.ref, (* remaining columns on page *)
- left_index : int Unsynchronized.ref, (* insertion index *)
- right_index : int Unsynchronized.ref, (* output index *)
- left_sum : int Unsynchronized.ref, (* size of strings and spaces inserted *)
- right_sum : int Unsynchronized.ref} (* size of strings and spaces printed *)
-
-type ppstream = ppstream_
-
-type ppconsumer = {consumer : string -> unit,
- linewidth : int,
- flush : unit -> unit}
-
-fun mk_ppstream {consumer,linewidth,flush} =
- if (linewidth<5)
- then raise Fail "PP-error: linewidth too_small"
- else let val buf_size = 3*linewidth
- in magic(
- PPS{consumer = consumer,
- linewidth = linewidth,
- flush = flush,
- the_token_buffer = array(buf_size, initial_token_value),
- the_delim_stack = new_delim_stack buf_size,
- the_indent_stack = mk_indent_stack (),
- ++ = fn i => i := ((!i + 1) mod buf_size),
- space_left = Unsynchronized.ref linewidth,
- left_index = Unsynchronized.ref 0, right_index = Unsynchronized.ref 0,
- left_sum = Unsynchronized.ref 0, right_sum = Unsynchronized.ref 0}
- ) : ppstream
- end
-
-fun dest_ppstream(pps : ppstream) =
- let val PPS{consumer,linewidth,flush, ...} = magic pps
- in {consumer=consumer,linewidth=linewidth,flush=flush} end
-
-local
- val space = " "
- fun mk_space (0,s) = String.concat s
- | mk_space (n,s) = mk_space((n-1), (space::s))
- val space_table = Vector.tabulate(100, fn i => mk_space(i,[]))
- fun nspaces n = Vector.sub(space_table, n)
- handle General.Subscript =>
- if n < 0
- then ""
- else let val n2 = n div 2
- val n2_spaces = nspaces n2
- val extra = if (n = (2*n2)) then "" else space
- in String.concat [n2_spaces, n2_spaces, extra]
- end
-in
- fun cr_indent (ofn, i) = ofn ("\n"^(nspaces i))
- fun indent (ofn,i) = ofn (nspaces i)
-end
-
-
-(* Print a the first member of a contiguous sequence of Begins. If there
- are "processed" Begins, then take the first off the list. If there are
- no processed Begins, take the last member off the "unprocessed" list.
- This works because the unprocessed list is treated as a stack, the
- processed list as a FIFO queue. How can an item on the unprocessed list
- be printable? Because of what goes on in add_string. See there for details.
-*)
-
-fun print_BB (_,{Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =
- raise Fail "PP-error: print_BB"
- | print_BB (PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
- {Pblocks as Unsynchronized.ref({How_to_indent=CONSISTENT,Block_size,
- Block_offset}::rst),
- Ublocks=Unsynchronized.ref[]}) =
- (push ((if (!Block_size > sp_left)
- then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
- else FITS),
- the_indent_stack);
- Pblocks := rst)
- | print_BB(PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
- {Pblocks as Unsynchronized.ref({Block_size,Block_offset,...}::rst),Ublocks=Unsynchronized.ref[]}) =
- (push ((if (!Block_size > sp_left)
- then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
- else FITS),
- the_indent_stack);
- Pblocks := rst)
- | print_BB (PPS{the_indent_stack, linewidth, space_left=Unsynchronized.ref sp_left,...},
- {Ublocks,...}) =
- let fun pr_end_Ublock [{How_to_indent=CONSISTENT,Block_size,Block_offset}] l =
- (push ((if (!Block_size > sp_left)
- then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
- else FITS),
- the_indent_stack);
- List.rev l)
- | pr_end_Ublock [{Block_size,Block_offset,...}] l =
- (push ((if (!Block_size > sp_left)
- then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
- else FITS),
- the_indent_stack);
- List.rev l)
- | pr_end_Ublock (a::rst) l = pr_end_Ublock rst (a::l)
- | pr_end_Ublock _ _ =
- raise Fail "PP-error: print_BB: internal error"
- in Ublocks := pr_end_Ublock(!Ublocks) []
- end
-
-
-(* Uend should always be 0 when print_E is called. *)
-fun print_E (_,{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
- raise Fail "PP-error: print_E"
- | print_E (istack,{Pend, ...}) =
- let fun pop_n_times 0 = ()
- | pop_n_times n = (pop istack; pop_n_times(n-1))
- in pop_n_times(!Pend); Pend := 0
- end
-
-
-(* "cursor" is how many spaces across the page we are. *)
-
-fun print_token(PPS{consumer,space_left,...}, S{String,Length}) =
- (consumer String;
- space_left := (!space_left) - Length)
- | print_token(ppstrm,BB b) = print_BB(ppstrm,b)
- | print_token(PPS{the_indent_stack,...},E e) =
- print_E (the_indent_stack,e)
- | print_token (PPS{the_indent_stack,space_left,consumer,linewidth,...},
- BR{Distance_to_next_break,Number_of_blanks,Break_offset}) =
- (case (top the_indent_stack)
- of FITS =>
- (space_left := (!space_left) - Number_of_blanks;
- indent (consumer,Number_of_blanks))
- | (ONE_PER_LINE cursor) =>
- let val new_cursor = cursor + Break_offset
- in space_left := linewidth - new_cursor;
- cr_indent (consumer,new_cursor)
- end
- | (PACK_ONTO_LINE cursor) =>
- if (!Distance_to_next_break > (!space_left))
- then let val new_cursor = cursor + Break_offset
- in space_left := linewidth - new_cursor;
- cr_indent(consumer,new_cursor)
- end
- else (space_left := !space_left - Number_of_blanks;
- indent (consumer,Number_of_blanks)))
-
-
-fun clear_ppstream(pps : ppstream) =
- let val PPS{the_token_buffer, the_delim_stack,
- the_indent_stack,left_sum, right_sum,
- left_index, right_index,space_left,linewidth,...}
- = magic pps
- val buf_size = 3*linewidth
- fun set i =
- if (i = buf_size)
- then ()
- else (update(the_token_buffer,i,initial_token_value);
- set (i+1))
- in set 0;
- clear_indent_stack the_indent_stack;
- reset_delim_stack the_delim_stack;
- left_sum := 0; right_sum := 0;
- left_index := 0; right_index := 0;
- space_left := linewidth
- end
-
-
-(* Move insertion head to right unless adding a BB and already at a BB,
- or unless adding an E and already at an E.
-*)
-fun BB_inc_right_index(PPS{the_token_buffer, right_index, ++,...})=
- case (the_token_buffer sub (!right_index))
- of (BB _) => ()
- | _ => ++right_index
-
-fun E_inc_right_index(PPS{the_token_buffer,right_index, ++,...})=
- case (the_token_buffer sub (!right_index))
- of (E _) => ()
- | _ => ++right_index
-
-
-fun pointers_coincide(PPS{left_index,right_index,the_token_buffer,...}) =
- (!left_index = !right_index) andalso
- (case (the_token_buffer sub (!left_index))
- of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) => true
- | (BB _) => false
- | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) => true
- | (E _) => false
- | _ => true)
-
-fun advance_left (ppstrm as PPS{consumer,left_index,left_sum,
- the_token_buffer,++,...},
- instr) =
- let val NEG = ~1
- val POS = 0
- fun inc_left_sum (BR{Number_of_blanks, ...}) =
- left_sum := (!left_sum) + Number_of_blanks
- | inc_left_sum (S{Length, ...}) = left_sum := (!left_sum) + Length
- | inc_left_sum _ = ()
-
- fun last_size [{Block_size, ...}:block_info] = !Block_size
- | last_size (_::rst) = last_size rst
- | last_size _ = raise Fail "PP-error: last_size: internal error"
- fun token_size (S{Length, ...}) = Length
- | token_size (BB b) =
- (case b
- of {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []} =>
- raise Fail "PP-error: BB_size"
- | {Pblocks as Unsynchronized.ref(_::_),Ublocks=Unsynchronized.ref[]} => POS
- | {Ublocks, ...} => last_size (!Ublocks))
- | token_size (E{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
- raise Fail "PP-error: token_size.E"
- | token_size (E{Pend = Unsynchronized.ref 0, ...}) = NEG
- | token_size (E _) = POS
- | token_size (BR {Distance_to_next_break, ...}) = !Distance_to_next_break
- fun loop (instr) =
- if (token_size instr < 0) (* synchronization point; cannot advance *)
- then ()
- else (print_token(ppstrm,instr);
- inc_left_sum instr;
- if (pointers_coincide ppstrm)
- then ()
- else (* increment left index *)
-
- (* When this is evaluated, we know that the left_index has not yet
- caught up to the right_index. If we are at a BB or an E, we can
- increment left_index if there is no work to be done, i.e., all Begins
- or Ends have been dealt with. Also, we should do some housekeeping and
- clear the buffer at left_index, otherwise we can get errors when
- left_index catches up to right_index and we reset the indices to 0.
- (We might find ourselves adding a BB to an "old" BB, with the result
- that the index is not pushed onto the delim_stack. This can lead to
- mangled output.)
- *)
- (case (the_token_buffer sub (!left_index))
- of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =>
- (update(the_token_buffer,!left_index,
- initial_token_value);
- ++left_index)
- | (BB _) => ()
- | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =>
- (update(the_token_buffer,!left_index,
- initial_token_value);
- ++left_index)
- | (E _) => ()
- | _ => ++left_index;
- loop (the_token_buffer sub (!left_index))))
- in loop instr
- end
-
-
-fun begin_block (pps : ppstream) style offset =
- let val ppstrm = magic pps : ppstream_
- val PPS{the_token_buffer, the_delim_stack,left_index,
- left_sum, right_index, right_sum,...}
- = ppstrm
- in
- (if (delim_stack_is_empty the_delim_stack)
- then (left_index := 0;
- left_sum := 1;
- right_index := 0;
- right_sum := 1)
- else BB_inc_right_index ppstrm;
- case (the_token_buffer sub (!right_index))
- of (BB {Ublocks, ...}) =>
- Ublocks := {Block_size = Unsynchronized.ref (~(!right_sum)),
- Block_offset = offset,
- How_to_indent = style}::(!Ublocks)
- | _ => (update(the_token_buffer, !right_index,
- BB{Pblocks = Unsynchronized.ref [],
- Ublocks = Unsynchronized.ref [{Block_size = Unsynchronized.ref (~(!right_sum)),
- Block_offset = offset,
- How_to_indent = style}]});
- push_delim_stack (!right_index, the_delim_stack)))
- end
-
-fun end_block(pps : ppstream) =
- let val ppstrm = magic pps : ppstream_
- val PPS{the_token_buffer,the_delim_stack,right_index,...}
- = ppstrm
- in
- if (delim_stack_is_empty the_delim_stack)
- then print_token(ppstrm,(E{Pend = Unsynchronized.ref 1, Uend = Unsynchronized.ref 0}))
- else (E_inc_right_index ppstrm;
- case (the_token_buffer sub (!right_index))
- of (E{Uend, ...}) => Uend := !Uend + 1
- | _ => (update(the_token_buffer,!right_index,
- E{Uend = Unsynchronized.ref 1, Pend = Unsynchronized.ref 0});
- push_delim_stack (!right_index, the_delim_stack)))
- end
-
-local
- fun check_delim_stack(PPS{the_token_buffer,the_delim_stack,right_sum,...}) =
- let fun check k =
- if (delim_stack_is_empty the_delim_stack)
- then ()
- else case(the_token_buffer sub (top_delim_stack the_delim_stack))
- of (BB{Ublocks as Unsynchronized.ref ((b as {Block_size, ...})::rst),
- Pblocks}) =>
- if (k>0)
- then (Block_size := !right_sum + !Block_size;
- Pblocks := b :: (!Pblocks);
- Ublocks := rst;
- if (List.length rst = 0)
- then pop_delim_stack the_delim_stack
- else ();
- check(k-1))
- else ()
- | (E{Pend,Uend}) =>
- (Pend := (!Pend) + (!Uend);
- Uend := 0;
- pop_delim_stack the_delim_stack;
- check(k + !Pend))
- | (BR{Distance_to_next_break, ...}) =>
- (Distance_to_next_break :=
- !right_sum + !Distance_to_next_break;
- pop_delim_stack the_delim_stack;
- if (k>0)
- then check k
- else ())
- | _ => raise Fail "PP-error: check_delim_stack.catchall"
- in check 0
- end
-in
-
- fun add_break (pps : ppstream) (n, break_offset) =
- let val ppstrm = magic pps : ppstream_
- val PPS{the_token_buffer,the_delim_stack,left_index,
- right_index,left_sum,right_sum, ++, ...}
- = ppstrm
- in
- (if (delim_stack_is_empty the_delim_stack)
- then (left_index := 0; right_index := 0;
- left_sum := 1; right_sum := 1)
- else ++right_index;
- update(the_token_buffer, !right_index,
- BR{Distance_to_next_break = Unsynchronized.ref (~(!right_sum)),
- Number_of_blanks = n,
- Break_offset = break_offset});
- check_delim_stack ppstrm;
- right_sum := (!right_sum) + n;
- push_delim_stack (!right_index,the_delim_stack))
- end
-
- fun flush_ppstream0(pps : ppstream) =
- let val ppstrm = magic pps : ppstream_
- val PPS{the_delim_stack,the_token_buffer, flush, left_index,...}
- = ppstrm
- in
- (if (delim_stack_is_empty the_delim_stack)
- then ()
- else (check_delim_stack ppstrm;
- advance_left(ppstrm, the_token_buffer sub (!left_index)));
- flush())
- end
-
-end (* local *)
-
-
-fun flush_ppstream ppstrm =
- (flush_ppstream0 ppstrm;
- clear_ppstream ppstrm)
-
-fun add_string (pps : ppstream) s =
- let val ppstrm = magic pps : ppstream_
- val PPS{the_token_buffer,the_delim_stack,consumer,
- right_index,right_sum,left_sum,
- left_index,space_left,++,...}
- = ppstrm
- fun fnl [{Block_size, ...}:block_info] = Block_size := INFINITY
- | fnl (_::rst) = fnl rst
- | fnl _ = raise Fail "PP-error: fnl: internal error"
-
- fun set(dstack,BB{Ublocks as Unsynchronized.ref[{Block_size,...}:block_info],...}) =
- (pop_bottom_delim_stack dstack;
- Block_size := INFINITY)
- | set (_,BB {Ublocks = Unsynchronized.ref(_::rst), ...}) = fnl rst
- | set (dstack, E{Pend,Uend}) =
- (Pend := (!Pend) + (!Uend);
- Uend := 0;
- pop_bottom_delim_stack dstack)
- | set (dstack,BR{Distance_to_next_break,...}) =
- (pop_bottom_delim_stack dstack;
- Distance_to_next_break := INFINITY)
- | set _ = raise (Fail "PP-error: add_string.set")
-
- fun check_stream () =
- if ((!right_sum - !left_sum) > !space_left)
- then if (delim_stack_is_empty the_delim_stack)
- then ()
- else let val i = bottom_delim_stack the_delim_stack
- in if (!left_index = i)
- then set (the_delim_stack, the_token_buffer sub i)
- else ();
- advance_left(ppstrm,
- the_token_buffer sub (!left_index));
- if (pointers_coincide ppstrm)
- then ()
- else check_stream ()
- end
- else ()
-
- val slen = String.size s
- val S_token = S{String = s, Length = slen}
-
- in if (delim_stack_is_empty the_delim_stack)
- then print_token(ppstrm,S_token)
- else (++right_index;
- update(the_token_buffer, !right_index, S_token);
- right_sum := (!right_sum)+slen;
- check_stream ())
- end
-
-
-(* Derived form. The +2 is for peace of mind *)
-fun add_newline (pps : ppstream) =
- let val PPS{linewidth, ...} = magic pps
- in add_break pps (linewidth+2,0) end
-
-(* Derived form. Builds a ppstream, sends pretty printing commands called in
- f to the ppstream, then flushes ppstream.
-*)
-
-fun with_pp ppconsumer ppfn =
- let val ppstrm = mk_ppstream ppconsumer
- in ppfn ppstrm;
- flush_ppstream0 ppstrm
- end
- handle Fail msg =>
- (TextIO.print (">>>> Pretty-printer failure: " ^ msg ^ "\n"))
-
-fun pp_to_string linewidth ppfn ob =
- let val l = Unsynchronized.ref ([]:string list)
- fun attach s = l := (s::(!l))
- in with_pp {consumer = attach, linewidth=linewidth, flush = fn()=>()}
- (fn ppstrm => ppfn ppstrm ob);
- String.concat(List.rev(!l))
- end
-end
-end;
-
(**** Original file: Useful.sig ****)
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001-2005 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Useful =
@@ -991,8 +258,6 @@
exception Bug of string
-val partial : exn -> ('a -> 'b option) -> 'a -> 'b
-
val total : ('a -> 'b) -> 'a -> 'b option
val can : ('a -> 'b) -> 'a -> bool
@@ -1023,10 +288,6 @@
val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a
-val equal : ''a -> ''a -> bool
-
-val notEqual : ''a -> ''a -> bool
-
(* ------------------------------------------------------------------------- *)
(* Pairs. *)
(* ------------------------------------------------------------------------- *)
@@ -1060,6 +321,33 @@
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. *)
(* ------------------------------------------------------------------------- *)
@@ -1073,15 +361,11 @@
val first : ('a -> 'b option) -> 'a list -> 'b option
-val index : ('a -> bool) -> 'a list -> int 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 enumerate : 'a list -> (int * 'a) list
-
-val zipwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+val zipWith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val zip : 'a list -> 'b list -> ('a * 'b) list
@@ -1091,6 +375,24 @@
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 *)
@@ -1122,23 +424,6 @@
val distinct : ''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 (* true < false *)
-
-(* ------------------------------------------------------------------------- *)
(* Sorting and searching. *)
(* ------------------------------------------------------------------------- *)
@@ -1186,12 +471,24 @@
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. *)
(* ------------------------------------------------------------------------- *)
@@ -1248,9 +545,11 @@
val date : unit -> string
+val readDirectory : {directory : string} -> {filename : string} list
+
val readTextFile : {filename : string} -> string
-val writeTextFile : {filename : string, contents : string} -> unit
+val writeTextFile : {contents : string, filename : string} -> unit
(* ------------------------------------------------------------------------- *)
(* Profiling and error reporting. *)
@@ -1258,6 +557,8 @@
val try : ('a -> 'b) -> 'a -> 'b
+val chat : string -> unit
+
val warn : string -> unit
val die : string -> 'exit
@@ -1274,7 +575,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
+nonfix ++ -- RL;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -1283,43 +584,62 @@
(* ========================================================================= *)
(* ML UTILITY FUNCTIONS *)
-(* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Useful :> Useful =
struct
(* ------------------------------------------------------------------------- *)
-(* Exceptions *)
+(* Exceptions. *)
(* ------------------------------------------------------------------------- *)
exception Error of string;
exception Bug of string;
-fun errorToString (Error message) = "\nError: " ^ message ^ "\n"
- | errorToString _ = raise Bug "errorToString: not an Error exception";
-
-fun bugToString (Bug message) = "\nBug: " ^ message ^ "\n"
- | bugToString _ = raise Bug "bugToString: not a Bug exception";
+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;
-fun partial (e as Error _) f x = (case f x of SOME y => y | NONE => raise e)
- | partial _ _ _ = raise Bug "partial: must take an Error exception";
-
-(* ------------------------------------------------------------------------- *)
-(* Tracing *)
+(* ------------------------------------------------------------------------- *)
+(* Tracing. *)
(* ------------------------------------------------------------------------- *)
val tracePrint = Unsynchronized.ref print;
-fun trace message = !tracePrint message;
-
-(* ------------------------------------------------------------------------- *)
-(* Combinators *)
+fun trace mesg = !tracePrint mesg;
+
+(* ------------------------------------------------------------------------- *)
+(* Combinators. *)
(* ------------------------------------------------------------------------- *)
fun C f x y = f y x;
@@ -1343,12 +663,8 @@
f
end;
-val equal = fn x => fn y => x = y;
-
-val notEqual = fn x => fn y => x <> y;
-
-(* ------------------------------------------------------------------------- *)
-(* Pairs *)
+(* ------------------------------------------------------------------------- *)
+(* Pairs. *)
(* ------------------------------------------------------------------------- *)
fun fst (x,_) = x;
@@ -1366,7 +682,7 @@
val op## = fn (f,g) => fn (x,y) => (f x, g y);
(* ------------------------------------------------------------------------- *)
-(* State transformers *)
+(* State transformers. *)
(* ------------------------------------------------------------------------- *)
val unit : 'a -> 's -> 'a * 's = pair;
@@ -1380,118 +696,21 @@
fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end;
(* ------------------------------------------------------------------------- *)
-(* 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 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 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 enumerate l = fst (maps (fn x => fn m => ((m, x), m + 1)) l 0);
-
-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 => rev (z [] xs ys)
- end;
-
-fun zip xs ys = zipwith pair xs ys;
-
-fun unzip ab =
- foldl (fn ((x, y), (xs, ys)) => (x :: xs, y :: ys)) ([], []) (rev ab);
-
-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' = rev xs in aux xs' [] xs' (rev ys) end
- end;
-
-fun cart xs ys = cartwith pair xs ys;
-
-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 (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;
-
-fun setify s = rev (foldl (fn (v,x) => if mem v x then x else v :: x) [] s);
-
-fun union s t = foldl (fn (v,x) => if mem v t then x else v :: x) t (rev s);
-
-fun intersect s t =
- foldl (fn (v,x) => if mem v t then v :: x else x) [] (rev s);
-
-fun difference s t =
- foldl (fn (v,x) => if mem v t then x else v :: x) [] (rev s);
-
-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;
+(* 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. *)
@@ -1527,11 +746,196 @@
| optionCompare _ (_,NONE) = GREATER
| optionCompare cmp (SOME x, SOME y) = cmp (x,y);
-fun boolCompare (true,false) = LESS
- | boolCompare (false,true) = GREATER
+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 => rev (z [] xs ys)
+ end;
+
+fun zip xs ys = zipWith pair xs ys;
+
+fun unzip ab =
+ foldl (fn ((x, y), (xs, ys)) => (x :: xs, y :: ys)) ([], []) (rev ab);
+
+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' = rev xs in aux xs' [] xs' (rev ys) end
+ end;
+
+fun cart xs ys = cartwith pair xs ys;
+
+fun takeWhile p =
+ let
+ fun f acc [] = rev acc
+ | f acc (x :: xs) = if p x then f (x :: acc) xs else 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 [] = (rev acc, [])
+ | f acc (l as x :: xs) = if p x then f (x :: acc) xs else (rev acc, l)
+ in
+ f []
+ end;
+
+fun groups f =
+ let
+ fun group acc row x l =
+ case l of
+ [] =>
+ let
+ val acc = if null row then acc else rev row :: acc
+ in
+ rev acc
+ end
+ | h :: t =>
+ let
+ val (eor,x) = f (h,x)
+ in
+ if eor then group (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), map snd l);
+in
+ fun groupsByFst l = 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 (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;
+
+fun setify s = rev (foldl (fn (v,x) => if mem v x then x else v :: x) [] s);
+
+fun union s t = foldl (fn (v,x) => if mem v t then x else v :: x) t (rev s);
+
+fun intersect s t =
+ foldl (fn (v,x) => if mem v t then v :: x else x) [] (rev s);
+
+fun difference s t =
+ foldl (fn (v,x) => if mem v t then x else v :: x) [] (rev s);
+
+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. *)
(* ------------------------------------------------------------------------- *)
@@ -1584,7 +988,7 @@
| l as [_] => l
| h :: t => mergePairs (findRuns [] h [] t)
end;
-
+
fun sortMap _ _ [] = []
| sortMap _ _ (l as [_]) = l
| sortMap f cmp xs =
@@ -1622,49 +1026,49 @@
end;
local
- fun both f g n = f n andalso g n;
-
- fun next f = let fun nx x = if f x then x else nx (x + 1) in nx end;
-
- fun looking res 0 _ _ = rev res
- | looking res n f x =
- let
- val p = next f x
- val res' = p :: res
- val f' = both f (not o divides p)
- in
- looking res' (n - 1) f' (p + 1)
- end;
-
- fun calcPrimes n = looking [] n (K true) 2
-
- val primesList = Unsynchronized.ref (calcPrimes 10);
-in
- fun primes n = CRITICAL (fn () =>
- if length (!primesList) <= n then List.take (!primesList,n)
+ fun calcPrimes ps n i =
+ if List.exists (fn p => divides p i) ps then calcPrimes ps n (i + 1)
else
let
- val l = calcPrimes n
- val () = primesList := l
- in
- l
- end);
-
- fun primesUpTo n = CRITICAL (fn () =>
- let
- fun f k [] =
- let
- val l = calcPrimes (2 * k)
- val () = primesList := l
- in
- f k (List.drop (l,k))
- end
- | f k (p :: ps) =
- if p <= n then f (k + 1) ps else List.take (!primesList, k)
- in
- f 0 (!primesList)
- end);
-end;
+ val ps = ps @ [i]
+ and n = n - 1
+ in
+ if n = 0 then ps else calcPrimes ps n (i + 1)
+ end;
+
+ val primesList = Unsynchronized.ref [2];
+in
+ fun primes n =
+ let
+ val Unsynchronized.ref ps = primesList
+
+ val k = n - length ps
+ in
+ if k <= 0 then List.take (ps,n)
+ else
+ let
+ val ps = calcPrimes ps k (List.last ps + 1)
+
+ val () = primesList := ps
+ in
+ ps
+ end
+ end;
+end;
+
+fun primesUpTo n =
+ let
+ fun f k =
+ let
+ val l = primes k
+
+ val p = List.last l
+ in
+ if p < n then f (2 * k) else takeWhile (fn j => j <= n) l
+ end
+ in
+ f 8
+ end;
(* ------------------------------------------------------------------------- *)
(* Strings. *)
@@ -1732,7 +1136,8 @@
val trim = implode o chop o rev o chop o rev o explode;
end;
-fun join _ [] = "" | join s (h :: t) = foldl (fn (x,y) => y ^ s ^ x) h t;
+fun join _ [] = ""
+ | join s (h :: t) = foldl (fn (x,y) => y ^ s ^ x) h t;
local
fun match [] l = SOME l
@@ -1755,23 +1160,58 @@
end;
end;
-(***
-fun pluralize {singular,plural} = fn 1 => singular | _ => plural;
-***)
+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 = String.isPrefix p s orelse raise Error "destPrefix"
+ fun check s =
+ if String.isPrefix p s then ()
+ else raise Error "destPrefix"
val sizeP = size p
in
- fn s => (check s; String.extract (s,sizeP,NONE))
+ 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. *)
(* ------------------------------------------------------------------------- *)
@@ -1790,13 +1230,20 @@
else padding ^ entry ^ row
end
in
- zipwith pad column
- end;
-
-fun alignTable [] rows = map (K "") rows
- | alignTable [{leftAlign = true, padChar = #" "}] rows = map hd rows
- | alignTable (align :: aligns) rows =
- alignColumn align (map hd rows) (alignTable aligns (map tl rows));
+ zipWith pad column
+ end;
+
+local
+ fun alignTab aligns rows =
+ case aligns of
+ [] => map (K "") rows
+ | [{leftAlign = true, padChar = #" "}] => map hd rows
+ | align :: aligns =>
+ alignColumn align (map hd rows) (alignTab aligns (map tl rows));
+in
+ fun alignTable aligns rows =
+ if null rows then [] else alignTab aligns rows;
+end;
(* ------------------------------------------------------------------------- *)
(* Reals. *)
@@ -1839,22 +1286,22 @@
local
val generator = Unsynchronized.ref 0
in
- fun newInt () = CRITICAL (fn () =>
+ fun newInt () =
let
val n = !generator
val () = generator := n + 1
in
n
- end);
+ end;
fun newInts 0 = []
- | newInts k = CRITICAL (fn () =>
+ | newInts k =
let
val n = !generator
val () = generator := n + k
in
interval n k
- end);
+ end;
end;
fun withRef (r,new) f x =
@@ -1884,17 +1331,43 @@
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
+ 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 {filename,contents} =
+fun writeTextFile {contents,filename} =
let
open TextIO
val h = openOut filename
@@ -1905,11 +1378,13 @@
end;
(* ------------------------------------------------------------------------- *)
-(* Profiling *)
-(* ------------------------------------------------------------------------- *)
-
-local
- fun err x s = TextIO.output (TextIO.stdErr, x ^ ": " ^ s ^ "\n");
+(* Profiling and error reporting. *)
+(* ------------------------------------------------------------------------- *)
+
+fun chat s = TextIO.output (TextIO.stdErr, s ^ "\n");
+
+local
+ fun err x s = chat (x ^ ": " ^ s);
in
fun try f x = f x
handle e as Error _ => (err "try" (errorToString e); raise e)
@@ -1959,7 +1434,7 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Lazy =
@@ -1967,6 +1442,8 @@
type 'a lazy
+val quickly : 'a -> 'a lazy
+
val delay : (unit -> 'a) -> 'a lazy
val force : 'a lazy -> 'a
@@ -1979,7 +1456,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
+nonfix ++ -- RL;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -1988,7 +1465,7 @@
(* ========================================================================= *)
(* SUPPORT FOR LAZY EVALUATION *)
-(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Lazy :> Lazy =
@@ -2000,16 +1477,21 @@
datatype 'a lazy = Lazy of 'a thunk Unsynchronized.ref;
+fun quickly v = Lazy (Unsynchronized.ref (Value v));
+
fun delay f = Lazy (Unsynchronized.ref (Thunk f));
-fun force (Lazy (Unsynchronized.ref (Value v))) = v
- | force (Lazy (s as Unsynchronized.ref (Thunk f))) =
- let
- val v = f ()
- val () = s := Value v
- in
- v
- end;
+fun force (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
@@ -2021,11 +1503,370 @@
end
end;
+(**** Original file: Stream.sig ****)
+
+(* ========================================================================= *)
+(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+signature Stream =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* The stream type. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'a stream = Nil | Cons of 'a * (unit -> 'a stream)
+
+(* If you're wondering how to create an infinite stream: *)
+(* val stream4 = let fun s4 () = Metis.Stream.Cons (4,s4) in s4 () end; *)
+
+(* ------------------------------------------------------------------------- *)
+(* Stream constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val repeat : 'a -> 'a stream
+
+val count : int -> int stream
+
+val funpows : ('a -> 'a) -> 'a -> 'a stream
+
+(* ------------------------------------------------------------------------- *)
+(* Stream versions of standard list operations: these should all terminate. *)
+(* ------------------------------------------------------------------------- *)
+
+val cons : 'a -> (unit -> 'a stream) -> 'a stream
+
+val null : 'a stream -> bool
+
+val hd : 'a stream -> 'a (* raises Empty *)
+
+val tl : 'a stream -> 'a stream (* raises Empty *)
+
+val hdTl : 'a stream -> 'a * 'a stream (* raises Empty *)
+
+val singleton : 'a -> 'a stream
+
+val append : 'a stream -> (unit -> 'a stream) -> 'a stream
+
+val map : ('a -> 'b) -> 'a stream -> 'b stream
+
+val maps :
+ ('a -> 's -> 'b * 's) -> ('s -> 'b stream) -> 's -> 'a stream -> 'b stream
+
+val zipwith : ('a -> 'b -> 'c) -> 'a stream -> 'b stream -> 'c stream
+
+val zip : 'a stream -> 'b stream -> ('a * 'b) stream
+
+val take : int -> 'a stream -> 'a stream (* raises Subscript *)
+
+val drop : int -> 'a stream -> 'a stream (* raises Subscript *)
+
+(* ------------------------------------------------------------------------- *)
+(* Stream versions of standard list operations: these might not terminate. *)
+(* ------------------------------------------------------------------------- *)
+
+val length : 'a stream -> int
+
+val exists : ('a -> bool) -> 'a stream -> bool
+
+val all : ('a -> bool) -> 'a stream -> bool
+
+val filter : ('a -> bool) -> 'a stream -> 'a stream
+
+val foldl : ('a * 's -> 's) -> 's -> 'a stream -> 's
+
+val concat : 'a stream stream -> 'a stream
+
+val mapPartial : ('a -> 'b option) -> 'a stream -> 'b stream
+
+val mapsPartial :
+ ('a -> 's -> 'b option * 's) -> ('s -> 'b stream) -> 's ->
+ 'a stream -> 'b stream
+
+val mapConcat : ('a -> 'b stream) -> 'a stream -> 'b stream
+
+val mapsConcat :
+ ('a -> 's -> 'b stream * 's) -> ('s -> 'b stream) -> 's ->
+ 'a stream -> 'b stream
+
+(* ------------------------------------------------------------------------- *)
+(* Stream operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val memoize : 'a stream -> 'a stream
+
+val listConcat : 'a list stream -> 'a stream
+
+val concatList : 'a stream list -> 'a stream
+
+val toList : 'a stream -> 'a list
+
+val fromList : 'a list -> 'a stream
+
+val toString : char stream -> string
+
+val fromString : string -> char stream
+
+val toTextFile : {filename : string} -> string stream -> unit
+
+val fromTextFile : {filename : string} -> string stream (* line by line *)
+
+end
+
+(**** Original file: Stream.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
+(* ========================================================================= *)
+(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+structure Stream :> Stream =
+struct
+
+val K = Useful.K;
+
+val pair = Useful.pair;
+
+val funpow = Useful.funpow;
+
+(* ------------------------------------------------------------------------- *)
+(* The stream type. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'a stream =
+ Nil
+ | Cons of 'a * (unit -> 'a stream);
+
+(* ------------------------------------------------------------------------- *)
+(* Stream constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun repeat x = let fun rep () = Cons (x,rep) in rep () end;
+
+fun count n = Cons (n, fn () => count (n + 1));
+
+fun funpows f x = Cons (x, fn () => funpows f (f x));
+
+(* ------------------------------------------------------------------------- *)
+(* Stream versions of standard list operations: these should all terminate. *)
+(* ------------------------------------------------------------------------- *)
+
+fun cons h t = Cons (h,t);
+
+fun null Nil = true
+ | null (Cons _) = false;
+
+fun hd Nil = raise Empty
+ | hd (Cons (h,_)) = h;
+
+fun tl Nil = raise Empty
+ | tl (Cons (_,t)) = t ();
+
+fun hdTl s = (hd s, tl s);
+
+fun singleton s = Cons (s, K Nil);
+
+fun append Nil s = s ()
+ | append (Cons (h,t)) s = Cons (h, fn () => append (t ()) s);
+
+fun map f =
+ let
+ fun m Nil = Nil
+ | m (Cons (h,t)) = Cons (f h, m o t)
+ in
+ m
+ end;
+
+fun maps f g =
+ let
+ fun mm s Nil = g s
+ | mm s (Cons (x,xs)) =
+ let
+ val (y,s') = f x s
+ in
+ Cons (y, mm s' o xs)
+ end
+ in
+ mm
+ end;
+
+fun zipwith f =
+ let
+ fun z Nil _ = Nil
+ | z _ Nil = Nil
+ | z (Cons (x,xs)) (Cons (y,ys)) =
+ Cons (f x y, fn () => z (xs ()) (ys ()))
+ in
+ z
+ end;
+
+fun zip s t = zipwith pair s t;
+
+fun take 0 _ = Nil
+ | take n Nil = raise Subscript
+ | take 1 (Cons (x,_)) = Cons (x, K Nil)
+ | take n (Cons (x,xs)) = Cons (x, fn () => take (n - 1) (xs ()));
+
+fun drop n s = funpow n tl s handle Empty => raise Subscript;
+
+(* ------------------------------------------------------------------------- *)
+(* Stream versions of standard list operations: these might not terminate. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun len n Nil = n
+ | len n (Cons (_,t)) = len (n + 1) (t ());
+in
+ fun length s = len 0 s;
+end;
+
+fun exists pred =
+ let
+ fun f Nil = false
+ | f (Cons (h,t)) = pred h orelse f (t ())
+ in
+ f
+ end;
+
+fun all pred = not o exists (not o pred);
+
+fun filter p Nil = Nil
+ | filter p (Cons (x,xs)) =
+ if p x then Cons (x, fn () => filter p (xs ())) else filter p (xs ());
+
+fun foldl f =
+ let
+ fun fold b Nil = b
+ | fold b (Cons (h,t)) = fold (f (h,b)) (t ())
+ in
+ fold
+ end;
+
+fun concat Nil = Nil
+ | concat (Cons (Nil, ss)) = concat (ss ())
+ | concat (Cons (Cons (x, xs), ss)) =
+ Cons (x, fn () => concat (Cons (xs (), ss)));
+
+fun mapPartial f =
+ let
+ fun mp Nil = Nil
+ | mp (Cons (h,t)) =
+ case f h of
+ NONE => mp (t ())
+ | SOME h' => Cons (h', fn () => mp (t ()))
+ in
+ mp
+ end;
+
+fun mapsPartial f g =
+ let
+ fun mp s Nil = g s
+ | mp s (Cons (h,t)) =
+ let
+ val (h,s) = f h s
+ in
+ case h of
+ NONE => mp s (t ())
+ | SOME h => Cons (h, fn () => mp s (t ()))
+ end
+ in
+ mp
+ end;
+
+fun mapConcat f =
+ let
+ fun mc Nil = Nil
+ | mc (Cons (h,t)) = append (f h) (fn () => mc (t ()))
+ in
+ mc
+ end;
+
+fun mapsConcat f g =
+ let
+ fun mc s Nil = g s
+ | mc s (Cons (h,t)) =
+ let
+ val (l,s) = f h s
+ in
+ append l (fn () => mc s (t ()))
+ end
+ in
+ mc
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Stream operations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun memoize Nil = Nil
+ | memoize (Cons (h,t)) = Cons (h, Lazy.memoize (fn () => memoize (t ())));
+
+fun concatList [] = Nil
+ | concatList (h :: t) = append h (fn () => concatList t);
+
+local
+ fun toLst res Nil = rev res
+ | toLst res (Cons (x, xs)) = toLst (x :: res) (xs ());
+in
+ fun toList s = toLst [] s;
+end;
+
+fun fromList [] = Nil
+ | fromList (x :: xs) = Cons (x, fn () => fromList xs);
+
+fun listConcat s = concat (map fromList s);
+
+fun toString s = implode (toList s);
+
+fun fromString s = fromList (explode s);
+
+fun toTextFile {filename = f} s =
+ let
+ val (h,close) =
+ if f = "-" then (TextIO.stdOut, K ())
+ else (TextIO.openOut f, TextIO.closeOut)
+
+ fun toFile Nil = ()
+ | toFile (Cons (x,y)) = (TextIO.output (h,x); toFile (y ()))
+
+ val () = toFile s
+ in
+ close h
+ end;
+
+fun fromTextFile {filename = f} =
+ let
+ val (h,close) =
+ if f = "-" then (TextIO.stdIn, K ())
+ else (TextIO.openIn f, TextIO.closeIn)
+
+ fun strm () =
+ case TextIO.inputLine h of
+ NONE => (close h; Nil)
+ | SOME s => Cons (s,strm)
+ in
+ memoize (strm ())
+ end;
+
+end
+end;
+
(**** Original file: Ordered.sig ****)
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Ordered =
@@ -2061,7 +1902,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
+nonfix ++ -- RL;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2070,51 +1911,3377 @@
(* ========================================================================= *)
(* ORDERED TYPES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure IntOrdered =
struct type t = int val compare = Int.compare end;
+structure 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 StringOrdered =
struct type t = string val compare = String.compare end;
end;
+(**** Original file: Map.sig ****)
+
+(* ========================================================================= *)
+(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+signature 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
+
+(* ------------------------------------------------------------------------- *)
+(* 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
+
+(* ------------------------------------------------------------------------- *)
+(* 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: Map.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
+(* ========================================================================= *)
+(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+structure Map :> Map =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* Importing useful functionality. *)
+(* ------------------------------------------------------------------------- *)
+
+exception Bug = Useful.Bug;
+
+exception Error = Useful.Error;
+
+val pointerEqual = Portable.pointerEqual;
+
+val K = Useful.K;
+
+val randomInt = Portable.randomInt;
+
+val randomWord = 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 "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 "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 "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 "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 "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 =
+ LR of ('key * 'value) * ('key,'value) tree * ('key,'value) node list
+ | RL of ('key * 'value) * ('key,'value) tree * ('key,'value) node list;
+
+fun fromSpineLR nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,right,...} :: nodes =>
+ SOME (LR ((key,value),right,nodes));
+
+fun fromSpineRL nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,left,...} :: nodes =>
+ SOME (RL ((key,value),left,nodes));
+
+fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+
+fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+
+fun treeMkIterator tree = addLR [] tree;
+
+fun treeMkRevIterator tree = addRL [] tree;
+
+fun readIterator iter =
+ case iter of
+ LR (key_value,_,_) => key_value
+ | RL (key_value,_,_) => key_value;
+
+fun advanceIterator iter =
+ case iter of
+ LR (_,tree,nodes) => addLR nodes tree
+ | RL (_,tree,nodes) => addRL 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 =
+ Map of ('key * 'key -> order) * ('key,'value) tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Map debugging functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+fun checkInvariants s m =
+ let
+ val Map (compareKey,tree) = m
+
+ val _ = treeCheckInvariants compareKey tree
+ in
+ m
+ end
+ handle Bug bug => raise Bug (s ^ "\n" ^ "Map.checkInvariants: " ^ bug);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun new compareKey =
+ let
+ val tree = treeNew ()
+ in
+ Map (compareKey,tree)
+ end;
+
+fun singleton compareKey key_value =
+ let
+ val tree = treeSingleton key_value
+ in
+ Map (compareKey,tree)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Map size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun size (Map (_,tree)) = treeSize tree;
+
+fun null m = size m = 0;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+fun peekKey (Map (compareKey,tree)) key = treePeekKey compareKey key tree;
+
+fun peek (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 "Map.get: element not found"
+ | SOME value => value;
+
+fun pick (Map (_,tree)) = treePick tree;
+
+fun nth (Map (_,tree)) n = treeNth n tree;
+
+fun random m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "Map.random: empty"
+ else nth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun insert (Map (compareKey,tree)) key_value =
+ let
+ val tree = treeInsert compareKey key_value tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val insert = fn m => fn kv =>
+ checkInvariants "Map.insert: result"
+ (insert (checkInvariants "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 (Map (compareKey,tree)) dkey =
+ let
+ val tree = treeDelete compareKey dkey tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val delete = fn m => fn k =>
+ checkInvariants "Map.delete: result"
+ (delete (checkInvariants "Map.delete: input" m) k);
+*)
+
+fun remove m key = if inDomain key m then delete m key else m;
+
+fun deletePick (Map (compareKey,tree)) =
+ let
+ val (key_value,tree) = treeDeletePick tree
+ in
+ (key_value, Map (compareKey,tree))
+ end;
+
+(*BasicDebug
+val deletePick = fn m =>
+ let
+ val (kv,m) = deletePick (checkInvariants "Map.deletePick: input" m)
+ in
+ (kv, checkInvariants "Map.deletePick: result" m)
+ end;
+*)
+
+fun deleteNth (Map (compareKey,tree)) n =
+ let
+ val (key_value,tree) = treeDeleteNth n tree
+ in
+ (key_value, Map (compareKey,tree))
+ end;
+
+(*BasicDebug
+val deleteNth = fn m => fn n =>
+ let
+ val (kv,m) = deleteNth (checkInvariants "Map.deleteNth: input" m) n
+ in
+ (kv, checkInvariants "Map.deleteNth: result" m)
+ end;
+*)
+
+fun deleteRandom m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "Map.deleteRandom: empty"
+ else deleteNth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map). *)
+(* ------------------------------------------------------------------------- *)
+
+fun merge {first,second,both} (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeMerge compareKey first second both tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val merge = fn f => fn m1 => fn m2 =>
+ checkInvariants "Map.merge: result"
+ (merge f
+ (checkInvariants "Map.merge: input 1" m1)
+ (checkInvariants "Map.merge: input 2" m2));
+*)
+
+fun union f (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ fun f2 kv = f (kv,kv)
+
+ val tree = treeUnion compareKey f f2 tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val union = fn f => fn m1 => fn m2 =>
+ checkInvariants "Map.union: result"
+ (union f
+ (checkInvariants "Map.union: input 1" m1)
+ (checkInvariants "Map.union: input 2" m2));
+*)
+
+fun intersect f (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeIntersect compareKey f tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val intersect = fn f => fn m1 => fn m2 =>
+ checkInvariants "Map.intersect: result"
+ (intersect f
+ (checkInvariants "Map.intersect: input 1" m1)
+ (checkInvariants "Map.intersect: input 2" m2));
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkIterator (Map (_,tree)) = treeMkIterator tree;
+
+fun mkRevIterator (Map (_,tree)) = treeMkRevIterator tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapPartial f (Map (compareKey,tree)) =
+ let
+ val tree = treeMapPartial f tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val mapPartial = fn f => fn m =>
+ checkInvariants "Map.mapPartial: result"
+ (mapPartial f (checkInvariants "Map.mapPartial: input" m));
+*)
+
+fun map f (Map (compareKey,tree)) =
+ let
+ val tree = treeMap f tree
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val map = fn f => fn m =>
+ checkInvariants "Map.map: result"
+ (map f (checkInvariants "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 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 Map (compareKey,_) = m1
+
+ val io1 = mkIterator m1
+ and io2 = mkIterator m2
+ in
+ equalIterator (equalKey compareKey) equalValue io1 io2
+ end);
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain. *)
+(* ------------------------------------------------------------------------- *)
+
+fun unionDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeUnionDomain compareKey tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val unionDomain = fn m1 => fn m2 =>
+ checkInvariants "Map.unionDomain: result"
+ (unionDomain
+ (checkInvariants "Map.unionDomain: input 1" m1)
+ (checkInvariants "Map.unionDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
+in
+ fun unionListDomain ms =
+ case ms of
+ [] => raise Bug "Map.unionListDomain: no sets"
+ | m :: ms => List.foldl uncurriedUnionDomain m ms;
+end;
+
+fun intersectDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeIntersectDomain compareKey tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val intersectDomain = fn m1 => fn m2 =>
+ checkInvariants "Map.intersectDomain: result"
+ (intersectDomain
+ (checkInvariants "Map.intersectDomain: input 1" m1)
+ (checkInvariants "Map.intersectDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
+in
+ fun intersectListDomain ms =
+ case ms of
+ [] => raise Bug "Map.intersectListDomain: no sets"
+ | m :: ms => List.foldl uncurriedIntersectDomain m ms;
+end;
+
+fun differenceDomain (Map (compareKey,tree1)) (Map (_,tree2)) =
+ let
+ val tree = treeDifferenceDomain compareKey tree1 tree2
+ in
+ Map (compareKey,tree)
+ end;
+
+(*BasicDebug
+val differenceDomain = fn m1 => fn m2 =>
+ checkInvariants "Map.differenceDomain: result"
+ (differenceDomain
+ (checkInvariants "Map.differenceDomain: input 1" m1)
+ (checkInvariants "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 (Map (compareKey,tree1)) (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
+end;
+
+(**** Original file: KeyMap.sig ****)
+
+(* ========================================================================= *)
+(* FINITE MAPS WITH A FIXED KEY TYPE *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+signature KeyMap =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of map keys. *)
+(* ------------------------------------------------------------------------- *)
+
+type key
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val new : unit -> 'a map
+
+val singleton : key * 'a -> 'a map
+
+(* ------------------------------------------------------------------------- *)
+(* 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
+
+(* ------------------------------------------------------------------------- *)
+(* 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: KeyMap.sml ****)
+
+(* ========================================================================= *)
+(* FINITE MAPS WITH A FIXED KEY TYPE *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* Importing from the input signature. *)
+(* ------------------------------------------------------------------------- *)
+
+open Metis; (* MODIFIED by Jasmin Blanchette *)
+
+type key = Key.t;
+
+val compareKey = Key.compare;
+
+(* ------------------------------------------------------------------------- *)
+(* Importing useful functionality. *)
+(* ------------------------------------------------------------------------- *)
+
+exception Bug = Useful.Bug;
+
+exception Error = Useful.Error;
+
+val pointerEqual = Portable.pointerEqual;
+
+val K = Useful.K;
+
+val randomInt = Portable.randomInt;
+
+val randomWord = 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 "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 op 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 op 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 op 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 "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 "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 "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 "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 =
+ LR of (key * 'value) * 'value tree * 'value node list
+ | RL of (key * 'value) * 'value tree * 'value node list;
+
+fun fromSpineLR nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,right,...} :: nodes =>
+ SOME (LR ((key,value),right,nodes));
+
+fun fromSpineRL nodes =
+ case nodes of
+ [] => NONE
+ | Node {key,value,left,...} :: nodes =>
+ SOME (RL ((key,value),left,nodes));
+
+fun addLR nodes tree = fromSpineLR (treeLeftSpine nodes tree);
+
+fun addRL nodes tree = fromSpineRL (treeRightSpine nodes tree);
+
+fun treeMkIterator tree = addLR [] tree;
+
+fun treeMkRevIterator tree = addRL [] tree;
+
+fun readIterator iter =
+ case iter of
+ LR (key_value,_,_) => key_value
+ | RL (key_value,_,_) => key_value;
+
+fun advanceIterator iter =
+ case iter of
+ LR (_,tree,nodes) => addLR nodes tree
+ | RL (_,tree,nodes) => addRL 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 =
+ Map of 'value tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Map debugging functions. *)
+(* ------------------------------------------------------------------------- *)
+
+(*BasicDebug
+fun checkInvariants s m =
+ let
+ val Map tree = m
+
+ val _ = treeCheckInvariants tree
+ in
+ m
+ end
+ handle Bug bug => raise Bug (s ^ "\n" ^ "KeyMap.checkInvariants: " ^ bug);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun new () =
+ let
+ val tree = treeNew ()
+ in
+ Map tree
+ end;
+
+fun singleton key_value =
+ let
+ val tree = treeSingleton key_value
+ in
+ Map tree
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Map size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun size (Map tree) = treeSize tree;
+
+fun null m = size m = 0;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+fun peekKey (Map tree) key = treePeekKey key tree;
+
+fun peek (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 "KeyMap.get: element not found"
+ | SOME value => value;
+
+fun pick (Map tree) = treePick tree;
+
+fun nth (Map tree) n = treeNth n tree;
+
+fun random m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "KeyMap.random: empty"
+ else nth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun insert (Map tree) key_value =
+ let
+ val tree = treeInsert key_value tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val insert = fn m => fn kv =>
+ checkInvariants "KeyMap.insert: result"
+ (insert (checkInvariants "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 (Map tree) dkey =
+ let
+ val tree = treeDelete dkey tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val delete = fn m => fn k =>
+ checkInvariants "KeyMap.delete: result"
+ (delete (checkInvariants "KeyMap.delete: input" m) k);
+*)
+
+fun remove m key = if inDomain key m then delete m key else m;
+
+fun deletePick (Map tree) =
+ let
+ val (key_value,tree) = treeDeletePick tree
+ in
+ (key_value, Map tree)
+ end;
+
+(*BasicDebug
+val deletePick = fn m =>
+ let
+ val (kv,m) = deletePick (checkInvariants "KeyMap.deletePick: input" m)
+ in
+ (kv, checkInvariants "KeyMap.deletePick: result" m)
+ end;
+*)
+
+fun deleteNth (Map tree) n =
+ let
+ val (key_value,tree) = treeDeleteNth n tree
+ in
+ (key_value, Map tree)
+ end;
+
+(*BasicDebug
+val deleteNth = fn m => fn n =>
+ let
+ val (kv,m) = deleteNth (checkInvariants "KeyMap.deleteNth: input" m) n
+ in
+ (kv, checkInvariants "KeyMap.deleteNth: result" m)
+ end;
+*)
+
+fun deleteRandom m =
+ let
+ val n = size m
+ in
+ if n = 0 then raise Bug "KeyMap.deleteRandom: empty"
+ else deleteNth m (randomInt n)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining (all join operations prefer keys in the second map). *)
+(* ------------------------------------------------------------------------- *)
+
+fun merge {first,second,both} (Map tree1) (Map tree2) =
+ let
+ val tree = treeMerge first second both tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val merge = fn f => fn m1 => fn m2 =>
+ checkInvariants "KeyMap.merge: result"
+ (merge f
+ (checkInvariants "KeyMap.merge: input 1" m1)
+ (checkInvariants "KeyMap.merge: input 2" m2));
+*)
+
+fun op union f (Map tree1) (Map tree2) =
+ let
+ fun f2 kv = f (kv,kv)
+
+ val tree = treeUnion f f2 tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val op union = fn f => fn m1 => fn m2 =>
+ checkInvariants "KeyMap.union: result"
+ (union f
+ (checkInvariants "KeyMap.union: input 1" m1)
+ (checkInvariants "KeyMap.union: input 2" m2));
+*)
+
+fun intersect f (Map tree1) (Map tree2) =
+ let
+ val tree = treeIntersect f tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val intersect = fn f => fn m1 => fn m2 =>
+ checkInvariants "KeyMap.intersect: result"
+ (intersect f
+ (checkInvariants "KeyMap.intersect: input 1" m1)
+ (checkInvariants "KeyMap.intersect: input 2" m2));
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over maps. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkIterator (Map tree) = treeMkIterator tree;
+
+fun mkRevIterator (Map tree) = treeMkRevIterator tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapPartial f (Map tree) =
+ let
+ val tree = treeMapPartial f tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val mapPartial = fn f => fn m =>
+ checkInvariants "KeyMap.mapPartial: result"
+ (mapPartial f (checkInvariants "KeyMap.mapPartial: input" m));
+*)
+
+fun map f (Map tree) =
+ let
+ val tree = treeMap f tree
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val map = fn f => fn m =>
+ checkInvariants "KeyMap.map: result"
+ (map f (checkInvariants "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 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 Map _ = m1
+
+ val io1 = mkIterator m1
+ and io2 = mkIterator m2
+ in
+ equalIterator equalValue io1 io2
+ end);
+
+(* ------------------------------------------------------------------------- *)
+(* Set operations on the domain. *)
+(* ------------------------------------------------------------------------- *)
+
+fun unionDomain (Map tree1) (Map tree2) =
+ let
+ val tree = treeUnionDomain tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val unionDomain = fn m1 => fn m2 =>
+ checkInvariants "KeyMap.unionDomain: result"
+ (unionDomain
+ (checkInvariants "KeyMap.unionDomain: input 1" m1)
+ (checkInvariants "KeyMap.unionDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedUnionDomain (m,acc) = unionDomain acc m;
+in
+ fun unionListDomain ms =
+ case ms of
+ [] => raise Bug "KeyMap.unionListDomain: no sets"
+ | m :: ms => List.foldl uncurriedUnionDomain m ms;
+end;
+
+fun intersectDomain (Map tree1) (Map tree2) =
+ let
+ val tree = treeIntersectDomain tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val intersectDomain = fn m1 => fn m2 =>
+ checkInvariants "KeyMap.intersectDomain: result"
+ (intersectDomain
+ (checkInvariants "KeyMap.intersectDomain: input 1" m1)
+ (checkInvariants "KeyMap.intersectDomain: input 2" m2));
+*)
+
+local
+ fun uncurriedIntersectDomain (m,acc) = intersectDomain acc m;
+in
+ fun intersectListDomain ms =
+ case ms of
+ [] => raise Bug "KeyMap.intersectListDomain: no sets"
+ | m :: ms => List.foldl uncurriedIntersectDomain m ms;
+end;
+
+fun differenceDomain (Map tree1) (Map tree2) =
+ let
+ val tree = treeDifferenceDomain tree1 tree2
+ in
+ Map tree
+ end;
+
+(*BasicDebug
+val differenceDomain = fn m1 => fn m2 =>
+ checkInvariants "KeyMap.differenceDomain: result"
+ (differenceDomain
+ (checkInvariants "KeyMap.differenceDomain: input 1" m1)
+ (checkInvariants "KeyMap.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 (Map tree1) (Map tree2) =
+ treeSubsetDomain 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 l =
+ let
+ val m = new ()
+ in
+ insertList m l
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
+
+end
+
+structure IntMap =
+KeyMap (Metis.IntOrdered); (* MODIFIED by Jasmin Blanchette *)
+
+structure IntPairMap =
+KeyMap (Metis.IntPairOrdered); (* MODIFIED by Jasmin Blanchette *)
+
+structure StringMap =
+KeyMap (Metis.StringOrdered); (* MODIFIED by Jasmin Blanchette *)
+
(**** Original file: Set.sig ****)
(* ========================================================================= *)
-(* FINITE SETS *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Set =
sig
(* ------------------------------------------------------------------------- *)
-(* Finite sets *)
+(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
type 'elt set
-val comparison : 'elt set -> ('elt * 'elt -> order)
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
val empty : ('elt * 'elt -> order) -> 'elt set
val singleton : ('elt * 'elt -> order) -> 'elt -> 'elt set
+(* ------------------------------------------------------------------------- *)
+(* Set size. *)
+(* ------------------------------------------------------------------------- *)
+
val null : 'elt set -> bool
val size : 'elt set -> int
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+val peek : 'elt set -> 'elt -> 'elt option
+
val member : 'elt -> 'elt set -> bool
+val pick : 'elt set -> 'elt (* an arbitrary element *)
+
+val nth : 'elt set -> int -> 'elt (* in the range [0,size-1] *)
+
+val random : 'elt set -> 'elt
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
val add : 'elt set -> 'elt -> 'elt set
val addList : 'elt set -> 'elt list -> 'elt set
-val delete : 'elt set -> 'elt -> 'elt set (* raises Error *)
-
-(* Union and intersect prefer elements in the second set *)
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : 'elt set -> 'elt -> 'elt set (* must be present *)
+
+val remove : 'elt set -> 'elt -> 'elt set
+
+val deletePick : 'elt set -> 'elt * 'elt set
+
+val deleteNth : 'elt set -> int -> 'elt * 'elt set
+
+val deleteRandom : 'elt set -> 'elt * 'elt set
+
+(* ------------------------------------------------------------------------- *)
+(* Joining. *)
+(* ------------------------------------------------------------------------- *)
val union : 'elt set -> 'elt set -> 'elt set
@@ -2128,22 +5295,24 @@
val symmetricDifference : 'elt set -> 'elt set -> 'elt set
-val disjoint : 'elt set -> 'elt set -> bool
-
-val subset : 'elt set -> 'elt set -> bool
-
-val equal : 'elt set -> 'elt set -> bool
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
val filter : ('elt -> bool) -> 'elt set -> 'elt set
val partition : ('elt -> bool) -> 'elt set -> 'elt set * 'elt set
-val count : ('elt -> bool) -> 'elt set -> int
+val app : ('elt -> unit) -> 'elt set -> unit
val foldl : ('elt * 's -> 's) -> 's -> 'elt set -> 's
val foldr : ('elt * 's -> 's) -> 's -> 'elt set -> 's
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
val findl : ('elt -> bool) -> 'elt set -> 'elt option
val findr : ('elt -> bool) -> 'elt set -> 'elt option
@@ -2156,27 +5325,45 @@
val all : ('elt -> bool) -> 'elt set -> bool
-val map : ('elt -> 'a) -> 'elt set -> ('elt * 'a) list
+val count : ('elt -> bool) -> 'elt set -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : 'elt set * 'elt set -> order
+
+val equal : 'elt set -> 'elt set -> bool
+
+val subset : 'elt set -> 'elt set -> bool
+
+val disjoint : 'elt set -> 'elt set -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
val transform : ('elt -> 'a) -> 'elt set -> 'a list
-val app : ('elt -> unit) -> 'elt set -> unit
-
val toList : 'elt set -> 'elt list
val fromList : ('elt * 'elt -> order) -> 'elt list -> 'elt set
-val pick : 'elt set -> 'elt (* raises Empty *)
-
-val random : 'elt set -> 'elt (* raises Empty *)
-
-val deletePick : 'elt set -> 'elt * 'elt set (* raises Empty *)
-
-val deleteRandom : 'elt set -> 'elt * 'elt set (* raises Empty *)
-
-val compare : 'elt set * 'elt set -> order
-
-val close : ('elt set -> 'elt set) -> 'elt set -> 'elt set
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type ('elt,'a) map = ('elt,'a) Metis.Map.map
+
+val mapPartial : ('elt -> 'a option) -> 'elt set -> ('elt,'a) map
+
+val map : ('elt -> 'a) -> 'elt set -> ('elt,'a) map
+
+val domain : ('elt,'a) map -> 'elt set
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
val toString : 'elt set -> string
@@ -2196,11 +5383,11 @@
end
-(**** Original file: RandomSet.sml ****)
+(**** Original file: Set.sml ****)
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
+nonfix ++ -- RL;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -2209,667 +5396,414 @@
(* ========================================================================= *)
(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-structure RandomSet :> Set =
-struct
-
-exception Bug = Useful.Bug;
-
-exception Error = Useful.Error;
-
-val pointerEqual = Portable.pointerEqual;
-
-val K = Useful.K;
-
-val snd = Useful.snd;
-
-val randomInt = Portable.randomInt;
-
-val randomWord = Portable.randomWord;
-
-(* ------------------------------------------------------------------------- *)
-(* Random search trees. *)
-(* ------------------------------------------------------------------------- *)
-
-type priority = Word.word;
-
-datatype 'a tree =
- E
- | T of
- {size : int,
- priority : priority,
- left : 'a tree,
- key : 'a,
- right : 'a tree};
-
-type 'a node =
- {size : int,
- priority : priority,
- left : 'a tree,
- key : 'a,
- right : 'a tree};
-
-datatype 'a set = Set of ('a * 'a -> order) * 'a tree;
-
-(* ------------------------------------------------------------------------- *)
-(* Random priorities. *)
-(* ------------------------------------------------------------------------- *)
-
-local
- val randomPriority = randomWord;
-
- val priorityOrder = Word.compare;
-in
- fun treeSingleton key =
- T {size = 1, priority = randomPriority (),
- left = E, key = key, right = E};
-
- fun nodePriorityOrder cmp (x1 : 'a node, x2 : 'a node) =
- let
- val {priority = p1, key = k1, ...} = x1
- and {priority = p2, key = k2, ...} = x2
- in
- case priorityOrder (p1,p2) of
- LESS => LESS
- | EQUAL => cmp (k1,k2)
- | GREATER => GREATER
- end;
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Debugging functions. *)
-(* ------------------------------------------------------------------------- *)
-
-local
- fun checkSizes E = 0
- | checkSizes (T {size,left,right,...}) =
- let
- val l = checkSizes left
- and r = checkSizes right
- val () = if l + 1 + r = size then () else raise Error "wrong size"
- in
- size
- end
-
- fun checkSorted _ x E = x
- | checkSorted cmp x (T {left,key,right,...}) =
- let
- val x = checkSorted cmp x left
- val () =
- case x of
- NONE => ()
- | SOME k =>
- case cmp (k,key) of
- LESS => ()
- | EQUAL => raise Error "duplicate keys"
- | GREATER => raise Error "unsorted"
- in
- checkSorted cmp (SOME key) right
- end;
-
- fun checkPriorities _ E = NONE
- | checkPriorities cmp (T (x as {left,right,...})) =
- let
- val () =
- case checkPriorities cmp left of
- NONE => ()
- | SOME l =>
- case nodePriorityOrder cmp (l,x) of
- LESS => ()
- | EQUAL => raise Error "left child has equal key"
- | GREATER => raise Error "left child has greater priority"
- val () =
- case checkPriorities cmp right of
- NONE => ()
- | SOME r =>
- case nodePriorityOrder cmp (r,x) of
- LESS => ()
- | EQUAL => raise Error "right child has equal key"
- | GREATER => raise Error "right child has greater priority"
- in
- SOME x
- end;
-in
- fun checkWellformed s (set as Set (cmp,tree)) =
- (let
- val _ = checkSizes tree
- val _ = checkSorted cmp NONE tree
- val _ = checkPriorities cmp tree
- in
- set
- end
- handle Error err => raise Bug err)
- handle Bug bug => raise Bug (s ^ "\nRandomSet.checkWellformed: " ^ bug);
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Basic operations. *)
-(* ------------------------------------------------------------------------- *)
-
-fun comparison (Set (cmp,_)) = cmp;
-
-fun empty cmp = Set (cmp,E);
-
-fun treeSize E = 0
- | treeSize (T {size = s, ...}) = s;
-
-fun size (Set (_,tree)) = treeSize tree;
-
-fun mkT p l k r =
- T {size = treeSize l + 1 + treeSize r, priority = p,
- left = l, key = k, right = r};
-
-fun singleton cmp key = Set (cmp, treeSingleton key);
-
-local
- fun treePeek cmp E pkey = NONE
- | treePeek cmp (T {left,key,right,...}) pkey =
- case cmp (pkey,key) of
- LESS => treePeek cmp left pkey
- | EQUAL => SOME key
- | GREATER => treePeek cmp right pkey
-in
- fun peek (Set (cmp,tree)) key = treePeek cmp tree key;
-end;
-
-(* treeAppend assumes that every element of the first tree is less than *)
-(* every element of the second tree. *)
-
-fun treeAppend _ t1 E = t1
- | treeAppend _ E t2 = t2
- | treeAppend cmp (t1 as T x1) (t2 as T x2) =
- case nodePriorityOrder cmp (x1,x2) of
- LESS =>
- let
- val {priority = p2, left = l2, key = k2, right = r2, ...} = x2
- in
- mkT p2 (treeAppend cmp t1 l2) k2 r2
- end
- | EQUAL => raise Bug "RandomSet.treeAppend: equal keys"
- | GREATER =>
- let
- val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
- in
- mkT p1 l1 k1 (treeAppend cmp r1 t2)
- end;
-
-(* nodePartition splits the node into three parts: the keys comparing less *)
-(* than the supplied key, an optional equal key, and the keys comparing *)
-(* greater. *)
-
-local
- fun mkLeft [] t = t
- | mkLeft (({priority,left,key,...} : 'a node) :: xs) t =
- mkLeft xs (mkT priority left key t);
-
- fun mkRight [] t = t
- | mkRight (({priority,key,right,...} : 'a node) :: xs) t =
- mkRight xs (mkT priority t key right);
-
- fun treePart _ _ lefts rights E = (mkLeft lefts E, NONE, mkRight rights E)
- | treePart cmp pkey lefts rights (T x) = nodePart cmp pkey lefts rights x
- and nodePart cmp pkey lefts rights (x as {left,key,right,...}) =
- case cmp (pkey,key) of
- LESS => treePart cmp pkey lefts (x :: rights) left
- | EQUAL => (mkLeft lefts left, SOME key, mkRight rights right)
- | GREATER => treePart cmp pkey (x :: lefts) rights right;
-in
- fun nodePartition cmp x pkey = nodePart cmp pkey [] [] x;
-end;
-
-(* union first calls treeCombineRemove, to combine the values *)
-(* for equal keys into the first map and remove them from the second map. *)
-(* Note that the combined key is always the one from the second map. *)
-
-local
- fun treeCombineRemove _ t1 E = (t1,E)
- | treeCombineRemove _ E t2 = (E,t2)
- | treeCombineRemove cmp (t1 as T x1) (t2 as T x2) =
- let
- val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
- val (l2,k2,r2) = nodePartition cmp x2 k1
- val (l1,l2) = treeCombineRemove cmp l1 l2
- and (r1,r2) = treeCombineRemove cmp r1 r2
- in
- case k2 of
- NONE => if treeSize l2 + treeSize r2 = #size x2 then (t1,t2)
- else (mkT p1 l1 k1 r1, treeAppend cmp l2 r2)
- | SOME k2 => (mkT p1 l1 k2 r1, treeAppend cmp l2 r2)
- end;
-
- fun treeUnionDisjoint _ t1 E = t1
- | treeUnionDisjoint _ E t2 = t2
- | treeUnionDisjoint cmp (T x1) (T x2) =
- case nodePriorityOrder cmp (x1,x2) of
- LESS => nodeUnionDisjoint cmp x2 x1
- | EQUAL => raise Bug "RandomSet.unionDisjoint: equal keys"
- | GREATER => nodeUnionDisjoint cmp x1 x2
-
- and nodeUnionDisjoint cmp x1 x2 =
- let
- val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
- val (l2,_,r2) = nodePartition cmp x2 k1
- val l = treeUnionDisjoint cmp l1 l2
- and r = treeUnionDisjoint cmp r1 r2
- in
- mkT p1 l k1 r
- end;
-in
- fun union (s1 as Set (cmp,t1)) (Set (_,t2)) =
- if pointerEqual (t1,t2) then s1
- else
- let
- val (t1,t2) = treeCombineRemove cmp t1 t2
- in
- Set (cmp, treeUnionDisjoint cmp t1 t2)
- end;
-end;
-
-(*DEBUG
-val union = fn t1 => fn t2 =>
- checkWellformed "RandomSet.union: result"
- (union (checkWellformed "RandomSet.union: input 1" t1)
- (checkWellformed "RandomSet.union: input 2" t2));
-*)
-
-(* intersect is a simple case of the union algorithm. *)
-
-local
- fun treeIntersect _ _ E = E
- | treeIntersect _ E _ = E
- | treeIntersect cmp (t1 as T x1) (t2 as T x2) =
- let
- val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
- val (l2,k2,r2) = nodePartition cmp x2 k1
- val l = treeIntersect cmp l1 l2
- and r = treeIntersect cmp r1 r2
- in
- case k2 of
- NONE => treeAppend cmp l r
- | SOME k2 => mkT p1 l k2 r
- end;
-in
- fun intersect (s1 as Set (cmp,t1)) (Set (_,t2)) =
- if pointerEqual (t1,t2) then s1
- else Set (cmp, treeIntersect cmp t1 t2);
-end;
-
-(*DEBUG
-val intersect = fn t1 => fn t2 =>
- checkWellformed "RandomSet.intersect: result"
- (intersect (checkWellformed "RandomSet.intersect: input 1" t1)
- (checkWellformed "RandomSet.intersect: input 2" t2));
-*)
-
-(* delete raises an exception if the supplied key is not found, which *)
-(* makes it simpler to maximize sharing. *)
-
-local
- fun treeDelete _ E _ = raise Error "RandomSet.delete: element not found"
- | treeDelete cmp (T {priority,left,key,right,...}) dkey =
- case cmp (dkey,key) of
- LESS => mkT priority (treeDelete cmp left dkey) key right
- | EQUAL => treeAppend cmp left right
- | GREATER => mkT priority left key (treeDelete cmp right dkey);
-in
- fun delete (Set (cmp,tree)) key = Set (cmp, treeDelete cmp tree key);
-end;
-
-(*DEBUG
-val delete = fn t => fn x =>
- checkWellformed "RandomSet.delete: result"
- (delete (checkWellformed "RandomSet.delete: input" t) x);
-*)
-
-(* Set difference *)
-
-local
- fun treeDifference _ t1 E = t1
- | treeDifference _ E _ = E
- | treeDifference cmp (t1 as T x1) (T x2) =
- let
- val {size = s1, priority = p1, left = l1, key = k1, right = r1} = x1
- val (l2,k2,r2) = nodePartition cmp x2 k1
- val l = treeDifference cmp l1 l2
- and r = treeDifference cmp r1 r2
- in
- if Option.isSome k2 then treeAppend cmp l r
- else if treeSize l + treeSize r + 1 = s1 then t1
- else mkT p1 l k1 r
- end;
-in
- fun difference (Set (cmp,tree1)) (Set (_,tree2)) =
- if pointerEqual (tree1,tree2) then Set (cmp,E)
- else Set (cmp, treeDifference cmp tree1 tree2);
-end;
-
-(*DEBUG
-val difference = fn t1 => fn t2 =>
- checkWellformed "RandomSet.difference: result"
- (difference (checkWellformed "RandomSet.difference: input 1" t1)
- (checkWellformed "RandomSet.difference: input 2" t2));
-*)
-
-(* Subsets *)
-
-local
- fun treeSubset _ E _ = true
- | treeSubset _ _ E = false
- | treeSubset cmp (t1 as T x1) (T x2) =
- let
- val {size = s1, left = l1, key = k1, right = r1, ...} = x1
- and {size = s2, ...} = x2
- in
- s1 <= s2 andalso
- let
- val (l2,k2,r2) = nodePartition cmp x2 k1
- in
- Option.isSome k2 andalso
- treeSubset cmp l1 l2 andalso
- treeSubset cmp r1 r2
- end
- end;
-in
- fun subset (Set (cmp,tree1)) (Set (_,tree2)) =
- pointerEqual (tree1,tree2) orelse
- treeSubset cmp tree1 tree2;
-end;
-
-(* Set equality *)
-
-local
- fun treeEqual _ E E = true
- | treeEqual _ E _ = false
- | treeEqual _ _ E = false
- | treeEqual cmp (t1 as T x1) (T x2) =
- let
- val {size = s1, left = l1, key = k1, right = r1, ...} = x1
- and {size = s2, ...} = x2
- in
- s1 = s2 andalso
- let
- val (l2,k2,r2) = nodePartition cmp x2 k1
- in
- Option.isSome k2 andalso
- treeEqual cmp l1 l2 andalso
- treeEqual cmp r1 r2
- end
- end;
-in
- fun equal (Set (cmp,tree1)) (Set (_,tree2)) =
- pointerEqual (tree1,tree2) orelse
- treeEqual cmp tree1 tree2;
-end;
-
-(* filter is the basic function for preserving the tree structure. *)
-
-local
- fun treeFilter _ _ E = E
- | treeFilter cmp pred (T {priority,left,key,right,...}) =
- let
- val left = treeFilter cmp pred left
- and right = treeFilter cmp pred right
- in
- if pred key then mkT priority left key right
- else treeAppend cmp left right
- end;
-in
- fun filter pred (Set (cmp,tree)) = Set (cmp, treeFilter cmp pred tree);
-end;
-
-(* nth picks the nth smallest key (counting from 0). *)
-
-local
- fun treeNth E _ = raise Subscript
- | treeNth (T {left,key,right,...}) n =
- let
- val k = treeSize left
- in
- if n = k then key
- else if n < k then treeNth left n
- else treeNth right (n - (k + 1))
- end;
-in
- fun nth (Set (_,tree)) n = treeNth tree n;
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Iterators. *)
-(* ------------------------------------------------------------------------- *)
-
-fun leftSpine E acc = acc
- | leftSpine (t as T {left,...}) acc = leftSpine left (t :: acc);
-
-fun rightSpine E acc = acc
- | rightSpine (t as T {right,...}) acc = rightSpine right (t :: acc);
-
-datatype 'a iterator =
- LR of 'a * 'a tree * 'a tree list
- | RL of 'a * 'a tree * 'a tree list;
-
-fun mkLR [] = NONE
- | mkLR (T {key,right,...} :: l) = SOME (LR (key,right,l))
- | mkLR (E :: _) = raise Bug "RandomSet.mkLR";
-
-fun mkRL [] = NONE
- | mkRL (T {key,left,...} :: l) = SOME (RL (key,left,l))
- | mkRL (E :: _) = raise Bug "RandomSet.mkRL";
-
-fun mkIterator (Set (_,tree)) = mkLR (leftSpine tree []);
-
-fun mkRevIterator (Set (_,tree)) = mkRL (rightSpine tree []);
-
-fun readIterator (LR (key,_,_)) = key
- | readIterator (RL (key,_,_)) = key;
-
-fun advanceIterator (LR (_,next,l)) = mkLR (leftSpine next l)
- | advanceIterator (RL (_,next,l)) = mkRL (rightSpine next l);
-
-(* ------------------------------------------------------------------------- *)
-(* Derived operations. *)
-(* ------------------------------------------------------------------------- *)
-
-fun null s = size s = 0;
-
-fun member x s = Option.isSome (peek s x);
-
-fun add s x = union s (singleton (comparison s) x);
-
-(*DEBUG
-val add = fn s => fn x =>
- checkWellformed "RandomSet.add: result"
- (add (checkWellformed "RandomSet.add: input" s) x);
-*)
-
-local
- fun unionPairs ys [] = rev ys
- | unionPairs ys (xs as [_]) = List.revAppend (ys,xs)
- | unionPairs ys (x1 :: x2 :: xs) = unionPairs (union x1 x2 :: ys) xs;
-in
- fun unionList [] = raise Error "RandomSet.unionList: no sets"
- | unionList [s] = s
- | unionList l = unionList (unionPairs [] l);
-end;
-
-local
- fun intersectPairs ys [] = rev ys
- | intersectPairs ys (xs as [_]) = List.revAppend (ys,xs)
- | intersectPairs ys (x1 :: x2 :: xs) =
- intersectPairs (intersect x1 x2 :: ys) xs;
-in
- fun intersectList [] = raise Error "RandomSet.intersectList: no sets"
- | intersectList [s] = s
- | intersectList l = intersectList (intersectPairs [] l);
-end;
-
-fun symmetricDifference s1 s2 = union (difference s1 s2) (difference s2 s1);
-
-fun disjoint s1 s2 = null (intersect s1 s2);
-
-fun partition pred set = (filter pred set, filter (not o pred) set);
-
-local
- fun fold _ NONE acc = acc
- | fold f (SOME iter) acc =
- let
- val key = readIterator iter
- in
- fold f (advanceIterator iter) (f (key,acc))
- end;
-in
- fun foldl f b m = fold f (mkIterator m) b;
-
- fun foldr f b m = fold f (mkRevIterator m) b;
-end;
-
-local
- fun find _ NONE = NONE
- | find pred (SOME iter) =
- let
- val key = readIterator iter
- in
- if pred key then SOME key
- else find pred (advanceIterator iter)
- end;
-in
- fun findl p m = find p (mkIterator m);
-
- fun findr p m = find p (mkRevIterator m);
-end;
-
-local
- fun first _ NONE = NONE
- | first f (SOME iter) =
- let
- val key = readIterator iter
- in
- case f key of
- NONE => first f (advanceIterator iter)
- | s => s
- end;
-in
- fun firstl f m = first f (mkIterator m);
-
- fun firstr f m = first f (mkRevIterator m);
-end;
-
-fun count p = foldl (fn (x,n) => if p x then n + 1 else n) 0;
-
-fun fromList cmp l = List.foldl (fn (k,s) => add s k) (empty cmp) l;
-
-fun addList s l = union s (fromList (comparison s) l);
-
-fun toList s = foldr op:: [] s;
-
-fun map f s = rev (foldl (fn (x,l) => (x, f x) :: l) [] s);
-
-fun transform f s = rev (foldl (fn (x,l) => f x :: l) [] s);
-
-fun app f s = foldl (fn (x,()) => f x) () s;
-
-fun exists p s = Option.isSome (findl p s);
-
-fun all p s = not (exists (not o p) s);
-
-local
- fun iterCompare _ NONE NONE = EQUAL
- | iterCompare _ NONE (SOME _) = LESS
- | iterCompare _ (SOME _) NONE = GREATER
- | iterCompare cmp (SOME i1) (SOME i2) =
- keyIterCompare cmp (readIterator i1) (readIterator i2) i1 i2
-
- and keyIterCompare cmp k1 k2 i1 i2 =
- case cmp (k1,k2) of
- LESS => LESS
- | EQUAL => iterCompare cmp (advanceIterator i1) (advanceIterator i2)
- | GREATER => GREATER;
-in
- fun compare (s1,s2) =
- if pointerEqual (s1,s2) then EQUAL
- else
- case Int.compare (size s1, size s2) of
- LESS => LESS
- | EQUAL => iterCompare (comparison s1) (mkIterator s1) (mkIterator s2)
- | GREATER => GREATER;
-end;
-
-fun pick s =
- case findl (K true) s of
- SOME p => p
- | NONE => raise Error "RandomSet.pick: empty";
-
-fun random s =
- case size s of
- 0 => raise Error "RandomSet.random: empty"
- | n => nth s (randomInt n);
-
-fun deletePick s = let val x = pick s in (x, delete s x) end;
-
-fun deleteRandom s = let val x = random s in (x, delete s x) end;
-
-fun close f s = let val s' = f s in if equal s s' then s else close f s' end;
-
-fun toString s = "{" ^ (if null s then "" else Int.toString (size s)) ^ "}";
-
-end
-end;
-
-(**** Original file: Set.sml ****)
-
-structure Metis = struct open Metis
-(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;
-val foldl = List.foldl;
-val foldr = List.foldr;
-
-(* ========================================================================= *)
-(* FINITE SETS *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-structure Set = RandomSet;
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+structure Set :> Set =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite sets. *)
+(* ------------------------------------------------------------------------- *)
+
+type ('elt,'a) map = ('elt,'a) Map.map;
+
+datatype 'elt set = Set of ('elt,unit) map;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps. *)
+(* ------------------------------------------------------------------------- *)
+
+fun dest (Set m) = m;
+
+fun mapPartial f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => Map.mapPartial mf m
+ end;
+
+fun map f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => Map.map mf m
+ end;
+
+fun domain m = Set (Map.transform (fn _ => ()) m);
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun empty cmp = Set (Map.new cmp);
+
+fun singleton cmp elt = Set (Map.singleton cmp (elt,()));
+
+(* ------------------------------------------------------------------------- *)
+(* Set size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun null (Set m) = Map.null m;
+
+fun size (Set m) = Map.size m;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+fun peek (Set m) elt =
+ case Map.peekKey m elt of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE;
+
+fun member elt (Set m) = Map.inDomain elt m;
+
+fun pick (Set m) =
+ let
+ val (elt,_) = Map.pick m
+ in
+ elt
+ end;
+
+fun nth (Set m) n =
+ let
+ val (elt,_) = Map.nth m n
+ in
+ elt
+ end;
+
+fun random (Set m) =
+ let
+ val (elt,_) = Map.random m
+ in
+ elt
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun add (Set m) elt =
+ let
+ val m = Map.insert m (elt,())
+ in
+ Set m
+ end;
+
+local
+ fun uncurriedAdd (elt,set) = add set elt;
+in
+ fun addList set = List.foldl uncurriedAdd set;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Set m) elt =
+ let
+ val m = Map.delete m elt
+ in
+ Set m
+ end;
+
+fun remove (Set m) elt =
+ let
+ val m = Map.remove m elt
+ in
+ Set m
+ end;
+
+fun deletePick (Set m) =
+ let
+ val ((elt,()),m) = Map.deletePick m
+ in
+ (elt, Set m)
+ end;
+
+fun deleteNth (Set m) n =
+ let
+ val ((elt,()),m) = Map.deleteNth m n
+ in
+ (elt, Set m)
+ end;
+
+fun deleteRandom (Set m) =
+ let
+ val ((elt,()),m) = Map.deleteRandom m
+ in
+ (elt, Set m)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining. *)
+(* ------------------------------------------------------------------------- *)
+
+fun union (Set m1) (Set m2) = Set (Map.unionDomain m1 m2);
+
+fun unionList sets =
+ let
+ val ms = List.map dest sets
+ in
+ Set (Map.unionListDomain ms)
+ end;
+
+fun intersect (Set m1) (Set m2) = Set (Map.intersectDomain m1 m2);
+
+fun intersectList sets =
+ let
+ val ms = List.map dest sets
+ in
+ Set (Map.intersectListDomain ms)
+ end;
+
+fun difference (Set m1) (Set m2) =
+ Set (Map.differenceDomain m1 m2);
+
+fun symmetricDifference (Set m1) (Set m2) =
+ Set (Map.symmetricDifferenceDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun filter pred =
+ let
+ fun mpred (elt,()) = pred elt
+ in
+ fn Set m => Set (Map.filter mpred m)
+ end;
+
+fun partition pred =
+ let
+ fun mpred (elt,()) = pred elt
+ in
+ fn Set m =>
+ let
+ val (m1,m2) = Map.partition mpred m
+ in
+ (Set m1, Set m2)
+ end
+ end;
+
+fun app f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => Map.app mf m
+ end;
+
+fun foldl f =
+ let
+ fun mf (elt,(),acc) = f (elt,acc)
+ in
+ fn acc => fn Set m => Map.foldl mf acc m
+ end;
+
+fun foldr f =
+ let
+ fun mf (elt,(),acc) = f (elt,acc)
+ in
+ fn acc => fn Set m => Map.foldr mf acc m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m =>
+ case Map.findl mp m of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE
+ end;
+
+fun findr p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m =>
+ case Map.findr mp m of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE
+ end;
+
+fun firstl f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => Map.firstl mf m
+ end;
+
+fun firstr f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => Map.firstr mf m
+ end;
+
+fun exists p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => Map.exists mp m
+ end;
+
+fun all p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => Map.all mp m
+ end;
+
+fun count p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => Map.count mp m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compareValue ((),()) = EQUAL;
+
+fun equalValue () () = true;
+
+fun compare (Set m1, Set m2) = Map.compare compareValue (m1,m2);
+
+fun equal (Set m1) (Set m2) = Map.equal equalValue m1 m2;
+
+fun subset (Set m1) (Set m2) = Map.subsetDomain m1 m2;
+
+fun disjoint (Set m1) (Set m2) = Map.disjointDomain m1 m2;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+fun transform f =
+ let
+ fun inc (x,l) = f x :: l
+ in
+ foldr inc []
+ end;
+
+fun toList (Set m) = Map.keys m;
+
+fun fromList cmp elts = addList (empty cmp) elts;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString set =
+ "{" ^ (if null set then "" else Int.toString (size set)) ^ "}";
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over sets *)
+(* ------------------------------------------------------------------------- *)
+
+type 'elt iterator = ('elt,unit) Map.iterator;
+
+fun mkIterator (Set m) = Map.mkIterator m;
+
+fun mkRevIterator (Set m) = Map.mkRevIterator m;
+
+fun readIterator iter =
+ let
+ val (elt,()) = Map.readIterator iter
+ in
+ elt
+ end;
+
+fun advanceIterator iter = Map.advanceIterator iter;
+
+end
end;
(**** Original file: ElementSet.sig ****)
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature ElementSet =
sig
+(* ------------------------------------------------------------------------- *)
+(* A type of set elements. *)
+(* ------------------------------------------------------------------------- *)
+
type element
(* ------------------------------------------------------------------------- *)
-(* Finite sets *)
+(* A type of finite sets. *)
(* ------------------------------------------------------------------------- *)
type set
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
val empty : set
val singleton : element -> set
+(* ------------------------------------------------------------------------- *)
+(* Set size. *)
+(* ------------------------------------------------------------------------- *)
+
val null : set -> bool
val size : set -> int
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+val peek : set -> element -> element option
+
val member : element -> set -> bool
+val pick : set -> element (* an arbitrary element *)
+
+val nth : set -> int -> element (* in the range [0,size-1] *)
+
+val random : set -> element
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
val add : set -> element -> set
val addList : set -> element list -> set
-val delete : set -> element -> set (* raises Error *)
-
-(* Union and intersect prefer elements in the second set *)
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+val delete : set -> element -> set (* must be present *)
+
+val remove : set -> element -> set
+
+val deletePick : set -> element * set
+
+val deleteNth : set -> int -> element * set
+
+val deleteRandom : set -> element * set
+
+(* ------------------------------------------------------------------------- *)
+(* Joining. *)
+(* ------------------------------------------------------------------------- *)
val union : set -> set -> set
@@ -2883,22 +5817,24 @@
val symmetricDifference : set -> set -> set
-val disjoint : set -> set -> bool
-
-val subset : set -> set -> bool
-
-val equal : set -> set -> bool
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
val filter : (element -> bool) -> set -> set
val partition : (element -> bool) -> set -> set * set
-val count : (element -> bool) -> set -> int
+val app : (element -> unit) -> set -> unit
val foldl : (element * 's -> 's) -> 's -> set -> 's
val foldr : (element * 's -> 's) -> 's -> set -> 's
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
val findl : (element -> bool) -> set -> element option
val findr : (element -> bool) -> set -> element option
@@ -2911,27 +5847,45 @@
val all : (element -> bool) -> set -> bool
-val map : (element -> 'a) -> set -> (element * 'a) list
+val count : (element -> bool) -> set -> int
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : set * set -> order
+
+val equal : set -> set -> bool
+
+val subset : set -> set -> bool
+
+val disjoint : set -> set -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
val transform : (element -> 'a) -> set -> 'a list
-val app : (element -> unit) -> set -> unit
-
val toList : set -> element list
val fromList : element list -> set
-val pick : set -> element (* raises Empty *)
-
-val random : set -> element (* raises Empty *)
-
-val deletePick : set -> element * set (* raises Empty *)
-
-val deleteRandom : set -> element * set (* raises Empty *)
-
-val compare : set * set -> order
-
-val close : (set -> set) -> set -> set
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map
+
+val mapPartial : (element -> 'a option) -> set -> 'a map
+
+val map : (element -> 'a) -> set -> 'a map
+
+val domain : 'a map -> set
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
val toString : set -> string
@@ -2955,1128 +5909,369 @@
(* ========================================================================= *)
(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-functor ElementSet (Key : Ordered) :> ElementSet where type element = Key.t =
-struct
-
- open Metis;
-
-type element = Key.t;
-
-(* ------------------------------------------------------------------------- *)
-(* Finite sets *)
-(* ------------------------------------------------------------------------- *)
-
-type set = Key.t Set.set;
-
-val empty = Set.empty Key.compare;
-
-fun singleton key = Set.singleton Key.compare key;
-
-val null = Set.null;
-
-val size = Set.size;
-
-val member = Set.member;
-
-val add = Set.add;
-
-val addList = Set.addList;
-
-val delete = Set.delete;
-
-val op union = Set.union;
-
-val unionList = Set.unionList;
-
-val intersect = Set.intersect;
-
-val intersectList = Set.intersectList;
-
-val difference = Set.difference;
-
-val symmetricDifference = Set.symmetricDifference;
-
-val disjoint = Set.disjoint;
-
-val op subset = Set.subset;
-
-val equal = Set.equal;
-
-val filter = Set.filter;
-
-val partition = Set.partition;
-
-val count = Set.count;
-
-val foldl = Set.foldl;
-
-val foldr = Set.foldr;
-
-val findl = Set.findl;
-
-val findr = Set.findr;
-
-val firstl = Set.firstl;
-
-val firstr = Set.firstr;
-
-val exists = Set.exists;
-
-val all = Set.all;
-
-val map = Set.map;
-
-val transform = Set.transform;
-
-val app = Set.app;
-
-val toList = Set.toList;
-
-fun fromList l = Set.fromList Key.compare l;
-
-val pick = Set.pick;
-
-val random = Set.random;
-
-val deletePick = Set.deletePick;
-
-val deleteRandom = Set.deleteRandom;
-
-val compare = Set.compare;
-
-val close = Set.close;
-
-val toString = Set.toString;
+(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+functor ElementSet (KM : KeyMap) :> ElementSet
+where type element = KM.key and type 'a map = 'a KM.map =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* A type of set elements. *)
+(* ------------------------------------------------------------------------- *)
+
+type element = KM.key;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of finite sets. *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a map = 'a KM.map;
+
+datatype set = Set of unit map;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from maps. *)
+(* ------------------------------------------------------------------------- *)
+
+fun dest (Set m) = m;
+
+fun mapPartial f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.mapPartial mf m
+ end;
+
+fun map f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.map mf m
+ end;
+
+fun domain m = Set (KM.transform (fn _ => ()) m);
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val empty = Set (KM.new ());
+
+fun singleton elt = Set (KM.singleton (elt,()));
+
+(* ------------------------------------------------------------------------- *)
+(* Set size. *)
+(* ------------------------------------------------------------------------- *)
+
+fun null (Set m) = KM.null m;
+
+fun size (Set m) = KM.size m;
+
+(* ------------------------------------------------------------------------- *)
+(* Querying. *)
+(* ------------------------------------------------------------------------- *)
+
+fun peek (Set m) elt =
+ case KM.peekKey m elt of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE;
+
+fun member elt (Set m) = KM.inDomain elt m;
+
+fun pick (Set m) =
+ let
+ val (elt,_) = KM.pick m
+ in
+ elt
+ end;
+
+fun nth (Set m) n =
+ let
+ val (elt,_) = KM.nth m n
+ in
+ elt
+ end;
+
+fun random (Set m) =
+ let
+ val (elt,_) = KM.random m
+ in
+ elt
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Adding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun add (Set m) elt =
+ let
+ val m = KM.insert m (elt,())
+ in
+ Set m
+ end;
+
+local
+ fun uncurriedAdd (elt,set) = add set elt;
+in
+ fun addList set = List.foldl uncurriedAdd set;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Removing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun delete (Set m) elt =
+ let
+ val m = KM.delete m elt
+ in
+ Set m
+ end;
+
+fun remove (Set m) elt =
+ let
+ val m = KM.remove m elt
+ in
+ Set m
+ end;
+
+fun deletePick (Set m) =
+ let
+ val ((elt,()),m) = KM.deletePick m
+ in
+ (elt, Set m)
+ end;
+
+fun deleteNth (Set m) n =
+ let
+ val ((elt,()),m) = KM.deleteNth m n
+ in
+ (elt, Set m)
+ end;
+
+fun deleteRandom (Set m) =
+ let
+ val ((elt,()),m) = KM.deleteRandom m
+ in
+ (elt, Set m)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Joining. *)
+(* ------------------------------------------------------------------------- *)
+
+fun op union (Set m1) (Set m2) = Set (KM.unionDomain m1 m2);
+
+fun unionList sets =
+ let
+ val ms = List.map dest sets
+ in
+ Set (KM.unionListDomain ms)
+ end;
+
+fun intersect (Set m1) (Set m2) = Set (KM.intersectDomain m1 m2);
+
+fun intersectList sets =
+ let
+ val ms = List.map dest sets
+ in
+ Set (KM.intersectListDomain ms)
+ end;
+
+fun difference (Set m1) (Set m2) =
+ Set (KM.differenceDomain m1 m2);
+
+fun symmetricDifference (Set m1) (Set m2) =
+ Set (KM.symmetricDifferenceDomain m1 m2);
+
+(* ------------------------------------------------------------------------- *)
+(* Mapping and folding. *)
+(* ------------------------------------------------------------------------- *)
+
+fun filter pred =
+ let
+ fun mpred (elt,()) = pred elt
+ in
+ fn Set m => Set (KM.filter mpred m)
+ end;
+
+fun partition pred =
+ let
+ fun mpred (elt,()) = pred elt
+ in
+ fn Set m =>
+ let
+ val (m1,m2) = KM.partition mpred m
+ in
+ (Set m1, Set m2)
+ end
+ end;
+
+fun app f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.app mf m
+ end;
+
+fun foldl f =
+ let
+ fun mf (elt,(),acc) = f (elt,acc)
+ in
+ fn acc => fn Set m => KM.foldl mf acc m
+ end;
+
+fun foldr f =
+ let
+ fun mf (elt,(),acc) = f (elt,acc)
+ in
+ fn acc => fn Set m => KM.foldr mf acc m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Searching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun findl p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m =>
+ case KM.findl mp m of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE
+ end;
+
+fun findr p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m =>
+ case KM.findr mp m of
+ SOME (elt,()) => SOME elt
+ | NONE => NONE
+ end;
+
+fun firstl f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.firstl mf m
+ end;
+
+fun firstr f =
+ let
+ fun mf (elt,()) = f elt
+ in
+ fn Set m => KM.firstr mf m
+ end;
+
+fun exists p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => KM.exists mp m
+ end;
+
+fun all p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => KM.all mp m
+ end;
+
+fun count p =
+ let
+ fun mp (elt,()) = p elt
+ in
+ fn Set m => KM.count mp m
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compareValue ((),()) = EQUAL;
+
+fun equalValue () () = true;
+
+fun compare (Set m1, Set m2) = KM.compare compareValue (m1,m2);
+
+fun equal (Set m1) (Set m2) = KM.equal equalValue m1 m2;
+
+fun op subset (Set m1) (Set m2) = KM.subsetDomain m1 m2;
+
+fun disjoint (Set m1) (Set m2) = KM.disjointDomain m1 m2;
+
+(* ------------------------------------------------------------------------- *)
+(* Converting to and from lists. *)
+(* ------------------------------------------------------------------------- *)
+
+fun transform f =
+ let
+ fun inc (x,l) = f x :: l
+ in
+ foldr inc []
+ end;
+
+fun toList (Set m) = KM.keys m;
+
+fun fromList elts = addList empty elts;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun toString set =
+ "{" ^ (if null set then "" else Int.toString (size set)) ^ "}";
(* ------------------------------------------------------------------------- *)
(* Iterators over sets *)
(* ------------------------------------------------------------------------- *)
-type iterator = Key.t Set.iterator;
-
-val mkIterator = Set.mkIterator;
-
-val mkRevIterator = Set.mkRevIterator;
-
-val readIterator = Set.readIterator;
-
-val advanceIterator = Set.advanceIterator;
-
-end
-
- structure Metis = struct open Metis;
+type iterator = unit KM.iterator;
+
+fun mkIterator (Set m) = KM.mkIterator m;
+
+fun mkRevIterator (Set m) = KM.mkRevIterator m;
+
+fun readIterator iter =
+ let
+ val (elt,()) = KM.readIterator iter
+ in
+ elt
+ end;
+
+fun advanceIterator iter = KM.advanceIterator iter;
+
+end
structure IntSet =
-ElementSet (IntOrdered);
+ElementSet (IntMap);
+
+structure IntPairSet =
+ElementSet (IntPairMap);
structure StringSet =
-ElementSet (StringOrdered);
-
- end;
-
-(**** Original file: Map.sig ****)
-
-(* ========================================================================= *)
-(* FINITE MAPS *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-signature Map =
-sig
-
-(* ------------------------------------------------------------------------- *)
-(* Finite maps *)
-(* ------------------------------------------------------------------------- *)
-
-type ('key,'a) map
-
-val new : ('key * 'key -> order) -> ('key,'a) map
-
-val null : ('key,'a) map -> bool
-
-val size : ('key,'a) map -> int
-
-val singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map
-
-val inDomain : 'key -> ('key,'a) map -> bool
-
-val peek : ('key,'a) map -> 'key -> 'a option
-
-val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map
-
-val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map
-
-val get : ('key,'a) map -> 'key -> 'a (* raises Error *)
-
-(* Union and intersect prefer keys in the second map *)
-
-val union :
- ('a * 'a -> 'a option) -> ('key,'a) map -> ('key,'a) map -> ('key,'a) map
-
-val intersect :
- ('a * 'a -> 'a option) -> ('key,'a) map -> ('key,'a) map -> ('key,'a) map
-
-val delete : ('key,'a) map -> 'key -> ('key,'a) map (* raises Error *)
-
-val difference : ('key,'a) map -> ('key,'b) map -> ('key,'a) map
-
-val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool
-
-val equalDomain : ('key,'a) map -> ('key,'a) map -> bool
-
-val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map
-
-val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) 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 foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
-
-val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
-
-val findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
-
-val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
-
-val firstl : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
-
-val firstr : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
-
-val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool
-
-val all : ('key * 'a -> bool) -> ('key,'a) map -> bool
-
-val domain : ('key,'a) map -> 'key list
-
-val toList : ('key,'a) map -> ('key * 'a) list
-
-val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map
-
-val random : ('key,'a) map -> 'key * 'a (* raises Empty *)
-
-val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order
-
-val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
-
-val 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: RandomMap.sml ****)
-
-structure Metis = struct open Metis
-(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;
-val foldl = List.foldl;
-val foldr = List.foldr;
-
-(* ========================================================================= *)
-(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-structure RandomMap :> Map =
-struct
-
-exception Bug = Useful.Bug;
-
-exception Error = Useful.Error;
-
-val pointerEqual = Portable.pointerEqual;
-
-val K = Useful.K;
-
-val snd = Useful.snd;
-
-val randomInt = Portable.randomInt;
-
-val randomWord = Portable.randomWord;
-
-(* ------------------------------------------------------------------------- *)
-(* Random search trees. *)
-(* ------------------------------------------------------------------------- *)
-
-type priority = Word.word;
-
-datatype ('a,'b) tree =
- E
- | T of
- {size : int,
- priority : priority,
- left : ('a,'b) tree,
- key : 'a,
- value : 'b,
- right : ('a,'b) tree};
-
-type ('a,'b) node =
- {size : int,
- priority : priority,
- left : ('a,'b) tree,
- key : 'a,
- value : 'b,
- right : ('a,'b) tree};
-
-datatype ('a,'b) map = Map of ('a * 'a -> order) * ('a,'b) tree;
-
-(* ------------------------------------------------------------------------- *)
-(* Random priorities. *)
-(* ------------------------------------------------------------------------- *)
-
-local
- val randomPriority = randomWord;
-
- val priorityOrder = Word.compare;
-in
- fun treeSingleton (key,value) =
- T {size = 1, priority = randomPriority (),
- left = E, key = key, value = value, right = E};
-
- fun nodePriorityOrder cmp (x1 : ('a,'b) node, x2 : ('a,'b) node) =
- let
- val {priority = p1, key = k1, ...} = x1
- and {priority = p2, key = k2, ...} = x2
- in
- case priorityOrder (p1,p2) of
- LESS => LESS
- | EQUAL => cmp (k1,k2)
- | GREATER => GREATER
- end;
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Debugging functions. *)
-(* ------------------------------------------------------------------------- *)
-
-local
- fun checkSizes E = 0
- | checkSizes (T {size,left,right,...}) =
- let
- val l = checkSizes left
- and r = checkSizes right
- val () = if l + 1 + r = size then () else raise Error "wrong size"
- in
- size
- end;
-
- fun checkSorted _ x E = x
- | checkSorted cmp x (T {left,key,right,...}) =
- let
- val x = checkSorted cmp x left
- val () =
- case x of
- NONE => ()
- | SOME k =>
- case cmp (k,key) of
- LESS => ()
- | EQUAL => raise Error "duplicate keys"
- | GREATER => raise Error "unsorted"
- in
- checkSorted cmp (SOME key) right
- end;
-
- fun checkPriorities _ E = NONE
- | checkPriorities cmp (T (x as {left,right,...})) =
- let
- val () =
- case checkPriorities cmp left of
- NONE => ()
- | SOME l =>
- case nodePriorityOrder cmp (l,x) of
- LESS => ()
- | EQUAL => raise Error "left child has equal key"
- | GREATER => raise Error "left child has greater priority"
- val () =
- case checkPriorities cmp right of
- NONE => ()
- | SOME r =>
- case nodePriorityOrder cmp (r,x) of
- LESS => ()
- | EQUAL => raise Error "right child has equal key"
- | GREATER => raise Error "right child has greater priority"
- in
- SOME x
- end;
-in
- fun checkWellformed s (m as Map (cmp,tree)) =
- (let
- val _ = checkSizes tree
- val _ = checkSorted cmp NONE tree
- val _ = checkPriorities cmp tree
- in
- m
- end
- handle Error err => raise Bug err)
- handle Bug bug => raise Bug (s ^ "\nRandomMap.checkWellformed: " ^ bug);
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Basic operations. *)
-(* ------------------------------------------------------------------------- *)
-
-fun comparison (Map (cmp,_)) = cmp;
-
-fun new cmp = Map (cmp,E);
-
-fun treeSize E = 0
- | treeSize (T {size = s, ...}) = s;
-
-fun size (Map (_,tree)) = treeSize tree;
-
-fun mkT p l k v r =
- T {size = treeSize l + 1 + treeSize r, priority = p,
- left = l, key = k, value = v, right = r};
-
-fun singleton cmp key_value = Map (cmp, treeSingleton key_value);
-
-local
- fun treePeek cmp E pkey = NONE
- | treePeek cmp (T {left,key,value,right,...}) pkey =
- case cmp (pkey,key) of
- LESS => treePeek cmp left pkey
- | EQUAL => SOME value
- | GREATER => treePeek cmp right pkey
-in
- fun peek (Map (cmp,tree)) key = treePeek cmp tree key;
-end;
-
-(* treeAppend assumes that every element of the first tree is less than *)
-(* every element of the second tree. *)
-
-fun treeAppend _ t1 E = t1
- | treeAppend _ E t2 = t2
- | treeAppend cmp (t1 as T x1) (t2 as T x2) =
- case nodePriorityOrder cmp (x1,x2) of
- LESS =>
- let
- val {priority = p2,
- left = l2, key = k2, value = v2, right = r2, ...} = x2
- in
- mkT p2 (treeAppend cmp t1 l2) k2 v2 r2
- end
- | EQUAL => raise Bug "RandomSet.treeAppend: equal keys"
- | GREATER =>
- let
- val {priority = p1,
- left = l1, key = k1, value = v1, right = r1, ...} = x1
- in
- mkT p1 l1 k1 v1 (treeAppend cmp r1 t2)
- end;
-
-(* nodePartition splits the node into three parts: the keys comparing less *)
-(* than the supplied key, an optional equal key, and the keys comparing *)
-(* greater. *)
-
-local
- fun mkLeft [] t = t
- | mkLeft (({priority,left,key,value,...} : ('a,'b) node) :: xs) t =
- mkLeft xs (mkT priority left key value t);
-
- fun mkRight [] t = t
- | mkRight (({priority,key,value,right,...} : ('a,'b) node) :: xs) t =
- mkRight xs (mkT priority t key value right);
-
- fun treePart _ _ lefts rights E = (mkLeft lefts E, NONE, mkRight rights E)
- | treePart cmp pkey lefts rights (T x) = nodePart cmp pkey lefts rights x
- and nodePart cmp pkey lefts rights (x as {left,key,value,right,...}) =
- case cmp (pkey,key) of
- LESS => treePart cmp pkey lefts (x :: rights) left
- | EQUAL => (mkLeft lefts left, SOME (key,value), mkRight rights right)
- | GREATER => treePart cmp pkey (x :: lefts) rights right;
-in
- fun nodePartition cmp x pkey = nodePart cmp pkey [] [] x;
-end;
-
-(* union first calls treeCombineRemove, to combine the values *)
-(* for equal keys into the first map and remove them from the second map. *)
-(* Note that the combined key is always the one from the second map. *)
-
-local
- fun treeCombineRemove _ _ t1 E = (t1,E)
- | treeCombineRemove _ _ E t2 = (E,t2)
- | treeCombineRemove cmp f (t1 as T x1) (t2 as T x2) =
- let
- val {priority = p1,
- left = l1, key = k1, value = v1, right = r1, ...} = x1
- val (l2,k2_v2,r2) = nodePartition cmp x2 k1
- val (l1,l2) = treeCombineRemove cmp f l1 l2
- and (r1,r2) = treeCombineRemove cmp f r1 r2
- in
- case k2_v2 of
- NONE =>
- if treeSize l2 + treeSize r2 = #size x2 then (t1,t2)
- else (mkT p1 l1 k1 v1 r1, treeAppend cmp l2 r2)
- | SOME (k2,v2) =>
- case f (v1,v2) of
- NONE => (treeAppend cmp l1 r1, treeAppend cmp l2 r2)
- | SOME v => (mkT p1 l1 k2 v r1, treeAppend cmp l2 r2)
- end;
-
- fun treeUnionDisjoint _ t1 E = t1
- | treeUnionDisjoint _ E t2 = t2
- | treeUnionDisjoint cmp (T x1) (T x2) =
- case nodePriorityOrder cmp (x1,x2) of
- LESS => nodeUnionDisjoint cmp x2 x1
- | EQUAL => raise Bug "RandomSet.unionDisjoint: equal keys"
- | GREATER => nodeUnionDisjoint cmp x1 x2
- and nodeUnionDisjoint cmp x1 x2 =
- let
- val {priority = p1,
- left = l1, key = k1, value = v1, right = r1, ...} = x1
- val (l2,_,r2) = nodePartition cmp x2 k1
- val l = treeUnionDisjoint cmp l1 l2
- and r = treeUnionDisjoint cmp r1 r2
- in
- mkT p1 l k1 v1 r
- end;
-in
- fun union f (m1 as Map (cmp,t1)) (Map (_,t2)) =
- if pointerEqual (t1,t2) then m1
- else
- let
- val (t1,t2) = treeCombineRemove cmp f t1 t2
- in
- Map (cmp, treeUnionDisjoint cmp t1 t2)
- end;
-end;
-
-(*DEBUG
-val union = fn f => fn t1 => fn t2 =>
- checkWellformed "RandomMap.union: result"
- (union f (checkWellformed "RandomMap.union: input 1" t1)
- (checkWellformed "RandomMap.union: input 2" t2));
-*)
-
-(* intersect is a simple case of the union algorithm. *)
-
-local
- fun treeIntersect _ _ _ E = E
- | treeIntersect _ _ E _ = E
- | treeIntersect cmp f (t1 as T x1) (t2 as T x2) =
- let
- val {priority = p1,
- left = l1, key = k1, value = v1, right = r1, ...} = x1
- val (l2,k2_v2,r2) = nodePartition cmp x2 k1
- val l = treeIntersect cmp f l1 l2
- and r = treeIntersect cmp f r1 r2
- in
- case k2_v2 of
- NONE => treeAppend cmp l r
- | SOME (k2,v2) =>
- case f (v1,v2) of
- NONE => treeAppend cmp l r
- | SOME v => mkT p1 l k2 v r
- end;
-in
- fun intersect f (m1 as Map (cmp,t1)) (Map (_,t2)) =
- if pointerEqual (t1,t2) then m1
- else Map (cmp, treeIntersect cmp f t1 t2);
-end;
-
-(*DEBUG
-val intersect = fn f => fn t1 => fn t2 =>
- checkWellformed "RandomMap.intersect: result"
- (intersect f (checkWellformed "RandomMap.intersect: input 1" t1)
- (checkWellformed "RandomMap.intersect: input 2" t2));
-*)
-
-(* delete raises an exception if the supplied key is not found, which *)
-(* makes it simpler to maximize sharing. *)
-
-local
- fun treeDelete _ E _ = raise Error "RandomMap.delete: element not found"
- | treeDelete cmp (T {priority,left,key,value,right,...}) dkey =
- case cmp (dkey,key) of
- LESS => mkT priority (treeDelete cmp left dkey) key value right
- | EQUAL => treeAppend cmp left right
- | GREATER => mkT priority left key value (treeDelete cmp right dkey);
-in
- fun delete (Map (cmp,tree)) key = Map (cmp, treeDelete cmp tree key);
-end;
-
-(*DEBUG
-val delete = fn t => fn x =>
- checkWellformed "RandomMap.delete: result"
- (delete (checkWellformed "RandomMap.delete: input" t) x);
-*)
-
-(* Set difference on domains *)
-
-local
- fun treeDifference _ t1 E = t1
- | treeDifference _ E _ = E
- | treeDifference cmp (t1 as T x1) (T x2) =
- let
- val {size = s1, priority = p1,
- left = l1, key = k1, value = v1, right = r1} = x1
- val (l2,k2_v2,r2) = nodePartition cmp x2 k1
- val l = treeDifference cmp l1 l2
- and r = treeDifference cmp r1 r2
- in
- if Option.isSome k2_v2 then treeAppend cmp l r
- else if treeSize l + treeSize r + 1 = s1 then t1
- else mkT p1 l k1 v1 r
- end;
-in
- fun difference (Map (cmp,tree1)) (Map (_,tree2)) =
- Map (cmp, treeDifference cmp tree1 tree2);
-end;
-
-(*DEBUG
-val difference = fn t1 => fn t2 =>
- checkWellformed "RandomMap.difference: result"
- (difference (checkWellformed "RandomMap.difference: input 1" t1)
- (checkWellformed "RandomMap.difference: input 2" t2));
-*)
-
-(* subsetDomain is mainly used when using maps as sets. *)
-
-local
- fun treeSubsetDomain _ E _ = true
- | treeSubsetDomain _ _ E = false
- | treeSubsetDomain cmp (t1 as T x1) (T x2) =
- let
- val {size = s1, left = l1, key = k1, right = r1, ...} = x1
- and {size = s2, ...} = x2
- in
- s1 <= s2 andalso
- let
- val (l2,k2_v2,r2) = nodePartition cmp x2 k1
- in
- Option.isSome k2_v2 andalso
- treeSubsetDomain cmp l1 l2 andalso
- treeSubsetDomain cmp r1 r2
- end
- end;
-in
- fun subsetDomain (Map (cmp,tree1)) (Map (_,tree2)) =
- pointerEqual (tree1,tree2) orelse
- treeSubsetDomain cmp tree1 tree2;
-end;
-
-(* Map equality *)
-
-local
- fun treeEqual _ _ E E = true
- | treeEqual _ _ E _ = false
- | treeEqual _ _ _ E = false
- | treeEqual cmp veq (t1 as T x1) (T x2) =
- let
- val {size = s1, left = l1, key = k1, value = v1, right = r1, ...} = x1
- and {size = s2, ...} = x2
- in
- s1 = s2 andalso
- let
- val (l2,k2_v2,r2) = nodePartition cmp x2 k1
- in
- (case k2_v2 of NONE => false | SOME (_,v2) => veq v1 v2) andalso
- treeEqual cmp veq l1 l2 andalso
- treeEqual cmp veq r1 r2
- end
- end;
-in
- fun equal veq (Map (cmp,tree1)) (Map (_,tree2)) =
- pointerEqual (tree1,tree2) orelse
- treeEqual cmp veq tree1 tree2;
-end;
-
-(* mapPartial is the basic function for preserving the tree structure. *)
-(* It applies the argument function to the elements *in order*. *)
-
-local
- fun treeMapPartial cmp _ E = E
- | treeMapPartial cmp f (T {priority,left,key,value,right,...}) =
- let
- val left = treeMapPartial cmp f left
- and value' = f (key,value)
- and right = treeMapPartial cmp f right
- in
- case value' of
- NONE => treeAppend cmp left right
- | SOME value => mkT priority left key value right
- end;
-in
- fun mapPartial f (Map (cmp,tree)) = Map (cmp, treeMapPartial cmp f tree);
-end;
-
-(* map is a primitive function for efficiency reasons. *)
-(* It also applies the argument function to the elements *in order*. *)
-
-local
- fun treeMap _ E = E
- | treeMap f (T {size,priority,left,key,value,right}) =
- let
- val left = treeMap f left
- and value = f (key,value)
- and right = treeMap f right
- in
- T {size = size, priority = priority, left = left,
- key = key, value = value, right = right}
- end;
-in
- fun map f (Map (cmp,tree)) = Map (cmp, treeMap f tree);
-end;
-
-(* nth picks the nth smallest key/value (counting from 0). *)
-
-local
- fun treeNth E _ = raise Subscript
- | treeNth (T {left,key,value,right,...}) n =
- let
- val k = treeSize left
- in
- if n = k then (key,value)
- else if n < k then treeNth left n
- else treeNth right (n - (k + 1))
- end;
-in
- fun nth (Map (_,tree)) n = treeNth tree n;
-end;
-
-(* ------------------------------------------------------------------------- *)
-(* Iterators. *)
-(* ------------------------------------------------------------------------- *)
-
-fun leftSpine E acc = acc
- | leftSpine (t as T {left,...}) acc = leftSpine left (t :: acc);
-
-fun rightSpine E acc = acc
- | rightSpine (t as T {right,...}) acc = rightSpine right (t :: acc);
-
-datatype ('key,'a) iterator =
- LR of ('key * 'a) * ('key,'a) tree * ('key,'a) tree list
- | RL of ('key * 'a) * ('key,'a) tree * ('key,'a) tree list;
-
-fun mkLR [] = NONE
- | mkLR (T {key,value,right,...} :: l) = SOME (LR ((key,value),right,l))
- | mkLR (E :: _) = raise Bug "RandomMap.mkLR";
-
-fun mkRL [] = NONE
- | mkRL (T {key,value,left,...} :: l) = SOME (RL ((key,value),left,l))
- | mkRL (E :: _) = raise Bug "RandomMap.mkRL";
-
-fun mkIterator (Map (_,tree)) = mkLR (leftSpine tree []);
-
-fun mkRevIterator (Map (_,tree)) = mkRL (rightSpine tree []);
-
-fun readIterator (LR (key_value,_,_)) = key_value
- | readIterator (RL (key_value,_,_)) = key_value;
-
-fun advanceIterator (LR (_,next,l)) = mkLR (leftSpine next l)
- | advanceIterator (RL (_,next,l)) = mkRL (rightSpine next l);
-
-(* ------------------------------------------------------------------------- *)
-(* Derived operations. *)
-(* ------------------------------------------------------------------------- *)
-
-fun null m = size m = 0;
-
-fun get m key =
- case peek m key of
- NONE => raise Error "RandomMap.get: element not found"
- | SOME value => value;
-
-fun inDomain key m = Option.isSome (peek m key);
-
-fun insert m key_value =
- union (SOME o snd) m (singleton (comparison m) key_value);
-
-(*DEBUG
-val insert = fn m => fn x =>
- checkWellformed "RandomMap.insert: result"
- (insert (checkWellformed "RandomMap.insert: input" m) x);
-*)
-
-local
- fun fold _ NONE acc = acc
- | fold f (SOME iter) acc =
- let
- val (key,value) = readIterator iter
- in
- fold f (advanceIterator iter) (f (key,value,acc))
- end;
-in
- fun foldl f b m = fold f (mkIterator m) b;
-
- fun foldr f b m = fold f (mkRevIterator m) b;
-end;
-
-local
- fun find _ NONE = NONE
- | find pred (SOME iter) =
- let
- val key_value = readIterator iter
- in
- if pred key_value then SOME key_value
- else find pred (advanceIterator iter)
- end;
-in
- fun findl p m = find p (mkIterator m);
-
- fun findr p m = find p (mkRevIterator m);
-end;
-
-local
- fun first _ NONE = NONE
- | first f (SOME iter) =
- let
- val key_value = readIterator iter
- in
- case f key_value of
- NONE => first f (advanceIterator iter)
- | s => s
- end;
-in
- fun firstl f m = first f (mkIterator m);
-
- fun firstr f m = first f (mkRevIterator m);
-end;
-
-fun fromList cmp l = List.foldl (fn (k_v,m) => insert m k_v) (new cmp) l;
-
-fun insertList m l = union (SOME o snd) m (fromList (comparison m) l);
-
-fun filter p =
- let
- fun f (key_value as (_,value)) =
- if p key_value then SOME value else NONE
- in
- mapPartial f
- end;
-
-fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
-
-fun transform f = map (fn (_,value) => f value);
-
-fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
-
-fun domain m = foldr (fn (key,_,l) => key :: l) [] m;
-
-fun exists p m = Option.isSome (findl p m);
-
-fun all p m = not (exists (not o p) m);
-
-fun random m =
- case size m of
- 0 => raise Error "RandomMap.random: empty"
- | n => nth m (randomInt n);
-
-local
- fun iterCompare _ _ NONE NONE = EQUAL
- | iterCompare _ _ NONE (SOME _) = LESS
- | iterCompare _ _ (SOME _) NONE = GREATER
- | iterCompare kcmp vcmp (SOME i1) (SOME i2) =
- keyIterCompare kcmp vcmp (readIterator i1) (readIterator i2) i1 i2
-
- and keyIterCompare kcmp vcmp (k1,v1) (k2,v2) i1 i2 =
- case kcmp (k1,k2) of
- LESS => LESS
- | EQUAL =>
- (case vcmp (v1,v2) of
- LESS => LESS
- | EQUAL =>
- iterCompare kcmp vcmp (advanceIterator i1) (advanceIterator i2)
- | GREATER => GREATER)
- | GREATER => GREATER;
-in
- fun compare vcmp (m1,m2) =
- if pointerEqual (m1,m2) then EQUAL
- else
- case Int.compare (size m1, size m2) of
- LESS => LESS
- | EQUAL =>
- iterCompare (comparison m1) vcmp (mkIterator m1) (mkIterator m2)
- | GREATER => GREATER;
-end;
-
-fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
-
-fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
-
-end
-end;
-
-(**** Original file: Map.sml ****)
-
-structure Metis = struct open Metis
-(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;
-val foldl = List.foldl;
-val foldr = List.foldr;
-
-(* ========================================================================= *)
-(* FINITE MAPS *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-structure Map = RandomMap;
-end;
-
-(**** Original file: KeyMap.sig ****)
-
-(* ========================================================================= *)
-(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-signature KeyMap =
-sig
-
-type key
-
-(* ------------------------------------------------------------------------- *)
-(* Finite maps *)
-(* ------------------------------------------------------------------------- *)
-
-type 'a map
-
-val new : unit -> 'a map
-
-val null : 'a map -> bool
-
-val size : 'a map -> int
-
-val singleton : key * 'a -> 'a map
-
-val inDomain : key -> 'a map -> bool
-
-val peek : 'a map -> key -> 'a option
-
-val insert : 'a map -> key * 'a -> 'a map
-
-val insertList : 'a map -> (key * 'a) list -> 'a map
-
-val get : 'a map -> key -> 'a (* raises Error *)
-
-(* Union and intersect prefer keys in the second map *)
-
-val union : ('a * 'a -> 'a option) -> 'a map -> 'a map -> 'a map
-
-val intersect : ('a * 'a -> 'a option) -> 'a map -> 'a map -> 'a map
-
-val delete : 'a map -> key -> 'a map (* raises Error *)
-
-val difference : 'a map -> 'a map -> 'a map
-
-val subsetDomain : 'a map -> 'a map -> bool
-
-val equalDomain : 'a map -> 'a map -> bool
-
-val mapPartial : (key * 'a -> 'b option) -> 'a map -> 'b map
-
-val filter : (key * 'a -> bool) -> 'a map -> 'a 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 foldl : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
-
-val foldr : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
-
-val findl : (key * 'a -> bool) -> 'a map -> (key * 'a) option
-
-val findr : (key * 'a -> bool) -> 'a map -> (key * 'a) option
-
-val firstl : (key * 'a -> 'b option) -> 'a map -> 'b option
-
-val firstr : (key * 'a -> 'b option) -> 'a map -> 'b option
-
-val exists : (key * 'a -> bool) -> 'a map -> bool
-
-val all : (key * 'a -> bool) -> 'a map -> bool
-
-val domain : 'a map -> key list
-
-val toList : 'a map -> (key * 'a) list
-
-val fromList : (key * 'a) list -> 'a map
-
-val compare : ('a * 'a -> order) -> 'a map * 'a map -> order
-
-val equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
-
-val random : 'a map -> key * 'a (* raises Empty *)
-
-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: KeyMap.sml ****)
-
-(* ========================================================================= *)
-(* FINITE MAPS WITH A FIXED KEY TYPE *)
-(* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
-struct
-
- open Metis;
-
-type key = Key.t;
-
-(* ------------------------------------------------------------------------- *)
-(* Finite maps *)
-(* ------------------------------------------------------------------------- *)
-
-type 'a map = (Key.t,'a) Map.map;
-
-fun new () = Map.new Key.compare;
-
-val null = Map.null;
-
-val size = Map.size;
-
-fun singleton key_value = Map.singleton Key.compare key_value;
-
-val inDomain = Map.inDomain;
-
-val peek = Map.peek;
-
-val insert = Map.insert;
-
-val insertList = Map.insertList;
-
-val get = Map.get;
-
-(* Both op union and intersect prefer keys in the second map *)
-
-val op union = Map.union;
-
-val intersect = Map.intersect;
-
-val delete = Map.delete;
-
-val difference = Map.difference;
-
-val subsetDomain = Map.subsetDomain;
-
-val equalDomain = Map.equalDomain;
-
-val mapPartial = Map.mapPartial;
-
-val filter = Map.filter;
-
-val map = Map.map;
-
-val app = Map.app;
-
-val transform = Map.transform;
-
-val foldl = Map.foldl;
-
-val foldr = Map.foldr;
-
-val findl = Map.findl;
-
-val findr = Map.findr;
-
-val firstl = Map.firstl;
-
-val firstr = Map.firstr;
-
-val exists = Map.exists;
-
-val all = Map.all;
-
-val domain = Map.domain;
-
-val toList = Map.toList;
-
-fun fromList l = Map.fromList Key.compare l;
-
-val compare = Map.compare;
-
-val equal = Map.equal;
-
-val random = Map.random;
-
-val toString = Map.toString;
-
-(* ------------------------------------------------------------------------- *)
-(* Iterators over maps *)
-(* ------------------------------------------------------------------------- *)
-
-type 'a iterator = (Key.t,'a) Map.iterator;
-
-val mkIterator = Map.mkIterator;
-
-val mkRevIterator = Map.mkRevIterator;
-
-val readIterator = Map.readIterator;
-
-val advanceIterator = Map.advanceIterator;
-
-end
-
- structure Metis = struct open Metis
-
-structure IntMap =
-KeyMap (IntOrdered);
-
-structure StringMap =
-KeyMap (StringOrdered);
-
- end;
+ElementSet (StringMap);
(**** Original file: Sharing.sig ****)
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Sharing =
sig
(* ------------------------------------------------------------------------- *)
-(* Pointer equality. *)
-(* ------------------------------------------------------------------------- *)
-
-val pointerEqual : 'a * 'a -> bool
+(* Option operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val mapOption : ('a -> 'a) -> 'a option -> 'a option
+
+val mapsOption : ('a -> 's -> 'a * 's) -> 'a option -> 's -> 'a option * 's
(* ------------------------------------------------------------------------- *)
(* List operations. *)
@@ -4084,6 +6279,12 @@
val map : ('a -> 'a) -> 'a list -> 'a list
+val revMap : ('a -> 'a) -> 'a list -> 'a list
+
+val maps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's
+
+val revMaps : ('a -> 's -> 'a * 's) -> 'a list -> 's -> 'a list * 's
+
val updateNth : int * 'a -> 'a list -> 'a list
val setify : ''a list -> ''a list
@@ -4106,7 +6307,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
+nonfix ++ -- RL;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4115,7 +6316,7 @@
(* ========================================================================= *)
(* PRESERVING SHARING OF ML VALUES *)
-(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Sharing :> Sharing =
@@ -4123,13 +6324,31 @@
infix ==
-(* ------------------------------------------------------------------------- *)
-(* Pointer equality. *)
-(* ------------------------------------------------------------------------- *)
-
-val pointerEqual = Portable.pointerEqual;
-
-val op== = pointerEqual;
+val op== = Portable.pointerEqual;
+
+(* ------------------------------------------------------------------------- *)
+(* Option operations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapOption f xo =
+ case xo of
+ SOME x =>
+ let
+ val y = f x
+ in
+ if x == y then xo else SOME y
+ end
+ | NONE => xo;
+
+fun mapsOption f xo acc =
+ case xo of
+ SOME x =>
+ let
+ val (y,acc) = f x acc
+ in
+ if x == y then (xo,acc) else (SOME y, acc)
+ end
+ | NONE => (xo,acc);
(* ------------------------------------------------------------------------- *)
(* List operations. *)
@@ -4137,17 +6356,78 @@
fun map f =
let
- fun m _ a_b [] = List.revAppend a_b
- | m ys a_b (x :: xs) =
- let
- val y = f x
- val ys = y :: ys
- in
- m ys (if x == y then a_b else (ys,xs)) xs
- end
- in
- fn l => m [] ([],l) l
- end;
+ fun m ys ys_xs xs =
+ case xs of
+ [] => List.revAppend ys_xs
+ | x :: xs =>
+ let
+ val y = f x
+ val ys = y :: ys
+ val ys_xs = if x == y then ys_xs else (ys,xs)
+ in
+ m ys ys_xs xs
+ end
+ in
+ fn xs => m [] ([],xs) xs
+ end;
+
+fun maps f =
+ let
+ fun m acc ys ys_xs xs =
+ case xs of
+ [] => (List.revAppend ys_xs, acc)
+ | x :: xs =>
+ let
+ val (y,acc) = f x acc
+ val ys = y :: ys
+ val ys_xs = if x == y then ys_xs else (ys,xs)
+ in
+ m acc ys ys_xs xs
+ end
+ in
+ fn xs => fn acc => m acc [] ([],xs) xs
+ end;
+
+local
+ fun revTails acc xs =
+ case xs of
+ [] => acc
+ | x :: xs' => revTails ((x,xs) :: acc) xs';
+in
+ fun revMap f =
+ let
+ fun m ys same xxss =
+ case xxss of
+ [] => ys
+ | (x,xs) :: xxss =>
+ let
+ val y = f x
+ val same = same andalso x == y
+ val ys = if same then xs else y :: ys
+ in
+ m ys same xxss
+ end
+ in
+ fn xs => m [] true (revTails [] xs)
+ end;
+
+ fun revMaps f =
+ let
+ fun m acc ys same xxss =
+ case xxss of
+ [] => (ys,acc)
+ | (x,xs) :: xxss =>
+ let
+ val (y,acc) = f x acc
+ val same = same andalso x == y
+ val ys = if same then xs else y :: ys
+ in
+ m acc ys same xxss
+ end
+ in
+ fn xs => fn acc => m acc [] true (revTails [] xs)
+ end;
+end;
fun updateNth (n,x) l =
let
@@ -4194,329 +6474,11 @@
end
end;
-(**** Original file: Stream.sig ****)
-
-(* ========================================================================= *)
-(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-signature Stream =
-sig
-
-(* ------------------------------------------------------------------------- *)
-(* The stream type *)
-(* ------------------------------------------------------------------------- *)
-
-datatype 'a stream = NIL | CONS of 'a * (unit -> 'a stream)
-
-(* If you're wondering how to create an infinite stream: *)
-(* val stream4 = let fun s4 () = Metis.Stream.CONS (4,s4) in s4 () end; *)
-
-(* ------------------------------------------------------------------------- *)
-(* Stream constructors *)
-(* ------------------------------------------------------------------------- *)
-
-val repeat : 'a -> 'a stream
-
-val count : int -> int stream
-
-val funpows : ('a -> 'a) -> 'a -> 'a stream
-
-(* ------------------------------------------------------------------------- *)
-(* Stream versions of standard list operations: these should all terminate *)
-(* ------------------------------------------------------------------------- *)
-
-val cons : 'a -> (unit -> 'a stream) -> 'a stream
-
-val null : 'a stream -> bool
-
-val hd : 'a stream -> 'a (* raises Empty *)
-
-val tl : 'a stream -> 'a stream (* raises Empty *)
-
-val hdTl : 'a stream -> 'a * 'a stream (* raises Empty *)
-
-val singleton : 'a -> 'a stream
-
-val append : 'a stream -> (unit -> 'a stream) -> 'a stream
-
-val map : ('a -> 'b) -> 'a stream -> 'b stream
-
-val maps : ('a -> 's -> 'b * 's) -> 's -> 'a stream -> 'b stream
-
-val zipwith : ('a -> 'b -> 'c) -> 'a stream -> 'b stream -> 'c stream
-
-val zip : 'a stream -> 'b stream -> ('a * 'b) stream
-
-val take : int -> 'a stream -> 'a stream (* raises Subscript *)
-
-val drop : int -> 'a stream -> 'a stream (* raises Subscript *)
-
-(* ------------------------------------------------------------------------- *)
-(* Stream versions of standard list operations: these might not terminate *)
-(* ------------------------------------------------------------------------- *)
-
-val length : 'a stream -> int
-
-val exists : ('a -> bool) -> 'a stream -> bool
-
-val all : ('a -> bool) -> 'a stream -> bool
-
-val filter : ('a -> bool) -> 'a stream -> 'a stream
-
-val foldl : ('a * 's -> 's) -> 's -> 'a stream -> 's
-
-val concat : 'a stream stream -> 'a stream
-
-val mapPartial : ('a -> 'b option) -> 'a stream -> 'b stream
-
-val mapsPartial : ('a -> 's -> 'b option * 's) -> 's -> 'a stream -> 'b stream
-
-(* ------------------------------------------------------------------------- *)
-(* Stream operations *)
-(* ------------------------------------------------------------------------- *)
-
-val memoize : 'a stream -> 'a stream
-
-val toList : 'a stream -> 'a list
-
-val fromList : 'a list -> 'a stream
-
-val toString : char stream -> string
-
-val fromString : string -> char stream
-
-val toTextFile : {filename : string} -> string stream -> unit
-
-val fromTextFile : {filename : string} -> string stream (* line by line *)
-
-end
-
-(**** Original file: Stream.sml ****)
-
-structure Metis = struct open Metis
-(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
-val explode = String.explode;
-val implode = String.implode;
-val print = TextIO.print;
-val foldl = List.foldl;
-val foldr = List.foldr;
-
-(* ========================================================================= *)
-(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-structure Stream :> Stream =
-struct
-
-val K = Useful.K;
-
-val pair = Useful.pair;
-
-val funpow = Useful.funpow;
-
-(* ------------------------------------------------------------------------- *)
-(* The datatype declaration encapsulates all the primitive operations *)
-(* ------------------------------------------------------------------------- *)
-
-datatype 'a stream =
- NIL
- | CONS of 'a * (unit -> 'a stream);
-
-(* ------------------------------------------------------------------------- *)
-(* Stream constructors *)
-(* ------------------------------------------------------------------------- *)
-
-fun repeat x = let fun rep () = CONS (x,rep) in rep () end;
-
-fun count n = CONS (n, fn () => count (n + 1));
-
-fun funpows f x = CONS (x, fn () => funpows f (f x));
-
-(* ------------------------------------------------------------------------- *)
-(* Stream versions of standard list operations: these should all terminate *)
-(* ------------------------------------------------------------------------- *)
-
-fun cons h t = CONS (h,t);
-
-fun null NIL = true | null (CONS _) = false;
-
-fun hd NIL = raise Empty
- | hd (CONS (h,_)) = h;
-
-fun tl NIL = raise Empty
- | tl (CONS (_,t)) = t ();
-
-fun hdTl s = (hd s, tl s);
-
-fun singleton s = CONS (s, K NIL);
-
-fun append NIL s = s ()
- | append (CONS (h,t)) s = CONS (h, fn () => append (t ()) s);
-
-fun map f =
- let
- fun m NIL = NIL
- | m (CONS (h, t)) = CONS (f h, fn () => m (t ()))
- in
- m
- end;
-
-fun maps f =
- let
- fun mm _ NIL = NIL
- | mm s (CONS (x, xs)) =
- let
- val (y, s') = f x s
- in
- CONS (y, fn () => mm s' (xs ()))
- end
- in
- mm
- end;
-
-fun zipwith f =
- let
- fun z NIL _ = NIL
- | z _ NIL = NIL
- | z (CONS (x,xs)) (CONS (y,ys)) =
- CONS (f x y, fn () => z (xs ()) (ys ()))
- in
- z
- end;
-
-fun zip s t = zipwith pair s t;
-
-fun take 0 _ = NIL
- | take n NIL = raise Subscript
- | take 1 (CONS (x,_)) = CONS (x, K NIL)
- | take n (CONS (x,xs)) = CONS (x, fn () => take (n - 1) (xs ()));
-
-fun drop n s = funpow n tl s handle Empty => raise Subscript;
-
-(* ------------------------------------------------------------------------- *)
-(* Stream versions of standard list operations: these might not terminate *)
-(* ------------------------------------------------------------------------- *)
-
-local
- fun len n NIL = n
- | len n (CONS (_,t)) = len (n + 1) (t ());
-in
- fun length s = len 0 s;
-end;
-
-fun exists pred =
- let
- fun f NIL = false
- | f (CONS (h,t)) = pred h orelse f (t ())
- in
- f
- end;
-
-fun all pred = not o exists (not o pred);
-
-fun filter p NIL = NIL
- | filter p (CONS (x,xs)) =
- if p x then CONS (x, fn () => filter p (xs ())) else filter p (xs ());
-
-fun foldl f =
- let
- fun fold b NIL = b
- | fold b (CONS (h,t)) = fold (f (h,b)) (t ())
- in
- fold
- end;
-
-fun concat NIL = NIL
- | concat (CONS (NIL, ss)) = concat (ss ())
- | concat (CONS (CONS (x, xs), ss)) =
- CONS (x, fn () => concat (CONS (xs (), ss)));
-
-fun mapPartial f =
- let
- fun mp NIL = NIL
- | mp (CONS (h,t)) =
- case f h of
- NONE => mp (t ())
- | SOME h' => CONS (h', fn () => mp (t ()))
- in
- mp
- end;
-
-fun mapsPartial f =
- let
- fun mm _ NIL = NIL
- | mm s (CONS (x, xs)) =
- let
- val (yo, s') = f x s
- val t = mm s' o xs
- in
- case yo of NONE => t () | SOME y => CONS (y, t)
- end
- in
- mm
- end;
-
-(* ------------------------------------------------------------------------- *)
-(* Stream operations *)
-(* ------------------------------------------------------------------------- *)
-
-fun memoize NIL = NIL
- | memoize (CONS (h,t)) = CONS (h, Lazy.memoize (fn () => memoize (t ())));
-
-local
- fun toLst res NIL = rev res
- | toLst res (CONS (x, xs)) = toLst (x :: res) (xs ());
-in
- fun toList s = toLst [] s;
-end;
-
-fun fromList [] = NIL
- | fromList (x :: xs) = CONS (x, fn () => fromList xs);
-
-fun toString s = implode (toList s);
-
-fun fromString s = fromList (explode s);
-
-fun toTextFile {filename = f} s =
- let
- val (h,close) =
- if f = "-" then (TextIO.stdOut, K ())
- else (TextIO.openOut f, TextIO.closeOut)
-
- fun toFile NIL = ()
- | toFile (CONS (x,y)) = (TextIO.output (h,x); toFile (y ()))
-
- val () = toFile s
- in
- close h
- end;
-
-fun fromTextFile {filename = f} =
- let
- val (h,close) =
- if f = "-" then (TextIO.stdIn, K ())
- else (TextIO.openIn f, TextIO.closeIn)
-
- fun strm () =
- case TextIO.inputLine h of
- NONE => (close h; NIL)
- | SOME s => CONS (s,strm)
- in
- memoize (strm ())
- end;
-
-end
-end;
-
(**** Original file: Heap.sig ****)
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Heap =
@@ -4550,7 +6512,7 @@
structure Metis = struct open Metis
(* Metis-specific ML environment *)
-nonfix ++ -- RL mem;
+nonfix ++ -- RL;
val explode = String.explode;
val implode = String.implode;
val print = TextIO.print;
@@ -4559,7 +6521,7 @@
(* ========================================================================= *)
(* A HEAP DATATYPE FOR ML *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
structure Heap :> Heap =
@@ -4622,12 +6584,12 @@
end;
fun toStream h =
- if null h then Stream.NIL
+ if null h then Stream.Nil
else
let
val (x,h) = remove h
in
- Stream.CONS (x, fn () => toStream h)
+ Stream.Cons (x, fn () => toStream h)
end;
fun toString h =
@@ -4636,89 +6598,1345 @@
end
end;
-(**** Original file: Parser.sig ****)
-
-(* ========================================================================= *)
-(* PARSING AND PRETTY PRINTING *)
-(* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
-(* ========================================================================= *)
-
-signature Parser =
+(**** Original file: Print.sig ****)
+
+(* ========================================================================= *)
+(* PRETTY-PRINTING *)
+(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+signature Print =
sig
(* ------------------------------------------------------------------------- *)
-(* Pretty printing for built-in types *)
-(* ------------------------------------------------------------------------- *)
-
-type ppstream = Metis.PP.ppstream
+(* A type of pretty-printers. *)
+(* ------------------------------------------------------------------------- *)
datatype breakStyle = Consistent | Inconsistent
-type 'a pp = ppstream -> 'a -> unit
-
-val lineLength : int Unsynchronized.ref
-
-val beginBlock : ppstream -> breakStyle -> int -> unit
-
-val endBlock : ppstream -> unit
-
-val addString : ppstream -> string -> unit
-
-val addBreak : ppstream -> int * int -> unit
-
-val addNewline : ppstream -> unit
+datatype ppStep =
+ BeginBlock of breakStyle * int
+ | EndBlock
+ | AddString of string
+ | AddBreak of int
+ | AddNewline
+
+type ppstream = ppStep Metis.Stream.stream
+
+type 'a pp = 'a -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer primitives. *)
+(* ------------------------------------------------------------------------- *)
+
+val beginBlock : breakStyle -> int -> ppstream
+
+val endBlock : ppstream
+
+val addString : string -> ppstream
+
+val addBreak : int -> ppstream
+
+val addNewline : ppstream
+
+val skip : ppstream
+
+val sequence : ppstream -> ppstream -> ppstream
+
+val duplicate : int -> ppstream -> ppstream
+
+val program : ppstream list -> ppstream
+
+val stream : ppstream Metis.Stream.stream -> ppstream
+
+val block : breakStyle -> int -> ppstream -> ppstream
+
+val blockProgram : breakStyle -> int -> ppstream list -> ppstream
+
+val bracket : string -> string -> ppstream -> ppstream
+
+val field : string -> ppstream -> ppstream
+
+val record : (string * ppstream) list -> ppstream
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer combinators. *)
+(* ------------------------------------------------------------------------- *)
val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
val ppBracket : string -> string -> 'a pp -> 'a pp
-val ppSequence : string -> 'a pp -> 'a list pp
-
-val ppBinop : string -> 'a pp -> 'b pp -> ('a * 'b) pp
+val ppOp : string -> ppstream
+
+val ppOp2 : string -> 'a pp -> 'b pp -> ('a * 'b) pp
+
+val ppOp3 : string -> string -> 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
+
+val ppOpList : string -> 'a pp -> 'a list pp
+
+val ppOpStream : string -> 'a pp -> 'a Metis.Stream.stream pp
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printers for common types. *)
+(* ------------------------------------------------------------------------- *)
val ppChar : char pp
val ppString : string pp
+val ppEscapeString : {escape : char list} -> string pp
+
val ppUnit : unit pp
val ppBool : bool pp
val ppInt : int pp
+val ppPrettyInt : int pp
+
val ppReal : real pp
+val ppPercent : real pp
+
val ppOrder : order pp
val ppList : 'a pp -> 'a list pp
+val ppStream : 'a pp -> 'a Metis.Stream.stream pp
+
val ppOption : 'a pp -> 'a option pp
val ppPair : 'a pp -> 'b pp -> ('a * 'b) pp
val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
-val toString : 'a pp -> 'a -> string (* Uses !lineLength *)
-
-val fromString : ('a -> string) -> 'a pp
-
-val ppTrace : 'a pp -> string -> 'a -> unit
-
-(* ------------------------------------------------------------------------- *)
-(* Recursive descent parsing combinators *)
-(* ------------------------------------------------------------------------- *)
-
-(* Generic parsers
-
-Recommended fixities:
+val ppBreakStyle : breakStyle pp
+
+val ppPpStep : ppStep pp
+
+val ppPpstream : ppstream pp
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing infix operators. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype infixes =
+ Infixes of
+ {token : string,
+ precedence : int,
+ leftAssoc : bool} list
+
+val tokensInfixes : infixes -> StringSet.set (* MODIFIED by Jasmin Blanchette *)
+
+val layerInfixes :
+ infixes ->
+ {tokens : {leftSpaces : int, token : string, rightSpaces : int} list,
+ leftAssoc : bool} list
+
+val ppInfixes :
+ infixes -> ('a -> (string * 'a * 'a) option) -> ('a * bool) pp ->
+ ('a * bool) pp
+
+(* ------------------------------------------------------------------------- *)
+(* Executing pretty-printers to generate lines. *)
+(* ------------------------------------------------------------------------- *)
+
+val execute : {lineLength : int} -> ppstream -> string Metis.Stream.stream
+
+(* ------------------------------------------------------------------------- *)
+(* Executing pretty-printers with a global line length. *)
+(* ------------------------------------------------------------------------- *)
+
+val lineLength : int Unsynchronized.ref
+
+val toString : 'a pp -> 'a -> string
+
+val toStream : 'a pp -> 'a -> string Metis.Stream.stream
+
+val trace : 'a pp -> string -> 'a -> unit
+
+end
+
+(**** Original file: Print.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+val foldl = List.foldl;
+val foldr = List.foldr;
+
+(* ========================================================================= *)
+(* PRETTY-PRINTING *)
+(* Copyright (c) 2001-2008 Joe Hurd, distributed under the BSD License *)
+(* ========================================================================= *)
+
+structure Print :> Print =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Constants. *)
+(* ------------------------------------------------------------------------- *)
+
+val initialLineLength = 75;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun revAppend xs s =
+ case xs of
+ [] => s ()
+ | x :: xs => revAppend xs (K (Stream.Cons (x,s)));
+
+fun revConcat strm =
+ case strm of
+ Stream.Nil => Stream.Nil
+ | Stream.Cons (h,t) => revAppend h (revConcat o t);
+
+local
+ fun join current prev = (prev ^ "\n", current);
+in
+ fun joinNewline strm =
+ case strm of
+ Stream.Nil => Stream.Nil
+ | Stream.Cons (h,t) => Stream.maps join Stream.singleton h (t ());
+end;
+
+local
+ fun calcSpaces n = nChars #" " n;
+
+ val cachedSpaces = Vector.tabulate (initialLineLength,calcSpaces);
+in
+ fun nSpaces n =
+ if n < initialLineLength then Vector.sub (cachedSpaces,n)
+ else calcSpaces n;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of pretty-printers. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype breakStyle = Consistent | Inconsistent;
+
+datatype ppStep =
+ BeginBlock of breakStyle * int
+ | EndBlock
+ | AddString of string
+ | AddBreak of int
+ | AddNewline;
+
+type ppstream = ppStep Stream.stream;
+
+type 'a pp = 'a -> ppstream;
+
+fun breakStyleToString style =
+ case style of
+ Consistent => "Consistent"
+ | Inconsistent => "Inconsistent";
+
+fun ppStepToString step =
+ case step of
+ BeginBlock _ => "BeginBlock"
+ | EndBlock => "EndBlock"
+ | AddString _ => "AddString"
+ | AddBreak _ => "AddBreak"
+ | AddNewline => "AddNewline";
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer primitives. *)
+(* ------------------------------------------------------------------------- *)
+
+fun beginBlock style indent = Stream.singleton (BeginBlock (style,indent));
+
+val endBlock = Stream.singleton EndBlock;
+
+fun addString s = Stream.singleton (AddString s);
+
+fun addBreak spaces = Stream.singleton (AddBreak spaces);
+
+val addNewline = Stream.singleton AddNewline;
+
+val skip : ppstream = Stream.Nil;
+
+fun sequence pp1 pp2 : ppstream = Stream.append pp1 (K pp2);
+
+local
+ fun dup pp n () = if n = 1 then pp else Stream.append pp (dup pp (n - 1));
+in
+ fun duplicate n pp = if n = 0 then skip else dup pp n ();
+end;
+
+val program : ppstream list -> ppstream = Stream.concatList;
+
+val stream : ppstream Stream.stream -> ppstream = Stream.concat;
+
+fun block style indent pp = program [beginBlock style indent, pp, endBlock];
+
+fun blockProgram style indent pps = block style indent (program pps);
+
+fun bracket l r pp =
+ blockProgram Inconsistent (size l)
+ [addString l,
+ pp,
+ addString r];
+
+fun field f pp =
+ blockProgram Inconsistent 2
+ [addString (f ^ " ="),
+ addBreak 1,
+ pp];
+
+val record =
+ let
+ val sep = sequence (addString ",") (addBreak 1)
+
+ fun recordField (f,pp) = field f pp
+
+ fun sepField f = sequence sep (recordField f)
+
+ fun fields [] = []
+ | fields (f :: fs) = recordField f :: map sepField fs
+ in
+ bracket "{" "}" o blockProgram Consistent 0 o fields
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printer combinators. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppMap f ppB a : ppstream = ppB (f a);
+
+fun ppBracket l r ppA a = bracket l r (ppA a);
+
+fun ppOp s = sequence (if s = "" then skip else addString s) (addBreak 1);
+
+fun ppOp2 ab ppA ppB (a,b) =
+ blockProgram Inconsistent 0
+ [ppA a,
+ ppOp ab,
+ ppB b];
+
+fun ppOp3 ab bc ppA ppB ppC (a,b,c) =
+ blockProgram Inconsistent 0
+ [ppA a,
+ ppOp ab,
+ ppB b,
+ ppOp bc,
+ ppC c];
+
+fun ppOpList s ppA =
+ let
+ fun ppOpA a = sequence (ppOp s) (ppA a)
+ in
+ fn [] => skip
+ | h :: t => blockProgram Inconsistent 0 (ppA h :: map ppOpA t)
+ end;
+
+fun ppOpStream s ppA =
+ let
+ fun ppOpA a = sequence (ppOp s) (ppA a)
+ in
+ fn Stream.Nil => skip
+ | Stream.Cons (h,t) =>
+ blockProgram Inconsistent 0
+ [ppA h,
+ Stream.concat (Stream.map ppOpA (t ()))]
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printers for common types. *)
+(* ------------------------------------------------------------------------- *)
+
+fun ppChar c = addString (str c);
+
+val ppString = addString;
+
+fun ppEscapeString {escape} =
+ let
+ val escapeMap = map (fn c => (c, "\\" ^ str c)) escape
+
+ fun escapeChar c =
+ case c of
+ #"\\" => "\\\\"
+ | #"\n" => "\\n"
+ | #"\t" => "\\t"
+ | _ =>
+ case List.find (equal c o fst) escapeMap of
+ SOME (_,s) => s
+ | NONE => str c
+ in
+ fn s => addString (String.translate escapeChar s)
+ end;
+
+val ppUnit : unit pp = K (addString "()");
+
+fun ppBool b = addString (if b then "true" else "false");
+
+fun ppInt i = addString (Int.toString i);
+
+local
+ val ppNeg = addString "~"
+ and ppSep = addString ","
+ and ppZero = addString "0"
+ and ppZeroZero = addString "00";
+
+ fun ppIntBlock i =
+ if i < 10 then sequence ppZeroZero (ppInt i)
+ else if i < 100 then sequence ppZero (ppInt i)
+ else ppInt i;
+
+ fun ppIntBlocks i =
+ if i < 1000 then ppInt i
+ else sequence (ppIntBlocks (i div 1000))
+ (sequence ppSep (ppIntBlock (i mod 1000)));
+in
+ fun ppPrettyInt i =
+ if i < 0 then sequence ppNeg (ppIntBlocks (~i))
+ else ppIntBlocks i;
+end;
+
+fun ppReal r = addString (Real.toString r);
+
+fun ppPercent p = addString (percentToString p);
+
+fun ppOrder x =
+ addString
+ (case x of
+ LESS => "Less"
+ | EQUAL => "Equal"
+ | GREATER => "Greater");
+
+fun ppList ppA = ppBracket "[" "]" (ppOpList "," ppA);
+
+fun ppStream ppA = ppBracket "[" "]" (ppOpStream "," ppA);
+
+fun ppOption ppA ao =
+ case ao of
+ SOME a => ppA a
+ | NONE => addString "-";
+
+fun ppPair ppA ppB = ppBracket "(" ")" (ppOp2 "," ppA ppB);
+
+fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppOp3 "," "," ppA ppB ppC);
+
+fun ppBreakStyle style = addString (breakStyleToString style);
+
+fun ppPpStep step =
+ let
+ val cmd = ppStepToString step
+ in
+ blockProgram Inconsistent 2
+ (addString cmd ::
+ (case step of
+ BeginBlock style_indent =>
+ [addBreak 1,
+ ppPair ppBreakStyle ppInt style_indent]
+ | EndBlock => []
+ | AddString s =>
+ [addBreak 1,
+ addString ("\"" ^ s ^ "\"")]
+ | AddBreak n =>
+ [addBreak 1,
+ ppInt n]
+ | AddNewline => []))
+ end;
+
+val ppPpstream = ppStream ppPpStep;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing infix operators. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype infixes =
+ Infixes of
+ {token : string,
+ precedence : int,
+ leftAssoc : bool} list;
+
+local
+ fun chop l =
+ case l of
+ #" " :: l => let val (n,l) = chop l in (n + 1, l) end
+ | _ => (0,l);
+in
+ fun opSpaces tok =
+ let
+ val tok = explode tok
+ val (r,tok) = chop (rev tok)
+ val (l,tok) = chop (rev tok)
+ val tok = implode tok
+ in
+ {leftSpaces = l, token = tok, rightSpaces = r}
+ end;
+end;
+
+fun ppOpSpaces {leftSpaces,token,rightSpaces} =
+ let
+ val leftSpacesToken =
+ if leftSpaces = 0 then token else nSpaces leftSpaces ^ token
+ in
+ sequence
+ (addString leftSpacesToken)
+ (addBreak rightSpaces)
+ end;
+
+local
+ fun new t l acc = {tokens = [opSpaces t], leftAssoc = l} :: acc;
+
+ fun add t l acc =
+ case acc of
+ [] => raise Bug "Print.layerInfixOps.layer"
+ | {tokens = ts, leftAssoc = l'} :: acc =>
+ if l = l' then {tokens = opSpaces t :: ts, leftAssoc = l} :: acc
+ else raise Bug "Print.layerInfixOps: mixed assocs";
+
+ fun layer ({token = t, precedence = p, leftAssoc = l}, (acc,p')) =
+ let
+ val acc = if p = p' then add t l acc else new t l acc
+ in
+ (acc,p)
+ end;
+in
+ fun layerInfixes (Infixes i) =
+ case sortMap #precedence Int.compare i of
+ [] => []
+ | {token = t, precedence = p, leftAssoc = l} :: i =>
+ let
+ val acc = new t l []
+
+ val (acc,_) = List.foldl layer (acc,p) i
+ in
+ acc
+ end;
+end;
+
+val tokensLayeredInfixes =
+ let
+ fun addToken ({leftSpaces = _, token = t, rightSpaces = _}, s) =
+ StringSet.add s t
+
+ fun addTokens ({tokens = t, leftAssoc = _}, s) =
+ List.foldl addToken s t
+ in
+ List.foldl addTokens StringSet.empty
+ end;
+
+val tokensInfixes = tokensLayeredInfixes o layerInfixes;
+
+local
+ val mkTokenMap =
+ let
+ fun add (token,m) =
+ let
+ val {leftSpaces = _, token = t, rightSpaces = _} = token
+ in
+ StringMap.insert m (t, ppOpSpaces token)
+ end
+ in
+ List.foldl add (StringMap.new ())
+ end;
+in
+ fun ppGenInfix {tokens,leftAssoc} =
+ let
+ val tokenMap = mkTokenMap tokens
+ in
+ fn dest => fn ppSub =>
+ let
+ fun dest' tm =
+ case dest tm of
+ NONE => NONE
+ | SOME (t,a,b) =>
+ case StringMap.peek tokenMap t of
+ NONE => NONE
+ | SOME p => SOME (p,a,b)
+
+ fun ppGo (tmr as (tm,r)) =
+ case dest' tm of
+ NONE => ppSub tmr
+ | SOME (p,a,b) =>
+ program
+ [(if leftAssoc then ppGo else ppSub) (a,true),
+ p,
+ (if leftAssoc then ppSub else ppGo) (b,r)]
+ in
+ fn tmr as (tm,_) =>
+ if Option.isSome (dest' tm) then
+ block Inconsistent 0 (ppGo tmr)
+ else
+ ppSub tmr
+ end
+ end;
+end
+
+fun ppInfixes ops =
+ let
+ val layeredOps = layerInfixes ops
+
+ val toks = tokensLayeredInfixes layeredOps
+
+ val iprinters = List.map ppGenInfix layeredOps
+ in
+ fn dest => fn ppSub =>
+ let
+ fun printer sub = foldl (fn (ip,p) => ip dest p) sub iprinters
+
+ fun isOp t =
+ case dest t of
+ SOME (x,_,_) => StringSet.member x toks
+ | NONE => false
+
+ fun subpr (tmr as (tm,_)) =
+ if isOp tm then
+ blockProgram Inconsistent 1
+ [addString "(",
+ printer subpr (tm,false),
+ addString ")"]
+ else
+ ppSub tmr
+ in
+ fn tmr => block Inconsistent 0 (printer subpr tmr)
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Executing pretty-printers to generate lines. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype blockBreakStyle =
+ InconsistentBlock
+ | ConsistentBlock
+ | BreakingBlock;
+
+datatype block =
+ Block of
+ {indent : int,
+ style : blockBreakStyle,
+ size : int,
+ chunks : chunk list}
+
+and chunk =
+ StringChunk of {size : int, string : string}
+ | BreakChunk of int
+ | BlockChunk of block;
+
+datatype state =
+ State of
+ {blocks : block list,
+ lineIndent : int,
+ lineSize : int};
+
+val initialIndent = 0;
+
+val initialStyle = Inconsistent;
+
+fun liftStyle style =
+ case style of
+ Inconsistent => InconsistentBlock
+ | Consistent => ConsistentBlock;
+
+fun breakStyle style =
+ case style of
+ ConsistentBlock => BreakingBlock
+ | _ => style;
+
+fun sizeBlock (Block {size,...}) = size;
+
+fun sizeChunk chunk =
+ case chunk of
+ StringChunk {size,...} => size
+ | BreakChunk spaces => spaces
+ | BlockChunk block => sizeBlock block;
+
+val splitChunks =
+ let
+ fun split _ [] = NONE
+ | split acc (chunk :: chunks) =
+ case chunk of
+ BreakChunk _ => SOME (rev acc, chunks)
+ | _ => split (chunk :: acc) chunks
+ in
+ split []
+ end;
+
+val sizeChunks = List.foldl (fn (c,z) => sizeChunk c + z) 0;
+
+local
+ fun render acc [] = acc
+ | render acc (chunk :: chunks) =
+ case chunk of
+ StringChunk {string = s, ...} => render (acc ^ s) chunks
+ | BreakChunk n => render (acc ^ nSpaces n) chunks
+ | BlockChunk (Block {chunks = l, ...}) =>
+ render acc (List.revAppend (l,chunks));
+in
+ fun renderChunks indent chunks = render (nSpaces indent) (rev chunks);
+
+ fun renderChunk indent chunk = renderChunks indent [chunk];
+end;
+
+fun isEmptyBlock block =
+ let
+ val Block {indent = _, style = _, size, chunks} = block
+
+ val empty = null chunks
+
+(*BasicDebug
+ val _ = not empty orelse size = 0 orelse
+ raise Bug "Print.isEmptyBlock: bad size"
+*)
+ in
+ empty
+ end;
+
+fun checkBlock ind block =
+ let
+ val Block {indent, style = _, size, chunks} = block
+ val _ = indent >= ind orelse raise Bug "Print.checkBlock: bad indents"
+ val size' = checkChunks indent chunks
+ val _ = size = size' orelse raise Bug "Print.checkBlock: wrong size"
+ in
+ size
+ end
+
+and checkChunks ind chunks =
+ case chunks of
+ [] => 0
+ | chunk :: chunks => checkChunk ind chunk + checkChunks ind chunks
+
+and checkChunk ind chunk =
+ case chunk of
+ StringChunk {size,...} => size
+ | BreakChunk spaces => spaces
+ | BlockChunk block => checkBlock ind block;
+
+val checkBlocks =
+ let
+ fun check ind blocks =
+ case blocks of
+ [] => 0
+ | block :: blocks =>
+ let
+ val Block {indent,...} = block
+ in
+ checkBlock ind block + check indent blocks
+ end
+ in
+ check initialIndent o rev
+ end;
+
+val initialBlock =
+ let
+ val indent = initialIndent
+ val style = liftStyle initialStyle
+ val size = 0
+ val chunks = []
+ in
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+ end;
+
+val initialState =
+ let
+ val blocks = [initialBlock]
+ val lineIndent = initialIndent
+ val lineSize = 0
+ in
+ State
+ {blocks = blocks,
+ lineIndent = lineIndent,
+ lineSize = lineSize}
+ end;
+
+(*BasicDebug
+fun checkState state =
+ (let
+ val State {blocks, lineIndent = _, lineSize} = state
+ val lineSize' = checkBlocks blocks
+ val _ = lineSize = lineSize' orelse
+ raise Error "wrong lineSize"
+ in
+ ()
+ end
+ handle Error err => raise Bug err)
+ handle Bug bug => raise Bug ("Print.checkState: " ^ bug);
+*)
+
+fun isFinalState state =
+ let
+ val State {blocks,lineIndent,lineSize} = state
+ in
+ case blocks of
+ [] => raise Bug "Print.isFinalState: no block"
+ | [block] => isEmptyBlock block
+ | _ :: _ :: _ => false
+ end;
+
+local
+ fun renderBreak lineIndent (chunks,lines) =
+ let
+ val line = renderChunks lineIndent chunks
+
+ val lines = line :: lines
+ in
+ lines
+ end;
+
+ fun renderBreaks lineIndent lineIndent' breaks lines =
+ case rev breaks of
+ [] => raise Bug "Print.renderBreaks"
+ | c :: cs =>
+ let
+ val lines = renderBreak lineIndent (c,lines)
+ in
+ List.foldl (renderBreak lineIndent') lines cs
+ end;
+
+ fun splitAllChunks cumulatingChunks =
+ let
+ fun split chunks =
+ case splitChunks chunks of
+ SOME (prefix,chunks) => prefix :: split chunks
+ | NONE => [List.concat (chunks :: cumulatingChunks)]
+ in
+ split
+ end;
+
+ fun mkBreak style cumulatingChunks chunks =
+ case splitChunks chunks of
+ NONE => NONE
+ | SOME (chunks,broken) =>
+ let
+ val breaks =
+ case style of
+ InconsistentBlock =>
+ [List.concat (broken :: cumulatingChunks)]
+ | _ => splitAllChunks cumulatingChunks broken
+ in
+ SOME (breaks,chunks)
+ end;
+
+ fun naturalBreak blocks =
+ case blocks of
+ [] => Right ([],[])
+ | block :: blocks =>
+ case naturalBreak blocks of
+ Left (breaks,blocks,lineIndent,lineSize) =>
+ let
+ val Block {size,...} = block
+
+ val blocks = block :: blocks
+
+ val lineSize = lineSize + size
+ in
+ Left (breaks,blocks,lineIndent,lineSize)
+ end
+ | Right (cumulatingChunks,blocks) =>
+ let
+ val Block {indent,style,size,chunks} = block
+
+ val style = breakStyle style
+ in
+ case mkBreak style cumulatingChunks chunks of
+ SOME (breaks,chunks) =>
+ let
+ val size = sizeChunks chunks
+
+ val block =
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+
+ val blocks = block :: blocks
+
+ val lineIndent = indent
+
+ val lineSize = size
+ in
+ Left (breaks,blocks,lineIndent,lineSize)
+ end
+ | NONE =>
+ let
+ val cumulatingChunks = chunks :: cumulatingChunks
+
+ val size = 0
+
+ val chunks = []
+
+ val block =
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+
+ val blocks = block :: blocks
+ in
+ Right (cumulatingChunks,blocks)
+ end
+ end;
+
+ fun forceBreakBlock cumulatingChunks block =
+ let
+ val Block {indent, style, size = _, chunks} = block
+
+ val style = breakStyle style
+
+ val break =
+ case mkBreak style cumulatingChunks chunks of
+ SOME (breaks,chunks) =>
+ let
+ val lineSize = sizeChunks chunks
+ val lineIndent = indent
+ in
+ SOME (breaks,chunks,lineIndent,lineSize)
+ end
+ | NONE => forceBreakChunks cumulatingChunks chunks
+ in
+ case break of
+ SOME (breaks,chunks,lineIndent,lineSize) =>
+ let
+ val size = lineSize
+
+ val block =
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+ in
+ SOME (breaks,block,lineIndent,lineSize)
+ end
+ | NONE => NONE
+ end
+
+ and forceBreakChunks cumulatingChunks chunks =
+ case chunks of
+ [] => NONE
+ | chunk :: chunks =>
+ case forceBreakChunk (chunks :: cumulatingChunks) chunk of
+ SOME (breaks,chunk,lineIndent,lineSize) =>
+ let
+ val chunks = [chunk]
+ in
+ SOME (breaks,chunks,lineIndent,lineSize)
+ end
+ | NONE =>
+ case forceBreakChunks cumulatingChunks chunks of
+ SOME (breaks,chunks,lineIndent,lineSize) =>
+ let
+ val chunks = chunk :: chunks
+
+ val lineSize = lineSize + sizeChunk chunk
+ in
+ SOME (breaks,chunks,lineIndent,lineSize)
+ end
+ | NONE => NONE
+
+ and forceBreakChunk cumulatingChunks chunk =
+ case chunk of
+ StringChunk _ => NONE
+ | BreakChunk _ => raise Bug "Print.forceBreakChunk: BreakChunk"
+ | BlockChunk block =>
+ case forceBreakBlock cumulatingChunks block of
+ SOME (breaks,block,lineIndent,lineSize) =>
+ let
+ val chunk = BlockChunk block
+ in
+ SOME (breaks,chunk,lineIndent,lineSize)
+ end
+ | NONE => NONE;
+
+ fun forceBreak cumulatingChunks blocks' blocks =
+ case blocks of
+ [] => NONE
+ | block :: blocks =>
+ let
+ val cumulatingChunks =
+ case cumulatingChunks of
+ [] => raise Bug "Print.forceBreak: null cumulatingChunks"
+ | _ :: cumulatingChunks => cumulatingChunks
+
+ val blocks' =
+ case blocks' of
+ [] => raise Bug "Print.forceBreak: null blocks'"
+ | _ :: blocks' => blocks'
+ in
+ case forceBreakBlock cumulatingChunks block of
+ SOME (breaks,block,lineIndent,lineSize) =>
+ let
+ val blocks = block :: blocks'
+ in
+ SOME (breaks,blocks,lineIndent,lineSize)
+ end
+ | NONE =>
+ case forceBreak cumulatingChunks blocks' blocks of
+ SOME (breaks,blocks,lineIndent,lineSize) =>
+ let
+ val blocks = block :: blocks
+
+ val Block {size,...} = block
+
+ val lineSize = lineSize + size
+ in
+ SOME (breaks,blocks,lineIndent,lineSize)
+ end
+ | NONE => NONE
+ end;
+
+ fun normalize lineLength lines state =
+ let
+ val State {blocks,lineIndent,lineSize} = state
+ in
+ if lineIndent + lineSize <= lineLength then (lines,state)
+ else
+ let
+ val break =
+ case naturalBreak blocks of
+ Left break => SOME break
+ | Right (c,b) => forceBreak c b blocks
+ in
+ case break of
+ SOME (breaks,blocks,lineIndent',lineSize) =>
+ let
+ val lines = renderBreaks lineIndent lineIndent' breaks lines
+
+ val state =
+ State
+ {blocks = blocks,
+ lineIndent = lineIndent',
+ lineSize = lineSize}
+ in
+ normalize lineLength lines state
+ end
+ | NONE => (lines,state)
+ end
+ end;
+
+(*BasicDebug
+ val normalize = fn lineLength => fn lines => fn state =>
+ let
+ val () = checkState state
+ in
+ normalize lineLength lines state
+ end
+ handle Bug bug =>
+ raise Bug ("Print.normalize: before normalize:\n" ^ bug)
+*)
+
+ fun executeBeginBlock (style,ind) lines state =
+ let
+ val State {blocks,lineIndent,lineSize} = state
+
+ val Block {indent,...} =
+ case blocks of
+ [] => raise Bug "Print.executeBeginBlock: no block"
+ | block :: _ => block
+
+ val indent = indent + ind
+
+ val style = liftStyle style
+
+ val size = 0
+
+ val chunks = []
+
+ val block =
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+
+ val blocks = block :: blocks
+
+ val state =
+ State
+ {blocks = blocks,
+ lineIndent = lineIndent,
+ lineSize = lineSize}
+ in
+ (lines,state)
+ end;
+
+ fun executeEndBlock lines state =
+ let
+ val State {blocks,lineIndent,lineSize} = state
+
+ val (lineSize,blocks) =
+ case blocks of
+ [] => raise Bug "Print.executeEndBlock: no block"
+ | topBlock :: blocks =>
+ let
+ val Block
+ {indent = topIndent,
+ style = topStyle,
+ size = topSize,
+ chunks = topChunks} = topBlock
+ in
+ case topChunks of
+ [] => (lineSize,blocks)
+ | headTopChunks :: tailTopChunks =>
+ let
+ val (lineSize,topSize,topChunks) =
+ case headTopChunks of
+ BreakChunk spaces =>
+ let
+ val lineSize = lineSize - spaces
+ and topSize = topSize - spaces
+ and topChunks = tailTopChunks
+ in
+ (lineSize,topSize,topChunks)
+ end
+ | _ => (lineSize,topSize,topChunks)
+
+ val topBlock =
+ Block
+ {indent = topIndent,
+ style = topStyle,
+ size = topSize,
+ chunks = topChunks}
+ in
+ case blocks of
+ [] => raise Error "Print.executeEndBlock: no block"
+ | block :: blocks =>
+ let
+ val Block {indent,style,size,chunks} = block
+
+ val size = size + topSize
+
+ val chunks = BlockChunk topBlock :: chunks
+
+ val block =
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+
+ val blocks = block :: blocks
+ in
+ (lineSize,blocks)
+ end
+ end
+ end
+
+ val state =
+ State
+ {blocks = blocks,
+ lineIndent = lineIndent,
+ lineSize = lineSize}
+ in
+ (lines,state)
+ end;
+
+ fun executeAddString lineLength s lines state =
+ let
+ val State {blocks,lineIndent,lineSize} = state
+
+ val n = size s
+
+ val blocks =
+ case blocks of
+ [] => raise Bug "Print.executeAddString: no block"
+ | Block {indent,style,size,chunks} :: blocks =>
+ let
+ val size = size + n
+
+ val chunk = StringChunk {size = n, string = s}
+
+ val chunks = chunk :: chunks
+
+ val block =
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+
+ val blocks = block :: blocks
+ in
+ blocks
+ end
+
+ val lineSize = lineSize + n
+
+ val state =
+ State
+ {blocks = blocks,
+ lineIndent = lineIndent,
+ lineSize = lineSize}
+ in
+ normalize lineLength lines state
+ end;
+
+ fun executeAddBreak lineLength spaces lines state =
+ let
+ val State {blocks,lineIndent,lineSize} = state
+
+ val (blocks,lineSize) =
+ case blocks of
+ [] => raise Bug "Print.executeAddBreak: no block"
+ | Block {indent,style,size,chunks} :: blocks' =>
+ case chunks of
+ [] => (blocks,lineSize)
+ | chunk :: chunks' =>
+ let
+ val spaces =
+ case style of
+ BreakingBlock => lineLength + 1
+ | _ => spaces
+
+ val size = size + spaces
+
+ val chunks =
+ case chunk of
+ BreakChunk k => BreakChunk (k + spaces) :: chunks'
+ | _ => BreakChunk spaces :: chunks
+
+ val block =
+ Block
+ {indent = indent,
+ style = style,
+ size = size,
+ chunks = chunks}
+
+ val blocks = block :: blocks'
+
+ val lineSize = lineSize + spaces
+ in
+ (blocks,lineSize)
+ end
+
+ val state =
+ State
+ {blocks = blocks,
+ lineIndent = lineIndent,
+ lineSize = lineSize}
+ in
+ normalize lineLength lines state
+ end;
+
+ fun executeBigBreak lineLength lines state =
+ executeAddBreak lineLength (lineLength + 1) lines state;
+
+ fun executeAddNewline lineLength lines state =
+ let
+ val (lines,state) = executeAddString lineLength "" lines state
+ val (lines,state) = executeBigBreak lineLength lines state
+ in
+ executeAddString lineLength "" lines state
+ end;
+
+ fun final lineLength lines state =
+ let
+ val lines =
+ if isFinalState state then lines
+ else
+ let
+ val (lines,state) = executeBigBreak lineLength lines state
+
+(*BasicDebug
+ val _ = isFinalState state orelse raise Bug "Print.final"
+*)
+ in
+ lines
+ end
+ in
+ if null lines then Stream.Nil else Stream.singleton lines
+ end;
+in
+ fun execute {lineLength} =
+ let
+ fun advance step state =
+ let
+ val lines = []
+ in
+ case step of
+ BeginBlock style_