phino 0.0.86 → 0.0.87

raw patch · 20 files changed

+345/−91 lines, 20 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +20/−4
• phino.cabal +1/−1
• resources/contextualization.yaml +82/−0
• resources/dataization.yaml +23/−8
• resources/morphing.yaml +8/−12
• src/CLI/Parsers.hs +4/−0
• src/CLI/Runners.hs +5/−4
• src/CLI/Types.hs +1/−0
• src/CST.hs +1/−1
• src/Dataize.hs +15/−14
• src/Functions.hs +1/−1
• src/LaTeX.hs +16/−1
• src/Parser.hs +1/−1
• src/Render.hs +9/−9
• src/Yaml.hs +53/−10
• test/CLISpec.hs +55/−16
• test/DataizeSpec.hs +25/−3
• test/ParserSpec.hs +2/−2
• test/PrinterSpec.hs +2/−2
• test/YamlSpec.hs +21/−2

@@ -206,9 +206,9 @@ ## Explain  You can _explain_ the built-in rules by printing them in [LaTeX][latex]-format. Pass exactly one of `--normalize`, `--morph` or `--dataize` for-the rewriting, morphing (𝕄) or dataization (𝔻) rules (or `--rule` for a-custom rule file):+format. Pass exactly one of `--normalize`, `--morph`, `--dataize` or+`--contextualize` for the rewriting, morphing (𝕄), dataization (𝔻) or+contextualization (𝒞) rules (or `--rule` for a custom rule file):  ```bash $ phino explain --normalize@@ -268,6 +268,22 @@ \end{tabular} ``` +```bash+$ phino explain --contextualize+\begin{phinoInference}+  \phinoName{cxi}+  \phinoLabel{xi}+  \phinoConclusion{ \phinoContextualize{ \phiTerminal{\xi} }{ k }{ k } }+\end{phinoInference}+...+\begin{phinoInference}+  \phinoName{cdispatch}+  \phinoLabel{disp}+  \phinoPremise{ \phinoContextualize{ n }{ k }{ n_1 } }+  \phinoConclusion{ \phinoContextualize{ n . \tau }{ k }{ n_1 . \tau } }+\end{phinoInference}+```+ For more details, use `phino [COMMAND] --help` option.  ## Rule structure@@ -393,7 +409,7 @@                 or `nf:` guard is needed * `!B` || `𝐵` - list of bindings * `!d` || `δ` - bytes in meta delta binding-* `!F` || `𝐹` - function name in meta lambda binding+* `!F` || `𝑓` - function name in meta lambda binding  Every meta variable may also be used with an integer index, like `!B1` or `𝜏0`. 

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

@@ -0,0 +1,82 @@+# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com+# SPDX-License-Identifier: MIT+---+# Contextualization 𝒞 — applied top-to-bottom, first matching clause wins. It is+# binary, 𝒞(n, c): n is the term being contextualized and c is the context (the+# expression that every free ξ inside n stands for). 𝒞 walks the term+# structurally, replacing each ξ with the context c, descending through+# dispatches and applications and stopping at formations — which introduce their+# own scope and are returned untouched — and at the global Φ and termination ⊥.+#+# Each rule is an inference rule: when 'match' matches the term and 'c-match'+# matches the context (binding the meta c), the rule yields the conclusion+# 'c-result' (a premise meta or a literal), provided the ordered 'premises'+# reduce as stated. A premise binds its 'n-result' to one 𝒞 ('contextualize')+# judgment. 'c-match' is the context-argument matcher of 𝒞(n, c); it is always+# the c meta. Derived terms are named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is+# skipped only when 'match' already binds it.++- name: cglobe+  label: globe+  match: Φ+  c-match: 𝑘+  c-result: Φ++- name: cxi+  label: xi+  match: ξ+  c-match: 𝑘+  c-result: 𝑘++- name: cdead+  label: dead+  match: ⊥+  c-match: 𝑘+  c-result: ⊥++- name: cprim+  label: prim+  match: ⟦𝐵⟧+  c-match: 𝑘+  c-result: ⟦𝐵⟧++- name: cdispatch+  label: disp+  match: '𝑛.𝜏'+  c-match: 𝑘+  c-result: '𝑛1.𝜏'+  premises:+    - n-result: 𝑛1+      contextualize:+        - 𝑛+        - 𝑘++- name: capplication+  label: app+  match: '𝑛(𝜏 ↦ 𝑒1)'+  c-match: 𝑘+  c-result: '𝑛1(𝜏 ↦ 𝑛2)'+  premises:+    - n-result: 𝑛1+      contextualize:+        - 𝑛+        - 𝑘+    - n-result: 𝑛2+      contextualize:+        - 𝑒1+        - 𝑘++- name: capplicationa+  label: appa+  match: '𝑛(α𝑖 ↦ 𝑒1)'+  c-match: 𝑘+  c-result: '𝑛1(α𝑖 ↦ 𝑛2)'+  premises:+    - n-result: 𝑛1+      contextualize:+        - 𝑛+        - 𝑘+    - n-result: 𝑛2+      contextualize:+        - 𝑒1+        - 𝑘

