WriteFn.hs revision 734257b9ea9fcaa18d4e3627f54f5295a99aa1f7
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# LANGUAGE CPP #-}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederModule : $Header$
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederDescription : Writing various formats, according to Hets options
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable(DevGraph)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederWriting various formats, according to Hets options
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedermodule Driver.WriteFn (writeSpecFiles, writeVerbFile) where
a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Data.List (partition, (\\))
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowskiimport Common.GlobalAnnotations (GlobalAnnos)
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport qualified Data.Map as Map
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Logic.Comorphism (targetLogic)
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maederimport qualified Static.ToXml as ToXml
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder#ifdef PROGRAMATICA
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederimport Isabelle.IsaPrint (printIsaTheory)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederimport FreeCAD.XMLPrinter (exportXMLFC)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder#ifndef NOOWLLOGIC
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maederimport qualified OWL2.ManchesterPrint as OWL2 (printOWLBasicTheory)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport qualified OWL2.ManchesterParser as OWL2 (basicSpec)
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder#ifdef RDFLOGIC
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder-- import qualified RDF.Print as RDF (printRDFBasicTheory)
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maederimport qualified CommonLogic.AS_CommonLogic as CL_AS (exportCLIF)
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maederimport qualified CommonLogic.Parse_CLIF as CL_Parse (cltext)
c2a4d8ae266aa37cc922eba97077520229a19902Christian Maederimport qualified Static.PrintDevGraph as DG
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maederimport Static.ComputeTheory (theoremsToAxioms, computeTheory)
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wangimport Driver.ReadFn (libNameToFile)
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettichimport OMDoc.Export (exportLibEnv)
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus LuettichwriteVerbFile :: HetcatsOpts -> FilePath -> String -> IO ()
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik LueckewriteVerbFile opts f str = do
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder putIfVerbose opts 2 $ "Writing file: " ++ f
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder writeEncFile (ioEncoding opts) f str
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-- | compute for each LibName in the List a path relative to the given FilePath
8a28707e9155465c6f2236a06eac6580a65c7025Christian MaederwriteVerbFiles :: HetcatsOpts -- ^ Hets options
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich -> String -- ^ A suffix to be combined with the libname
ea0dd71829400e24c3d8a7b7440cd6b42c34a3b8Christian Maeder -> [(LibName, String)] -- ^ An output list
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederwriteVerbFiles opts suffix outl =
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder where f (ln, s) = writeVerbFile opts (libNameToFile ln ++ suffix) s
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederwriteLibEnv :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> OutType
9e748851c150e1022fb952bab3315e869aaf0214Christian MaederwriteLibEnv opts filePrefix lenv ln ot =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let f = filePrefix ++ "." ++ show ot
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder dg = lookupDGraph ln lenv in case ot of
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Prf -> toShATermString (ln, lookupHistory ln lenv)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder >>= writeVerbFile opts f
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder XmlOut -> writeVerbFile opts f $ ppTopElement
15503d903d142d317200149b2d1d642053530365Christian Maeder OmdocOut -> do
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder let Result ds mOmd = exportLibEnv (recurse opts) (outdir opts) ln lenv
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder showDiags opts ds
776a1a086df734581431e6edb4343ed4c8d34d55Christian Maeder Just omd -> writeVerbFiles opts ".omdoc"
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder $ map (\ (libn, od) -> (libn, xmlOut od)) omd
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder Nothing -> putIfVerbose opts 0 "could not translate to OMDoc"
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder GraphOut (Dot showInternalNodeLabels) -> writeVerbFile opts f
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder $ dotGraph f showInternalNodeLabels "" dg
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder _ -> return ()
c0c2380bced8159ff0297ece14eba948bd236471Christian MaederwriteSoftFOL :: HetcatsOpts -> FilePath -> G_theory -> LibName -> SIMPLE_ID
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder -> SPFType -> Int -> String -> IO ()
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederwriteSoftFOL opts f gTh ln i c n msg = do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let cc = case c of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ConsistencyCheck -> True
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ProveTheory -> False
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder mDoc <- printTheoryAsSoftFOL ln i n cc
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder $ (if cc then theoremsToAxioms else id) gTh
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder maybe (putIfVerbose opts 0 $
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder "could not translate to " ++ msg ++ " file: " ++ f)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let str = shows d "\n"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder case parse (if n == 0 then forget parseSPASS else forget tptp)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Left err -> putIfVerbose opts 0 $ show err
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder writeVerbFile opts f str) mDoc
2d130d212db7208777ca896a7ecad619a8944971Christian MaederwriteFreeCADFile :: HetcatsOpts -> FilePath -> G_theory -> LibName -> SIMPLE_ID
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian MaederwriteFreeCADFile opts filePrefix (G_theory lid (ExtSign sign _) _ _ _) _ _ = do
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder fcSign <- coercePlainSign lid FreeCAD
bc8cbf12aa172bf5673b92a9e7a0151d4aa4c315Christian Maeder "Expecting a FreeCAD signature for writing FreeCAD xml" sign
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder writeVerbFile opts (filePrefix ++ ".xml") $ exportXMLFC fcSign
2d130d212db7208777ca896a7ecad619a8944971Christian MaederwriteIsaFile :: HetcatsOpts -> FilePath -> G_theory -> LibName -> SIMPLE_ID
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian MaederwriteIsaFile opts filePrefix raw_gTh ln i = do
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder let Result ds mTh = createIsaTheory raw_gTh
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder addThn = (++ '_' : show i)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder fp = addThn filePrefix
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder showDiags opts ds
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder putIfVerbose opts 0 $ "could not translate to Isabelle theory: " ++ fp
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder Just (sign, sens) -> do
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder let tn = addThn . reverse . takeWhile (/= '/') . reverse $ case
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder show $ getLibId ln of
88318aafc287e92931dceffbb943d58a9310001dChristian Maeder [] -> filePrefix
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder sf = shows (printIsaTheory tn sign sens) "\n"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder f = fp ++ ".thy"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder case parse parseTheory f sf of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Left err -> putIfVerbose opts 0 $ show err
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder writeVerbFile opts f sf
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder when (hasPrfOut opts && verbose opts >= 3) $ let
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder (axs, rest) = partition ( \ s -> isAxiom s || isDef s) sens
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder in mapM_ ( \ s -> let
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder tnf = tn ++ "_" ++ senAttr s
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder tf = fp ++ "_" ++ senAttr s ++ ".thy"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder in writeVerbFile opts tf $ shows
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder (printIsaTheory tnf sign $ s : axs) "\n") rest
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederwriteTheory :: HetcatsOpts -> FilePath -> GlobalAnnos -> G_theory -> LibName
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich -> SIMPLE_ID -> OutType -> IO ()
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederwriteTheory opts filePrefix ga
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder raw_gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) ln i ot =
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let fp = filePrefix ++ "_" ++ show i
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder f = fp ++ "." ++ show ot
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder th = (sign0, toNamedList sens0)
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder lang = language_name lid
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder in case ot of
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder FreeCADOut -> writeFreeCADFile opts filePrefix raw_gTh ln i
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder ThyFile -> writeIsaFile opts filePrefix raw_gTh ln i
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder DfgFile c -> writeSoftFOL opts f raw_gTh ln i c 0 "DFG"
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder TPTPFile c -> writeSoftFOL opts f raw_gTh ln i c 1 "TPTP"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder TheoryFile d -> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder if null $ show d then
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeVerbFile opts f $ shows (DG.printTh ga i raw_gTh) "\n"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder else putIfVerbose opts 0 "printing theory delta is not implemented"
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder when (lang == language_name VSE) $ do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder (sign, sens) <- coerceBasicTheory lid VSE "" th
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let (sign', sens') = addUniformRestr sign sens
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder lse = map (namedSenToSExpr sign') sens'
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder unless (null lse) $ writeVerbFile opts (fp ++ ".sexpr")
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ shows (prettySExpr $ SList lse) "\n"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder SigFile d -> do
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder if null $ show d then
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder writeVerbFile opts f $ shows (pretty $ signOf raw_gTh) "\n"
d946c1bfdd7d58aa7c023efe864d5999eb44a61bChristian Maeder else putIfVerbose opts 0 "printing signature delta is not implemented"
89f7631cbfbd1bb99fc152b434bd362a7799d295Christian Maeder when (lang == language_name VSE) $ do
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder (sign, sens) <- coerceBasicTheory lid VSE "" th
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let (sign', _sens') = addUniformRestr sign sens
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder writeVerbFile opts (f ++ ".sexpr")
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder $ shows (prettySExpr $ vseSignToSExpr sign') "\n"
f4505a64a089693012a3f5c3b1f12a82cd7a2a5aKlaus Luettich writeVerbFile opts f $ ToXml.showSymbolsTh raw_gTh
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder#ifdef PROGRAMATICA
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder HaskellOut -> case printModule raw_gTh of
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder putIfVerbose opts 0 $ "could not translate to Haskell file: " ++ f
4ed0007ac9caea5b468f202521352d153481423cChristian Maeder Just d -> writeVerbFile opts f $ shows d "\n"
2c619a4dfdc1df27573eba98e81ed1ace906941dChristian Maeder ComptableXml -> if lang == language_name CASL then do
b886e9e5db2098d0112cc4f70aeba232962939ddChristian Maeder th2 <- coerceBasicTheory lid CASL "" th
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder let Result ds res = computeCompTable i th2
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder showDiags opts ds
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Just td -> writeVerbFile opts f $ tableXmlStr td
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder Nothing -> return ()
42b12fba6830ada5057949f825fc27edf5574e5fChristian Maeder else putIfVerbose opts 0 $ "expected CASL theory for: " ++ f
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#ifndef NOOWLLOGIC
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder | lang == language_name OWL2 -> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder th2 <- coerceBasicTheory lid OWL2 "" th
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let owltext = shows (OWL2.printOWLBasicTheory th2) "\n"
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder case parse (OWL2.basicSpec >> eof) f owltext of
9df11f85fd7f8c4745d64464876e84ec4e263692Christian Maeder Left err -> putIfVerbose opts 0 $ show err
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
6770ec11184086a81daddba75e0cd1f45a2eff96Christian Maeder writeVerbFile opts f owltext
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich | otherwise -> putIfVerbose opts 0 $ "expected OWL theory for: " ++ f
cf04ba46b9eb495d334466e24e082e391055ca7bDominik Luecke#ifdef RDFLOGIC
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder | lang == language_name RDF -> do
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder th2 <- coerceBasicTheory lid RDF "" th
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder let rdftext = shows (RDF.printRDFBasicTheory th2) "\n"
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder writeVerbFile opts f rdftext
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers | otherwise -> putIfVerbose opts 0 $ "expected RDF theory for: " ++ f
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder | lang == language_name CommonLogic -> do
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder (_,th2) <- coerceBasicTheory lid CommonLogic "" th
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder let cltext = shows (CL_AS.exportCLIF th2) "\n"
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder case parse ((many CL_Parse.cltext) >> eof) f cltext of
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder Left err -> putIfVerbose opts 0 $ show err
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder writeVerbFile opts f cltext
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder | otherwise -> putIfVerbose opts 0 $ "expected Common Logic theory for: "
819e29dba060687cf391e444e0f6ff88c1908cc3Christian Maeder _ -> return () -- ignore other file types
819e29dba060687cf391e444e0f6ff88c1908cc3Christian MaedermodelSparQCheck :: HetcatsOpts -> G_theory -> SIMPLE_ID -> IO ()
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaedermodelSparQCheck opts gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) i =
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case coerceBasicTheory lid CASL "" (sign0, toNamedList sens0) of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just th2 -> do
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder table <- parseSparQTableFromFile $ modelSparQ opts
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder case table of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Left _ -> putIfVerbose opts 0
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder $ "could not parse SparQTable from file: " ++ modelSparQ opts
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Right y -> let Result d _ = modelCheck i th2 y in
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder if length d > 0 then showDiags opts {verbose = 2 } $ take 10 d
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder else putIfVerbose opts 0 "Modelcheck suceeded, no errors found"
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder putIfVerbose opts 0 $ "could not translate Theory to CASL:\n "
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ++ showDoc gTh ""
ac34194a668399bb8ef238da77c3a09e93fb253bChristian MaederwriteTheoryFiles :: HetcatsOpts -> [OutType] -> FilePath -> LibEnv
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder -> GlobalAnnos -> LibName -> SIMPLE_ID -> Int -> IO ()
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian MaederwriteTheoryFiles opts specOutTypes filePrefix lenv ga ln i n =
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder case computeTheory lenv ln n of
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maeder Nothing -> putIfVerbose opts 0 $ "could not compute theory of spec "
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Just raw_gTh0 -> do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let tr = transNames opts
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Result es mTh = if null tr then return (raw_gTh0, "") else do
6fe9628743562678acf97d6730ebcfee5e9e50c2Christian Maeder comor <- lookupCompComorphism (map tokStr tr) logicGraph
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder tTh <- mapG_theory comor raw_gTh0
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder return (tTh, show comor)
5ad5dffe06818a13e1632b1119fbca7881085fc1Dominik Luecke showDiags opts es
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder putIfVerbose opts 0 "could not translate theory"
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski Just (raw_gTh, tStr) -> do
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder unless (null tStr) $
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder putIfVerbose opts 2 $ "Translated using comorphism " ++ tStr
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder putIfVerbose opts 4 $ "Sublogic of " ++ show i ++ ": " ++
0b349288edfa50fdf38fda1a14e1562d03f92574Christian Maeder show (sublogicOfTh raw_gTh)
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder unless (modelSparQ opts == "") $
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich modelSparQCheck opts (theoremsToAxioms raw_gTh) i
fb328c4f646dd3dd78a9391c5cb58450a3dd0aa9Klaus Luettich mapM_ (writeTheory opts filePrefix ga raw_gTh ln i) specOutTypes
e96a0bf4040fd789339958c01f145c5057d26db6René WagnerwriteSpecFiles :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> DGraph
abf2487c3aece95c371ea89ac64319370dcb6483Klaus LuettichwriteSpecFiles opts file lenv ln dg = do
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder let gctx = globalEnv dg
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ga = globalAnnos dg
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder ns = specNames opts
8b0f493ae42bad8b94918cc0957f1af57096cda4Felix Reckers vs = viewNames opts
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder filePrefix = snd $ getFilePrefix opts file
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder outTypes = outtypes opts
b9b960bc75e34658e70c4a0231dbc6a6e7373f2dChristian Maeder specOutTypes = filter ( \ ot -> case ot of
18a4d5cb6828f080db9c5f9551785c5151027271Christian Maeder ThyFile -> True
0be0db405c49906bd7057255069bf6df53395ac9Klaus Luettich DfgFile _ -> True
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder TPTPFile _ -> True
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder XmlOut -> True
fdb2d618144159395f7bf8ce3327b3c112a17dd3Till Mossakowski OmdocOut -> True
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder TheoryFile _ -> True
383aa66e5142365fe9b1f88b18c1da5b27cc8c04Christian Maeder SigFile _ -> True
3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowski OWLOut -> True
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder CLIFOut -> True
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder FreeCADOut -> True
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder HaskellOut -> True
d8bebe0559abdfcd912ac68cf0948fe601249a66Christian Maeder ComptableXml -> True
edd1b7f4720bc2eea51fa0685417e1e4f3be4915Klaus Luettich SymXml -> True
9a5fda85e9eaf0e6a18d0dd2b8535805c5135e9aDominik Luecke _ -> False) outTypes
63e50b4c36074d5fb9de872c4007b688b4bce534Christian Maeder allSpecs = null ns
bd54a9917cd87169b8e40bcc5616c537fed85815Christian Maeder noViews = null vs
be218d4b48c5447b7b08c1e323e048a0cfae2d6eHendrik Iben ignore = null specOutTypes && modelSparQ opts == ""
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder mapM_ (writeLibEnv opts filePrefix lenv ln) $
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder if null $ dumpOpts opts then outTypes else EnvOut : outTypes
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder mapM_ ( \ i -> case Map.lookup i gctx of
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder Just (SpecEntry (ExtGenSig _ (NodeSig n _))) ->
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder writeTheoryFiles opts specOutTypes filePrefix lenv ga ln i n
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder _ -> unless allSpecs
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ putIfVerbose opts 0 $ "Unknown spec name: " ++ show i
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ) $ if ignore then [] else
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder if allSpecs then Map.keys gctx else ns
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder unless noViews $
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder mapM_ ( \ i -> case Map.lookup i gctx of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Just (ViewOrStructEntry _ (ExtViewSig _ (GMorphism cid _ _ m _) _)) ->
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder writeVerbFile opts (filePrefix ++ "_" ++ show i ++ ".view")
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich $ shows (pretty $ Map.toList $ symmap_of (targetLogic cid) m) "\n"
e8db9a65830cf71504e33c6f441a67b4d184a3caChristian Maeder _ -> putIfVerbose opts 0 $ "Unknown view name: " ++ show i
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder mapM_ ( \ n ->
1f8a7f8343f7df719768d2b1d7e3077ee291a1caChristian Maeder writeTheoryFiles opts specOutTypes filePrefix lenv ga ln
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder (genToken $ 'n' : show n) n)
6bf24e5eb644064ad650eb3fd9774483fccbf601Christian Maeder $ if ignore || not allSpecs then [] else
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke \\ Map.fold ( \ e l -> case e of
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder SpecEntry (ExtGenSig _ (NodeSig n _)) -> n : l
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke _ -> l) [] gctx
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder doDump opts "GlobalAnnos" $ putStrLn $ showGlobalDoc ga ga ""
53818ced114da21321063fff307aa41c1ab31dd3Achim Mahnke doDump opts "PrintStat" $ putStrLn $ printStatistics dg
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder doDump opts "DGraph" $ putStrLn $ showDoc dg ""
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder doDump opts "DuplicateDefEdges" $ let es = duplicateDefEdges dg in
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder unless (null es) $ print es
3e61f574717499939bd8e0ff538ea9e7b72d4e2dKlaus Luettich doDump opts "LogicGraph" $ putStrLn $ showDoc logicGraph ""
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder doDump opts "LibEnv" $
27785f379d6810811b4e6d23feab18845fde9a98Christian Maeder writeVerbFile opts (filePrefix ++ ".lenv") $
f443a57f2a8e0ca3daa7431b0c89a18ba52c337aChristian Maeder shows (DG.prettyLibEnv lenv) "\n"