phino 0.0.149 → 0.0.150
raw patch · 16 files changed
+711/−277 lines, 16 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
+ Deps: EvApplied :: Int -> Judgment -> Expression -> Expression -> Expression -> Evaluation
+ Deps: EvComputed :: Int -> Expression -> Expression -> Evaluation
+ Deps: [_built] :: Protocol -> Map Int Int
+ Deps: [_counted] :: Protocol -> Map Int Int
+ Deps: [_made] :: Protocol -> Named Expression
+ Deps: [_numbered] :: Nesting -> Map Int Int
+ Deps: [_objects] :: Nesting -> Named Expression
+ Deps: abbreviated :: Named Expression -> Expression -> Expression
+ Deps: abbreviatedInside :: Named Expression -> Expression -> Expression
+ Deps: alias :: Int -> Int -> Expression
+ Deps: dontSaveMade :: SaveMadeFunc
+ Deps: namedCarry :: Expression -> Expression -> Named a -> Named a
+ Deps: tier :: Evaluation -> Int
+ Deps: type SaveMadeFunc = Expression -> Expression -> IO ()
+ Rewriter: [_saveMade] :: RewriteContext -> SaveMadeFunc
- CLI.Helpers: aimed :: Maybe String -> Expression -> ReduceContext -> IO (Expression, ReduceContext)
+ CLI.Helpers: aimed :: PrintContext -> Judgment -> Maybe String -> Expression -> ReduceContext -> IO (Expression, ReduceContext)
- Deps: Nesting :: Int -> Map Int Int -> [(Int, String)] -> Nesting
+ Deps: Nesting :: Int -> [(Int, Int)] -> [(Int, String)] -> Named Expression -> Map Int Int -> Nesting
- Deps: Protocol :: Int -> Named -> Map Int Int -> Bool -> Protocol
+ Deps: Protocol :: Int -> Named Text -> [(Int, Int)] -> Bool -> Named Expression -> Map Int Int -> Map Int Int -> Protocol
- Deps: [_named] :: Protocol -> Named
+ Deps: [_named] :: Protocol -> Named Text
- Deps: [_open] :: Protocol -> Map Int Int
+ Deps: [_open] :: Protocol -> [(Int, Int)]
- Deps: [_openedAt] :: Nesting -> Map Int Int
+ Deps: [_openedAt] :: Nesting -> [(Int, Int)]
- Deps: namedInsert :: Expression -> Text -> Named -> Named
+ Deps: namedInsert :: Expression -> a -> Named a -> Named a
- Deps: namedLookup :: Expression -> Named -> Maybe Text
+ Deps: namedLookup :: Expression -> Named a -> Maybe a
- Deps: type Named = Map Int [(Expression, Text)]
+ Deps: type Named a = Map Int [(Expression, a)]
- Rewriter: RewriteContext :: Expression -> Int -> Int -> Bool -> Maybe Expression -> BuildTermFunc -> (Expression -> Bool) -> (Maybe Expression -> Expression -> Set Int) -> Must -> Maybe String -> SaveStepFunc -> RewriteContext
+ Rewriter: RewriteContext :: Expression -> Int -> Int -> Bool -> Maybe Expression -> BuildTermFunc -> (Expression -> Bool) -> (Maybe Expression -> Expression -> Set Int) -> Must -> Maybe String -> SaveStepFunc -> SaveMadeFunc -> RewriteContext
- Rule: Step :: String -> (RuleContext -> Expression -> IO (Maybe Expression)) -> Step
+ Rule: Step :: String -> (RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))) -> Step
- Rule: [_applied] :: Step -> RuleContext -> Expression -> IO (Maybe Expression)
+ Rule: [_applied] :: Step -> RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))
Files
- README.md +109/−36
- phino.cabal +1/−1
- src/CLI/Helpers.hs +11/−5
- src/CLI/Runners.hs +4/−6
- src/Deps.hs +166/−43
- src/LaTeX.hs +9/−1
- src/Morph.hs +6/−2
- src/Rewriter.hs +10/−8
- src/Rule.hs +1/−1
- test/CLISpec.hs +256/−125
- test/CompiledSpec.hs +2/−2
- test/DataizeSpec.hs +14/−7
- test/DepsSpec.hs +58/−4
- test/Fixtures.hs +32/−24
- test/LaTeXSpec.hs +2/−1
- test/RewriterSpec.hs +30/−11
README.md view
@@ -385,16 +385,23 @@ $ cat atoms.txt 𝔻(Φ) formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6 ) ⟧) # 𝔻(Φ)+ applied(𝑛.0.1) := 5 # 𝕄(Φ)+ applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6 ) # 𝕄(Φ) 𝔼(L_number_plus) # 𝔻(Φ)- formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵0)- formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)+ applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)+ formation(𝑛.1.1) # 𝔻(Φ.a🌵0)+ applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)+ formation(𝑛.1.2) # 𝔻(Φ.a🌵0) 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)- formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵1)- formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)+ applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)+ formation(𝑛.1.3) # 𝔻(Φ.a🌵1)+ applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)+ formation(𝑛.1.4) # 𝔻(Φ.a🌵1) 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)- 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛- 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧ # 𝕄(𝑛.1.1)- formation(⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ)+ 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛+ applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)+ 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)+ formation(𝑛.1.6) # 𝔻(Φ) ``` <!-- markdownlint-enable MD013 -->@@ -429,16 +436,41 @@ An answer stands on two lines and not one. A firing answers the term its entry wrote and `phino` morphs that term before standing it back into the program, so-`𝑛.1.1` is what the entry wrote, with the symbols this firing minted already in-it, commented with `𝑛` to name the key it was read from, and `𝑛.1.2` is the-normal form 𝕄 made of it, commented with `𝕄(𝑛.1.1)` to say where it came from.+`𝑛.1.5` is what the entry wrote, with the symbols this firing minted already in+it, commented with `𝑛` to name the key it was read from, and `𝑛.1.7` is the+normal form 𝕄 made of it, commented with `𝕄(𝑛.1.5)` to say where it came from. It is the same morphing every other term goes through, and writing only its outcome would have the formation of `number` appear in place of the three tokens the entry wrote with nothing saying why. Whatever that morphing fires-opens its own block between the two lines, exactly where a firing an operand-took opens one, so the order the lines come in is the order the work was done-in.+or applies writes its lines between the two, exactly where a firing an operand+took opens its block, so the order the lines come in is the order the work was+done in. +`applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)` is an object an application+made. The `copy` rule of normalization fills a void of a formation with the+argument it was given, and so makes a new object, whatever judgment is running+and wherever in the term the application stands. The line binds that object to+a fresh `𝑛` and spells the application: the object applied on the left and the+argument it got on the right, so `5` is `Φ.number( φ ↦ … )` in sugar. The `ρ` a+dispatch gives the attribute it takes writes no line. The comment names the+judgment that normalized and the site it stood at. The name is counted with the+metas of the firing the line stands in, `𝑛.1.5` before it and `𝑛.1.7` after it,+and an object made outside every firing is counted under `𝑛.0`. From then on+every line spells the object by that name rather than as the formation it is,+and the application by the same name, since `copy` makes the same object of the+same application wherever it stands: `formation(𝑛.1.1)` is the object `5` made,+`𝑛.0.1.plus( x ↦ 6 )` is the `plus` of the first `5` applied to `6`, one line+for one call, and `𝑛.1.7 := 𝑛.1.6` says the firing answered with the object 𝕄+made of what the entry wrote. An `applied` line names its head and its argument+that way, each on its own, and never the application as a whole, so a line+spells out every application, even one making an object an earlier one already+made, the way `applied(𝑛.1.1) := 5` does, and a later line names the latest of+them. Only an object still standing as it was made is named: once a rule+rewrote a part of it, it is another object and it is spelled out again. The+walk of `--deep` is no such rule. It stands its answers in the place of what it+computed, inside the bindings of the object it walks, and makes no new object+by doing so, so the object keeps its name once the walk is done with it.+ Where an operand came down to the datum a symbol stands for, the protocol writes `𝔻(𝜎1:λ)` in place of that 42 (`𝜎1:λ` is the formation `⟦ λ ⤍ 𝜎1 ⟧`, in the sugar every sweet term is written with), so a reader sees that the value was@@ -515,15 +547,22 @@ $ cat atoms.txt 𝔻(Φ) formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧, φ ↦ 5.plus( 6 ).nope ⟧) # 𝔻(Φ)+ applied(𝑛.0.1) := 5 # 𝕄(Φ)+ applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6 ) # 𝕄(Φ) 𝔼(L_number_plus) # 𝕄(Φ)- formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵0)- formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)+ applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)+ formation(𝑛.1.1) # 𝔻(Φ.a🌵0)+ applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)+ formation(𝑛.1.2) # 𝔻(Φ.a🌵0) 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)- formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵1)- formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)+ applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)+ formation(𝑛.1.3) # 𝔻(Φ.a🌵1)+ applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)+ formation(𝑛.1.4) # 𝔻(Φ.a🌵1) 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)- 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛- 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧ # 𝕄(𝑛.1.1)+ 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛+ applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)+ 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5) unanswered(L_number_nope) # 𝔻(L_number_nope:λ) ``` @@ -577,18 +616,24 @@ declared there, the copy was made of the one whose attributes cover its own, whose voids it fills the most, and which shares the most bindings with it. When the world declares no such object, or two of them tie, the copy is-written as it stood, such as `⟦ x ↦ 𝜎1:λ, φ ↦ x.next ⟧`.+written as it stood, such as `⟦ x ↦ 𝜎1:λ, φ ↦ x.next ⟧`, or by the name the+`applied` line of the application that made it gave it, such as `𝑛.0.1`. The markup spells it on one line, broken here for reading. The object stands in `of` and the arguments in `<with>`, both written whatever `--abridged`-says, and the copy as it stood stands in `<e>`, abridged as usual:+says, and the copy as it stood stands in `<e>`, abridged and named as usual: ```xml+<applied meta="𝑛.0.1" by="morph" at="Φ.y" of="Φ.box"><attr name="x">𝜎1</attr></applied> <deferred symbol="𝜎2" by="morph" at="Φ.y" of="Φ.box"> <with><attr name="x">𝜎1</attr></with>- <e>⟦ x ↦ 𝜎1:λ, φ ↦ x.next ⟧</e>+ <e>𝑛.0.1</e> </deferred> ``` +A deferred copy is one the walk did not make: the application that made it+writes its own `applied` line, and the `deferred` line says what the walk did+not do with that object.+ Every argument of the call is an `<attr>` of `<with>`. An argument that is a bare symbol, or a carrier of one whose `φ` leads to it, such as `Φ.number( φ ↦ 𝜎1:λ )` or `𝜎1:λ:φ`, is spelled as that symbol, and any other@@ -739,22 +784,29 @@ <?xml version="1.0" encoding="UTF-8"?> <dataize at="Φ"> <formation at="Φ" term="⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6 ) ⟧">+ <applied meta="𝑛.0.1" by="morph" at="Φ" of="Φ.number"><attr name="φ">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>+ <applied meta="𝑛.0.2" by="morph" at="Φ" of="𝑛.0.1.plus"><attr name="x">6</attr></applied> <evaluate λ="L_number_plus" by="dataize" at="Φ">- <formation at="Φ.a🌵0" term="⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧">- <formation at="Φ.a🌵0" term="40-14-00-00-00-00-00-00:Δ:φ">+ <applied meta="𝑛.1.1" by="morph" at="Φ.a🌵0" of="Φ.number"><attr name="φ">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>+ <formation at="Φ.a🌵0" term="𝑛.1.1">+ <applied meta="𝑛.1.2" by="morph" at="Φ.a🌵0" of="Φ.bytes"><attr name="φ">40-14-00-00-00-00-00-00:Δ</attr></applied>+ <formation at="Φ.a🌵0" term="𝑛.1.2"> </formation> </formation> <bind meta="𝛿1.1">40-14-00-00-00-00-00-00</bind>- <formation at="Φ.a🌵1" term="⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧">- <formation at="Φ.a🌵1" term="40-18-00-00-00-00-00-00:Δ:φ">+ <applied meta="𝑛.1.3" by="morph" at="Φ.a🌵1" of="Φ.number"><attr name="φ">Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )</attr></applied>+ <formation at="Φ.a🌵1" term="𝑛.1.3">+ <applied meta="𝑛.1.4" by="morph" at="Φ.a🌵1" of="Φ.bytes"><attr name="φ">40-18-00-00-00-00-00-00:Δ</attr></applied>+ <formation at="Φ.a🌵1" term="𝑛.1.4"> </formation> </formation> <bind meta="𝛿2.1">40-18-00-00-00-00-00-00</bind> <minted symbol="𝜎1">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>- <built meta="𝑛.1.1">Φ.number( φ ↦ 𝜎1:λ )</built>- <answer meta="𝑛.1.2">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧</answer>+ <built meta="𝑛.1.5">Φ.number( φ ↦ 𝜎1:λ )</built>+ <applied meta="𝑛.1.6" by="morph" at="Φ" of="Φ.number"><attr name="φ">𝜎1</attr></applied>+ <answer meta="𝑛.1.7">𝑛.1.6</answer> </evaluate>- <formation at="Φ" term="⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧">+ <formation at="Φ" term="𝑛.1.6"> </formation> </formation> </dataize>@@ -792,6 +844,19 @@ of: two elements rather than two attributes of one, for the same reason `<dataize>` is no `<bind>`. +`<applied meta="𝑛.1.6" by="morph" at="Φ" of="Φ.number">` is an object an+application made, which the text format writes as+`applied(𝑛.1.6) := … # 𝕄(Φ)`: `meta` names the object the way the text format+does, counted with the `<built>` and the `<answer>` of the firing it stands in,+`by` and `at` name the judgment that normalized and the site it stood at, and+`of` names the object applied, the way `<deferred>` and `<looped>` name it.+The argument stands in an `<attr>`, `name` naming the attribute it fills and+the text holding the name of the object or the application it is, the symbol,+such as `𝜎1`, where it is a bare one, and the term itself otherwise. A later+element holding that object holds its name instead, in its text or in its+`term`, so `<answer meta="𝑛.1.7">𝑛.1.6</answer>` says the firing answered with+it and `<formation at="Φ" term="𝑛.1.6">` that 𝔻 got into it.+ `<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@@ -847,20 +912,27 @@ <?xml version="1.0" encoding="UTF-8"?> <dataize at="Φ"> <formation at="Φ" term="⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧, φ ↦ 5.plus( 6 ).nope ⟧">+ <applied meta="𝑛.0.1" by="morph" at="Φ" of="Φ.number"><attr name="φ">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>+ <applied meta="𝑛.0.2" by="morph" at="Φ" of="𝑛.0.1.plus"><attr name="x">6</attr></applied> <evaluate λ="L_number_plus" by="morph" at="Φ">- <formation at="Φ.a🌵0" term="⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧">- <formation at="Φ.a🌵0" term="40-14-00-00-00-00-00-00:Δ:φ">+ <applied meta="𝑛.1.1" by="morph" at="Φ.a🌵0" of="Φ.number"><attr name="φ">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>+ <formation at="Φ.a🌵0" term="𝑛.1.1">+ <applied meta="𝑛.1.2" by="morph" at="Φ.a🌵0" of="Φ.bytes"><attr name="φ">40-14-00-00-00-00-00-00:Δ</attr></applied>+ <formation at="Φ.a🌵0" term="𝑛.1.2"> </formation> </formation> <bind meta="𝛿1.1">40-14-00-00-00-00-00-00</bind>- <formation at="Φ.a🌵1" term="⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧">- <formation at="Φ.a🌵1" term="40-18-00-00-00-00-00-00:Δ:φ">+ <applied meta="𝑛.1.3" by="morph" at="Φ.a🌵1" of="Φ.number"><attr name="φ">Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )</attr></applied>+ <formation at="Φ.a🌵1" term="𝑛.1.3">+ <applied meta="𝑛.1.4" by="morph" at="Φ.a🌵1" of="Φ.bytes"><attr name="φ">40-18-00-00-00-00-00-00:Δ</attr></applied>+ <formation at="Φ.a🌵1" term="𝑛.1.4"> </formation> </formation> <bind meta="𝛿2.1">40-18-00-00-00-00-00-00</bind> <minted symbol="𝜎1">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>- <built meta="𝑛.1.1">Φ.number( φ ↦ 𝜎1:λ )</built>- <answer meta="𝑛.1.2">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧</answer>+ <built meta="𝑛.1.5">Φ.number( φ ↦ 𝜎1:λ )</built>+ <applied meta="𝑛.1.6" by="morph" at="Φ" of="Φ.number"><attr name="φ">𝜎1</attr></applied>+ <answer meta="𝑛.1.7">𝑛.1.6</answer> </evaluate> <unanswered λ="L_number_nope" by="dataize">L_number_nope:λ</unanswered> </formation>@@ -1202,8 +1274,9 @@ ⟧ $ phino morph --deep --locator=Q.y --protocol=p.txt --sweet --hide-rho box.phi 𝜎2:λ-$ head -2 p.txt+$ head -3 p.txt 𝕄(Φ.y)+ applied(𝑛.0.1) := Φ.box( x ↦ 𝜎1:λ ) # 𝕄(Φ.y) deferred(𝜎2) := Φ.box( x ↦ 𝜎1:λ ) # 𝕄(Φ.y) ```
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.149+version: 0.0.150 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
src/CLI/Helpers.hs view
@@ -135,13 +135,19 @@ salted :: PrintContext -> Expression -> IO String salted ctx = flattened ctx{_sugar = SALTY} -aimed :: Maybe String -> Expression -> ReduceContext -> IO (Expression, ReduceContext)-aimed Nothing expr ctx = pure (expr, ctx)-aimed (Just src) expr@(ExFormation _) ctx = do+aimed :: PrintContext -> Judgment -> Maybe String -> Expression -> ReduceContext -> IO (Expression, ReduceContext)+aimed printCtx judgment Nothing expr ctx = do+ heading ctx._saveEval printCtx judgment ctx._locator+ pure (expr, ctx)+aimed printCtx judgment (Just src) expr@(ExFormation _) ctx = do target <- parseExpressionThrows src logDebug (printf "The option '--inside' is specified, reducing '%s' inside the given universe" (P.printExpression target))- insideUniverse target expr ctx-aimed (Just _) expr _ =+ held <- newIORef []+ (universe, aiming) <- insideUniverse target expr ctx{_saveEval = \record -> modifyIORef' held (record :)}+ heading ctx._saveEval printCtx judgment aiming._locator+ mapM_ ctx._saveEval . reverse =<< readIORef held+ pure (universe, aiming{_saveEval = ctx._saveEval})+aimed _ _ (Just _) expr _ = invalidCLIArguments (printf "The option --inside requires the input expression to be a formation, but given: %s" (P.printExpression expr))
src/CLI/Runners.hs view
@@ -23,7 +23,7 @@ import Data.Maybe (fromJust, isJust, isNothing) import qualified Data.Text as T import Dataize-import Deps (Judgment (..))+import Deps (Judgment (..), dontSaveMade) import Emit (emitted) import Encoding import Engine (Engine (..), building, current, stepOf)@@ -76,7 +76,7 @@ include = (`F.include` included) save <- saveStepFunc _stepsDir printCtx included excluded let steps = map (stepOf linked) rules- (rewrittens, exceeded) <- rewrite expr steps (RewriteContext loc _maxDepth _maxCycles _depthSensitive Nothing (building linked) linked._normal (every steps) _must _breakpoint save)+ (rewrittens, exceeded) <- rewrite expr steps (RewriteContext loc _maxDepth _maxCycles _depthSensitive Nothing (building linked) linked._normal (every steps) _must _breakpoint save dontSaveMade) rewrittens' <- include (if _sequence then NE.toList rewrittens else [NE.last rewrittens]) >>= exclude logDebug (printf "Printing rewritten 𝜑-expression as %s" (show _outputFormat)) exprs <- printRewrittens printCtx (rewrittens', exceeded)@@ -184,8 +184,7 @@ printCtx ( \record -> do let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 _depthSensitive _shuffle _partial False 1 _acyclic Dataization [] Map.empty lambdas (building linked) reduction evaluation fired save record linked- (universe, aiming) <- aimed _inside expr ctx- heading record printCtx Dataization aiming._locator+ (universe, aiming) <- aimed printCtx Dataization _inside expr ctx started universe aiming dataize universe emptyState aiming )@@ -267,8 +266,7 @@ printCtx ( \record -> do let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 _depthSensitive _shuffle _partial _deep _jobs _acyclic Morphing [] Map.empty lambdas (building linked) reduction evaluation fired save record linked- (universe, aiming) <- aimed _inside expr ctx- heading record printCtx Morphing aiming._locator+ (universe, aiming) <- aimed printCtx Morphing _inside expr ctx started universe aiming morph universe emptyState aiming )
src/Deps.hs view
@@ -1,5 +1,7 @@ {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT@@ -57,6 +59,11 @@ dontSaveStep :: SaveStepFunc dontSaveStep = saveStep Nothing "" (\_ -> pure "") 0 +type SaveMadeFunc = Expression -> Expression -> IO ()++dontSaveMade :: SaveMadeFunc+dontSaveMade _ _ = pure ()+ data Judgment = Normalization | Morphing@@ -108,6 +115,8 @@ | EvTerminate Int (Maybe (Either Int Bytes)) T.Text T.Text | EvMinted Int Int [Either Int Bytes] | EvDeferred Int Int Judgment Expression (Maybe Expression) Expression+ | EvApplied Int Judgment Expression Expression Expression+ | EvComputed Int Expression Expression | EvBuilt Int Expression | EvAnswer Int Expression @@ -133,6 +142,8 @@ record (EvTerminate depth condition side raising) = EvTerminate depth (fmap datum condition) side raising record (EvMinted depth sym operands) = EvMinted depth (symbol sym) (map datum operands) record (EvDeferred depth sym judgment copy call site) = EvDeferred depth (symbol sym) judgment (term copy) (fmap term call) (term site)+ record (EvApplied depth judgment call object site) = EvApplied depth judgment (term call) (term object) (term site)+ record (EvComputed depth before after) = EvComputed depth (term before) (term after) record (EvBuilt depth value) = EvBuilt depth (term value) record (EvAnswer depth value) = EvAnswer depth (term value) record other = other@@ -145,41 +156,98 @@ datum :: Either Int Bytes -> Either Int Bytes datum = either (Left . symbol) Right -type Named = Map.Map Int [(Expression, T.Text)]+tier :: Evaluation -> Int+tier EvRun{} = 0+tier (EvFiring depth _ _ _) = depth+tier (EvFormation depth _ _) = depth+tier (EvLooped depth _ _ _ _ _) = depth+tier (EvStuck depth _ _ _) = depth+tier (EvStall depth _) = depth+tier (EvStuckOn depth _) = depth+tier (EvStarved depth _ _ _) = depth+tier (EvTimeout depth _ _ _) = depth+tier (EvSpent depth _ _ _) = depth+tier (EvData depth _ _ _) = depth+tier (EvTerm depth _ _ _) = depth+tier (EvSymbolize depth _ _ _) = depth+tier (EvKnown depth _ _) = depth+tier (EvJoin depth _ _ _) = depth+tier (EvJoined depth _ _) = depth+tier (EvTerminate depth _ _ _) = depth+tier (EvMinted depth _ _) = depth+tier (EvDeferred depth _ _ _ _ _) = depth+tier (EvApplied depth _ _ _ _) = depth+tier (EvComputed depth _ _) = depth+tier (EvBuilt depth _) = depth+tier (EvAnswer depth _) = depth -namedLookup :: Expression -> Named -> Maybe T.Text+type Named a = Map.Map Int [(Expression, a)]++namedLookup :: Expression -> Named a -> Maybe a namedLookup term names = lookup term (Map.findWithDefault [] (hashExpression term) names) -namedInsert :: Expression -> T.Text -> Named -> Named+namedInsert :: forall a. Expression -> a -> Named a -> Named a namedInsert term naming = Map.alter renamed (hashExpression term) where- renamed :: Maybe [(Expression, T.Text)] -> Maybe [(Expression, T.Text)]+ renamed :: Maybe [(Expression, a)] -> Maybe [(Expression, a)] renamed entries = Just ((term, naming) : filter ((/= term) . fst) (fromMaybe [] entries)) +namedCarry :: Expression -> Expression -> Named a -> Named a+namedCarry before after names = maybe names (\naming -> namedInsert after naming names) (namedLookup before names)++abbreviated :: Named Expression -> Expression -> Expression+abbreviated names term+ | Map.null names = term+ | otherwise = fromMaybe (abbreviatedInside names term) (namedLookup term names)++abbreviatedInside :: Named Expression -> Expression -> Expression+abbreviatedInside names (ExFormation bds) = ExFormation (map binding bds)+ where+ binding :: Binding -> Binding+ binding (BiTau attr expr) = BiTau attr (abbreviated names expr)+ binding bd = bd+abbreviatedInside names (ExApplication expr (ArTau attr arg)) = ExApplication (abbreviated names expr) (ArTau attr (abbreviated names arg))+abbreviatedInside names (ExApplication expr (ArAlpha alpha arg)) = ExApplication (abbreviated names expr) (ArAlpha alpha (abbreviated names arg))+abbreviatedInside names (ExDispatch expr attr) = ExDispatch (abbreviated names expr) attr+abbreviatedInside _ term = term+ data Protocol = Protocol { _fired :: Int- , _named :: Named- , _open :: Map.Map Int Int+ , _named :: Named T.Text+ , _open :: [(Int, Int)] , _begun :: Bool+ , _made :: Named Expression+ , _counted :: Map.Map Int Int+ , _built :: Map.Map Int Int } emptyProtocol :: Protocol-emptyProtocol = Protocol 0 Map.empty Map.empty False+emptyProtocol = Protocol 0 Map.empty [] False Map.empty Map.empty Map.empty data Nesting = Nesting { _fires :: Int- , _openedAt :: Map.Map Int Int+ , _openedAt :: [(Int, Int)] , _closing :: [(Int, String)]+ , _objects :: Named Expression+ , _numbered :: Map.Map Int Int } emptyNesting :: Nesting-emptyNesting = Nesting 0 Map.empty []+emptyNesting = Nesting 0 [] [] Map.empty Map.empty saveEval :: Handle -> IORef Protocol -> (Expression -> IO String) -> (Expression -> IO String) -> SaveEvalFunc-saveEval handle cursor render salted report = do- line <- atomicModify cursor (written report)+saveEval handle cursor printed printed' report = do+ line <- atomicModify cursor (written report . outer (tier report)) mapM_ saved line where+ render :: Expression -> IO String+ render term = do+ protocol <- readIORef cursor+ printed (abbreviated protocol._made term)+ salted :: Expression -> IO String+ salted term = do+ protocol <- readIORef cursor+ printed' (abbreviated protocol._made term) saved :: String -> IO () saved line = do hPutStrLn handle line@@ -192,7 +260,7 @@ pure ( protocol { _fired = firings- , _open = Map.insert depth firings protocol._open+ , _open = (depth, firings) : protocol._open } , Just (indented depth (printf "𝔼(%s) # %s(%s)" (T.unpack key) (letter judgment) locator)) )@@ -228,19 +296,19 @@ pure (protocol, Just (indented depth (printf "spent(%d) # %s(%s)" limit (letter judgment) locator))) written (EvData depth spelling operand value) protocol = do datum <- spelled value- line <- commented (printf "%s := %s" (labelled protocol depth spelling) datum) Dataization operand+ line <- commented (printf "%s := %s" (labelled protocol spelling) datum) Dataization operand pure (protocol, Just (indented depth line)) where spelled :: Either Int Bytes -> IO String spelled (Left symbol) = printf "𝔻(%s)" <$> render (standing symbol) spelled (Right bytes) = render (ExBytes bytes) written (EvTerm depth spelling operand term) protocol = do- let naming = labelled protocol depth spelling+ let naming = labelled protocol spelling (protocol', value) <- valued protocol naming term line <- commented (printf "%s := %s" naming value) Morphing operand pure (protocol', Just (indented depth line)) written (EvSymbolize depth spelling source term) protocol = do- let naming = labelled protocol depth spelling+ let naming = labelled protocol spelling (protocol', value) <- valued protocol naming term line <- commented' (printf "%s := %s" naming value) source pure (protocol', Just (indented depth line))@@ -249,7 +317,7 @@ value <- render (ExBytes bytes) pure (protocol, Just (indented depth (printf "𝔻(%s) == %s" form value))) written (EvJoin depth spelling (left, right) term) protocol = do- let naming = labelled protocol depth spelling+ let naming = labelled protocol spelling (protocol', value) <- valued protocol naming term pure (protocol', Just (indented depth (printf "%s := %s # [%s, %s]" naming value (T.unpack left) (T.unpack right)))) written (EvJoined depth fresh (one, two)) protocol = do@@ -266,19 +334,29 @@ spelled (Right bytes) = render (ExBytes bytes) written EvMinted{} protocol = pure (protocol, Nothing) written (EvDeferred depth symbol judgment copy call site) protocol = do- form <- render (fromMaybe copy call)+ form <- maybe (render copy) (printed . abbreviatedInside protocol._made) call locator <- render site pure (protocol, Just (indented depth (printf "deferred(%s) := %s # %s(%s)" (printFunction (FnSymbol symbol)) form (letter judgment) locator)))+ written (EvApplied depth judgment call object site) protocol = do+ let (index, counted) = numbered protocol+ aliased :: Expression+ aliased = alias (opener protocol) index+ form <- printed (abbreviatedInside protocol._made call)+ locator <- render site+ pure (counted{_made = namedInsert call aliased (namedInsert object aliased counted._made)}, Just (indented depth (printf "applied(%s.%d) := %s # %s(%s)" (labelled protocol answer) index form (letter judgment) locator)))+ written (EvComputed _ before after) protocol = pure (protocol{_made = namedCarry before after protocol._made}, Nothing) written (EvBuilt depth term) protocol = do+ let (index, counted) = numbered protocol value <- borrowed protocol term- pure (protocol, Just (indented depth (printf "%s.1 := %s # %s" (labelled protocol depth answer) value (T.unpack answer))))+ pure (counted{_built = Map.insert (opener protocol) index counted._built}, Just (indented depth (printf "%s.%d := %s # %s" (labelled protocol answer) index value (T.unpack answer)))) written (EvAnswer depth term) protocol = do- let stem :: String- stem = labelled protocol depth answer+ let (index, counted) = numbered protocol+ stem :: String+ stem = labelled protocol answer naming :: String- naming = printf "%s.2" stem- (protocol', value) <- valued protocol naming term- pure (protocol', Just (indented depth (printf "%s := %s # 𝕄(%s.1)" naming value stem)))+ naming = printf "%s.%d" stem index+ (protocol', value) <- valued counted naming term+ pure (protocol', Just (indented depth (printf "%s := %s # 𝕄(%s.%d)" naming value stem (Map.findWithDefault 1 (opener protocol) protocol._built)))) valued :: Protocol -> String -> Expression -> IO (Protocol, String) valued protocol naming term = case denoted term of Nothing -> (,) protocol <$> render term@@ -293,9 +371,17 @@ commented line judgment operand = printf "%s # %s(%s)" line (letter judgment) <$> salted operand commented' :: String -> Expression -> IO String commented' line source = printf "%s # %s" line <$> salted source- labelled :: Protocol -> Int -> T.Text -> String- labelled protocol depth spelling =- printf "%s.%d" (T.unpack spelling) (fromMaybe 0 (Map.lookup (depth - 1) protocol._open))+ outer :: Int -> Protocol -> Protocol+ outer depth protocol = protocol{_open = dropWhile ((>= depth) . fst) protocol._open}+ labelled :: Protocol -> T.Text -> String+ labelled protocol spelling = printf "%s.%d" (T.unpack spelling) (opener protocol)+ opener :: Protocol -> Int+ opener protocol = maybe 0 snd (listToMaybe protocol._open)+ numbered :: Protocol -> (Int, Protocol)+ numbered protocol = (index, protocol{_counted = Map.insert (opener protocol) index protocol._counted})+ where+ index :: Int+ index = maybe 1 (+ 1) (Map.lookup (opener protocol) protocol._counted) endEval :: Handle -> IORef Protocol -> Double -> IO () endEval handle cursor began = do@@ -314,11 +400,15 @@ perSecond firings taken = round (fromIntegral firings * 1000 / fromIntegral (max 1 taken) :: Double) saveEvalXml :: Handle -> IORef Nesting -> (Expression -> IO String) -> SaveEvalFunc-saveEvalXml handle cursor render report = do- written <- atomicModify cursor (elements report)+saveEvalXml handle cursor printed report = do+ written <- atomicModify cursor (elements report . outer (tier report)) mapM_ (hPutStrLn handle) written logDebug (printf "Saved %d line(s) of the XML protocol" (length written)) where+ render :: Expression -> IO String+ render term = do+ nesting <- readIORef cursor+ printed (abbreviated nesting._objects term) elements :: Evaluation -> Nesting -> IO (Nesting, [String]) elements (EvRun judgment locator) nesting = pure@@ -334,7 +424,7 @@ pure ( nesting { _fires = fires- , _openedAt = Map.insert depth fires nesting._openedAt+ , _openedAt = (depth, fires) : nesting._openedAt , _closing = (depth, "evaluate") : kept } , closers ++ [indentedXml depth (printf "<evaluate λ=\"%s\" by=\"%s\" at=\"%s\">" (quoted key) (opened judgment) (escapeXML locator))]@@ -387,18 +477,18 @@ stood :: Either Int Bytes -> IO String stood (Left symbol) = do form <- render (standing symbol)- pure (printf "<dataize meta=\"%s\">%s</dataize>" (escapeXML (labelled nesting depth spelling)) (escapeXMLText form))+ pure (printf "<dataize meta=\"%s\">%s</dataize>" (escapeXML (labelled nesting spelling)) (escapeXMLText form)) stood (Right bytes) = do form <- render (ExBytes bytes)- pure (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting depth spelling)) (escapeXMLText form))+ pure (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting spelling)) (escapeXMLText form)) elements (EvTerm depth spelling _ term) nesting = do body <- render term let (kept, closers) = closed depth nesting._closing- pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting depth spelling)) (escapeXMLText body))])+ pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting spelling)) (escapeXMLText body))]) elements (EvSymbolize depth spelling _ term) nesting = do body <- render term let (kept, closers) = closed depth nesting._closing- pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting depth spelling)) (escapeXMLText body))])+ pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting spelling)) (escapeXMLText body))]) elements (EvKnown depth symbol bytes) nesting = do value <- render (ExBytes bytes) let (kept, closers) = closed depth nesting._closing@@ -406,7 +496,7 @@ elements (EvJoin depth spelling _ term) nesting = do body <- render term let (kept, closers) = closed depth nesting._closing- pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting depth spelling)) (escapeXMLText body))])+ pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<bind meta=\"%s\">%s</bind>" (escapeXML (labelled nesting spelling)) (escapeXMLText body))]) elements (EvJoined depth fresh (one, two)) nesting = pure (nesting{_closing = kept}, closers ++ [indentedXml depth joint]) where@@ -438,21 +528,42 @@ (origin, given) <- maybe (pure ("", "")) called call let (kept, closers) = closed depth nesting._closing pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<deferred symbol=\"%s\" by=\"%s\" at=\"%s\"%s>%s<e>%s</e></deferred>" (sigma symbol) (opened judgment) (escapeXML locator) origin given (escapeXMLText form))])+ elements (EvApplied depth judgment call object site) nesting = do+ (origin, given) <- parted (abbreviatedInside nesting._objects call)+ locator <- render site+ let (index, counted) = numbered nesting+ (kept, closers) = closed depth nesting._closing+ naming :: String+ naming = printf "%s.%d" (labelled nesting answer) index+ aliased :: Expression+ aliased = alias (opener nesting) index+ pure (counted{_closing = kept, _objects = namedInsert call aliased (namedInsert object aliased counted._objects)}, closers ++ [indentedXml depth (printf "<applied meta=\"%s\" by=\"%s\" at=\"%s\" of=\"%s\">%s</applied>" (escapeXML naming) (opened judgment) (escapeXML locator) (escapeXML origin) given)])+ elements (EvComputed _ before after) nesting = pure (nesting{_objects = namedCarry before after nesting._objects}, []) elements (EvBuilt depth term) nesting = do body <- render term- let (kept, closers) = closed depth nesting._closing+ let (index, counted) = numbered nesting+ (kept, closers) = closed depth nesting._closing naming :: String- naming = printf "%s.1" (labelled nesting depth answer)- pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<built meta=\"%s\">%s</built>" (escapeXML naming) (escapeXMLText body))])+ naming = printf "%s.%d" (labelled nesting answer) index+ pure (counted{_closing = kept}, closers ++ [indentedXml depth (printf "<built meta=\"%s\">%s</built>" (escapeXML naming) (escapeXMLText body))]) elements (EvAnswer depth term) nesting = do body <- render term- let (kept, closers) = closed depth nesting._closing+ let (index, counted) = numbered nesting+ (kept, closers) = closed depth nesting._closing naming :: String- naming = printf "%s.2" (labelled nesting depth answer)- pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "<answer meta=\"%s\">%s</answer>" (escapeXML naming) (escapeXMLText body))])- labelled :: Nesting -> Int -> T.Text -> String- labelled nesting depth spelling =- printf "%s.%d" (T.unpack spelling) (fromMaybe 0 (Map.lookup (depth - 1) nesting._openedAt))+ naming = printf "%s.%d" (labelled nesting answer) index+ pure (counted{_closing = kept}, closers ++ [indentedXml depth (printf "<answer meta=\"%s\">%s</answer>" (escapeXML naming) (escapeXMLText body))])+ outer :: Int -> Nesting -> Nesting+ outer depth nesting = nesting{_openedAt = dropWhile ((>= depth) . fst) nesting._openedAt}+ labelled :: Nesting -> T.Text -> String+ labelled nesting spelling = printf "%s.%d" (T.unpack spelling) (opener nesting)+ opener :: Nesting -> Int+ opener nesting = maybe 0 snd (listToMaybe nesting._openedAt)+ numbered :: Nesting -> (Int, Nesting)+ numbered nesting = (index, nesting{_numbered = Map.insert (opener nesting) index nesting._numbered})+ where+ index :: Int+ index = maybe 1 (+ 1) (Map.lookup (opener nesting) nesting._numbered) called :: Expression -> IO (String, String) called term = do let (object, arguments) = invoked term@@ -468,6 +579,15 @@ valued (ExFormation bds) = maybe "?" valued (listToMaybe [body | BiTau AtPhi body <- bds]) valued (ExApplication _ (ArTau AtPhi body)) = valued body valued _ = "?"+ parted :: Expression -> IO (String, String)+ parted (ExApplication term (ArTau attr value)) = do+ origin <- printed term+ given <- argued value+ pure (origin, printf "<attr name=\"%s\">%s</attr>" (escapeXML (printAttribute attr)) (escapeXMLText given))+ parted term = (,"") <$> printed term+ argued :: Expression -> IO String+ argued (ExFormation [BiLambda (FnSymbol idx)]) = pure (sigma idx)+ argued term = printed term sigma :: Int -> String sigma = printFunction . FnSymbol quoted :: T.Text -> String@@ -505,6 +625,9 @@ answer :: T.Text answer = "𝑛"++alias :: Int -> Int -> Expression+alias firing index = ExMeta (T.pack (printf "n.%d.%d" firing index)) dontSaveEval :: SaveEvalFunc dontSaveEval _ = pure ()
src/LaTeX.hs view
@@ -155,7 +155,15 @@ ( \idx comment (item, rule) reached -> let item' = toLatex (baseTab idx) item opening = if idx == 0 then item' else printf " %s %s" (relation reached) item'- in comment ++ maybe opening (\(judgment, name) -> printf "%s %s[\\nameref{r:%s}]" opening (relation judgment) (escaped name)) rule+ in comment+ ++ maybe+ opening+ ( \(judgment, name) ->+ if judgment == Contextualization+ then printf "%s %s" opening (relation judgment)+ else printf "%s %s[\\nameref{r:%s}]" opening (relation judgment) (escaped name)+ )+ rule ) [0 ..] comments
src/Morph.hs view
@@ -14,7 +14,7 @@ module Morph (Answer, Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, FiringFunc, Memo (..), ReductionFunc, Morphed, Refused (..), Steps (..), Tally (..), admitted, boxed, charged, counted, deeper, emptyState, enter, entering, execBuildTerm, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, parking, recalled, refused, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where import AST-import Builder (buildExpressionThrows, pathOf)+import Builder (buildExpressionThrows, nameIn, pathOf) import Control.Applicative ((<|>)) import Control.Exception (Exception, SomeException, catch, evaluate, throwIO, try) import Control.Monad (unless, when)@@ -431,6 +431,7 @@ case outcome of Left (Severed answer reached) -> pure (answer, reached) Right (walked, walkedState) -> do+ when (walked /= term) (here._saveEval (EvComputed here._nesting term walked)) placed <- ctx._engine._contextualize walked =<< context frame current <- readIORef world (answer, answered) <- ctx'._fire dispatched placed current walkedState ctx'{_universe = Just current} `catch` cut standing frame ctx'@@ -738,7 +739,10 @@ where rewriteContext :: ReduceContext -> RewriteContext rewriteContext ReduceContext{..} =- RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing _saveStep+ RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing _saveStep (\redex object -> _saveEval (EvApplied _nesting _judgment (called _universe redex) object _site))+ called :: Maybe Expression -> Expression -> Expression+ called universe (ExApplication head' arg) = ExApplication (nameIn universe head') arg+ called _ redex = redex universed :: Expression -> ReduceContext -> IO ReduceContext universed _ ctx@ReduceContext{_universe = Just _} = pure ctx
src/Rewriter.hs view
@@ -75,6 +75,7 @@ , _must :: Must , _breakpoint :: Maybe String , _saveStep :: SaveStepFunc+ , _saveMade :: SaveMadeFunc } data RewriteException@@ -109,13 +110,13 @@ rul expr -buildAndReplace' :: ToReplace -> ReplaceExpressionFunc -> IO Expression+buildAndReplace' :: ToReplace -> ReplaceExpressionFunc -> IO (Expression, [(Expression, Expression)]) buildAndReplace' (expr, ptn, res, substs) func = do ptns <- buildExpressionsThrows ptn substs repls <- buildExpressionsThrows res substs- pure (func (expr, ptns, map const repls))+ pure (func (expr, ptns, map const repls), zip ptns repls) -tryBuildAndReplaceFast :: ToReplace -> IO Expression+tryBuildAndReplaceFast :: ToReplace -> IO (Expression, [(Expression, Expression)]) tryBuildAndReplaceFast state@(expr, ptn@(ExFormation (_ : pbds)), res@(ExFormation (_ : rbds)), substs) | fast ptn res = do logDebug "Applying fast replacing since 'pattern' and 'result' are suitable for this..."@@ -152,7 +153,7 @@ interpreted :: Y.Rule -> Step interpreted rule = Step rule.name applied where- applied :: RuleContext -> Expression -> IO (Maybe Expression)+ applied :: RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)])) applied ctx expr = R.matchExpressionWithRule expr rule ctx >>= \case [] -> pure Nothing@@ -163,10 +164,10 @@ direct :: String -> Bool -> (Maybe Expression -> Expression -> [Expression]) -> Step direct name redex rewritten = Step name applied where- applied :: RuleContext -> Expression -> IO (Maybe Expression)+ applied :: RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)])) applied (RuleContext _ universe _) expr = pure $ case sites redex (rewritten universe) expr of [] -> Nothing- found -> Just (replaceExpression (expr, map fst found, map (const . snd) found))+ found -> Just (replaceExpression (expr, map fst found, map (const . snd) found), found) every :: [Step] -> Maybe Expression -> Expression -> Set Int every steps _ _ = Set.fromList (zipWith const [0 ..] steps)@@ -205,7 +206,7 @@ logDebug (printf "Rule '%s' is a breakpoint, dropping down all the previous rewritings..." ruleName) pure (_rewrittens, expression, _unique, True, _found) else pure (_rewrittens, expression, _unique, False, _found)- Just expr -> do+ Just (expr, rewritten) -> do logDebug (printf "Rule '%s' has been matched and applied" ruleName) if expression == expr then do@@ -226,6 +227,7 @@ ) updated <- withLocatedExpression _locator expr current _saveStep updated+ mapM_ (uncurry _saveMade) [(redex, object) | (redex@(ExApplication head' (ArTau attr _)), object@(ExFormation _)) <- rewritten, attr /= AtRho, object /= head'] _rewrite (leadsTo updated, expr, seenInsert digest expr _unique, False, Nothing) (_count + 1) where leadsTo :: Expression -> NonEmpty Rewritten@@ -237,7 +239,7 @@ applicable _ [] _ = pure False applicable expression (rule : rest) ctx@RewriteContext{..} = _applied rule (RuleContext _buildTerm _universe _normal) expression >>= \case- Just changed | changed /= expression -> pure True+ Just (changed, _) | changed /= expression -> pure True _ -> applicable expression rest ctx rewrite :: Expression -> [Step] -> RewriteContext -> IO Rewrittens
src/Rule.hs view
@@ -45,7 +45,7 @@ data Step = Step { _name :: String- , _applied :: RuleContext -> Expression -> IO (Maybe Expression)+ , _applied :: RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)])) } matchesAnyNormalizationRule :: Expression -> RuleContext -> Bool
test/CLISpec.hs view
@@ -1271,8 +1271,10 @@ records <- readProtocol path lines records `shouldBe` [ "𝔻(Φ.t)"- , " formation(⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧) # 𝔻(Φ.t)"- , " looped(⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧) # 𝔻(Φ.t), proven"+ , " applied(𝑛.0.1) := Φ.cyc( x ↦ ⟦⟧ ) # 𝕄(Φ.t)"+ , " formation(𝑛.0.1) # 𝔻(Φ.t)"+ , " applied(𝑛.0.2) := Φ.cyc( x ↦ ⟦⟧ ) # 𝕄(Φ.t)"+ , " looped(𝑛.0.2) # 𝔻(Φ.t), proven" ] it "writes the cut to the XML protocol with the formation in an element of its own" $@@ -1286,8 +1288,10 @@ lines records `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<dataize at=\"Φ.t\">"- , " <formation at=\"Φ.t\" term=\"⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧\">"- , " <looped by=\"dataize\" match=\"proven\" at=\"Φ.t\"><e>⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧</e></looped>"+ , " <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ.t\" of=\"Φ.cyc\"><attr name=\"x\">⟦⟧</attr></applied>"+ , " <formation at=\"Φ.t\" term=\"𝑛.0.1\">"+ , " <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ.t\" of=\"Φ.cyc\"><attr name=\"x\">⟦⟧</attr></applied>"+ , " <looped by=\"dataize\" match=\"proven\" at=\"Φ.t\"><e>𝑛.0.2</e></looped>" , " </formation>" , "</dataize>" ]@@ -1300,7 +1304,7 @@ ["dataize", "--locator=Q.t", "--acyclic=plausible", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"] [] records <- readProtocol path- lines records `shouldContain` [" looped(⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧) # 𝔻(Φ.t), plausible"]+ lines records `shouldContain` [" looped(𝑛.0.2) # 𝔻(Φ.t), plausible"] it "refuses the flag without a mode" $ withStdin "⟦ t ↦ ⟦ Δ ⤍ 01-02 ⟧ ⟧" $@@ -1321,7 +1325,7 @@ [ intercalate "\n" [ "\\begin{phiquation}"- , "[[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ \\phiContextualize[\\nameref{r:contextualize}]"+ , "[[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ \\phiContextualize" , " \\phiContextualize [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| \\phiNormalize[\\nameref{r:copy}]" , " \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] : |x| . |x| \\phiNormalize[\\nameref{r:dot}]" , " \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ D> |01-|, |y| -> [[]] ]] : |x| ) \\phiNormalize[\\nameref{r:skip}]"@@ -1354,7 +1358,7 @@ withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus -> [[ ^ -> ?, x -> ?, L> L_number_plus ]] ]] ]]" $ testCLISucceeded ["dataize", symbolic, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]- ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\phiContextualize[\\nameref{r:contextualize}]"]+ ["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\phiContextualize"] it "compresses a canonized whole-expression sequence into a meet" $ withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus -> [[ ^ -> ?, x -> ?, L> L_number_plus ]] ]] ]]" $@@ -1504,16 +1508,23 @@ lines records `shouldBe` [ "𝔻(Φ)" , " formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6 ) ⟧) # 𝔻(Φ)"+ , " applied(𝑛.0.1) := 5 # 𝕄(Φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6 ) # 𝕄(Φ)" , " 𝔼(L_number_plus) # 𝔻(Φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵0)"- , " formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵0)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵1)"- , " formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.3) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.4) # 𝔻(Φ.a🌵1)" , " 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧ # 𝕄(𝑛.1.1)"- , " formation(⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)"+ , " formation(𝑛.1.6) # 𝔻(Φ)" ] it "numbers the firings of one entry apart and names the symbol between them" $@@ -1525,24 +1536,36 @@ lines records `shouldBe` [ "𝔻(Φ)" , " formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6 ).plus( 7 ) ⟧) # 𝔻(Φ)"+ , " applied(𝑛.0.1) := 5 # 𝕄(Φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6 ) # 𝕄(Φ)" , " 𝔼(L_number_plus) # 𝕄(Φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵0)"- , " formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵0)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵1)"- , " formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.3) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.4) # 𝔻(Φ.a🌵1)" , " 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧ # 𝕄(𝑛.1.1)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)"+ , " applied(𝑛.0.3) := 𝑛.1.6.plus( x ↦ 7 ) # 𝕄(Φ)" , " 𝔼(L_number_plus) # 𝔻(Φ)"- , " formation(⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵2)"+ , " applied(𝑛.2.1) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ.a🌵2)"+ , " formation(𝑛.2.1) # 𝔻(Φ.a🌵2)" , " 𝛿1.2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵3)"- , " formation(40-1C-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵3)"+ , " applied(𝑛.2.2) := 7 # 𝕄(Φ.a🌵3)"+ , " formation(𝑛.2.2) # 𝔻(Φ.a🌵3)"+ , " applied(𝑛.2.3) := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵3)"+ , " formation(𝑛.2.3) # 𝔻(Φ.a🌵3)" , " 𝛿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)"- , " formation(⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ)"+ , " 𝑛.2.4 := Φ.number( φ ↦ 𝜎2:λ ) # 𝑛"+ , " applied(𝑛.2.5) := Φ.number( φ ↦ 𝜎2:λ ) # 𝕄(Φ)"+ , " 𝑛.2.6 := 𝑛.2.5 # 𝕄(𝑛.2.4)"+ , " formation(𝑛.2.5) # 𝔻(Φ)" ] it "numbers the firings of different entries apart" $@@ -1554,24 +1577,36 @@ lines records `shouldBe` [ "𝔻(Φ)" , " formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ ⟧, φ ↦ 5.plus( 6 ).times( 7 ) ⟧) # 𝔻(Φ)"+ , " applied(𝑛.0.1) := 5 # 𝕄(Φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6 ) # 𝕄(Φ)" , " 𝔼(L_number_plus) # 𝕄(Φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ ⟧) # 𝔻(Φ.a🌵0)"- , " formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵0)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ ⟧) # 𝔻(Φ.a🌵1)"- , " formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.3) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.4) # 𝔻(Φ.a🌵1)" , " 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ ⟧ # 𝕄(𝑛.1.1)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)"+ , " applied(𝑛.0.3) := 𝑛.1.6.times( x ↦ 7 ) # 𝕄(Φ)" , " 𝔼(L_number_times) # 𝔻(Φ)"- , " formation(⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ ⟧) # 𝔻(Φ.a🌵2)"+ , " applied(𝑛.2.1) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ.a🌵2)"+ , " formation(𝑛.2.1) # 𝔻(Φ.a🌵2)" , " 𝛿1.2 := 𝔻(𝜎1:λ) # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ ⟧) # 𝔻(Φ.a🌵3)"- , " formation(40-1C-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵3)"+ , " applied(𝑛.2.2) := 7 # 𝕄(Φ.a🌵3)"+ , " formation(𝑛.2.2) # 𝔻(Φ.a🌵3)"+ , " applied(𝑛.2.3) := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵3)"+ , " formation(𝑛.2.3) # 𝔻(Φ.a🌵3)" , " 𝛿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)"- , " formation(⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ, times(x) ↦ L_number_times:λ ⟧) # 𝔻(Φ)"+ , " 𝑛.2.4 := Φ.number( φ ↦ 𝜎2:λ ) # 𝑛"+ , " applied(𝑛.2.5) := Φ.number( φ ↦ 𝜎2:λ ) # 𝕄(Φ)"+ , " 𝑛.2.6 := 𝑛.2.5 # 𝕄(𝑛.2.4)"+ , " formation(𝑛.2.5) # 𝔻(Φ)" ] it "nests the firing an operand of another firing brought down" $@@ -1583,24 +1618,36 @@ lines records `shouldBe` [ "𝔻(Φ)" , " formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6.plus( 7 ) ) ⟧) # 𝔻(Φ)"+ , " applied(𝑛.0.1) := 5 # 𝕄(Φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6.plus( 7 ) ) # 𝕄(Φ)" , " 𝔼(L_number_plus) # 𝔻(Φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵0)"- , " formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵0)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)"+ , " applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)"+ , " applied(𝑛.1.4) := 𝑛.1.3.plus( x ↦ 7 ) # 𝕄(Φ.a🌵1)" , " 𝔼(L_number_plus) # 𝔻(Φ.a🌵1)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵2)"- , " formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵2)"+ , " applied(𝑛.2.1) := 6 # 𝕄(Φ.a🌵2)"+ , " formation(𝑛.2.1) # 𝔻(Φ.a🌵2)"+ , " applied(𝑛.2.2) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵2)"+ , " formation(𝑛.2.2) # 𝔻(Φ.a🌵2)" , " 𝛿1.2 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵3)"- , " formation(40-1C-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵3)"+ , " applied(𝑛.2.3) := 7 # 𝕄(Φ.a🌵3)"+ , " formation(𝑛.2.3) # 𝔻(Φ.a🌵3)"+ , " applied(𝑛.2.4) := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵3)"+ , " formation(𝑛.2.4) # 𝔻(Φ.a🌵3)" , " 𝛿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)"- , " formation(⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵1)"+ , " 𝑛.2.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.2.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ.a🌵1)"+ , " 𝑛.2.7 := 𝑛.2.6 # 𝕄(𝑛.2.5)"+ , " formation(𝑛.2.6) # 𝔻(Φ.a🌵1)" , " 𝛿2.1 := 𝔻(𝜎1:λ) # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎2:λ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧ # 𝕄(𝑛.1.1)"- , " formation(⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎2:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎2:λ ) # 𝕄(Φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)"+ , " formation(𝑛.1.6) # 𝔻(Φ)" ] it "writes what is known about every symbol a 'symbolize' line minted" $@@ -1634,7 +1681,7 @@ withStdin "⟦ wrap(v) ↦ ⟦⟧, y ↦ Φ.wrap( v ↦ ⟦ b(x) ↦ ⟦ φ ↦ x.next ⟧ ⟧ ).v.b( x ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ⟧" $ testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" deferred(𝜎2) := ⟦ x ↦ 𝜎1:λ, φ ↦ x.next ⟧ # 𝕄(Φ.y)"]+ lines records `shouldContain` [" applied(𝑛.0.2) := ⟦ x ↦ ∅, φ ↦ x.next ⟧( x ↦ 𝜎1:λ ) # 𝕄(Φ.y)", " deferred(𝜎2) := 𝑛.0.2 # 𝕄(Φ.y)"] it "writes the symbol a cut answers a copy with" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do@@ -1643,7 +1690,7 @@ withStdin "⟦ box(n) ↦ ⟦ φ ↦ Φ.loop( x ↦ Φ.box( n ↦ ξ.n ) ) ⟧, loop(x) ↦ L_loop:λ, y ↦ Φ.loop( x ↦ Φ.box( n ↦ ⟦ Δ ⤍ 01- ⟧ ) ) ⟧" $ testCLISucceeded ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=proven", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" looped(⟦ x ↦ Φ.box( n ↦ 01-:Δ ), λ ⤍ L_loop ⟧) := 𝜎1 # 𝕄(Φ.a🌵0.φ), proven"]+ lines records `shouldContain` [" applied(𝑛.1.3) := Φ.loop( x ↦ 𝑛.1.2 ) # 𝕄(Φ.a🌵0.φ)", " looped(𝑛.1.3) := 𝜎1 # 𝕄(Φ.a🌵0.φ), proven"] it "writes a told stall to the XML protocol" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do@@ -1696,15 +1743,22 @@ lines records `shouldBe` [ "𝔻(Φ)" , " formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧, φ ↦ 5.plus( 6 ).nope ⟧) # 𝔻(Φ)"+ , " applied(𝑛.0.1) := 5 # 𝕄(Φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6 ) # 𝕄(Φ)" , " 𝔼(L_number_plus) # 𝕄(Φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵0)"- , " formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵0)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵1)"- , " formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.3) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.4) # 𝔻(Φ.a🌵1)" , " 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ, nope ↦ L_number_nope:λ ⟧ # 𝕄(𝑛.1.1)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)" , " unanswered(L_number_nope) # 𝔻(L_number_nope:λ)" ] @@ -1721,7 +1775,7 @@ withStdin sum' $ testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--output=xmir", "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- records `shouldEndWith` " formation(⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ)\n"+ records `shouldEndWith` " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)\n 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)\n formation(𝑛.1.6) # 𝔻(Φ)\n" describe "as XML" $ do it "writes the document when the file is named .xml" $@@ -1734,22 +1788,29 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<dataize at=\"Φ\">" , " <formation at=\"Φ\" term=\"⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6 ) ⟧\">"+ , " <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ\" of=\"𝑛.0.1.plus\"><attr name=\"x\">6</attr></applied>" , " <evaluate λ=\"L_number_plus\" by=\"dataize\" at=\"Φ\">"- , " <formation at=\"Φ.a🌵0\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵0\" term=\"40-14-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.1.1\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.1\">"+ , " <applied meta=\"𝑛.1.2\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.bytes\"><attr name=\"φ\">40-14-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.2\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿1.1\">40-14-00-00-00-00-00-00</bind>"- , " <formation at=\"Φ.a🌵1\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵1\" term=\"40-18-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.1.3\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.3\">"+ , " <applied meta=\"𝑛.1.4\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.bytes\"><attr name=\"φ\">40-18-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.4\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿2.1\">40-18-00-00-00-00-00-00</bind>" , " <minted symbol=\"𝜎1\">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>"- , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧</answer>"+ , " <built meta=\"𝑛.1.5\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <applied meta=\"𝑛.1.6\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">𝜎1</attr></applied>"+ , " <answer meta=\"𝑛.1.7\">𝑛.1.6</answer>" , " </evaluate>"- , " <formation at=\"Φ\" term=\"⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧\">"+ , " <formation at=\"Φ\" term=\"𝑛.1.6\">" , " </formation>" , " </formation>" , "</dataize>"@@ -1798,7 +1859,7 @@ withStdin sum' $ testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records+ filter (not . isInfixOf "<applied ") (lines records) `shouldContain` [ " <formation at=\"Φ\" term=\"⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6 ) ⟧\">" , " <evaluate λ=\"L_number_plus\" by=\"dataize\" at=\"Φ\">" ]@@ -1825,35 +1886,47 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<dataize at=\"Φ\">" , " <formation at=\"Φ\" term=\"⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6 ).plus( 7 ) ⟧\">"+ , " <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ\" of=\"𝑛.0.1.plus\"><attr name=\"x\">6</attr></applied>" , " <evaluate λ=\"L_number_plus\" by=\"morph\" at=\"Φ\">"- , " <formation at=\"Φ.a🌵0\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵0\" term=\"40-14-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.1.1\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.1\">"+ , " <applied meta=\"𝑛.1.2\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.bytes\"><attr name=\"φ\">40-14-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.2\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿1.1\">40-14-00-00-00-00-00-00</bind>"- , " <formation at=\"Φ.a🌵1\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵1\" term=\"40-18-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.1.3\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.3\">"+ , " <applied meta=\"𝑛.1.4\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.bytes\"><attr name=\"φ\">40-18-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.4\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿2.1\">40-18-00-00-00-00-00-00</bind>" , " <minted symbol=\"𝜎1\">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>"- , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧</answer>"+ , " <built meta=\"𝑛.1.5\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <applied meta=\"𝑛.1.6\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">𝜎1</attr></applied>"+ , " <answer meta=\"𝑛.1.7\">𝑛.1.6</answer>" , " </evaluate>"+ , " <applied meta=\"𝑛.0.3\" by=\"morph\" at=\"Φ\" of=\"𝑛.1.6.plus\"><attr name=\"x\">7</attr></applied>" , " <evaluate λ=\"L_number_plus\" by=\"dataize\" at=\"Φ\">"- , " <formation at=\"Φ.a🌵2\" term=\"⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧\">"+ , " <applied meta=\"𝑛.2.1\" by=\"morph\" at=\"Φ.a🌵2\" of=\"Φ.number\"><attr name=\"φ\">𝜎1</attr></applied>"+ , " <formation at=\"Φ.a🌵2\" term=\"𝑛.2.1\">" , " </formation>" , " <dataize meta=\"𝛿1.2\">𝜎1:λ</dataize>"- , " <formation at=\"Φ.a🌵3\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵3\" term=\"40-1C-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.2.2\" by=\"morph\" at=\"Φ.a🌵3\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵3\" term=\"𝑛.2.2\">"+ , " <applied meta=\"𝑛.2.3\" by=\"morph\" at=\"Φ.a🌵3\" of=\"Φ.bytes\"><attr name=\"φ\">40-1C-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵3\" term=\"𝑛.2.3\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿2.2\">40-1C-00-00-00-00-00-00</bind>" , " <minted symbol=\"𝜎2\">𝜎1 40-1C-00-00-00-00-00-00</minted>"- , " <built meta=\"𝑛.2.1\">Φ.number( φ ↦ 𝜎2:λ )</built>"- , " <answer meta=\"𝑛.2.2\">⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧</answer>"+ , " <built meta=\"𝑛.2.4\">Φ.number( φ ↦ 𝜎2:λ )</built>"+ , " <applied meta=\"𝑛.2.5\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">𝜎2</attr></applied>"+ , " <answer meta=\"𝑛.2.6\">𝑛.2.5</answer>" , " </evaluate>"- , " <formation at=\"Φ\" term=\"⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧\">"+ , " <formation at=\"Φ\" term=\"𝑛.2.5\">" , " </formation>" , " </formation>" , "</dataize>"@@ -1951,7 +2024,8 @@ lines records `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<morph at=\"Φ.y\">"- , " <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.box\"><with><attr name=\"x\">𝜎1</attr></with><e>⟦ x ↦ 𝜎1:λ, φ ↦ x.next ⟧</e></deferred>"+ , " <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ.y\" of=\"Φ.box\"><attr name=\"x\">𝜎1</attr></applied>"+ , " <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.box\"><with><attr name=\"x\">𝜎1</attr></with><e>𝑛.0.1</e></deferred>" , "</morph>" ] @@ -1961,7 +2035,7 @@ withStdin "⟦ joined(items) ↦ ⟦ φ ↦ step( tup ↦ items ), step(ρ, tup) ↦ ⟦ φ ↦ tup.next ⟧ ⟧, y ↦ Φ.joined( items ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).φ ⟧" $ testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.joined.step\"><with><attr name=\"tup\">𝜎1</attr></with><e>⟦ tup ↦ 𝜎1:λ, φ ↦ tup.next ⟧</e></deferred>"]+ lines records `shouldContain` [" <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.joined.step\"><with><attr name=\"tup\">𝜎1</attr></with><e>𝑛.0.2</e></deferred>"] it "names the object a deferred copy was made of after the walk wrote an answer into its ρ" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do@@ -1970,7 +2044,7 @@ withStdin "⟦ bytes(φ) ↦ ⟦⟧, dataized(target) ↦ L_dataized:λ, joined(items) ↦ ⟦ φ ↦ step( tup ↦ items, s ↦ sep ), sep ↦ Φ.dataized( target ↦ items ), step(ρ, tup, s) ↦ ⟦ φ ↦ tup.next ⟧ ⟧, y ↦ Φ.joined( items ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).φ ⟧" $ testCLISucceeded ["morph", "--deep", "--symbolic=" ++ dataized, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" <deferred symbol=\"𝜎3\" by=\"morph\" at=\"Φ.y\" of=\"Φ.joined.step\"><with><attr name=\"tup\">𝜎1</attr><attr name=\"s\">𝜎2</attr></with><e>⟦ tup ↦ 𝜎1:λ, s ↦ 𝜎2:λ:φ, φ ↦ tup.next ⟧</e></deferred>"]+ lines records `shouldContain` [" <deferred symbol=\"𝜎3\" by=\"morph\" at=\"Φ.y\" of=\"Φ.joined.step\"><with><attr name=\"tup\">𝜎1</attr><attr name=\"s\">𝜎2</attr></with><e>𝑛.0.4</e></deferred>"] it "writes a question mark for an argument of a deferred copy that is no bare symbol" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do@@ -1978,7 +2052,7 @@ withStdin "⟦ box(x, w) ↦ ⟦ φ ↦ x.next ⟧, y ↦ Φ.box( x ↦ ⟦ λ ⤍ 𝜎1 ⟧, w ↦ ⟦ z ↦ Φ ⟧ ) ⟧" $ testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.box\"><with><attr name=\"x\">𝜎1</attr><attr name=\"w\">?</attr></with><e>⟦ x ↦ 𝜎1:λ, w ↦ Φ:z, φ ↦ x.next ⟧</e></deferred>"]+ lines records `shouldContain` [" <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.box\"><with><attr name=\"x\">𝜎1</attr><attr name=\"w\">?</attr></with><e>𝑛.0.2</e></deferred>"] it "writes the object a deferred copy was made of whatever --abridged says" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do@@ -1986,7 +2060,7 @@ withStdin "⟦ joined(items) ↦ ⟦ φ ↦ step( tup ↦ items ), step(ρ, tup) ↦ ⟦ φ ↦ tup.next ⟧ ⟧, y ↦ Φ.joined( items ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).φ ⟧" $ testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--abridged=20", "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.joined.step\"><with><attr name=\"tup\">𝜎1</attr></with><e>⟦ φ ↦ tup.next, +1 ⟧</e></deferred>"]+ lines records `shouldContain` [" <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\" of=\"Φ.joined.step\"><with><attr name=\"tup\">𝜎1</attr></with><e>𝑛.0.2</e></deferred>"] it "writes no object for a deferred copy of a formation the world does not declare" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do@@ -1994,7 +2068,7 @@ withStdin "⟦ wrap(v) ↦ ⟦⟧, y ↦ Φ.wrap( v ↦ ⟦ b(x) ↦ ⟦ φ ↦ x.next ⟧ ⟧ ).v.b( x ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ⟧" $ testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\"><e>⟦ x ↦ 𝜎1:λ, φ ↦ x.next ⟧</e></deferred>"]+ lines records `shouldContain` [" <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ.y\" of=\"⟦ x ↦ ∅, φ ↦ x.next ⟧\"><attr name=\"x\">𝜎1</attr></applied>", " <deferred symbol=\"𝜎2\" by=\"morph\" at=\"Φ.y\"><e>𝑛.0.2</e></deferred>"] it "writes the copy a cut answers as a call of the object it was made of" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do@@ -2003,7 +2077,7 @@ withStdin "⟦ num(φ) ↦ ⟦⟧, box(n) ↦ ⟦ φ ↦ Φ.loop( x ↦ Φ.box( n ↦ ξ.n ) ) ⟧, loop(x) ↦ L_loop:λ, y ↦ Φ.loop( x ↦ Φ.box( n ↦ Φ.num( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) ) ) ⟧" $ testCLISucceeded ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=plausible", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path- lines records `shouldContain` [" <looped symbol=\"𝜎2\" by=\"morph\" match=\"plausible\" at=\"Φ.a🌵0.φ\" of=\"Φ.box\"><with><attr name=\"n\">𝜎1</attr></with><e>⟦ x ↦ Φ.box( n ↦ Φ.num( φ ↦ 𝜎1:λ ) ), λ ⤍ L_loop ⟧</e></looped>"]+ lines records `shouldContain` [" <looped symbol=\"𝜎2\" by=\"morph\" match=\"plausible\" at=\"Φ.a🌵0.φ\" of=\"Φ.box\"><with><attr name=\"n\">𝜎1</attr></with><e>𝑛.0.1</e></looped>"] it "writes no 'minted' element for a firing minting nothing" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do@@ -2033,35 +2107,47 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<dataize at=\"Φ\">" , " <formation at=\"Φ\" term=\"⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(x) ↦ L_number_plus:λ ⟧, φ ↦ 5.plus( 6.plus( 7 ) ) ⟧\">"+ , " <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ\" of=\"𝑛.0.1.plus\"><attr name=\"x\">6.plus( 7 )</attr></applied>" , " <evaluate λ=\"L_number_plus\" by=\"dataize\" at=\"Φ\">"- , " <formation at=\"Φ.a🌵0\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵0\" term=\"40-14-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.1.1\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.1\">"+ , " <applied meta=\"𝑛.1.2\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.bytes\"><attr name=\"φ\">40-14-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.2\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿1.1\">40-14-00-00-00-00-00-00</bind>"+ , " <applied meta=\"𝑛.1.3\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <applied meta=\"𝑛.1.4\" by=\"morph\" at=\"Φ.a🌵1\" of=\"𝑛.1.3.plus\"><attr name=\"x\">7</attr></applied>" , " <evaluate λ=\"L_number_plus\" by=\"dataize\" at=\"Φ.a🌵1\">"- , " <formation at=\"Φ.a🌵2\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵2\" term=\"40-18-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.2.1\" by=\"morph\" at=\"Φ.a🌵2\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵2\" term=\"𝑛.2.1\">"+ , " <applied meta=\"𝑛.2.2\" by=\"morph\" at=\"Φ.a🌵2\" of=\"Φ.bytes\"><attr name=\"φ\">40-18-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵2\" term=\"𝑛.2.2\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿1.2\">40-18-00-00-00-00-00-00</bind>"- , " <formation at=\"Φ.a🌵3\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧\">"- , " <formation at=\"Φ.a🌵3\" term=\"40-1C-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.2.3\" by=\"morph\" at=\"Φ.a🌵3\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵3\" term=\"𝑛.2.3\">"+ , " <applied meta=\"𝑛.2.4\" by=\"morph\" at=\"Φ.a🌵3\" of=\"Φ.bytes\"><attr name=\"φ\">40-1C-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵3\" term=\"𝑛.2.4\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿2.2\">40-1C-00-00-00-00-00-00</bind>" , " <minted symbol=\"𝜎1\">40-18-00-00-00-00-00-00 40-1C-00-00-00-00-00-00</minted>"- , " <built meta=\"𝑛.2.1\">Φ.number( φ ↦ 𝜎1:λ )</built>"- , " <answer meta=\"𝑛.2.2\">⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧</answer>"+ , " <built meta=\"𝑛.2.5\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <applied meta=\"𝑛.2.6\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.number\"><attr name=\"φ\">𝜎1</attr></applied>"+ , " <answer meta=\"𝑛.2.7\">𝑛.2.6</answer>" , " </evaluate>"- , " <formation at=\"Φ.a🌵1\" term=\"⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧\">"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.2.6\">" , " </formation>" , " <dataize meta=\"𝛿2.1\">𝜎1:λ</dataize>" , " <minted symbol=\"𝜎2\">40-14-00-00-00-00-00-00 𝜎1</minted>"- , " <built meta=\"𝑛.1.1\">Φ.number( φ ↦ 𝜎2:λ )</built>"- , " <answer meta=\"𝑛.1.2\">⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧</answer>"+ , " <built meta=\"𝑛.1.5\">Φ.number( φ ↦ 𝜎2:λ )</built>"+ , " <applied meta=\"𝑛.1.6\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">𝜎2</attr></applied>"+ , " <answer meta=\"𝑛.1.7\">𝑛.1.6</answer>" , " </evaluate>"- , " <formation at=\"Φ\" term=\"⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧\">"+ , " <formation at=\"Φ\" term=\"𝑛.1.6\">" , " </formation>" , " </formation>" , "</dataize>"@@ -2077,20 +2163,27 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<dataize at=\"Φ\">" , " <formation at=\"Φ\" term=\"⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧, φ ↦ 2.times( 3 ).nope ⟧\">"+ , " <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ\" of=\"𝑛.0.1.times\"><attr name=\"x\">3</attr></applied>" , " <evaluate λ=\"L_number_times\" by=\"morph\" at=\"Φ\">"- , " <formation at=\"Φ.a🌵0\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ ), times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧\">"- , " <formation at=\"Φ.a🌵0\" term=\"40-00-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.1.1\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.1\">"+ , " <applied meta=\"𝑛.1.2\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.bytes\"><attr name=\"φ\">40-00-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.2\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿1.1\">40-00-00-00-00-00-00-00</bind>"- , " <formation at=\"Φ.a🌵1\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ 40-08-00-00-00-00-00-00:Δ ), times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧\">"- , " <formation at=\"Φ.a🌵1\" term=\"40-08-00-00-00-00-00-00:Δ:φ\">"+ , " <applied meta=\"𝑛.1.3\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ 40-08-00-00-00-00-00-00:Δ )</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.3\">"+ , " <applied meta=\"𝑛.1.4\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.bytes\"><attr name=\"φ\">40-08-00-00-00-00-00-00:Δ</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.4\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿2.1\">40-08-00-00-00-00-00-00</bind>" , " <minted symbol=\"𝜎1\">40-00-00-00-00-00-00-00 40-08-00-00-00-00-00-00</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.5\">Φ.number( φ ↦ 𝜎1:λ )</built>"+ , " <applied meta=\"𝑛.1.6\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">𝜎1</attr></applied>"+ , " <answer meta=\"𝑛.1.7\">𝑛.1.6</answer>" , " </evaluate>" , " <unanswered λ=\"L_number_nope\" by=\"dataize\">L_number_nope:λ</unanswered>" , " </formation>"@@ -2120,22 +2213,29 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<dataize at=\"Φ\">" , " <formation at=\"Φ\" term=\"⟦ bytes ↦ ⟦ φ ↦ ∅ ⟧, number ↦ ⟦ φ ↦ ∅, times ↦ ⟦ ρ ↦ ∅, x ↦ ∅, λ ⤍ L_number_times ⟧, nope ↦ ⟦ ρ ↦ ∅, λ ⤍ L_number_nope ⟧ ⟧, φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ) ).times( α0 ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧ ) ) ).nope ⟧\">"+ , " <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ )</attr></applied>"+ , " <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ\" of=\"𝑛.0.1.times\"><attr name=\"x\">Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧ ) )</attr></applied>" , " <evaluate λ=\"L_number_times\" by=\"morph\" at=\"Φ\">"- , " <formation at=\"Φ.a🌵0\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ), times ↦ ⟦ ρ ↦ ∅, x ↦ ∅, λ ⤍ L_number_times ⟧, nope ↦ ⟦ ρ ↦ ∅, λ ⤍ L_number_nope ⟧ ⟧\">"- , " <formation at=\"Φ.a🌵0\" term=\"⟦ φ ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧\">"+ , " <applied meta=\"𝑛.1.1\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ )</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.1\">"+ , " <applied meta=\"𝑛.1.2\" by=\"morph\" at=\"Φ.a🌵0\" of=\"Φ.bytes\"><attr name=\"φ\">⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧</attr></applied>"+ , " <formation at=\"Φ.a🌵0\" term=\"𝑛.1.2\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿1.1\">40-00-00-00-00-00-00-00</bind>"- , " <formation at=\"Φ.a🌵1\" term=\"⟦ φ ↦ Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧ ), times ↦ ⟦ ρ ↦ ∅, x ↦ ∅, λ ⤍ L_number_times ⟧, nope ↦ ⟦ ρ ↦ ∅, λ ⤍ L_number_nope ⟧ ⟧\">"- , " <formation at=\"Φ.a🌵1\" term=\"⟦ φ ↦ ⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧ ⟧\">"+ , " <applied meta=\"𝑛.1.3\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.number\"><attr name=\"φ\">Φ.bytes( φ ↦ ⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧ )</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.3\">"+ , " <applied meta=\"𝑛.1.4\" by=\"morph\" at=\"Φ.a🌵1\" of=\"Φ.bytes\"><attr name=\"φ\">⟦ Δ ⤍ 40-08-00-00-00-00-00-00 ⟧</attr></applied>"+ , " <formation at=\"Φ.a🌵1\" term=\"𝑛.1.4\">" , " </formation>" , " </formation>" , " <bind meta=\"𝛿2.1\">40-08-00-00-00-00-00-00</bind>" , " <minted symbol=\"𝜎1\">40-00-00-00-00-00-00-00 40-08-00-00-00-00-00-00</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.5\">Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )</built>"+ , " <applied meta=\"𝑛.1.6\" by=\"morph\" at=\"Φ\" of=\"Φ.number\"><attr name=\"φ\">𝜎1</attr></applied>"+ , " <answer meta=\"𝑛.1.7\">𝑛.1.6</answer>" , " </evaluate>"- , " <unanswered λ=\"L_number_nope\" by=\"dataize\">⟦ ρ ↦ Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), λ ⤍ L_number_nope ⟧</unanswered>"+ , " <unanswered λ=\"L_number_nope\" by=\"dataize\">⟦ ρ ↦ 𝑛.1.6, λ ⤍ L_number_nope ⟧</unanswered>" , " </formation>" , "</dataize>" ]@@ -2199,15 +2299,22 @@ lines records `shouldBe` [ "𝔻(Φ)" , " formation(⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧, φ ↦ 2.times( 3 ).nope ⟧) # 𝔻(Φ)"+ , " applied(𝑛.0.1) := 2 # 𝕄(Φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.times( x ↦ 3 ) # 𝕄(Φ)" , " 𝔼(L_number_times) # 𝕄(Φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ ), times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵0)"- , " formation(40-00-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.1) := 2 # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵0)" , " 𝛿1.1 := 40-00-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-08-00-00-00-00-00-00:Δ ), times(x) ↦ L_number_times:λ, nope ↦ L_number_nope:λ ⟧) # 𝔻(Φ.a🌵1)"- , " formation(40-08-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.3) := 3 # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.3) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-08-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.4) # 𝔻(Φ.a🌵1)" , " 𝛿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)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)" , " unanswered(L_number_nope) # 𝔻(L_number_nope:λ)" ] @@ -2279,6 +2386,22 @@ withStdin universe $ testCLISucceeded ["morph", symbolic, "--inside=5.plus( 6 )", "--sweet", "--hide-rho", "--flat"] ["⟦ x ↦ 6, λ ⤍ L_number_plus ⟧"] + it "opens the text protocol before the objects it made while aiming" $+ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+ hClose stream+ withStdin universe $+ testCLISucceeded ["morph", symbolic, "--inside=5.plus( 6 )", "--protocol=" ++ path, "--sweet", "--hide-rho", "--quiet"] []+ records <- readProtocol path+ takeWhile (/= '(') (concat (take 1 (lines records))) `shouldBe` "𝕄"++ it "opens the XML protocol before the objects it made while aiming" $+ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do+ hClose stream+ withStdin universe $+ testCLISucceeded ["dataize", symbolic, "--inside=5.plus( 6 )", "--protocol=" ++ path, "--sweet", "--hide-rho", "--quiet"] []+ records <- readProtocol path+ take 1 (lines records) `shouldBe` ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>"]+ it "cannot be used together with --locator" $ withStdin universe $ testCLIFailed ["dataize", "--inside=Q.@", "--locator=Q.@"] ["--inside and --locator cannot be used together"]@@ -2428,15 +2551,23 @@ records <- readProtocol path lines records `shouldBe` [ "𝕄(Φ.φ)"+ , " applied(𝑛.0.1) := 5 # 𝕄(Φ.φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.plus( x ↦ 6 ) # 𝕄(Φ.φ)" , " 𝔼(L_number_plus) # 𝕄(Φ.φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵0)"- , " formation(40-14-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.1) := 5 # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵0)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-14-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵0)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵0)" , " 𝛿1.1 := 40-14-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ), plus(x) ↦ L_number_plus:λ ⟧) # 𝔻(Φ.a🌵1)"- , " formation(40-18-00-00-00-00-00-00:Δ:φ) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.3) := 6 # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.3) # 𝔻(Φ.a🌵1)"+ , " applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-18-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵1)"+ , " formation(𝑛.1.4) # 𝔻(Φ.a🌵1)" , " 𝛿2.1 := 40-18-00-00-00-00-00-00 # 𝔻(ξ.x)"- , " 𝑛.1.1 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"- , " 𝑛.1.2 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧ # 𝕄(𝑛.1.1)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ.φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)"+ , " applied(𝑛.0.3) := 𝑛.1.6.plus( x ↦ 7 ) # 𝕄(Φ.φ)" ] it "saves morphing steps to dir with --steps-dir" $@@ -2600,7 +2731,7 @@ >>= (`shouldBe` ["# 𝕄(Φ.a)", "# 𝕄(Φ.a)", "# 𝕄(Φ.b)", "# 𝕄(Φ.b)"]) . map (dropWhile (/= '#')) . filter (isPrefixOf " 𝔼(") it "numbers the symbols of the protocol the way the answer numbers them" $- recorded ["--jobs=2"] >>= (`shouldSatisfy` elem " 𝑛.4.1 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎4 ⟧ ) # 𝑛")+ recorded ["--jobs=2"] >>= (`shouldSatisfy` elem " 𝑛.4.3 := Φ.number( φ ↦ ⟦ λ ⤍ 𝜎4 ⟧ ) # 𝑛") it "names what a binding mints after the binding" $ recorded ["--jobs=2"] >>= (`shouldSatisfy` any (isInfixOf "# 𝔻(Φ.a🌵4-0)"))@@ -2722,7 +2853,7 @@ recorded "plausible" >>= (`shouldSatisfy` ((== 4) . length . filter (isInfixOf "𝔼(L_number_plus)"))) it "answers a recalled firing with the line of the first under plausible" $- recorded "plausible" >>= (`shouldContain` [" 𝑛.4.2 := 𝑛.2.2 # 𝕄(𝑛.4.1)"])+ recorded "plausible" >>= (`shouldContain` [" 𝑛.4.2 := 𝑛.2.5 # 𝕄(𝑛.4.1)"]) it "dataizes to the same datum under plausible" $ withStdin chained $
test/CompiledSpec.hs view
@@ -16,7 +16,7 @@ import Data.Text qualified as T import Data.Yaml qualified as Yaml import Dataize (dataize')-import Deps (dontSaveStep)+import Deps (dontSaveMade, dontSaveStep) import Engine (Engine (..), building, fresh, yaml) import Files (allPathsIn) import Fixtures (defaultReduceContext, linked, withLambdasOf)@@ -82,7 +82,7 @@ <$> rewrite expr (_normalization engine)- (RewriteContext ExRoot 25 25 False universe (building engine) (_normal engine) (_matching engine) MtDisabled Nothing dontSaveStep)+ (RewriteContext ExRoot 25 25 False universe (building engine) (_normal engine) (_matching engine) MtDisabled Nothing dontSaveStep dontSaveMade) ) matched :: Expression -> IO (Set.Set Int) matched expr = Set.fromList . map fst <$> filterM (\(_, rule) -> not . null <$> matchExpressionWithRule expr rule (RuleContext (building yaml) Nothing (_normal yaml))) (zip [0 ..] Y.normalizationRules)
test/DataizeSpec.hs view
@@ -217,16 +217,23 @@ protocol `shouldBe` unlines [ " formation(⟦ bytes(φ) ↦ ⟦ not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧, bool(φ) ↦ ⟦ if(ρ, then, else) ↦ L_fork:λ ⟧, number(φ) ↦ ⟦ 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:λ ⟧, φ ↦ 2.times( 3 ).nope ⟧) # 𝔻(Φ)"+ , " applied(𝑛.0.1) := 2 # 𝕄(Φ)"+ , " applied(𝑛.0.2) := 𝑛.0.1.times( x ↦ 3 ) # 𝕄(Φ)" , " 𝔼(L_number_times) # 𝕄(Φ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ ), 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:λ ⟧) # 𝔻(Φ.a🌵17)"- , " formation(⟦ φ ↦ 40-00-00-00-00-00-00-00:Δ, not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧) # 𝔻(Φ.a🌵17)"+ , " applied(𝑛.1.1) := 2 # 𝕄(Φ.a🌵17)"+ , " formation(𝑛.1.1) # 𝔻(Φ.a🌵17)"+ , " applied(𝑛.1.2) := Φ.bytes( φ ↦ 40-00-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵17)"+ , " formation(𝑛.1.2) # 𝔻(Φ.a🌵17)" , " 𝛿1.1 := 40-00-00-00-00-00-00-00 # 𝔻(ξ.ρ)"- , " formation(⟦ φ ↦ Φ.bytes( φ ↦ 40-08-00-00-00-00-00-00:Δ ), 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:λ ⟧) # 𝔻(Φ.a🌵18)"- , " formation(⟦ φ ↦ 40-08-00-00-00-00-00-00:Δ, not(ρ) ↦ L_bytes_not:λ, eq(ρ, b) ↦ L_bytes_eq:λ ⟧) # 𝔻(Φ.a🌵18)"+ , " applied(𝑛.1.3) := 3 # 𝕄(Φ.a🌵18)"+ , " formation(𝑛.1.3) # 𝔻(Φ.a🌵18)"+ , " applied(𝑛.1.4) := Φ.bytes( φ ↦ 40-08-00-00-00-00-00-00:Δ ) # 𝕄(Φ.a🌵18)"+ , " formation(𝑛.1.4) # 𝔻(Φ.a🌵18)" , " 𝛿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)"- , " unanswered(L_number_nope) # 𝔻(⟦ ρ ↦ Φ.number( φ ↦ 𝜎1:λ ), λ ⤍ L_number_nope ⟧)"+ , " 𝑛.1.5 := Φ.number( φ ↦ 𝜎1:λ ) # 𝑛"+ , " applied(𝑛.1.6) := Φ.number( φ ↦ 𝜎1:λ ) # 𝕄(Φ)"+ , " 𝑛.1.7 := 𝑛.1.6 # 𝕄(𝑛.1.5)"+ , " unanswered(L_number_nope) # 𝔻(⟦ ρ ↦ 𝑛.1.6, λ ⤍ L_number_nope ⟧)" ] it "leaves an unanswered λ function dataized directly as the whole residue" $ do ((outcome, chain), protocol) <- partially known "[[ L> Sym_arg_0 ]]"
test/DepsSpec.hs view
@@ -5,14 +5,14 @@ module DepsSpec where -import AST (Argument (ArTau), Attribute (AtLabel), Binding (BiLambda, BiTau), Bytes (BtOne), Expression (ExApplication, ExDispatch, ExFormation, ExRoot, ExXi), Function (FnSymbol), symbols)+import AST (Argument (ArTau), Attribute (AtLabel, AtPhi), Binding (BiLambda, BiTau), Bytes (BtOne), Expression (ExApplication, ExDispatch, ExFormation, ExRoot, ExXi), Function (FnSymbol), symbols) import Control.Exception (bracket) import Control.Monad (replicateM_, when) import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (isInfixOf, isPrefixOf) import Data.Time.Clock.POSIX (getPOSIXTime)-import Deps (Acyclic (Proven), Evaluation (EvDeferred, EvFiring, EvFormation, EvJoined, EvLooped, EvMinted, EvRun, EvTerm), Judgment (Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, saveStep)-import Fixtures (readUtf8)+import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBuilt, EvComputed, EvDeferred, EvFiring, EvFormation, EvJoined, EvLooped, EvMinted, EvRun, EvTerm), Judgment (Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, saveStep)+import Fixtures (readUtf8, recorded, recordedXml) import GHC.Clock (getMonotonicTime) import Logger (LogLevel (DEBUG, ERROR, INFO), setLogConfig) import System.Directory@@ -25,7 +25,7 @@ import System.FilePath ((</>)) import System.IO (IOMode (WriteMode), stderr, withFile) import System.IO.Silently (hCapture_, hSilence)-import Test.Hspec (Spec, after_, describe, expectationFailure, it, shouldBe, shouldSatisfy)+import Test.Hspec (Spec, after_, describe, expectationFailure, it, shouldBe, shouldContain, shouldSatisfy) withScratchDir :: (FilePath -> IO a) -> IO a withScratchDir =@@ -128,6 +128,60 @@ case renumbered 2 5 (EvLooped 3 Morphing Proven (ExFormation []) ExXi (Just (4, Just (ExApplication (ExDispatch ExRoot (AtLabel "box")) (ArTau (AtLabel "n") (ExFormation [BiLambda (FnSymbol 7)])))))) of EvLooped _ _ _ _ _ answer -> fmap (fmap (fmap symbols)) answer `shouldBe` Just (9, Just [12]) _ -> expectationFailure "The record did not stay the record it was"+ it "raises the symbols an application and the object it made carry above the floor" $+ case renumbered 2 5 (EvApplied 3 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "box")) (ArTau (AtLabel "x") (ExFormation [BiLambda (FnSymbol 4)]))) (ExFormation [BiTau (AtLabel "x") (ExFormation [BiLambda (FnSymbol 1)])]) ExXi) of+ EvApplied _ _ call object _ -> (symbols call, symbols object) `shouldBe` ([9], [1])+ _ -> expectationFailure "The record did not stay the record it was"+ it "raises the symbols an object carries before and after the walk computed inside it above the floor" $+ case renumbered 3 4 (EvComputed 2 (ExFormation [BiTau (AtLabel "ш") (ExFormation [BiLambda (FnSymbol 2)])]) (ExFormation [BiTau (AtLabel "ш") (ExFormation [BiLambda (FnSymbol 6)])])) of+ EvComputed _ before after -> (symbols before, symbols after) `shouldBe` ([2], [10])+ _ -> expectationFailure "The record did not stay the record it was"++ describe "saveEval" $ do+ it "writes an application as a line binding what it made to a fresh 𝑛" $ do+ (_, written) <- recorded (\record -> record (EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "w"))))+ written `shouldBe` " applied(𝑛.0.1) := Φ.ёж( q ↦ ⟦⟧ ) # 𝕄(Φ.w)\n"+ it "spells an object an application made by its name on a later line" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvFiring 1 "L_щ" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvTerm 2 "𝑛1" (ExDispatch ExXi (AtLabel "z")) (ExFormation [BiTau (AtLabel "z") (ExFormation [BiTau (AtLabel "q") (ExFormation [])]), BiTau (AtLabel "у") (ExFormation [])])])+ last (lines written) `shouldBe` " 𝑛1.1 := ⟦ z ↦ 𝑛.1.1, у ↦ ⟦⟧ ⟧ # 𝕄(ξ.z)"+ it "numbers the answer of a firing past the objects applications made inside it" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvFiring 1 "L_ю" Morphing ExRoot, EvBuilt 2 (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))), EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvAnswer 2 (ExFormation [BiTau (AtLabel "q") (ExFormation [])])])+ last (lines written) `shouldBe` " 𝑛.1.3 := 𝑛.1.2 # 𝕄(𝑛.1.1)"+ it "spells an application an earlier line wrote by its name in the argument of a later one" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "жук")) (ArTau (AtLabel "w") (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))))) (ExFormation [BiTau (AtLabel "w") (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation [])))]) ExRoot])+ last (lines written) `shouldBe` " applied(𝑛.0.2) := Φ.жук( w ↦ 𝑛.0.1 ) # 𝕄(Φ)"+ it "spells an application made again by its head and argument rather than by the name of the first one" $ do+ (_, written) <- recorded (\record -> replicateM_ 2 (record (EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot)))+ last (lines written) `shouldBe` " applied(𝑛.0.2) := Φ.ёж( q ↦ ⟦⟧ ) # 𝕄(Φ)"+ it "writes a deferred copy as the call it was made of even when an earlier application spelled that call" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 3)]))) (ExFormation [BiTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 3)])]) ExRoot, EvDeferred 1 4 Morphing (ExFormation [BiTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 3)])]) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 3)])))) ExRoot])+ last (lines written) `shouldBe` " deferred(𝜎4) := Φ.ёж( q ↦ 𝜎3:λ ) # 𝕄(Φ)"+ it "spells an object the walk computed inside by the name its application gave it" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvFiring 1 "L_ъ" Morphing ExRoot, EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ф")))) (ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ф"))]) ExRoot, EvComputed 2 (ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ф"))]) (ExFormation [BiTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 8)])]), EvTerm 2 "𝑛1" (ExDispatch ExXi (AtLabel "z")) (ExFormation [BiTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 8)])])])+ last (lines written) `shouldBe` " 𝑛1.1 := 𝑛.1.1 # 𝕄(ξ.z)"+ it "spells out an object the walk computed inside when no application named it" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvComputed 1 (ExFormation [BiTau (AtLabel "ю") ExRoot]) (ExFormation [BiTau (AtLabel "ю") (ExFormation [BiLambda (FnSymbol 3)])]), EvTerm 1 "𝑛1" (ExDispatch ExXi (AtLabel "z")) (ExFormation [BiTau (AtLabel "ю") (ExFormation [BiLambda (FnSymbol 3)])])])+ last (lines written) `shouldBe` " 𝑛1.0 := 𝜎3:λ:ю # 𝕄(ξ.z)"+ it "writes no line for an object the walk computed inside" $ do+ (_, written) <- recorded (\record -> record (EvComputed 1 (ExFormation [BiTau (AtLabel "ю") ExRoot]) (ExFormation [BiTau (AtLabel "ю") (ExFormation [BiLambda (FnSymbol 3)])])))+ written `shouldBe` ""++ describe "saveEvalXml" $ do+ it "writes an application as an element naming its head and holding its argument" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ.w", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "w"))])+ lines written `shouldContain` [" <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ.w\" of=\"Φ.ёж\"><attr name=\"q\">⟦⟧</attr></applied>"]+ it "spells an argument an earlier application made by its name" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "жук")) (ArTau (AtLabel "w") (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))))) (ExFormation [BiTau (AtLabel "w") (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation [])))]) ExRoot])+ lines written `shouldContain` [" <applied meta=\"𝑛.0.2\" by=\"morph\" at=\"Φ\" of=\"Φ.жук\"><attr name=\"w\">𝑛.0.1</attr></applied>"]+ it "spells an argument that is a bare symbol as that symbol" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "цапля")) (ArTau AtPhi (ExFormation [BiLambda (FnSymbol 7)]))) (ExFormation [BiTau AtPhi (ExFormation [BiLambda (FnSymbol 7)])]) ExRoot])+ lines written `shouldContain` [" <applied meta=\"𝑛.0.1\" by=\"morph\" at=\"Φ\" of=\"Φ.цапля\"><attr name=\"φ\">𝜎7</attr></applied>"]+ it "spells an object an application made by its name in a later element" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_ы" Morphing ExRoot, EvBuilt 2 (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))), EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) ExRoot, EvAnswer 2 (ExFormation [BiTau (AtLabel "q") (ExFormation [])])])+ lines written `shouldContain` [" <answer meta=\"𝑛.1.3\">𝑛.1.2</answer>"]+ it "spells an object the walk computed inside by its name in a later element" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ф")))) (ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ф"))]) ExRoot, EvComputed 1 (ExFormation [BiTau (AtLabel "q") (ExDispatch ExRoot (AtLabel "ф"))]) (ExFormation [BiTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 8)])]), EvFormation 1 (ExFormation [BiTau (AtLabel "q") (ExFormation [BiLambda (FnSymbol 8)])]) ExRoot])+ lines written `shouldContain` [" <formation at=\"Φ\" term=\"𝑛.0.1\">"] describe "perSecond" $ do it "divides the firings by the seconds the run took" $
test/Fixtures.hs view
@@ -16,6 +16,7 @@ , readUtf8 , recorded , recorded'+ , recordedXml , withLambdas , withLambdasOf , withTemp@@ -110,32 +111,39 @@ recorded' :: Bool -> (SaveEvalFunc -> IO a) -> IO (a, String) recorded' hidden action = withTemp "phino-protocol-.txt" BS.empty $ \path -> do- answer <- withEvalFunc (Just path) printing action+ answer <- withEvalFunc (Just path) (printing hidden) action written <- withoutTotals <$> readUtf8 path pure (answer, written)- where- printing :: PrintContext- printing =- PrintCtx- SWEET- hidden- Nothing- False- MULTILINE- 2- defaultXmirContext- False- False- False- False- False- 1- 1- ExRoot- Nothing- Nothing- Nothing- PHI++recordedXml :: (SaveEvalFunc -> IO a) -> IO (a, String)+recordedXml action =+ withTemp "phino-protocol-.xml" BS.empty $ \path -> do+ answer <- withEvalFunc (Just path) (printing False) action+ written <- readProtocol path+ pure (answer, written)++printing :: Bool -> PrintContext+printing hidden =+ PrintCtx+ SWEET+ hidden+ Nothing+ False+ MULTILINE+ 2+ defaultXmirContext+ False+ False+ False+ False+ False+ 1+ 1+ ExRoot+ Nothing+ Nothing+ Nothing+ PHI newtype ExplainPack = ExplainPack String
test/LaTeXSpec.hs view
@@ -215,6 +215,7 @@ ] ( \(judgment, arrow) -> it ("ends a step taken by " ++ show judgment ++ " with " ++ arrow ++ " and opens the next one with it") $ do+ let reference = if judgment == Contextualization then "" else "[\\nameref{r:tv}]" first <- parseExpressionThrows "[[ q -> Q.f ]]" second <- parseExpressionThrows "[[ q -> Q.j ]]" latex <- rewrittensToLatex ([(first, Just (judgment, "tv")), (second, Nothing)], False) defaultLatexContext@@ -222,7 +223,7 @@ `shouldBe` intercalate "\n" [ "\\begin{phiquation}"- , "Q . |f| : |q| " ++ arrow ++ "[\\nameref{r:tv}]"+ , "Q . |f| : |q| " ++ arrow ++ reference , " " ++ arrow ++ " Q . |j| : |q|{.}" , "\\end{phiquation}" ]
test/RewriterSpec.hs view
@@ -9,16 +9,17 @@ module RewriterSpec where -import AST (Argument (ArTau), Attribute (AtLabel), Binding (BiMeta, BiTau, BiVoid), Expression (ExApplication, ExDispatch, ExFormation, ExRoot, ExTermination, ExXi))+import AST (Argument (ArTau), Attribute (AtLabel, AtRho), Binding (BiMeta, BiTau, BiVoid), Expression (ExApplication, ExDispatch, ExFormation, ExRoot, ExTermination, ExXi)) import Control.Exception (SomeException) import Control.Monad (forM_, unless) import Data.Aeson import Data.Char (isSpace)+import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (isInfixOf, nub) import Data.List.NonEmpty qualified as NE import Data.Set qualified as Set import Data.Yaml qualified as Yaml-import Deps (Judgment (..), dontSaveStep)+import Deps (Judgment (..), dontSaveMade, dontSaveStep) import Engine (Engine (_matching, _normal), building, stepOf) import Files (allPathsIn, ensuredFile) import Fixtures (linked)@@ -116,7 +117,7 @@ ] ( \(desc, input', (maxDepth, maxCycles, depthSensitive), expected) -> it desc $ do expr <- parseExpressionThrows input'- let action = rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext ExRoot maxDepth maxCycles depthSensitive Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep)+ let action = rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext ExRoot maxDepth maxCycles depthSensitive Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep dontSaveMade) case expected of Left fragment -> action `shouldThrow` (\exc -> fragment `isInfixOf` show (exc :: SomeException)) Right predicate -> do@@ -144,7 +145,7 @@ ] ( \(desc, must', expected) -> it desc $ do expr <- parseExpressionThrows "⟦ t ↦ ⊥.a.b.c ⟧"- let action = rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 1 1 False Nothing (building linked) (_normal linked) (_matching linked) must' Nothing dontSaveStep)+ let action = rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 1 1 False Nothing (building linked) (_normal linked) (_matching linked) must' Nothing dontSaveStep dontSaveMade) case expected of Left fragment -> action `shouldThrow` (\exc -> fragment `isInfixOf` show (exc :: SomeException)) Right predicate -> do@@ -155,17 +156,31 @@ describe "judges the steps it takes" $ it "takes every step by normalization" $ do expr <- parseExpressionThrows "⟦ k ↦ ⟦ w ↦ ⟦ Δ ⤍ 1F- ⟧ ⟧.w ⟧"- (rewrittens, _) <- rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep)+ (rewrittens, _) <- rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep dontSaveMade) nub [judgment | (_, Just (judgment, _)) <- NE.toList rewrittens] `shouldBe` [Normalization] + describe "tells what an application made" $ do+ it "tells the application a step turned into an object, beside the object" $ do+ made <- newIORef []+ _ <- rewrite (ExApplication (ExFormation [BiVoid (AtLabel "ж")]) (ArTau (AtLabel "ж") (ExFormation []))) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :)))+ readIORef made `shouldReturn` [(ExApplication (ExFormation [BiVoid (AtLabel "ж")]) (ArTau (AtLabel "ж") (ExFormation [])), ExFormation [BiTau (AtLabel "ж") (ExFormation [])])]+ it "tells nothing of an application a step left the object it was" $ do+ made <- newIORef []+ _ <- rewrite (ExApplication (ExFormation [BiTau (AtLabel "ъ") (ExFormation [])]) (ArTau AtRho (ExFormation []))) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :)))+ readIORef made `shouldReturn` []+ it "tells nothing of the ρ a dispatch fills" $ do+ made <- newIORef []+ _ <- rewrite (ExApplication (ExFormation [BiVoid AtRho, BiVoid (AtLabel "щ")]) (ArTau AtRho (ExFormation [BiTau (AtLabel "ё") (ExFormation [])]))) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :)))+ readIORef made `shouldReturn` []+ describe "rewrites by a locator" $ do it "rewrites the located part step after step" $ do expr <- parseExpressionThrows "⟦ t ↦ ⊥.a.b, u ↦ ⊥.c ⟧"- (rewrittens, _) <- rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext (ExDispatch ExRoot (AtLabel "t")) 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep)+ (rewrittens, _) <- rewrite expr (map (stepOf linked) normalizationRules) (RewriteContext (ExDispatch ExRoot (AtLabel "t")) 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep dontSaveMade) fst (NE.last rewrittens) `shouldBe` ExFormation [BiTau (AtLabel "t") ExTermination, BiTau (AtLabel "u") (ExDispatch ExTermination (AtLabel "c"))] it "fails on a locator that points nowhere even when no rule runs" $ do expr <- parseExpressionThrows "⟦ t ↦ ⊥.a ⟧"- rewrite expr [] (RewriteContext (ExDispatch ExRoot (AtLabel "w")) 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep)+ rewrite expr [] (RewriteContext (ExDispatch ExRoot (AtLabel "w")) 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep dontSaveMade) `shouldThrow` (\exc -> "Can't find object by locator" `isInfixOf` show (exc :: SomeException)) describe "rewrite packs" $ do@@ -225,6 +240,7 @@ must' Nothing dontSaveStep+ dontSaveMade ) let (rewritten, _) = NE.last rewrittens result' <- parseExpressionThrows (output pack)@@ -238,10 +254,10 @@ ) describe "asks which steps match" $ do it "does not try a step the matching does not name" $- (fst . NE.last . fst <$> rewrite ExXi [direct "qv" False (\_ expr -> [ExRoot | ExXi <- [expr]])] (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (\_ _ -> Set.empty) MtDisabled Nothing dontSaveStep))+ (fst . NE.last . fst <$> rewrite ExXi [direct "qv" False (\_ expr -> [ExRoot | ExXi <- [expr]])] (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (\_ _ -> Set.empty) MtDisabled Nothing dontSaveStep dontSaveMade)) `shouldReturn` ExXi it "asks the matching again once a step changed the term" $- (fst . NE.last . fst <$> rewrite ExXi [direct "xr" False (\_ expr -> [ExRoot | ExXi <- [expr]]), direct "rt" False (\_ expr -> [ExTermination | ExRoot <- [expr]])] (RewriteContext ExRoot 25 1 False Nothing (building linked) (_normal linked) (\_ expr -> Set.fromList [idx | (idx, ptn) <- [(0, ExXi), (1, ExRoot)], ptn == expr]) MtDisabled Nothing dontSaveStep))+ (fst . NE.last . fst <$> rewrite ExXi [direct "xr" False (\_ expr -> [ExRoot | ExXi <- [expr]]), direct "rt" False (\_ expr -> [ExTermination | ExRoot <- [expr]])] (RewriteContext ExRoot 25 1 False Nothing (building linked) (_normal linked) (\_ expr -> Set.fromList [idx | (idx, ptn) <- [(0, ExXi), (1, ExRoot)], ptn == expr]) MtDisabled Nothing dontSaveStep dontSaveMade)) `shouldReturn` ExTermination describe "every" $ it "names each of the steps it is handed" $@@ -249,13 +265,16 @@ `shouldBe` Set.fromList [0, 1, 2] describe "direct" $ do it "rewrites every place the function matches at" $- _applied (direct "tx" False (\_ expr -> [ExRoot | ExXi <- [expr]])) (RuleContext buildTerm Nothing (const True)) (ExDispatch (ExApplication ExXi (ArTau (AtLabel "o") ExXi)) (AtLabel "m"))+ fmap fst <$> _applied (direct "tx" False (\_ expr -> [ExRoot | ExXi <- [expr]])) (RuleContext buildTerm Nothing (const True)) (ExDispatch (ExApplication ExXi (ArTau (AtLabel "o") ExXi)) (AtLabel "m")) `shouldReturn` Just (ExDispatch (ExApplication ExRoot (ArTau (AtLabel "o") ExRoot)) (AtLabel "m"))+ it "tells every place it rewrote, beside what it rewrote it to" $+ fmap snd <$> _applied (direct "tq" False (\_ expr -> [ExRoot | ExXi <- [expr]])) (RuleContext buildTerm Nothing (const True)) (ExApplication ExXi (ArTau (AtLabel "ё") ExXi))+ `shouldReturn` Just [(ExXi, ExRoot), (ExXi, ExRoot)] it "tells it matched nowhere" $ _applied (direct "tx" False (\_ expr -> [ExRoot | ExXi <- [expr]])) (RuleContext buildTerm Nothing (const True)) (ExDispatch ExTermination (AtLabel "m")) `shouldReturn` Nothing it "hands the world to the function" $- _applied (direct "tw" False (\universe expr -> [world | ExXi <- [expr], Just world <- [universe]])) (RuleContext buildTerm (Just ExTermination) (const True)) ExXi+ fmap fst <$> _applied (direct "tw" False (\universe expr -> [world | ExXi <- [expr], Just world <- [universe]])) (RuleContext buildTerm (Just ExTermination) (const True)) ExXi `shouldReturn` Just ExTermination describe "fast" $ do it "holds for a formation rewritten between the same two meta bindings" $