{-|
  Copyright   :  (C) 2012-2016, University of Twente,
                     2021-2023, QBayLogic B.V.,
                     2022     , Google Inc.
  License     :  BSD2 (see the file LICENSE)
  Maintainer  :  QBayLogic B.V. <devops@qbaylogic.com>

  Smart constructor and destructor functions for CoreHW
-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TemplateHaskell #-}

module Clash.Core.Util where

import           Control.Concurrent.Supply     (Supply, freshId)
import Control.Monad.Trans.Except              (Except, throwE, runExcept)
import Data.Bifunctor                          (first, second)
import qualified Data.HashSet                  as HashSet
import qualified Data.Graph                    as Graph
import Data.List                               (mapAccumR, uncons)
import Data.List.Extra                         (zipEqual)
import Data.List.NonEmpty                      (NonEmpty (..), toList)
import Data.Maybe
  (fromMaybe, isJust, mapMaybe, catMaybes)
import qualified Data.Set                      as Set
import qualified Data.Set.Lens                 as Lens
import qualified Data.Text                     as T
import           GHC.Stack                     (HasCallStack)

#if MIN_VERSION_ghc(9,0,0)
import           GHC.Builtin.Names       (ipClassKey)
import           GHC.Types.Unique        (getKey)
#else
import           PrelNames               (ipClassKey)
import           Unique                  (getKey)
#endif

import Clash.Core.DataCon
import Clash.Core.EqSolver
import Clash.Core.FreeVars               (freeLocalIds)
import Clash.Core.HasFreeVars
import Clash.Core.HasType
import Clash.Core.Name
  (Name (..), OccName, mkUnsafeInternalName, mkUnsafeSystemName)
import Clash.Core.Pretty                 (showPpr)
import Clash.Core.Subst
import Clash.Core.Term
import Clash.Core.TyCon                  (TyConMap, tyConDataCons)
import Clash.Core.Type
import Clash.Core.TysPrim                (liftedTypeKind, typeNatKind)
import Clash.Core.Var                    (Id, Var(..), mkLocalId, mkTyVar)
import Clash.Core.VarEnv
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Debug                       (traceIf)
import Clash.Util

-- | Rebuild a let expression / let expressions by taking the SCCs of a list
-- of bindings and remaking Let (NonRec ...) ... and Let (Rec ...) ...
--
listToLets :: [LetBinding] -> Term -> Term
listToLets :: [LetBinding] -> Term -> Term
listToLets [LetBinding]
xs Term
body = (SCC LetBinding -> Term -> Term)
-> Term -> [SCC LetBinding] -> Term
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SCC LetBinding -> Term -> Term
go Term
body (HasCallStack => [LetBinding] -> [SCC LetBinding]
[LetBinding] -> [SCC LetBinding]
sccLetBindings [LetBinding]
xs)
 where
  go :: SCC LetBinding -> Term -> Term
go (Graph.AcyclicSCC (Id
i, Term
x)) Term
acc = Bind Term -> Term -> Term
Let (Id -> Term -> Bind Term
forall a. Id -> a -> Bind a
NonRec Id
i Term
x) Term
acc
  go (Graph.CyclicSCC [LetBinding]
binds) Term
acc = Bind Term -> Term -> Term
Let ([LetBinding] -> Bind Term
forall a. [(Id, a)] -> Bind a
Rec [LetBinding]
binds) Term
acc

-- | The type @forall a . a@
undefinedTy ::Type
undefinedTy :: Type
undefinedTy =
  let aNm :: Name a
aNm = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"a" Unique
0
      aTv :: Var a
aTv = (Name a -> Unique -> Type -> Var a
forall a. Name a -> Unique -> Type -> Var a
TyVar Name a
forall a. Name a
aNm Unique
0 Type
liftedTypeKind)
  in  TyVar -> Type -> Type
ForAllTy TyVar
forall a. Var a
aTv (TyVar -> Type
VarTy TyVar
forall a. Var a
aTv)

-- | The type @forall a. forall b. a -> b@
unsafeCoerceTy :: Type
unsafeCoerceTy :: Type
unsafeCoerceTy =
  let aNm :: Name a
aNm = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"a" Unique
0
      aTv :: Var a
aTv = Name a -> Unique -> Type -> Var a
forall a. Name a -> Unique -> Type -> Var a
TyVar Name a
forall a. Name a
aNm Unique
0 Type
liftedTypeKind
      bNm :: Name a
bNm = Text -> Unique -> Name a
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
"b" Unique
1
      bTv :: Var a
bTv = Name a -> Unique -> Type -> Var a
forall a. Name a -> Unique -> Type -> Var a
TyVar Name a
forall a. Name a
bNm Unique
1 Type
liftedTypeKind
  in TyVar -> Type -> Type
ForAllTy TyVar
forall a. Var a
aTv (TyVar -> Type -> Type
ForAllTy TyVar
forall a. Var a
bTv (Type -> Type -> Type
mkFunTy (TyVar -> Type
VarTy TyVar
forall a. Var a
aTv) (TyVar -> Type
VarTy TyVar
forall a. Var a
bTv)))

-- | Create a vector of supplied elements
mkVec :: DataCon -- ^ The Nil constructor
      -> DataCon -- ^ The Cons (:>) constructor
      -> Type    -- ^ Element type
      -> Integer -- ^ Length of the vector
      -> [Term]  -- ^ Elements to put in the vector
      -> Term
mkVec :: DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nilCon DataCon
consCon Type
resTy = Integer -> [Term] -> Term
go
  where
    go :: Integer -> [Term] -> Term
go Integer
_ [] = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
nilCon) [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0))
                                   ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
resTy
                                   ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Type -> Term
primCo Type
nilCoTy)
                                   ]

    go Integer
n (Term
x:[Term]
xs) = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
consCon) [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n))
                                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
resTy
                                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Type -> Term
primCo (Integer -> Type
consCoTy Integer
n))
                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
x
                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Integer -> [Term] -> Term
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [Term]
xs)]

    nilCoTy :: Type
nilCoTy    = case DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
nilCon [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0)) ,Type
resTy] of
                   Just (Type
x:[Type]
_) -> Type
x
                   Maybe [Type]
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
    consCoTy :: Integer -> Type
consCoTy Integer
n = case DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
consCon
                                        [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n))
                                        ,Type
resTy
                                        ,(LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))] of
                   Just (Type
x:[Type]
_) -> Type
x
                   Maybe [Type]
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"

-- | Append elements to the supplied vector
appendToVec :: 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
appendToVec :: DataCon -> Type -> Term -> Integer -> [Term] -> Term
appendToVec DataCon
consCon Type
resTy Term
vec = Integer -> [Term] -> Term
go
  where
    go :: Integer -> [Term] -> Term
go Integer
_ []     = Term
vec
    go Integer
n (Term
x:[Term]
xs) = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
consCon) [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n))
                                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
resTy
                                        ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Type -> Term
primCo (Integer -> Type
consCoTy Integer
n))
                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left Term
x
                                        ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Integer -> [Term] -> Term
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [Term]
xs)]

    consCoTy :: Integer -> Type
consCoTy Integer
n = case DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
consCon
                                        [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n))
                                        ,Type
resTy
                                        ,(LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))] of
                   Just (Type
x:[Type]
_) -> Type
x
                   Maybe [Type]
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"

-- | 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
extractElems
  :: HasCallStack
  => 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, NonEmpty (Term,NonEmpty (Id, Term)))
extractElems :: Supply
-> InScopeSet
-> DataCon
-> Type
-> Char
-> Integer
-> Term
-> (Supply, NonEmpty (Term, NonEmpty LetBinding))
extractElems Supply
supply InScopeSet
inScope DataCon
consCon Type
resTy Char
s Integer
maxN Term
vec =
  if Integer
maxN Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
1 then
    ((Supply, InScopeSet) -> Supply)
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
-> (Supply, NonEmpty (Term, NonEmpty LetBinding))
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Supply, InScopeSet) -> Supply
forall a b. (a, b) -> a
fst (Integer
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
go Integer
maxN (Supply
supply,InScopeSet
inScope) Term
vec)
  else
    [Char] -> (Supply, NonEmpty (Term, NonEmpty LetBinding))
