Documentation

Type environment/context

Kind environment/context

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

Solve given equations and return all non-absurd solutions

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.

Get constraint equations

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

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.

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

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

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

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 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.

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

Abstract a term over a list of term and type variables

Abstract a term over a list of term variables

Abstract a term over a list of type variables

Apply a list of types and terms to a term

Apply a list of terms to a term

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

Create a vector of supplied elements

Append elements to the supplied vector

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

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

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.

Determines whether given type is an (alias of en) Enable line.

Determines whether given type is an (alias of en) Clock or Reset line

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

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 literal type (Symbol or Nat), and subsequently extract its String representation

Determine whether we should split away types from a product type, i.e. clocks should always be separate arguments, and not part of a product.

Worker of shouldSplit, works on TypeView instead of Type

Potentially split apart a list of function argument types. e.g. given:

[Int,(Clock,(Reset,Bool)),Char]

we return

[Int,Clock,Reset,Bool,Char]

But we would leave

[Int, (Bool,Int), Char]

unchanged.

Strip implicit parameter wrappers (IP)

Do an inverse topological sorting of the let-bindings in a let-expression