Set up bind as an alias for >- in errormonad

This is so interactive uses can be set up to avoid the >- token, which
is handled magically by the quotation filter in "interactive"
settings, and which can thereby cause much annoyance.

Make a use of raw_backend utility actually do something

It turns out that print_from_grammars sets up the backend that will be
used when printing is being performed. Therefore the
testutils.raw_backend utility needs to be applied like so:

raw_backend print_from_grammars min_grammars

in order for the reference to get changed appropriately.

This selftest worked because it was run in a situation where the
backend was already raw_terminal. After the construction of the
heaps, the backend becomes something "interactive" by default.

Also make other tests use raw_backend so that this selftest file can
be run inside a hol.bare or hol environment.

Fix type-grammar becoming unprintable because of a stale tyop

In particular, if a tyop name is reused but picks up a different
arity, a grammar's type abbreviation information might think that
an abbreviation using that tyop is still valid.

Fix let-p/printing to lose spaces after semicolons in binding lists

These spaces are inconsistent with the way semicolons are "spaced" in
all other contexts (monad syntax, lists, sets, function updates).

Thanks to Andreas Lööw for the bug report.

Get irule (and IRULE_CANON) to do right thing with negated conclusions

Closes #775

Improve src/1's selftest

1. emit fewer HOL_{MESG,WARNING}s;
2. cleanup generated scratchTheory.{dat,sml,sig} files after test that
generates them is done even under Moscow ML, which doesn't seem to
implement Process.atExit.

Change testutils API to allow for counting of failures

Don't want to necessarily just always instantly abort. Changes die's
type from

string -> 'a

to

string -> unit

This causes a number of knock-on effects.

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

Fix typo in test description

Make "quoted variables" ($var$(..)) syntax more robust

In particular, they may contain quotation symbols and
backslash-escaped characters that are not necessarily UTF8 safe.

Thus: “$var$(\172)” parses to a variable whose name (as revealed by
dest_var), is the string containing character 172. The pretty-printer
correctly reverses this.

There are yet two infelicities in all this:
- quoted variables with challenging contents (spaces, quotations) need
to be preceded by whitespace to avoid completely confusing the lexer
- the pretty-printer doesn't safely print back quoted variables in
such contexts, so you get something that won't parse

The latter is easy to fix. The first is not.

Modify testutils.require_msg and derivatives to return values

It can be useful to get back the result of a passing test for use in
further tests that build on that.

Knock-on effects where it is now not possible to simply List.app such
functions; they must now have their results explicitly ignored.

Don't use $var$(..) syntax to print overloaded names

These can manifest as variables in the guts of the pretty-printer so
it has to pay attention to its knowledge that they may be "fake"
variables.

Change type_abbrev to not alter printing behaviour

If printing of abbreviations is desired, users must now use
type_abbrev_pp.

Closes #599

Have testutils.die automatically print out "FAILED"

Argument to die is then appended to that, but on a new line.

Adjust some selftests to take advantage of this, though of course, we
don't expect to see the FAILED output for any of them because they're
all passing.

More tweaks to testutils

- change API of check_HOL_ERR to be tupled rather than curried (makes
it easier to write the (fn _ => true) predicate)
- add check_result entrypoint

Provide more information in exceptions raised by Tactical.VALID

Get chained Unicode negations to print properly

Selftests for both the pretty-printing behaviour and the underlying
token-splitting function that this depends on.

mp_then: Make Pat selector backtrack over possible parses

With regression test.

Closes #567

Fix an mp_then/Pat selector bug

Include some more selftests. Thanks to Ramana for the bug report.

Add an mp_then + Pat selector selftest

Make a couple of selftests clean up a bit better

1. in src/1 it generates a scratchTheory, but did not remove the .dat
file
2. in tools/Holmake/tests/coproduct it does not clean testdir2 before
starting, allowing for stale/unhelpful Moscow ML dependency info to
linger there.

Fix pretty-printing bug for large-if-exprs in rator position

Closes #540

Change irule to not include a rpt conj_tac effect

Closes #465

Tweak printing of long function applications

