clash-lib-1.8.1: Clash: a functional hardware description language - As a library

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 | Safe-Inferred
Language | Haskell2010

Clash.Normalize.Transformations.Case

Description

Transformations on case-expressions

Synopsis

- caseCase :: HasCallStack => NormRewrite
- caseCon :: HasCallStack => NormRewrite
- caseElemNonReachable :: HasCallStack => NormRewrite
- caseFlat :: HasCallStack => NormRewrite
- caseLet :: HasCallStack => NormRewrite
- caseOneAlt :: Term -> NormalizeSession Term
- elimExistentials :: HasCallStack => NormRewrite

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