{- |
module: $Header$
description: OpenTheory packages
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

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.Strict (Map)
import qualified Data.Map.Strict as Map
import Prelude hiding ((<>))
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

-------------------------------------------------------------------------------
-- Package names
-------------------------------------------------------------------------------

newtype Name = Name {Name -> String
destName :: String}
  deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq,Eq Name
Eq Name
-> (Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord,Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show)

instance Printable Name where
  toDoc :: Name -> Doc
toDoc = String -> Doc
PP.text (String -> Doc) -> (Name -> String) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
destName

instance Parsable Name where
  parser :: Parsec Text st Name
parser = do
      String
c <- ParsecT Text st Identity String
forall u. ParsecT Text u Identity String
component
      [String]
cs <- ParsecT Text st Identity String
-> ParsecT Text st Identity [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many (ParsecT Text st Identity String -> ParsecT Text st Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m a
Parsec.try (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
sep ParsecT Text st Identity Char
-> ParsecT Text st Identity String
-> ParsecT Text st Identity String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT Text st Identity String
forall u. ParsecT Text u Identity String
component))
      Name -> Parsec Text st Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Parsec Text st Name) -> Name -> Parsec Text st Name
forall a b. (a -> b) -> a -> b
$ String -> Name
Name (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char
sep] (String
c String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
cs))
    where
      component :: ParsecT Text u Identity String
component = do
          Char
h <- ParsecT Text u Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
Parsec.lower
          String
t <- ParsecT Text u Identity Char -> ParsecT Text u Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many (ParsecT Text u Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
Parsec.lower ParsecT Text u Identity Char
-> ParsecT Text u Identity Char -> ParsecT Text u Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT Text u Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
Parsec.digit)
          String -> ParsecT Text u Identity String
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
h Char -> ShowS
forall a. a -> [a] -> [a]
: String
t)

      sep :: Char
sep = Char
'-'

-------------------------------------------------------------------------------
-- Package versions
-------------------------------------------------------------------------------

newtype Version = Version {Version -> String
destVersion :: String}
  deriving (Version -> Version -> Bool
(Version -> Version -> Bool)
-> (Version -> Version -> Bool) -> Eq Version
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Version -> Version -> Bool
$c/= :: Version -> Version -> Bool
== :: Version -> Version -> Bool
$c== :: Version -> Version -> Bool
Eq,Eq Version
Eq Version
-> (Version -> Version -> Ordering)
-> (Version -> Version -> Bool)
-> (Version -> Version -> Bool)
-> (Version -> Version -> Bool)
-> (Version -> Version -> Bool)
-> (Version -> Version -> Version)
-> (Version -> Version -> Version)
-> Ord Version
Version -> Version -> Bool
Version -> Version -> Ordering
Version -> Version -> Version
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Version -> Version -> Version
$cmin :: Version -> Version -> Version
max :: Version -> Version -> Version
$cmax :: Version -> Version -> Version
>= :: Version -> Version -> Bool
$c>= :: Version -> Version -> Bool
> :: Version -> Version -> Bool
$c> :: Version -> Version -> Bool
<= :: Version -> Version -> Bool
$c<= :: Version -> Version -> Bool
< :: Version -> Version -> Bool
$c< :: Version -> Version -> Bool
compare :: Version -> Version -> Ordering
$ccompare :: Version -> Version -> Ordering
$cp1Ord :: Eq Version
Ord,Int -> Version -> ShowS
[Version] -> ShowS
Version -> String
(Int -> Version -> ShowS)
-> (Version -> String) -> ([Version] -> ShowS) -> Show Version
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Version] -> ShowS
$cshowList :: [Version] -> ShowS
show :: Version -> String
$cshow :: Version -> String
showsPrec :: Int -> Version -> ShowS
$cshowsPrec :: Int -> Version -> ShowS
Show)

instance Printable Version where
  toDoc :: Version -> Doc
toDoc = String -> Doc
PP.text (String -> Doc) -> (Version -> String) -> Version -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Version -> String
destVersion

instance Parsable Version where
  parser :: Parsec Text st Version
parser = do
      [String]
cs <- ParsecT Text st Identity String
-> ParsecT Text st Identity Char
-> ParsecT Text st Identity [String]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
Parsec.sepBy1 ParsecT Text st Identity String
forall u. ParsecT Text u Identity String
component (Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
sep)
      Version -> Parsec Text st Version
forall (m :: * -> *) a. Monad m => a -> m a
return (Version -> Parsec Text st Version)
-> Version -> Parsec Text st Version
forall a b. (a -> b) -> a -> b
$ String -> Version
Version (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char
sep] [String]
cs)
    where
      component :: ParsecT Text u Identity String
component = ParsecT Text u Identity Char -> ParsecT Text u Identity String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
Parsec.many1 ParsecT Text u Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
Parsec.digit
      sep :: Char
sep = Char
'.'

-------------------------------------------------------------------------------
-- Packages are stored in repos as name-version
-------------------------------------------------------------------------------

data NameVersion = NameVersion {NameVersion -> Name
name :: Name, NameVersion -> Version
version :: Version}
  deriving (NameVersion -> NameVersion -> Bool
(NameVersion -> NameVersion -> Bool)
-> (NameVersion -> NameVersion -> Bool) -> Eq NameVersion
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NameVersion -> NameVersion -> Bool
$c/= :: NameVersion -> NameVersion -> Bool
== :: NameVersion -> NameVersion -> Bool
$c== :: NameVersion -> NameVersion -> Bool
Eq,Eq NameVersion
Eq NameVersion
-> (NameVersion -> NameVersion -> Ordering)
-> (NameVersion -> NameVersion -> Bool)
-> (NameVersion -> NameVersion -> Bool)
-> (NameVersion -> NameVersion -> Bool)
-> (NameVersion -> NameVersion -> Bool)
-> (NameVersion -> NameVersion -> NameVersion)
-> (NameVersion -> NameVersion -> NameVersion)
-> Ord NameVersion
NameVersion -> NameVersion -> Bool
NameVersion -> NameVersion -> Ordering
NameVersion -> NameVersion -> NameVersion
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NameVersion -> NameVersion -> NameVersion
$cmin :: NameVersion -> NameVersion -> NameVersion
max :: NameVersion -> NameVersion -> NameVersion
$cmax :: NameVersion -> NameVersion -> NameVersion
>= :: NameVersion -> NameVersion -> Bool
$c>= :: NameVersion -> NameVersion -> Bool
> :: NameVersion -> NameVersion -> Bool
$c> :: NameVersion -> NameVersion -> Bool
<= :: NameVersion -> NameVersion -> Bool
$c<= :: NameVersion -> NameVersion -> Bool
< :: NameVersion -> NameVersion -> Bool
$c< :: NameVersion -> NameVersion -> Bool
compare :: NameVersion -> NameVersion -> Ordering
$ccompare :: NameVersion -> NameVersion -> Ordering
$cp1Ord :: Eq NameVersion
Ord,Int -> NameVersion -> ShowS
[NameVersion] -> ShowS
NameVersion -> String
(Int -> NameVersion -> ShowS)
-> (NameVersion -> String)
-> ([NameVersion] -> ShowS)
-> Show NameVersion
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NameVersion] -> ShowS
$cshowList :: [NameVersion] -> ShowS
show :: NameVersion -> String
$cshow :: NameVersion -> String
showsPrec :: Int -> NameVersion -> ShowS
$cshowsPrec :: Int -> NameVersion -> ShowS
Show)

instance Printable NameVersion where
  toDoc :: NameVersion -> Doc
toDoc (NameVersion Name
n Version
v) = Name -> Doc
forall a. Printable a => a -> Doc
toDoc Name
n Doc -> Doc -> Doc
<> Char -> Doc
PP.char Char
'-' Doc -> Doc -> Doc
<> Version -> Doc
forall a. Printable a => a -> Doc
toDoc Version
v

instance Parsable NameVersion where
  parser :: Parsec Text st NameVersion
parser = do
      Name
n <- Parsec Text st Name
forall a st. Parsable a => Parsec Text st a
parser
      Char
_ <- Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'-'
      Version
v <- Parsec Text st Version
forall a st. Parsable a => Parsec Text st a
parser
      NameVersion -> Parsec Text st NameVersion
forall (m :: * -> *) a. Monad m => a -> m a
return (NameVersion -> Parsec Text st NameVersion)
-> NameVersion -> Parsec Text st NameVersion
forall a b. (a -> b) -> a -> b
$ Name -> Version -> NameVersion
NameVersion Name
n Version
v

-------------------------------------------------------------------------------
-- Information formatted as key: value
-------------------------------------------------------------------------------

