Safe Haskell	None

TIP.AbsTIP

Description

The abstract syntax of language TIP.

Synopsis

data Start = Start [Decl]
data Decl
- = DeclareDatatype AttrSymbol Datatype
- | DeclareDatatypes [DatatypeName] [Datatype]
- | DeclareSort AttrSymbol Integer
- | DeclareConst AttrSymbol ConstType
- | DeclareFun AttrSymbol FunType
- | DefineFun FunDec Expr
- | DefineFunRec FunDec Expr
- | DefineFunsRec [BracketedFunDec] [Expr]
- | Formula Assertion [Attr] Expr
- | FormulaPar Assertion [Attr] Par Expr
data Assertion
- = Assert
- | Prove
data Par = Par [Symbol]
data ConstType
- = ConstTypeMono Type
- | ConstTypePoly Par Type
data InnerFunType = InnerFunType [Type] Type
data FunType
- = FunTypeMono InnerFunType
- | FunTypePoly Par InnerFunType
data InnerFunDec = InnerFunDec [Binding] Type
data FunDec
- = FunDecMono AttrSymbol InnerFunDec
- | FunDecPoly AttrSymbol Par InnerFunDec
data BracketedFunDec = BracketedFunDec FunDec
data DatatypeName = DatatypeName AttrSymbol Integer
data InnerDatatype = InnerDatatype [Constructor]
data Datatype
- = DatatypeMono InnerDatatype
- | DatatypePoly Par InnerDatatype
data Constructor = Constructor AttrSymbol [Binding]
data Binding = Binding Symbol Type
data LetDecl = LetDecl Symbol Expr
data Type
- = TyVar Symbol
- | TyApp Symbol [Type]
- | ArrowTy [Type]
- | IntTy
- | RealTy
- | BoolTy
data Expr
- = Var PolySymbol
- | App Head [Expr]
- | Match Expr [Case]
- | Let [LetDecl] Expr
- | Binder Binder [Binding] Expr
- | Lit Lit
data Lit
- = LitInt Integer
- | LitNegInt Integer
- | LitTrue
- | LitFalse
data Binder
- = Lambda
- | Forall
- | Exists
data Case = Case Pattern Expr
data Pattern
- = Default
- | ConPat Symbol [Symbol]
- | SimplePat Symbol
- | LitPat Lit
data Head
- = Const PolySymbol
- | At
- | IfThenElse
- | And
- | Or
- | Not
- | Implies
- | Equal
- | Distinct
- | NumAdd
- | NumSub
- | NumMul
- | NumDiv
- | IntDiv
- | IntMod
- | NumGt
- | NumGe
- | NumLt
- | NumLe
- | NumWiden
data PolySymbol
- = NoAs Symbol
- | As Symbol [Type]
data AttrSymbol = AttrSymbol Symbol [Attr]
data Attr
- = NoValue Keyword
- | Value Keyword Symbol
data Symbol
- = Unquoted UnquotedSymbol
- | Quoted QuotedSymbol
newtype UnquotedSymbol = UnquotedSymbol ((Int, Int), String)
newtype QuotedSymbol = QuotedSymbol ((Int, Int), String)
newtype Keyword = Keyword String
type BNFC'Position = Maybe (Int, Int)
pattern BNFC'NoPosition :: BNFC'Position
pattern BNFC'Position :: Int -> Int -> BNFC'Position
class HasPosition a where
- hasPosition :: a -> BNFC'Position

Documentation

data Start Source #

Constructors

Start [Decl]

Instances

Instances details

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

data Decl Source #

Instances

Instances details

Eq Decl Source #
Instance details Defined in TIP.AbsTIP Methods (==) :: Decl -> Decl -> Bool (/=) :: Decl -> Decl -> Bool
Ord Decl Source #
Instance details Defined in TIP.AbsTIP 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
Read Decl Source #
Instance details Defined in TIP.AbsTIP Methods readsPrec :: Int -> ReadS Decl readList :: ReadS [Decl] readPrec :: ReadPrec Decl readListPrec :: ReadPrec [Decl]
Show Decl Source #
Instance details Defined in TIP.AbsTIP Methods showsPrec :: Int -> Decl -> ShowS show :: Decl -> String showList :: [Decl] -> ShowS
Print Decl Source #
Instance details Defined in TIP.PrintTIP Methods prt :: Int -> Decl -> Doc Source #
Print [Decl] Source #
Instance details Defined in TIP.PrintTIP Methods prt :: Int -> [Decl] -> Doc Source #

