phino 0.0.123 → 0.0.124
raw patch · 5 files changed
+172/−75 lines, 5 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- XMIR: XmirContext :: Bool -> Bool -> (Expression -> String) -> XmirContext
+ XMIR: XmirContext :: Bool -> Bool -> Bool -> (Expression -> String) -> XmirContext
Files
- phino.cabal +1/−1
- src/CLI/Runners.hs +14/−4
- src/XMIR.hs +115/−66
- test/CLISpec.hs +16/−0
- test/XMIRSpec.hs +26/−4
phino.cabal view
@@ -1,6 +1,6 @@ cabal-version: 3.0 name: phino-version: 0.0.123+version: 0.0.124 license: MIT synopsis: Command-Line Manipulator of 𝜑-Calculus Expressions description: Please see the README on GitHub at <https://github.com/objectionary/phino#readme>
src/CLI/Runners.hs view
@@ -63,7 +63,7 @@ ([], XMIR, XMIR) -> (\_ -> escapeXML input) ([], _, _) -> (\_ -> escapeXMLText input) (_, _, _) -> (\rewritten -> escapeXMLText (P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin)))- xmirCtx = XmirContext _omitListing _omitComments listing+ xmirCtx = XmirContext _omitListing _omitComments _hideRho listing printCtx = toPrintCtx xmirCtx foc exclude = (`F.exclude` excluded) include = (`F.include` included)@@ -205,7 +205,7 @@ _hideRho _flat _margin- defaultXmirContext+ (XmirContext _omitListing _omitComments _hideRho listing) _nonumber _compress _canonize@@ -218,6 +218,11 @@ _label _meetPrefix _outputFormat+ -- The listing of a dataization result is the 𝜑 text of the printed+ -- expression, the way 'rewrite' does it; the omit flags and '--hide-rho'+ -- reach the XMIR writer through this context (#1076)+ listing :: Expression -> String+ listing e = escapeXMLText (P.printExpression' e (_sugarType, UNICODE, _flat, _margin)) -- Run 𝕄 on its own, the way 'runDataize' runs 𝔻. The whole option surface of -- 'dataize' applies unchanged, since the two commands differ only in the@@ -277,7 +282,7 @@ _hideRho _flat _margin- defaultXmirContext+ (XmirContext _omitListing _omitComments _hideRho listing) _nonumber _compress _canonize@@ -290,6 +295,11 @@ _label _meetPrefix _outputFormat+ -- The listing of a dataization result is the 𝜑 text of the printed+ -- expression, the way 'rewrite' does it; the omit flags and '--hide-rho'+ -- reach the XMIR writer through this context (#1076)+ listing :: Expression -> String+ listing e = escapeXMLText (P.printExpression' e (_sugarType, UNICODE, _flat, _margin)) runExplain :: OptsExplain -> IO () runExplain OptsExplain{..} = do@@ -322,7 +332,7 @@ expr <- merge exprs validateXmirTopLevel _outputFormat expr let listing = const (escapeXMLText (P.printExpression' expr (_sugarType, UNICODE, _flat, _margin)))- xmirCtx = XmirContext _omitListing _omitComments listing+ xmirCtx = XmirContext _omitListing _omitComments False listing printCtx = toPrintCtx xmirCtx expr' <- printInFormat printCtx expr printOut _targetFile expr'
src/XMIR.hs view
@@ -24,6 +24,7 @@ import AST import Bytes (btsIsUtf8, btsSize, btsToNum, btsToStr, bytesToBts) import Control.Exception (Exception (displayException), throwIO)+import Control.Monad (unless) import Data.Bifunctor (bimap) import Data.Foldable (foldlM) import Data.List (intercalate)@@ -48,6 +49,7 @@ data XmirContext = XmirContext { _omitListing :: Bool , _omitComments :: Bool+ , _hideRho :: Bool , _listing :: Expression -> String } @@ -58,7 +60,7 @@ gitRevision = take 7 $(gitHash) defaultXmirContext :: XmirContext-defaultXmirContext = XmirContext True True (const "")+defaultXmirContext = XmirContext True True False (const "") data XMIRException = UnsupportedTopExpression Expression@@ -173,56 +175,48 @@ (base, children) <- expression expr ctx pure (object [("name", name), ("base", base)] children) +-- Render a formation's bindings as child nodes, honoring '--hide-rho' by+-- dropping every bound ρ before it reaches the nodes (#1076) nestedBindings :: [Binding] -> XmirContext -> IO [Node]-nestedBindings bds ctx = catMaybes <$> mapM (`formationBinding` ctx) bds+nestedBindings bds ctx@XmirContext{..} = catMaybes <$> mapM (`formationBinding` ctx) bds'+ where+ bds' :: [Binding]+ bds' = if _hideRho then filter (not . isRho) bds else bds+ isRho :: Binding -> Bool+ isRho (BiTau AtRho _) = True+ isRho _ = False expressionToXMIR :: Expression -> XmirContext -> IO Document-expressionToXMIR expr@(ExFormation [BiTau (AtLabel _) arg, BiVoid AtRho]) ctx@XmirContext{..} = case arg of- ExFormation _ -> expressionToXMIR'- ExApplication _ _ -> expressionToXMIR'- ExDispatch _ _ -> expressionToXMIR'- ExRoot -> expressionToXMIR'+expressionToXMIR expr@(ExFormation [BiTau (AtLabel _) arg, BiVoid AtRho]) ctx = case arg of+ ExFormation _ -> programToXMIR expr ctx+ ExApplication _ _ -> programToXMIR expr ctx+ ExDispatch _ _ -> programToXMIR expr ctx+ ExRoot -> programToXMIR expr ctx _ -> throwIO (UnsupportedTopExpression expr)+-- The top of a '--partial' residual and the result of 'merge' are arbitrary+-- formations: several τ/λ bindings, voids and a bound ρ. Every binding such a+-- formation carries becomes a child of <object>; 'xmirToPhi' reads the list+-- back (#1076)+expressionToXMIR expr@(ExFormation bds) ctx =+ documentWith ctx [] expr rootNodes where- expressionToXMIR' :: IO Document- expressionToXMIR' = do- started <- getCurrentTime- (pckg, expr') <- getPackage expr- root <- rootExpression expr' ctx- now <- getCurrentTime- let text = _listing expr- listing =- if _omitListing- then show (length (lines text)) ++ " line(s)"- else text- listing' = NodeElement (element "listing" [] [NodeContent (T.pack listing)])- metas = metasWithPackage (intercalate "." pckg)- ms :: Int- ms = round (diffUTCTime now started * 1000)- revisionAttr = [("revision", gitRevision) | gitRevision /= "UNKNOWN"]- attrs =- [ ("author", "phino")- , ("dob", formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now)- , ("ms", show ms)- , ("time", time now)- , ("version", showVersion version)- , ("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")- , ("xsi:noNamespaceSchemaLocation", "https://raw.githubusercontent.com/objectionary/eo/refs/heads/gh-pages/XMIR.xsd")- ]- <> revisionAttr- pure- ( Document- (Prologue [] Nothing [])- ( element- "object"- attrs- ( if null pckg- then [listing', root]- else [listing', metas, root]- )- )- []- )+ rootNodes :: IO [Node]+ rootNodes = do+ roots <- nestedBindings bds ctx+ unless (any isElement roots) (throwIO (UnsupportedTopExpression expr))+ pure roots+ isElement :: Node -> Bool+ isElement (NodeElement _) = True+ isElement _ = False+expressionToXMIR expr _ = throwIO (UnsupportedTopExpression expr)++-- A program document: the package spine is peeled off the top level into+-- <metas> and the single binding left becomes the root <o> element+programToXMIR :: Expression -> XmirContext -> IO Document+programToXMIR expr ctx = do+ (pckg, expr') <- getPackage expr+ documentWith ctx pckg expr (rootNodes expr' ctx)+ where -- Extract package from given expression -- The function returns tuple (X, Y), where -- - X: list of package parts@@ -237,12 +231,51 @@ getPackage (ExFormation [BiTau at ex, BiLambda (Function "Package"), BiVoid AtRho]) = pure ([], ExFormation [BiTau at ex, BiVoid AtRho]) getPackage (ExFormation [bd, BiVoid AtRho]) = pure ([], ExFormation [bd, BiVoid AtRho]) getPackage ex = throwIO (userError (printf "Can't extract package from given expression:\n %s" (printExpression ex)))- -- Convert root Expression to Node- rootExpression :: Expression -> XmirContext -> IO Node- rootExpression (ExFormation [bd, BiVoid AtRho]) c = do- [bd'] <- nestedBindings [bd] c- pure bd'- rootExpression ex _ = throwIO (UnsupportedExpression ex)+ rootNodes :: Expression -> XmirContext -> IO [Node]+ rootNodes (ExFormation [bd, BiVoid AtRho]) c = nestedBindings [bd] c+ rootNodes ex _ = throwIO (UnsupportedExpression ex)++-- Assemble the <object> document: timing attributes, the listing, <metas>+-- when the expression carries a package, and the root nodes below them+documentWith :: XmirContext -> [String] -> Expression -> IO [Node] -> IO Document+documentWith XmirContext{..} pckg expr rootsIO = do+ started <- getCurrentTime+ roots <- rootsIO+ now <- getCurrentTime+ let text = _listing expr+ listing =+ if _omitListing+ then show (length (lines text)) ++ " line(s)"+ else text+ listing' = NodeElement (element "listing" [] [NodeContent (T.pack listing)])+ metas = metasWithPackage (intercalate "." pckg)+ ms :: Int+ ms = round (diffUTCTime now started * 1000)+ revisionAttr = [("revision", gitRevision) | gitRevision /= "UNKNOWN"]+ attrs =+ [ ("author", "phino")+ , ("dob", formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now)+ , ("ms", show ms)+ , ("time", time now)+ , ("version", showVersion version)+ , ("xmlns:xsi", "http://www.w3.org/2001/XMLSchema-instance")+ , ("xsi:noNamespaceSchemaLocation", "https://raw.githubusercontent.com/objectionary/eo/refs/heads/gh-pages/XMIR.xsd")+ ]+ <> revisionAttr+ pure+ ( Document+ (Prologue [] Nothing [])+ ( element+ "object"+ attrs+ ( if null pckg+ then [listing'] <> roots+ else [listing', metas] <> roots+ )+ )+ []+ )+ where -- Returns metas Node with package: -- <metas> -- <meta>@@ -252,7 +285,7 @@ -- </meta> -- </metas> metasWithPackage :: String -> Node- metasWithPackage pckg =+ metasWithPackage package = NodeElement ( element "metas"@@ -262,21 +295,20 @@ "meta" [] [ NodeElement (element "head" [] [NodeContent (T.pack "package")])- , NodeElement (element "tail" [] [NodeContent (T.pack pckg)])- , NodeElement (element "part" [] [NodeContent (T.pack pckg)])+ , NodeElement (element "tail" [] [NodeContent (T.pack package)])+ , NodeElement (element "part" [] [NodeContent (T.pack package)]) ] ) ] ) time :: UTCTime -> String- time now =- let base = formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" now- posix = utcTimeToPOSIXSeconds now+ time stamp =+ let base = formatTime defaultTimeLocale "%Y-%m-%dT%H:%M:%S" stamp+ posix = utcTimeToPOSIXSeconds stamp fractional :: Double fractional = realToFrac posix - fromInteger (floor posix) nanos = floor (fractional * 1_000_000_000) :: Int in base ++ "." ++ printf "%09d" nanos ++ "Z"-expressionToXMIR expr _ = throwIO (UnsupportedTopExpression expr) escapeXML :: String -> String escapeXML = concatMap escapeChar@@ -390,15 +422,30 @@ parseXMIRThrows :: String -> IO Document parseXMIRThrows xmir = orThrow CouldNotParseXMIR (parseXMIR xmir) +-- Children of <object> that no document may carry: processing instructions+-- and bare text. Comments, the listing and the <o> bindings are legitimate;+-- anything else makes the element unrenderable back to 𝜑, so the reader+-- rejects the document whole (the cursor is shown by the error verbatim)+strayNodes :: C.Cursor -> [Node]+strayNodes doc = filter bad (map C.node (C.child doc))+ where+ bad :: Node -> Bool+ bad (NodeInstruction _) = True+ bad (NodeContent t) = not (T.null (T.strip t))+ bad _ = False+ xmirToPhi :: Document -> IO Expression xmirToPhi xmir = let doc = C.fromDocument xmir in case C.node doc of NodeElement el | nameLocalName (elementName el) == "object" -> do- obj <- case doc C.$/ C.element (toName "o") of- [o] -> xmirToFormationBinding o []- _ -> throwIO (InvalidXMIRFormat "Expected single <o> element in <object>" doc)+ unless (null (strayNodes doc)) (throwIO (InvalidXMIRFormat "No processing instructions or bare text are allowed in <object>" doc))+ bds <- case doc C.$/ C.element (toName "o") of+ [] -> throwIO (InvalidXMIRFormat "Expected at least one <o> element in <object>" doc)+ -- A residual document (printed by '--partial', #1076) carries+ -- one <o> per binding of the stuck formation, so read them all+ os -> uniqueBindings' =<< mapM (`xmirToFormationBinding` []) os let pckg = [ T.unpack t | meta <- doc C.$/ C.element (toName "metas") C.&/ C.element (toName "meta")@@ -408,10 +455,12 @@ , t <- T.splitOn "." tail' ] if null pckg- then pure (ExFormation [obj, BiVoid AtRho])- else- let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda (Function "Package"), BiVoid AtRho])) obj pckg- in pure (ExFormation [bd, BiVoid AtRho])+ then pure (ExFormation (withVoidRho bds))+ else case bds of+ [obj] ->+ let bd = foldr (\part acc -> BiTau (AtLabel (T.pack part)) (ExFormation [acc, BiLambda (Function "Package"), BiVoid AtRho])) obj pckg+ in pure (ExFormation [bd, BiVoid AtRho])+ _ -> throwIO (InvalidXMIRFormat "A <object> with <metas> package must hold a single <o>" doc) | otherwise -> throwIO (InvalidXMIRFormat "Expected single <object> element" doc) _ -> throwIO (InvalidXMIRFormat "NodeElement is expected as root element" doc)
test/CLISpec.hs view
@@ -1266,6 +1266,22 @@ withStdin "[[ bytes ↦ ⟦ φ ↦ ∅ ⟧, number(φ) -> [[ plus(x) -> [[ L> L_number_plus ]] ]], @ -> 5.plus(6) ]]" $ testCLISucceeded ["dataize", atoms, "--partial"] ["40-26-00-00-00-00-00-00"] + -- The residual is an arbitrary formation, and a multi-binding <object>+ -- is exactly what XMIR now carries: one <o> per binding (#1076)+ it "prints the residual to XMIR, with its real listing by default" $+ withAtoms $ \atoms ->+ withStdin stuck $+ testCLISucceeded+ ["dataize", atoms, "--partial", "--output=xmir"]+ ["<o name=\"λ\">L_number_nope</o>", "<o name=\"ρ\">", "<listing>⟦"]++ it "honors --hide-rho and --omit-listing when printing the residual to XMIR" $+ withAtoms $ \atoms ->+ withStdin stuck $+ testCLISucceeded+ ["dataize", atoms, "--partial", "--output=xmir", "--hide-rho", "--omit-listing"]+ ["<o name=\"λ\">L_number_nope</o>", "line(s)</listing>"]+ it "prints the chain of steps ending in the residue with --sequence" $ withAtoms $ \atoms -> withStdin stuck $
test/XMIRSpec.hs view
@@ -21,7 +21,7 @@ import GHC.Generics (Generic) import Parser (parseExpressionThrows) import System.FilePath (makeRelative)-import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldReturn, shouldThrow)+import Test.Hspec (Spec, anyException, describe, expectationFailure, it, runIO, shouldBe, shouldContain, shouldNotContain, shouldReturn, shouldThrow) import Text.XML (Document (..), Element (..), Node (NodeElement), Prologue (..)) import Text.XML.Cursor qualified as C import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirToPhi)@@ -208,12 +208,34 @@ xmir'' `shouldBe` phi'' ) + -- A '--partial' residual tops in an arbitrary formation: several bindings,+ -- voids, a bound ρ. Such a top now prints to XMIR and reads back whole (#1076)+ describe "round-trips non-program tops as XMIR (#1076)" $+ forM_+ [ "[[ x -> ? ]]"+ , "[[ ^ -> 5 ]]"+ , "[[ x -> 4, L> L_number_plus, ^ -> [[ y -> 5 ]] ]]"+ ]+ ( \phi' -> it phi' $ do+ expr <- parseExpressionThrows phi'+ doc <- expressionToXMIR expr defaultXmirContext+ doc' <- parseXMIRThrows (printXMIR doc)+ back <- xmirToPhi doc'+ back `shouldBe` expr+ )++ describe "--hide-rho in XMIR" $+ it "drops every bound ρ from the printed document" $ do+ expr <- parseExpressionThrows "[[ x -> 4, ^ -> [[ y -> 5 ]] ]]"+ doc <- expressionToXMIR expr (XmirContext True False True (const ""))+ let printed = printXMIR doc+ printed `shouldContain` "name=\"x\""+ printed `shouldNotContain` "name=\"ρ\""+ describe "prohibit to convert to XMIR" $ forM_ [ "[[ ]]" , "T"- , "[[ x -> ? ]]"- , "[[ ^ -> 5 ]]" , "Q.x.y.z" , "\"Hello\"" , "Q"@@ -330,7 +352,7 @@ describe "XMIR comments" $ do let commentedContext :: XmirContext- commentedContext = XmirContext True False (const "")+ commentedContext = XmirContext True False False (const "") it "includes a decimal comment for a number when comments aren't omitted" $ do expr <- parseExpressionThrows "[[ x -> 5 ]]"