phino 0.0.104 → 0.0.105

raw patch · 14 files changed

+161/−86 lines, 14 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• phino.cabal +1/−1
• resources/dataization.yaml +6/−8
• resources/morphing.yaml +11/−12
• src/AST.hs +8/−0
• src/CLI/Parsers.hs +1/−1
• src/CST.hs +10/−0
• src/Canonizer.hs +5/−5
• src/Dataize.hs +20/−12
• src/LaTeX.hs +38/−22
• src/Render.hs +1/−0
• test/CLISpec.hs +28/−10
• test/DataizeSpec.hs +2/−1
• test/LaTeXSpec.hs +19/−2
• test/YamlSpec.hs +11/−12

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

@@ -15,11 +15,11 @@ # to one judgment — 𝔻 ('dataize'), 𝕄 ('morph'), 𝒩 ('normalize'), 𝔼 ('evaluate') # or 𝒞 ('contextualize'). 'e-match' is the universe-argument matcher of # 𝔻(n, e); it is always the e meta. The single bytes result is named δ. A-# normal-form-valued result (𝕄 'morph', 𝒩 'normalize') is named 𝑛, 𝑛1, … in-# premise order, skipping the bare 𝑛 only when 'match' already binds it; an-# expression-valued result (𝒞 'contextualize', 𝔼 'evaluate') is not a normal-# form — that is why a 'normalize' premise follows it — so it takes an 𝑒-family-# name (𝑒1, 𝑒2, …, the next index free of 'match', 𝑒 itself being the universe)+# normal-form-valued result (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate') is named+# 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match' already binds+# it; an expression-valued result (𝒞 'contextualize') is not a normal form —+# that is why a 'normalize' premise follows it — so it takes an 𝑒-family name+# (𝑒1, 𝑒2, …, the next index free of 'match', 𝑒 itself being the universe) # rather than an 𝑛 name reserved for normal forms. # # The clauses are disjoint, so their relative order does not change behavior.@@ -61,12 +61,10 @@   e-match: 𝑒   d-result: δ   premises:-    - n-result: 𝑒1+    - n-result: 𝑛1       evaluate:         - ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧         - 𝑒-    - n-result: 𝑛1-      normalize: 𝑒1     - d-result: δ       dataize: 𝑛1 

@@ -19,12 +19,11 @@ # ordered 'premises' reduce as stated. A premise binds 'n-result' to the result # of one judgment — 𝕄 ('morph'), 𝒩 ('normalize') or 𝔼 ('evaluate'). 'e-match' is # the universe-argument matcher of 𝕄(n, e); usually the e meta, but a rule may-# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). A normal-form-valued-# result (𝕄 'morph', 𝒩 'normalize') is named 𝑛, 𝑛1, … in premise order, the bare-# 𝑛 skipped only when 'match' already binds it; an expression-valued result (𝔼-# 'evaluate') is not a normal form — that is why a 'normalize' premise follows-# it — so it takes an 𝑒-family name (𝑒1, 𝑒2, …, the next index free of 'match',-# 𝑒 itself being the universe) rather than an 𝑛 name reserved for normal forms.+# pin it to a literal (e.g. 'mg' fires only on 𝕄(Φ, Φ)). Every judgment here is+# normal-form-valued (𝕄 'morph', 𝒩 'normalize', 𝔼 'evaluate' — 𝔼 normalizes its+# atom's result internally), so results are named 𝑛, 𝑛1, … in premise order, the+# bare 𝑛 skipped only when 'match' already binds it; the 𝑒-family stays reserved+# for the universe 𝑒 itself. # # 'ml' and 'md' are kept mutually exclusive: 'md' fires only # when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation@@ -55,19 +54,19 @@   label: \lambda   match: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧.𝜏'   e-match: 𝑒-  n-result: 𝑛2+  n-result: 𝑛3   premises:-    - n-result: 𝑒1+    - n-result: 𝑛1       evaluate:         - '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'         - 𝑒-    - n-result: 𝑛1-      normalize: '𝑒1.𝜏'     - n-result: 𝑛2-      morph: 𝑛1+      normalize: '𝑛1.𝜏'+    - n-result: 𝑛3+      morph: 𝑛2  - name: mphi-  label: \phi+  label: \varphi   match: ⟦𝐵⟧.𝜏   e-match: 𝑒   n-result: 𝑛1

