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
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
getFilePrefixGeneric :: [String]
-> FilePath
-> 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)
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 ()
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)