src/Tools/Metis/metis.ML
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 30161 c26e515f1c29
child 33004 715566791eb0
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     1 (******************************************************************)
     2 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
     3 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
     4 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
     5 (******************************************************************)
     6 
     7 print_depth 0;
     8 
     9 structure Metis = struct structure Word = Word structure Array = Array end;
    10 
    11 (**** Original file: Portable.sig ****)
    12 
    13 (* ========================================================================= *)
    14 (* ML SPECIFIC FUNCTIONS                                                     *)
    15 (* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
    16 (* ========================================================================= *)
    17 
    18 signature Portable =
    19 sig
    20 
    21 (* ------------------------------------------------------------------------- *)
    22 (* The ML implementation.                                                    *)
    23 (* ------------------------------------------------------------------------- *)
    24 
    25 val ml : string
    26 
    27 (* ------------------------------------------------------------------------- *)
    28 (* Pointer equality using the run-time system.                               *)
    29 (* ------------------------------------------------------------------------- *)
    30 
    31 val pointerEqual : 'a * 'a -> bool
    32 
    33 (* ------------------------------------------------------------------------- *)
    34 (* Timing function applications.                                             *)
    35 (* ------------------------------------------------------------------------- *)
    36 
    37 val time : ('a -> 'b) -> 'a -> 'b
    38 
    39 (* ------------------------------------------------------------------------- *)
    40 (* Critical section markup (multiprocessing)                                 *)
    41 (* ------------------------------------------------------------------------- *)
    42 
    43 val CRITICAL: (unit -> 'a) -> 'a
    44 
    45 (* ------------------------------------------------------------------------- *)
    46 (* Generating random values.                                                 *)
    47 (* ------------------------------------------------------------------------- *)
    48 
    49 val randomBool : unit -> bool
    50 
    51 val randomInt : int -> int  (* n |-> [0,n) *)
    52 
    53 val randomReal : unit -> real  (* () |-> [0,1] *)
    54 
    55 val randomWord : unit -> Metis.Word.word
    56 
    57 end
    58 
    59 (**** Original file: PortableIsabelle.sml ****)
    60 
    61 structure Metis = struct open Metis
    62 (* Metis-specific ML environment *)
    63 nonfix ++ -- RL mem union subset;
    64 val explode = String.explode;
    65 val implode = String.implode;
    66 val print = TextIO.print;
    67 (* ========================================================================= *)
    68 (* Isabelle ML SPECIFIC FUNCTIONS                                            *)
    69 (* ========================================================================= *)
    70 
    71 structure Portable :> Portable =
    72 struct
    73 
    74 (* ------------------------------------------------------------------------- *)
    75 (* The ML implementation.                                                    *)
    76 (* ------------------------------------------------------------------------- *)
    77 
    78 val ml = ml_system;
    79 
    80 (* ------------------------------------------------------------------------- *)
    81 (* Pointer equality using the run-time system.                               *)
    82 (* ------------------------------------------------------------------------- *)
    83 
    84 val pointerEqual = pointer_eq;
    85 
    86 (* ------------------------------------------------------------------------- *)
    87 (* Timing function applications a la Mosml.time.                             *)
    88 (* ------------------------------------------------------------------------- *)
    89 
    90 val time = timeap;
    91 
    92 (* ------------------------------------------------------------------------- *)
    93 (* Critical section markup (multiprocessing)                                 *)
    94 (* ------------------------------------------------------------------------- *)
    95 
    96 fun CRITICAL e = NAMED_CRITICAL "metis" e;
    97 
    98 (* ------------------------------------------------------------------------- *)
    99 (* Generating random values.                                                 *)
   100 (* ------------------------------------------------------------------------- *)
   101 
   102 val randomWord = RandomWord.next_word;
   103 val randomBool = RandomWord.next_bool;
   104 fun randomInt n = RandomWord.next_int 0 (n - 1);
   105 val randomReal = RandomWord.next_real;
   106 
   107 end;
   108 
   109 (* ------------------------------------------------------------------------- *)
   110 (* Quotations a la Moscow ML.                                                *)
   111 (* ------------------------------------------------------------------------- *)
   112 
   113 datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a;
   114 end;
   115 
   116 (**** Original file: PP.sig ****)
   117 
   118 (* ========================================================================= *)
   119 (* PP -- pretty-printing -- from the SML/NJ library                          *)
   120 (*                                                                           *)
   121 (* Modified for Moscow ML from SML/NJ Library version 0.2                    *)
   122 (*                                                                           *)
   123 (* COPYRIGHT (c) 1992 by AT&T Bell Laboratories.                             *)
   124 (*                                                                           *)
   125 (* STANDARD ML OF NEW JERSEY COPYRIGHT NOTICE, LICENSE AND DISCLAIMER.       *)
   126 (*                                                                           *)
   127 (* Permission to use, copy, modify, and distribute this software and its     *)
   128 (* documentation for any purpose and without fee is hereby granted,          *)
   129 (* provided that the above copyright notice appear in all copies and that    *)
   130 (* both the copyright notice and this permission notice and warranty         *)
   131 (* disclaimer appear in supporting documentation, and that the name of       *)
   132 (* AT&T Bell Laboratories or any AT&T entity not be used in advertising      *)
   133 (* or publicity pertaining to distribution of the software without           *)
   134 (* specific, written prior permission.                                       *)
   135 (*                                                                           *)
   136 (* AT&T disclaims all warranties with regard to this software, including     *)
   137 (* all implied warranties of merchantability and fitness.  In no event       *)
   138 (* shall AT&T be liable for any special, indirect or consequential           *)
   139 (* damages or any damages whatsoever resulting from loss of use, data or     *)
   140 (* profits, whether in an action of contract, negligence or other            *)
   141 (* tortious action, arising out of or in connection with the use or          *)
   142 (* performance of this software.                                             *)
   143 (* ========================================================================= *)
   144 
   145 signature PP =
   146 sig
   147 
   148   type ppstream
   149 
   150   type ppconsumer =
   151        {consumer : string -> unit,
   152         linewidth : int,
   153         flush : unit -> unit}
   154 
   155   datatype break_style = 
   156       CONSISTENT
   157     | INCONSISTENT
   158 
   159   val mk_ppstream : ppconsumer -> ppstream
   160 
   161   val dest_ppstream : ppstream -> ppconsumer
   162 
   163   val add_break : ppstream -> int * int -> unit
   164 
   165   val add_newline : ppstream -> unit
   166 
   167   val add_string : ppstream -> string -> unit
   168 
   169   val begin_block : ppstream -> break_style -> int -> unit
   170 
   171   val end_block : ppstream -> unit
   172 
   173   val clear_ppstream : ppstream -> unit
   174 
   175   val flush_ppstream : ppstream -> unit
   176 
   177   val with_pp : ppconsumer -> (ppstream -> unit) -> unit
   178 
   179   val pp_to_string : int -> (ppstream -> 'a -> unit) -> 'a -> string
   180 
   181 end
   182 
   183 (* 
   184    This structure provides tools for creating customized Oppen-style
   185    pretty-printers, based on the type ppstream.  A ppstream is an
   186    output stream that contains prettyprinting commands.  The commands
   187    are placed in the stream by various function calls listed below.
   188 
   189    There following primitives add commands to the stream:
   190    begin_block, end_block, add_string, add_break, and add_newline.
   191    All calls to add_string, add_break, and add_newline must happen
   192    between a pair of calls to begin_block and end_block must be
   193    properly nested dynamically.  All calls to begin_block and
   194    end_block must be properly nested (dynamically).
   195 
   196    [ppconsumer] is the type of sinks for pretty-printing.  A value of 
   197    type ppconsumer is a record 
   198                  { consumer : string -> unit,
   199                    linewidth : int,
   200                    flush : unit -> unit }
   201    of a string consumer, a specified linewidth, and a flush function
   202    which is called whenever flush_ppstream is called.
   203 
   204    A prettyprinter can be called outright to print a value.  In
   205    addition, a prettyprinter for a base type or nullary datatype ty
   206    can be installed in the top-level system.  Then the installed
   207    prettyprinter will be invoked automatically whenever a value of
   208    type ty is to be printed.
   209 
   210    [break_style] is the type of line break styles for blocks:
   211 
   212    [CONSISTENT] specifies that if any line break occurs inside the
   213    block, then all indicated line breaks occur.
   214 
   215    [INCONSISTENT] specifies that breaks will be inserted to only to
   216    avoid overfull lines.
   217 
   218    [mk_ppstream {consumer, linewidth, flush}] creates a new ppstream
   219    which invokes the consumer to output text, putting at most
   220    linewidth characters on each line.
   221 
   222    [dest_ppstream ppstrm] extracts the linewidth, flush function, and
   223    consumer from a ppstream.
   224 
   225    [add_break ppstrm (size, offset)] notifies the pretty-printer that
   226    a line break is possible at this point.  
   227    * When the current block style is CONSISTENT:
   228       ** if the entire block fits on the remainder of the line, then
   229          output size spaces; else
   230       ** increase the current indentation by the block offset;
   231          further indent every item of the block by offset, and add
   232          one newline at every add_break in the block.
   233    * When the current block style is INCONSISTENT:
   234       ** if the next component of the block fits on the remainder of
   235          the line, then output size spaces; else
   236       ** issue a newline and indent to the current indentation level
   237          plus the block offset plus the offset.
   238 
   239    [add_newline ppstrm] issues a newline.
   240 
   241    [add_string ppstrm str] outputs the string str to the ppstream.
   242 
   243    [begin_block ppstrm style blockoffset] begins a new block and
   244    level of indentation, with the given style and block offset.
   245 
   246    [end_block ppstrm] closes the current block.  
   247 
   248    [clear_ppstream ppstrm] restarts the stream, without affecting the
   249    underlying consumer.
   250 
   251    [flush_ppstream ppstrm] executes any remaining commands in the
   252    ppstream (that is, flushes currently accumulated output to the
   253    consumer associated with ppstrm); executes the flush function
   254    associated with the consumer; and calls clear_ppstream.
   255 
   256    [with_pp consumer f] makes a new ppstream from the consumer and
   257    applies f (which can be thought of as a producer) to that
   258    ppstream, then flushed the ppstream and returns the value of f.
   259 
   260    [pp_to_string linewidth printit x] constructs a new ppstream
   261    ppstrm whose consumer accumulates the output in a string s.  Then
   262    evaluates (printit ppstrm x) and finally returns the string s.
   263 
   264 
   265    Example 1: A simple prettyprinter for Booleans:
   266 
   267        load "PP";
   268        fun ppbool pps d = 
   269            let open PP
   270            in
   271                begin_block pps INCONSISTENT 6; 
   272                add_string pps (if d then "right" else "wrong");
   273                end_block pps
   274            end;
   275 
   276    Now one may define a ppstream to print to, and exercise it:
   277 
   278        val ppstrm = Metis.PP.mk_ppstream {consumer  = 
   279                                     fn s => Metis.TextIO.output(Metis.TextIO.stdOut, s), 
   280                                     linewidth = 72,
   281                                     flush     = 
   282                                      fn () => Metis.TextIO.flushOut Metis.TextIO.stdOut};
   283 
   284        fun ppb b = (ppbool ppstrm b; Metis.PP.flush_ppstream ppstrm);
   285 
   286        - ppb false;
   287        wrong> val it = () : unit   
   288 
   289    The prettyprinter may also be installed in the toplevel system;
   290    then it will be used to print all expressions of type bool
   291    subsequently computed:
   292 
   293        - installPP ppbool;
   294        > val it = () : unit
   295        - 1=0;
   296        > val it = wrong : bool
   297        - 1=1;
   298        > val it = right : bool
   299 
   300    See library Meta for a description of installPP.
   301 
   302 
   303    Example 2: Prettyprinting simple expressions (examples/pretty/Metis.ppexpr.sml):
   304 
   305        datatype expr = 
   306            Cst of int 
   307          | Neg of expr
   308          | Plus of expr * expr
   309 
   310        fun ppexpr pps e0 = 
   311            let open PP
   312                fun ppe (Cst i)        = add_string pps (Metis.Int.toString i)
   313                  | ppe (Neg e)        = (add_string pps "~"; ppe e)
   314                  | ppe (Plus(e1, e2)) = (begin_block pps CONSISTENT 0;
   315                                          add_string pps "(";
   316                                          ppe e1; 
   317                                          add_string pps " + ";
   318                                          add_break pps (0, 1);
   319                                          ppe e2; 
   320                                          add_string pps ")";
   321                                          end_block pps)
   322            in
   323                begin_block pps INCONSISTENT 0; 
   324                ppe e0;
   325                end_block pps
   326            end
   327 
   328        val _ = installPP ppexpr;
   329 
   330        (* Some example values: *)
   331 
   332        val e1 = Cst 1;
   333        val e2 = Cst 2;
   334        val e3 = Plus(e1, Neg e2);
   335        val e4 = Plus(Neg e3, e3);
   336        val e5 = Plus(Neg e4, e4);
   337        val e6 = Plus(e5, e5);
   338        val e7 = Plus(e6, e6);
   339        val e8 = 
   340            Plus(e3, Plus(e3, Plus(e3, Plus(e3, Plus(e3, Plus(e3, e7))))));
   341 *)
   342 
   343 (**** Original file: PP.sml ****)
   344 
   345 structure Metis = struct open Metis
   346 (* Metis-specific ML environment *)
   347 nonfix ++ -- RL mem union subset;
   348 val explode = String.explode;
   349 val implode = String.implode;
   350 val print = TextIO.print;
   351 (* ========================================================================= *)
   352 (* PP -- pretty-printing -- from the SML/NJ library                          *)
   353 (*                                                                           *)
   354 (* Modified for Moscow ML from SML/NJ Library version 0.2                    *)
   355 (*                                                                           *)
   356 (* COPYRIGHT (c) 1992 by AT&T Bell Laboratories.                             *)
   357 (*                                                                           *)
   358 (* STANDARD ML OF NEW JERSEY COPYRIGHT NOTICE, LICENSE AND DISCLAIMER.       *)
   359 (*                                                                           *)
   360 (* Permission to use, copy, modify, and distribute this software and its     *)
   361 (* documentation for any purpose and without fee is hereby granted,          *)
   362 (* provided that the above copyright notice appear in all copies and that    *)
   363 (* both the copyright notice and this permission notice and warranty         *)
   364 (* disclaimer appear in supporting documentation, and that the name of       *)
   365 (* AT&T Bell Laboratories or any AT&T entity not be used in advertising      *)
   366 (* or publicity pertaining to distribution of the software without           *)
   367 (* specific, written prior permission.                                       *)
   368 (*                                                                           *)
   369 (* AT&T disclaims all warranties with regard to this software, including     *)
   370 (* all implied warranties of merchantability and fitness.  In no event       *)
   371 (* shall AT&T be liable for any special, indirect or consequential           *)
   372 (* damages or any damages whatsoever resulting from loss of use, data or     *)
   373 (* profits, whether in an action of contract, negligence or other            *)
   374 (* tortious action, arising out of or in connection with the use or          *)
   375 (* performance of this software.                                             *)
   376 (* ========================================================================= *)
   377 
   378 structure PP :> PP =
   379 struct
   380 
   381 open Array 
   382 infix 9 sub
   383 
   384 (* the queue library, formerly in unit Ppqueue *)
   385 
   386 datatype Qend = Qback | Qfront
   387 
   388 exception QUEUE_FULL
   389 exception QUEUE_EMPTY
   390 exception REQUESTED_QUEUE_SIZE_TOO_SMALL
   391 
   392 local 
   393     fun ++ i n = (i + 1) mod n
   394     fun -- i n = (i - 1) mod n
   395 in
   396 
   397 abstype 'a queue = QUEUE of {elems: 'a array, (* the contents *)
   398                              front: int Unsynchronized.ref,
   399                              back: int Unsynchronized.ref,
   400                              size: int}  (* fixed size of element array *)
   401 with
   402 
   403   fun is_empty (QUEUE{front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1,...}) = true
   404     | is_empty _ = false
   405 
   406   fun mk_queue n init_val =
   407       if (n < 2)
   408       then raise REQUESTED_QUEUE_SIZE_TOO_SMALL
   409       else QUEUE{elems=array(n, init_val), front=Unsynchronized.ref ~1, back=Unsynchronized.ref ~1, size=n}
   410 
   411   fun clear_queue (QUEUE{front,back,...}) = (front := ~1; back := ~1)
   412 
   413   fun queue_at Qfront (QUEUE{elems,front,...}) = elems sub !front
   414     | queue_at Qback (QUEUE{elems,back,...}) = elems sub !back
   415 
   416   fun en_queue Qfront item (Q as QUEUE{elems,front,back,size}) =
   417         if (is_empty Q)
   418         then (front := 0; back := 0;
   419               update(elems,0,item))
   420         else let val i = --(!front) size
   421              in  if (i = !back)
   422                  then raise QUEUE_FULL
   423                  else (update(elems,i,item); front := i)
   424              end
   425     | en_queue Qback item (Q as QUEUE{elems,front,back,size}) =
   426         if (is_empty Q)
   427         then (front := 0; back := 0;
   428               update(elems,0,item))
   429         else let val i = ++(!back) size
   430              in  if (i = !front)
   431                  then raise QUEUE_FULL
   432                  else (update(elems,i,item); back := i)
   433              end
   434 
   435   fun de_queue Qfront (Q as QUEUE{front,back,size,...}) =
   436         if (!front = !back) (* unitary queue *)
   437         then clear_queue Q
   438         else front := ++(!front) size
   439     | de_queue Qback (Q as QUEUE{front,back,size,...}) =
   440         if (!front = !back)
   441         then clear_queue Q
   442         else back := --(!back) size
   443 
   444 end (* abstype queue *)
   445 end (* local   *)
   446 
   447 
   448 val magic: 'a -> 'a = fn x => x
   449 
   450 (* exception PP_FAIL of string *)
   451 
   452 datatype break_style = CONSISTENT | INCONSISTENT
   453 
   454 datatype break_info
   455   = FITS
   456   | PACK_ONTO_LINE of int
   457   | ONE_PER_LINE of int
   458 
   459 (* Some global values *)
   460 val INFINITY = 999999
   461 
   462 abstype indent_stack = Istack of break_info list Unsynchronized.ref
   463 with
   464   fun mk_indent_stack() = Istack (Unsynchronized.ref([]:break_info list))
   465   fun clear_indent_stack (Istack stk) = (stk := ([]:break_info list))
   466   fun top (Istack stk) =
   467       case !stk
   468         of nil => raise Fail "PP-error: top: badly formed block"
   469 	 | x::_ => x
   470   fun push (x,(Istack stk)) = stk := x::(!stk)
   471   fun pop (Istack stk) =
   472       case !stk
   473         of nil => raise Fail "PP-error: pop: badly formed block"
   474 	 | _::rest => stk := rest
   475 end
   476 
   477 (* The delim_stack is used to compute the size of blocks. It is
   478    a stack of indices into the token buffer. The indices only point to
   479    BBs, Es, and BRs. We push BBs and Es onto the stack until a BR
   480    is encountered. Then we compute sizes and pop. When we encounter
   481    a BR in the middle of a block, we compute the Distance_to_next_break
   482    of the previous BR in the block, if there was one.
   483 
   484    We need to be able to delete from the bottom of the delim_stack, so
   485    we use a queue, treated with a stack discipline, i.e., we only add
   486    items at the head of the queue, but can delete from the front or
   487    back of the queue.
   488 *)
   489 abstype delim_stack = Dstack of int queue
   490 with
   491   fun new_delim_stack i = Dstack(mk_queue i ~1)
   492   fun reset_delim_stack (Dstack q) = clear_queue q
   493 
   494   fun pop_delim_stack (Dstack d) = de_queue Qfront d
   495   fun pop_bottom_delim_stack (Dstack d) = de_queue Qback d
   496 
   497   fun push_delim_stack(i,Dstack d) = en_queue Qfront i d
   498   fun top_delim_stack (Dstack d) = queue_at Qfront d
   499   fun bottom_delim_stack (Dstack d) = queue_at Qback d
   500   fun delim_stack_is_empty (Dstack d) = is_empty d
   501 end
   502 
   503 
   504 type block_info = { Block_size : int Unsynchronized.ref,
   505                     Block_offset : int,
   506                     How_to_indent : break_style }
   507 
   508 
   509 (* Distance_to_next_break includes Number_of_blanks. Break_offset is
   510    a local offset for the break. BB represents a sequence of contiguous
   511    Begins. E represents a sequence of contiguous Ends.
   512 *)
   513 datatype pp_token
   514   = S of  {String : string, Length : int}
   515   | BB of {Pblocks : block_info list Unsynchronized.ref,   (* Processed   *)
   516            Ublocks : block_info list Unsynchronized.ref}  (* Unprocessed *)
   517   | E of  {Pend : int Unsynchronized.ref, Uend : int Unsynchronized.ref}
   518   | BR of {Distance_to_next_break : int Unsynchronized.ref,
   519            Number_of_blanks : int,
   520            Break_offset : int}
   521 
   522 
   523 (* The initial values in the token buffer *)
   524 val initial_token_value = S{String = "", Length = 0}
   525 
   526 (* type ppstream = General.ppstream; *)
   527 datatype ppstream_ =
   528   PPS of
   529      {consumer : string -> unit,
   530       linewidth : int,
   531       flush : unit -> unit,
   532       the_token_buffer : pp_token array,
   533       the_delim_stack : delim_stack,
   534       the_indent_stack : indent_stack,
   535       ++ : int Unsynchronized.ref -> unit,    (* increment circular buffer index *)
   536       space_left : int Unsynchronized.ref,    (* remaining columns on page *)
   537       left_index : int Unsynchronized.ref,    (* insertion index *)
   538       right_index : int Unsynchronized.ref,   (* output index *)
   539       left_sum : int Unsynchronized.ref,      (* size of strings and spaces inserted *)
   540       right_sum : int Unsynchronized.ref}     (* size of strings and spaces printed *)
   541 
   542 type ppstream = ppstream_
   543 
   544 type ppconsumer = {consumer : string -> unit,
   545 		   linewidth : int,
   546 		   flush : unit -> unit}
   547 
   548 fun mk_ppstream {consumer,linewidth,flush} =
   549     if (linewidth<5)
   550     then raise Fail "PP-error: linewidth too_small"
   551     else let val buf_size = 3*linewidth
   552           in magic(
   553              PPS{consumer = consumer,
   554 		 linewidth = linewidth,
   555 		 flush = flush,
   556 		 the_token_buffer = array(buf_size, initial_token_value),
   557 		 the_delim_stack = new_delim_stack buf_size,
   558 		 the_indent_stack = mk_indent_stack (),
   559 		 ++ = fn i => i := ((!i + 1) mod buf_size),
   560 		 space_left = Unsynchronized.ref linewidth,
   561 		 left_index = Unsynchronized.ref 0, right_index = Unsynchronized.ref 0,
   562 		 left_sum = Unsynchronized.ref 0, right_sum = Unsynchronized.ref 0}
   563                  ) : ppstream
   564 	 end
   565 
   566 fun dest_ppstream(pps : ppstream) =
   567   let val PPS{consumer,linewidth,flush, ...} = magic pps
   568   in {consumer=consumer,linewidth=linewidth,flush=flush} end
   569 
   570 local
   571   val space = " "
   572   fun mk_space (0,s) = String.concat s
   573     | mk_space (n,s) = mk_space((n-1), (space::s))
   574   val space_table = Vector.tabulate(100, fn i => mk_space(i,[]))
   575   fun nspaces n = Vector.sub(space_table, n)
   576       handle General.Subscript =>
   577 	if n < 0
   578 	then ""
   579 	else let val n2 = n div 2
   580 		 val n2_spaces = nspaces n2
   581 		 val extra = if (n = (2*n2)) then "" else space
   582               in String.concat [n2_spaces, n2_spaces, extra]
   583 	     end
   584 in
   585   fun cr_indent (ofn, i) = ofn ("\n"^(nspaces i))
   586   fun indent (ofn,i) = ofn (nspaces i)
   587 end
   588 
   589 
   590 (* Print a the first member of a contiguous sequence of Begins. If there
   591    are "processed" Begins, then take the first off the list. If there are
   592    no processed Begins, take the last member off the "unprocessed" list.
   593    This works because the unprocessed list is treated as a stack, the
   594    processed list as a FIFO queue. How can an item on the unprocessed list
   595    be printable? Because of what goes on in add_string. See there for details.
   596 *)
   597 
   598 fun print_BB (_,{Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =
   599              raise Fail "PP-error: print_BB"
   600   | print_BB (PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
   601              {Pblocks as Unsynchronized.ref({How_to_indent=CONSISTENT,Block_size,
   602                               Block_offset}::rst),
   603               Ublocks=Unsynchronized.ref[]}) =
   604        (push ((if (!Block_size > sp_left)
   605                then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
   606                else FITS),
   607 	      the_indent_stack);
   608         Pblocks := rst)
   609   | print_BB(PPS{the_indent_stack,linewidth,space_left=Unsynchronized.ref sp_left,...},
   610              {Pblocks as Unsynchronized.ref({Block_size,Block_offset,...}::rst),Ublocks=Unsynchronized.ref[]}) =
   611        (push ((if (!Block_size > sp_left)
   612                then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
   613                else FITS),
   614 	      the_indent_stack);
   615         Pblocks := rst)
   616   | print_BB (PPS{the_indent_stack, linewidth, space_left=Unsynchronized.ref sp_left,...},
   617               {Ublocks,...}) =
   618       let fun pr_end_Ublock [{How_to_indent=CONSISTENT,Block_size,Block_offset}] l =
   619 		(push ((if (!Block_size > sp_left)
   620 			then ONE_PER_LINE (linewidth - (sp_left - Block_offset))
   621 			else FITS),
   622 		       the_indent_stack);
   623                  List.rev l)
   624 	    | pr_end_Ublock [{Block_size,Block_offset,...}] l =
   625 		(push ((if (!Block_size > sp_left)
   626 			then PACK_ONTO_LINE (linewidth - (sp_left - Block_offset))
   627 			else FITS),
   628 		       the_indent_stack);
   629                  List.rev l)
   630 	    | pr_end_Ublock (a::rst) l = pr_end_Ublock rst (a::l)
   631             | pr_end_Ublock _ _ =
   632                 raise Fail "PP-error: print_BB: internal error"
   633        in Ublocks := pr_end_Ublock(!Ublocks) []
   634       end
   635 
   636 
   637 (* Uend should always be 0 when print_E is called. *)
   638 fun print_E (_,{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
   639       raise Fail "PP-error: print_E"
   640   | print_E (istack,{Pend, ...}) =
   641       let fun pop_n_times 0 = ()
   642 	    | pop_n_times n = (pop istack; pop_n_times(n-1))
   643        in pop_n_times(!Pend); Pend := 0
   644       end
   645 
   646 
   647 (* "cursor" is how many spaces across the page we are. *)
   648 
   649 fun print_token(PPS{consumer,space_left,...}, S{String,Length}) =
   650       (consumer String;
   651        space_left := (!space_left) - Length)
   652   | print_token(ppstrm,BB b) = print_BB(ppstrm,b)
   653   | print_token(PPS{the_indent_stack,...},E e) =
   654       print_E (the_indent_stack,e)
   655   | print_token (PPS{the_indent_stack,space_left,consumer,linewidth,...},
   656                  BR{Distance_to_next_break,Number_of_blanks,Break_offset}) =
   657      (case (top the_indent_stack)
   658         of FITS =>
   659 	     (space_left := (!space_left) - Number_of_blanks;
   660               indent (consumer,Number_of_blanks))
   661          | (ONE_PER_LINE cursor) =>
   662              let val new_cursor = cursor + Break_offset
   663               in space_left := linewidth - new_cursor;
   664                  cr_indent (consumer,new_cursor)
   665 	     end
   666          | (PACK_ONTO_LINE cursor) =>
   667 	     if (!Distance_to_next_break > (!space_left))
   668 	     then let val new_cursor = cursor + Break_offset
   669 		   in space_left := linewidth - new_cursor;
   670 		      cr_indent(consumer,new_cursor)
   671 		  end
   672 	     else (space_left := !space_left - Number_of_blanks;
   673 		   indent (consumer,Number_of_blanks)))
   674 
   675 
   676 fun clear_ppstream(pps : ppstream) =
   677     let val PPS{the_token_buffer, the_delim_stack,
   678                 the_indent_stack,left_sum, right_sum,
   679                 left_index, right_index,space_left,linewidth,...}
   680               = magic pps
   681         val buf_size = 3*linewidth
   682 	fun set i =
   683 	    if (i = buf_size)
   684 	    then ()
   685 	    else (update(the_token_buffer,i,initial_token_value);
   686 		  set (i+1))
   687      in set 0;
   688 	clear_indent_stack the_indent_stack;
   689 	reset_delim_stack the_delim_stack;
   690 	left_sum := 0; right_sum := 0;
   691 	left_index := 0; right_index := 0;
   692 	space_left := linewidth
   693     end
   694 
   695 
   696 (* Move insertion head to right unless adding a BB and already at a BB,
   697    or unless adding an E and already at an E.
   698 *)
   699 fun BB_inc_right_index(PPS{the_token_buffer, right_index, ++,...})=
   700     case (the_token_buffer sub (!right_index))
   701       of (BB _) => ()
   702        | _ => ++right_index
   703 
   704 fun E_inc_right_index(PPS{the_token_buffer,right_index, ++,...})=
   705     case (the_token_buffer sub (!right_index))
   706       of (E _) => ()
   707        | _ => ++right_index
   708 
   709 
   710 fun pointers_coincide(PPS{left_index,right_index,the_token_buffer,...}) =
   711     (!left_index = !right_index) andalso
   712     (case (the_token_buffer sub (!left_index))
   713        of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) => true
   714 	| (BB _) => false
   715 	| (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) => true
   716 	| (E _) => false
   717 	| _ => true)
   718 
   719 fun advance_left (ppstrm as PPS{consumer,left_index,left_sum,
   720                                 the_token_buffer,++,...},
   721                   instr) =
   722     let val NEG = ~1
   723 	val POS = 0
   724 	fun inc_left_sum (BR{Number_of_blanks, ...}) =
   725 		 left_sum := (!left_sum) + Number_of_blanks
   726 	  | inc_left_sum (S{Length, ...}) = left_sum := (!left_sum) + Length
   727 	  | inc_left_sum _ = ()
   728 
   729 	fun last_size [{Block_size, ...}:block_info] = !Block_size
   730 	  | last_size (_::rst) = last_size rst
   731           | last_size _ = raise Fail "PP-error: last_size: internal error"
   732 	fun token_size (S{Length, ...}) = Length
   733 	  | token_size (BB b) =
   734 	     (case b
   735                 of {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []} =>
   736                      raise Fail "PP-error: BB_size"
   737 	         | {Pblocks as Unsynchronized.ref(_::_),Ublocks=Unsynchronized.ref[]} => POS
   738 		 | {Ublocks, ...} => last_size (!Ublocks))
   739 	  | token_size (E{Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =
   740               raise Fail "PP-error: token_size.E"
   741 	  | token_size (E{Pend = Unsynchronized.ref 0, ...}) = NEG
   742 	  | token_size (E _) = POS
   743 	  | token_size (BR {Distance_to_next_break, ...}) = !Distance_to_next_break
   744 	fun loop (instr) =
   745 	    if (token_size instr < 0)  (* synchronization point; cannot advance *)
   746 	    then ()
   747 	    else (print_token(ppstrm,instr);
   748 		  inc_left_sum instr;
   749 		  if (pointers_coincide ppstrm)
   750 		  then ()
   751 		  else (* increment left index *)
   752 
   753     (* When this is evaluated, we know that the left_index has not yet
   754        caught up to the right_index. If we are at a BB or an E, we can
   755        increment left_index if there is no work to be done, i.e., all Begins
   756        or Ends have been dealt with. Also, we should do some housekeeping and
   757        clear the buffer at left_index, otherwise we can get errors when
   758        left_index catches up to right_index and we reset the indices to 0.
   759        (We might find ourselves adding a BB to an "old" BB, with the result
   760        that the index is not pushed onto the delim_stack. This can lead to
   761        mangled output.)
   762     *)
   763 		       (case (the_token_buffer sub (!left_index))
   764 			  of (BB {Pblocks = Unsynchronized.ref [], Ublocks = Unsynchronized.ref []}) =>
   765 			       (update(the_token_buffer,!left_index,
   766 				       initial_token_value);
   767 				++left_index)
   768 			   | (BB _) => ()
   769 			   | (E {Pend = Unsynchronized.ref 0, Uend = Unsynchronized.ref 0}) =>
   770 			       (update(the_token_buffer,!left_index,
   771 				       initial_token_value);
   772 				++left_index)
   773 			   | (E _) => ()
   774 			   | _ => ++left_index;
   775 			loop (the_token_buffer sub (!left_index))))
   776      in loop instr
   777     end
   778 
   779 
   780 fun begin_block (pps : ppstream) style offset =
   781   let val ppstrm = magic pps : ppstream_
   782       val PPS{the_token_buffer, the_delim_stack,left_index,
   783               left_sum, right_index, right_sum,...}
   784             = ppstrm
   785   in
   786    (if (delim_stack_is_empty the_delim_stack)
   787     then (left_index := 0;
   788 	  left_sum := 1;
   789 	  right_index := 0;
   790 	  right_sum := 1)
   791     else BB_inc_right_index ppstrm;
   792     case (the_token_buffer sub (!right_index))
   793       of (BB {Ublocks, ...}) =>
   794 	   Ublocks := {Block_size = Unsynchronized.ref (~(!right_sum)),
   795 		       Block_offset = offset,
   796 		       How_to_indent = style}::(!Ublocks)
   797        | _ => (update(the_token_buffer, !right_index,
   798 		      BB{Pblocks = Unsynchronized.ref [],
   799 			 Ublocks = Unsynchronized.ref [{Block_size = Unsynchronized.ref (~(!right_sum)),
   800 					 Block_offset = offset,
   801 					 How_to_indent = style}]});
   802 	       push_delim_stack (!right_index, the_delim_stack)))
   803   end
   804 
   805 fun end_block(pps : ppstream) =
   806   let val ppstrm = magic pps : ppstream_
   807       val PPS{the_token_buffer,the_delim_stack,right_index,...}
   808             = ppstrm
   809   in
   810     if (delim_stack_is_empty the_delim_stack)
   811     then print_token(ppstrm,(E{Pend = Unsynchronized.ref 1, Uend = Unsynchronized.ref 0}))
   812     else (E_inc_right_index ppstrm;
   813 	  case (the_token_buffer sub (!right_index))
   814             of (E{Uend, ...}) => Uend := !Uend + 1
   815 	     | _ => (update(the_token_buffer,!right_index,
   816 			    E{Uend = Unsynchronized.ref 1, Pend = Unsynchronized.ref 0});
   817 		     push_delim_stack (!right_index, the_delim_stack)))
   818   end
   819 
   820 local
   821   fun check_delim_stack(PPS{the_token_buffer,the_delim_stack,right_sum,...}) =
   822       let fun check k =
   823 	      if (delim_stack_is_empty the_delim_stack)
   824 	      then ()
   825 	      else case(the_token_buffer sub (top_delim_stack the_delim_stack))
   826 		     of (BB{Ublocks as Unsynchronized.ref ((b as {Block_size, ...})::rst),
   827 			    Pblocks}) =>
   828 			   if (k>0)
   829 			   then (Block_size := !right_sum + !Block_size;
   830 				 Pblocks := b :: (!Pblocks);
   831 				 Ublocks := rst;
   832 				 if (List.length rst = 0)
   833 				 then pop_delim_stack the_delim_stack
   834 				 else ();
   835 				 check(k-1))
   836 			   else ()
   837 		      | (E{Pend,Uend}) =>
   838 			   (Pend := (!Pend) + (!Uend);
   839 			    Uend := 0;
   840 			    pop_delim_stack the_delim_stack;
   841 			    check(k + !Pend))
   842 		      | (BR{Distance_to_next_break, ...}) =>
   843 			   (Distance_to_next_break :=
   844 			      !right_sum + !Distance_to_next_break;
   845 			    pop_delim_stack the_delim_stack;
   846 			    if (k>0)
   847 			    then check k
   848 			    else ())
   849                       | _ => raise Fail "PP-error: check_delim_stack.catchall"
   850        in check 0
   851       end
   852 in
   853 
   854   fun add_break (pps : ppstream) (n, break_offset) =
   855     let val ppstrm = magic pps : ppstream_
   856         val PPS{the_token_buffer,the_delim_stack,left_index,
   857                 right_index,left_sum,right_sum, ++, ...}
   858               = ppstrm
   859     in
   860       (if (delim_stack_is_empty the_delim_stack)
   861        then (left_index := 0; right_index := 0;
   862 	     left_sum := 1;   right_sum := 1)
   863        else ++right_index;
   864        update(the_token_buffer, !right_index,
   865 	      BR{Distance_to_next_break = Unsynchronized.ref (~(!right_sum)),
   866 		 Number_of_blanks = n,
   867 		 Break_offset = break_offset});
   868        check_delim_stack ppstrm;
   869        right_sum := (!right_sum) + n;
   870        push_delim_stack (!right_index,the_delim_stack))
   871     end
   872 
   873   fun flush_ppstream0(pps : ppstream) =
   874     let val ppstrm = magic pps : ppstream_
   875         val PPS{the_delim_stack,the_token_buffer, flush, left_index,...}
   876               = ppstrm
   877     in
   878       (if (delim_stack_is_empty the_delim_stack)
   879        then ()
   880        else (check_delim_stack ppstrm;
   881 	     advance_left(ppstrm, the_token_buffer sub (!left_index)));
   882        flush())
   883     end
   884 
   885 end (* local *)
   886 
   887 
   888 fun flush_ppstream ppstrm =
   889     (flush_ppstream0 ppstrm;
   890      clear_ppstream ppstrm)
   891 
   892 fun add_string (pps : ppstream) s =
   893     let val ppstrm = magic pps : ppstream_
   894         val PPS{the_token_buffer,the_delim_stack,consumer,
   895                 right_index,right_sum,left_sum,
   896                 left_index,space_left,++,...}
   897               = ppstrm
   898         fun fnl [{Block_size, ...}:block_info] = Block_size := INFINITY
   899 	  | fnl (_::rst) = fnl rst
   900           | fnl _ = raise Fail "PP-error: fnl: internal error"
   901 
   902 	fun set(dstack,BB{Ublocks as Unsynchronized.ref[{Block_size,...}:block_info],...}) =
   903 	      (pop_bottom_delim_stack dstack;
   904 	       Block_size := INFINITY)
   905 	  | set (_,BB {Ublocks = Unsynchronized.ref(_::rst), ...}) = fnl rst
   906 	  | set (dstack, E{Pend,Uend}) =
   907 	      (Pend := (!Pend) + (!Uend);
   908 	       Uend := 0;
   909 	       pop_bottom_delim_stack dstack)
   910 	  | set (dstack,BR{Distance_to_next_break,...}) =
   911 	      (pop_bottom_delim_stack dstack;
   912 	       Distance_to_next_break := INFINITY)
   913           | set _ = raise (Fail "PP-error: add_string.set")
   914 
   915 	fun check_stream () =
   916 	    if ((!right_sum - !left_sum) > !space_left)
   917 	    then if (delim_stack_is_empty the_delim_stack)
   918 		 then ()
   919 		 else let val i = bottom_delim_stack the_delim_stack
   920 		       in if (!left_index = i)
   921 			  then set (the_delim_stack, the_token_buffer sub i)
   922 			  else ();
   923 			  advance_left(ppstrm,
   924                                        the_token_buffer sub (!left_index));
   925 		          if (pointers_coincide ppstrm)
   926 		          then ()
   927 		          else check_stream ()
   928 		      end
   929 	    else ()
   930 
   931 	val slen = String.size s
   932 	val S_token = S{String = s, Length = slen}
   933 
   934     in if (delim_stack_is_empty the_delim_stack)
   935        then print_token(ppstrm,S_token)
   936        else (++right_index;
   937              update(the_token_buffer, !right_index, S_token);
   938              right_sum := (!right_sum)+slen;
   939              check_stream ())
   940    end
   941 
   942 
   943 (* Derived form. The +2 is for peace of mind *)
   944 fun add_newline (pps : ppstream) =
   945   let val PPS{linewidth, ...} = magic pps
   946   in add_break pps (linewidth+2,0) end
   947 
   948 (* Derived form. Builds a ppstream, sends pretty printing commands called in
   949    f to the ppstream, then flushes ppstream.
   950 *)
   951 
   952 fun with_pp ppconsumer ppfn =
   953    let val ppstrm = mk_ppstream ppconsumer
   954     in ppfn ppstrm;
   955        flush_ppstream0 ppstrm
   956    end
   957    handle Fail msg =>
   958      (TextIO.print (">>>> Pretty-printer failure: " ^ msg ^ "\n"))
   959 
   960 fun pp_to_string linewidth ppfn ob =
   961     let val l = Unsynchronized.ref ([]:string list)
   962 	fun attach s = l := (s::(!l))
   963      in with_pp {consumer = attach, linewidth=linewidth, flush = fn()=>()}
   964 		(fn ppstrm =>  ppfn ppstrm ob);
   965 	String.concat(List.rev(!l))
   966     end
   967 end
   968 end;
   969 
   970 (**** Original file: Useful.sig ****)
   971 
   972 (* ========================================================================= *)
   973 (* ML UTILITY FUNCTIONS                                                      *)
   974 (* Copyright (c) 2001-2005 Joe Hurd, distributed under the BSD License *)
   975 (* ========================================================================= *)
   976 
   977 signature Useful =
   978 sig
   979 
   980 (* ------------------------------------------------------------------------- *)
   981 (* Exceptions.                                                               *)
   982 (* ------------------------------------------------------------------------- *)
   983 
   984 exception Error of string
   985 
   986 exception Bug of string
   987 
   988 val partial : exn -> ('a -> 'b option) -> 'a -> 'b
   989 
   990 val total : ('a -> 'b) -> 'a -> 'b option
   991 
   992 val can : ('a -> 'b) -> 'a -> bool
   993 
   994 (* ------------------------------------------------------------------------- *)
   995 (* Tracing.                                                                  *)
   996 (* ------------------------------------------------------------------------- *)
   997 
   998 val tracePrint : (string -> unit) Unsynchronized.ref
   999 
  1000 val trace : string -> unit
  1001 
  1002 (* ------------------------------------------------------------------------- *)
  1003 (* Combinators.                                                              *)
  1004 (* ------------------------------------------------------------------------- *)
  1005 
  1006 val C : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c
  1007 
  1008 val I : 'a -> 'a
  1009 
  1010 val K : 'a -> 'b -> 'a
  1011 
  1012 val S : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
  1013 
  1014 val W : ('a -> 'a -> 'b) -> 'a -> 'b
  1015 
  1016 val funpow : int -> ('a -> 'a) -> 'a -> 'a
  1017 
  1018 val exp : ('a * 'a -> 'a) -> 'a -> int -> 'a -> 'a
  1019 
  1020 val equal : ''a -> ''a -> bool
  1021 
  1022 val notEqual : ''a -> ''a -> bool
  1023 
  1024 (* ------------------------------------------------------------------------- *)
  1025 (* Pairs.                                                                    *)
  1026 (* ------------------------------------------------------------------------- *)
  1027 
  1028 val fst : 'a * 'b -> 'a
  1029 
  1030 val snd : 'a * 'b -> 'b
  1031 
  1032 val pair : 'a -> 'b -> 'a * 'b
  1033 
  1034 val swap : 'a * 'b -> 'b * 'a
  1035 
  1036 val curry : ('a * 'b -> 'c) -> 'a -> 'b -> 'c
  1037 
  1038 val uncurry : ('a -> 'b -> 'c) -> 'a * 'b -> 'c
  1039 
  1040 val ## : ('a -> 'c) * ('b -> 'd) -> 'a * 'b -> 'c * 'd
  1041 
  1042 (* ------------------------------------------------------------------------- *)
  1043 (* State transformers.                                                       *)
  1044 (* ------------------------------------------------------------------------- *)
  1045 
  1046 val unit : 'a -> 's -> 'a * 's
  1047 
  1048 val bind : ('s -> 'a * 's) -> ('a -> 's -> 'b * 's) -> 's -> 'b * 's
  1049 
  1050 val mmap : ('a -> 'b) -> ('s -> 'a * 's) -> 's -> 'b * 's
  1051 
  1052 val mjoin : ('s -> ('s -> 'a * 's) * 's) -> 's -> 'a * 's
  1053 
  1054 val mwhile : ('a -> bool) -> ('a -> 's -> 'a * 's) -> 'a -> 's -> 'a * 's
  1055 
  1056 (* ------------------------------------------------------------------------- *)
  1057 (* Lists: note we count elements from 0.                                     *)
  1058 (* ------------------------------------------------------------------------- *)
  1059 
  1060 val cons : 'a -> 'a list -> 'a list
  1061 
  1062 val hdTl : 'a list -> 'a * 'a list
  1063 
  1064 val append : 'a list -> 'a list -> 'a list
  1065 
  1066 val singleton : 'a -> 'a list
  1067 
  1068 val first : ('a -> 'b option) -> 'a list -> 'b option
  1069 
  1070 val index : ('a -> bool) -> 'a list -> int option
  1071 
  1072 val maps : ('a -> 's -> 'b * 's) -> 'a list -> 's -> 'b list * 's
  1073 
  1074 val mapsPartial : ('a -> 's -> 'b option * 's) -> 'a list -> 's -> 'b list * 's
  1075 
  1076 val enumerate : 'a list -> (int * 'a) list
  1077 
  1078 val zipwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
  1079 
  1080 val zip : 'a list -> 'b list -> ('a * 'b) list
  1081 
  1082 val unzip : ('a * 'b) list -> 'a list * 'b list
  1083 
  1084 val cartwith : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
  1085 
  1086 val cart : 'a list -> 'b list -> ('a * 'b) list
  1087 
  1088 val divide : 'a list -> int -> 'a list * 'a list  (* Subscript *)
  1089 
  1090 val revDivide : 'a list -> int -> 'a list * 'a list  (* Subscript *)
  1091 
  1092 val updateNth : int * 'a -> 'a list -> 'a list  (* Subscript *)
  1093 
  1094 val deleteNth : int -> 'a list -> 'a list  (* Subscript *)
  1095 
  1096 (* ------------------------------------------------------------------------- *)
  1097 (* Sets implemented with lists.                                              *)
  1098 (* ------------------------------------------------------------------------- *)
  1099 
  1100 val mem : ''a -> ''a list -> bool
  1101 
  1102 val insert : ''a -> ''a list -> ''a list
  1103 
  1104 val delete : ''a -> ''a list -> ''a list
  1105 
  1106 val setify : ''a list -> ''a list  (* removes duplicates *)
  1107 
  1108 val union : ''a list -> ''a list -> ''a list
  1109 
  1110 val intersect : ''a list -> ''a list -> ''a list
  1111 
  1112 val difference : ''a list -> ''a list -> ''a list
  1113 
  1114 val subset : ''a list -> ''a list -> bool
  1115 
  1116 val distinct : ''a list -> bool
  1117 
  1118 (* ------------------------------------------------------------------------- *)
  1119 (* Comparisons.                                                              *)
  1120 (* ------------------------------------------------------------------------- *)
  1121 
  1122 val mapCompare : ('a -> 'b) -> ('b * 'b -> order) -> 'a * 'a -> order
  1123 
  1124 val revCompare : ('a * 'a -> order) -> 'a * 'a -> order
  1125 
  1126 val prodCompare :
  1127     ('a * 'a -> order) -> ('b * 'b -> order) -> ('a * 'b) * ('a * 'b) -> order
  1128 
  1129 val lexCompare : ('a * 'a -> order) -> 'a list * 'a list -> order
  1130 
  1131 val optionCompare : ('a * 'a -> order) -> 'a option * 'a option -> order
  1132 
  1133 val boolCompare : bool * bool -> order  (* true < false *)
  1134 
  1135 (* ------------------------------------------------------------------------- *)
  1136 (* Sorting and searching.                                                    *)
  1137 (* ------------------------------------------------------------------------- *)
  1138 
  1139 val minimum : ('a * 'a -> order) -> 'a list -> 'a * 'a list  (* Empty *)
  1140 
  1141 val maximum : ('a * 'a -> order) -> 'a list -> 'a * 'a list  (* Empty *)
  1142 
  1143 val merge : ('a * 'a -> order) -> 'a list -> 'a list -> 'a list
  1144 
  1145 val sort : ('a * 'a -> order) -> 'a list -> 'a list
  1146 
  1147 val sortMap : ('a -> 'b) -> ('b * 'b -> order) -> 'a list -> 'a list
  1148 
  1149 (* ------------------------------------------------------------------------- *)
  1150 (* Integers.                                                                 *)
  1151 (* ------------------------------------------------------------------------- *)
  1152 
  1153 val interval : int -> int -> int list
  1154 
  1155 val divides : int -> int -> bool
  1156 
  1157 val gcd : int -> int -> int
  1158 
  1159 val primes : int -> int list
  1160 
  1161 val primesUpTo : int -> int list
  1162 
  1163 (* ------------------------------------------------------------------------- *)
  1164 (* Strings.                                                                  *)
  1165 (* ------------------------------------------------------------------------- *)
  1166 
  1167 val rot : int -> char -> char
  1168 
  1169 val charToInt : char -> int option
  1170 
  1171 val charFromInt : int -> char option
  1172 
  1173 val nChars : char -> int -> string
  1174 
  1175 val chomp : string -> string
  1176 
  1177 val trim : string -> string
  1178 
  1179 val join : string -> string list -> string
  1180 
  1181 val split : string -> string -> string list
  1182 
  1183 val mkPrefix : string -> string -> string
  1184 
  1185 val destPrefix : string -> string -> string
  1186 
  1187 val isPrefix : string -> string -> bool
  1188 
  1189 (* ------------------------------------------------------------------------- *)
  1190 (* Tables.                                                                   *)
  1191 (* ------------------------------------------------------------------------- *)
  1192 
  1193 type columnAlignment = {leftAlign : bool, padChar : char}
  1194 
  1195 val alignColumn : columnAlignment -> string list -> string list -> string list
  1196 
  1197 val alignTable : columnAlignment list -> string list list -> string list
  1198 
  1199 (* ------------------------------------------------------------------------- *)
  1200 (* Reals.                                                                    *)
  1201 (* ------------------------------------------------------------------------- *)
  1202 
  1203 val percentToString : real -> string
  1204 
  1205 val pos : real -> real
  1206 
  1207 val log2 : real -> real  (* Domain *)
  1208 
  1209 (* ------------------------------------------------------------------------- *)
  1210 (* Sum datatype.                                                             *)
  1211 (* ------------------------------------------------------------------------- *)
  1212 
  1213 datatype ('a,'b) sum = Left of 'a | Right of 'b
  1214 
  1215 val destLeft : ('a,'b) sum -> 'a
  1216 
  1217 val isLeft : ('a,'b) sum -> bool
  1218 
  1219 val destRight : ('a,'b) sum -> 'b
  1220 
  1221 val isRight : ('a,'b) sum -> bool
  1222 
  1223 (* ------------------------------------------------------------------------- *)
  1224 (* Useful impure features.                                                   *)
  1225 (* ------------------------------------------------------------------------- *)
  1226 
  1227 val newInt : unit -> int
  1228 
  1229 val newInts : int -> int list
  1230 
  1231 val withRef : 'r Unsynchronized.ref * 'r -> ('a -> 'b) -> 'a -> 'b
  1232 
  1233 val cloneArray : 'a Metis.Array.array -> 'a Metis.Array.array
  1234 
  1235 (* ------------------------------------------------------------------------- *)
  1236 (* The environment.                                                          *)
  1237 (* ------------------------------------------------------------------------- *)
  1238 
  1239 val host : unit -> string
  1240 
  1241 val time : unit -> string
  1242 
  1243 val date : unit -> string
  1244 
  1245 val readTextFile : {filename : string} -> string
  1246 
  1247 val writeTextFile : {filename : string, contents : string} -> unit
  1248 
  1249 (* ------------------------------------------------------------------------- *)
  1250 (* Profiling and error reporting.                                            *)
  1251 (* ------------------------------------------------------------------------- *)
  1252 
  1253 val try : ('a -> 'b) -> 'a -> 'b
  1254 
  1255 val warn : string -> unit
  1256 
  1257 val die : string -> 'exit
  1258 
  1259 val timed : ('a -> 'b) -> 'a -> real * 'b
  1260 
  1261 val timedMany : ('a -> 'b) -> 'a -> real * 'b
  1262 
  1263 val executionTime : unit -> real  (* Wall clock execution time *)
  1264 
  1265 end
  1266 
  1267 (**** Original file: Useful.sml ****)
  1268 
  1269 structure Metis = struct open Metis
  1270 (* Metis-specific ML environment *)
  1271 nonfix ++ -- RL mem union subset;
  1272 val explode = String.explode;
  1273 val implode = String.implode;
  1274 val print = TextIO.print;
  1275 (* ========================================================================= *)
  1276 (* ML UTILITY FUNCTIONS                                                      *)
  1277 (* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *)
  1278 (* ========================================================================= *)
  1279 
  1280 structure Useful :> Useful =
  1281 struct
  1282 
  1283 (* ------------------------------------------------------------------------- *)
  1284 (* Exceptions                                                                *)
  1285 (* ------------------------------------------------------------------------- *)
  1286 
  1287 exception Error of string;
  1288 
  1289 exception Bug of string;
  1290 
  1291 fun errorToString (Error message) = "\nError: " ^ message ^ "\n"
  1292   | errorToString _ = raise Bug "errorToString: not an Error exception";
  1293 
  1294 fun bugToString (Bug message) = "\nBug: " ^ message ^ "\n"
  1295   | bugToString _ = raise Bug "bugToString: not a Bug exception";
  1296 
  1297 fun total f x = SOME (f x) handle Error _ => NONE;
  1298 
  1299 fun can f = Option.isSome o total f;
  1300 
  1301 fun partial (e as Error _) f x = (case f x of SOME y => y | NONE => raise e)
  1302   | partial _ _ _ = raise Bug "partial: must take an Error exception";
  1303 
  1304 (* ------------------------------------------------------------------------- *)
  1305 (* Tracing                                                                   *)
  1306 (* ------------------------------------------------------------------------- *)
  1307 
  1308 val tracePrint = Unsynchronized.ref print;
  1309 
  1310 fun trace message = !tracePrint message;
  1311 
  1312 (* ------------------------------------------------------------------------- *)
  1313 (* Combinators                                                               *)
  1314 (* ------------------------------------------------------------------------- *)
  1315 
  1316 fun C f x y = f y x;
  1317 
  1318 fun I x = x;
  1319 
  1320 fun K x y = x;
  1321 
  1322 fun S f g x = f x (g x);
  1323 
  1324 fun W f x = f x x;
  1325 
  1326 fun funpow 0 _ x = x
  1327   | funpow n f x = funpow (n - 1) f (f x);
  1328 
  1329 fun exp m =
  1330     let
  1331       fun f _ 0 z = z
  1332         | f x y z = f (m (x,x)) (y div 2) (if y mod 2 = 0 then z else m (z,x))
  1333     in
  1334       f
  1335     end;
  1336 
  1337 val equal = fn x => fn y => x = y;
  1338 
  1339 val notEqual = fn x => fn y => x <> y;
  1340 
  1341 (* ------------------------------------------------------------------------- *)
  1342 (* Pairs                                                                     *)
  1343 (* ------------------------------------------------------------------------- *)
  1344 
  1345 fun fst (x,_) = x;
  1346 
  1347 fun snd (_,y) = y;
  1348 
  1349 fun pair x y = (x,y);
  1350 
  1351 fun swap (x,y) = (y,x);
  1352 
  1353 fun curry f x y = f (x,y);
  1354 
  1355 fun uncurry f (x,y) = f x y;
  1356 
  1357 val op## = fn (f,g) => fn (x,y) => (f x, g y);
  1358 
  1359 (* ------------------------------------------------------------------------- *)
  1360 (* State transformers                                                        *)
  1361 (* ------------------------------------------------------------------------- *)
  1362 
  1363 val unit : 'a -> 's -> 'a * 's = pair;
  1364 
  1365 fun bind f (g : 'a -> 's -> 'b * 's) = uncurry g o f;
  1366 
  1367 fun mmap f (m : 's -> 'a * 's) = bind m (unit o f);
  1368 
  1369 fun mjoin (f : 's -> ('s -> 'a * 's) * 's) = bind f I;
  1370 
  1371 fun mwhile c b = let fun f a = if c a then bind (b a) f else unit a in f end;
  1372 
  1373 (* ------------------------------------------------------------------------- *)
  1374 (* Lists                                                                     *)
  1375 (* ------------------------------------------------------------------------- *)
  1376 
  1377 fun cons x y = x :: y;
  1378 
  1379 fun hdTl l = (hd l, tl l);
  1380 
  1381 fun append xs ys = xs @ ys;
  1382 
  1383 fun singleton a = [a];
  1384 
  1385 fun first f [] = NONE
  1386   | first f (x :: xs) = (case f x of NONE => first f xs | s => s);
  1387 
  1388 fun index p =
  1389   let
  1390     fun idx _ [] = NONE
  1391       | idx n (x :: xs) = if p x then SOME n else idx (n + 1) xs
  1392   in
  1393     idx 0
  1394   end;
  1395 
  1396 fun maps (_ : 'a -> 's -> 'b * 's) [] = unit []
  1397   | maps f (x :: xs) =
  1398     bind (f x) (fn y => bind (maps f xs) (fn ys => unit (y :: ys)));
  1399 
  1400 fun mapsPartial (_ : 'a -> 's -> 'b option * 's) [] = unit []
  1401   | mapsPartial f (x :: xs) =
  1402     bind
  1403       (f x)
  1404       (fn yo =>
  1405           bind
  1406             (mapsPartial f xs)
  1407             (fn ys => unit (case yo of NONE => ys | SOME y => y :: ys)));
  1408 
  1409 fun enumerate l = fst (maps (fn x => fn m => ((m, x), m + 1)) l 0);
  1410 
  1411 fun zipwith f =
  1412     let
  1413       fun z l [] [] = l
  1414         | z l (x :: xs) (y :: ys) = z (f x y :: l) xs ys
  1415         | z _ _ _ = raise Error "zipwith: lists different lengths";
  1416     in
  1417       fn xs => fn ys => rev (z [] xs ys)
  1418     end;
  1419 
  1420 fun zip xs ys = zipwith pair xs ys;
  1421 
  1422 fun unzip ab =
  1423     foldl (fn ((x, y), (xs, ys)) => (x :: xs, y :: ys)) ([], []) (rev ab);
  1424 
  1425 fun cartwith f =
  1426   let
  1427     fun aux _ res _ [] = res
  1428       | aux xsCopy res [] (y :: yt) = aux xsCopy res xsCopy yt
  1429       | aux xsCopy res (x :: xt) (ys as y :: _) =
  1430         aux xsCopy (f x y :: res) xt ys
  1431   in
  1432     fn xs => fn ys =>
  1433     let val xs' = rev xs in aux xs' [] xs' (rev ys) end
  1434   end;
  1435 
  1436 fun cart xs ys = cartwith pair xs ys;
  1437 
  1438 local
  1439   fun revDiv acc l 0 = (acc,l)
  1440     | revDiv _ [] _ = raise Subscript
  1441     | revDiv acc (h :: t) n = revDiv (h :: acc) t (n - 1);
  1442 in
  1443   fun revDivide l = revDiv [] l;
  1444 end;
  1445 
  1446 fun divide l n = let val (a,b) = revDivide l n in (rev a, b) end;
  1447 
  1448 fun updateNth (n,x) l =
  1449     let
  1450       val (a,b) = revDivide l n
  1451     in
  1452       case b of [] => raise Subscript | _ :: t => List.revAppend (a, x :: t)
  1453     end;
  1454 
  1455 fun deleteNth n l =
  1456     let
  1457       val (a,b) = revDivide l n
  1458     in
  1459       case b of [] => raise Subscript | _ :: t => List.revAppend (a,t)
  1460     end;
  1461 
  1462 (* ------------------------------------------------------------------------- *)
  1463 (* Sets implemented with lists                                               *)
  1464 (* ------------------------------------------------------------------------- *)
  1465 
  1466 fun mem x = List.exists (equal x);
  1467 
  1468 fun insert x s = if mem x s then s else x :: s;
  1469 
  1470 fun delete x s = List.filter (not o equal x) s;
  1471 
  1472 fun setify s = rev (foldl (fn (v,x) => if mem v x then x else v :: x) [] s);
  1473 
  1474 fun union s t = foldl (fn (v,x) => if mem v t then x else v :: x) t (rev s);
  1475 
  1476 fun intersect s t =
  1477     foldl (fn (v,x) => if mem v t then v :: x else x) [] (rev s);
  1478 
  1479 fun difference s t =
  1480     foldl (fn (v,x) => if mem v t then x else v :: x) [] (rev s);
  1481 
  1482 fun subset s t = List.all (fn x => mem x t) s;
  1483 
  1484 fun distinct [] = true
  1485   | distinct (x :: rest) = not (mem x rest) andalso distinct rest;
  1486 
  1487 (* ------------------------------------------------------------------------- *)
  1488 (* Comparisons.                                                              *)
  1489 (* ------------------------------------------------------------------------- *)
  1490 
  1491 fun mapCompare f cmp (a,b) = cmp (f a, f b);
  1492 
  1493 fun revCompare cmp x_y =
  1494     case cmp x_y of LESS => GREATER | EQUAL => EQUAL | GREATER => LESS;
  1495 
  1496 fun prodCompare xCmp yCmp ((x1,y1),(x2,y2)) =
  1497     case xCmp (x1,x2) of
  1498       LESS => LESS
  1499     | EQUAL => yCmp (y1,y2)
  1500     | GREATER => GREATER;
  1501 
  1502 fun lexCompare cmp =
  1503     let
  1504       fun lex ([],[]) = EQUAL
  1505         | lex ([], _ :: _) = LESS
  1506         | lex (_ :: _, []) = GREATER
  1507         | lex (x :: xs, y :: ys) =
  1508           case cmp (x,y) of
  1509             LESS => LESS
  1510           | EQUAL => lex (xs,ys)
  1511           | GREATER => GREATER
  1512     in
  1513       lex
  1514     end;
  1515 
  1516 fun optionCompare _ (NONE,NONE) = EQUAL
  1517   | optionCompare _ (NONE,_) = LESS
  1518   | optionCompare _ (_,NONE) = GREATER
  1519   | optionCompare cmp (SOME x, SOME y) = cmp (x,y);
  1520 
  1521 fun boolCompare (true,false) = LESS
  1522   | boolCompare (false,true) = GREATER
  1523   | boolCompare _ = EQUAL;
  1524 
  1525 (* ------------------------------------------------------------------------- *)
  1526 (* Sorting and searching.                                                    *)
  1527 (* ------------------------------------------------------------------------- *)
  1528 
  1529 (* Finding the minimum and maximum element of a list, wrt some order. *)
  1530 
  1531 fun minimum cmp =
  1532     let
  1533       fun min (l,m,r) _ [] = (m, List.revAppend (l,r))
  1534         | min (best as (_,m,_)) l (x :: r) =
  1535           min (case cmp (x,m) of LESS => (l,x,r) | _ => best) (x :: l) r
  1536     in
  1537       fn [] => raise Empty
  1538        | h :: t => min ([],h,t) [h] t
  1539     end;
  1540 
  1541 fun maximum cmp = minimum (revCompare cmp);
  1542 
  1543 (* Merge (for the following merge-sort, but generally useful too). *)
  1544 
  1545 fun merge cmp =
  1546     let
  1547       fun mrg acc [] ys = List.revAppend (acc,ys)
  1548         | mrg acc xs [] = List.revAppend (acc,xs)
  1549         | mrg acc (xs as x :: xt) (ys as y :: yt) =
  1550           (case cmp (x,y) of
  1551              GREATER => mrg (y :: acc) xs yt
  1552            | _ => mrg (x :: acc) xt ys)
  1553     in
  1554       mrg []
  1555     end;
  1556 
  1557 (* Merge sort (stable). *)
  1558 
  1559 fun sort cmp =
  1560     let
  1561       fun findRuns acc r rs [] = rev (rev (r :: rs) :: acc)
  1562         | findRuns acc r rs (x :: xs) =
  1563           case cmp (r,x) of
  1564             GREATER => findRuns (rev (r :: rs) :: acc) x [] xs
  1565           | _ => findRuns acc x (r :: rs) xs
  1566 
  1567       fun mergeAdj acc [] = rev acc
  1568         | mergeAdj acc (xs as [_]) = List.revAppend (acc,xs)
  1569         | mergeAdj acc (x :: y :: xs) = mergeAdj (merge cmp x y :: acc) xs
  1570 
  1571       fun mergePairs [xs] = xs
  1572         | mergePairs l = mergePairs (mergeAdj [] l)
  1573     in
  1574       fn [] => []
  1575        | l as [_] => l
  1576        | h :: t => mergePairs (findRuns [] h [] t)
  1577     end;
  1578     
  1579 fun sortMap _ _ [] = []
  1580   | sortMap _ _ (l as [_]) = l
  1581   | sortMap f cmp xs =
  1582     let
  1583       fun ncmp ((m,_),(n,_)) = cmp (m,n)
  1584       val nxs = map (fn x => (f x, x)) xs
  1585       val nys = sort ncmp nxs
  1586     in
  1587       map snd nys
  1588     end;
  1589 
  1590 (* ------------------------------------------------------------------------- *)
  1591 (* Integers.                                                                 *)
  1592 (* ------------------------------------------------------------------------- *)
  1593 
  1594 fun interval m 0 = []
  1595   | interval m len = m :: interval (m + 1) (len - 1);
  1596 
  1597 fun divides _ 0 = true
  1598   | divides 0 _ = false
  1599   | divides a b = b mod (Int.abs a) = 0;
  1600 
  1601 local
  1602   fun hcf 0 n = n
  1603     | hcf 1 _ = 1
  1604     | hcf m n = hcf (n mod m) m;
  1605 in
  1606   fun gcd m n =
  1607       let
  1608         val m = Int.abs m
  1609         and n = Int.abs n
  1610       in
  1611         if m < n then hcf m n else hcf n m
  1612       end;
  1613 end;
  1614 
  1615 local
  1616   fun both f g n = f n andalso g n;
  1617 
  1618   fun next f = let fun nx x = if f x then x else nx (x + 1) in nx end;
  1619 
  1620   fun looking res 0 _ _ = rev res
  1621     | looking res n f x =
  1622       let
  1623         val p = next f x
  1624         val res' = p :: res
  1625         val f' = both f (not o divides p)
  1626       in
  1627         looking res' (n - 1) f' (p + 1)
  1628       end;
  1629 
  1630   fun calcPrimes n = looking [] n (K true) 2
  1631 
  1632   val primesList = Unsynchronized.ref (calcPrimes 10);
  1633 in
  1634   fun primes n = CRITICAL (fn () =>
  1635       if length (!primesList) <= n then List.take (!primesList,n)
  1636       else
  1637         let
  1638           val l = calcPrimes n
  1639           val () = primesList := l
  1640         in
  1641           l
  1642         end);
  1643 
  1644   fun primesUpTo n = CRITICAL (fn () =>
  1645       let
  1646         fun f k [] =
  1647             let
  1648               val l = calcPrimes (2 * k)
  1649               val () = primesList := l
  1650             in
  1651               f k (List.drop (l,k))
  1652             end
  1653           | f k (p :: ps) =
  1654             if p <= n then f (k + 1) ps else List.take (!primesList, k)
  1655       in
  1656         f 0 (!primesList)
  1657       end);
  1658 end;
  1659 
  1660 (* ------------------------------------------------------------------------- *)
  1661 (* Strings.                                                                  *)
  1662 (* ------------------------------------------------------------------------- *)
  1663 
  1664 local
  1665   fun len l = (length l, l)
  1666 
  1667   val upper = len (explode "ABCDEFGHIJKLMNOPQRSTUVWXYZ");
  1668 
  1669   val lower = len (explode "abcdefghijklmnopqrstuvwxyz");
  1670 
  1671   fun rotate (n,l) c k =
  1672       List.nth (l, (k + Option.valOf (index (equal c) l)) mod n);
  1673 in
  1674   fun rot k c =
  1675       if Char.isLower c then rotate lower c k
  1676       else if Char.isUpper c then rotate upper c k
  1677       else c;
  1678 end;
  1679 
  1680 fun charToInt #"0" = SOME 0
  1681   | charToInt #"1" = SOME 1
  1682   | charToInt #"2" = SOME 2
  1683   | charToInt #"3" = SOME 3
  1684   | charToInt #"4" = SOME 4
  1685   | charToInt #"5" = SOME 5
  1686   | charToInt #"6" = SOME 6
  1687   | charToInt #"7" = SOME 7
  1688   | charToInt #"8" = SOME 8
  1689   | charToInt #"9" = SOME 9
  1690   | charToInt _ = NONE;
  1691 
  1692 fun charFromInt 0 = SOME #"0"
  1693   | charFromInt 1 = SOME #"1"
  1694   | charFromInt 2 = SOME #"2"
  1695   | charFromInt 3 = SOME #"3"
  1696   | charFromInt 4 = SOME #"4"
  1697   | charFromInt 5 = SOME #"5"
  1698   | charFromInt 6 = SOME #"6"
  1699   | charFromInt 7 = SOME #"7"
  1700   | charFromInt 8 = SOME #"8"
  1701   | charFromInt 9 = SOME #"9"
  1702   | charFromInt _ = NONE;
  1703 
  1704 fun nChars x =
  1705     let
  1706       fun dup 0 l = l | dup n l = dup (n - 1) (x :: l)
  1707     in
  1708       fn n => implode (dup n [])
  1709     end;
  1710 
  1711 fun chomp s =
  1712     let
  1713       val n = size s
  1714     in
  1715       if n = 0 orelse String.sub (s, n - 1) <> #"\n" then s
  1716       else String.substring (s, 0, n - 1)
  1717     end;
  1718 
  1719 local
  1720   fun chop [] = []
  1721     | chop (l as (h :: t)) = if Char.isSpace h then chop t else l;
  1722 in
  1723   val trim = implode o chop o rev o chop o rev o explode;
  1724 end;
  1725 
  1726 fun join _ [] = "" | join s (h :: t) = foldl (fn (x,y) => y ^ s ^ x) h t;
  1727 
  1728 local
  1729   fun match [] l = SOME l
  1730     | match _ [] = NONE
  1731     | match (x :: xs) (y :: ys) = if x = y then match xs ys else NONE;
  1732 
  1733   fun stringify acc [] = acc
  1734     | stringify acc (h :: t) = stringify (implode h :: acc) t;
  1735 in
  1736   fun split sep =
  1737       let
  1738         val pat = String.explode sep
  1739         fun div1 prev recent [] = stringify [] (rev recent :: prev)
  1740           | div1 prev recent (l as h :: t) =
  1741             case match pat l of
  1742               NONE => div1 prev (h :: recent) t
  1743             | SOME rest => div1 (rev recent :: prev) [] rest
  1744       in
  1745         fn s => div1 [] [] (explode s)
  1746       end;
  1747 end;
  1748 
  1749 (***
  1750 fun pluralize {singular,plural} = fn 1 => singular | _ => plural;
  1751 ***)
  1752 
  1753 fun mkPrefix p s = p ^ s;
  1754 
  1755 fun destPrefix p =
  1756     let
  1757       fun check s = String.isPrefix p s orelse raise Error "destPrefix"
  1758 
  1759       val sizeP = size p
  1760     in
  1761       fn s => (check s; String.extract (s,sizeP,NONE))
  1762     end;
  1763 
  1764 fun isPrefix p = can (destPrefix p);
  1765 
  1766 (* ------------------------------------------------------------------------- *)
  1767 (* Tables.                                                                   *)
  1768 (* ------------------------------------------------------------------------- *)
  1769 
  1770 type columnAlignment = {leftAlign : bool, padChar : char}
  1771 
  1772 fun alignColumn {leftAlign,padChar} column =
  1773     let
  1774       val (n,_) = maximum Int.compare (map size column)
  1775 
  1776       fun pad entry row =
  1777           let
  1778             val padding = nChars padChar (n - size entry)
  1779           in
  1780             if leftAlign then entry ^ padding ^ row
  1781             else padding ^ entry ^ row
  1782           end
  1783     in
  1784       zipwith pad column
  1785     end;
  1786 
  1787 fun alignTable [] rows = map (K "") rows
  1788   | alignTable [{leftAlign = true, padChar = #" "}] rows = map hd rows
  1789   | alignTable (align :: aligns) rows =
  1790     alignColumn align (map hd rows) (alignTable aligns (map tl rows));
  1791 
  1792 (* ------------------------------------------------------------------------- *)
  1793 (* Reals.                                                                    *)
  1794 (* ------------------------------------------------------------------------- *)
  1795 
  1796 val realToString = Real.toString;
  1797 
  1798 fun percentToString x = Int.toString (Real.round (100.0 * x)) ^ "%";
  1799 
  1800 fun pos r = Real.max (r,0.0);
  1801 
  1802 local
  1803   val invLn2 = 1.0 / Math.ln 2.0;
  1804 in
  1805   fun log2 x = invLn2 * Math.ln x;
  1806 end;
  1807 
  1808 (* ------------------------------------------------------------------------- *)
  1809 (* Sums.                                                                     *)
  1810 (* ------------------------------------------------------------------------- *)
  1811 
  1812 datatype ('a,'b) sum = Left of 'a | Right of 'b
  1813 
  1814 fun destLeft (Left l) = l
  1815   | destLeft _ = raise Error "destLeft";
  1816 
  1817 fun isLeft (Left _) = true
  1818   | isLeft (Right _) = false;
  1819 
  1820 fun destRight (Right r) = r
  1821   | destRight _ = raise Error "destRight";
  1822 
  1823 fun isRight (Left _) = false
  1824   | isRight (Right _) = true;
  1825 
  1826 (* ------------------------------------------------------------------------- *)
  1827 (* Useful impure features.                                                   *)
  1828 (* ------------------------------------------------------------------------- *)
  1829 
  1830 local
  1831   val generator = Unsynchronized.ref 0
  1832 in
  1833   fun newInt () = CRITICAL (fn () =>
  1834       let
  1835         val n = !generator
  1836         val () = generator := n + 1
  1837       in
  1838         n
  1839       end);
  1840 
  1841   fun newInts 0 = []
  1842     | newInts k = CRITICAL (fn () =>
  1843       let
  1844         val n = !generator
  1845         val () = generator := n + k
  1846       in
  1847         interval n k
  1848       end);
  1849 end;
  1850 
  1851 fun withRef (r,new) f x =
  1852   let
  1853     val old = !r
  1854     val () = r := new
  1855     val y = f x handle e => (r := old; raise e)
  1856     val () = r := old
  1857   in
  1858     y
  1859   end;
  1860 
  1861 fun cloneArray a =
  1862     let
  1863       fun index i = Array.sub (a,i)
  1864     in
  1865       Array.tabulate (Array.length a, index)
  1866     end;
  1867 
  1868 (* ------------------------------------------------------------------------- *)
  1869 (* Environment.                                                              *)
  1870 (* ------------------------------------------------------------------------- *)
  1871 
  1872 fun host () = Option.getOpt (OS.Process.getEnv "HOSTNAME", "unknown");
  1873 
  1874 fun time () = Date.fmt "%H:%M:%S" (Date.fromTimeLocal (Time.now ()));
  1875 
  1876 fun date () = Date.fmt "%d/%m/%Y" (Date.fromTimeLocal (Time.now ()));
  1877 
  1878 fun readTextFile {filename} =
  1879   let
  1880     open TextIO
  1881     val h = openIn filename
  1882     val contents = inputAll h
  1883     val () = closeIn h
  1884   in
  1885     contents
  1886   end;
  1887 
  1888 fun writeTextFile {filename,contents} =
  1889   let
  1890     open TextIO
  1891     val h = openOut filename
  1892     val () = output (h,contents)
  1893     val () = closeOut h
  1894   in
  1895     ()
  1896   end;
  1897 
  1898 (* ------------------------------------------------------------------------- *)
  1899 (* Profiling                                                                 *)
  1900 (* ------------------------------------------------------------------------- *)
  1901 
  1902 local
  1903   fun err x s = TextIO.output (TextIO.stdErr, x ^ ": " ^ s ^ "\n");
  1904 in
  1905   fun try f x = f x
  1906       handle e as Error _ => (err "try" (errorToString e); raise e)
  1907            | e as Bug _ => (err "try" (bugToString e); raise e)
  1908            | e => (err "try" "strange exception raised"; raise e);
  1909 
  1910   val warn = err "WARNING";
  1911 
  1912   fun die s = (err "\nFATAL ERROR" s; OS.Process.exit OS.Process.failure);
  1913 end;
  1914 
  1915 fun timed f a =
  1916   let
  1917     val tmr = Timer.startCPUTimer ()
  1918     val res = f a
  1919     val {usr,sys,...} = Timer.checkCPUTimer tmr
  1920   in
  1921     (Time.toReal usr + Time.toReal sys, res)
  1922   end;
  1923 
  1924 local
  1925   val MIN = 1.0;
  1926 
  1927   fun several n t f a =
  1928     let
  1929       val (t',res) = timed f a
  1930       val t = t + t'
  1931       val n = n + 1
  1932     in
  1933       if t > MIN then (t / Real.fromInt n, res) else several n t f a
  1934     end;
  1935 in
  1936   fun timedMany f a = several 0 0.0 f a
  1937 end;
  1938 
  1939 val executionTime =
  1940     let
  1941       val startTime = Time.toReal (Time.now ())
  1942     in
  1943       fn () => Time.toReal (Time.now ()) - startTime
  1944     end;
  1945 
  1946 end
  1947 end;
  1948 
  1949 (**** Original file: Lazy.sig ****)
  1950 
  1951 (* ========================================================================= *)
  1952 (* SUPPORT FOR LAZY EVALUATION                                               *)
  1953 (* Copyright (c) 2007 Joe Hurd, distributed under the BSD License      *)
  1954 (* ========================================================================= *)
  1955 
  1956 signature Lazy =
  1957 sig
  1958 
  1959 type 'a lazy
  1960 
  1961 val delay : (unit -> 'a) -> 'a lazy
  1962 
  1963 val force : 'a lazy -> 'a
  1964 
  1965 val memoize : (unit -> 'a) -> unit -> 'a
  1966 
  1967 end
  1968 
  1969 (**** Original file: Lazy.sml ****)
  1970 
  1971 structure Metis = struct open Metis
  1972 (* Metis-specific ML environment *)
  1973 nonfix ++ -- RL mem union subset;
  1974 val explode = String.explode;
  1975 val implode = String.implode;
  1976 val print = TextIO.print;
  1977 (* ========================================================================= *)
  1978 (* SUPPORT FOR LAZY EVALUATION                                               *)
  1979 (* Copyright (c) 2007 Joe Hurd, distributed under the BSD License      *)
  1980 (* ========================================================================= *)
  1981 
  1982 structure Lazy :> Lazy =
  1983 struct
  1984 
  1985 datatype 'a thunk =
  1986     Value of 'a
  1987   | Thunk of unit -> 'a;
  1988 
  1989 datatype 'a lazy = Lazy of 'a thunk Unsynchronized.ref;
  1990 
  1991 fun delay f = Lazy (Unsynchronized.ref (Thunk f));
  1992 
  1993 fun force (Lazy (Unsynchronized.ref (Value v))) = v
  1994   | force (Lazy (s as Unsynchronized.ref (Thunk f))) =
  1995     let
  1996       val v = f ()
  1997       val () = s := Value v
  1998     in
  1999       v
  2000     end;
  2001 
  2002 fun memoize f =
  2003     let
  2004       val t = delay f
  2005     in
  2006       fn () => force t
  2007     end;
  2008 
  2009 end
  2010 end;
  2011 
  2012 (**** Original file: Ordered.sig ****)
  2013 
  2014 (* ========================================================================= *)
  2015 (* ORDERED TYPES                                                             *)
  2016 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  2017 (* ========================================================================= *)
  2018 
  2019 signature Ordered =
  2020 sig
  2021 
  2022 type t
  2023 
  2024 val compare : t * t -> order
  2025 
  2026 (*
  2027   PROVIDES
  2028 
  2029   !x : t. compare (x,x) = EQUAL
  2030 
  2031   !x y : t. compare (x,y) = LESS <=> compare (y,x) = GREATER
  2032 
  2033   !x y : t. compare (x,y) = EQUAL ==> compare (y,x) = EQUAL
  2034 
  2035   !x y z : t. compare (x,y) = EQUAL ==> compare (x,z) = compare (y,z)
  2036 
  2037   !x y z : t.
  2038     compare (x,y) = LESS andalso compare (y,z) = LESS ==>
  2039     compare (x,z) = LESS
  2040 
  2041   !x y z : t.
  2042     compare (x,y) = GREATER andalso compare (y,z) = GREATER ==>
  2043     compare (x,z) = GREATER
  2044 *)
  2045 
  2046 end
  2047 
  2048 (**** Original file: Ordered.sml ****)
  2049 
  2050 structure Metis = struct open Metis
  2051 (* Metis-specific ML environment *)
  2052 nonfix ++ -- RL mem union subset;
  2053 val explode = String.explode;
  2054 val implode = String.implode;
  2055 val print = TextIO.print;
  2056 (* ========================================================================= *)
  2057 (* ORDERED TYPES                                                             *)
  2058 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  2059 (* ========================================================================= *)
  2060 
  2061 structure IntOrdered =
  2062 struct type t = int val compare = Int.compare end;
  2063 
  2064 structure StringOrdered =
  2065 struct type t = string val compare = String.compare end;
  2066 end;
  2067 
  2068 (**** Original file: Set.sig ****)
  2069 
  2070 (* ========================================================================= *)
  2071 (* FINITE SETS                                                               *)
  2072 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  2073 (* ========================================================================= *)
  2074 
  2075 signature Set =
  2076 sig
  2077 
  2078 (* ------------------------------------------------------------------------- *)
  2079 (* Finite sets                                                               *)
  2080 (* ------------------------------------------------------------------------- *)
  2081 
  2082 type 'elt set
  2083 
  2084 val comparison : 'elt set -> ('elt * 'elt -> order)
  2085 
  2086 val empty : ('elt * 'elt -> order) -> 'elt set
  2087 
  2088 val singleton : ('elt * 'elt -> order) -> 'elt -> 'elt set
  2089 
  2090 val null : 'elt set -> bool
  2091 
  2092 val size : 'elt set -> int
  2093 
  2094 val member : 'elt -> 'elt set -> bool
  2095 
  2096 val add : 'elt set -> 'elt -> 'elt set
  2097 
  2098 val addList : 'elt set -> 'elt list -> 'elt set
  2099 
  2100 val delete : 'elt set -> 'elt -> 'elt set  (* raises Error *)
  2101 
  2102 (* Union and intersect prefer elements in the second set *)
  2103 
  2104 val union : 'elt set -> 'elt set -> 'elt set
  2105 
  2106 val unionList : 'elt set list -> 'elt set
  2107 
  2108 val intersect : 'elt set -> 'elt set -> 'elt set
  2109 
  2110 val intersectList : 'elt set list -> 'elt set
  2111 
  2112 val difference : 'elt set -> 'elt set -> 'elt set
  2113 
  2114 val symmetricDifference : 'elt set -> 'elt set -> 'elt set
  2115 
  2116 val disjoint : 'elt set -> 'elt set -> bool
  2117 
  2118 val subset : 'elt set -> 'elt set -> bool
  2119 
  2120 val equal : 'elt set -> 'elt set -> bool
  2121 
  2122 val filter : ('elt -> bool) -> 'elt set -> 'elt set
  2123 
  2124 val partition : ('elt -> bool) -> 'elt set -> 'elt set * 'elt set
  2125 
  2126 val count : ('elt -> bool) -> 'elt set -> int
  2127 
  2128 val foldl : ('elt * 's -> 's) -> 's -> 'elt set -> 's
  2129 
  2130 val foldr : ('elt * 's -> 's) -> 's -> 'elt set -> 's
  2131 
  2132 val findl : ('elt -> bool) -> 'elt set -> 'elt option
  2133 
  2134 val findr : ('elt -> bool) -> 'elt set -> 'elt option
  2135 
  2136 val firstl : ('elt -> 'a option) -> 'elt set -> 'a option
  2137 
  2138 val firstr : ('elt -> 'a option) -> 'elt set -> 'a option
  2139 
  2140 val exists : ('elt -> bool) -> 'elt set -> bool
  2141 
  2142 val all : ('elt -> bool) -> 'elt set -> bool
  2143 
  2144 val map : ('elt -> 'a) -> 'elt set -> ('elt * 'a) list
  2145 
  2146 val transform : ('elt -> 'a) -> 'elt set -> 'a list
  2147 
  2148 val app : ('elt -> unit) -> 'elt set -> unit
  2149 
  2150 val toList : 'elt set -> 'elt list
  2151 
  2152 val fromList : ('elt * 'elt -> order) -> 'elt list -> 'elt set
  2153 
  2154 val pick : 'elt set -> 'elt  (* raises Empty *)
  2155 
  2156 val random : 'elt set -> 'elt  (* raises Empty *)
  2157 
  2158 val deletePick : 'elt set -> 'elt * 'elt set  (* raises Empty *)
  2159 
  2160 val deleteRandom : 'elt set -> 'elt * 'elt set  (* raises Empty *)
  2161 
  2162 val compare : 'elt set * 'elt set -> order
  2163 
  2164 val close : ('elt set -> 'elt set) -> 'elt set -> 'elt set
  2165 
  2166 val toString : 'elt set -> string
  2167 
  2168 (* ------------------------------------------------------------------------- *)
  2169 (* Iterators over sets                                                       *)
  2170 (* ------------------------------------------------------------------------- *)
  2171 
  2172 type 'elt iterator
  2173 
  2174 val mkIterator : 'elt set -> 'elt iterator option
  2175 
  2176 val mkRevIterator : 'elt set -> 'elt iterator option
  2177 
  2178 val readIterator : 'elt iterator -> 'elt
  2179 
  2180 val advanceIterator : 'elt iterator -> 'elt iterator option
  2181 
  2182 end
  2183 
  2184 (**** Original file: RandomSet.sml ****)
  2185 
  2186 structure Metis = struct open Metis
  2187 (* Metis-specific ML environment *)
  2188 nonfix ++ -- RL mem union subset;
  2189 val explode = String.explode;
  2190 val implode = String.implode;
  2191 val print = TextIO.print;
  2192 (* ========================================================================= *)
  2193 (* FINITE SETS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
  2194 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  2195 (* ========================================================================= *)
  2196 
  2197 structure RandomSet :> Set =
  2198 struct
  2199 
  2200 exception Bug = Useful.Bug;
  2201 
  2202 exception Error = Useful.Error;
  2203 
  2204 val pointerEqual = Portable.pointerEqual;
  2205 
  2206 val K = Useful.K;
  2207 
  2208 val snd = Useful.snd;
  2209 
  2210 val randomInt = Portable.randomInt;
  2211 
  2212 val randomWord = Portable.randomWord;
  2213 
  2214 (* ------------------------------------------------------------------------- *)
  2215 (* Random search trees.                                                      *)
  2216 (* ------------------------------------------------------------------------- *)
  2217 
  2218 type priority = Word.word;
  2219 
  2220 datatype 'a tree =
  2221     E
  2222   | T of
  2223     {size : int,
  2224      priority : priority,
  2225      left : 'a tree,
  2226      key : 'a,
  2227      right : 'a tree};
  2228     
  2229 type 'a node =
  2230      {size : int,
  2231       priority : priority,
  2232       left : 'a tree,
  2233       key : 'a,
  2234       right : 'a tree};
  2235 
  2236 datatype 'a set = Set of ('a * 'a -> order) * 'a tree;
  2237 
  2238 (* ------------------------------------------------------------------------- *)
  2239 (* Random priorities.                                                        *)
  2240 (* ------------------------------------------------------------------------- *)
  2241 
  2242 local
  2243   val randomPriority = randomWord;
  2244 
  2245   val priorityOrder = Word.compare;
  2246 in
  2247   fun treeSingleton key =
  2248       T {size = 1, priority = randomPriority (),
  2249          left = E, key = key, right = E};
  2250 
  2251   fun nodePriorityOrder cmp (x1 : 'a node, x2 : 'a node) =
  2252       let
  2253         val {priority = p1, key = k1, ...} = x1
  2254         and {priority = p2, key = k2, ...} = x2
  2255       in
  2256         case priorityOrder (p1,p2) of
  2257           LESS => LESS
  2258         | EQUAL => cmp (k1,k2)
  2259         | GREATER => GREATER
  2260       end;
  2261 end;
  2262 
  2263 (* ------------------------------------------------------------------------- *)
  2264 (* Debugging functions.                                                      *)
  2265 (* ------------------------------------------------------------------------- *)
  2266 
  2267 local
  2268   fun checkSizes E = 0
  2269     | checkSizes (T {size,left,right,...}) =
  2270       let
  2271         val l = checkSizes left
  2272         and r = checkSizes right
  2273         val () = if l + 1 + r = size then () else raise Error "wrong size"
  2274       in
  2275         size
  2276       end
  2277 
  2278   fun checkSorted _ x E = x
  2279     | checkSorted cmp x (T {left,key,right,...}) =
  2280       let
  2281         val x = checkSorted cmp x left
  2282         val () =
  2283             case x of
  2284               NONE => ()
  2285             | SOME k =>
  2286               case cmp (k,key) of
  2287                 LESS => ()
  2288               | EQUAL => raise Error "duplicate keys"
  2289               | GREATER => raise Error "unsorted"
  2290       in
  2291         checkSorted cmp (SOME key) right
  2292       end;
  2293 
  2294   fun checkPriorities _ E = NONE
  2295     | checkPriorities cmp (T (x as {left,right,...})) =
  2296       let
  2297         val () =
  2298             case checkPriorities cmp left of
  2299               NONE => ()
  2300             | SOME l =>
  2301               case nodePriorityOrder cmp (l,x) of
  2302                 LESS => ()
  2303               | EQUAL => raise Error "left child has equal key"
  2304               | GREATER => raise Error "left child has greater priority"
  2305         val () =
  2306             case checkPriorities cmp right of
  2307               NONE => ()
  2308             | SOME r =>
  2309               case nodePriorityOrder cmp (r,x) of
  2310                 LESS => ()
  2311               | EQUAL => raise Error "right child has equal key"
  2312               | GREATER => raise Error "right child has greater priority"
  2313       in
  2314         SOME x
  2315       end;
  2316 in
  2317   fun checkWellformed s (set as Set (cmp,tree)) =
  2318       (let
  2319          val _ = checkSizes tree
  2320          val _ = checkSorted cmp NONE tree
  2321          val _ = checkPriorities cmp tree
  2322        in
  2323          set
  2324        end
  2325        handle Error err => raise Bug err)
  2326       handle Bug bug => raise Bug (s ^ "\nRandomSet.checkWellformed: " ^ bug);
  2327 end;
  2328 
  2329 (* ------------------------------------------------------------------------- *)
  2330 (* Basic operations.                                                         *)
  2331 (* ------------------------------------------------------------------------- *)
  2332 
  2333 fun comparison (Set (cmp,_)) = cmp;
  2334 
  2335 fun empty cmp = Set (cmp,E);
  2336 
  2337 fun treeSize E = 0
  2338   | treeSize (T {size = s, ...}) = s;
  2339 
  2340 fun size (Set (_,tree)) = treeSize tree;
  2341 
  2342 fun mkT p l k r =
  2343     T {size = treeSize l + 1 + treeSize r, priority = p,
  2344        left = l, key = k, right = r};
  2345 
  2346 fun singleton cmp key = Set (cmp, treeSingleton key);
  2347 
  2348 local
  2349   fun treePeek cmp E pkey = NONE
  2350     | treePeek cmp (T {left,key,right,...}) pkey =
  2351       case cmp (pkey,key) of
  2352         LESS => treePeek cmp left pkey
  2353       | EQUAL => SOME key
  2354       | GREATER => treePeek cmp right pkey
  2355 in
  2356   fun peek (Set (cmp,tree)) key = treePeek cmp tree key;
  2357 end;
  2358 
  2359 (* treeAppend assumes that every element of the first tree is less than *)
  2360 (* every element of the second tree. *)
  2361 
  2362 fun treeAppend _ t1 E = t1
  2363   | treeAppend _ E t2 = t2
  2364   | treeAppend cmp (t1 as T x1) (t2 as T x2) =
  2365     case nodePriorityOrder cmp (x1,x2) of
  2366       LESS =>
  2367       let
  2368         val {priority = p2, left = l2, key = k2, right = r2, ...} = x2
  2369       in
  2370         mkT p2 (treeAppend cmp t1 l2) k2 r2
  2371       end
  2372     | EQUAL => raise Bug "RandomSet.treeAppend: equal keys"
  2373     | GREATER =>
  2374       let
  2375         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
  2376       in
  2377         mkT p1 l1 k1 (treeAppend cmp r1 t2)
  2378       end;
  2379 
  2380 (* nodePartition splits the node into three parts: the keys comparing less *)
  2381 (* than the supplied key, an optional equal key, and the keys comparing *)
  2382 (* greater. *)
  2383 
  2384 local
  2385   fun mkLeft [] t = t
  2386     | mkLeft (({priority,left,key,...} : 'a node) :: xs) t =
  2387       mkLeft xs (mkT priority left key t);
  2388 
  2389   fun mkRight [] t = t
  2390     | mkRight (({priority,key,right,...} : 'a node) :: xs) t =
  2391       mkRight xs (mkT priority t key right);
  2392 
  2393   fun treePart _ _ lefts rights E = (mkLeft lefts E, NONE, mkRight rights E)
  2394     | treePart cmp pkey lefts rights (T x) = nodePart cmp pkey lefts rights x
  2395   and nodePart cmp pkey lefts rights (x as {left,key,right,...}) =
  2396       case cmp (pkey,key) of
  2397         LESS => treePart cmp pkey lefts (x :: rights) left
  2398       | EQUAL => (mkLeft lefts left, SOME key, mkRight rights right)
  2399       | GREATER => treePart cmp pkey (x :: lefts) rights right;
  2400 in
  2401   fun nodePartition cmp x pkey = nodePart cmp pkey [] [] x;
  2402 end;
  2403 
  2404 (* union first calls treeCombineRemove, to combine the values *)
  2405 (* for equal keys into the first map and remove them from the second map. *)
  2406 (* Note that the combined key is always the one from the second map. *)
  2407 
  2408 local
  2409   fun treeCombineRemove _ t1 E = (t1,E)
  2410     | treeCombineRemove _ E t2 = (E,t2)
  2411     | treeCombineRemove cmp (t1 as T x1) (t2 as T x2) =
  2412       let
  2413         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
  2414         val (l2,k2,r2) = nodePartition cmp x2 k1
  2415         val (l1,l2) = treeCombineRemove cmp l1 l2
  2416         and (r1,r2) = treeCombineRemove cmp r1 r2
  2417       in
  2418         case k2 of
  2419           NONE => if treeSize l2 + treeSize r2 = #size x2 then (t1,t2)
  2420                   else (mkT p1 l1 k1 r1, treeAppend cmp l2 r2)
  2421         | SOME k2 => (mkT p1 l1 k2 r1, treeAppend cmp l2 r2)
  2422       end;
  2423 
  2424   fun treeUnionDisjoint _ t1 E = t1
  2425     | treeUnionDisjoint _ E t2 = t2
  2426     | treeUnionDisjoint cmp (T x1) (T x2) =
  2427       case nodePriorityOrder cmp (x1,x2) of
  2428         LESS => nodeUnionDisjoint cmp x2 x1
  2429       | EQUAL => raise Bug "RandomSet.unionDisjoint: equal keys"
  2430       | GREATER => nodeUnionDisjoint cmp x1 x2
  2431 
  2432   and nodeUnionDisjoint cmp x1 x2 =
  2433       let
  2434         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
  2435         val (l2,_,r2) = nodePartition cmp x2 k1
  2436         val l = treeUnionDisjoint cmp l1 l2
  2437         and r = treeUnionDisjoint cmp r1 r2
  2438       in
  2439         mkT p1 l k1 r
  2440       end;
  2441 in
  2442   fun union (s1 as Set (cmp,t1)) (Set (_,t2)) =
  2443       if pointerEqual (t1,t2) then s1
  2444       else
  2445         let
  2446           val (t1,t2) = treeCombineRemove cmp t1 t2
  2447         in
  2448           Set (cmp, treeUnionDisjoint cmp t1 t2)
  2449         end;
  2450 end;
  2451 
  2452 (*DEBUG
  2453 val union = fn t1 => fn t2 =>
  2454     checkWellformed "RandomSet.union: result"
  2455       (union (checkWellformed "RandomSet.union: input 1" t1)
  2456              (checkWellformed "RandomSet.union: input 2" t2));
  2457 *)
  2458 
  2459 (* intersect is a simple case of the union algorithm. *)
  2460 
  2461 local
  2462   fun treeIntersect _ _ E = E
  2463     | treeIntersect _ E _ = E
  2464     | treeIntersect cmp (t1 as T x1) (t2 as T x2) =
  2465       let
  2466         val {priority = p1, left = l1, key = k1, right = r1, ...} = x1
  2467         val (l2,k2,r2) = nodePartition cmp x2 k1
  2468         val l = treeIntersect cmp l1 l2
  2469         and r = treeIntersect cmp r1 r2
  2470       in
  2471         case k2 of
  2472           NONE => treeAppend cmp l r
  2473         | SOME k2 => mkT p1 l k2 r
  2474       end;
  2475 in
  2476   fun intersect (s1 as Set (cmp,t1)) (Set (_,t2)) =
  2477       if pointerEqual (t1,t2) then s1
  2478       else Set (cmp, treeIntersect cmp t1 t2);
  2479 end;
  2480 
  2481 (*DEBUG
  2482 val intersect = fn t1 => fn t2 =>
  2483     checkWellformed "RandomSet.intersect: result"
  2484       (intersect (checkWellformed "RandomSet.intersect: input 1" t1)
  2485                  (checkWellformed "RandomSet.intersect: input 2" t2));
  2486 *)
  2487 
  2488 (* delete raises an exception if the supplied key is not found, which *)
  2489 (* makes it simpler to maximize sharing. *)
  2490 
  2491 local
  2492   fun treeDelete _ E _ = raise Error "RandomSet.delete: element not found"
  2493     | treeDelete cmp (T {priority,left,key,right,...}) dkey =
  2494       case cmp (dkey,key) of
  2495         LESS => mkT priority (treeDelete cmp left dkey) key right
  2496       | EQUAL => treeAppend cmp left right
  2497       | GREATER => mkT priority left key (treeDelete cmp right dkey);
  2498 in
  2499   fun delete (Set (cmp,tree)) key = Set (cmp, treeDelete cmp tree key);
  2500 end;
  2501  
  2502 (*DEBUG
  2503 val delete = fn t => fn x =>
  2504     checkWellformed "RandomSet.delete: result"
  2505       (delete (checkWellformed "RandomSet.delete: input" t) x);
  2506 *)
  2507 
  2508 (* Set difference *)
  2509 
  2510 local
  2511   fun treeDifference _ t1 E = t1
  2512     | treeDifference _ E _ = E
  2513     | treeDifference cmp (t1 as T x1) (T x2) =
  2514       let
  2515         val {size = s1, priority = p1, left = l1, key = k1, right = r1} = x1
  2516         val (l2,k2,r2) = nodePartition cmp x2 k1
  2517         val l = treeDifference cmp l1 l2
  2518         and r = treeDifference cmp r1 r2
  2519       in
  2520         if Option.isSome k2 then treeAppend cmp l r
  2521         else if treeSize l + treeSize r + 1 = s1 then t1
  2522         else mkT p1 l k1 r
  2523       end;
  2524 in
  2525   fun difference (Set (cmp,tree1)) (Set (_,tree2)) =
  2526       if pointerEqual (tree1,tree2) then Set (cmp,E)
  2527       else Set (cmp, treeDifference cmp tree1 tree2);
  2528 end;
  2529 
  2530 (*DEBUG
  2531 val difference = fn t1 => fn t2 =>
  2532     checkWellformed "RandomSet.difference: result"
  2533       (difference (checkWellformed "RandomSet.difference: input 1" t1)
  2534                   (checkWellformed "RandomSet.difference: input 2" t2));
  2535 *)
  2536 
  2537 (* Subsets *)
  2538 
  2539 local
  2540   fun treeSubset _ E _ = true
  2541     | treeSubset _ _ E = false
  2542     | treeSubset cmp (t1 as T x1) (T x2) =
  2543       let
  2544         val {size = s1, left = l1, key = k1, right = r1, ...} = x1
  2545         and {size = s2, ...} = x2
  2546       in
  2547         s1 <= s2 andalso
  2548         let
  2549           val (l2,k2,r2) = nodePartition cmp x2 k1
  2550         in
  2551           Option.isSome k2 andalso
  2552           treeSubset cmp l1 l2 andalso
  2553           treeSubset cmp r1 r2
  2554         end
  2555       end;
  2556 in
  2557   fun subset (Set (cmp,tree1)) (Set (_,tree2)) =
  2558       pointerEqual (tree1,tree2) orelse
  2559       treeSubset cmp tree1 tree2;
  2560 end;
  2561 
  2562 (* Set equality *)
  2563 
  2564 local
  2565   fun treeEqual _ E E = true
  2566     | treeEqual _ E _ = false
  2567     | treeEqual _ _ E = false
  2568     | treeEqual cmp (t1 as T x1) (T x2) =
  2569       let
  2570         val {size = s1, left = l1, key = k1, right = r1, ...} = x1
  2571         and {size = s2, ...} = x2
  2572       in
  2573         s1 = s2 andalso
  2574         let
  2575           val (l2,k2,r2) = nodePartition cmp x2 k1
  2576         in
  2577           Option.isSome k2 andalso
  2578           treeEqual cmp l1 l2 andalso
  2579           treeEqual cmp r1 r2
  2580         end
  2581       end;
  2582 in
  2583   fun equal (Set (cmp,tree1)) (Set (_,tree2)) =
  2584       pointerEqual (tree1,tree2) orelse
  2585       treeEqual cmp tree1 tree2;
  2586 end;
  2587 
  2588 (* filter is the basic function for preserving the tree structure. *)
  2589 
  2590 local
  2591   fun treeFilter _ _ E = E
  2592     | treeFilter cmp pred (T {priority,left,key,right,...}) =
  2593       let
  2594         val left = treeFilter cmp pred left
  2595         and right = treeFilter cmp pred right
  2596       in
  2597         if pred key then mkT priority left key right
  2598         else treeAppend cmp left right
  2599       end;
  2600 in
  2601   fun filter pred (Set (cmp,tree)) = Set (cmp, treeFilter cmp pred tree);
  2602 end;
  2603 
  2604 (* nth picks the nth smallest key (counting from 0). *)
  2605 
  2606 local
  2607   fun treeNth E _ = raise Subscript
  2608     | treeNth (T {left,key,right,...}) n =
  2609       let
  2610         val k = treeSize left
  2611       in
  2612         if n = k then key
  2613         else if n < k then treeNth left n
  2614         else treeNth right (n - (k + 1))
  2615       end;
  2616 in
  2617   fun nth (Set (_,tree)) n = treeNth tree n;
  2618 end;
  2619 
  2620 (* ------------------------------------------------------------------------- *)
  2621 (* Iterators.                                                                *)
  2622 (* ------------------------------------------------------------------------- *)
  2623 
  2624 fun leftSpine E acc = acc
  2625   | leftSpine (t as T {left,...}) acc = leftSpine left (t :: acc);
  2626 
  2627 fun rightSpine E acc = acc
  2628   | rightSpine (t as T {right,...}) acc = rightSpine right (t :: acc);
  2629 
  2630 datatype 'a iterator =
  2631     LR of 'a * 'a tree * 'a tree list
  2632   | RL of 'a * 'a tree * 'a tree list;
  2633 
  2634 fun mkLR [] = NONE
  2635   | mkLR (T {key,right,...} :: l) = SOME (LR (key,right,l))
  2636   | mkLR (E :: _) = raise Bug "RandomSet.mkLR";
  2637 
  2638 fun mkRL [] = NONE
  2639   | mkRL (T {key,left,...} :: l) = SOME (RL (key,left,l))
  2640   | mkRL (E :: _) = raise Bug "RandomSet.mkRL";
  2641 
  2642 fun mkIterator (Set (_,tree)) = mkLR (leftSpine tree []);
  2643 
  2644 fun mkRevIterator (Set (_,tree)) = mkRL (rightSpine tree []);
  2645 
  2646 fun readIterator (LR (key,_,_)) = key
  2647   | readIterator (RL (key,_,_)) = key;
  2648 
  2649 fun advanceIterator (LR (_,next,l)) = mkLR (leftSpine next l)
  2650   | advanceIterator (RL (_,next,l)) = mkRL (rightSpine next l);
  2651 
  2652 (* ------------------------------------------------------------------------- *)
  2653 (* Derived operations.                                                       *)
  2654 (* ------------------------------------------------------------------------- *)
  2655 
  2656 fun null s = size s = 0;
  2657 
  2658 fun member x s = Option.isSome (peek s x);
  2659 
  2660 fun add s x = union s (singleton (comparison s) x);
  2661 
  2662 (*DEBUG
  2663 val add = fn s => fn x =>
  2664     checkWellformed "RandomSet.add: result"
  2665       (add (checkWellformed "RandomSet.add: input" s) x);
  2666 *)
  2667 
  2668 local
  2669   fun unionPairs ys [] = rev ys
  2670     | unionPairs ys (xs as [_]) = List.revAppend (ys,xs)
  2671     | unionPairs ys (x1 :: x2 :: xs) = unionPairs (union x1 x2 :: ys) xs;
  2672 in
  2673   fun unionList [] = raise Error "RandomSet.unionList: no sets"
  2674     | unionList [s] = s
  2675     | unionList l = unionList (unionPairs [] l);
  2676 end;
  2677 
  2678 local
  2679   fun intersectPairs ys [] = rev ys
  2680     | intersectPairs ys (xs as [_]) = List.revAppend (ys,xs)
  2681     | intersectPairs ys (x1 :: x2 :: xs) =
  2682       intersectPairs (intersect x1 x2 :: ys) xs;
  2683 in
  2684   fun intersectList [] = raise Error "RandomSet.intersectList: no sets"
  2685     | intersectList [s] = s
  2686     | intersectList l = intersectList (intersectPairs [] l);
  2687 end;
  2688 
  2689 fun symmetricDifference s1 s2 = union (difference s1 s2) (difference s2 s1);
  2690 
  2691 fun disjoint s1 s2 = null (intersect s1 s2);
  2692 
  2693 fun partition pred set = (filter pred set, filter (not o pred) set);
  2694 
  2695 local
  2696   fun fold _ NONE acc = acc
  2697     | fold f (SOME iter) acc =
  2698       let
  2699         val key = readIterator iter
  2700       in
  2701         fold f (advanceIterator iter) (f (key,acc))
  2702       end;
  2703 in
  2704   fun foldl f b m = fold f (mkIterator m) b;
  2705 
  2706   fun foldr f b m = fold f (mkRevIterator m) b;
  2707 end;
  2708 
  2709 local
  2710   fun find _ NONE = NONE
  2711     | find pred (SOME iter) =
  2712       let
  2713         val key = readIterator iter
  2714       in
  2715         if pred key then SOME key
  2716         else find pred (advanceIterator iter)
  2717       end;
  2718 in
  2719   fun findl p m = find p (mkIterator m);
  2720 
  2721   fun findr p m = find p (mkRevIterator m);
  2722 end;
  2723 
  2724 local
  2725   fun first _ NONE = NONE
  2726     | first f (SOME iter) =
  2727       let
  2728         val key = readIterator iter
  2729       in
  2730         case f key of
  2731           NONE => first f (advanceIterator iter)
  2732         | s => s
  2733       end;
  2734 in
  2735   fun firstl f m = first f (mkIterator m);
  2736 
  2737   fun firstr f m = first f (mkRevIterator m);
  2738 end;
  2739 
  2740 fun count p = foldl (fn (x,n) => if p x then n + 1 else n) 0;
  2741 
  2742 fun fromList cmp l = List.foldl (fn (k,s) => add s k) (empty cmp) l;
  2743 
  2744 fun addList s l = union s (fromList (comparison s) l);
  2745 
  2746 fun toList s = foldr op:: [] s;
  2747 
  2748 fun map f s = rev (foldl (fn (x,l) => (x, f x) :: l) [] s);
  2749 
  2750 fun transform f s = rev (foldl (fn (x,l) => f x :: l) [] s);
  2751 
  2752 fun app f s = foldl (fn (x,()) => f x) () s;
  2753 
  2754 fun exists p s = Option.isSome (findl p s);
  2755 
  2756 fun all p s = not (exists (not o p) s);
  2757 
  2758 local
  2759   fun iterCompare _ NONE NONE = EQUAL
  2760     | iterCompare _ NONE (SOME _) = LESS
  2761     | iterCompare _ (SOME _) NONE = GREATER
  2762     | iterCompare cmp (SOME i1) (SOME i2) =
  2763       keyIterCompare cmp (readIterator i1) (readIterator i2) i1 i2
  2764 
  2765   and keyIterCompare cmp k1 k2 i1 i2 =
  2766       case cmp (k1,k2) of
  2767         LESS => LESS
  2768       | EQUAL => iterCompare cmp (advanceIterator i1) (advanceIterator i2)
  2769       | GREATER => GREATER;
  2770 in
  2771   fun compare (s1,s2) =
  2772       if pointerEqual (s1,s2) then EQUAL
  2773       else
  2774         case Int.compare (size s1, size s2) of
  2775           LESS => LESS
  2776         | EQUAL => iterCompare (comparison s1) (mkIterator s1) (mkIterator s2)
  2777         | GREATER => GREATER;
  2778 end;
  2779 
  2780 fun pick s =
  2781     case findl (K true) s of
  2782       SOME p => p
  2783     | NONE => raise Error "RandomSet.pick: empty";
  2784 
  2785 fun random s =
  2786     case size s of
  2787       0 => raise Error "RandomSet.random: empty"
  2788     | n => nth s (randomInt n);
  2789 
  2790 fun deletePick s = let val x = pick s in (x, delete s x) end;
  2791 
  2792 fun deleteRandom s = let val x = random s in (x, delete s x) end;
  2793 
  2794 fun close f s = let val s' = f s in if equal s s' then s else close f s' end;
  2795 
  2796 fun toString s = "{" ^ (if null s then "" else Int.toString (size s)) ^ "}";
  2797 
  2798 end
  2799 end;
  2800 
  2801 (**** Original file: Set.sml ****)
  2802 
  2803 structure Metis = struct open Metis
  2804 (* Metis-specific ML environment *)
  2805 nonfix ++ -- RL mem union subset;
  2806 val explode = String.explode;
  2807 val implode = String.implode;
  2808 val print = TextIO.print;
  2809 (* ========================================================================= *)
  2810 (* FINITE SETS                                                               *)
  2811 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  2812 (* ========================================================================= *)
  2813 
  2814 structure Set = RandomSet;
  2815 end;
  2816 
  2817 (**** Original file: ElementSet.sig ****)
  2818 
  2819 (* ========================================================================= *)
  2820 (* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
  2821 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  2822 (* ========================================================================= *)
  2823 
  2824 signature ElementSet =
  2825 sig
  2826 
  2827 type element
  2828 
  2829 (* ------------------------------------------------------------------------- *)
  2830 (* Finite sets                                                               *)
  2831 (* ------------------------------------------------------------------------- *)
  2832 
  2833 type set
  2834 
  2835 val empty : set
  2836 
  2837 val singleton : element -> set
  2838 
  2839 val null : set -> bool
  2840 
  2841 val size : set -> int
  2842 
  2843 val member : element -> set -> bool
  2844 
  2845 val add : set -> element -> set
  2846 
  2847 val addList : set -> element list -> set
  2848 
  2849 val delete : set -> element -> set  (* raises Error *)
  2850 
  2851 (* Union and intersect prefer elements in the second set *)
  2852 
  2853 val union : set -> set -> set
  2854 
  2855 val unionList : set list -> set
  2856 
  2857 val intersect : set -> set -> set
  2858 
  2859 val intersectList : set list -> set
  2860 
  2861 val difference : set -> set -> set
  2862 
  2863 val symmetricDifference : set -> set -> set
  2864 
  2865 val disjoint : set -> set -> bool
  2866 
  2867 val subset : set -> set -> bool
  2868 
  2869 val equal : set -> set -> bool
  2870 
  2871 val filter : (element -> bool) -> set -> set
  2872 
  2873 val partition : (element -> bool) -> set -> set * set
  2874 
  2875 val count : (element -> bool) -> set -> int
  2876 
  2877 val foldl : (element * 's -> 's) -> 's -> set -> 's
  2878 
  2879 val foldr : (element * 's -> 's) -> 's -> set -> 's
  2880 
  2881 val findl : (element -> bool) -> set -> element option
  2882 
  2883 val findr : (element -> bool) -> set -> element option
  2884 
  2885 val firstl : (element -> 'a option) -> set -> 'a option
  2886 
  2887 val firstr : (element -> 'a option) -> set -> 'a option
  2888 
  2889 val exists : (element -> bool) -> set -> bool
  2890 
  2891 val all : (element -> bool) -> set -> bool
  2892 
  2893 val map : (element -> 'a) -> set -> (element * 'a) list
  2894 
  2895 val transform : (element -> 'a) -> set -> 'a list
  2896 
  2897 val app : (element -> unit) -> set -> unit
  2898 
  2899 val toList : set -> element list
  2900 
  2901 val fromList : element list -> set
  2902 
  2903 val pick : set -> element  (* raises Empty *)
  2904 
  2905 val random : set -> element  (* raises Empty *)
  2906 
  2907 val deletePick : set -> element * set  (* raises Empty *)
  2908 
  2909 val deleteRandom : set -> element * set  (* raises Empty *)
  2910 
  2911 val compare : set * set -> order
  2912 
  2913 val close : (set -> set) -> set -> set
  2914 
  2915 val toString : set -> string
  2916 
  2917 (* ------------------------------------------------------------------------- *)
  2918 (* Iterators over sets                                                       *)
  2919 (* ------------------------------------------------------------------------- *)
  2920 
  2921 type iterator
  2922 
  2923 val mkIterator : set -> iterator option
  2924 
  2925 val mkRevIterator : set -> iterator option
  2926 
  2927 val readIterator : iterator -> element
  2928 
  2929 val advanceIterator : iterator -> iterator option
  2930 
  2931 end
  2932 
  2933 (**** Original file: ElementSet.sml ****)
  2934 
  2935 (* ========================================================================= *)
  2936 (* FINITE SETS WITH A FIXED ELEMENT TYPE                                     *)
  2937 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  2938 (* ========================================================================= *)
  2939 
  2940 functor ElementSet (Key : Ordered) :> ElementSet where type element = Key.t =
  2941 struct
  2942 
  2943  open Metis;
  2944 
  2945 type element = Key.t;
  2946 
  2947 (* ------------------------------------------------------------------------- *)
  2948 (* Finite sets                                                               *)
  2949 (* ------------------------------------------------------------------------- *)
  2950 
  2951 type set = Key.t Set.set;
  2952 
  2953 val empty = Set.empty Key.compare;
  2954 
  2955 fun singleton key = Set.singleton Key.compare key;
  2956 
  2957 val null = Set.null;
  2958 
  2959 val size = Set.size;
  2960 
  2961 val member = Set.member;
  2962 
  2963 val add = Set.add;
  2964 
  2965 val addList = Set.addList;
  2966 
  2967 val delete = Set.delete;
  2968 
  2969 val op union = Set.union;
  2970 
  2971 val unionList = Set.unionList;
  2972 
  2973 val intersect = Set.intersect;
  2974 
  2975 val intersectList = Set.intersectList;
  2976 
  2977 val difference = Set.difference;
  2978 
  2979 val symmetricDifference = Set.symmetricDifference;
  2980 
  2981 val disjoint = Set.disjoint;
  2982 
  2983 val op subset = Set.subset;
  2984 
  2985 val equal = Set.equal;
  2986 
  2987 val filter = Set.filter;
  2988 
  2989 val partition = Set.partition;
  2990 
  2991 val count = Set.count;
  2992 
  2993 val foldl = Set.foldl;
  2994 
  2995 val foldr = Set.foldr;
  2996 
  2997 val findl = Set.findl;
  2998 
  2999 val findr = Set.findr;
  3000 
  3001 val firstl = Set.firstl;
  3002 
  3003 val firstr = Set.firstr;
  3004 
  3005 val exists = Set.exists;
  3006 
  3007 val all = Set.all;
  3008 
  3009 val map = Set.map;
  3010 
  3011 val transform = Set.transform;
  3012 
  3013 val app = Set.app;
  3014 
  3015 val toList = Set.toList;
  3016 
  3017 fun fromList l = Set.fromList Key.compare l;
  3018 
  3019 val pick = Set.pick;
  3020 
  3021 val random = Set.random;
  3022 
  3023 val deletePick = Set.deletePick;
  3024 
  3025 val deleteRandom = Set.deleteRandom;
  3026 
  3027 val compare = Set.compare;
  3028 
  3029 val close = Set.close;
  3030 
  3031 val toString = Set.toString;
  3032 
  3033 (* ------------------------------------------------------------------------- *)
  3034 (* Iterators over sets                                                       *)
  3035 (* ------------------------------------------------------------------------- *)
  3036 
  3037 type iterator = Key.t Set.iterator;
  3038 
  3039 val mkIterator = Set.mkIterator;
  3040 
  3041 val mkRevIterator = Set.mkRevIterator;
  3042 
  3043 val readIterator = Set.readIterator;
  3044 
  3045 val advanceIterator = Set.advanceIterator;
  3046 
  3047 end
  3048 
  3049  structure Metis = struct open Metis;
  3050 
  3051 structure IntSet =
  3052 ElementSet (IntOrdered);
  3053 
  3054 structure StringSet =
  3055 ElementSet (StringOrdered);
  3056 
  3057  end;
  3058 
  3059 (**** Original file: Map.sig ****)
  3060 
  3061 (* ========================================================================= *)
  3062 (* FINITE MAPS                                                               *)
  3063 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  3064 (* ========================================================================= *)
  3065 
  3066 signature Map =
  3067 sig
  3068 
  3069 (* ------------------------------------------------------------------------- *)
  3070 (* Finite maps                                                               *)
  3071 (* ------------------------------------------------------------------------- *)
  3072 
  3073 type ('key,'a) map
  3074 
  3075 val new : ('key * 'key -> order) -> ('key,'a) map
  3076 
  3077 val null : ('key,'a) map -> bool
  3078 
  3079 val size : ('key,'a) map -> int
  3080 
  3081 val singleton : ('key * 'key -> order) -> 'key * 'a -> ('key,'a) map
  3082 
  3083 val inDomain : 'key -> ('key,'a) map -> bool
  3084 
  3085 val peek : ('key,'a) map -> 'key -> 'a option
  3086 
  3087 val insert : ('key,'a) map -> 'key * 'a -> ('key,'a) map
  3088 
  3089 val insertList : ('key,'a) map -> ('key * 'a) list -> ('key,'a) map
  3090 
  3091 val get : ('key,'a) map -> 'key -> 'a  (* raises Error *)
  3092 
  3093 (* Union and intersect prefer keys in the second map *)
  3094 
  3095 val union :
  3096     ('a * 'a -> 'a option) -> ('key,'a) map -> ('key,'a) map -> ('key,'a) map
  3097 
  3098 val intersect :
  3099     ('a * 'a -> 'a option) -> ('key,'a) map -> ('key,'a) map -> ('key,'a) map
  3100 
  3101 val delete : ('key,'a) map -> 'key -> ('key,'a) map  (* raises Error *)
  3102 
  3103 val difference : ('key,'a) map -> ('key,'b) map -> ('key,'a) map
  3104 
  3105 val subsetDomain : ('key,'a) map -> ('key,'a) map -> bool
  3106 
  3107 val equalDomain : ('key,'a) map -> ('key,'a) map -> bool
  3108 
  3109 val mapPartial : ('key * 'a -> 'b option) -> ('key,'a) map -> ('key,'b) map
  3110 
  3111 val filter : ('key * 'a -> bool) -> ('key,'a) map -> ('key,'a) map
  3112 
  3113 val map : ('key * 'a -> 'b) -> ('key,'a) map -> ('key,'b) map
  3114 
  3115 val app : ('key * 'a -> unit) -> ('key,'a) map -> unit
  3116 
  3117 val transform : ('a -> 'b) -> ('key,'a) map -> ('key,'b) map
  3118 
  3119 val foldl : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
  3120 
  3121 val foldr : ('key * 'a * 's -> 's) -> 's -> ('key,'a) map -> 's
  3122 
  3123 val findl : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
  3124 
  3125 val findr : ('key * 'a -> bool) -> ('key,'a) map -> ('key * 'a) option
  3126 
  3127 val firstl : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
  3128 
  3129 val firstr : ('key * 'a -> 'b option) -> ('key,'a) map -> 'b option
  3130 
  3131 val exists : ('key * 'a -> bool) -> ('key,'a) map -> bool
  3132 
  3133 val all : ('key * 'a -> bool) -> ('key,'a) map -> bool
  3134 
  3135 val domain : ('key,'a) map -> 'key list
  3136 
  3137 val toList : ('key,'a) map -> ('key * 'a) list
  3138 
  3139 val fromList : ('key * 'key -> order) -> ('key * 'a) list -> ('key,'a) map
  3140 
  3141 val random : ('key,'a) map -> 'key * 'a  (* raises Empty *)
  3142 
  3143 val compare : ('a * 'a -> order) -> ('key,'a) map * ('key,'a) map -> order
  3144 
  3145 val equal : ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool
  3146 
  3147 val toString : ('key,'a) map -> string
  3148 
  3149 (* ------------------------------------------------------------------------- *)
  3150 (* Iterators over maps                                                       *)
  3151 (* ------------------------------------------------------------------------- *)
  3152 
  3153 type ('key,'a) iterator
  3154 
  3155 val mkIterator : ('key,'a) map -> ('key,'a) iterator option
  3156 
  3157 val mkRevIterator : ('key,'a) map -> ('key,'a) iterator option
  3158 
  3159 val readIterator : ('key,'a) iterator -> 'key * 'a
  3160 
  3161 val advanceIterator : ('key,'a) iterator -> ('key,'a) iterator option
  3162 
  3163 end
  3164 
  3165 (**** Original file: RandomMap.sml ****)
  3166 
  3167 structure Metis = struct open Metis
  3168 (* Metis-specific ML environment *)
  3169 nonfix ++ -- RL mem union subset;
  3170 val explode = String.explode;
  3171 val implode = String.implode;
  3172 val print = TextIO.print;
  3173 (* ========================================================================= *)
  3174 (* FINITE MAPS IMPLEMENTED WITH RANDOMLY BALANCED TREES                      *)
  3175 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  3176 (* ========================================================================= *)
  3177 
  3178 structure RandomMap :> Map =
  3179 struct
  3180 
  3181 exception Bug = Useful.Bug;
  3182 
  3183 exception Error = Useful.Error;
  3184 
  3185 val pointerEqual = Portable.pointerEqual;
  3186 
  3187 val K = Useful.K;
  3188 
  3189 val snd = Useful.snd;
  3190 
  3191 val randomInt = Portable.randomInt;
  3192 
  3193 val randomWord = Portable.randomWord;
  3194 
  3195 (* ------------------------------------------------------------------------- *)
  3196 (* Random search trees.                                                      *)
  3197 (* ------------------------------------------------------------------------- *)
  3198 
  3199 type priority = Word.word;
  3200 
  3201 datatype ('a,'b) tree =
  3202     E
  3203   | T of
  3204     {size : int,
  3205      priority : priority,
  3206      left : ('a,'b) tree,
  3207      key : 'a,
  3208      value : 'b,
  3209      right : ('a,'b) tree};
  3210 
  3211 type ('a,'b) node =
  3212      {size : int,
  3213       priority : priority,
  3214       left : ('a,'b) tree,
  3215       key : 'a,
  3216       value : 'b,
  3217       right : ('a,'b) tree};
  3218 
  3219 datatype ('a,'b) map = Map of ('a * 'a -> order) * ('a,'b) tree;
  3220 
  3221 (* ------------------------------------------------------------------------- *)
  3222 (* Random priorities.                                                        *)
  3223 (* ------------------------------------------------------------------------- *)
  3224 
  3225 local
  3226   val randomPriority = randomWord;
  3227 
  3228   val priorityOrder = Word.compare;
  3229 in
  3230   fun treeSingleton (key,value) =
  3231       T {size = 1, priority = randomPriority (),
  3232          left = E, key = key, value = value, right = E};
  3233 
  3234   fun nodePriorityOrder cmp (x1 : ('a,'b) node, x2 : ('a,'b) node) =
  3235       let
  3236         val {priority = p1, key = k1, ...} = x1
  3237         and {priority = p2, key = k2, ...} = x2
  3238       in
  3239         case priorityOrder (p1,p2) of
  3240           LESS => LESS
  3241         | EQUAL => cmp (k1,k2)
  3242         | GREATER => GREATER
  3243       end;
  3244 end;
  3245 
  3246 (* ------------------------------------------------------------------------- *)
  3247 (* Debugging functions.                                                      *)
  3248 (* ------------------------------------------------------------------------- *)
  3249 
  3250 local
  3251   fun checkSizes E = 0
  3252     | checkSizes (T {size,left,right,...}) =
  3253       let
  3254         val l = checkSizes left
  3255         and r = checkSizes right
  3256         val () = if l + 1 + r = size then () else raise Error "wrong size"
  3257       in
  3258         size
  3259       end;
  3260 
  3261   fun checkSorted _ x E = x
  3262     | checkSorted cmp x (T {left,key,right,...}) =
  3263       let
  3264         val x = checkSorted cmp x left
  3265         val () =
  3266             case x of
  3267               NONE => ()
  3268             | SOME k =>
  3269               case cmp (k,key) of
  3270                 LESS => ()
  3271               | EQUAL => raise Error "duplicate keys"
  3272               | GREATER => raise Error "unsorted"
  3273       in
  3274         checkSorted cmp (SOME key) right
  3275       end;
  3276 
  3277   fun checkPriorities _ E = NONE
  3278     | checkPriorities cmp (T (x as {left,right,...})) =
  3279       let
  3280         val () =
  3281             case checkPriorities cmp left of
  3282               NONE => ()
  3283             | SOME l =>
  3284               case nodePriorityOrder cmp (l,x) of
  3285                 LESS => ()
  3286               | EQUAL => raise Error "left child has equal key"
  3287               | GREATER => raise Error "left child has greater priority"
  3288         val () =
  3289             case checkPriorities cmp right of
  3290               NONE => ()
  3291             | SOME r =>
  3292               case nodePriorityOrder cmp (r,x) of
  3293                 LESS => ()
  3294               | EQUAL => raise Error "right child has equal key"
  3295               | GREATER => raise Error "right child has greater priority"
  3296       in
  3297         SOME x
  3298       end;
  3299 in
  3300   fun checkWellformed s (m as Map (cmp,tree)) =
  3301       (let
  3302          val _ = checkSizes tree
  3303          val _ = checkSorted cmp NONE tree
  3304          val _ = checkPriorities cmp tree
  3305        in
  3306          m
  3307        end
  3308        handle Error err => raise Bug err)
  3309       handle Bug bug => raise Bug (s ^ "\nRandomMap.checkWellformed: " ^ bug);
  3310 end;
  3311 
  3312 (* ------------------------------------------------------------------------- *)
  3313 (* Basic operations.                                                         *)
  3314 (* ------------------------------------------------------------------------- *)
  3315 
  3316 fun comparison (Map (cmp,_)) = cmp;
  3317 
  3318 fun new cmp = Map (cmp,E);
  3319 
  3320 fun treeSize E = 0
  3321   | treeSize (T {size = s, ...}) = s;
  3322 
  3323 fun size (Map (_,tree)) = treeSize tree;
  3324 
  3325 fun mkT p l k v r =
  3326     T {size = treeSize l + 1 + treeSize r, priority = p,
  3327        left = l, key = k, value = v, right = r};
  3328 
  3329 fun singleton cmp key_value = Map (cmp, treeSingleton key_value);
  3330 
  3331 local
  3332   fun treePeek cmp E pkey = NONE
  3333     | treePeek cmp (T {left,key,value,right,...}) pkey =
  3334       case cmp (pkey,key) of
  3335         LESS => treePeek cmp left pkey
  3336       | EQUAL => SOME value
  3337       | GREATER => treePeek cmp right pkey
  3338 in
  3339   fun peek (Map (cmp,tree)) key = treePeek cmp tree key;
  3340 end;
  3341 
  3342 (* treeAppend assumes that every element of the first tree is less than *)
  3343 (* every element of the second tree. *)
  3344 
  3345 fun treeAppend _ t1 E = t1
  3346   | treeAppend _ E t2 = t2
  3347   | treeAppend cmp (t1 as T x1) (t2 as T x2) =
  3348     case nodePriorityOrder cmp (x1,x2) of
  3349       LESS =>
  3350       let
  3351         val {priority = p2,
  3352              left = l2, key = k2, value = v2, right = r2, ...} = x2
  3353       in
  3354         mkT p2 (treeAppend cmp t1 l2) k2 v2 r2
  3355       end
  3356     | EQUAL => raise Bug "RandomSet.treeAppend: equal keys"
  3357     | GREATER =>
  3358       let
  3359         val {priority = p1,
  3360              left = l1, key = k1, value = v1, right = r1, ...} = x1
  3361       in
  3362         mkT p1 l1 k1 v1 (treeAppend cmp r1 t2)
  3363       end;
  3364 
  3365 (* nodePartition splits the node into three parts: the keys comparing less *)
  3366 (* than the supplied key, an optional equal key, and the keys comparing *)
  3367 (* greater. *)
  3368 
  3369 local
  3370   fun mkLeft [] t = t
  3371     | mkLeft (({priority,left,key,value,...} : ('a,'b) node) :: xs) t =
  3372       mkLeft xs (mkT priority left key value t);
  3373 
  3374   fun mkRight [] t = t
  3375     | mkRight (({priority,key,value,right,...} : ('a,'b) node) :: xs) t =
  3376       mkRight xs (mkT priority t key value right);
  3377 
  3378   fun treePart _ _ lefts rights E = (mkLeft lefts E, NONE, mkRight rights E)
  3379     | treePart cmp pkey lefts rights (T x) = nodePart cmp pkey lefts rights x
  3380   and nodePart cmp pkey lefts rights (x as {left,key,value,right,...}) =
  3381       case cmp (pkey,key) of
  3382         LESS => treePart cmp pkey lefts (x :: rights) left
  3383       | EQUAL => (mkLeft lefts left, SOME (key,value), mkRight rights right)
  3384       | GREATER => treePart cmp pkey (x :: lefts) rights right;
  3385 in
  3386   fun nodePartition cmp x pkey = nodePart cmp pkey [] [] x;
  3387 end;
  3388 
  3389 (* union first calls treeCombineRemove, to combine the values *)
  3390 (* for equal keys into the first map and remove them from the second map. *)
  3391 (* Note that the combined key is always the one from the second map. *)
  3392 
  3393 local
  3394   fun treeCombineRemove _ _ t1 E = (t1,E)
  3395     | treeCombineRemove _ _ E t2 = (E,t2)
  3396     | treeCombineRemove cmp f (t1 as T x1) (t2 as T x2) =
  3397       let
  3398         val {priority = p1,
  3399              left = l1, key = k1, value = v1, right = r1, ...} = x1
  3400         val (l2,k2_v2,r2) = nodePartition cmp x2 k1
  3401         val (l1,l2) = treeCombineRemove cmp f l1 l2
  3402         and (r1,r2) = treeCombineRemove cmp f r1 r2
  3403       in
  3404         case k2_v2 of
  3405           NONE =>
  3406           if treeSize l2 + treeSize r2 = #size x2 then (t1,t2)
  3407           else (mkT p1 l1 k1 v1 r1, treeAppend cmp l2 r2)
  3408         | SOME (k2,v2) =>
  3409           case f (v1,v2) of
  3410             NONE => (treeAppend cmp l1 r1, treeAppend cmp l2 r2)
  3411           | SOME v => (mkT p1 l1 k2 v r1, treeAppend cmp l2 r2)
  3412       end;
  3413 
  3414   fun treeUnionDisjoint _ t1 E = t1
  3415     | treeUnionDisjoint _ E t2 = t2
  3416     | treeUnionDisjoint cmp (T x1) (T x2) =
  3417       case nodePriorityOrder cmp (x1,x2) of
  3418         LESS => nodeUnionDisjoint cmp x2 x1
  3419       | EQUAL => raise Bug "RandomSet.unionDisjoint: equal keys"
  3420       | GREATER => nodeUnionDisjoint cmp x1 x2
  3421   and nodeUnionDisjoint cmp x1 x2 =
  3422       let
  3423         val {priority = p1,
  3424              left = l1, key = k1, value = v1, right = r1, ...} = x1
  3425         val (l2,_,r2) = nodePartition cmp x2 k1
  3426         val l = treeUnionDisjoint cmp l1 l2
  3427         and r = treeUnionDisjoint cmp r1 r2
  3428       in
  3429         mkT p1 l k1 v1 r
  3430       end;
  3431 in
  3432   fun union f (m1 as Map (cmp,t1)) (Map (_,t2)) =
  3433       if pointerEqual (t1,t2) then m1
  3434       else
  3435         let
  3436           val (t1,t2) = treeCombineRemove cmp f t1 t2
  3437         in
  3438           Map (cmp, treeUnionDisjoint cmp t1 t2)
  3439         end;
  3440 end;
  3441 
  3442 (*DEBUG
  3443 val union = fn f => fn t1 => fn t2 =>
  3444     checkWellformed "RandomMap.union: result"
  3445       (union f (checkWellformed "RandomMap.union: input 1" t1)
  3446                (checkWellformed "RandomMap.union: input 2" t2));
  3447 *)
  3448 
  3449 (* intersect is a simple case of the union algorithm. *)
  3450 
  3451 local
  3452   fun treeIntersect _ _ _ E = E
  3453     | treeIntersect _ _ E _ = E
  3454     | treeIntersect cmp f (t1 as T x1) (t2 as T x2) =
  3455       let
  3456         val {priority = p1,
  3457              left = l1, key = k1, value = v1, right = r1, ...} = x1
  3458         val (l2,k2_v2,r2) = nodePartition cmp x2 k1
  3459         val l = treeIntersect cmp f l1 l2
  3460         and r = treeIntersect cmp f r1 r2
  3461       in
  3462         case k2_v2 of
  3463           NONE => treeAppend cmp l r
  3464         | SOME (k2,v2) =>
  3465           case f (v1,v2) of
  3466             NONE => treeAppend cmp l r
  3467           | SOME v => mkT p1 l k2 v r
  3468       end;
  3469 in
  3470   fun intersect f (m1 as Map (cmp,t1)) (Map (_,t2)) =
  3471       if pointerEqual (t1,t2) then m1
  3472       else Map (cmp, treeIntersect cmp f t1 t2);
  3473 end;
  3474 
  3475 (*DEBUG
  3476 val intersect = fn f => fn t1 => fn t2 =>
  3477     checkWellformed "RandomMap.intersect: result"
  3478       (intersect f (checkWellformed "RandomMap.intersect: input 1" t1)
  3479                    (checkWellformed "RandomMap.intersect: input 2" t2));
  3480 *)
  3481 
  3482 (* delete raises an exception if the supplied key is not found, which *)
  3483 (* makes it simpler to maximize sharing. *)
  3484 
  3485 local
  3486   fun treeDelete _ E _ = raise Error "RandomMap.delete: element not found"
  3487     | treeDelete cmp (T {priority,left,key,value,right,...}) dkey =
  3488       case cmp (dkey,key) of
  3489         LESS => mkT priority (treeDelete cmp left dkey) key value right
  3490       | EQUAL => treeAppend cmp left right
  3491       | GREATER => mkT priority left key value (treeDelete cmp right dkey);
  3492 in
  3493   fun delete (Map (cmp,tree)) key = Map (cmp, treeDelete cmp tree key);
  3494 end;
  3495  
  3496 (*DEBUG
  3497 val delete = fn t => fn x =>
  3498     checkWellformed "RandomMap.delete: result"
  3499       (delete (checkWellformed "RandomMap.delete: input" t) x);
  3500 *)
  3501 
  3502 (* Set difference on domains *)
  3503 
  3504 local
  3505   fun treeDifference _ t1 E = t1
  3506     | treeDifference _ E _ = E
  3507     | treeDifference cmp (t1 as T x1) (T x2) =
  3508       let
  3509         val {size = s1, priority = p1,
  3510              left = l1, key = k1, value = v1, right = r1} = x1
  3511         val (l2,k2_v2,r2) = nodePartition cmp x2 k1
  3512         val l = treeDifference cmp l1 l2
  3513         and r = treeDifference cmp r1 r2
  3514       in
  3515         if Option.isSome k2_v2 then treeAppend cmp l r
  3516         else if treeSize l + treeSize r + 1 = s1 then t1
  3517         else mkT p1 l k1 v1 r
  3518       end;
  3519 in
  3520   fun difference (Map (cmp,tree1)) (Map (_,tree2)) =
  3521       Map (cmp, treeDifference cmp tree1 tree2);
  3522 end;
  3523 
  3524 (*DEBUG
  3525 val difference = fn t1 => fn t2 =>
  3526     checkWellformed "RandomMap.difference: result"
  3527       (difference (checkWellformed "RandomMap.difference: input 1" t1)
  3528                   (checkWellformed "RandomMap.difference: input 2" t2));
  3529 *)
  3530 
  3531 (* subsetDomain is mainly used when using maps as sets. *)
  3532 
  3533 local
  3534   fun treeSubsetDomain _ E _ = true
  3535     | treeSubsetDomain _ _ E = false
  3536     | treeSubsetDomain cmp (t1 as T x1) (T x2) =
  3537       let
  3538         val {size = s1, left = l1, key = k1, right = r1, ...} = x1
  3539         and {size = s2, ...} = x2
  3540       in
  3541         s1 <= s2 andalso
  3542         let
  3543           val (l2,k2_v2,r2) = nodePartition cmp x2 k1
  3544         in
  3545           Option.isSome k2_v2 andalso
  3546           treeSubsetDomain cmp l1 l2 andalso
  3547           treeSubsetDomain cmp r1 r2
  3548         end
  3549       end;
  3550 in
  3551   fun subsetDomain (Map (cmp,tree1)) (Map (_,tree2)) =
  3552       pointerEqual (tree1,tree2) orelse
  3553       treeSubsetDomain cmp tree1 tree2;
  3554 end;
  3555 
  3556 (* Map equality *)
  3557 
  3558 local
  3559   fun treeEqual _ _ E E = true
  3560     | treeEqual _ _ E _ = false
  3561     | treeEqual _ _ _ E = false
  3562     | treeEqual cmp veq (t1 as T x1) (T x2) =
  3563       let
  3564         val {size = s1, left = l1, key = k1, value = v1, right = r1, ...} = x1
  3565         and {size = s2, ...} = x2
  3566       in
  3567         s1 = s2 andalso
  3568         let
  3569           val (l2,k2_v2,r2) = nodePartition cmp x2 k1
  3570         in
  3571           (case k2_v2 of NONE => false | SOME (_,v2) => veq v1 v2) andalso
  3572           treeEqual cmp veq l1 l2 andalso
  3573           treeEqual cmp veq r1 r2
  3574         end
  3575       end;
  3576 in
  3577   fun equal veq (Map (cmp,tree1)) (Map (_,tree2)) =
  3578       pointerEqual (tree1,tree2) orelse
  3579       treeEqual cmp veq tree1 tree2;
  3580 end;
  3581 
  3582 (* mapPartial is the basic function for preserving the tree structure. *)
  3583 (* It applies the argument function to the elements *in order*. *)
  3584 
  3585 local
  3586   fun treeMapPartial cmp _ E = E
  3587     | treeMapPartial cmp f (T {priority,left,key,value,right,...}) =
  3588       let
  3589         val left = treeMapPartial cmp f left
  3590         and value' = f (key,value)
  3591         and right = treeMapPartial cmp f right
  3592       in
  3593         case value' of
  3594           NONE => treeAppend cmp left right
  3595         | SOME value => mkT priority left key value right
  3596       end;
  3597 in
  3598   fun mapPartial f (Map (cmp,tree)) = Map (cmp, treeMapPartial cmp f tree);
  3599 end;
  3600 
  3601 (* map is a primitive function for efficiency reasons. *)
  3602 (* It also applies the argument function to the elements *in order*. *)
  3603 
  3604 local
  3605   fun treeMap _ E = E
  3606     | treeMap f (T {size,priority,left,key,value,right}) =
  3607       let
  3608         val left = treeMap f left
  3609         and value = f (key,value)
  3610         and right = treeMap f right
  3611       in
  3612         T {size = size, priority = priority, left = left,
  3613            key = key, value = value, right = right}
  3614       end;
  3615 in
  3616   fun map f (Map (cmp,tree)) = Map (cmp, treeMap f tree);
  3617 end;
  3618 
  3619 (* nth picks the nth smallest key/value (counting from 0). *)
  3620 
  3621 local
  3622   fun treeNth E _ = raise Subscript
  3623     | treeNth (T {left,key,value,right,...}) n =
  3624       let
  3625         val k = treeSize left
  3626       in
  3627         if n = k then (key,value)
  3628         else if n < k then treeNth left n
  3629         else treeNth right (n - (k + 1))
  3630       end;
  3631 in
  3632   fun nth (Map (_,tree)) n = treeNth tree n;
  3633 end;
  3634 
  3635 (* ------------------------------------------------------------------------- *)
  3636 (* Iterators.                                                                *)
  3637 (* ------------------------------------------------------------------------- *)
  3638 
  3639 fun leftSpine E acc = acc
  3640   | leftSpine (t as T {left,...}) acc = leftSpine left (t :: acc);
  3641 
  3642 fun rightSpine E acc = acc
  3643   | rightSpine (t as T {right,...}) acc = rightSpine right (t :: acc);
  3644 
  3645 datatype ('key,'a) iterator =
  3646     LR of ('key * 'a) * ('key,'a) tree * ('key,'a) tree list
  3647   | RL of ('key * 'a) * ('key,'a) tree * ('key,'a) tree list;
  3648 
  3649 fun mkLR [] = NONE
  3650   | mkLR (T {key,value,right,...} :: l) = SOME (LR ((key,value),right,l))
  3651   | mkLR (E :: _) = raise Bug "RandomMap.mkLR";
  3652 
  3653 fun mkRL [] = NONE
  3654   | mkRL (T {key,value,left,...} :: l) = SOME (RL ((key,value),left,l))
  3655   | mkRL (E :: _) = raise Bug "RandomMap.mkRL";
  3656 
  3657 fun mkIterator (Map (_,tree)) = mkLR (leftSpine tree []);
  3658 
  3659 fun mkRevIterator (Map (_,tree)) = mkRL (rightSpine tree []);
  3660 
  3661 fun readIterator (LR (key_value,_,_)) = key_value
  3662   | readIterator (RL (key_value,_,_)) = key_value;
  3663 
  3664 fun advanceIterator (LR (_,next,l)) = mkLR (leftSpine next l)
  3665   | advanceIterator (RL (_,next,l)) = mkRL (rightSpine next l);
  3666 
  3667 (* ------------------------------------------------------------------------- *)
  3668 (* Derived operations.                                                       *)
  3669 (* ------------------------------------------------------------------------- *)
  3670 
  3671 fun null m = size m = 0;
  3672 
  3673 fun get m key =
  3674     case peek m key of
  3675       NONE => raise Error "RandomMap.get: element not found"
  3676     | SOME value => value;
  3677 
  3678 fun inDomain key m = Option.isSome (peek m key);
  3679 
  3680 fun insert m key_value =
  3681     union (SOME o snd) m (singleton (comparison m) key_value);
  3682 
  3683 (*DEBUG
  3684 val insert = fn m => fn x =>
  3685     checkWellformed "RandomMap.insert: result"
  3686       (insert (checkWellformed "RandomMap.insert: input" m) x);
  3687 *)
  3688 
  3689 local
  3690   fun fold _ NONE acc = acc
  3691     | fold f (SOME iter) acc =
  3692       let
  3693         val (key,value) = readIterator iter
  3694       in
  3695         fold f (advanceIterator iter) (f (key,value,acc))
  3696       end;
  3697 in
  3698   fun foldl f b m = fold f (mkIterator m) b;
  3699 
  3700   fun foldr f b m = fold f (mkRevIterator m) b;
  3701 end;
  3702 
  3703 local
  3704   fun find _ NONE = NONE
  3705     | find pred (SOME iter) =
  3706       let
  3707         val key_value = readIterator iter
  3708       in
  3709         if pred key_value then SOME key_value
  3710         else find pred (advanceIterator iter)
  3711       end;
  3712 in
  3713   fun findl p m = find p (mkIterator m);
  3714 
  3715   fun findr p m = find p (mkRevIterator m);
  3716 end;
  3717 
  3718 local
  3719   fun first _ NONE = NONE
  3720     | first f (SOME iter) =
  3721       let
  3722         val key_value = readIterator iter
  3723       in
  3724         case f key_value of
  3725           NONE => first f (advanceIterator iter)
  3726         | s => s
  3727       end;
  3728 in
  3729   fun firstl f m = first f (mkIterator m);
  3730 
  3731   fun firstr f m = first f (mkRevIterator m);
  3732 end;
  3733 
  3734 fun fromList cmp l = List.foldl (fn (k_v,m) => insert m k_v) (new cmp) l;
  3735 
  3736 fun insertList m l = union (SOME o snd) m (fromList (comparison m) l);
  3737 
  3738 fun filter p =
  3739     let
  3740       fun f (key_value as (_,value)) =
  3741           if p key_value then SOME value else NONE
  3742     in
  3743       mapPartial f
  3744     end;
  3745 
  3746 fun app f m = foldl (fn (key,value,()) => f (key,value)) () m;
  3747 
  3748 fun transform f = map (fn (_,value) => f value);
  3749 
  3750 fun toList m = foldr (fn (key,value,l) => (key,value) :: l) [] m;
  3751 
  3752 fun domain m = foldr (fn (key,_,l) => key :: l) [] m;
  3753 
  3754 fun exists p m = Option.isSome (findl p m);
  3755 
  3756 fun all p m = not (exists (not o p) m);
  3757 
  3758 fun random m =
  3759     case size m of
  3760       0 => raise Error "RandomMap.random: empty"
  3761     | n => nth m (randomInt n);
  3762 
  3763 local
  3764   fun iterCompare _ _ NONE NONE = EQUAL
  3765     | iterCompare _ _ NONE (SOME _) = LESS
  3766     | iterCompare _ _ (SOME _) NONE = GREATER
  3767     | iterCompare kcmp vcmp (SOME i1) (SOME i2) =
  3768       keyIterCompare kcmp vcmp (readIterator i1) (readIterator i2) i1 i2
  3769 
  3770   and keyIterCompare kcmp vcmp (k1,v1) (k2,v2) i1 i2 =
  3771       case kcmp (k1,k2) of
  3772         LESS => LESS
  3773       | EQUAL =>
  3774         (case vcmp (v1,v2) of
  3775            LESS => LESS
  3776          | EQUAL =>
  3777            iterCompare kcmp vcmp (advanceIterator i1) (advanceIterator i2)
  3778          | GREATER => GREATER)
  3779       | GREATER => GREATER;
  3780 in
  3781   fun compare vcmp (m1,m2) =
  3782       if pointerEqual (m1,m2) then EQUAL
  3783       else
  3784         case Int.compare (size m1, size m2) of
  3785           LESS => LESS
  3786         | EQUAL =>
  3787           iterCompare (comparison m1) vcmp (mkIterator m1) (mkIterator m2)
  3788         | GREATER => GREATER;
  3789 end;
  3790 
  3791 fun equalDomain m1 m2 = equal (K (K true)) m1 m2;
  3792 
  3793 fun toString m = "<" ^ (if null m then "" else Int.toString (size m)) ^ ">";
  3794 
  3795 end
  3796 end;
  3797 
  3798 (**** Original file: Map.sml ****)
  3799 
  3800 structure Metis = struct open Metis
  3801 (* Metis-specific ML environment *)
  3802 nonfix ++ -- RL mem union subset;
  3803 val explode = String.explode;
  3804 val implode = String.implode;
  3805 val print = TextIO.print;
  3806 (* ========================================================================= *)
  3807 (* FINITE MAPS                                                               *)
  3808 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  3809 (* ========================================================================= *)
  3810 
  3811 structure Map = RandomMap;
  3812 end;
  3813 
  3814 (**** Original file: KeyMap.sig ****)
  3815 
  3816 (* ========================================================================= *)
  3817 (* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
  3818 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  3819 (* ========================================================================= *)
  3820 
  3821 signature KeyMap =
  3822 sig
  3823 
  3824 type key
  3825 
  3826 (* ------------------------------------------------------------------------- *)
  3827 (* Finite maps                                                               *)
  3828 (* ------------------------------------------------------------------------- *)
  3829 
  3830 type 'a map
  3831 
  3832 val new : unit -> 'a map
  3833 
  3834 val null : 'a map -> bool
  3835 
  3836 val size : 'a map -> int
  3837 
  3838 val singleton : key * 'a -> 'a map
  3839 
  3840 val inDomain : key -> 'a map -> bool
  3841 
  3842 val peek : 'a map -> key -> 'a option
  3843 
  3844 val insert : 'a map -> key * 'a -> 'a map
  3845 
  3846 val insertList : 'a map -> (key * 'a) list -> 'a map
  3847 
  3848 val get : 'a map -> key -> 'a  (* raises Error *)
  3849 
  3850 (* Union and intersect prefer keys in the second map *)
  3851 
  3852 val union : ('a * 'a -> 'a option) -> 'a map -> 'a map -> 'a map
  3853 
  3854 val intersect : ('a * 'a -> 'a option) -> 'a map -> 'a map -> 'a map
  3855 
  3856 val delete : 'a map -> key -> 'a map  (* raises Error *)
  3857 
  3858 val difference : 'a map -> 'a map -> 'a map
  3859 
  3860 val subsetDomain : 'a map -> 'a map -> bool
  3861 
  3862 val equalDomain : 'a map -> 'a map -> bool
  3863 
  3864 val mapPartial : (key * 'a -> 'b option) -> 'a map -> 'b map
  3865 
  3866 val filter : (key * 'a -> bool) -> 'a map -> 'a map
  3867 
  3868 val map : (key * 'a -> 'b) -> 'a map -> 'b map
  3869 
  3870 val app : (key * 'a -> unit) -> 'a map -> unit
  3871 
  3872 val transform : ('a -> 'b) -> 'a map -> 'b map
  3873 
  3874 val foldl : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
  3875 
  3876 val foldr : (key * 'a * 's -> 's) -> 's -> 'a map -> 's
  3877 
  3878 val findl : (key * 'a -> bool) -> 'a map -> (key * 'a) option
  3879 
  3880 val findr : (key * 'a -> bool) -> 'a map -> (key * 'a) option
  3881 
  3882 val firstl : (key * 'a -> 'b option) -> 'a map -> 'b option
  3883 
  3884 val firstr : (key * 'a -> 'b option) -> 'a map -> 'b option
  3885 
  3886 val exists : (key * 'a -> bool) -> 'a map -> bool
  3887 
  3888 val all : (key * 'a -> bool) -> 'a map -> bool
  3889 
  3890 val domain : 'a map -> key list
  3891 
  3892 val toList : 'a map -> (key * 'a) list
  3893 
  3894 val fromList : (key * 'a) list -> 'a map
  3895 
  3896 val compare : ('a * 'a -> order) -> 'a map * 'a map -> order
  3897 
  3898 val equal : ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
  3899 
  3900 val random : 'a map -> key * 'a  (* raises Empty *)
  3901 
  3902 val toString : 'a map -> string
  3903 
  3904 (* ------------------------------------------------------------------------- *)
  3905 (* Iterators over maps                                                       *)
  3906 (* ------------------------------------------------------------------------- *)
  3907 
  3908 type 'a iterator
  3909 
  3910 val mkIterator : 'a map -> 'a iterator option
  3911 
  3912 val mkRevIterator : 'a map -> 'a iterator option
  3913 
  3914 val readIterator : 'a iterator -> key * 'a
  3915 
  3916 val advanceIterator : 'a iterator -> 'a iterator option
  3917 
  3918 end
  3919 
  3920 (**** Original file: KeyMap.sml ****)
  3921 
  3922 (* ========================================================================= *)
  3923 (* FINITE MAPS WITH A FIXED KEY TYPE                                         *)
  3924 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  3925 (* ========================================================================= *)
  3926 
  3927 functor KeyMap (Key : Ordered) :> KeyMap where type key = Key.t =
  3928 struct
  3929 
  3930  open Metis;
  3931 
  3932 type key = Key.t;
  3933 
  3934 (* ------------------------------------------------------------------------- *)
  3935 (* Finite maps                                                               *)
  3936 (* ------------------------------------------------------------------------- *)
  3937 
  3938 type 'a map = (Key.t,'a) Map.map;
  3939 
  3940 fun new () = Map.new Key.compare;
  3941 
  3942 val null = Map.null;
  3943 
  3944 val size = Map.size;
  3945 
  3946 fun singleton key_value = Map.singleton Key.compare key_value;
  3947 
  3948 val inDomain = Map.inDomain;
  3949 
  3950 val peek = Map.peek;
  3951 
  3952 val insert = Map.insert;
  3953 
  3954 val insertList = Map.insertList;
  3955 
  3956 val get = Map.get;
  3957 
  3958 (* Both op union and intersect prefer keys in the second map *)
  3959 
  3960 val op union = Map.union;
  3961 
  3962 val intersect = Map.intersect;
  3963 
  3964 val delete = Map.delete;
  3965 
  3966 val difference = Map.difference;
  3967 
  3968 val subsetDomain = Map.subsetDomain;
  3969 
  3970 val equalDomain = Map.equalDomain;
  3971 
  3972 val mapPartial = Map.mapPartial;
  3973 
  3974 val filter = Map.filter;
  3975 
  3976 val map = Map.map;
  3977 
  3978 val app = Map.app;
  3979 
  3980 val transform = Map.transform;
  3981 
  3982 val foldl = Map.foldl;
  3983 
  3984 val foldr = Map.foldr;
  3985 
  3986 val findl = Map.findl;
  3987 
  3988 val findr = Map.findr;
  3989 
  3990 val firstl = Map.firstl;
  3991 
  3992 val firstr = Map.firstr;
  3993 
  3994 val exists = Map.exists;
  3995 
  3996 val all = Map.all;
  3997 
  3998 val domain = Map.domain;
  3999 
  4000 val toList = Map.toList;
  4001 
  4002 fun fromList l = Map.fromList Key.compare l;
  4003 
  4004 val compare = Map.compare;
  4005 
  4006 val equal = Map.equal;
  4007 
  4008 val random = Map.random;
  4009 
  4010 val toString = Map.toString;
  4011 
  4012 (* ------------------------------------------------------------------------- *)
  4013 (* Iterators over maps                                                       *)
  4014 (* ------------------------------------------------------------------------- *)
  4015 
  4016 type 'a iterator = (Key.t,'a) Map.iterator;
  4017 
  4018 val mkIterator = Map.mkIterator;
  4019 
  4020 val mkRevIterator = Map.mkRevIterator;
  4021 
  4022 val readIterator = Map.readIterator;
  4023 
  4024 val advanceIterator = Map.advanceIterator;
  4025 
  4026 end
  4027 
  4028  structure Metis = struct open Metis
  4029 
  4030 structure IntMap =
  4031 KeyMap (IntOrdered);
  4032 
  4033 structure StringMap =
  4034 KeyMap (StringOrdered);
  4035 
  4036  end;
  4037 
  4038 (**** Original file: Sharing.sig ****)
  4039 
  4040 (* ========================================================================= *)
  4041 (* PRESERVING SHARING OF ML VALUES                                           *)
  4042 (* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
  4043 (* ========================================================================= *)
  4044 
  4045 signature Sharing =
  4046 sig
  4047 
  4048 (* ------------------------------------------------------------------------- *)
  4049 (* Pointer equality.                                                         *)
  4050 (* ------------------------------------------------------------------------- *)
  4051 
  4052 val pointerEqual : 'a * 'a -> bool
  4053 
  4054 (* ------------------------------------------------------------------------- *)
  4055 (* List operations.                                                          *)
  4056 (* ------------------------------------------------------------------------- *)
  4057 
  4058 val map : ('a -> 'a) -> 'a list -> 'a list
  4059 
  4060 val updateNth : int * 'a -> 'a list -> 'a list
  4061 
  4062 val setify : ''a list -> ''a list
  4063 
  4064 (* ------------------------------------------------------------------------- *)
  4065 (* Function caching.                                                         *)
  4066 (* ------------------------------------------------------------------------- *)
  4067 
  4068 val cache : ('a * 'a -> order) -> ('a -> 'b) -> 'a -> 'b
  4069 
  4070 (* ------------------------------------------------------------------------- *)
  4071 (* Hash consing.                                                             *)
  4072 (* ------------------------------------------------------------------------- *)
  4073 
  4074 val hashCons : ('a * 'a -> order) -> 'a -> 'a
  4075 
  4076 end
  4077 
  4078 (**** Original file: Sharing.sml ****)
  4079 
  4080 structure Metis = struct open Metis
  4081 (* Metis-specific ML environment *)
  4082 nonfix ++ -- RL mem union subset;
  4083 val explode = String.explode;
  4084 val implode = String.implode;
  4085 val print = TextIO.print;
  4086 (* ========================================================================= *)
  4087 (* PRESERVING SHARING OF ML VALUES                                           *)
  4088 (* Copyright (c) 2005-2006 Joe Hurd, distributed under the BSD License *)
  4089 (* ========================================================================= *)
  4090 
  4091 structure Sharing :> Sharing =
  4092 struct
  4093 
  4094 infix ==
  4095 
  4096 (* ------------------------------------------------------------------------- *)
  4097 (* Pointer equality.                                                         *)
  4098 (* ------------------------------------------------------------------------- *)
  4099 
  4100 val pointerEqual = Portable.pointerEqual;
  4101 
  4102 val op== = pointerEqual;
  4103 
  4104 (* ------------------------------------------------------------------------- *)
  4105 (* List operations.                                                          *)
  4106 (* ------------------------------------------------------------------------- *)
  4107 
  4108 fun map f =
  4109     let
  4110       fun m _ a_b [] = List.revAppend a_b
  4111         | m ys a_b (x :: xs) =
  4112           let
  4113             val y = f x
  4114             val ys = y :: ys
  4115           in
  4116             m ys (if x == y then a_b else (ys,xs)) xs
  4117           end
  4118     in
  4119       fn l => m [] ([],l) l
  4120     end;
  4121 
  4122 fun updateNth (n,x) l =
  4123     let
  4124       val (a,b) = Useful.revDivide l n
  4125     in
  4126       case b of
  4127         [] => raise Subscript
  4128       | h :: t => if x == h then l else List.revAppend (a, x :: t)
  4129     end;
  4130 
  4131 fun setify l =
  4132     let
  4133       val l' = Useful.setify l
  4134     in
  4135       if length l' = length l then l else l'
  4136     end;
  4137 
  4138 (* ------------------------------------------------------------------------- *)
  4139 (* Function caching.                                                         *)
  4140 (* ------------------------------------------------------------------------- *)
  4141 
  4142 fun cache cmp f =
  4143     let
  4144       val cache = Unsynchronized.ref (Map.new cmp)
  4145     in
  4146       fn a =>
  4147          case Map.peek (!cache) a of
  4148            SOME b => b
  4149          | NONE =>
  4150            let
  4151              val b = f a
  4152              val () = cache := Map.insert (!cache) (a,b)
  4153            in
  4154              b
  4155            end
  4156     end;
  4157 
  4158 (* ------------------------------------------------------------------------- *)
  4159 (* Hash consing.                                                             *)
  4160 (* ------------------------------------------------------------------------- *)
  4161 
  4162 fun hashCons cmp = cache cmp Useful.I;
  4163 
  4164 end
  4165 end;
  4166 
  4167 (**** Original file: Stream.sig ****)
  4168 
  4169 (* ========================================================================= *)
  4170 (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML                                *)
  4171 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  4172 (* ========================================================================= *)
  4173 
  4174 signature Stream =
  4175 sig
  4176 
  4177 (* ------------------------------------------------------------------------- *)
  4178 (* The stream type                                                           *)
  4179 (* ------------------------------------------------------------------------- *)
  4180 
  4181 datatype 'a stream = NIL | CONS of 'a * (unit -> 'a stream)
  4182 
  4183 (* If you're wondering how to create an infinite stream: *)
  4184 (* val stream4 = let fun s4 () = Metis.Stream.CONS (4,s4) in s4 () end; *)
  4185 
  4186 (* ------------------------------------------------------------------------- *)
  4187 (* Stream constructors                                                       *)
  4188 (* ------------------------------------------------------------------------- *)
  4189 
  4190 val repeat : 'a -> 'a stream
  4191 
  4192 val count : int -> int stream
  4193 
  4194 val funpows : ('a -> 'a) -> 'a -> 'a stream
  4195 
  4196 (* ------------------------------------------------------------------------- *)
  4197 (* Stream versions of standard list operations: these should all terminate   *)
  4198 (* ------------------------------------------------------------------------- *)
  4199 
  4200 val cons : 'a -> (unit -> 'a stream) -> 'a stream
  4201 
  4202 val null : 'a stream -> bool
  4203 
  4204 val hd : 'a stream -> 'a  (* raises Empty *)
  4205 
  4206 val tl : 'a stream -> 'a stream  (* raises Empty *)
  4207 
  4208 val hdTl : 'a stream -> 'a * 'a stream  (* raises Empty *)
  4209 
  4210 val singleton : 'a -> 'a stream
  4211 
  4212 val append : 'a stream -> (unit -> 'a stream) -> 'a stream
  4213 
  4214 val map : ('a -> 'b) -> 'a stream -> 'b stream
  4215 
  4216 val maps : ('a -> 's -> 'b * 's) -> 's -> 'a stream -> 'b stream
  4217 
  4218 val zipwith : ('a -> 'b -> 'c) -> 'a stream -> 'b stream -> 'c stream
  4219 
  4220 val zip : 'a stream -> 'b stream -> ('a * 'b) stream
  4221 
  4222 val take : int -> 'a stream -> 'a stream  (* raises Subscript *)
  4223 
  4224 val drop : int -> 'a stream -> 'a stream  (* raises Subscript *)
  4225 
  4226 (* ------------------------------------------------------------------------- *)
  4227 (* Stream versions of standard list operations: these might not terminate    *)
  4228 (* ------------------------------------------------------------------------- *)
  4229 
  4230 val length : 'a stream -> int
  4231 
  4232 val exists : ('a -> bool) -> 'a stream -> bool
  4233 
  4234 val all : ('a -> bool) -> 'a stream -> bool
  4235 
  4236 val filter : ('a -> bool) -> 'a stream -> 'a stream
  4237 
  4238 val foldl : ('a * 's -> 's) -> 's -> 'a stream -> 's
  4239 
  4240 val concat : 'a stream stream -> 'a stream
  4241 
  4242 val mapPartial : ('a -> 'b option) -> 'a stream -> 'b stream
  4243 
  4244 val mapsPartial : ('a -> 's -> 'b option * 's) -> 's -> 'a stream -> 'b stream
  4245 
  4246 (* ------------------------------------------------------------------------- *)
  4247 (* Stream operations                                                         *)
  4248 (* ------------------------------------------------------------------------- *)
  4249 
  4250 val memoize : 'a stream -> 'a stream
  4251 
  4252 val toList : 'a stream -> 'a list
  4253 
  4254 val fromList : 'a list -> 'a stream
  4255 
  4256 val toString : char stream -> string
  4257 
  4258 val fromString : string -> char stream
  4259 
  4260 val toTextFile : {filename : string} -> string stream -> unit
  4261 
  4262 val fromTextFile : {filename : string} -> string stream  (* line by line *)
  4263 
  4264 end
  4265 
  4266 (**** Original file: Stream.sml ****)
  4267 
  4268 structure Metis = struct open Metis
  4269 (* Metis-specific ML environment *)
  4270 nonfix ++ -- RL mem union subset;
  4271 val explode = String.explode;
  4272 val implode = String.implode;
  4273 val print = TextIO.print;
  4274 (* ========================================================================= *)
  4275 (* A POSSIBLY-INFINITE STREAM DATATYPE FOR ML                                *)
  4276 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  4277 (* ========================================================================= *)
  4278 
  4279 structure Stream :> Stream =
  4280 struct
  4281 
  4282 val K = Useful.K;
  4283 
  4284 val pair = Useful.pair;
  4285 
  4286 val funpow = Useful.funpow;
  4287 
  4288 (* ------------------------------------------------------------------------- *)
  4289 (* The datatype declaration encapsulates all the primitive operations        *)
  4290 (* ------------------------------------------------------------------------- *)
  4291 
  4292 datatype 'a stream =
  4293     NIL
  4294   | CONS of 'a * (unit -> 'a stream);
  4295 
  4296 (* ------------------------------------------------------------------------- *)
  4297 (* Stream constructors                                                       *)
  4298 (* ------------------------------------------------------------------------- *)
  4299 
  4300 fun repeat x = let fun rep () = CONS (x,rep) in rep () end;
  4301 
  4302 fun count n = CONS (n, fn () => count (n + 1));
  4303 
  4304 fun funpows f x = CONS (x, fn () => funpows f (f x));
  4305 
  4306 (* ------------------------------------------------------------------------- *)
  4307 (* Stream versions of standard list operations: these should all terminate   *)
  4308 (* ------------------------------------------------------------------------- *)
  4309 
  4310 fun cons h t = CONS (h,t);
  4311 
  4312 fun null NIL = true | null (CONS _) = false;
  4313 
  4314 fun hd NIL = raise Empty
  4315   | hd (CONS (h,_)) = h;
  4316 
  4317 fun tl NIL = raise Empty
  4318   | tl (CONS (_,t)) = t ();
  4319 
  4320 fun hdTl s = (hd s, tl s);
  4321 
  4322 fun singleton s = CONS (s, K NIL);
  4323 
  4324 fun append NIL s = s ()
  4325   | append (CONS (h,t)) s = CONS (h, fn () => append (t ()) s);
  4326 
  4327 fun map f =
  4328     let
  4329       fun m NIL = NIL
  4330         | m (CONS (h, t)) = CONS (f h, fn () => m (t ()))
  4331     in
  4332       m
  4333     end;
  4334 
  4335 fun maps f =
  4336     let
  4337       fun mm _ NIL = NIL
  4338         | mm s (CONS (x, xs)) =
  4339           let
  4340             val (y, s') = f x s
  4341           in
  4342             CONS (y, fn () => mm s' (xs ()))
  4343           end
  4344     in
  4345       mm
  4346     end;
  4347 
  4348 fun zipwith f =
  4349     let
  4350       fun z NIL _ = NIL
  4351         | z _ NIL = NIL
  4352         | z (CONS (x,xs)) (CONS (y,ys)) =
  4353           CONS (f x y, fn () => z (xs ()) (ys ()))
  4354     in
  4355       z
  4356     end;
  4357 
  4358 fun zip s t = zipwith pair s t;
  4359 
  4360 fun take 0 _ = NIL
  4361   | take n NIL = raise Subscript
  4362   | take 1 (CONS (x,_)) = CONS (x, K NIL)
  4363   | take n (CONS (x,xs)) = CONS (x, fn () => take (n - 1) (xs ()));
  4364 
  4365 fun drop n s = funpow n tl s handle Empty => raise Subscript;
  4366 
  4367 (* ------------------------------------------------------------------------- *)
  4368 (* Stream versions of standard list operations: these might not terminate    *)
  4369 (* ------------------------------------------------------------------------- *)
  4370 
  4371 local
  4372   fun len n NIL = n
  4373     | len n (CONS (_,t)) = len (n + 1) (t ());
  4374 in
  4375   fun length s = len 0 s;
  4376 end;
  4377 
  4378 fun exists pred =
  4379     let
  4380       fun f NIL = false
  4381         | f (CONS (h,t)) = pred h orelse f (t ())
  4382     in
  4383       f
  4384     end;
  4385 
  4386 fun all pred = not o exists (not o pred);
  4387 
  4388 fun filter p NIL = NIL
  4389   | filter p (CONS (x,xs)) =
  4390     if p x then CONS (x, fn () => filter p (xs ())) else filter p (xs ());
  4391 
  4392 fun foldl f =
  4393     let
  4394       fun fold b NIL = b
  4395         | fold b (CONS (h,t)) = fold (f (h,b)) (t ())
  4396     in
  4397       fold
  4398     end;
  4399 
  4400 fun concat NIL = NIL
  4401   | concat (CONS (NIL, ss)) = concat (ss ())
  4402   | concat (CONS (CONS (x, xs), ss)) =
  4403     CONS (x, fn () => concat (CONS (xs (), ss)));
  4404 
  4405 fun mapPartial f =
  4406     let
  4407       fun mp NIL = NIL
  4408         | mp (CONS (h,t)) =
  4409           case f h of
  4410             NONE => mp (t ())
  4411           | SOME h' => CONS (h', fn () => mp (t ()))
  4412     in
  4413       mp
  4414     end;
  4415 
  4416 fun mapsPartial f =
  4417     let
  4418       fun mm _ NIL = NIL
  4419         | mm s (CONS (x, xs)) =
  4420           let
  4421             val (yo, s') = f x s
  4422             val t = mm s' o xs
  4423           in
  4424             case yo of NONE => t () | SOME y => CONS (y, t)
  4425           end
  4426     in
  4427       mm
  4428     end;
  4429 
  4430 (* ------------------------------------------------------------------------- *)
  4431 (* Stream operations                                                         *)
  4432 (* ------------------------------------------------------------------------- *)
  4433 
  4434 fun memoize NIL = NIL
  4435   | memoize (CONS (h,t)) = CONS (h, Lazy.memoize (fn () => memoize (t ())));
  4436 
  4437 local
  4438   fun toLst res NIL = rev res
  4439     | toLst res (CONS (x, xs)) = toLst (x :: res) (xs ());
  4440 in
  4441   fun toList s = toLst [] s;
  4442 end;
  4443 
  4444 fun fromList [] = NIL
  4445   | fromList (x :: xs) = CONS (x, fn () => fromList xs);
  4446 
  4447 fun toString s = implode (toList s);
  4448 
  4449 fun fromString s = fromList (explode s);
  4450 
  4451 fun toTextFile {filename = f} s =
  4452     let
  4453       val (h,close) =
  4454           if f = "-" then (TextIO.stdOut, K ())
  4455           else (TextIO.openOut f, TextIO.closeOut)
  4456 
  4457       fun toFile NIL = ()
  4458         | toFile (CONS (x,y)) = (TextIO.output (h,x); toFile (y ()))
  4459 
  4460       val () = toFile s
  4461     in
  4462       close h
  4463     end;
  4464 
  4465 fun fromTextFile {filename = f} =
  4466     let
  4467       val (h,close) =
  4468           if f = "-" then (TextIO.stdIn, K ())
  4469           else (TextIO.openIn f, TextIO.closeIn)
  4470 
  4471       fun strm () =
  4472           case TextIO.inputLine h of
  4473             NONE => (close h; NIL)
  4474           | SOME s => CONS (s,strm)
  4475     in
  4476       memoize (strm ())
  4477     end;
  4478 
  4479 end
  4480 end;
  4481 
  4482 (**** Original file: Heap.sig ****)
  4483 
  4484 (* ========================================================================= *)
  4485 (* A HEAP DATATYPE FOR ML                                                    *)
  4486 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  4487 (* ========================================================================= *)
  4488 
  4489 signature Heap =
  4490 sig
  4491 
  4492 type 'a heap
  4493 
  4494 val new : ('a * 'a -> order) -> 'a heap
  4495 
  4496 val add : 'a heap -> 'a -> 'a heap
  4497 
  4498 val null : 'a heap -> bool
  4499 
  4500 val top : 'a heap -> 'a  (* raises Empty *)
  4501 
  4502 val remove : 'a heap -> 'a * 'a heap  (* raises Empty *)
  4503 
  4504 val size : 'a heap -> int
  4505 
  4506 val app : ('a -> unit) -> 'a heap -> unit
  4507 
  4508 val toList : 'a heap -> 'a list
  4509 
  4510 val toStream : 'a heap -> 'a Metis.Stream.stream
  4511 
  4512 val toString : 'a heap -> string
  4513 
  4514 end
  4515 
  4516 (**** Original file: Heap.sml ****)
  4517 
  4518 structure Metis = struct open Metis
  4519 (* Metis-specific ML environment *)
  4520 nonfix ++ -- RL mem union subset;
  4521 val explode = String.explode;
  4522 val implode = String.implode;
  4523 val print = TextIO.print;
  4524 (* ========================================================================= *)
  4525 (* A HEAP DATATYPE FOR ML                                                    *)
  4526 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  4527 (* ========================================================================= *)
  4528 
  4529 structure Heap :> Heap =
  4530 struct
  4531 
  4532 (* Leftist heaps as in Purely Functional Data Structures, by Chris Okasaki *)
  4533 
  4534 datatype 'a node = E | T of int * 'a * 'a node * 'a node;
  4535 
  4536 datatype 'a heap = Heap of ('a * 'a -> order) * int * 'a node;
  4537 
  4538 fun rank E = 0
  4539   | rank (T (r,_,_,_)) = r;
  4540 
  4541 fun makeT (x,a,b) =
  4542   if rank a >= rank b then T (rank b + 1, x, a, b) else T (rank a + 1, x, b, a);
  4543 
  4544 fun merge cmp =
  4545     let
  4546       fun mrg (h,E) = h
  4547         | mrg (E,h) = h
  4548         | mrg (h1 as T (_,x,a1,b1), h2 as T (_,y,a2,b2)) =
  4549           case cmp (x,y) of
  4550             GREATER => makeT (y, a2, mrg (h1,b2))
  4551           | _ => makeT (x, a1, mrg (b1,h2))
  4552     in
  4553       mrg
  4554     end;
  4555 
  4556 fun new cmp = Heap (cmp,0,E);
  4557 
  4558 fun add (Heap (f,n,a)) x = Heap (f, n + 1, merge f (T (1,x,E,E), a));
  4559 
  4560 fun size (Heap (_, n, _)) = n;
  4561 
  4562 fun null h = size h = 0;
  4563 
  4564 fun top (Heap (_,_,E)) = raise Empty
  4565   | top (Heap (_, _, T (_,x,_,_))) = x;
  4566 
  4567 fun remove (Heap (_,_,E)) = raise Empty
  4568   | remove (Heap (f, n, T (_,x,a,b))) = (x, Heap (f, n - 1, merge f (a,b)));
  4569 
  4570 fun app f =
  4571     let
  4572       fun ap [] = ()
  4573         | ap (E :: rest) = ap rest
  4574         | ap (T (_,d,a,b) :: rest) = (f d; ap (a :: b :: rest))
  4575     in
  4576       fn Heap (_,_,a) => ap [a]
  4577     end;
  4578 
  4579 fun toList h =
  4580     if null h then []
  4581     else
  4582       let
  4583         val (x,h) = remove h
  4584       in
  4585         x :: toList h
  4586       end;
  4587 
  4588 fun toStream h =
  4589     if null h then Stream.NIL
  4590     else
  4591       let
  4592         val (x,h) = remove h
  4593       in
  4594         Stream.CONS (x, fn () => toStream h)
  4595       end;
  4596 
  4597 fun toString h =
  4598     "Heap[" ^ (if null h then "" else Int.toString (size h)) ^ "]";
  4599 
  4600 end
  4601 end;
  4602 
  4603 (**** Original file: Parser.sig ****)
  4604 
  4605 (* ========================================================================= *)
  4606 (* PARSING AND PRETTY PRINTING                                               *)
  4607 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  4608 (* ========================================================================= *)
  4609 
  4610 signature Parser =
  4611 sig
  4612 
  4613 (* ------------------------------------------------------------------------- *)
  4614 (* Pretty printing for built-in types                                        *)
  4615 (* ------------------------------------------------------------------------- *)
  4616 
  4617 type ppstream = Metis.PP.ppstream
  4618 
  4619 datatype breakStyle = Consistent | Inconsistent
  4620 
  4621 type 'a pp = ppstream -> 'a -> unit
  4622 
  4623 val lineLength : int Unsynchronized.ref
  4624 
  4625 val beginBlock : ppstream -> breakStyle -> int -> unit
  4626 
  4627 val endBlock : ppstream -> unit
  4628 
  4629 val addString : ppstream -> string -> unit
  4630 
  4631 val addBreak : ppstream -> int * int -> unit
  4632 
  4633 val addNewline : ppstream -> unit
  4634 
  4635 val ppMap : ('a -> 'b) -> 'b pp -> 'a pp
  4636 
  4637 val ppBracket : string -> string -> 'a pp -> 'a pp
  4638 
  4639 val ppSequence : string -> 'a pp -> 'a list pp
  4640 
  4641 val ppBinop : string -> 'a pp -> 'b pp -> ('a * 'b) pp
  4642 
  4643 val ppChar : char pp
  4644 
  4645 val ppString : string pp
  4646 
  4647 val ppUnit : unit pp
  4648 
  4649 val ppBool : bool pp
  4650 
  4651 val ppInt : int pp
  4652 
  4653 val ppReal : real pp
  4654 
  4655 val ppOrder : order pp
  4656 
  4657 val ppList : 'a pp -> 'a list pp
  4658 
  4659 val ppOption : 'a pp -> 'a option pp
  4660 
  4661 val ppPair : 'a pp -> 'b pp -> ('a * 'b) pp
  4662 
  4663 val ppTriple : 'a pp -> 'b pp -> 'c pp -> ('a * 'b * 'c) pp
  4664 
  4665 val toString : 'a pp -> 'a -> string  (* Uses !lineLength *)
  4666 
  4667 val fromString : ('a -> string) -> 'a pp
  4668 
  4669 val ppTrace : 'a pp -> string -> 'a -> unit
  4670 
  4671 (* ------------------------------------------------------------------------- *)
  4672 (* Recursive descent parsing combinators                                     *)
  4673 (* ------------------------------------------------------------------------- *)
  4674 
  4675 (* Generic parsers
  4676 
  4677 Recommended fixities:
  4678   infixr 9 >>++
  4679   infixr 8 ++
  4680   infixr 7 >>
  4681   infixr 6 ||
  4682 *)
  4683 
  4684 exception NoParse
  4685 
  4686 val error : 'a -> 'b * 'a
  4687 
  4688 val ++ : ('a -> 'b * 'a) * ('a -> 'c * 'a) -> 'a -> ('b * 'c) * 'a
  4689 
  4690 val >> : ('a -> 'b * 'a) * ('b -> 'c) -> 'a -> 'c * 'a
  4691 
  4692 val >>++ : ('a -> 'b * 'a) * ('b -> 'a -> 'c * 'a) -> 'a -> 'c * 'a
  4693 
  4694 val || : ('a -> 'b * 'a) * ('a -> 'b * 'a) -> 'a -> 'b * 'a
  4695 
  4696 val first : ('a -> 'b * 'a) list -> 'a -> 'b * 'a
  4697 
  4698 val mmany : ('s -> 'a -> 's * 'a) -> 's -> 'a -> 's * 'a
  4699 
  4700 val many : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
  4701 
  4702 val atLeastOne : ('a -> 'b * 'a) -> 'a -> 'b list * 'a
  4703 
  4704 val nothing : 'a -> unit * 'a
  4705 
  4706 val optional : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
  4707 
  4708 (* Stream based parsers *)
  4709 
  4710 type ('a,'b) parser = 'a Metis.Stream.stream -> 'b * 'a Metis.Stream.stream
  4711 
  4712 val everything : ('a, 'b list) parser -> 'a Metis.Stream.stream -> 'b Metis.Stream.stream
  4713 
  4714 val maybe : ('a -> 'b option) -> ('a,'b) parser
  4715 
  4716 val finished : ('a,unit) parser
  4717 
  4718 val some : ('a -> bool) -> ('a,'a) parser
  4719 
  4720 val any : ('a,'a) parser
  4721 
  4722 val exact : ''a -> (''a,''a) parser
  4723 
  4724 (* ------------------------------------------------------------------------- *)
  4725 (* Infix operators                                                           *)
  4726 (* ------------------------------------------------------------------------- *)
  4727 
  4728 type infixities = {token : string, precedence : int, leftAssoc : bool} list
  4729 
  4730 val infixTokens : infixities -> string list
  4731 
  4732 val parseInfixes :
  4733     infixities -> (string * 'a * 'a -> 'a) -> (string,'a) parser ->
  4734     (string,'a) parser
  4735 
  4736 val ppInfixes :
  4737     infixities -> ('a -> (string * 'a * 'a) option) -> ('a * bool) pp ->
  4738     ('a * bool) pp
  4739 
  4740 (* ------------------------------------------------------------------------- *)
  4741 (* Quotations                                                                *)
  4742 (* ------------------------------------------------------------------------- *)
  4743 
  4744 type 'a quotation = 'a Metis.frag list
  4745 
  4746 val parseQuotation : ('a -> string) -> (string -> 'b) -> 'a quotation -> 'b
  4747 
  4748 end
  4749 
  4750 (**** Original file: Parser.sml ****)
  4751 
  4752 structure Metis = struct open Metis
  4753 (* Metis-specific ML environment *)
  4754 nonfix ++ -- RL mem union subset;
  4755 val explode = String.explode;
  4756 val implode = String.implode;
  4757 val print = TextIO.print;
  4758 (* ========================================================================= *)
  4759 (* PARSER COMBINATORS                                                        *)
  4760 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  4761 (* ========================================================================= *)
  4762 
  4763 structure Parser :> Parser =
  4764 struct
  4765 
  4766 infixr 9 >>++
  4767 infixr 8 ++
  4768 infixr 7 >>
  4769 infixr 6 ||
  4770 
  4771 (* ------------------------------------------------------------------------- *)
  4772 (* Helper functions.                                                         *)
  4773 (* ------------------------------------------------------------------------- *)
  4774 
  4775 exception Bug = Useful.Bug;
  4776 
  4777 val trace = Useful.trace
  4778 and equal = Useful.equal
  4779 and I = Useful.I
  4780 and K = Useful.K
  4781 and C = Useful.C
  4782 and fst = Useful.fst
  4783 and snd = Useful.snd
  4784 and pair = Useful.pair
  4785 and curry = Useful.curry
  4786 and funpow = Useful.funpow
  4787 and mem = Useful.mem
  4788 and sortMap = Useful.sortMap;
  4789 
  4790 (* ------------------------------------------------------------------------- *)
  4791 (* Pretty printing for built-in types                                        *)
  4792 (* ------------------------------------------------------------------------- *)
  4793 
  4794 type ppstream = PP.ppstream
  4795 
  4796 datatype breakStyle = Consistent | Inconsistent
  4797 
  4798 type 'a pp = PP.ppstream -> 'a -> unit;
  4799 
  4800 val lineLength = Unsynchronized.ref 75;
  4801 
  4802 fun beginBlock pp Consistent = PP.begin_block pp PP.CONSISTENT
  4803   | beginBlock pp Inconsistent = PP.begin_block pp PP.INCONSISTENT;
  4804 
  4805 val endBlock = PP.end_block
  4806 and addString = PP.add_string
  4807 and addBreak = PP.add_break
  4808 and addNewline = PP.add_newline;
  4809 
  4810 fun ppMap f ppA (ppstrm : PP.ppstream) x : unit = ppA ppstrm (f x);
  4811 
  4812 fun ppBracket l r ppA pp a =
  4813     let
  4814       val ln = size l
  4815     in
  4816       beginBlock pp Inconsistent ln;
  4817       if ln = 0 then () else addString pp l;
  4818       ppA pp a;
  4819       if r = "" then () else addString pp r;
  4820       endBlock pp
  4821     end;
  4822 
  4823 fun ppSequence sep ppA pp =
  4824     let
  4825       fun ppX x = (addString pp sep; addBreak pp (1,0); ppA pp x)
  4826     in
  4827       fn [] => ()
  4828        | h :: t =>
  4829          (beginBlock pp Inconsistent 0;
  4830           ppA pp h;
  4831           app ppX t;
  4832           endBlock pp)
  4833     end;
  4834 
  4835 fun ppBinop s ppA ppB pp (a,b) =
  4836     (beginBlock pp Inconsistent 0;
  4837       ppA pp a;
  4838       if s = "" then () else addString pp s;
  4839       addBreak pp (1,0);
  4840       ppB pp b;
  4841       endBlock pp);
  4842 
  4843 fun ppTrinop ab bc ppA ppB ppC pp (a,b,c) =
  4844     (beginBlock pp Inconsistent 0;
  4845      ppA pp a;
  4846      if ab = "" then () else addString pp ab;
  4847      addBreak pp (1,0);
  4848      ppB pp b;
  4849      if bc = "" then () else addString pp bc;
  4850      addBreak pp (1,0);
  4851      ppC pp c;
  4852      endBlock pp);
  4853 
  4854 (* Pretty-printers for common types *)
  4855 
  4856 fun ppString pp s =
  4857     (beginBlock pp Inconsistent 0;
  4858      addString pp s;
  4859      endBlock pp);
  4860 
  4861 val ppUnit = ppMap (fn () => "()") ppString;
  4862 
  4863 val ppChar = ppMap str ppString;
  4864 
  4865 val ppBool = ppMap (fn true => "true" | false => "false") ppString;
  4866 
  4867 val ppInt = ppMap Int.toString ppString;
  4868 
  4869 val ppReal = ppMap Real.toString ppString;
  4870 
  4871 val ppOrder =
  4872     let
  4873       fun f LESS = "Less"
  4874         | f EQUAL = "Equal"
  4875         | f GREATER = "Greater"
  4876     in
  4877       ppMap f ppString
  4878     end;
  4879 
  4880 fun ppList ppA = ppBracket "[" "]" (ppSequence "," ppA);
  4881 
  4882 fun ppOption _ pp NONE = ppString pp "-"
  4883   | ppOption ppA pp (SOME a) = ppA pp a;
  4884 
  4885 fun ppPair ppA ppB = ppBracket "(" ")" (ppBinop "," ppA ppB);
  4886 
  4887 fun ppTriple ppA ppB ppC = ppBracket "(" ")" (ppTrinop "," "," ppA ppB ppC);
  4888 
  4889 (* Keep eta expanded to evaluate lineLength when supplied with a *)
  4890 fun toString ppA a = PP.pp_to_string (!lineLength) ppA a;
  4891 
  4892 fun fromString toS = ppMap toS ppString;
  4893 
  4894 fun ppTrace ppX nameX x =
  4895     trace (toString (ppBinop " =" ppString ppX) (nameX,x) ^ "\n");
  4896 
  4897 (* ------------------------------------------------------------------------- *)
  4898 (* Generic.                                                                  *)
  4899 (* ------------------------------------------------------------------------- *)
  4900 
  4901 exception NoParse;
  4902 
  4903 val error : 'a -> 'b * 'a = fn _ => raise NoParse;
  4904 
  4905 fun op ++ (parser1,parser2) input =
  4906     let
  4907       val (result1,input) = parser1 input
  4908       val (result2,input) = parser2 input
  4909     in
  4910       ((result1,result2),input)
  4911     end;
  4912 
  4913 fun op >> (parser : 'a -> 'b * 'a, treatment) input =
  4914     let
  4915       val (result,input) = parser input
  4916     in
  4917       (treatment result, input)
  4918     end;
  4919 
  4920 fun op >>++ (parser,treatment) input =
  4921     let
  4922       val (result,input) = parser input
  4923     in
  4924       treatment result input
  4925     end;
  4926 
  4927 fun op || (parser1,parser2) input =
  4928     parser1 input handle NoParse => parser2 input;
  4929 
  4930 fun first [] _ = raise NoParse
  4931   | first (parser :: parsers) input = (parser || first parsers) input;
  4932 
  4933 fun mmany parser state input =
  4934     let
  4935       val (state,input) = parser state input
  4936     in
  4937       mmany parser state input
  4938     end
  4939     handle NoParse => (state,input);
  4940 
  4941 fun many parser =
  4942     let
  4943       fun sparser l = parser >> (fn x => x :: l)
  4944     in
  4945       mmany sparser [] >> rev      
  4946     end;
  4947 
  4948 fun atLeastOne p = (p ++ many p) >> op::;
  4949 
  4950 fun nothing input = ((),input);
  4951 
  4952 fun optional p = (p >> SOME) || (nothing >> K NONE);
  4953 
  4954 (* ------------------------------------------------------------------------- *)
  4955 (* Stream-based.                                                             *)
  4956 (* ------------------------------------------------------------------------- *)
  4957 
  4958 type ('a,'b) parser = 'a Stream.stream -> 'b * 'a Stream.stream
  4959 
  4960 fun everything parser =
  4961     let
  4962       fun f input =
  4963           let
  4964             val (result,input) = parser input
  4965           in
  4966             Stream.append (Stream.fromList result) (fn () => f input)
  4967           end
  4968           handle NoParse =>
  4969             if Stream.null input then Stream.NIL else raise NoParse
  4970     in
  4971       f
  4972     end;
  4973 
  4974 fun maybe p Stream.NIL = raise NoParse
  4975   | maybe p (Stream.CONS (h,t)) =
  4976     case p h of SOME r => (r, t ()) | NONE => raise NoParse;
  4977 
  4978 fun finished Stream.NIL = ((), Stream.NIL)
  4979   | finished (Stream.CONS _) = raise NoParse;
  4980 
  4981 fun some p = maybe (fn x => if p x then SOME x else NONE);
  4982 
  4983 fun any input = some (K true) input;
  4984 
  4985 fun exact tok = some (fn item => item = tok);
  4986 
  4987 (* ------------------------------------------------------------------------- *)
  4988 (* Parsing and pretty-printing for infix operators.                          *)
  4989 (* ------------------------------------------------------------------------- *)
  4990 
  4991 type infixities = {token : string, precedence : int, leftAssoc : bool} list;
  4992 
  4993 local
  4994   fun unflatten ({token,precedence,leftAssoc}, ([],_)) =
  4995       ([(leftAssoc, [token])], precedence)
  4996     | unflatten ({token,precedence,leftAssoc}, ((a,l) :: dealt, p)) =
  4997       if p = precedence then
  4998         let
  4999           val _ = leftAssoc = a orelse
  5000                   raise Bug "infix parser/printer: mixed assocs"
  5001         in
  5002           ((a, token :: l) :: dealt, p)
  5003         end
  5004       else
  5005         ((leftAssoc,[token]) :: (a,l) :: dealt, precedence);
  5006 in
  5007   fun layerOps infixes =
  5008       let
  5009         val infixes = sortMap #precedence Int.compare infixes
  5010         val (parsers,_) = foldl unflatten ([],0) infixes
  5011       in
  5012         parsers
  5013       end;
  5014 end;
  5015 
  5016 local
  5017   fun chop (#" " :: chs) = let val (n,l) = chop chs in (n + 1, l) end
  5018     | chop chs = (0,chs);
  5019 
  5020   fun nspaces n = funpow n (curry op^ " ") "";
  5021 
  5022   fun spacify tok =
  5023       let
  5024         val chs = explode tok
  5025         val (r,chs) = chop (rev chs)
  5026         val (l,chs) = chop (rev chs)
  5027       in
  5028         ((l,r), implode chs)
  5029       end;
  5030 
  5031   fun lrspaces (l,r) =
  5032       (if l = 0 then K () else C addString (nspaces l),
  5033        if r = 0 then K () else C addBreak (r, 0));
  5034 in
  5035   fun opSpaces s = let val (l_r,s) = spacify s in (lrspaces l_r, s) end;
  5036 
  5037   val opClean = snd o spacify;
  5038 end;
  5039 
  5040 val infixTokens : infixities -> string list =
  5041     List.map (fn {token,...} => opClean token);
  5042 
  5043 fun parseGenInfix update sof toks parse inp =
  5044     let
  5045       val (e, rest) = parse inp
  5046                       
  5047       val continue =
  5048           case rest of
  5049             Stream.NIL => NONE
  5050           | Stream.CONS (h, t) => if mem h toks then SOME (h, t) else NONE
  5051     in
  5052       case continue of
  5053         NONE => (sof e, rest)
  5054       | SOME (h,t) => parseGenInfix update (update sof h e) toks parse (t ())
  5055     end;
  5056 
  5057 fun parseLeftInfix toks con =
  5058     parseGenInfix (fn f => fn t => fn a => fn b => con (t, f a, b)) I toks;
  5059 
  5060 fun parseRightInfix toks con =
  5061     parseGenInfix (fn f => fn t => fn a => fn b => f (con (t, a, b))) I toks;
  5062 
  5063 fun parseInfixes ops =
  5064     let
  5065       fun layeredOp (x,y) = (x, List.map opClean y)
  5066 
  5067       val layeredOps = List.map layeredOp (layerOps ops)
  5068 
  5069       fun iparser (a,t) = (if a then parseLeftInfix else parseRightInfix) t
  5070 
  5071       val iparsers = List.map iparser layeredOps
  5072     in
  5073       fn con => fn subparser => foldl (fn (p,sp) => p con sp) subparser iparsers
  5074     end;
  5075 
  5076 fun ppGenInfix left toks =
  5077     let
  5078       val spc = List.map opSpaces toks
  5079     in
  5080       fn dest => fn ppSub =>
  5081       let
  5082         fun dest' tm =
  5083             case dest tm of
  5084               NONE => NONE
  5085             | SOME (t, a, b) =>
  5086               Option.map (pair (a,b)) (List.find (equal t o snd) spc)
  5087 
  5088         open PP
  5089 
  5090         fun ppGo pp (tmr as (tm,r)) =
  5091             case dest' tm of
  5092               NONE => ppSub pp tmr
  5093             | SOME ((a,b),((lspc,rspc),tok)) =>
  5094               ((if left then ppGo else ppSub) pp (a,true);
  5095                lspc pp; addString pp tok; rspc pp;
  5096                (if left then ppSub else ppGo) pp (b,r))
  5097       in
  5098         fn pp => fn tmr as (tm,_) =>
  5099         case dest' tm of
  5100           NONE => ppSub pp tmr
  5101         | SOME _ => (beginBlock pp Inconsistent 0; ppGo pp tmr; endBlock pp)
  5102       end
  5103     end;
  5104 
  5105 fun ppLeftInfix toks = ppGenInfix true toks;
  5106 
  5107 fun ppRightInfix toks = ppGenInfix false toks;
  5108 
  5109 fun ppInfixes ops =
  5110     let
  5111       val layeredOps = layerOps ops
  5112                        
  5113       val toks = List.concat (List.map (List.map opClean o snd) layeredOps)
  5114                  
  5115       fun iprinter (a,t) = (if a then ppLeftInfix else ppRightInfix) t
  5116                            
  5117       val iprinters = List.map iprinter layeredOps
  5118     in
  5119       fn dest => fn ppSub =>
  5120       let
  5121         fun printer sub = foldl (fn (ip,p) => ip dest p) sub iprinters
  5122 
  5123         fun isOp t = case dest t of SOME (x,_,_) => mem x toks | _ => false
  5124 
  5125         open PP
  5126 
  5127         fun subpr pp (tmr as (tm,_)) =
  5128             if isOp tm then
  5129               (beginBlock pp Inconsistent 1; addString pp "(";
  5130                printer subpr pp (tm, false); addString pp ")"; endBlock pp)
  5131             else ppSub pp tmr
  5132       in
  5133         fn pp => fn tmr =>
  5134         (beginBlock pp Inconsistent 0; printer subpr pp tmr; endBlock pp)
  5135       end
  5136     end;
  5137 
  5138 (* ------------------------------------------------------------------------- *)
  5139 (* Quotations                                                                *)
  5140 (* ------------------------------------------------------------------------- *)
  5141 
  5142 type 'a quotation = 'a frag list;
  5143 
  5144 fun parseQuotation printer parser quote =
  5145   let
  5146     fun expand (QUOTE q, s) = s ^ q
  5147       | expand (ANTIQUOTE a, s) = s ^ printer a
  5148 
  5149     val string = foldl expand "" quote
  5150   in
  5151     parser string
  5152   end;
  5153 
  5154 end
  5155 end;
  5156 
  5157 (**** Original file: Options.sig ****)
  5158 
  5159 (* ========================================================================= *)
  5160 (* PROCESSING COMMAND LINE OPTIONS                                           *)
  5161 (* Copyright (c) 2003-2004 Joe Hurd, distributed under the BSD License *)
  5162 (* ========================================================================= *)
  5163 
  5164 signature Options =
  5165 sig
  5166 
  5167 (* ------------------------------------------------------------------------- *)
  5168 (* Option processors take an option with its associated arguments.           *)
  5169 (* ------------------------------------------------------------------------- *)
  5170 
  5171 type proc = string * string list -> unit
  5172 
  5173 type ('a,'x) mkProc = ('x -> proc) -> ('a -> 'x) -> proc
  5174 
  5175 (* ------------------------------------------------------------------------- *)
  5176 (* One command line option: names, arguments, description and a processor.   *)
  5177 (* ------------------------------------------------------------------------- *)
  5178 
  5179 type opt =
  5180      {switches : string list, arguments : string list,
  5181       description : string, processor : proc}
  5182 
  5183 (* ------------------------------------------------------------------------- *)
  5184 (* Option processors may raise an OptionExit exception.                      *)
  5185 (* ------------------------------------------------------------------------- *)
  5186 
  5187 type optionExit = {message : string option, usage : bool, success : bool}
  5188 
  5189 exception OptionExit of optionExit
  5190 
  5191 (* ------------------------------------------------------------------------- *)
  5192 (* Constructing option processors.                                           *)
  5193 (* ------------------------------------------------------------------------- *)
  5194 
  5195 val beginOpt : (string,'x) mkProc
  5196 
  5197 val endOpt : unit -> proc
  5198 
  5199 val stringOpt : (string,'x) mkProc
  5200 
  5201 val intOpt : int option * int option -> (int,'x) mkProc
  5202 
  5203 val realOpt : real option * real option -> (real,'x) mkProc
  5204 
  5205 val enumOpt : string list -> (string,'x) mkProc
  5206 
  5207 val optionOpt : string * ('a,'x) mkProc -> ('a option,'x) mkProc
  5208 
  5209 (* ------------------------------------------------------------------------- *)
  5210 (* Basic options useful for all programs.                                    *)
  5211 (* ------------------------------------------------------------------------- *)
  5212 
  5213 val basicOptions : opt list
  5214 
  5215 (* ------------------------------------------------------------------------- *)
  5216 (* All the command line options of a program.                                *)
  5217 (* ------------------------------------------------------------------------- *)
  5218 
  5219 type allOptions =
  5220      {name : string, version : string, header : string,
  5221       footer : string, options : opt list}
  5222 
  5223 (* ------------------------------------------------------------------------- *)
  5224 (* Usage information.                                                        *)
  5225 (* ------------------------------------------------------------------------- *)
  5226 
  5227 val versionInformation : allOptions -> string
  5228 
  5229 val usageInformation : allOptions -> string
  5230 
  5231 (* ------------------------------------------------------------------------- *)
  5232 (* Exit the program gracefully.                                              *)
  5233 (* ------------------------------------------------------------------------- *)
  5234 
  5235 val exit : allOptions -> optionExit -> 'exit
  5236 
  5237 val succeed : allOptions -> 'exit
  5238 
  5239 val fail : allOptions -> string -> 'exit
  5240 
  5241 val usage : allOptions -> string -> 'exit
  5242 
  5243 val version : allOptions -> 'exit
  5244 
  5245 (* ------------------------------------------------------------------------- *)
  5246 (* Process the command line options passed to the program.                   *)
  5247 (* ------------------------------------------------------------------------- *)
  5248 
  5249 val processOptions : allOptions -> string list -> string list * string list
  5250 
  5251 end
  5252 
  5253 (**** Original file: Options.sml ****)
  5254 
  5255 structure Metis = struct open Metis
  5256 (* Metis-specific ML environment *)
  5257 nonfix ++ -- RL mem union subset;
  5258 val explode = String.explode;
  5259 val implode = String.implode;
  5260 val print = TextIO.print;
  5261 (* ========================================================================= *)
  5262 (* PROCESSING COMMAND LINE OPTIONS                                           *)
  5263 (* Copyright (c) 2003-2004 Joe Hurd, distributed under the BSD License *)
  5264 (* ========================================================================= *)
  5265 
  5266 structure Options :> Options =
  5267 struct
  5268 
  5269 infix ##
  5270 
  5271 open Useful;
  5272 
  5273 (* ------------------------------------------------------------------------- *)
  5274 (* One command line option: names, arguments, description and a processor    *)
  5275 (* ------------------------------------------------------------------------- *)
  5276 
  5277 type proc = string * string list -> unit;
  5278 
  5279 type ('a,'x) mkProc = ('x -> proc) -> ('a -> 'x) -> proc;
  5280 
  5281 type opt = {switches : string list, arguments : string list,
  5282             description : string, processor : proc};
  5283 
  5284 (* ------------------------------------------------------------------------- *)
  5285 (* Option processors may raise an OptionExit exception                       *)
  5286 (* ------------------------------------------------------------------------- *)
  5287 
  5288 type optionExit = {message : string option, usage : bool, success : bool};
  5289 
  5290 exception OptionExit of optionExit;
  5291 
  5292 (* ------------------------------------------------------------------------- *)
  5293 (* Wrappers for option processors                                            *)
  5294 (* ------------------------------------------------------------------------- *)
  5295 
  5296 fun beginOpt f p (s : string, l : string list) : unit = f (p s) (s,l);
  5297 
  5298 fun endOpt () (_ : string, [] : string list) = ()
  5299   | endOpt _ (_, _ :: _) = raise Bug "endOpt";
  5300 
  5301 fun stringOpt _ _ (_ : string, []) = raise Bug "stringOpt"
  5302   | stringOpt f p (s, (h : string) :: t) : unit = f (p h) (s,t);
  5303 
  5304 local
  5305   fun range NONE NONE = "Z"
  5306     | range (SOME i) NONE = "{n IN Z | " ^ Int.toString i ^ " <= n}"
  5307     | range NONE (SOME j) = "{n IN Z | n <= " ^ Int.toString j ^ "}"
  5308     | range (SOME i) (SOME j) =
  5309     "{n IN Z | " ^ Int.toString i ^ " <= n <= " ^ Int.toString j ^ "}";
  5310   fun oLeq (SOME x) (SOME y) = x <= y | oLeq _ _ = true;
  5311   fun argToInt arg omin omax x =
  5312     (case Int.fromString x of
  5313        SOME i =>
  5314        if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else
  5315          raise OptionExit
  5316            {success = false, usage = false, message =
  5317             SOME (arg ^ " option needs an integer argument in the range "
  5318                   ^ range omin omax ^ " (not " ^ x ^ ")")}
  5319      | NONE =>
  5320        raise OptionExit
  5321          {success = false, usage = false, message =
  5322           SOME (arg ^ " option needs an integer argument (not \"" ^ x ^ "\")")})
  5323     handle Overflow =>
  5324        raise OptionExit
  5325          {success = false, usage = false, message =
  5326           SOME (arg ^ " option suffered integer overflow on argument " ^ x)};
  5327 in
  5328   fun intOpt _ _ _ (_,[]) = raise Bug "intOpt"
  5329     | intOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit =
  5330       f (p (argToInt s omin omax h)) (s,t);
  5331 end;
  5332 
  5333 local
  5334   fun range NONE NONE = "R"
  5335     | range (SOME i) NONE = "{n IN R | " ^ Real.toString i ^ " <= n}"
  5336     | range NONE (SOME j) = "{n IN R | n <= " ^ Real.toString j ^ "}"
  5337     | range (SOME i) (SOME j) =
  5338     "{n IN R | " ^ Real.toString i ^ " <= n <= " ^ Real.toString j ^ "}";
  5339   fun oLeq (SOME (x:real)) (SOME y) = x <= y | oLeq _ _ = true;
  5340   fun argToReal arg omin omax x =
  5341     (case Real.fromString x of
  5342        SOME i =>
  5343        if oLeq omin (SOME i) andalso oLeq (SOME i) omax then i else
  5344          raise OptionExit
  5345            {success = false, usage = false, message =
  5346             SOME (arg ^ " option needs an real argument in the range "
  5347                   ^ range omin omax ^ " (not " ^ x ^ ")")}
  5348      | NONE =>
  5349        raise OptionExit
  5350          {success = false, usage = false, message =
  5351           SOME (arg ^ " option needs an real argument (not \"" ^ x ^ "\")")})
  5352 in
  5353   fun realOpt _ _ _ (_,[]) = raise Bug "realOpt"
  5354     | realOpt (omin,omax) f p (s:string, h :: (t : string list)) : unit =
  5355       f (p (argToReal s omin omax h)) (s,t);
  5356 end;
  5357 
  5358 fun enumOpt _ _ _ (_,[]) = raise Bug "enumOpt"
  5359   | enumOpt (choices : string list) f p (s : string, h :: t) : unit =
  5360     if mem h choices then f (p h) (s,t) else
  5361       raise OptionExit
  5362         {success = false, usage = false,
  5363          message = SOME ("follow parameter " ^ s ^ " with one of {" ^
  5364                          join "," choices ^ "}, not \"" ^ h ^ "\"")};
  5365 
  5366 fun optionOpt _ _ _ (_,[]) = raise Bug "optionOpt"
  5367   | optionOpt (x : string, p) f q (s : string, l as h :: t) : unit =
  5368     if h = x then f (q NONE) (s,t) else p f (q o SOME) (s,l);
  5369 
  5370 (* ------------------------------------------------------------------------- *)
  5371 (* Basic options useful for all programs                                     *)
  5372 (* ------------------------------------------------------------------------- *)
  5373 
  5374 val basicOptions : opt list =
  5375   [{switches = ["--"], arguments = [],
  5376     description = "no more options",
  5377     processor = fn _ => raise Fail "basicOptions: --"},
  5378    {switches = ["-?","-h","--help"], arguments = [],
  5379     description = "display all options and exit",
  5380     processor = fn _ => raise OptionExit
  5381     {message = SOME "displaying all options", usage = true, success = true}},
  5382    {switches = ["-v", "--version"], arguments = [],
  5383     description = "display version information",
  5384     processor = fn _ => raise Fail "basicOptions: -v, --version"}];
  5385 
  5386 (* ------------------------------------------------------------------------- *)
  5387 (* All the command line options of a program                                 *)
  5388 (* ------------------------------------------------------------------------- *)
  5389 
  5390 type allOptions = {name : string, version : string, header : string,
  5391                    footer : string, options : opt list};
  5392 
  5393 (* ------------------------------------------------------------------------- *)
  5394 (* Usage information                                                         *)
  5395 (* ------------------------------------------------------------------------- *)
  5396 
  5397 fun versionInformation ({version, ...} : allOptions) = version;
  5398 
  5399 fun usageInformation ({name,version,header,footer,options} : allOptions) =
  5400   let
  5401     fun listOpts {switches = n, arguments = r, description = s,
  5402                   processor = _} =
  5403         let
  5404           fun indent (s, "" :: l) = indent (s ^ "  ", l) | indent x = x
  5405           val (res,n) = indent ("  ",n)
  5406           val res = res ^ join ", " n
  5407           val res = foldl (fn (x,y) => y ^ " " ^ x) res r
  5408         in
  5409           [res ^ " ...", " " ^ s]
  5410         end
  5411 
  5412     val alignment =
  5413         [{leftAlign = true, padChar = #"."},
  5414          {leftAlign = true, padChar = #" "}]
  5415 
  5416     val table = alignTable alignment (map listOpts options)
  5417   in
  5418     header ^ join "\n" table ^ "\n" ^ footer
  5419   end;
  5420 
  5421 (* ------------------------------------------------------------------------- *)
  5422 (* Exit the program gracefully                                               *)
  5423 (* ------------------------------------------------------------------------- *)
  5424 
  5425 fun exit (allopts : allOptions) (optexit : optionExit) =
  5426   let
  5427     val {name, options, ...} = allopts
  5428     val {message, usage, success} = optexit
  5429     fun err s = TextIO.output (TextIO.stdErr, s)
  5430   in
  5431     case message of NONE => () | SOME m => err (name ^ ": " ^ m ^ "\n");
  5432     if usage then err (usageInformation allopts) else ();
  5433     OS.Process.exit (if success then OS.Process.success else OS.Process.failure)
  5434   end;
  5435 
  5436 fun succeed allopts =
  5437     exit allopts {message = NONE, usage = false, success = true};
  5438 
  5439 fun fail allopts mesg =
  5440     exit allopts {message = SOME mesg, usage = false, success = false};
  5441 
  5442 fun usage allopts mesg =
  5443     exit allopts {message = SOME mesg, usage = true, success = false};
  5444 
  5445 fun version allopts =
  5446     (print (versionInformation allopts);
  5447      exit allopts {message = NONE, usage = false, success = true});
  5448 
  5449 (* ------------------------------------------------------------------------- *)
  5450 (* Process the command line options passed to the program                    *)
  5451 (* ------------------------------------------------------------------------- *)
  5452 
  5453 fun processOptions (allopts : allOptions) =
  5454   let
  5455     fun findOption x =
  5456       case List.find (fn {switches = n, ...} => mem x n) (#options allopts) of
  5457         NONE => raise OptionExit
  5458                         {message = SOME ("unknown switch \"" ^ x ^ "\""),
  5459                          usage = true, success = false}
  5460       | SOME {arguments = r, processor = f, ...} => (r,f)
  5461 
  5462     fun getArgs x r xs =
  5463       let
  5464         fun f 1 = "a following argument"
  5465           | f m = Int.toString m ^ " following arguments"
  5466         val m = length r
  5467         val () =
  5468           if m <= length xs then () else
  5469             raise OptionExit
  5470               {usage = false, success = false, message = SOME
  5471                (x ^ " option needs " ^ f m ^ ": " ^ join " " r)}
  5472       in
  5473         divide xs m
  5474       end
  5475 
  5476     fun process [] = ([], [])
  5477       | process ("--" :: xs) = ([("--",[])], xs)
  5478       | process ("-v" :: _) = version allopts
  5479       | process ("--version" :: _) = version allopts
  5480       | process (x :: xs) =
  5481       if x = "" orelse x = "-" orelse hd (explode x) <> #"-" then ([], x :: xs)
  5482       else
  5483         let
  5484           val (r,f) = findOption x
  5485           val (ys,xs) = getArgs x r xs
  5486           val () = f (x,ys)
  5487         in
  5488           (cons (x,ys) ## I) (process xs)
  5489         end
  5490   in
  5491     fn l =>
  5492     let
  5493       val (a,b) = process l
  5494       val a = foldl (fn ((x,xs),ys) => x :: xs @ ys) [] (rev a)
  5495     in
  5496       (a,b)
  5497     end
  5498     handle OptionExit x => exit allopts x
  5499   end;
  5500 
  5501 end
  5502 end;
  5503 
  5504 (**** Original file: Name.sig ****)
  5505 
  5506 (* ========================================================================= *)
  5507 (* NAMES                                                                     *)
  5508 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  5509 (* ========================================================================= *)
  5510 
  5511 signature Name =
  5512 sig
  5513 
  5514 type name = string
  5515 
  5516 val compare : name * name -> order
  5517 
  5518 val pp : name Metis.Parser.pp
  5519 
  5520 end
  5521 
  5522 (**** Original file: Name.sml ****)
  5523 
  5524 structure Metis = struct open Metis
  5525 (* Metis-specific ML environment *)
  5526 nonfix ++ -- RL mem union subset;
  5527 val explode = String.explode;
  5528 val implode = String.implode;
  5529 val print = TextIO.print;
  5530 (* ========================================================================= *)
  5531 (* NAMES                                                                     *)
  5532 (* Copyright (c) 2004-2006 Joe Hurd, distributed under the BSD License *)
  5533 (* ========================================================================= *)
  5534 
  5535 structure Name :> Name =
  5536 struct
  5537 
  5538 type name = string;
  5539 
  5540 val compare = String.compare;
  5541 
  5542 val pp = Parser.ppString;
  5543 
  5544 end
  5545 
  5546 structure NameOrdered =
  5547 struct type t = Name.name val compare = Name.compare end
  5548 
  5549 structure NameSet =
  5550 struct
  5551 
  5552   local
  5553     structure S = ElementSet (NameOrdered);
  5554   in
  5555     open S;
  5556   end;
  5557 
  5558   val pp =
  5559       Parser.ppMap
  5560         toList
  5561         (Parser.ppBracket "{" "}" (Parser.ppSequence "," Name.pp));
  5562 
  5563 end
  5564 
  5565 structure NameMap = KeyMap (NameOrdered);
  5566 
  5567 structure NameArity =
  5568 struct
  5569 
  5570 type nameArity = Name.name * int;
  5571 
  5572 fun name ((n,_) : nameArity) = n;
  5573 
  5574 fun arity ((_,i) : nameArity) = i;
  5575 
  5576 fun nary i n_i = arity n_i = i;
  5577 
  5578 val nullary = nary 0
  5579 and unary = nary 1
  5580 and binary = nary 2
  5581 and ternary = nary 3;
  5582 
  5583 fun compare ((n1,i1),(n2,i2)) =
  5584     case Name.compare (n1,n2) of
  5585       LESS => LESS
  5586     | EQUAL => Int.compare (i1,i2)
  5587     | GREATER => GREATER;
  5588 
  5589 val pp = Parser.ppMap (fn (n,i) => n ^ "/" ^ Int.toString i) Parser.ppString;
  5590 
  5591 end
  5592 
  5593 structure NameArityOrdered =
  5594 struct type t = NameArity.nameArity val compare = NameArity.compare end
  5595 
  5596 structure NameAritySet =
  5597 struct
  5598 
  5599   local
  5600     structure S = ElementSet (NameArityOrdered);
  5601   in
  5602     open S;
  5603   end;
  5604 
  5605   val allNullary = all NameArity.nullary;
  5606 
  5607   val pp =
  5608       Parser.ppMap
  5609         toList
  5610         (Parser.ppBracket "{" "}" (Parser.ppSequence "," NameArity.pp));
  5611 
  5612 end
  5613 
  5614 structure NameArityMap = KeyMap (NameArityOrdered);
  5615 end;
  5616 
  5617 (**** Original file: Term.sig ****)
  5618 
  5619 (* ========================================================================= *)
  5620 (* FIRST ORDER LOGIC TERMS                                                   *)
  5621 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  5622 (* ========================================================================= *)
  5623 
  5624 signature Term =
  5625 sig
  5626 
  5627 (* ------------------------------------------------------------------------- *)
  5628 (* A type of first order logic terms.                                        *)
  5629 (* ------------------------------------------------------------------------- *)
  5630 
  5631 type var = Metis.Name.name
  5632 
  5633 type functionName = Metis.Name.name
  5634 
  5635 type function = functionName * int
  5636 
  5637 type const = functionName
  5638 
  5639 datatype term =
  5640     Var of var
  5641   | Fn of functionName * term list
  5642 
  5643 (* ------------------------------------------------------------------------- *)
  5644 (* Constructors and destructors.                                             *)
  5645 (* ------------------------------------------------------------------------- *)
  5646 
  5647 (* Variables *)
  5648 
  5649 val destVar : term -> var
  5650 
  5651 val isVar : term -> bool
  5652 
  5653 val equalVar : var -> term -> bool
  5654 
  5655 (* Functions *)
  5656 
  5657 val destFn : term -> functionName * term list
  5658 
  5659 val isFn : term -> bool
  5660 
  5661 val fnName : term -> functionName
  5662 
  5663 val fnArguments : term -> term list
  5664 
  5665 val fnArity : term -> int
  5666 
  5667 val fnFunction : term -> function
  5668 
  5669 val functions : term -> Metis.NameAritySet.set
  5670 
  5671 val functionNames : term -> Metis.NameSet.set
  5672 
  5673 (* Constants *)
  5674 
  5675 val mkConst : const -> term
  5676 
  5677 val destConst : term -> const
  5678 
  5679 val isConst : term -> bool
  5680 
  5681 (* Binary functions *)
  5682 
  5683 val mkBinop : functionName -> term * term -> term
  5684 
  5685 val destBinop : functionName -> term -> term * term
  5686 
  5687 val isBinop : functionName -> term -> bool
  5688 
  5689 (* ------------------------------------------------------------------------- *)
  5690 (* The size of a term in symbols.                                            *)
  5691 (* ------------------------------------------------------------------------- *)
  5692 
  5693 val symbols : term -> int
  5694 
  5695 (* ------------------------------------------------------------------------- *)
  5696 (* A total comparison function for terms.                                    *)
  5697 (* ------------------------------------------------------------------------- *)
  5698 
  5699 val compare : term * term -> order
  5700 
  5701 (* ------------------------------------------------------------------------- *)
  5702 (* Subterms.                                                                 *)
  5703 (* ------------------------------------------------------------------------- *)
  5704 
  5705 type path = int list
  5706 
  5707 val subterm : term -> path -> term
  5708 
  5709 val subterms : term -> (path * term) list
  5710 
  5711 val replace : term -> path * term -> term
  5712 
  5713 val find : (term -> bool) -> term -> path option
  5714 
  5715 val ppPath : path Metis.Parser.pp
  5716 
  5717 val pathToString : path -> string
  5718 
  5719 (* ------------------------------------------------------------------------- *)
  5720 (* Free variables.                                                           *)
  5721 (* ------------------------------------------------------------------------- *)
  5722 
  5723 val freeIn : var -> term -> bool
  5724 
  5725 val freeVars : term -> Metis.NameSet.set
  5726 
  5727 (* ------------------------------------------------------------------------- *)
  5728 (* Fresh variables.                                                          *)
  5729 (* ------------------------------------------------------------------------- *)
  5730 
  5731 val newVar : unit -> term
  5732 
  5733 val newVars : int -> term list
  5734 
  5735 val variantPrime : Metis.NameSet.set -> var -> var
  5736 
  5737 val variantNum : Metis.NameSet.set -> var -> var
  5738 
  5739 (* ------------------------------------------------------------------------- *)
  5740 (* Special support for terms with type annotations.                          *)
  5741 (* ------------------------------------------------------------------------- *)
  5742 
  5743 val isTypedVar : term -> bool
  5744 
  5745 val typedSymbols : term -> int
  5746 
  5747 val nonVarTypedSubterms : term -> (path * term) list
  5748 
  5749 (* ------------------------------------------------------------------------- *)
  5750 (* Special support for terms with an explicit function application operator. *)
  5751 (* ------------------------------------------------------------------------- *)
  5752 
  5753 val mkComb : term * term -> term
  5754 
  5755 val destComb : term -> term * term
  5756 
  5757 val isComb : term -> bool
  5758 
  5759 val listMkComb : term * term list -> term
  5760 
  5761 val stripComb : term -> term * term list
  5762 
  5763 (* ------------------------------------------------------------------------- *)
  5764 (* Parsing and pretty printing.                                              *)
  5765 (* ------------------------------------------------------------------------- *)
  5766 
  5767 (* Infix symbols *)
  5768 
  5769 val infixes : Metis.Parser.infixities Unsynchronized.ref
  5770 
  5771 (* The negation symbol *)
  5772 
  5773 val negation : Metis.Name.name Unsynchronized.ref
  5774 
  5775 (* Binder symbols *)
  5776 
  5777 val binders : Metis.Name.name list Unsynchronized.ref
  5778 
  5779 (* Bracket symbols *)
  5780 
  5781 val brackets : (Metis.Name.name * Metis.Name.name) list Unsynchronized.ref
  5782 
  5783 (* Pretty printing *)
  5784 
  5785 val pp : term Metis.Parser.pp
  5786 
  5787 val toString : term -> string
  5788 
  5789 (* Parsing *)
  5790 
  5791 val fromString : string -> term
  5792 
  5793 val parse : term Metis.Parser.quotation -> term
  5794 
  5795 end
  5796 
  5797 (**** Original file: Term.sml ****)
  5798 
  5799 structure Metis = struct open Metis
  5800 (* Metis-specific ML environment *)
  5801 nonfix ++ -- RL mem union subset;
  5802 val explode = String.explode;
  5803 val implode = String.implode;
  5804 val print = TextIO.print;
  5805 (* ========================================================================= *)
  5806 (* FIRST ORDER LOGIC TERMS                                                   *)
  5807 (* Copyright (c) 2001-2006 Joe Hurd, distributed under the BSD License *)
  5808 (* ========================================================================= *)
  5809 
  5810 structure Term :> Term =
  5811 struct
  5812 
  5813 open Useful;
  5814 
  5815 (* ------------------------------------------------------------------------- *)
  5816 (* Helper functions.                                                         *)
  5817 (* ------------------------------------------------------------------------- *)
  5818 
  5819 fun stripSuffix pred s =
  5820     let
  5821       fun f 0 = ""
  5822         | f n =
  5823           let
  5824             val n' = n - 1
  5825           in
  5826             if pred (String.sub (s,n')) then f n'
  5827             else String.substring (s,0,n)
  5828           end
  5829     in
  5830       f (size s)
  5831     end;
  5832 
  5833 (* ------------------------------------------------------------------------- *)
  5834 (* A type of first order logic terms.                                        *)
  5835 (* ------------------------------------------------------------------------- *)
  5836 
  5837 type var = Name.name;
  5838 
  5839 type functionName = Name.name;
  5840 
  5841 type function = functionName * int;
  5842 
  5843 type const = functionName;
  5844 
  5845 datatype term =
  5846     Var of Name.name
  5847   | Fn of Name.name * term list;
  5848 
  5849 (* ------------------------------------------------------------------------- *)
  5850 (* Constructors and destructors.                                             *)
  5851 (* ------------------------------------------------------------------------- *)
  5852 
  5853 (* Variables *)
  5854 
  5855 fun destVar (Var v) = v
  5856   | destVar (Fn _) = raise Error "destVar";
  5857 
  5858 val isVar = can destVar;
  5859 
  5860 fun equalVar v (Var v') = v = v'
  5861   | equalVar _ _ = false;
  5862 
  5863 (* Functions *)
  5864 
  5865 fun destFn (Fn f) = f
  5866   | destFn (Var _) = raise Error "destFn";
  5867 
  5868 val isFn = can destFn;
  5869 
  5870 fun fnName tm = fst (destFn tm);
  5871 
  5872 fun fnArguments tm = snd (destFn tm);
  5873 
  5874 fun fnArity tm = length (fnArguments tm);
  5875 
  5876 fun fnFunction tm = (fnName tm, fnArity tm);
  5877 
  5878 local
  5879   fun func fs [] = fs
  5880     | func fs (Var _ :: tms) = func fs tms
  5881     | func fs (Fn (n,l) :: tms) =
  5882       func (NameAritySet.add fs (n, length l)) (l @ tms);
  5883 in
  5884   fun functions tm = func NameAritySet.empty [tm];
  5885 end;
  5886 
  5887 local
  5888   fun func fs [] = fs
  5889     | func fs (Var _ :: tms) = func fs tms
  5890     | func fs (Fn (n,l) :: tms) = func (NameSet.add fs n) (l @ tms);
  5891 in
  5892   fun functionNames tm = func NameSet.empty [tm];
  5893 end;
  5894 
  5895 (* Constants *)
  5896 
  5897 fun mkConst c = (Fn (c, []));
  5898 
  5899 fun destConst (Fn (c, [])) = c
  5900   | destConst _ = raise Error "destConst";
  5901 
  5902 val isConst = can destConst;
  5903 
  5904 (* Binary functions *)
  5905 
  5906 fun mkBinop f (a,b) = Fn (f,[a,b]);
  5907 
  5908 fun destBinop f (Fn (x,[a,b])) =
  5909     if x = f then (a,b) else raise Error "Term.destBinop: wrong binop"
  5910   | destBinop _ _ = raise Error "Term.destBinop: not a binop";
  5911 
  5912 fun isBinop f = can (destBinop f);
  5913 
  5914 (* ------------------------------------------------------------------------- *)
  5915 (* The size of a term in symbols.                                            *)
  5916 (* ------------------------------------------------------------------------- *)
  5917 
  5918 val VAR_SYMBOLS = 1;
  5919 
  5920 val FN_SYMBOLS = 1;
  5921 
  5922 local
  5923   fun sz n [] = n
  5924     | sz n (Var _ :: tms) = sz (n + VAR_SYMBOLS) tms
  5925     | sz n (Fn (func,args) :: tms) = sz (n + FN_SYMBOLS) (args @ tms);
  5926 in
  5927   fun symbols tm = sz 0 [tm];
  5928 end;
  5929 
  5930 (* ------------------------------------------------------------------------- *)
  5931 (* A total comparison function for terms.                                    *)
  5932 (* ------------------------------------------------------------------------- *)
  5933 
  5934 local
  5935   fun cmp [] [] = EQUAL
  5936     | cmp (Var _ :: _) (Fn _ :: _) = LESS
  5937     | cmp (Fn _ :: _) (Var _ :: _) = GREATER
  5938     | cmp (Var v1 :: tms1) (Var v2 :: tms2) =
  5939       (case Name.compare (v1,v2) of
  5940          LESS => LESS
  5941        | EQUAL => cmp tms1 tms2
  5942        | GREATER => GREATER)
  5943     | cmp (Fn (f1,a1) :: tms1) (Fn (f2,a2) :: tms2) =
  5944       (case Name.compare (f1,f2) of
  5945          LESS => LESS
  5946        | EQUAL =>
  5947          (case Int.compare (length a1, length a2) of
  5948             LESS => LESS
  5949           | EQUAL => cmp (a1 @ tms1) (a2 @ tms2)
  5950           | GREATER => GREATER)
  5951        | GREATER => GREATER)
  5952     | cmp _ _ = raise Bug "Term.compare";
  5953 in
  5954   fun compare (tm1,tm2) = cmp [tm1] [tm2];
  5955 end;
  5956 
  5957 (* ------------------------------------------------------------------------- *)
  5958 (* Subterms.                                                                 *)
  5959 (* ------------------------------------------------------------------------- *)
  5960 
  5961 type path = int list;
  5962 
  5963 fun subterm tm [] = tm
  5964   | subterm (Var _) (_ :: _) = raise Error "Term.subterm: Var"
  5965   | subterm (Fn (_,tms)) (h :: t) =
  5966     if h >= length tms then raise Error "Term.replace: Fn"
  5967     else subterm (List.nth (tms,h)) t;
  5968 
  5969 local
  5970   fun subtms [] acc = acc
  5971     | subtms ((path,tm) :: rest) acc =
  5972       let
  5973         fun f (n,arg) = (n :: path, arg)
  5974 
  5975         val acc = (rev path, tm) :: acc
  5976       in
  5977         case tm of
  5978           Var _ => subtms rest acc
  5979         | Fn (_,args) => subtms (map f (enumerate args) @ rest) acc
  5980       end;
  5981 in
  5982   fun subterms tm = subtms [([],tm)] [];
  5983 end;
  5984 
  5985 fun replace tm ([],res) = if res = tm then tm else res
  5986   | replace tm (h :: t, res) =
  5987     case tm of
  5988       Var _ => raise Error "Term.replace: Var"
  5989     | Fn (func,tms) =>
  5990       if h >= length tms then raise Error "Term.replace: Fn"
  5991       else
  5992         let
  5993           val arg = List.nth (tms,h)
  5994           val arg' = replace arg (t,res)
  5995         in
  5996           if Sharing.pointerEqual (arg',arg) then tm
  5997           else Fn (func, updateNth (h,arg') tms)
  5998         end;
  5999 
  6000 fun find pred =
  6001     let
  6002       fun search [] = NONE
  6003         | search ((path,tm) :: rest) =
  6004           if pred tm then SOME (rev path)
  6005           else
  6006             case tm of
  6007               Var _ => search rest
  6008             | Fn (_,a) =>
  6009               let
  6010                 val subtms = map (fn (i,t) => (i :: path, t)) (enumerate a)
  6011               in
  6012                 search (subtms @ rest)
  6013               end
  6014     in
  6015       fn tm => search [([],tm)]
  6016     end;
  6017 
  6018 val ppPath = Parser.ppList Parser.ppInt;
  6019 
  6020 val pathToString = Parser.toString ppPath;
  6021 
  6022 (* ------------------------------------------------------------------------- *)
  6023 (* Free variables.                                                           *)
  6024 (* ------------------------------------------------------------------------- *)
  6025 
  6026 local
  6027   fun free _ [] = false
  6028     | free v (Var w :: tms) = v = w orelse free v tms
  6029     | free v (Fn (_,args) :: tms) = free v (args @ tms);
  6030 in
  6031   fun freeIn v tm = free v [tm];
  6032 end;
  6033 
  6034 local
  6035   fun free vs [] = vs
  6036     | free vs (Var v :: tms) = free (NameSet.add vs v) tms
  6037     | free vs (Fn (_,args) :: tms) = free vs (args @ tms);
  6038 in
  6039   fun freeVars tm = free NameSet.empty [tm];
  6040 end;
  6041 
  6042 (* ------------------------------------------------------------------------- *)
  6043 (* Fresh variables.                                                          *)
  6044 (* ------------------------------------------------------------------------- *)
  6045 
  6046 local
  6047   val prefix  = "_";
  6048 
  6049   fun numVar i = Var (mkPrefix prefix (Int.toString i));
  6050 in
  6051   fun newVar () = numVar (newInt ());
  6052 
  6053   fun newVars n = map numVar (newInts n);
  6054 end;
  6055 
  6056 fun variantPrime avoid =
  6057     let
  6058       fun f v = if NameSet.member v avoid then f (v ^ "'") else v
  6059     in
  6060       f
  6061     end;
  6062 
  6063 fun variantNum avoid v =
  6064     if not (NameSet.member v avoid) then v
  6065     else
  6066       let
  6067         val v = stripSuffix Char.isDigit v
  6068                                                                     
  6069         fun f n =
  6070             let
  6071               val v_n = v ^ Int.toString n
  6072             in
  6073               if NameSet.member v_n avoid then f (n + 1) else v_n
  6074             end
  6075       in
  6076         f 0
  6077       end;
  6078 
  6079 (* ------------------------------------------------------------------------- *)
  6080 (* Special support for terms with type annotations.                          *)
  6081 (* ------------------------------------------------------------------------- *)
  6082 
  6083 fun isTypedVar (Var _) = true
  6084   | isTypedVar (Fn (":", [Var _, _])) = true
  6085   | isTypedVar (Fn _) = false;
  6086 
  6087 local
  6088   fun sz n [] = n
  6089     | sz n (Var _ :: tms) = sz (n + 1) tms
  6090     | sz n (Fn (":",[tm,_]) :: tms) = sz n (tm :: tms)
  6091     | sz n (Fn (_,args) :: tms) = sz (n + 1) (args @ tms);
  6092 in
  6093   fun typedSymbols tm = sz 0 [tm];
  6094 end;
  6095 
  6096 local
  6097   fun subtms [] acc = acc
  6098     | subtms ((_, Var _) :: rest) acc = subtms rest acc
  6099     | subtms ((_, Fn (":", [Var _, _])) :: rest) acc = subtms rest acc
  6100     | subtms ((path, tm as Fn func) :: rest) acc =
  6101       let
  6102         fun f (n,arg) = (n :: path, arg)
  6103 
  6104         val acc = (rev path, tm) :: acc
  6105       in
  6106         case func of
  6107           (":",[arg,_]) => subtms ((0 :: path, arg) :: rest) acc
  6108         | (_,args) => subtms (map f (enumerate args) @ rest) acc
  6109       end;
  6110 in
  6111   fun nonVarTypedSubterms tm = subtms [([],tm)] [];
  6112 end;
  6113 
  6114 (* ------------------------------------------------------------------------- *)
  6115 (* Special support for terms with an explicit function application operator. *)
  6116 (* ------------------------------------------------------------------------- *)
  6117 
  6118 fun mkComb (f,a) = Fn (".",[f,a]);
  6119 
  6120 fun destComb (Fn (".",[f,a])) = (f,a)
  6121   | destComb _ = raise Error "destComb";
  6122 
  6123 val isComb = can destComb;
  6124 
  6125 fun listMkComb (f,l) = foldl mkComb f l;
  6126 
  6127 local
  6128   fun strip tms (Fn (".",[f,a])) = strip (a :: tms) f
  6129     | strip tms tm = (tm,tms);
  6130 in
  6131   fun stripComb tm = strip [] tm;
  6132 end;
  6133 
  6134 (* ------------------------------------------------------------------------- *)
  6135 (* Parsing and pretty printing.                                              *)
  6136 (* ------------------------------------------------------------------------- *)
  6137 
  6138 (* Operators parsed and printed infix *)
  6139 
  6140 val infixes : Parser.infixities Unsynchronized.ref = Unsynchronized.ref
  6141   [(* ML symbols *)
  6142    {token = " / ", precedence = 7, leftAssoc = true},
  6143    {token = " div ", precedence = 7, leftAssoc = true},
  6144    {token = " mod ", precedence = 7, leftAssoc = true},
  6145    {token = " * ", precedence = 7, leftAssoc = true},
  6146    {token = " + ", precedence = 6, leftAssoc = true},
  6147    {token = " - ", precedence = 6, leftAssoc = true},
  6148    {token = " ^ ", precedence = 6, leftAssoc = true},
  6149    {token = " @ ", precedence = 5, leftAssoc = false},
  6150    {token = " :: ", precedence = 5, leftAssoc = false},
  6151    {token = " = ", precedence = 4, leftAssoc = true},
  6152    {token = " <> ", precedence = 4, leftAssoc = true},
  6153    {token = " <= ", precedence = 4, leftAssoc = true},
  6154    {token = " < ", precedence = 4, leftAssoc = true},
  6155    {token = " >= ", precedence = 4, leftAssoc = true},
  6156    {token = " > ", precedence = 4, leftAssoc = true},
  6157    {token = " o ", precedence = 3, leftAssoc = true},
  6158    {token = " -> ", precedence = 2, leftAssoc = false},  (* inferred prec *)
  6159    {token = " : ", precedence = 1, leftAssoc = false},  (* inferred prec *)
  6160    {token = ", ", precedence = 0, leftAssoc = false},  (* inferred prec *)
  6161 
  6162    (* Logical connectives *)
  6163    {token = " /\\ ", precedence = ~1, leftAssoc = false},
  6164    {token = " \\/ ", precedence = ~2, leftAssoc = false},
  6165    {token = " ==> ", precedence = ~3, leftAssoc = false},
  6166    {token = " <=> ", precedence = ~4, leftAssoc = false},
  6167 
  6168    (* Other symbols *)
  6169    {token = " . ", precedence = 9, leftAssoc = true},  (* function app *)
  6170    {token = " ** ", precedence = 8, leftAssoc = true},
  6171    {token = " ++ ", precedence = 6, leftAssoc = true},
  6172    {token = " -- ", precedence = 6, leftAssoc = true},
  6173    {token = " == ", precedence = 4, leftAssoc = true}];
  6174 
  6175 (* The negation symbol *)
  6176 
  6177 val negation : Name.name Unsynchronized.ref = Unsynchronized.ref "~";
  6178 
  6179 (* Binder symbols *)
  6180 
  6181 val binders : Name.name list Unsynchronized.ref = Unsynchronized.ref ["\\","!","?","?!"];
  6182 
  6183 (* Bracket symbols *)
  6184 
  6185 val brackets : (Name.name * Name.name) list Unsynchronized.ref = Unsynchronized.ref [("[","]"),("{","}")];
  6186 
  6187 (* Pretty printing *)
  6188 
  6189 local
  6190   open Parser;
  6191 in
  6192   fun pp inputPpstrm inputTerm =
  6193       let
  6194         val quants = !binders
  6195         and iOps = !infixes
  6196         and neg = !negation
  6197         and bracks = !brackets
  6198 
  6199         val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
  6200 
  6201         val bTokens = map #2 bracks @ map #3 bracks
  6202 
  6203         val iTokens = infixTokens iOps
  6204 
  6205         fun destI (Fn (f,[a,b])) =
  6206             if mem f iTokens then SOME (f,a,b) else NONE
  6207           | destI _ = NONE
  6208 
  6209         val iPrinter = ppInfixes iOps destI
  6210 
  6211         val specialTokens = neg :: quants @ ["$","(",")"] @ bTokens @ iTokens
  6212 
  6213         fun vName bv s = NameSet.member s bv
  6214 
  6215         fun checkVarName bv s = if vName bv s then s else "$" ^ s
  6216 
  6217         fun varName bv = ppMap (checkVarName bv) ppString
  6218 
  6219         fun checkFunctionName bv s =
  6220             if mem s specialTokens orelse vName bv s then "(" ^ s ^ ")" else s
  6221 
  6222         fun functionName bv = ppMap (checkFunctionName bv) ppString
  6223 
  6224         fun isI tm = Option.isSome (destI tm)
  6225 
  6226         fun stripNeg (tm as Fn (f,[a])) =
  6227             if f <> neg then (0,tm)
  6228             else let val (n,tm) = stripNeg a in (n + 1, tm) end
  6229           | stripNeg tm = (0,tm)
  6230 
  6231         val destQuant =
  6232             let
  6233               fun dest q (Fn (q', [Var v, body])) =
  6234                   if q <> q' then NONE
  6235                   else
  6236                     (case dest q body of
  6237                        NONE => SOME (q,v,[],body)
  6238                      | SOME (_,v',vs,body) => SOME (q, v, v' :: vs, body))
  6239                 | dest _ _ = NONE
  6240             in
  6241               fn tm => Useful.first (fn q => dest q tm) quants
  6242             end
  6243 
  6244         fun isQuant tm = Option.isSome (destQuant tm)
  6245 
  6246         fun destBrack (Fn (b,[tm])) =
  6247             (case List.find (fn (n,_,_) => n = b) bracks of
  6248                NONE => NONE
  6249              | SOME (_,b1,b2) => SOME (b1,tm,b2))
  6250           | destBrack _ = NONE
  6251 
  6252         fun isBrack tm = Option.isSome (destBrack tm)
  6253             
  6254         fun functionArgument bv ppstrm tm =
  6255             (addBreak ppstrm (1,0);
  6256              if isBrack tm then customBracket bv ppstrm tm
  6257              else if isVar tm orelse isConst tm then basic bv ppstrm tm
  6258              else bracket bv ppstrm tm)
  6259 
  6260         and basic bv ppstrm (Var v) = varName bv ppstrm v
  6261           | basic bv ppstrm (Fn (f,args)) =
  6262             (beginBlock ppstrm Inconsistent 2;
  6263              functionName bv ppstrm f;
  6264              app (functionArgument bv ppstrm) args;
  6265              endBlock ppstrm)
  6266 
  6267         and customBracket bv ppstrm tm =
  6268             case destBrack tm of
  6269               SOME (b1,tm,b2) => ppBracket b1 b2 (term bv) ppstrm tm
  6270             | NONE => basic bv ppstrm tm
  6271 
  6272         and innerQuant bv ppstrm tm =
  6273             case destQuant tm of
  6274               NONE => term bv ppstrm tm
  6275             | SOME (q,v,vs,tm) =>
  6276               let
  6277                 val bv = NameSet.addList (NameSet.add bv v) vs
  6278               in
  6279                 addString ppstrm q;
  6280                 varName bv ppstrm v;
  6281                 app (fn v => (addBreak ppstrm (1,0); varName bv ppstrm v)) vs;
  6282                 addString ppstrm ".";
  6283                 addBreak ppstrm (1,0);
  6284                 innerQuant bv ppstrm tm
  6285               end
  6286 
  6287         and quantifier bv ppstrm tm =
  6288             if not (isQuant tm) then customBracket bv ppstrm tm
  6289             else
  6290               (beginBlock ppstrm Inconsistent 2;
  6291                innerQuant bv ppstrm tm;
  6292                endBlock ppstrm)
  6293 
  6294         and molecule bv ppstrm (tm,r) =
  6295             let
  6296               val (n,tm) = stripNeg tm
  6297             in
  6298               beginBlock ppstrm Inconsistent n;
  6299               funpow n (fn () => addString ppstrm neg) ();
  6300               if isI tm orelse (r andalso isQuant tm) then bracket bv ppstrm tm
  6301               else quantifier bv ppstrm tm;
  6302               endBlock ppstrm
  6303             end
  6304 
  6305         and term bv ppstrm tm = iPrinter (molecule bv) ppstrm (tm,false)
  6306 
  6307         and bracket bv ppstrm tm = ppBracket "(" ")" (term bv) ppstrm tm
  6308   in
  6309     term NameSet.empty
  6310   end inputPpstrm inputTerm;
  6311 end;
  6312 
  6313 fun toString tm = Parser.toString pp tm;
  6314 
  6315 (* Parsing *)
  6316 
  6317 local
  6318   open Parser;
  6319 
  6320   infixr 9 >>++
  6321   infixr 8 ++
  6322   infixr 7 >>
  6323   infixr 6 ||
  6324 
  6325   val isAlphaNum =
  6326       let
  6327         val alphaNumChars = explode "_'"
  6328       in
  6329         fn c => mem c alphaNumChars orelse Char.isAlphaNum c
  6330       end;
  6331 
  6332   local
  6333     val alphaNumToken = atLeastOne (some isAlphaNum) >> implode;
  6334 
  6335     val symbolToken =
  6336         let
  6337           fun isNeg c = str c = !negation
  6338                         
  6339           val symbolChars = explode "<>=-*+/\\?@|!$%&#^:;~"
  6340 
  6341           fun isSymbol c = mem c symbolChars
  6342 
  6343           fun isNonNegSymbol c = not (isNeg c) andalso isSymbol c
  6344         in
  6345           some isNeg >> str ||
  6346           (some isNonNegSymbol ++ many (some isSymbol)) >> (implode o op::)
  6347         end;
  6348 
  6349     val punctToken =
  6350         let
  6351           val punctChars = explode "()[]{}.,"
  6352 
  6353           fun isPunct c = mem c punctChars
  6354         in
  6355           some isPunct >> str
  6356         end;
  6357 
  6358     val lexToken = alphaNumToken || symbolToken || punctToken;
  6359 
  6360     val space = many (some Char.isSpace);
  6361   in
  6362     val lexer = (space ++ lexToken ++ space) >> (fn (_,(tok,_)) => tok);
  6363   end;
  6364 
  6365   fun termParser inputStream =
  6366       let
  6367         val quants = !binders
  6368         and iOps = !infixes
  6369         and neg = !negation
  6370         and bracks = ("(",")") :: !brackets
  6371 
  6372         val bracks = map (fn (b1,b2) => (b1 ^ b2, b1, b2)) bracks
  6373 
  6374         val bTokens = map #2 bracks @ map #3 bracks
  6375 
  6376         fun possibleVarName "" = false
  6377           | possibleVarName s = isAlphaNum (String.sub (s,0))
  6378 
  6379         fun vName bv s = NameSet.member s bv
  6380 
  6381         val iTokens = infixTokens iOps
  6382 
  6383         val iParser = parseInfixes iOps (fn (f,a,b) => Fn (f,[a,b]))
  6384 
  6385         val specialTokens = neg :: quants @ ["$"] @ bTokens @ iTokens
  6386 
  6387         fun varName bv =
  6388             Parser.some (vName bv) ||
  6389             (exact "$" ++ some possibleVarName) >> (fn (_,s) => s)
  6390 
  6391         fun fName bv s = not (mem s specialTokens) andalso not (vName bv s)
  6392 
  6393         fun functionName bv =
  6394             Parser.some (fName bv) ||
  6395             (exact "(" ++ any ++ exact ")") >> (fn (_,(s,_)) => s)
  6396 
  6397         fun basic bv tokens =
  6398             let
  6399               val var = varName bv >> Var
  6400 
  6401               val const = functionName bv >> (fn f => Fn (f,[]))
  6402 
  6403               fun bracket (ab,a,b) =
  6404                   (exact a ++ term bv ++ exact b) >>
  6405                   (fn (_,(tm,_)) => if ab = "()" then tm else Fn (ab,[tm]))
  6406 
  6407               fun quantifier q =
  6408                   let
  6409                     fun bind (v,t) = Fn (q, [Var v, t])
  6410                   in
  6411                     (exact q ++ atLeastOne (some possibleVarName) ++
  6412                      exact ".") >>++
  6413                     (fn (_,(vs,_)) =>
  6414                         term (NameSet.addList bv vs) >>
  6415                         (fn body => foldr bind body vs))
  6416                   end
  6417             in
  6418               var ||
  6419               const ||
  6420               first (map bracket bracks) ||
  6421               first (map quantifier quants)
  6422             end tokens
  6423 
  6424         and molecule bv tokens =
  6425             let
  6426               val negations = many (exact neg) >> length
  6427 
  6428               val function =
  6429                   (functionName bv ++ many (basic bv)) >> Fn || basic bv
  6430             in
  6431               (negations ++ function) >>
  6432               (fn (n,tm) => funpow n (fn t => Fn (neg,[t])) tm)
  6433             end tokens
  6434 
  6435         and term bv tokens = iParser (molecule bv) tokens
  6436       in
  6437         term NameSet.empty
  6438       end inputStream;
  6439 in
  6440   fun fromString input =
  6441       let
  6442         val chars = Stream.fromList (explode input)
  6443 
  6444         val tokens = everything (lexer >> singleton) chars
  6445 
  6446         val terms = everything (termParser >> singleton) tokens
  6447       in
  6448         case Stream.toList terms of
  6449           [tm] => tm
  6450         | _ => raise Error "Syntax.stringToTerm"
  6451       end;
  6452 end;
  6453 
  6454 local
  6455   val antiquotedTermToString =
  6456       Parser.toString (Parser.ppBracket "(" ")" pp);
  6457 in
  6458   val parse = Parser.parseQuotation antiquotedTermToString fromString;
  6459 end;
  6460 
  6461 end
  6462 
  6463 structure TermOrdered =
  6464 struct type t = Term.term val compare = Term.compare end
  6465 
  6466 structure TermSet = ElementSet (TermOrdered);
  6467 
  6468 structure TermMap = KeyMap (TermOrdered);
  6469 end;
  6470 
  6471 (**** Original file: Subst.sig ****)
  6472 
  6473 (* ========================================================================= *)
  6474 (* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
  6475 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
  6476 (* ========================================================================= *)
  6477 
  6478 signature Subst =
  6479 sig
  6480 
  6481 (* ------------------------------------------------------------------------- *)
  6482 (* A type of first order logic substitutions.                                *)
  6483 (* ------------------------------------------------------------------------- *)
  6484 
  6485 type subst
  6486 
  6487 (* ------------------------------------------------------------------------- *)
  6488 (* Basic operations.                                                         *)
  6489 (* ------------------------------------------------------------------------- *)
  6490 
  6491 val empty : subst
  6492 
  6493 val null : subst -> bool
  6494 
  6495 val size : subst -> int
  6496 
  6497 val peek : subst -> Metis.Term.var -> Metis.Term.term option
  6498 
  6499 val insert : subst -> Metis.Term.var * Metis.Term.term -> subst
  6500 
  6501 val singleton : Metis.Term.var * Metis.Term.term -> subst
  6502 
  6503 val union : subst -> subst -> subst
  6504 
  6505 val toList : subst -> (Metis.Term.var * Metis.Term.term) list
  6506 
  6507 val fromList : (Metis.Term.var * Metis.Term.term) list -> subst
  6508 
  6509 val foldl : (Metis.Term.var * Metis.Term.term * 'a -> 'a) -> 'a -> subst -> 'a
  6510 
  6511 val foldr : (Metis.Term.var * Metis.Term.term * 'a -> 'a) -> 'a -> subst -> 'a
  6512 
  6513 val pp : subst Metis.Parser.pp
  6514 
  6515 val toString : subst -> string
  6516 
  6517 (* ------------------------------------------------------------------------- *)
  6518 (* Normalizing removes identity substitutions.                               *)
  6519 (* ------------------------------------------------------------------------- *)
  6520 
  6521 val normalize : subst -> subst
  6522 
  6523 (* ------------------------------------------------------------------------- *)
  6524 (* Applying a substitution to a first order logic term.                      *)
  6525 (* ------------------------------------------------------------------------- *)
  6526 
  6527 val subst : subst -> Metis.Term.term -> Metis.Term.term
  6528 
  6529 (* ------------------------------------------------------------------------- *)
  6530 (* Restricting a substitution to a smaller set of variables.                 *)
  6531 (* ------------------------------------------------------------------------- *)
  6532 
  6533 val restrict : subst -> Metis.NameSet.set -> subst
  6534 
  6535 val remove : subst -> Metis.NameSet.set -> subst
  6536 
  6537 (* ------------------------------------------------------------------------- *)
  6538 (* Composing two substitutions so that the following identity holds:         *)
  6539 (*                                                                           *)
  6540 (* subst (compose sub1 sub2) tm = subst sub2 (subst sub1 tm)                 *)
  6541 (* ------------------------------------------------------------------------- *)
  6542 
  6543 val compose : subst -> subst -> subst
  6544 
  6545 (* ------------------------------------------------------------------------- *)
  6546 (* Substitutions can be inverted iff they are renaming substitutions.        *) 
  6547 (* ------------------------------------------------------------------------- *)
  6548 
  6549 val invert : subst -> subst  (* raises Error *)
  6550 
  6551 val isRenaming : subst -> bool
  6552 
  6553 (* ------------------------------------------------------------------------- *)
  6554 (* Creating a substitution to freshen variables.                             *)
  6555 (* ------------------------------------------------------------------------- *)
  6556 
  6557 val freshVars : Metis.NameSet.set -> subst
  6558 
  6559 (* ------------------------------------------------------------------------- *)
  6560 (* Matching for first order logic terms.                                     *)
  6561 (* ------------------------------------------------------------------------- *)
  6562 
  6563 val match : subst -> Metis.Term.term -> Metis.Term.term -> subst  (* raises Error *)
  6564 
  6565 (* ------------------------------------------------------------------------- *)
  6566 (* Unification for first order logic terms.                                  *)
  6567 (* ------------------------------------------------------------------------- *)
  6568 
  6569 val unify : subst -> Metis.Term.term -> Metis.Term.term -> subst  (* raises Error *)
  6570 
  6571 end
  6572 
  6573 (**** Original file: Subst.sml ****)
  6574 
  6575 structure Metis = struct open Metis
  6576 (* Metis-specific ML environment *)
  6577 nonfix ++ -- RL mem union subset;
  6578 val explode = String.explode;
  6579 val implode = String.implode;
  6580 val print = TextIO.print;
  6581 (* ========================================================================= *)
  6582 (* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
  6583 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
  6584 (* ========================================================================= *)
  6585 
  6586 structure Subst :> Subst =
  6587 struct
  6588 
  6589 open Useful;
  6590 
  6591 (* ------------------------------------------------------------------------- *)
  6592 (* A type of first order logic substitutions.                                *)
  6593 (* ------------------------------------------------------------------------- *)
  6594 
  6595 datatype subst = Subst of Term.term NameMap.map;
  6596 
  6597 (* ------------------------------------------------------------------------- *)
  6598 (* Basic operations.                                                         *)
  6599 (* ------------------------------------------------------------------------- *)
  6600 
  6601 val empty = Subst (NameMap.new ());
  6602 
  6603 fun null (Subst m) = NameMap.null m;
  6604 
  6605 fun size (Subst m) = NameMap.size m;
  6606 
  6607 fun peek (Subst m) v = NameMap.peek m v;
  6608 
  6609 fun insert (Subst m) v_tm = Subst (NameMap.insert m v_tm);
  6610 
  6611 fun singleton v_tm = insert empty v_tm;
  6612 
  6613 local
  6614   fun compatible (tm1,tm2) =
  6615       if tm1 = tm2 then SOME tm1 else raise Error "Subst.union: incompatible";
  6616 in
  6617   fun union (s1 as Subst m1) (s2 as Subst m2) =
  6618       if NameMap.null m1 then s2
  6619       else if NameMap.null m2 then s1
  6620       else Subst (NameMap.union compatible m1 m2);
  6621 end;
  6622 
  6623 fun toList (Subst m) = NameMap.toList m;
  6624 
  6625 fun fromList l = Subst (NameMap.fromList l);
  6626 
  6627 fun foldl f b (Subst m) = NameMap.foldl f b m;
  6628 
  6629 fun foldr f b (Subst m) = NameMap.foldr f b m;
  6630 
  6631 fun pp ppstrm sub =
  6632     Parser.ppBracket "<[" "]>"
  6633       (Parser.ppSequence "," (Parser.ppBinop " |->" Parser.ppString Term.pp))
  6634       ppstrm (toList sub);
  6635 
  6636 val toString = Parser.toString pp;
  6637 
  6638 (* ------------------------------------------------------------------------- *)
  6639 (* Normalizing removes identity substitutions.                               *)
  6640 (* ------------------------------------------------------------------------- *)
  6641 
  6642 local
  6643   fun isNotId (v,tm) = not (Term.equalVar v tm);
  6644 in
  6645   fun normalize (sub as Subst m) =
  6646       let
  6647         val m' = NameMap.filter isNotId m
  6648       in
  6649         if NameMap.size m = NameMap.size m' then sub else Subst m'
  6650       end;
  6651 end;
  6652 
  6653 (* ------------------------------------------------------------------------- *)
  6654 (* Applying a substitution to a first order logic term.                      *)
  6655 (* ------------------------------------------------------------------------- *)
  6656 
  6657 fun subst sub =
  6658     let
  6659       fun tmSub (tm as Term.Var v) =
  6660           (case peek sub v of
  6661              SOME tm' => if Sharing.pointerEqual (tm,tm') then tm else tm'
  6662            | NONE => tm)
  6663         | tmSub (tm as Term.Fn (f,args)) =
  6664           let
  6665             val args' = Sharing.map tmSub args
  6666           in
  6667             if Sharing.pointerEqual (args,args') then tm
  6668             else Term.Fn (f,args')
  6669           end
  6670     in
  6671       fn tm => if null sub then tm else tmSub tm
  6672     end;
  6673 
  6674 (* ------------------------------------------------------------------------- *)
  6675 (* Restricting a substitution to a given set of variables.                   *)
  6676 (* ------------------------------------------------------------------------- *)
  6677 
  6678 fun restrict (sub as Subst m) varSet =
  6679     let
  6680       fun isRestrictedVar (v,_) = NameSet.member v varSet
  6681 
  6682       val m' = NameMap.filter isRestrictedVar m
  6683     in