ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst Schulz{- |

ce4924a895ca1c5859c24f5523d1e167fa04094aEwaryst SchulzModule : $Header$

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzDescription : Import data generated by hol2hets into a DG

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzLicense : GPLv2 or higher, see LICENSE.txt

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : jonathan.von_schroeder@dfki.de

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzStability : experimental

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzPortability : portable

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz-}

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzmodule HolLight.HolLight2DG where

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Static.GTheory

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Static.DevGraph

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Static.DgUtils

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Static.History

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Static.ComputeTheory

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Logic.Logic

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Logic.Prover

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Logic.ExtSign

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Logic.Grothendieck

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulzimport Common.LibName

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Common.Id

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Common.AS_Annotation

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Common.Result

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport HolLight.Sign

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulzimport HolLight.Sentence

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport HolLight.Term

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport HolLight.Logic_HolLight

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport HolLight.Helper

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulzimport Driver.Options

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Data.Graph.Inductive.Graph

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport qualified Data.Map as Map

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport qualified Data.Set as Set

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport qualified Data.Char

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport qualified System.FilePath.Posix

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport Text.XML.Expat.SAX

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzimport qualified Data.ByteString.Lazy as L

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulztype SaxEvL = [SAXEvent String String]

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzparsexml :: L.ByteString -> SaxEvL

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzparsexml txt = parse defaultParseOptions txt

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulzis_space :: String -> Bool

138b4f53daa114054371914372c3c5bc581ac79dEwaryst Schulzis_space = all Data.Char.isSpace

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulztag :: SaxEvL -> SaxEvL

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulztag = dropWhile (\e -> case e of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (CharacterData d) -> is_space d

138b4f53daa114054371914372c3c5bc581ac79dEwaryst Schulz _ -> False)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzdropSpaces :: SaxEvL -> SaxEvL

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzdropSpaces = tag

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzwhileJust :: b -> (b -> (Maybe a,b)) -> (Maybe [a],b)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzwhileJust d f =

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz case f d of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz (Just r,d') ->

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz case whileJust d' f of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz (Just l,d'') -> (Just (r:l),d'')

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Just [r],d')

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Just [],d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzreadL :: (SaxEvL -> (Maybe a,SaxEvL)) -> String -> SaxEvL -> (Maybe [a],SaxEvL)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzreadL f s d = case tag d of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz ((StartElement s' _):d') -> if (s'/=s) then (Nothing,d) else case whileJust d' f of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz (Just l,d'') -> case tag d'' of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz ((EndElement s''):d''') -> if (s''/=s) then (Nothing,d) else (Just l,d''')

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzreadList' :: (SaxEvL -> (Maybe a,SaxEvL)) -> SaxEvL -> (Maybe [a],SaxEvL)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzreadList' f d = case whileJust d f of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz (Just l,d') -> (Just l,d')

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzwhileJust' :: b -> (b -> a -> (Maybe a,b)) -> a -> (Maybe a,b)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzwhileJust' d f s = case f d s of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just s',d') -> case whileJust' d' f s' of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz r@(Just _,_) -> r

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Just s',d')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzfoldS :: (SaxEvL -> b -> (Maybe b,SaxEvL)) -> b -> String -> SaxEvL -> (Maybe b,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzfoldS f b s d = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement s' _):d') -> if (s'/=s) then (Nothing,d) else case whileJust' d' f b of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just b',d'') -> case tag d'' of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement s''):d''') -> if (s''/=s) then (Nothing,d) else (Just b',d''')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadTuple :: (Show a,Show b) => (SaxEvL -> (Maybe a,SaxEvL)) -> (SaxEvL -> (Maybe b,SaxEvL)) -> SaxEvL -> (Maybe (a,b),SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadTuple f1 f2 d = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "tuple" _):d1) -> case tag d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "fst" _):d2) -> case f1 d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just r1,d3) -> case tag d3 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "fst"):d4) -> case tag d4 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "snd" _):d5) -> case f2 d5 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just r2,d6) -> case tag d6 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "snd"):d7) -> case tag d7 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "tuple"):d8) -> (Just (r1,r2),d8)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadTuple' :: (SaxEvL -> (Maybe a,SaxEvL)) -> (SaxEvL -> a -> b -> (Maybe b,SaxEvL)) -> SaxEvL -> b -> (Maybe b,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadTuple' f1 f2 d b = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "tuple" _):d1) -> case tag d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "fst" _):d2) -> case f1 d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just r1,d3) -> case tag d3 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "fst"):d4) -> case tag d4 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "snd" _):d5) -> case f2 d5 r1 b of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just r2,d6) -> case tag d6 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "snd"):d7) -> case tag d7 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "tuple"):d8) -> (Just r2,d8)