forall a. HasCallStack => [Char] -> a
error [Char]
"extractElems must be called with positive number"
 where
  go :: Integer -> (Supply,InScopeSet) -> Term
     -> ((Supply,InScopeSet),NonEmpty (Term, NonEmpty (Id, Term)))
  go :: Integer
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
go Integer
n (Supply, InScopeSet)
uniqs0 Term
e = ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
-> Maybe
     ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
forall a. a -> Maybe a -> a
fromMaybe ([Char]
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
forall a. HasCallStack => [Char] -> a
error [Char]
"extractElems: failed to project elements") (Maybe ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
 -> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding)))
-> Maybe
     ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
forall a b. (a -> b) -> a -> b
$ do
    let tys :: [Type]
tys = [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n)),Type
resTy,(LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))]
    [Type]
idTys <- DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
consCon [Type]
tys
    let restTy :: Type
restTy = [Type] -> Type
forall a. [a] -> a
last [Type]
idTys

    let ((Supply, InScopeSet)
uniqs1,TyVar
mTV) = (Supply, InScopeSet)
-> (Text, Type) -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar (Supply, InScopeSet)
uniqs0 (Text
"m",Type
typeNatKind)
    ((Supply, InScopeSet)
uniqs2,[Id
elNId,Id
restNId,Id
co,Id
el,Id
rest]) <- ((Supply, InScopeSet), [Id]) -> Maybe ((Supply, InScopeSet), [Id])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (((Supply, InScopeSet), [Id])
 -> Maybe ((Supply, InScopeSet), [Id]))
-> ((Supply, InScopeSet), [Id])
-> Maybe ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$
      ((Supply, InScopeSet)
 -> (Text, Type) -> ((Supply, InScopeSet), Id))
-> (Supply, InScopeSet)
-> [(Text, Type)]
-> ((Supply, InScopeSet), [Id])
forall (t :: Type -> Type) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumR (Supply, InScopeSet) -> (Text, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply, InScopeSet)
uniqs1 ([(Text, Type)] -> ((Supply, InScopeSet), [Id]))
-> [(Text, Type)] -> ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$ [Text] -> [Type] -> [(Text, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual
        [Text
"el" Text -> Text -> Text
`T.append` (Char
s Char -> Text -> Text
`T.cons` [Char] -> Text
T.pack (Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer
maxNInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n)))
        ,Text
"rest" Text -> Text -> Text
`T.append` (Char
s Char -> Text -> Text
`T.cons` [Char] -> Text
T.pack (Integer -> [Char]
forall a. Show a => a -> [Char]
show (Integer
maxNInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n)))
        ,Text
"_co_"
        ,Text
"el"
        ,Text
"rest"
        ]
        (Type
resTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Type
restTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
idTys)

    let elNVar :: Term
elNVar    = Id -> Term
Var Id
elNId
        pat :: Pat
pat       = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
consCon [TyVar
mTV] [Id
co,Id
el,Id
rest]
        lhs :: Term
lhs       = Term -> Type -> [Alt] -> Term
Case Term
e Type
resTy  [(Pat
pat,Id -> Term
Var Id
el)]
        rhs :: Term
rhs       = Term -> Type -> [Alt] -> Term
Case Term
e Type
restTy [(Pat
pat,Id -> Term
Var Id
rest)]

    let ((Supply, InScopeSet)
uniqs3,[(Term, NonEmpty LetBinding)]
restVs) = if Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
2 then ((Supply, InScopeSet)
uniqs2,[]) else (NonEmpty (Term, NonEmpty LetBinding)
 -> [(Term, NonEmpty LetBinding)])
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
-> ((Supply, InScopeSet), [(Term, NonEmpty LetBinding)])
forall (p :: Type -> Type -> Type) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second NonEmpty (Term, NonEmpty LetBinding)
-> [(Term, NonEmpty LetBinding)]
forall a. NonEmpty a -> [a]
toList (Integer
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) (Supply, InScopeSet)
uniqs2 (Id -> Term
Var Id
restNId))

    ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
-> Maybe
     ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Supply, InScopeSet)
uniqs3,(Term
elNVar,(Id
elNId, Term
lhs) LetBinding -> [LetBinding] -> NonEmpty LetBinding
forall a. a -> [a] -> NonEmpty a
:| [(Id
restNId, Term
rhs)]) (Term, NonEmpty LetBinding)
-> [(Term, NonEmpty LetBinding)]
-> NonEmpty (Term, NonEmpty LetBinding)
forall a. a -> [a] -> NonEmpty a
:| [(Term, NonEmpty LetBinding)]
restVs)

-- | 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
extractTElems
  :: 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],[(Id, Term)]))
extractTElems :: Supply
-> InScopeSet
-> DataCon
-> DataCon
-> Type
-> Char
-> Integer
-> Term
-> (Supply, ([Term], [LetBinding]))
extractTElems Supply
supply InScopeSet
inScope DataCon
lrCon DataCon
brCon Type
resTy Char
s Integer
maxN Term
tree =
  ((Supply, InScopeSet) -> Supply)
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
-> (Supply, ([Term], [LetBinding]))
forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Supply, InScopeSet) -> Supply
forall a b. (a, b) -> a
fst (Integer
-> [Unique]
-> [Unique]
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
go Integer
maxN [Unique
0..(Unique
2Unique -> Integer -> Unique
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
maxNInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1))Unique -> Unique -> Unique
forall a. Num a => a -> a -> a
-Unique
2] [Unique
0..(Unique
2Unique -> Integer -> Unique
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
maxN Unique -> Unique -> Unique
forall a. Num a => a -> a -> a
- Unique
1)] (Supply
supply,InScopeSet
inScope) Term
tree)
 where
  go :: Integer
     -> [Int]
     -> [Int]
     -> (Supply,InScopeSet)
     -> Term
     -> ((Supply,InScopeSet),([Term],[(Id, Term)]))
  go :: Integer
-> [Unique]
-> [Unique]
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
go Integer
0 [Unique]
_ [Unique]
ks (Supply, InScopeSet)
uniqs0 Term
e = ((Supply, InScopeSet), ([Term], [LetBinding]))
-> Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> ((Supply, InScopeSet), ([Term], [LetBinding]))
forall a. HasCallStack => [Char] -> a
error [Char]
"extractTElems: failed to project elements") (Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
 -> ((Supply, InScopeSet), ([Term], [LetBinding])))
-> Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
forall a b. (a -> b) -> a -> b
$ do
    let tys :: [Type]
tys = [LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0),Type
resTy]
    [Type]
idTys <- DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
lrCon [Type]
tys
    (Unique
k,[Unique]
_) <- [Unique] -> Maybe (Unique, [Unique])
forall a. [a] -> Maybe (a, [a])
uncons [Unique]
ks

    ((Supply, InScopeSet)
uniqs1,[Id
elNId,Id
co,Id
el]) <- ((Supply, InScopeSet), [Id]) -> Maybe ((Supply, InScopeSet), [Id])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (((Supply, InScopeSet), [Id])
 -> Maybe ((Supply, InScopeSet), [Id]))
-> ((Supply, InScopeSet), [Id])
-> Maybe ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$
      ((Supply, InScopeSet)
 -> (Text, Type) -> ((Supply, InScopeSet), Id))
-> (Supply, InScopeSet)
-> [(Text, Type)]
-> ((Supply, InScopeSet), [Id])
forall (t :: Type -> Type) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumR (Supply, InScopeSet) -> (Text, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply, InScopeSet)
uniqs0 ([(Text, Type)] -> ((Supply, InScopeSet), [Id]))
-> [(Text, Type)] -> ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$ [Text] -> [Type] -> [(Text, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual
        [ Text
"el" Text -> Text -> Text
`T.append` (Char
s Char -> Text -> Text
`T.cons` [Char] -> Text
T.pack (Unique -> [Char]
forall a. Show a => a -> [Char]
show Unique
k))
        , Text
"_co_"
        , Text
"el"
        ]
        (Type
resTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
idTys)
    let elNVar :: Term
elNVar = Id -> Term
Var Id
elNId
        pat :: Pat
pat    = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
lrCon [] [Id
co,Id
el]
        rhs :: Term
rhs    = Term -> Type -> [Alt] -> Term
Case Term
e Type
resTy [(Pat
pat,Id -> Term
Var Id
el)]
    ((Supply, InScopeSet), ([Term], [LetBinding]))
-> Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Supply, InScopeSet)
uniqs1,([Term
elNVar],[(Id
elNId, Term
rhs)]))

  go Integer
