HOL.OpenTheory.Package

Documentation

newtype Name

Constructors

Name

Fields

• destName :: String

Instances

Eq Name

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Ord Name

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

Show Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

Parsable Name

Methods

parser :: Parsec Text st Name

fromText :: Text -> Maybe Name

fromString :: String -> Maybe Name

fromStringUnsafe :: String -> Name

fromTextFile :: FilePath -> IO Name

Printable Name

Methods

toDoc :: Name -> Doc

toStringWith :: Style -> Name -> String

toString :: Name -> String

newtype Version

Constructors

Version

Fields

• destVersion :: String

Instances

Eq Version

Methods

(==) :: Version -> Version -> Bool

(/=) :: Version -> Version -> Bool

Ord Version

Methods

compare :: Version -> Version -> Ordering

(<) :: Version -> Version -> Bool

(<=) :: Version -> Version -> Bool

(>) :: Version -> Version -> Bool

(>=) :: Version -> Version -> Bool

max :: Version -> Version -> Version

min :: Version -> Version -> Version

Show Version

Methods

showsPrec :: Int -> Version -> ShowS

show :: Version -> String

showList :: [Version] -> ShowS

Parsable Version

Methods

parser :: Parsec Text st Version

fromText :: Text -> Maybe Version

fromString :: String -> Maybe Version

fromStringUnsafe :: String -> Version

fromTextFile :: FilePath -> IO Version

Printable Version

Methods

toDoc :: Version -> Doc

toStringWith :: Style -> Version -> String

toString :: Version -> String

data NameVersion

Constructors

NameVersion

Fields

• name :: Name
• version :: Version

Instances

Eq NameVersion

Methods

(==) :: NameVersion -> NameVersion -> Bool

(/=) :: NameVersion -> NameVersion -> Bool

Ord NameVersion

Methods

compare :: NameVersion -> NameVersion -> Ordering

(<) :: NameVersion -> NameVersion -> Bool

(<=) :: NameVersion -> NameVersion -> Bool

(>) :: NameVersion -> NameVersion -> Bool

(>=) :: NameVersion -> NameVersion -> Bool

max :: NameVersion -> NameVersion -> NameVersion

min :: NameVersion -> NameVersion -> NameVersion

Show NameVersion

Methods

showsPrec :: Int -> NameVersion -> ShowS

show :: NameVersion -> String

showList :: [NameVersion] -> ShowS

Parsable NameVersion

Methods

parser :: Parsec Text st NameVersion

fromText :: Text -> Maybe NameVersion

fromString :: String -> Maybe NameVersion

fromStringUnsafe :: String -> NameVersion

fromTextFile :: FilePath -> IO NameVersion

Printable NameVersion

Methods

toDoc :: NameVersion -> Doc

toStringWith :: Style -> NameVersion -> String

toString :: NameVersion -> String

data KeyValue

Constructors

KeyValue Name String

Instances

Eq KeyValue

Methods

(==) :: KeyValue -> KeyValue -> Bool

(/=) :: KeyValue -> KeyValue -> Bool

Ord KeyValue

Methods

compare :: KeyValue -> KeyValue -> Ordering

(<) :: KeyValue -> KeyValue -> Bool

(<=) :: KeyValue -> KeyValue -> Bool

(>) :: KeyValue -> KeyValue -> Bool

(>=) :: KeyValue -> KeyValue -> Bool

max :: KeyValue -> KeyValue -> KeyValue

min :: KeyValue -> KeyValue -> KeyValue

Show KeyValue

Methods

showsPrec :: Int -> KeyValue -> ShowS

show :: KeyValue -> String

showList :: [KeyValue] -> ShowS

Parsable KeyValue

Methods

parser :: Parsec Text st KeyValue

fromText :: Text -> Maybe KeyValue

fromString :: String -> Maybe KeyValue

fromStringUnsafe :: String -> KeyValue

fromTextFile :: FilePath -> IO KeyValue

Printable KeyValue

Methods

toDoc :: KeyValue -> Doc

toStringWith :: Style -> KeyValue -> String

toString :: KeyValue -> String

printKeyValue :: Printable a => Name -> a -> KeyValue

matchKeyValue :: Name -> KeyValue -> Maybe String

parseKeyValue :: Parsable a => Name -> KeyValue -> Maybe a

newtype Info

Constructors

Info

Fields

• destInfo :: [KeyValue]

Instances

Eq Info

Methods

(==) :: Info -> Info -> Bool

