{- |
Module      :  ./Driver/AnaLib.hs
Description :  wrapper for static analysis of DOL
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

wrapper for static analysis of DOL reading and writing prf-files
-}

module Driver.AnaLib
    ( anaLib
    , anaLibExt
    , anaLibReadPrfs
    ) where

import Common.Utils (FileInfo(..))

import Proofs.Automatic
import Proofs.NormalForm

import Static.DevGraph
import Static.History
import Static.AnalysisLibrary
import Static.ApplyChanges
import Static.FromXml
import System.Directory (removeFile)

import Comorphisms.LogicGraph

import Common.Result
import Common.ResultT
import Common.LibName
import qualified Common.Lib.SizedList as SizedList

import Driver.Options
import Driver.ReadFn

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.List (isSuffixOf)
import Control.Monad
import Data.Maybe

anaLibReadPrfs :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLibReadPrfs :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLibReadPrfs opts :: HetcatsOpts
opts file :: FilePath
file = do
    Maybe (LibName, LibEnv)
m <- HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLib HetcatsOpts
opts
      { outtypes :: [OutType]
outtypes = []
      , specNames :: [SIMPLE_ID]
specNames = []
      , modelSparQ :: FilePath
modelSparQ = ""
      , dumpOpts :: [FilePath]
dumpOpts = [] } FilePath
file
    case Maybe (LibName, LibEnv)
m of
      Nothing -> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (LibName, LibEnv)
forall a. Maybe a
Nothing
      Just (ln :: LibName
ln, libEnv :: LibEnv
libEnv) -> do
        LibEnv
nEnv <- HetcatsOpts -> LibEnv -> IO LibEnv
readPrfFiles HetcatsOpts
opts LibEnv
libEnv
        Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv)))
-> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (LibName, LibEnv) -> Maybe (LibName, LibEnv)
forall a. a -> Maybe a
Just (LibName
ln, LibEnv
nEnv)

-- | lookup an env or read and analyze a file
anaLib :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLib :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLib opts :: HetcatsOpts
opts origName :: FilePath
origName = do
  let fname :: FilePath
fname = HetcatsOpts -> FilePath -> FilePath
useCatalogURL HetcatsOpts
opts FilePath
origName
      isPrfFile :: FilePath -> Bool
isPrfFile = FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSuffixOf FilePath
prfSuffix
  Either
  FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath)
ep <- HetcatsOpts
-> FilePath
-> IO
     (Either
        FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath))
getContentAndFileType HetcatsOpts
opts {intype :: InType
intype = InType
GuessIn}
    (FilePath
 -> IO
      (Either
         FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath)))
-> FilePath
-> IO
     (Either
        FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath))
forall a b. (a -> b) -> a -> b
$ if FilePath -> Bool
isPrfFile FilePath
fname then FilePath -> FilePath
rmSuffix FilePath
fname else FilePath
fname
  case Either
  FilePath (Maybe FilePath, Maybe FilePath, FileInfo, FilePath)
ep of
    Left _ -> HetcatsOpts
-> FilePath -> LibEnv -> DGraph -> IO (Maybe (LibName, LibEnv))
anaLibExt HetcatsOpts
opts FilePath
fname LibEnv
emptyLibEnv DGraph
emptyDG
    Right (_, _, fInfo :: FileInfo
fInfo, content :: FilePath
content)
      | FilePath -> Bool
isPrfFile (FileInfo -> FilePath
filePath FileInfo
fInfo) -> do
          HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "a matching source file for proof history '"
                           FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (FileInfo -> FilePath
filePath FileInfo
fInfo) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "' not found."
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FileInfo -> Bool
wasDownloaded FileInfo
fInfo) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
removeFile (FileInfo -> FilePath
filePath FileInfo
fInfo)
          Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (LibName, LibEnv)
forall a. Maybe a
Nothing
      | HetcatsOpts -> FilePath -> FilePath -> Bool
isDgXmlFile HetcatsOpts
opts (FileInfo -> FilePath
filePath FileInfo
fInfo) FilePath
content -> do
          Maybe (LibName, LibEnv)
res <- HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
readDGXml HetcatsOpts
opts (FileInfo -> FilePath
filePath FileInfo
fInfo)
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FileInfo -> Bool
wasDownloaded FileInfo
fInfo) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
removeFile (FileInfo -> FilePath
filePath FileInfo
fInfo)
          Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (LibName, LibEnv)
