{-|
  Copyright   :  (C) 2012-2016, University of Twente
  License     :  BSD2 (see the file LICENSE)
  Maintainer  :  Christiaan Baaij <christiaan.baaij@gmail.com>

  Smart constructor and destructor functions for CoreHW
-}

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

module Clash.Core.Util where

import           Control.Concurrent.Supply     (Supply, freshId)
import qualified Control.Lens                  as Lens
import Control.Monad.Trans.Except              (Except, throwE)
import qualified Data.HashSet                  as HashSet
import qualified Data.Graph                    as Graph
import Data.List                               (foldl', mapAccumR)
import Data.List.Extra                         (zipEqual)
import Data.Maybe
  (fromJust, isJust, mapMaybe, catMaybes)
import qualified Data.Set                      as Set
import qualified Data.Set.Lens                 as Lens
import qualified Data.Text                     as T
#if !MIN_VERSION_base(4,11,0)
import           Data.Semigroup
#endif

import           PrelNames               (ipClassKey)
import           Unique                  (getKey)

import Clash.Core.DataCon
import Clash.Core.EqSolver
import Clash.Core.FreeVars               (tyFVsOfTypes, typeFreeVars, freeLocalIds)
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                (typeNatKind)
import Clash.Core.Var                    (Id, Var(..), mkLocalId, mkTyVar)
import Clash.Core.VarEnv
import Clash.Debug                       (traceIf)
import Clash.Unique
import Clash.Util

-- | 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    = [Type] -> Type
forall a. [a] -> a
head (Maybe [Type] -> [Type]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Type] -> [Type]) -> Maybe [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$! DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
nilCon  [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0))
                                                             ,Type
resTy])
    consCoTy :: Integer -> Type
consCoTy Integer
n = [Type] -> Type
forall a. [a] -> a
head (Maybe [Type] -> [Type]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Type] -> [Type]) -> Maybe [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$! 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)))])

-- | 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 = [Type] -> Type
forall a. [a] -> a
head (Maybe [Type] -> [Type]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Type] -> [Type]) -> Maybe [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$! 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)))])

-- | 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
  :: 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])])
extractElems :: Supply
-> InScopeSet
-> DataCon
-> Type
-> Char
-> Integer
-> Term
-> (Supply, [(Term, [LetBinding])])
extractElems Supply
supply InScopeSet
inScope DataCon
consCon Type
resTy Char
s Integer
maxN Term
vec =
  ((Supply, InScopeSet) -> Supply)
-> ((Supply, InScopeSet), [(Term, [LetBinding])])
-> (Supply, [(Term, [LetBinding])])
forall (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Supply, InScopeSet) -> Supply
forall a b. (a, b) -> a
fst (Integer
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), [(Term, [LetBinding])])
go Integer
maxN (Supply
supply,InScopeSet
inScope) Term
vec)
 where
  go :: Integer -> (Supply,InScopeSet) -> Term
     -> ((Supply,InScopeSet),[(Term,[LetBinding])])
  go :: Integer
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), [(Term, [LetBinding])])
go Integer
0 (Supply, InScopeSet)
uniqs Term
_ = ((Supply, InScopeSet)
uniqs,[])
  go Integer
n (Supply, InScopeSet)
uniqs0 Term
e =
    ((Supply, InScopeSet)
uniqs3,(Term
elNVar,[(Id
elNId, Term
lhs),(Id
restNId, Term
rhs)])(Term, [LetBinding])
-> [(Term, [LetBinding])] -> [(Term, [LetBinding])]
forall a. a -> [a] -> [a]
:[(Term, [LetBinding])]
restVs)
   where
    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)))]
    (Just [Type]
idTys) = DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
consCon [Type]
tys
    restTy :: Type
restTy       = [Type] -> Type
forall a. [a] -> a
last [Type]
idTys

    ((Supply, InScopeSet)
uniqs1,TyVar
mTV) = (Supply, InScopeSet)
-> (OccName, Type) -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar (Supply, InScopeSet)
uniqs0 (OccName
"m",Type
typeNatKind)
    ((Supply, InScopeSet)
uniqs2,[Id
elNId,Id
restNId,Id
co,Id
el,Id
rest]) =
      ((Supply, InScopeSet)
 -> (OccName, Type) -> ((Supply, InScopeSet), Id))