@@ -10,11 +10,19 @@ # 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')+# 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 δ; derived # terms are 𝑛, 𝑛1, … in premise order, skipping the bare 𝑛 only when 'match' # already binds it.+#+# The clauses are disjoint, so their relative order does not change behavior.+# 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is+# guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',+# carving out 'delta', 'box', 'fire' and 'none') nor the termination ⊥+# ('not (𝑛 = ⊥)', carving out 'bott'). Without the guard 'norm' would behave+# correctly only by being declared last; with it the clauses no longer rely on+# their order.  - name: delta   label: \Delta@@ -23,7 +31,6 @@   d-result: δ  - name: box-  label: box   match: ⟦𝐵1, φ ↦ 𝑒1, 𝐵2⟧   e-match: 𝑒   d-result: δ@@ -42,35 +49,43 @@       dataize: 𝑛1  - name: fire-  label: fire-  match: ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧+  match: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧   e-match: 𝑒   d-result: δ   premises:     - n-result: 𝑛-      lambda: ⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧+      evaluate: ⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧     - n-result: 𝑛1       normalize: 𝑛     - d-result: δ       dataize: 𝑛1  - name: none-  label: none   match: ⟦𝐵⟧   e-match: 𝑒   d-result: '--'+  when:+    disjoint:+      - [Δ, λ, φ]+      - [𝐵]  - name: bott-  label: bott   match: ⊥   e-match: 𝑒   d-result: '--'  - name: norm-  label: norm   match: 𝑛   e-match: 𝑒   d-result: δ+  when:+    and:+      - not:+          formation: 𝑛+      - not:+          eq:+            - 𝑛+            - ⊥   premises:     - n-result: 𝑛1       morph: 𝑛

@@ -15,10 +15,11 @@ # 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.+# 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. 'globe' fires only on 𝕄(Φ, Φ)). 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@@ -26,19 +27,18 @@ # are disjoint and their relative order does not change behavior.  - name: prim-  label: prim   match: ⟦𝐵⟧   e-match: 𝑒   n-result: ⟦𝐵⟧  - name: lambda   label: \lambda-  match: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧.𝜏'+  match: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧.𝜏'   e-match: 𝑒   n-result: 𝑛2   premises:     - n-result: 𝑛-      lambda: '⟦𝐵1, λ ⤍ 𝐹, 𝐵2⟧'+      evaluate: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧'     - n-result: 𝑛1       normalize: '𝑛.𝜏'     - n-result: 𝑛2@@ -87,7 +87,6 @@       morph: 𝑛2  - name: root-  label: root   match: Φ   e-match: 𝑒   n-result: 𝑛1@@ -103,19 +102,16 @@       morph: 𝑛  - name: dead-  label: dead   match: ⊥   e-match: 𝑒   n-result: ⊥  - name: xi-  label: xi   match: ξ   e-match: 𝑒   n-result: ⊥  - name: globe-  label: globe   match: Φ-  e-match: 𝑒+  e-match: Φ   n-result: ⊥

