Implement Haskell-style $ as infix function application operator

With documentation and some simple test cases.

Improve pretty-printing of (term) grammars

Complete implementation of new API for declaring+using monads

Monadsyntax in general (the do..od notation) can be turned on and off.
In addition, specific monad instances can be declared and subsequently
enabled by just calling something like

monadsyntax.enable_monad "option"

Having state_transformerTheory as an ancestor turns on monadsyntax, and
enables the state monad. (Enabling a monad causes a bunch of calls to
overload to occur; disabling a monad undoes those calls.)

Fix pretty-printing of list-forms

Issue was that pretty-printing blocks need to be around the list
delimiters (and included elements), not around just the elements with
the delimiters outermost. The block_info field of the listspec
constructor is now ignored when these are printed; instead the binfo
is lifted (by term_grammar.add_listform) to the rule in which the
listspec appears.

Closes #529

Now up to PPBackEnd.sml (term_grammar.sml done)

functions to print terms without using overloads

Add type annotation to record parameter to get code past Moscow ML

The standard is unfortunately vague about what is and isn't required
on this front.

Closes #453

Handle infix cons-operators (like pred_set$INSERT) better

Still can't get past the self-test in src/pred_set/src

Term-grammars now maintain their own max-timestamp so that successive
rules' timestamps are guaranteed to increase. (Previously, the new
timestamp just got made bigger than the timestamps associated with
"related" grammar rules. This required a scan of all the grammar's
rules, and a careful definition of what it was to be related.)

Parsing of lets (even with ;'s) works; absyn post-processing doesn't

src/parse compiles but parser broken.

Completed change to remove LISTRULE form from grammar. Instead, all
list syntax is handled with embedded ListForms within normal rules.

WIP for change to list syntax handling.

Very broken at the moment

Use grammar-deltas for user-provided absyn post-processors

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.

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

Ensure Unicode lambda is in grammars from min onwards

Fixes bug identified in 7cfe487

Handle clear_overloads_on with user-deltas

Make 'remove-rules-with-tok' a user-delta

Provide "remove tok" update for term grammars

This one removes "all" rules that involve the given tok (except: the
behaviour with respect to list rules mimics what the remove_termtok
function does, and only looks at the first token of the various
components; this is probably something that can change).

Convert type-grammars to use deltas for updates

This is very much analogous to what has been done for term grammars.

Handle add_numeral_form et al with user-deltas

Also take the opportunity to remove redundant add_actual_overloading
entrypoint in Overload module.

Add deltas for moving overload operations

Sadly, making an inferior overload is not *quite* the same as making a
normal one, then then moving it "to the back", so I've left both
operations in the user_delta type for the moment.

Handle gen_remove_ovl_mapping

This gets tests as far as string_numTheory

Get tracked user_deltas to build grammars in Theory files

Begin process to use GrammarDeltas inside theories

This doesn't work yet (just attempting to load boolTheory leads to an
exception), but it's close to working, at least for some situations. I'm
generating new constructors for the user_delta type more or less as the
errors prompt me to.

The new constructors in this commit are IOVERLOAD_ON for "add inferior
overload on" (it's not really clear that this is used enough to warrant
inclusion, but hey); ASSOC_RESTR for "associate restriction", which is
used in boolTheory and probably nowhere else ever, and RMOVMAP for
"remove overload mapping", which is used to remove overloadings to
constants.

General pattern in Parse is to generate the user_delta values, and to
then feed these to the term_grammar.add_delta function to make the
grammar updates. This makes Parse simpler on the whole, which is
definitely an improvement.

Record overload_on calls in GrammarDeltas

Add 2 rule-removal constructors to user_delta type

These will help with concretisation of grammar changes in theory files.

Remove BRULE constructor from user_delta type

It is redundant, though the GRULE representation of a grammar's binder
rule contains information that is never used.

Properly re-org grammar code, removing rule_fixity

