module System.FilePath.Posix.Primitive where

open import Agda.Builtin.Bool
open import Agda.Builtin.Char
open import Agda.Builtin.List
open import Agda.Builtin.String
open import Data.Product
open import Data.Sum.Base
open import Foreign.Haskell as FFI
open import IO.Primitive

-- 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. 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 → FFI.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        #-}