data KeyValue = KeyValue Name String
  deriving (KeyValue -> KeyValue -> Bool
(KeyValue -> KeyValue -> Bool)
-> (KeyValue -> KeyValue -> Bool) -> Eq KeyValue
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: KeyValue -> KeyValue -> Bool
$c/= :: KeyValue -> KeyValue -> Bool
== :: KeyValue -> KeyValue -> Bool
$c== :: KeyValue -> KeyValue -> Bool
Eq,Eq KeyValue
Eq KeyValue
-> (KeyValue -> KeyValue -> Ordering)
-> (KeyValue -> KeyValue -> Bool)
-> (KeyValue -> KeyValue -> Bool)
-> (KeyValue -> KeyValue -> Bool)
-> (KeyValue -> KeyValue -> Bool)
-> (KeyValue -> KeyValue -> KeyValue)
-> (KeyValue -> KeyValue -> KeyValue)
-> Ord KeyValue
KeyValue -> KeyValue -> Bool
KeyValue -> KeyValue -> Ordering
KeyValue -> KeyValue -> KeyValue
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: KeyValue -> KeyValue -> KeyValue
$cmin :: KeyValue -> KeyValue -> KeyValue
max :: KeyValue -> KeyValue -> KeyValue
$cmax :: KeyValue -> KeyValue -> KeyValue
>= :: KeyValue -> KeyValue -> Bool
$c>= :: KeyValue -> KeyValue -> Bool
> :: KeyValue -> KeyValue -> Bool
$c> :: KeyValue -> KeyValue -> Bool
<= :: KeyValue -> KeyValue -> Bool
$c<= :: KeyValue -> KeyValue -> Bool
< :: KeyValue -> KeyValue -> Bool
$c< :: KeyValue -> KeyValue -> Bool
compare :: KeyValue -> KeyValue -> Ordering
$ccompare :: KeyValue -> KeyValue -> Ordering
$cp1Ord :: Eq KeyValue
Ord,Int -> KeyValue -> ShowS
[KeyValue] -> ShowS
KeyValue -> String
(Int -> KeyValue -> ShowS)
-> (KeyValue -> String) -> ([KeyValue] -> ShowS) -> Show KeyValue
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [KeyValue] -> ShowS
$cshowList :: [KeyValue] -> ShowS
show :: KeyValue -> String
$cshow :: KeyValue -> String
showsPrec :: Int -> KeyValue -> ShowS
$cshowsPrec :: Int -> KeyValue -> ShowS
Show)

instance Printable KeyValue where
  toDoc :: KeyValue -> Doc
toDoc (KeyValue Name
k String
v) = Name -> Doc
forall a. Printable a => a -> Doc
toDoc Name
k Doc -> Doc -> Doc
<> Char -> Doc
PP.char Char
':' Doc -> Doc -> Doc
<+> String -> Doc
PP.text String
v

instance Parsable KeyValue where
  parser :: Parsec Text st KeyValue
parser = do
      ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text st Identity ()
forall st. Parsec Text st ()
spaceParser
      Name
n <- Parsec Text st Name
forall a st. Parsable a => Parsec Text st a
parser
      ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text st Identity ()
forall st. Parsec Text st ()
spaceParser
      Char
_ <- Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
':'
      ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text st Identity ()
forall st. Parsec Text st ()
spaceParser
      String
v <- ParsecT Text st Identity Char -> ParsecT Text st Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many ParsecT Text st Identity Char
forall st. Parsec Text st Char
lineParser
      KeyValue -> Parsec Text st KeyValue
forall (m :: * -> *) a. Monad m => a -> m a
return (KeyValue -> Parsec Text st KeyValue)
-> KeyValue -> Parsec Text st KeyValue
forall a b. (a -> b) -> a -> b
$ Name -> String -> KeyValue
KeyValue Name
n ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Char -> Bool
Char.isSpace String
v)

printKeyValue :: Printable a => Name -> a -> KeyValue
printKeyValue :: Name -> a -> KeyValue
printKeyValue Name
n a
a = Name -> String -> KeyValue
KeyValue Name
n (a -> String
forall a. Printable a => a -> String
toString a
a)

matchKeyValue :: Name -> KeyValue -> Maybe String
matchKeyValue :: Name -> KeyValue -> Maybe String
matchKeyValue Name
n (KeyValue Name
k String
v) = if Name
k Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n then String -> Maybe String
forall a. a -> Maybe a
Just String
v else Maybe String
forall a. Maybe a
Nothing

parseKeyValue :: Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue :: Name -> KeyValue -> Maybe a
parseKeyValue Name
n KeyValue
v = do
    String
s <- Name -> KeyValue -> Maybe String
matchKeyValue Name
n KeyValue
v
    a
a <- String -> Maybe a
forall a. Parsable a => String -> Maybe a
fromString String
s
    a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-------------------------------------------------------------------------------
-- Package information
-------------------------------------------------------------------------------

newtype Info = Info {Info -> [KeyValue]
destInfo :: [KeyValue]}
  deriving (Info -> Info -> Bool
(Info -> Info -> Bool) -> (Info -> Info -> Bool) -> Eq Info
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Info -> Info -> Bool
$c/= :: Info -> Info -> Bool
== :: Info -> Info -> Bool
$c== :: Info -> Info -> Bool
Eq,Eq Info
Eq Info
-> (Info -> Info -> Ordering)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Bool)
-> (Info -> Info -> Info)
-> (Info -> Info -> Info)
-> Ord Info
Info -> Info -> Bool
Info -> Info -> Ordering
Info -> Info -> Info
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Info -> Info -> Info
$cmin :: Info -> Info -> Info
max :: Info -> Info -> Info
$cmax :: Info -> Info -> Info
>= :: Info -> Info -> Bool
$c>= :: Info -> Info -> Bool
> :: Info -> Info -> Bool
$c> :: Info -> Info -> Bool
<= :: Info -> Info -> Bool
$c<= :: Info -> Info -> Bool
< :: Info -> Info -> Bool
$c< :: Info -> Info -> Bool
compare :: Info -> Info -> Ordering
$ccompare :: Info -> Info -> Ordering
$cp1Ord :: Eq Info
Ord,Int -> Info -> ShowS
[Info] -> ShowS
Info -> String
(Int -> Info -> ShowS)
-> (Info -> String) -> ([Info] -> ShowS) -> Show Info
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Info] -> ShowS
$cshowList :: [Info] -> ShowS
show :: Info -> String
$cshow :: Info -> String
showsPrec :: Int -> Info -> ShowS
$cshowsPrec :: Int -> Info -> ShowS
Show)

nullInfo :: Info -> Bool
nullInfo :: Info -> Bool
nullInfo = [KeyValue] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([KeyValue] -> Bool) -> (Info -> [KeyValue]) -> Info -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Info -> [KeyValue]
destInfo

appendInfo :: Info -> Info -> Info
appendInfo :: Info -> Info -> Info
appendInfo (Info [KeyValue]
l) (Info [KeyValue]
l') = [KeyValue] -> Info
Info ([KeyValue]
l [KeyValue] -> [KeyValue] -> [KeyValue]
forall a. [a] -> [a] -> [a]
++ [KeyValue]
l')

concatInfo :: [Info] -> Info
concatInfo :: [Info] -> Info
concatInfo = [KeyValue] -> Info
Info ([KeyValue] -> Info) -> ([Info] -> [KeyValue]) -> [Info] -> Info
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[KeyValue]] -> [KeyValue]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[KeyValue]] -> [KeyValue])
-> ([Info] -> [[KeyValue]]) -> [Info] -> [KeyValue]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Info -> [KeyValue]) -> [Info] -> [[KeyValue]]
forall a b. (a -> b) -> [a] -> [b]
map Info -> [KeyValue]
destInfo

