content: {- |
  Module      :  ./Isabelle/Isa2DG.hs
  Description :  Import data generated by hol2hets into a DG
  Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  jonathan.von_schroeder@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  -}
  
  module Isabelle.Isa2DG where
  
  import Static.GTheory
  import Static.DevGraph
  
  import Static.DgUtils
  import Static.History
  import Static.ComputeTheory
  import Static.AnalysisStructured (insLink)
  
  import Logic.Prover
  import Logic.ExtSign
  import Logic.Grothendieck
  import Logic.Logic (ide)
  
  import Common.LibName
  import Common.Id
  import Common.AS_Annotation
  import Common.IRI (simpleIdToIRI)
  
  import Isabelle.Logic_Isabelle
  import Isabelle.IsaSign
  import Isabelle.IsaImport (importIsaDataIO, IsaData)
  
  import Driver.Options
  
  import qualified Data.Map as Map
  import Data.Graph.Inductive.Graph (Node)
  import Data.List (intercalate)
  import Data.Maybe (catMaybes)
  
  import Control.Monad (unless, when)
  import qualified Control.Monad.Fail as Fail
  import Control.Concurrent (forkIO, killThread)
  
  import Common.Utils
  import System.Exit
  import System.Directory
  import System.FilePath
  
  _insNodeDG :: Sign -> [Named Sentence] -> String
                -> DGraph -> (DGraph, Node)
  _insNodeDG sig sens n dg =
   let gt = G_theory Isabelle Nothing (makeExtSign Isabelle sig) startSigId
             (toThSens sens) startThId
       labelK = newInfoNodeLab
        (makeName (simpleIdToIRI (mkSimpleId n)))
        (newNodeInfo DGEmpty)
        gt
       k = getNewNodeDG dg
       insN = [InsertNode (k, labelK)]
       newDG = changesDGH dg insN
       labCh = [SetNodeLab labelK (k, labelK
        { globalTheory = computeLabelTheory Map.empty (emptyLibName "Imported Theory") newDG
          (k, labelK) })]
       newDG1 = changesDGH newDG labCh in (newDG1, k)
  
  analyzeMessages :: Int -> [String] -> IO ()
  analyzeMessages _ [] = return ()
  analyzeMessages i (x : xs) = do
   case x of
    'v' : i' : ':' : msg -> when (read [i'] < i) $ putStr $ msg ++ "\n"
    _ -> putStr $ x ++ "\n"
   analyzeMessages i xs
  
  anaThyFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
  anaThyFile opts path = do
   fp <- canonicalizePath path
   tempFile <- getTempFile "" (takeBaseName fp)
   fifo <- getTempFifo (takeBaseName fp)
   exportScript' <- fmap (</> "export.sh") $ getEnvDef
    "HETS_ISA_TOOLS" "./Isabelle/export"
   exportScript <- canonicalizePath exportScript'
   e1 <- doesFileExist exportScript
   unless e1 $ Fail.fail
    "Export script not available! Maybe you need to specify HETS_ISA_TOOLS"
   (l, close) <- readFifo fifo
   tid <- forkIO $ analyzeMessages (verbose opts) (lines . concat $ l)
   (ex, sout, err) <- executeProcess exportScript [fp, tempFile, fifo] ""
   close
   killThread tid
   removeFile fifo
   case ex of
    ExitFailure _ -> do
     removeFile tempFile
     soutF <- getTempFile sout (takeBaseName fp ++ ".sout")
     errF <- getTempFile err (takeBaseName fp ++ ".serr")
     Fail.fail $ "Export Failed! - Export script died prematurely. See " ++ soutF
            ++ " and " ++ errF ++ " for details."
    ExitSuccess -> do
     ret <- anaIsaFile opts tempFile
     removeFile tempFile
     return ret
  
  mkNode :: (DGraph, Map.Map String (Node, Sign)) -> IsaData ->
       (DGraph, Map.Map String (Node, Sign))
  mkNode (dg, m) (name, header', imps, keywords', uses', body) =
   let sens = map (\ sen ->
               let name' = case sen of
                    Locale n' _ _ _ -> "locale " ++ qname n'
                    Class n' _ _ _ -> "class " ++ qname n'
                    Datatypes dts -> "datatype " ++ intercalate "_"
                                       (map (qname . datatypeName) dts)
                    Consts cs -> "consts " ++ intercalate "_"
                                               (map (\ (n', _, _) -> n') cs)
                    TypeSynonym n' _ _ _ -> "type_synonym " ++ qname n'
                    Axioms axs -> "axioms " ++ intercalate "_"
                                   (map (qname . axiomName) axs)
                    Lemma _ _ _ l -> "lemma " ++ (intercalate "_" . map qname
                                        . catMaybes $ map propsName l)
                    Definition n' _ _ _ _ _ -> "definition " ++ show n'
                    Fun _ _ _ _ _ fsigs -> "fun " ++ intercalate "_"
                                              (map (\ (n', _, _, _) -> n') fsigs)
                    _ -> ""
               in makeNamed name' sen) body
       sgns = Map.foldrWithKey (\ k a l ->
               if elem k imps then snd a : l else l) [] m
       sgn = foldl union_sig (emptySign { imports = imps,
                                           header = header',
                                           keywords = keywords',
                                           uses = uses' }) sgns
       (dg', n) = _insNodeDG sgn sens name dg
       m' = Map.insert name (n, sgn) m
       dgRet = foldr (\ imp dg'' ->
                           case Map.lookup imp m of
                            Just (n', s') ->
                             let gsig = G_sign Isabelle (makeExtSign Isabelle s')
                                         startSigId
                                 incl = gEmbed2 gsig $ mkG_morphism Isabelle
                                         (ide sgn)
                             in insLink dg'' incl globalDef DGLinkImports n' n
                            Nothing -> dg'') dg' imps
   in (dgRet, m')
  
  anaIsaFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
  anaIsaFile _ path = do
   theories <- importIsaDataIO path
   let name = "Imported Theory"
       (dg, _) = foldl mkNode (emptyDG, Map.empty) theories
       le = Map.insert (emptyLibName name) dg Map.empty
   return $ Just (emptyLibName name,
    computeLibEnvTheories le)
  