clash-lib 0.5.13 → 0.6

raw patch · 14 files changed

+604/−206 lines, 14 filesdep ~clash-preludePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: clash-prelude

API changes (from Hackage documentation)

Files

• CHANGELOG.md +7/−0
• README.md +3/−3
• clash-lib.cabal +6/−5
• src/CLaSH/Core/Util.hs +22/−0
• src/CLaSH/Netlist.hs +1/−1
• src/CLaSH/Netlist/BlackBox/Parser.hs +5/−1
• src/CLaSH/Netlist/BlackBox/Types.hs +3/−0
• src/CLaSH/Netlist/BlackBox/Util.hs +23/−1
• src/CLaSH/Netlist/Util.hs +5/−3
• src/CLaSH/Normalize.hs +35/−16
• src/CLaSH/Normalize/PrimitiveReductions.hs +388/−0
• src/CLaSH/Normalize/Strategy.hs +1/−1
• src/CLaSH/Normalize/Transformations.hs +95/−173
• src/CLaSH/Rewrite/Util.hs +10/−2

@@ -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.

@@ -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. 

@@ -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

@@ -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

@@ -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,[])

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

@@ -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 

@@ -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"

@@ -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

@@ -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

@@ -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"

@@ -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'

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

@@ -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