Safe Haskell	Safe-Inferred
Language	Haskell2010

RSTT.Syntax.Abs

Description

The abstract syntax of language Syntax.

Documentation

data Program Source #

Constructors

Program [Decl]

Instances

Instances details

Read Program Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Program # readList :: ReadS [Program] # readPrec :: ReadPrec Program # readListPrec :: ReadPrec [Program] #
Show Program Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Program -> ShowS # show :: Program -> String # showList :: [Program] -> ShowS #
Eq Program Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Program -> Program -> Bool # (/=) :: Program -> Program -> Bool #
Ord Program Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Program -> Program -> Ordering # (<) :: Program -> Program -> Bool # (<=) :: Program -> Program -> Bool # (>) :: Program -> Program -> Bool # (>=) :: Program -> Program -> Bool # max :: Program -> Program -> Program # min :: Program -> Program -> Program #
Print Program Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Program -> Doc Source #

data Decl Source #

Constructors

DeclCube Label [PointConDecl]
DeclTopePrefix Label [Cube] [TopeRule]
DeclShape Var Shape
DeclCommandProve Sequent
DeclCommandRenderLatex Shape

Instances

Instances details

Read Decl Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Decl # readList :: ReadS [Decl] # readPrec :: ReadPrec Decl # readListPrec :: ReadPrec [Decl] #
Show Decl Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Decl -> ShowS # show :: Decl -> String # showList :: [Decl] -> ShowS #
Eq Decl Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Decl -> Decl -> Bool # (/=) :: Decl -> Decl -> Bool #
Ord Decl Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Decl -> Decl -> Ordering # (<) :: Decl -> Decl -> Bool # (<=) :: Decl -> Decl -> Bool # (>) :: Decl -> Decl -> Bool # (>=) :: Decl -> Decl -> Bool # max :: Decl -> Decl -> Decl # min :: Decl -> Decl -> Decl #
Print Decl Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Decl -> Doc Source #
Print [Decl] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [Decl] -> Doc Source #

data Shape Source #

Constructors

Shape PointPattern Cube Tope

Instances

Instances details

Read Shape Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Shape # readList :: ReadS [Shape] # readPrec :: ReadPrec Shape # readListPrec :: ReadPrec [Shape] #
Show Shape Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Shape -> ShowS # show :: Shape -> String # showList :: [Shape] -> ShowS #
Eq Shape Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Shape -> Shape -> Bool # (/=) :: Shape -> Shape -> Bool #
Ord Shape Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Shape -> Shape -> Ordering # (<) :: Shape -> Shape -> Bool # (<=) :: Shape -> Shape -> Bool # (>) :: Shape -> Shape -> Bool # (>=) :: Shape -> Shape -> Bool # max :: Shape -> Shape -> Shape # min :: Shape -> Shape -> Shape #
Print Shape Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Shape -> Doc Source #

data PointPattern Source #

Constructors

PointPatternVar Var
PointPatternPair PointPattern PointPattern

Instances

Instances details

Read PointPattern Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS PointPattern # readList :: ReadS [PointPattern] # readPrec :: ReadPrec PointPattern # readListPrec :: ReadPrec [PointPattern] #
Show PointPattern Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> PointPattern -> ShowS # show :: PointPattern -> String # showList :: [PointPattern] -> ShowS #
Eq PointPattern Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: PointPattern -> PointPattern -> Bool # (/=) :: PointPattern -> PointPattern -> Bool #
Ord PointPattern Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: PointPattern -> PointPattern -> Ordering # (<) :: PointPattern -> PointPattern -> Bool # (<=) :: PointPattern -> PointPattern -> Bool # (>) :: PointPattern -> PointPattern -> Bool # (>=) :: PointPattern -> PointPattern -> Bool # max :: PointPattern -> PointPattern -> PointPattern # min :: PointPattern -> PointPattern -> PointPattern #
Print PointPattern Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> PointPattern -> Doc Source #

data PointConDecl Source #

Constructors

NullaryPointConDecl Label
PrefixPointConDecl Label [Cube]

Instances

Instances details

Read PointConDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS PointConDecl # readList :: ReadS [PointConDecl] # readPrec :: ReadPrec PointConDecl # readListPrec :: ReadPrec [PointConDecl] #
Show PointConDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> PointConDecl -> ShowS # show :: PointConDecl -> String # showList :: [PointConDecl] -> ShowS #
Eq PointConDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: PointConDecl -> PointConDecl -> Bool # (/=) :: PointConDecl -> PointConDecl -> Bool #
Ord PointConDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: PointConDecl -> PointConDecl -> Ordering # (<) :: PointConDecl -> PointConDecl -> Bool # (<=) :: PointConDecl -> PointConDecl -> Bool # (>) :: PointConDecl -> PointConDecl -> Bool # (>=) :: PointConDecl -> PointConDecl -> Bool # max :: PointConDecl -> PointConDecl -> PointConDecl # min :: PointConDecl -> PointConDecl -> PointConDecl #
Print PointConDecl Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> PointConDecl -> Doc Source #
Print [PointConDecl] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [PointConDecl] -> Doc Source #

data Cube Source #

Constructors

CubeProduct Cube Cube
CubeUnit
CubeCon Label
CubeVar Var

Instances

Instances details

Read Cube Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Cube # readList :: ReadS [Cube] # readPrec :: ReadPrec Cube # readListPrec :: ReadPrec [Cube] #
Show Cube Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Cube -> ShowS # show :: Cube -> String # showList :: [Cube] -> ShowS #
Eq Cube Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Cube -> Cube -> Bool # (/=) :: Cube -> Cube -> Bool #
Ord Cube Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Cube -> Cube -> Ordering # (<) :: Cube -> Cube -> Bool # (<=) :: Cube -> Cube -> Bool # (>) :: Cube -> Cube -> Bool # (>=) :: Cube -> Cube -> Bool # max :: Cube -> Cube -> Cube # min :: Cube -> Cube -> Cube #
Print Cube Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Cube -> Doc Source #
Print [Cube] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [Cube] -> Doc Source #

data TopeRule Source #

Constructors

TopeRule RuleName [Sequent] Line Sequent

Instances

Instances details

Read TopeRule Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS TopeRule # readList :: ReadS [TopeRule] # readPrec :: ReadPrec TopeRule # readListPrec :: ReadPrec [TopeRule] #
Show TopeRule Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> TopeRule -> ShowS # show :: TopeRule -> String # showList :: [TopeRule] -> ShowS #
Eq TopeRule Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: TopeRule -> TopeRule -> Bool # (/=) :: TopeRule -> TopeRule -> Bool #
Ord TopeRule Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: TopeRule -> TopeRule -> Ordering # (<) :: TopeRule -> TopeRule -> Bool # (<=) :: TopeRule -> TopeRule -> Bool # (>) :: TopeRule -> TopeRule -> Bool # (>=) :: TopeRule -> TopeRule -> Bool # max :: TopeRule -> TopeRule -> TopeRule # min :: TopeRule -> TopeRule -> TopeRule #
Print TopeRule Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> TopeRule -> Doc Source #
Print [TopeRule] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [TopeRule] -> Doc Source #

data RuleName Source #

Constructors

RuleName String

Instances

Instances details

Read RuleName Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS RuleName # readList :: ReadS [RuleName] # readPrec :: ReadPrec RuleName # readListPrec :: ReadPrec [RuleName] #
Show RuleName Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> RuleName -> ShowS # show :: RuleName -> String # showList :: [RuleName] -> ShowS #
Eq RuleName Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: RuleName -> RuleName -> Bool # (/=) :: RuleName -> RuleName -> Bool #
Ord RuleName Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: RuleName -> RuleName -> Ordering # (<) :: RuleName -> RuleName -> Bool # (<=) :: RuleName -> RuleName -> Bool # (>) :: RuleName -> RuleName -> Bool # (>=) :: RuleName -> RuleName -> Bool # max :: RuleName -> RuleName -> RuleName # min :: RuleName -> RuleName -> RuleName #
Print RuleName Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> RuleName -> Doc Source #

data Sequent Source #

Constructors

Sequent CubeContext TopeContext Tope

Instances

Instances details

