Clash.Core.Util

Smart constructor and destructor functions for CoreHW

Documentation

type Gamma = VarEnv Type

Type environment/context

type Delta = VarEnv Kind

Kind environment/context

normalizeAdd :: (Type, Type) -> Maybe (Integer, Integer, Type)

Given the left and right side of an equation, normalize it such that equations of the following forms:

• 5 ~ n + 2
• 5 ~ 2 + n
• n + 2 ~ 5
• 2 + n ~ 5

are returned as (5, 2, n)

data TypeEqSolution

Data type that indicates what kind of solution (if any) was found

Constructors

Solution (TyVar, Type)

Solution was found. Variable equals some integer.

AbsurdSolution

A solution was found, but it involved negative naturals.

NoSolution

Given type wasn't an equation, or it was unsolvable.

Instances

Eq TypeEqSolution

Defined in Clash.Core.Util

Methods

(==) :: TypeEqSolution -> TypeEqSolution -> Bool

(/=) :: TypeEqSolution -> TypeEqSolution -> Bool

Show TypeEqSolution

Defined in Clash.Core.Util

Methods

showsPrec :: Int -> TypeEqSolution -> ShowS

show :: TypeEqSolution -> String

showList :: [TypeEqSolution] -> ShowS

catSolutions :: [TypeEqSolution] -> [(TyVar, Type)]

solveNonAbsurds :: TyConMap -> [(Type, Type)] -> [(TyVar, Type)]

Solve given equations and return all non-absurd solutions

solveEq :: TyConMap -> (Type, Type) -> [TypeEqSolution]

Solve simple equalities such as:

• a ~ 3
• 3 ~ a
• SomeType a b ~ SomeType 3 5
• SomeType 3 5 ~ SomeType a b
• SomeType a 5 ~ SomeType 3 b

solveAdd :: (Type, Type) -> TypeEqSolution

Solve equations supported by normalizeAdd. See documentation of TypeEqSolution to understand the return value.

typeEq :: TyConMap -> Type -> Maybe (Type, Type)

If type is an equation, return LHS and RHS.

altEqs :: TyConMap -> Alt -> [(Type, Type)]

Get constraint equations

isAbsurdAlt :: TyConMap -> Alt -> Bool

Tests for unreachable alternative due to types being "absurd". See isAbsurdEq for more info.

isAbsurdEq :: TyConMap -> (Type, Type) -> Bool

Determines if an "equation" obtained through altEqs or typeEq is absurd. That is, it tests if two types that are definitely not equal are asserted to be equal OR if the computation of the types yield some absurd (intermediate) result such as -1.

substGlobalsInExistentials

Arguments

:: HasCallStack

=> InScopeSet

Variables in scope

-> [TyVar]

List of existentials to apply the substitution for

-> [(TyVar, Type)]

Substitutions

-> [TyVar]

substInExistentialsList

Arguments

:: HasCallStack

=> InScopeSet

Variables in scope

-> [TyVar]

List of existentials to apply the substitution for

-> [(TyVar, Type)]

Substitutions

-> [TyVar]

Safely substitute type variables in a list of existentials. This function will account for cases where existentials shadow each other.

substInExistentials

Arguments

:: HasCallStack

=> InScopeSet

Variables in scope

-> [TyVar]

List of existentials to apply the substitution for

-> (TyVar, Type)

Substitution

-> [TyVar]

Safely substitute a type variable in a list of existentials. This function will account for cases where existentials shadow each other.

termType :: TyConMap -> Term -> Type

Determine the type of a term

collectBndrs :: Term -> ([Either Id TyVar], Term)

Split a (Type)Abstraction in the bound variables and the abstracted term

applyTypeToArgs :: Term -> TyConMap -> Type -> [Either Term Type] -> Type

Get the result type of a polymorphic function given a list of arguments

piResultTy :: TyConMap -> Type -> Type -> Type

Like piResultTyMaybe, but errors out when a type application is not valid.

Do not iterate piResultTy, because it's inefficient to substitute one variable at a time; instead use piResultTys

piResultTyMaybe :: TyConMap -> Type -> Type -> Maybe Type

Like piResultTys but for a single argument.

Do not iterate piResultTyMaybe, because it's inefficient to substitute one variable at a time; instead use piResultTys

piResultTys :: TyConMap -> Type -> [Type] -> Type

(piResultTys f_ty [ty1, ..., tyn]) give sthe type of (f ty1 .. tyn) where f :: f_ty

piResultTys is interesting because:

1. f_ty may have more foralls than there are args
2. Less obviously, it may have fewer foralls

Fore case 2. think of:

piResultTys (forall a . a) [forall b.b, Int]

This really can happen, such as situations involving undefineds type:

undefined :: forall a. a

undefined (forall b. b -> b) Int

This term should have the type (Int -> Int), but notice that there are more type args than foralls in undefineds type.

For efficiency reasons, when there are no foralls, we simply drop arrows from a function type/kind.

