4751N/A{- |

4751N/AModule : ./HolLight/HolLight2DG.hs

4751N/ADescription : Import data generated by hol2hets into a DG

4751N/ACopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010

4751N/ALicense : GPLv2 or higher, see LICENSE.txt

4751N/A

4751N/AMaintainer : jonathan.von_schroeder@dfki.de

4751N/AStability : experimental

4751N/APortability : portable

4751N/A

4751N/A-}

4751N/A

4751N/Amodule HolLight.HolLight2DG where

4751N/A

4751N/Aimport Static.GTheory

4751N/Aimport Static.DevGraph

4751N/A

4751N/Aimport Static.DgUtils

4751N/Aimport Static.History

4751N/Aimport Static.ComputeTheory

4751N/A

4751N/Aimport Logic.Logic

4751N/Aimport Logic.Prover

4751N/Aimport Logic.ExtSign

4751N/Aimport Logic.Grothendieck

5061N/A

4751N/Aimport Common.LibName

4751N/Aimport Common.Id

4751N/Aimport Common.IRI (simpleIdToIRI)

4751N/Aimport Common.AS_Annotation

4751N/Aimport Common.Result

4751N/Aimport Common.Utils

4751N/Aimport Common.SAX

4751N/Aimport Control.Monad

4751N/Aimport Common.Lib.Maybe

4751N/Aimport qualified Data.ByteString.Lazy as L

4751N/Aimport Text.XML.Expat.SAX

4751N/A

4751N/Aimport HolLight.Sign

4751N/Aimport HolLight.Sentence

4751N/Aimport HolLight.Term

4751N/Aimport HolLight.Logic_HolLight

4751N/A

4751N/Aimport HolLight.Helper (names)

4751N/A

4751N/Aimport Driver.Options

4751N/A

4751N/Aimport Data.Graph.Inductive.Graph

4751N/Aimport qualified Data.Map as Map

4751N/Aimport Data.Maybe (fromMaybe)

4751N/A

4751N/Aimport System.Exit

4751N/Aimport System.Directory

4751N/Aimport System.FilePath

4751N/A

4751N/AreadTuple :: (Show a, Show b) => MSaxState a -> MSaxState b -> MSaxState (a, b)

4751N/AreadTuple f1 f2 = do

4751N/A expectTag True "tuple"

4751N/A t1 <- readWithTag f1 "fst"

4751N/A t2 <- readWithTag f2 "snd"

4751N/A expectTag False "tuple"

4751N/A return (t1, t2)

4751N/A

4751N/AreadWord :: MSaxState String

4751N/AreadWord = liftM reverse $ foldCatchLeft (\ s ->

4751N/A do

4751N/A s' <- do

4751N/A dropSpaces

4751N/A d <- getD

4751N/A case d of

4751N/A [] -> error "HolLight.readWord"

4751N/A h : xs -> case h of

4751N/A CharacterData s' -> do

4751N/A putD xs

4751N/A return s'

4751N/A _ -> debugS $ "Expected character data but instead got: " ++ show h

4751N/A return $ trimLeft (reverse $ trimLeft s') ++ s) []

4751N/A

4751N/AreadStr :: MSaxState String

4751N/AreadStr = readWithTag readWord "s"

4751N/A

4751N/AreadInt :: MSaxState Int

4751N/AreadInt = do

4751N/A w <- readWord

4751N/A return $ fromMaybe (error "HolLight.readInt") $ readMaybe w

4751N/A

4751N/AreadInt' :: MSaxState Int

4751N/AreadInt' = readWithTag readInt "i"

4751N/A

4751N/AreadMappedInt :: Map.Map Int a -> MSaxState a

4751N/AreadMappedInt m = do

4751N/A i <- readInt

4751N/A case Map.lookup i m of

4751N/A Just a -> return a

4751N/A _ -> debugS $ "readMappedInt: Integer " ++ show i ++ " not mapped"

4751N/A

5061N/AlistToTypes :: Map.Map Int HolType -> [Int] -> Maybe [HolType]

4751N/AlistToTypes m l = case l of

4751N/A x : xs -> case Map.lookup x m of

4751N/A Just t -> case listToTypes m xs of

4751N/A Just ts -> Just (t : ts)

4751N/A _ -> Nothing

4751N/A _ -> Nothing

4751N/A [] -> Just []

4751N/A

4751N/AreadSharedHolType :: Map.Map Int String -> Map.Map Int HolType

4751N/A -> MSaxState (Map.Map Int HolType)

4751N/AreadSharedHolType sl m = do

4751N/A d <- getM

4751N/A (b, t) <- tag

4751N/A case (b, t) of

4751N/A (True, "TyApp") -> do

4751N/A (i, l) <- readTuple readInt (whileM readInt')

4751N/A case (Map.lookup i sl, listToTypes m l) of

4751N/A (Just s, Just l') -> do

4751N/A expectTag False "TyApp"

4751N/A return $ Map.insert (Map.size m + 1) (TyApp s $ reverse l') m

4751N/A (r1, r2) -> debugS $ "readSharedHolType: Couldn't build TyApp"

4751N/A ++ " because the result of the lookup for "

4751N/A ++ show (i, l) ++ " was " ++ show (r1, r2)

4751N/A (True, "TyVar") -> do

4751N/A i <- readInt

4751N/A case Map.lookup i sl of

4751N/A Just s -> do

4751N/A expectTag False "TyVar"

4751N/A return $ Map.insert (Map.size m + 1) (TyVar s) m

4751N/A _ -> debugS $ "readSharedHolType: Couldn't build TyVar"

4751N/A ++ " because looking up " ++ show i

4751N/A ++ " failed"

4751N/A _ -> do

4751N/A putM d

4751N/A debugS $ "readSharedHolType: Expected a hol type but"

4751N/A ++ " instead got following tag: " ++ show (b, t)

4751N/A

4751N/AreadParseType :: MSaxState HolParseType

4751N/AreadParseType = do

4751N/A (b, t) <- tag

4751N/A case (b, t) of

4751N/A (True, "Prefix") -> do

4751N/A expectTag False "Prefix"

4751N/A return PrefixT

4751N/A (True, "InfixR") -> do

4751N/A i <- readInt

4751N/A expectTag False "InfixR"

4751N/A return $ InfixR i

4751N/A (True, "InfixL") -> do

4751N/A i <- readInt

4751N/A expectTag False "InfixL"

4751N/A return $ InfixL i

4751N/A (True, "Normal") -> do

4751N/A expectTag False "Normal"

4751N/A return Normal

4751N/A (True, "Binder") -> do

4751N/A expectTag False "Binder"

4751N/A 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 :: Map.Map Int HolType -> Map.Map Int String

-> Map.Map Int Term -> MSaxState (Map.Map Int Term)

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 :: Map.Map String Int -> HolType -> Map.Map String Int

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 :: (Map.Map String Int, Map.Map String HolType)

-> (Map.Map String Int, Map.Map String HolType)

-> (Map.Map String Int, Map.Map String HolType)

mergeTypesOps (ts1, ops1) (ts2, ops2) =

(ts1 `Map.union` ts2, ops1 `Map.union` ops2)

getOps :: Term

-> (Map.Map String Int, Map.Map String HolType)

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))

(Map.empty, Map.empty) tm

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] -> 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 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 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 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))