Safe Haskell	None
Language	Haskell2010

HOL.OpenTheory.Package

Description

Documentation

newtype Name Source #

Constructors

Name
Fields destName :: String

Instances

Instances details

Eq Name Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Name -> Name -> Bool # (/=) :: Name -> Name -> Bool #
Ord Name Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Name -> ShowS # show :: Name -> String # showList :: [Name] -> ShowS #
Parsable Name Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st Name Source # fromText :: Text -> Maybe Name Source # fromString :: String -> Maybe Name Source # fromStringUnsafe :: String -> Name Source # fromTextFile :: FilePath -> IO Name Source #
Printable Name Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Name -> Doc Source # toStringWith :: Style -> Name -> String Source # toString :: Name -> String Source #

newtype Version Source #

Constructors

Version
Fields destVersion :: String

Instances

Instances details

Eq Version Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Version -> Version -> Bool # (/=) :: Version -> Version -> Bool #
Ord Version Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Version -> ShowS # show :: Version -> String # showList :: [Version] -> ShowS #
Parsable Version Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st Version Source # fromText :: Text -> Maybe Version Source # fromString :: String -> Maybe Version Source # fromStringUnsafe :: String -> Version Source # fromTextFile :: FilePath -> IO Version Source #
Printable Version Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Version -> Doc Source # toStringWith :: Style -> Version -> String Source # toString :: Version -> String Source #

data NameVersion Source #

Constructors

NameVersion
Fields name :: Name version :: Version

Instances

Instances details

Eq NameVersion Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: NameVersion -> NameVersion -> Bool # (/=) :: NameVersion -> NameVersion -> Bool #
Ord NameVersion Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> NameVersion -> ShowS # show :: NameVersion -> String # showList :: [NameVersion] -> ShowS #
Parsable NameVersion Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st NameVersion Source # fromText :: Text -> Maybe NameVersion Source # fromString :: String -> Maybe NameVersion Source # fromStringUnsafe :: String -> NameVersion Source # fromTextFile :: FilePath -> IO NameVersion Source #
Printable NameVersion Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: NameVersion -> Doc Source # toStringWith :: Style -> NameVersion -> String Source # toString :: NameVersion -> String Source #

data KeyValue Source #

Constructors

KeyValue Name String

Instances

Instances details

Eq KeyValue Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: KeyValue -> KeyValue -> Bool # (/=) :: KeyValue -> KeyValue -> Bool #
Ord KeyValue Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> KeyValue -> ShowS # show :: KeyValue -> String # showList :: [KeyValue] -> ShowS #
Parsable KeyValue Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st KeyValue Source # fromText :: Text -> Maybe KeyValue Source # fromString :: String -> Maybe KeyValue Source # fromStringUnsafe :: String -> KeyValue Source # fromTextFile :: FilePath -> IO KeyValue Source #
Printable KeyValue Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: KeyValue -> Doc Source # toStringWith :: Style -> KeyValue -> String Source # toString :: KeyValue -> String Source #

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

matchKeyValue :: Name -> KeyValue -> Maybe String Source #

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

newtype Info Source #

Constructors

Info
Fields destInfo :: [KeyValue]

Instances

Instances details

Eq Info Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Info -> Info -> Bool # (/=) :: Info -> Info -> Bool #
Ord Info Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Info -> ShowS # show :: Info -> String # showList :: [Info] -> ShowS #
Parsable Info Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st Info Source # fromText :: Text -> Maybe Info Source # fromString :: String -> Maybe Info Source # fromStringUnsafe :: String -> Info Source # fromTextFile :: FilePath -> IO Info Source #
Printable Info Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Info -> Doc Source # toStringWith :: Style -> Info -> String Source # toString :: Info -> String Source #

nullInfo :: Info -> Bool Source #

appendInfo :: Info -> Info -> Info Source #

concatInfo :: [Info] -> Info Source #

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

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

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

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

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

class Informative a where Source #

Minimal complete definition

toInfo, getInfo

Methods

toInfo :: a -> Info Source #

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

fromInfo :: Info -> Maybe a Source #

Instances

Instances details

Informative Operation Source #
Instance details Defined in HOL.OpenTheory.Package Methods toInfo :: Operation -> Info Source # getInfo :: Info -> Maybe (Operation, Info) Source # fromInfo :: Info -> Maybe Operation Source #
Informative Interpretation Source #
Instance details Defined in HOL.OpenTheory.Package Methods toInfo :: Interpretation -> Info Source # getInfo :: Info -> Maybe (Interpretation, Info) Source # fromInfo :: Info -> Maybe Interpretation Source #
Informative a => Informative [a] Source #
Instance details Defined in HOL.OpenTheory.Package Methods toInfo :: [a] -> Info Source # getInfo :: Info -> Maybe ([a], Info) Source # fromInfo :: Info -> Maybe [a] Source #
(Informative a, Informative b) => Informative (a, b) Source #
Instance details Defined in HOL.OpenTheory.Package Methods toInfo :: (a, b) -> Info Source # getInfo :: Info -> Maybe ((a, b), Info) Source # fromInfo :: Info -> Maybe (a, b) Source #

