WriteLibDefn.hs revision 46c318705d1532d90572abf9ee869016583d985b
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder{- |
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederModule : ./Driver/WriteLibDefn.hs
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederDescription : Writing out a DOL library
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederCopyright : (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006
c06dd8856a03b72f6b3f69e874f8700f10cb8522Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederMaintainer : Christian.Maeder@dfki.de
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederStability : provisional
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederPortability : non-portable(DevGraph)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederWriting out DOL env files as much as is needed for
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowskithe static analysis
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski-}
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maedermodule Driver.WriteLibDefn
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski ( getFilePrefix
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder , getFilePrefixGeneric
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski , writeLibDefn
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski , writeLibDefnLatex
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder , toShATermString
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder , writeShATermFile
9d34a8049237647d0188ee2ec88db2dc45f1f848Till Mossakowski , writeFileInfo
82d681fe6950e2a35f28fdefb874d060632faccaTill Mossakowski ) where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Common.Utils
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowskiimport Common.Doc
70e2af8d4bf21bcdfb53e9a0414e27173b577a1eTill Mossakowskiimport Common.LibName
70e2af8d4bf21bcdfb53e9a0414e27173b577a1eTill Mossakowskiimport Common.PrintLaTeX
2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowskiimport Common.GlobalAnnotations (GlobalAnnos)
2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowskiimport Common.ConvertGlobalAnnos ()
2b4130336e941b7d01c78a6da55449a4c6eca609Till Mossakowskiimport Common.IO
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
82d681fe6950e2a35f28fdefb874d060632faccaTill Mossakowskiimport Control.Exception as Exception
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport ATerm.AbstractSyntax
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport qualified ATerm.ReadWrite as AT
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport ATC.AS_Library ()
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport ATC.DevGraph ()
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport ATC.Grothendieck
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Logic.Grothendieck
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Syntax.AS_Library (LIB_DEFN ())
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Syntax.Print_AS_Library ()
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederimport Syntax.Print_AS_Structured
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Syntax.ToXml
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport Text.XML.Light (ppTopElement)
c529224e0ec191fbaa87261f05c34f89c17b3f3aTill Mossakowski
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maederimport Driver.Options
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder
02b3d9f81150bedd0916c2ffc637a14668e34097Till Mossakowskiimport System.FilePath
c529224e0ec191fbaa87261f05c34f89c17b3f3aTill Mossakowski
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | Compute the prefix for files to be written out
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetFilePrefix :: HetcatsOpts -> FilePath -> (FilePath, FilePath)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetFilePrefix opts = getFilePrefixGeneric (envSuffix : downloadExtensions)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder $ outdir opts
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder-- | Version of getFilePrefix with explicit parameters
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaedergetFilePrefixGeneric :: [String] -- ^ list of suffixes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> FilePath -- ^ the outdir
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> FilePath -> (FilePath, FilePath)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskigetFilePrefixGeneric suffs odir' file =
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let (base, path, _) = fileparse suffs file
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder odir = if null odir' then path else odir'
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski in (odir, odir </> base)
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder{- |
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder Write the given LIB_DEFN in every format that HetcatsOpts includes.
e3c9174a782e90f965a0b080c22861c3ef5af12dTill Mossakowski Filenames are determined by the output formats.
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski-}
8fe1a8e240ccd5f3682a936ef2fa4c22fee973bcTill MossakowskiwriteLibDefn :: LogicGraph -> GlobalAnnos -> FilePath -> HetcatsOpts
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder -> LIB_DEFN -> IO ()
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederwriteLibDefn lg ga file opts ld = do
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski let (odir, filePrefix) = getFilePrefix opts file
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printXml fn = writeFile fn $ ppTopElement (xmlLibDefn lg ga ld)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printAscii b fn = writeEncFile (ioEncoding opts) fn
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ renderExtText (StripComment b) ga (prettyLG lg ld) ++ "\n"
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski printHtml fn = writeEncFile (ioEncoding opts) fn
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski $ renderHtml ga $ prettyLG lg ld
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski write_type :: OutType -> IO ()
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski write_type ty = case ty of
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski PrettyOut pty -> do
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski let fn = filePrefix ++ "." ++ show ty
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski putIfVerbose opts 2 $ "Writing file: " ++ fn
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski case pty of
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder PrettyXml -> printXml fn
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder PrettyAscii b -> printAscii b fn
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski PrettyHtml -> printHtml fn
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski PrettyLatex b -> writeLibDefnLatex lg b ga fn ld
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder _ -> return () -- implemented elsewhere
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder putIfVerbose opts 3 ("Current OutDir: " ++ odir)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder mapM_ write_type $ outtypes opts
1bb1684c83317dfd1692ab53415027b67d8f2faeTill Mossakowski
7297175957c5ad3c0498032190b1dee9ec5fb873Christian MaederwriteLibDefnLatex :: LogicGraph -> Bool -> GlobalAnnos -> FilePath -> LIB_DEFN
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder -> IO ()
7297175957c5ad3c0498032190b1dee9ec5fb873Christian MaederwriteLibDefnLatex lg lbl ga oup = writeFile oup . renderLatex Nothing
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder . toLatexAux (StripComment False) (MkLabel lbl) ga . prettyLG lg
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder
1bb1684c83317dfd1692ab53415027b67d8f2faeTill MossakowskitoShATermString :: ShATermLG a => a -> IO String
1bb1684c83317dfd1692ab53415027b67d8f2faeTill MossakowskitoShATermString = fmap AT.writeSharedATerm . versionedATermTable
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederwriteShATermFile :: ShATermLG a => FilePath -> a -> IO ()
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederwriteShATermFile fp atcon = toShATermString atcon >>= writeFile fp
7297175957c5ad3c0498032190b1dee9ec5fb873Christian Maeder
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian MaederversionedATermTable :: ShATermLG a => a -> IO ATermTable
587fb54160b66128cf17e4c9bca7494a7f2c3c4aChristian MaederversionedATermTable atcon = do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (att1, versionnr) <- toShATermLG emptyATermTable hetsVersion
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder (att2, aterm) <- toShATermLG att1 atcon
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder return $ fst $ addATerm (ShAAppl "hets" [versionnr, aterm] []) att2
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder
ba904a15082557e939db689fcfba0c68c9a4f740Christian MaederwriteShATermFileSDoc :: ShATermLG a => FilePath -> a -> IO ()
7bf4436b6f9987b070033a323757b206c898c1beChristian MaederwriteShATermFileSDoc fp atcon =
e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski versionedATermTable atcon >>= AT.writeSharedATermFile fp
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder
ba904a15082557e939db689fcfba0c68c9a4f740Christian MaederwriteFileInfo :: ShATermLG a => HetcatsOpts -> LibName
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder -> FilePath -> LIB_DEFN -> a -> IO ()
9603ad7198b72e812688ad7970e4eac4b553837aKlaus LuettichwriteFileInfo opts ln file ld gctx =
9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettich let envFile = snd (getFilePrefix opts file) ++ envSuffix in
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder case analysis opts of
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder Basic -> do
0799b5dc3f06d2640e66e9ab54b8b217348fd719Christian Maeder putIfVerbose opts 2 ("Writing file: " ++ envFile)
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowski Exception.catch (writeShATermFileSDoc envFile (ln, (ld, gctx)))
c616e681da8c052b62e14247fea522da099ac0e4Christian Maeder $ \ err -> do
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder putIfVerbose opts 2 (envFile ++ " not written")
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder putIfVerbose opts 3 ("see following error description:\n"
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maeder ++ shows (err :: SomeException) "\n")
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> putIfVerbose opts 2 ("Not writing " ++ envFile)
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder