phino 0.0.96 → 0.0.97

raw patch · 8 files changed

+59/−40 lines, 8 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• README.md +1/−1
• phino.cabal +1/−1
• resources/dataization.yaml +5/−8
• resources/morphing.yaml +3/−2
• src/Dataize.hs +19/−9
• src/Rule.hs +1/−1
• test/CLISpec.hs +4/−7
• test/DataizeSpec.hs +25/−11

@@ -243,7 +243,7 @@   { }   { } ...-\phinoMorphingRule{root}+\phinoMorphingRule{universe}   { \mathbb{M}( Q, e ) }   { \mathbb{M}( \phinoNormalize{ e }, e ) }   { $ e \not= Q $ }

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

@@ -22,9 +22,11 @@ # '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 'end'). Without the guard 'norm' would behave-# correctly only by being declared last; with it the clauses no longer rely on-# their order.+# ('not (𝑛 = ⊥)'). 𝔻 is partial: ⊥ (the terminator T) signals an error and+# lies outside its domain, so it deliberately matches no clause and dataization+# stops there — there is no 'end' rule mapping ⊥ to empty bytes (see #955).+# 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@@ -75,11 +77,6 @@   premises:     - d-result: δ       dataize: ⊥--- name: end-  match: ⊥-  e-match: 𝑒-  d-result: '--'  - name: norm   match: 𝑛

@@ -4,7 +4,7 @@ # Morphing 𝕄 — applied top-to-bottom, first matching clause wins. It is ternary, # 𝕄(n, e, s): n is the morphed term, e is the fixed global universe and s is # the mutable state. The universe is threaded unchanged through every recursive-# call and substituted for Φ by the 'root' rule (Φ, rendered Q, is just the+# call and substituted for Φ by the 'universe' rule (Φ, rendered Q, is just the # locator of e); the state is threaded too and the new state returned. Only the # '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@@ -87,7 +87,8 @@     - n-result: 𝑛3       morph: 𝑛2 -- name: root+- name: universe+  label: \Phi   match: Φ   e-match: 𝑒   n-result: 𝑛1