Now there is just one fixity type. Also decide that set_fixity and
set_mapped_fixity shouldn't be in the grammar-delta type; instead the
"remove-termtok" and "add_rule" actions (which can be used to implement
the above) should be.

Refactor more grammar code

Ultimate is to switch to concrete "grammar-deltas" in theory files
rather than calls to the update_grms function. Start this process by
extending existing delta type with SET_MAPPED_FIXITY constructor. This
is not yet used.

Move grammar code, mostly simplifying term_grammar

Most significant change sees some code in term_grammar that is only
useful in the concrete syntax parser move to parse_term. Add a _dtype
structure for the latter's public datatypes as well.

Refactor grammar datatypes into separate struct

This removes duplicated datatype declarations

Update to new FunctionalRecordUpdate tech

This is from the mlton.org (as per URL in checked-in file). Also move
the source file to the Holmake directory so that I can use it there. The
Holmakefile in src/portableML then copies it from that location into
position so that it properly ends up in sigobj etc.

This version of the file supposedly compiles faster, and it also seems
to handle polymorphic fields.

Provide p/printer for rules part of a term grammar

Closes #249

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.

Update to better FunctionalRecordUpdate

This one has better compile times.

Allow multiple case-like constants in a grammar

Parsing handled; printing still not quite right

Absyn post-processors now see the current grammar

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

Fix errors in b3de5020; add fupd for pmatch_on

Add flag to term grammars saying if to use PMATCH

The reinstatement of opaque type ascriptions seems to have been skipped in the previous merges.

More opaque type ascriptions

Adaptations in preparation for the release of Poly/ML 5.6.

Note that HOL4 now relies on PolyML.addPrettyPrinter and PolyML.Compiler.compilerVersionNumber, which came with Poly/ML version 5.3.

Adaptations in preparation for the release of Poly/ML 5.6.

Note that HOL4 now relies on PolyML.addPrettyPrinter and PolyML.Compiler.compilerVersionNumber, which came with Poly/ML version 5.3.

Allow pretty-printing backends to modify grammar

If you know that you are targetting a particular backend, you may wish
to also modify the grammars that control pretty-printing.

For the moment, just use the identity update in all our backends, so
that nothing changes in terms of what the user sees.

first_tok: error message improved; unused code removed

Fix a horrid bug in removing rules from grammars.

Sense of a test was inverted when working over a grammar's binders.

Pretty-printer now annotates consts with their real names and types.

In "complicated" overload situations, such as the overloads for NOTIN
and <>, the annotation can't point to a "real" underlying constant,
but does still provide the type for the emacs tool-tips.

In passing, also create a new annotation form, the SymConst as well as
the Const. This is done for the TeX backend's benefit, so that it can
avoid treating things like + the same as normal identifiers. This
works well for math-mode munging where you want "+" to map to $+$, but
want "INSERT" to map to \textsf{INSERT}.

Closes #39

Allow case-constant printing to be overridden by user overloads.

For the if-then-else case, the specially installed user-printer code
from ParseExtras needs to be adjusted.

Closes #206

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.

informational function in Parse: print the term grammar rules

The existing term_grammar() returns the grammar which is pretty printed
by showing the rules, the known constants, and overloading info.
Sometimes this is too much information. So the new print_term_grammar()
just pretty prints the rules (and returns unit). This is useful
especially to see infix and precedence information.

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Fix bug of previous commit; compare with all fields of a grammar rule.

Fix pretty-printing of grammars with multiple custom printers.

Rework grammar infrastructure, losing 'preference' for concrete syntax.

Instead, the most recent rule is the one the pretty-printer will prefer.
The clear_prefs function disappears, but the prefer_form function stays
because it can just adjust the timestamp on the desired form to be most
recent.

Bugfix: unsetting Unicode trace wasn't correctly removing all Unicode rules.

Move theory min's grammars into {type,term}_grammar (out of Parse).

Add encoder and reader for grammar rules.

Also add some more entrypoints from optmonad to Coding.sig.

