--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/metis.ML Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,17459 @@
+(******************************************************************)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
+(******************************************************************)
+
+print_depth 0;
+
+structure Metis = struct end;
+
+(**** Original file: Portable.sig ****)
+
+(* ========================================================================= *)
+(* ML SPECIFIC FUNCTIONS *)
+(* Copyright (c) 2001-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Portable =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* The ML implementation *)
+(* ------------------------------------------------------------------------- *)
+
+val ml : string
+
+(* ------------------------------------------------------------------------- *)
+(* Pointer equality using the run-time system *)
+(* ------------------------------------------------------------------------- *)
+
+val pointerEqual : 'a * 'a -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Timing function applications *)
+(* ------------------------------------------------------------------------- *)
+
+val time : ('a -> 'b) -> 'a -> 'b
+
+end
+
+(**** Original file: PortableIsabelle.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* Isabelle ML SPECIFIC FUNCTIONS *)
+(* ========================================================================= *)
+
+structure Portable :> Portable =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* The ML implementation. *)
+(* ------------------------------------------------------------------------- *)
+
+val ml = ml_system;
+
+(* ------------------------------------------------------------------------- *)
+(* Pointer equality using the run-time system. *)
+(* ------------------------------------------------------------------------- *)
+
+val pointerEqual = pointer_eq;
+
+(* ------------------------------------------------------------------------- *)
+(* Timing function applications a la Mosml.time. *)
+(* ------------------------------------------------------------------------- *)
+
+val time = timeap;
+
+end
+
+(* ------------------------------------------------------------------------- *)
+(* Quotations a la Moscow ML. *)
+(* ------------------------------------------------------------------------- *)
+
+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 union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* 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 ref,
+ back: int ref,
+ size: int} (* fixed size of element array *)
+with
+
+ fun is_empty (QUEUE{front=ref ~1, back=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=ref ~1, back=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 ref
+with
+ fun mk_indent_stack() = Istack (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 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 ref, (* Processed *)
+ Ublocks : block_info list ref} (* Unprocessed *)
+ | E of {Pend : int ref, Uend : int ref}
+ | BR of {Distance_to_next_break : int 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 ref -> unit, (* increment circular buffer index *)
+ space_left : int ref, (* remaining columns on page *)
+ left_index : int ref, (* insertion index *)
+ right_index : int ref, (* output index *)
+ left_sum : int ref, (* size of strings and spaces inserted *)
+ right_sum : int 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 = ref linewidth,
+ left_index = ref 0, right_index = ref 0,
+ left_sum = ref 0, right_sum = 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 = ref [], Ublocks = ref []}) =
+ raise Fail "PP-error: print_BB"
+ | print_BB (PPS{the_indent_stack,linewidth,space_left=ref sp_left,...},
+ {Pblocks as ref({How_to_indent=CONSISTENT,Block_size,
+ Block_offset}::rst),
+ Ublocks=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=ref sp_left,...},
+ {Pblocks as ref({Block_size,Block_offset,...}::rst),Ublocks=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=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 = ref 0, Uend = 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 = ref [], Ublocks = ref []}) => true
+ | (BB _) => false
+ | (E {Pend = ref 0, Uend = 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 = ref [], Ublocks = ref []} =>
+ raise Fail "PP-error: BB_size"
+ | {Pblocks as ref(_::_),Ublocks=ref[]} => POS
+ | {Ublocks, ...} => last_size (!Ublocks))
+ | token_size (E{Pend = ref 0, Uend = ref 0}) =
+ raise Fail "PP-error: token_size.E"
+ | token_size (E{Pend = 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 = ref [], Ublocks = ref []}) =>
+ (update(the_token_buffer,!left_index,
+ initial_token_value);
+ ++left_index)
+ | (BB _) => ()
+ | (E {Pend = ref 0, Uend = 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 = ref (~(!right_sum)),
+ Block_offset = offset,
+ How_to_indent = style}::(!Ublocks)
+ | _ => (update(the_token_buffer, !right_index,
+ BB{Pblocks = ref [],
+ Ublocks = ref [{Block_size = 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 = ref 1, Uend = 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 = ref 1, Pend = 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 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 = 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 ref[{Block_size,...}:block_info],...}) =
+ (pop_bottom_delim_stack dstack;
+ Block_size := INFINITY)
+ | set (_,BB {Ublocks = 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 = 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: Random.sig ****)
+
+(* Random -- random number generator *)
+
+signature Random =
+sig
+
+type generator
+
+val newgenseed : real -> generator
+val newgen : unit -> generator
+val random : generator -> real
+val randomlist : int * generator -> real list
+val range : int * int -> generator -> int
+val rangelist : int * int -> int * generator -> int list
+
+end
+
+(*
+ [generator] is the type of random number generators, here the
+ linear congruential generators from Paulson 1991, 1996.
+
+ [newgenseed seed] returns a random number generator with the given seed.
+
+ [newgen ()] returns a random number generator, taking the seed from
+ the system clock.
+
+ [random gen] returns a random number in the interval [0..1).
+
+ [randomlist (n, gen)] returns a list of n random numbers in the
+ interval [0,1).
+
+ [range (min, max) gen] returns an integral random number in the
+ range [min, max). Raises Fail if min > max.
+
+ [rangelist (min, max) (n, gen)] returns a list of n integral random
+ numbers in the range [min, max). Raises Fail if min > max.
+*)
+
+(**** Original file: Random.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* Random -- Moscow ML library 1995-04-23, 1999-02-24 *)
+
+structure Random :> Random =
+struct
+
+type generator = {seedref : real ref}
+
+(* Generating random numbers. Paulson, page 96 *)
+
+val a = 16807.0
+val m = 2147483647.0
+fun nextrand seed =
+ let val t = a*seed
+ in t - m * real(floor(t/m)) end
+
+fun newgenseed seed =
+ {seedref = ref (nextrand seed)};
+
+fun newgen () = newgenseed (Time.toReal (Time.now ()));
+
+fun random {seedref as ref seed} =
+ (seedref := nextrand seed; seed / m);
+
+fun randomlist (n, {seedref as ref seed0}) =
+ let fun h 0 seed res = (seedref := seed; res)
+ | h i seed res = h (i-1) (nextrand seed) (seed / m :: res)
+ in h n seed0 [] end;
+
+fun range (min, max) =
+ if min > max then raise Fail "Random.range: empty range"
+ else
+ fn {seedref as ref seed} =>
+ (seedref := nextrand seed; min + (floor(real(max-min) * seed / m)));
+
+fun rangelist (min, max) =
+ if min > max then raise Fail "Random.rangelist: empty range"
+ else
+ fn (n, {seedref as ref seed0}) =>
+ let fun h 0 seed res = (seedref := seed; res)
+ | h i seed res = h (i-1) (nextrand seed)
+ (min + floor(real(max-min) * seed / m) :: res)
+ in h n seed0 [] end
+
+end
+end;
+
+(**** Original file: Useful.sig ****)
+
+(* ========================================================================= *)
+(* ML UTILITY FUNCTIONS *)
+(* Copyright (c) 2001-2005 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Useful =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Exceptions. *)
+(* ------------------------------------------------------------------------- *)
+
+exception Error of string
+
+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
+
+(* ------------------------------------------------------------------------- *)
+(* Tracing. *)
+(* ------------------------------------------------------------------------- *)
+
+val tracePrint : (string -> unit) ref
+
+val maxTraceLevel : int ref
+
+val traceLevel : int ref (* in the set {0, ..., maxTraceLevel} *)
+
+val traceAlign : {module : string, alignment : int -> int option} list ref
+
+val tracing : {module : string, level : int} -> bool
+
+val trace : string -> unit
+
+(* ------------------------------------------------------------------------- *)
+(* Combinators. *)
+(* ------------------------------------------------------------------------- *)
+
+val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
+
+val I : 'a -> 'a
+
+val K : 'a -> 'b -> 'a
+
+val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
+
+val W : ('a -> 'a -> 'b) -> 'a -> 'b
+
+val funpow : int -> ('a -> 'a) -> 'a -> 'a
+
+val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a
+
+val equal : ''a -> ''a -> bool
+
+val notEqual : ''a -> ''a -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Pairs. *)
+(* ------------------------------------------------------------------------- *)
+
+val fst : 'a * 'b -> 'a
+
+val snd : 'a * 'b -> 'b
+
+val pair : 'a -> 'b -> 'a * 'b
+
+val swap : 'a * 'b -> 'b * 'a
+
+val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
+
+val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
+
+val ## : ('a -> 'c) * ('b -> 'd) -> 'a * 'b -> 'c * 'd
+
+(* ------------------------------------------------------------------------- *)
+(* State transformers. *)
+(* ------------------------------------------------------------------------- *)
+
+val unit : 'a -> 's -> 'a * 's
+
+val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's
+
+val mmap : ('a -> 'b) -> ('s -> 'a * 's) -> 's -> 'b * 's
+
+val mjoin : ('s -> ('s -> 'a * 's) * 's) -> 's -> 'a * 's
+
+val mwhile : ('a -> bool) -> ('a -> 's -> 'a * 's) -> 'a -> 's -> 'a * 's
+
+(* ------------------------------------------------------------------------- *)
+(* Lists: note we count elements from 0. *)
+(* ------------------------------------------------------------------------- *)
+
+val cons : 'a -> 'a list -> 'a list
+
+val hdTl : 'a list -> 'a * 'a list
+
+val append : 'a list -> 'a list -> 'a list
+
+val singleton : 'a -> 'a list
+
+val first : ('a -> 'b option) -> 'a list -> 'b option
+
+val 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 zip : 'a list -> 'b list -> ('a * 'b) list
+
+val unzip : ('a * 'b) list -> 'a list * 'b list
+
+val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
+
+val cart : 'a list -> 'b list -> ('a * 'b) list
+
+val divide : 'a list -> int -> 'a list * 'a list (* Subscript *)
+
+val revDivide : 'a list -> int -> 'a list * 'a list (* Subscript *)
+
+val updateNth : int * 'a -> 'a list -> 'a list (* Subscript *)
+
+val deleteNth : int -> 'a list -> 'a list (* Subscript *)
+
+(* ------------------------------------------------------------------------- *)
+(* Sets implemented with lists. *)
+(* ------------------------------------------------------------------------- *)
+
+val mem : ''a -> ''a list -> bool
+
+val insert : ''a -> ''a list -> ''a list
+
+val delete : ''a -> ''a list -> ''a list
+
+val setify : ''a list -> ''a list (* removes duplicates *)
+
+val union : ''a list -> ''a list -> ''a list
+
+val intersect : ''a list -> ''a list -> ''a list
+
+val difference : ''a list -> ''a list -> ''a list
+
+val subset : ''a list -> ''a list -> bool
+
+val distinct : ''a list -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* 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 boolCompare : bool * bool -> order (* true < false *)
+
+(* ------------------------------------------------------------------------- *)
+(* Sorting and searching. *)
+(* ------------------------------------------------------------------------- *)
+
+val minimum : ('a * 'a -> order) -> 'a list -> 'a * 'a list (* Empty *)
+
+val maximum : ('a * 'a -> order) -> 'a list -> 'a * 'a list (* Empty *)
+
+val merge : ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
+
+val sort : ('a * 'a -> order) -> 'a list -> 'a list
+
+val sortMap : ('a -> 'b) -> ('b * 'b -> order) -> 'a list -> 'a list
+
+(* ------------------------------------------------------------------------- *)
+(* Integers. *)
+(* ------------------------------------------------------------------------- *)
+
+val interval : int -> int -> int list
+
+val divides : int -> int -> bool
+
+val gcd : int -> int -> int
+
+val primes : int -> int list
+
+val primesUpTo : int -> int list
+
+(* ------------------------------------------------------------------------- *)
+(* Strings. *)
+(* ------------------------------------------------------------------------- *)
+
+val rot : int -> char -> char
+
+val charToInt : char -> int option
+
+val charFromInt : int -> char option
+
+val nChars : char -> int -> string
+
+val chomp : string -> string
+
+val trim : string -> string
+
+val join : string -> string list -> string
+
+val split : string -> string -> string list
+
+val mkPrefix : string -> string -> string
+
+val destPrefix : string -> string -> string
+
+val isPrefix : string -> string -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Tables. *)
+(* ------------------------------------------------------------------------- *)
+
+type columnAlignment = {leftAlign : bool, padChar : char}
+
+val alignColumn : columnAlignment -> string list -> string list -> string list
+
+val alignTable : columnAlignment list -> string list list -> string list
+
+(* ------------------------------------------------------------------------- *)
+(* Reals. *)
+(* ------------------------------------------------------------------------- *)
+
+val percentToString : real -> string
+
+val pos : real -> real
+
+val log2 : real -> real (* Domain *)
+
+(* ------------------------------------------------------------------------- *)
+(* Sum datatype. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('a,'b) sum = Left of 'a | Right of 'b
+
+val destLeft : ('a,'b) sum -> 'a
+
+val isLeft : ('a,'b) sum -> bool
+
+val destRight : ('a,'b) sum -> 'b
+
+val isRight : ('a,'b) sum -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Useful impure features. *)
+(* ------------------------------------------------------------------------- *)
+
+val newInt : unit -> int
+
+val newInts : int -> int list
+
+val random : int -> int
+
+val uniform : unit -> real
+
+val coinFlip : unit -> bool
+
+val withRef : 'r ref * 'r -> ('a -> 'b) -> 'a -> 'b
+
+(* ------------------------------------------------------------------------- *)
+(* The environment. *)
+(* ------------------------------------------------------------------------- *)
+
+val host : unit -> string
+
+val time : unit -> string
+
+val date : unit -> string
+
+val readTextFile : {filename : string} -> string
+
+val writeTextFile : {filename : string, contents : string} -> unit
+
+(* ------------------------------------------------------------------------- *)
+(* Profiling and error reporting. *)
+(* ------------------------------------------------------------------------- *)
+
+val try : ('a -> 'b) -> 'a -> 'b
+
+val warn : string -> unit
+
+val die : string -> 'exit
+
+val timed : ('a -> 'b) -> 'a -> real * 'b
+
+val timedMany : ('a -> 'b) -> 'a -> real * 'b
+
+val executionTime : unit -> real (* Wall clock execution time *)
+
+end
+
+(**** Original file: Useful.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* ML UTILITY FUNCTIONS *)
+(* Copyright (c) 2001-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Useful :> Useful =
+struct
+
+infixr 0 oo ## |->
+
+(* ------------------------------------------------------------------------- *)
+(* 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 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 *)
+(* ------------------------------------------------------------------------- *)
+
+val tracePrint = ref print;
+
+val maxTraceLevel = ref 10;
+
+val traceLevel = ref 1;
+
+val traceAlign : {module : string, alignment : int -> int option} list ref
+ = ref [];
+
+local
+ fun query m l t =
+ case List.find (fn {module, ...} => module = m) (!traceAlign) of
+ NONE => l <= t
+ | SOME {alignment,...} =>
+ case alignment l of NONE => false | SOME l => l <= t;
+in
+ fun tracing {module,level} =
+ let
+ val ref T = maxTraceLevel
+ and ref t = traceLevel
+ in
+ 0 < t andalso (T <= t orelse query module level t)
+ end;
+end;
+
+fun trace message = !tracePrint message;
+
+(* ------------------------------------------------------------------------- *)
+(* Combinators *)
+(* ------------------------------------------------------------------------- *)
+
+fun C f x y = f y x;
+
+fun I x = x;
+
+fun K x y = x;
+
+fun S f g x = f x (g x);
+
+fun W f x = f x x;
+
+fun funpow 0 _ x = x
+ | funpow n f x = funpow (n - 1) f (f x);
+
+fun exp m =
+ let
+ fun f _ 0 z = z
+ | f x y z = f (m (x,x)) (y div 2) (if y mod 2 = 0 then z else m (z,x))
+ in
+ f
+ end;
+
+val equal = fn x => fn y => x = y;
+
+val notEqual = fn x => fn y => x <> y;
+
+(* ------------------------------------------------------------------------- *)
+(* Pairs *)
+(* ------------------------------------------------------------------------- *)
+
+fun fst (x,_) = x;
+
+fun snd (_,y) = y;
+
+fun pair x y = (x,y);
+
+fun swap (x,y) = (y,x);
+
+fun curry f x y = f (x,y);
+
+fun uncurry f (x,y) = f x y;
+
+val op## = fn (f,g) => fn (x,y) => (f x, g y);
+
+(* ------------------------------------------------------------------------- *)
+(* State transformers *)
+(* ------------------------------------------------------------------------- *)
+
+val unit : 'a -> 's -> 'a * 's = pair;
+
+fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f;
+
+fun mmap f (m : 's -> 'a * 's) = bind m (unit o f);
+
+fun mjoin (f : 's -> ('s -> 'a * 's) * 's) = bind f I;
+
+fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end;
+
+(* ------------------------------------------------------------------------- *)
+(* 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;
+
+(* ------------------------------------------------------------------------- *)
+(* Comparisons. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mapCompare f cmp (a,b) = cmp (f a, f b);
+
+fun revCompare cmp x_y =
+ case cmp x_y of LESS => GREATER | EQUAL => EQUAL | GREATER => LESS;
+
+fun prodCompare xCmp yCmp ((x1,y1),(x2,y2)) =
+ case xCmp (x1,x2) of
+ LESS => LESS
+ | EQUAL => yCmp (y1,y2)
+ | GREATER => GREATER;
+
+fun lexCompare cmp =
+ let
+ fun lex ([],[]) = EQUAL
+ | lex ([], _ :: _) = LESS
+ | lex (_ :: _, []) = GREATER
+ | lex (x :: xs, y :: ys) =
+ case cmp (x,y) of
+ LESS => LESS
+ | EQUAL => lex (xs,ys)
+ | GREATER => GREATER
+ in
+ lex
+ end;
+
+fun boolCompare (true,false) = LESS
+ | boolCompare (false,true) = GREATER
+ | boolCompare _ = EQUAL;
+
+(* ------------------------------------------------------------------------- *)
+(* Sorting and searching. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Finding the minimum and maximum element of a list, wrt some order. *)
+
+fun minimum cmp =
+ let
+ fun min (l,m,r) _ [] = (m, List.revAppend (l,r))
+ | min (best as (_,m,_)) l (x :: r) =
+ min (case cmp (x,m) of LESS => (l,x,r) | _ => best) (x :: l) r
+ in
+ fn [] => raise Empty
+ | h :: t => min ([],h,t) [h] t
+ end;
+
+fun maximum cmp = minimum (revCompare cmp);
+
+(* Merge (for the following merge-sort, but generally useful too). *)
+
+fun merge cmp =
+ let
+ fun mrg acc [] ys = List.revAppend (acc,ys)
+ | mrg acc xs [] = List.revAppend (acc,xs)
+ | mrg acc (xs as x :: xt) (ys as y :: yt) =
+ (case cmp (x,y) of
+ GREATER => mrg (y :: acc) xs yt
+ | _ => mrg (x :: acc) xt ys)
+ in
+ mrg []
+ end;
+
+(* Merge sort (stable). *)
+
+fun sort cmp =
+ let
+ fun findRuns acc r rs [] = rev (rev (r :: rs) :: acc)
+ | findRuns acc r rs (x :: xs) =
+ case cmp (r,x) of
+ GREATER => findRuns (rev (r :: rs) :: acc) x [] xs
+ | _ => findRuns acc x (r :: rs) xs
+
+ fun mergeAdj acc [] = rev acc
+ | mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
+ | mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
+
+ fun mergePairs [xs] = xs
+ | mergePairs l = mergePairs (mergeAdj [] l)
+ in
+ fn [] => []
+ | l as [_] => l
+ | h :: t => mergePairs (findRuns [] h [] t)
+ end;
+
+fun sortMap _ _ [] = []
+ | sortMap _ _ (l as [_]) = l
+ | sortMap f cmp xs =
+ let
+ fun ncmp ((m,_),(n,_)) = cmp (m,n)
+ val nxs = map (fn x => (f x, x)) xs
+ val nys = sort ncmp nxs
+ in
+ map snd nys
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Integers. *)
+(* ------------------------------------------------------------------------- *)
+
+fun interval m 0 = []
+ | interval m len = m :: interval (m + 1) (len - 1);
+
+fun divides _ 0 = true
+ | divides 0 _ = false
+ | divides a b = b mod (Int.abs a) = 0;
+
+local
+ fun hcf 0 n = n
+ | hcf 1 _ = 1
+ | hcf m n = hcf (n mod m) m;
+in
+ fun gcd m n =
+ let
+ val m = Int.abs m
+ and n = Int.abs n
+ in
+ if m < n then hcf m n else hcf n m
+ end;
+end;
+
+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 = ref (calcPrimes 10);
+in
+ fun primes n =
+ if length (!primesList) <= n then List.take (!primesList,n)
+ else
+ let
+ val l = calcPrimes n
+ val () = primesList := l
+ in
+ l
+ end;
+
+ fun primesUpTo n =
+ 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;
+
+(* ------------------------------------------------------------------------- *)
+(* Strings. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun len l = (length l, l)
+
+ val upper = len (explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
+
+ val lower = len (explode "abcdefghijklmnopqrstuvwxyz");
+
+ fun rotate (n,l) c k =
+ List.nth (l, (k + Option.valOf (index (equal c) l)) mod n);
+in
+ fun rot k c =
+ if Char.isLower c then rotate lower c k
+ else if Char.isUpper c then rotate upper c k
+ else c;
+end;
+
+fun charToInt #"0" = SOME 0
+ | charToInt #"1" = SOME 1
+ | charToInt #"2" = SOME 2
+ | charToInt #"3" = SOME 3
+ | charToInt #"4" = SOME 4
+ | charToInt #"5" = SOME 5
+ | charToInt #"6" = SOME 6
+ | charToInt #"7" = SOME 7
+ | charToInt #"8" = SOME 8
+ | charToInt #"9" = SOME 9
+ | charToInt _ = NONE;
+
+fun charFromInt 0 = SOME #"0"
+ | charFromInt 1 = SOME #"1"
+ | charFromInt 2 = SOME #"2"
+ | charFromInt 3 = SOME #"3"
+ | charFromInt 4 = SOME #"4"
+ | charFromInt 5 = SOME #"5"
+ | charFromInt 6 = SOME #"6"
+ | charFromInt 7 = SOME #"7"
+ | charFromInt 8 = SOME #"8"
+ | charFromInt 9 = SOME #"9"
+ | charFromInt _ = NONE;
+
+fun nChars x =
+ let
+ fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
+ in
+ fn n => implode (dup n [])
+ end;
+
+fun chomp s =
+ let
+ val n = size s
+ in
+ if n = 0 orelse String.sub (s, n - 1) <> #"\n" then s
+ else String.substring (s, 0, n - 1)
+ end;
+
+local
+ fun chop [] = []
+ | chop (l as (h :: t)) = if Char.isSpace h then chop t else l;
+in
+ 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;
+
+local
+ fun match [] l = SOME l
+ | match _ [] = NONE
+ | match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
+
+ fun stringify acc [] = acc
+ | stringify acc (h :: t) = stringify (implode h :: acc) t;
+in
+ fun split sep =
+ let
+ val pat = String.explode sep
+ fun div1 prev recent [] = stringify [] (rev recent :: prev)
+ | div1 prev recent (l as h :: t) =
+ case match pat l of
+ NONE => div1 prev (h :: recent) t
+ | SOME rest => div1 (rev recent :: prev) [] rest
+ in
+ fn s => div1 [] [] (explode s)
+ end;
+end;
+
+(***
+fun pluralize {singular,plural} = fn 1 => singular | _ => plural;
+***)
+
+fun mkPrefix p s = p ^ s;
+
+fun destPrefix p =
+ let
+ fun check s = String.isPrefix p s orelse raise Error "destPrefix"
+
+ val sizeP = size p
+ in
+ fn s => (check s; String.extract (s,sizeP,NONE))
+ end;
+
+fun isPrefix p = can (destPrefix p);
+
+(* ------------------------------------------------------------------------- *)
+(* Tables. *)
+(* ------------------------------------------------------------------------- *)
+
+type columnAlignment = {leftAlign : bool, padChar : char}
+
+fun alignColumn {leftAlign,padChar} column =
+ let
+ val (n,_) = maximum Int.compare (map size column)
+
+ fun pad entry row =
+ let
+ val padding = nChars padChar (n - size entry)
+ in
+ if leftAlign then entry ^ padding ^ row
+ else padding ^ entry ^ row
+ end
+ in
+ zipwith pad column
+ end;
+
+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));
+
+(* ------------------------------------------------------------------------- *)
+(* Reals. *)
+(* ------------------------------------------------------------------------- *)
+
+val realToString = Real.toString;
+
+fun percentToString x = Int.toString (Real.round (100.0 * x)) ^ "%";
+
+fun pos r = Real.max (r,0.0);
+
+local val ln2 = Math.ln 2.0 in fun log2 x = Math.ln x / ln2 end;
+
+(* ------------------------------------------------------------------------- *)
+(* Sums. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('a,'b) sum = Left of 'a | Right of 'b
+
+fun destLeft (Left l) = l
+ | destLeft _ = raise Error "destLeft";
+
+fun isLeft (Left _) = true
+ | isLeft (Right _) = false;
+
+fun destRight (Right r) = r
+ | destRight _ = raise Error "destRight";
+
+fun isRight (Left _) = false
+ | isRight (Right _) = true;
+
+(* ------------------------------------------------------------------------- *)
+(* Useful impure features. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val generator = ref 0
+in
+ fun newInt () =
+ let
+ val n = !generator
+ val () = generator := n + 1
+ in
+ n
+ end;
+
+ fun newInts 0 = []
+ | newInts k =
+ let
+ val n = !generator
+ val () = generator := n + k
+ in
+ interval n k
+ end;
+end;
+
+local
+ val gen = Random.newgenseed 1.0;
+in
+ fun random max = Random.range (0,max) gen;
+
+ fun uniform () = Random.random gen;
+
+ fun coinFlip () = Random.range (0,2) gen = 0;
+end;
+
+fun withRef (r,new) f x =
+ let
+ val old = !r
+ val () = r := new
+ val y = f x handle e => (r := old; raise e)
+ val () = r := old
+ in
+ y
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Environment. *)
+(* ------------------------------------------------------------------------- *)
+
+fun host () = Option.getOpt (OS.Process.getEnv "HOSTNAME", "unknown");
+
+fun time () = Date.fmt "%H:%M:%S" (Date.fromTimeLocal (Time.now ()));
+
+fun date () = Date.fmt "%d/%m/%Y" (Date.fromTimeLocal (Time.now ()));
+
+fun readTextFile {filename} =
+ let
+ open TextIO
+ val h = openIn filename
+ val contents = inputAll h
+ val () = closeIn h
+ in
+ contents
+ end;
+
+fun writeTextFile {filename,contents} =
+ let
+ open TextIO
+ val h = openOut filename
+ val () = output (h,contents)
+ val () = closeOut h
+ in
+ ()
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Profiling *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun err x s = TextIO.output (TextIO.stdErr, x ^ ": " ^ s ^ "\n");
+in
+ fun try f x = f x
+ handle e as Error _ => (err "try" (errorToString e); raise e)
+ | e as Bug _ => (err "try" (bugToString e); raise e)
+ | e => (err "try" "strange exception raised"; raise e);
+
+ val warn = err "WARNING";
+
+ fun die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure);
+end;
+
+fun timed f a =
+ let
+ val tmr = Timer.startCPUTimer ()
+ val res = f a
+ val {usr,sys,...} = Timer.checkCPUTimer tmr
+ in
+ (Time.toReal usr + Time.toReal sys, res)
+ end;
+
+local
+ val MIN = 1.0;
+
+ fun several n t f a =
+ let
+ val (t',res) = timed f a
+ val t = t + t'
+ val n = n + 1
+ in
+ if t > MIN then (t / Real.fromInt n, res) else several n t f a
+ end;
+in
+ fun timedMany f a = several 0 0.0 f a
+end;
+
+val executionTime =
+ let
+ val startTime = Time.toReal (Time.now ())
+ in
+ fn () => Time.toReal (Time.now ()) - startTime
+ end;
+
+end
+end;
+
+(**** Original file: Lazy.sig ****)
+
+(* ========================================================================= *)
+(* SUPPORT FOR LAZY EVALUATION *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Lazy =
+sig
+
+type 'a lazy
+
+val delay : (unit -> 'a) -> 'a lazy
+
+val force : 'a lazy -> 'a
+
+val memoize : (unit -> 'a) -> unit -> 'a
+
+end
+
+(**** Original file: Lazy.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* SUPPORT FOR LAZY EVALUATION *)
+(* Copyright (c) 2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Lazy :> Lazy =
+struct
+
+datatype 'a thunk =
+ Value of 'a
+ | Thunk of unit -> 'a;
+
+datatype 'a lazy = Lazy of 'a thunk ref;
+
+fun delay f = Lazy (ref (Thunk f));
+
+fun force (Lazy (ref (Value v))) = v
+ | force (Lazy (s as ref (Thunk f))) =
+ let
+ val v = f ()
+ val () = s := Value v
+ in
+ v
+ end;
+
+fun memoize f =
+ let
+ val t = delay f
+ in
+ fn () => force t
+ end;
+
+end
+end;
+
+(**** Original file: Ordered.sig ****)
+
+(* ========================================================================= *)
+(* ORDERED TYPES *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Ordered =
+sig
+
+type t
+
+val compare : t * t -> order
+
+(*
+ PROVIDES
+
+ !x : t. compare (x,x) = EQUAL
+
+ !x y : t. compare (x,y) = LESS <=> compare (y,x) = GREATER
+
+ !x y : t. compare (x,y) = EQUAL ==> compare (y,x) = EQUAL
+
+ !x y z : t. compare (x,y) = EQUAL ==> compare (x,z) = compare (y,z)
+
+ !x y z : t.
+ compare (x,y) = LESS andalso compare (y,z) = LESS ==>
+ compare (x,z) = LESS
+
+ !x y z : t.
+ compare (x,y) = GREATER andalso compare (y,z) = GREATER ==>
+ compare (x,z) = GREATER
+*)
+
+end
+
+(**** Original file: Ordered.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* ORDERED TYPES *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure IntOrdered =
+struct type t = int val compare = Int.compare end;
+
+structure StringOrdered =
+struct type t = string val compare = String.compare end;
+end;
+
+(**** Original file: Set.sig ****)
+
+(* ========================================================================= *)
+(* FINITE SETS *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Set =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Finite sets *)
+(* ------------------------------------------------------------------------- *)
+
+type 'elt set
+
+val comparison : 'elt set -> ('elt * 'elt -> order)
+
+val empty : ('elt * 'elt -> order) -> 'elt set
+
+val singleton : ('elt * 'elt -> order) -> 'elt -> 'elt set
+
+val null : 'elt set -> bool
+
+val size : 'elt set -> int
+
+val member : 'elt -> 'elt set -> bool
+
+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 *)
+
+val union : 'elt set -> 'elt set -> 'elt set
+
+val unionList : 'elt set list -> 'elt set
+
+val intersect : 'elt set -> 'elt set -> 'elt set
+
+val intersectList : 'elt set list -> 'elt set
+
+val difference : 'elt set -> 'elt set -> 'elt set
+
+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
+
+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 foldl : ('elt * 's -> 's) -> 's -> 'elt set -> 's
+
+val foldr : ('elt * 's -> 's) -> 's -> 'elt set -> 's
+
+val findl : ('elt -> bool) -> 'elt set -> 'elt option
+
+val findr : ('elt -> bool) -> 'elt set -> 'elt option
+
+val firstl : ('elt -> 'a option) -> 'elt set -> 'a option
+
+val firstr : ('elt -> 'a option) -> 'elt set -> 'a option
+
+val exists : ('elt -> bool) -> 'elt set -> bool
+
+val all : ('elt -> bool) -> 'elt set -> bool
+
+val map : ('elt -> 'a) -> 'elt set -> ('elt * 'a) list
+
+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
+
+val toString : 'elt set -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over sets *)
+(* ------------------------------------------------------------------------- *)
+
+type 'elt iterator
+
+val mkIterator : 'elt set -> 'elt iterator option
+
+val mkRevIterator : 'elt set -> 'elt iterator option
+
+val readIterator : 'elt iterator -> 'elt
+
+val advanceIterator : 'elt iterator -> 'elt iterator option
+
+end
+
+(**** Original file: RandomSet.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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 = Useful.random;
+
+(* ------------------------------------------------------------------------- *)
+(* Random search trees. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype 'a tree =
+ E
+ | T of
+ {size : int,
+ priority : real,
+ left : 'a tree,
+ key : 'a,
+ right : 'a tree};
+
+type 'a node =
+ {size : int,
+ priority : real,
+ left : 'a tree,
+ key : 'a,
+ right : 'a tree};
+
+datatype 'a set = Set of ('a * 'a -> order) * 'a tree;
+
+(* ------------------------------------------------------------------------- *)
+(* Random priorities. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val randomPriority =
+ let
+ val gen = Random.newgenseed 2.0
+ in
+ fn () => Random.random gen
+ end;
+
+ val priorityOrder = Real.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);
+
+(* add must be primitive to get hold of the comparison function *)
+
+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 "Set.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 "Set.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 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 union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FINITE SETS *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Set = RandomSet;
+end;
+
+(**** Original file: ElementSet.sig ****)
+
+(* ========================================================================= *)
+(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature ElementSet =
+sig
+
+type element
+
+(* ------------------------------------------------------------------------- *)
+(* Finite sets *)
+(* ------------------------------------------------------------------------- *)
+
+type set
+
+val empty : set
+
+val singleton : element -> set
+
+val null : set -> bool
+
+val size : set -> int
+
+val member : element -> set -> bool
+
+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 *)
+
+val union : set -> set -> set
+
+val unionList : set list -> set
+
+val intersect : set -> set -> set
+
+val intersectList : set list -> set
+
+val difference : set -> set -> set
+
+val symmetricDifference : set -> set -> set
+
+val disjoint : set -> set -> bool
+
+val subset : set -> set -> bool
+
+val equal : set -> set -> bool
+
+val filter : (element -> bool) -> set -> set
+
+val partition : (element -> bool) -> set -> set * set
+
+val count : (element -> bool) -> set -> int
+
+val foldl : (element * 's -> 's) -> 's -> set -> 's
+
+val foldr : (element * 's -> 's) -> 's -> set -> 's
+
+val findl : (element -> bool) -> set -> element option
+
+val findr : (element -> bool) -> set -> element option
+
+val firstl : (element -> 'a option) -> set -> 'a option
+
+val firstr : (element -> 'a option) -> set -> 'a option
+
+val exists : (element -> bool) -> set -> bool
+
+val all : (element -> bool) -> set -> bool
+
+val map : (element -> 'a) -> set -> (element * 'a) list
+
+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
+
+val toString : set -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Iterators over sets *)
+(* ------------------------------------------------------------------------- *)
+
+type iterator
+
+val mkIterator : set -> iterator option
+
+val mkRevIterator : set -> iterator option
+
+val readIterator : iterator -> element
+
+val advanceIterator : iterator -> iterator option
+
+end
+
+(**** Original file: ElementSet.sml ****)
+
+(* ========================================================================= *)
+(* FINITE SETS WITH A FIXED ELEMENT TYPE *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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;
+
+(* ------------------------------------------------------------------------- *)
+(* 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;
+
+structure IntSet =
+ElementSet (IntOrdered);
+
+structure StringSet =
+ElementSet (StringOrdered);
+
+ end;
+
+(**** Original file: Map.sig ****)
+
+(* ========================================================================= *)
+(* FINITE MAPS *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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 union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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 = Useful.random;
+
+(* ------------------------------------------------------------------------- *)
+(* Random search trees. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype ('a,'b) tree =
+ E
+ | T of
+ {size : int,
+ priority : real,
+ left : ('a,'b) tree,
+ key : 'a,
+ value : 'b,
+ right : ('a,'b) tree};
+
+type ('a,'b) node =
+ {size : int,
+ priority : real,
+ 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 =
+ let
+ val gen = Random.newgenseed 2.0
+ in
+ fn () => Random.random gen
+ end;
+
+ val priorityOrder = Real.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 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 union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FINITE MAPS *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Map = RandomMap;
+end;
+
+(**** Original file: KeyMap.sig ****)
+
+(* ========================================================================= *)
+(* FINITE MAPS WITH A FIXED KEY TYPE *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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 GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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;
+
+(**** Original file: Sharing.sig ****)
+
+(* ========================================================================= *)
+(* PRESERVING SHARING OF ML VALUES *)
+(* Copyright (c) 2005-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Sharing =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Pointer equality. *)
+(* ------------------------------------------------------------------------- *)
+
+val pointerEqual : 'a * 'a -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* List operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val map : ('a -> 'a) -> 'a list -> 'a list
+
+val updateNth : int * 'a -> 'a list -> 'a list
+
+val setify : ''a list -> ''a list
+
+(* ------------------------------------------------------------------------- *)
+(* Function caching. *)
+(* ------------------------------------------------------------------------- *)
+
+val cache : ('a * 'a -> order) -> ('a -> 'b) -> 'a -> 'b
+
+(* ------------------------------------------------------------------------- *)
+(* Hash consing. *)
+(* ------------------------------------------------------------------------- *)
+
+val hashCons : ('a * 'a -> order) -> 'a -> 'a
+
+end
+
+(**** Original file: Sharing.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* PRESERVING SHARING OF ML VALUES *)
+(* Copyright (c) 2005-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Sharing :> Sharing =
+struct
+
+infix ==
+
+(* ------------------------------------------------------------------------- *)
+(* Pointer equality. *)
+(* ------------------------------------------------------------------------- *)
+
+val pointerEqual = Portable.pointerEqual;
+
+val op== = pointerEqual;
+
+(* ------------------------------------------------------------------------- *)
+(* List operations. *)
+(* ------------------------------------------------------------------------- *)
+
+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 updateNth (n,x) l =
+ let
+ val (a,b) = Useful.revDivide l n
+ in
+ case b of
+ [] => raise Subscript
+ | h :: t => if x == h then l else List.revAppend (a, x :: t)
+ end;
+
+fun setify l =
+ let
+ val l' = Useful.setify l
+ in
+ if length l' = length l then l else l'
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Function caching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun cache cmp f =
+ let
+ val cache = ref (Map.new cmp)
+ in
+ fn a =>
+ case Map.peek (!cache) a of
+ SOME b => b
+ | NONE =>
+ let
+ val b = f a
+ val () = cache := Map.insert (!cache) (a,b)
+ in
+ b
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Hash consing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun hashCons cmp = cache cmp Useful.I;
+
+end
+end;
+
+(**** Original file: Stream.sig ****)
+
+(* ========================================================================= *)
+(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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 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 union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+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 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 GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Heap =
+sig
+
+type 'a heap
+
+val new : ('a * 'a -> order) -> 'a heap
+
+val add : 'a heap -> 'a -> 'a heap
+
+val null : 'a heap -> bool
+
+val top : 'a heap -> 'a (* raises Empty *)
+
+val remove : 'a heap -> 'a * 'a heap (* raises Empty *)
+
+val size : 'a heap -> int
+
+val app : ('a -> unit) -> 'a heap -> unit
+
+val toList : 'a heap -> 'a list
+
+val toStream : 'a heap -> 'a Metis.Stream.stream
+
+val toString : 'a heap -> string
+
+end
+
+(**** Original file: Heap.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* A HEAP DATATYPE FOR ML *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Heap :> Heap =
+struct
+
+(* Leftist heaps as in Purely Functional Data Structures, by Chris Okasaki *)
+
+datatype 'a node = E | T of int * 'a * 'a node * 'a node;
+
+datatype 'a heap = Heap of ('a * 'a -> order) * int * 'a node;
+
+fun rank E = 0
+ | rank (T (r,_,_,_)) = r;
+
+fun makeT (x,a,b) =
+ if rank a >= rank b then T (rank b + 1, x, a, b) else T (rank a + 1, x, b, a);
+
+fun merge cmp =
+ let
+ fun mrg (h,E) = h
+ | mrg (E,h) = h
+ | mrg (h1 as T (_,x,a1,b1), h2 as T (_,y,a2,b2)) =
+ case cmp (x,y) of
+ GREATER => makeT (y, a2, mrg (h1,b2))
+ | _ => makeT (x, a1, mrg (b1,h2))
+ in
+ mrg
+ end;
+
+fun new cmp = Heap (cmp,0,E);
+
+fun add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (T (1,x,E,E), a));
+
+fun size (Heap (_, n, _)) = n;
+
+fun null h = size h = 0;
+
+fun top (Heap (_,_,E)) = raise Empty
+ | top (Heap (_, _, T (_,x,_,_))) = x;
+
+fun remove (Heap (_,_,E)) = raise Empty
+ | remove (Heap (f, n, T (_,x,a,b))) = (x, Heap (f, n - 1, merge f (a,b)));
+
+fun app f =
+ let
+ fun ap [] = ()
+ | ap (E :: rest) = ap rest
+ | ap (T (_,d,a,b) :: rest) = (f d; ap (a :: b :: rest))
+ in
+ fn Heap (_,_,a) => ap [a]
+ end;
+
+fun toList h =
+ if null h then []
+ else
+ let
+ val (x,h) = remove h
+ in
+ x :: toList h
+ end;
+
+fun toStream h =
+ if null h then Stream.NIL
+ else
+ let
+ val (x,h) = remove h
+ in
+ Stream.CONS (x, fn () => toStream h)
+ end;
+
+fun toString h =
+ "Heap[" ^ (if null h then "" else Int.toString (size h)) ^ "]";
+
+end
+end;
+
+(**** Original file: Parser.sig ****)
+
+(* ========================================================================= *)
+(* PARSING AND PRETTY PRINTING *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Parser =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing for built-in types *)
+(* ------------------------------------------------------------------------- *)
+
+type ppstream = Metis.PP.ppstream
+
+datatype breakStyle = Consistent | Inconsistent
+
+type 'a pp = ppstream -> 'a -> unit
+
+val lineLength : int 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
+
+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 ppChar : char pp
+
+val ppString : string pp
+
+val ppUnit : unit pp
+
+val ppBool : bool pp
+
+val ppInt : int pp
+
+val ppReal : real pp
+
+val ppOrder : order pp
+
+val ppList : 'a pp -> 'a list 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:
+ infixr 9 >>++
+ infixr 8 ++
+ infixr 7 >>
+ infixr 6 ||
+*)
+
+exception NoParse
+
+val error : 'a -> 'b * 'a
+
+val ++ : ('a -> 'b * 'a) * ('a -> 'c * 'a) -> 'a -> ('b * 'c) * 'a
+
+val >> : ('a -> 'b * 'a) * ('b -> 'c) -> 'a -> 'c * 'a
+
+val >>++ : ('a -> 'b * 'a) * ('b -> 'a -> 'c * 'a) -> 'a -> 'c * 'a
+
+val || : ('a -> 'b * 'a) * ('a -> 'b * 'a) -> 'a -> 'b * 'a
+
+val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a
+
+val mmany : ('s -> 'a -> 's * 'a) -> 's -> 'a -> 's * 'a
+
+val many : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+
+val atLeastOne : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
+
+val nothing : 'a -> unit * 'a
+
+val optional : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
+
+(* Stream based parsers *)
+
+type ('a,'b) parser = 'a Metis.Stream.stream -> 'b * 'a Metis.Stream.stream
+
+val everything : ('a, 'b list) parser -> 'a Metis.Stream.stream -> 'b Metis.Stream.stream
+
+val maybe : ('a -> 'b option) -> ('a,'b) parser
+
+val finished : ('a,unit) parser
+
+val some : ('a -> bool) -> ('a,'a) parser
+
+val any : ('a,'a) parser
+
+val exact : ''a -> (''a,''a) parser
+
+(* ------------------------------------------------------------------------- *)
+(* Infix operators *)
+(* ------------------------------------------------------------------------- *)
+
+type infixities = {token : string, precedence : int, leftAssoc : bool} list
+
+val infixTokens : infixities -> string list
+
+val parseInfixes :
+ infixities -> (string * 'a * 'a -> 'a) -> (string,'a) parser ->
+ (string,'a) parser
+
+val ppInfixes :
+ infixities -> ('a -> (string * 'a * 'a) option) -> ('a * bool) pp ->
+ ('a * bool) pp
+
+(* ------------------------------------------------------------------------- *)
+(* Quotations *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a quotation = 'a Metis.frag list
+
+val parseQuotation : ('a -> string) -> (string -> 'b) -> 'a quotation -> 'b
+
+end
+
+(**** Original file: Parser.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* PARSER COMBINATORS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Parser :> Parser =
+struct
+
+infixr 9 >>++
+infixr 8 ++
+infixr 7 >>
+infixr 6 ||
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+exception Bug = Useful.Bug;
+
+val trace = Useful.trace
+and equal = Useful.equal
+and I = Useful.I
+and K = Useful.K
+and C = Useful.C
+and fst = Useful.fst
+and snd = Useful.snd
+and pair = Useful.pair
+and curry = Useful.curry
+and funpow = Useful.funpow
+and mem = Useful.mem
+and sortMap = Useful.sortMap;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty printing for built-in types *)
+(* ------------------------------------------------------------------------- *)
+
+type ppstream = PP.ppstream
+
+datatype breakStyle = Consistent | Inconsistent
+
+type 'a pp = PP.ppstream -> 'a -> unit;
+
+val lineLength = ref 75;
+
+fun beginBlock pp Consistent = PP.begin_block pp PP.CONSISTENT
+ | beginBlock pp Inconsistent = PP.begin_block pp PP.INCONSISTENT;
+
+val endBlock = PP.end_block
+and addString = PP.add_string
+and addBreak = PP.add_break
+and addNewline = PP.add_newline;
+
+fun ppMap f ppA (ppstrm : PP.ppstream) x : unit = ppA ppstrm (f x);
+
+fun ppBracket l r ppA pp a =
+ let
+ val ln = size l
+ in
+ beginBlock pp Inconsistent ln;
+ if ln = 0 then () else addString pp l;
+ ppA pp a;
+ if r = "" then () else addString pp r;
+ endBlock pp
+ end;
+
+fun ppSequence sep ppA pp =
+ let
+ fun ppX x = (addString pp sep; addBreak pp (1,0); ppA pp x)
+ in
+ fn [] => ()
+ | h :: t =>
+ (beginBlock pp Inconsistent 0;
+ ppA pp h;
+ app ppX t;
+ endBlock pp)
+ end;
+
+fun ppBinop s ppA ppB pp (a,b) =
+ (beginBlock pp Inconsistent 0;
+ ppA pp a;
+ if s = "" then () else addString pp s;
+ addBreak pp (1,0);
+ ppB pp b;
+ endBlock pp);
+
+fun ppTrinop ab bc ppA ppB ppC pp (a,b,c) =
+ (beginBlock pp Inconsistent 0;
+ ppA pp a;
+ if ab = "" then () else addString pp ab;
+ addBreak pp (1,0);
+ ppB pp b;
+ if bc = "" then () else addString pp bc;
+ addBreak pp (1,0);
+ ppC pp c;
+ endBlock pp);
+
+(* Pretty-printers for common types *)
+
+fun ppString pp s =
+ (beginBlock pp Inconsistent 0;
+ addString pp s;
+ endBlock pp);
+
+val ppUnit = ppMap (fn () => "()") ppString;
+
+val ppChar = ppMap str ppString;
+
+val ppBool = ppMap (fn true => "true" | false => "false") ppString;
+
+val ppInt = ppMap Int.toString ppString;
+
+val ppReal = ppMap Real.toString ppString;
+
+val ppOrder =
+ let
+ fun f LESS = "Less"
+ | f EQUAL = "Equal"
+ | f GREATER = "Greater"
+ in
+ ppMap f ppString
+ end;
+
+fun ppList ppA = ppBracket "[" "]" (ppSequence "," ppA);
+
+fun ppOption _ pp NONE = ppString pp "-"
+ | ppOption ppA pp (SOME a) = ppA pp a;
+
+fun ppPair ppA ppB = ppBracket "(" ")" (ppBinop "," ppA ppB);
+
+fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppTrinop "," "," ppA ppB ppC);
+
+fun toString ppA a = PP.pp_to_string (!lineLength) ppA a;
+
+fun fromString toS = ppMap toS ppString;
+
+fun ppTrace ppX nameX x =
+ trace (toString (ppBinop " =" ppString ppX) (nameX,x) ^ "\n");
+
+(* ------------------------------------------------------------------------- *)
+(* Generic. *)
+(* ------------------------------------------------------------------------- *)
+
+exception NoParse;
+
+val error : 'a -> 'b * 'a = fn _ => raise NoParse;
+
+fun op ++ (parser1,parser2) input =
+ let
+ val (result1,input) = parser1 input
+ val (result2,input) = parser2 input
+ in
+ ((result1,result2),input)
+ end;
+
+fun op >> (parser : 'a -> 'b * 'a, treatment) input =
+ let
+ val (result,input) = parser input
+ in
+ (treatment result, input)
+ end;
+
+fun op >>++ (parser,treatment) input =
+ let
+ val (result,input) = parser input
+ in
+ treatment result input
+ end;
+
+fun op || (parser1,parser2) input =
+ parser1 input handle NoParse => parser2 input;
+
+fun first [] _ = raise NoParse
+ | first (parser :: parsers) input = (parser || first parsers) input;
+
+fun mmany parser state input =
+ let
+ val (state,input) = parser state input
+ in
+ mmany parser state input
+ end
+ handle NoParse => (state,input);
+
+fun many parser =
+ let
+ fun sparser l = parser >> (fn x => x :: l)
+ in
+ mmany sparser [] >> rev
+ end;
+
+fun atLeastOne p = (p ++ many p) >> op::;
+
+fun nothing input = ((),input);
+
+fun optional p = (p >> SOME) || (nothing >> K NONE);
+
+(* ------------------------------------------------------------------------- *)
+(* Stream-based. *)
+(* ------------------------------------------------------------------------- *)
+
+type ('a,'b) parser = 'a Stream.stream -> 'b * 'a Stream.stream
+
+fun everything parser =
+ let
+ fun f input =
+ let
+ val (result,input) = parser input
+ in
+ Stream.append (Stream.fromList result) (fn () => f input)
+ end
+ handle NoParse =>
+ if Stream.null input then Stream.NIL else raise NoParse
+ in
+ f
+ end;
+
+fun maybe p Stream.NIL = raise NoParse
+ | maybe p (Stream.CONS (h,t)) =
+ case p h of SOME r => (r, t ()) | NONE => raise NoParse;
+
+fun finished Stream.NIL = ((), Stream.NIL)
+ | finished (Stream.CONS _) = raise NoParse;
+
+fun some p = maybe (fn x => if p x then SOME x else NONE);
+
+fun any input = some (K true) input;
+
+fun exact tok = some (fn item => item = tok);
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing for infix operators. *)
+(* ------------------------------------------------------------------------- *)
+
+type infixities = {token : string, precedence : int, leftAssoc : bool} list;
+
+local
+ fun unflatten ({token,precedence,leftAssoc}, ([],_)) =
+ ([(leftAssoc, [token])], precedence)
+ | unflatten ({token,precedence,leftAssoc}, ((a,l) :: dealt, p)) =
+ if p = precedence then
+ let
+ val _ = leftAssoc = a orelse
+ raise Bug "infix parser/printer: mixed assocs"
+ in
+ ((a, token :: l) :: dealt, p)
+ end
+ else
+ ((leftAssoc,[token]) :: (a,l) :: dealt, precedence);
+in
+ fun layerOps infixes =
+ let
+ val infixes = sortMap #precedence Int.compare infixes
+ val (parsers,_) = foldl unflatten ([],0) infixes
+ in
+ parsers
+ end;
+end;
+
+local
+ fun chop (#" " :: chs) = let val (n,l) = chop chs in (n + 1, l) end
+ | chop chs = (0,chs);
+
+ fun nspaces n = funpow n (curry op^ " ") "";
+
+ fun spacify tok =
+ let
+ val chs = explode tok
+ val (r,chs) = chop (rev chs)
+ val (l,chs) = chop (rev chs)
+ in
+ ((l,r), implode chs)
+ end;
+
+ fun lrspaces (l,r) =
+ (if l = 0 then K () else C addString (nspaces l),
+ if r = 0 then K () else C addBreak (r, 0));
+in
+ fun opSpaces s = let val (l_r,s) = spacify s in (lrspaces l_r, s) end;
+
+ val opClean = snd o spacify;
+end;
+
+val infixTokens : infixities -> string list =
+ List.map (fn {token,...} => opClean token);
+
+fun parseGenInfix update sof toks parse inp =
+ let
+ val (e, rest) = parse inp
+
+ val continue =
+ case rest of
+ Stream.NIL => NONE
+ | Stream.CONS (h, t) => if mem h toks then SOME (h, t) else NONE
+ in
+ case continue of
+ NONE => (sof e, rest)
+ | SOME (h,t) => parseGenInfix update (update sof h e) toks parse (t ())
+ end;
+
+fun parseLeftInfix toks con =
+ parseGenInfix (fn f => fn t => fn a => fn b => con (t, f a, b)) I toks;
+
+fun parseRightInfix toks con =
+ parseGenInfix (fn f => fn t => fn a => fn b => f (con (t, a, b))) I toks;
+
+fun parseInfixes ops =
+ let
+ fun layeredOp (x,y) = (x, List.map opClean y)
+
+ val layeredOps = List.map layeredOp (layerOps ops)
+
+ fun iparser (a,t) = (if a then parseLeftInfix else parseRightInfix) t
+
+ val iparsers = List.map iparser layeredOps
+ in
+ fn con => fn subparser => foldl (fn (p,sp) => p con sp) subparser iparsers
+ end;
+
+fun ppGenInfix left toks =
+ let
+ val spc = List.map opSpaces toks
+ in
+ fn dest => fn ppSub =>
+ let
+ fun dest' tm =
+ case dest tm of
+ NONE => NONE
+ | SOME (t, a, b) =>
+ Option.map (pair (a,b)) (List.find (equal t o snd) spc)
+
+ open PP
+
+ fun ppGo pp (tmr as (tm,r)) =
+ case dest' tm of
+ NONE => ppSub pp tmr
+ | SOME ((a,b),((lspc,rspc),tok)) =>
+ ((if left then ppGo else ppSub) pp (a,true);
+ lspc pp; addString pp tok; rspc pp;
+ (if left then ppSub else ppGo) pp (b,r))
+ in
+ fn pp => fn tmr as (tm,_) =>
+ case dest' tm of
+ NONE => ppSub pp tmr
+ | SOME _ => (beginBlock pp Inconsistent 0; ppGo pp tmr; endBlock pp)
+ end
+ end;
+
+fun ppLeftInfix toks = ppGenInfix true toks;
+
+fun ppRightInfix toks = ppGenInfix false toks;
+
+fun ppInfixes ops =
+ let
+ val layeredOps = layerOps ops
+
+ val toks = List.concat (List.map (List.map opClean o snd) layeredOps)
+
+ fun iprinter (a,t) = (if a then ppLeftInfix else ppRightInfix) t
+
+ val iprinters = List.map iprinter 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,_,_) => mem x toks | _ => false
+
+ open PP
+
+ fun subpr pp (tmr as (tm,_)) =
+ if isOp tm then
+ (beginBlock pp Inconsistent 1; addString pp "(";
+ printer subpr pp (tm, false); addString pp ")"; endBlock pp)
+ else ppSub pp tmr
+ in
+ fn pp => fn tmr =>
+ (beginBlock pp Inconsistent 0; printer subpr pp tmr; endBlock pp)
+ end
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Quotations *)
+(* ------------------------------------------------------------------------- *)
+
+type 'a quotation = 'a frag list;
+
+fun parseQuotation printer parser quote =
+ let
+ fun expand (QUOTE q, s) = s ^ q
+ | expand (ANTIQUOTE a, s) = s ^ printer a
+
+ val string = foldl expand "" quote
+ in
+ parser string
+ end;
+
+end
+end;
+
+(**** Original file: Options.sig ****)
+
+(* ========================================================================= *)
+(* PROCESSING COMMAND LINE OPTIONS *)
+(* Copyright (c) 2003-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Options =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* Option processors take an option with its associated arguments. *)
+(* ------------------------------------------------------------------------- *)
+
+type proc = string * string list -> unit
+
+type ('a,'x) mkProc = ('x -> proc) -> ('a -> 'x) -> proc
+
+(* ------------------------------------------------------------------------- *)
+(* One command line option: names, arguments, description and a processor. *)
+(* ------------------------------------------------------------------------- *)
+
+type opt =
+ {switches : string list, arguments : string list,
+ description : string, processor : proc}
+
+(* ------------------------------------------------------------------------- *)
+(* Option processors may raise an OptionExit exception. *)
+(* ------------------------------------------------------------------------- *)
+
+type optionExit = {message : string option, usage : bool, success : bool}
+
+exception OptionExit of optionExit
+
+(* ------------------------------------------------------------------------- *)
+(* Constructing option processors. *)
+(* ------------------------------------------------------------------------- *)
+
+val beginOpt : (string,'x) mkProc
+
+val endOpt : unit -> proc
+
+val stringOpt : (string,'x) mkProc
+
+val intOpt : int option * int option -> (int,'x) mkProc
+
+val realOpt : real option * real option -> (real,'x) mkProc
+
+val enumOpt : string list -> (string,'x) mkProc
+
+val optionOpt : string * ('a,'x) mkProc -> ('a option,'x) mkProc
+
+(* ------------------------------------------------------------------------- *)
+(* Basic options useful for all programs. *)
+(* ------------------------------------------------------------------------- *)
+
+val basicOptions : opt list
+
+(* ------------------------------------------------------------------------- *)
+(* All the command line options of a program. *)
+(* ------------------------------------------------------------------------- *)
+
+type allOptions =
+ {name : string, version : string, header : string,
+ footer : string, options : opt list}
+
+(* ------------------------------------------------------------------------- *)
+(* Usage information. *)
+(* ------------------------------------------------------------------------- *)
+
+val versionInformation : allOptions -> string
+
+val usageInformation : allOptions -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Exit the program gracefully. *)
+(* ------------------------------------------------------------------------- *)
+
+val exit : allOptions -> optionExit -> 'exit
+
+val succeed : allOptions -> 'exit
+
+val fail : allOptions -> string -> 'exit
+
+val usage : allOptions -> string -> 'exit
+
+val version : allOptions -> 'exit
+
+(* ------------------------------------------------------------------------- *)
+(* Process the command line options passed to the program. *)
+(* ------------------------------------------------------------------------- *)
+
+val processOptions : allOptions -> string list -> string list * string list
+
+end
+
+(**** Original file: Options.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* PROCESSING COMMAND LINE OPTIONS *)
+(* Copyright (c) 2003-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Options :> Options =
+struct
+
+infix ##
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* One command line option: names, arguments, description and a processor *)
+(* ------------------------------------------------------------------------- *)
+
+type proc = string * string list -> unit;
+
+type ('a,'x) mkProc = ('x -> proc) -> ('a -> 'x) -> proc;
+
+type opt = {switches : string list, arguments : string list,
+ description : string, processor : proc};
+
+(* ------------------------------------------------------------------------- *)
+(* Option processors may raise an OptionExit exception *)
+(* ------------------------------------------------------------------------- *)
+
+type optionExit = {message : string option, usage : bool, success : bool};
+
+exception OptionExit of optionExit;
+
+(* ------------------------------------------------------------------------- *)
+(* Wrappers for option processors *)
+(* ------------------------------------------------------------------------- *)
+
+fun beginOpt f p (s : string, l : string list) : unit = f (p s) (s,l);
+
+fun endOpt () (_ : string, [] : string list) = ()
+ | endOpt _ (_, _ :: _) = raise Bug "endOpt";
+
+fun stringOpt _ _ (_ : string, []) = raise Bug "stringOpt"
+ | stringOpt f p (s, (h : string) :: t) : unit = f (p h) (s,t);
+
+local
+ fun range NONE NONE = "Z"
+ | range (SOME i) NONE = "{n IN Z | " ^ Int.toString i ^ " <= n}"
+ | range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
+ | range (SOME i) (SOME j) =
+ "{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}";
+ fun oLeq (SOME x) (SOME y) = x <= y | oLeq _ _ = true;
+ fun argToInt arg omin omax x =
+ (case Int.fromString x of
+ SOME i =>
+ if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else
+ raise OptionExit
+ {success = false, usage = false, message =
+ SOME (arg ^ " option needs an integer argument in the range "
+ ^ range omin omax ^ " (not " ^ x ^ ")")}
+ | NONE =>
+ raise OptionExit
+ {success = false, usage = false, message =
+ SOME (arg ^ " option needs an integer argument (not \"" ^ x ^ "\")")})
+ handle Overflow =>
+ raise OptionExit
+ {success = false, usage = false, message =
+ SOME (arg ^ " option suffered integer overflow on argument " ^ x)};
+in
+ fun intOpt _ _ _ (_,[]) = raise Bug "intOpt"
+ | intOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit =
+ f (p (argToInt s omin omax h)) (s,t);
+end;
+
+local
+ fun range NONE NONE = "R"
+ | range (SOME i) NONE = "{n IN R | " ^ Real.toString i ^ " <= n}"
+ | range NONE (SOME j) = "{n IN R | n <= " ^ Real.toString j ^ "}"
+ | range (SOME i) (SOME j) =
+ "{n IN R | " ^ Real.toString i ^ " <= n <= " ^ Real.toString j ^ "}";
+ fun oLeq (SOME (x:real)) (SOME y) = x <= y | oLeq _ _ = true;
+ fun argToReal arg omin omax x =
+ (case Real.fromString x of
+ SOME i =>
+ if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else
+ raise OptionExit
+ {success = false, usage = false, message =
+ SOME (arg ^ " option needs an real argument in the range "
+ ^ range omin omax ^ " (not " ^ x ^ ")")}
+ | NONE =>
+ raise OptionExit
+ {success = false, usage = false, message =
+ SOME (arg ^ " option needs an real argument (not \"" ^ x ^ "\")")})
+in
+ fun realOpt _ _ _ (_,[]) = raise Bug "realOpt"
+ | realOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit =
+ f (p (argToReal s omin omax h)) (s,t);
+end;
+
+fun enumOpt _ _ _ (_,[]) = raise Bug "enumOpt"
+ | enumOpt (choices : string list) f p (s : string, h :: t) : unit =
+ if mem h choices then f (p h) (s,t) else
+ raise OptionExit
+ {success = false, usage = false,
+ message = SOME ("follow parameter " ^ s ^ " with one of {" ^
+ join "," choices ^ "}, not \"" ^ h ^ "\"")};
+
+fun optionOpt _ _ _ (_,[]) = raise Bug "optionOpt"
+ | optionOpt (x : string, p) f q (s : string, l as h :: t) : unit =
+ if h = x then f (q NONE) (s,t) else p f (q o SOME) (s,l);
+
+(* ------------------------------------------------------------------------- *)
+(* Basic options useful for all programs *)
+(* ------------------------------------------------------------------------- *)
+
+val basicOptions : opt list =
+ [{switches = ["--"], arguments = [],
+ description = "no more options",
+ processor = fn _ => raise Fail "basicOptions: --"},
+ {switches = ["--verbose"], arguments = ["0..10"],
+ description = "the degree of verbosity",
+ processor = intOpt (SOME 0, SOME 10) endOpt (fn i => traceLevel := i)},
+ {switches = ["--secret"], arguments = [],
+ description = "process then hide the next option",
+ processor = fn _ => raise Fail "basicOptions: --secret"},
+ {switches = ["-?","-h","--help"], arguments = [],
+ description = "display all options and exit",
+ processor = fn _ => raise OptionExit
+ {message = SOME "displaying all options", usage = true, success = true}},
+ {switches = ["-v", "--version"], arguments = [],
+ description = "display version information",
+ processor = fn _ => raise Fail "basicOptions: -v, --version"}];
+
+(* ------------------------------------------------------------------------- *)
+(* All the command line options of a program *)
+(* ------------------------------------------------------------------------- *)
+
+type allOptions = {name : string, version : string, header : string,
+ footer : string, options : opt list};
+
+(* ------------------------------------------------------------------------- *)
+(* Usage information *)
+(* ------------------------------------------------------------------------- *)
+
+fun versionInformation ({version, ...} : allOptions) = version;
+
+fun usageInformation ({name,version,header,footer,options} : allOptions) =
+ let
+ fun filt ["--verbose"] = false
+ | filt ["--secret"] = false
+ | filt _ = true
+
+ fun listOpts {switches = n, arguments = r, description = s,
+ processor = _} =
+ let
+ fun indent (s, "" :: l) = indent (s ^ " ", l) | indent x = x
+ val (res,n) = indent (" ",n)
+ val res = res ^ join ", " n
+ val res = foldl (fn (x,y) => y ^ " " ^ x) res r
+ in
+ [res ^ " ...", " " ^ s]
+ end
+
+ val options = List.filter (filt o #switches) options
+
+ val alignment =
+ [{leftAlign = true, padChar = #"."},
+ {leftAlign = true, padChar = #" "}]
+
+ val table = alignTable alignment (map listOpts options)
+ in
+ header ^ join "\n" table ^ "\n" ^ footer
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Exit the program gracefully *)
+(* ------------------------------------------------------------------------- *)
+
+fun exit (allopts : allOptions) (optexit : optionExit) =
+ let
+ val {name, options, ...} = allopts
+ val {message, usage, success} = optexit
+ fun err s = TextIO.output (TextIO.stdErr, s)
+ in
+ case message of NONE => () | SOME m => err (name ^ ": " ^ m ^ "\n");
+ if usage then err (usageInformation allopts) else ();
+ OS.Process.exit (if success then OS.Process.success else OS.Process.failure)
+ end;
+
+fun succeed allopts =
+ exit allopts {message = NONE, usage = false, success = true};
+
+fun fail allopts mesg =
+ exit allopts {message = SOME mesg, usage = false, success = false};
+
+fun usage allopts mesg =
+ exit allopts {message = SOME mesg, usage = true, success = false};
+
+fun version allopts =
+ (print (versionInformation allopts);
+ exit allopts {message = NONE, usage = false, success = true});
+
+(* ------------------------------------------------------------------------- *)
+(* Process the command line options passed to the program *)
+(* ------------------------------------------------------------------------- *)
+
+fun processOptions (allopts : allOptions) =
+ let
+ fun findOption x =
+ case List.find (fn {switches = n, ...} => mem x n) (#options allopts) of
+ NONE => raise OptionExit
+ {message = SOME ("unknown switch \"" ^ x ^ "\""),
+ usage = true, success = false}
+ | SOME {arguments = r, processor = f, ...} => (r,f)
+
+ fun getArgs x r xs =
+ let
+ fun f 1 = "a following argument"
+ | f m = Int.toString m ^ " following arguments"
+ val m = length r
+ val () =
+ if m <= length xs then () else
+ raise OptionExit
+ {usage = false, success = false, message = SOME
+ (x ^ " option needs " ^ f m ^ ": " ^ join " " r)}
+ in
+ divide xs m
+ end
+
+ fun process [] = ([], [])
+ | process ("--" :: xs) = ([("--",[])], xs)
+ | process ("--secret" :: xs) = (tl ## I) (process xs)
+ | process ("-v" :: _) = version allopts
+ | process ("--version" :: _) = version allopts
+ | process (x :: xs) =
+ if x = "" orelse x = "-" orelse hd (explode x) <> #"-" then ([], x :: xs)
+ else
+ let
+ val (r,f) = findOption x
+ val (ys,xs) = getArgs x r xs
+ val () = f (x,ys)
+ in
+ (cons (x,ys) ## I) (process xs)
+ end
+ in
+ fn l =>
+ let
+ val (a,b) = process l
+ val a = foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (rev a)
+ in
+ (a,b)
+ end
+ handle OptionExit x => exit allopts x
+ end;
+
+end
+end;
+
+(**** Original file: Name.sig ****)
+
+(* ========================================================================= *)
+(* NAMES *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Name =
+sig
+
+type name = string
+
+val compare : name * name -> order
+
+val pp : name Metis.Parser.pp
+
+end
+
+(**** Original file: Name.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* NAMES *)
+(* Copyright (c) 2004-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Name :> Name =
+struct
+
+type name = string;
+
+val compare = String.compare;
+
+val pp = Parser.ppString;
+
+end
+
+structure NameOrdered =
+struct type t = Name.name val compare = Name.compare end
+
+structure NameSet =
+struct
+
+ local
+ structure S = ElementSet (NameOrdered);
+ in
+ open S;
+ end;
+
+ val pp =
+ Parser.ppMap
+ toList
+ (Parser.ppBracket "{" "}" (Parser.ppSequence "," Name.pp));
+
+end
+
+structure NameMap = KeyMap (NameOrdered);
+
+structure NameArity =
+struct
+
+type nameArity = Name.name * int;
+
+fun name ((n,_) : nameArity) = n;
+
+fun arity ((_,i) : nameArity) = i;
+
+fun nary i n_i = arity n_i = i;
+
+val nullary = nary 0
+and unary = nary 1
+and binary = nary 2
+and ternary = nary 3;
+
+fun compare ((n1,i1),(n2,i2)) =
+ case Name.compare (n1,n2) of
+ LESS => LESS
+ | EQUAL => Int.compare (i1,i2)
+ | GREATER => GREATER;
+
+val pp = Parser.ppMap (fn (n,i) => n ^ "/" ^ Int.toString i) Parser.ppString;
+
+end
+
+structure NameArityOrdered =
+struct type t = NameArity.nameArity val compare = NameArity.compare end
+
+structure NameAritySet =
+struct
+
+ local
+ structure S = ElementSet (NameArityOrdered);
+ in
+ open S;
+ end;
+
+ val allNullary = all NameArity.nullary;
+
+ val pp =
+ Parser.ppMap
+ toList
+ (Parser.ppBracket "{" "}" (Parser.ppSequence "," NameArity.pp));
+
+end
+
+structure NameArityMap = KeyMap (NameArityOrdered);
+end;
+
+(**** Original file: Term.sig ****)
+
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC TERMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Term =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic terms. *)
+(* ------------------------------------------------------------------------- *)
+
+type var = Metis.Name.name
+
+type functionName = Metis.Name.name
+
+type function = functionName * int
+
+type const = functionName
+
+datatype term =
+ Var of var
+ | Fn of functionName * term list
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Variables *)
+
+val destVar : term -> var
+
+val isVar : term -> bool
+
+val equalVar : var -> term -> bool
+
+(* Functions *)
+
+val destFn : term -> functionName * term list
+
+val isFn : term -> bool
+
+val fnName : term -> functionName
+
+val fnArguments : term -> term list
+
+val fnArity : term -> int
+
+val fnFunction : term -> function
+
+val functions : term -> Metis.NameAritySet.set
+
+val functionNames : term -> Metis.NameSet.set
+
+(* Constants *)
+
+val mkConst : const -> term
+
+val destConst : term -> const
+
+val isConst : term -> bool
+
+(* Binary functions *)
+
+val mkBinop : functionName -> term * term -> term
+
+val destBinop : functionName -> term -> term * term
+
+val isBinop : functionName -> term -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a term in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : term -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for terms. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : term * term -> order
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+type path = int list
+
+val subterm : term -> path -> term
+
+val subterms : term -> (path * term) list
+
+val replace : term -> path * term -> term
+
+val find : (term -> bool) -> term -> path option
+
+val ppPath : path Metis.Parser.pp
+
+val pathToString : path -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : var -> term -> bool
+
+val freeVars : term -> Metis.NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Fresh variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val newVar : unit -> term
+
+val newVars : int -> term list
+
+val variantPrime : Metis.NameSet.set -> var -> var
+
+val variantNum : Metis.NameSet.set -> var -> var
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+val isTypedVar : term -> bool
+
+val typedSymbols : term -> int
+
+val nonVarTypedSubterms : term -> (path * term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with an explicit function application operator. *)
+(* ------------------------------------------------------------------------- *)
+
+val mkComb : term * term -> term
+
+val destComb : term -> term * term
+
+val isComb : term -> bool
+
+val listMkComb : term * term list -> term
+
+val stripComb : term -> term * term list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Infix symbols *)
+
+val infixes : Metis.Parser.infixities ref
+
+(* The negation symbol *)
+
+val negation : Metis.Name.name ref
+
+(* Binder symbols *)
+
+val binders : Metis.Name.name list ref
+
+(* Bracket symbols *)
+
+val brackets : (Metis.Name.name * Metis.Name.name) list ref
+
+(* Pretty printing *)
+
+val pp : term Metis.Parser.pp
+
+val toString : term -> string
+
+(* Parsing *)
+
+val fromString : string -> term
+
+val parse : term Metis.Parser.quotation -> term
+
+end
+
+(**** Original file: Term.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC TERMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Term :> Term =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* Helper functions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun stripSuffix pred s =
+ let
+ fun f 0 = ""
+ | f n =
+ let
+ val n' = n - 1
+ in
+ if pred (String.sub (s,n')) then f n'
+ else String.substring (s,0,n)
+ end
+ in
+ f (size s)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic terms. *)
+(* ------------------------------------------------------------------------- *)
+
+type var = Name.name;
+
+type functionName = Name.name;
+
+type function = functionName * int;
+
+type const = functionName;
+
+datatype term =
+ Var of Name.name
+ | Fn of Name.name * term list;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Variables *)
+
+fun destVar (Var v) = v
+ | destVar (Fn _) = raise Error "destVar";
+
+val isVar = can destVar;
+
+fun equalVar v (Var v') = v = v'
+ | equalVar _ _ = false;
+
+(* Functions *)
+
+fun destFn (Fn f) = f
+ | destFn (Var _) = raise Error "destFn";
+
+val isFn = can destFn;
+
+fun fnName tm = fst (destFn tm);
+
+fun fnArguments tm = snd (destFn tm);
+
+fun fnArity tm = length (fnArguments tm);
+
+fun fnFunction tm = (fnName tm, fnArity tm);
+
+local
+ fun func fs [] = fs
+ | func fs (Var _ :: tms) = func fs tms
+ | func fs (Fn (n,l) :: tms) =
+ func (NameAritySet.add fs (n, length l)) (l @ tms);
+in
+ fun functions tm = func NameAritySet.empty [tm];
+end;
+
+local
+ fun func fs [] = fs
+ | func fs (Var _ :: tms) = func fs tms
+ | func fs (Fn (n,l) :: tms) = func (NameSet.add fs n) (l @ tms);
+in
+ fun functionNames tm = func NameSet.empty [tm];
+end;
+
+(* Constants *)
+
+fun mkConst c = (Fn (c, []));
+
+fun destConst (Fn (c, [])) = c
+ | destConst _ = raise Error "destConst";
+
+val isConst = can destConst;
+
+(* Binary functions *)
+
+fun mkBinop f (a,b) = Fn (f,[a,b]);
+
+fun destBinop f (Fn (x,[a,b])) =
+ if x = f then (a,b) else raise Error "Term.destBinop: wrong binop"
+ | destBinop _ _ = raise Error "Term.destBinop: not a binop";
+
+fun isBinop f = can (destBinop f);
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a term in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun sz n [] = n
+ | sz n (Var _ :: tms) = sz (n + 1) tms
+ | sz n (Fn (_,args) :: tms) = sz (n + 1) (args @ tms);
+in
+ fun symbols tm = sz 0 [tm];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for terms. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun cmp [] [] = EQUAL
+ | cmp (Var _ :: _) (Fn _ :: _) = LESS
+ | cmp (Fn _ :: _) (Var _ :: _) = GREATER
+ | cmp (Var v1 :: tms1) (Var v2 :: tms2) =
+ (case Name.compare (v1,v2) of
+ LESS => LESS
+ | EQUAL => cmp tms1 tms2
+ | GREATER => GREATER)
+ | cmp (Fn (f1,a1) :: tms1) (Fn (f2,a2) :: tms2) =
+ (case Name.compare (f1,f2) of
+ LESS => LESS
+ | EQUAL =>
+ (case Int.compare (length a1, length a2) of
+ LESS => LESS
+ | EQUAL => cmp (a1 @ tms1) (a2 @ tms2)
+ | GREATER => GREATER)
+ | GREATER => GREATER)
+ | cmp _ _ = raise Bug "Term.compare";
+in
+ fun compare (tm1,tm2) = cmp [tm1] [tm2];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+type path = int list;
+
+fun subterm tm [] = tm
+ | subterm (Var _) (_ :: _) = raise Error "Term.subterm: Var"
+ | subterm (Fn (_,tms)) (h :: t) =
+ if h >= length tms then raise Error "Term.replace: Fn"
+ else subterm (List.nth (tms,h)) t;
+
+local
+ fun subtms [] acc = acc
+ | subtms ((path,tm) :: rest) acc =
+ let
+ fun f (n,arg) = (n :: path, arg)
+
+ val acc = (rev path, tm) :: acc
+ in
+ case tm of
+ Var _ => subtms rest acc
+ | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
+ end;
+in
+ fun subterms tm = subtms [([],tm)] [];
+end;
+
+fun replace tm ([],res) = if res = tm then tm else res
+ | replace tm (h :: t, res) =
+ case tm of
+ Var _ => raise Error "Term.replace: Var"
+ | Fn (func,tms) =>
+ if h >= length tms then raise Error "Term.replace: Fn"
+ else
+ let
+ val arg = List.nth (tms,h)
+ val arg' = replace arg (t,res)
+ in
+ if Sharing.pointerEqual (arg',arg) then tm
+ else Fn (func, updateNth (h,arg') tms)
+ end;
+
+fun find pred =
+ let
+ fun search [] = NONE
+ | search ((path,tm) :: rest) =
+ if pred tm then SOME (rev path)
+ else
+ case tm of
+ Var _ => search rest
+ | Fn (_,a) =>
+ let
+ val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
+ in
+ search (subtms @ rest)
+ end
+ in
+ fn tm => search [([],tm)]
+ end;
+
+val ppPath = Parser.ppList Parser.ppInt;
+
+val pathToString = Parser.toString ppPath;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun free _ [] = false
+ | free v (Var w :: tms) = v = w orelse free v tms
+ | free v (Fn (_,args) :: tms) = free v (args @ tms);
+in
+ fun freeIn v tm = free v [tm];
+end;
+
+local
+ fun free vs [] = vs
+ | free vs (Var v :: tms) = free (NameSet.add vs v) tms
+ | free vs (Fn (_,args) :: tms) = free vs (args @ tms);
+in
+ fun freeVars tm = free NameSet.empty [tm];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Fresh variables. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ val prefix = "_";
+
+ fun numVar i = Var (mkPrefix prefix (Int.toString i));
+in
+ fun newVar () = numVar (newInt ());
+
+ fun newVars n = map numVar (newInts n);
+end;
+
+fun variantPrime avoid =
+ let
+ fun f v = if NameSet.member v avoid then f (v ^ "'") else v
+ in
+ f
+ end;
+
+fun variantNum avoid v =
+ if not (NameSet.member v avoid) then v
+ else
+ let
+ val v = stripSuffix Char.isDigit v
+
+ fun f n =
+ let
+ val v_n = v ^ Int.toString n
+ in
+ if NameSet.member v_n avoid then f (n + 1) else v_n
+ end
+ in
+ f 0
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun isTypedVar (Var _) = true
+ | isTypedVar (Fn (":", [Var _, _])) = true
+ | isTypedVar (Fn _) = false;
+
+local
+ fun sz n [] = n
+ | sz n (Var _ :: tms) = sz (n + 1) tms
+ | sz n (Fn (":",[tm,_]) :: tms) = sz n (tm :: tms)
+ | sz n (Fn (_,args) :: tms) = sz (n + 1) (args @ tms);
+in
+ fun typedSymbols tm = sz 0 [tm];
+end;
+
+local
+ fun subtms [] acc = acc
+ | subtms ((_, Var _) :: rest) acc = subtms rest acc
+ | subtms ((_, Fn (":", [Var _, _])) :: rest) acc = subtms rest acc
+ | subtms ((path, tm as Fn func) :: rest) acc =
+ let
+ fun f (n,arg) = (n :: path, arg)
+
+ val acc = (rev path, tm) :: acc
+ in
+ case func of
+ (":",[arg,_]) => subtms ((0 :: path, arg) :: rest) acc
+ | (_,args) => subtms (map f (enumerate args) @ rest) acc
+ end;
+in
+ fun nonVarTypedSubterms tm = subtms [([],tm)] [];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with an explicit function application operator. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkComb (f,a) = Fn (".",[f,a]);
+
+fun destComb (Fn (".",[f,a])) = (f,a)
+ | destComb _ = raise Error "destComb";
+
+val isComb = can destComb;
+
+fun listMkComb (f,l) = foldl mkComb f l;
+
+local
+ fun strip tms (Fn (".",[f,a])) = strip (a :: tms) f
+ | strip tms tm = (tm,tms);
+in
+ fun stripComb tm = strip [] tm;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Operators parsed and printed infix *)
+
+val infixes : Parser.infixities ref = ref
+ [(* ML symbols *)
+ {token = " / ", precedence = 7, leftAssoc = true},
+ {token = " div ", precedence = 7, leftAssoc = true},
+ {token = " mod ", precedence = 7, leftAssoc = true},
+ {token = " * ", precedence = 7, leftAssoc = true},
+ {token = " + ", precedence = 6, leftAssoc = true},
+ {token = " - ", precedence = 6, leftAssoc = true},
+ {token = " ^ ", precedence = 6, leftAssoc = true},
+ {token = " @ ", precedence = 5, leftAssoc = false},
+ {token = " :: ", precedence = 5, leftAssoc = false},
+ {token = " = ", precedence = 4, leftAssoc = true},
+ {token = " <> ", precedence = 4, leftAssoc = true},
+ {token = " <= ", precedence = 4, leftAssoc = true},
+ {token = " < ", precedence = 4, leftAssoc = true},
+ {token = " >= ", precedence = 4, leftAssoc = true},
+ {token = " > ", precedence = 4, leftAssoc = true},
+ {token = " o ", precedence = 3, leftAssoc = true},
+ {token = " -> ", precedence = 2, leftAssoc = false}, (* inferred prec *)
+ {token = " : ", precedence = 1, leftAssoc = false}, (* inferred prec *)
+ {token = ", ", precedence = 0, leftAssoc = false}, (* inferred prec *)
+
+ (* Logical connectives *)
+ {token = " /\\ ", precedence = ~1, leftAssoc = false},
+ {token = " \\/ ", precedence = ~2, leftAssoc = false},
+ {token = " ==> ", precedence = ~3, leftAssoc = false},
+ {token = " <=> ", precedence = ~4, leftAssoc = false},
+
+ (* Other symbols *)
+ {token = " . ", precedence = 9, leftAssoc = true}, (* function app *)
+ {token = " ** ", precedence = 8, leftAssoc = true},
+ {token = " ++ ", precedence = 6, leftAssoc = true},
+ {token = " -- ", precedence = 6, leftAssoc = true},
+ {token = " == ", precedence = 4, leftAssoc = true}];
+
+(* The negation symbol *)
+
+val negation : Name.name ref = ref "~";
+
+(* Binder symbols *)
+
+val binders : Name.name list ref = ref ["\\","!","?","?!"];
+
+(* Bracket symbols *)
+
+val brackets : (Name.name * Name.name) list ref = ref [("[","]"),("{","}")];
+
+(* Pretty printing *)
+
+local
+ open Parser;
+in
+ fun pp inputPpstrm inputTerm =
+ let
+ val quants = !binders
+ and iOps = !infixes
+ and neg = !negation
+ and bracks = !brackets
+
+ val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
+
+ val bTokens = map #2 bracks @ map #3 bracks
+
+ val iTokens = infixTokens iOps
+
+ fun destI (Fn (f,[a,b])) =
+ if mem f iTokens then SOME (f,a,b) else NONE
+ | destI _ = NONE
+
+ val iPrinter = ppInfixes iOps destI
+
+ val specialTokens = neg :: quants @ ["$","(",")"] @ bTokens @ iTokens
+
+ fun vName bv s = NameSet.member s bv
+
+ fun checkVarName bv s = if vName bv s then s else "$" ^ s
+
+ fun varName bv = ppMap (checkVarName bv) ppString
+
+ fun checkFunctionName bv s =
+ if mem s specialTokens orelse vName bv s then "(" ^ s ^ ")" else s
+
+ fun functionName bv = ppMap (checkFunctionName bv) ppString
+
+ fun isI tm = Option.isSome (destI tm)
+
+ fun stripNeg (tm as Fn (f,[a])) =
+ if f <> neg then (0,tm)
+ else let val (n,tm) = stripNeg a in (n + 1, tm) end
+ | stripNeg tm = (0,tm)
+
+ val destQuant =
+ let
+ fun dest q (Fn (q', [Var v, body])) =
+ if q <> q' then NONE
+ else
+ (case dest q body of
+ NONE => SOME (q,v,[],body)
+ | SOME (_,v',vs,body) => SOME (q, v, v' :: vs, body))
+ | dest _ _ = NONE
+ in
+ fn tm => Useful.first (fn q => dest q tm) quants
+ end
+
+ fun isQuant tm = Option.isSome (destQuant tm)
+
+ fun destBrack (Fn (b,[tm])) =
+ (case List.find (fn (n,_,_) => n = b) bracks of
+ NONE => NONE
+ | SOME (_,b1,b2) => SOME (b1,tm,b2))
+ | destBrack _ = NONE
+
+ fun isBrack tm = Option.isSome (destBrack tm)
+
+ fun functionArgument bv ppstrm tm =
+ (addBreak ppstrm (1,0);
+ if isBrack tm then customBracket bv ppstrm tm
+ else if isVar tm orelse isConst tm then basic bv ppstrm tm
+ else bracket bv ppstrm tm)
+
+ and basic bv ppstrm (Var v) = varName bv ppstrm v
+ | basic bv ppstrm (Fn (f,args)) =
+ (beginBlock ppstrm Inconsistent 2;
+ functionName bv ppstrm f;
+ app (functionArgument bv ppstrm) args;
+ endBlock ppstrm)
+
+ and customBracket bv ppstrm tm =
+ case destBrack tm of
+ SOME (b1,tm,b2) => ppBracket b1 b2 (term bv) ppstrm tm
+ | NONE => basic bv ppstrm tm
+
+ and innerQuant bv ppstrm tm =
+ case destQuant tm of
+ NONE => term bv ppstrm tm
+ | SOME (q,v,vs,tm) =>
+ let
+ val bv = NameSet.addList (NameSet.add bv v) vs
+ in
+ addString ppstrm q;
+ varName bv ppstrm v;
+ app (fn v => (addBreak ppstrm (1,0); varName bv ppstrm v)) vs;
+ addString ppstrm ".";
+ addBreak ppstrm (1,0);
+ innerQuant bv ppstrm tm
+ end
+
+ and quantifier bv ppstrm tm =
+ if not (isQuant tm) then customBracket bv ppstrm tm
+ else
+ (beginBlock ppstrm Inconsistent 2;
+ innerQuant bv ppstrm tm;
+ endBlock ppstrm)
+
+ and molecule bv ppstrm (tm,r) =
+ let
+ val (n,tm) = stripNeg tm
+ in
+ beginBlock ppstrm Inconsistent n;
+ funpow n (fn () => addString ppstrm neg) ();
+ if isI tm orelse (r andalso isQuant tm) then bracket bv ppstrm tm
+ else quantifier bv ppstrm tm;
+ endBlock ppstrm
+ end
+
+ and term bv ppstrm tm = iPrinter (molecule bv) ppstrm (tm,false)
+
+ and bracket bv ppstrm tm = ppBracket "(" ")" (term bv) ppstrm tm
+ in
+ term NameSet.empty
+ end inputPpstrm inputTerm;
+end;
+
+fun toString tm = Parser.toString pp tm;
+
+(* Parsing *)
+
+local
+ open Parser;
+
+ infixr 9 >>++
+ infixr 8 ++
+ infixr 7 >>
+ infixr 6 ||
+
+ val isAlphaNum =
+ let
+ val alphaNumChars = explode "_'"
+ in
+ fn c => mem c alphaNumChars orelse Char.isAlphaNum c
+ end;
+
+ local
+ val alphaNumToken = atLeastOne (some isAlphaNum) >> implode;
+
+ val symbolToken =
+ let
+ fun isNeg c = str c = !negation
+
+ val symbolChars = explode "<>=-*+/\\?@|!$%&#^:;~"
+
+ fun isSymbol c = mem c symbolChars
+
+ fun isNonNegSymbol c = not (isNeg c) andalso isSymbol c
+ in
+ some isNeg >> str ||
+ (some isNonNegSymbol ++ many (some isSymbol)) >> (implode o op::)
+ end;
+
+ val punctToken =
+ let
+ val punctChars = explode "()[]{}.,"
+
+ fun isPunct c = mem c punctChars
+ in
+ some isPunct >> str
+ end;
+
+ val lexToken = alphaNumToken || symbolToken || punctToken;
+
+ val space = many (some Char.isSpace);
+ in
+ val lexer = (space ++ lexToken ++ space) >> (fn (_,(tok,_)) => tok);
+ end;
+
+ fun termParser inputStream =
+ let
+ val quants = !binders
+ and iOps = !infixes
+ and neg = !negation
+ and bracks = ("(",")") :: !brackets
+
+ val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
+
+ val bTokens = map #2 bracks @ map #3 bracks
+
+ fun possibleVarName "" = false
+ | possibleVarName s = isAlphaNum (String.sub (s,0))
+
+ fun vName bv s = NameSet.member s bv
+
+ val iTokens = infixTokens iOps
+
+ val iParser = parseInfixes iOps (fn (f,a,b) => Fn (f,[a,b]))
+
+ val specialTokens = neg :: quants @ ["$"] @ bTokens @ iTokens
+
+ fun varName bv =
+ Parser.some (vName bv) ||
+ (exact "$" ++ some possibleVarName) >> (fn (_,s) => s)
+
+ fun fName bv s = not (mem s specialTokens) andalso not (vName bv s)
+
+ fun functionName bv =
+ Parser.some (fName bv) ||
+ (exact "(" ++ any ++ exact ")") >> (fn (_,(s,_)) => s)
+
+ fun basic bv tokens =
+ let
+ val var = varName bv >> Var
+
+ val const = functionName bv >> (fn f => Fn (f,[]))
+
+ fun bracket (ab,a,b) =
+ (exact a ++ term bv ++ exact b) >>
+ (fn (_,(tm,_)) => if ab = "()" then tm else Fn (ab,[tm]))
+
+ fun quantifier q =
+ let
+ fun bind (v,t) = Fn (q, [Var v, t])
+ in
+ (exact q ++ atLeastOne (some possibleVarName) ++
+ exact ".") >>++
+ (fn (_,(vs,_)) =>
+ term (NameSet.addList bv vs) >>
+ (fn body => foldr bind body vs))
+ end
+ in
+ var ||
+ const ||
+ first (map bracket bracks) ||
+ first (map quantifier quants)
+ end tokens
+
+ and molecule bv tokens =
+ let
+ val negations = many (exact neg) >> length
+
+ val function =
+ (functionName bv ++ many (basic bv)) >> Fn || basic bv
+ in
+ (negations ++ function) >>
+ (fn (n,tm) => funpow n (fn t => Fn (neg,[t])) tm)
+ end tokens
+
+ and term bv tokens = iParser (molecule bv) tokens
+ in
+ term NameSet.empty
+ end inputStream;
+in
+ fun fromString input =
+ let
+ val chars = Stream.fromList (explode input)
+
+ val tokens = everything (lexer >> singleton) chars
+
+ val terms = everything (termParser >> singleton) tokens
+ in
+ case Stream.toList terms of
+ [tm] => tm
+ | _ => raise Error "Syntax.stringToTerm"
+ end;
+end;
+
+local
+ val antiquotedTermToString =
+ Parser.toString (Parser.ppBracket "(" ")" pp);
+in
+ val parse = Parser.parseQuotation antiquotedTermToString fromString;
+end;
+
+end
+
+structure TermOrdered =
+struct type t = Term.term val compare = Term.compare end
+
+structure TermSet = ElementSet (TermOrdered);
+
+structure TermMap = KeyMap (TermOrdered);
+end;
+
+(**** Original file: Subst.sig ****)
+
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC SUBSTITUTIONS *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Subst =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+type subst
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val empty : subst
+
+val null : subst -> bool
+
+val size : subst -> int
+
+val peek : subst -> Metis.Term.var -> Metis.Term.term option
+
+val insert : subst -> Metis.Term.var * Metis.Term.term -> subst
+
+val singleton : Metis.Term.var * Metis.Term.term -> subst
+
+val union : subst -> subst -> subst
+
+val toList : subst -> (Metis.Term.var * Metis.Term.term) list
+
+val fromList : (Metis.Term.var * Metis.Term.term) list -> subst
+
+val foldl : (Metis.Term.var * Metis.Term.term * 'a -> 'a) -> 'a -> subst -> 'a
+
+val foldr : (Metis.Term.var * Metis.Term.term * 'a -> 'a) -> 'a -> subst -> 'a
+
+val pp : subst Metis.Parser.pp
+
+val toString : subst -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Normalizing removes identity substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val normalize : subst -> subst
+
+(* ------------------------------------------------------------------------- *)
+(* Applying a substitution to a first order logic term. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : subst -> Metis.Term.term -> Metis.Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Restricting a substitution to a smaller set of variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val restrict : subst -> Metis.NameSet.set -> subst
+
+val remove : subst -> Metis.NameSet.set -> subst
+
+(* ------------------------------------------------------------------------- *)
+(* Composing two substitutions so that the following identity holds: *)
+(* *)
+(* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *)
+(* ------------------------------------------------------------------------- *)
+
+val compose : subst -> subst -> subst
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions can be inverted iff they are renaming substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val invert : subst -> subst (* raises Error *)
+
+val isRenaming : subst -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Creating a substitution to freshen variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freshVars : Metis.NameSet.set -> subst
+
+(* ------------------------------------------------------------------------- *)
+(* Matching for first order logic terms. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : subst -> Metis.Term.term -> Metis.Term.term -> subst (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* Unification for first order logic terms. *)
+(* ------------------------------------------------------------------------- *)
+
+val unify : subst -> Metis.Term.term -> Metis.Term.term -> subst (* raises Error *)
+
+end
+
+(**** Original file: Subst.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC SUBSTITUTIONS *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Subst :> Subst =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype subst = Subst of Term.term NameMap.map;
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations. *)
+(* ------------------------------------------------------------------------- *)
+
+val empty = Subst (NameMap.new ());
+
+fun null (Subst m) = NameMap.null m;
+
+fun size (Subst m) = NameMap.size m;
+
+fun peek (Subst m) v = NameMap.peek m v;
+
+fun insert (Subst m) v_tm = Subst (NameMap.insert m v_tm);
+
+fun singleton v_tm = insert empty v_tm;
+
+local
+ fun compatible (tm1,tm2) =
+ if tm1 = tm2 then SOME tm1 else raise Error "Subst.union: incompatible";
+in
+ fun union (s1 as Subst m1) (s2 as Subst m2) =
+ if NameMap.null m1 then s2
+ else if NameMap.null m2 then s1
+ else Subst (NameMap.union compatible m1 m2);
+end;
+
+fun toList (Subst m) = NameMap.toList m;
+
+fun fromList l = Subst (NameMap.fromList l);
+
+fun foldl f b (Subst m) = NameMap.foldl f b m;
+
+fun foldr f b (Subst m) = NameMap.foldr f b m;
+
+fun pp ppstrm sub =
+ Parser.ppBracket "<[" "]>"
+ (Parser.ppSequence "," (Parser.ppBinop " |->" Parser.ppString Term.pp))
+ ppstrm (toList sub);
+
+val toString = Parser.toString pp;
+
+(* ------------------------------------------------------------------------- *)
+(* Normalizing removes identity substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun isNotId (v,tm) = not (Term.equalVar v tm);
+in
+ fun normalize (sub as Subst m) =
+ let
+ val m' = NameMap.filter isNotId m
+ in
+ if NameMap.size m = NameMap.size m' then sub else Subst m'
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Applying a substitution to a first order logic term. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub =
+ let
+ fun tmSub (tm as Term.Var v) =
+ (case peek sub v of
+ SOME tm' => if Sharing.pointerEqual (tm,tm') then tm else tm'
+ | NONE => tm)
+ | tmSub (tm as Term.Fn (f,args)) =
+ let
+ val args' = Sharing.map tmSub args
+ in
+ if Sharing.pointerEqual (args,args') then tm
+ else Term.Fn (f,args')
+ end
+ in
+ fn tm => if null sub then tm else tmSub tm
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Restricting a substitution to a given set of variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun restrict (sub as Subst m) varSet =
+ let
+ fun isRestrictedVar (v,_) = NameSet.member v varSet
+
+ val m' = NameMap.filter isRestrictedVar m
+ in
+ if NameMap.size m = NameMap.size m' then sub else Subst m'
+ end;
+
+fun remove (sub as Subst m) varSet =
+ let
+ fun isRestrictedVar (v,_) = not (NameSet.member v varSet)
+
+ val m' = NameMap.filter isRestrictedVar m
+ in
+ if NameMap.size m = NameMap.size m' then sub else Subst m'
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Composing two substitutions so that the following identity holds: *)
+(* *)
+(* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm) *)
+(* ------------------------------------------------------------------------- *)
+
+fun compose (sub1 as Subst m1) sub2 =
+ let
+ fun f (v,tm,s) = insert s (v, subst sub2 tm)
+ in
+ if null sub2 then sub1 else NameMap.foldl f sub2 m1
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions can be inverted iff they are renaming substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun inv (v, Term.Var w, s) =
+ if NameMap.inDomain w s then raise Error "Subst.invert: non-injective"
+ else NameMap.insert s (w, Term.Var v)
+ | inv (_, Term.Fn _, _) = raise Error "Subst.invert: non-variable";
+in
+ fun invert (Subst m) = Subst (NameMap.foldl inv (NameMap.new ()) m);
+end;
+
+val isRenaming = can invert;
+
+(* ------------------------------------------------------------------------- *)
+(* Creating a substitution to freshen variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freshVars =
+ let
+ fun add (v,m) = insert m (v, Term.newVar ())
+ in
+ NameSet.foldl add empty
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching for first order logic terms. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun matchList sub [] = sub
+ | matchList sub ((Term.Var v, tm) :: rest) =
+ let
+ val sub =
+ case peek sub v of
+ NONE => insert sub (v,tm)
+ | SOME tm' =>
+ if tm = tm' then sub
+ else raise Error "Subst.match: incompatible matches"
+ in
+ matchList sub rest
+ end
+ | matchList sub ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) =
+ if f1 = f2 andalso length args1 = length args2 then
+ matchList sub (zip args1 args2 @ rest)
+ else raise Error "Subst.match: different structure"
+ | matchList _ _ = raise Error "Subst.match: functions can't match vars";
+in
+ fun match sub tm1 tm2 = matchList sub [(tm1,tm2)];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Unification for first order logic terms. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun solve sub [] = sub
+ | solve sub ((tm1_tm2 as (tm1,tm2)) :: rest) =
+ if Portable.pointerEqual tm1_tm2 then solve sub rest
+ else solve' sub (subst sub tm1) (subst sub tm2) rest
+
+ and solve' sub (Term.Var v) tm rest =
+ if Term.equalVar v tm then solve sub rest
+ else if Term.freeIn v tm then raise Error "Subst.unify: occurs check"
+ else
+ (case peek sub v of
+ NONE => solve (compose sub (singleton (v,tm))) rest
+ | SOME tm' => solve' sub tm' tm rest)
+ | solve' sub tm1 (tm2 as Term.Var _) rest = solve' sub tm2 tm1 rest
+ | solve' sub (Term.Fn (f1,args1)) (Term.Fn (f2,args2)) rest =
+ if f1 = f2 andalso length args1 = length args2 then
+ solve sub (zip args1 args2 @ rest)
+ else
+ raise Error "Subst.unify: different structure";
+in
+ fun unify sub tm1 tm2 = solve sub [(tm1,tm2)];
+end;
+
+end
+end;
+
+(**** Original file: Atom.sig ****)
+
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Atom =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+type relationName = Metis.Name.name
+
+type relation = relationName * int
+
+type atom = relationName * Metis.Term.term list
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val name : atom -> relationName
+
+val arguments : atom -> Metis.Term.term list
+
+val arity : atom -> int
+
+val relation : atom -> relation
+
+val functions : atom -> Metis.NameAritySet.set
+
+val functionNames : atom -> Metis.NameSet.set
+
+(* Binary relations *)
+
+val mkBinop : relationName -> Metis.Term.term * Metis.Term.term -> atom
+
+val destBinop : relationName -> atom -> Metis.Term.term * Metis.Term.term
+
+val isBinop : relationName -> atom -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* The size of an atom in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : atom -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : atom * atom -> order
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+val subterm : atom -> Metis.Term.path -> Metis.Term.term
+
+val subterms : atom -> (Metis.Term.path * Metis.Term.term) list
+
+val replace : atom -> Metis.Term.path * Metis.Term.term -> atom
+
+val find : (Metis.Term.term -> bool) -> atom -> Metis.Term.path option
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Metis.Term.var -> atom -> bool
+
+val freeVars : atom -> Metis.NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Metis.Subst.subst -> atom -> atom
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : Metis.Subst.subst -> atom -> atom -> Metis.Subst.subst (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+val unify : Metis.Subst.subst -> atom -> atom -> Metis.Subst.subst (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val eqRelation : relation
+
+val mkEq : Metis.Term.term * Metis.Term.term -> atom
+
+val destEq : atom -> Metis.Term.term * Metis.Term.term
+
+val isEq : atom -> bool
+
+val mkRefl : Metis.Term.term -> atom
+
+val destRefl : atom -> Metis.Term.term
+
+val isRefl : atom -> bool
+
+val sym : atom -> atom (* raises Error if given a refl *)
+
+val lhs : atom -> Metis.Term.term
+
+val rhs : atom -> Metis.Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+val typedSymbols : atom -> int
+
+val nonVarTypedSubterms : atom -> (Metis.Term.path * Metis.Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : atom Metis.Parser.pp
+
+val toString : atom -> string
+
+val fromString : string -> atom
+
+val parse : Metis.Term.term Metis.Parser.quotation -> atom
+
+end
+
+(**** Original file: Atom.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC ATOMS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Atom :> Atom =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+type relationName = Name.name;
+
+type relation = relationName * int;
+
+type atom = relationName * Term.term list;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun name ((rel,_) : atom) = rel;
+
+fun arguments ((_,args) : atom) = args;
+
+fun arity atm = length (arguments atm);
+
+fun relation atm = (name atm, arity atm);
+
+val functions =
+ let
+ fun f (tm,acc) = NameAritySet.union (Term.functions tm) acc
+ in
+ fn atm => foldl f NameAritySet.empty (arguments atm)
+ end;
+
+val functionNames =
+ let
+ fun f (tm,acc) = NameSet.union (Term.functionNames tm) acc
+ in
+ fn atm => foldl f NameSet.empty (arguments atm)
+ end;
+
+(* Binary relations *)
+
+fun mkBinop p (a,b) : atom = (p,[a,b]);
+
+fun destBinop p (x,[a,b]) =
+ if x = p then (a,b) else raise Error "Atom.destBinop: wrong binop"
+ | destBinop _ _ = raise Error "Atom.destBinop: not a binop";
+
+fun isBinop p = can (destBinop p);
+
+(* ------------------------------------------------------------------------- *)
+(* The size of an atom in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+fun symbols atm = foldl (fn (tm,z) => Term.symbols tm + z) 1 (arguments atm);
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for atoms. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare ((p1,tms1),(p2,tms2)) =
+ case Name.compare (p1,p2) of
+ LESS => LESS
+ | EQUAL => lexCompare Term.compare (tms1,tms2)
+ | GREATER => GREATER;
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subterm _ [] = raise Bug "Atom.subterm: empty path"
+ | subterm ((_,tms) : atom) (h :: t) =
+ if h >= length tms then raise Error "Atom.subterm: bad path"
+ else Term.subterm (List.nth (tms,h)) t;
+
+fun subterms ((_,tms) : atom) =
+ let
+ fun f ((n,tm),l) = map (fn (p,s) => (n :: p, s)) (Term.subterms tm) @ l
+ in
+ foldl f [] (enumerate tms)
+ end;
+
+fun replace _ ([],_) = raise Bug "Atom.replace: empty path"
+ | replace (atm as (rel,tms)) (h :: t, res) : atom =
+ if h >= length tms then raise Error "Atom.replace: bad path"
+ else
+ let
+ val tm = List.nth (tms,h)
+ val tm' = Term.replace tm (t,res)
+ in
+ if Sharing.pointerEqual (tm,tm') then atm
+ else (rel, updateNth (h,tm') tms)
+ end;
+
+fun find pred =
+ let
+ fun f (i,tm) =
+ case Term.find pred tm of
+ SOME path => SOME (i :: path)
+ | NONE => NONE
+ in
+ fn (_,tms) : atom => first f (enumerate tms)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v atm = List.exists (Term.freeIn v) (arguments atm);
+
+val freeVars =
+ let
+ fun f (tm,acc) = NameSet.union (Term.freeVars tm) acc
+ in
+ fn atm => foldl f NameSet.empty (arguments atm)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub (atm as (p,tms)) : atom =
+ let
+ val tms' = Sharing.map (Subst.subst sub) tms
+ in
+ if Sharing.pointerEqual (tms',tms) then atm else (p,tms')
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun matchArg ((tm1,tm2),sub) = Subst.match sub tm1 tm2;
+in
+ fun match sub (p1,tms1) (p2,tms2) =
+ let
+ val _ = (p1 = p2 andalso length tms1 = length tms2) orelse
+ raise Error "Atom.match"
+ in
+ foldl matchArg sub (zip tms1 tms2)
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun unifyArg ((tm1,tm2),sub) = Subst.unify sub tm1 tm2;
+in
+ fun unify sub (p1,tms1) (p2,tms2) =
+ let
+ val _ = (p1 = p2 andalso length tms1 = length tms2) orelse
+ raise Error "Atom.unify"
+ in
+ foldl unifyArg sub (zip tms1 tms2)
+ end;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val eqName = "=";
+
+val eqArity = 2;
+
+val eqRelation = (eqName,eqArity);
+
+val mkEq = mkBinop eqName;
+
+fun destEq x = destBinop eqName x;
+
+fun isEq x = isBinop eqName x;
+
+fun mkRefl tm = mkEq (tm,tm);
+
+fun destRefl atm =
+ let
+ val (l,r) = destEq atm
+ val _ = l = r orelse raise Error "Atom.destRefl"
+ in
+ l
+ end;
+
+fun isRefl x = can destRefl x;
+
+fun sym atm =
+ let
+ val (l,r) = destEq atm
+ val _ = l <> r orelse raise Error "Atom.sym: refl"
+ in
+ mkEq (r,l)
+ end;
+
+fun lhs atm = fst (destEq atm);
+
+fun rhs atm = snd (destEq atm);
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun typedSymbols ((_,tms) : atom) =
+ foldl (fn (tm,z) => Term.typedSymbols tm + z) 1 tms;
+
+fun nonVarTypedSubterms (_,tms) =
+ let
+ fun addArg ((n,arg),acc) =
+ let
+ fun addTm ((path,tm),acc) = (n :: path, tm) :: acc
+ in
+ foldl addTm acc (Term.nonVarTypedSubterms arg)
+ end
+ in
+ foldl addArg [] (enumerate tms)
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Parser.ppMap Term.Fn Term.pp;
+
+val toString = Parser.toString pp;
+
+fun fromString s = Term.destFn (Term.fromString s);
+
+val parse = Parser.parseQuotation Term.toString fromString;
+
+end
+
+structure AtomOrdered =
+struct type t = Atom.atom val compare = Atom.compare end
+
+structure AtomSet = ElementSet (AtomOrdered);
+
+structure AtomMap = KeyMap (AtomOrdered);
+end;
+
+(**** Original file: Formula.sig ****)
+
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC FORMULAS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Formula =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+ True
+ | False
+ | Atom of Metis.Atom.atom
+ | Not of formula
+ | And of formula * formula
+ | Or of formula * formula
+ | Imp of formula * formula
+ | Iff of formula * formula
+ | Forall of Metis.Term.var * formula
+ | Exists of Metis.Term.var * formula
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Booleans *)
+
+val mkBoolean : bool -> formula
+
+val destBoolean : formula -> bool
+
+val isBoolean : formula -> bool
+
+(* Functions *)
+
+val functions : formula -> Metis.NameAritySet.set
+
+val functionNames : formula -> Metis.NameSet.set
+
+(* Relations *)
+
+val relations : formula -> Metis.NameAritySet.set
+
+val relationNames : formula -> Metis.NameSet.set
+
+(* Atoms *)
+
+val destAtom : formula -> Metis.Atom.atom
+
+val isAtom : formula -> bool
+
+(* Negations *)
+
+val destNeg : formula -> formula
+
+val isNeg : formula -> bool
+
+val stripNeg : formula -> int * formula
+
+(* Conjunctions *)
+
+val listMkConj : formula list -> formula
+
+val stripConj : formula -> formula list
+
+val flattenConj : formula -> formula list
+
+(* Disjunctions *)
+
+val listMkDisj : formula list -> formula
+
+val stripDisj : formula -> formula list
+
+val flattenDisj : formula -> formula list
+
+(* Equivalences *)
+
+val listMkEquiv : formula list -> formula
+
+val stripEquiv : formula -> formula list
+
+val flattenEquiv : formula -> formula list
+
+(* Universal quantification *)
+
+val destForall : formula -> Metis.Term.var * formula
+
+val isForall : formula -> bool
+
+val listMkForall : Metis.Term.var list * formula -> formula
+
+val stripForall : formula -> Metis.Term.var list * formula
+
+(* Existential quantification *)
+
+val destExists : formula -> Metis.Term.var * formula
+
+val isExists : formula -> bool
+
+val listMkExists : Metis.Term.var list * formula -> formula
+
+val stripExists : formula -> Metis.Term.var list * formula
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a formula in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : formula -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : formula * formula -> order
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Metis.Term.var -> formula -> bool
+
+val freeVars : formula -> Metis.NameSet.set
+
+val specialize : formula -> formula
+
+val generalize : formula -> formula
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Metis.Subst.subst -> formula -> formula
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val mkEq : Metis.Term.term * Metis.Term.term -> formula
+
+val destEq : formula -> Metis.Term.term * Metis.Term.term
+
+val isEq : formula -> bool
+
+val mkNeq : Metis.Term.term * Metis.Term.term -> formula
+
+val destNeq : formula -> Metis.Term.term * Metis.Term.term
+
+val isNeq : formula -> bool
+
+val mkRefl : Metis.Term.term -> formula
+
+val destRefl : formula -> Metis.Term.term
+
+val isRefl : formula -> bool
+
+val sym : formula -> formula (* raises Error if given a refl *)
+
+val lhs : formula -> Metis.Term.term
+
+val rhs : formula -> Metis.Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+type quotation = formula Metis.Parser.quotation
+
+val pp : formula Metis.Parser.pp
+
+val toString : formula -> string
+
+val fromString : string -> formula
+
+val parse : quotation -> formula
+
+end
+
+(**** Original file: Formula.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC FORMULAS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Formula :> Formula =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type of first order logic formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formula =
+ True
+ | False
+ | Atom of Atom.atom
+ | Not of formula
+ | And of formula * formula
+ | Or of formula * formula
+ | Imp of formula * formula
+ | Iff of formula * formula
+ | Forall of Term.var * formula
+ | Exists of Term.var * formula;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+(* Booleans *)
+
+fun mkBoolean true = True
+ | mkBoolean false = False;
+
+fun destBoolean True = true
+ | destBoolean False = false
+ | destBoolean _ = raise Error "destBoolean";
+
+val isBoolean = can destBoolean;
+
+(* Functions *)
+
+local
+ fun funcs fs [] = fs
+ | funcs fs (True :: fms) = funcs fs fms
+ | funcs fs (False :: fms) = funcs fs fms
+ | funcs fs (Atom atm :: fms) =
+ funcs (NameAritySet.union (Atom.functions atm) fs) fms
+ | funcs fs (Not p :: fms) = funcs fs (p :: fms)
+ | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
+ | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
+in
+ fun functions fm = funcs NameAritySet.empty [fm];
+end;
+
+local
+ fun funcs fs [] = fs
+ | funcs fs (True :: fms) = funcs fs fms
+ | funcs fs (False :: fms) = funcs fs fms
+ | funcs fs (Atom atm :: fms) =
+ funcs (NameSet.union (Atom.functionNames atm) fs) fms
+ | funcs fs (Not p :: fms) = funcs fs (p :: fms)
+ | funcs fs (And (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Or (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Imp (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Iff (p,q) :: fms) = funcs fs (p :: q :: fms)
+ | funcs fs (Forall (_,p) :: fms) = funcs fs (p :: fms)
+ | funcs fs (Exists (_,p) :: fms) = funcs fs (p :: fms);
+in
+ fun functionNames fm = funcs NameSet.empty [fm];
+end;
+
+(* Relations *)
+
+local
+ fun rels fs [] = fs
+ | rels fs (True :: fms) = rels fs fms
+ | rels fs (False :: fms) = rels fs fms
+ | rels fs (Atom atm :: fms) =
+ rels (NameAritySet.add fs (Atom.relation atm)) fms
+ | rels fs (Not p :: fms) = rels fs (p :: fms)
+ | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
+ | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
+in
+ fun relations fm = rels NameAritySet.empty [fm];
+end;
+
+local
+ fun rels fs [] = fs
+ | rels fs (True :: fms) = rels fs fms
+ | rels fs (False :: fms) = rels fs fms
+ | rels fs (Atom atm :: fms) = rels (NameSet.add fs (Atom.name atm)) fms
+ | rels fs (Not p :: fms) = rels fs (p :: fms)
+ | rels fs (And (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Or (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Imp (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Iff (p,q) :: fms) = rels fs (p :: q :: fms)
+ | rels fs (Forall (_,p) :: fms) = rels fs (p :: fms)
+ | rels fs (Exists (_,p) :: fms) = rels fs (p :: fms);
+in
+ fun relationNames fm = rels NameSet.empty [fm];
+end;
+
+(* Atoms *)
+
+fun destAtom (Atom atm) = atm
+ | destAtom _ = raise Error "Formula.destAtom";
+
+val isAtom = can destAtom;
+
+(* Negations *)
+
+fun destNeg (Not p) = p
+ | destNeg _ = raise Error "Formula.destNeg";
+
+val isNeg = can destNeg;
+
+val stripNeg =
+ let
+ fun strip n (Not fm) = strip (n + 1) fm
+ | strip n fm = (n,fm)
+ in
+ strip 0
+ end;
+
+(* Conjunctions *)
+
+fun listMkConj fms =
+ case rev fms of [] => True | fm :: fms => foldl And fm fms;
+
+local
+ fun strip cs (And (p,q)) = strip (p :: cs) q
+ | strip cs fm = rev (fm :: cs);
+in
+ fun stripConj True = []
+ | stripConj fm = strip [] fm;
+end;
+
+val flattenConj =
+ let
+ fun flat acc [] = acc
+ | flat acc (And (p,q) :: fms) = flat acc (q :: p :: fms)
+ | flat acc (True :: fms) = flat acc fms
+ | flat acc (fm :: fms) = flat (fm :: acc) fms
+ in
+ fn fm => flat [] [fm]
+ end;
+
+(* Disjunctions *)
+
+fun listMkDisj fms =
+ case rev fms of [] => False | fm :: fms => foldl Or fm fms;
+
+local
+ fun strip cs (Or (p,q)) = strip (p :: cs) q
+ | strip cs fm = rev (fm :: cs);
+in
+ fun stripDisj False = []
+ | stripDisj fm = strip [] fm;
+end;
+
+val flattenDisj =
+ let
+ fun flat acc [] = acc
+ | flat acc (Or (p,q) :: fms) = flat acc (q :: p :: fms)
+ | flat acc (False :: fms) = flat acc fms
+ | flat acc (fm :: fms) = flat (fm :: acc) fms
+ in
+ fn fm => flat [] [fm]
+ end;
+
+(* Equivalences *)
+
+fun listMkEquiv fms =
+ case rev fms of [] => True | fm :: fms => foldl Iff fm fms;
+
+local
+ fun strip cs (Iff (p,q)) = strip (p :: cs) q
+ | strip cs fm = rev (fm :: cs);
+in
+ fun stripEquiv True = []
+ | stripEquiv fm = strip [] fm;
+end;
+
+val flattenEquiv =
+ let
+ fun flat acc [] = acc
+ | flat acc (Iff (p,q) :: fms) = flat acc (q :: p :: fms)
+ | flat acc (True :: fms) = flat acc fms
+ | flat acc (fm :: fms) = flat (fm :: acc) fms
+ in
+ fn fm => flat [] [fm]
+ end;
+
+(* Universal quantifiers *)
+
+fun destForall (Forall v_f) = v_f
+ | destForall _ = raise Error "destForall";
+
+val isForall = can destForall;
+
+fun listMkForall ([],body) = body
+ | listMkForall (v :: vs, body) = Forall (v, listMkForall (vs,body));
+
+local
+ fun strip vs (Forall (v,b)) = strip (v :: vs) b
+ | strip vs tm = (rev vs, tm);
+in
+ val stripForall = strip [];
+end;
+
+(* Existential quantifiers *)
+
+fun destExists (Exists v_f) = v_f
+ | destExists _ = raise Error "destExists";
+
+val isExists = can destExists;
+
+fun listMkExists ([],body) = body
+ | listMkExists (v :: vs, body) = Exists (v, listMkExists (vs,body));
+
+local
+ fun strip vs (Exists (v,b)) = strip (v :: vs) b
+ | strip vs tm = (rev vs, tm);
+in
+ val stripExists = strip [];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a formula in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun sz n [] = n
+ | sz n (True :: fms) = sz (n + 1) fms
+ | sz n (False :: fms) = sz (n + 1) fms
+ | sz n (Atom atm :: fms) = sz (n + Atom.symbols atm) fms
+ | sz n (Not p :: fms) = sz (n + 1) (p :: fms)
+ | sz n (And (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Or (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Imp (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Iff (p,q) :: fms) = sz (n + 1) (p :: q :: fms)
+ | sz n (Forall (_,p) :: fms) = sz (n + 1) (p :: fms)
+ | sz n (Exists (_,p) :: fms) = sz (n + 1) (p :: fms);
+in
+ fun symbols fm = sz 0 [fm];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for formulas. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun cmp [] = EQUAL
+ | cmp ((True,True) :: l) = cmp l
+ | cmp ((True,_) :: _) = LESS
+ | cmp ((_,True) :: _) = GREATER
+ | cmp ((False,False) :: l) = cmp l
+ | cmp ((False,_) :: _) = LESS
+ | cmp ((_,False) :: _) = GREATER
+ | cmp ((Atom atm1, Atom atm2) :: l) =
+ (case Atom.compare (atm1,atm2) of
+ LESS => LESS
+ | EQUAL => cmp l
+ | GREATER => GREATER)
+ | cmp ((Atom _, _) :: _) = LESS
+ | cmp ((_, Atom _) :: _) = GREATER
+ | cmp ((Not p1, Not p2) :: l) = cmp ((p1,p2) :: l)
+ | cmp ((Not _, _) :: _) = LESS
+ | cmp ((_, Not _) :: _) = GREATER
+ | cmp ((And (p1,q1), And (p2,q2)) :: l) = cmp ((p1,p2) :: (q1,q2) :: l)
+ | cmp ((And _, _) :: _) = LESS
+ | cmp ((_, And _) :: _) = GREATER
+ | cmp ((Or (p1,q1), Or (p2,q2)) :: l) = cmp ((p1,p2) :: (q1,q2) :: l)
+ | cmp ((Or _, _) :: _) = LESS
+ | cmp ((_, Or _) :: _) = GREATER
+ | cmp ((Imp (p1,q1), Imp (p2,q2)) :: l) = cmp ((p1,p2) :: (q1,q2) :: l)
+ | cmp ((Imp _, _) :: _) = LESS
+ | cmp ((_, Imp _) :: _) = GREATER
+ | cmp ((Iff (p1,q1), Iff (p2,q2)) :: l) = cmp ((p1,p2) :: (q1,q2) :: l)
+ | cmp ((Iff _, _) :: _) = LESS
+ | cmp ((_, Iff _) :: _) = GREATER
+ | cmp ((Forall (v1,p1), Forall (v2,p2)) :: l) =
+ (case Name.compare (v1,v2) of
+ LESS => LESS
+ | EQUAL => cmp ((p1,p2) :: l)
+ | GREATER => GREATER)
+ | cmp ((Forall _, Exists _) :: _) = LESS
+ | cmp ((Exists _, Forall _) :: _) = GREATER
+ | cmp ((Exists (v1,p1), Exists (v2,p2)) :: l) =
+ (case Name.compare (v1,v2) of
+ LESS => LESS
+ | EQUAL => cmp ((p1,p2) :: l)
+ | GREATER => GREATER);
+in
+ fun compare fm1_fm2 = cmp [fm1_fm2];
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v =
+ let
+ fun f [] = false
+ | f (True :: fms) = f fms
+ | f (False :: fms) = f fms
+ | f (Atom atm :: fms) = Atom.freeIn v atm orelse f fms
+ | f (Not p :: fms) = f (p :: fms)
+ | f (And (p,q) :: fms) = f (p :: q :: fms)
+ | f (Or (p,q) :: fms) = f (p :: q :: fms)
+ | f (Imp (p,q) :: fms) = f (p :: q :: fms)
+ | f (Iff (p,q) :: fms) = f (p :: q :: fms)
+ | f (Forall (w,p) :: fms) = if v = w then f fms else f (p :: fms)
+ | f (Exists (w,p) :: fms) = if v = w then f fms else f (p :: fms)
+ in
+ fn fm => f [fm]
+ end;
+
+local
+ fun fv vs [] = vs
+ | fv vs ((_,True) :: fms) = fv vs fms
+ | fv vs ((_,False) :: fms) = fv vs fms
+ | fv vs ((bv, Atom atm) :: fms) =
+ fv (NameSet.union vs (NameSet.difference (Atom.freeVars atm) bv)) fms
+ | fv vs ((bv, Not p) :: fms) = fv vs ((bv,p) :: fms)
+ | fv vs ((bv, And (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Or (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Imp (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Iff (p,q)) :: fms) = fv vs ((bv,p) :: (bv,q) :: fms)
+ | fv vs ((bv, Forall (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms)
+ | fv vs ((bv, Exists (v,p)) :: fms) = fv vs ((NameSet.add bv v, p) :: fms);
+in
+ fun freeVars fm = fv NameSet.empty [(NameSet.empty,fm)];
+end;
+
+fun specialize fm = snd (stripForall fm);
+
+fun generalize fm = listMkForall (NameSet.toList (freeVars fm), fm);
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+local
+ fun substCheck sub fm = if Subst.null sub then fm else substFm sub fm
+
+ and substFm sub fm =
+ case fm of
+ True => fm
+ | False => fm
+ | Atom (p,tms) =>
+ let
+ val tms' = Sharing.map (Subst.subst sub) tms
+ in
+ if Sharing.pointerEqual (tms,tms') then fm else Atom (p,tms')
+ end
+ | Not p =>
+ let
+ val p' = substFm sub p
+ in
+ if Sharing.pointerEqual (p,p') then fm else Not p'
+ end
+ | And (p,q) => substConn sub fm And p q
+ | Or (p,q) => substConn sub fm Or p q
+ | Imp (p,q) => substConn sub fm Imp p q
+ | Iff (p,q) => substConn sub fm Iff p q
+ | Forall (v,p) => substQuant sub fm Forall v p
+ | Exists (v,p) => substQuant sub fm Exists v p
+
+ and substConn sub fm conn p q =
+ let
+ val p' = substFm sub p
+ and q' = substFm sub q
+ in
+ if Sharing.pointerEqual (p,p') andalso
+ Sharing.pointerEqual (q,q')
+ then fm
+ else conn (p',q')
+ end
+
+ and substQuant sub fm quant v p =
+ let
+ val v' =
+ let
+ fun f (w,s) =
+ if w = v then s
+ else
+ case Subst.peek sub w of
+ NONE => NameSet.add s w
+ | SOME tm => NameSet.union s (Term.freeVars tm)
+
+ val vars = freeVars p
+ val vars = NameSet.foldl f NameSet.empty vars
+ in
+ Term.variantPrime vars v
+ end
+
+ val sub =
+ if v = v' then Subst.remove sub (NameSet.singleton v)
+ else Subst.insert sub (v, Term.Var v')
+
+ val p' = substCheck sub p
+ in
+ if v = v' andalso Sharing.pointerEqual (p,p') then fm
+ else quant (v',p')
+ end;
+in
+ val subst = substCheck;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkEq a_b = Atom (Atom.mkEq a_b);
+
+fun destEq fm = Atom.destEq (destAtom fm);
+
+val isEq = can destEq;
+
+fun mkNeq a_b = Not (mkEq a_b);
+
+fun destNeq (Not fm) = destEq fm
+ | destNeq _ = raise Error "Formula.destNeq";
+
+val isNeq = can destNeq;
+
+fun mkRefl tm = Atom (Atom.mkRefl tm);
+
+fun destRefl fm = Atom.destRefl (destAtom fm);
+
+val isRefl = can destRefl;
+
+fun sym fm = Atom (Atom.sym (destAtom fm));
+
+fun lhs fm = fst (destEq fm);
+
+fun rhs fm = snd (destEq fm);
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+type quotation = formula Parser.quotation
+
+val truthSymbol = "T"
+and falsitySymbol = "F"
+and conjunctionSymbol = "/\\"
+and disjunctionSymbol = "\\/"
+and implicationSymbol = "==>"
+and equivalenceSymbol = "<=>"
+and universalSymbol = "!"
+and existentialSymbol = "?";
+
+local
+ fun demote True = Term.Fn (truthSymbol,[])
+ | demote False = Term.Fn (falsitySymbol,[])
+ | demote (Atom (p,tms)) = Term.Fn (p,tms)
+ | demote (Not p) = Term.Fn (!Term.negation, [demote p])
+ | demote (And (p,q)) = Term.Fn (conjunctionSymbol, [demote p, demote q])
+ | demote (Or (p,q)) = Term.Fn (disjunctionSymbol, [demote p, demote q])
+ | demote (Imp (p,q)) = Term.Fn (implicationSymbol, [demote p, demote q])
+ | demote (Iff (p,q)) = Term.Fn (equivalenceSymbol, [demote p, demote q])
+ | demote (Forall (v,b)) = Term.Fn (universalSymbol, [Term.Var v, demote b])
+ | demote (Exists (v,b)) =
+ Term.Fn (existentialSymbol, [Term.Var v, demote b]);
+in
+ fun pp ppstrm fm = Term.pp ppstrm (demote fm);
+end;
+
+val toString = Parser.toString pp;
+
+local
+ fun isQuant [Term.Var _, _] = true
+ | isQuant _ = false;
+
+ fun promote (Term.Var v) = Atom (v,[])
+ | promote (Term.Fn (f,tms)) =
+ if f = truthSymbol andalso null tms then
+ True
+ else if f = falsitySymbol andalso null tms then
+ False
+ else if f = !Term.negation andalso length tms = 1 then
+ Not (promote (hd tms))
+ else if f = conjunctionSymbol andalso length tms = 2 then
+ And (promote (hd tms), promote (List.nth (tms,1)))
+ else if f = disjunctionSymbol andalso length tms = 2 then
+ Or (promote (hd tms), promote (List.nth (tms,1)))
+ else if f = implicationSymbol andalso length tms = 2 then
+ Imp (promote (hd tms), promote (List.nth (tms,1)))
+ else if f = equivalenceSymbol andalso length tms = 2 then
+ Iff (promote (hd tms), promote (List.nth (tms,1)))
+ else if f = universalSymbol andalso isQuant tms then
+ Forall (Term.destVar (hd tms), promote (List.nth (tms,1)))
+ else if f = existentialSymbol andalso isQuant tms then
+ Exists (Term.destVar (hd tms), promote (List.nth (tms,1)))
+ else
+ Atom (f,tms);
+in
+ fun fromString s = promote (Term.fromString s);
+end;
+
+val parse = Parser.parseQuotation toString fromString;
+
+end
+end;
+
+(**** Original file: Literal.sig ****)
+
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC LITERALS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Literal =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic literals. *)
+(* ------------------------------------------------------------------------- *)
+
+type polarity = bool
+
+type literal = polarity * Metis.Atom.atom
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val polarity : literal -> polarity
+
+val atom : literal -> Metis.Atom.atom
+
+val name : literal -> Metis.Atom.relationName
+
+val arguments : literal -> Metis.Term.term list
+
+val arity : literal -> int
+
+val positive : literal -> bool
+
+val negative : literal -> bool
+
+val negate : literal -> literal
+
+val relation : literal -> Metis.Atom.relation
+
+val functions : literal -> Metis.NameAritySet.set
+
+val functionNames : literal -> Metis.NameSet.set
+
+(* Binary relations *)
+
+val mkBinop : Metis.Atom.relationName -> polarity * Metis.Term.term * Metis.Term.term -> literal
+
+val destBinop : Metis.Atom.relationName -> literal -> polarity * Metis.Term.term * Metis.Term.term
+
+val isBinop : Metis.Atom.relationName -> literal -> bool
+
+(* Formulas *)
+
+val toFormula : literal -> Metis.Formula.formula
+
+val fromFormula : Metis.Formula.formula -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a literal in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+val symbols : literal -> int
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for literals. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : literal * literal -> order (* negative < positive *)
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+val subterm : literal -> Metis.Term.path -> Metis.Term.term
+
+val subterms : literal -> (Metis.Term.path * Metis.Term.term) list
+
+val replace : literal -> Metis.Term.path * Metis.Term.term -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Metis.Term.var -> literal -> bool
+
+val freeVars : literal -> Metis.NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Metis.Subst.subst -> literal -> literal
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+val match : (* raises Error *)
+ Metis.Subst.subst -> literal -> literal -> Metis.Subst.subst
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+val unify : (* raises Error *)
+ Metis.Subst.subst -> literal -> literal -> Metis.Subst.subst
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+val mkEq : Metis.Term.term * Metis.Term.term -> literal
+
+val destEq : literal -> Metis.Term.term * Metis.Term.term
+
+val isEq : literal -> bool
+
+val mkNeq : Metis.Term.term * Metis.Term.term -> literal
+
+val destNeq : literal -> Metis.Term.term * Metis.Term.term
+
+val isNeq : literal -> bool
+
+val mkRefl : Metis.Term.term -> literal
+
+val destRefl : literal -> Metis.Term.term
+
+val isRefl : literal -> bool
+
+val mkIrrefl : Metis.Term.term -> literal
+
+val destIrrefl : literal -> Metis.Term.term
+
+val isIrrefl : literal -> bool
+
+(* The following work with both equalities and disequalities *)
+
+val sym : literal -> literal (* raises Error if given a refl or irrefl *)
+
+val lhs : literal -> Metis.Term.term
+
+val rhs : literal -> Metis.Term.term
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+val typedSymbols : literal -> int
+
+val nonVarTypedSubterms : literal -> (Metis.Term.path * Metis.Term.term) list
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp : literal Metis.Parser.pp
+
+val toString : literal -> string
+
+val fromString : string -> literal
+
+val parse : Metis.Term.term Metis.Parser.quotation -> literal
+
+end
+
+(**** Original file: Literal.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* FIRST ORDER LOGIC LITERALS *)
+(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Literal :> Literal =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* A type for storing first order logic literals. *)
+(* ------------------------------------------------------------------------- *)
+
+type polarity = bool;
+
+type literal = polarity * Atom.atom;
+
+(* ------------------------------------------------------------------------- *)
+(* Constructors and destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun polarity ((pol,_) : literal) = pol;
+
+fun atom ((_,atm) : literal) = atm;
+
+fun name lit = Atom.name (atom lit);
+
+fun arguments lit = Atom.arguments (atom lit);
+
+fun arity lit = Atom.arity (atom lit);
+
+fun positive lit = polarity lit;
+
+fun negative lit = not (polarity lit);
+
+fun negate (pol,atm) : literal = (not pol, atm)
+
+fun relation lit = Atom.relation (atom lit);
+
+fun functions lit = Atom.functions (atom lit);
+
+fun functionNames lit = Atom.functionNames (atom lit);
+
+(* Binary relations *)
+
+fun mkBinop rel (pol,a,b) : literal = (pol, Atom.mkBinop rel (a,b));
+
+fun destBinop rel ((pol,atm) : literal) =
+ case Atom.destBinop rel atm of (a,b) => (pol,a,b);
+
+fun isBinop rel = can (destBinop rel);
+
+(* Formulas *)
+
+fun toFormula (true,atm) = Formula.Atom atm
+ | toFormula (false,atm) = Formula.Not (Formula.Atom atm);
+
+fun fromFormula (Formula.Atom atm) = (true,atm)
+ | fromFormula (Formula.Not (Formula.Atom atm)) = (false,atm)
+ | fromFormula _ = raise Error "Literal.fromFormula";
+
+(* ------------------------------------------------------------------------- *)
+(* The size of a literal in symbols. *)
+(* ------------------------------------------------------------------------- *)
+
+fun symbols ((_,atm) : literal) = Atom.symbols atm;
+
+(* ------------------------------------------------------------------------- *)
+(* A total comparison function for literals. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare ((pol1,atm1),(pol2,atm2)) =
+ case boolCompare (pol1,pol2) of
+ LESS => GREATER
+ | EQUAL => Atom.compare (atm1,atm2)
+ | GREATER => LESS;
+
+(* ------------------------------------------------------------------------- *)
+(* Subterms. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subterm lit path = Atom.subterm (atom lit) path;
+
+fun subterms lit = Atom.subterms (atom lit);
+
+fun replace (lit as (pol,atm)) path_tm =
+ let
+ val atm' = Atom.replace atm path_tm
+ in
+ if Sharing.pointerEqual (atm,atm') then lit else (pol,atm')
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v lit = Atom.freeIn v (atom lit);
+
+fun freeVars lit = Atom.freeVars (atom lit);
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions. *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub (lit as (pol,atm)) : literal =
+ let
+ val atm' = Atom.subst sub atm
+ in
+ if Sharing.pointerEqual (atm',atm) then lit else (pol,atm')
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Matching. *)
+(* ------------------------------------------------------------------------- *)
+
+fun match sub ((pol1,atm1) : literal) (pol2,atm2) =
+ let
+ val _ = pol1 = pol2 orelse raise Error "Literal.match"
+ in
+ Atom.match sub atm1 atm2
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* Unification. *)
+(* ------------------------------------------------------------------------- *)
+
+fun unify sub ((pol1,atm1) : literal) (pol2,atm2) =
+ let
+ val _ = pol1 = pol2 orelse raise Error "Literal.unify"
+ in
+ Atom.unify sub atm1 atm2
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* The equality relation. *)
+(* ------------------------------------------------------------------------- *)
+
+fun mkEq l_r : literal = (true, Atom.mkEq l_r);
+
+fun destEq ((true,atm) : literal) = Atom.destEq atm
+ | destEq (false,_) = raise Error "Literal.destEq";
+
+val isEq = can destEq;
+
+fun mkNeq l_r : literal = (false, Atom.mkEq l_r);
+
+fun destNeq ((false,atm) : literal) = Atom.destEq atm
+ | destNeq (true,_) = raise Error "Literal.destNeq";
+
+val isNeq = can destNeq;
+
+fun mkRefl tm = (true, Atom.mkRefl tm);
+
+fun destRefl (true,atm) = Atom.destRefl atm
+ | destRefl (false,_) = raise Error "Literal.destRefl";
+
+val isRefl = can destRefl;
+
+fun mkIrrefl tm = (false, Atom.mkRefl tm);
+
+fun destIrrefl (true,_) = raise Error "Literal.destIrrefl"
+ | destIrrefl (false,atm) = Atom.destRefl atm;
+
+val isIrrefl = can destIrrefl;
+
+fun sym (pol,atm) : literal = (pol, Atom.sym atm);
+
+fun lhs ((_,atm) : literal) = Atom.lhs atm;
+
+fun rhs ((_,atm) : literal) = Atom.rhs atm;
+
+(* ------------------------------------------------------------------------- *)
+(* Special support for terms with type annotations. *)
+(* ------------------------------------------------------------------------- *)
+
+fun typedSymbols ((_,atm) : literal) = Atom.typedSymbols atm;
+
+fun nonVarTypedSubterms ((_,atm) : literal) = Atom.nonVarTypedSubterms atm;
+
+(* ------------------------------------------------------------------------- *)
+(* Parsing and pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val pp = Parser.ppMap toFormula Formula.pp;
+
+val toString = Parser.toString pp;
+
+fun fromString s = fromFormula (Formula.fromString s);
+
+val parse = Parser.parseQuotation Term.toString fromString;
+
+end
+
+structure LiteralOrdered =
+struct type t = Literal.literal val compare = Literal.compare end
+
+structure LiteralSet =
+struct
+
+ local
+ structure S = ElementSet (LiteralOrdered);
+ in
+ open S;
+ end;
+
+ fun negateMember lit set = member (Literal.negate lit) set;
+
+ val negate =
+ let
+ fun f (lit,set) = add set (Literal.negate lit)
+ in
+ foldl f empty
+ end;
+
+ val relations =
+ let
+ fun f (lit,set) = NameAritySet.add set (Literal.relation lit)
+ in
+ foldl f NameAritySet.empty
+ end;
+
+ val functions =
+ let
+ fun f (lit,set) = NameAritySet.union set (Literal.functions lit)
+ in
+ foldl f NameAritySet.empty
+ end;
+
+ val freeVars =
+ let
+ fun f (lit,set) = NameSet.union set (Literal.freeVars lit)
+ in
+ foldl f NameSet.empty
+ end;
+
+ val symbols =
+ let
+ fun f (lit,z) = Literal.symbols lit + z
+ in
+ foldl f 0
+ end;
+
+ val typedSymbols =
+ let
+ fun f (lit,z) = Literal.typedSymbols lit + z
+ in
+ foldl f 0
+ end;
+
+ fun subst sub lits =
+ let
+ fun substLit (lit,(eq,lits')) =
+ let
+ val lit' = Literal.subst sub lit
+ val eq = eq andalso Sharing.pointerEqual (lit,lit')
+ in
+ (eq, add lits' lit')
+ end
+
+ val (eq,lits') = foldl substLit (true,empty) lits
+ in
+ if eq then lits else lits'
+ end;
+
+ val pp =
+ Parser.ppMap
+ toList
+ (Parser.ppBracket "{" "}" (Parser.ppSequence "," Literal.pp));
+
+end
+
+structure LiteralMap = KeyMap (LiteralOrdered);
+end;
+
+(**** Original file: Thm.sig ****)
+
+(* ========================================================================= *)
+(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSES *)
+(* Copyright (c) 2001-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Thm =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* An abstract type of first order logic theorems. *)
+(* ------------------------------------------------------------------------- *)
+
+type clause = Metis.LiteralSet.set
+
+datatype inferenceType =
+ Axiom
+ | Assume
+ | Subst
+ | Factor
+ | Resolve
+ | Refl
+ | Equality
+
+type thm
+
+type inference = inferenceType * thm list
+
+(* ------------------------------------------------------------------------- *)
+(* Theorem destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+val clause : thm -> clause
+
+val inference : thm -> inference
+
+(* Tautologies *)
+
+val isTautology : thm -> bool
+
+(* Contradictions *)
+
+val isContradiction : thm -> bool
+
+(* Unit theorems *)
+
+val destUnit : thm -> Metis.Literal.literal
+
+val isUnit : thm -> bool
+
+(* Unit equality theorems *)
+
+val destUnitEq : thm -> Metis.Term.term * Metis.Term.term
+
+val isUnitEq : thm -> bool
+
+(* Literals *)
+
+val member : Metis.Literal.literal -> thm -> bool
+
+val negateMember : Metis.Literal.literal -> thm -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* A total order. *)
+(* ------------------------------------------------------------------------- *)
+
+val compare : thm * thm -> order
+
+val equal : thm -> thm -> bool
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+val freeIn : Metis.Term.var -> thm -> bool
+
+val freeVars : thm -> Metis.NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+val ppInferenceType : inferenceType Metis.Parser.pp
+
+val inferenceTypeToString : inferenceType -> string
+
+val pp : thm Metis.Parser.pp
+
+val toString : thm -> string
+
+(* ------------------------------------------------------------------------- *)
+(* Primitive rules of inference. *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* *)
+(* ----- axiom C *)
+(* C *)
+(* ------------------------------------------------------------------------- *)
+
+val axiom : clause -> thm
+
+(* ------------------------------------------------------------------------- *)
+(* *)
+(* ----------- assume L *)
+(* L \/ ~L *)
+(* ------------------------------------------------------------------------- *)
+
+val assume : Metis.Literal.literal -> thm
+
+(* ------------------------------------------------------------------------- *)
+(* C *)
+(* -------- subst s *)
+(* C[s] *)
+(* ------------------------------------------------------------------------- *)
+
+val subst : Metis.Subst.subst -> thm -> thm
+
+(* ------------------------------------------------------------------------- *)
+(* L \/ C ~L \/ D *)
+(* --------------------- resolve L *)
+(* C \/ D *)
+(* *)
+(* The literal L must occur in the first theorem, and the literal ~L must *)
+(* occur in the second theorem. *)
+(* ------------------------------------------------------------------------- *)
+
+val resolve : Metis.Literal.literal -> thm -> thm -> thm
+
+(* ------------------------------------------------------------------------- *)
+(* *)
+(* --------- refl t *)
+(* t = t *)
+(* ------------------------------------------------------------------------- *)
+
+val refl : Metis.Term.term -> thm
+
+(* ------------------------------------------------------------------------- *)
+(* *)
+(* ------------------------ equality L p t *)
+(* ~(s = t) \/ ~L \/ L' *)
+(* *)
+(* where s is the subterm of L at path p, and L' is L with the subterm at *)
+(* path p being replaced by t. *)
+(* ------------------------------------------------------------------------- *)
+
+val equality : Metis.Literal.literal -> Metis.Term.path -> Metis.Term.term -> thm
+
+end
+
+(**** Original file: Thm.sml ****)
+
+structure Metis = struct open Metis
+(* Metis-specific ML environment *)
+nonfix ++ -- RL mem union subset;
+val explode = String.explode;
+val implode = String.implode;
+val print = TextIO.print;
+(* ========================================================================= *)
+(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSES *)
+(* Copyright (c) 2001-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Thm :> Thm =
+struct
+
+open Useful;
+
+(* ------------------------------------------------------------------------- *)
+(* An abstract type of first order logic theorems. *)
+(* ------------------------------------------------------------------------- *)
+
+type clause = LiteralSet.set;
+
+datatype inferenceType =
+ Axiom
+ | Assume
+ | Subst
+ | Factor
+ | Resolve
+ | Refl
+ | Equality;
+
+datatype thm = Thm of clause * (inferenceType * thm list);
+
+type inference = inferenceType * thm list;
+
+(* ------------------------------------------------------------------------- *)
+(* Theorem destructors. *)
+(* ------------------------------------------------------------------------- *)
+
+fun clause (Thm (cl,_)) = cl;
+
+fun inference (Thm (_,inf)) = inf;
+
+(* Tautologies *)
+
+local
+ fun chk (_,NONE) = NONE
+ | chk ((pol,atm), SOME set) =
+ if (pol andalso Atom.isRefl atm) orelse AtomSet.member atm set then NONE
+ else SOME (AtomSet.add set atm);
+in
+ fun isTautology th =
+ case LiteralSet.foldl chk (SOME AtomSet.empty) (clause th) of
+ SOME _ => false
+ | NONE => true;
+end;
+
+(* Contradictions *)
+
+fun isContradiction th = LiteralSet.null (clause th);
+
+(* Unit theorems *)
+
+fun destUnit (Thm (cl,_)) =
+ if LiteralSet.size cl = 1 then LiteralSet.pick cl
+ else raise Error "Thm.destUnit";
+
+val isUnit = can destUnit;
+
+(* Unit equality theorems *)
+
+fun destUnitEq th = Literal.destEq (destUnit th);
+
+val isUnitEq = can destUnitEq;
+
+(* Literals *)
+
+fun member lit (Thm (cl,_)) = LiteralSet.member lit cl;
+
+fun negateMember lit (Thm (cl,_)) = LiteralSet.negateMember lit cl;
+
+(* ------------------------------------------------------------------------- *)
+(* A total order. *)
+(* ------------------------------------------------------------------------- *)
+
+fun compare (th1,th2) = LiteralSet.compare (clause th1, clause th2);
+
+fun equal th1 th2 = LiteralSet.equal (clause th1) (clause th2);
+
+(* ------------------------------------------------------------------------- *)
+(* Free variables. *)
+(* ------------------------------------------------------------------------- *)
+
+fun freeIn v (Thm (cl,_)) = LiteralSet.exists (Literal.freeIn v) cl;
+
+local
+ fun free (lit,set) = NameSet.union (Literal.freeVars lit) set;
+in
+ fun freeVars (Thm (cl,_)) = LiteralSet.foldl free NameSet.empty cl;
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Pretty-printing. *)
+(* ------------------------------------------------------------------------- *)
+
+fun inferenceTypeToString Axiom = "Axiom"
+ | inferenceTypeToString Assume = "Assume"
+ | inferenceTypeToString Subst = "Subst"
+ | inferenceTypeToString Factor = "Factor"
+ | inferenceTypeToString Resolve = "Resolve"
+ | inferenceTypeToString Refl = "Refl"
+ | inferenceTypeToString Equality = "Equality";
+
+fun ppInferenceType ppstrm inf =
+ Parser.ppString ppstrm (inferenceTypeToString inf);
+
+local
+ fun toFormula th =
+ Formula.listMkDisj
+ (map Literal.toFormula (LiteralSet.toList (clause th)));
+in
+ fun pp ppstrm th =
+ let
+ open PP
+ in
+ begin_block ppstrm INCONSISTENT 3;
+ add_string ppstrm "|- ";
+ Formula.pp ppstrm (toFormula th);
+ end_block ppstrm
+ end;
+end;
+
+val toString = Parser.toString pp;
+
+(* ------------------------------------------------------------------------- *)
+(* Primitive rules of inference. *)
+(* ------------------------------------------------------------------------- *)
+
+(* ------------------------------------------------------------------------- *)
+(* *)
+(* ----- axiom C *)
+(* C *)
+(* ------------------------------------------------------------------------- *)
+
+fun axiom cl = Thm (cl,(Axiom,[]));
+
+(* ------------------------------------------------------------------------- *)
+(* *)
+(* ----------- assume L *)
+(* L \/ ~L *)
+(* ------------------------------------------------------------------------- *)
+
+fun assume lit =
+ Thm (LiteralSet.fromList [lit, Literal.negate lit], (Assume,[]));
+
+(* ------------------------------------------------------------------------- *)
+(* C *)
+(* -------- subst s *)
+(* C[s] *)
+(* ------------------------------------------------------------------------- *)
+
+fun subst sub (th as Thm (cl,inf)) =
+ let
+ val cl' = LiteralSet.subst sub cl
+ in
+ if Sharing.pointerEqual (cl,cl') then th
+ else
+ case inf of
+ (Subst,_) => Thm (cl',inf)
+ | _ => Thm (cl',(Subst,[th]))
+ end;
+
+(* ------------------------------------------------------------------------- *)
+(* L \/ C ~L \/ D *)
+(* --------------------- resolve L *)
+(* C \/ D *)
+(* *)
+(* The literal L must occur in the first theorem, and the literal ~L must *)
+(* occur in the second theorem. *)
+(* ------------------------------------------------------------------------- *)
+
+fun resolve lit (th1 as Thm (cl1,_)) (th2 as Thm (cl2,_)) =
+ let
+ val cl1' = LiteralSet.delete cl1 lit
+ and cl2' = LiteralSet.delete cl2 (Literal.negate lit)
+ in
+ Thm (LiteralSet.union cl1' cl2', (Resolve,[th1,th2]))
+ end;
+
+(*DEBUG
+val resolve = fn lit => fn pos => fn neg =>
+ resolve lit pos neg
+ handle Error err =>
+ raise Error ("Thm.resolve:\nlit = " ^ Literal.toString lit ^
+ "\npos = " ^ toString pos ^
+ "\nneg = " ^ toString neg ^ "\n" ^ err);
+*)
+
+(* ------------------------------------------------------------------------- *)
+(* *)
+(* --------- refl t *)
+(* t = t *)
+(* ------------------------------------------------------------------------- *)
+
+fun refl tm = Thm (LiteralSet.singleton (true, Atom.mkRefl tm), (Refl,[]));
+
+(* ------------------------------------------------------------------------- *)
+(* *)