firstInfo :: (KeyValue -> Maybe a) -> Info -> Maybe (a,Info)
firstInfo :: (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo KeyValue -> Maybe a
f = [KeyValue] -> [KeyValue] -> Maybe (a, Info)
g [] ([KeyValue] -> Maybe (a, Info))
-> (Info -> [KeyValue]) -> Info -> Maybe (a, Info)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Info -> [KeyValue]
destInfo
  where
    g :: [KeyValue] -> [KeyValue] -> Maybe (a, Info)
g [KeyValue]
_ [] = Maybe (a, Info)
forall a. Maybe a
Nothing
    g [KeyValue]
l (KeyValue
h : [KeyValue]
t) = case KeyValue -> Maybe a
f KeyValue
h of
                    Just a
a -> (a, Info) -> Maybe (a, Info)
forall a. a -> Maybe a
Just (a
a, [KeyValue] -> Info
Info (([KeyValue] -> KeyValue -> [KeyValue])
-> [KeyValue] -> [KeyValue] -> [KeyValue]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((KeyValue -> [KeyValue] -> [KeyValue])
-> [KeyValue] -> KeyValue -> [KeyValue]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (:)) [KeyValue]
t [KeyValue]
l))
                    Maybe a
Nothing -> [KeyValue] -> [KeyValue] -> Maybe (a, Info)
g (KeyValue
h KeyValue -> [KeyValue] -> [KeyValue]
forall a. a -> [a] -> [a]
: [KeyValue]
l) [KeyValue]
t

firstGetInfo :: [Info -> Maybe (a,Info)] -> Info -> Maybe (a,Info)
firstGetInfo :: [Info -> Maybe (a, Info)] -> Info -> Maybe (a, Info)
firstGetInfo [] Info
_ = Maybe (a, Info)
forall a. Maybe a
Nothing
firstGetInfo (Info -> Maybe (a, Info)
f : [Info -> Maybe (a, Info)]
fs) Info
i =
    case Info -> Maybe (a, Info)
f Info
i of
      Maybe (a, Info)
Nothing -> [Info -> Maybe (a, Info)] -> Info -> Maybe (a, Info)
forall a. [Info -> Maybe (a, Info)] -> Info -> Maybe (a, Info)
firstGetInfo [Info -> Maybe (a, Info)]
fs Info
i
      Maybe (a, Info)
x -> Maybe (a, Info)
x

mapGetInfo :: (a -> b) -> (Info -> Maybe (a,Info)) -> Info -> Maybe (b,Info)
mapGetInfo :: (a -> b) -> (Info -> Maybe (a, Info)) -> Info -> Maybe (b, Info)
mapGetInfo a -> b
f Info -> Maybe (a, Info)
g = let f0 :: (a, b) -> (b, b)
f0 (a
a,b
i) = (a -> b
f a
a, b
i) in ((a, Info) -> (b, Info)) -> Maybe (a, Info) -> Maybe (b, Info)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a, Info) -> (b, Info)
forall b. (a, b) -> (b, b)
f0 (Maybe (a, Info) -> Maybe (b, Info))
-> (Info -> Maybe (a, Info)) -> Info -> Maybe (b, Info)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Info -> Maybe (a, Info)
g

maybeGetInfo :: (Info -> Maybe (a,Info)) -> Info -> (Maybe a, Info)
maybeGetInfo :: (Info -> Maybe (a, Info)) -> Info -> (Maybe a, Info)
maybeGetInfo Info -> Maybe (a, Info)
f Info
i =
    case Info -> Maybe (a, Info)
f Info
i of
      Just (a
a,Info
i') -> (a -> Maybe a
forall a. a -> Maybe a
Just a
a, Info
i')
      Maybe (a, Info)
Nothing -> (Maybe a
forall a. Maybe a
Nothing,Info
i)

listGetInfo :: (Info -> Maybe (a,Info)) -> Info -> ([a], Info)
listGetInfo :: (Info -> Maybe (a, Info)) -> Info -> ([a], Info)
listGetInfo Info -> Maybe (a, Info)
f = [a] -> Info -> ([a], Info)
g []
  where
    g :: [a] -> Info -> ([a], Info)
g [a]
l Info
i = case Info -> Maybe (a, Info)
f Info
i of
              Just (a
a,Info
i') -> [a] -> Info -> ([a], Info)
g (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
l) Info
i'
              Maybe (a, Info)
Nothing -> ([a]
l,Info
i)

instance Printable Info where
  toDoc :: Info -> Doc
toDoc = [Doc] -> Doc
PP.vcat ([Doc] -> Doc) -> (Info -> [Doc]) -> Info -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (KeyValue -> Doc) -> [KeyValue] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map KeyValue -> Doc
forall a. Printable a => a -> Doc
toDoc ([KeyValue] -> [Doc]) -> (Info -> [KeyValue]) -> Info -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Info -> [KeyValue]
destInfo

instance Parsable Info where
  parser :: Parsec Text st Info
parser = ([KeyValue] -> Info)
-> ParsecT Text st Identity [KeyValue] -> Parsec Text st Info
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [KeyValue] -> Info
Info (ParsecT Text st Identity [KeyValue] -> Parsec Text st Info)
-> ParsecT Text st Identity [KeyValue] -> Parsec Text st Info
forall a b. (a -> b) -> a -> b
$ ParsecT Text st Identity KeyValue
-> ParsecT Text st Identity ()
-> ParsecT Text st Identity [KeyValue]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
Parsec.endBy ParsecT Text st Identity KeyValue
forall a st. Parsable a => Parsec Text st a
parser ParsecT Text st Identity ()
forall st. Parsec Text st ()
eolParser

class Informative a where
  toInfo :: a -> Info

  getInfo :: Info -> Maybe (a,Info)

  fromInfo :: Info -> Maybe a
  fromInfo Info
i = do
      (a
a,Info
i') <- Info -> Maybe (a, Info)
forall a. Informative a => Info -> Maybe (a, Info)
getInfo Info
i
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Info -> Bool
nullInfo Info
i'
      a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

instance Informative a => Informative [a] where
  toInfo :: [a] -> Info
toInfo = [Info] -> Info
concatInfo ([Info] -> Info) -> ([a] -> [Info]) -> [a] -> Info
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Info) -> [a] -> [Info]
forall a b. (a -> b) -> [a] -> [b]
map a -> Info
forall a. Informative a => a -> Info
toInfo

  getInfo :: Info -> Maybe ([a], Info)
getInfo = ([a], Info) -> Maybe ([a], Info)
forall a. a -> Maybe a
Just (([a], Info) -> Maybe ([a], Info))
-> (Info -> ([a], Info)) -> Info -> Maybe ([a], Info)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Info -> Maybe (a, Info)) -> Info -> ([a], Info)
forall a. (Info -> Maybe (a, Info)) -> Info -> ([a], Info)
listGetInfo Info -> Maybe (a, Info)
forall a. Informative a => Info -> Maybe (a, Info)
getInfo

instance (Informative a, Informative b) => Informative (a,b) where
  toInfo :: (a, b) -> Info
toInfo (a
a,b
b) = Info -> Info -> Info
appendInfo (a -> Info
forall a. Informative a => a -> Info
toInfo a
a) (b -> Info
forall a. Informative a => a -> Info
toInfo b
b)

  getInfo :: Info -> Maybe ((a, b), Info)
getInfo Info
i = do
      (a
a,Info
i') <- Info -> Maybe (a, Info)
forall a. Informative a => Info -> Maybe (a, Info)
getInfo Info
i
      (b
b,Info
i'') <- Info -> Maybe (b, Info)
forall a. Informative a => Info -> Maybe (a, Info)
getInfo Info
i'
      ((a, b), Info) -> Maybe ((a, b), Info)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a,b
b),Info
i'')

-------------------------------------------------------------------------------
-- Package files
-------------------------------------------------------------------------------

newtype File = File {File -> String
destFile :: FilePath}
  deriving (File -> File -> Bool
(File -> File -> Bool) -> (File -> File -> Bool) -> Eq File
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: File -> File -> Bool
$c/= :: File -> File -> Bool
== :: File -> File -> Bool
$c== :: File -> File -> Bool
Eq,Eq File
Eq File
-> (File -> File -> Ordering)
-> (File -> File -> Bool)
-> (File -> File -> Bool)
-> (File -> File -> Bool)
-> (File -> File -> Bool)
-> (File -> File -> File)
-> (File -> File -> File)
-> Ord File
File -> File -> Bool
File -> File -> Ordering
File -> File -> File
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: File -> File -> File
$cmin :: File -> File -> File
max :: File -> File -> File
$cmax :: File -> File -> File
>= :: File -> File -> Bool
$c>= :: File -> File -> Bool
> :: File -> File -> Bool
$c> :: File -> File -> Bool
<= :: File -> File -> Bool
$c<= :: File -> File -> Bool
< :: File -> File -> Bool
$c< :: File -> File -> Bool
compare :: File -> File -> Ordering
$ccompare :: File -> File -> Ordering
$cp1Ord :: Eq File
Ord,Int -> File -> ShowS
[File] -> ShowS
File -> String
(Int -> File -> ShowS)
-> (File -> String) -> ([File] -> ShowS) -> Show File
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [File] -> ShowS
$cshowList :: [File] -> ShowS
show :: File -> String
$cshow :: File -> String
showsPrec :: Int -> File -> ShowS
$cshowsPrec :: Int -> File -> ShowS
Show)

instance Printable File where
  toDoc :: File -> Doc
toDoc = Doc -> Doc
PP.doubleQuotes (Doc -> Doc) -> (File -> Doc) -> File -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
PP.text (String -> Doc) -> (File -> String) -> File -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. File -> String
destFile

instance Parsable File where
  parser :: Parsec Text st File
parser = do
      Char
_ <- Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'"'
      String
f <- ParsecT Text st Identity Char -> ParsecT Text st Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
Parsec.many (String -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
Parsec.noneOf String
"\"\n")
      Char
_ <- Char -> ParsecT Text st Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'"'
      File -> Parsec Text st File
forall (m :: * -> *) a. Monad m => a -> m a
return (File -> Parsec Text st File) -> File -> Parsec Text st File
forall a b. (a -> b) -> a -> b
$ String -> File
File String
f