-> (Supply, InScopeSet)
-> [(OccName, 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)
-> (OccName, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply, InScopeSet)
uniqs1 ([(OccName, Type)] -> ((Supply, InScopeSet), [Id]))
-> [(OccName, Type)] -> ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$ [OccName] -> [Type] -> [(OccName, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual
        [OccName
"el" OccName -> OccName -> OccName
`T.append` (Char
s Char -> OccName -> OccName
`T.cons` String -> OccName
T.pack (Integer -> String
forall a. Show a => a -> String
show (Integer
maxNInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n)))
        ,OccName
"rest" OccName -> OccName -> OccName
`T.append` (Char
s Char -> OccName -> OccName
`T.cons` String -> OccName
T.pack (Integer -> String
forall a. Show a => a -> String
show (Integer
maxNInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
n)))
        ,OccName
"_co_"
        ,OccName
"el"
        ,OccName
"rest"
        ]
        (Type
resTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Type
restTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
idTys)

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

    ((Supply, InScopeSet)
uniqs3,[(Term, [LetBinding])]
restVs) = Integer
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), [(Term, [LetBinding])])
go (Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
-Integer
1) (Supply, InScopeSet)
uniqs2 (Id -> Term
Var Id
restNId)

-- | 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],[LetBinding]))
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 (a :: Type -> Type -> Type) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Supply, InScopeSet) -> Supply
forall a b. (a, b) -> a
fst (Integer
-> [Int]
-> [Int]
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
go Integer
maxN [Int
0..(Int
2Int -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^(Integer
maxNInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1))Int -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2] [Int
0..(Int
2Int -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
maxN Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)] (Supply
supply,InScopeSet
inScope) Term
tree)
 where
  go :: Integer
     -> [Int]
     -> [Int]
     -> (Supply,InScopeSet)
     -> Term
     -> ((Supply,InScopeSet),([Term],[LetBinding]))
  go :: Integer
-> [Int]
-> [Int]
-> (Supply, InScopeSet)
-> Term
-> ((Supply, InScopeSet), ([Term], [LetBinding]))
go Integer
0 [Int]
_ [Int]
ks (Supply, InScopeSet)
uniqs0 Term
e = ((Supply, InScopeSet)
uniqs1,([Term
elNVar],[(Id
elNId, Term
rhs)]))
   where
    tys :: [Type]
tys          = [LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0),Type
resTy]
    (Just [Type]
idTys) = DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
lrCon [Type]
tys

    ((Supply, InScopeSet)
uniqs1,[Id
elNId,Id
co,Id
el]) =
      ((Supply, InScopeSet)
 -> (OccName, Type) -> ((Supply, InScopeSet), Id))
-> (Supply, InScopeSet)
-> [(OccName, 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)
-> (OccName, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply, InScopeSet)
uniqs0 ([(OccName, Type)] -> ((Supply, InScopeSet), [Id]))
-> [(OccName, Type)] -> ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$ [OccName] -> [Type] -> [(OccName, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual
        [ OccName
"el" OccName -> OccName -> OccName
`T.append` (Char
s Char -> OccName -> OccName
`T.cons` String -> OccName
T.pack (Int -> String
forall a. Show a => a -> String
show ([Int] -> Int
forall a. [a] -> a
head [Int]
ks)))
        , OccName
"_co_"
        , OccName
"el"
        ]
        (Type
resTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
idTys)
    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)]

  go Integer
n [Int]
bs [Int]
ks (Supply, InScopeSet)
uniqs0 Term
e =
    ((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)))
   where
    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))]
    (Just [Type]
idTys) = DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
brCon [Type]
tys

    ((Supply, InScopeSet)
uniqs1,TyVar
mTV) = (Supply, InScopeSet)
-> (OccName, Type) -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar (Supply, InScopeSet)
uniqs0 (OccName
"m",Type
typeNatKind)
    (Int
b0:[Int]
bL,Int
b1:[Int]
bR) = Int -> [Int] -> ([Int], [Int])
forall a. Int -> [a] -> ([a], [a])
splitAt ([Int] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Int]
bs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [Int]
bs
    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)
 -> (OccName, Type) -> ((Supply, InScopeSet), Id))
-> (Supply, InScopeSet)
-> [(OccName, 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)
-> (OccName, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply, InScopeSet)
uniqs1 ([(OccName, Type)] -> ((Supply, InScopeSet), [Id]))
-> [(OccName, Type)] -> ((Supply, InScopeSet), [Id])
forall a b. (a -> b) -> a -> b
$ [OccName] -> [Type] -> [(OccName, Type)]
forall a b. HasCallStack => [a] -> [b] -> [(a, b)]
zipEqual
        [OccName
"lt" OccName -> OccName -> OccName
`T.append` (Char
s Char -> OccName -> OccName
`T.cons` String -> OccName
T.pack (Int -> String
forall a. Show a => a -> String
show Int
b0))
        ,OccName
"rt" OccName -> OccName -> OccName
`T.append` (Char
s Char -> OccName -> OccName
`T.cons` String -> OccName
T.pack (Int -> String
forall a. Show a => a -> String
show Int
b1))
        ,OccName
"_co_"
        ,OccName
"lt"
        ,OccName
"rt"
        ]
        (Type
brTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:Type
brTyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
idTys)
    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)]

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

