DDC.Source.Tetra.Compounds

Utilities for constructing and destructing Source Tetra expressions.

Documentation

module DDC.Type.Compounds

takeAnnotOfExp :: GExp l -> Maybe (GAnnot l)

Take the outermost annotation from an expression, or Nothing if this is an XType or XWitness without an annotation.

Lambdas

xLAMs :: GAnnot l -> [GBind l] -> GExp l -> GExp l

Make some nested type lambdas.

xLams :: GAnnot l -> [GBind l] -> GExp l -> GExp l

Make some nested value or witness lambdas.

makeXLamFlags :: GAnnot l -> [(Bool, GBind l)] -> GExp l -> GExp l

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

takeXLAMs :: GExp l -> Maybe ([GBind l], GExp l)

Split type lambdas from the front of an expression, or Nothing if there aren't any.

takeXLams :: GExp l -> Maybe ([GBind l], GExp l)

Split nested value or witness lambdas from the front of an expression, or Nothing if there aren't any.

takeXLamFlags :: GExp l -> Maybe ([(Bool, GBind l)], GExp l)

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

xApps :: GAnnot l -> GExp l -> [GExp l] -> GExp l

Build sequence of value applications.

makeXAppsWithAnnots :: GExp l -> [(GExp l, GAnnot l)] -> GExp l

Build sequence of applications. Similar to xApps but also takes list of annotations for the XApp constructors.

takeXApps :: GExp l -> Maybe (GExp l, [GExp l])

Flatten an application into the function part and its arguments.

Returns Nothing if there is no outer application.

takeXApps1 :: GExp l -> GExp l -> (GExp l, [GExp l])

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 :: GExp l -> [GExp l]

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

takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, GAnnot l)])

Destruct sequence of applications. Similar to takeXAppsAsList but also keeps annotations for later.

takeXConApps :: GExp l -> Maybe (DaCon (GName l), [GExp l])

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

Returns Nothing if the expression isn't a constructor application.

takeXPrimApps :: GExp l -> Maybe (GPrim l, [GExp l])

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

Returns Nothing if the expression isn't a primop application.

Casts

xBox :: GAnnot l -> GExp l -> GExp l

xRun :: GAnnot l -> GExp l -> GExp l

Data Constructors

dcUnit :: DaCon n

The unit data constructor.

takeNameOfDaCon :: DaCon n -> Maybe n

Take the name of data constructor, if there is one.

takeTypeOfDaCon :: DaCon n -> Maybe (Type n)

Take the type annotation of a data constructor, if we know it locally.

Patterns

bindsOfPat :: Pat n -> [Bind n]

Take the binds of a Pat.

pTrue :: (~) * (GName l) Name => GPat l

pFalse :: (~) * (GName l) Name => GPat l

Witnesses

wApp :: a -> Witness a n -> Witness a n -> Witness a n

Construct a witness application

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

Construct a sequence of witness applications

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

Take the witness from an XWitness argument, if any.

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

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

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

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.

Primitives

xErrorDefault :: (GPrim l ~ PrimVal, GName l ~ Name) => GAnnot l -> Text -> Integer -> GExp l