@@ -26,6 +26,13 @@   | ExMeta Text   | ExPhiMeet (Maybe String) Int Expression   | ExPhiAgain (Maybe String) Int Expression+  | {- | Bare data 𝛿 — the raw bytes extracted by the 'delta' dataization rule.+    It is not a phi-calculus term but a rendering-only chain node, so a+    '--sequence' derivation can terminate at the data itself rather than at+    the data object it was pulled out of (see #980). It never flows into the+    matcher, builder or the dataization relation.+    -}+    ExBytes Bytes   deriving (Eq, Ord, Show, Generic)  data Argument@@ -110,6 +117,7 @@       ExMeta t -> hashText (step h 7) t       ExPhiMeet ms i ex -> goExpr (hashMaybeString (step (step h 9) i) ms) ex       ExPhiAgain ms i ex -> goExpr (hashMaybeString (step (step h 10) i) ms) ex+      ExBytes bts -> goBytes (step h 8) bts     goBinding :: Int -> Binding -> Int     goBinding h = \case       BiTau at ex -> goExpr (goAttribute (step h 11) at) ex

@@ -122,7 +122,7 @@ optSequence = switch (long "sequence" <> help "Result output contains all intermediate 𝜑-expressions concatenated with EOL")  optCanonize :: Parser Bool-optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with F1, F2, etc.")+optCanonize = switch (long "canonize" <> help "Rename all functions attached to λ binding with Fn1, Fn2, etc.")  optExpression :: Parser (Maybe String) optExpression = optional (strOption (long "expression" <> metavar "NAME" <> help "Name for 'phiExpression' element when rendering to LaTeX (see --output option)"))

@@ -177,6 +177,7 @@   | EX_META {meta :: META}   | EX_PHI_MEET {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}   | EX_PHI_AGAIN {prefix :: Maybe String, idx :: Int, expr :: EXPRESSION}+  | EX_BYTES {bytes :: BYTES} -- bare data 𝛿, a rendering-only terminal chain node (see #980)   deriving (Eq, Show)  data ATTRIBUTE@@ -251,6 +252,14 @@ expressionToCST :: Expression -> EXPRESSION expressionToCST = toCST' +-- Like 'expressionToCST', but lays the expression out from a given base tab+-- instead of column 0. Used when an expression sits on an already-indented+-- line (e.g. a '\leadsto' continuation step in the LaTeX --sequence output),+-- so its wrapped member lines nest one level below that line and its closing+-- bracket aligns with the opening one.+expressionToCSTFrom :: Int -> Expression -> EXPRESSION+expressionToCSTFrom tabs expr = toCST expr (tabs, EOL)+ -- A number can be rendered with the sweet numeric literal only when it is -- finite. NaN and the infinities have no such literal — and the bare `show` -- tokens (`NaN`, `Infinity`, `-Infinity`) would collide with object/function@@ -310,6 +319,7 @@   toCST ExXi _ = EX_XI XI   toCST (ExMeta mt) _ = EX_META (META NO_EXCL (exMetaHead mt) (metaTail mt))   toCST ExTermination _ = EX_TERMINATION DEAD+  toCST (ExBytes bts) ctx = EX_BYTES (toCST bts ctx)   toCST (ExPhiMeet prefix idx expr) ctx = EX_PHI_MEET prefix idx (toCST expr ctx)   toCST (ExPhiAgain prefix idx expr) ctx = EX_PHI_AGAIN prefix idx (toCST expr ctx)   toCST (ExFormation [BiVoid AtRho]) ctx = toCST (ExFormation []) ctx

@@ -1,9 +1,9 @@ -- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com -- SPDX-License-Identifier: MIT --- Canonization is the process of replacing function names attrached to--- lambda bindings with numbered identifiers started from 'F'--- like 'F1', 'F2', etc.+-- Canonization is the process of replacing function names attached to+-- lambda bindings with numbered identifiers prefixed with 'Fn'+-- like 'Fn1', 'Fn2', etc. module Canonizer (canonize, canonizeExpr) where  import AST@@ -14,7 +14,7 @@ canonizeBindings [] idx = ([], idx) canonizeBindings ((BiLambda (Function _)) : rest) idx =   let (bds', idx') = canonizeBindings rest (idx + 1)-   in (BiLambda (Function (T.pack ('F' : show idx))) : bds', idx')+   in (BiLambda (Function (T.pack ("Fn" <> show idx))) : bds', idx') canonizeBindings (BiTau attr expr : rest) idx =   let (expr', idx') = canonizeExpression expr idx       (bds', idx'') = canonizeBindings rest idx'@@ -50,7 +50,7 @@   let (expr', idx') = canonizeExpression expr idx    in (ArAlpha alpha expr', idx') --- Canonize a single expression, restarting the 'F' counter from 1 so the+-- Canonize a single expression, restarting the 'Fn' counter from 1 so the -- numbering is local to that expression. canonizeExpr :: Expression -> Expression canonizeExpr expr = fst (canonizeExpression expr 1)

@@ -208,11 +208,12 @@       Nothing -> do         (final, state') <- sides rule.premises subst         bts <- buildBytesThrows rule.dresult final-        pure ((bts, NE.toList seq), state')+        seq' <- leadsTo seq rule.name (ExBytes bts) ctx+        pure ((bts, NE.toList seq'), state')       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.+        -- 𝔻(𝒩(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.         Just normal@(Y.Premise _ (Y.OpNormalize inner)) -> do           let side = rule.premises `excluding` [concl, normal]           (final, state') <- sides side subst@@ -227,9 +228,12 @@           built <- buildExpressionThrows inner final           ((morphed', seq'), state'') <- morph (built, seq) univ state' ctx           dataize' (morphed', seq') univ state'' ctx-        -- 𝔻(⊥) (the 'none' rule) hands a literal term straight to 𝔻 with no-        -- producing side-computation, so the transition to that term is labelled-        -- by the conclusion's own verb ('dataize') rather than a side premise.+        -- The dataize argument is produced with no 'normalize'/'morph' spine to+        -- splice: 'fire' by its 'evaluate' side-computation (𝔼 now yields a+        -- normal form itself, so no follow-up 'normalize' is needed) and 'none'+        -- by handing the literal ⊥ straight to 𝔻. The transition is labelled by+        -- the side-computation ('evaluate') when there is one, else by the+        -- conclusion's own verb ('dataize' for 𝔻(⊥)).         _ -> do           let side = rule.premises `excluding` [concl]           (final, state') <- sides side subst@@ -401,10 +405,12 @@ execBuildTerm _ ctx func = _buildTerm ctx func  -- 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.+-- against the global universe 'e', under the incoming state 𝑠, normalizes the+-- atom's raw result 𝒩(e₁) = n, and returns that normal form together with the+-- new state. Normalizing here makes 𝔼's codomain 𝓝 (as its type demands), so+-- callers ('fire', 'ml') need no follow-up 'normalize' premise. The universe is+-- 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@@ -413,7 +419,9 @@     ExFormation bds -> do       resolved <- formation bds univ state ctx       case resolved of-        Just (obj, state') -> pure (TeExpression obj, state')+        Just (obj, state') -> do+          (normal, _) <- normalized obj ((univ, Nothing) :| []) ctx+          pure (TeExpression normal, 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 2 expression arguments")

@@ -153,17 +153,27 @@     , maybe "" (printf "\\phiExpression{%s} ") _expression     ] -body :: [(a, Maybe String)] -> (a -> String) -> String+-- Join the rendered steps with '\leadsto'. Every step after the first carries+-- the two-space '\leadsto' indent, so it is rendered from base tab 1 rather+-- than 0 (via 'baseTab'); this keeps a wrapped multi-line step's members nested+-- one level below its '\leadsto [[' line and its closing bracket aligned with+-- that line. The first step has no '\leadsto' prefix and stays at base tab 0.+body :: [(a, Maybe String)] -> (Int -> a -> String) -> String body printed toLatex =   intercalate     "\n  \\leadsto "-    ( map-        ( \(item, maybeName) ->-            let item' = toLatex item+    ( zipWith+        ( \idx (item, maybeName) ->+            let item' = toLatex (baseTab idx) item              in maybe item' (printf "%s \\leadsto_{\\nameref{r:%s}}" item') maybeName         )+        [0 ..]         printed     )+  where+    baseTab :: Int -> Int+    baseTab 0 = 0+    baseTab _ = 1  ending :: Bool -> LatexContext -> String ending True ctx = printf " \\leadsto\n  \\leadsto \\dots\n\\end{%s}" (phiquation ctx)@@ -202,7 +212,7 @@   pure     ( concat         [ preamble ctx-        , body (canonizedRewrittens (compressedRewrittens rewrittens ctx) ctx) (\expr -> renderToLatex (expressionToCST expr) ctx)+        , body (canonizedRewrittens (compressedRewrittens rewrittens ctx) ctx) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)         , ending exceeded ctx         ]     )@@ -212,7 +222,7 @@   pure     ( concat         [ preamble ctx-        , body (zip (canonizedExpressions (compressedExpressions focused ctx) ctx) rules) (\expr -> renderToLatex (expressionToCST expr) ctx)+        , body (zip (canonizedExpressions (compressedExpressions focused ctx) ctx) rules) (\tabs expr -> renderToLatex (expressionToCSTFrom tabs expr) ctx)         , ending exceeded ctx         ]     )@@ -240,6 +250,7 @@   toLaTeX EX_PHI_AGAIN{..} = EX_PHI_AGAIN prefix idx (toLaTeX expr)   toLaTeX EX_META{..} = EX_META (toLaTeX meta)   toLaTeX EX_XI{} = EX_XI XI'+  toLaTeX EX_BYTES{..} = EX_BYTES (toLaTeX bytes)   toLaTeX expr = expr  instance ToLaTeX ATTRIBUTE where@@ -392,7 +403,7 @@     premises     (phinoMorph (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderExpr rule.nresult))   where-    (premises, final) = premisesToLatex rule.premises+    (premises, final) = premisesToLatex (renderExpr rule.ematch) rule.premises  -- 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@@ -407,7 +418,7 @@     premises     (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (conclusionStateName final 1) (conclusionStateName final final) (renderBytes rule.dresult))   where-    (premises, final) = premisesToLatex rule.premises+    (premises, final) = premisesToLatex (renderExpr rule.ematch) rule.premises  -- Render a contextualization rule as a LaTeX inference rule, with 𝒞(match, c) ⟿ -- c-result as the conclusion below the line. 𝒞 carries no state, so its premises@@ -419,7 +430,7 @@     rule.name     rule.label     Nothing-    (fst (premisesToLatex rule.premises))+    (fst (premisesToLatex "e" rule.premises))     (phinoContextualize (renderExpr rule.match) (renderExpr rule.cmatch) (renderExpr rule.cresult))  -- The state metavariable for index 'n', rendered as s_1, s_2, … to mirror the@@ -440,27 +451,32 @@ -- 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+-- the state through the premises ('sidePremise' in 'Dataize.hs'). The 'universe'+-- is the rule's own e-match, threaded into 𝕄/𝔻 premises (bound by the conclusion)+-- rather than a free 'e'. Returns the rendered judgments and the final state+-- index, which the conclusion returns.+premisesToLatex :: String -> [Y.Premise] -> ([String], Int)+premisesToLatex universe = go 1   where+    go :: Int -> [Y.Premise] -> ([String], Int)     go index [] = ([], index)     go index (premise : rest) = (rendered : more, final)       where-        (rendered, next) = premiseToLatex index premise+        (rendered, next) = premiseToLatex universe 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)+-- state-changing operations 𝕄 ('morph'), 𝔻 ('dataize') and 𝔼 ('evaluate') consume+-- s_index and yield s_index+1 (so they return the bumped index); the rest are+-- stateless and leave the index as is. 𝕄 and 𝔻 carry the rule's own 'universe'+-- (its e-match) so the premise stays bound by the conclusion instead of naming a+-- free 'e'; 𝔼 carries the explicit universe from its own operation.+premiseToLatex :: String -> Int -> Y.Premise -> (String, Int)+premiseToLatex universe index premise = case premise.operation of+  Y.OpMorph arg -> (phinoMorph (renderExpr arg) universe (stateName index) (stateName (index + 1)) (renderExpr (ExMeta premise.result)), index + 1)+  Y.OpDataize arg -> (phinoDataize (renderExpr arg) universe (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.OpEvaluate arg evalUniverse -> (phinoEvaluate (renderExpr arg) (renderExpr evalUniverse) (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

@@ -207,6 +207,7 @@   render EX_META{..} = render meta   render EX_PHI_MEET{..} = "\\phinoMeet{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}{ " <> render expr <> " }"   render EX_PHI_AGAIN{..} = "\\phinoAgain{" <> maybe "" (\p -> T.pack p <> ":") prefix <> render idx <> "}"+  render EX_BYTES{..} = render bytes  instance Render [ATTRIBUTE] where   render attrs = T.intercalate ", " (map render attrs)

@@ -842,7 +842,7 @@       withStdin "[[ x -> [[ y -> [[ L> Func ]].q, z -> Q.x(a -> [[ w -> [[ L> Atom ]], L> Hello ]]) ]], L> Package ]]" $         testCLISucceeded           ["rewrite", "--canonize", "--sweet", "--flat"]-          ["⟦ x ↦ ⟦ y ↦ ⟦ λ ⤍ F1 ⟧.q, z ↦ Φ.x( a ↦ ⟦ w ↦ ⟦ λ ⤍ F2 ⟧, λ ⤍ F3 ⟧ ) ⟧, λ ⤍ F4 ⟧"]+          ["⟦ x ↦ ⟦ y ↦ ⟦ λ ⤍ Fn1 ⟧.q, z ↦ Φ.x( a ↦ ⟦ w ↦ ⟦ λ ⤍ Fn2 ⟧, λ ⤍ Fn3 ⟧ ) ⟧, λ ⤍ Fn4 ⟧"]      it "rewrites by locator" $       withStdin "[[ ex -> [[ x -> [[ y -> 5 ]].y ]], abc -> [[ x -> ? ]](x -> 5) ]]" $@@ -882,12 +882,31 @@               , "  \\leadsto [[ |x| -> [[ D> |01-|, |y| -> ? ]] ( |y| -> [[]] ) ]] . |x| \\leadsto_{\\nameref{r:copy}}"               , "  \\leadsto [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] . |x| \\leadsto_{\\nameref{r:dot}}"               , "  \\leadsto [[ D> |01-|, |y| -> [[]] ]] ( \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ) \\leadsto_{\\nameref{r:copy}}"-              , "  \\leadsto [[ D> |01-|, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ]]{.}"+              , "  \\leadsto [[ D> |01-|, |y| -> [[]], \\phiTerminal{\\rho} -> [[ |x| -> [[ D> |01-|, |y| -> [[]] ]] ]] ]] \\leadsto_{\\nameref{r:delta}}"+              , "  \\leadsto |01-|{.}"               , "\\end{phiquation}"               , "01-"               ]           ] +    it "keeps the delta step in --sequence under --quiet" $+      withStdin "[[ D> 01- ]]" $+        testCLISucceeded+          ["dataize", "--sequence", "--quiet", "--output=latex", "--flat", "--sweet"]+          [ intercalate+              "\n"+              [ "[[ D> |01-| ]] \\leadsto_{\\nameref{r:delta}}"+              , "  \\leadsto |01-|{.}"+              , "\\end{phiquation}"+              ]+          ]++    it "ends the phi --sequence at the bare data" $+      withStdin "[[ D> 01- ]]" $+        testCLISucceeded+          ["dataize", "--sequence", "--quiet", "--flat", "--sweet"]+          ["⟦ Δ ⤍ 01- ⟧\n01-"]+     it "focuses a compressed sequence whose meet replaces a step root" $       withStdin "[[ @ -> [[ @ -> $.c.plus( 32.0 ), c -> 25.0 ]], bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus -> [[ x -> ?, L> L_number_plus ]] ]] ]]" $         testCLISucceeded@@ -1063,14 +1082,14 @@             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{ml}"             , "  \\phinoLabel{\\lambda}"-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ e_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ e_1 . \\tau }{ n_1 } }"-            , "  \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ s_2 }{ n_2 }{ s_3 } }"-            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_2 }{ s_3 } }"+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ s_2 }{ n_3 }{ s_3 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ s_1 }{ n_3 }{ s_3 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{mphi}"-            , "  \\phinoLabel{\\phi}"+            , "  \\phinoLabel{\\varphi}"             , "  \\phinoCondition{ @ \\in B \\;\\text{and}\\; \\tau \\notin B \\;\\text{and}\\; L \\notin B }"             , "  \\phinoPremise{ \\phinoNormalize{ [[ B ]] . @ . \\tau }{ n } }"             , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"@@ -1129,7 +1148,7 @@             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"             , "  \\phinoName{mg}"-            , "  \\phinoPremise{ \\phinoMorph{ T }{ e }{ s_1 }{ n }{ s_2 } }"+            , "  \\phinoPremise{ \\phinoMorph{ T }{ Q }{ s_1 }{ n }{ s_2 } }"             , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ s_1 }{ n }{ s_2 } }"             , "\\end{phinoMorphingInference}"             ]@@ -1154,8 +1173,7 @@             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{fire}"-            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ e_1 }{ s_2 } }"-            , "  \\phinoPremise{ \\phinoNormalize{ e_1 }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ n_1 }{ s_2 } }"             , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ s_2 }{ \\delta }{ s_3 } }"             , "  \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ s_1 }{ \\delta }{ s_3 } }"             , "\\end{phinoDataizationInference}"

@@ -281,10 +281,11 @@                    , "contextualize"                    , "dot"                    , "copy"+                   , "delta"                    ]     it "dataizes a located reference through the expected rules" $ do       labels <- labelsOf "Q.foo.bar" "[[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]"-      labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf"]+      labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf", "delta"]     -- The 'none' rule dataizes ⊥ (𝔻(⟦⟧) → 𝔻(⊥)), which matches no clause now     -- that there is no 'end' rule, so an empty formation reduces through one     -- labelled 'dataize' step and then fails: it has nothing to dataize (#955).

@@ -10,10 +10,12 @@  import AST (Expression (ExMeta)) import Control.Monad (forM_)+import Data.List (intercalate) import Data.Text qualified as T-import LaTeX (LatexContext (..), conditionToLatex, defaultLatexContext, meetInExpression, meetInExpressions)+import LaTeX (LatexContext (..), conditionToLatex, defaultLatexContext, meetInExpression, meetInExpressions, rewrittensToLatex)+import Lining (LineFormat (MULTILINE)) import Parser (parseExpressionThrows)-import Test.Hspec (Spec, describe, expectationFailure, it, shouldBe)+import Test.Hspec (Spec, describe, expectationFailure, it, shouldBe, shouldContain) import Yaml qualified as Y  spec :: Spec@@ -48,6 +50,21 @@       case meetInExpressions exprs ctx of         (firstStep : _) -> T.count "ExPhiMeet" (T.pack (show firstStep)) `shouldBe` 2         [] -> expectationFailure "meetInExpressions returned no expressions"++  describe "indents wrapped continuation steps in a --sequence (#981)" $+    it "nests a wrapped step's members below its two-space \\leadsto line and aligns the closing bracket with it, rather than laying the step out from column 0" $ do+      start <- parseExpressionThrows "[[ x -> Q.y ]]"+      wrapped <- parseExpressionThrows "[[ a -> Q.b, c -> Q.d ]]"+      let ctx = defaultLatexContext{_line = MULTILINE, _margin = 20}+      latex <- rewrittensToLatex ([(start, Just "first"), (wrapped, Just "second")], False) ctx+      latex+        `shouldContain` intercalate+          "\n"+          [ "  \\leadsto [["+          , "    |a| -> Q . |b|,"+          , "    |c| -> Q . |d|"+          , "  ]] \\leadsto_{\\nameref{r:second}}"+          ]    describe "renders the 'formation' condition" $     forM_

@@ -75,23 +75,22 @@       (labels \\ nub labels) `shouldBe` []    describe "reserves 𝑛-family metas for normal forms" $-    -- 𝒞 ('contextualize') and 𝔼 ('evaluate') return an expression that is not-    -- necessarily a normal form — that is why a 'normalize' premise follows-    -- them — so binding their result to an 𝑛-reserved meta (internal prefix-    -- "n") in a morphing or dataization rule conflates the calculus's 'e'-    -- (expression) with 'n' (normal form). Such a slip is notational, not-    -- functional (the meta name is only a substitution-map key), so it is easy-    -- to miss by eye; flag it automatically instead. Contextualization is-    -- excluded on purpose: its 𝒞-valued results are the point and its header-    -- reserves nothing (see #971).-    it "no contextualize/evaluate premise in a morphing or dataization rule binds an 𝑛-reserved meta" $ do+    -- 𝒞 ('contextualize') returns an expression that is not necessarily a normal+    -- form — that is why a 'normalize' premise follows it — so binding its result+    -- to an 𝑛-reserved meta (internal prefix "n") in a morphing or dataization+    -- rule conflates the calculus's 'e' (expression) with 'n' (normal form). Such+    -- a slip is notational, not functional (the meta name is only a+    -- substitution-map key), so it is easy to miss by eye; flag it automatically+    -- instead. 𝔼 ('evaluate') is excluded on purpose (partially reverting #971):+    -- it normalizes its atom's result internally, so its codomain is 𝓝 and an+    -- 𝑛-family result is exactly right (see #990). Contextualization keeps being+    -- flagged: its 𝒞-valued results are non-normal (see #971).+    it "no contextualize premise in a morphing or dataization rule binds an 𝑛-reserved meta" $ do       let expressionValued :: Operation -> Bool           expressionValued OpContextualize{} = True-          expressionValued OpEvaluate{} = True           expressionValued _ = False           verbOf :: Operation -> String           verbOf OpContextualize{} = "contextualize"-          verbOf OpEvaluate{} = "evaluate"           verbOf _ = "?"           premisesOf :: [(String, [Premise])]           premisesOf =