HOL.OpenTheory.Article

Documentation

newtype Number

Constructors

Number Integer

Instances

Eq Number

Methods

(==) :: Number -> Number -> Bool

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

Ord Number

Methods

compare :: Number -> Number -> Ordering

(<) :: Number -> Number -> Bool

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

(>) :: Number -> Number -> Bool

(>=) :: Number -> Number -> Bool

max :: Number -> Number -> Number

min :: Number -> Number -> Number

Show Number

Methods

showsPrec :: Int -> Number -> ShowS

show :: Number -> String

showList :: [Number] -> ShowS

Parsable Number

Methods

parser :: Parsec Text st Number

fromText :: Text -> Maybe Number

fromString :: String -> Maybe Number

fromStringUnsafe :: String -> Number

fromTextFile :: FilePath -> IO Number

Printable Number

Methods

toDoc :: Number -> Doc

toStringWith :: Style -> Number -> String

toString :: Number -> String

Objective Number

Methods

toObject :: Number -> Object

fromObject :: Object -> Maybe Number

data Object

Constructors

NumberObject Number

NameObject Name

ListObject [Object]

TypeOpObject TypeOp

TypeObject Type

ConstObject Const

VarObject Var

TermObject Term

ThmObject Thm

Instances

Eq Object

Methods

(==) :: Object -> Object -> Bool

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

Ord Object

Methods

compare :: Object -> Object -> Ordering

(<) :: Object -> Object -> Bool

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

(>) :: Object -> Object -> Bool

(>=) :: Object -> Object -> Bool

max :: Object -> Object -> Object

min :: Object -> Object -> Object

Show Object

Methods

showsPrec :: Int -> Object -> ShowS

show :: Object -> String

showList :: [Object] -> ShowS

Printable Object

Methods

toDoc :: Object -> Doc

toStringWith :: Style -> Object -> String

toString :: Object -> String

Objective Object

Methods

toObject :: Object -> Object

fromObject :: Object -> Maybe Object

class Objective a where

Minimal complete definition

toObject, fromObject

Methods

toObject :: a -> Object

fromObject :: Object -> Maybe a

Instances

Objective Name

Methods

toObject :: Name -> Object

fromObject :: Object -> Maybe Name

Objective Term

Methods

toObject :: Term -> Object

fromObject :: Object -> Maybe Term

Objective Const

Methods

toObject :: Const -> Object

fromObject :: Object -> Maybe Const

Objective Var

Methods

toObject :: Var -> Object

fromObject :: Object -> Maybe Var

Objective Type

Methods

toObject :: Type -> Object

fromObject :: Object -> Maybe Type

Objective TypeOp

Methods

toObject :: TypeOp -> Object

fromObject :: Object -> Maybe TypeOp

Objective Thm

Methods

toObject :: Thm -> Object

fromObject :: Object -> Maybe Thm

Objective Object

Methods

toObject :: Object -> Object

fromObject :: Object -> Maybe Object

Objective Number

Methods

toObject :: Number -> Object

fromObject :: Object -> Maybe Number

Objective a => Objective [a]

Methods

toObject :: [a] -> Object

fromObject :: Object -> Maybe [a]

(Objective a, Objective b) => Objective (a, b)

Methods

toObject :: (a, b) -> Object

fromObject :: Object -> Maybe (a, b)

sequentObject :: Object -> Object -> Maybe Sequent

pushObject :: Objective a => a -> [Object] -> [Object]

push2Object :: (Objective a, Objective b) => a -> b -> [Object] -> [Object]

push3Object :: (Objective a, Objective b, Objective c) => a -> b -> c -> [Object] -> [Object]

push4Object :: (Objective a, Objective b, Objective c, Objective d) => a -> b -> c -> d -> [Object] -> [Object]

push5Object :: (Objective a, Objective b, Objective c, Objective d, Objective e) => a -> b -> c -> d -> e -> [Object] -> [Object]

popObject :: Objective a => [Object] -> Maybe (a, [Object])