res
      | Bool
otherwise -> do
          Maybe (LibName, LibEnv)
res <- HetcatsOpts
-> FilePath -> LibEnv -> DGraph -> IO (Maybe (LibName, LibEnv))
anaLibExt HetcatsOpts
opts (HetcatsOpts -> FilePath -> FilePath -> FilePath
keepOrigClifName HetcatsOpts
opts FilePath
origName (FileInfo -> FilePath
filePath FileInfo
fInfo))
            LibEnv
emptyLibEnv DGraph
emptyDG
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FileInfo -> Bool
wasDownloaded FileInfo
fInfo) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
removeFile (FileInfo -> FilePath
filePath FileInfo
fInfo)
          Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (LibName, LibEnv)
res

-- | read a file and extended the current library environment
anaLibExt :: HetcatsOpts -> FilePath -> LibEnv -> DGraph
  -> IO (Maybe (LibName, LibEnv))
anaLibExt :: HetcatsOpts
-> FilePath -> LibEnv -> DGraph -> IO (Maybe (LibName, LibEnv))
anaLibExt opts :: HetcatsOpts
opts file :: FilePath
file libEnv :: LibEnv
libEnv initDG :: DGraph
initDG = do
    Result ds :: [Diagnosis]
ds res :: Maybe (LibName, LibEnv)
res <- ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> HetcatsOpts
-> LNS
-> LibEnv
-> DGraph
-> Maybe LibName
-> FilePath
-> ResultT IO (LibName, LibEnv)
anaLibFileOrGetEnv (FilePath -> LogicGraph
logicGraphForFile FilePath
file) HetcatsOpts
opts
      LNS
forall a. Set a
Set.empty LibEnv
libEnv DGraph
initDG Maybe LibName
forall a. Maybe a
Nothing FilePath
file
    HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
    case Maybe (LibName, LibEnv)
res of
        Nothing -> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (LibName, LibEnv)
forall a. Maybe a
Nothing
        Just (ln :: LibName
ln, lenv :: LibEnv
lenv) -> do
            let envRes :: Result LibEnv
envRes = if HetcatsOpts -> Bool
computeNormalForm HetcatsOpts
opts then LibName -> LibEnv -> Result LibEnv
normalForm LibName
ln LibEnv
lenv else
                  LibEnv -> Result LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return LibEnv
lenv
                envN :: LibEnv
envN = LibEnv -> Maybe LibEnv -> LibEnv
forall a. a -> Maybe a -> a
fromMaybe LibEnv
lenv (Maybe LibEnv -> LibEnv) -> Maybe LibEnv -> LibEnv
forall a b. (a -> b) -> a -> b
$ Result LibEnv -> Maybe LibEnv
forall a. Result a -> Maybe a
maybeResult Result LibEnv
envRes
                nEnv :: LibEnv
nEnv = if HetcatsOpts -> Bool
applyAutomatic HetcatsOpts
opts Bool -> Bool -> Bool
|| HetcatsOpts -> Bool
hasPrfOut HetcatsOpts
opts
                       then LibName -> LibEnv -> LibEnv
automatic LibName
ln LibEnv
envN else LibEnv
envN
                xd :: FilePath
xd = HetcatsOpts -> FilePath
xupdate HetcatsOpts
opts
            HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts ([Diagnosis] -> IO ()) -> [Diagnosis] -> IO ()
forall a b. (a -> b) -> a -> b
$ Result LibEnv -> [Diagnosis]
forall a. Result a -> [Diagnosis]
diags Result LibEnv
envRes
            (LibName, LibEnv)
p <- if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
xd then (LibName, LibEnv) -> IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return (LibName
ln, LibEnv
nEnv) else do
              HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Reading " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
xd
              FilePath
xs <- FilePath -> IO FilePath
readFile FilePath
xd
              Result es :: [Diagnosis]