n [Unique]
bs [Unique]
ks (Supply, InScopeSet)
uniqs0 Term
e = ((Supply, InScopeSet), ([Term], [LetBinding]))
-> Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> ((Supply, InScopeSet), ([Term], [LetBinding]))
forall a. HasCallStack => [Char] -> a
error [Char]
"extractTElems: failed to project elements") (Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
 -> ((Supply, InScopeSet), ([Term], [LetBinding])))
-> Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
forall a b. (a -> b) -> a -> b
$ do
    let tys :: [Type]
tys = [LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n),Type
resTy,LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1))]
    [Type]
idTys <- DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
brCon [Type]
tys

    let ((Supply, InScopeSet)
uniqs1,TyVar
mTV) = (Supply, InScopeSet)
-> (Text, Type) -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar (Supply, InScopeSet)
uniqs0 (Text
"m",Type
typeNatKind)
    (Unique
b0:[Unique]
bL,Unique
b1:[Unique]
bR) <- ([Unique], [Unique]) -> Maybe ([Unique], [Unique])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Unique -> [Unique] -> ([Unique], [Unique])
forall a. Unique -> [a] -> ([a], [a])
splitAt ([Unique] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [Unique]
bs Unique -> Unique -> Unique
forall a. Integral a => a -> a -> a
`div` Unique
2) [Unique]
bs)
    let brTy :: Type
brTy = [Type] -> Type
forall a. [a] -> a
last [Type]
idTys
    ((Supply, InScopeSet)
uniqs2,[Id
ltNId,Id
rtNId,Id
co,Id
lt,Id
rt]) <- ((Supply, InScopeSet), [Id]) -> Maybe ((Supply, InScopeSet), [Id])
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (((Supply, InScopeSet), [Id])
 -> Maybe ((Supply, InScopeSet), [Id]))
-> ((Supply, InScopeSet), [Id])
-> Maybe ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$
      ((Supply, InScopeSet)
 -> (Text, Type) -> ((Supply, InScopeSet), Id))
-> (Supply, InScopeSet)
-> [(Text, Type)]
-> ((Supply, InScopeSet), [Id])
forall (t :: Type -> Type) a b c.
Traversable t =>
(a -> b -> (a, c)) -> a -> t b -> (a, t c)
mapAccumR (Supply, InScopeSet) -> (Text, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply, InScopeSet)
uniqs1 ([(Text, Type)] -> ((Supply, InScopeSet), [Id]))
-> [(Text, Type)] -> ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$ [Text] -> [Type] -> [(Text, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual
        [Text
"lt" Text -> Text -> Text
`T.append` (Char
s Char -> Text -> Text
`T.cons` [Char] -> Text
T.pack (Unique -> [Char]
forall a. Show a => a -> [Char]
show Unique
b0))
        ,Text
"rt" Text -> Text -> Text
`T.append` (Char
s Char -> Text -> Text
`T.cons` [Char] -> Text
T.pack (Unique -> [Char]
forall a. Show a => a -> [Char]
show Unique
b1))
        ,Text
"_co_"
        ,Text
"lt"
        ,Text
"rt"
        ]
        (Type
brTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Type
brTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
idTys)
    let ltVar :: Term
ltVar = Id -> Term
Var Id
ltNId
        rtVar :: Term
rtVar = Id -> Term
Var Id
rtNId
        pat :: Pat
pat   = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
brCon [TyVar
mTV] [Id
co,Id
lt,Id
rt]
        ltRhs :: Term
ltRhs = Term -> Type -> [Alt] -> Term
Case Term
e Type
brTy [(Pat
pat,Id -> Term
Var Id
lt)]
        rtRhs :: Term
rtRhs = Term -> Type -> [Alt] -> Term
Case Term
e Type
brTy [(Pat
pat,Id -> Term
Var Id
rt)]

        ([Unique]
kL,[Unique]
kR) = Unique -> [Unique] -> ([Unique], [Unique])
forall a. Unique -> [a] -> ([a], [a])
splitAt ([Unique] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [Unique]
ks Unique -> Unique -> Unique
forall a. Integral a => a -> a -> a
`div` Unique
2) [Unique]
ks
        ((Supply, InScopeSet)
uniqs3,([Term]
lVars,[LetBinding]
lBinds)) = Integer
-> [Unique]
-> [Unique]
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [Unique]
bL [Unique]
kL (Supply, InScopeSet)
uniqs2 Term
ltVar
        ((Supply, InScopeSet)
uniqs4,([Term]
rVars,[LetBinding]
rBinds)) = Integer
-> [Unique]
-> [Unique]
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [Unique]
bR [Unique]
kR (Supply, InScopeSet)
uniqs3 Term
rtVar

    ((Supply, InScopeSet), ([Term], [LetBinding]))
-> Maybe ((Supply, InScopeSet), ([Term], [LetBinding]))
forall (m :: Type -> Type) a. Monad m => a -> m a
return ( (Supply, InScopeSet)
uniqs4
           , ( [Term]
lVars [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
rVars
             , (Id
ltNId, Term
ltRhs)LetBinding -> [LetBinding] -> [LetBinding]
forall a. a -> [a] -> [a]
:(Id
rtNId, Term
rtRhs)LetBinding -> [LetBinding] -> [LetBinding]
forall a. a -> [a] -> [a]
: ([LetBinding]
lBinds [LetBinding] -> [LetBinding] -> [LetBinding]
forall a. [a] -> [a] -> [a]
++ [LetBinding]
rBinds)
             )
           )

-- | Create a vector of supplied elements
mkRTree :: DataCon -- ^ The LR constructor
        -> DataCon -- ^ The BR constructor
        -> Type    -- ^ Element type
        -> Integer -- ^ Depth of the tree
        -> [Term]  -- ^ Elements to put in the tree
        -> Term
mkRTree :: DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkRTree DataCon
lrCon DataCon
brCon Type
resTy = Integer -> [Term] -> Term
go
  where
    go :: Integer -> [Term] -> Term
go Integer
_ [Term
x] = Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
lrCon) [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0))
                                    ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
resTy
                                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left  (Type -> Term
primCo Type
lrCoTy)
                                    ,Term -> Either Term Type
forall a b. a -> Either a b
Left  Term
x
                                    ]

    go Integer
n [Term]
xs =
      let ([Term]
xsL,[Term]
xsR) = Unique -> [Term] -> ([Term], [Term])
forall a. Unique -> [a] -> ([a], [a])
splitAt ([Term] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [Term]
xs Unique -> Unique -> Unique
forall a. Integral a => a -> a -> a
`div` Unique
2) [Term]
xs
      in  Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
brCon) [Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n))
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right Type
resTy
                              ,Type -> Either Term Type
forall a b. b -> Either a b
Right (LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Type -> Term
primCo (Integer -> Type
brCoTy Integer
n))
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Integer -> [Term] -> Term
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [Term]
xsL)
                              ,Term -> Either Term Type
forall a b. a -> Either a b
Left (Integer -> [Term] -> Term
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) [Term]
xsR)]

    lrCoTy :: Type
lrCoTy   = case DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
lrCon [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0)) ,Type
resTy] of
                 Just (Type
x:[Type]
_) -> Type
x
                 Maybe [Type]
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"
    brCoTy :: Integer -> Type
brCoTy Integer
n = case DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
brCon
                                      [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
n))
                                      ,Type
resTy
                                      ,(LitTy -> Type
LitTy (Integer -> LitTy
NumTy (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)))] of
                 Just (Type
x:[Type]
_) -> Type
x
                 Maybe [Type]
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible"

-- | 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.
--
isSignalType :: TyConMap -> Type -> Bool
isSignalType :: TyConMap -> Type -> Bool
isSignalType TyConMap
tcm Type
ty = HashSet TyConName -> Type -> Bool
go HashSet TyConName
forall a. HashSet a
HashSet.empty Type
ty
  where
    go :: HashSet TyConName -> Type -> Bool
go HashSet TyConName
tcSeen (Type -> TypeView
tyView -> TyConApp TyConName
tcNm [Type]
args) = case TyConName -> Text
forall a. Name a -> Text
nameOcc TyConName
tcNm of
      Text
