{- |
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 :: Sign -> [Named Sentence] -> String -> DGraph -> (DGraph, Node)
_insNodeDG sig :: Sign
sig sens :: [Named Sentence]
sens n :: String
n dg :: DGraph
dg =
 let gt :: G_theory
gt = Isabelle
-> Maybe IRI
-> ExtSign Sign ()
-> SigId
-> ThSens Sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory Isabelle
Isabelle Maybe IRI
forall a. Maybe a
Nothing (Isabelle -> Sign -> ExtSign Sign ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Isabelle
Isabelle Sign
sig) SigId
startSigId
           ([Named Sentence] -> ThSens Sentence (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
sens) ThId
startThId
     labelK :: DGNodeLab
labelK = NodeName -> DGNodeInfo -> G_theory -> DGNodeLab
newInfoNodeLab
      (IRI -> NodeName
makeName (SIMPLE_ID -> IRI
simpleIdToIRI (String -> SIMPLE_ID
mkSimpleId String
n)))
      (DGOrigin -> DGNodeInfo
newNodeInfo DGOrigin
DGEmpty)
      G_theory
gt
     k :: Node
k = DGraph -> Node
getNewNodeDG DGraph
dg
     insN :: [DGChange]
insN = [LNode DGNodeLab -> DGChange
InsertNode (Node
k, DGNodeLab
labelK)]
     newDG :: DGraph
newDG = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
dg [DGChange]
insN
     labCh :: [DGChange]
labCh = [DGNodeLab -> LNode DGNodeLab -> DGChange
SetNodeLab DGNodeLab
labelK (Node
k, DGNodeLab
labelK
      { globalTheory :: Maybe G_theory
globalTheory = LibEnv -> LibName -> DGraph -> LNode DGNodeLab -> Maybe G_theory
computeLabelTheory LibEnv
forall k a. Map k a
Map.empty (String -> LibName
emptyLibName "Imported Theory") DGraph
newDG
        (Node
k, DGNodeLab
labelK) })]
     newDG1 :: DGraph
newDG1 = DGraph -> [DGChange] -> DGraph
changesDGH DGraph
newDG [DGChange]
labCh in (DGraph
newDG1, Node
k)

analyzeMessages :: Int -> [String] -> IO ()
analyzeMessages :: Node -> [String] -> IO ()
analyzeMessages _ [] = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
analyzeMessages i :: Node
i (x :: String
x : xs :: [String]
xs) = do
 case String
x of
  'v' : i' :: Char
i' : ':' : msg :: String
msg -> Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String -> Node
forall a. Read a => String -> a
read [Char
i'] Node -> Node -> Bool
forall a. Ord a => a -> a -> Bool
< Node
i) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
  _ -> String -> IO ()
putStr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
 Node -> [String] -> IO ()
analyzeMessages Node
i [String]
xs

anaThyFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaThyFile :: HetcatsOpts -> String -> IO (Maybe (LibName, LibEnv))
anaThyFile opts :: HetcatsOpts
opts path :: String
path = do
 String
fp <- String -> IO String
canonicalizePath String
path
 String
tempFile <- String -> String -> IO String
getTempFile "" (String -> String
takeBaseName String
fp)
 String
fifo <- String -> IO String
getTempFifo (String -> String
takeBaseName String
fp)
 String
exportScript' <- (String -> String) -> IO String -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> String -> String
</> "export.sh") (IO String -> IO String) -> IO String -> IO String
forall a b. (a -> b) -> a -> b
$ String -> String -> IO String
getEnvDef
  "HETS_ISA_TOOLS" "./Isabelle/export"
 String
exportScript <- String -> IO String
canonicalizePath String
exportScript'
 Bool
e1 <- String -> IO Bool
doesFileExist String
exportScript
 Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
e1 (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail
  "Export script not available! Maybe you need to specify HETS_ISA_TOOLS"
 (l :: [String]
l, close :: IO ()
close) <- String -> IO ([String], IO ())
readFifo String
fifo
 ThreadId
tid <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ Node -> [String] -> IO ()
analyzeMessages (HetcatsOpts -> Node
verbose HetcatsOpts
opts) (String -> [String]
lines (String -> [String])
-> ([String] -> String) -> [String] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [String]
l)
 (ex :: ExitCode
ex, sout :: String
sout, err :: String
err) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
exportScript [String
fp, String
tempFile, String
fifo] ""
 IO ()
close
 ThreadId -> IO ()
killThread ThreadId
tid
 String -> IO ()
removeFile String
fifo
 case ExitCode
ex of
  ExitFailure _ -> do
   String -> IO ()
removeFile String
tempFile
   String
soutF <- String -> String -> IO String
getTempFile String
sout (String -> String
takeBaseName String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".sout")
   String
errF <- String -> String -> IO String
getTempFile String
err (String -> String
takeBaseName String
fp String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".serr")
   String -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> IO (Maybe (LibName, LibEnv)))
-> String -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ "Export Failed! - Export script died prematurely. See " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
soutF
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errF String -> String -> String
forall a. [a] -> [a] -> [a]
++ " for details."
  ExitSuccess -> do
   Maybe (LibName, LibEnv)
ret <- HetcatsOpts -> String -> IO (Maybe (LibName, LibEnv))
anaIsaFile HetcatsOpts
opts String
tempFile
   String -> IO ()
removeFile String
tempFile
   Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (LibName, LibEnv)
ret

mkNode :: (DGraph, Map.Map String (Node, Sign)) -> IsaData ->
     (DGraph, Map.Map String (Node, Sign))
mkNode :: (DGraph, Map String (Node, Sign))
-> IsaData -> (DGraph, Map String (Node, Sign))
mkNode (dg :: DGraph
dg, m :: Map String (Node, Sign)
m) (name :: String
name, header' :: Maybe String
header', imps :: [String]
imps, keywords' :: [String]
keywords', uses' :: [String]
uses', body :: [Sentence]
body) =
 let sens :: [Named Sentence]
sens = (Sentence -> Named Sentence) -> [Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ sen :: Sentence
sen ->
             let name' :: String
name' = case Sentence
sen of
                  Locale n' _ _ _ -> "locale " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
qname QName
n'
                  Class n' _ _ _ -> "class " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
qname QName
n'
                  Datatypes dts -> "datatype " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "_"
                                     ((Datatype -> String) -> [Datatype] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> String
qname (QName -> String) -> (Datatype -> QName) -> Datatype -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Datatype -> QName
datatypeName) [Datatype]
dts)
                  Consts cs -> "consts " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "_"
                                             (((String, Maybe Mixfix, Typ) -> String)
-> [(String, Maybe Mixfix, Typ)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n' :: String
n', _, _) -> String
n') [(String, Maybe Mixfix, Typ)]
cs)
                  TypeSynonym n' _ _ _ -> "type_synonym " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
qname QName
n'
                  Axioms axs -> "axioms " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "_"
                                 ((Axiom -> String) -> [Axiom] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (QName -> String
qname (QName -> String) -> (Axiom -> QName) -> Axiom -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Axiom -> QName
axiomName) [Axiom]
axs)
                  Lemma _ _ _ l -> "lemma " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "_" ([String] -> String)
-> ([Maybe QName] -> [String]) -> [Maybe QName] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (QName -> String) -> [QName] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map QName -> String
qname
                                      ([QName] -> [String])
-> ([Maybe QName] -> [QName]) -> [Maybe QName] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe QName] -> [QName]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe QName] -> String) -> [Maybe QName] -> String
forall a b. (a -> b) -> a -> b
$ (Props -> Maybe QName) -> [Props] -> [Maybe QName]
forall a b. (a -> b) -> [a] -> [b]
map Props -> Maybe QName
propsName [Props]
l)
                  Definition n' _ _ _ _ _ -> "definition " String -> String -> String
