{-# LANGUAGE ScopedTypeVariables #-}

-- | This module contains Haskell variables representing globally visible
-- names for files, paths, extensions.
--
-- Rather than have strings floating around the system, all constant names
-- should be defined here, and the (exported) variables should be used and
-- manipulated elsewhere.

module Language.Fixpoint.Utils.Files (

  -- * Hardwired file extension names
    Ext (..)
  , extFileName
  , extFileNameR
  , tempDirectory
  , extModuleName
  , withExt
  , isExtFile
  , isBinary

  -- * Hardwired paths
  , getFixpointPath
  , getZ3LibPath

  -- * Various generic utility functions for finding and removing files
  , getFileInDirs
  , copyFiles

) where

import qualified Control.Exception      as Ex
import           Control.Monad
import           Data.List              hiding (find)
import           Data.Maybe             (fromMaybe)
import           System.Directory
import           System.FilePath
import           Language.Fixpoint.Misc (errorstar)

------------------------------------------------------------
-- | Hardwired Paths and Files -----------------------------
------------------------------------------------------------

getFixpointPath :: IO FilePath
getFixpointPath :: IO FilePath
getFixpointPath = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
fromMaybe FilePath
forall a. a
msg (Maybe FilePath -> FilePath)
-> ([Maybe FilePath] -> Maybe FilePath)
-> [Maybe FilePath]
-> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe FilePath] -> Maybe FilePath
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([Maybe FilePath] -> FilePath)
-> IO [Maybe FilePath] -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                  [IO (Maybe FilePath)] -> IO [Maybe FilePath]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ FilePath -> IO (Maybe FilePath)
findExecutable FilePath
"fixpoint.native"
                           , FilePath -> IO (Maybe FilePath)
findExecutable FilePath
"fixpoint.native.exe"
                             -- fallback for developing in-tree...
                           , [FilePath] -> FilePath -> IO (Maybe FilePath)
findFile [FilePath
"external/fixpoint"] FilePath
"fixpoint.native"
                           ]
  where
    msg :: a
msg = FilePath -> a
forall a. (?callStack::CallStack) => FilePath -> a
errorstar FilePath
"Cannot find fixpoint binary [fixpoint.native]"

getZ3LibPath :: IO FilePath
getZ3LibPath :: IO FilePath
getZ3LibPath    = FilePath -> FilePath
dropFileName (FilePath -> FilePath) -> IO FilePath -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO FilePath
getFixpointPath


--checkM f msg p
--  = do ex <- f p
--       if ex then return p else errorstar $ "Cannot find " ++ msg ++ " at :" ++ p


 -----------------------------------------------------------------------------------

data Ext = Cgi      -- ^ Constraint Generation Information
         | Fq       -- ^ Input to constraint solving (fixpoint)
         | Out      -- ^ Output from constraint solving (fixpoint)
         | Html     -- ^ HTML file with inferred type annotations
         | Annot    -- ^ Text file with inferred types
         | Vim      -- ^ Vim annotation file
         | Hs       -- ^ Haskell source
         | HsBoot   -- ^ Haskell source
         | LHs      -- ^ Literate Haskell source
         | Js       -- ^ JavaScript source
         | Ts       -- ^ Typescript source
         | Spec     -- ^ Spec file (e.g. include/Prelude.spec)
         | BinSpec  -- ^ Lifted-Spec file, containing automatically generated specifications 
         | Hquals   -- ^ Qualifiers file (e.g. include/Prelude.hquals)
         | Result   -- ^ Final result: SAFE/UNSAFE
         | Cst      -- ^ HTML file with templates?
         | Mkdn     -- ^ Markdown file (temporarily generated from .Lhs + annots)
         | Json     -- ^ JSON file containing result (annots + errors)
         | Saved    -- ^ Previous source (for incremental checking)
         | Cache    -- ^ Previous output (for incremental checking)
         | Dot      -- ^ Constraint Graph
         | Part Int -- ^ Partition
         | Auto Int -- ^ SMTLIB2 queries for automatically created proofs
         | Pred
         | PAss
         | Dat
         | BinFq    -- ^ Binary representation of .fq / FInfo
         | Smt2     -- ^ SMTLIB2 query file
         | Min      -- ^ filter constraints with delta debug
         | MinQuals -- ^ filter qualifiers with delta debug
         | MinKVars -- ^ filter kvars with delta debug
         deriving (Ext -> Ext -> Bool
(Ext -> Ext -> Bool) -> (Ext -> Ext -> Bool) -> Eq Ext
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ext -> Ext -> Bool
$c/= :: Ext -> Ext -> Bool
== :: Ext -> Ext -> Bool
$c== :: Ext -> Ext -> Bool
Eq, Eq Ext
Eq Ext
-> (Ext -> Ext -> Ordering)
-> (Ext -> Ext -> Bool)
-> (Ext -> Ext -> Bool)
-> (Ext -> Ext -> Bool)
-> (Ext -> Ext -> Bool)
-> (Ext -> Ext -> Ext)
-> (Ext -> Ext -> Ext)
-> Ord Ext
Ext -> Ext -> Bool
Ext -> Ext -> Ordering
Ext -> Ext -> Ext
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Ext -> Ext -> Ext
$cmin :: Ext -> Ext -> Ext
max :: Ext -> Ext -> Ext
$cmax :: Ext -> Ext -> Ext
>= :: Ext -> Ext -> Bool
$c>= :: Ext -> Ext -> Bool
> :: Ext -> Ext -> Bool
$c> :: Ext -> Ext -> Bool
<= :: Ext -> Ext -> Bool
$c<= :: Ext -> Ext -> Bool
< :: Ext -> Ext -> Bool
$c< :: Ext -> Ext -> Bool
compare :: Ext -> Ext -> Ordering
$ccompare :: Ext -> Ext -> Ordering
$cp1Ord :: Eq Ext
Ord, Int -> Ext -> FilePath -> FilePath
[Ext] -> FilePath -> FilePath
Ext -> FilePath
(Int -> Ext -> FilePath -> FilePath)
-> (Ext -> FilePath) -> ([Ext] -> FilePath -> FilePath) -> Show Ext
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [Ext] -> FilePath -> FilePath
$cshowList :: [Ext] -> FilePath -> FilePath
show :: Ext -> FilePath
$cshow :: Ext -> FilePath
showsPrec :: Int -> Ext -> FilePath -> FilePath
$cshowsPrec :: Int -> Ext -> FilePath -> FilePath
Show)