-------------------------------------------------------------------------------
-- Interpretations
-------------------------------------------------------------------------------

data Interpretation =
    Interpret Interpret.Rename
  | Interpretation File
  deriving (Interpretation -> Interpretation -> Bool
(Interpretation -> Interpretation -> Bool)
-> (Interpretation -> Interpretation -> Bool) -> Eq Interpretation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Interpretation -> Interpretation -> Bool
$c/= :: Interpretation -> Interpretation -> Bool
== :: Interpretation -> Interpretation -> Bool
$c== :: Interpretation -> Interpretation -> Bool
Eq,Eq Interpretation
Eq Interpretation
-> (Interpretation -> Interpretation -> Ordering)
-> (Interpretation -> Interpretation -> Bool)
-> (Interpretation -> Interpretation -> Bool)
-> (Interpretation -> Interpretation -> Bool)
-> (Interpretation -> Interpretation -> Bool)
-> (Interpretation -> Interpretation -> Interpretation)
-> (Interpretation -> Interpretation -> Interpretation)
-> Ord Interpretation
Interpretation -> Interpretation -> Bool
Interpretation -> Interpretation -> Ordering
Interpretation -> Interpretation -> Interpretation
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Interpretation -> Interpretation -> Interpretation
$cmin :: Interpretation -> Interpretation -> Interpretation
max :: Interpretation -> Interpretation -> Interpretation
$cmax :: Interpretation -> Interpretation -> Interpretation
>= :: Interpretation -> Interpretation -> Bool
$c>= :: Interpretation -> Interpretation -> Bool
> :: Interpretation -> Interpretation -> Bool
$c> :: Interpretation -> Interpretation -> Bool
<= :: Interpretation -> Interpretation -> Bool
$c<= :: Interpretation -> Interpretation -> Bool
< :: Interpretation -> Interpretation -> Bool
$c< :: Interpretation -> Interpretation -> Bool
compare :: Interpretation -> Interpretation -> Ordering
$ccompare :: Interpretation -> Interpretation -> Ordering
$cp1Ord :: Eq Interpretation
Ord,Int -> Interpretation -> ShowS
[Interpretation] -> ShowS
Interpretation -> String
(Int -> Interpretation -> ShowS)
-> (Interpretation -> String)
-> ([Interpretation] -> ShowS)
-> Show Interpretation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Interpretation] -> ShowS
$cshowList :: [Interpretation] -> ShowS
show :: Interpretation -> String
$cshow :: Interpretation -> String
showsPrec :: Int -> Interpretation -> ShowS
$cshowsPrec :: Int -> Interpretation -> ShowS
Show)

instance Informative Interpretation where
  toInfo :: Interpretation -> Info
toInfo (Interpret Rename
i) = [KeyValue] -> Info
Info [Name -> Rename -> KeyValue
forall a. Printable a => Name -> a -> KeyValue
printKeyValue (String -> Name
Name String
"interpret") Rename
i]
  toInfo (Interpretation File
f) = [KeyValue] -> Info
Info [Name -> File -> KeyValue
forall a. Printable a => Name -> a -> KeyValue
printKeyValue (String -> Name
Name String
"interpretation") File
f]

  getInfo :: Info -> Maybe (Interpretation, Info)
getInfo = [Info -> Maybe (Interpretation, Info)]
-> Info -> Maybe (Interpretation, Info)
forall a. [Info -> Maybe (a, Info)] -> Info -> Maybe (a, Info)
firstGetInfo [Info -> Maybe (Interpretation, Info)
getInterpret,Info -> Maybe (Interpretation, Info)
getInterpretation]
    where
      getInterpret :: Info -> Maybe (Interpretation, Info)
getInterpret =
        (Rename -> Interpretation)
-> (Info -> Maybe (Rename, Info))
-> Info
-> Maybe (Interpretation, Info)
forall a b.
(a -> b) -> (Info -> Maybe (a, Info)) -> Info -> Maybe (b, Info)
mapGetInfo Rename -> Interpretation
Interpret
          ((KeyValue -> Maybe Rename) -> Info -> Maybe (Rename, Info)
forall a. (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo (Name -> KeyValue -> Maybe Rename
forall a. Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue (String -> Name
Name String
"interpret")))

      getInterpretation :: Info -> Maybe (Interpretation, Info)
getInterpretation =
        (File -> Interpretation)
-> (Info -> Maybe (File, Info))
-> Info
-> Maybe (Interpretation, Info)
forall a b.
(a -> b) -> (Info -> Maybe (a, Info)) -> Info -> Maybe (b, Info)
mapGetInfo File -> Interpretation
Interpretation
          ((KeyValue -> Maybe File) -> Info -> Maybe (File, Info)
forall a. (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo (Name -> KeyValue -> Maybe File
forall a. Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue (String -> Name
Name String
"interpretation")))

readInterpretation :: FilePath -> [Interpretation] -> IO Interpret
readInterpretation :: String -> [Interpretation] -> IO Interpret
readInterpretation String
dir [Interpretation]
ints = do
    [Renames]
rs <- (Interpretation -> IO Renames) -> [Interpretation] -> IO [Renames]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Interpretation -> IO Renames
readRen [Interpretation]
ints
    Interpret -> IO Interpret
forall (m :: * -> *) a. Monad m => a -> m a
return (Interpret -> IO Interpret) -> Interpret -> IO Interpret
forall a b. (a -> b) -> a -> b
$ Renames -> Interpret
Interpret.fromRenamesUnsafe ([Renames] -> Renames
Interpret.concatRenames [Renames]
rs)
  where
    readRen :: Interpretation -> IO Renames
readRen (Interpret Rename
r) = Renames -> IO Renames
forall (m :: * -> *) a. Monad m => a -> m a
return (Renames -> IO Renames) -> Renames -> IO Renames
forall a b. (a -> b) -> a -> b
$ [Rename] -> Renames
Interpret.Renames [Rename
r]
    readRen (Interpretation File
f) = String -> IO Renames
forall a. Parsable a => String -> IO a
fromTextFile (String
dir String -> ShowS
</> File -> String
destFile File
f)

-------------------------------------------------------------------------------
-- Theory blocks
-------------------------------------------------------------------------------

data Operation =
    Article File
  | Include {Operation -> NameVersion
package :: NameVersion, Operation -> Maybe String
checksum :: Maybe String}
  | Union
  deriving (Operation -> Operation -> Bool
(Operation -> Operation -> Bool)
-> (Operation -> Operation -> Bool) -> Eq Operation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Operation -> Operation -> Bool
$c/= :: Operation -> Operation -> Bool
== :: Operation -> Operation -> Bool
$c== :: Operation -> Operation -> Bool
Eq,Eq Operation
Eq Operation
-> (Operation -> Operation -> Ordering)
-> (Operation -> Operation -> Bool)
-> (Operation -> Operation -> Bool)
-> (Operation -> Operation -> Bool)
-> (Operation -> Operation -> Bool)
-> (Operation -> Operation -> Operation)
-> (Operation -> Operation -> Operation)
-> Ord Operation
Operation -> Operation -> Bool
Operation -> Operation -> Ordering
Operation -> Operation -> Operation
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Operation -> Operation -> Operation
$cmin :: Operation -> Operation -> Operation
max :: Operation -> Operation -> Operation
$cmax :: Operation -> Operation -> Operation
>= :: Operation -> Operation -> Bool
$c>= :: Operation -> Operation -> Bool
> :: Operation -> Operation -> Bool
$c> :: Operation -> Operation -> Bool
<= :: Operation -> Operation -> Bool
$c<= :: Operation -> Operation -> Bool
< :: Operation -> Operation -> Bool
$c< :: Operation -> Operation -> Bool
compare :: Operation -> Operation -> Ordering
$ccompare :: Operation -> Operation -> Ordering
$cp1Ord :: Eq Operation
Ord,Int -> Operation -> ShowS
[Operation] -> ShowS
Operation -> String
(Int -> Operation -> ShowS)
-> (Operation -> String)
-> ([Operation] -> ShowS)
-> Show Operation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Operation] -> ShowS
$cshowList :: [Operation] -> ShowS
show :: Operation -> String
$cshow :: Operation -> String
showsPrec :: Int -> Operation -> ShowS
$cshowsPrec :: Int -> Operation -> ShowS
Show)

data Block =
    Block
      {Block -> Name
block :: Name,
       Block -> [Name]
imports :: [Name],
       Block -> [Interpretation]
interpret :: [Interpretation],
       Block -> Operation
operation :: Operation}
  deriving (Block -> Block -> Bool
(Block -> Block -> Bool) -> (Block -> Block -> Bool) -> Eq Block
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Block -> Block -> Bool
$c/= :: Block -> Block -> Bool
== :: Block -> Block -> Bool
$c== :: Block -> Block -> Bool
Eq,Eq Block
Eq Block
-> (Block -> Block -> Ordering)
-> (Block -> Block -> Bool)
-> (Block -> Block -> Bool)
-> (Block -> Block -> Bool)
-> (Block -> Block -> Bool)
-> (Block -> Block -> Block)
-> (Block -> Block -> Block)
-> Ord Block
Block -> Block -> Bool
Block -> Block -> Ordering
Block -> Block -> Block
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Block -> Block -> Block
$cmin :: Block -> Block -> Block
max :: Block -> Block -> Block
$cmax :: Block -> Block -> Block
>= :: Block -> Block -> Bool
$c>= :: Block -> Block -> Bool
> :: Block -> Block -> Bool
$c> :: Block -> Block -> Bool
<= :: Block -> Block -> Bool
$c<= :: Block -> Block -> Bool
< :: Block -> Block -> Bool
$c< :: Block -> Block -> Bool
compare :: Block -> Block -> Ordering
$ccompare :: Block -> Block -> Ordering
$cp1Ord :: Eq Block
Ord,Int -> Block -> ShowS
[Block] -> ShowS
Block -> String
(Int -> Block -> ShowS)
-> (Block -> String) -> ([Block] -> ShowS) -> Show Block
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Block] -> ShowS
$cshowList :: [Block] -> ShowS
show :: Block -> String
$cshow :: Block -> String
showsPrec :: Int -> Block -> ShowS
$cshowsPrec :: Int -> Block -> ShowS
Show)