@@ -180,6 +180,9 @@ optDataize :: Parser Bool optDataize = switch (long "dataize" <> help "Explain built-in dataization rules") +optContextualize :: Parser Bool+optContextualize = switch (long "contextualize" <> help "Explain built-in contextualization rules")+ optTarget :: Parser (Maybe FilePath) optTarget = optional (strOption (long "target" <> short 't' <> metavar "FILE" <> help "File to save output to")) @@ -234,6 +237,7 @@             <*> optNormalize             <*> optMorph             <*> optDataize+            <*> optContextualize             <*> optShuffle             <*> optTarget         )

@@ -22,7 +22,7 @@ import Encoding import qualified Filter as F import Functions (buildTerm)-import LaTeX (explainDataizeRules, explainMorphRules, explainRules)+import LaTeX (explainContextualizeRules, explainDataizeRules, explainMorphRules, explainRules) import Logger import Margin (defaultMargin) import Merge (merge)@@ -189,12 +189,13 @@     explained       | _morph = pure (explainMorphRules Y.morphingRules)       | _dataize = pure (explainDataizeRules Y.dataizationRules)+      | _contextualize = pure (explainContextualizeRules Y.contextualizationRules)       | otherwise = explainRules <$> getRules _normalize _shuffle _rules     validateOpts :: IO ()     validateOpts = do-      let selected = length (filter id [not (null _rules), _normalize, _morph, _dataize])-      when (selected == 0) (invalidCLIArguments "Either --rule, --normalize, --morph or --dataize must be specified")-      when (selected > 1) (invalidCLIArguments "Only one of --rule, --normalize, --morph or --dataize can be specified")+      let selected = length (filter id [not (null _rules), _normalize, _morph, _dataize, _contextualize])+      when (selected == 0) (invalidCLIArguments "Either --rule, --normalize, --morph, --dataize or --contextualize must be specified")+      when (selected > 1) (invalidCLIArguments "Only one of --rule, --normalize, --morph, --dataize or --contextualize can be specified")  runMerge :: OptsMerge -> IO () runMerge OptsMerge{..} = do

@@ -108,6 +108,7 @@   , _normalize :: Bool   , _morph :: Bool   , _dataize :: Bool+  , _contextualize :: Bool   , _shuffle :: Bool   , _targetFile :: Maybe FilePath   }

@@ -92,7 +92,7 @@   | B' -- B   | D -- δ   | D' -- \delta-  | F -- 𝐹+  | F -- 𝑓   | F' -- F   deriving (Eq, Show) 

@@ -72,8 +72,9 @@  -- 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+-- expression — and matches it against the rule's 'e-match' pattern (usually the+-- '𝑒' meta, which binds 'e' so the 'root' rule substitutes it, but a rule may+-- pin it to a literal such as 'globe' matching Φ). It is driven by -- the ordered rules from 'morphing.yaml': the first matching rule's premises are -- evaluated and its conclusion 'nresult' is built, always forwarding the same -- universe. The 'morph' premise that produces the conclusion is the spine: when@@ -197,7 +198,7 @@     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.+    -- 'box' by its 'contextualize', 'fire' by its 'evaluate'; with none it is blank.     labelOf :: [Y.Premise] -> String     labelOf (premise : _) = verb premise.operation     labelOf [] = ""@@ -220,9 +221,9 @@ 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'+-- Evaluate one side-computation premise — a 'morph', 'evaluate' 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+-- steps into the trace: 'morph' and 'evaluate' 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@@ -241,7 +242,7 @@ verb :: Y.Operation -> String verb (Y.OpMorph _) = "morph" verb (Y.OpNormalize _) = "normalize"-verb (Y.OpLambda _) = "lambda"+verb (Y.OpEvaluate _) = "evaluate" verb (Y.OpContextualize _ _) = "contextualize" verb (Y.OpDataize _) = "dataize" @@ -249,7 +250,7 @@ verbArgs :: Y.Operation -> [ExtraArgument] verbArgs (Y.OpMorph expr) = [ArgExpression expr] verbArgs (Y.OpNormalize expr) = [ArgExpression expr]-verbArgs (Y.OpLambda expr) = [ArgExpression expr]+verbArgs (Y.OpEvaluate expr) = [ArgExpression expr] verbArgs (Y.OpContextualize expr context) = [ArgExpression expr, ArgExpression context] verbArgs (Y.OpDataize expr) = [ArgExpression expr] @@ -327,25 +328,25 @@ 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 universe: 'lambda' applies an atom and+-- morphing operations that need the universe: 'evaluate' applies an atom and -- 'morph' morphs a sub-expression. Both receive the universe 'univ'. Every other -- function is delegated unchanged. execBuildTerm :: Expression -> DataizeContext -> BuildTermFunc-execBuildTerm univ ctx "lambda" = _lambda univ ctx+execBuildTerm univ ctx "evaluate" = _evaluate univ ctx execBuildTerm univ ctx "morph" = _morph univ ctx execBuildTerm _ ctx func = _buildTerm ctx func -_lambda :: Expression -> DataizeContext -> BuildTermMethod-_lambda univ ctx [ArgExpression expr] subst = do+_evaluate :: Expression -> DataizeContext -> BuildTermMethod+_evaluate univ ctx [ArgExpression expr] subst = do   form <- buildExpressionThrows expr subst   case form of     ExFormation bds -> do       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")+        Nothing -> throwIO (userError "Function evaluate() expects a formation with a λ binding")+    _ -> throwIO (userError "Function evaluate() expects a formation")+_evaluate _ _ _ _ = throwIO (userError "Function evaluate() requires exactly 1 expression argument")  -- 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

@@ -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", "morph"]+execFunctions = ["evaluate", "morph"]  buildTerm :: BuildTermFunc buildTerm func args subst = do

@@ -12,6 +12,7 @@   ( explainRules   , explainMorphRules   , explainDataizeRules+  , explainContextualizeRules   , rewrittensToLatex   , programToLaTeX   , expressionToLaTeX@@ -392,6 +393,17 @@     (map premiseToLatex rule.premises)     (phinoDataize (renderExpr rule.match) (renderExpr rule.ematch) (renderBytes rule.dresult)) +-- Render a contextualization rule as a LaTeX inference rule, with 𝒞(match, c) ⟿+-- c-result as the conclusion below the line.+explainContextualizeRule :: Y.ContextualizeRule -> String+explainContextualizeRule rule =+  inference+    rule.name+    rule.label+    Nothing+    (map premiseToLatex rule.premises)+    (phinoContextualize (renderExpr rule.match) (renderExpr rule.cmatch) (renderExpr rule.cresult))+ -- One premise judgment, rendered per its operation. 𝕄 ('morph') and 𝔻 -- ('dataize') are binary and carry the universe 'e' they were given; the rest -- are unary.@@ -400,7 +412,7 @@   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.OpEvaluate 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@@ -487,3 +499,6 @@  explainDataizeRules :: [Y.DataizeRule] -> String explainDataizeRules = intercalate "\n" . map explainDataizeRule++explainContextualizeRules :: [Y.ContextualizeRule] -> String+explainContextualizeRules = intercalate "\n" . map explainContextualizeRule

@@ -299,7 +299,7 @@         BiLambda . Function . T.pack <$> function     , do         _ <- lambda-        BiLambda . FnMeta <$> meta' 'F' "𝐹"+        BiLambda . FnMeta <$> meta' 'F' "𝑓"     ]     <?> "binding" 

