quickspec-2.2: Equational laws for free!
Safe HaskellSafe-Inferred
LanguageHaskell2010

QuickSpec.Internal.Type

Description

This module is internal to QuickSpec.

Polymorphic types and dynamic values.

Synopsis

Types

class Typeable (a :: k) #

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

Minimal complete definition

typeRep#

Instances

Instances details
HasDict (Typeable k, Typeable a) (TypeRep a) 
Instance details

Defined in Data.Constraint

Methods

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

class Arity f where Source #

Methods

arity :: f -> Int Source #

Measure the arity.

type Type = Term TyCon Source #

A (possibly polymorphic) type.

data TyCon Source #

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

Instances details
CoArbitrary Type Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

Show TyCon Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

showsPrec :: Int -> TyCon -> ShowS #

show :: TyCon -> String #

showList :: [TyCon] -> ShowS #

Eq TyCon Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

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

Ord TyCon Source # 
Instance details

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 Source # 
Instance details

Defined in QuickSpec.Internal.Type

Apply Type Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Type -> Type -> Maybe Type Source #

Typed Type Source # 
Instance details

Defined in QuickSpec.Internal.Type

PrettyTerm TyCon Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

termStyle :: TyCon -> TermStyle #

Labelled TyCon Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

label :: TyCon -> Label TyCon #

CoArbitrary (TermList TyCon) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

Typed a => Has (TypeView a) Type Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

the :: TypeView a -> Type #

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

Get the outermost TyCon of a Typeable.

fromTyCon :: TyCon -> TyCon Source #

Construct a TyCon type from a Data.Typeable TyCon.

data A Source #

data B Source #

data C Source #

data D Source #

data E Source #

type SymA = "__polymorphic_symbol__" Source #

A polymorphic type of kind Symbol.

typeVar :: Type Source #

A type variable.

isTypeVar :: Type -> Bool Source #

Check if a type is a type variable.

typeOf :: Typeable a => a -> Type Source #

Construct a type from a Typeable.

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

Construct a type from a Typeable.

typeFromTyCon :: TyCon -> Type Source #

Turn a TyCon into a type.

applyType :: Type -> Type -> Type Source #

Function application for type constructors.

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

fromTypeRep :: TypeRep -> Type Source #

Construct a type from a TypeRep.

arrowType :: [Type] -> Type -> Type Source #

Construct a function type.

isArrowType :: Type -> Bool Source #

Is a given type a function type?

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

Decompose a function type into (argument, result).

For multiple-argument functions, unpacks one argument.

typeArgs :: Type -> [Type] Source #

The arguments of a function type.

typeRes :: Type -> Type Source #

The result of a function type.

typeDrop :: Int -> Type -> Type Source #

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 Source #

How many arguments does a function take?

isDictionary :: Type -> Bool Source #

Check if a type is of the form Dict c.

getDictionary :: Type -> Maybe Type Source #

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

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

Split a type into constraints and normal type.

dictArity :: Type -> Int Source #

Count how many dictionary arguments a type has.

pPrintType :: Type -> Doc Source #

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

Things that have types

class Typed a where Source #

A class for things that have a type.

Minimal complete definition

typ, typeSubst_

Methods

typ :: a -> Type Source #

The type.

otherTypesDL :: a -> DList Type Source #

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 Source #

Substitute for all type variables.

Instances

Instances details
Typed Var Source # 
Instance details

Defined in QuickSpec.Internal.Term

Typed Type Source # 
Instance details

Defined in QuickSpec.Internal.Type

Typed f => Typed (Term f) Source # 
Instance details

Defined in QuickSpec.Internal.Term

Typed a => Typed (Poly a) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Typed a => Typed [a] Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

typ :: [a] -> Type Source #

otherTypesDL :: [a] -> DList Type Source #

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

(Typed a, Typed b) => Typed (Either a b) Source # 
Instance details

Defined in QuickSpec.Internal.Type

(Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) Source # 
Instance details

Defined in QuickSpec.Internal.Term

Methods

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

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

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

Typed (Value f) Source # 
Instance details

Defined in QuickSpec.Internal.Type

(Typed a, Typed b) => Typed (a, b) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

typ :: (a, b) -> Type Source #

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

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

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

Substitute for all type variables in a Typed.

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

All types that occur in a Typed.

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

All type variables that occur in a Typed.

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

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) Source #

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

newtype TypeView a Source #

A wrapper for using the Symbolic machinery on types.

Constructors

TypeView 

Fields

Instances

Instances details
Typed a => Symbolic (TypeView a) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Associated Types

type ConstantOf (TypeView a) #

Typed a => Has (TypeView a) Type Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

the :: TypeView a -> Type #

type ConstantOf (TypeView a) Source # 
Instance details

Defined in QuickSpec.Internal.Type

class Typed a => Apply a where Source #

Typed things that support function application.

Methods

tryApply :: a -> a -> Maybe a Source #

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

Instances details
Apply Type Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

tryApply :: Type -> Type -> Maybe Type Source #

(PrettyTerm f, Typed f) => Apply (Term f) Source # 
Instance details

Defined in QuickSpec.Internal.Term

Methods

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

Apply a => Apply (Poly a) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

Applicative f => Apply (Value f) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

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

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 Source #

Check if a function can be applied to its argument.

oneTypeVar :: Typed a => a -> a Source #

Unify all type variables in a type.

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

Replace all type variables with a particular type.

skolemiseTypeVars :: Typed a => a -> a Source #

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

Polymorphic types

canonicaliseType :: Typed a => a -> a Source #

Alpha-rename type variables in a canonical way.

data Poly a Source #

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

Instances details
Show a => Show (Poly a) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

showsPrec :: Int -> Poly a -> ShowS #

show :: Poly a -> String #

showList :: [Poly a] -> ShowS #

Eq a => Eq (Poly a) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

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

Ord a => Ord (Poly a) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

Typed a => Typed (Poly a) Source # 
Instance details

Defined in QuickSpec.Internal.Type

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

Convert an ordinary value to a dynamic value.

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

Build a Poly.

unPoly :: Poly a -> a Source #

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

Get the polymorphic type of a polymorphic value.

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

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 Source #

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) Source #

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

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

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

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

Find the most general unifier of two types.

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

Dynamic values

data Value f Source #

Dynamic values inside an applicative functor.

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

Instances

Instances details
Show (Value f) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

showsPrec :: Int -> Value f -> ShowS #

show :: Value f -> String #

showList :: [Value f] -> ShowS #

Applicative f => Apply (Value f) Source # 
Instance details

Defined in QuickSpec.Internal.Type

Methods

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

Typed (Value f) Source # 
Instance details

Defined in QuickSpec.Internal.Type

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

Construct a Value.

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

Deconstruct a Value.

unwrap :: Value f -> Unwrapped f Source #

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

data Unwrapped f where Source #

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 Source #

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 Source #

Apply a polymorphic function to a Value.

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

Apply a polymorphic function to a Value.

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

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

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

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 Source #

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 Source #

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