instance Informative Operation where
  toInfo :: Operation -> Info
toInfo (Article File
f) = [KeyValue] -> Info
Info [Name -> File -> KeyValue
forall a. Printable a => Name -> a -> KeyValue
printKeyValue (String -> Name
Name String
"article") File
f]
  toInfo (Include NameVersion
p Maybe String
c) = [KeyValue] -> Info
Info (KeyValue
pv KeyValue -> [KeyValue] -> [KeyValue]
forall a. a -> [a] -> [a]
: [KeyValue]
cv)
    where
      pv :: KeyValue
pv = Name -> NameVersion -> KeyValue
forall a. Printable a => Name -> a -> KeyValue
printKeyValue (String -> Name
Name String
"package") NameVersion
p
      cv :: [KeyValue]
cv = case Maybe String
c of
             Just String
s -> [Name -> String -> KeyValue
KeyValue (String -> Name
Name String
"checksum") String
s]
             Maybe String
Nothing -> []
  toInfo Operation
Union = [KeyValue] -> Info
Info []

  getInfo :: Info -> Maybe (Operation, Info)
getInfo =
      [Info -> Maybe (Operation, Info)]
-> Info -> Maybe (Operation, Info)
forall a. [Info -> Maybe (a, Info)] -> Info -> Maybe (a, Info)
firstGetInfo [Info -> Maybe (Operation, Info)
getArticle,Info -> Maybe (Operation, Info)
getInclude,Info -> Maybe (Operation, Info)
forall b. b -> Maybe (Operation, b)
getUnion]
    where
      getArticle :: Info -> Maybe (Operation, Info)
getArticle = (File -> Operation)
-> (Info -> Maybe (File, Info)) -> Info -> Maybe (Operation, Info)
forall a b.
(a -> b) -> (Info -> Maybe (a, Info)) -> Info -> Maybe (b, Info)
mapGetInfo File -> Operation
Article Info -> Maybe (File, Info)
getArticleFile

      getInclude :: Info -> Maybe (Operation, Info)
getInclude Info
i = do
        (NameVersion
p,Info
i') <- Info -> Maybe (NameVersion, Info)
getPackage Info
i
        let (Maybe String
c,Info
i'') = (Info -> Maybe (String, Info)) -> Info -> (Maybe String, Info)
forall a. (Info -> Maybe (a, Info)) -> Info -> (Maybe a, Info)
maybeGetInfo Info -> Maybe (String, Info)
getChecksum Info
i'
        (Operation, Info) -> Maybe (Operation, Info)
forall (m :: * -> *) a. Monad m => a -> m a
return (NameVersion -> Maybe String -> Operation
Include NameVersion
p Maybe String
c, Info
i'')

      getUnion :: b -> Maybe (Operation, b)
getUnion b
i = (Operation, b) -> Maybe (Operation, b)
forall a. a -> Maybe a
Just (Operation
Union,b
i)

      getArticleFile :: Info -> Maybe (File, Info)
getArticleFile = (KeyValue -> Maybe File) -> Info -> Maybe (File, Info)
forall a. (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo (Name -> KeyValue -> Maybe File
forall a. Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue (String -> Name
Name String
"article"))
      getPackage :: Info -> Maybe (NameVersion, Info)
getPackage = (KeyValue -> Maybe NameVersion)
-> Info -> Maybe (NameVersion, Info)
forall a. (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo (Name -> KeyValue -> Maybe NameVersion
forall a. Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue (String -> Name
Name String
"package"))
      getChecksum :: Info -> Maybe (String, Info)
getChecksum = (KeyValue -> Maybe String) -> Info -> Maybe (String, Info)
forall a. (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo (Name -> KeyValue -> Maybe String
matchKeyValue (String -> Name
Name String
"checksum"))

mkBlock :: Name -> Info -> Maybe Block
mkBlock :: Name -> Info -> Maybe Block
mkBlock Name
n Info
info = do
    let ([Name]
imp,Info
info') = (Info -> Maybe (Name, Info)) -> Info -> ([Name], Info)
forall a. (Info -> Maybe (a, Info)) -> Info -> ([a], Info)
listGetInfo Info -> Maybe (Name, Info)
getImport Info
info
    ([Interpretation]
int,Operation
op) <- Info -> Maybe ([Interpretation], Operation)
forall a. Informative a => Info -> Maybe a
fromInfo Info
info'
    Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Operation
op Operation -> Operation -> Bool
forall a. Eq a => a -> a -> Bool
/= Operation
Union Bool -> Bool -> Bool
|| [Interpretation] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Interpretation]
int)
    Block -> Maybe Block
forall (m :: * -> *) a. Monad m => a -> m a
return (Block -> Maybe Block) -> Block -> Maybe Block
forall a b. (a -> b) -> a -> b
$ Name -> [Name] -> [Interpretation] -> Operation -> Block
Block Name
n [Name]
imp [Interpretation]
int Operation
op
  where
    getImport :: Info -> Maybe (Name, Info)
getImport = (KeyValue -> Maybe Name) -> Info -> Maybe (Name, Info)
forall a. (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo (Name -> KeyValue -> Maybe Name
forall a. Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue (String -> Name
Name String
"import"))

destBlock :: Block -> (Name,Info)
destBlock :: Block -> (Name, Info)
destBlock (Block Name
n [Name]
imp [Interpretation]
int Operation
op) =
    (Name
n, Info -> Info -> Info
appendInfo Info
impInfo (([Interpretation], Operation) -> Info
forall a. Informative a => a -> Info
toInfo ([Interpretation]
int,Operation
op)))
  where
    impInfo :: Info
impInfo = [KeyValue] -> Info
Info ((Name -> KeyValue) -> [Name] -> [KeyValue]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Name -> KeyValue
forall a. Printable a => Name -> a -> KeyValue
printKeyValue (String -> Name
Name String
"import")) [Name]
imp)

instance Printable Block where
  toDoc :: Block -> Doc
toDoc Block
b =
      (Name -> Doc
forall a. Printable a => a -> Doc
toDoc Name
n Doc -> Doc -> Doc
<+> Doc
PP.lbrace) Doc -> Doc -> Doc
$+$
      Int -> Doc -> Doc
PP.nest Int
2 (Info -> Doc
forall a. Printable a => a -> Doc
toDoc Info
i) Doc -> Doc -> Doc
$+$
      Doc
PP.rbrace
    where
      (Name
n,Info
i) = Block -> (Name, Info)
destBlock Block
b

instance Parsable Block where
  parser :: Parsec Text st Block
parser = do
      Name
n <- ParsecT Text st Identity Name
forall st. Parsec Text st Name
opener
      Info
i <- Parsec Text st Info
forall a st. Parsable a => Parsec Text st a
parser
      ParsecT Text st Identity ()
forall st. Parsec Text st ()
closer
      case Name -> Info -> Maybe Block
mkBlock Name
n Info
i of
        Just Block
b -> Block -> Parsec Text st Block
forall (m :: * -> *) a. Monad m => a -> m a
return Block
b
        Maybe Block
Nothing -> String -> Parsec Text st Block
forall s u (m :: * -> *) a. String -> ParsecT s u m a
Parsec.parserFail String
"couldn't parse block"
    where
      opener :: ParsecT Text u Identity Name
opener = do
        ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text u Identity ()
forall st. Parsec Text st ()
spaceParser
        Name
n <- ParsecT Text u Identity Name
forall a st. Parsable a => Parsec Text st a
parser
        ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text u Identity ()
forall st. Parsec Text st ()
spaceParser
        Char
_ <- Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'{'
        ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text u Identity ()
forall st. Parsec Text st ()
spaceParser
        ParsecT Text u Identity ()
forall st. Parsec Text st ()
eolParser
        Name -> ParsecT Text u Identity Name
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n

      closer :: ParsecT Text u Identity ()
closer = do
        ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text u Identity ()
forall st. Parsec Text st ()
spaceParser
        Char
_ <- Char -> ParsecT Text u Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
Parsec.char Char
'}'
        ParsecT Text u Identity () -> ParsecT Text u Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text u Identity ()
forall st. Parsec Text st ()
spaceParser

-------------------------------------------------------------------------------
-- Packages
-------------------------------------------------------------------------------

data Package =
    Package
      {Package -> Info
information :: Info,
       Package -> [Block]
source :: [Block]}
  deriving (Package -> Package -> Bool
(Package -> Package -> Bool)
-> (Package -> Package -> Bool) -> Eq Package
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Package -> Package -> Bool
$c/= :: Package -> Package -> Bool
== :: Package -> Package -> Bool
$c== :: Package -> Package -> Bool
Eq,Eq Package
Eq Package
-> (Package -> Package -> Ordering)
-> (Package -> Package -> Bool)
-> (Package -> Package -> Bool)
-> (Package -> Package -> Bool)
-> (Package -> Package -> Bool)
-> (Package -> Package -> Package)
-> (Package -> Package -> Package)
-> Ord Package
Package -> Package -> Bool
Package -> Package -> Ordering
Package -> Package -> Package
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Package -> Package -> Package
$cmin :: Package -> Package -> Package
max :: Package -> Package -> Package
$cmax :: Package -> Package -> Package
>= :: Package -> Package -> Bool
$c>= :: Package -> Package -> Bool
> :: Package -> Package -> Bool
$c> :: Package -> Package -> Bool
<= :: Package -> Package -> Bool
$c<= :: Package -> Package -> Bool
< :: Package -> Package -> Bool
$c< :: Package -> Package -> Bool
compare :: Package -> Package -> Ordering
$ccompare :: Package -> Package -> Ordering
$cp1Ord :: Eq Package
Ord,Int -> Package -> ShowS
[Package] -> ShowS
Package -> String
(Int -> Package -> ShowS)
-> (Package -> String) -> ([Package] -> ShowS) -> Show Package
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Package] -> ShowS
$cshowList :: [Package] -> ShowS
show :: Package -> String
$cshow :: Package -> String
showsPrec :: Int -> Package -> ShowS
$cshowsPrec :: Int -> Package -> ShowS
Show)

instance Printable Package where
  toDoc :: Package -> Doc
toDoc (Package Info
i [Block]
bs) =
      [Doc] -> Doc
PP.vcat (Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
List.intersperse (String -> Doc
PP.text String
"") (Info -> Doc
forall a. Printable a => a -> Doc
toDoc Info
i Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Block -> Doc) -> [Block] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Block -> Doc
forall a. Printable a => a -> Doc
toDoc [Block]
bs))

instance Parsable Package where
  parser :: Parsec Text st Package
parser = do
    ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text st Identity ()
forall st. Parsec Text st ()
eolParser
    Info
i <- Parsec Text st Info
forall a st. Parsable a => Parsec Text st a
parser
    ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany ParsecT Text st Identity ()
forall st. Parsec Text st ()
eolParser
    [Block]
bs <- ParsecT Text st Identity Block
-> ParsecT Text st Identity () -> ParsecT Text st Identity [Block]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
Parsec.sepEndBy ParsecT Text st Identity Block
forall a st. Parsable a => Parsec Text st a
parser (ParsecT Text st Identity () -> ParsecT Text st Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
Parsec.skipMany1 ParsecT Text st Identity ()
forall st. Parsec Text st ()
eolParser)
    Package -> Parsec Text st Package
forall (m :: * -> *) a. Monad m => a -> m a
return (Package -> Parsec Text st Package)
-> Package -> Parsec Text st Package
forall a b. (a -> b) -> a -> b
$ Info -> [Block] -> Package
Package Info
i [Block]
bs

requires :: Package -> [Name]
requires :: Package -> [Name]
requires = ([Name], Info) -> [Name]
forall a b. (a, b) -> a
fst (([Name], Info) -> [Name])
-> (Package -> ([Name], Info)) -> Package -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Info -> Maybe (Name, Info)) -> Info -> ([Name], Info)
forall a. (Info -> Maybe (a, Info)) -> Info -> ([a], Info)
listGetInfo Info -> Maybe (Name, Info)
getRequires (Info -> ([Name], Info))
-> (Package -> Info) -> Package -> ([Name], Info)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Package -> Info
information
  where
    getRequires :: Info -> Maybe (Name, Info)