@@ -71,7 +71,7 @@  instance Render DELTA where   render DELTA = "Δ"-  render DELTA' = "\\Delta"+  render DELTA' = "D"  instance Render XI where   render XI = "ξ"@@ -128,7 +128,7 @@   render B' = "B"   render D = "δ"   render D' = "\\delta"-  render F = "𝐹"+  render F = "𝑓"   render F' = "F"  instance Render META where@@ -256,26 +256,26 @@     where       renderWrapped :: CONDITION -> Text       renderWrapped CO_LOGIC{conditions = [cond]} = render cond-      renderWrapped cond@CO_LOGIC{} = "( " <> render cond <> " )"+      renderWrapped cond@CO_LOGIC{} = "\\lparen " <> render cond <> " \\rparen"       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_MATCHES{..} = "matches\\lparen " <> T.pack regex <> ", " <> render expr <> " \\rparen"+  render CO_PART_OF{..} = "part-of\\lparen " <> render expr <> ", " <> render binding <> " \\rparen"   render CO_FORMATION{..} = "\\phinoIsFormation{ " <> render expr <> " }"   render CO_DISJOINT{..} =     "[ "       <> T.intercalate ", " (map render attrs)-      <> " ] \\cap ( "+      <> " ] \\cap \\lparen "       <> T.intercalate " \\cup " (map render groups)-      <> " ) = \\emptyset"+      <> " \\rparen = \\emptyset"   render CO_EMPTY = ""  renderFunc :: Render a => Text -> a -> Text-renderFunc func renderable = func <> "( " <> render renderable <> " )"+renderFunc func renderable = func <> "\\lparen " <> render renderable <> " \\rparen"  instance Render EXTRA_ARG where   render ARG_ATTR{..} = render attr@@ -292,5 +292,5 @@   render EXTRA{..} = render meta <> " \\coloneqq " <> macro func <> "{ " <> T.intercalate ", " (map render args) <> " }"     where       macro :: String -> Text-      macro "lambda" = "\\phinoEvaluate"+      macro "evaluate" = "\\phinoEvaluate"       macro name = "\\" <> T.pack name

