Add more utility functions to Portable

fold{l,r}2' are the obvious "primed" variants of ListPair.fold{l,r},
where priming means that the function takes its arguments curried, and
the accumulator is the last argument, as with foldl' and foldr'.

the_list and the_default handle option values and convert them to
something else: the_list to an empty or singleton list, and
the_default to the some value, or to the given default.

Promote list-singleton related functions from Isabelle to Portable

single: 'a -> 'a list
the_single : 'a list -> 'a
singleton: ('a list -> 'b list) -> 'a -> 'b

Promote Isabelle's Exn.reraise to Portable

This function keeps Poly/ML's location information from the original
exception intact (otherwise, the location information given to it is
that of the new raise). Under Moscow ML, there is no location
information so reraise is just equal to raise.

Promote more Isabelle concurrency code

Portable gets slightly richer with

make_counter : {inc:int,init:int} -> unit -> int
syncref : 'a -> {get:unit->'a, upd : ('a -> 'b * 'a) -> 'b}

Under Moscow ML these map to obvious operations on references. Under
Poly/ML these map to synchronised variables that are operated on
atomically.

Promote more functions from Isabelle Library into Portable

- enclose l r mid is "just" an application of string concatenation,
but is useful when partially applied to two arguments
- filter_out is filter with the sense of the predicate flipped
- ? provides a compact way of writing "if b then f x else x"

Finally, move fold_product from Library to Graph, where it is used.
This library function is effectively a fold over a cross product of
two lists + an accumulator. It's nice not to have to compute the
cross product explicitly, but it's a bit too exotic for me. I grepped
for uses of it in the Isabelle sources, and even there it's used only
6 times.

Lift Table functor out of fromIsabelle into src/portableML

This code is Isabelle's workhorse version of our Binarymap. It has a
better API for working with maps into lists of values, and is also
better in that its use of a functor means that the types of
maps/dictionaries/tables using different comparison functions are
different.

I have altered it to use HOL style comparison functions that are
curried rather than tupled. (I.e., in Isabelle the equivalents of our
various op_<operation> functions are take a comparison function that
takes a pair of arguments; our tradition is to use a curried
function.)

I have also added pretty-printing, requiring KEY-structures to provide
a pp function. (These functions ignore depth arguments for the
moment.)

Finally, there are a number of knock-on effects in the fromIsabelle
directory.

Add wall clock ("real time") analogue of time function

Add aliases for {rev_,}itlist that better indicate "direction"

In particular, itlist is a right fold, and rev_itlist goes from the
left (thus, foldr' and foldl' respectively). These functions have two
differences with the functions in the Basis (List.foldl and
List.foldr):

1. the function argument is curried
2. the accumulator comes last, which is arguably better as the partial
application leaving out just the accumulator is more likely to be
wanted than the one that leaves out the list

Add "flipped" versions of apfst, apsnd and uncurry (from Isabelle)

These are "flipped" infixes just as |> is a flipped application
operator.

Thus

pair |>> f

is the same as

apfst f pair

||> is apsnd, and ||-> is uncurry. The latter has definition

fun (x,y) ||-> f = f x y

This is a prelude to better incorporation of the concurrent futures
implementation currently stashed in portableML/poly/fromIsabelle,
which is in turn work towards github issue #575.

Add option_compare to Portable

Put pprint entry-point back into Portable

Now up to Parse.sml

Updated as far as Pretype.sml

Still no use of smpp tech.

Work towards use of PolyML.pretty type for most pretty-printing

Compiles up to src/parse under Poly/ML

Useful functions for dealing with terms up-to aconv

Taken from remove-term-eqtype branch

Remove some early code assuming term is an equality type

Add 2 time-related utility functions to Portable

Add Haskell's $ for infix applications

This can save parentheses. For example, instead of

qspecl_then [`x`, `y`] (conjuncts_then (qx_choose_then `z` mp_tac))

one can write

qspecl_then [`x`, `y`] $ conjuncts_then $ qx_choose_then `z` mp_tac

(where the space saved by parenthesis-removal has been wasted on extra
white-space...)

Move many things from Lib into Portable

The signature of Lib remains unchanged, but these functions that do not
depend on any HOL-specific stuff can now be used more widely.

Add Theory.quote_adjoin_to_theory. Use this in llistTheory.

This should close #304.

This has been implemented using a new function Portable.quote_to_string_list. Other uses of adjoin_to_theory under src/ have been updated.

Define sort_vars for use w/RESORT_{FORALL,EXISTS}_CONV

Provide string replacement function for Portable

(From CakeML's preamble.)

Better document our use of the Susp code from Moscow ML.

Unfortunately, a Moscow ML 2.01 bug (now reported) means we end up
having to use a new name (HOLSusp) to get the dependencies working
properly. Without this change, building the standard kernel on Moscow
ML would always recompile Thm.sml, seemingly because it couldn't see
the non-existent Susp.ui in SIGOBJ (this file only appears there in the
Poly/ML build). There may still be a Holmake bug here too.

Moved a bunch of things from tools-poly/poly to portableML/poly.

Still to do: make Poly Arb{int,num} use Poly's built-in arbitrarily
large integer type. Also want to get rid of the last remaining
"redirect" in tools-poly/poly/poly-init2.ML.

Reorder the initial build sequence so implementation specific files come 1st.

This will make fiddling with the Poly/ML build easier.

Move the pretty-printing facilities around a bit so that both SML
implementations use our own version of the PP structure. This
implementation is called HOLPP in src/portableML. After the kernel's
Overlay.sml is loaded, it is also available under the name PP. This
retains fairly good backwards incompatibility. The one deliberate
incompatibility is to make references to General.ppstream invalid.
This makes us better conform with Basis 2002.

The advantage of this manoeuvre is to allow me to better control what
our pretty-printers do at a low level.

Debugging Preterm.sml made me write a pretty-printer for pretype
values (and I was almost annoyed enough to write one for Preterms
too). I use Moscow ML compiler magic to get numbers for references,
and have written to the Poly/ML mailing list to ask how to do the same
in poly.

Minor changes to increase portability. In particular, added the Interrupt
exception to Portable instead of assuming that it is in General, and added type
annotations to resolve the types of non-expansive definitions that the smlnj
typechecker doesn't handle (Moscow ML is more flexible with respect to the
value restriction).

Rewrote both kernels to cope with Overflow in Time.toSeconds by instead
going via a real, and using Arbnum. Also simplified the thyid type in
Theory.sml so that the representation was a pair of nums rather than a
time value that was being converted into and out of.

Added a simple way to invoke a prettyprinter to see what it does.

Many small changes, most associated with boolification or lifting.

Added "norm_quote" in Portable.

Added signature to Portable. Trivial changes to Arbnum.