Safe Haskell	None
Language	Haskell2010

Tip.Types

Contents

Other views of theories

Description

the abstract syntax

Synopsis

Documentation

data Head a Source

Constructors

Gbl (Global a)
Builtin Builtin

Instances

Functor Head Source
Foldable Head Source
Traversable Head Source
Eq a => Eq (Head a) Source
Ord a => Ord (Head a) Source
Show a => Show (Head a) Source
TransformBi (Head a) (Expr a) Source
TransformBi (Head a) (Theory a) Source

data Local a Source

Constructors

Local
Fields lcl_name :: a lcl_type :: Type a

Instances

Functor Local Source
Foldable Local Source
Traversable Local Source
Monad m => TransformBiM m (Local a) (Expr a) Source
Eq a => Eq (Local a) Source
Ord a => Ord (Local a) Source
Show a => Show (Local a) Source
UniverseBi (Theory a) (Local a) Source
UniverseBi (Expr a) (Local a) Source
TransformBi (Local a) (Expr a) Source

data Global a Source

Constructors

Global
Fields gbl_name :: a gbl_type :: PolyType a gbl_args :: [Type a]

Instances

Functor Global Source
Foldable Global Source
Traversable Global Source
Eq a => Eq (Global a) Source
Ord a => Ord (Global a) Source
Show a => Show (Global a) Source
UniverseBi (Theory a) (Global a) Source
UniverseBi (Function a) (Global a) Source
UniverseBi (Expr a) (Global a) Source
TransformBi (Global a) (Theory a) Source

data Expr a Source

Constructors

(Head a) :@: [Expr a] infix 5	Function application: always perfectly saturated. Lambdas and locals are applied with `At` as head.
Lcl (Local a)
Lam [Local a] (Expr a)
Match (Expr a) [Case a]	The default case comes first if there is one
Let (Local a) (Expr a) (Expr a)	`Let (Local x t) b e` = `(let ((l x)) b e)` Unlike SMT-LIB, this does not accept a list of bound variable-/expression-pairs. Fix?
Quant QuantInfo Quant [Local a] (Expr a)

Instances

Functor Expr Source
Foldable Expr Source
Traversable Expr Source
TransformBi a (Expr a) Source
Monad m => TransformBiM m (Expr a) (Formula a) Source
Monad m => TransformBiM m (Expr a) (Theory a) Source
Monad m => TransformBiM m (Local a) (Expr a) Source
Monad m => TransformBiM m (Pattern a) (Expr a) Source
Monad m => TransformBiM m (Expr a) (Function a) Source
Monad m => TransformBiM m (Expr a) (Expr a) Source
Eq a => Eq (Expr a) Source
Ord a => Ord (Expr a) Source
Show a => Show (Expr a) Source
UniverseBi (Theory a) (Expr a) Source
UniverseBi (Function a) (Expr a) Source
UniverseBi (Expr a) (Expr a) Source
UniverseBi (Expr a) (Pattern a) Source
UniverseBi (Expr a) (Local a) Source
UniverseBi (Expr a) (Global a) Source
TransformBi (Type a) (Expr a) Source
TransformBi (Pattern a) (Expr a) Source
TransformBi (Expr a) (Expr a) Source
TransformBi (Expr a) (Function a) Source
TransformBi (Expr a) (Theory a) Source
TransformBi (Local a) (Expr a) Source
TransformBi (Head a) (Expr a) Source

data Quant Source

Constructors

Forall
Exists

Instances

Eq Quant Source
Ord Quant Source
Show Quant Source

data QuantInfo Source

Constructors

NoInfo
QuantIH Int

Instances

Eq QuantInfo Source
Ord QuantInfo Source
Show QuantInfo Source

data Case a Source

Constructors

Case
Fields case_pat :: Pattern a case_rhs :: Expr a

Instances

Functor Case Source
Foldable Case Source
Traversable Case Source
Eq a => Eq (Case a) Source
Ord a => Ord (Case a) Source
Show a => Show (Case a) Source

data Builtin Source

Constructors

At
Lit Lit
And
Or
Not
Implies
Equal
Distinct
IntAdd
IntSub
IntMul
IntDiv
IntMod
IntGt
IntGe
IntLt
IntLe

Instances

