DDC.Core.Exp.Annot

Abstract Syntax

module DDC.Type.Exp

Expressions

data Exp a n

Well-typed expressions have types of kind Data.

Constructors

XVar !a !(Bound n)

Value variable or primitive operation.

XCon !a !(DaCon n (Type n))

Data constructor or literal.

XLAM !a !(Bind n) !(Exp a n)

Type abstraction (level-1).

XLam !a !(Bind n) !(Exp a n)

Value and Witness abstraction (level-0).

XApp !a !(Exp a n) !(Exp a n)

Application.

XLet !a !(Lets a n) !(Exp a n)

Possibly recursive bindings.

XCase !a !(Exp a n) ![Alt a n]

Case branching.

XCast !a !(Cast a n) !(Exp a n)

Type cast.

XType !a !(Type n)

Type can appear as the argument of an application.

XWitness !a !(Witness a n)

Witness can appear as the argument of an application.

Instances

Reannotate Exp

Methods

reannotate :: (a -> b) -> Exp a n -> Exp b n

reannotateM :: Monad m => (a -> m b) -> Exp a n -> m (Exp b n)

Complies Exp

Methods

compliesX :: (Ord n, Show n) => Profile n -> Env n -> Env n -> Context -> Exp a n -> CheckM a n (Set n, Set n)

SubstituteWX Exp

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Exp a n -> Exp a n

SubstituteXX Exp

Methods

substituteWithXX :: Ord n => Exp a n -> Sub n -> Exp a n -> Exp a n

SpreadX (Exp a)

Methods

spreadX :: Ord n => Env n -> Env n -> Exp a n -> Exp a n

SupportX (Exp a)

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Exp a n -> Support n

