This is a command-line normalizer, rewriter, and dataizer of 𝜑-calculus expressions.

First, you write a simple 𝜑-calculus program in the hello.phi file:

Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧

Then you can install phino in two ways:

Install Cabal first and then:

cabal update
cabal install --overwrite-policy=always phino-0.0.79
phino --version

Or download binary from the internet using curl or wget:

sudo curl -o /usr/local/bin/phino http://phino.objectionary.com/releases/macos-15/phino-latest
sudo chmod +x /usr/local/bin/phino
phino --version

Download paths are:

• Ubuntu 22.04: http://phino.objectionary.com/releases/ubuntu-22.04/phino-latest
• Ubuntu 24.04: http://phino.objectionary.com/releases/ubuntu-24.04/phino-latest
• MacOS (ARM): http://phino.objectionary.com/releases/macos-15/phino-latest
• MacOS (Intel): http://phino.objectionary.com/releases/macos-14-large/phino-latest
• Windows: http://phino.objectionary.com/releases/windows-2022/phino-latest.exe

To build phino from source, clone this repository:

git clone git@github.com:objectionary/phino.git
cd phino

Then, run the following command (ensure you have Cabal installed):

cabal build all

Next, run this command to install phino system-wide:

sudo cp "$(cabal list-bin phino)" /usr/local/bin/phino

Verify that phino is installed correctly:

$ phino --version
0.0.0

You can ensure scripts are run with a specific version of phino using the --pin global option. It exits with an error when the version supplied doesn't match the installed one:

phino --pin=0.0.0.67 dataize hello.phi

Then, you dataize the program:

$ phino dataize hello.phi
68-65-6C-6C-6F

You can rewrite this expression with the help of rules defined in the my-rule.yml YAML file (here, the !d is a capturing group, similar to regular expressions):

name: My custom rule
pattern: Δ ⤍ !d
result: Δ ⤍ 62-79-65

Then, rewrite:

$ phino rewrite --rule=my-rule.yml hello.phi
Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧, t ↦ ξ.k, k ↦ ⟦⟧ ⟧

If you want to use many rules, just use --rule as many times as you need:

phino rewrite --rule=rule1.yaml --rule=rule2.yaml ...

You can also use built-in rules, which are designed to normalize expressions:

phino rewrite --normalize hello.phi

If no input file is provided, the 𝜑-expression is taken from stdin:

$ echo 'Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧ ⟧' | phino rewrite --rule=my-rule.yml
Φ ↦ ⟦ φ ↦ ⟦ Δ ⤍ 62-79-65 ⟧ ⟧

You're able to pass XMIR as input. Use --input=xmir and phino will parse given XMIR from file or stdin and convert it to phi AST.

phino rewrite --rule=my-rule.yaml --input=xmir file.xmir

Also phino supports 𝜑-expressions in ASCII format and with syntax sugar. The rewrite command also allows you to desugar the expression and print it in canonical syntax:

$ echo 'Q -> [[ @ -> Q.io.stdout("hello") ]]' | phino rewrite
Φ ↦ ⟦
  φ ↦ Φ.io.stdout(
    α0 ↦ Φ.string(
      α0 ↦ Φ.bytes(
        α0 ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧
      )
    )
  )
⟧

You can merge several 𝜑-programs into a single one by merging their top level formations:

$ cat bytes.phi
{⟦ bytes(data) ↦ ⟦ φ ↦ data ⟧ ⟧}
$ cat number.phi
{⟦
  number(as-bytes) ↦ ⟦
    φ ↦ as-bytes,
    plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧
  ⟧
⟧}
$ cat minus.phi
{⟦ number ↦ ⟦ minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧ ⟧ ⟧}
$ phino merge bytes.phi number.phi minus.phi --sweet
{⟦
  bytes(data) ↦ ⟦ φ ↦ data ⟧,
  number(as-bytes) ↦ ⟦
    φ ↦ as-bytes,
    plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
    minus(x) ↦ ⟦ λ ⤍ L_number_minus ⟧
  ⟧
⟧}

You can test the 𝜑-program matches against the rule pattern. The result output contains matched substitutions:

$ phino match --pattern='⟦ Δ ⤍ !d, !B ⟧' hello.phi
B >> ⟦ ρ ↦ ∅ ⟧
d >> 68-65-6C-6C-6F

