phino-0.0.141: README.md
<!--
SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
SPDX-License-Identifier: MIT
-->
# Command-Line Manipulator of π-Calculus Expressions
[](https://www.rultor.com/p/objectionary/phino)
[](http://hackage.haskell.org/package/phino)
[](https://github.com/objectionary/phino/actions/workflows/cabal.yml)
[](https://github.com/objectionary/phino/actions/workflows/stack.yml)
[](https://app.codecov.io/gh/objectionary/phino)
[](https://objectionary.github.io/phino/)
[](LICENSES/MIT.txt)
[](https://hitsofcode.com/github/objectionary/phino/view?branch=master&label=Hits-of-Code)
[](https://www.0pdd.com/p?name=objectionary/phino)
This is a command-line normalizer, rewriter, and dataizer
of [π-calculus](https://www.eolang.org) expressions.
First, you write a simple [π-calculus](https://www.eolang.org) expression
in the `hello.phi` file:
```text
β¦ Ο β¦ β¦ Ξ β€ 68-65-6C-6C-6F β§, t β¦ ΞΎ.k, k β¦ β¦β§ β§
```
## Installation
Then you can install `phino` in two ways:
Install [Cabal][cabal] first and then:
```bash
cabal update
cabal install --overwrite-policy=always phino-0.0.140
phino --version
```
Or download binary from the internet using [curl](https://curl.se/) or
[wget](https://en.wikipedia.org/wiki/Wget):
```bash
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>
## Build
To build `phino` from source, clone this repository:
```bash
git clone git@github.com:objectionary/phino.git
cd phino
```
Then, run the following command (ensure you have [Cabal][cabal] installed):
```bash
cabal build all
```
Next, run this command to install `phino` system-wide:
```bash
sudo cp "$(cabal list-bin phino)" /usr/local/bin/phino
```
Verify that `phino` is installed correctly:
```bash
$ 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:
```bash
phino --pin=0.0.0.67 dataize hello.phi
```
The `--pin-file` global option does the same, but reads the version from
a file, ignoring the whitespace around it:
```bash
phino --pin-file=version.txt dataize hello.phi
```
## Dataize
Then, you dataize the expression:
```bash
$ phino dataize hello.phi
68-65-6C-6C-6F
```
### Symbolic Ξ» functions
Which Ξ» functions exist is a property of the object model being dataized, not
of the calculus, so `phino` implements none of them. They come from a YAML file
given with `--symbolic`, one entry per Ξ» function:
```yaml
- Ξ»: L_number_(plus|times)
dataize:
πΏ1: $.Ο
πΏ2: $.x
π: Ξ¦.number( Ο β¦ β¦ Ξ» β€ π β§ )
```
The `Ξ»` of an entry is the Ξ» names it answers for, as a regular expression, so
the one above stands for `L_number_plus` and `L_number_times`. Under `dataize`
stand the operands it brings down to data through π», each binding a bytes meta
`πΏ1`, `πΏ2` and so on; under `morph` the operands it reduces to a normal
form through π, each binding an expression meta `π1`, `π2`. Both blocks are
terms of the calculus, read against the formation being fired, so `ΞΎ` is that
formation and `$.x` its `x`, while `Ξ¦` is the universe. Every entry numbers its
own metas from `πΏ1` and `π1`, and the entry is what tells two `πΏ1` apart.
The term under `π` is what the firing answers with. `phino` normalizes it
exactly as it normalizes anything else, so `--protocol`, `--partial` and
`--max-steps` work on it unchanged. It may name any meta the entry bound,
those of the two blocks below among them.
### Rewriting a term into another shape
There is a third block, `rewrite`, and it reduces nothing. Each line of it
takes a term another meta of the entry is already bound to, named under `of`,
applies a list of ordinary rules to it, spelled with the very `pattern`,
`result`, `when` and meta variables a rule file uses, and binds an expression
meta of its own to the outcome:
```yaml
- Ξ»: L_fork
dataize:
πΏ1: $.Ο
morph:
π1: $.left
π2: $.right
rewrite:
π3:
of: π1
rules: &bool
- name: false-literal
pattern: >-
β¦ !B1, Ο β¦ Ξ¦.bool( if β¦ β¦ Ο β¦ β
, left β¦ β
, right β¦ β
,
Ο β¦ ΞΎ.right β§ ), !B2 β§
result: >-
β¦ Ο β¦ Ξ¦.bool( if β¦ β¦ Ξ» β€ L_fork, left β¦ β
, right β¦ β
,
Ο β¦ β¦ Ξ β€ 00- β§ β§ ) β§
π4:
of: π2
rules: *bool
π: π3
```
The meta under `of` is one bound by `morph` or by a `rewrite` line above it,
and nothing else. A rule is tried at every position of the term, the outermost
first; the first rule whose pattern matches a position rewrites it, and a
rewritten position is not walked into again, so a rule whose result carries
its own pattern never loops. Nothing is normalized afterwards: a rewrite is a
substitution the entry vouches for and not a reduction, exactly as an answer
is. A rule writing a `π` into its result, or reading a meta its pattern never
binds, is refused where the file is read.
This is how a program brings two branches of a fork to one shape before they
are compared. In EO a `Ξ¦.false` is written `Ο β¦ ΞΎ.right` while a bool a firing
answered carries a symbol, and the two are one value in two spellings that
only the program knows to be one. The block runs before `symbolize` on purpose:
a result may write the datum a literal stands for, as `β¦ Ξ β€ 00- β§` above, and
that datum is then stood into a known symbol the join can pair.
### Standing data into unknowns
There is a fourth block, `symbolize`, and it reduces nothing. It takes a term
another meta of the entry is already bound to and binds an expression meta of
its own to that same term with every datum in it standing for an unknown:
```yaml
- Ξ»: L_fork
dataize:
πΏ1: $.Ο
morph:
π1: $.left
π2: $.right
symbolize:
π3: π1
π4: π2
π: π3
```
The right-hand side of a line names a meta bound by `morph`, by `rewrite` or by
a `symbolize` line above it, and nothing else; a term nobody reduced has no data
to stand. Every `Ξ β€ b` binding of that term becomes a `Ξ» β€ πk` naming a
fresh symbol, one per occurrence, so `β¦ Ξ β€ b β§` reads as `β¦ Ξ» β€ πk β§` and a
literal tuple gets several. A term carrying no datum passes through as it was.
Only the `Ο` chain is walked. A term carries the value it stands for where
that chain ends, so a datum standing anywhere else says nothing about the term
and is left alone, the whole subtree of it. What sits under `Ο` belongs to the
object around this one, and a normal form drags the universe it was reduced
inside along under `Ο`, so a walk reaching into it would stand the data of the
whole program into unknowns to say one thing about one term. What sits under a
method is code and not data: the `-1` of a `neg β¦ β¦ Ο β¦ ΞΎ.Ο.times( -1 ) β§`
nobody has called is the body of a method, and minting a symbol for it, and for
every other literal every method of the carrier declares, would write unknowns
nobody ever reads.
This is what lets an entry compare two branches of a fork. A literal is sugar
for `Ξ¦.number( Ξ¦.bytes( β¦ Ξ β€ β¦ β§ ) )`, so a branch computed from a literal
keeps a datum three levels down where a branch computed from an unknown keeps
`β¦ Ξ» β€ π β§`. A `Ξ` against a `Ξ»` is a difference in kind and not in value, and
after the stage both branches carry `β¦ Ξ» β€ π β§` where they differ.
### Joining the branches of a fork
A branching Ξ» function answers neither of its branches. Which one the program
takes is decided by a value nobody worked out, so handing one of them through
would drop the branch point from the program altogether and a reader would see
the condition computed and thrown away. `join` is the fifth block, and it
reduces nothing either: it takes two metas the entry has bound already and
binds one of its own to the two terms joined into one.
```yaml
- Ξ»: L_fork
dataize:
πΏ1: $.Ο
morph:
π1: $.left
π2: $.right
symbolize:
π3: π1
π4: π2
join:
π5: [π3, π4]
π: π5
```
A line names two metas bound by `morph`, by `rewrite`, by `symbolize` or by a
`join` line above it, and never three: it stands for a choice between two
branches, and a walk over three terms in parallel is no such choice. The meta it
binds is one like any other, so the answer may name it alone, as above, or stand
it inside a larger term.
`phino` takes the two terms and requires them to match verbatim, with one
exception: where `β¦ Ξ» β€ πA β§` in one meets a different `β¦ Ξ» β€ πB β§` in the
other, it mints a fresh `πC` and stands it there. The same symbol on both sides
stays as it is, and the same pair met again further down gets the same fresh
symbol, since it is one choice however often the two terms differ by it; two
different pairs get two fresh symbols. Two identical terms join into that same
term and nothing is minted at all. The join keeps the type by construction,
being the terms' own shape, so the file needs to know nothing about carriers.
Only the `Ο` chain is compared, exactly as `symbolize` stands only that chain
into unknowns: a term carries the value it stands for where its `Ο` chain ends,
so every other binding is taken from the first branch, the whole subtree of it,
and never compared at all. The two branches of a fork reach their normal forms
in scopes of their own, so their `Ο` differ wherever the reduction left a
trace, and comparing them would refuse the join over something saying nothing
about either branch; a method is the same, its body being code nobody has
called, so two branches differing inside one are not two values. The joined
term keeps the methods and the `Ο` of the first of the two, being of its shape,
which is what lets the program go on dispatching on what the fork answered.
A join is only ever between two expressions and a datum is never joined with
anything, which is why `symbolize` runs before it: a known symbol, one that
stage minted for a datum, is a symbol like any other here, so a literal branch
joins with a computed one and two literal branches join too. Any other
difference β a datum against a symbol, two different data, a binding one term
carries and the other does not β is no join at all, and the firing gets stuck
the way a Ξ» function no entry answers does, so `--partial` parks it rather than
aborting the run. A fork whose branches differ in structure, such as a `Ξ¦.true`
and a `Ξ¦.false` written as `Ο β¦ ΞΎ.left` against `Ο β¦ ΞΎ.right`, is stuck, and
bringing two such branches to one shape is the program's job and not `phino`'s,
which its entry does in a `rewrite` block.
One term being `β₯` is the exception, since `if. cond value β₯` is how EO spells
"raise unless `cond`": the program raises on that side of the condition and
has a perfectly good value on the other. The join then mints nothing, binds
its meta to the other term as it stands and writes on which side the program
raises, naming the condition by what the first `dataize` operand of the entry
came down to, as `terminate(π»(π2:Ξ»), right) # π4` in the text format and
`<terminate symbol="π2" branch="right"/>` in the markup. The deep walk fires
such a fork too, since that `β₯` is an argument the program wrote rather than
one the reduction made.
Every symbol a join mints is written into the protocol as a fact of its own,
so a reader ties it to the two it stands for without diffing the terms; the
section on `--protocol` below shows one.
### Symbols
An entry answers, it never computes. The job of these functions is symbolic
morphing: what `5.plus( 6 )` comes to is the arithmetic of the object model and
not `phino`'s, so an entry answers a term carrying a symbol standing for a
value nobody worked out, and the data its `dataize` operands came down to is
not its to read. An answer mentioning a `πΏ` is refused where the file is read.
`π` is a meta of the calculus, beside `π`, `πΏ` and `π`, and it stands where
a Ξ» name stands. In a term, `π1` is a concrete symbol: a Ξ» function nothing
answers, which is what makes the value the term carries unknown. Firing it is
therefore the same question as firing a Ξ» name the `--symbolic` file does not
carry, and gets the same answer: πΌ stops there, the protocol records the site as
`?(π1)`, and `--partial` leaves the term where it stands. Dispatching an
attribute off a symbol β `β¦ Ξ» β€ π1 β§.plus( 5 )` β therefore taints its own
binding and nothing else; what stands beside it still computes. In an answer, a
bare `π` asks for a fresh one, minted as the firing happens and numbered by the
run, so no two unknowns are ever spelled alike. Minting starts after the symbols
the program already carries, so a run over the π-program an earlier run wrote
never spells a fresh symbol like one already standing there.
Dataizing a symbol never gets stuck. It answers a fixed datum, 42
(`40-45-00-00-00-00-00-00`), the same one for every symbol, so π» always
answers, a `πΏ` always holds concrete data and no firing ever declines for the
lack of it:
```bash
$ 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
```
### The keys of the file
Each `Ξ»` is a regular expression, and it must match the whole Ξ» name, so a
plain name such as `L_number_plus` means that one function and nothing else,
while `L_number_.*` stands for every function of `number`. The keys are unique:
nothing tells two entries under one key apart, so a second entry under a key is
unreachable and the file is refused rather than merely redundant.
A Ξ» name no key matches has no Ξ» function at all, so πΌ gets stuck on it.
Without `--symbolic` there is no entry at all and every Ξ» function gets stuck:
```bash
$ phino dataize --sweet --hide-rho sum.phi
[ERROR]: No entry of --symbolic answers the Ξ» function 'L_number_plus'
```
The file is read before anything is parsed or reduced, so a key that is no
regular expression, an operand that is no meta of the kind its block binds, or
an answer the calculus cannot read fails the run up front rather than half-way
through a derivation.
### Recording what fired
Every Ξ» function fired on the way to the answer may be recorded in a
machine-readable protocol, with the `--protocol` option. The protocol is a
tree: the run at the top, one block per firing under it, and inside the block
the operands the firing bound and the term it answered with. A formation that
dataization gets into opens a block too, and what fires inside it stands under
it.
<!-- markdownlint-disable MD013 -->
```bash
$ phino dataize --symbolic=atoms.yaml --protocol=atoms.txt --quiet \
--sweet --hide-rho sum.phi
$ cat atoms.txt
π»(Ξ¦)
formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6 ) β§) # π»(Ξ¦)
πΌ(L_number_plus) # π»(Ξ¦)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ» β§) # π»(Ξ¦.aπ΅0)
formation(40-14-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅0)
πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ» β§) # π»(Ξ¦.aπ΅1)
formation(40-18-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅1)
πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)
π.1.1 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π
π.1.2 := β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ» β§ # π(π.1.1)
formation(β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ» β§) # π»(Ξ¦)
```
<!-- markdownlint-enable MD013 -->
`π»(β¦)` is the run and the term it was aimed at, `π(β¦)` where the run is a
morphing, and `πΌ(β¦)` is one firing, named by the entry that answered it and
commented with the judgment that asked for it and the site it was fired at.
Every comment of the file is of that shape: a judgment applied to a term, which
is the intent the value beside it came from. The firings are numbered across the
whole run, in the order they open, so `πΏ1.2` is the value bound to `πΏ1` by
the second firing of the run, whichever Ξ» function that was, `π1.2` the same
for a `morph` meta, and `π.3.2` the answer of the third firing, so
`π1.2 := π.3.2` reads "the `π1` of this firing is what the third firing
answered". One firing binds a meta once and no two firings
share a number, so every one of these names stands on exactly one line of the
file and a line naming another one points at it and no other.
`formation(β¦)` is a formation π» got into through its `box` rule, which
dataizes the `Ο` of a formation carrying neither `Ξ` nor `Ξ»`. It is commented
with `π»` and the site it was entered at, the way a firing is, and what the `Ο`
body does stands one level deeper under it: the firings its dataization
demands, and the formations it gets into in turn. A reader therefore sees which
object a firing was made on the way into, rather than a flat list of firings.
Only `box` writes one, since π stops at a formation without getting into it
and a formation whose Ξ» is fired is already an `πΌ(β¦)` block. The line is no
firing: it binds no meta and takes no number, so the metas of the firings under
it are numbered as if it were not there. In the run above π» gets into the
program itself, since `Ξ¦` binds `Ο`; then into each number the entry brings
down, and through its `Ο` into the bytes that number holds; and last into the
number the entry answered, whose `Ο` is the symbol `π1`, so nothing fires under
that one.
An answer stands on two lines and not one. A firing answers the term its entry
wrote and `phino` morphs that term before standing it back into the program, so
`π.1.1` is what the entry wrote, with the symbols this firing minted already in
it, commented with `π` to name the key it was read from, and `π.1.2` is the
normal form π made of it, commented with `π(π.1.1)` to say where it came from.
It is the same morphing every other term goes through, and writing only its
outcome would have the formation of `number` appear in place of the three
tokens the entry wrote with nothing saying why. Whatever that morphing fires
opens its own block between the two lines, exactly where a firing an operand
took opens one, so the order the lines come in is the order the work was done
in.
Where an operand came down to the datum a symbol stands for, the protocol writes
`π»(π1:Ξ»)` in place of that 42 (`π1:Ξ»` is the formation `β¦ Ξ» β€ π1 β§`, in the
sugar every sweet term is written with), so a reader sees that the value was
manufactured rather than read out of the program. A `π` is the name of a Ξ»
function and no term of its own, so π» is applied to the formation carrying it
and never to the name alone.
A `symbolize` line writes a line per fresh symbol it minted, ahead of the line
binding the term that carries them, and that line is a fact and no assignment:
`π»(π44:Ξ») == 3F-F0-00-00-00-00-00-00` says that dataizing the formation
`π44` names answers those bytes. Nothing binds bytes to a `π`, since it is
neither a datum nor a term. A consumer reading the protocol back treats a
symbol with such a fact as a constant and every other symbol as an unknown.
The line binding the term of a `symbolize` one is commented with the meta it
was told to stand, `π3.1 := β¦ Ξ» β€ π8 β§ # π1`, and with no judgment
around it: standing the data of a term into unknowns is the file's own
operation and nothing of the calculus runs there, so the line names a meta of
the entry the way a `join` line names the two it joined. A comment carries the
letter of a judgment exactly where a judgment made the value.
The site of a firing is a locator, written as a comment the way an operand
line writes the term it came from, under the letter of the judgment that asked
for the firing: πΌ is fired by the `ml` rule of morphing and by the `fire` rule
of dataization, so `π(Ξ¦.demo.a.Ο)` is a Ξ» function fired while π was reducing
that binding and `π»(Ξ¦)` one fired because dataization demanded data of `Ξ¦`.
A chain such as `5.plus( 6 ).plus( 7 )` writes both: the inner call is fired
while π reduces the head of the outer dispatch, the outer one because π» asked
for the data. The site itself is where in the program the firing
belongs: the term the run was aimed at, so `Ξ¦` for a run that was aimed at
nothing in particular, and, under `--deep`, the binding the walk had entered
when the Ξ» function fired, since that walk reduces every part of the program
in turn and one entry answers the same way wherever it is fired. A locator
names a binding and reaches no further, so a firing standing deeper inside a
term than that β under a dispatch, or in the argument of an application β is
written under the last binding the walk entered, which is the smallest part of
the program a reader can aim a run of their own at. An operand of a firing is
reduced bound to a synthetic attribute of the universe (see `--inside` below),
so a Ξ» function fired while it came down is written under that attribute and
not under the site of the firing that asked for it.
An operand line ends in the judgment that reduced it and the term it was
reduced from, written as a comment after two spaces and `#`. The value alone
says what the meta was bound to and neither what it was bound from nor what
was done to it, so `πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)` reads "the
`πΏ1` of this firing is the `Ο` of the formation brought down through π», and
it came down to 20", where a `morph` operand reads `π1.5 := π.3.2 # π(ΞΎ.then)`
and says that the `then` of the formation reached its normal form through π.
Which of the two judgments ran is the whole difference between a line ending
in data and one ending in a term. It is the very term the entry wrote under
that meta, spelled the way the calculus reads it β `$` is read as `ΞΎ` β so a
reader never has to open the `--symbolic` file beside the protocol and match
every line by Ξ» name and meta number.
`?(β¦)` is a Ξ» name no entry answers, standing where the block of its firing
would have stood. Nothing fired, so nothing opens under it. The line is
commented with the judgment that asked and the formation it was asking about,
`π(L_none:Ξ»)`, the way an operand line is commented with the term it was
reduced from: πΌ is fired by the `ml` rule of morphing and by the `fire` rule
of dataization, so the letter says where in the reduction the site stands and
the term says which object the Ξ» function that could not fire belongs to. It
is written
whether or not `--partial` goes on to park the run, since the protocol records
what πΌ was asked for, and a question it could not answer belongs there as much
as one it could β once per site and not once per attempt, since a site
`--partial` parks stays in the residue and `--deep` walks over it again:
<!-- markdownlint-disable MD013 -->
```bash
$ phino dataize --symbolic=atoms.yaml --protocol=atoms.txt --quiet \
--sweet --hide-rho stuck.phi
[ERROR]: No entry of --symbolic answers the Ξ» function 'L_number_nope'
$ cat atoms.txt
π»(Ξ¦)
formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§, Ο β¦ 5.plus( 6 ).nope β§) # π»(Ξ¦)
πΌ(L_number_plus) # π(Ξ¦)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§) # π»(Ξ¦.aπ΅0)
formation(40-14-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅0)
πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§) # π»(Ξ¦.aπ΅1)
formation(40-18-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅1)
πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)
π.1.1 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π
π.1.2 := β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§ # π(π.1.1)
?(L_number_nope) # π»(L_number_nope:Ξ»)
```
<!-- markdownlint-enable MD013 -->
The very same file comes back with `--partial`, where the run answers the
residue instead of failing: what `phino` could not decide is a property of the
program and not of the option that decides what to do about it.
Every term is π on a single line, whatever `--output` and `--flat` say about
the result of the run, so a program reading the protocol back never has to know
what the run printed. The file is truncated at the beginning of every run, so
it always holds the firings of exactly one run.
The blocks come in the order the reduction walks the term, and that order is
not what the dependencies are read from β the symbols are. Take a comparison
nobody can decide, a fork branching on it, and an `atoms.yaml` of three
entries, the Ξ» functions named briefly to keep the lines below short:
```yaml
- Ξ»: L_plus
dataize:
πΏ1: $.Ο
πΏ2: $.x
π: Ξ¦.number( Ο β¦ β¦ Ξ» β€ π β§ )
- Ξ»: L_gt
dataize:
πΏ1: $.Ο
πΏ2: $.x
π: Ξ¦.bool( if β¦ β¦ Ξ» β€ L_fork, then β¦ β
, else β¦ β
, Ο β¦ β¦ Ξ» β€ π β§ β§ )
- Ξ»: L_fork
dataize:
πΏ1: $.Ο
morph:
π1: $.then
π2: $.else
join:
π3: [π1, π2]
π: π3
```
<!-- markdownlint-disable MD013 -->
```bash
$ cat fork.phi
β¦
bytes β¦ β¦ Ο β¦ β
β§,
bool β¦ β¦ if β¦ β
β§,
number β¦ β¦ Ο β¦ β
, plus(Ο, x) β¦ β¦ Ξ» β€ L_plus β§, gt(Ο, x) β¦ β¦ Ξ» β€ L_gt β§ β§,
foo(x) β¦ β¦
Ο β¦ ΞΎ.x.gt( 0 ).if( ΞΎ.x.plus( ΞΎ.x.plus( 1 ) ), ΞΎ.x.plus( ΞΎ.x ) ).plus( 5 )
β§,
demo β¦ β¦ a β¦ Ξ¦.foo( Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) ) β§
β§
$ phino morph --deep --symbolic=atoms.yaml --locator=Q.demo.a \
--protocol=fork.txt --quiet --sweet --hide-rho fork.phi
$ cat fork.txt
π(Ξ¦.demo.a)
πΌ(L_gt) # π(Ξ¦.demo.a.Ο)
formation(β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅0)
πΏ1.1 := π»(π1:Ξ») # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 00-00-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅1)
formation(00-00-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅1)
πΏ2.1 := 00-00-00-00-00-00-00-00 # π»(ΞΎ.x)
π.1.1 := Ξ¦.bool( if(then, else) β¦ β¦ Ξ» β€ L_fork, Ο β¦ π2:Ξ» β§ ) # π
π.1.2 := β¦ if(then, else) β¦ β¦ Ξ» β€ L_fork, Ο β¦ π2:Ξ» β§ β§ # π(π.1.1)
πΌ(L_plus) # π(Ξ¦.demo.a.Ο)
formation(β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅2)
πΏ1.2 := π»(π1:Ξ») # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 3F-F0-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅3)
formation(3F-F0-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅3)
πΏ2.2 := 3F-F0-00-00-00-00-00-00 # π»(ΞΎ.x)
π.2.1 := Ξ¦.number( Ο β¦ π3:Ξ» ) # π
π.2.2 := β¦ Ο β¦ π3:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§ # π(π.2.1)
πΌ(L_plus) # π(Ξ¦.demo.a.Ο)
formation(β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅4)
πΏ1.3 := π»(π1:Ξ») # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ π3:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅5)
πΏ2.3 := π»(π3:Ξ») # π»(ΞΎ.x)
π.3.1 := Ξ¦.number( Ο β¦ π4:Ξ» ) # π
π.3.2 := β¦ Ο β¦ π4:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§ # π(π.3.1)
πΌ(L_plus) # π(Ξ¦.demo.a.Ο)
formation(β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅6)
πΏ1.4 := π»(π1:Ξ») # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅7)
πΏ2.4 := π»(π1:Ξ») # π»(ΞΎ.x)
π.4.1 := Ξ¦.number( Ο β¦ π5:Ξ» ) # π
π.4.2 := β¦ Ο β¦ π5:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§ # π(π.4.1)
πΌ(L_fork) # π(Ξ¦.demo.a.Ο)
πΏ1.5 := π»(π2:Ξ») # π»(ΞΎ.Ο)
π1.5 := π.3.2 # π(ΞΎ.then)
π2.5 := π.4.2 # π(ΞΎ.else)
π»(π6:Ξ») β { π»(π4:Ξ»), π»(π5:Ξ») }
π3.5 := β¦ Ο β¦ π6:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§ # [π1, π2]
π.5.1 := π3.5 # π
π.5.2 := π3.5 # π(π.5.1)
πΌ(L_plus) # π(Ξ¦.demo.a.Ο)
formation(β¦ Ο β¦ π6:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅11)
πΏ1.6 := π»(π6:Ξ») # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§) # π»(Ξ¦.aπ΅12)
formation(40-14-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅12)
πΏ2.6 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.x)
π.6.1 := Ξ¦.number( Ο β¦ π7:Ξ» ) # π
π.6.2 := β¦ Ο β¦ π7:Ξ», plus(x) β¦ L_plus:Ξ», gt(x) β¦ L_gt:Ξ» β§ # π(π.6.1)
```
<!-- markdownlint-enable MD013 -->
`π3` is minted by the second firing and consumed by the third as
`π»(π3:Ξ»)`, and `π2` by the first and consumed by the fork. `π4` and
`π5` are what the two branches came to, and the fork consumes both: its `join`
line makes them one term carrying `π6`, which the `plus( 5 )` standing after
the fork then reads as `π»(π6:Ξ»)`. The line
`π»(π6:Ξ») β { π»(π4:Ξ»), π»(π5:Ξ») }` is what ties the three
together: dataizing the formation `π6` names answers what dataizing one of the
other two answers. A reader who knows the entry knows that `πΏ1` is what decides
between them and that the first of the two belongs to `then`. Nothing is
assigned to a `π`, it being the name of a Ξ» function, so the fact stands on a
line of its own the way what a `symbolize` line knows does, and the line under
it binds the meta, commented with the two metas it joined.
Were the fork to answer one of its branches instead, the value of the other
would be minted and never consumed, and `foo` would read as a program that
computes a condition, computes both branches and then drops the branch point.
All six firings stand under `Ξ¦.demo.a.Ο`, which is as near as a locator gets
to any of them: the walk entered the `Ο` of the formation `Ξ¦.demo.a` morphs to,
and everything under it β the dispatches of the chain, the arguments of `if` β
stands under no attribute of any formation, so the binding the walk had entered
is what the protocol writes them under.
A firing that happened while an operand of another was being reduced stands one
level deeper, under the firing that asked for it. Here it never happens,
because deep morphing reduces both branches where they sit as arguments of
`if`, long before the dispatch that fires the fork.
### The protocol as XML
The name of the file decides which of the two formats `--protocol` writes: a
name ending in `.xml` gets the same tree as markup, every other name gets the
indented text above. There is no option for it, since a caller who asks for a
file called `atoms.xml` and gets text back has been told nothing useful. Here
is the run at the top of this section again:
<!-- markdownlint-disable MD013 -->
```bash
$ phino dataize --symbolic=atoms.yaml --protocol=atoms.xml --quiet \
--sweet --hide-rho sum.phi
$ cat atoms.xml
<?xml version="1.0" encoding="UTF-8"?>
<dataize at="Ξ¦">
<formation at="Ξ¦" term="β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6 ) β§">
<evaluate Ξ»="L_number_plus" by="dataize" at="Ξ¦">
<formation at="Ξ¦.aπ΅0" term="β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ» β§">
<formation at="Ξ¦.aπ΅0" term="40-14-00-00-00-00-00-00:Ξ:Ο">
</formation>
</formation>
<bind meta="πΏ1.1">40-14-00-00-00-00-00-00</bind>
<formation at="Ξ¦.aπ΅1" term="β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ» β§">
<formation at="Ξ¦.aπ΅1" term="40-18-00-00-00-00-00-00:Ξ:Ο">
</formation>
</formation>
<bind meta="πΏ2.1">40-18-00-00-00-00-00-00</bind>
<minted symbol="π1">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>
<built meta="π.1.1">Ξ¦.number( Ο β¦ π1:Ξ» )</built>
<answer meta="π.1.2">β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ» β§</answer>
</evaluate>
<formation at="Ξ¦" term="β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ» β§">
</formation>
</formation>
</dataize>
```
<!-- markdownlint-enable MD013 -->
The root is the run itself, named after the judgment it ran β `<dataize>` for a
π», `<morph>` for a π β with `at` naming the term it was aimed at, which is
what the text format opens with as `π»(Ξ¦)`. `<evaluate>` is one firing of πΌ, `Ξ»`
naming the entry that answered it, `by` naming the judgment that asked for the
firing β the same word the root is named after and a `<stuck>` carries β and
`at` naming the site it was fired at. The text format writes those two as the
comment of its line, `π»(Ξ¦)`.
`<formation at="Ξ¦" term="β¦ β¦ β§">` is a formation π» got into through `box`,
which the text format writes as `formation(β¦ β¦ β§) # π»(Ξ¦)`: `at` names the
site it was entered at and `term` holds the formation. Whatever the `Ο` body
does is written inside the element, so it closes where the text format drops
back to the indentation it opened at, and like the text line it counts nothing
and names no meta.
`<bind>` is one meta the firing bound, `meta` naming it the same way the text
format names it, counter and all, and the element holding the value it took: a
term where the operand was reduced with π, the datum itself where a `dataize`
operand came down to data. `<dataize>` inside a firing is the other thing a
`dataize` operand may come to, the datum manufactured for an unknown, and holds
the formation that unknown names rather than the 42 standing for it: a `π` is
the name of a Ξ» function and no term of its own, so what π» was applied to is
`π2:Ξ»` and never `π2` alone. It carries `meta` where the root carries
`at`, the same difference the text format draws between `π»(Ξ¦)` at the top
and `πΏ1.2 := π»(β¦)` in a block. The name of the element is what tells a
manufactured datum from data, the way `π»(β¦)` does in the text format, so
nothing has to be read off the presence of an attribute. `<answer>` holds the
term the firing answered with, named the same way by its own `meta`, and
`<built>` before it holds the term the entry wrote, the one π made that answer
of: two elements rather than two attributes of one, for the same reason
`<dataize>` is no `<bind>`.
`<known symbol="π44">3F-F0-00-00-00-00-00-00</known>` is the fact a `symbolize`
line writes about a symbol it minted, which the text format writes as
`π»(π44:Ξ») == β¦`: the symbol stands in the attribute a reader joins
lines on and the data dataizing its formation answers are the text of the
element. It takes `symbol` and not `meta`, since the fact is about the unknown
and not about a meta the firing bound.
`<joined symbol="π6">π4 π5</joined>` is the same kind of fact about a symbol
a `join` line minted, which the text format writes as
`π»(π6:Ξ») β { π»(π4:Ξ»), π»(π5:Ξ») }`: the fresh symbol stands
in `symbol` and the two it was minted for are the text, in the order the line
listed the metas it joined. A line whose two terms differ at several places
writes one element per pair of symbols, and one whose terms are alike writes
none. The meta the line binds is a `<bind>` like every other meta of the
firing.
`<minted symbol="π1">40-14-β¦ 40-18-β¦</minted>` is one symbol the firing
minted, one element per bare `π` the entry wrote its answer with, standing
inside the block ahead of the `<built>` carrying them. The symbol stands in
`symbol`, the way `<known>` and `<joined>` put theirs, and the text is what is
known about it: the values the `dataize` lines of the entry took, in the order
the entry declares them, each spelled as its own line spells it β the bytes
for a datum, `π1` for a symbol β and separated by a space the way `<joined>`
lists its pair. With the `Ξ»` of the block the element reads as the fact
`π»(π1:Ξ») == L_number_plus(40-14-β¦, 40-18-β¦)`, and a firing of an entry with
no `dataize` line writes `<minted symbol="π1"/>`. The symbol is also the edge
a reader joins on: a later `<dataize meta="πΏ1.5">π2:Ξ»</dataize>` names the
symbol the firing that wrote `<minted symbol="π2">` handed out. A firing
minting two symbols writes two elements and one minting none writes none,
which no attribute on the answer could say: a term may carry several symbols,
or carry one where the value it stands for is not a symbol at all. In the fork
above, `πΌ(L_gt)` writes `<minted symbol="π2">` although `π2` sits under `if`
and not where the value of the term is, while `πΌ(L_fork)` writes none at all,
since the symbol it answers with comes from a `join` line and stands in a
`<joined>` of its own.
A Ξ» name no entry answers is `<stuck Ξ»="β¦">`, standing where its `<evaluate>`
would have stood with the formation πΌ was fired against as its text and the
judgment that asked in its `by` attribute, where the text format writes
the letter of it. A firing that happened while an operand of another was being
reduced is an `<evaluate>` inside the one that asked, which is what the deeper
indentation means in the text. Elements are written as the run goes and
the open ones are closed when it ends, so a run that fails still leaves a
well-formed document behind:
<!-- markdownlint-disable MD013 -->
```bash
$ phino dataize --symbolic=atoms.yaml --protocol=atoms.xml --quiet \
--sweet --hide-rho stuck.phi
[ERROR]: No entry of --symbolic answers the Ξ» function 'L_number_nope'
$ cat atoms.xml
<?xml version="1.0" encoding="UTF-8"?>
<dataize at="Ξ¦">
<formation at="Ξ¦" term="β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§, Ο β¦ 5.plus( 6 ).nope β§">
<evaluate Ξ»="L_number_plus" by="morph" at="Ξ¦">
<formation at="Ξ¦.aπ΅0" term="β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§">
<formation at="Ξ¦.aπ΅0" term="40-14-00-00-00-00-00-00:Ξ:Ο">
</formation>
</formation>
<bind meta="πΏ1.1">40-14-00-00-00-00-00-00</bind>
<formation at="Ξ¦.aπ΅1" term="β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§">
<formation at="Ξ¦.aπ΅1" term="40-18-00-00-00-00-00-00:Ξ:Ο">
</formation>
</formation>
<bind meta="πΏ2.1">40-18-00-00-00-00-00-00</bind>
<minted symbol="π1">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>
<built meta="π.1.1">Ξ¦.number( Ο β¦ π1:Ξ» )</built>
<answer meta="π.1.2">β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§</answer>
</evaluate>
<stuck Ξ»="L_number_nope" by="dataize">L_number_nope:Ξ»</stuck>
</formation>
</dataize>
```
<!-- markdownlint-enable MD013 -->
### Abridging the protocol
A formation carrying a whole object is written flat on one line, so a real
run fills the protocol with lines tens of thousands of characters long. The
`--abridged` option shortens every term the protocol writes, in the text and
the XML alike: a formation longer than sixty characters keeps its `Ο`, `Ξ` and
`Ξ»` bindings and folds the rest into a count, and a byte string longer than
eight bytes keeps its first four bytes and its length. The result the run
prints stays whole, and the option is refused without `--protocol`:
<!-- markdownlint-disable MD013 -->
```bash
$ cat wide.phi
β¦
t β¦ β¦
Ο β¦ β¦ Ξ β€ 48-65-6C-6C-6F-2C-20-77-6F-72-6C-64 β§,
left β¦ ΞΎ.right,
right β¦ ΞΎ.left,
middle β¦ ΞΎ.left
β§
β§
$ phino dataize --locator=Q.t --protocol=wide.txt --abridged --quiet \
--sweet --hide-rho wide.phi
$ cat wide.txt
π»(Ξ¦.t)
formation(β¦ Ο β¦ 48-65-6C-6C-...(12b):Ξ, +3 attrs β§) # π»(Ξ¦.t)
```
<!-- markdownlint-enable MD013 -->
### Reducing a term inside a universe
A term that is no part of the program may still be reduced against it, with the
`--inside` option: the expression it names is bound to a synthetic attribute
prepended to the input expression, which the run takes as the universe Ξ¦,
normalized there and then reduced.
```bash
$ 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
```
This is the very trick `phino` plays internally to reduce the operands of a
firing, made available to whoever asks it to reduce a term the program does not
hold. The option cannot be combined with `--locator`, since it aims the run at
the binding it mints itself. Both `dataize` and `morph` take `--symbolic` and
`--inside`.
### Partial evaluation
A Ξ» function no entry of the `--symbolic` file answers fails the run. This is
what happens when an operation is deliberately left out β an input the object
model has not declared yet, or an operation whose answer is not known. With
`--partial`, dataization becomes partial evaluation instead: what the known
inputs decide is computed, the rest survives as the residual program, which is
printed in place of the bytes, and the run ends successfully:
```bash
$ 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 answered by the entries the file carries, so
it was reduced β the symbol it came to sits in the hidden `Ο` of the residual
program β while `as-bool` names a Ξ» function no entry answers, so it stays in
place as a normal-form subterm. A stuck site opens no block in the
`--protocol` file, since nothing fired there, and stands in it as `?(β¦)`:
<!-- markdownlint-disable MD013 -->
```bash
$ phino dataize --symbolic=atoms.yaml --partial --protocol=atoms.txt --quiet \
--sweet --hide-rho partial.phi
$ cat atoms.txt
π»(Ξ¦)
formation(β¦ 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 β§) # π»(Ξ¦)
πΌ(L_number_times) # π(Ξ¦)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-00-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ», times(x) β¦ L_number_times:Ξ», as-bool β¦ L_number_as_bool:Ξ» β§) # π»(Ξ¦.aπ΅0)
formation(40-00-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅0)
πΏ1.1 := 40-00-00-00-00-00-00-00 # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-08-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ», times(x) β¦ L_number_times:Ξ», as-bool β¦ L_number_as_bool:Ξ» β§) # π»(Ξ¦.aπ΅1)
formation(40-08-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅1)
πΏ2.1 := 40-08-00-00-00-00-00-00 # π»(ΞΎ.x)
π.1.1 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π
π.1.2 := β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ», times(x) β¦ L_number_times:Ξ», as-bool β¦ L_number_as_bool:Ξ» β§ # π(π.1.1)
πΌ(L_number_plus) # π(Ξ¦)
formation(β¦ Ο β¦ π1:Ξ», plus(x) β¦ L_number_plus:Ξ», times(x) β¦ L_number_times:Ξ», as-bool β¦ L_number_as_bool:Ξ» β§) # π»(Ξ¦.aπ΅2)
πΏ1.2 := π»(π1:Ξ») # π»(ΞΎ.Ο)
formation(β¦ Ο β¦ Ξ¦.bytes( Ο β¦ 40-10-00-00-00-00-00-00:Ξ ), plus(x) β¦ L_number_plus:Ξ», times(x) β¦ L_number_times:Ξ», as-bool β¦ L_number_as_bool:Ξ» β§) # π»(Ξ¦.aπ΅3)
formation(40-10-00-00-00-00-00-00:Ξ:Ο) # π»(Ξ¦.aπ΅3)
πΏ2.2 := 40-10-00-00-00-00-00-00 # π»(ΞΎ.x)
π.2.1 := Ξ¦.number( Ο β¦ π2:Ξ» ) # π
π.2.2 := β¦ Ο β¦ π2:Ξ», plus(x) β¦ L_number_plus:Ξ», times(x) β¦ L_number_times:Ξ», as-bool β¦ L_number_as_bool:Ξ» β§ # π(π.2.1)
?(L_number_as_bool) # π»(L_number_as_bool:Ξ»)
```
<!-- markdownlint-enable MD013 -->
Evaluation stays demand-driven, as the calculus prescribes: an argument
that nothing asked for before the run got stuck is left as it is in the
residual program, for the next iteration.
An operand of a firing that reaches the terminator `β₯`, or a term no
dataization rule matches, such as a formation whose `Ο` is a void nothing
filled, never comes down to data either, and `--partial` parks that firing
the same way, writing the dead end into the protocol as `?(β₯)` with the term
that could not be dataized beside it. Dataization aimed at `β₯` itself still
fails, with or without `--partial`, since there is no firing to park.
The nested morphing and dataization recursion is bounded by the
`--max-steps` option (default `1000`): when the budget is exhausted, the run
fails with `Dataization did not finish before reaching the limit of steps`.
This guards against non-terminating terms, which used to loop forever before
the bound was introduced:
```bash
$ phino dataize --max-steps=50 problem.phi
[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=50
```
That budget bounds how deep one branch goes, not how much the whole run does.
An entry that reduces two operands, each firing it again, doubles its work at
every level and still never gets deep, so no `--max-steps` stops it. The
`--max-firings` option counts every Ξ» function the run fires and fails the
run once the count is spent; `--partial` parks it instead, the way it parks a
spent `--max-steps`. There is no limit unless the option is given:
```bash
$ cat split.yaml
- Ξ»: L_split
morph:
π1: Ξ¦.s.foo
π2: Ξ¦.s.foo
π: β¦ l β¦ π1, r β¦ π2 β§
$ cat split.phi
β¦ s β¦ β¦ Ξ» β€ L_split β§, x β¦ Ξ¦.s.foo β§
$ phino morph --symbolic=split.yaml --locator=Q.x --max-firings=64 split.phi
[ERROR]: Evaluation did not finish before reaching the limit of firings: --max-firings=64
```
## Morph
Dataization insists on bytes. Morphing π asks a different question: evaluate
as far as the object model allows, without demanding data. It resolves Ξ¦
against the universe, peels dispatches and applications through
normalization, fires whichever Ξ» functions sit under a dispatch, and stops at
the first formation it reaches, handing that formation back untouched. The
`morph` command runs π on its own:
```bash
$ 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, Ξ» β€ L_number_plus β§
```
The inner `5.plus( 6 )` fires, because `.plus` is dispatched on its result,
and the symbol it answered with lands in the `Ο` hidden by `--hide-rho`. The
outer application is saturated but bare, so π returns it and is finished;
firing it is dataization's job and takes `dataize` on to a datum.
The default locator `Q` morphs the whole top formation, which π returns
unchanged, so `--locator` is how one aims π at a subterm, exactly as in
`dataize`. Unlike π», π is total: where no formation is reachable the answer
is the terminator `β₯`, printed rather than reported as a failed run:
```bash
$ phino morph --locator=Q.x <<< 'β¦ x β¦ ΞΎ β§'
β₯
```
The whole `dataize` option surface applies unchanged β `--symbolic`,
`--inside`, `--sequence`, `--headers`, `--steps-dir`, `--protocol`,
`--partial`, `--max-steps`, `--shuffle`/`--seed`, `--output`, `--focus` and the
rest.
### Deep morphing
π stops at the first formation it reaches and hands its bindings back as they
were written, since firing a bare Ξ» is dataization's job, and `dataize`
follows the one path dataization demands and ends in bytes. What a program
holds but nothing demands β the argument of a Ξ» function no entry answers, for
one β is therefore reduced by neither. The `--deep` flag enters it:
```bash
$ cat gap.phi
β¦
bytes β¦ β¦ Ο β¦ β
β§,
number β¦ β¦ Ο β¦ β
, times(Ο, x) β¦ β¦ Ξ» β€ L_number_times β§ β§,
bar(x) β¦ β¦ Ξ» β€ L_bar β§,
demo β¦ β¦ foo β¦ β¦ n β¦ 3, Ο β¦ Ξ¦.bar( ΞΎ.n.times( 5 ).times( 7 ) ) β§ β§
β§
$ phino morph --symbolic=atoms.yaml --inside='Q.demo.foo' \
--sweet --hide-rho gap.phi
β¦ n β¦ 3, Ο β¦ Ξ¦.bar( n.times( 5 ).times( 7 ) ) β§
$ phino morph --deep --symbolic=atoms.yaml --inside='Q.demo.foo' \
--sweet --hide-rho gap.phi
β¦ n β¦ 3, Ο β¦ Ξ¦.bar( β¦ Ο β¦ π2:Ξ», times(x) β¦ L_number_times:Ξ» β§ ) β§
```
Every binding of the formation is entered, recursively. π is asked about the
term standing there and, where it lands on a saturated formation whose Ξ» an
entry answers, that Ξ» is fired and π is asked about the answer again. A term on
whose way a Ξ» function fired is replaced by the answer of the last firing,
morphed: an entry answering `Ξ¦.number( Ο β¦ β¦ Ξ» β€ π β§ )` stands the formation of
`number` there, the very one the same term written in the program morphs to, so
a value that came out of a firing and a value that was written as a literal are
one shape and can be compared leaf by leaf. That costs the size of the object's
formation in the residual, which is the price of saying the same thing one way.
A term nothing fired on stays exactly as it was written and only its own parts
are walked, so `Ξ¦.bar` keeps its name and what comes back is still the same
program, reduced as far as the file allows. The step joins the chain under the
name `deep`, so `--sequence` shows it, and `--max-steps` bounds the walk.
Two things are left alone. A Ξ» no entry answers is not fired at all, so
`--deep` stays as total as π itself and needs no `--partial`; a Ξ» function that
gets stuck deeper on a spine still fails the run, and `--partial` parks it,
leaving that term as it was written. A firing the walk does make and cannot
finish β one whose operand never comes down to data, because a Ξ» nothing
answers stands in it β is parked by `--partial` the same way: the binding it
stood in is left as it was written, the walk enters the next one, and the
protocol shows the firing with nothing bound under it. One entry nothing can
answer therefore taints its own binding and not the whole run. A formation
still holding a void
binding is not fired either: the void is an argument the program has not given
yet, so `times(x) β¦ L_number_times:Ξ»` is a method waiting to be applied,
not an application waiting to be computed. Walking the whole program therefore
folds what it can and leaves the object model as it was declared:
```bash
$ phino morph --deep --symbolic=atoms.yaml --sweet --hide-rho gap.phi
β¦
bytes(Ο) β¦ β¦β§,
number(Ο) β¦ β¦ times(x) β¦ L_number_times:Ξ» β§,
bar(x) β¦ L_bar:Ξ»,
demo β¦ β¦ n β¦ 3, Ο β¦ Ξ¦.bar( β¦ Ο β¦ π2:Ξ», times(x) β¦ L_number_times:Ξ» β§ ) β§:foo
β§
```
### Acyclic morphing
Whether a program terminates is the object model's business, not the
calculus's, so phino prevents no recursion of its own and `--max-steps` is what
ends a run that never finishes. An entry answering with a firing of itself
therefore spends the whole budget before it fails, and what it fails on is the
limit rather than the loop:
```bash
$ cat loop.yaml
- Ξ»: L_loop
π: β¦ Ξ» β€ L_loop β§
$ cat loop.phi
β¦ x β¦ β¦ Ξ» β€ L_loop β§.foo β§
$ phino morph --symbolic=loop.yaml --locator='Q.x' --max-steps=40 loop.phi
[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40
```
The `--acyclic=<mode>` option makes a reduction notice. Every frame of π and
of π» remembers the formations the frames above it have entered, and only four
places enter one: `fire` of π» and `ml` of π, which fire the Ξ» function of a
formation, the walk of `--deep`, which fires the Ξ» function of every formation
π leaves bare, and `box` of π», which gets into the `Ο` body of a formation
carrying no Ξ» and no `Ξ`. A frame about to enter a formation one of the frames
above it has already entered is asking a question only ever answered by asking
it again, so the option stops there and parks the site the way `--partial`
parks a Ξ» function that cannot fire: the answer is the term the spine had
reached, left where it stood, and the command exits successfully.
```bash
$ phino morph --symbolic=loop.yaml --locator='Q.x' --acyclic=proven \
--max-steps=40 --hide-rho loop.phi
β¦ Ξ» β€ L_loop β§.foo
```
π and π» share that one memory. They call each other on the very term they
were asked about, and that handover is no loop, but it enters no formation
either, so it is never remembered and never mistaken for one. A body
dispatching the object it stands in is a loop π» walks round on its own β π
stops at a formation every round, and `box` gets into it again β so `dataize`
takes the option too, and so does the run of π» a Ξ» function's `dataize` operand
is brought down with:
```bash
$ cat cyc.phi
β¦ cyc β¦ β¦ x β¦ β
, Ο β¦ Ξ¦.cyc( ΞΎ.x ) β§, t β¦ Ξ¦.cyc( β¦β§ ) β§
$ phino dataize --locator='Q.t' --acyclic=proven --partial \
--sweet --hide-rho --flat cyc.phi
β¦ cyc(x) β¦ Ξ¦.cyc( x ):Ο, t β¦ Ξ¦.cyc( β¦β§ ) β§
```
π» insists on bytes and a parked term carries none, so under `dataize` the option
wants `--partial` to have something to print: the residual program, exactly the
one it prints for a Ξ» function that cannot fire. Without it the run stops on
the loop all the same, naming the formation it entered again instead of running
the budget down. Under `morph` nothing is asked for: π always has a term to
answer with, a loop π» meets under a firing parks the site the firing stands at,
and the walk of `--deep` goes on to the next binding.
The mode says what "the same formation" means, and there is no default, since
no answer is right for every run. Under `proven` it means the same up to a
renaming of symbols: two
formations are one where some one-to-one pairing of the symbols of the first
with those of the second makes them equal, so `π5` may stand where `π3` stood
as long as it does so everywhere and no other symbol stands there too. Data,
attribute names and Ξ» names must still match exactly. That is what catches a
recursion over an unknown, which never repeats a term: every round mints fresh
symbols, so the formation it enters on the second round is the one it entered
on the first with new names for the unknowns. The renaming is sound because a
symbol is an opaque value nobody worked out β every one of them dataizes to the
same manufactured datum and no entry of `--symbolic` answers one β so a
formation entered again with nothing but its symbols renamed replays the round
it is inside forever. Data still tells rounds apart: a formation entered with
`n β¦ 3` and then with `n β¦ 2` is two formations, so a recursion over data is
not cut while it goes on computing. Take a factorial over a symbolic argument,
with `fact.yaml` answering `L_zero`, `L_dec` and `L_mul` with a fresh symbol
each and `L_if` a fork joining its two branches:
<!-- markdownlint-disable MD013 -->
```bash
$ cat fact.phi
β¦
if β¦ β¦ c β¦ β
, left β¦ β
, right β¦ β
, Ξ» β€ L_if β§,
zero β¦ β¦ x β¦ β
, Ξ» β€ L_zero β§,
dec β¦ β¦ x β¦ β
, Ξ» β€ L_dec β§,
mul β¦ β¦ a β¦ β
, b β¦ β
, Ξ» β€ L_mul β§,
fact β¦ β¦ n β¦ β
, Ο β¦ Ξ¦.if( c β¦ Ξ¦.zero( x β¦ ΞΎ.n ), left β¦ β¦ Ξ β€ 01- β§, right β¦ Ξ¦.mul( a β¦ ΞΎ.n, b β¦ Ξ¦.fact( n β¦ Ξ¦.dec( x β¦ ΞΎ.n ) ) ) ) β§,
x β¦ Ξ¦.fact( n β¦ β¦ Ξ» β€ π1 β§ )
β§
$ cat fact.yaml
- Ξ»: L_zero
dataize:
πΏ1: $.x
π: β¦ Ξ» β€ π β§
- Ξ»: L_dec
dataize:
πΏ1: $.x
π: β¦ Ξ» β€ π β§
- Ξ»: L_mul
dataize:
πΏ1: $.a
πΏ2: $.b
π: β¦ Ξ» β€ π β§
- Ξ»: L_if
dataize:
πΏ1: $.c
morph:
π1: $.left
π2: $.right
symbolize:
π3: π1
π4: π2
join:
π5: [π3, π4]
π: π5
$ phino morph --deep --acyclic=proven --partial --sweet --hide-rho --flat \
--symbolic=fact.yaml --locator='Q.x' --protocol=fact.txt fact.phi
β¦ n β¦ π1:Ξ», Ο β¦ Ξ¦.if( c β¦ π2:Ξ», left β¦ 01-:Ξ, right β¦ Ξ¦.mul( a β¦ n, b β¦ Ξ¦.fact( n β¦ π3:Ξ» ) ) ) β§
$ cat fact.txt
π(Ξ¦.x)
πΌ(L_zero) # π(Ξ¦.x.Ο)
πΏ1.1 := π»(π1:Ξ») # π»(ΞΎ.x)
π.1.1 := π2:Ξ» # π
π.1.2 := π2:Ξ» # π(π.1.1)
πΌ(L_dec) # π(Ξ¦.x.Ο)
πΏ1.2 := π»(π1:Ξ») # π»(ΞΎ.x)
π.2.1 := π3:Ξ» # π
π.2.2 := π3:Ξ» # π(π.2.1)
πΌ(L_mul) # π(Ξ¦.x.Ο)
πΏ1.3 := π»(π1:Ξ») # π»(ΞΎ.a)
formation(β¦ n β¦ π3:Ξ», Ο β¦ Ξ¦.if( c β¦ Ξ¦.zero( x β¦ n ), left β¦ 01-:Ξ, right β¦ Ξ¦.mul( a β¦ n, b β¦ Ξ¦.fact( n β¦ Ξ¦.dec( x β¦ n ) ) ) ) β§) # π»(Ξ¦.aπ΅3)
πΌ(L_if) # π»(Ξ¦.aπ΅3)
πΌ(L_zero) # π»(Ξ¦.aπ΅4)
πΏ1.5 := π»(π3:Ξ») # π»(ΞΎ.x)
π.5.1 := π4:Ξ» # π
π.5.2 := π4:Ξ» # π(π.5.1)
πΏ1.4 := π»(π4:Ξ») # π»(ΞΎ.c)
π1.4 := 01-:Ξ # π(ΞΎ.left)
πΌ(L_dec) # π(Ξ¦.aπ΅7.b)
πΏ1.6 := π»(π3:Ξ») # π»(ΞΎ.x)
π.6.1 := π5:Ξ» # π
π.6.2 := π5:Ξ» # π(π.6.1)
looped(β¦ a β¦ π1:Ξ», b β¦ Ξ¦.fact( n β¦ π3:Ξ» ), Ξ» β€ L_mul β§) # π(Ξ¦.aπ΅7), proven
π2.4 := β¦ a β¦ π3:Ξ», b β¦ Ξ¦.fact( n β¦ π5:Ξ» ), Ξ» β€ L_mul β§ # π(ΞΎ.right)
π»(π6:Ξ») == 01-
π3.4 := π6:Ξ» # π1
π4.4 := β¦ a β¦ π3:Ξ», b β¦ Ξ¦.fact( n β¦ π5:Ξ» ), Ξ» β€ L_mul β§ # π2
πΌ(L_if) # π(Ξ¦.x.Ο)
πΏ1.7 := π»(π2:Ξ») # π»(ΞΎ.c)
π1.7 := 01-:Ξ # π(ΞΎ.left)
πΌ(L_mul) # π(Ξ¦.aπ΅11)
πΏ1.8 := π»(π1:Ξ») # π»(ΞΎ.a)
formation(β¦ n β¦ π3:Ξ», Ο β¦ Ξ¦.if( c β¦ Ξ¦.zero( x β¦ n ), left β¦ 01-:Ξ, right β¦ Ξ¦.mul( a β¦ n, b β¦ Ξ¦.fact( n β¦ Ξ¦.dec( x β¦ n ) ) ) ) β§) # π»(Ξ¦.aπ΅13)
πΌ(L_if) # π»(Ξ¦.aπ΅13)
πΌ(L_zero) # π»(Ξ¦.aπ΅14)
πΏ1.10 := π»(π3:Ξ») # π»(ΞΎ.x)
π.10.1 := π.5.2 # π
π.10.2 := π.5.2 # π(π.10.1)
πΏ1.9 := π»(π4:Ξ») # π»(ΞΎ.c)
π1.9 := 01-:Ξ # π(ΞΎ.left)
πΌ(L_dec) # π(Ξ¦.aπ΅17.b)
πΏ1.11 := π»(π3:Ξ») # π»(ΞΎ.x)
π.11.1 := π.6.2 # π
π.11.2 := π.6.2 # π(π.11.1)
looped(β¦ a β¦ π1:Ξ», b β¦ Ξ¦.fact( n β¦ π3:Ξ» ), Ξ» β€ L_mul β§) # π(Ξ¦.aπ΅17), proven
π2.9 := β¦ a β¦ π3:Ξ», b β¦ Ξ¦.fact( n β¦ π5:Ξ» ), Ξ» β€ L_mul β§ # π(ΞΎ.right)
π»(π6:Ξ») == 01-
π3.9 := π3.4 # π1
π4.9 := β¦ a β¦ π3:Ξ», b β¦ Ξ¦.fact( n β¦ π5:Ξ» ), Ξ» β€ L_mul β§ # π2
π2.7 := β¦ a β¦ π1:Ξ», b β¦ Ξ¦.fact( n β¦ π3:Ξ» ), Ξ» β€ L_mul β§ # π(ΞΎ.right)
π»(π4:Ξ») == 01-
π3.7 := π.10.2 # π1
π4.7 := β¦ a β¦ π1:Ξ», b β¦ Ξ¦.fact( n β¦ π3:Ξ» ), Ξ» β€ L_mul β§ # π2
```
<!-- markdownlint-enable MD013 -->
The first `L_mul` brings its `b` down, and that gets π» into `fact` with
`n β¦ π3`, the `formation(β¦)` line under it. Inside, the fork reduces its right
branch, and the walk of `--deep` over it would fire `L_mul` with `a β¦ π3` and
`b β¦ Ξ¦.fact( n β¦ π5 )`: the formation the first `L_mul` was fired with, `π3`
standing where `π1` stood and `π5` where `π3` stood, so the firing is cut
before it opens. The cut is the `looped(β¦)` line under `π.6.2`, standing where
the block of the cut firing would have stood and commented with the judgment
the frame belonged to, the site it was cut at and the mode that cut it. What it
carries is the formation the frame above entered, as that frame had it, so the
two are paired by their terms and no reader has to rename symbols by eye or
find the cut in the residue. Nothing runs under a cut, so no block opens under
the line. In the XML protocol it is a self-closing element,
`<looped by="morph" match="proven" at="Ξ¦.aπ΅7" term="β¦"/>`, with the
attributes a `<formation>` carries and the mode. Without the option the same
run nests one round inside another until `--max-steps` runs out.
What a frame remembers is the branch from the run down to it, never everything
the run has touched, so two siblings entering one formation enter it twice and
only a formation entered from inside itself is a loop: the fork at `Ξ¦.x.Ο`
above gets into `fact` with `n β¦ π3` once more, on a branch of its own, and is
not cut there. The cut costs one lookup and fires on the turn the repeat
appears, so raising `--max-steps` from 40 to a million changes neither the
answer nor the time.
What `proven` cannot see is a recursion that never comes back to the same
formation: one whose accumulator grows by a wrapper every round. Give the
factorial an `acc` it builds a `pair` onto, drop `L_mul` from `fact.yaml`, and
under `proven` the run nests deeper until `--max-steps` runs out, since no
renaming of symbols turns a longer chain of pairs into a shorter one:
<!-- markdownlint-disable MD013 -->
```bash
$ cat facta.phi
β¦
if β¦ β¦ c β¦ β
, left β¦ β
, right β¦ β
, Ξ» β€ L_if β§,
zero β¦ β¦ x β¦ β
, Ξ» β€ L_zero β§,
dec β¦ β¦ x β¦ β
, Ξ» β€ L_dec β§,
pair β¦ β¦ head β¦ β
, tail β¦ β
β§,
fact β¦ β¦ n β¦ β
, acc β¦ β
, Ο β¦ Ξ¦.if( c β¦ Ξ¦.zero( x β¦ ΞΎ.n ), left β¦ ΞΎ.acc, right β¦ Ξ¦.fact( n β¦ Ξ¦.dec( x β¦ ΞΎ.n ), acc β¦ Ξ¦.pair( head β¦ ΞΎ.n, tail β¦ ΞΎ.acc ) ) ) β§,
x β¦ Ξ¦.fact( n β¦ β¦ Ξ» β€ π1 β§, acc β¦ β¦ Ξ β€ 00- β§ )
β§
$ phino morph --deep --acyclic=plausible --partial --sweet --hide-rho --flat \
--symbolic=facta.yaml --locator='Q.x' --protocol=facta.txt facta.phi
β¦ n β¦ π1:Ξ», acc β¦ 00-:Ξ, Ο β¦ Ξ¦.if( c β¦ π2:Ξ», left β¦ acc, right β¦ Ξ¦.fact( n β¦ π3:Ξ», acc β¦ Ξ¦.pair( head β¦ n, tail β¦ acc ) ) ) β§
$ grep looped facta.txt
looped(β¦ c β¦ π2:Ξ», left β¦ 00-:Ξ, right β¦ Ξ¦.fact( n β¦ π3:Ξ», acc β¦ Ξ¦.pair( head β¦ π1:Ξ», tail β¦ 00-:Ξ ) ), Ξ» β€ L_if β§) # π(Ξ¦.aπ΅4.Ο), plausible
```
<!-- markdownlint-enable MD013 -->
Under `plausible` the same formation means one the formation entered earlier
is embedded in: the two have the same attributes, data and Ξ» function at the
top, and every term the earlier one bound there is found again in the later
one, as it stands or somewhere below a wrapper it gained. Any symbol stands for
any other, and nothing is looked for under a `Ο`, which holds the object a term
came from rather than a term it grew into. The second `if` above holds the
first under one more `pair`, so it is cut, and its `looped(β¦)` line says
`plausible`. A call nested in its own operand, such as a sum of sums, is never
cut, since the inner call is smaller than the outer one and cannot hold it.
The mode is not sound, though: a recursion whose argument grows on its way to
stopping is cut too, which is why the line names the mode that made the cut.
The mode also fires every formation once. Every use of a binding copies the
term bound to it, so a program reading `truncated β¦ Ο.abs.floor` in five
places fires `abs` and `floor` five times over and mints five symbols for one
value, and a guard written that way spends its whole budget saying the same
thing again. πΌ is a function of the formation it fires: the entry that
answers is found by the Ξ» name the formation carries, every operand is
reduced from its bindings inside the one universe of the run, and the answer
is built from what they came down to. So a run under `plausible` keeps what
every firing answered, by the formation it fired, and a later firing of the
same formation takes that answer, with the very symbols the first one minted,
instead of making it again. Two bindings spelling one term then come to one
symbol:
```bash
$ cat twins.phi
β¦
bytes β¦ β¦ Ο β¦ β
β§,
number β¦ β¦ Ο β¦ β
, plus(Ο, x) β¦ β¦ Ξ» β€ L_number_plus β§ β§,
a β¦ 7.plus( 5.plus( 6 ) ),
b β¦ 7.plus( 5.plus( 6 ) )
β§
$ phino morph --symbolic=atoms.yaml --acyclic=plausible --deep --sweet \
--hide-rho twins.phi
β¦
bytes(Ο) β¦ β¦β§,
number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§,
a β¦ β¦ Ο β¦ π2:Ξ», plus(x) β¦ L_number_plus:Ξ» β§,
b β¦ β¦ Ο β¦ π2:Ξ», plus(x) β¦ L_number_plus:Ξ» β§
β§
```
Under `proven` `b` lands on `π4`, since the walk over it fires the inner sum
and the outer one once more. The protocol of the run above still holds four
firings, two under `a` and two under `b`, since it records where πΌ was asked
and what it answered there; the two under `b` carry the answer lines of the
two under `a` and no operand line, since nothing was reduced for them, and
they are not charged to `--max-firings`, which counts the firings the run
made. The formation is compared with everything it carries, `Ο` included, so
a firing on another object is another firing, and a firing that got stuck
keeps nothing, since nothing was answered. A firing cut by the mode on its
way to an answer keeps the cut, and the next firing of the same formation is
cut at its own site without reducing anything first.
The mode also walks a binding of the world once. Every dispatch on an object
of the world copies it, and `--deep` walks every copy, so the tests of an
object are reduced once per copy of it the program holds. A copy goes by a
name in the world, such as `Ξ¦.num( Ο β¦ β¦ Ξ β€ 2A- β§ )`, the name `dot` writes
into its `Ο`, and that name without its application, `Ξ¦.num`, stands for every
copy. So a run under `plausible` enters `test` of `Ξ¦.num` in the first copy it
meets and leaves it as written in every later one:
```bash
$ cat atoms.yaml
- Ξ»: L_id
morph:
π1: $.x
π: π1
- Ξ»: L_twice
dataize:
πΏ1: $.Ο
π: Ξ¦.num( Ο β¦ β¦ Ξ» β€ π β§ )
$ cat world.phi
β¦
num β¦ β¦
Ο β¦ β
,
twice β¦ β¦ Ο β¦ β
, Ξ» β€ L_twice β§,
test β¦ Ξ¦.num( Ο β¦ β¦ Ξ β€ 01- β§ ).twice
β§,
a β¦ β¦ Ξ» β€ L_id, x β¦ Ξ¦.num( Ο β¦ β¦ Ξ β€ 2A- β§ ) β§,
b β¦ β¦ Ξ» β€ L_id, x β¦ Ξ¦.num( Ο β¦ β¦ Ξ β€ 2B- β§ ) β§
β§
$ phino morph --symbolic=atoms.yaml --acyclic=plausible --deep --partial \
--sweet --hide-rho world.phi
β¦
num(Ο) β¦ β¦ twice β¦ L_twice:Ξ», test β¦ Ξ¦.num( Ο β¦ 01-:Ξ ).twice β§,
a β¦ β¦
Ο β¦ 2A-:Ξ,
twice β¦ L_twice:Ξ»,
test β¦ β¦ Ο β¦ π1:Ξ», twice β¦ L_twice:Ξ», test β¦ Ξ¦.num( Ο β¦ 01-:Ξ ).twice β§
β§,
b β¦ β¦ Ο β¦ 2B-:Ξ, twice β¦ L_twice:Ξ», test β¦ Ξ¦.num( Ο β¦ 01-:Ξ ).twice β§
β§
```
A binding the copy filled, such as `Ο` above, belongs to that copy alone and
is entered every time. A binding left out is never replaced by what an earlier
copy came to, since a method may read the `Ο` or the `Ο` of the copy it
stands in, and so a recursion over copies of one object stops after its first
round, with the second one as written.
## Rewrite
You can rewrite this expression with the help of [rules](#rule-structure)
defined in the `my-rule.yml` YAML file (here, the `!d` is a capturing group,
similar to regular expressions):
```yaml
name: My custom rule
pattern: Ξ β€ !d
result: Ξ β€ 62-79-65
```
Then, rewrite:
```bash
$ 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:
```bash
phino rewrite --rule=rule1.yaml --rule=rule2.yaml ...
```
You can also use [built-in rules](resources), which are designed
to normalize expressions:
```bash
phino rewrite --normalize hello.phi
```
Both flags may be combined, so that your own rules are applied
alongside the built-in ones, in a single rewriting session:
```bash
phino rewrite --normalize --rule=my-rule.yaml hello.phi
```
Some rules mint fresh synthetic names via the `random-string` built-in. To
keep the output reproducible across runs, `phino` seeds the random generator
deterministically with `0` by default. Use `--seed` to pick a different seed:
```bash
phino rewrite --seed=42 --rule=my-rule.yml hello.phi
```
If no input file is provided, the π-expression is taken from `stdin`:
```bash
$ echo 'β¦ Ο β¦ β¦ Ξ β€ 68-65-6C-6C-6F β§ β§' | phino rewrite --rule=my-rule.yml
β¦ Ο β¦ β¦ Ξ β€ 62-79-65 β§ β§
```
You're able to pass [`XMIR`][xmir] as input. Use `--input=xmir` and `phino`
will parse given `XMIR` from file or `stdin` and convert it to `phi` AST.
```bash
phino rewrite --rule=my-rule.yaml --input=xmir file.xmir
```
Also `phino` supports π-expressions in
[ASCII](https://en.wikipedia.org/wiki/ASCII) format and with
syntax sugar. The `rewrite` command also allows you to desugar the expression
and print it in canonical syntax:
```bash
$ echo '[[ @ -> Q.io.stdout("hello") ]]' | phino rewrite
β¦
Ο β¦ Ξ¦.io.stdout( Ξ±0 β¦ Ξ¦.string( Ο β¦ Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 68-65-6C-6C-6F β§ ) ) )
β§
```
A formation of a single binding may be written as its asset, a colon,
and the attribute the asset is bound to:
```text
β¦ Ξ β€ 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, so
`β¦ x β¦ β¦ Ο β¦ ΞΎ.a β§ β§` comes out as `a:Ο:x` and `β¦ x(a) β¦ β¦ Ο β¦ a β§ β§`
as `β¦ x(a) β¦ a:Ο β§`: the formation inline voids open takes the sugar,
while the one holding the voids keeps its brackets, and so does
every formation in the salty syntax and in [LaTeX][latex].
A formation has a receiver `Ο` only when it declares one among its voids, the
way EO declares `^`: `β¦ Ο β¦ β
, t β¦ ΞΎ.Ο.k β§`, or `a(Ο) β¦ β¦ t β¦ ΞΎ.Ο.k β§` with
the void inline. `phino` adds none of its own, and a dispatch into a formation
that declares none hands it no `Ο` (the `skip` rule), so `ΞΎ.Ο` there is `β₯`:
<!-- markdownlint-disable MD013 -->
```bash
$ echo 'β¦ x β¦ β¦ k β¦ β¦ Ξ β€ 01- β§, a β¦ β¦ Ο β¦ β
, t β¦ ΞΎ.Ο.k β§ β§.a.t β§' | phino rewrite --normalize --sweet
01-:Ξ:x
$ echo 'β¦ x β¦ β¦ k β¦ β¦ Ξ β€ 01- β§, b β¦ β¦ t β¦ ΞΎ.Ο.k β§ β§.b.t β§' | phino rewrite --normalize --sweet
β₯:x
```
<!-- markdownlint-enable MD013 -->
## Merge
You can merge several π-expressions into a single one by merging their
top level formations:
```bash
$ 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](#rule-structure)
pattern. The result output contains matched substitutions:
```bash
$ phino match --pattern='β¦ Ξ β€ !d, !B β§' hello.phi
B >> β¦β§
d >> 68-65-6C-6C-6F
```
## Explain
You can _explain_ the built-in rules by printing them in [LaTeX][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):
```bash
$ phino explain --normalize
\begin{tabular}{rl}
\phinoNormalizationRule{alpha}
{ [[ B_1, \tau -> ?, B_2 ]] ( \phiTerminal{\alpha_{i}} -> e ) }
{ [[ B_1, \tau -> ?, B_2 ]] ( \tau -> e ) }
{ $ i = \vert \overline{ B_1 } \vert $ }
{ }
\phinoNormalizationRule{dc}
{ T ( \tau -> e ) }
{ T }
{ }
{ }
...
\phinoNormalizationRule{stop}
{ [[ B ]] . \tau }
{ T }
{ $ [ \tau \char44{} @ \char44{} L ] \cap B = \emptyset $ }
{ }
\end{tabular}
```
The morphing and dataization rules are printed the same way:
```bash
$ phino explain --morph
\begin{tabular}{rl}
\phinoMorphingRule{mf}
{ \mathbb{M}( [[ B ]], e ) }
{ [[ B ]] }
{ }
{ }
...
\phinoMorphingRule{universe}
{ \mathbb{M}( Q, e ) }
{ \mathbb{M}( \phinoNormalize{ e }, e ) }
{ $ e \not= Q $ }
{ }
\end{tabular}
```
```bash
$ phino explain --dataize
\begin{tabular}{rl}
\phinoDataizationRule{delta}
{ \phinoDataize{ [[ B_1, D> \delta_0, B_2 ]] } }
{ \delta_0 }
{ }
{ }
...
\phinoDataizationRule{norm}
{ \phinoDataize{ n } }
{ \phinoDataize{ \mathbb{M}( n, e ) } }
{ }
{ }
\end{tabular}
```
```bash
$ phino explain --contextualize
\begin{phinoContextualizationInference}
\phinoName{cxi}
\phinoConclusion{ \phinoContextualize{ \phiTerminal{\xi} }{ k }{ k } }
\end{phinoContextualizationInference}
...
\begin{phinoContextualizationInference}
\phinoName{cd}
\phinoPremise{ \phinoContextualize{ n }{ k }{ n_1 } }
\phinoConclusion{ \phinoContextualize{ n . \tau }{ k }{ n_1 . \tau } }
\end{phinoContextualizationInference}
```
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](src/AST.hs)
```bnfc
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](assets/contextualize.jpg)
* `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`.
* `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
[Symbols](#symbols)). 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. An index starts with one: a suffix of `0`, as in `!B0` or
`π0`, is refused where it is written, because it is a first index spelled
wrong and no name. A positional argument keeps counting from zero, though,
since `Ξ±0` is an index of the calculus and no meta variable.
Written bare, with no suffix at all, a meta variable is anonymous: it matches
whatever term stands in its place, every occurrence on its own, and binds no
name. Two anonymous metas of one kind are therefore two different captures,
which is what lets a pattern ask for any two attributes without inventing
names for them:
```yaml
name: two-attributes
pattern: 'β¦ π β¦ π, π β¦ π β§'
result: 'β¦ x β¦ β¦ Ξ β€ 2A- β§ β§'
```
Spelled with suffixes, that pattern would read `β¦ π1 β¦ π1, π2 β¦ π2 β§` and
name four captures the result never mentions, while `β¦ π1 β¦ π1, π1 β¦ π1 β§`
would be rejected as a duplicated attribute.
Nothing can refer to an anonymous meta, since it has no name to be referred to
by. Writing one outside a `pattern` (or the `match`, `universe` and `c-match` of
an inference rule) is a mistake in the rule and is reported as the rule loads.
A positional (Ξ±) application argument is written as `Ξ±0`, `~0` (ASCII), or
`Ξ±π`/`~!i` when its index is captured by an `!i`/`π` meta variable.
Incorrect usage of meta variables in π-expression patterns leads to
parsing errors.
## Benchmark
To run performance benchmarks, you need [Java 8+][java] and [curl][curl].
Maven is downloaded automatically on first run via `benchmark/mvnw`.
The benchmark uses the compiled [`Native`][jna-native] class from
[JNA][jna] β a large real-world Java class β as its test input.
On first run, `make bench` downloads the class, disassembles it to
[XMIR][xmir] via [jeo-maven-plugin][jeo], converts it to π using
`phino rewrite`, and caches the results in `benchmark/tmp/`.
Subsequent runs skip straight to the benchmarks.
Besides parsing, printing and rewriting that class, the suite morphs
symbolically. `benchmark/demo.phi` is a small world whose entries name the Ξ»
functions of `benchmark/atoms.yaml`, and each entry is a case of its own, so
that a slowdown of one of them is a line of the report rather than a share of
a single total. The smallest entry β one Ξ» function fired against one unknown
β is timed twice, over the demo world alone and over the same world merged
into the class, and the two numbers say between them what the world around an
entry costs (see [#1291][issue-1291]).
A case whose single run is measured in seconds gets fewer warmups and fewer
batches than a case measured in microseconds, since the whole suite runs
inside one job; the report says how many of each a case was given.
```bash
make bench
```
<!-- benchmark_begin -->
```text
=== parse/phi ===
warmup: 3 iterations
batches: 10 x 1
total: 1235604.619 ΞΌs
avg: 123560.462 ΞΌs
min: 112999.536 ΞΌs
max: 146848.289 ΞΌs
std dev: 13523.687 ΞΌs
=== parse/xmir ===
warmup: 3 iterations
batches: 10 x 1
total: 6181027.602 ΞΌs
avg: 618102.760 ΞΌs
min: 562545.414 ΞΌs
max: 682531.677 ΞΌs
std dev: 33378.489 ΞΌs
=== rewrite/normalize ===
warmup: 3 iterations
batches: 10 x 1
total: 14.492 ΞΌs
avg: 1.449 ΞΌs
min: 1.221 ΞΌs
max: 1.863 ΞΌs
std dev: 0.164 ΞΌs
=== print/sweet/multiline ===
warmup: 3 iterations
batches: 10 x 1
total: 3687452.277 ΞΌs
avg: 368745.228 ΞΌs
min: 340283.380 ΞΌs
max: 395918.805 ΞΌs
std dev: 19962.268 ΞΌs
=== print/sweet/flat ===
warmup: 3 iterations
batches: 10 x 1
total: 3607637.694 ΞΌs
avg: 360763.769 ΞΌs
min: 340150.409 ΞΌs
max: 401378.260 ΞΌs
std dev: 20648.726 ΞΌs
=== print/salty/multiline ===
warmup: 3 iterations
batches: 10 x 1
total: 10349170.023 ΞΌs
avg: 1034917.002 ΞΌs
min: 1011977.349 ΞΌs
max: 1103222.564 ΞΌs
std dev: 28732.304 ΞΌs
=== morph/symbolic/demo/e1 ===
warmup: 3 iterations
batches: 10 x 3
total: 129778.599 ΞΌs
avg: 4325.953 ΞΌs
min: 4287.416 ΞΌs
max: 4382.296 ΞΌs
std dev: 30.864 ΞΌs
=== morph/symbolic/demo/e2 ===
warmup: 3 iterations
batches: 10 x 5
total: 201800.582 ΞΌs
avg: 4036.012 ΞΌs
min: 3982.252 ΞΌs
max: 4124.524 ΞΌs
std dev: 43.136 ΞΌs
=== morph/symbolic/demo/e3 ===
warmup: 3 iterations
batches: 10 x 3
total: 174129.187 ΞΌs
avg: 5804.306 ΞΌs
min: 5765.516 ΞΌs
max: 5875.392 ΞΌs
std dev: 31.510 ΞΌs
=== morph/symbolic/demo/e4 ===
warmup: 3 iterations
batches: 10 x 5
total: 195942.319 ΞΌs
avg: 3918.846 ΞΌs
min: 3416.828 ΞΌs
max: 7676.874 ΞΌs
std dev: 1255.938 ΞΌs
=== morph/symbolic/demo/e5 ===
warmup: 3 iterations
batches: 10 x 15
total: 184899.602 ΞΌs
avg: 1232.664 ΞΌs
min: 1224.459 ΞΌs
max: 1242.434 ΞΌs
std dev: 5.749 ΞΌs
=== morph/symbolic/native/e5 ===
warmup: 3 iterations
batches: 10 x 1
total: 192336.003 ΞΌs
avg: 19233.600 ΞΌs
min: 18688.555 ΞΌs
max: 19909.284 ΞΌs
std dev: 427.461 ΞΌs
=== morph/symbolic/accum/0 ===
warmup: 3 iterations
batches: 10 x 2
total: 211409.497 ΞΌs
avg: 10570.475 ΞΌs
min: 10490.484 ΞΌs
max: 10743.310 ΞΌs
std dev: 66.154 ΞΌs
=== morph/symbolic/accum/400 ===
warmup: 3 iterations
batches: 10 x 1
total: 361054.043 ΞΌs
avg: 36105.404 ΞΌs
min: 35194.312 ΞΌs
max: 41143.240 ΞΌs
std dev: 1694.561 ΞΌs
```
The results were calculated in [this GHA job][benchmark-gha]
on 2026-09-27 at 05:24,
on Linux with 4 CPUs.
<!-- benchmark_end -->
## How to Contribute
Fork repository, make changes, then send us a [pull request][guidelines].
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:
```bash
make all
```
To generate a local coverage report for development, run:
```bash
make coverage
```
To build a `phino` executable into the root of the repository, run:
```bash
make phino
```
This produces an executable `phino` (or `phino.exe` on Windows) in the
project root, which you can run directly for quick local testing:
```bash
./phino --version
```
You will need [GHC β₯ 9.6.7][GHC] and [Cabal β₯ 3.0 (recommended)][cabal]
or [Stack β₯ 3.0][stack] installed.
[cabal]: https://www.haskell.org/cabal/
[stack]: https://docs.haskellstack.org/en/stable/install_and_upgrade/
[GHC]: https://www.haskell.org/ghc/
[guidelines]: https://www.yegor256.com/2014/04/15/github-guidelines.html
[xmir]: https://news.eolang.org/2022-11-25-xmir-guide.html
[latex]: https://en.wikipedia.org/wiki/LaTeX
[java]: https://www.java.com/en/download/
[curl]: https://curl.se/
[jna]: https://github.com/java-native-access/jna
[jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java
[jeo]: https://github.com/objectionary/jeo-maven-plugin
[issue-1291]: https://github.com/objectionary/phino/issues/1291
[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/36296915429