-- | 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) = Int -> [Term] -> ([Term], [Term])
forall a. Int -> [a] -> ([a], [a])
splitAt ([Term] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Term]
xs Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
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   = [Type] -> Type
forall a. [a] -> a
head (Maybe [Type] -> [Type]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Type] -> [Type]) -> Maybe [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$! DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys DataCon
lrCon  [(LitTy -> Type
LitTy (Integer -> LitTy
NumTy Integer
0))
                                                         ,Type
resTy])
    brCoTy :: Integer -> Type
brCoTy Integer
n = [Type] -> Type
forall a. [a] -> a
head (Maybe [Type] -> [Type]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [Type] -> [Type]) -> Maybe [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$! 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)))])

-- | 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 -> OccName
forall a. Name a -> OccName
nameOcc TyConName
tcNm of
      OccName
"Clash.Signal.Internal.Signal"      -> Bool
True
      OccName
"Clash.Signal.BiSignal.BiSignalIn"  -> Bool
True
      OccName
"Clash.Signal.Internal.BiSignalOut" -> Bool
True
      OccName
_ | 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
lookupUniqMap 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 -> String -> Bool -> Bool
forall a. Bool -> String -> a -> a
traceIf Bool
True ($(String
curLoc) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"isSignalType: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TyConName -> String
forall a. Show a => a -> String
show TyConName
tcNm
                                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 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 -> OccName
forall a. Name a -> OccName
nameOcc -> OccName
"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 -> OccName
forall a. Name a -> OccName
nameOcc TyConName
tcNm of
  OccName
"Clash.Signal.Internal.Clock" -> Bool
True
  OccName
"Clash.Signal.Internal.Reset" -> Bool
True
  OccName
_ -> Bool
False
isClockOrReset TyConMap
_ Type
_ = Bool
False

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


mkUniqSystemTyVar
  :: (Supply, InScopeSet)
  -> (OccName, Kind)
  -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar :: (Supply, InScopeSet)
-> (OccName, Type) -> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar (Supply
supply,InScopeSet
inScope) (OccName
nm, Type
ki) =
  ((Supply
supply',InScopeSet -> TyVar -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
inScope TyVar
v'), TyVar
v')
 where
  (Int
u,Supply
supply') = Supply -> (Int, Supply)
freshId Supply
supply
  v :: TyVar
v           = Type -> TyName -> TyVar
mkTyVar Type
ki (OccName -> Int -> TyName
forall a. OccName -> Int -> Name a
mkUnsafeSystemName OccName
nm Int
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)
-> (OccName, Type) -> ((Supply, InScopeSet), Id)
mkUniqSystemId (Supply
supply,InScopeSet
inScope) (OccName
nm, Type
ty) =
  ((Supply
supply',InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
inScope Id
v'), Id
v')
 where
  (Int
u,Supply
supply') = Supply -> (Int, Supply)
freshId Supply
supply
  v :: Id
v           = Type -> TmName -> Id
mkLocalId Type
ty (OccName -> Int -> TmName
forall a. OccName -> Int -> Name a
mkUnsafeSystemName OccName
nm Int
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)
-> (OccName, Type) -> ((Supply, InScopeSet), Id)
mkUniqInternalId (Supply
supply,InScopeSet
inScope) (OccName
nm, Type
ty) =
  ((Supply
supply',InScopeSet -> Id -> InScopeSet
forall a. InScopeSet -> Var a -> InScopeSet
extendInScopeSet InScopeSet
inScope Id
v'), Id
v')
 where
  (Int
u,Supply
supply') = Supply -> (Int, Supply)
freshId Supply
supply
  v :: Id
v           = Type -> TmName -> Id
mkLocalId Type
ty (OccName -> Int -> TmName
forall a. OccName -> Int -> Name a
mkUnsafeInternalName OccName
nm Int
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 (f :: Type -> Type). Foldable f => f Type -> VarSet
tyFVsOfTypes [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] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [TyVar]
tyvars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Type] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
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 (OccName -> Type -> WorkInfo -> PrimInfo
PrimInfo OccName
"_CO_" Type
ty WorkInfo
WorkNever)

-- | Make an undefined term
undefinedTm
  :: Type
  -> Term
undefinedTm :: Type -> Term
undefinedTm = Term -> Type -> Term
TyApp (PrimInfo -> Term
Prim (OccName -> Type -> WorkInfo -> PrimInfo
PrimInfo OccName
"Clash.Transformations.undefined" Type
undefinedTy WorkInfo
WorkNever))

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 = (VarSet -> VarSet -> VarSet) -> VarSet -> [VarSet] -> VarSet
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' VarSet -> VarSet -> VarSet
unionVarSet VarSet
emptyVarSet
                  ((Type -> VarSet) -> [Type] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (Getting VarSet Type TyVar -> (TyVar -> VarSet) -> Type -> VarSet
forall r s a. Getting r s a -> (a -> r) -> s -> r
Lens.foldMapOf Getting VarSet Type TyVar
Fold Type TyVar
typeFreeVars TyVar -> VarSet
forall a. Var a -> VarSet
unitVarSet) [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 String String
tyLitShow TyConMap
m (TyConMap -> Type -> Maybe Type
coreView1 TyConMap
m -> Just Type
ty) = TyConMap -> Type -> Except String String
tyLitShow TyConMap
m Type
ty
tyLitShow TyConMap
_ (LitTy (SymTy String
s))        = String -> Except String String
forall (m :: Type -> Type) a. Monad m => a -> m a
return String
s
tyLitShow TyConMap
_ (LitTy (NumTy Integer
s))        = String -> Except String String
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Integer -> String
forall a. Show a => a -> String
show Integer
s)
tyLitShow TyConMap
_ Type
ty = String -> Except String String
forall (m :: Type -> Type) e a. Monad m => e -> ExceptT e m a
throwE (String -> Except String String) -> String -> Except String String
forall a b. (a -> b) -> a -> b
$ $(String
curLoc) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Cannot reduce to a string:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type -> String
forall p. PrettyPrec p => p -> String
showPpr Type
ty

-- | 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,[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 2., creates a value of the examined type
  --
  -- 2. 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), [Int, (Clock, Bool)])
  --
  -- An outer loop is required to subsequently split the /(Clock, Bool)/ tuple.
shouldSplit :: TyConMap -> Type -> Maybe (Term, [Type])
shouldSplit TyConMap
tcm (Type -> TypeView
tyView ->  TyConApp (TyConName -> OccName
forall a. Name a -> OccName
nameOcc -> OccName
"Clash.Explicit.SimIO.SimIO") [Type
tyArg]) =
  -- We also look through `SimIO` to find things like Files
  TyConMap -> Type -> Maybe (Term, [Type])
shouldSplit TyConMap
tcm Type
tyArg
shouldSplit TyConMap
tcm Type
ty = TyConMap -> TypeView -> Maybe (Term, [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,[Type])
shouldSplit0 :: TyConMap -> TypeView -> Maybe (Term, [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
lookupUniqMap TyConName
tcNm TyConMap
tcm
  , [DataCon
dc] <- TyCon -> [DataCon]
tyConDataCons TyCon
tc
  , let dcArgs :: [Type]
dcArgs  = DataCon -> [Type] -> [Type]
substArgTys DataCon
dc [Type]
tyArgs
  , 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, [Type]) -> Maybe (Term, [Type])
forall a. a -> Maybe a
Just (Term -> [Either Term Type] -> Term
mkApps (DataCon -> Term
Data DataCon
dc) ((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), [Type]
dcArgs)
    else
      Maybe (Term, [Type])
forall a. Maybe a
Nothing
 where
  shouldSplitTy :: TypeView -> Bool
  shouldSplitTy :: TypeView -> Bool
shouldSplitTy TypeView
ty = Maybe (Term, [Type]) -> Bool
forall a. Maybe a -> Bool
isJust (TyConMap -> TypeView -> Maybe (Term, [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 -> OccName
forall a. Name a -> OccName
nameOcc Name a
nm OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
"GHC.Classes.(%,%)"
    Bool -> Bool -> Bool
&& TypeView -> Bool
splitTy (Type -> TypeView
tyView (Type -> Type
stripIP Type
a1))
    Bool -> Bool -> Bool
&& TyConName -> OccName
forall a. Name a -> OccName
nameOcc TyConName
a2Nm OccName -> OccName -> Bool
forall a. Eq a => a -> a -> Bool
== OccName
"Clash.Signal.Internal.KnownDomain"
  isHidden Name a
_ [Type]
_ = Bool
False

  -- Currently we're only interested in splitting of Clock, Reset, and Enable
  splitTy :: TypeView -> Bool
splitTy (TyConApp TyConName
tcNm0 [Type]
_)
    = TyConName -> OccName
forall a. Name a -> OccName
nameOcc TyConName
tcNm0 OccName -> [OccName] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` [ OccName
"Clash.Signal.Internal.Clock"
                           , OccName
"Clash.Signal.Internal.Reset"
                           , OccName
"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
                           , OccName
"Clash.Explicit.SimIO.File"
                           , OccName
"GHC.IO.Handle.Types.Handle"
                           ]
  splitTy TypeView
_ = Bool
False

shouldSplit0 TyConMap
_ TypeView
_ = Maybe (Term, [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, [Type])
shouldSplit TyConMap
tcm Type
ty of
    Just (Term
_,[Type]
tys) -> TyConMap -> [Type] -> [Type]
splitShouldSplit TyConMap
tcm [Type]
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
rest
    Maybe (Term, [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 -> Int
forall a. Name a -> Int
nameUniq TyConName
tcNm Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Unique -> Int
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
  => Term
  -> Term
inverseTopSortLetBindings :: Term -> Term
inverseTopSortLetBindings (Letrec [LetBinding]
bndrs0 Term
res) =
  let (Graph
graph,Int -> (LetBinding, Int, [Int])
nodeMap,Int -> Maybe Int
_) =
        [(LetBinding, Int, [Int])]
-> (Graph, Int -> (LetBinding, Int, [Int]), Int -> Maybe Int)
forall key node.
Ord key =>
[(node, key, [key])]
-> (Graph, Int -> (node, key, [key]), key -> Maybe Int)
Graph.graphFromEdges
          ((LetBinding -> (LetBinding, Int, [Int]))
-> [LetBinding] -> [(LetBinding, Int, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Id
i,Term
e) -> let fvs :: [Int]
fvs = (Id -> Int) -> [Id] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> Int
forall a. Var a -> Int
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 -> Int
forall a. Var a -> Int
varUniq Id
i,[Int]
fvs)) [LetBinding]
bndrs0)
      nodes :: [Int]
nodes  = Graph -> [Int]
postOrd Graph
graph
      bndrs1 :: [LetBinding]
bndrs1 = (Int -> LetBinding) -> [Int] -> [LetBinding]
forall a b. (a -> b) -> [a] -> [b]
map ((\(LetBinding
x,Int
_,[Int]
_) -> LetBinding
x) ((LetBinding, Int, [Int]) -> LetBinding)
-> (Int -> (LetBinding, Int, [Int])) -> Int -> LetBinding
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (LetBinding, Int, [Int])
nodeMap) [Int]
nodes
  in  [LetBinding] -> Term -> Term
Letrec [LetBinding]
bndrs1 Term
res
 where
  postOrd :: Graph.Graph -> [Graph.Vertex]
  postOrd :: Graph -> [Int]
postOrd Graph
g = Forest Int -> [Int] -> [Int]
forall a. Forest a -> [a] -> [a]
postorderF (Graph -> Forest Int
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 Forest a
ts) = Forest a -> [a] -> [a]
forall a. Forest a -> [a] -> [a]
postorderF Forest 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]
:)

inverseTopSortLetBindings Term
e = Term
e
{-# SCC inverseTopSortLetBindings #-}

-- | Group let-bindings into cyclic groups and acyclic individual bindings
sccLetBindings
  :: HasCallStack
  => [LetBinding]
  -> [Graph.SCC LetBinding]
sccLetBindings :: [LetBinding] -> [SCC LetBinding]
sccLetBindings =
  [(LetBinding, Int, [Int])] -> [SCC LetBinding]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
Graph.stronglyConnComp ([(LetBinding, Int, [Int])] -> [SCC LetBinding])
-> ([LetBinding] -> [(LetBinding, Int, [Int])])
-> [LetBinding]
-> [SCC LetBinding]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  ((LetBinding -> (LetBinding, Int, [Int]))
-> [LetBinding] -> [(LetBinding, Int, [Int])]
forall a b. (a -> b) -> [a] -> [b]
map (\(Id
i,Term
e) -> let fvs :: [Int]
fvs = (Id -> Int) -> [Id] -> [Int]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Id -> Int
forall a. Var a -> Int
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 -> Int
forall a. Var a -> Int
varUniq Id
i,[Int]
fvs)))
{-# SCC sccLetBindings #-}