newtype File Source #

Constructors

File
Fields destFile :: FilePath

Instances

Instances details

Eq File Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: File -> File -> Bool # (/=) :: File -> File -> Bool #
Ord File Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> File -> ShowS # show :: File -> String # showList :: [File] -> ShowS #
Parsable File Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st File Source # fromText :: Text -> Maybe File Source # fromString :: String -> Maybe File Source # fromStringUnsafe :: String -> File Source # fromTextFile :: FilePath -> IO File Source #
Printable File Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: File -> Doc Source # toStringWith :: Style -> File -> String Source # toString :: File -> String Source #

data Interpretation Source #

Constructors

Interpret Rename
Interpretation File

Instances

Instances details

Eq Interpretation Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Interpretation -> Interpretation -> Bool # (/=) :: Interpretation -> Interpretation -> Bool #
Ord Interpretation Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Interpretation -> ShowS # show :: Interpretation -> String # showList :: [Interpretation] -> ShowS #
Informative Interpretation Source #
Instance details Defined in HOL.OpenTheory.Package Methods toInfo :: Interpretation -> Info Source # getInfo :: Info -> Maybe (Interpretation, Info) Source # fromInfo :: Info -> Maybe Interpretation Source #

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

data Operation Source #

Constructors

Article File
Include
Fields package :: NameVersion checksum :: Maybe String
Union

Instances

Instances details

Eq Operation Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Operation -> Operation -> Bool # (/=) :: Operation -> Operation -> Bool #
Ord Operation Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Operation -> ShowS # show :: Operation -> String # showList :: [Operation] -> ShowS #
Informative Operation Source #
Instance details Defined in HOL.OpenTheory.Package Methods toInfo :: Operation -> Info Source # getInfo :: Info -> Maybe (Operation, Info) Source # fromInfo :: Info -> Maybe Operation Source #

data Block Source #

Constructors

Block
Fields block :: Name imports :: [Name] interpret :: [Interpretation] operation :: Operation

Instances

Instances details

Eq Block Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Block -> Block -> Bool # (/=) :: Block -> Block -> Bool #
Ord Block Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Block -> ShowS # show :: Block -> String # showList :: [Block] -> ShowS #
Parsable Block Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st Block Source # fromText :: Text -> Maybe Block Source # fromString :: String -> Maybe Block Source # fromStringUnsafe :: String -> Block Source # fromTextFile :: FilePath -> IO Block Source #
Printable Block Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Block -> Doc Source # toStringWith :: Style -> Block -> String Source # toString :: Block -> String Source #

mkBlock :: Name -> Info -> Maybe Block Source #

destBlock :: Block -> (Name, Info) Source #

data Package Source #

Constructors

Package
Fields information :: Info source :: [Block]

Instances

Instances details

Eq Package Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Package -> Package -> Bool # (/=) :: Package -> Package -> Bool #
Ord Package Source #
Instance details Defined in HOL.OpenTheory.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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Package -> ShowS # show :: Package -> String # showList :: [Package] -> ShowS #
Parsable Package Source #
Instance details Defined in HOL.OpenTheory.Package Methods parser :: Parsec Text st Package Source # fromText :: Text -> Maybe Package Source # fromString :: String -> Maybe Package Source # fromStringUnsafe :: String -> Package Source # fromTextFile :: FilePath -> IO Package Source #
Printable Package Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Package -> Doc Source # toStringWith :: Style -> Package -> String Source # toString :: Package -> String Source #

requires :: Package -> [Name] Source #

packageFile :: FilePath -> Name -> FilePath Source #

opentheory :: [String] -> IO String Source #

opentheoryDirectory :: String -> IO FilePath Source #

directory :: Name -> IO FilePath Source #

directoryVersion :: NameVersion -> IO FilePath Source #

newtype Blocks Source #

Constructors

Blocks
Fields destBlocks :: [Block]

Instances

Instances details

Eq Blocks Source #
Instance details Defined in HOL.OpenTheory.Package Methods (==) :: Blocks -> Blocks -> Bool # (/=) :: Blocks -> Blocks -> Bool #
Ord Blocks Source #
Instance details Defined in HOL.OpenTheory.Package 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 Source #
Instance details Defined in HOL.OpenTheory.Package Methods showsPrec :: Int -> Blocks -> ShowS # show :: Blocks -> String # showList :: [Blocks] -> ShowS #

mkBlocks :: [Block] -> Blocks Source #

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

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

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

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

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

newtype Requires Source #

Constructors

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

emptyRequires :: Requires Source #

addRequires :: Requires -> Name -> IO Requires Source #

fromListRequires :: [Name] -> IO Requires Source #

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