diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -289,9 +289,9 @@ ## Protocol The `--protocol` option writes every λ function the run fired into a file, -as a tree. -A file whose name ends in `.xml` gets the tree as XML, for a program to read, -and any other name gets indented text. +as a tree in XML, for a program to read. +The `--minutes` option writes the same tree as indented text, and one run +may take both. Here, `L_down` answers with a call of its own object over a fresh symbol, so without `--acyclic` the run would go on until `--max-steps` runs out: @@ -307,7 +307,7 @@ y ↦ Φ.down( x ↦ ⟦ λ ⤍ 𝜎1 ⟧ ).φ ⟧ $ phino morph --symbolic=down.yaml --locator=Q.y --acyclic=proven \ - --protocol=down.txt --sweet --hide-rho down.phi + --minutes=down.txt --sweet --hide-rho down.phi ⟦ x ↦ 𝜎1:λ, λ ⤍ L_down ⟧.φ $ cat down.txt 𝕄(Φ.y): diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino -version: 0.0.162 +version: 0.0.163 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/CLI/Helpers.hs b/src/CLI/Helpers.hs --- a/src/CLI/Helpers.hs +++ b/src/CLI/Helpers.hs @@ -17,7 +17,7 @@ import Control.Exception import Control.Monad (mfilter, when, (>=>)) import qualified Data.ByteString as BS -import Data.Char (isDigit, toLower) +import Data.Char (isDigit) import Data.Functor ((<&>)) import Data.IORef import Data.List (intercalate, nub) @@ -48,7 +48,7 @@ import Rewriter (Rewrittens', stepHeaders) import Sugar (SugarType (SALTY), withoutRho) import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, listDirectory, removeFile) -import System.FilePath (splitExtension, takeDirectory, takeExtension, ()) +import System.FilePath (splitExtension, takeDirectory, ()) import System.IO (Handle, IOMode (WriteMode), getContents', hClose, hSetEncoding, openFile, utf8) import Text.Printf (printf) import XMIR (Atoms, expressionToXMIR, gitRevision, parseXMIRThrows, printXMIR, renameAtoms, xmirAtoms, xmirToPhi) @@ -96,8 +96,8 @@ saveStep stepsDir ioToExt render step expr pure save -withEvalFunc :: forall a. Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a -withEvalFunc target ctx action = withEvalFunc' target ctx (tracked >=> action) +withEvalFunc :: forall a. Maybe FilePath -> Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a +withEvalFunc xml text ctx action = withEvalFunc' xml text ctx (tracked >=> action) where tracked :: SaveEvalFunc -> IO SaveEvalFunc tracked record = do @@ -108,29 +108,29 @@ pure (progressed cursor 5 (flattened ctx) record) else pure record -withEvalFunc' :: forall a. Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a -withEvalFunc' Nothing _ action = action dontSaveEval -withEvalFunc' (Just file) ctx action = do - createDirectoryIfMissing True (takeDirectory file) - logDebug (printf "The option '--protocol' is specified, every firing will be recorded in '%s' as %s" file (if markup then "XML" else "text")) - if markup then markedUp else plain +withEvalFunc' :: forall a. Maybe FilePath -> Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a +withEvalFunc' xml text ctx action = + markedUp xml (\marked -> plain text (\lined -> action (\record -> marked record >> lined record))) where - markup :: Bool - markup = map toLower (takeExtension file) == ".xml" - markedUp :: IO a - markedUp = do + markedUp :: Maybe FilePath -> (SaveEvalFunc -> IO a) -> IO a + markedUp Nothing go = go dontSaveEval + markedUp (Just file) go = do + logDebug (printf "The option '--protocol' is specified, every firing will be recorded in '%s' as XML" file) cursor <- newIORef emptyNesting began <- getMonotonicTime - bracket opened (\protocol -> endEvalXml protocol cursor began `finally` hClose protocol) $ \protocol -> - action (saveEvalXml protocol cursor (flattened ctx)) - plain :: IO a - plain = do + bracket (opened file) (\protocol -> endEvalXml protocol cursor began `finally` hClose protocol) $ \protocol -> + go (saveEvalXml protocol cursor (flattened ctx)) + plain :: Maybe FilePath -> (SaveEvalFunc -> IO a) -> IO a + plain Nothing go = go dontSaveEval + plain (Just file) go = do + logDebug (printf "The option '--minutes' is specified, every firing will be recorded in '%s' as text" file) cursor <- newIORef emptyProtocol began <- getMonotonicTime - bracket opened (\protocol -> endEval protocol cursor began `finally` hClose protocol) $ \protocol -> - action (saveEval protocol cursor (flattened ctx) (salted ctx)) - opened :: IO Handle - opened = do + bracket (opened file) (\protocol -> endEval protocol cursor began `finally` hClose protocol) $ \protocol -> + go (saveEval protocol cursor (flattened ctx) (salted ctx)) + opened :: FilePath -> IO Handle + opened file = do + createDirectoryIfMissing True (takeDirectory file) protocol <- openFile file WriteMode hSetEncoding protocol utf8 pure protocol diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -318,13 +318,24 @@ ( long "protocol" <> metavar "FILE" <> help - "File to record every λ function fired during the run: the run at the top, one block per firing \ - \under it, and inside each block the operands it bound and the term it answered with, with a \ - \firing nested in the reduction of an operand one level deeper again. The name of the file \ - \decides the format: '.xml' writes XML, every other name writes the same tree as indented text" + "File to record every λ function fired during the run as XML, for a program to read: the run at \ + \the top, one block per firing under it, and inside each block the operands it bound and the term \ + \it answered with, with a firing nested in the reduction of an operand one level deeper again" ) ) +optMinutes :: Parser (Maybe FilePath) +optMinutes = + optional + ( strOption + ( long "minutes" + <> metavar "FILE" + <> help + "File to record the same tree as --protocol does, as indented text for a person to read; \ + \given together with --protocol, one run writes both files" + ) + ) + optAbridged :: Parser (Maybe Int) optAbridged = optional @@ -332,9 +343,9 @@ 64 ( long "abridged" <> help - "Shorten every 𝜑-expression written to the --protocol file: a formation longer than the width \ - \keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', while every byte string \ - \it writes stays whole; the width is 64 characters unless given as --abridged=WIDTH" + "Shorten every 𝜑-expression written to the --protocol and --minutes files: a formation longer \ + \than the width keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', while \ + \every byte string it writes stays whole; the width is 64 characters unless given as --abridged=WIDTH" ) <|> option (boundedIntOption >>= validateIntOption (> 0) "--abridged must be positive") @@ -464,6 +475,7 @@ <*> optInside <*> optStepsDir <*> optProtocol + <*> optMinutes <*> optAbridged <*> optAbridgedData <*> optSymbolic @@ -516,6 +528,7 @@ <*> optInside <*> optStepsDir <*> optProtocol + <*> optMinutes <*> optAbridged <*> optAbridgedData <*> optSymbolic diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -189,6 +189,7 @@ ((outcome, chain, _), universe, aim) <- withEvalFunc _protocol + _minutes printCtx ( \record -> do let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles _maxNodes _maxMemory (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Dataization, loc)) _depthSensitive _shuffle _partial _acyclic _maxLoops Dataization [] Map.empty (Just facts) lambdas [] False (building linked) reduction evaluation save record linked @@ -215,7 +216,7 @@ [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")] validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus when (length _show > 1) (invalidCLIArguments "The option --show can be used only once") - when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged") + when (isJust _abridged && isNothing _protocol && isNothing _minutes) (invalidCLIArguments "The option --abridged requires --protocol or --minutes, since only the protocol is abridged") when (_abridgedData && isNothing _abridged) (invalidCLIArguments "The option --abridged-data requires --abridged, since only an abridged protocol cuts its data") when (_maxLoops > 0 && isNothing _acyclic) (invalidCLIArguments "The option --max-loops requires --acyclic, since only --acyclic cuts a loop") when (isJust _inside) $ do @@ -275,6 +276,7 @@ ((morphed, chain, _), universe, aim) <- withEvalFunc _protocol + _minutes printCtx ( \record -> do let ctx = ReduceContext loc loc Nothing _maxDepth _maxCycles _maxNodes _maxMemory (Steps _maxSteps 0) tally minted deadline memo 1 (Just (1, Morphing, loc)) _depthSensitive _shuffle _partial _acyclic _maxLoops Morphing [] Map.empty (Just facts) lambdas [] False (building linked) reduction evaluation save record linked @@ -307,7 +309,7 @@ [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")] validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus when (length _show > 1) (invalidCLIArguments "The option --show can be used only once") - when (isJust _abridged && isNothing _protocol) (invalidCLIArguments "The option --abridged requires --protocol, since only the protocol is abridged") + when (isJust _abridged && isNothing _protocol && isNothing _minutes) (invalidCLIArguments "The option --abridged requires --protocol or --minutes, since only the protocol is abridged") when (_abridgedData && isNothing _abridged) (invalidCLIArguments "The option --abridged-data requires --abridged, since only an abridged protocol cuts its data") when (_maxLoops > 0 && isNothing _acyclic) (invalidCLIArguments "The option --max-loops requires --acyclic, since only --acyclic cuts a loop") when (isJust _inside) $ do diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -134,6 +134,7 @@ , _inside :: Maybe String , _stepsDir :: Maybe FilePath , _protocol :: Maybe FilePath + , _minutes :: Maybe FilePath , _abridged :: Maybe Int , _abridgedData :: Bool , _symbolic :: Maybe FilePath @@ -183,6 +184,7 @@ , _inside :: Maybe String , _stepsDir :: Maybe FilePath , _protocol :: Maybe FilePath + , _minutes :: Maybe FilePath , _abridged :: Maybe Int , _abridgedData :: Bool , _symbolic :: Maybe FilePath diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -18,7 +18,7 @@ import Data.Time.Clock.POSIX (getPOSIXTime) import Data.Version (showVersion) import Files (allPathsIn) -import Fixtures (explainPack, lambdasFile, loopingLambdas, readProtocol, readUtf8, withLambdasOf) +import Fixtures (explainPack, lambdasFile, loopingLambdas, readProtocol, readUtf8, recording, withLambdasOf) import GHC.IO.Encoding (TextEncoding (textEncodingName), getFileSystemEncoding) import GHC.IO.Handle import Paths_phino (version) @@ -1513,7 +1513,7 @@ hClose stream withStdin circling $ testCLISucceeded - ["dataize", "--locator=Q.t", "--acyclic=proven", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"] + ["dataize", "--locator=Q.t", "--acyclic=proven", "--partial", "--minutes=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"] [] records <- readProtocol path lines records @@ -1578,7 +1578,7 @@ hClose stream withStdin circling $ testCLISucceeded - ["dataize", "--locator=Q.t", "--acyclic=plausible", "--partial", "--protocol=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"] + ["dataize", "--locator=Q.t", "--acyclic=plausible", "--partial", "--minutes=" ++ path, "--sweet", "--hide-rho", "--flat", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [" looped 𝜎1 := Φ.cyc( x ↦ 𝑛·0·9 ) # 𝔻(𝑛·0·5), plausible, repeats 𝑛·0·8"] @@ -1631,7 +1631,7 @@ withLambdasOf calling $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", recording path, "--quiet", "--sweet", "--hide-rho"] [] lines <$> readProtocol path it "answers the recursive call it cuts with a fresh symbol and goes on" $ @@ -1655,7 +1655,7 @@ withLambdasOf forking $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-loops=" ++ loops, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=plausible", "--max-loops=" ++ loops, recording path, "--quiet", "--sweet", "--hide-rho"] [] lines <$> readProtocol path it "answers the copy a side of a fork makes again with a fresh symbol and joins" $ @@ -1682,7 +1682,7 @@ withLambdasOf forking $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", recording path, "--quiet", "--sweet", "--hide-rho"] [] lines <$> readProtocol path it "answers the copy holding a λ it cuts with a fresh symbol and goes on" $ @@ -1711,7 +1711,7 @@ withLambdasOf forking $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", recording path, "--quiet", "--sweet", "--hide-rho"] [] lines <$> readProtocol path it "writes the copy it cuts to the protocol as a call of the object with the attribute it ends with" $ @@ -1734,7 +1734,7 @@ withLambdasOf atoms $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--max-seconds=30", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--max-seconds=30", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path filter (isInfixOf "looped") (lines records) `shouldBe` [" looped 𝜎1 := Φ.dataized( target ↦ Φ.x ) # 𝔼(𝑛·6·2.b), plausible, repeats 𝑛·6·5", " looped 𝜎2 := Φ.times( b ↦ 𝜎1:λ ) # plausible, repeats 𝑛·6·2"] @@ -1746,7 +1746,7 @@ withLambdasOf (T.pack "- λ: L_times\n terminators: [L_throw]\n dataize:\n 𝛿1: $.b\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n- λ: L_dataized\n terminators: [L_throw]\n dataize:\n 𝛿1: $.target\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \file -> withStdin "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, throw(message) ↦ ⟦ λ ⤍ L_throw ⟧, times(b, c) ↦ ⟦ λ ⤍ L_times ⟧, x ↦ Φ.times( Φ.dataized( Φ.x ), Φ.throw( 𝜎1:λ ) ) ⟧" $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--max-seconds=30", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--max-seconds=30", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path filter (isInfixOf "looped 𝜎3") (lines records) `shouldBe` [" looped 𝜎3 := Φ.times( b ↦ 𝜎2:λ, c ↦ 𝑛·6·11 ) # plausible, repeats 𝑛·6·4"] @@ -1761,7 +1761,7 @@ withLambdasOf forking $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] lines <$> readProtocol path it "answers the fork it cuts inside a formation the memo fabricated with a fresh symbol and goes on" $ @@ -1787,7 +1787,7 @@ withLambdasOf forking $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] lines <$> readProtocol path it "answers the fork it cuts with a fresh symbol and goes on" $ @@ -1811,7 +1811,7 @@ withLambdasOf forking $ \file -> withStdin recursive $ testCLISucceeded - ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] + ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] lines <$> readProtocol path it "writes the loop it cuts inside the nested fork by its symbol alone, since no fact names it" $ @@ -1893,7 +1893,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin stuck $ - testCLISucceeded ["dataize", "--locator=Q.t", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] [] + testCLISucceeded ["dataize", "--locator=Q.t", "--partial", "--minutes=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [" unanswered L_weit # 𝔻(⟦ λ ⤍ L_weit, +4 ⟧)"] it "names a long formation in the XML protocol by its path rather than folding it" $ @@ -1913,7 +1913,7 @@ hClose stream withLambdasOf (T.pack "- λ: L_outer\n dataize:\n 𝛿1: ξ.arg\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \outer -> withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ Δ ⤍ 01-02-03-04-05-06-07-08-09-0A-0B-0C ⟧, λ ⤍ L_outer ⟧ ⟧" $ - testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--abridged-data", "--sweet", "--hide-rho", "--quiet"] [] + testCLISucceeded ["dataize", "--symbolic=" ++ outer, "--locator=Q.x", "--partial", recording path, "--abridged", "--abridged-data", "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [line] ) @@ -1927,7 +1927,7 @@ hClose stream withLambdasOf (T.pack "- λ: L_hex\n dataize:\n 𝛿1: ξ.arg\n 𝑛: ⟦ λ ⤍ 𝜎 ⟧\n") $ \hex -> withStdin "⟦ x ↦ ⟦ arg ↦ ⟦ Δ ⤍ 30-31-32-33-34-35-36-37-38-39-41-42-43-44-45-46 ⟧, λ ⤍ L_hex ⟧ ⟧" $ - testCLISucceeded ["dataize", "--symbolic=" ++ hex, "--locator=Q.x", "--partial", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--quiet"] [] + testCLISucceeded ["dataize", "--symbolic=" ++ hex, "--locator=Q.x", "--partial", recording path, "--abridged", "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [line] ) @@ -1935,14 +1935,14 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin stuck $ - testCLISucceeded ["dataize", "--locator=Q.t", "--partial", "--protocol=" ++ path, "--abridged=64", "--sweet", "--hide-rho", "--quiet"] [] + testCLISucceeded ["dataize", "--locator=Q.t", "--partial", "--minutes=" ++ path, "--abridged=64", "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [" unanswered L_weit # 𝔻(⟦ λ ⤍ L_weit, +4 ⟧)"] it "keeps a formation whole under a width it fits in" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin stuck $ - testCLISucceeded ["dataize", "--locator=Q.t", "--partial", "--protocol=" ++ path, "--abridged=200", "--sweet", "--hide-rho", "--quiet"] [] + testCLISucceeded ["dataize", "--locator=Q.t", "--partial", "--minutes=" ++ path, "--abridged=200", "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path lines records `shouldContain` [" unanswered L_weit # 𝔻(⟦ λ ⤍ L_weit, anfang ↦ schluss, mitte ↦ anfang, schluss ↦ mitte, rand ↦ schluss ⟧)"] it "refuses a width that is not a number" $ @@ -1952,7 +1952,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin wide $ - testCLISucceeded ["morph", "--locator=Q.t", "--protocol=" ++ path, "--abridged", "--sweet", "--hide-rho", "--flat"] ["anfang ↦ schluss, mitte ↦ anfang"] + testCLISucceeded ["morph", "--locator=Q.t", "--minutes=" ++ path, "--abridged", "--sweet", "--hide-rho", "--flat"] ["anfang ↦ schluss, mitte ↦ anfang"] it "refuses the flag without a protocol" $ withStdin wide $ testCLIFailed ["dataize", "--locator=Q.t", "--abridged"] ["The option --abridged requires --protocol"] @@ -1972,7 +1972,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "[[ D> 01- ]]" $ - testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", "--minutes=" ++ path, "--quiet"] [] records <- readProtocol path records `shouldBe` "𝔻(Φ):\n 𝛿·0·1 := 01-\n" @@ -1980,7 +1980,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "[[ D> 01- ]]" $ - testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path records `shouldSatisfy` isPrefixOf ("# Written by phino " ++ showVersion version ++ " ") @@ -1988,15 +1988,15 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "[[ D> 01- ]]" $ - testCLISucceeded ["dataize", "--protocol=" ++ takeFileName path, "--quiet"] [] + testCLISucceeded ["dataize", "--minutes=" ++ takeFileName path, "--quiet"] [] records <- readUtf8 path - lines records `shouldContain` ["# Command: phino dataize --protocol=" ++ takeFileName path ++ " --quiet"] + lines records `shouldContain` ["# Command: phino dataize --minutes=" ++ takeFileName path ++ " --quiet"] it "writes the world read from the standard input into the header" $ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "⟦ t ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" $ - testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", "--locator=Q.t", "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path lines records `shouldContain` ["# World: stdin, 1 line, 32 bytes, 1 object at the top, 2 bindings"] @@ -2004,7 +2004,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withTempFileContent "worldXXXXXX.phi" "[[\n t -> [[ D> 01- ]]\n]]\n" $ \world -> do - testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--quiet", world] [] + testCLISucceeded ["dataize", "--locator=Q.t", "--minutes=" ++ path, "--quiet", world] [] records <- readUtf8 path lines records `shouldContain` [printf "# World: %s, 3 lines, 26 bytes, 1 object at the top, 2 bindings" world] @@ -2012,7 +2012,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin sum' $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path lines records `shouldContain` [printf "# Symbolic: %s, 5 entries" lambdasFile] @@ -2020,7 +2020,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "⟦ t ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" $ - testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", "--locator=Q.t", "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path lines records `shouldContain` ["# Locator: Φ.t"] @@ -2028,7 +2028,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "⟦ t ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" $ - testCLISucceeded ["dataize", "--locator=Q.t", "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", "--locator=Q.t", "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path lines records `shouldContain` ["# Expression: ⟦ Δ ⤍ 01- ⟧"] @@ -2036,7 +2036,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "⟦ t ↦ ⟦ Δ ⤍ 01- ⟧ ⟧" $ - testCLISucceeded ["morph", "--inside=Φ.t", "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["morph", "--inside=Φ.t", "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path lines records `shouldContain` ["# Expression: Φ.t"] @@ -2052,7 +2052,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin sum' $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path (lines records !! (length (lines records) - 3)) `shouldSatisfy` isPrefixOf "msec " @@ -2060,7 +2060,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin sum' $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path lines records `shouldContain` ["firings 1"] @@ -2068,7 +2068,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin sum' $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path last (lines records) `shouldSatisfy` isPrefixOf "fps " @@ -2076,7 +2076,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin "[[ D> 01- ]]" $ - testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] [] + testCLISucceeded ["dataize", "--minutes=" ++ path, "--quiet"] [] records <- readUtf8 path lines records `shouldContain` ["firings 0"] @@ -2084,7 +2084,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin sum' $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldBe` [ "𝔻(Φ):" @@ -2137,7 +2137,7 @@ hClose stream withLambdasOf (T.pack "- λ: L_make\n 𝑛: ⟦ φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ) ⟧\n") $ \makes -> withStdin "⟦ bytes ↦ ⟦ φ ↦ ∅ ⟧, make ↦ ⟦ λ ⤍ L_make ⟧, foo ↦ ⟦ φ ↦ Φ.make ⟧, e ↦ Φ.foo ⟧" $ - testCLISucceeded ["dataize", "--symbolic=" ++ makes, "--locator=Q.e", "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", "--symbolic=" ++ makes, "--locator=Q.e", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldBe` [ "𝔻(Φ.e):" @@ -2167,7 +2167,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin chained $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldBe` [ "𝔻(Φ):" @@ -2249,7 +2249,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin mixed $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldBe` [ "𝔻(Φ):" @@ -2331,7 +2331,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin nested $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldBe` [ "𝔻(Φ):" @@ -2434,7 +2434,7 @@ withTempFile template $ \(path, stream) -> do hClose stream withStdin "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧" $ - testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-cycles=7", "--partial", "--locator=Q.x", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-cycles=7", "--partial", "--locator=Q.x", recording path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path any (isPrefixOf record . dropWhile (== ' ')) (lines records) `shouldBe` True @@ -2445,7 +2445,7 @@ withTempFile template $ \(path, stream) -> do hClose stream withStdin "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧" $ - testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-nodes=60", "--partial", "--locator=Q.x", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-nodes=60", "--partial", "--locator=Q.x", recording path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path any (isPrefixOf record . dropWhile (== ' ')) (lines records) `shouldBe` True @@ -2456,7 +2456,7 @@ withTempFile template $ \(path, stream) -> do hClose stream withStdin "⟦ m(p) ↦ ⟦ φ ↦ ξ.a( ξ.p ).φ, a(ρ, tup) ↦ ⟦ φ ↦ ρ.a( ξ.tup.tail ).φ ⟧ ⟧, x ↦ Φ.m( 𝜎1:λ ) ⟧" $ - testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-memory=1K", "--partial", "--locator=Q.x", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", "--acyclic=plausible", "--max-loops=2", "--max-memory=1K", "--partial", "--locator=Q.x", recording path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path any (isPrefixOf record . dropWhile (== ' ')) (lines records) `shouldBe` True @@ -2468,7 +2468,7 @@ hClose stream loopingLambdas $ \endless -> withStdin "⟦ @ ↦ ⟦ λ ⤍ L_loop ⟧ ⟧" $ - testCLIFailed ["dataize", "--symbolic=" ++ endless, "--max-steps=400", "--max-firings=5", "--protocol=" ++ path] ["--max-firings=5"] + testCLIFailed ["dataize", "--symbolic=" ++ endless, "--max-steps=400", "--max-firings=5", recording path] ["--max-firings=5"] records <- readProtocol path any (record `isInfixOf`) (lines records) `shouldBe` True ) @@ -2478,7 +2478,7 @@ 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"] + ["dataize", symbolic, "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] ["No entry of --symbolic answers the λ function 'L_number_nope'"] records <- readProtocol path lines records @@ -2529,7 +2529,7 @@ 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"] [] + testCLISucceeded ["dataize", "--minutes=" ++ path, "--quiet"] [] records <- readProtocol path records `shouldBe` "𝔻(Φ):\n 𝛿·0·1 := 01-\n" @@ -2537,7 +2537,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin sum' $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--output=xmir", "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ path, "--output=xmir", "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path records `shouldEndWith` " 𝕄(𝑛·1·17):\n 𝑛·1·18 := Φ.number( φ ↦ 𝜎1:λ )\n 𝑛·1·19 := ⟦ φ ↦ 𝜎1:λ, plus(x) ↦ L_number_plus:λ ⟧\n morphed 𝑛·1·20 := 𝑛·1·19\n 𝑛·1·21 := 𝑛·1·20 # 𝕄(𝑛·1·17)\n boxed 𝑛·0·7 := 𝑛·1·21.φ\n 𝛿·0·1 := 𝔻(𝜎1:λ)\n" @@ -2547,7 +2547,7 @@ hClose one hClose two withStdin nested $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ text, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ text, "--quiet", "--sweet", "--hide-rho"] [] withStdin nested $ testCLISucceeded ["dataize", symbolic, "--protocol=" ++ xml, "--quiet", "--sweet", "--hide-rho"] [] lined <- readProtocol text @@ -3200,14 +3200,58 @@ , "" ] - it "keeps writing text when the file is named anything else" $ - withTempFile "protocolXXXXXX.xmir" $ \(path, stream) -> do - hClose stream - withStdin sum' $ - testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] - records <- readProtocol path - take 1 (lines records) `shouldBe` ["𝔻(Φ):"] + it "writes XML into a file named .txt" $ + withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "[[ D> 01- ]]" $ + testCLISucceeded ["dataize", "--protocol=" ++ path, "--quiet"] [] + records <- readUtf8 path + records `shouldSatisfy` isPrefixOf " [[ plus(^, x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" + it "writes the indented text into a file named .xml" $ + withTempFile "minutesXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withStdin "[[ D> 01- ]]" $ + testCLISucceeded ["dataize", "--minutes=" ++ path, "--quiet"] [] + records <- readProtocol path + records `shouldBe` "𝔻(Φ):\n 𝛿·0·1 := 01-\n" + + it "writes the same text beside --protocol as alone" $ + withTempFile "minutesXXXXXX.txt" $ \(alone, one) -> + withTempFile "minutesXXXXXX.txt" $ \(beside, two) -> + withTempFile "protocolXXXXXX.xml" $ \(xml, three) -> do + mapM_ hClose [one, two, three] + withStdin sum' $ + testCLISucceeded ["dataize", symbolic, "--minutes=" ++ alone, "--quiet", "--sweet", "--hide-rho"] [] + withStdin sum' $ + testCLISucceeded ["dataize", symbolic, "--protocol=" ++ xml, "--minutes=" ++ beside, "--quiet", "--sweet", "--hide-rho"] [] + first <- readProtocol alone + second <- readProtocol beside + second `shouldBe` first + + it "writes the same XML beside --minutes as alone" $ + withTempFile "protocolXXXXXX.xml" $ \(alone, one) -> + withTempFile "protocolXXXXXX.xml" $ \(beside, two) -> + withTempFile "minutesXXXXXX.txt" $ \(text, three) -> do + mapM_ hClose [one, two, three] + withStdin sum' $ + testCLISucceeded ["dataize", symbolic, "--protocol=" ++ alone, "--quiet", "--sweet", "--hide-rho"] [] + withStdin sum' $ + testCLISucceeded ["dataize", symbolic, "--protocol=" ++ beside, "--minutes=" ++ text, "--quiet", "--sweet", "--hide-rho"] [] + first <- readProtocol alone + second <- readProtocol beside + second `shouldBe` first + + it "abridges the text without --protocol" $ + withTempFile "minutesXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withStdin "[[ D> 01- ]]" $ + testCLISucceeded ["dataize", "--minutes=" ++ path, "--abridged", "--quiet"] [] + records <- readProtocol path + records `shouldBe` "𝔻(Φ):\n 𝛿·0·1 := 01-\n" + 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 ]]" @@ -3234,7 +3278,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin stuck $ - testCLISucceeded ["dataize", symbolic, "--partial", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", symbolic, "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldBe` [ "𝔻(Φ):" @@ -3369,7 +3413,7 @@ hClose stream withLambdasOf joining $ \joins -> withStdin "⟦ y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎1 ⟧, a ↦ ⟦ λ ⤍ 𝜎2 ⟧, b ↦ ⊥, λ ⤍ L_fork ⟧ ⟧" $ - testCLISucceeded ["dataize", "--symbolic=" ++ joins, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["dataize", "--symbolic=" ++ joins, "--locator=Q.y", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldContain` [" joined 𝜎4 := 𝛿1·1 ? 𝜎2 : 𝜎3 # where 𝜎3 is ⊥"] @@ -3395,7 +3439,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin universe $ - testCLISucceeded ["morph", symbolic, "--inside=5.plus( 6 )", "--protocol=" ++ path, "--sweet", "--hide-rho", "--quiet"] [] + testCLISucceeded ["morph", symbolic, "--inside=5.plus( 6 )", "--minutes=" ++ path, "--sweet", "--hide-rho", "--quiet"] [] records <- readProtocol path takeWhile (/= '(') (concat (take 1 (lines records))) `shouldBe` "𝕄" @@ -3411,7 +3455,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin universe $ - testCLISucceeded ["dataize", "--inside=[[ x -> ? ]]( x -> [[ D> 2A- ]] ).x", "--protocol=" ++ path, "--sweet", "--quiet"] [] + testCLISucceeded ["dataize", "--inside=[[ x -> ? ]]( x -> [[ D> 2A- ]] ).x", "--minutes=" ++ path, "--sweet", "--quiet"] [] records <- readProtocol path take 2 (lines records) `shouldBe` ["𝔻(Φ.a🌵0):", " 𝑛·0·1 := ∅:x( x ↦ 2A-:Δ )"] @@ -3596,7 +3640,7 @@ withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do hClose stream withStdin chained $ - testCLISucceeded ["morph", symbolic, "--locator=Q.@", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + testCLISucceeded ["morph", symbolic, "--locator=Q.@", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path lines records `shouldBe` [ "𝕄(Φ.φ):" @@ -3701,7 +3745,7 @@ hClose stream withStdin split $ testCLISucceeded - ["morph", "--symbolic=" ++ table, "--locator=Q.x", "--max-firings=64", "--partial", "--protocol=" ++ path, "--quiet"] + ["morph", "--symbolic=" ++ table, "--locator=Q.x", "--max-firings=64", "--partial", "--minutes=" ++ path, "--quiet"] [] records <- readProtocol path length (filter (isInfixOf "𝔼(L_split)") (lines records)) `shouldBe` 64 @@ -3801,7 +3845,7 @@ bounded $ withStdin rungs $ testCLIFailed - (["morph", "--symbolic=" ++ table, "--max-seconds=1", "--protocol=" ++ path, "--quiet"] ++ opts) + (["morph", "--symbolic=" ++ table, "--max-seconds=1", "--minutes=" ++ path, "--quiet"] ++ opts) ["--max-seconds=1"] records <- readProtocol path dropWhile (== ' ') (last (lines records)) `shouldBe` "timeout 1" @@ -3918,7 +3962,7 @@ withLambdasOf pairs $ \file -> withStdin twins $ testCLISucceeded - ["morph", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=" ++ mode, "--protocol=" ++ path, "--quiet"] + ["morph", "--symbolic=" ++ file, "--locator=Q.t", "--acyclic=" ++ mode, "--minutes=" ++ path, "--quiet"] [] lines <$> readProtocol path it "charges a formation once per argument spelling it under proven" $ @@ -3989,7 +4033,7 @@ hClose stream withStdin "⟦ x ↦ ⟦ λ ⤍ L_loop ⟧.foo ⟧" $ testCLISucceeded - ["morph", "--symbolic=" ++ endless, "--locator=Q.x", "--acyclic=proven", "--max-loops=1", "--protocol=" ++ path, "--quiet"] + ["morph", "--symbolic=" ++ endless, "--locator=Q.x", "--acyclic=proven", "--max-loops=1", "--minutes=" ++ path, "--quiet"] [] records <- readProtocol path length (filter (isInfixOf "𝔼(L_loop)") (lines records)) `shouldBe` 2 diff --git a/test/Fixtures.hs b/test/Fixtures.hs --- a/test/Fixtures.hs +++ b/test/Fixtures.hs @@ -18,6 +18,7 @@ , recorded' , recordedWhole , recordedXml + , recording , withLambdas , withLambdasOf , withTemp @@ -112,21 +113,21 @@ recorded' :: Bool -> (SaveEvalFunc -> IO a) -> IO (a, String) recorded' hidden action = withTemp "phino-protocol-.txt" BS.empty $ \path -> do - answer <- withEvalFunc (Just path) (printing hidden) action + answer <- withEvalFunc Nothing (Just path) (printing hidden) action written <- withoutTotals <$> readUtf8 path pure (answer, written) recordedXml :: (SaveEvalFunc -> IO a) -> IO (a, String) recordedXml action = withTemp "phino-protocol-.xml" BS.empty $ \path -> do - answer <- withEvalFunc (Just path) (printing False) action + answer <- withEvalFunc (Just path) Nothing (printing False) action written <- readProtocol path pure (answer, written) recordedWhole :: (SaveEvalFunc -> IO a) -> IO (a, String) recordedWhole action = withTemp "phino-protocol-.xml" BS.empty $ \path -> do - answer <- withEvalFunc (Just path) (printing False) action + answer <- withEvalFunc (Just path) Nothing (printing False) action written <- readUtf8 path pure (answer, written) @@ -171,13 +172,18 @@ _ <- evaluate (length content) pure content +recording :: FilePath -> String +recording path + | map toLower (takeExtension path) == ".xml" = "--protocol=" ++ path + | otherwise = "--minutes=" ++ path + readProtocol :: FilePath -> IO String readProtocol path = sansTotals <$> readUtf8 path where sansTotals :: String -> String - sansTotals - | map toLower (takeExtension path) == ".xml" = withoutWrapper - | otherwise = withoutTotals . withoutHeader + sansTotals text + | " String withoutHeader text = case span ("# " `isPrefixOf`) (lines text) of