clash-lib-1.0.1: CAES Language for Synchronous Hardware - As a Library

Clash.Core.Util

Description

Smart constructor and destructor functions for CoreHW

Synopsis

# Documentation

Type environment/context

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 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
 Source # Instance detailsDefined in Clash.Core.Util Methods Source # Instance detailsDefined in Clash.Core.Util MethodsshowList :: [TypeEqSolution] -> ShowS #

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

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

If type is an equation, return LHS and RHS.

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

Get constraint equations

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.

Arguments

 :: HasCallStack => InScopeSet Variables in scope -> [TyVar] List of existentials to apply the substitution for -> [(TyVar, Type)] Substitutions -> [TyVar]

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.

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.

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

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

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 #

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

Does a term have a function type?

Does a term have a function or polymorphic type?

Is a term a term-abstraction?

Is a term a recursive let-binding?

Is a term a variable reference?

Is a term a datatype constructor?

Is a term a primitive?

Make variable reference out of term variable

Make a term variable out of a variable reference

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

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

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

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

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

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.

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.

Make a coercion

Make an undefined term

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