Add black-box quotation preprocessor

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_<NAME>; then EC_QUOTE_CMD; then an executable handlers/<name>
  (also .py/.sh) next to the source file.

Handler protocol
  The handler reads the body (after a header line) on stdin and writes the
  expanded source, a form-feed, and a JSON source map on stdout; a non-zero
  exit reports an error at the quotation.

  See doc/quotations.rst for the full reference.

Author: strub

Makefile

@@ -43,7 +43,7 @@ uninstall:
 	$(DUNE) uninstall
 
 unit: build
-	$(CHECK) unit
+	$(CHECK) unit quotations-disabled
 
 stdlib: build
 	$(CHECK) prelude stdlib

config/tests.config

@@ -14,4 +14,11 @@ exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomple
 okdirs = examples/MEE-CBC
 
 [test-unit]
-okdirs = tests tests/exception
+args   = -enable-quotations
+okdirs = tests tests/exception tests/quotations tests/quotations-project
+
+# Quotations are disabled by default (they run external programs); a file
+# using one must fail when -enable-quotations is NOT given.  This scenario
+# deliberately omits the flag.
+[test-quotations-disabled]
+kodirs = tests/quotations-disabled

doc/index.rst

@@ -5,3 +5,4 @@ EasyCrypt reference manual
    :maxdepth: 2
 
    tactics
+   quotations

doc/quotations.rst

