    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Primitive System.FilePath.Posix simple bindings to Haskell functions
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module System.FilePath.Posix.Primitive where

    open import Agda.Builtin.Bool using (Bool)
    open import Agda.Builtin.Char using (Char)
    open import Agda.Builtin.List using (List)
    open import Agda.Builtin.Maybe using (Maybe)
    open import Agda.Builtin.String using (String)
    open import Foreign.Haskell as FFI using (Pair; Either)
    open import IO.Primitive.Core using (IO)

    -- A filepath has a nature: it can be either relative or absolute.
    -- We postulate this nature rather than defining it as an inductive
    -- type so that the user cannot inspect it. The only way to cast an
    -- arbitrary filepath nature @n@ to either @relative@ or @absolute@
    -- is to use @checkFilePath@.

    module Nature where

      postulate
        Nature : Set
        relative absolute unknown : Nature

    -- In the Haskell backend these @natures@ are simply erased as the
    -- libraries represent all filepaths in the same way.

      {-# FOREIGN GHC import Data.Kind     #-}
      {-# COMPILE GHC Nature   = type Type #-}
      {-# COMPILE GHC relative = type ()   #-}
      {-# COMPILE GHC absolute = type ()   #-}
      {-# COMPILE GHC unknown  = type ()   #-}

    open Nature using (Nature) public

    private
      variable
        m n : Nature

    postulate

      FilePath     : Nature → Set
      getFilePath  : FilePath n → String

      Extension    : Set
      mkExtension  : String → Extension
      getExtension : Extension → String

    {-# FOREIGN GHC import Data.Text                        #-}
    {-# FOREIGN GHC import System.FilePath.Posix            #-}
    {-# FOREIGN GHC type AgdaFilePath n = FilePath          #-}
    {-# COMPILE GHC FilePath            = type AgdaFilePath #-}
    {-# COMPILE GHC getFilePath         = const pack        #-}
    {-# COMPILE GHC Extension           = type String       #-}
    {-# COMPILE GHC mkExtension         = unpack            #-}
    {-# COMPILE GHC getExtension        = pack              #-}

    -- We provide convenient short names for the two types of filepaths

    AbsolutePath = FilePath Nature.absolute
    RelativePath = FilePath Nature.relative
    SomePath     = FilePath Nature.unknown

    -- In order to prevent users from picking whether a string gets
    -- converted to a @relative@ or an @absolute@ path we have:
    -- * a postulated @unknown@ nature
    -- * a function @mkFilePath@ producing filepaths of this postulated nature

    postulate
      mkFilePath : String → SomePath

    {-# COMPILE GHC mkFilePath = unpack #-}

    postulate

      -- Separator predicates

      pathSeparator         : Char
      pathSeparators        : List Char
      isPathSeparator       : Char → Bool
      searchPathSeparator   : Char
      isSearchPathSeparator : Char → Bool
      extSeparator          : Char
      isExtSeparator        : Char → Bool

      -- $PATH methods

      splitSearchPath : String → List SomePath
      getSearchPath   : IO (List SomePath)

      -- Extension functions

      splitExtension    : FilePath n → Pair (FilePath n) Extension
      takeExtension     : FilePath n → Extension
      replaceExtension  : FilePath n → Extension → FilePath n
      dropExtension     : FilePath n → FilePath n
      addExtension      : FilePath n → Extension → FilePath n
      hasExtension      : FilePath n → Bool
      splitExtensions   : FilePath n → Pair (FilePath n) Extension
      takeExtensions    : FilePath n → Extension
      replaceExtensions : FilePath n → Extension → FilePath n
      dropExtensions    : FilePath n → FilePath n
      isExtensionOf     : Extension → FilePath n → Bool
      stripExtension    : Extension → FilePath n → Maybe (FilePath n)

      -- Filename/directory functions

      splitFileName    : FilePath n → Pair (FilePath n) RelativePath
      takeFileName     : FilePath n → String
      replaceFileName  : FilePath n → String → FilePath n
      dropFileName     : FilePath n → FilePath n
      takeBaseName     : FilePath n → String
      replaceBaseName  : FilePath n → String → FilePath n
      takeDirectory    : FilePath n → FilePath n
      replaceDirectory : FilePath m → FilePath n → FilePath n
      combine          : FilePath n → RelativePath → FilePath n
      splitPath        : FilePath n → List RelativePath
      joinPath         : List RelativePath → RelativePath
      splitDirectories : FilePath n → List RelativePath

      -- Drive functions

      splitDrive : FilePath n → Pair (FilePath n) RelativePath
      joinDrive  : FilePath n → RelativePath → FilePath n
      takeDrive  : FilePath n → FilePath n
      hasDrive   : FilePath n → Bool
      dropDrive  : FilePath n → RelativePath
      isDrive    : FilePath n → Bool

      -- Trailing slash functions

      hasTrailingPathSeparator  : FilePath n → Bool
      addTrailingPathSeparator  : FilePath n → FilePath n
      dropTrailingPathSeparator : FilePath n → FilePath n

      -- File name manipulations

      normalise     : FilePath n → FilePath n
      equalFilePath : FilePath m → FilePath n → Bool
      makeRelative  : FilePath m → FilePath n → RelativePath
      checkFilePath : FilePath n → Either RelativePath AbsolutePath
      isRelative    : FilePath n → Bool
      isAbsolute    : FilePath n → Bool
      isValid       : FilePath n → Bool
      makeValid     : FilePath n → FilePath n

    {-# FOREIGN GHC
    checkFilePath fp
      | isRelative fp = Left fp
      | otherwise     = Right fp
    #-}

    {-# COMPILE GHC pathSeparator         = pathSeparator         #-}
    {-# COMPILE GHC pathSeparators        = pathSeparators        #-}
    {-# COMPILE GHC isPathSeparator       = isPathSeparator       #-}
    {-# COMPILE GHC searchPathSeparator   = searchPathSeparator   #-}
    {-# COMPILE GHC isSearchPathSeparator = isSearchPathSeparator #-}
    {-# COMPILE GHC extSeparator          = extSeparator          #-}
    {-# COMPILE GHC isExtSeparator        = isExtSeparator        #-}

    {-# COMPILE GHC splitSearchPath = splitSearchPath . unpack #-}
    {-# COMPILE GHC getSearchPath   = getSearchPath            #-}

    {-# COMPILE GHC splitExtension    = const splitExtension    #-}
    {-# COMPILE GHC takeExtension     = const takeExtension     #-}
    {-# COMPILE GHC replaceExtension  = const replaceExtension  #-}
    {-# COMPILE GHC dropExtension     = const dropExtension     #-}
    {-# COMPILE GHC addExtension      = const addExtension      #-}
    {-# COMPILE GHC hasExtension      = const hasExtension      #-}
    {-# COMPILE GHC splitExtensions   = const splitExtensions   #-}
    {-# COMPILE GHC takeExtensions    = const takeExtensions    #-}
    {-# COMPILE GHC replaceExtensions = const replaceExtensions #-}
    {-# COMPILE GHC dropExtensions    = const dropExtensions    #-}
    {-# COMPILE GHC isExtensionOf     = const isExtensionOf     #-}
    {-# COMPILE GHC stripExtension    = const stripExtension    #-}

    {-# COMPILE GHC splitFileName    = const splitFileName                     #-}
    {-# COMPILE GHC takeFileName     = const $ pack . takeFileName             #-}
    {-# COMPILE GHC replaceFileName  = const $ fmap (. unpack) replaceFileName #-}
    {-# COMPILE GHC dropFileName     = const dropFileName                      #-}
    {-# COMPILE GHC takeBaseName     = const $ pack . takeBaseName             #-}
    {-# COMPILE GHC replaceBaseName  = const $ fmap (. unpack) replaceBaseName #-}
    {-# COMPILE GHC takeDirectory    = const takeDirectory                     #-}
    {-# COMPILE GHC replaceDirectory = \ _ _ -> replaceDirectory               #-}
    {-# COMPILE GHC combine          = const combine                           #-}
    {-# COMPILE GHC splitPath        = const splitPath                         #-}
    {-# COMPILE GHC joinPath         = joinPath                                #-}
    {-# COMPILE GHC splitDirectories = const splitDirectories                  #-}

    {-# COMPILE GHC splitDrive = const splitDrive #-}
    {-# COMPILE GHC joinDrive  = const joinDrive  #-}
    {-# COMPILE GHC takeDrive  = const takeDrive  #-}
    {-# COMPILE GHC hasDrive   = const hasDrive   #-}
    {-# COMPILE GHC dropDrive  = const dropDrive  #-}
    {-# COMPILE GHC isDrive    = const isDrive    #-}

    {-# COMPILE GHC hasTrailingPathSeparator  = const hasTrailingPathSeparator  #-}
    {-# COMPILE GHC addTrailingPathSeparator  = const addTrailingPathSeparator  #-}
    {-# COMPILE GHC dropTrailingPathSeparator = const dropTrailingPathSeparator #-}

    {-# COMPILE GHC normalise     = const normalise        #-}
    {-# COMPILE GHC equalFilePath = \ _ _ -> equalFilePath #-}
    {-# COMPILE GHC makeRelative  = \ _ _ -> makeRelative  #-}
    {-# COMPILE GHC isRelative    = const isRelative       #-}
    {-# COMPILE GHC isAbsolute    = const isAbsolute       #-}
    {-# COMPILE GHC checkFilePath = const checkFilePath    #-}
    {-# COMPILE GHC isValid       = const isValid          #-}
    {-# COMPILE GHC makeValid     = const makeValid        #-}