Add black-box quotation preprocessor

[strub]

Introduce {% name body %} quotations, expanded during lexing by an external
tool over stdin/stdout. A quotation expands to a sentence fragment that is
spliced into the surrounding sentence, so it may replace only part of a
sentence (and several may appear in one). The terminating '.' is always
written by the user. Locations in the expansion are remapped back to the
original source, so errors point at the original quoted text.

Usage
Write a quotation as {% name body %}, where name selects a handler and
body is arbitrary text (the {% %} delimiters nest). The expansion is a
fragment, so the surrounding sentence and its '.' are written outside the
quotation:

op forty_two = {% calc 6 * 7 %}.

Quotations compose with ordinary source and with each other in one
sentence:

op mixed = {% calc 6 * 7 %} + ({% calc 2 + 3 %} * 10).

Enabling quotations
Quotations run external programs, so the feature is OFF by default and a
quotation encountered while it is off is a hard error (never a silent skip
or a silent execution). Enable it for a run in one of two ways:

easycrypt -enable-quotations compile foo.ec
EC_ENABLE_QUOTATIONS=1 easycrypt compile foo.ec

It cannot be enabled from easycrypt.project, which ships inside a
checked-out tree -- letting it turn the feature on would defeat the
safeguard. Only enable quotations for sources you trust.

Binding handlers
Once enabled, a name is resolved to a shell command in order: a
'quote = name:command' entry in the [general] section of easycrypt.project
(relative paths resolved against the project directory); then
EC_QUOTE_; then EC_QUOTE_CMD; then an executable handlers/
(also .py/.sh) next to the source file.

Handler protocol
The handler reads the body (after a header line) on stdin and writes a
single JSON object on stdout: { "expanded": , "segments": [...] },
where segments is the source map used for error-location remapping. A
non-zero exit reports an error at the quotation.

See doc/quotations.rst for the full reference.

[alleystoughton]

What's the way to enable quotations when running in Emacs/Proof General?

What's the significance of the kind field in the JSON?

[alleystoughton]

I may be missing something obvious, but when debugging, one wants to see the output of the handler without EC running it. How does one do that?

[alleystoughton]

What's the way to enable quotations when running in Emacs/Proof General?

(defun easycrypt-toggle-enable-quotations ()
  "Toggle enabling quotations in easycrypt mode"
  (interactive)
  (if (member "-enable-quotations" easycrypt-prog-args)
      (progn
        (setq easycrypt-prog-args
              (remove "-enable-quotations" easycrypt-prog-args))
        (message "quotations disabled"))
    (setq easycrypt-prog-args
          (append easycrypt-prog-args (list "-enable-quotations")))
    (message "quotations enabled")))

[strub]

What's the significance of the kind field in the JSON?

Documentation has been updated.

[alleystoughton]

Two things:

(1) If one puts a "." in the middle of a quotation, this works as expected in batch mode. But with Proof General, the region up to the "." is highlighted, and easycrypt or Emacs (?) hangs. I'm not sure if this is a syntax table issue with Proof General. Any ideas what's going on? It seems it would be OK to prohibit this, but when I change the lexer to do that, things still hang in Proof General (but it works fine in batch mode).

(2) Given that a sentence can have multiple quotations, I'm struggling to see how a debugging mode for quotations can be implemented - in which the output of the quotation is printed in the response buffer. Any ideas/suggestions?

[alleystoughton]

Two things:

(1) If one puts a "." in the middle of a quotation, this works as expected in batch mode. But with Proof General, the region up to the "." is highlighted, and easycrypt or Emacs (?) hangs. I'm not sure if this is a syntax table issue with Proof General. Any ideas what's going on? It seems it would be OK to prohibit this, but when I change the lexer to do that, things still hang in Proof General (but it works fine in batch mode).

The reason for the "hanging" is that the Proof General prompt isn't being issued. With the existing code, we get in the *easycrypt* buffer

[1|check]>
op forty_two = {% calc 6 * 7 .

and no subsequent prompt. If I change the lexer to make a "." followed by whitespace illegal in a quotation, we get

[1|check]>
op forty_two = {% calc 6 * 7 .
[error-29-31]parse error: sentence termination in quotation

[alleystoughton]

If I understand the function expand_quotation correctly, it doesn't allow the expansion of a quotation to have multiple sentences. But this is precisely what the m4 macros I use do do. Is there a reason for this limitation? To be useful to me, I'll need to remove it.

[alleystoughton]

Two things:

(1) If one puts a "." in the middle of a quotation, this works as expected in batch mode. But with Proof General, the region up to the "." is highlighted, and easycrypt or Emacs (?) hangs. I'm not sure if this is a syntax table issue with Proof General. Any ideas what's going on? It seems it would be OK to prohibit this, but when I change the lexer to do that, things still hang in Proof General (but it works fine in batch mode).

I fixed this on branch quotation-preprocessor-alt.

[alleystoughton]

(2) Given that a sentence can have multiple quotations, I'm struggling to see how a debugging mode for quotations can be implemented - in which the output of the quotation is printed in the response buffer. Any ideas/suggestions?

On quotation-preprocessor-alt, added debugging mode: {%* ... %}, which prints the quotation's handler, body and expansion (in Proof General, this will go in the response buffer).