getRequires = (KeyValue -> Maybe Name) -> Info -> Maybe (Name, Info)
forall a. (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)
firstInfo (Name -> KeyValue -> Maybe Name
forall a. Parsable a => Name -> KeyValue -> Maybe a
parseKeyValue (String -> Name
Name String
"requires"))

-------------------------------------------------------------------------------
-- Interface to the OpenTheory package repository
-------------------------------------------------------------------------------

packageFile :: FilePath -> Name -> FilePath
packageFile :: String -> Name -> String
packageFile String
d (Name String
n) = String
d String -> ShowS
</> String
n String -> ShowS
<.> String
"thy"

opentheory :: [String] -> IO String
opentheory :: [String] -> IO String
opentheory [String]
args = String -> [String] -> String -> IO String
System.Process.readProcess String
"opentheory" [String]
args []

opentheoryDirectory :: String -> IO FilePath
opentheoryDirectory :: String -> IO String
opentheoryDirectory String
s = do
    String
dir <- [String] -> IO String
opentheory [String
"info",String
"--directory",String
s]
    String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Char -> Bool
Char.isSpace String
dir

directory :: Name -> IO FilePath
directory :: Name -> IO String
directory = String -> IO String
opentheoryDirectory (String -> IO String) -> (Name -> String) -> Name -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
forall a. Printable a => a -> String
toString

directoryVersion :: NameVersion -> IO FilePath
directoryVersion :: NameVersion -> IO String
directoryVersion = String -> IO String
opentheoryDirectory (String -> IO String)
-> (NameVersion -> String) -> NameVersion -> IO String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameVersion -> String
forall a. Printable a => a -> String
toString

-------------------------------------------------------------------------------
-- Dependencies between theory blocks
-------------------------------------------------------------------------------

newtype Blocks = Blocks {Blocks -> [Block]
destBlocks :: [Block]}
  deriving (Blocks -> Blocks -> Bool
(Blocks -> Blocks -> Bool)
-> (Blocks -> Blocks -> Bool) -> Eq Blocks
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Blocks -> Blocks -> Bool
$c/= :: Blocks -> Blocks -> Bool
== :: Blocks -> Blocks -> Bool
$c== :: Blocks -> Blocks -> Bool
Eq,Eq Blocks
Eq Blocks
-> (Blocks -> Blocks -> Ordering)
-> (Blocks -> Blocks -> Bool)
-> (Blocks -> Blocks -> Bool)
-> (Blocks -> Blocks -> Bool)
-> (Blocks -> Blocks -> Bool)
-> (Blocks -> Blocks -> Blocks)
-> (Blocks -> Blocks -> Blocks)
-> Ord Blocks
Blocks -> Blocks -> Bool
Blocks -> Blocks -> Ordering
Blocks -> Blocks -> Blocks
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Blocks -> Blocks -> Blocks
$cmin :: Blocks -> Blocks -> Blocks
max :: Blocks -> Blocks -> Blocks
$cmax :: Blocks -> Blocks -> Blocks
>= :: Blocks -> Blocks -> Bool
$c>= :: Blocks -> Blocks -> Bool
> :: Blocks -> Blocks -> Bool
$c> :: Blocks -> Blocks -> Bool
<= :: Blocks -> Blocks -> Bool
$c<= :: Blocks -> Blocks -> Bool
< :: Blocks -> Blocks -> Bool
$c< :: Blocks -> Blocks -> Bool
compare :: Blocks -> Blocks -> Ordering
$ccompare :: Blocks -> Blocks -> Ordering
$cp1Ord :: Eq Blocks
Ord,Int -> Blocks -> ShowS
[Blocks] -> ShowS
Blocks -> String
(Int -> Blocks -> ShowS)
-> (Blocks -> String) -> ([Blocks] -> ShowS) -> Show Blocks
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Blocks] -> ShowS
$cshowList :: [Blocks] -> ShowS
show :: Blocks -> String
$cshow :: Blocks -> String
showsPrec :: Int -> Blocks -> ShowS
$cshowsPrec :: Int -> Blocks -> ShowS
Show)

mkBlocks :: [Block] -> Blocks
mkBlocks :: [Block] -> Blocks
mkBlocks [Block]
bl = [Block] -> Blocks
Blocks ([Name] -> [Block] -> Name -> [Block]
check [] [] (String -> Name
Name String
"main"))
  where
    check :: [Name] -> [Block] -> Name -> [Block]
