Don't report tyvar guesses when warning of actual typecheck errors

Also check for "atomic" preterms (a question that only comes up
generating the error message) without converting to full-blown terms
first.

Remove some early code assuming term is an equality type

Fix bug in free-var calculation for preterms (with test)

Reorganise flow of overloading resolution

This should let more specific errors escape the process. Now, the test
case in the selftest lets a (located) error about the impossible
interaction between < and T escape to the user. Previously, 3 + 4 <
T (with < and + overloaded to integer and number possibilities) was
just generating the "no resolution of overloads possible" message
without a helpful location.

Remove unnecessary/unused code from Preterm

Start to refactor parsing-in-context code

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.

Move Preterm datatype definition to separate file.

As was done with Absyn in 019a332d49, this reduces redundancy and helps
with Poly/ML's pretty-printing

Add entry-points to let parsing to return >1 parse

This is possible in the presence of overloading.

Also some minor tidy-ups in the body of Preterm.sml (more still to be
done in this vein).

Get Defn to compile; also report ambiguous overloads

Set comprehensions will be the next task

Get BasicProvers to compile

Switch type-checking to errormonad everywhere

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

Get basic kernel working

Interactive behaviour in terms of error messages and the like may still
be broken.

Make progress with functional pretype

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

Get Preterm to compile

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.

Allow multiple case-like constants in a grammar

Parsing handled; printing still not quite right

Make "by" quieter when the provided quotation doesn't type check.

Also make sure that a typecheck error message exactly coincides with the
corresponding exception's message.

Minor bug fix: ``&3:num`` should parse to a bare ``3:num``.

Otherwise, the result of parsing includes the unusable
``nat_elim__magic`` term.

Handle variables of different types within case-expressions and Defn.

The code calculating free variables over preterms needs to be aware
that the free variables of

case x of
(a,b) => a + b + c

are x and c. In other words, the variables to the left of the arrow
bind what’s to the right.

Also include a relevant test-case, and improve the output of the
src/tfl/src selftest.

Make Preterm’s public API a bit richer.

Add has_unbound_uvar and mk_fun_ty to Pretype API.

Also document some entrypoints there in the .sig suffix.

Attach locations to the error messages generated when overloading
resolution can't find a type for a constant.

Fix for a bug found by Anthony, caused by syntactic patterns not
getting their pretype variables assigned properly during inference.

Also adjust wordsScript to remove its change to <>'s precedence, and
adjust the other operators in the same place (-- and ><) to use
set_fixity rather than add_infix.

The advantage of set_fixity is that it removes other rules for the
same token. This avoids complaints about grammar ambiguity. Calls to
add_infix can result in multiple rules for the same token through the
grammar.

So, Anthony, if you really wants <> back at original level, please put
it there with set_fixity. Users inheriting wordsTheory can then cope
with <> having a different precedence from elsewhere.

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 use of Raise from Parse.sml, as most sub-modules are printing
messages anyway, and if they're not, they should (at least under the
control of a trace variable)
* Also add location information to the 'last error' information in Preterm.

Put the reporting of type-checking errors under the control of a trace
variable, put the message into the exception raised, and also record
the cause of the error in a special reference. This should allow
better programmatic handling of the parser when it might fail.

Added a hook for a "post processing" phase to the term parser.

Parse.post_process_term : (term -> term) ref

By default this does nothing.

----------------------------------------------------------------------

Committing in bug fix for a degenerate case.

Modified Files:
Preterm.sml
----------------------------------------------------------------------

----------------------------------------------------------------------

Committing in fix for minor bug with case expressions.
Before, ``case n of i -> i`` raised an error;
now, it produces ``n``.

Modified Files:
hol98/src/parse/Preterm.sml
----------------------------------------------------------------------

----------------------------------------------------------------------
Enter Log. Lines beginning with `CVS:' are removed automatically

Committing in a new version of literal patterns and case expressions.
This includes a new constant, literal_case : ('a -> 'b) -> ('a -> 'b)
which wraps the previously constructed chains of bool_case expressions
that represent cases branching on literal patterns.

Modified Files:
hol98/src/bool/DefnBase.sml hol98/src/bool/Pmatch.sml
hol98/src/bool/TypeBasePure.sml hol98/src/bool/boolScript.sml
hol98/src/bool/boolSyntax.sig hol98/src/bool/boolSyntax.sml
hol98/src/parse/Preterm.sml hol98/src/tfl/src/Functional.sml
----------------------------------------------------------------------

Fix the bug that was masking HOL_ERRs from within remove_case_magic.
Also reformat the function so that it is a little closer to the left
margin.

----------------------------------------------------------------------
Committing in more polished versions of the literals in patterns code.
The new results should be alpha-equivalent to before.

Modified Files:
hol98/src/bool/Pmatch.sml hol98/src/parse/Preterm.sml
hol98/src/tfl/src/Functional.sml
----------------------------------------------------------------------

----------------------------------------------------------------------

Committing in simplifications/bug fix for parsing literals in patterns.

Modified Files:
hol98/src/parse/Preterm.sml
----------------------------------------------------------------------

----------------------------------------------------------------------
Enter Log. Lines beginning with `CVS:' are removed automatically

