Normalizer for 𝜑-calculus

This command line tool helps you deal with 𝜑-calculus expressions, usually produced by the EO compiler.

First, install it (you should install Stack first):

stack update
stack install eo-phi-normalizer

Then, normalize a simple 𝜑-expression:

$ cat > foo.phi
{⟦ m ↦ ⟦ x ↦ ⟦ ρ ↦ ∅ ⟧.ρ.k, k ↦ ⟦ Δ ⤍ 42- ⟧ ⟧.x ⟧}
$ eo-phi-normalizer rewrite --chain --tex foo.phi

The output will contain a ready-to-use LaTeX document, where all rewritting steps are explained.

More detailed documentation is here.

How to use custom rules?

By default, the rules of normalization of 𝜑-calculus are used. They are defined in the rules.yaml file. You can use your own rules, with the help of our custom YAML format, for example in forty-three.yml:

title: "forty-three"
rules:
  - name: forty-three
    description: 'change 33 double to 42 double'
    pattern: |
      Φ.org.eolang.bytes ( α0 ↦ ⟦ Δ ⤍ 40-40-80-00-00-00-00-00 ⟧ )
    result: |
      Φ.org.eolang.bytes ( α0 ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧ )
    tests: [ ]

Then, use this file:

eo-phi-normalizer rewrite --rules=forty-three.yml foo.phi