Eq Builtin Source
Ord Builtin Source
Show Builtin Source
UniverseBi (Theory a) Builtin Source

intBuiltin :: Builtin -> Bool Source

litBuiltin :: Builtin -> Bool Source

logicalBuiltin :: Builtin -> Bool Source

data Lit Source

Constructors

Int Integer
Bool Bool
String String

Instances

Eq Lit Source
Ord Lit Source
Show Lit Source

data Pattern a Source

Patterns in branches

Constructors

Default
ConPat
Fields pat_con :: Global a pat_args :: [Local a]
LitPat Lit

Instances

Functor Pattern Source
Foldable Pattern Source
Traversable Pattern Source
Monad m => TransformBiM m (Pattern a) (Expr a) Source
Eq a => Eq (Pattern a) Source
Ord a => Ord (Pattern a) Source
Show a => Show (Pattern a) Source
UniverseBi (Expr a) (Pattern a) Source
TransformBi (Pattern a) (Expr a) Source
TransformBi (Pattern a) (Theory a) Source

data PolyType a Source

Polymorphic types

Constructors

PolyType
Fields polytype_tvs :: [a] polytype_args :: [Type a] polytype_res :: Type a

Instances

Functor PolyType Source
Foldable PolyType Source
Traversable PolyType Source
Eq a => Eq (PolyType a) Source
Ord a => Ord (PolyType a) Source
Show a => Show (PolyType a) Source

data Type a Source

Types

Constructors

TyVar a
TyCon a [Type a]
[Type a] :=>: (Type a)
BuiltinType BuiltinType

Instances

Functor Type Source
Foldable Type Source
Traversable Type Source
Monad m => TransformBiM m (Type a) (Theory a) Source
Monad m => TransformBiM m (Type a) (Type a) Source
Eq a => Eq (Type a) Source
Ord a => Ord (Type a) Source
Show a => Show (Type a) Source
UniverseBi (Theory a) (Type a) Source
UniverseBi (Datatype a) (Type a) Source
UniverseBi (Function a) (Type a) Source
UniverseBi (Type a) (Type a) Source
TransformBi (Type a) (Theory a) Source
TransformBi (Type a) (Decl a) Source
TransformBi (Type a) (Expr a) Source
TransformBi (Type a) (Type a) Source

data BuiltinType Source

Constructors

Integer
Boolean

Instances

Eq BuiltinType Source
Ord BuiltinType Source
Show BuiltinType Source

data Function a Source

Constructors

Function
Fields func_name :: a func_tvs :: [a] func_args :: [Local a] func_res :: Type a func_body :: Expr a

Instances

Functor Function Source
Foldable Function Source
Traversable Function Source
Definition Function Source
Monad m => TransformBiM m (Function a) (Theory a) Source
Monad m => TransformBiM m (Expr a) (Function a) Source
Eq a => Eq (Function a) Source
Ord a => Ord (Function a) Source
Show a => Show (Function a) Source
UniverseBi (Function a) (Expr a) Source
UniverseBi (Function a) (Global a) Source
UniverseBi (Function a) (Type a) Source
TransformBi (Expr a) (Function a) Source

data Signature a Source

Uninterpreted function

Constructors

Signature
Fields sig_name :: a sig_type :: PolyType a

Instances

Functor Signature Source
Foldable Signature Source
Traversable Signature Source
Definition Signature Source
Eq a => Eq (Signature a) Source
Ord a => Ord (Signature a) Source
Show a => Show (Signature a) Source

data Sort a Source

Uninterpreted sort

Constructors

Sort
Fields sort_name :: a sort_tvs :: [a]

Instances

Functor Sort Source
Foldable Sort Source
Traversable Sort Source
Eq a => Eq (Sort a) Source
Ord a => Ord (Sort a) Source
Show a => Show (Sort a) Source

data Datatype a Source

Data definition

Constructors

Datatype
Fields data_name :: a data_tvs :: [a] data_cons :: [Constructor a]

Instances

Functor Datatype Source
Foldable Datatype Source
Traversable Datatype Source
Definition Datatype Source
Eq a => Eq (Datatype a) Source
Ord a => Ord (Datatype a) Source
Show a => Show (Datatype a) Source
UniverseBi (Datatype a) (Type a) Source

data Constructor a Source

Constructors

