{- |
Module : ./HolLight/HolLight2DG.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 HolLight.HolLight2DG where
import Static.GTheory
import Static.DevGraph
import Static.DgUtils
import Static.History
import Static.ComputeTheory
import Logic.Logic
import Logic.Prover
import Logic.ExtSign
import Logic.Grothendieck
import Common.LibName
import Common.Id
import Common.IRI (simpleIdToIRI)
import Common.AS_Annotation
import Common.Result
import Common.Utils
import Common.SAX
import Control.Monad
import Common.Lib.Maybe
import qualified Data.ByteString.Lazy as L
import Text.XML.Expat.SAX
import HolLight.Sign
import HolLight.Sentence
import HolLight.Term
import HolLight.Logic_HolLight
import HolLight.Helper (names)
import Driver.Options
import Data.Graph.Inductive.Graph
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import System.Exit
import System.Directory
import System.FilePath
readTuple :: (Show a, Show b) => MSaxState a -> MSaxState b -> MSaxState (a, b)
readTuple f1 f2 = do
expectTag True "tuple"
t1 <- readWithTag f1 "fst"
t2 <- readWithTag f2 "snd"
expectTag False "tuple"
return (t1, t2)
readWord :: MSaxState String
readWord = liftM reverse $ foldCatchLeft (\ s ->
do
s' <- do
dropSpaces
d <- getD
case d of
[] -> error "HolLight.readWord"
h : xs -> case h of
CharacterData s' -> do
putD xs
return s'
_ -> debugS $ "Expected character data but instead got: " ++ show h
return $ trimLeft (reverse $ trimLeft s') ++ s) []
readStr :: MSaxState String
readStr = readWithTag readWord "s"
readInt :: MSaxState Int
readInt = do
w <- readWord
return $ fromMaybe (error "HolLight.readInt") $ readMaybe w
readInt' :: MSaxState Int
readInt' = readWithTag readInt "i"
readMappedInt :: Map.Map Int a -> MSaxState a
readMappedInt m = do
i <- readInt
case Map.lookup i m of
Just a -> return a
_ -> debugS $ "readMappedInt: Integer " ++ show i ++ " not mapped"
listToTypes :: Map.Map Int HolType -> [Int] -> Maybe [HolType]
listToTypes m l = case l of
x : xs -> case Map.lookup x m of
Just t -> case listToTypes m xs of
Just ts -> Just (t : ts)
_ -> Nothing
_ -> Nothing
[] -> Just []
-> MSaxState (Map.Map Int HolType)
readSharedHolType sl m = do
d <- getM
(b, t) <- tag
case (b, t) of
(True, "TyApp") -> do
(i, l) <- readTuple readInt (whileM readInt')
case (Map.lookup i sl, listToTypes m l) of
(Just s, Just l') -> do
expectTag False "TyApp"
return $ Map.insert (Map.size m + 1) (TyApp s $ reverse l') m
(r1, r2) -> debugS $ "readSharedHolType: Couldn't build TyApp"
++ " because the result of the lookup for "
++ show (i, l) ++ " was " ++ show (r1, r2)
(True, "TyVar") -> do
i <- readInt
case Map.lookup i sl of
Just s -> do
expectTag False "TyVar"
return $ Map.insert (Map.size m + 1) (TyVar s) m
_ -> debugS $ "readSharedHolType: Couldn't build TyVar"
++ " because looking up " ++ show i
++ " failed"
_ -> do
putM d
debugS $ "readSharedHolType: Expected a hol type but"
++ " instead got following tag: " ++ show (b, t)
readParseType :: MSaxState HolParseType
readParseType = do
(b, t) <- tag
case (b, t) of
(True, "Prefix") -> do
expectTag False "Prefix"
return PrefixT
(True, "InfixR") -> do
i <- readInt
expectTag False "InfixR"
return $ InfixR i
(True, "InfixL") -> do
i <- readInt
expectTag False "InfixL"
return $ InfixL i
(True, "Normal") -> do
expectTag False "Normal"
return Normal
(True, "Binder") -> do
expectTag False "Binder"
return Binder
_ -> debugS $ "readParseType: Expected a parse type but"
++ " instead got following tag: " ++ show (b, t)
readTermInfo :: MSaxState HolTermInfo
readTermInfo = do
p <- readParseType
MaybeT $ do
v <- runMaybeT $ readTuple readWord readParseType
case v of
Just _ -> return $ Just $ HolTermInfo (p, v)
_ -> return $ Just $ HolTermInfo (p, Nothing)
readSharedHolTerm ts sl m = do
d <- getM
(b, tg) <- tag
case (b, tg) of
(True, "Var") -> do
(n, t) <- readTuple readInt readInt
ti <- readTermInfo
case (Map.lookup n sl, Map.lookup t ts) of
(Just name, Just tp) -> do
expectTag False "Var"
return $ Map.insert (Map.size m + 1) (Var name tp ti) m
(r1, r2) -> debugS $ "readSharedHolTerm: Couldn't build Var"
++ " because the result of the lookup for "
++ show (n, t) ++ " was " ++ show (r1, r2)
(True, "Const") -> do
(n, t) <- readTuple readInt readInt
ti <- readTermInfo
case (Map.lookup n sl, Map.lookup t ts) of
(Just name, Just tp) -> do
expectTag False "Const"
return $ Map.insert (Map.size m + 1) (Const name tp ti) m
(r1, r2) -> debugS $ "readSharedHolTerm: Couldn't build Const"
++ " because the result of the lookup for "
++ show (n, t) ++ " was " ++ show (r1, r2)
(True, "Comb") -> do
(t1, t2) <- readTuple readInt readInt
case (Map.lookup t1 m, Map.lookup t2 m) of
(Just t1', Just t2') -> do
expectTag False "Comb"
return $ Map.insert (Map.size m + 1) (Comb t1' t2') m
(r1, r2) -> debugS $ "readSharedHolTerm: Couldn't build Comb"
++ " because the result of the lookup for "
++ show (t1, t2) ++ " was " ++ show (r1, r2)
(True, "Abs") -> do
(t1, t2) <- readTuple readInt readInt
case (Map.lookup t1 m, Map.lookup t2 m) of
(Just t1', Just t2') -> do
expectTag False "Abs"
return $ Map.insert (Map.size m + 1) (Abs t1' t2') m
(r1, r2) -> debugS $ "readSharedHoLTerm: Couldn't build Abs"
++ " because the result of the lookup for "
++ show (t1, t2) ++ " was " ++ show (r1, r2)
_ -> do
putM d
debugS $ "readSharedHolTerm: Expected a hol term but"
++ " instead got following tag: " ++ show (b, tg)
importData :: HetcatsOpts -> FilePath
-> IO ([(String, [(String, Term)])], [(String, String)])
importData opts fp' = do
fp <- canonicalizePath fp'
let image = "hol_light.dmtcp"
dmtcpBin = "dmtcp_restart"
tmpImage <- getTempFile "" image
imageFile <- fmap (</> image) $ getEnvDef
"HETS_HOLLIGHT_TOOLS" "HolLight/OcamlTools/"
-- for dmtcp we need an image owned by the current user
copyFile imageFile tmpImage
e2 <- doesFileExist imageFile
unless e2 $ fail $ image ++ " not found"
tempFile <- getTempFile "" (takeBaseName fp)
(ex, sout, err) <- executeProcess dmtcpBin [tmpImage]
$ "use_file " ++ show fp ++ ";;\n"
++ "inject_hol_include " ++ show fp ++ ";;\n"
++ "export_libs (get_libs()) " ++ show tempFile ++ ";;\n"
++ "exit 0;;\n"
removeFile tmpImage
s <- L.readFile tempFile
case ex of
ExitFailure _ -> do
removeFile tempFile
fail $ "HolLight.importData: " ++ err
ExitSuccess -> do
putIfVerbose opts 5 sout
let e = ([], [])
(r, evl, msgs) <- return $ case runMSaxState (do
expectTag True "HolExport"
sl <- readL readStr "Strings"
let strings = Map.fromList (zip [1 ..] sl)
hol_types <- foldS (readSharedHolType strings)
Map.empty "SharedHolTypes"
hol_terms <- foldS (readSharedHolTerm hol_types strings)
Map.empty "SharedHolTerms"
libs <- readL (readTuple readWord
(whileM (readTuple readWord
(readMappedInt hol_terms)))) "Libs"
liblinks <- readL (readTuple readWord readWord) "LibLinks"
return (libs, liblinks)) (parsexml s) (verbose opts >= 6) of
(de, msgs) -> (fromMaybe e de, "Next 5 items: "
++ show (take 5 $ fst msgs), fst $ snd msgs)
case msgs of
Just ms -> putIfVerbose opts 6 $ unlines (reverse ms) ++ evl
Nothing -> return ()
removeFile tempFile
return r
getTypes m t = case t of
TyVar _ -> m
TyApp s ts -> let m' = foldl getTypes m ts in
Map.insert s (length ts) m'
mergeTypesOps (ts1, ops1) (ts2, ops2) =
getOps :: Term
getOps tm = case tm of
Var _ t _ -> let ts = getTypes Map.empty t
in (ts, Map.empty)
Const s t _ -> let ts = getTypes Map.empty t
in (ts, Map.insert s t Map.empty)
Comb t1 t2 -> mergeTypesOps
(getOps t1)
(getOps t2)
Abs t1 t2 -> mergeTypesOps
(getOps t1)
(getOps t2)
calcSig :: [(String, Term)] -> Sign
calcSig tm = let (ts, os) = foldl
(\ p (_, t) -> (mergeTypesOps (getOps t) p))
in Sign {
types = ts
, ops = os }
sigDepends :: Sign -> Sign -> Bool
sigDepends s1 s2 = (Map.size (Map.intersection (types s1) (types s2)) /= 0) ||
(Map.size (Map.intersection (ops s1) (ops s2)) /= 0)
prettifyTypeVarsTp :: HolType -> Map.Map String String
-> (HolType, Map.Map String String)
prettifyTypeVarsTp (TyVar s) m = case Map.lookup s m of
Just s' -> (TyVar s', m)
Nothing -> let s' = '\'' : (names !! Map.size m)
in (TyVar s', Map.insert s s' m)
prettifyTypeVarsTp (TyApp s ts) m =
let (ts', m') = foldl (\ (ts'', m'') t ->
let (t', m''') = prettifyTypeVarsTp t m''
in (t' : ts'', m''')) ([], m) ts
in (TyApp s ts', m')
prettifyTypeVarsTm :: Term -> Map.Map String String
-> (Term, Map.Map String String)
prettifyTypeVarsTm (Const s t p) _ =
let (t1, m1) = prettifyTypeVarsTp t Map.empty
in (Const s t1 p, m1)
prettifyTypeVarsTm (Comb tm1 tm2) m =
let (tm1', m1) = prettifyTypeVarsTm tm1 m
(tm2', m2) = prettifyTypeVarsTm tm2 m1
in (Comb tm1' tm2', m2)
prettifyTypeVarsTm (Abs tm1 tm2) m =
let (tm1', m1) = prettifyTypeVarsTm tm1 m
(tm2', m2) = prettifyTypeVarsTm tm2 m1
in (Abs tm1' tm2', m2)
prettifyTypeVarsTm t m = (t, m)
prettifyTypeVars :: ([(String, [(String, Term)])], [(String, String)]) ->
([(String, [(String, Term)])], [(String, String)])
prettifyTypeVars (libs, lnks) =
let libs' = map (\ (s, terms) ->
let terms' = foldl (\ tms (ts, t) ->
let (t', _) = prettifyTypeVarsTm t Map.empty
in ((ts, t') : tms))
[] terms
in (s, terms')
) libs
in (libs', lnks)
treeLevels :: [(String, String)] -> Map.Map Int [(String, String)]
treeLevels l =
let lk = foldr (\ (imp, t) l' ->
case lookup t l' of
Just (p, _) -> (imp, (p + 1, t)) : l'
Nothing -> (imp, (1, t)) : (t, (0, "")) : l') [] l
in foldl (\ m (imp, (p, t)) ->
let s = Map.findWithDefault [] p m
in Map.insert p ((imp, t) : s) m) Map.empty lk
makeNamedSentence :: String -> Term -> Named Sentence
makeNamedSentence n t = makeNamed n Sentence { term = t, proof = Nothing }
_insNodeDG :: Sign -> [Named Sentence] -> FilePath -> String
-> (DGraph, Map.Map String
(String, Data.Graph.Inductive.Graph.Node, DGNodeLab))
-> (DGraph, Map.Map String
(String, Data.Graph.Inductive.Graph.Node, DGNodeLab))
_insNodeDG sig sens path n (dg, m) =
let gt = G_theory HolLight Nothing (makeExtSign HolLight sig) startSigId
(toThSens sens) startThId
n' = snd (System.FilePath.splitFileName n)
labelK = newInfoNodeLab
(makeName (simpleIdToIRI $ mkSimpleId n'))
(newNodeInfo DGEmpty)
gt
k = getNewNodeDG dg
m' = Map.insert n (n, k, labelK) m
insN = [InsertNode (k, labelK)]
newDG = changesDGH dg insN
labCh = [SetNodeLab labelK (k, labelK
{ globalTheory = computeLabelTheory Map.empty (emptyLibName
(System.FilePath.takeBaseName path)) newDG
(k, labelK) })]
newDG1 = changesDGH newDG labCh in (newDG1, m')
anaHolLightFile :: HetcatsOpts -> FilePath -> IO (Maybe (LibName, LibEnv))
anaHolLightFile opts path = do
(libs_, lnks_) <- importData opts path
let (libs, lnks) = prettifyTypeVars (libs_, lnks_)
let h = treeLevels lnks
let fixLinks m l =
case l of
(l1 : l2 : l') ->
if snd l1 == snd l2 && sigDepends
(Map.findWithDefault emptySig (fst l1) m)
(Map.findWithDefault emptySig (fst l2) m) then
(fst l1, fst l2) : fixLinks m (l2 : l')
else l1 : l2 : fixLinks m l'
l' -> l'
let uniteSigs = foldl (\ m' (s, t) ->
case resultToMaybe
(sigUnion (Map.findWithDefault emptySig s m')
(Map.findWithDefault emptySig t m')) of
Nothing -> m'
Just new_tsig -> Map.insert t new_tsig m')
let m = foldl (\ m' (s, l) -> Map.insert s (calcSig l) m') Map.empty libs
let (m', lnks') = foldr (\ lvl (m'', lnks_loc) ->
let lvl' = Map.findWithDefault [] lvl h
lnks_next = fixLinks m'' (reverse lvl')
{- we'd probably need to take care of dependencies on previously
imported files not imported by the file imported last -}
in (uniteSigs m'' lnks_next, lnks_next ++ lnks_loc)
) (m, []) [0 .. (Map.size h - 1)]
let (dg', node_m) = foldr (\ (lname, lterms) (dg, node_m') ->
let sig = Map.findWithDefault emptySig lname m'
sens = map (uncurry makeNamedSentence) lterms in
_insNodeDG sig sens path lname (dg, node_m')) (emptyDG, Map.empty) libs
dg'' = foldr (\ (source, target) dg ->
case Map.lookup source node_m of
Just (n, k, _) ->
case Map.lookup target node_m of
Just (n1, k1, _) ->
let sig = Map.findWithDefault emptySig n m'
sig1 = Map.findWithDefault emptySig n1 m'
in case resultToMaybe $
subsig_inclusion HolLight sig sig1 of
Nothing -> dg
Just incl ->
let inclM = gEmbed $ mkG_morphism HolLight incl
insE = [InsertEdge (k, k1, globDefLink inclM DGLinkImports)]
in changesDGH dg insE
Nothing -> dg
Nothing -> dg) dg' lnks'
le = Map.insert (emptyLibName
(System.FilePath.takeBaseName path))
dg'' Map.empty
return (Just (emptyLibName
(System.FilePath.takeBaseName path),
computeLibEnvTheories le))