@@ -0,0 +1,197 @@
+========================================================================
+Quotations (external preprocessor)
+========================================================================
+
+A *quotation* lets you embed, directly in an EasyCrypt source file, a
+fragment written in some other surface syntax, and have EasyCrypt expand it
+into ordinary EasyCrypt code by delegating to an **external tool**. The tool
+is a black box: EasyCrypt communicates with it over standard input and
+standard output, so it can be written in any language.
+
+.. warning::
+
+   Quotations run external programs, so the feature is **disabled by
+   default**. Enable it explicitly with the command-line flag
+   ``-enable-quotations`` or the environment variable
+   ``EC_ENABLE_QUOTATIONS=1``. It cannot be enabled from ``easycrypt.project``
+   (that file ships inside a checked-out tree, so allowing it to turn the
+   feature on would defeat the safeguard). While disabled, encountering a
+   quotation is a hard error, never a silent skip or a silent execution. Only
+   enable quotations for sources you trust.
+
+Quotations are processed during lexing, before parsing. A quotation expands
+to a **sentence fragment**: its tokens are spliced into the surrounding
+sentence, so a quotation may stand for only *part* of a sentence and several
+quotations may appear in one sentence. The sentence terminator (``.``) is
+always written by the user and never produced by a quotation. When the
+external tool — or EasyCrypt's handling of its output — produces an error, the
+location reported by EasyCrypt is mapped back to the **original** quoted text,
+not to the generated code.
+
+------------------------------------------------------------------------
+Syntax
+------------------------------------------------------------------------
+
+A quotation is delimited by ``{%`` and ``%}``:
+
+.. admonition:: Syntax
+
+  ``{% {name} {body} %}``
+
+Here:
+
+- ``{name}`` is a lowercase identifier selecting which external *handler*
+  expands the quotation (see `Configuring handlers`_).
+
+- ``{body}`` is arbitrary text. It runs from the character following
+  ``{name}`` up to the matching ``%}``. The delimiters nest: a ``{% ... %}``
+  pair occurring inside the body is kept verbatim and does not close the
+  outer quotation, so a body may itself contain quotation delimiters.
+
+A quotation expands to a sentence *fragment*, so the ``.`` that ends the
+sentence is written outside the quotation. For example, a ``calc`` handler
+that returns the value of an arithmetic expression::
+
+    op forty_two = {% calc 6 * 7 %}.
+
+expands to ``op forty_two = 42.``. Because the expansion is only a fragment,
+quotations compose with ordinary source and with each other within one
+sentence::
+
+    op mixed = {% calc 6 * 7 %} + ({% calc 2 + 3 %} * 10).
+
+It is an error for a quotation's expansion to contain a sentence terminator
+(``.``): the fragment must not close the sentence itself.
+
+------------------------------------------------------------------------
+Configuring handlers
+------------------------------------------------------------------------
+
+A quotation ``name`` is resolved to a shell command in this order:
+
+- a binding in ``easycrypt.project`` (see below);
+
+- ``EC_QUOTE_<NAME>`` — where ``<NAME>`` is ``name`` uppercased — gives the
+  command for that specific quotation name;
+
+- ``EC_QUOTE_CMD`` — a fallback command used for any quotation whose specific
+  variable is unset;
+
+- otherwise, an executable ``handlers/<name>`` (also tried with the ``.py``
+  and ``.sh`` extensions) sitting next to the source file. This lets a
+  directory of files be self-contained, needing no environment to set up — it
+  is how the test suite binds its handlers.
+
+The recommended way is the project file. In the ``[general]`` section of
+``easycrypt.project``, add one repeatable ``quote`` entry per handler, of the
+form ``name:command``::
+
+  [general]
+  quote = calc:handlers/calc.py
+  quote = verbatim:python3 tools/verbatim.py
+
+The ``command`` is a shell command (so it may include an interpreter and
+arguments). When it is, verbatim, a relative path to an existing file, it is
+resolved against the directory containing ``easycrypt.project``; otherwise it
+is passed to the shell unchanged. Project-file bindings take precedence over
+the environment, so the committed configuration is authoritative.
+
+To bind a quotation ad hoc through the environment instead::
+
+  export EC_QUOTE_CALC=/path/to/calc-handler
+
+A quotation whose name resolves to no command raises an error located at the
+quotation.
+
+------------------------------------------------------------------------
+The handler protocol
+------------------------------------------------------------------------
+
+For each quotation, EasyCrypt launches the bound command, writes a request to
+its standard input, and reads the expansion from its standard output.
+
+Request (sent by EasyCrypt)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+A single header line, followed by the raw body::
+
+  #ec-quote v1 name=<name> file=<orig-file> line=<L> col=<C> off=<O>
+  <body bytes...>
+
+where ``line``/``col`` are the 1-based line and 0-based column of the body's
+first character in the original file, and ``off`` is its absolute character
+offset.
+
+Response (returned by the handler)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The expanded EasyCrypt source, then a form-feed byte (``\f``, ``0x0C``), then
+a JSON *source map*::
+
+  <expanded EasyCrypt source>
+  \f
+  { "segments": [ { "out": [ob, oe], "in": [ib, ie], "kind": "verbatim" },
+                  ... ] }
+
+Each segment maps a half-open character range ``[ob, oe)`` of the **output**
+back to a range ``[ib, ie)`` of the **body** (offsets relative to the start of
+each, the body being the handler's own stdin payload):
+
+- ``"kind": "verbatim"`` — the output range is a character-for-character copy
+  of the input range (``oe - ob == ie - ib``); reverse mapping is
+  column-precise.
+
+- ``"kind": "synthesized"`` — the output range was generated by the handler
+  and has no one-to-one origin; the whole output range is attributed to the
+  whole input range, so an error there points at the responsible region of
+  the body rather than at a misleading column.
+
+If the response contains no source-map section, the entire expansion is
+attributed to the entire quotation (coarse mapping).
+
+Errors
+~~~~~~
+
+A handler that exits with a non-zero status makes EasyCrypt raise an error
+located at the quotation, using the handler's standard-error output as the
+message.
+
+------------------------------------------------------------------------
+Location mapping
+------------------------------------------------------------------------
+
+Because the expanded code is lexed and parsed in a separate buffer, the
+positions EasyCrypt computes for it would, naively, refer to the generated
+text. Using the source map and the body's original offset, EasyCrypt rewrites
+those positions so that **every** location it reports — parse errors, type
+errors, and printed locations alike — refers to the original source file.
+
+For a ``verbatim`` segment this is exact down to the column; for a
+``synthesized`` segment the location collapses to the originating region of
+the body.
+
+------------------------------------------------------------------------
+Examples
+------------------------------------------------------------------------
+
+A ``calc`` handler that evaluates an integer expression returns the resulting
+literal as a fragment, so::
+
+  op forty_two = {% calc 6 * 7 %}.
+
+expands to ``op forty_two = 42.``.
+
+A ``verbatim`` handler that copies its body through with a single ``verbatim``
+segment lets EasyCrypt point at the exact original character on error. Given::
+
+  {% verbatim op broken : int = no_such_op + 1 %}.
+
+EasyCrypt reports the unknown-identifier error at the column of ``no_such_op``
+inside the quotation, even though that identifier sits at a different offset in
+the generated buffer.
+
+.. note::
+
+   The result of expanding a quotation is stored in the compiled ``.eco``
+   file. When iterating on a handler, remove the stale ``.eco`` so the
+   quotation is expanded afresh.

src/ec.ml

@@ -398,6 +398,14 @@ let main () =
       ldropts.ldro_idirs;
   end;
 
+  (* Quotations: enabled only via CLI/env (never easycrypt.project), and the
+     handlers declared in easycrypt.project are registered only then. *)
+  EcQuotation.set_enabled options.o_options.o_enable_quotes;
+  if options.o_options.o_enable_quotes then
+    List.iter
+      (fun (name, command) -> EcQuotation.register ~name ~command)
+      ldropts.ldro_quotes;
+
   (* Initialize printer *)
   EcCorePrinting.Registry.register (module EcPrinting);
 
@@ -780,6 +788,14 @@ let main () =
               List.iter
                 (fun p ->
                    let loc = p.EP.gl_action.EcLocation.pl_loc in
+                   (* Mechanism B: a location should never escape quotation
+                      position-remapping (EcIo) carrying the synthetic buffer
+                      filename.  If one does, collapse it rather than print
+                      meaningless <quotation:...> coordinates. *)
+                   let loc =
+                     if EcQuotation.is_sentinel loc.EcLocation.loc_fname
+                     then EcLocation._dummy else loc
+                   in
 
                    (* -upto: if this command starts past the target, print goals and exit *)
                    if past_upto loc then begin

src/ecIo.ml

@@ -38,6 +38,11 @@ type ecreader_r = {
   mutable ecr_atstart : bool;
   mutable ecr_trim    : int;
   mutable ecr_tokens  : EcParser.token list;
+  (* Pre-positioned triples produced by expanding a quotation.  These are
+     emitted (front-first) before any token is read from [ecr_lexbuf], so a
+     single quotation can expand to several EC sentences across successive
+     [parse] calls.  Positions are already remapped into the original file. *)
+  mutable ecr_expand  : (EcParser.token * L.position * L.position) list;
 }
 
 type ecreader = ecreader_r Disposable.t
@@ -48,7 +53,8 @@ let ecreader_of_lexbuf (buffer : Buffer.t) (lexbuf : L.lexbuf) : ecreader_r =
     ecr_source  = buffer;
     ecr_atstart = true;
     ecr_trim    = 0;
-    ecr_tokens  = []; }
+    ecr_tokens  = [];
+    ecr_expand  = []; }
 
 (* -------------------------------------------------------------------- *)
 let lexbuf (reader : ecreader) =
