Safe Haskell | Safe-Inferred |
---|

Utilities for constructing and destructing compound expressions.

For the annotated version of the AST.

- module DDC.Type.Compounds
- takeAnnotOfExp :: Exp a n -> Maybe a
- xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n
- xLams :: a -> [Bind n] -> Exp a n -> Exp a n
- makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a n
- takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n)
- takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)
- takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n)
- xApps :: a -> Exp a n -> [Exp a n] -> Exp a n
- makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a n
- takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n])
- takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n])
- takeXAppsAsList :: Exp a n -> [Exp a n]
- takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)])
- takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n])
- takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n])
- xLets :: a -> [Lets a n] -> Exp a n -> Exp a n
- xLetsAnnot :: [(Lets a n, a)] -> Exp a n -> Exp a n
- splitXLets :: Exp a n -> ([Lets a n], Exp a n)
- bindsOfLets :: Lets a n -> ([Bind n], [Bind n])
- specBindsOfLets :: Lets a n -> [Bind n]
- valwitBindsOfLets :: Lets a n -> [Bind n]
- bindsOfPat :: Pat n -> [Bind n]
- takeCtorNameOfAlt :: Alt a n -> Maybe n
- wApp :: a -> Witness a n -> Witness a n -> Witness a n
- wApps :: a -> Witness a n -> [Witness a n] -> Witness a n
- takeXWitness :: Exp a n -> Maybe (Witness a n)
- takeWAppsAsList :: Witness a n -> [Witness a n]
- takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n])
- takeXType :: Exp a n -> Maybe (Type n)
- xUnit :: a -> Exp a n
- dcUnit :: DaCon n
- mkDaConAlg :: n -> Type n -> DaCon n
- mkDaConSolid :: n -> Type n -> DaCon n
- takeNameOfDaCon :: DaCon n -> Maybe n
- typeOfDaCon :: DaCon n -> Type n

# Documentation

module DDC.Type.Compounds

# Annotations

takeAnnotOfExp :: Exp a n -> Maybe aSource

# Lambdas

makeXLamFlags :: a -> [(Bool, Bind n)] -> Exp a n -> Exp a nSource

Make some nested lambda abstractions, using a flag to indicate whether the lambda is a level-1 (True), or level-0 (False) binder.

takeXLAMs :: Exp a n -> Maybe ([Bind n], Exp a n)Source

Split type lambdas from the front of an expression,
or `Nothing`

if there aren't any.

takeXLams :: Exp a n -> Maybe ([Bind n], Exp a n)Source

Split nested value or witness lambdas from the front of an expression,
or `Nothing`

if there aren't any.

takeXLamFlags :: Exp a n -> Maybe ([(Bool, Bind n)], Exp a n)Source

Split nested lambdas from the front of an expression, with a flag indicating whether the lambda was a level-1 (True), or level-0 (False) binder.

# Applications

makeXAppsWithAnnots :: Exp a n -> [(Exp a n, a)] -> Exp a nSource

takeXApps :: Exp a n -> Maybe (Exp a n, [Exp a n])Source

Flatten an application into the function part and its arguments.

Returns `Nothing`

if there is no outer application.

takeXApps1 :: Exp a n -> Exp a n -> (Exp a n, [Exp a n])Source

Flatten an application into the function part and its arguments.

This is like `takeXApps`

above, except we know there is at least one argument.

takeXAppsAsList :: Exp a n -> [Exp a n]Source

Flatten an application into the function parts and arguments, if any.

takeXAppsWithAnnots :: Exp a n -> (Exp a n, [(Exp a n, a)])Source

Destruct sequence of applications.
Similar to `takeXAppsAsList`

but also keeps annotations for later.

takeXConApps :: Exp a n -> Maybe (DaCon n, [Exp a n])Source

Flatten an application of a data constructor into the constructor and its arguments.

Returns `Nothing`

if the expression isn't a constructor application.

takeXPrimApps :: Exp a n -> Maybe (n, [Exp a n])Source

Flatten an application of a primop into the variable and its arguments.

Returns `Nothing`

if the expression isn't a primop application.

# Lets

xLetsAnnot :: [(Lets a n, a)] -> Exp a n -> Exp a nSource

Wrap some let-bindings around an expression, with individual annotations.

splitXLets :: Exp a n -> ([Lets a n], Exp a n)Source

Split let-bindings from the front of an expression, if any.

bindsOfLets :: Lets a n -> ([Bind n], [Bind n])Source

Take the binds of a `Lets`

.

The level-1 and level-0 binders are returned separately.

specBindsOfLets :: Lets a n -> [Bind n]Source

Like `bindsOfLets`

but only take the spec (level-1) binders.

valwitBindsOfLets :: Lets a n -> [Bind n]Source

Like `bindsOfLets`

but only take the value and witness (level-0) binders.

# Patterns

bindsOfPat :: Pat n -> [Bind n]Source

Take the binds of a `Pat`

.

# Alternatives

takeCtorNameOfAlt :: Alt a n -> Maybe nSource

Take the constructor name of an alternative, if there is one.

# Witnesses

wApps :: a -> Witness a n -> [Witness a n] -> Witness a nSource

Construct a sequence of witness applications

takeXWitness :: Exp a n -> Maybe (Witness a n)Source

Take the witness from an `XWitness`

argument, if any.

takeWAppsAsList :: Witness a n -> [Witness a n]Source

Flatten an application into the function parts and arguments, if any.

takePrimWiConApps :: Witness a n -> Maybe (n, [Witness a n])Source

Flatten an application of a witness into the witness constructor name and its arguments.

Returns nothing if there is no witness constructor in head position.

# Types

# Data Constructors

mkDaConAlg :: n -> Type n -> DaCon nSource

Make an algebraic data constructor.

mkDaConSolid :: n -> Type n -> DaCon nSource

Make a non-algebraic (solid) constructor. These are used for location values in the interpreter, and for floating point literals in the main compiler.

takeNameOfDaCon :: DaCon n -> Maybe nSource

Take the name of data constructor.

typeOfDaCon :: DaCon n -> Type nSource

Take the type annotation of a data constructor.