feat(notations): add user-extensible notations

Adds a `notation` construct that lets users declare `#`-prefixed
syntactic sugar for formulas, with template-based parsing and
typing-time expansion.

Notations are stored as operators (sharing abbreviation
infrastructure), so they work uniformly with import/export, clone,
locality, sections, qualified lookup, and `rewrite /#foo` unfolds.

Declarations:

    notation #big ['a] #< i : 'a >
        (r : 'a list)
        (P : i ==> bool = predT)
        (F : i ==> t)
      "[" i " : " r ("| " P)? "] " F =
      big P F r.

Uses:

    lemma L (d : 'a distr) (f : 'a -> real) J :
      uniq J =>
      BRA.#big [ x : J ] (mu1 d x * f x).`1 <= 1%r.

    lemma M &m (bs : out_t list) :
      Dst.#big [ b : bs ] (Pr[A.guess() @ &m : res = b]) <= 1%r.

    (* slot placeholders work as pose / rewrite patterns *)
    pose c := #big [ _ : _ | _ ] _.

Expansions round-trip back to template syntax in the pretty-printer.

Includes a stdlib port: `#big` / `#bigi` are declared in Bigop.eca
and used across algebra, analysis, distributions, modules, and
crypto files.

Tests under tests/notations/ (wired into `make unit`) and reference
documentation under doc/notation.rst.

Author: strub

config/tests.config

@@ -14,4 +14,4 @@ exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomple
 okdirs = examples/MEE-CBC
 
 [test-unit]
-okdirs = tests tests/exception
+okdirs = tests tests/exception tests/notations

doc/index.rst

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

doc/notation.rst

@@ -0,0 +1,275 @@
+========================================================================
+Notations
+========================================================================
+
+Notations are user-declared surface-syntax forms for formulas.  A
+declaration binds a name prefixed by ``#`` to a template of literal
+punctuation and slots; uses of the notation at the call site are parsed
+against the template and expanded to an underlying body at type-checking
+time.  Notations live in the same namespace as operators and
+abbreviations: they follow ``import``/``export``/``clone`` rules, they
+can be declared ``local`` inside a ``section``, and the pretty-printer
+automatically renders expanded bodies back to template syntax whenever
+possible.
+
+------------------------------------------------------------------------
+Anatomy of a declaration
+------------------------------------------------------------------------
+
+.. admonition:: Syntax
+
+   | ``local``? ``notation`` ``#``\ *name*
+   |   *tyvars*?
+   |   *binder-slots*?
+   |   *form-slots*\ *
+   |   *template*
+   |   (``:`` *codom*)?
+   |   ``=`` *body* ``.``
+
+Every piece except the name, template, and body is optional.  The
+declaration mirrors an operator declaration with an extra *template*
+section that describes the surface syntax.
+
+Example::
+
+  notation #pair (a : int) (b : int) " [" a ", " b "] " = (a, b).
+
+  lemma L (x y : int) : #pair [x, y] = (x, y).
+  proof. by trivial. qed.
+
+------------------------------------------------------------------------
+Template literals and punctuations
+------------------------------------------------------------------------
+
+A template is a sequence that alternates **STRING literals** and **slot
+references**.  The first element of the template must be a STRING.
+
+Each STRING must lex to exactly one of six punctuation tokens:
+
+  ``[``   ``]``   ``:``   ``|``   ``,``   ``;``
+
+Additional whitespace *inside* the string is ignored by the input
+matcher but preserved verbatim by the pretty-printer.  For example,
+``" [ "`` and ``"["`` both match a single ``[`` at the call site, but
+the former pretty-prints with spaces on both sides.
+
+A STRING that lexes to zero tokens, two or more tokens, or an
+unsupported symbol is rejected at declaration time::
+
+  notation #bad " @" a " @ " = a.
+  (* rejected: notation punctuation `" @"' must lex to one of: [ ] : | , ; *)
+
+------------------------------------------------------------------------
+Slots
+------------------------------------------------------------------------
+
+A slot is a bare lowercase identifier inside the template.  Each slot
+must be declared earlier in the notation as either a **form slot** or a
+**binder slot**.
+
+Form slots
+   Declared with ``( name : ty )`` in the usual function-argument style.
+   At the call site the slot consumes a formula; at typing time the
+   formula is checked against ``ty``.
+
+Binder slots
+   Declared inside ``#< ... >`` before the form-slot block, for example
+   ``#< i : int >`` or ``#< i : int, j : int >``.  A binder slot reads
+   an *identifier* at the call site.  The chosen identifier becomes a
+   locally-bound name visible to any form slot that depends on it.
+
+Per-slot binder dependencies
+   A form slot can declare that it depends on binder slots via
+   ``==>``::
+
+     notation #mapI #< i : int > (n : int) (f : i ==> int)
+       " [" i " : " n " : " f "] " =
+       map f (iota_ 0 n).
+
+   At typing, ``f`` has type ``int -> int`` (curried over the binders
+   it declares).  At the call site the user writes the body of the
+   lambda in terms of the chosen binder name, and the expansion wraps
+   it automatically::
+
+     lemma M : #mapI [k : 4 : k + 1] = map (fun k => k + 1) (iota_ 0 4).
+     proof. by trivial. qed.
+
+**Template ordering constraint.** A form slot that depends on a binder
+``i`` must appear *after* ``i`` in the template.  Forward references
+are rejected at declaration time.
+
+**Slot kind is inferred from the declaration, not the template.** A
+template reference like ``i`` means "ident slot" iff ``i`` is in the
+``#< ... >`` group; otherwise it means "form slot".
+
+------------------------------------------------------------------------
+Type parameters
+------------------------------------------------------------------------
+
+Notations may be polymorphic.  Type parameters are declared in the same
+``['a 'b]`` syntax used by operators, appearing before the slot lists::
+
+  notation #ppair ['a 'b] (a : 'a) (b : 'b) " [" a ", " b "] " = (a, b).
+
+  lemma L (x : int) (y : bool) : #ppair [x, y] = (x, y).
+  proof. by trivial. qed.
+
+Type parameters are freshened at every call site, so independent uses
+do not leak type equalities.
+
+------------------------------------------------------------------------
+Semantics
+------------------------------------------------------------------------
+
+A notation is compiled to a regular operator of kind ``OB_nott`` that
+records the template alongside the typed body.  At a call site
+``#name [ ... ]``:
+
+1. The parser looks up the template for ``#name`` and consumes tokens
+   according to its items, collecting the slot arguments.
+2. The resulting ``PFntt`` node is type-checked.  For each form slot
+   with binder dependencies, the argument is type-checked in an
+   environment extended with the user-chosen binder idents, then
+   wrapped in ``fun`` over those idents.  For each ident slot, a fresh
+   local is created with the user-chosen name.  The body is then
+   obtained by substituting all slot idents with their resolved
+   values and alpha-renaming each bound binder to the user-chosen
+   name.
+
+Because expansion happens at typing, slot-level errors attribute to the
+user's source and not to the declaration's body.
+
+------------------------------------------------------------------------
+Locality
+------------------------------------------------------------------------
+
+A declaration may be prefixed with ``local`` inside a ``section``; the
+notation is then discharged when the section closes::
+
+  section.
+    local notation #tmp (a : int) " [" a "] " = a + 1.
+    lemma inside : #tmp [3] = 4.
+    proof. by trivial. qed.
+  end section.
+  (* #tmp is no longer visible here. *)
+
+Outside a section, ``local notation`` is rejected, as for other
+operators.
+
+------------------------------------------------------------------------
+Pretty-printing
+------------------------------------------------------------------------
+
+The pretty-printer reverse-matches the body of each registered notation
+against each formula it prints.  When a formula matches the body of a
+notation, the printer renders it using the template, honouring
+whitespace from the declaration's STRING literals::
+
+  notation #pair (a : int) (b : int) " [" a ", " b "] " = (a, b).
+
+  lemma L (x y : int) : #pair [x, y] = (x, y).
+
+  print L.
+  (* lemma L: forall (x y : int), #pair [x, y]  = #pair [x, y] . *)
+
+For notations with binder slots, the printer unwraps the matched
+lambdas to recover the user's chosen binder names.
+
+------------------------------------------------------------------------
+Examples
+------------------------------------------------------------------------
+
+A polymorphic pair::
+
+  notation #pair ['a 'b] (a : 'a) (b : 'b) " [" a ", " b "] " = (a, b).
+
+  lemma L (x : int) (y : bool) : #pair [x, y] = (x, y).
+  proof. by trivial. qed.
+
+A polymorphic map notation with an explicit lambda::
+
+  notation #pmap ['a 'b] (f : 'a -> 'b) (xs : 'a list)
+    " [" f " : " xs "] " =
+    map f xs.
+
+  lemma L : #pmap [(fun x => x + 1) : [1; 2; 3]] = [2; 3; 4].
+  proof. by trivial. qed.
+
+A binder-slot map notation where the user-chosen name scopes into the
+body form::
+
+  notation #mapI #< i : int > (n : int) (f : i ==> int)
+    " [" i " : " n " : " f "] " =
+    map f (iota_ 0 n).
+
+  lemma L : #mapI [k : 4 : k + 1] = map (fun k => k + 1) (iota_ 0 4).
+  proof. by trivial. qed.
+
+A notation inside a section::
+
+  section.
+
+    notation #gpair (a : int) (b : int) " [" a ", " b "] " = (a, b).
+    local notation #lpair (a : int) (b : int) " [" a ", " b "] " = (a, b).
+
+    lemma t_g : #gpair [1, 2] = (1, 2).
+    proof. by trivial. qed.
+
+    lemma t_l : #lpair [1, 2] = (1, 2).
+    proof. by trivial. qed.
+
+  end section.
+
+  lemma after : #gpair [3, 4] = (3, 4).
+  proof. by trivial. qed.
+
+------------------------------------------------------------------------
+Error catalogue
+------------------------------------------------------------------------
+
+The following errors may appear at notation-declaration or call time.
+
+``notation punctuation `"x"' must lex to one of: [ ] : | , ;``
+   A template STRING could not be lexed to exactly one of the six
+   accepted punctuation tokens.
+
+``template references unknown slot: `x'``
+   The template refers to a slot name that is not declared as either a
+   binder slot (``#< ... >``) or a form slot (``( ... )``).
+
+``form slot depends on binder `i', which must be declared earlier in the template``
+   A form slot's ``==>`` dependency was listed, but the binder slot
+   appears *after* the form slot in the template.  Re-order the
+   template.
+
+``parse error: unknown notation `#name'``
+   The call site used a notation name that is not in scope.  The
+   notation may not be ``import``-ed, may be ``local`` and out of
+   scope, or simply not declared.
+
+``parse error: in notation `#name': expected `:'``
+   The call site did not match the template at the indicated punct.
+   Check that the call reproduces the declaration template verbatim.
+
+``parse error: in notation `#name': expected identifier for binder slot `i'``
+   A binder slot consumes an identifier at the call site; another
+   token was supplied.
+
+------------------------------------------------------------------------
+Limitations
+------------------------------------------------------------------------
+
+- The punctuation palette is fixed to the six tokens listed above.
+  Arbitrary keywords or operator symbols are not accepted because the
+  lexer tokenizes ahead of the notation-aware parser.
+
+- Templates cannot describe iteration (e.g. ``item*`` or
+  ``item, ...``) or optional parts.  Each declaration has a single,
+  fixed shape.
+
+- Within a single theory file loaded via ``require``, a notation
+  declared on line *N* is visible from line *N + 1* onward.  In
+  interactive mode the visibility is immediate.
+
+- A ``local notation`` must appear inside a ``section``, as for other
+  ``local`` operators.

src/dune

@@ -31,4 +31,4 @@
 (menhir
  (modules ecParser)
  (explain true)
- (flags --table --unused-token COMMENT))
+ (flags --table --unused-token COMMENT --inspection))

src/ecCommands.ml

@@ -556,12 +556,24 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) =
         let i_pragma = Pragma.get () in
 
         try_finally (fun () ->
-          let commands = EcIo.parseall (EcIo.from_file filename) in
-          let commands =
-            List.fold_left
-              (fun scope g -> process_internal subld scope g.gl_action)
-              iscope commands in
-          commands)
+          let reader = EcIo.from_file filename in
+          let rec loop scope =
+            let notations = EcEnv.Op.lookup_template (EcScope.env scope) in
+            match EcLocation.unloc (EcIo.parse ~notations reader) with
+            | EcParsetree.P_Prog (commands, terminate) ->
+                let scope =
+                  List.fold_left
+                    (fun scope g -> process_internal subld scope g.gl_action)
+                    scope commands in
+                if terminate then scope else loop scope
+            | EcParsetree.P_DocComment _ ->
+                loop scope
+            | EcParsetree.P_Undo _ | EcParsetree.P_Exit ->
+                assert false
+          in
+          try_finally
+            (fun () -> loop iscope)
+            (fun () -> EcIo.finalize reader))
         (fun () -> Pragma.set i_pragma)
       in
 