"Clash.Signal.Internal.Signal"      -> Bool
True
      Text
"Clash.Signal.BiSignal.BiSignalIn"  -> Bool
True
      Text
"Clash.Signal.BiSignal.BiSignalOut" -> Bool
True
      Text
_ | TyConName
tcNm TyConName -> HashSet TyConName -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`HashSet.member` HashSet TyConName
tcSeen    -> Bool
False -- Do not follow rec types
        | Bool
otherwise -> case TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tcNm TyConMap
tcm of
            Just TyCon
tc -> let dcs :: [DataCon]
dcs         = TyCon -> [DataCon]
tyConDataCons TyCon
tc
                           dcInsArgTys :: [Type]
dcInsArgTys = [[Type]] -> [Type]
forall (t :: Type -> Type) a. Foldable t => t [a] -> [a]
concat
                                       ([[Type]] -> [Type]) -> [[Type]] -> [Type]
forall a b. (a -> b) -> a -> b
$ (DataCon -> Maybe [Type]) -> [DataCon] -> [[Type]]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (DataCon -> [Type] -> Maybe [Type]
`dataConInstArgTys` [Type]
args) [DataCon]
dcs
                           tcSeen' :: HashSet TyConName
tcSeen'     = TyConName -> HashSet TyConName -> HashSet TyConName
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
HashSet.insert TyConName
tcNm HashSet TyConName
tcSeen
                       in  (Type -> Bool) -> [Type] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (HashSet TyConName -> Type -> Bool
go HashSet TyConName
tcSeen') [Type]
dcInsArgTys
            Maybe TyCon
Nothing -> Bool -> [Char] -> Bool -> Bool
forall a. Bool -> [Char] -> a -> a
traceIf Bool
True ($([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"isSignalType: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyConName -> [Char]
forall a. Show a => a -> [Char]
show TyConName
tcNm
                                     [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" not found.") Bool
False

    go HashSet TyConName
_ Type
_ = Bool
False

-- | Determines whether given type is an (alias of en) Enable line.
isEnable
  :: TyConMap
  -> Type
  -> Bool
isEnable :: TyConMap -> Type -> Bool
isEnable TyConMap
m Type
ty0
  | TyConApp (TyConName -> Text
forall a. Name a -> Text
nameOcc -> Text
"Clash.Signal.Internal.Enable") [Type]
_ <- Type -> TypeView
tyView Type
ty0 = Bool
True
  | Just Type
ty1 <- TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m Type
ty0 = TyConMap -> Type -> Bool
isEnable TyConMap
m Type
ty1
isEnable TyConMap
_ Type
_ = Bool
False

-- | Determines whether given type is an (alias of en) Clock or Reset line
isClockOrReset
  :: TyConMap
  -> Type
  -> Bool
isClockOrReset :: TyConMap -> Type -> Bool
isClockOrReset TyConMap
m (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just Type
ty)    = TyConMap -> Type -> Bool
isClockOrReset TyConMap
m Type
ty
isClockOrReset TyConMap
_ (Type -> TypeView
tyView -> TyConApp TyConName
tcNm [Type]
_) = case TyConName -> Text
forall a. Name a -> Text
nameOcc TyConName
tcNm of
  Text
"Clash.Signal.Internal.Clock" -> Bool
True
  Text
"Clash.Signal.Internal.ClockN" -> Bool
True
  Text
"Clash.Signal.Internal.Reset" -> Bool
True
  Text
_ -> Bool
False
isClockOrReset TyConMap
_ Type
_ = Bool
False

tyNatSize :: TyConMap
          -> Type
          -> Except String Integer
tyNatSize :: TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
m (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just Type
ty) = TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
m Type
ty
tyNatSize TyConMap
_ (LitTy (NumTy Integer
i))        = Integer -> Except [Char] Integer
forall (m :: Type -> Type) a. Monad m => a -> m a
return Integer
i
tyNatSize TyConMap
_ Type
ty = [Char] -> Except [Char] Integer
forall (m :: Type -> Type) e a. Monad m => e -> ExceptT e m a
throwE ([Char] -> Except [Char] Integer)
-> [Char] -> Except [Char] Integer
forall a b. (a -> b) -> a -> b
$ $([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Cannot reduce to an integer:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr Type
ty


mkUniqSystemTyVar
  :: (Supply, InScopeSet)
  -> (OccName, Kind)
  -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar :: (Supply, InScopeSet)
-> (Text, Type) -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar (Supply
supply,InScopeSet
inScope) (Text
nm, Type
ki) =
  ((Supply
supply',InScopeSet -> TyVar -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
inScope TyVar
v'), TyVar
v')
 where
  (Unique
u,Supply
supply') = Supply -> (Unique, Supply)
freshId Supply
supply
  v :: TyVar
v           = Type -> TyName -> TyVar
mkTyVar Type
ki (Text -> Unique -> TyName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
nm Unique
u)
  v' :: TyVar
v'          = InScopeSet -> TyVar -> TyVar
forall a. (Uniquable a, ClashPretty a) => InScopeSet -> a -> a
uniqAway InScopeSet
inScope TyVar
v

mkUniqSystemId
  :: (Supply, InScopeSet)
  -> (OccName, Type)
  -> ((Supply,InScopeSet), Id)
mkUniqSystemId :: (Supply, InScopeSet) -> (Text, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply
supply,InScopeSet
inScope) (Text
nm, Type
ty) =
  ((Supply
supply',InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
inScope Id
v'), Id
v')
 where
  (Unique
u,Supply
supply') = Supply -> (Unique, Supply)
freshId Supply
supply
  v :: Id
v           = Type -> TmName -> Id
mkLocalId Type
ty (Text -> Unique -> TmName
forall a. Text -> Unique -> Name a
mkUnsafeSystemName Text
nm Unique
u)
  v' :: Id
v'          = InScopeSet -> Id -> Id
forall a. (Uniquable a, ClashPretty a) => InScopeSet -> a -> a
uniqAway InScopeSet
inScope Id
v

mkUniqInternalId
  :: (Supply, InScopeSet)
  -> (OccName, Type)
  -> ((Supply,InScopeSet), Id)
mkUniqInternalId :: (Supply, InScopeSet) -> (Text, Type) -> ((Supply, InScopeSet), Id)
mkUniqInternalId (Supply
supply,InScopeSet
inScope) (Text
nm, Type
ty) =
  ((Supply
supply',InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
inScope Id
v'), Id
v')
 where
  (Unique
u,Supply
supply') = Supply -> (Unique, Supply)
freshId Supply
supply
  v :: Id
v           = Type -> TmName -> Id
mkLocalId Type
ty (Text -> Unique -> TmName
forall a. Text -> Unique -> Name a
mkUnsafeInternalName Text
nm Unique
u)
  v' :: Id
v'          = InScopeSet -> Id -> Id
forall a. (Uniquable a, ClashPretty a) => InScopeSet -> a -> a
uniqAway InScopeSet
inScope Id
v


-- | 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
dataConInstArgTysE
  :: HasCallStack
  => InScopeSet
  -> TyConMap
  -> DataCon
  -> [Type]
  -> Maybe [Type]
dataConInstArgTysE :: InScopeSet -> TyConMap -> DataCon -> [Type] -> Maybe [Type]
dataConInstArgTysE InScopeSet
is0 TyConMap
tcm (MkData { [Type]
dcArgTys :: DataCon -> [Type]
dcArgTys :: [Type]
dcArgTys, [TyVar]
dcExtTyVars :: DataCon -> [TyVar]
dcExtTyVars :: [TyVar]
dcExtTyVars, [TyVar]
dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars :: [TyVar]
dcUnivTyVars }) [Type]
inst_tys = do
  -- TODO: Check if all existentials were solved (they should be, or the wouldn't have
  -- TODO: been solved in the caseElemExistentials transformation)
  let is1 :: InScopeSet
is1   = InScopeSet -> [TyVar] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList InScopeSet
is0 [TyVar]
dcExtTyVars
      is2 :: InScopeSet
is2   = InScopeSet -> InScopeSet -> InScopeSet
unionInScope InScopeSet
is1 (VarSet -> InScopeSet
mkInScopeSet ([Type] -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf [Type]
inst_tys))
      subst :: Subst
subst = Subst -> [(TyVar, Type)] -> Subst
extendTvSubstList (InScopeSet -> Subst
mkSubst InScopeSet
is2) ([TyVar] -> [Type] -> [(TyVar, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual [TyVar]
dcUnivTyVars [Type]
inst_tys)
  [TyVar] -> [Type] -> Maybe [Type]
go
    (HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
substGlobalsInExistentials InScopeSet
is0 [TyVar]
dcExtTyVars ([TyVar] -> [Type] -> [(TyVar, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual [TyVar]
dcUnivTyVars [Type]
inst_tys))
    ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) [Type]
dcArgTys)

 where
  exts :: VarSet
exts = [TyVar] -> VarSet
forall a. [Var a] -> VarSet
mkVarSet [TyVar]
dcExtTyVars
  go
    :: [TyVar]
    -- ^ Existentials
    -> [Type]
    -- ^ Type arguments
    -> Maybe [Type]
    -- ^ Maybe ([type of non-existential])
  go :: [TyVar] -> [Type] -> Maybe [Type]
go [TyVar]
exts0 [Type]
args0 =
    let eqs :: [(Type, Type)]
eqs = [Maybe (Type, Type)] -> [(Type, Type)]
forall a. [Maybe a] -> [a]
catMaybes ((Type -> Maybe (Type, Type)) -> [Type] -> [Maybe (Type, Type)]
forall a b. (a -> b) -> [a] -> [b]
map (TyConMap -> Type -> Maybe (Type, Type)
typeEq TyConMap
tcm) [Type]
args0) in
    case TyConMap -> VarSet -> [(Type, Type)] -> [(TyVar, Type)]
solveNonAbsurds TyConMap
tcm VarSet
exts [(Type, Type)]
eqs of
      [] ->
        [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
args0
      [(TyVar, Type)]
sols ->
        [TyVar] -> [Type] -> Maybe [Type]
go [TyVar]
exts1 [Type]
args1
        where
          exts1 :: [TyVar]
exts1 = HasCallStack => InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
InScopeSet -> [TyVar] -> [(TyVar, Type)] -> [TyVar]
substInExistentialsList InScopeSet
is0 [TyVar]
exts0 [(TyVar, Type)]
sols
          is2 :: InScopeSet
is2   = InScopeSet -> [TyVar] -> InScopeSet
forall a. InScopeSet -> [Var a] -> InScopeSet
extendInScopeSetList InScopeSet
is0 [TyVar]
exts1
          subst :: Subst
subst = Subst -> [(TyVar, Type)] -> Subst
extendTvSubstList (InScopeSet -> Subst
mkSubst InScopeSet
is2) [(TyVar, Type)]
sols
          args1 :: [Type]
args1 = (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) [Type]
args0


-- | 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.
dataConInstArgTys :: DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys :: DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys (MkData { [Type]
dcArgTys :: [Type]
dcArgTys :: DataCon -> [Type]
dcArgTys, [TyVar]
dcUnivTyVars :: [TyVar]
dcUnivTyVars :: DataCon -> [TyVar]
dcUnivTyVars, [TyVar]
dcExtTyVars :: [TyVar]
dcExtTyVars :: DataCon -> [TyVar]
dcExtTyVars }) [Type]
inst_tys =
  -- TODO: Check if inst_tys do not contain any free variables on call sites. If
  -- TODO: they do, this function is unsafe to use.
  let tyvars :: [TyVar]
tyvars = [TyVar]
dcUnivTyVars [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
dcExtTyVars in
  if [TyVar] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [TyVar]
tyvars Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [Type]
inst_tys then
    [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => [TyVar] -> [Type] -> Type -> Type
[TyVar] -> [Type] -> Type -> Type
substTyWith [TyVar]
tyvars [Type]
inst_tys) [Type]
dcArgTys)
  else
    Maybe [Type]
forall a. Maybe a
Nothing

-- | Make a coercion
primCo
  :: Type
  -> Term
primCo :: Type -> Term
primCo Type
ty = PrimInfo -> Term
Prim (Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo Text
"_CO_" Type
ty WorkInfo
WorkNever IsMultiPrim
SingleResult PrimUnfolding
NoUnfolding)

-- | Make an unsafe coercion
primUCo :: Term
primUCo :: Term
primUCo =
  PrimInfo -> Term
Prim PrimInfo :: Text
-> Type -> WorkInfo -> IsMultiPrim -> PrimUnfolding -> PrimInfo
PrimInfo { primName :: Text
primName        = Text
"GHC.Prim.unsafeCoerce#"
                , primType :: Type
primType        = Type
unsafeCoerceTy
                , primWorkInfo :: WorkInfo
primWorkInfo    = WorkInfo
WorkNever
                , primMultiResult :: IsMultiPrim
primMultiResult = IsMultiPrim
SingleResult
                , primUnfolding :: PrimUnfolding
primUnfolding = PrimUnfolding
NoUnfolding
                }

undefinedPrims :: [T.Text]
undefinedPrims :: [Text]
undefinedPrims =
  [ Text
"Clash.Normalize.Primitives.undefined"
  , Text
"Control.Exception.Base.absentError"
  , Text
"Control.Exception.Base.patError"
  , Text
"GHC.Err.error"
  , Text
"GHC.Err.errorWithoutStackTrace"
  , Text
"GHC.Err.undefined"
  , Text
"GHC.Prim.Panic.absentError"
  , Text
"GHC.Real.divZeroError"
  , Text
"GHC.Real.overflowError"
  , Text
"GHC.Real.ratioZeroDenominatorError"
  , Text
"GHC.Real.underflowError"
  ]

undefinedXPrims :: [T.Text]
undefinedXPrims :: [Text]
undefinedXPrims =
  [ Text
"Clash.Normalize.Primitives.undefinedX"
  , Text
"Clash.XException.errorX"
  ]

substArgTys
  :: DataCon
  -> [Type]
  -> [Type]
substArgTys :: DataCon -> [Type] -> [Type]
substArgTys DataCon
dc [Type]
args =
  let univTVs :: [TyVar]
univTVs = DataCon -> [TyVar]
dcUnivTyVars DataCon
dc
      extTVs :: [TyVar]
extTVs  = DataCon -> [TyVar]
dcExtTyVars DataCon
dc
      argsFVs :: VarSet
argsFVs = [Type] -> VarSet
forall a. HasFreeVars a => a -> VarSet
freeVarsOf [Type]
args
      is :: InScopeSet
is      = VarSet -> InScopeSet
mkInScopeSet (VarSet
argsFVs VarSet -> VarSet -> VarSet
`unionVarSet` [TyVar] -> VarSet
forall a. [Var a] -> VarSet
mkVarSet [TyVar]
extTVs)
      -- See Note [The substitution invariant]
      subst :: Subst
subst   = Subst -> [(TyVar, Type)] -> Subst
extendTvSubstList (InScopeSet -> Subst
mkSubst InScopeSet
is) ([TyVar]
univTVs [TyVar] -> [Type] -> [(TyVar, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
`zipEqual` [Type]
args)
  in  (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (HasCallStack => Subst -> Type -> Type
Subst -> Type -> Type
substTy Subst
subst) (DataCon -> [Type]
dcArgTys DataCon
dc)

-- | Try to reduce an arbitrary type to a literal type (Symbol or Nat),
-- and subsequently extract its String representation
tyLitShow
  :: TyConMap
  -> Type
  -> Except String String
tyLitShow :: TyConMap -> Type -> Except [Char] [Char]
tyLitShow TyConMap
m (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just Type
ty) = TyConMap -> Type -> Except [Char] [Char]
tyLitShow TyConMap
m Type
ty
tyLitShow TyConMap
_ (LitTy (SymTy [Char]
s))        = [Char] -> Except [Char] [Char]
forall (m :: Type -> Type) a. Monad m => a -> m a
return [Char]
s
tyLitShow TyConMap
_ (LitTy (NumTy Integer
s))        = [Char] -> Except [Char] [Char]
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
s)
tyLitShow TyConMap
_ Type
ty = [Char] -> Except [Char] [Char]
forall (m :: Type -> Type) e a. Monad m => e -> ExceptT e m a
throwE ([Char] -> Except [Char] [Char]) -> [Char] -> Except [Char] [Char]
forall a b. (a -> b) -> a -> b
$ $([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Cannot reduce to a string:\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr Type
ty

-- | Helper existential for 'shouldSplit', contains a function that:
--
-- 1. given a term of a type that should be split,
-- 2. creates projections of that term for all the constructor arguments
data Projections where
  Projections :: (forall m . MonadUnique m => InScopeSet -> Term -> m [Term])
              -> Projections

-- | 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.
shouldSplit
  :: TyConMap
  -> Type
  -- ^ Type to examine
  -> Maybe ([Term] -> Term, Projections, [Type])
  -- ^ If we want to split values of the given type then we have /Just/:
  --
  -- 1. The (type-applied) data-constructor which, when applied to values of
  --    the types in 3., creates a value of the examined type
  --
  -- 2. Function that give a term of the type we need to split, creates projections
  --    of that term for all the types in 3.
  --
  -- 3. The arguments types of the product we are trying to split.
  --
  -- Note that we only split one level at a time (although we check all the way
  -- down), e.g. given /(Int, (Clock, Bool))/ we return:
  --
  -- > Just ( (,) @Int @(Clock, Bool)
  -- >      , \s -> [case s of (a,b) -> a, case s of (a,b) -> b]
  -- >      , [Int, (Clock, Bool)])
  --
  -- An outer loop is required to subsequently split the /(Clock, Bool)/ tuple.
shouldSplit :: TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm (Type -> TypeView
tyView ->  TyConApp (TyConName -> Text
forall a. Name a -> Text
nameOcc -> Text
"Clash.Explicit.SimIO.SimIO") [Type
tyArg]) =
  -- We also look through `SimIO` to find things like Files
  TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
tyArg
shouldSplit TyConMap
tcm Type
ty = TyConMap -> TypeView -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit0 TyConMap
tcm (Type -> TypeView
tyView (TyConMap -> Type -> Type
coreView TyConMap
tcm Type
ty))

-- | Worker of 'shouldSplit', works on 'TypeView' instead of 'Type'
shouldSplit0
  :: TyConMap
  -> TypeView
  -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit0 :: TyConMap -> TypeView -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit0 TyConMap
tcm (TyConApp TyConName
tcNm [Type]
tyArgs)
  | Just TyCon
tc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tcNm TyConMap
tcm
  , [DataCon
dc] <- TyCon -> [DataCon]
tyConDataCons TyCon
tc
  , let dcArgs :: [Type]
dcArgs = DataCon -> [Type] -> [Type]
substArgTys DataCon
dc [Type]
tyArgs
  , let dcArgsLen :: Unique
dcArgsLen = [Type] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [Type]
dcArgs
  , Unique
dcArgsLen Unique -> Unique -> Bool
forall a. Ord a => a -> a -> Bool
> Unique
1
  , let dcArgVs :: [TypeView]
dcArgVs = (Type -> TypeView) -> [Type] -> [TypeView]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> TypeView
tyView (Type -> TypeView) -> (Type -> Type) -> Type -> TypeView
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyConMap -> Type -> Type
coreView TyConMap
tcm) [Type]
dcArgs
  = if (TypeView -> Bool) -> [TypeView] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any TypeView -> Bool
shouldSplitTy [TypeView]
dcArgVs Bool -> Bool -> Bool
&& Bool -> Bool
not (TyConName -> [Type] -> Bool
forall a. Name a -> [Type] -> Bool
isHidden TyConName
tcNm [Type]
tyArgs) then
      ([Term] -> Term, Projections, [Type])
-> Maybe ([Term] -> Term, Projections, [Type])
forall a. a -> Maybe a
Just ( Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
dc) ([Either Term Type] -> Term)
-> ([Term] -> [Either Term Type]) -> [Term] -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Type -> Either Term Type) -> [Type] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Either Term Type
forall a b. b -> Either a b
Right [Type]
tyArgs [Either Term Type] -> [Either Term Type] -> [Either Term Type]
forall a. [a] -> [a] -> [a]
++) ([Either Term Type] -> [Either Term Type])
-> ([Term] -> [Either Term Type]) -> [Term] -> [Either Term Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> Either Term Type) -> [Term] -> [Either Term Type]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Either Term Type
forall a b. a -> Either a b
Left
           , (forall (m :: Type -> Type).
 MonadUnique m =>
 InScopeSet -> Term -> m [Term])
-> Projections
Projections
             (\InScopeSet
is0 Term
subj -> (Unique -> m Term) -> [Unique] -> m [Term]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([Char]
-> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
[Char]
-> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
mkSelectorCase ($([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"splitArg") InScopeSet
is0 TyConMap
tcm Term
subj Unique
1)
                                [Unique
0..Unique
dcArgsLen Unique -> Unique -> Unique
forall a. Num a => a -> a -> a
- Unique
1])
           , [Type]
dcArgs
           )
    else
      Maybe ([Term] -> Term, Projections, [Type])
forall a. Maybe a
Nothing
  | Text
"Clash.Sized.Vector.Vec" <- TyConName -> Text
forall a. Name a -> Text
nameOcc TyConName
tcNm
  , [Type
nTy,Type
argTy] <- [Type]
tyArgs
  , Right Integer
n <- Except [Char] Integer -> Either [Char] Integer
forall e a. Except e a -> Either e a
runExcept (TyConMap -> Type -> Except [Char] Integer
tyNatSize TyConMap
tcm Type
nTy)
  , Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1
  , Just TyCon
tc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
UniqMap.lookup TyConName
tcNm TyConMap
tcm
  , [DataCon
nil,DataCon
cons] <- TyCon -> [DataCon]
tyConDataCons TyCon
tc
  = if TypeView -> Bool
shouldSplitTy (Type -> TypeView
tyView (TyConMap -> Type -> Type
coreView TyConMap
tcm Type
argTy)) then
      ([Term] -> Term, Projections, [Type])
-> Maybe ([Term] -> Term, Projections, [Type])
forall a. a -> Maybe a
Just ( DataCon -> DataCon -> Type -> Integer -> [Term] -> Term
mkVec DataCon
nil DataCon
cons Type
argTy Integer
n
           , (forall (m :: Type -> Type).
 MonadUnique m =>
 InScopeSet -> Term -> m [Term])
-> Projections
Projections (\InScopeSet
is0 Term
subj -> (Integer -> m Term) -> [Integer] -> m [Term]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InScopeSet -> Term -> Integer -> m Term
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Term -> Integer -> m Term
mkVecSelector InScopeSet
is0 Term
subj) [Integer
0..Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1])
           , Unique -> Type -> [Type]
forall a. Unique -> a -> [a]
replicate (Integer -> Unique
forall a. Num a => Integer -> a
fromInteger Integer
n) Type
argTy)
    else
      Maybe ([Term] -> Term, Projections, [Type])
forall a. Maybe a
Nothing
 where
  -- Project the n'th value out of a vector
  --
  -- >>> mkVecSelector subj 0
  -- case subj of Cons x xs -> x
  --
  -- >>> mkVecSelector subj 2
  -- case (case (case subj of Cons x xs -> xs) of Cons x xs -> xs) of Cons x xs -> x
  mkVecSelector :: forall m . MonadUnique m => InScopeSet -> Term -> Integer -> m Term
  mkVecSelector :: InScopeSet -> Term -> Integer -> m Term
mkVecSelector InScopeSet
is0 Term
subj Integer
0 =
    [Char]
-> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
[Char]
-> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
mkSelectorCase ($([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"mkVecSelector") InScopeSet
is0 TyConMap
tcm Term
subj Unique
2 Unique
1

  mkVecSelector InScopeSet
is0 Term
subj !Integer
n = do
    Term
subj1 <- [Char]
-> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
forall (m :: Type -> Type).
(HasCallStack, MonadUnique m) =>
[Char]
-> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
mkSelectorCase ($([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"mkVecSelector") InScopeSet
is0 TyConMap
tcm Term
subj Unique
2 Unique
2
    InScopeSet -> Term -> Integer -> m Term
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Term -> Integer -> m Term
mkVecSelector InScopeSet
is0 Term
subj1 (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1)

  shouldSplitTy :: TypeView -> Bool
  shouldSplitTy :: TypeView -> Bool
shouldSplitTy TypeView
ty = Maybe ([Term] -> Term, Projections, [Type]) -> Bool
forall a. Maybe a -> Bool
isJust (TyConMap -> TypeView -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit0 TyConMap
tcm TypeView
ty) Bool -> Bool -> Bool
|| TypeView -> Bool
splitTy TypeView
ty

  -- Hidden constructs (HiddenClock, HiddenReset, ..) don't need to be split
  -- because KnownDomain will be filtered anyway during netlist generation due
  -- to it being a zero-width type
  --
  -- TODO: This currently only handles (IP $x, KnownDomain) given that $x is any
  -- TODO: of the constructs handled in 'splitTy'. In practise this means only
  -- TODO: HiddenClock, HiddenReset, and HiddenEnable are handled. If a user were
  -- TODO: to define their own versions with -for example- the elements of the
  -- TODO: tuple swapped, 'isHidden' wouldn't recognize it. We could generalize
  -- TODO: this in the future.
  --
  isHidden :: Name a -> [Type] -> Bool
  isHidden :: Name a -> [Type] -> Bool
isHidden Name a
nm [Type
a1, Type
a2] | TyConApp TyConName
a2Nm [Type]
_ <- Type -> TypeView
tyView Type
a2 =
       Name a -> Text
forall a. Name a -> Text
nameOcc Name a
nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"GHC.Classes.(%,%)"
    Bool -> Bool -> Bool
&& TypeView -> Bool
splitTy (Type -> TypeView
tyView (Type -> Type
stripIP Type
a1))
    Bool -> Bool -> Bool
&& TyConName -> Text
forall a. Name a -> Text
nameOcc TyConName
a2Nm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
"Clash.Signal.Internal.KnownDomain"
  isHidden Name a
_ [Type]
_ = Bool
False

  splitTy :: TypeView -> Bool
splitTy (TyConApp TyConName
tcNm0 [Type]
_)
    = TyConName -> Text
forall a. Name a -> Text
nameOcc TyConName
tcNm0 Text -> [Text] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [ Text
"Clash.Signal.Internal.Clock"
                           , Text
"Clash.Signal.Internal.ClockN"
                           , Text
"Clash.Signal.Internal.Reset"
                           , Text
"Clash.Signal.Internal.Enable"
                           -- iverilog doesn't like it when we put file handles
                           -- in a bitvector, so we need to make sure Clash
                           -- splits them off
                           , Text
"Clash.Explicit.SimIO.File"
                           , Text
"GHC.IO.Handle.Types.Handle"
                           ]
  splitTy TypeView
_ = Bool
False

shouldSplit0 TyConMap
_ TypeView
_ = Maybe ([Term] -> Term, Projections, [Type])
forall a. Maybe a
Nothing

-- | 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.
splitShouldSplit
  :: TyConMap
  -> [Type]
  -> [Type]
splitShouldSplit :: TyConMap -> [Type] -> [Type]
splitShouldSplit TyConMap
tcm = (Type -> [Type] -> [Type]) -> [Type] -> [Type] -> [Type]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> [Type] -> [Type]
go []
 where
  go :: Type -> [Type] -> [Type]
go Type
ty [Type]
rest = case TyConMap -> Type -> Maybe ([Term] -> Term, Projections, [Type])
shouldSplit TyConMap
tcm Type
ty of
    Just ([Term] -> Term
_,Projections
_,[Type]
tys) -> TyConMap -> [Type] -> [Type]
splitShouldSplit TyConMap
tcm [Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
rest
    Maybe ([Term] -> Term, Projections, [Type])
Nothing        -> Type
ty Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
rest

-- | Strip implicit parameter wrappers (IP)
stripIP :: Type -> Type
stripIP :: Type -> Type
stripIP t :: Type
t@(Type -> TypeView
tyView -> TyConApp TyConName
tcNm [Type
_a1, Type
a2]) =
  if TyConName -> Unique
forall a. Name a -> Unique
nameUniq TyConName
tcNm Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Unique
getKey Unique
ipClassKey then Type
a2 else Type
t
stripIP Type
t = Type
t

-- | Do an inverse topological sorting of the let-bindings in a let-expression
inverseTopSortLetBindings
  :: HasCallStack
  => [(Id, Term)]
  -> [(Id, Term)]
inverseTopSortLetBindings :: [LetBinding] -> [LetBinding]
inverseTopSortLetBindings [LetBinding]
bndrs0 =
  let (Graph
graph,Unique -> (LetBinding, Unique, [Unique])
nodeMap,Unique -> Maybe Unique
_) =
        [(LetBinding, Unique, [Unique])]
-> (Graph, Unique -> (LetBinding, Unique, [Unique]),
    Unique -> Maybe Unique)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Unique -> (node, key, [key]), key -> Maybe Unique)
Graph.graphFromEdges
          ((LetBinding -> (LetBinding, Unique, [Unique]))
-> [LetBinding] -> [(LetBinding, Unique, [Unique])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Id
i,Term
e) -> let fvs :: [Unique]
fvs = (Id -> Unique) -> [Id] -> [Unique]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> Unique
forall a. Var a -> Unique
varUniq
                                    (Set Id -> [Id]
forall a. Set a -> [a]
Set.elems (Getting (Set Id) Term Id -> Term -> Set Id
forall a s. Getting (Set a) s a -> s -> Set a
Lens.setOf Getting (Set Id) Term Id
Fold Term Id
freeLocalIds Term
e) )
                          in  ((Id
i,Term
e),Id -> Unique
forall a. Var a -> Unique
varUniq Id
i,[Unique]
fvs)) [LetBinding]
bndrs0)
      nodes :: [Unique]
nodes  = Graph -> [Unique]
postOrd Graph
graph
      bndrs1 :: [LetBinding]
bndrs1 = (Unique -> LetBinding) -> [Unique] -> [LetBinding]
forall a b. (a -> b) -> [a] -> [b]
map ((\(LetBinding
x,Unique
_,[Unique]
_) -> LetBinding
x) ((LetBinding, Unique, [Unique]) -> LetBinding)
-> (Unique -> (LetBinding, Unique, [Unique]))
-> Unique
-> LetBinding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> (LetBinding, Unique, [Unique])
nodeMap) [Unique]
nodes
   in [LetBinding]
bndrs1
 where
  postOrd :: Graph.Graph -> [Graph.Vertex]
  postOrd :: Graph -> [Unique]
postOrd Graph
g = Forest Unique -> [Unique] -> [Unique]
forall a. Forest a -> [a] -> [a]
postorderF (Graph -> Forest Unique
Graph.dff Graph
g) []

  postorderF :: Graph.Forest a -> [a] -> [a]
  postorderF :: Forest a -> [a] -> [a]
postorderF Forest a
ts = (([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a])
-> ([a] -> [a]) -> [[a] -> [a]] -> [a] -> [a]
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) [a] -> [a]
forall a. a -> a
id ((Tree a -> [a] -> [a]) -> Forest a -> [[a] -> [a]]
forall a b. (a -> b) -> [a] -> [b]
map Tree a -> [a] -> [a]
forall a. Tree a -> [a] -> [a]
postorder Forest a
ts)

  postorder :: Graph.Tree a -> [a] -> [a]
  postorder :: Tree a -> [a] -> [a]
postorder (Graph.Node a
a [Tree a]
ts) = [Tree a] -> [a] -> [a]
forall a. Forest a -> [a] -> [a]
postorderF [Tree a]
ts ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
:)
{-# SCC inverseTopSortLetBindings #-}

-- | Group let-bindings into cyclic groups and acyclic individual bindings
sccLetBindings
  :: HasCallStack
  => [(Id, Term)]
  -> [Graph.SCC (Id, Term)]
sccLetBindings :: [LetBinding] -> [SCC LetBinding]
sccLetBindings =
  [(LetBinding, Unique, [Unique])] -> [SCC LetBinding]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
Graph.stronglyConnComp ([(LetBinding, Unique, [Unique])] -> [SCC LetBinding])
-> ([LetBinding] -> [(LetBinding, Unique, [Unique])])
-> [LetBinding]
-> [SCC LetBinding]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  ((LetBinding -> (LetBinding, Unique, [Unique]))
-> [LetBinding] -> [(LetBinding, Unique, [Unique])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Id
i,Term
e) -> let fvs :: [Unique]
fvs = (Id -> Unique) -> [Id] -> [Unique]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> Unique
forall a. Var a -> Unique
varUniq
                            (Set Id -> [Id]
forall a. Set a -> [a]
Set.elems (Getting (Set Id) Term Id -> Term -> Set Id
forall a s. Getting (Set a) s a -> s -> Set a
Lens.setOf Getting (Set Id) Term Id
Fold Term Id
freeLocalIds Term
e) )
                  in  ((Id
i,Term
e),Id -> Unique
forall a. Var a -> Unique
varUniq Id
i,[Unique]
fvs)))
{-# SCC sccLetBindings #-}

-- | Make a case-decomposition that extracts a field out of a (Sum-of-)Product type
mkSelectorCase
  :: HasCallStack
  => MonadUnique m
  => String -- ^ Name of the caller of this function
  -> InScopeSet
  -> TyConMap -- ^ TyCon cache
  -> Term -- ^ Subject of the case-composition
  -> Int -- ^ n'th DataCon
  -> Int -- ^ n'th field
  -> m Term
mkSelectorCase :: [Char]
-> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
mkSelectorCase [Char]
caller InScopeSet
inScope TyConMap
tcm Term
scrut Unique
dcI Unique
fieldI = Type -> m Term
go (TyConMap -> Term -> Type
forall a. InferType a => TyConMap -> a -> Type
inferCoreTypeOf TyConMap
tcm Term
scrut)
  where
    go :: Type -> m Term
go (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
tcm -> Just Type
ty') = Type -> m Term
go Type
ty'
    go scrutTy :: Type
scrutTy@(Type -> TypeView
tyView -> TyConApp TyConName
tc [Type]
args) =
      case TyCon -> [DataCon]
tyConDataCons (TyConName -> TyConMap -> TyCon
forall a b. Uniquable a => a -> UniqMap b -> b
UniqMap.find TyConName
tc TyConMap
tcm) of
        [] -> [Char] -> [Char] -> Type -> m Term
forall a. [Char] -> [Char] -> Type -> a
cantCreate $([Char]
curLoc) ([Char]
"TyCon has no DataCons: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyConName -> [Char]
forall a. Show a => a -> [Char]
show TyConName
tc [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyConName -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr TyConName
tc) Type
scrutTy
        [DataCon]
dcs | Unique
dcI Unique -> Unique -> Bool
forall a. Ord a => a -> a -> Bool
> [DataCon] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [DataCon]
dcs -> [Char] -> [Char] -> Type -> m Term
forall a. [Char] -> [Char] -> Type -> a
cantCreate $([Char]
curLoc) [Char]
"DC index exceeds max" Type
scrutTy
            | Bool
otherwise -> do
          let dc :: DataCon
dc = [Char] -> [DataCon] -> Unique -> DataCon
forall a. HasCallStack => [Char] -> [a] -> Unique -> a
indexNote ($([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"No DC with tag: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Unique -> [Char]
forall a. Show a => a -> [Char]
show (Unique
dcIUnique -> Unique -> Unique
forall a. Num a => a -> a -> a
-Unique
1)) [DataCon]
dcs (Unique
dcIUnique -> Unique -> Unique
forall a. Num a => a -> a -> a
-Unique
1)
          let fieldTys :: [Type]
fieldTys =
                [Type] -> Maybe [Type] -> [Type]
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> [Char] -> Type -> [Type]
forall a. [Char] -> [Char] -> Type -> a
cantCreate $([Char]
curLoc) [Char]
"Cannot instantiate dataCon" Type
scrutTy)
                          (HasCallStack =>
InScopeSet -> TyConMap -> DataCon -> [Type] -> Maybe [Type]
InScopeSet -> TyConMap -> DataCon -> [Type] -> Maybe [Type]
dataConInstArgTysE InScopeSet
inScope TyConMap
tcm DataCon
dc [Type]
args)
          if Unique
fieldI Unique -> Unique -> Bool
forall a. Ord a => a -> a -> Bool
>= [Type] -> Unique
forall (t :: Type -> Type) a. Foldable t => t a -> Unique
length [Type]
fieldTys
            then [Char] -> [Char] -> Type -> m Term
forall a. [Char] -> [Char] -> Type -> a
cantCreate $([Char]
curLoc) [Char]
"Field index exceed max" Type
scrutTy
            else do
              [Id]
wildBndrs <- (Type -> m Id) -> [Type] -> m [Id]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (InScopeSet -> Type -> m Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Type -> m Id
mkWildValBinder InScopeSet
inScope) [Type]
fieldTys
              let ty :: Type
ty = [Char] -> [Type] -> Unique -> Type
forall a. HasCallStack => [Char] -> [a] -> Unique -> a
indexNote ($([Char]
curLoc) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"No DC field#: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Unique -> [Char]
forall a. Show a => a -> [Char]
show Unique
fieldI) [Type]
fieldTys Unique
fieldI
              Id
selBndr <- InScopeSet -> Text -> Type -> m Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Text -> Type -> m Id
mkInternalVar InScopeSet
inScope Text
"sel" Type
ty
              let bndrs :: [Id]
bndrs  = Unique -> [Id] -> [Id]
forall a. Unique -> [a] -> [a]
take Unique
fieldI [Id]
wildBndrs [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id
selBndr] [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ Unique -> [Id] -> [Id]
forall a. Unique -> [a] -> [a]
drop (Unique
fieldIUnique -> Unique -> Unique
forall a. Num a => a -> a -> a
+Unique
1) [Id]
wildBndrs
                  pat :: Pat
pat    = DataCon -> [TyVar] -> [Id] -> Pat
DataPat DataCon
dc (DataCon -> [TyVar]
dcExtTyVars DataCon
dc) [Id]
bndrs
                  retVal :: Term
retVal = Term -> Type -> [Alt] -> Term
Case Term
scrut Type
ty [ (Pat
pat, Id -> Term
Var Id
selBndr) ]
              Term -> m Term
forall (m :: Type -> Type) a. Monad m => a -> m a
return Term
retVal
    go Type
scrutTy = [Char] -> [Char] -> Type -> m Term
forall a. [Char] -> [Char] -> Type -> a
cantCreate $([Char]
curLoc) ([Char]
"Type of subject is not a datatype: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr Type
scrutTy) Type
scrutTy

    cantCreate :: String -> String -> Type -> a
    cantCreate :: [Char] -> [Char] -> Type -> a
cantCreate [Char]
loc [Char]
info Type
scrutTy = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
loc [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"Can't create selector " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ ([Char], Unique, Unique) -> [Char]
forall a. Show a => a -> [Char]
show ([Char]
caller,Unique
dcI,Unique
fieldI) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" for: (" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Term -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr Term
scrut [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" :: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Type -> [Char]
forall p. PrettyPrec p => p -> [Char]
showPpr Type
scrutTy [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
")\nAdditional info: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
info

-- | Make a binder that should not be referenced
mkWildValBinder
  :: (MonadUnique m)
  => InScopeSet
  -> Type
  -> m Id
mkWildValBinder :: InScopeSet -> Type -> m Id
mkWildValBinder InScopeSet
is = InScopeSet -> Text -> Type -> m Id
forall (m :: Type -> Type).
MonadUnique m =>
InScopeSet -> Text -> Type -> m Id
mkInternalVar InScopeSet
is Text
"wild"

-- | Make a new, unique, identifier
mkInternalVar
  :: (MonadUnique m)
  => InScopeSet
  -> OccName
  -- ^ Name of the identifier
  -> KindOrType
  -> m Id
mkInternalVar :: InScopeSet -> Text -> Type -> m Id
mkInternalVar InScopeSet
inScope Text
name Type
ty = do
  Unique
i <- m Unique
forall (m :: Type -> Type). MonadUnique m => m Unique
getUniqueM
  let nm :: TmName
nm = Text -> Unique -> TmName
forall a. Text -> Unique -> Name a
mkUnsafeInternalName Text
name Unique
i
  Id -> m Id
forall (m :: Type -> Type) a. Monad m => a -> m a
return (InScopeSet -> Id -> Id
forall a. (Uniquable a, ClashPretty a) => InScopeSet -> a -> a
uniqAway InScopeSet
inScope (Type -> TmName -> Id
mkLocalId Type
ty TmName
nm))