ddc-source-tetra-0.4.3.1: Disciplined Disciple Compiler source language.

Safe HaskellSafe
LanguageHaskell98

DDC.Source.Tetra.Exp.Compounds

Contents

Description

Utilities for constructing and destructing Source Tetra expressions.

Synopsis

Documentation

takeAnnotOfExp :: GExp l -> Maybe (GXAnnot l) Source #

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

Binds

bindOfBindMT :: GXBindVarMT l -> GXBindVar l Source #

Take the GBind of a GBindMT

takeTypeOfBindMT :: GXBindVarMT l -> Maybe (GType l) Source #

Take the type of a GBindMT.

Types

Type Applications

makeTApps :: GType l -> [GType l] -> GType l #

Construct a sequence of type applications.

takeTApps :: GType l -> [GType l] #

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

Sum Types

makeTBot :: GType l -> GType l Source #

Make an empty union type of the given kind.

Function Types

makeTFun :: GType l -> GType l -> GType l infixr 9 #

Construct a function type with the given parameter and result type.

makeTFuns :: [GType l] -> GType l -> GType l #

Like makeFun but taking a list of parameter types.

makeTFuns' :: [GType l] -> Maybe (GType l) #

Like makeTFuns but taking the parameter and return types as a list.

(~>) :: GType l -> GType l -> GType l infixr 9 #

takeTFun :: GType l -> Maybe (GType l, GType l) #

Destruct a function type into its parameter and result types, returning Nothing if this isn't a function type.

takeTFuns :: GType l -> ([GType l], GType l) #

Destruct a function type into into all its parameters and result type, returning an empty parameter list if this isn't a function type.

takeTFuns' :: GType l -> [GType l] #

Like takeFuns, but yield the parameter and return types in the same list.

Forall Types

makeTForall :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l #

Construct a forall quantified type using an anonymous binder.

makeTForalls :: Anon l => l -> [GType l] -> ([GType l] -> GType l) -> GType l #

Construct a forall quantified type using some anonymous binders.

takeTForall :: GType l -> Maybe (GType l, GTBindVar l, GType l) #

Destruct a forall quantified type, if this is one.

The kind we return comes from the abstraction rather than the Forall constructor.

Exists Types

makeTExists :: Anon l => l -> GType l -> (GType l -> GType l) -> GType l #

Construct an exists quantified type using an anonymous binder.

takeTExists :: GType l -> Maybe (GType l, GTBindVar l, GType l) #

Destruct an exists quantified type, if this is one.

The kind we return comes from the abstraction rather than the Exists constructor.

Union types

takeTUnion :: GType l -> Maybe (GType l, GType l, GType l) #

Take the kind, left and right types from a union type.

makeTUnions :: GType l -> [GType l] -> GType l #

Make a union type from a kind and list of component types.

takeTUnions :: Eq (GType l) => GType l -> Maybe (GType l, [GType l]) #

Split a union type into its components. If this is not a union, or is an ill kinded union then Nothing.

splitTUnionsOfKind :: Eq (GType l) => GType l -> GType l -> Maybe [GType l] #

Split a union of the given kind into its components. When we split a sum we need to check that the kind attached to the sum type constructor is the one that we were expecting, otherwise we risk splitting ill-kinded sums without noticing it.

Terms

Lambdas

makeXLAMs :: [GXBindVarMT l] -> GExp l -> GExp l Source #

Make some nested type lambdas.

makeXLams :: [GXBindVarMT l] -> GExp l -> GExp l Source #

Make some nested value or witness lambdas.

makeXLamFlags :: [(Bool, GXBindVarMT l)] -> GExp l -> GExp l Source #

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 ([GXBindVarMT l], GExp l) Source #

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

takeXLams :: GExp l -> Maybe ([GXBindVarMT l], GExp l) Source #

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

takeXLamFlags :: GExp l -> Maybe ([(Bool, GXBindVarMT l)], GExp l) 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

makeXApps :: GExp l -> [GExp l] -> GExp l Source #

Build sequence of value applications.

makeXAppsWithAnnots :: GExp l -> [(GExp l, Maybe (GXAnnot l))] -> GExp l Source #

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

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

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

takeXAppsWithAnnots :: GExp l -> (GExp l, [(GExp l, Maybe (GXAnnot l))]) Source #

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

takeXConApps :: GExp l -> Maybe (DaCon (GXBoundCon l) (GType l), [GExp l]) 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 :: GExp l -> Maybe (GXPrim l, [GExp l]) Source #

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

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

Clauses

bindOfClause :: GClause l -> GXBindVar l Source #

Take the binding variable of a clause.

Casts

pattern XRun :: forall t. GExp t -> GExp t Source #

pattern XBox :: forall t. GExp t -> GExp t Source #

Data Constructors

dcUnit :: DaCon n t #

The unit data constructor.

takeNameOfDaCon :: DaCon n t -> Maybe n #

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

takeTypeOfDaCon :: DaCon n (Type 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.

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.