Command-Line Manipulator of 𝜑-Calculus Expressions

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

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

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

Installation

Then you can install phino in two ways:

Install Cabal first and then:

cabal update
cabal install --overwrite-policy=always phino-0.0.161
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

In a GitHub Actions workflow, one step downloads the binary for the runner and puts it on the PATH:

- uses: objectionary/phino@0.0.161
  with:
    version-file: phino-version.txt
- run: phino --version

The file holds the version to install, such as 0.0.150. Give version: 0.0.150 instead of version-file to write the version in the workflow itself.

Build

To build phino from source, clone this repository and build it with Cabal:

git clone git@github.com:objectionary/phino.git
cd phino
cabal build all
sudo cp "$(cabal list-bin phino)" /usr/local/bin/phino

The global --pin option fails the run when the installed version is not the one given, and --pin-file reads that version from a file:

phino --pin=0.0.0.67 dataize hello.phi

Dataize

Then, you dataize the expression:

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

Symbolic λ functions

phino implements no λ function. They come from a YAML file given with --symbolic, one entry per λ function. An entry never computes a value. It answers with a term that holds a symbol, 𝜎, which names a value nobody worked out. Here is atoms.yaml, which the examples below use:

- λ: L_number_(plus|times)
  dataize:
    𝛿1: $.ρ
    𝛿2: $.x
  𝑛: Φ.number( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )

$ cat sum.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,
  φ ↦ 5.plus( 6 )
⟧
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho sum.phi
40-45-00-00-00-00-00-00

Dataizing a symbol always gives the same bytes, the number 42, as above.

Inside an entry, $ is the formation being fired and Φ is the universe. A meta is a named placeholder: 𝛿1, 𝛿2 and so on hold bytes, while 𝑛1, 𝑛2 and so on hold terms. An entry may hold only the keys below, and any other key refuses the whole file:

• λ is a regular expression that matches the whole λ name. No two entries may match the same name.
• dataize binds a bytes meta to the data a term comes down to through dataization, 𝔻. The term is a path from $, as in 𝛿1: $.ρ, or a meta another line binds, as in 𝛿2: 𝑛1.
• morph binds a term meta to the normal form a term reaches through morphing, 𝕄. The term is a path from $, as in 𝑛1: $.x, or a meta another line binds, as in 𝑛4: 𝑛3.
• undress binds a term meta as morph does, and then, while the term is a formation binding φ alone beside its ρ, takes its φ and morphs that.
• evaluate binds a term meta to the answer of firing the formation another meta holds, through evaluation, 𝔼, as in 𝑛2: 𝑛1.
• defer binds a term meta to a fresh symbol when another meta holds a copy of an object whose argument is a bare symbol, ⟦ λ ⤍ 𝜎1 ⟧, and to that term as it is otherwise.
• stay binds a term meta to the term another meta holds, with every ( ρ ↦ … ) applied to a dispatch dropped.
• symbolize binds a term meta to the term another meta holds, with every datum turned into a fresh symbol.
• rewrite binds a term meta to the term the meta under of holds, with the rules under rules applied and nothing normalized afterwards. The rules are written as in a rule file.
• cast holds exactly two lines and binds their two metas as one pair. When one term is a bare symbol, ⟦ λ ⤍ 𝜎1 ⟧, and the other is a formation binding φ, the bare symbol becomes a copy of the other term with 𝜎1 in place of the term its φ chain ends in, whatever that term is.
• 𝑛 is the term the entry answers with. A bare 𝜎 in it stands for a fresh symbol, and no 𝛿 may appear in it.
• join answers with one term made of two sides, in place of 𝑛. It holds on, the condition, which is a bytes meta of dataize or a path from $. It holds left and right, the two sides, each a path from $ or a term meta. It may hold otherwise, a λ name that joins two formations of different shapes one attribute at a time, and the file must answer that name too.
• terminators lists λ names that only raise, as in [L_throw]. A term holding one of them, or an application of one, passes every line as it is, and join takes it for a side that raises, as it takes ⊥. No entry of the file may answer such a name.

An entry holds either 𝑛 or join, never both. The lines of all blocks run in the order of the metas they read, not in the order of the blocks. A line that reads a meta nothing binds refuses the file.

Partial evaluation

