    -- | Expand environment variables in strings
    module Agda.Utils.Environment ( expandEnvironmentVariables ) where

    import Data.Char
    import Data.Maybe
    import System.Environment
    import System.Directory ( getHomeDirectory )

    expandEnvironmentVariables :: String -> IO String
    expandEnvironmentVariables :: [Char] -> IO [Char]
    expandEnvironmentVariables [Char]
    s = do
      [([Char], [Char])]
    env  <- IO [([Char], [Char])]
    getEnvironment
      [Char]
    home <- IO [Char]
    getHomeDirectory
      [Char] -> IO [Char]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Char] -> IO [Char]) -> [Char] -> IO [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [([Char], [Char])] -> [Char] -> [Char]
    expandVars [Char]
    home [([Char], [Char])]
    env [Char]
    s

    expandVars
      :: String              -- ^ Home directory.
      -> [(String, String)]  -- ^ Environment variable substitution map.
      -> String              -- ^ Input.
      -> String              -- ^ Output with variables and @~@ (home) substituted.
    expandVars :: [Char] -> [([Char], [Char])] -> [Char] -> [Char]
    expandVars [Char]
    home [([Char], [Char])]
    env [Char]
    s = (Token -> [Char]) -> [Token] -> [Char]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Token -> [Char]
    repl ([Token] -> [Char]) -> [Token] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Token]
    tokens [Char]
    s
      where
        repl :: Token -> [Char]
    repl Token
    Home    = [Char]
    home [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "/"
        repl (Var [Char]
    x) = [Char] -> Maybe [Char] -> [Char]
    forall a. a -> Maybe a -> a
    fromMaybe [Char]
    "" (Maybe [Char] -> [Char]) -> Maybe [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [([Char], [Char])] -> Maybe [Char]
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    lookup [Char]
    x [([Char], [Char])]
    env
        repl (Str [Char]
    s) = [Char]
    s

    -- | Tokenization for environment variable substitution.
    data Token
      = Home        -- ^ @~@.
      | Var String  -- ^ @$VARIABLE@ or @${VARIABLE}$.
      | Str String  -- ^ Ordinary characters.
      deriving (Token -> Token -> Bool
    (Token -> Token -> Bool) -> (Token -> Token -> Bool) -> Eq Token
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Token -> Token -> Bool
    $c/= :: Token -> Token -> Bool
    == :: Token -> Token -> Bool
    $c== :: Token -> Token -> Bool
    Eq, Int -> Token -> [Char] -> [Char]
    [Token] -> [Char] -> [Char]
    Token -> [Char]
    (Int -> Token -> [Char] -> [Char])
    -> (Token -> [Char]) -> ([Token] -> [Char] -> [Char]) -> Show Token
    forall a.
    (Int -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    showList :: [Token] -> [Char] -> [Char]
    $cshowList :: [Token] -> [Char] -> [Char]
    show :: Token -> [Char]
    $cshow :: Token -> [Char]
    showsPrec :: Int -> Token -> [Char] -> [Char]
    $cshowsPrec :: Int -> Token -> [Char] -> [Char]
    Show)

    -- | Tokenize a string.
    --   The @~@ is recognized as @$HOME@ only at the beginning of the string.
    tokens :: String -> [Token]
    tokens :: [Char] -> [Token]
    tokens = \case
      Char
    '~'  : Char
    '/' : [Char]
    s -> Token
    Home Token -> [Token] -> [Token]
    forall a. a -> [a] -> [a]
    : [Char] -> [Token]
    tokens' [Char]
    s
      Char
    '\\' : Char
    '~' : [Char]
    s -> Char -> [Token] -> [Token]
    cons Char
    '~' ([Token] -> [Token]) -> [Token] -> [Token]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Token]
    tokens' [Char]
    s
      [Char]
    s -> [Char] -> [Token]
    tokens' [Char]
    s
      where
        tokens' :: String -> [Token]
        tokens' :: [Char] -> [Token]
    tokens' = \case
            Char
    '$' : Char
    '$' : [Char]
    s -> Char -> [Token] -> [Token]
    cons Char
    '$' ([Token] -> [Token]) -> [Token] -> [Token]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Token]
    tokens' [Char]
    s
            Char
    '$' : s :: [Char]
    s@(Char
    c : [Char]
    _) | Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '_' Bool -> Bool -> Bool
    || Char -> Bool
    isAlpha Char
    c -> [Char] -> Token
    Var [Char]
    x Token -> [Token] -> [Token]
    forall a. a -> [a] -> [a]
    : [Char] -> [Token]
    tokens' [Char]
    s'
              where
              ([Char]
    x, [Char]
    s') = (Char -> Bool) -> [Char] -> ([Char], [Char])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (\ Char
    c -> Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '_' Bool -> Bool -> Bool
    || Char -> Bool
    isAlphaNum Char
    c) [Char]
    s
            Char
    '$' : Char
    '{' : [Char]
    s ->
              case (Char -> Bool) -> [Char] -> ([Char], [Char])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '}') [Char]
    s of
                ([Char]
    x, Char
    '}' : [Char]
    s) -> [Char] -> Token
    Var [Char]
    x Token -> [Token] -> [Token]
    forall a. a -> [a] -> [a]
    : [Char] -> [Token]
    tokens' [Char]
    s
                ([Char], [Char])
    _            -> [[Char] -> Token
    Str ([Char] -> Token) -> [Char] -> Token
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "${" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s] -- abort on unterminated '{'
            Char
    c : [Char]
    s -> Char -> [Token] -> [Token]
    cons Char
    c ([Token] -> [Token]) -> [Token] -> [Token]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Token]
    tokens' [Char]
    s
            [Char]
    ""    -> []
        cons :: Char -> [Token] -> [Token]
        cons :: Char -> [Token] -> [Token]
    cons Char
    c (Str [Char]
    s : [Token]
    ts) = [Char] -> Token
    Str (Char
    c Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : [Char]
    s) Token -> [Token] -> [Token]
    forall a. a -> [a] -> [a]
    : [Token]
    ts
        cons Char
    c [Token]
    ts           = [Char] -> Token
    Str [Char
    c] Token -> [Token] -> [Token]
    forall a. a -> [a] -> [a]
    : [Token]
    ts