ddc-core-0.4.3.1: Disciplined Disciple Compiler core language and type checker.

Safe HaskellSafe
LanguageHaskell98

DDC.Type.Exp.Simple.Exp

Synopsis

Documentation

data Binder n Source #

Constructors

RNone 
RAnon 
RName !n 

Instances

Show n => Show (Binder n) Source # 

Methods

showsPrec :: Int -> Binder n -> ShowS #

show :: Binder n -> String #

showList :: [Binder n] -> ShowS #

data Bind n Source #

A variable binder with its type.

Constructors

BNone !(Type n)

A variable with no uses in the body doesn't need a name.

BAnon !(Type n)

Nameless variable on the deBruijn stack.

BName n !(Type n)

Named variable in the environment.

Instances

SpreadT Bind Source # 

Methods

spreadT :: Ord n => TypeEnv n -> Bind n -> Bind n Source #

Rename Bind Source # 

Methods

renameWith :: Ord n => Sub n -> Bind n -> Bind n Source #

SpreadX Bind Source # 

Methods

spreadX :: Ord n => Env n -> Env n -> Bind n -> Bind n Source #

SupportX Bind Source # 

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Bind n -> Support n Source #

SubstituteT Bind Source # 

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Bind n -> Bind n Source #

SubstituteTX Bind Source # 

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Bind n -> Bind n Source #

Ord n => MapBoundT Bind n Source # 

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bind n -> Bind n Source #

Show n => Show (Bind n) Source # 

Methods

showsPrec :: Int -> Bind n -> ShowS #

show :: Bind n -> String #

showList :: [Bind n] -> ShowS #

data Bound n Source #

A bound occurrence of a variable, with its type.

If variable hasn't been annotated with its real type then this can be tBot (an empty sum).

Constructors

UIx !Int

Nameless variable that should be on the deBruijn stack.

UName !n

Named variable that should be in the environment.

UPrim !n !(Type n)

Named primitive that has its type attached to it. The types of primitives must be closed.

Instances

SpreadT Bound Source # 

Methods

spreadT :: Ord n => TypeEnv n -> Bound n -> Bound n Source #

SpreadX Bound Source # 

Methods

spreadX :: Ord n => Env n -> Env n -> Bound n -> Bound n Source #

MapBoundT Bound n Source # 

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n Source #

MapBoundX Bound n Source # 

Methods

mapBoundAtDepthX :: (Int -> Bound n -> Bound n) -> Int -> Bound n -> Bound n Source #

Show n => Show (Bound n) Source # 

Methods

showsPrec :: Int -> Bound n -> ShowS #

show :: Bound n -> String #

showList :: [Bound n] -> ShowS #

data Type n Source #

A value type, kind, or sort.

We use the same data type to represent all three universes, as they have a similar algebraic structure.

Constructors

TCon !(TyCon n)

Constructor.

TVar !(Bound n)

Variable.

TAbs !(Bind n) !(Type n)

Abstraction.

TApp !(Type n) !(Type n)

Application.

TForall !(Bind n) !(Type n)

Universal Quantification.

TSum !(TypeSum n)

Least upper bound.

Instances

SpreadT Type Source # 

Methods

spreadT :: Ord n => TypeEnv n -> Type n -> Type n Source #

Rename Type Source # 

Methods

renameWith :: Ord n => Sub n -> Type n -> Type n Source #

FreeVarConT Type Source # 

Methods

freeVarConT :: Ord n => KindEnv n -> Type n -> (Set (Bound n), Set (Bound n)) Source #

SupportX Type Source # 

Methods

support :: Ord n => KindEnv n -> TypeEnv n -> Type n -> Support n Source #

SubstituteT Type Source # 

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> Type n -> Type n Source #

SubstituteTX Type Source # 

Methods

substituteWithTX :: Ord n => Type n -> Sub n -> Type n -> Type n Source #

Ord n => MapBoundT Type n Source # 

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> Type n -> Type n Source #

Show n => Show (Type n) Source # 

Methods

showsPrec :: Int -> Type n -> ShowS #

show :: Type n -> String #

showList :: [Type n] -> ShowS #

type Sort n = Type n Source #

Sorts are types at level 3.

type Kind n = Type n Source #

Kinds are types at level 2

type Region n = Type n Source #

Alias for region types.

type Effect n = Type n Source #

Alias for effect types.

type Closure n = Type n Source #

Alias for closure types.

data TypeSum n Source #

A least upper bound of several types.

We keep type sums in this normalised format instead of joining them together with a binary operator (like (+)). This makes sums easier to work with, as a given sum type often only has a single physical representation.

Constructors

TypeSumBot 

Fields

TypeSumSet 

Fields

Instances

SpreadT TypeSum Source # 

Methods

spreadT :: Ord n => TypeEnv n -> TypeSum n -> TypeSum n Source #

Rename TypeSum Source # 

Methods

renameWith :: Ord n => Sub n -> TypeSum n -> TypeSum n Source #

SubstituteT TypeSum Source # 

Methods

substituteWithT :: Ord n => Bound n -> Type n -> Set n -> BindStack n -> TypeSum n -> TypeSum n Source #

Ord n => MapBoundT TypeSum n Source # 

Methods

mapBoundAtDepthT :: (Int -> Bound n -> Bound n) -> Int -> TypeSum n -> TypeSum n Source #

Show n => Show (TypeSum n) Source # 

Methods

showsPrec :: Int -> TypeSum n -> ShowS #

show :: TypeSum n -> String #

showList :: [TypeSum n] -> ShowS #

data TypeSumVarCon n Source #