You can explain the built-in rules by printing them in LaTeX format. Pass exactly one of --normalize, --morph or --dataize for the rewriting, morphing (𝕄) or dataization (𝔻) rules (or --rule for a custom rule file):

$ phino explain --normalize
\begin{tabular}{rl}
\trrule{alpha}
  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_2 -> e ) }
  { [[ B_1, \tau_1 -> ?, B_2 ]] ( \tau_1 -> e ) }
  { if $ \indexof{ \tau_2 } = \vert B_1 \vert $ }
  { }
\trrule{dc}
  { T ( \tau -> e ) }
  { T }
  { }
  { }
...
\trrule{stop}
  { [[ B ]] . \tau }
  { T }
  { if $ \tau \notin B \;\text{and}\; @ \notin B \;\text{and}\; L \notin B $ }
  { }
\end{tabular}

The morphing and dataization rules are printed the same way:

$ phino explain --morph
\begin{tabular}{rl}
\trrule{Mprim}
  { \mathbb{M}( e ) }
  { e }
  { if $ e \in \mathcal{P} $ }
  { }
...
\trrule{Mphi}
  { \mathbb{M}( Q . \tau * t ) }
  { \mathbb{M}( e * t ) }
  { }
  { where $ e \coloneqq global( \tau ) $ }
\end{tabular}

$ phino explain --dataize
\begin{tabular}{rl}
\trrule{delta}
  { \mathbb{D}( [[ B_1, D> δ, B_2 ]] ) }
  { δ }
  { }
  { }
...
\trrule{none}
  { \mathbb{D}( e ) }
  { \varnothing }
  { }
  { }
\end{tabular}

For more details, use phino [COMMAND] --help option.

This is BNF-like yaml rule structure. Here types ended with apostrophe, like Attribute' are built types from 𝜑-program AST

Rule:
  name: String
  pattern: String
  result: String
  when: Condition?       # predicate, works with substitutions before extension
  where: [Extension]?    # substitution extensions
  having: Condition?     # predicate, works with substitutions after extension

Condition:
  = and: [Condition]     # logical AND
  | or:  [Condition]     # logical OR
  | not: Condition       # logical NOT
  | alpha: Attribute'    # check if given attribute is alpha
  | eq:                  # compare two comparable objects
      - Comparable
      - Comparable
  | in:                  # check if attributes exist in bindings
      - Attribute'
      - Binding'
  | nf: Expression'      # returns True if given expression in normal form
                         # which means that no more other normalization rules
                         # can be applied
  | absolute: Expression' # returns True if given expression is xi-free, i.e.
                         # there is no ξ outside of a formation: it is Φ, a
                         # formation, a dispatch with a xi-free subject, or an
                         # application with a xi-free subject and argument.
                         # Combined with a normal-form check by the '𝑘'/'!k'
                         # meta variable, which ranges over the absolute
                         # expressions 𝒦 ⊆ 𝒩, used by the Rcopy rule.
  | matches:             # returns True if given expression after dataization
      - String           # matches to given regex
      - Expression
  | part-of:             # returns True if given expression is attached to any
      - Expression'      # attribute in ginve bindings
      - BiMeta'

Comparable:              # comparable object that may be used in 'eq' condition
  = Attribute'
  | Number
  | Expression'

Number:                  # comparable number
  = Integer              # just regular integer
  | index: Attribute'    # calculate index of alpha attribute
  | length: BiMeta'      # calculate length of bindings by given meta binding

Extension:               # substitutions extension used to introduce new meta variables
  meta: [ExtArgument]    # new introduced meta variable
  function: String       # name of the function
  args: [ExtArgument]    # arguments of the function

ExtArgument
  = Bytes'               # !d
  | Binding'             # !B
  | Expression'          # !e
  | Attribute'           # !a

Here's list of functions that are supported for extensions:

