QuickSpec.Internal.Type

This module is internal to QuickSpec.

Polymorphic types and dynamic values.

Types

class Typeable (a :: k)

The class Typeable allows a concrete representation of a type to be calculated.

Minimal complete definition

typeRep#

Instances

HasDict (Typeable k, Typeable a) (TypeRep a)

Defined in Data.Constraint

Methods

evidence :: TypeRep a -> Dict (Typeable k, Typeable a)

class Arity f where

Methods

arity :: f -> Int

Measure the arity.

type Type = Term TyCon

A (possibly polymorphic) type.

data TyCon

A type constructor.

Constructors

Arrow

The function type constructor (->).

TyCon TyCon

An ordinary Haskell type constructor.

String String

A string. Can be used to represent miscellaneous types that do not really exist in Haskell.

Instances

CoArbitrary Type

Defined in QuickSpec.Internal.Type

Methods

coarbitrary :: Type -> Gen b -> Gen b

Show TyCon

Defined in QuickSpec.Internal.Type

Methods

showsPrec :: Int -> TyCon -> ShowS

show :: TyCon -> String

showList :: [TyCon] -> ShowS

Eq TyCon

Defined in QuickSpec.Internal.Type

Methods

(==) :: TyCon -> TyCon -> Bool

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

Ord TyCon

Defined in QuickSpec.Internal.Type

Methods

compare :: TyCon -> TyCon -> Ordering

(<) :: TyCon -> TyCon -> Bool

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

(>) :: TyCon -> TyCon -> Bool

(>=) :: TyCon -> TyCon -> Bool

max :: TyCon -> TyCon -> TyCon

min :: TyCon -> TyCon -> TyCon

Pretty TyCon

Defined in QuickSpec.Internal.Type

Methods

pPrintPrec :: PrettyLevel -> Rational -> TyCon -> Doc

pPrint :: TyCon -> Doc

pPrintList :: PrettyLevel -> [TyCon] -> Doc

Apply Type

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Type -> Type -> Maybe Type

Typed Type

Defined in QuickSpec.Internal.Type

Methods

typ :: Type -> Type

otherTypesDL :: Type -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Type -> Type

PrettyTerm TyCon

Defined in QuickSpec.Internal.Type

Methods

termStyle :: TyCon -> TermStyle

Labelled TyCon

Defined in QuickSpec.Internal.Type

Methods

label :: TyCon -> Label TyCon

CoArbitrary (TermList TyCon)

Defined in QuickSpec.Internal.Type

Methods

coarbitrary :: TermList TyCon -> Gen b -> Gen b

Typed a => Has (TypeView a) Type

Defined in QuickSpec.Internal.Type

Methods

the :: TypeView a -> Type

tyCon :: Typeable a => proxy a -> TyCon

Get the outermost TyCon of a Typeable.

fromTyCon :: TyCon -> TyCon

Construct a TyCon type from a Data.Typeable TyCon.

data A

data B

data C

data D

data E

class ClassA

class ClassB

class ClassC

class ClassD

class ClassE

class ClassF

type SymA = "__polymorphic_symbol__"

A polymorphic type of kind Symbol.

typeVar :: Type

A type variable.

isTypeVar :: Type -> Bool

Check if a type is a type variable.

typeOf :: Typeable a => a -> Type

Construct a type from a Typeable.

typeRep :: Typeable (a :: k) => proxy a -> Type

Construct a type from a Typeable.

typeFromTyCon :: TyCon -> Type

Turn a TyCon into a type.

applyType :: Type -> Type -> Type

Function application for type constructors.

For example, applyType (typeRep (Proxy :: Proxy [])) (typeRep (Proxy :: Proxy Int)) == typeRep (Proxy :: Proxy [Int]).

fromTypeRep :: TypeRep -> Type

Construct a type from a TypeRep.

arrowType :: [Type] -> Type -> Type

Construct a function type.

isArrowType :: Type -> Bool

Is a given type a function type?

unpackArrow :: Type -> Maybe (Type, Type)

Decompose a function type into (argument, result).

For multiple-argument functions, unpacks one argument.

typeArgs :: Type -> [Type]

The arguments of a function type.

typeRes :: Type -> Type

The result of a function type.

typeDrop :: Int -> Type -> Type

Given the type of a function, returns the type of applying that function to n arguments. Crashes if the type does not have enough arguments.

typeArity :: Type -> Int

How many arguments does a function take?

isDictionary :: Type -> Bool

Check if a type is of the form Dict c.

getDictionary :: Type -> Maybe Type

Check if a type is of the form Dict c, and if so, return c.

splitConstrainedType :: Type -> ([Type], Type)

Split a type into constraints and normal type.

dictArity :: Type -> Int

Count how many dictionary arguments a type has.

pPrintType :: Type -> Doc

Pretty-print a type. Differs from the Pretty instance by printing type variables in lowercase.

Things that have types

