Improve error message emitted by Q.SPEC_THEN

Thanks to Tom Sewell and Heiko Becker for the bug reports.

With test case.

Closes #754

Implement INST_TYPE facility within Q.SPEC_THEN

Closes #718

Make Q.RENAME_TAC and friends quieter

With test-cases.

Closes #499

Remove eqtype declaration for term type

Provide access to more switches when parsing in context

In particular, allow setting of Feedback traces which will be used
when parsing of quotations occurs.

This allows Q.PAT_ASSUM to be made quiet about inventing type
variables. This is deemed desirable in github issue #425. (I'm not
100% sure now of this, but hey.)

Closes #425

Allow Q.MATCH_RENAME_TAC (and friends) to backtrack over pat. parses

When a pattern is passed to `Q.MATCH_RENAME_TAC` (and others in this
family), it is parsed once (making a fixed choice for overloaded
names) and then used as a matching-pattern. The behaviour should be
that all possible overload-choices are used as possible patterns.

Less clear is how the choices in the assumption and subterm based
tactics should be ordered: for example it might be:

<choose parse> -> <choose assumption/subterm for match>

The current implementation has subterm selection happening last, but
assumption selection happening first. So, the ordering for
MATCH_ASMSUB_RENAME_TAC is:

find an assumption
find a parse
find a sub-term

Regardless of this order, the parsing only happens once so this
shouldn't any difference to efficiency. This ordering can make a
difference to ultimate user-visible behaviour.

Includes some test-cases.

Closes #430

Fix Q.GENL to handle variables in same order as GENL.

Closes #428

Move Q.ID_EX_TAC to Tactic.

ID_EX_TAC doesn't take any arguments, let alone a quotation, so
doesn't belong in Q.

Closes #359

Use cache Absyn to speed up QTY_TAC

Addressing github issue #383

Make more functions in Q use Q_TAC and QTY_TAC

This should make the behaviours more uniform, and certainly makes the
definitions shorter.

By using Q_TAC, code can backtrack over multiple possible parses (which
are caused by overloading). In places where success/failure can't be
distinguished by subsequent backtracking, the old code is retained. For
example, in Q.ABS, once you have a successful parse of the right type,
the use of the parsed term in SPEC is always going to succeed.

The exception is the definition of ISPECL_THEN, which stays complicated
because you have to parse the list of terms all at once, and pass them
to ISPECL. As per the comment in Drule, just iterating ISPEC "DOESN'T
WORK". (This is because you want to calculate one type-instantiation all
at once. Iterating may cause later type variables to get identified with
earlier ones by earlier parts of the instantiation.)

Modify Q_TAC to try all possible parses

This makes a difference in the presence of overloads. Modify
implementations of Q.SPEC_THEN and Q.SPECL_THEN to use QTY_TAC (making
them simpler), and check that they seem to behave as desired with some
test-cases.

Use new typed-quotation-parsing APIs in Q

This removes need for Q to define its own versions of these, and brings
PAT_{,X}_ASSUM back into line with its old behaviour, whereby it (quite
reasonably) asserted that the provided quotation should have boolean
type.

Stop boolean parsing in Q from applying hook twice

The post_process_term hook gets applied to terms at the very end of
parsing (as part of Preterm.typecheck), but the internal btm function
was calling it again

Rename pat_assum to pat_x_assum; provide pat_assum

To be consistent with naming conventions elsewhere, change the name of
qpat_assum (and PAT_ASSUM, and Q.PAT_ASSUM) to include an extra _x_ (or
_X_), indicating that the matching assumption is pulled out of the
assumption list.

Use the old names to provide a version that doesn't pull the assumption
out of the list.

Again, seeking consistency with other similar tactics, make variable
names that appear in the pattern and the goal be forced to have the type
that they have in the goal.

Implement Q.RENAME_TAC / bossLib.rename

This tactic is more powerful than rename1 as it allows multiple patterns
to be matched at once, and without regard to the initial goal's free
variables (which might otherwise cause unpredictable clashes).

Rename: qcase_tac/rename1; Q.FIND_CASE_TAC/Q.RENAME1_TAC

