Provide a delete_trailing_wspace : string -> string function in Lib

Add binding for option_compare in Lib

Progress through Parse.sml

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

Compiles up to src/parse under Poly/ML

Add syntax/ops to make set manipulations easier

Remove some early code assuming term is an equality type

Add an op_assoc to Lib (by analogy with other op_ functions)

Ensure HOL4 works with fixed-width integers under Poly/ML.

Integers under Poly/ML 5.6.1 are likely to be fixed-width by default (up until now they've always been arbitrary precision). Some changes were needed to cope with this:

- The Arbint and Artbnum structures effectively assumed Int.int = IntInf.int.
- The Standard ML structure Time is based on LargeInt.int and not Int.int. Code for printing times has been re-implemented using the Date structure.
- The smart-configure.sml file used the Overflow exception to distinguish between Moscow ML and Poly/ML. This test is now based on a difference in the printing of General.Fail exceptions.

Move useful apnth function to Lib

Also make it raise a HOL_ERR rather than a Bind error if the index is
negative or greater than the length of the list.

Add extra term/syntax functions to HolKernel. Also tweak definition of HolKernel.find_terms.

The new definition of find_terms may or may not be quicker.

The new functions are:

list_mk_icomb (a type instantiating version of list_mk_comb)
mk_monop (this is essentially a curried version of boolSyntax.mk_icomb)
mk_binop
mk_triop
mk_quadop
syntax_fns (This is taken from bitSyntax and provides a quick way to define syntax functions. Designed to work with the "mk" functions above.)

Revise more of Parse's pretty-printing APIs.

In particular, remove a bunch of entry-points with names matching
*backend_string* and print_backend*.

The objective with these was to accompany things like
term_to_string (which printed to a raw_terminal backend) with a
printer that printed to the current backend. This is now easy enough
to do with

ppstring pp_term

and

print o ppstring pp_term

The flip of the current_backend reference so that it points at
"raw_terminal" can now also be done with the rawterm_pp function.

The other convenience entry-points that have gone, for the moment, are
those that did all of the above while also removing certain specified
overloads. Because pp_term_without_overloads_on is still present, you
have to make do with

print (ppstring (pp_term_without_overloads_on ["/\\"]) ``p /\ q``);

or

rawterm_pp (ppstring (pp_term_without_overloads_on ["/\\"]))
``p /\ q``;

Closes #13. I will open a fresh issue to do with making the last two
use-cases slightly easier to deal with.

To successfully link to HTML documentation, a space is required before colons in sig files.

I'd call this feature a bug.

Try to standardise the formatting of Lib code.

The changes should hopefully improve code legibility. Have attempted to follow the style guide at
http://mlton.org/SyntacticConventions.

Add a lex_cmp to Lib

and stop using an ad-hoc definition in OpenTheoryMap

Add a n(log n) and linear time topsorts to Lib

Requires input as a dictionary/vector of adjacency lists, whereas the
existing quadratic topsort just takes a list and a partial order on its
elements.

Added functions triple and quadruple for creating tuples.

Added functions to turn lists into tuples (with length checking). Lib.single documented.

Removed itotal from Lib. Please DO NOT use handle _ in your code! Exception
Interrupt should (almost) never be handled without being re-raised. Note that
Lib.total already does the right thing.

Added functions rpair : 'a -> 'b -> 'b * 'a and swap : 'a * 'b -> 'b * 'a to
Lib. These are occasionally useful when working with pairs in SML.

Removed Lib.gather. Use {Lib,List}.filter instead.

Move 4 copies of mapshape in src/bool to Lib.

Also tidy up more of those non-exhaustive match warnings.

Add support for keeping track of real time. This gives more realistic timings
when external tools are being invoked, e.g. the SAT tools in HolSatLib.

Functions apfst and apsnd added. These apply a function to the first (second,
respectively) component of a pair.

An extended version of get_first was added. get_first gets a function f:'a -> 'b option and a list l:'a list. It then returns valOf (f e) for the first element e of l for which f is not NULL.

The new function first_opt is very similar, however, f now gets the position of the element in the original list as well.

Add extremely useful |> combinator (stolen from the standard Isabelle
library). Instead of writing
(f o g o h o j) x
or
f (g (h (j x)))
both of which are painful, write
x |> j |> h |> g
where there is a more natural flow from left-to-right: "starting with
x, we first apply j, then h, then g".

Add a version of List.all for strings to the standard library.

Add a variant of Konrad's trypluck, and document it. Also adjust some
Lib code to use the Basis library's List.revAppend.

Fix to bug spotted by Anthony, whereby the induction
theorem for functions defined by pattern-matching
on literals was failing to be proved. Misc.
simplifications to TFL code plus adding "trypluck" to Lib.

Add some useful functions
get_first : ('a -> 'b option) -> 'a list -> 'b option
bool_compare : bool * bool -> order
flip_cmp : ('a * 'a -> order) -> ('a * 'a -> order)

The get_first function is useful if you want to find the guy that
can be transformed successfully by some function, and you want the
result of the transformation, not the input to it. (Otherwise, you'd
use List.find (isSome o f).)

The get_first name is taken from Isabelle's standard library (I've
used it multiple times under different names throughout HOL).