138b4f53daa114054371914372c3c5bc581ac79dEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadWord' :: SaxEvL -> (Maybe String, SaxEvL)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst SchulzreadWord' d = case d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((CharacterData s):d') -> let b = Data.Char.isSpace

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz in case readWord' d' of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz (Just s',d'') -> (Just (reverse (dropWhile b (reverse (dropWhile b (s++s'))))),d'')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Just (reverse (dropWhile b (reverse (dropWhile b s)))),d')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadWord :: SaxEvL -> (Maybe String,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadWord d = case dropSpaces d of

138b4f53daa114054371914372c3c5bc581ac79dEwaryst Schulz ((CharacterData s):d') -> let b = Data.Char.isSpace

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz in case readWord' d' of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just s',d'') -> (Just (reverse (dropWhile b (reverse (dropWhile b (s++s'))))),d'')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Just (reverse (dropWhile b (reverse (dropWhile b s)))),d')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadStr :: SaxEvL -> (Maybe String,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadStr d = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "s" _):d') -> case readWord d' of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just s,d'') -> case tag d'' of

138b4f53daa114054371914372c3c5bc581ac79dEwaryst Schulz ((EndElement "s"):d''') -> (Just s,d''')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadInt :: SaxEvL -> (Maybe Int,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadInt d = case readWord d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just s,d') -> (Just ((read s)::Int),d')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadInt' :: SaxEvL -> (Maybe Int,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadInt' d = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "i" _):d') -> case readInt d' of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just i,d'') -> case tag d'' of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "i"):d''') -> (Just i,d''')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadMappedInt :: Map.Map Int a -> SaxEvL -> (Maybe a,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadMappedInt m d = case readInt d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just i,d') -> case Map.lookup i m of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just a) -> (Just a,d')

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzlistToTypes :: Map.Map Int HolType -> [Int] -> Maybe [HolType]

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzlistToTypes m l = case l of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (x:xs) -> case Map.lookup x m of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just t) -> case listToTypes m xs of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just ts) -> Just (t:ts)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> Nothing

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> Nothing

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz [] -> Just []

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadSharedHolType :: Map.Map Int String -> SaxEvL -> Map.Map Int HolType -> (Maybe (Map.Map Int HolType),SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadSharedHolType sl d m = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "TyApp" _):d1) -> case readTuple readInt (readList' readInt') d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just (i,l),d2) -> case Map.lookup i sl of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz (Just s) -> case listToTypes m l of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just l') -> case tag d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "TyApp"):d3) -> (Just (Map.insert ((Map.size m)+1) (TyApp s l') m),d3)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "TyVar" _):d1) -> case readInt d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just i,d2) -> case Map.lookup i sl of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just s) -> case tag d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "TyVar"):d3) -> (Just (Map.insert ((Map.size m)+1) (TyVar s) m),d3)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadParseType :: SaxEvL -> (Maybe HolParseType,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadParseType d = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "Prefix" _):d1) -> case tag d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "Prefix"):d2) -> (Just Prefix,d2)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "InfixR" _):d1) -> case readInt d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just i,d2) -> case tag d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "InfixR"):d3) -> (Just (InfixR i),d3)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "InfixL" _):d1) -> case readInt d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just i,d2) -> case tag d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "InfixL"):d3) -> (Just (InfixL i),d3)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz ((StartElement "Normal" _):d1) -> case tag d1 of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz ((EndElement "Normal"):d2) -> (Just Normal,d2)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz ((StartElement "Binder" _):d1) -> case tag d1 of

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz ((EndElement "Binder"):d2) -> (Just Binder,d2)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz _ -> (Nothing,d)

807f96a7e76bb825b1cb645f0f332c70c02ba145Ewaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadTermInfo :: SaxEvL -> (Maybe HolTermInfo,SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadTermInfo d = case readParseType d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just p,d1) -> case readTuple readWord readParseType d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just (s,p1),d2) -> (Just (HolTermInfo (p, Just (s,p1))),d2)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Just (HolTermInfo (p,Nothing)),d1)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadSharedHolTerm :: Map.Map Int HolType -> Map.Map Int String -> SaxEvL -> Map.Map Int Term -> (Maybe (Map.Map Int Term),SaxEvL)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst SchulzreadSharedHolTerm ts sl d m = case tag d of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "Var" _):d1) -> case readTuple readInt readInt d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just (n,t),d2) -> case readTermInfo d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just ti,d3) -> case Map.lookup n sl of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just name) -> case Map.lookup t ts of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just tp) -> case tag d3 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((EndElement "Var"):d4) -> (Just (Map.insert ((Map.size m)+1) (Var name tp ti) m),d4)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz _ -> (Nothing,d)

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz ((StartElement "Const" _):d1) -> case readTuple readInt readInt d1 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just (n,t),d2) -> case readTermInfo d2 of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just ti,d3) -> case Map.lookup n sl of

