HOL.OpenTheory.Interpret

Documentation

data Symbol

Constructors

TypeOpSymbol Name

ConstSymbol Name

Instances

Eq Symbol

Methods

(==) :: Symbol -> Symbol -> Bool

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

Ord Symbol

Methods

compare :: Symbol -> Symbol -> Ordering

(<) :: Symbol -> Symbol -> Bool

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

(>) :: Symbol -> Symbol -> Bool

(>=) :: Symbol -> Symbol -> Bool

max :: Symbol -> Symbol -> Symbol

min :: Symbol -> Symbol -> Symbol

Show Symbol

Methods

showsPrec :: Int -> Symbol -> ShowS

show :: Symbol -> String

showList :: [Symbol] -> ShowS

Parsable Symbol

Methods

parser :: Parsec Text st Symbol

fromText :: Text -> Maybe Symbol

fromString :: String -> Maybe Symbol

fromStringUnsafe :: String -> Symbol

fromTextFile :: FilePath -> IO Symbol

Printable Symbol

Methods

toDoc :: Symbol -> Doc

toStringWith :: Style -> Symbol -> String

toString :: Symbol -> String

symbolName :: Symbol -> Name

renameSymbol :: Symbol -> Name -> Symbol

data Rename

Constructors

Rename Symbol Name

Instances

Eq Rename

Methods

(==) :: Rename -> Rename -> Bool

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

Ord Rename

Methods

compare :: Rename -> Rename -> Ordering

(<) :: Rename -> Rename -> Bool

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

(>) :: Rename -> Rename -> Bool

(>=) :: Rename -> Rename -> Bool

max :: Rename -> Rename -> Rename

min :: Rename -> Rename -> Rename

Show Rename

Methods

showsPrec :: Int -> Rename -> ShowS

show :: Rename -> String

showList :: [Rename] -> ShowS

Parsable Rename

Methods

parser :: Parsec Text st Rename

fromText :: Text -> Maybe Rename

fromString :: String -> Maybe Rename

fromStringUnsafe :: String -> Rename

fromTextFile :: FilePath -> IO Rename

Printable Rename

Methods

toDoc :: Rename -> Doc

toStringWith :: Style -> Rename -> String

toString :: Rename -> String

destRename :: Rename -> (Symbol, Name)

newtype Renames

Constructors

Renames

Fields

• destRenames :: [Rename]

Instances

Eq Renames

Methods

(==) :: Renames -> Renames -> Bool

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

Ord Renames

Methods

compare :: Renames -> Renames -> Ordering

(<) :: Renames -> Renames -> Bool

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

(>) :: Renames -> Renames -> Bool

(>=) :: Renames -> Renames -> Bool

max :: Renames -> Renames -> Renames

min :: Renames -> Renames -> Renames

Show Renames

Methods

showsPrec :: Int -> Renames -> ShowS

show :: Renames -> String

showList :: [Renames] -> ShowS

Parsable Renames

Methods

parser :: Parsec Text st Renames

fromText :: Text -> Maybe Renames

fromString :: String -> Maybe Renames

fromStringUnsafe :: String -> Renames

fromTextFile :: FilePath -> IO Renames

Printable Renames

Methods

toDoc :: Renames -> Doc

toStringWith :: Style -> Renames -> String

toString :: Renames -> String

concatRenames :: [Renames] -> Renames

data Interpret

Constructors

Interpret (Map Symbol Name)

Instances

Parsable Interpret

Methods

parser :: Parsec Text st Interpret

fromText :: Text -> Maybe Interpret

fromString :: String -> Maybe Interpret

fromStringUnsafe :: String -> Interpret

fromTextFile :: FilePath -> IO Interpret

Printable Interpret

Methods

toDoc :: Interpret -> Doc

toStringWith :: Style -> Interpret -> String

toString :: Interpret -> String

mk :: Map Symbol Name -> Interpret

empty :: Interpret

toRenames :: Interpret -> Renames

fromRenames :: Renames -> Maybe Interpret

fromRenamesUnsafe :: Renames -> Interpret

interpret :: Interpret -> Symbol -> Name

interpretTypeOp :: Interpret -> Name -> Name

interpretConst :: Interpret -> Name -> Name

compose :: Interpret -> Interpret -> Interpret

• interpret (compose i1 i2) s == interpret i2 (interpret i1 s)