@@ -97,13 +103,71 @@ let finalize (ecreader : ecreader) =
   Disposable.dispose ecreader
 
 (* -------------------------------------------------------------------- *)
-let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
+(* Expand a quotation into a list of pre-positioned token triples.       *)
+(* The handler output is lexed in its own buffer; each token's positions  *)
+(* are remapped into the original file via the source map.               *)
+(*                                                                        *)
+(* A quotation expands to a FRAGMENT that is spliced into the surrounding *)
+(* sentence: it may stand for only part of a sentence, and the sentence   *)
+(* terminator ('.') is always written by the user, never produced by the *)
+(* expansion.  Hence the fragment must contain no FINAL.                  *)
+let expand_quotation (q : EcQuotation.quotation)
+  : (EcParser.token * L.position * L.position) list
+=
+  let (expanded, sm) = EcQuotation.run q in
+  let sub = Lexing.from_string expanded in
+  Lexing.set_filename sub (EcQuotation.sentinel_fname q);
+
+  let remap o = EcQuotation.remap_position sm q o in
+
+  let rec collect acc =
+    let toks =
+      try EcLexer.main sub
+      with EcLexer.LexicalError (_, msg) ->
+        EcQuotation.error q
+          (Printf.sprintf "lexical error in expansion: %s" msg)
+    in
+    (* positions of the lexeme just consumed by EcLexer.main *)
+    let sp = remap (Lexing.lexeme_start sub) in
+    let ep = remap (Lexing.lexeme_end   sub) in
+    let acc =
+      List.fold_left (fun acc tk -> (tk, sp, ep) :: acc) acc toks in
+    match toks with
+    | [EcParser.EOF] -> List.rev acc
+    | _              -> collect acc
+  in
+  let triples = collect [] in
+
+  (* drop the lexed EOF; the surrounding stream supplies sentence flow *)
+  let body = List.filter (fun (t, _, _) -> t <> EcParser.EOF) triples in
+  (* a fragment must not terminate the sentence: the '.' is the user's *)
+  let isfinal = function EcParser.FINAL _ -> true | _ -> false in
+  if List.exists (fun (t, _, _) -> isfinal t) body then
+    EcQuotation.error q
+      "quotation expansion must be a sentence fragment (it must not contain '.')";
+  body
+
+(* -------------------------------------------------------------------- *)
+let rec lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
   let lexbuf = ecreader.ecr_lexbuf in
 
   let isfinal = function
     | EcParser.FINAL _ -> true
     | _ -> false in
 
+  (* Emit the next pre-positioned expansion triple, if any. *)
+  let emit_expand () =
+    match ecreader.ecr_expand with
+    | [] -> None
+    | triple :: rest ->
+        ecreader.ecr_expand <- rest;
+        Some triple
+  in
+
+  match emit_expand () with
+  | Some triple -> triple
+  | None ->
+
   if ecreader.ecr_atstart then
     ecreader.ecr_trim <- ecreader.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum;
 
@@ -119,6 +183,17 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
         ecreader.ecr_tokens <- tokens
   done;
 
+  (* Intercept a quotation token: expand it into a fragment and splice it.
+     A quotation always sits at the head of [ecr_tokens] (its lexer rule
+     returns a singleton list).  An empty fragment is allowed -- recurse to
+     produce the next real token. *)
+  match ecreader.ecr_tokens with
+  | EcParser.QUOTATION q :: queue ->
+      ecreader.ecr_tokens <- queue;
+      ecreader.ecr_expand <- expand_quotation q;
+      lexer ?checkpoint ecreader
+  | _ ->
+
   let token, queue = List.destruct ecreader.ecr_tokens in
 
   let token, prequeue =