Read Sequent Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Sequent # readList :: ReadS [Sequent] # readPrec :: ReadPrec Sequent # readListPrec :: ReadPrec [Sequent] #
Show Sequent Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Sequent -> ShowS # show :: Sequent -> String # showList :: [Sequent] -> ShowS #
Eq Sequent Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Sequent -> Sequent -> Bool # (/=) :: Sequent -> Sequent -> Bool #
Ord Sequent Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Sequent -> Sequent -> Ordering # (<) :: Sequent -> Sequent -> Bool # (<=) :: Sequent -> Sequent -> Bool # (>) :: Sequent -> Sequent -> Bool # (>=) :: Sequent -> Sequent -> Bool # max :: Sequent -> Sequent -> Sequent # min :: Sequent -> Sequent -> Sequent #
Print Sequent Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Sequent -> Doc Source #
Print [Sequent] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [Sequent] -> Doc Source #

data CubeContext Source #

Constructors

CubeContextEmpty
CubeContextNonEmpty [PointDecl]

Instances

Instances details

Read CubeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS CubeContext # readList :: ReadS [CubeContext] # readPrec :: ReadPrec CubeContext # readListPrec :: ReadPrec [CubeContext] #
Show CubeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> CubeContext -> ShowS # show :: CubeContext -> String # showList :: [CubeContext] -> ShowS #
Eq CubeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: CubeContext -> CubeContext -> Bool # (/=) :: CubeContext -> CubeContext -> Bool #
Ord CubeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: CubeContext -> CubeContext -> Ordering # (<) :: CubeContext -> CubeContext -> Bool # (<=) :: CubeContext -> CubeContext -> Bool # (>) :: CubeContext -> CubeContext -> Bool # (>=) :: CubeContext -> CubeContext -> Bool # max :: CubeContext -> CubeContext -> CubeContext # min :: CubeContext -> CubeContext -> CubeContext #
Print CubeContext Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> CubeContext -> Doc Source #

data PointDecl Source #

Constructors

PointDecl Var Cube

Instances

Instances details

Read PointDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS PointDecl # readList :: ReadS [PointDecl] # readPrec :: ReadPrec PointDecl # readListPrec :: ReadPrec [PointDecl] #
Show PointDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> PointDecl -> ShowS # show :: PointDecl -> String # showList :: [PointDecl] -> ShowS #
Eq PointDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: PointDecl -> PointDecl -> Bool # (/=) :: PointDecl -> PointDecl -> Bool #
Ord PointDecl Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: PointDecl -> PointDecl -> Ordering # (<) :: PointDecl -> PointDecl -> Bool # (<=) :: PointDecl -> PointDecl -> Bool # (>) :: PointDecl -> PointDecl -> Bool # (>=) :: PointDecl -> PointDecl -> Bool # max :: PointDecl -> PointDecl -> PointDecl # min :: PointDecl -> PointDecl -> PointDecl #
Print PointDecl Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> PointDecl -> Doc Source #
Print [PointDecl] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [PointDecl] -> Doc Source #

data TopeContext Source #

Constructors

TopeContextEmpty
TopeContextNonEmpty [Tope]

Instances

Instances details

Read TopeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS TopeContext # readList :: ReadS [TopeContext] # readPrec :: ReadPrec TopeContext # readListPrec :: ReadPrec [TopeContext] #
Show TopeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> TopeContext -> ShowS # show :: TopeContext -> String # showList :: [TopeContext] -> ShowS #
Eq TopeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: TopeContext -> TopeContext -> Bool # (/=) :: TopeContext -> TopeContext -> Bool #
Ord TopeContext Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: TopeContext -> TopeContext -> Ordering # (<) :: TopeContext -> TopeContext -> Bool # (<=) :: TopeContext -> TopeContext -> Bool # (>) :: TopeContext -> TopeContext -> Bool # (>=) :: TopeContext -> TopeContext -> Bool # max :: TopeContext -> TopeContext -> TopeContext # min :: TopeContext -> TopeContext -> TopeContext #
Print TopeContext Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> TopeContext -> Doc Source #

data Tope Source #

Constructors

TopeTop
TopeBottom
TopeImplies Tope Tope
TopeOr Tope Tope
TopeAnd Tope Tope
TopeEQ Point Point
TopeCon Label [Point]
TopeVar Var

Instances

Instances details