check [Name]
st [Block]
bs Name
n =
        if (Block -> Bool) -> [Block] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) Name
n (Name -> Bool) -> (Block -> Name) -> Block -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> Name
block) [Block]
bs then [Block]
bs
        else if Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Name
n [Name]
st then [Name] -> [Block] -> Block -> [Block]
add (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
st) [Block]
bs (Name -> Block
get Name
n)
        else String -> [Block]
forall a. HasCallStack => String -> a
error (String -> [Block]) -> String -> [Block]
forall a b. (a -> b) -> a -> b
$ String
"import cycle including theory block " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Printable a => a -> String
toString Name
n

    add :: [Name] -> [Block] -> Block -> [Block]
add [Name]
st [Block]
bs Block
b = Block
b Block -> [Block] -> [Block]
forall a. a -> [a] -> [a]
: ([Block] -> Name -> [Block]) -> [Block] -> [Name] -> [Block]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([Name] -> [Block] -> Name -> [Block]
check [Name]
st) [Block]
bs (Block -> [Name]
imports Block
b)

    get :: Name -> Block
get Name
n =
        case (Block -> Bool) -> [Block] -> [Block]
forall a. (a -> Bool) -> [a] -> [a]
filter (Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
(==) Name
n (Name -> Bool) -> (Block -> Name) -> Block -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block -> Name
block) [Block]
bl of
          [] -> String -> Block
forall a. HasCallStack => String -> a
error (String -> Block) -> String -> Block
forall a b. (a -> b) -> a -> b
$ String
"missing theory block " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Printable a => a -> String
toString Name
n
          [Block
b] -> Block
b
          Block
_ : Block
_ : [Block]
_ -> String -> Block
forall a. HasCallStack => String -> a
error (String -> Block) -> String -> Block
forall a b. (a -> b) -> a -> b
$ String
"multiple theory blocks named " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Printable a => a -> String
toString Name
n

-------------------------------------------------------------------------------
-- Reading one package
-------------------------------------------------------------------------------

readVersion :: Theory -> Interpret -> NameVersion -> IO Theory
readVersion :: Theory -> Interpret -> NameVersion -> IO Theory
readVersion Theory
thy Interpret
int NameVersion
nv = do
    String
dir <- NameVersion -> IO String
directoryVersion NameVersion
nv
    Theory -> Interpret -> String -> IO Theory
readPackageFile Theory
thy Interpret
int (String -> Name -> String
packageFile String
dir (NameVersion -> Name
name NameVersion
nv))

readPackageFile :: Theory -> Interpret -> FilePath -> IO Theory
readPackageFile :: Theory -> Interpret -> String -> IO Theory
readPackageFile Theory
thy Interpret
int String
file = do
    Package
pkg <- String -> IO Package
forall a. Parsable a => String -> IO a
fromTextFile String
file
    Theory -> Interpret -> String -> Package -> IO Theory
readPackage Theory
thy Interpret
int (ShowS
takeDirectory String
file) Package
pkg

readPackage :: Theory -> Interpret -> FilePath -> Package -> IO Theory
readPackage :: Theory -> Interpret -> String -> Package -> IO Theory
readPackage Theory
thy Interpret
int String
dir Package
pkg = Theory -> Interpret -> String -> Blocks -> IO Theory
readBlocks Theory
thy Interpret
int String
dir ([Block] -> Blocks
mkBlocks (Package -> [Block]
source Package
pkg))

readBlocks :: Theory -> Interpret -> FilePath -> Blocks -> IO Theory
readBlocks :: Theory -> Interpret -> String -> Blocks -> IO Theory
readBlocks Theory
thy Interpret
int String
dir (Blocks [Block]
bs) = do
    Map Name (MVar Theory)
vs <- (Map Name (MVar Theory) -> Block -> IO (Map Name (MVar Theory)))
-> Map Name (MVar Theory) -> [Block] -> IO (Map Name (MVar Theory))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Name (MVar Theory) -> Block -> IO (Map Name (MVar Theory))
forall a. Map Name (MVar a) -> Block -> IO (Map Name (MVar a))
initT Map Name (MVar Theory)
forall k a. Map k a
Map.empty [Block]
bs
    (Block -> IO ThreadId) -> [Block] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> (Block -> IO ()) -> Block -> IO ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (MVar Theory) -> Block -> IO ()
mkT Map Name (MVar Theory)
vs) [Block]
bs
    MVar Theory -> IO Theory
forall a. MVar a -> IO a
readMVar (Map Name (MVar Theory) -> Name -> MVar Theory
forall a p. (Ord a, Show a) => Map a p -> a -> p
getT Map Name (MVar Theory)
vs (Block -> Name
block ([Block] -> Block
forall a. [a] -> a
head [Block]
bs)))
  where
    mkT :: Map Name (MVar Theory) -> Block -> IO ()
mkT Map Name (MVar Theory)
vs Block
b = do
        [Theory]
ts <- (Name -> IO Theory) -> [Name] -> IO [Theory]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MVar Theory -> IO Theory
forall a. MVar a -> IO a
readMVar (MVar Theory -> IO Theory)
-> (Name -> MVar Theory) -> Name -> IO Theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (MVar Theory) -> Name -> MVar Theory
forall a p. (Ord a, Show a) => Map a p -> a -> p
getT Map Name (MVar Theory)
vs) (Block -> [Name]
imports Block
b)
        Theory
t <- Theory -> Interpret -> String -> [Theory] -> Block -> IO Theory
readBlock Theory
thy Interpret
int String
dir [Theory]
ts Block
b
        MVar Theory -> Theory -> IO ()
forall a. MVar a -> a -> IO ()
putMVar (Map Name (MVar Theory) -> Name -> MVar Theory
forall a p. (Ord a, Show a) => Map a p -> a -> p
getT Map Name (MVar Theory)
vs (Block -> Name
block Block
b)) Theory
t

    getT :: Map a p -> a -> p
getT Map a p
vs a
n =
        case a -> Map a p -> Maybe p
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
n Map a p
vs of
          Just p
v -> p
v
          Maybe p
Nothing -> String -> p
forall a. HasCallStack => String -> a
error (String -> p) -> String -> p
forall a b. (a -> b) -> a -> b
$ String
"bad theory block " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n

    initT :: Map Name (MVar a) -> Block -> IO (Map Name (MVar a))
initT Map Name (MVar a)
vs Block
b = do
        MVar a