This use of the "case" substring was just confusing given things like
Cases_on. The "1" is there because I want to now implement a more
general version that
- deals with the issue (identified in the .doc file), where existing
names in the goal can still get in the way; and
- allows multiple subterms to be matched and renamed as a unit

Though seemingly independent, the second feature is really needed if the
first is to be done: implementing the first will require all the free
variables in a goal to be renamed away (to genvars, I expect), and then
it's impossible to ground particular matches against known free
variables.

Define special backtracking cases of pat_assum

In particular, the "pattern" is a single term or quotation that has to
either be the head constant of the assumption or the head of the lhs of
the assumption. Unlike pat_assum as it stands currently, the behaviour
backtracks (à la first_assum) if the theorem-tactic doesn't succeed with
the first assumption found.

Versions come in "copy assumption" and "cut assumption" versions, just
like first_assum and first_x_assum.

implement abbrevation tactics for subterms.

Fix bugs in Q's match_{rename,abbrev} tactics; refine spec.

In particular, make sure that instantiations arising from the matches
are applied in an order that is sure to make the substitutions apply
as much as possible. There are two obvious ways in which things can
go wrong (resulting in a goal-term that doesn't in fact look like the
supplied pattern).

1. If the match results in an instantiation that has a variable
binding a term that appears within another. E.g., (example from
Ramana):

Q.MATCH_RENAME_TAC `f v = z` (?- `f (h s) = s`)

The match will return (v |-> h s, z |-> s), but if this is applied
with the z going first, the goal won't contain `h s` when the
substitution for v is attempted. So that's bad, and affects both
renaming and abbreviating tactics.

The fix is to sort the instantiation list so that larger terms are
substituted out first.

2. Distinct variables in the pattern may end up binding the same
term. This is something users are less likely to bring about, but
it still seems worth trying to nail down what the behaviour should
be. E.g.,

Q.MATCH_RENAME_TAC `a + b = 10` (?- 5 + 5 = 10)

This will want to bind a and b to 5. When abbreviating, you might
like to see abbreviations `a = 5` and `b = 5` in the assumptions,
and when renaming or abbreviating, you might like to have the goal
become `a + b = 10`. Achieving both these might be possible, but
seems hard. Instead, the operational approach of performing
substitutions in a sequence is stuck to, but the substitution is
sorted so that the variable with the earlier name goes first. This
means you'll get ?- a + a = 10 as the goal, and when abbreviating,
you'll get `a = b` and `b = 5` as abbreviations in the
assumptions.

The fixes in examples/ are generally because proofs have relied on
abbreviations *not* occurring, despite the presence of variables in
the pattern. The situation is analogous to the situation in 1. above,
where the user has exploited the fact that a binding hasn't been
introduced for v.

Change API of Q's MATCH...RENAME_TACs.

Now rather than a string list hanging off the end specifying which
variable bindings aren't supposed to induce a renaming, just put
underscores into the pattern in those positions.

Documentation and release notes updated.

Fix a bug in Q.MATCH_{GOAL,ASM}SUB_RENAME_TAC

The old code wouldn't allow a match to go through if the returned
instantiation was empty, but some patterns don't have any free
variables, so this was bogus. The new check is more careful: it
requires the instantiation to be exactly the right size.

Document new FIND_CASE_TAC.

Implement Q.MATCH_ASMSUB_RENAME_TAC.

Progress with #81.

A renaming/matching tactic that matches against subterms in the goal.

Progress with Github issue #81 (which also calls for the same against
assumptions and an abbreviation version too).

Implement new scheme to allow simple addition of theorems to theorem "sets".

When saving or storing theorems, simply add [name1,name2] strings to the
end of the binding, and the theorem being saved will be added to the
theorem set with that name.

Add Q.GENL.

Fix a bug in Q.REFINE_EXISTS_TAC.

This failed if the goal had more than one existential quantifier. Add
a selftest to check for the right behaviour.

Added MATCH_ASSUM_ABBREV_TAC to Q and markerLib.

This completes the set of pattern-matching tactics spanning the two dimensions of abbreviate/rename and conclusion/assumptions.

Two new tactics in Q for renaming parts of a goal by pattern matching.

