phino-0.0.124: src/XMIR.hs

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TemplateHaskell #-}

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

module XMIR
  ( expressionToXMIR
  , printXMIR
  , toName
  , parseXMIR
  , parseXMIRThrows
  , xmirToPhi
  , defaultXmirContext
  , escapeXML
  , escapeXMLText
  , XmirContext (XmirContext)
  )
where

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)
import qualified Data.Map as M
import Data.Maybe (catMaybes)
import qualified Data.Text as T
import qualified Data.Text.Lazy as TL
import qualified Data.Text.Lazy.Builder as TB
import Data.Time (UTCTime, diffUTCTime, getCurrentTime)
import Data.Time.Clock.POSIX (utcTimeToPOSIXSeconds)
import Data.Time.Format (defaultTimeLocale, formatTime)
import Data.Version (showVersion)
import Development.GitRev (gitHash)
import Misc
import Paths_phino (version)
import Printer
import Text.Printf (printf)
import qualified Text.Read as TR
import Text.XML
import qualified Text.XML.Cursor as C

data XmirContext = XmirContext
  { _omitListing :: Bool
  , _omitComments :: Bool
  , _hideRho :: Bool
  , _listing :: Expression -> 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.
gitRevision :: String
gitRevision = take 7 $(gitHash)

defaultXmirContext :: XmirContext
defaultXmirContext = XmirContext True True False (const "")

data XMIRException
  = UnsupportedTopExpression Expression
  | UnsupportedExpression Expression
  | UnsupportedBinding Binding
  | CouldNotParseXMIR String
  | InvalidXMIRFormat String C.Cursor
  deriving (Exception)

instance Show XMIRException where
  show (UnsupportedTopExpression expr) = printf "XMIR does not support such top-level expression:\n%s" (printExpression expr)
  show (UnsupportedExpression expr) = printf "XMIR does not support such expression:\n%s" (printExpression expr)
  show (UnsupportedBinding bd) = printf "XMIR does not support such bindings: %s" (printBinding bd)
  show (CouldNotParseXMIR msg) = printf "Couldn't parse given XMIR, cause: %s" msg
  show (InvalidXMIRFormat msg cur) =
    printf
      "Couldn't traverse though given XMIR, cause: %s\nXMIR:\n%s"
      msg
      ( case C.node cur of
          NodeElement el -> printXMIR (Document (Prologue [] Nothing []) el [])
          _ -> "Unknown"
      )

toName :: String -> Name
toName str = Name (T.pack str) Nothing Nothing

element :: String -> [(String, String)] -> [Node] -> Element
element name attrs children =
  let name' = toName name
      attrs' = M.fromList (map (bimap toName T.pack) attrs)
   in Element name' attrs' children

object :: [(String, String)] -> [Node] -> Node
object attrs children = NodeElement (element "o" attrs children)

expression :: Expression -> XmirContext -> IO (String, [Node])
expression ExXi _ = pure (printExpression ExXi, [])
expression ExRoot _ = pure (printExpression ExRoot, [])
expression ExTermination _ = pure ("⊥", [])
expression (ExFormation bds) ctx = do
  nested <- nestedBindings bds ctx
  pure ("", nested)
expression (ExDispatch expr attr) ctx = do
  (base, children) <- expression expr ctx
  let attr' = printAttribute attr
  case base of
    [] -> pure ('.' : attr', [object [] children])
    ch : _ ->
      if ch == '.' || not (null children)
        then pure ('.' : attr', [object [("base", base)] children])
        else pure (base ++ ('.' : attr'), children)
expression (DataNumber bytes) XmirContext{..} =
  let bts =
        object
          [("as", "φ"), ("base", "Φ.bytes")]
          [object [("as", "φ")] [NodeContent (T.pack (printBytes bytes))]]
   in pure
        ( "Φ.number"
        , if _omitComments || btsSize bytes /= 8
            then [bts]
            else
              [ NodeComment (T.pack (either show show (btsToNum bytes)))
              , bts
              ]
        )
expression (DataString bytes) XmirContext{..} =
  let bts =
        object
          [("as", "φ"), ("base", "Φ.bytes")]
          [object [("as", "φ")] [NodeContent (T.pack (printBytes bytes))]]
   in pure
        ( "Φ.string"
        , if _omitComments || not (btsIsUtf8 bytes)
            then [bts]
            else
              [ NodeComment (T.pack ('"' : btsToStr bytes ++ "\""))
              , bts
              ]
        )
expression (ExApplication expr arg) ctx = do
  (base, children) <- expression expr ctx
  (base', children') <- expression texpr ctx
  let attrs =
        if null base'
          then [("as", as)]
          else [("as", as), ("base", base')]
  pure (base, children ++ [object attrs children'])
  where
    (as, texpr) = case arg of
      ArTau attr value -> (printAttribute attr, value)
      ArAlpha alpha value -> (printAlpha alpha, value)
expression expr _ = throwIO (UnsupportedExpression expr)

formationBinding :: Binding -> XmirContext -> IO (Maybe Node)
formationBinding (BiTau (AtLabel label) expr) ctx = Just <$> namedBinding (T.unpack label) expr ctx
formationBinding (BiTau AtRho expr) ctx = Just <$> namedBinding (show AtRho) expr ctx
formationBinding (BiTau AtPhi expr) ctx = do
  (base, children) <- expression expr ctx
  pure (Just (object [("name", show AtPhi), ("base", base)] children))
formationBinding (BiDelta bytes) _ = pure (Just (NodeContent (T.pack (printBytes bytes))))
formationBinding (BiLambda (Function name)) _ = pure (Just (object [("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", "∅")] []))
formationBinding binding _ = throwIO (UnsupportedBinding binding)

-- Render a bound attribute as a named element: a formation nests its bindings
-- right inside it, while any other expression is carried by the @base attribute
namedBinding :: String -> Expression -> XmirContext -> IO Node
namedBinding name (ExFormation bds) ctx = object [("name", name)] <$> nestedBindings bds ctx
namedBinding name expr ctx = do
  (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@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 = 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
    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
    -- - Y: root object expression
    getPackage :: Expression -> IO ([String], Expression)
    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]), BiVoid AtRho]) = do
      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho])
      pure (T.unpack label : pckg, expr')
    getPackage (ExFormation [BiTau (AtLabel label) (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho]), BiLambda (Function "Package"), BiVoid AtRho]) = do
      (pckg, expr') <- getPackage (ExFormation [bd, BiLambda (Function "Package"), BiVoid AtRho])
      pure (T.unpack label : pckg, expr')
    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)))
    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>
    --     <head>package</head>
    --     <tail><!-- package here --></tail>
    --     <part><!-- package here --></part>
    --   </meta>
    -- </metas>
    metasWithPackage :: String -> Node
    metasWithPackage package =
      NodeElement
        ( element
            "metas"
            []
            [ NodeElement
                ( element
                    "meta"
                    []
                    [ NodeElement (element "head" [] [NodeContent (T.pack "package")])
                    , NodeElement (element "tail" [] [NodeContent (T.pack package)])
                    , NodeElement (element "part" [] [NodeContent (T.pack package)])
                    ]
                )
            ]
        )
    time :: UTCTime -> String
    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"

escapeXML :: String -> String
escapeXML = concatMap escapeChar
  where
    escapeChar :: Char -> String
    escapeChar '&' = "&amp;"
    escapeChar '<' = "&lt;"
    escapeChar '>' = "&gt;"
    escapeChar '"' = "&quot;"
    escapeChar '\'' = "&apos;"
    escapeChar ch = [ch]

-- Escape just the characters that are mandatory in XML text content ('&' and
-- '<'); '>' and the quotes are optional there and staying literal keeps the
-- content readable, e.g. the '->' arrow inside a <listing>.
escapeXMLText :: String -> String
escapeXMLText = concatMap escapeChar
  where
    escapeChar :: Char -> String
    escapeChar '&' = "&amp;"
    escapeChar '<' = "&lt;"
    escapeChar ch = [ch]

-- Add indentation (2 spaces per level).
indent :: Int -> TB.Builder
indent n = TB.fromText (T.replicate n (T.pack "  "))

newline' :: Bool -> TB.Builder
newline' True = newline
newline' False = ""

newline :: TB.Builder
newline = TB.fromString "\n"

-- >>> printElement 0 (element "doc" [("a", ""), ("b", ""), ("c", ""), ("d", ""), ("e", "")] []) True
-- "<doc a=\"\" b=\"\" c=\"\" d=\"\" e=\"\"/>\n"
printElement :: Int -> Element -> Bool -> TB.Builder
printElement indentLevel (Element name attrs nodes) eol
  | null nodes =
      indent indentLevel
        <> TB.fromString "<"
        <> TB.fromText (nameLocalName name)
        <> attrsText
        <> TB.fromString "/>"
        <> newline' eol
  | all isTextNode nodes =
      indent indentLevel
        <> TB.fromString "<"
        <> TB.fromText (nameLocalName name)
        <> attrsText
        <> TB.fromString ">"
        <> mconcat (map printRawText nodes)
        <> TB.fromString "</"
        <> TB.fromText (nameLocalName name)
        <> TB.fromString ">"
        <> newline' eol
  | otherwise =
      indent indentLevel
        <> TB.fromString "<"
        <> TB.fromText (nameLocalName name)
        <> attrsText
        <> TB.fromString ">"
        <> newline
        <> mconcat (map (printNode (indentLevel + 1)) nodes)
        <> indent indentLevel
        <> TB.fromString "</"
        <> TB.fromText (nameLocalName name)
        <> TB.fromString ">"
        <> newline' eol
  where
    attrsText =
      mconcat
        [ TB.fromString " " <> TB.fromText (nameLocalName k) <> TB.fromString "=\"" <> TB.fromText (T.pack (escapeXML (T.unpack v))) <> TB.fromString "\""
        | (k, v) <- M.toList attrs
        ]

    isTextNode (NodeContent _) = True
    isTextNode _ = False

    printRawText (NodeContent t) = TB.fromText t
    printRawText _ = mempty

-- >>> printNode 0 (NodeComment (T.pack "--hello--"))
-- "<!-- &#45;&#45;hello&#45;&#45; -->\n"
printNode :: Int -> Node -> TB.Builder
printNode _ (NodeContent t) = TB.fromText t -- print text exactly as-is
printNode i (NodeElement e) = printElement i e True -- pretty-print elements
printNode i (NodeComment t) =
  indent i
    <> TB.fromString "<!-- "
    <> TB.fromText (T.replace "--" "&#45;&#45;" t)
    <> TB.fromString " -->"
    <> newline
printNode _ _ = mempty

printXMIR :: Document -> String
printXMIR (Document _ root _) =
  TL.unpack
    ( TB.toLazyText
        ( TB.fromString "<?xml version=\"1.0\" encoding=\"UTF-8\"?>"
            <> newline
            <> printElement 0 root False
        )
    )

parseXMIR :: String -> Either String Document
parseXMIR xmir = case parseText def (TL.pack xmir) of
  Right doc -> Right doc
  Left err -> Left (displayException err)

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
              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")
                    , let heads = meta C.$/ C.element (toName "head") C.&/ C.content
                    , heads == ["package"]
                    , tail' <- meta C.$/ C.element (toName "tail") C.&/ C.content
                    , t <- T.splitOn "." tail'
                    ]
              if null pckg
                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)

xmirToFormationBinding :: C.Cursor -> [String] -> IO Binding
xmirToFormationBinding cur fqn
  | not (hasAttr "name" cur) = throwIO (InvalidXMIRFormat "Formation children must have @name attribute" cur)
  | not (hasAttr "base" cur) = do
      name <- getAttr "name" cur
      case name of
        "λ" -> BiLambda . Function <$> lambdaFunction
        ('α' : _) -> throwIO (InvalidXMIRFormat "Formation child @name can't start with α" cur)
        "φ" -> BiTau AtPhi <$> xmirToFormation cur (name : fqn)
        "ρ" -> BiTau AtRho <$> xmirToFormation cur (name : fqn)
        _ -> BiTau (AtLabel (T.pack name)) <$> xmirToFormation cur (name : fqn)
  | otherwise = do
      name <- getAttr "name" cur
      base <- getAttr "base" cur
      attr <- case name of
        "φ" -> pure AtPhi
        "ρ" -> pure AtRho
        ('α' : _) -> throwIO (InvalidXMIRFormat "Formation child @name can't start with α" cur)
        _ -> pure (AtLabel (T.pack name))
      case base of
        "∅" -> pure (BiVoid attr)
        _ -> 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
    lambdaFunction :: IO T.Text
    lambdaFunction
      | hasText cur = T.strip . T.pack <$> getText cur
      | otherwise = pure (T.pack (intercalate "_" ("L" : reverse fqn)))

-- 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
-- nested <o> elements
xmirToFormation :: C.Cursor -> [String] -> IO Expression
xmirToFormation cur fqn = do
  nested <- mapM (`xmirToFormationBinding` fqn) (cur C.$/ C.element (toName "o"))
  bds <- if hasText cur then (: nested) <$> delta else pure nested
  ExFormation . withVoidRho <$> uniqueBindings' bds
  where
    delta :: IO Binding
    delta = BiDelta . bytesToBts . T.unpack . T.strip . T.pack <$> getText cur

xmirToExpression :: C.Cursor -> [String] -> IO Expression
xmirToExpression cur fqn
  | hasAttr "base" cur = do
      base <- getAttr "base" cur
      case base of
        '.' : rest ->
          if null rest
            then throwIO (InvalidXMIRFormat "The @base attribute can't be just '.'" cur)
            else
              let args = cur C.$/ C.element (toName "o")
               in case args of
                    [] -> throwIO (InvalidXMIRFormat (printf "Element with @base='%s' must have at least one child" base) cur)
                    arg : args' -> do
                      expr <- xmirToExpression arg fqn
                      attr <- toAttr rest cur
                      let disp = ExDispatch expr attr
                      xmirToApplication disp args' fqn
        "ξ" ->
          if null (cur C.$/ C.element (toName "o"))
            then pure ExXi
            else throwIO (InvalidXMIRFormat "Application of 'ξ' is illegal in XMIR" cur)
        "Φ" ->
          if null (cur C.$/ C.element (toName "o"))
            then pure ExRoot
            else throwIO (InvalidXMIRFormat "Application of 'Φ' is illegal in XMIR" cur)
        "⊥" -> xmirToApplication ExTermination (cur C.$/ C.element (toName "o")) fqn
        'Φ' : '.' : rest -> xmirToExpression' ExRoot "Φ" rest cur fqn
        'ξ' : '.' : rest -> xmirToExpression' ExXi "ξ" rest cur fqn
        _ -> throwIO (InvalidXMIRFormat "The @base attribute must be either ['∅'|'Φ'] or start with ['Φ.'|'ξ.'|'.']" cur)
  | otherwise = xmirToFormation cur fqn
  where
    xmirToExpression' :: Expression -> String -> String -> C.Cursor -> [String] -> IO Expression
    xmirToExpression' start symbol rst c names =
      if null rst
        then throwIO (InvalidXMIRFormat (printf "The @base='%s.' is illegal in XMIR" symbol) c)
        else do
          head' <-
            foldlM
              (\acc part -> ExDispatch acc <$> toAttr (T.unpack part) c)
              start
              (T.splitOn "." (T.pack rst))
          xmirToApplication head' (c C.$/ C.element (toName "o")) names

xmirToApplication :: Expression -> [C.Cursor] -> [String] -> IO Expression
xmirToApplication = xmirToApplication' 0
  where
    xmirToApplication' :: Int -> Expression -> [C.Cursor] -> [String] -> IO Expression
    xmirToApplication' _ expr [] _ = pure expr
    xmirToApplication' idx expr (arg : args) fqn = do
      let app
            | hasAttr "name" arg = throwIO (InvalidXMIRFormat "Application argument can't have @name attribute" arg)
            | hasAttr "base" arg && hasText arg = throwIO (InvalidXMIRFormat "It's illegal in XMIR to have @base and text() at the same time" arg)
            | not (hasAttr "base" arg) && not (hasText arg) = do
                bds <- mapM (`xmirToFormationBinding` fqn) (arg C.$/ C.element (toName "o"))
                key <- asToKey arg idx
                pure (ExApplication expr (mkArg key (ExFormation (withVoidRho bds))))
            | not (hasAttr "base" arg) && hasText arg = do
                key <- asToKey arg idx
                bytes <- getText arg
                pure (ExApplication expr (mkArg key (ExFormation [BiDelta (bytesToBts bytes), BiVoid AtRho])))
            | otherwise = do
                key <- asToKey arg idx
                arg' <- xmirToExpression arg fqn
                pure (ExApplication expr (mkArg key arg'))
      app' <- app
      xmirToApplication' (idx + 1) app' args fqn
    mkArg :: Either Alpha Attribute -> Expression -> Argument
    mkArg (Left alpha) expr = ArAlpha alpha expr
    mkArg (Right attr) expr = ArTau attr expr
    asToKey :: C.Cursor -> Int -> IO (Either Alpha Attribute)
    asToKey cur position
      | hasAttr "as" cur = do
          as <- getAttr "as" cur
          case as of
            'α' : rest' -> case TR.readMaybe rest' :: Maybe Int of
              Just idx -> pure (Left (Alpha idx))
              Nothing -> throwIO (InvalidXMIRFormat "The attribute started with 'α' must be followed by integer" cur)
            "ρ" -> throwIO (InvalidXMIRFormat "The 'ρ' in @as attribute is illegal in XMIR" cur)
            _ -> Right <$> toAttr as cur
      | otherwise = pure (Left (Alpha position))

toAttr :: String -> C.Cursor -> IO Attribute
toAttr attr cur = case attr of
  "φ" -> pure AtPhi
  "ρ" -> pure AtRho
  'α' : _ -> throwIO (InvalidXMIRFormat "α-index is not a valid dispatch attribute in XMIR" cur)
  ch : _
    | ch `notElem` ['a' .. 'z'] -> throwIO (InvalidXMIRFormat (printf "The attribute '%s' must start with ['a'..'z']" attr) cur)
    | '.' `elem` attr -> throwIO (InvalidXMIRFormat "Attribute can't contain dots" cur)
    | otherwise -> pure (AtLabel (T.pack attr))
  _ -> throwIO (InvalidXMIRFormat (printf "Invalid attribute given: %s" attr) cur)

hasAttr :: String -> C.Cursor -> Bool
hasAttr key cur = not (null (C.attribute (toName key) cur))

getAttr :: String -> C.Cursor -> IO String
getAttr key cur =
  let attrs = C.attribute (toName key) cur
   in case attrs of
        [] -> throwIO (InvalidXMIRFormat (printf "Couldn't find attribute '%s'" key) cur)
        at : _ ->
          let attr = T.unpack at
           in if null attr
                then throwIO (InvalidXMIRFormat (printf "The attribute '%s' is not expected to be empty" attr) cur)
                else pure attr

hasText :: C.Cursor -> Bool
hasText cur = any isNonEmptyTextNode (C.child cur)
  where
    isNonEmptyTextNode cur' = case C.node cur' of
      NodeContent t -> not (T.null (T.strip t)) -- strip to ignore whitespace-only
      _ -> False

getText :: C.Cursor -> IO String
getText cur =
  case [t | c <- C.child cur, NodeContent t <- [C.node c]] of
    (t : _) -> pure (T.unpack t)
    [] -> throwIO (InvalidXMIRFormat "Text content inside <o> element can't be empty" cur)