SubstituteTX (Exp a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Exp a n -> Exp a n

MapBoundX (Exp a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Exp a n -> Exp a n

(Eq a, Eq n) => Eq (Exp a n)

Methods

(==) :: Exp a n -> Exp a n -> Bool

(/=) :: Exp a n -> Exp a n -> Bool

(Show a, Show n) => Show (Exp a n)

Methods

showsPrec :: Int -> Exp a n -> ShowS

show :: Exp a n -> String

showList :: [Exp a n] -> ShowS

(NFData a, NFData n) => NFData (Exp a n)

Methods

rnf :: Exp a n -> ()

data PrettyMode (Exp a n)

data PrettyMode (Exp a n) = PrettyModeExp {

• modeExpLets :: PrettyMode (Lets a n)
• modeExpAlt :: PrettyMode (Alt a n)
• modeExpVarTypes :: Bool
• modeExpConTypes :: Bool
• modeExpUseLetCase :: Bool

}

data Lets a n

Possibly recursive bindings.

Constructors

LLet !(Bind n) !(Exp a n)

Non-recursive expression binding.

LRec ![(Bind n, Exp a n)]

Recursive binding of lambda abstractions.

LPrivate ![Bind n] !(Maybe (Type n)) ![Bind n]

Bind a private region variable, and witnesses to its properties.

Instances

Reannotate Lets

Methods

reannotate :: (a -> b) -> Lets a n -> Lets b n

reannotateM :: Monad m => (a -> m b) -> Lets a n -> m (Lets b n)

SpreadX (Lets a)

Methods

spreadX :: Ord n => Env n -> Env n -> Lets a n -> Lets a n

SupportX (Lets a)

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Lets a n -> Support n

(Eq a, Eq n) => Eq (Lets a n)

Methods

(==) :: Lets a n -> Lets a n -> Bool

(/=) :: Lets a n -> Lets a n -> Bool

(Show a, Show n) => Show (Lets a n)

Methods

showsPrec :: Int -> Lets a n -> ShowS

show :: Lets a n -> String

showList :: [Lets a n] -> ShowS

(NFData a, NFData n) => NFData (Lets a n)

Methods

rnf :: Lets a n -> ()

data PrettyMode (Lets a n)

data PrettyMode (Lets a n) = PrettyModeLets {

• modeLetsExp :: PrettyMode (Exp a n)
• modeLetsSuppressTypes :: Bool

}

data Alt a n

Case alternatives.

Constructors

AAlt !(Pat n) !(Exp a n)

Instances

Reannotate Alt

Methods

reannotate :: (a -> b) -> Alt a n -> Alt b n

reannotateM :: Monad m => (a -> m b) -> Alt a n -> m (Alt b n)

Complies Alt

Methods

compliesX :: (Ord n, Show n) => Profile n -> Env n -> Env n -> Context -> Alt a n -> CheckM a n (Set n, Set n)

SubstituteWX Alt

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Alt a n -> Alt a n

SubstituteXX Alt

Methods

substituteWithXX :: Ord n => Exp a n -> Sub n -> Alt a n -> Alt a n

SpreadX (Alt a)

Methods

spreadX :: Ord n => Env n -> Env n -> Alt a n -> Alt a n

SupportX (Alt a)

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Alt a n -> Support n

SubstituteTX (Alt a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Alt a n -> Alt a n

MapBoundX (Alt a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Alt a n -> Alt a n

(Eq a, Eq n) => Eq (Alt a n)

Methods

(==) :: Alt a n -> Alt a n -> Bool

(/=) :: Alt a n -> Alt a n -> Bool

(Show a, Show n) => Show (Alt a n)

Methods

showsPrec :: Int -> Alt a n -> ShowS

show :: Alt a n -> String

showList :: [Alt a n] -> ShowS

(NFData a, NFData n) => NFData (Alt a n)

Methods

rnf :: Alt a n -> ()

data PrettyMode (Alt a n)

data PrettyMode (Alt a n) = PrettyModeAlt {

• modeAltExp :: PrettyMode (Exp a n)

}

data Pat n

Pattern matching.

Constructors

PDefault

The default pattern always succeeds.

PData !(DaCon n (Type n)) ![Bind n]

Match a data constructor and bind its arguments.

Instances

SpreadX Pat

Methods

spreadX :: Ord n => Env n -> Env n -> Pat n -> Pat n

Eq n => Eq (Pat n)

Methods

(==) :: Pat n -> Pat n -> Bool

(/=) :: Pat n -> Pat n -> Bool

Show n => Show (Pat n)

Methods

showsPrec :: Int -> Pat n -> ShowS

show :: Pat n -> String

showList :: [Pat n] -> ShowS

NFData n => NFData (Pat n)

Methods

rnf :: Pat n -> ()

data Cast a n

Type casts.

Constructors

CastWeakenEffect !(Effect n)

Weaken the effect of an expression. The given effect is added to the effect of the body.

CastPurify !(Witness a n)

Purify the effect (action) of an expression.

CastBox

Box up a computation, capturing its effects in the S computation type.

CastRun

Run a computation, releasing its effects into the environment.

Instances

Reannotate Cast

Methods

reannotate :: (a -> b) -> Cast a n -> Cast b n

reannotateM :: Monad m => (a -> m b) -> Cast a n -> m (Cast b n)

SubstituteWX Cast

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Cast a n -> Cast a n

SubstituteXX Cast

Methods

substituteWithXX :: Ord n => Exp a n -> Sub n -> Cast a n -> Cast a n

SpreadX (Cast a)

Methods

spreadX :: Ord n => Env n -> Env n -> Cast a n -> Cast a n

SupportX (Cast a)

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Cast a n -> Support n

SubstituteTX (Cast a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Cast a n -> Cast a n

MapBoundX (Cast a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Cast a n -> Cast a n

(Eq a, Eq n) => Eq (Cast a n)

Methods

(==) :: Cast a n -> Cast a n -> Bool

(/=) :: Cast a n -> Cast a n -> Bool

(Show a, Show n) => Show (Cast a n)

Methods

showsPrec :: Int -> Cast a n -> ShowS

show :: Cast a n -> String

showList :: [Cast a n] -> ShowS

(NFData a, NFData n) => NFData (Cast a n)

Methods

rnf :: Cast a n -> ()

Witnesses

data Witness a n

When a witness exists in the program it guarantees that a certain property of the program is true.

Constructors

WVar a !(Bound n)

Witness variable.

WCon a !(WiCon n)

Witness constructor.

WApp a !(Witness a n) !(Witness a n)

Witness application.

WType a !(Type n)

Type can appear as the argument of an application.

Instances

Reannotate Witness

Methods

reannotate :: (a -> b) -> Witness a n -> Witness b n

reannotateM :: Monad m => (a -> m b) -> Witness a n -> m (Witness b n)

SubstituteWX Witness

Methods

substituteWithWX :: Ord n => Witness a n -> Sub n -> Witness a n -> Witness a n

SpreadX (Witness a)

Methods

spreadX :: Ord n => Env n -> Env n -> Witness a n -> Witness a n

SupportX (Witness a)

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Witness a n -> Support n

SubstituteTX (Witness a)

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Witness a n -> Witness a n

MapBoundX (Witness a) n

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Witness a n -> Witness a n

(Eq a, Eq n) => Eq (Witness a n)

Methods

(==) :: Witness a n -> Witness a n -> Bool

(/=) :: Witness a n -> Witness a n -> Bool

(Show a, Show n) => Show (Witness a n)

Methods

showsPrec :: Int -> Witness a n -> ShowS

show :: Witness a n -> String

showList :: [Witness a n] -> ShowS

(NFData a, NFData n) => NFData (Witness a n)

Methods

rnf :: Witness a n -> ()

Data Constructors

data DaCon n t

Data constructors.

Constructors

DaConUnit

Baked in unit data constructor.

DaConPrim

Primitive data constructor used for literals and baked-in constructors.

The type of the constructor needs to be attached to handle the case where there are too many constructors in the data type to list, like for Int literals. In this case we determine what data type it belongs to from the attached type of the data constructor.

Fields

• daConName :: !n

  Name of the data constructor.

• daConType :: !t

  Type of the data constructor.

DaConBound

Data constructor that has a data type declaration.

Fields

• daConName :: !n

  Name of the data constructor.

Instances

(Eq n, Eq t) => Eq (DaCon n t)

Methods

(==) :: DaCon n t -> DaCon n t -> Bool

(/=) :: DaCon n t -> DaCon n t -> Bool

(Show n, Show t) => Show (DaCon n t)

Methods

showsPrec :: Int -> DaCon n t -> ShowS

show :: DaCon n t -> String

showList :: [DaCon n t] -> ShowS

(NFData n, NFData t) => NFData (DaCon n t)

Methods

rnf :: DaCon n t -> ()

Witness Constructors

data WiCon n

Witness constructors.

Constructors

WiConBound !(Bound n) !(Type n)

Witness constructors defined in the environment. In the interpreter we use this to hold runtime capabilities. The attached type must be closed.

Instances

SpreadX WiCon

Methods

spreadX :: Ord n => Env n -> Env n -> WiCon n -> WiCon n

Eq n => Eq (WiCon n)

Methods

(==) :: WiCon n -> WiCon n -> Bool

(/=) :: WiCon n -> WiCon n -> Bool

Show n => Show (WiCon n)

Methods

showsPrec :: Int -> WiCon n -> ShowS

show :: WiCon n -> String

showList :: [WiCon n] -> ShowS

NFData n => NFData (WiCon n)

Methods

rnf :: WiCon n -> ()

Predicates

module DDC.Type.Exp.Simple.Predicates

Atoms

isXVar :: Exp a n -> Bool

Check whether an expression is a variable.

isXCon :: Exp a n -> Bool

Check whether an expression is a constructor.

isAtomX :: Exp a n -> Bool

Check whether an expression is a XVar or an XCon, or some type or witness atom.

isAtomW :: Witness a n -> Bool

Check whether a witness is a WVar or WCon.

Lambdas

isXLAM :: Exp a n -> Bool

Check whether an expression is a spec abstraction (level-1).

isXLam :: Exp a n -> Bool

Check whether an expression is a value or witness abstraction (level-0).

isLambdaX :: Exp a n -> Bool

Check whether an expression is a spec, value, or witness abstraction.

Applications

isXApp :: Exp a n -> Bool

Check whether an expression is an XApp.

Cast

isXCast :: Exp a n -> Bool

Check whether this is a cast expression.

isXCastBox :: Exp a n -> Bool

Check whether this is a box cast.

isXCastRun :: Exp a n -> Bool

Check whether this is a run cast.

Let bindings

isXLet :: Exp a n -> Bool

Check whether an expression is a XLet.

Patterns

isPDefault :: Pat n -> Bool

Check whether an alternative is a PDefault.

Types and Witnesses

isXType :: Exp a n -> Bool

Check whether an expression is an XType.

isXWitness :: Exp a n -> Bool

Check whether an expression is an XWitness.

Compounds

module DDC.Type.Exp.Simple.Compounds

Annotations

annotOfExp :: Exp a n -> a

Take the outermost annotation from an expression.

mapAnnotOfExp :: (a -> a) -> Exp a n -> Exp a n

Apply a function to the annotation of an expression.

Lambdas

xLAMs :: a -> [Bind n] -> Exp a n -> Exp a n

Make some nested type lambdas.

xLams :: a -> [Bind n] -> Exp a n -> Exp a n

Make some nested value or witness lambdas.

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

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)

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)

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)

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.

data Param n

Parameters of a function.

Constructors

ParamType (Bind n)

ParamValue (Bind n)

ParamBox

Instances

Show n => Show (Param n)

Methods

showsPrec :: Int -> Param n -> ShowS

show :: Param n -> String

showList :: [Param n] -> ShowS

takeXLamParam :: Exp a n -> Maybe ([Param n], Exp a n)

Take the parameters of a function.

Applications

xApps :: a -> Exp a n -> [Exp a n] -> Exp a n

Build sequence of value applications.

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

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

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

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

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]

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

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

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

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

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

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

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

Lets

xLets :: a -> [Lets a n] -> Exp a n -> Exp a n

Wrap some let-bindings around an expression.

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

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

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

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

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

Split let-bindings from the front of an expression, with annotations.

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

Take the binds of a Lets.

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

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

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

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

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

Alternatives

patOfAlt :: Alt a n -> Pat n

Take the pattern of an alternative.

takeCtorNameOfAlt :: Alt a n -> Maybe n

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

Patterns

bindsOfPat :: Pat n -> [Bind n]

Take the binds of a Pat.

Casts

makeRuns :: a -> Int -> Exp a n -> Exp a n

Wrap an expression in the given number of run casts.

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

annotOfWitness :: Witness a n -> a

Take the annotation from a witness.

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.

Types

takeXType :: Exp a n -> Maybe (Type n)

Take the type from an XType argument, if any.

Data Constructors

xUnit :: a -> Exp a n

Construct a value of unit type.

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.