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

Safe HaskellSafe-Inferred

DDC.Type.Collect

Description

Collecting sets of variables and constructors.

Synopsis

Documentation

freeT :: (BindStruct c, Ord n) => Env n -> c n -> Set (Bound n)Source

Collect the free Spec variables in a thing (level-1).

freeVarsT :: Ord n => KindEnv n -> Type n -> Set (Bound n)Source

Collect the free type variables in a type.

class FreeVarConT c whereSource

Methods

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

Collect the free type variables and constructors used in a thing.

Instances

collectBound :: (BindStruct c, Ord n) => c n -> Set (Bound n)Source

Collect all the bound variables in a thing, independent of whether they are free or not.

collectBinds :: (BindStruct c, Ord n) => c n -> ([Bind n], [Bind n])Source

Collect all the spec and exp binders in a thing.

data BindTree n Source

A description of the binding structure of some type or expression.

Constructors

BindDef BindWay [Bind n] [BindTree n]

An abstract binding expression.

BindUse BoundLevel (Bound n)

Use of a variable.

BindCon BoundLevel (Bound n) (Maybe (Kind n))

Use of a constructor.

Instances

Eq n => Eq (BindTree n) 
Show n => Show (BindTree n) 

data BindWay Source

Describes how a variable was bound.

Instances

Eq BindWay 
Show BindWay 

data BoundLevel Source

What level this binder is at.

Constructors

BoundSpec 
BoundExp 
BoundWit 

Instances

isBoundExpWit :: BoundLevel -> BoolSource

Check if a boundlevel is expression or witness

bindDefT :: BindStruct c => BindWay -> [Bind n] -> [c n] -> BindTree nSource

Helper for constructing the BindTree for a type binder.