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

Safe HaskellSafe
LanguageHaskell98

DDC.Type.Collect

Description

Collecting sets of variables and constructors.

Synopsis

Documentation

freeT :: (BindStruct c n, Ord n) => Env n -> c -> 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 where Source

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.

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

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

collectBinds :: (BindStruct c n, Ord n) => c -> ([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) Source 
Show n => Show (BindTree n) Source 

data BindWay Source

Describes how a variable was bound.

class BindStruct c n | c -> n where Source

Methods

slurpBindTree :: c -> [BindTree n] Source

Instances

data BoundLevel Source

What level this binder is at.

Constructors

BoundSpec 
BoundExp 
BoundWit 

isBoundExpWit :: BoundLevel -> Bool Source

Check if a boundlevel is expression or witness

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

Helper for constructing the BindTree for a type binder.