phino 0.0.162 → 0.0.163
raw patch · 8 files changed
+170/−103 lines, 8 files
Files
- README.md +4/−4
- phino.cabal +1/−1
- src/CLI/Helpers.hs +22/−22
- src/CLI/Parsers.hs +20/−7
- src/CLI/Runners.hs +4/−2
- src/CLI/Types.hs +2/−0
- test/CLISpec.hs +105/−61
- test/Fixtures.hs +12/−6
README.md view
@@ -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):
phino.cabal view
@@ -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 <https://github.com/objectionary/phino#readme>
src/CLI/Helpers.hs view
@@ -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
src/CLI/Parsers.hs view
@@ -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
src/CLI/Runners.hs view
@@ -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
src/CLI/Types.hs view
@@ -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
test/CLISpec.hs view
@@ -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 @@ , "</morph>" ] - it "keeps writing text when the file is named anything else" $- withTempFile "protocolXXXXXX.xmir" $ \(path, stream) -> do- hClose stream- withStdin sum' $- testCLISucceeded ["dataize", symbolic, "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] []- records <- readProtocol path- take 1 (lines records) `shouldBe` ["𝔻(Φ):"]+ 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 "<?xml" + describe "--minutes" $ do+ let sum' = "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ 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
test/Fixtures.hs view
@@ -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+ | "<?xml" `isPrefixOf` text = withoutWrapper text+ | otherwise = withoutTotals (withoutHeader text) withoutHeader :: String -> String withoutHeader text = case span ("# " `isPrefixOf`) (lines text) of