Conversation
strub
force-pushed
the
notations
branch
2 times, most recently
from
022943c to
50d9941
Compare
Moves the polymorphic variant types used by the SMT option grammar
rules (`prover`, `pi`, `smt`) out of the parser's `%{ ... %}` header
into `EcParsetree` (renamed to `psmtprover`, `psmt_prover_info`,
`psmt` for consistency with the other `p*` parsetree types).
Also enables menhir's `--inspection` flag on the parser so the
generated `MenhirInterpreter` module exposes nonterminal symbols for
external inspection. The flag requires nonterminal action types to
be accessible from outside the parser module, which is why the types
have to leave the `%{ ... %}` header.
Prep for a subsequent feature commit that relies on `--inspection`.
No semantic change to SMT parsing.
strub
force-pushed
the
notations
branch
7 times, most recently
from
ac46337 to
2f2088e
Compare
When [f_match_core] hits a mismatch it already tries beta-reduction, higher-order matching, and delta-unfolding. Adds an eta-normalisation fallback that runs [EcReduction.eta_norm] on both sides and retries once. Also exposes [eta_norm] from [EcReduction]'s signature. The matcher is sensitive to how functions are eta-packaged: a slot written `fun i => f i` vs the equivalent `f` would fail to match if one side was stored with an extra lambda. Rather than normalising at every rewrite site, handle it once inside the unifier.
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds a
notationconstruct that lets users declare#-prefixedsyntactic 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 /#foounfolds.Declarations:
Uses:
Expansions round-trip back to template syntax in the pretty-printer.
Includes a stdlib port:
#big/#bigiare declared in Bigop.ecaand used across algebra, analysis, distributions, modules, and
crypto files.
Tests under tests/notations/ (wired into
make unit) and referencedocumentation under doc/notation.rst.