Remove eqtype declaration for term type

fix issue #416

fix bug in case expression pretty printer

In case a sub-casesplit is splitting on not a pattern variable then stop
splitting. A comment said this should be the case already, but this did
not work.

decision-tree case expressions: fail when mixing literals and constructor patterns

Before, it was possible to mix literal and constructor patterns in one
column. The results were not as intended though. For example

``case x of 0 => 0 | 1 => 1 | SUC _ => 2``

is compiled to (with pretty printing turned off)

``literal_case
(λv.
if v = 0 then 0
else if v = 1 then 1
else if v = SUC m then 2
else ARB) x``

The pattern "SUC m" is handled as a value. "m" is a free variable of the
resulting case expression. It is not - as most likely intended by the
user - matched against "x".

The problem is that this case expression mixes literals and constructor
patterns. The documentation states explicitly that this is an
unsupported case expression. I thought the parser would fail on such
case expressions. I suspect (but am uncertain and could not find
anything going through the old versions) that it did at some point.
Anyhow, this commits adds such a check during pattern compilation now
that prevents such patterns from being parsed.

Implement fix for issue #271.

fix issue #196

Delete some trailing whitespace

Improve error message when a user provides a bad pattern.

Closes #119

cleanup of Pmatch

Following a suggestion of Anthony, I cleaned-up the interface of Pmatch.
To this end, I moved much of the heuristics-code to a new library called
PmatchHeuristics. This new library is used by Pmatch. This allows to
clean-up the code and interface of Pmatch. If less frequently used functions
are needed, the library PmatchHeuristics has to be used now.

minor tweaks for pattern matching

added trace "pp_cases" that allows to turn pretty-printing for case-expressions off

added exhaustive pattern match heuristic (useful only for very small examples)

execute several heuristics for pattern-matching and choose the best result
interface of pattern matching simplified

implemented qba heurtic for pattern matching; don't do splits for which
lead to same result for all cases

started with writing more complex pattern match heuristics

modify pattern matching to use heuristics for picking the column to split on

Report bad-pattern errors more specifically.

Closes #107.

Fix bug in parsing of case-expressions involving “literals”.

Issue arises when the parsing code thinks that it’s seeing a literal,
which it does on seeing a “if var = exp then e1 else e2” under a case
expression, even when exp includes free variables. (The same buggy
behaviour was seen before the case-const arg-flipping work began, but
it had to be a bool_case term then.)

The fix is to make the parsing code check that the exp in expressions
such as the above really does have no free variables. Then it can
treat that as a literal case expression.

Remove duplication of code between Pmatch and TypeBasePure.

The case-syntax code in the latter has moved entirely to Pmatch.

Fixed a bug in Pmatch (residual assumptions about argument order).

This is progress with github issue #97.

Changes bringing Pmatch more into line with revisions to tfl’s Functional.sml.

Move mk_pattern_fn from old Functional structure to Pmatch.

Obvious (but insufficient) fixes for Pmatch.

Change src/bool to src/1 as a prelude to experimentation!