f26489cf50364d60a14c9bf33ca2c91855ad438aChristian Maeder{-# LANGUAGE CPP #-}

9658657e918981d91c8647ed8c220464f10a6235Christian Maeder{- |

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederModule : $Header$

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Writing various formats, according to Hets options

1954518162694c2ef8e0e1263283dd3c75e9ca72Christian MaederCopyright : (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability : provisional

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : non-portable(DevGraph)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiWriting various formats, according to Hets options

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-}

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maedermodule Driver.WriteFn (writeSpecFiles, writeVerbFile) where

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maederimport Control.Monad

ae35311385999d91f812155fe99439724d54063bChristian Maederimport Text.ParserCombinators.Parsec

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport Text.XML.Light

3143271856dbf456bd7acc1c07193173f886d986Christian Maederimport Data.List (partition, (\\))

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport Common.AS_Annotation

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Id

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport Common.IRI (IRI, simpleIdToIRI, iriToStringShortUnsecure)

28bec3c11488588bcc3c8eae6996c8d9dbe582bdChristian Maederimport Common.DocUtils

47d6bc7bc9a708427f96be8d805f712697ad3d9eChristian Maederimport Common.ExtSign

f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederimport Common.LibName

28bec3c11488588bcc3c8eae6996c8d9dbe582bdChristian Maederimport Common.Result

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.Parsec (forget)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Common.GlobalAnnotations (GlobalAnnos)

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport qualified Data.Map as Map

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.SExpr

64c2422e1ba0691556a6639e959820add102315cChristian Maederimport Common.IO

64c2422e1ba0691556a6639e959820add102315cChristian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Coerce

c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maederimport Logic.Comorphism (targetLogic)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Logic.Logic

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport Logic.Grothendieck

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport Comorphisms.LogicGraph

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maederimport qualified Static.ToXml as ToXml

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport CASL.Logic_CASL

28bec3c11488588bcc3c8eae6996c8d9dbe582bdChristian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport CASL.CompositionTable.ToXml

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport CASL.CompositionTable.ComputeTable

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowskiimport CASL.CompositionTable.ModelChecker

b4d51ce3a34a074859f5f34cf430307f5963f912Christian Maederimport CASL.CompositionTable.ParseSparQ

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder

c8a9d35be2207e0d4fbd26a2411e1ba17e3e4c96Christian Maeder#ifdef PROGRAMATICA

c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maederimport Haskell.CreateModules

3986813db69106b9bb1b62faa77532af42512a0cChristian Maeder#endif

3986813db69106b9bb1b62faa77532af42512a0cChristian Maederimport Isabelle.CreateTheories

3986813db69106b9bb1b62faa77532af42512a0cChristian Maederimport Isabelle.IsaParse

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maederimport Isabelle.IsaPrint (printIsaTheory)

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maederimport SoftFOL.CreateDFGDoc

596a8e9039bd2f42c09cc0da4a57c8073f96fbddChristian Maederimport SoftFOL.DFGParser

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport SoftFOL.ParseTPTP

e982190515f83fe6615436530ebe89bb320770d6Christian Maeder

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport FreeCAD.XMLPrinter (exportXMLFC)

f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettichimport FreeCAD.Logic_FreeCAD

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder

9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettichimport VSE.Logic_VSE

1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maederimport VSE.ToSExpr

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

2dcec0e101ddd4169f5323462911e988337c2deeChristian Maeder#ifndef NOOWLLOGIC

0b73fd9cab131c1b25b542007c98b5f8717b1d36Klaus Luettichimport OWL2.Logic_OWL2

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maederimport qualified OWL2.ManchesterPrint as OWL2 (printOWLBasicTheory)

9f08800df9da91d444560875167fbf7acb8396edChristian Maederimport qualified OWL2.ManchesterParser as OWL2 (basicSpec)

333780eae2be9f20fe46dedbf5eb46ffa0cbfd02Christian Maeder#endif

46b1095ba983ce859e17c2a12f48b50583b7150cChristian Maeder

64c2422e1ba0691556a6639e959820add102315cChristian Maeder{-

11280087fb7891a39bae5305886e76c0cc30886cChristian Maeder#ifdef RDFLOGIC

64c2422e1ba0691556a6639e959820add102315cChristian Maederimport RDF.Logic_RDF

64c2422e1ba0691556a6639e959820add102315cChristian Maederimport qualified RDF.Print as RDF (printRDFBasicTheory)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder#endif

865ae561becd3cb451d6280125886b3e03ddf0a4Hendrik Iben-}

865ae561becd3cb451d6280125886b3e03ddf0a4Hendrik Iben

add408dd9d1f792ed3606410f5eede2dd4180614Christian Maederimport CommonLogic.Logic_CommonLogic

add408dd9d1f792ed3606410f5eede2dd4180614Christian Maederimport qualified CommonLogic.AS_CommonLogic as CL_AS (exportCLIF)

63719301448519453f66383f4e583d9fd5b89ecbChristian Maederimport qualified CommonLogic.Parse_CLIF as CL_Parse (cltext)

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

add408dd9d1f792ed3606410f5eede2dd4180614Christian Maederimport Logic.Prover

add408dd9d1f792ed3606410f5eede2dd4180614Christian Maederimport Static.GTheory

add408dd9d1f792ed3606410f5eede2dd4180614Christian Maederimport Static.DevGraph

add408dd9d1f792ed3606410f5eede2dd4180614Christian Maederimport Static.CheckGlobalContext

9658657e918981d91c8647ed8c220464f10a6235Christian Maederimport Static.DotGraph

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport qualified Static.PrintDevGraph as DG

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Proofs.StatusUtils

b53688bfed888214b485cf76439d57262d80e0a7Christian Maederimport Static.ComputeTheory

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maederimport Driver.Options

63719301448519453f66383f4e583d9fd5b89ecbChristian Maederimport Driver.ReadFn (libNameToFile)

f11b87e6fd9aeb5514f97da1ce0149f30f3e3f8aChristian Maederimport Driver.WriteLibDefn

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

f11b87e6fd9aeb5514f97da1ce0149f30f3e3f8aChristian Maederimport OMDoc.XmlInterface (xmlOut)

f0eb47a1c9a5eff66911524130dcf327de641c95Christian Maederimport OMDoc.Export (exportLibEnv)

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder

f11b87e6fd9aeb5514f97da1ce0149f30f3e3f8aChristian MaederwriteVerbFile :: HetcatsOpts -> FilePath -> String -> IO ()

f11b87e6fd9aeb5514f97da1ce0149f30f3e3f8aChristian MaederwriteVerbFile opts f str = do

951bd6674ebe0958d7ac959f3de9be6c49f3fa79Christian Maeder putIfVerbose opts 2 $ "Writing file: " ++ f

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder writeEncFile (ioEncoding opts) f str

f11b87e6fd9aeb5514f97da1ce0149f30f3e3f8aChristian Maeder

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder-- | compute for each LibName in the List a path relative to the given FilePath

9f08800df9da91d444560875167fbf7acb8396edChristian MaederwriteVerbFiles :: HetcatsOpts -- ^ Hets options

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -> String -- ^ A suffix to be combined with the libname

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -> [(LibName, String)] -- ^ An output list

f11b87e6fd9aeb5514f97da1ce0149f30f3e3f8aChristian Maeder -> IO ()

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederwriteVerbFiles opts suffix = mapM_ f

875bba59f1d2ae102148ab089ccd6d00b5efa7e5Christian Maeder where f (ln, s) = writeVerbFile opts (libNameToFile ln ++ suffix) s

28bec3c11488588bcc3c8eae6996c8d9dbe582bdChristian Maeder

b53688bfed888214b485cf76439d57262d80e0a7Christian MaederwriteLibEnv :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> OutType

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -> IO ()

1954518162694c2ef8e0e1263283dd3c75e9ca72Christian MaederwriteLibEnv opts filePrefix lenv ln ot =

3447c1e95850c17a7949e674deb7fbde25f09e5fChristian Maeder let f = filePrefix ++ "." ++ show ot

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder dg = lookupDGraph ln lenv in case ot of

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Prf -> toShATermString (ln, lookupHistory ln lenv)

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder >>= writeVerbFile opts f

28bec3c11488588bcc3c8eae6996c8d9dbe582bdChristian Maeder XmlOut -> writeVerbFile opts f $ ppTopElement

28bec3c11488588bcc3c8eae6996c8d9dbe582bdChristian Maeder $ ToXml.dGraph lenv ln dg

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder OmdocOut -> do

9658657e918981d91c8647ed8c220464f10a6235Christian Maeder let Result ds mOmd = exportLibEnv (recurse opts) (outdir opts) ln lenv

28bec3c11488588bcc3c8eae6996c8d9dbe582bdChristian Maeder showDiags opts ds

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case mOmd of

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder Just omd -> writeVerbFiles opts ".omdoc"

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder $ map (\ (libn, od) -> (libn, xmlOut od)) omd

59ffdc90faada70cc1580ba5963f8f6d7e88cb25Christian Maeder Nothing -> putIfVerbose opts 0 "could not translate to OMDoc"

c64d33a7fbeae730cbe65193fe3cc24e7aa1ddd6Christian Maeder GraphOut (Dot showInternalNodeLabels) -> writeVerbFile opts f

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder $ dotGraph f showInternalNodeLabels "" dg

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> return ()

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian MaederwriteSoftFOL :: HetcatsOpts -> FilePath -> G_theory -> IRI

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder -> SPFType -> Int -> String -> IO ()

62ec122da8d4fdfa66cc059b97dabbf10c81affeChristian MaederwriteSoftFOL opts f gTh i c n msg = do

62ec122da8d4fdfa66cc059b97dabbf10c81affeChristian Maeder let cc = case c of

62ec122da8d4fdfa66cc059b97dabbf10c81affeChristian Maeder ConsistencyCheck -> True

951bd6674ebe0958d7ac959f3de9be6c49f3fa79Christian Maeder ProveTheory -> False

59ffdc90faada70cc1580ba5963f8f6d7e88cb25Christian Maeder mDoc <- printTheoryAsSoftFOL i n cc

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder $ (if cc then theoremsToAxioms else id) gTh

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder maybe (putIfVerbose opts 0 $

edc4d8faa97073b96157868aaa887d6e4dfddf85Christian Maeder "could not translate to " ++ msg ++ " file: " ++ f)

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ( \ d -> do

0e7407d270da049e0b19b3b737996c5577b4970cChristian Maeder let str = shows d "\n"

2afae0880da7ca73c9376fd4d653ab19833fe858Christian Maeder case parse (if n == 0 then forget parseSPASS else forget tptp)

b83ff3749d99d03b641adee264b781039a551addChristian Maeder f str of

d3720ba517d582ba9eeed603fe3bd015ac02ab8eChristian Maeder Left err -> putIfVerbose opts 0 $ show err

951bd6674ebe0958d7ac959f3de9be6c49f3fa79Christian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f

951bd6674ebe0958d7ac959f3de9be6c49f3fa79Christian Maeder writeVerbFile opts f str) mDoc

951bd6674ebe0958d7ac959f3de9be6c49f3fa79Christian Maeder

b83ff3749d99d03b641adee264b781039a551addChristian MaederwriteFreeCADFile :: HetcatsOpts -> FilePath -> G_theory -> IO ()

64c2422e1ba0691556a6639e959820add102315cChristian MaederwriteFreeCADFile opts filePrefix (G_theory lid (ExtSign sign _) _ _ _) = do

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder fcSign <- coercePlainSign lid FreeCAD

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder "Expecting a FreeCAD signature for writing FreeCAD xml" sign

1651d17a9d7530af8763c462c93ac5f2f4d5fcf9Christian Maeder writeVerbFile opts (filePrefix ++ ".xml") $ exportXMLFC fcSign

b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder

b83ff3749d99d03b641adee264b781039a551addChristian MaederwriteIsaFile :: HetcatsOpts -> FilePath -> G_theory -> LibName -> IRI

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -> IO ()

63719301448519453f66383f4e583d9fd5b89ecbChristian MaederwriteIsaFile opts filePrefix raw_gTh ln i = do

c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maeder let Result ds mTh = createIsaTheory raw_gTh

c2257f94016aeb9e5c3ff3d4d675a81f8f873f0dChristian Maeder addThn = (++ '_' : iriToStringShortUnsecure i)

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder fp = addThn filePrefix

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder showDiags opts ds

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder case mTh of

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder Nothing ->

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder putIfVerbose opts 0 $ "could not translate to Isabelle theory: " ++ fp

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Just (sign, sens) -> do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let tn = addThn . reverse . takeWhile (/= '/') . reverse $ case

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder show $ getLibId ln of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder [] -> filePrefix

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder lstr -> lstr

bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder sf = shows (printIsaTheory tn sign sens) "\n"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder f = fp ++ ".thy"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder case parse parseTheory f sf of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Left err -> putIfVerbose opts 0 $ show err

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski _ -> putIfVerbose opts 3 $ "reparsed: " ++ f

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder writeVerbFile opts f sf

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder when (hasPrfOut opts && verbose opts >= 3) $ let

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder (axs, rest) = partition ( \ s -> isAxiom s || isDef s) sens

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder in mapM_ ( \ s -> let

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder tnf = tn ++ "_" ++ senAttr s

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder tf = fp ++ "_" ++ senAttr s ++ ".thy"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in writeVerbFile opts tf $ shows

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder (printIsaTheory tnf sign $ s : axs) "\n") rest

08d506ebb78da1e8656a73a349492e042f4c9f72Christian Maeder

08d506ebb78da1e8656a73a349492e042f4c9f72Christian MaederwriteTheory :: [String] -> String -> HetcatsOpts -> FilePath -> GlobalAnnos

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder -> G_theory -> LibName -> IRI -> OutType -> IO ()

63719301448519453f66383f4e583d9fd5b89ecbChristian MaederwriteTheory ins nam opts filePrefix ga

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder raw_gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) ln i ot =

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let fp = filePrefix ++ "_" ++ iriToStringShortUnsecure i

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder f = fp ++ "." ++ show ot

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder th = (sign0, toNamedList sens0)

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder lang = language_name lid

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in case ot of

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder FreeCADOut -> writeFreeCADFile opts filePrefix raw_gTh

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ThyFile -> writeIsaFile opts filePrefix raw_gTh ln i

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder DfgFile c -> writeSoftFOL opts f raw_gTh i c 0 "DFG"

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder TPTPFile c -> writeSoftFOL opts f raw_gTh i c 1 "TPTP"

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder TheoryFile d -> do

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder if null $ show d then

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder writeVerbFile opts f $ shows (DG.printTh ga i raw_gTh) "\n"

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder else putIfVerbose opts 0 "printing theory delta is not implemented"

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder when (lang == language_name VSE) $ do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder (sign, sens) <- coerceBasicTheory lid VSE "" th

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let (sign', sens') = addUniformRestr sign sens

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder lse = map (namedSenToSExpr sign') sens'

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder unless (null lse) $ writeVerbFile opts (fp ++ ".sexpr")

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $ shows (prettySExpr $ SList lse) "\n"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder SigFile d -> do

63719301448519453f66383f4e583d9fd5b89ecbChristian 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"

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder when (lang == language_name VSE) $ do

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder (sign, sens) <- coerceBasicTheory lid VSE "" th

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder let (sign', _sens') = addUniformRestr sign sens

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder writeVerbFile opts (f ++ ".sexpr")

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder $ shows (prettySExpr $ vseSignToSExpr sign') "\n"

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder SymXml -> writeVerbFile opts f $ ppTopElement

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder $ ToXml.showSymbolsTh ins nam ga raw_gTh

ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder#ifdef PROGRAMATICA

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder HaskellOut -> case printModule raw_gTh of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Nothing ->

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder putIfVerbose opts 0 $ "could not translate to Haskell file: " ++ f

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just d -> writeVerbFile opts f $ shows d "\n"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder#endif

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ComptableXml -> if lang == language_name CASL then do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder th2 <- coerceBasicTheory lid CASL "" th

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder let Result ds res = computeCompTable i th2

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder showDiags opts ds

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder case res of

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Just td -> writeVerbFile opts f $ tableXmlStr td

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Nothing -> return ()

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder else putIfVerbose opts 0 $ "expected CASL theory for: " ++ f

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder#ifndef NOOWLLOGIC

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder OWLOut

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder | lang == language_name OWL2 -> do

b4d51ce3a34a074859f5f34cf430307f5963f912Christian Maeder th2 <- coerceBasicTheory lid OWL2 "" th

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder let owltext = shows (OWL2.printOWLBasicTheory th2) "\n"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder case parse (OWL2.basicSpec >> eof) f owltext of

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Left err -> putIfVerbose opts 0 $ show err

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeVerbFile opts f owltext

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder | otherwise -> putIfVerbose opts 0 $ "expected OWL theory for: " ++ f

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder#endif

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder#ifdef RDFLOGIC

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder{-

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder RDFOut

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder | lang == language_name RDF -> do

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder th2 <- coerceBasicTheory lid RDF "" th

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder let rdftext = shows (RDF.printRDFBasicTheory th2) "\n"

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder writeVerbFile opts f rdftext

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder | otherwise -> putIfVerbose opts 0 $ "expected RDF theory for: " ++ f

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder-}

b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder#endif

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder CLIFOut

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder | lang == language_name CommonLogic -> do

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder (_, th2) <- coerceBasicTheory lid CommonLogic "" th

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let cltext = shows (CL_AS.exportCLIF th2) "\n"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder case parse (many CL_Parse.cltext >> eof) f cltext of

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder Left err -> putIfVerbose opts 0 $ show err

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder _ -> putIfVerbose opts 3 $ "reparsed: " ++ f

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder writeVerbFile opts f cltext

b085709d4b69dc84724000b7b917f348edfa932eChristian Maeder | otherwise -> putIfVerbose opts 0 $ "expected Common Logic theory for: "

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ++ f

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder _ -> return () -- ignore other file types

48a98aa04f4c2c1f5f8f79c007e1ff95e699b31aFlorian Mossakowski

8865728716566f42fa73e7e0bc080ba3225df764Christian MaedermodelSparQCheck :: HetcatsOpts -> G_theory -> IRI -> IO ()

8865728716566f42fa73e7e0bc080ba3225df764Christian MaedermodelSparQCheck opts gTh@(G_theory lid (ExtSign sign0 _) _ sens0 _) i =

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder case coerceBasicTheory lid CASL "" (sign0, toNamedList sens0) of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just th2 -> do

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder table <- parseSparQTableFromFile $ modelSparQ opts

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder case table of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Left _ -> putIfVerbose opts 0

7e828434af28f94f7e27524575844ce3a44df45dChristian Maeder $ "could not parse SparQTable from file: " ++ modelSparQ opts

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Right y -> let Result d _ = modelCheck i th2 y in

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder if length d > 0 then showDiags opts {verbose = 2 } $ take 10 d

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder else putIfVerbose opts 0 "Modelcheck suceeded, no errors found"

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder _ ->

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder putIfVerbose opts 0 $ "could not translate Theory to CASL:\n "

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder ++ showDoc gTh ""

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian MaederwriteTheoryFiles :: HetcatsOpts -> [OutType] -> FilePath -> LibEnv

78e7910c3360f74f1db172d63d20bb07c64e56e3Christian Maeder -> GlobalAnnos -> LibName -> IRI -> Int -> IO ()

63719301448519453f66383f4e583d9fd5b89ecbChristian MaederwriteTheoryFiles opts specOutTypes filePrefix lenv ga ln i n =

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let dg = lookupDGraph ln lenv

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder nam = getDGNodeName $ labDG dg n

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ins = getImportNames dg n

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder in case globalNodeTheory dg n of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Nothing -> putIfVerbose opts 0 $ "could not compute theory of spec "

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder ++ show i

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just raw_gTh0 -> do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let tr = transNames opts

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Result es mTh = if null tr then return (raw_gTh0, "") else do

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder comor <- lookupCompComorphism (map tokStr tr) logicGraph

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder tTh <- mapG_theory comor raw_gTh0

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder return (tTh, show comor)

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder showDiags opts es

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder case mTh of

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Nothing ->

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder putIfVerbose opts 0 "could not translate theory"

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder Just (raw_gTh, tStr) -> do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder unless (null tStr) $

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder putIfVerbose opts 2 $ "Translated using comorphism " ++ tStr

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder putIfVerbose opts 4 $ "Sublogic of " ++ show i ++ ": " ++

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder show (sublogicOfTh raw_gTh)

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder unless (modelSparQ opts == "") $

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder modelSparQCheck opts (theoremsToAxioms raw_gTh) i

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder mapM_ (writeTheory ins nam opts filePrefix ga raw_gTh ln i)

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder specOutTypes

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder

3143271856dbf456bd7acc1c07193173f886d986Christian MaederwriteSpecFiles :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> DGraph

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder -> IO ()

63719301448519453f66383f4e583d9fd5b89ecbChristian MaederwriteSpecFiles opts file lenv ln dg = do

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder let gctx = globalEnv dg

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder ga = globalAnnos dg

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder ns = specNames opts

7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder vs = viewNames opts

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder filePrefix = snd $ getFilePrefix opts file

9f08800df9da91d444560875167fbf7acb8396edChristian Maeder outTypes = outtypes opts

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder specOutTypes = filter ( \ ot -> case ot of

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder ThyFile -> True

4067eba4f5605d9569d78085deb1a27f08ac34e2Christian Maeder DfgFile _ -> True

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder TPTPFile _ -> True

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder XmlOut -> True

efb44558d78b59ea6ce8c16cb5eb1ac0a2604c84Christian Maeder OmdocOut -> True

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder TheoryFile _ -> True

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder SigFile _ -> True

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder OWLOut -> True

7688e20f844fe88f75c04016841ebb5e5e3d927fChristian Maeder CLIFOut -> True

3143271856dbf456bd7acc1c07193173f886d986Christian Maeder FreeCADOut -> True

63719301448519453f66383f4e583d9fd5b89ecbChristian Maeder HaskellOut -> True

ComptableXml -> True

SymXml -> True

_ -> False) outTypes

allSpecs = null ns

noViews = null vs

ignore = null specOutTypes && modelSparQ opts == ""

mapM_ (writeLibEnv opts filePrefix lenv ln) $

if null $ dumpOpts opts then outTypes else EnvOut : outTypes

mapM_ ( \ i -> case Map.lookup i gctx of

Just (SpecEntry (ExtGenSig _ (NodeSig n _))) ->

writeTheoryFiles opts specOutTypes filePrefix lenv ga ln i n

_ -> unless allSpecs

$ putIfVerbose opts 0 $ "Unknown spec name: " ++ show i

) $ if ignore then [] else

if allSpecs then Map.keys gctx else map simpleIdToIRI ns

unless noViews $

mapM_ ( \ si -> let i = simpleIdToIRI si in case Map.lookup i gctx of

Just (ViewOrStructEntry _ (ExtViewSig _ (GMorphism cid _ _ m _) _)) ->

writeVerbFile opts (filePrefix ++ "_" ++ show i ++ ".view")

$ shows (pretty $ Map.toList $ symmap_of (targetLogic cid) m) "\n"

_ -> putIfVerbose opts 0 $ "Unknown view name: " ++ show i

) vs

mapM_ ( \ n ->

writeTheoryFiles opts specOutTypes filePrefix lenv ga ln

(simpleIdToIRI $ genToken $ 'n' : show n) n)

$ if ignore || not allSpecs then [] else

nodesDG dg

\\ Map.fold ( \ e l -> case e of

SpecEntry (ExtGenSig _ (NodeSig n _)) -> n : l

_ -> l) [] gctx

doDump opts "GlobalAnnos" $ putStrLn $ showGlobalDoc ga ga ""

doDump opts "PrintStat" $ putStrLn $ printStatistics dg

doDump opts "DGraph" $ putStrLn $ showDoc dg ""

doDump opts "DuplicateDefEdges" $ let es = duplicateDefEdges dg in

unless (null es) $ print es

doDump opts "LogicGraph" $ putStrLn $ showDoc logicGraph ""

doDump opts "LibEnv" $

writeVerbFile opts (filePrefix ++ ".lenv") $

shows (DG.prettyLibEnv lenv) "\n"