A λ name that no entry answers stops the run with an error. With --partial, the run prints the residual program instead: what the known inputs decide is computed, and the rest stays in place:

$ cat partial.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦
    φ ↦ ∅,
    plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧,
    times(ρ, x) ↦ ⟦ λ ⤍ L_number_times ⟧,
    as-bool ↦ ⟦ λ ⤍ L_number_as_bool ⟧
  ⟧,
  φ ↦ 2.times( 3 ).plus( 4 ).as-bool
⟧
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho partial.phi
[ERROR]: No entry of --symbolic answers the λ function 'L_number_as_bool'
$ phino dataize --symbolic=atoms.yaml --partial --sweet --hide-rho partial.phi
L_number_as_bool:λ

Here 2.times( 3 ).plus( 4 ) was computed, and the symbol it came to sits in the hidden ρ, while as-bool stays where it was. An operand that reaches the terminator ⊥ is left in place the same way.

Reducing a term inside a universe

The --inside option reduces a term the program does not hold, taking the program as the universe Φ. It cannot be combined with --locator:

$ cat universe.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧
⟧
$ phino dataize --symbolic=atoms.yaml --inside='5.plus( 6 )' universe.phi
40-45-00-00-00-00-00-00

Limits

Five options stop a run that goes on for too long:

• --max-steps bounds how deep morphing and dataization may nest, 1000 by default;
• --max-firings bounds how many λ functions the whole run may fire;
• --max-seconds bounds how many seconds the whole run may take;
• --max-nodes bounds how many nodes the term of the run may grow to;
• --max-memory bounds the live heap of the run, such as 8G.

--partial leaves a site in place when it runs out of steps, firings, nodes or memory, but a run out of time always fails.

Morph

Morphing, 𝕄, evaluates as far as the object model allows without asking for data, and stops at the first formation it reaches:

$ cat two.phi
⟦
  bytes ↦ ⟦ φ ↦ ∅ ⟧,
  number ↦ ⟦ φ ↦ ∅, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧,
  φ ↦ 5.plus( 6 ).plus( 7 )
⟧
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho two.phi
40-45-00-00-00-00-00-00
$ phino morph --symbolic=atoms.yaml --locator=Q.φ --sweet --hide-rho two.phi
⟦ x ↦ 7.0, λ ⤍ L_number_plus ⟧

The inner 5.plus( 6 ) fires, because .plus is dispatched on its result, while the outer call is left for dataization. Where no formation is reachable, morph prints ⊥. It fails on a term that is not a normal form. It takes every option of dataize.

Acyclic morphing

phino stops no recursion by itself, so a run that never ends fails once --max-steps runs out, with Morphing did not finish before reaching the limit of steps: --max-steps=<n>. The --acyclic=<mode> option makes the run notice a loop instead. When a reduction is about to enter a formation it is already inside, the run answers a copy of an object binding φ with a fresh symbol and goes on, and stops at any other formation and leaves the term in place, as --partial does. The mode says when two formations are the same:

• proven means equal up to a renaming of symbols;
• plausible also means that the later one holds the earlier one under wrappers it gained, such as a growing accumulator, so it may cut a recursion that would have stopped.

Under plausible, a formation is fired only once, and a later firing of it takes the answer of the first one. The --max-loops=<n> option lets a reduction enter such a formation n more times before it is cut. dataize takes --acyclic too, and fails on a term left in place unless --partial is given, since such a term holds no data to print.

Protocol

The --protocol option writes every λ function the run fired into a file, as a tree in XML, for a program to read. The --minutes option writes the same tree as indented text, and one run may take both. Here, L_down answers with a call of its own object over a fresh symbol, so without --acyclic the run would go on until --max-steps runs out:

$ cat down.yaml
- λ: L_down
  dataize:
    𝛿1: $.x
  𝑛: Φ.down( x ↦ ⟦ λ ⤍ 𝜎 ⟧ )
$ cat down.phi
⟦
  down ↦ ⟦ x ↦ ∅, λ ⤍ L_down ⟧,
  y ↦ Φ.down( x ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).φ
⟧
$ phino morph --symbolic=down.yaml --locator=Q.y --acyclic=proven \
    --minutes=down.txt --sweet --hide-rho down.phi
⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧.φ
$ cat down.txt
𝕄(Φ.y):
  remembered 𝑛·0·1 ≡ Φ.down  # ⟦ x ↦ ∅, λ ⤍ L_down ⟧
  𝑛·0·2 := Φ.down( x ↦ 𝜎1:λ )
  𝑛·0·3 := ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧
  remembered 𝑛·0·3 ≡ 𝑛·0·1( x ↦ 𝜎1:λ )
  𝔼(L_down):
    𝔻(ξ.x):
      𝛿·1·1 := 𝔻(𝜎1:λ)
    𝛿1·1 := 𝛿·1·1  # 𝔻(ξ.x)
    𝑛·1·1 := Φ.down( x ↦ 𝜎2:λ )  # 𝑛
    𝕄(𝑛·1·1):
      𝑛·1·2 := Φ.down( x ↦ 𝜎2:λ )
      𝑛·1·3 := ⟦ x ↦ 𝜎2:λ, λ ⤍ L_down ⟧
      remembered 𝑛·1·3 ≡ 𝑛·0·1( x ↦ 𝜎2:λ )
      morphed 𝑛·1·4 := 𝑛·1·3
    𝑛·1·5 := 𝑛·1·3  # 𝕄(𝑛·1·1)
    remembered 𝑛·1·3 ≡ 𝑛·0·3
  looped 𝑛·0·3  # proven

In a name such as 𝑛·1·2, the first number counts the firings, 0 outside every firing, and the second counts the names within that firing. The name 𝛿1·1 is the meta 𝛿1 of the first firing. A protocol may hold these lines:

• # … lines open the file with the phino that wrote it, the command, the world, the λ functions, the locator, and the expression it points at.
• 𝔻(…): and 𝕄(…): open a block where dataization or morphing starts at a new site, and what it does stands under it.
• 𝔼(…): opens one firing, named by its λ function.
• 𝑛·0·1 := … names an application, and the line after it names the object the application made.
• 𝛿1·1 := … binds a meta of the entry, and the comment names the judgment and the term it came from.
• 𝑛·1·1 := … # 𝑛 is the term the entry answered with, and the line commented with 𝕄(𝑛·1·1) is its normal form.
• boxed … is dataization stepping into the φ of a formation.
• undressed … is an undress line taking the φ of a formation.
• 𝛿·1·1 := … closes a 𝔻 block with the data it found, or with 𝔻(𝜎1:λ) where it came down to a symbol.
• morphed … closes a 𝕄 block with the term it came to.
• joined …, fabricated …, diverged … and unripe … are what a join made of its two sides, or why it could not join them.
• deferred … and symbolized … are the symbols a defer or a symbolize line minted.
• cast … binds a meta to the copy a cast block made of a bare symbol, and the comment names the meta it read and the meta whose shape it took.
• unanswered … is a λ name no entry answers.
• stuck … closes a firing that got stuck, and stall … stands under one that --acyclic=plausible answered with an earlier stall.
• remembered 𝑛·0·1 ≡ Φ.down is a fact the run keeps: the term on the left came from the one on the right, a path or a call of the world, or a formation it was the answer of.
• memoized 𝑛·0·5 ⇛ 𝑛·1·9 is what --acyclic=plausible keeps: the formation on the left fired to the term on the right.
• recalled 𝑛·0·3 ⇒ 𝑛·0·1( x ↦ ⟦⟧ ) is a fact or a memo entry used again, spelled as its remembered or memoized line spelled it.
• looped … is where --acyclic cut a loop, and looped 𝜎1 := … names the call of the object it answered with that symbol, when a fact names it.
• starved …, spent …, timeout …, oversized … and blown … are where --max-steps, --max-firings, --max-seconds, --max-nodes and --max-memory ran out.
• msec …, firings … and fps … close the file, and the listing above leaves them and the # … lines out, since they differ from run to run.

The --abridged option folds every formation longer than sixty-four characters, or than --abridged=WIDTH, into its φ, Δ and λ and a count of the rest. The --abridged-data option also cuts every byte string longer than eight bytes down to its first two bytes and its last two.

Rewrite

You can rewrite this expression with the help of rules defined in the my-rule.yml YAML file (here, the !d1 and !B1 are capturing groups, similar to regular expressions):

