diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ ```bash cabal update -cabal install --overwrite-policy=always phino-0.0.115 +cabal install --overwrite-policy=always phino-0.0.118 phino --version ``` @@ -404,6 +404,60 @@ `--sequence`, `--headers`, `--steps-dir`, `--evaluations`, `--partial`, `--max-steps`, `--shuffle`/`--seed`, `--output`, `--focus` and the rest. +### Deep morphing + +𝕄 stops at the first formation it reaches and hands its bindings back as they +were written, since firing a bare λ is dataization's job, and `dataize` +follows the one path dataization demands and ends in bytes. What a program +holds but nothing demands — the argument of an atom the registry does not +serve, for one — is therefore reduced by neither. The `--deep` flag enters it: + +```bash +$ cat gap.phi +⟦ + bytes(data) ↦ ⟦ φ ↦ ξ.data ⟧, + number(as-bytes) ↦ ⟦ φ ↦ ξ.as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, + bar(x) ↦ ⟦ λ ⤍ L_bar ⟧, + demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( ξ.n.times( 5 ).times( 7 ) ) ⟧ ⟧ +⟧ +$ phino morph --atoms=atoms.json --inside='Q.demo.foo' \ + --sweet --hide-rho gap.phi +⟦ n ↦ 3, φ ↦ Φ.bar( n.times( 5 ).times( 7 ) ) ⟧ +$ phino morph --deep --atoms=atoms.json --inside='Q.demo.foo' \ + --sweet --hide-rho gap.phi +⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧ +``` + +Every binding of the formation is entered, recursively. 𝕄 is asked about the +term standing there and, where it lands on a saturated formation whose λ the +registry serves, that λ is fired and 𝕄 is asked about the answer again. A term +on whose way an atom fired is replaced by the answer of the last firing, which +is the 𝜑-program the atom wrote rather than the normal form of it, so `105` +stands where the arithmetic stood. A term no atom touched stays exactly as it +was written and only its own parts are walked, so `Φ.bar` keeps its name and +what comes back is still the same program, reduced as far as the registry +allows. The step joins the chain under the name `deep`, so `--sequence` shows +it, and `--max-steps` bounds the walk. + +Two things are left alone. A λ the registry does not serve is not fired at +all, so `--deep` stays as total as 𝕄 itself and needs no `--partial`; an atom +that gets stuck deeper on a spine still fails the run, and `--partial` parks +it, leaving that term as it was written. A formation still holding a void +binding is not fired either: the void is an argument the program has not given +yet, so `times(x) ↦ ⟦ λ ⤍ L_number_times ⟧` is a method waiting to be applied, +not an application waiting to be computed. Walking the whole program therefore +folds what it can and leaves the object model as it was declared: + +```bash +$ phino morph --deep --atoms=atoms.json --sweet --hide-rho gap.phi +⟦ + bytes(data) ↦ ⟦ φ ↦ data ⟧, + number(as-bytes) ↦ ⟦ φ ↦ as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧, + bar(x) ↦ ⟦ λ ⤍ L_bar ⟧, + demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧ ⟧ +⟧ +``` + ## Rewrite You can rewrite this expression with the help of [rules](#rule-structure) @@ -788,55 +842,55 @@ === parse/phi === warmup: 3 iterations batches: 10 x 1 - total: 1781621.932 μs - avg: 178162.193 μs - min: 163679.993 μs - max: 209804.570 μs - std dev: 17409.000 μs + total: 1598588.273 μs + avg: 159858.827 μs + min: 147759.554 μs + max: 193999.679 μs + std dev: 17143.300 μs === parse/xmir === warmup: 3 iterations batches: 10 x 1 - total: 7611171.011 μs - avg: 761117.101 μs - min: 679176.096 μs - max: 899930.605 μs - std dev: 69464.089 μs + total: 7813131.215 μs + avg: 781313.122 μs + min: 724999.135 μs + max: 842487.724 μs + std dev: 32948.399 μs === rewrite/normalize === warmup: 3 iterations batches: 10 x 1 - total: 811837.328 μs - avg: 81183.733 μs - min: 67331.161 μs - max: 92232.373 μs - std dev: 8117.233 μs + total: 1071335.155 μs + avg: 107133.516 μs + min: 82715.009 μs + max: 127072.342 μs + std dev: 15148.984 μs === print/sweet/multiline === warmup: 3 iterations batches: 10 x 1 - total: 4199718.146 μs - avg: 419971.815 μs - min: 396063.240 μs - max: 442595.822 μs - std dev: 16504.492 μs + total: 4764374.575 μs + avg: 476437.457 μs + min: 443528.234 μs + max: 508780.337 μs + std dev: 21790.459 μs === print/sweet/flat === warmup: 3 iterations batches: 10 x 1 - total: 4060839.345 μs - avg: 406083.934 μs - min: 387257.807 μs - max: 417907.724 μs - std dev: 8861.891 μs + total: 4829704.670 μs + avg: 482970.467 μs + min: 444530.419 μs + max: 514344.452 μs + std dev: 23249.943 μs === print/salty/multiline === warmup: 3 iterations batches: 10 x 1 - total: 14257603.693 μs - avg: 1425760.369 μs - min: 1405945.748 μs - max: 1449825.539 μs - std dev: 11882.320 μs + total: 14789056.654 μs + avg: 1478905.665 μs + min: 1426640.434 μs + max: 1589233.894 μs + std dev: 46147.565 μs ``` The results were calculated in [this GHA job][benchmark-gha] -on 2026-09-07 at 19:51, +on 2026-09-08 at 20:28, on Linux with 4 CPUs. @@ -885,4 +939,4 @@ [jna]: https://github.com/java-native-access/jna [jna-native]: https://github.com/java-native-access/jna/blob/master/src/com/sun/jna/Native.java [jeo]: https://github.com/objectionary/jeo-maven-plugin -[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/34156988456 +[benchmark-gha]: https://github.com/objectionary/phino/actions/runs/34274639466 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.118 +version: 0.0.119 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/normalize/alpha.yaml b/resources/normalize/alpha.yaml --- a/resources/normalize/alpha.yaml +++ b/resources/normalize/alpha.yaml @@ -5,6 +5,11 @@ pattern: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(α𝑖1 ↦ 𝑒1) result: ⟦𝐵1, 𝜏1 ↦ ∅, 𝐵2⟧(𝜏1 ↦ 𝑒1) when: - eq: - - 𝑖1 - - domain: 𝐵1 + and: + - eq: + - 𝑖1 + - domain: 𝐵1 + - not: + eq: + - 𝜏1 + - ρ diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -206,6 +206,12 @@ optPartial :: Parser Bool optPartial = switch (long "partial" <> help "Partial evaluation: compute what the known inputs decide and, instead of failing on an atom that cannot fire (its λ function is not in the --atoms registry), leave it in place and print the residual 𝜑-program") +-- 𝕄 stops at the first formation it reaches and hands its bindings back as +-- they were written, so what a program holds but nothing demands is never +-- reduced. This walks into them (see 'deepened'). +optDeep :: Parser Bool +optDeep = switch (long "deep" <> help "Don't stop at the first formation: enter its bindings too, recursively, firing every λ function the --atoms registry serves and standing its answer in the place of what it computed, while everything else stays as it was written") + -- Which λ functions this run may fire. phino implements none of them itself -- (see 'Atoms'), so without this option every atom a program names gets stuck. optAtoms :: Parser (Maybe FilePath) @@ -376,6 +382,7 @@ <*> optSeed <*> switch (long "quiet" <> help "Don't print the result of morphing") <*> optPartial + <*> optDeep <*> optCompress <*> optMaxDepth <*> optMaxCycles diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -165,7 +165,9 @@ _evaluations printCtx ( \record -> do - let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record + -- The deep walk belongs to 𝕄 alone (the '--deep' of 'morph'), since 𝔻 + -- reduces what dataization demands and ends in bytes, so it is off here. + let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial False atoms buildTerm save record (universe, aiming) <- aimed _inside expr ctx dataize universe aiming ) @@ -245,7 +247,7 @@ _evaluations printCtx ( \record -> do - let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial atoms buildTerm save record + let ctx = DataizeContext loc _maxDepth _maxCycles (Steps _maxSteps 0) _depthSensitive _shuffle _partial _deep atoms buildTerm save record (universe, aiming) <- aimed _inside expr ctx morph universe aiming ) diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -140,6 +140,7 @@ , _seed :: Int , _quiet :: Bool , _partial :: Bool + , _deep :: Bool , _compress :: Bool , _maxDepth :: Int , _maxCycles :: Int diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -11,7 +11,7 @@ module CST where import AST -import Bytes (NonFinite, btsToNonFinite, btsToNum, btsToStr) +import Bytes (NonFinite, btsSize, btsToNonFinite, btsToNum, btsToStr) import Data.Maybe (isJust) import qualified Data.Text as T import qualified Yaml as Y @@ -270,6 +270,8 @@ -- pattern, such as a NaN carrying a payload, is kept in its byte form so that -- no bit of it is lost. sweetNumber :: Bytes -> Bool +sweetNumber bts + | btsSize bts /= 8 = False sweetNumber bts = case btsToNum bts of Right dbl | isNaN dbl || isInfinite dbl -> isJust (btsToNonFinite bts) _ -> True diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -14,12 +14,13 @@ import AST import Atoms (Registry, fireAtom, registeredAtom) -import Builder (buildBytesThrows, buildExpressionThrows) +import Builder (buildBytesThrows, buildExpressionThrows, contextualize) import Control.Exception (Exception, catch, throwIO, try) import Control.Monad (foldM, when) import Data.List (find, partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE +import Data.Maybe (fromMaybe) import qualified Data.Text as T import Deps (BuildTermFunc, BuildTermMethodS, Evaluation (..), SaveEvalFunc, SaveStepFunc, State, Term (..)) import Locator (locatedExpression, withLocatedExpression) @@ -74,6 +75,7 @@ , _depthSensitive :: Bool , _shuffle :: Bool , _partial :: Bool + , _deep :: Bool , _atoms :: Registry , _buildTerm :: BuildTermFunc , _saveStep :: SaveStepFunc @@ -134,6 +136,23 @@ isLambda (BiLambda _) = True isLambda _ = False +-- The same as 'lambda', but only for a formation that is saturated: one with no +-- void binding left in it. A void is an argument the program has not given yet, +-- so such a formation is a method waiting to be applied rather than an +-- application waiting to be computed, and firing it would hand the atom a ∅ +-- where it expects a value. 𝔻 needs no such guard, since it fires only what +-- dataization demands and nothing demands a method; the deep walk meets every +-- one a program declares — the method table of the object model above all — so +-- it asks first (see 'deepened'). +saturated :: [Binding] -> Maybe (T.Text, Expression) +saturated bds = case lambda bds of + Just (func, ExFormation rest) | all filled rest -> Just (func, ExFormation rest) + _ -> Nothing + where + filled :: Binding -> Bool + filled (BiVoid _) = False + filled _ = True + -- Run one frame of the 𝕄/𝔻 spine, attaching its derivation to a stuck atom -- escaping it. 'Stuck' is raised deep inside an atom, which knows nothing about -- the chain, so the innermost spine frame it reaches is the one to record where @@ -242,19 +261,157 @@ -- with the terminator ⊥ ('dead', 'xi', 'mg', 'mad', 'maad') rather than failing. -- Only the atoms 'ml' fires can still get stuck, and '_partial' parks them just -- as it does under 𝔻: the answer is then the residual subterm the spine had --- reached, taken from '_locator' of its working expression. +-- reached, taken from '_locator' of its working expression. Stopping at the +-- first formation leaves everything that formation holds as it was written, +-- which is what '_deep' walks into before the answer is handed back (see +-- 'deepened'). morph :: Expression -> DataizeContext -> IO (Expression, [Rewritten]) morph universe ctx@DataizeContext{..} = do expr <- locatedExpression _locator universe - -- Morphing starts from the empty state; the final state is not yet - -- consumed by any caller, so it is discarded here. result <- try (morph' (expr, (universe, Nothing) :| []) universe emptyState ctx) case result of - Right ((morphed, seq), _state) -> pure (morphed, reverse (NE.toList seq)) + Right ((morphed, seq), state) -> walked morphed seq state Left (StuckAt _ seq) | _partial -> do residue <- locatedExpression _locator (fst (NE.head seq)) - pure (residue, reverse (NE.toList seq)) + walked residue seq emptyState Left failure -> throwIO (failure :: DataizeException) + where + -- The answer 𝕄 reached, walked by '_deep' before it is handed back (see + -- 'deepened'), and the chain that led to both. The walk joins the chain as + -- one step named 'deep', so '--sequence' ends on the term the command + -- prints. Morphing starts from the empty state and the state the walk ends + -- on goes the way 𝕄's own goes: no caller consumes it yet. + walked :: Expression -> NonEmpty Rewritten -> State -> IO (Expression, [Rewritten]) + walked morphed seq state + | not _deep = pure (morphed, reverse (NE.toList seq)) + | otherwise = do + (deep, _) <- deepened morphed universe state ctx + seq' <- leadsTo seq "deep" deep ctx + pure (deep, reverse (NE.toList seq')) + +-- Walk what 𝕄 answered with, entering everything it left as it was written — +-- the mechanism behind '--deep' ('_deep'). 𝕄 navigates a term to the first +-- formation it reaches and 'mf' hands that formation back with its bindings +-- untouched, since firing a bare λ is 𝔻's business; 𝔻 in turn follows the one +-- path dataization demands and ends in bytes. A part of a program that nothing +-- demands — the argument of an atom that cannot fire, for one — is therefore +-- reduced by neither, and the object structure is lost to the one that does +-- reduce it (#1124). This walk demands nothing either. It asks 𝕄 about every +-- sub-expression and, where 𝕄 lands on a formation whose λ the registry +-- serves, fires it and asks 𝕄 about the answer again (see 'fired'). A +-- sub-expression on whose way an atom fired is replaced by the answer of the +-- last firing; where none fired it stays as it was written and only its own +-- parts are walked, so the calls the registry does not serve keep their names +-- and what comes back is still the same program, reduced as far as the +-- registry allows. Every entry is charged to the '--max-steps' budget, which +-- is what bounds the walk. +deepened :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) +deepened expr univ = go ExXi expr + where + -- A term as it was written, together with what its free ξ stands for: the + -- formation the walk entered it from, without the binding it came from, + -- exactly the context the 'dot' rule hands a dispatched body. At the top + -- there is no such formation, so ξ stands for itself and contextualization + -- leaves the term alone. + go :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) + go context term state' caller = do + ctx' <- deeper caller + answer <- fired (contextualize term context) univ state' ctx' + maybe (parts context term state' ctx') pure answer + -- The parts of a term nothing fired on, walked one by one and put back + -- where they were, so the term keeps the shape it was written in. + parts :: Expression -> Expression -> State -> DataizeContext -> IO (Expression, State) + parts _ (ExFormation bds) state' caller = do + (entered, state'') <- bindings bds bds state' caller + pure (ExFormation entered, state'') + parts context (ExDispatch target attr) state' caller = do + (entered, state'') <- go context target state' caller + pure (ExDispatch entered attr, state'') + parts context (ExApplication target arg) state' caller = do + (entered, state'') <- go context target state' caller + (applied, state''') <- argument context arg state'' caller + pure (ExApplication entered applied, state''') + parts _ term state' _ = pure (term, state') + -- Walk the bindings of a formation left to right, threading the state + -- through them. Only what the formation itself holds is entered: ρ names + -- the object around it rather than one inside it, and a void, Δ or λ + -- binding carries no term to walk at all. + bindings :: [Binding] -> [Binding] -> State -> DataizeContext -> IO ([Binding], State) + bindings _ [] state' _ = pure ([], state') + bindings whole (BiTau attr body : rest) state' caller + | attr /= AtRho = do + (entered, state'') <- go (scope attr whole) body state' caller + (others, state''') <- bindings whole rest state'' caller + pure (BiTau attr entered : others, state''') + bindings whole (bd : rest) state' caller = do + (others, state'') <- bindings whole rest state' caller + pure (bd : others, state'') + -- The context a binding's body is entered in: the formation without that + -- binding, the very context 'dot' contextualizes a dispatched body in, so + -- a body reaching back at itself through ξ collapses instead of looping. + scope :: Attribute -> [Binding] -> Expression + scope attr bds = ExFormation (filter (not . named) bds) + where + named :: Binding -> Bool + named (BiTau attr' _) = attr' == attr + named _ = False + -- Both sides of an application stand in the same context: the term it + -- applies is walked by the caller and the argument it binds is walked here. + argument :: Expression -> Argument -> State -> DataizeContext -> IO (Argument, State) + argument context (ArTau attr arg) state' caller = do + (entered, state'') <- go context arg state' caller + pure (ArTau attr entered, state'') + argument context (ArAlpha alpha arg) state' caller = do + (entered, state'') <- go context arg state' caller + pure (ArAlpha alpha entered, state'') + +-- Ask 𝕄 about a term and fire the λ of the formation it reaches, as long as +-- the registry serves it, asking 𝕄 about every answer again: what comes back +-- is the answer of the last firing, or nothing at all where no atom fired. This +-- is the firing 'ml' makes without the dispatch that makes 'ml' make it — the +-- one 𝕄 leaves to 𝔻 — except in what it hands back: the atom's raw answer, not +-- the normal form 𝔼 makes of it, since the deep walk stands that answer back +-- into the program, where a normal form would spell the whole object out in +-- place of the name the program called it by. A λ the registry does not carry +-- is left alone rather than fired and got stuck on, so what phino cannot +-- compute stays as it was written with or without '_partial'; an atom that +-- cannot fire deeper on the spine still fails the run, exactly as it does +-- under 𝕄 alone, and '_partial' parks it. A formation still waiting for its +-- arguments is left alone too (see 'saturated'). +fired :: Expression -> Expression -> State -> DataizeContext -> IO (Maybe (Expression, State)) +fired term univ state caller = do + ctx <- deeper caller + morphed <- try (reduced ctx) + case morphed of + Right (ExFormation bds, state') -> maybe (pure Nothing) (evaluated ctx state') (saturated bds) + Right _ -> pure Nothing + Left failure -> parked failure + where + -- 𝕄 takes normal forms only and a term taken from the program as it was + -- written is not necessarily one, so it is normalized against the universe + -- first, exactly as '--inside' normalizes what it is handed. Both chains + -- are dropped: the walk is not the spine and reports one step of its own + -- (see 'morph'), so a stuck atom leaves without a derivation ('unparked'). + reduced :: DataizeContext -> IO (Expression, State) + reduced ctx = unparked $ do + (normal, _) <- normalized term ((univ, Nothing) :| []) ctx + ((morphed, _), state') <- morph' (normal, (univ, Nothing) :| []) univ state ctx + pure (morphed, state') + -- Fire the λ of the formation 𝕄 reached and go on from its answer, keeping + -- the answer of the last firing. The firing is reported to '_saveEval' like + -- every other one, with the term the caller is given, so the protocol and + -- the program agree on what the atom answered. + evaluated :: DataizeContext -> State -> (T.Text, Expression) -> IO (Maybe (Expression, State)) + evaluated ctx state' (func, self) = case registeredAtom ctx._atoms func of + Nothing -> pure Nothing + Just registered -> do + answer <- fireAtom func registered self univ + ctx._saveEval (Evaluation func self (Just answer)) + again <- fired answer univ state' ctx + pure (Just (fromMaybe (answer, state') again)) + parked :: DataizeException -> IO (Maybe a) + parked (Stuck _) | caller._partial = pure Nothing + parked failure = throwIO failure -- Dataize the expression located at '_locator'. The whole input expression is -- itself the universe Q (the 'e' argument) threaded through 𝔻 and 𝕄, so it is diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -169,7 +169,10 @@ _string [Y.ArgExpression expr] subst = do expr' <- buildExpressionThrows expr subst str <- case expr' of - DataNumber bts -> pure (DataString (strToBts (either show show (btsToNum bts)))) + DataNumber bts + | btsSize bts /= 8 -> + throwIO (userError (printf "Expected 8 bytes for a number, got %d" (btsSize bts))) + | otherwise -> pure (DataString (strToBts (either show show (btsToNum bts)))) DataString bts -> pure (DataString bts) ex -> throwIO diff --git a/src/Rule.hs b/src/Rule.hs --- a/src/Rule.hs +++ b/src/Rule.hs @@ -125,6 +125,7 @@ where notAsset (BiDelta _) = False notAsset (BiLambda _) = False + notAsset (BiVoid AtRho) = False notAsset _ = True numToInt (Y.Literal num) _ = Just num numToInt _ _ = Nothing diff --git a/src/XMIR.hs b/src/XMIR.hs --- a/src/XMIR.hs +++ b/src/XMIR.hs @@ -22,7 +22,7 @@ where import AST -import Bytes (btsToNum, btsToStr, bytesToBts) +import Bytes (btsSize, btsToNum, btsToStr, bytesToBts) import Control.Exception (Exception (displayException), throwIO) import Data.Bifunctor (bimap) import Data.Foldable (foldlM) @@ -97,6 +97,7 @@ expression :: Expression -> XmirContext -> IO (String, [Node]) expression ExXi _ = pure (printExpression ExXi, []) expression ExRoot _ = pure (printExpression ExRoot, []) +expression ExTermination _ = pure ("⊥", []) expression (ExFormation bds) ctx = do nested <- nestedBindings bds ctx pure ("", nested) @@ -116,7 +117,7 @@ [object [("as", "data")] [NodeContent (T.pack (printBytes bytes))]] in pure ( "Φ.number" - , if _omitComments + , if _omitComments || btsSize bytes /= 8 then [bts] else [ NodeComment (T.pack (either show show (btsToNum bytes))) @@ -484,6 +485,10 @@ if null (cur C.$/ C.element (toName "o")) then pure ExRoot else throwIO (InvalidXMIRFormat "Application of 'Φ' is illegal in XMIR" cur) + "⊥" -> + if null (cur C.$/ C.element (toName "o")) + then pure ExTermination + else throwIO (InvalidXMIRFormat "Application of '⊥' is illegal in XMIR" cur) 'Φ' : '.' : rest -> xmirToExpression' ExRoot "Φ" rest cur fqn 'ξ' : '.' : rest -> xmirToExpression' ExXi "ξ" rest cur fqn _ -> throwIO (InvalidXMIRFormat "The @base attribute must be either ['∅'|'Φ'] or start with ['Φ.'|'ξ.'|'.']" cur) diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -1502,6 +1502,64 @@ ["morph", "--locator=Q.@", "--partial", "--flat", "--hide-rho"] ["⟦ λ ⤍ Sym_arg_0 ⟧.foo"] + -- 𝕄 stops at the first formation and hands its bindings back as they were + -- written, so a program whose parts nothing demands is never reduced; + -- '--deep' enters every binding and finishes what 'mf' left, while what no + -- atom touched keeps its name and the answer stays a program (#1124) + describe "--deep" $ do + let program = + "[[ bytes(data) -> [[ @ -> $.data ]], \ + \number(as-bytes) -> [[ @ -> $.as-bytes, times(x) -> [[ L> L_number_times ]] ]], \ + \bar(x) -> [[ L> L_bar ]], \ + \demo -> [[ foo -> [[ n -> 3, @ -> Q.bar( $.n.times( 5 ).times( 7 ) ) ]] ]] ]]" + it "answers the formation as it was written without the flag" $ + withAtoms $ \atoms -> + withStdin program $ + testCLISucceeded + ["morph", atoms, "--inside=Q.demo.foo", "--sweet", "--hide-rho", "--flat"] + ["⟦ n ↦ 3, φ ↦ Φ.bar( n.times( 5 ).times( 7 ) ) ⟧"] + + -- 'L_bar' is not in the registry, so the call to it stays as written and + -- keeps its name, while the arithmetic in the argument nothing demands + -- folds into the number it makes + it "reduces every binding it can and leaves the rest in place" $ + withAtoms $ \atoms -> + withStdin program $ + testCLISucceeded + ["morph", atoms, "--deep", "--inside=Q.demo.foo", "--sweet", "--hide-rho", "--flat"] + ["⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧"] + + -- The same term the run above stops at as a bare λ-formation: 'mf' leaves + -- it to 𝔻, and the walk fires it instead of demanding bytes + it "fires the bare saturated λ-formation mf hands back" $ + withAtoms $ \atoms -> + withStdin chained $ + testCLISucceeded + ["morph", atoms, "--deep", "--locator=Q.@", "--sweet", "--hide-rho", "--flat"] + ["18"] + + -- The default locator walks the whole program: the method table of the + -- object model keeps every one of its λ-formations, since not one of them + -- is saturated, while the one place that can be computed is + it "keeps the object model intact while it folds the program" $ + withAtoms $ \atoms -> + withStdin program $ + testCLISucceeded + ["morph", atoms, "--deep", "--sweet", "--hide-rho", "--flat"] + [ "number(as-bytes) ↦ ⟦ φ ↦ as-bytes, times(x) ↦ ⟦ λ ⤍ L_number_times ⟧ ⟧" + , "demo ↦ ⟦ foo ↦ ⟦ n ↦ 3, φ ↦ Φ.bar( 105 ) ⟧ ⟧" + ] + + it "keeps a binding whose spine got stuck with --partial" $ + withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $ + testCLISucceeded + ["morph", "--deep", "--partial", "--sweet", "--hide-rho", "--flat"] + ["⟦ x ↦ ⟦ λ ⤍ Sym_arg_0 ⟧.foo ⟧"] + + it "fails on that same spine without --partial" $ + withStdin "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" $ + testCLIFailed ["morph", "--deep"] ["Atom 'Sym_arg_0' does not exist"] + describe "fails" $ do it "with --output != latex and --nonumber" $ withStdin "" $ @@ -1586,7 +1644,7 @@ [ "\\phinoNormalizationRule{alpha}" , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\phiTerminal{\\alpha_{i1}} -> e_1 ) }" , " { [[ B_1, \\tau_1 -> ?, B_2 ]] ( \\tau_1 -> e_1 ) }" - , " { i_1 = \\vert \\overline{ B_1 } \\vert }" + , " { i_1 = \\vert \\overline{ B_1 } \\vert \\;\\text{and}\\; \\tau_1 \\not= \\phiTerminal{\\rho} }" , " { }" , "\\phinoNormalizationRule{amiss}" , " { [[ B_1 ]] ( \\phiTerminal{\\alpha_{i1}} -> e ) }" diff --git a/test/CSTSpec.hs b/test/CSTSpec.hs --- a/test/CSTSpec.hs +++ b/test/CSTSpec.hs @@ -150,6 +150,8 @@ , ("is true for negative infinity", BtMany ["FF", "F0", "00", "00", "00", "00", "00", "00"], True) , ("is false for a NaN carrying a payload", BtMany ["7F", "F8", "00", "00", "00", "00", "00", "01"], False) , ("is false for the negative quiet NaN", BtMany ["FF", "F8", "00", "00", "00", "00", "00", "00"], False) + , ("is false for fewer than eight bytes", BtOne "21", False) + , ("is false for empty bytes", BtEmpty, False) ] (\(desc, bts, expected) -> it desc (sweetNumber bts `shouldBe` expected)) diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -32,7 +32,7 @@ -- empty, since phino implements none of them: a case that needs an atom to -- answer brings the fixture registry in through 'withAtoms'. defaultDataizeContext :: Expression -> DataizeContext -defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval +defaultDataizeContext loc = DataizeContext loc 25 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval -- The same context with the fixture λ functions registered (see 'Fixtures'). withAtoms :: Registry -> DataizeContext -> DataizeContext @@ -71,6 +71,20 @@ (morphed, _) <- morph expr (defaultDataizeContext loc') morphed `shouldBe` expected +-- The same as 'testMorph', with the deep walk on ('_deep') and the fixture λ +-- functions registered, since a case that reduces anything has to fire one: it +-- is pending where 'node' is not installed. +testDeep :: Registry -> [(String, String, String, String)] -> Spec +testDeep registry useCases = + forM_ useCases $ \(name, loc, src, res) -> + it name $ + withNode $ do + expr <- parseExpressionThrows src + loc' <- parseExpressionThrows loc + expected <- parseExpressionThrows res + (morphed, _) <- morph expr (withAtoms registry (defaultDataizeContext loc')){_deep = True} + morphed `shouldBe` expected + -- The EO objects the fixture λ functions answer for, declared the way -- 'number.eo' and 'bytes.eo' declare them, so a case below only has to spell -- the expression under φ. 'number.eq' is the one operation with no atom of its @@ -196,6 +210,78 @@ (residue, _) <- morph expr (defaultDataizeContext loc){_partial = True} residue `shouldBe` expected + -- 𝕄 stops at the first formation 'mf' hands back and leaves its bindings as + -- they were written, since firing a bare λ is 𝔻's business, so a program + -- whose parts nothing demands is never reduced (#1124). The deep walk + -- ('_deep') enters every binding and finishes what 'mf' left, while what no + -- atom touched keeps the shape it was written in and the answer stays a + -- program. + describe "morph with '_deep'" $ do + testDeep + registry + [ + ( "stands the answer of the λ that 'mf' left bare in its place" + , "Q.@" + , primitives "[[ x -> 5.plus( 6 ) ]]" + , "[[ x -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-26-00-00-00-00-00-00 ]] ) ) ]]" + ) + , + ( "keeps the answer of the last atom fired along one chain of them" + , "Q.@" + , primitives "[[ x -> 5.plus( 6 ).plus( 7 ) ]]" + , "[[ x -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-32-00-00-00-00-00-00 ]] ) ) ]]" + ) + , + ( "resolves the ξ of a binding against the formation that holds it" + , "Q.@" + , primitives "[[ n -> 5, x -> $.n.plus( 6 ) ]]" + , "[[ n -> 5, x -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-26-00-00-00-00-00-00 ]] ) ) ]]" + ) + , -- The registry carries no 'L_number_nope', so there is nothing to fire + -- and the binding keeps the name it was written under + + ( "leaves the λ the registry does not serve as it was written" + , "Q.@" + , primitives "[[ x -> 5.nope ]]" + , "[[ x -> 5.nope ]]" + ) + , -- A λ-formation whose bindings are still void is a method waiting to be + -- applied, not an application waiting to be computed: nothing demands + -- one, so 𝔻 never meets one, while the walk meets every one the object + -- model declares. Both the void ρ of 'not' and the void 'b' of 'eq' + -- keep their atoms unfired here. + + ( "leaves a λ-formation still waiting for its arguments alone" + , "Q.bytes" + , primitives "[[ ]]" + , "[[ data -> ?, @ -> $.data, not -> [[ L> L_bytes_not ]], eq -> [[ b -> ?, L> L_bytes_eq ]] ]]" + ) + , -- Nothing demands the argument of an atom that cannot fire, so 𝔻 never + -- reaches it; the walk does, and the atom around it stays in place + + ( "walks into the argument of an atom it cannot fire" + , "Q.@" + , primitives "[[ x -> [[ y -> ?, L> L_bar ]]( y -> 6.plus( 7 ) ) ]]" + , "[[ x -> [[ y -> ?, L> L_bar ]]( y -> Q.number( as-bytes -> Q.bytes( data -> [[ D> 40-2A-00-00-00-00-00-00 ]] ) ) ) ]]" + ) + ] + + -- An atom deeper on a binding's spine gets stuck exactly as it does under + -- 𝕄 alone: the run fails, unless '_partial' parks it, and then the binding + -- stays as it was written and the walk goes on + describe "a stuck atom on the spine of a binding" $ do + let stuck :: IO Expression + stuck = parseExpressionThrows "[[ x -> [[ L> Sym_arg_0 ]].foo ]]" + it "fails the run without '_partial'" $ do + expr <- stuck + morph expr (defaultDataizeContext ExRoot){_deep = True} + `shouldThrow` (\e -> "Atom 'Sym_arg_0' does not exist" `isInfixOf` show (e :: SomeException)) + + it "leaves the binding as it was written under '_partial'" $ do + expr <- stuck + (morphed, _) <- morph expr (defaultDataizeContext ExRoot){_deep = True, _partial = True} + morphed `shouldBe` expr + describe "morph'" $ test' morph' @@ -487,7 +573,7 @@ it "fails on the step limit instead of morphing forever" $ withNode $ do expr <- parseExpressionThrows "⟦ @ ↦ ⟦ λ ⤍ L_number_div, ρ ↦ ⟦ Δ ⤍ 40-45-00-00-00-00-00-00 ⟧, x ↦ ⟦ Δ ⤍ 40-00-00-00-00-00-00-00 ⟧ ⟧ ⟧" - dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False registry buildTerm dontSaveStep dontSaveEval) + dataize expr (DataizeContext ExRoot 25 25 (Steps 40 0) False True False False registry buildTerm dontSaveStep dontSaveEval) `shouldThrow` (\e -> "--max-steps=40" `isInfixOf` show (e :: SomeException)) -- An atom phino does not know — a name the '--atoms' registry does not carry, @@ -551,12 +637,12 @@ forM_ [ ( "--max-cycles" - , DataizeContext ExRoot 25 0 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval + , DataizeContext ExRoot 25 0 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval , "--max-cycles=0" ) , ( "--max-depth" - , DataizeContext ExRoot 0 25 (Steps 250 0) True True False emptyRegistry buildTerm dontSaveStep dontSaveEval + , DataizeContext ExRoot 0 25 (Steps 250 0) True True False False emptyRegistry buildTerm dontSaveStep dontSaveEval , "--max-depth=0" ) ] @@ -566,8 +652,8 @@ dataize expr ctx `shouldThrow` (\e -> message `isInfixOf` show (e :: SomeException)) ) forM_ - [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval) - , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False emptyRegistry buildTerm dontSaveStep dontSaveEval) + [ ("--max-cycles", DataizeContext ExRoot 25 0 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval) + , ("--max-depth", DataizeContext ExRoot 0 25 (Steps 250 0) False True False False emptyRegistry buildTerm dontSaveStep dontSaveEval) ] ( \(flag, ctx) -> it ("does not throw without --depth-sensitive even once " ++ flag ++ " is exhausted") $ do diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -102,6 +102,20 @@ parseExpression printed `shouldBe` Right expr ) + describe "printExpression keeps a number with fewer than eight bytes in byte form" $ + forM_ + [ ("one byte", BtOne "21") + , ("three bytes", BtMany ["00", "01", "02"]) + ] + ( \(desc, bts) -> + it desc $ do + let expr = DataNumber bts + printed = printExpression' expr (SWEET, ASCII, SINGLELINE, defaultMargin) + printed `shouldContain` "number" + printed `shouldContain` "bytes" + parseExpression printed `shouldBe` Right expr + ) + describe "printExpression keeps a compressed meet atomic under a narrow margin" $ -- A \phinoMeet is a single \overbracket visual unit, so its body must stay -- on one line even when the surrounding margin forces the outer formation to diff --git a/test/XMIRSpec.hs b/test/XMIRSpec.hs --- a/test/XMIRSpec.hs +++ b/test/XMIRSpec.hs @@ -219,7 +219,6 @@ , "Q" , "$" , "[[ x -> T ]]" - , "[[ top -> [[ x -> T ]] ]]" , "[[ x -> [[ !t1 -> 5 ]] ]]" , "[[ org -> [[ z -> ?, L> Package ]] ]]" ] @@ -271,7 +270,7 @@ , ( "explains an unsupported nested expression" , do - expr <- parseExpressionThrows "[[ x -> [[ y -> T ]] ]]" + expr <- parseExpressionThrows "[[ x -> [[ y -> !e1 ]] ]]" try (void (expressionToXMIR expr defaultXmirContext)) :: IO (Either SomeException ()) , ["XMIR does not support such expression"] )