phino 0.0.163 → 0.0.164

raw patch · 27 files changed

+467/−137 lines, 27 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +9/−4
• phino.cabal +1/−1
• src/Abridge.hs +20/−1
• src/CLI/Parsers.hs +2/−1
• src/Dataize.hs +3/−1
• src/Evaluate.hs +7/−3
• src/Functions.hs +1/−1
• src/Morph.hs +104/−47
• src/Regexp.hs +2/−0
• src/Render.hs +4/−0
• src/XMIR.hs +27/−8
• src/Yaml.hs +3/−0
• test-resources/evaluate-packs/copies-a-call-written-twice-once.yaml +17/−0
• test-resources/evaluate-packs/joins-two-sides-a-stay-brought-to-one-shape.yaml +6/−4
• test-resources/evaluate-packs/refuses-a-meta-bound-to-a-term-that-is-not-a-normal-form.yaml +30/−0
• test-resources/morph-packs/answers-bottom-on-rho-of-a-formation-without-rho.yaml +4/−2
• test-resources/morph-packs/fails-on-an-input-that-is-not-a-normal-form.yaml +3/−3
• test/AbridgeSpec.hs +28/−0
• test/CLISpec.hs +50/−30
• test/DataizeSpec.hs +4/−4
• test/EvaluateSpec.hs +7/−1
• test/FunctionsSpec.hs +12/−0
• test/MorphSpec.hs +58/−14
• test/RegexpSpec.hs +3/−0
• test/RenderSpec.hs +12/−0
• test/XMIRSpec.hs +23/−1
• test/YamlSpec.hs +27/−11

@@ -126,10 +126,12 @@ ```  Dataizing a symbol always gives the same bytes, the number 42, as above.+Like `morph`, `dataize` fails on a term that is not a normal form.  Inside an entry, `$` is the formation being fired and `Φ` is the universe. A meta is a named placeholder: `𝛿1`, `𝛿2` and so on hold bytes, while `𝑛1`,-`𝑛2` and so on hold terms.+`𝑛2` and so on hold normal forms, and a line that would bind one to any other+term fails the run. An entry may hold only the keys below, and any other key refuses the whole file: @@ -236,7 +238,7 @@ * `--max-memory` bounds the live heap of the run, such as `8G`.  `--partial` leaves a site in place when it runs out of steps, firings,-nodes or memory, but a run out of time always fails.+seconds, nodes or memory.  ## Morph @@ -377,7 +379,8 @@  The `--abridged` option folds every formation longer than sixty-four characters, or than `--abridged=WIDTH`, into its `φ`, `Δ` and `λ` and a count-of the rest.+of the rest, and every application that long into its head and a count of its+arguments. The `--abridged-data` option also cuts every byte string longer than eight bytes down to its first two bytes and its last two. @@ -628,7 +631,9 @@   replaces all the spaces with empty string. To escape braces and slashes   in pattern and replacement parts - use them with `\\`,   e.g. `s/\\(.+\\)//g`. In the replacement, `\\1` to `\\9`, as well as-  `$1`, put what a group of the pattern matched, e.g. `s/([0-9]+)/\\1!/g`.+  `$1`, put what a group of the pattern matched, e.g. `s/([0-9]+)/\\1!/g`,+  and `&` puts the whole match, e.g. `s/[0-9]+/<&>/g`, while `\\&` puts a+  literal `&`. * `random-string` - accepts dataizable expression or bytes as pattern.   Replaces `%x` and `%d` formatters with random hex numbers and   decimals accordingly. Uniqueness is guaranteed during one

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.163+version: 0.0.164 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>

@@ -21,7 +21,9 @@       | short expr || salient pair = EX_SINGLE (goPair pair) space (goExpr formation)       | otherwise = goExpr formation     goExpr EX_DISPATCH{..} = EX_DISPATCH (goExpr expr) space attr-    goExpr EX_APPLICATION{..} = EX_APPLICATION (goExpr expr) space eol tab (goArgument argument) eol' tab' indent+    goExpr app@EX_APPLICATION{..}+      | short app = EX_APPLICATION (goExpr expr) space eol tab (goArgument argument) eol' tab' indent+      | otherwise = EX_APPLICATION (goExpr expr) space eol tab (AA_TAU (APP_BINDING (PA_FOLDED (counted argument)))) eol' tab' indent     goExpr EX_PHI_MEET{..} = EX_PHI_MEET prefix idx (goExpr expr)     goExpr EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (goExpr expr)     goExpr EX_BYTES{..} = EX_BYTES (goBytes bytes)@@ -55,6 +57,23 @@     goArgument (AA_TAU APP_BINDING{..}) = AA_TAU (APP_BINDING (goPair pair))     goArgument (AA_TAUS binding) = AA_TAUS (goIntact binding)     goArgument (AA_EXPRS APP_ARG{..}) = AA_EXPRS (APP_ARG (goExpr expr) (goAppArgs args))+    counted :: APP_ARGUMENT -> Int+    counted (AA_TAU _) = 1+    counted (AA_TAUS binding) = goCount binding+      where+        goCount :: BINDING -> Int+        goCount BI_EMPTY{} = 0+        goCount BI_PAIR{..} = 1 + goCounts bindings+        goCount BI_META{..} = 1 + goCounts bindings+        goCounts :: BINDINGS -> Int+        goCounts BDS_EMPTY{} = 0+        goCounts BDS_PAIR{..} = 1 + goCounts bindings+        goCounts BDS_META{..} = 1 + goCounts bindings+    counted (AA_EXPRS APP_ARG{args = rest}) = 1 + goCount rest+      where+        goCount :: APP_ARGS -> Int+        goCount AAS_EMPTY = 0+        goCount AAS_EXPR{..} = 1 + goCount args     goIntact :: BINDING -> BINDING     goIntact BI_PAIR{..} = BI_PAIR (goPair pair) (goIntacts bindings) tab     goIntact BI_META{..} = BI_META meta (goIntacts bindings) tab

@@ -344,7 +344,8 @@         ( long "abridged"             <> help               "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 \+              \than the width keeps its φ, Δ and λ bindings and folds the rest into a count, as '+34', an \+              \application longer than the width keeps its head and folds its arguments the same way, while \               \every byte string it writes stays whole; the width is 64 characters unless given as --abridged=WIDTH"         )         <|> option

