phino 0.0.88 → 0.0.89
raw patch · 11 files changed
+115/−118 lines, 11 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- README.md +8/−8
- phino.cabal +1/−1
- resources/contextualization.yaml +6/−6
- resources/dataization.yaml +2/−2
- resources/morphing.yaml +10/−13
- src/Dataize.hs +4/−4
- src/Deps.hs +1/−1
- src/LaTeX.hs +7/−4
- test/CLISpec.hs +57/−60
- test/DataizeSpec.hs +18/−18
- test/YamlSpec.hs +1/−1
README.md view
@@ -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'
phino.cabal view
@@ -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 <https://github.com/objectionary/phino#readme>
resources/contextualization.yaml view
@@ -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)'
resources/dataization.yaml view
@@ -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: '--'
resources/morphing.yaml view
@@ -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: ⊥
src/Dataize.hs view
@@ -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.
src/Deps.hs view
@@ -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
src/LaTeX.hs view
@@ -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
test/CLISpec.hs view
@@ -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}" ] ]
test/DataizeSpec.hs view
@@ -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 [
test/YamlSpec.hs view
@@ -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)