This brings the behaviour (on at least the examples I've tested) back
to the way things appeared in Kananaskis-11.

The change in the munger test only consists of some extra space
characters appearing in the output on a line by
themselves. (Previously the line had just consisted of a newline
without the preceding spaces.)

Another p/printing test-case for if-expressions

Would catch a bug fixed by 709f4dcf04.

Restore ppstream_funs as nullary type operator in term_pp_types

This name is used in user-written code (users' special purpose
pretty-printers), and there is no reason to rebind this name, forcing
them to change things.

Fix p/printers and selftests to agree with one another again

Fixes for mp_then/drule bug found in previous commit

Provide more test-cases as well. Extend normalisation done by
goal_assum after a theorem is returned to it after "resolution".

Test-case demonstrating bug in drule (ultimately mp_then)

Fix mp_then bug: its PART_MATCH variant wasn't instantiating types

(It has a PART_MATCH variant in order to make sure preserve universal
quantification of variables that don't get specialised to make the
match happen.)

Implement & document controlled resolution tactics (drule & friends)

Fix p/printing bug where restriction variables were shown as bound

Closes #503

Add failing test-cases for github issue #503

This bug has the free-bound status of the restricted variable
contaminate the free/bound status of variables within the restriction.
The printer is also too keen to see restrictions as identical when
they are not because the freeness of variables within the restrictions
are different.

Remove TABs in some source code, replacing them with spaces

Use Emacs's conception of how many spaces the TAB was
representing (and the M-x untabify command).

This may not line up with the author's original conception, but then,
using TABs makes it impossible to tell just what the original
conception was in the first place anyway.

Should probably script this over all of repository (excluding
makefiles of course), and use standard expand or col utilities rather
than emacs.

Remove eqtype declaration for term type

Add selftest for COND_CONV

Fix test-case that depended on SML equality between non-atom terms

We have never guaranteed that terms with the same logical structure
should compare equal with SML equality. Variables and constants yes,
but others no. In particular, the explicit substitution machinery can
break this.

Update let pretty-printing to print let-chains in "list style"

The weird "and" syntax is still handled as before so that it is
possible to write

let x = y and y = x and z = y + 2 ; u = x * 10 in [x;y;z;u]

and have the x, y and z bindings refer to free occurrences of x and y.

Closes #154

Fix let-absyn post-processing

Tests and theories work up until pred_setTheory.

General list-form not yet right: parser now barfs on { x | y }.

Extract pretty-printing of LET-terms from term_pp.sml

It is now part of user-printer "land" in src/bool/boolpp.sml,
alongside the custom printer for if-then-else (COND).

This refactoring revealed a bug in the way overloaded constants
couldn't be handled by user-printers if they could have extra
arguments hanging off to the right (as in “LET f x y”), *unless* they
were overloaded to "case" (as in COND).

To make sure one's user-printer is going to work, you have to consult
the grammar's overload information to check if your term is one you
want to print according to the grammar_name function. Unfortunately,
looking for particular constants is not guaranteed to work, as the
process of descending terms in the pretty-printer is liable to turn
real constants into special "fake" constants that are actually
variables with special names.

This is progress with Github issue #154, to allow new (Isabelle-style)
syntax for let expressions.

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

Preserve add_user_printer properly in grammar data

This requires a slightly involved process for storing references to
code in theory files.

Update the .doc file on add_user_printer (which was already incredibly
long), and add a test.

Closes #367

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.

Unify handling of type abbrevs and type operators

This is analogous to what is done with terms, where the handling of
genuine constants passes through the overload map.

The main desirable effect should be that if multiple genuine type
operators with the same name are in the grammar, then only one will
print unqualified; all the others will print with theory-qualification.

Currently fails in src/datatype's selftest as ParseDatatype doesn't see
bare names that are existing types as possible occurrences of recursive
types.

Fix 2 more LVTermNet bugs

1. handling of function variables, supposedly improved by 3e5a7a35 was
broken if functions appeared before end of polish notation path
towards leaves
2. local-variable functions were not seen as such

More test cases to catch these bugs added.

Get LVTermNet tests to compile under Moscow ML

Fix matching error in LVTermNet code

Problem was that a pattern like ``R x`` (where R is a variable) didn't
match ``f a b``.

Closes #332

Thanks to Joseph Chan for the original bug report.

Fix over-aggressive normalisation in goal_assum

In particular, it's important that

P1 /\ P2 /\ ... Pn ==> F

stays as an implication and not turned into a negation.

Add test for expected behaviour with some instantiation provided by
mp_then.

Fix basic unification bug (add derived test-case)

Fix a bug in handling of case expressions

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

Find and fix a parsing bug in monad implementation

Fix EVERY_CONJ_CONV; add tests for EVERY_DISJ_CONV

Write more tests for EVERY_CONJ_CONV (one fails)

Make selftest output line up with parallel Holmake's

Also make tests use testutils.OK to report OK

Move match_goal selftests to boss

Enables writing tests depending on more stuff (including BasicProvers).

Add an initial implementation of match_goal

This is a tactic builder that does automatic logic-programming-style
search over (sub)terms in the assumptions and conclusion of a goal
ensuring certain patterns match and that a given tactic (which can refer
to the terms and assumptions named by the pattern) succeeds.

Work with Jack Gallagher, and inspired by a similar facility in Coq.

Fix src/1/selftest to hide temporary constants

Having a "c" around that is now a constant can mess with your parsing of
innocent seeming terms.

Fix bug in irule found by Jeremy.

Wasn't collapsing groups of assumptions together in terms of their
shared free variables correctly.

Fix irule to handle input thms with hyps better

As per selftests. Other possible differences will be in ordering of new
subgoal, and distribution of existentials over those subgoals.

Add two selftests for irule tactic.

Adjust documentation to make example correspond to what tactic actually
does.

Fix thm_to_string to use raw backend properly.

The term_to_string and type_to_string functions do this already.

Implement and document remove_type_abbrev.

Closes #148

Delete trailing whitespace in src/

test for VALIDATE in src/1/selftest

self-test for some list-tactics, eg ROTATE_LT, REVERSE_LT, SPLIT_LT

self-test for USE_SG_TAC and some other list-tactics

Make save_thm etc reject names that will cause uncompilable theory files

This causes exceptions/errors earlier rather than later.

Add regression test for issue #214

Make PP.avoid_unicode also work for bare constant names.

Previously, unicode infixes, suffixes were avoided, but if one did an
outright

overload_on("unicode-ish thing", ``constant``)

then PP.avoid_unicode wouldn't help.

Handle Unicode on Windows better with new PP.avoid_unicode trace

If the trace variable is true, then the pretty-printer strives to not
print Unicode characters. If it's false, then it obeys the grammar
(which encodes various printing preferences as well). The trace
is initialised to true on Windows systems.

Get src/1/selftest.sml to compile under Moscow ML again.

Change in 1ffe317 (new test-case for issue #172) broke compilation
because Moscow ML's handling of record types differs from Poly/ML's.

Test-case for github issue #172

The problem is that the pattern ``x: bool -> bool`` is matching
everything.

Fix minor bug in behaviour of EVERY_CONJ_CONV (with selftest)

Allow prefix-operators to be printed without parens in rand-position

This is a refinement to the decision in aeb0085a3d11, which insisted
that prefix operators (like if-then-else, binders, case-expressions
and others) should always get parentheses when printed as arguments to
functions.

Now you can tweak this by choosing the NotEvenIfRand parenthesis style
as an argument to add_rule. For particularly tight operators, ones
that may omit spaces before their arguments say, this may look better.
For example, you might define a "#" operator, when it might be nicer
to have

f #2 + g #n

print that way, rather than with extra parentheses. At the moment, our
standard number injection function & does print with parentheses, but
this case does feel like one where dispensing with the parentheses
might be a good idea.

Correct bug in type pretty-printer when unary op is "unknown"

The buggy behaviour would cause

minprint ``x: ('a -> 'b) option``

to print

x: ('a -> 'b option$option)

Improve pretty-printing of if-then-else. Closes #20

Include some regression tests.

Add some type pretty-printing selftests.

Change some regression tests to cope with bool_case = COND.

If you write `case x of T => 3 | F => 4`, it doesn’t print like that
any more; instead it will print as `if x then 3 else 4`. So old
test-cases that relied on the old behaviour failed.

So, the test-cases, which were all about pretty-printing of nested
case expressions (correct parenthesisation etc) are now about case
expressions over nums testing the same issue.

Fix a bug where REWRITE_TAC and friends with rewrite |- T could loop.

Fix a couple of selftest bugs arising from issue #13 hacks.

Allow case expressions to parse with leading bars. Closes #25.

New tests for regressions in case-expression pretty-printing.

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

Add test for DiskThms functionality.

This test also causes the current bug to do with dependency failures with mlyacc
stuff to exhibit.

Fix a pretty-printing bug to do with polymorphic constants.

Printing of w2w terms with show_types on works correctly. In fact, it
looks as if it was working correctly before, but the algorithm that
was achieving this was still utterly wrong. The accompanying
self-test demonstrates an instance that the old algorithm got wrong.

Two more printing tests for parens around prefixes.

Add (failing) test for insertion of parens to args with prefix-forms.

Failing test; edit grammar to change break behaviour and see no change.

Failing tests for base printing of dollared escapes.

Turns out last checkin was just a documentation bug

Add test for a new INST_TYPE bug

This bug is not yet fixed.
Please forgive me if it's not actually a bug... at least the Docfile for
INST_TYPE should change if this is expected behaviour.

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