bool_compare should be in the Basis Library but isn't.

Combinators A and B removed (dead code, not used anywhere).

Added fold_map and separate.

Add a new utility function, unprefix, which removes a putative prefix
from a string, or raises an error if it's not a prefix. (There is a
function of the same name and behaviour in the Isabelle library.ML.)

Rename Lib.concat to Lib.strcat so that when Lib is opened (via HolKernel) in
an interactive session, the SML pervasive concat isn't shadowed.

Additional functionality for abbreviations.

1. The labels library has been merged into
markerLib and the src/labels directory eliminated.
2. Have added markerSyntax structure.
3. Operations on abbrevs used to all be in
structure Q, even those that didn't deal
with quotations (like UNABBREV_ALL_TAC). Now
markerLib provides all abbrev. operations and
these take terms. Operations that benefit from
quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc.
are still to be found in Q.
4. Abbrevs are kept reduced by the simplifiers and
there is a REABBREV_TAC which can be separately called.
This sorts abbrevs topologically, so that they get
restored in a sensible order.
5. For situations where one wants to get rid of all
abbrevs, apply a tactic, and then restore the abbrevs,
there is WITHOUT_ABBREVS: tactic->tactic.
6. Have added a simple topological sort to Lib.
7. Updated proofs in the src directories, and also
in examples/lambda.

Add a mapi function to accompany the similar appi.

Random other bits deemed useful.

Define now handles simple definitions defined by
pattern-matching against (numeric) constants, e.g.

Define `(f 0 = 1) /\ (f 1 = 1) /\ (f n = f (n-1) + f (n-2)`;

But more testing/robustification needs to be done.

In Feedback, changed some errors into warnings. This lets some files
get reloaded via cut-and-paste after being "load"ed. Helps for
debugging.

In Lib: added itotal, which is like total, except it also catches
Interrupt and turns it into NONE. Also added a type of "verdicts",
used for the "failure monad". We should gather all the monads
used in the system somewhere (probably in prekernel).

Another useful function (the sort of thing that should be in the Basis
library but isn't) for working with comparison functions.

Add a version of app that passes in the index of the list-element being
operated on.

For portability, the frag datatype and constructors should come from the
Portable structure and be exported to the top level by opening the Lib
structure.

Some more useful manipulations on compare functions (these really should
be in the Basis library).

Pretty significant "refactoring" of the early source code. All the stuff
that was in common between 0 and experimental-kernel moves into a new
prekernel directory. This can be thought of as the kernel utilities
directory, full of code that is not quite portableML because it's fairly
HOL specific, but that isn't really part of the core implementation of
types, terms and theorems.
(Also add a new pair_compare function to Lib.)