phino 0.0.136 → 0.0.137

raw patch · 7 files changed

+111/−40 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +1/−1
• phino.cabal +1/−1
• src/CLI/Helpers.hs +11/−1
• src/CLI/Runners.hs +14/−14
• src/XMIR.hs +48/−17
• test/CLISpec.hs +13/−0
• test/XMIRSpec.hs +23/−6

@@ -34,7 +34,7 @@  ```bash cabal update-cabal install --overwrite-policy=always phino-0.0.135+cabal install --overwrite-policy=always phino-0.0.136 phino --version ``` 

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

@@ -3,6 +3,7 @@ {-# LANGUAGE OverloadedRecordDot #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-}  module CLI.Helpers where @@ -16,6 +17,7 @@ import Data.Functor ((<&>)) import Data.IORef import Data.List (intercalate, nub)+import qualified Data.Map.Strict as M import Data.Maybe import qualified Data.Text as T import Deps (Evaluation (EvRun), Judgment, SaveEvalFunc, SaveStepFunc, State (..), dontSaveEval, emptyNesting, emptyProtocol, endEvalXml, saveEval, saveEvalXml, saveStep)@@ -37,7 +39,7 @@ import System.FilePath (takeDirectory, takeExtension) import System.IO (Handle, IOMode (WriteMode), getContents', hClose, hSetEncoding, openFile, utf8) import Text.Printf (printf)-import XMIR (expressionToXMIR, parseXMIRThrows, printXMIR, xmirToPhi)+import XMIR (Atoms, expressionToXMIR, parseXMIRThrows, printXMIR, xmirAtoms, xmirToPhi) import Yaml (normalizationRules) import qualified Yaml as Y @@ -181,6 +183,14 @@ parseInput phi PHI = parseExpressionThrows phi parseInput xmir XMIR = parseXMIRThrows xmir >>= xmirToPhi parseInput _ LATEX = invalidCLIArguments "LaTeX cannot be used as input format"++-- Parse expression like 'parseInput' does, together with the result types+-- the atoms of an XMIR input carry, which the XMIR writer restores (#1389)+parseInputWithAtoms :: String -> IOFormat -> IO (Expression, Atoms)+parseInputWithAtoms xmir XMIR = do+  doc <- parseXMIRThrows xmir+  (,) <$> xmirToPhi doc <*> xmirAtoms doc+parseInputWithAtoms input format = (,M.empty) <$> parseInput input format  -- The LaTeX sequence path canonizes inside 'rewrittensToLatex', after the meet -- compression (see 'canonizedRewrittens' there); the remaining formats have no

@@ -59,7 +59,7 @@   rules <- getRules _normalize _shuffle _rules   validateBreakpoint _breakpoint rules   input <- readInput _inputFile-  expr <- parseInput input _inputFormat+  (expr, atoms) <- parseInputWithAtoms input _inputFormat   validateXmirTopLevel _outputFormat expr   seedTaus expr   logDebug (printf "Amount of rewriting cycles across all the rules: %d, per rule: %d" _maxCycles _maxDepth)@@ -67,7 +67,7 @@         ([], XMIR, XMIR) -> (\_ -> escapeXML input)         ([], _, _) -> (\_ -> escapeXMLText input)         (_, _, _) -> (\rewritten -> escapeXMLText (P.printExpression' rewritten (_sugarType, UNICODE, _flat, _margin)))-      xmirCtx = XmirContext _omitListing _omitComments _hideRho listing+      xmirCtx = XmirContext _omitListing _omitComments _hideRho listing atoms       printCtx = toPrintCtx xmirCtx foc       exclude = (`F.exclude` excluded)       include = (`F.include` included)@@ -157,10 +157,10 @@   [foc] <- validatedDispatches "focus" [_focus]   validateNoOverlap "show" included "hide" excluded   input <- readInput _inputFile-  expr <- parseInput input _inputFormat+  (expr, atoms) <- parseInputWithAtoms input _inputFormat   setStdGen (mkStdGen _seed)   seedTaus expr-  let printCtx = toPrintCtx foc+  let printCtx = toPrintCtx atoms foc       exclude = (`F.exclude` excluded)       include = (`F.include` included)   save <- saveStepFunc _stepsDir printCtx@@ -201,14 +201,14 @@       when         (isJust _inside && _locator /= "Q")         (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")-    toPrintCtx :: Expression -> PrintContext-    toPrintCtx focus =+    toPrintCtx :: Atoms -> Expression -> PrintContext+    toPrintCtx atoms focus =       PrintCtx         _sugarType         _hideRho         _flat         _margin-        (XmirContext _omitListing _omitComments _hideRho listing)+        (XmirContext _omitListing _omitComments _hideRho listing atoms)         _nonumber         _compress         _canonize@@ -243,10 +243,10 @@   [foc] <- validatedDispatches "focus" [_focus]   validateNoOverlap "show" included "hide" excluded   input <- readInput _inputFile-  expr <- parseInput input _inputFormat+  (expr, atoms) <- parseInputWithAtoms input _inputFormat   setStdGen (mkStdGen _seed)   seedTaus expr-  let printCtx = toPrintCtx foc+  let printCtx = toPrintCtx atoms foc       exclude = (`F.exclude` excluded)       include = (`F.include` included)   save <- saveStepFunc _stepsDir printCtx@@ -275,14 +275,14 @@       when         (isJust _inside && _locator /= "Q")         (invalidCLIArguments "The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")-    toPrintCtx :: Expression -> PrintContext-    toPrintCtx focus =+    toPrintCtx :: Atoms -> Expression -> PrintContext+    toPrintCtx atoms focus =       PrintCtx         _sugarType         _hideRho         _flat         _margin-        (XmirContext _omitListing _omitComments _hideRho listing)+        (XmirContext _omitListing _omitComments _hideRho listing atoms)         _nonumber         _compress         _canonize@@ -329,11 +329,11 @@   validateOpts   inputs' <- traverse (readInput . Just) _inputs   setStdGen (mkStdGen _seed)-  exprs <- traverse (`parseInput` _inputFormat) inputs'+  (exprs, atoms) <- unzip <$> traverse (`parseInputWithAtoms` _inputFormat) inputs'   expr <- merge exprs   validateXmirTopLevel _outputFormat expr   let listing = const (escapeXMLText (P.printExpression' expr (_sugarType, UNICODE, _flat, _margin)))-      xmirCtx = XmirContext _omitListing _omitComments False listing+      xmirCtx = XmirContext _omitListing _omitComments False listing (Map.unions atoms)       printCtx = toPrintCtx xmirCtx   expr' <- printInFormat printCtx expr   printOut _targetFile expr'

@@ -14,6 +14,8 @@   , parseXMIR   , parseXMIRThrows   , xmirToPhi+  , xmirAtoms+  , Atoms   , defaultXmirContext   , escapeXML   , escapeXMLText@@ -52,8 +54,14 @@   , _omitComments :: Bool   , _hideRho :: Bool   , _listing :: Expression -> String+  , _atoms :: Atoms   } +-- The result type an atom of the EO parser carries in its @atom attribute,+-- like 'Φ.number', keyed by the name of its λ function. The type is no name+-- phino can read, so it lives beside the λ binding and not in it (#1389)+type Atoms = M.Map T.Text String+ -- The 7-character Git SHA of the phino build that produced the document, -- matching the XMIR schema pattern [0-9a-f]{7}. When built outside a git -- checkout gitrev yields "UNKNOWN", which the schema allows us to omit.@@ -61,7 +69,7 @@ gitRevision = take 7 $(gitHash)  defaultXmirContext :: XmirContext-defaultXmirContext = XmirContext True True False (const "")+defaultXmirContext = XmirContext True True False (const "") M.empty  data XMIRException   = UnsupportedTopExpression Expression@@ -160,9 +168,8 @@ formationBinding (BiTau AtRho expr) ctx = Just <$> namedBinding (show AtRho) expr ctx formationBinding (BiTau AtPhi expr) ctx = Just <$> namedBinding (show AtPhi) expr ctx formationBinding (BiDelta bytes) _ = pure (Just (NodeContent (T.pack (printBytes bytes))))-formationBinding (BiLambda (Function name)) _-  | "Φ." `T.isPrefixOf` name = pure (Just (object [("atom", T.unpack name), ("name", show AtLambda)] []))-  | otherwise = pure (Just (object [("name", show AtLambda)] [NodeContent name]))+formationBinding (BiLambda (Function name)) XmirContext{..} =+  pure (Just (object (maybe [] (\atom -> [("atom", atom)]) (M.lookup name _atoms) ++ [("name", show AtLambda)]) [NodeContent name])) formationBinding (BiVoid AtRho) _ = pure Nothing formationBinding (BiVoid AtPhi) _ = pure (Just (object [("name", show AtPhi), ("base", "∅")] [])) formationBinding (BiVoid (AtLabel label)) _ = pure (Just (object [("name", T.unpack label), ("base", "∅")] []))@@ -483,7 +490,7 @@   | not (hasAttr "base" cur) = do       name <- getAttr "name" cur       case name of-        "λ" -> BiLambda . Function <$> atomOrLambda+        "λ" -> BiLambda . Function <$> lambdaName cur fqn         ('α' : _) -> throwIO (InvalidXMIRFormat "Formation child @name can't start with α" cur)         "φ" -> BiTau AtPhi <$> xmirToFormation cur (name : fqn)         "ρ" -> BiTau AtRho <$> xmirToFormation cur (name : fqn)@@ -501,24 +508,48 @@         _ -> do           expr <- xmirToExpression cur fqn           pure (BiTau attr expr)-  where-    -- The λ function name is carried by the text of the marker element. XMIR-    -- coming from elsewhere holds no name, so fall back to the position in the-    -- tree, which is the only hint left-    atomOrLambda :: IO T.Text-    atomOrLambda-      | hasAttr "atom" cur = T.pack <$> getAttr "atom" cur-      | otherwise = lambdaFunction -    lambdaFunction :: IO T.Text-    lambdaFunction-      | hasText cur = T.strip . T.pack <$> getText cur-      | otherwise = pure (T.pack (intercalate "_" ("L" : map (map spell) (reverse fqn))))+-- The λ function name is carried by the text of the marker element. XMIR+-- coming from elsewhere holds no name, so fall back to the position in the+-- tree, which is the only hint left. The @atom attribute the EO parser writes+-- is the result type of the atom and never its name (#1389)+lambdaName :: C.Cursor -> [String] -> IO T.Text+lambdaName cur fqn+  | hasText cur = T.strip . T.pack <$> getText cur+  | otherwise = pure (T.pack (intercalate "_" ("L" : map (map spell) (reverse fqn))))+  where     -- A binding label admits nearly any character, while 'function' admits a     -- digit, an ASCII lowercase letter, '_' and 'φ' only, so everything else     -- folds into '_' and the derived name stays readable back (#1188)     spell :: Char -> Char     spell ch = if isDigit ch || isAsciiLower ch || ch == '_' || ch == 'φ' then ch else '_'++-- The result types of the atoms in a document, keyed by the names 'xmirToPhi'+-- gives their λ functions, so that 'expressionToXMIR' writes them back (#1389).+-- The reader grows the locator of a λ marker by every formation it descends+-- into, that is by every enclosing <o> with @name and neither @base nor @as+xmirAtoms :: Document -> IO Atoms+xmirAtoms xmir = M.fromList <$> mapM entry markers+  where+    markers :: [C.Cursor]+    markers =+      C.fromDocument xmir+        C.$// C.element (toName "o")+        C.>=> C.attributeIs (toName "name") "λ"+        C.>=> C.check (hasAttr "atom")+    entry :: C.Cursor -> IO (T.Text, String)+    entry cur = do+      name <- lambdaName cur (locator cur)+      atom <- getAttr "atom" cur+      pure (name, atom)+    locator :: C.Cursor -> [String]+    locator cur =+      [ T.unpack label+      | enclosing <- cur C.$| (C.ancestor C.>=> C.element (toName "o"))+      , not (hasAttr "base" enclosing)+      , not (hasAttr "as" enclosing)+      , label <- C.attribute (toName "name") enclosing+      ]  -- A formation keeps its Δ data in the text content of its own element, the way -- the printer emits a Δ binding, while the rest of the bindings live in the

@@ -2481,6 +2481,19 @@         ["merge", resource "desugar.phi", "--output=xmir"]         ["<?xml version=\"1.0\" encoding=\"UTF-8\"?>", "<listing>⟦ foo ↦ ξ.x, ρ ↦ ∅ ⟧</listing>", "<o base=\"ξ.x\" name=\"foo\"/>"] +    -- The @atom of an EO atom is its result type, not the name of its λ+    -- function, so the merged 𝜑 names the function after its locator and+    -- the XMIR printed back restores the type (#1389)+    it "names an atom of XMIR after its locator and keeps its type" $ do+      let xmir = "<object><o name=\"number\"><o name=\"plus\"><o base=\"∅\" name=\"b\"/><o atom=\"Φ.number\" name=\"λ\"/></o></o></object>"+      withTempFileContent "phino-atom.xmir" xmir $ \file -> do+        testCLISucceeded+          ["merge", "--input=xmir", "--sweet", "--flat", file]+          ["λ ⤍ L_number_plus"]+        testCLISucceeded+          ["merge", "--input=xmir", "--output=xmir", file]+          ["<o atom=\"Φ.number\" name=\"λ\">L_number_plus</o>"]+     it "reproduces the same output for the same --seed" $ do       let args =             [ "merge"

@@ -25,7 +25,7 @@ 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)+import XMIR (XmirContext (XmirContext), defaultXmirContext, escapeXML, expressionToXMIR, parseXMIRThrows, printXMIR, toName, xmirAtoms, xmirToPhi)  data ParsePack = ParsePack   { failure :: Maybe Bool@@ -233,19 +233,36 @@       expr <- xmirToPhi doc       parseExpressionThrows (printExpression expr) `shouldReturn` expr -  describe "atom result types in XMIR" $+  describe "atom result types in XMIR" $ do+    let atom :: String+        atom = "<object><o name=\"number\"><o name=\"plus\"><o base=\"∅\" name=\"b\"/><o atom=\"Φ.number\" name=\"λ\"/></o></o></object>"     it "survives a round trip through a λ marker" $ do-      doc <- parseXMIRThrows "<object><o name=\"bar\"><o base=\"∅\" name=\"x\"/><o atom=\"Φ.number\" name=\"λ\"/></o></object>"+      doc <- parseXMIRThrows atom       expr <- xmirToPhi doc-      result <- expressionToXMIR expr defaultXmirContext+      atoms <- xmirAtoms doc+      result <- expressionToXMIR expr (XmirContext True True False (const "") atoms)       let printed = printXMIR result       printed `shouldContain` "atom=\"Φ.number\""       printed `shouldNotContain` "<o name=\"λ\">"+    -- The @atom attribute is the result type of the atom, not its name, so+    -- the λ function is still named after its locator (#1389)+    it "names the λ function after its locator, not after the type" $ do+      expr <- parseXMIRThrows atom >>= xmirToPhi+      printExpression expr `shouldContain` "L_number_plus"+      printExpression expr `shouldNotContain` "Φ.number"+      parseExpressionThrows (printExpression expr) `shouldReturn` expr+    it "keeps the type keyed by the λ function name" $+      (parseXMIRThrows atom >>= xmirAtoms) `shouldReturn` M.fromList [("L_number_plus", "Φ.number")]+    it "keeps the type of a λ marker that carries its name" $+      ( parseXMIRThrows "<object><o name=\"x\"><o atom=\"?\" name=\"λ\">Foo</o></o></object>"+          >>= xmirAtoms+      )+        `shouldReturn` M.fromList [("Foo", "?")]    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 ""))+      doc <- expressionToXMIR expr (XmirContext True False True (const "") M.empty)       let printed = printXMIR doc       printed `shouldContain` "name=\"x\""       printed `shouldNotContain` "name=\"ρ\""@@ -371,7 +388,7 @@    describe "XMIR comments" $ do     let commentedContext :: XmirContext-        commentedContext = XmirContext True False False (const "")+        commentedContext = XmirContext True False False (const "") M.empty      it "includes a decimal comment for a number when comments aren't omitted" $ do       expr <- parseExpressionThrows "[[ x -> 5 ]]"