pop2Object :: (Objective a, Objective b) => [Object] -> Maybe (a, b, [Object])

pop3Object :: (Objective a, Objective b, Objective c) => [Object] -> Maybe (a, b, c, [Object])

pop4Object :: (Objective a, Objective b, Objective c, Objective d) => [Object] -> Maybe (a, b, c, d, [Object])

pop5Object :: (Objective a, Objective b, Objective c, Objective d, Objective e) => [Object] -> Maybe (a, b, c, d, e, [Object])

data Command

Constructors

NumberCommand Number

NameCommand Name

AbsTermCommand

AbsThmCommand

AppTermCommand

AppThmCommand

AssumeCommand

AxiomCommand

BetaConvCommand

ConsCommand

ConstCommand

ConstTermCommand

DeductAntisymCommand

DefCommand

DefineConstCommand

DefineConstListCommand

DefineTypeOpCommand

EqMpCommand

HdTlCommand

NilCommand

OpTypeCommand

PopCommand

PragmaCommand

ProveHypCommand

RefCommand

ReflCommand

RemoveCommand

SubstCommand

SymCommand

ThmCommand

TransCommand

TypeOpCommand

VarCommand

VarTermCommand

VarTypeCommand

VersionCommand

DefineTypeOpLegacyCommand

Instances

Eq Command

Methods

(==) :: Command -> Command -> Bool

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

Ord Command

Methods

compare :: Command -> Command -> Ordering

(<) :: Command -> Command -> Bool

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

(>) :: Command -> Command -> Bool

(>=) :: Command -> Command -> Bool

max :: Command -> Command -> Command

min :: Command -> Command -> Command

Show Command

Methods

showsPrec :: Int -> Command -> ShowS

show :: Command -> String

showList :: [Command] -> ShowS

Parsable Command

Methods

parser :: Parsec Text st Command

fromText :: Text -> Maybe Command

fromString :: String -> Maybe Command

fromStringUnsafe :: String -> Command

fromTextFile :: FilePath -> IO Command

Printable Command

Methods

toDoc :: Command -> Doc

toStringWith :: Style -> Command -> String

toString :: Command -> String

regularCommands :: [(Command, String)]

type Version = Number

supportedCommand :: Version -> Command -> Bool

versionCommand :: Version -> Command -> Maybe Command

data State

Constructors

State

Fields

• stack :: [Object]
• dict :: Map Number Object
• theorems :: Set Thm

Instances

Eq State

Methods

(==) :: State -> State -> Bool

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

Ord State

Methods

compare :: State -> State -> Ordering

(<) :: State -> State -> Bool

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

(>) :: State -> State -> Bool

(>=) :: State -> State -> Bool

max :: State -> State -> State

min :: State -> State -> State

Show State

Methods

showsPrec :: Int -> State -> ShowS

show :: State -> String

showList :: [State] -> ShowS

Printable State

Methods

toDoc :: State -> Doc

toStringWith :: Style -> State -> String

toString :: State -> String

pushState :: Objective a => a -> State -> State

push2State :: (Objective a, Objective b) => a -> b -> State -> State

push5State :: (Objective a, Objective b, Objective c, Objective d, Objective e) => a -> b -> c -> d -> e -> State -> State

popState :: Objective a => State -> Maybe (a, State)

pop2State :: (Objective a, Objective b) => State -> Maybe (a, b, State)

pop3State :: (Objective a, Objective b, Objective c) => State -> Maybe (a, b, c, State)

pop5State :: (Objective a, Objective b, Objective c, Objective d, Objective e) => State -> Maybe (a, b, c, d, e, State)

peekState :: Objective a => State -> Maybe a

defState :: Number -> Object -> State -> State

refState :: Number -> State -> Maybe Object

removeState :: Number -> State -> Maybe (Object, State)

thmState :: Thm -> State -> State

initialState :: State

executeCommand :: Theory -> Interpret -> State -> Command -> Maybe State

type LineNumber = Integer

readArticle :: Theory -> Interpret -> FilePath -> IO (Set Thm)