WriteFn.hs revision bc263f610d20a9cd3014ddfca903026127fa0d48
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder{-# LANGUAGE CPP #-}
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian MaederModule : $Header$
b03274844ecd270f9e9331f51cc4236a33e2e671Christian MaederDescription : Writing various formats, according to Hets options
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederCopyright : (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian MaederMaintainer : Christian.Maeder@dfki.de
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederStability : provisional
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiPortability : non-portable(DevGraph)
679d3f541f7a9ede4079e045f7758873bb901872Till MossakowskiWriting various formats, according to Hets options
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maedermodule Driver.WriteFn (writeSpecFiles) where
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maederimport Data.List (partition, (\\))
f3faf4e4346b6224a3aaeeac11bac8b5c8932a29Christian Maederimport Common.GlobalAnnotations (GlobalAnnos)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport qualified Data.Map as Map
ba904a15082557e939db689fcfba0c68c9a4f740Christian Maederimport qualified Static.ToXml as ToXml
54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder#ifdef PROGRAMATICA
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maederimport Isabelle.IsaPrint (printIsaTheory)
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder#ifndef NOOWLLOGIC
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maederimport OWL.Print (printOWLBasicTheory)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maederimport OWL.Parse (basicSpec)
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maederimport qualified Static.PrintDevGraph as DG
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maederimport Static.ComputeTheory (theoremsToAxioms, computeTheory)
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder#ifdef HXTFILTER
95c27038582e8a2ce24923bee69ef15931b8b87bChristian MaederwriteVerbFile :: HetcatsOpts -> FilePath -> String -> IO ()
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian MaederwriteVerbFile opts f str = do
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder putIfVerbose opts 2 $ "Writing file: " ++ f
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder writeFile f str
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian MaederwriteLibEnv :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> OutType
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian MaederwriteLibEnv opts filePrefix lenv ln ot =
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder let f = filePrefix ++ "." ++ show ot
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder dg = lookupDGraph ln lenv in case ot of
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder Prf -> toShATermString (ln, lookupHistory ln lenv)
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder >>= writeVerbFile opts f
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder#ifdef HXTFILTER
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder OmdocOut -> hetsToOMDoc opts (ln, lenv) f
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder XmlOut -> writeVerbFile opts f $ ppTopElement $ ToXml.dGraph lenv dg
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder ExperimentalOut ->
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder writeVerbFile opts (filePrefix ++ ".xml")
7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder $ xmlOut $ exportDGraph ln (lookupDGraph ln lenv)
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder GraphOut (Dot showInternalNodeLabels) -> writeVerbFile opts f
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder $ dotGraph showInternalNodeLabels dg
be3f5e3e69900ececafea5b010a8400f26af5362Christian Maeder _ -> return ()
0d0047d6eb457b56ff10987569769a420754a56fChristian MaederwriteSoftFOL :: HetcatsOpts -> FilePath -> G_theory -> LibName -> SIMPLE_ID
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -> SPFType -> Int -> String -> IO ()
0d0047d6eb457b56ff10987569769a420754a56fChristian MaederwriteSoftFOL opts f gTh ln i c n msg = do
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder let cc = case c of
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder ConsistencyCheck -> True
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder ProveTheory -> False
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder mDoc <- printTheoryAsSoftFOL ln i n cc
d11391a2447a2005329a95b5d770f24e62bf5b63Christian Maeder $ (if cc then theoremsToAxioms else id) gTh
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder maybe (putIfVerbose opts 0 $
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder "could not translate to " ++ msg ++ " file: " ++ f)
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder let str = shows d "\n"
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder forget = fmap (const ())
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder case parse (if n == 0 then forget parseSPASS else forget tptp)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder Left err -> putIfVerbose opts 0 $ show err
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder writeVerbFile opts f str) mDoc
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian MaederwriteIsaFile :: HetcatsOpts -> FilePath -> G_theory -> LibName -> SIMPLE_ID
278af20bd154d99e884bdf8c66d35d36699643c9Christian MaederwriteIsaFile opts filePrefix raw_gTh ln i = do
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder let Result ds mTh = createIsaTheory raw_gTh
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder addThn = (++ "_" ++ show i)
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder fp = addThn filePrefix
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder showDiags opts ds
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder putIfVerbose opts 0 $ "could not translate to Isabelle theory: " ++ fp
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder Just (sign, sens) -> do
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder let tn = addThn . reverse . takeWhile (/= '/') . reverse $ case
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder show $ getLibId ln of
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder [] -> filePrefix
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder sf = shows (printIsaTheory tn sign sens) "\n"
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder f = fp ++ ".thy"
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder case parse parseTheory f sf of
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder Left err -> putIfVerbose opts 0 $ show err
81337d455794a0b50fae10b53d0ed85d9e8f2fafChristian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
412aa5e819f3cd18f0be10b5571661036515b151Christian Maeder writeVerbFile opts f sf
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder when (hasPrfOut opts && verbose opts >= 3) $ let
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder (axs, rest) = partition ( \ s -> isAxiom s || isDef s) sens
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder in mapM_ ( \ s -> let
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder tnf = tn ++ "_" ++ senAttr s
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder tf = fp ++ "_" ++ senAttr s ++ ".thy"
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder in writeVerbFile opts tf $ shows
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder (printIsaTheory tnf sign $ s : axs) "\n") rest
46947810076241f06f3e2919edb2289ed84d6c15Christian MaederwriteTheory :: HetcatsOpts -> FilePath -> GlobalAnnos -> G_theory -> LibName
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder -> SIMPLE_ID -> OutType -> IO ()
46947810076241f06f3e2919edb2289ed84d6c15Christian MaederwriteTheory opts filePrefix ga
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder raw_gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) ln i ot =
bd986fa9d0f451b8166efdb9027c153d101aa65bChristian Maeder let fp = filePrefix ++ "_" ++ show i
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder f = fp ++ "." ++ show ot
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder th = (sign0, toNamedList sens0)
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder in case ot of
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder ThyFile -> writeIsaFile opts filePrefix raw_gTh ln i
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder DfgFile c -> writeSoftFOL opts f raw_gTh ln i c 0 "DFG"
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder TPTPFile c -> writeSoftFOL opts f raw_gTh ln i c 1 "TPTP"
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder TheoryFile d -> do
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder if null $ show d then
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder writeVerbFile opts f $ shows (DG.printTh ga i raw_gTh) "\n"
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder else putIfVerbose opts 0 "printing theory delta is not implemented"
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder when (language_name lid == language_name VSE) $ do
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder (sign, sens) <- coerceBasicTheory lid VSE "" th
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder let (sign', sens') = addUniformRestr sign sens
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder lse = map (namedSenToSExpr sign') sens'
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder unless (null lse) $ writeVerbFile opts (fp ++ ".sexpr")
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder $ shows (prettySExpr $ SList lse) "\n"
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder SigFile d -> do
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder if null $ show d then
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder writeVerbFile opts f $ shows (pretty $ signOf raw_gTh) "\n"
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder else putIfVerbose opts 0 "printing signature delta is not implemented"
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder when (language_name lid == language_name VSE) $ do
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder (sign, sens) <- coerceBasicTheory lid VSE "" th
cc4537e2e13b93e08fc8391d3abb8e412cb71b80Christian Maeder let (sign', _sens') = addUniformRestr sign sens
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder writeVerbFile opts (f ++ ".sexpr")
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder $ shows (prettySExpr $ vseSignToSExpr sign') "\n"
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder#ifdef PROGRAMATICA
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder HaskellOut -> case printModule raw_gTh of
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder putIfVerbose opts 0 $ "could not translate to Haskell file: " ++ f
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder Just d -> writeVerbFile opts f $ shows d "\n"
46947810076241f06f3e2919edb2289ed84d6c15Christian Maeder ComptableXml -> if language_name lid == language_name CASL then do
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder th2 <- coerceBasicTheory lid CASL "" th
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder let Result ds res = computeCompTable i th2
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder showDiags opts ds
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder Just td -> writeVerbFile opts f $ tableXmlStr td
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder Nothing -> return ()
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder else putIfVerbose opts 0 $ "expected CASL theory for: " ++ f
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder#ifndef NOOWLLOGIC
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder OWLOut -> if language_name lid == language_name OWL then do
1af66b491a6164e07ac202abfa0d06c6c2462d64Christian Maeder th2 <- coerceBasicTheory lid OWL "" th
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder let owltext = shows (printOWLBasicTheory th2) "\n"
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder case parse (basicSpec >> eof) f owltext of
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder Left err -> putIfVerbose opts 0 $ show err
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder writeVerbFile opts f owltext
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder else putIfVerbose opts 0 $ "expected OWL theory for: " ++ f
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder _ -> return () -- ignore other file types
7297175957c5ad3c0498032190b1dee9ec5fb873Christian MaedermodelSparQCheck :: HetcatsOpts -> G_theory -> SIMPLE_ID -> IO ()
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian MaedermodelSparQCheck opts gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) i =
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder case coerceBasicTheory lid CASL "" (sign0, toNamedList sens0) of
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder Just th2 -> do
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder table <- parseSparQTableFromFile $ modelSparQ opts
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder case table of
95c27038582e8a2ce24923bee69ef15931b8b87bChristian Maeder Left _ -> putIfVerbose opts 0
3f9fabb8ac5cfd9234431ecf19b51ff3e985595aChristian Maeder $ "could not parse SparQTable from file: " ++ modelSparQ opts
3f9fabb8ac5cfd9234431ecf19b51ff3e985595aChristian Maeder Right y -> let Result d _ = modelCheck i th2 y in
de66af0f4b27f08f81c7ca9c573ef9cdf7ca7a07Christian Maeder if length d > 0 then showDiags opts {verbose = 2 } $ take 10 d
c30cfe2a6ab063befdfb47449bc286caee6d8fc3Christian Maeder else putIfVerbose opts 0 "Modelcheck suceeded, no errors found"
12368e292c1abf7eaf975f20ee30ef7820ac5dd5Christian Maeder putIfVerbose opts 0 $ "could not translate Theory to CASL:\n "
278af20bd154d99e884bdf8c66d35d36699643c9Christian Maeder ++ showDoc gTh ""
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian MaederwriteTheoryFiles :: HetcatsOpts -> [OutType] -> FilePath -> LibEnv
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian Maeder -> GlobalAnnos -> LibName -> SIMPLE_ID -> Int -> IO ()
df098122ddc81fe1cb033a151f7305c1dda2dc81Christian MaederwriteTheoryFiles opts specOutTypes filePrefix lenv ga ln i n = do
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder let Result ds mcTh = computeTheory lenv ln n
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder showDiags opts ds
1c8c2b04b40b5c054da07b8d059e5ef29d4dbc32Christian Maeder Nothing -> putIfVerbose opts 0 $ "could not compute theory of spec "
6157bf81d295795067c177aa870fedff83cbe750Christian Maeder Just raw_gTh0 -> do
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder let tr = transNames opts
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski Result es mTh = if null tr then return (raw_gTh0, "") else do
2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder comor <- lookupCompComorphism (map tokStr tr) logicGraph
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder tTh <- mapG_theory comor raw_gTh0
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder return (tTh, show comor)
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder showDiags opts es
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder putIfVerbose opts 0 "could not translate theory"
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder Just (raw_gTh, tStr) -> do
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder unless (null tStr) $
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian Maeder putIfVerbose opts 2 $ "Translated using comorphism " ++ tStr
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski putIfVerbose opts 4 $ "Sublogic of " ++ show i ++ ": " ++
2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder show (sublogicOfTh raw_gTh)
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder unless (modelSparQ opts == "") $
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder modelSparQCheck opts (theoremsToAxioms raw_gTh) i
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder mapM_ (writeTheory opts filePrefix ga raw_gTh ln i) specOutTypes
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederwriteSpecFiles :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> DGraph
95c3e5d11dcee331dc3876a9bf0c1d6daa38e2caChristian MaederwriteSpecFiles opts file lenv0 ln dg = do
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder let gctx = globalEnv dg
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder ga = globalAnnos dg
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder ns = specNames opts
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder filePrefix = snd $ getFilePrefix opts file
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder outTypes = outtypes opts
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder specOutTypes = filter ( \ ot -> case ot of
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder ThyFile -> True
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder DfgFile _ -> True
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder TPTPFile _ -> True
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski XmlOut -> True
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder ExperimentalOut -> True
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski TheoryFile _ -> True
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder SigFile _ -> True
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder OWLOut -> True
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder HaskellOut -> True
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder ComptableXml -> True
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> False) outTypes
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder allSpecs = null ns
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder ignore = null specOutTypes && modelSparQ opts == ""
0d0047d6eb457b56ff10987569769a420754a56fChristian Maeder -- experimental out needs the qualification of names:
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder lenv = if null $ filter (\ ot -> case ot of
9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder ExperimentalOut -> True
a05cad7f2f387b795a71a3aaec543c78e1b89d38Christian Maeder _ -> False) specOutTypes
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder else fromJust $ maybeResult $ qualifyLibEnv lenv0
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder mapM_ (writeLibEnv opts filePrefix lenv ln) $
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder if null $ dumpOpts opts then outTypes else EnvOut : outTypes
5a87ed846cc38cb0e3adf8f736d95614d3e724a3Christian Maeder mapM_ ( \ i -> case Map.lookup i gctx of
e379124f467e5d0ef7d3c0ca238bff0521f70831Till Mossakowski Just (SpecEntry (ExtGenSig _ (NodeSig n _))) ->
c5bc8d60f7c753f81746828329d9e92db1ab7abaChristian Maeder writeTheoryFiles opts specOutTypes filePrefix lenv ga ln i n
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder _ -> if allSpecs then return () else
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder putIfVerbose opts 0 $ "Unknown spec name: " ++ show i
24f14a27a838087b661c2e66fdec4e436ddbd832Christian Maeder ) $ if ignore then [] else
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder if allSpecs then Map.keys gctx else ns
6b00a9239fe7c804524099ca3d25f4ffc6079ceeChristian Maeder mapM_ ( \ n ->
22dd6d9af47163ee081d6c505d0a13dbf40ba87aChristian Maeder writeTheoryFiles opts specOutTypes filePrefix lenv ga ln
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder (genToken $ 'n' : show n) n)
996a56a455d65cfac4ddedd44fd90cfc1ea849aeChristian Maeder $ if ignore || not allSpecs then [] else
b9804822fb178b0fc27ce967a6a8cedc42c5bf90Christian Maeder \\ Map.fold ( \ e l -> case e of
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder SpecEntry (ExtGenSig _ (NodeSig n _)) -> n : l
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder _ -> l) [] gctx
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder doDump opts "GlobalAnnos" $ putStrLn $ showGlobalDoc ga ga ""
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder doDump opts "PrintStat" $ putStrLn $ printStatistics dg
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder doDump opts "DGraph" $ putStrLn $ showDoc dg ""
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder doDump opts "DuplicateDefEdges" $ let es = duplicateDefEdges dg in
a4cb1786d23060c8521a88f08f9909589fa83a12Christian Maeder unless (null es) $ print es
283fdbf051a1cbcfe003ffdcb434564495106f13Christian Maeder doDump opts "LogicGraph" $ putStrLn $ showDoc logicGraph ""
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder doDump opts "LibEnv" $
3d774b4dfa0e459c1a3b08b4aa32c85aa4875362Christian Maeder writeVerbFile opts (filePrefix ++ ".lenv") $
c0380b947eef252db81ee562246bb732555427f4Till Mossakowski shows (DG.prettyLibEnv lenv) "\n"