diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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`. diff --git a/phino.cabal b/phino.cabal --- a/phino.cabal +++ b/phino.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino -version: 0.0.86 +version: 0.0.87 license: MIT synopsis: Command-Line Manipulator of πœ‘-Calculus Expressions description: Please see the README on GitHub at diff --git a/resources/contextualization.yaml b/resources/contextualization.yaml new file mode 100644 --- /dev/null +++ b/resources/contextualization.yaml @@ -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 + - π‘˜ diff --git a/resources/dataization.yaml b/resources/dataization.yaml --- a/resources/dataization.yaml +++ b/resources/dataization.yaml @@ -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: 𝑛 diff --git a/resources/morphing.yaml b/resources/morphing.yaml --- a/resources/morphing.yaml +++ b/resources/morphing.yaml @@ -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: βŠ₯ diff --git a/src/CLI/Parsers.hs b/src/CLI/Parsers.hs --- a/src/CLI/Parsers.hs +++ b/src/CLI/Parsers.hs @@ -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 ) diff --git a/src/CLI/Runners.hs b/src/CLI/Runners.hs --- a/src/CLI/Runners.hs +++ b/src/CLI/Runners.hs @@ -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 diff --git a/src/CLI/Types.hs b/src/CLI/Types.hs --- a/src/CLI/Types.hs +++ b/src/CLI/Types.hs @@ -108,6 +108,7 @@ , _normalize :: Bool , _morph :: Bool , _dataize :: Bool + , _contextualize :: Bool , _shuffle :: Bool , _targetFile :: Maybe FilePath } diff --git a/src/CST.hs b/src/CST.hs --- a/src/CST.hs +++ b/src/CST.hs @@ -92,7 +92,7 @@ | B' -- B | D -- Ξ΄ | D' -- \delta - | F -- 𝐹 + | F -- 𝑓 | F' -- F deriving (Eq, Show) diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -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 diff --git a/src/Functions.hs b/src/Functions.hs --- a/src/Functions.hs +++ b/src/Functions.hs @@ -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 diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -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 diff --git a/src/Parser.hs b/src/Parser.hs --- a/src/Parser.hs +++ b/src/Parser.hs @@ -299,7 +299,7 @@ BiLambda . Function . T.pack <$> function , do _ <- lambda - BiLambda . FnMeta <$> meta' 'F' "𝐹" + BiLambda . FnMeta <$> meta' 'F' "𝑓" ] "binding" diff --git a/src/Render.hs b/src/Render.hs --- a/src/Render.hs +++ b/src/Render.hs @@ -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 diff --git a/src/Yaml.hs b/src/Yaml.hs --- a/src/Yaml.hs +++ b/src/Yaml.hs @@ -238,7 +238,7 @@ data Operation = OpMorph Expression | OpNormalize Expression - | 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") diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -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 diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -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" diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -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")) diff --git a/test/PrinterSpec.hs b/test/PrinterSpec.hs --- a/test/PrinterSpec.hs +++ b/test/PrinterSpec.hs @@ -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_ diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs --- a/test/YamlSpec.hs +++ b/test/YamlSpec.hs @@ -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