extMap :: Ext -> FilePath
extMap :: Ext -> FilePath
extMap          = Ext -> FilePath
go
  where
    go :: Ext -> FilePath
go Ext
Cgi      = FilePath
".cgi"
    go Ext
Pred     = FilePath
".pred"
    go Ext
PAss     = FilePath
".pass"
    go Ext
Dat      = FilePath
".dat"
    go Ext
Out      = FilePath
".fqout"
    go Ext
Fq       = FilePath
".fq"
    go Ext
Html     = FilePath
".html"
    go Ext
Cst      = FilePath
".cst"
    go Ext
Annot    = FilePath
".annot"
    go Ext
Vim      = FilePath
".vim.annot"
    go Ext
Hs       = FilePath
".hs"
    go Ext
LHs      = FilePath
".lhs"
    go Ext
HsBoot   = FilePath
".hs-boot"
    go Ext
Js       = FilePath
".js"
    go Ext
Ts       = FilePath
".ts"
    go Ext
Mkdn     = FilePath
".markdown"
    go Ext
Json     = FilePath
".json"
    go Ext
Spec     = FilePath
".spec"
    go Ext
BinSpec  = FilePath
".bspec"
    go Ext
Hquals   = FilePath
".hquals"
    go Ext
Result   = FilePath
".out"
    go Ext
Saved    = FilePath
".bak"
    go Ext
Cache    = FilePath
".err"
    go Ext
Smt2     = FilePath
".smt2"
    go (Auto Int
n) = FilePath
".auto." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n
    go Ext
Dot      = FilePath
".dot"
    go Ext
BinFq    = FilePath
".bfq"
    go (Part Int
n) = FilePath
"." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n
    go Ext
Min      = FilePath
".minfq"
    go Ext
MinQuals = FilePath
".minquals"
    go Ext
MinKVars = FilePath
".minkvars"
    -- go _      = errorstar $ "extMap: Unknown extension " ++ show e

withExt         :: FilePath -> Ext -> FilePath
withExt :: FilePath -> Ext -> FilePath
withExt FilePath
f Ext
ext   =  FilePath -> FilePath -> FilePath
replaceExtension FilePath
f (Ext -> FilePath
extMap Ext
ext)

extFileName     :: Ext -> FilePath -> FilePath
extFileName :: Ext -> FilePath -> FilePath
extFileName Ext
e FilePath
f = FilePath
path FilePath -> FilePath -> FilePath
</> FilePath -> FilePath -> FilePath
addExtension FilePath
file FilePath
ext
  where
    path :: FilePath
path        = FilePath -> FilePath
tempDirectory FilePath
f
    file :: FilePath
file        = FilePath -> FilePath
takeFileName  FilePath
f
    ext :: FilePath
ext         = Ext -> FilePath
extMap Ext
e

tempDirectory   :: FilePath -> FilePath
tempDirectory :: FilePath -> FilePath
tempDirectory FilePath
f
  | FilePath -> Bool
isTmp FilePath
dir   = FilePath
dir
  | Bool
otherwise   = FilePath
dir FilePath -> FilePath -> FilePath
</> FilePath
tmpDirName
  where
    dir :: FilePath
dir         = FilePath -> FilePath
takeDirectory FilePath
f
    isTmp :: FilePath -> Bool