Make the interface supported by Unicode slightly richer so that I can
make the Unicode not-equals not overlap entirely with <>, thereby
allowing <> to be used both for word_slice and for not-equals, without
it inheriting the \neq symbol when Unicode is on.

Change & (the overloaded injection function from natural numbers into
other numeric types), to be a prefix symbol in the grammar. This
allows things like -&n to pretty-print better. There are a few
breakages here and there. I realise that the type-annotation suffix
should be looser than &'s precedence level so that &n:int parses as
(&n):int rather than &(n:int). Changing this revealed some faults in
the handling of operators like unary minus, so the construction of the
precedence matrix in term_parse needed to change a little. Changes to
later files and theories were mainly caused by people writing ``&``;
you now need to write ``$&``, or ``(&)``.

Concrete syntax can be such a pain. Anthony has pointed out that we
need to be able to parse both

r with fld := value

and

r with <| ... ; fld := subrcd with subfld := subvalue |>

Both of these seem as if the forms above should be accepted. This
requires "with" and ":=" (and their unpopular friend "updated_by"), to
all be at the same level and right-associative. I've put them at 460,
making them looser than the loosest value operator, which is
left-associated ++ (at 480). This ensures that

fld := x ++ y

parses correctly.

Fix for record parsing bug spotted by Anthony: the "with" and ":="
infixes used to live at same right-associated level, making the
standard idiom of `r with fld := value` associate correctly. Now that
450 is non-associative, this fails. Move "with" to level 445 and keep
it non-associative.

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

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.

Update the handling of binders so that different concrete syntax forms
can map to the same abstract syntax form. This makes binders more
similar to other forms. For example, the if-then-else and =>-|
concrete forms might both map to the underlying name "COND". Now,
with Unicode enabled, the Unicode universal quantifier as well as "!"
can both map to the name "!". (Internally, there is a preferred flag
set, so that the pretty-printer knows which should be printed when it
comes to the term "!".)

This couldn't be done before, so for example the Unicode universal
quantifier mapped to itself, and this name was then overloaded to be
an alias for "!". This use of the overloading level for Unicode led
to some problems, and was inconsistent with the approach taken for the
other symbols.

There are some other tidy-ups now that binders are more like other
forms.

Modify the ability to add user-printers so that they're keyed off
term-matches (using first order term-matching). Also give the user's
function access to the relevant grammars, and to the "smart"
add_string and add_break functions that the system printer uses itself
to avoid symbol merging.

A stepping stone on the way to allowing arbitrary abstract syntax
post-processing to be added to user parsers in a straightforward way.
Also add the useful FunctionalRecordUpdate code from mlton.org to
portableML.

Another fix to the way Unicode-overloading works. It now checks to
see if the term you are overloading to has an ASCII concrete syntax.
(For example, integer$int_le has an ASCII concrete syntax of <= as an
infix.) If so, it will set up the Unicode symbol as an alias for that
concrete syntax. This means that subsequent overloads on the same
ASCII symbol will also pick up the Unicode symbol.

Graphically, we have something like



x <= y +----- arithmetic$<=
\ |
>---> COMB(COMB(<=,x),y) >---+----- integer$int_le
/ |
x ≤ y +----- words$word_le
|
... etc

where the middle column is the result of Absyn applied to the given
quotation.

Remove more Polyhash occurrences.

Extend the add_listform interface so that the user can specify a printing
"consistency" for the block of list elements. Previously, it was just
assumed that the user always wanted (INCONSISTENT,0). This is the value
now specified in the various places where add_listform is used.

Adapting to new Basis (and SML/NJ).

Open up the grammar interface, so that users can modify the "specials"
component of the grammar. This then allows them to change the magic
tokens that stand for lambda abstraction (\), the symbol that introduces
type annotations (:), the symbol used to mark the end of a variable binding
sequence (.), the restricted quantifiers (this is already accessible
through the API), and the restricted quantifier token (::).

To parse/print with a grammar, use functions in Parse such as
temp_set_grammars
parse_from_grammars
print_from_grammars
print_term_by_grammar

