phino 0.0.161 → 0.0.162
raw patch · 78 files changed
+1977/−568 lines, 78 filesdep +conduitdep +libyamldep ~optparse-applicative
Dependencies added: conduit, libyaml
Dependency ranges changed: optparse-applicative
Files
- README.md +109/−93
- app/Main.hs +2/−3
- benchmark/Main.hs +10/−4
- phino.cabal +7/−4
- src/AST.hs +4/−4
- src/CLI.hs +9/−2
- src/CLI/Helpers.hs +24/−1
- src/CLI/Parsers.hs +32/−1
- src/CLI/Runners.hs +4/−2
- src/CLI/Types.hs +4/−0
- src/Condition.hs +1/−1
- src/Deps.hs +104/−10
- src/Evaluate.hs +49/−23
- src/Functions.hs +4/−1
- src/Morph.hs +239/−69
- src/Regexp.hs +4/−1
- src/Rewriter.hs +2/−2
- src/Rule.hs +19/−11
- src/Yaml.hs +36/−3
- test-resources/cli/rules/join-broken.yaml +2/−2
- test-resources/cli/rules/kind-dataize-to-expression.yaml +12/−0
- test-resources/cli/rules/kind-size-to-attribute.yaml +12/−0
- test-resources/cli/rules/kind-tau-to-attribute.yaml +10/−0
- test-resources/cli/rules/kind-tau-to-expression.yaml +10/−0
- test-resources/condition-packs/eq-mismatched-comparable-kinds.yaml +0/−10
- test-resources/condition-packs/gt-non-numeric.yaml +0/−8
- test-resources/condition-packs/matches-non-data.yaml +8/−0
- test-resources/condition-packs/matches-unbound-nested-meta.yaml +8/−0
- test-resources/condition-packs/part-of-unbound-meta.yaml +8/−0
- test-resources/evaluate-packs/answers-a-firing-whose-operand-loops.yaml +43/−0
- test-resources/evaluate-packs/answers-an-operand-that-dataizes-in-circles-with-a-symbol.yaml +19/−15
- test-resources/evaluate-packs/answers-bottom-for-a-meta-that-raises.yaml +31/−0
- test-resources/evaluate-packs/answers-its-own-sides-on-a-condition-another-join-read.yaml +16/−7
- test-resources/evaluate-packs/answers-the-same-dataization-loop-under-partial.yaml +19/−15
- test-resources/evaluate-packs/binds-a-copy-over-no-bare-symbol-as-it-is.yaml +11/−9
- test-resources/evaluate-packs/cuts-a-loop-met-at-a-dispatch-off-an-atom.yaml +66/−0
- test-resources/evaluate-packs/cuts-a-recursion-running-through-evaluate-lines.yaml +18/−6
- test-resources/evaluate-packs/cuts-a-recursion-that-differs-by-symbols-only.yaml +15/−5
- test-resources/evaluate-packs/cuts-an-entry-that-answers-with-a-firing-of-itself.yaml +25/−0
- test-resources/evaluate-packs/defers-a-copy-a-join-passed-through-stay-and-symbolize.yaml +10/−6
- test-resources/evaluate-packs/defers-a-copy-whose-phi-reads-nothing-of-its-own.yaml +12/−8
- test-resources/evaluate-packs/fails-on-an-operand-that-reaches-the-terminator.yaml +4/−2
- test-resources/evaluate-packs/fires-a-formation-once-however-often-it-is-met.yaml +4/−0
- test-resources/evaluate-packs/fires-a-formation-written-in-place-after-a-stay-line.yaml +1/−0
- test-resources/evaluate-packs/fires-a-formation-written-in-place-with-its-voids-filled.yaml +1/−0
- test-resources/evaluate-packs/fires-the-arguments-of-a-copy-a-defer-line-defers.yaml +17/−10
- test-resources/evaluate-packs/joins-a-side-a-morph-line-brought-down-from-what-a-rewrite-line-unwrapped.yaml +4/−3
- test-resources/evaluate-packs/joins-a-side-reading-the-rho-it-binds-in-a-fabricated-formation.yaml +5/−3
- test-resources/evaluate-packs/joins-a-side-that-dispatches-on-a-terminator.yaml +44/−0
- test-resources/evaluate-packs/joins-a-side-that-raises-through-a-terminator.yaml +8/−6
- test-resources/evaluate-packs/joins-a-side-whose-operand-raises.yaml +50/−0
- test-resources/evaluate-packs/joins-again-the-attribute-of-a-fabricated-formation.yaml +10/−7
- test-resources/evaluate-packs/joins-two-sides-differing-in-a-datum-a-symbolize-found-off-the-phi-chain.yaml +5/−3
- test-resources/evaluate-packs/leaves-a-formation-with-an-attribute-of-its-own-as-it-is.yaml +19/−10
- test-resources/evaluate-packs/morphs-two-branches-spelling-one-term-through-one-firing.yaml +5/−0
- test-resources/evaluate-packs/parks-a-firing-whose-deferred-argument-got-stuck.yaml +12/−6
- test-resources/evaluate-packs/parks-a-firing-whose-operand-loops.yaml +0/−33
- test-resources/evaluate-packs/parks-a-firing-whose-operand-reaches-the-terminator.yaml +4/−2
- test-resources/evaluate-packs/parks-an-entry-that-answers-with-a-firing-of-itself.yaml +0/−23
- test-resources/evaluate-packs/spends-a-step-on-every-firing-of-an-evaluate-line.yaml +4/−2
- test-resources/evaluate-packs/takes-the-answer-of-a-firing-with-the-same-operands.yaml +23/−12
- test-resources/evaluate-packs/tells-two-symbols-of-one-datum-apart-between-firings.yaml +29/−17
- test-resources/evaluate-packs/undresses-a-formation-wrapping-itself-until-the-steps-run-out.yaml +8/−7
- test-resources/evaluate-packs/work-out-an-argument-that-comes-to-a-hanging-object.yaml +76/−0
- test-resources/evaluate-packs/writes-no-joined-line-for-a-join-the-memo-answered.yaml +10/−1
- test-resources/rewriter-packs/custom/eq-expression-with-a-quoted-number.yaml +18/−0
- test/CLISpec.hs +330/−72
- test/ConditionSpec.hs +10/−2
- test/DataizeSpec.hs +6/−6
- test/DepsSpec.hs +45/−3
- test/EvaluateSpec.hs +25/−1
- test/Fixtures.hs +1/−1
- test/FunctionsSpec.hs +12/−0
- test/MorphSpec.hs +38/−2
- test/RegexpSpec.hs +4/−0
- test/RewriterSpec.hs +31/−5
- test/RuleSpec.hs +29/−1
- test/YamlSpec.hs +67/−2
README.md view
@@ -34,7 +34,7 @@ ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.160+cabal install --overwrite-policy=always phino-0.0.161 phino --version ``` @@ -59,7 +59,7 @@ for the runner and puts it on the `PATH`: ```yaml-- uses: objectionary/phino@0.0.160+- uses: objectionary/phino@0.0.161 with: version-file: phino-version.txt - run: phino --version@@ -226,15 +226,17 @@ ### Limits -Three options stop a run that goes on for too long:+Five options stop a run that goes on for too long: * `--max-steps` bounds how deep morphing and dataization may nest, `1000` by default; * `--max-firings` bounds how many λ functions the whole run may fire;-* `--max-seconds` bounds how many seconds the whole run may take.+* `--max-seconds` bounds how many seconds the whole run may take;+* `--max-nodes` bounds how many nodes the term of the run may grow to;+* `--max-memory` bounds the live heap of the run, such as `8G`. -`--partial` leaves a site in place when it runs out of steps or firings, but-a run out of time always fails.+`--partial` leaves a site in place when it runs out of steps, firings,+nodes or memory, but a run out of time always fails. ## Morph @@ -263,7 +265,8 @@ ### Acyclic morphing `phino` stops no recursion by itself, so a run that never ends fails once-`--max-steps` runs out.+`--max-steps` runs out, with `Morphing did not finish before reaching the+limit of steps: --max-steps=<n>`. The `--acyclic=<mode>` option makes the run notice a loop instead. When a reduction is about to enter a formation it is already inside, the run answers a copy of an object binding φ with a fresh symbol and goes on, and@@ -308,8 +311,10 @@ ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧.φ $ cat down.txt 𝕄(Φ.y):- 𝑛·0·1 := Φ.down( x ↦ 𝜎1:λ )- 𝑛·0·2 := ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧+ remembered 𝑛·0·1 ≡ Φ.down # ⟦ x ↦ ∅, λ ⤍ L_down ⟧+ 𝑛·0·2 := Φ.down( x ↦ 𝜎1:λ )+ 𝑛·0·3 := ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧+ remembered 𝑛·0·3 ≡ 𝑛·0·1( x ↦ 𝜎1:λ ) 𝔼(L_down): 𝔻(ξ.x): 𝛿·1·1 := 𝔻(𝜎1:λ)@@ -318,9 +323,11 @@ 𝕄(𝑛·1·1): 𝑛·1·2 := Φ.down( x ↦ 𝜎2:λ ) 𝑛·1·3 := ⟦ x ↦ 𝜎2:λ, λ ⤍ L_down ⟧+ remembered 𝑛·1·3 ≡ 𝑛·0·1( x ↦ 𝜎2:λ ) morphed 𝑛·1·4 := 𝑛·1·3 𝑛·1·5 := 𝑛·1·3 # 𝕄(𝑛·1·1)- looped 𝑛·0·2 # proven+ remembered 𝑛·1·3 ≡ 𝑛·0·3+ looped 𝑛·0·3 # proven ``` In a name such as `𝑛·1·2`, the first number counts the firings, `0` outside@@ -353,10 +360,18 @@ * `unanswered …` is a λ name no entry answers. * `stuck …` closes a firing that got stuck, and `stall …` stands under one that `--acyclic=plausible` answered with an earlier stall.+* `remembered 𝑛·0·1 ≡ Φ.down` is a fact the run keeps: the term on the+ left came from the one on the right, a path or a call of the world, or+ a formation it was the answer of.+* `memoized 𝑛·0·5 ⇛ 𝑛·1·9` is what `--acyclic=plausible` keeps: the+ formation on the left fired to the term on the right.+* `recalled 𝑛·0·3 ⇒ 𝑛·0·1( x ↦ ⟦⟧ )` is a fact or a memo entry used again,+ spelled as its `remembered` or `memoized` line spelled it. * `looped …` is where `--acyclic` cut a loop, and `looped 𝜎1 := …` names- the call of the object it answered with that symbol.-* `starved …`, `spent …` and `timeout …` are where `--max-steps`,- `--max-firings` and `--max-seconds` ran out.+ the call of the object it answered with that symbol, when a fact names it.+* `starved …`, `spent …`, `timeout …`, `oversized …` and `blown …` are+ where `--max-steps`, `--max-firings`, `--max-seconds`, `--max-nodes` and+ `--max-memory` ran out. * `msec …`, `firings …` and `fps …` close the file, and the listing above leaves them and the `# …` lines out, since they differ from run to run. @@ -612,7 +627,8 @@ separated by `/`, for example, this pattern `s/\\s+//g` replaces all the spaces with empty string. To escape braces and slashes in pattern and replacement parts - use them with `\\`,- e.g. `s/\\(.+\\)//g`.+ e.g. `s/\\(.+\\)//g`. In the replacement, `\\1` to `\\9`, as well as+ `$1`, put what a group of the pattern matched, e.g. `s/([0-9]+)/\\1!/g`. * `random-string` - accepts dataizable expression or bytes as pattern. Replaces `%x` and `%d` formatters with random hex numbers and decimals accordingly. Uniqueness is guaranteed during one@@ -689,119 +705,119 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1- total: 2364731.566 μs- avg: 236473.157 μs- min: 211300.467 μs- max: 292747.941 μs- std dev: 27820.705 μs+ total: 2471508.678 μs+ avg: 247150.868 μs+ min: 221146.358 μs+ max: 280070.951 μs+ std dev: 22173.343 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1- total: 9413355.678 μs- avg: 941335.568 μs- min: 877776.308 μs- max: 1027338.259 μs- std dev: 48859.029 μs+ total: 9900009.942 μs+ avg: 990000.994 μs+ min: 913216.401 μs+ max: 1064034.163 μs+ std dev: 51646.433 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1- total: 20.380 μs- avg: 2.038 μs- min: 1.683 μs- max: 2.665 μs- std dev: 0.306 μs+ total: 20.277 μs+ avg: 2.028 μs+ min: 1.763 μs+ max: 2.444 μs+ std dev: 0.206 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1- total: 5757294.693 μs- avg: 575729.469 μs- min: 538059.300 μs- max: 598828.490 μs- std dev: 18128.062 μs+ total: 5893919.071 μs+ avg: 589391.907 μs+ min: 546710.930 μs+ max: 622324.691 μs+ std dev: 22402.952 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1- total: 677431.913 μs- avg: 67743.191 μs- min: 60183.418 μs- max: 82804.920 μs- std dev: 9547.482 μs+ total: 745153.374 μs+ avg: 74515.337 μs+ min: 64906.612 μs+ max: 87781.583 μs+ std dev: 10272.240 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1- total: 18322088.429 μs- avg: 1832208.843 μs- min: 1797579.128 μs- max: 1855894.416 μs- std dev: 17033.785 μs+ total: 18806006.234 μs+ avg: 1880600.623 μs+ min: 1829320.397 μs+ max: 1936784.646 μs+ std dev: 32771.969 μs === morph/symbolic/demo/e1 === warmup: 3 iterations batches: 10 x 9- total: 11891.278 μs- avg: 132.125 μs- min: 122.627 μs- max: 167.660 μs- std dev: 13.084 μs+ total: 12166.226 μs+ avg: 135.180 μs+ min: 131.121 μs+ max: 144.901 μs+ std dev: 3.769 μs === morph/symbolic/demo/e2 === warmup: 3 iterations- batches: 10 x 139- total: 175033.685 μs- avg: 125.924 μs- min: 124.889 μs- max: 126.740 μs- std dev: 0.630 μs+ batches: 10 x 129+ total: 173694.366 μs+ avg: 134.647 μs+ min: 133.356 μs+ max: 136.014 μs+ std dev: 0.741 μs === morph/symbolic/demo/e3 === warmup: 3 iterations- batches: 10 x 134- total: 170791.687 μs- avg: 127.456 μs- min: 126.059 μs- max: 128.848 μs- std dev: 0.830 μs+ batches: 10 x 129+ total: 178632.645 μs+ avg: 138.475 μs+ min: 133.065 μs+ max: 163.122 μs+ std dev: 9.065 μs === morph/symbolic/demo/e4 === warmup: 3 iterations- batches: 10 x 106- total: 134964.020 μs- avg: 127.325 μs- min: 125.971 μs- max: 128.683 μs- std dev: 0.765 μs+ batches: 10 x 113+ total: 158155.239 μs+ avg: 139.960 μs+ min: 133.878 μs+ max: 168.699 μs+ std dev: 10.055 μs === morph/symbolic/demo/e5 === warmup: 3 iterations- batches: 10 x 128- total: 167197.696 μs- avg: 130.623 μs- min: 129.334 μs- max: 132.171 μs- std dev: 0.854 μs+ batches: 10 x 126+ total: 172774.638 μs+ avg: 137.123 μs+ min: 136.318 μs+ max: 138.811 μs+ std dev: 0.767 μs === morph/symbolic/native/e5 === warmup: 3 iterations- batches: 10 x 5- total: 65499.420 μs- avg: 1309.988 μs- min: 1146.675 μs- max: 1920.625 μs- std dev: 229.609 μs+ batches: 10 x 4+ total: 53810.789 μs+ avg: 1345.270 μs+ min: 1165.754 μs+ max: 2105.284 μs+ std dev: 261.412 μs === morph/symbolic/accum/0 === warmup: 3 iterations- batches: 10 x 94- total: 100369.800 μs- avg: 106.776 μs- min: 105.512 μs- max: 109.443 μs- std dev: 1.070 μs+ batches: 10 x 76+ total: 85572.821 μs+ avg: 112.596 μs+ min: 111.501 μs+ max: 114.714 μs+ std dev: 1.060 μs === morph/symbolic/accum/400 === warmup: 3 iterations- batches: 10 x 66- total: 81652.018 μs- avg: 123.715 μs- min: 121.695 μs- max: 126.110 μs- std dev: 1.480 μs+ batches: 10 x 65+ total: 85508.304 μs+ avg: 131.551 μs+ min: 131.274 μs+ max: 131.842 μs+ std dev: 0.180 μs ``` The results were calculated in [this GHA job][benchmark-gha]-on 2026-11-03 at 13:03,+on 2026-11-10 at 19:10, on Linux with 4 CPUs. <!-- benchmark_end -->@@ -844,4 +860,4 @@ [jna]: https://github.com/java-native-access/jna [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin-[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/41639970792+[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/42882136890
app/Main.hs view
@@ -3,9 +3,8 @@ module Main where -import CLI (runCLI)-import GHC.IO.Encoding (setLocaleEncoding, utf8)+import CLI (prepareIO, runCLI) import System.Environment (getArgs) main :: IO ()-main = setLocaleEncoding utf8 >> getArgs >>= runCLI+main = prepareIO >> getArgs >>= runCLI
benchmark/Main.hs view
@@ -23,7 +23,7 @@ import Lining (LineFormat (MULTILINE, SINGLELINE)) import Margin (defaultMargin) import Merge (merge)-import Morph (Memo, ReduceContext (ReduceContext), Steps (Steps), emptyState, memoized, morph)+import Morph (Facts, Memo, ReduceContext (ReduceContext), Steps (Steps), emptyState, factual, memoized, morph) import Must (Must (MtDisabled)) import Parser (parseExpressionThrows) import Printer (printExpression')@@ -62,14 +62,16 @@ dontSaveStep dontSaveMade -symbolicCtx :: Acyclic -> Maybe Memo -> IORef Int -> Lambdas -> Expression -> ReduceContext-symbolicCtx acyclic memo minted lambdas locator =+symbolicCtx :: Acyclic -> Maybe Memo -> Maybe Facts -> IORef Int -> Lambdas -> Expression -> ReduceContext+symbolicCtx acyclic memo facts minted lambdas locator = ReduceContext locator locator Nothing 25 25+ Nothing+ Nothing (Steps 1000 0) Nothing minted@@ -85,7 +87,10 @@ Morphing [] Map.empty+ facts lambdas+ []+ False (building linked) reduction evaluation@@ -194,8 +199,9 @@ symbolic acyclic universe lambdas locator = do seedTaus universe memo <- memoized (Just acyclic)+ facts <- Just <$> factual minted <- newIORef 0- let ctx = symbolicCtx acyclic memo minted lambdas locator+ let ctx = symbolicCtx acyclic memo facts minted lambdas locator started universe ctx (answer, _, _) <- morph universe emptyState ctx pure (hashExpression answer)
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.161+version: 0.0.162 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>@@ -12,6 +12,7 @@ copyright: 2025 Objectionary.com category: Language, Code Analysis build-type: Simple+tested-with: GHC ==9.6.7 || ==9.8.4 || ==9.10.3 extra-source-files: resources/normalize/*.yaml resources/morphing/*.yaml resources/dataization/*.yaml resources/contextualization/*.yaml benchmark/demo.phi benchmark/atoms.yaml benchmark/accum.phi benchmark/accum.yaml test-resources/**/*.yaml test-resources/**/*.phi extra-doc-files: README.md @@ -111,13 +112,15 @@ base >=4.18.3.0 && <5, binary-ieee754 >=0.1.0 && <0.2, bytestring >=0.11.4 && <0.13,+ conduit >=1.3 && <1.4, containers >=0.6.5 && <0.9, directory >=1.3.7 && <1.4, file-embed >=0.0.15 && <0.0.17, filepath >=1.4.200 && <1.6, gitrev >=1.3.1 && <1.4,+ libyaml >=0.1 && <0.2, megaparsec >=9.5 && <9.9,- optparse-applicative >=0.18 && <0.20,+ optparse-applicative >=0.19 && <0.20, random >=1.2 && <1.4, regex-pcre-builtin >=0.95.2 && <0.96, scientific >=0.3.7 && <0.4,@@ -135,7 +138,7 @@ executable phino import: warnings main-is: Main.hs- ghc-options: -threaded+ ghc-options: -threaded "-with-rtsopts=-T" hs-source-dirs: app build-depends: base,@@ -149,7 +152,7 @@ type: exitcode-stdio-1.0 main-is: Main.hs hs-source-dirs: test- ghc-options: -threaded+ ghc-options: -threaded "-with-rtsopts=-T" other-modules: AbridgeSpec ASTSpec
src/AST.hs view
@@ -42,7 +42,7 @@ import Data.Bits (xor) import qualified Data.IntMap.Strict as IntMap-import Data.List (foldl')+import qualified Data.List as List import qualified Data.Map.Strict as Map import Data.Maybe (isJust, isNothing, listToMaybe) import Data.Text (Text)@@ -248,7 +248,7 @@ hashText :: Int -> Text -> Int hashText = T.foldl' (\h c -> step h (fromEnum c)) hashString :: Int -> String -> Int- hashString = foldl' (\h c -> step h (fromEnum c))+ hashString = List.foldl' (\h c -> step h (fromEnum c)) goSlot :: Int -> Slot -> Int goSlot h (Slot kind idx) = step (hashText h kind) idx hashMaybeString :: Int -> Maybe String -> Int@@ -256,7 +256,7 @@ hashMaybeString h (Just s) = hashString (step h 1) s goExpr :: Int -> Expression -> Int goExpr h = \case- ExFormation bds -> foldl' goBinding (step h 1) bds+ ExFormation bds -> List.foldl' goBinding (step h 1) bds ExXi -> step h 2 ExRoot -> step h 3 ExTermination -> step h 4@@ -279,7 +279,7 @@ goBytes h = \case BtEmpty -> step h 17 BtOne s -> hashString (step h 18) s- BtMany ss -> foldl' hashString (step h 19) ss+ BtMany ss -> List.foldl' hashString (step h 19) ss BtMeta t -> hashText (step h 20) t BtAny slot -> goSlot (step h 34) slot goAttribute :: Int -> Attribute -> Int
src/CLI.hs view
@@ -5,7 +5,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module CLI (runCLI) where+module CLI (prepareIO, runCLI) where import CLI.Parsers import CLI.Runners@@ -15,13 +15,20 @@ import Data.List (dropWhileEnd) import Data.Version (showVersion) import Files (ensuredFile)+import GHC.IO.Encoding (setFileSystemEncoding, setLocaleEncoding) import GHC.IO.Exception (IOErrorType (ResourceVanished)) import Logger import Options.Applicative import Paths_phino (version) import System.Exit (ExitCode (..), exitFailure, exitWith)-import System.IO (hPutStrLn, stderr)+import System.IO (hPutStrLn, hSetEncoding, stderr, utf8) import System.IO.Error (ioeGetErrorType)++prepareIO :: IO ()+prepareIO =+ setLocaleEncoding utf8+ >> setFileSystemEncoding utf8+ >> hSetEncoding stderr utf8 runCLI :: [String] -> IO () runCLI args = handle handler $ do
src/CLI/Helpers.hs view
@@ -340,10 +340,33 @@ in case filter (\fn -> fn `notElem` (buildFunctions ++ execFunctions)) used of (fn : _) -> invalidCLIArguments (printf "Function '%s' in rule '%s' is not supported" fn rule.name) [] -> case filter (`elem` execFunctions) used of- [] -> pure rule+ [] -> case filter (\extra -> returned (Y.function extra) /= kind (Y.meta extra)) (fromMaybe [] rule.where_) of+ [] -> pure rule+ (extra : _) ->+ invalidCLIArguments+ ( printf+ "Function '%s' in rule '%s' returns %s, but its meta '%s' is %s"+ (Y.function extra)+ rule.name+ (returned (Y.function extra))+ (P.printExtraArg (Y.meta extra))+ (kind (Y.meta extra))+ ) (fn : _) -> invalidCLIArguments (printf "Function '%s' in rule '%s' is available only for dataization and morphing, not for rewriting" fn rule.name)+ where+ returned :: String -> String+ returned "random-tau" = "an attribute"+ returned "tau" = "an attribute"+ returned "join" = "bindings"+ returned "dataize" = "bytes"+ returned _ = "an expression"+ kind :: Y.ExtraArgument -> String+ kind (Y.ArgAttribute _) = "an attribute"+ kind (Y.ArgBinding _) = "bindings"+ kind (Y.ArgBytes _) = "bytes"+ kind (Y.ArgExpression _) = "an expression" printOut :: Maybe FilePath -> String -> IO () printOut target content = case target of
src/CLI/Parsers.hs view
@@ -4,7 +4,7 @@ module CLI.Parsers where import CLI.Types-import Data.Char (toLower, toUpper)+import Data.Char (isDigit, toLower, toUpper) import Data.List (intercalate) import Data.Version (showVersion) import Deps (Acyclic, certainty)@@ -116,6 +116,33 @@ (long "max-seconds" <> metavar "SECONDS" <> help "Maximum number of seconds the whole run may take, unlimited unless given") ) +optMaxNodes :: Parser (Maybe Int)+optMaxNodes =+ optional+ ( option+ (boundedIntOption >>= validateIntOption (> 0) "--max-nodes must be positive")+ (long "max-nodes" <> metavar "NODES" <> help "Maximum number of nodes the term of the run may grow to, unlimited unless given")+ )++optMaxMemory :: Parser (Maybe Int)+optMaxMemory =+ optional+ ( option+ (eitherReader bytes >>= validateIntOption (> 0) "--max-memory must be positive")+ (long "max-memory" <> metavar "BYTES" <> help "Maximum size of the live heap the run may grow to, such as 512M or 8G, unlimited unless given")+ )+ where+ bytes :: String -> Either String Int+ bytes spelling = case span isDigit spelling of+ (digits@(_ : _), unit) -> maybe malformed (bounded . (read digits *)) (lookup (map toUpper unit) (zip ["", "K", "M", "G", "T"] (iterate (* 1024) 1)))+ _ -> malformed+ bounded :: Integer -> Either String Int+ bounded num+ | num > toInteger (maxBound :: Int) = Left (printf "--max-memory must not exceed %d bytes" (maxBound :: Int))+ | otherwise = Right (fromInteger num)+ malformed :: Either String Int+ malformed = Left "--max-memory must be a number of bytes, optionally ending with K, M, G or T"+ optMargin :: Parser Int optMargin = option@@ -422,6 +449,8 @@ <*> optMaxSteps <*> optMaxFirings <*> optMaxSeconds+ <*> optMaxNodes+ <*> optMaxMemory <*> optMargin <*> optMeetPopularity <*> optMeetLength@@ -472,6 +501,8 @@ <*> optMaxSteps <*> optMaxFirings <*> optMaxSeconds+ <*> optMaxNodes+ <*> optMaxMemory <*> optMargin <*> optMeetPopularity <*> optMeetLength
src/CLI/Runners.hs view
@@ -183,6 +183,7 @@ tally <- tallied _maxFirings minted <- newIORef 0 memo <- memoized _acyclic+ facts <- factual linked <- engine header <- headerOf args _inputFile input expr _symbolic lambdas ((outcome, chain, _), universe, aim) <-@@ -190,7 +191,7 @@ _protocol printCtx ( \record -> do- let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Dataization, loc)) _depthSensitive _shuffle _partial _acyclic _maxLoops Dataization [] Map.empty lambdas (building linked) reduction evaluation save record linked+ let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles _maxNodes _maxMemory (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Dataization, loc)) _depthSensitive _shuffle _partial _acyclic _maxLoops Dataization [] Map.empty (Just facts) lambdas [] False (building linked) reduction evaluation save record linked (universe, aiming) <- aimed printCtx Dataization header _inside expr ctx started universe aiming (,universe,aiming._locator) <$> dataize universe emptyState aiming@@ -268,6 +269,7 @@ tally <- tallied _maxFirings minted <- newIORef 0 memo <- memoized _acyclic+ facts <- factual linked <- engine header <- headerOf args _inputFile input expr _symbolic lambdas ((morphed, chain, _), universe, aim) <-@@ -275,7 +277,7 @@ _protocol printCtx ( \record -> do- let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Morphing, loc)) _depthSensitive _shuffle _partial _acyclic _maxLoops Morphing [] Map.empty lambdas (building linked) reduction evaluation save record linked+ let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles _maxNodes _maxMemory (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Morphing, loc)) _depthSensitive _shuffle _partial _acyclic _maxLoops Morphing [] Map.empty (Just facts) lambdas [] False (building linked) reduction evaluation save record linked (universe, aiming) <- aimed printCtx Morphing header _inside expr ctx started universe aiming (,universe,aiming._locator) <$> morph universe emptyState aiming
src/CLI/Types.hs view
@@ -119,6 +119,8 @@ , _maxSteps :: Int , _maxFirings :: Maybe Int , _maxSeconds :: Maybe Int+ , _maxNodes :: Maybe Int+ , _maxMemory :: Maybe Int , _margin :: Int , _meetPopularity :: Maybe Int , _meetLength :: Maybe Int@@ -166,6 +168,8 @@ , _maxSteps :: Int , _maxFirings :: Maybe Int , _maxSeconds :: Maybe Int+ , _maxNodes :: Maybe Int+ , _maxMemory :: Maybe Int , _margin :: Int , _meetPopularity :: Maybe Int , _meetLength :: Maybe Int
src/Condition.hs view
@@ -160,7 +160,7 @@ "condition" input case parsed of- Right parsed' -> Right parsed'+ Right parsed' -> parsed' <$ Y.wellCompared parsed' Left err -> Left (errorBundlePretty err) parseConditionThrows :: String -> IO Y.Condition
src/Deps.hs view
@@ -133,13 +133,16 @@ | EvManufactured Int Int | EvBoxed Int Expression | EvUndressed Int Expression- | EvLooped Int Judgment Acyclic Expression Expression (Maybe (Int, 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 | EvStarved Int Int Judgment Expression | EvTimeout Int Int Judgment Expression | EvSpent Int Int Judgment Expression+ | EvExceeded Int Int Judgment Expression+ | EvOversized Int Int Judgment Expression+ | EvBlown Int Int Judgment Expression | EvData Int T.Text Expression (Either Int Bytes) | EvTerm Int T.Text Judgment Expression Expression | EvBound Int Expression Expression@@ -157,6 +160,9 @@ | EvUnripe Int (Expression, Expression) (Expression, Expression) Side Attribute | EvFabricated Int (Expression, Expression) (Expression, Expression) Expression | EvTaken Int Expression+ | EvRemembered Int Expression Expression+ | EvMemoized Int Expression Expression+ | EvRecalled Int Expression Expression | EvWorld Expression | EvHeader Header Expression Expression @@ -176,6 +182,9 @@ 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 (EvExceeded depth limit judgment site) = EvExceeded depth limit judgment (moved site)+ record (EvOversized depth limit judgment site) = EvOversized depth limit judgment (moved site)+ record (EvBlown depth limit judgment site) = EvBlown 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@@ -204,6 +213,9 @@ tier (EvStarved depth _ _ _) = depth tier (EvTimeout depth _ _ _) = depth tier (EvSpent depth _ _ _) = depth+tier (EvExceeded depth _ _ _) = depth+tier (EvOversized depth _ _ _) = depth+tier (EvBlown depth _ _ _) = depth tier (EvData depth _ _ _) = depth tier (EvTerm depth _ _ _ _) = depth tier (EvBound depth _ _) = depth@@ -221,6 +233,9 @@ tier (EvUnripe depth _ _ _ _) = depth tier (EvFabricated depth _ _ _) = depth tier (EvTaken depth _) = depth+tier (EvRemembered depth _ _) = depth+tier (EvMemoized depth _ _) = depth+tier (EvRecalled depth _ _) = depth tier EvWorld{} = maxBound tier EvHeader{} = 0 @@ -256,6 +271,14 @@ abbreviatedInside names (ExDispatch expr attr) = ExDispatch (abbreviated names expr) attr abbreviatedInside _ term = term +sized :: Int -> String+sized bytes = fromMaybe (show bytes) (listToMaybe [printf "%d%c" (div bytes scale) unit | (unit, scale) <- reverse (zip "KMGT" (iterate (* 1024) 1024)), mod bytes scale == 0])++dispatched :: Expression -> ([Attribute], Expression)+dispatched (ExDispatch term attr)+ | (attrs, call@(ExApplication _ _)) <- dispatched term = (attrs ++ [attr], call)+dispatched term = ([], term)+ data Protocol = Protocol { _fired :: Int , _named :: Named T.Text@@ -269,10 +292,11 @@ , _blocks :: [(Int, Maybe (Judgment, String), String, Bool)] , _answered :: [(Int, Expression, String)] , _unwritten :: Map.Map Int (Named Expression)+ , _stated :: Named [(Expression, (String, String))] } emptyProtocol :: Protocol-emptyProtocol = Protocol 0 Map.empty [] False Map.empty Map.empty Map.empty Map.empty Nothing [] [] Map.empty+emptyProtocol = Protocol 0 Map.empty [] False Map.empty Map.empty Map.empty Map.empty Nothing [] [] Map.empty Map.empty data Nesting = Nesting { _fires :: Int@@ -290,13 +314,20 @@ , _shapes :: Map.Map [Maybe Attribute] [(Expression, [Binding])] , _opaque :: Int , _unmarked :: Map.Map Int (Named Expression)+ , _attested :: Named [(Expression, (String, String))] } type Naming = StateT (Nesting, [String]) IO emptyNesting :: Nesting-emptyNesting = Nesting 0 [] [] Map.empty Map.empty Map.empty Map.empty Nothing [] [] [] Map.empty Map.empty 0 Map.empty+emptyNesting = Nesting 0 [] [] Map.empty Map.empty Map.empty Map.empty Nothing [] [] [] Map.empty Map.empty 0 Map.empty Map.empty +stated :: Expression -> Expression -> String -> String -> Named [(Expression, (String, String))] -> Named [(Expression, (String, String))]+stated object source left right facts = namedInsert object ((source, (left, right)) : fromMaybe [] (namedLookup object facts)) facts++statement :: Expression -> Expression -> Named [(Expression, (String, String))] -> Maybe (String, String)+statement object source facts = namedLookup object facts >>= lookup source+ saveEval :: Handle -> IORef Protocol -> (Expression -> IO String) -> (Expression -> IO String) -> SaveEvalFunc saveEval handle cursor printed printed' report = do made <- atomicModify cursor (fmap (first (forgotten report) . headed) . written (tier report) report . beside (tier report) report . outer (tier report))@@ -347,6 +378,19 @@ saved line = do hPutStrLn handle line logDebug (printf "Saved one line of the protocol: %s" (dropWhile (== ' ') line))+ stating :: Int -> String -> String -> Expression -> Expression -> Protocol -> IO (Protocol, Maybe String)+ stating at word arrow object source protocol = do+ origin <- render source+ case namedLookup object protocol._made of+ Just _ -> do+ known <- render object+ pure (protocol{_stated = stated object source known origin protocol._stated}, Just (indented at (printf "%s %s %s %s" word known arrow origin)))+ Nothing -> do+ let (index, counted) = numbered protocol+ naming :: String+ naming = printf "%s·%d" (labelled protocol answer) index+ body <- printed (abbreviatedInside protocol._made object)+ pure (counted{_made = namedInsert object (alias (opener protocol) index) counted._made, _stated = stated object source naming origin counted._stated}, Just (indented at (printf "%s %s %s %s # %s" word naming arrow origin body))) written :: Int -> Evaluation -> Protocol -> IO (Protocol, Maybe String) written _ (EvRun judgment locator) protocol = pure (protocol{_begun = True, _blocks = [(0, Just (judgment, heading), heading ++ ":", True)]}, Just (heading ++ ":"))@@ -389,10 +433,10 @@ (line, notes) <- maybe (pure (printf "looped %s" form, [])) (severed form) answered pure (protocol, Just (indented at (remarked line (remarks ++ certainty mode : notes)))) where- severed :: String -> (Int, Expression) -> IO (String, [String])+ severed :: String -> (Int, Maybe Expression) -> IO (String, [String]) severed form (symbol, call) = do- made <- printed (abbreviatedInside protocol._made call)- pure (printf "looped %s := %s" (printFunction (FnSymbol symbol)) made, [printf "repeats %s" form])+ made <- traverse (printed . abbreviatedInside protocol._made) call+ pure (printf "looped %s%s" (printFunction (FnSymbol symbol)) (maybe "" (" := " ++) made), [printf "repeats %s" form]) written at (EvStuck _ key judgment self) protocol = do form <- render self pure (protocol, Just (indented at (printf "unanswered %s # %s(%s)" (T.unpack key) (letter judgment) form)))@@ -409,6 +453,15 @@ written at (EvSpent _ limit judgment site) protocol = do remarks <- context protocol judgment site pure (protocol, Just (indented at (remarked (printf "spent %d" limit) remarks)))+ written at (EvExceeded _ limit judgment site) protocol = do+ remarks <- context protocol judgment site+ pure (protocol, Just (indented at (remarked (printf "exceeded %d" limit) remarks)))+ written at (EvOversized _ limit judgment site) protocol = do+ remarks <- context protocol judgment site+ pure (protocol, Just (indented at (remarked (printf "oversized %d" limit) remarks)))+ written at (EvBlown _ limit judgment site) protocol = do+ remarks <- context protocol judgment site+ pure (protocol, Just (indented at (remarked (printf "blown %s" (sized limit)) remarks))) written at (EvData _ spelling operand value) protocol = do datum <- maybe (spelt value) pure (found value protocol._found) line <- commented protocol (printf "%s := %s" (labelled protocol spelling) datum) Dataization operand@@ -498,6 +551,11 @@ naming = printf "%s·%d" (labelled protocol answer) index (protocol', value) <- valued counted naming term pure (protocol'{_made = namedFormation term (alias (opener protocol) index) protocol'._made}, Just (indented at (printf "%s := %s" naming value)))+ written at (EvRemembered _ object source) protocol = stating at "remembered" "≡" object source protocol+ written at (EvMemoized _ form reply) protocol = stating at "memoized" "⇛" form reply protocol+ written at (EvRecalled _ term reply) protocol = do+ (known, given) <- maybe ((,) <$> render term <*> render reply) pure (statement term reply protocol._stated)+ pure (protocol, Just (indented at (printf "recalled %s ⇒ %s" known given))) written _ (EvWorld world) protocol = pure (protocol{_made = namedInsert world ExRoot protocol._made}, Nothing) written _ (EvHeader (Header release revision dated command (World file count size tops bindings) table) locator expression) protocol = do place <- printed locator@@ -674,12 +732,17 @@ locator <- located depth site origin <- sole depth self pure (enclosed "looped" (printf "<looped by=\"%s\" match=\"%s\" at=\"%s\"" (opened judgment) (certainty mode) (escapeXML locator)) origin)- elements at (EvLooped depth judgment mode self site (Just (symbol, call))) nesting =+ elements at (EvLooped depth judgment mode self site (Just (symbol, Nothing))) nesting = placed at nesting $ do locator <- located depth site origin <- leaf depth self+ pure (printf "<looped symbol=\"%s\" by=\"%s\" match=\"%s\" at=\"%s\" of=\"%s\"/>" (sigma symbol) (opened judgment) (certainty mode) (escapeXML locator) (escapeXML origin))+ elements at (EvLooped depth judgment mode self site (Just (symbol, Just call))) nesting =+ placed at nesting $ do+ locator <- located depth site+ origin <- leaf depth self (object, given) <- called depth call- pure (printf "<looped symbol=\"%s\" by=\"%s\" match=\"%s\" at=\"%s\" of=\"%s\" object=\"%s\">%s</looped>" (sigma symbol) (opened judgment) (certainty mode) (escapeXML locator) (escapeXML origin) (escapeXML object) given)+ pure (printf "<looped symbol=\"%s\" by=\"%s\" match=\"%s\" at=\"%s\" of=\"%s\" object=\"%s\"%s>%s</looped>" (sigma symbol) (opened judgment) (certainty mode) (escapeXML locator) (escapeXML origin) (escapeXML object) (trailed call) given) elements at (EvStuck depth key judgment self) nesting = placed at nesting (printf "<unanswered λ=\"%s\" by=\"%s\">%s</unanswered>" (quoted key) (opened judgment) . escapeXMLText <$> leaf depth self) elements at (EvStall _ key) nesting =@@ -692,6 +755,12 @@ placed at nesting (printf "<timeout limit=\"%d\" by=\"%s\" at=\"%s\"/>" limit (opened judgment) . escapeXML <$> located depth site) elements at (EvSpent depth limit judgment site) nesting = placed at nesting (printf "<spent limit=\"%d\" by=\"%s\" at=\"%s\"/>" limit (opened judgment) . escapeXML <$> located depth site)+ elements at (EvExceeded depth limit judgment site) nesting =+ placed at nesting (printf "<exceeded limit=\"%d\" by=\"%s\" at=\"%s\"/>" limit (opened judgment) . escapeXML <$> located depth site)+ elements at (EvOversized depth limit judgment site) nesting =+ placed at nesting (printf "<oversized limit=\"%d\" by=\"%s\" at=\"%s\"/>" limit (opened judgment) . escapeXML <$> located depth site)+ elements at (EvBlown depth limit judgment site) nesting =+ placed at nesting (printf "<blown limit=\"%s\" by=\"%s\" at=\"%s\"/>" (sized limit) (opened judgment) . escapeXML <$> located depth site) elements at (EvDelta _ bytes) nesting = do datum <- printed (ExBytes bytes) let (naming, nesting') = stored (Right bytes) nesting@@ -777,6 +846,12 @@ (naming, _) <- counted pure (printf "<fabricated meta=\"%s\" left=\"%s\" right=\"%s\">%s</fabricated>" (escapeXML naming) (escapeXML one) (escapeXML two) (escapeXMLText body)) elements at (EvTaken depth term) nesting = placed at nesting (concluded "answered" depth term)+ elements at (EvRemembered depth object source) nesting = placed at nesting (attesting "remembered" depth nesting object source)+ elements at (EvMemoized depth form reply) nesting = placed at nesting (attesting "memoized" depth nesting form reply)+ elements at (EvRecalled depth term reply) nesting =+ placed at nesting $ do+ (asked, given) <- maybe ((,) <$> leaf depth term <*> leaf depth reply) pure (statement term reply nesting._attested)+ pure (printf "<recalled of=\"%s\" as=\"%s\"/>" (escapeXML asked) (escapeXML given)) elements _ (EvWorld world) nesting = pure (known world nesting, []) prologue :: Nesting -> [String] prologue nesting@@ -811,6 +886,18 @@ where index :: Int index = maybe 1 (+ 1) (Map.lookup (opener nesting) nesting._numbered)+ attesting :: String -> Int -> Nesting -> Expression -> Expression -> Naming String+ attesting word depth nesting object source = do+ origin <- leaf depth source+ case namedLookup object nesting._objects of+ Just _ -> do+ kept <- leaf depth object+ modify (first (\nesting' -> nesting'{_attested = stated object source kept origin nesting'._attested}))+ pure (printf "<%s of=\"%s\" as=\"%s\"/>" word (escapeXML kept) (escapeXML origin))+ Nothing -> do+ (naming, aliased) <- counted+ modify (first (\nesting' -> nesting'{_objects = namedInsert object aliased nesting'._objects, _attested = stated object source naming origin nesting'._attested}))+ pure (printf "<%s meta=\"%s\" as=\"%s\"/>" word (escapeXML naming) (escapeXML origin)) counted :: Naming (String, Expression) counted = do (nesting, records) <- get@@ -947,9 +1034,16 @@ enclosed :: String -> String -> (String, String) -> String enclosed _ opening (origin, "") = printf "%s of=\"%s\"/>" opening (escapeXML origin) enclosed tag opening (origin, inner) = printf "%s of=\"%s\">%s</%s>" opening (escapeXML origin) inner tag+ trailed :: Expression -> String+ trailed call = case fst (dispatched call) of+ [] -> ""+ attrs -> printf " dispatch=\"%s\"" (escapeXML (intercalate "." (map printAttribute attrs))) invoked :: Expression -> (Expression, [(Attribute, Expression)])- invoked (ExApplication term (ArTau attr value)) = second (++ [(attr, value)]) (invoked term)- invoked term = (term, [])+ invoked = applied . snd . dispatched+ where+ applied :: Expression -> (Expression, [(Attribute, Expression)])+ applied (ExApplication term (ArTau attr value)) = second (++ [(attr, value)]) (applied term)+ applied term = (term, []) passed :: (Attribute, Expression) -> Naming String passed (attr, value) = valued value >>= lift . attributed (printAttribute attr) valued :: Expression -> Naming Expression
src/Evaluate.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TupleSections #-}@@ -10,19 +12,19 @@ import AST import Builder (buildExpressionThrows)-import Control.Exception (throwIO, try)-import Control.Monad (foldM, unless)+import Control.Exception (Exception, catch, throwIO, try)+import Control.Monad (foldM, unless, when) import Data.IORef (readIORef, writeIORef) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..))-import Data.Maybe (fromMaybe, listToMaybe)+import Data.Maybe (fromMaybe, isJust, listToMaybe) import qualified Data.Text as T import Deps (Evaluation (..), Judgment (Evaluation, Morphing), State (..), dontSaveEval, dontSaveStep, resited) import Engine (Engine (..)) import Forks (Refusal (Unnamed, Unripe), forked, joined) import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), cast, emptyLambdas, matched, minted, rewritten, stayed, symbolized, thrown) import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)-import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, opening, origin, recalled, remember, remembered, retained, settled, starved, unparked)+import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, noted, opening, recalled, remember, remembered, remembering, retained, settled, starved, unparked, voided) import Printer (printFunction) import Rule (RuleContext (RuleContext)) import Text.Printf (printf)@@ -53,32 +55,37 @@ name :: T.Text name = T.pack (printFunction (FnSymbol idx)) +data Raise = Raise+ deriving stock (Show)+ deriving anyclass (Exception)+ symbol :: T.Text -> Expression -> Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) symbol func form self univ state caller = case matched caller._symbolic func of Nothing -> do unless (func `elem` caller._parked) (caller._saveEval (EvStuck caller._nesting func caller._judgment form)) throwIO (Stuck func) Just entry -> do+ charged caller known <- recalled caller._memo form caller._steps._spent maybe (made entry) told known where made :: Lambda -> IO (Expression, State) made entry = do- charged caller stamp <- counted caller._memo exhausted <- starved caller._memo caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)- let ctx = caller{_nesting = caller._nesting + 1}- outcome <- try $ do+ let ctx = caller{_nesting = caller._nesting + 1, _raising = entry._terminators}+ outcome <- try $ raised ctx $ do (bound, dataized, conditions) <- foldM (down ctx) (substEmpty, state, []) entry._dataized (bound', morphed, normals) <- foldM (through ctx "morph" (still pure)) (bound, dataized, []) entry._morphed (bound'', undressed, normals') <- foldM (through ctx "undress" (peeled ctx)) (bound', morphed, normals) entry._undressed firing <- Firing func (reverse conditions) . (reverse normals' ++) <$> sides entry._ending known <- remembered caller._memo firing- maybe (worked ctx entry firing bound'' undressed) (\answer -> (answer, undressed) <$ shown ctx._nesting answer) known+ maybe (worked ctx entry firing bound'' undressed) (\(first, answer) -> (answer, undressed) <$ recited ctx._nesting first answer) known case outcome of Right (answer, state') -> do retained caller._memo form stamp (Answered answer)+ when (isJust caller._memo) (caller._saveEval (EvMemoized (caller._nesting + 1) form (ended answer))) pure (ended answer, state') Left failure -> do exhausted' <- starved caller._memo@@ -89,8 +96,14 @@ worked ctx entry firing@(Firing _ operands _) bound state' = do (lined, state'') <- foldM (passing ctx entry) (bound, state') entry._lines (answer, state''') <- concluded ctx entry operands lined state''- remember caller._memo firing answer+ remember caller._memo firing form answer+ known <- remembering caller._facts form+ when (known && spoken (ended answer)) (noted ctx (ended answer) form) pure (answer, state''')+ spoken :: Expression -> Bool+ spoken (ExFormation [BiLambda _]) = False+ spoken (ExFormation _) = True+ spoken _ = False sides :: Ending -> IO [Expression] sides (Answering _) = pure [] sides (Joining _ left right _) = traverse keyed [left, right]@@ -131,6 +144,11 @@ caller._saveEval (EvBuilt depth built) caller._saveEval (EvAnswer depth normal) shown depth (Joined normal) = caller._saveEval (EvTaken depth normal)+ shown depth Raised = caller._saveEval (EvTaken depth ExTermination)+ raised :: ReduceContext -> IO (Answer, State) -> IO (Answer, State)+ raised ctx work = catch work (\Raise -> (Raised, state) <$ shown ctx._nesting Raised)+ raising :: ReduceContext -> Expression -> IO ()+ raising ctx term = when (maybe False (thrown ctx._raising) (walked term)) (throwIO Raise) kept :: Bool -> ReduceException -> Maybe Kept kept _ (Looping term) = Just (Looped term) kept _ (LoopingAt term _ _) = Just (Looped term)@@ -150,7 +168,7 @@ told :: Kept -> IO (Expression, State) told (Answered answer) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)- shown (caller._nesting + 1) answer+ recited (caller._nesting + 1) form answer pure (ended answer, state) told (Looped term) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site)@@ -160,13 +178,21 @@ caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) caller._saveEval (EvStall (caller._nesting + 1) name) throwIO (Stuck name)+ recited :: Int -> Expression -> Answer -> IO ()+ recited depth term answer = do+ caller._saveEval (EvRecalled depth term (ended answer))+ shown depth answer down :: ReduceContext -> (Subst, State, [Either Int Bytes]) -> (Meta, Expression) -> IO (Subst, State, [Either Int Bytes]) down ctx (bound, state', conditions) (meta, term) = do- (datum, bound', state'') <- brought ctx bound state' meta term =<< operand term+ placed <- operand term+ raising ctx placed+ (datum, bound', state'') <- brought ctx bound state' meta term placed pure (bound', state'', datum : conditions) lowered :: ReduceContext -> (Subst, State) -> Meta -> Meta -> IO (Subst, State) lowered ctx (bound, state') meta source = do- (_, bound', state'') <- brought ctx bound state' meta (ExMeta source._name) =<< buildExpressionThrows (ExMeta source._name) bound+ term <- buildExpressionThrows (ExMeta source._name) bound+ raising ctx term+ (_, bound', state'') <- brought ctx bound state' meta (ExMeta source._name) term pure (bound', state'') brought :: ReduceContext -> Subst -> State -> Meta -> Expression -> Expression -> IO (Either Int Bytes, Subst, State) brought ctx bound state' meta origin term = do@@ -259,13 +285,13 @@ pure (bound', state'') kindled :: ReduceContext -> Ending -> Expression -> State -> Expression -> IO (Expression, State) kindled _ _ _ state' term@(ExFormation [BiLambda (FnSymbol _)]) = pure (term, state')- kindled ctx _ _ state' term@(ExFormation bds)- | owned ctx bds = pure (term, state')- kindled ctx _ site state' term@(ExFormation _) = fire ctx site state' term+ kindled ctx _ site state' term@(ExFormation bds) = do+ held <- owned ctx term bds+ if held then pure (term, state') else fire ctx site state' term kindled _ Joining{} _ state' term = pure (term, state') kindled ctx _ site state' term = fire ctx site state' term- owned :: ReduceContext -> [Binding] -> Bool- owned ctx bds = maybe False (\(_, voids) -> any (`notElem` (AtRho : [attr | BiVoid attr <- voids])) [attr | BiTau attr _ <- bds, not (cactus attr)]) (origin univ ctx bds)+ owned :: ReduceContext -> Expression -> [Binding] -> IO Bool+ owned ctx term bds = maybe False (\voids -> any (`notElem` (AtRho : voids)) [attr | BiTau attr _ <- bds, not (cactus attr)]) <$> voided ctx term cactus :: Attribute -> Bool cactus (AtLabel label) = "🌵" `T.isSuffixOf` label cactus _ = False@@ -320,7 +346,7 @@ reading = ctx{_symbolic = emptyLambdas, _memo = Nothing, _tally = Nothing, _acyclic = Nothing, _saveStep = dontSaveStep, _saveEval = dontSaveEval} postponed :: [Binding] -> IO Expression postponed known = do- call <- traverse (argued univ ctx state' site known) (called univ ctx known)+ call <- called univ ctx (ExFormation bds) known >>= traverse (argued univ ctx state' site known) fresh <- coined caller ctx._saveEval (EvDeferred ctx._nesting fresh Morphing (ExFormation known) call (ExDispatch site AtPhi)) pure (ExFormation [BiLambda (FnSymbol fresh)])@@ -381,11 +407,11 @@ held term = case walked term of Just (ExFormation bds) -> listToMaybe ([Left idx | BiLambda (FnSymbol idx) <- bds] ++ [Right bytes | BiDelta bytes <- bds]) _ -> Nothing- walked :: Expression -> Maybe Expression- walked (ExDispatch base attr) = case walked base of- Just (ExFormation bds) -> listToMaybe [term | BiTau attr' term <- bds, attr' == attr]- _ -> Nothing- walked term = Just term+ walked :: Expression -> Maybe Expression+ walked (ExDispatch base attr) = case walked base of+ Just (ExFormation bds) -> listToMaybe [term | BiTau attr' term <- bds, attr' == attr]+ _ -> Nothing+ walked term = Just term reached :: ReduceContext -> Subst -> Expression -> State -> IO (Expression, State) reached _ bound (ExMeta name) state' = (,state') <$> buildExpressionThrows (ExMeta name) bound reached ctx _ side state' = (\placed -> morphing univ ctx{_site = side} placed state') =<< operand side
src/Functions.hs view
@@ -12,6 +12,7 @@ import Control.Exception (throwIO) import Control.Monad (when) import qualified Data.ByteString.Char8 as B+import Data.Char (isDigit) import Data.Functor import qualified Data.Map.Strict as Map import qualified Data.Set as Set@@ -169,10 +170,12 @@ Nothing -> (acc, B.empty, False) Just (h, rest) | h == '\\' -> case B.uncons rest of- Just (h', rest') -> nextUntilSlash rest' ((if escape then acc else B.snoc acc '\\') `B.append` B.singleton h') escape+ Just (h', rest') -> nextUntilSlash rest' ((if escape && not (referring h') then acc else B.snoc acc '\\') `B.append` B.singleton h') escape Nothing -> (if escape then acc else B.snoc acc '\\', B.empty, False) | h == '/' -> (acc, rest, True) | otherwise -> nextUntilSlash rest (B.snoc acc h) escape+ referring :: Char -> Bool+ referring char = isDigit char || char == '\\' _randomString :: BuildTermMethod _randomString [arg] subst = do
src/Morph.hs view
@@ -11,32 +11,34 @@ -- 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 (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, deeper, emptyState, ended, enter, entering, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, opening, origin, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked) where+module Morph (Answer (..), Deadline (..), Firing (..), Facts, Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, declared, deeper, emptyState, ended, enter, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, factual, memoized, morph, noted, remembering, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked, voided) where import AST import Builder (buildExpressionThrows, nameIn) import Control.Applicative ((<|>)) import Control.Exception (Exception, catch, evaluate, throwIO, try)-import Control.Monad (when)+import Control.Monad (forM_, guard, unless, when)+import Data.Bifunctor (first, second) import Data.IORef (IORef, atomicModifyIORef', modifyIORef', newIORef, readIORef, writeIORef)-import Data.List (find, partition)+import Data.List (find, partition, sortOn) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map import Data.Maybe (fromMaybe, isJust, listToMaybe) import qualified Data.Text as T-import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dontSaveStep)+import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dispatched, dontSaveStep, sized) import Engine (Engine (..)) import GHC.Clock (getMonotonicTime)+import GHC.Stats (GCDetails (..), RTSStats (..), getRTSStats, getRTSStatsEnabled) import qualified Inference as In-import Lambdas (Lambdas)+import Lambdas (Lambdas, thrown) import Locator (locatedExpression, withLocatedExpression) import Matcher (substEmpty) import Must (Must (..)) import Printer (printExpression) import Random (shuffle) import Rewriter (RewriteContext (RewriteContext), Rewritten, Seen, rewrite, seenInsert)-import Rule (RuleContext (RuleContext))+import Rule (RuleContext (RuleContext), xiFree) import System.Timeout (timeout) import Text.Printf (printf) import Yaml (ExtraArgument (..))@@ -65,15 +67,17 @@ , _until :: Double } -data Memo = Memo (IORef (Store (Int, Kept))) (IORef (Map.Map Firing Answer)) (IORef Int) (IORef Int)+data Memo = Memo (IORef (Store (Int, Kept))) (IORef (Map.Map Firing (Expression, Answer))) (IORef Int) (IORef Int) data Answer = Answer Expression Expression | Joined Expression+ | Raised ended :: Answer -> Expression ended (Answer _ normal) = normal ended (Joined normal) = normal+ended Raised = ExTermination data Firing = Firing T.Text [Either Int Bytes] [Expression] deriving (Eq, Ord)@@ -85,12 +89,16 @@ type Store answer = Map.Map Int [(Expression, answer)] +type Facts = IORef (Store Expression)+ data ReduceContext = ReduceContext { _locator :: Expression , _site :: Expression , _universe :: Maybe Expression , _maxDepth :: Int , _maxCycles :: Int+ , _maxNodes :: Maybe Int+ , _maxMemory :: Maybe Int , _steps :: Steps , _tally :: Maybe Tally , _minted :: IORef Int@@ -106,7 +114,10 @@ , _judgment :: Judgment , _parked :: [T.Text] , _entered :: Seen+ , _facts :: Maybe Facts , _symbolic :: Lambdas+ , _raising :: [T.Text]+ , _reckoning :: Bool , _buildTerm :: BuildTermFunc , _reduce :: ReductionFunc , _evaluate :: EvaluationFunc@@ -119,6 +130,8 @@ = Depth Judgment Int | Firings Int | Cycles Int+ | Nodes Int+ | Memory Int data ReduceException = OutOfSteps Budget@@ -140,6 +153,10 @@ printf "Evaluation did not finish before reaching the limit of firings: --max-firings=%d" limit show (OutOfSteps (Cycles limit)) = printf "Normalization did not finish before reaching the limit of cycles: --max-cycles=%d" limit+ show (OutOfSteps (Nodes limit)) =+ printf "Evaluation did not finish before reaching the limit of nodes: --max-nodes=%d" limit+ show (OutOfSteps (Memory limit)) =+ printf "Evaluation did not finish before reaching the limit of memory: --max-memory=%s" (sized limit) show (OutOfStepsAt budget _ _) = show (OutOfSteps budget) show (OutOfTime limit) = printf "Evaluation did not finish before reaching the limit of seconds: --max-seconds=%d" limit@@ -165,6 +182,21 @@ starve Nothing = pure () starve (Just (Memo _ _ _ exhausted)) = modifyIORef' exhausted (+ 1) +measured :: ReduceContext -> Expression -> IO ()+measured ctx term = do+ forM_ ctx._maxNodes $ \cap ->+ when (countNodes term > cap) (overflown (EvOversized ctx._nesting cap ctx._judgment ctx._site) (Nodes cap))+ forM_ ctx._maxMemory $ \cap -> do+ enabled <- getRTSStatsEnabled+ unless enabled (ioError (userError "--max-memory needs the statistics of the runtime, which this binary was linked without"))+ stats <- getRTSStats+ when (toInteger (gcdetails_live_bytes (gc stats)) > toInteger cap) (overflown (EvBlown ctx._nesting cap ctx._judgment ctx._site) (Memory cap))+ where+ overflown :: Evaluation -> Budget -> IO ()+ overflown record budget = do+ ctx._saveEval record+ throwIO (OutOfSteps budget)+ tallied :: Maybe Int -> IO (Maybe Tally) tallied = traverse (\cap -> Tally cap <$> newIORef 0) @@ -236,14 +268,14 @@ retained (Just (Memo store _ _ _)) form stamp kept = modifyIORef' store (Map.insertWith (++) (hashExpression form) [(form, (stamp, kept))]) -remembered :: Maybe Memo -> Firing -> IO (Maybe Answer)+remembered :: Maybe Memo -> Firing -> IO (Maybe (Expression, Answer)) remembered Nothing _ = pure Nothing remembered (Just (Memo _ firings _ _)) firing = Map.lookup firing <$> readIORef firings -remember :: Maybe Memo -> Firing -> Answer -> IO ()-remember Nothing _ _ = pure ()-remember (Just (Memo _ firings answers _)) firing answer = do- modifyIORef' firings (Map.insert firing answer)+remember :: Maybe Memo -> Firing -> Expression -> Answer -> IO ()+remember Nothing _ _ _ = pure ()+remember (Just (Memo _ firings answers _)) firing form answer = do+ modifyIORef' firings (Map.insert firing (form, answer)) modifyIORef' answers (+ 1) parking :: NonEmpty Rewritten -> State -> IO a -> IO a@@ -264,9 +296,6 @@ rethrow (LoopingAt term _ _) = throwIO (Looping term) rethrow failure = throwIO failure -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) @@ -280,68 +309,141 @@ severing :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, ReduceContext) severing term univ state ctx = case entrance ctx._judgment term of- Just form -> either (,ctx) (term,) <$> sever form univ state ctx+ Just form -> either (,ctx) (term,) <$> sever (over term) form univ state ctx Nothing -> pure (term, ctx)+ where+ over :: Expression -> Maybe Attribute+ over (ExDispatch _ attr) = Just attr+ over _ = Nothing -sever :: Expression -> Expression -> State -> ReduceContext -> IO (Either Expression ReduceContext)-sever form univ state ctx = admitted form ctx >>= either cut (pure . Right)+sever :: Maybe Attribute -> Expression -> Expression -> State -> ReduceContext -> IO (Either Expression ReduceContext)+sever taken form univ state ctx = admitted form ctx >>= either cut (pure . Right) where cut :: (Acyclic, Expression) -> IO (Either Expression ReduceContext) cut loop = case form of- ExFormation bds- | boxed bds || ctx._judgment == Dataization- , Just call <- called univ ctx bds ->- Left <$> severed univ ctx state form bds call loop+ ExFormation bds -> Left <$> severed taken univ ctx state form bds loop _ -> refused form ctx loop -severed :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> (Acyclic, Expression) -> IO Expression-severed univ ctx state form bds call (mode, before) = do- reckoned <- argued univ ctx state form bds call+severed :: Maybe Attribute -> Expression -> ReduceContext -> State -> Expression -> [Binding] -> (Acyclic, Expression) -> IO Expression+severed taken univ ctx state form bds (mode, before) = do+ call <- (<|>) <$> traced ctx._facts form <*> traced ctx._facts before+ forM_ call (recited ctx . snd)+ reckoned <- traverse (spelled taken . fst) call fresh <- coined ctx ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site (Just (fresh, reckoned))) pure (ExFormation [BiLambda (FnSymbol fresh)])+ where+ spelled :: Maybe Attribute -> Expression -> IO Expression+ spelled (Just attr) found = pure (ExDispatch found attr)+ spelled Nothing found+ | ctx._reckoning = pure found+ | otherwise = argued univ ctx{_reckoning = True} state form bds found +recited :: ReduceContext -> [(Expression, Expression)] -> IO ()+recited ctx = mapM_ (\(term, source) -> ctx._saveEval (EvRecalled ctx._nesting term source))++factual :: IO Facts+factual = newIORef Map.empty++noted :: ReduceContext -> Expression -> Expression -> IO ()+noted ctx object source = forM_ ctx._facts $ \facts -> do+ known <- (Just source ==) . lookup object . Map.findWithDefault [] (hashExpression object) <$> readIORef facts+ unless known $ do+ modifyIORef' facts (Map.insertWith (++) (hashExpression object) [(object, source)])+ ctx._saveEval (EvRemembered ctx._nesting object source)++remembering :: Maybe Facts -> Expression -> IO Bool+remembering Nothing _ = pure False+remembering (Just facts) term = isJust . lookup term . Map.findWithDefault [] (hashExpression term) <$> readIORef facts++traced :: Maybe Facts -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))+traced Nothing _ = pure Nothing+traced (Just facts) form = do+ known <- readIORef facts+ pure (go known (Map.size known) form)+ where+ go :: Store Expression -> Int -> Expression -> Maybe (Expression, [(Expression, Expression)])+ go _ 0 _ = Nothing+ go known budget term = listToMaybe [(named, (object, source) : hops) | (path, object, source) <- sortOn (\(path, _, _) -> length path) [(path, object, source) | (object, source) <- concat (Map.elems known), path <- take 1 (lodged term object)], let (base, hops) = resolved known budget source, Just named <- [rooted (foldl ExDispatch base path)]]+ resolved :: Store Expression -> Int -> Expression -> (Expression, [(Expression, Expression)])+ resolved known budget source = case lookup source (Map.findWithDefault [] (hashExpression source) known) of+ Just _ -> fromMaybe (source, []) (go known (budget - 1) source)+ Nothing -> case source of+ ExApplication target arg -> first (`ExApplication` arg) (resolved known budget target)+ ExDispatch target attr -> first (`ExDispatch` attr) (resolved known budget target)+ _ -> (source, [])+ rooted :: Expression -> Maybe Expression+ rooted term = term <$ guard (grounded term)+ grounded :: Expression -> Bool+ grounded ExRoot = True+ grounded (ExDispatch target _) = grounded target+ grounded (ExApplication target _) = grounded target+ grounded _ = False+ lodged :: Expression -> Expression -> [[Attribute]]+ lodged (ExFormation bds) whole = searched (filter (not . rho) bds) [([], whole)] Map.empty+ lodged _ _ = []+ searched :: [Binding] -> [([Attribute], Expression)] -> Store () -> [[Attribute]]+ searched _ [] _ = []+ searched own ((path, term@(ExFormation inner)) : rest) seen+ | isJust (lookup term (Map.findWithDefault [] (hashExpression term) seen)) = searched own rest seen+ | filter (not . rho) inner == own = reverse path : searched own rest seen+ | otherwise = searched own (rest ++ [(attr : path, body) | BiTau attr body <- inner, attr /= AtRho]) (Map.insertWith (++) (hashExpression term) [(term, ())] seen)+ searched own (_ : rest) seen = searched own rest seen+ rho :: Binding -> Bool+ rho bd = attributeFromBinding bd == Just AtRho+ coined :: ReduceContext -> IO Int coined ctx = atomicModifyIORef' ctx._minted (\count -> (succ count, succ count)) fired :: Expression -> ReduceContext -> Expression -> State -> Expression -> IO (Expression, State)-fired univ ctx site state form = sever form univ state ctx{_judgment = Evaluation, _site = site} >>= either (pure . (,state)) kindled+fired univ ctx site state form = sever Nothing form univ state ctx{_judgment = Evaluation, _site = site} >>= either (pure . (,state)) kindled where kindled :: ReduceContext -> IO (Expression, State) kindled entered = do deep <- deeper entered deep._evaluate deep state form univ -called :: Expression -> ReduceContext -> [Binding] -> Maybe Expression-called univ ctx known = uncurry applied <$> origin univ ctx known+voided :: ReduceContext -> Expression -> IO (Maybe [Attribute])+voided ReduceContext{_facts = Nothing} _ = pure Nothing+voided ctx@ReduceContext{_facts = Just facts} form@(ExFormation bds) = do+ known <- readIORef facts+ case lookup form (Map.findWithDefault [] (hashExpression form) known) of+ Just source -> do+ let (voids, hops) = placed known (Map.size known) bds source+ recited ctx ((form, source) : hops)+ pure voids+ Nothing -> pure Nothing where+ placed :: Store Expression -> Int -> [Binding] -> Expression -> (Maybe [Attribute], [(Expression, Expression)])+ placed known budget _ (ExApplication head' _) = headed known budget head'+ placed _ _ own (ExDispatch _ _) = (Just [attr | BiVoid attr <- own], [])+ placed _ _ _ _ = (Nothing, [])+ headed :: Store Expression -> Int -> Expression -> (Maybe [Attribute], [(Expression, Expression)])+ headed known budget (ExApplication head' _) = headed known budget head'+ headed known budget head'@(ExFormation inner) = case lookup head' (Map.findWithDefault [] (hashExpression head') known) of+ Just source | budget > 0 -> second ((head', source) :) (placed known (budget - 1) inner source)+ _ -> (Just [attr | BiVoid attr <- inner], [])+ headed _ _ _ = (Nothing, [])+voided _ _ = pure Nothing++called :: Expression -> ReduceContext -> Expression -> [Binding] -> IO (Maybe Expression)+called univ ctx form known = fmap (uncurry applied) <$> declared univ ctx form+ where applied :: Expression -> [Binding] -> Expression- applied path declared = foldl ExApplication path [ArTau attr value | BiTau attr value <- known, attr /= AtRho, BiVoid attr `elem` declared]+ applied path voids = foldl ExApplication path [ArTau attr value | BiTau attr value <- known, attr /= AtRho, BiVoid attr `elem` voids] -origin :: Expression -> ReduceContext -> [Binding] -> Maybe (Expression, [Binding])-origin univ ctx bds = do- parent <- case filter ((== Just AtRho) . attributeFromBinding) bds of- [] -> Just ExRoot- [BiTau AtRho (ExFormation outer)] -> fst <$> origin univ ctx 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]+declared :: Expression -> ReduceContext -> Expression -> IO (Maybe (Expression, [Binding]))+declared univ ctx form = traced ctx._facts form >>= maybe (pure Nothing) placed where- fits :: [Binding] -> Bool- fits declared = all (`elem` map attributeFromBinding declared) [attributeFromBinding bd | bd <- bds, 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 _ <- bds, BiVoid attr `elem` declared], length (filter (`elem` declared) bds))- located :: Expression -> Expression -> Maybe Expression- located ExRoot whole = Just whole+ placed :: (Expression, [(Expression, Expression)]) -> IO (Maybe (Expression, [Binding]))+ placed (call, hops) = do+ recited ctx hops+ pure ((erased call,) <$> located (erased call) (fromMaybe univ ctx._universe))+ located :: Expression -> Expression -> Maybe [Binding]+ located ExRoot (ExFormation bds) = Just bds located (ExDispatch path attr) whole = case located path whole of- Just (ExFormation siblings) -> listToMaybe [body | BiTau attr' body <- siblings, attr' == attr]- _ -> Nothing+ Just siblings -> listToMaybe [inner | BiTau attr' (ExFormation inner) <- siblings, attr' == attr]+ Nothing -> Nothing located _ _ = Nothing erased :: Expression -> Expression erased (ExApplication target _) = erased target@@ -349,13 +451,16 @@ erased other = other argued :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> IO Expression-argued univ ctx state site bds = go+argued univ ctx state site bds call = foldl ExDispatch <$> go inner <*> pure attrs where+ attrs :: [Attribute]+ inner :: Expression+ (attrs, inner) = dispatched call go :: Expression -> IO Expression go (ExApplication target (ArTau attr body)) = do target' <- go target ExApplication target' . ArTau attr <$> reckoned attr body- go call = pure call+ go term = pure term reckoned :: Attribute -> Expression -> IO Expression reckoned _ body@(ExFormation [BiLambda (FnSymbol _)]) = pure body reckoned attr body = do@@ -366,10 +471,22 @@ named _ _ = False figured :: Expression -> Expression -> IO Expression figured place placed = unparked $ do- (normal, morphed) <- settled placed univ state =<< opening Morphing ctx{_site = place}- case normal of- ExFormation _ -> fst <$> fired univ ctx place morphed normal- _ -> pure normal+ (answer, state') <- worked place placed state+ if hanging answer+ then fst <$> worked (ExDispatch place AtPhi) (ExDispatch answer AtPhi) state'+ else pure answer+ where+ worked :: Expression -> Expression -> State -> IO (Expression, State)+ worked place' placed' state' = do+ (normal, morphed) <- settled placed' univ state' =<< opening Morphing ctx{_site = place'}+ case normal of+ ExFormation _+ | thrown ctx._raising normal -> pure (normal, morphed)+ | otherwise -> fired univ ctx place' morphed normal+ _ -> pure (normal, morphed)+ hanging :: Expression -> Bool+ hanging (ExFormation bds) = not (any isLambda bds) && or [not (xiFree body) | BiTau AtPhi body <- bds]+ hanging _ = False admitted :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext) admitted form ctx = maybe (pure (Right ctx)) remembered ctx._acyclic@@ -426,9 +543,10 @@ where go :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State) go (expr, seq) univ state caller = do- ctx <- opening Morphing =<< deeper =<< entering expr =<< parking seq state (universed univ caller{_judgment = Morphing})+ (term, entered) <- severing expr univ state =<< parking seq state (universed univ caller{_judgment = Morphing})+ ctx <- opening Morphing =<< deeper entered parking seq state $ do- reached <- inferred expr univ state ctx ctx._engine._morphing+ reached <- maybe (inferred term univ state ctx ctx._engine._morphing) (\raise -> pure (Just (In.Answered (Morphing, "raise") raise, state))) (raised term) case reached of Just (In.Answered step built, state') -> do when owner (ctx._saveEval (EvMorphed ctx._nesting built))@@ -437,7 +555,12 @@ Just (In.Onward way built world, state') -> do (morphed, state'') <- onward seq state' way built ctx go morphed world state'' ctx- Nothing -> throwIO (Unmorphable expr)+ Nothing -> throwIO (Unmorphable term)+ where+ raised :: Expression -> Maybe Expression+ raised (ExDispatch target@(ExFormation _) _)+ | thrown caller._raising target = Just target+ raised _ = Nothing morph :: Expression -> State -> ReduceContext -> IO (Expression, [Rewritten], State) morph universe state caller@ReduceContext{..} = do@@ -501,17 +624,65 @@ normalized :: Expression -> NonEmpty Rewritten -> ReduceContext -> IO (Expression, NonEmpty Rewritten) normalized expr seq ctx@ReduceContext{..} = do+ measured ctx expr whole <- withLocatedExpression _locator expr (fst (NE.head seq))- (rewrittens, exceeded) <- rewrite whole _engine._normalization (rewriteContext ctx)- when exceeded (throwIO (OutOfSteps (Cycles _maxCycles)))+ taken <- newIORef Map.empty+ peeled <- newIORef Map.empty+ (rewrittens, exceeded) <- rewrite whole _engine._normalization (rewriteContext taken peeled ctx)+ when exceeded $ do+ _saveEval (EvExceeded _nesting _maxCycles _judgment _site)+ throwIO (OutOfSteps (Cycles _maxCycles)) let (rw :| rws) = NE.reverse rewrittens seq' = rw :| rws <> NE.tail seq expr' <- locatedExpression _locator (fst rw) pure (expr', seq') where- rewriteContext :: ReduceContext -> RewriteContext- rewriteContext ReduceContext{..} =- RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing _saveStep (\redex object -> _saveEval (EvApplied _nesting _judgment (called _universe redex) object _site))+ rewriteContext :: IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> RewriteContext+ rewriteContext taken peeled whole@ReduceContext{..} =+ RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing (\term -> (measured whole =<< locatedExpression _locator term) >> _saveStep term) (made taken peeled whole)+ made :: IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> Expression -> Expression -> IO ()+ made _ _ whole redex@(ExApplication head' (ArTau attr _)) object@(ExFormation bds)+ | attr /= AtRho && object /= head' = do+ whole._saveEval (EvApplied whole._nesting whole._judgment (called whole._universe redex) object whole._site)+ known <- remembering whole._facts head'+ when (known && copied bds) (noted whole object redex)+ made taken _ whole redex@(ExApplication _ (ArTau AtRho _)) object@(ExFormation bds)+ | copied bds = do+ pending <- readIORef taken+ forM_ (lookup redex (Map.findWithDefault [] (hashExpression redex) pending)) (noted whole object)+ made taken peeled whole redex@(ExDispatch target attr) object+ | attr /= AtRho = do+ stripped peeled whole target attr+ dispatched taken peeled whole redex object+ made _ _ _ _ _ = pure ()+ stripped :: IORef (Store Expression) -> ReduceContext -> Expression -> Attribute -> IO ()+ stripped peeled whole target@(ExFormation bds) attr = do+ known <- remembering whole._facts target+ when known (modifyIORef' peeled (Map.insertWith (++) (hashExpression (left bds)) [(left bds, target)]))+ where+ left :: [Binding] -> Expression+ left inner = ExFormation [bd | bd <- inner, attributeFromBinding bd /= Just attr]+ stripped _ _ _ _ = pure ()+ dispatched :: IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> Expression -> Expression -> IO ()+ dispatched taken peeled whole redex object@(ExApplication (ExFormation bds) (ArTau AtRho _))+ | copied bds = sourced peeled whole redex >>= mapM_ (\path -> modifyIORef' taken (Map.insertWith (++) (hashExpression object) [(object, path)]))+ dispatched _ peeled whole redex object@(ExFormation bds)+ | copied bds = sourced peeled whole redex >>= mapM_ (noted whole object)+ dispatched _ _ _ _ _ = pure ()+ sourced :: IORef (Store Expression) -> ReduceContext -> Expression -> IO (Maybe Expression)+ sourced peeled whole redex@(ExDispatch target attr) = case worldly whole._universe redex of+ Just path -> pure (Just path)+ Nothing -> do+ known <- remembering whole._facts target+ held <- readIORef peeled+ pure (if known then Just redex else (`ExDispatch` attr) <$> lookup target (Map.findWithDefault [] (hashExpression target) held))+ sourced _ _ _ = pure Nothing+ copied :: [Binding] -> Bool+ copied bds = boxed bds || isJust (lambda bds)+ worldly :: Maybe Expression -> Expression -> Maybe Expression+ worldly universe (ExDispatch target attr) = (`ExDispatch` attr) <$> worldly universe target+ worldly _ ExRoot = Just ExRoot+ worldly universe target = ExRoot <$ guard (Just target == universe) called :: Maybe Expression -> Expression -> Expression called universe (ExApplication head' arg) = ExApplication (nameIn universe head') arg called _ redex = redex@@ -519,7 +690,7 @@ universed :: Expression -> ReduceContext -> IO ReduceContext universed _ ctx@ReduceContext{_universe = Just _} = pure ctx universed univ ctx = do- (normal, _) <- normalized univ ((univ, Nothing) :| []) ctx{_locator = ExRoot, _saveStep = dontSaveStep}+ (normal, _) <- normalized univ ((univ, Nothing) :| []) ctx{_locator = ExRoot, _maxNodes = Nothing, _saveStep = dontSaveStep} ctx._saveEval (EvWorld normal) pure ctx{_universe = Just normal} @@ -563,11 +734,10 @@ recurring :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) recurring term@(ExFormation bds) world state' opened | Just mode <- opened._acyclic- , boxed bds- , Just call <- called world opened bds = do+ , boxed bds = do hits <- repeats mode term opened case drop opened._maxLoops hits of- before : _ -> (,state') <$> severed world opened state' term bds call (mode, before)+ before : _ -> (,state') <$> severed Nothing world opened state' term bds (mode, before) [] | null hits -> pure (term, state') | otherwise -> pure (term, state'{_copies = state'._copies ++ [term]})
src/Regexp.hs view
@@ -6,7 +6,7 @@ import Control.Exception import Data.Array (bounds, (!)) import qualified Data.ByteString.Char8 as B-import Data.Char (isDigit, ord)+import Data.Char (digitToInt, isDigit, ord) import Data.Maybe (fromMaybe) import Text.Read (readMaybe) import qualified Text.Regex.PCRE.ByteString as R@@ -67,6 +67,9 @@ Nothing -> B.pack ('$' : digits) Just idx -> fromMaybe (B.pack ('$' : digits)) (safeIndex idx groups) in val : go afterDigits+ go ('\\' : '\\' : rest) = B.singleton '\\' : go rest+ go ('\\' : digit : rest)+ | isDigit digit = fromMaybe (B.pack ['\\', digit]) (safeIndex (toInteger (digitToInt digit)) groups) : go rest go (c : rest) = B.singleton c : go rest safeIndex :: Integer -> [B.ByteString] -> Maybe B.ByteString safeIndex i xs
src/Rewriter.hs view
@@ -228,7 +228,7 @@ ) updated <- withLocatedExpression _locator expr current _saveStep updated- mapM_ (uncurry _saveMade) [(redex, object) | (redex@(ExApplication head' (ArTau attr _)), object@(ExFormation _)) <- rewritten, attr /= AtRho, object /= head']+ mapM_ (uncurry _saveMade) rewritten _rewrite (leadsTo updated, expr, seenInsert digest expr _unique, False, Nothing) (_count + 1) where leadsTo :: Expression -> NonEmpty Rewritten@@ -263,7 +263,7 @@ rewrite :: Expression -> [Step] -> RewriteContext -> IO Rewrittens rewrite expr rules ctx@RewriteContext{..} = do located <- locatedExpression _locator expr- (rewrittens, exceeded) <- _rewrite ((expr, Nothing) :| [], located, Map.empty, False, Nothing) 0+ (rewrittens, exceeded) <- _rewrite ((expr, Nothing) :| [], located, seenInsert (hashExpression located) located Map.empty, False, Nothing) 0 pure (NE.reverse rewrittens, exceeded) where _rewrite :: RewriteState -> Int -> IO Rewrittens
src/Rule.hs view
@@ -11,7 +11,7 @@ import AST import Builder ( buildAttribute- , buildBindingThrows+ , buildBinding , buildBindingUnchecked , buildExpression , buildExpressionThrows@@ -21,7 +21,8 @@ import Control.Exception.Base (SomeException, try) import Control.Monad (when) import Data.Foldable (foldlM)-import Data.List (foldl', intersect, nub)+import Data.List (intersect, nub)+import qualified Data.List as List import qualified Data.Map.Strict as M import Data.Maybe (catMaybes) import qualified Data.Text as T@@ -233,17 +234,24 @@ _matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup (Named meta) mp of Just (MvExpression expr) -> _matches pat expr (Subst mp) ctx _ -> pure []-_matches pat expr subst ctx = do- (TeBytes tgt) <- _buildTerm ctx "dataize" [Y.ArgExpression expr] subst- matched <- match (T.encodeUtf8 (T.pack pat)) (T.encodeUtf8 (T.pack (btsToUnescapedStr tgt)))- pure [subst | matched]+_matches pat expr subst ctx = case buildExpression expr subst of+ Right built -> do+ (TeBytes tgt) <- _buildTerm ctx "dataize" [Y.ArgExpression built] subst+ matched <- match (T.encodeUtf8 (T.pack pat)) (T.encodeUtf8 (T.pack (btsToUnescapedStr tgt)))+ pure [subst | matched]+ Left err -> do+ logDebug (printf "Condition matches(%s, %s) can't be built and was treated as not met: %s" (printExpression expr) pat err)+ pure [] _partOf :: Expression -> Binding -> Subst -> RuleContext -> IO [Subst]-_partOf exp bd subst _ = do- exp' <- buildExpressionThrows exp subst- bds <- buildBindingThrows bd subst- pure [subst | partOf exp' bds]+_partOf exp bd subst _ = case (buildExpression exp subst, buildBinding bd subst) of+ (Right exp', Right bds) -> pure [subst | partOf exp' bds]+ (_, Left err) -> unbuilt err+ (Left err, _) -> unbuilt err where+ unbuilt err = do+ logDebug (printf "Condition part-of(%s, %s) can't be built and was treated as not met: %s" (printExpression exp) (printBinding bd) err)+ pure [] partOf :: Expression -> [Binding] -> Bool partOf _ [] = False partOf expr (BiTau _ (ExFormation bds) : rest) = expr == ExFormation bds || partOf expr bds || partOf expr rest@@ -396,7 +404,7 @@ demanded bds (Y.In attrs metas) | all (\meta -> isMeta meta && meta `elem` bds) metas = attrs demanded bds (Y.And conds) = concatMap (demanded bds) conds- demanded bds (Y.Or (cond : conds)) = foldl' (\attrs cond' -> attrs `intersect` demanded bds cond') (demanded bds cond) conds+ demanded bds (Y.Or (cond : conds)) = List.foldl' (\attrs cond' -> attrs `intersect` demanded bds cond') (demanded bds cond) conds demanded _ _ = [] isMeta :: Binding -> Bool isMeta (BiMeta _) = True
src/Yaml.hs view
@@ -19,6 +19,8 @@ import qualified Data.Aeson.KeyMap as KeyMap import Data.Aeson.Types (formatRelativePath) import qualified Data.ByteString as BS+import Data.Conduit ((.|))+import qualified Data.Conduit.List as CL import Data.FileEmbed (embedDir) import Data.Maybe (fromMaybe) import Data.Scientific (isInteger)@@ -26,11 +28,12 @@ import qualified Data.Text as T import Data.Yaml (Parser) import qualified Data.Yaml as Yaml-import Data.Yaml.Internal (Warning (DuplicateKey))+import Data.Yaml.Internal (Warning (DuplicateKey), decodeHelper_) import GHC.Generics (Generic) import Metas import Parser import Slots+import qualified Text.Libyaml as Libyaml import Text.Printf (printf) import Text.Regex.PCRE ((=~)) @@ -127,7 +130,9 @@ parseJSON _ = fail "An argument of 'eq' or 'gt' is a number, an attribute, an expression, or an object of 'length' or 'domain'" instance FromJSON Condition where- parseJSON = withObject "Condition" parseCondition+ parseJSON = withObject "Condition" $ \v -> do+ cond <- parseCondition v+ cond <$ either fail pure (wellCompared cond) parseCondition :: Object -> Parser Condition parseCondition v = do@@ -184,6 +189,28 @@ several :: FromJSON a => Value -> Parser [a] several val = parseJSON val <|> (pure <$> parseJSON val) +kindOf :: Comparable -> String+kindOf (CmpNum _) = "a number"+kindOf (CmpAttr _) = "an attribute"+kindOf (CmpExpr _) = "an expression"++wellCompared :: Condition -> Either String ()+wellCompared = \case+ And conds -> mapM_ wellCompared conds+ Or conds -> mapM_ wellCompared conds+ Not cond -> wellCompared cond+ Eq left right+ | kindOf left == kindOf right -> Right ()+ | otherwise -> mismatch "eq" "two numbers, two attributes or two expressions" left right+ Gt left right+ | kindOf left == "a number" && kindOf right == "a number" -> Right ()+ | otherwise -> mismatch "gt" "two numbers" left right+ _ -> Right ()+ where+ mismatch :: String -> String -> Comparable -> Comparable -> Either String ()+ mismatch verb allowed left right =+ Left (printf "The '%s' condition compares %s with %s, while it can compare only %s" verb (kindOf left) (kindOf right) allowed)+ instance FromJSON ExtraArgument where parseJSON v@(String _) = foldr1@@ -508,11 +535,17 @@ yamlRule :: FilePath -> IO Rule yamlRule path = do- decoded <- Yaml.decodeFileWithWarnings path+ decoded <- decodeHelper_ (Libyaml.decodeFile path .| CL.map worded) case decoded of Left err -> throwIO err Right (warnings, rule) -> rule <$ mapM_ reportDuplicateKey warnings where+ worded :: Libyaml.Event -> Libyaml.Event+ worded (Libyaml.EventScalar value Libyaml.NoTag style anchor)+ | value `elem` spelled = Libyaml.EventScalar value Libyaml.StrTag style anchor+ worded event = event+ spelled :: [BS.ByteString]+ spelled = ["y", "Y", "yes", "Yes", "YES", "n", "N", "no", "No", "NO", "on", "On", "ON", "off", "Off", "OFF"] reportDuplicateKey :: Warning -> IO () reportDuplicateKey (DuplicateKey jsonPath) = fail (printf "The key '%s' is repeated in the rule file '%s', only the last value is kept" (formatRelativePath jsonPath) path)
test-resources/cli/rules/join-broken.yaml view
@@ -6,9 +6,9 @@ # correctly (it used to say "'go" instead of "join()"). name: uses-join-on-non-binding pattern: '!e2'-result: '!e1'+result: '[[ !B1 ]]' where:- - meta: '!e1'+ - meta: '!B1' function: join args: - 'some-text'
+ test-resources/cli/rules/kind-dataize-to-expression.yaml view
@@ -0,0 +1,12 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# Binds the bytes that dataize returns to an expression meta.+name: dataize-to-expression+pattern: "⟦ foo ↦ 𝑒1 ⟧"+result: "⟦ foo ↦ 𝑒2 ⟧"+where:+ - meta: "𝑒2"+ function: dataize+ args:+ - "𝑒1"
+ test-resources/cli/rules/kind-size-to-attribute.yaml view
@@ -0,0 +1,12 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# Binds the number that size returns to an attribute meta.+name: size-to-attribute+pattern: "⟦ 𝐵1, foo ↦ 𝑒1 ⟧"+result: "⟦ 𝜏2 ↦ 𝑒1 ⟧"+where:+ - meta: "𝜏2"+ function: size+ args:+ - "𝐵1"
+ test-resources/cli/rules/kind-tau-to-attribute.yaml view
@@ -0,0 +1,10 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# Binds the attribute that random-tau returns to an attribute meta.+name: tau-to-attribute+pattern: "⟦ foo ↦ 𝑒1 ⟧"+result: "⟦ 𝜏2 ↦ 𝑒1 ⟧"+where:+ - meta: "𝜏2"+ function: random-tau
+ test-resources/cli/rules/kind-tau-to-expression.yaml view
@@ -0,0 +1,10 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# Binds the attribute that random-tau returns to an expression meta.+name: tau-to-expression+pattern: "⟦ foo ↦ 𝑒1 ⟧"+result: "⟦ foo ↦ 𝑒2 ⟧"+where:+ - meta: "𝑒2"+ function: random-tau
− test-resources/condition-packs/eq-mismatched-comparable-kinds.yaml
@@ -1,10 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----expression: '[[ x -> "Hello" ]]'-pattern: '[[ x -> !e1 ]]'-condition:- not:- eq:- - foo- - '"Hello"'
− test-resources/condition-packs/gt-non-numeric.yaml
@@ -1,8 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----expression: '[[ x -> Q.y, z -> Q.z ]]'-pattern: '[[ x -> !e1, z -> !e2 ]]'-condition:- not:- gt: ['!e1', '!e2']
+ test-resources/condition-packs/matches-non-data.yaml view
@@ -0,0 +1,8 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+failure: true+expression: '[[ x -> Q.z ]]'+pattern: '[[ x -> !e1 ]]'+condition:+ matches: ['Q', '!e1']
+ test-resources/condition-packs/matches-unbound-nested-meta.yaml view
@@ -0,0 +1,8 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+failure: true+expression: '[[ x -> Q.y ]]'+pattern: '[[ x -> !e1 ]]'+condition:+ matches: ['Q', 'Q.x.!t9']
+ test-resources/condition-packs/part-of-unbound-meta.yaml view
@@ -0,0 +1,8 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+failure: true+expression: '[[ x -> Q.y ]]'+pattern: '[[ x -> !e1 ]]'+condition:+ part-of: ['!e1', '!B1']
+ test-resources/evaluate-packs/answers-a-firing-whose-operand-loops.yaml view
@@ -0,0 +1,43 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# A loop met while an operand is being brought down to data, one whole run of 𝔻+# below the spine. The operand dispatches 'foo' off a formation of 'L_loop',+# whose firing answers that very formation, so 𝕄 is about to dispatch off it+# again. The cut answers the whole dispatch with a fresh symbol, named by the+# symbol alone, since no fact leads that formation back to the world (#2307).+# The operand comes down to the datum of the symbol and 'L_outer' answers, and+# the dispatch of 'bar' off its answer is what the run parks on.+symbolic: |+ - λ: L_outer+ dataize:+ 𝛿1: ξ.arg+ 𝑛: ⟦ λ ⤍ 𝜎 ⟧+ - λ: L_loop+ 𝑛: ⟦ λ ⤍ L_loop ⟧+location: 'Q.x'+acyclic: proven+steps: 250+partial: true+input: >+ ⟦ x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_loop ⟧.foo, λ ⤍ L_outer ⟧.bar ⟧+result: '𝜎2:λ.bar'+protocol: |+ 𝕄(Φ.x):+ 𝔼(L_outer):+ 𝔻(ξ.arg):+ 𝕄(ξ.arg):+ 𝔼(L_loop):+ 𝑛·2·1 := L_loop:λ # 𝑛+ 𝕄(𝑛·2·1):+ morphed 𝑛·2·2 := L_loop:λ+ 𝑛·2·3 := L_loop:λ # 𝕄(𝑛·2·1)+ looped 𝜎1 # proven, repeats L_loop:λ+ morphed 𝑛·1·1 := 𝜎1:λ+ 𝛿·1·1 := 𝔻(𝜎1:λ)+ 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.arg)+ 𝑛·1·2 := 𝜎2:λ # 𝑛+ 𝕄(𝑛·1·2):+ morphed 𝑛·1·3 := 𝜎2:λ+ 𝑛·1·4 := 𝑛·1·3 # 𝕄(𝑛·1·2)+ unanswered 𝜎2 # 𝕄(𝜎2:λ)
test-resources/evaluate-packs/answers-an-operand-that-dataizes-in-circles-with-a-symbol.yaml view
@@ -27,21 +27,25 @@ 𝔼(L_outer): 𝔻(ξ.arg): 𝕄(ξ.arg):- 𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )- 𝑛·1·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧- morphed 𝑛·1·3 := 𝑛·1·2- boxed 𝑛·1·4 := 𝑛·1·3.φ- 𝕄(𝑛·1·4):- 𝑛·1·5 := Φ.cyc( x ↦ ⟦⟧ )- 𝑛·1·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧- morphed 𝑛·1·7 := 𝑛·1·6- 𝕄(𝑛·1·7.x):- morphed 𝑛·1·8 := ⟦⟧- looped 𝜎1 := Φ.cyc( x ↦ 𝑛·1·8 ) # 𝔻(𝑛·1·4), proven, repeats 𝑛·1·7+ remembered 𝑛·1·1 ≡ Φ.cyc # ⟦ x ↦ ∅, φ ↦ Φ.cyc( x ) ⟧+ 𝑛·1·2 := Φ.cyc( x ↦ ⟦⟧ )+ 𝑛·1·3 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( x ↦ ⟦⟧ )+ morphed 𝑛·1·4 := 𝑛·1·3+ boxed 𝑛·1·5 := 𝑛·1·4.φ+ 𝕄(𝑛·1·5):+ 𝑛·1·6 := Φ.cyc( x ↦ ⟦⟧ )+ 𝑛·1·7 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+ morphed 𝑛·1·8 := 𝑛·1·7+ recalled 𝑛·1·3 ⇒ 𝑛·1·1( x ↦ ⟦⟧ )+ recalled 𝑛·1·1 ⇒ Φ.cyc+ 𝕄(𝑛·1·8.x):+ morphed 𝑛·1·9 := ⟦⟧+ looped 𝜎1 := Φ.cyc( x ↦ 𝑛·1·9 ) # 𝔻(𝑛·1·5), proven, repeats 𝑛·1·8 𝛿·1·1 := 𝔻(𝜎1:λ) 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.arg)- 𝑛·1·9 := 𝜎2:λ:bar # 𝑛- 𝕄(𝑛·1·9):- morphed 𝑛·1·10 := 𝜎2:λ:bar- 𝑛·1·11 := 𝑛·1·10 # 𝕄(𝑛·1·9)+ 𝑛·1·10 := 𝜎2:λ:bar # 𝑛+ 𝕄(𝑛·1·10):+ morphed 𝑛·1·11 := 𝜎2:λ:bar+ 𝑛·1·12 := 𝑛·1·11 # 𝕄(𝑛·1·10) morphed 𝑛·0·1 := 𝜎2:λ
+ test-resources/evaluate-packs/answers-bottom-for-a-meta-that-raises.yaml view
@@ -0,0 +1,31 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The entry 'L_wrap' morphs its operand 'x', a copy of 'throw', and then+# brings the meta it bound down to data. The λ function 'L_throw' is one of+# its 'terminators', and data that comes from something that raises is the+# same raise, so 'L_wrap' answers ⊥ and never fires 'L_throw' (#2330).+symbolic: |+ - λ: L_wrap+ terminators: [L_throw]+ morph:+ 𝑛1: $.x+ dataize:+ 𝛿1: 𝑛1+ 𝑛: ⟦ λ ⤍ 𝜎 ⟧+location: 'Q.y'+input: '⟦ wrap(x) ↦ ⟦ λ ⤍ L_wrap ⟧, y ↦ Φ.wrap( ⟦ λ ⤍ L_throw ⟧ ).φ ⟧'+result: '⊥'+protocol: |+ 𝕄(Φ.y):+ remembered 𝑛·0·1 ≡ Φ.wrap # ⟦ x ↦ ∅, λ ⤍ L_wrap ⟧+ 𝑛·0·2 := Φ.wrap( x ↦ L_throw:λ )+ 𝑛·0·3 := ⟦ x ↦ L_throw:λ, λ ⤍ L_wrap ⟧+ remembered 𝑛·0·3 ≡ 𝑛·0·1( x ↦ L_throw:λ )+ 𝔼(L_wrap):+ 𝕄(ξ.x):+ morphed 𝑛·1·1 := L_throw:λ+ 𝑛1·1 := L_throw:λ # 𝕄(ξ.x)+ 𝑛·1·2 := ⊥+ morphed 𝑛·0·4 := ⊥
test-resources/evaluate-packs/answers-its-own-sides-on-a-condition-another-join-read.yaml view
@@ -39,10 +39,13 @@ result: '⟦ φ ↦ ⟦ Δ ⤍ 40-51-80-00-00-00-00-00 ⟧ ⟧' protocol: | 𝕄(Φ.φ):- 𝑛·0·1 := Φ.pick( x ↦ 5.0.gt( 0.0 ).if( 7.0, 7.0 ) )- 𝑛·0·2 := ⟦ x ↦ 5.0.gt( 0.0 ).if( 7.0, 7.0 ), y ↦ ∅, λ ⤍ L_pick ⟧- 𝑛·0·3 := 𝑛·0·1( y ↦ 5.0.gt( 0.0 ).if( 70.0, 70.0 ) )- 𝑛·0·4 := ⟦ x ↦ 5.0.gt( 0.0 ).if( 7.0, 7.0 ), y ↦ 5.0.gt( 0.0 ).if( 70.0, 70.0 ), λ ⤍ L_pick ⟧+ remembered 𝑛·0·1 ≡ Φ.pick # ⟦ x ↦ ∅, y ↦ ∅, λ ⤍ L_pick ⟧+ 𝑛·0·2 := Φ.pick( x ↦ 5.0.gt( 0.0 ).if( 7.0, 7.0 ) )+ 𝑛·0·3 := ⟦ x ↦ 5.0.gt( 0.0 ).if( 7.0, 7.0 ), y ↦ ∅, λ ⤍ L_pick ⟧+ remembered 𝑛·0·3 ≡ 𝑛·0·1( x ↦ 5.0.gt( 0.0 ).if( 7.0, 7.0 ) )+ 𝑛·0·4 := 𝑛·0·2( y ↦ 5.0.gt( 0.0 ).if( 70.0, 70.0 ) )+ 𝑛·0·5 := ⟦ x ↦ 5.0.gt( 0.0 ).if( 7.0, 7.0 ), y ↦ 5.0.gt( 0.0 ).if( 70.0, 70.0 ), λ ⤍ L_pick ⟧+ remembered 𝑛·0·5 ≡ 𝑛·0·3( y ↦ 5.0.gt( 0.0 ).if( 70.0, 70.0 ) ) 𝔼(L_pick): 𝔻(ξ.x): 𝕄(ξ.x):@@ -83,6 +86,7 @@ 𝑛·2·19 := ⟦ φ ↦ 𝜎1:λ, if(then, else) ↦ L_fork:λ ⟧ morphed 𝑛·2·20 := 𝑛·2·19 𝑛·2·21 := 𝑛·2·20 # 𝕄(𝑛·2·17)+ memoized 𝑛·1·4 ⇛ 𝑛·2·21 𝑛·1·5 := 𝑛·2·18.if( then ↦ 7.0 ) 𝑛·1·6 := ⟦ then ↦ 7.0, else ↦ ∅, λ ⤍ L_fork ⟧ 𝑛·1·7 := 𝑛·1·5( else ↦ 7.0 )@@ -106,6 +110,7 @@ 𝑛·3·9 := ⟦ φ ↦ Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ ), gt(x) ↦ L_number_gt:λ ⟧ morphed 𝑛·3·10 := 𝑛·3·9 𝑛·3·11 := 𝑛·3·10+ memoized 𝑛·1·8 ⇛ 𝑛·3·11 boxed 𝑛·1·10 := 𝑛·3·11.φ 𝕄(𝑛·1·10): 𝑛·1·11 := Φ.bytes( φ ↦ 40-1C-00-00-00-00-00-00:Δ )@@ -120,6 +125,7 @@ 𝑛·1·17 := 𝑛·1·15.gt( x ↦ 𝑛·2·9 ) 𝑛·1·18 := ⟦ x ↦ 𝑛·2·9, λ ⤍ L_number_gt ⟧ 𝔼(L_number_gt):+ recalled 𝑛·1·4 ⇒ 𝑛·2·21 𝑛·4·1 := 𝑛·3·1 # 𝑛 𝑛·4·2 := 𝑛·2·21 # 𝕄(𝑛·4·1) 𝑛·1·19 := 𝑛·3·1.if( then ↦ 70.0 )@@ -146,11 +152,14 @@ 𝑛·5·9 := ⟦ φ ↦ Φ.bytes( φ ↦ 40-51-80-00-00-00-00-00:Δ ), gt(x) ↦ L_number_gt:λ ⟧ morphed 𝑛·5·10 := 𝑛·5·9 𝑛·5·11 := 𝑛·5·10+ memoized 𝑛·1·22 ⇛ 𝑛·5·11 𝑛2·1 := 𝑛·5·11 # 𝔼(𝑛1) 𝑛·1·24 := 𝑛·5·11 # 𝑛 𝕄(𝑛·1·24): morphed 𝑛·1·25 := 𝑛·5·11 𝑛·1·26 := 𝑛·1·25 # 𝕄(𝑛·1·24)- 𝑛·0·5 := Φ.bytes( φ ↦ 40-51-80-00-00-00-00-00:Δ )- 𝑛·0·6 := 40-51-80-00-00-00-00-00:Δ:φ- morphed 𝑛·0·7 := 𝑛·0·6+ remembered 𝑛·1·26 ≡ 𝑛·0·5+ memoized 𝑛·0·5 ⇛ 𝑛·1·26+ 𝑛·0·6 := Φ.bytes( φ ↦ 40-51-80-00-00-00-00-00:Δ )+ 𝑛·0·7 := 40-51-80-00-00-00-00-00:Δ:φ+ morphed 𝑛·0·8 := 𝑛·0·7
test-resources/evaluate-packs/answers-the-same-dataization-loop-under-partial.yaml view
@@ -24,21 +24,25 @@ 𝔼(L_outer): 𝔻(ξ.arg): 𝕄(ξ.arg):- 𝑛·1·1 := Φ.cyc( x ↦ ⟦⟧ )- 𝑛·1·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧- morphed 𝑛·1·3 := 𝑛·1·2- boxed 𝑛·1·4 := 𝑛·1·3.φ- 𝕄(𝑛·1·4):- 𝑛·1·5 := Φ.cyc( x ↦ ⟦⟧ )- 𝑛·1·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧- morphed 𝑛·1·7 := 𝑛·1·6- 𝕄(𝑛·1·7.x):- morphed 𝑛·1·8 := ⟦⟧- looped 𝜎1 := Φ.cyc( x ↦ 𝑛·1·8 ) # 𝔻(𝑛·1·4), proven, repeats 𝑛·1·7+ remembered 𝑛·1·1 ≡ Φ.cyc # ⟦ x ↦ ∅, φ ↦ Φ.cyc( x ) ⟧+ 𝑛·1·2 := Φ.cyc( x ↦ ⟦⟧ )+ 𝑛·1·3 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( x ↦ ⟦⟧ )+ morphed 𝑛·1·4 := 𝑛·1·3+ boxed 𝑛·1·5 := 𝑛·1·4.φ+ 𝕄(𝑛·1·5):+ 𝑛·1·6 := Φ.cyc( x ↦ ⟦⟧ )+ 𝑛·1·7 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧+ morphed 𝑛·1·8 := 𝑛·1·7+ recalled 𝑛·1·3 ⇒ 𝑛·1·1( x ↦ ⟦⟧ )+ recalled 𝑛·1·1 ⇒ Φ.cyc+ 𝕄(𝑛·1·8.x):+ morphed 𝑛·1·9 := ⟦⟧+ looped 𝜎1 := Φ.cyc( x ↦ 𝑛·1·9 ) # 𝔻(𝑛·1·5), proven, repeats 𝑛·1·8 𝛿·1·1 := 𝔻(𝜎1:λ) 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.arg)- 𝑛·1·9 := 𝜎2:λ:bar # 𝑛- 𝕄(𝑛·1·9):- morphed 𝑛·1·10 := 𝜎2:λ:bar- 𝑛·1·11 := 𝑛·1·10 # 𝕄(𝑛·1·9)+ 𝑛·1·10 := 𝜎2:λ:bar # 𝑛+ 𝕄(𝑛·1·10):+ morphed 𝑛·1·11 := 𝜎2:λ:bar+ 𝑛·1·12 := 𝑛·1·11 # 𝕄(𝑛·1·10) morphed 𝑛·0·1 := 𝜎2:λ
test-resources/evaluate-packs/binds-a-copy-over-no-bare-symbol-as-it-is.yaml view
@@ -20,12 +20,14 @@ 𝕄(Φ.y): 𝔼(L_hold): 𝕄(ξ.b):- 𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail )- 𝑛·1·2 := ⟦ tup ↦ Φ.items.tail, φ ↦ tup.next ⟧- morphed 𝑛·1·3 := 𝑛·1·2- 𝑛1·1 := 𝑛·1·3 # 𝕄(ξ.b)- 𝑛·1·4 := 𝑛·1·3:φ # 𝑛- 𝕄(𝑛·1·4):- morphed 𝑛·1·5 := 𝑛·1·3:φ- 𝑛·1·6 := 𝑛·1·5 # 𝕄(𝑛·1·4)- morphed 𝑛·0·1 := 𝑛·1·3+ remembered 𝑛·1·1 ≡ Φ.step # ⟦ tup ↦ ∅, φ ↦ tup.next ⟧+ 𝑛·1·2 := Φ.step( tup ↦ Φ.items.tail )+ 𝑛·1·3 := ⟦ tup ↦ Φ.items.tail, φ ↦ tup.next ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( tup ↦ Φ.items.tail )+ morphed 𝑛·1·4 := 𝑛·1·3+ 𝑛1·1 := 𝑛·1·4 # 𝕄(ξ.b)+ 𝑛·1·5 := 𝑛·1·4:φ # 𝑛+ 𝕄(𝑛·1·5):+ morphed 𝑛·1·6 := 𝑛·1·4:φ+ 𝑛·1·7 := 𝑛·1·6 # 𝕄(𝑛·1·5)+ morphed 𝑛·0·1 := 𝑛·1·4
+ test-resources/evaluate-packs/cuts-a-loop-met-at-a-dispatch-off-an-atom.yaml view
@@ -0,0 +1,66 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# A loop found where 𝕄 is about to dispatch 'q' off a copy of the atom+# 'L_times', under '--acyclic=plausible'. The operand of 'L_dataized' reads+# 'Φ.x.q' again, so the dispatch repeats the one above it. The cut answers the+# whole dispatch with a fresh symbol, named after the call the facts trace with+# 'q' on top, and leaves the argument of the call as it is, since working it+# out would run into the same loop again (#2307). Both firings then answer.+symbolic: |+ - λ: L_times+ dataize:+ 𝛿1: $.b+ 𝑛: ⟦ λ ⤍ 𝜎 ⟧+ - λ: L_dataized+ dataize:+ 𝛿1: $.target+ 𝑛: ⟦ λ ⤍ 𝜎 ⟧+location: 'Q.y'+acyclic: plausible+partial: true+input: >+ ⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧,+ times(b) ↦ ⟦ λ ⤍ L_times ⟧,+ x ↦ Φ.times( Φ.dataized( Φ.x.q ) ),+ y ↦ Φ.x.q ⟧+result: '𝜎3:λ.q'+protocol: |+ 𝕄(Φ.y):+ remembered 𝑛·0·1 ≡ Φ.times # ⟦ b ↦ ∅, λ ⤍ L_times ⟧+ 𝑛·0·2 := Φ.times( b ↦ Φ.dataized( Φ.x.q ) )+ 𝑛·0·3 := ⟦ b ↦ Φ.dataized( Φ.x.q ), λ ⤍ L_times ⟧+ remembered 𝑛·0·3 ≡ 𝑛·0·1( b ↦ Φ.dataized( Φ.x.q ) )+ 𝔼(L_times):+ 𝔻(ξ.b):+ 𝕄(ξ.b):+ remembered 𝑛·1·1 ≡ Φ.dataized # ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧+ 𝑛·1·2 := Φ.dataized( target ↦ Φ.x.q )+ 𝑛·1·3 := ⟦ target ↦ Φ.x.q, λ ⤍ L_dataized ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( target ↦ Φ.x.q )+ morphed 𝑛·1·4 := 𝑛·1·3+ 𝔼(L_dataized):+ 𝔻(ξ.target):+ 𝕄(ξ.target):+ 𝑛·2·1 := Φ.times( b ↦ Φ.dataized( Φ.x.q ) )+ 𝑛·2·2 := ⟦ b ↦ Φ.dataized( Φ.x.q ), λ ⤍ L_times ⟧+ recalled 𝑛·0·3 ⇒ 𝑛·0·1( b ↦ Φ.dataized( Φ.x.q ) )+ recalled 𝑛·0·1 ⇒ Φ.times+ looped 𝜎1 := 𝑛·2·1.q # plausible, repeats 𝑛·2·2+ morphed 𝑛·2·3 := 𝜎1:λ+ 𝛿·2·1 := 𝔻(𝜎1:λ)+ 𝛿1·2 := 𝛿·2·1 # 𝔻(ξ.target)+ 𝑛·2·4 := 𝜎2:λ # 𝑛+ 𝕄(𝑛·2·4):+ morphed 𝑛·2·5 := 𝜎2:λ+ 𝑛·2·6 := 𝑛·2·5 # 𝕄(𝑛·2·4)+ memoized 𝑛·1·3 ⇛ 𝜎2:λ+ 𝛿·1·1 := 𝔻(𝜎2:λ)+ 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.b)+ 𝑛·1·5 := 𝜎3:λ # 𝑛+ 𝕄(𝑛·1·5):+ morphed 𝑛·1·6 := 𝜎3:λ+ 𝑛·1·7 := 𝑛·1·6 # 𝕄(𝑛·1·5)+ memoized 𝑛·2·2 ⇛ 𝜎3:λ+ unanswered 𝜎3 # 𝕄(𝜎3:λ)
test-resources/evaluate-packs/cuts-a-recursion-running-through-evaluate-lines.yaml view
@@ -7,8 +7,10 @@ # fired from, and its 'evaluate' line fires that formation again. The line # enters the formation the way 'ml' does, so the second firing is cut before # it opens and writes a 'looped' line where its block would have stood-# (#1882). The budget of firings is there only to end the run if the cut-# is ever lost again.+# (#1882). The formation is a copy of 'Φ.loop', so the cut answers it with a+# fresh symbol (#2275), and the dispatch of φ off that symbol is parked. The+# budget of firings is there only to end the run if the cut is ever lost+# again. symbolic: | - λ: L_loop morph:@@ -18,13 +20,23 @@ 𝑛: 𝑛2 location: 'Q.app' acyclic: proven+partial: true firings: 5 input: '⟦ loop ↦ ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧, app ↦ Φ.loop.φ ⟧'-result: '⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧.φ'+result: '𝜎1:λ.φ' protocol: | 𝕄(Φ.app):+ remembered 𝑛·0·1 ≡ Φ.loop # ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧ 𝔼(L_loop): 𝕄(ξ.next🌵):- morphed 𝑛·1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧- 𝑛1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧ # 𝕄(ξ.next🌵)- looped ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧ # 𝔼(𝑛1), proven+ morphed 𝑛·1·1 := 𝑛·0·1+ 𝑛1·1 := 𝑛·0·1 # 𝕄(ξ.next🌵)+ recalled 𝑛·0·1 ⇒ Φ.loop+ recalled 𝑛·0·1 ⇒ Φ.loop+ looped 𝜎1 := Φ.loop # 𝔼(𝑛1), proven, repeats 𝑛·0·1+ 𝑛2·1 := 𝜎1:λ # 𝔼(𝑛1)+ 𝑛·1·2 := 𝑛2·1 # 𝑛+ 𝕄(𝑛·1·2):+ morphed 𝑛·1·3 := 𝑛2·1+ 𝑛·1·4 := 𝑛2·1 # 𝕄(𝑛·1·2)+ unanswered 𝜎1 # 𝕄(𝜎1:λ)
test-resources/evaluate-packs/cuts-a-recursion-that-differs-by-symbols-only.yaml view
@@ -10,7 +10,9 @@ # compares by (#1420), and 'ml' enters the formation it fires, so the second # firing is cut before it opens and writes a 'looped' line where its block # would have stood, carrying the term of the round that was kept (#1434). The-# budget is generous here, so what ends the run is the cut and not the limit.+# cut answers the whole dispatch of 'φ' with a fresh symbol, named after the+# call the facts trace with 'φ' on top (#2307). The budget is generous here,+# so what ends the run is the cut and not the limit. symbolic: | - λ: L_down dataize:@@ -20,11 +22,13 @@ acyclic: proven steps: 250 input: '⟦ down ↦ ⟦ x ↦ ∅, λ ⤍ L_down ⟧, y ↦ Φ.down( x ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).φ ⟧'-result: '⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧.φ'+result: '𝜎3:λ' protocol: | 𝕄(Φ.y):- 𝑛·0·1 := Φ.down( x ↦ 𝜎1:λ )- 𝑛·0·2 := ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧+ remembered 𝑛·0·1 ≡ Φ.down # ⟦ x ↦ ∅, λ ⤍ L_down ⟧+ 𝑛·0·2 := Φ.down( x ↦ 𝜎1:λ )+ 𝑛·0·3 := ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧+ remembered 𝑛·0·3 ≡ 𝑛·0·1( x ↦ 𝜎1:λ ) 𝔼(L_down): 𝔻(ξ.x): 𝛿·1·1 := 𝔻(𝜎1:λ)@@ -33,6 +37,12 @@ 𝕄(𝑛·1·1): 𝑛·1·2 := Φ.down( x ↦ 𝜎2:λ ) 𝑛·1·3 := ⟦ x ↦ 𝜎2:λ, λ ⤍ L_down ⟧+ remembered 𝑛·1·3 ≡ 𝑛·0·1( x ↦ 𝜎2:λ ) morphed 𝑛·1·4 := 𝑛·1·3 𝑛·1·5 := 𝑛·1·3 # 𝕄(𝑛·1·1)- looped 𝑛·0·2 # proven+ remembered 𝑛·1·3 ≡ 𝑛·0·3+ recalled 𝑛·1·3 ⇒ 𝑛·0·3+ recalled 𝑛·0·3 ⇒ 𝑛·0·1( x ↦ 𝜎1:λ )+ recalled 𝑛·0·1 ⇒ Φ.down+ looped 𝜎3 := 𝑛·0·2.φ # proven, repeats 𝑛·0·3+ morphed 𝑛·0·4 := 𝜎3:λ
+ test-resources/evaluate-packs/cuts-an-entry-that-answers-with-a-firing-of-itself.yaml view
@@ -0,0 +1,25 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# The same entry answering with a firing of itself, under '_acyclic': morphing+# comes back to the very dispatch it is already reducing, so it stops there+# instead of going round until the budget is gone, and answers the dispatch+# with a fresh symbol (#2307). The budget is generous here, so what ends the+# run is the cut and not the limit.+symbolic: |+ - λ: L_loop+ 𝑛: ⟦ λ ⤍ L_loop ⟧+location: 'Q.x'+acyclic: proven+steps: 250+input: '⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo ⟧'+result: '𝜎1:λ'+protocol: |+ 𝕄(Φ.x):+ 𝔼(L_loop):+ 𝑛·1·1 := L_loop:λ # 𝑛+ 𝕄(𝑛·1·1):+ morphed 𝑛·1·2 := L_loop:λ+ 𝑛·1·3 := L_loop:λ # 𝕄(𝑛·1·1)+ looped 𝜎1 # proven, repeats L_loop:λ+ morphed 𝑛·0·1 := 𝜎1:λ
test-resources/evaluate-packs/defers-a-copy-a-join-passed-through-stay-and-symbolize.yaml view
@@ -50,15 +50,19 @@ morphed 𝑛·2·1 := 01-:Δ 𝑛1·2 := 01-:Δ # 𝕄(ξ.a) 𝕄(ξ.b):- 𝑛·2·2 := Φ.step( tup ↦ Φ.items.tail )- 𝑛·2·3 := ⟦ tup ↦ Φ.items.tail, φ ↦ tup.next ⟧- morphed 𝑛·2·4 := 𝑛·2·3- 𝑛2·2 := 𝑛·2·4 # 𝕄(ξ.b)+ remembered 𝑛·2·2 ≡ Φ.step # ⟦ tup ↦ ∅, φ ↦ tup.next ⟧+ 𝑛·2·3 := Φ.step( tup ↦ Φ.items.tail )+ 𝑛·2·4 := ⟦ tup ↦ Φ.items.tail, φ ↦ tup.next ⟧+ remembered 𝑛·2·4 ≡ 𝑛·2·2( tup ↦ Φ.items.tail )+ morphed 𝑛·2·5 := 𝑛·2·4+ 𝑛2·2 := 𝑛·2·5 # 𝕄(ξ.b) symbolized 𝜎3 := 01- 𝑛5·2 := 𝜎3:λ # symbolize(⟦ Δ ⤍ 01- ⟧)- deferred 𝜎4 := Φ.step( tup ↦ 𝜎1:λ ) # 𝕄(𝑛·2·4.φ)+ recalled 𝑛·2·4 ⇒ 𝑛·2·2( tup ↦ Φ.items.tail )+ recalled 𝑛·2·2 ⇒ Φ.step+ deferred 𝜎4 := Φ.step( tup ↦ 𝜎1:λ ) # 𝕄(𝑛·2·5.φ) joined 𝜎5 := 𝛿1·2 ? 𝜎3 : 𝜎4- 𝑛·2·5 := 𝜎5:λ+ 𝑛·2·6 := 𝜎5:λ 𝛿·1·1 := 𝔻(𝜎5:λ) 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.x) 𝑛·1·1 := Φ.num( φ ↦ 𝜎6:λ ) # 𝑛
test-resources/evaluate-packs/defers-a-copy-whose-phi-reads-nothing-of-its-own.yaml view
@@ -21,13 +21,17 @@ 𝕄(Φ.y): 𝔼(L_hold): 𝕄(ξ.b):- 𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail )- 𝑛·1·2 := ⟦ tup ↦ Φ.items.tail, φ ↦ Φ.done ⟧- morphed 𝑛·1·3 := 𝑛·1·2- 𝑛1·1 := 𝑛·1·3 # 𝕄(ξ.b)+ remembered 𝑛·1·1 ≡ Φ.step # ⟦ tup ↦ ∅, φ ↦ Φ.done ⟧+ 𝑛·1·2 := Φ.step( tup ↦ Φ.items.tail )+ 𝑛·1·3 := ⟦ tup ↦ Φ.items.tail, φ ↦ Φ.done ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( tup ↦ Φ.items.tail )+ morphed 𝑛·1·4 := 𝑛·1·3+ 𝑛1·1 := 𝑛·1·4 # 𝕄(ξ.b)+ recalled 𝑛·1·3 ⇒ 𝑛·1·1( tup ↦ Φ.items.tail )+ recalled 𝑛·1·1 ⇒ Φ.step deferred 𝜎2 := Φ.step( tup ↦ 𝜎1:λ ) # 𝕄(𝑛1.φ)- 𝑛·1·4 := 𝜎2:λ:φ # 𝑛- 𝕄(𝑛·1·4):- morphed 𝑛·1·5 := 𝜎2:λ:φ- 𝑛·1·6 := 𝑛·1·5 # 𝕄(𝑛·1·4)+ 𝑛·1·5 := 𝜎2:λ:φ # 𝑛+ 𝕄(𝑛·1·5):+ morphed 𝑛·1·6 := 𝜎2:λ:φ+ 𝑛·1·7 := 𝑛·1·6 # 𝕄(𝑛·1·5) morphed 𝑛·0·1 := 𝜎2:λ
test-resources/evaluate-packs/fails-on-an-operand-that-reaches-the-terminator.yaml view
@@ -57,6 +57,8 @@ 𝕄(ξ.v.φ): 𝑛·1·9 := Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ) 𝑛·1·10 := ⟦ data ↦ ∅, buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ), read ↦ Φ.dataized( target ↦ ρ.data.size ).as-bytes:φ ⟧- 𝑛·1·11 := Φ.dataized( target ↦ ⊥ )- 𝑛·1·12 := ⟦ target ↦ ⊥, λ ⤍ L_dataized ⟧+ remembered 𝑛·1·11 ≡ Φ.dataized # ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧+ 𝑛·1·12 := Φ.dataized( target ↦ ⊥ )+ 𝑛·1·13 := ⟦ target ↦ ⊥, λ ⤍ L_dataized ⟧+ remembered 𝑛·1·13 ≡ 𝑛·1·11( target ↦ ⊥ ) 𝔼(L_dataized):
test-resources/evaluate-packs/fires-a-formation-once-however-often-it-is-met.yaml view
@@ -109,6 +109,7 @@ 𝑛·3·19 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·3·20 := 𝑛·3·19 𝑛·3·21 := 𝑛·3·20 # 𝕄(𝑛·3·17)+ memoized 𝑛·2·12 ⇛ 𝑛·3·21 boxed 𝑛·2·14 := 𝑛·3·21.φ 𝛿·2·2 := 𝔻(𝜎1:λ) 𝛿2·2 := 𝛿·2·2 # 𝔻(ξ.x)@@ -118,8 +119,10 @@ 𝑛·2·17 := ⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·2·18 := 𝑛·2·17 𝑛·2·19 := 𝑛·2·18 # 𝕄(𝑛·2·15)+ memoized 𝑛·1·9 ⇛ 𝑛·2·19 𝑛3·1 := 𝑛·2·19 # 𝔼(𝑛1) 𝔼(L_number_plus): # 𝔼(𝑛2)+ recalled 𝑛·1·9 ⇒ 𝑛·2·19 𝑛·4·1 := 𝑛·2·16 # 𝑛 𝑛·4·2 := 𝑛3·1 # 𝕄(𝑛·4·1) 𝑛4·1 := 𝑛·4·2 # 𝔼(𝑛2)@@ -127,4 +130,5 @@ 𝕄(𝑛·1·11): morphed 𝑛·1·12 := ⟦ a ↦ 𝑛·4·2, b ↦ 𝑛·4·2 ⟧:φ 𝑛·1·13 := 𝑛·1·12 # 𝕄(𝑛·1·11)+ memoized 𝑛·1·14 ⇛ 𝑛·1·13 # ⟦ a ↦ 𝑛·2·1.plus( 𝑛·3·1.plus( 𝑛·3·9 ) ), b ↦ 𝑛·2·1.plus( 𝑛·3·1.plus( 𝑛·3·9 ) ), λ ⤍ L_pair ⟧ morphed 𝑛·0·1 := ⟦ a ↦ 𝑛·4·2, b ↦ 𝑛·4·2 ⟧
test-resources/evaluate-packs/fires-a-formation-written-in-place-after-a-stay-line.yaml view
@@ -29,6 +29,7 @@ 𝕄(Φ.y): 𝑛·0·1 := ⟦ v ↦ ∅, λ ⤍ L_box ⟧( v ↦ Φ.k ) 𝑛·0·2 := ⟦ v ↦ Φ.k, λ ⤍ L_box ⟧+ remembered 𝑛·0·3 ≡ Φ.x # ⟦ λ ⤍ L_probe, side🌵 ↦ 𝑛·0·2 ⟧ 𝔼(L_probe): 𝕄(ξ.side🌵): morphed 𝑛·1·1 := 𝑛·0·2
test-resources/evaluate-packs/fires-a-formation-written-in-place-with-its-voids-filled.yaml view
@@ -34,6 +34,7 @@ 𝕄(Φ.y): 𝑛·0·1 := ⟦ v ↦ ∅, λ ⤍ L_box ⟧( v ↦ 𝜎2:λ ) 𝑛·0·2 := ⟦ v ↦ 𝜎2:λ, λ ⤍ L_box ⟧+ remembered 𝑛·0·3 ≡ Φ.x # ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ 𝑛·0·2, right🌵 ↦ 𝜎3:λ ⟧ 𝔼(L_fork): 𝔻(ξ.on🌵): 𝛿·1·1 := 𝔻(𝜎1:λ)
test-resources/evaluate-packs/fires-the-arguments-of-a-copy-a-defer-line-defers.yaml view
@@ -43,16 +43,22 @@ morphed 𝑛·2·1 := 𝜎3:λ 𝑛1·2 := 𝑛·2·1 # 𝕄(ξ.a) 𝕄(ξ.b):- 𝑛·2·2 := Φ.box( x ↦ Φ.items.tail )- 𝑛·2·3 := ⟦ x ↦ Φ.items.tail, w ↦ ∅, φ ↦ x.next ⟧- 𝑛·2·4 := 𝑛·2·2( w ↦ Φ.inc( 2A-:Δ ) )- 𝑛·2·5 := ⟦ x ↦ Φ.items.tail, w ↦ Φ.inc( 2A-:Δ ), φ ↦ x.next ⟧- morphed 𝑛·2·6 := 𝑛·2·5- 𝑛2·2 := 𝑛·2·6 # 𝕄(ξ.b)+ remembered 𝑛·2·2 ≡ Φ.box # ⟦ x ↦ ∅, w ↦ ∅, φ ↦ x.next ⟧+ 𝑛·2·3 := Φ.box( x ↦ Φ.items.tail )+ 𝑛·2·4 := ⟦ x ↦ Φ.items.tail, w ↦ ∅, φ ↦ x.next ⟧+ remembered 𝑛·2·4 ≡ 𝑛·2·2( x ↦ Φ.items.tail )+ 𝑛·2·5 := 𝑛·2·3( w ↦ Φ.inc( 2A-:Δ ) )+ 𝑛·2·6 := ⟦ x ↦ Φ.items.tail, w ↦ Φ.inc( 2A-:Δ ), φ ↦ x.next ⟧+ remembered 𝑛·2·6 ≡ 𝑛·2·4( w ↦ Φ.inc( 2A-:Δ ) )+ morphed 𝑛·2·7 := 𝑛·2·6+ 𝑛2·2 := 𝑛·2·7 # 𝕄(ξ.b)+ recalled 𝑛·2·6 ⇒ 𝑛·2·4( w ↦ Φ.inc( 2A-:Δ ) )+ recalled 𝑛·2·4 ⇒ 𝑛·2·2( x ↦ Φ.items.tail )+ recalled 𝑛·2·2 ⇒ Φ.box 𝕄(𝑛2.w):- 𝑛·2·7 := Φ.inc( x ↦ 2A-:Δ )- 𝑛·2·8 := ⟦ x ↦ 2A-:Δ, λ ⤍ L_inc ⟧- morphed 𝑛·2·9 := 𝑛·2·8+ 𝑛·2·8 := Φ.inc( x ↦ 2A-:Δ )+ 𝑛·2·9 := ⟦ x ↦ 2A-:Δ, λ ⤍ L_inc ⟧+ morphed 𝑛·2·10 := 𝑛·2·9 𝔼(L_inc): # 𝔼(𝑛2.w) 𝔻(ξ.x): 𝛿·3·1 := 2A-@@ -63,9 +69,10 @@ 𝑛·3·3 := 𝜎4:λ:φ morphed 𝑛·3·4 := 𝑛·3·3 𝑛·3·5 := 𝑛·3·4 # 𝕄(𝑛·3·1)+ remembered 𝑛·3·5 ≡ 𝑛·2·9 deferred 𝜎5 := Φ.box( x ↦ 𝜎1:λ, w ↦ 𝑛·3·5 ) # 𝕄(𝑛2.φ) joined 𝜎6 := 𝛿1·2 ? 𝜎3 : 𝜎5- 𝑛·2·10 := 𝜎6:λ+ 𝑛·2·11 := 𝜎6:λ 𝛿·1·1 := 𝔻(𝜎6:λ) 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.x) 𝑛·1·1 := Φ.num( φ ↦ 𝜎7:λ ) # 𝑛
test-resources/evaluate-packs/joins-a-side-a-morph-line-brought-down-from-what-a-rewrite-line-unwrapped.yaml view
@@ -48,8 +48,9 @@ 𝑛2·1 := 𝑛·1·2 # 𝕄(ξ.b) 𝑛3·1 := Φ.t # rewrite(𝑛2) 𝕄(𝑛3):- morphed 𝑛·1·3 := 𝜎3:λ:φ- 𝑛4·1 := 𝑛·1·3 # 𝕄(𝑛3)+ remembered 𝑛·1·3 ≡ Φ.t # 𝜎3:λ:φ+ morphed 𝑛·1·4 := 𝑛·1·3+ 𝑛4·1 := 𝑛·1·4 # 𝕄(𝑛3) joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3- 𝑛·1·4 := 𝜎4:λ:φ+ 𝑛·1·5 := 𝜎4:λ:φ morphed 𝑛·0·1 := 𝜎4:λ
test-resources/evaluate-packs/joins-a-side-reading-the-rho-it-binds-in-a-fabricated-formation.yaml view
@@ -34,13 +34,15 @@ 𝛿·1·1 := 𝔻(𝜎1:λ) 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.c) 𝕄(ξ.a):- morphed 𝑛·1·1 := ⟦ tu ↦ ∅, φ ↦ ρ.s ⟧+ remembered 𝑛·1·1 ≡ Φ.t # ⟦ tu ↦ ∅, φ ↦ ρ.s ⟧+ morphed 𝑛·1·2 := 𝑛·1·1 𝕄(ξ.b):- morphed 𝑛·1·2 := 𝜎3:λ:k:φ- fabricated 𝑛·1·3 := 𝑛·1·1 and 𝑛·1·2 # ⟦ tu ↦ ∅, left🌵 ↦ 𝑛·1·1( tu ↦ tu ), right🌵 ↦ 𝑛·1·2, φ ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧ ⟧+ morphed 𝑛·1·3 := 𝜎3:λ:k:φ+ fabricated 𝑛·1·4 := 𝑛·1·2 and 𝑛·1·3 # ⟦ tu ↦ ∅, left🌵 ↦ 𝑛·1·2( tu ↦ tu ), right🌵 ↦ 𝑛·1·3, φ ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧ ⟧ 𝔼(L_join): 𝑛·2·1 := Φ.t( tu ↦ ⊥ ) # 𝕄(ξ.left🌵) 𝑛·2·2 := ⟦ tu ↦ ⊥, φ ↦ ρ.s ⟧+ remembered 𝑛·2·2 ≡ 𝑛·1·2( tu ↦ ⊥ ) 𝕄(ξ.left🌵): morphed 𝑛·2·3 := 𝜎2:λ:k 𝕄(ξ.right🌵):
+ test-resources/evaluate-packs/joins-a-side-that-dispatches-on-a-terminator.yaml view
@@ -0,0 +1,44 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The right side takes 'q' of a copy of 'throw', whose λ function 'L_throw'+# the entry names under 'terminators'. A dispatch on something that raises+# is the same raise, so the morph of the side stops at the copy of 'throw'+# and never fires 'L_throw', and the join takes it for a side that raises,+# the way it does without the '.q' (#2308).+symbolic: |+ - λ: L_fork+ terminators: [L_throw]+ dataize:+ 𝛿1: $.on🌵+ morph:+ 𝑛1: $.left🌵+ 𝑛2: $.right🌵+ join:+ on: 𝛿1+ left: 𝑛1+ right: 𝑛2+ otherwise: L_fork+location: 'Q.x'+input: '⟦ throw(message) ↦ ⟦ λ ⤍ L_throw ⟧, x ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ⟦ k ↦ ⟦⟧, φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, right🌵 ↦ Φ.throw( "bad" ).q ⟧.φ ⟧'+result: '𝜎4:λ'+protocol: |+ 𝕄(Φ.x):+ 𝔼(L_fork):+ 𝔻(ξ.on🌵):+ 𝛿·1·1 := 𝔻(𝜎1:λ)+ 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.on🌵)+ 𝕄(ξ.left🌵):+ morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎2:λ ⟧+ 𝑛1·1 := 𝑛·1·1 # 𝕄(ξ.left🌵)+ 𝕄(ξ.right🌵):+ remembered 𝑛·1·2 ≡ Φ.throw # ⟦ message ↦ ∅, λ ⤍ L_throw ⟧+ 𝑛·1·3 := Φ.throw( message ↦ "bad" )+ 𝑛·1·4 := ⟦ message ↦ "bad", λ ⤍ L_throw ⟧+ remembered 𝑛·1·4 ≡ 𝑛·1·2( message ↦ "bad" )+ morphed 𝑛·1·5 := 𝑛·1·4+ 𝑛2·1 := 𝑛·1·4 # 𝕄(ξ.right🌵)+ joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3 # where 𝜎3 is ⊥ raised by 𝑛·1·4+ 𝑛·1·6 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧+ morphed 𝑛·0·1 := 𝜎4:λ
test-resources/evaluate-packs/joins-a-side-that-raises-through-a-terminator.yaml view
@@ -47,10 +47,12 @@ morphed 𝑛·1·1 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎2:λ ⟧ 𝑛1·1 := 𝑛·1·1 # 𝕄(ξ.left🌵) 𝕄(ξ.right🌵):- 𝑛·1·2 := Φ.throw( message ↦ "bad" )- 𝑛·1·3 := ⟦ message ↦ "bad", λ ⤍ L_throw ⟧- morphed 𝑛·1·4 := 𝑛·1·3- 𝑛2·1 := 𝑛·1·3 # 𝕄(ξ.right🌵)- joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3 # where 𝜎3 is ⊥ raised by 𝑛·1·3- 𝑛·1·5 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧+ remembered 𝑛·1·2 ≡ Φ.throw # ⟦ message ↦ ∅, λ ⤍ L_throw ⟧+ 𝑛·1·3 := Φ.throw( message ↦ "bad" )+ 𝑛·1·4 := ⟦ message ↦ "bad", λ ⤍ L_throw ⟧+ remembered 𝑛·1·4 ≡ 𝑛·1·2( message ↦ "bad" )+ morphed 𝑛·1·5 := 𝑛·1·4+ 𝑛2·1 := 𝑛·1·4 # 𝕄(ξ.right🌵)+ joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3 # where 𝜎3 is ⊥ raised by 𝑛·1·4+ 𝑛·1·6 := ⟦ k ↦ ⟦⟧, φ ↦ 𝜎4:λ ⟧ morphed 𝑛·0·1 := 𝜎4:λ
+ test-resources/evaluate-packs/joins-a-side-whose-operand-raises.yaml view
@@ -0,0 +1,50 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The right side fires 'L_wrap', whose only operand under 'dataize' is a+# copy of 'throw', whose λ function 'L_throw' the entry names under+# 'terminators'. Data that comes from something that raises is the same+# raise, so 'L_wrap' answers ⊥ and never fires 'L_throw', and the join+# takes the right side for a side that raises (#2330).+symbolic: |+ - λ: L_wrap+ terminators: [L_throw]+ dataize:+ 𝛿1: $.x+ 𝑛: ⟦ λ ⤍ 𝜎 ⟧+ - λ: L_pick+ terminators: [L_throw]+ dataize:+ 𝛿1: $.c+ morph:+ 𝑛1: $.l+ 𝑛2: $.r+ join:+ on: 𝛿1+ left: 𝑛1+ right: 𝑛2+location: 'Q.y'+input: '⟦ wrap(x) ↦ ⟦ λ ⤍ L_wrap ⟧, y ↦ ⟦ λ ⤍ L_pick, c ↦ ⟦ λ ⤍ 𝜎1 ⟧, l ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, r ↦ Φ.wrap( ⟦ λ ⤍ L_throw ⟧ ).φ ⟧.φ ⟧'+result: '𝜎4:λ'+protocol: |+ 𝕄(Φ.y):+ 𝔼(L_pick):+ 𝔻(ξ.c):+ 𝛿·1·1 := 𝔻(𝜎1:λ)+ 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.c)+ 𝕄(ξ.l):+ morphed 𝑛·1·1 := 𝜎2:λ:φ+ 𝑛1·1 := 𝑛·1·1 # 𝕄(ξ.l)+ 𝕄(ξ.r):+ remembered 𝑛·1·2 ≡ Φ.wrap # ⟦ x ↦ ∅, λ ⤍ L_wrap ⟧+ 𝑛·1·3 := Φ.wrap( x ↦ L_throw:λ )+ 𝑛·1·4 := ⟦ x ↦ L_throw:λ, λ ⤍ L_wrap ⟧+ remembered 𝑛·1·4 ≡ 𝑛·1·2( x ↦ L_throw:λ )+ 𝔼(L_wrap):+ 𝑛·2·1 := ⊥+ morphed 𝑛·1·5 := ⊥+ 𝑛2·1 := ⊥ # 𝕄(ξ.r)+ joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3 # where 𝜎3 is ⊥+ 𝑛·1·6 := 𝜎4:λ:φ+ morphed 𝑛·0·1 := 𝜎4:λ
test-resources/evaluate-packs/joins-again-the-attribute-of-a-fabricated-formation.yaml view
@@ -40,13 +40,16 @@ fabricated 𝑛·1·3 := 𝑛·1·1 and 𝑛·1·2 # ⟦ left🌵 ↦ 𝑛·1·1, right🌵 ↦ 𝑛·1·2, φ ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.φ, right🌵 ↦ ρ.right🌵.φ ⟧, ob ↦ ⟦ λ ⤍ L_join, on🌵 ↦ 𝜎1:λ, left🌵 ↦ ρ.left🌵.ob, right🌵 ↦ ρ.right🌵.ob ⟧ ⟧ 𝔼(L_join): 𝕄(ξ.left🌵):- 𝑛·2·1 := Φ.hx( ke ↦ 𝜎2:λ )- 𝑛·2·2 := ⟦ ke ↦ 𝜎2:λ, φ ↦ ke ⟧- morphed 𝑛·2·3 := 𝑛·2·2+ remembered 𝑛·2·1 ≡ Φ.hx # ⟦ ke ↦ ∅, φ ↦ ke ⟧+ 𝑛·2·2 := Φ.hx( ke ↦ 𝜎2:λ )+ 𝑛·2·3 := ⟦ ke ↦ 𝜎2:λ, φ ↦ ke ⟧+ remembered 𝑛·2·3 ≡ 𝑛·2·1( ke ↦ 𝜎2:λ )+ morphed 𝑛·2·4 := 𝑛·2·3 𝕄(ξ.right🌵):- 𝑛·2·4 := Φ.hx( ke ↦ 𝜎3:λ )- 𝑛·2·5 := ⟦ ke ↦ 𝜎3:λ, φ ↦ ke ⟧- morphed 𝑛·2·6 := 𝑛·2·5+ 𝑛·2·5 := Φ.hx( ke ↦ 𝜎3:λ )+ 𝑛·2·6 := ⟦ ke ↦ 𝜎3:λ, φ ↦ ke ⟧+ remembered 𝑛·2·6 ≡ 𝑛·2·1( ke ↦ 𝜎3:λ )+ morphed 𝑛·2·7 := 𝑛·2·6 joined 𝜎4 := ξ.on🌵 ? 𝜎2 : 𝜎3- 𝑛·2·7 := ⟦ ke ↦ 𝜎4:λ, φ ↦ ke ⟧+ 𝑛·2·8 := ⟦ ke ↦ 𝜎4:λ, φ ↦ ke ⟧ morphed 𝑛·0·1 := 𝜎4:λ
test-resources/evaluate-packs/joins-two-sides-differing-in-a-datum-a-symbolize-found-off-the-phi-chain.yaml view
@@ -44,6 +44,8 @@ 𝑛3·1 := Φ.bool( if ↦ 𝜎3:λ:φ ):φ # symbolize(𝑛1) joined 𝜎4 := 𝛿1·1 ? 𝜎3 : 𝜎2 𝑛·1·3 := Φ.bool( if ↦ 𝜎4:λ:φ ):φ- 𝑛·0·1 := Φ.bool( if ↦ 𝜎4:λ:φ )- 𝑛·0·2 := ⟦ if ↦ 𝜎4:λ:φ, φ ↦ if ⟧- morphed 𝑛·0·3 := 𝑛·0·2+ remembered 𝑛·0·1 ≡ Φ.bool # ⟦ if ↦ ∅, φ ↦ if ⟧+ 𝑛·0·2 := Φ.bool( if ↦ 𝜎4:λ:φ )+ 𝑛·0·3 := ⟦ if ↦ 𝜎4:λ:φ, φ ↦ if ⟧+ remembered 𝑛·0·3 ≡ 𝑛·0·1( if ↦ 𝜎4:λ:φ )+ morphed 𝑛·0·4 := 𝑛·0·3
test-resources/evaluate-packs/leaves-a-formation-with-an-attribute-of-its-own-as-it-is.yaml view
@@ -34,20 +34,29 @@ result: '𝜎4:λ' protocol: | 𝕄(Φ.y):+ remembered 𝑛·0·1 ≡ Φ.x # ⟦ λ ⤍ L_fork, on🌵 ↦ 𝜎1:λ, left🌵 ↦ Φ.box( 𝜎2:λ ), right🌵 ↦ Φ.box( 𝜎3:λ ) ⟧ 𝔼(L_fork): 𝔻(ξ.on🌵): 𝛿·1·1 := 𝔻(𝜎1:λ) 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.on🌵) 𝕄(ξ.left🌵):- 𝑛·1·1 := Φ.box( v ↦ 𝜎2:λ )- 𝑛·1·2 := ⟦ v ↦ 𝜎2:λ, tag ↦ v, λ ⤍ L_box ⟧- morphed 𝑛·1·3 := 𝑛·1·2- 𝑛1·1 := 𝑛·1·2 # 𝕄(ξ.left🌵)+ remembered 𝑛·1·1 ≡ Φ.box # ⟦ v ↦ ∅, tag ↦ v, λ ⤍ L_box ⟧+ 𝑛·1·2 := Φ.box( v ↦ 𝜎2:λ )+ 𝑛·1·3 := ⟦ v ↦ 𝜎2:λ, tag ↦ v, λ ⤍ L_box ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( v ↦ 𝜎2:λ )+ morphed 𝑛·1·4 := 𝑛·1·3+ 𝑛1·1 := 𝑛·1·3 # 𝕄(ξ.left🌵) 𝕄(ξ.right🌵):- 𝑛·1·4 := Φ.box( v ↦ 𝜎3:λ )- 𝑛·1·5 := ⟦ v ↦ 𝜎3:λ, tag ↦ v, λ ⤍ L_box ⟧- morphed 𝑛·1·6 := 𝑛·1·5- 𝑛2·1 := 𝑛·1·5 # 𝕄(ξ.right🌵)+ 𝑛·1·5 := Φ.box( v ↦ 𝜎3:λ )+ 𝑛·1·6 := ⟦ v ↦ 𝜎3:λ, tag ↦ v, λ ⤍ L_box ⟧+ remembered 𝑛·1·6 ≡ 𝑛·1·1( v ↦ 𝜎3:λ )+ morphed 𝑛·1·7 := 𝑛·1·6+ 𝑛2·1 := 𝑛·1·6 # 𝕄(ξ.right🌵)+ recalled 𝑛·1·3 ⇒ 𝑛·1·1( v ↦ 𝜎2:λ )+ recalled 𝑛·1·1 ⇒ Φ.box+ recalled 𝑛·1·6 ⇒ 𝑛·1·1( v ↦ 𝜎3:λ )+ recalled 𝑛·1·1 ⇒ Φ.box joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3- 𝑛·1·7 := ⟦ v ↦ 𝜎4:λ, tag ↦ v, λ ⤍ L_box ⟧- morphed 𝑛·0·1 := 𝜎4:λ+ 𝑛·1·8 := ⟦ v ↦ 𝜎4:λ, tag ↦ v, λ ⤍ L_box ⟧+ remembered 𝑛·1·9 ≡ 𝑛·0·1 # ⟦ v ↦ 𝜎4:λ, tag ↦ v, λ ⤍ L_box ⟧+ morphed 𝑛·0·2 := 𝜎4:λ
test-resources/evaluate-packs/morphs-two-branches-spelling-one-term-through-one-firing.yaml view
@@ -77,6 +77,7 @@ 𝑛·1·19 := ⟦ φ ↦ 𝜎1:λ, if(then, else) ↦ L_fork:λ ⟧ morphed 𝑛·1·20 := 𝑛·1·19 𝑛·1·21 := 𝑛·1·20 # 𝕄(𝑛·1·17)+ memoized 𝑛·0·4 ⇛ 𝑛·1·21 𝑛·0·5 := 𝑛·1·18.if( then ↦ 1.0.plus( 2.0 ).plus( 3.0 ) ) 𝑛·0·6 := ⟦ then ↦ 1.0.plus( 2.0 ).plus( 3.0 ), else ↦ ∅, λ ⤍ L_fork ⟧ 𝑛·0·7 := 𝑛·0·5( else ↦ 1.0.plus( 2.0 ).plus( 3.0 ) )@@ -128,6 +129,7 @@ 𝑛·3·19 := ⟦ φ ↦ 𝜎2:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·3·20 := 𝑛·3·19 𝑛·3·21 := 𝑛·3·20 # 𝕄(𝑛·3·17)+ memoized 𝑛·2·8 ⇛ 𝑛·3·21 𝑛·2·9 := 𝑛·3·18.plus( x ↦ 3.0 ) 𝑛·2·10 := ⟦ x ↦ 3.0, λ ⤍ L_number_plus ⟧ morphed 𝑛·2·11 := 𝑛·2·10@@ -138,6 +140,7 @@ 𝑛·2·14 := 𝑛·2·12.plus( x ↦ 𝑛·3·9 ) 𝑛·2·15 := ⟦ x ↦ 𝑛·3·9, λ ⤍ L_number_plus ⟧ 𝔼(L_number_plus):+ recalled 𝑛·2·8 ⇒ 𝑛·3·21 𝑛·4·1 := 𝑛·3·18 # 𝑛 𝑛·4·2 := 𝑛·3·21 # 𝕄(𝑛·4·1) 𝑛·2·16 := 𝑛·3·18.plus( x ↦ 3.0 )@@ -148,6 +151,7 @@ 𝕄(𝑛·2·19): morphed 𝑛·2·20 := 𝑛·2·17 𝑛·2·21 := 𝑛·2·17 # 𝕄(𝑛·2·19)+ memoized 𝑛·0·8 ⇛ 𝑛·2·17 𝔼(L_number_plus): 𝔻(ξ.ρ): 𝕄(ξ.ρ):@@ -176,6 +180,7 @@ 𝑛·5·15 := ⟦ φ ↦ 𝜎3:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·5·16 := 𝑛·5·15 𝑛·5·17 := 𝑛·5·16 # 𝕄(𝑛·5·13)+ memoized 𝑛·2·17 ⇛ 𝑛·5·17 𝑛·0·9 := 𝑛·5·14.plus( x ↦ 9.0 ) 𝑛·0·10 := ⟦ x ↦ 9.0, λ ⤍ L_number_plus ⟧ morphed 𝑛·0·11 := 𝑛·0·10
test-resources/evaluate-packs/parks-a-firing-whose-deferred-argument-got-stuck.yaml view
@@ -31,12 +31,18 @@ 𝕄(Φ.p): 𝔼(L_pair): 𝕄(ξ.c):- 𝑛·1·1 := Φ.box( s ↦ 𝜎1:λ )- 𝑛·1·2 := ⟦ s ↦ 𝜎1:λ, x ↦ ∅, φ ↦ s.next ⟧- 𝑛·1·3 := 𝑛·1·1( x ↦ ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ )- 𝑛·1·4 := ⟦ s ↦ 𝜎1:λ, x ↦ ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ, φ ↦ s.next ⟧- morphed 𝑛·1·5 := 𝑛·1·4- 𝑛1·1 := 𝑛·1·5 # 𝕄(ξ.c)+ remembered 𝑛·1·1 ≡ Φ.box # ⟦ s ↦ ∅, x ↦ ∅, φ ↦ s.next ⟧+ 𝑛·1·2 := Φ.box( s ↦ 𝜎1:λ )+ 𝑛·1·3 := ⟦ s ↦ 𝜎1:λ, x ↦ ∅, φ ↦ s.next ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( s ↦ 𝜎1:λ )+ 𝑛·1·4 := 𝑛·1·2( x ↦ ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ )+ 𝑛·1·5 := ⟦ s ↦ 𝜎1:λ, x ↦ ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ, φ ↦ s.next ⟧+ remembered 𝑛·1·5 ≡ 𝑛·1·3( x ↦ ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ )+ morphed 𝑛·1·6 := 𝑛·1·5+ 𝑛1·1 := 𝑛·1·6 # 𝕄(ξ.c)+ recalled 𝑛·1·5 ⇒ 𝑛·1·3( x ↦ ⟦ arg ↦ L_none:λ, λ ⤍ L_outer ⟧.φ )+ recalled 𝑛·1·3 ⇒ 𝑛·1·1( s ↦ 𝜎1:λ )+ recalled 𝑛·1·1 ⇒ Φ.box 𝕄(𝑛1.x): 𝔼(L_outer): 𝔻(ξ.arg):
− test-resources/evaluate-packs/parks-a-firing-whose-operand-loops.yaml
@@ -1,33 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# A loop met while an operand is being brought down to data, one whole run of 𝔻-# below the spine. That run reduces the operand under a synthetic attribute of-# its own, so what it parks on is no term of the program; the spine around the-# firing is what answers instead, with the term it had reached when the firing-# started (see 'down' in 'Morph'). The entry never fires, and the protocol keeps-# the firing it opened and the loop it met underneath.-symbolic: |- - λ: L_outer- dataize:- 𝛿1: ξ.arg- 𝑛: ⟦ λ ⤍ 𝜎 ⟧- - λ: L_loop- 𝑛: ⟦ λ ⤍ L_loop ⟧-location: 'Q.x'-acyclic: proven-steps: 250-input: >- ⟦ x ↦ ⟦ arg ↦ ⟦ λ ⤍ L_loop ⟧.foo, λ ⤍ L_outer ⟧.bar ⟧-result: '⟦ arg ↦ L_loop:λ.foo, λ ⤍ L_outer ⟧.bar'-protocol: |- 𝕄(Φ.x):- 𝔼(L_outer):- 𝔻(ξ.arg):- 𝕄(ξ.arg):- 𝔼(L_loop):- 𝑛·2·1 := L_loop:λ # 𝑛- 𝕄(𝑛·2·1):- morphed 𝑛·2·2 := L_loop:λ- 𝑛·2·3 := L_loop:λ # 𝕄(𝑛·2·1)- looped L_loop:λ # proven
test-resources/evaluate-packs/parks-a-firing-whose-operand-reaches-the-terminator.yaml view
@@ -58,8 +58,10 @@ 𝕄(ξ.v.φ): 𝑛·1·9 := Φ.block( buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ) 𝑛·1·10 := ⟦ data ↦ ∅, buffer ↦ Φ.bytes( φ ↦ 𝜎1:λ ), read ↦ Φ.dataized( target ↦ ρ.data.size ).as-bytes:φ ⟧- 𝑛·1·11 := Φ.dataized( target ↦ ⊥ )- 𝑛·1·12 := ⟦ target ↦ ⊥, λ ⤍ L_dataized ⟧+ remembered 𝑛·1·11 ≡ Φ.dataized # ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧+ 𝑛·1·12 := Φ.dataized( target ↦ ⊥ )+ 𝑛·1·13 := ⟦ target ↦ ⊥, λ ⤍ L_dataized ⟧+ remembered 𝑛·1·13 ≡ 𝑛·1·11( target ↦ ⊥ ) 𝔼(L_dataized): unanswered ⊥ # 𝔻(⊥) stuck ⊥
− test-resources/evaluate-packs/parks-an-entry-that-answers-with-a-firing-of-itself.yaml
@@ -1,23 +0,0 @@-# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com-# SPDX-License-Identifier: MIT-----# The same entry answering with a firing of itself, under '_acyclic': morphing-# comes back to the very term it is already reducing, so it stops there instead-# of going round until the budget is gone. The budget is generous here, so what-# ends the run is the cut and not the limit.-symbolic: |- - λ: L_loop- 𝑛: ⟦ λ ⤍ L_loop ⟧-location: 'Q.x'-acyclic: proven-steps: 250-input: '⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo ⟧'-result: 'L_loop:λ.foo'-protocol: |- 𝕄(Φ.x):- 𝔼(L_loop):- 𝑛·1·1 := L_loop:λ # 𝑛- 𝕄(𝑛·1·1):- morphed 𝑛·1·2 := L_loop:λ- 𝑛·1·3 := L_loop:λ # 𝕄(𝑛·1·1)- looped L_loop:λ # proven
test-resources/evaluate-packs/spends-a-step-on-every-firing-of-an-evaluate-line.yaml view
@@ -22,10 +22,12 @@ fails: 'reaching the limit of steps' protocol: | 𝕄(Φ.app):+ remembered 𝑛·0·1 ≡ Φ.loop # ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧ 𝔼(L_loop): 𝕄(ξ.next🌵):- morphed 𝑛·1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧- 𝑛1·1 := ⟦ next🌵 ↦ Φ.loop, λ ⤍ L_loop ⟧ # 𝕄(ξ.next🌵)+ morphed 𝑛·1·1 := 𝑛·0·1+ 𝑛1·1 := 𝑛·0·1 # 𝕄(ξ.next🌵)+ recalled 𝑛·0·1 ⇒ Φ.loop 𝔼(L_loop): # 𝔼(𝑛1) 𝕄(ξ.next🌵): starved 6
test-resources/evaluate-packs/takes-the-answer-of-a-firing-with-the-same-operands.yaml view
@@ -39,15 +39,20 @@ 𝕄(Φ.p): 𝔼(L_pair): 𝕄(ξ.a):- 𝑛·1·1 := Φ.dataized( target ↦ Φ.x )- 𝑛·1·2 := ⟦ target ↦ Φ.x, λ ⤍ L_dataized ⟧- morphed 𝑛·1·3 := 𝑛·1·2- 𝑛1·1 := 𝑛·1·2 # 𝕄(ξ.a)+ remembered 𝑛·1·1 ≡ Φ.dataized # ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧+ 𝑛·1·2 := Φ.dataized( target ↦ Φ.x )+ 𝑛·1·3 := ⟦ target ↦ Φ.x, λ ⤍ L_dataized ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( target ↦ Φ.x )+ morphed 𝑛·1·4 := 𝑛·1·3+ 𝑛1·1 := 𝑛·1·3 # 𝕄(ξ.a) 𝕄(ξ.b):- 𝑛·1·4 := Φ.dataized( target ↦ Φ.y )- 𝑛·1·5 := ⟦ target ↦ Φ.y, λ ⤍ L_dataized ⟧- morphed 𝑛·1·6 := 𝑛·1·5- 𝑛2·1 := 𝑛·1·5 # 𝕄(ξ.b)+ 𝑛·1·5 := Φ.dataized( target ↦ Φ.y )+ 𝑛·1·6 := ⟦ target ↦ Φ.y, λ ⤍ L_dataized ⟧+ remembered 𝑛·1·6 ≡ 𝑛·1·1( target ↦ Φ.y )+ morphed 𝑛·1·7 := 𝑛·1·6+ 𝑛2·1 := 𝑛·1·6 # 𝕄(ξ.b)+ recalled 𝑛·1·3 ⇒ 𝑛·1·1( target ↦ Φ.x )+ recalled 𝑛·1·1 ⇒ Φ.dataized 𝔼(L_dataized): # 𝔼(𝑛1) 𝔻(ξ.target): 𝕄(ξ.target):@@ -58,18 +63,24 @@ 𝕄(𝑛·2·2): morphed 𝑛·2·3 := 𝜎1:λ 𝑛·2·4 := 𝑛·2·3 # 𝕄(𝑛·2·2)+ memoized 𝑛·1·3 ⇛ 𝜎1:λ 𝑛3·1 := 𝑛·2·4 # 𝔼(𝑛1)+ recalled 𝑛·1·6 ⇒ 𝑛·1·1( target ↦ Φ.y )+ recalled 𝑛·1·1 ⇒ Φ.dataized 𝔼(L_dataized): # 𝔼(𝑛2) 𝔻(ξ.target): 𝕄(ξ.target): morphed 𝑛·3·1 := 01-:Δ 𝛿·3·1 := 01- 𝛿1·3 := 𝛿·3·1 # 𝔻(ξ.target)+ recalled 𝑛·1·3 ⇒ 𝜎1:λ 𝑛·3·2 := 𝑛3·1 # 𝑛 𝑛·3·3 := 𝑛3·1 # 𝕄(𝑛·3·2)+ memoized 𝑛·1·6 ⇛ 𝜎1:λ 𝑛4·1 := 𝑛·3·3 # 𝔼(𝑛2)- 𝑛·1·7 := ⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧:φ # 𝑛- 𝕄(𝑛·1·7):- morphed 𝑛·1·8 := ⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧:φ- 𝑛·1·9 := 𝑛·1·8 # 𝕄(𝑛·1·7)+ 𝑛·1·8 := ⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧:φ # 𝑛+ 𝕄(𝑛·1·8):+ morphed 𝑛·1·9 := ⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧:φ+ 𝑛·1·10 := 𝑛·1·9 # 𝕄(𝑛·1·8)+ memoized 𝑛·1·11 ⇛ 𝑛·1·10 # ⟦ a ↦ 𝑛·1·2, b ↦ 𝑛·1·5, λ ⤍ L_pair ⟧ morphed 𝑛·0·1 := ⟦ a ↦ 𝜎1:λ, b ↦ 𝜎1:λ ⟧
test-resources/evaluate-packs/tells-two-symbols-of-one-datum-apart-between-firings.yaml view
@@ -32,14 +32,19 @@ result: '⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧' protocol: | 𝕄(Φ.φ):- 𝑛·0·1 := Φ.pair( x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ )- 𝑛·0·2 := ⟦ x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ, y ↦ ∅, λ ⤍ L_pair ⟧- 𝑛·0·3 := 𝑛·0·1( y ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ )- 𝑛·0·4 := ⟦ x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ, y ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ, λ ⤍ L_pair ⟧+ remembered 𝑛·0·1 ≡ Φ.pair # ⟦ x ↦ ∅, y ↦ ∅, λ ⤍ L_pair ⟧+ 𝑛·0·2 := Φ.pair( x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ )+ 𝑛·0·3 := ⟦ x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ, y ↦ ∅, λ ⤍ L_pair ⟧+ remembered 𝑛·0·3 ≡ 𝑛·0·1( x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ )+ 𝑛·0·4 := 𝑛·0·2( y ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ )+ 𝑛·0·5 := ⟦ x ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎1:λ ) ).φ, y ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ, λ ⤍ L_pair ⟧+ remembered 𝑛·0·5 ≡ 𝑛·0·3( y ↦ Φ.dataized( Φ.bytes( φ ↦ 𝜎2:λ ) ).φ ) 𝔼(L_pair): 𝕄(ξ.x):- 𝑛·1·1 := Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎1:λ ) )- 𝑛·1·2 := ⟦ target ↦ Φ.bytes( φ ↦ 𝜎1:λ ), λ ⤍ L_dataized ⟧+ remembered 𝑛·1·1 ≡ Φ.dataized # ⟦ target ↦ ∅, λ ⤍ L_dataized ⟧+ 𝑛·1·2 := Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎1:λ ) )+ 𝑛·1·3 := ⟦ target ↦ Φ.bytes( φ ↦ 𝜎1:λ ), λ ⤍ L_dataized ⟧+ remembered 𝑛·1·3 ≡ 𝑛·1·1( target ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ) 𝔼(L_dataized): 𝔻(ξ.target): 𝕄(ξ.target):@@ -55,11 +60,14 @@ 𝑛·2·7 := 𝜎3:λ:φ morphed 𝑛·2·8 := 𝑛·2·7 𝑛·2·9 := 𝑛·2·8 # 𝕄(𝑛·2·5)- morphed 𝑛·1·3 := 𝜎3:λ- 𝑛1·1 := 𝑛·1·3 # 𝕄(ξ.x)+ remembered 𝑛·2·9 ≡ 𝑛·1·3+ memoized 𝑛·1·3 ⇛ 𝑛·2·9+ morphed 𝑛·1·4 := 𝜎3:λ+ 𝑛1·1 := 𝑛·1·4 # 𝕄(ξ.x) 𝕄(ξ.y):- 𝑛·1·4 := Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎2:λ ) )- 𝑛·1·5 := ⟦ target ↦ Φ.bytes( φ ↦ 𝜎2:λ ), λ ⤍ L_dataized ⟧+ 𝑛·1·5 := Φ.dataized( target ↦ Φ.bytes( φ ↦ 𝜎2:λ ) )+ 𝑛·1·6 := ⟦ target ↦ Φ.bytes( φ ↦ 𝜎2:λ ), λ ⤍ L_dataized ⟧+ remembered 𝑛·1·6 ≡ 𝑛·1·1( target ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ) 𝔼(L_dataized): 𝔻(ξ.target): 𝕄(ξ.target):@@ -75,10 +83,14 @@ 𝑛·3·7 := 𝜎4:λ:φ morphed 𝑛·3·8 := 𝑛·3·7 𝑛·3·9 := 𝑛·3·8 # 𝕄(𝑛·3·5)- morphed 𝑛·1·6 := 𝜎4:λ- 𝑛2·1 := 𝑛·1·6 # 𝕄(ξ.y)- 𝑛·1·7 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧:φ # 𝑛- 𝕄(𝑛·1·7):- morphed 𝑛·1·8 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧:φ- 𝑛·1·9 := 𝑛·1·8 # 𝕄(𝑛·1·7)- morphed 𝑛·0·5 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧+ remembered 𝑛·3·9 ≡ 𝑛·1·6+ memoized 𝑛·1·6 ⇛ 𝑛·3·9+ morphed 𝑛·1·7 := 𝜎4:λ+ 𝑛2·1 := 𝑛·1·7 # 𝕄(ξ.y)+ 𝑛·1·8 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧:φ # 𝑛+ 𝕄(𝑛·1·8):+ morphed 𝑛·1·9 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧:φ+ 𝑛·1·10 := 𝑛·1·9 # 𝕄(𝑛·1·8)+ remembered 𝑛·1·10 ≡ 𝑛·0·5+ memoized 𝑛·0·5 ⇛ 𝑛·1·10+ morphed 𝑛·0·6 := ⟦ x ↦ 𝜎3:λ, y ↦ 𝜎4:λ ⟧
test-resources/evaluate-packs/undresses-a-formation-wrapping-itself-until-the-steps-run-out.yaml view
@@ -22,11 +22,12 @@ 𝕄(Φ.y): 𝔼(L_peel): 𝕄(ξ.x):- morphed 𝑛·1·1 := Φ.w:φ- 𝑛1·1 := 𝑛·1·1 # 𝕄(ξ.x)- undressed 𝑛·1·2 := 𝑛·1·1.φ- 𝕄(𝑛·1·2):- morphed 𝑛·1·3 := 𝑛·1·1- undressed 𝑛·1·4 := 𝑛·1·3.φ- 𝕄(𝑛·1·4):+ remembered 𝑛·1·1 ≡ Φ.w # Φ.w:φ+ morphed 𝑛·1·2 := 𝑛·1·1+ 𝑛1·1 := 𝑛·1·2 # 𝕄(ξ.x)+ undressed 𝑛·1·3 := 𝑛·1·2.φ+ 𝕄(𝑛·1·3):+ morphed 𝑛·1·4 := 𝑛·1·2+ undressed 𝑛·1·5 := 𝑛·1·4.φ+ 𝕄(𝑛·1·5): starved 6
+ test-resources/evaluate-packs/work-out-an-argument-that-comes-to-a-hanging-object.yaml view
@@ -0,0 +1,76 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The deferral of #1892 over a copy with two arguments: 'x' reads to the bare+# symbol '𝜎1', so the 'defer' line defers the copy, and 'w' is a call of+# 'Φ.hang'. Its morph stops at a formation with no λ whose φ reads 'ξ.x', so+# the line morphs that φ and fires it once more, the way a branch whose φ reads+# its own object is worked out in #1885. The line then names 'w' by a meta+# leading to a formation whose φ ends in a symbol, instead of leaving a '?'+# in '<with>' (#1919).+symbolic: |+ - λ: L_inc+ dataize:+ 𝛿1: $.x+ 𝑛: Φ.num( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )+ - λ: L_fork+ dataize:+ 𝛿1: $.c+ morph:+ 𝑛1: $.a+ 𝑛2: $.b+ defer:+ 𝑛3: 𝑛1+ 𝑛4: 𝑛2+ join:+ on: 𝛿1+ left: 𝑛3+ right: 𝑛4+location: 'Q.y'+input: '⟦ box(x, w) ↦ ⟦ φ ↦ x.next ⟧, done ↦ ⟦⟧, hang(x) ↦ ⟦ φ ↦ ξ.x ⟧, num(φ) ↦ ⟦⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ x ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎2 ⟧, a ↦ ⟦ λ ⤍ 𝜎3 ⟧, b ↦ Φ.box( x ↦ Φ.items.tail, w ↦ Φ.hang( Φ.num( φ ↦ ⟦ λ ⤍ 𝜎4 ⟧ ) ) ), λ ⤍ L_fork ⟧, λ ⤍ L_inc ⟧.φ ⟧'+result: '𝜎7:λ'+protocol: |+ 𝕄(Φ.y):+ 𝔼(L_inc):+ 𝔻(ξ.x):+ 𝔼(L_fork):+ 𝔻(ξ.c):+ 𝛿·2·1 := 𝔻(𝜎2:λ)+ 𝛿1·2 := 𝛿·2·1 # 𝔻(ξ.c)+ 𝕄(ξ.a):+ morphed 𝑛·2·1 := 𝜎3:λ+ 𝑛1·2 := 𝑛·2·1 # 𝕄(ξ.a)+ 𝕄(ξ.b):+ remembered 𝑛·2·2 ≡ Φ.box # ⟦ x ↦ ∅, w ↦ ∅, φ ↦ x.next ⟧+ 𝑛·2·3 := Φ.box( x ↦ Φ.items.tail )+ 𝑛·2·4 := ⟦ x ↦ Φ.items.tail, w ↦ ∅, φ ↦ x.next ⟧+ remembered 𝑛·2·4 ≡ 𝑛·2·2( x ↦ Φ.items.tail )+ 𝑛·2·5 := 𝑛·2·3( w ↦ Φ.hang( Φ.num( φ ↦ 𝜎4:λ ) ) )+ 𝑛·2·6 := ⟦ x ↦ Φ.items.tail, w ↦ Φ.hang( Φ.num( φ ↦ 𝜎4:λ ) ), φ ↦ x.next ⟧+ remembered 𝑛·2·6 ≡ 𝑛·2·4( w ↦ Φ.hang( Φ.num( φ ↦ 𝜎4:λ ) ) )+ morphed 𝑛·2·7 := 𝑛·2·6+ 𝑛2·2 := 𝑛·2·7 # 𝕄(ξ.b)+ recalled 𝑛·2·6 ⇒ 𝑛·2·4( w ↦ Φ.hang( Φ.num( φ ↦ 𝜎4:λ ) ) )+ recalled 𝑛·2·4 ⇒ 𝑛·2·2( x ↦ Φ.items.tail )+ recalled 𝑛·2·2 ⇒ Φ.box+ 𝕄(𝑛2.w):+ 𝑛·2·8 := Φ.hang( x ↦ Φ.num( φ ↦ 𝜎4:λ ) )+ 𝑛·2·9 := ⟦ x ↦ Φ.num( φ ↦ 𝜎4:λ ), φ ↦ x ⟧+ morphed 𝑛·2·10 := 𝑛·2·9+ 𝕄(𝑛2.w.φ):+ 𝑛·2·11 := Φ.num( φ ↦ 𝜎4:λ )+ 𝑛·2·12 := 𝜎4:λ:φ+ morphed 𝑛·2·13 := 𝑛·2·12+ deferred 𝜎5 := Φ.box( x ↦ 𝜎1:λ, w ↦ 𝑛·2·13 ) # 𝕄(𝑛2.φ)+ joined 𝜎6 := 𝛿1·2 ? 𝜎3 : 𝜎5+ 𝑛·2·14 := 𝜎6:λ+ 𝛿·1·1 := 𝔻(𝜎6:λ)+ 𝛿1·1 := 𝛿·1·1 # 𝔻(ξ.x)+ 𝑛·1·1 := Φ.num( φ ↦ 𝜎7:λ ) # 𝑛+ 𝕄(𝑛·1·1):+ 𝑛·1·2 := Φ.num( φ ↦ 𝜎7:λ )+ 𝑛·1·3 := 𝜎7:λ:φ+ morphed 𝑛·1·4 := 𝑛·1·3+ 𝑛·1·5 := 𝑛·1·4 # 𝕄(𝑛·1·1)+ morphed 𝑛·0·1 := 𝜎7:λ
test-resources/evaluate-packs/writes-no-joined-line-for-a-join-the-memo-answered.yaml view
@@ -77,6 +77,7 @@ 𝑛·1·19 := ⟦ φ ↦ 𝜎1:λ, if(then, else) ↦ L_fork:λ ⟧ morphed 𝑛·1·20 := 𝑛·1·19 𝑛·1·21 := 𝑛·1·20 # 𝕄(𝑛·1·17)+ memoized 𝑛·0·4 ⇛ 𝑛·1·21 𝑛·0·5 := 𝑛·1·18.if( then ↦ 1.0.plus( 2.0 ).plus( 𝑛·1·9 ) ) 𝑛·0·6 := ⟦ then ↦ 1.0.plus( 2.0 ).plus( 𝑛·1·9 ), else ↦ ∅, λ ⤍ L_fork ⟧ 𝑛·0·7 := 𝑛·0·5( else ↦ 3.0.plus( 4.0 ).plus( 𝑛·1·9 ) )@@ -128,6 +129,7 @@ 𝑛·3·19 := ⟦ φ ↦ 𝜎2:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·3·20 := 𝑛·3·19 𝑛·3·21 := 𝑛·3·20 # 𝕄(𝑛·3·17)+ memoized 𝑛·2·8 ⇛ 𝑛·3·21 𝑛·2·9 := 𝑛·3·18.plus( x ↦ 𝑛·1·9 ) 𝑛·2·10 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧ morphed 𝑛·2·11 := 𝑛·2·10@@ -169,11 +171,13 @@ 𝑛·4·19 := ⟦ φ ↦ 𝜎3:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·4·20 := 𝑛·4·19 𝑛·4·21 := 𝑛·4·20 # 𝕄(𝑛·4·17)+ memoized 𝑛·2·15 ⇛ 𝑛·4·21 𝑛·2·16 := 𝑛·4·18.plus( x ↦ 𝑛·1·9 ) 𝑛·2·17 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧ morphed 𝑛·2·18 := 𝑛·2·17 joined 𝜎4 := 𝛿1·2 ? 𝜎2 : 𝜎3 𝑛·2·19 := ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧+ memoized 𝑛·0·8 ⇛ ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧ 𝔼(L_number_plus): 𝔻(ξ.ρ): 𝕄(ξ.ρ):@@ -202,6 +206,7 @@ 𝑛·5·15 := ⟦ φ ↦ 𝜎5:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·5·16 := 𝑛·5·15 𝑛·5·17 := 𝑛·5·16 # 𝕄(𝑛·5·13)+ memoized 𝑛·5·18 ⇛ 𝑛·5·17 # ⟦ x ↦ 𝑛·5·5, λ ⤍ L_number_plus ⟧ 𝑛·0·9 := 𝑛·5·14.plus( x ↦ Φ.f ) 𝑛·0·10 := ⟦ x ↦ Φ.f, λ ⤍ L_number_plus ⟧ 𝔼(L_number_plus):@@ -220,6 +225,7 @@ 𝑛·6·7 := 𝑛·6·5.gt( x ↦ 𝑛·5·5 ) 𝑛·6·8 := ⟦ x ↦ 𝑛·5·5, λ ⤍ L_number_gt ⟧ 𝔼(L_number_gt):+ recalled 𝑛·0·4 ⇒ 𝑛·1·21 𝑛·7·1 := 𝑛·2·1 # 𝑛 𝑛·7·2 := 𝑛·1·21 # 𝕄(𝑛·7·1) 𝑛·6·9 := 𝑛·2·1.if( then ↦ 𝑛·3·1.plus( 𝑛·3·9 ).plus( 𝑛·5·5 ) )@@ -228,8 +234,10 @@ 𝑛·6·12 := ⟦ then ↦ 𝑛·3·1.plus( 𝑛·3·9 ).plus( 𝑛·5·5 ), else ↦ 𝑛·4·1.plus( 𝑛·4·9 ).plus( 𝑛·5·5 ), λ ⤍ L_fork ⟧ morphed 𝑛·6·13 := 𝑛·6·12 𝔼(L_fork):- 𝑛·8·1 := ⟦ x ↦ 𝑛·5·5, λ ⤍ L_number_plus ⟧+ recalled 𝑛·0·8 ⇒ ⟦ x ↦ 𝑛·1·9, λ ⤍ L_number_plus ⟧+ 𝑛·8·1 := 𝑛·5·18 𝔼(L_number_plus):+ recalled 𝑛·5·18 ⇒ 𝑛·5·17 𝑛·9·1 := 𝑛·6·1 # 𝑛 𝑛·9·2 := 𝑛·5·17 # 𝕄(𝑛·9·1) boxed 𝑛·6·14 := 𝑛·9·2.φ@@ -241,4 +249,5 @@ 𝑛·6·17 := ⟦ φ ↦ 𝜎6:λ, gt(x) ↦ L_number_gt:λ, plus(x) ↦ L_number_plus:λ ⟧ morphed 𝑛·6·18 := 𝑛·6·17 𝑛·6·19 := 𝑛·6·18 # 𝕄(𝑛·6·15)+ memoized 𝑛·0·10 ⇛ 𝑛·6·19 morphed 𝑛·0·11 := 𝜎6:λ
+ test-resources/rewriter-packs/custom/eq-expression-with-a-quoted-number.yaml view
@@ -0,0 +1,18 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+input: '[[ price -> 5, count -> 7 ]]'+output: |-+ ⟦+ price ↦ ⊥,+ count ↦ 7+ ⟧+rules:+ custom:+ - name: eq-expression-with-a-quoted-number+ pattern: '⟦ 𝜏1 ↦ 𝑒1, 𝐵1 ⟧'+ result: '⟦ 𝜏1 ↦ ⊥, 𝐵1 ⟧'+ when:+ eq:+ - '𝑒1'+ - '5'
test/CLISpec.hs view
@@ -6,7 +6,7 @@ module CLISpec (spec) where -import CLI (runCLI)+import CLI (prepareIO, runCLI) import CLI.Types (CmdException (..), IOFormat (..)) import Control.Concurrent (threadDelay) import Control.Exception@@ -19,6 +19,7 @@ import Data.Version (showVersion) import Files (allPathsIn) import Fixtures (explainPack, lambdasFile, loopingLambdas, readProtocol, readUtf8, withLambdasOf)+import GHC.IO.Encoding (TextEncoding (textEncodingName), getFileSystemEncoding) import GHC.IO.Handle import Paths_phino (version) import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, getTemporaryDirectory, listDirectory, makeAbsolute, removeDirectoryRecursive, removeFile, removePathForcibly, setModificationTime, withCurrentDirectory)@@ -680,6 +681,19 @@ ["rewrite", rule "evaluate-in-rewrite.yaml"] ["Function 'evaluate' in rule 'uses-evaluate' is available only for dataization and morphing, not for rewriting"] + forM_+ [ ("kind-tau-to-expression.yaml", "Function 'random-tau' in rule 'tau-to-expression' returns an attribute, but its meta '𝑒2' is an expression")+ , ("kind-size-to-attribute.yaml", "Function 'size' in rule 'size-to-attribute' returns an expression, but its meta '𝜏2' is an attribute")+ , ("kind-dataize-to-expression.yaml", "Function 'dataize' in rule 'dataize-to-expression' returns bytes, but its meta '𝑒2' is an expression")+ ]+ ( \(file, message) ->+ it ("refuses " ++ file ++ " at load time, before the pattern matches") $+ withStdin "⟦ bar ↦ ⟦⟧ ⟧" (testCLIFailed ["rewrite", rule file] [message])+ )++ it "accepts a where step whose function returns the kind of its meta" $+ withStdin "⟦ bar ↦ ⟦⟧ ⟧" (testCLISucceeded ["rewrite", rule "kind-tau-to-attribute.yaml"] ["bar ↦ ⟦⟧"])+ it "names the join function in the error message" $ withStdin "⟦⟧" $ testCLIFailed@@ -876,32 +890,32 @@ ["\"bar\":x"] it "prints many expressions with --sequence" $- withStdin "[[ x -> \"foo\" ]]" $+ withStdin "[[ x -> \"0\" ]]" $ testCLISucceeded [ "rewrite" , rule "first.yaml" , rule "second.yaml" , "--max-depth=1"- , "--max-cycles=2"+ , "--max-cycles=1" , "--sequence" , "--sweet" , "--flat" ] [ unlines- [ "\"foo\":x"- , "Φ.x( y ↦ \"foo\" )"- , "\"foo\":x"+ [ "\"0\":x"+ , "Φ.x( y ↦ \"1\" )"+ , "\"1\":x" ] ] it "prefixes every step with a header when --headers is on" $- withStdin "[[ x -> \"foo\" ]]" $+ withStdin "[[ x -> \"0\" ]]" $ testCLISucceeded [ "rewrite" , rule "first.yaml" , rule "second.yaml" , "--max-depth=1"- , "--max-cycles=2"+ , "--max-cycles=1" , "--sequence" , "--headers" , "--sweet"@@ -911,13 +925,13 @@ "\n" [ "" , "=== Step #1"- , "\"foo\":x"+ , "\"0\":x" , "" , "=== Step #2, Rule 'first', 23t -> 26t"- , "Φ.x( y ↦ \"foo\" )"+ , "Φ.x( y ↦ \"1\" )" , "" , "=== Step #3, Rule 'second', 26t -> 23t"- , "\"foo\":x"+ , "\"1\":x" ] ] @@ -928,13 +942,13 @@ ["\"bar\":x"] it "emits step headers as LaTeX comments with --headers" $- withStdin "[[ x -> \"foo\" ]]" $+ withStdin "[[ x -> \"0\" ]]" $ testCLISucceeded [ "rewrite" , rule "first.yaml" , rule "second.yaml" , "--max-depth=1"- , "--max-cycles=2"+ , "--max-cycles=1" , "--sequence" , "--headers" , "--sweet"@@ -944,23 +958,24 @@ [ unlines [ "\\begin{phiquation}" , "% === Step #1"- , "\"foo\" : |x| \\phiNormalize[\\nameref{r:first}]"+ , "\"0\" : |x| \\phiNormalize[\\nameref{r:first}]" , "% === Step #2, Rule 'first', 23t -> 26t"- , " \\phiNormalize Q . |x| ( |y| -> \"foo\" ) \\phiNormalize[\\nameref{r:second}]"+ , " \\phiNormalize Q . |x| ( |y| -> \"1\" ) \\phiNormalize[\\nameref{r:second}]" , "% === Step #3, Rule 'second', 26t -> 23t"- , " \\phiNormalize \"foo\" : |x|{.}"+ , " \\phiNormalize \"1\" : |x| \\phiNormalize"+ , " \\phiNormalize \\dots" , "\\end{phiquation}" ] ] it "prints only one latex preamble with --sequence" $- withStdin "[[ x -> \"foo\" ]]" $+ withStdin "[[ x -> \"0\" ]]" $ testCLISucceeded [ "rewrite" , rule "first.yaml" , rule "second.yaml" , "--max-depth=1"- , "--max-cycles=2"+ , "--max-cycles=1" , "--sequence" , "--sweet" , "--flat"@@ -968,9 +983,10 @@ ] [ unlines [ "\\begin{phiquation}"- , "\"foo\" : |x| \\phiNormalize[\\nameref{r:first}]"- , " \\phiNormalize Q . |x| ( |y| -> \"foo\" ) \\phiNormalize[\\nameref{r:second}]"- , " \\phiNormalize \"foo\" : |x|{.}"+ , "\"0\" : |x| \\phiNormalize[\\nameref{r:first}]"+ , " \\phiNormalize Q . |x| ( |y| -> \"1\" ) \\phiNormalize[\\nameref{r:second}]"+ , " \\phiNormalize \"1\" : |x| \\phiNormalize"+ , " \\phiNormalize \\dots" , "\\end{phiquation}" ] ]@@ -1503,17 +1519,21 @@ lines records `shouldBe` [ "𝔻(Φ.t):" , " 𝕄(Φ.t):"- , " 𝑛·0·1 := Φ.cyc( x ↦ ⟦⟧ )"- , " 𝑛·0·2 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧"- , " morphed 𝑛·0·3 := 𝑛·0·2"- , " boxed 𝑛·0·4 := 𝑛·0·3.φ"- , " 𝕄(𝑛·0·4):"- , " 𝑛·0·5 := Φ.cyc( x ↦ ⟦⟧ )"- , " 𝑛·0·6 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧"- , " morphed 𝑛·0·7 := 𝑛·0·6"- , " 𝕄(𝑛·0·7.x):"- , " morphed 𝑛·0·8 := ⟦⟧"- , " looped 𝜎1 := Φ.cyc( x ↦ 𝑛·0·8 ) # 𝔻(𝑛·0·4), proven, repeats 𝑛·0·7"+ , " remembered 𝑛·0·1 ≡ Φ.cyc # ⟦ x ↦ ∅, φ ↦ Φ.cyc( x ) ⟧"+ , " 𝑛·0·2 := Φ.cyc( x ↦ ⟦⟧ )"+ , " 𝑛·0·3 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧"+ , " remembered 𝑛·0·3 ≡ 𝑛·0·1( x ↦ ⟦⟧ )"+ , " morphed 𝑛·0·4 := 𝑛·0·3"+ , " boxed 𝑛·0·5 := 𝑛·0·4.φ"+ , " 𝕄(𝑛·0·5):"+ , " 𝑛·0·6 := Φ.cyc( x ↦ ⟦⟧ )"+ , " 𝑛·0·7 := ⟦ x ↦ ⟦⟧, φ ↦ Φ.cyc( x ) ⟧"+ , " morphed 𝑛·0·8 := 𝑛·0·7"+ , " recalled 𝑛·0·3 ⇒ 𝑛·0·1( x ↦ ⟦⟧ )"+ , " recalled 𝑛·0·1 ⇒ Φ.cyc"+ , " 𝕄(𝑛·0·8.x):"+ , " morphed 𝑛·0·9 := ⟦⟧"+ , " looped 𝜎1 := Φ.cyc( x ↦ 𝑛·0·9 ) # 𝔻(𝑛·0·5), proven, repeats 𝑛·0·8" , " 𝛿·0·1 := 𝔻(𝜎1:λ)" ] @@ -1529,21 +1549,26 @@ `shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>" , "<dataize at=\"Φ.t\">" , " <morph at=\"Φ.t\">"+ , " <remembered meta=\"𝑛·0·1\" as=\"Φ.cyc\"/>" , " <formed meta=\"𝑒·0·1\"/>"- , " <applied meta=\"𝑛·0·1\" by=\"morph\" at=\"Φ.t\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></applied>"- , " <formed meta=\"𝑛·0·2\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></formed>"- , " <morphed meta=\"𝑛·0·3\">𝑛·0·2</morphed>"+ , " <applied meta=\"𝑛·0·2\" by=\"morph\" at=\"Φ.t\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></applied>"+ , " <formed meta=\"𝑛·0·3\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></formed>"+ , " <applied meta=\"𝑒·0·2\" of=\"𝑛·0·1\"><meta attr=\"x\">𝑒·0·1</meta></applied>"+ , " <remembered of=\"𝑛·0·3\" as=\"𝑒·0·2\"/>"+ , " <morphed meta=\"𝑛·0·4\">𝑛·0·3</morphed>" , " </morph>"- , " <boxed meta=\"𝑛·0·4\">𝑛·0·3.φ</boxed>"- , " <morph at=\"𝑛·0·4\">"- , " <applied meta=\"𝑛·0·5\" by=\"morph\" at=\"𝑛·0·4\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></applied>"- , " <formed meta=\"𝑛·0·6\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></formed>"- , " <morphed meta=\"𝑛·0·7\">𝑛·0·6</morphed>"+ , " <boxed meta=\"𝑛·0·5\">𝑛·0·4.φ</boxed>"+ , " <morph at=\"𝑛·0·5\">"+ , " <applied meta=\"𝑛·0·6\" by=\"morph\" at=\"𝑛·0·5\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></applied>"+ , " <formed meta=\"𝑛·0·7\" of=\"Φ.cyc\"><meta attr=\"x\">𝑒·0·1</meta></formed>"+ , " <morphed meta=\"𝑛·0·8\">𝑛·0·7</morphed>" , " </morph>"- , " <morph at=\"𝑛·0·7.x\">"- , " <morphed meta=\"𝑛·0·8\">𝑒·0·1</morphed>"+ , " <recalled of=\"𝑛·0·3\" as=\"𝑒·0·2\"/>"+ , " <recalled of=\"𝑛·0·1\" as=\"Φ.cyc\"/>"+ , " <morph at=\"𝑛·0·8.x\">"+ , " <morphed meta=\"𝑛·0·9\">𝑒·0·1</morphed>" , " </morph>"- , " <looped symbol=\"𝜎1\" by=\"dataize\" match=\"proven\" at=\"𝑛·0·4\" of=\"𝑛·0·7\" object=\"Φ.cyc\"><with><meta attr=\"x\">𝑛·0·8</meta></with></looped>"+ , " <looped symbol=\"𝜎1\" by=\"dataize\" match=\"proven\" at=\"𝑛·0·5\" of=\"𝑛·0·8\" object=\"Φ.cyc\"><with><meta attr=\"x\">𝑛·0·9</meta></with></looped>" , " <manufactured meta=\"𝛿·0·1\">𝜎1</manufactured>" , "</dataize>" ]@@ -1556,7 +1581,7 @@ ["dataize", "--locator=Q.t", "--acyclic=plausible", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"] [] records <- readProtocol path- lines records `shouldContain` [" looped 𝜎1 := Φ.cyc( x ↦ 𝑛·0·8 ) # 𝔻(𝑛·0·4), plausible, repeats 𝑛·0·7"]+ lines records `shouldContain` [" looped 𝜎1 := Φ.cyc( x ↦ 𝑛·0·9 ) # 𝔻(𝑛·0·5), plausible, repeats 𝑛·0·8"] it "refuses the flag without a mode" $ withStdin "⟦ t ↦ ⟦ Δ ⤍ 01-02 ⟧ ⟧" $@@ -1615,10 +1640,10 @@ testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible"] ["40-45-00-00-00-00-00-00"] it "writes the recursive call it cuts to the protocol as a call of the object" $- recorded "protocolXXXXXX.txt" >>= (`shouldContain` [" looped 𝜎1 := Φ.down( i ↦ 𝑛·1·6 ) # plausible, repeats 𝑛·0·3"])+ recorded "protocolXXXXXX.txt" >>= (`shouldContain` [" looped 𝜎1 := Φ.down( i ↦ 𝑛·1·6 ) # plausible, repeats 𝑛·0·4"]) it "writes the recursive call it cuts to the XML protocol with the object and the metas of its arguments" $- recorded "protocolXXXXXX.xml" >>= (`shouldContain` [" <looped symbol=\"𝜎1\" by=\"morph\" match=\"plausible\" at=\"ξ.a\" of=\"𝑛·0·3\" object=\"Φ.down\"><with><meta attr=\"i\">𝑛·1·6</meta></with></looped>"])+ recorded "protocolXXXXXX.xml" >>= (`shouldContain` [" <looped symbol=\"𝜎1\" by=\"morph\" match=\"plausible\" at=\"ξ.a\" of=\"𝑛·0·4\" object=\"Φ.down\"><with><meta attr=\"i\">𝑛·1·6</meta></with></looped>"]) describe "--acyclic at a recursive call through a fork" $ do let recursive = "⟦ if(c, a, b) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ξ.c, left🌵 ↦ ξ.a, right🌵 ↦ ξ.b ⟧, wrap(v) ↦ ⟦⟧, down(i) ↦ ⟦ φ ↦ Φ.if( c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ Φ.down( i ↦ Φ.wrap( v ↦ i ) ), b ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧ ) ⟧, t ↦ Φ.down( i ↦ ⟦ Δ ⤍ 01- ⟧ ) ⟧"@@ -1639,13 +1664,13 @@ testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-loops=1"] ["40-45-00-00-00-00-00-00"] it "writes the copy it cuts in a side of a fork to the protocol as a call of the object" $- recorded "1" "protocolXXXXXX.txt" >>= (`shouldContain` [" looped 𝜎3 := Φ.down( i ↦ 𝑛·3·6 ) # plausible, repeats 𝑛·0·3"])+ recorded "1" "protocolXXXXXX.txt" >>= (`shouldContain` [" looped 𝜎3 := Φ.down( i ↦ 𝑛·3·6 ) # plausible, repeats 𝑛·0·4"]) it "writes the copy it cuts in a side of a fork to the XML protocol with the object and the metas of its arguments" $- recorded "1" "protocolXXXXXX.xml" >>= (`shouldContain` [" <looped symbol=\"𝜎3\" by=\"morph\" match=\"plausible\" at=\"ξ.left🌵\" of=\"𝑛·0·3\" object=\"Φ.down\"><with><meta attr=\"i\">𝑛·3·6</meta></with></looped>"])+ recorded "1" "protocolXXXXXX.xml" >>= (`shouldContain` [" <looped symbol=\"𝜎3\" by=\"morph\" match=\"plausible\" at=\"ξ.left🌵\" of=\"𝑛·0·4\" object=\"Φ.down\"><with><meta attr=\"i\">𝑛·3·6</meta></with></looped>"]) it "counts the copies the sides of earlier rounds of a fork made under --max-loops=2" $- recorded "2" "protocolXXXXXX.txt" >>= (`shouldContain` [" looped 𝜎3 := Φ.down( i ↦ 𝑛·6·6 ) # plausible, repeats 𝑛·0·3"])+ recorded "2" "protocolXXXXXX.txt" >>= (`shouldContain` [" looped 𝜎3 := Φ.down( i ↦ 𝑛·6·6 ) # plausible, repeats 𝑛·0·4"]) describe "--acyclic at a copy holding a λ" $ do let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, down(i) ↦ ⟦ φ ↦ Φ.dataized( Φ.fork( Φ.dataized( Φ.down( ⟦ λ ⤍ 𝜎2 ⟧ ) ), ⟦ λ ⤍ 𝜎3 ⟧ ) ) ⟧, x ↦ Φ.down( ⟦ λ ⤍ 𝜎1 ⟧ ) ⟧"@@ -1668,6 +1693,133 @@ it "writes the copy holding a λ it cuts to the protocol as a call of the object" $ recorded "protocolXXXXXX.txt" >>= (`shouldContain` [" looped 𝜎8 := Φ.dataized( target ↦ 𝜎7:λ ) # 𝔻(𝑛·6·4), plausible, repeats 𝑛·7·2"]) + describe "--acyclic at a copy holding a λ that evaluate fires" $ do+ let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ ⟦ φ ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x ) ) ) ⟧ ⟧"+ forking = T.pack "- λ: L_fork\n dataize:\n 𝛿1: $.on🌵\n morph:\n 𝑛1: $.left🌵\n 𝑛2: $.right🌵\n evaluate:\n 𝑛3: 𝑛1\n 𝑛4: 𝑛2\n join:\n on: 𝛿1\n left: 𝑛3\n right: 𝑛4\n otherwise: L_fork\n- λ: L_dataized\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"+ it "answers the copy holding a λ that evaluate cuts with a fresh symbol and goes on" $+ withLambdasOf forking $ \file ->+ withStdin recursive $+ testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]++ describe "--acyclic at a copy whose call ends with an attribute" $ do+ let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ), Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x ) ) ) ) ⟧"+ forking = T.pack "- λ: L_fork\n dataize:\n 𝛿1: $.on🌵\n morph:\n 𝑛1: $.left🌵\n 𝑛2: $.right🌵\n evaluate:\n 𝑛3: 𝑛1\n 𝑛4: 𝑛2\n join:\n on: 𝛿1\n left: 𝑛3\n right: 𝑛4\n otherwise: L_fork\n- λ: L_dataized\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"+ recorded :: String -> IO [String]+ recorded name =+ withTempFile name $ \(path, stream) -> do+ hClose stream+ withLambdasOf forking $ \file ->+ withStdin recursive $+ testCLISucceeded+ ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+ []+ lines <$> readProtocol path+ it "writes the copy it cuts to the protocol as a call of the object with the attribute it ends with" $+ recorded "protocolXXXXXX.txt" >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎6 := Φ.fork( left ↦ 𝑛·9·9, right ↦ 𝑛·11·1 ).φ # 𝔻(𝑛·9·6)"))++ it "writes the copy it cuts to the XML protocol with the object, the metas of its arguments and the attribute it ends with" $+ recorded "protocolXXXXXX.xml" >>= (`shouldSatisfy` any (isInfixOf "object=\"Φ.fork\" dispatch=\"φ\"><with><meta attr=\"left\">𝑛·9·9</meta><meta attr=\"right\">𝑛·11·1</meta></with></looped>"))++ describe "--acyclic at a copy whose argument repeats the same loop" $ do+ let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, times(b) ↦ ⟦ λ ⤍ L_times ⟧, x ↦ Φ.times( Φ.dataized( Φ.x ) ) ⟧"+ atoms = T.pack "- λ: L_times\n dataize:\n 𝛿1: $.b\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n- λ: L_dataized\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"+ it "ends the run with an answer once it cuts the loop" $+ withLambdasOf atoms $ \file ->+ withStdin recursive $+ testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--max-seconds=30"] ["40-45-00-00-00-00-00-00"]++ it "writes the cut of the argument inside the cut of the call to the protocol" $+ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+ hClose stream+ withLambdasOf atoms $ \file ->+ withStdin recursive $+ testCLISucceeded+ ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--max-seconds=30", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+ []+ records <- readProtocol path+ filter (isInfixOf "looped") (lines records) `shouldBe` [" looped 𝜎1 := Φ.dataized( target ↦ Φ.x ) # 𝔼(𝑛·6·2.b), plausible, repeats 𝑛·6·5", " looped 𝜎2 := Φ.times( b ↦ 𝜎1:λ ) # plausible, repeats 𝑛·6·2"]++ describe "--acyclic at a copy whose argument raises" $+ it "writes the copy of the terminator into the call it cuts by its name, never firing it" $+ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+ hClose stream+ withLambdasOf (T.pack "- λ: L_times\n terminators: [L_throw]\n dataize:\n 𝛿1: $.b\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n- λ: L_dataized\n terminators: [L_throw]\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \file ->+ withStdin "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, throw(message) ↦ ⟦ λ ⤍ L_throw ⟧, times(b, c) ↦ ⟦ λ ⤍ L_times ⟧, x ↦ Φ.times( Φ.dataized( Φ.x ), Φ.throw( 𝜎1:λ ) ) ⟧" $+ testCLISucceeded+ ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--max-seconds=30", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+ []+ records <- readProtocol path+ filter (isInfixOf "looped 𝜎3") (lines records) `shouldBe` [" looped 𝜎3 := Φ.times( b ↦ 𝜎2:λ, c ↦ 𝑛·6·11 ) # plausible, repeats 𝑛·6·4"]++ describe "--acyclic at a fork the memo fabricated" $ do+ let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, bool(fork) ↦ ⟦ if ↦ ξ.fork ⟧, num(φ) ↦ ⟦⟧, p ↦ ⟦ φ ↦ Φ.bool( ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧ ).if( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.p ) ) ) ⟧, q ↦ ⟦ φ ↦ Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ) ⟧, x ↦ Φ.bool( ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, on🌵 ↦ ⟦ λ ⤍ 𝜎1 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧ ).if( Φ.p, Φ.q ) ⟧"+ forking = T.pack "- λ: L_fork\n dataize:\n 𝛿1: $.on🌵\n morph:\n 𝑛1: $.left🌵\n 𝑛2: $.right🌵\n evaluate:\n 𝑛3: 𝑛1\n 𝑛4: 𝑛2\n join:\n on: 𝛿1\n left: 𝑛3\n right: 𝑛4\n otherwise: L_fork\n- λ: L_dataized\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"+ recorded :: IO [String]+ recorded =+ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+ hClose stream+ withLambdasOf forking $ \file ->+ withStdin recursive $+ testCLISucceeded+ ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+ []+ lines <$> readProtocol path+ it "answers the fork it cuts inside a formation the memo fabricated with a fresh symbol and goes on" $+ withLambdasOf forking $ \file ->+ withStdin recursive $+ testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]++ it "writes the fork it cuts inside a fabricated formation by its symbol alone, since no fact names it" $+ recorded >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎6 # 𝔻("))++ it "answers the fork it cuts inside a formation fabricated from a fork of the world with a fresh symbol and goes on" $+ withLambdasOf forking $ \file ->+ withStdin "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, p ↦ ⟦ φ ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.p ) ) ) ⟧, q ↦ ⟦ φ ↦ Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ) ⟧, x ↦ Φ.fork( Φ.p, Φ.q ) ⟧" $+ testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]++ describe "--acyclic at a fork written in place" $ do+ let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, bool(fork) ↦ ⟦ if ↦ ξ.fork ⟧, num(φ) ↦ ⟦⟧, p ↦ ⟦ φ ↦ Φ.bool( ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧ ).if( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.p ) ) ) ⟧, x ↦ Φ.p ⟧"+ forking = T.pack "- λ: L_fork\n dataize:\n 𝛿1: $.on🌵\n morph:\n 𝑛1: $.left🌵\n 𝑛2: $.right🌵\n evaluate:\n 𝑛3: 𝑛1\n 𝑛4: 𝑛2\n join:\n on: 𝛿1\n left: 𝑛3\n right: 𝑛4\n otherwise: L_fork\n- λ: L_dataized\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"+ recorded :: IO [String]+ recorded =+ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+ hClose stream+ withLambdasOf forking $ \file ->+ withStdin recursive $+ testCLISucceeded+ ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+ []+ lines <$> readProtocol path+ it "answers the fork it cuts with a fresh symbol and goes on" $+ withLambdasOf forking $ \file ->+ withStdin recursive $+ testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]++ it "writes the loop it cuts as a call of the object whose bindings the copy repeats exactly" $+ recorded >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎5 := Φ.p #"))++ it "dont get stuck above the fork it cuts" $+ recorded >>= (`shouldNotSatisfy` any (isInfixOf "stuck L_dataized"))++ describe "--acyclic at a fork nested in a side of another fork" $ do+ let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, bool(fork) ↦ ⟦ if ↦ ξ.fork ⟧, num(φ) ↦ ⟦⟧, p ↦ ⟦ φ ↦ Φ.bool( ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧ ).if( Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ), Φ.bool( ⟦ λ ⤍ L_fork, left ↦ ∅, right ↦ ∅, on🌵 ↦ ⟦ λ ⤍ 𝜎6 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧ ).if( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.p ) ) ) ) ⟧, x ↦ Φ.p ⟧"+ forking = T.pack "- λ: L_fork\n dataize:\n 𝛿1: $.on🌵\n morph:\n 𝑛1: $.left🌵\n 𝑛2: $.right🌵\n evaluate:\n 𝑛3: 𝑛1\n 𝑛4: 𝑛2\n join:\n on: 𝛿1\n left: 𝑛3\n right: 𝑛4\n otherwise: L_fork\n- λ: L_dataized\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"+ recorded :: IO [String]+ recorded =+ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+ hClose stream+ withLambdasOf forking $ \file ->+ withStdin recursive $+ testCLISucceeded+ ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]+ []+ lines <$> readProtocol path+ it "writes the loop it cuts inside the nested fork by its symbol alone, since no fact names it" $+ recorded >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎7 # 𝔻(𝑛·9·10), plausible"))++ it "dont get stuck above the nested fork it cuts" $+ recorded >>= (`shouldNotSatisfy` any (isInfixOf "stuck L_dataized"))+ it "dataizes with --sequence" $ withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $ testCLISucceeded@@ -1990,21 +2142,24 @@ lines records `shouldBe` [ "𝔻(Φ.e):" , " 𝕄(Φ.e):"- , " morphed 𝑛·0·1 := Φ.make:φ"- , " boxed 𝑛·0·2 := 𝑛·0·1.φ"- , " 𝕄(𝑛·0·2):"- , " morphed 𝑛·0·3 := L_make:λ"- , " 𝔼(L_make): # 𝔻(𝑛·0·2)"+ , " remembered 𝑛·0·1 ≡ Φ.foo # Φ.make:φ"+ , " morphed 𝑛·0·2 := 𝑛·0·1"+ , " boxed 𝑛·0·3 := 𝑛·0·2.φ"+ , " 𝕄(𝑛·0·3):"+ , " remembered 𝑛·0·4 ≡ Φ.make # L_make:λ"+ , " morphed 𝑛·0·5 := 𝑛·0·4"+ , " 𝔼(L_make): # 𝔻(𝑛·0·3)" , " 𝑛·1·1 := Φ.bytes( φ ↦ 𝜎1:λ ):φ # 𝑛" , " 𝕄(𝑛·1·1):" , " morphed 𝑛·1·2 := Φ.bytes( φ ↦ 𝜎1:λ ):φ" , " 𝑛·1·3 := 𝑛·1·2 # 𝕄(𝑛·1·1)"- , " boxed 𝑛·0·4 := 𝑛·1·3.φ"- , " 𝕄(𝑛·0·4):"- , " 𝑛·0·5 := Φ.bytes( φ ↦ 𝜎1:λ )"- , " 𝑛·0·6 := 𝜎1:λ:φ"- , " morphed 𝑛·0·7 := 𝑛·0·6"- , " boxed 𝑛·0·8 := 𝑛·0·7.φ"+ , " remembered 𝑛·1·3 ≡ 𝑛·0·4"+ , " boxed 𝑛·0·6 := 𝑛·1·3.φ"+ , " 𝕄(𝑛·0·6):"+ , " 𝑛·0·7 := Φ.bytes( φ ↦ 𝜎1:λ )"+ , " 𝑛·0·8 := 𝜎1:λ:φ"+ , " morphed 𝑛·0·9 := 𝑛·0·8"+ , " boxed 𝑛·0·10 := 𝑛·0·9.φ" , " 𝛿·0·1 := 𝔻(𝜎1:λ)" ] @@ -2273,6 +2428,39 @@ lines records `shouldContain` [" <starved limit=\"3\" by=\"dataize\" at=\"𝑛·1·2\"/>"] forM_+ [("XMLXXXXXX.xml", "<exceeded limit=\"7\" by=\"dataize\" at="), ("textXXXXXX.txt", "exceeded 7 # 𝔻(")]+ $ \(template, record) ->+ it ("writes the reached --max-cycles to the protocol " ++ template) $+ withTempFile template $ \(path, stream) -> do+ hClose stream+ withStdin "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧" $+ testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-cycles=7", "--partial", "--locator=Q.x", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+ records <- readProtocol path+ any (isPrefixOf record . dropWhile (== ' ')) (lines records) `shouldBe` True++ forM_+ [("XMLXXXXXX.xml", "<oversized limit=\"60\" by=\"morph\" at="), ("textXXXXXX.txt", "oversized 60")]+ $ \(template, record) ->+ it ("writes the reached --max-nodes to the protocol " ++ template) $+ withTempFile template $ \(path, stream) -> do+ hClose stream+ withStdin "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧" $+ testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-nodes=60", "--partial", "--locator=Q.x", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+ records <- readProtocol path+ any (isPrefixOf record . dropWhile (== ' ')) (lines records) `shouldBe` True++ forM_+ [("XMLXXXXXX.xml", "<blown limit=\"1K\" by="), ("textXXXXXX.txt", "blown 1K")]+ $ \(template, record) ->+ it ("writes the reached --max-memory to the protocol " ++ template) $+ withTempFile template $ \(path, stream) -> do+ hClose stream+ withStdin "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧" $+ testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-memory=1K", "--partial", "--locator=Q.x", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []+ records <- readProtocol path+ any (isPrefixOf record . dropWhile (== ' ')) (lines records) `shouldBe` True++ forM_ [("XMLXXXXXX.xml", "<spent limit=\"5\" by="), ("textXXXXXX.txt", " spent 5")] ( \(template, record) -> it ("writes a spent firing budget to the protocol as " ++ record) $@@ -3518,6 +3706,54 @@ records <- readProtocol path length (filter (isInfixOf "𝔼(L_split)") (lines records)) `shouldBe` 64 + describe "--max-nodes" $ do+ let growing = "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧"+ it "fails with non-positive --max-nodes" $+ withStdin growing $+ testCLIFailed ["dataize", "--max-nodes=0"] ["--max-nodes must be positive"]++ it "fails once the term grows over --max-nodes" $+ withStdin growing $+ testCLIFailed+ ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-nodes=60", "--locator=Q.x"]+ ["[ERROR]: Evaluation did not finish before reaching the limit of nodes: --max-nodes=60"]++ it "ends the growing term with --partial" $+ withStdin growing $+ testCLISucceeded+ ["morph", "--acyclic=plausible", "--max-loops=2", "--max-nodes=60", "--partial", "--locator=Q.x", "--flat", "--hide-rho", "--sweet"]+ ["Φ.m( 𝜎1:λ )"]++ it "passes a small run in a large program under --max-nodes" $+ withStdin ("⟦ x ↦ ⟦ φ ↦ ⟦ y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧.y ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $+ testCLISucceeded ["dataize", "--max-nodes=50", "--locator=Q.x"] ["05-"]++ describe "--max-memory" $ do+ let growing = "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧"+ it "fails with non-positive --max-memory" $+ withStdin growing $+ testCLIFailed ["dataize", "--max-memory=0G"] ["--max-memory must be positive"]++ it "fails with --max-memory of an unknown unit" $+ withStdin growing $+ testCLIFailed ["dataize", "--max-memory=8Q"] ["--max-memory must be a number of bytes, optionally ending with K, M, G or T"]++ it "fails once the heap grows over --max-memory" $+ withStdin growing $+ testCLIFailed+ ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-memory=1K", "--locator=Q.x"]+ ["[ERROR]: Evaluation did not finish before reaching the limit of memory: --max-memory=1K"]++ it "ends the growing term with --partial under --max-memory" $+ withStdin growing $+ testCLISucceeded+ ["morph", "--acyclic=plausible", "--max-loops=2", "--max-memory=1K", "--partial", "--locator=Q.x", "--flat", "--hide-rho", "--sweet"]+ ["Φ.m( 𝜎1:λ )"]++ it "passes a small run in a large program under --max-memory" $+ withStdin ("⟦ x ↦ ⟦ φ ↦ ⟦ y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧.y ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $+ testCLISucceeded ["dataize", "--max-memory=1G", "--locator=Q.x"] ["05-"]+ describe "--max-seconds" $ do let ladder = withLambdasOf (T.pack "- λ: L_split\n morph:\n 𝑛1: ξ.n.foo\n 𝑛2: ξ.n.foo\n 𝑛: ⟦ l ↦ 𝑛1, r ↦ 𝑛2 ⟧\n") rungs = "⟦ " ++ intercalate ", " [printf "l%d ↦ ⟦ λ ⤍ L_split, n ↦ Φ.l%d ⟧" rung (rung + 1) | rung <- [0 .. 23 :: Int]] ++ ", l24 ↦ ⟦⟧, x ↦ Φ.l0.foo ⟧"@@ -3640,11 +3876,16 @@ , " </morph>" , " <bound meta=\"𝑛1·1\">01-</bound>" , " <morph at=\"ξ.b\">"- , " <applied meta=\"𝑛·1·2\" by=\"morph\" at=\"ξ.b\" of=\"Φ.step\"><ref attr=\"tup\">Φ.items.tail</ref></applied>"- , " <formed meta=\"𝑛·1·3\" of=\"Φ.step\"><ref attr=\"tup\">Φ.items.tail</ref></formed>"- , " <morphed meta=\"𝑛·1·4\">𝑛·1·3</morphed>"+ , " <remembered meta=\"𝑛·1·2\" as=\"Φ.step\"/>"+ , " <applied meta=\"𝑛·1·3\" by=\"morph\" at=\"ξ.b\" of=\"Φ.step\"><ref attr=\"tup\">Φ.items.tail</ref></applied>"+ , " <formed meta=\"𝑛·1·4\" of=\"Φ.step\"><ref attr=\"tup\">Φ.items.tail</ref></formed>"+ , " <applied meta=\"𝑒·1·1\" of=\"𝑛·1·2\"><ref attr=\"tup\">Φ.items.tail</ref></applied>"+ , " <remembered of=\"𝑛·1·4\" as=\"𝑒·1·1\"/>"+ , " <morphed meta=\"𝑛·1·5\">𝑛·1·4</morphed>" , " </morph>"- , " <bound meta=\"𝑛2·1\">𝑛·1·4</bound>"+ , " <bound meta=\"𝑛2·1\">𝑛·1·5</bound>"+ , " <recalled of=\"𝑛·1·4\" as=\"𝑒·1·1\"/>"+ , " <recalled of=\"𝑛·1·2\" as=\"Φ.step\"/>" , " <deferred symbol=\"𝜎3\" by=\"morph\" at=\"𝑛2.φ\" of=\"Φ.step\"><with><symbol attr=\"tup\">𝜎1</symbol></with></deferred>" , " <diverged left=\"01-\" right=\"𝜎3\" at=\".Δ\" reason=\"the join names no otherwise\"><left Δ=\"01-\"/><right/></diverged>" , " </evaluate>"@@ -3657,7 +3898,7 @@ it "names an argument of a deferred copy that is no bare symbol by the meta its morph bound, though an element formed it" $ do records <- deferred [] "⟦ box(x, w) ↦ ⟦ φ ↦ x.next ⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎2 ⟧, a ↦ ⟦ Δ ⤍ 01- ⟧, b ↦ Φ.box( x ↦ Φ.items.tail, w ↦ ⟦ z ↦ Φ ⟧ ), λ ⤍ L_fork ⟧ ⟧"- records `shouldContain` [" <deferred symbol=\"𝜎3\" by=\"morph\" at=\"𝑛2.φ\" of=\"Φ.box\"><with><symbol attr=\"x\">𝜎1</symbol><meta attr=\"w\">𝑛·1·7</meta></with></deferred>"]+ records `shouldContain` [" <deferred symbol=\"𝜎3\" by=\"morph\" at=\"𝑛2.φ\" of=\"Φ.box\"><with><symbol attr=\"x\">𝜎1</symbol><meta attr=\"w\">𝑛·1·8</meta></with></deferred>"] it "names a deferred copy of a formation the world does not declare by the element that formed it" $ do records <- deferred [] "⟦ wrap(v) ↦ ⟦⟧, items ↦ ⟦ tail ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎2 ⟧, a ↦ ⟦ Δ ⤍ 01- ⟧, b ↦ Φ.wrap( v ↦ ⟦ inner(x) ↦ ⟦ φ ↦ x.next ⟧ ⟧ ).v.inner( x ↦ Φ.items.tail ), λ ⤍ L_fork ⟧ ⟧"@@ -3687,11 +3928,18 @@ ["morph", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=proven", "--max-firings=4"] ["[ERROR]: Evaluation did not finish before reaching the limit of firings: --max-firings=4"] - it "charges a formation once for the run under plausible" $+ it "charges a firing the memo answers under plausible" $ withLambdasOf pairs $ \file -> withStdin twins $+ testCLIFailed+ ["morph", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-firings=3"]+ ["[ERROR]: Evaluation did not finish before reaching the limit of firings: --max-firings=3"]++ it "answers every firing within the budget under plausible" $+ withLambdasOf pairs $ \file ->+ withStdin twins $ testCLISucceeded- ["morph", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-firings=3", "--flat", "--hide-rho", "--sweet"]+ ["morph", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-firings=4", "--flat", "--hide-rho", "--sweet"] ["b ↦ ⟦ φ ↦ 𝜎2:λ, plus(x) ↦ L_number_plus:λ ⟧"] it "reduces the operands of a formation once per argument spelling it under proven" $@@ -3721,12 +3969,12 @@ ["morph", "--symbolic=" ++ endless, "--locator=Q.x", "--max-steps=40"] ["[ERROR]: Morphing did not finish before reaching the limit of steps: --max-steps=40"] - it "prints the residue and exits successfully with the flag" $+ it "answers the looping dispatch with a symbol and exits successfully with the flag" $ loopingLambdas $ \endless -> withStdin looping $ testCLISucceeded ["morph", "--symbolic=" ++ endless, "--locator=Q.x", "--acyclic=proven", "--max-steps=4000", "--flat", "--hide-rho"]- ["⟦ λ ⤍ L_loop ⟧.foo"]+ ["⟦ λ ⤍ 𝜎1 ⟧"] it "answers a terminating program the same way with the flag" $ withStdin chained $@@ -4003,7 +4251,7 @@ it "refuses a rule it cannot compile" $ withTempDirectory "phino-compile" $ \dir -> do createDirectoryIfMissing True dir- writeFile (dir </> "having.yaml") "name: hv\npattern: '[[ x -> !e1, !B1 ]]'\nresult: '[[ !B1 ]]'\nhaving:\n eq: ['!e1', 'Q']\n"+ writeFile (dir </> "having.yaml") "name: hv\npattern: '[[ x -> !e1, !B1 ]]'\nresult: '[[ !B1 ]]'\nhaving:\n eq: ['!e1', '!e1']\n" withCurrentDirectory dir (testCLIFailed ["compile", "--rule=having.yaml", "--target=Compiled.hs"] ["The rule 'hv' cannot be compiled, since it has a 'having' condition"]) describe "match" $ do@@ -4061,9 +4309,9 @@ withStdin "[[ x -> Q.x, y -> Q.y ]]" $ testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x\n------\nt >> y"] - it "does not match a length against a literal that wraps around Int" $+ it "refuses a length compared with a literal that does not fit into Int" $ withStdin "[[ a -> $, b -> Q ]]" $- testCLIFailed ["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),18446744073709551618)"] ["no substitutions are built"]+ testCLIFailed ["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),18446744073709551618)"] ["compares a number with an expression"] it "builds substitutions with conditions" $ withStdin "[[ x -> Q.y ]].x" $@@ -4187,3 +4435,13 @@ testCLISucceeded ["merge", "--monoform", path] ["⟦ x ↦ ∅ ⟧"] it "rewrite names --monoform in its help" $ testCLISucceeded ["rewrite", "--help"] ["--monoform"]++ describe "prepareIO" $ do+ it "forces UTF-8 on the file system encoding, whatever the locale" $ do+ prepareIO+ enc <- getFileSystemEncoding+ textEncodingName enc `shouldBe` "UTF-8"+ it "forces UTF-8 on stderr, whatever the locale" $ do+ prepareIO+ enc <- hGetEncoding stderr+ maybe (expectationFailure "stderr has no encoding") (("UTF-8" `shouldBe`) . textEncodingName) enc
test/ConditionSpec.hs view
@@ -11,7 +11,7 @@ import Control.Monad (forM_) import Data.Either (isLeft, isRight) import Data.List (isInfixOf)-import Test.Hspec (Spec, describe, it, shouldBe, shouldSatisfy, shouldThrow)+import Test.Hspec (Spec, describe, expectationFailure, it, shouldBe, shouldSatisfy, shouldThrow) import Yaml qualified as Y spec :: Spec@@ -39,7 +39,6 @@ , ("eq(!i1,length(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i1")) (Y.CmpNum (Y.Length (BiMeta "B1")))) , ("eq(!i2,domain(!B1))", Y.Eq (Y.CmpNum (Y.MetaIndex "i2")) (Y.CmpNum (Y.Domain (BiMeta "B1")))) , ("gt(domain(!B1),!i1)", Y.Gt (Y.CmpNum (Y.Domain (BiMeta "B1"))) (Y.CmpNum (Y.MetaIndex "i1")))- , ("eq(!t1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "t1")) (Y.CmpExpr (ExMeta "e2"))) , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))]) , ("and(matches(\"hi\", !e1),part-of(!e1, !B1))", Y.And [Y.Matches "hi" (ExMeta "e1"), Y.PartOf (ExMeta "e1") (BiMeta "B1")]) , ("not(formation(!n1))", Y.Not (Y.IsFormation (ExMeta "n1")))@@ -54,8 +53,17 @@ [ "some()" , "in(!t, !t)" , "or(or(), or())"+ , "eq(!t1, !e2)" ] (\expr -> it expr (parseCondition expr `shouldSatisfy` isLeft))++ describe "refuses a condition that compares different kinds" $ do+ it "names the two kinds it cannot compare" $+ case parseCondition "eq(!e1, 5)" of+ Left err -> "compares an expression with a number" `isInfixOf` err `shouldBe` True+ Right _ -> expectationFailure "expected a refusal"+ it "accepts a quoted argument as an expression" $+ parseCondition "eq(!e1, \"5\")" `shouldSatisfy` isRight describe "parseConditionThrows" $ it "throws with a descriptive message on unparsable input" $
test/DataizeSpec.hs view
@@ -175,14 +175,14 @@ looping $ \endless -> do expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧" minted <- newIORef 0- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Dataization [] Map.empty endless (building linked) reduction evaluation dontSaveStep dontSaveEval linked)+ dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 Nothing Nothing (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Dataization [] Map.empty Nothing endless [] False (building linked) reduction evaluation dontSaveStep dontSaveEval linked) `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException)) it "parks the step limit as a residual with --partial" $ looping $ \endless -> do expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧" minted <- newIORef 0- (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True True Nothing 0 Dataization [] Map.empty endless (building linked) reduction evaluation dontSaveStep dontSaveEval linked)+ (outcome, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 25 Nothing Nothing (Steps 40 0) Nothing minted Nothing Nothing 1 Nothing False True True Nothing 0 Dataization [] Map.empty Nothing endless [] False (building linked) reduction evaluation dontSaveStep dontSaveEval linked) case outcome of Residual _ -> pure () Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts)@@ -302,12 +302,12 @@ forM_ [ ( "--max-cycles"- , \minted -> ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False Nothing 0 Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation dontSaveStep dontSaveEval linked+ , \minted -> ReduceContext ExRoot ExRoot Nothing 25 0 Nothing Nothing (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False Nothing 0 Dataization [] Map.empty Nothing emptyLambdas [] False (building linked) reduction evaluation dontSaveStep dontSaveEval linked , "--max-cycles=0" ) , ( "--max-depth"- , \minted -> ReduceContext ExRoot ExRoot Nothing 0 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False Nothing 0 Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation dontSaveStep dontSaveEval linked+ , \minted -> ReduceContext ExRoot ExRoot Nothing 0 25 Nothing Nothing (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing True True False Nothing 0 Dataization [] Map.empty Nothing emptyLambdas [] False (building linked) reduction evaluation dontSaveStep dontSaveEval linked , "--max-depth=0" ) ]@@ -320,12 +320,12 @@ it "does not throw without --depth-sensitive even once --max-depth is exhausted" $ do expr <- parseExpressionThrows boxed minted <- newIORef 0- (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 1 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation dontSaveStep dontSaveEval linked)+ (value, _, _) <- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 1 25 Nothing Nothing (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Dataization [] Map.empty Nothing emptyLambdas [] False (building linked) reduction evaluation dontSaveStep dontSaveEval linked) value `shouldBe` Dataized (BtOne "00") it "throws once --max-cycles is exhausted even without --depth-sensitive" $ do expr <- parseExpressionThrows boxed minted <- newIORef 0- dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Dataization [] Map.empty emptyLambdas (building linked) reduction evaluation dontSaveStep dontSaveEval linked)+ dataize expr emptyState (ReduceContext ExRoot ExRoot Nothing 25 0 Nothing Nothing (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Dataization [] Map.empty Nothing emptyLambdas [] False (building linked) reduction evaluation dontSaveStep dontSaveEval linked) `shouldThrow` (\e -> "--max-cycles=0" `isInfixOf` show (e :: SomeException)) describe "labels every step with a defined rule or operation" $ do
test/DepsSpec.hs view
@@ -12,7 +12,7 @@ import Data.List (isInfixOf, isPrefixOf) import Data.Time (LocalTime (LocalTime), TimeOfDay (TimeOfDay), ZonedTime (ZonedTime), fromGregorian, hoursToTimeZone) import Data.Time.Clock.POSIX (getPOSIXTime)-import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBound, EvBoxed, EvBuilt, EvCast, EvData, EvDeferred, EvDelta, EvDiverged, EvFabricated, EvFiring, EvHeader, EvJoined, EvLooped, EvManufactured, EvMorphed, EvReshaped, EvRun, EvStarted, EvStuck, EvStuckOn, EvSymbolized, EvTaken, EvTerm, EvUndressed, EvUnripe, EvWorld), Header (Header), Judgment (Dataization, Evaluation, Morphing), Nesting (..), Protocol (..), World (World), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep)+import Deps (Acyclic (Proven), Evaluation (EvAnswer, EvApplied, EvBound, EvBoxed, EvBuilt, EvCast, EvData, EvDeferred, EvDelta, EvDiverged, EvFabricated, EvFiring, EvHeader, EvJoined, EvLooped, EvManufactured, EvMemoized, EvMorphed, EvRecalled, EvRemembered, EvReshaped, EvRun, EvStarted, EvStuck, EvStuckOn, EvSymbolized, EvTaken, EvTerm, EvUndressed, EvUnripe, EvWorld), Header (Header), Judgment (Dataization, Evaluation, Morphing), Nesting (..), Protocol (..), World (World), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, resited, saveStep) import Fixtures (readUtf8, recorded, recordedWhole, recordedXml) import Forks (Refusal (..), Side (..)) import GHC.Clock (getMonotonicTime)@@ -255,8 +255,29 @@ 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 Nothing]) last (lines written) `shouldBe` " looped ⟦⟧ # proven"+ it "writes a cut that answered a copy no fact names by its symbol alone" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation []) ExRoot (Just (31, Nothing))])+ last (lines written) `shouldBe` " looped 𝜎31 # proven, repeats ⟦⟧"+ it "names the copy a path made in the fact it remembers" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvRemembered 1 (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "ёж"))]) (ExDispatch ExRoot (AtLabel "клён"))])+ last (lines written) `shouldBe` " remembered 𝑛·0·1 ≡ Φ.клён # ёж:φ"+ it "writes a fact about a named copy by its name alone" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ива")) (ArTau (AtLabel "у") ExRoot)) (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "у"))]) ExRoot, EvRemembered 1 (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "у"))]) (ExApplication (ExDispatch ExRoot (AtLabel "ива")) (ArTau (AtLabel "у") ExRoot))])+ last (lines written) `shouldBe` " remembered 𝑛·0·2 ≡ 𝑛·0·1"+ it "recalls a fact by the names its remembered line gave both sides, after a morphed line renamed the term" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvRun Morphing "Φ", EvRemembered 1 (ExFormation [BiTau (AtLabel "ель") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "ель"))]) (ExDispatch ExRoot (AtLabel "пихта")), EvMorphed 1 (ExFormation [BiTau (AtLabel "ель") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "ель"))]), EvRecalled 1 (ExFormation [BiTau (AtLabel "ель") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "ель"))]) (ExDispatch ExRoot (AtLabel "пихта"))])+ last (lines written) `shouldBe` " recalled 𝑛·0·1 ⇒ Φ.пихта"+ it "writes the answer the memo keeps for a formation as a memoized line" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ёрш" Dataization ExRoot, EvMemoized 2 (ExDispatch ExRoot (AtLabel "налим")) (ExFormation [BiLambda (FnSymbol 8)])])+ last (lines written) `shouldBe` " memoized 𝑛·1·1 ⇛ 𝜎8:λ # Φ.налим"+ it "recalls an answer the memo kept as its remembered line spelled it" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ёрш" Dataization ExRoot, EvMemoized 2 (ExFormation [BiTau (AtLabel "лещ") (ExFormation [])]) (ExFormation [BiLambda (FnSymbol 8)]), EvMorphed 2 (ExFormation [BiTau (AtLabel "лещ") (ExFormation [])]), EvRecalled 2 (ExFormation [BiTau (AtLabel "лещ") (ExFormation [])]) (ExFormation [BiLambda (FnSymbol 8)])])+ last (lines written) `shouldBe` " recalled 𝑛·1·1 ⇒ 𝜎8:λ"+ it "writes what the memo mapped a term to beside the term" $ do+ (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_сом" Dataization ExRoot, EvRecalled 2 (ExDispatch ExRoot (AtLabel "окунь")) (ExDispatch ExRoot (AtLabel "щука"))])+ last (lines written) `shouldBe` " recalled Φ.окунь ⇒ Φ.щука" it "writes a cut that answered a copy as the call of the object it repeats" $ do- (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation []) ExRoot (Just (14, ExApplication (ExDispatch ExRoot (AtLabel "клён")) (ArTau (AtLabel "ось") (ExFormation [BiLambda (FnSymbol 3)]))))])+ (_, written) <- recorded (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation []) ExRoot (Just (14, Just (ExApplication (ExDispatch ExRoot (AtLabel "клён")) (ArTau (AtLabel "ось") (ExFormation [BiLambda (FnSymbol 3)])))))]) last (lines written) `shouldBe` " looped 𝜎14 := Φ.клён( ось ↦ 𝜎3:λ ) # proven, repeats ⟦⟧" 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 "ю"))])@@ -610,9 +631,30 @@ it "writes a cut that answered no copy as an element naming the formation it entered" $ do (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvLooped 1 Morphing Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot Nothing]) lines written `shouldContain` [" <looped by=\"morph\" match=\"proven\" at=\"Φ\" of=\"𝑒·0·1\"/>"]+ it "writes a cut that answered a copy no fact names as an element naming no object" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot (Just (31, Nothing))])+ lines written `shouldContain` [" <looped symbol=\"𝜎31\" by=\"dataize\" match=\"proven\" at=\"Φ\" of=\"𝑒·0·1\"/>"]+ it "names the copy a path made in the element of the fact it remembers" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvRemembered 1 (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "ёж"))]) (ExDispatch ExRoot (AtLabel "клён"))])+ lines written `shouldContain` [" <remembered meta=\"𝑛·0·1\" as=\"Φ.клён\"/>"]+ it "writes a fact about a named copy as an element naming both sides" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "ива")) (ArTau (AtLabel "у") ExRoot)) (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "у"))]) ExRoot, EvRemembered 1 (ExFormation [BiTau AtPhi (ExDispatch ExXi (AtLabel "у"))]) (ExDispatch ExRoot (AtLabel "ива"))])+ lines written `shouldContain` [" <remembered of=\"𝑛·0·2\" as=\"Φ.ива\"/>"]+ it "recalls a fact as an element naming both sides the way its remembered element did, after a morphed element renamed the term" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvRemembered 1 (ExFormation [BiTau (AtLabel "ель") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "ель"))]) (ExDispatch ExRoot (AtLabel "пихта")), EvMorphed 1 (ExFormation [BiTau (AtLabel "ель") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "ель"))]), EvRecalled 1 (ExFormation [BiTau (AtLabel "ель") (ExFormation []), BiTau AtPhi (ExDispatch ExXi (AtLabel "ель"))]) (ExDispatch ExRoot (AtLabel "пихта"))])+ lines written `shouldContain` [" <recalled of=\"𝑛·0·1\" as=\"Φ.пихта\"/>"]+ it "writes the answer the memo keeps for a formation as a memoized element" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_ёрш" Dataization ExRoot, EvMemoized 2 (ExDispatch ExRoot (AtLabel "налим")) (ExFormation [BiLambda (FnSymbol 8)])])+ lines written `shouldContain` [" <memoized meta=\"𝑛·1·1\" as=\"𝜎8\"/>"]+ it "writes what the memo mapped a term to as an element naming both" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvFiring 1 "L_сом" Dataization ExRoot, EvRecalled 2 (ExDispatch ExRoot (AtLabel "окунь")) (ExDispatch ExRoot (AtLabel "щука"))])+ lines written `shouldContain` [" <recalled of=\"Φ.окунь\" as=\"Φ.щука\"/>"] it "writes a cut that answered a copy as an element naming the formation it repeats, the object and its arguments" $ do- (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot (Just (14, ExApplication (ExDispatch ExRoot (AtLabel "клён")) (ArTau (AtLabel "ось") (ExFormation [BiLambda (FnSymbol 3)]))))])+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot (Just (14, Just (ExApplication (ExDispatch ExRoot (AtLabel "клён")) (ArTau (AtLabel "ось") (ExFormation [BiLambda (FnSymbol 3)])))))]) lines written `shouldContain` [" <looped symbol=\"𝜎14\" by=\"dataize\" match=\"proven\" at=\"Φ\" of=\"𝑒·0·1\" object=\"Φ.клён\"><with><symbol attr=\"ось\">𝜎3</symbol></with></looped>"]+ it "writes a cut whose call ends with attributes as an element naming the object, its arguments and those attributes" $ do+ (_, written) <- recordedXml (\record -> mapM_ record [EvRun Dataization "Φ", EvLooped 1 Dataization Proven (ExFormation [BiTau (AtLabel "ъ") ExRoot]) ExRoot (Just (19, Just (ExDispatch (ExDispatch (ExApplication (ExDispatch ExRoot (AtLabel "вяз")) (ArTau (AtLabel "корень") (ExFormation [BiLambda (FnSymbol 5)]))) AtPhi) (AtLabel "ветка"))))])+ lines written `shouldContain` [" <looped symbol=\"𝜎19\" by=\"dataize\" match=\"proven\" at=\"Φ\" of=\"𝑒·0·1\" object=\"Φ.вяз\" dispatch=\"φ.ветка\"><with><symbol attr=\"корень\">𝜎5</symbol></with></looped>"] it "names an argument of a deferred copy by the formation an application made" $ do (_, written) <- recordedXml (\record -> mapM_ record [EvRun Morphing "Φ", EvApplied 1 Morphing (ExApplication (ExDispatch ExRoot (AtLabel "кулик")) (ArTau (AtLabel "ш") ExRoot)) (ExFormation [BiTau (AtLabel "ш") ExRoot]) ExRoot, EvDeferred 1 31 Morphing (ExFormation [BiTau (AtLabel "щ") (ExFormation [BiTau (AtLabel "ш") ExRoot]), BiTau AtPhi (ExDispatch ExXi (AtLabel "щ"))]) (Just (ExApplication (ExDispatch ExRoot (AtLabel "ёж")) (ArTau (AtLabel "щ") (ExFormation [BiTau (AtLabel "ш") ExRoot])))) ExRoot]) lines written `shouldContain` [" <deferred symbol=\"𝜎31\" by=\"morph\" at=\"Φ\" of=\"Φ.ёж\"><with><meta attr=\"щ\">𝑛·0·2</meta></with></deferred>"]
test/EvaluateSpec.hs view
@@ -10,6 +10,7 @@ import AST import CLI.Helpers (started)+import Control.Applicative ((<|>)) import Control.Exception (SomeException) import Control.Monad import Data.Aeson (FromJSON (parseJSON), camelTo2, defaultOptions, fieldLabelModifier, genericParseJSON)@@ -27,7 +28,7 @@ import Lining (LineFormat (SINGLELINE)) import Margin (defaultMargin) import Matcher (substEmpty)-import Morph (Deadline (..), ReduceContext (..), Steps (..), emptyState, execBuildTerm, memoized, morph, tallied)+import Morph (Deadline (..), ReduceContext (..), Steps (..), emptyState, execBuildTerm, factual, memoized, morph, tallied) import Parser (Form (MONOFORM), parseExpressionThrows') import Printer (printExpression, printExpression', printExpressionHidingRho') import Sugar (SugarType (SWEET))@@ -67,6 +68,7 @@ (_, written) <- recorded' hidden $ \record -> do let mode = named <$> acyclic cells <- memoized mode+ facts <- factual tally <- tallied firings base <- defaultReduceContext loc let ctx =@@ -74,6 +76,7 @@ { _partial = partial == Just True , _acyclic = mode , _memo = cells+ , _facts = Just facts , _steps = Steps (fromMaybe 250 steps) 0 , _tally = tally , _symbolic = known@@ -98,6 +101,22 @@ spelled hidden term = (if hidden then printExpressionHidingRho' else printExpression') term (SWEET, UNICODE, SINGLELINE, defaultMargin) +testRecalls :: FilePath -> Expectation+testRecalls pth = do+ pack <- Decode.decodeFileThrow pth+ orphans (map (dropWhile (== ' ')) (lines (protocol (pack :: SymbolPack)))) [] `shouldBe` []+ where+ orphans :: [String] -> [(String, String)] -> [String]+ orphans [] _ = []+ orphans (line : rest) facts = case (T.stripPrefix "remembered " (T.pack line) <|> T.stripPrefix "memoized " (T.pack line), T.stripPrefix "recalled " (T.pack line)) of+ (Just fact, _) -> orphans rest ([paired arrow (fst (T.breakOn " # " fact)) | arrow <- [" ≡ ", " ⇛ "], arrow `T.isInfixOf` fact] ++ facts)+ (_, Just recall)+ | paired " ⇒ " recall `elem` facts -> orphans rest facts+ | otherwise -> line : orphans rest facts+ _ -> orphans rest facts+ paired :: T.Text -> T.Text -> (String, String)+ paired arrow text = let (left, right) = T.breakOn arrow text in (T.unpack left, T.unpack (T.drop (T.length arrow) right))+ spec :: Spec spec = do known <- runIO fixtureLambdas@@ -106,6 +125,11 @@ let resources = "test-resources/evaluate-packs" packs <- runIO (allPathsIn resources) forM_ packs (\pth -> it (makeRelative resources pth) (testSymbols pth))++ describe "recalls only what the protocol of a pack remembered above" $ do+ let resources = "test-resources/evaluate-packs"+ packs <- runIO (allPathsIn resources)+ forM_ packs (\pth -> it (makeRelative resources pth) (testRecalls pth)) describe "execBuildTerm 'evaluate'" $ do let univ = ExFormation []
test/Fixtures.hs view
@@ -56,7 +56,7 @@ defaultReduceContext :: Expression -> IO ReduceContext defaultReduceContext loc = do minted <- newIORef 0- pure (ReduceContext loc loc Nothing 25 25 (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Morphing [] Map.empty emptyLambdas (building linked) reduction evaluation dontSaveStep dontSaveEval linked)+ pure (ReduceContext loc loc Nothing 25 25 Nothing Nothing (Steps 250 0) Nothing minted Nothing Nothing 1 Nothing False True False Nothing 0 Morphing [] Map.empty Nothing emptyLambdas [] False (building linked) reduction evaluation dontSaveStep dontSaveEval linked) linked :: Engine linked = fromMaybe yaml compiled
test/FunctionsSpec.hs view
@@ -146,6 +146,18 @@ , \term -> expectExpression term (DataString (strToBts "HellO")) ) ,+ ( "sed puts the group a back reference names into the replacement"+ , "sed"+ , [ArgExpression (DataString (strToBts "Hello, 2025")), ArgExpression (DataString (strToBts "s/([0-9]+)/\\1!/g"))]+ , \term -> expectExpression term (DataString (strToBts "Hello, 2025!"))+ )+ ,+ ( "sed keeps a digit after an escaped backslash in the replacement"+ , "sed"+ , [ArgExpression (DataString (strToBts "a")), ArgExpression (DataString (strToBts "s/a/\\\\1/"))]+ , \term -> expectExpression term (DataString (strToBts "\\1"))+ )+ , ( "random-string returns a literal pattern with no specials unchanged" , "random-string" , [ArgExpression (DataString (strToBts "static-name"))]
test/MorphSpec.hs view
@@ -17,10 +17,11 @@ import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (find, isInfixOf, nub) import Data.List.NonEmpty (NonEmpty (..))+import Data.Map.Strict qualified as Map import Data.Maybe (fromMaybe) import Data.Yaml qualified as Decode import Dataize (Outcome (..), dataize)-import Deps (Acyclic (..), Evaluation (EvMorphed, EvWorld), Judgment (..), State, Term (TeExpression))+import Deps (Acyclic (..), Evaluation (EvMorphed, EvRecalled, EvWorld), Judgment (..), State, Term (TeExpression)) import Engine (Engine (_normal)) import Files (allPathsIn) import Fixtures (defaultReduceContext, fixtureLambdas, linked, overdue, primitives)@@ -29,7 +30,7 @@ import Inference (Conclusion (Answered), Premises (Concludes, Morphs), direct) import Lambdas (Lambdas, emptyLambdas) import Matcher (substEmpty)-import Morph (Deadline (..), ReduceContext (..), emptyState, enter, execBuildTerm, inferred, insideUniverse, morph, morph')+import Morph (Deadline (..), ReduceContext (..), declared, emptyState, enter, execBuildTerm, inferred, insideUniverse, morph, morph', voided) import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule')@@ -299,3 +300,38 @@ base <- defaultReduceContext ExRoot (enter (formation 7) =<< enter (formation 6) =<< enter (formation 5) base{_acyclic = Just Plausible, _maxLoops = 1}) `shouldThrow` (\e -> "already inside" `isInfixOf` show (e :: SomeException))++ describe "places a formation among the objects of the world" $ do+ it "places a formation by the object the fact table maps it to" $ do+ let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))+ facts <- newIORef (Map.fromList [(hashExpression (ExFormation [BiTau AtPhi body]), [(ExFormation [BiTau AtPhi body], ExDispatch ExRoot (AtLabel "nq"))])])+ base <- defaultReduceContext ExRoot+ fmap fst <$> declared (ExFormation [BiTau (AtLabel "nq") (ExFormation [BiVoid AtPhi]), BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])+ `shouldReturn` Just (ExDispatch ExRoot (AtLabel "nq"))+ it "recalls every fact it follows on its way to the world, one by one" $ do+ let head' = ExFormation [BiVoid (AtLabel "ru"), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]+ copy = ExFormation [BiTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]+ applied = ExApplication head' (ArTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]))+ facts <- newIORef (Map.fromListWith (++) [(hashExpression term, [(term, source)]) | (term, source) <- [(head', ExDispatch ExRoot (AtLabel "vex")), (copy, applied)]])+ told <- newIORef []+ base <- defaultReduceContext ExRoot+ _ <- declared (ExFormation [BiTau (AtLabel "vex") head']) base{_facts = Just facts, _saveEval = \record -> modifyIORef' told (record :)} copy+ records <- readIORef told+ reverse [(term, reply) | EvRecalled _ term reply <- records] `shouldBe` [(copy, applied), (head', ExDispatch ExRoot (AtLabel "vex"))]+ it "answers the voids of the first head a chain of remembered copies was applied to" $ do+ let head' = ExFormation [BiVoid (AtLabel "ka"), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]+ half = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]+ full = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)]), BiLambda (Function "L_ozu")]+ facts <- newIORef (Map.fromListWith (++) [(hashExpression term, [(term, source)]) | (term, source) <- [(head', ExDispatch ExRoot (AtLabel "ozu")), (half, ExApplication head' (ArTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]))), (full, ExApplication half (ArTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)])))]])+ base <- defaultReduceContext ExRoot+ voided base{_facts = Just facts} full `shouldReturn` Just [AtLabel "ka", AtLabel "mu"]+ it "answers no voids for a formation the fact table does not hold" $ do+ facts <- newIORef Map.empty+ base <- defaultReduceContext ExRoot+ voided base{_facts = Just facts} (ExFormation [BiTau (AtLabel "pe") (ExFormation []), BiLambda (Function "L_uv")]) `shouldReturn` Nothing+ it "places nothing the fact table does not map" $ do+ let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))+ facts <- newIORef Map.empty+ base <- defaultReduceContext ExRoot+ fmap fst <$> declared (ExFormation [BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])+ `shouldReturn` Nothing
test/RegexpSpec.hs view
@@ -109,6 +109,10 @@ , ("handles unicode in replacement", "結果: $1", ["all", "データ"], "結果: データ") , ("handles dollar at end of string", "test$", ["x"], "test$") , ("handles double dollar", "$$1", ["x", "y"], "$y")+ , ("substitutes a group named by a back reference", "<\\1>", ["full", "a"], "<a>")+ , ("reads a back reference as a single digit", "\\10", ["full", "a"], "a0")+ , ("keeps an out of bounds back reference literal", "\\9", ["only"], "\\9")+ , ("keeps a digit after an escaped backslash literal", "\\\\1", ["full", "a"], "\\1") ] ( \(desc, template, groups, expected) -> it desc $ R.substituteGroups (utf8 template) (map utf8 groups) `shouldBe` utf8 expected
test/RewriterSpec.hs view
@@ -194,14 +194,18 @@ made <- newIORef [] _ <- rewrite (ExApplication (ExFormation [BiVoid (AtLabel "ж")]) (ArTau (AtLabel "ж") (ExFormation []))) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :))) readIORef made `shouldReturn` [(ExApplication (ExFormation [BiVoid (AtLabel "ж")]) (ArTau (AtLabel "ж") (ExFormation [])), ExFormation [BiTau (AtLabel "ж") (ExFormation [])])]- it "tells nothing of an application a step left the object it was" $ do+ it "tells an application a step left the object it was" $ do made <- newIORef []- _ <- rewrite (ExApplication (ExFormation [BiTau (AtLabel "ъ") (ExFormation [])]) (ArTau AtRho (ExFormation []))) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :)))- readIORef made `shouldReturn` []- it "tells nothing of the ρ a dispatch fills" $ do+ _ <- rewrite (ExApplication (ExFormation [BiTau AtRho (ExFormation []), BiTau (AtLabel "ъ") (ExFormation [])]) (ArTau AtRho (ExFormation [BiVoid (AtLabel "ц")]))) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :)))+ readIORef made `shouldReturn` [(ExApplication (ExFormation [BiTau AtRho (ExFormation []), BiTau (AtLabel "ъ") (ExFormation [])]) (ArTau AtRho (ExFormation [BiVoid (AtLabel "ц")])), ExFormation [BiTau AtRho (ExFormation []), BiTau (AtLabel "ъ") (ExFormation [])])]+ it "tells the ρ a dispatch fills, beside the object it made" $ do made <- newIORef [] _ <- rewrite (ExApplication (ExFormation [BiVoid AtRho, BiVoid (AtLabel "щ")]) (ArTau AtRho (ExFormation [BiTau (AtLabel "ё") (ExFormation [])]))) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :)))- readIORef made `shouldReturn` []+ readIORef made `shouldReturn` [(ExApplication (ExFormation [BiVoid AtRho, BiVoid (AtLabel "щ")]) (ArTau AtRho (ExFormation [BiTau (AtLabel "ё") (ExFormation [])])), ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "ё") (ExFormation [])]), BiVoid (AtLabel "щ")])]+ it "tells the dispatch a step took into an object" $ do+ made <- newIORef []+ _ <- rewrite (ExDispatch (ExFormation [BiTau (AtLabel "ыж") (ExFormation [BiVoid (AtLabel "ю")])]) (AtLabel "ыж")) (map (stepOf linked) normalizationRules) (RewriteContext ExRoot 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep (\redex copy -> modifyIORef' made ((redex, copy) :)))+ readIORef made >>= (`shouldSatisfy` elem (ExDispatch (ExFormation [BiTau (AtLabel "ыж") (ExFormation [BiVoid (AtLabel "ю")])]) (AtLabel "ыж")) . map fst) describe "rewrites by a locator" $ do it "rewrites the located part step after step" $ do@@ -212,6 +216,28 @@ expr <- parseExpressionThrows "⟦ t ↦ ⊥.a ⟧" rewrite expr [] (RewriteContext (ExDispatch ExRoot (AtLabel "w")) 25 25 False Nothing (building linked) (_normal linked) (_matching linked) MtDisabled Nothing dontSaveStep dontSaveMade) `shouldThrow` (\exc -> "Can't find object by locator" `isInfixOf` show (exc :: SomeException))++ describe "catches a loop that comes back to the term the run started from" $ do+ let steps =+ [ direct "a-to-b" False (\_ expr -> [ExFormation [BiTau (AtLabel "b") ExXi] | ExFormation [BiTau (AtLabel "a") ExXi] <- [expr]])+ , direct "b-to-a" False (\_ expr -> [ExFormation [BiTau (AtLabel "a") ExXi] | ExFormation [BiTau (AtLabel "b") ExXi] <- [expr]])+ ]+ context cycles locator some =+ RewriteContext locator 25 cycles False Nothing (building linked) (_normal linked) (every some) MtDisabled Nothing dontSaveStep dontSaveMade+ looping exc = "looping" `isInfixOf` show (exc :: SomeException)+ it "catches a loop that comes back to the term the run started from" $ do+ forM_+ [ (ExFormation [BiTau (AtLabel "a") ExXi], steps)+ , (ExFormation [BiTau (AtLabel "b") ExXi], steps)+ , (ExFormation [BiTau (AtLabel "a") ExXi], reverse steps)+ , (ExFormation [BiTau (AtLabel "b") ExXi], reverse steps)+ ]+ (\(start, some) -> rewrite start some (context 25 ExRoot some) `shouldThrow` looping)+ rewrite+ (ExFormation [BiTau (AtLabel "x") (ExFormation [BiTau (AtLabel "a") ExXi])])+ steps+ (context 1 (ExDispatch ExRoot (AtLabel "x")) steps)+ `shouldThrow` looping describe "rewrite packs" $ do let resources = "test-resources/rewriter-packs"
test/RuleSpec.hs view
@@ -12,18 +12,22 @@ import Builder (buildExpressionThrows) import Control.Monad import Data.Aeson+import Data.List (isInfixOf) import Data.Yaml qualified as Y import Engine (Engine (_normal)) import Files (allPathsIn) import Fixtures (linked) import Functions (buildTerm) import GHC.Generics+import Logger (LogLevel (DEBUG, ERROR), setLogConfig) import Matcher import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Printer (printSubsts) import Rule (RuleContext (RuleContext), isNF, matchExpressionWithRule, meetCondition, normalHeld, redex) import System.FilePath-import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldBe, shouldReturn, shouldSatisfy)+import System.IO (stderr)+import System.IO.Silently (hCapture)+import Test.Hspec (Spec, after_, describe, expectationFailure, it, runIO, shouldBe, shouldReturn, shouldSatisfy) import Yaml qualified data ConditionPack = ConditionPack@@ -256,3 +260,27 @@ terms <- mapM parseExpressionThrows samples found <- concat <$> sequence [matches term rule | term <- terms, rule <- Yaml.normalizationRules] found `shouldBe` []++ describe "a condition that cannot be built" $ do+ after_ (setLogConfig ERROR 25) $ do+ let context :: RuleContext+ context = RuleContext buildTerm Nothing (_normal linked)+ it "logs an unbound meta in 'part-of' and treats the condition as not met" $ do+ expr <- parseExpressionThrows "[[ x -> Q.y ]]"+ let substs = matchExpressionDeep (ExFormation [BiTau (AtLabel "x") (ExMeta "e1")]) expr+ cond = Yaml.PartOf (ExMeta "e1") (BiMeta "B1")+ length substs `shouldBe` 1+ setLogConfig DEBUG 25+ (captured, met) <- hCapture [stderr] (meetCondition cond substs context)+ met `shouldBe` []+ "Condition part-of(" `isInfixOf` captured `shouldBe` True+ it "logs an unbound meta in 'matches' and treats the condition as not met" $ do+ expr <- parseExpressionThrows "[[ x -> Q.y ]]"+ nested <- parseExpressionThrows "Q.x.!t9"+ let substs = matchExpressionDeep (ExFormation [BiTau (AtLabel "x") (ExMeta "e1")]) expr+ cond = Yaml.Matches "Q" nested+ length substs `shouldBe` 1+ setLogConfig DEBUG 25+ (captured, met) <- hCapture [stderr] (meetCondition cond substs context)+ met `shouldBe` []+ "Condition matches(" `isInfixOf` captured `shouldBe` True
test/YamlSpec.hs view
@@ -7,16 +7,19 @@ module YamlSpec where import AST (Alpha, Attribute, Binding, Bytes, Expression (ExMeta, ExRoot))-import Control.Exception (Exception (displayException), SomeException)+import Control.Exception (Exception (displayException), SomeException, bracket) import Control.Monad+import Data.ByteString qualified as BS import Data.Either (isLeft, isRight)-import Data.List (isInfixOf, nub, sort, (\\))+import Data.List (intercalate, isInfixOf, nub, sort, (\\)) import Data.Maybe (fromMaybe) import Data.Text qualified as T import Data.Text.Encoding (encodeUtf8) import Data.Yaml qualified as Yaml import Files (allPathsIn)+import System.Directory (getTemporaryDirectory, removeFile) import System.FilePath+import System.IO (hClose, openTempFile) import Test.Hspec (Spec, describe, expectationFailure, it, runIO, shouldBe, shouldSatisfy, shouldThrow) import Yaml (Condition (..), ContextualizeRule (..), DataizeRule (..), MorphRule (..), Number, Operation (..), Premise (..), Rule, contextualizationRules, dataizationRules, morphingRules, yamlRule) @@ -56,6 +59,25 @@ packs (\pth -> it (makeRelative resources pth) (void (yamlRule pth))) + it "reads a bare y, n, yes, no, on and off in a rule file as the attributes they spell" $ do+ let written :: (String -> String) -> String+ written spelled = "name: bare-words\npattern: ⟦ 𝜏1 ↦ 𝑒1, 𝐵1 ⟧\nresult: ⟦ 𝐵1 ⟧\nwhen:\n and:\n - eq: [𝜏1, " ++ spelled "n" ++ "]\n - in: [" ++ spelled "y" ++ ", 𝐵1]\n - disjoint: [[" ++ intercalate ", " (map spelled ["yes", "no", "on", "off"]) ++ "], [𝐵1]]"+ tmp <- getTemporaryDirectory+ bare <-+ bracket+ (openTempFile tmp "bare-words.yaml")+ (\(path, handle) -> hClose handle >> removeFile path)+ ( \(path, handle) -> do+ BS.hPut handle (encodeUtf8 (T.pack (written id)))+ hClose handle+ yamlRule path+ )+ show bare+ `shouldBe` either+ Yaml.prettyPrintParseException+ (show :: Rule -> String)+ (decodeYaml' (written (\word -> "'" ++ word ++ "'")))+ describe "fails on yaml typos" $ do let resources = "test-resources/yaml-typos" packs <- runIO (allPathsIn resources)@@ -330,6 +352,49 @@ describe "rejects a fractional literal number" $ it "fails on a fraction instead of silently rounding it" $ (decodeYaml' "2.5" :: Either Yaml.ParseException Number) `shouldSatisfy` isLeft++ describe "refuses a condition that compares different kinds" $ do+ forM_+ [+ ( "an expression with a number in 'eq'"+ , "eq: [𝑒1, 5]"+ , "The 'eq' condition compares an expression with a number, while it can compare only two numbers, two attributes or two expressions"+ )+ ,+ ( "an expression with an integral number in 'eq'"+ , "eq: [𝑒1, 5.0]"+ , "The 'eq' condition compares an expression with a number"+ )+ ,+ ( "an expression with a number in 'gt'"+ , "gt: [𝑒1, 3]"+ , "The 'gt' condition compares an expression with a number, while it can compare only two numbers"+ )+ ,+ ( "an expression with an attribute in 'eq'"+ , "eq: [𝑒1, 𝜏1]"+ , "The 'eq' condition compares an expression with an attribute"+ )+ ,+ ( "an attribute with an attribute in 'gt'"+ , "gt: ['!t1', '!t2']"+ , "The 'gt' condition compares an attribute with an attribute, while it can compare only two numbers"+ )+ ,+ ( "a nested 'not' that compares an expression with a number"+ , "not: {eq: ['!e1', 5]}"+ , "compares an expression with a number"+ )+ ]+ (\(desc, yaml, message) -> it ("rejects " ++ desc) ((decodeYaml' yaml :: Either Yaml.ParseException Condition) `shouldSatisfy` failsWith message))+ it "rejects a rule whose 'having' compares an expression with a number" $+ (decodeYaml' "name: hv\npattern: '⟦ x ↦ 𝑒1 ⟧'\nresult: '⟦ ⟧'\nhaving:\n eq: ['!e1', 5]" :: Either Yaml.ParseException Rule)+ `shouldSatisfy` failsWith "compares an expression with a number"+ it "rejects a morphing rule whose 'when' compares an expression with a number" $+ (decodeYaml' "name: mv\nmatch: '⟦ 𝜏1 ↦ 𝑒1 ⟧'\nuniverse: '⟦ ⟧'\nconclusion: '⟦ ⟧'\nwhen:\n eq: ['𝑒1', 5]" :: Either Yaml.ParseException MorphRule)+ `shouldSatisfy` failsWith "compares an expression with a number"+ it "accepts a quoted number as an expression" $+ (decodeYaml' "eq: ['𝑒1', '5']" :: Either Yaml.ParseException Condition) `shouldSatisfy` isRight describe "rejects an empty 'and' condition" $ it "fails on 'and: []'" $