(/=) :: Info -> Info -> Bool

Ord Info

Methods

compare :: Info -> Info -> Ordering

(<) :: Info -> Info -> Bool

(<=) :: Info -> Info -> Bool

(>) :: Info -> Info -> Bool

(>=) :: Info -> Info -> Bool

max :: Info -> Info -> Info

min :: Info -> Info -> Info

Show Info

Methods

showsPrec :: Int -> Info -> ShowS

show :: Info -> String

showList :: [Info] -> ShowS

Parsable Info

Methods

parser :: Parsec Text st Info

fromText :: Text -> Maybe Info

fromString :: String -> Maybe Info

fromStringUnsafe :: String -> Info

fromTextFile :: FilePath -> IO Info

Printable Info

Methods

toDoc :: Info -> Doc

toStringWith :: Style -> Info -> String

toString :: Info -> String

nullInfo :: Info -> Bool

appendInfo :: Info -> Info -> Info

concatInfo :: [Info] -> Info

firstInfo :: (KeyValue -> Maybe a) -> Info -> Maybe (a, Info)

firstGetInfo :: [Info -> Maybe (a, Info)] -> Info -> Maybe (a, Info)

mapGetInfo :: (a -> b) -> (Info -> Maybe (a, Info)) -> Info -> Maybe (b, Info)

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

listGetInfo :: (Info -> Maybe (a, Info)) -> Info -> ([a], Info)

class Informative a where

Minimal complete definition

toInfo, getInfo

Methods

toInfo :: a -> Info

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

fromInfo :: Info -> Maybe a

Instances

Informative Operation

Methods

toInfo :: Operation -> Info

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

fromInfo :: Info -> Maybe Operation

Informative Interpretation

Methods

toInfo :: Interpretation -> Info

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

fromInfo :: Info -> Maybe Interpretation

Informative a => Informative [a]

Methods

toInfo :: [a] -> Info

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

fromInfo :: Info -> Maybe [a]

(Informative a, Informative b) => Informative (a, b)

Methods

toInfo :: (a, b) -> Info

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

fromInfo :: Info -> Maybe (a, b)

newtype File

Constructors

File

Fields

• destFile :: FilePath

Instances

Eq File

Methods

(==) :: File -> File -> Bool

(/=) :: File -> File -> Bool

Ord File

Methods

compare :: File -> File -> Ordering

(<) :: File -> File -> Bool

(<=) :: File -> File -> Bool

(>) :: File -> File -> Bool

(>=) :: File -> File -> Bool

max :: File -> File -> File

min :: File -> File -> File

Show File

Methods

showsPrec :: Int -> File -> ShowS

show :: File -> String

showList :: [File] -> ShowS

Parsable File

Methods

parser :: Parsec Text st File

fromText :: Text -> Maybe File

fromString :: String -> Maybe File

fromStringUnsafe :: String -> File

fromTextFile :: FilePath -> IO File

Printable File

Methods

toDoc :: File -> Doc

toStringWith :: Style -> File -> String

toString :: File -> String

data Interpretation

Constructors

Interpret Rename

Interpretation File

Instances

Eq Interpretation

Methods

(==) :: Interpretation -> Interpretation -> Bool

(/=) :: Interpretation -> Interpretation -> Bool

Ord Interpretation

Methods

compare :: Interpretation -> Interpretation -> Ordering

(<) :: Interpretation -> Interpretation -> Bool

(<=) :: Interpretation -> Interpretation -> Bool

(>) :: Interpretation -> Interpretation -> Bool

(>=) :: Interpretation -> Interpretation -> Bool

max :: Interpretation -> Interpretation -> Interpretation

min :: Interpretation -> Interpretation -> Interpretation

Show Interpretation

Methods

showsPrec :: Int -> Interpretation -> ShowS

show :: Interpretation -> String

showList :: [Interpretation] -> ShowS

Informative Interpretation

Methods

toInfo :: Interpretation -> Info

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

fromInfo :: Info -> Maybe Interpretation

readInterpretation :: FilePath -> [Interpretation] -> IO Interpret

data Operation

Constructors

Article File

Include

Fields

• package :: NameVersion
• checksum :: Maybe String

Union

Instances

Eq Operation

Methods

(==) :: Operation -> Operation -> Bool

(/=) :: Operation -> Operation -> Bool

Ord Operation

Methods

compare :: Operation -> Operation -> Ordering

(<) :: Operation -> Operation -> Bool

