diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,12 @@ # Changelog for the [`clash-lib`](http://hackage.haskell.org/package/clash-lib) package +## 0.6 *October 3rd 2015* +* New features: + * Support for `clash-prelude` 0.10 + * Add `~INDEXTYPE` tag: primitives get access to the `Index` clash-prelude type + * Add `~IF` construct: primitives can do conditional templating + * Unroll "definitions" of the following primitives: `fold`, `dfold`, `foldr` + ## 0.5.13 *September 21st 2015* * Fixes bugs: * Performance bug: top-level definitions of type "Signal" erroneously inlined. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -11,8 +11,8 @@ Features of CλaSH: * Strongly typed (like VHDL), yet with a very high degree of type inference, - which enables both safe and fast prototying using consise descriptions (like - Verilog) + enabling both safe and fast prototying using consise descriptions (like + Verilog). * Interactive REPL: load your designs in an interpreter and easily test all your component without needing to setup a test bench. @@ -21,7 +21,7 @@ fully parametric by default. * Synchronous sequential circuit design based on streams of values, called - `Signal`s. + `Signal`s, lead to natural descriptions of feedback loops. * Support for multiple clock domains, with type safe clock domain crossing. diff --git a/clash-lib.cabal b/clash-lib.cabal --- a/clash-lib.cabal +++ b/clash-lib.cabal @@ -1,5 +1,5 @@ Name: clash-lib -Version: 0.5.13 +Version: 0.6 Synopsis: CAES Language for Synchronous Hardware - As a Library Description: CλaSH (pronounced ‘clash’) is a functional hardware description language that @@ -10,8 +10,8 @@ Features of CλaSH: . * Strongly typed (like VHDL), yet with a very high degree of type inference, - which enables both safe and fast prototying using consise descriptions (like - Verilog) + enabling both safe and fast prototying using consise descriptions (like + Verilog). . * Interactive REPL: load your designs in an interpreter and easily test all your component without needing to setup a test bench. @@ -20,7 +20,7 @@ fully parametric by default. . * Synchronous sequential circuit design based on streams of values, called - @Signal@s. + @Signal@s, lead to natural descriptions of feedback loops. . * Support for multiple clock domains, with type safe clock domain crossing. . @@ -89,7 +89,7 @@ attoparsec >= 0.10.4.0, base >= 4.8 && < 5, bytestring >= 0.10.0.2, - clash-prelude >= 0.8, + clash-prelude >= 0.10, concurrent-supply >= 0.1.7, containers >= 0.5.0.0, deepseq >= 1.3.0.2, @@ -140,6 +140,7 @@ CLaSH.Netlist.Util CLaSH.Normalize + CLaSH.Normalize.PrimitiveReductions CLaSH.Normalize.Strategy CLaSH.Normalize.Transformations CLaSH.Normalize.Types diff --git a/src/CLaSH/Core/Util.hs b/src/CLaSH/Core/Util.hs --- a/src/CLaSH/Core/Util.hs +++ b/src/CLaSH/Core/Util.hs @@ -258,6 +258,28 @@ ,resTy ,(LitTy (NumTy (n-1)))]) +-- | Append elements to the supplied vector +appendToVec :: DataCon -- ^ The Cons (:>) constructor + -> Type -- ^ Element type + -> Term -- ^ The vector to append the elements to + -> Int -- ^ Length of the vector + -> [Term] -- ^ Elements to append + -> Term +appendToVec consCon resTy vec = go + where + go _ [] = vec + go n (x:xs) = mkApps (Data consCon) [Right (LitTy (NumTy n)) + ,Right resTy + ,Right (LitTy (NumTy (n-1))) + ,Left (Prim "_CO_" (consCoTy n)) + ,Left x + ,Left (go (n-1) xs)] + + consCoTy n = head (fromJust $! dataConInstArgTys consCon + [(LitTy (NumTy n)) + ,resTy + ,(LitTy (NumTy (n-1)))]) + -- | Create let-bindings with case-statements that select elements out of a -- vector. Returns both the variables to which element-selections are bound -- and the let-bindings diff --git a/src/CLaSH/Netlist.hs b/src/CLaSH/Netlist.hs --- a/src/CLaSH/Netlist.hs +++ b/src/CLaSH/Netlist.hs @@ -303,7 +303,7 @@ case appF of Data dc | all (\e -> isConstant e || isVar e) tmArgs -> mkDcApplication hwTy dc tmArgs - | otherwise -> error $ $(curLoc) ++ "Not in normal form: DataCon-application with non-Simple arguments" + | otherwise -> error $ $(curLoc) ++ "Not in normal form: DataCon-application with non-Simple arguments: " ++ showDoc app Prim nm _ -> mkPrimitive False bbEasD nm args ty Var _ f | null tmArgs -> return (Identifier (mkBasicId . Text.pack $ name2String f) Nothing,[]) diff --git a/src/CLaSH/Netlist/BlackBox/Parser.hs b/src/CLaSH/Netlist/BlackBox/Parser.hs --- a/src/CLaSH/Netlist/BlackBox/Parser.hs +++ b/src/CLaSH/Netlist/BlackBox/Parser.hs @@ -36,7 +36,10 @@ -- | Parse a Declaration or Expression element pTagD :: Parser Element -pTagD = D <$> pDecl +pTagD = IF <$> (pTokenWS "~IF" *> pTagE) + <*> (pSpaces *> (pToken "~THEN" *> pBlackBoxD)) + <*> (pToken "~ELSE" *> pBlackBoxD <* pToken "~FI") + <|> D <$> pDecl <|> pTagE -- | Parse a Declaration @@ -69,6 +72,7 @@ <|> Err Nothing <$ pToken "~ERRORO" <|> (Err . Just) <$> (pToken "~ERROR" *> pBrackets pNatural) <|> TypElem <$> (pToken "~TYPEL" *> pBrackets pTagE) + <|> IndexType <$> (pToken "~INDEXTYPE" *> pBrackets pTagE) <|> CompName <$ pToken "~COMPNAME" <|> Size <$> (pToken "~SIZE" *> pBrackets pTagE) <|> Length <$> (pToken "~LENGTH" *> pBrackets pTagE) diff --git a/src/CLaSH/Netlist/BlackBox/Types.hs b/src/CLaSH/Netlist/BlackBox/Types.hs --- a/src/CLaSH/Netlist/BlackBox/Types.hs +++ b/src/CLaSH/Netlist/BlackBox/Types.hs @@ -22,11 +22,14 @@ | TypElem !Element -- ^ Select element type from a vector type | CompName -- ^ Hole for the name of the component in which -- the blackbox is instantiated + | IndexType !Element -- ^ Index data type hole, the field is the + -- (exclusive) maximum index | Size !Element -- ^ Size of a type hole | Length !Element -- ^ Length of a vector hole | FilePath !Element -- ^ Hole containing a filepath for a data file | Gen !Bool -- ^ Hole marking beginning (True) or end (False) -- of a generative construct + | IF !Element [Element] [Element] | SigD [Element] !(Maybe Int) deriving Show diff --git a/src/CLaSH/Netlist/BlackBox/Util.hs b/src/CLaSH/Netlist/BlackBox/Util.hs --- a/src/CLaSH/Netlist/BlackBox/Util.hs +++ b/src/CLaSH/Netlist/BlackBox/Util.hs @@ -1,7 +1,8 @@ +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ViewPatterns #-} -- | Utilties to verify blackbox contexts against templates and rendering -- filled in templates @@ -79,6 +80,7 @@ return (Sym k) Just k -> return (Sym k) D (Decl n l') -> D <$> (Decl n <$> mapM (combineM setSym' setSym') l') + IF c t f -> IF <$> pure c <*> setSym' t <*> setSym' f SigD e' m -> SigD <$> (setSym' e') <*> pure m _ -> pure e ) @@ -98,6 +100,7 @@ setClocks bc bt = mapM setClocks' bt where setClocks' (D (Decl n l)) = D <$> (Decl n <$> mapM (combineM (setClocks bc) (setClocks bc)) l) + setClocks' (IF c t f) = IF <$> pure c <*> setClocks bc t <*> setClocks bc f setClocks' (SigD e m) = SigD <$> (setClocks bc e) <*> pure m setClocks' (Clk Nothing) = let (clk,rate) = clkSyncId $ fst $ bbResult bc @@ -186,6 +189,18 @@ t <- hdlSig e' ty return (displayT $ renderOneLine t) +renderElem b (IF c t f) = do + let c' = case c of + (Size e) -> typeSize (lineToType b [e]) + (Length e) -> case lineToType b [e] of + (Vector n _) -> n + _ -> error $ $(curLoc) ++ "IF: veclen of a non-vector type" + (L n) -> case bbInputs b !! n of + (either id fst -> Literal _ (NumLit i),_,_) -> fromInteger i + _ -> error $ $(curLoc) ++ "IF: LIT must be a numeric lit" + _ -> error $ $(curLoc) ++ "IF: condition must be: SIZE, LENGHT, or LIT" + if c' > 0 then renderBlackBox t b else renderBlackBox f b + renderElem b e = renderTag b e parseFail :: Text -> BlackBoxTemplate @@ -218,6 +233,11 @@ lineToType b [(TypElem t)] = case lineToType b [t] of Vector _ elTy -> elTy _ -> error $ $(curLoc) ++ "Element type selection of a non-vector type" +lineToType b [(IndexType (L n))] = + case bbInputs b !! n of + (Left (Literal _ (NumLit n')),_,_) -> Index (fromInteger n') + x -> error $ $(curLoc) ++ "Index type not given a literal: " ++ show x + lineToType _ _ = error $ $(curLoc) ++ "Unexpected type manipulation" -- | Give a context and a tagged hole (of a template), returns part of the @@ -252,9 +272,11 @@ renderTag b e@(TypElem _) = let ty = lineToType b [e] in (displayT . renderOneLine) <$> hdlType ty renderTag _ (Gen b) = displayT . renderOneLine <$> genStmt b +renderTag _ (IF _ _ _) = error $ $(curLoc) ++ "Unexpected IF" renderTag _ (D _) = error $ $(curLoc) ++ "Unexpected component declaration" renderTag _ (SigD _ _) = error $ $(curLoc) ++ "Unexpected signal declaration" renderTag _ (Clk _) = error $ $(curLoc) ++ "Unexpected clock" renderTag _ (Rst _) = error $ $(curLoc) ++ "Unexpected reset" renderTag _ CompName = error $ $(curLoc) ++ "Unexpected component name" +renderTag _ (IndexType _) = error $ $(curLoc) ++ "Unexpected index type" renderTag _ (FilePath _) = error $ $(curLoc) ++ "Unexpected file name" diff --git a/src/CLaSH/Netlist/Util.hs b/src/CLaSH/Netlist/Util.hs --- a/src/CLaSH/Netlist/Util.hs +++ b/src/CLaSH/Netlist/Util.hs @@ -158,18 +158,20 @@ -> HashMap TyConName TyCon -> Type -> Bool -representableType builtInTranslation m = either (const False) (const True) . coreTypeToHWType builtInTranslation m +representableType builtInTranslation m = either (const False) ((> 0) . typeSize) . coreTypeToHWType builtInTranslation m -- | Determines the bitsize of a type typeSize :: HWType -> Int -typeSize Void = 1 +typeSize Void = 0 typeSize Bool = 1 typeSize (Clock _ _) = 1 typeSize (Reset _ _) = 1 typeSize Integer = 32 typeSize (BitVector i) = i -typeSize (Index u) = clog2 (max 2 u) +typeSize (Index 0) = 0 +typeSize (Index 1) = 1 +typeSize (Index u) = clog2 u typeSize (Signed i) = i typeSize (Unsigned i) = i typeSize (Vector n el) = n * typeSize el diff --git a/src/CLaSH/Normalize.hs b/src/CLaSH/Normalize.hs --- a/src/CLaSH/Normalize.hs +++ b/src/CLaSH/Normalize.hs @@ -20,7 +20,7 @@ import CLaSH.Core.Pretty (showDoc) import CLaSH.Core.Subst (substTms) import CLaSH.Core.Term (Term (..), TmName) -import CLaSH.Core.Type (Type) +import CLaSH.Core.Type (Type, splitFunForallTy) import CLaSH.Core.TyCon (TyCon, TyConName) import CLaSH.Core.Util (collectArgs, mkApps, termType) import CLaSH.Core.Var (Id,varName) @@ -36,7 +36,8 @@ import CLaSH.Rewrite.Types (DebugLevel (..), RewriteEnv (..), RewriteState (..), bindings, curFun, dbgLevel, tcCache, extra) -import CLaSH.Rewrite.Util (runRewrite, +import CLaSH.Rewrite.Util (isUntranslatableType, + runRewrite, runRewriteSession) import CLaSH.Util @@ -97,20 +98,38 @@ exprM <- HashMap.lookup nm <$> Lens.use bindings let nmS = showDoc nm case exprM of - Just (_,tm) -> do - tmNorm <- makeCached nm (extra.normalized) $ do - curFun .= nm - tm' <- rewriteExpr ("normalization",normalization) (nmS,tm) - tcm <- Lens.view tcCache - ty' <- termType tcm tm' - return (ty',tm') - let usedBndrs = Lens.toListOf termFreeIds (snd tmNorm) - traceIf (nm `elem` usedBndrs) - ($(curLoc) ++ "Expr belonging to bndr: " ++ nmS ++ " (:: " ++ showDoc (fst tmNorm) ++ ") remains recursive after normalization:\n" ++ showDoc (snd tmNorm)) - (return ()) - prevNorm <- fmap HashMap.keys $ Lens.use (extra.normalized) - let toNormalize = filter (`notElem` (nm:prevNorm)) usedBndrs - return (toNormalize,(nm,tmNorm)) + Just (ty,tm) -> do + let (_,resTy) = splitFunForallTy ty + resTyRep <- not <$> isUntranslatableType resTy + if resTyRep + then do + tmNorm <- makeCached nm (extra.normalized) $ do + curFun .= nm + tm' <- rewriteExpr ("normalization",normalization) (nmS,tm) + tcm <- Lens.view tcCache + ty' <- termType tcm tm' + return (ty',tm') + let usedBndrs = Lens.toListOf termFreeIds (snd tmNorm) + traceIf (nm `elem` usedBndrs) + (concat [ $(curLoc),"Expr belonging to bndr: ",nmS ," (:: " + , showDoc (fst tmNorm) + , ") remains recursive after normalization:\n" + , showDoc (snd tmNorm) ]) + (return ()) + prevNorm <- fmap HashMap.keys $ Lens.use (extra.normalized) + let toNormalize = filter (`notElem` (nm:prevNorm)) usedBndrs + return (toNormalize,(nm,tmNorm)) + else do + let usedBndrs = Lens.toListOf termFreeIds tm + prevNorm <- fmap HashMap.keys $ Lens.use (extra.normalized) + let toNormalize = filter (`notElem` (nm:prevNorm)) usedBndrs + lvl <- Lens.view dbgLevel + traceIf (lvl >= DebugFinal) + (concat [$(curLoc), "Expr belonging to bndr: ", nmS, " (:: " + , showDoc ty + , ") has a non-representable return type." + , " Not normalising:\n", showDoc tm] ) + (return (toNormalize,(nm,(ty,tm)))) Nothing -> error $ $(curLoc) ++ "Expr belonging to bndr: " ++ nmS ++ " not found" -- | Rewrite a term according to the provided transformation diff --git a/src/CLaSH/Normalize/PrimitiveReductions.hs b/src/CLaSH/Normalize/PrimitiveReductions.hs new file mode 100644 --- /dev/null +++ b/src/CLaSH/Normalize/PrimitiveReductions.hs @@ -0,0 +1,388 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskell #-} + +-- | Reductions of primitives +-- +-- Currently, it contains reductions for: +-- +-- * CLaSH.Sized.Vector.map +-- * CLaSH.Sized.Vector.zipWith +-- * CLaSH.Sized.Vector.traverse# +-- * CLaSH.Sized.Vector.foldr +-- * CLaSH.Sized.Vector.fold +-- * CLaSH.Sized.Vector.dfold +-- * CLaSH.Sized.Vector.(++) +-- * CLaSH.Sized.Vector.head +-- * CLaSH.Sized.Vector.tail +-- * CLaSH.Sized.Vector.unconcatBitVector# +-- +-- Partially handles: +-- +-- * CLaSH.Sized.Vector.unconcat +-- * CLaSH.Sized.Vector.transpose +module CLaSH.Normalize.PrimitiveReductions where + +import qualified Control.Lens as Lens +import qualified Data.HashMap.Lazy as HashMap +import qualified Data.Maybe as Maybe +import Unbound.Generics.LocallyNameless (bind, embed, rec, rebind, + string2Name) + +import CLaSH.Core.DataCon (DataCon, dataConInstArgTys) +import CLaSH.Core.Term (Term (..), Pat (..)) +import CLaSH.Core.Type (LitTy (..), Type (..), + TypeView (..), mkFunTy, + mkTyConApp, splitFunForallTy, + tyView) +import CLaSH.Core.TyCon (TyConName, tyConDataCons) +import CLaSH.Core.TysPrim (typeNatKind) +import CLaSH.Core.Util (appendToVec, extractElems, + idToVar, mkApps, mkVec, + termType) +import CLaSH.Core.Var (Var (..)) + +import CLaSH.Normalize.Types +import CLaSH.Rewrite.Types +import CLaSH.Rewrite.Util +import CLaSH.Util + +-- import CLaSH.Core.Pretty + +-- | Replace an application of the @CLaSH.Sized.Vector.zipWith@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.zipWith@ +reduceZipWith :: Int -- ^ Length of the vector(s) + -> Type -- ^ Type of the lhs of the function + -> Type -- ^ Type of the rhs of the function + -> Type -- ^ Type of the result of the function + -> Term -- ^ The zipWith'd functions + -> Term -- ^ The 1st vector argument + -> Term -- ^ The 2nd vector argument + -> NormalizeSession Term +reduceZipWith n lhsElTy rhsElTy resElTy fun lhsArg rhsArg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm lhsArg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [nilCon,consCon] = tyConDataCons vecTc + (varsL,elemsL) = second concat . unzip + $ extractElems consCon lhsElTy 'L' n lhsArg + (varsR,elemsR) = second concat . unzip + $ extractElems consCon rhsElTy 'R' n rhsArg + funApps = zipWith (\l r -> mkApps fun [Left l,Left r]) varsL varsR + lbody = mkVec nilCon consCon resElTy n funApps + lb = Letrec (bind (rec (init elemsL ++ init elemsR)) lbody) + changed lb + +-- | Replace an application of the @CLaSH.Sized.Vector.map@ primitive on vectors +-- of a known length @n@, by the fully unrolled recursive "definition" of +-- @CLaSH.Sized.Vector.map@ +reduceMap :: Int -- ^ Length of the vector + -> Type -- ^ Argument type of the function + -> Type -- ^ Result type of the function + -> Term -- ^ The map'd function + -> Term -- ^ The map'd over vector + -> NormalizeSession Term +reduceMap n argElTy resElTy fun arg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm arg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [nilCon,consCon] = tyConDataCons vecTc + (vars,elems) = second concat . unzip + $ extractElems consCon argElTy 'A' n arg + funApps = map (fun `App`) vars + lbody = mkVec nilCon consCon resElTy n funApps + lb = Letrec (bind (rec (init elems)) lbody) + changed lb + +-- | Replace an application of the @CLaSH.Sized.Vector.traverse#@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.traverse#@ +reduceTraverse :: Int -- ^ Length of the vector + -> Type -- ^ Element type of the argument vector + -> Type -- ^ The type of the applicative + -> Type -- ^ Element type of the result vector + -> Term -- ^ The @Applicative@ dictionary + -> Term -- ^ The function to traverse with + -> Term -- ^ The argument vector + -> NormalizeSession Term +reduceTraverse n aTy fTy bTy dict fun arg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm arg + (TyConApp apDictTcNm _) <- tyView <$> termType tcm dict + let (Just apDictTc) = HashMap.lookup apDictTcNm tcm + [apDictCon] = tyConDataCons apDictTc + (Just apDictIdTys) = dataConInstArgTys apDictCon [fTy] + apDictIds = zipWith Id (map string2Name ["functorDict" + ,"pure" + ,"ap" + ,"apConstL" + ,"apConstR"]) + (map embed apDictIdTys) + + (TyConApp funcDictTcNm _) = tyView (head apDictIdTys) + (Just funcDictTc) = HashMap.lookup funcDictTcNm tcm + [funcDictCon] = tyConDataCons funcDictTc + (Just funcDictIdTys) = dataConInstArgTys funcDictCon [fTy] + funcDicIds = zipWith Id (map string2Name ["fmap","fmapConst"]) + (map embed funcDictIdTys) + + apPat = DataPat (embed apDictCon) (rebind [] apDictIds) + fnPat = DataPat (embed funcDictCon) (rebind [] funcDicIds) + + -- Extract the 'pure' function from the Applicative dictionary + pureTy = apDictIdTys!!1 + pureTm = Case dict pureTy [bind apPat (Var pureTy (string2Name "pure"))] + + -- Extract the '<*>' function from the Applicative dictionary + apTy = apDictIdTys!!2 + apTm = Case dict apTy [bind apPat (Var apTy (string2Name "ap"))] + + -- Extract the Functor dictionary from the Applicative dictionary + funcTy = (head apDictIdTys) + funcTm = Case dict funcTy + [bind apPat (Var funcTy (string2Name "functorDict"))] + + -- Extract the 'fmap' function from the Functor dictionary + fmapTy = (head funcDictIdTys) + fmapTm = Case (Var funcTy (string2Name "functorDict")) fmapTy + [bind fnPat (Var fmapTy (string2Name "fmap"))] + + (Just vecTc) = HashMap.lookup vecTcNm tcm + [nilCon,consCon] = tyConDataCons vecTc + (vars,elems) = second concat . unzip + $ extractElems consCon aTy 'T' n arg + + funApps = map (fun `App`) vars + + lbody = mkTravVec vecTcNm nilCon consCon (idToVar (apDictIds!!1)) + (idToVar (apDictIds!!2)) + (idToVar (funcDicIds!!0)) + bTy n funApps + + lb = Letrec (bind (rec ([((apDictIds!!0),embed funcTm) + ,((apDictIds!!1),embed pureTm) + ,((apDictIds!!2),embed apTm) + ,((funcDicIds!!0),embed fmapTm) + ] ++ init elems)) lbody) + changed lb + +-- | Create the traversable vector +-- +-- e.g. for a length '2' input vector, we get +-- +-- > (:>) <$> x0 <*> ((:>) <$> x1 <*> pure Nil) +mkTravVec :: TyConName -- ^ Vec tcon + -> DataCon -- ^ Nil con + -> DataCon -- ^ Cons con + -> Term -- ^ 'pure' term + -> Term -- ^ '<*>' term + -> Term -- ^ 'fmap' term + -> Type -- ^ 'b' ty + -> Int -- ^ Length of the vector + -> [Term] -- ^ Elements of the vector + -> Term +mkTravVec vecTc nilCon consCon pureTm apTm fmapTm bTy = go + where + go :: Int -> [Term] -> Term + go _ [] = mkApps pureTm [Right (mkTyConApp vecTc [LitTy (NumTy 0),bTy]) + ,Left (mkApps (Data nilCon) + [Right (LitTy (NumTy 0)) + ,Right bTy + ,Left (Prim "_CO_" nilCoTy)])] + + go n (x:xs) = mkApps apTm + [Right (mkTyConApp vecTc [LitTy (NumTy (n-1)),bTy]) + ,Right (mkTyConApp vecTc [LitTy (NumTy n),bTy]) + ,Left (mkApps fmapTm [Right bTy + ,Right (mkFunTy (mkTyConApp vecTc [LitTy (NumTy (n-1)),bTy]) + (mkTyConApp vecTc [LitTy (NumTy n),bTy])) + ,Left (mkApps (Data consCon) + [Right (LitTy (NumTy n)) + ,Right bTy + ,Right (LitTy (NumTy (n-1))) + ,Left (Prim "_CO_" (consCoTy n)) + ]) + ,Left x]) + ,Left (go (n-1) xs)] + + nilCoTy = head (Maybe.fromJust (dataConInstArgTys nilCon [(LitTy (NumTy 0)) + ,bTy])) + + consCoTy n = head (Maybe.fromJust (dataConInstArgTys consCon + [(LitTy (NumTy n)) + ,bTy + ,(LitTy (NumTy (n-1)))])) + +-- | Replace an application of the @CLaSH.Sized.Vector.foldr@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.foldr@ +reduceFoldr :: Int -- ^ Length of the vector + -> Type -- ^ Element type of the argument vector + -> Type -- ^ Type of the starting element + -> Term -- ^ The function to fold with + -> Term -- ^ The starting value + -> Term -- ^ The argument vector + -> NormalizeSession Term +reduceFoldr n aTy _bTy fun start arg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm arg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [_,consCon] = tyConDataCons vecTc + (vars,elems) = second concat . unzip + $ extractElems consCon aTy 'G' n arg + lbody = foldr (\l r -> mkApps fun [Left l,Left r]) start vars + lb = Letrec (bind (rec (init elems)) lbody) + changed lb + +-- | Replace an application of the @CLaSH.Sized.Vector.fold@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.fold@ +reduceFold :: Int -- ^ Length of the vector + -> Type -- ^ Element type of the argument vector + -> Term -- ^ The function to fold with + -> Term -- ^ The argument vector + -> NormalizeSession Term +reduceFold n aTy fun arg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm arg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [_,consCon] = tyConDataCons vecTc + (vars,elems) = second concat . unzip + $ extractElems consCon aTy 'F' n arg + lbody = foldV vars + lb = Letrec (bind (rec (init elems)) lbody) + changed lb + where + foldV [a] = a + foldV as = let (l,r) = splitAt (length as `div` 2) as + lF = foldV l + rF = foldV r + in mkApps fun [Left lF, Left rF] + +-- | Replace an application of the @CLaSH.Sized.Vector.dfold@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.dfold@ +reduceDFold :: Int -- ^ Length of the vector + -> Type -- ^ Element type of the argument vector + -> Term -- ^ Function to fold with + -> Term -- ^ Starting value + -> Term -- ^ The vector to fold + -> NormalizeSession Term +reduceDFold n aTy fun start arg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm arg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [_,consCon] = tyConDataCons vecTc + (vars,elems) = second concat . unzip + $ extractElems consCon aTy 'D' n arg + ([_ltv,Right dsTy,_etaTy,_eta1Ty],_) <- splitFunForallTy <$> termType tcm fun + let (TyConApp proxyTcNm _) = tyView dsTy + (Just proxyTc) = HashMap.lookup proxyTcNm tcm + [proxyDc] = tyConDataCons proxyTc + lbody = doFold (Data proxyDc) (n-1) vars + lb = Letrec (bind (rec (init elems)) lbody) + changed lb + where + doFold _ _ [] = start + doFold pDc k (x:xs) = mkApps fun + [Right (LitTy (NumTy k)) + ,Left (mkApps pDc [Right typeNatKind + ,Right (LitTy (NumTy k))]) + ,Left x + ,Left (doFold pDc (k-1) xs) + ] + +-- | Replace an application of the @CLaSH.Sized.Vector.head@ primitive on +-- vectors of a known length @n@, by a projection of the first element of a +-- vector. +reduceHead :: Int -- ^ Length of the vector + -> Type -- ^ Element type of the vector + -> Term -- ^ The argument vector + -> NormalizeSession Term +reduceHead n aTy vArg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm vArg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [_,consCon] = tyConDataCons vecTc + (vars,elems) = second concat . unzip + $ extractElems consCon aTy 'H' n vArg + lb = Letrec (bind (rec [head elems]) (head vars)) + changed lb + +-- | Replace an application of the @CLaSH.Sized.Vector.tail@ primitive on +-- vectors of a known length @n@, by a projection of the tail of a +-- vector. +reduceTail :: Int -- ^ Length of the vector + -> Type -- ^ Element type of the vector + -> Term -- ^ The argument vector + -> NormalizeSession Term +reduceTail n aTy vArg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm vArg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [_,consCon] = tyConDataCons vecTc + (_,elems) = second concat . unzip + $ extractElems consCon aTy 'L' n vArg + b@(tB,_) = elems !! 1 + lb = Letrec (bind (rec [b]) (idToVar tB)) + changed lb + +-- | Replace an application of the @CLaSH.Sized.Vector.(++)@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.(++)@ +reduceAppend :: Int -- ^ Length of the LHS arg + -> Int -- ^ Lenght of the RHS arg + -> Type -- ^ Element type of the vectors + -> Term -- ^ The LHS argument + -> Term -- ^ The RHS argument + -> NormalizeSession Term +reduceAppend n m aTy lArg rArg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm lArg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [_,consCon] = tyConDataCons vecTc + (vars,elems) = second concat . unzip + $ extractElems consCon aTy 'C' n lArg + lbody = appendToVec consCon aTy rArg (n+m) vars + lb = Letrec (bind (rec (init elems)) lbody) + changed lb + +-- | Replace an application of the @CLaSH.Sized.Vector.unconcat@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.unconcat@ +reduceUnconcat :: Int -- ^ Length of the result vector + -> Int -- ^ Length of the elements of the result vector + -> Type -- ^ Element type + -> Term -- ^ Argument vector + -> NormalizeSession Term +reduceUnconcat n 0 aTy arg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm arg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [nilCon,consCon] = tyConDataCons vecTc + nilVec = mkVec nilCon consCon aTy 0 [] + innerVecTy = mkTyConApp vecTcNm [LitTy (NumTy 0), aTy] + retVec = mkVec nilCon consCon innerVecTy n (replicate n nilVec) + changed retVec + +reduceUnconcat _ _ _ _ = error $ $(curLoc) ++ "reduceUnconcat: unimplemented" + +-- | Replace an application of the @CLaSH.Sized.Vector.transpose@ primitive on +-- vectors of a known length @n@, by the fully unrolled recursive "definition" +-- of @CLaSH.Sized.Vector.transpose@ +reduceTranspose :: Int -- ^ Length of the result vector + -> Int -- ^ Length of the elements of the result vector + -> Type -- ^ Element type + -> Term -- ^ Argument vector + -> NormalizeSession Term +reduceTranspose n 0 aTy arg = do + tcm <- Lens.view tcCache + (TyConApp vecTcNm _) <- tyView <$> termType tcm arg + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [nilCon,consCon] = tyConDataCons vecTc + nilVec = mkVec nilCon consCon aTy 0 [] + innerVecTy = mkTyConApp vecTcNm [LitTy (NumTy 0), aTy] + retVec = mkVec nilCon consCon innerVecTy n (replicate n nilVec) + changed retVec + +reduceTranspose _ _ _ _ = error $ $(curLoc) ++ "reduceTranspose: unimplemented" diff --git a/src/CLaSH/Normalize/Strategy.hs b/src/CLaSH/Normalize/Strategy.hs --- a/src/CLaSH/Normalize/Strategy.hs +++ b/src/CLaSH/Normalize/Strategy.hs @@ -169,7 +169,7 @@ > f = \a x -> (a x) && (f a x) > f' = \x -> (not x) && (f not x) -Because f has already been specialised on the alpha-equivalent-to-itself not +Because `f` has already been specialised on the alpha-equivalent-to-itself `not` function, liftNonRep leads to: > main = f' diff --git a/src/CLaSH/Normalize/Transformations.hs b/src/CLaSH/Normalize/Transformations.hs --- a/src/CLaSH/Normalize/Transformations.hs +++ b/src/CLaSH/Normalize/Transformations.hs @@ -33,17 +33,17 @@ import qualified Control.Lens as Lens import qualified Control.Monad as Monad import Control.Monad.Writer (WriterT (..), lift, tell) +import Data.Bits ((.&.), complement) import qualified Data.Either as Either import qualified Data.HashMap.Lazy as HashMap import qualified Data.List as List import qualified Data.Maybe as Maybe -import Unbound.Generics.LocallyNameless (Bind, Embed (..), bind, embed, +import Unbound.Generics.LocallyNameless (Bind, Embed (..), bind, embed, rec, unbind, unembed, unrebind, - unrec, name2String, string2Name, - rebind) + unrec, name2String) import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) -import CLaSH.Core.DataCon (DataCon (..), dataConInstArgTys) +import CLaSH.Core.DataCon (DataCon (..)) import CLaSH.Core.FreeVars (termFreeIds, termFreeTyVars, typeFreeVars) import CLaSH.Core.Pretty (showDoc) @@ -54,10 +54,9 @@ LitTy (..), applyFunTy, applyTy, isPolyFunCoreTy, splitFunTy, typeKind, - tyView, mkTyConApp, mkFunTy) -import CLaSH.Core.TyCon (TyConName, tyConDataCons) -import CLaSH.Core.Util (collectArgs, extractElems, - idToVar, isCon, + tyView) +import CLaSH.Core.TyCon (tyConDataCons) +import CLaSH.Core.Util (collectArgs, idToVar, isCon, isFun, isLet, isPolyFun, isPrim, isSignalType, isVar, mkApps, mkLams, mkTmApps, mkVec, @@ -65,6 +64,7 @@ import CLaSH.Core.Var (Id, Var (..)) import CLaSH.Netlist.Util (representableType, splitNormalized) +import CLaSH.Normalize.PrimitiveReductions import CLaSH.Normalize.Types import CLaSH.Normalize.Util import CLaSH.Rewrite.Combinators @@ -271,6 +271,7 @@ changed (Letrec (bind binds (App appConPrim body))) (True,Case {}) -> specializeNorm ctx e (True,Lam _) -> specializeNorm ctx e + (True,TyLam _) -> specializeNorm ctx e _ -> return e nonRepANF _ e = return e @@ -737,10 +738,24 @@ -- * CLaSH.Sized.Vector.map -- * CLaSH.Sized.Vector.zipWith -- * CLaSH.Sized.Vector.traverse# +-- * CLaSH.Sized.Vector.foldr +-- * CLaSH.Sized.Vector.fold +-- * CLaSH.Sized.Vector.dfold +-- * CLaSH.Sized.Vector.(++) +-- * CLaSH.Sized.Vector.head +-- * CLaSH.Sized.Vector.tail reduceNonRepPrim :: NormRewrite -reduceNonRepPrim _ e@(App _ _) - | (Prim f _, args) <- collectArgs e - = case f of +reduceNonRepPrim _ e@(App _ _) | (Prim f _, args) <- collectArgs e = do + tcm <- Lens.view tcCache + eTy <- termType tcm e + case tyView eTy of + (TyConApp vecTcNm@(name2String -> "CLaSH.Sized.Vector.Vec") + [LitTy (NumTy 0), aTy]) -> do + let (Just vecTc) = HashMap.lookup vecTcNm tcm + [nilCon,consCon] = tyConDataCons vecTc + nilE = mkVec nilCon consCon aTy 0 [] + changed nilE + _ -> case f of "CLaSH.Sized.Vector.zipWith" | length args == 7 -> do let [lhsElTy,rhsElty,resElTy,nTy] = Either.rights args case nTy of @@ -768,168 +783,75 @@ let [dict,fun,arg] = Either.lefts args in reduceTraverse n aTy fTy bTy dict fun arg _ -> return e + "CLaSH.Sized.Vector.fold" | length args == 4 -> do + let [aTy,nTy] = Either.rights args + isPow2 x = x /= 0 && (x .&. (complement x + 1)) == x + untranslatableTy <- isUntranslatableType aTy + case nTy of + (LitTy (NumTy n)) | not (isPow2 (n + 1)) || untranslatableTy -> + let [fun,arg] = Either.lefts args + in reduceFold (n + 1) aTy fun arg + _ -> return e + "CLaSH.Sized.Vector.foldr" | length args == 6 -> + let [aTy,bTy,nTy] = Either.rights args + in case nTy of + (LitTy (NumTy n)) -> do + untranslatableTys <- mapM isUntranslatableType [aTy,bTy] + if or untranslatableTys + then let [fun,start,arg] = Either.lefts args + in reduceFoldr n aTy bTy fun start arg + else return e + _ -> return e + "CLaSH.Sized.Vector.dfold" | length args == 7 -> + let [_mTy,nTy,aTy] = Either.rights args + in case nTy of + (LitTy (NumTy n)) -> + let [_motive,fun,start,arg] = Either.lefts args + in reduceDFold n aTy fun start arg + _ -> return e + "CLaSH.Sized.Vector.++" | length args == 5 -> + let [nTy,aTy,mTy] = Either.rights args + [lArg,rArg] = Either.lefts args + in case (nTy,mTy) of + (LitTy (NumTy n), LitTy (NumTy m)) + | n == 0 -> changed rArg + | m == 0 -> changed lArg + | otherwise -> do + untranslatableTy <- isUntranslatableType aTy + if untranslatableTy + then reduceAppend n m aTy lArg rArg + else return e + _ -> return e + "CLaSH.Sized.Vector.head" | length args == 3 -> do + let [nTy,aTy] = Either.rights args + [vArg] = Either.lefts args + case nTy of + (LitTy (NumTy n)) -> do + untranslatableTy <- isUntranslatableType aTy + if untranslatableTy + then reduceHead n aTy vArg + else return e + _ -> return e + "CLaSH.Sized.Vector.tail" | length args == 3 -> do + let [nTy,aTy] = Either.rights args + [vArg] = Either.lefts args + case nTy of + (LitTy (NumTy n)) -> do + untranslatableTy <- isUntranslatableType aTy + if untranslatableTy + then reduceTail n aTy vArg + else return e + _ -> return e + "CLaSH.Sized.Vector.unconcat" | length args == 6 -> do + let ([_knN,_sm,arg],[mTy,nTy,aTy]) = Either.partitionEithers args + case (nTy,mTy) of + (LitTy (NumTy n), LitTy (NumTy 0)) -> reduceUnconcat n 0 aTy arg + _ -> return e + "CLaSH.Sized.Vector.transpose" | length args == 5 -> do + let ([_knN,arg],[mTy,nTy,aTy]) = Either.partitionEithers args + case (nTy,mTy) of + (LitTy (NumTy n), LitTy (NumTy 0)) -> reduceTranspose n 0 aTy arg + _ -> return e _ -> return e reduceNonRepPrim _ e = return e - --- | Replace an application of @CLaSH.Sized.Vector.zipWith@ primitive on vectors --- of a known length @n@, by the fully unrolled recursive "definition" of of --- @CLaSH.Sized.Vector.zipWith@ -reduceZipWith :: Int -- ^ Length of the vector(s) - -> Type -- ^ Type of the lhs of the function - -> Type -- ^ Type of the rhs of the function - -> Type -- ^ Type of the result of the function - -> Term -- ^ The zipWith'd functions - -> Term -- ^ The 1st vector argument - -> Term -- ^ The 2nd vector argument - -> NormalizeSession Term -reduceZipWith n lhsElTy rhsElTy resElTy fun lhsArg rhsArg = do - tcm <- Lens.view tcCache - (TyConApp vecTcNm _) <- tyView <$> termType tcm lhsArg - let (Just vecTc) = HashMap.lookup vecTcNm tcm - [nilCon,consCon] = tyConDataCons vecTc - (varsL,elemsL) = second concat . unzip $ extractElems consCon lhsElTy 'L' n lhsArg - (varsR,elemsR) = second concat . unzip $ extractElems consCon rhsElTy 'R' n rhsArg - funApps = zipWith (\l r -> mkApps fun [Left l,Left r]) varsL varsR - lbody = mkVec nilCon consCon resElTy n funApps - lb = Letrec (bind (rec (init elemsL ++ init elemsR)) lbody) - changed lb - --- | Replace an application of @CLaSH.Sized.Vector.map@ primitive on vectors --- of a known length @n@, by the fully unrolled recursive "definition" of of --- @CLaSH.Sized.Vector.map@ -reduceMap :: Int -- ^ Length of the vector - -> Type -- ^ Argument type of the function - -> Type -- ^ Result type of the function - -> Term -- ^ The map'd function - -> Term -- ^ The map'd over vector - -> NormalizeSession Term -reduceMap n argElTy resElTy fun arg = do - tcm <- Lens.view tcCache - (TyConApp vecTcNm _) <- tyView <$> termType tcm arg - let (Just vecTc) = HashMap.lookup vecTcNm tcm - [nilCon,consCon] = tyConDataCons vecTc - (vars,elems) = second concat . unzip $ extractElems consCon argElTy 'A' n arg - funApps = map (fun `App`) vars - lbody = mkVec nilCon consCon resElTy n funApps - lb = Letrec (bind (rec (init elems)) lbody) - changed lb - --- | Replace an application of @CLaSH.Sized.Vector.traverse#@ primitive on --- vectors of a known length @n@, by the fully unrolled recursive "definition" --- of @CLaSH.Sized.Vector.map@ -reduceTraverse :: Int -- ^ Length of the vector - -> Type -- ^ Element type of the argument vector - -> Type -- ^ The type of the applicative - -> Type -- ^ Element type of the result vector - -> Term -- ^ The @Applicative@ dictionary - -> Term -- ^ The function to traverse with - -> Term -- ^ The argument vector - -> NormalizeSession Term -reduceTraverse n aTy fTy bTy dict fun arg = do - tcm <- Lens.view tcCache - (TyConApp vecTcNm _) <- tyView <$> termType tcm arg - (TyConApp apDictTcNm _) <- tyView <$> termType tcm dict - let (Just apDictTc) = HashMap.lookup apDictTcNm tcm - [apDictCon] = tyConDataCons apDictTc - (Just apDictIdTys) = dataConInstArgTys apDictCon [fTy] - apDictIds = zipWith Id (map string2Name ["functorDict" - ,"pure" - ,"ap" - ,"apConstL" - ,"apConstR"]) - (map embed apDictIdTys) - - (TyConApp funcDictTcNm _) = tyView (head apDictIdTys) - (Just funcDictTc) = HashMap.lookup funcDictTcNm tcm - [funcDictCon] = tyConDataCons funcDictTc - (Just funcDictIdTys) = dataConInstArgTys funcDictCon [fTy] - funcDicIds = zipWith Id (map string2Name ["fmap","fmapConst"]) - (map embed funcDictIdTys) - - apPat = DataPat (embed apDictCon) (rebind [] apDictIds) - fnPat = DataPat (embed funcDictCon) (rebind [] funcDicIds) - - -- Extract the 'pure' function from the Applicative dictionary - pureTy = apDictIdTys!!1 - pureTm = Case dict pureTy [bind apPat (Var pureTy (string2Name "pure"))] - - -- Extract the '<*>' function from the Applicative dictionary - apTy = apDictIdTys!!2 - apTm = Case dict apTy [bind apPat (Var apTy (string2Name "ap"))] - - -- Extract the Functor dictionary from the Applicative dictionary - funcTy = (head apDictIdTys) - funcTm = Case dict funcTy - [bind apPat (Var funcTy (string2Name "functorDict"))] - - -- Extract the 'fmap' function from the Functor dictionary - fmapTy = (head funcDictIdTys) - fmapTm = Case (Var funcTy (string2Name "functorDict")) fmapTy - [bind fnPat (Var fmapTy (string2Name "fmap"))] - - (Just vecTc) = HashMap.lookup vecTcNm tcm - [nilCon,consCon] = tyConDataCons vecTc - (vars,elems) = second concat . unzip - $ extractElems consCon aTy 'T' n arg - - funApps = map (fun `App`) vars - - lbody = mkTravVec vecTcNm nilCon consCon (idToVar (apDictIds!!1)) - (idToVar (apDictIds!!2)) - (idToVar (funcDicIds!!0)) - bTy n funApps - - lb = Letrec (bind (rec ([((apDictIds!!0),embed funcTm) - ,((apDictIds!!1),embed pureTm) - ,((apDictIds!!2),embed apTm) - ,((funcDicIds!!0),embed fmapTm) - ] ++ init elems)) lbody) - changed lb - --- | Create the traversable vector --- --- e.g. for a length '2' input vector, we get --- --- > (:>) <$> x0 <*> ((:>) <$> x1 <*> pure Nil) -mkTravVec :: TyConName -- ^ Vec tcon - -> DataCon -- ^ Nil con - -> DataCon -- ^ Cons con - -> Term -- ^ 'pure' term - -> Term -- ^ '<*>' term - -> Term -- ^ 'fmap' term - -> Type -- ^ 'b' ty - -> Int -- ^ Length of the vector - -> [Term] -- ^ Elements of the vector - -> Term -mkTravVec vecTc nilCon consCon pureTm apTm fmapTm bTy = go - where - go :: Int -> [Term] -> Term - go _ [] = mkApps pureTm [Right (mkTyConApp vecTc [LitTy (NumTy 0),bTy]) - ,Left (mkApps (Data nilCon) - [Right (LitTy (NumTy 0)) - ,Right bTy - ,Left (Prim "_CO_" nilCoTy)])] - - go n (x:xs) = mkApps apTm - [Right (mkTyConApp vecTc [LitTy (NumTy (n-1)),bTy]) - ,Right (mkTyConApp vecTc [LitTy (NumTy n),bTy]) - ,Left (mkApps fmapTm [Right bTy - ,Right (mkFunTy (mkTyConApp vecTc [LitTy (NumTy (n-1)),bTy]) - (mkTyConApp vecTc [LitTy (NumTy n),bTy])) - ,Left (mkApps (Data consCon) - [Right (LitTy (NumTy n)) - ,Right bTy - ,Right (LitTy (NumTy (n-1))) - ,Left (Prim "_CO_" (consCoTy n)) - ]) - ,Left x]) - ,Left (go (n-1) xs)] - - nilCoTy = head (Maybe.fromJust (dataConInstArgTys nilCon [(LitTy (NumTy 0)) - ,bTy])) - - consCoTy n = head (Maybe.fromJust (dataConInstArgTys consCon - [(LitTy (NumTy n)) - ,bTy - ,(LitTy (NumTy (n-1)))])) diff --git a/src/CLaSH/Rewrite/Util.hs b/src/CLaSH/Rewrite/Util.hs --- a/src/CLaSH/Rewrite/Util.hs +++ b/src/CLaSH/Rewrite/Util.hs @@ -537,8 +537,16 @@ (specBndrs,specVars) <- specArgBndrsAndVars ctx (Left specArg) -- Create specialized function let newBody = mkAbstraction specArg specBndrs - cf <- Lens.use curFun - newf <- mkFunction (string2Name (name2String cf ++ "_" ++ "specF")) newBody + -- See if there's an existing binder that's alpha-equivalent to the + -- specialised function + existing <- HML.filter ((== newBody) . snd) <$> Lens.use bindings + -- Create a new function if an alpha-equivalent binder doesn't exist + newf <- case HML.toList existing of + [] -> do cf <- Lens.use curFun + mkFunction (string2Name (name2String cf ++ "_" ++ "specF")) newBody + ((k,(kTy,_)):_) -> return (k,kTy) + -- cf <- Lens.use curFun + -- newf <- mkFunction (string2Name (name2String cf ++ "_" ++ "specF")) newBody -- Create specialized argument let newArg = Left $ mkApps ((uncurry . flip) Var newf) specVars -- Use specialized argument