Skip to content

Command Line Normalizer and Rewriter of πœ‘-calculus Expressions (part of EOLANG family)

License

Notifications You must be signed in to change notification settings

objectionary/eo-phi-normalizer

Folders and files

NameName
Last commit message
Last commit date

Latest commit

a34269f Β· Dec 17, 2024
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Normalizer for πœ‘-calculus

eo-phi-normalizer on Hackage Haddock License Hits-of-Code Lines of code

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