{- |
Module      :  ./Driver/WriteLibDefn.hs
Description :  Writing out a DOL library
Copyright   :  (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(DevGraph)

Writing out DOL env files as much as is needed for
the static analysis
-}

module Driver.WriteLibDefn
  ( getFilePrefix
  , getFilePrefixGeneric
  , writeLibDefn
  , writeLibDefnLatex
  , toShATermString
  , writeShATermFile
  , writeFileInfo
  ) where

import Common.Utils
import Common.Doc
import Common.LibName
import Common.PrintLaTeX
import Common.GlobalAnnotations (GlobalAnnos)
import Common.ConvertGlobalAnnos ()
import Common.IO

import Control.Exception as Exception

import ATerm.AbstractSyntax
import qualified ATerm.ReadWrite as AT

import ATC.AS_Library ()
import ATC.DevGraph ()
import ATC.Grothendieck

import Logic.Grothendieck

import Syntax.AS_Library (LIB_DEFN ())
import Syntax.Print_AS_Library ()
import Syntax.Print_AS_Structured
import Syntax.ToXml

import Text.XML.Light (ppTopElement)

import Driver.Options
import Driver.Version

import System.FilePath

-- | Compute the prefix for files to be written out
getFilePrefix :: HetcatsOpts -> FilePath -> (FilePath, FilePath)
getFilePrefix :: HetcatsOpts -> FilePath -> (FilePath, FilePath)
getFilePrefix opts :: HetcatsOpts
opts = [FilePath] -> FilePath -> FilePath -> (FilePath, FilePath)
getFilePrefixGeneric (FilePath
envSuffix FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
downloadExtensions)
                     (FilePath -> FilePath -> (FilePath, FilePath))
-> FilePath -> FilePath -> (FilePath, FilePath)
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath
outdir HetcatsOpts
opts

-- | Version of getFilePrefix with explicit parameters
getFilePrefixGeneric :: [String] -- ^ list of suffixes
                     -> FilePath -- ^ the outdir
                     -> FilePath -> (FilePath, FilePath)
getFilePrefixGeneric :: [FilePath] -> FilePath -> FilePath -> (FilePath, FilePath)
getFilePrefixGeneric suffs :: [FilePath]
suffs odir' :: FilePath
odir' file :: FilePath
file =
    let (base :: FilePath
base, path :: FilePath
path, _) = [FilePath] -> FilePath -> (FilePath, FilePath, Maybe FilePath)
fileparse [FilePath]
suffs FilePath
file
        odir :: FilePath
odir = if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
odir' then FilePath
path else FilePath
odir'
    in (FilePath
odir, FilePath
odir FilePath -> FilePath -> FilePath
</> FilePath
base)

{- |
  Write the given LIB_DEFN in every format that HetcatsOpts includes.
  Filenames are determined by the output formats.
-}
writeLibDefn :: LogicGraph -> GlobalAnnos -> FilePath -> HetcatsOpts
  -> LIB_DEFN -> IO ()
writeLibDefn :: LogicGraph
-> GlobalAnnos -> FilePath -> HetcatsOpts -> LIB_DEFN -> IO ()
writeLibDefn lg :: LogicGraph
lg ga :: GlobalAnnos
ga fullFileName :: FilePath
fullFileName opts :: HetcatsOpts
opts ld :: LIB_DEFN
ld = do
    let file :: FilePath
file = FilePath -> FilePath -> FilePath
tryToStripPrefix "file://" FilePath
fullFileName
        (odir :: FilePath
odir, filePrefix :: FilePath
filePrefix) = HetcatsOpts -> FilePath -> (FilePath, FilePath)
getFilePrefix HetcatsOpts
opts FilePath
file
        printXml :: FilePath -> IO ()
printXml fn :: FilePath
fn = FilePath -> FilePath -> IO ()
writeFile FilePath
fn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Element -> FilePath
ppTopElement (LogicGraph -> GlobalAnnos -> LIB_DEFN -> Element
xmlLibDefn LogicGraph
lg GlobalAnnos
ga LIB_DEFN
ld)
        printAscii :: Bool -> FilePath -> IO ()
printAscii b :: Bool
b fn :: FilePath
fn = Enc -> FilePath -> FilePath -> IO ()
writeEncFile (HetcatsOpts -> Enc
ioEncoding HetcatsOpts
opts) FilePath
fn
          (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ StripComment -> GlobalAnnos -> Doc -> FilePath
renderExtText (Bool -> StripComment
StripComment Bool
b) GlobalAnnos
ga (LogicGraph -> LIB_DEFN -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg LIB_DEFN
ld) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n"
        printHtml :: FilePath -> IO ()
printHtml fn :: FilePath
fn = Enc -> FilePath -> FilePath -> IO ()
writeEncFile (HetcatsOpts -> Enc
ioEncoding HetcatsOpts
opts) FilePath
fn
          (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> Doc -> FilePath
renderHtml GlobalAnnos
ga (Doc -> FilePath) -> Doc -> FilePath
forall a b. (a -> b) -> a -> b
$ LogicGraph -> LIB_DEFN -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg LIB_DEFN
ld
        write_type :: OutType -> IO ()
        write_type :: OutType -> IO ()
write_type ty :: OutType
ty = case OutType
ty of
            PrettyOut pty :: PrettyType
pty -> do
              let fn :: FilePath
fn = FilePath
filePrefix FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ OutType -> FilePath
forall a. Show a => a -> FilePath
show OutType
ty
              HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Writing file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fn
              case PrettyType
pty of
                PrettyXml -> FilePath -> IO ()
printXml FilePath
fn
                PrettyAscii b :: Bool
b -> Bool -> FilePath -> IO ()
printAscii Bool
b FilePath
fn
                PrettyHtml -> FilePath -> IO ()
printHtml FilePath
fn
                PrettyLatex b :: Bool
b -> LogicGraph -> Bool -> GlobalAnnos -> FilePath -> LIB_DEFN -> IO ()
writeLibDefnLatex LogicGraph
lg Bool
b GlobalAnnos
ga FilePath
fn LIB_DEFN
ld
            _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- implemented elsewhere
    HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 3 ("Current OutDir: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
odir)
    (OutType -> IO ()) -> [OutType] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ OutType -> IO ()
write_type ([OutType] -> IO ()) -> [OutType] -> IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts

writeLibDefnLatex :: LogicGraph -> Bool -> GlobalAnnos -> FilePath -> LIB_DEFN
  -> IO ()
writeLibDefnLatex :: LogicGraph -> Bool -> GlobalAnnos -> FilePath -> LIB_DEFN -> IO ()
writeLibDefnLatex lg :: LogicGraph
lg lbl :: Bool
lbl ga :: GlobalAnnos
ga oup :: FilePath
oup = FilePath -> FilePath -> IO ()
writeFile FilePath
oup (FilePath -> IO ()) -> (LIB_DEFN -> FilePath) -> LIB_DEFN -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Int -> Doc -> FilePath
renderLatex Maybe Int
forall a. Maybe a
Nothing
  (Doc -> FilePath) -> (LIB_DEFN -> Doc) -> LIB_DEFN -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StripComment -> Label -> GlobalAnnos -> Doc -> Doc
toLatexAux (Bool -> StripComment
StripComment Bool
False) (Bool -> Label
MkLabel Bool
lbl) GlobalAnnos
ga (Doc -> Doc) -> (LIB_DEFN -> Doc) -> LIB_DEFN -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LogicGraph -> LIB_DEFN -> Doc
forall a. PrettyLG a => LogicGraph -> a -> Doc
prettyLG LogicGraph
lg

toShATermString :: ShATermLG a => a -> IO String
toShATermString :: a -> IO FilePath
toShATermString = (ATermTable -> FilePath) -> IO ATermTable -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ATermTable -> FilePath
AT.writeSharedATerm (IO ATermTable -> IO FilePath)
-> (a -> IO ATermTable) -> a -> IO FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> IO ATermTable
forall a. ShATermLG a => a -> IO ATermTable
versionedATermTable

writeShATermFile :: ShATermLG a => FilePath -> a -> IO ()
writeShATermFile :: FilePath -> a -> IO ()
writeShATermFile fp :: FilePath
fp atcon :: a
atcon = a -> IO FilePath
forall a. ShATermLG a => a -> IO FilePath
toShATermString a
atcon IO FilePath -> (FilePath -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> FilePath -> IO ()
writeFile FilePath
fp

versionedATermTable :: ShATermLG a => a -> IO ATermTable
versionedATermTable :: a -> IO ATermTable
versionedATermTable atcon :: a
atcon = do
    (att1 :: ATermTable
att1, versionno :: Int
versionno) <- ATermTable -> FilePath -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG ATermTable
emptyATermTable FilePath
hetsVersionNumeric
    (att2 :: ATermTable
att2, aterm :: Int
aterm) <- ATermTable -> a -> IO (ATermTable, Int)
forall t. ShATermLG t => ATermTable -> t -> IO (ATermTable, Int)
toShATermLG ATermTable
att1 a
atcon
    ATermTable -> IO ATermTable
forall (m :: * -> *) a. Monad m => a -> m a
return (ATermTable -> IO ATermTable) -> ATermTable -> IO ATermTable
forall a b. (a -> b) -> a -> b
$ (ATermTable, Int) -> ATermTable
forall a b. (a, b) -> a
fst ((ATermTable, Int) -> ATermTable)
-> (ATermTable, Int) -> ATermTable
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (FilePath -> [Int] -> [Int] -> ShATerm
ShAAppl "hets" [Int
versionno, Int
aterm] []) ATermTable
att2

writeShATermFileSDoc :: ShATermLG a => FilePath -> a -> IO ()
writeShATermFileSDoc :: FilePath -> a -> IO ()
writeShATermFileSDoc fp :: FilePath
fp atcon :: a
atcon =
   a -> IO ATermTable
forall a. ShATermLG a => a -> IO ATermTable
versionedATermTable a
atcon IO ATermTable -> (ATermTable -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> ATermTable -> IO ()
AT.writeSharedATermFile FilePath
fp

writeFileInfo :: ShATermLG a => HetcatsOpts -> LibName
              -> FilePath -> LIB_DEFN -> a -> IO ()
writeFileInfo :: HetcatsOpts -> LibName -> FilePath -> LIB_DEFN -> a -> IO ()
writeFileInfo opts :: HetcatsOpts
opts ln :: LibName
ln fullFileName :: FilePath
fullFileName ld :: LIB_DEFN
ld gctx :: a
gctx =
  let file :: FilePath
file = FilePath -> FilePath -> FilePath
tryToStripPrefix "file://" FilePath
fullFileName
      envFile :: FilePath
envFile = (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> b
snd (HetcatsOpts -> FilePath -> (FilePath, FilePath)
getFilePrefix HetcatsOpts
opts FilePath
file) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
envSuffix in
  case HetcatsOpts -> AnaType
analysis HetcatsOpts
opts of
  Basic -> do
      HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 ("Writing file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
envFile)
      IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
Exception.catch (FilePath -> (LibName, (LIB_DEFN, a)) -> IO ()
forall a. ShATermLG a => FilePath -> a -> IO ()
writeShATermFileSDoc FilePath
envFile (LibName
ln, (LIB_DEFN
ld, a
gctx)))
           ((SomeException -> IO ()) -> IO ())
-> (SomeException -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ err :: SomeException
err -> do
              HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 (FilePath
envFile FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " not written")
              HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 3 ("see following error description:\n"
                                   FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SomeException -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows (SomeException
err :: SomeException) "\n")
  _ -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 ("Not writing " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
envFile)