Read Tope Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Tope # readList :: ReadS [Tope] # readPrec :: ReadPrec Tope # readListPrec :: ReadPrec [Tope] #
Show Tope Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Tope -> ShowS # show :: Tope -> String # showList :: [Tope] -> ShowS #
Eq Tope Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Tope -> Tope -> Bool # (/=) :: Tope -> Tope -> Bool #
Ord Tope Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Tope -> Tope -> Ordering # (<) :: Tope -> Tope -> Bool # (<=) :: Tope -> Tope -> Bool # (>) :: Tope -> Tope -> Bool # (>=) :: Tope -> Tope -> Bool # max :: Tope -> Tope -> Tope # min :: Tope -> Tope -> Tope #
Print Tope Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Tope -> Doc Source #
Print [Tope] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [Tope] -> Doc Source #

data Point Source #

Constructors

PointUnit
PointPair Point Point
PointFirst Point
PointSecond Point
PointCon Label [Point]
PointVar Var

Instances

Instances details

Read Point Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Point # readList :: ReadS [Point] # readPrec :: ReadPrec Point # readListPrec :: ReadPrec [Point] #
Show Point Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Point -> ShowS # show :: Point -> String # showList :: [Point] -> ShowS #
Eq Point Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Point -> Point -> Bool # (/=) :: Point -> Point -> Bool #
Ord Point Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Point -> Point -> Ordering # (<) :: Point -> Point -> Bool # (<=) :: Point -> Point -> Bool # (>) :: Point -> Point -> Bool # (>=) :: Point -> Point -> Bool # max :: Point -> Point -> Point # min :: Point -> Point -> Point #
Print Point Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Point -> Doc Source #
Print [Point] Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> [Point] -> Doc Source #

nullaryPoint :: Label -> Point Source #

newtype Label Source #

Constructors

Label String

Instances

Instances details

IsString Label Source #
Instance details Defined in RSTT.Syntax.Abs Methods fromString :: String -> Label #
Read Label Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Label # readList :: ReadS [Label] # readPrec :: ReadPrec Label # readListPrec :: ReadPrec [Label] #
Show Label Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Label -> ShowS # show :: Label -> String # showList :: [Label] -> ShowS #
Eq Label Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Label -> Label -> Bool # (/=) :: Label -> Label -> Bool #
Ord Label Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Label -> Label -> Ordering # (<) :: Label -> Label -> Bool # (<=) :: Label -> Label -> Bool # (>) :: Label -> Label -> Bool # (>=) :: Label -> Label -> Bool # max :: Label -> Label -> Label # min :: Label -> Label -> Label #
Print Label Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Label -> Doc Source #

newtype Var Source #

Constructors

Var String

Instances

Instances details

IsString Var Source #
Instance details Defined in RSTT.Syntax.Abs Methods fromString :: String -> Var #
Read Var Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Var # readList :: ReadS [Var] # readPrec :: ReadPrec Var # readListPrec :: ReadPrec [Var] #
Show Var Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #
Eq Var Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Var -> Var -> Ordering # (<) :: Var -> Var -> Bool # (<=) :: Var -> Var -> Bool # (>) :: Var -> Var -> Bool # (>=) :: Var -> Var -> Bool # max :: Var -> Var -> Var # min :: Var -> Var -> Var #
Print Var Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Var -> Doc Source #

newtype Line Source #

Constructors

Line String

Instances

Instances details

IsString Line Source #
Instance details Defined in RSTT.Syntax.Abs Methods fromString :: String -> Line #
Read Line Source #
Instance details Defined in RSTT.Syntax.Abs Methods readsPrec :: Int -> ReadS Line # readList :: ReadS [Line] # readPrec :: ReadPrec Line # readListPrec :: ReadPrec [Line] #
Show Line Source #
Instance details Defined in RSTT.Syntax.Abs Methods showsPrec :: Int -> Line -> ShowS # show :: Line -> String # showList :: [Line] -> ShowS #
Eq Line Source #
Instance details Defined in RSTT.Syntax.Abs Methods (==) :: Line -> Line -> Bool # (/=) :: Line -> Line -> Bool #
Ord Line Source #
Instance details Defined in RSTT.Syntax.Abs Methods compare :: Line -> Line -> Ordering # (<) :: Line -> Line -> Bool # (<=) :: Line -> Line -> Bool # (>) :: Line -> Line -> Bool # (>=) :: Line -> Line -> Bool # max :: Line -> Line -> Line # min :: Line -> Line -> Line #
Print Line Source #
Instance details Defined in RSTT.Syntax.Print Methods prt :: Int -> Line -> Doc Source #