clash-lib-0.9999: CAES Language for Synchronous Hardware - As a Library
Copyright(C) 2012-2016 University of Twente
LicenseBSD2 (see the file LICENSE)
MaintainerChristiaan Baaij <christiaan.baaij@gmail.com>
Safe HaskellNone
LanguageHaskell2010

Clash.Core.Util

Description

Smart constructor and destructor functions for CoreHW

Synopsis

Documentation

type Gamma = VarEnv Type Source #

Type environment/context

type Delta = VarEnv Kind Source #

Kind environment/context

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

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 Source #

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

Instances details
Eq TypeEqSolution Source # 
Instance details

Defined in Clash.Core.Util

Show TypeEqSolution Source # 
Instance details

Defined in Clash.Core.Util

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

Solve given equations and return all non-absurd solutions

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

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 Source #

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

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

If type is an equation, return LHS and RHS.

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

Get constraint equations

isAbsurdAlt :: TyConMap -> Alt -> Bool Source #

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

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

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 Source #

Arguments

:: HasCallStack 
=> InScopeSet

Variables in scope

-> [TyVar]

List of existentials to apply the substitution for

-> [(TyVar, Type)]

Substitutions

-> [TyVar] 

substInExistentialsList Source #

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 Source #

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 Source #

Determine the type of a term

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

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

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

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

piResultTy :: TyConMap -> Type -> Type -> Type Source #

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 Source #

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 Source #

(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]) Source #

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

patVars :: Pat -> [Var a] Source #

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

Abstract a term over a list of term and type variables

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

Abstract a term over a list of term variables

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

Abstract a term over a list of type variables

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

Apply a list of types and terms to a term

mkTmApps :: Term -> [Term] -> Term Source #

Apply a list of terms to a term

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

Apply a list of types to a term

isFun :: TyConMap -> Term -> Bool Source #

Does a term have a function type?

isPolyFun :: TyConMap -> Term -> Bool Source #

Does a term have a function or polymorphic type?

isLam :: Term -> Bool Source #

Is a term a term-abstraction?

isLet :: Term -> Bool Source #

Is a term a recursive let-binding?

isVar :: Term -> Bool Source #

Is a term a variable reference?

isCon :: Term -> Bool Source #

Is a term a datatype constructor?

isPrim :: Term -> Bool Source #

Is a term a primitive?

idToVar :: Id -> Term Source #

Make variable reference out of term variable

varToId :: Term -> Id Source #

Make a term variable out of a variable reference

mkVec Source #

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 Source #

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

extractElems Source #

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 Source #

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 Source #

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 Source #

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.

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

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] Source #

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 Source #

Make a coercion

undefinedTm :: Type -> Term Source #

Make an undefined term

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

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