@@ -238,7 +238,7 @@ data Operation   = OpMorph Expression   | OpNormalize Expression-  | OpLambda Expression+  | OpEvaluate Expression   | OpContextualize Expression Expression   | OpDataize Expression   deriving (Eq, Generic, Show)@@ -272,6 +272,20 @@   }   deriving (Generic, Show) +-- One contextualization rule in inference-rule form, structured like 'MorphRule'+-- but binary in 𝒞(n, c): the second argument is the context 'c' ('cmatch',+-- always the 'c' meta) rather than the universe 'e', and the conclusion is the+-- contextualized term 'cresult'.+data ContextualizeRule = ContextualizeRule+  { name :: String+  , label :: Maybe String+  , match :: Expression+  , cmatch :: Expression+  , cresult :: Expression+  , premises :: [Premise]+  }+  deriving (Generic, Show)+ instance FromJSON Premise where   parseJSON =     withObject@@ -299,7 +313,7 @@   asum     [ OpMorph <$> o .: "morph"     , OpNormalize <$> o .: "normalize"-    , OpLambda <$> o .: "lambda"+    , OpEvaluate <$> o .: "evaluate"     , do         vals <- o .: "contextualize"         case vals of@@ -308,14 +322,25 @@     , OpDataize <$> o .: "dataize"     ] +-- Parse the optional 'label', rejecting one that merely repeats the rule's+-- 'name'. A label equal to the name typesets the same token across two macros+-- and adds nothing, so it is forbidden: 'label' is meant to carry a symbol that+-- differs from the plain name (for example '\lambda' or 'disp').+parseLabel :: String -> Object -> Parser (Maybe String)+parseLabel ruleName o = do+  label' <- o .:? "label"+  if label' == Just ruleName+    then fail $ "'label' is redundant when it equals 'name' (" ++ ruleName ++ "); drop it"+    else pure label'+ instance FromJSON MorphRule where   parseJSON =     withObject       "MorphRule"-      ( \o ->-          MorphRule-            <$> o .: "name"-            <*> o .:? "label"+      ( \o -> do+          ruleName <- o .: "name"+          MorphRule ruleName+            <$> parseLabel ruleName o             <*> o .: "match"             <*> o .: "e-match"             <*> o .: "n-result"@@ -327,10 +352,10 @@   parseJSON =     withObject       "DataizeRule"-      ( \o ->-          DataizeRule-            <$> o .: "name"-            <*> o .:? "label"+      ( \o -> do+          ruleName <- o .: "name"+          DataizeRule ruleName+            <$> parseLabel ruleName o             <*> o .: "match"             <*> o .: "e-match"             <*> o .: "d-result"@@ -338,6 +363,20 @@             <*> o .:? "premises" .!= []       ) +instance FromJSON ContextualizeRule where+  parseJSON =+    withObject+      "ContextualizeRule"+      ( \o -> do+          ruleName <- o .: "name"+          ContextualizeRule ruleName+            <$> parseLabel ruleName o+            <*> o .: "match"+            <*> o .: "c-match"+            <*> o .: "c-result"+            <*> o .:? "premises" .!= []+      )+ decodeRules :: (FromJSON a) => FilePath -> BS.ByteString -> [a] decodeRules path bs = case Yaml.decodeEither' bs of   Right rs -> rs@@ -350,3 +389,7 @@ dataizationRules :: [DataizeRule] {-# NOINLINE dataizationRules #-} dataizationRules = decodeRules "resources/dataization.yaml" $(embedFile "resources/dataization.yaml")++contextualizationRules :: [ContextualizeRule]+{-# NOINLINE contextualizationRules #-}+contextualizationRules = decodeRules "resources/contextualization.yaml" $(embedFile "resources/contextualization.yaml")

@@ -367,8 +367,8 @@     it "fails when a rewriting rule uses a dataization-only function" $       withStdin "{⟦⟧}" $         testCLIFailed-          ["rewrite", rule "lambda-in-rewrite.yaml"]-          ["Function 'lambda' in rule 'uses-lambda' is available only for dataization and morphing, not for rewriting"]+          ["rewrite", rule "evaluate-in-rewrite.yaml"]+          ["Function 'evaluate' in rule 'uses-evaluate' is available only for dataization and morphing, not for rewriting"]      it "normalizes with --normalize flag" $       testCLISucceeded@@ -1047,7 +1047,6 @@         [ unlines             [ "\\begin{phinoInference}"             , "  \\phinoName{prim}"-            , "  \\phinoLabel{prim}"             , "  \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ [[ B ]] } }"             , "\\end{phinoInference}"             , "\\begin{phinoInference}"@@ -1085,7 +1084,6 @@             , "\\end{phinoInference}"             , "\\begin{phinoInference}"             , "  \\phinoName{root}"-            , "  \\phinoLabel{root}"             , "  \\phinoCondition{ e \\not= Q }"             , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"             , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"@@ -1093,18 +1091,15 @@             , "\\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 } }"+            , "  \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ T } }"             , "\\end{phinoInference}"             ]         ]@@ -1120,8 +1115,7 @@             , "\\end{phinoInference}"             , "\\begin{phinoInference}"             , "  \\phinoName{box}"-            , "  \\phinoLabel{box}"-            , "  \\phinoCondition{ [ \\Delta, L ] \\cap ( B_1 \\cup B_2 ) = \\emptyset }"+            , "  \\phinoCondition{ [ D, L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }"             , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ n } }"             , "  \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }"             , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"@@ -1129,7 +1123,6 @@             , "\\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 } }"@@ -1137,17 +1130,16 @@             , "\\end{phinoInference}"             , "\\begin{phinoInference}"             , "  \\phinoName{none}"-            , "  \\phinoLabel{none}"+            , "  \\phinoCondition{ [ D, L, @ ] \\cap \\lparen B \\rparen = \\emptyset }"             , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ -- } }"             , "\\end{phinoInference}"             , "\\begin{phinoInference}"             , "  \\phinoName{bott}"-            , "  \\phinoLabel{bott}"             , "  \\phinoConclusion{ \\phinoDataize{ T }{ e }{ -- } }"             , "\\end{phinoInference}"             , "\\begin{phinoInference}"             , "  \\phinoName{norm}"-            , "  \\phinoLabel{norm}"+            , "  \\phinoCondition{ \\phinoNotFormation{ n } \\;\\text{and}\\; n \\not= T }"             , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }"             , "  \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }"             , "  \\phinoConclusion{ \\phinoDataize{ n }{ e }{ \\delta } }"@@ -1155,15 +1147,62 @@             ]         ] +    it "explains contextualization rules" $+      testCLISucceeded+        ["explain", "--contextualize"]+        [ unlines+            [ "\\begin{phinoInference}"+            , "  \\phinoName{cglobe}"+            , "  \\phinoLabel{globe}"+            , "  \\phinoConclusion{ \\phinoContextualize{ Q }{ k }{ Q } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{cxi}"+            , "  \\phinoLabel{xi}"+            , "  \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k }{ k } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{cdead}"+            , "  \\phinoLabel{dead}"+            , "  \\phinoConclusion{ \\phinoContextualize{ T }{ k }{ T } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{cprim}"+            , "  \\phinoLabel{prim}"+            , "  \\phinoConclusion{ \\phinoContextualize{ [[ B ]] }{ k }{ [[ B ]] } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{cdispatch}"+            , "  \\phinoLabel{disp}"+            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ n . \\tau }{ k }{ n_1 . \\tau } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{capplication}"+            , "  \\phinoLabel{app}"+            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k }{ n_2 } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ n ( \\tau -> e_1 ) }{ k }{ n_1 ( \\tau -> n_2 ) } }"+            , "\\end{phinoInference}"+            , "\\begin{phinoInference}"+            , "  \\phinoName{capplicationa}"+            , "  \\phinoLabel{appa}"+            , "  \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }"+            , "  \\phinoPremise{ \\phinoContextualize{ e_1 }{ k }{ n_2 } }"+            , "  \\phinoConclusion{ \\phinoContextualize{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ k }{ n_1 ( \\phiTerminal{\\alpha_{i}} -> n_2 ) } }"+            , "\\end{phinoInference}"+            ]+        ]+     it "fails with no rules specified" $       testCLIFailed         ["explain"]-        ["Either --rule, --normalize, --morph or --dataize must be specified"]+        ["Either --rule, --normalize, --morph, --dataize or --contextualize must be specified"]      it "fails when more than one rule set is specified" $       testCLIFailed         ["explain", "--morph", "--dataize"]-        ["Only one of --rule, --normalize, --morph or --dataize can be specified"]+        ["Only one of --rule, --normalize, --morph, --dataize or --contextualize can be specified"]      it "writes to target file" $       bracket