patIds :: Pat -> ([TyVar], [Id])

Get the list of term-binders out of a DataType pattern

patVars :: Pat -> [Var a]

mkAbstraction :: Term -> [Either Id TyVar] -> Term

Abstract a term over a list of term and type variables

mkTyLams :: Term -> [TyVar] -> Term

Abstract a term over a list of term variables

mkLams :: Term -> [Id] -> Term

Abstract a term over a list of type variables

mkApps :: Term -> [Either Term Type] -> Term

Apply a list of types and terms to a term

mkTmApps :: Term -> [Term] -> Term

Apply a list of terms to a term

mkTyApps :: Term -> [Type] -> Term

Apply a list of types to a term

mkTicks :: Term -> [TickInfo] -> Term

isFun :: TyConMap -> Term -> Bool

Does a term have a function type?

isPolyFun :: TyConMap -> Term -> Bool

Does a term have a function or polymorphic type?

isLam :: Term -> Bool

Is a term a term-abstraction?

isLet :: Term -> Bool

Is a term a recursive let-binding?

isVar :: Term -> Bool

Is a term a variable reference?

isLocalVar :: Term -> Bool

isCon :: Term -> Bool

Is a term a datatype constructor?

isPrim :: Term -> Bool

Is a term a primitive?

idToVar :: Id -> Term

Make variable reference out of term variable

varToId :: Term -> Id

Make a term variable out of a variable reference

termSize :: Term -> Word

mkVec

Arguments

:: DataCon

The Nil constructor

-> DataCon

The Cons (:>) constructor

-> Type

Element type

-> Integer

Length of the vector

-> [Term]

Elements to put in the vector

-> Term

Create a vector of supplied elements

appendToVec

Arguments

:: DataCon

The Cons (:>) constructor

-> Type

Element type

-> Term

The vector to append the elements to

-> Integer

Length of the vector

-> [Term]

Elements to append

-> Term

Append elements to the supplied vector

availableUniques :: Term -> [Unique]

extractElems

Arguments

:: Supply

Unique supply

-> InScopeSet

(Superset of) in scope variables

-> DataCon

The Cons (:>) constructor

-> Type

The element type

-> Char

Char to append to the bound variable names

-> Integer

Length of the vector

-> Term

The vector

-> (Supply, [(Term, [LetBinding])])

Create let-bindings with case-statements that select elements out of a vector. Returns both the variables to which element-selections are bound and the let-bindings

extractTElems

Arguments

:: Supply

Unique supply

-> InScopeSet

(Superset of) in scope variables

-> DataCon

The LR constructor

-> DataCon

The BR constructor

-> Type

The element type

-> Char

Char to append to the bound variable names

-> Integer

Depth of the tree

-> Term

The tree

-> (Supply, ([Term], [LetBinding]))

Create let-bindings with case-statements that select elements out of a tree. Returns both the variables to which element-selections are bound and the let-bindings

mkRTree

Arguments

:: DataCon

The LR constructor

-> DataCon

The BR constructor

-> Type

Element type

-> Integer

Depth of the tree

-> [Term]

Elements to put in the tree

-> Term

Create a vector of supplied elements

isSignalType :: TyConMap -> Type -> Bool

Determine whether a type is isomorphic to Clash.Signal.Internal.Signal

It is i.e.:

• Signal clk a
• (Signal clk a, Signal clk b)
• Vec n (Signal clk a)
• data Wrap = W (Signal clk' Int)
• etc.

This also includes BiSignals, i.e.:

• BiSignalIn High System Int
• etc.

isClockOrReset :: TyConMap -> Type -> Bool

tyNatSize :: TyConMap -> Type -> Except String Integer

mkUniqSystemTyVar :: (Supply, InScopeSet) -> (OccName, Kind) -> ((Supply, InScopeSet), TyVar)

mkUniqSystemId :: (Supply, InScopeSet) -> (OccName, Type) -> ((Supply, InScopeSet), Id)

mkUniqInternalId :: (Supply, InScopeSet) -> (OccName, Type) -> ((Supply, InScopeSet), Id)

dataConInstArgTysE :: HasCallStack => InScopeSet -> TyConMap -> DataCon -> [Type] -> Maybe [Type]

Same as dataConInstArgTys, but it tries to compute existentials too, hence the extra argument TyConMap. WARNING: It will return the types of non-existentials only

dataConInstArgTys :: DataCon -> [Type] -> Maybe [Type]

Given a DataCon and a list of types, the type variables of the DataCon type are substituted for the list of types. The argument types are returned.

The list of types should be equal to the number of type variables, otherwise Nothing is returned.

primCo :: Type -> Term

Make a coercion

undefinedTm :: Type -> Term

Make an undefined term

substArgTys :: DataCon -> [Type] -> [Type]

stripTicks :: Term -> Term

tySym :: TyConMap -> Type -> Except String String

Try to reduce an arbitrary type to a Symbol, and subsequently extract its String representation