Complete implementation of new API for declaring+using monads

Monadsyntax in general (the do..od notation) can be turned on and off.
In addition, specific monad instances can be declared and subsequently
enabled by just calling something like

monadsyntax.enable_monad "option"

Having state_transformerTheory as an ancestor turns on monadsyntax, and
enables the state monad. (Enabling a monad causes a bunch of calls to
overload to occur; disabling a monad undoes those calls.)

WIP for change to list syntax handling.

Very broken at the moment

Allow multiple case-like constants in a grammar

Parsing handled; printing still not quite right

Undo all pmatch changes to src/parse

I now want to make new-style pmatch parsing happen via the mechanism of
absyn post-processors (as is done with monad syntax). I don't think
that changing the "core" parser is necessary (and it's certainly not
desirable).

Code for new style pattern-match parsing

Syntax as described in github issue #286 parses.

Examples:

> ``case x of 0 => 3 | SUC n when n < 10 => n + 1``;
val it =
``PMATCH x
[PMATCH_ROW (λ_. 0) (K T) (λ_. 3);
PMATCH_ROW (λn. SUC n) (λn. n < 10) (λn. n + 1)]``:
term
> Datatype `tree = Lf | Nd tree 'a tree`;
<<HOL message: Defined type: "tree">>
val it = (): unit
> ``case t of Lf => 0 | Nd t1 x t2 => x + f t1``;
val it =
``PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λ(t1,x,t2). Nd t1 x t2) (K T) (λ(t1,x,t2). x + f t1)]``:
term
> ``x + case t of Lf => 0 | x .| Nd t1 x t2 => f t1``;
<<HOL message: inventing new type variable names: 'a>>
val it =
``x +
PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λx. Nd t1 x t2) (K T) (λx. f t1)]``:
term
> ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 => f t1``;
val it =
``x +
PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (K T) (λ(t1,t2). f t1)]``:
term
> ``x + case t of Lf => 0 | t1,t2 .| Nd t1 x t2 when g t2 > 6 => f t1``;
val it =
``x +
PMATCH t
[PMATCH_ROW (λ_. Lf) (K T) (λ_. 0);
PMATCH_ROW (λ(t1,t2). Nd t1 x t2) (λ(t1,t2). g t2 > 6)
(λ(t1,t2). f t1)]``:
term

I think we do still need a separate notation to indicate no variables
are to be bound, as

| .| pat => rhs

won't work when .| is an infix. Maybe

| ..| pat => rhs

This would be needed in a situation where all of the variables in pat
have to be read as free (referring to variables occurring in a wider
context).

Special internal name for .| infix (pmatch syntax)

Pretty-printer now annotates consts with their real names and types.

In "complicated" overload situations, such as the overloads for NOTIN
and <>, the annotation can't point to a "real" underlying constant,
but does still provide the type for the emacs tool-tips.

In passing, also create a new annotation form, the SymConst as well as
the Const. This is done for the TeX backend's benefit, so that it can
avoid treating things like + the same as normal identifiers. This
works well for math-mode munging where you want "+" to map to $+$, but
want "INSERT" to map to \textsf{INSERT}.

Closes #39

Parse decimal fractions, turning them into divisions.

Client theories need to overload the magic string

GrammarSpecials.decimal_fraction_special

to their division constant in order to get this to work.

Add a new function whereby the pretty-printer can be told to treat
certain "impossible-to-occur-naturally" variables as constants. This
is a prerequisite for my scheme to print "syntactic macro" patterns
(like not-equals, not-a-member, boolean-equality).

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

Changes to make it easier to dispense with the let-and concrete syntax
and put something else there instead. Even without throwing them away
it is now possible to write ``$let`` and have this just be a variable of
type alpha, rather than a parse error. So that's an improvement.
If you wanted to define a constant "and", allowing this would be as
simple as chucking the rule for "and", by using
remove_termtok {term = GrammarSpecials.and_special, tok = "and"}
and then defining the new constant "and" with Define, and possibly
giving it fixities etc, as you might with any other constant. Similarly
for let.

Changes to accommodate the efficient definition and manipulation of big
records. It's not a pretty picture underneath, but the pretty-printer is
called on to make everything look as if nothing has changed.

Added new facilities for dropping or preferring certain numeric types
all at once. Documented one of the new functions, and fixed the
documentation for add_numeral_form, which now automatically adds the
appropriate overloading for "&" (I realised that we didn't need to
force the user to do this themselves).

Changed the way overloading handles numerals slightly so that &x will
now always be resolved as a function away from :num. (Whether it be from
:int or :real.) The drawback is that people need to explicitly overload
& if they develop a new numeric type.

Modifications to implement parsing and printing of case expressions.

Case expressions now parse and convert appropriately. Still to print them.

More changes to Kananaskis parsing. System now doesn't allow for
possibility of overloading to different type instantiations of
polymorphic constants. Nor does it allow for printing of polymorphic
constants in any more than one way.
Treatment of number injection overloading is slightly simplified by
actually having a constant in arithmeticTheory with the magical property
that it can never be parsed as the LHS of an application.

Changing "fromNum" to "&" for consistency's sake.

Quite radical changes which allow for "." to be used as the record
field selection operator. Lexer has changed quite dramatically:
it is no longer responsible for determining whether or not a token
is a "keyword" or not. Instead this is done at the parsing level.

The lexer is also now unable to cope with identifiers that are a mix
of alphabetically acceptable and symbolically acceptable characters.

Many changes, mainly to do with record syntax. Also implemented long IDs
as theory-name$id. All of HOL doesn't quite build because field selection
operator is ->, which is used in the real library. Will change this to be
just a simple "." Have also started on concrete syntax for updates.