Committing in fixes to term parser for patterns with literals.
Also fixes bug in Functional.mk_pattern_fn.

Modified Files:
hol98/src/bool/Pmatch.sml hol98/src/bool/TypeBase.sig
hol98/src/bool/TypeBase.sml hol98/src/bool/TypeBasePure.sig
hol98/src/parse/Preterm.sml hol98/src/tfl/src/Functional.sml
----------------------------------------------------------------------

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.

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.

If a case-expression had functional type and was applied to one or more
arguments, the parser bodged it, and didn't convert it correctly.

Starting to remove redundant (and potentially error-introducing) infix
declarations.

Adapting to new Basis (and SML/NJ).

Welcome to the 1980s... type and overloading errors now report
source-file locations!

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.

Sacrilege!

+ I abolished the Meson: ... spots!
+ Ditto for <<inventing new type names>> and <<overloading>> messages
+ save_thm now prints the name of the theorem it is saving.

Actually, all of the above only happens when Globals.interactive is
false, i.e., when Holmaking/building the system.

Hope you like the new look!

Register a trace variable from the type-checking process.
It's tempting to put type-checking error messages under trace variables
as well.

Modifications to implement parsing and printing of case expressions.

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

Interface by which TypeBase can augment preterm conversion with case
information.

Even better error-handling. Now copes with
``(1 + x) y``
better.

Slight extension to error-reporting capability in type-checking.
If you now type in ``1 + T`` where + might be either integer or
natural number addition, then the behaviour is as follows:

- Term`1 + T`;
No possible type for overloaded constant +
Wanted it to have type: :bool -> bool -> bool
! Uncaught exception:
! HOL_ERR

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.

If an exception is raised in converting terms (using to_term) in the
typechecking, then the value of show_types was not being reset to its
original value.

Support for new representation of strings.Minor changes.

Latest mods for making everything paired.

Made overload_info type opaque, and added a reverse map to it, under the
hood, which remembers how constants should be printed. Also reworked
Preterm slightly to stop it carking on type-checking errors involving
overloaded constants (things like `0:bool`, if nothing else).

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.

Improved the reporting of type errors by having constants be annotated with
their types when printed.

Modified warning message to fit onto one line.

Reorganised the interface to Preterm; with sensible names for functions,
and all of the useful ones exported.

Added a comment to print out a message saying that overloading resolution
might take a while in certain cases.

Greatly improved the efficiency of the treatment of the overloading when
type-checking is done. This results in what appears to be a threefold
speed-up. However, parsing as a whole is still too slow and this is
because of the lexer being so inefficient.

Fairly extensive changes, implementing a scheme whereby each theory keeps
track of its own personal grammar value, which can then be relied on by
other libraries. This is in contrast with the term_grammar() value. This
gets changed all the time, and library implementations can't really rely
on it being sensible.

For example, numLib quotes a term involving >. If this symbol was over-
ridden or messed with in some other way, before numLib was loaded, it
would try to parse that term and come a cropper. No more.

Changes in Preterm are more to do with trying to improve the error
reporting from the type-checking, particularly as with regards numerals.

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.

Bug fix; error message when a type constraint unification failed wasn't
being generated.

Many changes to allow numerals to be overloaded as well as operators.

Changes to get overloading to properly resolve types. I claimed yesterday
that if an overloaded constant didn't have its type determined by normal
type-checking, then it could be instantiated with any type in the candidate
list of types because if type-checking hadn't constrained it, then it
must be OK. This is rubbish though, because there may be constraints
implicit in other overloaded operators. For example, imagine that ~ is
overloaded to be both a boolean operator (not) and over integers
(negation).
Further, imagine that + is overloaded. Then consider the phrase
~x + 2
If we just guess the first type that comes to hand for x, then we may guess
bool, and this will be wrong, because the + has to go to num->num->num or
int->int->int. So, we need to do backtracking unifications through all
of the possibilities. Hence the use of seqs and seqmonad to implement
this.

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.

A number of changes, doing away with the old Pretype and Strm modules.
These changes support the new implementation of the ParseDatatype
module, which now refers to the type parser provided in this directory,
meaning that ParseDatatype can see new user-defined type infixes as and
when they become available.

Small changes to accomodate new-look of portableML.

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

Modified definition of is_atom in order to get better behaviour while
printing type checking error messages. Numerals are handled correctly,
and constrained terms are also considered atomic.

Initial revision