isTmp       = (FilePath
tmpDirName FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSuffixOf`)

tmpDirName :: FilePath
tmpDirName :: FilePath
tmpDirName      = FilePath
".liquid"

extFileNameR     :: Ext -> FilePath -> FilePath
extFileNameR :: Ext -> FilePath -> FilePath
extFileNameR Ext
ext = (FilePath -> FilePath -> FilePath
`addExtension` Ext -> FilePath
extMap Ext
ext)

isExtFile ::  Ext -> FilePath -> Bool
isExtFile :: Ext -> FilePath -> Bool
isExtFile Ext
ext = (Ext -> FilePath
extMap Ext
ext FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
==) (FilePath -> Bool) -> (FilePath -> FilePath) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath
takeExtension

extModuleName ::  String -> Ext -> FilePath
extModuleName :: FilePath -> Ext -> FilePath
extModuleName FilePath
modName Ext
ext =
  case FilePath -> [FilePath]
explode FilePath
modName of
    [] -> FilePath -> FilePath
forall a. (?callStack::CallStack) => FilePath -> a
errorstar (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath
"malformed module name: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
modName
    [FilePath]
ws -> Ext -> FilePath -> FilePath
extFileNameR Ext
ext (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ (FilePath -> FilePath -> FilePath) -> [FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 FilePath -> FilePath -> FilePath
(</>) [FilePath]
ws
  where
    explode :: FilePath -> [FilePath]
explode = FilePath -> [FilePath]
words (FilePath -> [FilePath])
-> (FilePath -> FilePath) -> FilePath -> [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map (\Char
c -> if Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.' then Char
' ' else Char
c)

copyFiles :: [FilePath] -> FilePath -> IO ()
copyFiles :: [FilePath] -> FilePath -> IO ()
copyFiles [FilePath]
srcs FilePath
tgt
  = do IO () -> (IOException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Ex.catch (FilePath -> IO ()
removeFile FilePath
tgt) ((IOException -> IO ()) -> IO ())
-> (IOException -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(IOException
_ :: Ex.IOException) -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       [FilePath] -> (FilePath -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [FilePath]
srcs (FilePath -> IO FilePath
readFile (FilePath -> IO FilePath)
-> (FilePath -> IO ()) -> FilePath -> IO ()
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> FilePath -> FilePath -> IO ()
appendFile FilePath
tgt)


----------------------------------------------------------------------------------

-- getHsTargets p = mapM canonicalizePath =<< files
--   where
--     files
--       | hasTrailingPathSeparator p = getHsSourceFiles p
--       | otherwise                  = return [p]

-- getHsSourceFiles = find dirs hs
--   where hs   = extension ==? ".hs" ||? extension ==? ".lhs"
--         dirs = liftM (not . ("dist" `isSuffixOf`)) directory

---------------------------------------------------------------------------


getFileInDirs :: FilePath -> [FilePath] -> IO (Maybe FilePath)
getFileInDirs :: FilePath -> [FilePath] -> IO (Maybe FilePath)
getFileInDirs FilePath
name = (FilePath -> IO [FilePath]) -> [FilePath] -> IO (Maybe FilePath)
forall (m :: * -> *) t a.
Monad m =>
(t -> m [a]) -> [t] -> m (Maybe a)
findFirst ((FilePath -> IO Bool) -> FilePath -> IO [FilePath]
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> a -> m [a]
testM FilePath -> IO Bool
doesFileExist (FilePath -> IO [FilePath])
-> (FilePath -> FilePath) -> FilePath -> IO [FilePath]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> FilePath -> FilePath
</> FilePath
name))

testM :: (Monad m) => (a -> m Bool) -> a -> m [a]
testM :: (a -> m Bool) -> a -> m [a]
testM a -> m Bool
f a
x = do Bool
b <- a -> m Bool
f a
x
               [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [ a
x | Bool
b ]

findFirst ::  Monad m => (t -> m [a]) -> [t] -> m (Maybe a)
findFirst :: (t -> m [a]) -> [t] -> m (Maybe a)
findFirst t -> m [a]
_ []     = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
findFirst t -> m [a]
f (t
x:[t]
xs) = do [a]
r <- t -> m [a]
f t
x
                        case [a]
r of
                          a
y:[a]
_ -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Maybe a
forall a. a -> Maybe a
Just a
y)
                          []  -> (t -> m [a]) -> [t] -> m (Maybe a)
forall (m :: * -> *) t a.
Monad m =>
(t -> m [a]) -> [t] -> m (Maybe a)
findFirst t -> m [a]
f [t]
xs

-- findFileInDirs ::  FilePath -> [FilePath] -> IO FilePath
-- findFileInDirs file dirs
--   = liftM (fromMaybe err) (findFirst (find always (fileName ==? file)) dirs)
--     where err = errorstar $ "findFileInDirs: cannot find " ++ file ++ " in " ++ show dirs

isBinary :: FilePath -> Bool
isBinary :: FilePath -> Bool
isBinary = Ext -> FilePath -> Bool
isExtFile Ext
BinFq