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.89 +version: 0.0.90 license: MIT synopsis: Command-Line Manipulator of πœ‘-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/dataization.yaml b/resources/dataization.yaml --- a/resources/dataization.yaml +++ b/resources/dataization.yaml @@ -56,7 +56,9 @@ d-result: Ξ΄ premises: - n-result: 𝑛 - evaluate: ⟦𝐡1, Ξ» ‍ 𝑓, 𝐡2⟧ + evaluate: + - ⟦𝐡1, Ξ» ‍ 𝑓, 𝐡2⟧ + - 𝑒 - n-result: 𝑛1 normalize: 𝑛 - d-result: Ξ΄ diff --git a/resources/morphing.yaml b/resources/morphing.yaml --- a/resources/morphing.yaml +++ b/resources/morphing.yaml @@ -40,7 +40,9 @@ n-result: 𝑛2 premises: - n-result: 𝑛 - evaluate: '⟦𝐡1, Ξ» ‍ 𝑓, 𝐡2⟧' + evaluate: + - '⟦𝐡1, Ξ» ‍ 𝑓, 𝐡2⟧' + - 𝑒 - n-result: 𝑛1 normalize: '𝑛.𝜏' - n-result: 𝑛2 diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -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 diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -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 diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -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 diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -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 diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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}" ] ] diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -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 =