class Typed a where

A class for things that have a type.

Minimal complete definition

typ, typeSubst_

Methods

typ :: a -> Type

The type.

otherTypesDL :: a -> DList Type

Types that appear elsewhere in the Typed, for example, types of subterms. Should return everything which is affected by typeSubst.

typeSubst_ :: (Var -> Builder TyCon) -> a -> a

Substitute for all type variables.

Instances

Typed Var

Defined in QuickSpec.Internal.Term

Methods

typ :: Var -> Type

otherTypesDL :: Var -> DList Type

typeSubst_ :: (Var0 -> Builder TyCon) -> Var -> Var

Typed Type

Defined in QuickSpec.Internal.Type

Methods

typ :: Type -> Type

otherTypesDL :: Type -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Type -> Type

Typed f => Typed (Term f)

Defined in QuickSpec.Internal.Term

Methods

typ :: Term f -> Type

otherTypesDL :: Term f -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Term f -> Term f

Typed a => Typed (Poly a)

Defined in QuickSpec.Internal.Type

Methods

typ :: Poly a -> Type

otherTypesDL :: Poly a -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Poly a -> Poly a

Typed a => Typed [a]

Defined in QuickSpec.Internal.Type

Methods

typ :: [a] -> Type

otherTypesDL :: [a] -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> [a] -> [a]

(Typed a, Typed b) => Typed (Either a b)

Defined in QuickSpec.Internal.Type

Methods

typ :: Either a b -> Type

otherTypesDL :: Either a b -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Either a b -> Either a b

(Typed fun1, Typed fun2) => Typed (fun1 :+: fun2)

Defined in QuickSpec.Internal.Term

Methods

typ :: (fun1 :+: fun2) -> Type

otherTypesDL :: (fun1 :+: fun2) -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> (fun1 :+: fun2) -> fun1 :+: fun2

Typed (Value f)

Defined in QuickSpec.Internal.Type

Methods

typ :: Value f -> Type

otherTypesDL :: Value f -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Value f -> Value f

(Typed a, Typed b) => Typed (a, b)

Defined in QuickSpec.Internal.Type

Methods

typ :: (a, b) -> Type

otherTypesDL :: (a, b) -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> (a, b) -> (a, b)

typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s -> a -> a

Substitute for all type variables in a Typed.

typesDL :: Typed a => a -> DList Type

All types that occur in a Typed.

tyVars :: Typed a => a -> [Var]

All type variables that occur in a Typed.

cast :: Typed a => Type -> a -> Maybe a

Cast a Typed to a target type. Succeeds if the target type is an instance of the current type.

matchType :: Type -> Type -> Maybe (Subst TyCon)

Check if the second argument is an instance of the first argument.

newtype TypeView a

A wrapper for using the Symbolic machinery on types.

Constructors

TypeView

Fields

• unTypeView :: a

Instances

Typed a => Symbolic (TypeView a)

Defined in QuickSpec.Internal.Type

Associated Types

type ConstantOf (TypeView a)

Methods

termsDL :: TypeView a -> DList (TermListOf (TypeView a))

subst_ :: (Var -> BuilderOf (TypeView a)) -> TypeView a -> TypeView a

Typed a => Has (TypeView a) Type

Defined in QuickSpec.Internal.Type

Methods

the :: TypeView a -> Type

type ConstantOf (TypeView a)

Defined in QuickSpec.Internal.Type

type ConstantOf (TypeView a) = TyCon

class Typed a => Apply a where

Typed things that support function application.

Methods

tryApply :: a -> a -> Maybe a

Apply a function to its argument.

For most instances of Typed, the type of the argument must be exactly equal to the function's argument type. If you want unification to happen, use the Typed instance of Poly.

Instances

Apply Type

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Type -> Type -> Maybe Type

(PrettyTerm f, Typed f) => Apply (Term f)

Defined in QuickSpec.Internal.Term

Methods

tryApply :: Term f -> Term f -> Maybe (Term f)

Apply a => Apply (Poly a)

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Poly a -> Poly a -> Maybe (Poly a)

Applicative f => Apply (Value f)

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Value f -> Value f -> Maybe (Value f)

apply :: Apply a => a -> a -> a infixl 9

Apply a function to its argument, crashing on failure.

For most instances of Typed, the type of the argument must be exactly equal to the function's argument type. If you want unification to happen, use the Typed instance of Poly.

canApply :: Apply a => a -> a -> Bool

Check if a function can be applied to its argument.

oneTypeVar :: Typed a => a -> a

Unify all type variables in a type.

defaultTo :: Typed a => Type -> a -> a

Replace all type variables with a particular type.

skolemiseTypeVars :: Typed a => a -> a

Make a type ground by replacing all type variables with Skolem constants.

Polymorphic types

canonicaliseType :: Typed a => a -> a

Alpha-rename type variables in a canonical way.

data Poly a

