phino 0.0.85 → 0.0.86

raw patch · 20 files changed

+743/−474 lines, 20 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +9/−5
• phino.cabal +1/−1
• resources/dataization.yaml +52/−31
• resources/morphing.yaml +85/−57
• src/CLI/Runners.hs +4/−4
• src/CST.hs +2/−0
• src/Condition.hs +5/−0
• src/Dataize.hs +234/−151
• src/Encoding.hs +1/−0
• src/Functions.hs +1/−1
• src/LaTeX.hs +70/−36
• src/Lining.hs +1/−0
• src/Render.hs +7/−3
• src/Rule.hs +25/−6
• src/Sugar.hs +1/−0
• src/Yaml.hs +71/−71
• test/CLISpec.hs +103/−78
• test/ConditionSpec.hs +2/−0
• test/DataizeSpec.hs +56/−28
• test/LaTeXSpec.hs +13/−2

@@ -238,16 +238,16 @@ $ phino explain --morph \begin{tabular}{rl} \phinoMorphingRule{prim}-  { \mathbb{M}( [[ B ]] ) }+  { \mathbb{M}( [[ B ]], e ) }   { [[ B ]] }   { }   { } ... \phinoMorphingRule{root}-  { \mathbb{M}( Q ) }-  { \mathbb{M}( \phinoNormalize{ e } ) }+  { \mathbb{M}( Q, e ) }+  { \mathbb{M}( \phinoNormalize{ e }, e ) }   { $ e \not= Q $ }-  { $ e \coloneqq \phinoGlobal{  } $ }+  { } \end{tabular} ``` @@ -262,7 +262,7 @@ ... \phinoDataizationRule{norm}   { \phinoDataize{ n } }-  { \phinoDataize{ \mathbb{M}( n ) } }+  { \phinoDataize{ \mathbb{M}( n, e ) } }   { }   { } \end{tabular}@@ -310,6 +310,10 @@   | part-of:             # returns True if given expression is attached to any       - Expression'      # attribute in ginve bindings       - BiMeta'+  | formation:           # returns True if given expression is a formation+      Expression'        # (an abstraction ⟦…⟧); used by morphing 'dispatch'+                         # as 'not (formation 𝑛)', so a non-formation head is+                         # morphed and a formation head is left to 'lambda'  Comparable:              # comparable object that may be used in 'eq' condition   = Attribute'

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

@@ -1,57 +1,78 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. The input-# is always a normal form: a non-NF expression matches no clause.+# Dataization 𝔻 — applied top-to-bottom, first matching clause wins. It is+# binary, 𝔻(n, e): the second argument e is the global universe, the same+# expression that 𝕄 takes as its second argument; 𝔻 forwards it to 𝕄. The first+# argument is always a normal form: a non-NF expression matches no clause.+#+# Each rule is an inference rule: when 'match' matches the term and 'e-match'+# matches the universe (binding the meta e), the rule yields the conclusion+# 'd-result' (a premise bytes meta or a literal), provided 'when' holds and the+# ordered 'premises' reduce as stated. A premise binds its 'n-result'/'d-result'+# to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('lambda')+# or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of+# 𝔻(n, e); it is always the e meta. The single bytes result is named δ; derived+# terms are 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match'+# already binds it.  - name: delta   label: \Delta-  description: '𝔻(⟦𝐵1, Δ ⤍ δ, 𝐵2⟧) ⟿ δ'   match: ⟦𝐵1, Δ ⤍ δ, 𝐵2⟧-  then: δ+  e-match: 𝑒+  d-result: δ  - name: box-  description: '𝔻(⟦𝐵1, φ ↦ e, 𝐵2⟧) ⟿ 𝔻(𝒩(𝒞(e))) if [Δ, λ] ∩ (𝐵1 ∪ 𝐵2) = ∅'-  match: ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧-  where:-    - meta: 𝑒1-      function: contextualize-      args:-        - 𝑒-        - ⟦𝐵1, φ ↦ 𝑒, 𝐵2⟧+  label: box+  match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧+  e-match: 𝑒+  d-result: δ   when:     disjoint:       - [Δ, λ]       - [𝐵1, 𝐵2]-  then:-    dataize:-      normalize: 𝑒1+  premises:+    - n-result: 𝑛+      contextualize:+        - 𝑒1+        - ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧+    - n-result: 𝑛1+      normalize: 𝑛+    - d-result: δ+      dataize: 𝑛1  - name: fire-  description: '𝔻(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧) ⟿ 𝔻(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧)))'+  label: fire   match: ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧-  where:-    - meta: 𝑒-      function: lambda-      args:-        - ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧-  then:-    dataize:-      normalize: 𝑒+  e-match: 𝑒+  d-result: δ+  premises:+    - n-result: 𝑛+      lambda: ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧+    - n-result: 𝑛1+      normalize: 𝑛+    - d-result: δ+      dataize: 𝑛1  - name: none-  description: '𝔻(⟦𝐵⟧) ⟿ nothing'+  label: none   match: ⟦𝐵⟧-  then: nothing+  e-match: 𝑒+  d-result: '--'  - name: bott-  description: '𝔻(⊥) ⟿ nothing'+  label: bott   match: ⊥-  then: nothing+  e-match: 𝑒+  d-result: '--'  - name: norm-  description: '𝔻(n) ⟿ 𝔻(𝕄(n)) otherwise'+  label: norm   match: 𝑛-  then:-    dataize:+  e-match: 𝑒+  d-result: δ+  premises:+    - n-result: 𝑛1       morph: 𝑛+    - d-result: δ+      dataize: 𝑛1

@@ -1,93 +1,121 @@ # SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com # SPDX-License-Identifier: MIT ----# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. The input is+# Morphing 𝕄 — applied top-to-bottom, first matching clause wins. It is binary,+# 𝕄(n, e): n is the term being morphed and e is the fixed global universe,+# threaded unchanged through every recursive call and substituted for Φ by the+# 'root' rule (Φ, rendered Q, is just the locator of e). The first argument is # always a normal form: a non-NF expression matches no clause. 𝕄 navigates a-# normal form down to a formation one operation at a time,-# resolving the universe Φ and peeling dispatches and applications through-# normalization 𝒩. It never fires a bare atom: a saturated λ-formation is-# returned untouched and fired later by 𝔼 (the 'fire' rule of 𝔻).+# normal form to a formation one operation at a time, resolving Φ against e and+# peeling dispatches and applications through normalization 𝒩. It never fires a+# bare atom: a saturated λ-formation is returned untouched and fired later by 𝔼+# (the 'fire' rule of 𝔻).+#+# Each rule is an inference rule: when 'match' matches the term and 'e-match'+# matches the universe (binding the meta e), the rule yields the conclusion+# 'n-result' (a premise meta or a literal), provided 'when' holds and the+# ordered 'premises' reduce as stated. A premise binds 'n-result' to the result+# of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('lambda'). 'e-match' is+# the universe-argument matcher of 𝕄(n, e); it is always the e meta. Derived+# terms are named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is skipped only when+# 'match' already binds it.+#+# 'lambda' and 'dispatch' are kept mutually exclusive: 'dispatch' fires only+# when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation+# head — λ-bearing or not — is left to 'lambda' (and 'prim'). The two clauses+# are disjoint and their relative order does not change behavior.  - name: prim-  description: '𝕄(⟦𝐵⟧) ⟿ ⟦𝐵⟧'+  label: prim   match: ⟦𝐵⟧-  then: ⟦𝐵⟧+  e-match: 𝑒+  n-result: ⟦𝐵⟧  - name: lambda   label: \lambda-  description: '𝕄(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.τ) ⟿ 𝕄(𝒩(𝔼(⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧).τ))'   match: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.𝜏'-  where:-    - meta: 𝑒-      function: lambda-      args:-        - '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧'-  then:-    morph:-      normalize: '𝑒.𝜏'+  e-match: 𝑒+  n-result: 𝑛2+  premises:+    - n-result: 𝑛+      lambda: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧'+    - n-result: 𝑛1+      normalize: '𝑛.𝜏'+    - n-result: 𝑛2+      morph: 𝑛1  - name: dispatch-  description: '𝕄(n.τ) ⟿ 𝕄(𝒩(𝕄(n).τ))'+  label: disp   match: '𝑛.𝜏'-  where:-    - meta: 𝑒-      function: morph-      args:-        - 𝑛-  then:-    morph:-      normalize: '𝑒.𝜏'+  e-match: 𝑒+  n-result: 𝑛3+  when:+    not:+      formation: 𝑛+  premises:+    - n-result: 𝑛1+      morph: 𝑛+    - n-result: 𝑛2+      normalize: '𝑛1.𝜏'+    - n-result: 𝑛3+      morph: 𝑛2  - name: application-  description: '𝕄(n(τ ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(τ ↦ e)))'-  match: '𝑛(𝜏 ↦ 𝑒)'-  where:-    - meta: 𝑒1-      function: morph-      args:-        - 𝑛-  then:-    morph:-      normalize: '𝑒1(𝜏 ↦ 𝑒)'+  label: app+  match: '𝑛(𝜏 ↦ 𝑒1)'+  e-match: 𝑒+  n-result: 𝑛3+  premises:+    - n-result: 𝑛1+      morph: 𝑛+    - n-result: 𝑛2+      normalize: '𝑛1(𝜏 ↦ 𝑒1)'+    - n-result: 𝑛3+      morph: 𝑛2  - name: applicationa-  description: '𝕄(n(α_i ↦ e)) ⟿ 𝕄(𝒩(𝕄(n)(α_i ↦ e)))'-  match: '𝑛(α𝑖 ↦ 𝑒)'-  where:-    - meta: 𝑒1-      function: morph-      args:-        - 𝑛-  then:-    morph:-      normalize: '𝑒1(α𝑖 ↦ 𝑒)'+  label: appa+  match: '𝑛(α𝑖 ↦ 𝑒1)'+  e-match: 𝑒+  n-result: 𝑛3+  premises:+    - n-result: 𝑛1+      morph: 𝑛+    - n-result: 𝑛2+      normalize: '𝑛1(α𝑖 ↦ 𝑒1)'+    - n-result: 𝑛3+      morph: 𝑛2  - name: root-  description: '𝕄(Φ) ⟿ 𝕄(𝒩(e)) where e := global(), unless e is Φ'+  label: root   match: Φ-  where:-    - meta: 𝑒-      function: global+  e-match: 𝑒+  n-result: 𝑛1   when:     not:       eq:         - 𝑒         - Φ-  then:-    morph:+  premises:+    - n-result: 𝑛       normalize: 𝑒+    - n-result: 𝑛1+      morph: 𝑛  - name: dead-  description: '𝕄(⊥) ⟿ ⊥'+  label: dead   match: ⊥-  then: ⊥+  e-match: 𝑒+  n-result: ⊥  - name: xi-  description: '𝕄(ξ) ⟿ ⊥'+  label: xi   match: ξ-  then: ⊥+  e-match: 𝑒+  n-result: ⊥  - name: globe-  description: '𝕄(Φ) ⟿ ⊥ when the universe is Φ itself'+  label: globe   match: Φ-  then: ⊥+  e-match: 𝑒+  n-result: ⊥

@@ -147,9 +147,9 @@       canonize = if _canonize then C.canonize else id       exclude = (`F.exclude` excluded)       include = (`F.include` included)-  (maybeBytes, chain) <- dataize (context loc prog printCtx)+  (bytes, chain) <- dataize prog (context loc printCtx)   when _sequence (printRewrittens printCtx (canonize $ exclude $ include chain, False) >>= putStrLn)-  unless _quiet (putStrLn (maybe (P.printExpression ExTermination) P.printBytes maybeBytes))+  unless _quiet (putStrLn (P.printBytes bytes))   where     validateOpts :: IO ()     validateOpts = do@@ -160,8 +160,8 @@         [(_meetPopularity, "meet-popularity"), (_meetLength, "meet-length")]       validateXmirOptions _outputFormat [(_omitListing, "omit-listing"), (_omitComments, "omit-comments")] _focus       when (length _show > 1) (invalidCLIArguments "The option --show can be used only once")-    context :: Expression -> Program -> PrintProgramContext -> DataizeContext-    context loc prog ctx = DataizeContext loc prog _maxDepth _maxCycles _depthSensitive buildTerm (saveStepFunc _stepsDir ctx)+    context :: Expression -> PrintProgramContext -> DataizeContext+    context loc ctx = DataizeContext loc _maxDepth _maxCycles _depthSensitive buildTerm (saveStepFunc _stepsDir ctx)     printProgCtx :: Expression -> PrintProgramContext     printProgCtx focus =       PrintProgCtx

@@ -234,6 +234,7 @@   | CO_MATCHES {regex :: String, expr :: EXPRESSION}   | CO_PART_OF {expr :: EXPRESSION, binding :: BINDING}   | CO_DISJOINT {attrs :: [ATTRIBUTE], groups :: [BINDING]}+  | CO_FORMATION {expr :: EXPRESSION}   deriving (Eq, Show)  data EXTRA_ARG@@ -540,6 +541,7 @@   toCST (Y.Gt left right) _ = CO_COMPARE (comparableToCST left) GREATER (comparableToCST right)   toCST (Y.Matches regex expr) _ = CO_MATCHES regex (expressionToCST expr)   toCST (Y.PartOf expr binding) _ = CO_PART_OF (expressionToCST expr) (bindingsToCST [binding])+  toCST (Y.IsFormation expr) _ = CO_FORMATION (expressionToCST expr)  instance ToCST Y.Comparable COMPARABLE where   toCST (Y.CmpAttr attr) _ = CMP_ATTR (attributeToCST attr)

@@ -142,6 +142,11 @@         bd <- _binding phiParser         _ <- rparen         return (Y.PartOf expr bd)+    , do+        _ <- symbol "formation" >> lparen+        expr <- _expression phiParser+        _ <- rparen+        return (Y.IsFormation expr)     ]  parseCondition :: String -> Either String Y.Condition

@@ -14,13 +14,14 @@ import AST import Builder (buildBytesThrows, buildExpressionThrows) import Control.Exception (throwIO)-import Data.List (partition)+import Control.Monad (foldM)+import Data.List (find, partition) import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Text as T-import Deps (BuildTermFunc, BuildTermMethod, SaveStepFunc, Term (TeAttribute, TeExpression))+import Deps (BuildTermFunc, BuildTermMethod, SaveStepFunc, Term (..)) import Locator (locatedExpression, withLocatedExpression)-import Matcher (Subst (..), substEmpty)+import Matcher (MetaValue (..), Subst (..), combine, matchExpression', substEmpty, substSingle) import Misc import Must (Must (..)) import Rewriter (RewriteContext (RewriteContext), Rewritten, rewrite)@@ -29,15 +30,19 @@ import Yaml (ExtraArgument (..), normalizationRules) import qualified Yaml as Y -type Dataized = (Maybe Bytes, [Rewritten])+type Dataized = (Bytes, [Rewritten])  type Dataizable = (Expression, NonEmpty Rewritten)  type Morphed = Dataizable +-- The evaluation context carries only configuration. Nothing global is fixed+-- here: the universe (the second argument 'e' of 𝕄(n, e) and 𝔻(n, e)) is a plain+-- expression threaded as an argument to 'dataize'', 'morph' and on to the atoms.+-- The working program needed for normalization is taken from the head of the+-- step chain, so no 'Program' is threaded around. data DataizeContext = DataizeContext   { _locator :: Expression-  , _program :: Program   , _maxDepth :: Int   , _maxCycles :: Int   , _depthSensitive :: Bool@@ -46,13 +51,13 @@   }  -- Resolve formation for LAMBDA Morphing rule.--- If formation contains λ binding, the called atom--- result is returned.-formation :: [Binding] -> DataizeContext -> IO (Maybe Expression)-formation bds ctx = do+-- If formation contains λ binding, the called atom result is returned. The+-- universe 'univ' is forwarded to the atom.+formation :: [Binding] -> Expression -> DataizeContext -> IO (Maybe Expression)+formation bds univ ctx = do   let (lambda, bds') = maybeLambda bds   case lambda of-    Just (BiLambda (Function func)) -> Just <$> atom func (ExFormation bds') ctx+    Just (BiLambda (Function func)) -> Just <$> atom func (ExFormation bds') univ ctx     _ -> pure Nothing   where     maybeLambda :: [Binding] -> (Maybe Binding, [Binding])@@ -65,119 +70,202 @@             [bd] -> (Just bd, rest)             _ -> (Nothing, bds) --- The Morphing function 𝕄 maps normal forms to formations. It is driven by the--- ordered rules from 'morphing.yaml': the first matching rule's 'then' outcome--- either stops at a formation ('MoStop') or keeps morphing ('MoMorph'). When--- the morphed argument is a normalization ('MaNormalize', as in the 'lambda' and--- 'root' rules), the rewriter runs over the rule's product and its individual--- steps are spliced into the chain before morphing continues.-morph :: Morphed -> DataizeContext -> IO Morphed-morph (expr, seq) ctx@DataizeContext{..} = do+-- The Morphing function 𝕄 maps normal forms to formations. It is binary,+-- 𝕄(n, e): besides the term 'n' it takes the universe 'e' ('univ') — a plain+-- expression — and matches it against the rule's 'e-match' pattern (always the+-- '𝑒' meta), which binds 'e' so the 'root' rule substitutes it. 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+-- 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 -> DataizeContext -> IO Morphed+morph (expr, seq) univ ctx = do   matched <- firstMatch Y.morphingRules   case matched of-    Just (rule, subst) -> apply rule.then_ rule.name subst+    Just (rule, subst) -> reduce rule subst     Nothing -> throwIO (userError "no morphing rule matched")   where     firstMatch :: [Y.MorphRule] -> IO (Maybe (Y.MorphRule, Subst))     firstMatch [] = pure Nothing     firstMatch (rule : rest) = do-      substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx))+      substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))       case substs of         (subst : _) -> pure (Just (rule, subst))         [] -> firstMatch rest-    -- The M/D rules evaluate as 'match → where → when', so the rule's guard-    -- maps onto the 'having' slot (which runs after 'where'), not 'when' (which-    -- 'matchExpressionWithRule'' runs before 'where').+    -- Match the conclusion term and check the guard; premises are no longer the+    -- matcher's business, so 'where'/'having' stay empty and the guard lives in+    -- 'when'. Every morphing guard reads only meta-variables bound by 'match'+    -- and 'e-match', so it holds before any premise runs.     asRule :: Y.MorphRule -> Y.Rule-    asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when-    apply :: Y.MorphOutcome -> String -> Subst -> IO Morphed-    apply (Y.MoStop result) name subst = do-      built <- buildExpressionThrows result subst-      seq' <- leadsTo seq name built ctx-      pure (built, seq')-    apply (Y.MoMorph (Y.MaExpr result)) name subst = do-      built <- buildExpressionThrows result subst-      seq' <- leadsTo seq name built ctx-      morph (built, seq') ctx-    -- 𝕄(𝒩(e)) records the producing step, then delegates to the normalization-    -- rewriter and splices its individual steps (alpha, copy, dot, …) into the-    -- chain before morphing on the resulting normal form. Termination is the-    -- rules' job: the 'root' rule's 'when' refuses to expand a universe that is-    -- Φ itself, so the 'globe' rule catches it and yields ⊥ instead of looping.-    apply (Y.MoMorph (Y.MaNormalize arg)) name subst = do-      built <- buildExpressionThrows arg subst-      labelled <- leadsTo seq name built ctx-      (expr', seq') <- normalized built labelled ctx-      morph (expr', seq') ctx+    asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing+    -- Evaluate the rule's premises and build its conclusion. A literal+    -- conclusion is terminal. Otherwise the conclusion meta is produced by a+    -- trailing 'morph' premise (the spine); if that premise's argument is itself+    -- bound by a 'normalize' premise, the normalization joins the spine and its+    -- steps splice in before morphing continues.+    reduce :: Y.MorphRule -> Subst -> IO Morphed+    reduce rule subst = case producer rule.nresult rule.premises of+      Nothing -> do+        final <- sides rule.premises subst+        built <- buildExpressionThrows rule.nresult final+        seq' <- leadsTo seq rule.name built ctx+        pure (built, seq')+      Just concl@(Y.Premise _ (Y.OpMorph arg)) -> case producer arg rule.premises of+        Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do+          final <- sides (rule.premises `excluding` [concl, normal]) subst+          built <- buildExpressionThrows inner final+          labelled <- leadsTo seq rule.name built ctx+          (normal', seq') <- normalized built labelled ctx+          morph (normal', seq') univ ctx+        _ -> do+          final <- sides (rule.premises `excluding` [concl]) subst+          built <- buildExpressionThrows arg final+          seq' <- leadsTo seq rule.name built ctx+          morph (built, seq') univ ctx+      Just _ -> throwIO (userError (printf "morphing rule '%s' must conclude with a 'morph' premise" rule.name))+    sides :: [Y.Premise] -> Subst -> IO Subst+    sides premises subst = foldM (sidePremise univ ctx) subst premises -dataize :: DataizeContext -> IO Dataized-dataize ctx@DataizeContext{..} = do-  expr <- locatedExpression _locator _program-  (maybeBytes, seq) <- dataize' (expr, (_program, Nothing) :| []) ctx-  pure (maybeBytes, reverse seq)+-- Dataize the program located at '_locator'. The program's root is the universe+-- (the 'e' argument) passed to 𝔻 and 𝕄.+dataize :: Program -> DataizeContext -> IO Dataized+dataize program@(Program univ) ctx@DataizeContext{..} = do+  expr <- locatedExpression _locator program+  (bytes, seq) <- dataize' (expr, (program, Nothing) :| []) univ ctx+  pure (bytes, reverse seq) --- The Dataization function 𝔻 retrieves bytes from an expression. It is driven--- by the ordered rules from 'dataization.yaml': 'delta' yields the asset bytes,--- 'none' (a formation) and 'bott' (⊥) yield nothing, 'box' contextualizes the--- φ-body and keeps dataizing (its step is labelled by the operation,--- 'contextualize'), and 'norm' reduces through morphing, splicing the morphing--- steps into the chain.-dataize' :: Dataizable -> DataizeContext -> IO Dataized-dataize' (expr, seq) ctx = do+-- The Dataization function 𝔻 retrieves bytes from an expression. It is total and+-- binary, 𝔻(n, e): besides the term 'n' it takes the universe 'e' ('univ'),+-- which it forwards to 𝕄. It is driven by the ordered rules from+-- 'dataization.yaml': 'delta' yields the asset bytes, 'none' (a formation) and+-- 'bott' (⊥) yield empty bytes (--), 'box' contextualizes the φ-body and keeps+-- dataizing (its step is labelled by its 'contextualize' side-computation), and+-- 'norm' reduces through morphing, splicing the morphing steps into the chain.+-- The conclusion bytes 'dresult' are produced by a trailing 'dataize' premise;+-- when its argument is bound by a 'morph' or 'normalize' premise, that step+-- joins the spine, otherwise the premise is an isolated side-computation.+dataize' :: Dataizable -> Expression -> DataizeContext -> IO Dataized+dataize' (expr, seq) univ ctx = do   matched <- firstMatch Y.dataizationRules   case matched of-    Just (rule, subst) -> apply rule subst+    Just (rule, subst) -> reduce rule subst     Nothing -> throwIO (userError "no dataization rule matched")   where     firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))     firstMatch [] = pure Nothing     firstMatch (rule : rest) = do-      substs <- matchExpressionWithRule' expr (asRule rule) (RuleContext (execBuildTerm ctx))+      substs <- matchExpressionWithRule' (matchExpression' rule.ematch univ) expr (asRule rule) (RuleContext (execBuildTerm univ ctx))       case substs of         (subst : _) -> pure (Just (rule, subst))         [] -> firstMatch rest     asRule :: Y.DataizeRule -> Y.Rule-    asRule rule = Y.Rule rule.name Nothing rule.description rule.match ExRoot Nothing rule.where_ rule.when-    apply :: Y.DataizeRule -> Subst -> IO Dataized-    apply rule subst = case rule.then_ of-      Y.DoData bytes -> do-        bts <- buildBytesThrows bytes subst-        pure (Just bts, NE.toList seq)-      Y.DoNothing -> pure (Nothing, NE.toList seq)-      Y.DoDataize (Y.DaExpr result) -> do-        built <- buildExpressionThrows result subst-        seq' <- leadsTo seq (operation rule) built ctx-        dataize' (built, seq') ctx-      -- 𝔻(𝕄(e)) delegates to the morphing relation, splicing its steps into-      -- the chain before dataizing on.-      Y.DoDataize (Y.DaMorph arg) -> do-        built <- buildExpressionThrows arg subst-        (morphed, seq') <- morph (built, seq) ctx-        dataize' (morphed, seq') ctx-      -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization), then-      -- normalizes its result back to a normal form before dataizing on, so 𝔻-      -- only ever sees normal forms.-      Y.DoDataize (Y.DaNormalize arg) -> do-        built <- buildExpressionThrows arg subst-        labelled <- leadsTo seq (operation rule) built ctx-        (normal, seq') <- normalized built labelled ctx-        dataize' (normal, seq') ctx-    operation :: Y.DataizeRule -> String-    operation rule = case rule.where_ of-      Just (extra : _) -> Y.function extra-      _ -> ""+    asRule rule = Y.Rule rule.name Nothing Nothing rule.match ExRoot rule.when Nothing Nothing+    reduce :: Y.DataizeRule -> Subst -> IO Dataized+    reduce rule subst = case bytesProducer rule.dresult rule.premises of+      Nothing -> do+        final <- sides rule.premises subst+        bts <- buildBytesThrows rule.dresult final+        pure (bts, NE.toList seq)+      Just concl@(Y.Premise _ (Y.OpDataize arg)) -> case producer arg rule.premises of+        -- 𝔻(𝒩(e)) records the producing step (the 'box' contextualization or the+        -- 'fire' λ-application), then normalizes its result back to a normal form+        -- before dataizing on, so 𝔻 only ever sees normal forms.+        Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do+          let side = rule.premises `excluding` [concl, normal]+          final <- sides side subst+          built <- buildExpressionThrows inner final+          labelled <- leadsTo seq (labelOf side) built ctx+          (normal', seq') <- normalized built labelled ctx+          dataize' (normal', seq') univ ctx+        -- 𝔻(𝕄(e)) delegates to the morphing relation, splicing its steps into the+        -- chain before dataizing on.+        Just morphed@(Y.Premise _ (Y.OpMorph inner)) -> do+          final <- sides (rule.premises `excluding` [concl, morphed]) subst+          built <- buildExpressionThrows inner final+          (morphed', seq') <- morph (built, seq) univ ctx+          dataize' (morphed', seq') univ ctx+        _ -> do+          let side = rule.premises `excluding` [concl]+          final <- sides side subst+          built <- buildExpressionThrows arg final+          seq' <- leadsTo seq (labelOf side) built ctx+          dataize' (built, seq') univ ctx+      Just _ -> throwIO (userError (printf "dataization rule '%s' must conclude with a 'dataize' premise" rule.name))+    sides :: [Y.Premise] -> Subst -> IO Subst+    sides premises subst = foldM (sidePremise univ ctx) subst premises+    -- A spliced dataization step is labelled by its first side-computation —+    -- 'box' by its 'contextualize', 'fire' by its 'lambda'; with none it is blank.+    labelOf :: [Y.Premise] -> String+    labelOf (premise : _) = verb premise.operation+    labelOf [] = "" +-- The premise binding the given expression meta, if any. The conclusion of a+-- morphing rule and the argument of a continuation premise are looked up here to+-- find the premise that produces them.+producer :: Expression -> [Y.Premise] -> Maybe Y.Premise+producer (ExMeta name) = find (\premise -> premise.result == name)+producer _ = const Nothing++-- The premise binding the given bytes meta, if any — the dataization analogue of+-- 'producer' for a rule's bytes conclusion.+bytesProducer :: Bytes -> [Y.Premise] -> Maybe Y.Premise+bytesProducer (BtMeta name) = find (\premise -> premise.result == name)+bytesProducer _ = const Nothing++-- The premises whose result meta is not bound by any of the given ones — the+-- side-computations left once the spine premises are removed.+excluding :: [Y.Premise] -> [Y.Premise] -> [Y.Premise]+excluding premises removed = filter (\premise -> premise.result `notElem` map (.result) removed) premises++-- Evaluate one side-computation premise — a 'morph', 'lambda' or 'contextualize'+-- of an earlier term — in isolation, binding its result meta. These never splice+-- steps into the trace: 'morph' and 'lambda' reduce on a fresh chain and discard+-- it, 'contextualize' is pure.+sidePremise :: Expression -> DataizeContext -> Subst -> Y.Premise -> IO Subst+sidePremise univ ctx subst premise = do+  term <- execBuildTerm univ ctx (verb premise.operation) (verbArgs premise.operation) subst+  case combine (substSingle premise.result (metaValue term)) subst of+    Just subst' -> pure subst'+    Nothing -> throwIO (userError (printf "premise meta '%s' clashes with an existing binding" (T.unpack premise.result)))+  where+    metaValue :: Term -> MetaValue+    metaValue (TeExpression value) = MvExpression value+    metaValue (TeAttribute value) = MvAttribute value+    metaValue (TeBytes value) = MvBytes value+    metaValue (TeBindings value) = MvBindings value++-- The build-term function name backing a premise operation.+verb :: Y.Operation -> String+verb (Y.OpMorph _) = "morph"+verb (Y.OpNormalize _) = "normalize"+verb (Y.OpLambda _) = "lambda"+verb (Y.OpContextualize _ _) = "contextualize"+verb (Y.OpDataize _) = "dataize"++-- The build-term arguments backing a premise operation.+verbArgs :: Y.Operation -> [ExtraArgument]+verbArgs (Y.OpMorph expr) = [ArgExpression expr]+verbArgs (Y.OpNormalize expr) = [ArgExpression expr]+verbArgs (Y.OpLambda expr) = [ArgExpression expr]+verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context]+verbArgs (Y.OpDataize expr) = [ArgExpression expr]+ leadsTo :: NonEmpty Rewritten -> String -> Expression -> DataizeContext -> IO (NonEmpty Rewritten) leadsTo ((prog, _) :| rest) rule expr DataizeContext{..} = do   prog' <- withLocatedExpression _locator expr prog   pure ((prog', Nothing) :| (prog, Just rule) : rest) --- Reduce 'expr' to its normal form through the normalization rewriter,--- splicing the individual steps (alpha, copy, dot, …) into the chain and--- returning the normalized expression together with the extended sequence.+-- Reduce 'expr' to its normal form through the normalization rewriter, embedding+-- it at '_locator' into the working program taken from the head of the step+-- chain so the rewriter sees the surrounding context. Splices the individual+-- steps (alpha, copy, dot, …) into the chain and returns the normalized+-- expression together with the extended sequence. normalized :: Expression -> NonEmpty Rewritten -> DataizeContext -> IO (Expression, NonEmpty Rewritten) normalized expr seq ctx@DataizeContext{..} = do-  prog' <- withLocatedExpression _locator expr _program+  prog' <- withLocatedExpression _locator expr (fst (NE.head seq))   (rewrittens, _) <- rewrite prog' normalizationRules (rewriteContext ctx)   let (rw :| rws) = NE.reverse rewrittens       seq' = rw :| rws <> NE.tail seq@@ -190,87 +278,82 @@     rewriteContext DataizeContext{..} =       RewriteContext _locator _maxDepth _maxCycles _depthSensitive _buildTerm MtDisabled Nothing _saveStep --- Synthetic dataize function for internal usage inside atoms--- Here we modify original program from context by adding new binding--- which refers to expression we want to dataize. As a caller of 𝔻, it first--- reduces the expression to a normal form, since 𝔻 only accepts normal forms.-_dataize :: Expression -> DataizeContext -> IO (Maybe Bytes)-_dataize expr ctx@DataizeContext{_buildTerm = buildTerm, _program = Program (ExFormation bds)} = do-  (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty-  let prog = Program (ExFormation (BiTau attr expr : bds))-      ctx' = ctx{_program = prog}-  (normal, seq) <- normalized expr ((prog, Nothing) :| []) ctx'-  (bts, _) <- dataize' (normal, seq) ctx'-  pure bts-_dataize _ _ = throwIO (userError "Can't call _dataize from atoms with non-formation program")+-- Synthetic dataize function for internal usage inside atoms. Here we modify the+-- universe by adding a new binding which refers to the expression we want to+-- dataize, building a local working program to reduce within. As a caller of 𝔻,+-- it first reduces the expression to a normal form, since 𝔻 only accepts normal+-- forms. The universe 'univ' itself is forwarded unchanged, so morphing Φ under+-- this context still resolves to the true universe rather than to this+-- synthetic, binding-prepended formation.+_dataize :: Expression -> Expression -> DataizeContext -> IO Bytes+_dataize expr univ ctx@DataizeContext{_buildTerm = buildTerm} = case univ of+  ExFormation bds -> do+    (TeAttribute attr) <- buildTerm "random-tau" [] substEmpty+    let prog = Program (ExFormation (BiTau attr expr : bds))+    (normal, seq) <- normalized expr ((prog, Nothing) :| []) ctx+    (bts, _) <- dataize' (normal, seq) univ ctx+    pure bts+  _ -> throwIO (userError "Can't call _dataize from atoms with non-formation universe") -atom :: T.Text -> Expression -> DataizeContext -> IO Expression-atom "L_number_plus" self ctx = do-  left <- _dataize (ExDispatch self (AtLabel "x")) ctx-  right <- _dataize (ExDispatch self AtRho) ctx-  case (left, right) of-    (Just left', Just right') -> do-      let first = either toDouble id (btsToNum left')-          second = either toDouble id (btsToNum right')-          sum = first + second-      pure (DataNumber (numToBts sum))+-- A number atom only operates on numeric data. Empty bytes (the result of+-- dataizing a bare formation ⟦𝐵⟧ or ⊥ now that 𝔻 is total) carry no number,+-- so the operand is rejected and the atom yields ⊥.+asNumber :: Bytes -> Maybe Double+asNumber BtEmpty = Nothing+asNumber bts = Just (either toDouble id (btsToNum bts))++atom :: T.Text -> Expression -> Expression -> DataizeContext -> IO Expression+atom "L_number_plus" self univ ctx = do+  left <- _dataize (ExDispatch self (AtLabel "x")) univ ctx+  right <- _dataize (ExDispatch self AtRho) univ ctx+  case (asNumber left, asNumber right) of+    (Just first, Just second) -> pure (DataNumber (numToBts (first + second)))     _ -> pure ExTermination-atom "L_number_times" self ctx = do-  left <- _dataize (ExDispatch self (AtLabel "x")) ctx-  right <- _dataize (ExDispatch self AtRho) ctx-  case (left, right) of-    (Just left', Just right') -> do-      let first = either toDouble id (btsToNum left')-          second = either toDouble id (btsToNum right')-          sum = first * second-      pure (DataNumber (numToBts sum))+atom "L_number_times" self univ ctx = do+  left <- _dataize (ExDispatch self (AtLabel "x")) univ ctx+  right <- _dataize (ExDispatch self AtRho) univ ctx+  case (asNumber left, asNumber right) of+    (Just first, Just second) -> pure (DataNumber (numToBts (first * second)))     _ -> pure ExTermination-atom "L_number_eq" self ctx = do-  x <- _dataize (ExDispatch self (AtLabel "x")) ctx-  rho <- _dataize (ExDispatch self AtRho) ctx-  case (x, rho) of-    (Just x', Just rho') -> do-      let self' = either toDouble id (btsToNum rho')-          first = either toDouble id (btsToNum x')+atom "L_number_eq" self univ ctx = do+  x <- _dataize (ExDispatch self (AtLabel "x")) univ ctx+  rho <- _dataize (ExDispatch self AtRho) univ ctx+  case (asNumber x, asNumber rho) of+    (Just first, Just self') ->       if self' == first         then pure (DataNumber (numToBts first))         else pure (ExDispatch self (AtLabel "y"))     _ -> pure ExTermination-atom func _ _ = throwIO (userError (printf "Atom '%s' does not exist" (T.unpack func)))+atom func _ _ _ = throwIO (userError (printf "Atom '%s' does not exist" (T.unpack func)))  -- Augment the injected, context-free term builder with the dataization and--- morphing operations that need the full evaluation context: 'lambda' applies--- an atom and 'global' dispatches from the universe Q. Every other function is--- delegated unchanged.-execBuildTerm :: DataizeContext -> BuildTermFunc-execBuildTerm ctx "lambda" = _lambda ctx-execBuildTerm ctx "global" = _global ctx-execBuildTerm ctx "morph" = _morph ctx-execBuildTerm ctx func = _buildTerm ctx func+-- morphing operations that need the universe: 'lambda' applies an atom and+-- 'morph' morphs a sub-expression. Both receive the universe 'univ'. Every other+-- function is delegated unchanged.+execBuildTerm :: Expression -> DataizeContext -> BuildTermFunc+execBuildTerm univ ctx "lambda" = _lambda univ ctx+execBuildTerm univ ctx "morph" = _morph univ ctx+execBuildTerm _ ctx func = _buildTerm ctx func -_lambda :: DataizeContext -> BuildTermMethod-_lambda ctx [ArgExpression expr] subst = do+_lambda :: Expression -> DataizeContext -> BuildTermMethod+_lambda univ ctx [ArgExpression expr] subst = do   form <- buildExpressionThrows expr subst   case form of     ExFormation bds -> do-      resolved <- formation bds ctx+      resolved <- formation bds univ ctx       case resolved of         Just obj -> pure (TeExpression obj)         Nothing -> throwIO (userError "Function lambda() expects a formation with a λ binding")     _ -> throwIO (userError "Function lambda() expects a formation")-_lambda _ _ _ = throwIO (userError "Function lambda() requires exactly 1 expression argument")--_global :: DataizeContext -> BuildTermMethod-_global DataizeContext{_program = Program prog} [] _ = pure (TeExpression prog)-_global _ _ _ = throwIO (userError "Function global() requires no arguments")+_lambda _ _ _ _ = throwIO (userError "Function lambda() requires exactly 1 expression argument")  -- The Morphing function 𝕄 exposed as a build-term function so a rule can morph -- a sub-expression in its 'where' (the 'dispatch' and 'application' rules morph -- the head before re-attaching it). The step chain is discarded: the producing -- rule splices the surrounding normalization steps itself.-_morph :: DataizeContext -> BuildTermMethod-_morph ctx@DataizeContext{_program = prog} [ArgExpression expr] subst = do+_morph :: Expression -> DataizeContext -> BuildTermMethod+_morph univ ctx [ArgExpression expr] subst = do   built <- buildExpressionThrows expr subst-  (morphed, _) <- morph (built, (prog, Nothing) :| []) ctx+  (morphed, _) <- morph (built, (Program univ, Nothing) :| []) univ ctx   pure (TeExpression morphed)-_morph _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")+_morph _ _ _ _ = throwIO (userError "Function morph() requires exactly 1 expression argument")

@@ -104,6 +104,7 @@   toASCII CO_MATCHES{..} = CO_MATCHES regex (toASCII expr)   toASCII CO_PART_OF{..} = CO_PART_OF (toASCII expr) (toASCII binding)   toASCII CO_DISJOINT{..} = CO_DISJOINT (map toASCII attrs) (map toASCII groups)+  toASCII CO_FORMATION{..} = CO_FORMATION (toASCII expr)   toASCII CO_EMPTY = CO_EMPTY  instance ToASCII EXTRA_ARG where

@@ -29,7 +29,7 @@ -- 'Dataize.execBuildTerm', not by 'buildTerm'. They are available while -- executing dataization and morphing rules, but not rewriting rules. execFunctions :: [String]-execFunctions = ["lambda", "global", "morph"]+execFunctions = ["lambda", "morph"]  buildTerm :: BuildTermFunc buildTerm func args subst = do

@@ -21,6 +21,7 @@   , LatexContext (..)   , meetInPrograms   , meetInProgram+  , conditionToLatex   ) where  import AST@@ -339,6 +340,7 @@   toLaTeX CO_MATCHES{..} = CO_MATCHES regex (toLaTeX expr)   toLaTeX CO_PART_OF{..} = CO_PART_OF (toLaTeX expr) (toLaTeX binding)   toLaTeX CO_DISJOINT{..} = CO_DISJOINT (map toLaTeX attrs) (map toLaTeX groups)+  toLaTeX CO_FORMATION{..} = CO_FORMATION (toLaTeX expr)   toLaTeX CO_EMPTY = CO_EMPTY  instance ToLaTeX EXTRA_ARG where@@ -368,46 +370,63 @@     joinedConditions Nothing second@(Just _) = second     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. explainMorphRule :: Y.MorphRule -> String explainMorphRule rule =-  trrule-    "\\phinoMorphingRule"-    rule.label+  inference     rule.name-    (morph (renderToLatex (expressionToCST rule.match) defaultLatexContext))-    (morphOutcome rule.then_)+    rule.label     rule.when-    rule.where_-  where-    morphOutcome :: Y.MorphOutcome -> String-    morphOutcome (Y.MoMorph (Y.MaExpr expr)) = morph (renderToLatex (expressionToCST expr) defaultLatexContext)-    morphOutcome (Y.MoMorph (Y.MaNormalize expr)) = morph (normalize (renderToLatex (expressionToCST expr) defaultLatexContext))-    morphOutcome (Y.MoStop expr) = renderToLatex (expressionToCST expr) defaultLatexContext+    (map premiseToLatex rule.premises)+    (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (renderExpr rule.nresult)) +-- Render a dataization rule as a LaTeX inference rule, with 𝔻(match, e) ⟿+-- d-result as the conclusion below the line. explainDataizeRule :: Y.DataizeRule -> String explainDataizeRule rule =-  trrule-    "\\phinoDataizationRule"-    rule.label+  inference     rule.name-    (dataize (renderToLatex (expressionToCST rule.match) defaultLatexContext))-    (dataizeOutcome rule.then_)+    rule.label     rule.when-    rule.where_-  where-    dataizeOutcome :: Y.DataizeOutcome -> String-    dataizeOutcome (Y.DoDataize (Y.DaExpr expr)) = dataize (renderToLatex (expressionToCST expr) defaultLatexContext)-    dataizeOutcome (Y.DoDataize (Y.DaMorph expr)) = dataize (morph (renderToLatex (expressionToCST expr) defaultLatexContext))-    dataizeOutcome (Y.DoDataize (Y.DaNormalize expr)) = dataize (normalize (renderToLatex (expressionToCST expr) defaultLatexContext))-    dataizeOutcome (Y.DoData bytes) = T.unpack (render (toLaTeX (toCST' bytes :: BYTES)))-    dataizeOutcome Y.DoNothing = "\\varnothing"+    (map premiseToLatex rule.premises)+    (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (renderBytes rule.dresult)) --- Render a single rule row through the given macro (one of--- \phinoMorphingRule, \phinoNormalizationRule, \phinoDataizationRule): an--- optional typeset label, name, left-hand side, right-hand side, the optional--- 'if' condition and 'where' extras. When the label is present it becomes the--- macro's first optional argument ('\macro[label]{name}'); when absent the--- optional argument is omitted entirely ('\macro{name}').+-- 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.OpLambda arg -> phinoEvaluate (renderExpr arg) (renderExpr (ExMeta premise.result))+  Y.OpContextualize arg context -> phinoContextualize (renderExpr arg) (renderExpr context) (renderExpr (ExMeta premise.result))++-- Assemble an inference block from a name, optional label, optional side+-- condition, the premise judgments and the conclusion judgment.+inference :: String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String+inference name label cond premises conclusion =+  intercalate "\n" $+    ["\\begin{phinoInference}", "  \\phinoName{" ++ name ++ "}"]+      ++ maybe [] (\symbol -> ["  \\phinoLabel{" ++ symbol ++ "}"]) label+      ++ maybe [] (\rendered -> ["  \\phinoCondition{ " ++ rendered ++ " }"]) (conditionInLatex cond)+      ++ map (\premise -> "  \\phinoPremise{ " ++ premise ++ " }") premises+      ++ ["  \\phinoConclusion{ " ++ conclusion ++ " }", "\\end{phinoInference}"]++renderExpr :: Expression -> String+renderExpr expr = renderToLatex (expressionToCST expr) defaultLatexContext++renderBytes :: Bytes -> String+renderBytes bytes = T.unpack (render (toLaTeX (toCST' bytes :: BYTES)))++-- Render a single normalization rule row through the \phinoNormalizationRule+-- macro: an optional typeset label, name, left-hand side, right-hand side, the+-- optional 'if' condition and 'where' extras. When the label is present it+-- becomes the macro's first optional argument ('\macro[label]{name}'); when+-- absent the optional argument is omitted entirely ('\macro{name}').+-- Morphing and dataization rules render as inference rules instead (see+-- 'explainMorphRule' and 'explainDataizeRule'). trrule :: String -> Maybe String -> String -> String -> String -> Maybe Y.Condition -> Maybe [Y.Extra] -> String trrule macro label name lhs rhs cond extras =   intercalate@@ -421,14 +440,29 @@   where     labelArg = maybe "" (\symbol -> "[" ++ symbol ++ "]") label -morph :: String -> String-morph inner = "\\phinoMorph{ " ++ inner ++ " }"+-- 𝕄 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 -dataize :: String -> String-dataize inner = "\\phinoDataize{ " ++ inner ++ " }"+phinoDataize :: String -> String -> String -> String+phinoDataize input univ output = printf "\\phinoDataize{ %s }{ %s }{ %s }" input univ output -normalize :: String -> String-normalize inner = "\\phinoNormalize{ " ++ inner ++ " }"+phinoNormalize :: String -> String -> String+phinoNormalize input = printf "\\phinoNormalize{ %s }{ %s }" input++phinoEvaluate :: String -> String -> String+phinoEvaluate input = printf "\\phinoEvaluate{ %s }{ %s }" input++phinoContextualize :: String -> String -> String -> String+phinoContextualize input context = printf "\\phinoContextualize{ %s }{ %s }{ %s }" input context++conditionInLatex :: Maybe Y.Condition -> Maybe String+conditionInLatex Nothing = Nothing+conditionInLatex (Just cond) = case conditionToCST cond of+  CO_EMPTY -> Nothing+  cond' -> Just (renderToLatex cond' defaultLatexContext)  braced :: String -> String braced = printf "{ %s }"

@@ -83,6 +83,7 @@   toSingleLine CO_MATCHES{..} = CO_MATCHES regex (toSingleLine expr)   toSingleLine CO_PART_OF{..} = CO_PART_OF (toSingleLine expr) (toSingleLine binding)   toSingleLine CO_DISJOINT{..} = CO_DISJOINT attrs (map toSingleLine groups)+  toSingleLine CO_FORMATION{..} = CO_FORMATION (toSingleLine expr)   toSingleLine CO_EMPTY = CO_EMPTY  instance ToSingleLine EXTRA_ARG where

@@ -247,7 +247,7 @@   render EQUAL = "="   render NOT_EQUAL = "\\not="   render GREATER = ">"-  render NOT_GREATER = "\\not>"+  render NOT_GREATER = "\\leq"  instance Render CONDITION where   render CO_BELONGS{..} = render attr <> " " <> render belongs <> " " <> render set@@ -260,10 +260,12 @@       renderWrapped cond = render cond   render CO_NF{..} = "\\isnormal{ " <> render expr <> " }"   render CO_ABSOLUTE{..} = render expr <> " " <> render belongs <> " \\mathcal{K}"+  render CO_NOT{condition = CO_FORMATION{..}} = "\\phinoNotFormation{ " <> render expr <> " }"   render CO_NOT{..} = renderFunc "not" condition   render CO_COMPARE{..} = render left <> " " <> render equal <> " " <> render right   render CO_MATCHES{..} = "matches( " <> T.pack regex <> ", " <> render expr <> " )"   render CO_PART_OF{..} = "part-of( " <> render expr <> ", " <> render binding <> " )"+  render CO_FORMATION{..} = "\\phinoIsFormation{ " <> render expr <> " }"   render CO_DISJOINT{..} =     "[ "       <> T.intercalate ", " (map render attrs)@@ -283,10 +285,12 @@  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 }"   render EXTRA{..} = render meta <> " \\coloneqq " <> macro func <> "{ " <> T.intercalate ", " (map render args) <> " }"     where       macro :: String -> Text       macro "lambda" = "\\phinoEvaluate"-      macro "morph" = "\\phinoMorph"-      macro "global" = "\\phinoGlobal"       macro name = "\\" <> T.pack name

@@ -195,6 +195,18 @@     xiFree (ExDispatch e _) = xiFree e     xiFree _ = False +-- Hold when the given expression is a formation (an abstraction ⟦…⟧). A meta+-- is resolved first, so 'binding 𝑛' inspects whatever 𝑛 is bound to.+_isFormation :: Expression -> Subst -> RuleContext -> IO [Subst]+_isFormation (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of+  Just (MvExpression expr) -> _isFormation expr (Subst mp) ctx+  _ -> pure []+_isFormation expr subst _ = pure [subst | isFormation expr]+  where+    isFormation :: Expression -> Bool+    isFormation (ExFormation _) = True+    isFormation _ = False+ _matches :: String -> Expression -> Subst -> RuleContext -> IO [Subst] _matches pat (ExMeta meta) (Subst mp) ctx = case M.lookup meta mp of   Just (MvExpression expr) -> _matches pat expr (Subst mp) ctx@@ -247,6 +259,7 @@ meetCondition' (Y.Matches pat expr) = _matches pat expr meetCondition' (Y.PartOf expr bd) = _partOf expr bd meetCondition' (Y.Disjoint attrs bds) = _disjoint attrs bds+meetCondition' (Y.IsFormation expr) = _isFormation expr  -- For each substitution check if it meetCondition to given condition -- If substitution does not meet the condition - it's thrown out@@ -343,19 +356,25 @@ kMetaNames = metaNamesWithPrefix "k"  matchExpressionWithRule :: Expression -> Y.Rule -> RuleContext -> IO [Subst]-matchExpressionWithRule = matchExpressionBy matchExpression+matchExpressionWithRule = matchExpressionBy matchExpression [substEmpty]  -- Like 'matchExpressionWithRule' but matches the pattern against the whole -- expression only (no deep, sub-expression matching). Used by the dataization -- and morphing driver, where a rule applies to the entire configuration rather--- than to nested redexes.-matchExpressionWithRule' :: Expression -> Y.Rule -> RuleContext -> IO [Subst]+-- than to nested redexes. The leading '[Subst]' seeds matching with pre-bound+-- meta-variables: the morphing driver passes the global universe bound to 'e',+-- the second argument of 𝕄(n, e), so the 'root' rule reads it directly instead+-- of through a 'global()' build-term function. Pass '[substEmpty]' for no seed.+matchExpressionWithRule' :: [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst] matchExpressionWithRule' = matchExpressionBy matchExpression' -matchExpressionBy :: MatchExpressionFunc -> Expression -> Y.Rule -> RuleContext -> IO [Subst]-matchExpressionBy matcher expr rule ctx =+-- The seed substitutions are combined into every match, so a pre-bound meta in+-- the seed is dropped only when the pattern binds the same name to a different+-- value; rules that do not mention the name simply carry it along unused.+matchExpressionBy :: MatchExpressionFunc -> [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst]+matchExpressionBy matcher seed expr rule ctx =   let ptn = rule.pattern-      matched = matcher ptn expr+      matched = combineMany seed (matcher ptn expr)       name = rule.name    in if null matched         then do

@@ -197,6 +197,7 @@   toSalty CO_MATCHES{..} = CO_MATCHES regex (toSalty expr)   toSalty CO_PART_OF{..} = CO_PART_OF (toSalty expr) (toSalty binding)   toSalty CO_DISJOINT{..} = CO_DISJOINT attrs (map toSalty groups)+  toSalty CO_FORMATION{..} = CO_FORMATION (toSalty expr)   toSalty CO_EMPTY = CO_EMPTY  instance ToSalty EXTRA_ARG where

@@ -83,13 +83,14 @@     withObject       "Condition"       ( \v -> do-          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "gt", "in", "matches", "part-of", "disjoint"]+          validateYamlObject v ["and", "or", "not", "nf", "absolute", "eq", "gt", "in", "matches", "part-of", "disjoint", "formation"]           asum             [ And <$> v .: "and"             , Or <$> v .: "or"             , Not <$> v .: "not"             , NF <$> v .: "nf"             , Absolute <$> v .: "absolute"+            , IsFormation <$> v .: "formation"             , do                 vals <- v .: "disjoint"                 case vals of@@ -180,6 +181,7 @@   | Matches String Expression   | PartOf Expression Binding   | Disjoint [Attribute] [Binding]+  | IsFormation Expression   deriving (Eq, Generic, Show)  data ExtraArgument@@ -221,92 +223,90 @@ yamlRule :: FilePath -> IO Rule yamlRule = Yaml.decodeFileThrow --- The right-hand side of a morphing reduction 𝕄(match) ⟿ then.--- A mapping ('{ morph: arg }') keeps reducing under 𝕄; a bare expression--- (including ⊥) is the terminal result.-data MorphOutcome-  = MoMorph MorphArg-  | MoStop Expression-  deriving (Eq, Generic, Show)---- The argument of a morphing continuation: either a plain expression ('𝕄(e)')--- or the normalization of one ('𝕄(𝒩(e))', written '{ normalize: e }').-data MorphArg-  = MaExpr Expression-  | MaNormalize Expression-  deriving (Eq, Generic, Show)---- The right-hand side of a dataization reduction 𝔻(match) ⟿ then.--- A mapping ('{ dataize: arg }') keeps reducing under 𝔻; a bare bytes scalar--- yields data; the 'nothing' keyword marks the function as undefined.-data DataizeOutcome-  = DoDataize DataizeArg-  | DoData Bytes-  | DoNothing+-- One premise above the inference line of a morphing or dataization rule: bind+-- the meta named 'result' to the value of applying 'operation' to its argument.+-- The universe e is the fixed second argument of 𝕄 and 𝔻, not a per-premise+-- value, so it is not recorded here.+data Premise = Premise+  { result :: Text+  , operation :: Operation+  }   deriving (Eq, Generic, Show) --- The argument of a dataization continuation: a plain expression ('𝔻(e)'),--- the morphing of one ('𝔻(𝕄(e))', written '{ morph: e }'), or the--- normalization of one ('𝔻(𝒩(e))', written '{ normalize: e }').-data DataizeArg-  = DaExpr Expression-  | DaMorph Expression-  | DaNormalize Expression+-- The reduction a premise performs, mirroring the build-term functions and the+-- 𝒩 and 𝔻 reducers the engine already provides.+data Operation+  = OpMorph Expression+  | OpNormalize Expression+  | OpLambda Expression+  | OpContextualize Expression Expression+  | OpDataize Expression   deriving (Eq, Generic, Show) --- One ordered morphing rule: match the expression, build extra metas in--- 'where', filter by 'when', then reduce per 'then'.+-- One morphing rule in inference-rule form: when 'match' matches the term and+-- 'ematch' matches the universe (binding 'e'), the rule yields 'nresult' (a+-- premise meta or a literal) provided 'when' holds and the ordered 'premises'+-- reduce as stated. 'ematch' is the universe-argument matcher of 𝕄(n, e), in+-- practice always the '𝑒' meta. data MorphRule = MorphRule   { name :: String   , label :: Maybe String-  , description :: Maybe String   , match :: Expression-  , where_ :: Maybe [Extra]+  , ematch :: Expression+  , nresult :: Expression   , when :: Maybe Condition-  , then_ :: MorphOutcome+  , premises :: [Premise]   }   deriving (Generic, Show) --- One ordered dataization rule, structured like 'MorphRule' but reducing--- under 𝔻 and able to terminate with bytes or 'nothing'.+-- One dataization rule in inference-rule form, structured like 'MorphRule' but+-- terminating with bytes ('dresult'). data DataizeRule = DataizeRule   { name :: String   , label :: Maybe String-  , description :: Maybe String   , match :: Expression-  , where_ :: Maybe [Extra]+  , ematch :: Expression+  , dresult :: Bytes   , when :: Maybe Condition-  , then_ :: DataizeOutcome+  , premises :: [Premise]   }   deriving (Generic, Show) -instance FromJSON MorphOutcome where-  parseJSON (Object o) = do-    validateYamlObject o ["morph"]-    MoMorph <$> o .: "morph"-  parseJSON v = MoStop <$> parseJSON v--instance FromJSON MorphArg where-  parseJSON (Object o) = do-    validateYamlObject o ["normalize"]-    MaNormalize <$> o .: "normalize"-  parseJSON v = MaExpr <$> parseJSON v+instance FromJSON Premise where+  parseJSON =+    withObject+      "Premise"+      (\o -> Premise <$> premiseResult o <*> premiseOperation o) -instance FromJSON DataizeOutcome where-  parseJSON (Object o) = do-    validateYamlObject o ["dataize"]-    DoDataize <$> o .: "dataize"-  parseJSON (String "nothing") = pure DoNothing-  parseJSON v = DoData <$> parseJSON v+-- The meta a premise binds, taken from its 'n-result' (an expression meta) or+-- 'd-result' (a bytes meta).+premiseResult :: Object -> Parser Text+premiseResult o = do+  expr <- o .:? "n-result"+  case expr of+    Just (ExMeta metaName) -> pure metaName+    Just _ -> fail "'n-result' must be an expression meta"+    Nothing -> do+      bytes <- o .:? "d-result"+      case bytes of+        Just (BtMeta metaName) -> pure metaName+        Just _ -> fail "'d-result' must be a bytes meta"+        Nothing -> fail "a premise needs an 'n-result' or 'd-result' meta" -instance FromJSON DataizeArg where-  parseJSON (Object o) = do-    validateYamlObject o ["morph", "normalize"]-    morphed <- o .:? "morph"-    case morphed of-      Just expr -> pure (DaMorph expr)-      Nothing -> DaNormalize <$> o .: "normalize"-  parseJSON v = DaExpr <$> parseJSON v+-- The single verb of a premise.+premiseOperation :: Object -> Parser Operation+premiseOperation o =+  asum+    [ OpMorph <$> o .: "morph"+    , OpNormalize <$> o .: "normalize"+    , OpLambda <$> o .: "lambda"+    , do+        vals <- o .: "contextualize"+        case vals of+          [expr, context] -> OpContextualize <$> parseJSON expr <*> parseJSON context+          _ -> fail "'contextualize' expects exactly two arguments"+    , OpDataize <$> o .: "dataize"+    ]  instance FromJSON MorphRule where   parseJSON =@@ -316,11 +316,11 @@           MorphRule             <$> o .: "name"             <*> o .:? "label"-            <*> o .:? "description"             <*> o .: "match"-            <*> o .:? "where"+            <*> o .: "e-match"+            <*> o .: "n-result"             <*> o .:? "when"-            <*> o .: "then"+            <*> o .:? "premises" .!= []       )  instance FromJSON DataizeRule where@@ -331,11 +331,11 @@           DataizeRule             <$> o .: "name"             <*> o .:? "label"-            <*> o .:? "description"             <*> o .: "match"-            <*> o .:? "where"+            <*> o .: "e-match"+            <*> o .: "d-result"             <*> o .:? "when"-            <*> o .: "then"+            <*> o .:? "premises" .!= []       )  decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a]

@@ -867,9 +867,9 @@       withStdin "Q -> [[ D> 01- ]]" $         testCLISucceeded ["dataize"] ["01-"] -    it "dataizes to dead" $+    it "dataizes empty object to empty bytes" $       withStdin "Q -> [[ ]]" $-        testCLISucceeded ["dataize"] ["⊥"]+        testCLISucceeded ["dataize"] ["--"]      it "dataizes with --sequence" $       withStdin "{[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]}" $@@ -981,7 +981,7 @@             , "\\phinoNormalizationRule{amiss}"             , "  { [[ B ]] ( \\phiTerminal{\\alpha_{i}} -> e ) }"             , "  { T }"-            , "  { \\vert \\overline{ B } \\vert \\not> i }"+            , "  { \\vert \\overline{ B } \\vert \\leq i }"             , "  { }"             , "\\phinoNormalizationRule{copy}"             , "  { [[ B_1, \\tau -> ?, B_2 ]] ( \\tau -> k ) }"@@ -1045,51 +1045,67 @@       testCLISucceeded         ["explain", "--morph"]         [ unlines-            [ "\\phinoMorphingRule{prim}"-            , "  { \\phinoMorph{ [[ B ]] } }"-            , "  { [[ B ]] }"-            , "  { }"-            , "  { }"-            , "\\phinoMorphingRule[\\lambda]{lambda}"-            , "  { \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau } }"-            , "  { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }"-            , "  { }"-            , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"-            , "\\phinoMorphingRule{dispatch}"-            , "  { \\phinoMorph{ n . \\tau } }"-            , "  { \\phinoMorph{ \\phinoNormalize{ e . \\tau } } }"-            , "  { }"-            , "  { e \\coloneqq \\phinoMorph{ n } }"-            , "\\phinoMorphingRule{application}"-            , "  { \\phinoMorph{ n ( \\tau -> e ) } }"-            , "  { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\tau -> e ) } } }"-            , "  { }"-            , "  { e_1 \\coloneqq \\phinoMorph{ n } }"-            , "\\phinoMorphingRule{applicationa}"-            , "  { \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e ) } }"-            , "  { \\phinoMorph{ \\phinoNormalize{ e_1 ( \\phiTerminal{\\alpha_{i}} -> e ) } } }"-            , "  { }"-            , "  { e_1 \\coloneqq \\phinoMorph{ n } }"-            , "\\phinoMorphingRule{root}"-            , "  { \\phinoMorph{ Q } }"-            , "  { \\phinoMorph{ \\phinoNormalize{ e } } }"-            , "  { e \\not= Q }"-            , "  { e \\coloneqq \\phinoGlobal{  } }"-            , "\\phinoMorphingRule{dead}"-            , "  { \\phinoMorph{ T } }"-            , "  { T }"-            , "  { }"-            , "  { }"-            , "\\phinoMorphingRule{xi}"-            , "  { \\phinoMorph{ \\phiTerminal{\\xi} } }"-            , "  { T }"-            , "  { }"-            , "  { }"-            , "\\phinoMorphingRule{globe}"-            , "  { \\phinoMorph{ Q } }"-            , "  { T }"-            , "  { }"-            , "  { }"+            [ "\\begin{phinoInference}"+            , "  \\phinoName{prim}"+            , "  \\phinoLabel{prim}"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ [[ B ]] } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{lambda}"+            , "  \\phinoLabel{\\lambda}"+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }"+            , "  \\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 } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{dispatch}"+            , "  \\phinoLabel{disp}"+            , "  \\phinoCondition{ \\phinoNotFormation{ n } }"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ n_3 } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{application}"+            , "  \\phinoLabel{app}"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\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 } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{applicationa}"+            , "  \\phinoLabel{appa}"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\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 } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{root}"+            , "  \\phinoLabel{root}"+            , "  \\phinoCondition{ e \\not= Q }"+            , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ n_1 } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{dead}"+            , "  \\phinoLabel{dead}"+            , "  \\phinoConclusion{ \\phinoMorph{ T }{ e }{ T } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{xi}"+            , "  \\phinoLabel{xi}"+            , "  \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ T } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{globe}"+            , "  \\phinoLabel{globe}"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ T } }"+            , "\\end{phinoInference}"             ]         ] @@ -1097,36 +1113,45 @@       testCLISucceeded         ["explain", "--dataize"]         [ unlines-            [ "\\phinoDataizationRule[\\Delta]{delta}"-            , "  { \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] } }"-            , "  { \\delta }"-            , "  { }"-            , "  { }"-            , "\\phinoDataizationRule{box}"-            , "  { \\phinoDataize{ [[ B_1, @ -> e, B_2 ]] } }"-            , "  { \\phinoDataize{ \\phinoNormalize{ e_1 } } }"-            , "  { [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset }"-            , "  { e_1 \\coloneqq \\ctx{ e }{ [[ B_1, @ -> e, B_2 ]] } }"-            , "\\phinoDataizationRule{fire}"-            , "  { \\phinoDataize{ [[ B_1, L> F, B_2 ]] } }"-            , "  { \\phinoDataize{ \\phinoNormalize{ e } } }"-            , "  { }"-            , "  { e \\coloneqq \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] } }"-            , "\\phinoDataizationRule{none}"-            , "  { \\phinoDataize{ [[ B ]] } }"-            , "  { \\varnothing }"-            , "  { }"-            , "  { }"-            , "\\phinoDataizationRule{bott}"-            , "  { \\phinoDataize{ T } }"-            , "  { \\varnothing }"-            , "  { }"-            , "  { }"-            , "\\phinoDataizationRule{norm}"-            , "  { \\phinoDataize{ n } }"-            , "  { \\phinoDataize{ \\phinoMorph{ n } } }"-            , "  { }"-            , "  { }"+            [ "\\begin{phinoInference}"+            , "  \\phinoName{delta}"+            , "  \\phinoLabel{\\Delta}"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ \\delta } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{box}"+            , "  \\phinoLabel{box}"+            , "  \\phinoCondition{ [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\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 } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{fire}"+            , "  \\phinoLabel{fire}"+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }"+            , "  \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ \\delta } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{none}"+            , "  \\phinoLabel{none}"+            , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ -- } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{bott}"+            , "  \\phinoLabel{bott}"+            , "  \\phinoConclusion{ \\phinoDataize{ T }{ e }{ -- } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{norm}"+            , "  \\phinoLabel{norm}"+            , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"+            , "  \\phinoConclusion{ \\phinoDataize{ n }{ e }{ \\delta } }"+            , "\\end{phinoInference}"             ]         ] 

@@ -25,6 +25,7 @@       , "absolute(!e1)"       , "matches(\"hello(\\\"\\u0000)\", !e)"       , "part-of ( [[ x -> 1 ]] , !B ) "+      , "not(formation(!n))"       ]       (\expr -> it expr (parseCondition expr `shouldSatisfy` isRight)) @@ -39,6 +40,7 @@       , ("eq(!t1, !e2)", Y.Eq (Y.CmpAttr (AtMeta "t1")) (Y.CmpExpr (ExMeta "e2")))       , ("or(absolute(!e1), nf(Q.x))", Y.Or [Y.Absolute (ExMeta "e1"), Y.NF (ExDispatch ExRoot (AtLabel "x"))])       , ("and(matches(\"hi\", !e),part-of(!e, !B))", Y.And [Y.Matches "hi" (ExMeta "e"), Y.PartOf (ExMeta "e") (BiMeta "B")])+      , ("not(formation(!n))", Y.Not (Y.IsFormation (ExMeta "n")))       ]       (\(expr, res) -> it expr (parseCondition expr `shouldBe` Right res)) 

@@ -7,35 +7,38 @@ module DataizeSpec (spec) where  import AST+import Control.Exception (SomeException) import Control.Monad-import Data.List (nub)+import Data.List (find, isInfixOf, nub) import Data.List.NonEmpty (NonEmpty (..))+import Data.Maybe (fromMaybe) import Dataize (DataizeContext (DataizeContext), dataize, dataize', execBuildTerm, morph)-import Deps (Term (TeExpression), dontSaveStep)+import Deps (dontSaveStep) import Functions (buildTerm) import Matcher (substEmpty) import Parser (parseExpressionThrows, parseProgramThrows) import Rewriter (Rewritten)+import Rule (RuleContext (RuleContext), matchExpressionWithRule') import Test.Hspec import Yaml qualified -defaultDataizeContext :: Expression -> Program -> DataizeContext-defaultDataizeContext loc prog = DataizeContext loc prog 25 25 False buildTerm dontSaveStep+defaultDataizeContext :: Expression -> DataizeContext+defaultDataizeContext loc = DataizeContext loc 25 25 False buildTerm dontSaveStep -test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> DataizeContext -> IO (Maybe a, [Rewritten])) -> [(String, Expression, Expression, Maybe a)] -> Spec+test :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> DataizeContext -> IO (a, [Rewritten])) -> [(String, Expression, Expression, a)] -> Spec test func useCases =   forM_ useCases $ \(desc, input, expr, output) ->     it desc $ do       let prog = Program expr-      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog)+      (res, _) <- func (input, (prog, Nothing) :| []) expr (defaultDataizeContext ExRoot)       res `shouldBe` output -test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> DataizeContext -> IO (a, NonEmpty Rewritten)) -> [(String, Expression, Expression, a)] -> Spec+test' :: (Eq a, Show a) => ((Expression, NonEmpty Rewritten) -> Expression -> DataizeContext -> IO (a, NonEmpty Rewritten)) -> [(String, Expression, Expression, a)] -> Spec test' func useCases =   forM_ useCases $ \(desc, input, expr, output) ->     it desc $ do       let prog = Program expr-      (res, _) <- func (input, (prog, Nothing) :| []) (defaultDataizeContext ExRoot prog)+      (res, _) <- func (input, (prog, Nothing) :| []) expr (defaultDataizeContext ExRoot)       res `shouldBe` output  testDataize :: [(String, String, String, Bytes)] -> Spec@@ -44,8 +47,8 @@     it name $ do       prog' <- parseProgramThrows prog       loc' <- parseExpressionThrows loc-      (value, _) <- dataize (defaultDataizeContext loc' prog')-      value `shouldBe` Just res+      (value, _) <- dataize prog' (defaultDataizeContext loc')+      value `shouldBe` res  spec :: Spec spec = do@@ -64,16 +67,45 @@         )       ] +  -- 'dispatch' fires only when its head is not a formation ('not (formation 𝑛)'),+  -- so a formation head — λ-bearing or not — is left to 'lambda'/'prim'. The+  -- two clauses are mutually exclusive and their order in 'morphing.yaml'+  -- cannot change behavior.+  describe "morphing 'dispatch' is disjoint from 'lambda'" $ do+    let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot))+        morphRule :: String -> Yaml.MorphRule+        morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules)+        asRule :: Yaml.MorphRule -> Yaml.Rule+        asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing+        lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho]+    it "does not fire on a λ-bearing formation dispatch" $ do+      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "dispatch")) rctx+      substs `shouldBe` []+    it "still fires on a non-λ-formation dispatch" $ do+      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "dispatch")) rctx+      null substs `shouldBe` False+    -- ⟦λ ⤍ F⟧.a.b.c : 'dispatch' peels .c then .b (their heads are dispatches,+    -- not λ-formations, so 'λ ∉ 𝐵' holds), then 'lambda' handles the base+    -- ⟦λ ⤍ F⟧.a and fires the atom. The chain therefore routes+    -- dispatch → dispatch → lambda; firing the undefined atom 'F' is what+    -- raises the error, proving the base λ-formation reached 'lambda'.+    it "drills a chained λ-formation dispatch down to the base 'lambda'" $ do+      let base = ExFormation [BiLambda (Function "F")]+          chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c")+      morph (chain, (Program ExRoot, Nothing) :| []) ExRoot (defaultDataizeContext ExRoot)+        `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException))+   describe "dataize" $     test       dataize'-      [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, Just (BtOne "00"))-      , ("T => X", ExTermination, ExRoot, Nothing)+      [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, BtOne "00")+      , ("T => --", ExTermination, ExRoot, BtEmpty)+      , ("[[ ]] => --", ExFormation [], ExRoot, BtEmpty)       ,         ( "[[ @ -> [[ D> 00-]] ]] => 00-"         , ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "00"), BiVoid AtRho]), BiVoid AtRho]         , ExRoot-        , Just (BtOne "00")+        , BtOne "00"         )       ,         ( "[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]] => 01-"@@ -99,27 +131,23 @@                 )             ]         , ExRoot-        , Just (BtOne "01")+        , BtOne "01"         )       ] -  describe "execBuildTerm" $-    it "returns the universe Q body for global()" $ do-      prog <- parseProgramThrows "Q -> [[ x -> [[ D> 42- ]] ]]"-      expected <- parseExpressionThrows "[[ x -> [[ D> 42- ]] ]]"-      term <- execBuildTerm (defaultDataizeContext ExRoot prog) "global" [] substEmpty-      case term of-        TeExpression actual -> actual `shouldBe` expected-        _ -> expectationFailure "global() did not return an expression"-   describe "labels every step with a defined rule or operation" $ do-    let funcs = maybe [] (map Yaml.function)+    let verb op = case op of+          Yaml.OpMorph _ -> "morph"+          Yaml.OpNormalize _ -> "normalize"+          Yaml.OpLambda _ -> "lambda"+          Yaml.OpContextualize _ _ -> "contextualize"+          Yaml.OpDataize _ -> "dataize"         allowed =           map (.name) Yaml.morphingRules             ++ map (.name) Yaml.dataizationRules             ++ map (.name) Yaml.normalizationRules-            ++ concatMap (funcs . (.where_)) Yaml.morphingRules-            ++ concatMap (funcs . (.where_)) Yaml.dataizationRules+            ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.morphingRules+            ++ concatMap (map (verb . (.operation)) . (.premises)) Yaml.dataizationRules     it "uses no step label without a defining rule or operation" $ do       prog <-         parseProgramThrows@@ -132,7 +160,7 @@               ]           )       loc <- parseExpressionThrows "Q"-      (_, chain) <- dataize (defaultDataizeContext loc prog)+      (_, chain) <- dataize prog (defaultDataizeContext loc)       let orphans = nub [label | (_, Just label) <- chain, label `notElem` allowed]       unless         (null orphans)@@ -151,7 +179,7 @@     let labelsOf loc src = do           prog <- parseProgramThrows src           loc' <- parseExpressionThrows loc-          (_, chain) <- dataize (defaultDataizeContext loc' prog)+          (_, chain) <- dataize prog (defaultDataizeContext loc')           pure [label | (_, Just label) <- chain]     it "dataizes 5.plus(6) through the expected rules" $ do       labels <-

@@ -1,3 +1,5 @@+{-# LANGUAGE OverloadedStrings #-}+ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT @@ -6,13 +8,15 @@ -} module LaTeXSpec where +import AST (Expression (ExMeta)) import Control.Monad (forM_)-import LaTeX (meetInProgram)+import LaTeX (conditionToLatex, meetInProgram) import Parser (parseExpressionThrows, parseProgramThrows) import Test.Hspec (Spec, describe, it, shouldBe)+import Yaml qualified as Y  spec :: Spec-spec =+spec = do   describe "meet program in program" $     forM_       [ ("Q.x.y", "{Q.x.y}", "{[[ x -> Q.x.y ]]}", ["Q.x.y"])@@ -28,3 +32,10 @@           res <- traverse parseExpressionThrows exprs           meetInProgram ptn 4 tgt `shouldBe` res       )++  describe "renders the 'formation' condition" $+    forM_+      [ ("formation", Y.IsFormation (ExMeta "n"), "{ \\phinoIsFormation{ n } }")+      , ("not formation", Y.Not (Y.IsFormation (ExMeta "n")), "{ \\phinoNotFormation{ n } }")+      ]+      (\(desc, cond, expected) -> it desc (conditionToLatex (Just cond) `shouldBe` expected))