v <- IO (MVar a)
forall a. IO (MVar a)
newEmptyMVar
        Map Name (MVar a) -> IO (Map Name (MVar a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Name (MVar a) -> IO (Map Name (MVar a)))
-> Map Name (MVar a) -> IO (Map Name (MVar a))
forall a b. (a -> b) -> a -> b
$ Name -> MVar a -> Map Name (MVar a) -> Map Name (MVar a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Block -> Name
block Block
b) MVar a
v Map Name (MVar a)
vs

readBlock :: Theory -> Interpret -> FilePath -> [Theory] -> Block -> IO Theory
readBlock :: Theory -> Interpret -> String -> [Theory] -> Block -> IO Theory
readBlock Theory
envThy Interpret
envInt String
dir [Theory]
impThys Block
b = do
    Interpret
blockInt <- String -> [Interpretation] -> IO Interpret
readInterpretation String
dir (Block -> [Interpretation]
interpret Block
b)
    let int :: Interpret
int = Interpret -> Interpret -> Interpret
Interpret.compose Interpret
blockInt Interpret
envInt
    case Block -> Operation
operation Block
b of
      Article File
f -> do
          Set Thm
ths <- Theory -> Interpret -> String -> IO (Set Thm)
readArticle Theory
thy Interpret
int (String
dir String -> ShowS
</> File -> String
destFile File
f)
          Theory -> IO Theory
forall (m :: * -> *) a. Monad m => a -> m a
return (Theory -> IO Theory) -> Theory -> IO Theory
forall a b. (a -> b) -> a -> b
$ Set Thm -> Theory
Theory.fromThmSet Set Thm
ths
      Include {package :: Operation -> NameVersion
package = NameVersion
nv} -> Theory -> Interpret -> NameVersion -> IO Theory
readVersion Theory
thy Interpret
int NameVersion
nv
      Operation
Union -> Theory -> IO Theory
forall (m :: * -> *) a. Monad m => a -> m a
return Theory
impThy
  where
    thy :: Theory
thy = Theory -> Theory -> Theory
Theory.union Theory
envThy Theory
impThy
    impThy :: Theory
impThy = [Theory] -> Theory
Theory.unionList [Theory]
impThys

-------------------------------------------------------------------------------
-- Dependencies between packages
-------------------------------------------------------------------------------

newtype Requires = Requires (Map Name ([Name],FilePath,Blocks))

emptyRequires :: Requires
emptyRequires :: Requires
emptyRequires = Map Name ([Name], String, Blocks) -> Requires
Requires Map Name ([Name], String, Blocks)
forall k a. Map k a
Map.empty

addRequires :: Requires -> Name -> IO Requires
addRequires :: Requires -> Name -> IO Requires
addRequires = Requires -> Name -> IO Requires
add
  where
    add :: Requires -> Name -> IO Requires
add (Requires Map Name ([Name], String, Blocks)
m) Name
n = (Map Name ([Name], String, Blocks) -> Requires)
-> IO (Map Name ([Name], String, Blocks)) -> IO Requires
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Map Name ([Name], String, Blocks) -> Requires
Requires (IO (Map Name ([Name], String, Blocks)) -> IO Requires)
-> IO (Map Name ([Name], String, Blocks)) -> IO Requires
forall a b. (a -> b) -> a -> b
$ [Name]
-> Map Name ([Name], String, Blocks)
-> Name
-> IO (Map Name ([Name], String, Blocks))
check [] Map Name ([Name], String, Blocks)
m Name
n

    check :: [Name]
-> Map Name ([Name], String, Blocks)
-> Name
-> IO (Map Name ([Name], String, Blocks))
check [Name]
st Map Name ([Name], String, Blocks)
m Name
n =
        if Name -> Map Name ([Name], String, Blocks) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Name
n Map Name ([Name], String, Blocks)
m then Map Name ([Name], String, Blocks)
-> IO (Map Name ([Name], String, Blocks))
forall (m :: * -> *) a. Monad m => a -> m a
return Map Name ([Name], String, Blocks)
m
        else if Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Name
n [Name]
st then [Name]
-> Map Name ([Name], String, Blocks)
-> Name
-> IO (Map Name ([Name], String, Blocks))
pkg (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
st) Map Name ([Name], String, Blocks)
m Name
n
        else String -> IO (Map Name ([Name], String, Blocks))
forall a. HasCallStack => String -> a
error (String -> IO (Map Name ([Name], String, Blocks)))
-> String -> IO (Map Name ([Name], String, Blocks))
forall a b. (a -> b) -> a -> b
$ String
"requires cycle including package " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Printable a => a -> String
toString Name
n

    pkg :: [Name]
-> Map Name ([Name], String, Blocks)
-> Name
-> IO (Map Name ([Name], String, Blocks))
pkg [Name]
st Map Name ([Name], String, Blocks)
m Name
n = do
        String
d <- Name -> IO String
directory Name
n
        Package
p <- String -> IO Package
forall a. Parsable a => String -> IO a
fromTextFile (String -> Name -> String
packageFile String
d Name
n)
        let r :: [Name]
r = Package -> [Name]
requires Package
p
        let s :: Blocks
s = [Block] -> Blocks
mkBlocks (Package -> [Block]
source Package
p)
        (Map Name ([Name], String, Blocks)
 -> Name -> IO (Map Name ([Name], String, Blocks)))
-> Map Name ([Name], String, Blocks)
-> [Name]
-> IO (Map Name ([Name], String, Blocks))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ([Name]
-> Map Name ([Name], String, Blocks)
-> Name
-> IO (Map Name ([Name], String, Blocks))
check [Name]
st) (Name
-> ([Name], String, Blocks)
-> Map Name ([Name], String, Blocks)
-> Map Name ([Name], String, Blocks)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
n ([Name]
r,String
d,Blocks
s) Map Name ([Name], String, Blocks)
m) [Name]
r

fromListRequires :: [Name] -> IO Requires
fromListRequires :: [Name] -> IO Requires
fromListRequires = (Requires -> Name -> IO Requires)
-> Requires -> [Name] -> IO Requires
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Requires -> Name -> IO Requires
addRequires Requires
emptyRequires

-------------------------------------------------------------------------------
-- Reading packages
-------------------------------------------------------------------------------

readList :: [Name] -> IO [Theory]
readList :: [Name] -> IO [Theory]
readList [Name]
ns = do
    [(Name, ([Name], String, Blocks))]
req <- IO [(Name, ([Name], String, Blocks))]
mkReq
    Map Name (MVar Theory)
vs <- (Map Name (MVar Theory)
 -> (Name, ([Name], String, Blocks)) -> IO (Map Name (MVar Theory)))
-> Map Name (MVar Theory)
-> [(Name, ([Name], String, Blocks))]
-> IO (Map Name (MVar Theory))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Map Name (MVar Theory)
-> (Name, ([Name], String, Blocks)) -> IO (Map Name (MVar Theory))
forall k a b.
Ord k =>
Map k (MVar a) -> (k, b) -> IO (Map k (MVar a))
initT Map Name (MVar Theory)
forall k a. Map k a
Map.empty [(Name, ([Name], String, Blocks))]
req
    ((Name, ([Name], String, Blocks)) -> IO ThreadId)
-> [(Name, ([Name], String, Blocks))] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId)
-> ((Name, ([Name], String, Blocks)) -> IO ())
-> (Name, ([Name], String, Blocks))
-> IO ThreadId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (MVar Theory) -> (Name, ([Name], String, Blocks)) -> IO ()
forall a.
(Ord a, Show a) =>
Map a (MVar Theory) -> (a, ([a], String, Blocks)) -> IO ()
mkT Map Name (MVar Theory)
vs) [(Name, ([Name], String, Blocks))]
req
    (Name -> IO Theory) -> [Name] -> IO [Theory]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MVar Theory -> IO Theory
forall a. MVar a -> IO a
readMVar (MVar Theory -> IO Theory)
-> (Name -> MVar Theory) -> Name -> IO Theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Name (MVar Theory) -> Name -> MVar Theory
forall a p. (Ord a, Show a) => Map a p -> a -> p
getT Map Name (MVar Theory)
vs) [Name]
ns
  where
    mkReq :: IO [(Name, ([Name], String, Blocks))]
mkReq = do
        Requires Map Name ([Name], String, Blocks)
m <- [Name] -> IO Requires
fromListRequires [Name]
ns
        [(Name, ([Name], String, Blocks))]
-> IO [(Name, ([Name], String, Blocks))]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, ([Name], String, Blocks))]
 -> IO [(Name, ([Name], String, Blocks))])
-> [(Name, ([Name], String, Blocks))]
-> IO [(Name, ([Name], String, Blocks))]
forall a b. (a -> b) -> a -> b
$ Map Name ([Name], String, Blocks)
-> [(Name, ([Name], String, Blocks))]
forall k a. Map k a -> [(k, a)]
Map.toList Map Name ([Name], String, Blocks)
m

    mkT :: Map a (MVar Theory) -> (a, ([a], String, Blocks)) -> IO ()
mkT Map a (MVar Theory)
vs (a
n,([a]
r,String
d,Blocks
s)) = do
        [Theory]
ts <- (a -> IO Theory) -> [a] -> IO [Theory]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (MVar Theory -> IO Theory
forall a. MVar a -> IO a
readMVar (MVar Theory -> IO Theory) -> (a -> MVar Theory) -> a -> IO Theory
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (MVar Theory) -> a -> MVar Theory
forall a p. (Ord a, Show a) => Map a p -> a -> p
getT Map a (MVar Theory)
vs) [a]
r
        let thy :: Theory
thy = [Theory] -> Theory
Theory.unionList (Theory
Theory.standard Theory -> [Theory] -> [Theory]
forall a. a -> [a] -> [a]
: [Theory]
ts)
        Theory
t <- Theory -> Interpret -> String -> Blocks -> IO Theory
readBlocks Theory
thy Interpret
Interpret.empty String
d Blocks
s
        MVar Theory -> Theory -> IO ()
forall a. MVar a -> a -> IO ()
putMVar (Map a (MVar Theory) -> a -> MVar Theory
forall a p. (Ord a, Show a) => Map a p -> a -> p
getT Map a (MVar Theory)
vs a
n) Theory
t

    getT :: Map a p -> a -> p
getT Map a p
vs a
n =
        case a -> Map a p -> Maybe p
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup a
n Map a p
vs of
          Just p
v -> p
v
          Maybe p
Nothing -> String -> p
forall a. HasCallStack => String -> a
error (String -> p) -> String -> p
forall a b. (a -> b) -> a -> b
$ String
"bad package " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n

    initT :: Map k (MVar a) -> (k, b) -> IO (Map k (MVar a))
initT Map k (MVar a)
vs (k
n,b
_) = do
        MVar a
v <- IO (MVar a)
forall a. IO (MVar a)
newEmptyMVar
        Map k (MVar a) -> IO (Map k (MVar a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Map k (MVar a) -> IO (Map k (MVar a)))
-> Map k (MVar a) -> IO (Map k (MVar a))
forall a b. (a -> b) -> a -> b
$ k -> MVar a -> Map k (MVar a) -> Map k (MVar a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
n MVar a
v Map k (MVar a)
vs