Make grammar-deltas s-expressions when stored in theory .dat files

This makes them more legible, and is also a prelude to being more
uniform in the treatment of theory data that merges deltas across
ancestors.

Implement a remove_strliteral_form

This undoes the effect of add_strliteral_form. With test cases and a
nod in the direction of documentation.

Closes #778

Do pretty-printing for different string literal forms

Entrypoint is Parse.add_strliteral_form, which needs documentation.
But this otherwise completes issue #510.

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

functions to print terms without using overloads

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

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

Get tracked user_deltas to build grammars in Theory files

Record overload_on calls in GrammarDeltas

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

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.

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

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.

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.

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.

Remove a misleading comment.

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

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.

hanges to upgrade EVAL on BIGUNION {}.



M src/parse/term_grammar.sig
M src/pred_set/src/pred_setScript.sml
M src/pred_set/src/pred_setLib.sml
M src/pred_set/src/PFset_conv.sml

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.

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.

Modifications to implement parsing and printing of case expressions.

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.

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 bring about Kananaskis parser. Known bug exists in
treatment of qualified identifiers.

Slew of changes to get rid of local open in end in signature files, and
one or two other fixes to make source mosml2.00 compatible. Also added
ability to set and get term_printer function, as per request by Peter
Homeier.

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

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.

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.

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.

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