MATCH_RENAME_TAC works on the goal statement; MATCH_ASSUM_RENAME_TAC on the
assumption list. Both tactics attempt to match a pattern against the goal (or
an assumption). Matching parts of the goal are then replaced by the
corresponding pattern variables.

Useful for renaming ugly generated variable names with minimal effort. The
pattern does double duty in the assumption case: it both picks out the matching
assumption and also specifies what the new variable names should be.

Stop double-reporting of type-check errors in various Q tactics.

The issue is that when parsing becomes part of a tactic application,
the type-checking of the quotation will print out its usual error
message and raise an exception containing the same information. This
exception is then Raise-d by the proofManagerLib.expand ("e"),
resulting in the same information being printed out twice. The trick
is turn off the printing of the message during the parse by using the
show_typecheck_errors trace.

Recently I was writing structures like

Q.EXISTS_TAC `e1` THEN
Q.EXISTS_TAC `e2` THEN
...
Q.EXISTS_TAC `en` THEN

in my proof scripts a lot. This is lengthy and tidious. So I added

Q.LIST_EXISTS_TAC [`e1`, `e2`, ..., `en`]

as a shortcut.

Fix Q.INST to also heed free variables that appear in a theorem's hypotheses.

Additions to multiset and primeFactor
theories. Fixed definition of PRIMES
sequence in dividesTheory. Also added misc.
theorems to arithmetic. Some amount of
meaningless shuffling about.

A minor change required in light of change to parse_in_context. If
you are possibly instantiating a theorem with the subst `a` |-> `n`,
and there is no free variable `a` in the term, but there is an `n`,
then the old implementation would raise an error. This was because it
would parse `a` to be ``a : 'a``. It would then require `n` to have
that type, causing a clash with its real type. So, the new
implementation just drops an subst-pair that will never do anything
anyway.

Remove an unnecessary dependency on tautLib.

Additional functionality for abbreviations.

1. The labels library has been merged into
markerLib and the src/labels directory eliminated.
2. Have added markerSyntax structure.
3. Operations on abbrevs used to all be in
structure Q, even those that didn't deal
with quotations (like UNABBREV_ALL_TAC). Now
markerLib provides all abbrev. operations and
these take terms. Operations that benefit from
quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc.
are still to be found in Q.
4. Abbrevs are kept reduced by the simplifiers and
there is a REABBREV_TAC which can be separately called.
This sorts abbrevs topologically, so that they get
restored in a sensible order.
5. For situations where one wants to get rid of all
abbrevs, apply a tactic, and then restore the abbrevs,
there is WITHOUT_ABBREVS: tactic->tactic.
6. Have added a simple topological sort to Lib.
7. Updated proofs in the src directories, and also
in examples/lambda.

Changed behaviour of simplifier to
propagate the abbreviation coming from
a let binding in the goal being moved to
the assumptions. This helps keep the goal
in "fully abbreviated form". Also added

Q.REABBREV_TAC

which re-abbreviates the goal and

Q.WITHOUT_ABBREVS tac

which temporarily removes all abbreviations,
runs tac, then reabbreviates.

Probably, Q is not the right place for these
functions, but the rest of the abbreviation
stuff is there.

Also added some internal documentation on what
Q.ABBRS_THEN does, and the like.

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

Parse.post_process_term : (term -> term) ref

By default this does nothing.

Fixed bug in Q.EXISTS, spotted by Eunsuk Kang and Joe Hurd.

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

Two changes.

1. Moved definition of ty_antiq to Parse so that it will
appear in the docs. Other changes arose.

2. "Fixed" HolCheck so that it builds. Is this a
difference between the std and expt kernels?
The change swaps type variables in arguments to
type operators so is probably not what Hasan had
in mind.

A little code reorganisation and a fix for a bug in the implementation
of ASM_SIMP_TAC and FULL_SIMP_TAC: abbreviation references in the
argument list weren't being dealt with early enough. In the case of
ASM_SIMP_TAC this caused the effect of an abbreviation being eliminated
in the assumptions but not in the goal.

