2665d7759e63acff0bcd4135678f2cc6f2041d46Christian Maeder{-# LANGUAGE CPP #-}
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Writing various formats, according to Hets options
d5fe06af711a6912ae028ebf873eada4ee8733f8Christian MaederCopyright : (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability : provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : non-portable(DevGraph)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiWriting various formats, according to Hets options
a7a43d265fef55ddfd7c4412cd96c621ef9738ffChristian Maeder ( writeSpecFiles
a7a43d265fef55ddfd7c4412cd96c621ef9738ffChristian Maeder , writeVerbFile
b33c310b053e6a4a48dc40e51ba56c50ac37d547notanartistimport Data.List (partition, (\\), intercalate)
8ddb1f6f0aa4eb1836867ba3dde21ac1ec79a58dcmaederimport Common.IRI (IRI, simpleIdToIRI, iriToStringShortUnsecure, setAngles)
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederimport Common.Json (ppJson)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.GlobalAnnotations (GlobalAnnos)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
411392046c2ba1752cde81eaa92a95a2c28b672dChristian Maederimport Logic.Comorphism (targetLogic)
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maederimport qualified Static.PrintDevGraph as DG
46b207daf66b64930a59f3615c8b127aac0b8e43Christian Maederimport qualified Static.ToXml as ToXml
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaederimport qualified Static.ToJson as ToJson
596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maeder#ifdef PROGRAMATICA
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport Isabelle.IsaPrint (printIsaTheory)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksaimport qualified TPTP.Pretty as TPTPPretty
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulzimport FreeCAD.XMLPrinter (exportXMLFC)
ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder#ifndef NOOWLLOGIC
7af6ad49991a7f73b5d4233c89648a5a523f72bdTill Mossakowskiimport OWL2.ParseOWL (convertOWL)
411588cc915b27cef4e7e66fb23e67514b3a0c92Christian Maederimport qualified OWL2.ManchesterPrint as OWL2 (prepareBasicTheory)
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maederimport qualified OWL2.ManchesterParser as OWL2 (basicSpec)
e4f0eaffd002e9e553ee113be33f9aa6e4181c43Christian Maeder#ifdef RDFLOGIC
961978c71545e0177683279f8b63358b3e3804b8Christian Maederimport qualified RDF.Print as RDF (printRDFBasicTheory)
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksaimport qualified CommonLogic.AS_CommonLogic as CL_AS (exportCLIF)
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksaimport qualified CommonLogic.Parse_CLIF as CL_Parse (cltext)
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulzeimport qualified CommonLogic.Print_KIF as Print_KIF (exportKIF)
938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulzimport Driver.ReadFn (libNameToFile)
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulzimport OMDoc.Export (exportLibEnv)
b83ff3749d99d03b641adee264b781039a551addChristian MaederwriteVerbFile :: HetcatsOpts -> FilePath -> String -> IO ()
649fdc0d0502d62d160c150684356fef2c273484Eugen KuksawriteVerbFile opts fullFileName str = do
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa let f = tryToStripPrefix "file://" fullFileName
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder putIfVerbose opts 2 $ "Writing file: " ++ f
520c5bce318eff52d9315f7c4491c3381a0c4336Christian Maeder writeEncFile (ioEncoding opts) f str
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz-- | compute for each LibName in the List a path relative to the given FilePath
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzwriteVerbFiles :: HetcatsOpts -- ^ Hets options
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz -> String -- ^ A suffix to be combined with the libname
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz -> [(LibName, String)] -- ^ An output list
961978c71545e0177683279f8b63358b3e3804b8Christian MaederwriteVerbFiles opts suffix = mapM_ f
938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz where f (ln, s) = writeVerbFile opts (libNameToFile ln ++ suffix) s
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederwriteLibEnv :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> OutType
63719301448519453f66383f4e583d9fd5b89ecbChristian MaederwriteLibEnv opts filePrefix lenv ln ot =
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder let f = filePrefix ++ "." ++ show ot
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder dg = lookupDGraph ln lenv in case ot of
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Prf -> toShATermString (ln, lookupHistory ln lenv)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder >>= writeVerbFile opts f
a43c1a7fa08c12524415386aa13a566cc9e53a4fChristian Maeder XmlOut -> writeVerbFile opts f $ ppTopElement
034d9e2e9ada5aaa5665180720744d51166dacd4Christian Maeder $ ToXml.dGraph opts lenv ln dg
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DbOut -> Persistence.DevGraph.exportLibEnv opts lenv
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder JsonOut -> writeVerbFile opts f $ ppJson
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder $ ToJson.dGraph opts lenv ln dg
427ff3172ae2dfebe3c8fc972735158999997e8aChristian Maeder SymsXml -> writeVerbFile opts f $ ppTopElement
72079df98b3cb7cc1fd82a0a24984893dcd05ecaEwaryst Schulz OmdocOut -> do
5ca1fe655d7d4e35e59a082b5955b306643329d0Ewaryst Schulz let Result ds mOmd = exportLibEnv (recurse opts) (outdir opts) ln lenv
5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulz showDiags opts ds
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz Just omd -> writeVerbFiles opts ".omdoc"
0850c3e5fb6285405ebaeb5aa433985203ac892dEwaryst Schulz $ map (\ (libn, od) -> (libn, xmlOut od)) omd
5f2c34b8971f9ca7e63364b69e167851d001168eEwaryst Schulz Nothing -> putIfVerbose opts 0 "could not translate to OMDoc"
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder GraphOut (Dot showInternalNodeLabels) -> writeVerbFile opts f
4d54e7814b18ce142359c92a5868e6dcff9219b5Christian Maeder $ dotGraph f showInternalNodeLabels "" dg
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder _ -> return ()
aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian MaederwriteSoftFOL :: HetcatsOpts -> FilePath -> G_theory -> IRI
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder -> SPFType -> Int -> String -> IO ()
aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian MaederwriteSoftFOL opts f gTh i c n msg = do
53e165a53dfa59f717588d1f8236c9a763826525Christian Maeder let cc = case c of
53e165a53dfa59f717588d1f8236c9a763826525Christian Maeder ConsistencyCheck -> True
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder ProveTheory -> False
aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian Maeder mDoc <- printTheoryAsSoftFOL i n cc
53e165a53dfa59f717588d1f8236c9a763826525Christian Maeder $ (if cc then theoremsToAxioms else id) gTh
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder maybe (putIfVerbose opts 0 $
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder "could not translate to " ++ msg ++ " file: " ++ f)
08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder let str = shows d "\n"
d27d203b3f42f0e0ecea00e3f19f55f66045bd96Christian Maeder case parse (if n == 0 then forget parseSPASS else forget tptp)
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Left err -> putIfVerbose opts 0 $ show err
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeVerbFile opts f str) mDoc
074f8feaf71e0b71a95145e7439746f8eb8e2a7cChristian MaederwriteFreeCADFile :: HetcatsOpts -> FilePath -> G_theory -> IO ()
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian MaederwriteFreeCADFile opts filePrefix (G_theory lid _ (ExtSign sign _) _ _ _) = do
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz fcSign <- coercePlainSign lid FreeCAD
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz "Expecting a FreeCAD signature for writing FreeCAD xml" sign
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz writeVerbFile opts (filePrefix ++ ".xml") $ exportXMLFC fcSign
ea8e98e298f33f9362293f392c8fb192722b8904Eugen KuksawriteIsaFile :: HetcatsOpts -> FilePath -> G_theory -> LibName -> IRI
e6ac593966607b1da5b619e0f9492d37820eed74Christian MaederwriteIsaFile opts filePrefix raw_gTh ln i = do
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder let Result ds mTh = createIsaTheory raw_gTh
074f8feaf71e0b71a95145e7439746f8eb8e2a7cChristian Maeder addThn = (++ '_' : iriToStringShortUnsecure i)
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder fp = addThn filePrefix
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder showDiags opts ds
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder putIfVerbose opts 0 $ "could not translate to Isabelle theory: " ++ fp
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder Just (sign, sens) -> do
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder let tn = addThn . reverse . takeWhile (/= '/') . reverse $ case
11c3a215d5cf043181e83929f1ce214df65cb587Christian Maeder libToFileName ln of
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder [] -> filePrefix
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder sf = shows (printIsaTheory tn sign sens) "\n"
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder f = fp ++ ".thy"
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder case parse parseTheory f sf of
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Left err -> putIfVerbose opts 0 $ show err
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeVerbFile opts f sf
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder when (hasPrfOut opts && verbose opts >= 3) $ let
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder (axs, rest) = partition ( \ s -> isAxiom s || isDef s) sens
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in mapM_ ( \ s -> let
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder tnf = tn ++ "_" ++ senAttr s
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder tf = fp ++ "_" ++ senAttr s ++ ".thy"
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in writeVerbFile opts tf $ shows
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder (printIsaTheory tnf sign $ s : axs) "\n") rest
a7b34c1a61dabe150288424d90389d5988bf9d7aChristian MaederwriteTheory :: [String] -> String -> HetcatsOpts -> FilePath -> GlobalAnnos
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -> G_theory -> LibName -> IRI -> OutType -> IO ()
a7b34c1a61dabe150288424d90389d5988bf9d7aChristian MaederwriteTheory ins nam opts filePrefix ga
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian Maeder raw_gTh@(G_theory lid _ (ExtSign sign0 _) _ sens0 _) ln i ot =
9e6789e67e329416d7f3acf0e7b8367b8dea991bnotanartist let fp = filePrefix ++ "_" ++ i'
9e6789e67e329416d7f3acf0e7b8367b8dea991bnotanartist i' = encode (iriToStringShortUnsecure $ setAngles False i)
5382091fd2a705e6f026026e8a6adcd3607bdb9fChristian Maeder f = fp ++ "." ++ show ot
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder th = (sign0, toNamedList sens0)
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder lang = language_name lid
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder in case ot of
074f8feaf71e0b71a95145e7439746f8eb8e2a7cChristian Maeder FreeCADOut -> writeFreeCADFile opts filePrefix raw_gTh
e6ac593966607b1da5b619e0f9492d37820eed74Christian Maeder ThyFile -> writeIsaFile opts filePrefix raw_gTh ln i
aad8b6ac810a08fca14ce0fbbf324fcce5305ad6Christian Maeder DfgFile c -> writeSoftFOL opts f raw_gTh i c 0 "DFG"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa | lang == language_name TPTP -> do
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa th2 <- coerceBasicTheory lid TPTP "" th
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa let tptpText = show (TPTPPretty.printBasicTheory th2)
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa writeVerbFile opts f tptpText
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa | otherwise -> putIfVerbose opts 0 $ "expected RDF theory for: " ++ f
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder TheoryFile d -> do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder if null $ show d then
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeVerbFile opts f $ shows (DG.printTh ga i raw_gTh) "\n"
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder else putIfVerbose opts 0 "printing theory delta is not implemented"
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder when (lang == language_name VSE) $ do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder (sign, sens) <- coerceBasicTheory lid VSE "" th
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu let (sign', sens') = addUniformRestr sign sens
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu lse = map (namedSenToSExpr sign') sens'
25662bf82f592e3268fddcc2c86e83c203b82e53Ewaryst Schulz unless (null lse) $ writeVerbFile opts (fp ++ ".sexpr")
21489db35f79507a68ee6e6926e01b8e8ea60c6bChristian Maeder $ shows (prettySExpr $ SList lse) "\n"
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder SigFile d -> do
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder if null $ show d then
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeVerbFile opts f $ shows (pretty $ signOf raw_gTh) "\n"
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder else putIfVerbose opts 0 "printing signature delta is not implemented"
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder when (lang == language_name VSE) $ do
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu (sign, sens) <- coerceBasicTheory lid VSE "" th
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu let (sign', _sens') = addUniformRestr sign sens
7fe976d9f9c4af1aa7636c568d9919859523de0aChristian Maeder writeVerbFile opts (f ++ ".sexpr")
154be5bfac61cf5b61fd1571e7bfc2572c4b546aMihai Codescu $ shows (prettySExpr $ vseSignToSExpr sign') "\n"
486db0a875bcdd0b80cf0d447d14c9c00a92ae94Simon Ulbricht SymXml -> writeVerbFile opts f $ ppTopElement
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa $ ToXml.showSymbolsTh opts ins nam ga raw_gTh
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder#ifdef PROGRAMATICA
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder HaskellOut -> case printModule raw_gTh of
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder putIfVerbose opts 0 $ "could not translate to Haskell file: " ++ f
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just d -> writeVerbFile opts f $ shows d "\n"
21dbca247d5964daf2c5abd2de2ac1101e3e1ef4Christian Maeder ComptableXml -> if lang == language_name CASL then do
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder th2 <- coerceBasicTheory lid CASL "" th
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder let Result ds res = computeCompTable i th2
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder showDiags opts ds
706201451843aa76b8d862de800570c9838c9910Christian Maeder Just td -> writeVerbFile opts f $ tableXmlStr td
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Nothing -> return ()
38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder else putIfVerbose opts 0 $ "expected CASL theory for: " ++ f
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski MedusaJson -> if lang == language_name OWL2 then do
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski th2 <- coerceBasicTheory lid OWL2 "" th
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski let Result ds res = medusa i th2
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski showDiags opts ds
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski Just td -> writeVerbFile opts f $ medusaToJsonString td
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski Nothing -> return ()
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski else putIfVerbose opts 0 $ "expected OWL2 theory for: " ++ f
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist#ifdef RDFLOGIC
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist | lang == language_name RDF -> do
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist th2 <- coerceBasicTheory lid RDF "" th
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist let rdftext = shows (RDF.printRDFBasicTheory th2) "\n"
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist writeVerbFile opts f rdftext
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist | otherwise -> putIfVerbose opts 0 $ "expected RDF theory for: " ++ f
ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder#ifndef NOOWLLOGIC
7bf6fd9cf7a2649a7ec8c72e47ebc69855e3ca84notanartist OWLOut ty -> case ty of
7bf6fd9cf7a2649a7ec8c72e47ebc69855e3ca84notanartist Manchester -> case createOWLTheory raw_gTh of
7bf6fd9cf7a2649a7ec8c72e47ebc69855e3ca84notanartist Result _ Nothing ->
7bf6fd9cf7a2649a7ec8c72e47ebc69855e3ca84notanartist putIfVerbose opts 0 $ "expected OWL theory for: " ++ f
7bf6fd9cf7a2649a7ec8c72e47ebc69855e3ca84notanartist Result ds (Just th2) -> do
411588cc915b27cef4e7e66fb23e67514b3a0c92Christian Maeder let sy = defSyntax opts
411588cc915b27cef4e7e66fb23e67514b3a0c92Christian Maeder ms = if null sy then Nothing
411588cc915b27cef4e7e66fb23e67514b3a0c92Christian Maeder else Just $ simpleIdToIRI $ mkSimpleId sy
411588cc915b27cef4e7e66fb23e67514b3a0c92Christian Maeder owltext = shows
411588cc915b27cef4e7e66fb23e67514b3a0c92Christian Maeder (printTheory ms OWL2 $ OWL2.prepareBasicTheory th2) "\n"
32607d06fe7826eb0711c19d348ee4e395f2577aChristian Maeder showDiags opts ds
411588cc915b27cef4e7e66fb23e67514b3a0c92Christian Maeder when (null sy)
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze $ case parse (OWL2.basicSpec Map.empty >> eof) f owltext of
ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder Left err -> putIfVerbose opts 0 $ show err
ec351e60425e2f99448cb44e933d3828f8025dddChristian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
7bf6fd9cf7a2649a7ec8c72e47ebc69855e3ca84notanartist writeVerbFile opts f owltext
b33c310b053e6a4a48dc40e51ba56c50ac37d547notanartist _ -> let flp = getFilePath ln in case guess flp GuessIn of
b33c310b053e6a4a48dc40e51ba56c50ac37d547notanartist OWLIn _ -> writeVerbFile opts f =<< convertOWL flp (show ty)
b33c310b053e6a4a48dc40e51ba56c50ac37d547notanartist _ -> putIfVerbose opts 0
b33c310b053e6a4a48dc40e51ba56c50ac37d547notanartist $ "OWL output only supported for owl input types ("
b33c310b053e6a4a48dc40e51ba56c50ac37d547notanartist ++ intercalate ", " (map show plainOwlFormats) ++ ")"
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa | lang == language_name CommonLogic -> do
961978c71545e0177683279f8b63358b3e3804b8Christian Maeder (_, th2) <- coerceBasicTheory lid CommonLogic "" th
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa let cltext = shows (CL_AS.exportCLIF th2) "\n"
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze case parse (many (CL_Parse.cltext Map.empty) >> eof) f cltext of
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa Left err -> putIfVerbose opts 0 $ show err
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa _ -> putIfVerbose opts 3 $ "reparsed: " ++ f
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa writeVerbFile opts f cltext
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa | otherwise -> putIfVerbose opts 0 $ "expected Common Logic theory for: "
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze | lang == language_name CommonLogic -> do
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze (_, th2) <- coerceBasicTheory lid CommonLogic "" th
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze let kiftext = shows (Print_KIF.exportKIF th2) "\n"
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze writeVerbFile opts f kiftext
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze | otherwise -> putIfVerbose opts 0 $ "expected Common Logic theory for: "
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder _ -> return () -- ignore other file types
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaedermodelSparQCheck :: HetcatsOpts -> G_theory -> IO ()
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian MaedermodelSparQCheck opts gTh@(G_theory lid _ (ExtSign sign0 _) _ sens0 _) =
b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder case coerceBasicTheory lid CASL "" (sign0, toNamedList sens0) of
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Just th2 -> do
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder table <- parseSparQTableFromFile $ modelSparQ opts
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder case table of
c1168d10047d2c1394b82953158747775a9b4556Christian Maeder Left err -> putIfVerbose opts 0
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $ "could not parse SparQTable from file: " ++ modelSparQ opts
c1168d10047d2c1394b82953158747775a9b4556Christian Maeder ++ "\n" ++ show err
57075b3ac70f37e55f72aa86aa1b70c6ccca8207Christian Maeder Right y -> do
57075b3ac70f37e55f72aa86aa1b70c6ccca8207Christian Maeder putIfVerbose opts 4 $ unlines
57075b3ac70f37e55f72aa86aa1b70c6ccca8207Christian Maeder ["lisp file content:", show $ table2Doc y, "lisp file end."]
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder let Result d _ = modelCheck (counterSparQ opts) th2 y
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder if null d then
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder putIfVerbose opts 0 "Modelcheck succeeded, no errors found"
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder else showDiags
d34c6711bc746459074986c06f7c28b083b4be2fChristian Maeder (if verbose opts >= 2 then opts else opts {verbose = 2}) d
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder putIfVerbose opts 0 $ "could not translate Theory to CASL:\n "
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder ++ showDoc gTh ""
8865728716566f42fa73e7e0bc080ba3225df764Christian MaederwriteTheoryFiles :: HetcatsOpts -> [OutType] -> FilePath -> LibEnv
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa -> GlobalAnnos -> LibName -> IRI -> Int -> IO ()
1937dccb04b363364f7a7de17fdaae1d70583af9Christian MaederwriteTheoryFiles opts specOutTypes filePrefix lenv ga ln i n =
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder let dg = lookupDGraph ln lenv
a7b34c1a61dabe150288424d90389d5988bf9d7aChristian Maeder nam = getDGNodeName $ labDG dg n
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder ins = getImportNames dg n
bb9642ff292545658dc11251b83a7b7af3c1fccbChristian Maeder in case globalNodeTheory dg n of
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder Nothing -> putIfVerbose opts 0 $ "could not compute theory of spec "
6c08e47c4275556c18f4f89521bf21fe94c28dd5Christian Maeder Just raw_gTh0 -> do
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let tr = transNames opts
f6b2c6c33c635279973b8f378470da7dbb8ecee8Christian Maeder Result es mTh = if null tr then return (raw_gTh0, "") else do
78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder comor <- lookupCompComorphism (map tokStr tr) logicGraph
78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder tTh <- mapG_theory comor raw_gTh0
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder return (tTh, "Translated using comorphism " ++ show comor)
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder (raw_gTh, tStr) =
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder fromMaybe (raw_gTh0, "Keeping untranslated theory") mTh
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder showDiags opts $ map (updDiagKind
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder (\ k -> if k == Error then Warning else k)) es
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder unless (null tStr) $ putIfVerbose opts 2 tStr
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder putIfVerbose opts 4 $ "Sublogic of " ++ show i ++ ": " ++
4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder show (sublogicOfTh raw_gTh)
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder unless (modelSparQ opts == "") $
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder modelSparQCheck opts (theoremsToAxioms raw_gTh)
eaa88a5cefdc814e61039c5dcc1bffc324a2f93eChristian Maeder mapM_ (writeTheory ins nam opts filePrefix ga raw_gTh ln i)
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian MaederwriteSpecFiles :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> DGraph
938677803842b384a91fef21f58f86b8e3188b43Ewaryst SchulzwriteSpecFiles opts file lenv ln dg = do
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder let gctx = globalEnv dg
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder mns = map $ \ t -> Map.findWithDefault (simpleIdToIRI t) (tokStr t)
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder $ Map.fromList $ map (\ i -> (iriToStringShortUnsecure i, i)) gns
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ga = globalAnnos dg
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder ns = mns $ specNames opts
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder vs = mns $ viewNames opts
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder filePrefix = snd $ getFilePrefix opts file
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder outTypes = outtypes opts
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder specOutTypes = filter ( \ ot -> case ot of
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder ThyFile -> True
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder DfgFile _ -> True
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTPFile -> True
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder XmlOut -> True
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder JsonOut -> True
938677803842b384a91fef21f58f86b8e3188b43Ewaryst Schulz OmdocOut -> True
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder TheoryFile _ -> True
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder SigFile _ -> True
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist OWLOut _ -> True
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa CLIFOut -> True
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze KIFOut -> True
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz FreeCADOut -> True
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder HaskellOut -> True
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder ComptableXml -> True
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski MedusaJson -> True
c30231257d9116b514dce02703a515fe21cd427dTill Mossakowski SymXml -> True
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder _ -> False) outTypes
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder allSpecs = null ns
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder noViews = null vs
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ignore = null specOutTypes && modelSparQ opts == ""
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder mapM_ (writeLibEnv opts filePrefix lenv ln) $
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder if null $ dumpOpts opts then outTypes else EnvOut : outTypes
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder mapM_ ( \ i -> case Map.lookup i gctx of
ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder Just (SpecEntry (ExtGenSig _ (NodeSig n _))) ->
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeTheoryFiles opts specOutTypes filePrefix lenv ga ln i n
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder _ -> unless allSpecs
1937dccb04b363364f7a7de17fdaae1d70583af9Christian Maeder $ putIfVerbose opts 0 $ "Unknown spec name: " ++ show i
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder ) $ if ignore then [] else
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder if allSpecs then gns else ns
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder unless noViews $
35cb254f1f46a6f33b5c24111a37fbab49d79cfeChristian Maeder mapM_ ( \ i -> case Map.lookup i gctx of
88e08f20c80fea4b7892bbb5e70c5002f7c1da18Christian Maeder Just (ViewOrStructEntry _ (ExtViewSig _ (GMorphism cid _ _ m _) _)) ->
ef4c609cebc5260771dae6e4f3a54a8959e81ed9Christian Maeder writeVerbFile opts (filePrefix ++ "_" ++ show i ++ ".view")
180ab8c3df8cb0c88f0e881bca93354df6b5d560Christian Maeder $ shows (pretty $ Map.toList $ symmap_of (targetLogic cid) m) "\n"
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder _ -> putIfVerbose opts 0 $ "Unknown view name: " ++ show i
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder mapM_ ( \ n ->
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeTheoryFiles opts specOutTypes filePrefix lenv ga ln
ea8e98e298f33f9362293f392c8fb192722b8904Eugen Kuksa (simpleIdToIRI $ genToken $ 'n' : show n) n)
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder $ if ignore || not allSpecs then [] else
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder \\ Map.fold ( \ e l -> case e of
ef2affdc0cdf3acd5c051597c04ab9b08a346a7dChristian Maeder SpecEntry (ExtGenSig _ (NodeSig n _)) -> n : l
3143271856dbf456bd7acc1c07193173f886d986Christian Maeder _ -> l) [] gctx
63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder doDump opts "GlobalAnnos" $ putStrLn $ showGlobalDoc ga ga ""
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder doDump opts "PrintStat" $ putStrLn $ printStatistics dg
ce900a84ed9d9882c64fccbd6300f6b0d67efa82Christian Maeder doDump opts "DGraph" $ putStrLn $ showDoc dg ""
fb37a248ebad4696bbc9d9b94ce1cfc6497a9160Christian Maeder doDump opts "DuplicateDefEdges" $ let es = duplicateDefEdges dg in
fb37a248ebad4696bbc9d9b94ce1cfc6497a9160Christian Maeder unless (null es) $ print es
f527d5da7cd679c1a9b50a4906a0c12d395a6087Christian Maeder doDump opts "LibEnv" $ writeVerbFile opts (filePrefix ++ ".lenv")
f527d5da7cd679c1a9b50a4906a0c12d395a6087Christian Maeder $ shows (DG.prettyLibEnv lenv) "\n"
9175e29c044318498a40f323f189f9dfd50378efChristian MaederwriteLG :: HetcatsOpts -> IO ()
9175e29c044318498a40f323f189f9dfd50378efChristian MaederwriteLG opts = do
9175e29c044318498a40f323f189f9dfd50378efChristian Maeder doDump opts "LogicGraph" $ putStrLn $ showDoc logicGraph ""
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let writeLGXML = do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa lG <- lGToXml logicGraph
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa writeVerbFile opts { verbose = 2 } (outdir opts </> "LogicGraph.xml")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa $ ppTopElement lG
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa if null $ outtypes opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa then writeLGXML
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa mapM_ (\ outtype -> case outtype of
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa XmlOut -> writeLGXML
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa JsonOut -> do
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa lG <- lGToJson logicGraph
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa writeVerbFile opts { verbose = 2 } (outdir opts </> "LogicGraph.json")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DbOut -> Persistence.LogicGraph.exportLogicGraph opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa _ -> return ()
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ) $ outtypes opts