diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -589,9 +589,11 @@ ``` -Every argument of the call is an `` of ``, and an argument that -is not a bare symbol is spelled `?`. A copy with no object of the world has -neither `of` nor ``, only ``. +Every argument of the call is an `` of ``. An argument that is a +bare symbol, or a carrier of one whose `Ο†` leads to it, such as +`Ξ¦.number( Ο† ↦ 𝜎1:Ξ» )` or `𝜎1:Ξ»:Ο†`, is spelled as that symbol, and any other +argument is spelled `?`. A copy with no object of the world has neither `of` +nor ``, only ``. Every term is πœ‘ on a single line, whatever `--output` and `--flat` say about the result of the run, so a program reading the protocol back never has to know @@ -1385,10 +1387,32 @@ carries is the formation the frame above entered, as that frame had it, so the two are paired by their terms and no reader has to rename symbols by eye or find the cut in the residue. Nothing runs under a cut, so no block opens under -the line. In the XML protocol it is a self-closing element, -``, with the -attributes a `` carries and the mode. Without the option the same -run nests one round inside another until `--max-steps` runs out. +the line. In the XML protocol it is +`…`, with the +site and the mode as attributes and the formation in ``. Without the option +the same run nests one round inside another until `--max-steps` runs out. + +A cut at the `Ο†` of a copy the walk of `--deep` has placed, such as +`Ξ¦.a🌡4.Ο†`, answers that copy with a fresh symbol, the way a deferred copy is +answered. A fork above it then joins that symbol with its other branch, +instead of getting stuck on a copy nobody can read. The line names the +symbol, as in `looped(…) := 𝜎6 # 𝕄(Ξ¦.a🌡4.Ο†), plausible`, and the markup +writes the object the copy was made of and its arguments the way it writes +them for a deferred copy, on one line, broken here for reading: + + + +```xml + + 𝜎3? + ⟦ c ↦ 𝜎2:Ξ», left ↦ 00-:Ξ”, right ↦ Ξ¦.fact( n ↦ 𝜎3:Ξ»:Ο†, acc ↦ Ξ¦.pair( head ↦ 𝜎1:Ξ»:Ο†, tail ↦ 00-:Ξ” ) ), Ξ» ‍ L_if ⟧ + +``` + + + +A cut anywhere else, or at the `Ο†` of a copy nested inside a term, answers +nothing and leaves the copy as it stood. What a frame remembers is the branch from the run down to it, never everything the run has touched, so two siblings entering one formation enter it twice and 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.147 +version: 0.0.148 license: MIT synopsis: Command-Line Manipulator of πœ‘-Calculus Expressions description: Please see the README on GitHub at diff --git a/src/Deps.hs b/src/Deps.hs --- a/src/Deps.hs +++ b/src/Deps.hs @@ -8,10 +8,11 @@ import AST import Control.Monad (unless, when) +import Data.Bifunctor (bimap) import Data.IORef (IORef, readIORef, writeIORef) import Data.List (intercalate) import qualified Data.Map.Strict as Map -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, listToMaybe) import qualified Data.Text as T import Files (overwrite) import GHC.Clock (getMonotonicTime) @@ -92,7 +93,7 @@ = EvRun Judgment T.Text | EvFiring Int T.Text Judgment Expression | EvFormation Int Expression Expression - | EvLooped Int Judgment Acyclic Expression Expression + | EvLooped Int Judgment Acyclic Expression Expression (Maybe (Int, Maybe Expression)) | EvStuck Int T.Text Judgment Expression | EvStall Int T.Text | EvStuckOn Int T.Text @@ -119,7 +120,7 @@ record :: Evaluation -> Evaluation record (EvFiring depth key judgment site) = EvFiring depth key judgment (term site) record (EvFormation depth self site) = EvFormation depth (term self) (term site) - record (EvLooped depth judgment mode self site) = EvLooped depth judgment mode (term self) (term site) + record (EvLooped depth judgment mode self site answered) = EvLooped depth judgment mode (term self) (term site) (fmap (bimap symbol (fmap term)) answered) record (EvStuck depth key judgment self) = EvStuck depth key judgment (term self) record (EvStarved depth limit judgment site) = EvStarved depth limit judgment (term site) record (EvTimeout depth limit judgment site) = EvTimeout depth limit judgment (term site) @@ -203,10 +204,13 @@ form <- render self locator <- render site pure (protocol, Just (indented depth (printf "formation(%s) # %s(%s)" form (letter Dataization) locator))) - written (EvLooped depth judgment mode self site) protocol = do + written (EvLooped depth judgment mode self site answered) protocol = do form <- render self locator <- render site - pure (protocol, Just (indented depth (printf "looped(%s) # %s(%s), %s" form (letter judgment) locator (certainty mode)))) + pure (protocol, Just (indented depth (printf "looped(%s)%s # %s(%s), %s" form (maybe "" symbolized answered) (letter judgment) locator (certainty mode)))) + where + symbolized :: (Int, Maybe Expression) -> String + symbolized (symbol, _) = printf " := %s" (printFunction (FnSymbol symbol)) written (EvStuck depth key judgment self) protocol = do form <- render self pure (protocol, Just (indented depth (printf "unanswered(%s) # %s(%s)" (T.unpack key) (letter judgment) form))) @@ -345,11 +349,15 @@ locator <- render site let (kept, closers) = closed depth nesting._closing pure (nesting{_closing = (depth, "formation") : kept}, closers ++ [indentedXml depth (printf "" (escapeXML locator) (escapeXML form))]) - elements (EvLooped depth judgment mode self site) nesting = do + elements (EvLooped depth judgment mode self site answered) nesting = do form <- render self locator <- render site + (origin, given) <- maybe (pure ("", "")) called (answered >>= snd) let (kept, closers) = closed depth nesting._closing - pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "" (opened judgment) (certainty mode) (escapeXML locator) (escapeXML form))]) + pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s%s" (maybe "" symbolized answered) (opened judgment) (certainty mode) (escapeXML locator) origin given (escapeXMLText form))]) + where + symbolized :: (Int, Maybe Expression) -> String + symbolized (symbol, _) = printf " symbol=\"%s\"" (sigma symbol) elements (EvStuck depth key judgment self) nesting = do form <- render self let (kept, closers) = closed depth nesting._closing @@ -431,20 +439,6 @@ (origin, given) <- maybe (pure ("", "")) called call let (kept, closers) = closed depth nesting._closing pure (nesting{_closing = kept}, closers ++ [indentedXml depth (printf "%s%s" (sigma symbol) (opened judgment) (escapeXML locator) origin given (escapeXMLText form))]) - where - called :: Expression -> IO (String, String) - called term = do - let (object, arguments) = invoked term - path <- render object - pure (printf " of=\"%s\"" (escapeXML path), printf "%s" (concat arguments)) - invoked :: Expression -> (Expression, [String]) - invoked (ExApplication term (ArTau attr value)) = - let (object, arguments) = invoked term - in (object, arguments ++ [printf "%s" (escapeXML (printAttribute attr)) (escapeXMLText (valued value))]) - invoked term = (term, []) - valued :: Expression -> String - valued (ExFormation [BiLambda (FnSymbol idx)]) = sigma idx - valued _ = "?" elements (EvBuilt depth term) nesting = do body <- render term let (kept, closers) = closed depth nesting._closing @@ -460,6 +454,21 @@ labelled :: Nesting -> Int -> T.Text -> String labelled nesting depth spelling = printf "%s.%d" (T.unpack spelling) (fromMaybe 0 (Map.lookup (depth - 1) nesting._openedAt)) + called :: Expression -> IO (String, String) + called term = do + let (object, arguments) = invoked term + path <- render object + pure (printf " of=\"%s\"" (escapeXML path), printf "%s" (concat arguments)) + invoked :: Expression -> (Expression, [String]) + invoked (ExApplication term (ArTau attr value)) = + let (object, arguments) = invoked term + in (object, arguments ++ [printf "%s" (escapeXML (printAttribute attr)) (escapeXMLText (valued value))]) + invoked term = (term, []) + valued :: Expression -> String + valued (ExFormation [BiLambda (FnSymbol idx)]) = sigma idx + valued (ExFormation bds) = maybe "?" valued (listToMaybe [body | BiTau AtPhi body <- bds]) + valued (ExApplication _ (ArTau AtPhi body)) = valued body + valued _ = "?" sigma :: Int -> String sigma = printFunction . FnSymbol quoted :: T.Text -> String diff --git a/src/Evaluate.hs b/src/Evaluate.hs --- a/src/Evaluate.hs +++ b/src/Evaluate.hs @@ -9,7 +9,7 @@ import AST import Builder (buildExpressionThrows) -import Control.Exception (throwIO, try) +import Control.Exception (catch, throwIO, try) import Control.Monad (foldM, unless) import Data.List (partition) import Data.List.NonEmpty (NonEmpty (..)) @@ -19,7 +19,7 @@ import Engine (Engine (..)) import Lambdas (Lambda (..), Meta (..), joined, matched, minted, symbolized) import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot) -import Morph (Answer, Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), charged, counted, deeper, enter, isLambda, lambda, morphing, normalized, recalled, remember, remembered, retained, settled, starved, unparked) +import Morph (Answer, Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Refused (..), Steps (..), admitted, charged, counted, deeper, isLambda, lambda, morphing, normalized, recalled, refused, remember, remembered, retained, settled, starved, unparked) import Printer (printFunction) import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Text.Printf (printf) @@ -114,7 +114,7 @@ pure (snd answer, state) told (Looped term) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) - mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site)) caller._acyclic + mapM_ (\mode -> caller._saveEval (EvLooped (caller._nesting + 1) caller._judgment mode term caller._site Nothing)) caller._acyclic throwIO (Looping term) told (Stalled name _) = do caller._saveEval (EvFiring caller._nesting func caller._judgment caller._site) @@ -255,10 +255,10 @@ evaluated ctx state' form (func, self) | isNothing (matched ctx._symbolic func) = pure (Nothing, state') | otherwise = do - made <- try (enter form ctx >>= symbol func form self univ state') + made <- try (admitted form ctx >>= either (\(mode, before) -> throwIO (Refused mode before state')) (symbol func form self univ state')) case made of Right (answer, answered) -> do - (again, reached) <- fired dispatched answer univ answered ctx + (again, reached) <- fired dispatched answer univ answered ctx `catch` refused ctx pure (Just (fromMaybe answer again), reached) Left failure -> parked state' failure parked :: State -> ReduceException -> IO (Maybe Expression, State) diff --git a/src/Morph.hs b/src/Morph.hs --- a/src/Morph.hs +++ b/src/Morph.hs @@ -1,7 +1,6 @@ {-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} @@ -12,7 +11,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Morph (Answer, Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, FiringFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), boxed, charged, counted, deeper, emptyState, enter, entering, execBuildTerm, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, parking, recalled, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where +module Morph (Answer, Deadline (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, FiringFunc, Memo (..), ReductionFunc, Morphed, Refused (..), Steps (..), Tally (..), admitted, boxed, charged, counted, deeper, emptyState, enter, entering, execBuildTerm, inferred, insideUniverse, isLambda, lambda, leadsTo, memoized, morph, morph', morphing, normalized, onward, parking, recalled, refused, remember, remembered, retained, settled, starved, tallied, timed, universed, unparked) where import AST import Builder (buildExpressionThrows, pathOf) @@ -153,6 +152,18 @@ show (Undataizable _ _) = "no dataization rule matched" show (Unmorphable term) = printf "Morphing expects a normal form, but no morphing rule matches: %s" (printExpression term) +data Refused = Refused Acyclic Expression State + deriving anyclass (Exception) + +instance Show Refused where + show (Refused _ before _) = show (Looping before) + +data Severed = Severed Expression State + deriving anyclass (Exception) + +instance Show Severed where + show (Severed answer _) = printf "The deep walk answered a copy it cut with %s" (printExpression answer) + deeper :: ReduceContext -> IO ReduceContext deeper ctx@ReduceContext{_steps = Steps limit spent} = do clocked ctx @@ -270,15 +281,20 @@ entering term ctx = maybe (pure ctx) (`enter` ctx) (entrance ctx._judgment term) enter :: Expression -> ReduceContext -> IO ReduceContext -enter form ctx = maybe (pure ctx) remembered ctx._acyclic +enter form ctx = admitted form ctx >>= either refuse pure where - remembered :: Acyclic -> IO ReduceContext + refuse :: (Acyclic, Expression) -> IO ReduceContext + refuse (mode, before) = do + looped ctx mode before Nothing + throwIO (Looping form) + +admitted :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext) +admitted form ctx = maybe (pure (Right ctx)) remembered ctx._acyclic + where + remembered :: Acyclic -> IO (Either (Acyclic, Expression) ReduceContext) remembered mode = - awaited (find (repeated mode form) (Map.findWithDefault [] (digest mode form) ctx._entered)) >>= \case - Just before -> do - ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site) - throwIO (Looping form) - Nothing -> pure ctx{_entered = seenInsert (digest mode form) form ctx._entered} + maybe (Right ctx{_entered = seenInsert (digest mode form) form ctx._entered}) (Left . (mode,)) + <$> awaited (find (repeated mode form) (Map.findWithDefault [] (digest mode form) ctx._entered)) awaited :: Maybe Expression -> IO (Maybe Expression) awaited found = case ctx._deadline of Nothing -> pure found @@ -292,6 +308,12 @@ repeated Proven form before = alike form before repeated Plausible form before = within before form +refused :: ReduceContext -> Refused -> IO (Maybe Expression, State) +refused ctx (Refused mode before reached) = (Nothing, reached) <$ looped ctx mode before Nothing + +looped :: ReduceContext -> Acyclic -> Expression -> Maybe (Int, Maybe Expression) -> IO () +looped ctx mode before answer = ctx._saveEval (EvLooped ctx._nesting ctx._judgment mode before ctx._site answer) + entrance :: Judgment -> Expression -> Maybe Expression entrance Dataization term@(ExFormation bds) | boxed bds || isJust (lambda bds) = Just term @@ -404,15 +426,33 @@ case copy of Just form -> deferred form state' here Nothing -> do - (walked, walkedState) <- walk standing frame term state' here - placed <- ctx._engine._contextualize walked =<< context frame - current <- readIORef world - (answer, answered) <- ctx'._fire dispatched placed current walkedState ctx'{_universe = Just current} - mapM_ (noted here._site frame walked) answer - pure (fromMaybe walked answer, answered) + outcome <- try (walk standing frame term state' here) + case outcome of + Left (Severed answer reached) -> pure (answer, reached) + Right (walked, walkedState) -> do + placed <- ctx._engine._contextualize walked =<< context frame + current <- readIORef world + (answer, answered) <- ctx'._fire dispatched placed current walkedState ctx'{_universe = Just current} `catch` cut standing frame ctx' + mapM_ (noted here._site frame walked) answer + pure (fromMaybe walked answer, answered) + cut :: Maybe Expression -> Frame -> ReduceContext -> Refused -> IO (Maybe Expression, State) + cut (Just _) (Frame _ store path (Just AtPhi)) caller refusal@(Refused mode before reached) = do + form <- held path store + if copied form + then do + looped caller mode before (Just (fresh, called form)) + throwIO (Severed (ExFormation [BiLambda (FnSymbol fresh)]) reached{_minted = fresh}) + else refused caller refusal + where + fresh :: Int + fresh = reached._minted + 1 + cut _ _ caller refusal = refused caller refusal + copied :: Expression -> Bool + copied (ExFormation bds) = boxed bds && not (any abstract bds) && any code bds + copied _ = False deferrable :: Maybe Attribute -> IORef Expression -> Expression -> State -> ReduceContext -> IO (Maybe Expression) deferrable dispatched world form@(ExFormation bds) state' caller - | boxed bds && not (any abstract bds) && any code bds && maybe True (\attr -> not (any (named attr) bds)) dispatched = do + | copied form && maybe True (\attr -> not (any (named attr) bds)) dispatched = do current <- readIORef world known <- mapM (resolved current form state' caller) bds pure (if any bare known then Just (ExFormation known) else Nothing) @@ -518,15 +558,15 @@ where floor' :: Int floor' = state'._minted - planned :: Maybe (Expression, [Attribute]) -> (Int, Binding) -> IO (IO ([Evaluation], Either SomeException (Int -> (Binding, Maybe State)))) + planned :: Maybe (Expression, [Attribute]) -> (Int, Binding) -> IO (IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State)))) planned alias (idx, BiTau attr body) | attr /= AtRho = do new <- if closed body then fresh alias attr caller else pure True pure (if new then worker idx attr body else kept (BiTau attr body)) planned _ (_, bd) = pure (kept bd) - kept :: Binding -> IO ([Evaluation], Either SomeException (Int -> (Binding, Maybe State))) - kept bd = pure ([], Right (const (bd, Nothing))) - worker :: Int -> Attribute -> Expression -> IO ([Evaluation], Either SomeException (Int -> (Binding, Maybe State))) + kept :: Binding -> IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State))) + kept bd = pure ([], Right (const (pure (bd, Nothing)))) + worker :: Int -> Attribute -> Expression -> IO ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State))) worker idx attr body = do buffer <- newIORef [] tau <- tausOf idx @@ -535,19 +575,21 @@ copy <- newIORef =<< readIORef world (store, path) <- home standing copy form let own = caller{_jobs = 1, _tally = tally, _memo = memo, _saveEval = modifyIORef' buffer . (:), _buildTerm = minting tau caller._buildTerm} - outcome <- try (go (fmap (`ExDispatch` attr) standing) Nothing (Frame copy store path (Just attr)) body state' own) + outcome <- try (try (go (fmap (`ExDispatch` attr) standing) Nothing (Frame copy store path (Just attr)) body state' own)) records <- reverse <$> readIORef buffer - pure (records, fmap (\(term, walked) offset -> (BiTau attr (lifted floor' offset term), Just (moved offset walked))) outcome) + pure (records, fmap (either severed (\(term, walked) offset -> pure (BiTau attr (lifted floor' offset term), Just (moved offset walked)))) outcome) + severed :: Severed -> Int -> IO (Binding, Maybe State) + severed (Severed answer reached) offset = throwIO (Severed (lifted floor' offset answer) (moved offset reached)) moved :: Int -> State -> State moved offset walked = walked { _minted = walked._minted + offset , _manufactured = fmap (\sym -> if sym > floor' then sym + offset else sym) walked._manufactured } - gathered :: ([Binding], Int, State) -> ([Evaluation], Either SomeException (Int -> (Binding, Maybe State))) -> IO ([Binding], Int, State) + gathered :: ([Binding], Int, State) -> ([Evaluation], Either SomeException (Int -> IO (Binding, Maybe State))) -> IO ([Binding], Int, State) gathered (done, offset, current) (records, outcome) = do mapM_ (caller._saveEval . renumbered floor' offset) records - (bd, walked) <- either throwIO (pure . ($ offset)) outcome + (bd, walked) <- either throwIO ($ offset) outcome pure (bd : done, maybe offset (\after -> after._minted - floor') walked, fromMaybe current walked) spread standing frame term state' caller = parts standing frame term state' caller minting :: IO T.Text -> BuildTermFunc -> BuildTermFunc diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -1259,7 +1259,7 @@ , " looped(⟦ x ↦ ⟦⟧, Ο† ↦ Ξ¦.cyc( x ) ⟧) # 𝔻(Ξ¦.t), proven" ] - it "writes the cut to the XML protocol as a self-closing element" $ + it "writes the cut to the XML protocol with the formation in an element of its own" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do hClose stream withStdin circling $ @@ -1271,7 +1271,7 @@ `shouldBe` [ "" , "" , " " - , " " + , " ⟦ x ↦ ⟦⟧, Ο† ↦ Ξ¦.cyc( x ) ⟧" , " " , "" ] @@ -1600,6 +1600,15 @@ records <- readProtocol path lines records `shouldContain` [" deferred(𝜎2) := ⟦ x ↦ 𝜎1:Ξ», Ο† ↦ x.next ⟧ # 𝕄(Ξ¦.y)"] + it "writes the symbol a cut answers a copy with" $ + withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do + hClose stream + withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n 𝑛1: $.x\n 𝑛: 𝑛1\n") $ \loops -> + withStdin "⟦ box(n) ↦ ⟦ Ο† ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ ΞΎ.n ) ) ⟧, loop(x) ↦ L_loop:Ξ», y ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ ⟦ Ξ” ‍ 01- ⟧ ) ) ⟧" $ + testCLISucceeded ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=proven", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" looped(⟦ x ↦ Ξ¦.box( n ↦ 01-:Ξ” ), Ξ» ‍ L_loop ⟧) := 𝜎1 # 𝕄(Ξ¦.a🌡0.Ο†), proven"] + it "writes a told stall to the XML protocol" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do hClose stream @@ -1925,7 +1934,7 @@ withStdin "⟦ bytes(Ο†) ↦ ⟦⟧, dataized(target) ↦ L_dataized:Ξ», joined(items) ↦ ⟦ Ο† ↦ step( tup ↦ items, s ↦ sep ), sep ↦ Ξ¦.dataized( target ↦ items ), step(ρ, tup, s) ↦ ⟦ Ο† ↦ tup.next ⟧ ⟧, y ↦ Ξ¦.joined( items ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ).Ο† ⟧" $ testCLISucceeded ["morph", "--deep", "--symbolic=" ++ dataized, "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] records <- readProtocol path - lines records `shouldContain` [" 𝜎1?⟦ tup ↦ 𝜎1:Ξ», s ↦ 𝜎2:Ξ»:Ο†, Ο† ↦ tup.next ⟧"] + lines records `shouldContain` [" 𝜎1𝜎2⟦ tup ↦ 𝜎1:Ξ», s ↦ 𝜎2:Ξ»:Ο†, Ο† ↦ tup.next ⟧"] it "writes a question mark for an argument of a deferred copy that is no bare symbol" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do @@ -1951,6 +1960,15 @@ records <- readProtocol path lines records `shouldContain` [" ⟦ x ↦ 𝜎1:Ξ», Ο† ↦ x.next ⟧"] + it "writes the copy a cut answers as a call of the object it was made of" $ + withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do + hClose stream + withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n 𝑛1: $.x\n 𝑛: 𝑛1\n") $ \loops -> + withStdin "⟦ num(Ο†) ↦ ⟦⟧, box(n) ↦ ⟦ Ο† ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ ΞΎ.n ) ) ⟧, loop(x) ↦ L_loop:Ξ», y ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ Ξ¦.num( Ο† ↦ ⟦ Ξ» ‍ 𝜎1 ⟧ ) ) ) ⟧" $ + testCLISucceeded ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=plausible", "--locator=Q.y", "--protocol=" ++ path, "--quiet", "--sweet", "--hide-rho"] [] + records <- readProtocol path + lines records `shouldContain` [" 𝜎1⟦ x ↦ Ξ¦.box( n ↦ Ξ¦.num( Ο† ↦ 𝜎1:Ξ» ) ), Ξ» ‍ L_loop ⟧"] + it "writes no 'minted' element for a firing minting nothing" $ withTempFile "protocolXXXXXX.xml" $ \(path, stream) -> do hClose stream @@ -2704,6 +2722,20 @@ testCLISucceeded ["morph", "--symbolic=" ++ endless, "--deep", "--acyclic=proven", "--max-steps=4000", "--flat", "--hide-rho"] ["⟦ x ↦ ⟦ Ξ» ‍ L_loop ⟧.foo, y ↦ ⟦ z ↦ ⟦⟧ ⟧ ⟧"] + + it "answers a copy with a fresh symbol once it cuts the Ο† of the copy" $ + withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n 𝑛1: $.x\n 𝑛: 𝑛1\n") $ \loops -> + withStdin "⟦ box(n) ↦ ⟦ Ο† ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ ΞΎ.n ) ) ⟧, loop(x) ↦ L_loop:Ξ», y ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ ⟦ Ξ” ‍ 01- ⟧ ) ) ⟧" $ + testCLISucceeded + ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=proven", "--locator=Q.y", "--flat", "--hide-rho", "--sweet"] + ["𝜎1:Ξ»"] + + it "answers a cut copy with the symbol one walk gives it whatever --jobs says" $ + withLambdasOf (T.pack "- Ξ»: L_loop\n morph:\n 𝑛1: $.x\n 𝑛: 𝑛1\n- Ξ»: L_mint\n 𝑛: ⟦ Ξ» ‍ 𝜎 ⟧\n") $ \loops -> + withStdin "⟦ mint ↦ L_mint:Ξ», box(n) ↦ ⟦ k ↦ Ξ¦.mint, Ο† ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ ΞΎ.n ) ) ⟧, loop(x) ↦ L_loop:Ξ», y ↦ Ξ¦.loop( x ↦ Ξ¦.box( n ↦ ⟦ Ξ” ‍ 01- ⟧ ) ) ⟧" $ + testCLISucceeded + ["morph", "--symbolic=" ++ loops, "--deep", "--acyclic=proven", "--jobs=2", "--locator=Q.y", "--flat", "--hide-rho", "--sweet"] + ["𝜎2:Ξ»"] describe "fails" $ do it "with --output=xmir on a top formation of several bindings" $ diff --git a/test/DepsSpec.hs b/test/DepsSpec.hs --- a/test/DepsSpec.hs +++ b/test/DepsSpec.hs @@ -11,7 +11,7 @@ import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (isInfixOf, isPrefixOf) import Data.Time.Clock.POSIX (getPOSIXTime) -import Deps (Evaluation (EvDeferred, EvFiring, EvFormation, EvJoined, EvMinted, EvRun, EvTerm), Judgment (Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, saveStep) +import Deps (Acyclic (Proven), Evaluation (EvDeferred, EvFiring, EvFormation, EvJoined, EvLooped, EvMinted, EvRun, EvTerm), Judgment (Morphing), Nesting (..), Protocol (..), dontSaveEval, dontSaveStep, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, perSecond, progressed, renumbered, saveStep) import Fixtures (readUtf8) import GHC.Clock (getMonotonicTime) import Logger (LogLevel (DEBUG, ERROR, INFO), setLogConfig) @@ -123,6 +123,10 @@ it "raises the symbols the call a deferred copy stands for carries above the floor" $ case renumbered 2 5 (EvDeferred 3 4 Morphing (ExFormation []) (Just (ExApplication (ExDispatch ExRoot (AtLabel "box")) (ArTau (AtLabel "x") (ExFormation [BiLambda (FnSymbol 7)])))) ExXi) of EvDeferred _ _ _ _ call _ -> fmap symbols call `shouldBe` Just [12] + _ -> expectationFailure "The record did not stay the record it was" + it "raises the symbol a cut answers a copy with and the symbols of its call above the floor" $ + case renumbered 2 5 (EvLooped 3 Morphing Proven (ExFormation []) ExXi (Just (4, Just (ExApplication (ExDispatch ExRoot (AtLabel "box")) (ArTau (AtLabel "n") (ExFormation [BiLambda (FnSymbol 7)])))))) of + EvLooped _ _ _ _ _ answer -> fmap (fmap (fmap symbols)) answer `shouldBe` Just (9, Just [12]) _ -> expectationFailure "The record did not stay the record it was" describe "perSecond" $ do