Wraps a variable or constructor that can be added the typeSumElems array.

Constructors

TypeSumVar !(Bound n) 
TypeSumCon !(Bound n) !(Kind n) 

data TyCon n Source #

Kind, type and witness constructors.

These are grouped to make it easy to determine the universe that they belong to.

Constructors

TyConSort !SoCon

(level 3) Builtin Sort constructors.

TyConKind !KiCon

(level 2) Builtin Kind constructors.

TyConWitness !TwCon

(level 1) Builtin Spec constructors for the types of witnesses.

TyConSpec !TcCon

(level 1) Builtin Spec constructors for types of other kinds.

TyConBound !(Bound n) !(Kind n)

User defined type constructor.

TyConExists !Int !(Kind n)

An existentially quantified name, with its kind. Used during type checking, but not accepted in source programs.

Instances

SpreadT TyCon Source # 

Methods

spreadT :: Ord n => TypeEnv n -> TyCon n -> TyCon n Source #

Show n => Show (TyCon n) Source # 

Methods

showsPrec :: Int -> TyCon n -> ShowS #

show :: TyCon n -> String #

showList :: [TyCon n] -> ShowS #

data SoCon Source #

Sort constructor.

Constructors

SoConProp

Sort of witness kinds.

SoConComp

Sort of computation kinds.

Instances

Eq SoCon Source # 

Methods

(==) :: SoCon -> SoCon -> Bool #

(/=) :: SoCon -> SoCon -> Bool #

Ord SoCon Source # 

Methods

compare :: SoCon -> SoCon -> Ordering #

(<) :: SoCon -> SoCon -> Bool #

(<=) :: SoCon -> SoCon -> Bool #

(>) :: SoCon -> SoCon -> Bool #

(>=) :: SoCon -> SoCon -> Bool #

max :: SoCon -> SoCon -> SoCon #

min :: SoCon -> SoCon -> SoCon #

Show SoCon Source # 

Methods

showsPrec :: Int -> SoCon -> ShowS #

show :: SoCon -> String #

showList :: [SoCon] -> ShowS #

data KiCon Source #

Kind constructor.

Constructors

KiConFun

Function kind constructor. This is only well formed when it is fully applied.

KiConWitness

Kind of witnesses.

KiConData

Kind of data values.

KiConRegion

Kind of regions.

KiConEffect

Kind of effects.

KiConClosure

Kind of closures.

Instances

Eq KiCon Source # 

Methods

(==) :: KiCon -> KiCon -> Bool #

(/=) :: KiCon -> KiCon -> Bool #

Ord KiCon Source # 

Methods

compare :: KiCon -> KiCon -> Ordering #

(<) :: KiCon -> KiCon -> Bool #

(<=) :: KiCon -> KiCon -> Bool #

(>) :: KiCon -> KiCon -> Bool #

(>=) :: KiCon -> KiCon -> Bool #

max :: KiCon -> KiCon -> KiCon #

min :: KiCon -> KiCon -> KiCon #

Show KiCon Source # 

Methods

showsPrec :: Int -> KiCon -> ShowS #

show :: KiCon -> String #

showList :: [KiCon] -> ShowS #

data TwCon Source #

Witness type constructors.

Constructors

TwConImpl 
TwConPure

Purity of some effect.

TwConConst

Constancy of some region.

TwConDeepConst

Constancy of material regions in some type

TwConMutable

Mutability of some region.

TwConDeepMutable

Mutability of material regions in some type.

TwConDistinct Int

Distinctness of some n regions

TwConDisjoint

Non-interfering effects are disjoint. Used for rewrite rules.

Instances

Eq TwCon Source # 

Methods

(==) :: TwCon -> TwCon -> Bool #

(/=) :: TwCon -> TwCon -> Bool #

Ord TwCon Source # 

Methods

compare :: TwCon -> TwCon -> Ordering #

(<) :: TwCon -> TwCon -> Bool #

(<=) :: TwCon -> TwCon -> Bool #

(>) :: TwCon -> TwCon -> Bool #

(>=) :: TwCon -> TwCon -> Bool #

max :: TwCon -> TwCon -> TwCon #

min :: TwCon -> TwCon -> TwCon #

Show TwCon Source # 

Methods

showsPrec :: Int -> TwCon -> ShowS #

show :: TwCon -> String #

showList :: [TwCon] -> ShowS #

data TcCon Source #

Other constructors at the spec level.

Constructors

TcConUnit

The unit data type constructor is baked in.

TcConFun

Pure function.

TcConSusp

A suspended computation.

TcConRead

Read of some region.

TcConHeadRead

Read the head region in a data type.

TcConDeepRead

Read of all material regions in a data type.

TcConWrite

Write of some region.

TcConDeepWrite

Write to all material regions in some data type.

TcConAlloc

Allocation into some region.

TcConDeepAlloc

Allocation into all material regions in some data type.

Instances

Eq TcCon Source # 

Methods

(==) :: TcCon -> TcCon -> Bool #

(/=) :: TcCon -> TcCon -> Bool #

Ord TcCon Source # 

Methods

compare :: TcCon -> TcCon -> Ordering #

(<) :: TcCon -> TcCon -> Bool #

(<=) :: TcCon -> TcCon -> Bool #

(>) :: TcCon -> TcCon -> Bool #

(>=) :: TcCon -> TcCon -> Bool #

max :: TcCon -> TcCon -> TcCon #

min :: TcCon -> TcCon -> TcCon #

Show TcCon Source # 

Methods

showsPrec :: Int -> TcCon -> ShowS #

show :: TcCon -> String #

showList :: [TcCon] -> ShowS #