@@ -95,6 +95,27 @@       morph (chain, (Program ExRoot, Nothing) :| []) ExRoot (defaultDataizeContext ExRoot)         `shouldThrow` (\e -> "Atom 'F' does not exist" `isInfixOf` show (e :: SomeException)) +  -- 'norm' matches the bare meta 𝑛, which unifies with any expression, so it is+  -- guarded to fire only when 𝑛 is neither a formation ('not (formation 𝑛)',+  -- left to 'delta'/'box'/'fire'/'none') nor the termination ⊥ ('not (𝑛 = ⊥)',+  -- left to 'bott'). The dataization clauses are therefore disjoint and their+  -- order in 'dataization.yaml' cannot change behavior.+  describe "dataization 'norm' is disjoint from the specific clauses" $ do+    let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot))+        dataizeRule :: String -> Yaml.DataizeRule+        dataizeRule nm = fromMaybe (error ("no dataization rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.dataizationRules)+        asRule :: Yaml.DataizeRule -> Yaml.Rule+        asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing+    it "does not fire on a formation" $ do+      substs <- matchExpressionWithRule' [substEmpty] (ExFormation [BiDelta (BtOne "00")]) (asRule (dataizeRule "norm")) rctx+      substs `shouldBe` []+    it "does not fire on the termination ⊥" $ do+      substs <- matchExpressionWithRule' [substEmpty] ExTermination (asRule (dataizeRule "norm")) rctx+      substs `shouldBe` []+    it "still fires on a non-formation, non-termination normal form" $ do+      substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (dataizeRule "norm")) rctx+      null substs `shouldBe` False+   describe "dataize" $     test       dataize'@@ -139,7 +160,7 @@     let verb op = case op of           Yaml.OpMorph _ -> "morph"           Yaml.OpNormalize _ -> "normalize"-          Yaml.OpLambda _ -> "lambda"+          Yaml.OpEvaluate _ -> "evaluate"           Yaml.OpContextualize _ _ -> "contextualize"           Yaml.OpDataize _ -> "dataize"         allowed =@@ -167,11 +188,12 @@         (expectationFailure ("Dataization emitted step labels with no defining rule or operation: " ++ show orphans))    describe "names every rule uniquely across rule sets" $-    it "shares no rule name between morphing, dataization and normalization" $ do+    it "shares no rule name between morphing, dataization, normalization and contextualization" $ do       let names =             map (.name) Yaml.morphingRules               ++ map (.name) Yaml.dataizationRules               ++ map (.name) Yaml.normalizationRules+              ++ map (.name) Yaml.contextualizationRules           clashes = nub (filter (\n -> length (filter (== n) names) > 1) names)       clashes `shouldBe` [] @@ -192,7 +214,7 @@                    , "alpha"                    , "copy"                    , "prim"-                   , "lambda"+                   , "evaluate"                    , "applicationa"                    , "alpha"                    , "copy"

@@ -309,8 +309,8 @@       , ("λ ⤍ Test", Just (BiLambda (Function "Test")))       , ("L> !F", Just (BiLambda (FnMeta "F")))       , ("L> !F0", Just (BiLambda (FnMeta "F0")))-      , ("λ ⤍ 𝐹", Just (BiLambda (FnMeta "F")))-      , ("L> 𝐹2", Just (BiLambda (FnMeta "F2")))+      , ("λ ⤍ 𝑓", Just (BiLambda (FnMeta "F")))+      , ("L> 𝑓2", Just (BiLambda (FnMeta "F2")))       , ("!B", Just (BiMeta "B"))       , ("!B0", Just (BiMeta "B0"))       , ("!B_test", Just (BiMeta "B_test"))

@@ -63,8 +63,8 @@       )    describe "printExpression with SWEET UNICODE renders the pretty function meta" $-    it "meta lambda becomes 𝐹" $-      printExpression' (ExFormation [BiLambda (FnMeta "F")]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ λ ⤍ 𝐹 ⟧"+    it "meta lambda becomes 𝑓" $+      printExpression' (ExFormation [BiLambda (FnMeta "F")]) (SWEET, UNICODE, SINGLELINE, defaultMargin) `shouldBe` "⟦ λ ⤍ 𝑓 ⟧"    describe "printExpression keeps special double values in byte form so they re-parse" $     forM_

@@ -6,10 +6,13 @@ import Control.Exception (Exception (displayException), SomeException) import Control.Monad import Data.List (isInfixOf)+import Data.Text qualified as T+import Data.Text.Encoding (encodeUtf8)+import Data.Yaml qualified as Yaml import Misc import System.FilePath-import Test.Hspec (Spec, describe, it, runIO, shouldReturn, shouldThrow)-import Yaml (yamlRule)+import Test.Hspec (Spec, describe, it, runIO, shouldReturn, shouldSatisfy, shouldThrow)+import Yaml (ContextualizeRule, DataizeRule, MorphRule, yamlRule)  spec :: Spec spec = do@@ -37,3 +40,19 @@                    in "Unknown" `isInfixOf` msg || "Exactly one" `isInfixOf` msg               )       )++  describe "rejects a label that equals the name" $ do+    let failsAsRedundant decoded = case decoded of+          Left err -> "redundant" `isInfixOf` Yaml.prettyPrintParseException err+          Right _ -> False+        decodeYaml :: (Yaml.FromJSON a) => String -> Either Yaml.ParseException a+        decodeYaml = Yaml.decodeEither' . encodeUtf8 . T.pack+    it "in a morphing rule" $+      (decodeYaml "name: prim\nlabel: prim\nmatch: ⟦𝐵⟧\ne-match: 𝑒\nn-result: ⟦𝐵⟧" :: Either Yaml.ParseException MorphRule)+        `shouldSatisfy` failsAsRedundant+    it "in a dataization rule" $+      (decodeYaml "name: bott\nlabel: bott\nmatch: ⊥\ne-match: 𝑒\nd-result: '--'" :: Either Yaml.ParseException DataizeRule)+        `shouldSatisfy` failsAsRedundant+    it "in a contextualization rule" $+      (decodeYaml "name: cxi\nlabel: cxi\nmatch: ξ\nc-match: 𝑘\nc-result: 𝑘" :: Either Yaml.ParseException ContextualizeRule)+        `shouldSatisfy` failsAsRedundant