5c6b95ba1b2e35f8dd6b0a7f25aacba91fff3aa2Tinderbox User{- |

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsModule : $Header$

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsDescription : Writing out a HetCASL library

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsCopyright : (c) Klaus L�ttich, C.Maeder, Uni Bremen 2002-2006

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark Andrews

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsMaintainer : Christian.Maeder@dfki.de

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsStability : provisional

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsPortability : non-portable(DevGraph)

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark Andrews

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark AndrewsWriting out HetCASL env files as much as is needed for

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark Andrewsthe static analysis

bf8267aa453e5d2a735ed732a043b77a0b355b20Mark Andrews-}

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrews

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsmodule Driver.WriteLibDefn where

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrews

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.Utils

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.Doc

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.DocUtils

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.LibName

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.PrintLaTeX

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.GlobalAnnotations (GlobalAnnos)

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.ConvertGlobalAnnos ()

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.SimpPretty (writeFileSDoc)

d0522678a12b3a3a430bfb48839b3d8c70cadf49Mark Andrews

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.ATerm.Lib

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport Common.ATerm.ReadWrite

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrews

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport ATC.AS_Library ()

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsimport ATC.DevGraph ()

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Hunt

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Huntimport Syntax.AS_Library (LIB_DEFN())

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Huntimport Syntax.Print_AS_Library ()

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Hunt

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Huntimport Driver.Options

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Hunt

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Hunt-- | compute the prefix for files to be written out

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan HuntgetFilePrefix :: HetcatsOpts -> FilePath -> (FilePath, FilePath)

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan HuntgetFilePrefix opts file =

4bf686cf5d6b83981abdf2d8157c829922acc6d4Evan Hunt let odir' = outdir opts

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt (base, path, _) = fileparse (envSuffix : downloadExtensions) file

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt odir = if null odir' then path else odir'

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt in (odir, pathAndBase odir base)

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt{- |

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt Write the given LIB_DEFN in every format that HetcatsOpts includes.

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt Filenames are determined by the output formats.

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt-}

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Huntwrite_LIB_DEFN :: GlobalAnnos -> FilePath -> HetcatsOpts -> LIB_DEFN -> IO ()

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Huntwrite_LIB_DEFN ga file opts ld = do

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt let (odir, filePrefix) = getFilePrefix opts file

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt filename ty = filePrefix ++ "." ++ show ty

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews verbMesg ty = putIfVerbose opts 2 $ "Writing file: " ++ filename ty

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews printAscii ty = do

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews verbMesg ty

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews write_casl_asc opts ga (filename ty) ld

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews write_type :: OutType -> IO ()

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews write_type t = case t of

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews PrettyOut PrettyAscii -> printAscii t

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews PrettyOut PrettyLatex -> do

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews verbMesg t

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews write_casl_latex opts ga (filename t) ld

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews _ -> return () -- implemented elsewhere

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews putIfVerbose opts 3 ("Current OutDir: " ++ odir)

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews mapM_ write_type $ outtypes opts

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrews

26bb3b7a67b833f0a18072567de036226890ca1aMark Andrewswrite_casl_asc :: HetcatsOpts -> GlobalAnnos -> FilePath -> LIB_DEFN -> IO ()

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Huntwrite_casl_asc _ ga oup ld = writeFile oup $

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt shows (useGlobalAnnos ga $ pretty ld) "\n"

578e3196076b409c509c6c0a0873e7bfe54f4d61Evan Hunt

c1ced49662181d2fb2343ed7bde71d170f0d1119Mark Andrewsdebug_latex_filename :: FilePath -> FilePath

debug_latex_filename =

( \ (b, p, _) -> p ++ b ++ ".debug.tex") . fileparse [".pp.tex"]

write_casl_latex :: HetcatsOpts -> GlobalAnnos -> FilePath -> LIB_DEFN -> IO ()

write_casl_latex opts ga oup ld =

do let ldoc = toLatex ga $ pretty ld

writeFile oup $ renderLatex Nothing ldoc

doDump opts "DebugLatex" $

writeFile (debug_latex_filename oup) $

debugRenderLatex Nothing ldoc

toShATermString :: (ShATermConvertible a) => a -> IO String

toShATermString atcon = fmap writeSharedATerm $ versionedATermTable atcon

writeShATermFile :: (ShATermConvertible a) => FilePath -> a -> IO ()

writeShATermFile fp atcon = toShATermString atcon >>= writeFile fp

versionedATermTable :: (ShATermConvertible a) => a -> IO ATermTable

versionedATermTable atcon = do

att0 <- newATermTable

(att1, versionnr) <- toShATermAux att0 hetsVersion

(att2, aterm) <- toShATermAux att1 atcon

return $ fst $ addATerm (ShAAppl "hets" [versionnr,aterm] []) att2

writeShATermFileSDoc :: (ShATermConvertible a) => FilePath -> a -> IO ()

writeShATermFileSDoc fp atcon = do

att <- versionedATermTable atcon

writeFileSDoc fp $ writeSharedATermSDoc att

writeFileInfo :: (ShATermConvertible a) => HetcatsOpts -> LIB_NAME

-> FilePath -> LIB_DEFN -> a -> IO ()

writeFileInfo opts ln file ld gctx =

let envFile = snd (getFilePrefix opts file) ++ envSuffix in

case analysis opts of

Basic -> do

putIfVerbose opts 2 ("Writing file: " ++ envFile)

catch (writeShATermFileSDoc envFile (ln, (ld, gctx))) $ \ err -> do

putIfVerbose opts 2 (envFile ++ " not written")

putIfVerbose opts 3 ("see following error description:\n"

++ shows err "\n")

_ -> putIfVerbose opts 2 ("Not writing " ++ envFile)