Restore ppstream_funs as nullary type operator in term_pp_types

This name is used in user-written code (users' special purpose
pretty-printers), and there is no reason to rebind this name, forcing
them to change things.

Builds core HOL; quotient fails for lack of (temporary) html_theory

patternMatchesLib: improve wildcard normalisation

Now, wildcards, i.e. pattern variables that start with an underscore,
are renamed to proper variable names. This makes case expressions
readable. Before this change, eliminating guards could lead to
previously unused pattern variables (which are replaced by wildcard)
being now needed by not named decently.

patternMachesLib: minor improvements

This commit focuses on the pattern compilation implemented in
patternMatchesLib. Some minor bugs were removed and it was polished.
More selftests were written. Some effort was put into producing decision
trees that pretty print well. This meant inserting "literal_CASE"
expressions. Finally, also the runtime speed was improved.

The speed optimisations lead to further cleanups of PMATCH_SIMP_CONV.
Now, there is a PMATCH_FAST_SIMP_CONV as well as a PMATCH_NORMALISE_CONV
as well. Furthermore, a bug in dest_PMATCH_COLS was removed and the
destruction function made more robost.

patternMatchesLib: improve lifting

The lifting of pmatch case-expressions to the next boolean level was not
implemented well. It was rather slow, there was poor support for rows
with overlapping patterns and variable names were not chosen nicely.

This commit reimplements PMATCH_LIFT_BOOL_CONV and PMATCH_TO_TOP_RULE.
As part of this reimplementation, checking for exhaustiveness got
improved. In this process PMATCH_IS_EXHAUSTIVE_CONSEQ_CONV got renamed
to PMATCH_IS_EXHAUSTIVE_FULL_CONSEQ_CHECK (since it is no consequence
conversion). However, usually the new PMATCH_IS_EXHAUSTIVE_CONSEQ_CHECK
should be used instead.

minor improvements on patternMatchesLib

- speed up PMATCH_SIMP_CONV
- rename PMATCH_REMOVE_SUBSUMED_CONV -> PMATCH_REMOVE_FAST_SUBSUMED_CONV
- simplify guards resulting from removing double binds
- removing double binds now also removes unbound pattern vars
- use variable name "_uv" instead of "uv" consistently. Before, many
tools introduced the name "uv", which was by "PMATCH_SIMP_CONV" then
replaced by "_uv".

patternMatchesLib: avoid replacing double bound vars by wildcards

The simplifications for PMATCH case expressions replaces variables only
used in the pattern with wildcards. If the variable is used multiple
times in the pattern, this leads to confusing output. The pretty-printed
version does not allow to identify these double binds any more (while
they are still present in the underlying term). This commit fixes this
issue.

For example, before ``case l of | x::x::_ => T | _ => F`` was simplified
to ``case l of | _::_::_ => T | _ => F``. This looks like any list with
at least 2 elements was excepted. The internal representation used the
same wildcard var for the first 2 elements though and was therefore
correct.

pattern_matches: fix pretty printing and add additional selftests

In recent changes I produced unnecessary verbose pretty printing. In
case a pattern "p" contains no variables, the notation "| (). | p =>
rhs" was used instead of "| p => rhs". This commit should fix it.

Moreover, more selftests were added to test the behaviour of parser and
pretty printer for case expressions.

tweak case expression pretty printing

- when PMATCH-case expression parsing is enabled, print tree-based case-
expressions as "dtcase"
- if more than the variables used in the patter are bound, print all
variables
- add parenthesis around PMATCH case expressions if necessary

pattern_matches library: use new syntax everywhere

After Michael's work on how to parse PMATCH expressions nicely, they use
the same syntax as decision tree based case expressions. The old syntax
something like `CASE ... OF [...; ...; ...]` therefore needs updating to
`case ... of | ... | ... | ...`.

This commit changes the syntax of case expressions in the examples files
and comments. This did not cause problems before, because this code is
only run manually either during debugging or as a documentation aid.

Moreover, some code that is unused due to Michael's changes now is
removed by this commit.

Properly re-org grammar code, removing rule_fixity

Now there is just one fixity type. Also decide that set_fixity and
set_mapped_fixity shouldn't be in the grammar-delta type; instead the
"remove-termtok" and "add_rule" actions (which can be used to implement
the above) should be.

Fix for minor PMATCH-printing bug

Enable PMATCH with one patternMatchesLib call

Namely: ENABLE_PMATCH_CASES : unit -> unit

This enables dtcase as a method to get old style "decision tree" cases,
and turns on the relevant pretty-printers and parsers for the PMATCH
forms.

Spelling correction: DECEND_CONV -> DESCEND_CONV

Clean up patternMatchesSyntax

1. remove uses of the term parser
2. remove old pmatch-parsing code

Fix pmatch p/printing for () .| SUC n => ... case

Progress with new-style pattern-match syntax

Two things
- give up on using K T as a representation of the "null" guard. This
breaks too much existing code in patternMatchesLib etc
- Modify pretty-printer
- Some selftests

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).

patternMatches: change syntax

Use ||| instead of || everywhere. This avoids the conflict with
n-bit and therefore allows to build HOL 4 again.

This is a temporary measure till Michael implements the changes
discussed in issue #286. Since now HOL 4 builds again, it is
easier to test changes to e.g. EmitML.

move "pattern_matches" examples to "src"