Fix pretty-printing: list-syntax for SX_CONS should take precedence

Just as with list-syntax for CONS (see 70e6ee11), this now needs to be
done by having the list-rule come after the rule for the binary
operator to pick up a later timestamp, and thus be preferred.

Avoid ARB in simpleSexp grammar and parser

Location in parser done (up to a cheat)

Change monadsyntax to NOT change global grammar on load

Instead, users must explicitly call {temp_,}add_monadsyntax to turn do
.. od and the <- syntax on, along with the pretty-printing and
augmented parsing.

Prove string case of peg_eval_print_sexp

Needed to augment valid_sexp to restrict strings to printable
characters. Also did some a bit of work on the final (hardest) case of
the lemma.

I think a symbol should not start with a . or a "

It would probably be possible to allow symbols starting with ".", but is
it worth the effort?

Also, I noticed a discrepancy with my understanding of sexps:
(this is a dotted . list) is not allowed, but I think it should be
(representing (this . (is . (a . (dotted . list)))))

define valid_sexp

the only restriction is on symbols (hopefully that's enough for parsing
back what's printed)

fix sexpPEG so it is wfG (and still passes tests)

rather ugly peg expression for sexpnum, but seems hard to avoid

sxMEM_sizelt (moved from CakeML)

playground for formal language theory developments.