@@ -83,7 +83,7 @@ -- 𝕄(n, e, s): besides the term 'n' it takes the universe 'e' ('univ') — a plain -- 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+-- pattern (usually the '𝑒' meta, which binds 'e' so the 'universe' rule substitutes -- it, but a rule may pin it to a literal such as 'mg' matching Φ). Its rules -- come from 'morphing.yaml': the first matching rule's premises are evaluated and -- its conclusion 'nresult' is built, always forwarding the same universe. The@@ -157,12 +157,15 @@   ((bytes, seq), _state) <- dataize' (expr, (program, Nothing) :| []) univ emptyState ctx   pure (bytes, reverse seq) --- The Dataization function 𝔻 retrieves bytes from an expression. It is total and--- ternary, 𝔻(n, e, s): besides the term 'n' it takes the universe 'e' ('univ'),+-- The Dataization function 𝔻 retrieves bytes from an expression. It is partial+-- and 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, 'end' (⊥) yields empty bytes (--) and 'none' (a formation with no--- Δ/λ/φ) delegates to 'end' by dataizing ⊥,+-- asset bytes and 'none' (a formation with no Δ/λ/φ) has nothing to dataize, so+-- it dataizes ⊥. The terminator ⊥ signals an error and lies outside 𝔻's domain,+-- so it matches no clause (there is no 'end' rule mapping it to empty bytes) and+-- dataization stops there; a data-less formation therefore fails through the+-- same path (see #955). -- '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@@ -181,8 +184,15 @@   matched <- firstMatch rules   case matched of     Just (rule, subst) -> reduce rule subst-    Nothing -> throwIO (userError "no dataization rule matched")+    Nothing -> throwIO (userError (unmatched expr))   where+    -- 𝔻 is partial: the terminator ⊥ signals an error and lies outside its+    -- domain (see #955), so it matches no clause and lands here. Name it in the+    -- message rather than reporting the generic "no dataization rule matched",+    -- which would otherwise hide that the computation reached a dead end.+    unmatched :: Expression -> String+    unmatched ExTermination = "dataization reached the terminator ⊥, which signals an error and cannot be dataized"+    unmatched _ = "no dataization rule matched"     firstMatch :: [Y.DataizeRule] -> IO (Maybe (Y.DataizeRule, Subst))     firstMatch [] = pure Nothing     firstMatch (rule : rest) = do@@ -345,9 +355,9 @@     pure (bts, state')   _ -> throwIO (userError "Can't call _dataize from atoms with non-formation universe") --- A number atom only operates on numeric data. Empty bytes (the result of--- dataizing a bare formation ⟦𝐵⟧ or ⊥ now that 𝔻 is total) carry no number,--- so the operand is rejected and the atom yields ⊥.+-- A number atom only operates on numeric data. Empty bytes — a genuine+-- zero-length byte array ⟦Δ ⤍ --⟧ — carry no number, so the operand is rejected+-- and the atom yields ⊥. asNumber :: Bytes -> Maybe Double asNumber BtEmpty = Nothing asNumber bts = Just (either toDouble id (btsToNum bts))

@@ -363,7 +363,7 @@ -- and morphing driver, where a rule applies to the entire configuration rather -- than to nested redexes. The leading '[Subst]' seeds matching with pre-bound -- meta-variables: the morphing driver passes the global universe bound to 'e',--- the second argument of 𝕄(n, e), so the 'root' rule reads it directly instead+-- the second argument of 𝕄(n, e), so the 'universe' rule reads it directly instead -- of through a 'global()' build-term function. Pass '[substEmpty]' for no seed. matchExpressionWithRule' :: [Subst] -> Expression -> Y.Rule -> RuleContext -> IO [Subst] matchExpressionWithRule' = matchExpressionBy matchExpression'

@@ -867,9 +867,9 @@       withStdin "Q -> [[ D> 01- ]]" $         testCLISucceeded ["dataize"] ["01-"] -    it "dataizes empty object to empty bytes" $+    it "fails to dataize an empty object, which dataizes the terminator ⊥" $       withStdin "Q -> [[ ]]" $-        testCLISucceeded ["dataize"] ["--"]+        testCLIFailed ["dataize"] ["terminator ⊥"]      it "dataizes with --sequence" $       withStdin "{[[ @ -> [[ x -> [[ D> 01-, y -> ? ]](y -> [[ ]]) ]].x ]]}" $@@ -1085,7 +1085,8 @@             , "  \\phinoConclusion{ \\phinoMorph{ n ( \\phiTerminal{\\alpha_{i}} -> e_1 ) }{ e }{ s_1 }{ n_3 }{ s_3 } }"             , "\\end{phinoMorphingInference}"             , "\\begin{phinoMorphingInference}"-            , "  \\phinoName{root}"+            , "  \\phinoName{universe}"+            , "  \\phinoLabel{\\Phi}"             , "  \\phinoCondition{ e \\not= Q }"             , "  \\phinoPremise{ \\phinoNormalize{ e }{ n } }"             , "  \\phinoPremise{ \\phinoMorph{ n }{ e }{ s_1 }{ n_1 }{ s_2 } }"@@ -1137,10 +1138,6 @@             , "  \\phinoCondition{ [ D \\char44{} L \\char44{} @ ] \\cap B = \\emptyset }"             , "  \\phinoPremise{ \\phinoDataize{ T }{ e }{ s_1 }{ \\delta }{ s_2 } }"             , "  \\phinoConclusion{ \\phinoDataize{ [[ B ]] }{ e }{ s_1 }{ \\delta }{ s_2 } }"-            , "\\end{phinoDataizationInference}"-            , "\\begin{phinoDataizationInference}"-            , "  \\phinoName{end}"-            , "  \\phinoConclusion{ \\phinoDataize{ T }{ e }{ s }{ |--| }{ s } }"             , "\\end{phinoDataizationInference}"             , "\\begin{phinoDataizationInference}"             , "  \\phinoName{norm}"

@@ -127,9 +127,10 @@    -- '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 'end'). The dataization clauses are therefore disjoint and their-  -- order in 'dataization.yaml' cannot change behavior.+  -- left to 'delta'/'box'/'fire'/'none') nor the termination ⊥ ('not (𝑛 = ⊥)').+  -- 𝔻 is partial: ⊥ matches no clause and lands on the unmatched-term error+  -- (#955). 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@@ -150,8 +151,6 @@     test       dataize'       [ ("[[ D> 00- ]] => 00-", ExFormation [BiDelta (BtOne "00")], ExRoot, BtOne "00")-      , ("T => --", ExTermination, ExRoot, BtEmpty)-      , ("[[ ]] => --", ExFormation [], ExRoot, BtEmpty)       ,         ( "[[ @ -> [[ D> 00-]] ]] => 00-"         , ExFormation [BiTau AtPhi (ExFormation [BiDelta (BtOne "00"), BiVoid AtRho]), BiVoid AtRho]@@ -186,6 +185,19 @@         )       ] +  -- 𝔻 is partial (#955): the terminator ⊥ signals an error and lies outside its+  -- domain, so it matches no dataization clause and 𝔻 stops there instead of+  -- yielding empty bytes. A data-less formation ⟦⟧ ('none') dataizes ⊥, so it+  -- fails through the very same path — it has nothing to dataize.+  describe "fails to dataize the terminator" $ do+    let failsOn desc input =+          it desc $+            let prog = Program ExRoot+             in dataize' (input, (prog, Nothing) :| []) ExRoot emptyState (defaultDataizeContext ExRoot)+                  `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))+    failsOn "throws on ⊥ instead of mapping it to empty bytes" ExTermination+    failsOn "throws on a data-less formation, which dataizes ⊥" (ExFormation [])+   describe "labels every step with a defined rule or operation" $ do     let verb op = case op of           Yaml.OpMorph _ -> "morph"@@ -261,12 +273,14 @@     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", "md", "dot", "copy", "mf"]-    -- The 'none' rule no longer emits '--' itself: it delegates to 'end' by-    -- dataizing ⊥, so the empty formation reduces through one labelled 'dataize'-    -- step (𝔻(⟦⟧) → 𝔻(⊥)) before 'end' yields the empty bytes (#942).-    it "dataizes an empty formation by delegating to end" $ do-      labels <- labelsOf "Q" "Q -> [[ ]]"-      labels `shouldBe` ["dataize"]+    -- The 'none' rule dataizes ⊥ (𝔻(⟦⟧) → 𝔻(⊥)), which matches no clause now+    -- that there is no 'end' rule, so an empty formation reduces through one+    -- labelled 'dataize' step and then fails: it has nothing to dataize (#955).+    it "fails to dataize an empty formation, which dataizes ⊥" $ do+      prog <- parseProgramThrows "Q -> [[ ]]"+      loc <- parseExpressionThrows "Q"+      dataize prog (defaultDataizeContext loc)+        `shouldThrow` (\e -> "terminator" `isInfixOf` show (e :: SomeException))    testDataize     [