Copyright | (C) 2012-2016 University of Twente 2016-2017 Myrtle Software Ltd 2017-2022 Google Inc. 2021-2022 QBayLogic B.V. |
---|---|

License | BSD2 (see the file LICENSE) |

Maintainer | QBayLogic B.V. <devops@qbaylogic.com> |

Safe Haskell | None |

Language | Haskell2010 |

Transformations on case-expressions

## Synopsis

# Documentation

caseCase :: HasCallStack => NormRewrite Source #

Move a Case-decomposition from the subject of a Case-decomposition to the alternatives

caseCon :: HasCallStack => NormRewrite Source #

caseElemNonReachable :: HasCallStack => NormRewrite Source #

Remove non-reachable alternatives. For example, consider:

data STy ty where SInt :: Int -> STy Int SBool :: Bool -> STy Bool

f :: STy ty -> ty f (SInt b) = b + 1 f (SBool True) = False f (SBool False) = True {-# NOINLINE f #-}

g :: STy Int -> Int g = f

`f`

is always specialized on `STy Int`

. The SBool alternatives are therefore
unreachable. Additional information can be found at:
https://github.com/clash-lang/clash-compiler/pull/465

caseFlat :: HasCallStack => NormRewrite Source #

Flatten ridiculous case-statements generated by GHC

For case-statements in haskell of the form:

f :: Unsigned 4 -> Unsigned 4 f x = case x of 0 -> 3 1 -> 2 2 -> 1 3 -> 0

GHC generates Core that looks like:

f = (x :: Unsigned 4) -> case x == fromInteger 3 of False -> case x == fromInteger 2 of False -> case x == fromInteger 1 of False -> case x == fromInteger 0 of False -> error "incomplete case" True -> fromInteger 3 True -> fromInteger 2 True -> fromInteger 1 True -> fromInteger 0

Which would result in a priority decoder circuit where a normal decoder circuit was desired.

This transformation transforms the above Core to the saner:

f = (x :: Unsigned 4) -> case x of _ -> error "incomplete case" 0 -> fromInteger 3 1 -> fromInteger 2 2 -> fromInteger 1 3 -> fromInteger 0

caseLet :: HasCallStack => NormRewrite Source #

Lift the let-bindings out of the subject of a Case-decomposition

caseOneAlt :: Term -> NormalizeSession Term Source #

elimExistentials :: HasCallStack => NormRewrite Source #

Tries to eliminate existentials by using heuristics to determine what the existential should be. For example, consider Vec:

data Vec :: Nat -> Type -> Type where Nil :: Vec 0 a Cons x xs :: a -> Vec n a -> Vec (n + 1) a

Thus, `null`

(annotated with existentials) could look like:

null :: forall n . Vec n Bool -> Bool null v = case v of Nil {n ~ 0} -> True Cons {n1:Nat} {n~n1+1} (x :: a) (xs :: Vec n1 a) -> False

When it's applied to a vector of length 5, this becomes:

null :: Vec 5 Bool -> Bool null v = case v of Nil {5 ~ 0} -> True Cons {n1:Nat} {5~n1+1} (x :: a) (xs :: Vec n1 a) -> False

This function solves `n1`

and replaces every occurrence with its solution. A
very limited number of solutions are currently recognized: only adds (such
as in the example) will be solved.