(<=) :: Operation -> Operation -> Bool

(>) :: Operation -> Operation -> Bool

(>=) :: Operation -> Operation -> Bool

max :: Operation -> Operation -> Operation

min :: Operation -> Operation -> Operation

Show Operation

Methods

showsPrec :: Int -> Operation -> ShowS

show :: Operation -> String

showList :: [Operation] -> ShowS

Informative Operation

Methods

toInfo :: Operation -> Info

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

fromInfo :: Info -> Maybe Operation

data Block

Constructors

Block

Fields

• block :: Name
• imports :: [Name]
• interpret :: [Interpretation]
• operation :: Operation

Instances

Eq Block

Methods

(==) :: Block -> Block -> Bool

(/=) :: Block -> Block -> Bool

Ord Block

Methods

compare :: Block -> Block -> Ordering

(<) :: Block -> Block -> Bool

(<=) :: Block -> Block -> Bool

(>) :: Block -> Block -> Bool

(>=) :: Block -> Block -> Bool

max :: Block -> Block -> Block

min :: Block -> Block -> Block

Show Block

Methods

showsPrec :: Int -> Block -> ShowS

show :: Block -> String

showList :: [Block] -> ShowS

Parsable Block

Methods

parser :: Parsec Text st Block

fromText :: Text -> Maybe Block

fromString :: String -> Maybe Block

fromStringUnsafe :: String -> Block

fromTextFile :: FilePath -> IO Block

Printable Block

Methods

toDoc :: Block -> Doc

toStringWith :: Style -> Block -> String

toString :: Block -> String

mkBlock :: Name -> Info -> Maybe Block

destBlock :: Block -> (Name, Info)

data Package

Constructors

Package

Fields

• information :: Info
• source :: [Block]

Instances

Eq Package

Methods

(==) :: Package -> Package -> Bool

(/=) :: Package -> Package -> Bool

Ord Package

Methods

compare :: Package -> Package -> Ordering

(<) :: Package -> Package -> Bool

(<=) :: Package -> Package -> Bool

(>) :: Package -> Package -> Bool

(>=) :: Package -> Package -> Bool

max :: Package -> Package -> Package

min :: Package -> Package -> Package

Show Package

Methods

showsPrec :: Int -> Package -> ShowS

show :: Package -> String

showList :: [Package] -> ShowS

Parsable Package

Methods

parser :: Parsec Text st Package

fromText :: Text -> Maybe Package

fromString :: String -> Maybe Package

fromStringUnsafe :: String -> Package

fromTextFile :: FilePath -> IO Package

Printable Package

Methods

toDoc :: Package -> Doc

toStringWith :: Style -> Package -> String

toString :: Package -> String

requires :: Package -> [Name]

packageFile :: FilePath -> Name -> FilePath

opentheory :: [String] -> IO String

opentheoryDirectory :: String -> IO FilePath

directory :: Name -> IO FilePath

directoryVersion :: NameVersion -> IO FilePath

newtype Blocks

Constructors

Blocks

Fields

• destBlocks :: [Block]

Instances

Eq Blocks

Methods

(==) :: Blocks -> Blocks -> Bool

(/=) :: Blocks -> Blocks -> Bool

Ord Blocks

Methods

compare :: Blocks -> Blocks -> Ordering

(<) :: Blocks -> Blocks -> Bool

(<=) :: Blocks -> Blocks -> Bool

(>) :: Blocks -> Blocks -> Bool

(>=) :: Blocks -> Blocks -> Bool

max :: Blocks -> Blocks -> Blocks

min :: Blocks -> Blocks -> Blocks

Show Blocks

Methods

showsPrec :: Int -> Blocks -> ShowS

show :: Blocks -> String

showList :: [Blocks] -> ShowS

mkBlocks :: [Block] -> Blocks

readVersion :: Theory -> Interpret -> NameVersion -> IO Theory

readPackageFile :: Theory -> Interpret -> FilePath -> IO Theory

readPackage :: Theory -> Interpret -> FilePath -> Package -> IO Theory

readBlocks :: Theory -> Interpret -> FilePath -> Blocks -> IO Theory

readBlock :: Theory -> Interpret -> FilePath -> [Theory] -> Block -> IO Theory

newtype Requires

Constructors

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

emptyRequires :: Requires

addRequires :: Requires -> Name -> IO Requires

fromListRequires :: [Name] -> IO Requires

readList :: [Name] -> IO [Theory]