Copyright | (C) 2012-2016 University of Twente |
---|---|

License | BSD2 (see the file LICENSE) |

Maintainer | Christiaan Baaij <christiaan.baaij@gmail.com> |

Safe Haskell | None |

Language | Haskell2010 |

Smart constructor and destructor functions for CoreHW

## Synopsis

- type Gamma = VarEnv Type
- type Delta = VarEnv Kind
- normalizeAdd :: (Type, Type) -> Maybe (Integer, Integer, Type)
- data TypeEqSolution
- = Solution (TyVar, Type)
- | AbsurdSolution
- | NoSolution

- catSolutions :: [TypeEqSolution] -> [(TyVar, Type)]
- solveNonAbsurds :: TyConMap -> [(Type, Type)] -> [(TyVar, Type)]
- solveEq :: TyConMap -> (Type, Type) -> [TypeEqSolution]
- solveAdd :: (Type, Type) -> TypeEqSolution
- typeEq :: TyConMap -> Type -> Maybe (Type, Type)
- altEqs :: TyConMap -> Alt -> [(Type, Type)]
- isAbsurdAlt :: TyConMap -> Alt -> Bool
- isAbsurdEq :: TyConMap -> (Type, Type) -> Bool
- substGlobalsInExistentials :: HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
- substInExistentialsList :: HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
- substInExistentials :: HasCallStack => InScopeSet -> [TyVar] -> (TyVar, Type) -> [TyVar]
- termType :: TyConMap -> Term -> Type
- collectBndrs :: Term -> ([Either Id TyVar], Term)
- applyTypeToArgs :: Term -> TyConMap -> Type -> [Either Term Type] -> Type
- piResultTy :: TyConMap -> Type -> Type -> Type
- piResultTyMaybe :: TyConMap -> Type -> Type -> Maybe Type
- piResultTys :: TyConMap -> Type -> [Type] -> Type
- patIds :: Pat -> ([TyVar], [Id])
- patVars :: Pat -> [Var a]
- mkAbstraction :: Term -> [Either Id TyVar] -> Term
- mkTyLams :: Term -> [TyVar] -> Term
- mkLams :: Term -> [Id] -> Term
- mkApps :: Term -> [Either Term Type] -> Term
- mkTmApps :: Term -> [Term] -> Term
- mkTyApps :: Term -> [Type] -> Term
- mkTicks :: Term -> [TickInfo] -> Term
- isFun :: TyConMap -> Term -> Bool
- isPolyFun :: TyConMap -> Term -> Bool
- isLam :: Term -> Bool
- isLet :: Term -> Bool
- isVar :: Term -> Bool
- isLocalVar :: Term -> Bool
- isCon :: Term -> Bool
- isPrim :: Term -> Bool
- idToVar :: Id -> Term
- varToId :: Term -> Id
- termSize :: Term -> Word
- mkVec :: DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
- appendToVec :: DataCon -> Type -> Term -> Integer -> [Term] -> Term
- availableUniques :: Term -> [Unique]
- extractElems :: Supply -> InScopeSet -> DataCon -> Type -> Char -> Integer -> Term -> (Supply, [(Term, [LetBinding])])
- extractTElems :: Supply -> InScopeSet -> DataCon -> DataCon -> Type -> Char -> Integer -> Term -> (Supply, ([Term], [LetBinding]))
- mkRTree :: DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
- isSignalType :: TyConMap -> Type -> Bool
- 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]
- dataConInstArgTys :: DataCon -> [Type] -> Maybe [Type]
- primCo :: Type -> Term
- undefinedTm :: Type -> Term
- substArgTys :: DataCon -> [Type] -> [Type]
- stripTicks :: Term -> Term
- tySym :: TyConMap -> Type -> Except String String

# Documentation

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

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

Defined in Clash.Core.Util (==) :: TypeEqSolution -> TypeEqSolution -> Bool # (/=) :: TypeEqSolution -> TypeEqSolution -> Bool # | |

Show TypeEqSolution Source # | |

Defined in Clash.Core.Util showsPrec :: Int -> TypeEqSolution -> ShowS # show :: TypeEqSolution -> String # showList :: [TypeEqSolution] -> ShowS # |

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

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.

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 #

:: HasCallStack | |

=> InScopeSet | Variables in scope |

-> [TyVar] | List of existentials to apply the substitution for |

-> [(TyVar, Type)] | Substitutions |

-> [TyVar] |

substInExistentialsList Source #

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

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

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:

`f_ty`

may have more foralls than there are args- 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 `undefined`

s 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 `undefined`

s type.

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

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

Abstract a term over a list of term and type variables

isLocalVar :: Term -> Bool Source #

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

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

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

:: Supply | Unique supply |

-> InScopeSet | (Superset of) in scope variables |

-> DataCon | The |

-> DataCon | The |

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

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

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

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

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

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.

undefinedTm :: Type -> Term Source #

Make an undefined term

stripTicks :: Term -> Term Source #