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,5 @@ 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
+kodirs = tests/notations-ko

doc/index.rst

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