clash-lib-1.10.0: src/Clash/Normalize/Transformations/Reduce.hs
{-|
Copyright : (C) 2012-2016, University of Twente,
2016-2017, Myrtle Software Ltd,
2017-2018, Google Inc.,
2021-2022, QBayLogic B.V.
License : BSD2 (see the file LICENSE)
Maintainer : QBayLogic B.V. <devops@qbaylogic.com>
Transformations for compile-time reduction of expressions / primitives.
-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module Clash.Normalize.Transformations.Reduce
( reduceBinders
, reduceConst
, reduceNonRepPrim
) where
import qualified Control.Lens as Lens
import Control.Monad.Trans.Except (runExcept)
import qualified Data.Either as Either
import qualified Data.List as List
import qualified Data.List.Extra as List
import qualified Data.Maybe as Maybe
import Data.Maybe (fromMaybe, listToMaybe)
import GHC.Stack (HasCallStack)
import Clash.Core.FreeVars (typeFreeVars)
import Clash.Core.HasType
import Clash.Core.Name (nameOcc)
import Clash.Core.Pretty (showPpr)
import Clash.Core.Subst (Subst, extendIdSubst, substTm)
import Clash.Core.Term
( CoreContext(..), LetBinding, PrimInfo(..), Term(..), TickInfo(..), collectArgs
, collectArgsTicks, mkApps, mkTicks, mkTmApps)
import Clash.Core.TyCon (tyConDataCons)
import Clash.Core.Type (Type, TypeView(..), mkTyConApp, splitFunForallTy, tyView)
import Clash.Core.Util (mkVec, shouldSplit, tyNatSize, mkInternalVar)
import Clash.Core.VarEnv (extendInScopeSet)
import qualified Clash.Data.UniqMap as UniqMap
import Clash.Normalize.PrimitiveReductions
import Clash.Normalize.Primitives (removedArg)
import Clash.Normalize.Types (NormRewrite, NormalizeSession)
import Clash.Normalize.Util (shouldReduce)
import Clash.Rewrite.Types (TransformContext(..), tcCache, normalizeUltra)
import Clash.Rewrite.Util (changed, isUntranslatableType, setChanged, whnfRW)
-- | XXX: is given inverse topologically sorted binders, but returns
-- topologically sorted binders
--
-- TODO: check further speed improvements:
--
-- 1. Store the processed binders in a `Map Expr LetBinding`:
-- * Trades O(1) `cons` and O(n)*aeqTerm `find` for:
-- * O(log n)*aeqTerm `insert` and O(log n)*aeqTerm `lookup`
-- 2. Store the processed binders in a `AEQTrie Expr LetBinding`
-- * Trades O(1) `cons` and O(n)*aeqTerm `find` for:
-- * O(e) `insert` and O(e) `lookup`
reduceBinders
:: Subst
-> [LetBinding]
-> [LetBinding]
-> NormalizeSession (Subst, [LetBinding])
reduceBinders !subst processed [] = return (subst,processed)
reduceBinders !subst processed ((i,substTm "reduceBinders" subst -> e):rest)
| (_,_,ticks) <- collectArgsTicks e
, NoDeDup `notElem` ticks
, Just (i1,_) <- List.find ((== e) . snd) processed
= do
let subst1 = extendIdSubst subst i (Var i1)
setChanged
reduceBinders subst1 processed rest
| otherwise
= reduceBinders subst ((i,e):processed) rest
{-# SCC reduceBinders #-}
reduceConst :: HasCallStack => NormRewrite
reduceConst ctx e@(App _ _)
| (Prim p0, _) <- collectArgs e
= whnfRW False ctx e $ \_ctx1 e1 -> case e1 of
(collectArgs -> (Prim p1, _)) | primName p0 == primName p1 -> return e
_ -> changed e1
reduceConst _ e = return e
{-# SCC reduceConst #-}
-- | Replace primitives by their "definition" if they would lead to let-bindings
-- with a non-representable type when a function is in ANF. This happens for
-- example when Clash.Size.Vector.map consumes or produces a vector of
-- non-representable elements.
--
-- Basically what this transformation does is replace a primitive the completely
-- unrolled recursive definition that it represents. e.g.
--
-- > zipWith ($) (xs :: Vec 2 (Int -> Int)) (ys :: Vec 2 Int)
--
-- is replaced by:
--
-- > let (x0 :: (Int -> Int)) = case xs of (:>) _ x xr -> x
-- > (xr0 :: Vec 1 (Int -> Int)) = case xs of (:>) _ x xr -> xr
-- > (x1 :: (Int -> Int)( = case xr0 of (:>) _ x xr -> x
-- > (y0 :: Int) = case ys of (:>) _ y yr -> y
-- > (yr0 :: Vec 1 Int) = case ys of (:>) _ y yr -> xr
-- > (y1 :: Int = case yr0 of (:>) _ y yr -> y
-- > in (($) x0 y0 :> ($) x1 y1 :> Nil)
--
-- Currently, it only handles the following functions:
--
-- * Clash.Sized.Vector.zipWith
-- * Clash.Sized.Vector.map
-- * Clash.Sized.Vector.traverse#
-- * Clash.Sized.Vector.fold
-- * Clash.Sized.Vector.foldr
-- * Clash.Sized.Vector.dfold
-- * Clash.Sized.Vector.(++)
-- * Clash.Sized.Vector.head
-- * Clash.Sized.Vector.tail
-- * Clash.Sized.Vector.last
-- * Clash.Sized.Vector.init
-- * Clash.Sized.Vector.unconcat
-- * Clash.Sized.Vector.transpose
-- * Clash.Sized.Vector.replicate
-- * Clash.Sized.Vector.replace_int
-- * Clash.Sized.Vector.imap
-- * Clash.Sized.Vector.dtfold
-- * Clash.Sized.RTree.tdfold
-- * Clash.Sized.RTree.treplicate
-- * Clash.Sized.Internal.BitVector.split#
-- * Clash.Sized.Internal.BitVector.eq#
--
-- Note [Unroll shouldSplit types]
-- 1. Certain higher-order functions over Vec, such as map, have specialized
-- code-paths to turn them into generate-for loops in HDL, instead of having to
-- having to unroll/inline their recursive definitions, e.g. Clash.Sized.Vector.map
--
-- 2. Clash, in general, translates Haskell product types to VHDL records. This
-- mostly works out fine, there is however one exception: certain synthesis
-- tools, and some HDL simulation tools (like verilator), do not like it when
-- the clock (and certain other global control signals) is contained in a
-- record type; they want them to be separate inputs to the entity/module.
-- And Clash actually does some transformations to try to ensure that values of
-- type Clock do not end up in a VHDL record type.
--
-- The problem is that the transformations in 2. never took into account the
-- specialized code-paths in 1. Making the code-paths in 1. aware of the
-- transformations in 2. is really not worth the effort for such a niche case.
-- It's easier to just unroll the recursive definitions.
--
-- See https://github.com/clash-lang/clash-compiler/issues/1606
reduceNonRepPrim :: HasCallStack => NormRewrite
reduceNonRepPrim c@(TransformContext _ ctx) e@(App _ _) | (Prim p, args, ticks) <- collectArgsTicks e = do
tcm <- Lens.view tcCache
ultra <- Lens.view normalizeUltra
let eTy = inferCoreTypeOf tcm e
let resTy = snd (splitFunForallTy eTy)
case tyView resTy of
(TyConApp vecTcNm@(nameOcc -> "Clash.Sized.Vector.Vec")
[runExcept . tyNatSize tcm -> Right 0, aTy]) -> do
let nilE = fromMaybe (error "reduceNonRepPrim: unable to create Vec DCs") $ do
vecTc <- UniqMap.lookup vecTcNm tcm
[nilCon,consCon] <- pure (tyConDataCons vecTc)
return (mkVec nilCon consCon aTy 0 [])
changed (mkTicks nilE ticks)
tv -> let argLen = length args in case primName p of
"Clash.Sized.Vector.zipWith"
| (tmArgs,[lhsElTy,rhsElty,resElTy,nTy]) <- Either.partitionEithers args
, TyConApp vecTcNm _ <- tv
, let lhsTy = mkTyConApp vecTcNm [nTy,lhsElTy]
, let rhsTy = mkTyConApp vecTcNm [nTy,rhsElty]
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ pure (ultra || n < 2)
, shouldReduce ctx
, List.anyM isUntranslatableType_not_poly
[lhsElTy,rhsElty,resElTy]
-- Note [Unroll shouldSplit types]
, pure (any (Maybe.isJust . shouldSplit tcm)
[lhsTy,rhsTy,resTy]) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c
(reduceZipWith p n lhsElTy rhsElty resElTy)
else return e
_ -> return e
| argLen >= 4
-> error ("reduceNonRepPrim: zipWith bad args" <> showPpr e)
"Clash.Sized.Vector.map"
| (tmArgs,[argElTy,resElTy,nTy]) <- Either.partitionEithers args
, TyConApp vecTcNm _ <- tv
, let argTy = mkTyConApp vecTcNm [nTy,argElTy]
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ pure (ultra || n < 2 )
, shouldReduce ctx
, List.anyM isUntranslatableType_not_poly
[argElTy,resElTy]
-- Note [Unroll shouldSplit types]
, pure (any (Maybe.isJust . shouldSplit tcm)
[argTy,resTy]) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c
(reduceMap p n argElTy resElTy)
else return e
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: map bad args" <> showPpr e)
"Clash.Sized.Vector.traverse#"
| (tmArgs,[aTy,fTy,bTy,nTy]) <- Either.partitionEithers args
-> case runExcept (tyNatSize tcm nTy) of
Right n -> abstractOverMissingArgs ticks tmArgs eTy c (reduceTraverse n aTy fTy bTy)
_ -> return e
| argLen >= 4
-> error ("reduceNonRepPrim: traverse# bad args" <> showPpr e)
"Clash.Sized.Vector.fold"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
, (_:Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [nTy,aTy]))
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ pure (ultra || n == 0)
, shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy))]
if shouldReduce1 then
abstractOverMissingArgs ticks tmArgs eTy c (reduceFold (n + 1) aTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: fold bad args" <> showPpr e)
"Clash.Sized.Vector.foldr"
| (tmArgs,[aTy,bTy,nTy]) <- Either.partitionEithers args
, (_:_:Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [aTy,bTy,nTy]))
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ pure ultra
, shouldReduce ctx
, List.anyM isUntranslatableType_not_poly [aTy,bTy]
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy)) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceFoldr p n aTy)
else return e
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: foldr bad args" <> showPpr e)
"Clash.Sized.Vector.dfold"
| (tmArgs,[_mTy,nTy,aTy]) <- Either.partitionEithers args
-> case runExcept (tyNatSize tcm nTy) of
Right n -> abstractOverMissingArgs ticks tmArgs eTy c (reduceDFold n aTy)
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: dfold bad args" <> showPpr e)
"Clash.Sized.Vector.++"
| (tmArgs,[nTy,aTy,mTy]) <- Either.partitionEithers args
-> case (runExcept (tyNatSize tcm nTy), runExcept (tyNatSize tcm mTy)) of
(Right n, Right m) -> do
shouldReduce1 <- List.orM [ pure (n==0)
, pure (m==0)
, shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm resTy)) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceAppend n m aTy)
else return e
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: ++ bad args" <> showPpr e)
"Clash.Sized.Vector.head"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
, (Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [nTy,aTy]))
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy)) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceHead (n+1) aTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: head bad args" <> showPpr e)
"Clash.Sized.Vector.tail"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
, (Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [nTy,aTy]))
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy)) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceTail (n+1) aTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: tail bad args" <> showPpr e)
"Clash.Sized.Vector.last"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
, (Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [nTy,aTy]))
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy))
]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceLast (n+1) aTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: last bad args" <> showPpr e)
"Clash.Sized.Vector.init"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
, (Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [nTy,aTy]))
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy)) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceInit p n aTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: init bad args" <> showPpr e)
"Clash.Sized.Vector.unconcat"
| (tmArgs,[nTy,mTy,aTy]) <- Either.partitionEithers args
, (_:_:Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [nTy,mTy,aTy]))
-> case (runExcept (tyNatSize tcm nTy), runExcept (tyNatSize tcm mTy)) of
(Right n, Right m) -> do
shouldReduce1 <- List.orM [ pure (m==0)
, shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy))
]
if shouldReduce1 then
abstractOverMissingArgs ticks tmArgs eTy c (reduceUnconcat p n m aTy)
else
return e
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: unconcat bad args" <> showPpr e)
"Clash.Sized.Vector.transpose"
| (tmArgs,[mTy,nTy,aTy]) <- Either.partitionEithers args
-> case (runExcept (tyNatSize tcm nTy), runExcept (tyNatSize tcm mTy)) of
(Right n, Right 0) -> abstractOverMissingArgs ticks tmArgs eTy c (reduceTranspose n 0 aTy)
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: transpose bad args" <> showPpr e)
"Clash.Sized.Vector.replicate"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm resTy))
]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceReplicate n aTy resTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: replicate bad args" <> showPpr e)
-- replace_int :: KnownNat n => Vec n a -> Int -> a -> Vec n a
"Clash.Sized.Vector.replace_int"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ pure ultra
, shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm resTy))
]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceReplace_int n aTy resTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: replace_int bad args" <> showPpr e)
"Clash.Sized.Vector.index_int"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
, (_:Right argTy:_) <- fst (splitFunForallTy (piResultTys tcm (primType p) [nTy,aTy]))
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ pure ultra
, shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm argTy)) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceIndex_int n aTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: index_int bad args" <> showPpr e)
"Clash.Sized.Vector.imap"
| (tmArgs,[nTy,argElTy,resElTy]) <- Either.partitionEithers args
, TyConApp vecTcNm _ <- tv
, let argTy = mkTyConApp vecTcNm [nTy,argElTy]
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ pure (ultra || n < 2)
, shouldReduce ctx
, List.anyM isUntranslatableType_not_poly [argElTy,resElTy]
-- Note [Unroll shouldSplit types]
, pure (any (Maybe.isJust . shouldSplit tcm)
[argTy,resTy]) ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceImap n argElTy resElTy)
else return e
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: imap bad args" <> showPpr e)
"Clash.Sized.Vector.iterateI"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
-> case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM
[ pure (ultra || n < 2)
, shouldReduce ctx
, isUntranslatableType_not_poly aTy
-- Note [Unroll shouldSplit types]
, pure (Maybe.isJust (shouldSplit tcm resTy)) ]
if shouldReduce1 then
abstractOverMissingArgs ticks tmArgs eTy c (reduceIterateI n aTy resTy)
else
return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: iterateI bad args" <> showPpr e)
"Clash.Sized.Vector.dtfold"
| (tmArgs,[_mTy,nTy,aTy]) <- Either.partitionEithers args
-> case runExcept (tyNatSize tcm nTy) of
Right n -> abstractOverMissingArgs ticks tmArgs eTy c (reduceDTFold n aTy)
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: dtfold bad args" <> showPpr e)
"Clash.Sized.Vector.reverse"
| ultra
, (tmArgs,[nTy,aTy]) <- Either.partitionEithers args
, Right n <- runExcept (tyNatSize tcm nTy)
-> abstractOverMissingArgs ticks tmArgs eTy c (reduceReverse n aTy)
"Clash.Sized.RTree.tdfold"
| (tmArgs,[_mTy,nTy,aTy]) <- Either.partitionEithers args
-> case runExcept (tyNatSize tcm nTy) of
Right n -> abstractOverMissingArgs ticks tmArgs eTy c (reduceTFold n aTy)
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: tdfold bad args" <> showPpr e)
"Clash.Sized.RTree.treplicate"
| (tmArgs,[nTy,aTy]) <- Either.partitionEithers args ->
case runExcept (tyNatSize tcm nTy) of
Right n -> do
shouldReduce1 <- List.orM [ shouldReduce ctx
, isUntranslatableType False aTy ]
if shouldReduce1
then abstractOverMissingArgs ticks tmArgs eTy c (reduceTReplicate n aTy resTy)
else return e
_ -> return e
| argLen >= 2
-> error ("reduceNonRepPrim: treplicate bad args" <> showPpr e)
"Clash.Sized.Internal.BitVector.split#"
| (tmArgs,[nTy,mTy]) <- Either.partitionEithers args ->
case (runExcept (tyNatSize tcm nTy), runExcept (tyNatSize tcm mTy), tv) of
(Right n, Right m, TyConApp tupTcNm [lTy,rTy])
| n == 0 -> abstractOverMissingArgs ticks tmArgs eTy c $ \(_kn :: Term) bvArg (_ctx :: TransformContext) -> do
let tup = mkApps (Data tupDc)
[Right lTy
,Right rTy
,Left bvArg
,Left (TyApp (Prim removedArg) rTy)
]
(changed (mkTicks tup ticks) :: NormalizeSession Term)
| m == 0 -> abstractOverMissingArgs ticks tmArgs eTy c $ \(_kn :: Term) bvArg (_ctx :: TransformContext) -> do
let tup = mkApps (Data tupDc)
[Right lTy
,Right rTy
,Left (TyApp (Prim removedArg) lTy)
,Left bvArg
]
(changed (mkTicks tup ticks) :: NormalizeSession Term)
where
tupDc = fromMaybe (error "reduceNonRepPrim: faield to create tup DC") $ do
tupTc <- UniqMap.lookup tupTcNm tcm
listToMaybe (tyConDataCons tupTc)
_ -> return e
| argLen >= 3
-> error ("reduceNonRepPrim: split# bad args" <> showPpr e)
"Clash.Sized.Internal.BitVector.eq#"
| (tmArgs,[nTy]) <- Either.partitionEithers args
, Right 0 <- runExcept (tyNatSize tcm nTy)
, TyConApp boolTcNm [] <- tv
-> abstractOverMissingArgs ticks tmArgs eTy c $ \(_kn :: Term) (_l :: Term) (_r :: Term) (_ctx :: TransformContext) -> do
let trueDc = fromMaybe (error "reduceNonRepPrim: failed to create True DC") $ do
boolTc <- UniqMap.lookup boolTcNm tcm
[_falseDc,dc] <- pure (tyConDataCons boolTc)
return dc
in (changed (Data trueDc) :: NormalizeSession Term)
_ -> return e
where
isUntranslatableType_not_poly t = do
u <- isUntranslatableType False t
if u
then return (null $ Lens.toListOf typeFreeVars t)
else return False
reduceNonRepPrim _ e = return e
{-# SCC reduceNonRepPrim #-}
class AbstractOverMissingArgs a where
-- | Abstract over a primitive until it is saturated
abstractOverMissingArgs ::
HasCallStack =>
-- | Ticks originally tagged to the applied primitive
[TickInfo] ->
-- | Available arguments
[Term] ->
-- | The type of the expression containing the applied primitive
Type ->
-- | The context in which reduceNonRepPrim was called
TransformContext ->
a ->
NormalizeSession Term
instance AbstractOverMissingArgs (TransformContext -> NormalizeSession Term) where
abstractOverMissingArgs ticks args _ is f = (`mkTmApps` args) <$> (`mkTicks` ticks) <$> f is
instance AbstractOverMissingArgs a => AbstractOverMissingArgs (Term -> a) where
abstractOverMissingArgs ticks (t:ts) ty ctx f = abstractOverMissingArgs ticks ts ty ctx (f t)
abstractOverMissingArgs ticks [] (tyView -> FunTy argTy resTy) (TransformContext is0 ctx) f = do
newId <- mkInternalVar is0 "arg" argTy
let ctx1 = TransformContext (extendInScopeSet is0 newId) (LamBody newId : ctx)
Lam newId <$> abstractOverMissingArgs ticks [] resTy ctx1 (f (Var newId))
abstractOverMissingArgs _ _ ty _ _ = error ("not a funty: " <> showPpr ty)