New treatment of abbreviations. Documentation still to be updated.
Backwards compatibility illustrated in examples/lambda/standardisationScript
and examples/arm6. New techniques and entry-points illustrated in
core distribution and some of the lambda example scripts.

Provide "backup copies" of the old implementations of the abbreviation
tactics so that old proofs (such as those in the arm6 examples) can go
through even as the abbreviation tactics evolve. First evolution is to
modify UNABBREV_TAC to remove the abbreviation assumption, and to do
a SUBST_ALL_TAC rather than just a SUBST1_TAC.

Have to add the new functions to the signature. Take the opportunity to
define type abbreviations and align all those pesky colons.

A couple of new and useful tactics (documentation to follow).

Fix for bug 916157 (from Lockwood Morris). Q.UNDISCH_THEN now behaves
like UNDISCH_TAC rather than PAT_UNDISCH_TAC.

Want matching on the goal and not on the assumption list (to avoid abbreviating previous
abbreviations created using the same pattern), and do not abbreviate variables or
constants (this isn't helpful and can be done with ABBREV_TAC).

Modified so that free variables in the goal (assumptions included) are
treated as local constants when matching against the pattern is done.

Thanks to Joe for this modification that enables PAT_ABBREV_TAC to come up with a variant
of the variable name.

Implemented Anthony's PAT_ABBREV_TAC. He should write some documentation
for it :-)

Arrange that error messages give *absolute* locations (within a file),
rather than *relative* (within a fragment).

* add absolute locations to src/0/locn, with rendering.

* make unquote (tools/quote-filter/filter.lex) insert "location
pragma" comments (*#loc <row> <col>*) into the text of quotation
fragments. The pragma indicates the absolute location of the
character following the final close paren, and may appear anywhere a
comment may. They are actually inserted at the beginning of a
quotation, and after each newline.

Note that we actually insert a space before the pragma, to work
around a pre-existent problem with the lexer: a comment is not
recognised as such if it is preceded by an open paren or a symbol.
I have placed the text of the commit message explaining this, as a
comment, in the source file of base_lexer.

* make a comment on filter.lex's drop_upto less misleading.

* make the base_lexer read these location pragmas, and use them to
obtain an absolute location for each token.

(We recognise location pragmas even inside string constants; this
may be an error but is in any case an unlikely scenario.)

* add functions to src/0/Lib that strip leading comments from a
quotation, for use in places where the usual lexer is not used (Thm,
Q.GEN, Q.UNABBREV_TAC, and some Boolify/test stuff).

* arrange that Thm can accept comments and multi-fragment frag lists
(this is necessary because Holmake now runs unquote over *all*
files, including *Theory.sml files, as noted in a previous commit).

Fairly radical changes: theorems' hypotheses now stored in a binary tree.
Also made INST behave in a generally smarter fashion.

Had wrong UNDISCH_TAC.

Feh. Paired syntax.

New versions of old stuff.

Fixed bug whereby UNDISCH_TAC wasn't parsing in context. Found by
Anthony Fox.

Theorem argument to the new SPEC_THEN functions must be last for
better composition with other tacticals. Want to be able to write
things like
FIRST_X_ASSUM (Q.SPEC_THEN `x` (Q.X_CHOOSE_THEN `y` SUBST_ALL_TAC))

Added SPEC_THEN (and obvious friends) to make it easier to specialise
theorems in the middle of proofs and use the current parsing context.

Added REFINE_EXISTS_TAC, which allows you to turn an existential goal
into a new existential goal, where the variable has been replaced by
a more concrete term.
E.g.,
?n. 0 < n
================ REFINE_EXISTS_TAC `SUC m`
?m. 0 < SUC m

Fixes due to implementation of move of hide/show information from
Parse_support list into grammars.

Modifications to improve some error-message reporting.

Accomodates fact that Ho_tactics now gone: PAT_ASSUM found in
Tactical instead.

PAT_ASSUM revised to include parse_from_context call.

Modified Q.prove to be in line with prove, i.e., taking a tuple of
arguments.

Revised to use parse_in_context wherever possible.

Modified definition of PAT_ASSUM to fit in with the "real" PAT_ASSUM,
which is now in a different structure (Ho_tactics).

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

Initial revision