diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ ```bash cabal update -cabal install --overwrite-policy=always phino-0.0.153 +cabal install --overwrite-policy=always phino-0.0.154 phino --version ``` @@ -59,7 +59,7 @@ for the runner and puts it on the `PATH`: ```yaml -- uses: objectionary/phino@0.0.153 +- uses: objectionary/phino@0.0.154 with: version-file: phino-version.txt - run: phino --version @@ -173,8 +173,8 @@ 𝑛: 𝑛5 ``` -The right-hand side of a line names a meta bound by `morph` or by an `evaluate` -line above it, and nothing else. A formation with a λ function is fired by the +The right-hand side of a line names a meta bound by `morph` or by another line +of the entry, and nothing else. A formation with a λ function is fired by the entry its λ name matches, the way 𝕄 fires it, and the line binds its meta to the normal form of the answer. A formation with no λ function is no call and stays as it is, and so does `⊥`. A λ name no entry answers gets stuck, as it @@ -222,8 +222,8 @@ 𝑛: 𝑛3 ``` -The meta under `of` is one bound by `morph`, by `evaluate` or by a `rewrite` -line above it, and nothing else. A rule is tried at every position of the term, +The meta under `of` is one bound by `morph` or by another line of the entry, +and nothing else. A rule is tried at every position of the term, the outermost first; the first rule whose pattern matches a position rewrites it, and a rewritten position is not walked into again, so a rule whose result carries its own pattern never loops. Nothing is normalized afterwards: a @@ -235,13 +235,57 @@ This is how a program brings two branches of a fork to one shape before they are compared. In EO a `Φ.false` is written `φ ↦ ξ.right` while a bool a firing answered carries a symbol, and the two are one value in two spellings that -only the program knows to be one. The block runs before `symbolize` on purpose: -a result may write the datum a literal stands for, as `⟦ Δ ⤍ 00- ⟧` above, and -that datum is then stood into a known symbol the join can pair. +only the program knows to be one. A `symbolize` line may read what a `rewrite` +line made on purpose: a result may write the datum a literal stands for, as +`⟦ Δ ⤍ 00- ⟧` above, and that datum is then stood into a known symbol the join +can pair. +### Dropping the ρ of a dispatch + +There is a fifth block, `stay`, and it reduces nothing either. Each line of it +takes a term another meta of the entry is already bound to and binds an +expression meta of its own to that term with every `( ρ ↦ … )` dropped that is +applied to a dispatch: + +```yaml +- λ: L_fork + morph: + 𝑛1: $.left + 𝑛2: $.right + stay: + 𝑛3: 𝑛1 + 𝑛4: 𝑛2 + join: + 𝑛5: [𝑛3, 𝑛4] + 𝑛: 𝑛5 +``` + +The right-hand side of a line names a meta bound by `morph` or by another line +of the entry, and nothing else. Every position of the term is walked, the +methods and the `ρ` of a formation among them, and `𝑒.𝜏( ρ ↦ 𝑒2 )` becomes +`𝑒.𝜏`. So does a dispatch heading a chain of applications that bind no `ρ`: +`𝑒.𝜏( φ ↦ 𝑒3 )( ρ ↦ 𝑒2 )` becomes +`𝑒.𝜏( φ ↦ 𝑒3 )`. A `ρ` applied to anything else, such as a formation, stays. + +Dropping it changes no value. The `dot` rule answers a dispatch as +`𝑛1( ρ ↦ ⟦…⟧ )`, and then `copy` fills a void `ρ` of the body, `stay` keeps a +bound one and `skip` drops it where the body declares none. So once `𝑒.𝜏` +comes to a formation, a later `( ρ ↦ 𝑒2 )` meets a `ρ` that is bound or not +there, and `stay` or `skip` drops it. The block only drops it earlier, before +the dispatch is reduced. + +This is how a fork brings two numbers to one shape. In EO `bytes.as-number` +reads its `data` as `ρ`, so a branch computed through it comes to +`Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1 )( ρ ↦ ⟦ … ⟧ ) )`, with the copy hung on the +bytes as their `ρ`, while a branch made of no object comes to +`Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2 ) )`. The join compares the two as written and +the tail refuses it; after `stay` they differ in their symbols alone. The +protocol writes each line of the block the way it writes a `rewrite` one, +commented with the meta it took. + ### Standing data into unknowns -There is a fifth block, `symbolize`, and it reduces nothing. It takes a term +There is a sixth block, `symbolize`, and it reduces nothing. It takes a term another meta of the entry is already bound to and binds an expression meta of its own to that same term with every datum in it standing for an unknown: @@ -258,9 +302,9 @@ 𝑛: 𝑛3 ``` -The right-hand side of a line names a meta bound by `morph`, by `evaluate`, by -`rewrite` or by a `symbolize` line above it, and nothing else; a term nobody -reduced has no data to stand. Every `Δ ⤍ b` binding of that term becomes a +The right-hand side of a line names a meta bound by `morph` or by another line +of the entry, and nothing else; a term nobody reduced has no data to stand. +Every `Δ ⤍ b` binding of that term becomes a `λ ⤍ 𝜎k` naming a fresh symbol, one per occurrence, so `⟦ Δ ⤍ b ⟧` reads as `⟦ λ ⤍ 𝜎k ⟧` and a literal tuple gets several. A term carrying no datum passes through as it was. @@ -287,7 +331,7 @@ A branching λ function answers neither of its branches. Which one the program takes is decided by a value nobody worked out, so handing one of them through would drop the branch point from the program altogether and a reader would see -the condition computed and thrown away. `join` is the sixth block, and it +the condition computed and thrown away. `join` is the seventh block, and it reduces nothing either: it takes two metas the entry has bound already and binds one of its own to the two terms joined into one. @@ -306,12 +350,10 @@ 𝑛: 𝑛5 ``` -A line names two metas bound by `morph`, by `evaluate`, by `rewrite`, by -`symbolize` or by a `join` line above it, and never three: it stands for a -choice between two branches, and a walk over three terms in parallel is no such -choice. The meta it binds is one like any other, so the answer may name it -alone, as above, or stand -it inside a larger term. +A line names two metas bound by `morph` or by other lines of the entry, and +never three: it stands for a choice between two branches, and a walk over three +terms in parallel is no such choice. The meta it binds is one like any other, +so the answer may name it alone, as above, or stand it inside a larger term. `phino` takes the two terms and requires them to match verbatim, with one exception: where `⟦ λ ⤍ 𝜎A ⟧` in one meets a different `⟦ λ ⤍ 𝜎B ⟧` in the @@ -334,11 +376,12 @@ which is what lets the program go on dispatching on what the fork answered. A join is only ever between two expressions and a datum is never joined with -anything, which is why `symbolize` runs before it: a known symbol, one that -stage minted for a datum, is a symbol like any other here, so a literal branch -joins with a computed one and two literal branches join too. Any other -difference — a datum against a symbol, two different data, a binding one term -carries and the other does not — is no join at all, and the firing gets stuck +anything, which is why its branches go through `symbolize` first: a known +symbol, one that stage minted for a datum, is a symbol like any other here, so +a literal branch joins with a computed one and two literal branches join too. +Any other difference — a datum against a symbol, two different data, a binding +one term carries and the other does not — is no join at all, and the firing +gets stuck the way a λ function no entry answers does, so `--partial` parks it rather than aborting the run. A fork whose branches differ in structure, such as a `Φ.true` and a `Φ.false` written as `φ ↦ ξ.left` against `φ ↦ ξ.right`, is stuck, and @@ -403,6 +446,40 @@ `⟦ φ ↦ Φ.bool( … ) ⟧`, is left as it is, since morphing it only expands the call. +That step gets stuck on a branch that is a copy, such as +`Φ.step( tup ↦ Φ.items.tail )`, one of whose arguments reads to a bare +symbol `⟦ λ ⤍ 𝜎1 ⟧`: morphing its `φ`, `tup.next`, asks `𝜎1` for an +attribute nobody knows. An entry that says `defer: true` beside +`lenient: true` does not enter such a copy. It answers the copy with a fresh +symbol, joins that symbol instead, and writes what it stands for: + +```text +deferred(𝜎3) := Φ.step( tup ↦ 𝜎1:λ ) # 𝕄(𝑛2.φ) +``` + +The markup writes it as ``, holding a +`` element with an `𝜎1` per argument, a `?` for +an argument that is no bare symbol, and the copy itself in ``. The `of` is +left out when the world declares no object the copy was made of. A copy whose +arguments read to no bare symbol is entered as before. An entry that says +`defer: true` and is not lenient is refused when the file is read. + +The same entry answers a copy it did enter when `--acyclic` cuts the firing +its `φ` comes to. With `rec(n) ↦ ⟦ φ ↦ Φ.fork( ⟦ λ ⤍ 𝜎1 ⟧, Φ.rec( ξ.n ) ) ⟧`, +the copy `Φ.rec( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ )` reads to no bare symbol, so the step +enters it, comes to the same fork, and fires it again, and the cut refuses +that firing. A lenient entry without `defer: true` loses the whole firing to +the cut. A deferring one answers the copy with a fresh symbol, joins that +symbol, and writes it on the `looped` line: + +```text +looped(𝑛·1·3) := 𝜎3 # 𝔼(𝑛2), proven +``` + +The markup writes it as `` with the same +`` element a `deferred` record holds, here `𝜎2`, +since an argument whose `φ` holds a bare symbol counts as that symbol. + One term being `⊥` is the exception, since `if. cond value ⊥` is how EO spells "raise unless `cond`": the program raises on that side of the condition and has a perfectly good value on the other. The join then mints nothing, binds @@ -445,6 +522,37 @@ so a reader ties it to the two it stands for without diffing the terms; the section on `--protocol` below shows one. +### The order of the lines + +The lines of `evaluate`, `rewrite`, `stay`, `symbolize` and `join` run in the +order of the metas they read, not in the order of their blocks. A line runs +once every meta it reads is bound, so this entry fires what its `rewrite` line +unwrapped: + +```yaml +- λ: L_pick + morph: + 𝑛1: $.x + rewrite: + 𝑛2: + of: 𝑛1 + rules: + - name: unwrap + pattern: ⟦ φ ↦ 𝑒1 ⟧ + result: 𝑒1 + evaluate: + 𝑛3: 𝑛2 + 𝑛: 𝑛3 +``` + +The `evaluate` line reads `𝑛2`, which the `rewrite` line binds, so the +`rewrite` line runs first. The `dataize` and `morph` blocks read no meta and +always run before all the others. Where no meta orders two lines, they run in +the order the list above gives their blocks, and the lines of one block in the +order of their metas, `𝑛2` before `𝑛10`. A line reading a meta nothing binds +is refused when the file is read, and so is a line that reads the meta it +binds, directly or through other lines, since it could never run. + ### Symbols An entry answers, it never computes. The job of these functions is symbolic @@ -721,11 +829,16 @@ residue instead of failing: what `phino` could not decide is a property of the program and not of the option that decides what to do about it. -Three more lines say why a firing gave no answer. +Four more lines say why a firing gave no answer. `stuck(L_outer)` is the last line of a firing that got stuck, naming the λ function it got stuck on, which is seldom the one `unanswered(…)` names: that one is written where it was asked for, and this one closes every firing the failure passed on its way out. +`unjoined(L_fork)` takes its place in the firing whose `join` line could not +pair its two branches, and carries them as the join last saw them, +`unjoined(L_fork) # 𝜎1:λ:l vs ⟦ l ↦ 𝜎2:λ, x ↦ ⟦⟧ ⟧`, so a fork the program +left in two shapes never reads as an operand that ran out of steps; the +firings around it still close with `stuck(L_fork)`. `stall(L_outer)` stands under a firing that `--acyclic=plausible` answered with the stall an earlier firing of the same formation kept, so a told stall never reads as a fresh firing that wrote nothing. @@ -748,8 +861,9 @@ stuck(L_outer) ``` -The markup spells them ``, `` -and ``. +The markup spells them ``, +`𝜎1:λ:l⟦ l ↦ 𝜎2:λ, x ↦ ⟦⟧ ⟧`, +`` and ``. `timeout(5)` is where `--max-seconds=5` ran out, placed and commented the same way and written at the first step the deadline refused. @@ -1755,6 +1869,13 @@ ⟧ ``` +The two styles may be mixed in one expression, so `[[ x -> ∅ ]]` reads the +same as `⟦ x ↦ ∅ ⟧`. The `--monoform` option forbids that: the first symbol +that has two spellings picks the style of the whole expression, and a later +symbol of the other style is an error. Under `--monoform`, `[[ x -> ∅ ]]` +fails, since `∅` at 1:9 mixes with the ASCII `[[` at 1:1. The option is +accepted by `rewrite`, `dataize`, `morph`, `merge` and `match`. + A formation of a single binding may be written as its asset, a colon, and the attribute the asset is bound to: @@ -2158,119 +2279,119 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 2101646.837 μs - avg: 210164.684 μs - min: 191034.014 μs - max: 247000.010 μs - std dev: 21885.360 μs + total: 1797890.573 μs + avg: 179789.057 μs + min: 162091.874 μs + max: 210027.085 μs + std dev: 16246.548 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 9327965.748 μs - avg: 932796.575 μs - min: 864569.297 μs - max: 1038777.636 μs - std dev: 67090.644 μs + total: 7935401.706 μs + avg: 793540.171 μs + min: 737257.079 μs + max: 864759.805 μs + std dev: 46225.278 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 21.780 μs - avg: 2.178 μs - min: 1.663 μs - max: 2.535 μs - std dev: 0.286 μs + total: 17.396 μs + avg: 1.740 μs + min: 1.603 μs + max: 2.082 μs + std dev: 0.127 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 4374361.243 μs - avg: 437436.124 μs - min: 398758.490 μs - max: 473283.855 μs - std dev: 26607.005 μs + total: 5454056.634 μs + avg: 545405.663 μs + min: 515758.348 μs + max: 582503.512 μs + std dev: 22764.961 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 663496.668 μs - avg: 66349.667 μs - min: 58505.945 μs - max: 81586.458 μs - std dev: 8909.299 μs + total: 552072.467 μs + avg: 55207.247 μs + min: 49412.521 μs + max: 67399.308 μs + std dev: 7769.298 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 14094681.991 μs - avg: 1409468.199 μs - min: 1353470.986 μs - max: 1470382.428 μs - std dev: 30647.729 μs + total: 17341236.442 μs + avg: 1734123.644 μs + min: 1695951.065 μs + max: 1783518.134 μs + std dev: 22630.032 μs === morph/symbolic/demo/e1 === warmup: 3 iterations - batches: 10 x 2 - total: 179986.717 μs - avg: 8999.336 μs - min: 8393.411 μs - max: 11474.177 μs - std dev: 1088.979 μs + batches: 10 x 11 + total: 10945.365 μs + avg: 99.503 μs + min: 97.173 μs + max: 103.887 μs + std dev: 1.985 μs === morph/symbolic/demo/e2 === warmup: 3 iterations - batches: 10 x 2 - total: 162405.617 μs - avg: 8120.281 μs - min: 8045.820 μs - max: 8235.901 μs - std dev: 55.769 μs + batches: 10 x 174 + total: 174504.049 μs + avg: 100.290 μs + min: 99.832 μs + max: 101.139 μs + std dev: 0.345 μs === morph/symbolic/demo/e3 === warmup: 3 iterations - batches: 10 x 2 - total: 231633.663 μs - avg: 11581.683 μs - min: 11461.187 μs - max: 11878.593 μs - std dev: 123.097 μs + batches: 10 x 171 + total: 173859.715 μs + avg: 101.672 μs + min: 101.424 μs + max: 102.096 μs + std dev: 0.212 μs === morph/symbolic/demo/e4 === warmup: 3 iterations - batches: 10 x 3 - total: 208729.614 μs - avg: 6957.654 μs - min: 6899.022 μs - max: 6999.483 μs - std dev: 29.412 μs + batches: 10 x 152 + total: 155114.153 μs + avg: 102.049 μs + min: 101.576 μs + max: 103.791 μs + std dev: 0.632 μs === morph/symbolic/demo/e5 === warmup: 3 iterations - batches: 10 x 9 - total: 200950.553 μs - avg: 2232.784 μs - min: 2216.430 μs - max: 2252.836 μs - std dev: 10.899 μs + batches: 10 x 160 + total: 164432.368 μs + avg: 102.770 μs + min: 101.849 μs + max: 105.495 μs + std dev: 1.045 μs === morph/symbolic/native/e5 === warmup: 3 iterations - batches: 10 x 1 - total: 173698.880 μs - avg: 17369.888 μs - min: 16596.425 μs - max: 19463.645 μs - std dev: 879.974 μs + batches: 10 x 165 + total: 171308.171 μs + avg: 103.823 μs + min: 102.973 μs + max: 106.133 μs + std dev: 0.997 μs === morph/symbolic/accum/0 === warmup: 3 iterations - batches: 10 x 2 - total: 202491.620 μs - avg: 10124.581 μs - min: 10011.657 μs - max: 10336.836 μs - std dev: 78.856 μs + batches: 10 x 121 + total: 105704.677 μs + avg: 87.359 μs + min: 87.144 μs + max: 87.909 μs + std dev: 0.218 μs === morph/symbolic/accum/400 === warmup: 3 iterations - batches: 10 x 1 - total: 330874.174 μs - avg: 33087.417 μs - min: 32906.916 μs - max: 33429.534 μs - std dev: 166.375 μs + batches: 10 x 79 + total: 70197.862 μs + avg: 88.858 μs + min: 88.372 μs + max: 89.549 μs + std dev: 0.357 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-10-12 at 16:04, +on 2026-10-13 at 15:50, on Linux with 4 CPUs. @@ -2321,4 +2442,4 @@ [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin [issue-1291]: https://github.com/objectionary/phino/issues/1291 -[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/38274371324 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/38425077680 diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino -version: 0.0.154 +version: 0.0.155 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at @@ -122,6 +122,7 @@ scientific >=0.3.7 && <0.4, text >=2.0.2 && <2.2, time >=1.12 && <1.17, + transformers >=0.6.1 && <0.7, utf8-string >=1.0.2 && <1.1, vector >=0.13.0 && <0.14, xml-conduit >=1.9 && <1.11, diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -37,7 +37,7 @@ import Locator (locatedExpression) import Logger import Morph (ReduceContext (..), insideUniverse) -import Parser (parseExpressionThrows) +import Parser (Form, parseExpressionThrows, parseExpressionThrows') import qualified Printer as P import qualified Random as R import Rewriter (Rewrittens', stepHeaders) @@ -185,16 +185,16 @@ withoutBOM ('\xFEFF' : rest) = rest withoutBOM input = input -parseInput :: String -> IOFormat -> IO Expression -parseInput phi PHI = parseExpressionThrows phi -parseInput xmir XMIR = parseXMIRThrows xmir >>= xmirToPhi -parseInput _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format" +parseInput :: String -> IOFormat -> Form -> IO Expression +parseInput phi PHI form = parseExpressionThrows' form phi +parseInput xmir XMIR _ = parseXMIRThrows xmir >>= xmirToPhi +parseInput _ LATEX _ = invalidCLIArguments "LaTeX cannot be used as input format" -parseInputWithAtoms :: String -> IOFormat -> IO (Expression, Atoms) -parseInputWithAtoms xmir XMIR = do +parseInputWithAtoms :: String -> IOFormat -> Form -> IO (Expression, Atoms) +parseInputWithAtoms xmir XMIR _ = do doc <- parseXMIRThrows xmir (,) <$> xmirToPhi doc <*> xmirAtoms doc -parseInputWithAtoms input format = (,M.empty) <$> parseInput input format +parseInputWithAtoms input format form = (,M.empty) <$> parseInput input format form printRewrittens :: PrintContext -> Rewrittens' -> IO String printRewrittens ctx@PrintCtx{..} rewrittens@(chain, _) diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -14,6 +14,7 @@ import Margin (defaultMargin) import Must import Options.Applicative +import Parser (Form (..)) import Paths_phino (version) import Sugar (SugarType (..)) import Text.Printf (printf) @@ -69,6 +70,9 @@ ("latex", "output") -> Right LATEX _ -> Left (printf "The value '%s' can't be used for '--%s' option, use --help to check possible values" format type') +optMonoform :: Parser Form +optMonoform = flag POLYFORM MONOFORM (long "monoform" <> help "Reject a 𝜑-expression that spells some symbols in ASCII and others in Unicode, such as -> inside ⟦ ⟧") + optOutputFormat :: Parser IOFormat optOutputFormat = option @@ -256,8 +260,10 @@ \it reduces to a normal form under \"morph\", the terms it rewrites by rules of its own under \ \\"rewrite\", the terms of those it stands the data of into unknowns under \"symbolize\" and the \ \pairs of branches it joins into one term under \"join\", whether a join takes a term and a \ - \formation whose φ is that term for one under \"lenient\", the λ functions whose objects a join \ - \takes for a branch that raises under \"terminators\", and answering with the term under \"𝑛\"" + \formation whose φ is that term for one under \"lenient\", whether a lenient join answers a fresh \ + \symbol for a copy one of whose arguments reads to a bare symbol instead of entering it, or for \ + \a copy whose firing a cut refuses, under \"defer\", the λ functions whose objects a join takes for a branch that raises under \ + \\"terminators\", and answering with the term under \"𝑛\"" ) ) @@ -386,6 +392,7 @@ <$> optLogLevel <*> optLogLines <*> optInputFormat + <*> optMonoform <*> optOutputFormat <*> optSugar <*> optHideRho @@ -435,6 +442,7 @@ <$> optLogLevel <*> optLogLines <*> optInputFormat + <*> optMonoform <*> optOutputFormat <*> optSugar <*> optHideRho @@ -484,6 +492,7 @@ <$> optLogLevel <*> optLogLines <*> optInputFormat + <*> optMonoform <*> optOutputFormat <*> optSugar <*> optHideRho @@ -528,6 +537,7 @@ <$> optLogLevel <*> optLogLines <*> optInputFormat + <*> optMonoform <*> option (parseIOFormat "output") (long "output" <> metavar "FORMAT" <> help (printf "Result expression output format (phi, xmir, latex)") <> value PHI <> showDefault) <*> optSugar' <*> optLineFormat' @@ -545,6 +555,7 @@ <$> ( OptsMatch <$> optLogLevel <*> optLogLines + <*> optMonoform <*> optSugar' <*> optLineFormat' <*> optional (strOption (long "pattern" <> metavar "EXPRESSION" <> help "Pattern expression to match against")) diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -64,7 +64,7 @@ linked <- engine validateBreakpoint _breakpoint rules input <- readInput _inputFile - (expr, atoms) <- parseInputWithAtoms input _inputFormat + (expr, atoms) <- parseInputWithAtoms input _inputFormat _monoform validateXmirTopLevel _outputFormat expr seedTaus expr logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth) @@ -171,7 +171,7 @@ [foc] <- validatedDispatches "focus" [_focus] validateNoOverlap "show" included "hide" excluded input <- readInput _inputFile - (expr, atoms) <- parseInputWithAtoms input _inputFormat + (expr, atoms) <- parseInputWithAtoms input _inputFormat _monoform setStdGen (mkStdGen _seed) seedTaus expr let printCtx = toPrintCtx atoms foc @@ -253,7 +253,7 @@ [foc] <- validatedDispatches "focus" [_focus] validateNoOverlap "show" included "hide" excluded input <- readInput _inputFile - (expr, atoms) <- parseInputWithAtoms input _inputFormat + (expr, atoms) <- parseInputWithAtoms input _inputFormat _monoform setStdGen (mkStdGen _seed) seedTaus expr let printCtx = toPrintCtx atoms foc @@ -356,7 +356,7 @@ validateOpts inputs' <- traverse (readInput . Just) _inputs setStdGen (mkStdGen _seed) - (exprs, atoms) <- unzip <$> traverse (`parseInputWithAtoms` _inputFormat) inputs' + (exprs, atoms) <- unzip <$> traverse (\input -> parseInputWithAtoms input _inputFormat _monoform) inputs' expr <- merge exprs validateXmirTopLevel _outputFormat expr let listing = const (escapeXMLText (P.printExpression' expr (_sugarType, UNICODE, _flat, _margin))) @@ -397,7 +397,7 @@ when (isJust _when && isNothing _pattern) (invalidCLIArguments "The option --when requires --pattern, since there is nothing to check it against") setStdGen (mkStdGen _seed) input <- readInput _inputFile - expr <- parseInput input PHI + expr <- parseInput input PHI _monoform if isNothing _pattern then logDebug "The --pattern is not provided, no substitutions are built" else do diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -12,6 +12,7 @@ import Lining (LineFormat) import Logger (LogLevel) import Must (Must) +import Parser (Form) import Sugar (SugarType) import Text.Printf (printf) import XMIR (XmirContext) @@ -94,6 +95,7 @@ { _logLevel :: LogLevel , _logLines :: Int , _inputFormat :: IOFormat + , _monoform :: Form , _outputFormat :: IOFormat , _sugarType :: SugarType , _hideRho :: Bool @@ -140,6 +142,7 @@ { _logLevel :: LogLevel , _logLines :: Int , _inputFormat :: IOFormat + , _monoform :: Form , _outputFormat :: IOFormat , _sugarType :: SugarType , _hideRho :: Bool @@ -199,6 +202,7 @@ { _logLevel :: LogLevel , _logLines :: Int , _inputFormat :: IOFormat + , _monoform :: Form , _outputFormat :: IOFormat , _sugarType :: SugarType , _hideRho :: Bool @@ -240,6 +244,7 @@ { _logLevel :: LogLevel , _logLines :: Int , _inputFormat :: IOFormat + , _monoform :: Form , _outputFormat :: IOFormat , _sugarType :: SugarType , _flat :: LineFormat @@ -254,6 +259,7 @@ data OptsMatch = OptsMatch { _logLevel :: LogLevel , _logLines :: Int + , _monoform :: Form , _sugarType :: SugarType , _flat :: LineFormat , _pattern :: Maybe String diff --git a/src/Deps.hs b/src/Deps.hs --- a/src/Deps.hs +++ b/src/Deps.hs @@ -101,10 +101,11 @@ | EvFiring Int T.Text Judgment Expression | EvStarted Int Judgment Expression | EvDelta Int Bytes - | EvLooped Int Judgment Acyclic Expression Expression + | EvLooped Int Judgment Acyclic Expression Expression (Maybe (Int, Maybe Expression)) | EvStuck Int T.Text Judgment Expression | EvStall Int T.Text | EvStuckOn Int T.Text + | EvUnjoined Int T.Text Expression Expression | EvStarved Int Int Judgment Expression | EvTimeout Int Int Judgment Expression | EvSpent Int Int Judgment Expression @@ -116,6 +117,7 @@ | EvJoined Int Int (Int, Int) | EvTerminate Int (Maybe (Either Int Bytes)) T.Text T.Text (Maybe Expression) | EvMinted Int Int [Either Int Bytes] + | EvDeferred Int Int Judgment Expression (Maybe Expression) Expression | EvApplied Int Judgment Expression Expression Expression | EvBuilt Int Expression | EvAnswer Int Expression @@ -128,10 +130,11 @@ record :: Evaluation -> Evaluation record (EvFiring depth key judgment site) = EvFiring depth key judgment (moved site) record (EvStarted depth judgment site) = EvStarted depth judgment (moved site) - record (EvLooped depth judgment mode self site) = EvLooped depth judgment mode self (moved site) + record (EvLooped depth judgment mode self site answered) = EvLooped depth judgment mode self (moved site) answered record (EvStarved depth limit judgment site) = EvStarved depth limit judgment (moved site) record (EvTimeout depth limit judgment site) = EvTimeout depth limit judgment (moved site) record (EvSpent depth limit judgment site) = EvSpent depth limit judgment (moved site) + record (EvDeferred depth sym judgment copy call site) = EvDeferred depth sym judgment copy call (moved site) record (EvApplied depth judgment call object site) = EvApplied depth judgment call object (moved site) record other = other moved :: Expression -> Expression @@ -149,10 +152,11 @@ tier (EvFiring depth _ _ _) = depth tier (EvStarted depth _ _) = depth tier (EvDelta depth _) = depth -tier (EvLooped depth _ _ _ _) = depth +tier (EvLooped depth _ _ _ _ _) = depth tier (EvStuck depth _ _ _) = depth tier (EvStall depth _) = depth tier (EvStuckOn depth _) = depth +tier (EvUnjoined depth _ _ _) = depth tier (EvStarved depth _ _ _) = depth tier (EvTimeout depth _ _ _) = depth tier (EvSpent depth _ _ _) = depth @@ -164,6 +168,7 @@ tier (EvJoined depth _ _) = depth tier (EvTerminate depth _ _ _ _) = depth tier (EvMinted depth _ _) = depth +tier (EvDeferred depth _ _ _ _ _) = depth tier (EvApplied depth _ _ _ _) = depth tier (EvBuilt depth _) = depth tier (EvAnswer depth _) = depth @@ -306,10 +311,13 @@ naming :: String naming = printf "%s·%d" (labelled protocol sigil) index pure (protocol{_deltas = Map.insert (opener protocol) index protocol._deltas, _found = Just (bytes, naming)}, Just (indented depth (remarked (printf "%s := %s" naming datum) (maybe [] pure (ieee bytes))))) - written (EvLooped depth judgment mode self site) protocol = do + written (EvLooped depth judgment mode self site answered) protocol = do form <- render self remarks <- context protocol judgment site - pure (protocol, Just (indented depth (remarked (printf "looped(%s)" form) (remarks ++ [certainty mode])))) + pure (protocol, Just (indented depth (remarked (printf "looped(%s)%s" form (maybe "" symbolized answered)) (remarks ++ [certainty mode])))) + where + symbolized :: (Int, Maybe Expression) -> String + symbolized (symbol, _) = printf " := %s" (printFunction (FnSymbol symbol)) written (EvStuck depth key judgment self) protocol = do form <- render self pure (protocol, Just (indented depth (printf "unanswered(%s) # %s(%s)" (T.unpack key) (letter judgment) form))) @@ -317,6 +325,10 @@ pure (protocol, Just (indented depth (printf "stall(%s)" (T.unpack key)))) written (EvStuckOn depth key) protocol = pure (protocol, Just (indented depth (printf "stuck(%s)" (T.unpack key)))) + written (EvUnjoined depth key one two) protocol = do + left <- render one + right <- render two + pure (protocol, Just (indented depth (printf "unjoined(%s) # %s vs %s" (T.unpack key) left right))) written (EvStarved depth limit judgment site) protocol = do remarks <- context protocol judgment site pure (protocol, Just (indented depth (remarked (printf "starved(%d)" limit) remarks))) @@ -366,6 +378,10 @@ spelled (Left symbol) = printf "𝔻(%s)" <$> render (standing symbol) spelled (Right bytes) = render (ExBytes bytes) written EvMinted{} protocol = pure (protocol, Nothing) + written (EvDeferred depth symbol judgment copy call site) protocol = do + form <- maybe (render copy) (printed . abbreviatedInside protocol._made) call + remarks <- context protocol judgment site + pure (protocol, Just (indented depth (remarked (printf "deferred(%s) := %s" (printFunction (FnSymbol symbol)) form) remarks))) written (EvApplied depth judgment call object site) protocol = do let (index, counted) = numbered protocol aliased :: Expression @@ -490,11 +506,15 @@ pure $ case inner of (level, opening') : _ | level == depth && opening' == opening -> (nesting{_heads = inner, _pending = pending}, []) _ -> (nesting{_heads = (depth, opening) : dropWhile ((>= depth) . fst) inner, _pending = (depth, opened judgment, opening) : dropWhile (\(level, _, _) -> level >= depth) pending, _closing = kept}, closers) - elements (EvLooped depth judgment mode self site) nesting = do + elements (EvLooped depth judgment mode self site answered) nesting = do form <- render self locator <- located nesting site + (origin, given) <- maybe (pure ("", "")) called (answered >>= snd) let (kept, closers) = closed depth nesting._closing - pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s" (opened judgment) (certainty mode) (escapeXML locator) (escapeXMLText form))]) + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s%s" (maybe "" symbolized answered) (opened judgment) (certainty mode) (escapeXML locator) origin given (escapeXMLText form))]) + where + symbolized :: (Int, Maybe Expression) -> String + symbolized (symbol, _) = printf " symbol=\"%s\"" (sigma symbol) elements (EvStuck depth key judgment self) nesting = do form <- render self let (kept, closers) = closed depth nesting._closing @@ -504,7 +524,12 @@ pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "" (quoted key))]) elements (EvStuckOn depth key) nesting = do let (kept, closers) = closed depth nesting._closing - pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "" (quoted key))]) + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "" (quoted key))]) + elements (EvUnjoined depth key one two) nesting = do + left <- render one + right <- render two + let (kept, closers) = closed depth nesting._closing + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s%s" (quoted key) (escapeXMLText left) (escapeXMLText right))]) elements (EvStarved depth limit judgment site) nesting = do locator <- located nesting site let (kept, closers) = closed depth nesting._closing @@ -581,6 +606,12 @@ spelled :: Either Int Bytes -> IO String spelled (Left fresh) = pure (sigma fresh) spelled (Right bytes) = render (ExBytes bytes) + elements (EvDeferred depth symbol judgment copy call site) nesting = do + form <- render copy + locator <- located nesting site + (origin, given) <- maybe (pure ("", "")) called call + let (kept, closers) = closed depth nesting._closing + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s%s" (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 <- located nesting site @@ -616,6 +647,21 @@ 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 + path <- render object + pure (printf " of=\"%s\"" (escapeXML path), printf "%s" (concat arguments)) + invoked :: Expression -> (Expression, [String]) + invoked (ExApplication term (ArTau attr value)) = + let (object, arguments) = invoked term + in (object, arguments ++ [printf "%s" (escapeXML (printAttribute attr)) (escapeXMLText (valued value))]) + invoked term = (term, []) + valued :: Expression -> String + valued (ExFormation [BiLambda (FnSymbol idx)]) = sigma idx + 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 diff --git a/src/Evaluate.hs b/src/Evaluate.hs --- a/src/Evaluate.hs +++ b/src/Evaluate.hs @@ -1,5 +1,6 @@ {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} {-# OPTIONS_GHC -Wno-name-shadowing #-} -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com @@ -11,16 +12,16 @@ import Builder (buildExpressionThrows) import Control.Exception (throwIO, try) import Control.Monad (foldM, unless) -import Data.IORef (readIORef, writeIORef) +import Data.IORef (atomicModifyIORef', readIORef, writeIORef) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..)) import Data.Maybe (fromMaybe, listToMaybe) import qualified Data.Text as T -import Deps (Evaluation (..), Judgment (Evaluation, Morphing), State (..), resited) +import Deps (Acyclic, Evaluation (..), Judgment (Evaluation, Morphing), State (..), dontSaveEval, dontSaveStep, resited) import Engine (Engine (..)) -import Lambdas (Lambda (..), Meta (..), joined, matched, message, minted, symbolized, thrown) +import Lambdas (Lambda (..), Line (..), Meta (..), emptyLambdas, joined, matched, message, minted, stayed, symbolized, thrown) import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot) -import Morph (Answer, Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), charged, counted, deeper, entering, isLambda, lambda, morphing, normalized, opening, recalled, remember, remembered, retained, settled, starved, unparked) +import Morph (Answer, Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), admitting, boxed, charged, counted, deeper, expired, isLambda, lambda, morphing, normalized, opening, recalled, refused, remember, remembered, retained, settled, starved, unparked) import Printer (printFunction) import Rule (RuleContext (RuleContext), matchExpressionWithRule', xiFree) import Text.Printf (printf) @@ -80,18 +81,21 @@ pure (snd answer, state') Left failure -> do exhausted' <- starved caller._memo - mapM_ (retained caller._memo form stamp) (kept (exhausted' /= exhausted) failure) + mapM_ (retained caller._memo form stamp) (kept (exhausted' /= exhausted) (escaped failure)) mapM_ (caller._saveEval . EvStuckOn (caller._nesting + 1)) (stranded failure) - throwIO failure + throwIO (escaped failure) worked :: ReduceContext -> Lambda -> Firing -> Subst -> State -> IO (Answer, State) worked ctx entry firing@(Firing _ operands _) bound state' = do - (fired, state'') <- foldM (evaluated ctx entry) (bound, state') entry._evaluated - rewrote <- foldM (reshaped ctx) fired entry._rewritten - stood <- foldM (masked ctx) rewrote entry._symbolized - (forked, joining) <- foldM (paired ctx entry (listToMaybe operands)) (stood, state'') entry._paired - (answer, state''') <- answered ctx entry operands forked joining + (lined, state'') <- foldM (line ctx entry (listToMaybe operands)) (bound, state') entry._lines + (answer, state''') <- answered ctx entry operands lined state'' remember caller._memo firing answer pure (answer, state''') + line :: ReduceContext -> Lambda -> Maybe (Either Int Bytes) -> (Subst, State) -> Line -> IO (Subst, State) + line ctx entry _ held (Evaluated meta source) = evaluated ctx entry held meta source + line ctx _ _ (bound, state') (Rewritten meta source rules) = (,state') <$> reshaped ctx bound meta source rules + line ctx _ _ (bound, state') (Stayed meta source) = (,state') <$> trimmed ctx bound meta source + line ctx _ _ (bound, state') (Symbolized meta source) = (,state') <$> masked ctx bound meta source + line ctx entry condition held (Paired meta left right) = paired ctx entry condition held meta left right shown :: Int -> Answer -> IO () shown depth (built, normal) = do caller._saveEval (EvBuilt depth built) @@ -109,6 +113,9 @@ stranded (Stuck name) = Just name stranded (StuckAt name _ _) = Just name stranded _ = Nothing + escaped :: ReduceException -> ReduceException + escaped (Unjoined name) = Stuck name + escaped failure = failure told :: Kept -> IO (Expression, State) told (Answered answer) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) @@ -116,7 +123,7 @@ pure (snd answer, state) told (Looped term) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) - mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site)) caller._acyclic + mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site Nothing)) caller._acyclic throwIO (Looping term) told (Stalled name _) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) @@ -140,39 +147,51 @@ ctx._saveEval (EvTerm ctx._nesting meta._spelling Morphing term normal) bound' <- bind meta (MvExpression normal) bound pure (bound', state'', normal : normals) - evaluated :: ReduceContext -> Lambda -> (Subst, State) -> (Meta, Meta) -> IO (Subst, State) - evaluated ctx entry (bound, state') (meta, source) = do + evaluated :: ReduceContext -> Lambda -> (Subst, State) -> Meta -> Meta -> IO (Subst, State) + evaluated ctx entry (bound, state') meta source = do term <- buildExpressionThrows (ExMeta source._name) bound - (answer, state'') <- fire ctx entry source state' term + (answer, state'') <- fire refused ctx entry source state' term ctx._saveEval (EvTerm ctx._nesting meta._spelling Evaluation (ExMeta source._name) answer) bound' <- bind meta (MvExpression answer) bound pure (bound', state'') - fire :: ReduceContext -> Lambda -> Meta -> State -> Expression -> IO (Expression, State) - fire _ entry _ state' term + fire :: (Expression -> ReduceContext -> (Acyclic, Expression) -> IO Expression) -> ReduceContext -> Lambda -> Meta -> State -> Expression -> IO (Expression, State) + fire _ _ entry _ state' term | raising entry term = pure (term, state') - fire ctx _ source state' term@(ExFormation _) = do - entered <- deeper =<< entering term ctx{_judgment = Evaluation, _site = ExMeta source._name} - evaluation entered state' term univ - fire _ _ _ _ _ = throwIO (Stuck func) - reshaped :: ReduceContext -> Subst -> (Meta, (Meta, [Y.Rule])) -> IO Subst - reshaped ctx bound (meta, (source, rules)) = do + fire cut ctx _ source state' term@(ExFormation _) = do + let firing = ctx{_judgment = Evaluation, _site = ExMeta source._name} + admission <- admitting term firing + case admission of + Left refusal -> do + answer <- cut term firing refusal + pure (answer, state') + Right admitted -> do + entered <- deeper admitted + evaluation entered state' term univ + fire _ _ _ _ _ _ = throwIO (Stuck func) + reshaped :: ReduceContext -> Subst -> Meta -> Meta -> [Y.Rule] -> IO Subst + reshaped ctx bound meta source rules = do term <- buildExpressionThrows (ExMeta source._name) bound shaped <- rewritten rules (RuleContext ctx._buildTerm Nothing ctx._engine._normal) term ctx._saveEval (EvSymbolize ctx._nesting meta._spelling (ExMeta source._name) shaped) bind meta (MvExpression shaped) bound - masked :: ReduceContext -> Subst -> (Meta, Expression) -> IO Subst - masked ctx bound (meta, term) = do - reduced <- buildExpressionThrows term bound + trimmed :: ReduceContext -> Subst -> Meta -> Meta -> IO Subst + trimmed ctx bound meta source = do + term <- stayed <$> buildExpressionThrows (ExMeta source._name) bound + ctx._saveEval (EvSymbolize ctx._nesting meta._spelling (ExMeta source._name) term) + bind meta (MvExpression term) bound + masked :: ReduceContext -> Subst -> Meta -> Meta -> IO Subst + masked ctx bound meta source = do + reduced <- buildExpressionThrows (ExMeta source._name) bound (stood, known, spent) <- symbolized reduced <$> readIORef ctx._minted writeIORef ctx._minted spent mapM_ (ctx._saveEval . fact) known - ctx._saveEval (EvSymbolize ctx._nesting meta._spelling term stood) + ctx._saveEval (EvSymbolize ctx._nesting meta._spelling (ExMeta source._name) stood) bind meta (MvExpression stood) bound where fact :: (Int, Bytes) -> Evaluation fact (fresh, bytes) = EvKnown ctx._nesting fresh bytes - paired :: ReduceContext -> Lambda -> Maybe (Either Int Bytes) -> (Subst, State) -> (Meta, (Meta, Meta)) -> IO (Subst, State) - paired ctx entry condition (bound, state') (meta, (left, right)) = do + paired :: ReduceContext -> Lambda -> Maybe (Either Int Bytes) -> (Subst, State) -> Meta -> Meta -> Meta -> IO (Subst, State) + paired ctx entry condition (bound, state') meta left right = do one <- branch left two <- branch right case (raising entry one, raising entry two) of @@ -190,8 +209,12 @@ (one', reducing) <- reduced left one state' (two', state'') <- reduced right two reducing outcome' <- joined entry._lenient one' two' <$> readIORef ctx._minted - maybe (throwIO (Stuck func)) (written state'') outcome' - | otherwise -> throwIO (Stuck func) + maybe (unjoined one' two') (written state'') outcome' + | otherwise -> unjoined one two + unjoined :: Expression -> Expression -> IO a + unjoined one two = do + ctx._saveEval (EvUnjoined ctx._nesting func one two) + throwIO (Unjoined func) written :: State -> (Expression, [(Int, (Int, Int))], Int) -> IO (Subst, State) written state'' (term, made, spent) = do writeIORef ctx._minted spent @@ -200,17 +223,102 @@ bound' <- bind meta (MvExpression term) bound pure (bound', state'') reduced :: Meta -> Expression -> State -> IO (Expression, State) + reduced side term@(ExFormation bds) state'' + | hanging term && entry._defer && copied bds = deferred side bds state'' >>= maybe (entered (severed bds) side term state'') (\answer -> pure (answer, state'')) reduced side term state'' - | hanging term = do - (normal, morphed) <- morphing univ ctx (ExDispatch term AtPhi) state'' - ctx._saveEval (EvTerm ctx._nesting side._spelling Morphing (ExDispatch (ExMeta side._name) AtPhi) normal) - (answer, state''') <- fire ctx entry side morphed normal - ctx._saveEval (EvTerm ctx._nesting side._spelling Evaluation (ExMeta side._name) answer) - pure (answer, state''') + | hanging term = entered refused side term state'' | otherwise = pure (term, state'') + entered :: (Expression -> ReduceContext -> (Acyclic, Expression) -> IO Expression) -> Meta -> Expression -> State -> IO (Expression, State) + entered cut side term state'' = do + (normal, morphed) <- morphing univ ctx (ExDispatch term AtPhi) state'' + ctx._saveEval (EvTerm ctx._nesting side._spelling Morphing (ExDispatch (ExMeta side._name) AtPhi) normal) + (answer, state''') <- fire cut ctx entry side morphed normal + ctx._saveEval (EvTerm ctx._nesting side._spelling Evaluation (ExMeta side._name) answer) + pure (answer, state''') hanging :: Expression -> Bool hanging (ExFormation bds) = not (any isLambda bds) && or [not (xiFree body) | BiTau AtPhi body <- bds] hanging _ = False + copied :: [Binding] -> Bool + copied bds = boxed bds && not (any void bds) && or [not (formed body) | BiTau AtPhi body <- bds] + where + void :: Binding -> Bool + void (BiVoid _) = True + void _ = False + formed :: Expression -> Bool + formed (ExFormation _) = True + formed _ = False + deferred :: Meta -> [Binding] -> State -> IO (Maybe Expression) + deferred side bds state'' = do + known <- mapM resolved bds + if any bare known then Just <$> postponed known else pure Nothing + where + bare :: Binding -> Bool + bare (BiTau attr (ExFormation [BiLambda (FnSymbol _)])) = attr /= AtPhi && attr /= AtRho + bare _ = False + resolved :: Binding -> IO Binding + resolved bd@(BiTau attr body) + | attr /= AtPhi && attr /= AtRho && reducible body = do + placed <- ctx._engine._contextualize body (ExFormation (filter (not . named attr) bds)) + outcome <- try (settled placed univ state'' reading) + case outcome of + Right (sole@(ExFormation [BiLambda (FnSymbol _)]), _) -> pure (BiTau attr sole) + Left (OutOfTime cap) -> expired ctx cap + _ -> pure bd + resolved bd = pure bd + reducible :: Expression -> Bool + reducible (ExDispatch _ _) = True + reducible (ExApplication _ _) = True + reducible _ = False + named :: Attribute -> Binding -> Bool + named attr (BiTau attr' _) = attr == attr' + named _ _ = False + reading :: ReduceContext + reading = ctx{_symbolic = emptyLambdas, _memo = Nothing, _tally = Nothing, _acyclic = Nothing, _saveStep = dontSaveStep, _saveEval = dontSaveEval} + postponed :: [Binding] -> IO Expression + postponed known = do + fresh <- coined + ctx._saveEval (EvDeferred ctx._nesting fresh Morphing (ExFormation known) (called known) (ExDispatch (ExMeta side._name) AtPhi)) + pure (ExFormation [BiLambda (FnSymbol fresh)]) + severed :: [Binding] -> Expression -> ReduceContext -> (Acyclic, Expression) -> IO Expression + severed bds _ firing (mode, before) = do + fresh <- coined + firing._saveEval (EvLooped firing._nesting firing._judgment mode before firing._site (Just (fresh, called bds))) + pure (ExFormation [BiLambda (FnSymbol fresh)]) + coined :: IO Int + coined = atomicModifyIORef' ctx._minted (\count -> (succ count, succ count)) + called :: [Binding] -> Maybe Expression + called known = do + (path, declared) <- origin known + pure (foldl ExApplication path [ArTau attr value | BiTau attr value <- known, attr /= AtRho, BiVoid attr `elem` declared]) + origin :: [Binding] -> Maybe (Expression, [Binding]) + origin known = do + parent <- case filter ((== Just AtRho) . attributeFromBinding) known of + [] -> Just ExRoot + [BiTau AtRho (ExFormation outer)] -> fst <$> origin outer + [BiTau AtRho path] -> Just (erased path) + _ -> Nothing + ExFormation siblings <- located parent (fromMaybe univ ctx._universe) + chosen [(ExDispatch parent attr, declared) | BiTau attr (ExFormation declared) <- siblings, attr /= AtRho, fits declared] + where + fits :: [Binding] -> Bool + fits declared = all (`elem` map attributeFromBinding declared) [attributeFromBinding bd | bd <- known, attributeFromBinding bd /= Just AtRho] + chosen :: [(Expression, [Binding])] -> Maybe (Expression, [Binding]) + chosen [] = Nothing + chosen candidates = case [candidate | candidate <- candidates, agreed candidate == maximum (map agreed candidates)] of + [one] -> Just one + _ -> Nothing + agreed :: (Expression, [Binding]) -> (Int, Int) + agreed (_, declared) = (length [attr | BiTau attr _ <- known, BiVoid attr `elem` declared], length (filter (`elem` declared) known)) + located :: Expression -> Expression -> Maybe Expression + located ExRoot whole = Just whole + located (ExDispatch path attr) whole = case located path whole of + Just (ExFormation siblings) -> listToMaybe [body | BiTau attr' body <- siblings, attr' == attr] + _ -> Nothing + located _ _ = Nothing + erased :: Expression -> Expression + erased (ExApplication target _) = erased target + erased (ExDispatch target attr) = ExDispatch (erased target) attr + erased other = other terminating :: T.Text -> Meta -> Expression -> Expression -> IO (Subst, State) terminating side raised fault term = do ctx._saveEval (EvTerminate ctx._nesting condition side raised._spelling (message fault)) diff --git a/src/Lambdas.hs b/src/Lambdas.hs --- a/src/Lambdas.hs +++ b/src/Lambdas.hs @@ -10,6 +10,7 @@ ( Lambda (..) , LambdaException (..) , Lambdas + , Line (..) , Meta (..) , emptyLambdas , joined @@ -17,6 +18,7 @@ , message , minted , readLambdas + , stayed , symbolized , taken , thrown @@ -26,13 +28,12 @@ import AST import Control.Applicative ((<|>)) import Control.Exception (Exception, throwIO) -import Control.Monad (void) import Data.Aeson (FromJSON (parseJSON), Key, Object, Value (Object), withObject, (.!=), (.:), (.:?)) import Data.Char (isDigit) import Data.List (find, nub, sortOn) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map -import Data.Maybe (listToMaybe) +import Data.Maybe (fromMaybe, listToMaybe) import Data.Text (Text) import qualified Data.Text as T import Data.Text.Encoding (encodeUtf8) @@ -53,15 +54,20 @@ , _name :: Text } +data Line + = Evaluated Meta Meta + | Rewritten Meta Meta [Y.Rule] + | Stayed Meta Meta + | Symbolized Meta Meta + | Paired Meta Meta Meta + data Lambda = Lambda { _key :: Text , _dataized :: [(Meta, Expression)] , _morphed :: [(Meta, Expression)] - , _evaluated :: [(Meta, Meta)] - , _rewritten :: [(Meta, (Meta, [Y.Rule]))] - , _symbolized :: [(Meta, Expression)] - , _paired :: [(Meta, (Meta, Meta))] + , _lines :: [Line] , _lenient :: Bool + , _defer :: Bool , _terminators :: [Text] , _answer :: Expression } @@ -80,20 +86,17 @@ parseJSON = withObject "Lambda" $ \entry -> do key <- entry .:? "λ" >>= maybe (fail "The entry has no 'λ' key") pure answer <- entry .:? "𝑛" >>= maybe (fail "The entry has no '𝑛' key") pure + dataized <- operands key bytesMeta entry "dataize" + morphed <- operands key expressionMeta entry "morph" lambda <- - Lambda key - <$> operands key bytesMeta entry "dataize" - <*> operands key expressionMeta entry "morph" - <*> evaluations entry - <*> rewrites (T.unpack key) entry - <*> operands key expressionMeta entry "symbolize" - <*> pairs (T.unpack key) entry + Lambda key dataized morphed + <$> (written (T.unpack key) entry >>= ordered (T.unpack key) (map (_name . fst) morphed)) <*> entry .:? "lenient" .!= False + <*> entry .:? "defer" .!= False <*> entry .:? "terminators" .!= [] <*> pure answer sigmas (T.unpack key) lambda._answer dataless (T.unpack key) lambda._answer - earlier (T.unpack key) lambda once (T.unpack key) lambda mapM_ (metaless (T.unpack key) "dataize") lambda._dataized mapM_ (metaless (T.unpack key) "morph") lambda._morphed @@ -118,20 +121,27 @@ bytesMeta meta = case parseBytes (T.unpack meta) of Right (BtMeta name) -> pure (Meta meta name) _ -> fail (printf "The operand '%s' is not a bytes meta, such as '𝛿1'" (T.unpack meta)) - evaluations :: Object -> Yaml.Parser [(Meta, Meta)] - evaluations entry = do - mapping <- entry .:? "evaluate" .!= (Map.empty :: Map Text Text) - mapM (\(meta, source) -> (,) <$> expressionMeta meta <*> expressionMeta source) (numbered mapping) - pairs :: String -> Object -> Yaml.Parser [(Meta, (Meta, Meta))] + written :: String -> Object -> Yaml.Parser [Line] + written key entry = + concat + <$> sequence + [ links Evaluated entry "evaluate" + , rewrites key entry + , links Stayed entry "stay" + , links Symbolized entry "symbolize" + , pairs key entry + ] + links :: (Meta -> Meta -> Line) -> Object -> Key -> Yaml.Parser [Line] + links kind entry name = do + mapping <- entry .:? name .!= (Map.empty :: Map Text Text) + mapM (\(meta, source) -> kind <$> expressionMeta meta <*> expressionMeta source) (numbered mapping) + pairs :: String -> Object -> Yaml.Parser [Line] pairs key entry = do mapping <- entry .:? "join" .!= (Map.empty :: Map Text [Text]) mapM joins (numbered mapping) where - joins :: (Text, [Text]) -> Yaml.Parser (Meta, (Meta, Meta)) - joins (meta, [left, right]) = do - named <- expressionMeta meta - branches <- (,) <$> expressionMeta left <*> expressionMeta right - pure (named, branches) + joins :: (Text, [Text]) -> Yaml.Parser Line + joins (meta, [left, right]) = Paired <$> expressionMeta meta <*> expressionMeta left <*> expressionMeta right joins (meta, _) = fail ( printf @@ -139,18 +149,17 @@ (T.unpack meta) key ) - rewrites :: String -> Object -> Yaml.Parser [(Meta, (Meta, [Y.Rule]))] + rewrites :: String -> Object -> Yaml.Parser [Line] rewrites key entry = do mapping <- entry .:? "rewrite" .!= (Map.empty :: Map Text Object) mapM line (numbered mapping) where - line :: (Text, Object) -> Yaml.Parser (Meta, (Meta, [Y.Rule])) + line :: (Text, Object) -> Yaml.Parser Line line (meta, body) = do named <- expressionMeta meta source <- body .: "of" >>= expressionMeta - written <- body .: "rules" - rules <- mapM rule written - pure (named, (source, rules)) + listed <- body .: "rules" + Rewritten named source <$> mapM rule listed rule :: Object -> Yaml.Parser Y.Rule rule body = do result <- body .: "result" @@ -176,36 +185,49 @@ where known :: [Text] known = metas parsed.pattern ++ concatMap (metas . (.meta)) (concat parsed.where_) - earlier :: String -> Lambda -> Yaml.Parser () - earlier key lambda = do - fired <- goSources (map (_name . fst) lambda._morphed) lambda._evaluated - rewrote <- goSources fired [(meta, source) | (meta, (source, _)) <- lambda._rewritten] - stood <- go rewrote lambda._symbolized - void (goJoins stood lambda._paired) + ordered :: String -> [Text] -> [Line] -> Yaml.Parser [Line] + ordered key reduced waiting = mapM_ bound (concatMap sources waiting) >> go reduced waiting where - goSources :: [Text] -> [(Meta, Meta)] -> Yaml.Parser [Text] - goSources reduced [] = pure reduced - goSources reduced ((meta, source) : rest) - | source._name `elem` reduced = goSources (meta._name : reduced) rest - | otherwise = unbound source - go :: [Text] -> [(Meta, Expression)] -> Yaml.Parser [Text] - go reduced [] = pure reduced - go reduced ((meta, term) : rest) = case term of - ExMeta name | name `elem` reduced -> go (meta._name : reduced) rest - _ -> unbound meta - goJoins :: [Text] -> [(Meta, (Meta, Meta))] -> Yaml.Parser [Text] - goJoins reduced [] = pure reduced - goJoins reduced ((meta, (left, right)) : rest) - | all ((`elem` reduced) . _name) [left, right] = goJoins (meta._name : reduced) rest - | otherwise = unbound (if left._name `elem` reduced then right else left) - unbound :: Meta -> Yaml.Parser a - unbound meta = - fail - ( printf - "The operand '%s' of λ function '%s' names no meta bound by 'morph' or by a line above it" - (T.unpack meta._spelling) - key - ) + bound :: Meta -> Yaml.Parser () + bound meta + | meta._name `elem` reduced ++ map (_name . binding) waiting = pure () + | otherwise = + fail + ( printf + "The operand '%s' of λ function '%s' names no meta bound by 'morph' or by any line" + (T.unpack meta._spelling) + key + ) + go :: [Text] -> [Line] -> Yaml.Parser [Line] + go _ [] = pure [] + go known pending@(first : _) = case break (all ((`elem` known) . _name) . sources) pending of + (before, line : after) -> (line :) <$> go ((binding line)._name : known) (before ++ after) + (_, []) -> + fail + ( printf + "The line binding '%s' of λ function '%s' reads the meta it binds, directly or through other lines" + (T.unpack (goCircle [] (binding first))._spelling) + key + ) + where + goCircle :: [Text] -> Meta -> Meta + goCircle seen meta + | meta._name `elem` seen = meta + | otherwise = goCircle (meta._name : seen) (fromMaybe meta (listToMaybe (feeding meta))) + feeding :: Meta -> [Meta] + feeding meta = [source | line <- pending, (binding line)._name == meta._name, source <- sources line, source._name `notElem` known] + sources :: Line -> [Meta] + sources (Evaluated _ source) = [source] + sources (Rewritten _ source _) = [source] + sources (Stayed _ source) = [source] + sources (Symbolized _ source) = [source] + sources (Paired _ left right) = [left, right] + binding :: Line -> Meta + binding (Evaluated meta _) = meta + binding (Rewritten meta _ _) = meta + binding (Stayed meta _) = meta + binding (Symbolized meta _) = meta + binding (Paired meta _ _) = meta sigmas :: String -> Expression -> Yaml.Parser () sigmas key answer = case ([kind | Slot kind _ <- slots answer, kind /= "S"], symbols answer) of ([], []) -> pure () @@ -218,11 +240,7 @@ where bound :: [Text] bound = - map (_spelling . fst) lambda._morphed - ++ map (_spelling . fst) lambda._evaluated - ++ map (_spelling . fst) lambda._rewritten - ++ map (_spelling . fst) lambda._symbolized - ++ map (_spelling . fst) lambda._paired + map (_spelling . fst) lambda._morphed ++ map (_spelling . binding) lambda._lines twice :: [Text] -> [Text] -> Maybe Text twice _ [] = Nothing twice seen (meta : rest) @@ -249,13 +267,11 @@ known = map (_name . fst) lambda._dataized ++ map (_name . fst) lambda._morphed - ++ map (_name . fst) lambda._evaluated - ++ map (_name . fst) lambda._rewritten - ++ map (_name . fst) lambda._symbolized - ++ map (_name . fst) lambda._paired + ++ map (_name . binding) lambda._lines lonely :: String -> Lambda -> Yaml.Parser () lonely key lambda - | lambda._lenient && null lambda._paired = fail (printf "The λ function '%s' is lenient but has no 'join' line to be lenient in" key) + | lambda._lenient && null [meta | Paired meta _ _ <- lambda._lines] = fail (printf "The λ function '%s' is lenient but has no 'join' line to be lenient in" key) + | lambda._defer && not lambda._lenient = fail (printf "The λ function '%s' defers but is not lenient, while only a lenient join may enter a copy" key) | otherwise = pure () dataless :: String -> Expression -> Yaml.Parser () dataless key answer @@ -372,6 +388,29 @@ where fresh :: [Slot] fresh = [slot | slot@(Slot kind _) <- slots answer, kind == "S"] + +stayed :: Expression -> Expression +stayed = goExpr + where + goExpr :: Expression -> Expression + goExpr (ExFormation bds) = ExFormation (map goBinding bds) + goExpr (ExApplication expr arg) = case (goExpr expr, arg) of + (target, ArTau AtRho _) | dispatched target -> target + (target, _) -> ExApplication target (goArgument arg) + goExpr (ExDispatch expr attr) = ExDispatch (goExpr expr) attr + goExpr (ExPhiMeet prefix idx expr) = ExPhiMeet prefix idx (goExpr expr) + goExpr (ExPhiAgain prefix idx expr) = ExPhiAgain prefix idx (goExpr expr) + goExpr expr = expr + goBinding :: Binding -> Binding + goBinding (BiTau attr expr) = BiTau attr (goExpr expr) + goBinding bd = bd + goArgument :: Argument -> Argument + goArgument (ArTau attr expr) = ArTau attr (goExpr expr) + goArgument (ArAlpha alpha expr) = ArAlpha alpha (goExpr expr) + dispatched :: Expression -> Bool + dispatched (ExDispatch _ _) = True + dispatched (ExApplication expr _) = dispatched expr + dispatched _ = False type Minting = (Int, [(Int, Bytes)]) diff --git a/src/Morph.hs b/src/Morph.hs --- a/src/Morph.hs +++ b/src/Morph.hs @@ -1,7 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} @@ -11,7 +10,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Morph (Answer, Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), boxed, charged, counted, deeper, emptyState, enter, entering, execBuildTerm, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, parking, recalled, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where +module Morph (Answer, Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, boxed, charged, counted, deeper, emptyState, enter, entering, execBuildTerm, expired, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where import AST import Builder (buildExpressionThrows, nameIn) @@ -119,6 +118,7 @@ | OutOfTime Int | Stuck T.Text | StuckAt T.Text (NonEmpty Rewritten) State + | Unjoined T.Text | OutOfStepsAt Budget (NonEmpty Rewritten) State | Looping Expression | LoopingAt Expression (NonEmpty Rewritten) State @@ -138,6 +138,7 @@ printf "Evaluation did not finish before reaching the limit of seconds: --max-seconds=%d" limit show (Stuck func) = printf "No entry of --symbolic answers the λ function '%s'" (T.unpack func) show (StuckAt func _ _) = show (Stuck func) + show (Unjoined func) = printf "The λ function '%s' could not join its two branches" (T.unpack func) show (Looping term) = printf "Reduction entered a formation it is already inside: %s" (printExpression term) show (LoopingAt term _ _) = show (Looping term) show (Undataizable ExTermination _) = "dataization reached the terminator ⊥, which signals an error and cannot be dataized" @@ -252,16 +253,24 @@ entering :: Expression -> ReduceContext -> IO ReduceContext entering term ctx = maybe (pure ctx) (`enter` ctx) (entrance ctx._judgment term) +admitting :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext) +admitting term ctx = maybe (pure (Right ctx)) (`admitted` ctx) (entrance ctx._judgment term) + enter :: Expression -> ReduceContext -> IO ReduceContext -enter form ctx = maybe (pure ctx) remembered ctx._acyclic +enter form ctx = admitted form ctx >>= either (refused form ctx) pure + +refused :: Expression -> ReduceContext -> (Acyclic, Expression) -> IO a +refused form ctx (mode, before) = do + ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site Nothing) + throwIO (Looping form) + +admitted :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext) +admitted form ctx = maybe (pure (Right ctx)) remembered ctx._acyclic where - remembered :: Acyclic -> IO ReduceContext + remembered :: Acyclic -> IO (Either (Acyclic, Expression) ReduceContext) remembered mode = - awaited (listToMaybe (drop ctx._maxLoops (filter (repeated mode form) (Map.findWithDefault [] (digest mode form) ctx._entered)))) >>= \case - Just before -> do - ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site) - throwIO (Looping form) - Nothing -> pure ctx{_entered = seenInsert (digest mode form) form ctx._entered} + maybe (Right ctx{_entered = seenInsert (digest mode form) form ctx._entered}) (\before -> Left (mode, before)) + <$> awaited (listToMaybe (drop ctx._maxLoops (filter (repeated mode form) (Map.findWithDefault [] (digest mode form) ctx._entered)))) awaited :: Maybe Expression -> IO (Maybe Expression) awaited found = case ctx._deadline of Nothing -> pure found diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -6,7 +6,10 @@ module Parser ( parseExpression + , parseExpression' , parseExpressionThrows + , parseExpressionThrows' + , Form (..) , parseAttribute , parseAttributeThrows , ParserException (..) @@ -25,6 +28,7 @@ import Bytes (nonFiniteBts, nonFiniteOf, numToBts, strToBts) import Control.Exception (Exception) import Control.Monad (guard, when) +import Control.Monad.Trans.State.Strict (StateT, evalStateT, get, put) import Data.Char (isAsciiLower, isAsciiUpper, isDigit) import Data.Scientific (scientific, toRealFloat) import qualified Data.Set as Set @@ -38,8 +42,16 @@ import qualified Text.Megaparsec.Char.Lexer as L import Text.Printf (printf) -type Parser = Parsec Void String +data Form = MONOFORM | POLYFORM + deriving (Eq, Show) +data Script = Ascii | Unicode + deriving (Eq) + +data Style = Free | Open | Fixed Script String SourcePos + +type Parser = StateT Style (Parsec Void String) + data ParserException = CouldNotParseExpression {message :: String} | CouldNotParseAttribute {message :: String} @@ -47,16 +59,19 @@ deriving (Exception) data PhiParser = PhiParser - { _attribute :: Parser Attribute - , _alpha :: Parser Alpha - , _index :: Parser (Either Slot T.Text) - , _binding :: Parser Binding - , _expression :: Parser Expression - , _string :: Parser String + { _attribute :: Parsec Void String Attribute + , _alpha :: Parsec Void String Alpha + , _index :: Parsec Void String (Either Slot T.Text) + , _binding :: Parsec Void String Binding + , _expression :: Parsec Void String Expression + , _string :: Parsec Void String String } phiParser :: PhiParser -phiParser = PhiParser attribute alpha indexVar binding expression quotedStr +phiParser = PhiParser (free attribute) (free alpha) (free indexVar) (free binding) (free expression) (free quotedStr) + where + free :: Parser a -> Parsec Void String a + free parser = evalStateT parser Free instance Show ParserException where show CouldNotParseExpression{..} = printf "Couldn't parse given phi expression, cause: %s" message @@ -72,6 +87,34 @@ symbol :: String -> Parser String symbol = L.symbol whiteSpace +twofold :: Parser String -> Parser String -> Parser String +twofold ascii' unicode' = get >>= spelled + where + spelled :: Style -> Parser String + spelled Free = ascii' <|> unicode' + spelled Open = do + pos <- getSourcePos + (script, word) <- written + put (Fixed script word pos) + return word + spelled (Fixed first spelling at) = do + offset <- getOffset + pos <- getSourcePos + (script, word) <- written + when + (script /= first) + ( registerParseError (FancyError offset (Set.singleton (ErrorFail (printf "The %s symbol \"%s\" at %s mixes with the %s \"%s\" at %s, while --monoform is set" (named script) word (place pos) (named first) spelling (place at))))) + >> put Free + ) + return word + written :: Parser (Script, String) + written = ((,) Ascii <$> ascii') <|> ((,) Unicode <$> unicode') + named :: Script -> String + named Ascii = "ASCII" + named Unicode = "Unicode" + place :: SourcePos -> String + place pos = printf "%d:%d" (unPos (sourceLine pos)) (unPos (sourceColumn pos)) + label' :: Parser T.Text label' = lexeme $ do first <- oneOf ['a' .. 'z'] @@ -94,27 +137,19 @@ "function name" delta :: Parser String -delta = - choice - [ symbol "D>" - , symbol "Δ" >> dashedArrow - ] +delta = twofold (symbol "D>") ("Δ ⤍" <$ (symbol "Δ" >> dashedArrow)) lambda :: Parser String -lambda = - choice - [ symbol "L>" - , symbol "λ" >> dashedArrow - ] +lambda = twofold (symbol "L>") ("λ ⤍" <$ (symbol "λ" >> dashedArrow)) dashedArrow :: Parser String dashedArrow = symbol "⤍" arrow :: Parser String -arrow = choice [symbol "->", symbol "↦"] +arrow = twofold (symbol "->") (symbol "↦") global :: Parser String -global = choice [ascii 'Q', symbol "Φ"] +global = twofold (ascii 'Q') (symbol "Φ") ascii :: Char -> Parser String ascii letter = lexeme (try (pure <$> char letter <* notFollowedBy (satisfy named <|> '_' <$ lambdaOf))) @@ -130,11 +165,7 @@ metaVar :: Char -> String -> Parser (Either Slot T.Text) metaVar ch uni = do offset <- getOffset - suf <- - choice - [ char '!' >> char ch >> metaSuffix - , string uni >> metaSuffix - ] + suf <- twofold (['!', ch] <$ (char '!' >> char ch)) (string uni) >> metaSuffix when (suf == "0") (fail (printf "the meta variable '!%c0' is indexed with zero, while indexes start with one" ch)) @@ -318,16 +349,19 @@ deltaHead :: Parser Expression deltaHead = lookAhead (satisfy (\ch -> isDigit ch || ('A' <= ch && ch <= 'F') || ch `elem` ("-!𝛿" :: String))) - >> alone (try (BiDelta <$> bytes <* colon <* choice [symbol "D", symbol "Δ"])) + >> alone (try (BiDelta <$> bytes <* colon <* twofold (symbol "D") (symbol "Δ"))) lambdaHead :: Parser Expression lambdaHead = lookAhead (satisfy (\ch -> isAsciiUpper ch || ch `elem` ("!𝑓𝜎" :: String))) - >> alone (try (BiLambda <$> lambdaName <* colon <* choice [symbol "L", symbol "λ"])) + >> alone (try (BiLambda <$> lambdaName <* colon <* twofold (symbol "L") (symbol "λ"))) voidHead :: Parser Expression -voidHead = alone (choice [symbol "?", symbol "∅"] >> colon >> BiVoid <$> attribute) +voidHead = alone (vacant >> colon >> BiVoid <$> attribute) +vacant :: Parser String +vacant = twofold (symbol "?") (symbol "∅") + metaBinding :: Parser Binding metaBinding = either BiAny BiMeta <$> metaVar 'B' "𝐵" @@ -351,17 +385,17 @@ "binding" where blank :: Parser String - blank = arrow >> choice [symbol "?", symbol "∅"] <* notFollowedBy colon + blank = arrow >> vacant <* notFollowedBy colon void' :: Parser Attribute void' = choice [ AtLabel <$> label' , do - _ <- choice [symbol "^", symbol "ρ"] + _ <- twofold (symbol "^") (symbol "ρ") return AtRho , do - _ <- choice [symbol "@", symbol "φ"] + _ <- twofold (symbol "@") (symbol "φ") return AtPhi ] @@ -378,7 +412,7 @@ alpha :: Parser Alpha alpha = do - _ <- choice [symbol "~", symbol "α"] + _ <- twofold (symbol "~") (symbol "α") choice [ lexeme L.decimal >>= ranged , either AlAny AlMeta <$> indexVar @@ -416,7 +450,7 @@ formationBindingsOffsets :: Parser [(Int, Binding)] formationBindingsOffsets = do - _ <- choice [symbol "[[", symbol "⟦"] + _ <- twofold (symbol "[[") (symbol "⟦") choice [ rsb >> return [] , do @@ -425,7 +459,7 @@ ] where rsb :: Parser String - rsb = choice [symbol "]]", symbol "⟧"] + rsb = twofold (symbol "]]") (symbol "⟧") formationBindings :: Parser [Binding] formationBindings = formationBindingsOffsets >>= reportDuplicates @@ -435,11 +469,11 @@ choice [ ExFormation <$> formationBindings , do - _ <- choice [symbol "$", symbol "ξ"] + _ <- twofold (symbol "$") (symbol "ξ") return ExXi , root , do - _ <- choice [ascii 'T', symbol "⊥"] + _ <- twofold (ascii 'T') (symbol "⊥") return ExTermination , lexeme (DataString . strToBts <$> quotedStr) , deltaHead @@ -500,11 +534,14 @@ parse' name parser input = do let parsed = runParser - ( do - _ <- whiteSpace - p <- parser - _ <- eof - return p + ( evalStateT + ( do + _ <- whiteSpace + p <- parser + _ <- eof + return p + ) + Free ) name input @@ -537,7 +574,14 @@ parseAttributeThrows attr = orThrow CouldNotParseAttribute (parseAttribute attr) parseExpression :: String -> Either String Expression -parseExpression = parse' "expression" expression +parseExpression = parseExpression' POLYFORM +parseExpression' :: Form -> String -> Either String Expression +parseExpression' MONOFORM = parse' "expression" (put Open >> expression) +parseExpression' POLYFORM = parse' "expression" expression + parseExpressionThrows :: String -> IO Expression -parseExpressionThrows ex = orThrow CouldNotParseExpression (parseExpression ex) +parseExpressionThrows = parseExpressionThrows' POLYFORM + +parseExpressionThrows' :: Form -> String -> IO Expression +parseExpressionThrows' form ex = orThrow CouldNotParseExpression (parseExpression' form ex) diff --git a/test-resources/condition-packs/domain-meta-missing.yaml b/test-resources/condition-packs/domain-meta-missing.yaml --- a/test-resources/condition-packs/domain-meta-missing.yaml +++ b/test-resources/condition-packs/domain-meta-missing.yaml @@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT --- -expression: '[[ x -> $, w -> $ ]](α0 -> Q)' +expression: '[[ x -> $, w -> $ ]](~0 -> Q)' pattern: '[[ !B1 ]](α𝑖1 ↦ Q)' condition: not: diff --git a/test-resources/condition-packs/eq-with-attributes.yaml b/test-resources/condition-packs/eq-with-attributes.yaml --- a/test-resources/condition-packs/eq-with-attributes.yaml +++ b/test-resources/condition-packs/eq-with-attributes.yaml @@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT --- -expression: '[[ x -> Φ.hone.o-filter ]]' +expression: '[[ x -> Q.hone.o-filter ]]' pattern: '[[ x -> Q.hone.𝜏-filter ]]' condition: or: diff --git a/test-resources/condition-packs/gt-domain.yaml b/test-resources/condition-packs/gt-domain.yaml --- a/test-resources/condition-packs/gt-domain.yaml +++ b/test-resources/condition-packs/gt-domain.yaml @@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT --- -expression: '[[ x -> $, w -> $ ]](α0 -> Q)' +expression: '[[ x -> $, w -> $ ]](~0 -> Q)' pattern: '[[ !B1 ]](α𝑖1 ↦ Q)' condition: gt: diff --git a/test-resources/condition-packs/nf-dot-recursive.yaml b/test-resources/condition-packs/nf-dot-recursive.yaml --- a/test-resources/condition-packs/nf-dot-recursive.yaml +++ b/test-resources/condition-packs/nf-dot-recursive.yaml @@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT --- -expression: '⟦ x ↦ [[ t -> ⊥.z ]].t ⟧.x' +expression: '⟦ x ↦ ⟦ t ↦ ⊥.z ⟧.t ⟧.x' pattern: '[[ x -> !e1 ]].x' condition: not: diff --git a/test-resources/condition-packs/not-gt.yaml b/test-resources/condition-packs/not-gt.yaml --- a/test-resources/condition-packs/not-gt.yaml +++ b/test-resources/condition-packs/not-gt.yaml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: MIT --- failure: true -expression: '[[ x -> $, w -> $ ]](α3 -> Q)' +expression: '[[ x -> $, w -> $ ]](~3 -> Q)' pattern: '[[ !B1 ]](α𝑖1 ↦ Q)' condition: gt: diff --git a/test-resources/condition-packs/not-nf-on-dd.yaml b/test-resources/condition-packs/not-nf-on-dd.yaml --- a/test-resources/condition-packs/not-nf-on-dd.yaml +++ b/test-resources/condition-packs/not-nf-on-dd.yaml @@ -1,7 +1,7 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT --- -expression: '[[ x -> ⊥.𝜏1 ]]' +expression: '[[ x -> T.!t1 ]]' pattern: '[[ x -> !e1 ]]' condition: not: diff --git a/test-resources/cst/printing-packs/jeo.yaml b/test-resources/cst/printing-packs/jeo.yaml --- a/test-resources/cst/printing-packs/jeo.yaml +++ b/test-resources/cst/printing-packs/jeo.yaml @@ -3,8 +3,8 @@ # yamllint disable rule:line-length --- expression: | - [[ - x -> Q.x(Φ.jeo.opcode.lconst_0( + ⟦ + x ↦ Φ.x(Φ.jeo.opcode.lconst_0( 9 ), Φ.jeo.opcode.lstore( @@ -25,7 +25,7 @@ ⟧ ) )) - ]] + ⟧ result: |- Φ.x( Φ.jeo.opcode.lconst_0( 9 ), diff --git a/test-resources/dataization-packs/dataizes-the-number-five.yaml b/test-resources/dataization-packs/dataizes-the-number-five.yaml --- a/test-resources/dataization-packs/dataizes-the-number-five.yaml +++ b/test-resources/dataization-packs/dataizes-the-number-five.yaml @@ -6,8 +6,8 @@ location: 'Q.x' input: | [[ - number ↦ ⟦ φ ↦ ∅ ⟧, - bytes ↦ ⟦ φ ↦ ∅ ⟧, + number -> [[ @ -> ? ]], + bytes -> [[ @ -> ? ]], x -> 5 ]] result: '40-14-00-00-00-00-00-00' diff --git a/test-resources/evaluate-packs/answers-a-copy-a-cut-stops-with-a-fresh-symbol-when-deferring.yaml b/test-resources/evaluate-packs/answers-a-copy-a-cut-stops-with-a-fresh-symbol-when-deferring.yaml new file mode 100644 --- /dev/null +++ b/test-resources/evaluate-packs/answers-a-copy-a-cut-stops-with-a-fresh-symbol-when-deferring.yaml @@ -0,0 +1,45 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# yamllint disable rule:line-length +# The cut of #1735 without the walk of --deep: the branch 'b' of the fork is +# the copy 'rec( n ↦ ⟦ φ ↦ 𝜎2 ⟧ )', whose argument reads to no bare symbol, so +# a lenient join enters it, morphs its φ to the same fork and fires it. +# '--acyclic=proven' refuses that firing, since the run is already inside the +# fork. An entry that says 'defer: true' answers the copy with a fresh symbol +# there, writes it on the 'looped' line, and joins it with the symbol the +# other branch holds, instead of losing the whole entry (#1895). +symbolic: | + - λ: L_fork + morph: + 𝑛1: $.a + 𝑛2: $.b + join: + 𝑛3: [𝑛1, 𝑛2] + lenient: true + defer: true + 𝑛: ⟦ φ ↦ 𝑛3 ⟧ +location: 'Q.y' +acyclic: proven +input: '⟦ fork(a, b) ↦ ⟦ λ ⤍ L_fork ⟧, rec(n) ↦ ⟦ φ ↦ Φ.fork( ⟦ λ ⤍ 𝜎1 ⟧, Φ.rec( ξ.n ) ) ⟧, y ↦ Φ.rec( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ).φ.φ ⟧' +result: '𝜎4:λ' +protocol: | + 𝕄(Φ.y): + 𝑛·0·1 := Φ.rec( n ↦ 𝜎2:λ:φ ) + 𝑛·0·2 := Φ.fork( a ↦ 𝜎1:λ ) + 𝑛·0·3 := 𝑛·0·2( b ↦ Φ.rec( 𝜎2:λ:φ ) ) + 𝔼(L_fork): + 𝑛1·1 := 𝜎1:λ # 𝕄(ξ.a) + 𝕄(Φ.a🌵1): + 𝑛·1·1 := Φ.rec( n ↦ 𝜎2:λ:φ ) + 𝑛2·1 := 𝑛·1·1 # 𝕄(ξ.b) + 𝕄(Φ.a🌵2): + 𝑛·1·2 := Φ.fork( a ↦ 𝜎1:λ ) + 𝑛·1·3 := 𝑛·1·2( b ↦ Φ.rec( 𝜎2:λ:φ ) ) + 𝑛2·1 := 𝑛·1·3 # 𝕄(𝑛2.φ) + looped(𝑛·1·3) := 𝜎3 # 𝔼(𝑛2), proven + 𝑛2·1 := 𝜎3:λ # 𝔼(𝑛2) + 𝔻(𝜎4:λ) ∈ { 𝔻(𝜎1:λ), 𝔻(𝜎3:λ) } + 𝑛3·1 := 𝜎4:λ # [𝑛1, 𝑛2] + 𝑛·1·4 := 𝜎4:λ:φ # 𝑛 + 𝑛·1·5 := 𝜎4:λ:φ # 𝕄(𝑛·1·4) diff --git a/test-resources/evaluate-packs/answers-a-symbol-nobody-has-worked-out.yaml b/test-resources/evaluate-packs/answers-a-symbol-nobody-has-worked-out.yaml --- a/test-resources/evaluate-packs/answers-a-symbol-nobody-has-worked-out.yaml +++ b/test-resources/evaluate-packs/answers-a-symbol-nobody-has-worked-out.yaml @@ -16,7 +16,7 @@ input: > ⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.plus( 6 ).φ ⟧ + φ ↦ 5.plus( 6 ).φ ⟧ result: '𝜎1:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/answers-a-whole-family-of-names-with-one-entry.yaml b/test-resources/evaluate-packs/answers-a-whole-family-of-names-with-one-entry.yaml --- a/test-resources/evaluate-packs/answers-a-whole-family-of-names-with-one-entry.yaml +++ b/test-resources/evaluate-packs/answers-a-whole-family-of-names-with-one-entry.yaml @@ -16,7 +16,7 @@ number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧, times(ρ, x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, - @ ↦ 5.plus( 6 ).times( 7 ).φ ⟧ + φ ↦ 5.plus( 6 ).times( 7 ).φ ⟧ result: '𝜎2:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/answers-the-same-under-acyclic.yaml b/test-resources/evaluate-packs/answers-the-same-under-acyclic.yaml --- a/test-resources/evaluate-packs/answers-the-same-under-acyclic.yaml +++ b/test-resources/evaluate-packs/answers-the-same-under-acyclic.yaml @@ -17,7 +17,7 @@ input: > ⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.plus( 6 ).φ ⟧ + φ ↦ 5.plus( 6 ).φ ⟧ result: '𝜎1:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/defers-a-copy-whose-argument-reads-to-a-bare-symbol.yaml b/test-resources/evaluate-packs/defers-a-copy-whose-argument-reads-to-a-bare-symbol.yaml new file mode 100644 --- /dev/null +++ b/test-resources/evaluate-packs/defers-a-copy-whose-argument-reads-to-a-bare-symbol.yaml @@ -0,0 +1,36 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# yamllint disable rule:line-length +# The loop of #1729 without the walk of --deep: the branch 'b' of the fork is +# the copy 'step( tup ↦ Φ.items.tail )', and 'Φ.items.tail' reads to the bare +# symbol '𝜎1', an object nobody knows. A lenient join fails on the copy and +# morphs its φ, which asks '𝜎1' for 'next' and gets stuck. An entry that says +# 'defer: true' does not enter such a copy: it answers it with a fresh symbol, +# writes a 'deferred' line naming the call the copy stands for, and joins that +# symbol with the one the other branch holds (#1892). +symbolic: | + - λ: L_fork + morph: + 𝑛1: $.a + 𝑛2: $.b + join: + 𝑛3: [𝑛1, 𝑛2] + lenient: true + defer: true + 𝑛: ⟦ φ ↦ 𝑛3 ⟧ +location: 'Q.y' +input: '⟦ step(tup) ↦ ⟦ φ ↦ tup.next ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.step( tup ↦ Φ.items.tail ), λ ⤍ L_fork ⟧.φ ⟧' +result: '𝜎4:λ' +protocol: | + 𝕄(Φ.y): + 𝔼(L_fork): + 𝑛1·1 := 𝜎2:λ # 𝕄(ξ.a) + 𝕄(Φ.a🌵1): + 𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail ) + 𝑛2·1 := 𝑛·1·1 # 𝕄(ξ.b) + deferred(𝜎3) := Φ.step( tup ↦ 𝜎1:λ ) # 𝕄(𝑛2.φ) + 𝔻(𝜎4:λ) ∈ { 𝔻(𝜎2:λ), 𝔻(𝜎3:λ) } + 𝑛3·1 := 𝜎4:λ # [𝑛1, 𝑛2] + 𝑛·1·2 := 𝜎4:λ:φ # 𝑛 + 𝑛·1·3 := 𝜎4:λ:φ # 𝕄(𝑛·1·2) diff --git a/test-resources/evaluate-packs/enters-a-copy-whose-argument-reads-to-no-bare-symbol-when-deferring.yaml b/test-resources/evaluate-packs/enters-a-copy-whose-argument-reads-to-no-bare-symbol-when-deferring.yaml new file mode 100644 --- /dev/null +++ b/test-resources/evaluate-packs/enters-a-copy-whose-argument-reads-to-no-bare-symbol-when-deferring.yaml @@ -0,0 +1,35 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# yamllint disable rule:line-length +# An entry that says 'defer: true' defers only a copy one of whose arguments +# reads to a bare symbol (#1892). Here 'Φ.items.tail' reads to an object that +# knows its 'next', so the lenient join enters the copy as it did before +# (#1885): it morphs its φ, fires what it comes to, and joins two symbols. No +# 'deferred' line is written and no symbol is minted for the copy. +symbolic: | + - λ: L_fork + morph: + 𝑛1: $.a + 𝑛2: $.b + join: + 𝑛3: [𝑛1, 𝑛2] + lenient: true + defer: true + 𝑛: ⟦ φ ↦ 𝑛3 ⟧ +location: 'Q.y' +input: '⟦ step(tup) ↦ ⟦ φ ↦ tup.next ⟧, items ↦ ⟦ tail ↦ ⟦ next ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧ ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.step( tup ↦ Φ.items.tail ), λ ⤍ L_fork ⟧.φ ⟧' +result: '𝜎3:λ' +protocol: | + 𝕄(Φ.y): + 𝔼(L_fork): + 𝑛1·1 := 𝜎2:λ # 𝕄(ξ.a) + 𝕄(Φ.a🌵1): + 𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail ) + 𝑛2·1 := 𝑛·1·1 # 𝕄(ξ.b) + 𝑛2·1 := 𝜎1:λ:φ # 𝕄(𝑛2.φ) + 𝑛2·1 := 𝑛2·1 # 𝔼(𝑛2) + 𝔻(𝜎3:λ) ∈ { 𝔻(𝜎2:λ), 𝔻(𝜎1:λ) } + 𝑛3·1 := 𝜎3:λ # [𝑛1, 𝑛2] + 𝑛·1·2 := 𝜎3:λ:φ # 𝑛 + 𝑛·1·3 := 𝜎3:λ:φ # 𝕄(𝑛·1·2) diff --git a/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-one-symbol-when-strict.yaml b/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-one-symbol-when-strict.yaml --- a/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-one-symbol-when-strict.yaml +++ b/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-one-symbol-when-strict.yaml @@ -30,4 +30,4 @@ 𝔼(L_fork): 𝑛1·1 := 𝜎1:λ # 𝕄(ξ.a) 𝑛2·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ ):φ # 𝕄(ξ.b) - stuck(L_fork) + unjoined(L_fork) # 𝜎1:λ vs Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ ⟧ ):φ diff --git a/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-two-symbols-when-lenient.yaml b/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-two-symbols-when-lenient.yaml --- a/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-two-symbols-when-lenient.yaml +++ b/test-resources/evaluate-packs/fails-on-a-bare-symbol-and-a-branch-holding-two-symbols-when-lenient.yaml @@ -31,4 +31,4 @@ 𝔼(L_fork): 𝑛1·1 := 𝜎1:λ # 𝕄(ξ.a) 𝑛2·1 := Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ, was ↦ 𝜎3:λ ⟧ ):φ # 𝕄(ξ.b) - stuck(L_fork) + unjoined(L_fork) # 𝜎1:λ vs Φ.bool( if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎2:λ, was ↦ 𝜎3:λ ⟧ ):φ diff --git a/test-resources/evaluate-packs/fails-on-a-branch-and-a-decorator-of-it-when-strict.yaml b/test-resources/evaluate-packs/fails-on-a-branch-and-a-decorator-of-it-when-strict.yaml --- a/test-resources/evaluate-packs/fails-on-a-branch-and-a-decorator-of-it-when-strict.yaml +++ b/test-resources/evaluate-packs/fails-on-a-branch-and-a-decorator-of-it-when-strict.yaml @@ -22,4 +22,4 @@ 𝔼(L_fork): 𝑛1·1 := ⟦ φ ↦ 𝜎1:λ, neg ↦ ⟦⟧ ⟧ # 𝕄(ξ.a) 𝑛2·1 := ⟦ φ ↦ 𝜎2:λ, neg ↦ ⟦⟧ ⟧:φ # 𝕄(ξ.b) - stuck(L_fork) + unjoined(L_fork) # ⟦ φ ↦ 𝜎1:λ, neg ↦ ⟦⟧ ⟧ vs ⟦ φ ↦ 𝜎2:λ, neg ↦ ⟦⟧ ⟧:φ diff --git a/test-resources/evaluate-packs/fails-on-a-branch-whose-phi-reads-its-own-object-when-strict.yaml b/test-resources/evaluate-packs/fails-on-a-branch-whose-phi-reads-its-own-object-when-strict.yaml --- a/test-resources/evaluate-packs/fails-on-a-branch-whose-phi-reads-its-own-object-when-strict.yaml +++ b/test-resources/evaluate-packs/fails-on-a-branch-whose-phi-reads-its-own-object-when-strict.yaml @@ -24,4 +24,4 @@ 𝔼(L_fork): 𝑛1·1 := ⟦ φ ↦ eq, eq ↦ L_eq:λ ⟧ # 𝕄(ξ.a) 𝑛2·1 := 𝜎1:λ:φ # 𝕄(ξ.b) - stuck(L_fork) + unjoined(L_fork) # ⟦ φ ↦ eq, eq ↦ L_eq:λ ⟧ vs 𝜎1:λ:φ diff --git a/test-resources/evaluate-packs/fails-on-a-copy-whose-argument-reads-to-a-bare-symbol-when-not-deferring.yaml b/test-resources/evaluate-packs/fails-on-a-copy-whose-argument-reads-to-a-bare-symbol-when-not-deferring.yaml new file mode 100644 --- /dev/null +++ b/test-resources/evaluate-packs/fails-on-a-copy-whose-argument-reads-to-a-bare-symbol-when-not-deferring.yaml @@ -0,0 +1,30 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# yamllint disable rule:line-length +# The fork the deferral of #1892 gets through, under a lenient entry that does +# not say 'defer: true'. The lenient join morphs the φ of the copy +# 'step( tup ↦ Φ.items.tail )', which asks the bare symbol '𝜎1' for 'next', +# and the firing gets stuck on that symbol, as it did since '--deep' was gone. +symbolic: | + - λ: L_fork + morph: + 𝑛1: $.a + 𝑛2: $.b + join: + 𝑛3: [𝑛1, 𝑛2] + lenient: true + 𝑛: ⟦ φ ↦ 𝑛3 ⟧ +location: 'Q.y' +input: '⟦ step(tup) ↦ ⟦ φ ↦ tup.next ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.step( tup ↦ Φ.items.tail ), λ ⤍ L_fork ⟧.φ ⟧' +fails: "No entry of --symbolic answers the λ function '𝜎1'" +protocol: | + 𝕄(Φ.y): + 𝔼(L_fork): + 𝑛1·1 := 𝜎2:λ # 𝕄(ξ.a) + 𝕄(Φ.a🌵1): + 𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail ) + 𝑛2·1 := 𝑛·1·1 # 𝕄(ξ.b) + 𝕄(Φ.a🌵2): + unanswered(𝜎1) # 𝕄(𝜎1:λ) + stuck(𝜎1) diff --git a/test-resources/evaluate-packs/fails-on-a-fork-whose-branches-do-not-join.yaml b/test-resources/evaluate-packs/fails-on-a-fork-whose-branches-do-not-join.yaml --- a/test-resources/evaluate-packs/fails-on-a-fork-whose-branches-do-not-join.yaml +++ b/test-resources/evaluate-packs/fails-on-a-fork-whose-branches-do-not-join.yaml @@ -23,4 +23,4 @@ 𝔼(L_fork): 𝑛1·1 := 𝜎1:λ:l # 𝕄(ξ.a) 𝑛2·1 := ⟦ l ↦ 𝜎2:λ, x ↦ ⟦⟧ ⟧ # 𝕄(ξ.b) - stuck(L_fork) + unjoined(L_fork) # 𝜎1:λ:l vs ⟦ l ↦ 𝜎2:λ, x ↦ ⟦⟧ ⟧ diff --git a/test-resources/evaluate-packs/fires-what-a-rewrite-line-unwrapped.yaml b/test-resources/evaluate-packs/fires-what-a-rewrite-line-unwrapped.yaml new file mode 100644 --- /dev/null +++ b/test-resources/evaluate-packs/fires-what-a-rewrite-line-unwrapped.yaml @@ -0,0 +1,37 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# yamllint disable rule:line-length +# The lines of an entry run in the order of the metas they read, not of their +# blocks: the 'evaluate' line fires what the 'rewrite' line unwrapped, so the +# 'rewrite' line runs first, although its block comes later (#1903). +symbolic: | + - λ: L_inner + 𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧ + - λ: L_pick + morph: + 𝑛1: $.x + rewrite: + 𝑛2: + of: 𝑛1 + rules: + - name: unwrap + pattern: ⟦ φ ↦ 𝑒1 ⟧ + result: 𝑒1 + evaluate: + 𝑛3: 𝑛2 + 𝑛: 𝑛3 +location: 'Q.y' +input: '⟦ y ↦ ⟦ x ↦ ⟦ φ ↦ ⟦ λ ⤍ L_inner ⟧ ⟧, λ ⤍ L_pick ⟧.φ ⟧' +result: '𝜎1:λ' +protocol: | + 𝕄(Φ.y): + 𝔼(L_pick): + 𝑛1·1 := L_inner:λ:φ # 𝕄(ξ.x) + 𝑛2·1 := L_inner:λ # 𝑛1 + 𝔼(L_inner): # 𝔼(𝑛2) + 𝑛·2·1 := 𝜎1:λ:φ # 𝑛 + 𝑛·2·2 := 𝜎1:λ:φ # 𝕄(𝑛·2·1) + 𝑛3·1 := 𝑛·2·2 # 𝔼(𝑛2) + 𝑛·1·1 := 𝑛3·1 # 𝑛 + 𝑛·1·2 := 𝑛3·1 # 𝕄(𝑛·1·1) diff --git a/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-raises.yaml b/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-raises.yaml --- a/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-raises.yaml +++ b/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-raises.yaml @@ -37,7 +37,7 @@ number(φ) ↦ ⟦ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.gt( 0 ).if( then ↦ 1.plus( 2 ), else ↦ ⊥ ).plus( 6 ).φ ⟧ + φ ↦ 5.gt( 0 ).if( then ↦ 1.plus( 2 ), else ↦ ⊥ ).plus( 6 ).φ ⟧ result: '𝜎3:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml b/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml --- a/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml +++ b/test-resources/evaluate-packs/joins-a-fork-one-branch-of-which-throws.yaml @@ -41,7 +41,7 @@ number(φ) ↦ ⟦ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.gt( 0 ).if( then ↦ 1.plus( 2 ), else ↦ Φ.error( message ↦ 7.plus( 8 ) ) ).plus( 6 ).φ ⟧ + φ ↦ 5.gt( 0 ).if( then ↦ 1.plus( 2 ), else ↦ Φ.error( message ↦ 7.plus( 8 ) ) ).plus( 6 ).φ ⟧ result: '𝜎3:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/joins-a-fork-that-raises-on-the-left.yaml b/test-resources/evaluate-packs/joins-a-fork-that-raises-on-the-left.yaml --- a/test-resources/evaluate-packs/joins-a-fork-that-raises-on-the-left.yaml +++ b/test-resources/evaluate-packs/joins-a-fork-that-raises-on-the-left.yaml @@ -36,7 +36,7 @@ number(φ) ↦ ⟦ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.gt( 0 ).if( ⊥, 1.plus( 2 ) ).plus( 6 ).φ ⟧ + φ ↦ 5.gt( 0 ).if( ⊥, 1.plus( 2 ) ).plus( 6 ).φ ⟧ result: '𝜎3:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/joins-a-fork-whose-branches-a-stay-brought-to-one-shape.yaml b/test-resources/evaluate-packs/joins-a-fork-whose-branches-a-stay-brought-to-one-shape.yaml new file mode 100644 --- /dev/null +++ b/test-resources/evaluate-packs/joins-a-fork-whose-branches-a-stay-brought-to-one-shape.yaml @@ -0,0 +1,41 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# yamllint disable rule:line-length +# A branch reading the ρ of a copy, the way 'as-number' of EO reads its 'data', +# comes to a dispatch the copy hangs on as its ρ, '( ρ ↦ ⟦ … ⟧ )', while the +# other branch, made of no object, carries no such tail. Both are numbers made +# of one symbol, yet the join compares the terms as written and the tail makes +# their shapes differ. A 'stay' line drops every ρ a dispatch is applied to, +# which 'stay' or 'skip' of normalization drops anyway once the dispatch comes +# to a formation, so the two have one shape and the fork answers their join. +# Each 'stay' line binds a meta of its own, which the protocol writes like a +# 'rewrite' one, commented with the meta it kept; a branch with no tail is +# bound as it was (#1902). +symbolic: | + - λ: L_fork + morph: + 𝑛1: $.a + 𝑛2: $.b + stay: + 𝑛3: 𝑛1 + 𝑛4: 𝑛2 + join: + 𝑛5: [𝑛3, 𝑛4] + 𝑛: 𝑛5 +location: 'Q.y' +hide-rho: false +input: '⟦ number ↦ ⟦ φ ↦ ∅ ⟧, bytes ↦ ⟦ φ ↦ ∅ ⟧, y ↦ ⟦ a ↦ ⟦ φ ↦ Φ.number( φ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), x ↦ ∅ ⟧.ρ ) ⟧, b ↦ ⟦ φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) ) ⟧, λ ⤍ L_fork ⟧.φ ⟧' +result: 'Φ.bytes( φ ↦ 𝜎3:λ ):φ' +protocol: | + 𝕄(Φ.y): + 𝔼(L_fork): + 𝑛1·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ, ρ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ 𝜎1:λ ), x ↦ ∅ ⟧ ) ):φ # 𝕄(ξ.a) + 𝑛2·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ):φ # 𝕄(ξ.b) + 𝑛3·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ):φ # 𝑛1 + 𝑛4·1 := 𝑛2·1 # 𝑛2 + 𝔻(𝜎3:λ) ∈ { 𝔻(𝜎1:λ), 𝔻(𝜎2:λ) } + 𝑛5·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎3:λ ) ):φ # [𝑛3, 𝑛4] + 𝑛·1·1 := 𝑛5·1 # 𝑛 + 𝑛·1·2 := 𝑛5·1 # 𝕄(𝑛·1·1) + 𝑛·0·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎3:λ ) ) diff --git a/test-resources/evaluate-packs/joins-the-branches-a-program-forks-into.yaml b/test-resources/evaluate-packs/joins-the-branches-a-program-forks-into.yaml --- a/test-resources/evaluate-packs/joins-the-branches-a-program-forks-into.yaml +++ b/test-resources/evaluate-packs/joins-the-branches-a-program-forks-into.yaml @@ -41,7 +41,7 @@ number(φ) ↦ ⟦ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.gt( 0 ).if( 1.plus( 2 ), 3.plus( 4 ) ).plus( 6 ).φ ⟧ + φ ↦ 5.gt( 0 ).if( 1.plus( 2 ), 3.plus( 4 ) ).plus( 6 ).φ ⟧ result: '𝜎5:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/mints-a-fresh-symbol-for-every-firing.yaml b/test-resources/evaluate-packs/mints-a-fresh-symbol-for-every-firing.yaml --- a/test-resources/evaluate-packs/mints-a-fresh-symbol-for-every-firing.yaml +++ b/test-resources/evaluate-packs/mints-a-fresh-symbol-for-every-firing.yaml @@ -16,7 +16,7 @@ input: > ⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.plus( 6 ).plus( 7 ).φ ⟧ + φ ↦ 5.plus( 6 ).plus( 7 ).φ ⟧ result: '𝜎2:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/morphs-a-program-that-already-carries-a-symbol.yaml b/test-resources/evaluate-packs/morphs-a-program-that-already-carries-a-symbol.yaml --- a/test-resources/evaluate-packs/morphs-a-program-that-already-carries-a-symbol.yaml +++ b/test-resources/evaluate-packs/morphs-a-program-that-already-carries-a-symbol.yaml @@ -16,7 +16,7 @@ input: > ⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).plus( 7 ).φ ⟧ + φ ↦ Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).plus( 7 ).φ ⟧ result: '𝜎2:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/morphs-two-branches-spelling-one-term-through-one-firing.yaml b/test-resources/evaluate-packs/morphs-two-branches-spelling-one-term-through-one-firing.yaml --- a/test-resources/evaluate-packs/morphs-two-branches-spelling-one-term-through-one-firing.yaml +++ b/test-resources/evaluate-packs/morphs-two-branches-spelling-one-term-through-one-firing.yaml @@ -36,7 +36,7 @@ number(φ) ↦ ⟦ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.gt( 0 ).if( 1.plus( 2 ).plus( 3 ), 1.plus( 2 ).plus( 3 ) ).plus( 9 ) ⟧ + φ ↦ 5.gt( 0 ).if( 1.plus( 2 ).plus( 3 ), 1.plus( 2 ).plus( 3 ) ).plus( 9 ) ⟧ result: '⟦ x ↦ 9, λ ⤍ L_number_plus ⟧' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/nests-the-firing-an-operand-brought-down.yaml b/test-resources/evaluate-packs/nests-the-firing-an-operand-brought-down.yaml --- a/test-resources/evaluate-packs/nests-the-firing-an-operand-brought-down.yaml +++ b/test-resources/evaluate-packs/nests-the-firing-an-operand-brought-down.yaml @@ -18,7 +18,7 @@ input: > ⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.plus( 6.plus( 7 ) ).plus( 8 ) ⟧ + φ ↦ 5.plus( 6.plus( 7 ) ).plus( 8 ) ⟧ protocol: | 𝕄(Φ.φ): 𝑛·0·1 := 5 diff --git a/test-resources/evaluate-packs/parks-a-fork-whose-branches-do-not-join.yaml b/test-resources/evaluate-packs/parks-a-fork-whose-branches-do-not-join.yaml --- a/test-resources/evaluate-packs/parks-a-fork-whose-branches-do-not-join.yaml +++ b/test-resources/evaluate-packs/parks-a-fork-whose-branches-do-not-join.yaml @@ -24,4 +24,4 @@ 𝔼(L_fork): 𝑛1·1 := 𝜎1:λ:l # 𝕄(ξ.a) 𝑛2·1 := ⟦ l ↦ 𝜎2:λ, x ↦ ⟦⟧ ⟧ # 𝕄(ξ.b) - stuck(L_fork) + unjoined(L_fork) # 𝜎1:λ:l vs ⟦ l ↦ 𝜎2:λ, x ↦ ⟦⟧ ⟧ diff --git a/test-resources/evaluate-packs/reduces-the-branches-of-a-fork-through-morphing.yaml b/test-resources/evaluate-packs/reduces-the-branches-of-a-fork-through-morphing.yaml --- a/test-resources/evaluate-packs/reduces-the-branches-of-a-fork-through-morphing.yaml +++ b/test-resources/evaluate-packs/reduces-the-branches-of-a-fork-through-morphing.yaml @@ -37,7 +37,7 @@ number(φ) ↦ ⟦ gt(ρ, x) ↦ ⟦ λ ⤍ L_number_gt ⟧, plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ 5.gt( 0 ).if( 1.plus( 2 ), 3.plus( 4 ) ).φ ⟧ + φ ↦ 5.gt( 0 ).if( 1.plus( 2 ), 3.plus( 4 ) ).φ ⟧ result: '𝜎2:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/starts-minting-after-the-symbols-the-program-carries.yaml b/test-resources/evaluate-packs/starts-minting-after-the-symbols-the-program-carries.yaml --- a/test-resources/evaluate-packs/starts-minting-after-the-symbols-the-program-carries.yaml +++ b/test-resources/evaluate-packs/starts-minting-after-the-symbols-the-program-carries.yaml @@ -16,7 +16,7 @@ ⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, old ↦ ⟦ λ ⤍ 𝜎3 ⟧, - @ ↦ 5.plus( 6 ).φ ⟧ + φ ↦ 5.plus( 6 ).φ ⟧ result: '𝜎4:λ' protocol: | 𝕄(Φ.φ): diff --git a/test-resources/evaluate-packs/stops-an-accumulator-recursion-under-plausible.yaml b/test-resources/evaluate-packs/stops-an-accumulator-recursion-under-plausible.yaml --- a/test-resources/evaluate-packs/stops-an-accumulator-recursion-under-plausible.yaml +++ b/test-resources/evaluate-packs/stops-an-accumulator-recursion-under-plausible.yaml @@ -74,4 +74,4 @@ 𝑛3·1 := 𝜎3:λ # 𝑛1 𝔻(𝜎4:λ) == 00- 𝑛4·1 := 𝑛·1·2( acc ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 𝜎4:λ ) ).φ # 𝑛2 - stuck(L_if) + unjoined(L_if) # 𝜎3:λ vs 𝑛·1·2( acc ↦ Φ.pair( head ↦ 𝜎1:λ, tail ↦ 𝜎4:λ ) ).φ diff --git a/test-resources/evaluate-packs/tells-two-carried-symbols-apart-in-one-firing.yaml b/test-resources/evaluate-packs/tells-two-carried-symbols-apart-in-one-firing.yaml --- a/test-resources/evaluate-packs/tells-two-carried-symbols-apart-in-one-firing.yaml +++ b/test-resources/evaluate-packs/tells-two-carried-symbols-apart-in-one-firing.yaml @@ -15,7 +15,7 @@ input: > ⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ plus(ρ, x) ↦ ⟦ λ ⤍ L_number_plus ⟧ ⟧, - @ ↦ Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ).plus( + φ ↦ Φ.number( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ).plus( Φ.number( φ ↦ ⟦ λ ⤍ 𝜎5 ⟧ ) ).φ ⟧ result: '𝜎6:λ' protocol: | diff --git a/test-resources/evaluate-packs/tells-two-symbols-of-one-datum-apart-between-firings.yaml b/test-resources/evaluate-packs/tells-two-symbols-of-one-datum-apart-between-firings.yaml --- a/test-resources/evaluate-packs/tells-two-symbols-of-one-datum-apart-between-firings.yaml +++ b/test-resources/evaluate-packs/tells-two-symbols-of-one-datum-apart-between-firings.yaml @@ -26,7 +26,7 @@ ⟦ bytes(φ) ↦ ⟦⟧, dataized(target) ↦ L_dataized:λ, pair(x, y) ↦ L_pair:λ, - @ ↦ Φ.pair( + φ ↦ Φ.pair( Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ, Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ ).φ ⟧ result: '⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧' diff --git a/test-resources/evaluate-packs/writes-the-reduced-branches-a-lenient-join-could-not-pair.yaml b/test-resources/evaluate-packs/writes-the-reduced-branches-a-lenient-join-could-not-pair.yaml new file mode 100644 --- /dev/null +++ b/test-resources/evaluate-packs/writes-the-reduced-branches-a-lenient-join-could-not-pair.yaml @@ -0,0 +1,34 @@ +# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com +# SPDX-License-Identifier: MIT +--- +# yamllint disable rule:line-length +# A lenient entry morphs the φ of the branch that reads its own object, fires +# what it comes to and joins once more, but a symbol never joins a datum, so +# the firing gets stuck all the same. The protocol says why: 'unjoined(…)' +# closes the firing in place of the generic 'stuck(…)', and it carries the two +# branches as the last join saw them, the reduced one included (#1900). +symbolic: | + - λ: L_eq + 𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧ + - λ: L_fork + morph: + 𝑛1: $.a + 𝑛2: $.b + join: + 𝑛3: [𝑛1, 𝑛2] + lenient: true + 𝑛: 𝑛3 +location: 'Q.y' +input: '⟦ y ↦ ⟦ a ↦ ⟦ φ ↦ ξ.eq, eq ↦ ⟦ λ ⤍ L_eq ⟧ ⟧, b ↦ ⟦ φ ↦ ⟦ Δ ⤍ 01- ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧' +fails: "No entry of --symbolic answers the λ function 'L_fork'" +protocol: | + 𝕄(Φ.y): + 𝔼(L_fork): + 𝑛1·1 := ⟦ φ ↦ eq, eq ↦ L_eq:λ ⟧ # 𝕄(ξ.a) + 𝑛2·1 := 01-:Δ:φ # 𝕄(ξ.b) + 𝑛1·1 := L_eq:λ # 𝕄(𝑛1.φ) + 𝔼(L_eq): # 𝔼(𝑛1) + 𝑛·2·1 := 𝜎1:λ:φ # 𝑛 + 𝑛·2·2 := 𝜎1:λ:φ # 𝕄(𝑛·2·1) + 𝑛1·1 := 𝑛·2·2 # 𝔼(𝑛1) + unjoined(L_fork) # 𝜎1:λ:φ vs 01-:Δ:φ diff --git a/test-resources/rewriter-packs/basic/alpha-first.yaml b/test-resources/rewriter-packs/basic/alpha-first.yaml --- a/test-resources/rewriter-packs/basic/alpha-first.yaml +++ b/test-resources/rewriter-packs/basic/alpha-first.yaml @@ -6,4 +6,4 @@ input: | [[ x -> ?, y -> [[ ]] ]](~0 -> Q.y) output: |- - ⟦ x ↦ ∅, y -> [[ ]] ⟧(x ↦ Φ.y) + ⟦ x ↦ ∅, y ↦ ⟦ ⟧ ⟧(x ↦ Φ.y) diff --git a/test-resources/rewriter-packs/basic/alpha-fourth.yaml b/test-resources/rewriter-packs/basic/alpha-fourth.yaml --- a/test-resources/rewriter-packs/basic/alpha-fourth.yaml +++ b/test-resources/rewriter-packs/basic/alpha-fourth.yaml @@ -6,4 +6,4 @@ input: | [[ q -> $.y, w -> ?, z -> ?, x -> ?, y -> [[ ]] ]](~3 -> Q.y) output: |- - ⟦ q -> $.y, w -> ?, z -> ?, x -> ?, y -> [[ ]] ⟧(x ↦ Φ.y) + [[ q -> $.y, w -> ?, z -> ?, x -> ?, y -> [[ ]] ]](x -> Q.y) diff --git a/test-resources/rewriter-packs/basic/alpha-second.yaml b/test-resources/rewriter-packs/basic/alpha-second.yaml --- a/test-resources/rewriter-packs/basic/alpha-second.yaml +++ b/test-resources/rewriter-packs/basic/alpha-second.yaml @@ -6,4 +6,4 @@ input: | [[ q -> $.y, x -> ?, y -> [[ ]] ]](~1 -> Q.y) output: |- - ⟦ q -> $.y, x ↦ ∅, y -> [[ ]] ⟧(x ↦ Φ.y) + ⟦ q ↦ ξ.y, x ↦ ∅, y ↦ ⟦ ⟧ ⟧(x ↦ Φ.y) diff --git a/test-resources/rewriter-packs/basic/alpha-skips-delta-asset.yaml b/test-resources/rewriter-packs/basic/alpha-skips-delta-asset.yaml --- a/test-resources/rewriter-packs/basic/alpha-skips-delta-asset.yaml +++ b/test-resources/rewriter-packs/basic/alpha-skips-delta-asset.yaml @@ -6,4 +6,4 @@ input: | [[ D> 42-, x -> ? ]](~0 -> Q.y) output: |- - ⟦ D> 42-, x ↦ ∅ ⟧(x ↦ Φ.y) + ⟦ Δ ⤍ 42-, x ↦ ∅ ⟧(x ↦ Φ.y) diff --git a/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-hits-rho.yaml b/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-hits-rho.yaml --- a/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-hits-rho.yaml +++ b/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-hits-rho.yaml @@ -6,4 +6,4 @@ input: | [[ L> Fn, x -> ? ]](~1 -> Q.y) output: |- - ⟦ L> Fn, x ↦ ∅ ⟧(α1 ↦ Φ.y) + ⟦ λ ⤍ Fn, x ↦ ∅ ⟧(α1 ↦ Φ.y) diff --git a/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-out-of-range.yaml b/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-out-of-range.yaml --- a/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-out-of-range.yaml +++ b/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset-out-of-range.yaml @@ -6,4 +6,4 @@ input: | [[ L> Fn, x -> ? ]](~2 -> Q.y) output: |- - ⟦ L> Fn, x ↦ ∅ ⟧(~2 ↦ Φ.y) + ⟦ λ ⤍ Fn, x ↦ ∅ ⟧(α2 ↦ Φ.y) diff --git a/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset.yaml b/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset.yaml --- a/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset.yaml +++ b/test-resources/rewriter-packs/basic/alpha-skips-lambda-asset.yaml @@ -6,4 +6,4 @@ input: | [[ L> Fn, x -> ? ]](~0 -> Q.y) output: |- - ⟦ L> Fn, x ↦ ∅ ⟧(x ↦ Φ.y) + ⟦ λ ⤍ Fn, x ↦ ∅ ⟧(x ↦ Φ.y) diff --git a/test-resources/rewriter-packs/basic/alpha-stops-at-length.yaml b/test-resources/rewriter-packs/basic/alpha-stops-at-length.yaml --- a/test-resources/rewriter-packs/basic/alpha-stops-at-length.yaml +++ b/test-resources/rewriter-packs/basic/alpha-stops-at-length.yaml @@ -6,4 +6,4 @@ input: | [[ x -> ?, y -> $.x ]](~1 -> Q.y) output: |- - ⟦ x -> ?, y -> $.x ⟧(~1 ↦ Φ.y) + [[ x -> ?, y -> $.x ]](~1 -> Q.y) diff --git a/test-resources/rewriter-packs/basic/dot-with-dd.yaml b/test-resources/rewriter-packs/basic/dot-with-dd.yaml --- a/test-resources/rewriter-packs/basic/dot-with-dd.yaml +++ b/test-resources/rewriter-packs/basic/dot-with-dd.yaml @@ -4,6 +4,6 @@ rules: basic: ['dot'] input: | - [[ t -> ⊥.z ]].t + [[ t -> T.z ]].t output: |- - [[ t -> ⊥.z ]].t + [[ t -> T.z ]].t diff --git a/test-resources/rewriter-packs/custom/attribute-from-string.yaml b/test-resources/rewriter-packs/custom/attribute-from-string.yaml --- a/test-resources/rewriter-packs/custom/attribute-from-string.yaml +++ b/test-resources/rewriter-packs/custom/attribute-from-string.yaml @@ -2,9 +2,9 @@ # SPDX-License-Identifier: MIT --- input: | - ⟦ x -> "foo" ⟧ + ⟦ x ↦ "foo" ⟧ output: |- - ⟦ x -> "foo", foo -> ⟦⟧ ⟧ + ⟦ x ↦ "foo", foo ↦ ⟦⟧ ⟧ rules: custom: - name: attribute from string diff --git a/test-resources/rewriter-packs/custom/desugar-strings.yaml b/test-resources/rewriter-packs/custom/desugar-strings.yaml --- a/test-resources/rewriter-packs/custom/desugar-strings.yaml +++ b/test-resources/rewriter-packs/custom/desugar-strings.yaml @@ -2,13 +2,13 @@ # SPDX-License-Identifier: MIT --- input: | - ⟦ + [[ str -> "hello", ch -> "h", uni -> "\u0001\u0002", empty -> "", new-line -> "h\ne" - ⟧ + ]] output: |- ⟦ str ↦ Φ.string( diff --git a/test-resources/rewriter-packs/custom/desugares-without-match.yaml b/test-resources/rewriter-packs/custom/desugares-without-match.yaml --- a/test-resources/rewriter-packs/custom/desugares-without-match.yaml +++ b/test-resources/rewriter-packs/custom/desugares-without-match.yaml @@ -2,11 +2,11 @@ # SPDX-License-Identifier: MIT --- input: | - [[ + ⟦ foo ↦ ⟦ - x -> 4294967295 + x ↦ 4294967295 ⟧ - ]] + ⟧ output: |- ⟦ foo ↦ ⟦ diff --git a/test-resources/rewriter-packs/custom/desugares.yaml b/test-resources/rewriter-packs/custom/desugares.yaml --- a/test-resources/rewriter-packs/custom/desugares.yaml +++ b/test-resources/rewriter-packs/custom/desugares.yaml @@ -2,11 +2,11 @@ # SPDX-License-Identifier: MIT --- input: | - [[ + ⟦ foo ↦ ⟦ - x -> 4294967295 + x ↦ 4294967295 ⟧ - ]] + ⟧ output: |- ⟦ foo ↦ ⟦ diff --git a/test-resources/rewriter-packs/custom/does-not-fail-on-ambiguous.yaml b/test-resources/rewriter-packs/custom/does-not-fail-on-ambiguous.yaml --- a/test-resources/rewriter-packs/custom/does-not-fail-on-ambiguous.yaml +++ b/test-resources/rewriter-packs/custom/does-not-fail-on-ambiguous.yaml @@ -3,9 +3,9 @@ --- input: '[[ k -> [[ x -> "hello" ]] ]]' output: |- - ⟦ + [[ k -> [[ x -> "hi" ]] - ⟧ + ]] rules: custom: - name: custom diff --git a/test-resources/rewriter-packs/custom/nested-part-of.yaml b/test-resources/rewriter-packs/custom/nested-part-of.yaml --- a/test-resources/rewriter-packs/custom/nested-part-of.yaml +++ b/test-resources/rewriter-packs/custom/nested-part-of.yaml @@ -4,10 +4,10 @@ repeat: 10 input: '[[ x -> Q.y ]]' output: |- - ⟦ - x ↦ Φ.y, + [[ + x -> Q.y, z -> [[ w -> [[ q -> "foo" ]] ]] - ⟧ + ]] rules: custom: - name: nested part of diff --git a/test-resources/rewriter-packs/custom/number.yaml b/test-resources/rewriter-packs/custom/number.yaml --- a/test-resources/rewriter-packs/custom/number.yaml +++ b/test-resources/rewriter-packs/custom/number.yaml @@ -5,7 +5,7 @@ output: |- ⟦ x ↦ 5, - y -> 42.1 + y ↦ 42.1 ⟧ rules: custom: diff --git a/test-resources/rewriter-packs/custom/part-of-after.yaml b/test-resources/rewriter-packs/custom/part-of-after.yaml --- a/test-resources/rewriter-packs/custom/part-of-after.yaml +++ b/test-resources/rewriter-packs/custom/part-of-after.yaml @@ -6,7 +6,7 @@ output: |- ⟦ x ↦ Φ.y, - z -> "hello world" + z ↦ "hello world" ⟧ rules: custom: diff --git a/test-resources/rewriter-packs/custom/part-of.yaml b/test-resources/rewriter-packs/custom/part-of.yaml --- a/test-resources/rewriter-packs/custom/part-of.yaml +++ b/test-resources/rewriter-packs/custom/part-of.yaml @@ -6,7 +6,7 @@ output: |- ⟦ x ↦ Φ.y, - z -> "foo" + z ↦ "foo" ⟧ rules: custom: diff --git a/test-resources/rewriter-packs/custom/random-tau-mints-fresh.yaml b/test-resources/rewriter-packs/custom/random-tau-mints-fresh.yaml --- a/test-resources/rewriter-packs/custom/random-tau-mints-fresh.yaml +++ b/test-resources/rewriter-packs/custom/random-tau-mints-fresh.yaml @@ -2,9 +2,9 @@ # SPDX-License-Identifier: MIT --- input: | - ⟦ x -> "foo" ⟧ + ⟦ x ↦ "foo" ⟧ output: |- - ⟦ x -> "foo", a🌵0 -> ⟦⟧ ⟧ + ⟦ x ↦ "foo", a🌵0 ↦ ⟦⟧ ⟧ rules: custom: - name: append fresh tau diff --git a/test-resources/rewriter-packs/custom/random-tau-skips-program-wide.yaml b/test-resources/rewriter-packs/custom/random-tau-skips-program-wide.yaml --- a/test-resources/rewriter-packs/custom/random-tau-skips-program-wide.yaml +++ b/test-resources/rewriter-packs/custom/random-tau-skips-program-wide.yaml @@ -7,13 +7,13 @@ # must be 'a🌵2'. input: | [[ - used -> [[ a🌵0 -> ⟦⟧, a🌵1 -> ⟦⟧ ]], + used -> [[ a🌵0 -> [[]], a🌵1 -> [[]] ]], target -> [[ x -> "foo" ]] ]] output: |- [[ - used -> [[ a🌵0 -> ⟦⟧, a🌵1 -> ⟦⟧ ]], - target -> [[ x -> "foo", a🌵2 -> ⟦⟧ ]] + used -> [[ a🌵0 -> [[]], a🌵1 -> [[]] ]], + target -> [[ x -> "foo", a🌵2 -> [[]] ]] ]] rules: custom: diff --git a/test-resources/rewriter-packs/custom/sed-with-slashes.yaml b/test-resources/rewriter-packs/custom/sed-with-slashes.yaml --- a/test-resources/rewriter-packs/custom/sed-with-slashes.yaml +++ b/test-resources/rewriter-packs/custom/sed-with-slashes.yaml @@ -13,7 +13,7 @@ x ↦ "java/lang/Integer", y ↦ "invokevirtual", z ↦ "invokestatic", - w -> "java\\/lang\\/Integer" + w ↦ "java\\/lang\\/Integer" ⟧ rules: custom: diff --git a/test-resources/rewriter-packs/custom/string.yaml b/test-resources/rewriter-packs/custom/string.yaml --- a/test-resources/rewriter-packs/custom/string.yaml +++ b/test-resources/rewriter-packs/custom/string.yaml @@ -4,7 +4,7 @@ input: | [[ attr -> 55 ]] output: |- - ⟦ str ↦ "attr", num -> "55" ⟧ + ⟦ str ↦ "attr", num ↦ "55" ⟧ rules: custom: - name: string function diff --git a/test-resources/rewriter-packs/custom/sum.yaml b/test-resources/rewriter-packs/custom/sum.yaml --- a/test-resources/rewriter-packs/custom/sum.yaml +++ b/test-resources/rewriter-packs/custom/sum.yaml @@ -4,7 +4,7 @@ input: '[[ x -> 5, y -> 6 ]]' output: |- ⟦ - z -> 12 + z ↦ 12 ⟧ rules: custom: diff --git a/test-resources/rewriter-packs/custom/with-alpha-index.yaml b/test-resources/rewriter-packs/custom/with-alpha-index.yaml --- a/test-resources/rewriter-packs/custom/with-alpha-index.yaml +++ b/test-resources/rewriter-packs/custom/with-alpha-index.yaml @@ -2,7 +2,7 @@ # SPDX-License-Identifier: MIT --- input: '[[ x -> ? ]](~0 -> Q.y)' -output: '⟦ x ↦ ∅ ⟧(~0 ↦ Φ)' +output: '⟦ x ↦ ∅ ⟧(α0 ↦ Φ)' rules: custom: - name: with-alpha-index diff --git a/test-resources/xmir-parsing-packs/application.yaml b/test-resources/xmir-parsing-packs/application.yaml --- a/test-resources/xmir-parsing-packs/application.yaml +++ b/test-resources/xmir-parsing-packs/application.yaml @@ -16,4 +16,4 @@ -phi: '[[ app -> [[ x -> Q.org.eolang(α0 -> Q.x)(α1 -> Q.y.plus)(arg -> [[ y -> $ ]]) ]] ]]' +phi: '[[ app -> [[ x -> Q.org.eolang(~0 -> Q.x)(~1 -> Q.y.plus)(arg -> [[ y -> $ ]]) ]] ]]' diff --git a/test-resources/xmir-parsing-packs/dispatch-rho.yaml b/test-resources/xmir-parsing-packs/dispatch-rho.yaml --- a/test-resources/xmir-parsing-packs/dispatch-rho.yaml +++ b/test-resources/xmir-parsing-packs/dispatch-rho.yaml @@ -9,4 +9,4 @@ -phi: '[[ app -> [[ x -> Q.ρ ]] ]]' +phi: '[[ app -> [[ x -> Q.^ ]] ]]' diff --git a/test-resources/xmir-parsing-packs/with-phi.yaml b/test-resources/xmir-parsing-packs/with-phi.yaml --- a/test-resources/xmir-parsing-packs/with-phi.yaml +++ b/test-resources/xmir-parsing-packs/with-phi.yaml @@ -7,4 +7,4 @@ -phi: '[[ app -> [[ φ -> $.φ ]] ]]' +phi: '[[ app -> [[ @ -> $.@ ]] ]]' diff --git a/test/CLIHelpersSpec.hs b/test/CLIHelpersSpec.hs --- a/test/CLIHelpersSpec.hs +++ b/test/CLIHelpersSpec.hs @@ -5,7 +5,7 @@ module CLIHelpersSpec (spec) where -import AST (Expression (ExRoot)) +import AST (Attribute (AtLabel), Binding (BiTau), Expression (ExFormation, ExRoot)) import CLI.Helpers (getRules, parseInput, printExpression, readInput) import CLI.Types (IOFormat (LATEX, PHI, XMIR), PrintContext (PrintCtx)) import Control.Exception (SomeException, bracket, try) @@ -15,6 +15,7 @@ import Data.Text.Encoding qualified as TE import Data.Time.Clock.POSIX (getPOSIXTime) import Lining (LineFormat (MULTILINE)) +import Parser (Form (MONOFORM, POLYFORM)) import Sugar (SugarType (SWEET)) import System.Directory (createDirectoryIfMissing, getTemporaryDirectory, removeDirectoryRecursive) import System.FilePath (()) @@ -44,10 +45,15 @@ spec :: Spec spec = do - describe "parseInput" $ + describe "parseInput" $ do it "fails when asked to parse LaTeX as an input format" $ do - result <- try (parseInput "whatever" LATEX) :: IO (Either SomeException Expression) + result <- try (parseInput "whatever" LATEX POLYFORM) :: IO (Either SomeException Expression) result `shouldSatisfy` isLeft + it "fails on a 𝜑-expression mixing ASCII and Unicode symbols under monoform" $ do + result <- try (parseInput "⟦ x -> ? ]]" PHI MONOFORM) :: IO (Either SomeException Expression) + result `shouldSatisfy` isLeft + it "parses a 𝜑-expression mixing ASCII and Unicode symbols without monoform" $ + parseInput "⟦ x -> Q ]]" PHI POLYFORM `shouldReturn` ExFormation [BiTau (AtLabel "x") ExRoot] describe "printExpression" $ forM_ diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -1328,7 +1328,7 @@ testCLISucceeded ["dataize", "--help"] ["Dataize the 𝜑-expression"] it "names every block of a --symbolic entry in its help" $ - testCLISucceeded ["dataize", "--help"] ["\"dataize\"", "\"morph\"", "\"rewrite\"", "\"symbolize\"", "\"join\"", "\"lenient\"", "\"terminators\""] + testCLISucceeded ["dataize", "--help"] ["\"dataize\"", "\"morph\"", "\"rewrite\"", "\"symbolize\"", "\"join\"", "\"lenient\"", "\"defer\"", "\"terminators\""] it "dataizes simple expression" $ withStdin "[[ D> 01- ]]" $ @@ -1853,8 +1853,17 @@ withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_absent ⟧, λ ⤍ L_outer ⟧.φ ⟧" $ testCLISucceeded ["morph", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path - lines records `shouldContain` [" "] + lines records `shouldContain` [" "] + it "writes a fork whose branches do not join to the XML protocol" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withLambdasOf (T.pack "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛3\n") $ \forks -> + withStdin "⟦ y ↦ ⟦ a ↦ ⟦ l ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, b ↦ ⟦ l ↦ ⟦ λ ⤍ 𝜎2 ⟧, x ↦ ⟦⟧ ⟧, λ ⤍ L_fork ⟧.l ⟧" $ + testCLISucceeded ["morph", "--symbolic=" ++ forks, "--locator=Q.y", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" 𝜎1:λ:l⟦ l ↦ 𝜎2:λ, x ↦ ⟦⟧ ⟧"] + it "writes a starved step budget to the XML protocol" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do hClose stream @@ -2906,6 +2915,52 @@ ["morph", "--symbolic=" ++ forks, "--locator=Q.y", "--sweet", "--hide-rho", "--flat"] ["⟦ if(left, right) ↦ ⟦ λ ⤍ L_fork, φ ↦ 𝜎3:λ ⟧, φ ↦ if( FF-:Δ, 00-:Δ ) ⟧"] + describe "a deferring join" $ do + let deferring = T.pack "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛2]\n lenient: true\n defer: true\n 𝑛: ⟦ φ ↦ 𝑛3 ⟧\n" + deferred :: [String] -> String -> IO [String] + deferred options program = + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withLambdasOf deferring $ \forks -> + withStdin program $ + testCLISucceeded (["morph", "--symbolic=" ++ forks, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] ++ options) [] + lines <$> readProtocol path + it "writes the copy it deferred to the XML protocol as a call of the object it was made of" $ do + records <- deferred [] "⟦ step(tup) ↦ ⟦ φ ↦ tup.next ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.step( tup ↦ Φ.items.tail ), λ ⤍ L_fork ⟧.φ ⟧" + records + `shouldBe` [ "" + , "" + , " " + , " 𝜎2:λ" + , " " + , " Φ.items.tail" + , " " + , " 𝑛·1·1" + , " 𝜎1⟦ tup ↦ 𝜎1:λ, φ ↦ tup.next ⟧" + , " 𝜎2 𝜎3" + , " 𝜎4:λ" + , " 𝜎4:λ:φ" + , " 𝜎4:λ:φ" + , " " + , "" + ] + + it "names the object a deferred copy was made of through the formation its ρ holds" $ do + records <- deferred [] "⟦ joined(items) ↦ ⟦ φ ↦ step( tup ↦ items ), step(ρ, tup) ↦ ⟦ φ ↦ tup.next ⟧ ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.joined( items ↦ Φ.items.tail ).φ, λ ⤍ L_fork ⟧.φ ⟧" + records `shouldContain` [" 𝜎1⟦ tup ↦ 𝜎1:λ, φ ↦ tup.next ⟧"] + + it "writes a question mark for an argument of a deferred copy that is no bare symbol" $ do + records <- deferred [] "⟦ box(x, w) ↦ ⟦ φ ↦ x.next ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.box( x ↦ Φ.items.tail, w ↦ ⟦ z ↦ Φ ⟧ ), λ ⤍ L_fork ⟧.φ ⟧" + records `shouldContain` [" 𝜎1?⟦ x ↦ 𝜎1:λ, w ↦ Φ:z, φ ↦ x.next ⟧"] + + it "writes no object for a deferred copy of a formation the world does not declare" $ do + records <- deferred [] "⟦ wrap(v) ↦ ⟦⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ Φ.wrap( v ↦ ⟦ inner(x) ↦ ⟦ φ ↦ x.next ⟧ ⟧ ).v.inner( x ↦ Φ.items.tail ), λ ⤍ L_fork ⟧.φ ⟧" + records `shouldContain` [" ⟦ x ↦ 𝜎1:λ, φ ↦ x.next ⟧"] + + it "writes the copy a cut stopped to the XML protocol with its symbol and the call of the object it was made of" $ do + records <- deferred ["--acyclic=proven"] "⟦ fork(a, b) ↦ ⟦ λ ⤍ L_fork ⟧, rec(n) ↦ ⟦ φ ↦ Φ.fork( ⟦ λ ⤍ 𝜎1 ⟧, Φ.rec( ξ.n ) ) ⟧, y ↦ Φ.rec( ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ).φ.φ ⟧" + records `shouldContain` [" 𝜎2𝑛·1·3"] + describe "--acyclic=plausible" $ do let twins = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], pair(a, b) -> [[ L> L_pair ]], t -> Φ.pair( 7.plus( 5.plus( 6 ) ), 7.plus( 5.plus( 6 ) ) ).φ ]]" pairs = T.pack "- λ: L_number_plus\n dataize:\n 𝛿1: $.ρ\n 𝛿2: $.x\n 𝑛: Φ.number( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )\n- λ: L_pair\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n evaluate:\n 𝑛3: 𝑛1\n 𝑛4: 𝑛2\n 𝑛: ⟦ φ ↦ ⟦ a ↦ 𝑛3, b ↦ 𝑛4 ⟧ ⟧\n" @@ -3373,3 +3428,33 @@ it (desc ++ " renders as " ++ expected) $ show format `shouldBe` expected ) + + describe "--monoform" $ do + forM_ + [ ("rewrite", ["rewrite", "--monoform"]) + , ("dataize", ["dataize", "--monoform"]) + , ("morph", ["morph", "--monoform"]) + , ("match", ["match", "--monoform", "--pattern=[[ !B ]]"]) + ] + ( \(command, args) -> + it (command ++ " rejects a program mixing ASCII and Unicode symbols") $ + withStdin "⟦ x -> ? ]]" $ + testCLIFailed args ["The ASCII symbol \"->\" at 1:5 mixes with the Unicode \"⟦\" at 1:1, while --monoform is set"] + ) + it "merge rejects a program mixing ASCII and Unicode symbols" $ + withTempFileContent "monoformXXXXXX.phi" "⟦ x -> ? ]]" $ \path -> + testCLIFailed ["merge", "--monoform", path] ["The ASCII symbol \"->\" at 1:5 mixes with the Unicode \"⟦\" at 1:1, while --monoform is set"] + forM_ + [ ("rewrite accepts a program spelled in ASCII alone", "[[ x -> ? ]]", ["rewrite", "--monoform"], "⟦ x ↦ ∅ ⟧") + , ("rewrite accepts a program spelled in Unicode alone", "⟦ x ↦ ∅ ⟧", ["rewrite", "--monoform"], "⟦ x ↦ ∅ ⟧") + , ("rewrite accepts a program mixing ASCII and Unicode symbols without --monoform", "⟦ x -> ? ]]", ["rewrite"], "⟦ x ↦ ∅ ⟧") + , ("dataize accepts a program spelled in ASCII alone", "[[ D> 01- ]]", ["dataize", "--monoform"], "01-") + , ("morph accepts a program spelled in ASCII alone", "[[ x -> ? ]]", ["morph", "--monoform"], "⟦ x ↦ ∅ ⟧") + , ("match accepts a program spelled in ASCII alone", "[[ x -> ? ]]", ["match", "--monoform", "--pattern=[[ !B ]]"], "B >> ⟦ x ↦ ∅ ⟧") + ] + (\(desc, input, args, expected) -> it desc (withStdin input (testCLISucceeded args [expected]))) + it "merge accepts programs spelled in ASCII alone" $ + withTempFileContent "monoformXXXXXX.phi" "[[ x -> ? ]]" $ \path -> + testCLISucceeded ["merge", "--monoform", path] ["⟦ x ↦ ∅ ⟧"] + it "rewrite names --monoform in its help" $ + testCLISucceeded ["rewrite", "--help"] ["--monoform"] diff --git a/test/CSTSpec.hs b/test/CSTSpec.hs --- a/test/CSTSpec.hs +++ b/test/CSTSpec.hs @@ -21,7 +21,7 @@ import GHC.Generics (Generic) import Lining (LineFormat (SINGLELINE), withLineFormat) import Margin (defaultMargin, withMargin) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Render (Render (render)) import Sugar import System.FilePath @@ -105,7 +105,7 @@ packs ( \pth -> it (makeRelative resources pth) $ do pack <- cstPack pth - parsed <- parseExpressionThrows (expression pack) + parsed <- parseExpressionThrows' MONOFORM (expression pack) render (withMargin defaultMargin (expressionToCST parsed)) `shouldBe` result pack ) @@ -116,7 +116,7 @@ packs ( \pth -> it (makeRelative resources pth) $ do pack <- cstPack pth - parsed <- parseExpressionThrows (expression pack) + parsed <- parseExpressionThrows' MONOFORM (expression pack) let cst = expressionToCST parsed salty = toSalty cst render salty `shouldBe` result pack @@ -129,7 +129,7 @@ packs ( \pth -> it (makeRelative resources pth) $ do pack <- cstPack pth - parsed <- parseExpressionThrows (expression pack) + parsed <- parseExpressionThrows' MONOFORM (expression pack) let cst = expressionToCST parsed ascii = withMargin defaultMargin (withEncoding ASCII cst) render ascii `shouldBe` result pack @@ -142,7 +142,7 @@ packs ( \pth -> it (makeRelative resources pth) $ do pack <- cstPack pth - parsed <- parseExpressionThrows (expression pack) + parsed <- parseExpressionThrows' MONOFORM (expression pack) let cst = expressionToCST parsed ascii = withLineFormat SINGLELINE cst render ascii `shouldBe` result pack diff --git a/test/CompiledSpec.hs b/test/CompiledSpec.hs --- a/test/CompiledSpec.hs +++ b/test/CompiledSpec.hs @@ -24,7 +24,7 @@ import Lambdas (Lambdas, readLambdas) import Morph (ReduceContext (..), Steps (..), emptyState, morph') import Must (Must (MtDisabled)) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows') import Rewriter (RewriteContext (RewriteContext), rewrite) import Rule (RuleContext (RuleContext), matchExpressionWithRule) import System.Random (StdGen, mkStdGen, randomR) @@ -40,7 +40,7 @@ it "runs the rules phino carries" $ fresh linked `shouldBe` True it "normalizes the term of every rewriter pack into the chain the rules of YAML make" $ do - terms <- allPathsIn "test-resources/rewriter-packs" >>= mapM (Yaml.decodeFileThrow >=> parseExpressionThrows . input) + terms <- allPathsIn "test-resources/rewriter-packs" >>= mapM (Yaml.decodeFileThrow >=> parseExpressionThrows' MONOFORM . input) filterM (\expr -> (/=) <$> chain linked Nothing expr <*> chain yaml Nothing expr) terms `shouldReturn` [] it "normalizes random terms into the chains the rules of YAML make" $ diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -29,7 +29,7 @@ import Lambdas (Lambdas, emptyLambdas, readLambdas) import Matcher (substEmpty) import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm) -import Parser (parseBytes, parseExpressionThrows) +import Parser (Form (MONOFORM), parseBytes, parseExpressionThrows, parseExpressionThrows') import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import System.FilePath (makeRelative) @@ -56,8 +56,8 @@ testDataize :: Lambdas -> FilePath -> Expectation testDataize known pth = do DataizePack{..} <- Decode.decodeFileThrow pth - expr <- parseExpressionThrows (if model == Just True then primitives input else input) - loc <- parseExpressionThrows (fromMaybe "Q" location) + expr <- parseExpressionThrows' MONOFORM (if model == Just True then primitives input else input) + loc <- parseExpressionThrows' MONOFORM (fromMaybe "Q" location) base <- defaultReduceContext loc let ctx = base{_symbolic = if symbolic == Just True then known else emptyLambdas} case (result, fails) of diff --git a/test/DepsSpec.hs b/test/DepsSpec.hs --- a/test/DepsSpec.hs +++ b/test/DepsSpec.hs @@ -11,7 +11,7 @@ import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (isInfixOf, isPrefixOf) import Data.Time.Clock.POSIX (getPOSIXTime) -import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBuilt, EvData, EvDelta, EvFiring, EvLooped, EvRun, EvStarted, EvTerm, EvTerminate), Judgment (Dataization, Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep) +import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBuilt, EvData, EvDeferred, EvDelta, EvFiring, EvLooped, EvRun, EvStarted, EvStuckOn, EvTerm, EvTerminate, EvUnjoined), Judgment (Dataization, Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep) import Fixtures (readUtf8, recorded, recordedXml) import GHC.Clock (getMonotonicTime) import Logger (LogLevel (DEBUG, ERROR, INFO), setLogConfig) @@ -182,8 +182,11 @@ (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvStarted 1 Morphing (ExDispatch ExRoot (AtLabel "w")), EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "w")), EvDelta 1 (BtOne "0B"), EvStarted 1 Morphing (ExDispatch ExRoot (AtLabel "w")), EvApplied 2 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "w"))]) length (filter (== " 𝕄(Φ.w):") (lines written)) `shouldBe` 2 it "keeps the mode of a cut made at the site of its block" $ do - (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation []) ExRoot]) + (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation []) ExRoot Nothing]) last (lines written) `shouldBe` " looped(⟦⟧) # proven" + it "writes the symbol a cut answered a copy with beside the formation it cut" $ do + (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot (Just (13, Nothing))]) + last (lines written) `shouldBe` " looped(Φ:ъ) := 𝜎13 # proven" it "names the block over an answer by the line that built it" $ do (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ф" Dataization ExRoot, EvBuilt 2 (ExDispatch ExRoot (AtLabel "ю")), EvStarted 2 Morphing (ExDispatch ExRoot (AtLabel "ю")), EvApplied 3 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "q") (ExFormation []))) (ExFormation [BiTau (AtLabel "q") (ExFormation [])]) (ExDispatch ExRoot (AtLabel "ю"))]) lines written `shouldContain` [" 𝕄(𝑛·1·1):"] @@ -193,6 +196,15 @@ it "writes no message for a fork that raises with none" $ do (_, written) <- recorded (\record -> mapM_ record [EvFiring 1 "L_ф" Morphing ExRoot, EvTerminate 2 (Just (Right (BtOne "0D"))) "left" "𝑛3" Nothing]) last (lines written) `shouldBe` " terminate(0D-, left) # 𝑛3" + it "writes a deferred copy as the call of the object it was made of" $ do + (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvDeferred 1 9 Morphing (ExFormation [BiTau (AtLabel "щ") (ExFormation [BiLambda (FnSymbol 4)]), BiTau AtPhi (ExDispatch (ExDispatch ExXi (AtLabel "щ")) (AtLabel "й"))]) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "щ") (ExFormation [BiLambda (FnSymbol 4)])))) ExRoot]) + last (lines written) `shouldBe` " deferred(𝜎9) := Φ.ёж( щ ↦ 𝜎4:λ )" + it "writes a deferred copy as it stands when no object of the world made it" $ do + (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvDeferred 1 9 Morphing (ExFormation [BiTau (AtLabel "щ") (ExFormation [BiLambda (FnSymbol 4)]), BiTau AtPhi (ExDispatch (ExDispatch ExXi (AtLabel "щ")) (AtLabel "й"))]) Nothing ExRoot]) + last (lines written) `shouldBe` " deferred(𝜎9) := ⟦ щ ↦ 𝜎4:λ, φ ↦ щ.й ⟧" + it "writes a join that failed with the two branches it could not pair" $ do + (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_щ" Morphing ExRoot, EvUnjoined 2 "L_щ" (ExFormation [BiLambda (FnSymbol 5)]) (ExFormation [BiTau (AtLabel "ю") (ExFormation [BiLambda (FnSymbol 8)]), BiTau (AtLabel "ц") ExRoot])]) + last (lines written) `shouldBe` " unjoined(L_щ) # 𝜎5:λ vs ⟦ ю ↦ 𝜎8:λ, ц ↦ Φ ⟧" describe "saveEvalXml" $ do it "writes an application as an element naming its head and holding its argument" $ do @@ -237,6 +249,18 @@ it "writes the message a fork raises with beside the datum of its condition" $ do (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvTerminate 1 (Just (Right (BtOne "0D"))) "left" "𝑛3" (Just (ExDispatch ExRoot (AtLabel "щука")))]) lines written `shouldContain` [" 0D-"] + it "writes a deferred copy as an element naming its object and the symbols of its arguments" $ do + (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvDeferred 1 9 Morphing (ExFormation [BiTau (AtLabel "щ") (ExFormation [BiLambda (FnSymbol 4)]), BiTau AtPhi (ExDispatch (ExDispatch ExXi (AtLabel "щ")) (AtLabel "й"))]) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "щ") (ExFormation [BiLambda (FnSymbol 4)])))) ExRoot]) + lines written `shouldContain` [" 𝜎4⟦ щ ↦ 𝜎4:λ, φ ↦ щ.й ⟧"] + it "writes a cut that answered a copy as an element naming its symbol, its object and the symbols of its arguments" $ do + (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot (Just (13, Just (ExApplication (ExDispatch ExRoot (AtLabel "ёрш")) (ArTau (AtLabel "ц") (ExFormation [BiLambda (FnSymbol 6)])))))]) + lines written `shouldContain` [" 𝜎6Φ:ъ"] + it "writes a join that failed as an element holding the two branches it could not pair" $ do + (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_щ" Morphing ExRoot, EvUnjoined 2 "L_щ" (ExFormation [BiLambda (FnSymbol 5)]) (ExFormation [BiTau (AtLabel "ю") (ExFormation [BiLambda (FnSymbol 8)]), BiTau (AtLabel "ц") ExRoot])]) + lines written `shouldContain` [" 𝜎5:λ⟦ ю ↦ 𝜎8:λ, ц ↦ Φ ⟧"] + it "writes a stuck firing as an element of the word the text uses" $ do + (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvFiring 1 "L_щ" Morphing ExRoot, EvStuckOn 2 "L_жук"]) + lines written `shouldContain` [" "] describe "perSecond" $ do it "divides the firings by the seconds the run took" $ diff --git a/test/EvaluateSpec.hs b/test/EvaluateSpec.hs --- a/test/EvaluateSpec.hs +++ b/test/EvaluateSpec.hs @@ -27,7 +27,7 @@ import Margin (defaultMargin) import Matcher (substEmpty) import Morph (ReduceContext (..), Steps (..), emptyState, execBuildTerm, memoized, morph, tallied) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows') import Printer (printExpression, printExpression', printExpressionHidingRho') import Sugar (SugarType (SWEET)) import System.FilePath (makeRelative) @@ -56,9 +56,9 @@ testSymbols :: FilePath -> Expectation testSymbols pth = do SymbolPack{..} <- Decode.decodeFileThrow pth - expr <- parseExpressionThrows input + expr <- parseExpressionThrows' MONOFORM input seedTaus expr - loc <- parseExpressionThrows (fromMaybe "Q" location) + loc <- parseExpressionThrows' MONOFORM (fromMaybe "Q" location) let hidden = hideRho /= Just False withLambdasOf (T.pack symbolic) $ \file -> do known <- readLambdas file @@ -86,7 +86,7 @@ Nothing -> do (morphed, _, _) <- morph expr emptyState ctx forM_ result $ \res -> do - expected <- parseExpressionThrows res + expected <- parseExpressionThrows' MONOFORM res spelled hidden morphed `shouldBe` spelled False expected written `shouldBe` protocol where diff --git a/test/FilterSpec.hs b/test/FilterSpec.hs --- a/test/FilterSpec.hs +++ b/test/FilterSpec.hs @@ -17,7 +17,7 @@ import Files (allPathsIn) import Filter qualified as F import GHC.Generics (Generic) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Rewriter (Rewritten) import System.FilePath import Test.Hspec @@ -42,10 +42,10 @@ packs ( \pth -> it (makeRelative resources pth) $ do YamlPack{..} <- yamlPack pth - expr <- parseExpressionThrows expression - included <- traverse parseExpressionThrows shown - excluded <- traverse parseExpressionThrows hidden - res <- parseExpressionThrows result + expr <- parseExpressionThrows' MONOFORM expression + included <- traverse (parseExpressionThrows' MONOFORM) shown + excluded <- traverse (parseExpressionThrows' MONOFORM) hidden + res <- parseExpressionThrows' MONOFORM result [(expr', _)] <- F.include [(expr, Nothing)] included >>= (`F.exclude` excluded) expr' `shouldBe` res ) diff --git a/test/Fixtures.hs b/test/Fixtures.hs --- a/test/Fixtures.hs +++ b/test/Fixtures.hs @@ -83,17 +83,17 @@ unlines [ "[[" , " bytes -> [[" - , " φ -> ?," + , " @ -> ?," , " not -> [[ ^ -> ?, L> L_bytes_not ]]," , " eq -> [[ ^ -> ?, b -> ?, L> L_bytes_eq ]]" , " ]]," , " bool -> [[" - , " φ -> ?," + , " @ -> ?," , " if -> [[ ^ -> ?, then -> ?, else -> ?, L> L_fork ]]" , " ]]," , " number -> [[" - , " φ -> ?," - , " as-bytes -> $.φ," + , " @ -> ?," + , " as-bytes -> $.@," , " plus -> [[ ^ -> ?, x -> ?, L> L_number_plus ]]," , " times -> [[ ^ -> ?, x -> ?, L> L_number_times ]]," , " div -> [[ ^ -> ?, x -> ?, L> L_number_div ]]," diff --git a/test/LaTeXSpec.hs b/test/LaTeXSpec.hs --- a/test/LaTeXSpec.hs +++ b/test/LaTeXSpec.hs @@ -33,7 +33,7 @@ , rewrittensToLatex ) import Lining (LineFormat (MULTILINE)) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import System.FilePath (makeRelative, (<.>), ()) import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldBe, shouldContain) import Yaml qualified as Y @@ -56,7 +56,7 @@ packs ( \pth -> it (makeRelative resources pth) $ do pack <- latexPack pth - parsed <- parseExpressionThrows (expression pack) + parsed <- parseExpressionThrows' MONOFORM (expression pack) expressionToLaTeX parsed defaultLatexContext `shouldBe` result pack ) diff --git a/test/LambdasSpec.hs b/test/LambdasSpec.hs --- a/test/LambdasSpec.hs +++ b/test/LambdasSpec.hs @@ -12,7 +12,7 @@ import Data.List (isInfixOf) import Data.Text qualified as T import Fixtures (withLambdasOf) -import Lambdas (Lambda (..), Lambdas, Meta (..), emptyLambdas, joined, matched, message, minted, readLambdas, symbolized, taken, thrown) +import Lambdas (Lambda (..), Lambdas, Line (..), Meta (..), emptyLambdas, joined, matched, message, minted, readLambdas, stayed, symbolized, taken, thrown) import Parser (parseExpressionThrows) import Test.Hspec @@ -25,26 +25,39 @@ answering :: Lambdas -> T.Text -> Maybe T.Text answering known func = _key <$> matched known func -joins :: Lambdas -> T.Text -> [(T.Text, (T.Text, T.Text))] -joins known func = map spelled (maybe [] _paired (matched known func)) - where - spelled :: (Meta, (Meta, Meta)) -> (T.Text, (T.Text, T.Text)) - spelled (meta, (left, right)) = (_spelling meta, (_spelling left, _spelling right)) +lined :: Lambdas -> T.Text -> [Line] +lined known func = maybe [] _lines (matched known func) -evaluates :: Lambdas -> T.Text -> [(T.Text, T.Text)] -evaluates known func = map spelled (maybe [] _evaluated (matched known func)) +order :: Lambdas -> T.Text -> [T.Text] +order known func = map bound (lined known func) where - spelled :: (Meta, Meta) -> (T.Text, T.Text) - spelled (meta, source) = (_spelling meta, _spelling source) + bound :: Line -> T.Text + bound (Evaluated meta _) = _spelling meta + bound (Rewritten meta _ _) = _spelling meta + bound (Stayed meta _) = _spelling meta + bound (Symbolized meta _) = _spelling meta + bound (Paired meta _ _) = _spelling meta +joins :: Lambdas -> T.Text -> [(T.Text, (T.Text, T.Text))] +joins known func = [(_spelling meta, (_spelling left, _spelling right)) | Paired meta left right <- lined known func] + +fired :: Lambdas -> T.Text -> [(T.Text, T.Text)] +fired known func = [(_spelling meta, _spelling source) | Evaluated meta source <- lined known func] + +stays :: Lambdas -> T.Text -> [(T.Text, T.Text)] +stays known func = [(_spelling meta, _spelling source) | Stayed meta source <- lined known func] + +stood :: Lambdas -> T.Text -> [T.Text] +stood known func = [_spelling meta | Symbolized meta _ <- lined known func] + rewriting :: T.Text -> T.Text rewriting lines' = "- λ: L_fork\n morph:\n 𝑛1: $.a\n rewrite:\n" <> lines' rules :: T.Text rules = " rules:\n - name: no-x\n pattern: ⟦ !B1, x ↦ ⟦⟧, !B2 ⟧\n result: ⟦ !B1, !B2 ⟧\n" -rewrote :: (Meta, (Meta, [a])) -> (T.Text, T.Text, Int) -rewrote (meta, (source, written)) = (_spelling meta, _spelling source, length written) +rewrote :: Lambdas -> T.Text -> [(T.Text, T.Text, Int)] +rewrote known func = [(_spelling meta, _spelling source, length written) | Rewritten meta source written <- lined known func] spec :: Spec spec = do @@ -83,7 +96,7 @@ it "reads a 'symbolize' line that stands the term of line nine as line ten" $ do known <- lambdasOf "- λ: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛9: 𝑛1\n 𝑛10: 𝑛9\n 𝑛: 𝑛10\n" - map (_spelling . fst) (maybe [] _symbolized (matched known "L_pair")) `shouldBe` ["𝑛9", "𝑛10"] + stood known "L_pair" `shouldBe` ["𝑛9", "𝑛10"] it "reads a meta under both the name it is spelled with and the name it binds" $ do known <- lambdasOf "- λ: L_pair\n dataize:\n 𝛿1: $.ρ\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n" @@ -95,11 +108,11 @@ it "reads the operands of 'symbolize' under expression metas" $ do known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.then\n symbolize:\n 𝑛2: 𝑛1\n 𝑛: 𝑛2\n" - map (_spelling . fst) (maybe [] _symbolized (matched known "L_fork")) `shouldBe` ["𝑛2"] + stood known "L_fork" `shouldBe` ["𝑛2"] it "reads a 'symbolize' line standing the term the line above it made" $ do known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.then\n symbolize:\n 𝑛2: 𝑛1\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n" - map (_spelling . fst) (maybe [] _symbolized (matched known "L_fork")) `shouldBe` ["𝑛2", "𝑛3"] + stood known "L_fork" `shouldBe` ["𝑛2", "𝑛3"] it "reads the term an operand is reduced from" $ do known <- lambdasOf "- λ: L_pair\n dataize:\n 𝛿1: $.x\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n" @@ -135,6 +148,14 @@ known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.then\n 𝑛2: $.else\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛3\n" fmap _lenient (matched known "L_fork") `shouldBe` Just False + it "reads a lenient entry that defers a copy reading a bare symbol" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.then\n 𝑛2: $.else\n join:\n 𝑛3: [𝑛1, 𝑛2]\n lenient: true\n defer: true\n 𝑛: 𝑛3\n" + fmap _defer (matched known "L_fork") `shouldBe` Just True + + it "reads a lenient entry saying nothing of deferring as entering every copy" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.then\n 𝑛2: $.else\n join:\n 𝑛3: [𝑛1, 𝑛2]\n lenient: true\n 𝑛: 𝑛3\n" + fmap _defer (matched known "L_fork") `shouldBe` Just False + it "reads the terminators an entry names beside its 'join' block" $ do known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.then\n 𝑛2: $.else\n join:\n 𝑛3: [𝑛1, 𝑛2]\n terminators: [L_throw, L_halt]\n 𝑛: 𝑛3\n" fmap _terminators (matched known "L_fork") `shouldBe` Just ["L_throw", "L_halt"] @@ -149,27 +170,67 @@ it "reads the lines of 'rewrite' with the metas they read and their rules" $ do known <- lambdasOf (rewriting " 𝑛2:\n of: 𝑛1\n" <> rules <> " 𝑛3:\n of: 𝑛2\n" <> rules <> " 𝑛: 𝑛3\n") - map rewrote (maybe [] _rewritten (matched known "L_fork")) `shouldBe` [("𝑛2", "𝑛1", 1), ("𝑛3", "𝑛2", 1)] + rewrote known "L_fork" `shouldBe` [("𝑛2", "𝑛1", 1), ("𝑛3", "𝑛2", 1)] it "reads a 'symbolize' line standing the term a 'rewrite' line made" $ do known <- lambdasOf (rewriting " 𝑛2:\n of: 𝑛1\n" <> rules <> " symbolize:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n") - map (_spelling . fst) (maybe [] _symbolized (matched known "L_fork")) `shouldBe` ["𝑛3"] + stood known "L_fork" `shouldBe` ["𝑛3"] it "reads the metas the lines of 'evaluate' fire" $ do known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n evaluate:\n 𝑛3: 𝑛1\n 𝑛4: 𝑛2\n 𝑛: 𝑛3\n" - evaluates known "L_fork" `shouldBe` [("𝑛3", "𝑛1"), ("𝑛4", "𝑛2")] + fired known "L_fork" `shouldBe` [("𝑛3", "𝑛1"), ("𝑛4", "𝑛2")] it "reads an 'evaluate' line firing what the line above it fired" $ do known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛2: 𝑛1\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n" - evaluates known "L_fork" `shouldBe` [("𝑛2", "𝑛1"), ("𝑛3", "𝑛2")] + fired known "L_fork" `shouldBe` [("𝑛2", "𝑛1"), ("𝑛3", "𝑛2")] it "reads a 'rewrite' line rewriting what an 'evaluate' line fired" $ do known <- lambdasOf ("- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛2: 𝑛1\n rewrite:\n 𝑛3:\n of: 𝑛2\n" <> rules <> " 𝑛: 𝑛3\n") - map rewrote (maybe [] _rewritten (matched known "L_fork")) `shouldBe` [("𝑛3", "𝑛2", 1)] + rewrote known "L_fork" `shouldBe` [("𝑛3", "𝑛2", 1)] + it "reads the metas the lines of 'stay' keep, a line keeping what the line above it kept" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n stay:\n 𝑛2: 𝑛1\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n" + stays known "L_fork" `shouldBe` [("𝑛2", "𝑛1"), ("𝑛3", "𝑛2")] + + it "reads a 'stay' line keeping what a 'rewrite' line made" $ do + known <- lambdasOf (rewriting " 𝑛2:\n of: 𝑛1\n" <> rules <> " stay:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n") + stays known "L_fork" `shouldBe` [("𝑛3", "𝑛2")] + + it "reads a 'symbolize' line standing what a 'stay' line kept" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n stay:\n 𝑛2: 𝑛1\n symbolize:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n" + stood known "L_fork" `shouldBe` ["𝑛3"] + + it "runs a 'rewrite' line before the 'evaluate' line firing what it made" $ do + known <- lambdasOf (rewriting " 𝑛2:\n of: 𝑛1\n" <> rules <> " evaluate:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n") + order known "L_fork" `shouldBe` ["𝑛2", "𝑛3"] + + it "runs a line before the line of its own block reading what it made" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛2: 𝑛3\n 𝑛3: 𝑛1\n 𝑛: 𝑛2\n" + order known "L_fork" `shouldBe` ["𝑛3", "𝑛2"] + + it "runs a 'symbolize' line before the 'rewrite' line rewriting what it stood" $ do + known <- lambdasOf (rewriting " 𝑛3:\n of: 𝑛2\n" <> rules <> " symbolize:\n 𝑛2: 𝑛1\n 𝑛: 𝑛3\n") + order known "L_fork" `shouldBe` ["𝑛2", "𝑛3"] + + it "runs a 'symbolize' line before the 'stay' line keeping what it stood" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n stay:\n 𝑛3: 𝑛2\n symbolize:\n 𝑛2: 𝑛1\n 𝑛: 𝑛3\n" + order known "L_fork" `shouldBe` ["𝑛2", "𝑛3"] + + it "runs a 'join' line before the 'symbolize' line standing what it joined" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n symbolize:\n 𝑛4: 𝑛3\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛4\n" + order known "L_fork" `shouldBe` ["𝑛3", "𝑛4"] + + it "runs the lines no meta orders in the order of their blocks" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛2]\n symbolize:\n 𝑛4: 𝑛1\n stay:\n 𝑛5: 𝑛2\n evaluate:\n 𝑛6: 𝑛1\n 𝑛: 𝑛3\n" + order known "L_fork" `shouldBe` ["𝑛6", "𝑛5", "𝑛4", "𝑛3"] + + it "reads an entry naming no 'stay' block at all" $ do + known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛: 𝑛1\n" + stays known "L_fork" `shouldBe` [] + it "reads an entry naming no 'evaluate' block at all" $ do known <- lambdasOf "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛: 𝑛1\n" - evaluates known "L_fork" `shouldBe` [] + fired known "L_fork" `shouldBe` [] it "reads an entry naming no 'join' block at all" $ do known <- lambdasOf "- λ: L_pair\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n" @@ -201,8 +262,7 @@ , ("an operand of 'morph' which is no expression meta", "- λ: L_pair\n morph:\n 𝛿1: $.x\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "is not an expression meta") , ("an operand of 'symbolize' which is no expression meta", "- λ: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝛿1: 𝑛1\n 𝑛: 𝑛1\n", "is not an expression meta") , ("an operand of 'symbolize' the entry never bound", "- λ: L_pair\n symbolize:\n 𝑛2: 𝑛1\n 𝑛: 𝑛2\n", "names no meta") - , ("an operand of 'symbolize' which is no meta at all", "- λ: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛2: $.x\n 𝑛: 𝑛2\n", "names no meta") - , ("an operand of 'symbolize' standing the term of a line below it", "- λ: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛2: 𝑛3\n 𝑛3: 𝑛1\n 𝑛: 𝑛2\n", "names no meta") + , ("an operand of 'symbolize' which is no meta at all", "- λ: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛2: $.x\n 𝑛: 𝑛2\n", "is not an expression meta") , ("an operand referencing a meta the entry never matched", "- λ: L_pair\n dataize:\n 𝛿1: '!n'\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "cannot be referenced") , ("an answer reading the data its operands came down to", "- λ: L_pair\n dataize:\n 𝛿1: $.ρ\n 𝑛: ⟦ Δ ⤍ 𝛿1 ⟧\n", "reads data") , ("a meta bound by 'morph' and again by 'symbolize'", "- λ: L_pair\n morph:\n 𝑛1: $.x\n symbolize:\n 𝑛1: 𝑛1\n 𝑛: 𝑛1\n", "The meta '𝑛1' of λ function 'L_pair' is bound by more than one line") @@ -212,31 +272,34 @@ , ("a 'join' line joining three metas", "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n 𝑛3: $.c\n join:\n 𝑛4: [𝑛1, 𝑛2, 𝑛3]\n 𝑛: 𝑛4\n", "must join exactly two metas") , ("a 'join' line joining what is no expression meta", "- λ: L_fork\n morph:\n 𝑛1: $.then\n join:\n 𝑛2: [𝑛1, $.else]\n 𝑛: 𝑛2\n", "is not an expression meta") , ("a 'join' line bound to what is no expression meta", "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝛿1: [𝑛1, 𝑛2]\n 𝑛: 𝑛1\n", "is not an expression meta") - , ("a 'join' line joining a meta the entry never bound", "- λ: L_fork\n morph:\n 𝑛1: $.then\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by a line above it") + , ("a 'join' line joining a meta the entry never bound", "- λ: L_fork\n morph:\n 𝑛1: $.then\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by any line") , ("a 'join' line joining a meta that came down to data", "- λ: L_fork\n dataize:\n 𝛿1: $.ρ\n morph:\n 𝑛1: $.then\n join:\n 𝑛2: [𝑛1, 𝛿1]\n 𝑛: 𝑛2\n", "is not an expression meta") - , ("a 'join' line joining what a line below it made", "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛4]\n 𝑛4: [𝑛1, 𝑛2]\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by a line above it") - , ("a 'rewrite' line rewriting a meta the entry never bound", rewriting " 𝑛2:\n of: 𝑛5\n" <> rules <> " 𝑛: 𝑛2\n", "names no meta bound by 'morph' or by a line above it") - , ("a 'rewrite' line rewriting what a line below it made", rewriting " 𝑛2:\n of: 𝑛3\n" <> rules <> " 𝑛3:\n of: 𝑛1\n" <> rules <> " 𝑛: 𝑛2\n", "names no meta bound by 'morph' or by a line above it") - , ("a 'rewrite' line rewriting what a 'symbolize' line made", rewriting " 𝑛3:\n of: 𝑛2\n" <> rules <> " symbolize:\n 𝑛2: 𝑛1\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by a line above it") + , ("a 'rewrite' line rewriting a meta the entry never bound", rewriting " 𝑛2:\n of: 𝑛5\n" <> rules <> " 𝑛: 𝑛2\n", "names no meta bound by 'morph' or by any line") , ("a 'rewrite' line bound to what is no expression meta", rewriting " 𝛿1:\n of: 𝑛1\n" <> rules <> " 𝑛: 𝑛1\n", "is not an expression meta") , ("a 'rewrite' line with no rules at all", rewriting " 𝑛2:\n of: 𝑛1\n 𝑛: 𝑛2\n", "cannot be read") , ("a rule of 'rewrite' minting a fresh symbol", rewriting " 𝑛2:\n of: 𝑛1\n rules:\n - name: minting\n pattern: ⟦ φ ↦ 𝑒1 ⟧\n result: ⟦ λ ⤍ 𝜎 ⟧\n 𝑛: 𝑛2\n", "writes a symbol 𝜎 into its result") , ("a rule of 'rewrite' writing a symbol nobody minted", rewriting " 𝑛2:\n of: 𝑛1\n rules:\n - name: naming\n pattern: ⟦ φ ↦ 𝑒1 ⟧\n result: ⟦ λ ⤍ 𝜎1 ⟧\n 𝑛: 𝑛2\n", "writes a symbol 𝜎 into its result") , ("a rule of 'rewrite' reading a meta it never binds", rewriting " 𝑛2:\n of: 𝑛1\n rules:\n - name: unbound\n pattern: ⟦ φ ↦ 𝑒1 ⟧\n result: ⟦ φ ↦ 𝑒2 ⟧\n 𝑛: 𝑛2\n", "reads the meta 'e2' it never binds") , ("a rule of 'rewrite' with no result", rewriting " 𝑛2:\n of: 𝑛1\n rules:\n - name: empty\n pattern: ⟦ φ ↦ 𝑒1 ⟧\n 𝑛: 𝑛2\n", "cannot be read") - , ("an 'evaluate' line firing a meta the entry never bound", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by a line above it") - , ("an 'evaluate' line firing what a line below it fired", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛2: 𝑛3\n 𝑛3: 𝑛1\n 𝑛: 𝑛2\n", "names no meta bound by 'morph' or by a line above it") - , ("an 'evaluate' line firing what a 'rewrite' line made", rewriting " 𝑛2:\n of: 𝑛1\n" <> rules <> " evaluate:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by a line above it") + , ("an 'evaluate' line firing a meta the entry never bound", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by any line") , ("an 'evaluate' line bound to what is no expression meta", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝛿1: 𝑛1\n 𝑛: 𝑛1\n", "is not an expression meta") , ("an 'evaluate' line firing a meta that came down to data", "- λ: L_fork\n dataize:\n 𝛿1: $.ρ\n evaluate:\n 𝑛1: 𝛿1\n 𝑛: 𝑛1\n", "is not an expression meta") , ("an 'evaluate' line firing a term instead of a meta", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛2: $.a\n 𝑛: 𝑛2\n", "is not an expression meta") , ("a meta bound by 'morph' and again by 'evaluate'", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛1: 𝑛1\n 𝑛: 𝑛1\n", "The meta '𝑛1' of λ function 'L_fork' is bound by more than one line") + , ("a 'stay' line keeping a meta the entry never bound", "- λ: L_fork\n morph:\n 𝑛1: $.a\n stay:\n 𝑛3: 𝑛2\n 𝑛: 𝑛3\n", "names no meta bound by 'morph' or by any line") + , ("a 'stay' line bound to what is no expression meta", "- λ: L_fork\n morph:\n 𝑛1: $.a\n stay:\n 𝛿1: 𝑛1\n 𝑛: 𝑛1\n", "is not an expression meta") + , ("a 'stay' line keeping a term instead of a meta", "- λ: L_fork\n morph:\n 𝑛1: $.a\n stay:\n 𝑛2: $.a\n 𝑛: 𝑛2\n", "is not an expression meta") + , ("a meta bound by 'morph' and again by 'stay'", "- λ: L_fork\n morph:\n 𝑛1: $.a\n stay:\n 𝑛1: 𝑛1\n 𝑛: 𝑛1\n", "The meta '𝑛1' of λ function 'L_fork' is bound by more than one line") + , ("a line reading the meta it binds", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛2: 𝑛2\n 𝑛: 𝑛2\n", "The line binding '𝑛2' of λ function 'L_fork' reads the meta it binds") + , ("two lines reading what each other made", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛2: 𝑛3\n symbolize:\n 𝑛3: 𝑛2\n 𝑛: 𝑛2\n", "The line binding '𝑛2' of λ function 'L_fork' reads the meta it binds") + , ("a line reading what two lines reading each other made, blaming one of the two", "- λ: L_fork\n morph:\n 𝑛1: $.a\n evaluate:\n 𝑛5: 𝑛3\n symbolize:\n 𝑛3: 𝑛4\n 𝑛4: 𝑛3\n 𝑛: 𝑛5\n", "The line binding '𝑛3' of λ function 'L_fork' reads the meta it binds") , ("an answer naming a meta no block binds", "- λ: L_pair\n dataize:\n 𝛿1: $.ρ\n 𝑛: 𝑛7\n", "reads the meta 'n7' that no block binds") , ("an operand of 'dataize' reading a meta", "- λ: L_pair\n dataize:\n 𝛿1: 𝑛5\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "of 'dataize' of λ function 'L_pair' reads the meta 'n5'") , ("an operand of 'morph' reading a meta", "- λ: L_pair\n morph:\n 𝑛1: $.x.𝜏1\n 𝑛: 𝑛1\n", "of 'morph' of λ function 'L_pair' reads the meta 't1'") , ("a lenient entry with no 'join' line to be lenient in", "- λ: L_pair\n dataize:\n 𝛿1: $.ρ\n lenient: true\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n", "is lenient but has no 'join' line") , ("a 'lenient' key which is no boolean", "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛2]\n lenient: often\n 𝑛: 𝑛3\n", "lenient: expected Bool") - , ("a 'symbolize' line standing what a 'join' line made", "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n symbolize:\n 𝑛5: 𝑛3\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛5\n", "names no meta bound by 'morph' or by a line above it") + , ("an entry that defers but is not lenient", "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛2]\n defer: true\n 𝑛: 𝑛3\n", "defers but is not lenient") + , ("a 'defer' key which is no boolean", "- λ: L_fork\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛2]\n lenient: true\n defer: later\n 𝑛: 𝑛3\n", "defer: expected Bool") , ("a 'terminators' key which is no list", "- λ: L_fork\n morph:\n 𝑛1: $.a\n terminators: L_throw\n 𝑛: 𝑛1\n", "expected Array") , ( "a terminator an entry of the file answers" @@ -322,6 +385,41 @@ term <- parseExpressionThrows "Φ.number( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )" let (_, _, spent) = symbolized term 4 spent `shouldBe` 4 + + describe "stayed" $ do + let keeping :: String -> String -> IO (Expression, Expression) + keeping written expected = do + term <- parseExpressionThrows written + kept <- parseExpressionThrows expected + pure (stayed term, kept) + + it "drops the ρ a dispatch is applied to" $ do + (term, kept) <- keeping "Φ.bytes( ρ ↦ ⟦ x ↦ ∅ ⟧ )" "Φ.bytes" + term `shouldBe` kept + + it "drops the ρ a dispatch is applied to after an argument binding no ρ" $ do + (term, kept) <- keeping "Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )( ρ ↦ ⟦ x ↦ ∅ ⟧ )" "Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )" + term `shouldBe` kept + + it "drops every ρ a chain of applications gives a dispatch" $ do + (term, kept) <- keeping "ξ.f( ρ ↦ ⟦ a ↦ ∅ ⟧ )( α0 ↦ ⟦⟧ )( ρ ↦ ⟦ b ↦ ∅ ⟧ )" "ξ.f( α0 ↦ ⟦⟧ )" + term `shouldBe` kept + + it "keeps the ρ a formation is applied to" $ do + (term, kept) <- keeping "⟦ ρ ↦ ∅, t ↦ ∅ ⟧( t ↦ ⟦⟧ )( ρ ↦ ⟦ x ↦ ∅ ⟧ )" "⟦ ρ ↦ ∅, t ↦ ∅ ⟧( t ↦ ⟦⟧ )( ρ ↦ ⟦ x ↦ ∅ ⟧ )" + term `shouldBe` kept + + it "drops a ρ standing deep inside the argument of an application" $ do + (term, kept) <- keeping "Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ )( ρ ↦ ⟦ x ↦ ∅ ⟧ ) )" "Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ) )" + term `shouldBe` kept + + it "drops a ρ standing in a method of a formation and not only in its φ" $ do + (term, kept) <- keeping "⟦ φ ↦ ⟦⟧, m ↦ ⟦ φ ↦ Φ.f( ρ ↦ ⟦ x ↦ ∅ ⟧ ) ⟧ ⟧" "⟦ φ ↦ ⟦⟧, m ↦ ⟦ φ ↦ Φ.f ⟧ ⟧" + term `shouldBe` kept + + it "drops a ρ standing inside a ρ the term keeps" $ do + (term, kept) <- keeping "⟦ x ↦ ∅ ⟧( ρ ↦ Φ.f( ρ ↦ ⟦ y ↦ ∅ ⟧ ) )" "⟦ x ↦ ∅ ⟧( ρ ↦ Φ.f )" + term `shouldBe` kept describe "joined" $ do let joining :: Bool -> String -> String -> Int -> IO (Maybe (Expression, [(Int, (Int, Int))], Int)) diff --git a/test/MergeSpec.hs b/test/MergeSpec.hs --- a/test/MergeSpec.hs +++ b/test/MergeSpec.hs @@ -15,7 +15,7 @@ import Files (allPathsIn) import GHC.Generics (Generic) import Merge (merge) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Printer (printExpression) import System.FilePath import Test.Hspec @@ -41,11 +41,11 @@ packs ( \pth -> it (makeRelative resources pth) $ do YamlPack{..} <- yamlPack pth - parsed <- mapM parseExpressionThrows [left, right] + parsed <- mapM (parseExpressionThrows' MONOFORM) [left, right] case (result, fails) of (Just expected, Nothing) -> do merged <- merge parsed - expected' <- parseExpressionThrows expected + expected' <- parseExpressionThrows' MONOFORM expected merged `shouldBe` expected' (Nothing, Just message) -> do thrown <- try (merge parsed) :: IO (Either SomeException Expression) diff --git a/test/MorphSpec.hs b/test/MorphSpec.hs --- a/test/MorphSpec.hs +++ b/test/MorphSpec.hs @@ -30,7 +30,7 @@ import Lambdas (Lambdas, emptyLambdas) import Matcher (substEmpty) import Morph (Deadline (..), ReduceContext (..), emptyState, enter, execBuildTerm, inferred, insideUniverse, morph, morph') -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import System.FilePath (makeRelative) @@ -61,9 +61,9 @@ testMorph :: Lambdas -> FilePath -> Expectation testMorph known pth = do MorphPack{..} <- Decode.decodeFileThrow pth - expr <- parseExpressionThrows (if model == Just True then primitives input else input) + expr <- parseExpressionThrows' MONOFORM (if model == Just True then primitives input else input) seedTaus expr - loc <- parseExpressionThrows (fromMaybe "Q" location) + loc <- parseExpressionThrows' MONOFORM (fromMaybe "Q" location) base <- defaultReduceContext loc let ctx = base @@ -72,7 +72,7 @@ } case (result, fails) of (Just res, Nothing) -> do - expected <- parseExpressionThrows res + expected <- parseExpressionThrows' MONOFORM res (morphed, _, _) <- morph expr emptyState ctx morphed `shouldBe` expected (Nothing, Just message) -> diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -755,3 +755,72 @@ (\ipt -> (ipt, Nothing :: Maybe Expression)) ["⟦ x(y) ↦ 42 ⟧", "⟦ x(y) ↦ 42:a.b ⟧", "⟦ x(y) ↦ 42:a(z) ⟧", "⟦ x(y) ↦ ξ.a ⟧", "Q.x(y(z) ↦ FF-:Δ.b)", "⟦ x(y) ↦ ⟦ ⟧.a ⟧", "⟦ x(y) ↦ ⟦ ⟧(a ↦ ξ) ⟧", "⟦ x(y) ↦ ⟦ ⟧:y ⟧"] ) + + describe "rejects a mix of ASCII and Unicode symbols under monoform" $ + fails + (parseExpression' MONOFORM) + [ ("⟦ x -> ? ]]", "The ASCII symbol \"->\" at 1:5 mixes with the Unicode \"⟦\" at 1:1, while --monoform is set") + , ("[[ x ↦ ∅ ]]", "The Unicode symbol \"↦\" at 1:6 mixes with the ASCII \"[[\" at 1:1, while --monoform is set") + , ("⟦\n x -> ?\n⟧", "The ASCII symbol \"->\" at 2:5 mixes with the Unicode \"⟦\" at 1:1") + , ("\"hi\".x(y ↦ ξ, z -> $)", "The ASCII symbol \"->\" at 1:17 mixes with the Unicode \"↦\" at 1:10") + , ("[[ x -> ∅ ]]", "The Unicode symbol \"∅\" at 1:9") + , ("⟦ x ↦ ? ⟧", "The ASCII symbol \"?\" at 1:7") + , ("[[ x -> ξ ]]", "The Unicode symbol \"ξ\" at 1:9") + , ("⟦ x ↦ $ ⟧", "The ASCII symbol \"$\" at 1:7") + , ("[[ x -> Φ.y ]]", "The Unicode symbol \"Φ\" at 1:9") + , ("⟦ x ↦ Q.y ⟧", "The ASCII symbol \"Q\" at 1:7") + , ("[[ x -> ⊥ ]]", "The Unicode symbol \"⊥\" at 1:9") + , ("⟦ x ↦ T ⟧", "The ASCII symbol \"T\" at 1:7") + , ("[[ x -> $.ρ ]]", "The Unicode symbol \"ρ\" at 1:11") + , ("⟦ x ↦ ξ.^ ⟧", "The ASCII symbol \"^\" at 1:9") + , ("[[ φ -> $ ]]", "The Unicode symbol \"φ\" at 1:4") + , ("⟦ @ ↦ ξ ⟧", "The ASCII symbol \"@\" at 1:3") + , ("Q.x(α0 -> $)", "The Unicode symbol \"α\" at 1:5 mixes with the ASCII \"Q\" at 1:1") + , ("Φ.x(~0 ↦ ξ)", "The ASCII symbol \"~\" at 1:5 mixes with the Unicode \"Φ\" at 1:1") + , ("[[ Δ ⤍ 00- ]]", "The Unicode symbol \"Δ ⤍\" at 1:4") + , ("⟦ D> 00- ⟧", "The ASCII symbol \"D>\" at 1:3") + , ("[[ λ ⤍ Fn ]]", "The Unicode symbol \"λ ⤍\" at 1:4") + , ("⟦ L> Fn ⟧", "The ASCII symbol \"L>\" at 1:3") + , ("[[ x -> 00-:Δ ]]", "The Unicode symbol \"Δ\" at 1:13") + , ("⟦ x ↦ 00-:D ⟧", "The ASCII symbol \"D\" at 1:11") + , ("[[ x -> Fn:λ ]]", "The Unicode symbol \"λ\" at 1:12") + , ("⟦ x ↦ Fn:L ⟧", "The ASCII symbol \"L\" at 1:10") + , ("⟦ x ↦ ∅ ]]", "The ASCII symbol \"]]\" at 1:9") + , ("[[ x -> 𝑒1 ]]", "The Unicode symbol \"𝑒\" at 1:9") + , ("⟦ x ↦ !e1 ⟧", "The ASCII symbol \"!e\" at 1:7") + , ("⟦ x ↦ !n1 ⟧", "The ASCII symbol \"!n\" at 1:7") + , ("⟦ x ↦ !k1 ⟧", "The ASCII symbol \"!k\" at 1:7") + , ("[[ 𝐵1 ]]", "The Unicode symbol \"𝐵\" at 1:4") + , ("[[ 𝜏1 -> $ ]]", "The Unicode symbol \"𝜏\" at 1:4") + , ("[[ D> 𝛿1 ]]", "The Unicode symbol \"𝛿\" at 1:7") + , ("[[ L> 𝑓1 ]]", "The Unicode symbol \"𝑓\" at 1:7") + , ("[[ L> 𝜎1 ]]", "The Unicode symbol \"𝜎\" at 1:7") + , ("Φ.x(α!i1 ↦ ξ)", "The ASCII symbol \"!i\" at 1:6") + , ("⟦ y ↦ ξ, x -> ξ ⟧", "expression:1:12:") + ] + + describe "accepts a program spelled in one script under monoform" $ + test + (parseExpression' MONOFORM) + [ ("[[ x -> ? ]]", Just (ExFormation [BiVoid (AtLabel "x")])) + , ("⟦ x ↦ ∅ ⟧", Just (ExFormation [BiVoid (AtLabel "x")])) + , ("\"hi\".x(42)", Just (ExApplication (ExDispatch (DataString (BtMany ["68", "69"])) (AtLabel "x")) (ArAlpha (Alpha 0) (DataNumber (BtMany ["40", "45", "00", "00", "00", "00", "00", "00"]))))) + , ("Q:λ", Just (ExFormation [BiLambda (Function "Q")])) + , ("T:L", Just (ExFormation [BiLambda (Function "T")])) + , ("Q.x(~0 -> [[ D> 00-, L> Fn, ^ -> $, @ -> T, y -> !e1, z -> 01-:D ]])", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArAlpha (Alpha 0) (ExFormation [BiDelta (BtOne "00"), BiLambda (Function "Fn"), BiTau AtRho ExXi, BiTau AtPhi ExTermination, BiTau (AtLabel "y") (ExMeta "e1"), BiTau (AtLabel "z") (ExFormation [BiDelta (BtOne "01")])])))) + , ("Φ.x(α0 ↦ ⟦ Δ ⤍ 00-, λ ⤍ Fn, ρ ↦ ξ, φ ↦ ⊥, y ↦ 𝑒1, z ↦ 01-:Δ ⟧)", Just (ExApplication (ExDispatch ExRoot (AtLabel "x")) (ArAlpha (Alpha 0) (ExFormation [BiDelta (BtOne "00"), BiLambda (Function "Fn"), BiTau AtRho ExXi, BiTau AtPhi ExTermination, BiTau (AtLabel "y") (ExMeta "e1"), BiTau (AtLabel "z") (ExFormation [BiDelta (BtOne "01")])])))) + ] + + describe "accepts a mix of ASCII and Unicode symbols without monoform" $ + test + (parseExpression' POLYFORM) + [ ("⟦ x -> ? ]]", Just (ExFormation [BiVoid (AtLabel "x")])) + , ("[[ x ↦ ∅ ⟧", Just (ExFormation [BiVoid (AtLabel "x")])) + ] + + describe "parseExpressionThrows' under monoform" $ + forM_ + [ ("throws on a program mixing ASCII and Unicode symbols", parseExpressionThrows' MONOFORM "⟦ x -> ? ]]" `shouldThrow` anyException) + , ("returns the expression of a program spelled in Unicode alone", parseExpressionThrows' MONOFORM "⟦ x ↦ ∅ ⟧" `shouldReturn` ExFormation [BiVoid (AtLabel "x")]) + ] + (uncurry it) diff --git a/test/RewriterSpec.hs b/test/RewriterSpec.hs --- a/test/RewriterSpec.hs +++ b/test/RewriterSpec.hs @@ -26,7 +26,7 @@ import Functions (buildTerm) import GHC.Generics import Must (Must (..)) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Printer (printExpression) import Rewriter (RewriteContext (RewriteContext), direct, every, fast, rewrite) import Rule (RuleContext (RuleContext), Step (Step, _applied)) @@ -205,7 +205,7 @@ case skip pack of Just True -> pending _ -> do - expr <- parseExpressionThrows (input pack) + expr <- parseExpressionThrows' MONOFORM (input pack) seedTaus expr rules' <- case rules pack of Just _rules -> case custom _rules of @@ -243,7 +243,7 @@ dontSaveMade ) let (rewritten, _) = NE.last rewrittens - result' <- parseExpressionThrows (output pack) + result' <- parseExpressionThrows' MONOFORM (output pack) unless (rewritten == result') $ expectationFailure ( "Wrong rewritten expression. Expected:\n" diff --git a/test/RuleSpec.hs b/test/RuleSpec.hs --- a/test/RuleSpec.hs +++ b/test/RuleSpec.hs @@ -19,7 +19,7 @@ import Functions (buildTerm) import GHC.Generics import Matcher -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Printer (printSubsts) import Rule (RuleContext (RuleContext), isNF, matchExpressionWithRule, meetCondition, normalHeld, redex) import System.FilePath @@ -28,7 +28,7 @@ data ConditionPack = ConditionPack { failure :: Maybe Bool - , expression :: Expression + , expression :: String , pattern :: Expression , condition :: Yaml.Condition } @@ -43,7 +43,7 @@ packs ( \pth -> it (makeRelative resources pth) $ do pack <- Y.decodeFileThrow pth :: IO ConditionPack - let expr = expression pack + expr <- parseExpressionThrows' MONOFORM (expression pack) let matched = matchExpression (pattern pack) expr unless (matched /= []) (expectationFailure "List of matched substitutions is empty which is not expected") met <- meetCondition (condition pack) matched (RuleContext buildTerm Nothing (_normal linked)) diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs --- a/test/XMIRSpec.hs +++ b/test/XMIRSpec.hs @@ -20,7 +20,7 @@ import Data.Yaml qualified as Yaml import Files (allPathsIn) import GHC.Generics (Generic) -import Parser (parseExpressionThrows) +import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Printer (printExpression) import System.FilePath (makeRelative) import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldNotContain, shouldReturn, shouldThrow) @@ -197,7 +197,7 @@ Just True -> xmir' `shouldThrow` anyException _ -> do xmir'' <- xmir' - phi'' <- parseExpressionThrows phi' + phi'' <- parseExpressionThrows' MONOFORM phi' xmir'' `shouldBe` phi'' ) @@ -287,7 +287,7 @@ it (makeRelative resources pth) $ do pack <- printPack pth let PrintPack{phi = phi', xpaths = xpaths'} = pack - expr <- parseExpressionThrows phi' + expr <- parseExpressionThrows' MONOFORM phi' xmir' <- expressionToXMIR expr defaultXmirContext let failed = filter (not . matches xmir') xpaths' unless