name: My custom rule
pattern: ⟦ Δ ⤍ !d1, !B1 ⟧
result: ⟦ Δ ⤍ 62-79-65, !B1 ⟧

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, alone or together with your own rules:

phino rewrite --normalize --rule=my-rule.yaml hello.phi

Some rules mint fresh names with the random-string function, and --seed picks the seed of its random generator, 0 by default.

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.io.stdout("hello") ]]' | phino rewrite
⟦
  φ ↦ Φ.io.stdout( α0 ↦ Φ.string( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 68-65-6C-6C-6F ⟧ ) ) )
⟧

The two styles may be mixed in one expression, unless --monoform is given.

A formation of a single binding may be written as its asset, a colon, and the attribute the asset is bound to:

⟦ Δ ⤍ FF-AA ⟧    = FF-AA:Δ    = FF-AA:D
⟦ λ ⤍ 𝜎1 ⟧       = 𝜎1:λ       = !S1:L
⟦ a ↦ ∅ ⟧        = ∅:a        = ?:a
⟦ φ ↦ ξ.a ⟧      = ξ.a:φ      = $.a:@

The colon binds as tightly as a dot, so ξ.a:φ.b is ⟦ φ ↦ ξ.a ⟧.b. With --sweet, phino prints every such formation this way.

A formation has a receiver ρ only when it declares one among its voids, the way EO declares ^, as in ⟦ ρ ↦ ∅, t ↦ ξ.ρ.k ⟧. phino adds none of its own, so ξ.ρ in a formation that declares none is ⊥.

Merge

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

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

Match

You can test the 𝜑-expression 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

Compile

By default, phino reads its rules from YAML and interprets them at every step. The compile command turns the built-in rules of normalization, contextualization, morphing and dataization, and every --rule file, into the Haskell module compiled/generated/Compiled.hs, and a second build links it in:

phino compile
cabal build all

The build links the module in only when the Cabal flag compiled is on. If there is no cabal.project.local, compile creates one that turns the flag on, and otherwise it prints the lines to add to it. The compiled rules take exactly the same steps as the YAML ones. compile refuses a rule it cannot turn into Haskell and names the reason. A binary built this way refuses to run once the built-in rules changed after the last compile. To test the whole suite against the compiled rules, run make compiled.

Explain

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

phino explain --normalize

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

Rule structure