@@ -20,7 +20,7 @@ import Engine (Engine (..)) import qualified Inference as In import Locator (locatedExpression)-import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, carried, deeper, inferred, insideUniverse, leadsTo, onward, opening, parking, severing, universed)+import Morph (Morphed, ReduceContext (..), ReduceException (..), ReductionFunc, carried, deeper, inferred, insideUniverse, leadsTo, onward, opening, parking, severing, universed, vetted) import Rewriter (Rewritten)  type Dataized = (Bytes, [Rewritten])@@ -35,11 +35,13 @@ dataize :: Expression -> State -> ReduceContext -> IO (Outcome, [Rewritten], State) dataize universe state ctx@ReduceContext{..} = do   expr <- locatedExpression _locator universe+  vetted Dataization expr ctx   result <- try (dataize' (expr, (universe, Nothing) :| []) universe state ctx)   case result of     Right ((bytes, seq), state') -> pure (Dataized bytes, reverse seq, state')     Left (StuckAt func seq parked) | _partial -> residual seq parked{_stuck = Just func}     Left (OutOfStepsAt _ seq parked) | _partial -> residual seq parked+    Left (OutOfSteps _) | _partial -> pure (Residual expr, [(universe, Nothing)], state)     Left (LoopingAt _ seq parked) | _partial -> residual seq parked     Left (Undataizable term seq parked) | _partial -> do       unless (dead `elem` _parked) (_saveEval (EvStuck _nesting dead Dataization term))

@@ -24,8 +24,8 @@ import Forks (Refusal (Unnamed, Unripe), forked, joined) import Lambdas (Ending (..), Lambda (..), Line (..), Meta (..), cast, emptyLambdas, matched, minted, rewritten, stayed, symbolized, thrown) import Matcher (MetaValue (..), Subst, combine, substEmpty, substSingle, substSlot)-import Morph (Answer (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, noted, opening, recalled, remember, remembered, remembering, retained, settled, starved, unparked, voided)-import Printer (printFunction)+import Morph (Answer (..), Budget (..), Firing (..), Kept (..), ReduceContext (..), ReduceException (..), Steps (..), argued, awaited, boxed, called, charged, coined, counted, deeper, ended, expired, fired, isLambda, lambda, morphing, normalized, noted, opening, recalled, remember, remembered, remembering, retained, settled, starved, unparked, voided)+import Printer (printExpression, printFunction) import Rule (RuleContext (RuleContext)) import Text.Printf (printf) @@ -335,7 +335,8 @@               outcome <- try (settled placed univ state' reading)               case outcome of                 Right (sole@(ExFormation [BiLambda (FnSymbol _)]), _) -> pure (BiTau attr sole)-                Left (OutOfTime cap) -> expired ctx cap+                Left (OutOfSteps (Seconds cap)) -> expired ctx cap+                Left (OutOfStepsAt (Seconds cap) _ _) -> expired ctx cap                 _ -> pure bd         resolved bd = pure bd         reducible :: Expression -> Bool@@ -422,6 +423,9 @@     operand :: Expression -> IO Expression     operand term = caller._engine._contextualize term self     bind :: Meta -> MetaValue -> Subst -> IO Subst+    bind meta (MvExpression term) _+      | not (caller._engine._normal term) =+          throwIO (userError (printf "The meta '%s' of λ function '%s' may hold only a normal form, but got: %s" (T.unpack meta._spelling) (T.unpack func) (printExpression term)))     bind meta value bound = case combine (substSingle meta._name value) bound of       Just bound' -> pure bound'       Nothing ->

@@ -175,7 +175,7 @@         | h == '/' -> (acc, rest, True)         | otherwise -> nextUntilSlash rest (B.snoc acc h) escape     referring :: Char -> Bool-    referring char = isDigit char || char == '\\'+    referring char = isDigit char || char == '\\' || char == '&'  _randomString :: BuildTermMethod _randomString [arg] subst = do

@@ -11,7 +11,7 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT -module Morph (Answer (..), Deadline (..), Firing (..), Facts, Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, declared, deeper, emptyState, ended, enter, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, factual, memoized, morph, noted, remembering, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked, voided) where+module Morph (Answer (..), Budget (..), Deadline (..), Firing (..), Facts, Kept (..), ReduceContext (..), ReduceException (..), EvaluationFunc, Memo (..), ReductionFunc, Morphed, Steps (..), Tally (..), admitting, argued, awaited, boxed, called, carried, charged, coined, counted, declared, deeper, emptyState, ended, enter, execBuildTerm, expired, fired, inferred, insideUniverse, isLambda, lambda, leadsTo, factual, memoized, morph, noted, remembering, morph', morphing, normalized, onward, opening, parking, recalled, refused, remember, remembered, retained, settled, severing, starved, tallied, timed, universed, unparked, vetted, voided) where  import AST import Builder (buildExpressionThrows, nameIn)@@ -21,10 +21,12 @@ import Data.Bifunctor (first, second) import Data.IORef (IORef, atomicModifyIORef', modifyIORef', newIORef, readIORef, writeIORef) import Data.List (find, partition, sortOn)+import qualified Data.List as List import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map-import Data.Maybe (fromMaybe, isJust, listToMaybe)+import Data.Maybe (fromMaybe, isJust, listToMaybe, maybeToList)+import qualified Data.Set as Set import qualified Data.Text as T import Deps (Acyclic (..), BuildTermFunc, BuildTermMethod, Evaluation (..), Judgment (..), SaveEvalFunc, SaveStepFunc, State (..), Term (..), dispatched, dontSaveStep, sized) import Engine (Engine (..))@@ -89,8 +91,12 @@  type Store answer = Map.Map Int [(Expression, answer)] -type Facts = IORef (Store Expression)+data Facts = Facts (IORef (Store Expression)) (IORef Lodgings) +data Lodging = Lodging [(Expression, Attribute)] [(Attribute, Expression)]++data Lodgings = Lodgings !(Store Lodging) !(Map.Map Int [Expression])+ data ReduceContext = ReduceContext   { _locator :: Expression   , _site :: Expression@@ -132,10 +138,10 @@   | Cycles Int   | Nodes Int   | Memory Int+  | Seconds Int  data ReduceException   = OutOfSteps Budget-  | OutOfTime Int   | Stuck T.Text   | StuckAt T.Text (NonEmpty Rewritten) State   | OutOfStepsAt Budget (NonEmpty Rewritten) State@@ -144,6 +150,7 @@   | LoopingAt Expression (NonEmpty Rewritten) State   | Undataizable Expression (NonEmpty Rewritten) State   | Unmorphable Expression+  | Abnormal Judgment Expression   deriving anyclass (Exception)  instance Show ReduceException where@@ -157,9 +164,9 @@     printf "Evaluation did not finish before reaching the limit of nodes: --max-nodes=%d" limit   show (OutOfSteps (Memory limit)) =     printf "Evaluation did not finish before reaching the limit of memory: --max-memory=%s" (sized limit)-  show (OutOfStepsAt budget _ _) = show (OutOfSteps budget)-  show (OutOfTime limit) =+  show (OutOfSteps (Seconds limit)) =     printf "Evaluation did not finish before reaching the limit of seconds: --max-seconds=%d" limit+  show (OutOfStepsAt budget _ _) = show (OutOfSteps budget)   show (Stuck func) = printf "No entry of --symbolic answers the λ function '%s'" (T.unpack func)   show (StuckAt func _ _) = show (Stuck func)   show (Diverged func) = printf "The λ function '%s' could not join its two sides" (T.unpack func)@@ -168,6 +175,8 @@   show (Undataizable ExTermination _ _) = "dataization reached the terminator ⊥, which signals an error and cannot be dataized"   show (Undataizable term _ _) = printf "no dataization rule matched, while dataization expects a normal form: %s" (printExpression term)   show (Unmorphable term) = printf "Morphing expects a normal form, but no morphing rule matches: %s" (printExpression term)+  show (Abnormal Morphing term) = printf "Morphing expects a normal form, but the term at the locator is not one: %s" (printExpression term)+  show (Abnormal _ term) = printf "Dataization expects a normal form, but the term at the locator is not one: %s" (printExpression term)  deeper :: ReduceContext -> IO ReduceContext deeper ctx@ReduceContext{_steps = Steps limit spent} = do@@ -227,7 +236,7 @@ expired :: ReduceContext -> Int -> IO a expired ctx cap = do   ctx._saveEval (EvTimeout ctx._nesting cap ctx._judgment ctx._site)-  throwIO (OutOfTime cap)+  throwIO (OutOfSteps (Seconds cap))  awaited :: ReduceContext -> IO a -> IO a awaited ctx action = case ctx._deadline of@@ -326,7 +335,7 @@  severed :: Maybe Attribute -> Expression -> ReduceContext -> State -> Expression -> [Binding] -> (Acyclic, Expression) -> IO Expression severed taken univ ctx state form bds (mode, before) = do-  call <- (<|>) <$> traced ctx._facts form <*> traced ctx._facts before+  call <- awaited ctx (evaluate =<< ((<|>) <$> traced ctx._facts form <*> traced ctx._facts before))   forM_ call (recited ctx . snd)   reckoned <- traverse (spelled taken . fst) call   fresh <- coined ctx@@ -343,34 +352,55 @@ recited ctx = mapM_ (\(term, source) -> ctx._saveEval (EvRecalled ctx._nesting term source))  factual :: IO Facts-factual = newIORef Map.empty+factual = Facts <$> newIORef Map.empty <*> newIORef (Lodgings Map.empty Map.empty)  noted :: ReduceContext -> Expression -> Expression -> IO ()-noted ctx object source = forM_ ctx._facts $ \facts -> do+noted ctx object source = forM_ ctx._facts $ \(Facts facts lodgings) -> do   known <- (Just source ==) . lookup object . Map.findWithDefault [] (hashExpression object) <$> readIORef facts   unless known $ do     modifyIORef' facts (Map.insertWith (++) (hashExpression object) [(object, source)])+    modifyIORef' lodgings (\index -> fst (lodged Nothing index object))     ctx._saveEval (EvRemembered ctx._nesting object source)+  where+    lodged :: Maybe (Expression, Attribute) -> Lodgings -> Expression -> (Lodgings, Expression)+    lodged edge index@(Lodgings nodes shapes) term@(ExFormation bds) = case [node | (node, _) <- Map.findWithDefault [] (hashExpression term) nodes, node == term] of+      node : _ -> (maybe index (\parent -> Lodgings (Map.adjust (map (adopted node parent)) (hashExpression node) nodes) shapes) edge, node)+      [] -> case List.foldl' (lodging term) (index, []) [(attr, body) | BiTau attr body@(ExFormation _) <- bds, attr /= AtRho] of+        (Lodgings inner shapes', kids) -> (Lodgings (Map.insertWith (++) (hashExpression term) [(term, Lodging (maybeToList edge) (reverse kids))] inner) (Map.insertWith (++) (shaped bds) [term] shapes'), term)+    lodged _ index term = (index, term)+    lodging :: Expression -> (Lodgings, [(Attribute, Expression)]) -> (Attribute, Expression) -> (Lodgings, [(Attribute, Expression)])+    lodging parent (index, kids) (attr, body) = case lodged (Just (parent, attr)) index body of+      (index', kid) -> index' `seq` (index', (attr, kid) : kids)+    adopted :: Expression -> (Expression, Attribute) -> (Expression, Lodging) -> (Expression, Lodging)+    adopted node parent (term, Lodging parents kids)+      | term == node = (term, Lodging (parent : parents) kids)+      | otherwise = (term, Lodging parents kids) +shaped :: [Binding] -> Int+shaped bds = hashExpression (ExFormation (rholess bds))++rholess :: [Binding] -> [Binding]+rholess = filter ((/= Just AtRho) . attributeFromBinding)+ remembering :: Maybe Facts -> Expression -> IO Bool remembering Nothing _ = pure False-remembering (Just facts) term = isJust . lookup term . Map.findWithDefault [] (hashExpression term) <$> readIORef facts+remembering (Just (Facts facts _)) term = isJust . lookup term . Map.findWithDefault [] (hashExpression term) <$> readIORef facts  traced :: Maybe Facts -> Expression -> IO (Maybe (Expression, [(Expression, Expression)])) traced Nothing _ = pure Nothing-traced (Just facts) form = do+traced (Just (Facts facts lodgings)) form = do   known <- readIORef facts-  pure (go known (Map.size known) form)+  index <- readIORef lodgings+  pure (go index known [] form)   where-    go :: Store Expression -> Int -> Expression -> Maybe (Expression, [(Expression, Expression)])-    go _ 0 _ = Nothing-    go known budget term = listToMaybe [(named, (object, source) : hops) | (path, object, source) <- sortOn (\(path, _, _) -> length path) [(path, object, source) | (object, source) <- concat (Map.elems known), path <- take 1 (lodged term object)], let (base, hops) = resolved known budget source, Just named <- [rooted (foldl ExDispatch base path)]]-    resolved :: Store Expression -> Int -> Expression -> (Expression, [(Expression, Expression)])-    resolved known budget source = case lookup source (Map.findWithDefault [] (hashExpression source) known) of-      Just _ -> fromMaybe (source, []) (go known (budget - 1) source)+    go :: Lodgings -> Store Expression -> [Expression] -> Expression -> Maybe (Expression, [(Expression, Expression)])+    go index known passed term = listToMaybe [(named, (object, source) : hops) | (path, object, source) <- lodged index known term, object `notElem` passed, let (base, hops) = resolved index known (object : passed) source, Just named <- [rooted (foldl ExDispatch base path)]]+    resolved :: Lodgings -> Store Expression -> [Expression] -> Expression -> (Expression, [(Expression, Expression)])+    resolved index known passed source = case lookup source (Map.findWithDefault [] (hashExpression source) known) of+      Just _ -> fromMaybe (source, []) (go index known passed source)       Nothing -> case source of-        ExApplication target arg -> first (`ExApplication` arg) (resolved known budget target)-        ExDispatch target attr -> first (`ExDispatch` attr) (resolved known budget target)+        ExApplication target arg -> first (`ExApplication` arg) (resolved index known passed target)+        ExDispatch target attr -> first (`ExDispatch` attr) (resolved index known passed target)         _ -> (source, [])     rooted :: Expression -> Maybe Expression     rooted term = term <$ guard (grounded term)@@ -379,18 +409,29 @@     grounded (ExDispatch target _) = grounded target     grounded (ExApplication target _) = grounded target     grounded _ = False-    lodged :: Expression -> Expression -> [[Attribute]]-    lodged (ExFormation bds) whole = searched (filter (not . rho) bds) [([], whole)] Map.empty-    lodged _ _ = []-    searched :: [Binding] -> [([Attribute], Expression)] -> Store () -> [[Attribute]]-    searched _ [] _ = []-    searched own ((path, term@(ExFormation inner)) : rest) seen-      | isJust (lookup term (Map.findWithDefault [] (hashExpression term) seen)) = searched own rest seen-      | filter (not . rho) inner == own = reverse path : searched own rest seen-      | otherwise = searched own (rest ++ [(attr : path, body) | BiTau attr body <- inner, attr /= AtRho]) (Map.insertWith (++) (hashExpression term) [(term, ())] seen)-    searched own (_ : rest) seen = searched own rest seen-    rho :: Binding -> Bool-    rho bd = attributeFromBinding bd == Just AtRho+    lodged :: Lodgings -> Store Expression -> Expression -> [([Attribute], Expression, Expression)]+    lodged (Lodgings nodes shapes) known (ExFormation bds) = sortOn (\(path, _, _) -> length path) [(descended distances object, object, source) | digest <- Set.toAscList (Set.fromList (map hashExpression (concatMap (map fst) (Map.elems distances)))), (object, source) <- Map.findWithDefault [] digest known, isJust (lookup object (Map.findWithDefault [] digest distances))]+      where+        distances :: Store Int+        distances = spread 0 matched (Map.fromListWith (++) [(hashExpression node, [(node, 0)]) | node <- matched])+        matched :: [Expression]+        matched = [node | node@(ExFormation inner) <- Map.findWithDefault [] (shaped bds) shapes, rholess inner == rholess bds]+        spread :: Int -> [Expression] -> Store Int -> Store Int+        spread _ [] reached = reached+        spread depth frontier reached = uncurry (spread (succ depth)) (List.foldl' (climbed (succ depth)) ([], reached) [parent | node <- frontier, (parent, _) <- lodging node])+        climbed :: Int -> ([Expression], Store Int) -> Expression -> ([Expression], Store Int)+        climbed depth (next, reached) parent+          | isJust (lookup parent (Map.findWithDefault [] (hashExpression parent) reached)) = (next, reached)+          | otherwise = (parent : next, Map.insertWith (++) (hashExpression parent) [(parent, depth)] reached)+        descended :: Store Int -> Expression -> [Attribute]+        descended reached node = case lookup node (Map.findWithDefault [] (hashExpression node) reached) of+          Just depth | depth > 0 -> concat (take 1 [attr : descended reached kid | (attr, kid) <- children node, lookup kid (Map.findWithDefault [] (hashExpression kid) reached) == Just (pred depth)])+          _ -> []+        lodging :: Expression -> [(Expression, Attribute)]+        lodging node = maybe [] (\(Lodging parents _) -> parents) (lookup node (Map.findWithDefault [] (hashExpression node) nodes))+        children :: Expression -> [(Attribute, Expression)]+        children node = maybe [] (\(Lodging _ kids) -> kids) (lookup node (Map.findWithDefault [] (hashExpression node) nodes))+    lodged _ _ _ = []  coined :: ReduceContext -> IO Int coined ctx = atomicModifyIORef' ctx._minted (\count -> (succ count, succ count))@@ -405,7 +446,7 @@  voided :: ReduceContext -> Expression -> IO (Maybe [Attribute]) voided ReduceContext{_facts = Nothing} _ = pure Nothing-voided ctx@ReduceContext{_facts = Just facts} form@(ExFormation bds) = do+voided ctx@ReduceContext{_facts = Just (Facts facts _)} form@(ExFormation bds) = do   known <- readIORef facts   case lookup form (Map.findWithDefault [] (hashExpression form) known) of     Just source -> do@@ -501,7 +542,12 @@     hits = take (succ ctx._maxLoops) (filter (repeated mode) (Map.findWithDefault [] (digest mode form) ctx._entered))     repeated :: Acyclic -> Expression -> Bool     repeated Proven before = alike form before-    repeated Plausible before = within before form+    repeated Plausible before+      | atomic form = alike form before+      | otherwise = within before form+    atomic :: Expression -> Bool+    atomic (ExFormation bds) = any isLambda bds+    atomic _ = False  digest :: Acyclic -> Expression -> Int digest Proven = hashShape@@ -565,6 +611,7 @@ morph :: Expression -> State -> ReduceContext -> IO (Expression, [Rewritten], State) morph universe state caller@ReduceContext{..} = do   expr <- locatedExpression _locator universe+  vetted Morphing expr caller   prepared <- try (universed universe caller)   case prepared of     Left (OutOfSteps _) | _partial -> pure (expr, [(universe, Nothing)], state)@@ -578,6 +625,7 @@         Right ((morphed, seq), state') -> pure (morphed, reverse (NE.toList seq), state')         Left (StuckAt func seq parked) | _partial -> residue seq parked{_stuck = Just func}         Left (OutOfStepsAt _ seq parked) | _partial -> residue seq parked+        Left (OutOfSteps _) | _partial -> pure (expr, [(universe, Nothing)], state)         Left (LoopingAt _ seq parked) -> residue seq parked         Left failure -> throwIO (failure :: ReduceException)     residue :: NonEmpty Rewritten -> State -> IO (Expression, [Rewritten], State)@@ -585,6 +633,9 @@       expr <- locatedExpression _locator (fst (NE.head seq))       pure (expr, reverse (NE.toList seq), parked) +vetted :: Judgment -> Expression -> ReduceContext -> IO ()+vetted judgment expr ctx = unless (ctx._engine._normal expr) (throwIO (Abnormal judgment expr))+ inferred :: Expression -> Expression -> State -> ReduceContext -> [In.Inference value] -> IO (Maybe (In.Conclusion value, State)) inferred expr univ state ctx rules = do   ordered <- if ctx._shuffle then shuffle rules else pure rules@@ -628,7 +679,8 @@   whole <- withLocatedExpression _locator expr (fst (NE.head seq))   taken <- newIORef Map.empty   peeled <- newIORef Map.empty-  (rewrittens, exceeded) <- rewrite whole _engine._normalization (rewriteContext taken peeled ctx)+  copies <- newIORef Map.empty+  (rewrittens, exceeded) <- rewrite whole _engine._normalization (rewriteContext taken peeled copies ctx)   when exceeded $ do     _saveEval (EvExceeded _nesting _maxCycles _judgment _site)     throwIO (OutOfSteps (Cycles _maxCycles))@@ -637,24 +689,29 @@   expr' <- locatedExpression _locator (fst rw)   pure (expr', seq')   where-    rewriteContext :: IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> RewriteContext-    rewriteContext taken peeled whole@ReduceContext{..} =-      RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing (\term -> (measured whole =<< locatedExpression _locator term) >> _saveStep term) (made taken peeled whole)-    made :: IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> Expression -> Expression -> IO ()-    made _ _ whole redex@(ExApplication head' (ArTau attr _)) object@(ExFormation bds)+    rewriteContext :: IORef (Store Expression) -> IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> RewriteContext+    rewriteContext taken peeled copies whole@ReduceContext{..} =+      RewriteContext _locator _maxDepth _maxCycles _depthSensitive _universe _buildTerm _engine._normal _engine._matching MtDisabled Nothing (\term -> (measured whole =<< locatedExpression _locator term) >> _saveStep term) (made taken peeled copies whole)+    made :: IORef (Store Expression) -> IORef (Store Expression) -> IORef (Store Expression) -> ReduceContext -> Expression -> Expression -> IO ()+    made _ _ copies whole redex@(ExApplication head' (ArTau attr _)) object@(ExFormation bds)       | attr /= AtRho && object /= head' = do-          whole._saveEval (EvApplied whole._nesting whole._judgment (called whole._universe redex) object whole._site)-          known <- remembering whole._facts head'-          when (known && copied bds) (noted whole object redex)-    made taken _ whole redex@(ExApplication _ (ArTau AtRho _)) object@(ExFormation bds)+          made' <- readIORef copies+          if lookup redex (Map.findWithDefault [] (hashExpression redex) made') == Just object+            then whole._saveEval (EvRecalled whole._nesting (called whole._universe redex) object)+            else do+              modifyIORef' copies (Map.insertWith (++) (hashExpression redex) [(redex, object)])+              whole._saveEval (EvApplied whole._nesting whole._judgment (called whole._universe redex) object whole._site)+              known <- remembering whole._facts head'+              when (known && copied bds) (noted whole object redex)+    made taken _ _ whole redex@(ExApplication _ (ArTau AtRho _)) object@(ExFormation bds)       | copied bds = do           pending <- readIORef taken           forM_ (lookup redex (Map.findWithDefault [] (hashExpression redex) pending)) (noted whole object)-    made taken peeled whole redex@(ExDispatch target attr) object+    made taken peeled _ whole redex@(ExDispatch target attr) object       | attr /= AtRho = do           stripped peeled whole target attr           dispatched taken peeled whole redex object-    made _ _ _ _ _ = pure ()+    made _ _ _ _ _ _ = pure ()     stripped :: IORef (Store Expression) -> ReduceContext -> Expression -> Attribute -> IO ()     stripped peeled whole target@(ExFormation bds) attr = do       known <- remembering whole._facts target

@@ -68,8 +68,10 @@                     Just idx -> fromMaybe (B.pack ('$' : digits)) (safeIndex idx groups)                in val : go afterDigits     go ('\\' : '\\' : rest) = B.singleton '\\' : go rest+    go ('\\' : '&' : rest) = B.singleton '&' : go rest     go ('\\' : digit : rest)       | isDigit digit = fromMaybe (B.pack ['\\', digit]) (safeIndex (toInteger (digitToInt digit)) groups) : go rest+    go ('&' : rest) = fromMaybe (B.singleton '&') (safeIndex 0 groups) : go rest     go (c : rest) = B.singleton c : go rest     safeIndex :: Integer -> [B.ByteString] -> Maybe B.ByteString     safeIndex i xs

@@ -322,6 +322,10 @@     where       macro :: String -> Text       macro "evaluate" = "\\phinoEvaluate"+      macro "number" = "\\phinoNumber"+      macro "string" = "\\phinoString"+      macro "sum" = "\\phinoSum"+      macro "tau" = "\\phinoTau"       macro name = "\\" <> T.concat (zipWith camel [0 :: Int ..] (T.splitOn "-" (T.pack name)))       camel :: Int -> Text -> Text       camel 0 part = part

@@ -183,8 +183,14 @@   pure (object [("name", name), ("base", base)] children)  nestedBindings :: [Binding] -> XmirContext -> IO [Node]-nestedBindings bds ctx@XmirContext{..} = catMaybes <$> mapM (`formationBinding` ctx) bds'+nestedBindings bds ctx@XmirContext{..} = catMaybes <$> mapM (\bd -> fmap (typed bd) <$> formationBinding bd ctx) bds'   where+    typed :: Binding -> Node -> Node+    typed (BiVoid (AtLabel label)) (NodeElement (Element name attrs kids)) =+      NodeElement (Element name (M.union attrs (M.fromList [(toName key, T.pack value) | fn <- lambda, key <- ["type", "args"], Just value <- [M.lookup (voidKey fn label key) _atoms]])) kids)+    typed _ node = node+    lambda :: [T.Text]+    lambda = [fn | BiLambda (Function fn) <- bds]     bds' :: [Binding]     bds' = if _hideRho then filter (not . isRho) bds else bds     isRho :: Binding -> Bool@@ -309,8 +315,14 @@  renameAtoms :: [(T.Text, T.Text)] -> XmirContext -> XmirContext renameAtoms renames ctx@XmirContext{..} =-  ctx{_atoms = M.fromList [(new, atom) | (old, new) <- renames, Just atom <- [M.lookup old _atoms]]}+  ctx{_atoms = M.fromList [(new <> rest, atom) | (old, new) <- renames, (key, atom) <- M.toList _atoms, Just rest <- [owned old key]]}+  where+    owned :: T.Text -> T.Text -> Maybe T.Text+    owned old key = T.stripPrefix old key >>= \rest -> if T.null rest || T.isPrefixOf "." rest then Just rest else Nothing +voidKey :: T.Text -> T.Text -> String -> T.Text+voidKey fn label key = fn <> "." <> label <> "@" <> T.pack key+ escapeXML :: String -> String escapeXML = concatMap escapeChar   where@@ -539,21 +551,28 @@   ]  xmirAtoms :: Document -> IO Atoms-xmirAtoms xmir = M.fromList <$> mapM entry markers+xmirAtoms xmir = M.fromList . concat <$> mapM entries markers   where     markers :: [C.Cursor]     markers =       C.fromDocument xmir         C.$// C.element (toName "o")         C.>=> C.attributeIs (toName "name") "λ"-        C.>=> C.check (hasAttr "atom")     derived :: Derived     derived = derivedNames xmir-    entry :: C.Cursor -> IO (T.Text, String)-    entry cur = do+    entries :: C.Cursor -> IO [(T.Text, String)]+    entries cur = do       name <- lambdaName derived cur (lambdaPath cur)-      atom <- getAttr "atom" cur-      pure (name, atom)+      atom <- if hasAttr "atom" cur then (\value -> [(name, value)]) <$> getAttr "atom" cur else pure []+      pure+        ( atom+            ++ [ (voidKey name label key, T.unpack value)+               | void <- (C.parent C.>=> C.child C.>=> C.element (toName "o") C.>=> C.attributeIs (toName "base") "∅") cur+               , label <- C.attribute (toName "name") void+               , key <- ["type", "args"]+               , value <- C.attribute (toName key) void+               ]+        )  xmirToFormation :: Derived -> C.Cursor -> [String] -> IO Expression xmirToFormation derived cur fqn = do

@@ -19,6 +19,7 @@ import qualified Data.Aeson.KeyMap as KeyMap import Data.Aeson.Types (formatRelativePath) import qualified Data.ByteString as BS+import qualified Data.ByteString.Char8 as BC import Data.Conduit ((.|)) import qualified Data.Conduit.List as CL import Data.FileEmbed (embedDir)@@ -543,6 +544,8 @@     worded :: Libyaml.Event -> Libyaml.Event     worded (Libyaml.EventScalar value Libyaml.NoTag style anchor)       | value `elem` spelled = Libyaml.EventScalar value Libyaml.StrTag style anchor+    worded (Libyaml.EventScalar value (Libyaml.UriTag tag@('!' : _)) style anchor)+      | BS.null value = Libyaml.EventScalar (BC.pack tag) Libyaml.StrTag style anchor     worded event = event     spelled :: [BS.ByteString]     spelled = ["y", "Y", "yes", "Yes", "YES", "n", "N", "no", "No", "NO", "on", "On", "ON", "off", "Off", "OFF"]

@@ -0,0 +1,17 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# The call '⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ )' stands twice in 'c', once in 'a'+# and once in 'b'. Normalization of the world copies it once and recalls that+# copy for the second place, instead of copying the same call again (#2343).+symbolic: '[]'+location: 'Q.y'+input: '⟦ c ↦ ⟦ a ↦ ⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ ), b ↦ ⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ ) ⟧, y ↦ Φ.c.b ⟧'+result: '⟦ x ↦ 𝜎1:λ, φ ↦ x ⟧'+protocol: |+  𝕄(Φ.y):+    𝑛·0·1 := ⟦ x ↦ ∅, φ ↦ x ⟧( x ↦ 𝜎1:λ )+    𝑛·0·2 := ⟦ x ↦ 𝜎1:λ, φ ↦ x ⟧+    recalled 𝑛·0·1 ⇒ 𝑛·0·2+    morphed 𝑛·0·3 := 𝑛·0·2

@@ -29,10 +29,11 @@       right: 𝑛4 location: 'Q.y' hide-rho: false-input: '⟦ number ↦ ⟦ φ ↦ ∅ ⟧, bytes ↦ ⟦ φ ↦ ∅ ⟧, y ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎3 ⟧, a ↦ ⟦ φ ↦ Φ.number( φ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), x ↦ ∅ ⟧.ρ ) ⟧, b ↦ ⟦ φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) ) ⟧, λ ⤍ L_fork ⟧.φ ⟧'+input: '⟦ number ↦ ⟦ φ ↦ ∅ ⟧, bytes ↦ ⟦ φ ↦ ∅ ⟧, f ↦ ⟦ c ↦ ⟦ λ ⤍ 𝜎3 ⟧, a ↦ ⟦ φ ↦ Φ.number( φ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ), x ↦ ∅ ⟧.ρ ) ⟧, b ↦ ⟦ φ ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ) ) ⟧, λ ⤍ L_fork ⟧, y ↦ Φ.f.φ ⟧' result: 'Φ.bytes( φ ↦ 𝜎4:λ ):φ' protocol: |   𝕄(Φ.y):+    remembered 𝑛·0·1 ≡ Φ.f  # ⟦ c ↦ 𝜎3:λ, a ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ, ρ ↦ ⟦ ρ ↦ Φ.bytes( φ ↦ 𝜎1:λ ), x ↦ ∅ ⟧ ) ):φ, b ↦ Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎2:λ ) ):φ, λ ⤍ L_fork ⟧     𝔼(L_fork):       𝔻(ξ.c):         𝛿·1·1 := 𝔻(𝜎3:λ)@@ -46,6 +47,7 @@       𝑛3·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎1:λ ) ):φ  # stay(𝑛1)       joined 𝜎4 := 𝛿1·1 ? 𝜎1 : 𝜎2       𝑛·1·3 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) ):φ-    𝑛·0·1 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) )-    𝑛·0·2 := Φ.bytes( φ ↦ 𝜎4:λ ):φ-    morphed 𝑛·0·3 := 𝑛·0·2+      remembered 𝑛·1·3 ≡ 𝑛·0·1+    𝑛·0·2 := Φ.number( φ ↦ Φ.bytes( φ ↦ 𝜎4:λ ) )+    𝑛·0·3 := Φ.bytes( φ ↦ 𝜎4:λ ):φ+    morphed 𝑛·0·4 := 𝑛·0·3

@@ -0,0 +1,30 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# yamllint disable rule:line-length+# A meta 𝑛 of an entry may hold only a normal form (#2343). The 'rewrite'+# line normalizes nothing, and its rule wraps the term into a dispatch off a+# formation, which 'dot' of normalization would still take, so the firing+# refuses to bind '𝑛2' to it.+symbolic: |+  - λ: L_wrap+    morph:+      𝑛1: $.x+    rewrite:+      𝑛2:+        of: 𝑛1+        rules:+          - name: wrap+            pattern: ⟦ 𝐵1 ⟧+            result: ⟦ k ↦ ⟦ 𝐵1 ⟧ ⟧.k+    𝑛: 𝑛2+location: 'Q.y'+input: '⟦ y ↦ ⟦ x ↦ ⟦ Δ ⤍ 01- ⟧, λ ⤍ L_wrap ⟧.φ ⟧'+fails: "The meta '𝑛2' of λ function 'L_wrap' may hold only a normal form"+protocol: |+  𝕄(Φ.y):+    𝔼(L_wrap):+      𝕄(ξ.x):+        morphed 𝑛·1·1 := 01-:Δ+      𝑛1·1 := 01-:Δ  # 𝕄(ξ.x)+      𝑛2·1 := 01-:Δ:k.k  # rewrite(𝑛1)

@@ -2,7 +2,9 @@ # SPDX-License-Identifier: MIT --- # A formation that declares no ρ has no receiver, so asking it for one is-# dead and does not go through its φ (#1859).+# dead and does not go through its φ (#1859). The dispatch stands in the+# world, since 'morph' refuses a term at the locator that is not a normal+# form (#2343). location: 'Q.x'-input: '[[ x -> [[ @ -> $.y, y -> [[ ]] ]].^ ]]'+input: '[[ k -> [[ @ -> $.y, y -> [[ ]] ]].^, x -> Q.k ]]' result: '⊥'

@@ -3,10 +3,10 @@ --- # 𝕄 maps normal forms to formations, and 'morph' does not normalize what it is # handed. A dispatch off a formation with neither φ nor λ is not a normal form,-# since 'dot' of normalization eats it, and no morphing rule takes it, so the-# run tells the user so instead of failing with a bare "user error" (#1442).+# since 'dot' of normalization eats it, so the run refuses it as broken input+# instead of failing with a bare "user error" (#1442, #2343). location: 'Q.t' input: '⟦ t ↦ ⟦ x ↦ ⟦⟧ ⟧.x ⟧' fails: >--  Morphing expects a normal form, but no morphing rule matches:+  Morphing expects a normal form, but the term at the locator is not one:   ⟦⟧:x.x

@@ -70,6 +70,34 @@         )         (SWEET, UNICODE, SINGLELINE, defaultMargin)         `shouldBe` "⟦ λ ⤍ L_weit, φ ↦ ∅, +5 ⟧"+    it "leaves an application no longer than the width as it is" $+      printExpressionWith+        (const (abridged True 64))+        (ExApplication (ExApplication (ExDispatch ExRoot (AtLabel "brücke")) (ArTau (AtLabel "links") ExXi)) (ArTau (AtLabel "rechts") ExRoot))+        (SWEET, UNICODE, SINGLELINE, defaultMargin)+        `shouldBe` "Φ.brücke( links ↦ ξ, rechts ↦ Φ )"+    it "folds the arguments of an application wider than the width into a count" $+      printExpressionWith+        (const (abridged True 64))+        (foldl (\expr idx -> ExApplication expr (ArTau (AtLabel (T.pack ("strasse-" <> show idx))) ExRoot)) (ExDispatch ExRoot (AtLabel "stadt")) [1 .. 7 :: Int])+        (SWEET, UNICODE, SINGLELINE, defaultMargin)+        `shouldBe` "Φ.stadt( +7 )"+    it "folds a long application in the φ of a long formation" $+      printExpressionWith+        (const (abridged True 64))+        ( ExFormation+            [ BiTau (AtLabel "wolke") ExRoot+            , BiTau AtPhi (foldl (\expr idx -> ExApplication expr (ArTau (AtLabel (T.pack ("regen-" <> show idx))) ExXi)) (ExDispatch ExXi (AtLabel "himmel")) [1 .. 8 :: Int])+            ]+        )+        (SWEET, UNICODE, SINGLELINE, defaultMargin)+        `shouldBe` "⟦ φ ↦ himmel( +8 ), +1 ⟧"+    it "folds a long application its dispatch is made of" $+      printExpressionWith+        (const (abridged True 64))+        (ExDispatch (foldl (\expr idx -> ExApplication expr (ArAlpha (Alpha idx) (ExDispatch ExRoot (AtLabel "langer-name")))) (ExDispatch ExRoot (AtLabel "fluss")) [0 .. 5 :: Int]) (AtLabel "ufer"))+        (SWEET, UNICODE, SINGLELINE, defaultMargin)+        `shouldBe` "Φ.fluss( +6 ).ufer"     it "cuts a long byte string to its first bytes, its last bytes and the count of the bytes between them" $       printExpressionWith         (const (abridged True 64))

@@ -1433,7 +1433,7 @@    it "names the term dataization cannot take, and says a normal form is expected" $     withStdin "⟦ x ↦ ⟦ b ↦ ⟦ Δ ⤍ 01- ⟧ ⟧.b ⟧" $-      testCLIFailed ["dataize", "--locator=Q.x"] ["expects a normal form: 01-:Δ:b.b"]+      testCLIFailed ["dataize", "--locator=Q.x"] ["Dataization expects a normal form, but the term at the locator is not one: 01-:Δ:b.b"]    describe "--partial parks a universe that --max-cycles stops" $ do     let heavy = "⟦ simple ↦ ⟦ Δ ⤍ 01- ⟧, heavy ↦ ⟦ a ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 02- ⟧ ⟧ ⟧ ⟧.a.b.c ⟧"@@ -1673,7 +1673,7 @@         recorded "2" "protocolXXXXXX.txt" >>= (`shouldContain` ["          looped 𝜎3 := Φ.down( i ↦ 𝑛·6·6 )  # plausible, repeats 𝑛·0·4"])      describe "--acyclic at a copy holding a λ" $ do-      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, down(i) ↦ ⟦ φ ↦ Φ.dataized( Φ.fork( Φ.dataized( Φ.down( ⟦ λ ⤍ 𝜎2 ⟧ ) ), ⟦ λ ⤍ 𝜎3 ⟧ ) ) ⟧, x ↦ Φ.down( ⟦ λ ⤍ 𝜎1 ⟧ ) ⟧"+      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, x ↦ Φ.dataized( Φ.fork( Φ.dataized( Φ.x ), ⟦ λ ⤍ 𝜎3 ⟧ ) ) ⟧"           forking = T.pack "- λ: L_fork\n  dataize:\n    𝛿1: $.on🌵\n  morph:\n    𝑛1: $.left🌵\n    𝑛2: $.right🌵\n  evaluate:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  join:\n    on: 𝛿1\n    left: 𝑛3\n    right: 𝑛4\n    otherwise: L_fork\n- λ: L_dataized\n  dataize:\n    𝛿1: $.target\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"           recorded :: String -> IO [String]           recorded name =@@ -1691,7 +1691,7 @@             testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]        it "writes the copy holding a λ it cuts to the protocol as a call of the object" $-        recorded "protocolXXXXXX.txt" >>= (`shouldContain` ["                      looped 𝜎8 := Φ.dataized( target ↦ 𝜎7:λ )  # 𝔻(𝑛·6·4), plausible, repeats 𝑛·7·2"])+        recorded "protocolXXXXXX.txt" >>= (`shouldContain` ["                                looped 𝜎6 := Φ.dataized( target ↦ 𝜎5:λ )  # plausible, repeats 𝑛·9·2"])      describe "--acyclic at a copy holding a λ that evaluate fires" $ do       let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ ⟦ φ ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x ) ) ) ⟧ ⟧"@@ -1702,7 +1702,7 @@             testCLISucceeded ["dataize", "--symbolic=" ++ file, "--locator=Q.x", "--acyclic=plausible", "--max-loops=2"] ["40-45-00-00-00-00-00-00"]      describe "--acyclic at a copy whose call ends with an attribute" $ do-      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ), Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x ) ) ) ) ⟧"+      let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, fork(left, right) ↦ ⟦ λ ⤍ L_fork, on🌵 ↦ ⟦ λ ⤍ 𝜎4 ⟧, left🌵 ↦ ξ.left, right🌵 ↦ ξ.right ⟧, num(φ) ↦ ⟦⟧, x ↦ Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎5 ⟧ ), Φ.fork( Φ.num( ⟦ λ ⤍ 𝜎3 ⟧ ), Φ.num( Φ.dataized( Φ.x.φ ) ) ) ) ⟧"           forking = T.pack "- λ: L_fork\n  dataize:\n    𝛿1: $.on🌵\n  morph:\n    𝑛1: $.left🌵\n    𝑛2: $.right🌵\n  evaluate:\n    𝑛3: 𝑛1\n    𝑛4: 𝑛2\n  join:\n    on: 𝛿1\n    left: 𝑛3\n    right: 𝑛4\n    otherwise: L_fork\n- λ: L_dataized\n  dataize:\n    𝛿1: $.target\n  𝑛: ⟦ λ ⤍ 𝜎 ⟧\n"           recorded :: String -> IO [String]           recorded name =@@ -1715,10 +1715,10 @@                     []               lines <$> readProtocol path       it "writes the copy it cuts to the protocol as a call of the object with the attribute it ends with" $-        recorded "protocolXXXXXX.txt" >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎6 := Φ.fork( left ↦ 𝑛·9·9, right ↦ 𝑛·11·1 ).φ  # 𝔻(𝑛·9·6)"))+        recorded "protocolXXXXXX.txt" >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎6 := Φ.fork( left ↦ 𝑛·13·8, right ↦ 𝑛·15·1 ).right🌵.φ  # plausible"))        it "writes the copy it cuts to the XML protocol with the object, the metas of its arguments and the attribute it ends with" $-        recorded "protocolXXXXXX.xml" >>= (`shouldSatisfy` any (isInfixOf "object=\"Φ.fork\" dispatch=\"φ\"><with><meta attr=\"left\">𝑛·9·9</meta><meta attr=\"right\">𝑛·11·1</meta></with></looped>"))+        recorded "protocolXXXXXX.xml" >>= (`shouldSatisfy` any (isInfixOf "object=\"Φ.fork\" dispatch=\"right🌵.φ\"><with><meta attr=\"left\">𝑛·13·8</meta><meta attr=\"right\">𝑛·15·1</meta></with></looped>"))      describe "--acyclic at a copy whose argument repeats the same loop" $ do       let recursive = "⟦ dataized(target) ↦ ⟦ λ ⤍ L_dataized ⟧, times(b) ↦ ⟦ λ ⤍ L_times ⟧, x ↦ Φ.times( Φ.dataized( Φ.x ) ) ⟧"@@ -1814,29 +1814,41 @@                     ["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" $-        recorded >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎7  # 𝔻(𝑛·9·10), plausible"))+      it "writes the loop it cuts inside the nested fork as a call of the object" $+        recorded >>= (`shouldSatisfy` any (isInfixOf "looped 𝜎7 := Φ.p  # plausible"))        it "dont get stuck above the nested fork it cuts" $         recorded >>= (`shouldNotSatisfy` any (isInfixOf "stuck L_dataized")) +    describe "--acyclic at copies of one atom called from different places" $+      it "dont cut a copy of an atom that only resembles the copies open above it" $+        withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do+          hClose stream+          withLambdasOf (T.pack "- λ: L_d\n  dataize:\n    𝛿1: $.t\n  𝑛: Φ.w( φ ↦ ⟦ λ ⤍ 𝜎 ⟧ )\n") $ \file ->+            withStdin "⟦ w ↦ ⟦ φ ↦ ∅, me ↦ ξ, you ↦ ξ, x ↦ Φ.d( t ↦ ξ ).me.you ⟧, d(t) ↦ ⟦ λ ⤍ L_d ⟧, e ↦ Φ.d( t ↦ Φ.d( t ↦ Φ.d( t ↦ ⟦ φ ↦ Φ.d( t ↦ ⟦ Δ ⤍ 01- ⟧ ).x ⟧ ) ) ) ⟧" $+              testCLISucceeded+                ["dataize", "--symbolic=" ++ file, "--locator=Q.e", "--acyclic=plausible", "--max-loops=2", "--partial", "--minutes=" ++ path, "--quiet", "--sweet", "--hide-rho"]+                []+          records <- readProtocol path+          lines records `shouldNotSatisfy` any (isInfixOf "looped")+     it "dataizes with --sequence" $-      withStdin "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]" $+      withStdin "[[ @ -> $.f(y -> [[ ]]), f -> [[ D> 00-, y -> ? ]] ]]" $         testCLISucceeded           ["dataize", "--sequence", "--output=latex", "--flat", "--sweet"]           [ intercalate               "\n"               [ "\\begin{phiquation}"-              , "[[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ \\phiDataize[\\nameref{r:box}]"-              , "  \\phiDataize [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) : |x| . |x| : @ . @ \\phiNormalize[\\nameref{r:copy}]"-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] : |x| . |x| : @ . @ \\phiNormalize[\\nameref{r:dot}]"-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ D> |01-|, |y| -> [[]] ]] : |x| ) : @ . @ \\phiNormalize[\\nameref{r:skip}]"-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] : @ . @ \\phiNormalize[\\nameref{r:dot}]"-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:skip}]"-              , "  \\phiNormalize [[ D> |01-|, |y| -> [[]] ]] \\phiDataize[\\nameref{r:delta}]"-              , "  \\phiDataize |01-|{.}"+              , "[[ @ -> |f| ( |y| -> [[]] ), |f|(|y|) -> |00-| : D ]] \\phiDataize[\\nameref{r:box}]"+              , "  \\phiDataize [[ @ -> |f| ( |y| -> [[]] ), |f|(|y|) -> |00-| : D ]] . @ \\phiNormalize[\\nameref{r:dot}]"+              , "  \\phiNormalize [[ |f|(|y|) -> |00-| : D ]] . |f| ( |y| -> [[]], \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:dot}]"+              , "  \\phiNormalize [[ D> |00-|, |y| -> ? ]] ( \\phiTerminal{\\rho} -> [[ |f|(|y|) -> |00-| : D ]], |y| -> [[]], \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:skip}]"+              , "  \\phiNormalize [[ D> |00-|, |y| -> ? ]] ( |y| -> [[]], \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:copy}]"+              , "  \\phiNormalize [[ D> |00-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> Q ) \\phiNormalize[\\nameref{r:skip}]"+              , "  \\phiNormalize [[ D> |00-|, |y| -> [[]] ]] \\phiDataize[\\nameref{r:delta}]"+              , "  \\phiDataize |00-|{.}"               , "\\end{phiquation}"-              , "01-"+              , "00-"               ]           ] @@ -3545,7 +3557,7 @@         testCLISucceeded ["dataize", "--max-cycles=1"] ["01-"]      it "reports --max-cycles exceeded when a rule still applies at the limit" $-      withStdin "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]" $+      withStdin "[[ @ -> $.f(y -> [[ ]]), f -> [[ D> 00-, y -> ? ]] ]]" $         testCLIFailed           ["dataize", "--max-cycles=1"]           ["[ERROR]: Normalization did not finish before reaching the limit of cycles: --max-cycles=1"]@@ -3769,7 +3781,7 @@             ["Φ.m( 𝜎1:λ )"]        it "passes a small run in a large program under --max-nodes" $-        withStdin ("⟦ x ↦ ⟦ φ ↦ ⟦ y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧.y ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $+        withStdin ("⟦ x ↦ ⟦ φ ↦ ξ.y, y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $           testCLISucceeded ["dataize", "--max-nodes=50", "--locator=Q.x"] ["05-"]      describe "--max-memory" $ do@@ -3795,7 +3807,7 @@             ["Φ.m( 𝜎1:λ )"]        it "passes a small run in a large program under --max-memory" $-        withStdin ("⟦ x ↦ ⟦ φ ↦ ⟦ y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧.y ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $+        withStdin ("⟦ x ↦ ⟦ φ ↦ ξ.y, y ↦ ⟦ Δ ⤍ 05- ⟧ ⟧, junk ↦ ⟦ " ++ intercalate ", " [printf "a%d ↦ ⟦ b ↦ ⟦ c ↦ ⟦ Δ ⤍ 01- ⟧ ⟧ ⟧" index | index <- [0 .. 999 :: Int]] ++ " ⟧ ⟧") $           testCLISucceeded ["dataize", "--max-memory=1G", "--locator=Q.x"] ["05-"]      describe "--max-seconds" $ do@@ -3829,24 +3841,32 @@                 ["dataize", "--symbolic=" ++ table, "--locator=Q.x", "--max-seconds=1"]                 ["[ERROR]: Evaluation did not finish before reaching the limit of seconds: --max-seconds=1"] -      it "fails once the --max-seconds budget is spent with --partial" $+      it "prints the residue once the --max-seconds budget is spent with --partial" $         ladder $ \table ->           bounded $             withStdin rungs $-              testCLIFailed-                ["morph", "--symbolic=" ++ table, "--max-seconds=1", "--locator=Q.x", "--partial"]-                ["[ERROR]: Evaluation did not finish before reaching the limit of seconds: --max-seconds=1"]+              testCLISucceeded+                ["morph", "--symbolic=" ++ table, "--max-seconds=1", "--locator=Q.x", "--partial", "--flat", "--hide-rho", "--sweet"]+                ["⟦ λ ⤍ L_split, n ↦ Φ.l1 ⟧.foo"] -      forM_ [["--locator=Q.x"], ["--locator=Q.x", "--partial"]] $ \opts ->+      it "prints the residue of a dataization once the --max-seconds budget is spent with --partial" $+        ladder $ \table ->+          bounded $+            withStdin rungs $+              testCLISucceeded+                ["dataize", "--symbolic=" ++ table, "--max-seconds=1", "--locator=Q.x", "--partial", "--flat", "--hide-rho", "--sweet"]+                ["⟦ λ ⤍ L_split, n ↦ Φ.l1 ⟧.foo"]++      forM_ [(testCLIFailed, ["--max-seconds=1"], ["--locator=Q.x"]), (testCLISucceeded, [], ["--locator=Q.x", "--partial"])] $ \(run, outputs, opts) ->         it ("writes the timeout as the last line of the protocol with " ++ unwords opts) $           ladder $ \table ->             withTempFile "protocolXXXXXX.txt" $ \(path, stream) -> do               hClose stream               bounded $                 withStdin rungs $-                  testCLIFailed+                  run                     (["morph", "--symbolic=" ++ table, "--max-seconds=1", "--minutes=" ++ path, "--quiet"] ++ opts)-                    ["--max-seconds=1"]+                    outputs               records <- readProtocol path               dropWhile (== ' ') (last (lines records)) `shouldBe` "timeout 1" @@ -3856,9 +3876,9 @@             hClose stream             bounded $               withStdin rungs $-                testCLIFailed+                testCLISucceeded                   ["morph", "--symbolic=" ++ table, "--locator=Q.x", "--partial", "--max-seconds=1", "--protocol=" ++ path, "--quiet"]-                  ["--max-seconds=1"]+                  []             records <- readProtocol path             length (filter (isInfixOf "<timeout limit=\"1\" by=\"morph\" at=\"") (lines records)) `shouldBe` 1 