Modify the add_listform function in line with a suggestion of Lockwood
Morris's to provide slightly more flexibility in the way that list forms
are pretty-printed. Previously, the format was fixed as
<left-delimiter> el1 <sep> <a space> el2 <sep> <a space> ...
Now, the spacing is more directly under user-control.

Changes to parsing technology to allow left-associated infixes to
co-exist with function application in the same slot in the grammar.
Application of this new facility to the example of FAPPLY in finite_map
theory. Might also be useful if and when we get round to modelling sets
as functions in pred_set theory.

Another change to the precedence of the record update lexemes (with and :=).
There is method to the madness, honest. In particular, these operators
now live between the logical operators (=, /\, \/, ==>) and the
"value-constructing operators" of theories like arithmetic etc.

Made the record infixes (with, := and updated_by) of tighter precedence.
In particular, made them tighter than pairing (,). It was stupid that
(p, x with ...) was being parsed as (p,x) with ...

Modifications to implement parsing and printing of case expressions.

Added a pretty-printer for type grammars and extended the term grammar
to note the existence of user pretty-printers.

Added ability for users to add their own pretty-printers, tied to the type
of the term being printed out.

Cleaned up treatment of overloading and extended pretty-printer to
show types verbosely, when appropriate.

Overload.sml now uses a Binarymap internally to store the map from
names to sets of constants. A slight change to Overload.sig affected
only term_grammar's internals, and only the grammar pretty-printer
at that.

Changed pretty-printing of grammars so that overloading to constants
where the name for that constant is shared among more than one is made
clearer.

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

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.

Fixed a couple of grammar modification operation bugs. One was that
if a LISTRULE constructor came to have an empty list as argument, it
wasn't purged from the grammar, and the other was that LISTRULEs
weren't considered by remove_form (in turn called by
Parse.remove_rules_for_term).

Improved pretty-printing of grammars.

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

Adjusted string form of <end of string> to be <end of input> after comments
from Mike to the effect that he would find this less confusing.

Implemented pretty-printing for grammars. In order to allow for this
to be installed as a pretty-printer for all values of this type, made
grammar implementation a datatype; this change invisible externally.

Fixed a couple of bugs in grammar merging. Binder lists were being
appended, not union-ed, and the treatment of closefix and listrule rules
was completely wrong.

Changes to support the proper construction and export of theory grammar
values. Theory export now takes an extra parameter, which is a string
that will be pre-pended to the Theory.sml file. This allows me to
remove code in TheoryPP that was rather specific to what was being
done in Parse. Now, this code can remain ignorant of that level of the
system, as should be the case.

Implemented new operation of grammar merging. This will be used
to deal with the dodgy implementation of internal grammar value
calculation done in theories.

Concrete syntax for records now very close to done. Thanks to Mark Staples
for suggesting that records with singleton updates could be done without
the brackets around the lists, thus: r with fld1 := 10.

Quite radical changes which allow for "." to be used as the record
field selection operator. Lexer has changed quite dramatically:
it is no longer responsible for determining whether or not a token
is a "keyword" or not. Instead this is done at the parsing level.

The lexer is also now unable to cope with identifiers that are a mix
of alphabetically acceptable and symbolically acceptable characters.

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.

Record field selection implemented as far as parsing and pretty-printing are
concerned.

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

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

Implementation of new pretty-printing support whereby grammar rules now
contain extra information on how various forms are to be printed, with
extra information specifying spacing, block structure and when things
should be parenthesised, even if not strictly necessary.

Changes necessary to make :: an infix operator representing CONS as well
as the restricted quantification operator. This change has required some
changes to the basic design of the parser; it's now not possible to have
more than one res. quan. operator.

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.

Made changes to allow slightly better feedback on a term_grammar error,
and also changed the construction of the precedence matrix to allow
equality relations to simply overwrite others without causing an error.
This allows { | } (set comprehension) to co-exist with the old style
conditional expression.

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