es mdg :: Maybe (LibName, LibEnv)
mdg <- ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv)))
-> ResultT IO (LibName, LibEnv) -> IO (Result (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ HetcatsOpts
-> FilePath
-> LibEnv
-> LibName
-> DGraph
-> ResultT IO (LibName, LibEnv)
dgXUpdate HetcatsOpts
opts FilePath
xs LibEnv
nEnv LibName
ln
                (LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
nEnv)
              HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
es
              (LibName, LibEnv) -> IO (LibName, LibEnv)
forall (m :: * -> *) a. Monad m => a -> m a
return ((LibName, LibEnv) -> IO (LibName, LibEnv))
-> (LibName, LibEnv) -> IO (LibName, LibEnv)
forall a b. (a -> b) -> a -> b
$ (LibName, LibEnv) -> Maybe (LibName, LibEnv) -> (LibName, LibEnv)
forall a. a -> Maybe a -> a
fromMaybe (LibName
ln, LibEnv
nEnv) Maybe (LibName, LibEnv)
mdg
            Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv)))
-> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (LibName, LibEnv) -> Maybe (LibName, LibEnv)
forall a. a -> Maybe a
Just (LibName, LibEnv)
p

readPrfFile :: HetcatsOpts -> LibEnv -> LibName -> IO LibEnv
readPrfFile :: HetcatsOpts -> LibEnv -> LibName -> IO LibEnv
readPrfFile opts :: HetcatsOpts
opts ps :: LibEnv
ps ln :: LibName
ln = do
    let fname :: FilePath
fname = LibName -> FilePath
libNameToFile LibName
ln
        prfFile :: FilePath
prfFile = FilePath -> FilePath
rmSuffix FilePath
fname FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
prfSuffix
    Bool
recent <- HetcatsOpts -> FilePath -> FilePath -> IO Bool
checkRecentEnv HetcatsOpts
opts FilePath
prfFile FilePath
fname
    SizedList HistElem
h <- if Bool
recent then
          (Maybe (SizedList HistElem) -> SizedList HistElem)
-> IO (Maybe (SizedList HistElem)) -> IO (SizedList HistElem)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SizedList HistElem
-> Maybe (SizedList HistElem) -> SizedList HistElem
forall a. a -> Maybe a -> a
fromMaybe SizedList HistElem
forall a. SizedList a
SizedList.empty)
            (IO (Maybe (SizedList HistElem)) -> IO (SizedList HistElem))
-> IO (Maybe (SizedList HistElem)) -> IO (SizedList HistElem)
forall a b. (a -> b) -> a -> b
$ LogicGraph
-> HetcatsOpts
-> Maybe LibName
-> FilePath
-> IO (Maybe (SizedList HistElem))
forall a.
ShATermLG a =>
LogicGraph
-> HetcatsOpts -> Maybe LibName -> FilePath -> IO (Maybe a)
readVerbose LogicGraph
logicGraph HetcatsOpts
opts (LibName -> Maybe LibName
forall a. a -> Maybe a
Just LibName
ln) FilePath
prfFile
       else SizedList HistElem -> IO (SizedList HistElem)
forall (m :: * -> *) a. Monad m => a -> m a
return SizedList HistElem
forall a. SizedList a
SizedList.empty
    LibEnv -> IO LibEnv
forall (m :: * -> *) a. Monad m => a -> m a
return (LibEnv -> IO LibEnv) -> LibEnv -> IO LibEnv
forall a b. (a -> b) -> a -> b
$ (DGraph -> Maybe DGraph) -> LibName -> LibEnv -> LibEnv
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (DGraph -> Maybe DGraph
forall a. a -> Maybe a
Just (DGraph -> Maybe DGraph)
-> (DGraph -> DGraph) -> DGraph -> Maybe DGraph
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SizedList HistElem -> DGraph -> DGraph
applyProofHistory SizedList HistElem
h) LibName
ln LibEnv
ps

readPrfFiles :: HetcatsOpts -> LibEnv -> IO LibEnv
readPrfFiles :: HetcatsOpts -> LibEnv -> IO LibEnv
readPrfFiles opts :: HetcatsOpts
opts le :: LibEnv
le = (LibEnv -> LibName -> IO LibEnv)
-> LibEnv -> [LibName] -> IO LibEnv
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (HetcatsOpts -> LibEnv -> LibName -> IO LibEnv
readPrfFile HetcatsOpts
opts) LibEnv
le ([LibName] -> IO LibEnv) -> [LibName] -> IO LibEnv
forall a b. (a -> b) -> a -> b
$ LibEnv -> [LibName]
forall k a. Map k a -> [k]
Map.keys LibEnv
le