phino-0.0.140: 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 "--pin-file" $
forM_
[
( "succeeds when --pin-file holds actual version among spaces"
, Just (" \n" ++ showVersion version ++ " \t\n\n")
, testCLISucceeded
, ["⟦⟧"]
)
,
( "fails when --pin-file holds another version"
, Just "7.3.0.41\n"
, testCLIFailed
, ["Version mismatch: --pin requires '7.3.0.41', but this is phino " ++ showVersion version]
)
,
( "fails when --pin-file is empty"
, Just " \n"
, testCLIFailed
, ["Version mismatch: --pin requires ''"]
)
,
( "fails when --pin-file is absent"
, Nothing
, testCLIFailed
, ["does not exist"]
)
]
( \(desc, content, test, expected) ->
it desc $
withTempDirectory "phino-pin-file" $ \dir -> do
createDirectoryIfMissing True dir
let file = dir </> "vérsion.txt"
forM_ content (writeFile file)
withStdin "[[ ]]" (test ["--pin-file=" ++ file, "rewrite", "--sweet"] expected)
)
it "fails when both --pin and --pin-file are given" $
withStdin "[[ ]]" $
testCLIFailed
["--pin=" ++ showVersion version, "--pin-file=pinned-version.txt", "rewrite"]
["[ERROR]"]
describe "--hide-rho" $
forM_
[
( "drops every rho binding from the default salty output"
, "[[ foo -> [[ x -> [[ ]], ^ -> $.y ]], y -> [[ ]] ]]"
, ["rewrite", "--flat", "--hide-rho"]
, ["⟦ foo ↦ ⟦ x ↦ ⟦⟧ ⟧, y ↦ ⟦⟧ ⟧"]
)
,
( "also drops the rho that --sweet leaves behind"
, "[[ foo -> [[ x -> [[ ]], ^ -> $.y ]], y -> [[ ]] ]]"
, ["rewrite", "--flat", "--sweet", "--hide-rho"]
, ["⟦ foo ↦ ⟦⟧:x, y ↦ ⟦⟧ ⟧"]
)
,
( "keeps sweet numeric literals intact"
, "[[ a -> 42 ]]"
, ["rewrite", "--flat", "--sweet", "--hide-rho"]
, ["42:a"]
)
]
(\(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"]
)
]
(\(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"]
["5:x"]
it "defaults --seed to 0 in help" $
testCLISucceeded
["rewrite", "--help"]
["default: 0"]
it "reproduces the same shuffle order for the same --seed" $ do
let args =
[ "rewrite"
, "--shuffle"
, "--seed=42"
, "--sweet"
, "--sequence"
, "--max-depth=1"
, "--max-cycles=1"
, rule "swap-a.yaml"
, rule "swap-b.yaml"
]
(firstRun, _) <- withStdin "[[ x -> 5 ]]" $ withStdout (runCLI args)
(secondRun, _) <- withStdin "[[ x -> 5 ]]" $ withStdout (runCLI args)
firstRun `shouldBe` secondRun
it "fails with a non-integer --seed" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--seed=abc"]
["[ERROR]"]
it "saves steps to dir with --steps-dir" $
withTempDirectory "phino-steps" $ \dir ->
withStdin "[[ x -> \"hello\"]]" $ do
testCLISucceeded
["rewrite", rule "infinite.yaml", "--max-cycles=2", "--max-depth=2", "--steps-dir=" ++ dir, "--sweet"]
["hello_hi_hi"]
doesDirectoryExist dir `shouldReturn` True
files <- listDirectory dir
length files `shouldBe` 4
doesFileExist (dir ++ "/00001.phi") `shouldReturn` True
doesFileExist (dir ++ "/00003.phi") `shouldReturn` True
it "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-:Δ, j ↦ FF-:Δ ⟧"]
it "normalizes from stdin" $
withStdin "⟦ a ↦ ⟦ b ↦ ∅ ⟧ (b ↦ [[ ]]) ⟧" $
testCLISucceeded
["rewrite", "--normalize", "--margin=20"]
["⟦ a ↦ ⟦ b ↦ ⟦⟧ ⟧ ⟧"]
it "rewrites with --sweet flag" $
withStdin "[[ x -> 5]]" $
testCLISucceeded
["rewrite", "--sweet"]
["5:x"]
it "rewrites as XMIR" $
withStdin "[[ x -> Q.y ]]" $
testCLISucceeded
["rewrite", "--output=xmir"]
["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<object", " <o base=\"Φ.y\" name=\"x\"/>"]
it "emits a real revision and ms in XMIR" $ do
(output, _) <- withStdin "[[ x -> Q.y ]]" $ withStdout (runCLI ["rewrite", "--output=xmir"])
let attrValue :: String -> String -> String
attrValue name text =
let needle = name ++ "=\""
breakOn :: String -> Maybe String
breakOn haystack
| needle `isPrefixOf` haystack = Just (drop (length needle) haystack)
| null haystack = Nothing
| otherwise = breakOn (drop 1 haystack)
in case breakOn text of
Just afterNeedle -> takeWhile (/= '"') afterNeedle
Nothing -> ""
revision = attrValue "revision" output
ms = attrValue "ms" output
revision `shouldSatisfy` (\sha -> length sha == 7 && all (`elem` "0123456789abcdef") sha)
revision `shouldNotBe` "1234567"
ms `shouldSatisfy` (all isDigit)
it "rewrites as LaTeX" $
withStdin "[[ x_o -> Q.z(y -> 5), q$ -> T, w -> $, ^ -> Q, @ -> 1, y -> \"H$@^M\", L> Fu_nc ]]" $
testCLISucceeded
["rewrite", "--output=latex", "--sweet"]
[ unlines
[ "\\begin{phiquation}"
, "[["
, " |x\\char95{}o| -> Q . |z| ( |y| -> 5 ),"
, " |q\\char36{}| -> T,"
, " |w| -> \\phiTerminal{\\xi},"
, " \\phiTerminal{\\rho} -> Q,"
, " @ -> 1,"
, " |y| -> \"H$@^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"]
["Φ.number:x:app"]
it "rewrites and prints with XMIR as input and output" $
withStdin
( intercalate
""
[ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<object><o name=\"app\"><o name=\"x\" base=\"Φ.number\"/></o></object>"
]
)
( testCLISucceeded
["rewrite", "--input=xmir", "--output=xmir", "--sweet"]
[ "<?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"]
["\"bar\":x"]
it "prints many expressions with --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
[ "rewrite"
, rule "first.yaml"
, rule "second.yaml"
, "--max-depth=1"
, "--max-cycles=2"
, "--sequence"
, "--sweet"
, "--flat"
]
[ unlines
[ "\"foo\":x"
, "Φ.x( y ↦ \"foo\" )"
, "\"foo\":x"
]
]
it "prefixes every step with a header when --headers is on" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
[ "rewrite"
, rule "first.yaml"
, rule "second.yaml"
, "--max-depth=1"
, "--max-cycles=2"
, "--sequence"
, "--headers"
, "--sweet"
, "--flat"
]
[ intercalate
"\n"
[ ""
, "=== Step #1"
, "\"foo\":x"
, ""
, "=== Step #2, Rule 'first', 23t -> 26t"
, "Φ.x( y ↦ \"foo\" )"
, ""
, "=== Step #3, Rule 'second', 26t -> 23t"
, "\"foo\":x"
]
]
it "ignores --headers without --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--headers", "--sweet", "--flat"]
["\"bar\":x"]
it "emits step headers as LaTeX comments with --headers" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
[ "rewrite"
, rule "first.yaml"
, rule "second.yaml"
, "--max-depth=1"
, "--max-cycles=2"
, "--sequence"
, "--headers"
, "--sweet"
, "--flat"
, "--output=latex"
]
[ unlines
[ "\\begin{phiquation}"
, "% === Step #1"
, "[[ |x| -> \"foo\" ]] \\leadsto_{\\nameref{r:first}}"
, "% === Step #2, Rule 'first', 23t -> 26t"
, " \\leadsto Q . |x| ( |y| -> \"foo\" ) \\leadsto_{\\nameref{r:second}}"
, "% === Step #3, Rule 'second', 26t -> 23t"
, " \\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| -> [[ D> |42-| ]] ) . |y| \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto \\phinoMeet{foo:1}{ [[ |x| -> [[ D> |42-| ]], |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto [[ |x| -> [[ D> |42-| ]] ]] . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |42-| ]] ]], \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:skip}}"
, " \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{foo:1} ) \\leadsto_{\\nameref{r:skip}}"
, " \\leadsto [[ D> |42-| ]]{.}"
, "\\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| -> [[ D> |42-| ]] ) . |y| \\leadsto_{\\nameref{r:copy}}"
, " \\leadsto \\phinoMeet{1}{ [[ |x| -> [[ D> |42-| ]], |y| -> |x| ]] } . |y| \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto [[ |x| -> [[ D> |42-| ]] ]] . |x| ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:dot}}"
, " \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |42-| ]] ]], \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:skip}}"
, " \\leadsto [[ D> |42-| ]] ( \\phiTerminal{\\rho} -> \\phinoAgain{1} ) \\leadsto_{\\nameref{r:skip}}"
, " \\leadsto [[ D> |42-| ]]{.}"
, "\\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
[ "⟦ y ↦ ∅, k ↦ 42:t ⟧( y ↦ 42:t ):x.i"
, "⟦ y ↦ 42:t, k ↦ 42:t ⟧:x.i"
, "⊥"
]
]
it "prints input as listing in XMIR" $
withStdin "[[ app -> [[]] ]]" $
testCLISucceeded
["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat"]
[" <listing>[[ app -> [[]] ]]</listing>"]
it "print expression in listing in XMIRs with --sequence" $
withStdin "[[ x -> \"foo\" ]]" $
testCLISucceeded
["rewrite", "--output=xmir", "--omit-comments", "--sweet", "--flat", "--sequence", rule "simple.yaml"]
[" <listing>\"foo\":x</listing>", " <listing>\"bar\":x</listing>"]
describe "must range tests" $ do
describe "fails" $ do
it "when cycles exceed range ..1" $
withStdin "[[ x -> [[ y -> 5 ]].y ]].x" $
testCLIFailed
["rewrite", "--max-depth=1", "--max-cycles=2", "--normalize", "--must=..1"]
["it's expected rewriting cycles to be in range [..1], but rewriting has already reached 2"]
it "when cycles below range 2.." $
withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $
testCLIFailed
["rewrite", rule "simple.yaml", "--must=2.."]
["it's expected rewriting cycles to be in range [2..], but rewriting stopped after 1"]
it "with invalid range 5..3" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--must=5..3"]
["cannot parse value `5..3'"]
it "with negative in range -1..5" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--must=-1..5"]
["cannot parse value `-1..5'"]
it "with malformed range syntax" $
withStdin "[[ ]]" $
testCLIFailed
["rewrite", "--must=3...5"]
["cannot parse value `3...5'"]
it "accepts range ..5 (0 to 5 cycles)" $
withStdin "[[ ]]" $
testCLISucceeded ["rewrite", "--must=..5", "--sweet"] ["⟦⟧"]
it "accepts range 0..0 (exactly 0 cycles)" $
withStdin "[[ ]]" $
testCLISucceeded ["rewrite", "--must=0..0", "--sweet"] ["⟦⟧"]
it "accepts range 1..1 (exactly 1 cycle)" $
withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--must=1..1", "--sweet"]
["\"bar\":x"]
it "accepts range 1..3 when 1 cycle happens" $
withStdin "⟦ t ↦ ⟦ x ↦ \"foo\" ⟧ ⟧" $
testCLISucceeded
["rewrite", rule "simple.yaml", "--must=1..3", "--sweet"]
["\"bar\":x"]
it "accepts range 0.. (0 or more)" $
withStdin "[[ ]]" $
testCLISucceeded ["rewrite", "--must=0..", "--sweet"] ["⟦⟧"]
it "prints to target file" $
withStdin "[[ ]]" $
withTempFile "targetXXXXXX.tmp" $ \(path, h) -> do
hClose h
testCLISucceeded ["rewrite", "--sweet", printf "--target=%s" path] []
content <- readFile path
content `shouldBe` "⟦⟧"
it "modifies file in-place" $
withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
hPutStr h "[[ x -> \"foo\" ]]"
hClose h
testCLISucceeded ["rewrite", rule "simple.yaml", "--in-place", "--sweet", path] []
content <- readFile path
content `shouldBe` "\"bar\":x"
it "skips rewriting with --update when target is newer than source" $
withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
now <- getCurrentTime
setModificationTime src (addUTCTime (-60) now)
setModificationTime tgt now
testCLISucceeded
["rewrite", rule "simple.yaml", "--update", "--sweet", "--target=" ++ tgt, src]
[]
content <- readFile tgt
content `shouldBe` "ORIGINAL"
it "logs the skip reason at debug level when --update finds a newer target" $
withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
now <- getCurrentTime
setModificationTime src (addUTCTime (-60) now)
setModificationTime tgt now
testCLISucceeded
["rewrite", rule "simple.yaml", "--update", "--sweet", "--log-level=DEBUG", "--target=" ++ tgt, src]
["is newer than source", "skipping rewriting (--update)"]
it "logs progress at debug level when printing to --target" $
withStdin "[[ ]]" $
withTempFile "targetXXXXXX.tmp" $ \(path, h) -> do
hClose h
testCLISucceeded
["rewrite", "--sweet", "--log-level=DEBUG", printf "--target=%s" path]
["The option '--target' is specified, printing to", "The command result was saved in"]
it "logs progress at debug level when modifying a file in-place" $
withTempFile "inplaceXXXXXX.phi" $ \(path, h) -> do
hPutStr h "[[ x -> \"foo\" ]]"
hClose h
testCLISucceeded
["rewrite", rule "simple.yaml", "--in-place", "--sweet", "--log-level=DEBUG", path]
["The option '--in-place' is specified, writing back to", "was modified in-place"]
it "rewrites with --update when source is newer than target" $
withTempFileContent "src-XXXXXX.phi" "[[ x -> \"foo\" ]]" $ \src ->
withTempFileContent "tgt-XXXXXX.phi" "ORIGINAL" $ \tgt -> do
now <- getCurrentTime
setModificationTime tgt (addUTCTime (-60) now)
setModificationTime src now
testCLISucceeded
["rewrite", rule "simple.yaml", "--update", "--sweet", "--target=" ++ tgt, src]
[]
content <- readFile tgt
content `shouldBe` "\"bar\":x"
it "rewrites with cycles" $
withStdin "[[ x -> \"x\" ]]" $
testCLISucceeded
["rewrite", "--sweet", rule "infinite.yaml", "--max-depth=1", "--max-cycles=2"]
["\"x_hi_hi\":x"]
it "hides default package" $
withStdin "[[ org -> [[ eolang -> [[ number -> [[]] ]]]], x -> 42 ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--hide=Q.org"]
["42:x"]
it "hides several FQNs" $
withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--hide=Q.org.eolang", "--hide=Q.org.yegor256"]
["⟦ org ↦ ⟦⟧, x ↦ 42 ⟧"]
it "shows and hides" $
withStdin "[[ org -> [[ eolang -> Q.x, yegor256 -> Q.y ]], x -> 42 ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--show=Q.org", "--hide=Q.org.eolang"]
["Φ.y:yegor256:org"]
it "prints in line with --flat" $
withStdin "[[ x -> 5, y -> \"hey\", z -> [[ w -> [[ ]] ]] ]]" $
testCLISucceeded
["rewrite", "--sweet", "--flat"]
["⟦ x ↦ 5, y ↦ \"hey\", z ↦ ⟦⟧:w ⟧"]
it "removes unnecessary rho bindings in primitive applications" $
withStdin
( unlines
[ "[["
, " z -> [[ x -> [[ t -> 42 ]].t ]].x,"
, " org -> [[ eolang -> [[ bytes -> [[ data -> ? ]], number -> [[ as-bytes -> ? ]] ]] ]]"
, "]]"
]
)
( testCLISucceeded
["rewrite", "--sweet", "--normalize", "--flat"]
["⟦ z ↦ 42, org ↦ ⟦ bytes(data) ↦ ⟦⟧, number(as-bytes) ↦ ⟦⟧ ⟧:eolang ⟧"]
)
it "reduces log message" $
withStdin "[[ x -> [[ y -> ? ]](y -> 5) ]]" $
testCLISucceeded
["rewrite", "--log-level=debug", "--log-lines=1", "--normalize"]
[ intercalate
"\n"
[ "[DEBUG]: Applied 'copy' (32 nodes -> 27 nodes)"
, "---| log is limited by --log-lines=1 option |---"
]
]
-- '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 ↦ 5:x, abc ↦ ∅:x( x ↦ 5 ) ⟧"]
it "returns original expression on --breakpoint" $
withStdin "[[ x -> ?, y -> $.x ]](x -> [[ D> 42- ]]).y" $
testCLISucceeded
["rewrite", "--sweet", "--flat", "--normalize", "--breakpoint=stop", "--log-level=debug"]
[ "Applied 'copy' (22 nodes -> 17 nodes)"
, "Rule 'stop' is a breakpoint, dropping down all the previous rewritings..."
, "⟦ x ↦ ∅, y ↦ x ⟧( x ↦ 42-:Δ ).y"
]
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:skip}}"
, " \\leadsto [[ 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 := 𝜎1:λ:z # 𝑛"
, " 𝑛.1.2 := 𝜎1:λ:z # 𝕄(𝑛.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\">𝜎1:λ:z</built>"
, " <answer meta=\"𝑛.1.2\">𝜎1:λ:z</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>"
]
-- A 'join' line one side of which is ⊥ joins nothing: the program
-- raises on that side of the condition, so the markup names the
-- symbol the condition was dataized to and the side that raises, and
-- the meta is bound to the other side as it stands (#1405)
it "writes on which side of the condition a fork raises" $
withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do
hClose stream
withLambdasOf (T.pack "- λ: L_fork\n dataize:\n 𝛿1: $.c\n morph:\n 𝑛1: $.a\n 𝑛2: $.b\n join:\n 𝑛3: [𝑛1, 𝑛2]\n 𝑛: 𝑛3\n") $ \forks ->
withStdin "⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ⟧, b ↦ ⊥, λ ⤍ L_fork ⟧.φ ⟧" $
testCLISucceeded ["morph", "--symbolic=" ++ forks, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []
records <- readUtf8 path
lines records
`shouldBe` [ "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
, "<morph locator=\"Φ.y\">"
, " <evaluate λ=\"L_fork\" id=\"1\" judgment=\"morph\" locator=\"Φ.y\">"
, " <dataize meta=\"𝛿1.1\">𝜎1:λ</dataize>"
, " <bind meta=\"𝑛1.1\">𝜎2:λ:φ</bind>"
, " <bind meta=\"𝑛2.1\">⊥</bind>"
, " <raise-if symbol=\"𝜎1\" branch=\"right\"/>"
, " <bind meta=\"𝑛3.1\">𝜎2:λ:φ</bind>"
, " <built meta=\"𝑛.1.1\">𝜎2:λ:φ</built>"
, " <answer meta=\"𝑛.1.2\">𝜎2:λ:φ</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\">01-:Δ:z</built>"
, " <answer meta=\"𝑛.1.2\">01-:Δ:z</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\">⟦ ρ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, times ↦ ⟦ ρ ↦ ∅, x ↦ ∅, λ ⤍ L_number_times ⟧, nope ↦ ⟦ ρ ↦ ∅, λ ⤍ L_number_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 ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( ⟦ φ ↦ 𝜎2:λ, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧ ) ⟧:foo"
]
it "keeps a binding whose spine got stuck with --partial" $
withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $
testCLISucceeded
["morph", "--deep", "--partial", "--sweet", "--hide-rho", "--flat"]
["Sym_arg_0:λ.foo:x"]
it "fails on that same spine without --partial" $
withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $
testCLIFailed ["morph", "--deep"] ["No entry of --symbolic answers the λ function 'Sym_arg_0'"]
-- 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 \\;\\text{and}\\; \\lparen [ L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\;\\text{or}\\; [ D ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\rparen }"
, " { \\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 \\;\\text{and}\\; \\lparen [ L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\;\\text{or}\\; [ D ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset \\rparen }"
, " { \\phinoContextualize{ n }{ [[ B_1, B_2 ]] }{ e_2 } }"
, "\\phinoNormalizationRule{miss}"
, " { [[ B ]] ( \\tau -> e ) }"
, " { T }"
, " { \\tau \\notin B \\;\\text{and}\\; \\tau \\not= \\phiTerminal{\\rho} }"
, " { }"
, "\\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{skip}"
, " { [[ B ]] ( \\phiTerminal{\\rho} -> e ) }"
, " { [[ B ]] }"
, " { \\phiTerminal{\\rho} \\notin B }"
, " { }"
, "\\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"]
["x:foo"]
it "merges EO expressions" $
testCLISucceeded
["merge", "--sweet", resource "number.phi", resource "bytes.phi", resource "string.phi", "--margin=25"]
[ unlines
[ "⟦"
, " eolang ↦ ⟦"
, " number(φ) ↦ ⟦⟧,"
, " bytes(data) ↦ ⟦⟧,"
, " string(φ) ↦ ⟦⟧,"
, " λ ⤍ Package"
, " ⟧,"
, " λ ⤍ Package"
, "⟧:org"
]
]
it "fails on merging non formations" $
testCLIFailed
["merge", resource "dispatch.phi", resource "number.phi"]
["Invalid expression format, only expressions with top level formations are supported for 'merge' command"]
it "fails on merging conflicted bindings" $
testCLIFailed
["merge", resource "foo.phi", resource "desugar.phi"]
["Can't merge two bindings, conflict found"]
it "fails on merging empty list of expressions" $
testCLIFailed
["merge"]
["At least one input file must be specified for 'merge' command"]
it "merges and prints as XMIR, with the listing rendered from the merged expression" $
testCLISucceeded
["merge", resource "desugar.phi", "--output=xmir"]
["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<listing>⟦ foo ↦ ξ.x ⟧</listing>", "<o base=\"ξ.x\" name=\"foo\"/>"]
-- The @atom of an EO atom is its result type, not the name of its λ
-- function, so the merged 𝜑 names the function after its locator and
-- the XMIR printed back restores the type (#1389)
it "names an atom of XMIR after its locator and keeps its type" $ do
let xmir = "<object><o name=\"number\"><o name=\"plus\"><o base=\"∅\" name=\"b\"/><o atom=\"Φ.number\" name=\"λ\"/></o></o></object>"
withTempFileContent "phino-atom.xmir" xmir $ \file -> do
testCLISucceeded
["merge", "--input=xmir", "--sweet", "--flat", file]
["λ ⤍ L_number_plus"]
testCLISucceeded
["merge", "--input=xmir", "--output=xmir", file]
["<o atom=\"Φ.number\" name=\"λ\">L_number_plus</o>"]
it "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),0)"]
["B1 >> ⟦⟧\nt1 >> x"]
it "builds with condition from file" $
testCLISucceeded
["match", "--pattern=[[ !B1 ]]", "--when=eq(length(!B1),1)", resource "foo.phi"]
["B1 >> ⟦ foo ↦ Φ.org.eolang.x ⟧"]
it "rejects an anonymous meta in --when" $
withStdin "[[ x -> Q.y ]]" $
testCLIFailed
["match", "--pattern=[[ !B ]]", "--when=eq(length(!B),1)"]
["[ERROR]: Anonymous meta '!B' cannot be referenced in --when"]
it "fails on parsing --when condition" $
withStdin "[[]]" $
testCLIFailed
["match", "--pattern=[[!B]]", "--when=hello"]
["[ERROR]: Couldn't parse given condition"]
it "fails on empty substitutions" $
withStdin "Q.x.y" $
testCLIFailed
["match", "--pattern=$.!t"]
["[ERROR]"]
describe "CmdException Show instance" $
forM_
[ ("InvalidCLIArguments", InvalidCLIArguments "bad flag", "Invalid set of arguments: bad flag")
, ("CouldNotReadFromStdin", CouldNotReadFromStdin "broken pipe", "Could not read input from stdin\nReason: broken pipe")
, ("CouldNotDataize", CouldNotDataize, "Could not dataize given expression")
,
( "CouldNotPrintExpressionInXMIR"
, CouldNotPrintExpressionInXMIR
, "Could not print expression with --output=xmir, only expression printing is allowed"
)
, ("EmptySubstsOnMatch", EmptySubstsOnMatch, "Provided pattern was not matched, no substitutions are built")
,
( "VersionMismatch"
, VersionMismatch "1.2.3" "4.5.6"
, "Version mismatch: --pin requires '1.2.3', but this is phino 4.5.6"
)
]
( \(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
)