@@ -188,12 +188,12 @@           Dataized bts -> expectationFailure ("expected a residual, dataized to " ++ show bts)    describe "stops a dataization by the clock of --max-seconds" $-    it "fails a partial dataization once the deadline has passed" $ do+    it "leaves a partial dataization as a residual once the deadline has passed" $ do       expr <- parseExpressionThrows "[[ @ -> [[ D> 7E- ]] ]]"       deadline <- overdue 29       ctx <- defaultReduceContext ExRoot-      dataize expr emptyState ctx{_deadline = Just deadline, _partial = True}-        `shouldThrow` (\e -> "--max-seconds=29" `isInfixOf` show (e :: SomeException))+      (outcome, _, _) <- dataize expr emptyState ctx{_deadline = Just deadline, _partial = True}+      outcome `shouldBe` Residual expr    describe "partially evaluates around a λ function that cannot fire (--partial)" $ do     let placeholder = ExFormation [BiLambda (Function "Sym_arg_0")]@@ -313,7 +313,7 @@       ]       ( \(flag, reducing, message) ->           it ("throws once " ++ flag ++ " is exhausted with --depth-sensitive") $ do-            expr <- parseExpressionThrows "[[ @ -> [[ x -> [[ D> 00- ]] ]].x ]]"+            expr <- parseExpressionThrows "[[ @ -> $.f(y -> [[ ]]), f -> [[ D> 00-, y -> ? ]] ]]"             ctx <- reducing <$> newIORef 0             dataize expr emptyState ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException))       )