This is BNF-like yaml rule structure. Here types ended with apostrophe, like Attribute' are built types from 𝜑-expression 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
  | eq:                  # compare two comparable objects
      - Comparable
      - Comparable
  | in:                  # returns True if every given attribute exists in
      - Attribute' | [Attribute'] # the union of the given bindings
      - Binding' | [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'
  | formation:           # returns True if given expression is a formation
      Expression'        # (an abstraction ⟦…⟧); used by morphing 'md'
                         # as 'not (formation 𝑛)', so a non-formation head is
                         # morphed and a formation head is left to 'ml'
  | gt:                  # returns True if the first comparable object is
      - Comparable       # greater than the second one
      - Comparable
  | disjoint:            # returns True if none of the given attributes exists
      - [Attribute']     # in the given bindings
      - Binding'

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

Number:                  # comparable number
  = Integer              # just regular integer
  | IndexMeta'           # 𝑖 (or !i), the index captured by an α𝑖 argument
  | length: BiMeta'      # calculate length of bindings by given meta binding
  | domain: BiMeta'      # calculate number of unique attributes in given
                         # meta binding (excluding 'assets')

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'           # !t

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 an attribute with a random unique name. It accepts no arguments; uniqueness is guaranteed across all names already taken in the document.
• 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. In the replacement, \\1 to \\9, as well as $1, put what a group of the pattern matched, e.g. s/([0-9]+)/\\1!/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.

Meta variables

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

This is the list of supported meta variables:

• !t || 𝜏 - attribute
• !i || 𝑖 - the index of a positional (α) application argument, captured by writing α𝑖 (or ~!i)
• !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
• !F || 𝑓 - function name in meta lambda binding
• !S || 𝜎 - a symbol standing where a λ name stands (see Symbolic λ functions). It is spelled the way a meta variable is spelled but is a name and no capture: 𝜎1 is one concrete symbol, which no substitution ever binds, and a bare 𝜎 in the answer of a --symbolic entry asks for a fresh one

A meta variable carries a suffix, like !B1 or 𝜏2, to name what it captured, so that the result, when, where and having of a rule can read it back. A suffix starts with one, so !B0 is refused. Without a suffix, a meta variable is anonymous: it matches any term on its own, binds no name, and is refused anywhere but in a pattern, so ⟦ 𝜏 ↦ 𝑒, 𝜏 ↦ 𝑒 ⟧ matches any two attributes.

A positional (α) application argument is written as α0, ~0 (ASCII), or α𝑖/~!i when its index is captured by an !i/𝑖 meta variable.

Benchmark

To run performance benchmarks, you need Java 8+ and curl:

make bench

On the first run, make bench downloads the compiled Native class of JNA, turns it into XMIR with jeo-maven-plugin and then into 𝜑, and caches the results in benchmark/tmp/. Besides parsing, printing and rewriting that class, the suite morphs the entries of benchmark/demo.phi symbolically, one case per entry.

=== parse/phi ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      2471508.678 μs
  avg:        247150.868 μs
  min:        221146.358 μs
  max:        280070.951 μs
  std dev:    22173.343 μs
=== parse/xmir ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      9900009.942 μs
  avg:        990000.994 μs
  min:        913216.401 μs
  max:        1064034.163 μs
  std dev:    51646.433 μs
=== rewrite/normalize ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      20.277 μs
  avg:        2.028 μs
  min:        1.763 μs
  max:        2.444 μs
  std dev:    0.206 μs
=== print/sweet/multiline ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      5893919.071 μs
  avg:        589391.907 μs
  min:        546710.930 μs
  max:        622324.691 μs
  std dev:    22402.952 μs
=== print/sweet/flat ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      745153.374 μs
  avg:        74515.337 μs
  min:        64906.612 μs
  max:        87781.583 μs
  std dev:    10272.240 μs
=== print/salty/multiline ===
  warmup:     3 iterations
  batches:    10 x 1
  total:      18806006.234 μs
  avg:        1880600.623 μs
  min:        1829320.397 μs
  max:        1936784.646 μs
  std dev:    32771.969 μs
=== morph/symbolic/demo/e1 ===
  warmup:     3 iterations
  batches:    10 x 9
  total:      12166.226 μs
  avg:        135.180 μs
  min:        131.121 μs
  max:        144.901 μs
  std dev:    3.769 μs
=== morph/symbolic/demo/e2 ===
  warmup:     3 iterations
  batches:    10 x 129
  total:      173694.366 μs
  avg:        134.647 μs
  min:        133.356 μs
  max:        136.014 μs
  std dev:    0.741 μs
=== morph/symbolic/demo/e3 ===
  warmup:     3 iterations
  batches:    10 x 129
  total:      178632.645 μs
  avg:        138.475 μs
  min:        133.065 μs
  max:        163.122 μs
  std dev:    9.065 μs
=== morph/symbolic/demo/e4 ===
  warmup:     3 iterations
  batches:    10 x 113
  total:      158155.239 μs
  avg:        139.960 μs
  min:        133.878 μs
  max:        168.699 μs
  std dev:    10.055 μs
=== morph/symbolic/demo/e5 ===
  warmup:     3 iterations
  batches:    10 x 126
  total:      172774.638 μs
  avg:        137.123 μs
  min:        136.318 μs
  max:        138.811 μs
  std dev:    0.767 μs
=== morph/symbolic/native/e5 ===
  warmup:     3 iterations
  batches:    10 x 4
  total:      53810.789 μs
  avg:        1345.270 μs
  min:        1165.754 μs
  max:        2105.284 μs
  std dev:    261.412 μs
=== morph/symbolic/accum/0 ===
  warmup:     3 iterations
  batches:    10 x 76
  total:      85572.821 μs
  avg:        112.596 μs
  min:        111.501 μs
  max:        114.714 μs
  std dev:    1.060 μs
=== morph/symbolic/accum/400 ===
  warmup:     3 iterations
  batches:    10 x 65
  total:      85508.304 μs
  avg:        131.551 μs
  min:        131.274 μs
  max:        131.842 μs
  std dev:    0.180 μs

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

How to Contribute

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

To build a phino executable into the root of the repository, run:

make phino

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