{- |
Module      :  $Header$
Description :  wrapper for static analysis of HetCASL
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 HetCASL reading and writing prf-files
-}

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

import Proofs.Automatic
import Proofs.NormalForm

import Static.DevGraph
import Static.History
import Static.AnalysisLibrary
import Static.ApplyChanges
import Static.FromXml

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 opts file = do
    m <- anaLib opts
      { outtypes = []
      , specNames = []
      , modelSparQ = ""
      , dumpOpts = [] } file
    case m of
      Nothing -> return Nothing
      Just (ln, libEnv) -> do
        nEnv <- readPrfFiles opts libEnv
        return $ Just (ln, nEnv)

-- | lookup an env or read and analyze a file
anaLib :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaLib opts origName = do
  let fname = useCatalogURL opts origName
      isPrfFile = isSuffixOf prfSuffix
  ep <- getContent opts {intype = GuessIn}
    $ if isPrfFile fname then rmSuffix fname else fname
  case ep of
    Left _ -> anaLibExt opts fname emptyLibEnv emptyDG
    Right (file, content)
      | isPrfFile file -> do
            putIfVerbose opts 0 $ "a matching source file for proof history '"
                             ++ file ++ "' not found."
            return Nothing
      | isDgXmlFile opts file content -> readDGXml opts file
      | otherwise -> anaLibExt opts (keepOrigClifName opts origName file)
            emptyLibEnv emptyDG

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

readPrfFile :: HetcatsOpts -> LibEnv -> LibName -> IO LibEnv
readPrfFile opts ps ln = do
    let fname = libNameToFile ln
        prfFile = rmSuffix fname ++ prfSuffix
    recent <- checkRecentEnv opts prfFile fname
    h <- if recent then
          fmap (fromMaybe SizedList.empty)
            $ readVerbose logicGraph opts (Just ln) prfFile
       else return SizedList.empty
    return $ Map.update (Just . applyProofHistory h) ln ps

readPrfFiles :: HetcatsOpts -> LibEnv -> IO LibEnv
readPrfFiles opts le = foldM (readPrfFile opts) le $ Map.keys le
