Update src for strip_binop change

Fix a bug where 'paranoid string printing' caused bad prints of \n

Add single guillemets ‹...› as delimiters to string-literal o/loads

Do pretty-printing for different string literal forms

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

Rework handling of string literals

Can now do the parsing side of github issue #510, allowing string
literals to be invisibly injected into other types, just as numbers
are. Add to this feature with the ability to use the «...» delimiters
as a separate flavour of string (with the underlying term being the
application of an injection function to a "normal" string literal).

Pretty-printing still needs to be done.

Allow matching over integer literals.

Changes the mechanism for supporting new literals.

Fix for issue #126.

Bug-fix: exported xTheory.sig files could contain spurious 'comments'.

In particular, if a comment-string (i.e., (* or *)) appeared as part
of a string literal in an exported theorem, this caused the resulting
Theory.sig file to be malformed SML. The fix was to create a trace
variable allowing string-literal printing to become more 'paranoid'
when done in the TheoryPP code. In that context, occurrences of the
bad strings have their asterisks replaced by \042, which is correct
SML/HOL notation for ASCII character 42, which is the asterisk.

Note that this problem doesn't arise in normal interactive use: the
HOL lexer doesn't get confused by comment strings in string literals,
and the SML level thinks all of the content in a quotation is inside
one of its own string literals.

Include a comment in the Description manual about not using tokens
that include comment strings or whitespace.

Thanks to Magnus for the bug report.

Recast strings as lists of characters. The type :string is now an
alias for :char list. The old constant names (STRCAT, STRLEN, STRING,
EMPTYSTRING) are retained, but they are now just parsing/printing
forms for (APPEND, LENGTH, CONS and NIL). String literals still work.
For the moment, the string names are also preferred when printing,
though I think there's a case for just printing with the list names.
(Of course, the list names are used when the arguments are not of type
:char list.)

Made notion of literal extensible. This allows
word literals to be used in pattern-matching,
as is done in Anthony's ARM stuff.

This check-in mainly fixes a problem with
literals occurring in patterns of TFL-style
definitions. There are a host of other minor
changes as well.

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

Committing in .

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

Adding changes to support literals in patterns.

It now works for Functional.mk_functional, for parsing in ``...``,
and for output by the prettyprinter.

I have also added a new function, Functional.mk_pattern_fn, which
takes a list of (pattern,expression) pairs and creates a function
using a nested case term to branch among the various patterns.

Try

- ``(checkPrefix : 'a list # 'a list -> 'a list option)
((subl :'a list),(supl :'a list)) =
case (subl,supl) of
(([] :'a list),(v3 :'a list)) -> SOME supl
|| ((subhd :'a)::(subtl :'a list),([] :'a list)) ->
(NONE :'a list option)
|| (subhd::subtl,(suphd :'a)::(suptl :'a list)) ->
(if subhd = suphd then
checkPrefix (subtl,suptl)
else
(NONE :'a list option))``;
> val it =
``checkPrefix (subl,supl) =
case (subl,supl) of
([],v3) -> SOME supl
|| (subhd::subtl,[]) -> NONE
|| (subhd::subtl,suphd::suptl) ->
(if subhd = suphd then checkPrefix (subtl,suptl) else NONE)`` : term

or try

- load "stringTheory";
> val it = () : unit
- ``case z of (2,g,_a) -> STRLEN g
|| (_n,"",x) -> 5
|| (s,"super",[1]) -> 7
|| _ -> 2``;
> val it =
``case z of
(2,"",v11) -> STRLEN ""
|| (2,"super",[]) -> STRLEN "super"
|| (2,"super",[1]) -> STRLEN "super"
|| (2,"super",1::v31::v32) -> STRLEN "super"
|| (2,"super",v21::v22) -> STRLEN "super"
|| (2,g,v11) -> STRLEN g
|| (s,"",x) -> 5
|| (s,"super",[]) -> 2
|| (s,"super",[1]) -> 7
|| (s,"super",1::v52::v53) -> 2
|| (s,"super",v44::v45) -> 2
|| (s,v35,x) -> 2`` : term

Peter

Changes having to do with generating ML. System should build again.

*** empty log message ***

If, as the netsem project wants to, you want to have string terms that
are 150000 characters long, then there all sorts of places in the
parsing code where your stack blows up. This is just the first such place.
Anyway, making this one tail-recursive is easy. There are a number
of other non-tail-recursive functions in Preterm that will be fiddlier
to fix.

Upgrading EmitML to support records. Lots of associated changes
as well.

Implement a new pretty-printing/parsing notation for character literals.
Use the SML notation for this. For example, #"f", and #"\"". This notation
was easy to implement because lexing could piggy-back on the handling
of strings. I also think that compatibility with SML is a good thing.
Changing the notation should be easy enough if we do decide to do this.
Pulled the character pretty-printer out of stringSyntax as well.

Changed NUMERAL_BIT1 and NUMERAL_BIT2 to BIT1 and BIT2, respectively.
Sorry, they were just too long. Also, ALT_ZERO is now named ZERO.

Minor changes.

Simplified some proofs in MachineTransitionScript.

Reverted to Taupo-6 RW_TAC. This should make RW_TAC faster, and a little
less eager to case-split conditionals. Some proofs may break as a result.
In that case, use the drop-in replacement BasicProvers.NORM_TAC.

Term destructors now operate using same_const to check the operator
of the term being destructed. This may increase efficiency somewhat.
There were consequent changes to the xSyntax modules of the system.

Fixes to building strings (the char type is in stringTheory).

Fixing problem with prettyprinting the empty string.

Minor change.....

Added support for string literals to Numeral and changed its name.