diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -237,7 +237,7 @@ ```bash $ phino explain --morph \begin{tabular}{rl} -\phinoMorphingRule{prim} +\phinoMorphingRule{mf} { \mathbb{M}( [[ B ]], e ) } { [[ B ]] } { } @@ -270,16 +270,16 @@ ```bash $ phino explain --contextualize -\begin{phinoInference} +\begin{phinoContextualizationInference} \phinoName{cxi} \phinoConclusion{ \phinoContextualize{ \phiTerminal{\xi} }{ k }{ k } } -\end{phinoInference} +\end{phinoContextualizationInference} ... -\begin{phinoInference} - \phinoName{cdispatch} +\begin{phinoContextualizationInference} + \phinoName{cd} \phinoPremise{ \phinoContextualize{ n }{ k }{ n_1 } } \phinoConclusion{ \phinoContextualize{ n . \tau }{ k }{ n_1 . \tau } } -\end{phinoInference} +\end{phinoContextualizationInference} ``` For more details, use `phino [COMMAND] --help` option. @@ -325,9 +325,9 @@ - Expression' # attribute in ginve bindings - BiMeta' | formation: # returns True if given expression is a formation - Expression' # (an abstraction ⟦…⟧); used by morphing 'dispatch' + Expression' # (an abstraction ⟦…⟧); used by morphing 'md' # as 'not (formation 𝑛)', so a non-formation head is - # morphed and a formation head is left to 'lambda' + # morphed and a formation head is left to 'ml' Comparable: # comparable object that may be used in 'eq' condition = Attribute' 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.88 +version: 0.0.89 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 --- a/resources/contextualization.yaml +++ b/resources/contextualization.yaml @@ -16,7 +16,7 @@ # the c meta. Derived terms are named 𝑛, 𝑛1, … in premise order; the bare 𝑛 is # skipped only when 'match' already binds it. -- name: cglobe +- name: cg match: Φ c-match: 𝑘 c-result: Φ @@ -26,17 +26,17 @@ c-match: 𝑘 c-result: 𝑘 -- name: cdead +- name: ct match: ⊥ c-match: 𝑘 c-result: ⊥ -- name: cprim +- name: cf match: ⟦𝐵⟧ c-match: 𝑘 c-result: ⟦𝐵⟧ -- name: cdispatch +- name: cd match: '𝑛.𝜏' c-match: 𝑘 c-result: '𝑛1.𝜏' @@ -46,7 +46,7 @@ - 𝑛 - 𝑘 -- name: capplication +- name: ca match: '𝑛(𝜏 ↦ 𝑒1)' c-match: 𝑘 c-result: '𝑛1(𝜏 ↦ 𝑛2)' @@ -60,7 +60,7 @@ - 𝑒1 - 𝑘 -- name: capplicationa +- name: caa match: '𝑛(α𝑖 ↦ 𝑒1)' c-match: 𝑘 c-result: '𝑛1(α𝑖 ↦ 𝑛2)' diff --git a/resources/dataization.yaml b/resources/dataization.yaml --- a/resources/dataization.yaml +++ b/resources/dataization.yaml @@ -22,7 +22,7 @@ # '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 +# ('not (𝑛 = ⊥)', carving out 'end'). Without the guard 'norm' would behave # correctly only by being declared last; with it the clauses no longer rely on # their order. @@ -71,7 +71,7 @@ - [Δ, λ, φ] - [𝐵] -- name: bott +- name: end match: ⊥ e-match: 𝑒 d-result: '--' diff --git a/resources/morphing.yaml b/resources/morphing.yaml --- a/resources/morphing.yaml +++ b/resources/morphing.yaml @@ -6,7 +6,7 @@ # the mutable state. The universe is threaded unchanged through every recursive # call and substituted for Φ by the 'root' rule (Φ, rendered Q, is just the # locator of e); the state is threaded too and the new state returned. Only the -# 'lambda' rule changes it, by firing an atom through 𝔼. The first argument is +# 'ml' rule changes it, by firing an atom through 𝔼. The first argument is # always a normal form: a non-NF expression matches no clause. 𝕄 navigates a # normal form to a formation one operation at a time, resolving Φ against e and # peeling dispatches and applications through normalization 𝒩. It never fires a @@ -19,21 +19,21 @@ # 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. 'globe' fires only on 𝕄(Φ, Φ)). Derived terms are +# pin it to a literal (e.g. 'mg' 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 +# 'ml' and 'md' are kept mutually exclusive: 'md' fires only # when its head 𝑛 is not a formation ('not (formation 𝑛)'), so every formation -# head — λ-bearing or not — is left to 'lambda' (and 'prim'). The two clauses +# head — λ-bearing or not — is left to 'ml' (and 'mf'). The two clauses # are disjoint and their relative order does not change behavior. -- name: prim +- name: mf match: ⟦𝐵⟧ e-match: 𝑒 n-result: ⟦𝐵⟧ -- name: lambda +- name: ml label: \lambda match: '⟦𝐵1, λ ⤍ 𝑓, 𝐵2⟧.𝜏' e-match: 𝑒 @@ -46,8 +46,7 @@ - n-result: 𝑛2 morph: 𝑛1 -- name: dispatch - label: disp +- name: md match: '𝑛.𝜏' e-match: 𝑒 n-result: 𝑛3 @@ -62,8 +61,7 @@ - n-result: 𝑛3 morph: 𝑛2 -- name: application - label: app +- name: ma match: '𝑛(𝜏 ↦ 𝑒1)' e-match: 𝑒 n-result: 𝑛3 @@ -75,8 +73,7 @@ - n-result: 𝑛3 morph: 𝑛2 -- name: applicationa - label: appa +- name: maa match: '𝑛(α𝑖 ↦ 𝑒1)' e-match: 𝑒 n-result: 𝑛3 @@ -113,7 +110,7 @@ e-match: 𝑒 n-result: ⊥ -- name: globe +- name: mg match: Φ e-match: Φ n-result: ⊥ diff --git a/src/Dataize.hs b/src/Dataize.hs --- a/src/Dataize.hs +++ b/src/Dataize.hs @@ -82,7 +82,7 @@ -- expression — and the mutable state 's', returning the morphed term together -- with the new state. The universe is matched against the rule's 'e-match' -- pattern (usually the '𝑒' meta, which binds 'e' so the 'root' rule substitutes --- it, but a rule may pin it to a literal such as 'globe' matching Φ). It is +-- it, but a rule may pin it to a literal such as 'mg' matching Φ). It is -- driven by -- the ordered rules from 'morphing.yaml': the first matching rule's premises are -- evaluated and its conclusion 'nresult' is built, always forwarding the same @@ -153,7 +153,7 @@ -- ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'), -- which it forwards to 𝕄, and the mutable state 's', returning the bytes together -- with the new state. Its rules come from 'dataization.yaml': 'delta' yields the --- asset bytes, 'none' (a formation) and 'bott' (⊥) yield empty bytes (--), +-- asset bytes, 'none' (a formation) and 'end' (⊥) yield empty bytes (--), -- 'box' contextualizes the φ-body and keeps dataizing (its step is labelled by -- its 'contextualize' side-computation), and 'norm' reduces through morphing, -- splicing the morphing steps into the chain. The clauses are disjoint (see @@ -244,7 +244,7 @@ -- of an earlier term — in isolation, binding its result meta. These never splice -- steps into the trace: 'morph' and 'evaluate' reduce on a fresh chain and discard -- it, 'contextualize' is pure. The state is threaded through: 'evaluate' (the --- 𝔼 of the 'lambda' and 'fire' rules) takes the incoming state 𝑠1 and yields a +-- 𝔼 of the 'ml' and 'fire' rules) takes the incoming state 𝑠1 and yields a -- new one 𝑠2, 'morph' propagates whatever its sub-reduction produced, and every -- other operation leaves the state untouched. sidePremise :: Expression -> DataizeContext -> (Subst, State) -> Y.Premise -> IO (Subst, State) @@ -386,7 +386,7 @@ _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 +-- a sub-expression in its 'where' (the 'md' and 'ma' rules morph -- the head before re-attaching it). The step chain is discarded: the producing -- rule splices the surrounding normalization steps itself. The state is threaded -- through and the new state returned alongside the morphed term. diff --git a/src/Deps.hs b/src/Deps.hs --- a/src/Deps.hs +++ b/src/Deps.hs @@ -30,7 +30,7 @@ -- is, so it is a plain string for now. Unlike the universe 𝑒, which is immutable -- and threaded unchanged, the state is mutable: 𝔼 takes a state 𝑠1 and returns a -- new one 𝑠2, and 𝕄/𝔻 propagate that change to their callers. Only the rules --- that fire an atom — 'lambda' (morphing) and 'fire' (dataization) — can change +-- that fire an atom — 'ml' (morphing) and 'fire' (dataization) — can change -- the state; every other rule threads it through untouched. type State = String diff --git a/src/LaTeX.hs b/src/LaTeX.hs --- a/src/LaTeX.hs +++ b/src/LaTeX.hs @@ -376,6 +376,7 @@ explainMorphRule :: Y.MorphRule -> String explainMorphRule rule = inference + "phinoMorphingInference" rule.name rule.label rule.when @@ -387,6 +388,7 @@ explainDataizeRule :: Y.DataizeRule -> String explainDataizeRule rule = inference + "phinoDataizationInference" rule.name rule.label rule.when @@ -398,6 +400,7 @@ explainContextualizeRule :: Y.ContextualizeRule -> String explainContextualizeRule rule = inference + "phinoContextualizationInference" rule.name rule.label Nothing @@ -417,14 +420,14 @@ -- Assemble an inference block from a name, optional label, optional side -- condition, the premise judgments and the conclusion judgment. -inference :: String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String -inference name label cond premises conclusion = +inference :: String -> String -> Maybe String -> Maybe Y.Condition -> [String] -> String -> String +inference env name label cond premises conclusion = intercalate "\n" $ - ["\\begin{phinoInference}", " \\phinoName{" ++ name ++ "}"] + ["\\begin{" ++ env ++ "}", " \\phinoName{" ++ name ++ "}"] ++ maybe [] (\symbol -> [" \\phinoLabel{" ++ symbol ++ "}"]) label ++ maybe [] (\rendered -> [" \\phinoCondition{ " ++ rendered ++ " }"]) (conditionInLatex cond) ++ map (\premise -> " \\phinoPremise{ " ++ premise ++ " }") premises - ++ [" \\phinoConclusion{ " ++ conclusion ++ " }", "\\end{phinoInference}"] + ++ [" \\phinoConclusion{ " ++ conclusion ++ " }", "\\end{" ++ env ++ "}"] renderExpr :: Expression -> String renderExpr expr = renderToLatex (expressionToCST expr) defaultLatexContext diff --git a/test/CLISpec.hs b/test/CLISpec.hs --- a/test/CLISpec.hs +++ b/test/CLISpec.hs @@ -1045,62 +1045,59 @@ testCLISucceeded ["explain", "--morph"] [ unlines - [ "\\begin{phinoInference}" - , " \\phinoName{prim}" + [ "\\begin{phinoMorphingInference}" + , " \\phinoName{mf}" , " \\phinoConclusion{ \\phinoMorph{ [[ B ]] }{ e }{ [[ B ]] } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{lambda}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{ml}" , " \\phinoLabel{\\lambda}" , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }" , " \\phinoPremise{ \\phinoNormalize{ n . \\tau }{ n_1 } }" , " \\phinoPremise{ \\phinoMorph{ n_1 }{ e }{ n_2 } }" , " \\phinoConclusion{ \\phinoMorph{ [[ B_1, L> F, B_2 ]] . \\tau }{ e }{ n_2 } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{dispatch}" - , " \\phinoLabel{disp}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{md}" , " \\phinoCondition{ \\phinoNotFormation{ n } }" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }" , " \\phinoPremise{ \\phinoNormalize{ n_1 . \\tau }{ n_2 } }" , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }" , " \\phinoConclusion{ \\phinoMorph{ n . \\tau }{ e }{ n_3 } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{application}" - , " \\phinoLabel{app}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{ma}" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }" , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\tau -> e_1 ) }{ n_2 } }" , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }" , " \\phinoConclusion{ \\phinoMorph{ n ( \\tau -> e_1 ) }{ e }{ n_3 } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{applicationa}" - , " \\phinoLabel{appa}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{maa}" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }" , " \\phinoPremise{ \\phinoNormalize{ n_1 ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ n_2 } }" , " \\phinoPremise{ \\phinoMorph{ n_2 }{ e }{ n_3 } }" , " \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ n_3 } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" , " \\phinoName{root}" , " \\phinoCondition{ e \\not= Q }" , " \\phinoPremise{ \\phinoNormalize{ e }{ n } }" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }" , " \\phinoConclusion{ \\phinoMorph{ Q }{ e }{ n_1 } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" , " \\phinoName{dead}" , " \\phinoConclusion{ \\phinoMorph{ T }{ e }{ T } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" , " \\phinoName{xi}" , " \\phinoConclusion{ \\phinoMorph{ \\phiTerminal{\\xi} }{ e }{ T } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{globe}" + , "\\end{phinoMorphingInference}" + , "\\begin{phinoMorphingInference}" + , " \\phinoName{mg}" , " \\phinoConclusion{ \\phinoMorph{ Q }{ Q }{ T } }" - , "\\end{phinoInference}" + , "\\end{phinoMorphingInference}" ] ] @@ -1108,42 +1105,42 @@ testCLISucceeded ["explain", "--dataize"] [ unlines - [ "\\begin{phinoInference}" + [ "\\begin{phinoDataizationInference}" , " \\phinoName{delta}" , " \\phinoLabel{\\Delta}" , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, D> \\delta, B_2 ]] }{ e }{ \\delta } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoDataizationInference}" + , "\\begin{phinoDataizationInference}" , " \\phinoName{box}" , " \\phinoCondition{ [ D, L ] \\cap \\lparen B_1 \\cup B_2 \\rparen = \\emptyset }" , " \\phinoPremise{ \\phinoContextualize{ e_1 }{ [[ B_1, @ -> e_1, B_2 ]] }{ n } }" , " \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }" , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }" , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, @ -> e_1, B_2 ]] }{ e }{ \\delta } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoDataizationInference}" + , "\\begin{phinoDataizationInference}" , " \\phinoName{fire}" , " \\phinoPremise{ \\phinoEvaluate{ [[ B_1, L> F, B_2 ]] }{ n } }" , " \\phinoPremise{ \\phinoNormalize{ n }{ n_1 } }" , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }" , " \\phinoConclusion{ \\phinoDataize{ [[ B_1, L> F, B_2 ]] }{ e }{ \\delta } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoDataizationInference}" + , "\\begin{phinoDataizationInference}" , " \\phinoName{none}" , " \\phinoCondition{ [ D, L, @ ] \\cap \\lparen B \\rparen = \\emptyset }" , " \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ -- } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{bott}" + , "\\end{phinoDataizationInference}" + , "\\begin{phinoDataizationInference}" + , " \\phinoName{end}" , " \\phinoConclusion{ \\phinoDataize{ T }{ e }{ -- } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoDataizationInference}" + , "\\begin{phinoDataizationInference}" , " \\phinoName{norm}" , " \\phinoCondition{ \\phinoNotFormation{ n } \\;\\text{and}\\; n \\not= T }" , " \\phinoPremise{ \\phinoMorph{ n }{ e }{ n_1 } }" , " \\phinoPremise{ \\phinoDataize{ n_1 }{ e }{ \\delta } }" , " \\phinoConclusion{ \\phinoDataize{ n }{ e }{ \\delta } }" - , "\\end{phinoInference}" + , "\\end{phinoDataizationInference}" ] ] @@ -1151,39 +1148,39 @@ testCLISucceeded ["explain", "--contextualize"] [ unlines - [ "\\begin{phinoInference}" - , " \\phinoName{cglobe}" + [ "\\begin{phinoContextualizationInference}" + , " \\phinoName{cg}" , " \\phinoConclusion{ \\phinoContextualize{ Q }{ k }{ Q } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" + , "\\end{phinoContextualizationInference}" + , "\\begin{phinoContextualizationInference}" , " \\phinoName{cxi}" , " \\phinoConclusion{ \\phinoContextualize{ \\phiTerminal{\\xi} }{ k }{ k } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{cdead}" + , "\\end{phinoContextualizationInference}" + , "\\begin{phinoContextualizationInference}" + , " \\phinoName{ct}" , " \\phinoConclusion{ \\phinoContextualize{ T }{ k }{ T } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{cprim}" + , "\\end{phinoContextualizationInference}" + , "\\begin{phinoContextualizationInference}" + , " \\phinoName{cf}" , " \\phinoConclusion{ \\phinoContextualize{ [[ B ]] }{ k }{ [[ B ]] } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{cdispatch}" + , "\\end{phinoContextualizationInference}" + , "\\begin{phinoContextualizationInference}" + , " \\phinoName{cd}" , " \\phinoPremise{ \\phinoContextualize{ n }{ k }{ n_1 } }" , " \\phinoConclusion{ \\phinoContextualize{ n . \\tau }{ k }{ n_1 . \\tau } }" - , "\\end{phinoInference}" - , "\\begin{phinoInference}" - , " \\phinoName{capplication}" + , "\\end{phinoContextualizationInference}" + , "\\begin{phinoContextualizationInference}" + , " \\phinoName{ca}" , " \\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}" + , "\\end{phinoContextualizationInference}" + , "\\begin{phinoContextualizationInference}" + , " \\phinoName{caa}" , " \\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}" + , "\\end{phinoContextualizationInference}" ] ] diff --git a/test/DataizeSpec.hs b/test/DataizeSpec.hs --- a/test/DataizeSpec.hs +++ b/test/DataizeSpec.hs @@ -70,11 +70,11 @@ ) ] - -- 'dispatch' fires only when its head is not a formation ('not (formation 𝑛)'), - -- so a formation head — λ-bearing or not — is left to 'lambda'/'prim'. The + -- 'md' fires only when its head is not a formation ('not (formation 𝑛)'), + -- so a formation head — λ-bearing or not — is left to 'ml'/'mf'. The -- two clauses are mutually exclusive and their order in 'morphing.yaml' -- cannot change behavior. - describe "morphing 'dispatch' is disjoint from 'lambda'" $ do + describe "morphing 'md' is disjoint from 'ml'" $ do let rctx = RuleContext (execBuildTerm ExRoot (defaultDataizeContext ExRoot)) morphRule :: String -> Yaml.MorphRule morphRule nm = fromMaybe (error ("no morphing rule named " ++ nm)) (find (\r -> r.name == nm) Yaml.morphingRules) @@ -82,17 +82,17 @@ asRule r = Yaml.Rule r.name Nothing Nothing r.match ExRoot r.when Nothing Nothing lambdaFormation = ExFormation [BiLambda (Function "L_dummy"), BiVoid AtRho] it "does not fire on a λ-bearing formation dispatch" $ do - substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "dispatch")) rctx + substs <- matchExpressionWithRule' [substEmpty] (ExDispatch lambdaFormation (AtLabel "x")) (asRule (morphRule "md")) rctx substs `shouldBe` [] it "still fires on a non-λ-formation dispatch" $ do - substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "dispatch")) rctx + substs <- matchExpressionWithRule' [substEmpty] (ExDispatch ExXi (AtLabel "x")) (asRule (morphRule "md")) rctx null substs `shouldBe` False - -- ⟦λ ⤍ F⟧.a.b.c : 'dispatch' peels .c then .b (their heads are dispatches, - -- not λ-formations, so 'λ ∉ 𝐵' holds), then 'lambda' handles the base + -- ⟦λ ⤍ F⟧.a.b.c : 'md' peels .c then .b (their heads are dispatches, + -- not λ-formations, so 'λ ∉ 𝐵' holds), then 'ml' handles the base -- ⟦λ ⤍ F⟧.a and fires the atom. The chain therefore routes - -- dispatch → dispatch → lambda; firing the undefined atom 'F' is what - -- raises the error, proving the base λ-formation reached 'lambda'. - it "drills a chained λ-formation dispatch down to the base 'lambda'" $ do + -- md → md → ml; firing the undefined atom 'F' is what + -- raises the error, proving the base λ-formation reached 'ml'. + it "drills a chained λ-formation dispatch down to the base 'ml'" $ do let base = ExFormation [BiLambda (Function "F")] chain = ExDispatch (ExDispatch (ExDispatch base (AtLabel "a")) (AtLabel "b")) (AtLabel "c") morph (chain, (Program ExRoot, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot) @@ -101,7 +101,7 @@ -- '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 + -- left to 'end'). 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)) @@ -213,27 +213,27 @@ "Q -> [[ bytes(data) -> [[ @ -> $.data ]], number(as-bytes) -> [[ @ -> $.as-bytes, plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" labels `shouldBe` [ "contextualize" - , "applicationa" + , "maa" , "alpha" , "copy" - , "prim" + , "mf" , "evaluate" - , "applicationa" + , "maa" , "alpha" , "copy" - , "prim" + , "mf" , "contextualize" , "dot" - , "application" + , "ma" , "stay" - , "prim" + , "mf" , "contextualize" , "dot" , "copy" ] it "dataizes a located reference through the expected rules" $ do labels <- labelsOf "Q.foo.bar" "Q -> [[ foo -> [[ bar -> [[ @ -> Q.x ]] ]], x -> [[ D> 42- ]] ]]" - labels `shouldBe` ["contextualize", "dispatch", "dot", "copy", "prim"] + labels `shouldBe` ["contextualize", "md", "dot", "copy", "mf"] testDataize [ diff --git a/test/YamlSpec.hs b/test/YamlSpec.hs --- a/test/YamlSpec.hs +++ b/test/YamlSpec.hs @@ -55,7 +55,7 @@ (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) + (decodeYaml "name: end\nlabel: end\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)