forall a. [a] -> [a] -> [a]
++ QName -> String
forall a. Show a => a -> String
show QName
n'
                  Fun _ _ _ _ _ fsigs -> "fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "_"
                                            (((String, Maybe Mixfix, Typ, [([Term], Term)]) -> String)
-> [(String, Maybe Mixfix, Typ, [([Term], Term)])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n' :: String
n', _, _, _) -> String
n') [(String, Maybe Mixfix, Typ, [([Term], Term)])]
fsigs)
                  _ -> ""
             in String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed String
name' Sentence
sen) [Sentence]
body
     sgns :: [Sign]
sgns = (String -> (Node, Sign) -> [Sign] -> [Sign])
-> [Sign] -> Map String (Node, Sign) -> [Sign]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (\ k :: String
k a :: (Node, Sign)
a l :: [Sign]
l ->
             if String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
k [String]
imps then (Node, Sign) -> Sign
forall a b. (a, b) -> b
snd (Node, Sign)
a Sign -> [Sign] -> [Sign]
forall a. a -> [a] -> [a]
: [Sign]
l else [Sign]
l) [] Map String (Node, Sign)
m
     sgn :: Sign
sgn = (Sign -> Sign -> Sign) -> Sign -> [Sign] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Sign -> Sign -> Sign
union_sig (Sign
emptySign { imports :: [String]
imports = [String]
imps,
                                         header :: Maybe String
header = Maybe String
header',
                                         keywords :: [String]
keywords = [String]
keywords',
                                         uses :: [String]
uses = [String]
uses' }) [Sign]
sgns
     (dg' :: DGraph
dg', n :: Node
n) = Sign -> [Named Sentence] -> String -> DGraph -> (DGraph, Node)
_insNodeDG Sign
sgn [Named Sentence]
sens String
name DGraph
dg
     m' :: Map String (Node, Sign)
m' = String
-> (Node, Sign)
-> Map String (Node, Sign)
-> Map String (Node, Sign)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
name (Node
n, Sign
sgn) Map String (Node, Sign)
m
     dgRet :: DGraph
dgRet = (String -> DGraph -> DGraph) -> DGraph -> [String] -> DGraph
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ imp :: String
imp dg'' :: DGraph
dg'' ->
                         case String -> Map String (Node, Sign) -> Maybe (Node, Sign)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
imp Map String (Node, Sign)
m of
                          Just (n' :: Node
n', s' :: Sign
s') ->
                           let gsig :: G_sign
gsig = Isabelle -> ExtSign Sign () -> SigId -> G_sign
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> ExtSign sign symbol -> SigId -> G_sign
G_sign Isabelle
Isabelle (Isabelle -> Sign -> ExtSign Sign ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign Isabelle
Isabelle Sign
s')
                                       SigId
startSigId
                               incl :: GMorphism
incl = G_sign -> G_morphism -> GMorphism
gEmbed2 G_sign
gsig (G_morphism -> GMorphism) -> G_morphism -> GMorphism
forall a b. (a -> b) -> a -> b
$ Isabelle -> IsabelleMorphism -> G_morphism
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> morphism -> G_morphism
mkG_morphism Isabelle
Isabelle
                                       (Sign -> IsabelleMorphism
forall object morphism.
Category object morphism =>
object -> morphism
ide Sign
sgn)
                           in DGraph
-> GMorphism
-> DGLinkType
-> DGLinkOrigin
-> Node
-> Node
-> DGraph
insLink DGraph
dg'' GMorphism
incl DGLinkType
globalDef DGLinkOrigin
DGLinkImports Node
n' Node
n
                          Nothing -> DGraph
dg'') DGraph
dg' [String]
imps
 in (DGraph
dgRet, Map String (Node, Sign)
m')

anaIsaFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaIsaFile :: HetcatsOpts -> String -> IO (Maybe (LibName, LibEnv))
anaIsaFile _ path :: String
path = do
 [IsaData]
theories <- String -> IO [IsaData]
importIsaDataIO String
path
 let name :: String
name = "Imported Theory"
     (dg :: DGraph
dg, _) = ((DGraph, Map String (Node, Sign))
 -> IsaData -> (DGraph, Map String (Node, Sign)))
-> (DGraph, Map String (Node, Sign))
-> [IsaData]
-> (DGraph, Map String (Node, Sign))
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (DGraph, Map String (Node, Sign))
-> IsaData -> (DGraph, Map String (Node, Sign))
mkNode (DGraph
emptyDG, Map String (Node, Sign)
forall k a. Map k a
Map.empty) [IsaData]
theories
     le :: LibEnv
le = LibName -> DGraph -> LibEnv -> LibEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (String -> LibName
emptyLibName String
name) DGraph
dg LibEnv
forall k a. Map k a
Map.empty
 Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv)))
-> Maybe (LibName, LibEnv) -> IO (Maybe (LibName, LibEnv))
forall a b. (a -> b) -> a -> b
$ (LibName, LibEnv) -> Maybe (LibName, LibEnv)
forall a. a -> Maybe a
Just (String -> LibName
emptyLibName String
name,
  LibEnv -> LibEnv
computeLibEnvTheories LibEnv
le)