Constructor
Fields con_name :: a Constructor name (e.g. `Cons`) con_discrim :: a Discriminator name (e.g. `is-Cons`) con_args :: [(a, Type a)] Argument types names of their projectors (e.g. [(`head`,a),(`tail`,List a)])

Instances

Functor Constructor Source
Foldable Constructor Source
Traversable Constructor Source
Eq a => Eq (Constructor a) Source
Ord a => Ord (Constructor a) Source
Show a => Show (Constructor a) Source
UniverseBi (Theory a) (Constructor a) Source

data Theory a Source

Constructors

Theory
Fields thy_datatypes :: [Datatype a] thy_sorts :: [Sort a] thy_sigs :: [Signature a] thy_funcs :: [Function a] thy_asserts :: [Formula a]

Instances

Functor Theory Source
Foldable Theory Source
Traversable Theory Source
Monad m => TransformBiM m (Function a) (Theory a) Source
Monad m => TransformBiM m (Type a) (Theory a) Source
Monad m => TransformBiM m (Expr a) (Theory a) Source
Eq a => Eq (Theory a) Source
Ord a => Ord (Theory a) Source
Show a => Show (Theory a) Source
Monoid (Theory a) Source
UniverseBi (Theory a) Builtin Source
UniverseBi (Theory a) (Expr a) Source
UniverseBi (Theory a) (Type a) Source
UniverseBi (Theory a) (Constructor a) Source
UniverseBi (Theory a) (Global a) Source
UniverseBi (Theory a) (Local a) Source
TransformBi (Type a) (Theory a) Source
TransformBi (Pattern a) (Theory a) Source
TransformBi (Expr a) (Theory a) Source
TransformBi (Global a) (Theory a) Source
TransformBi (Head a) (Theory a) Source

emptyTheory :: Theory a Source

joinTheories :: Theory a -> Theory a -> Theory a Source

data Formula a Source

Constructors

Formula
Fields fm_role :: Role fm_info :: Info a fm_tvs :: [a] top-level quantified type variables fm_body :: Expr a

Instances

Functor Formula Source
Foldable Formula Source
Traversable Formula Source
TransformBi a (Formula a) Source
Monad m => TransformBiM m (Expr a) (Formula a) Source
Eq a => Eq (Formula a) Source
Ord a => Ord (Formula a) Source
Show a => Show (Formula a) Source

data Info a Source

Constructors

Definition a
IH Int
Lemma Int
Projection a
DataDomain a
DataProjection a
DataDistinct a
Defunction a
UserAsserted
Unknown

Instances

Functor Info Source
Foldable Info Source
Traversable Info Source
Eq a => Eq (Info a) Source
Ord a => Ord (Info a) Source
Show a => Show (Info a) Source

data Role Source

Constructors

Assert
Prove

Instances

Eq Role Source
Ord Role Source
Show Role Source

Other views of theories

data Decl a Source

The different kinds of declarations in a Theory.

Constructors

DataDecl (Datatype a)
SortDecl (Sort a)
SigDecl (Signature a)
FuncDecl (Function a)
AssertDecl (Formula a)

Instances

Functor Decl Source
Foldable Decl Source
Traversable Decl Source
Eq a => Eq (Decl a) Source
Ord a => Ord (Decl a) Source
Show a => Show (Decl a) Source
TransformBi (Type a) (Decl a) Source

theoryDecls :: Theory a -> [Decl a] Source

Declarations in a Theory

declsToTheory :: [Decl a] -> Theory a Source

Assemble a Theory from some Declarations

declsPass :: ([Decl a] -> [Decl b]) -> Theory a -> Theory b Source

transformExpr :: (Expr a -> Expr a) -> Expr a -> Expr a Source

transformExprM :: Monad m => (Expr a -> m (Expr a)) -> Expr a -> m (Expr a) Source

transformExprIn :: TransformBi (Expr a) (f a) => (Expr a -> Expr a) -> f a -> f a Source

transformExprInM :: TransformBiM m (Expr a) (f a) => (Expr a -> m (Expr a)) -> f a -> m (f a) Source

transformType :: (Type a -> Type a) -> Type a -> Type a Source

transformTypeInExpr :: (Type a -> Type a) -> Expr a -> Expr a Source

transformTypeInDecl :: (Type a -> Type a) -> Decl a -> Decl a Source