{-# LANGUAGE CPP #-}
{- |
Module      :  ./Driver/WriteFn.hs
Description :  Writing various formats, according to Hets options
Copyright   :  (c) Klaus Luettich, C.Maeder, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable(DevGraph)

Writing various formats, according to Hets options
-}

module Driver.WriteFn
  ( writeSpecFiles
  , writeVerbFile
  , writeLG
  ) where

import Text.ParserCombinators.Parsec
import Text.XML.Light

import System.FilePath

import Control.Monad

import Data.List (partition, (\\), intercalate)
import Data.Maybe

import Common.AS_Annotation
import Common.Id
import Common.IRI (IRI, simpleIdToIRI, iriToStringShortUnsecure, setAngles)
import Common.Json (ppJson)
import Common.DocUtils
import Common.ExtSign
import Common.LibName
import Common.Result
import Common.Parsec (forget)
import Common.Percent
import Common.GlobalAnnotations (GlobalAnnos)
import qualified Data.Map as Map
import Common.SExpr
import Common.IO
import Common.Utils

import Comorphisms.LogicGraph

import Logic.Coerce
import Logic.Comorphism (targetLogic)
import Logic.Grothendieck
import Logic.LGToXml
import Logic.LGToJson
import Logic.Logic
import Logic.Prover

import Proofs.StatusUtils

import Static.GTheory
import Static.DevGraph
import Static.CheckGlobalContext
import Static.DotGraph
import qualified Static.PrintDevGraph as DG
import Static.ComputeTheory
import qualified Static.ToXml as ToXml
import qualified Static.ToJson as ToJson
import qualified Persistence.DevGraph
import qualified Persistence.LogicGraph

import CASL.Logic_CASL
import CASL.CompositionTable.Pretty2
import CASL.CompositionTable.ToXml
import CASL.CompositionTable.ComputeTable
import CASL.CompositionTable.ModelChecker
import CASL.CompositionTable.ParseTable2

import OWL2.Medusa
import OWL2.MedusaToJson
import OWL2.XMLConversion (xmlOntologyDoc)
import OWL2.Sign (emptySign)

#ifdef PROGRAMATICA
import Haskell.CreateModules
#endif

import Isabelle.CreateTheories
import Isabelle.IsaParse
import Isabelle.IsaPrint (printIsaTheory)

import SoftFOL.CreateDFGDoc
import SoftFOL.DFGParser
import SoftFOL.ParseTPTP

import TPTP.Logic_TPTP
import qualified TPTP.Pretty as TPTPPretty

import FreeCAD.XMLPrinter (exportXMLFC)
import FreeCAD.Logic_FreeCAD

import VSE.Logic_VSE
import VSE.ToSExpr

#ifndef NOOWLLOGIC
import OWL2.CreateOWL
import OWL2.Logic_OWL2
import OWL2.ParseOWL (convertOWL)
import qualified OWL2.ManchesterPrint as OWL2 (prepareBasicTheory, convertBasicTheory)
#endif

#ifdef RDFLOGIC
import RDF.Logic_RDF
import qualified RDF.Print as RDF (printRDFBasicTheory)
#endif

import CommonLogic.Logic_CommonLogic
import qualified CommonLogic.AS_CommonLogic as CL_AS (exportCLIF)
import qualified CommonLogic.Parse_CLIF as CL_Parse (cltext)
import qualified CommonLogic.Print_KIF as Print_KIF (exportKIF)

import Driver.Options
import Driver.ReadFn (libNameToFile)
import Driver.WriteLibDefn

import OMDoc.XmlInterface (xmlOut)
import OMDoc.Export (exportLibEnv)

writeVerbFile :: HetcatsOpts -> FilePath -> String -> IO ()
writeVerbFile :: HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile opts :: HetcatsOpts
opts fullFileName :: FilePath
fullFileName str :: FilePath
str = do
    let f :: FilePath
f = FilePath -> FilePath -> FilePath
tryToStripPrefix "file://" FilePath
fullFileName
    HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Writing file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f
    Enc -> FilePath -> FilePath -> IO ()
writeEncFile (HetcatsOpts -> Enc
ioEncoding HetcatsOpts
opts) FilePath
f FilePath
str

-- | compute for each LibName in the List a path relative to the given FilePath
writeVerbFiles :: HetcatsOpts -- ^ Hets options
               -> String -- ^ A suffix to be combined with the libname
               -> [(LibName, String)] -- ^ An output list
               -> IO ()
writeVerbFiles :: HetcatsOpts -> FilePath -> [(LibName, FilePath)] -> IO ()
writeVerbFiles opts :: HetcatsOpts
opts suffix :: FilePath
suffix = ((LibName, FilePath) -> IO ()) -> [(LibName, FilePath)] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (LibName, FilePath) -> IO ()
f
        where f :: (LibName, FilePath) -> IO ()
f (ln :: LibName
ln, s :: FilePath
s) = HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts (LibName -> FilePath
libNameToFile LibName
ln FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
suffix) FilePath
s

writeLibEnv :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> OutType
            -> IO ()
writeLibEnv :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> OutType -> IO ()
writeLibEnv opts :: HetcatsOpts
opts filePrefix :: FilePath
filePrefix lenv :: LibEnv
lenv ln :: LibName
ln ot :: OutType
ot =
    let f :: FilePath
f = FilePath
filePrefix FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ OutType -> FilePath
forall a. Show a => a -> FilePath
show OutType
ot
        dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
lenv in case OutType
ot of
      Prf -> (LibName, ProofHistory) -> IO FilePath
forall a. ShATermLG a => a -> IO FilePath
toShATermString (LibName
ln, LibName -> LibEnv -> ProofHistory
lookupHistory LibName
ln LibEnv
lenv)
             IO FilePath -> (FilePath -> IO ()) -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f
      XmlOut -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Element -> FilePath
ppTopElement
          (Element -> FilePath) -> Element -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> LibEnv -> LibName -> DGraph -> Element
ToXml.dGraph HetcatsOpts
opts LibEnv
lenv LibName
ln DGraph
dg
      DbOut -> HetcatsOpts -> LibEnv -> IO ()
Persistence.DevGraph.exportLibEnv HetcatsOpts
opts LibEnv
lenv
      JsonOut -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Json -> FilePath
ppJson
          (Json -> FilePath) -> Json -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> LibEnv -> LibName -> DGraph -> Json
ToJson.dGraph HetcatsOpts
opts LibEnv
lenv LibName
ln DGraph
dg
      SymsXml -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Element -> FilePath
ppTopElement
          (Element -> FilePath) -> Element -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> DGraph -> Element
ToXml.dgSymbols HetcatsOpts
opts DGraph
dg
      OmdocOut -> do
          let Result ds :: [Diagnosis]
ds mOmd :: Maybe [(LibName, OMDoc)]
mOmd = Bool -> FilePath -> LibName -> LibEnv -> Result [(LibName, OMDoc)]
exportLibEnv (HetcatsOpts -> Bool
recurse HetcatsOpts
opts) (HetcatsOpts -> FilePath
outdir HetcatsOpts
opts) LibName
ln LibEnv
lenv
          HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
          case Maybe [(LibName, OMDoc)]
mOmd of
               Just omd :: [(LibName, OMDoc)]
omd -> HetcatsOpts -> FilePath -> [(LibName, FilePath)] -> IO ()
writeVerbFiles HetcatsOpts
opts ".omdoc"
                           ([(LibName, FilePath)] -> IO ()) -> [(LibName, FilePath)] -> IO ()
forall a b. (a -> b) -> a -> b
$ ((LibName, OMDoc) -> (LibName, FilePath))
-> [(LibName, OMDoc)] -> [(LibName, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (libn :: LibName
libn, od :: OMDoc
od) -> (LibName
libn, OMDoc -> FilePath
forall a. XmlRepresentable a => a -> FilePath
xmlOut OMDoc
od)) [(LibName, OMDoc)]
omd
               Nothing -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 "could not translate to OMDoc"
      GraphOut (Dot showInternalNodeLabels :: Bool
showInternalNodeLabels) -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f
        (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Bool -> FilePath -> DGraph -> FilePath
dotGraph FilePath
f Bool
showInternalNodeLabels "" DGraph
dg
      _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

writeSoftFOL :: HetcatsOpts -> FilePath -> G_theory -> IRI
             -> SPFType -> Int -> String -> IO ()
writeSoftFOL :: HetcatsOpts
-> FilePath
-> G_theory
-> IRI
-> SPFType
-> Int
-> FilePath
-> IO ()
writeSoftFOL opts :: HetcatsOpts
opts f :: FilePath
f gTh :: G_theory
gTh i :: IRI
i c :: SPFType
c n :: Int
n msg :: FilePath
msg = do
      let cc :: Bool
cc = case SPFType
c of
                 ConsistencyCheck -> Bool
True
                 ProveTheory -> Bool
False
      Maybe Doc
mDoc <- IRI -> Int -> Bool -> G_theory -> IO (Maybe Doc)
printTheoryAsSoftFOL IRI
i Int
n Bool
cc
              (G_theory -> IO (Maybe Doc)) -> G_theory -> IO (Maybe Doc)
forall a b. (a -> b) -> a -> b
$ (if Bool
cc then G_theory -> G_theory
theoremsToAxioms else G_theory -> G_theory
forall a. a -> a
id) G_theory
gTh
      IO () -> (Doc -> IO ()) -> Maybe Doc -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$
             "could not translate to " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
msg FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f)
          ( \ d :: Doc
d -> do
              let str :: FilePath
str = Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows Doc
d "\n"
              case Parsec FilePath () ()
-> FilePath -> FilePath -> Either ParseError ()
forall s t a.
Stream s Identity t =>
Parsec s () a -> FilePath -> s -> Either ParseError a
parse (if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then ParsecT FilePath () Identity SPProblem -> Parsec FilePath () ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ParsecT FilePath () Identity SPProblem
parseSPASS else ParsecT FilePath () Identity [TPTP] -> Parsec FilePath () ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget ParsecT FilePath () Identity [TPTP]
tptp)
                   FilePath
f FilePath
str of
                Left err :: ParseError
err -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err
                _ -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 3 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "reparsed: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f
              HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
str) Maybe Doc
mDoc

writeFreeCADFile :: HetcatsOpts -> FilePath -> G_theory -> IO ()
writeFreeCADFile :: HetcatsOpts -> FilePath -> G_theory -> IO ()
writeFreeCADFile opts :: HetcatsOpts
opts filePrefix :: FilePath
filePrefix (G_theory lid :: lid
lid _ (ExtSign sign :: sign
sign _) _ _ _) = do
  Sign
fcSign <- lid -> FreeCAD -> FilePath -> sign -> IO Sign
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1 -> lid2 -> FilePath -> sign1 -> m sign2
coercePlainSign lid
lid FreeCAD
FreeCAD
            "Expecting a FreeCAD signature for writing FreeCAD xml" sign
sign
  HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts (FilePath
filePrefix FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".xml") (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Sign -> FilePath
exportXMLFC Sign
fcSign

writeIsaFile :: HetcatsOpts -> FilePath -> G_theory -> LibName -> IRI
             -> IO ()
writeIsaFile :: HetcatsOpts -> FilePath -> G_theory -> LibName -> IRI -> IO ()
writeIsaFile opts :: HetcatsOpts
opts filePrefix :: FilePath
filePrefix raw_gTh :: G_theory
raw_gTh ln :: LibName
ln i :: IRI
i = do
  let Result ds :: [Diagnosis]
ds mTh :: Maybe (Sign, [Named Sentence])
mTh = G_theory -> Result (Sign, [Named Sentence])
createIsaTheory G_theory
raw_gTh
      addThn :: FilePath -> FilePath
addThn = (FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ '_' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: IRI -> FilePath
iriToStringShortUnsecure IRI
i)
      fp :: FilePath
fp = FilePath -> FilePath
addThn FilePath
filePrefix
  HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
  case Maybe (Sign, [Named Sentence])
mTh of
    Nothing ->
      HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "could not translate to Isabelle theory: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
fp
    Just (sign :: Sign
sign, sens :: [Named Sentence]
sens) -> do
      let tn :: FilePath
tn = FilePath -> FilePath
addThn (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '/') (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath
forall a. [a] -> [a]
reverse (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ case
               LibName -> FilePath
libToFileName LibName
ln of
                   [] -> FilePath
filePrefix
                   lstr :: FilePath
lstr -> FilePath
lstr
          sf :: FilePath
sf = Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows (FilePath -> Sign -> [Named Sentence] -> Doc
printIsaTheory FilePath
tn Sign
sign [Named Sentence]
sens) "\n"
          f :: FilePath
f = FilePath
fp FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".thy"
      case Parsec FilePath () (TheoryHead, Body)
-> FilePath -> FilePath -> Either ParseError (TheoryHead, Body)
forall s t a.
Stream s Identity t =>
Parsec s () a -> FilePath -> s -> Either ParseError a
parse Parsec FilePath () (TheoryHead, Body)
parseTheory FilePath
f FilePath
sf of
        Left err :: ParseError
err -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err
        _ -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 3 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "reparsed: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f
      HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
sf
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HetcatsOpts -> Bool
hasPrfOut HetcatsOpts
opts Bool -> Bool -> Bool
&& HetcatsOpts -> Int
verbose HetcatsOpts
opts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 3) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ let
        (axs :: [Named Sentence]
axs, rest :: [Named Sentence]
rest) = (Named Sentence -> Bool)
-> [Named Sentence] -> ([Named Sentence], [Named Sentence])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ( \ s :: Named Sentence
s -> Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isAxiom Named Sentence
s Bool -> Bool -> Bool
|| Named Sentence -> Bool
forall s a. SenAttr s a -> Bool
isDef Named Sentence
s) [Named Sentence]
sens
         in (Named Sentence -> IO ()) -> [Named Sentence] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ s :: Named Sentence
s -> let
           tnf :: FilePath
tnf = FilePath
tn FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Named Sentence -> FilePath
forall s a. SenAttr s a -> a
senAttr Named Sentence
s
           tf :: FilePath
tf = FilePath
fp FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Named Sentence -> FilePath
forall s a. SenAttr s a -> a
senAttr Named Sentence
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".thy"
           in HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
tf (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows
                   (FilePath -> Sign -> [Named Sentence] -> Doc
printIsaTheory FilePath
tnf Sign
sign ([Named Sentence] -> Doc) -> [Named Sentence] -> Doc
forall a b. (a -> b) -> a -> b
$ Named Sentence
s Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: [Named Sentence]
axs) "\n") [Named Sentence]
rest

wrongLogicMsg :: String -> String -> String -> String            
wrongLogicMsg :: FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg file :: FilePath
file expected :: FilePath
expected found :: FilePath
found =
  "expected " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
expected FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " theory for: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " but found " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
found

writeTheory :: [String] -> String -> HetcatsOpts -> FilePath -> GlobalAnnos
  -> G_theory -> LibName -> IRI -> OutType -> IO ()
writeTheory :: [FilePath]
-> FilePath
-> HetcatsOpts
-> FilePath
-> GlobalAnnos
-> G_theory
-> LibName
-> IRI
-> OutType
-> IO ()
writeTheory ins :: [FilePath]
ins nam :: FilePath
nam opts :: HetcatsOpts
opts filePrefix :: FilePath
filePrefix ga :: GlobalAnnos
ga
  raw_gTh :: G_theory
raw_gTh@(G_theory lid :: lid
lid _ (ExtSign sign0 :: sign
sign0 _) _ sens0 :: ThSens sentence (AnyComorphism, BasicProof)
sens0 _) ln :: LibName
ln i :: IRI
i ot :: OutType
ot =
    let fp :: FilePath
fp = FilePath
filePrefix FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
i'
        i' :: FilePath
i' = FilePath -> FilePath
encode (IRI -> FilePath
iriToStringShortUnsecure (IRI -> FilePath) -> IRI -> FilePath
forall a b. (a -> b) -> a -> b
$ Bool -> IRI -> IRI
setAngles Bool
False IRI
i)
        f :: FilePath
f = FilePath
fp FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "." FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ OutType -> FilePath
forall a. Show a => a -> FilePath
show OutType
ot
        th :: (sign, [Named sentence])
th = (sign
sign0, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens0)
        lang :: FilePath
lang = lid -> FilePath
forall lid. Language lid => lid -> FilePath
language_name lid
lid
    in case OutType
ot of
    FreeCADOut -> HetcatsOpts -> FilePath -> G_theory -> IO ()
writeFreeCADFile HetcatsOpts
opts FilePath
filePrefix G_theory
raw_gTh
    ThyFile -> HetcatsOpts -> FilePath -> G_theory -> LibName -> IRI -> IO ()
writeIsaFile HetcatsOpts
opts FilePath
filePrefix G_theory
raw_gTh LibName
ln IRI
i
    DfgFile c :: SPFType
c -> HetcatsOpts
-> FilePath
-> G_theory
-> IRI
-> SPFType
-> Int
-> FilePath
-> IO ()
writeSoftFOL HetcatsOpts
opts FilePath
f G_theory
raw_gTh IRI
i SPFType
c 0 "DFG"
    TPTPFile
        | FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== TPTP -> FilePath
forall lid. Language lid => lid -> FilePath
language_name TPTP
TPTP -> do
            (Sign, [Named Sentence])
th2 <- lid
-> TPTP
-> FilePath
-> (sign, [Named sentence])
-> IO (Sign, [Named Sentence])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid TPTP
TPTP "" (sign, [Named sentence])
th
            let tptpText :: FilePath
tptpText = Doc -> FilePath
forall a. Show a => a -> FilePath
show ((Sign, [Named Sentence]) -> Doc
TPTPPretty.printBasicTheory (Sign, [Named Sentence])
th2)
            HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
tptpText
        | Bool
otherwise -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "TPTP" FilePath
lang
    TheoryFile d :: Delta
d -> do
      if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (FilePath -> Bool) -> FilePath -> Bool
forall a b. (a -> b) -> a -> b
$ Delta -> FilePath
forall a. Show a => a -> FilePath
show Delta
d then
        HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows (GlobalAnnos -> IRI -> G_theory -> Doc
DG.printTh GlobalAnnos
ga IRI
i G_theory
raw_gTh) "\n"
        else HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 "printing theory delta is not implemented"
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== VSE -> FilePath
forall lid. Language lid => lid -> FilePath
language_name VSE
VSE) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        (sign :: VSESign
sign, sens :: [Named Sentence]
sens) <- lid
-> VSE
-> FilePath
-> (sign, [Named sentence])
-> IO (VSESign, [Named Sentence])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid VSE
VSE "" (sign, [Named sentence])
th
        let (sign' :: VSESign
sign', sens' :: [Named Sentence]
sens') = VSESign -> [Named Sentence] -> (VSESign, [Named Sentence])
forall f.
Sign f Procs
-> [Named Sentence] -> (Sign f Procs, [Named Sentence])
addUniformRestr VSESign
sign [Named Sentence]
sens
            lse :: [SExpr]
lse = (Named Sentence -> SExpr) -> [Named Sentence] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map (VSESign -> Named Sentence -> SExpr
forall f. Sign f Procs -> Named Sentence -> SExpr
namedSenToSExpr VSESign
sign') [Named Sentence]
sens'
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([SExpr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SExpr]
lse) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts (FilePath
fp FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".sexpr")
            (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows (SExpr -> Doc
prettySExpr (SExpr -> Doc) -> SExpr -> Doc
forall a b. (a -> b) -> a -> b
$ [SExpr] -> SExpr
SList [SExpr]
lse) "\n"
    SigFile d :: Delta
d -> do
      if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (FilePath -> Bool) -> FilePath -> Bool
forall a b. (a -> b) -> a -> b
$ Delta -> FilePath
forall a. Show a => a -> FilePath
show Delta
d then
        HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows (G_sign -> Doc
forall a. Pretty a => a -> Doc
pretty (G_sign -> Doc) -> G_sign -> Doc
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
raw_gTh) "\n"
        else HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 "printing signature delta is not implemented"
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== VSE -> FilePath
forall lid. Language lid => lid -> FilePath
language_name VSE
VSE) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        (sign :: VSESign
sign, sens :: [Named Sentence]
sens) <- lid
-> VSE
-> FilePath
-> (sign, [Named sentence])
-> IO (VSESign, [Named Sentence])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid VSE
VSE "" (sign, [Named sentence])
th
        let (sign' :: VSESign
sign', _sens' :: [Named Sentence]
_sens') = VSESign -> [Named Sentence] -> (VSESign, [Named Sentence])
forall f.
Sign f Procs
-> [Named Sentence] -> (Sign f Procs, [Named Sentence])
addUniformRestr VSESign
sign [Named Sentence]
sens
        HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts (FilePath
f FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".sexpr")
          (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows (SExpr -> Doc
prettySExpr (SExpr -> Doc) -> SExpr -> Doc
forall a b. (a -> b) -> a -> b
$ VSESign -> SExpr
forall f. Sign f Procs -> SExpr
vseSignToSExpr VSESign
sign') "\n"
    SymXml -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Element -> FilePath
ppTopElement
           (Element -> FilePath) -> Element -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts
-> [FilePath] -> FilePath -> GlobalAnnos -> G_theory -> Element
ToXml.showSymbolsTh HetcatsOpts
opts [FilePath]
ins FilePath
nam GlobalAnnos
ga G_theory
raw_gTh
#ifdef PROGRAMATICA
    HaskellOut -> case printModule raw_gTh of
        Nothing ->
            putIfVerbose opts 0 $ "could not translate to Haskell file: " ++ f
        Just d -> writeVerbFile opts f $ shows d "\n"
#endif
    ComptableXml -> if FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== CASL -> FilePath
forall lid. Language lid => lid -> FilePath
language_name CASL
CASL then do
          (CASLSign, [Named CASLFORMULA])
th2 <- lid
-> CASL
-> FilePath
-> (sign, [Named sentence])
-> IO (CASLSign, [Named CASLFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CASL
CASL "" (sign, [Named sentence])
th
          let Result ds :: [Diagnosis]
ds res :: Maybe Table
res = IRI -> (CASLSign, [Named CASLFORMULA]) -> Result Table
forall f e. IRI -> (Sign f e, [Named (FORMULA f)]) -> Result Table
computeCompTable IRI
i (CASLSign, [Named CASLFORMULA])
th2
          HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
          case Maybe Table
res of
            Just td :: Table
td -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Table -> FilePath
tableXmlStr Table
td
            Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "CASL" FilePath
lang
    MedusaJson -> if FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== OWL2 -> FilePath
forall lid. Language lid => lid -> FilePath
language_name OWL2
OWL2 then do
          (Sign, [Named Axiom])
th2 <- lid
-> OWL2
-> FilePath
-> (sign, [Named sentence])
-> IO (Sign, [Named Axiom])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid OWL2
OWL2 "" (sign, [Named sentence])
th
          let Result ds :: [Diagnosis]
ds res :: Maybe Medusa
res = IRI -> (Sign, [Named Axiom]) -> Result Medusa
medusa IRI
i (Sign, [Named Axiom])
th2
          HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
          case Maybe Medusa
res of
            Just td :: Medusa
td -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Medusa -> FilePath
medusaToJsonString Medusa
td
            Nothing -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        else HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "OWL2" FilePath
lang
#ifdef RDFLOGIC
    RDFOut
        | FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== RDF -> FilePath
forall lid. Language lid => lid -> FilePath
language_name RDF
RDF -> do
            (Sign, [Named Axiom])
th2 <- lid
-> RDF
-> FilePath
-> (sign, [Named sentence])
-> IO (Sign, [Named Axiom])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid RDF
RDF "" (sign, [Named sentence])
th
            let rdftext :: FilePath
rdftext = Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows ((Sign, [Named Axiom]) -> Doc
RDF.printRDFBasicTheory (Sign, [Named Axiom])
th2) "\n"
            HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
rdftext
        | Bool
otherwise -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "RDF" FilePath
lang
#endif
#ifndef NOOWLLOGIC
    OWLOut ty :: OWLFormat
ty -> case OWLFormat
ty of
      Manchester -> HetcatsOpts
-> OWLFormat -> FilePath -> G_theory -> FilePath -> IO ()
writeOWL2VerbFile HetcatsOpts
opts OWLFormat
ty FilePath
f G_theory
raw_gTh "Manchester"

      --  TODO: implement OWL2 RDF parser/printer
      -- RdfXml -> trace "-- RdfXml" $ case createOWLTheory raw_gTh of

      Functional -> HetcatsOpts
-> OWLFormat -> FilePath -> G_theory -> FilePath -> IO ()
writeOWL2VerbFile HetcatsOpts
opts OWLFormat
ty FilePath
f G_theory
raw_gTh "Functional"

      OwlXml -> case G_theory -> Result (Sign, [Named Axiom])
createOWLTheory G_theory
raw_gTh of
        Result _ Nothing ->
          HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "OWL" (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ OWLFormat -> FilePath
forall a. Show a => a -> FilePath
show OWLFormat
ty
        Result ds :: [Diagnosis]
ds (Just th2 :: (Sign, [Named Axiom])
th2) -> do
            let owltext :: FilePath
owltext =
                  Element -> FilePath
ppTopElement (Element -> FilePath) -> Element -> FilePath
forall a b. (a -> b) -> a -> b
$ Sign -> OntologyDocument -> Element
xmlOntologyDoc Sign
emptySign (OntologyDocument -> Element) -> OntologyDocument -> Element
forall a b. (a -> b) -> a -> b
$ (Sign, [Named Axiom]) -> OntologyDocument
OWL2.convertBasicTheory (Sign, [Named Axiom])
th2
            HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
            HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
owltext

      _ -> let flp :: FilePath
flp = LibName -> FilePath
getFilePath LibName
ln in case FilePath -> InType -> InType
guess FilePath
flp InType
GuessIn of
        OWLIn _ -> HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f (FilePath -> IO ()) -> IO FilePath -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> FilePath -> IO FilePath
convertOWL FilePath
flp (OWLFormat -> FilePath
forall a. Show a => a -> FilePath
show OWLFormat
ty)
        _ -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0
          (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "OWL output only supported for owl input types ("
          FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((OWLFormat -> FilePath) -> [OWLFormat] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map OWLFormat -> FilePath
forall a. Show a => a -> FilePath
show [OWLFormat]
plainOwlFormats) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")"
#endif
    CLIFOut
      | FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== CommonLogic -> FilePath
forall lid. Language lid => lid -> FilePath
language_name CommonLogic
CommonLogic -> do
            (_, th2 :: [Named TEXT_META]
th2) <- lid
-> CommonLogic
-> FilePath
-> (sign, [Named sentence])
-> IO (Sign, [Named TEXT_META])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CommonLogic
CommonLogic "" (sign, [Named sentence])
th
            let cltext :: FilePath
cltext = Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows ([Named TEXT_META] -> Doc
CL_AS.exportCLIF [Named TEXT_META]
th2) "\n"
            case Parsec FilePath () ()
-> FilePath -> FilePath -> Either ParseError ()
forall s t a.
Stream s Identity t =>
Parsec s () a -> FilePath -> s -> Either ParseError a
parse (ParsecT FilePath () Identity TEXT_META
-> ParsecT FilePath () Identity [TEXT_META]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (PrefixMap -> ParsecT FilePath () Identity TEXT_META
forall st. PrefixMap -> CharParser st TEXT_META
CL_Parse.cltext PrefixMap
forall k a. Map k a
Map.empty) ParsecT FilePath () Identity [TEXT_META]
-> Parsec FilePath () () -> Parsec FilePath () ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parsec FilePath () ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof) FilePath
f FilePath
cltext of
              Left err :: ParseError
err -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err
              _ -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 3 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "reparsed: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
f
            HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
cltext
      | Bool
otherwise -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "Common Logic" FilePath
lang
    KIFOut
      | FilePath
lang FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== CommonLogic -> FilePath
forall lid. Language lid => lid -> FilePath
language_name CommonLogic
CommonLogic -> do
            (_, th2 :: [Named TEXT_META]
th2) <- lid
-> CommonLogic
-> FilePath
-> (sign, [Named sentence])
-> IO (Sign, [Named TEXT_META])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CommonLogic
CommonLogic "" (sign, [Named sentence])
th
            let kiftext :: FilePath
kiftext = Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows ([Named TEXT_META] -> Doc
Print_KIF.exportKIF [Named TEXT_META]
th2) "\n"
            HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
kiftext
      | Bool
otherwise -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "Common Logic" FilePath
lang
    _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- ignore other file types

allowedOWL2Syntaxes :: [String]
allowedOWL2Syntaxes :: [FilePath]
allowedOWL2Syntaxes = ["Functional", "Manchester"]

writeOWL2VerbFile :: HetcatsOpts -> OWLFormat -> FilePath -> G_theory -> String -> IO ()
writeOWL2VerbFile :: HetcatsOpts
-> OWLFormat -> FilePath -> G_theory -> FilePath -> IO ()
writeOWL2VerbFile opts :: HetcatsOpts
opts ty :: OWLFormat
ty f :: FilePath
f raw_gTh :: G_theory
raw_gTh syntax :: FilePath
syntax = case G_theory -> Result (Sign, [Named Axiom])
createOWLTheory G_theory
raw_gTh of
  Result _ Nothing ->
    HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
wrongLogicMsg FilePath
f "OWL" (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ OWLFormat -> FilePath
forall a. Show a => a -> FilePath
show OWLFormat
ty
  Result ds :: [Diagnosis]
ds (Just th2 :: (Sign, [Named Axiom])
th2) -> if FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FilePath
syntax [FilePath]
allowedOWL2Syntaxes
    then do 
      let sy :: FilePath
sy = FilePath
syntax
          ms :: Maybe IRI
ms = IRI -> Maybe IRI
forall a. a -> Maybe a
Just (IRI -> Maybe IRI) -> IRI -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> SIMPLE_ID
mkSimpleId FilePath
sy
          owltext :: FilePath
owltext = Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows
            (Maybe IRI -> OWL2 -> (Sign, [Named Axiom]) -> Doc
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
printTheory Maybe IRI
ms OWL2
OWL2 ((Sign, [Named Axiom]) -> Doc) -> (Sign, [Named Axiom]) -> Doc
forall a b. (a -> b) -> a -> b
$ (Sign, [Named Axiom]) -> (Sign, [Named Axiom])
OWL2.prepareBasicTheory (Sign, [Named Axiom])
th2) "\n"
      HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts [Diagnosis]
ds
      HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts FilePath
f FilePath
owltext
    else HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Syntax '" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
syntax FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "' is not allowed for OWL2."

modelSparQCheck :: HetcatsOpts -> G_theory -> IO ()
modelSparQCheck :: HetcatsOpts -> G_theory -> IO ()
modelSparQCheck opts :: HetcatsOpts
opts gTh :: G_theory
gTh@(G_theory lid :: lid
lid _ (ExtSign sign0 :: sign
sign0 _) _ sens0 :: ThSens sentence (AnyComorphism, BasicProof)
sens0 _) =
    case lid
-> CASL
-> FilePath
-> (sign, [Named sentence])
-> Maybe (CASLSign, [Named CASLFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> FilePath
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CASL
CASL "" (sign
sign0, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens0) of
    Just th2 :: (CASLSign, [Named CASLFORMULA])
th2 -> do
      Either ParseError Table2
table <- FilePath -> IO (Either ParseError Table2)
parseSparQTableFromFile (FilePath -> IO (Either ParseError Table2))
-> FilePath -> IO (Either ParseError Table2)
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath
modelSparQ HetcatsOpts
opts
      case Either ParseError Table2
table of
        Left err :: ParseError
err -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0
          (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "could not parse SparQTable from file: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ HetcatsOpts -> FilePath
modelSparQ HetcatsOpts
opts
          FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ParseError -> FilePath
forall a. Show a => a -> FilePath
show ParseError
err
        Right y :: Table2
y -> do
            HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 4 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines
               ["lisp file content:", Doc -> FilePath
forall a. Show a => a -> FilePath
show (Doc -> FilePath) -> Doc -> FilePath
forall a b. (a -> b) -> a -> b
$ Table2 -> Doc
table2Doc Table2
y, "lisp file end."]
            let Result d :: [Diagnosis]
d _ = Int -> (CASLSign, [Named CASLFORMULA]) -> Table2 -> Result ()
modelCheck (HetcatsOpts -> Int
counterSparQ HetcatsOpts
opts) (CASLSign, [Named CASLFORMULA])
th2 Table2
y
            if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
d then
                HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 "Modelcheck succeeded, no errors found"
             else HetcatsOpts -> [Diagnosis] -> IO ()
showDiags
               (if HetcatsOpts -> Int
verbose HetcatsOpts
opts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 2 then HetcatsOpts
opts else HetcatsOpts
opts {verbose :: Int
verbose = 2}) [Diagnosis]
d
    _ ->
      HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "could not translate Theory to CASL:\n "
         FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ G_theory -> FilePath -> FilePath
forall a. Pretty a => a -> FilePath -> FilePath
showDoc G_theory
gTh ""

writeTheoryFiles :: HetcatsOpts -> [OutType] -> FilePath -> LibEnv
                 -> GlobalAnnos -> LibName -> IRI -> Int -> IO ()
writeTheoryFiles :: HetcatsOpts
-> [OutType]
-> FilePath
-> LibEnv
-> GlobalAnnos
-> LibName
-> IRI
-> Int
-> IO ()
writeTheoryFiles opts :: HetcatsOpts
opts specOutTypes :: [OutType]
specOutTypes filePrefix :: FilePath
filePrefix lenv :: LibEnv
lenv ga :: GlobalAnnos
ga ln :: LibName
ln i :: IRI
i n :: Int
n =
  let dg :: DGraph
dg = LibName -> LibEnv -> DGraph
lookupDGraph LibName
ln LibEnv
lenv
      nam :: FilePath
nam = DGNodeLab -> FilePath
getDGNodeName (DGNodeLab -> FilePath) -> DGNodeLab -> FilePath
forall a b. (a -> b) -> a -> b
$ DGraph -> Int -> DGNodeLab
labDG DGraph
dg Int
n
      ins :: [FilePath]
ins = DGraph -> Int -> [FilePath]
getImportNames DGraph
dg Int
n
  in case DGraph -> Int -> Maybe G_theory
globalNodeTheory DGraph
dg Int
n of
      Nothing -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "could not compute theory of spec "
                 FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
i
      Just raw_gTh0 :: G_theory
raw_gTh0 -> do
            let tr :: [SIMPLE_ID]
tr = HetcatsOpts -> [SIMPLE_ID]
transNames HetcatsOpts
opts
                Result es :: [Diagnosis]
es mTh :: Maybe (G_theory, FilePath)
mTh = if [SIMPLE_ID] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SIMPLE_ID]
tr then (G_theory, FilePath) -> Result (G_theory, FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory
raw_gTh0, "") else do
                   AnyComorphism
comor <- [FilePath] -> LogicGraph -> Result AnyComorphism
forall (m :: * -> *).
MonadFail m =>
[FilePath] -> LogicGraph -> m AnyComorphism
lookupCompComorphism ((SIMPLE_ID -> FilePath) -> [SIMPLE_ID] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> FilePath
tokStr [SIMPLE_ID]
tr) LogicGraph
logicGraph
                   G_theory
tTh <- Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory (HetcatsOpts -> Bool
lossyTrans HetcatsOpts
opts) AnyComorphism
comor G_theory
raw_gTh0
                   (G_theory, FilePath) -> Result (G_theory, FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory
tTh, "Translated using comorphism " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ AnyComorphism -> FilePath
forall a. Show a => a -> FilePath
show AnyComorphism
comor)
                (raw_gTh :: G_theory
raw_gTh, tStr :: FilePath
tStr) =
                  (G_theory, FilePath)
-> Maybe (G_theory, FilePath) -> (G_theory, FilePath)
forall a. a -> Maybe a -> a
fromMaybe (G_theory
raw_gTh0, "Keeping untranslated theory") Maybe (G_theory, FilePath)
mTh
            HetcatsOpts -> [Diagnosis] -> IO ()
showDiags HetcatsOpts
opts ([Diagnosis] -> IO ()) -> [Diagnosis] -> IO ()
forall a b. (a -> b) -> a -> b
$ (Diagnosis -> Diagnosis) -> [Diagnosis] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ((DiagKind -> DiagKind) -> Diagnosis -> Diagnosis
updDiagKind
                (\ k :: DiagKind
k -> if DiagKind
k DiagKind -> DiagKind -> Bool
forall a. Eq a => a -> a -> Bool
== DiagKind
Error then DiagKind
Warning else DiagKind
k)) [Diagnosis]
es
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
tStr) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 2 FilePath
tStr
            HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 4 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Sublogic of " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
i FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ": " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                   G_sublogics -> FilePath
forall a. Show a => a -> FilePath
show (G_theory -> G_sublogics
sublogicOfTh G_theory
raw_gTh)
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (HetcatsOpts -> FilePath
modelSparQ HetcatsOpts
opts FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "") (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                   HetcatsOpts -> G_theory -> IO ()
modelSparQCheck HetcatsOpts
opts (G_theory -> G_theory
theoremsToAxioms G_theory
raw_gTh)
            (OutType -> IO ()) -> [OutType] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([FilePath]
-> FilePath
-> HetcatsOpts
-> FilePath
-> GlobalAnnos
-> G_theory
-> LibName
-> IRI
-> OutType
-> IO ()
writeTheory [FilePath]
ins FilePath
nam HetcatsOpts
opts FilePath
filePrefix GlobalAnnos
ga G_theory
raw_gTh LibName
ln IRI
i)
                 [OutType]
specOutTypes

writeSpecFiles :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> DGraph
               -> IO ()
writeSpecFiles :: HetcatsOpts -> FilePath -> LibEnv -> LibName -> DGraph -> IO ()
writeSpecFiles opts :: HetcatsOpts
opts file :: FilePath
file lenv :: LibEnv
lenv ln :: LibName
ln dg :: DGraph
dg = do
    let gctx :: GlobalEnv
gctx = DGraph -> GlobalEnv
globalEnv DGraph
dg
        gns :: [IRI]
gns = GlobalEnv -> [IRI]
forall k a. Map k a -> [k]
Map.keys GlobalEnv
gctx
        mns :: [SIMPLE_ID] -> [IRI]
mns = (SIMPLE_ID -> IRI) -> [SIMPLE_ID] -> [IRI]
forall a b. (a -> b) -> [a] -> [b]
map ((SIMPLE_ID -> IRI) -> [SIMPLE_ID] -> [IRI])
-> (SIMPLE_ID -> IRI) -> [SIMPLE_ID] -> [IRI]
forall a b. (a -> b) -> a -> b
$ \ t :: SIMPLE_ID
t -> IRI -> FilePath -> PrefixMap -> IRI
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (SIMPLE_ID -> IRI
simpleIdToIRI SIMPLE_ID
t) (SIMPLE_ID -> FilePath
tokStr SIMPLE_ID
t)
          (PrefixMap -> IRI) -> PrefixMap -> IRI
forall a b. (a -> b) -> a -> b
$ [(FilePath, IRI)] -> PrefixMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(FilePath, IRI)] -> PrefixMap) -> [(FilePath, IRI)] -> PrefixMap
forall a b. (a -> b) -> a -> b
$ (IRI -> (FilePath, IRI)) -> [IRI] -> [(FilePath, IRI)]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: IRI
i -> (IRI -> FilePath
iriToStringShortUnsecure IRI
i, IRI
i)) [IRI]
gns
        ga :: GlobalAnnos
ga = DGraph -> GlobalAnnos
globalAnnos DGraph
dg
        ns :: [IRI]
ns = [SIMPLE_ID] -> [IRI]
mns ([SIMPLE_ID] -> [IRI]) -> [SIMPLE_ID] -> [IRI]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [SIMPLE_ID]
specNames HetcatsOpts
opts
        vs :: [IRI]
vs = [SIMPLE_ID] -> [IRI]
mns ([SIMPLE_ID] -> [IRI]) -> [SIMPLE_ID] -> [IRI]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [SIMPLE_ID]
viewNames HetcatsOpts
opts
        filePrefix :: FilePath
filePrefix = (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> b
snd ((FilePath, FilePath) -> FilePath)
-> (FilePath, FilePath) -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath -> (FilePath, FilePath)
getFilePrefix HetcatsOpts
opts FilePath
file
        outTypes :: [OutType]
outTypes = HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts
        specOutTypes :: [OutType]
specOutTypes = (OutType -> Bool) -> [OutType] -> [OutType]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ ot :: OutType
ot -> case OutType
ot of
            ThyFile -> Bool
True
            DfgFile _ -> Bool
True
            TPTPFile -> Bool
True
            XmlOut -> Bool
True
            JsonOut -> Bool
True
            OmdocOut -> Bool
True
            TheoryFile _ -> Bool
True
            SigFile _ -> Bool
True
            OWLOut _ -> Bool
True
            CLIFOut -> Bool
True
            KIFOut -> Bool
True
            FreeCADOut -> Bool
True
            HaskellOut -> Bool
True
            ComptableXml -> Bool
True
            MedusaJson -> Bool
True
            SymXml -> Bool
True
            _ -> Bool
False) [OutType]
outTypes
        allSpecs :: Bool
allSpecs = [IRI] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IRI]
ns
        noViews :: Bool
noViews = [IRI] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IRI]
vs
        ignore :: Bool
ignore = [OutType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OutType]
specOutTypes Bool -> Bool -> Bool
&& HetcatsOpts -> FilePath
modelSparQ HetcatsOpts
opts FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== ""
    (OutType -> IO ()) -> [OutType] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (HetcatsOpts -> FilePath -> LibEnv -> LibName -> OutType -> IO ()
writeLibEnv HetcatsOpts
opts FilePath
filePrefix LibEnv
lenv LibName
ln) ([OutType] -> IO ()) -> [OutType] -> IO ()
forall a b. (a -> b) -> a -> b
$
          if [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([FilePath] -> Bool) -> [FilePath] -> Bool
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [FilePath]
dumpOpts HetcatsOpts
opts then [OutType]
outTypes else OutType
EnvOut OutType -> [OutType] -> [OutType]
forall a. a -> [a] -> [a]
: [OutType]
outTypes
    (IRI -> IO ()) -> [IRI] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ i :: IRI
i -> case IRI -> GlobalEnv -> Maybe GlobalEntry
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
i GlobalEnv
gctx of
        Just (SpecEntry (ExtGenSig _ (NodeSig n :: Int
n _))) ->
            HetcatsOpts
-> [OutType]
-> FilePath
-> LibEnv
-> GlobalAnnos
-> LibName
-> IRI
-> Int
-> IO ()
writeTheoryFiles HetcatsOpts
opts [OutType]
specOutTypes FilePath
filePrefix LibEnv
lenv GlobalAnnos
ga LibName
ln IRI
i Int
n
        _ -> Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allSpecs
               (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Unknown spec name: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
i
      ) ([IRI] -> IO ()) -> [IRI] -> IO ()
forall a b. (a -> b) -> a -> b
$ if Bool
ignore then [] else
        if Bool
allSpecs then [IRI]
gns else [IRI]
ns
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
noViews (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
      (IRI -> IO ()) -> [IRI] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ i :: IRI
i -> case IRI -> GlobalEnv -> Maybe GlobalEntry
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup IRI
i GlobalEnv
gctx of
        Just (ViewOrStructEntry _ (ExtViewSig _ (GMorphism cid :: cid
cid _ _ m :: morphism2
m _) _)) ->
            HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts (FilePath
filePrefix FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "_" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
i FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".view")
              (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows ([(symbol2, symbol2)] -> Doc
forall a. Pretty a => a -> Doc
pretty ([(symbol2, symbol2)] -> Doc) -> [(symbol2, symbol2)] -> Doc
forall a b. (a -> b) -> a -> b
$ Map symbol2 symbol2 -> [(symbol2, symbol2)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map symbol2 symbol2 -> [(symbol2, symbol2)])
-> Map symbol2 symbol2 -> [(symbol2, symbol2)]
forall a b. (a -> b) -> a -> b
$ lid2 -> morphism2 -> Map symbol2 symbol2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid -> lid2
targetLogic cid
cid) morphism2
m) "\n"
        _ -> HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose HetcatsOpts
opts 0 (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Unknown view name: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ IRI -> FilePath
forall a. Show a => a -> FilePath
show IRI
i
      ) [IRI]
vs
    (Int -> IO ()) -> [Int] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ( \ n :: Int
n ->
      HetcatsOpts
-> [OutType]
-> FilePath
-> LibEnv
-> GlobalAnnos
-> LibName
-> IRI
-> Int
-> IO ()
writeTheoryFiles HetcatsOpts
opts [OutType]
specOutTypes FilePath
filePrefix LibEnv
lenv GlobalAnnos
ga LibName
ln
         (SIMPLE_ID -> IRI
simpleIdToIRI (SIMPLE_ID -> IRI) -> SIMPLE_ID -> IRI
forall a b. (a -> b) -> a -> b
$ FilePath -> SIMPLE_ID
genToken (FilePath -> SIMPLE_ID) -> FilePath -> SIMPLE_ID
forall a b. (a -> b) -> a -> b
$ 'n' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n) Int
n)
      ([Int] -> IO ()) -> [Int] -> IO ()
forall a b. (a -> b) -> a -> b
$ if Bool
ignore Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
allSpecs then [] else
      DGraph -> [Int]
nodesDG DGraph
dg
      [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ (GlobalEntry -> [Int] -> [Int]) -> [Int] -> GlobalEnv -> [Int]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr ( \ e :: GlobalEntry
e l :: [Int]
l -> case GlobalEntry
e of
            SpecEntry (ExtGenSig _ (NodeSig n :: Int
n _)) -> Int
n Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
l
            _ -> [Int]
l) [] GlobalEnv
gctx
    HetcatsOpts -> FilePath -> IO () -> IO ()
doDump HetcatsOpts
opts "GlobalAnnos" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ GlobalAnnos -> GlobalAnnos -> FilePath -> FilePath
forall a. Pretty a => GlobalAnnos -> a -> FilePath -> FilePath
showGlobalDoc GlobalAnnos
ga GlobalAnnos
ga ""
    HetcatsOpts -> FilePath -> IO () -> IO ()
doDump HetcatsOpts
opts "PrintStat" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ DGraph -> FilePath
printStatistics DGraph
dg
    HetcatsOpts -> FilePath -> IO () -> IO ()
doDump HetcatsOpts
opts "DGraph" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ DGraph -> FilePath -> FilePath
forall a. Pretty a => a -> FilePath -> FilePath
showDoc DGraph
dg ""
    HetcatsOpts -> FilePath -> IO () -> IO ()
doDump HetcatsOpts
opts "DuplicateDefEdges" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ let es :: [Edge]
es = DGraph -> [Edge]
duplicateDefEdges DGraph
dg in
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Edge] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Edge]
es) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [Edge] -> IO ()
forall a. Show a => a -> IO ()
print [Edge]
es
    HetcatsOpts -> FilePath -> IO () -> IO ()
doDump HetcatsOpts
opts "LibEnv" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts (FilePath
filePrefix FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ".lenv")
      (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Doc -> FilePath -> FilePath
forall a. Show a => a -> FilePath -> FilePath
shows (LibEnv -> Doc
DG.prettyLibEnv LibEnv
lenv) "\n"

writeLG :: HetcatsOpts -> IO ()
writeLG :: HetcatsOpts -> IO ()
writeLG opts :: HetcatsOpts
opts = do
    HetcatsOpts -> FilePath -> IO () -> IO ()
doDump HetcatsOpts
opts "LogicGraph" (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ LogicGraph -> FilePath -> FilePath
forall a. Pretty a => a -> FilePath -> FilePath
showDoc LogicGraph
logicGraph ""
    let writeLGXML :: IO ()
writeLGXML = do
          Element
lG <- LogicGraph -> IO Element
lGToXml LogicGraph
logicGraph
          HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts { verbose :: Int
verbose = 2 } (HetcatsOpts -> FilePath
outdir HetcatsOpts
opts FilePath -> FilePath -> FilePath
</> "LogicGraph.xml")
            (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Element -> FilePath
ppTopElement Element
lG
    if [OutType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([OutType] -> Bool) -> [OutType] -> Bool
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts
    then IO ()
writeLGXML
    else
      (OutType -> IO ()) -> [OutType] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ outtype :: OutType
outtype -> case OutType
outtype of
              XmlOut -> IO ()
writeLGXML
              JsonOut -> do
                Json
lG <- LogicGraph -> IO Json
lGToJson LogicGraph
logicGraph
                HetcatsOpts -> FilePath -> FilePath -> IO ()
writeVerbFile HetcatsOpts
opts { verbose :: Int
verbose = 2 } (HetcatsOpts -> FilePath
outdir HetcatsOpts
opts FilePath -> FilePath -> FilePath
</> "LogicGraph.json")
                  (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Json -> FilePath
ppJson Json
lG
              DbOut -> HetcatsOpts -> IO ()
Persistence.LogicGraph.exportLogicGraph HetcatsOpts
opts
              _ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            ) ([OutType] -> IO ()) -> [OutType] -> IO ()
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts