Remove unused code in Parse_support

Make progress with functional pretype

The change to pretty-printing raises an exception, but parsing simple
cases seems to work.

Begin to make pretypes purely functional

I want to do without the references that are used in the unification
algorithm.

Slightly more open-ness in core src/parse APIs

Allow for user "preterm processors"

These are inserted into the process where the abstract syntax gets
turned into preterms, and can call back to the builtin processor if
necessary.

Something like this is necessary if you are going to mess with binding
structure and need to do so in a way that is itself aware of what the
context's free variables are. This technology is needed for
pattern-matching, and should allow us to move the handling of
set-comprehension out of src/parse as well.

Make Parse_support API more open

See earlier (reverted) 9fc2c8a

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

Open up some of the internal parsing APIs

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

Rename Parse_support.make_case_arrow

New name is old_make_case_arrow, with intention that this is only called
with pmatch_on is false.

Polish preterm API to remove unused parameter.

make_qconst didn't read/use its overload_info parameter, so there seems
no point having that parameter in the API.

Variables in the patterns of case expressions are now properly
'fresh'. They bind expressions on the other side of the case-arrow,
but do not affect variables outside the case expression or in other
branches. This revealed a bug in DecodeScript, where a theorem about
encoding sums ended up being about sums of type 'a + 'a only because
case pattern variables that should have been independent weren't.

Modifications to support overloading to a pattern. For example, one
can now do
overload_on ("<>", ``\x y. ~(x = y)``)
The parser does the right thing. The pretty-printer remains
blissfully ignorant for the moment. I don't think Unicode aliasing
will work quite yet either. Backwards compatible in that all the
functions in Parse behave the same if given inputs that were
previously acceptable.

"The parser does the right thing" means the following

- set_fixity "<>" (Infix(NONASSOC, 100));
> val it = () : unit

- ``$<>``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``\x y. ~(x = y)`` : term

- ``$<> p``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``\y. ~(p = y)`` : term

- ``p <> q``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``~(p = q)`` : term

When the pretty-printer is working correctly, the output will probably
be

``\x y. x <> y``

``\y. p <> y``

``p <> q``

In the first two cases, fixing what would appear to the user to be an
odd eta-expansion may be too difficult.

Revised exportML so that it takes a path parameter, which tells
where the ML corresponding to a theory is to be written.

This has been propagated to all the theories that already export
ML, and the mkword.exe tool has been upgraded to also take a
path where it should write the generated ML. This is useful,
because doing an exportML to the same directory as the theory
files will end up confusing Holmake.

Add a Locn field to each constructor of Preterm.preterm, in
preparation for located type error messages etc.

* Thanks to Joe Hurd for helping locate a bug in an earlier version:
Preterm, while still an equality type, is no longer safe to compare
for equality. Instead, Preterm.eq must be used; this ignores the
locations. (The symptom was a parse_in_context failing to notice
that the binder variables were the same as the bound occurrences,
leading to weird failure in Q.PAT_ASSUM).

* Constrained and Antiq now take records, to accommodate the Locn field.

* Lots of small changes, mainly adding ",...", to code using preterms.

* Pass locations down into the preterm constructor functions.

Further improve error reporting:

* make_atom failures (e.g., update of nonexistent field) now give
located errors; ditto all friends in Parse_support. Modified
absyn_to_preterm and Parse_suport.* to pass locations downward to
accommodate this.

* Fix a bug in parse_term that was causing ranges to be confused for
certain sequences of tokens (was reporting left edge of last token
to right edge of first token, oops!).

* Add text " (possibly missing semicolon)" to error "May not use
record update functions at top level", as this is a common error.

* Fix a small bug in location-handling in type_tokens.

Other changes:

* Remove another printing of the tail of the input (no longer
necessary).

* Various code tidy-ups.

* Reduce Loc_Near (Loc_Near locn) to Loc_Near locn (otherwise they
pile up dramatically!).

Minor change.....

Support for new representation of strings.Minor changes.

Treatment of known constants and overloading was bogus. Now known constants
are just the domain of the map in the overloading info. reveal now
puts all constants of the given name into the overloading map. Will
have to add a precise function for removing pairs from this.

Changes to bring about Kananaskis parser. Known bug exists in
treatment of qualified identifiers.

Implementation of move of hide/show information from Parse_support list
into grammars.

Big raft of changes allowing a simple form of overloading to be supported.

Implementation of type checking is now entirely above the level of the
kernel. New TCPretype module (type-checking pretype) implements much
of the required functionality, including type unification.
Parse_type generalised to target any type providing the appropriate
constructor functions.

Change to antiquote processing. Now free variables in the antiquotation
will affect type inference in the surrounding term. This is the
way it was done in HOL88, but not HOL90.

Also, some now outdated code has been removed.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Initial revision