objectionary / normalizer

Command Line Normalizer of 𝜑-calculus Expressions
https://www.objectionary.com/normalizer/
MIT License
7 stars 2 forks source link

423 custom rules #432

Closed fizruk closed 1 month ago

fizruk commented 2 months ago

This PR aims to close #423. However, the implementation diverges with the initial proposal. Here is what is in this PR:

Here are the differences with the initial proposal in #423:

  1. Metavariable identifiers start with ! and we do not (yet) distinguish their types (attribute/object/binding/etc.).
  2. Instead of t1 * t2 we use one-hole context patterns !C1 [1| obj |1]. The notation is subject to change (in particular, we may allow obj * !C1, for example). Importantly, the one-hole context pattern allows to match against objects in application arguments.
  3. forall is implicit: all metavariables used in the pattern are automatically put under the forall.
  4. exists is replaced with fresh (and can only yield fresh attributes).
  5. Only one pattern and result are supported, multiple pattern-result pairs will be supported later (see #440).

PR-Codex overview

This PR updates object and meta ID handling in the EO Phi normalizer.

Detailed summary

The following files were skipped due to too many changes: eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs, eo-phi-normalizer/src/Language/EO/Phi/Syntax/Lex.x, eo-phi-normalizer/test/eo/phi/rules/yegor.yaml, eo-phi-normalizer/src/Language/EO/Phi/Syntax/Print.hs, eo-phi-normalizer/src/Language/EO/Phi/Syntax/Par.y, eo-phi-normalizer/src/Language/EO/Phi/Syntax/Doc.txt, eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs

✨ Ask PR-Codex anything about this PR by commenting with /codex {your question}

0crat commented 1 month ago

@deemp Thanks for the review! You've earned +35 points for this: +25 as a basis; +5 for 876 hits-of-code; +5 for 0 comments. Your running balance is +5.

0crat commented 1 month ago

@fizruk Thanks for the contribution! You've earned +5 points for this: +20 as a basis; +5 for 876 hits-of-code; -7 for too many hits-of-code (876 >= 100); -15 for way too many hits-of-code (876 >= 400); -5 for 0 comments; +7 to give you at least something. Please, keep them coming. Your running balance is +30.