Tip.Types

The abstract syntax

Documentation

data Head a

Constructors

Gbl (Global a)

Builtin Builtin

Instances

Functor Head

Foldable Head

Traversable Head

Eq a => Eq (Head a)

Ord a => Ord (Head a)

Show a => Show (Head a)

PrettyVar a => Pretty (Head a)

TransformBi (Head a) (Expr a)

TransformBi (Head a) (Theory a)

data Local a

Constructors

Local

Fields

lcl_name :: a

lcl_type :: Type a

Instances

Functor Local

Foldable Local

Traversable Local

Monad m => TransformBiM m (Local a) (Expr a)

Eq a => Eq (Local a)

Ord a => Ord (Local a)

Show a => Show (Local a)

PrettyVar a => Pretty (Local a)

UniverseBi (Expr a) (Local a)

TransformBi (Local a) (Expr a)

data Global a

Constructors

Global

Fields

gbl_name :: a

gbl_type :: PolyType a

gbl_args :: [Type a]

Instances

Functor Global

Foldable Global

Traversable Global

Eq a => Eq (Global a)

Ord a => Ord (Global a)

Show a => Show (Global a)

PrettyVar a => Pretty (Global a)

UniverseBi (Theory a) (Global a)

UniverseBi (Function a) (Global a)

UniverseBi (Expr a) (Global a)

data Expr a

Constructors

(Head a) :@: [Expr a] infix 5

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)

Quant QuantInfo Quant [Local a] (Expr a)

Instances

Functor Expr

Foldable Expr

Traversable Expr

TransformBi a (Expr a)

Monad m => TransformBiM m (Expr a) (Formula a)

Monad m => TransformBiM m (Expr a) (Theory a)

Monad m => TransformBiM m (Local a) (Expr a)

Monad m => TransformBiM m (Pattern a) (Expr a)

Monad m => TransformBiM m (Expr a) (Function a)

Monad m => TransformBiM m (Expr a) (Expr a)

Eq a => Eq (Expr a)

Ord a => Ord (Expr a)

Show a => Show (Expr a)

(Ord a, PrettyVar a) => Pretty (Expr a)

UniverseBi (Theory a) (Expr a)

UniverseBi (Function a) (Expr a)

UniverseBi (Expr a) (Expr a)

UniverseBi (Expr a) (Pattern a)

UniverseBi (Expr a) (Local a)

UniverseBi (Expr a) (Global a)

TransformBi (Type a) (Expr a)

TransformBi (Pattern a) (Expr a)

TransformBi (Expr a) (Expr a)

TransformBi (Expr a) (Function a)

TransformBi (Expr a) (Theory a)

TransformBi (Local a) (Expr a)

TransformBi (Head a) (Expr a)

data Quant

Constructors

Forall

Exists

Instances

Eq Quant

Ord Quant

Show Quant

data QuantInfo

Constructors

NoInfo

Instances

Eq QuantInfo

Ord QuantInfo

Show QuantInfo

data Case a

Constructors

Case

Fields

case_pat :: Pattern a

case_rhs :: Expr a

Instances

Functor Case

Foldable Case

Traversable Case

Eq a => Eq (Case a)

Ord a => Ord (Case a)

Show a => Show (Case a)

data Builtin

Constructors

At

Lit Lit

And

Or

Not

Implies

Equal

Distinct

IntAdd

IntSub

IntMul

IntDiv

IntMod

IntGt

IntGe

IntLt

IntLe

Instances

Eq Builtin

Ord Builtin

Show Builtin

UniverseBi (Theory a) Builtin

intBuiltin :: Builtin -> Bool

litBuiltin :: Builtin -> Bool

eqRelatedBuiltin :: Builtin -> Bool

logicalBuiltin :: Builtin -> Bool

data Lit

Constructors

Int Integer

Bool Bool

String String

Instances

Eq Lit

Ord Lit

Show Lit

data Pattern a

Patterns in branches

Constructors

Default

ConPat

Fields

pat_con :: Global a

pat_args :: [Local a]

LitPat Lit

Instances

Functor Pattern

Foldable Pattern

Traversable Pattern

Monad m => TransformBiM m (Pattern a) (Expr a)

Eq a => Eq (Pattern a)

Ord a => Ord (Pattern a)

Show a => Show (Pattern a)

PrettyVar a => Pretty (Pattern a)

UniverseBi (Expr a) (Pattern a)

TransformBi (Pattern a) (Expr a)

TransformBi (Pattern a) (Theory a)

data PolyType a

Polymorphic types

Constructors

PolyType

Fields

polytype_tvs :: [a]

polytype_args :: [Type a]

polytype_res :: Type a

Instances

Functor PolyType

