DDC.Core.Flow.Exp

Documentation

module DDC.Type.Exp

Expressions

data Exp a n

Well-typed expressions have types of kind Data.

Constructors

XAnnot a (Exp a n)

Annotation.

XVar !(Bound n)

Value variable or primitive operation.

XCon !(DaCon n (Type n))

Data constructor or literal.

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

Type abstraction (level-1).

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

Value and Witness abstraction (level-0).

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

Application.

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

Possibly recursive bindings.

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

Case branching.

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

Type cast.

XType !(Type n)

Type can appear as the argument of an application.

XWitness !(Witness a n)

Witness can appear as the argument of an application.

Instances

Deannotate Exp Exp

Methods

deannotate :: (a -> Maybe a) -> Exp a n -> Exp a n

Annotate Exp Exp

Methods

annotate :: a -> 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 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

Deannotate Cast Cast

Methods

deannotate :: (a -> Maybe a) -> Cast a n -> Cast a n

Annotate Cast Cast

Methods

annotate :: a -> 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 -> ()

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 local region variable, and witnesses to its properties.

Instances

Deannotate Lets Lets

Methods

deannotate :: (a -> Maybe a) -> Lets a n -> Lets a n

Annotate Lets Lets

Methods

annotate :: a -> Lets a n -> Lets a 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 Alt a n

Case alternatives.

Constructors

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

Instances

Deannotate Alt Alt

Methods

deannotate :: (a -> Maybe a) -> Alt a n -> Alt a n

Annotate Alt Alt

Methods

annotate :: a -> 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 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

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

Witnesses

data Witness a n

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

Constructors

WAnnot a (Witness a n)

WVar !(Bound n)

Witness variable.

WCon !(WiCon n)

Witness constructor.

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

Witness application.

WType !(Type n)

Type can appear as the argument of an application.

Instances

Deannotate Witness Witness

Methods

deannotate :: (a -> Maybe a) -> Witness a n -> Witness a n

Annotate Witness Witness

Methods

annotate :: a -> 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

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

type KindEnvF = Env Name

type TypeEnvF = Env Name

type TypeF = Type Name

type ModuleF = Module () Name

type ExpF = Exp () Name

type CastF = Cast () Name

type LetsF = Lets () Name

type AltF = Alt () Name

type PatF = Pat Name

type WitnessF = Witness () Name

type BoundF = Bound Name

type BindF = Bind Name