diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -128,9 +128,57 @@
`--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 third block, `symbolize`, and it reduces nothing. It takes a term
+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:
@@ -147,8 +195,8 @@
π: π3
```
-The right-hand side of a line names a meta bound by `morph` or by a
-`symbolize` line above it, and nothing else; a term nobody reduced has no data
+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.
@@ -175,7 +223,7 @@
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 fourth block, and it
+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.
@@ -194,11 +242,11 @@
π: π5
```
-A line names two metas bound by `morph`, 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.
+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
@@ -229,8 +277,19 @@
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.
+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 `raise-if(π»(π2:Ξ»), right) # π4` in the text format and
+`` 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.
@@ -265,7 +324,7 @@
$ cat sum.phi
β¦
bytes β¦ β¦ Ο β¦ β β§,
- number β¦ β¦ Ο β¦ β , plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§,
+ number β¦ β¦ Ο β¦ β , plus(Ο, x) β¦ β¦ Ξ» β€ L_number_plus β§ β§,
Ο β¦ 5.plus( 6 )
β§
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho sum.phi
@@ -469,7 +528,7 @@
β¦
bytes β¦ β¦ Ο β¦ β β§,
bool β¦ β¦ if β¦ β β§,
- number β¦ β¦ Ο β¦ β , plus(x) β¦ β¦ Ξ» β€ L_plus β§, gt(x) β¦ β¦ Ξ» β€ L_gt β§ β§,
+ 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 )
β§,
@@ -662,7 +721,7 @@
$ cat universe.phi
β¦
bytes β¦ β¦ Ο β¦ β β§,
- number β¦ β¦ Ο β¦ β , plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§
+ 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
@@ -689,8 +748,8 @@
bytes β¦ β¦ Ο β¦ β β§,
number β¦ β¦
Ο β¦ β ,
- plus(x) β¦ β¦ Ξ» β€ L_number_plus β§,
- times(x) β¦ β¦ Ξ» β€ L_number_times β§,
+ plus(Ο, x) β¦ β¦ Ξ» β€ L_number_plus β§,
+ times(Ο, x) β¦ β¦ Ξ» β€ L_number_times β§,
as-bool β¦ β¦ Ξ» β€ L_number_as_bool β§
β§,
Ο β¦ 2.times( 3 ).plus( 4 ).as-bool
@@ -733,6 +792,13 @@
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`.
@@ -757,7 +823,7 @@
$ cat two.phi
β¦
bytes β¦ β¦ Ο β¦ β β§,
- number β¦ β¦ Ο β¦ β , plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§,
+ number β¦ β¦ Ο β¦ β , plus(Ο, x) β¦ β¦ Ξ» β€ L_number_plus β§ β§,
Ο β¦ 5.plus( 6 ).plus( 7 )
β§
$ phino dataize --symbolic=atoms.yaml --sweet --hide-rho two.phi
@@ -798,7 +864,7 @@
$ cat gap.phi
β¦
bytes β¦ β¦ Ο β¦ β β§,
- number β¦ β¦ Ο β¦ β , times(x) β¦ β¦ Ξ» β€ L_number_times β§ β§,
+ number β¦ β¦ Ο β¦ β , times(Ο, x) β¦ β¦ Ξ» β€ L_number_times β§ β§,
bar(x) β¦ β¦ Ξ» β€ L_bar β§,
demo β¦ β¦ foo β¦ β¦ n β¦ 3, Ο β¦ Ξ¦.bar( ΞΎ.n.times( 5 ).times( 7 ) ) β§ β§
β§
@@ -984,10 +1050,7 @@
```bash
$ echo '[[ @ -> Q.io.stdout("hello") ]]' | phino rewrite
β¦
- Ο β¦ Ξ¦.io.stdout(
- Ξ±0 β¦ Ξ¦.string( Ο β¦ Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 68-65-6C-6C-6F, Ο β¦ β β§ ) )
- ),
- Ο β¦ β
+ Ο β¦ Ξ¦.io.stdout( Ξ±0 β¦ Ξ¦.string( Ο β¦ Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 68-65-6C-6C-6F β§ ) ) )
β§
```
@@ -1002,11 +1065,27 @@
```
The colon binds as tightly as a dot, so `ΞΎ.a:Ο.b` is `β¦ Ο β¦ ΞΎ.a β§.b`.
-With `--sweet`, `phino` prints every such formation this way, the implicit
-`Ο β¦ β ` aside, so `β¦ x β¦ β¦ Ο β¦ ΞΎ.a β§ β§` comes out as `a:Ο:x`. A formation
+With `--sweet`, `phino` prints every such formation this way, so
+`β¦ x β¦ β¦ Ο β¦ ΞΎ.a β§ β§` comes out as `a:Ο:x`. A formation
with inline voids keeps its brackets, as in `x(a) β¦ β¦ Ο β¦ a β§`, 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 `β₯`:
+
+
+
+```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
+```
+
+
+
## Merge
You can merge several π-expressions into a single one by merging their
@@ -1041,7 +1120,7 @@
```bash
$ phino match --pattern='β¦ Ξ β€ !d, !B β§' hello.phi
-B >> β¦ Ο β¦ β β§
+B >> β¦β§
d >> 68-65-6C-6C-6F
```
diff --git a/benchmark/demo.phi b/benchmark/demo.phi
--- a/benchmark/demo.phi
+++ b/benchmark/demo.phi
@@ -3,11 +3,11 @@
bool β¦ β¦ if β¦ β β§,
number β¦ β¦
Ο β¦ β ,
- plus(x) β¦ β¦ Ξ» β€ L_number_plus β§,
- times(x) β¦ β¦ Ξ» β€ L_number_times β§,
- gt(x) β¦ β¦ Ξ» β€ L_number_gt β§,
- neg β¦ β¦ Ο β¦ ΞΎ.Ο.times( -1 ) β§,
- minus(x) β¦ β¦ Ο β¦ ΞΎ.Ο.plus( ΞΎ.x.neg ) β§
+ plus(Ο, x) β¦ β¦ Ξ» β€ L_number_plus β§,
+ times(Ο, x) β¦ β¦ Ξ» β€ L_number_times β§,
+ gt(Ο, x) β¦ β¦ Ξ» β€ L_number_gt β§,
+ neg(Ο) β¦ β¦ Ο β¦ ΞΎ.Ο.times( -1 ) β§,
+ minus(Ο, x) β¦ β¦ Ο β¦ ΞΎ.Ο.plus( ΞΎ.x.neg ) β§
β§,
demo β¦ β¦
gap(a, b) β¦ β¦ Ο β¦ ΞΎ.a.minus( ΞΎ.b ).times( ΞΎ.a.minus( ΞΎ.b ) ) β§,
diff --git a/phino.cabal b/phino.cabal
--- a/phino.cabal
+++ b/phino.cabal
@@ -1,6 +1,6 @@
cabal-version: 3.0
name: phino
-version: 0.0.138
+version: 0.0.139
license: MIT
synopsis: Command-Line Manipulator of π-Calculus Expressions
description: Please see the README on GitHub at
diff --git a/resources/normalize/miss.yaml b/resources/normalize/miss.yaml
--- a/resources/normalize/miss.yaml
+++ b/resources/normalize/miss.yaml
@@ -1,11 +1,20 @@
# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
+# An application of an attribute the formation does not declare is β₯, save
+# Ο: a formation declares a receiver only when it lists Ο among its voids, and
+# one that does not merely ignores the Ο a dispatch hands it, which is what
+# the 'skip' rule says (#1407).
name: miss
pattern: β¦π΅1β§(π1 β¦ π)
result: β₯
when:
- not:
- in:
- - π1
- - π΅1
+ and:
+ - not:
+ in:
+ - π1
+ - π΅1
+ - not:
+ eq:
+ - π1
+ - Ο
diff --git a/resources/normalize/skip.yaml b/resources/normalize/skip.yaml
new file mode 100644
--- /dev/null
+++ b/resources/normalize/skip.yaml
@@ -0,0 +1,15 @@
+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
+# SPDX-License-Identifier: MIT
+---
+# A formation that declares no Ο has no receiver, so the Ο 'dot' and 'dotg'
+# hand every dispatched body is dropped once that body turns out to be such a
+# formation. 'copy' fills a Ο the formation declares void, and 'stay' keeps one
+# it has already bound (#1407).
+name: skip
+pattern: β¦π΅1β§(Ο β¦ π1)
+result: β¦π΅1β§
+when:
+ not:
+ in:
+ - Ο
+ - π΅1
diff --git a/src/AST.hs b/src/AST.hs
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -297,8 +297,8 @@
matchesBytes (ExPhiAgain _ _ (BaseObject "bytes")) = True
matchesBytes _ = False
matchFormation :: Expression -> Maybe Bytes
- matchFormation (ExFormation [BiDelta bts, BiVoid AtRho]) = Just bts
- matchFormation (ExPhiAgain _ _ (ExFormation [BiDelta bts, BiVoid AtRho])) = Just bts
+ matchFormation (ExFormation [BiDelta bts]) = Just bts
+ matchFormation (ExPhiAgain _ _ (ExFormation [BiDelta bts])) = Just bts
matchFormation _ = Nothing
matchDataObject _ = Nothing
@@ -314,7 +314,7 @@
DataObject label bts =
ExApplication (BaseObject label) (ArTau AtPhi (dataBytes bts))
--- The bytes object Ξ¦.bytes(Ο β¦ β¦ Ξ β€ β¦, Ο β¦ β β§) β what a 'bytes' atom
+-- The bytes object Ξ¦.bytes(Ο β¦ β¦ Ξ β€ β¦ β§) β what a 'bytes' atom
-- yields and what a 'DataObject' carries under its Ο argument.
-- The payload is bound to 'Ο', the void that the real 'bytes' object
-- declares ([@] > bytes), so that every dispatch on the literal can bind
@@ -323,4 +323,4 @@
dataBytes bts =
ExApplication
(BaseObject "bytes")
- (ArTau AtPhi (ExFormation [BiDelta bts, BiVoid AtRho]))
+ (ArTau AtPhi (ExFormation [BiDelta bts]))
diff --git a/src/CLI/Validators.hs b/src/CLI/Validators.hs
--- a/src/CLI/Validators.hs
+++ b/src/CLI/Validators.hs
@@ -75,15 +75,17 @@
in validateBoolOpts (zip bools' (map (printf "The --%s can be used only with --output=xmir") opts))
-- Check that an expression is printable as XMIR: its top level must be a
--- single binding followed by Ο β¦ β (the shape 'expressionToXMIR' accepts).
--- Called right after parsing, so a bad shape fails before any rewriting or
--- dataization work instead of at print time (issue #1082).
+-- single binding, optionally next to a void Ο (the shape 'expressionToXMIR'
+-- accepts). Called right after parsing, so a bad shape fails before any
+-- rewriting or dataization work instead of at print time (issue #1082).
validateXmirTopLevel :: IOFormat -> Expression -> IO ()
+validateXmirTopLevel XMIR (ExFormation [_]) = pure ()
validateXmirTopLevel XMIR (ExFormation [_, BiVoid AtRho]) = pure ()
+validateXmirTopLevel XMIR (ExFormation [BiVoid AtRho, _]) = pure ()
validateXmirTopLevel XMIR expr =
invalidCLIArguments
( printf
- "Expression cannot be printed with --output=xmir: its top level must be a single binding followed by Ο β¦ β , but got: %s"
+ "Expression cannot be printed with --output=xmir: its top level must be a single binding, but got: %s"
(printExpression expr)
)
validateXmirTopLevel _ _ = pure ()
diff --git a/src/CST.hs b/src/CST.hs
--- a/src/CST.hs
+++ b/src/CST.hs
@@ -97,8 +97,10 @@
| D'' -- d
| F -- π
| F' -- F
+ | F'' -- f
| S -- π
| S' -- S
+ | S'' -- \sigma
deriving (Eq, Show)
data EXCLAMATION = EXCL | NO_EXCL
@@ -347,19 +349,18 @@
toCST (ExBytes bts) ctx = EX_BYTES (toCST bts ctx)
toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)
toCST (ExPhiAgain prefix idx expr) ctx = EX_PHI_AGAIN prefix idx (toCST expr ctx)
- toCST (ExFormation [BiVoid AtRho]) ctx = toCST (ExFormation []) ctx
toCST (ExFormation []) _ = EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY NO_TAB) NO_EOL NO_TAB RSB
-- A formation of a single binding is sugared into its asset, a colon and
-- the attribute, as `FF-:Ξ`, `Plus:Ξ»`, `β :a` or `ΞΎ.a:Ο` (see #1385). The
-- full formation is kept next to it, for the notations that have no such
-- sugar: the salty one, LaTeX and the one '--hide-rho' strips.
toCST (ExFormation bds) ctx@(tabs, eol) =
- maybe full (`EX_SINGLE` full) (single (withoutLastVoidRho bds))
+ maybe full (`EX_SINGLE` full) (single bds)
where
full :: EXPRESSION
full =
let next = tabs + 1
- bds' = toCST (withoutLastVoidRho bds) (next, eol) :: BINDING
+ bds' = toCST bds (next, eol) :: BINDING
in EX_FORMATION
LSB
EOL
@@ -370,21 +371,22 @@
RSB
-- The asset of the only binding, laid out where the formation stands,
-- unless it has no sugar: a meta binding, a Ο binding whose attribute
- -- the parser takes for a Ξ or a Ξ», or one that carries a formation with
- -- inline voids, which reads better as 'x(a) β¦ β¦ β¦ β§'
+ -- the parser takes for a Ξ or a Ξ», one that carries a formation with
+ -- inline voids, which reads better as 'x(a) β¦ β¦ β¦ β§', or the void Ο a
+ -- formation declares as its receiver, which reads better as 'β¦ Ο β¦ β β§'
single :: [Binding] -> Maybe PAIR
single [BiTau AtDelta _] = Nothing
single [BiTau AtLambda _] = Nothing
- single [BiTau _ (ExFormation (BiVoid attr : rest))] | not (null rest) || attr /= AtRho = Nothing
+ single [bd@(BiTau _ ExFormation{})] | inlined (toCST bd ctx) = Nothing
single [BiTau attr expr] = Just (PA_TAU (toCST attr ctx) ARROW (toCST expr ctx))
+ single [BiVoid AtRho] = Nothing
single [bd@(BiVoid _)] = Just (toCST bd ctx)
single [bd@(BiDelta _)] = Just (toCST bd ctx)
single [bd@(BiLambda _)] = Just (toCST bd ctx)
single _ = Nothing
- withoutLastVoidRho :: [Binding] -> [Binding]
- withoutLastVoidRho [] = []
- withoutLastVoidRho [BiVoid AtRho] = []
- withoutLastVoidRho (bd : bds') = bd : withoutLastVoidRho bds'
+ inlined :: PAIR -> Bool
+ inlined PA_FORMATION{voids = _ : _} = True
+ inlined _ = False
toCST (DataString bts) (tabs, _) | sweetString bts = EX_STRING (btsToStr bts) (TAB tabs) []
-- The three canonical non-finite doubles have no sweet numeric literal, so
-- they become the root dispatches `Ξ¦.nan`, `Ξ¦.pinf` and `Ξ¦.ninf`. Any other
@@ -518,28 +520,34 @@
instance ToCST Binding PAIR where
toCST (BiTau attr exp@(ExFormation bds)) ctx =
- let voids' = voids bds
+ let (head', rest) = span positionless bds
+ voids' = [void | BiVoid void <- head']
+ others = filter (not . isVoid) head'
attr' = toCST attr ctx
in if null voids'
then PA_TAU attr' ARROW (toCST exp ctx)
else
- let (_voids, _bds) = if length voids' == length bds && last voids' == AtRho then (init voids', []) else (voids', drop (length voids') bds)
- in PA_FORMATION
- attr'
- (map (`toCST` ctx) _voids)
- ARROW
- (unsugared (toCST (ExFormation _bds) ctx))
+ PA_FORMATION
+ attr'
+ (map (`toCST` ctx) voids')
+ ARROW
+ (unsugared (toCST (ExFormation (others ++ rest)) ctx))
where
-- Inline voids open a formation, which no one-binding sugar may stand
-- for, so 'x(a) β¦ β¦ Ο β¦ ΞΎ.a β§' is never printed as 'x(a) β¦ a:Ο'
unsugared :: EXPRESSION -> EXPRESSION
unsugared EX_SINGLE{..} = formation
unsugared expr = expr
- voids :: [Binding] -> [Attribute]
- voids [] = []
- voids (bd : bds) = case bd of
- BiVoid attr -> attr : voids bds
- _ -> []
+ -- Neither Ξ» nor Ξ is an attribute, so neither holds a position among
+ -- the voids, and 'x β¦ β¦ Ξ» β€ F, a β¦ β β§' is still printed as 'x(a) β¦ β¦ Ξ» β€ F β§'
+ positionless :: Binding -> Bool
+ positionless BiVoid{} = True
+ positionless BiLambda{} = True
+ positionless BiDelta{} = True
+ positionless _ = False
+ isVoid :: Binding -> Bool
+ isVoid BiVoid{} = True
+ isVoid _ = False
toCST (BiTau attr exp) ctx = PA_TAU (toCST attr ctx) ARROW (toCST exp ctx)
toCST (BiVoid attr) ctx = PA_VOID (toCST attr ctx) ARROW EMPTY
toCST (BiDelta bts) ctx = PA_DELTA (toCST bts ctx)
diff --git a/src/Dataize.hs b/src/Dataize.hs
--- a/src/Dataize.hs
+++ b/src/Dataize.hs
@@ -16,12 +16,13 @@
import AST
import Builder (buildBytesThrows, buildExpressionThrows)
import Control.Exception (throwIO, try)
-import Control.Monad (foldM)
+import Control.Monad (foldM, unless)
import Data.List (find)
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Maybe (listToMaybe)
-import Deps (Judgment (..), State (..))
+import qualified Data.Text as T
+import Deps (Evaluation (..), Judgment (..), State (..))
import Locator (locatedExpression)
import Matcher (Subst, matchExpression')
import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, deeper, excluding, execBuildTerm, insideUniverse, leadsTo, morph', normalized, parking, producer, sidePremise, universed, unvisited, verb)
@@ -78,7 +79,10 @@
-- it dataizes β₯. The terminator β₯ signals an error and lies outside π»'s domain,
-- so it matches no clause (there is no 'end' rule mapping it to empty bytes) and
-- dataization stops there; a data-less formation therefore fails through the
--- same path (see #955).
+-- same path (see #955). The dead end is signalled as 'Undataizable', whose
+-- message names the terminator where that is what was reached rather than
+-- reporting the generic "no dataization rule matched", and which an operand of
+-- a firing parks on under '_partial' (see 'reduction', #1401).
-- 'box' contextualizes the Ο-body and keeps dataizing (its step is labelled by
-- its 'contextualize' side-computation), and 'norm' reduces through morphing,
-- splicing the morphing steps into the chain. The clauses are disjoint (see
@@ -106,7 +110,7 @@
matched <- firstMatch ctx rules
case matched of
Just (rule, subst) -> reduce ctx rule subst
- Nothing -> throwIO (userError (unmatched expr))
+ Nothing -> throwIO (Undataizable expr state)
where
-- The symbol a formation carries in place of a Ξ» name, if any. Such a
-- formation is what a Ξ» function answered with where it could not work the
@@ -125,13 +129,6 @@
manufactured idx ctx = do
seq' <- leadsTo seq "symbol" (ExBytes datum) ctx
pure ((datum, NE.toList seq'), state{_manufactured = Just idx})
- -- π» is partial: the terminator β₯ signals an error and lies outside its
- -- domain (see #955), so it matches no clause and lands here. Name it in the
- -- message rather than reporting the generic "no dataization rule matched",
- -- which would otherwise hide that the computation reached a dead end.
- unmatched :: Expression -> String
- unmatched ExTermination = "dataization reached the terminator β₯, which signals an error and cannot be dataized"
- unmatched _ = "no dataization rule matched"
firstMatch :: ReduceContext -> [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))
firstMatch _ [] = pure Nothing
firstMatch ctx (rule : rest) = do
@@ -213,12 +210,29 @@
-- the run bounds the nesting, and the state π goes in and comes back out, so
-- the symbols this reduction mints are counted in the same sequence as the ones
-- around it.
+--
+-- An operand reaching a term outside the domain of π» β 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 under '_partial' it
+-- leaves the firing stuck the same way rather than ending the run: an unfilled
+-- void or an error object is as much a property of the program as a Ξ» function
+-- nobody answers (#1401). The protocol records the dead end as a stuck site
+-- named 'β₯', written with the term π» could not dataize, and the name travels
+-- back in the state as the one the firing got stuck on (see '_stuck'). A run
+-- of π» that is not an operand still fails on it, '_partial' or not (#955).
reduction :: ReductionFunc
reduction univ ctx expr state = do
(universe, aiming) <- insideUniverse expr univ ctx
- (outcome, _, state') <- dataize universe state aiming
- pure (reached outcome, state')
+ result <- try (dataize universe state aiming)
+ case result of
+ Right (outcome, _, state') -> pure (reached outcome, state')
+ Left (Undataizable term state') | ctx._partial -> do
+ unless (dead `elem` ctx._parked) (ctx._saveEval (EvStuck ctx._nesting dead Dataization term))
+ pure (Nothing, state'{_stuck = Just dead})
+ Left failure -> throwIO failure
where
+ dead :: T.Text
+ dead = "β₯"
reached :: Outcome -> Maybe Bytes
reached (Dataized bytes) = Just bytes
reached (Residual _) = Nothing
diff --git a/src/Deps.hs b/src/Deps.hs
--- a/src/Deps.hs
+++ b/src/Deps.hs
@@ -14,6 +14,7 @@
import AST
import Data.IORef (IORef, readIORef, writeIORef)
+import Data.List (intercalate)
import qualified Data.Map.Strict as Map
import Data.Maybe (fromMaybe)
import qualified Data.Text as T
@@ -163,7 +164,9 @@
-- commented with, since nothing of the calculus runs here: the line names
-- a meta the entry bound above it, the way a 'join' line names the two it
-- joined, where an operand line names the judgment that reduced it
- -- (#1306).
+ -- (#1306). A 'rewrite' line is written the same way and for the same
+ -- reason: it applies the rules of the entry to a meta bound above it and
+ -- reduces nothing either (#1409).
EvSymbolize Int T.Text Expression Expression
| -- What is known about a symbol a 'symbolize' line minted: dataizing the
-- formation the symbol names answers these bytes. It is a fact about the
@@ -185,6 +188,14 @@
-- knows which of them belongs to which branch. It is a fact about the
-- symbol and no binding of it, exactly as 'EvKnown' is (#1246).
EvJoined Int Int (Int, Int)
+ | -- A 'join' line one of whose two terms is β₯, which is how a program
+ -- spells "raise unless the condition holds": what the condition of the
+ -- fork came down to β the first operand the entry dataized, a symbol or
+ -- data, where it dataized any β the side that raises, 'left' or 'right' in
+ -- the order the entry wrote the two metas, and the meta holding the β₯. It
+ -- stands ahead of the 'join' line, which binds the other side, so a reader
+ -- renders the record as a throw on that side of the condition (#1405).
+ EvRaiseIf Int (Maybe (Either Int Bytes)) T.Text T.Text
| -- A fresh symbol the answer of the firing asked for, one record per bare π
-- the entry wrote it with. It is a fact about the firing and no property of
-- any one term of it, since an answer may carry several symbols or none and
@@ -368,6 +379,13 @@
left <- render (standing one)
right <- render (standing two)
pure (protocol, Just (indented depth (printf "π»(%s) β { π»(%s), π»(%s) }" form left right)))
+ written (EvRaiseIf depth condition side raised) protocol = do
+ cond <- maybe (pure []) (fmap pure . spelled) condition
+ pure (protocol, Just (indented depth (printf "raise-if(%s) # %s" (intercalate ", " (cond ++ [T.unpack side])) (T.unpack raised))))
+ where
+ spelled :: Either Int Bytes -> IO String
+ spelled (Left symbol) = printf "π»(%s)" <$> render (standing symbol)
+ spelled (Right bytes) = pure (printBytes bytes)
written (EvMinted _ _) protocol = pure (protocol, Nothing)
written (EvBuilt depth term) protocol = do
value <- borrowed protocol term
@@ -546,6 +564,17 @@
(kept, closers) = closed depth nesting._closing
joint :: String
joint = printf "%s %s" (sigma fresh) (sigma one) (sigma two)
+ elements (EvRaiseIf depth condition side _) nesting =
+ pure (nesting{_closing = kept}, closers ++ [indented depth raise])
+ where
+ (kept, closers) = closed depth nesting._closing
+ -- The condition a symbol stands for is named by it, the way 'joined'
+ -- names one, and data the condition came down to is the text.
+ raise :: String
+ raise = case condition of
+ Just (Left symbol) -> printf "" (sigma symbol) (quoted side)
+ Just (Right bytes) -> printf "%s" (quoted side) (escapeXMLText (printBytes bytes))
+ Nothing -> printf "" (quoted side)
elements (EvMinted depth symbol) nesting =
pure (nesting{_closing = kept}, closers ++ [indented depth (printf "%s" (sigma symbol))])
where
diff --git a/src/Evaluate.hs b/src/Evaluate.hs
--- a/src/Evaluate.hs
+++ b/src/Evaluate.hs
@@ -22,15 +22,17 @@
import Control.Monad (foldM, unless)
import Data.List (partition)
import Data.List.NonEmpty (NonEmpty (..))
-import Data.Maybe (fromMaybe, isNothing)
+import Data.Maybe (fromMaybe, isNothing, listToMaybe)
import qualified Data.Text as T
import Deps (BuildTermMethodS, Evaluation (..), State (..), Term (..))
import Lambdas (Lambda (..), Meta (..), joined, matched, minted, symbolized)
import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)
import Morph (ReduceContext (..), ReduceException (..), deeper, morph', morphing, normalized, unparked)
import Printer (printFunction)
+import Rule (RuleContext (RuleContext), matchExpressionWithRule')
import Text.Printf (printf)
import Yaml (ExtraArgument (..))
+import qualified Yaml as Y
-- The Evaluation function πΌ(b, e, s): it fires the Ξ» function of a formation
-- 'b' against the global universe 'e', under the incoming state π , normalizes
@@ -129,10 +131,11 @@
Just entry -> do
caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)
let ctx = caller{_nesting = caller._nesting + 1}
- (bound, dataized) <- foldM (down ctx) (substEmpty, state) entry._dataized
+ (bound, dataized, conditions) <- foldM (down ctx) (substEmpty, state, []) entry._dataized
(bound', morphed) <- foldM (through ctx) (bound, dataized) entry._morphed
- (bound'', stood) <- foldM (masked ctx) (bound', morphed) entry._symbolized
- (bound''', forked) <- foldM (paired ctx) (bound'', stood) entry._paired
+ rewrote <- foldM (reshaped ctx) bound' entry._rewritten
+ (bound'', stood) <- foldM (masked ctx) (rewrote, morphed) entry._symbolized
+ (bound''', forked) <- foldM (paired ctx (listToMaybe (reverse conditions))) (bound'', stood) entry._paired
answered ctx entry bound''' forked
where
-- Bring one 'dataize' operand down through π» and bind the bytes meta that
@@ -153,15 +156,20 @@
-- it and lets the spine frame around this firing attach its own, which is
-- what keeps '--sequence' free of the synthetic attribute the operand was
-- reduced under.
- down :: ReduceContext -> (Subst, State) -> (Meta, Expression) -> IO (Subst, State)
- down ctx (bound, state') (meta, term) = do
+ --
+ -- What the operand came down to goes on beside the substitution, the last
+ -- operand first, since the first of them is the condition a fork branches
+ -- on and a 'join' line one side of which reaches β₯ names it (see 'paired').
+ down :: ReduceContext -> (Subst, State, [Either Int Bytes]) -> (Meta, Expression) -> IO (Subst, State, [Either Int Bytes])
+ down ctx (bound, state', conditions) (meta, term) = do
(value, state'') <- unparked (ctx._reduce univ ctx (operand term) state'{_manufactured = Nothing, _stuck = Nothing})
case value of
Nothing -> throwIO (Stuck (fromMaybe func state''._stuck))
Just bytes -> do
- ctx._saveEval (EvData ctx._nesting meta._spelling term (maybe (Right bytes) Left state''._manufactured))
+ let datum = maybe (Right bytes) Left state''._manufactured
+ ctx._saveEval (EvData ctx._nesting meta._spelling term datum)
bound' <- bind meta (MvBytes bytes) bound
- pure (bound', state'')
+ pure (bound', state'', datum : conditions)
-- Reduce one 'morph' operand through π and bind the expression meta that
-- names it. Unlike a dataized one it may stay an unknown: a term carrying a
-- symbol is a perfectly good normal form, and standing it into the answer
@@ -172,6 +180,20 @@
ctx._saveEval (EvTerm ctx._nesting meta._spelling term normal)
bound' <- bind meta (MvExpression normal) bound
pure (bound', state'')
+ -- Rewrite a term another line of the entry has bound with the rules of the
+ -- line and bind the expression meta naming what it becomes (see
+ -- 'rewritten'). Nothing is reduced and nothing is minted: a rewrite is a
+ -- substitution the entry vouches for, exactly as an answer is, so the term
+ -- it makes is written to the protocol and bound as it is, which is what
+ -- lets a program bring the branches of a fork to one shape before they
+ -- are compared (#1409). The line is commented with the meta it rewrote,
+ -- the way a 'symbolize' line is, since no judgment of the calculus made it.
+ reshaped :: ReduceContext -> Subst -> (Meta, (Meta, [Y.Rule])) -> IO Subst
+ reshaped ctx bound (meta, (source, rules)) = do
+ term <- buildExpressionThrows (ExMeta source._name) bound
+ shaped <- rewritten rules (RuleContext ctx._buildTerm) term
+ ctx._saveEval (EvSymbolize ctx._nesting meta._spelling (ExMeta source._name) shaped)
+ bind meta (MvExpression shaped) bound
-- Stand the data of a term another line of the entry has bound into
-- unknowns and bind the expression meta naming what it becomes. Nothing is
-- reduced here: what changes is that every datum of the term becomes a
@@ -205,18 +227,43 @@
-- the line binding the term, the way a 'symbolize' line writes what it
-- knows, since a reader ties the join to the two values it was made from
-- by that fact alone and never by diffing the terms.
- paired :: ReduceContext -> (Subst, State) -> (Meta, (Meta, Meta)) -> IO (Subst, State)
- paired ctx (bound, state') (meta, (left, right)) = do
+ --
+ -- One side reaching β₯ is a join too, the one 'if. cond value β₯' spells
+ -- "raise unless cond" with: the program raises on that side of the
+ -- condition and has a perfectly good value on the other. The protocol is
+ -- told on which side it raises, naming the condition by what the first
+ -- operand the entry dataized came down to, and the meta is bound to the
+ -- other side as it stands, which is the one value the fork can still
+ -- answer with. Both sides reaching β₯ is no such case: they are one term
+ -- and join into β₯ verbatim (#1405).
+ paired :: ReduceContext -> Maybe (Either Int Bytes) -> (Subst, State) -> (Meta, (Meta, Meta)) -> IO (Subst, State)
+ paired ctx condition (bound, state') (meta, (left, right)) = do
one <- branch left
two <- branch right
- case joined one two state'._minted of
- Nothing -> throwIO (Stuck func)
- Just (term, made, spent) -> do
- mapM_ (ctx._saveEval . fact) made
+ case (one, two) of
+ (ExTermination, ExTermination) -> both one two
+ (ExTermination, _) -> raising "left" left two
+ (_, ExTermination) -> raising "right" right one
+ _ -> both one two
+ where
+ -- The two sides joined symbol by symbol (see 'joined').
+ both :: Expression -> Expression -> IO (Subst, State)
+ both one two = case joined one two state'._minted of
+ Nothing -> throwIO (Stuck func)
+ Just (term, made, spent) -> do
+ mapM_ (ctx._saveEval . fact) made
+ ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
+ bound' <- bind meta (MvExpression term) bound
+ pure (bound', state'{_minted = spent})
+ -- The side that raises written down, named by the meta holding its β₯,
+ -- and the other side bound as the join; nothing is minted, since one
+ -- value is left and a symbol would stand for nothing but it.
+ raising :: T.Text -> Meta -> Expression -> IO (Subst, State)
+ raising side raised term = do
+ ctx._saveEval (EvRaiseIf ctx._nesting condition side raised._spelling)
ctx._saveEval (EvJoin ctx._nesting meta._spelling (left._spelling, right._spelling) term)
bound' <- bind meta (MvExpression term) bound
- pure (bound', state'{_minted = spent})
- where
+ pure (bound', state')
-- The term one side of the join is bound to, which is what a meta of
-- the entry reads out of the substitution the firing has made (see
-- 'earlier' in 'Lambdas': a 'join' line names metas bound above it and
@@ -275,6 +322,43 @@
throwIO
(userError (printf "The meta '%s' of Ξ» function '%s' clashes with an existing binding" (T.unpack meta._spelling) (T.unpack func)))
+-- The term with the rules of a 'rewrite' line applied to it. Every position of
+-- the term is tried, the outermost first, and the first rule whose pattern
+-- matches a position as a whole rewrites it with the first match it made; the
+-- position rewritten is not walked into again, so a rule whose result carries
+-- its own pattern rewrites it once and never loops. A position no rule matches
+-- is walked into, every binding and every argument of it, Ο among them, since
+-- the shape of a branch is the program's to say and phino has no say in where
+-- that shape is written. Nothing is normalized afterwards: the rules are the
+-- program's word on what one term stands for, and reducing their outcome would
+-- have phino second-guess it (#1409).
+rewritten :: [Y.Rule] -> RuleContext -> Expression -> IO Expression
+rewritten rules ctx = goExpr
+ where
+ goExpr :: Expression -> IO Expression
+ goExpr expr = goRules rules
+ where
+ goRules :: [Y.Rule] -> IO Expression
+ goRules [] = inside expr
+ goRules (rule : rest) = do
+ substs <- matchExpressionWithRule' [substEmpty] expr rule ctx
+ case substs of
+ subst : _ -> buildExpressionThrows rule.result subst
+ [] -> goRules rest
+ inside :: Expression -> IO Expression
+ inside (ExFormation bds) = ExFormation <$> mapM goBinding bds
+ inside (ExApplication expr arg) = ExApplication <$> goExpr expr <*> goArgument arg
+ inside (ExDispatch expr attr) = (`ExDispatch` attr) <$> goExpr expr
+ inside (ExPhiMeet prefix idx expr) = ExPhiMeet prefix idx <$> goExpr expr
+ inside (ExPhiAgain prefix idx expr) = ExPhiAgain prefix idx <$> goExpr expr
+ inside expr = pure expr
+ goBinding :: Binding -> IO Binding
+ goBinding (BiTau attr expr) = BiTau attr <$> goExpr expr
+ goBinding bd = pure bd
+ goArgument :: Argument -> IO Argument
+ goArgument (ArTau attr expr) = ArTau attr <$> goExpr expr
+ goArgument (ArAlpha alpha expr) = ArAlpha alpha <$> goExpr expr
+
-- Ask π about a term and fire the Ξ» of the formation it reaches, as long as an
-- entry of the '--symbolic' file answers it, asking π about every answer again:
-- what comes back is the answer of the last firing, or nothing at all where
@@ -293,7 +377,7 @@
morphed <- try (reduced ctx)
case morphed of
Right (ExFormation bds, state')
- | demanded bds -> maybe (pure (Nothing, state')) (evaluated ctx state' (ExFormation bds)) (saturated bds)
+ | demanded bds -> maybe (pure (Nothing, state')) (evaluated ctx state' (ExFormation bds)) (saturated term bds)
Right (_, state') -> pure (Nothing, state')
Left failure -> parked state failure
where
@@ -404,17 +488,56 @@
-- fires only what dataization demands and nothing demands a method; the deep
-- walk meets every one a program declares β the method table of the object
-- model above all β so it asks first (see 'deepened').
-saturated :: [Binding] -> Maybe (T.Text, Expression)
-saturated bds = case lambda bds of
- Just (func, ExFormation rest) | all filled rest -> Just (func, ExFormation rest)
+--
+-- A binding holding β₯ counts as filled only where the term the walk was handed
+-- wrote that β₯ as an argument itself. A β₯ the reduction made is no argument:
+-- the deep walk reduces a body in the scope of the formation around it, and a
+-- formation declaring Ο and standing unapplied still holds Ο β¦ β , so a ΞΎ.Ο in
+-- that body comes back as β₯ rather than as the object the next dispatch
+-- supplies (#1196). A β₯
+-- written as an argument is what the program meant, and 'if. cond value β₯' is
+-- how it spells "raise unless cond", so a fork like that fires and its join
+-- says on which side it raises (#1405). An argument given by name covers the
+-- binding of that name; one given by position covers some binding, so there
+-- have to be as many of them as β₯ bindings no name covers. A term handing
+-- nothing but β₯ is still left alone, since there is no value for a firing to
+-- work with and all it could do is get stuck on one of them.
+saturated :: Expression -> [Binding] -> Maybe (T.Text, Expression)
+saturated term bds = case lambda bds of
+ Just (func, ExFormation rest)
+ | all filled rest && (not (any raising rest) || given rest) -> Just (func, ExFormation rest)
_ -> Nothing
+ where
+ named :: [Attribute]
+ positional :: Int
+ valued :: Bool
+ (named, positional, valued) = written term
+ -- Whether every β₯ of the bindings is one the term wrote, beside some
+ -- argument that is not β₯.
+ given :: [Binding] -> Bool
+ given rest = valued && length (filter unwritten rest) <= positional
+ raising :: Binding -> Bool
+ raising (BiTau _ ExTermination) = True
+ raising _ = False
+ -- Whether a binding holds a β₯ no argument given by name wrote.
+ unwritten :: Binding -> Bool
+ unwritten (BiTau attr ExTermination) = attr `notElem` named
+ unwritten _ = False
+ -- The attributes the application chain of a term hands a literal β₯ by
+ -- name, how many literal β₯ it hands by position, and whether it hands
+ -- anything but β₯ at all.
+ written :: Expression -> ([Attribute], Int, Bool)
+ written (ExApplication expr (ArTau attr ExTermination)) =
+ let (attrs, count, other) = written expr in (attr : attrs, count, other)
+ written (ExApplication expr (ArAlpha _ ExTermination)) =
+ let (attrs, count, other) = written expr in (attrs, count + 1, other)
+ written (ExApplication expr _) =
+ let (attrs, count, _) = written expr in (attrs, count, True)
+ written _ = ([], 0, False)
-- Whether a binding hands the formation something to work with. A void does
--- not: it names an argument the program has still to supply. Neither does β₯:
--- the deep walk reduces a body in the scope of the formation around it, and a
--- formation standing unapplied still holds Ο β¦ β , so a ΞΎ.Ο in that body comes
--- back as β₯ rather than as the object the next dispatch supplies (#1196).
+-- not: it names an argument the program has still to supply. A β₯ is told
+-- apart by 'saturated', which knows the term it was written in.
filled :: Binding -> Bool
filled (BiVoid _) = False
-filled (BiTau _ ExTermination) = False
filled _ = True
diff --git a/src/Filter.hs b/src/Filter.hs
--- a/src/Filter.hs
+++ b/src/Filter.hs
@@ -38,7 +38,7 @@
forms -> mergeForms forms
where
def :: Expression
- def = ExFormation [BiVoid AtRho]
+ def = ExFormation []
pick :: Expression -> Maybe Expression
pick fqn = do
attrs <- fqnToAttrs fqn
@@ -47,12 +47,12 @@
mergeForms forms =
let bds = concat [bs | ExFormation bs <- forms]
bds' = filter (\bd -> attributeFromBinding bd /= Just AtRho) bds
- in ExFormation (withVoidRho bds')
+ in ExFormation bds'
includedFormation :: Expression -> [Attribute] -> Maybe Expression
includedFormation (ExFormation bindings) [at] =
let bs = [bd | bd <- bindings, attributeFromBinding bd == Just at]
- in if null bs then Nothing else Just (ExFormation (withVoidRho bs))
- includedFormation (ExFormation bindings) atts = includedBindings bindings atts >>= (Just . ExFormation . (: [BiVoid AtRho]))
+ in if null bs then Nothing else Just (ExFormation bs)
+ includedFormation (ExFormation bindings) atts = includedBindings bindings atts >>= (Just . ExFormation . pure)
where
includedBindings :: [Binding] -> [Attribute] -> Maybe Binding
includedBindings ((BiTau at' form@(ExFormation _)) : bs) as@(at'' : rs)
diff --git a/src/LaTeX.hs b/src/LaTeX.hs
--- a/src/LaTeX.hs
+++ b/src/LaTeX.hs
@@ -333,8 +333,10 @@
toLaTeX B = B'
toLaTeX D = D'
toLaTeX D'' = D'
- toLaTeX F = F'
- toLaTeX S = S'
+ toLaTeX F = F''
+ toLaTeX F' = F''
+ toLaTeX S = S''
+ toLaTeX S' = S''
toLaTeX mh = mh
instance ToLaTeX BYTES where
diff --git a/src/Lambdas.hs b/src/Lambdas.hs
--- a/src/Lambdas.hs
+++ b/src/Lambdas.hs
@@ -27,14 +27,23 @@
-- under 'π' is what the firing answers with, and a bare π in it mints a fresh
-- symbol.
--
--- 'symbolize' is the third block and reduces nothing at all. It takes a term
+-- 'rewrite' is the third block and reduces nothing either. Each line of it
+-- names a meta the entry has bound already under 'of' and a list of ordinary
+-- rules under 'rules', spelled the way a rule file spells one, and binds an
+-- expression meta of its own to that term with the rules applied to it (see
+-- 'rewritten' in 'Evaluate'). It is how a program brings two branches of a
+-- fork to one shape before they are compared: one literal of a bool and the
+-- answer of a firing are one value in two spellings, and nothing but the
+-- program knows that (#1409).
+--
+-- 'symbolize' is the fourth block and reduces nothing at all. It takes a term
-- an earlier block of the very same entry has already bound and binds an
-- expression meta of its own to that term with every datum in it standing for
-- an unknown, so a normal form reached from a literal is written the way one
-- reached from an unknown is written and the two of them compare as
-- expressions (see 'symbolized').
--
--- 'join' is the fourth block and reduces nothing either. It takes two metas the
+-- 'join' is the fifth block and reduces nothing either. It takes two metas the
-- entry has bound already and binds one of its own to the two terms joined,
-- which is what a branching Ξ» function answers with: a fork stands for either
-- of its branches and no one branch stands for both, so the shape both of them
@@ -69,7 +78,7 @@
import AST
import Control.Exception (Exception, throwIO)
import Control.Monad (void)
-import Data.Aeson (FromJSON (parseJSON), Key, Object, withObject, (.!=), (.:), (.:?))
+import Data.Aeson (FromJSON (parseJSON), Key, Object, Value (Object), withObject, (.!=), (.:), (.:?))
import Data.List (find)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
@@ -78,12 +87,14 @@
import Data.Text.Encoding (encodeUtf8)
import qualified Data.Yaml as Yaml
import Logger (logDebug)
+import Metas (Metas (metas))
import Parser (parseBytes, parseExpression)
import Slots (Slots (slots))
import Text.Printf (printf)
import Text.Regex.PCRE (matchTest)
import Text.Regex.PCRE.ByteString (Regex, compUTF8, compile, execBlank)
import Yaml (referenceless)
+import qualified Yaml as Y
-- One meta an entry of the file binds: the name the file spells it with, which
-- is the name the protocol of '--protocol' reports it back under, and the name
@@ -98,13 +109,14 @@
-- One Ξ» function phino may fire, as the file spells it: the key it is
-- registered under, the operands it brings down to data, the operands it
--- reduces to a normal form, the terms of those it stands the data of into
--- unknowns, the pairs of those it joins into one term and the term it answers
+-- reduces to a normal form, the terms of those it rewrites with rules of its
+-- own, the terms of those it stands the data of into unknowns, the pairs of those it joins into one term and the term it answers
-- with.
data Lambda = Lambda
{ _key :: Text
, _dataized :: [(Meta, Expression)]
, _morphed :: [(Meta, Expression)]
+ , _rewritten :: [(Meta, (Meta, [Y.Rule]))]
, _symbolized :: [(Meta, Expression)]
, _paired :: [(Meta, (Meta, Meta))]
, _answer :: Expression
@@ -133,6 +145,7 @@
Lambda key
<$> operands key bytesMeta entry "dataize"
<*> operands key expressionMeta entry "morph"
+ <*> rewrites (T.unpack key) entry
<*> operands key expressionMeta entry "symbolize"
<*> pairs (T.unpack key) entry
<*> entry .: "π"
@@ -188,17 +201,73 @@
(T.unpack meta)
key
)
- -- Every 'symbolize' and 'join' line reads terms the entry has bound
- -- already: a 'morph' operand, a line above it in its own block or, for a
- -- 'join' line, a 'symbolize' one, since nothing else of an entry is a
+ -- The metas a 'rewrite' block binds, each paired with the meta whose
+ -- term it rewrites and the rules it rewrites that term with, ordered by
+ -- the name of the meta the way every other block is. A rule is read the
+ -- way a rule file reads one, and on top of that a rule writing a symbol
+ -- into its result or reading a meta its match never bound is refused
+ -- here: a symbol is minted by a firing and never spelled by hand, and a
+ -- meta nothing bound is one the rule cannot be built with.
+ rewrites :: String -> Object -> Yaml.Parser [(Meta, (Meta, [Y.Rule]))]
+ rewrites key entry = do
+ mapping <- entry .:? "rewrite" .!= (Map.empty :: Map Text Object)
+ mapM line (Map.toAscList mapping)
+ where
+ line :: (Text, Object) -> Yaml.Parser (Meta, (Meta, [Y.Rule]))
+ line (meta, body) = do
+ named <- expressionMeta meta
+ source <- body .: "of" >>= expressionMeta
+ written <- body .: "rules"
+ rules <- mapM rule written
+ pure (named, (source, rules))
+ rule :: Object -> Yaml.Parser Y.Rule
+ rule body = do
+ result <- body .: "result"
+ symbolless result
+ parsed <- parseJSON (Object body)
+ bound parsed
+ pure parsed
+ -- A bare π or a numbered one written into a result: the one names a
+ -- symbol a rewrite has no business minting, since it is a
+ -- substitution the entry vouches for and no firing, and the other
+ -- one nobody minted at all.
+ symbolless :: Expression -> Yaml.Parser ()
+ symbolless result
+ | null (symbols result) && null [kind | Slot kind _ <- slots result, kind == "S"] = pure ()
+ | otherwise = fail (printf "A rule of the 'rewrite' block of Ξ» function '%s' writes a symbol π into its result" key)
+ -- Every meta a result reads is one the pattern, the 'e-match' or a
+ -- 'where' extension of the very same rule binds.
+ bound :: Y.Rule -> Yaml.Parser ()
+ bound parsed = case filter (`notElem` known) (metas parsed.result) of
+ [] -> pure ()
+ meta : _ ->
+ fail
+ ( printf
+ "The rule '%s' of the 'rewrite' block of Ξ» function '%s' reads the meta '%s' it never binds"
+ parsed.name
+ key
+ (T.unpack meta)
+ )
+ where
+ known :: [Text]
+ known = metas parsed.pattern ++ metas parsed.ematch ++ concatMap (metas . (.meta)) (concat parsed.where_)
+ -- Every 'rewrite', 'symbolize' and 'join' line reads terms the entry has
+ -- bound already: a 'morph' operand, a line above it in its own block or
+ -- a line of a block above its own, since nothing else of an entry is a
-- normal form yet and the blocks run in the order the entry lists them
-- here. A line naming anything else names a term nobody reduced, and the
-- file is wrong where it is read rather than half-way through a firing.
earlier :: String -> Lambda -> Yaml.Parser ()
earlier key lambda = do
- stood <- go (map (_name . fst) lambda._morphed) lambda._symbolized
+ rewrote <- goRewrites (map (_name . fst) lambda._morphed) lambda._rewritten
+ stood <- go rewrote lambda._symbolized
void (goJoins stood lambda._paired)
where
+ goRewrites :: [Text] -> [(Meta, (Meta, [Y.Rule]))] -> Yaml.Parser [Text]
+ goRewrites reduced [] = pure reduced
+ goRewrites reduced ((meta, (source, _)) : rest)
+ | source._name `elem` reduced = goRewrites (meta._name : reduced) rest
+ | otherwise = unbound source
go :: [Text] -> [(Meta, Expression)] -> Yaml.Parser [Text]
go reduced [] = pure reduced
go reduced ((meta, term) : rest) = case term of
@@ -440,9 +509,9 @@
-- binding one of them carries and the other does not β is no join, and nothing
-- comes back: a fork whose branches differ in structure is stuck the way a Ξ»
-- function no entry answers is, and bringing two such branches to one shape is
--- the program's business rather than phino's. This is why a datum is never
--- joined with anything and why a branch carrying one goes through 'symbolized'
--- first (#1246).
+-- the program's business rather than phino's, which its entry does in a
+-- 'rewrite' block (#1409). This is why a datum is never joined with anything
+-- and why a branch carrying one goes through 'symbolized' first (#1246).
--
-- What each fresh symbol stands for comes back beside the term, the two
-- symbols it was minted for in the order the branches were given, since
diff --git a/src/Misc.hs b/src/Misc.hs
--- a/src/Misc.hs
+++ b/src/Misc.hs
@@ -3,9 +3,7 @@
-- This module provides commonly used helper functions for other modules
module Misc
- ( withVoidRho
- , recoverFormations
- , toDouble
+ ( toDouble
, fqnToAttrs
, attributesFromBindings
, attributesFromBindings'
@@ -70,41 +68,6 @@
| attr `Set.member` seen -> Just attr
| otherwise -> duplicated rest (Set.insert attr seen)
Nothing -> duplicated rest seen
-
--- Add void rho binding to the end of the list of any rho binding is not present
-withVoidRho :: [Binding] -> [Binding]
-withVoidRho bds = go bds False
- where
- go :: [Binding] -> Bool -> [Binding]
- go [] hasRho = [BiVoid AtRho | not hasRho]
- go (bd : rest) hasRho =
- case bd of
- BiMeta _ -> bd : rest
- BiAny _ -> bd : rest
- BiVoid (AtMeta _) -> bd : rest
- BiVoid (AtAny _) -> bd : rest
- BiTau (AtMeta _) _ -> bd : rest
- BiTau (AtAny _) _ -> bd : rest
- BiVoid AtRho -> bd : go rest True
- BiTau AtRho _ -> bd : go rest True
- _ -> bd : go rest hasRho
-
--- Recursively ensure all formations have a BiVoid AtRho binding (Ο β¦ β ).
--- Fixes in-memory ExFormation [] to ExFormation [BiVoid AtRho] after rewriting,
--- keeping the invariant that the parser enforces via withVoidRho.
-recoverFormations :: Expression -> Expression
-recoverFormations (ExFormation bindings) = ExFormation (withVoidRho (map recoverFormations' bindings))
-recoverFormations (ExDispatch expr attr) = ExDispatch (recoverFormations expr) attr
-recoverFormations (ExApplication expr arg) = ExApplication (recoverFormations expr) (recoverArgument arg)
-recoverFormations expr = expr
-
-recoverFormations' :: Binding -> Binding
-recoverFormations' (BiTau attr expr) = BiTau attr (recoverFormations expr)
-recoverFormations' binding = binding
-
-recoverArgument :: Argument -> Argument
-recoverArgument (ArTau attr expr) = ArTau attr (recoverFormations expr)
-recoverArgument (ArAlpha alpha expr) = ArAlpha alpha (recoverFormations expr)
-- Transform dispatch to list of attributes
-- >>> fqnToAttrs (ExDispatch (ExDispatch (ExDispatch ExRoot (AtLabel "org")) (AtLabel "eolang")) (AtLabel "number"))
diff --git a/src/Morph.hs b/src/Morph.hs
--- a/src/Morph.hs
+++ b/src/Morph.hs
@@ -208,6 +208,14 @@
-- working expression β the term that came back left exactly where it stood,
-- the way an exhausted budget stops on the last step it could afford.
LoopingAt Expression (NonEmpty Rewritten) State
+ | -- π» was handed a term outside its domain: the terminator β₯, which signals
+ -- an error (see #955), or a term no dataization rule matches, such as a
+ -- formation whose Ο is a void nothing filled. It carries the term and the
+ -- state the frame that met it had reached. A run of π» fails on it, with or
+ -- without '_partial', but an operand of a firing that meets it parks that
+ -- firing under '_partial' the way an unanswered Ξ» function does, since the
+ -- dead end is a property of the program rather than of phino (#1401).
+ Undataizable Expression State
deriving anyclass (Exception)
instance Show ReduceException where
@@ -218,6 +226,8 @@
show (StuckAt func _ _) = show (Stuck func)
show (Looping term) = printf "Reduction came back to a term it is already reducing: %s" (printExpression term)
show (LoopingAt term _ _) = show (Looping term)
+ show (Undataizable ExTermination _) = "dataization reached the terminator β₯, which signals an error and cannot be dataized"
+ show (Undataizable _ _) = "no dataization rule matched"
-- Charge one step of the π/π» recursion to the budget, refusing to descend once
-- it is gone. '--max-cycles' and '--max-depth' bound only the normalization run
@@ -476,9 +486,9 @@
-- bound in has its own Ο bound: Ο is the parameter a dispatch binds, and
-- 'dot' binds it in every copy a reduction reaches, so a formation still
-- holding Ο β¦ β inside such a copy is a method nobody dispatched, and its
- -- ΞΎ.Ο can only collapse to β₯ (#1397). The program as it was written holds
- -- Ο β¦ β all the way down, since nothing dispatched it either, and its
- -- objects are walked the way they always were.
+ -- ΞΎ.Ο can only collapse to β₯ (#1397). In the program as it was written
+ -- nothing is dispatched yet, so the void Ο an object declares there keeps
+ -- it from nothing and its objects are walked the way they always were.
parts :: Bool -> Maybe Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State)
parts attached _ _ term@(ExFormation bds) state' _
| any abstract bds = pure (term, state')
diff --git a/src/Parser.hs b/src/Parser.hs
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -315,7 +315,7 @@
_ <- arrow
bs <- formationBindings
bds <- validatedBindings (voids ++ bs)
- return (ExFormation (withVoidRho bds))
+ return (ExFormation bds)
]
where
rb :: Parser String
@@ -341,7 +341,7 @@
-- could be taken for and opened by a look at a character it must start with,
-- so the heads a program is mostly made of never try it.
alone :: Parser Binding -> Parser Expression
-alone bd = ExFormation . withVoidRho . pure <$> bd
+alone bd = ExFormation . pure <$> bd
-- `FF-AA:Ξ`, `--:D` or `πΏ1:Ξ`
deltaHead :: Parser Expression
@@ -487,7 +487,7 @@
choice
[ do
bs <- formationBindings >>= validatedBindings
- return (ExFormation (withVoidRho bs))
+ return (ExFormation bs)
, do
_ <- choice [symbol "$", symbol "ΞΎ"]
return ExXi
@@ -542,7 +542,7 @@
return (application expr bds)
, do
_ <- colon
- ExFormation . withVoidRho . pure . (`BiTau` expr) <$> attribute
+ ExFormation . pure . (`BiTau` expr) <$> attribute
]
"dispatch or application"
exTail next
diff --git a/src/Render.hs b/src/Render.hs
--- a/src/Render.hs
+++ b/src/Render.hs
@@ -133,8 +133,10 @@
render D'' = "d"
render F = "π"
render F' = "F"
+ render F'' = "f"
render S = "π"
render S' = "S"
+ render S'' = "\\sigma"
instance Render META where
render META{..} = render excl <> render hd <> render rest
diff --git a/src/Rewriter.hs b/src/Rewriter.hs
--- a/src/Rewriter.hs
+++ b/src/Rewriter.hs
@@ -22,7 +22,6 @@
import Locator (locatedExpression, withLocatedExpression)
import Logger (logDebug)
import Matcher (Subst)
-import Misc (recoverFormations)
import Must (Must (..), exceedsUpperBound, inRange)
import Printer (printExpression)
import Replacer (ReplaceContext (ReplaceCtx), ReplaceExpressionFunc, replaceExpression, replaceExpressionFast)
@@ -214,7 +213,7 @@
else pure (_rewrittens, _unique, False)
matched -> do
logDebug (printf "Rule '%s' has been matched, applying..." ruleName)
- expr <- recoverFormations <$> tryBuildAndReplaceFast (expression, ptn, res, matched) (ReplaceCtx _maxDepth)
+ expr <- tryBuildAndReplaceFast (expression, ptn, res, matched) (ReplaceCtx _maxDepth)
if expression == expr
then do
logDebug (printf "Applied '%s', no changes made" ruleName)
diff --git a/src/Sugar.hs b/src/Sugar.hs
--- a/src/Sugar.hs
+++ b/src/Sugar.hs
@@ -18,32 +18,11 @@
withSugarType SWEET node = node
withSugarType SALTY node = toSalty node
-voidRho :: PAIR
-voidRho = PA_VOID (AT_RHO RHO) ARROW EMPTY
-
-bdWithVoidRho :: BINDING -> BINDING
-bdWithVoidRho BI_EMPTY{..} = BI_PAIR voidRho (BDS_EMPTY tab) tab
-bdWithVoidRho bd@BI_PAIR{pair = PA_VOID{attr = AT_RHO _}} = bd
-bdWithVoidRho bd@BI_PAIR{pair = PA_TAU{attr = AT_RHO _}} = bd
-bdWithVoidRho bd@BI_PAIR{pair = PA_FORMATION{attr = AT_RHO _}} = bd
-bdWithVoidRho BI_PAIR{..} = BI_PAIR pair (bdsWithVoidRho bindings) tab
- where
- bdsWithVoidRho :: BINDINGS -> BINDINGS
- bdsWithVoidRho BDS_EMPTY{..} = BDS_PAIR EOL tab voidRho (BDS_EMPTY tab)
- bdsWithVoidRho bds@BDS_PAIR{pair = PA_VOID{attr = AT_RHO _}} = bds
- bdsWithVoidRho bds@BDS_PAIR{pair = PA_TAU{attr = AT_RHO _}} = bds
- bdsWithVoidRho bds@BDS_PAIR{pair = PA_FORMATION{attr = AT_RHO _}} = bds
- bdsWithVoidRho BDS_PAIR{..} = BDS_PAIR eol tab pair (bdsWithVoidRho bindings)
- bdsWithVoidRho bds@BDS_META{} = bds
-bdWithVoidRho bd@BI_META{} = bd
-
data SugarType = SWEET | SALTY
deriving (Eq, Show)
-- Drop every Ο binding (Ο β¦ β , Ο β¦ e and Ο(β¦) β¦ e) from a rendered CST, the
--- effect of the '--hide-rho' switch. It runs after 'withSugarType', so it also
--- removes the Ο β¦ β that 'bdWithVoidRho' re-inserts into every formation on the
--- SALTY path. Both formation bindings and application arguments are stripped;
+-- effect of the '--hide-rho' switch. Both formation bindings and application arguments are stripped;
-- dispatches such as ΞΎ.Ο are left untouched. A formation left empty by the
-- strip collapses to the compact 'β¦β§' layout, and an application left with no
-- argument collapses to its bare callee (no leftover 'e()'). In the SWEET
@@ -120,7 +99,14 @@
goPair :: PAIR -> PAIR
goPair PA_TAU{..} = PA_TAU attr arrow (goExpr expr)
goPair PA_ALPHA{..} = PA_ALPHA alpha arrow (goExpr expr)
- goPair PA_FORMATION{..} = PA_FORMATION attr voids arrow (unsugared (goExpr expr))
+ goPair PA_FORMATION{..} = case filter (not . rho) voids of
+ [] -> PA_TAU attr arrow (goExpr expr)
+ voids' -> PA_FORMATION attr voids' arrow (unsugared (goExpr expr))
+ where
+ -- A void Ο the formation declares is listed among its inline voids
+ rho :: ATTRIBUTE -> Bool
+ rho AT_RHO{} = True
+ rho _ = False
goPair pair = pair
-- Inline voids open a formation, which the sugar may not stand for
unsugared :: EXPRESSION -> EXPRESSION
@@ -149,7 +135,6 @@
-- | a -> 42 | Q.number(Q.bytes([[ D> 40-45-00-00-00-00-00-00 ]])) |
-- | a -> Q.nan | Q.number(Q.bytes([[ D> 7F-F8-00-00-00-00-00-00 ]])) |
-- | a -> "Hey" | Q.number(Q.bytes([[ D> 48-65-79 ]])) |
--- | [[ B ]] | [[ B, ^ -> ? ]], if rho is absent in 'B' |
-- | e:a | [[ a -> e ]], and so for D, L and ? (see #1385) |
-- | a1(a2, a3, ...) -> [[ B ]] | a1 -> [[ a2 -> ?, a3 -> ?, ..., B ]] |
-- | e(e0, e1, ...) | e(~0 -> e0, ~1 -> e1, ...) |
@@ -161,8 +146,8 @@
instance ToSalty EXPRESSION where
toSalty EX_ATTR{..} = EX_DISPATCH (EX_XI XI) NO_SPACE attr
toSalty EX_DISPATCH{..} = EX_DISPATCH (toSalty expr) space attr
- toSalty EX_FORMATION{lsb, binding = bd@BI_EMPTY{}, rsb} = EX_FORMATION lsb NO_EOL TAB' (toSalty (bdWithVoidRho bd)) NO_EOL TAB' rsb
- toSalty EX_FORMATION{..} = EX_FORMATION lsb eol tab (toSalty (bdWithVoidRho binding)) eol' tab' rsb
+ toSalty formation@EX_FORMATION{binding = BI_EMPTY{}} = formation
+ toSalty EX_FORMATION{..} = EX_FORMATION lsb eol tab (toSalty binding) eol' tab' rsb
toSalty EX_APPLICATION{argument = AA_TAU tau, ..} = EX_APPLICATION (toSalty expr) space EOL (TAB indent) (AA_TAU (toSalty tau)) EOL (TAB (indent - 1)) indent
toSalty EX_APPLICATION{argument = AA_TAUS taus, ..} =
foldl
diff --git a/src/XMIR.hs b/src/XMIR.hs
--- a/src/XMIR.hs
+++ b/src/XMIR.hs
@@ -170,7 +170,7 @@
formationBinding (BiDelta bytes) _ = pure (Just (NodeContent (T.pack (printBytes bytes))))
formationBinding (BiLambda (Function name)) XmirContext{..} =
pure (Just (object (maybe [] (\atom -> [("atom", atom)]) (M.lookup name _atoms) ++ [("name", show AtLambda)]) [NodeContent name]))
-formationBinding (BiVoid AtRho) _ = pure Nothing
+formationBinding (BiVoid AtRho) _ = pure (Just (object [("name", show AtRho), ("base", "β ")] []))
formationBinding (BiVoid AtPhi) _ = pure (Just (object [("name", show AtPhi), ("base", "β ")] []))
formationBinding (BiVoid (AtLabel label)) _ = pure (Just (object [("name", T.unpack label), ("base", "β ")] []))
formationBinding binding _ = throwIO (UnsupportedBinding binding)
@@ -184,7 +184,7 @@
pure (object [("name", name), ("base", base)] children)
-- Render a formation's bindings as child nodes, honoring '--hide-rho' by
--- dropping every bound Ο before it reaches the nodes (#1076)
+-- dropping every Ο, void or bound, before it reaches the nodes (#1076)
nestedBindings :: [Binding] -> XmirContext -> IO [Node]
nestedBindings bds ctx@XmirContext{..} = catMaybes <$> mapM (`formationBinding` ctx) bds'
where
@@ -192,15 +192,17 @@
bds' = if _hideRho then filter (not . isRho) bds else bds
isRho :: Binding -> Bool
isRho (BiTau AtRho _) = True
+ isRho (BiVoid AtRho) = True
isRho _ = False
expressionToXMIR :: Expression -> XmirContext -> IO Document
-expressionToXMIR expr@(ExFormation [BiTau (AtLabel _) arg, BiVoid AtRho]) ctx = case arg of
- ExFormation _ -> programToXMIR expr ctx
- ExApplication _ _ -> programToXMIR expr ctx
- ExDispatch _ _ -> programToXMIR expr ctx
- ExRoot -> programToXMIR expr ctx
- _ -> throwIO (UnsupportedTopExpression expr)
+expressionToXMIR expr@(ExFormation bds) ctx
+ | [BiTau (AtLabel _) arg] <- withoutVoidRho bds = case arg of
+ ExFormation _ -> programToXMIR expr ctx
+ ExApplication _ _ -> programToXMIR expr ctx
+ ExDispatch _ _ -> programToXMIR expr ctx
+ ExRoot -> programToXMIR expr ctx
+ _ -> throwIO (UnsupportedTopExpression expr)
-- The top of a '--partial' residual and the result of 'merge' are arbitrary
-- formations: several Ο/Ξ» bindings, voids and a bound Ο. The schema allows a
-- single under