ddc-core-0.4.1.3: Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe-Inferred

DDC.Type.Compounds

Contents

Synopsis

Binds

takeNameOfBind :: Bind n -> Maybe nSource

Take the variable name of a bind. If this is an anonymous binder then there won't be a name.

typeOfBind :: Bind n -> Type nSource

Take the type of a bind.

replaceTypeOfBind :: Type n -> Bind n -> Bind nSource

Replace the type of a bind with a new one.

Binders

binderOfBind :: Bind n -> Binder nSource

Take the binder of a bind.

makeBindFromBinder :: Binder n -> Type n -> Bind nSource

Make a bind from a binder and its type.

partitionBindsByType :: Eq n => [Bind n] -> [([Binder n], Type n)]Source

Make lists of binds that have the same type.

Bounds

takeNameOfBound :: Bound n -> Maybe nSource

Take the name of bound variable. If this is a deBruijn index then there won't be a name.

takeTypeOfBound :: Bound n -> Maybe (Type n)Source

Get the attached type of a Bound, if any.

boundMatchesBind :: Eq n => Bound n -> Bind n -> BoolSource

Check whether a bound maches a bind. UName and BName match if they have the same name. UIx 0 _ and BAnon _ always match. Yields False for other combinations of bounds and binds.

namedBoundMatchesBind :: Eq n => Bound n -> Bind n -> BoolSource

Check whether a named bound matches a named bind. Yields False if they are not named or have different names.

takeSubstBoundOfBind :: Bind n -> Maybe (Bound n)Source

Convert a Bind to a Bound, ready for substitution.

Returns UName for BName, UIx 0 for BAnon and Nothing for BNone, because there's nothing to substitute.

takeSubstBoundsOfBinds :: [Bind n] -> [Bound n]Source

Convert some Binds to Bounds

replaceTypeOfBound :: Type n -> Bound n -> Bound nSource

If this Bound is a UPrim then replace it's embedded type with a new one, otherwise return it unharmed.

Kinds

kFun :: Kind n -> Kind n -> Kind nSource

Construct a kind function.

kFuns :: [Kind n] -> Kind n -> Kind nSource

Construct some kind functions.

takeKFun :: Kind n -> Maybe (Kind n, Kind n)Source

Destruct a kind function

takeKFuns :: Kind n -> ([Kind n], Kind n)Source

Destruct a chain of kind functions into the arguments

takeKFuns' :: Kind n -> [Kind n]Source

Like takeKFuns, but return argument and return kinds in the same list.

takeResultKind :: Kind n -> Kind nSource

Take the result kind of a kind function, or return the same kind unharmed if it's not a kind function.

Quantifiers

tForall :: Kind n -> (Type n -> Type n) -> Type nSource

Build an anonymous type abstraction, with a single parameter.

tForall' :: Int -> Kind n -> (Type n -> Type n) -> Type nSource

Build an anonymous type abstraction, with a single parameter. Starting the next index from the given value.

tForalls :: [Kind n] -> ([Type n] -> Type n) -> Type nSource

Build an anonymous type abstraction, with several parameters. Starting the next index from the given value.

tForalls' :: Int -> [Kind n] -> ([Type n] -> Type n) -> Type nSource

Build an anonymous type abstraction, with several parameters. Starting the next index from the given value.

takeTForalls :: Type n -> Maybe ([Bind n], Type n)Source

Split nested foralls from the front of a type, or Nothing if there was no outer forall.

eraseTForalls :: Ord n => Type n -> Type nSource

Erase all TForall quantifiers from a type.

Sums

tBot :: Kind n -> Type nSource

Construct an empty type sum.

tSum :: Ord n => Kind n -> [Type n] -> Type nSource

Applications

tApp :: Type n -> Type n -> Type nSource

Construct a type application.

($:) :: Type n -> Type n -> Type nSource

Construct a type application.

tApps :: Type n -> [Type n] -> Type nSource

Construct a sequence of type applications.

takeTApps :: Type n -> [Type n]Source

Flatten a sequence ot type applications into the function part and arguments, if any.

takeTyConApps :: Type n -> Maybe (TyCon n, [Type n])Source

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one.

takePrimTyConApps :: Type n -> Maybe (n, [Type n])Source

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one. Only accept primitive type constructors.

takeDataTyConApps :: Type n -> Maybe (TyCon n, [Type n])Source

Flatten a sequence of type applications, returning the type constructor and arguments, if there is one. Only accept data type constructors.

takePrimeRegion :: Type n -> Maybe (Type n)Source

Take the prime region variable of a data type. This corresponds to the region the outermost constructor is allocated into.

Functions

tFun :: Type n -> Type n -> Type nSource

Construct a pure function type.

tFunOfList :: [Type n] -> Maybe (Type n)Source

Construct a pure and empty function from a list containing the parameter and return type. Yields Nothing if the list is empty.

tFunPE :: Type n -> Type n -> Type nSource

Construct a pure and empty value type function.

tFunOfListPE :: [Type n] -> Maybe (Type n)Source

Construct a pure and empty function from a list containing the parameter and return type. Yields Nothing if the list is empty.

tFunEC :: Type n -> Effect n -> Closure n -> Type n -> Type nSource

Construct a value type function, with the provided effect and closure.

takeTFun :: Type n -> Maybe (Type n, Type n)Source

Yield the argument and result type of a function type.

Works for both TcConFun and TcConFunEC.

takeTFunEC :: Type n -> Maybe (Type n, Effect n, Closure n, Type n)Source

Yield the argument and result type of a function type.

takeTFunArgResult :: Type n -> ([Type n], Type n)Source

Destruct the type of a function, returning just the argument and result types.

Works for both TcConFun and TcConFunEC.

takeTFunWitArgResult :: Type n -> ([Type n], [Type n], Type n)Source

Destruct the type of a function, returning the witness argument, value argument and result types. The function type must have the witness implications before the value arguments, eg T1 => T2 -> T3 -> T4 -> T5.

Works for both TcConFun and TcConFunEC.

takeTFunAllArgResult :: Type n -> ([Type n], Type n)Source

Destruct the type of a possibly polymorphic function returning all kinds of quantifiers, witness arguments, and value arguments in the order they appear, along with the type of the result.

arityOfType :: Type n -> IntSource

Determine the arity of an expression by looking at its type. Count all the function arrows, and foralls.

This assumes the type is in prenex form, meaning that all the quantifiers are at the front.

Suspensions

tSusp :: Effect n -> Type n -> Type nSource

Implications

tImpl :: Type n -> Type n -> Type nSource

Construct a witness implication type.

Units

Variables

tIx :: Kind n -> Int -> Type nSource

Construct a deBruijn index.

takeTExists :: Type n -> Maybe IntSource

Take an existential variable from a type.

Sort construction

Kind construction

Effect type constructors

Closure type constructors

tUse :: Type n -> Type nSource

Witness type constructors

tDistinct :: Int -> [Type n] -> Type nSource

tConData0 :: n -> Kind n -> Type nSource

Build a nullary type constructor of the given kind.

tConData1 :: n -> Kind n -> Type n -> Type nSource

Build a type constructor application of one argumnet.