Foldable PolyType

Traversable PolyType

Eq a => Eq (PolyType a)

Ord a => Ord (PolyType a)

Show a => Show (PolyType a)

PrettyVar a => Pretty (PolyType a)

data Type a

Types

Constructors

TyVar a

TyCon a [Type a]

[Type a] :=>: (Type a)

BuiltinType BuiltinType

Instances

Functor Type

Foldable Type

Traversable Type

Monad m => TransformBiM m (Type a) (Type a)

Eq a => Eq (Type a)

Ord a => Ord (Type a)

Show a => Show (Type a)

PrettyVar a => Pretty (Type a)

UniverseBi (Theory a) (Type a)

UniverseBi (Datatype a) (Type a)

UniverseBi (Function a) (Type a)

UniverseBi (Type a) (Type a)

TransformBi (Type a) (Theory a)

TransformBi (Type a) (Expr a)

TransformBi (Type a) (Type a)

data BuiltinType

Constructors

Integer

Boolean

Instances

Eq BuiltinType

Ord BuiltinType

Show BuiltinType

data Function a

Constructors

Function

Fields

func_name :: a

func_tvs :: [a]

func_args :: [Local a]

func_res :: Type a

func_body :: Expr a

Instances

Functor Function

Foldable Function

Traversable Function

Definition Function

Monad m => TransformBiM m (Function a) (Theory a)

Monad m => TransformBiM m (Expr a) (Function a)

Eq a => Eq (Function a)

Ord a => Ord (Function a)

Show a => Show (Function a)

(Ord a, PrettyVar a) => Pretty (Function a)

UniverseBi (Function a) (Expr a)

UniverseBi (Function a) (Global a)

UniverseBi (Function a) (Type a)

TransformBi (Expr a) (Function a)

data Signature a

Uninterpreted function

Constructors

Signature

Fields

sig_name :: a

sig_type :: PolyType a

Instances

Functor Signature

Foldable Signature

Traversable Signature

Definition Signature

Eq a => Eq (Signature a)

Ord a => Ord (Signature a)

Show a => Show (Signature a)

PrettyVar a => Pretty (Signature a)

data Sort a

Uninterpreted sort

Constructors

Sort

Fields

sort_name :: a

sort_arity :: Int

Instances

Functor Sort

Foldable Sort

Traversable Sort

Eq a => Eq (Sort a)

Ord a => Ord (Sort a)

Show a => Show (Sort a)

data Datatype a

Data definition

Constructors

Datatype

Fields

data_name :: a

data_tvs :: [a]

data_cons :: [Constructor a]

Instances

Functor Datatype

Foldable Datatype

Traversable Datatype

Definition Datatype

Eq a => Eq (Datatype a)

Ord a => Ord (Datatype a)

Show a => Show (Datatype a)

PrettyVar a => Pretty (Datatype a)

UniverseBi (Datatype a) (Type a)

data Constructor a

Constructors

Constructor

Fields

con_name :: a

con_discrim :: a

con_args :: [(a, Type a)]

Instances

Functor Constructor

Foldable Constructor

Traversable Constructor

Eq a => Eq (Constructor a)

Ord a => Ord (Constructor a)

Show a => Show (Constructor a)

UniverseBi (Theory a) (Constructor a)

data Theory a

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

Foldable Theory

Traversable Theory

Monad m => TransformBiM m (Function a) (Theory a)

Monad m => TransformBiM m (Expr a) (Theory a)

Eq a => Eq (Theory a)

Ord a => Ord (Theory a)

Show a => Show (Theory a)

Monoid (Theory a)

(Ord a, PrettyVar a) => Pretty (Theory a)

UniverseBi (Theory a) Builtin

UniverseBi (Theory a) (Expr a)

UniverseBi (Theory a) (Type a)

UniverseBi (Theory a) (Constructor a)

UniverseBi (Theory a) (Global a)

TransformBi (Type a) (Theory a)

TransformBi (Pattern a) (Theory a)

TransformBi (Expr a) (Theory a)

TransformBi (Head a) (Theory a)

emptyTheory :: Theory a

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

data Formula a

Constructors

Formula

Fields

fm_role :: Role

fm_tvs :: [a]

top-level quantified type variables

fm_body :: Expr a

Instances

Functor Formula

Foldable Formula

Traversable Formula

TransformBi a (Formula a)

Monad m => TransformBiM m (Expr a) (Formula a)

Eq a => Eq (Formula a)

Ord a => Ord (Formula a)

Show a => Show (Formula a)

(Ord a, PrettyVar a) => Pretty (Formula a)

data Role

Constructors

Assert

Prove

Instances

Eq Role

Ord Role

Show Role

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

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

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

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

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

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