phino-0.0.150: test/CLISpec.hs
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}
-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT
module CLISpec (spec) where
import CLI (runCLI)
import CLI.Types (CmdException (..), IOFormat (..))
import Control.Exception
import Control.Monad (forM_, unless)
import Data.Char (isDigit)
import Data.List (intercalate, isInfixOf, isPrefixOf, sort)
import Data.Text qualified as T
import Data.Time.Clock (addUTCTime, getCurrentTime)
import Data.Time.Clock.POSIX (getPOSIXTime)
import Data.Version (showVersion)
import Files (allPathsIn)
import Fixtures (explainPack, lambdasFile, loopingLambdas, readProtocol, readUtf8, withLambdasOf)
import GHC.IO.Handle
import Paths_phino (version)
import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, getTemporaryDirectory, listDirectory, makeAbsolute, removeDirectoryRecursive, removeFile, removePathForcibly, setModificationTime, withCurrentDirectory)
import System.Exit (ExitCode (ExitFailure))
import System.FilePath ((</>))
import System.IO
import System.Timeout (timeout)
import Test.Hspec
import Text.Printf (printf)
import Text.XML qualified as X
withStdin :: String -> IO a -> IO a
withStdin input action =
bracket (openTempFile "." "stdinXXXXXX.tmp") cleanup $ \(filePath, h) -> do
hSetEncoding h utf8
hPutStr h input
hFlush h
hClose h
withFile filePath ReadMode $ \hIn -> do
hSetEncoding hIn utf8
bracket (hDuplicate stdin) restoreStdin $ \_ -> do
hDuplicateTo hIn stdin
hSetEncoding stdin utf8
action
where
restoreStdin orig = hDuplicateTo orig stdin >> hClose orig
cleanup (fp, _) = removeFile fp
withStdout :: IO a -> IO (String, a)
withStdout action =
bracket
(openTempFile "." "stdoutXXXXXX.tmp")
cleanup
( \(path, hTmp) -> do
hSetEncoding hTmp utf8
oldOut <- hDuplicate stdout
oldErr <- hDuplicate stderr
hDuplicateTo hTmp stdout
hDuplicateTo hTmp stderr
result <-
action `finally` do
hFlush stdout
hFlush stderr
hDuplicateTo oldOut stdout >> hClose oldOut
hDuplicateTo oldErr stderr >> hClose oldErr
hClose hTmp
captured <- readFile path
_ <- evaluate (length captured)
return (captured, result)
)
where
cleanup (fp, _) = removeFile fp
withTempFile :: String -> ((FilePath, Handle) -> IO a) -> IO a
withTempFile pattern =
bracket
(openTempFile "." pattern)
(\(path, _) -> removeFile path)
withTempFileContent :: String -> String -> (FilePath -> IO a) -> IO a
withTempFileContent pattern content action =
withTempFile pattern $ \(path, h) -> do
hPutStr h content
hClose h
action path
withTempDirectory :: String -> (FilePath -> IO a) -> IO a
withTempDirectory prefix action = do
tmp <- getTemporaryDirectory
stamp <- getPOSIXTime
let dir = tmp </> (prefix ++ "-" ++ show (round (stamp * 1000000) :: Integer))
bracket (pure dir) removePathForcibly action
testCLI' :: [String] -> [String] -> Either ExitCode () -> Expectation
testCLI' args outputs exit = do
(out, result) <- withStdout (try (runCLI args) :: IO (Either ExitCode ()))
if null outputs
then
unless (null out) $
expectationFailure ("Expected that output is empty, but got:\n" ++ out)
else
forM_
outputs
( \output ->
unless (output `isInfixOf` out) $
expectationFailure
("Expected that output contains:\n" ++ output ++ "\nbut got:\n" ++ out)
)
result `shouldBe` exit
testCLISucceeded :: [String] -> [String] -> Expectation
testCLISucceeded args outputs = testCLI' args outputs (Right ())
symbolic :: String
symbolic = "--symbolic=" ++ lambdasFile
testCLIFailed :: [String] -> [String] -> Expectation
testCLIFailed args outputs = testCLI' args outputs (Left (ExitFailure 1))
resource :: String -> String
resource file = "test-resources/cli/expressions/" <> file
rule :: String -> String
rule file = "--rule=test-resources/cli/rules/" <> file
spec :: Spec
spec = do
it "prints version" $
testCLISucceeded ["--version"] [showVersion version]
it "prints help" $
testCLISucceeded
["--help"]
["Phino - CLI Manipulator of π-Calculus Expressions", "Usage:"]
describe "--pin" $
forM_
[
( "succeeds when --pin matches actual version"
, ["--pin=" ++ showVersion version, "rewrite", "--sweet"]
, testCLISucceeded
, ["β¦β§"]
)
,
( "fails when --pin doesn't match actual version"
, ["--pin=9.9.9.9", "rewrite"]
, testCLIFailed
, ["Version mismatch: --pin requires '9.9.9.9', but this is phino " ++ showVersion version]
)
,
( "fails when --pin is empty"
, ["--pin=", "rewrite"]
, testCLIFailed
, ["Version mismatch: --pin requires ''"]
)
]
(\(desc, args, test, expected) -> it desc (withStdin "[[ ]]" (test args expected)))
describe "--pin-file" $
forM_
[
( "succeeds when --pin-file holds actual version among spaces"
, Just (" \n" ++ showVersion version ++ " \t\n\n")
, testCLISucceeded
, ["β¦β§"]
)
,
( "fails when --pin-file holds another version"
, Just "7.3.0.41\n"
, testCLIFailed
, ["Version mismatch: --pin requires '7.3.0.41', but this is phino " ++ showVersion version]
)
,
( "fails when --pin-file is empty"
, Just " \n"
, testCLIFailed
, ["Version mismatch: --pin requires ''"]
)
,
( "fails when --pin-file is absent"
, Nothing
, testCLIFailed
, ["does not exist"]
)
]
( \(desc, content, test, expected) ->
it desc $
withTempDirectory "phino-pin-file" $ \dir -> do
createDirectoryIfMissing True dir
let file = dir </> "vΓ©rsion.txt"
forM_ content (writeFile file)
withStdin "[[ ]]" (test ["--pin-file=" ++ file, "rewrite", "--sweet"] expected)
)
it "fails when both --pin and --pin-file are given" $
withStdin "[[ ]]" $
testCLIFailed
["--pin=" ++ showVersion version, "--pin-file=pinned-version.txt", "rewrite"]
["[ERROR]"]
describe "--hide-rho" $
forM_
[
( "drops every rho binding from the default salty output"
, "[[ foo -> [[ x -> [[ ]], ^ -> $.y ]], y -> [[ ]] ]]"
, ["rewrite", "--flat", "--hide-rho"]
, ["β¦ foo β¦ β¦ x β¦ β¦β§ β§, y β¦ β¦β§ β§"]
)
,
( "also drops the rho that --sweet leaves behind"
, "[[ foo -> [[ x -> [[ ]], ^ -> $.y ]], y -> [[ ]] ]]"
, ["rewrite", "--flat", "--sweet", "--hide-rho"]
, ["β¦ foo β¦ β¦β§:x, y β¦ β¦β§ β§"]
)
,
( "keeps sweet numeric literals intact"
, "[[ a -> 42 ]]"
, ["rewrite", "--flat", "--sweet", "--hide-rho"]
, ["42:a"]
)
,
( "keeps the one-binding sugar after inline voids"
, "[[ x(y) -> [[ a -> 42, ^ -> ? ]] ]]"
, ["rewrite", "--flat", "--sweet", "--hide-rho"]
, ["β¦ x(y) β¦ 42:a β§"]
)
,
( "prints a lone void as the term without the rho would be printed"
, "β¦ a β¦ β¦ x β¦ β¦ Ο β¦ ΞΎ, y β¦ β
β§ β§ β§"
, ["rewrite", "--sweet", "--hide-rho"]
, ["β¦ x(y) β¦ β¦β§ β§:a"]
)
,
( "indents the body as the term without the rho would be indented"
, "β¦ a β¦ β¦ x β¦ β¦ Ο β¦ β
, b β¦ β¦ c β¦ β
, Ο β¦ β
β§ β§ β§ β§"
, ["rewrite", "--sweet", "--hide-rho", "--margin=3"]
, ["β¦\n b(c) β¦ β¦β§\nβ§:x:a"]
)
,
( "prints positional arguments as such once the rho is gone"
, "β¦ a β¦ ΞΎ.b(Ο β¦ ΞΎ, Ξ±0 β¦ ΞΎ.c, Ξ±1 β¦ ΞΎ.d) β§"
, ["rewrite", "--flat", "--sweet", "--hide-rho"]
, ["b( c, d ):a"]
)
]
(\(desc, input, args, expected) -> it desc (withStdin input (testCLISucceeded args expected)))
it "keeps a data literal sugared when it is applied to more arguments" $
withStdin "β¦ i β¦ 42(z β¦ ΞΎ.f), s β¦ \"Hello\"(z β¦ ΞΎ.f) β§" $
testCLISucceeded ["rewrite", "--sweet", "--flat"] ["β¦ i β¦ 42( z β¦ f ), s β¦ \"Hello\"( z β¦ f ) β§"]
it "prints the one-binding sugar after inline voids with --sweet" $
withStdin "[[ x(y) -> [[ a -> 42 ]] ]]" $
testCLISucceeded ["rewrite", "--sweet"] ["β¦ x(y) β¦ 42:a β§"]
it "prints debug info with --log-level=DEBUG" $
withStdin "[[]]" $
testCLISucceeded ["rewrite", "--log-level=DEBUG"] ["[DEBUG]:"]
describe "--log-level accepts every named level" $
forM_
["INFO", "info", "ERROR", "ERR", "error", "NONE", "none"]
( \flagValue ->
it ("--log-level=" ++ flagValue) $
withStdin "[[]]" $
testCLISucceeded ["rewrite", "--log-level=" ++ flagValue] ["β§"]
)
describe "--log-level prints nothing below its level" $
forM_
[("NONE", ["[DEBUG]", "[INFO]"]), ("ERROR", ["[DEBUG]", "[INFO]"]), ("INFO", ["[DEBUG]"])]
( \(level, hidden) ->
it ("--log-level=" ++ level) $
withStdin "[[]]" $ do
(out, _) <- withStdout (try (runCLI ["rewrite", "--log-level=" ++ level]) :: IO (Either ExitCode ()))
forM_ hidden (out `shouldNotContain`)
)
it "fails on an unrecognized --log-level value" $
withStdin "[[]]" $
testCLIFailed ["rewrite", "--log-level=verbose"] ["unknown log-level: verbose"]
describe "rewriting" $ do
describe "fails" $ do
forM_
[ ("with --input=latex", "", ["rewrite", "--input=latex"], ["The value 'latex' can't be used for '--input' option"])
, ("with negative --log-lines", "", ["rewrite", "--log-lines=-2"], ["--log-lines must be >= -1"])
, ("with negative --max-depth", "", ["rewrite", "--max-depth=-1"], ["--max-depth must be positive"])
, ("with zero --max-cycles", "", ["rewrite", "--max-cycles=0"], ["--max-cycles must be positive"])
, ("with zero --meet-length", "", ["rewrite", "--output=latex", "--meet-length=0"], ["--meet-length must be positive"])
,
( "with --normalize and --must=1"
, "[[ x -> [[ y -> 5 ]].y ]].x"
, ["rewrite", "--max-cycles=2", "--max-depth=1", "--normalize", "--must=1"]
, ["it's expected rewriting cycles to be in range [1], but rewriting has already reached 2"]
)
, ("when --in-place is used without input file", "[[ ]]", ["rewrite", "--in-place"], ["--in-place requires an input file"])
,
( "with --output=xmir on a non-top-level expression"
, "β¦ x β¦ 1, Ο β¦ 2 β§"
, ["rewrite", "--output=xmir"]
, ["[ERROR]:", "its top level must be a single binding"]
)
]
(\(desc, input, args, expected) -> it desc (withStdin input (testCLIFailed args expected)))
it "when --in-place is used with --target" $
withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
hPutStr h "[[ ]]"
hClose h
testCLIFailed
["rewrite", "--in-place", "--target=output.phi", path]
["--in-place and --target cannot be used together"]
it "fails when --in-place is used with a non-phi output format" $
withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
hPutStr h "[[ ]]"
hClose h
testCLIFailed
["rewrite", "--in-place", "--output=latex", path]
["--in-place can only be used together with --output=phi"]
it "does not leak a HasCallStack backtrace into errors" $ do
(out, _) <- withStdout (try (runCLI ["rewrite", "--in-place"]) :: IO (Either ExitCode ()))
out `shouldNotContain` "HasCallStack backtrace"
out `shouldNotContain` "ExitFailure 1"
out `shouldContain` "[ERROR]:"
it "prints optparse errors once, without a backtrace" $ do
(out, _) <- withStdout (try (runCLI ["rewrite", "--badopt"]) :: IO (Either ExitCode ()))
out `shouldNotContain` "HasCallStack backtrace"
out `shouldNotContain` "ExitFailure 1"
out `shouldContain` "[ERROR]:"
forM_
[ ("when --update is used without --target", "[[ ]]", ["rewrite", "--update"], ["--update requires --target"])
,
( "when --update is used without an input file"
, "[[ ]]"
, ["rewrite", "--update", "--target=output.phi"]
, ["--update requires an input file"]
)
,
( "when --sequence is used with --in-place"
, "[[ ]]"
, ["rewrite", "--sequence", "--in-place", "input.phi"]
, ["--in-place and --sequence cannot be used together"]
)
,
( "when --focus is used with --in-place"
, "[[ ]]"
, ["rewrite", "--focus=Q.y", "--in-place", "input.phi"]
, ["--in-place and --focus cannot be used together"]
)
,
( "when --show is used with --in-place"
, "[[ ]]"
, ["rewrite", "--show=Q.y", "--in-place", "input.phi"]
, ["--in-place and --show cannot be used together"]
)
,
( "when --update is used with --in-place"
, "[[ ]]"
, ["rewrite", "--update", "--in-place", "input.phi"]
, ["--update and --in-place cannot be used together"]
)
,
( "with --depth-sensitive"
, "[[ x -> \"x\"]]"
, ["rewrite", "--depth-sensitive", "--max-depth=1", "--max-cycles=1", rule "infinite.yaml"]
, ["[ERROR]: With option --depth-sensitive it's expected rewriting iterations amount does not reach the limit: --max-depth=1"]
)
,
( "with looping rules"
, "[[ x -> \"0\" ]]"
, ["rewrite", rule "first.yaml", rule "second.yaml", "--max-depth=1", "--max-cycles=3"]
, ["it seems rewriting is looping"]
)
]
(\(desc, input, args, expected) -> it desc (withStdin input (testCLIFailed args expected)))
it "with wrong attribute and valid error message" $
testCLIFailed
["rewrite", resource "with-$this-attribute.phi"]
[ "[ERROR]: Couldn't parse given phi expression, cause:"
, "unexpected"
]
forM_
[
( "with --output != latex and --nonumber"
, ["rewrite", "--nonumber", "--output=xmir"]
, ["The --nonumber option can stay together with --output=latex only"]
)
, ("with --omit-listing and --output != xmir", ["rewrite", "--omit-listing", "--output=phi"], ["--omit-listing"])
, ("with --omit-comments and --output != xmir", ["rewrite", "--omit-comments", "--output=phi"], ["--omit-comments"])
,
( "with --expression and --output != latex"
, ["rewrite", "--expression=foo", "--output=phi"]
, ["--expression option can stay together with --output=latex only"]
)
,
( "with --label and --output != latex"
, ["rewrite", "--label=foo", "--output=phi"]
, ["--label option can stay together with --output=latex only"]
)
,
( "with --compress and --output != latex"
, ["rewrite", "--compress", "--output=phi"]
, ["--compress option can stay together with --output=latex only"]
)
,
( "with --meet-prefix and --output != latex"
, ["rewrite", "--meet-prefix=foo", "--output=phi"]
, ["--meet-prefix option can stay together with --output=latex only"]
)
,
( "with wrong --hide option"
, ["rewrite", "--hide=Q.x(Q.y)"]
, ["[ERROR]: Invalid set of arguments: Only dispatch expression", "but given: Ξ¦.x( Ξ¦.y )"]
)
, ("with many --show options", ["rewrite", "--show=Q.x.y", "--show=hello"], ["The option --show can be used only once"])
,
( "with wrong --show option"
, ["rewrite", "--show=Q.x(Q.y)"]
, ["[ERROR]:", "Only dispatch expression started with Ξ¦ (or Q) can be used in --show"]
)
, ("with --show overlapping --hide", ["rewrite", "--show=Q.x", "--hide=Q.x"], ["[ERROR]:", "The --show locator 'Ξ¦.x' is also listed in --hide"])
, ("with --hide of an ancestor of --show", ["rewrite", "--show=Q.y.z", "--hide=Q.y"], ["[ERROR]:", "The --show locator 'Ξ¦.y.z' lies inside the --hide locator 'Ξ¦.y'"])
, ("with --meet-popularity < 0", ["rewrite", "--meet-popularity=-1"], ["[ERROR]:", "--meet-popularity must be positive"])
, ("with --meet-popularity > 100", ["rewrite", "--meet-popularity=102"], ["[ERROR]:", "--meet-popularity must be <= 100"])
,
( "with --meet-popularity and output != latex"
, ["rewrite", "--meet-popularity=51", "--output=phi"]
, ["[ERROR]:", "--meet-popularity option can stay together with --output=latex only"]
)
,
( "with --meet-length and output != latex"
, ["rewrite", "--meet-length=4", "--output=phi"]
, ["[ERROR]:", "--meet-length option can stay together with --output=latex only"]
)
, ("with non-dispatch --focus", ["rewrite", "--focus=Q.x(Q.y)"], ["[ERROR]"])
, ("with --focus!=Q and --output=XMIR", ["rewrite", "--focus=Q.x", "--output=xmir"], ["[ERROR]"])
, ("with --margin < 0", ["rewrite", "--margin=-1"], ["[ERROR]"])
, ("with --breakpoint which does not exist across the rules", ["rewrite", "--breakpoint=hello", "--normalize"], ["[ERROR]"])
]
(\(desc, args, expected) -> it desc (withStdin "" (testCLIFailed args expected)))
it "prints help" $
testCLISucceeded
["rewrite", "--help"]
["Rewrite the π-expression", "--seed SEED"]
it "accepts --seed flag" $
withStdin "[[ x -> 5 ]]" $
testCLISucceeded
["rewrite", "--seed=42", "--sweet"]
["5:x"]
it "defaults --seed to 0 in help" $
testCLISucceeded
["rewrite", "--help"]
["default: 0"]
it "reproduces the same shuffle order for the same --seed" $ do
let args =
[ "rewrite"
, "--shuffle"
, "--seed=42"
, "--sweet"
, "--sequence"
, "--max-depth=1"
, "--max-cycles=1"
, rule "swap-a.yaml"
, rule "swap-b.yaml"
]
(firstRun, _) <- withStdin "[[ x -> 5 ]]" $ withStdout (runCLI args)
(secondRun, _) <- withStdin "[[ x -> 5 ]]" $ withStdout (runCLI args)
firstRun `shouldBe` secondRun
it "fails with a non-integer --seed" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--seed=abc"]
["[ERROR]"]
it "saves steps to dir with --steps-dir" $
withTempDirectory "phino-steps" $ \dir ->
withStdin "[[ x -> \"hello\"]]" $ do
testCLISucceeded
["rewrite", rule "infinite.yaml", "--max-cycles=2", "--max-depth=2", "--steps-dir=" ++ dir, "--sweet"]
["hello_hi_hi"]
doesDirectoryExist dir `shouldReturn` True
files <- listDirectory dir
length files `shouldBe` 4
doesFileExist (dir ++ "/00001.phi") `shouldReturn` True
doesFileExist (dir ++ "/00003.phi") `shouldReturn` True
it "gives the saved steps the --canonize and --hide of the printed ones" $
withTempDirectory "phino-steps-filtered" $ \dir ->
withStdin "[[ m -> [[ x -> [[ L> Plus ]], y -> $.x ]].y, k -> [[ L> Minus ]] ]]" $ do
testCLISucceeded
["rewrite", "--normalize", "--hide=Q.k", "--canonize", "--steps-dir=" ++ dir, "--flat"]
["Fn1"]
files <- listDirectory dir
null files `shouldBe` False
saved <- mapM (\file -> readFile (dir ++ "/" ++ file)) files
concat saved `shouldNotContain` "Minus"
concat saved `shouldNotContain` "Plus"
it "saves dataize steps to dir with --steps-dir" $
withTempDirectory "phino-steps-dataize" $ \dir ->
withStdin "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]" $ do
testCLISucceeded
["dataize", symbolic, "--steps-dir=" ++ dir, "--sweet"]
["40-45"]
doesDirectoryExist dir `shouldReturn` True
files <- listDirectory dir
let steps = sort files
steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]
length steps `shouldSatisfy` (> 18)
it "saves steps with a .tex extension when --output=latex is used with --steps-dir" $
withTempDirectory "phino-steps-latex" $ \dir ->
withStdin "[[ x -> \"hello\"]]" $ do
testCLISucceeded
["rewrite", rule "infinite.yaml", "--max-cycles=2", "--max-depth=2", "--steps-dir=" ++ dir, "--output=latex", "--sweet"]
["\\begin{phiquation}"]
doesDirectoryExist dir `shouldReturn` True
files <- listDirectory dir
length files `shouldBe` 4
doesFileExist (dir ++ "/00001.tex") `shouldReturn` True
doesFileExist (dir ++ "/00003.tex") `shouldReturn` True
it "desugares without any rules flag from file" $
testCLISucceeded
["rewrite", resource "desugar.phi"]
["β¦ foo β¦ ΞΎ.x β§"]
it "desugares with without any rules flag from stdin" $
withStdin "[[foo β¦ x]]" $
testCLISucceeded ["rewrite"] ["β¦ foo β¦ ΞΎ.x β§"]
it "keeps the bytes of a string intact while desugaring it" $
withStdin "β¦ Ο β¦ Ξ¦.string(as-bytes β¦ Ξ¦.bytes(data β¦ β¦ Ξ β€ 65-0A-65, Ο β¦ β
β§)), Ο β¦ β
β§" $
testCLISucceeded ["rewrite", "--flat"] ["Ξ β€ 65-0A-65"]
it "rewrites with single rule" $
withStdin "T(x -> Q.y)" $
testCLISucceeded ["rewrite", "--rule=resources/normalize/dc.yaml"] ["β₯"]
it "fails when a rewriting rule uses a dataization-only function" $
withStdin "β¦β§" $
testCLIFailed
["rewrite", rule "evaluate-in-rewrite.yaml"]
["Function 'evaluate' in rule 'uses-evaluate' is available only for dataization and morphing, not for rewriting"]
it "names the join function in the error message" $
withStdin "β¦β§" $
testCLIFailed
["rewrite", rule "join-broken.yaml"]
["Function join() can work with bindings only"]
it "normalizes with --normalize flag" $
testCLISucceeded
["rewrite", "--normalize", resource "normalize.phi", "--margin=25"]
[ unlines
[ "β¦"
, " x β¦ β¦"
, " Ο β¦ β¦ y β¦ β¦ Ο β¦ β
β§ β§"
, " β§"
, "β§"
]
]
it "normalizes and applies --rule at the same time" $
withStdin "β¦ k β¦ β¦ m β¦ β¦ Ξ β€ 01- β§ β§.m, j β¦ β¦ Ξ» β€ Marker β§ β§" $
testCLISucceeded
["rewrite", "--normalize", rule "marker.yaml", "--sweet"]
["β¦ k β¦ 01-:Ξ, j β¦ FF-:Ξ β§"]
it "normalizes from stdin" $
withStdin "β¦ a β¦ β¦ b β¦ β
β§ (b β¦ [[ ]]) β§" $
testCLISucceeded
["rewrite", "--normalize", "--margin=20"]
["β¦ a β¦ β¦ b β¦ β¦β§ β§ β§"]
it "rewrites with --sweet flag" $
withStdin "[[ x -> 5]]" $
testCLISucceeded
["rewrite", "--sweet"]
["5:x"]
it "rewrites as XMIR" $
withStdin "[[ x -> Q.y ]]" $
testCLISucceeded
["rewrite", "--output=xmir"]
["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", " <o base=\"Ξ¦.y\" name=\"x\"/>"]
it "emits a real revision and ms in XMIR" $ do
(output, _) <- withStdin "[[ x -> Q.y ]]" $ withStdout (runCLI ["rewrite", "--output=xmir"])
let attrValue :: String -> String -> String
attrValue name text =
let needle = name ++ "=\""
breakOn :: String -> Maybe String
breakOn haystack
| needle `isPrefixOf` haystack = Just (drop (length needle) haystack)
| null haystack = Nothing
| otherwise = breakOn (drop 1 haystack)
in case breakOn text of
Just afterNeedle -> takeWhile (/= '"') afterNeedle
Nothing -> ""
revision = attrValue "revision" output
ms = attrValue "ms" output
revision `shouldSatisfy` (\sha -> length sha == 7 && all (`elem` "0123456789abcdef") sha)
revision `shouldNotBe` "1234567"
ms `shouldSatisfy` (all isDigit)
it "rewrites as LaTeX" $
withStdin "[[ x_o -> Q.z(y -> 5), q$ -> T, w -> $, ^ -> Q, @ -> 1, y -> \"H$@^M\", L> Fu_nc ]]" $
testCLISucceeded
["rewrite", "--output=latex", "--sweet"]
[ unlines
[ "\\begin{phiquation}"
, "[["
, " |x\\char95{}o| -> Q . |z| ( |y| -> 5 ),"
, " |q\\char36{}| -> T,"
, " |w| -> \\phiTerminal{\\xi},"
, " \\phiTerminal{\\rho} -> Q,"
, " @ -> 1,"
, " |y| -> \"H\\char36{}\\char64{}\\char94{}M\","
, " L> |Fu\\char95{}nc|"
, "]]{.}"
, "\\end{phiquation}"
]
]
it "rewrites as LaTeX without numeration" $
withStdin "[[ x -> 5 ]]" $
testCLISucceeded
["rewrite", "--output=latex", "--sweet", "--nonumber", "--flat"]
[ unlines
[ "\\begin{phiquation*}"
, "5 : |x|{.}"
, "\\end{phiquation*}"
]
]
it "rewrites an alpha-index argument as \\alpha subscript in LaTeX" $
withStdin "Q.foo(~1 -> Q.y)" $
testCLISucceeded
["rewrite", "--output=latex", "--flat", "--nonumber"]
[ unlines
[ "\\begin{phiquation*}"
, "Q . |foo| ( \\phiTerminal{\\alpha_{1}} -> Q . |y| ){.}"
, "\\end{phiquation*}"
]
]
it "rewrite as LaTeX with expression name" $
withStdin "[[ x -> 5 ]]" $
testCLISucceeded
["rewrite", "--output=latex", "--sweet", "--flat", "--expression=foo"]
[ unlines
[ "\\begin{phiquation}"
, "\\phiExpression{foo} 5 : |x|{.}"
, "\\end{phiquation}"
]
]
it "rewrite as LaTeX with label name" $
withStdin "[[ x -> 5 ]]" $
testCLISucceeded
["rewrite", "--output=latex", "--sweet", "--flat", "--label=foo"]
[ unlines
[ "\\begin{phiquation}\n\\label{foo}"
, "5 : |x|{.}"
, "\\end{phiquation}"
]
]
it "rewrites with XMIR as input" $
withStdin "<object><o name=\"app\"><o name=\"x\" base=\"Ξ¦.number\"/></o></object>" $
testCLISucceeded
["rewrite", "--input=xmir", "--sweet"]
["Ξ¦.number:x:app"]
it "rewrites and prints with XMIR as input and output" $
withStdin
( intercalate
""
[ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<object><o name=\"app\"><o name=\"x\" base=\"Ξ¦.number\"/></o></object>"
]
)
( testCLISucceeded
["rewrite", "--input=xmir", "--output=xmir", "--sweet", "--flat"]
[ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<listing>Ξ¦.number:x:app</listing>"
]
)
it "rewrites as XMIR with omit-listing flag" $
withStdin "[[ x -> Q.y ]]" $
testCLISucceeded
["rewrite", "--output=xmir", "--omit-listing"]
["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", "<listing>1 line(s)</listing>", " <o base=\"Ξ¦.y\" name=\"x\"/>"]
it "does not fail on exactly 1 rewriting" $
withStdin "β¦ t β¦ β¦ x β¦ \"foo\" β§ β§" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--must=1", "--sweet"]
["\"bar\":x"]
it "prints many expressions with --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
[ "rewrite"
, rule "first.yaml"
, rule "second.yaml"
, "--max-depth=1"
, "--max-cycles=2"
, "--sequence"
, "--sweet"
, "--flat"
]
[ unlines
[ "\"foo\":x"
, "Ξ¦.x( y β¦ \"foo\" )"
, "\"foo\":x"
]
]
it "prefixes every step with a header when --headers is on" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
[ "rewrite"
, rule "first.yaml"
, rule "second.yaml"
, "--max-depth=1"
, "--max-cycles=2"
, "--sequence"
, "--headers"
, "--sweet"
, "--flat"
]
[ intercalate
"\n"
[ ""
, "=== Step #1"
, "\"foo\":x"
, ""
, "=== Step #2, Rule 'first', 23t -> 26t"
, "Ξ¦.x( y β¦ \"foo\" )"
, ""
, "=== Step #3, Rule 'second', 26t -> 23t"
, "\"foo\":x"
]
]
it "ignores --headers without --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--headers", "--sweet", "--flat"]
["\"bar\":x"]
it "emits step headers as LaTeX comments with --headers" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
[ "rewrite"
, rule "first.yaml"
, rule "second.yaml"
, "--max-depth=1"
, "--max-cycles=2"
, "--sequence"
, "--headers"
, "--sweet"
, "--flat"
, "--output=latex"
]
[ unlines
[ "\\begin{phiquation}"
, "% === Step #1"
, "\"foo\" : |x| \\phiNormalize[\\nameref{r:first}]"
, "% === Step #2, Rule 'first', 23t -> 26t"
, " \\phiNormalize Q . |x| ( |y| -> \"foo\" ) \\phiNormalize[\\nameref{r:second}]"
, "% === Step #3, Rule 'second', 26t -> 23t"
, " \\phiNormalize \"foo\" : |x|{.}"
, "\\end{phiquation}"
]
]
it "prints only one latex preamble with --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
[ "rewrite"
, rule "first.yaml"
, rule "second.yaml"
, "--max-depth=1"
, "--max-cycles=2"
, "--sequence"
, "--sweet"
, "--flat"
, "--output=latex"
]
[ unlines
[ "\\begin{phiquation}"
, "\"foo\" : |x| \\phiNormalize[\\nameref{r:first}]"
, " \\phiNormalize Q . |x| ( |y| -> \"foo\" ) \\phiNormalize[\\nameref{r:second}]"
, " \\phiNormalize \"foo\" : |x|{.}"
, "\\end{phiquation}"
]
]
it "prints meet prefix with --meet-prefix=foo in LaTeX" $
withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $
testCLISucceeded
["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress", "--meet-prefix=foo"]
[ unlines
[ "\\begin{phiquation}"
, "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> |42-| : D ) . |y| \\phiNormalize[\\nameref{r:copy}]"
, " \\phiNormalize \\phinoMeet{foo:1}{ [[ |x| -> |42-| : D, |y| -> |x| ]] } . |y| \\phiNormalize[\\nameref{r:dot}]"
, " \\phiNormalize |42-| : D : |x| . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\phiNormalize[\\nameref{r:dot}]"
, " \\phiNormalize |42-| : D ( \\phiTerminal{\\rho} -> |42-| : D : |x|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\phiNormalize[\\nameref{r:skip}]"
, " \\phiNormalize |42-| : D ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\phiNormalize[\\nameref{r:skip}]"
, " \\phiNormalize |42-| : D{.}"
, "\\end{phiquation}"
]
]
it "prints with compressed expressions in LaTeX" $
withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $
testCLISucceeded
["rewrite", "--normalize", "--sweet", "--sequence", "--output=latex", "--flat", "--compress"]
[ unlines
[ "\\begin{phiquation}"
, "[[ |x| -> ?, |y| -> |x| ]] ( |x| -> |42-| : D ) . |y| \\phiNormalize[\\nameref{r:copy}]"
, " \\phiNormalize \\phinoMeet{1}{ [[ |x| -> |42-| : D, |y| -> |x| ]] } . |y| \\phiNormalize[\\nameref{r:dot}]"
, " \\phiNormalize |42-| : D : |x| . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\phiNormalize[\\nameref{r:dot}]"
, " \\phiNormalize |42-| : D ( \\phiTerminal{\\rho} -> |42-| : D : |x|, \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\phiNormalize[\\nameref{r:skip}]"
, " \\phiNormalize |42-| : D ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\phiNormalize[\\nameref{r:skip}]"
, " \\phiNormalize |42-| : D{.}"
, "\\end{phiquation}"
]
]
it "should not print \\phinoMeet{} twice" $
withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
testCLISucceeded
["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet"]
[ unlines
[ "\\begin{phiquation}"
, "[[ |y| -> ?, |k| -> \\phinoMeet{1}{ 42 : |t| } ]] ( |y| -> \\phinoAgain{1} ) : |x| . |i| : |ex| \\phiNormalize[\\nameref{r:copy}]"
, " \\phiNormalize [[ |y| -> \\phinoAgain{1}, |k| -> \\phinoAgain{1} ]] : |x| . |i| : |ex| \\phiNormalize[\\nameref{r:stop}]"
, " \\phiNormalize T : |ex|{.}"
, "\\end{phiquation}"
]
]
it "should not meet expression with high --meet-popularity" $
withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
testCLISucceeded
["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-popularity=70"]
[ unlines
[ "\\begin{phiquation}"
, "[[ |y| -> ?, |k| -> 42 : |t| ]] ( |y| -> 42 : |t| ) : |x| . |i| : |ex| \\phiNormalize[\\nameref{r:copy}]"
, " \\phiNormalize [[ |y| -> 42 : |t|, |k| -> 42 : |t| ]] : |x| . |i| : |ex| \\phiNormalize[\\nameref{r:stop}]"
, " \\phiNormalize T : |ex|{.}"
, "\\end{phiquation}"
]
]
it "meets with --meet-length=32" $
withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
testCLISucceeded
["rewrite", "--normalize", "--sequence", "--flat", "--compress", "--output=latex", "--sweet", "--meet-length=32"]
[ unlines
[ "\\begin{phiquation}"
, "[[ |y| -> ?, |k| -> 42 : |t| ]] ( |y| -> 42 : |t| ) : |x| . |i| : |ex| \\phiNormalize[\\nameref{r:copy}]"
, " \\phiNormalize [[ |y| -> 42 : |t|, |k| -> 42 : |t| ]] : |x| . |i| : |ex| \\phiNormalize[\\nameref{r:stop}]"
, " \\phiNormalize T : |ex|{.}"
, "\\end{phiquation}"
]
]
it "focuses expression in latex with sequence" $
withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
testCLISucceeded
["rewrite", "--normalize", "--sequence", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"]
[ unlines
[ "\\begin{phiquation}"
, "[[ |y| -> ?, |k| -> 42 : |t| ]] ( |y| -> 42 : |t| ) : |x| . |i| \\phiNormalize[\\nameref{r:copy}]"
, " \\phiNormalize [[ |y| -> 42 : |t|, |k| -> 42 : |t| ]] : |x| . |i| \\phiNormalize[\\nameref{r:stop}]"
, " \\phiNormalize T{.}"
, "\\end{phiquation}"
]
]
it "focuses expression in latex without sequence" $
withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
testCLISucceeded
["rewrite", "--normalize", "--flat", "--output=latex", "--sweet", "--focus=Q.ex"]
[ unlines
[ "\\begin{phiquation}"
, "T{.}"
, "\\end{phiquation}"
]
]
it "shows exceeding of limits in latex" $
withStdin "[[ x -> $.y, y -> $.x ]].x" $
testCLISucceeded
["rewrite", "--normalize", "--flat", "--sequence", "--output=latex", "--sweet", "--max-depth=1", "--max-cycles=1"]
[ unlines
[ "\\begin{phiquation}"
, "[[ |x| -> |y|, |y| -> |x| ]] . |x| \\phiNormalize[\\nameref{r:dot}]"
, " \\phiNormalize |x| : |y| . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\phiNormalize"
, " \\phiNormalize \\dots"
, "\\end{phiquation}"
]
]
it "focuses expression in phi without sequence" $
withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
testCLISucceeded
["rewrite", "--normalize", "--flat", "--output=phi", "--sweet", "--focus=Q.ex"]
["β₯"]
it "focuses expression in phi with sequence" $
withStdin "[[ ex -> [[ x -> [[ y -> ?, k -> [[ t -> 42]] ]]( y -> [[ t -> 42 ]]) ]].i ]]" $
testCLISucceeded
["rewrite", "--normalize", "--sequence", "--flat", "--output=phi", "--sweet", "--focus=Q.ex"]
[ unlines
[ "β¦ y β¦ β
, k β¦ 42:t β§( y β¦ 42:t ):x.i"
, "β¦ y β¦ 42:t, k β¦ 42:t β§:x.i"
, "β₯"
]
]
it "prints input as listing in XMIR" $
withStdin "[[ app -> [[]] ]]" $
testCLISucceeded
["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat"]
[" <listing>[[ app -> [[]] ]]</listing>"]
it "print expression in listing in XMIRs with --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat", "--sequence", rule "simple.yaml"]
[" <listing>\"foo\":x</listing>", " <listing>\"bar\":x</listing>"]
describe "must range tests" $ do
describe "fails" $ do
it "when cycles exceed range ..1" $
withStdin "[[ x -> [[ y -> 5 ]].y ]].x" $
testCLIFailed
["rewrite", "--max-depth=1", "--max-cycles=2", "--normalize", "--must=..1"]
["it's expected rewriting cycles to be in range [..1], but rewriting has already reached 2"]
it "when cycles below range 2.." $
withStdin "β¦ t β¦ β¦ x β¦ \"foo\" β§ β§" $
testCLIFailed
["rewrite", rule "simple.yaml", "--must=2.."]
["it's expected rewriting cycles to be in range [2..], but rewriting stopped after 1"]
it "with invalid range 5..3" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--must=5..3"]
["cannot parse value `5..3'"]
it "with negative in range -1..5" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--must=-1..5"]
["cannot parse value `-1..5'"]
it "with malformed range syntax" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--must=3...5"]
["cannot parse value `3...5'"]
it "accepts range ..5 (0 to 5 cycles)" $
withStdin "[[ ]]" $
testCLISucceeded ["rewrite", "--must=..5", "--sweet"] ["β¦β§"]
it "accepts range 0..0 (exactly 0 cycles)" $
withStdin "[[ ]]" $
testCLISucceeded ["rewrite", "--must=0..0", "--sweet"] ["β¦β§"]
it "accepts range 1..1 (exactly 1 cycle)" $
withStdin "β¦ t β¦ β¦ x β¦ \"foo\" β§ β§" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--must=1..1", "--sweet"]
["\"bar\":x"]
it "accepts range 1..3 when 1 cycle happens" $
withStdin "β¦ t β¦ β¦ x β¦ \"foo\" β§ β§" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--must=1..3", "--sweet"]
["\"bar\":x"]
it "accepts range 0.. (0 or more)" $
withStdin "[[ ]]" $
testCLISucceeded ["rewrite", "--must=0..", "--sweet"] ["β¦β§"]
it "prints to target file" $
withStdin "[[ ]]" $
withTempFile "targetXXXXXX.tmp" $ \(path, h) -> do
hClose h
testCLISucceeded ["rewrite", "--sweet", printf "--target=%s" path] []
content <- readFile path
content `shouldBe` "β¦β§"
it "modifies file in-place" $
withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
hPutStr h "[[ x -> \"foo\" ]]"
hClose h
testCLISucceeded ["rewrite", rule "simple.yaml", "--in-place", "--sweet", path] []
content <- readFile path
content `shouldBe` "\"bar\":x"
it "skips rewriting with --update when target is newer than source" $
withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
now <- getCurrentTime
setModificationTime src (addUTCTime (-60) now)
setModificationTime tgt now
testCLISucceeded
["rewrite", rule "simple.yaml", "--update", "--sweet", "--target=" ++ tgt, src]
[]
content <- readFile tgt
content `shouldBe` "ORIGINAL"
it "logs the skip reason at debug level when --update finds a newer target" $
withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
now <- getCurrentTime
setModificationTime src (addUTCTime (-60) now)
setModificationTime tgt now
testCLISucceeded
["rewrite", rule "simple.yaml", "--update", "--sweet", "--log-level=DEBUG", "--target=" ++ tgt, src]
["is newer than source", "skipping rewriting (--update)"]
it "logs progress at debug level when printing to --target" $
withStdin "[[ ]]" $
withTempFile "targetXXXXXX.tmp" $ \(path, h) -> do
hClose h
testCLISucceeded
["rewrite", "--sweet", "--log-level=DEBUG", printf "--target=%s" path]
["The option '--target' is specified, printing to", "The command result was saved in"]
it "logs progress at debug level when modifying a file in-place" $
withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
hPutStr h "[[ x -> \"foo\" ]]"
hClose h
testCLISucceeded
["rewrite", rule "simple.yaml", "--in-place", "--sweet", "--log-level=DEBUG", path]
["The option '--in-place' is specified, writing back to", "was modified in-place"]
it "rewrites with --update when source is newer than target" $
withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
now <- getCurrentTime
setModificationTime tgt (addUTCTime (-60) now)
setModificationTime src now
testCLISucceeded
["rewrite", rule "simple.yaml", "--update", "--sweet", "--target=" ++ tgt, src]
[]
content <- readFile tgt
content `shouldBe` "\"bar\":x"
it "rewrites with cycles" $
withStdin "[[ x -> \"x\" ]]" $
testCLISucceeded
["rewrite", "--sweet", rule "infinite.yaml", "--max-depth=1", "--max-cycles=2"]
["\"x_hi_hi\":x"]
it "hides default package" $
withStdin "[[ org -> [[ eolang -> [[ number -> [[]] ]]]], x -> 42 ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--hide=Q.org"]
["42:x"]
it "hides several FQNs" $
withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--hide=Q.org.eolang", "--hide=Q.org.yegor256"]
["β¦ org β¦ β¦β§, x β¦ 42 β§"]
it "shows and hides" $
withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--show=Q.org", "--hide=Q.org.eolang"]
["Ξ¦.y:yegor256:org"]
it "fails on a --show locator that matches nothing" $
withStdin "[[ a -> [[ b -> Q, c -> Q ]], d -> Q ]]" $
testCLIFailed
["rewrite", "--flat", "--show=Q.zzz"]
["[ERROR]:", "Can't find object by locator: 'Ξ¦.zzz'"]
it "shows the whole program with --show=Q" $
withStdin "[[ a -> [[ b -> Q, c -> Q ]], d -> Q ]]" $
testCLISucceeded
["rewrite", "--flat", "--show=Q"]
["β¦ a β¦ β¦ b β¦ Ξ¦, c β¦ Ξ¦ β§, d β¦ Ξ¦ β§"]
it "prints in line with --flat" $
withStdin "[[ x -> 5, y -> \"hey\", z -> [[ w -> [[ ]] ]] ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat"]
["β¦ x β¦ 5, y β¦ \"hey\", z β¦ β¦β§:w β§"]
it "removes unnecessary rho bindings in primitive applications" $
withStdin
( unlines
[ "[["
, " z -> [[ x -> [[ t -> 42 ]].t ]].x,"
, " org -> [[ eolang -> [[ bytes -> [[ data -> ? ]], number -> [[ as-bytes -> ? ]] ]] ]]"
, "]]"
]
)
( testCLISucceeded
["rewrite", "--sweet", "--normalize", "--flat"]
["β¦ z β¦ 42, org β¦ β¦ bytes(data) β¦ β¦β§, number(as-bytes) β¦ β¦β§ β§:eolang β§"]
)
it "reduces log message" $
withStdin "[[ x -> [[ y -> ? ]](y -> 5) ]]" $
testCLISucceeded
["rewrite", "--log-level=debug", "--log-lines=1", "--normalize"]
[ intercalate
"\n"
[ "[DEBUG]: Applied 'copy' (32 nodes -> 27 nodes)"
, "---| log is limited by --log-lines=1 option |---"
]
]
it "reports a condition that raised while being evaluated" $
withStdin "[[ x -> [[ y -> β
]] ]]" $
testCLISucceeded
["rewrite", rule "raising-condition.yaml", "--log-level=debug", "--flat"]
[ "raised and was treated as not met: user error (Only data objects and bytes are supported"
, "β¦ x β¦ β¦ y β¦ β
β§ β§"
]
it "canonizes expression" $
withStdin "[[ x -> [[ y -> [[ L> Func ]].q, z -> Q.x(a -> [[ w -> [[ L> Atom ]], L> Hello ]]) ]], L> Package ]]" $
testCLISucceeded
["rewrite", "--canonize", "--sweet", "--flat"]
["β¦ x β¦ β¦ y β¦ Fn1:Ξ».q, z β¦ Ξ¦.x( a β¦ β¦ w β¦ Fn2:Ξ», Ξ» β€ Fn3 β§ ) β§, Ξ» β€ Package β§"]
it "rewrites by locator" $
withStdin "[[ ex -> [[ x -> [[ y -> 5 ]].y ]], abc -> [[ x -> ? ]](x -> 5) ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--locator=Q.ex", "--normalize"]
["β¦ ex β¦ 5:x, abc β¦ β
:x( x β¦ 5 ) β§"]
it "returns original expression on --breakpoint" $
withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--normalize", "--breakpoint=stop", "--log-level=debug"]
[ "Applied 'copy' (22 nodes -> 17 nodes)"
, "Rule 'stop' is a breakpoint, dropping down all the previous rewritings..."
, "β¦ x β¦ β
, y β¦ x β§( x β¦ 42-:Ξ ).y"
]
it "finishes under --depth-sensitive when the only match left would not change the term" $
withTempFileContent "phino-fixpoint.yaml" "name: fix\npattern: '[[ x -> !e1, !B1 ]]'\nresult: '[[ x -> Q, !B1 ]]'\n" $ \fix ->
withStdin "[[ x -> $ ]]" $
testCLISucceeded ["rewrite", "--rule=" ++ fix, "--max-depth=1", "--depth-sensitive", "--flat"] ["β¦ x β¦ Ξ¦ β§"]
it "keeps the rewritten expression when the --breakpoint rule fired" $
withStdin "β¦ a β¦ β¦ b β¦ Ξ¦ β§.b β§" $
testCLISucceeded
["rewrite", "--flat", "--normalize", "--breakpoint=dot"]
["β¦ a β¦ Ξ¦( Ο β¦ β¦ b β¦ Ξ¦ β§ ) β§"]
describe "morph --focus under --locator" $ do
it "finds the same object for the steps and for the answer" $
withStdin "β¦ t β¦ β¦ a β¦ β¦ Ξ β€ 01- β§ β§, a β¦ β¦ Ξ β€ 02- β§ β§" $ do
(out, _) <- withStdout (runCLI ["morph", "--locator=Q.t", "--focus=Q.a", "--flat", "--sequence"])
filter (not . null) (lines out) `shouldSatisfy` all (== "β¦ Ξ β€ 02- β§")
it "prints the answer when --focus names the object at --locator" $
withStdin "β¦ t β¦ β¦ a β¦ β¦ Ξ β€ 01- β§ β§ β§" $
testCLISucceeded ["morph", "--locator=Q.t", "--focus=Q.t", "--flat", "--sequence"] ["β¦ a β¦ β¦ Ξ β€ 01- β§ β§"]
it "fails on a --focus it cannot find before it prints any step" $
withStdin "β¦ t β¦ β¦ a β¦ β¦ Ξ β€ 01- β§ β§ β§" $ do
(out, _) <- withStdout (try (runCLI ["morph", "--locator=Q.t", "--focus=Q.nope", "--flat", "--sequence"]) :: IO (Either ExitCode ()))
out `shouldNotContain` "β¦ t β¦"
it "fails on a --hide locator that matches nothing, as --show does" $
withStdin "[[ x -> Q.y ]]" $
testCLIFailed ["rewrite", "--hide=Q.nope"] ["Can't find object by locator: 'Ξ¦.nope'"]
describe "dataize" $ do
it "prints help" $
testCLISucceeded ["dataize", "--help"] ["Dataize the π-expression"]
it "names every block of a --symbolic entry in its help" $
testCLISucceeded ["dataize", "--help"] ["\"dataize\"", "\"morph\"", "\"rewrite\"", "\"symbolize\"", "\"join\""]
it "dataizes simple expression" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize"] ["01-"]
it "accepts --seed flag" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--seed=7"] ["01-"]
it "fails to dataize an empty object, which dataizes the terminator β₯" $
withStdin "[[ ]]" $
testCLIFailed ["dataize"] ["terminator β₯"]
it "fails with negative --max-steps" $
withStdin "[[ D> 01- ]]" $
testCLIFailed ["dataize", "--max-steps=-1"] ["--max-steps must be positive"]
it "fails on --max-steps instead of dataizing forever" $
loopingLambdas $ \endless ->
withStdin "β¦ @ β¦ β¦ Ξ» β€ L_loop β§ β§" $
testCLIFailed
["dataize", "--symbolic=" ++ endless, "--max-steps=40"]
["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]
it "parks --max-steps on a residual with --partial" $
loopingLambdas $ \endless ->
withStdin "β¦ @ β¦ β¦ Ξ» β€ L_loop β§ β§" $
testCLISucceeded
["dataize", "--symbolic=" ++ endless, "--max-steps=40", "--partial", "--flat", "--hide-rho"]
["β¦ Ξ» β€ L_loop β§"]
it "fails on --max-firings before --max-steps is spent" $
loopingLambdas $ \endless ->
withStdin "β¦ @ β¦ β¦ Ξ» β€ L_loop β§ β§" $
testCLIFailed
["dataize", "--symbolic=" ++ endless, "--max-steps=400", "--max-firings=5"]
["[ERROR]: Evaluation did not finish before reaching the limit of firings: --max-firings=5"]
describe "--acyclic=proven" $ do
let circling = "β¦ cyc β¦ β¦ x β¦ β
, Ο β¦ Ξ¦.cyc( ΞΎ.x ) β§, t β¦ Ξ¦.cyc( β¦β§ ) β§"
it "spends the whole budget and fails on the limit without the flag" $
withStdin circling $
testCLIFailed
["dataize", "--locator=Q.t", "--max-steps=40"]
["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]
it "names the term it came back to with the flag" $
withStdin circling $
testCLIFailed
["dataize", "--locator=Q.t", "--acyclic=proven", "--max-steps=4000"]
["[ERROR]: Reduction entered a formation it is already inside:"]
it "prints the residue and exits successfully with --partial" $
withStdin circling $
testCLISucceeded
["dataize", "--locator=Q.t", "--acyclic=proven", "--partial", "--max-steps=4000", "--flat", "--hide-rho"]
["Ξ¦.cyc( Ξ±0 β¦ β¦β§ )"]
it "writes the cut to the protocol where the formation would have opened" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin circling $
testCLISucceeded
["dataize", "--locator=Q.t", "--acyclic=proven", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"]
[]
records <- readProtocol path
lines records
`shouldBe` [ "π»(Ξ¦.t)"
, " applied(π.0.1) := Ξ¦.cyc( x β¦ β¦β§ ) # π(Ξ¦.t)"
, " formation(π.0.1) # π»(Ξ¦.t)"
, " applied(π.0.2) := Ξ¦.cyc( x β¦ β¦β§ ) # π(Ξ¦.t)"
, " looped(π.0.2) # π»(Ξ¦.t), proven"
]
it "writes the cut to the XML protocol with the formation in an element of its own" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin circling $
testCLISucceeded
["dataize", "--locator=Q.t", "--acyclic=proven", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"]
[]
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize at=\"Ξ¦.t\">"
, " <applied meta=\"π.0.1\" by=\"morph\" at=\"Ξ¦.t\" of=\"Ξ¦.cyc\"><attr name=\"x\">β¦β§</attr></applied>"
, " <formation at=\"Ξ¦.t\" term=\"π.0.1\">"
, " <applied meta=\"π.0.2\" by=\"morph\" at=\"Ξ¦.t\" of=\"Ξ¦.cyc\"><attr name=\"x\">β¦β§</attr></applied>"
, " <looped by=\"dataize\" match=\"proven\" at=\"Ξ¦.t\"><e>π.0.2</e></looped>"
, " </formation>"
, "</dataize>"
]
it "writes a plausible cut to the protocol as plausible" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin circling $
testCLISucceeded
["dataize", "--locator=Q.t", "--acyclic=plausible", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"]
[]
records <- readProtocol path
lines records `shouldContain` [" looped(π.0.2) # π»(Ξ¦.t), plausible"]
it "refuses the flag without a mode" $
withStdin "β¦ t β¦ β¦ Ξ β€ 01-02 β§ β§" $
testCLIFailed ["dataize", "--locator=Q.t", "--acyclic"] ["The option `--acyclic` expects an argument"]
it "refuses a mode it does not know" $
withStdin "β¦ t β¦ β¦ Ξ β€ 01-02 β§ β§" $
testCLIFailed ["dataize", "--locator=Q.t", "--acyclic=sure"] ["The value 'sure' can't be used for '--acyclic' option"]
it "answers a terminating program the same way with the flag" $
withStdin "β¦ t β¦ β¦ Ξ β€ 01-02 β§ β§" $
testCLISucceeded ["dataize", "--locator=Q.t", "--acyclic=proven"] ["01-02"]
it "dataizes with --sequence" $
withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $
testCLISucceeded
["dataize", "--sequence", "--output=latex", "--flat", "--sweet"]
[ intercalate
"\n"
[ "\\begin{phiquation}"
, "[[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ \\phiContextualize"
, " \\phiContextualize [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| \\phiNormalize[\\nameref{r:copy}]"
, " \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] : |x| . |x| \\phiNormalize[\\nameref{r:dot}]"
, " \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ D> |01-|, |y| -> [[]] ]] : |x| ) \\phiNormalize[\\nameref{r:skip}]"
, " \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] \\phiDataize[\\nameref{r:delta}]"
, " \\phiDataize |01-|{.}"
, "\\end{phiquation}"
, "01-"
]
]
it "keeps the delta step in --sequence under --quiet" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded
["dataize", "--sequence", "--quiet", "--output=latex", "--flat", "--sweet"]
[ intercalate
"\n"
[ "|01-| : D \\phiDataize[\\nameref{r:delta}]"
, " \\phiDataize |01-|{.}"
, "\\end{phiquation}"
]
]
it "ends the phi --sequence at the bare data" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded
["dataize", "--sequence", "--quiet", "--flat", "--sweet"]
["01-:Ξ\n01-"]
it "focuses a compressed sequence whose meet replaces a step root" $
withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus -> [[ ^ -> ?, x -> ?, L> L_number_plus ]] ]] ]]" $
testCLISucceeded
["dataize", symbolic, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--hide=Q.bytes", "--hide=Q.number", "--locator=Q.@", "--focus=Q.@", "--meet-length=5", "--meet-popularity=1"]
["\\phinoMeet{dataization:1}{ [[ @ -> |c| . |plus| ( 32 ), |c| -> 25 ]] } \\phiContextualize"]
it "compresses a canonized whole-expression sequence into a meet" $
withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus -> [[ ^ -> ?, x -> ?, L> L_number_plus ]] ]] ]]" $
testCLISucceeded
["dataize", symbolic, "--output=latex", "--sweet", "--nonumber", "--compress", "--canonize", "--meet-prefix=dataization", "--sequence", "--flat", "--quiet", "--meet-length=5", "--meet-popularity=1"]
["\\phinoMeet{dataization:1}"]
it "canonizes the residue it prints with --partial" $
withStdin "[[ @ -> [[ L> Foo ]] ]]" $
testCLISucceeded ["dataize", "--partial", "--canonize", "--flat", "--sweet"] ["Fn1:Ξ»"]
it "dataizes with --locator" $
withStdin "[[ ex -> [[ @ -> Q.x ]], x -> [[ D> 42- ]] ]]" $
testCLISucceeded ["dataize", "--locator=Q.ex"] ["42-"]
it "does not print bytes with --quiet" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--quiet"] []
describe "--abridged" $ do
let wide = "β¦ t β¦ β¦ Ο β¦ β¦ Ξ β€ 01-02 β§, anfang β¦ ΞΎ.schluss, mitte β¦ ΞΎ.anfang, schluss β¦ ΞΎ.mitte, rand β¦ ΞΎ.schluss β§ β§"
it "folds a long formation in the text protocol" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin wide $
testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
lines records `shouldContain` [" formation(β¦ Ο β¦ 01-02:Ξ, +4 β§) # π»(Ξ¦.t)"]
it "folds a long formation in the XML protocol" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin wide $
testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
lines records `shouldContain` [" <formation at=\"Ξ¦.t\" term=\"β¦ Ο β¦ 01-02:Ξ, +4 β§\">"]
forM_
[ ("textXXXXXX.txt", " πΏ1.1 := 01-02-..(8b)..-0B-0C # π»(ΞΎ.arg)")
, ("XMLXXXXXX.xml", " <bind meta=\"πΏ1.1\">01-02-..(8b)..-0B-0C</bind>")
]
( \(template, line) ->
it ("cuts a long datum a firing came down to under --abridged-data, as " ++ line) $
withTempFile template $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_outer\n dataize:\n πΏ1: ΞΎ.arg\n π: β¦ Ξ» β€ π β§\n") $ \outer ->
withStdin "β¦ x β¦ β¦ arg β¦ β¦ Ξ β€ 01-02-03-04-05-06-07-08-09-0A-0B-0C β§, Ξ» β€ L_outer β§ β§" $
testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--abridged-data", "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
lines records `shouldContain` [line]
)
forM_
[ ("textXXXXXX.txt", " πΏ1.1 := 30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46 # π»(ΞΎ.arg)")
, ("XMLXXXXXX.xml", " <bind meta=\"πΏ1.1\">30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46</bind>")
]
( \(template, line) ->
it ("keeps a long datum a firing came down to whole without --abridged-data, as " ++ line) $
withTempFile template $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_hex\n dataize:\n πΏ1: ΞΎ.arg\n π: β¦ Ξ» β€ π β§\n") $ \hex ->
withStdin "β¦ x β¦ β¦ arg β¦ β¦ Ξ β€ 30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46 β§, Ξ» β€ L_hex β§ β§" $
testCLISucceeded ["dataize", "--symbolic=" ++ hex, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
lines records `shouldContain` [line]
)
it "folds a long formation under the width given as the value" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin wide $
testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged=64", "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
lines records `shouldContain` [" formation(β¦ Ο β¦ 01-02:Ξ, +4 β§) # π»(Ξ¦.t)"]
it "keeps a formation whole under a width it fits in" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin wide $
testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--abridged=200", "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
lines records `shouldContain` [" formation(β¦ Ο β¦ 01-02:Ξ, anfang β¦ schluss, mitte β¦ anfang, schluss β¦ mitte, rand β¦ schluss β§) # π»(Ξ¦.t)"]
it "refuses a width that is not a number" $
withStdin wide $
testCLIFailed ["dataize", "--locator=Q.t", "--protocol=breit.txt", "--abridged=breit"] ["cannot parse value `breit'"]
it "leaves the printed result whole" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin wide $
testCLISucceeded ["morph", "--locator=Q.t", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--flat"] ["anfang β¦ schluss, mitte β¦ anfang"]
it "refuses the flag without a protocol" $
withStdin wide $
testCLIFailed ["dataize", "--locator=Q.t", "--abridged"] ["The option --abridged requires --protocol"]
it "refuses to cut the data in dataize without --abridged" $
withStdin wide $
testCLIFailed ["dataize", "--locator=Q.t", "--protocol=daten.txt", "--abridged-data"] ["The option --abridged-data requires --abridged"]
it "refuses to cut the data in morph without --abridged" $
withStdin wide $
testCLIFailed ["morph", "--locator=Q.t", "--protocol=daten.xml", "--abridged-data"] ["The option --abridged-data requires --abridged"]
describe "--protocol" $ do
let sum' = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
chained = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]"
nested = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6.plus(7)) ]]"
mixed = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]], times(^, x) -> [[ L> L_number_times ]] ]], @ -> 5.plus(6).times(7) ]]"
it "opens the protocol with the run it is the protocol of" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readProtocol path
records `shouldBe` "π»(Ξ¦)\n"
it "closes the protocol with its msec on the third line from the end" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
(lines records !! (length (lines records) - 3)) `shouldSatisfy` isPrefixOf "msec("
it "closes the protocol with the firings it counted" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
lines records `shouldContain` ["firings(1)"]
it "closes the protocol with its fps on the last line" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
last (lines records) `shouldSatisfy` isPrefixOf "fps("
it "closes the protocol with zero firings when the run fires nothing" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
lines records `shouldContain` ["firings(0)"]
it "writes one line per operand and one per answer of a firing" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6 ) β§) # π»(Ξ¦)"
, " applied(π.0.1) := 5 # π(Ξ¦)"
, " applied(π.0.2) := π.0.1.plus( x β¦ 6 ) # π(Ξ¦)"
, " πΌ(L_number_plus) # π»(Ξ¦)"
, " applied(π.1.1) := 5 # π(Ξ¦.aπ΅0)"
, " formation(π.1.1) # π»(Ξ¦.aπ΅0)"
, " applied(π.1.2) := Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅0)"
, " formation(π.1.2) # π»(Ξ¦.aπ΅0)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.1.3) := 6 # π(Ξ¦.aπ΅1)"
, " formation(π.1.3) # π»(Ξ¦.aπ΅1)"
, " applied(π.1.4) := Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅1)"
, " formation(π.1.4) # π»(Ξ¦.aπ΅1)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.5 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π"
, " applied(π.1.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦)"
, " π.1.7 := π.1.6 # π(π.1.5)"
, " formation(π.1.6) # π»(Ξ¦)"
]
it "numbers the firings of one entry apart and names the symbol between them" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin chained $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6 ).plus( 7 ) β§) # π»(Ξ¦)"
, " applied(π.0.1) := 5 # π(Ξ¦)"
, " applied(π.0.2) := π.0.1.plus( x β¦ 6 ) # π(Ξ¦)"
, " πΌ(L_number_plus) # π(Ξ¦)"
, " applied(π.1.1) := 5 # π(Ξ¦.aπ΅0)"
, " formation(π.1.1) # π»(Ξ¦.aπ΅0)"
, " applied(π.1.2) := Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅0)"
, " formation(π.1.2) # π»(Ξ¦.aπ΅0)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.1.3) := 6 # π(Ξ¦.aπ΅1)"
, " formation(π.1.3) # π»(Ξ¦.aπ΅1)"
, " applied(π.1.4) := Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅1)"
, " formation(π.1.4) # π»(Ξ¦.aπ΅1)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.5 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π"
, " applied(π.1.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦)"
, " π.1.7 := π.1.6 # π(π.1.5)"
, " applied(π.0.3) := π.1.6.plus( x β¦ 7 ) # π(Ξ¦)"
, " πΌ(L_number_plus) # π»(Ξ¦)"
, " applied(π.2.1) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦.aπ΅2)"
, " formation(π.2.1) # π»(Ξ¦.aπ΅2)"
, " πΏ1.2 := π»(π1:Ξ») # π»(ΞΎ.Ο)"
, " applied(π.2.2) := 7 # π(Ξ¦.aπ΅3)"
, " formation(π.2.2) # π»(Ξ¦.aπ΅3)"
, " applied(π.2.3) := Ξ¦.bytes( Ο β¦ 40-1C-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅3)"
, " formation(π.2.3) # π»(Ξ¦.aπ΅3)"
, " πΏ2.2 := 40-1C-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.2.4 := Ξ¦.number( Ο β¦ π2:Ξ» ) # π"
, " applied(π.2.5) := Ξ¦.number( Ο β¦ π2:Ξ» ) # π(Ξ¦)"
, " π.2.6 := π.2.5 # π(π.2.4)"
, " formation(π.2.5) # π»(Ξ¦)"
]
it "numbers the firings of different entries apart" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin mixed $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ», times(x) β¦ L_number_times:Ξ» β§, Ο β¦ 5.plus( 6 ).times( 7 ) β§) # π»(Ξ¦)"
, " applied(π.0.1) := 5 # π(Ξ¦)"
, " applied(π.0.2) := π.0.1.plus( x β¦ 6 ) # π(Ξ¦)"
, " πΌ(L_number_plus) # π(Ξ¦)"
, " applied(π.1.1) := 5 # π(Ξ¦.aπ΅0)"
, " formation(π.1.1) # π»(Ξ¦.aπ΅0)"
, " applied(π.1.2) := Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅0)"
, " formation(π.1.2) # π»(Ξ¦.aπ΅0)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.1.3) := 6 # π(Ξ¦.aπ΅1)"
, " formation(π.1.3) # π»(Ξ¦.aπ΅1)"
, " applied(π.1.4) := Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅1)"
, " formation(π.1.4) # π»(Ξ¦.aπ΅1)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.5 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π"
, " applied(π.1.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦)"
, " π.1.7 := π.1.6 # π(π.1.5)"
, " applied(π.0.3) := π.1.6.times( x β¦ 7 ) # π(Ξ¦)"
, " πΌ(L_number_times) # π»(Ξ¦)"
, " applied(π.2.1) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦.aπ΅2)"
, " formation(π.2.1) # π»(Ξ¦.aπ΅2)"
, " πΏ1.2 := π»(π1:Ξ») # π»(ΞΎ.Ο)"
, " applied(π.2.2) := 7 # π(Ξ¦.aπ΅3)"
, " formation(π.2.2) # π»(Ξ¦.aπ΅3)"
, " applied(π.2.3) := Ξ¦.bytes( Ο β¦ 40-1C-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅3)"
, " formation(π.2.3) # π»(Ξ¦.aπ΅3)"
, " πΏ2.2 := 40-1C-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.2.4 := Ξ¦.number( Ο β¦ π2:Ξ» ) # π"
, " applied(π.2.5) := Ξ¦.number( Ο β¦ π2:Ξ» ) # π(Ξ¦)"
, " π.2.6 := π.2.5 # π(π.2.4)"
, " formation(π.2.5) # π»(Ξ¦)"
]
it "nests the firing an operand of another firing brought down" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin nested $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6.plus( 7 ) ) β§) # π»(Ξ¦)"
, " applied(π.0.1) := 5 # π(Ξ¦)"
, " applied(π.0.2) := π.0.1.plus( x β¦ 6.plus( 7 ) ) # π(Ξ¦)"
, " πΌ(L_number_plus) # π»(Ξ¦)"
, " applied(π.1.1) := 5 # π(Ξ¦.aπ΅0)"
, " formation(π.1.1) # π»(Ξ¦.aπ΅0)"
, " applied(π.1.2) := Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅0)"
, " formation(π.1.2) # π»(Ξ¦.aπ΅0)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.1.3) := 6 # π(Ξ¦.aπ΅1)"
, " applied(π.1.4) := π.1.3.plus( x β¦ 7 ) # π(Ξ¦.aπ΅1)"
, " πΌ(L_number_plus) # π»(Ξ¦.aπ΅1)"
, " applied(π.2.1) := 6 # π(Ξ¦.aπ΅2)"
, " formation(π.2.1) # π»(Ξ¦.aπ΅2)"
, " applied(π.2.2) := Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅2)"
, " formation(π.2.2) # π»(Ξ¦.aπ΅2)"
, " πΏ1.2 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.2.3) := 7 # π(Ξ¦.aπ΅3)"
, " formation(π.2.3) # π»(Ξ¦.aπ΅3)"
, " applied(π.2.4) := Ξ¦.bytes( Ο β¦ 40-1C-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅3)"
, " formation(π.2.4) # π»(Ξ¦.aπ΅3)"
, " πΏ2.2 := 40-1C-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.2.5 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π"
, " applied(π.2.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦.aπ΅1)"
, " π.2.7 := π.2.6 # π(π.2.5)"
, " formation(π.2.6) # π»(Ξ¦.aπ΅1)"
, " πΏ2.1 := π»(π1:Ξ») # π»(ΞΎ.x)"
, " π.1.5 := Ξ¦.number( Ο β¦ π2:Ξ» ) # π"
, " applied(π.1.6) := Ξ¦.number( Ο β¦ π2:Ξ» ) # π(Ξ¦)"
, " π.1.7 := π.1.6 # π(π.1.5)"
, " formation(π.1.6) # π»(Ξ¦)"
]
it "writes what is known about every symbol a 'symbolize' line minted" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_stand\n morph:\n π1: $.x\n symbolize:\n π2: π1\n π: β¦ z β¦ π2 β§\n") $ \stands ->
withStdin "β¦ y β¦ β¦ x β¦ β¦ Ξ β€ 01- β§, Ξ» β€ L_stand β§.z β§" $
testCLISucceeded ["morph", "--symbolic=" ++ stands, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "π(Ξ¦.y)"
, " πΌ(L_stand) # π(Ξ¦.y)"
, " π1.1 := 01-:Ξ # π(ΞΎ.x)"
, " π»(π1:Ξ») == 01-"
, " π2.1 := π1:Ξ» # π1"
, " π.1.1 := π1:Ξ»:z # π"
, " π.1.2 := π1:Ξ»:z # π(π.1.1)"
]
it "writes a deferred copy as a call of the object of the world it was made of" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin "β¦ box(x) β¦ β¦ Ο β¦ x.next β§, y β¦ Ξ¦.box( x β¦ β¦ Ξ» β€ π1 β§ ) β§" $
testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" deferred(π2) := Ξ¦.box( x β¦ π1:Ξ» ) # π(Ξ¦.y)"]
it "writes a deferred copy as it stands when the world declares no object it was made of" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin "β¦ wrap(v) β¦ β¦β§, y β¦ Ξ¦.wrap( v β¦ β¦ b(x) β¦ β¦ Ο β¦ x.next β§ β§ ).v.b( x β¦ β¦ Ξ» β€ π1 β§ ) β§" $
testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" applied(π.0.2) := β¦ x β¦ β
, Ο β¦ x.next β§( x β¦ π1:Ξ» ) # π(Ξ¦.y)", " deferred(π2) := π.0.2 # π(Ξ¦.y)"]
it "writes the symbol a cut answers a copy with" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n π1: $.x\n π: π1\n") $ \loops ->
withStdin "β¦ box(n) β¦ β¦ Ο β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ ΞΎ.n ) ) β§, loop(x) β¦ L_loop:Ξ», y β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ β¦ Ξ β€ 01- β§ ) ) β§" $
testCLISucceeded ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=proven", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" applied(π.1.3) := Ξ¦.loop( x β¦ π.1.2 ) # π(Ξ¦.aπ΅0.Ο)", " looped(π.1.3) := π1 # π(Ξ¦.aπ΅0.Ο), proven"]
it "writes a told stall to the XML protocol" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_outer\n dataize:\n πΏ1: ΞΎ.arg\n π: β¦ Ξ» β€ π β§\n") $ \outer ->
withStdin "β¦ x β¦ β¦ arg β¦ β¦ Ξ» β€ L_none β§, Ξ» β€ L_outer β§, y β¦ β¦ arg β¦ β¦ Ξ» β€ L_none β§, Ξ» β€ L_outer β§ β§" $
testCLISucceeded ["morph", "--symbolic=" ++ outer, "--deep", "--partial", "--acyclic=plausible", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <stall Ξ»=\"L_none\"/>"]
it "writes a stuck firing to the XML protocol" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_outer\n dataize:\n πΏ1: ΞΎ.arg\n π: β¦ Ξ» β€ π β§\n") $ \outer ->
withStdin "β¦ x β¦ β¦ arg β¦ β¦ Ξ» β€ L_absent β§, Ξ» β€ L_outer β§ β§" $
testCLISucceeded ["morph", "--symbolic=" ++ outer, "--deep", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <unfinished Ξ»=\"L_absent\"/>"]
it "writes a starved step budget to the XML protocol" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_outer\n dataize:\n πΏ1: ΞΎ.arg\n π: β¦ Ξ» β€ π β§\n") $ \outer ->
withStdin "β¦ x β¦ β¦ arg β¦ β¦ Ο β¦ β¦ Ο β¦ β¦ Ξ β€ 07- β§ β§ β§, Ξ» β€ L_outer β§ β§" $
testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--max-steps=3", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho", "--flat"] []
records <- readProtocol path
lines records `shouldContain` [" <starved limit=\"3\" by=\"dataize\" at=\"Ξ¦.aπ΅0\"/>"]
forM_
[("XMLXXXXXX.xml", "<spent limit=\"5\" by="), ("textXXXXXX.txt", "spent(5) # ")]
( \(template, record) ->
it ("writes a spent firing budget to the protocol as " ++ record) $
withTempFile template $ \(path, stream) -> do
hClose stream
loopingLambdas $ \endless ->
withStdin "β¦ @ β¦ β¦ Ξ» β€ L_loop β§ β§" $
testCLIFailed ["dataize", "--symbolic=" ++ endless, "--max-steps=400", "--max-firings=5", "--protocol=" ++ path] ["--max-firings=5"]
records <- readProtocol path
any (record `isInfixOf`) (lines records) `shouldBe` True
)
it "keeps the lines of a run that fails" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]], nope -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> 5.plus(6).nope ]]" $
testCLIFailed
["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"]
["No entry of --symbolic answers the Ξ» function 'L_number_nope'"]
records <- readProtocol path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ», nope β¦ L_number_nope:Ξ» β§, Ο β¦ 5.plus( 6 ).nope β§) # π»(Ξ¦)"
, " applied(π.0.1) := 5 # π(Ξ¦)"
, " applied(π.0.2) := π.0.1.plus( x β¦ 6 ) # π(Ξ¦)"
, " πΌ(L_number_plus) # π(Ξ¦)"
, " applied(π.1.1) := 5 # π(Ξ¦.aπ΅0)"
, " formation(π.1.1) # π»(Ξ¦.aπ΅0)"
, " applied(π.1.2) := Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅0)"
, " formation(π.1.2) # π»(Ξ¦.aπ΅0)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.1.3) := 6 # π(Ξ¦.aπ΅1)"
, " formation(π.1.3) # π»(Ξ¦.aπ΅1)"
, " applied(π.1.4) := Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅1)"
, " formation(π.1.4) # π»(Ξ¦.aπ΅1)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.5 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π"
, " applied(π.1.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦)"
, " π.1.7 := π.1.6 # π(π.1.5)"
, " unanswered(L_number_nope) # π»(L_number_nope:Ξ»)"
]
it "truncates the lines left over from the previous run" $
withTempFileContent "protocolXXXXXX.txt" "πΌ(L_number_gt)\n" $ \path -> do
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readProtocol path
records `shouldBe` "π»(Ξ¦)\n"
it "writes the lines in π even with --output=xmir" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--output=xmir", "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
records `shouldEndWith` " applied(π.1.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦)\n π.1.7 := π.1.6 # π(π.1.5)\n formation(π.1.6) # π»(Ξ¦)\n"
describe "as XML" $ do
it "writes the document when the file is named .xml" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize at=\"Ξ¦\">"
, " <formation at=\"Ξ¦\" term=\"β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6 ) β§\">"
, " <applied meta=\"π.0.1\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <applied meta=\"π.0.2\" by=\"morph\" at=\"Ξ¦\" of=\"π.0.1.plus\"><attr name=\"x\">6</attr></applied>"
, " <evaluate Ξ»=\"L_number_plus\" by=\"dataize\" at=\"Ξ¦\">"
, " <applied meta=\"π.1.1\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.1\">"
, " <applied meta=\"π.1.2\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-14-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.2\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ1.1\">40-14-00-00-00-00-00-00</bind>"
, " <applied meta=\"π.1.3\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.3\">"
, " <applied meta=\"π.1.4\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-18-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.4\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ2.1\">40-18-00-00-00-00-00-00</bind>"
, " <minted symbol=\"π1\">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>"
, " <built meta=\"π.1.5\">Ξ¦.number( Ο β¦ π1:Ξ» )</built>"
, " <applied meta=\"π.1.6\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">π1</attr></applied>"
, " <answer meta=\"π.1.7\">π.1.6</answer>"
, " </evaluate>"
, " <formation at=\"Ξ¦\" term=\"π.1.6\">"
, " </formation>"
, " </formation>"
, "</dataize>"
]
it "nests the judgment one level inside a '<protocol>' root" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
take 4 (lines records)
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<protocol>"
, " <dataize at=\"Ξ¦\">"
, " </dataize>"
]
it "closes the '<protocol>' root with its msec" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
(lines records !! 4) `shouldSatisfy` isPrefixOf " <msec>"
it "closes the '<protocol>' root with its firings" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
lines records `shouldContain` [" <firings>0</firings>"]
it "closes the '<protocol>' root with its fps, then '</protocol>' itself" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readUtf8 path
drop 6 (lines records) `shouldBe` [" <fps>0</fps>", "</protocol>"]
it "nests what a Ο body fires inside the formation element it was boxed from" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
filter (not . isInfixOf "<applied ") (lines records)
`shouldContain` [ " <formation at=\"Ξ¦\" term=\"β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6 ) β§\">"
, " <evaluate Ξ»=\"L_number_plus\" by=\"dataize\" at=\"Ξ¦\">"
]
it "closes the document even when nothing fires" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize at=\"Ξ¦\">"
, "</dataize>"
]
it "tells a manufactured datum from data by the name of the element" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin chained $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize at=\"Ξ¦\">"
, " <formation at=\"Ξ¦\" term=\"β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6 ).plus( 7 ) β§\">"
, " <applied meta=\"π.0.1\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <applied meta=\"π.0.2\" by=\"morph\" at=\"Ξ¦\" of=\"π.0.1.plus\"><attr name=\"x\">6</attr></applied>"
, " <evaluate Ξ»=\"L_number_plus\" by=\"morph\" at=\"Ξ¦\">"
, " <applied meta=\"π.1.1\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.1\">"
, " <applied meta=\"π.1.2\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-14-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.2\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ1.1\">40-14-00-00-00-00-00-00</bind>"
, " <applied meta=\"π.1.3\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.3\">"
, " <applied meta=\"π.1.4\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-18-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.4\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ2.1\">40-18-00-00-00-00-00-00</bind>"
, " <minted symbol=\"π1\">40-14-00-00-00-00-00-00 40-18-00-00-00-00-00-00</minted>"
, " <built meta=\"π.1.5\">Ξ¦.number( Ο β¦ π1:Ξ» )</built>"
, " <applied meta=\"π.1.6\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">π1</attr></applied>"
, " <answer meta=\"π.1.7\">π.1.6</answer>"
, " </evaluate>"
, " <applied meta=\"π.0.3\" by=\"morph\" at=\"Ξ¦\" of=\"π.1.6.plus\"><attr name=\"x\">7</attr></applied>"
, " <evaluate Ξ»=\"L_number_plus\" by=\"dataize\" at=\"Ξ¦\">"
, " <applied meta=\"π.2.1\" by=\"morph\" at=\"Ξ¦.aπ΅2\" of=\"Ξ¦.number\"><attr name=\"Ο\">π1</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅2\" term=\"π.2.1\">"
, " </formation>"
, " <dataize meta=\"πΏ1.2\">π1:Ξ»</dataize>"
, " <applied meta=\"π.2.2\" by=\"morph\" at=\"Ξ¦.aπ΅3\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-1C-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅3\" term=\"π.2.2\">"
, " <applied meta=\"π.2.3\" by=\"morph\" at=\"Ξ¦.aπ΅3\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-1C-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅3\" term=\"π.2.3\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ2.2\">40-1C-00-00-00-00-00-00</bind>"
, " <minted symbol=\"π2\">π1 40-1C-00-00-00-00-00-00</minted>"
, " <built meta=\"π.2.4\">Ξ¦.number( Ο β¦ π2:Ξ» )</built>"
, " <applied meta=\"π.2.5\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">π2</attr></applied>"
, " <answer meta=\"π.2.6\">π.2.5</answer>"
, " </evaluate>"
, " <formation at=\"Ξ¦\" term=\"π.2.5\">"
, " </formation>"
, " </formation>"
, "</dataize>"
]
it "writes what is known about a symbol as an element of its own" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_stand\n morph:\n π1: $.x\n symbolize:\n π2: π1\n π: β¦ z β¦ π2 β§\n") $ \stands ->
withStdin "β¦ y β¦ β¦ x β¦ β¦ Ξ β€ 01- β§, Ξ» β€ L_stand β§.z β§" $
testCLISucceeded ["morph", "--symbolic=" ++ stands, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_stand\" by=\"morph\" at=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">01-:Ξ</bind>"
, " <known symbol=\"π1\">01-</known>"
, " <bind meta=\"π2.1\">π1:Ξ»</bind>"
, " <built meta=\"π.1.1\">π1:Ξ»:z</built>"
, " <answer meta=\"π.1.2\">π1:Ξ»:z</answer>"
, " </evaluate>"
, "</morph>"
]
it "writes what a 'join' line knows as an element of its own" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_fork\n morph:\n π1: $.a\n π2: $.b\n join:\n π3: [π1, π2]\n π: π3\n") $ \forks ->
withStdin "β¦ y β¦ β¦ a β¦ β¦ Ο β¦ β¦ Ξ» β€ π1 β§ β§, b β¦ β¦ Ο β¦ β¦ Ξ» β€ π2 β§ β§, Ξ» β€ L_fork β§.Ο β§" $
testCLISucceeded ["morph", "--symbolic=" ++ forks, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_fork\" by=\"morph\" at=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">π1:Ξ»:Ο</bind>"
, " <bind meta=\"π2.1\">π2:Ξ»:Ο</bind>"
, " <joined symbol=\"π3\">π1 π2</joined>"
, " <bind meta=\"π3.1\">π3:Ξ»:Ο</bind>"
, " <built meta=\"π.1.1\">π3:Ξ»:Ο</built>"
, " <answer meta=\"π.1.2\">π3:Ξ»:Ο</answer>"
, " </evaluate>"
, "</morph>"
]
it "writes on which side of the condition a fork raises" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_fork\n dataize:\n πΏ1: $.c\n morph:\n π1: $.a\n π2: $.b\n join:\n π3: [π1, π2]\n π: π3\n") $ \forks ->
withStdin "β¦ y β¦ β¦ c β¦ β¦ Ξ» β€ π1 β§, a β¦ β¦ Ο β¦ β¦ Ξ» β€ π2 β§ β§, b β¦ β₯, Ξ» β€ L_fork β§.Ο β§" $
testCLISucceeded ["morph", "--symbolic=" ++ forks, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_fork\" by=\"morph\" at=\"Ξ¦.y\">"
, " <dataize meta=\"πΏ1.1\">π1:Ξ»</dataize>"
, " <bind meta=\"π1.1\">π2:Ξ»:Ο</bind>"
, " <bind meta=\"π2.1\">β₯</bind>"
, " <terminate symbol=\"π1\" branch=\"right\"/>"
, " <bind meta=\"π3.1\">π2:Ξ»:Ο</bind>"
, " <built meta=\"π.1.1\">π2:Ξ»:Ο</built>"
, " <answer meta=\"π.1.2\">π2:Ξ»:Ο</answer>"
, " </evaluate>"
, "</morph>"
]
it "writes one 'minted' element per symbol the answer asked for" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_pair\n morph:\n π1: $.x\n π: β¦ left β¦ β¦ Ξ» β€ π β§, right β¦ β¦ Ξ» β€ π β§ β§\n") $ \pairs ->
withStdin "β¦ y β¦ β¦ x β¦ β¦ Ξ β€ 01- β§, Ξ» β€ L_pair β§.left β§" $
testCLISucceeded ["morph", "--symbolic=" ++ pairs, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_pair\" by=\"morph\" at=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">01-:Ξ</bind>"
, " <minted symbol=\"π1\"/>"
, " <minted symbol=\"π2\"/>"
, " <built meta=\"π.1.1\">β¦ left β¦ π1:Ξ», right β¦ π2:Ξ» β§</built>"
, " <answer meta=\"π.1.2\">β¦ left β¦ π1:Ξ», right β¦ π2:Ξ» β§</answer>"
, " </evaluate>"
, "</morph>"
]
it "writes the copy a deferred symbol stands for as an element of its own" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "β¦ box(x) β¦ β¦ Ο β¦ x.next β§, y β¦ Ξ¦.box( x β¦ β¦ Ξ» β€ π1 β§ ) β§" $
testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.y\">"
, " <applied meta=\"π.0.1\" by=\"morph\" at=\"Ξ¦.y\" of=\"Ξ¦.box\"><attr name=\"x\">π1</attr></applied>"
, " <deferred symbol=\"π2\" by=\"morph\" at=\"Ξ¦.y\" of=\"Ξ¦.box\"><with><attr name=\"x\">π1</attr></with><e>π.0.1</e></deferred>"
, "</morph>"
]
it "names the object a deferred copy was made of through the formation its Ο holds" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "β¦ joined(items) β¦ β¦ Ο β¦ step( tup β¦ items ), step(Ο, tup) β¦ β¦ Ο β¦ tup.next β§ β§, y β¦ Ξ¦.joined( items β¦ β¦ Ξ» β€ π1 β§ ).Ο β§" $
testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <deferred symbol=\"π2\" by=\"morph\" at=\"Ξ¦.y\" of=\"Ξ¦.joined.step\"><with><attr name=\"tup\">π1</attr></with><e>π.0.2</e></deferred>"]
it "names the object a deferred copy was made of after the walk wrote an answer into its Ο" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_dataized\n dataize:\n πΏ1: $.target\n π: Ξ¦.bytes( Ο β¦ β¦ Ξ» β€ π β§ )\n") $ \dataized ->
withStdin "β¦ bytes(Ο) β¦ β¦β§, dataized(target) β¦ L_dataized:Ξ», joined(items) β¦ β¦ Ο β¦ step( tup β¦ items, s β¦ sep ), sep β¦ Ξ¦.dataized( target β¦ items ), step(Ο, tup, s) β¦ β¦ Ο β¦ tup.next β§ β§, y β¦ Ξ¦.joined( items β¦ β¦ Ξ» β€ π1 β§ ).Ο β§" $
testCLISucceeded ["morph", "--deep", "--symbolic=" ++ dataized, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <deferred symbol=\"π3\" by=\"morph\" at=\"Ξ¦.y\" of=\"Ξ¦.joined.step\"><with><attr name=\"tup\">π1</attr><attr name=\"s\">π2</attr></with><e>π.0.4</e></deferred>"]
it "writes a question mark for an argument of a deferred copy that is no bare symbol" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "β¦ box(x, w) β¦ β¦ Ο β¦ x.next β§, y β¦ Ξ¦.box( x β¦ β¦ Ξ» β€ π1 β§, w β¦ β¦ z β¦ Ξ¦ β§ ) β§" $
testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <deferred symbol=\"π2\" by=\"morph\" at=\"Ξ¦.y\" of=\"Ξ¦.box\"><with><attr name=\"x\">π1</attr><attr name=\"w\">?</attr></with><e>π.0.2</e></deferred>"]
it "writes the object a deferred copy was made of whatever --abridged says" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "β¦ joined(items) β¦ β¦ Ο β¦ step( tup β¦ items ), step(Ο, tup) β¦ β¦ Ο β¦ tup.next β§ β§, y β¦ Ξ¦.joined( items β¦ β¦ Ξ» β€ π1 β§ ).Ο β§" $
testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--abridged=20", "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <deferred symbol=\"π2\" by=\"morph\" at=\"Ξ¦.y\" of=\"Ξ¦.joined.step\"><with><attr name=\"tup\">π1</attr></with><e>π.0.2</e></deferred>"]
it "writes no object for a deferred copy of a formation the world does not declare" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "β¦ wrap(v) β¦ β¦β§, y β¦ Ξ¦.wrap( v β¦ β¦ b(x) β¦ β¦ Ο β¦ x.next β§ β§ ).v.b( x β¦ β¦ Ξ» β€ π1 β§ ) β§" $
testCLISucceeded ["morph", "--deep", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <applied meta=\"π.0.2\" by=\"morph\" at=\"Ξ¦.y\" of=\"β¦ x β¦ β
, Ο β¦ x.next β§\"><attr name=\"x\">π1</attr></applied>", " <deferred symbol=\"π2\" by=\"morph\" at=\"Ξ¦.y\"><e>π.0.2</e></deferred>"]
it "writes the copy a cut answers as a call of the object it was made of" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n π1: $.x\n π: π1\n") $ \loops ->
withStdin "β¦ num(Ο) β¦ β¦β§, box(n) β¦ β¦ Ο β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ ΞΎ.n ) ) β§, loop(x) β¦ L_loop:Ξ», y β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ Ξ¦.num( Ο β¦ β¦ Ξ» β€ π1 β§ ) ) ) β§" $
testCLISucceeded ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=plausible", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records `shouldContain` [" <looped symbol=\"π2\" by=\"morph\" match=\"plausible\" at=\"Ξ¦.aπ΅0.Ο\" of=\"Ξ¦.box\"><with><attr name=\"n\">π1</attr></with><e>π.0.1</e></looped>"]
it "writes no 'minted' element for a firing minting nothing" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_keep\n morph:\n π1: $.x\n π: β¦ z β¦ π1 β§\n") $ \keeps ->
withStdin "β¦ y β¦ β¦ x β¦ β¦ Ξ β€ 01- β§, Ξ» β€ L_keep β§.z β§" $
testCLISucceeded ["morph", "--symbolic=" ++ keeps, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_keep\" by=\"morph\" at=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">01-:Ξ</bind>"
, " <built meta=\"π.1.1\">01-:Ξ:z</built>"
, " <answer meta=\"π.1.2\">01-:Ξ:z</answer>"
, " </evaluate>"
, "</morph>"
]
it "nests a firing an operand took inside the firing that asked" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin nested $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize at=\"Ξ¦\">"
, " <formation at=\"Ξ¦\" term=\"β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ plus(x) β¦ L_number_plus:Ξ» β§, Ο β¦ 5.plus( 6.plus( 7 ) ) β§\">"
, " <applied meta=\"π.0.1\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <applied meta=\"π.0.2\" by=\"morph\" at=\"Ξ¦\" of=\"π.0.1.plus\"><attr name=\"x\">6.plus( 7 )</attr></applied>"
, " <evaluate Ξ»=\"L_number_plus\" by=\"dataize\" at=\"Ξ¦\">"
, " <applied meta=\"π.1.1\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.1\">"
, " <applied meta=\"π.1.2\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-14-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.2\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ1.1\">40-14-00-00-00-00-00-00</bind>"
, " <applied meta=\"π.1.3\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <applied meta=\"π.1.4\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"π.1.3.plus\"><attr name=\"x\">7</attr></applied>"
, " <evaluate Ξ»=\"L_number_plus\" by=\"dataize\" at=\"Ξ¦.aπ΅1\">"
, " <applied meta=\"π.2.1\" by=\"morph\" at=\"Ξ¦.aπ΅2\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅2\" term=\"π.2.1\">"
, " <applied meta=\"π.2.2\" by=\"morph\" at=\"Ξ¦.aπ΅2\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-18-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅2\" term=\"π.2.2\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ1.2\">40-18-00-00-00-00-00-00</bind>"
, " <applied meta=\"π.2.3\" by=\"morph\" at=\"Ξ¦.aπ΅3\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-1C-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅3\" term=\"π.2.3\">"
, " <applied meta=\"π.2.4\" by=\"morph\" at=\"Ξ¦.aπ΅3\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-1C-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅3\" term=\"π.2.4\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ2.2\">40-1C-00-00-00-00-00-00</bind>"
, " <minted symbol=\"π1\">40-18-00-00-00-00-00-00 40-1C-00-00-00-00-00-00</minted>"
, " <built meta=\"π.2.5\">Ξ¦.number( Ο β¦ π1:Ξ» )</built>"
, " <applied meta=\"π.2.6\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.number\"><attr name=\"Ο\">π1</attr></applied>"
, " <answer meta=\"π.2.7\">π.2.6</answer>"
, " </evaluate>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.2.6\">"
, " </formation>"
, " <dataize meta=\"πΏ2.1\">π1:Ξ»</dataize>"
, " <minted symbol=\"π2\">40-14-00-00-00-00-00-00 π1</minted>"
, " <built meta=\"π.1.5\">Ξ¦.number( Ο β¦ π2:Ξ» )</built>"
, " <applied meta=\"π.1.6\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">π2</attr></applied>"
, " <answer meta=\"π.1.7\">π.1.6</answer>"
, " </evaluate>"
, " <formation at=\"Ξ¦\" term=\"π.1.6\">"
, " </formation>"
, " </formation>"
, "</dataize>"
]
it "records a Ξ» function no entry answers as a childless element" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ times(^, x) -> [[ L> L_number_times ]], nope -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]" $
testCLISucceeded ["dataize", symbolic, "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize at=\"Ξ¦\">"
, " <formation at=\"Ξ¦\" term=\"β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ times(x) β¦ L_number_times:Ξ», nope β¦ L_number_nope:Ξ» β§, Ο β¦ 2.times( 3 ).nope β§\">"
, " <applied meta=\"π.0.1\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-00-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <applied meta=\"π.0.2\" by=\"morph\" at=\"Ξ¦\" of=\"π.0.1.times\"><attr name=\"x\">3</attr></applied>"
, " <evaluate Ξ»=\"L_number_times\" by=\"morph\" at=\"Ξ¦\">"
, " <applied meta=\"π.1.1\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-00-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.1\">"
, " <applied meta=\"π.1.2\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-00-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.2\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ1.1\">40-00-00-00-00-00-00-00</bind>"
, " <applied meta=\"π.1.3\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ 40-08-00-00-00-00-00-00:Ξ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.3\">"
, " <applied meta=\"π.1.4\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">40-08-00-00-00-00-00-00:Ξ</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.4\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ2.1\">40-08-00-00-00-00-00-00</bind>"
, " <minted symbol=\"π1\">40-00-00-00-00-00-00-00 40-08-00-00-00-00-00-00</minted>"
, " <built meta=\"π.1.5\">Ξ¦.number( Ο β¦ π1:Ξ» )</built>"
, " <applied meta=\"π.1.6\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">π1</attr></applied>"
, " <answer meta=\"π.1.7\">π.1.6</answer>"
, " </evaluate>"
, " <unanswered Ξ»=\"L_number_nope\" by=\"dataize\">L_number_nope:Ξ»</unanswered>"
, " </formation>"
, "</dataize>"
]
it "names the root after the judgment a morphing ran" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ x -> [[ L> L_number_nope ]].foo ]]" $
testCLISucceeded ["morph", "--locator=Q.x", "--partial", "--protocol=" ++ path, "--quiet"] []
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.x\">"
, " <unanswered Ξ»=\"L_number_nope\" by=\"morph\">β¦ Ξ» β€ L_number_nope β§</unanswered>"
, "</morph>"
]
it "closes the document even when the run fails" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ times(^, x) -> [[ L> L_number_times ]], nope -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]" $
testCLIFailed ["dataize", symbolic, "--protocol=" ++ path] ["No entry of --symbolic answers"]
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize at=\"Ξ¦\">"
, " <formation at=\"Ξ¦\" term=\"β¦ bytes β¦ β¦ Ο β¦ β
β§, number β¦ β¦ Ο β¦ β
, times β¦ β¦ Ο β¦ β
, x β¦ β
, Ξ» β€ L_number_times β§, nope β¦ β¦ Ο β¦ β
, Ξ» β€ L_number_nope β§ β§, Ο β¦ Ξ¦.number( Ο β¦ Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 40-00-00-00-00-00-00-00 β§ ) ).times( Ξ±0 β¦ Ξ¦.number( Ο β¦ Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 40-08-00-00-00-00-00-00 β§ ) ) ).nope β§\">"
, " <applied meta=\"π.0.1\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 40-00-00-00-00-00-00-00 β§ )</attr></applied>"
, " <applied meta=\"π.0.2\" by=\"morph\" at=\"Ξ¦\" of=\"π.0.1.times\"><attr name=\"x\">Ξ¦.number( Ο β¦ Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 40-08-00-00-00-00-00-00 β§ ) )</attr></applied>"
, " <evaluate Ξ»=\"L_number_times\" by=\"morph\" at=\"Ξ¦\">"
, " <applied meta=\"π.1.1\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 40-00-00-00-00-00-00-00 β§ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.1\">"
, " <applied meta=\"π.1.2\" by=\"morph\" at=\"Ξ¦.aπ΅0\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">β¦ Ξ β€ 40-00-00-00-00-00-00-00 β§</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅0\" term=\"π.1.2\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ1.1\">40-00-00-00-00-00-00-00</bind>"
, " <applied meta=\"π.1.3\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.number\"><attr name=\"Ο\">Ξ¦.bytes( Ο β¦ β¦ Ξ β€ 40-08-00-00-00-00-00-00 β§ )</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.3\">"
, " <applied meta=\"π.1.4\" by=\"morph\" at=\"Ξ¦.aπ΅1\" of=\"Ξ¦.bytes\"><attr name=\"Ο\">β¦ Ξ β€ 40-08-00-00-00-00-00-00 β§</attr></applied>"
, " <formation at=\"Ξ¦.aπ΅1\" term=\"π.1.4\">"
, " </formation>"
, " </formation>"
, " <bind meta=\"πΏ2.1\">40-08-00-00-00-00-00-00</bind>"
, " <minted symbol=\"π1\">40-00-00-00-00-00-00-00 40-08-00-00-00-00-00-00</minted>"
, " <built meta=\"π.1.5\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ )</built>"
, " <applied meta=\"π.1.6\" by=\"morph\" at=\"Ξ¦\" of=\"Ξ¦.number\"><attr name=\"Ο\">π1</attr></applied>"
, " <answer meta=\"π.1.7\">π.1.6</answer>"
, " </evaluate>"
, " <unanswered Ξ»=\"L_number_nope\" by=\"dataize\">β¦ Ο β¦ π.1.6, Ξ» β€ L_number_nope β§</unanswered>"
, " </formation>"
, "</dataize>"
]
it "writes the terminator as the term a meta was bound to" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- Ξ»: L_pick\n morph:\n π1: ΞΎ.absent\n π: β¦ Ξ» β€ π β§\n") $ \picks ->
withStdin "[[ x -> [[ here -> [[ ]], L> L_pick ]].foo ]]" $
testCLIFailed ["morph", "--symbolic=" ++ picks, "--locator=Q.x", "--protocol=" ++ path, "--quiet", "--hide-rho"] ["No entry of --symbolic answers the Ξ» function 'π1'"]
records <- readProtocol path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph at=\"Ξ¦.x\">"
, " <evaluate Ξ»=\"L_pick\" by=\"morph\" at=\"Ξ¦.x\">"
, " <bind meta=\"π1.1\">β₯</bind>"
, " <minted symbol=\"π1\"/>"
, " <built meta=\"π.1.1\">β¦ Ξ» β€ π1 β§</built>"
, " <answer meta=\"π.1.2\">β¦ Ξ» β€ π1 β§</answer>"
, " </evaluate>"
, " <unanswered Ξ»=\"π1\" by=\"morph\">β¦ Ξ» β€ π1 β§</unanswered>"
, "</morph>"
]
it "keeps writing text when the file is named anything else" $
withTempFile "protocolXXXXXX.xmir" $ \(path, stream) -> do
hClose stream
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
take 1 (lines records) `shouldBe` ["π»(Ξ¦)"]
describe "--partial" $ do
let stuck = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ times(^, x) -> [[ L> L_number_times ]], nope -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> 2.times(3).nope ]]"
dispatched = "[[ foo -> [[ bar -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> Q.foo.bar ]]"
wrapped = "[[ app -> [[ foo -> [[ bar -> [[ ^ -> ?, L> L_number_nope ]] ]], @ -> Q.app.foo.bar ]] ]]"
it "fails on a Ξ» function that cannot fire without the flag" $
withStdin stuck $
testCLIFailed
["dataize", symbolic, "--sweet", "--hide-rho"]
["No entry of --symbolic answers the Ξ» function 'L_number_nope'"]
it "prints the residue with the stuck application intact and exits successfully" $
withStdin stuck $
testCLISucceeded
["dataize", symbolic, "--partial", "--sweet", "--hide-rho"]
["L_number_nope:Ξ»"]
it "keeps what was evaluated before the stuck site in the residue" $
withStdin stuck $
testCLISucceeded
["dataize", symbolic, "--partial", "--sweet"]
["Ο β¦ π1:Ξ»"]
it "records every firing before the stuck site in --protocol" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin stuck $
testCLISucceeded ["dataize", symbolic, "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " formation(β¦ bytes(Ο) β¦ β¦β§, number(Ο) β¦ β¦ times(x) β¦ L_number_times:Ξ», nope β¦ L_number_nope:Ξ» β§, Ο β¦ 2.times( 3 ).nope β§) # π»(Ξ¦)"
, " applied(π.0.1) := 2 # π(Ξ¦)"
, " applied(π.0.2) := π.0.1.times( x β¦ 3 ) # π(Ξ¦)"
, " πΌ(L_number_times) # π(Ξ¦)"
, " applied(π.1.1) := 2 # π(Ξ¦.aπ΅0)"
, " formation(π.1.1) # π»(Ξ¦.aπ΅0)"
, " applied(π.1.2) := Ξ¦.bytes( Ο β¦ 40-00-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅0)"
, " formation(π.1.2) # π»(Ξ¦.aπ΅0)"
, " πΏ1.1 := 40-00-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.1.3) := 3 # π(Ξ¦.aπ΅1)"
, " formation(π.1.3) # π»(Ξ¦.aπ΅1)"
, " applied(π.1.4) := Ξ¦.bytes( Ο β¦ 40-08-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅1)"
, " formation(π.1.4) # π»(Ξ¦.aπ΅1)"
, " πΏ2.1 := 40-08-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.5 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π"
, " applied(π.1.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦)"
, " π.1.7 := π.1.6 # π(π.1.5)"
, " unanswered(L_number_nope) # π»(L_number_nope:Ξ»)"
]
it "still prints bytes when nothing gets stuck" $
withStdin "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $
testCLISucceeded ["dataize", symbolic, "--partial"] ["40-45-00-00-00-00-00-00"]
it "prints the residual at --locator, which XMIR has no top level for" $
withStdin wrapped $
testCLIFailed
["dataize", symbolic, "--partial", "--locator=Q.app", "--output=xmir", "--hide-rho"]
["[ERROR]:", "its top level must be a single binding"]
it "prints the residual at --locator, not the whole program" $
withStdin wrapped $ do
(out, _) <- withStdout (runCLI ["dataize", symbolic, "--partial", "--locator=Q.app", "--hide-rho", "--flat"])
lines out `shouldBe` ["β¦ Ξ» β€ L_number_nope β§"]
it "cannot print a residual of several top bindings as XMIR" $
withStdin dispatched $
testCLIFailed
["dataize", symbolic, "--partial", "--output=xmir"]
["[ERROR]:", "its top level must be a single binding"]
it "prints the chain of steps ending in the residue with --sequence" $
withStdin stuck $
testCLISucceeded
["dataize", symbolic, "--partial", "--sequence", "--sweet", "--hide-rho", "--flat"]
["2.times( 3 ).nope", "L_number_nope:Ξ»"]
it "still stops on the terminator β₯, since a wrong operand is not a stuck Ξ» function" $
withStdin "[[ ]]" $
testCLIFailed ["dataize", "--partial"] ["terminator β₯"]
describe "--symbolic" $ do
let sum' = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
it "fires the Ξ» function an entry of the file answers" $
withStdin sum' $
testCLISucceeded ["dataize", symbolic] ["40-45-00-00-00-00-00-00"]
it "reports the progress of the run with --log-level=INFO" $
withStdin sum' $
testCLISucceeded ["dataize", symbolic, "--log-level=INFO", "--quiet"] ["[INFO]: Entered "]
it "gets stuck on every Ξ» function when it is not given" $
withStdin sum' $
testCLIFailed ["dataize"] ["No entry of --symbolic answers the Ξ» function 'L_number_plus'"]
it "fails when the file is not there" $
withStdin sum' $
testCLIFailed ["dataize", "--symbolic=no-such-file.yaml"] ["no-such-file.yaml"]
it "fails on a file that carries no entries at all, before dataizing anything" $
withTempFileContent "symbolicXXXXXX.yaml" "nope: true\n" $ \path ->
withStdin sum' $
testCLIFailed ["dataize", "--symbolic=" ++ path] ["cannot be read"]
describe "--inside" $ do
let universe = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> [[ D> 01- ]] ]]"
it "dataizes an expression the input does not contain" $
withStdin universe $
testCLISucceeded ["dataize", symbolic, "--inside=5.plus( 6 )"] ["40-45-00-00-00-00-00-00"]
it "normalizes what it is handed before dataizing it" $
withStdin universe $
testCLISucceeded ["dataize", "--inside=[[ x -> [[ D> 2A- ]] ]].x"] ["2A-"]
it "morphs inside the universe just as it dataizes inside it" $
withStdin universe $
testCLISucceeded ["morph", symbolic, "--inside=5.plus( 6 )", "--sweet", "--hide-rho", "--flat"] ["β¦ x β¦ 6, Ξ» β€ L_number_plus β§"]
it "opens the text protocol before the objects it made while aiming" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin universe $
testCLISucceeded ["morph", symbolic, "--inside=5.plus( 6 )", "--protocol=" ++ path, "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
takeWhile (/= '(') (concat (take 1 (lines records))) `shouldBe` "π"
it "opens the XML protocol before the objects it made while aiming" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withStdin universe $
testCLISucceeded ["dataize", symbolic, "--inside=5.plus( 6 )", "--protocol=" ++ path, "--sweet", "--hide-rho", "--quiet"] []
records <- readProtocol path
take 1 (lines records) `shouldBe` ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>"]
it "cannot be used together with --locator" $
withStdin universe $
testCLIFailed ["dataize", "--inside=Q.@", "--locator=Q.@"] ["--inside and --locator cannot be used together"]
it "fails when the input expression is not a formation" $
withStdin "Q.x" $
testCLIFailed ["dataize", "--inside=Q.x"] ["--inside requires the input expression to be a formation"]
describe "fails" $ do
it "with --output != latex and --nonumber" $
withStdin "" $
testCLIFailed
["dataize", "--nonumber", "--output=xmir"]
["The --nonumber option can stay together with --output=latex only"]
it "with --omit-listing and --output != xmir" $
withStdin "" $
testCLIFailed
["dataize", "--omit-listing", "--output=phi"]
["--omit-listing"]
it "with --omit-comments and --output != xmir" $
withStdin "" $
testCLIFailed
["dataize", "--omit-comments", "--output=phi"]
["--omit-comments"]
it "with --expression and --output != latex" $
withStdin "" $
testCLIFailed
["dataize", "--expression=foo", "--output=phi"]
["--expression option can stay together with --output=latex only"]
it "with --label and --output != latex" $
withStdin "" $
testCLIFailed
["dataize", "--label=foo", "--output=phi"]
["--label option can stay together with --output=latex only"]
it "with wrong --hide option" $
withStdin "" $
testCLIFailed
["dataize", "--hide=Q.x(Q.y)"]
["[ERROR]: Invalid set of arguments: Only dispatch expression", "but given: Ξ¦.x( Ξ¦.y )"]
it "with wrong --show option" $
withStdin "" $
testCLIFailed
["dataize", "--show=Q.x(Q.y)"]
["[ERROR]:", "Only dispatch expression started with Ξ¦ (or Q) can be used in --show"]
it "with wrong --locator option" $
withStdin "" $
testCLIFailed
["dataize", "--locator=Q.x(Q.y)"]
["[ERROR]:", "Only dispatch expression started with Ξ¦ (or Q) can be used in --locator"]
it "with wrong --focus option" $
withStdin "" $
testCLIFailed
["dataize", "--focus=Q.x(Q.y)"]
["[ERROR]:", "Only dispatch expression started with Ξ¦ (or Q) can be used in --focus"]
it "accepts --depth-sensitive" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["dataize", "--depth-sensitive"] ["01-"]
describe "morph" $ do
let chained = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6).plus(7) ]]"
it "prints help" $
testCLISucceeded ["morph", "--help"] ["Morph the π-expression"]
it "hands the top formation back untouched under the default locator" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["morph", "--flat", "--hide-rho"] ["β¦ Ξ β€ 01- β§"]
it "stops at the bare saturated Ξ»-formation" $
withStdin chained $
testCLISucceeded
["morph", symbolic, "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]
["β¦ x β¦ 7, Ξ» β€ L_number_plus β§"]
it "leaves to dataize the firing that takes the same term to bytes" $
withStdin chained $
testCLISucceeded ["dataize", symbolic] ["40-45-00-00-00-00-00-00"]
it "morphs the subterm --locator aims at" $
withStdin "[[ ex -> Q.x, x -> [[ D> 42- ]] ]]" $
testCLISucceeded ["morph", "--locator=Q.ex", "--flat", "--hide-rho"] ["β¦ Ξ β€ 42- β§"]
it "canonizes the answer it prints" $
withStdin "[[ x -> [[ L> Foo ]], y -> [[ L> Bar ]] ]]" $
testCLISucceeded ["morph", "--canonize", "--flat", "--sweet"] ["β¦ x β¦ Fn1:Ξ», y β¦ Fn2:Ξ» β§"]
it "hides a binding of the answer it prints" $
withStdin "[[ x -> [[ L> Foo ]], y -> [[ L> Bar ]] ]]" $
testCLISucceeded ["morph", "--hide=Q.x", "--flat", "--sweet"] ["Bar:Ξ»:y"]
it "shows only one binding of the answer it prints" $
withStdin "[[ x -> [[ L> Foo ]], y -> [[ L> Bar ]] ]]" $
testCLISucceeded ["morph", "--show=Q.x", "--flat", "--sweet"] ["Foo:Ξ»:x"]
it "prints β₯ instead of failing the run" $
withStdin "[[ x -> $ ]]" $
testCLISucceeded ["morph", "--locator=Q.x"] ["β₯"]
it "fails to dataize what it morphs to β₯" $
withStdin "[[ x -> $ ]]" $
testCLIFailed ["dataize", "--locator=Q.x"] ["terminator β₯"]
it "prints the chain of morphing steps with --sequence" $
withStdin chained $
testCLISucceeded
["morph", symbolic, "--locator=Q.@", "--sequence", "--headers", "--sweet", "--hide-rho", "--flat"]
[ "Rule 'maa'"
, "Rule 'alpha'"
, "Rule 'copy'"
, "Rule 'mf'"
, "β¦ x β¦ 7, Ξ» β€ L_number_plus β§"
]
it "writes every step of a LaTeX --sequence with the arrow of its judgment" $
withStdin "[[ q -> [[ ]], k -> Q.q ]]" $
testCLISucceeded
["morph", "--locator=Q.k", "--sequence", "--output=latex", "--flat", "--sweet", "--quiet"]
[ intercalate
"\n"
[ "\\begin{phiquation}"
, "[[ |q| -> [[]], |k| -> Q . |q| ]] \\phiMorph[\\nameref{r:md}]"
, " \\phiMorph [[ |q| -> [[]], |k| -> [[ |q| -> [[]], |k| -> Q . |q| ]] . |q| ]] \\phiNormalize[\\nameref{r:dot}]"
, " \\phiNormalize [[ |q| -> [[]], |k| -> [[]] ( \\phiTerminal{\\rho} -> Q ) ]] \\phiNormalize[\\nameref{r:skip}]"
, " \\phiNormalize [[ |q| -> [[]], |k| -> [[]] ]] \\phiMorph[\\nameref{r:mf}]"
, " \\phiMorph [[ |q| -> [[]], |k| -> [[]] ]]{.}"
, "\\end{phiquation}"
]
]
it "does not print the result with --quiet" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["morph", "--quiet"] []
it "records the Ξ» functions it fires with --protocol" $
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin chained $
testCLISucceeded ["morph", symbolic, "--locator=Q.@", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readProtocol path
lines records
`shouldBe` [ "π(Ξ¦.Ο)"
, " applied(π.0.1) := 5 # π(Ξ¦.Ο)"
, " applied(π.0.2) := π.0.1.plus( x β¦ 6 ) # π(Ξ¦.Ο)"
, " πΌ(L_number_plus) # π(Ξ¦.Ο)"
, " applied(π.1.1) := 5 # π(Ξ¦.aπ΅0)"
, " formation(π.1.1) # π»(Ξ¦.aπ΅0)"
, " applied(π.1.2) := Ξ¦.bytes( Ο β¦ 40-14-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅0)"
, " formation(π.1.2) # π»(Ξ¦.aπ΅0)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " applied(π.1.3) := 6 # π(Ξ¦.aπ΅1)"
, " formation(π.1.3) # π»(Ξ¦.aπ΅1)"
, " applied(π.1.4) := Ξ¦.bytes( Ο β¦ 40-18-00-00-00-00-00-00:Ξ ) # π(Ξ¦.aπ΅1)"
, " formation(π.1.4) # π»(Ξ¦.aπ΅1)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.5 := Ξ¦.number( Ο β¦ π1:Ξ» ) # π"
, " applied(π.1.6) := Ξ¦.number( Ο β¦ π1:Ξ» ) # π(Ξ¦.Ο)"
, " π.1.7 := π.1.6 # π(π.1.5)"
, " applied(π.0.3) := π.1.6.plus( x β¦ 7 ) # π(Ξ¦.Ο)"
]
it "saves morphing steps to dir with --steps-dir" $
withTempDirectory "phino-steps-morph" $ \dir ->
withStdin chained $ do
testCLISucceeded
["morph", symbolic, "--locator=Q.@", "--steps-dir=" ++ dir, "--sweet", "--hide-rho", "--flat"]
["β¦ x β¦ 7, Ξ» β€ L_number_plus β§"]
steps <- sort <$> listDirectory dir
steps `shouldBe` map (\n -> printf "%05d.phi" (n :: Int)) [1 .. length steps]
length steps `shouldSatisfy` (> 0)
it "accepts --seed, --shuffle and --depth-sensitive" $
withStdin "[[ D> 01- ]]" $
testCLISucceeded ["morph", "--seed=7", "--shuffle", "--depth-sensitive", "--flat", "--hide-rho"] ["β¦ Ξ β€ 01- β§"]
it "returns the Ξ»-formation dataize cannot finish on" $
withStdin "β¦ @ β¦ β¦ Ξ» β€ L_number_div, Ο β¦ β¦ Ξ β€ 40-45-00-00-00-00-00-00 β§, x β¦ β¦ Ξ β€ 40-00-00-00-00-00-00-00 β§ β§ β§" $
testCLISucceeded
["morph", "--locator=Q.@", "--max-steps=40", "--flat", "--hide-rho"]
["β¦ Ξ» β€ L_number_div"]
it "fails once the --max-steps budget is spent" $
withStdin chained $
testCLIFailed
["morph", "--locator=Q.@", "--max-steps=3"]
["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=3"]
describe "--max-firings" $ do
let splitting = withLambdasOf (T.pack "- Ξ»: L_split\n morph:\n π1: Ξ¦.s.foo\n π2: Ξ¦.s.foo\n π: β¦ l β¦ π1, r β¦ π2 β§\n")
split = "β¦ s β¦ β¦ Ξ» β€ L_split β§, x β¦ Ξ¦.s.foo β§"
it "fails with non-positive --max-firings" $
withStdin split $
testCLIFailed ["morph", "--max-firings=0"] ["--max-firings must be positive"]
it "fails once the --max-firings budget is spent on a widening recursion" $
splitting $ \table ->
withStdin split $
testCLIFailed
["morph", "--symbolic=" ++ table, "--locator=Q.x", "--max-firings=64"]
["[ERROR]: Evaluation did not finish before reaching the limit of firings: --max-firings=64"]
it "ends the widening recursion with --partial" $
splitting $ \table ->
withStdin split $
testCLISucceeded
["morph", "--symbolic=" ++ table, "--locator=Q.x", "--max-firings=64", "--partial", "--flat", "--hide-rho", "--sweet"]
["β₯"]
it "parks the spent --max-firings budget with --deep and --partial" $
splitting $ \table ->
withStdin split $
testCLISucceeded
["morph", "--symbolic=" ++ table, "--deep", "--max-firings=64", "--partial", "--flat", "--hide-rho", "--sweet"]
["x β¦ Ξ¦.s.foo"]
it "fires no more Ξ» functions than --max-firings allows" $
splitting $ \table ->
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin split $
testCLISucceeded
["morph", "--symbolic=" ++ table, "--deep", "--max-firings=64", "--partial", "--protocol=" ++ path, "--quiet"]
[]
records <- readProtocol path
length (filter (isInfixOf "πΌ(L_split)") (lines records)) `shouldBe` 64
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 β§"
bounded :: Expectation -> Expectation
bounded check = timeout 60000000 check >>= (`shouldBe` Just ())
it "fails with non-positive --max-seconds" $
withStdin rungs $
testCLIFailed ["morph", "--max-seconds=0"] ["--max-seconds must be positive"]
it "fails once the --max-seconds budget is spent" $
ladder $ \table ->
bounded $
withStdin rungs $
testCLIFailed
["morph", "--symbolic=" ++ table, "--locator=Q.x", "--max-seconds=1"]
["[ERROR]: Evaluation did not finish before reaching the limit of seconds: --max-seconds=1"]
it "fails dataize once the --max-seconds budget is spent" $
ladder $ \table ->
bounded $
withStdin rungs $
testCLIFailed
["dataize", "--symbolic=" ++ table, "--locator=Q.x", "--max-seconds=1"]
["[ERROR]: Evaluation did not finish before reaching the limit of seconds: --max-seconds=1"]
forM_ [["--locator=Q.x", "--partial"], ["--deep", "--partial"]] $ \opts ->
it ("fails once the --max-seconds budget is spent with " ++ unwords opts) $
ladder $ \table ->
bounded $
withStdin rungs $
testCLIFailed
(["morph", "--symbolic=" ++ table, "--max-seconds=1"] ++ opts)
["[ERROR]: Evaluation did not finish before reaching the limit of seconds: --max-seconds=1"]
forM_ [["--locator=Q.x"], ["--locator=Q.x", "--partial"], ["--deep", "--partial"], ["--deep", "--partial", "--jobs=4"]] $ \opts ->
it ("writes the timeout as the last line of the protocol with " ++ unwords opts) $
ladder $ \table ->
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
bounded $
withStdin rungs $
testCLIFailed
(["morph", "--symbolic=" ++ table, "--max-seconds=1", "--protocol=" ++ path, "--quiet"] ++ opts)
["--max-seconds=1"]
records <- readProtocol path
dropWhile (== ' ') (last (lines records)) `shouldStartWith` "timeout(1) # π("
it "writes the timeout once to the XML protocol of a deep run" $
ladder $ \table ->
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
bounded $
withStdin rungs $
testCLIFailed
["morph", "--symbolic=" ++ table, "--deep", "--partial", "--max-seconds=1", "--protocol=" ++ path, "--quiet"]
["--max-seconds=1"]
records <- readProtocol path
length (filter (isInfixOf "<timeout limit=\"1\" by=\"morph\" at=\"") (lines records)) `shouldBe` 1
it "closes the XML protocol of a run out of time" $
ladder $ \table ->
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
bounded $
withStdin rungs $
testCLIFailed
["morph", "--symbolic=" ++ table, "--locator=Q.x", "--max-seconds=1", "--protocol=" ++ path, "--quiet"]
["--max-seconds=1"]
document <- X.readFile X.def path
X.nameLocalName (X.elementName (X.documentRoot document)) `shouldBe` T.pack "protocol"
describe "--jobs" $ do
let twins = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], a -> 7.plus( 5.plus( 6 ) ), b -> 7.plus( 5.plus( 6 ) ) ]]"
recorded :: [String] -> IO [String]
recorded extra =
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin twins $
testCLISucceeded (["morph", symbolic, "--deep", "--protocol=" ++ path, "--quiet"] ++ extra) []
lines <$> readProtocol path
untaued :: String -> String
untaued [] = []
untaued text
| "aπ΅" `isPrefixOf` text = "aπ΅" ++ untaued (dropWhile (\ch -> isDigit ch || ch == '-') (drop 2 text))
untaued (ch : rest) = ch : untaued rest
it "prints the answer one walk over the bindings prints" $
withStdin twins $
testCLISucceeded
["morph", symbolic, "--deep", "--acyclic=proven", "--jobs=3", "--flat", "--hide-rho", "--sweet"]
["a β¦ β¦ Ο β¦ π2:Ξ», plus(x) β¦ L_number_plus:Ξ» β§, b β¦ β¦ Ο β¦ π4:Ξ», plus(x) β¦ L_number_plus:Ξ» β§"]
it "writes the firings of a binding after those of the bindings before it" $
recorded ["--jobs=2"]
>>= (`shouldBe` ["# π(Ξ¦.a)", "# π(Ξ¦.a)", "# π(Ξ¦.b)", "# π(Ξ¦.b)"]) . map (dropWhile (/= '#')) . filter (isPrefixOf " πΌ(")
it "numbers the symbols of the protocol the way the answer numbers them" $
recorded ["--jobs=2"] >>= (`shouldSatisfy` elem " π.4.3 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π4 β§ ) # π")
it "names what a binding mints after the binding" $
recorded ["--jobs=2"] >>= (`shouldSatisfy` any (isInfixOf "# π»(Ξ¦.aπ΅4-0)"))
it "writes the protocol one walk writes, the names a binding mints apart" $ do
one <- recorded ["--jobs=1"]
many <- recorded ["--jobs=4"]
map untaued many `shouldBe` map untaued one
it "writes the same protocol however many workers it is given" $ do
few <- recorded ["--jobs=2"]
many <- recorded ["--jobs=5"]
many `shouldBe` few
it "keeps a memo of its own for every binding under plausible" $
withStdin twins $
testCLISucceeded
["morph", symbolic, "--deep", "--acyclic=plausible", "--jobs=2", "--flat", "--hide-rho", "--sweet"]
["b β¦ β¦ Ο β¦ π4:Ξ», plus(x) β¦ L_number_plus:Ξ» β§"]
it "fails with non-positive --jobs" $
withStdin twins $
testCLIFailed ["morph", "--deep", "--jobs=0"] ["--jobs must be positive"]
it "fails with --jobs above one and no --deep" $
withStdin twins $
testCLIFailed ["morph", "--jobs=2"] ["The option --jobs requires --deep, since only the deep walk runs on several workers"]
it "parks the spent budget as a residual with --partial" $
withStdin "β¦ Ο β¦ 5.gt(Ξ¦.nan) β§" $
testCLISucceeded
["morph", "--locator=Q.@", "--max-steps=10", "--partial", "--flat", "--hide-rho", "--sweet"]
["5.gt( Ξ¦.nan )"]
describe "--partial" $ do
let stuck = "[[ @ -> [[ L> Sym_arg_0 ]].foo ]]"
it "fails on a Ξ» function that cannot fire without the flag" $
withStdin stuck $
testCLIFailed ["morph", "--locator=Q.@"] ["No entry of --symbolic answers the Ξ» function 'Sym_arg_0'"]
it "prints the residue with the stuck application intact and exits successfully" $
withStdin stuck $
testCLISucceeded
["morph", "--locator=Q.@", "--partial", "--flat", "--hide-rho"]
["β¦ Ξ» β€ Sym_arg_0 β§.foo"]
describe "--deep" $ do
let program =
"[[ bytes β¦ β¦ Ο β¦ β
β§, \
\number(Ο) -> [[ times(^, x) -> [[ L> L_number_times ]] ]], \
\bar(x) -> [[ L> L_bar ]], \
\demo -> [[ foo -> [[ n -> 3, @ -> Q.bar( $.n.times( 5 ).times( 7 ) ) ]] ]] ]]"
it "answers the formation as it was written without the flag" $
withStdin program $
testCLISucceeded
["morph", symbolic, "--inside=Q.demo.foo", "--sweet", "--hide-rho", "--flat"]
["β¦ n β¦ 3, Ο β¦ Ξ¦.bar( n.times( 5 ).times( 7 ) ) β§"]
it "reduces every binding it can and leaves the rest in place" $
withStdin program $
testCLISucceeded
["morph", symbolic, "--deep", "--inside=Q.demo.foo", "--sweet", "--hide-rho", "--flat"]
["β¦ n β¦ 3, Ο β¦ Ξ¦.bar( β¦ Ο β¦ π2:Ξ», times(x) β¦ L_number_times:Ξ» β§ ) β§"]
it "fires the bare saturated Ξ»-formation mf hands back" $
withStdin chained $
testCLISucceeded
["morph", symbolic, "--deep", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]
["β¦ Ο β¦ π2:Ξ», plus(x) β¦ L_number_plus:Ξ» β§"]
it "keeps the object model intact while it folds the program" $
withStdin program $
testCLISucceeded
["morph", symbolic, "--deep", "--sweet", "--hide-rho", "--flat"]
[ "number(Ο) β¦ β¦ times(x) β¦ L_number_times:Ξ» β§"
, "demo β¦ β¦ n β¦ 3, Ο β¦ Ξ¦.bar( β¦ Ο β¦ π2:Ξ», times(x) β¦ L_number_times:Ξ» β§ ) β§:foo"
]
it "keeps a binding whose spine got stuck with --partial" $
withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $
testCLISucceeded
["morph", "--deep", "--partial", "--sweet", "--hide-rho", "--flat"]
["Sym_arg_0:Ξ».foo:x"]
it "fails on that same spine without --partial" $
withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $
testCLIFailed ["morph", "--deep"] ["No entry of --symbolic answers the Ξ» function 'Sym_arg_0'"]
describe "--acyclic=plausible" $ do
let twins = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(^, x) -> [[ L> L_number_plus ]] ]], a -> 7.plus( 5.plus( 6 ) ), b -> 7.plus( 5.plus( 6 ) ) ]]"
recorded :: String -> IO [String]
recorded mode =
withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do
hClose stream
withStdin twins $
testCLISucceeded
["morph", symbolic, "--deep", "--acyclic=" ++ mode, "--protocol=" ++ path, "--quiet"]
[]
lines <$> readProtocol path
it "charges a formation once per binding spelling it under proven" $
withStdin twins $
testCLIFailed
["morph", symbolic, "--deep", "--acyclic=proven", "--max-firings=3"]
["[ERROR]: Evaluation did not finish before reaching the limit of firings: --max-firings=3"]
it "charges a formation once for the run under plausible" $
withStdin twins $
testCLISucceeded
["morph", symbolic, "--deep", "--acyclic=plausible", "--max-firings=2", "--flat", "--hide-rho", "--sweet"]
["b β¦ β¦ Ο β¦ π2:Ξ», plus(x) β¦ L_number_plus:Ξ» β§"]
it "reduces the operands of a formation once per binding spelling it under proven" $
recorded "proven" >>= (`shouldSatisfy` ((== 4) . length . filter (isInfixOf "πΏ1.")))
it "reduces the operands of a formation once for the run under plausible" $
recorded "plausible" >>= (`shouldSatisfy` ((== 2) . length . filter (isInfixOf "πΏ1.")))
it "writes a recalled firing at its own site under plausible" $
recorded "plausible" >>= (`shouldSatisfy` ((== 4) . length . filter (isInfixOf "πΌ(L_number_plus)")))
it "answers a recalled firing with the line of the first under plausible" $
recorded "plausible" >>= (`shouldContain` [" π.4.2 := π.2.5 # π(π.4.1)"])
it "dataizes to the same datum under plausible" $
withStdin chained $
testCLISucceeded
["dataize", symbolic, "--acyclic=plausible", "--locator=Q.@"]
["40-45-00-00-00-00-00-00"]
describe "--acyclic=proven" $ do
let looping = "β¦ x β¦ β¦ Ξ» β€ L_loop β§.foo β§"
it "spends the whole budget and fails on the limit without the flag" $
loopingLambdas $ \endless ->
withStdin looping $
testCLIFailed
["morph", "--symbolic=" ++ endless, "--locator=Q.x", "--max-steps=40"]
["[ERROR]: Dataization did not finish before reaching the limit of steps: --max-steps=40"]
it "prints the residue 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"]
it "answers a terminating program the same way with the flag" $
withStdin chained $
testCLISucceeded
["morph", symbolic, "--acyclic=proven", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]
["β¦ x β¦ 7, Ξ» β€ L_number_plus β§"]
it "parks the looping binding and keeps walking with --deep" $
loopingLambdas $ \endless ->
withStdin "β¦ x β¦ β¦ Ξ» β€ L_loop, Ο β¦ β
β§.foo, y β¦ β¦ z β¦ β¦β§ β§ β§" $
testCLISucceeded
["morph", "--symbolic=" ++ endless, "--deep", "--acyclic=proven", "--max-steps=4000", "--flat", "--hide-rho"]
["β¦ x β¦ β¦ Ξ» β€ L_loop β§.foo, y β¦ β¦ z β¦ β¦β§ β§ β§"]
it "answers a copy with a fresh symbol once it cuts the Ο of the copy" $
withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n π1: $.x\n π: π1\n") $ \loops ->
withStdin "β¦ box(n) β¦ β¦ Ο β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ ΞΎ.n ) ) β§, loop(x) β¦ L_loop:Ξ», y β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ β¦ Ξ β€ 01- β§ ) ) β§" $
testCLISucceeded
["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=proven", "--locator=Q.y", "--flat", "--hide-rho", "--sweet"]
["π1:Ξ»"]
it "answers a cut copy with the symbol one walk gives it whatever --jobs says" $
withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n π1: $.x\n π: π1\n- Ξ»: L_mint\n π: β¦ Ξ» β€ π β§\n") $ \loops ->
withStdin "β¦ mint β¦ L_mint:Ξ», box(n) β¦ β¦ k β¦ Ξ¦.mint, Ο β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ ΞΎ.n ) ) β§, loop(x) β¦ L_loop:Ξ», y β¦ Ξ¦.loop( x β¦ Ξ¦.box( n β¦ β¦ Ξ β€ 01- β§ ) ) β§" $
testCLISucceeded
["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=proven", "--jobs=2", "--locator=Q.y", "--flat", "--hide-rho", "--sweet"]
["π2:Ξ»"]
describe "fails" $ do
it "with --output=xmir on a top formation of several bindings" $
withStdin "[[ x -> [[ D> 01- ]], y -> [[ D> 02- ]] ]]" $
testCLIFailed
["morph", "--output=xmir"]
["[ERROR]:", "its top level must be a single binding"]
it "with --output != latex and --nonumber" $
withStdin "" $
testCLIFailed
["morph", "--nonumber", "--output=xmir"]
["The --nonumber option can stay together with --output=latex only"]
it "with --show used more than once" $
withStdin "" $
testCLIFailed
["morph", "--show=Q.a", "--show=Q.b"]
["The option --show can be used only once"]
it "with wrong --locator option" $
withStdin "" $
testCLIFailed
["morph", "--locator=Q.x(Q.y)"]
["[ERROR]:", "Only dispatch expression started with Ξ¦ (or Q) can be used in --locator"]
describe "explain" $ do
forM_
["--morph", "--dataize", "--contextualize"]
( \judgment ->
it ("refuses --normalize together with " ++ judgment) $
testCLIFailed ["explain", judgment, "--normalize"] ["The --normalize option cannot be used together with"]
)
it "prints help" $
testCLISucceeded
["explain", "--help"]
["Explain built-in morphing rules", "Explain built-in dataization rules", "Explain built-in contextualization rules"]
it "explains single rule" $ do
latex <- explainPack "test-resources/explain-packs/normalize/copy.yaml"
testCLISucceeded ["explain", "--rule=resources/normalize/copy.yaml"] [latex <> "\n"]
it "explains single rule with a label" $
testCLISucceeded
["explain", rule "labeled.yaml"]
[ unlines
[ "\\phinoNormalizationRule[\\lambda]{copy}"
, " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
, " { [[ B_1, \\tau -> k, B_2 ]] }"
, " { }"
, " { }"
]
]
it "explains multiple rules" $
testCLISucceeded
["explain", "--rule=resources/normalize/copy.yaml", "--rule=resources/normalize/alpha.yaml"]
["\\phinoNormalizationRule{copy}", "\\phinoNormalizationRule{alpha}"]
it "reproduces the same shuffle order for the same --seed" $ do
let args =
[ "explain"
, "--shuffle"
, "--seed=42"
, rule "swap-a.yaml"
, rule "swap-b.yaml"
]
(firstRun, _) <- withStdout (runCLI args)
(secondRun, _) <- withStdout (runCLI args)
firstRun `shouldBe` secondRun
it "accepts --seed flag" $
testCLISucceeded
["explain", "--seed=7", "--normalize"]
["\\phinoNormalizationRule{alpha}"]
forM_
[ ("normalization", "--normalize", "normalize")
, ("morphing", "--morph", "morphing")
, ("dataization", "--dataize", "dataization")
, ("contextualization", "--contextualize", "contextualization")
]
( \(judgment, option, dir) -> it ("explains " <> judgment <> " rules") $ do
packs <- allPathsIn ("test-resources/explain-packs" </> dir)
latex <- mapM explainPack (sort packs)
testCLISucceeded ["explain", option] [unlines latex]
)
it "fails with no rules specified" $
testCLIFailed
["explain"]
["Either --rule, --normalize, --morph, --dataize or --contextualize must be specified"]
it "fails when more than one rule set is specified" $
testCLIFailed
["explain", "--morph", "--dataize"]
["Only one of --morph, --dataize or --contextualize can be specified"]
it "allows --normalize together with --rule" $
testCLISucceeded
["explain", "--normalize", "--rule=resources/normalize/copy.yaml"]
["\\phinoNormalizationRule{copy}"]
it "allows --shuffle together with --morph" $
testCLISucceeded
["explain", "--morph", "--shuffle"]
["\\begin{phinoMorphingInference}"]
it "writes to target file" $
bracket
( do
tmp <- getTemporaryDirectory
stamp <- getPOSIXTime
let dir = tmp </> ("phino-test-" ++ show (floor stamp :: Integer))
createDirectoryIfMissing True dir
pure (dir </> "explain.tex", dir)
)
(\(_, dir) -> removeDirectoryRecursive dir)
( \(path, _) -> do
testCLISucceeded ["explain", "--normalize", printf "--target=%s" path] []
content <- readFile path
_ <- evaluate (length content)
content `shouldContain` "\\phinoNormalizationRule{alpha}"
)
describe "merge" $ do
it "prints help" $
testCLISucceeded ["merge", "--help"] ["Paths to input files"]
it "merges single expression" $
testCLISucceeded
["merge", resource "desugar.phi", "--sweet", "--flat"]
["x:foo"]
it "merges EO expressions" $
testCLISucceeded
["merge", "--sweet", resource "number.phi", resource "bytes.phi", resource "string.phi", "--margin=25"]
[ unlines
[ "β¦"
, " eolang β¦ β¦"
, " number(Ο) β¦ β¦β§,"
, " bytes(data) β¦ β¦β§,"
, " string(Ο) β¦ β¦β§,"
, " Ξ» β€ Package"
, " β§,"
, " Ξ» β€ Package"
, "β§:org"
]
]
it "fails on merging non formations" $
testCLIFailed
["merge", resource "dispatch.phi", resource "number.phi"]
["Invalid expression format, only expressions with top level formations are supported for 'merge' command"]
it "fails on merging conflicted bindings" $
testCLIFailed
["merge", resource "foo.phi", resource "desugar.phi"]
["Can't merge two bindings, conflict found"]
it "fails on merging empty list of expressions" $
testCLIFailed
["merge"]
["At least one input file must be specified for 'merge' command"]
it "merges and prints as XMIR, with the listing rendered from the merged expression" $
testCLISucceeded
["merge", resource "desugar.phi", "--output=xmir"]
["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<listing>β¦ foo β¦ ΞΎ.x β§</listing>", "<o base=\"ΞΎ.x\" name=\"foo\"/>"]
it "names an atom of XMIR after its locator and keeps its type" $ do
let xmir = "<object><o name=\"number\"><o name=\"plus\"><o base=\"β
\" name=\"b\"/><o atom=\"Ξ¦.number\" name=\"Ξ»\"/></o></o></object>"
withTempFileContent "phino-atom.xmir" xmir $ \file -> do
testCLISucceeded
["merge", "--input=xmir", "--sweet", "--flat", file]
["L_number_plus:Ξ»"]
testCLISucceeded
["merge", "--input=xmir", "--output=xmir", file]
["<o atom=\"Ξ¦.number\" name=\"Ξ»\">L_number_plus</o>"]
it "keeps the type of an atom of XMIR under --canonize" $ do
let xmir = "<object><o name=\"number\"><o name=\"plus\"><o base=\"β
\" name=\"b\"/><o atom=\"Ξ¦.number\" name=\"Ξ»\"/></o></o></object>"
withTempFileContent "phino-canonized-atom.xmir" xmir $ \file ->
testCLISucceeded
["rewrite", "--input=xmir", "--output=xmir", "--canonize", file]
["<o atom=\"Ξ¦.number\" name=\"Ξ»\">Fn1</o>"]
it "reproduces the same output for the same --seed" $ do
let args =
[ "merge"
, "--seed=42"
, "--sweet"
, resource "number.phi"
, resource "bytes.phi"
]
(firstRun, _) <- withStdout (runCLI args)
(secondRun, _) <- withStdout (runCLI args)
firstRun `shouldBe` secondRun
describe "compile" $ do
it "writes the module to the target" $
withTempDirectory "phino-compile" $ \dir -> do
createDirectoryIfMissing True dir
withCurrentDirectory dir (runCLI ["compile", "--target=gen/Compiled.hs"])
doesFileExist (dir </> "gen" </> "Compiled.hs") `shouldReturn` True
it "writes the rules of --rule into the module" $
withTempDirectory "phino-compile" $ \dir -> do
createDirectoryIfMissing True dir
simple <- makeAbsolute "test-resources/cli/rules/simple.yaml"
withCurrentDirectory dir (runCLI ["compile", "--rule=" ++ simple, "--target=Compiled.hs"])
readFile' (dir </> "Compiled.hs") >>= (`shouldSatisfy` ("R.direct \"foo\"" `isInfixOf`))
it "turns the flag on in a new cabal.project.local" $
withTempDirectory "phino-compile" $ \dir -> do
createDirectoryIfMissing True dir
withCurrentDirectory dir (runCLI ["compile", "--target=Compiled.hs"])
readFile (dir </> "cabal.project.local") `shouldReturn` "package phino\n flags: +compiled\n"
it "prints the lines an existing cabal.project.local lacks" $
withTempDirectory "phino-compile" $ \dir -> do
createDirectoryIfMissing True dir
writeFile (dir </> "cabal.project.local") "tests: True\n"
withCurrentDirectory dir (testCLISucceeded ["compile", "--target=Compiled.hs"] ["package phino\n flags: +compiled"])
it "leaves an existing cabal.project.local as it is" $
withTempDirectory "phino-compile" $ \dir -> do
createDirectoryIfMissing True dir
writeFile (dir </> "cabal.project.local") "tests: True\n"
withStdout (withCurrentDirectory dir (runCLI ["compile", "--target=Compiled.hs"]))
readFile (dir </> "cabal.project.local") `shouldReturn` "tests: True\n"
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"
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
it "prints help" $
testCLISucceeded
["match", "--help"]
["Pattern expression to match against", "Predicate for matched substitutions"]
it "takes from stdin" $
withStdin "[[]]" $
testCLISucceeded ["match", "--log-level=debug"] ["[DEBUG]"]
it "takes from file" $
testCLISucceeded ["match", resource "foo.phi", "--log-level=debug"] ["[DEBUG]"]
it "does not print substitutions without pattern" $
withStdin "[[]]" $
testCLISucceeded ["match", "--log-level=debug"] ["[DEBUG]: The --pattern is not provided, no substitutions are built"]
it "refuses --when without --pattern" $
withStdin "[[]]" $
testCLIFailed ["match", "--when=bogus"] ["The option --when requires --pattern"]
it "reproduces the same output for the same --seed" $ do
dir <- getTemporaryDirectory
let file = dir ++ "/phino-match-seed-test.phi"
writeFile file "[[ x -> Q.x, y -> Q.y, z -> Q.z ]]"
let args =
[ "match"
, "--seed=42"
, "--sweet"
, "--flat"
, "--pattern=Q.!t"
, file
]
(firstRun, _) <- withStdout (runCLI args)
(secondRun, _) <- withStdout (runCLI args)
firstRun `shouldBe` secondRun
removeFile file
it "numbers two anonymous captures of one kind, so they stay apart" $
withStdin "[[ a -> [[ ]], b -> Q ]]" $
testCLISucceeded ["match", "--pattern=[[ !t -> !e, !t -> !e ]]"] ["e#1 >> β¦β§\ne#2 >> Ξ¦\nt#1 >> a\nt#2 >> b"]
it "prints many substitutions" $
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" $
withStdin "[[ a -> $, b -> Q ]]" $
testCLIFailed ["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),18446744073709551618)"] ["no substitutions are built"]
it "builds substitutions with conditions" $
withStdin "[[ x -> Q.y ]].x" $
testCLISucceeded
["match", "--pattern=[[ !t1 -> Q.y, !B1 ]].!t1", "--when=eq(length(!B1),0)"]
["B1 >> β¦β§\nt1 >> x"]
it "builds with condition from file" $
testCLISucceeded
["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),1)", resource "foo.phi"]
["B1 >> β¦ foo β¦ Ξ¦.org.eolang.x β§"]
it "rejects an anonymous meta in --when" $
withStdin "[[ x -> Q.y ]]" $
testCLIFailed
["match", "--pattern=[[ !B ]]", "--when=eq(length(!B),1)"]
["[ERROR]: Anonymous meta '!B' cannot be referenced in --when"]
it "fails on parsing --when condition" $
withStdin "[[]]" $
testCLIFailed
["match", "--pattern=[[!B]]", "--when=hello"]
["[ERROR]: Couldn't parse given condition"]
it "fails on empty substitutions" $
withStdin "Q.x.y" $
testCLIFailed
["match", "--pattern=$.!t"]
["[ERROR]"]
describe "CmdException Show instance" $
forM_
[ ("InvalidCLIArguments", InvalidCLIArguments "bad flag", "Invalid set of arguments: bad flag")
, ("CouldNotReadFromStdin", CouldNotReadFromStdin "broken pipe", "Could not read input from stdin\nReason: broken pipe")
, ("CouldNotDataize", CouldNotDataize, "Could not dataize given expression")
,
( "CouldNotPrintExpressionInXMIR"
, CouldNotPrintExpressionInXMIR
, "Could not print expression with --output=xmir, only expression printing is allowed"
)
, ("EmptySubstsOnMatch", EmptySubstsOnMatch, "Provided pattern was not matched, no substitutions are built")
,
( "VersionMismatch"
, VersionMismatch "1.2.3" "4.5.6"
, "Version mismatch: --pin requires '1.2.3', but this is phino 4.5.6"
)
, ("CouldNotCompile", CouldNotCompile "The rule 'q' cannot be compiled, since it is odd", "The rule 'q' cannot be compiled, since it is odd")
,
( "StaleEngine"
, StaleEngine
, "The compiled rules are stale, since the rules of phino changed after 'phino compile', so run it again and rebuild"
)
]
( \(desc, exception, expected) ->
it (desc ++ " renders its message") $ do
show exception `shouldBe` expected
displayException exception `shouldBe` expected
)
describe "IOFormat Show instance" $
forM_
[ ("XMIR", XMIR, "xmir")
, ("PHI", PHI, "phi")
, ("LATEX", LATEX, "latex")
]
( \(desc, format, expected) ->
it (desc ++ " renders as " ++ expected) $
show format `shouldBe` expected
)