    {-|
      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 a b. (a -> b -> b) -> b -> [a] -> b
    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]
    _ -> String -> Type
    forall a. HasCallStack => String -> a
    error String
    "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]
    _ -> String -> Type
    forall a. HasCallStack => String -> a
    error String
    "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]
    _ -> String -> Type
    forall a. HasCallStack => String -> a
    error String
    "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 :: HasCallStack =>
    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 a b c. (a -> b) -> (a, c) -> (b, c)
    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
        String -> (Supply, NonEmpty (Term, NonEmpty LetBinding))
    forall a. HasCallStack => String -> a
    error String
    "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 (String
    -> ((Supply, InScopeSet), NonEmpty (Term, NonEmpty LetBinding))
    forall a. HasCallStack => String -> a
    error String
    "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. HasCallStack => [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 a. a -> Maybe a
    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) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    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. [a] -> [b] -> [(a, b)]
    zipEqual
            [Text
    "el" Text -> Text -> Text
    `T.append` (Char
    s Char -> Text -> Text
    `T.cons` String -> Text
    T.pack (Integer -> String
    forall a. Show a => a -> String
    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` String -> Text
    T.pack (Integer -> String
    forall a. Show a => a -> String
    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 b c a. (b -> c) -> (a, b) -> (a, c)
    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 a. a -> Maybe a
    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 a b c. (a -> b) -> (a, c) -> (b, c)
    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 (String -> ((Supply, InScopeSet), ([Term], [LetBinding]))
    forall a. HasCallStack => String -> a
    error String
    "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 a. a -> Maybe a
    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) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    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. [a] -> [b] -> [(a, b)]
    zipEqual
            [ Text
    "el" Text -> Text -> Text
    `T.append` (Char
    s Char -> Text -> Text
    `T.cons` String -> Text
    T.pack (Unique -> String
    forall a. Show a => a -> String
    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 a. a -> Maybe a
    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 (String -> ((Supply, InScopeSet), ([Term], [LetBinding]))
    forall a. HasCallStack => String -> a
    error String
    "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 a. a -> Maybe a
    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 a. [a] -> 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. HasCallStack => [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 a. a -> Maybe a
    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) s a b.
    Traversable t =>
    (s -> a -> (s, b)) -> s -> t a -> (s, t b)
    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. [a] -> [b] -> [(a, b)]
    zipEqual
            [Text
    "lt" Text -> Text -> Text
    `T.append` (Char
    s Char -> Text -> Text
    `T.cons` String -> Text
    T.pack (Unique -> String
    forall a. Show a => a -> String
    show Unique
    b0))
            ,Text
    "rt" Text -> Text -> Text
    `T.append` (Char
    s Char -> Text -> Text
    `T.cons` String -> Text
    T.pack (Unique -> String
    forall a. Show a => a -> String
    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 a. [a] -> 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 a. a -> Maybe a
    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 a. [a] -> 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]
    _ -> String -> Type
    forall a. HasCallStack => String -> a
    error String
    "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]
    _ -> String -> Type
    forall a. HasCallStack => String -> a
    error String
    "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 -> String -> Bool -> Bool
    forall a. Bool -> String -> a -> a
    traceIf Bool
    True ($(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 -> 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 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 a. a -> ExceptT String Identity a
    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
    $ $(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)
    -> (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 :: HasCallStack =>
    InScopeSet -> TyConMap -> DataCon -> [Type] -> Maybe [Type]
    dataConInstArgTysE InScopeSet
    is0 TyConMap
    tcm (MkData { [Type]
    dcArgTys :: [Type]
    dcArgTys :: DataCon -> [Type]
    dcArgTys, [TyVar]
    dcExtTyVars :: [TyVar]
    dcExtTyVars :: DataCon -> [TyVar]
    dcExtTyVars, [TyVar]
    dcUnivTyVars :: [TyVar]
    dcUnivTyVars :: DataCon -> [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. [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. [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 :: DataCon -> [Type]
    dcArgTys :: [Type]
    dcArgTys, [TyVar]
    dcUnivTyVars :: DataCon -> [TyVar]
    dcUnivTyVars :: [TyVar]
    dcUnivTyVars, [TyVar]
    dcExtTyVars :: DataCon -> [TyVar]
    dcExtTyVars :: [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 a. [a] -> 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 a. [a] -> 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 { 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. [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 a. a -> ExceptT String Identity a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return String
    s
    tyLitShow TyConMap
    _ (LitTy (NumTy Integer
    s))        = String -> Except String String
    forall a. a -> ExceptT String Identity a
    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
    $ $(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

    -- | 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 a. [a] -> 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])
    -> ([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)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [b]
    mapM (String
    -> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
    forall (m :: Type -> Type).
    (HasCallStack, MonadUnique m) =>
    String
    -> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
    mkSelectorCase ($(curLoc) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "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 String Integer -> Either String Integer
    forall e a. Except e a -> Either e a
    runExcept (TyConMap -> Type -> Except String 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)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [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 :: forall (m :: Type -> Type).
    MonadUnique m =>
    InScopeSet -> Term -> Integer -> m Term
    mkVecSelector InScopeSet
    is0 Term
    subj Integer
    0 =
        String
    -> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
    forall (m :: Type -> Type).
    (HasCallStack, MonadUnique m) =>
    String
    -> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
    mkSelectorCase ($(curLoc) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "mkVecSelector") InScopeSet
    is0 TyConMap
    tcm Term
    subj Unique
    2 Unique
    1

      mkVecSelector InScopeSet
    is0 Term
    subj !Integer
    n = do
        Term
    subj1 <- String
    -> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
    forall (m :: Type -> Type).
    (HasCallStack, MonadUnique m) =>
    String
    -> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
    mkSelectorCase ($(curLoc) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "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 practice 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 :: forall a. 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 a. Eq a => a -> [a] -> 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 a b. (a -> b -> b) -> b -> [a] -> b
    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 :: HasCallStack => [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 a b. (a -> b) -> [a] -> [b]
    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 :: forall a. Forest a -> [a] -> [a]
    postorderF Forest a
    ts = (([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a])
    -> ([a] -> [a]) -> [[a] -> [a]] -> [a] -> [a]
    forall a b. (a -> b -> b) -> b -> [a] -> b
    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 :: forall a. 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 :)
    {-# SCC inverseTopSortLetBindings #-}

    -- | Group let-bindings into cyclic groups and acyclic individual bindings
    sccLetBindings
      :: HasCallStack
      => [(Id, Term)]
      -> [Graph.SCC (Id, Term)]
    sccLetBindings :: HasCallStack => [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 a b. (a -> b) -> [a] -> [b]
    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 :: forall (m :: Type -> Type).
    (HasCallStack, MonadUnique m) =>
    String
    -> InScopeSet -> TyConMap -> Term -> Unique -> Unique -> m Term
    mkSelectorCase String
    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
            [] -> String -> String -> Type -> m Term
    forall a. String -> String -> Type -> a
    cantCreate $(curLoc) (String
    "TyCon has no DataCons: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ TyConName -> String
    forall a. Show a => a -> String
    show TyConName
    tc String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ TyConName -> String
    forall p. PrettyPrec p => p -> String
    showPpr TyConName
    tc) Type
    scrutTy
            [DataCon]
    dcs | Unique
    dcI Unique -> Unique -> Bool
    forall a. Ord a => a -> a -> Bool
    > [DataCon] -> Unique
    forall a. [a] -> Unique
    forall (t :: Type -> Type) a. Foldable t => t a -> Unique
    length [DataCon]
    dcs -> String -> String -> Type -> m Term
    forall a. String -> String -> Type -> a
    cantCreate $(curLoc) String
    "DC index exceeds max" Type
    scrutTy
                | Bool
    otherwise -> do
              let dc :: DataCon
    dc = String -> [DataCon] -> Unique -> DataCon
    forall a. HasCallStack => String -> [a] -> Unique -> a
    indexNote ($(curLoc) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "No DC with tag: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Unique -> String
    forall a. Show a => a -> String
    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 (String -> String -> Type -> [Type]
    forall a. String -> String -> Type -> a
    cantCreate $(curLoc) String
    "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 a. [a] -> Unique
    forall (t :: Type -> Type) a. Foldable t => t a -> Unique
    length [Type]
    fieldTys
                then String -> String -> Type -> m Term
    forall a. String -> String -> Type -> a
    cantCreate $(curLoc) String
    "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)
    forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> [a] -> m [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 = String -> [Type] -> Unique -> Type
    forall a. HasCallStack => String -> [a] -> Unique -> a
    indexNote ($(curLoc) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "No DC field#: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Unique -> String
    forall a. Show a => a -> String
    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 a. a -> m a
    forall (m :: Type -> Type) a. Monad m => a -> m a
    return Term
    retVal
        go Type
    scrutTy = String -> String -> Type -> m Term
    forall a. String -> String -> Type -> a
    cantCreate $(curLoc) (String
    "Type of subject is not a datatype: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Type -> String
    forall p. PrettyPrec p => p -> String
    showPpr Type
    scrutTy) Type
    scrutTy

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

    -- | Make a binder that should not be referenced
    mkWildValBinder
      :: (MonadUnique m)
      => InScopeSet
      -> Type
      -> m Id
    mkWildValBinder :: forall (m :: Type -> Type).
    MonadUnique m =>
    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 :: forall (m :: Type -> Type).
    MonadUnique m =>
    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 a. a -> m a
    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))