packages feed

phino 0.0.89 → 0.0.90

raw patch · 9 files changed

+167/−86 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Yaml: OpEvaluate :: Expression -> Operation
+ Yaml: OpEvaluate :: Expression -> Expression -> Operation

Files

phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.89+version: 0.0.90 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
resources/dataization.yaml view
@@ -56,7 +56,9 @@   d-result: δ   premises:     - n-result: 𝑛-      evaluate: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧+      evaluate:+        - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧+        - 𝑒     - n-result: 𝑛1       normalize: 𝑛     - d-result: δ
resources/morphing.yaml view
@@ -40,7 +40,9 @@   n-result: 𝑛2   premises:     - n-result: 𝑛-      evaluate: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'+      evaluate:+        - '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'+        - 𝑒     - n-result: 𝑛1       normalize: '𝑛.𝜏'     - n-result: 𝑛2
src/Dataize.hs view
@@ -82,18 +82,24 @@ -- expression — and the mutable state 's', returning the morphed term together -- with the new state. The universe is matched against the rule's 'e-match' -- pattern (usually the '𝑒' meta, which binds 'e' so the 'root' rule substitutes--- it, but a rule may pin it to a literal such as 'mg' matching Φ). It is--- driven by--- the ordered rules from 'morphing.yaml': the first matching rule's premises are--- evaluated and its conclusion 'nresult' is built, always forwarding the same--- universe. The 'morph' premise that produces the conclusion is the spine: when+-- it, but a rule may pin it to a literal such as 'mg' matching Φ). Its rules+-- come from 'morphing.yaml': the first matching rule's premises are evaluated and+-- its conclusion 'nresult' is built, always forwarding the same universe. The+-- clauses are disjoint (see #856, #860), so their declaration order must not be+-- load-bearing; when '_shuffle' is on (the '--shuffle' flag) the rules are+-- shuffled before the 'firstMatch' walk to exercise that invariant — mirroring+-- normalization's "apply until they stop matching". A genuinely order-independent+-- step stays deterministic; a hidden overlap surfaces as a nondeterministic+-- failure rather than staying silently green.+-- The 'morph' premise that produces the conclusion is the spine: when -- its argument comes from a 'normalize' premise, the rewriter runs over that -- argument and its individual steps (alpha, copy, dot, …) are spliced into the -- chain before morphing continues. Every other premise is a side-computation -- evaluated in isolation by 'sidePremise', its own steps discarded. morph :: Morphed -> Expression -> State -> DataizeContext -> IO (Morphed, State) morph (expr, seq) univ state ctx = do-  matched <- firstMatch Y.morphingRules+  rules <- if ctx._shuffle then shuffle Y.morphingRules else pure Y.morphingRules+  matched <- firstMatch rules   case matched of     Just (rule, subst) -> reduce rule subst     Nothing -> throwIO (userError "no morphing rule matched")@@ -259,7 +265,7 @@     -- and the incoming state is returned unchanged.     runOperation :: IO (Term, State)     runOperation = case premise.operation of-      Y.OpEvaluate expr -> _evaluate univ ctx state [ArgExpression expr] subst+      Y.OpEvaluate expr universe -> _evaluate ctx state [ArgExpression expr, ArgExpression universe] subst       Y.OpMorph expr -> _morph univ ctx state [ArgExpression expr] subst       operation -> do         term <- execBuildTerm univ ctx (verb operation) (verbArgs operation) subst@@ -274,7 +280,7 @@ verb :: Y.Operation -> String verb (Y.OpMorph _) = "morph" verb (Y.OpNormalize _) = "normalize"-verb (Y.OpEvaluate _) = "evaluate"+verb (Y.OpEvaluate _ _) = "evaluate" verb (Y.OpContextualize _ _) = "contextualize" verb (Y.OpDataize _) = "dataize" @@ -282,7 +288,7 @@ verbArgs :: Y.Operation -> [ExtraArgument] verbArgs (Y.OpMorph expr) = [ArgExpression expr] verbArgs (Y.OpNormalize expr) = [ArgExpression expr]-verbArgs (Y.OpEvaluate expr) = [ArgExpression expr]+verbArgs (Y.OpEvaluate expr universe) = [ArgExpression expr, ArgExpression universe] verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context] verbArgs (Y.OpDataize expr) = [ArgExpression expr] @@ -361,21 +367,26 @@  -- Augment the injected, context-free term builder with the dataization and -- morphing operations that need the universe: 'evaluate' applies an atom and--- 'morph' morphs a sub-expression. Both receive the universe 'univ'. Every other--- function is delegated unchanged. This is the matcher's condition path (guards--- in 'when'/'having'), which has no state to thread, so 𝔼 ('evaluate') and 𝕄--- ('morph') run here on a fresh, empty state whose result is discarded; the+-- 'morph' morphs a sub-expression. 𝔼 ('evaluate') takes the universe as an+-- explicit second expression argument, while 𝕄 ('morph') is handed the threaded+-- 'univ'. Every other function is delegated unchanged. This is the matcher's+-- condition path (guards in 'when'/'having'), which has no state to thread, so 𝔼+-- and 𝕄 run here on a fresh, empty state whose result is discarded; the -- state-threading callers in 'sidePremise' use '_evaluate' and '_morph' directly. execBuildTerm :: Expression -> DataizeContext -> BuildTermFunc-execBuildTerm univ ctx "evaluate" = \args subst -> fst <$> _evaluate univ ctx emptyState args subst+execBuildTerm _ ctx "evaluate" = \args subst -> fst <$> _evaluate ctx emptyState args subst execBuildTerm univ ctx "morph" = \args subst -> fst <$> _morph univ ctx emptyState args subst execBuildTerm _ ctx func = _buildTerm ctx func --- The Evaluation function 𝔼(b, s): it fires the λ atom of a formation 'b' under--- the incoming state 𝑠 and returns the atom's result together with the new state.-_evaluate :: Expression -> DataizeContext -> State -> BuildTermMethodS-_evaluate univ ctx state [ArgExpression expr] subst = do+-- The Evaluation function 𝔼(b, e, s): it fires the λ atom of a formation 'b'+-- against the global universe 'e', under the incoming state 𝑠, and returns the+-- atom's result together with the new state. The universe is now passed+-- explicitly as the second argument (rather than threaded behind the scenes),+-- matching how the morphing 𝕄 and dataization 𝔻 functions carry it.+_evaluate :: DataizeContext -> State -> BuildTermMethodS+_evaluate ctx state [ArgExpression expr, ArgExpression universe] subst = do   form <- buildExpressionThrows expr subst+  univ <- buildExpressionThrows universe subst   case form of     ExFormation bds -> do       resolved <- formation bds univ state ctx@@ -383,7 +394,7 @@         Just (obj, state') -> pure (TeExpression obj, state')         Nothing -> throwIO (userError "Function evaluate() expects a formation with a λ binding")     _ -> throwIO (userError "Function evaluate() expects a formation")-_evaluate _ _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 1 expression argument")+_evaluate _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 2 expression arguments")  -- The Morphing function 𝕄 exposed as a build-term function so a rule can morph -- a sub-expression in its 'where' (the 'md' and 'ma' rules morph
src/LaTeX.hs view
@@ -372,7 +372,8 @@     joinedConditions (Just first) (Just second) = Just (Y.And [first, second])  -- Render a morphing rule as a LaTeX inference rule: each premise becomes a--- judgment above the line and the conclusion is 𝕄(match, e) ⟿ n-result below.+-- judgment above the line and the conclusion is 𝕄(match, e, s_1) ⟿ ⟨n-result, s_k⟩+-- below, where s_k is the final state threaded through the premises. explainMorphRule :: Y.MorphRule -> String explainMorphRule rule =   inference@@ -380,11 +381,14 @@     rule.name     rule.label     rule.when-    (map premiseToLatex rule.premises)-    (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (renderExpr rule.nresult))+    premises+    (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (stateName 1) (stateName final) (renderExpr rule.nresult))+  where+    (premises, final) = premisesToLatex rule.premises --- Render a dataization rule as a LaTeX inference rule, with 𝔻(match, e) ⟿--- d-result as the conclusion below the line.+-- Render a dataization rule as a LaTeX inference rule, with 𝔻(match, e, s_1) ⟿+-- ⟨d-result, s_k⟩ as the conclusion below the line, s_k being the final threaded+-- state. explainDataizeRule :: Y.DataizeRule -> String explainDataizeRule rule =   inference@@ -392,11 +396,14 @@     rule.name     rule.label     rule.when-    (map premiseToLatex rule.premises)-    (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (renderBytes rule.dresult))+    premises+    (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (stateName 1) (stateName final) (renderBytes rule.dresult))+  where+    (premises, final) = premisesToLatex rule.premises  -- Render a contextualization rule as a LaTeX inference rule, with 𝒞(match, c) ⟿--- c-result as the conclusion below the line.+-- c-result as the conclusion below the line. 𝒞 carries no state, so its premises+-- (all contextualizations) leave the state index untouched. explainContextualizeRule :: Y.ContextualizeRule -> String explainContextualizeRule rule =   inference@@ -404,20 +411,40 @@     rule.name     rule.label     Nothing-    (map premiseToLatex rule.premises)+    (fst (premisesToLatex rule.premises))     (phinoContextualize (renderExpr rule.match) (renderExpr rule.cmatch) (renderExpr rule.cresult)) --- One premise judgment, rendered per its operation. 𝕄 ('morph') and 𝔻--- ('dataize') are binary and carry the universe 'e' they were given; the rest--- are unary.-premiseToLatex :: Y.Premise -> String-premiseToLatex premise = case premise.operation of-  Y.OpMorph arg -> phinoMorph (renderExpr arg) "e" (renderExpr (ExMeta premise.result))-  Y.OpDataize arg -> phinoDataize (renderExpr arg) "e" (renderBytes (BtMeta premise.result))-  Y.OpNormalize arg -> phinoNormalize (renderExpr arg) (renderExpr (ExMeta premise.result))-  Y.OpEvaluate arg -> phinoEvaluate (renderExpr arg) (renderExpr (ExMeta premise.result))-  Y.OpContextualize arg context -> phinoContextualize (renderExpr arg) (renderExpr context) (renderExpr (ExMeta premise.result))+-- The state metavariable for index 'n', rendered as s_1, s_2, … to mirror the+-- n/n_1 convention used for terms.+stateName :: Int -> String+stateName n = "s_" ++ show n +-- Render a rule's premises in order, threading the state through them. The rule+-- starts in state s_1; each state-changing premise (𝕄, 𝔻, 𝔼) consumes the+-- current state and yields the next (s_2, s_3, …), matching how the engine folds+-- the state through the premises ('sidePremise' in 'Dataize.hs'). Returns the+-- rendered judgments and the final state index, which the conclusion returns.+premisesToLatex :: [Y.Premise] -> ([String], Int)+premisesToLatex = go 1+  where+    go index [] = ([], index)+    go index (premise : rest) = (rendered : more, final)+      where+        (rendered, next) = premiseToLatex index premise+        (more, final) = go next rest++-- One premise judgment in state s_index, rendered per its operation. The+-- state-changing operations 𝕄 ('morph'), 𝔻 ('dataize') and 𝔼 ('evaluate') carry+-- the universe 'e' they were given, consume s_index and yield s_index+1 (so they+-- return the bumped index); the rest are stateless and leave the index as is.+premiseToLatex :: Int -> Y.Premise -> (String, Int)+premiseToLatex index premise = case premise.operation of+  Y.OpMorph arg -> (phinoMorph (renderExpr arg) "e" (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)+  Y.OpDataize arg -> (phinoDataize (renderExpr arg) "e" (stateName index) (stateName (index + 1)) (renderBytes (BtMeta premise.result)), index + 1)+  Y.OpNormalize arg -> (phinoNormalize (renderExpr arg) (renderExpr (ExMeta premise.result)), index)+  Y.OpEvaluate arg universe -> (phinoEvaluate (renderExpr arg) (renderExpr universe) (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)+  Y.OpContextualize arg context -> (phinoContextualize (renderExpr arg) (renderExpr context) (renderExpr (ExMeta premise.result)), index)+ -- Assemble an inference block from a name, optional label, optional side -- condition, the premise judgments and the conclusion judgment. inference :: String -> String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String@@ -455,20 +482,27 @@   where     labelArg = maybe "" (\symbol -> "[" ++ symbol ++ "]") label --- 𝕄 and 𝔻 are binary, 𝕄(input, e) ⟿ output, so they render with the universe--- as the middle argument: \phinoMorph{ input }{ e }{ output }. 𝒩, 𝔼 and 𝒞 carry--- no universe.-phinoMorph :: String -> String -> String -> String-phinoMorph input univ output = printf "\\phinoMorph{ %s }{ %s }{ %s }" input univ output+-- 𝕄, 𝔻 and 𝔼 carry the universe and thread the state from 'sIn' to a new+-- 'sOut', 𝕄(input, e, sIn) ⟿ ⟨output, sOut⟩, so they render with the universe+-- and incoming state as the middle arguments and a paired conclusion:+-- \phinoMorph{ input }{ e }{ sIn }{ ⟨output, sOut⟩ }. 𝒩 and 𝒞 carry neither+-- universe nor state.+phinoMorph :: String -> String -> String -> String -> String -> String+phinoMorph input univ sIn sOut output = printf "\\phinoMorph{ %s }{ %s }{ %s }{ %s }" input univ sIn (paired output sOut) -phinoDataize :: String -> String -> String -> String-phinoDataize input univ output = printf "\\phinoDataize{ %s }{ %s }{ %s }" input univ output+phinoDataize :: String -> String -> String -> String -> String -> String+phinoDataize input univ sIn sOut output = printf "\\phinoDataize{ %s }{ %s }{ %s }{ %s }" input univ sIn (paired output sOut)  phinoNormalize :: String -> String -> String phinoNormalize input = printf "\\phinoNormalize{ %s }{ %s }" input -phinoEvaluate :: String -> String -> String-phinoEvaluate input = printf "\\phinoEvaluate{ %s }{ %s }" input+phinoEvaluate :: String -> String -> String -> String -> String -> String+phinoEvaluate input univ sIn sOut output = printf "\\phinoEvaluate{ %s }{ %s }{ %s }{ %s }" input univ sIn (paired output sOut)++-- The state-passing functions 𝕄, 𝔻 and 𝔼 return a pair ⟨output, state⟩, the+-- new value alongside the threaded state.+paired :: String -> String -> String+paired output state = printf "\\langle %s, %s \\rangle" output state  phinoContextualize :: String -> String -> String -> String phinoContextualize input context = printf "\\phinoContextualize{ %s }{ %s }{ %s }" input context
src/Render.hs view
@@ -285,10 +285,11 @@  instance Render EXTRA where   render EXTRA{func = "contextualize", args = arg : rest, ..} = render meta <> " \\coloneqq \\ctx{ " <> render arg <> " }{ " <> T.intercalate ", " (map render rest) <> " }"-  -- 𝕄 is binary, 𝕄(n, e), so a 'morph' extra renders with the universe-  -- metavariable 'e' as its second argument, matching how the morphing rules-  -- forward the universe unchanged.-  render EXTRA{func = "morph", ..} = render meta <> " \\coloneqq \\phinoMorph{ " <> T.intercalate ", " (map render args) <> " }{ e }"+  -- 𝕄 carries the universe and threads a state, 𝕄(n, e, s_1), so a 'morph' extra+  -- renders with the universe metavariable 'e' and the incoming state 's_1' as its+  -- trailing arguments. This is a one-off application binding only 'meta', so the+  -- returned state is dropped (the engine discards it too, see 'execBuildTerm').+  render EXTRA{func = "morph", ..} = render meta <> " \\coloneqq \\phinoMorph{ " <> T.intercalate ", " (map render args) <> " }{ e }{ s_1 }"   render EXTRA{..} = render meta <> " \\coloneqq " <> macro func <> "{ " <> T.intercalate ", " (map render args) <> " }"     where       macro :: String -> Text
src/Yaml.hs view
@@ -238,7 +238,7 @@ data Operation   = OpMorph Expression   | OpNormalize Expression-  | OpEvaluate Expression+  | OpEvaluate Expression Expression   | OpContextualize Expression Expression   | OpDataize Expression   deriving (Eq, Generic, Show)@@ -313,7 +313,11 @@   asum     [ OpMorph <$> o .: "morph"     , OpNormalize <$> o .: "normalize"-    , OpEvaluate <$> o .: "evaluate"+    , do+        vals <- o .: "evaluate"+        case vals of+          [expr, universe] -> OpEvaluate <$> parseJSON expr <*> parseJSON universe+          _ -> fail "'evaluate' expects exactly two arguments"     , do         vals <- o .: "contextualize"         case vals of
test/CLISpec.hs view
@@ -1047,56 +1047,56 @@         [ unlines             [ "\\begin{phinoMorphingInference}"             , "  \\phinoName{mf}"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ [[ B ]] } }"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ s_1 }{ \\langle [[ B ]], s_1 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{ml}"             , "  \\phinoLabel{\\lambda}"-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }"+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\langle n, s_2 \\rangle } }"             , "  \\phinoPremise{ \\phinoNormalize{ n . \\tau }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ n_2 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ n_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_2 }{ \\langle n_2, s_3 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ \\langle n_2, s_3 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{md}"             , "  \\phinoCondition{ \\phinoNotFormation{ n } }"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }"             , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ n_3 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ \\langle n_3, s_3 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ s_1 }{ \\langle n_3, s_3 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{ma}"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }"             , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> e_1 ) }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> e_1 ) }{ e }{ n_3 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ \\langle n_3, s_3 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> e_1 ) }{ e }{ s_1 }{ \\langle n_3, s_3 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{maa}"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }"             , "  \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ n_2 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ n_3 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ \\langle n_3, s_3 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ s_1 }{ \\langle n_3, s_3 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{root}"             , "  \\phinoCondition{ e \\not= Q }"             , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{dead}"-            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e }{ T } }"+            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e }{ s_1 }{ \\langle T, s_1 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{xi}"-            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ T } }"+            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ s_1 }{ \\langle T, s_1 \\rangle } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{mg}"-            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ T } }"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ \\langle T, s_1 \\rangle } }"             , "\\end{phinoMorphingInference}"             ]         ]@@ -1108,38 +1108,38 @@             [ "\\begin{phinoDataizationInference}"             , "  \\phinoName{delta}"             , "  \\phinoLabel{\\Delta}"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ \\delta } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ s_1 }{ \\langle \\delta, s_1 \\rangle } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{box}"             , "  \\phinoCondition{ [ D, L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }"             , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ n } }"             , "  \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ \\delta } }"+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_1 }{ \\langle \\delta, s_2 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ s_1 }{ \\langle \\delta, s_2 \\rangle } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{fire}"-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }"+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\langle n, s_2 \\rangle } }"             , "  \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ \\delta } }"+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\langle \\delta, s_3 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\langle \\delta, s_3 \\rangle } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{none}"             , "  \\phinoCondition{ [ D, L, @ ] \\cap \\lparen B \\rparen = \\emptyset }"-            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ -- } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\langle --, s_1 \\rangle } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{end}"-            , "  \\phinoConclusion{ \\phinoDataize{ T }{ e }{ -- } }"+            , "  \\phinoConclusion{ \\phinoDataize{ T }{ e }{ s_1 }{ \\langle --, s_1 \\rangle } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{norm}"             , "  \\phinoCondition{ \\phinoNotFormation{ n } \\;\\text{and}\\; n \\not= T }"-            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"-            , "  \\phinoConclusion{ \\phinoDataize{ n }{ e }{ \\delta } }"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ \\langle n_1, s_2 \\rangle } }"+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\langle \\delta, s_3 \\rangle } }"+            , "  \\phinoConclusion{ \\phinoDataize{ n }{ e }{ s_1 }{ \\langle \\delta, s_3 \\rangle } }"             , "\\end{phinoDataizationInference}"             ]         ]
test/DataizeSpec.hs view
@@ -70,6 +70,33 @@         )       ] +  -- 'defaultDataizeContext' runs with '_shuffle' on, so 'morph' walks the+  -- morphing rules in a random order on every step. Every clause is+  -- order-independent (the known overlaps were removed in #856 and #860), so the+  -- outcome must never depend on that order: morphing each input many times under+  -- a shuffling context yields exactly the formation the fixed declaration order+  -- does, proving the rules may be applied in any order with the same result.+  -- Were a hidden overlap re-introduced, some of these random orders would+  -- disagree and 'nub' would collect more than the single expected form.+  describe "morphing is order-independent under --shuffle" $ do+    let cases =+          [ ("a byte formation", ExFormation [BiDelta (BtOne "00")], ExRoot, ExFormation [BiDelta (BtOne "00")])+          , ("termination", ExTermination, ExRoot, ExTermination)+          , ("xi", ExXi, ExRoot, ExTermination)+          , ("the global object", ExRoot, ExRoot, ExTermination)+          ,+            ( "a dispatch over a formation"+            , ExDispatch ExRoot (AtLabel "x")+            , ExFormation [BiTau (AtLabel "x") (ExFormation [])]+            , ExFormation [BiTau AtRho (ExFormation [BiTau (AtLabel "x") (ExFormation [BiVoid AtRho]), BiVoid AtRho])]+            )+          ]+    forM_ cases $ \(desc, input, univ, expected) ->+      it ("morphs " ++ desc ++ " to the same form across 100 random rule orders") $ do+        let prog = Program univ+        results <- replicateM 100 (fst . fst <$> morph (input, (prog, Nothing) :| []) univ emptyState (defaultDataizeContext ExRoot))+        nub results `shouldBe` [expected]+   -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'),   -- so a formation head — λ-bearing or not — is left to 'ml'/'mf'. The   -- two clauses are mutually exclusive and their order in 'morphing.yaml'@@ -163,7 +190,7 @@     let verb op = case op of           Yaml.OpMorph _ -> "morph"           Yaml.OpNormalize _ -> "normalize"-          Yaml.OpEvaluate _ -> "evaluate"+          Yaml.OpEvaluate _ _ -> "evaluate"           Yaml.OpContextualize _ _ -> "contextualize"           Yaml.OpDataize _ -> "dataize"         allowed =