phino-0.0.134: 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 Fixtures (lambdasFile, loopingLambdas, readUtf8, withLambdasOf)
import GHC.IO.Handle
import Paths_phino (version)
import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, getTemporaryDirectory, listDirectory, removeDirectoryRecursive, removeFile, removePathForcibly, setModificationTime)
import System.Exit (ExitCode (ExitFailure))
import System.FilePath ((</>))
import System.IO
import Test.Hspec
import Text.Printf (printf)
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
-- A fresh, uniquely-named directory under the system temp directory, removed
-- afterwards even when the action throws (an assertion failure included), so a
-- red run never leaves it behind for the next run to depend on.
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 ())
-- phino implements no Ξ» function of its own, so a case that needs one to
-- answer hands the fixture file to the command as '--symbolic' (see
-- 'Fixtures').
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 "--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"]
, ["β¦ a β¦ 42 β§"]
)
]
(\(desc, input, args, expected) -> it desc (withStdin input (testCLISucceeded args expected)))
it "prints debug info with --log-level=DEBUG" $
withStdin "[[]]" $
testCLISucceeded ["rewrite", "--log-level=DEBUG"] ["[DEBUG]:"]
describe "--log-level accepts every named level" $
forM_
["ERROR", "ERR", "error", "NONE", "none"]
( \flagValue ->
it ("--log-level=" ++ flagValue) $
withStdin "[[]]" $
testCLISucceeded ["rewrite", "--log-level=" ++ flagValue] ["β§"]
)
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 followed by Ο β¦ β
"]
)
]
(\(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 --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)))
-- Only assert the stable parts of the parse error: phino's envelope and
-- that megaparsec reports an 'unexpected' token. The exact line:column and
-- offending token depend on megaparsec's internal try/longest-match error
-- merging, which shifts between megaparsec releases (deps are unpinned), so
-- pinning them here makes the test brittle without testing anything extra.
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 --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"]
["β¦ x β¦ 5 β§"]
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 "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
-- The fix is about numbering, not about a specific rule set: the file
-- names must be distinct and contiguous from 00001, and there must be
-- more of them than a single normalization pass produces (this input
-- runs several normalizations, so a global counter yields more steps).
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-, Ο β¦ β¦ m β¦ β¦ Ξ β€ 01- β§ β§ β§, j β¦ β¦ Ξ β€ FF- β§ β§"]
it "normalizes from stdin" $
withStdin "β¦ a β¦ β¦ b β¦ β
β§ (b β¦ [[ ]]) β§" $
testCLISucceeded
["rewrite", "--normalize", "--margin=20"]
[ unlines
[ "β¦"
, " a β¦ β¦"
, " b β¦ β¦ Ο β¦ β
β§,"
, " Ο β¦ β
"
, " β§,"
, " Ο β¦ β
"
, "β§"
]
]
it "rewrites with --sweet flag" $
withStdin "[[ x -> 5]]" $
testCLISucceeded
["rewrite", "--sweet"]
["β¦ x β¦ 5 β§"]
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$@^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*}"
, "[[ |x| -> 5 ]]{.}"
, "\\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} [[ |x| -> 5 ]]{.}"
, "\\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}"
, "[[ |x| -> 5 ]]{.}"
, "\\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"]
["β¦ app β¦ β¦ x β¦ Ξ¦.number β§ β§"]
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"]
[ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<listing><?xml version="1.0" encoding="UTF-8"?><object><o name="app"><o name="x" base="Ξ¦.number"/></o></object></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"]
["x β¦ \"bar\""]
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
[ "β¦ x β¦ \"foo\" β§"
, "Ξ¦.x( y β¦ \"foo\" )"
, "β¦ x β¦ \"foo\" β§"
]
]
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"
, "β¦ x β¦ \"foo\" β§"
, ""
, "=== Step #2, Rule 'first', 31t -> 30t"
, "Ξ¦.x( y β¦ \"foo\" )"
, ""
, "=== Step #3, Rule 'second', 30t -> 31t"
, "β¦ x β¦ \"foo\" β§"
]
]
it "ignores --headers without --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--headers", "--sweet", "--flat"]
["β¦ x β¦ \"bar\" β§"]
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"
, "[[ |x| -> \"foo\" ]] \\leadsto_{\\nameref{r:first}}"
, "% === Step #2, Rule 'first', 31t -> 30t"
, " \\leadsto Q . |x| ( |y| -> \"foo\" ) \\leadsto_{\\nameref{r:second}}"
, "% === Step #3, Rule 'second', 30t -> 31t"
, " \\leadsto [[ |x| -> \"foo\" ]]{.}"
, "\\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}"
, "[[ |x| -> \"foo\" ]] \\leadsto_{\\nameref{r:first}}"
, " \\leadsto Q . |x| ( |y| -> \"foo\" ) \\leadsto_{\\nameref{r:second}}"
, " \\leadsto [[ |x| -> \"foo\" ]]{.}"
, "\\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| -> \\phinoMeet{foo:1}{ [[ D> |42-| ]] } ) . |y| \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto \\phinoMeet{foo:2}{ [[ |x| -> \\phinoAgain{foo:1}, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto \\phinoMeet{foo:3}{ [[ |x| -> \\phinoAgain{foo:1} ]] } . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto \\phinoAgain{foo:1} ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:3}, \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:3} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:2} ) \\leadsto_{\\nameref{r:stay}}"
, " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{foo:3} ]]{.}"
, "\\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| -> \\phinoMeet{1}{ [[ D> |42-| ]] } ) . |y| \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto \\phinoMeet{2}{ [[ |x| -> \\phinoAgain{1}, |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto \\phinoMeet{3}{ [[ |x| -> \\phinoAgain{1} ]] } . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto \\phinoAgain{1} ( \\phiTerminal{\\rho} -> \\phinoAgain{3}, \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{3} ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{2} ) \\leadsto_{\\nameref{r:stay}}"
, " \\leadsto [[ D> |42-|, \\phiTerminal{\\rho} -> \\phinoAgain{3} ]]{.}"
, "\\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}"
, "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> \\phinoMeet{1}{ [[ |t| -> 42 ]] } ]] ( |y| -> \\phinoAgain{1} ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> \\phinoAgain{1}, |k| -> \\phinoAgain{1} ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"
, " \\leadsto [[ |ex| -> T ]]{.}"
, "\\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}"
, "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"
, " \\leadsto [[ |ex| -> T ]]{.}"
, "\\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}"
, "[[ |ex| -> [[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| ]] \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ |ex| -> [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| ]] \\leadsto_{\\nameref{r:stop}}"
, " \\leadsto [[ |ex| -> T ]]{.}"
, "\\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}"
, "[[ |x| -> [[ |y| -> ?, |k| -> [[ |t| -> 42 ]] ]] ( |y| -> [[ |t| -> 42 ]] ) ]] . |i| \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ |x| -> [[ |y| -> [[ |t| -> 42 ]], |k| -> [[ |t| -> 42 ]] ]] ]] . |i| \\leadsto_{\\nameref{r:stop}}"
, " \\leadsto 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| \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto [[ |y| -> |x| ]] . |y| ( \\phiTerminal{\\rho} -> [[ |x| -> |y|, |y| -> |x| ]] ) \\leadsto"
, " \\leadsto \\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
[ "β¦ x β¦ β¦ y β¦ β
, k β¦ β¦ t β¦ 42 β§ β§( y β¦ β¦ t β¦ 42 β§ ) β§.i"
, "β¦ x β¦ β¦ y β¦ β¦ t β¦ 42 β§, k β¦ β¦ t β¦ 42 β§ β§ β§.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>β¦ x β¦ \"foo\" β§</listing>", " <listing>β¦ x β¦ \"bar\" β§</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"]
["x β¦ \"bar\""]
it "accepts range 1..3 when 1 cycle happens" $
withStdin "β¦ t β¦ β¦ x β¦ \"foo\" β§ β§" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--must=1..3", "--sweet"]
["x β¦ \"bar\""]
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` "β¦ x β¦ \"bar\" β§"
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` "β¦ x β¦ \"bar\" β§"
it "rewrites with cycles" $
withStdin "[[ x -> \"x\" ]]" $
testCLISucceeded
["rewrite", "--sweet", rule "infinite.yaml", "--max-depth=1", "--max-cycles=2"]
["β¦ x β¦ \"x_hi_hi\" β§"]
it "hides default package" $
withStdin "[[ org -> [[ eolang -> [[ number -> [[]] ]]]], x -> 42 ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--hide=Q.org"]
["β¦ x β¦ 42 β§"]
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"]
["β¦ org β¦ β¦ yegor256 β¦ Ξ¦.y β§ β§"]
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 β¦ β¦ eolang β¦ β¦ bytes(data) β¦ β¦β§, number(as-bytes) β¦ β¦β§ β§ β§ β§"]
)
it "reduces log message" $
withStdin "[[ x -> [[ y -> ? ]](y -> 5) ]]" $
testCLISucceeded
["rewrite", "--log-level=debug", "--log-lines=1", "--normalize"]
[ intercalate
"\n"
[ "[DEBUG]: Applied 'copy' (44 nodes -> 39 nodes)"
, "---| log is limited by --log-lines=1 option |---"
]
]
-- 'matches' inside 'when' raises while dataizing a formation: the
-- substitution is still dropped (the policy #1079 questions), but the
-- reason surfaces in the debug log instead of vanishing
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 β§ ) β§, Ξ» β€ Fn4 β§"]
it "rewrites by locator" $
withStdin "[[ ex -> [[ x -> [[ y -> 5 ]].y ]], abc -> [[ x -> ? ]](x -> 5) ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--locator=Q.ex", "--normalize"]
["β¦ ex β¦ β¦ x β¦ 5 β§, abc β¦ β¦ x β¦ β
β§( x β¦ 5 ) β§"]
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' (30 nodes -> 25 nodes)"
, "Rule 'stop' is a breakpoint, dropping down all the previous rewritings..."
, "β¦ x β¦ β
, y β¦ x β§( x β¦ β¦ Ξ β€ 42- β§ ).y"
]
describe "dataize" $ do
it "prints help" $
testCLISucceeded ["dataize", "--help"] ["Dataize the π-expression"]
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"]
-- The π/π» recursion used to be unbounded, so a Ξ» function answering with a
-- firing of itself kept morphing forever and no option could stop it
-- (#1052)
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"]
-- Under '--partial' the same term does not fail: the spent budget is a
-- stuck site too, and the run ends on the residual the spine reached (#1078)
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 β§"]
-- '--acyclic' used to be the 'morph' command's alone, so a program coming
-- back to a term through π» rather than π β a body dispatching the very
-- object it stands in, which π stops at a formation of every round and
-- only π» walks round β spent the whole budget and failed on the limit
-- (#1290)
describe "--acyclic" $ 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"]
-- The budget here is far larger than the one the run above failed on, so
-- what ends this one is the cut and not the limit
it "names the term it came back to with the flag" $
withStdin circling $
testCLIFailed
["dataize", "--locator=Q.t", "--acyclic", "--max-steps=4000"]
["[ERROR]: Reduction came back to a term it is already reducing:"]
-- π» insists on bytes and a parked term carries none, so what a cut run
-- prints is the residual program, exactly as it prints one for a Ξ»
-- function that cannot fire
it "prints the residue and exits successfully with --partial" $
withStdin circling $
testCLISucceeded
["dataize", "--locator=Q.t", "--acyclic", "--partial", "--max-steps=4000", "--flat", "--hide-rho"]
["β¦ cyc β¦ β¦ x β¦ β
, Ο β¦ Ξ¦.cyc( Ξ±0 β¦ ΞΎ.x ) β§, t β¦ β¦ x β¦ β¦β§, Ο β¦ Ξ¦.cyc( Ξ±0 β¦ ΞΎ.x ) β§ β§"]
-- The guard reads nothing but the terms the frames above it are
-- dataizing, so a run that never comes back to one answers as it always did
it "answers a terminating program the same way with the flag" $
withStdin "β¦ t β¦ β¦ Ξ β€ 01-02 β§ β§" $
testCLISucceeded ["dataize", "--locator=Q.t", "--acyclic"] ["01-02"]
it "dataizes with --sequence" $
withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $
testCLISucceeded
["dataize", "--sequence", "--output=latex", "--flat", "--sweet"]
[ intercalate
"\n"
[ "\\begin{phiquation}"
, "[[ @ -> [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| ]] \\leadsto_{\\nameref{r:contextualize}}"
, " \\leadsto [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] . |x| \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ) \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto [[ D> |01-|, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ]] \\leadsto_{\\nameref{r:delta}}"
, " \\leadsto |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"
[ "[[ D> |01-| ]] \\leadsto_{\\nameref{r:delta}}"
, " \\leadsto |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 ]] } \\leadsto_{\\nameref{r:contextualize}}"]
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 "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"] []
-- Every firing of the run reaches the protocol as a tree: the run itself,
-- one line per firing, one per operand it brought down or reduced and one
-- per answer it gave. Nothing but the symbols ties them together, so the
-- lines a firing writes are what a reader of the file walks back (#1226).
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 <- readUtf8 path
records `shouldBe` "π»(Ξ¦)\n"
-- An operand line says what the meta was bound to and, after two spaces
-- and '#', the term the entry wrote under it, so a reader never has to
-- open the '--symbolic' file beside the protocol to see what came down
-- to what (#1265)
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 <- readUtf8 path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " πΌ(L_number_plus) # π»(Ξ¦)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) # π"
, " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§ # π(π.1.1)"
]
-- The second firing of one entry numbers its own metas πΏ1.2 and πΏ2.2,
-- and the operand it brings down is the answer of the first, which the
-- protocol names rather than dataizes: every symbol answers the same 42
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 <- readUtf8 path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " πΌ(L_number_plus) # π(Ξ¦)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) # π"
, " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§ # π(π.1.1)"
, " πΌ(L_number_plus) # π»(Ξ¦)"
, " πΏ1.2 := π»(β¦ Ξ» β€ π1 β§) # π»(ΞΎ.Ο)"
, " πΏ2.2 := 40-1C-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.2.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π2 β§ ) # π"
, " π.2.2 := β¦ Ο β¦ β¦ Ξ» β€ π2 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§ # π(π.2.1)"
]
-- A meta is a variable bound exactly once, so its name has to be unique
-- in the whole file and the protocol refers back to it as a name. The
-- firings are therefore numbered across the run and not per Ξ» function:
-- the first firing of 'L_number_times' calls its operand πΏ1.2, never the
-- πΏ1.1 the first firing of 'L_number_plus' has already taken (#1261)
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 <- readUtf8 path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " πΌ(L_number_plus) # π(Ξ¦)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) # π"
, " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§, times(x) β¦ β¦ Ξ» β€ L_number_times β§ β§ # π(π.1.1)"
, " πΌ(L_number_times) # π»(Ξ¦)"
, " πΏ1.2 := π»(β¦ Ξ» β€ π1 β§) # π»(ΞΎ.Ο)"
, " πΏ2.2 := 40-1C-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.2.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π2 β§ ) # π"
, " π.2.2 := β¦ Ο β¦ β¦ Ξ» β€ π2 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§, times(x) β¦ β¦ Ξ» β€ L_number_times β§ β§ # π(π.2.1)"
]
-- An operand is brought down by a whole run of π», so a Ξ» function it
-- fires on the way sits one level deeper than the firing waiting for it
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 <- readUtf8 path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " πΌ(L_number_plus) # π»(Ξ¦)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΌ(L_number_plus) # π»(Ξ¦.aπ΅1)"
, " πΏ1.2 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΏ2.2 := 40-1C-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.2.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) # π"
, " π.2.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§ # π(π.2.1)"
, " πΏ2.1 := π»(β¦ Ξ» β€ π1 β§) # π»(ΞΎ.x)"
, " π.1.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π2 β§ ) # π"
, " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π2 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§ # π(π.1.1)"
]
-- A 'symbolize' line stands the data of a term an earlier line bound
-- into unknowns, so the protocol says what is known about each fresh
-- symbol before it writes the term carrying them. The fact is no
-- assignment to the symbol: a π is the name of a Ξ» function and
-- nothing binds bytes to it, so what is known is that dataizing the
-- formation it names answers them (#1269)
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 <- readUtf8 path
lines records
`shouldBe` [ "π(Ξ¦.y)"
, " πΌ(L_stand) # π(Ξ¦.y)"
, " π1.1 := β¦ Ξ β€ 01- β§ # π(ΞΎ.x)"
, " π»(β¦ Ξ» β€ π1 β§) == 01-"
, " π2.1 := β¦ Ξ» β€ π1 β§ # π1"
, " π.1.1 := β¦ z β¦ β¦ Ξ» β€ π1 β§ β§ # π"
, " π.1.2 := β¦ z β¦ β¦ Ξ» β€ π1 β§ β§ # π(π.1.1)"
]
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 <- readUtf8 path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " πΌ(L_number_plus) # π(Ξ¦)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) # π"
, " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§, nope β¦ β¦ Ξ» β€ L_number_nope β§ β§ # π(π.1.1)"
, " ?(L_number_nope) # π»(β¦ Ξ» β€ L_number_nope β§)"
]
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 <- readUtf8 path
records `shouldBe` "π»(Ξ¦)\n"
-- The protocol is a tree of one-line π records whatever the run prints
-- its own answer as, so a program reading it back never has to know
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 <- readUtf8 path
records `shouldEndWith` " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§ # π(π.1.1)\n"
-- The same facts as markup, so a program reading the protocol back never
-- has to parse π to learn them: the name of an element says what its
-- record is, the value a meta took is the text of the element and each
-- symbol a firing minted stands in a record of its own (#1245, #1257,
-- #1280). Which of the two formats is written is decided by the name of
-- the file and by nothing else
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize locator=\"Ξ¦\">"
, " <evaluate Ξ»=\"L_number_plus\" id=\"1\" judgment=\"dataize\" locator=\"Ξ¦\">"
, " <bind meta=\"πΏ1.1\">40-14-00-00-00-00-00-00</bind>"
, " <bind meta=\"πΏ2.1\">40-18-00-00-00-00-00-00</bind>"
, " <minted>π1</minted>"
, " <built meta=\"π.1.1\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ )</built>"
, " <answer meta=\"π.1.2\">β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§</answer>"
, " </evaluate>"
, "</dataize>"
]
-- A run firing nothing still writes a document a parser can read,
-- since the root is closed on the way out and not by the last firing
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize locator=\"Ξ¦\">"
, "</dataize>"
]
-- An operand that came down to a manufactured datum is a 'dataize'
-- holding the formation its symbol names, never the 42 every symbol
-- answers and never the bare name a π» cannot be applied to (#1278),
-- while one that came down to data is a 'bind' holding that data: the
-- name of the element is what tells the two apart (#1257)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize locator=\"Ξ¦\">"
, " <evaluate Ξ»=\"L_number_plus\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦\">"
, " <bind meta=\"πΏ1.1\">40-14-00-00-00-00-00-00</bind>"
, " <bind meta=\"πΏ2.1\">40-18-00-00-00-00-00-00</bind>"
, " <minted>π1</minted>"
, " <built meta=\"π.1.1\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ )</built>"
, " <answer meta=\"π.1.2\">β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§</answer>"
, " </evaluate>"
, " <evaluate Ξ»=\"L_number_plus\" id=\"2\" judgment=\"dataize\" locator=\"Ξ¦\">"
, " <dataize meta=\"πΏ1.2\">β¦ Ξ» β€ π1 β§</dataize>"
, " <bind meta=\"πΏ2.2\">40-1C-00-00-00-00-00-00</bind>"
, " <minted>π2</minted>"
, " <built meta=\"π.2.1\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π2 β§ )</built>"
, " <answer meta=\"π.2.2\">β¦ Ο β¦ β¦ Ξ» β€ π2 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§</answer>"
, " </evaluate>"
, "</dataize>"
]
-- The fact a 'symbolize' line knows about a symbol is an element of
-- its own, next to '<bind>' and '<dataize>': the symbol stands in the
-- attribute a reader joins lines on and the data it stands for is the
-- text, so a consumer reads a constant off the markup without parsing
-- π (#1269)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph locator=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_stand\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">β¦ Ξ β€ 01- β§</bind>"
, " <known symbol=\"π1\">01-</known>"
, " <bind meta=\"π2.1\">β¦ Ξ» β€ π1 β§</bind>"
, " <built meta=\"π.1.1\">β¦ z β¦ β¦ Ξ» β€ π1 β§ β§</built>"
, " <answer meta=\"π.1.2\">β¦ z β¦ β¦ Ξ» β€ π1 β§ β§</answer>"
, " </evaluate>"
, "</morph>"
]
-- What a 'join' line knows about the symbol it minted is an element of
-- its own too, the way the fact a 'symbolize' line writes is: the
-- fresh symbol stands in the attribute a reader joins lines on and the
-- two symbols it was minted for are the text, in the order the line
-- lists the metas it joins. The meta it binds is a '<bind>' like every
-- other meta of the firing (#1246). The branches differ under Ο, that
-- being where the value of a branch is reached and so the only place a
-- join looks at all (#1293)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph locator=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_fork\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">β¦ Ο β¦ β¦ Ξ» β€ π1 β§ β§</bind>"
, " <bind meta=\"π2.1\">β¦ Ο β¦ β¦ Ξ» β€ π2 β§ β§</bind>"
, " <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>"
]
-- Which symbols a firing minted is a fact about the firing and not a
-- property of one term of it, so each of them stands in a record of
-- its own, the way what is known about a symbol does: an answer
-- minting two writes two, and nothing is left to guess which of the
-- two an attribute summarizing the term would have named (#1280)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph locator=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_pair\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">β¦ Ξ β€ 01- β§</bind>"
, " <minted>π1</minted>"
, " <minted>π2</minted>"
, " <built meta=\"π.1.1\">β¦ left β¦ β¦ Ξ» β€ π1 β§, right β¦ β¦ Ξ» β€ π2 β§ β§</built>"
, " <answer meta=\"π.1.2\">β¦ left β¦ β¦ Ξ» β€ π1 β§, right β¦ β¦ Ξ» β€ π2 β§ β§</answer>"
, " </evaluate>"
, "</morph>"
]
-- An entry answering a meta it already bound asks for no symbol of its
-- own, so its block holds no 'minted' at all: the records say what the
-- firing did and never stand empty to say that it did nothing (#1280)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph locator=\"Ξ¦.y\">"
, " <evaluate Ξ»=\"L_keep\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦.y\">"
, " <bind meta=\"π1.1\">β¦ Ξ β€ 01- β§</bind>"
, " <built meta=\"π.1.1\">β¦ z β¦ β¦ Ξ β€ 01- β§ β§</built>"
, " <answer meta=\"π.1.2\">β¦ z β¦ β¦ Ξ β€ 01- β§ β§</answer>"
, " </evaluate>"
, "</morph>"
]
-- A firing taken while an operand of another was coming down stands
-- inside that firing's element, which is where the indented tree of
-- the text format stands it too
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize locator=\"Ξ¦\">"
, " <evaluate Ξ»=\"L_number_plus\" id=\"1\" judgment=\"dataize\" locator=\"Ξ¦\">"
, " <bind meta=\"πΏ1.1\">40-14-00-00-00-00-00-00</bind>"
, " <evaluate Ξ»=\"L_number_plus\" id=\"2\" judgment=\"dataize\" locator=\"Ξ¦.aπ΅1\">"
, " <bind meta=\"πΏ1.2\">40-18-00-00-00-00-00-00</bind>"
, " <bind meta=\"πΏ2.2\">40-1C-00-00-00-00-00-00</bind>"
, " <minted>π1</minted>"
, " <built meta=\"π.2.1\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ )</built>"
, " <answer meta=\"π.2.2\">β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§</answer>"
, " </evaluate>"
, " <dataize meta=\"πΏ2.1\">β¦ Ξ» β€ π1 β§</dataize>"
, " <minted>π2</minted>"
, " <built meta=\"π.1.1\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π2 β§ )</built>"
, " <answer meta=\"π.1.2\">β¦ Ο β¦ β¦ Ξ» β€ π2 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§</answer>"
, " </evaluate>"
, "</dataize>"
]
-- Nothing fired, so the element stands alone and nothing opens under
-- it, exactly as '?(β¦)' stands alone in the text format; the formation
-- πΌ was asked about stands as the text of it, the way the comment of
-- the text format carries it (#1300)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize locator=\"Ξ¦\">"
, " <evaluate Ξ»=\"L_number_times\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦\">"
, " <bind meta=\"πΏ1.1\">40-00-00-00-00-00-00-00</bind>"
, " <bind meta=\"πΏ2.1\">40-08-00-00-00-00-00-00</bind>"
, " <minted>π1</minted>"
, " <built meta=\"π.1.1\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ )</built>"
, " <answer meta=\"π.1.2\">β¦ Ο β¦ β¦ Ξ» β€ π1 β§, times(x) β¦ β¦ Ξ» β€ L_number_times β§, nope β¦ β¦ Ξ» β€ L_number_nope β§ β§</answer>"
, " </evaluate>"
, " <stuck Ξ»=\"L_number_nope\" judgment=\"dataize\">β¦ Ξ» β€ L_number_nope β§</stuck>"
, "</dataize>"
]
-- The root is named after the judgment the run ran, the way every
-- record under it is named after the judgment it carries, and the term
-- the run was aimed at stands in its one attribute: a morphing opens
-- 'morph' where the text format opens π(Ξ¦.x) (#1279)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph locator=\"Ξ¦.x\">"
, " <stuck Ξ»=\"L_number_nope\" judgment=\"morph\">β¦ Ξ» β€ L_number_nope, Ο β¦ β
β§</stuck>"
, "</morph>"
]
-- A document a parser chokes on is worth nothing, so what the run left
-- open is closed on the way out and not by the last record: a run that
-- dies half-way through a derivation still leaves the firings it paid
-- for, inside elements that end
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<dataize locator=\"Ξ¦\">"
, " <evaluate Ξ»=\"L_number_times\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦\">"
, " <bind meta=\"πΏ1.1\">40-00-00-00-00-00-00-00</bind>"
, " <bind meta=\"πΏ2.1\">40-08-00-00-00-00-00-00</bind>"
, " <minted>π1</minted>"
, " <built meta=\"π.1.1\">Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1, Ο β¦ β
β§ )</built>"
, " <answer meta=\"π.1.2\">β¦ Ο β¦ β¦ Ξ» β€ π1, Ο β¦ β
β§, times β¦ β¦ x β¦ β
, Ξ» β€ L_number_times, Ο β¦ β
β§, nope β¦ β¦ Ξ» β€ L_number_nope, Ο β¦ β
β§, Ο β¦ Ξ¦ β§</answer>"
, " </evaluate>"
, " <stuck Ξ»=\"L_number_nope\" judgment=\"dataize\">β¦ Ξ» β€ L_number_nope, Ο β¦ β¦ Ο β¦ β¦ Ξ» β€ π1, Ο β¦ β
β§, times β¦ β¦ x β¦ β
, Ξ» β€ L_number_times, Ο β¦ β
β§, nope β¦ β¦ Ξ» β€ L_number_nope, Ο β¦ β
β§, Ο β¦ Ξ¦ β§ β§</stuck>"
, "</dataize>"
]
-- A 'morph' operand π answered the terminator for says what it is by
-- being β₯ and nothing else, the way every other bound meta says what
-- it is by its own term. The entry answers with a fresh symbol and the
-- dispatch '.foo' then stands on it, so the run ends on the symbol the
-- way it ends on a Ξ» name nothing answers, and the markup carries that
-- site too (#1287)
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 <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph locator=\"Ξ¦.x\">"
, " <evaluate Ξ»=\"L_pick\" id=\"1\" judgment=\"morph\" locator=\"Ξ¦.x\">"
, " <bind meta=\"π1.1\">β₯</bind>"
, " <minted>π1</minted>"
, " <built meta=\"π.1.1\">β¦ Ξ» β€ π1 β§</built>"
, " <answer meta=\"π.1.2\">β¦ Ξ» β€ π1 β§</answer>"
, " </evaluate>"
, " <stuck Ξ»=\"π1\" judgment=\"morph\">β¦ Ξ» β€ π1 β§</stuck>"
, "</morph>"
]
-- The extension decides and nothing else, so a name ending in
-- anything but '.xml' keeps the indented text it has always written
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 <- readUtf8 path
take 1 (lines records) `shouldBe` ["π»(Ξ¦)"]
-- A Ξ» function no entry of the '--symbolic' file answers cannot fire β a
-- placeholder such as β¦ Ξ» β€ Sym_arg_0 β§ standing in for a data input, or
-- an operation the caller left out of its file on purpose. The run used
-- to die on it, discarding what it had already evaluated (#1060)
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 ]]"
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 β§"]
-- What the firing before the stuck one answered is a symbol, and the
-- residue carries it where the value nobody worked out belongs
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 <- readUtf8 path
lines records
`shouldBe` [ "π»(Ξ¦)"
, " πΌ(L_number_times) # π(Ξ¦)"
, " πΏ1.1 := 40-00-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΏ2.1 := 40-08-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) # π"
, " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, times(x) β¦ β¦ Ξ» β€ L_number_times β§, nope β¦ β¦ Ξ» β€ L_number_nope β§ β§ # π(π.1.1)"
, " ?(L_number_nope) # π»(β¦ Ξ» β€ L_number_nope β§)"
]
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"]
-- The residual is an arbitrary formation, and a multi-binding <object>
-- is exactly what XMIR now carries: one <o> per binding (#1076)
it "prints the residual to XMIR, with its real listing by default" $
withStdin dispatched $
testCLISucceeded
["dataize", symbolic, "--partial", "--output=xmir"]
["<o name=\"Ξ»\">L_number_nope</o>", "<o name=\"Ο\">", "<listing>β¦"]
it "honors --hide-rho and --omit-listing when printing the residual to XMIR" $
withStdin dispatched $
testCLISucceeded
["dataize", symbolic, "--partial", "--output=xmir", "--hide-rho", "--omit-listing"]
["<o name=\"Ξ»\">L_number_nope</o>", "line(s)</listing>"]
-- A symbol is a name of the calculus, and XMIR carries no notation for
-- one, so a residue standing for an unknown cannot be printed as XMIR
it "cannot print a residue carrying a symbol as XMIR" $
withStdin stuck $
testCLIFailed
["dataize", symbolic, "--partial", "--output=xmir"]
["XMIR does not support such bindings"]
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 β₯"]
-- Which Ξ» functions exist is not phino's business: the file given with
-- '--symbolic' decides, and phino carries none of its own
describe "--symbolic" $ do
let sum' = "[[ bytes β¦ β¦ Ο β¦ β
β§, number(Ο) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]"
-- Nothing is worked out: the entry answers a number standing for the sum
-- and the run brings that symbol down to the datum every symbol answers
it "fires the Ξ» function an entry of the file answers" $
withStdin sum' $
testCLISucceeded ["dataize", symbolic] ["40-45-00-00-00-00-00-00"]
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"]
-- A file that is no list of entries is refused where it is read, which
-- is before the input is even parsed, rather than when a Ξ» function of
-- it fires
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"]
-- An expression the program does not carry is reduced inside it all the
-- same: '--inside' binds it to a synthetic attribute of the universe and
-- aims the run at it, which is what the 'dataize' block of a Ξ» function
-- does for every operand it names
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"]
-- The expression is normalized first, so a dispatch off a formation β
-- the very shape an operand reaches π» as, 'β¦ x β¦ 6, Ο β¦ 5 β§.x' β
-- reduces too
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 "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-"]
-- π was reachable only from inside π», through the 'norm' rule of the
-- dataization relation, so there was no way to ask phino for π(n, Ξ¦) on its
-- own (#1114)
describe "morph" $ do
-- Two chained Ξ» function calls: the inner fires under 'ml', because '.plus'
-- is dispatched on its result, while the outer application is saturated but
-- bare, so 'mf' hands it back and firing it is π»'s job
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 β§"]
-- The same term under π», which insists on bytes and fires what π left bare
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"]
-- 'mf' hands a formation back as it is, so '--locator' is how one aims π at
-- a subterm worth navigating: here it resolves Ξ¦ against the universe and
-- peels the dispatch through π©
it "morphs the subterm --locator aims at" $
withStdin "[[ ex -> Q.x, x -> [[ D> 42- ]] ]]" $
testCLISucceeded ["morph", "--locator=Q.ex", "--flat", "--hide-rho"] ["β¦ Ξ β€ 42- β§"]
-- π is total and π» is not: where the derivation dies, π answers β₯ ('xi'
-- here) and the run succeeds, while π» has no bytes to give and fails
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 β₯"]
-- The chain carries the spine: the morphing rules that reduced the term
-- ('maa', then the terminal 'mf') with the normalization steps they spliced
-- in ('alpha', 'copy'). The 'ml' firing of the inner call is not there by
-- design β it happens in a side premise, which reduces on a chain of its
-- own and discards it
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 "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 <- readUtf8 path
lines records
`shouldBe` [ "π(Ξ¦.Ο)"
, " πΌ(L_number_plus) # π(Ξ¦.Ο)"
, " πΏ1.1 := 40-14-00-00-00-00-00-00 # π»(ΞΎ.Ο)"
, " πΏ2.1 := 40-18-00-00-00-00-00-00 # π»(ΞΎ.x)"
, " π.1.1 := Ξ¦.number( Ο β¦ β¦ Ξ» β€ π1 β§ ) # π"
, " π.1.2 := β¦ Ο β¦ β¦ Ξ» β€ π1 β§, plus(x) β¦ β¦ Ξ» β€ L_number_plus β§ β§ # π(π.1.1)"
]
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- β§"]
-- The division π» cannot finish, whatever '--max-steps' it is given (#1052),
-- is no work at all for π: the term is already a formation, so 'mf' hands
-- it back and the Ξ» function is never fired
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"]
-- '--max-steps' bounds the π recursion just as it bounds the π/π» one
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"]
-- '--partial' parks a spent π budget the same way it parks a stuck Ξ»:
-- the answer is the term the walk had reached, dispatch intact (#1078)
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 )"]
-- π never fires a bare Ξ»-formation, so only the Ξ» functions sitting under
-- a dispatch ('ml') can get stuck; '--partial' parks them as under π»
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"]
-- π stops at the first formation and hands its bindings back as they were
-- written, so a program whose parts nothing demands is never reduced;
-- '--deep' enters every binding and finishes what 'mf' left, while what no
-- Ξ» function touched keeps its name and the answer stays a program (#1124)
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 ) ) β§"]
-- No entry answers 'L_bar', so the call to it stays as written and keeps
-- its name, while the arithmetic in the argument nothing demands folds
-- into the symbol standing for the number nobody worked out
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 β§ β§ ) β§"]
-- The same term the run above stops at as a bare Ξ»-formation: 'mf' leaves
-- it to π», and the walk fires it instead of demanding bytes
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 β§ β§"]
-- The default locator walks the whole program: the method table of the
-- object model keeps every one of its Ξ»-formations, since not one of them
-- is saturated, while the one place that can be computed is
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 β¦ β¦ foo β¦ β¦ n β¦ 3, Ο β¦ Ξ¦.bar( β¦ Ο β¦ β¦ Ξ» β€ π2 β§, times(x) β¦ β¦ Ξ» β€ L_number_times β§ β§ ) β§ β§"
]
it "keeps a binding whose spine got stuck with --partial" $
withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $
testCLISucceeded
["morph", "--deep", "--partial", "--sweet", "--hide-rho", "--flat"]
["β¦ x β¦ β¦ Ξ» β€ Sym_arg_0 β§.foo β§"]
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'"]
-- The step budget used to be the only thing ending the π/π» recursion, so an
-- entry answering with a firing of itself spent the whole of it and then
-- failed on the limit; '--acyclic' stops the moment morphing comes back to a
-- term a frame above it is already reducing and parks that site the way
-- '--partial' parks a Ξ» function that cannot fire
describe "--acyclic" $ 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"]
-- The budget here is far larger than the one the run above failed on, so
-- what ends this one is the cut and not the limit
it "prints the residue and exits successfully with the flag" $
loopingLambdas $ \endless ->
withStdin looping $
testCLISucceeded
["morph", "--symbolic=" ++ endless, "--locator=Q.x", "--acyclic", "--max-steps=4000", "--flat", "--hide-rho"]
["β¦ Ξ» β€ L_loop β§.foo"]
-- The guard reads nothing but the terms the frames above it are reducing,
-- so a run that never comes back to one answers exactly as it did before
it "answers a terminating program the same way with the flag" $
withStdin chained $
testCLISucceeded
["morph", symbolic, "--acyclic", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"]
["β¦ x β¦ 7, Ξ» β€ L_number_plus β§"]
-- The deep walk parks the one binding that loops and walks on, the way it
-- walks on past a Ξ» function '--partial' could not fire, so what the loop
-- costs is that binding and not the rest of the program
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", "--max-steps=4000", "--flat", "--hide-rho"]
["β¦ x β¦ β¦ Ξ» β€ L_loop β§.foo, y β¦ β¦ z β¦ β¦β§ β§ β§"]
describe "fails" $ do
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
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" $
testCLISucceeded
["explain", "--rule=resources/normalize/copy.yaml"]
[ unlines
[ "\\phinoNormalizationRule{copy}"
, " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
, " { [[ B_1, \\tau -> k, B_2 ]] }"
, " { }"
, " { }"
]
]
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}"]
it "explains normalization rules" $
testCLISucceeded
["explain", "--normalize"]
[ unlines
[ "\\phinoNormalizationRule{alpha}"
, " { [[ B_1, \\tau -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"
, " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> e ) }"
, " { i = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }"
, " { }"
, "\\phinoNormalizationRule{amiss}"
, " { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"
, " { T }"
, " { \\vert \\overline{ B } \\vert \\leq i }"
, " { }"
, "\\phinoNormalizationRule{copy}"
, " { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"
, " { [[ B_1, \\tau -> k, B_2 ]] }"
, " { }"
, " { }"
, "\\phinoNormalizationRule{dc}"
, " { T ( \\tau -> e ) }"
, " { T }"
, " { }"
, " { }"
, "\\phinoNormalizationRule{dca}"
, " { T ( \\phiTerminal{\\alpha_{i}} -> e ) }"
, " { T }"
, " { }"
, " { }"
, "\\phinoNormalizationRule{dd}"
, " { T . \\tau }"
, " { T }"
, " { }"
, " { }"
, "\\phinoNormalizationRule{dl}"
, " { [[ B_1, L> F, B_2 ]] }"
, " { T }"
, " { D \\in B_1 \\;\\text{or}\\; D \\in B_2 }"
, " { }"
, "\\phinoNormalizationRule{dot}"
, " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"
, " { e_2 ( \\phiTerminal{\\rho} -> [[ B_1, \\tau -> n, B_2 ]] ) }"
, " { [[ B_1, \\tau -> n, B_2 ]] \\not= e_1 }"
, " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_2 } }"
, "\\phinoNormalizationRule{dotg}"
, " { [[ B_1, \\tau -> n, B_2 ]] . \\tau }"
, " { e_2 ( \\phiTerminal{\\rho} -> Q ) }"
, " { [[ B_1, \\tau -> n, B_2 ]] = e_1 }"
, " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_2 } }"
, "\\phinoNormalizationRule{miss}"
, " { [[ B ]] ( \\tau -> e ) }"
, " { T }"
, " { \\tau \\notin B }"
, " { }"
, "\\phinoNormalizationRule{null}"
, " { [[ B_1, \\tau -> ?, B_2 ]] . \\tau }"
, " { T }"
, " { }"
, " { }"
, "\\phinoNormalizationRule{over}"
, " { [[ B_1, \\tau -> e_1, B_2 ]] ( \\tau -> e_2 ) }"
, " { T }"
, " { \\tau \\not= \\phiTerminal{\\rho} }"
, " { }"
, "\\phinoNormalizationRule{overa}"
, " { [[ B_1, \\tau -> e_1, B_2 ]] ( \\phiTerminal{\\alpha_{i}} -> e_2 ) }"
, " { T }"
, " { i = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }"
, " { }"
, "\\phinoNormalizationRule{stay}"
, " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] ( \\phiTerminal{\\rho} -> e_2 ) }"
, " { [[ B_1, \\phiTerminal{\\rho} -> e_1, B_2 ]] }"
, " { }"
, " { }"
, "\\phinoNormalizationRule{stop}"
, " { [[ B ]] . \\tau }"
, " { T }"
, " { \\tau \\notin B \\;\\text{and}\\; @ \\notin B \\;\\text{and}\\; L \\notin B }"
, " { }"
]
]
it "explains morphing rules" $
testCLISucceeded
["explain", "--morph"]
[ unlines
[ "\\begin{phinoMorphingInference}"
, " \\phinoName{dead}"
, " \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s }{ T }{ s } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{ma}"
, " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoPremise{ \\phinoNormalize{ n_2 ( \\tau -> k ) }{ n_3 } }"
, " \\phinoPremise{ \\phinoMorph{ n_3 }{ e }{ s_2 }{ n_4 }{ s_3 } }"
, " \\phinoConclusion{ \\phinoMorph{ n_1 ( \\tau -> k ) }{ e }{ s_1 }{ n_4 }{ s_3 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{maa}"
, " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoPremise{ \\phinoNormalize{ n_2 ( \\phiTerminal{\\alpha_{i}} -> k ) }{ n_3 } }"
, " \\phinoPremise{ \\phinoMorph{ n_3 }{ e }{ s_2 }{ n_4 }{ s_3 } }"
, " \\phinoConclusion{ \\phinoMorph{ n_1 ( \\phiTerminal{\\alpha_{i}} -> k ) }{ e }{ s_1 }{ n_4 }{ s_3 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{maad}"
, " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"
, " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{mad}"
, " \\phinoCondition{ \\phinoNotAbsolute{ n_1 } }"
, " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> n_1 ) }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{md}"
, " \\phinoCondition{ \\phinoNotFormation{ n_1 } }"
, " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoPremise{ \\phinoNormalize{ n_2 . \\tau }{ n_3 } }"
, " \\phinoPremise{ \\phinoMorph{ n_3 }{ e }{ s_2 }{ n_4 }{ s_3 } }"
, " \\phinoConclusion{ \\phinoMorph{ n_1 . \\tau }{ e }{ s_1 }{ n_4 }{ s_3 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{mf}"
, " \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s }{ [[ B ]] }{ s } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{mg}"
, " \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n }{ s_2 } }"
, " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{ml}"
, " \\phinoLabel{\\lambda}"
, " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"
, " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"
, " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"
, " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{mphi}"
, " \\phinoLabel{\\varphi}"
, " \\phinoCondition{ @ \\in B \\;\\text{and}\\; \\tau \\notin B \\;\\text{and}\\; L \\notin B }"
, " \\phinoPremise{ \\phinoNormalize{ [[ B ]] . @ . \\tau }{ n_1 } }"
, " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoConclusion{ \\phinoMorph{ [[ B ]] . \\tau }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{universe}"
, " \\phinoLabel{\\Phi}"
, " \\phinoCondition{ e \\not= Q }"
, " \\phinoPremise{ \\phinoNormalize{ e }{ n_1 } }"
, " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, "\\end{phinoMorphingInference}"
, "\\begin{phinoMorphingInference}"
, " \\phinoName{xi}"
, " \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"
, " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ n }{ s_2 } }"
, "\\end{phinoMorphingInference}"
]
]
it "explains dataization rules" $
testCLISucceeded
["explain", "--dataize"]
[ unlines
[ "\\begin{phinoDataizationInference}"
, " \\phinoName{box}"
, " \\phinoCondition{ [ D \\char44{} L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }"
, " \\phinoPremise{ \\phinoContextualize{ e_2 }{ [[ B_1, @ -> e_2, B_2 ]] }{ e_3 } }"
, " \\phinoPremise{ \\phinoNormalize{ e_3 }{ n } }"
, " \\phinoPremise{ \\phinoDataize{ n }{ e_1 }{ s_1 }{ \\delta }{ s_2 } }"
, " \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_2, B_2 ]] }{ e_1 }{ s_1 }{ \\delta }{ s_2 } }"
, "\\end{phinoDataizationInference}"
, "\\begin{phinoDataizationInference}"
, " \\phinoName{delta}"
, " \\phinoLabel{\\Delta}"
, " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s }{ \\delta }{ s } }"
, "\\end{phinoDataizationInference}"
, "\\begin{phinoDataizationInference}"
, " \\phinoName{fire}"
, " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n }{ s_2 } }"
, " \\phinoPremise{ \\phinoDataize{ n }{ e }{ s_2 }{ \\delta }{ s_3 } }"
, " \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_3 } }"
, "\\end{phinoDataizationInference}"
, "\\begin{phinoDataizationInference}"
, " \\phinoName{none}"
, " \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B = \\emptyset }"
, " \\phinoPremise{ \\phinoDataize{ T }{ e }{ s_1 }{ \\delta }{ s_2 } }"
, " \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"
, "\\end{phinoDataizationInference}"
, "\\begin{phinoDataizationInference}"
, " \\phinoName{norm}"
, " \\phinoCondition{ \\phinoNotFormation{ n_1 } \\;\\text{and}\\; n_1 \\not= T }"
, " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_1 }{ n_2 }{ s_2 } }"
, " \\phinoPremise{ \\phinoDataize{ n_2 }{ e }{ s_2 }{ \\delta }{ s_3 } }"
, " \\phinoConclusion{ \\phinoDataize{ n_1 }{ e }{ s_1 }{ \\delta }{ s_3 } }"
, "\\end{phinoDataizationInference}"
]
]
it "explains contextualization rules" $
testCLISucceeded
["explain", "--contextualize"]
[ unlines
[ "\\begin{phinoContextualizationInference}"
, " \\phinoName{ca}"
, " \\phinoPremise{ \\phinoContextualize{ n_1 }{ k }{ n_2 } }"
, " \\phinoPremise{ \\phinoContextualize{ e }{ k }{ n_3 } }"
, " \\phinoConclusion{ \\phinoContextualize{ n_1 ( \\tau -> e ) }{ k }{ n_2 ( \\tau -> n_3 ) } }"
, "\\end{phinoContextualizationInference}"
, "\\begin{phinoContextualizationInference}"
, " \\phinoName{caa}"
, " \\phinoPremise{ \\phinoContextualize{ n_1 }{ k }{ n_2 } }"
, " \\phinoPremise{ \\phinoContextualize{ e }{ k }{ n_3 } }"
, " \\phinoConclusion{ \\phinoContextualize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> e ) }{ k }{ n_2 ( \\phiTerminal{\\alpha_{i}} -> n_3 ) } }"
, "\\end{phinoContextualizationInference}"
, "\\begin{phinoContextualizationInference}"
, " \\phinoName{cd}"
, " \\phinoPremise{ \\phinoContextualize{ n_1 }{ k }{ n_2 } }"
, " \\phinoConclusion{ \\phinoContextualize{ n_1 . \\tau }{ k }{ n_2 . \\tau } }"
, "\\end{phinoContextualizationInference}"
, "\\begin{phinoContextualizationInference}"
, " \\phinoName{cf}"
, " \\phinoConclusion{ \\phinoContextualize{ [[ B ]] }{ k }{ [[ B ]] } }"
, "\\end{phinoContextualizationInference}"
, "\\begin{phinoContextualizationInference}"
, " \\phinoName{cg}"
, " \\phinoConclusion{ \\phinoContextualize{ Q }{ k }{ Q } }"
, "\\end{phinoContextualizationInference}"
, "\\begin{phinoContextualizationInference}"
, " \\phinoName{ct}"
, " \\phinoConclusion{ \\phinoContextualize{ T }{ k }{ T } }"
, "\\end{phinoContextualizationInference}"
, "\\begin{phinoContextualizationInference}"
, " \\phinoName{cxi}"
, " \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k }{ k } }"
, "\\end{phinoContextualizationInference}"
]
]
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"]
["β¦ foo β¦ x β§"]
it "merges EO expressions" $
testCLISucceeded
["merge", "--sweet", resource "number.phi", resource "bytes.phi", resource "string.phi", "--margin=25"]
[ unlines
[ "β¦"
, " org β¦ β¦"
, " eolang β¦ β¦"
, " number(Ο) β¦ β¦β§,"
, " bytes(data) β¦ β¦β§,"
, " string(Ο) β¦ β¦β§,"
, " Ξ» β€ Package"
, " β§,"
, " Ξ» β€ Package"
, " β§"
, "β§"
]
]
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 "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 "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 "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 "prints many substitutions" $
withStdin "[[ x -> Q.x, y -> Q.y ]]" $
testCLISucceeded ["match", "--pattern=Q.!t"] ["t >> x\n------\nt >> y"]
it "builds substitutions with conditions" $
withStdin "[[ x -> Q.y ]].x" $
testCLISucceeded
["match", "--pattern=[[ !t1 -> Q.y, !B1 ]].!t1", "--when=eq(length(!B1),1)"]
["B1 >> β¦ Ο β¦ β
β§\nt1 >> x"]
it "builds with condition from file" $
testCLISucceeded
["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),2)", 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"
)
]
( \(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
)