f3bef2616133ba9b19e678e463fccc799e284abaEwaryst Schulz (Just name) -> case Map.lookup t ts of

(Just tp) -> case tag d3 of

((EndElement "Const"):d4) -> (Just (Map.insert ((Map.size m)+1) (Const name tp ti) m),d4)

_ -> (Nothing,d)

_ -> (Nothing,d)

_ -> (Nothing,d)

_ -> (Nothing,d)

_ -> (Nothing,d)

((StartElement "Comb" _):d1) -> case readTuple readInt readInt d1 of

(Just (t1,t2),d2) -> case (Map.lookup t1 m,Map.lookup t2 m) of

(Just t1',Just t2') -> case tag d2 of

((EndElement "Comb"):d3) -> (Just (Map.insert ((Map.size m)+1) (Comb t1' t2') m),d3)

_ -> (Nothing,d)

_ -> (Nothing,d)

_ -> (Nothing,d)

((StartElement "Abs" _):d1) -> case readTuple readInt readInt d1 of

(Just (t1,t2),d2) -> case (Map.lookup t1 m,Map.lookup t2 m) of

(Just t1',Just t2') -> case tag d2 of

((EndElement "Abs"):d3) -> (Just (Map.insert ((Map.size m)+1) (Abs t1' t2') m),d3)

_ -> (Nothing,d)

_ -> (Nothing,d)

_ -> (Nothing,d)

_ -> (Nothing,d)

importData :: FilePath -> IO ([(String,[(String,Term)])],[(String,String)])

importData fp = do

s <- L.readFile fp

let e = ([],[])

case tag (parsexml s) of

((StartElement "HolExport" _):d) -> case readL readStr "Strings" d of

(Just sl,d1) ->

let strings = Map.fromList (zip [1..] sl)

in case foldS (readSharedHolType strings) Map.empty "SharedHolTypes" d1 of

(Just hol_types,d2) -> case foldS (readSharedHolTerm hol_types strings) Map.empty "SharedHolTerms" d2 of

(Just hol_terms,d3) -> case readL (readTuple readWord (readList' (readTuple readWord (readMappedInt hol_terms)))) "Libs" d3 of

(Just libs,d4) -> case readL (readTuple readWord readWord) "LibLinks" d4 of

(Just liblinks,_) -> return (libs,liblinks)

_ -> return e

_ -> return e

_ -> return e

_ -> return e

_ -> return e

_ -> return e

get_types :: Map.Map String Int -> HolType -> Map.Map String Int

get_types m t = case t of

(TyVar _) -> m

(TyApp s ts) -> let m' = foldl get_types m ts in

Map.insert s (length ts) m'

mergeTypesOps :: (Map.Map String Int,Map.Map String (Set.Set HolType))

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

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

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

(Map.union ts1 ts2,Map.unionWith Set.union ops1 ops2)

get_ops :: [String] -> Term

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

get_ops ign tm = case tm of

(Var s t _) -> let ts = get_types Map.empty t

in if not (elem s ign) then

(ts,Map.insert s (Set.fromList [t]) Map.empty)

else (ts,Map.empty)

(Const s t _) -> let ts = get_types Map.empty t

in (ts,Map.insert s (Set.fromList [t]) Map.empty)

(Comb t1 t2) -> mergeTypesOps

(get_ops ((name_of t1):ign) t1)

(get_ops ((name_of t1):ign) t2)

(Abs t1 t2) -> mergeTypesOps

(get_ops ((name_of t1):ign) t1)

(get_ops ((name_of t1):ign) t2)

calcSig :: [(String,Term)] -> Sign

calcSig tm = let (ts,os) = foldl

(\p (_,t) -> (mergeTypesOps (get_ops [] 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) ||

(foldl (||) False (map snd (Map.toList (Map.intersectionWith

(\a b -> (Set.size (Set.intersection a b))/=0)

(ops s1) (ops s2)))))

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 (makeExtSign HolLight sig) startSigId

(toThSens sens) startThId

n' = snd (System.FilePath.Posix.splitFileName n)

labelK = newInfoNodeLab

(makeName (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 path

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 m lnks' = 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') m lnks'

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 (\(n,t) -> makeNamedSentence n t) 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,lk) -> case Map.lookup target node_m of

Just (n1,k1,lk1) -> 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)]

newDG = changesDGH dg insE

updL = [SetNodeLab lk1 (k1, lk1

{ globalTheory = computeLabelTheory Map.empty newDG

(k1, lk1) }),

SetNodeLab lk (k, lk

{ globalTheory = computeLabelTheory Map.empty newDG

(k, lk) })]

in changesDGH newDG updL

Nothing -> dg

Nothing -> dg) dg' lnks'

le = Map.insert (emptyLibName (System.FilePath.Posix.takeBaseName path)) dg'' (Map.empty)

return (Just (emptyLibName (System.FilePath.Posix.takeBaseName path), le))