phino 0.0.135 → 0.0.136
raw patch · 19 files changed
+606/−291 lines, 19 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
+ CST: EX_SINGLE :: PAIR -> EXPRESSION -> EXPRESSION
+ CST: [formation] :: EXPRESSION -> EXPRESSION
- CST: [pair] :: BINDINGS -> PAIR
+ CST: [pair] :: EXPRESSION -> PAIR
- Sugar: withoutRho :: EXPRESSION -> EXPRESSION
+ Sugar: withoutRho :: SugarType -> EXPRESSION -> EXPRESSION
Files
- README.md +132/−117
- phino.cabal +1/−1
- src/CST.hs +38/−12
- src/Encoding.hs +1/−0
- src/LaTeX.hs +3/−0
- src/Lining.hs +1/−0
- src/Margin.hs +6/−0
- src/Parser.hs +67/−6
- src/Printer.hs +3/−3
- src/Render.hs +13/−0
- src/Sugar.hs +26/−4
- test/CLISpec.hs +104/−106
- test/CSTSpec.hs +21/−3
- test/DataizeSpec.hs +4/−4
- test/EvaluateSpec.hs +1/−1
- test/MarginSpec.hs +27/−10
- test/ParserSpec.hs +54/−0
- test/PrinterSpec.hs +82/−22
- test/SugarSpec.hs +22/−2
README.md view
@@ -34,7 +34,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.134+cabal install --overwrite-policy=always phino-0.0.135 phino --version ``` @@ -310,8 +310,8 @@ 𝔼(L_number_plus) # 𝔻(Φ) 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ) 𝛿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)+ 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛+ 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1) ``` <!-- markdownlint-enable MD013 -->@@ -342,14 +342,15 @@ in. Where an operand came down to the datum a symbol stands for, the protocol writes-`𝔻(⟦ λ ⤍ 𝜎1 ⟧)` in place of that 42, so a reader sees that the value was+`𝔻(𝜎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:λ) == 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.@@ -397,7 +398,7 @@ `?(…)` 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+`𝕄(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@@ -418,9 +419,9 @@ 𝔼(L_number_plus) # 𝕄(Φ) 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ) 𝛿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 ⟧)+ 𝑛.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 -->@@ -479,48 +480,48 @@ $ cat fork.txt 𝕄(Φ.demo.a) 𝔼(L_gt) # 𝕄(Φ.demo.a.φ)- 𝛿1.1 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.ρ)+ 𝛿1.1 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ) 𝛿2.1 := 00-00-00-00-00-00-00-00 # 𝔻(ξ.x)- 𝑛.1.1 := Φ.bool( if ↦ ⟦ λ ⤍ L_fork, then ↦ ∅, else ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ) # 𝑛- 𝑛.1.2 := ⟦ if ↦ ⟦ λ ⤍ L_fork, then ↦ ∅, else ↦ ∅, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ⟧ # 𝕄(𝑛.1.1)+ 𝑛.1.1 := Φ.bool( if ↦ ⟦ λ ⤍ L_fork, then ↦ ∅, else ↦ ∅, φ ↦ 𝜎2:λ ⟧ ) # 𝑛+ 𝑛.1.2 := ⟦ λ ⤍ L_fork, then ↦ ∅, else ↦ ∅, φ ↦ 𝜎2:λ ⟧:if # 𝕄(𝑛.1.1) 𝔼(L_plus) # 𝕄(Φ.demo.a.φ)- 𝛿1.2 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.ρ)+ 𝛿1.2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ) 𝛿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)+ 𝑛.2.1 := Φ.number( φ ↦ 𝜎3:λ ) # 𝑛+ 𝑛.2.2 := ⟦ φ ↦ 𝜎3:λ, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧ # 𝕄(𝑛.2.1) 𝔼(L_plus) # 𝕄(Φ.demo.a.φ)- 𝛿1.3 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.ρ)- 𝛿2.3 := 𝔻(⟦ λ ⤍ 𝜎3 ⟧) # 𝔻(ξ.x)- 𝑛.3.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎4 ⟧ ) # 𝑛- 𝑛.3.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎4 ⟧, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧ # 𝕄(𝑛.3.1)+ 𝛿1.3 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)+ 𝛿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.φ)- 𝛿1.4 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.ρ)- 𝛿2.4 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.x)- 𝑛.4.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎5 ⟧ ) # 𝑛- 𝑛.4.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎5 ⟧, plus(x) ↦ ⟦ λ ⤍ L_plus ⟧, gt(x) ↦ ⟦ λ ⤍ L_gt ⟧ ⟧ # 𝕄(𝑛.4.1)+ 𝛿1.4 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)+ 𝛿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 := 𝔻(𝜎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]+ 𝔻(𝜎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.φ)- 𝛿1.6 := 𝔻(⟦ λ ⤍ 𝜎6 ⟧) # 𝔻(ξ.ρ)+ 𝛿1.6 := 𝔻(𝜎6:λ) # 𝔻(ξ.ρ) 𝛿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)+ 𝑛.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+`𝔻(𝜎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+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@@ -561,8 +562,8 @@ <bind meta="𝛿1.1">40-14-00-00-00-00-00-00</bind> <bind meta="𝛿2.1">40-18-00-00-00-00-00-00</bind> <minted>𝜎1</minted>- <built meta="𝑛.1.1">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>- <answer meta="𝑛.1.2">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>+ <built meta="𝑛.1.1">Φ.number( φ ↦ 𝜎1:λ )</built>+ <answer meta="𝑛.1.2">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer> </evaluate> </dataize> ```@@ -581,7 +582,7 @@ `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+`𝜎2:λ` and never `𝜎2` alone. It carries `meta` where the root carries `locator`, 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@@ -593,14 +594,14 @@ `<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+`𝔻(𝜎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+`𝔻(𝜎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@@ -610,7 +611,7 @@ `<minted>𝜎1</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. That is the edge a reader joins on: a later-`<dataize meta="𝛿1.5">⟦ λ ⤍ 𝜎2 ⟧</dataize>` names the symbol the firing that+`<dataize meta="𝛿1.5">𝜎2:λ</dataize>` names the symbol the firing that wrote `<minted>𝜎2</minted>` 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@@ -641,10 +642,10 @@ <bind meta="𝛿1.1">40-14-00-00-00-00-00-00</bind> <bind meta="𝛿2.1">40-18-00-00-00-00-00-00</bind> <minted>𝜎1</minted>- <built meta="𝑛.1.1">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>- <answer meta="𝑛.1.2">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, nope ↦ ⟦ λ ⤍ L_number_nope ⟧ ⟧</answer>+ <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" judgment="dataize">⟦ λ ⤍ L_number_nope ⟧</stuck>+ <stuck λ="L_number_nope" judgment="dataize">L_number_nope:λ</stuck> </dataize> ``` @@ -697,7 +698,7 @@ $ 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 ⟧+L_number_as_bool:λ ``` Here `2.times( 3 ).plus( 4 )` was answered by the entries the file carries, so@@ -716,14 +717,14 @@ 𝔼(L_number_times) # 𝕄(Φ) 𝛿1.1 := 40-00-00-00-00-00-00-00 # 𝔻(ξ.ρ) 𝛿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)+ 𝑛.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) # 𝕄(Φ)- 𝛿1.2 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.ρ)+ 𝛿1.2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ) 𝛿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 ⟧)+ 𝑛.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 -->@@ -806,7 +807,7 @@ ⟦ 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 ⟧ ⟧ ) ⟧+⟦ n ↦ 3, φ ↦ Φ.bar( ⟦ φ ↦ 𝜎2:λ, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ ) ⟧ ``` Every binding of the formation is entered, recursively. 𝕄 is asked about the@@ -845,11 +846,9 @@ number(φ) ↦ ⟦ times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, bar(x) ↦ ⟦ λ ⤍ L_bar ⟧, demo ↦ ⟦- foo ↦ ⟦- n ↦ 3,- φ ↦ Φ.bar( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ )- ⟧- ⟧+ n ↦ 3,+ φ ↦ Φ.bar( ⟦ φ ↦ 𝜎2:λ, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ )+ ⟧:foo ⟧ ``` @@ -992,6 +991,22 @@ ⟧ ``` +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, the implicit+`ρ ↦ ∅` aside, 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].+ ## Merge You can merge several 𝜑-expressions into a single one by merging their@@ -1317,103 +1332,103 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1- total: 1821425.151 μs- avg: 182142.515 μs- min: 170750.493 μs- max: 209499.629 μs- std dev: 15132.778 μs+ total: 1810402.021 μs+ avg: 181040.202 μs+ min: 169827.114 μs+ max: 204681.114 μs+ std dev: 13154.216 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1- total: 7708084.189 μs- avg: 770808.419 μs- min: 701670.454 μs- max: 827995.748 μs- std dev: 39123.293 μs+ total: 7538811.226 μs+ avg: 753881.123 μs+ min: 694204.271 μs+ max: 840942.094 μs+ std dev: 41681.127 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1- total: 507305.249 μs- avg: 50730.525 μs- min: 48912.624 μs- max: 54335.144 μs- std dev: 1596.161 μs+ total: 597613.462 μs+ avg: 59761.346 μs+ min: 54912.144 μs+ max: 65342.026 μs+ std dev: 2994.555 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1- total: 4188218.626 μs- avg: 418821.863 μs- min: 403263.572 μs- max: 449353.774 μs- std dev: 14512.853 μs+ total: 4130310.545 μs+ avg: 413031.054 μs+ min: 404823.433 μs+ max: 426597.938 μs+ std dev: 7495.509 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1- total: 4025720.702 μs- avg: 402572.070 μs- min: 382540.835 μs- max: 428138.472 μs- std dev: 11933.717 μs+ total: 4284120.069 μs+ avg: 428412.007 μs+ min: 413571.324 μs+ max: 445658.981 μs+ std dev: 11624.236 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1- total: 14045902.469 μs- avg: 1404590.247 μs- min: 1384313.216 μs- max: 1438197.181 μs- std dev: 15501.328 μs+ total: 13724020.907 μs+ avg: 1372402.091 μs+ min: 1344331.661 μs+ max: 1409368.695 μs+ std dev: 17786.287 μs === morph/symbolic/demo/e1 === warmup: 3 iterations batches: 10 x 1- total: 880309.436 μs- avg: 88030.944 μs- min: 86359.252 μs- max: 90267.072 μs- std dev: 1248.861 μs+ total: 866700.384 μs+ avg: 86670.038 μs+ min: 86184.411 μs+ max: 87168.132 μs+ std dev: 285.902 μs === morph/symbolic/demo/e2 === warmup: 3 iterations batches: 10 x 1- total: 1215850.964 μs- avg: 121585.096 μs- min: 117038.580 μs- max: 138033.783 μs- std dev: 5877.028 μs+ total: 1188660.494 μs+ avg: 118866.049 μs+ min: 116047.655 μs+ max: 136278.751 μs+ std dev: 5832.266 μs === morph/symbolic/demo/e3 === warmup: 3 iterations batches: 10 x 1- total: 1844780.073 μs- avg: 184478.007 μs- min: 180633.446 μs- max: 192191.924 μs- std dev: 3471.827 μs+ total: 1867565.431 μs+ avg: 186756.543 μs+ min: 185066.327 μs+ max: 187725.046 μs+ std dev: 1004.396 μs === morph/symbolic/demo/e4 === warmup: 3 iterations batches: 10 x 1- total: 617914.516 μs- avg: 61791.452 μs- min: 60976.930 μs- max: 62245.020 μs- std dev: 354.771 μs+ total: 623551.322 μs+ avg: 62355.132 μs+ min: 61620.682 μs+ max: 63797.384 μs+ std dev: 728.465 μs === morph/symbolic/demo/e5 === warmup: 3 iterations batches: 10 x 1- total: 185308.236 μs- avg: 18530.824 μs- min: 17898.792 μs- max: 19243.924 μs- std dev: 442.924 μs+ total: 186679.533 μs+ avg: 18667.953 μs+ min: 18384.769 μs+ max: 18868.158 μs+ std dev: 149.307 μs === morph/symbolic/native/e5 ===- warmup: 2 iterations+ warmup: 1 iterations batches: 4 x 1- total: 18057164.992 μs- avg: 4514291.248 μs- min: 4280917.084 μs- max: 4860213.506 μs- std dev: 215452.202 μs+ total: 17947336.400 μs+ avg: 4486834.100 μs+ min: 4167627.934 μs+ max: 4633560.228 μs+ std dev: 189453.769 μs ``` The results were calculated in [this GHA job][benchmark-gha]-on 2026-09-20 at 06:19,+on 2026-09-22 at 19:05, on Linux with 4 CPUs. <!-- benchmark_end -->@@ -1463,4 +1478,4 @@ [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/35493401441+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/35770947279
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.135+version: 0.0.136 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
src/CST.hs view
@@ -183,6 +183,7 @@ | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION} | EX_PHI_AGAIN {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION} | EX_BYTES {bytes :: BYTES} -- bare data 𝛿, a rendering-only terminal chain node (see #980)+ | EX_SINGLE {pair :: PAIR, formation :: EXPRESSION} -- one-binding formation as 'FF-:Δ' or 'ξ.a:φ', with its full form (see #1385) deriving (Eq, Show) data ATTRIBUTE@@ -348,18 +349,38 @@ 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- toCST (ExFormation bds) (tabs, eol) =- let next = tabs + 1- bds' = toCST (withoutLastVoidRho bds) (next, eol) :: BINDING- in EX_FORMATION- LSB- EOL- (TAB next)- bds'- EOL- (TAB tabs)- 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)) where+ full :: EXPRESSION+ full =+ let next = tabs + 1+ bds' = toCST (withoutLastVoidRho bds) (next, eol) :: BINDING+ in EX_FORMATION+ LSB+ EOL+ (TAB next)+ bds'+ EOL+ (TAB tabs)+ 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) ↦ ⟦ … ⟧'+ 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 [BiTau attr expr] = Just (PA_TAU (toCST attr ctx) ARROW (toCST expr ctx))+ 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] = []@@ -507,8 +528,13 @@ attr' (map (`toCST` ctx) _voids) ARROW- (toCST (ExFormation _bds) ctx)+ (unsugared (toCST (ExFormation _bds) 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
src/Encoding.hs view
@@ -31,6 +31,7 @@ toASCII EX_META{..} = EX_META (META EXCL E' (rest meta)) toASCII EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toASCII expr) toASCII EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toASCII expr)+ toASCII EX_SINGLE{..} = EX_SINGLE (toASCII pair) (toASCII formation) toASCII expr = expr instance ToASCII APP_BINDING where
src/LaTeX.hs view
@@ -273,6 +273,9 @@ -- one here too, with its name piped the way any other label is (see #1065) toLaTeX EX_NONFINITE{..} = EX_DISPATCH (EX_GLOBAL global) SPACE (toLaTeX (AT_LABEL (nonFiniteName nonfinite))) toLaTeX EX_BYTES{..} = EX_BYTES (toLaTeX bytes)+ -- The eolang LaTeX package knows no one-binding sugar, so the full+ -- formation is written instead (see #1385)+ toLaTeX EX_SINGLE{..} = toLaTeX formation toLaTeX expr = expr instance ToLaTeX ATTRIBUTE where
src/Lining.hs view
@@ -25,6 +25,7 @@ toSingleLine EX_APPLICATION{..} = EX_APPLICATION (toSingleLine expr) space NO_EOL TAB' (toSingleLine argument) NO_EOL TAB' indent toSingleLine EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr) toSingleLine EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSingleLine expr)+ toSingleLine EX_SINGLE{..} = EX_SINGLE (toSingleLine pair) (toSingleLine formation) toSingleLine expr = expr instance ToSingleLine APP_BINDING where
src/Margin.hs view
@@ -32,6 +32,12 @@ withMargin' cfg EX_DISPATCH{..} = EX_DISPATCH (withMargin' cfg expr) space attr withMargin' cfg EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (withMargin' cfg expr) withMargin' _ EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSingleLine expr)+ -- The asset of a one-binding sugar is followed by a colon and the attribute,+ -- so it gets that much less of the margin to be laid out in+ withMargin' cfg@(extra, margin) ex@EX_SINGLE{pair = PA_TAU{..}, ..} =+ let single = toSingleLine ex+ asset = withMargin' (extra, margin - lengthOf attr - 1) expr+ in if lengthOf single + extra <= margin then single else EX_SINGLE (PA_TAU attr arrow asset) (withMargin' cfg formation) withMargin' cfg@(extra, margin) ex@EX_APPLICATION{tab = tab@(TAB indt), ..} = let single = toSingleLine ex main = withMargin' cfg expr
src/Parser.hs view
@@ -25,7 +25,7 @@ import Bytes (nonFiniteBts, nonFiniteOf, numToBts, strToBts) import Control.Exception (Exception) import Control.Monad (guard, when)-import Data.Char (isAsciiLower, isDigit)+import Data.Char (isAsciiLower, isAsciiUpper, isDigit) import Data.Scientific (toRealFloat) import qualified Data.Text as T import Data.Void@@ -118,8 +118,20 @@ arrow = choice [symbol "->", symbol "↦"] global :: Parser String-global = choice [symbol "Q", symbol "Φ"]+global = choice [ascii 'Q', symbol "Φ"] +-- A one-letter ASCII token that a function name may start with, `Q` or `T`,+-- which is no such token where it is a function name itself or the start of+-- one, so `Q:λ` and `Qx:λ` stay the λ functions `Q` and `Qx` in the+-- one-binding sugar of #1385+ascii :: Char -> Parser String+ascii letter = lexeme (try (pure <$> char letter <* notFollowedBy (satisfy named <|> '_' <$ lambdaOf)))+ where+ named :: Char -> Bool+ named ch = isDigit ch || isAsciiLower ch || ch == '_' || ch == 'φ'+ lambdaOf :: Parser Char+ lambdaOf = whiteSpace >> char ':' >> whiteSpace >> oneOf ['L', 'λ']+ metaSuffix :: Parser String metaSuffix = lexeme (many (oneOf ('_' : '-' : ['0' .. '9'] ++ ['a' .. 'z'] ++ ['A' .. 'Z']) <?> "meta suffix")) @@ -309,6 +321,44 @@ rb :: Parser String rb = symbol ")" +-- The name a λ binding carries: a function, a meta standing for one, or a symbol+lambdaName :: Parser Function+lambdaName = choice [Function . T.pack <$> function, try (either FnAny FnMeta <$> metaVar 'F' "𝑓"), sigma]++-- The colon that attaches an attribute to what stands before it, making a+-- formation of one binding out of the two (see #1385)+colon :: Parser String+colon = symbol ":"++-- A formation of one binding written as its asset followed by a colon and the+-- attribute it is bound to, the way the sugar of #1385 spells it:+-- `FF-AA:Δ` is `⟦ Δ ⤍ FF-AA ⟧`, `𝜎1:λ` is `⟦ λ ⤍ 𝜎1 ⟧` and `∅:a` is+-- `⟦ a ↦ ∅ ⟧`. A τ binding, `ξ.a:φ` for `⟦ φ ↦ ξ.a ⟧`, is no head but a tail,+-- since it attaches to a whole expression (see 'exTail'). Bytes and λ names+-- look like numbers and function-like heads, so their shapes are only+-- committed to once the attribute after the colon is read. Each of the three+-- is a head of its own in 'exHead', standing right before the first head it+-- 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++-- `FF-AA:Δ`, `--:D` or `𝛿1:Δ`+deltaHead :: Parser Expression+deltaHead =+ lookAhead (satisfy (\ch -> isDigit ch || ('A' <= ch && ch <= 'F') || ch `elem` ("-!𝛿" :: String)))+ >> alone (try (BiDelta <$> bytes <* colon <* choice [symbol "D", symbol "Δ"]))++-- `Plus:λ`, `𝜎1:λ` or `!F1:L`+lambdaHead :: Parser Expression+lambdaHead =+ lookAhead (satisfy (\ch -> isAsciiUpper ch || ch `elem` ("!𝑓𝜎" :: String)))+ >> alone (try (BiLambda <$> lambdaName <* colon <* choice [symbol "L", symbol "λ"]))++-- `∅:a` or `?:a`+voidHead :: Parser Expression+voidHead = alone (choice [symbol "?", symbol "∅"] >> colon >> BiVoid <$> attribute)+ metaBinding :: Parser Binding metaBinding = either BiAny BiMeta <$> metaVar 'B' "𝐵" @@ -333,7 +383,7 @@ , try metaBinding , do _ <- try lambda- BiLambda <$> choice [Function . T.pack <$> function, try (either FnAny FnMeta <$> metaVar 'F' "𝑓"), sigma]+ BiLambda <$> lambdaName , do attr <- attribute choice@@ -343,8 +393,10 @@ ] <?> "binding" where+ -- A void followed by a colon is no void of this binding but the head of+ -- a one-binding formation the binding is bound to, as in `x ↦ ∅:a` blank :: Parser String- blank = arrow >> choice [symbol "?", symbol "∅"]+ blank = arrow >> choice [symbol "?", symbol "∅"] <* notFollowedBy colon -- inlined void attribute -- 1. label@@ -428,6 +480,8 @@ -- 4. termination -- 5. meta expression -- 6. full attribute -> sugar for $.attr+-- 7. one-binding formation of a Δ, λ or void binding -> sugar for ⟦ Δ ⤍ FF- ⟧,+-- each standing before the first head it could be taken for exHead :: Parser Expression exHead = choice@@ -439,14 +493,17 @@ return ExXi , root , do- _ <- choice [symbol "T", symbol "⊥"]+ _ <- choice [ascii 'T', symbol "⊥"] return ExTermination- , number , lexeme (DataString . strToBts <$> quotedStr)+ , deltaHead+ , number , try (either ExAny ExMeta <$> metaVar 'e' "𝑒") , try (either ExAny ExMeta <$> metaVar 'n' "𝑛") , try (either ExAny ExMeta <$> metaVar 'k' "𝑘")+ , lambdaHead , ExDispatch ExXi <$> attribute+ , voidHead ] <?> "expression head" @@ -456,6 +513,7 @@ -- tail optional part of application -- 1. any head + dispatch -- 2. any head except $ and Q + application+-- 3. any head + colon and attribute -> sugar for ⟦ attr ↦ head ⟧ exTail :: Expression -> Parser Expression exTail expr = choice@@ -482,6 +540,9 @@ ] _ <- symbol ")" return (application expr bds)+ , do+ _ <- colon+ ExFormation . withVoidRho . pure . (`BiTau` expr) <$> attribute ] <?> "dispatch or application" exTail next
src/Printer.hs view
@@ -44,7 +44,7 @@ logPrintConfig = (SWEET, UNICODE, SINGLELINE, defaultMargin) printExpression' :: Expression -> PrintConfig -> String-printExpression' = printExpressionWith id+printExpression' = printExpressionWith (const id) -- Like 'printExpression'', but drops every ρ binding from the rendered -- expression (the '--hide-rho' switch). See 'withoutRho'.@@ -53,9 +53,9 @@ -- Shared rendering pipeline with a hook applied to the sugared CST, right -- before encoding and margin wrapping.-printExpressionWith :: (EXPRESSION -> EXPRESSION) -> Expression -> PrintConfig -> String+printExpressionWith :: (SugarType -> EXPRESSION -> EXPRESSION) -> Expression -> PrintConfig -> String printExpressionWith hide ex (sugar, encoding, line, margin) =- T.unpack $ render (withLineFormat line $ withMargin margin $ withEncoding encoding $ hide $ withSugarType sugar $ expressionToCST ex)+ T.unpack $ render (withLineFormat line $ withMargin margin $ withEncoding encoding $ hide sugar $ withSugarType sugar $ expressionToCST ex) printExpression :: Expression -> String printExpression ex = printExpression' ex defaultPrintConfig
src/Render.hs view
@@ -213,6 +213,19 @@ render EX_PHI_MEET{..} = "\\phinoMeet{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}{ " <> render expr <> " }" render EX_PHI_AGAIN{..} = "\\phinoAgain{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}" render EX_BYTES{..} = render bytes+ render EX_SINGLE{..} = case pair of+ PA_TAU{..} -> render expr <> ":" <> render attr+ PA_FORMATION{voids = [], ..} -> render expr <> ":" <> render attr+ PA_VOID{..} -> render void <> ":" <> render attr+ PA_DELTA{..} -> render bytes <> ":" <> render DELTA+ PA_DELTA'{..} -> render bytes <> ":" <> render DELTA'+ PA_META_DELTA{..} -> render meta <> ":" <> render DELTA+ PA_META_DELTA'{..} -> render meta <> ":" <> render DELTA'+ PA_LAMBDA{..} -> render func <> ":" <> render LAMBDA+ PA_LAMBDA'{..} -> render func <> ":" <> render LAMBDA'+ PA_META_LAMBDA{..} -> render meta <> ":" <> render LAMBDA+ PA_META_LAMBDA'{..} -> render meta <> ":" <> render LAMBDA'+ _ -> render formation instance Render [ATTRIBUTE] where render attrs = T.intercalate ", " (map render attrs)
src/Sugar.hs view
@@ -46,13 +46,18 @@ -- SALTY path. 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()').-withoutRho :: EXPRESSION -> EXPRESSION-withoutRho = goExpr+-- argument collapses to its bare callee (no leftover 'e()'). In the SWEET+-- syntax a formation left with one binding takes the sugar of #1385, 'ξ.a:φ',+-- the way it would have taken it had the ρ never been there; the SALTY one+-- has no such sugar.+withoutRho :: SugarType -> EXPRESSION -> EXPRESSION+withoutRho sugar = goExpr where goExpr :: EXPRESSION -> EXPRESSION goExpr EX_FORMATION{..} = case goBinding binding of empty@BI_EMPTY{} -> EX_FORMATION lsb NO_EOL NO_TAB empty NO_EOL NO_TAB rsb+ binding'@BI_PAIR{pair = pair', bindings = BDS_EMPTY{}}+ | sugar == SWEET && sugared pair' -> EX_SINGLE pair' (EX_FORMATION lsb eol tab binding' eol' tab' rsb) binding' -> EX_FORMATION lsb eol tab binding' eol' tab' rsb goExpr EX_DISPATCH{..} = EX_DISPATCH (goExpr expr) space attr goExpr EX_APPLICATION{..} = case goArgument argument of@@ -60,6 +65,9 @@ Just argument' -> EX_APPLICATION (goExpr expr) space eol tab argument' eol' tab' indent goExpr EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (goExpr expr) goExpr EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (goExpr expr)+ goExpr EX_SINGLE{..}+ | isRho pair = goExpr formation+ | otherwise = EX_SINGLE (goPair pair) (goExpr formation) goExpr expr = expr -- Formation bindings: drop the ρ pairs, recurse into whatever remains. goBinding :: BINDING -> BINDING@@ -112,8 +120,20 @@ 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 (goExpr expr)+ goPair PA_FORMATION{..} = PA_FORMATION attr voids arrow (unsugared (goExpr expr)) goPair pair = pair+ -- Inline voids open a formation, which the sugar may not stand for+ unsugared :: EXPRESSION -> EXPRESSION+ unsugared EX_SINGLE{..} = formation+ unsugared expr = expr+ -- Whether the only binding of a formation has the one-binding sugar+ sugared :: PAIR -> Bool+ sugared PA_TAU{attr = AT_DELTA{}} = False+ sugared PA_TAU{attr = AT_LAMBDA{}} = False+ sugared PA_ALPHA{} = False+ sugared PA_FORMATION{voids = []} = True+ sugared PA_FORMATION{} = False+ sugared _ = True isRho :: PAIR -> Bool isRho PA_VOID{attr = AT_RHO _} = True isRho PA_TAU{attr = AT_RHO _} = True@@ -130,6 +150,7 @@ -- | 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, ...) | -- | e(a1 -> e1, a2 -> e2, ...) | e(a1 -> e1)(a2 -> e2)... |@@ -193,6 +214,7 @@ rhos toSalty EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (toSalty expr) toSalty EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toSalty expr)+ toSalty EX_SINGLE{..} = toSalty formation toSalty expr = expr saltifyPrimitive :: EXPRESSION -> EXPRESSION -> EXPRESSION -> TAB -> [Argument] -> EXPRESSION
test/CLISpec.hs view
@@ -173,13 +173,13 @@ ( "also drops the rho that --sweet leaves behind" , "[[ foo -> [[ x -> [[ ]], ^ -> $.y ]], y -> [[ ]] ]]" , ["rewrite", "--flat", "--sweet", "--hide-rho"]- , ["⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧"]+ , ["⟦ foo ↦ ⟦⟧:x, y ↦ ⟦⟧ ⟧"] ) , ( "keeps sweet numeric literals intact" , "[[ a -> 42 ]]" , ["rewrite", "--flat", "--sweet", "--hide-rho"]- , ["⟦ a ↦ 42 ⟧"]+ , ["42:a"] ) ] (\(desc, input, args, expected) -> it desc (withStdin input (testCLISucceeded args expected)))@@ -362,7 +362,7 @@ withStdin "[[ x -> 5 ]]" $ testCLISucceeded ["rewrite", "--seed=42", "--sweet"]- ["⟦ x ↦ 5 ⟧"]+ ["5:x"] it "defaults --seed to 0 in help" $ testCLISucceeded@@ -480,7 +480,7 @@ withStdin "⟦ k ↦ ⟦ m ↦ ⟦ Δ ⤍ 01- ⟧ ⟧.m, j ↦ ⟦ λ ⤍ Marker ⟧ ⟧" $ testCLISucceeded ["rewrite", "--normalize", rule "marker.yaml", "--sweet"]- ["⟦ k ↦ ⟦ Δ ⤍ 01-, ρ ↦ ⟦ m ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧, j ↦ ⟦ Δ ⤍ FF- ⟧ ⟧"]+ ["⟦ k ↦ ⟦ Δ ⤍ 01-, ρ ↦ 01-:Δ:m ⟧, j ↦ FF-:Δ ⟧"] it "normalizes from stdin" $ withStdin "⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ [[ ]]) ⟧" $@@ -501,7 +501,7 @@ withStdin "[[ x -> 5]]" $ testCLISucceeded ["rewrite", "--sweet"]- ["⟦ x ↦ 5 ⟧"]+ ["5:x"] it "rewrites as XMIR" $ withStdin "[[ x -> Q.y ]]" $@@ -595,7 +595,7 @@ withStdin "<object><o name=\"app\"><o name=\"x\" base=\"Φ.number\"/></o></object>" $ testCLISucceeded ["rewrite", "--input=xmir", "--sweet"]- ["⟦ app ↦ ⟦ x ↦ Φ.number ⟧ ⟧"]+ ["Φ.number:x:app"] it "rewrites and prints with XMIR as input and output" $ withStdin@@ -622,7 +622,7 @@ withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $ testCLISucceeded ["rewrite", rule "simple.yaml", "--must=1", "--sweet"]- ["x ↦ \"bar\""]+ ["\"bar\":x"] it "prints many expressions with --sequence" $ withStdin "[[ x -> \"foo\" ]]" $@@ -637,9 +637,9 @@ , "--flat" ] [ unlines- [ "⟦ x ↦ \"foo\" ⟧"+ [ "\"foo\":x" , "Φ.x( y ↦ \"foo\" )"- , "⟦ x ↦ \"foo\" ⟧"+ , "\"foo\":x" ] ] @@ -660,13 +660,13 @@ "\n" [ "" , "=== Step #1"- , "⟦ x ↦ \"foo\" ⟧"+ , "\"foo\":x" , "" , "=== Step #2, Rule 'first', 31t -> 30t" , "Φ.x( y ↦ \"foo\" )" , "" , "=== Step #3, Rule 'second', 30t -> 31t"- , "⟦ x ↦ \"foo\" ⟧"+ , "\"foo\":x" ] ] @@ -674,7 +674,7 @@ withStdin "[[ x -> \"foo\" ]]" $ testCLISucceeded ["rewrite", rule "simple.yaml", "--headers", "--sweet", "--flat"]- ["⟦ x ↦ \"bar\" ⟧"]+ ["\"bar\":x"] it "emits step headers as LaTeX comments with --headers" $ withStdin "[[ x -> \"foo\" ]]" $@@ -843,8 +843,8 @@ testCLISucceeded ["rewrite", "--normalize", "--sequence", "--flat", "--output=phi", "--sweet", "--focus=Q.ex"] [ unlines- [ "⟦ x ↦ ⟦ y ↦ ∅, k ↦ ⟦ t ↦ 42 ⟧ ⟧( y ↦ ⟦ t ↦ 42 ⟧ ) ⟧.i"- , "⟦ x ↦ ⟦ y ↦ ⟦ t ↦ 42 ⟧, k ↦ ⟦ t ↦ 42 ⟧ ⟧ ⟧.i"+ [ "⟦ y ↦ ∅, k ↦ 42:t ⟧( y ↦ 42:t ):x.i"+ , "⟦ y ↦ 42:t, k ↦ 42:t ⟧:x.i" , "⊥" ] ]@@ -859,7 +859,7 @@ withStdin "[[ x -> \"foo\" ]]" $ testCLISucceeded ["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat", "--sequence", rule "simple.yaml"]- [" <listing>⟦ x ↦ \"foo\" ⟧</listing>", " <listing>⟦ x ↦ \"bar\" ⟧</listing>"]+ [" <listing>\"foo\":x</listing>", " <listing>\"bar\":x</listing>"] describe "must range tests" $ do describe "fails" $ do@@ -905,13 +905,13 @@ withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $ testCLISucceeded ["rewrite", rule "simple.yaml", "--must=1..1", "--sweet"]- ["x ↦ \"bar\""]+ ["\"bar\":x"] it "accepts range 1..3 when 1 cycle happens" $ withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $ testCLISucceeded ["rewrite", rule "simple.yaml", "--must=1..3", "--sweet"]- ["x ↦ \"bar\""]+ ["\"bar\":x"] it "accepts range 0.. (0 or more)" $ withStdin "[[ ]]" $@@ -931,7 +931,7 @@ hClose h testCLISucceeded ["rewrite", rule "simple.yaml", "--in-place", "--sweet", path] [] content <- readFile path- content `shouldBe` "⟦ x ↦ \"bar\" ⟧"+ content `shouldBe` "\"bar\":x" it "skips rewriting with --update when target is newer than source" $ withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->@@ -981,19 +981,19 @@ ["rewrite", rule "simple.yaml", "--update", "--sweet", "--target=" ++ tgt, src] [] content <- readFile tgt- content `shouldBe` "⟦ x ↦ \"bar\" ⟧"+ content `shouldBe` "\"bar\":x" it "rewrites with cycles" $ withStdin "[[ x -> \"x\" ]]" $ testCLISucceeded ["rewrite", "--sweet", rule "infinite.yaml", "--max-depth=1", "--max-cycles=2"]- ["⟦ x ↦ \"x_hi_hi\" ⟧"]+ ["\"x_hi_hi\":x"] it "hides default package" $ withStdin "[[ org -> [[ eolang -> [[ number -> [[]] ]]]], x -> 42 ]]" $ testCLISucceeded ["rewrite", "--sweet", "--flat", "--hide=Q.org"]- ["⟦ x ↦ 42 ⟧"]+ ["42:x"] it "hides several FQNs" $ withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $@@ -1005,13 +1005,13 @@ withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $ testCLISucceeded ["rewrite", "--sweet", "--flat", "--show=Q.org", "--hide=Q.org.eolang"]- ["⟦ org ↦ ⟦ yegor256 ↦ Φ.y ⟧ ⟧"]+ ["Φ.y:yegor256:org"] it "prints in line with --flat" $ withStdin "[[ x -> 5, y -> \"hey\", z -> [[ w -> [[ ]] ]] ]]" $ testCLISucceeded ["rewrite", "--sweet", "--flat"]- ["⟦ x ↦ 5, y ↦ \"hey\", z ↦ ⟦ w ↦ ⟦⟧ ⟧ ⟧"]+ ["⟦ x ↦ 5, y ↦ \"hey\", z ↦ ⟦⟧:w ⟧"] it "removes unnecessary rho bindings in primitive applications" $ withStdin@@ -1024,7 +1024,7 @@ ) ( testCLISucceeded ["rewrite", "--sweet", "--normalize", "--flat"]- ["⟦ z ↦ 42, org ↦ ⟦ eolang ↦ ⟦ bytes(data) ↦ ⟦⟧, number(as-bytes) ↦ ⟦⟧ ⟧ ⟧ ⟧"]+ ["⟦ z ↦ 42, org ↦ ⟦ bytes(data) ↦ ⟦⟧, number(as-bytes) ↦ ⟦⟧ ⟧:eolang ⟧"] ) it "reduces log message" $@@ -1053,13 +1053,13 @@ withStdin "[[ x -> [[ y -> [[ L> Func ]].q, z -> Q.x(a -> [[ w -> [[ L> Atom ]], L> Hello ]]) ]], L> Package ]]" $ testCLISucceeded ["rewrite", "--canonize", "--sweet", "--flat"]- ["⟦ x ↦ ⟦ y ↦ ⟦ λ ⤍ Fn1 ⟧.q, z ↦ Φ.x( a ↦ ⟦ w ↦ ⟦ λ ⤍ Fn2 ⟧, λ ⤍ Fn3 ⟧ ) ⟧, λ ⤍ Fn4 ⟧"]+ ["⟦ x ↦ ⟦ y ↦ Fn1:λ.q, z ↦ Φ.x( a ↦ ⟦ w ↦ Fn2:λ, λ ⤍ Fn3 ⟧ ) ⟧, λ ⤍ Fn4 ⟧"] it "rewrites by locator" $ withStdin "[[ ex -> [[ x -> [[ y -> 5 ]].y ]], abc -> [[ x -> ? ]](x -> 5) ]]" $ testCLISucceeded ["rewrite", "--sweet", "--flat", "--locator=Q.ex", "--normalize"]- ["⟦ ex ↦ ⟦ x ↦ 5 ⟧, abc ↦ ⟦ x ↦ ∅ ⟧( x ↦ 5 ) ⟧"]+ ["⟦ ex ↦ 5:x, abc ↦ ∅:x( x ↦ 5 ) ⟧"] it "returns original expression on --breakpoint" $ withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $@@ -1067,7 +1067,7 @@ ["rewrite", "--sweet", "--flat", "--normalize", "--breakpoint=stop", "--log-level=debug"] [ "Applied 'copy' (30 nodes -> 25 nodes)" , "Rule 'stop' is a breakpoint, dropping down all the previous rewritings..."- , "⟦ x ↦ ∅, y ↦ x ⟧( x ↦ ⟦ Δ ⤍ 42- ⟧ ).y"+ , "⟦ x ↦ ∅, y ↦ x ⟧( x ↦ 42-:Δ ).y" ] describe "dataize" $ do@@ -1179,7 +1179,7 @@ withStdin "[[ D> 01- ]]" $ testCLISucceeded ["dataize", "--sequence", "--quiet", "--flat", "--sweet"]- ["⟦ Δ ⤍ 01- ⟧\n01-"]+ ["01-:Δ\n01-"] it "focuses a compressed sequence whose meet replaces a step root" $ withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $@@ -1233,8 +1233,8 @@ , " 𝔼(L_number_plus) # 𝔻(Φ)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿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)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1)" ] -- The second firing of one entry numbers its own metas 𝛿1.2 and 𝛿2.2,@@ -1251,13 +1251,13 @@ , " 𝔼(L_number_plus) # 𝕄(Φ)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿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)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1)" , " 𝔼(L_number_plus) # 𝔻(Φ)"- , " 𝛿1.2 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.ρ)"+ , " 𝛿1.2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)" , " 𝛿2.2 := 40-1C-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.2.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) # 𝑛"- , " 𝑛.2.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.2.1)"+ , " 𝑛.2.1 := Φ.number( φ ↦ 𝜎2:λ ) # 𝑛"+ , " 𝑛.2.2 := ⟦ φ ↦ 𝜎2:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.2.1)" ] -- A meta is a variable bound exactly once, so its name has to be unique@@ -1276,13 +1276,13 @@ , " 𝔼(L_number_plus) # 𝕄(Φ)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ # 𝕄(𝑛.1.1)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ # 𝕄(𝑛.1.1)" , " 𝔼(L_number_times) # 𝔻(Φ)"- , " 𝛿1.2 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.ρ)"+ , " 𝛿1.2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)" , " 𝛿2.2 := 40-1C-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.2.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) # 𝑛"- , " 𝑛.2.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ # 𝕄(𝑛.2.1)"+ , " 𝑛.2.1 := Φ.number( φ ↦ 𝜎2:λ ) # 𝑛"+ , " 𝑛.2.2 := ⟦ φ ↦ 𝜎2:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ # 𝕄(𝑛.2.1)" ] -- An operand is brought down by a whole run of 𝔻, so a λ function it@@ -1300,11 +1300,11 @@ , " 𝔼(L_number_plus) # 𝔻(Φ.a🌵1)" , " 𝛿1.2 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿2.2 := 40-1C-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.2.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) # 𝑛"- , " 𝑛.2.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.2.1)"- , " 𝛿2.1 := 𝔻(⟦ λ ⤍ 𝜎1 ⟧) # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1)"+ , " 𝑛.2.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.2.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.2.1)"+ , " 𝛿2.1 := 𝔻(𝜎1:λ) # 𝔻(ξ.x)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎2:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎2:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1)" ] -- A 'symbolize' line stands the data of a term an earlier line bound@@ -1323,11 +1323,11 @@ lines records `shouldBe` [ "𝕄(Φ.y)" , " 𝔼(L_stand) # 𝕄(Φ.y)"- , " 𝑛1.1 := ⟦ Δ ⤍ 01- ⟧ # 𝕄(ξ.x)"- , " 𝔻(⟦ λ ⤍ 𝜎1 ⟧) == 01-"- , " 𝑛2.1 := ⟦ λ ⤍ 𝜎1 ⟧ # 𝑛1"- , " 𝑛.1.1 := ⟦ z ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧ # 𝑛"- , " 𝑛.1.2 := ⟦ z ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧ # 𝕄(𝑛.1.1)"+ , " 𝑛1.1 := 01-:Δ # 𝕄(ξ.x)"+ , " 𝔻(𝜎1:λ) == 01-"+ , " 𝑛2.1 := 𝜎1:λ # 𝑛1"+ , " 𝑛.1.1 := 𝜎1:λ:z # 𝑛"+ , " 𝑛.1.2 := 𝜎1:λ:z # 𝕄(𝑛.1.1)" ] it "keeps the lines of a run that fails" $@@ -1343,9 +1343,9 @@ , " 𝔼(L_number_plus) # 𝕄(Φ)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿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 ⟧)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, nope ↦ L_number_nope:λ ⟧ # 𝕄(𝑛.1.1)"+ , " ?(L_number_nope) # 𝔻(L_number_nope:λ)" ] it "truncates the lines left over from the previous run" $@@ -1363,7 +1363,7 @@ withStdin sum' $ testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--output=xmir", "--quiet", "--sweet", "--hide-rho"] [] records <- readUtf8 path- records `shouldEndWith` " 𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1)\n"+ records `shouldEndWith` " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1)\n" -- The same facts as markup, so a program reading the protocol back never -- has to parse 𝜑 to learn them: the name of an element says what its@@ -1385,8 +1385,8 @@ , " <bind meta=\"𝛿1.1\">40-14-00-00-00-00-00-00</bind>" , " <bind meta=\"𝛿2.1\">40-18-00-00-00-00-00-00</bind>" , " <minted>𝜎1</minted>"- , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>"+ , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>" , " </evaluate>" , "</dataize>" ]@@ -1423,15 +1423,15 @@ , " <bind meta=\"𝛿1.1\">40-14-00-00-00-00-00-00</bind>" , " <bind meta=\"𝛿2.1\">40-18-00-00-00-00-00-00</bind>" , " <minted>𝜎1</minted>"- , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>"+ , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>" , " </evaluate>" , " <evaluate λ=\"L_number_plus\" id=\"2\" judgment=\"dataize\" locator=\"Φ\">"- , " <dataize meta=\"𝛿1.2\">⟦ λ ⤍ 𝜎1 ⟧</dataize>"+ , " <dataize meta=\"𝛿1.2\">𝜎1:λ</dataize>" , " <bind meta=\"𝛿2.2\">40-1C-00-00-00-00-00-00</bind>" , " <minted>𝜎2</minted>"- , " <built meta=\"𝑛.2.1\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ )</built>"- , " <answer meta=\"𝑛.2.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>"+ , " <built meta=\"𝑛.2.1\">Φ.number( φ ↦ 𝜎2:λ )</built>"+ , " <answer meta=\"𝑛.2.2\">⟦ φ ↦ 𝜎2:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>" , " </evaluate>" , "</dataize>" ]@@ -1452,11 +1452,11 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<morph locator=\"Φ.y\">" , " <evaluate λ=\"L_stand\" id=\"1\" judgment=\"morph\" locator=\"Φ.y\">"- , " <bind meta=\"𝑛1.1\">⟦ Δ ⤍ 01- ⟧</bind>"+ , " <bind meta=\"𝑛1.1\">01-:Δ</bind>" , " <known symbol=\"𝜎1\">01-</known>"- , " <bind meta=\"𝑛2.1\">⟦ λ ⤍ 𝜎1 ⟧</bind>"- , " <built meta=\"𝑛.1.1\">⟦ z ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧</built>"- , " <answer meta=\"𝑛.1.2\">⟦ z ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧</answer>"+ , " <bind meta=\"𝑛2.1\">𝜎1:λ</bind>"+ , " <built meta=\"𝑛.1.1\">𝜎1:λ:z</built>"+ , " <answer meta=\"𝑛.1.2\">𝜎1:λ:z</answer>" , " </evaluate>" , "</morph>" ]@@ -1480,12 +1480,12 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<morph locator=\"Φ.y\">" , " <evaluate λ=\"L_fork\" id=\"1\" judgment=\"morph\" locator=\"Φ.y\">"- , " <bind meta=\"𝑛1.1\">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧</bind>"- , " <bind meta=\"𝑛2.1\">⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧</bind>"+ , " <bind meta=\"𝑛1.1\">𝜎1:λ:φ</bind>"+ , " <bind meta=\"𝑛2.1\">𝜎2:λ:φ</bind>" , " <joined symbol=\"𝜎3\">𝜎1 𝜎2</joined>"- , " <bind meta=\"𝑛3.1\">⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧</bind>"- , " <built meta=\"𝑛.1.1\">⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧</answer>"+ , " <bind meta=\"𝑛3.1\">𝜎3:λ:φ</bind>"+ , " <built meta=\"𝑛.1.1\">𝜎3:λ:φ</built>"+ , " <answer meta=\"𝑛.1.2\">𝜎3:λ:φ</answer>" , " </evaluate>" , "</morph>" ]@@ -1506,11 +1506,11 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<morph locator=\"Φ.y\">" , " <evaluate λ=\"L_pair\" id=\"1\" judgment=\"morph\" locator=\"Φ.y\">"- , " <bind meta=\"𝑛1.1\">⟦ Δ ⤍ 01- ⟧</bind>"+ , " <bind meta=\"𝑛1.1\">01-:Δ</bind>" , " <minted>𝜎1</minted>" , " <minted>𝜎2</minted>"- , " <built meta=\"𝑛.1.1\">⟦ left ↦ ⟦ λ ⤍ 𝜎1 ⟧, right ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧</built>"- , " <answer meta=\"𝑛.1.2\">⟦ left ↦ ⟦ λ ⤍ 𝜎1 ⟧, right ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧</answer>"+ , " <built meta=\"𝑛.1.1\">⟦ left ↦ 𝜎1:λ, right ↦ 𝜎2:λ ⟧</built>"+ , " <answer meta=\"𝑛.1.2\">⟦ left ↦ 𝜎1:λ, right ↦ 𝜎2:λ ⟧</answer>" , " </evaluate>" , "</morph>" ]@@ -1529,9 +1529,9 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<morph locator=\"Φ.y\">" , " <evaluate λ=\"L_keep\" id=\"1\" judgment=\"morph\" locator=\"Φ.y\">"- , " <bind meta=\"𝑛1.1\">⟦ Δ ⤍ 01- ⟧</bind>"- , " <built meta=\"𝑛.1.1\">⟦ z ↦ ⟦ Δ ⤍ 01- ⟧ ⟧</built>"- , " <answer meta=\"𝑛.1.2\">⟦ z ↦ ⟦ Δ ⤍ 01- ⟧ ⟧</answer>"+ , " <bind meta=\"𝑛1.1\">01-:Δ</bind>"+ , " <built meta=\"𝑛.1.1\">01-:Δ:z</built>"+ , " <answer meta=\"𝑛.1.2\">01-:Δ:z</answer>" , " </evaluate>" , "</morph>" ]@@ -1554,13 +1554,13 @@ , " <bind meta=\"𝛿1.2\">40-18-00-00-00-00-00-00</bind>" , " <bind meta=\"𝛿2.2\">40-1C-00-00-00-00-00-00</bind>" , " <minted>𝜎1</minted>"- , " <built meta=\"𝑛.2.1\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>"- , " <answer meta=\"𝑛.2.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>"+ , " <built meta=\"𝑛.2.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <answer meta=\"𝑛.2.2\">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>" , " </evaluate>"- , " <dataize meta=\"𝛿2.1\">⟦ λ ⤍ 𝜎1 ⟧</dataize>"+ , " <dataize meta=\"𝛿2.1\">𝜎1:λ</dataize>" , " <minted>𝜎2</minted>"- , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ )</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>"+ , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎2:λ )</built>"+ , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎2:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧</answer>" , " </evaluate>" , "</dataize>" ]@@ -1582,10 +1582,10 @@ , " <bind meta=\"𝛿1.1\">40-00-00-00-00-00-00-00</bind>" , " <bind meta=\"𝛿2.1\">40-08-00-00-00-00-00-00</bind>" , " <minted>𝜎1</minted>"- , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, nope ↦ ⟦ λ ⤍ L_number_nope ⟧ ⟧</answer>"+ , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎1:λ, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, nope ↦ L_number_nope:λ ⟧</answer>" , " </evaluate>"- , " <stuck λ=\"L_number_nope\" judgment=\"dataize\">⟦ λ ⤍ L_number_nope ⟧</stuck>"+ , " <stuck λ=\"L_number_nope\" judgment=\"dataize\">L_number_nope:λ</stuck>" , "</dataize>" ] @@ -1683,7 +1683,7 @@ withStdin stuck $ testCLISucceeded ["dataize", symbolic, "--partial", "--sweet", "--hide-rho"]- ["⟦ λ ⤍ L_number_nope ⟧"]+ ["L_number_nope:λ"] -- What the firing before the stuck one answered is a symbol, and the -- residue carries it where the value nobody worked out belongs@@ -1691,7 +1691,7 @@ withStdin stuck $ testCLISucceeded ["dataize", symbolic, "--partial", "--sweet"]- ["φ ↦ ⟦ λ ⤍ 𝜎1 ⟧"]+ ["φ ↦ 𝜎1:λ"] it "records every firing before the stuck site in --protocol" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do@@ -1704,9 +1704,9 @@ , " 𝔼(L_number_times) # 𝕄(Φ)" , " 𝛿1.1 := 40-00-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿2.1 := 40-08-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, nope ↦ ⟦ λ ⤍ L_number_nope ⟧ ⟧ # 𝕄(𝑛.1.1)"- , " ?(L_number_nope) # 𝔻(⟦ λ ⤍ L_number_nope ⟧)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, nope ↦ L_number_nope:λ ⟧ # 𝕄(𝑛.1.1)"+ , " ?(L_number_nope) # 𝔻(L_number_nope:λ)" ] it "still prints bytes when nothing gets stuck" $@@ -1739,7 +1739,7 @@ withStdin stuck $ testCLISucceeded ["dataize", symbolic, "--partial", "--sequence", "--sweet", "--hide-rho", "--flat"]- ["2.times( 3 ).nope", "⟦ λ ⤍ L_number_nope ⟧"]+ ["2.times( 3 ).nope", "L_number_nope:λ"] it "still stops on the terminator ⊥, since a wrong operand is not a stuck λ function" $ withStdin "[[ ]]" $@@ -1933,8 +1933,8 @@ , " 𝔼(L_number_plus) # 𝕄(Φ.φ)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿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)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧ # 𝕄(𝑛.1.1)" ] it "saves morphing steps to dir with --steps-dir" $@@ -2012,7 +2012,7 @@ withStdin program $ testCLISucceeded ["morph", symbolic, "--deep", "--inside=Q.demo.foo", "--sweet", "--hide-rho", "--flat"]- ["⟦ n ↦ 3, φ ↦ Φ.bar( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ ) ⟧"]+ ["⟦ n ↦ 3, φ ↦ Φ.bar( ⟦ φ ↦ 𝜎2:λ, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ ) ⟧"] -- The same term the run above stops at as a bare λ-formation: 'mf' leaves -- it to 𝔻, and the walk fires it instead of demanding bytes@@ -2020,7 +2020,7 @@ withStdin chained $ testCLISucceeded ["morph", symbolic, "--deep", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]- ["⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧"]+ ["⟦ φ ↦ 𝜎2:λ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧"] -- The default locator walks the whole program: the method table of the -- object model keeps every one of its λ-formations, since not one of them@@ -2030,14 +2030,14 @@ testCLISucceeded ["morph", symbolic, "--deep", "--sweet", "--hide-rho", "--flat"] [ "number(φ) ↦ ⟦ times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧"- , "demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ ) ⟧ ⟧"+ , "demo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( ⟦ φ ↦ 𝜎2:λ, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ ) ⟧:foo" ] it "keeps a binding whose spine got stuck with --partial" $ withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $ testCLISucceeded ["morph", "--deep", "--partial", "--sweet", "--hide-rho", "--flat"]- ["⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧.foo ⟧"]+ ["Sym_arg_0:λ.foo:x"] it "fails on that same spine without --partial" $ withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $@@ -2443,23 +2443,21 @@ it "merges single expression" $ testCLISucceeded ["merge", resource "desugar.phi", "--sweet", "--flat"]- ["⟦ foo ↦ x ⟧"]+ ["x:foo"] it "merges EO expressions" $ testCLISucceeded ["merge", "--sweet", resource "number.phi", resource "bytes.phi", resource "string.phi", "--margin=25"] [ unlines [ "⟦"- , " org ↦ ⟦"- , " eolang ↦ ⟦"- , " number(φ) ↦ ⟦⟧,"- , " bytes(data) ↦ ⟦⟧,"- , " string(φ) ↦ ⟦⟧,"- , " λ ⤍ Package"- , " ⟧,"+ , " eolang ↦ ⟦"+ , " number(φ) ↦ ⟦⟧,"+ , " bytes(data) ↦ ⟦⟧,"+ , " string(φ) ↦ ⟦⟧," , " λ ⤍ Package"- , " ⟧"- , "⟧"+ , " ⟧,"+ , " λ ⤍ Package"+ , "⟧:org" ] ]
test/CSTSpec.hs view
@@ -44,11 +44,29 @@ [ ("Q", EX_GLOBAL Φ) , ( "[[ x -> Q.y ]]"+ , EX_SINGLE+ (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y")))+ ( EX_FORMATION+ LSB+ EOL+ (TAB 1)+ (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1))+ EOL+ (TAB 0)+ RSB+ )+ )+ ,+ ( "[[ x -> Q.y, z -> Q ]]" , EX_FORMATION LSB EOL (TAB 1)- (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y"))) (BDS_EMPTY (TAB 1)) (TAB 1))+ ( BI_PAIR+ (PA_TAU (AT_LABEL "x") ARROW (EX_DISPATCH (EX_GLOBAL Φ) NO_SPACE (AT_LABEL "y")))+ (BDS_PAIR EOL (TAB 1) (PA_TAU (AT_LABEL "z") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 1)))+ (TAB 1)+ ) EOL (TAB 0) RSB@@ -131,12 +149,12 @@ describe "expressionToCSTFrom lays out a formation from a given base indent" $ it "nests the body one level below the given tabs and closes at it" $- expressionToCSTFrom 2 (ExFormation [BiTau (AtLabel "x") ExRoot])+ expressionToCSTFrom 2 (ExFormation [BiTau (AtLabel "x") ExRoot, BiVoid (AtLabel "y")]) `shouldBe` EX_FORMATION LSB EOL (TAB 3)- (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_EMPTY (TAB 3)) (TAB 3))+ (BI_PAIR (PA_TAU (AT_LABEL "x") ARROW (EX_GLOBAL Φ)) (BDS_PAIR EOL (TAB 3) (PA_VOID (AT_LABEL "y") ARROW EMPTY) (BDS_EMPTY (TAB 3))) (TAB 3)) EOL (TAB 2) RSB
test/DataizeSpec.hs view
@@ -259,14 +259,14 @@ [ " 𝔼(L_number_times) # 𝕄(Φ)" , " 𝛿1.1 := 40-00-00-00-00-00-00-00 # 𝔻(ξ.ρ)" , " 𝛿2.1 := 40-08-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, as-bytes ↦ φ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, div(x) ↦ ⟦ λ ⤍ L_number_div ⟧, gt(x) ↦ ⟦ λ ⤍ L_number_gt ⟧, eq(x) ↦ ⟦ φ ↦ ρ.as-bytes.eq( x.as-bytes ) ⟧, nope ↦ ⟦ λ ⤍ L_number_nope ⟧, ρ ↦ Φ ⟧ # 𝕄(𝑛.1.1)"- , " ?(L_number_nope) # 𝔻(⟦ λ ⤍ L_number_nope, ρ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, as-bytes ↦ φ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, div(x) ↦ ⟦ λ ⤍ L_number_div ⟧, gt(x) ↦ ⟦ λ ⤍ L_number_gt ⟧, eq(x) ↦ ⟦ φ ↦ ρ.as-bytes.eq( x.as-bytes ) ⟧, nope ↦ ⟦ λ ⤍ L_number_nope ⟧, ρ ↦ Φ ⟧ ⟧)"+ , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, as-bytes ↦ φ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, div(x) ↦ ⟦ λ ⤍ L_number_div ⟧, gt(x) ↦ ⟦ λ ⤍ L_number_gt ⟧, eq(x) ↦ ⟦ φ ↦ ρ.as-bytes.eq( x.as-bytes ) ⟧, nope ↦ L_number_nope:λ, ρ ↦ Φ ⟧ # 𝕄(𝑛.1.1)"+ , " ?(L_number_nope) # 𝔻(⟦ λ ⤍ L_number_nope, ρ ↦ ⟦ φ ↦ 𝜎1:λ, as-bytes ↦ φ, plus(x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧, div(x) ↦ ⟦ λ ⤍ L_number_div ⟧, gt(x) ↦ ⟦ λ ⤍ L_number_gt ⟧, eq(x) ↦ ⟦ φ ↦ ρ.as-bytes.eq( x.as-bytes ) ⟧, nope ↦ L_number_nope:λ, ρ ↦ Φ ⟧ ⟧)" ] it "leaves an unanswered λ function dataized directly as the whole residue" $ do ((outcome, chain), protocol) <- partially known "[[ L> Sym_arg_0 ]]" outcome `shouldBe` Residual placeholder- protocol `shouldBe` " ?(Sym_arg_0) # 𝔻(⟦ λ ⤍ Sym_arg_0 ⟧)\n"+ protocol `shouldBe` " ?(Sym_arg_0) # 𝔻(Sym_arg_0:λ)\n" map fst chain `shouldEndWith` [placeholder] it "still reaches the manufactured datum when nothing is stuck" $ do ((outcome, _), _) <- partially known "2.times(3)"
test/EvaluateSpec.hs view
@@ -164,7 +164,7 @@ let stuck = (withLambdas known (defaultReduceContext ExRoot)){_saveEval = record} fire = execBuildTerm univ stuck "evaluate" [ArgExpression (ExFormation [BiLambda (FnSymbol 1)]), ArgExpression univ] substEmpty fire `shouldThrow` (\e -> "No entry of --symbolic answers the λ function '𝜎1'" `isInfixOf` show (e :: SomeException))- written `shouldBe` " ?(𝜎1) # 𝕄(⟦ λ ⤍ 𝜎1 ⟧)\n"+ written `shouldBe` " ?(𝜎1) # 𝕄(𝜎1:λ)\n" -- Two λ bindings never reach 𝔼: the builder refuses to make a formation out -- of them first. The case is here anyway, since what matters is that such a
test/MarginSpec.hs view
@@ -18,7 +18,7 @@ bigLabel = AtLabel "aVeryLongAttributeNameThatWontFitOnOneLine" bigFormation :: Expression-bigFormation = ExFormation [BiTau bigLabel ExRoot]+bigFormation = ExFormation [BiTau bigLabel ExRoot, BiTau AtRho ExRoot] nestedFormation :: Expression nestedFormation =@@ -69,31 +69,31 @@ ( "keeps the whole application on one line when it all fits" , 100 , longCalleeShortArg- , "⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ ⟧( y ↦ ρ )"+ , "⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ, ρ ↦ Φ ⟧( y ↦ ρ )" ) , ( "wraps only the callee formation when the callee alone still fits alongside the argument" , 10 , longCalleeShortArg- , "⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ\n⟧( y ↦ ρ )"+ , "⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ,\n ρ ↦ Φ\n⟧( y ↦ ρ )" ) , ( "wraps both the callee and the argument when neither fits alongside the other" , 1 , longCalleeShortArg- , "⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ\n⟧(\n y ↦ ρ\n)"+ , "⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ,\n ρ ↦ Φ\n⟧(\n y ↦ ρ\n)" ) , ( "keeps a short callee on one line and wraps only the argument"- , 60+ , 65 , shortCalleeLongArg- , "Φ.x(\n y ↦ ⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ ⟧\n)"+ , "Φ.x(\n y ↦ ⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ, ρ ↦ Φ ⟧\n)" ) , ( "wraps the argument formation itself when it does not fit even on its own line" , 1 , shortCalleeLongArg- , "Φ.x(\n y ↦ ⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ\n ⟧\n)"+ , "Φ.x(\n y ↦ ⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ,\n ρ ↦ Φ\n ⟧\n)" ) ] (\(desc, margin, expression, expected) -> it desc (render (withMargin margin (expressionToCST expression)) `shouldBe` expected))@@ -114,10 +114,10 @@ describe "withMargin on mixed tau/alpha (AA_TAUS with PA_ALPHA) application arguments" $ forM_- [ (100, "Φ.x( a ↦ Φ, α5 ↦ ⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ ⟧ )")+ [ (100, "Φ.x( a ↦ Φ, α5 ↦ ⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ, ρ ↦ Φ ⟧ )") , ( 1- , "Φ.x(\n a ↦ Φ,\n α5 ↦ ⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ\n ⟧\n)"+ , "Φ.x(\n a ↦ Φ,\n α5 ↦ ⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ,\n ρ ↦ Φ\n ⟧\n)" ) ] ( \(margin, expected) ->@@ -148,7 +148,24 @@ ( "recurses into the dispatched-upon expression" , 1 , ExDispatch bigFormation (AtLabel "z")- , "⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ\n⟧.z"+ , "⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ,\n ρ ↦ Φ\n⟧.z"+ )+ ]+ (\(desc, margin, expression, expected) -> it desc (render (withMargin margin (expressionToCST expression)) `shouldBe` expected))++ describe "withMargin on a one-binding formation" $+ forM_+ [+ ( "keeps the sugar on one line when it fits the margin"+ , 100+ , ExFormation [BiTau (AtLabel "x") shortCalleeLongArg]+ , "Φ.x( y ↦ ⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ, ρ ↦ Φ ⟧ ):x"+ )+ ,+ ( "wraps the asset of the sugar and keeps the attribute after it"+ , 1+ , ExFormation [BiTau (AtLabel "x") shortCalleeLongArg]+ , "Φ.x(\n y ↦ ⟦\n aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ,\n ρ ↦ Φ\n ⟧\n):x" ) ] (\(desc, margin, expression, expected) -> it desc (render (withMargin margin (expressionToCST expression)) `shouldBe` expected))
test/ParserSpec.hs view
@@ -668,3 +668,57 @@ [ ("[[ x -> \"\\uD835\\u0041\"]]", "Invalid low surrogate:") , ("[[ x -> \"\\uDFFF\"]]", "Unexpected low surrogate:") ]++ describe "parse the one-binding formation sugar" $+ forM_+ [ ("FF-AA:Δ", "⟦ Δ ⤍ FF-AA ⟧")+ , ("FF-AA:D", "⟦ Δ ⤍ FF-AA ⟧")+ , ("--:Δ", "⟦ Δ ⤍ -- ⟧")+ , ("1F-:Δ", "⟦ Δ ⤍ 1F- ⟧")+ , ("𝛿1:Δ", "⟦ Δ ⤍ 𝛿1 ⟧")+ , ("𝜎1:λ", "⟦ λ ⤍ 𝜎1 ⟧")+ , ("!S1:L", "⟦ λ ⤍ 𝜎1 ⟧")+ , ("Plus:λ", "⟦ λ ⤍ Plus ⟧")+ , ("Q:λ", "⟦ λ ⤍ Q ⟧")+ , ("T:L", "⟦ λ ⤍ T ⟧")+ , ("Qx:λ", "⟦ λ ⤍ Qx ⟧")+ , ("T_1 : λ", "⟦ λ ⤍ T_1 ⟧")+ , ("T:x", "⟦ x ↦ ⊥ ⟧")+ , ("Q.x:y", "⟦ y ↦ Φ.x ⟧")+ , ("!F1:L", "⟦ λ ⤍ 𝑓1 ⟧")+ , ("∅:a", "⟦ a ↦ ∅ ⟧")+ , ("?:a", "⟦ a ↦ ∅ ⟧")+ , ("?:!t1", "⟦ 𝜏1 ↦ ∅ ⟧")+ , ("ξ.a:φ", "⟦ φ ↦ ξ.a ⟧")+ , ("$.a:@", "⟦ φ ↦ ξ.a ⟧")+ , ("$.a : @", "⟦ φ ↦ ξ.a ⟧")+ , ("ξ:ρ", "⟦ ρ ↦ ξ ⟧")+ , ("Q:x", "⟦ x ↦ Φ ⟧")+ , ("Q.x(y):z", "⟦ z ↦ Φ.x(y) ⟧")+ , ("42:φ", "⟦ φ ↦ 42 ⟧")+ , ("1E-05:φ", "⟦ φ ↦ 1E-05 ⟧")+ , ("\"hi\":φ", "⟦ φ ↦ \"hi\" ⟧")+ , ("𝑒1:𝜏1", "⟦ 𝜏1 ↦ 𝑒1 ⟧")+ , ("ξ.a:φ.b", "⟦ φ ↦ ξ.a ⟧.b")+ , ("ξ.a:φ:b", "⟦ b ↦ ⟦ φ ↦ ξ.a ⟧ ⟧")+ , ("FF-:Δ.x", "⟦ Δ ⤍ FF- ⟧.x")+ , ("Q.x(ξ.a:φ)", "Q.x(⟦ φ ↦ ξ.a ⟧)")+ , ("⟦ x ↦ y:φ, z ↦ FF-:Δ ⟧", "⟦ x ↦ ⟦ φ ↦ ξ.y ⟧, z ↦ ⟦ Δ ⤍ FF- ⟧ ⟧")+ , ("⟦ x ↦ ∅:a, y ↦ ∅ ⟧", "⟦ x ↦ ⟦ a ↦ ∅ ⟧, y ↦ ∅ ⟧")+ , ("[[ x -> ?:a ]]", "⟦ x ↦ ⟦ a ↦ ∅ ⟧ ⟧")+ , ("Q.x(y -> ?:a)", "Q.x(y ↦ ⟦ a ↦ ∅ ⟧)")+ , ("Q.x(α0 ↦ Plus:λ)", "Q.x(α0 ↦ ⟦ λ ⤍ Plus ⟧)")+ ]+ ( \(sweet, plain) ->+ it sweet $ do+ parseExpression plain `shouldSatisfy` isRight+ parseExpression sweet `shouldBe` parseExpression plain+ )++ describe "rejects a broken one-binding formation sugar" $+ test+ parseExpression+ ( map+ (\ipt -> (ipt, Nothing :: Maybe Expression))+ ["FF-AA:φ", "Plus:x", "∅:Δ", "ξ.a:", ":φ", "ξ.a:Δ", "ξ.a:λ"]+ )
test/PrinterSpec.hs view
@@ -30,15 +30,15 @@ , ("Φ renders as Q", ExRoot, "Q") , ("⊥ renders as T", ExTermination, "T") , ("ρ void becomes empty", ExFormation [BiVoid AtRho], "[[]]")- , ("φ void", ExFormation [BiVoid AtPhi], "[[ @ -> ? ]]")- , ("label void", ExFormation [BiVoid (AtLabel "名前")], "[[ 名前 -> ? ]]")- , ("x to Φ", ExFormation [BiTau (AtLabel "x") ExRoot], "[[ x -> Q ]]")- , ("ρ to ⊥", ExFormation [BiTau AtRho ExTermination], "[[ ^ -> T ]]")- , ("empty delta", ExFormation [BiDelta BtEmpty], "[[ D> -- ]]")- , ("single byte", ExFormation [BiDelta (BtOne "1F")], "[[ D> 1F- ]]")- , ("multiple bytes", ExFormation [BiDelta (BtMany ["00", "01", "02"])], "[[ D> 00-01-02 ]]")- , ("función lambda", ExFormation [BiLambda (Function "Función")], "[[ L> Función ]]")- , ("クラス lambda", ExFormation [BiLambda (Function "クラス")], "[[ L> クラス ]]")+ , ("φ void", ExFormation [BiVoid AtPhi], "?:@")+ , ("label void", ExFormation [BiVoid (AtLabel "名前")], "?:名前")+ , ("x to Φ", ExFormation [BiTau (AtLabel "x") ExRoot], "Q:x")+ , ("ρ to ⊥", ExFormation [BiTau AtRho ExTermination], "T:^")+ , ("empty delta", ExFormation [BiDelta BtEmpty], "--:D")+ , ("single byte", ExFormation [BiDelta (BtOne "1F")], "1F-:D")+ , ("multiple bytes", ExFormation [BiDelta (BtMany ["00", "01", "02"])], "00-01-02:D")+ , ("función lambda", ExFormation [BiLambda (Function "Función")], "Función:L")+ , ("クラス lambda", ExFormation [BiLambda (Function "クラス")], "クラス:L") , ("Φ.org", ExDispatch ExRoot (AtLabel "org"), "Q.org") , ("ξ.ρ as sugar", ExDispatch ExXi AtRho, "^") , ("ξ.φ as sugar", ExDispatch ExXi AtPhi, "@")@@ -55,8 +55,8 @@ ) , ("meta expr", ExMeta "e", "!e") , ("meta binding", ExFormation [BiMeta "B"], "[[ !B ]]")- , ("meta lambda", ExFormation [BiLambda (FnMeta "F")], "[[ L> !F ]]")- , ("meta attr tau", ExFormation [BiTau (AtMeta "t") ExXi], "[[ !t -> $ ]]")+ , ("meta lambda", ExFormation [BiLambda (FnMeta "F")], "!F:L")+ , ("meta attr tau", ExFormation [BiTau (AtMeta "t") ExXi], "$:!t") ] ( \(desc, expr, expected) -> it desc (printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin) `shouldBe` expected)@@ -73,7 +73,7 @@ describe "printExpression with SWEET UNICODE renders the pretty function meta" $ it "meta lambda becomes 𝑓" $- printExpression' (ExFormation [BiLambda (FnMeta "F")]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ λ ⤍ 𝑓 ⟧"+ printExpression' (ExFormation [BiLambda (FnMeta "F")]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "𝑓:λ" describe "printExpression names the non-finite doubles instead of spelling their bytes" $ forM_@@ -225,12 +225,12 @@ ] forM_ [ ("salty clears both void and dispatch-valued rho", SALTY, issueExpr, "⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧")- , ("sweet also drops the rho that --sweet keeps", SWEET, issueExpr, "⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧")+ , ("sweet also drops the rho that --sweet keeps", SWEET, issueExpr, "⟦ foo ↦ ⟦⟧:x, y ↦ ⟦⟧ ⟧") , ( "a rho bound to an expression is removed" , SWEET , ExFormation [BiTau (AtLabel "a") ExRoot, BiTau AtRho (ExDispatch ExXi (AtLabel "y"))]- , "⟦ a ↦ Φ ⟧"+ , "Φ:a" ) , ("a formation holding only rho collapses to empty", SALTY, ExFormation [BiVoid AtRho], "⟦⟧") ,@@ -288,12 +288,12 @@ ] (\(desc, alpha, expected) -> it desc (printAlpha alpha `shouldBe` expected)) - describe "printBinding renders as formation" $+ describe "printBinding renders as a one-binding formation" $ forM_- [ ("tau binding", BiTau (AtLabel "x") ExRoot, "x ↦ Φ")- , ("void binding", BiVoid (AtLabel "y"), "y ↦ ∅")- , ("delta binding", BiDelta (BtOne "00"), "Δ ⤍ 00-")- , ("lambda binding", BiLambda (Function "Func"), "λ ⤍ Func")+ [ ("tau binding", BiTau (AtLabel "x") ExRoot, "Φ:x")+ , ("void binding", BiVoid (AtLabel "y"), "∅:y")+ , ("delta binding", BiDelta (BtOne "00"), "00-:Δ")+ , ("lambda binding", BiLambda (Function "Func"), "Func:λ") , ("meta binding", BiMeta "B", "𝐵") ] ( \(desc, bd, expected) ->@@ -314,7 +314,7 @@ describe "printExtraArg renders arguments" $ forM_ [ ("attribute arg", ArgAttribute (AtLabel "tëst"), "tëst")- , ("binding arg", ArgBinding (BiVoid (AtLabel "βind")), "βind ↦ ∅")+ , ("binding arg", ArgBinding (BiVoid (AtLabel "βind")), "∅:βind") , ("expression arg", ArgExpression ExRoot, "Φ") , ("bytes arg", ArgBytes (BtOne "FF"), "FF-") ]@@ -328,7 +328,7 @@ , ("MvIndex", [Subst (Map.singleton (Named "i") (MvIndex 3))], (SWEET, UNICODE, MULTILINE, defaultMargin), "i >> 3") , ("MvExpression", [Subst (Map.singleton (Named "e") (MvExpression ExRoot))], (SWEET, UNICODE, MULTILINE, defaultMargin), "e >> Φ") , ("MvBytes", [Subst (Map.singleton (Named "b") (MvBytes (BtOne "1F")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "b >> 1F-")- , ("MvBindings", [Subst (Map.singleton (Named "bnd") (MvBindings [BiVoid (AtLabel "y")]))], (SWEET, UNICODE, MULTILINE, defaultMargin), "bnd >> ⟦ y ↦ ∅ ⟧")+ , ("MvBindings", [Subst (Map.singleton (Named "bnd") (MvBindings [BiVoid (AtLabel "y")]))], (SWEET, UNICODE, MULTILINE, defaultMargin), "bnd >> ∅:y") , ("MvFunction", [Subst (Map.singleton (Named "f") (MvFunction (Function "func")))], (SWEET, UNICODE, MULTILINE, defaultMargin), "f >> func") , ( "keys of a multi-entry substitution are sorted and each is on its own line"@@ -367,8 +367,68 @@ ) , BiTau AtRho ExRoot ]- printExpressionHidingRho' deep (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ a ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧"+ printExpressionHidingRho' deep (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦⟧:b:a" describe "logPrintConfig" $ it "is a fixed SWEET/UNICODE/SINGLELINE config at the default margin" $ logPrintConfig `shouldBe` (SWEET, UNICODE, SINGLELINE, defaultMargin)++ describe "printExpression' spells one-binding formations the way the parser reads them back" $+ forM_+ [ "⟦ x ↦ ξ.a ⟧"+ , "⟦ Δ ⤍ FF-AA ⟧"+ , "⟦ Δ ⤍ -- ⟧"+ , "⟦ λ ⤍ Plus ⟧"+ , "⟦ λ ⤍ 𝜎1 ⟧"+ , "⟦ λ ⤍ Q ⟧"+ , "⟦ λ ⤍ Tx ⟧"+ , "⟦ a ↦ ∅ ⟧"+ , "⟦ ρ ↦ ξ ⟧"+ , "⟦ φ ↦ ⊥ ⟧"+ , "⟦ φ ↦ Φ ⟧"+ , "⟦ φ ↦ 42 ⟧"+ , "⟦ φ ↦ -4.5 ⟧"+ , "⟦ φ ↦ \"hi\" ⟧"+ , "⟦ x ↦ ⟦ y ↦ ⟦ z ↦ ξ.q ⟧ ⟧ ⟧"+ , "⟦ x ↦ ⟦ φ ↦ ξ.a ⟧.b ⟧"+ , "⟦ x ↦ ⟦ φ ↦ ξ.a ⟧(y ↦ ⟦ Δ ⤍ 01- ⟧) ⟧"+ , "⟦ x(a) ↦ ⟦ φ ↦ a ⟧ ⟧"+ , "⟦ x ↦ ⟦⟧ ⟧"+ , "⟦ x ↦ Φ.number(Φ.bytes(⟦ Δ ⤍ 7F-F8-00-00-00-00-00-01 ⟧)) ⟧"+ , "⟦ x ↦ Φ.y(⟦ φ ↦ ξ.z ⟧, ⟦ λ ⤍ Fn ⟧) ⟧"+ , "⟦ x ↦ ⟦ λ ⤍ Fn, ρ ↦ ⟦ φ ↦ ξ ⟧ ⟧, y ↦ ∅ ⟧"+ , "⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ.x(y ↦ ⟦ aVeryLongAttributeNameThatWontFitOnOneLine ↦ Φ ⟧) ⟧"+ ]+ ( \src -> it src $ do+ let expr = either error id (parseExpression src)+ forM_+ [ (encoding, line)+ | encoding <- [UNICODE, ASCII]+ , line <- [SINGLELINE, MULTILINE]+ ]+ ( \(encoding, line) ->+ parseExpression (printExpression' expr (SWEET, encoding, line, 20)) `shouldBe` Right expr+ )+ )++ describe "printExpression' writes the one-binding sugar in the sweet syntax only" $+ forM_+ [ ("⟦ x ↦ ξ.a ⟧", SWEET, UNICODE, "a:x")+ , ("⟦ Δ ⤍ FF-AA ⟧", SWEET, UNICODE, "FF-AA:Δ")+ , ("⟦ Δ ⤍ FF-AA ⟧", SWEET, ASCII, "FF-AA:D")+ , ("⟦ λ ⤍ 𝜎1 ⟧", SWEET, UNICODE, "𝜎1:λ")+ , ("⟦ λ ⤍ 𝜎1 ⟧", SWEET, ASCII, "!S1:L")+ , ("⟦ a ↦ ∅ ⟧", SWEET, ASCII, "?:a")+ , ("⟦ φ ↦ ξ.a ⟧", SWEET, ASCII, "a:@")+ , ("⟦ x ↦ ⟦ y ↦ ξ.z ⟧ ⟧", SWEET, UNICODE, "z:y:x")+ , ("⟦ x ↦ ⟦ φ ↦ ξ.a ⟧.b ⟧", SWEET, UNICODE, "a:φ.b:x")+ , ("⟦ x(a) ↦ ⟦ φ ↦ a ⟧ ⟧", SWEET, UNICODE, "⟦ x(a) ↦ ⟦ φ ↦ a ⟧ ⟧")+ , ("⟦ x ↦ ξ.a, y ↦ ∅ ⟧", SWEET, UNICODE, "⟦ x ↦ a, y ↦ ∅ ⟧")+ , ("⟦ x ↦ ξ.a ⟧", SALTY, UNICODE, "⟦ x ↦ ξ.a, ρ ↦ ∅ ⟧")+ , ("⟦ Δ ⤍ FF-AA ⟧", SALTY, ASCII, "[[ D> FF-AA, ^ -> ? ]]")+ ]+ ( \(src, sugar, encoding, expected) ->+ it (src ++ " " ++ show sugar ++ " " ++ show encoding) $ do+ let expr = either error id (parseExpression src)+ printExpression' expr (sugar, encoding, SINGLELINE, defaultMargin) `shouldBe` expected+ )
test/SugarSpec.hs view
@@ -618,8 +618,28 @@ , EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "some.func") (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB ) ]- (\(desc, input, expected) -> it desc (withoutRho input `shouldBe` expected))+ (\(desc, input, expected) -> it desc (withoutRho SALTY input `shouldBe` expected)) + describe "withoutRho in the sweet syntax" $+ forM_+ [+ ( "a formation left with one binding takes the one-binding sugar"+ , EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "Fn") (BDS_PAIR EOL (TAB 1) (PA_TAU (AT_RHO RHO) ARROW xiExpr) (BDS_EMPTY (TAB 1))) (TAB 1)) EOL (TAB 0) RSB+ , EX_SINGLE (PA_LAMBDA "Fn") (EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "Fn") (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB)+ )+ ,+ ( "a formation left with two bindings stays a formation"+ , EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "Fn") (BDS_PAIR EOL (TAB 1) (PA_DELTA BT_EMPTY) (BDS_EMPTY (TAB 1))) (TAB 1)) EOL (TAB 0) RSB+ , EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_LAMBDA "Fn") (BDS_PAIR EOL (TAB 1) (PA_DELTA BT_EMPTY) (BDS_EMPTY (TAB 1))) (TAB 1)) EOL (TAB 0) RSB+ )+ ,+ ( "a one-binding sugar standing for a rho collapses to the empty formation"+ , EX_SINGLE (PA_TAU (AT_RHO RHO) ARROW xiExpr) (EX_FORMATION LSB EOL (TAB 1) (BI_PAIR (PA_TAU (AT_RHO RHO) ARROW xiExpr) (BDS_EMPTY (TAB 1)) (TAB 1)) EOL (TAB 0) RSB)+ , EX_FORMATION LSB NO_EOL NO_TAB (BI_EMPTY (TAB 1)) NO_EOL NO_TAB RSB+ )+ ]+ (\(desc, input, expected) -> it desc (withoutRho SWEET input `shouldBe` expected))+ describe "full pipeline round trips, SWEET vs SALTY" $ do let config :: SugarType -> (SugarType, Encoding, LineFormat, Int) config sugar = (sugar, UNICODE, SINGLELINE, defaultMargin)@@ -651,5 +671,5 @@ "a phi-meet/phi-again chain renders identically under both sugar types" $ do let meetChain = ExFormation [BiTau (AtLabel "x") (ExPhiMeet Nothing 2 (ExPhiAgain (Just "a") 1 (ExDispatch ExXi (AtLabel "y"))))]- printExpression' meetChain (config SWEET) `shouldBe` "⟦ x ↦ \\phinoMeet{2}{ \\phinoAgain{a:1} } ⟧"+ printExpression' meetChain (config SWEET) `shouldBe` "\\phinoMeet{2}{ \\phinoAgain{a:1} }:x" printExpression' meetChain (config SALTY) `shouldBe` "⟦ x ↦ \\phinoMeet{2}{ \\phinoAgain{a:1} }, ρ ↦ ∅ ⟧"