module HOL.OpenTheory.Package
where
import Control.Concurrent (forkIO)
import Control.Concurrent.MVar (newEmptyMVar,putMVar,readMVar)
import Control.Monad (foldM,guard)
import qualified Data.Char as Char
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import System.FilePath ((</>),(<.>),takeDirectory)
import qualified System.Process
import Text.Parsec ((<|>))
import qualified Text.Parsec as Parsec
import Text.Parsec.Text.Lazy ()
import Text.PrettyPrint ((<>),(<+>),($+$))
import qualified Text.PrettyPrint as PP
import HOL.OpenTheory.Article (readArticle)
import HOL.OpenTheory.Interpret (Interpret)
import qualified HOL.OpenTheory.Interpret as Interpret
import HOL.Parse
import HOL.Print
import HOL.Theory (Theory)
import qualified HOL.Theory as Theory
newtype Name = Name {destName :: String}
deriving (Eq,Ord,Show)
instance Printable Name where
toDoc = PP.text . destName
instance Parsable Name where
parser = do
c <- component
cs <- Parsec.many (Parsec.try (Parsec.char sep >> component))
return $ Name (List.intercalate [sep] (c : cs))
where
component = do
h <- Parsec.lower
t <- Parsec.many (Parsec.lower <|> Parsec.digit)
return (h : t)
sep = '-'
newtype Version = Version {destVersion :: String}
deriving (Eq,Ord,Show)
instance Printable Version where
toDoc = PP.text . destVersion
instance Parsable Version where
parser = do
cs <- Parsec.sepBy1 component (Parsec.char sep)
return $ Version (List.intercalate [sep] cs)
where
component = Parsec.many1 Parsec.digit
sep = '.'
data NameVersion = NameVersion {name :: Name, version :: Version}
deriving (Eq,Ord,Show)
instance Printable NameVersion where
toDoc (NameVersion n v) = toDoc n <> PP.char '-' <> toDoc v
instance Parsable NameVersion where
parser = do
n <- parser
_ <- Parsec.char '-'
v <- parser
return $ NameVersion n v
data KeyValue = KeyValue Name String
deriving (Eq,Ord,Show)
instance Printable KeyValue where
toDoc (KeyValue k v) = toDoc k <> PP.char ':' <+> PP.text v
instance Parsable KeyValue where
parser = do
Parsec.skipMany spaceParser
n <- parser
Parsec.skipMany spaceParser
_ <- Parsec.char ':'
Parsec.skipMany spaceParser
v <- Parsec.many lineParser
return $ KeyValue n (List.dropWhileEnd Char.isSpace v)
printKeyValue :: Printable a => Name -> a -> KeyValue
printKeyValue n a = KeyValue n (toString a)
matchKeyValue :: Name -> KeyValue -> Maybe String
matchKeyValue n (KeyValue k v) = if k == n then Just v else Nothing
parseKeyValue :: Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue n v = do
s <- matchKeyValue n v
a <- fromString s
return a
newtype Info = Info {destInfo :: [KeyValue]}
deriving (Eq,Ord,Show)
nullInfo :: Info -> Bool
nullInfo = null . destInfo
appendInfo :: Info -> Info -> Info
appendInfo (Info l) (Info l') = Info (l ++ l')
concatInfo :: [Info] -> Info
concatInfo = Info . concat . map destInfo
firstInfo :: (KeyValue -> Maybe a) -> Info -> Maybe (a,Info)
firstInfo f = g [] . destInfo
where
g _ [] = Nothing
g l (h : t) = case f h of
Just a -> Just (a, Info (foldl (flip (:)) t l))
Nothing -> g (h : l) t
firstGetInfo :: [Info -> Maybe (a,Info)] -> Info -> Maybe (a,Info)
firstGetInfo [] _ = Nothing
firstGetInfo (f : fs) i =
case f i of
Nothing -> firstGetInfo fs i
x -> x
mapGetInfo :: (a -> b) -> (Info -> Maybe (a,Info)) -> Info -> Maybe (b,Info)
mapGetInfo f g = let f0 (a,i) = (f a, i) in fmap f0 . g
maybeGetInfo :: (Info -> Maybe (a,Info)) -> Info -> (Maybe a, Info)
maybeGetInfo f i =
case f i of
Just (a,i') -> (Just a, i')
Nothing -> (Nothing,i)
listGetInfo :: (Info -> Maybe (a,Info)) -> Info -> ([a], Info)
listGetInfo f = g []
where
g l i = case f i of
Just (a,i') -> g (a : l) i'
Nothing -> (l,i)
instance Printable Info where
toDoc = PP.vcat . map toDoc . destInfo
instance Parsable Info where
parser = fmap Info $ Parsec.endBy parser eolParser
class Informative a where
toInfo :: a -> Info
getInfo :: Info -> Maybe (a,Info)
fromInfo :: Info -> Maybe a
fromInfo i = do
(a,i') <- getInfo i
guard $ nullInfo i'
return a
instance Informative a => Informative [a] where
toInfo = concatInfo . map toInfo
getInfo = Just . listGetInfo getInfo
instance (Informative a, Informative b) => Informative (a,b) where
toInfo (a,b) = appendInfo (toInfo a) (toInfo b)
getInfo i = do
(a,i') <- getInfo i
(b,i'') <- getInfo i'
return ((a,b),i'')
newtype File = File {destFile :: FilePath}
deriving (Eq,Ord,Show)
instance Printable File where
toDoc = PP.doubleQuotes . PP.text . destFile
instance Parsable File where
parser = do
_ <- Parsec.char '"'
f <- Parsec.many (Parsec.noneOf "\"\n")
_ <- Parsec.char '"'
return $ File f
data Interpretation =
Interpret Interpret.Rename
| Interpretation File
deriving (Eq,Ord,Show)
instance Informative Interpretation where
toInfo (Interpret i) = Info [printKeyValue (Name "interpret") i]
toInfo (Interpretation f) = Info [printKeyValue (Name "interpretation") f]
getInfo = firstGetInfo [getInterpret,getInterpretation]
where
getInterpret =
mapGetInfo Interpret
(firstInfo (parseKeyValue (Name "interpret")))
getInterpretation =
mapGetInfo Interpretation
(firstInfo (parseKeyValue (Name "interpretation")))
readInterpretation :: FilePath -> [Interpretation] -> IO Interpret
readInterpretation dir ints = do
rs <- mapM readRen ints
return $ Interpret.fromRenamesUnsafe (Interpret.concatRenames rs)
where
readRen (Interpret r) = return $ Interpret.Renames [r]
readRen (Interpretation f) = fromTextFile (dir </> destFile f)
data Operation =
Article File
| Include {package :: NameVersion, checksum :: Maybe String}
| Union
deriving (Eq,Ord,Show)
data Block =
Block
{block :: Name,
imports :: [Name],
interpret :: [Interpretation],
operation :: Operation}
deriving (Eq,Ord,Show)
instance Informative Operation where
toInfo (Article f) = Info [printKeyValue (Name "article") f]
toInfo (Include p c) = Info (pv : cv)
where
pv = printKeyValue (Name "package") p
cv = case c of
Just s -> [KeyValue (Name "checksum") s]
Nothing -> []
toInfo Union = Info []
getInfo =
firstGetInfo [getArticle,getInclude,getUnion]
where
getArticle = mapGetInfo Article getArticleFile
getInclude i = do
(p,i') <- getPackage i
let (c,i'') = maybeGetInfo getChecksum i'
return (Include p c, i'')
getUnion i = Just (Union,i)
getArticleFile = firstInfo (parseKeyValue (Name "article"))
getPackage = firstInfo (parseKeyValue (Name "package"))
getChecksum = firstInfo (matchKeyValue (Name "checksum"))
mkBlock :: Name -> Info -> Maybe Block
mkBlock n info = do
let (imp,info') = listGetInfo getImport info
(int,op) <- fromInfo info'
guard (op /= Union || null int)
return $ Block n imp int op
where
getImport = firstInfo (parseKeyValue (Name "import"))
destBlock :: Block -> (Name,Info)
destBlock (Block n imp int op) =
(n, appendInfo impInfo (toInfo (int,op)))
where
impInfo = Info (map (printKeyValue (Name "import")) imp)
instance Printable Block where
toDoc b =
(toDoc n <+> PP.lbrace) $+$
PP.nest 2 (toDoc i) $+$
PP.rbrace
where
(n,i) = destBlock b
instance Parsable Block where
parser = do
n <- opener
i <- parser
closer
case mkBlock n i of
Just b -> return b
Nothing -> Parsec.parserFail "couldn't parse block"
where
opener = do
Parsec.skipMany spaceParser
n <- parser
Parsec.skipMany spaceParser
_ <- Parsec.char '{'
Parsec.skipMany spaceParser
eolParser
return n
closer = do
Parsec.skipMany spaceParser
_ <- Parsec.char '}'
Parsec.skipMany spaceParser
data Package =
Package
{information :: Info,
source :: [Block]}
deriving (Eq,Ord,Show)
instance Printable Package where
toDoc (Package i bs) =
PP.vcat (List.intersperse (PP.text "") (toDoc i : map toDoc bs))
instance Parsable Package where
parser = do
Parsec.skipMany eolParser
i <- parser
Parsec.skipMany eolParser
bs <- Parsec.sepEndBy parser (Parsec.skipMany1 eolParser)
return $ Package i bs
requires :: Package -> [Name]
requires = fst . listGetInfo getRequires . information
where
getRequires = firstInfo (parseKeyValue (Name "requires"))
packageFile :: FilePath -> Name -> FilePath
packageFile d (Name n) = d </> n <.> "thy"
opentheory :: [String] -> IO String
opentheory args = System.Process.readProcess "opentheory" args []
opentheoryDirectory :: String -> IO FilePath
opentheoryDirectory s = do
dir <- opentheory ["info","--directory",s]
return $ List.dropWhileEnd Char.isSpace dir
directory :: Name -> IO FilePath
directory = opentheoryDirectory . toString
directoryVersion :: NameVersion -> IO FilePath
directoryVersion = opentheoryDirectory . toString
newtype Blocks = Blocks {destBlocks :: [Block]}
deriving (Eq,Ord,Show)
mkBlocks :: [Block] -> Blocks
mkBlocks bl = Blocks (check [] [] (Name "main"))
where
check st bs n =
if any ((==) n . block) bs then bs
else if notElem n st then add (n : st) bs (get n)
else error $ "import cycle including theory block " ++ toString n
add st bs b = b : foldl (check st) bs (imports b)
get n =
case filter ((==) n . block) bl of
[] -> error $ "missing theory block " ++ toString n
[b] -> b
_ : _ : _ -> error $ "multiple theory blocks named " ++ toString n
readVersion :: Theory -> Interpret -> NameVersion -> IO Theory
readVersion thy int nv = do
dir <- directoryVersion nv
readPackageFile thy int (packageFile dir (name nv))
readPackageFile :: Theory -> Interpret -> FilePath -> IO Theory
readPackageFile thy int file = do
pkg <- fromTextFile file
readPackage thy int (takeDirectory file) pkg
readPackage :: Theory -> Interpret -> FilePath -> Package -> IO Theory
readPackage thy int dir pkg = readBlocks thy int dir (mkBlocks (source pkg))
readBlocks :: Theory -> Interpret -> FilePath -> Blocks -> IO Theory
readBlocks thy int dir (Blocks bs) = do
vs <- foldM initT Map.empty bs
mapM_ (forkIO . mkT vs) bs
readMVar (getT vs (block (head bs)))
where
mkT vs b = do
ts <- mapM (readMVar . getT vs) (imports b)
t <- readBlock thy int dir ts b
putMVar (getT vs (block b)) t
getT vs n =
case Map.lookup n vs of
Just v -> v
Nothing -> error $ "bad theory block " ++ show n
initT vs b = do
v <- newEmptyMVar
return $ Map.insert (block b) v vs
readBlock :: Theory -> Interpret -> FilePath -> [Theory] -> Block -> IO Theory
readBlock envThy envInt dir impThys b = do
blockInt <- readInterpretation dir (interpret b)
let int = Interpret.compose blockInt envInt
case operation b of
Article f -> do
ths <- readArticle thy int (dir </> destFile f)
return $ Theory.fromThmSet ths
Include {package = nv} -> readVersion thy int nv
Union -> return impThy
where
thy = Theory.union envThy impThy
impThy = Theory.unionList impThys
newtype Requires = Requires (Map Name ([Name],FilePath,Blocks))
emptyRequires :: Requires
emptyRequires = Requires Map.empty
addRequires :: Requires -> Name -> IO Requires
addRequires = add
where
add (Requires m) n = fmap Requires $ check [] m n
check st m n =
if Map.member n m then return m
else if notElem n st then pkg (n : st) m n
else error $ "requires cycle including package " ++ toString n
pkg st m n = do
d <- directory n
p <- fromTextFile (packageFile d n)
let r = requires p
let s = mkBlocks (source p)
foldM (check st) (Map.insert n (r,d,s) m) r
fromListRequires :: [Name] -> IO Requires
fromListRequires = foldM addRequires emptyRequires
readList :: [Name] -> IO [Theory]
readList ns = do
req <- mkReq
vs <- foldM initT Map.empty req
mapM_ (forkIO . mkT vs) req
mapM (readMVar . getT vs) ns
where
mkReq = do
Requires m <- fromListRequires ns
return $ Map.toList m
mkT vs (n,(r,d,s)) = do
ts <- mapM (readMVar . getT vs) r
let thy = Theory.unionList (Theory.standard : ts)
t <- readBlocks thy Interpret.empty d s
putMVar (getT vs n) t
getT vs n =
case Map.lookup n vs of
Just v -> v
Nothing -> error $ "bad package " ++ show n
initT vs (n,_) = do
v <- newEmptyMVar
return $ Map.insert n v vs