@@ -113,7 +113,13 @@       (_, Just recall)         | paired " ⇒ " recall `elem` facts -> orphans rest facts         | otherwise -> line : orphans rest facts-      _ -> orphans rest facts+      _ -> orphans rest (applied line rest ++ facts)+    applied :: String -> [String] -> [(String, String)]+    applied line (next : _)+      | " := " `T.isInfixOf` T.pack line && " := " `T.isInfixOf` T.pack next = [(named line, named next)]+    applied _ _ = []+    named :: String -> String+    named = T.unpack . fst . T.breakOn " := " . T.pack     paired :: T.Text -> T.Text -> (String, String)     paired arrow text = let (left, right) = T.breakOn arrow text in (T.unpack left, T.unpack (T.drop (T.length arrow) right)) 

@@ -158,6 +158,18 @@         , \term -> expectExpression term (DataString (strToBts "\\1"))         )       ,+        ( "sed puts the whole match where the replacement holds an ampersand"+        , "sed"+        , [ArgExpression (DataString (strToBts "order 42")), ArgExpression (DataString (strToBts "s/([0-9]+)/<&>/g"))]+        , \term -> expectExpression term (DataString (strToBts "order <42>"))+        )+      ,+        ( "sed keeps an escaped ampersand in the replacement literal"+        , "sed"+        , [ArgExpression (DataString (strToBts "order 42")), ArgExpression (DataString (strToBts "s/([0-9]+)/<\\&>/g"))]+        , \term -> expectExpression term (DataString (strToBts "order <&>"))+        )+      ,         ( "random-string returns a literal pattern with no specials unchanged"         , "random-string"         , [ArgExpression (DataString (strToBts "static-name"))]

@@ -17,11 +17,11 @@ import Data.IORef (modifyIORef', newIORef, readIORef) import Data.List (find, isInfixOf, nub) import Data.List.NonEmpty (NonEmpty (..))-import Data.Map.Strict qualified as Map import Data.Maybe (fromMaybe)+import Data.Text qualified as T import Data.Yaml qualified as Decode import Dataize (Outcome (..), dataize)-import Deps (Acyclic (..), Evaluation (EvMorphed, EvRecalled, EvWorld), Judgment (..), State, Term (TeExpression))+import Deps (Acyclic (..), Evaluation (EvLooped, EvMorphed, EvRecalled, EvWorld), Judgment (..), State, Term (TeExpression)) import Engine (Engine (_normal)) import Files (allPathsIn) import Fixtures (defaultReduceContext, fixtureLambdas, linked, overdue, primitives)@@ -30,7 +30,7 @@ import Inference (Conclusion (Answered), Premises (Concludes, Morphs), direct) import Lambdas (Lambdas, emptyLambdas) import Matcher (substEmpty)-import Morph (Deadline (..), ReduceContext (..), declared, emptyState, enter, execBuildTerm, inferred, insideUniverse, morph, morph', voided)+import Morph (Deadline (..), ReduceContext (..), declared, emptyState, enter, execBuildTerm, factual, fired, inferred, insideUniverse, morph, morph', noted, voided) import Parser (Form (MONOFORM), parseExpressionThrows, parseExpressionThrows') import Rewriter (Rewritten) import Rule (RuleContext (RuleContext), matchExpressionWithRule')@@ -270,68 +270,112 @@       ctx <- defaultReduceContext ExRoot       morph expr emptyState ctx{_deadline = Just deadline}         `shouldThrow` (\e -> "--max-seconds=17" `isInfixOf` show (e :: SomeException))-    it "fails a partial morphing once the deadline has passed" $ do+    it "leaves a partial morphing in place once the deadline has passed" $ do       expr <- parseExpressionThrows "[[ q -> [[ D> 5A- ]] ]]"       deadline <- overdue 23       ctx <- defaultReduceContext ExRoot-      morph expr emptyState ctx{_deadline = Just deadline, _partial = True}-        `shouldThrow` (\e -> "--max-seconds=23" `isInfixOf` show (e :: SomeException))+      (residue, _, _) <- morph expr emptyState ctx{_deadline = Just deadline, _partial = True}+      residue `shouldBe` expr    describe "stops an entrance by the clock of --max-seconds" $     it "fails a comparison that outlasts the deadline" $ do       due <- (+ 0.2) <$> getMonotonicTime       let formation :: Expression -> Int -> Expression-          formation base depth = ExFormation [BiTau (AtLabel "x") (iterate (`ExDispatch` AtLabel "w") base !! depth), BiLambda (Function "L_q")]+          formation base depth = ExFormation [BiTau (AtLabel "x") (iterate (`ExDispatch` AtLabel "w") base !! depth), BiTau AtPhi ExRoot]       base <- defaultReduceContext ExRoot       ctx <- enter (formation ExRoot 1300) base{_acyclic = Just Plausible, _deadline = Just (Deadline 31 due)}       timeout 10000000 (enter (formation ExXi 1700) ctx)         `shouldThrow` (\e -> "--max-seconds=31" `isInfixOf` show (e :: SomeException)) +  describe "names a cut by the facts however wide they are" $+    it "names a cut held at the end of a wide fact long before the deadline" $ do+      let looping :: Expression+          looping = ExFormation [BiTau AtPhi (ExDispatch ExRoot (AtLabel "pz"))]+          wide :: Expression+          wide = ExFormation ([BiTau (AtLabel (T.pack ("w" ++ show index))) (ExFormation [BiTau (AtLabel (T.pack ("v" ++ show index))) (ExFormation [BiDelta (BtOne "5C")])]) | index <- [1 :: Int .. 30000]] ++ [BiTau (AtLabel "kq") looping])+      facts <- factual+      told <- newIORef []+      base <- defaultReduceContext ExRoot+      noted base{_facts = Just facts} wide (ExDispatch ExRoot (AtLabel "cq"))+      due <- (+ 2) <$> getMonotonicTime+      ctx <- enter looping base{_acyclic = Just Plausible, _maxLoops = 0, _facts = Just facts, _reckoning = True, _deadline = Just (Deadline 43 due), _saveEval = \record -> modifyIORef' told (record :)}+      _ <- timeout 10000000 (fired ExRoot ctx ExRoot emptyState looping)+      records <- readIORef told+      [answered | EvLooped _ _ _ _ _ (Just (_, answered)) <- records] `shouldBe` [Just (ExDispatch (ExDispatch ExRoot (AtLabel "cq")) (AtLabel "kq"))]+   describe "enters a formation again as many times as --max-loops allows" $ do     it "enters a formation holding the one entered above it under --max-loops=1" $ do       let formation :: Int -> Expression-          formation depth = ExFormation [BiTau (AtLabel "kv") (iterate (`ExDispatch` AtLabel "zu") ExRoot !! depth), BiLambda (Function "L_hop")]+          formation depth = ExFormation [BiTau (AtLabel "kv") (iterate (`ExDispatch` AtLabel "zu") ExRoot !! depth), BiTau AtPhi ExRoot]       base <- defaultReduceContext ExRoot       ctx <- enter (formation 4) =<< enter (formation 3) base{_acyclic = Just Plausible, _maxLoops = 1}       length (concat ctx._entered) `shouldBe` 2     it "cuts a formation holding the two entered above it under --max-loops=1" $ do       let formation :: Int -> Expression-          formation depth = ExFormation [BiTau (AtLabel "qe") (iterate (`ExDispatch` AtLabel "yo") ExRoot !! depth), BiLambda (Function "L_kit")]+          formation depth = ExFormation [BiTau (AtLabel "qe") (iterate (`ExDispatch` AtLabel "yo") ExRoot !! depth), BiTau AtPhi ExRoot]       base <- defaultReduceContext ExRoot       (enter (formation 7) =<< enter (formation 6) =<< enter (formation 5) base{_acyclic = Just Plausible, _maxLoops = 1})         `shouldThrow` (\e -> "already inside" `isInfixOf` show (e :: SomeException))+    it "enters a copy of an atom that only resembles the copy entered above it" $ do+      base <- defaultReduceContext ExRoot+      ctx <- enter (ExFormation [BiTau (AtLabel "t") (ExFormation [BiLambda (FnSymbol 4)]), BiLambda (Function "L_vo")]) =<< enter (ExFormation [BiTau (AtLabel "t") (ExDispatch ExRoot (AtLabel "pu")), BiLambda (Function "L_vo")]) base{_acyclic = Just Plausible, _maxLoops = 0}+      length (concat ctx._entered) `shouldBe` 2+    it "cuts a copy of an atom that repeats the copy entered above it exactly" $ do+      let formation :: Expression+          formation = ExFormation [BiTau (AtLabel "ka") (ExDispatch ExRoot (AtLabel "mi")), BiLambda (Function "L_ru")]+      base <- defaultReduceContext ExRoot+      (enter formation =<< enter formation base{_acyclic = Just Plausible, _maxLoops = 0})+        `shouldThrow` (\e -> "already inside" `isInfixOf` show (e :: SomeException))    describe "places a formation among the objects of the world" $ do     it "places a formation by the object the fact table maps it to" $ do       let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))-      facts <- newIORef (Map.fromList [(hashExpression (ExFormation [BiTau AtPhi body]), [(ExFormation [BiTau AtPhi body], ExDispatch ExRoot (AtLabel "nq"))])])+      facts <- factual       base <- defaultReduceContext ExRoot+      noted base{_facts = Just facts} (ExFormation [BiTau AtPhi body]) (ExDispatch ExRoot (AtLabel "nq"))       fmap fst <$> declared (ExFormation [BiTau (AtLabel "nq") (ExFormation [BiVoid AtPhi]), BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])         `shouldReturn` Just (ExDispatch ExRoot (AtLabel "nq"))     it "recalls every fact it follows on its way to the world, one by one" $ do       let head' = ExFormation [BiVoid (AtLabel "ru"), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]           copy = ExFormation [BiTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]), BiTau AtPhi (ExDispatch ExXi (AtLabel "ru"))]           applied = ExApplication head' (ArTau (AtLabel "ru") (ExFormation [BiLambda (FnSymbol 6)]))-      facts <- newIORef (Map.fromListWith (++) [(hashExpression term, [(term, source)]) | (term, source) <- [(head', ExDispatch ExRoot (AtLabel "vex")), (copy, applied)]])+      facts <- factual       told <- newIORef []       base <- defaultReduceContext ExRoot+      mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "vex")), (copy, applied)]       _ <- declared (ExFormation [BiTau (AtLabel "vex") head']) base{_facts = Just facts, _saveEval = \record -> modifyIORef' told (record :)} copy       records <- readIORef told       reverse [(term, reply) | EvRecalled _ term reply <- records] `shouldBe` [(copy, applied), (head', ExDispatch ExRoot (AtLabel "vex"))]+    it "recalls every fact of a circle of facts once, whatever symbol the copy holds" $ do+      let recalls :: Int -> IO Int+          recalls symbol = do+            let head' = ExFormation [BiVoid (AtLabel "ko"), BiLambda (Function "L_jew")]+                copy = ExFormation [BiTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]), BiLambda (Function "L_jew")]+                twin = ExFormation [BiTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]), BiLambda (Function "L_jew"), BiTau AtRho (ExDispatch ExRoot (AtLabel "jew"))]+                answer = ExFormation [BiTau AtPhi twin]+            facts <- factual+            told <- newIORef []+            base <- defaultReduceContext ExRoot+            mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "jew")), (copy, ExApplication head' (ArTau (AtLabel "ko") (ExFormation [BiLambda (FnSymbol symbol)]))), (answer, copy), (twin, ExDispatch answer AtPhi)]+            mapM_ (\index -> noted base{_facts = Just facts} (ExFormation [BiLambda (FnSymbol (symbol + index))]) (ExDispatch ExRoot (AtLabel "pad"))) [1 .. 12]+            _ <- declared (ExFormation [BiTau (AtLabel "jew") head']) base{_facts = Just facts, _saveEval = \record -> modifyIORef' told (record :)} answer+            (\records -> length [term | EvRecalled _ term _ <- records]) <$> readIORef told+      mapM recalls [3, 17 .. 700] `shouldReturn` replicate 50 3     it "answers the voids of the first head a chain of remembered copies was applied to" $ do       let head' = ExFormation [BiVoid (AtLabel "ka"), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]           half = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiVoid (AtLabel "mu"), BiLambda (Function "L_ozu")]           full = ExFormation [BiTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]), BiTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)]), BiLambda (Function "L_ozu")]-      facts <- newIORef (Map.fromListWith (++) [(hashExpression term, [(term, source)]) | (term, source) <- [(head', ExDispatch ExRoot (AtLabel "ozu")), (half, ExApplication head' (ArTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]))), (full, ExApplication half (ArTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)])))]])+      facts <- factual       base <- defaultReduceContext ExRoot+      mapM_ (uncurry (noted base{_facts = Just facts})) [(head', ExDispatch ExRoot (AtLabel "ozu")), (half, ExApplication head' (ArTau (AtLabel "ka") (ExFormation [BiLambda (FnSymbol 4)]))), (full, ExApplication half (ArTau (AtLabel "mu") (ExFormation [BiLambda (FnSymbol 9)])))]       voided base{_facts = Just facts} full `shouldReturn` Just [AtLabel "ka", AtLabel "mu"]     it "answers no voids for a formation the fact table does not hold" $ do-      facts <- newIORef Map.empty+      facts <- factual       base <- defaultReduceContext ExRoot       voided base{_facts = Just facts} (ExFormation [BiTau (AtLabel "pe") (ExFormation []), BiLambda (Function "L_uv")]) `shouldReturn` Nothing     it "places nothing the fact table does not map" $ do       let body = ExApplication (ExDispatch ExRoot (AtLabel "zuq")) (ArTau (AtLabel "wo") (ExFormation [BiLambda (FnSymbol 7)]))-      facts <- newIORef Map.empty+      facts <- factual       base <- defaultReduceContext ExRoot       fmap fst <$> declared (ExFormation [BiTau (AtLabel "kel") (ExFormation [BiTau AtPhi body])]) base{_facts = Just facts} (ExFormation [BiTau AtPhi body])         `shouldReturn` Nothing

@@ -113,6 +113,9 @@       , ("reads a back reference as a single digit", "\\10", ["full", "a"], "a0")       , ("keeps an out of bounds back reference literal", "\\9", ["only"], "\\9")       , ("keeps a digit after an escaped backslash literal", "\\\\1", ["full", "a"], "\\1")+      , ("substitutes the whole match for an ampersand", "<&>", ["full", "a"], "<full>")+      , ("keeps an escaped ampersand literal", "\\&", ["full"], "&")+      , ("substitutes the whole match after an escaped backslash", "\\\\&", ["full"], "\\full")       ]       ( \(desc, template, groups, expected) ->           it desc $ R.substituteGroups (utf8 template) (map utf8 groups) `shouldBe` utf8 expected

@@ -386,6 +386,18 @@       ( render (EXTRA (ARG_EXPR xiExpr) "evaluate" [ARG_ATTR (AT_LABEL "n")])           `shouldBe` "ξ \\coloneqq \\phinoEvaluate{ n }"       )+    forM_+      [ ("number", "\\phinoNumber{ n }")+      , ("string", "\\phinoString{ n }")+      , ("sum", "\\phinoSum{ n }")+      , ("tau", "\\phinoTau{ n }")+      , ("random-tau", "\\randomTau{ n }")+      ]+      ( \(fn, expected) ->+          it+            (fn ++ " does not collide with a TeX primitive or symbol")+            (render (EXTRA (ARG_EXPR xiExpr) fn [ARG_ATTR (AT_LABEL "n")]) `shouldBe` "ξ \\coloneqq " <> expected)+      )     it       "any other function becomes its own backslash macro"       ( render (EXTRA (ARG_EXPR xiExpr) "dataize" [ARG_ATTR (AT_LABEL "n")])

@@ -26,7 +26,7 @@ import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldNotContain, shouldReturn, shouldThrow) import Text.XML (Document (..), Element (..), Node (NodeElement), Prologue (..)) import Text.XML.Cursor qualified as C-import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirAtoms, xmirTime, xmirToPhi)+import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, renameAtoms, toName, xmirAtoms, xmirTime, xmirToPhi)  data ParsePack = ParsePack   { failure :: Maybe Bool@@ -225,6 +225,28 @@     it "stays unique when two paths spell alike, and keeps the type of each atom" $ do       doc <- parseXMIRThrows "<object><o name=\"top\"><o name=\"as-int\"><o atom=\"Φ.number\" name=\"λ\"/></o><o name=\"as_int\"><o atom=\"Φ.string\" name=\"λ\"/></o></o></object>"       xmirAtoms doc `shouldReturn` M.fromList [("L_top_as_int", "Φ.number"), ("L_top_as_int_2", "Φ.string")]++  describe "types of the voids of an atom in XMIR" $ do+    let alloc :: String+        alloc = "<object><o name=\"alloc\"><o base=\"∅\" name=\"size\" type=\"Φ.number\"/><o args=\"Φ.chunk\" base=\"∅\" name=\"scope\"/><o base=\"∅\" name=\"free\"/><o atom=\"Φ.bytes\" name=\"λ\"/></o></object>"+        printed :: IO String+        printed = do+          doc <- parseXMIRThrows alloc+          expr <- xmirToPhi doc+          atoms <- xmirAtoms doc+          printXMIR <$> expressionToXMIR expr (XmirContext True True False (const "") atoms)+    it "keeps @type of a void through a round trip" $+      printed >>= (`shouldContain` "<o base=\"∅\" name=\"size\" type=\"Φ.number\"/>")+    it "keeps @args of a void through a round trip" $+      printed >>= (`shouldContain` "<o args=\"Φ.chunk\" base=\"∅\" name=\"scope\"/>")+    it "adds nothing to a void without a type" $+      printed >>= (`shouldContain` "<o base=\"∅\" name=\"free\"/>")+    it "keeps the type when the λ function is renamed" $ do+      doc <- parseXMIRThrows alloc+      atoms <- xmirAtoms doc+      expr <- parseExpressionThrows "⟦ alloc ↦ ⟦ size ↦ ∅, scope ↦ ∅, free ↦ ∅, λ ⤍ Fn1 ⟧ ⟧"+      result <- expressionToXMIR expr (renameAtoms [("L_alloc", "Fn1")] (XmirContext True True False (const "") atoms))+      printXMIR result `shouldContain` "<o base=\"∅\" name=\"size\" type=\"Φ.number\"/>"    describe "atom result types in XMIR" $ do     let atom :: String

@@ -34,6 +34,21 @@ failsAsRedundant :: Either Yaml.ParseException a -> Bool failsAsRedundant = failsWith "redundant" +loadedFrom :: String -> String -> IO Rule+loadedFrom file content = do+  tmp <- getTemporaryDirectory+  bracket+    (openTempFile tmp file)+    (\(path, handle) -> hClose handle >> removeFile path)+    ( \(path, handle) -> do+        BS.hPut handle (encodeUtf8 (T.pack content))+        hClose handle+        yamlRule path+    )++quoted :: String -> String+quoted word = "'" ++ word ++ "'"+ spec :: Spec spec = do   describe "validates rewriting rule keys" $ do@@ -62,21 +77,22 @@   it "reads a bare y, n, yes, no, on and off in a rule file as the attributes they spell" $ do     let written :: (String -> String) -> String         written spelled = "name: bare-words\npattern: ⟦ 𝜏1 ↦ 𝑒1, 𝐵1 ⟧\nresult: ⟦ 𝐵1 ⟧\nwhen:\n  and:\n    - eq: [𝜏1, " ++ spelled "n" ++ "]\n    - in: [" ++ spelled "y" ++ ", 𝐵1]\n    - disjoint: [[" ++ intercalate ", " (map spelled ["yes", "no", "on", "off"]) ++ "], [𝐵1]]"-    tmp <- getTemporaryDirectory-    bare <--      bracket-        (openTempFile tmp "bare-words.yaml")-        (\(path, handle) -> hClose handle >> removeFile path)-        ( \(path, handle) -> do-            BS.hPut handle (encodeUtf8 (T.pack (written id)))-            hClose handle-            yamlRule path-        )+    bare <- loadedFrom "bare-words.yaml" (written id)     show bare       `shouldBe` either         Yaml.prettyPrintParseException         (show :: Rule -> String)-        (decodeYaml' (written (\word -> "'" ++ word ++ "'")))+        (decodeYaml' (written quoted))++  it "reads a bare ASCII meta in a rule file as the meta it spells" $ do+    let written :: (String -> String) -> String+        written spelled = "name: bare-metas\npattern: ⟦ φ ↦ !e1, !t1 ↦ !e2, !B1 ⟧.!t2\nresult: " ++ spelled "!e1" ++ "\nwhen:\n  and:\n    - nf: " ++ spelled "!e2" ++ "\n    - not:\n        eq:\n          - " ++ spelled "!t1" ++ "\n          - " ++ spelled "!t2" ++ "\n    - not:\n        in:\n          - " ++ spelled "!t2" ++ "\n          - " ++ spelled "!B1"+    bare <- loadedFrom "bare-metas.yaml" (written id)+    show bare+      `shouldBe` either+        Yaml.prettyPrintParseException+        (show :: Rule -> String)+        (decodeYaml' (written quoted))    describe "fails on yaml typos" $ do     let resources = "test-resources/yaml-typos"