src/ecDecl.ml

@@ -110,11 +110,35 @@ and opbranch = {
   opb_sub  : opbranches;
 }
 
+and nt_punct_kind =
+  [ `LBRACKET | `RBRACKET | `COLON | `PIPE | `COMMA | `SEMICOLON ]
+
+and nt_punct = {
+  np_kind    : nt_punct_kind;   (* lexed token to match at use sites *)
+  np_display : string;          (* verbatim source, for pretty-printing *)
+}
+
+and nt_slot_kind =
+  | NTS_Form  of EcSymbols.symbol list (* binder slots this form depends on, in order *)
+  | NTS_Ident
+
+and nt_template_item =
+  | NTI_Punct    of nt_punct
+  | NTI_Slot     of EcSymbols.symbol * nt_slot_kind
+  | NTI_Optional of nt_template_item list   (* first item must be NTI_Punct *)
+
+and nt_template = nt_template_item list
+
 and notation = {
-  ont_args  : (EcIdent.t * EcTypes.ty) list;
-  ont_resty : EcTypes.ty;
-  ont_body  : expr;
-  ont_ponly : bool;
+  ont_args     : (EcIdent.t * EcTypes.ty) list;
+  ont_resty    : EcTypes.ty;
+  ont_body     : expr;
+  ont_ponly    : bool;
+  ont_template : nt_template option;
+  ont_defaults : expr EcIdent.Mid.t;
+    (* Default value for each slot that only appears inside optional
+       template groups. Keys are ont_args idents; absent slots → no
+       default (must appear outside all optional groups). *)
 }
 
 and prind = {
@@ -234,10 +258,25 @@ let mk_exception (exn_loca : locality) (exn_dom : ty list) : exception_ =
 
 let mk_abbrev ?(ponly = false) tparams xs (codom, body) lc =
   let kind = {
-    ont_args  = xs;
-    ont_resty = codom;
-    ont_body  = body;
-    ont_ponly = ponly;
+    ont_args     = xs;
+    ont_resty    = codom;
+    ont_body     = body;
+    ont_ponly    = ponly;
+    ont_template = None;
+    ont_defaults = EcIdent.Mid.empty;
+  } in
+
+  gen_op ~opaque:optransparent tparams
+    (EcTypes.toarrow (List.map snd xs) codom) (OB_nott kind) lc
+
+let mk_notation ?(defaults = EcIdent.Mid.empty) tparams xs (codom, body) template lc =
+  let kind = {
+    ont_args     = xs;
+    ont_resty    = codom;
+    ont_body     = body;
+    ont_ponly    = false;
+    ont_template = Some template;
+    ont_defaults = defaults;
   } in
 
   gen_op ~opaque:optransparent tparams