data Assertion Source #

Constructors

Assert
Prove

Instances

Instances details

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

data Par Source #

Constructors

Par [Symbol]

Instances

Instances details

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

data ConstType Source #

Constructors

ConstTypeMono Type
ConstTypePoly Par Type

Instances

Instances details

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

data InnerFunType Source #

Constructors

InnerFunType [Type] Type

Instances

Instances details

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

data FunType Source #

Constructors

FunTypeMono InnerFunType
FunTypePoly Par InnerFunType

Instances

Instances details

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

data InnerFunDec Source #

Constructors

InnerFunDec [Binding] Type

Instances

Instances details

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

data FunDec Source #

Constructors

FunDecMono AttrSymbol InnerFunDec
FunDecPoly AttrSymbol Par InnerFunDec

Instances

Instances details

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

data BracketedFunDec Source #

Constructors

BracketedFunDec FunDec

Instances

Instances details

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

data DatatypeName Source #

Constructors

DatatypeName AttrSymbol Integer

Instances

Instances details

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

data InnerDatatype Source #

Constructors

InnerDatatype [Constructor]

Instances

Instances details

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

data Datatype Source #

Constructors

DatatypeMono InnerDatatype
DatatypePoly Par InnerDatatype

Instances

Instances details

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

data Constructor Source #

Constructors

Constructor AttrSymbol [Binding]

Instances

Instances details

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

data Binding Source #

Constructors

Binding Symbol Type

Instances

Instances details

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

data LetDecl Source #

Constructors

LetDecl Symbol Expr

Instances

Instances details

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

data Type Source #

Constructors

TyVar Symbol
TyApp Symbol [Type]
ArrowTy [Type]
IntTy
RealTy
BoolTy

Instances

Instances details

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

data Expr Source #

Constructors

Var PolySymbol
App Head [Expr]
Match Expr [Case]
Let [LetDecl] Expr
Binder Binder [Binding] Expr
Lit Lit

Instances

Instances details

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

data Lit Source #

Constructors

LitInt Integer
LitNegInt Integer
LitTrue
LitFalse

Instances

Instances details

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

data Binder Source #

Constructors

Lambda
Forall
Exists

Instances

Instances details

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

data Case Source #

Constructors

Case Pattern Expr

Instances

Instances details

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

data Pattern Source #

Constructors

Default
ConPat Symbol [Symbol]
SimplePat Symbol
LitPat Lit

Instances

Instances details

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

data Head Source #

Constructors

Const PolySymbol
At
IfThenElse
And
Or
Not
Implies
Equal
Distinct
NumAdd
NumSub
NumMul
NumDiv
IntDiv
IntMod
NumGt
NumGe
NumLt
NumLe
NumWiden

Instances

Instances details

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

data PolySymbol Source #

Constructors

NoAs Symbol
As Symbol [Type]

Instances

Instances details

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

data AttrSymbol Source #

Constructors

AttrSymbol Symbol [Attr]

Instances

Instances details

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

data Attr Source #

Constructors

NoValue Keyword
Value Keyword Symbol

Instances

Instances details

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

data Symbol Source #

Constructors

Unquoted UnquotedSymbol
Quoted QuotedSymbol

Instances

Instances details

Eq Symbol Source #
Instance details Defined in TIP.AbsTIP Methods (==) :: Symbol -> Symbol -> Bool (/=) :: Symbol -> Symbol -> Bool
Ord Symbol Source #
Instance details Defined in TIP.AbsTIP 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
Read Symbol Source #
Instance details Defined in TIP.AbsTIP Methods readsPrec :: Int -> ReadS Symbol readList :: ReadS [Symbol] readPrec :: ReadPrec Symbol readListPrec :: ReadPrec [Symbol]
Show Symbol Source #
Instance details Defined in TIP.AbsTIP Methods showsPrec :: Int -> Symbol -> ShowS show :: Symbol -> String showList :: [Symbol] -> ShowS
Print Symbol Source #
Instance details Defined in TIP.PrintTIP Methods prt :: Int -> Symbol -> Doc Source #
Print [Symbol] Source #
Instance details Defined in TIP.PrintTIP Methods prt :: Int -> [Symbol] -> Doc Source #