Represents a forall-quantifier over all the type variables in a type. Wrapping a term in Poly normalises the type by alpha-renaming type variables canonically.

The Apply instance for Poly does unification to handle applying a polymorphic function.

Instances

Show a => Show (Poly a)

Defined in QuickSpec.Internal.Type

Methods

showsPrec :: Int -> Poly a -> ShowS

show :: Poly a -> String

showList :: [Poly a] -> ShowS

Eq a => Eq (Poly a)

Defined in QuickSpec.Internal.Type

Methods

(==) :: Poly a -> Poly a -> Bool

(/=) :: Poly a -> Poly a -> Bool

Ord a => Ord (Poly a)

Defined in QuickSpec.Internal.Type

Methods

compare :: Poly a -> Poly a -> Ordering

(<) :: Poly a -> Poly a -> Bool

(<=) :: Poly a -> Poly a -> Bool

(>) :: Poly a -> Poly a -> Bool

(>=) :: Poly a -> Poly a -> Bool

max :: Poly a -> Poly a -> Poly a

min :: Poly a -> Poly a -> Poly a

Pretty a => Pretty (Poly a)

Defined in QuickSpec.Internal.Type

Methods

pPrintPrec :: PrettyLevel -> Rational -> Poly a -> Doc

pPrint :: Poly a -> Doc

pPrintList :: PrettyLevel -> [Poly a] -> Doc

Apply a => Apply (Poly a)

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Poly a -> Poly a -> Maybe (Poly a)

Typed a => Typed (Poly a)

Defined in QuickSpec.Internal.Type

Methods

typ :: Poly a -> Type

otherTypesDL :: Poly a -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Poly a -> Poly a

toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)

Convert an ordinary value to a dynamic value.

poly :: Typed a => a -> Poly a

Build a Poly.

unPoly :: Poly a -> a

polyTyp :: Typed a => Poly a -> Poly Type

Get the polymorphic type of a polymorphic value.

polyRename :: (Typed a, Typed b) => a -> Poly b -> b

Rename the type variables of the second argument so that they don't overlap with those of the first argument.

polyApply :: (Typed a, Typed b, Typed c) => (a -> b -> c) -> Poly a -> Poly b -> Poly c

Rename the type variables of both arguments so that they don't overlap.

polyPair :: (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)

Rename the type variables of both arguments so that they don't overlap.

polyList :: Typed a => [Poly a] -> Poly [a]

Rename the type variables of all arguments so that they don't overlap.

polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type)

Find the most general unifier of two types.

polyFunctionMgu :: Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))

Dynamic values

data Value f

Dynamic values inside an applicative functor.

For example, a value of type Value Maybe represents a Maybe something.

Instances

Show (Value f)

Defined in QuickSpec.Internal.Type

Methods

showsPrec :: Int -> Value f -> ShowS

show :: Value f -> String

showList :: [Value f] -> ShowS

Applicative f => Apply (Value f)

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Value f -> Value f -> Maybe (Value f)

Typed (Value f)

Defined in QuickSpec.Internal.Type

Methods

typ :: Value f -> Type

otherTypesDL :: Value f -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Value f -> Value f

toValue :: forall f (a :: *). Typeable a => f a -> Value f

Construct a Value.

fromValue :: forall f (a :: *). Typeable a => Value f -> Maybe (f a)

Deconstruct a Value.

valueType :: Value f -> Type

unwrap :: Value f -> Unwrapped f

Unwrap a value to get at the thing inside, with an existential type.

data Unwrapped f where

The unwrapped value. Consists of the value itself (with an existential type) and functions to wrap it up again.

Constructors

In :: f a -> Wrapper a -> Unwrapped f

data Wrapper a

Functions for re-wrapping an Unwrapped value.

Constructors

Wrapper

Fields

• wrap :: forall g. g a -> Value g

  Wrap up a value which has the same existential type as this one.

• reunwrap :: forall g. Value g -> g a

  Unwrap a value which has the same existential type as this one.

mapValue :: (forall a. f a -> g a) -> Value f -> Value g

Apply a polymorphic function to a Value.

forValue :: Value f -> (forall a. f a -> g a) -> Value g

Apply a polymorphic function to a Value.

ofValue :: (forall a. f a -> b) -> Value f -> b

Apply a polymorphic function that returns a non-Value result to a Value.

withValue :: Value f -> (forall a. f a -> b) -> b

Apply a polymorphic function that returns a non-Value result to a Value.

pairValues :: forall f g. Typeable g => (forall a b. f a -> f b -> f (g a b)) -> Value f -> Value f -> Value f

Apply a polymorphic function to a pair of Values.

wrapFunctor :: forall f g h. Typeable h => (forall a. f a -> g (h a)) -> Value f -> Value g

unwrapFunctor :: forall f g h. Typeable g => (forall a. f (g a) -> h a) -> Value f -> Value h

bringFunctor :: Functor f => Value f -> f (Value Identity)