Make type-checking handle antiquotes more efficiently

Previously, all antiquoted terms were converted back into preterms
before the machinery in Preterm ever saw them. Now, these terms get to
stay as terms. They are still scanned so that their free variables can
influence those in any surrounding term. This also preserves the way in
which something like

val t = mk_conj(``x:bool``, ``f x:bool``);
``^t``;

raises an exception.

Remove unused code in Parse_support

Fix parsing/type-checking of set comprehensions

Fix a bug in handling of case expressions

Also fix Holmakefile so that selftest gets recompiled properly under
Moscow ML.

Switch type-checking to errormonad everywhere

The optionmonad doesn't hold any advantage, and flipping back and forth
between them was just annoying.

Make progress with functional pretype

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

Change error monads to wrap the state & result

So, the state-error monad (called optmonad here) changes from

'state -> ('state * 'a option)

to

'state -> ('state * 'a) option

No doubt there is some precise monad-transformer jargon I could use to
describe this change.

The advantage of the latter is that it makes for an easy lift into the
seqmonad (which replaces option above with seq).

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

Minor tweak to default-case handling

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

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

Implementation and test-cases for pmatch parsing

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.

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

Identifiers composed entirely of underscores are now replaced by
uniquified versions (formed by appending digits in a gensym like
way). This makes
``case p of (_,_) -> T``
(and other more realistic variations on this theme) work properly.
This is of use when there are multiple underscores in the one pattern.
My previous check-in already handled the slightly different situation
in
``case l of _ :: t -> LENGTH t || _ -> 0``

I have not touched TFL's code for doing the same thing in function
definitions, which still runs and does its thing. Though now
redundant, I believe, I figured we might as well keep it running, if
only to preserve its choice of variable names.

Note that uniquification happens everywhere, so that if you enter
``_ /\ _ /\ _``
you get back
> val it = ``_0 /\ _1 /\ _2`` : term

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.

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

Recast strings as lists of characters. The type :string is now an
alias for :char list. The old constant names (STRCAT, STRLEN, STRING,
EMPTYSTRING) are retained, but they are now just parsing/printing
forms for (APPEND, LENGTH, CONS and NIL). String literals still work.
For the moment, the string names are also preferred when printing,
though I think there's a case for just printing with the list names.
(Of course, the list names are used when the arguments are not of type
:char list.)

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.

Remove what I now think is an unnecessary sanity check. In
particular, there is already code elsewhere that prevents use of
numerals or string literals as bound variables. Without this check
being eliminated, the system forbids use of Unicode characters that
aren't also ASCII in bound position.

Updates to make large string literals parseable. This required two changes:
* the parsing process doesn't bother making literals into preterms, but
takes them directly to anti-quoted terms. This avoids lots of term
traversals in Preterm.sml
* but remove_case_magic is unavoidable (it is over terms, not preterms),
so rewrite this to be tail recursive. It now also avoids rebuilding
terms unnecessarily. Code for doing this is a little involved.

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.

Implement a new pretty-printing/parsing notation for character literals.
Use the SML notation for this. For example, #"f", and #"\"". This notation
was easy to implement because lexing could piggy-back on the handling
of strings. I also think that compatibility with SML is a good thing.
Changing the notation should be easy enough if we do decide to do this.
Pulled the character pretty-printer out of stringSyntax as well.

Changed NUMERAL_BIT1 and NUMERAL_BIT2 to BIT1 and BIT2, respectively.
Sorry, they were just too long. Also, ALT_ZERO is now named ZERO.

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

Must check full build before checking things in (bangs head against wall).

Cause a couple of parsing error messages to be printed out immediately,
rather than just raised as exceptions.

Fixes to building strings (the char type is in stringTheory).

Minor change to parsing set abstractions, to accomodate situation
where one side or the other has no free variables.

Changes to make the type parser handle thy$tyname syntax. This syntax
can only be used as suffixes. Thus: (bool,bool) min$fun, for example.

Fixing problem with prettyprinting the empty string.

Change of CHAR to CHR in code for generating string literals in OL.

Support for new representation of strings.Minor changes.

Slight efficiency change; use the is_overloaded function, which checks
the binary tree directly rather than the known_constants list which first
extracts the keys from the tree and then does a linear search on them.

Latest mods for making everything paired.

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 the way in which constant names are resolved. There is now
a much simpler map from names in the abstract syntax tree to actual
constant terms; everything now goes through the "overload" map.

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

Bug that was causing string constants not to be recognised fixed. (Needless
to say, the previous change caused the bug.)

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

When there was only one choice for an overloaded name, the type variables
in the term chosen needed to be properly turned into unification variables.

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.

When there is just one option available in the overloading information
for a given term, this can be inserted much earlier, removing the need
to do any late inference for this case.

Allow symbolic identifiers as well as normal ones in binding positions.

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.

Numerous changes allowing for printing and parsing of numerals and
treating them as members of different families depending on the contents
of the numeral_info part of the term_grammar. Tested inasmuch the
distribution builds correctly, and with integerTheory loaded.

Changes in Parse to call now-zeroed versions of export_theory etc in Theory.
Changes elsewhere to implement string literals.

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

Implementation of "bare zero" numerals.

Initial revision