newtype UnquotedSymbol Source #

Constructors

UnquotedSymbol ((Int, Int), String)

Instances

Instances details

Eq UnquotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods (==) :: UnquotedSymbol -> UnquotedSymbol -> Bool (/=) :: UnquotedSymbol -> UnquotedSymbol -> Bool
Ord UnquotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods compare :: UnquotedSymbol -> UnquotedSymbol -> Ordering (<) :: UnquotedSymbol -> UnquotedSymbol -> Bool (<=) :: UnquotedSymbol -> UnquotedSymbol -> Bool (>) :: UnquotedSymbol -> UnquotedSymbol -> Bool (>=) :: UnquotedSymbol -> UnquotedSymbol -> Bool max :: UnquotedSymbol -> UnquotedSymbol -> UnquotedSymbol min :: UnquotedSymbol -> UnquotedSymbol -> UnquotedSymbol
Read UnquotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods readsPrec :: Int -> ReadS UnquotedSymbol readList :: ReadS [UnquotedSymbol] readPrec :: ReadPrec UnquotedSymbol readListPrec :: ReadPrec [UnquotedSymbol]
Show UnquotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods showsPrec :: Int -> UnquotedSymbol -> ShowS show :: UnquotedSymbol -> String showList :: [UnquotedSymbol] -> ShowS
HasPosition UnquotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods hasPosition :: UnquotedSymbol -> BNFC'Position Source #
Print UnquotedSymbol Source #
Instance details Defined in TIP.PrintTIP Methods prt :: Int -> UnquotedSymbol -> Doc Source #

newtype QuotedSymbol Source #

Constructors

QuotedSymbol ((Int, Int), String)

Instances

Instances details

Eq QuotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods (==) :: QuotedSymbol -> QuotedSymbol -> Bool (/=) :: QuotedSymbol -> QuotedSymbol -> Bool
Ord QuotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods compare :: QuotedSymbol -> QuotedSymbol -> Ordering (<) :: QuotedSymbol -> QuotedSymbol -> Bool (<=) :: QuotedSymbol -> QuotedSymbol -> Bool (>) :: QuotedSymbol -> QuotedSymbol -> Bool (>=) :: QuotedSymbol -> QuotedSymbol -> Bool max :: QuotedSymbol -> QuotedSymbol -> QuotedSymbol min :: QuotedSymbol -> QuotedSymbol -> QuotedSymbol
Read QuotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods readsPrec :: Int -> ReadS QuotedSymbol readList :: ReadS [QuotedSymbol] readPrec :: ReadPrec QuotedSymbol readListPrec :: ReadPrec [QuotedSymbol]
Show QuotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods showsPrec :: Int -> QuotedSymbol -> ShowS show :: QuotedSymbol -> String showList :: [QuotedSymbol] -> ShowS
HasPosition QuotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods hasPosition :: QuotedSymbol -> BNFC'Position Source #
Print QuotedSymbol Source #
Instance details Defined in TIP.PrintTIP Methods prt :: Int -> QuotedSymbol -> Doc Source #

newtype Keyword Source #

Constructors

Keyword String

Instances

Instances details

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

type BNFC'Position = Maybe (Int, Int) Source #

Start position (line, column) of something.

pattern BNFC'NoPosition :: BNFC'Position Source #

pattern BNFC'Position :: Int -> Int -> BNFC'Position Source #

class HasPosition a where Source #

Get the start position of something.

Methods

hasPosition :: a -> BNFC'Position Source #

Instances

Instances details

HasPosition QuotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods hasPosition :: QuotedSymbol -> BNFC'Position Source #
HasPosition UnquotedSymbol Source #
Instance details Defined in TIP.AbsTIP Methods hasPosition :: UnquotedSymbol -> BNFC'Position Source #

DeclareDatatype AttrSymbol Datatype
DeclareDatatypes [DatatypeName] [Datatype]
DeclareSort AttrSymbol Integer
DeclareConst AttrSymbol ConstType
DeclareFun AttrSymbol FunType
DefineFun FunDec Expr
DefineFunRec FunDec Expr
DefineFunsRec [BracketedFunDec] [Expr]
Formula Assertion [Attr] Expr
FormulaPar Assertion [Attr] Par Expr