• contextualize - function of two arguments, that rewrites given expression depending on provided context according to the contextualization rules
• random-tau - creates attribute with random unique name. Accepts bindings, and attributes. Ensures that created attribute is not present in list of provided attributes and does not exist as attribute in provided bindings.
• dataize - dataizes given expression and returns bytes.
• concat - accepts bytes or dataizable expressions as arguments, concatenates them into single sequence and convert it to expression that can be pretty printed as human readable string: Φ.string(Φ.bytes⟦ Δ ⤍ !d ⟧).
• sed - pattern replacer, works like unix sed function. Accepts two arguments: target expression and pattern. Pattern must start with s/, consists of three parts separated by /, for example, this pattern s/\\s+//g replaces all the spaces with empty string. To escape braces and slashes in pattern and replacement parts - use them with \\, e.g. s/\\(.+\\)//g.
• random-string - accepts dataizable expression or bytes as pattern. Replaces %x and %d formatters with random hex numbers and decimals accordingly. Uniqueness is guaranteed during one execution of phino.
• size - accepts exactly one meta binding and returns size of it and Φ.number.
• tau - accepts Φ.string, dataizes it and converts it to attribute. If dataized string can't be converted to attribute - an error is thrown.
• string - accepts Φ.string or Φ.number or attribute and converts it to Φ.string.
• number - accepts Φ.string and converts it Φ.number
• sum - accepts list of Φ.number or Φ.bytes and returns sum of them as Φ.number
• join - accepts list of bindings and returns list of joined bindings. Duplicated ρ, Δ and λ attributes are ignored, all other duplicated attributes are replaced with unique attributes using random-tau function.

The phino supports meta variables to write 𝜑-expression patterns for capturing attributes, bindings, etc.

This is the list of supported meta variables:

• !a || 𝜏 - attribute
• !e || 𝑒 - any expression
• !n || 𝑛 - any expression that is already in normal form (behaves like !e/𝑒, but only binds a sub-expression in NF, so no explicit nf: guard is needed)
• !k || 𝑘 - any expression that is absolute, i.e. xi-free and in normal form (ranges over 𝒦 ⊆ 𝒩); behaves like !e/𝑒 but only binds an absolute sub-expression, so no explicit absolute: or nf: guard is needed
• !B || 𝐵 - list of bindings
• !d || δ - bytes in meta delta binding
• !t - tail after expression, a possibly empty sequence of applications and/or dispatches
• !F - function name in meta lambda binding

Every meta variable may also be used with an integer index, like !B1 or 𝜏0.

Incorrect usage of meta variables in 𝜑-expression patterns leads to parsing errors.

To run performance benchmarks, you need Java 8+ and curl. Maven is downloaded automatically on first run via benchmark/mvnw.

The benchmark uses the compiled Native class from JNA — a large real-world Java class — as its test input. On first run, make bench downloads the class, disassembles it to XMIR via jeo-maven-plugin, converts it to 𝜑 using phino rewrite, and caches the results in benchmark/tmp/. Subsequent runs skip straight to the benchmarks.

make bench

=== parse/phi ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      1299342.512 μs
  avg:        129934.251 μs
  min:        118253.218 μs
  max:        162332.377 μs
  std dev:    16619.006 μs
=== parse/xmir ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      7609340.593 μs
  avg:        760934.059 μs
  min:        697264.466 μs
  max:        801903.360 μs
  std dev:    31387.398 μs
=== rewrite/normalize ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      394738.996 μs
  avg:        39473.900 μs
  min:        38668.484 μs
  max:        40389.889 μs
  std dev:    473.832 μs
=== print/sweet/multiline ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      4562591.028 μs
  avg:        456259.103 μs
  min:        451902.950 μs
  max:        462770.604 μs
  std dev:    3059.588 μs
=== print/sweet/flat ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      4529234.270 μs
  avg:        452923.427 μs
  min:        418300.611 μs
  max:        476533.304 μs
  std dev:    23032.941 μs
=== print/salty/multiline ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      13656171.599 μs
  avg:        1365617.160 μs
  min:        1311639.249 μs
  max:        1429575.023 μs
  std dev:    37618.391 μs

The results were calculated in this GHA job on 2026-06-11 at 11:02, on Linux with 4 CPUs.

Fork repository, make changes, then send us a pull request. We will review your changes and apply them to the master branch shortly, provided they don't violate our quality standards. To avoid frustration, before sending us your pull request please make sure all your tests pass:

make all

To generate a local coverage report for development, run:

make coverage

You will need GHC ≥ 9.6.7 and Cabal ≥ 3.0 (recommended) or Stack ≥ 3.0 installed.