packages feed

hardware-edsl 0.1.2 → 0.1.5

raw patch · 13 files changed

+1115/−418 lines, 13 files

Files

hardware-edsl.cabal view
@@ -1,5 +1,5 @@ name:                hardware-edsl-version:             0.1.2+version:             0.1.5 synopsis:            Deep embedding of hardware descriptions with code generation. description:         Deep embedding of hardware descriptions with code generation. license:             BSD3@@ -28,6 +28,7 @@     Language.Embedded.Hardware.Expression.Represent.Bit,     Language.Embedded.Hardware.Expression.Syntax,     Language.Embedded.Hardware.Interface,+    Language.Embedded.Hardware.Interface.AXI     Language.Embedded.Hardware.Command,     Language.Embedded.Hardware.Command.Backend.VHDL,     Language.Embedded.Hardware.Command.CMD,@@ -37,7 +38,6 @@     Language.Embedded.VHDL.Monad.Type,     Language.Embedded.VHDL.Monad.Expression     Language.Embedded.VHDL.Monad.Util---    Language.Embedded.Hardware.Common.AXI    --other-modules:
src/Language/Embedded/Hardware/Command.hs view
@@ -4,17 +4,22 @@ {-# LANGUAGE TypeOperators       #-} {-# LANGUAGE ConstraintKinds     #-} +{-# LANGUAGE GADTs #-}+ module Language.Embedded.Hardware.Command-  ( compile+  (+  -- Regular hardware compilers.+    compile   , icompile   , runIO-+  -- AXI compilers.+  , compileAXILite+  , icompileAXILite+  -- compilers that wraps a program in a dummy entity.   , compileWrap   , icompileWrap-  , runIOWrap-+     , VHDL.Mode(..)-   , module CMD   , module Language.Embedded.Hardware.Command.CMD   , module Language.Embedded.Hardware.Command.Frontend@@ -26,6 +31,7 @@ import Language.Embedded.Hardware.Command.Frontend import Language.Embedded.Hardware.Command.Backend.VHDL import Language.Embedded.Hardware.Interface+import Language.Embedded.Hardware.Interface.AXI  import Language.Embedded.VHDL (VHDL, prettyVHDL) @@ -34,6 +40,8 @@  import Control.Monad.Operational.Higher +import Control.Monad.Identity+ import qualified GHC.Exts as GHC (Constraint)  --------------------------------------------------------------------------------@@ -69,7 +77,29 @@ runIO = interpretBi (return . evalE)  --------------------------------------------------------------------------------+-- Some extra compilers that might be handy to have. +compileAXILite :: forall instr (exp :: * -> *) (pred :: * -> GHC.Constraint) a .+  ( Interp instr VHDL (Param2 exp pred)+  , HFunctor instr+  , AXIPred instr exp pred+  )+  => Comp instr exp pred Identity a+  -> String+compileAXILite = compile . void . component . axi_light ++icompileAXILite :: forall instr (exp :: * -> *) (pred :: * -> GHC.Constraint) a .+  ( Interp instr VHDL (Param2 exp pred)+  , HFunctor instr+  , AXIPred instr exp pred+  )+  => Comp instr exp pred Identity a+  -> IO ()+icompileAXILite = putStrLn . compileAXILite++--------------------------------------------------------------------------------+-- todo: Not sure we need these any more.+ compileWrap :: forall instr (exp :: * -> *) (pred :: * -> GHC.Constraint) a .      ( Interp instr VHDL (Param2 exp pred)      , HFunctor instr@@ -93,21 +123,6 @@   => (Signal Bool -> Signal Bool -> Program instr (Param2 exp pred) ())   -> IO () icompileWrap = icompile . wrap--runIOWrap :: forall instr (exp :: * -> *) (pred :: * -> GHC.Constraint) a-   . ( InterpBi instr IO (Param1 pred)-     , HBifunctor instr-     , EvaluateExp exp-     , ComponentCMD  :<: instr-     , StructuralCMD :<: instr-     , SignalCMD     :<: instr-     , pred Bool-     )-  => (Signal Bool -> Signal Bool -> Program instr (Param2 exp pred) ())-  -> IO ()-runIOWrap = runIO . wrap----------------------------------------------------------------------------------  -- | Wrap a hardware program in a architecture/entity pair. wrap :: forall instr (exp :: * -> *) (pred :: * -> GHC.Constraint) a .
src/Language/Embedded/Hardware/Command/Backend/VHDL.hs view
@@ -37,42 +37,33 @@ -- * Translation of hardware commands into VHDL. -------------------------------------------------------------------------------- ------------------------------------------------------------------------------------ ** ...--evalEM :: forall exp a . EvaluateExp exp => Maybe (exp a) -> a-evalEM e = maybe (error "empty value") id $ fmap evalE e--compEM :: forall exp a . CompileExp exp => Maybe (exp a) -> VHDL (Maybe V.Expression)-compEM e = maybe (return Nothing) (>>= return . Just) $ fmap compE e------------------------------------------------------------------------------------- ** ...- class CompileType ct   where     compileType :: ct a => proxy1 ct -> proxy2 a -> VHDL V.Type     compileLit  :: ct a => proxy1 ct ->        a -> VHDL V.Expression     compileBits :: ct a => proxy1 ct ->        a -> VHDL V.Expression -instance CompileType HType+instance CompileType PrimType   where     compileType _ = compT-    compileLit  _ = return . literal . printVal-    compileBits _ = return . literal . printBits+    compileLit  _ = return . literal . primTypeVal+    compileBits _ = return . literal . primTypeBits  -------------------------------------------------------------------------------- -compT :: HType a => proxy a -> VHDL V.Type-compT = declare+compT :: forall proxy a . PrimType a => proxy a -> VHDL V.Type+compT _ = declareType (Proxy :: Proxy a) -compTM :: forall proxy ct exp a . (CompileType ct, ct a) => proxy ct -> Maybe (exp a) -> VHDL V.Type+compTM :: forall proxy ct exp a . (CompileType ct, ct a)+  => proxy ct -> Maybe (exp a) -> VHDL V.Type compTM _ _ = compileType (Proxy::Proxy ct) (Proxy::Proxy a) -compTF :: forall proxy ct exp a b . (CompileType ct, ct a) => proxy ct -> (exp a -> b) -> VHDL V.Type+compTF :: forall proxy ct exp a b . (CompileType ct, ct a)+  => proxy ct -> (exp a -> b) -> VHDL V.Type compTF _ _ = compileType (Proxy::Proxy ct) (Proxy::Proxy a) -compTA :: forall proxy ct array i a . (CompileType ct, ct a) => proxy ct -> V.Range -> array a -> VHDL V.Type+compTA :: forall proxy ct array i a . (CompileType ct, ct a)+  => proxy ct -> V.Range -> array a -> VHDL V.Type compTA _ range _ =   do i <- newSym (Base "array")      t <- compileType (Proxy::Proxy ct) (Proxy::Proxy a)@@ -92,6 +83,16 @@  -------------------------------------------------------------------------------- +evalEM :: forall exp a . EvaluateExp exp+  => Maybe (exp a) -> a+evalEM e = maybe (error "empty value") id $ fmap evalE e++compEM :: forall exp a . CompileExp exp+  => Maybe (exp a) -> VHDL (Maybe V.Expression)+compEM e = maybe (return Nothing) (>>= return . Just) $ fmap compE e++--------------------------------------------------------------------------------+ proxyE :: exp a -> Proxy a proxyE _ = Proxy @@ -102,12 +103,7 @@ proxyF _ = Proxy  ----------------------------------------------------------------------------------- ** ... -newSym :: Name -> VHDL String-newSym (Base  n) = V.newSym n-newSym (Exact n) = return   n- freshVar :: forall proxy ct exp a . (CompileType ct, ct a)   => proxy ct -> Name -> VHDL (Val a) freshVar _ prefix =@@ -116,8 +112,26 @@      V.variable (ident' i) t Nothing      return (ValC i) +newSym :: Name -> VHDL String+newSym (Base  n) = V.newSym n+newSym (Exact n) = return   n++ident :: ToIdent a => a -> String+ident a = let (Ident s) = toIdent a in s++ident' :: ToIdent a => a -> V.Identifier+ident' a = V.Ident $ ident a++-- todo: this... why does this work?+instance ToIdent String where toIdent = Ident+instance ToIdent Ident  where toIdent = id+instance ToIdent Name   where+  toIdent (Base s)  = Ident s+  toIdent (Exact s) = Ident s+ -------------------------------------------------------------------------------- -- ** Signals.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp SignalCMD VHDL (Param2 exp ct)   where@@ -160,6 +174,7 @@  -------------------------------------------------------------------------------- -- ** Variables.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp VariableCMD VHDL (Param2 exp ct)   where@@ -200,6 +215,7 @@  -------------------------------------------------------------------------------- -- ** Constants.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp ConstantCMD VHDL (Param2 exp ct)   where@@ -225,6 +241,7 @@  -------------------------------------------------------------------------------- -- ** Arrays.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp ArrayCMD VHDL (Param2 exp ct)   where@@ -278,6 +295,7 @@  -------------------------------------------------------------------------------- -- ** Virtual Arrays.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp VArrayCMD VHDL (Param2 exp ct)   where@@ -361,6 +379,7 @@  -------------------------------------------------------------------------------- -- ** Loops.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp LoopCMD VHDL (Param2 exp ct)   where@@ -402,6 +421,7 @@  -------------------------------------------------------------------------------- -- ** Conditional.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp ConditionalCMD VHDL (Param2 exp ct)   where@@ -456,6 +476,7 @@  -------------------------------------------------------------------------------- -- ** Components.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp ComponentCMD VHDL (Param2 exp ct)   where@@ -524,6 +545,7 @@  -------------------------------------------------------------------------------- -- ** Structural.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp StructuralCMD VHDL (Param2 exp ct)   where@@ -552,6 +574,7 @@  -------------------------------------------------------------------------------- -- ** VHDL.+--------------------------------------------------------------------------------  instance (CompileExp exp, CompileType ct) => Interp VHDLCMD VHDL (Param2 exp ct)   where@@ -616,26 +639,7 @@ runVHDL = error "hardware-edsl.runVHDL: todo."  ----------------------------------------------------------------------------------- Helpers.------ todo : make a lift that first tries to go backwards. If that's not possible,---        perform a regular lift. This should get rid of most extra parenthesis. -ident :: ToIdent a => a -> String-ident a = let (Ident s) = toIdent a in s--ident' :: ToIdent a => a -> V.Identifier-ident' a = V.Ident $ ident a---- todo: this... why does this work?-instance ToIdent String where toIdent = Ident-instance ToIdent Ident  where toIdent = id-instance ToIdent Name   where-  toIdent (Base s)  = Ident s-  toIdent (Exact s) = Ident s----------------------------------------------------------------------------------- simple   :: String -> V.Name simple   s = V.simple s @@ -654,13 +658,9 @@ slice'   :: String -> V.Range -> V.Expression slice'   s = lift . V.name . slice s ---------------------------------------------------------------------------------- literal :: String -> V.Expression literal s = lift $ V.literal $ V.number s ---------------------------------------------------------------------------------- range  :: V.Expression -> V.Direction -> V.Expression -> V.Range range l dir r = V.range (unpackSimple l) dir (unpackSimple r) @@ -671,7 +671,6 @@ rangePoint a = V.range (V.point $ toInteger a) V.downto (V.point 0)  ----------------------------------------------------------------------------------- ...  unpackShift :: V.Expression -> V.ShiftExpression unpackShift (V.ENand (V.Relation s Nothing) Nothing) = s@@ -685,24 +684,4 @@ unpackTerm (V.ENand (V.Relation (V.ShiftExpression (V.SimpleExpression Nothing t []) Nothing) Nothing) Nothing) = t unpackTerm e = lift e ---------------------------------------------------------------------------------------------------------------------------------------------------------------------{--ident :: String -> V.Identifier-ident s = V.Ident s--ident' :: Name -> V.Identifier-ident' (Base  n) = ident n-ident' (Exact n) = ident n--name :: String -> V.Primary-name = V.PrimName . V.NSimple . ident--}----------------------------------------------------------------------------------{--fromIdent :: ToIdent a => a -> V.Identifier-fromIdent a = let (Ident i) = toIdent a in ident i--} --------------------------------------------------------------------------------
src/Language/Embedded/Hardware/Command/CMD.hs view
@@ -15,7 +15,7 @@  import Language.Embedded.VHDL (Mode) import Language.Embedded.Hardware.Interface-import Language.Embedded.Hardware.Expression.Represent (Inhabited, Sized)+import Language.Embedded.Hardware.Expression.Represent (PrimType, Inhabited, Sized) import Language.Embedded.Hardware.Expression.Represent.Bit (Bit, Bits)  import Control.Monad.Reader (ReaderT(..), runReaderT, lift)@@ -411,11 +411,11 @@ data Signature fs a   where     Ret  :: prog () -> Signature (Param3 prog exp pred) ()-    SSig :: (pred a, Inhabited a, Sized a)+    SSig :: (pred a, Integral a, PrimType a)       => Name -> Mode       -> (Signal a -> Signature (Param3 prog exp pred) b)       -> Signature (Param3 prog exp pred) (Signal a -> b)-    SArr :: (pred a, Inhabited a, Sized a, pred i, Integral i, Ix i)+    SArr :: (pred a, Integral a, PrimType a, pred i, Integral i, Ix i)       => Name -> Mode -> i       -> (Array i a -> Signature (Param3 prog exp pred) b)       -> Signature (Param3 prog exp pred) (Array i a -> b)@@ -443,11 +443,11 @@ data Argument pred a   where     Nil  :: Argument pred ()-    ASig :: (pred a, Inhabited a, Sized a)+    ASig :: (pred a, Integral a, PrimType a)       => Signal a       -> Argument pred b       -> Argument pred (Signal a -> b)-    AArr :: (pred a, Inhabited a, Sized a, Integral i, Ix i)+    AArr :: (pred a, Integral a, PrimType a, pred i, Integral i, Ix i)       => Array i a       -> Argument pred b       -> Argument pred (Array i a -> b)
src/Language/Embedded/Hardware/Command/Frontend.hs view
@@ -20,6 +20,7 @@ import Data.IORef (readIORef) import Data.Int import Data.Word+import Data.Typeable  import System.IO.Unsafe -- used for `veryUnsafeFreezeVariable`. @@ -401,43 +402,63 @@  -------------------------------------------------------------------------------- -exactInput  :: (pred a, Inhabited a, Sized a) => String -> (Signal a -> Sig instr exp pred m b) -> Sig instr exp pred m (Signal a -> b)+exactInput  :: (pred a, Integral a, PrimType a)+  => String+  -> (Signal a -> Sig instr exp pred m b)+  -> Sig instr exp pred m (Signal a -> b) exactInput  n = SSig (Exact n) In -namedInput :: (pred a, Inhabited a, Sized a) => String -> (Signal a -> Sig instr exp pred m b) -> Sig instr exp pred m (Signal a -> b)+namedInput :: (pred a, Integral a, PrimType a)+  => String+  -> (Signal a -> Sig instr exp pred m b)+  -> Sig instr exp pred m (Signal a -> b) namedInput n = SSig (Base n) In -input :: (pred a, Inhabited a, Sized a) => (Signal a -> Sig instr exp pred m b) -> Sig instr exp pred m (Signal a -> b)+input :: (pred a, Integral a, PrimType a)+  => (Signal a -> Sig instr exp pred m b)+  -> Sig instr exp pred m (Signal a -> b) input = namedInput "in" -exactInputArr :: (pred a, Inhabited a, Sized a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b)+{-+exactInputArr :: (pred a, Inhabited a, Sized a, Integral a, Rep a, Typeable a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b) exactInputArr n l = SArr (Exact n) In l -namedInputArr :: (pred a, Inhabited a, Sized a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b)+namedInputArr :: (pred a, Inhabited a, Sized a, Integral a, Rep a, Typeable a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b) namedInputArr n l = SArr (Base n) In l -inputArr :: (pred a, Inhabited a, Sized a, pred i, Integral i, Ix i) => i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b)+inputArr :: (pred a, Inhabited a, Sized a, Integral a, Rep a, Typeable a, pred i, Integral i, Ix i) => i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b) inputArr = namedInputArr "in"+-} -exactOutput :: (pred a, Inhabited a, Sized a) => String -> (Signal a -> Sig instr exp pred m b) -> Sig instr exp pred m (Signal a -> b)+exactOutput :: (pred a, Integral a, PrimType a)+  => String+  -> (Signal a -> Sig instr exp pred m b)+  -> Sig instr exp pred m (Signal a -> b) exactOutput n = SSig (Exact n) Out -namedOutput :: (pred a, Inhabited a, Sized a) => String -> (Signal a -> Sig instr exp pred m b) -> Sig instr exp pred m (Signal a -> b)+namedOutput :: (pred a, Integral a, PrimType a)+  => String+  -> (Signal a -> Sig instr exp pred m b)+  -> Sig instr exp pred m (Signal a -> b) namedOutput n = SSig (Base n) Out -output :: (pred a, Inhabited a, Sized a) => (Signal a -> Sig instr exp pred m b) -> Sig instr exp pred m (Signal a -> b)+output :: (pred a, Integral a, PrimType a)+  => (Signal a -> Sig instr exp pred m b)+  -> Sig instr exp pred m (Signal a -> b) output = namedOutput "out" -exactOutputArr :: (pred a, Inhabited a, Sized a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b)+{-+exactOutputArr :: (pred a, Inhabited a, Sized a, Integral a, Rep a, Typeable a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b) exactOutputArr n l = SArr (Exact n) Out l -namedOutputArr :: (pred a, Inhabited a, Sized a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b)+namedOutputArr :: (pred a, Inhabited a, Sized a, Integral a, Rep a, Typeable a, pred i, Integral i, Ix i) => String -> i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b) namedOutputArr n l = SArr (Base n) Out l -outputArr :: (pred a, Inhabited a, pred i, Sized a, Integral i, Ix i) => i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b)+outputArr :: (pred a, Inhabited a, Sized a, Integral a, Rep a, Typeable a, pred i, Integral i, Ix i) => i -> (Array i a -> Sig instr exp pred m b) -> Sig instr exp pred m (Array i a -> b) outputArr = namedOutputArr "out"+-} -ret :: (ProgramT instr (Param2 exp pred) m) () -> Signature (Param3 (ProgramT instr (Param2 exp pred) m) exp pred) ()+ret :: ProgramT instr (Param2 exp pred) m () -> Sig instr exp pred m () ret = Ret  --------------------------------------------------------------------------------
src/Language/Embedded/Hardware/Expression.hs view
@@ -2,11 +2,8 @@   ( HExp   , HType   , module Language.Embedded.Hardware.Expression.Frontend-  , module Language.Embedded.Hardware.Expression.Represent.Bit   ) where -import Language.Embedded.Hardware.Expression.Syntax (HExp)+import Language.Embedded.Hardware.Expression.Syntax (HExp, HType) import Language.Embedded.Hardware.Expression.Frontend-import Language.Embedded.Hardware.Expression.Represent (HType)-import Language.Embedded.Hardware.Expression.Represent.Bit import Language.Embedded.Hardware.Expression.Backend.VHDL ()
src/Language/Embedded/Hardware/Expression/Backend/VHDL.hs view
@@ -29,7 +29,7 @@  instance FreeExp HExp   where-    type PredicateExp HExp = HType+    type PredicateExp HExp = PrimType     litE = value     varE = var @@ -52,11 +52,13 @@   where     compE  = compHExp -compHType :: forall a . HType a => HExp a -> VHDL VHDL.Type-compHType _ = declare (undefined :: proxy a)+compHType :: forall a . PrimType a+  => HExp a -> VHDL VHDL.Type+compHType _ = declareType (Proxy :: Proxy a) -compHTypeFun :: forall a b . (HType a, HType b) => (a -> b) -> VHDL VHDL.Type-compHTypeFun _ = declare (undefined :: proxy a)+compHTypeFun :: forall a b . (PrimType a, PrimType b)+  => (a -> b) -> VHDL VHDL.Type+compHTypeFun _ = declareType (Proxy :: Proxy a)  compHExp :: forall a . HExp a -> VHDL VHDL.Expression compHExp e = Hoist.lift <$> compSimple e@@ -69,7 +71,7 @@      compDomain       :: forall sig-       . HType (DenResult sig)+       . PrimType (DenResult sig)       => Dom sig       -> Args (AST T) sig       -> VHDL Kind@@ -172,12 +174,16 @@           x' <- Hoist.lift <$> compLoop x           return $ Hoist.E $ VHDL.uCast x' tf tt     compDomain primary args-      | Just (Name n)       <- prj primary = return $ Hoist.P $ VHDL.name n-      | Just (Literal i)    <- prj primary = return $ Hoist.P $ VHDL.literal $ VHDL.number $ printVal i-      | Just (Aggregate a)  <- prj primary = return $ Hoist.P $ VHDL.aggregate a+      | Just (Name n)       <- prj primary =+          return $ Hoist.P $ VHDL.name n+      | Just (Literal i)    <- prj primary =+          return $ Hoist.P $ VHDL.literal $ VHDL.number $ primTypeVal i+      | Just (Aggregate a)  <- prj primary =+          return $ Hoist.P $ VHDL.aggregate a       | Just (Function f _) <- prj primary = do           as <- sequence $ listArgs compLoop args           return $ Hoist.P $ VHDL.function (VHDL.simple f) (fmap Hoist.lift as)-      | Just (Allocator)    <- prj primary = error "expression-backend: todo"+      | Just (Allocator)    <- prj primary =+          error "expression-backend-todo: allocators."  --------------------------------------------------------------------------------
src/Language/Embedded/Hardware/Expression/Frontend.hs view
@@ -7,11 +7,9 @@  import qualified Language.VHDL as V -import Language.Embedded.Hardware.Interface-import Language.Embedded.Hardware.Expression.Syntax hiding (Term, Factor, Primary)-import Language.Embedded.Hardware.Expression.Hoist-import Language.Embedded.Hardware.Expression.Represent-import Language.Embedded.Hardware.Expression.Represent.Bit+import Language.Embedded.Hardware.Expression.Syntax (HExp, HType, sugarT)+import Language.Embedded.Hardware.Expression.Represent.Bit (Bits, bitFromInteger, bitToInteger)+import qualified Language.Embedded.Hardware.Expression.Syntax as H import qualified Language.Embedded.VHDL.Monad.Expression as V  import Data.Typeable (Typeable)@@ -51,31 +49,31 @@ instance Expr HExp where   true  = value True   false = value False-  and   = sugarT And-  or    = sugarT Or-  xor   = sugarT Xor-  xnor  = sugarT Xnor-  nand  = sugarT Nand-  nor   = sugarT Nor+  and   = sugarT H.And+  or    = sugarT H.Or+  xor   = sugarT H.Xor+  xnor  = sugarT H.Xnor+  nand  = sugarT H.Nand+  nor   = sugarT H.Nor  --------------------------------------------------------------------------------  -- | Relational operators. class Rel exp where-  eq  :: (HType a, Eq a) => exp a -> exp a -> exp Bool-  neq :: (HType a, Eq a) => exp a -> exp a -> exp Bool+  eq  :: (HType a, Eq a)  => exp a -> exp a -> exp Bool+  neq :: (HType a, Eq a)  => exp a -> exp a -> exp Bool   lt  :: (HType a, Ord a) => exp a -> exp a -> exp Bool   lte :: (HType a, Ord a) => exp a -> exp a -> exp Bool   gt  :: (HType a, Ord a) => exp a -> exp a -> exp Bool   gte :: (HType a, Ord a) => exp a -> exp a -> exp Bool  instance Rel HExp where-  eq  = sugarT Eq-  neq = sugarT Neq-  lt  = sugarT Lt-  lte = sugarT Lte-  gt  = sugarT Gt-  gte = sugarT Gte+  eq  = sugarT H.Eq+  neq = sugarT H.Neq+  lt  = sugarT H.Lt+  lte = sugarT H.Lte+  gt  = sugarT H.Gt+  gte = sugarT H.Gte  -------------------------------------------------------------------------------- @@ -89,12 +87,12 @@   ror :: (HType a, B.Bits a) => exp a -> exp Integer -> exp a  instance Shift HExp where-  sll = sugarT Sll-  srl = sugarT Srl-  sla = sugarT Sla-  sra = sugarT Sra-  rol = sugarT Rol-  ror = sugarT Ror+  sll = sugarT H.Sll+  srl = sugarT H.Srl+  sla = sugarT H.Sla+  sra = sugarT H.Sra+  rol = sugarT H.Rol+  ror = sugarT H.Ror  -------------------------------------------------------------------------------- @@ -103,14 +101,14 @@   neg :: (HType a, Num a) => exp a -> exp a   add :: (HType a, Num a) => exp a -> exp a -> exp a   sub :: (HType a, Num a) => exp a -> exp a -> exp a-  cat :: ( KnownNat n, KnownNat m, KnownNat (n + m), Typeable (n + m))+  cat :: (KnownNat n, KnownNat m, KnownNat (n + m), Typeable (n + m))       => exp (Bits n) -> exp (Bits m) -> exp (Bits (n + m))  instance Simple HExp where-  neg = sugarT Neg-  add = sugarT Add-  sub = sugarT Sub-  cat = sugarT Cat+  neg = sugarT H.Neg+  add = sugarT H.Add+  sub = sugarT H.Sub+  cat = sugarT H.Cat  -------------------------------------------------------------------------------- @@ -122,10 +120,10 @@   rem :: (HType a, Integral a) => exp a -> exp a -> exp a  instance Term HExp where-  mul = sugarT Mul-  div = sugarT Div-  mod = sugarT Mod-  rem = sugarT Rem+  mul = sugarT H.Mul+  div = sugarT H.Div+  mod = sugarT H.Mod+  rem = sugarT H.Rem  -------------------------------------------------------------------------------- @@ -136,9 +134,9 @@   not :: exp Bool -> exp Bool  instance Factor HExp where-  exp = sugarT Exp-  abs = sugarT Abs-  not = sugarT Not+  exp = sugarT H.Exp+  abs = sugarT H.Abs+  not = sugarT H.Not  -------------------------------------------------------------------------------- @@ -149,33 +147,37 @@   cast  :: (HType a, HType b) => (a -> b) -> exp a -> exp b    instance Primary HExp where-  value  = sugarT . Literal-  name n = sugarT (Name (V.NSimple (V.Ident n)))-  cast f = sugarT (Conversion f)+  value  = sugarT . H.Literal+  name n = sugarT (H.Name (V.NSimple (V.Ident n)))+  cast f = sugarT (H.Conversion f)  -- | Creates a variable from a string. var :: (Primary exp, HType a) => String -> exp a var = name  -- | Converts an integral (signed/unsigned/integer) to an integer.-toInteger :: (Primary exp, HType a, Integral a) => exp a -> exp Integer+toInteger :: (Primary exp, HType a, Integral a)+  => exp a -> exp Integer toInteger = cast (fromIntegral)  -- | Converts an integral to a signed value.-toSigned :: (Primary exp, HType a, HType b, Integral a, Num b) => exp a -> exp b+toSigned :: (Primary exp, HType a, HType b, Integral a, Num b)+  => exp a -> exp b toSigned = cast (fromIntegral)  -- | Converts an integral to a unsigned value.-toUnsigned :: (Primary exp, HType a, HType b, Integral a, Num b) => exp a -> exp b+toUnsigned :: (Primary exp, HType a, HType b, Integral a, Num b)+  => exp a -> exp b toUnsigned = cast (fromIntegral)  -- | Converts an integral to its bit representation.-toBits :: (Primary exp, HType a, HType (Bits b), Integral a, KnownNat b) => exp a -> exp (Bits b)+toBits :: (Primary exp, HType a, Integral a, KnownNat b)+  => exp a -> exp (Bits b) toBits = cast (bitFromInteger . fromIntegral) -----------------------------------------------------------------------------------fromBits :: (Primary exp, HType (Bits a), HType b, Num b, KnownNat a) => exp (Bits a) -> exp b+-- | Converts a bit representation of integral into its original form.+fromBits :: (Primary exp, HType b, Num b, KnownNat a)+  => exp (Bits a) -> exp b fromBits = cast (fromIntegral . bitToInteger)  --------------------------------------------------------------------------------
src/Language/Embedded/Hardware/Expression/Represent.hs view
@@ -1,143 +1,29 @@+{-# LANGUAGE GADTs                #-} {-# LANGUAGE FlexibleInstances    #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ScopedTypeVariables  #-}--module Language.Embedded.Hardware.Expression.Represent-  ( Rep(..)-  , Inhabited(..)-  , Sized(..)-  , HType(..)-  -  , declareBoolean-  , declareNumeric-  , declareFloating-    -  , module Data.Int-  , module Data.Word-  ) where+{-# LANGUAGE StandaloneDeriving   #-} -import qualified Language.VHDL as V+module Language.Embedded.Hardware.Expression.Represent where -import Language.VHDL (Expression)+import Language.Embedded.Hardware.Expression.Represent.Bit  import Language.Embedded.VHDL (VHDL) import Language.Embedded.VHDL.Monad (newSym, newLibrary, newImport) import Language.Embedded.VHDL.Monad.Type-import qualified Language.Embedded.VHDL.Monad.Util as Util (printBits)--import Language.Embedded.Hardware.Expression.Hoist (lift)+import Language.Embedded.VHDL.Monad.Util (printBits)  import Data.Char (isDigit) import Data.Int import Data.Word-import Data.Typeable-import Text.Printf------------------------------------------------------------------------------------- * Representation of types.---------------------------------------------------------------------------------+import Data.Proxy (Proxy(..))+import Data.Typeable (Typeable) --- | Collection of required classes for hardware expressions.-class    (Typeable a, Rep a, Eq a) => HType a-instance (Typeable a, Rep a, Eq a) => HType a+import GHC.TypeLits  ----------------------------------------------------------------------------------- ** Representable types.---- | 'Rep'resentable types.-class Rep a-  where-    declare   :: proxy a -> VHDL Type-    printVal  :: a -> String-    printBits :: a -> String--instance Rep Bool where-  declare  _     = declareBoolean >> return std_logic-  printVal True  = "\'1\'"-  printVal False = "\'0\'"-  printBits      = printVal--instance Rep Int8 where-  declare _ = declareNumeric >> return signed8-  printVal  = show-  printBits = Util.printBits 8--instance Rep Int16 where-  declare _ = declareNumeric >> return signed16-  printVal  = show-  printBits = Util.printBits 16--instance Rep Int32 where-  declare _ = declareNumeric >> return signed32-  printVal  = show-  printBits = Util.printBits 32--instance Rep Int64 where-  declare _ = declareNumeric >> return signed64-  printVal  = show-  printBits = Util.printBits 64--instance Rep Word8 where-  declare _ = declareNumeric >> return usigned8-  printVal  = show-  printBits = Util.printBits 8--instance Rep Word16 where-  declare _ = declareNumeric >> return usigned16-  printVal  = show-  printBits = Util.printBits 16--instance Rep Word32 where-  declare _ = declareNumeric >> return usigned32-  printVal  = show-  printBits = Util.printBits 32--instance Rep Word64 where-  declare _ = declareNumeric >> return usigned64-  printVal  = show-  printBits = Util.printBits 64--instance Rep Int where-  declare _ = return (integer Nothing)-  printVal  = show-  printBits = error "hardware-edsl.printBits: int."--instance Rep Integer where-  declare _ = return (integer Nothing)-  printVal  = show-  printBits = error "hardware-edsl.printBits: integer."--instance Rep Float where-  declare _ = declareFloating >> return float-  printVal  = show-  printBits = error "hardware-edsl.printBits: float."--instance Rep Double where-  declare _ = declareFloating >> return double-  printVal  = show-  printBits = error "hardware-edsl.printBits: double."---- | Declare the necessary libraries to support boolean operations.-declareBoolean :: VHDL ()-declareBoolean =-  do newLibrary "IEEE"-     newImport  "IEEE.std_logic_1164"---- | Declare the necessary libraries to support numerical operations.-declareNumeric :: VHDL ()-declareNumeric =-  do newLibrary "IEEE"-     newImport  "IEEE.std_logic_1164"-     newImport  "IEEE.numeric_std"---- | Declare the necessary libraries to support floating point operations.-declareFloating :: VHDL ()-declareFloating =-  do newLibrary "IEEE"-     newImport  "IEEE.float_pkg"-+-- * Inhabited types. ----------------------------------------------------------------------------------- ** Inhabited types.  -- | Inhabited types, that is, types with a base element. class Inhabited a@@ -159,8 +45,13 @@ instance Inhabited Float   where reset = 0 instance Inhabited Double  where reset = 0 +instance forall n . KnownNat n => Inhabited (Bits n)+  where+    reset = bitFromInteger 0+ ----------------------------------------------------------------------------------- ** Sized types.+-- * Sized types.+--------------------------------------------------------------------------------  -- | Types with a known size. class Sized a@@ -177,18 +68,158 @@ instance Sized Word16  where bits _ = 16 instance Sized Word32  where bits _ = 32 instance Sized Word64  where bits _ = 64+instance Sized Int     where bits _ = 32+instance Sized Integer where bits _ = 64+instance Sized Float   where bits _ = 32+instance Sized Double  where bits _ = 64 +instance forall n . KnownNat n => Sized (Bits n)+  where+    bits _ = ni (Proxy :: Proxy n)+ ----------------------------------------------------------------------------------- ** Hmm...+-- * Representable types.+-------------------------------------------------------------------------------- -instance Num Bool where-  (+)    = error "(+) not implemented for Bool"-  (-)    = error "(-) not implemented for Bool"-  (*)    = error "(*) not implemented for Bool"-  abs    = id-  signum = id-  fromInteger 0 = False-  fromInteger 1 = True-  fromInteger _ = error "bool-num: >1"  +-- | Representation of primitive hardware types.+data TypeRep a+  where+    -- booleans.+    BoolT    :: TypeRep Bool+    -- signed numbers.+    Int8T    :: TypeRep Int8+    Int16T   :: TypeRep Int16+    Int32T   :: TypeRep Int32+    Int64T   :: TypeRep Int64+    -- unsigned numbers.+    Word8T   :: TypeRep Word8+    Word16T  :: TypeRep Word16+    Word32T  :: TypeRep Word32+    Word64T  :: TypeRep Word64+    -- integers.+    IntT     :: TypeRep Int+    IntegerT :: TypeRep Integer+    -- floating point numbers.+    FloatT   :: TypeRep Float+    DoubleT  :: TypeRep Double+    -- variable sized bit values (todo).+    BitsT    :: KnownNat n => TypeRep (Bits n)++deriving instance Eq       (TypeRep a)+deriving instance Show     (TypeRep a)+deriving instance Typeable (TypeRep a)++--------------------------------------------------------------------------------++-- | Primitive hardware types.+class (Eq a, Show a, Typeable a, Inhabited a, Sized a) => PrimType a+  where+    typeRep :: TypeRep a++instance PrimType Bool    where typeRep = BoolT+instance PrimType Int8    where typeRep = Int8T+instance PrimType Int16   where typeRep = Int16T+instance PrimType Int32   where typeRep = Int32T+instance PrimType Int64   where typeRep = Int64T+instance PrimType Word8   where typeRep = Word8T+instance PrimType Word16  where typeRep = Word16T+instance PrimType Word32  where typeRep = Word32T+instance PrimType Word64  where typeRep = Word64T+instance PrimType Int     where typeRep = IntT+instance PrimType Integer where typeRep = IntegerT+instance PrimType Float   where typeRep = FloatT+instance PrimType Double  where typeRep = DoubleT++instance forall n . KnownNat n => PrimType (Bits n)+  where+    typeRep = BitsT++--------------------------------------------------------------------------------++-- | Print a value.+primTypeVal :: forall a . PrimType a => a -> String+primTypeVal a = case typeRep :: TypeRep a of+  BoolT    -> if a then "\'1\'" else "\'0\'"+  _        -> show a++-- | Print a value as its bit representation.+primTypeBits :: forall a . PrimType a => a -> String+primTypeBits a = case typeRep :: TypeRep a of+  BoolT    -> primTypeVal a+  Int8T    -> printBits 8  a+  Int16T   -> printBits 16 a+  Int32T   -> printBits 32 a+  Int64T   -> printBits 64 a+  Word8T   -> printBits 8  a+  Word16T  -> printBits 16 a+  Word32T  -> printBits 32 a+  Word64T  -> printBits 64 a+  IntT     -> error "todo: print ints as bits."+  IntegerT -> error "todo: print integers as bits."+  FloatT   -> error "todo: print floats as bits."+  DoubleT  -> error "todo: print doubles as bits."++-- | Hardware type representation of a primitive type.+primTypeRep :: forall a . PrimType a => Proxy a -> Type+primTypeRep _ = case typeRep :: TypeRep a of+  BoolT    -> std_logic+  Int8T    -> signed8+  Int16T   -> signed16+  Int32T   -> signed32+  Int64T   -> signed64+  Word8T   -> usigned8+  Word16T  -> usigned16+  Word32T  -> usigned32+  Word64T  -> usigned64+  IntT     -> integer Nothing -- todo: might be wrong.+  IntegerT -> integer Nothing -- todo: migth be wrong.+  FloatT   -> float+  DoubleT  -> double+  BitsT    -> primTypeRepBits (Proxy :: Proxy a)++primTypeRepBits :: forall n . KnownNat n => Proxy (Bits n) -> Type+primTypeRepBits _ = std_logic_vector size+  where size = fromInteger (ni (undefined :: Bits n))++-- | Declare the necessary imports/packages to support a primitive type.+primTypeDeclare :: forall a . PrimType a => Proxy a -> VHDL ()+primTypeDeclare p = case typeRep :: TypeRep a of+  BoolT    -> declareBoolean+  Int8T    -> declareNumeric+  Int16T   -> declareNumeric+  Int32T   -> declareNumeric+  Int64T   -> declareNumeric+  Word8T   -> declareNumeric+  Word16T  -> declareNumeric+  Word32T  -> declareNumeric+  Word64T  -> declareNumeric+  IntT     -> declareNumeric+  IntegerT -> declareNumeric+  FloatT   -> declareFloating+  DoubleT  -> declareFloating+  BitsT    -> declareBoolean++-- | Declare a primitive hardware type and get back its representation.+declareType :: PrimType a => Proxy a -> VHDL Type+declareType proxy = primTypeDeclare proxy >> return (primTypeRep proxy)++-- | Declare the necessary libraries to support boolean operations.+declareBoolean :: VHDL ()+declareBoolean =+  do newLibrary "IEEE"+     newImport  "IEEE.std_logic_1164"++-- | Declare the necessary libraries to support numerical operations.+declareNumeric :: VHDL ()+declareNumeric =+  do newLibrary "IEEE"+     newImport  "IEEE.std_logic_1164"+     newImport  "IEEE.numeric_std"++-- | Declare the necessary libraries to support floating point operations.+declareFloating :: VHDL ()+declareFloating =+  do newLibrary "IEEE"+     newImport  "IEEE.float_pkg"  --------------------------------------------------------------------------------
src/Language/Embedded/Hardware/Expression/Represent/Bit.hs view
@@ -38,25 +38,15 @@   , bitToList   , bitShowBin   , bitShowHex--  , UBits-  , forgetBits-  , recallBits   )   where -import Language.Embedded.Hardware.Expression.Represent--import Language.Embedded.VHDL            (VHDL)-import Language.Embedded.VHDL.Monad      (newSym, newLibrary, newImport)-import Language.Embedded.VHDL.Monad.Type- import Data.Ix import Data.Typeable import Data.Bits hiding (Bits) import qualified Data.Bits as Bit (Bits) -import Control.Monad   (guard)+import Control.Monad (guard) import Control.DeepSeq (NFData(..))  import Data.Char (intToDigit)@@ -65,54 +55,14 @@ import GHC.TypeLits  ----------------------------------------------------------------------------------- * ...+-- * Bit vectors of known lenght. -------------------------------------------------------------------------------- ------------------------------------------------------------------------------------ ** Single bit.--type Bit = Bool------------------------------------------------------------------------------------- These aren't great to have..--instance Real Bool-  where-    toRational = error "toRational not implemented for bit."--instance Integral Bool-  where-    toInteger True  = 1-    toInteger False = 0-    quotRem         = error "quotRem not implemented for bit."------------------------------------------------------------------------------------- ** Bit vectors of known lenght.- newtype Bits (n :: Nat) = B Integer -instance forall n. KnownNat n => Inhabited (Bits n)-  where-    reset = bitFromInteger 0--instance forall n. KnownNat n => Rep (Bits n)-  where-    declare     = declareBits-    printVal    = show . bitToInteger-    printBits b = '\"' : (tail $ bitShowBin b) ++ ['\"'] -- *** why tail?--instance forall n. KnownNat n => Sized (Bits n)-  where-    bits _ = ni (Proxy::Proxy n)- deriving instance Typeable (Bits n)--declareBits :: forall proxy n. KnownNat n => proxy (Bits n) -> VHDL Type-declareBits _ = declareBoolean >> return (std_logic_vector size)-  where size = fromInteger (ni (undefined :: Bits n))          ----------------------------------------------------------------------------------- *** ...  ni :: KnownNat n => proxy n -> Integer ni = fromIntegral . natVal@@ -127,7 +77,6 @@ bitToInteger (B i) = i  ----------------------------------------------------------------------------------- *** ...  lift1 :: KnownNat n => (Integer -> Integer) -> Bits n -> Bits n lift1 f (B i) = norm (B (f i))@@ -136,7 +85,6 @@ lift2 f (B i) (B j) = norm (B (f i j))  ----------------------------------------------------------------------------------- *** ...  bitAdd :: KnownNat n => Bits n -> Bits n -> Bits n bitAdd = lift2 (+)@@ -207,7 +155,9 @@ bitRotate :: KnownNat n => Bits n -> Int -> Bits n bitRotate b@(B i) n   | si < 2    = b-  | otherwise = bitOr (bitFromInteger (shiftL i n)) (bitFromInteger (shiftR i (si - n)))+  | otherwise =+      bitOr (bitFromInteger (shiftL i n))+            (bitFromInteger (shiftR i (si - n)))   where n' = mod n si         si = fromInteger (ni b) @@ -303,36 +253,32 @@   inRange = undefined  ----------------------------------------------------------------------------------- ** Bit vectors of unknown lenght.--newtype UBits = UB Integer-  deriving (Eq, Enum, Ord, Num, Real, Integral)--instance Rep UBits-  where-    declare  = declareUBits-    printVal = show-    -- *** This is bad and produces a warning in vhdl as there's no guarantee-    --     that the lenght of the printed binary will be the expected one.-    --     Give UB an extra 'Maybe Integer' for storing the length whenever its-    --     available.-    printBits (UB i) = '\"' : (N.showIntAtBase 2 intToDigit i "") ++ ['\"']-    +-- * Bit.+-------------------------------------------------------------------------------- -declareUBits :: proxy UBits -> VHDL Type-declareUBits _ = declareBoolean >> return std_logic+type Bit = Bool  ----------------------------------------------------------------------------------forgetBits :: Bits n -> UBits-forgetBits b = UB (bitToInteger b)+-- These aren't too great to have.. -recallBits :: KnownNat n => UBits -> Bits n-recallBits (UB i) = (B i)+instance Num Bool where+  (+)    = error "(+) not implemented for Bool"+  (-)    = error "(-) not implemented for Bool"+  (*)    = error "(*) not implemented for Bool"+  abs    = id+  signum = id+  fromInteger 0 = False+  fromInteger 1 = True+  fromInteger _ = error "bool-num: >1"   ---------------------------------------------------------------------------------+instance Real Bool+  where+    toRational = error "toRational not implemented for bit." -instance Show UBits where-  showsPrec p (UB x) = showsPrec p x+instance Integral Bool+  where+    toInteger True  = 1+    toInteger False = 0+    quotRem         = error "quotRem not implemented for bit."  --------------------------------------------------------------------------------
src/Language/Embedded/Hardware/Expression/Syntax.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances  #-} {-# LANGUAGE DataKinds             #-}+{-# LANGUAGE ConstraintKinds       #-}  module Language.Embedded.Hardware.Expression.Syntax where @@ -14,7 +15,9 @@  import qualified Language.VHDL as V (Name, Aggregate) -import Language.Embedded.Hardware.Command (CompArrayIx)+--import Language.Embedded.Hardware.Command (CompArrayIx)+--instance CompArrayIx HExp+ import Language.Embedded.Hardware.Interface import Language.Embedded.Hardware.Expression.Represent import Language.Embedded.Hardware.Expression.Represent.Bit@@ -41,7 +44,7 @@ -- | Typed expressions. data T sig   where-    T :: HType (DenResult sig) => { unT :: Dom sig } -> T sig+    T :: PrimType (DenResult sig) => { unT :: Dom sig } -> T sig  -- | Specialized sugarSym for T. sugarT@@ -49,11 +52,14 @@      , T :<: SmartSym fi      , SyntacticN f fi      , SmartFun (SmartSym fi) (SmartSig fi) ~ fi-     , HType (DenResult (SmartSig fi)))+     , PrimType (DenResult (SmartSig fi)))   => sub (SmartSig fi)   -> f sugarT sym = sugarSym (T $ inj sym) +-- | Hardware primitive types.+type HType = PrimType+ -- | Hardware expressions. newtype HExp a = HExp { unHExp :: ASTF T a } @@ -81,66 +87,65 @@ -- | Relational expressions. data Relational sig   where-    Eq   :: (HType a)        => Relational (a :-> a :-> Full Bool)-    Neq  :: (HType a)        => Relational (a :-> a :-> Full Bool)-    Lt   :: (HType a, Ord a) => Relational (a :-> a :-> Full Bool)-    Lte  :: (HType a, Ord a) => Relational (a :-> a :-> Full Bool)-    Gt   :: (HType a, Ord a) => Relational (a :-> a :-> Full Bool)-    Gte  :: (HType a, Ord a) => Relational (a :-> a :-> Full Bool)+    Eq   :: (PrimType a)        => Relational (a :-> a :-> Full Bool)+    Neq  :: (PrimType a)        => Relational (a :-> a :-> Full Bool)+    Lt   :: (PrimType a, Ord a) => Relational (a :-> a :-> Full Bool)+    Lte  :: (PrimType a, Ord a) => Relational (a :-> a :-> Full Bool)+    Gt   :: (PrimType a, Ord a) => Relational (a :-> a :-> Full Bool)+    Gte  :: (PrimType a, Ord a) => Relational (a :-> a :-> Full Bool)  -- | Bit vector expressions. data ShiftExpression sig   where-    Sll :: (HType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)-    Srl :: (HType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)-    Sla :: (HType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)-    Sra :: (HType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)-    Rol :: (HType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)-    Ror :: (HType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)+    Sll :: (PrimType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)+    Srl :: (PrimType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)+    Sla :: (PrimType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)+    Sra :: (PrimType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)+    Rol :: (PrimType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)+    Ror :: (PrimType a, B.Bits a) => ShiftExpression (a :-> Integer :-> Full a)  -- | Numerical expressions. data SimpleExpression sig   where-    Neg :: (HType a, Num a) => SimpleExpression (a :->       Full a)-    Pos :: (HType a, Num a) => SimpleExpression (a :->       Full a)-    Add :: (HType a, Num a) => SimpleExpression (a :-> a :-> Full a)-    Sub :: (HType a, Num a) => SimpleExpression (a :-> a :-> Full a)+    Neg :: (PrimType a, Num a) => SimpleExpression (a :->       Full a)+    Pos :: (PrimType a, Num a) => SimpleExpression (a :->       Full a)+    Add :: (PrimType a, Num a) => SimpleExpression (a :-> a :-> Full a)+    Sub :: (PrimType a, Num a) => SimpleExpression (a :-> a :-> Full a)     Cat :: (KnownNat n, KnownNat m)         => SimpleExpression (Bits n :-> Bits m :-> Full (Bits (n + m)))  -- | Integral expressions. data Term sig   where-    Mul :: (HType a, Num a)      => Term (a :-> a :-> Full a)-    Div :: (HType a, Integral a) => Term (a :-> a :-> Full a)-    Mod :: (HType a, Integral a) => Term (a :-> a :-> Full a)-    Rem :: (HType a, Integral a) => Term (a :-> a :-> Full a)+    Mul :: (PrimType a, Num a)      => Term (a :-> a :-> Full a)+    Div :: (PrimType a, Integral a) => Term (a :-> a :-> Full a)+    Mod :: (PrimType a, Integral a) => Term (a :-> a :-> Full a)+    Rem :: (PrimType a, Integral a) => Term (a :-> a :-> Full a)  -- | ... data Factor sig   where-    Exp :: (HType a, Num a, HType b, Integral b) => Factor (a :-> b :-> Full a)-    Abs :: (HType a, Num a) => Factor (a :-> Full a)+    Exp :: (PrimType a, Num a, PrimType b, Integral b)+        => Factor (a :-> b :-> Full a)+    Abs :: (PrimType a, Num a) => Factor (a :-> Full a)     Not :: Factor (Bool :-> Full Bool)  -- | ... data Primary sig   where-    Name       :: (HType a) => V.Name      -> Primary (Full a)-    Literal    :: (HType a) => a           -> Primary (Full a)-    Aggregate  :: (HType a) => V.Aggregate -> Primary (Full a)+    Name       :: (PrimType a) => V.Name -> Primary (Full a)+    Literal    :: (PrimType a) => a -> Primary (Full a)+    Aggregate  :: (PrimType a) => V.Aggregate -> Primary (Full a)     Function   :: (Signature sig) => String -> Denotation sig -> Primary sig-    Qualified  :: (HType a, HType b) => b        -> Primary (a :-> Full a)-    Conversion :: (HType a, HType b) => (a -> b) -> Primary (a :-> Full b)-    Allocator  :: (HType a) => Primary (Full a)+    Qualified  :: (PrimType a, PrimType b) => b -> Primary (a :-> Full a)+    Conversion :: (PrimType a, PrimType b) => (a -> b) -> Primary (a :-> Full b)+    Allocator  :: (PrimType a) => Primary (Full a)     -- *** todo: expanded aggregate     Others     :: Primary (Bit :-> Full (Bits n))      -------------------------------------------------------------------------------- -- ** Syntactic instances. -instance CompArrayIx HExp- instance Equality T   where     equal (T s) (T t) = equal s t@@ -378,3 +383,51 @@ instance EvalEnv Primary env  --------------------------------------------------------------------------------+-- *** Temporary fix until GHC fixes their class resolution for DTC ***+--------------------------------------------------------------------------------++instance {-# OVERLAPPING #-} Project sub Dom => Project sub (AST T)+  where+    prj (Sym s) = prj s++instance {-# OVERLAPPING #-} Project sub Dom => Project sub T+  where+    prj (T a) = prj a++instance {-# OVERLAPPING #-} Project Expression Dom+  where+    prj (InjL a) = Just a+    prj _ = Nothing++instance {-# OVERLAPPING #-} Project Relational Dom+  where+    prj (InjR (InjL a)) = Just a+    prj _ = Nothing++instance {-# OVERLAPPING #-} Project ShiftExpression Dom+  where+    prj (InjR (InjR (InjL a))) = Just a+    prj _ = Nothing++instance {-# OVERLAPPING #-} Project SimpleExpression Dom+  where+    prj (InjR (InjR (InjR (InjL a)))) = Just a+    prj _ = Nothing++instance {-# OVERLAPPING #-} Project Term Dom+  where+    prj (InjR (InjR (InjR (InjR (InjL a))))) = Just a+    prj _ = Nothing++instance {-# OVERLAPPING #-} Project Factor Dom+  where+    prj (InjR (InjR (InjR (InjR (InjR (InjL a)))))) = Just a+    prj _ = Nothing++instance {-# OVERLAPPING #-} Project Primary Dom+  where+    prj ((InjR (InjR (InjR (InjR (InjR (InjR a))))))) = Just a+    prj _ = Nothing++--------------------------------------------------------------------------------+
+ src/Language/Embedded/Hardware/Interface/AXI.hs view
@@ -0,0 +1,644 @@+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}++module Language.Embedded.Hardware.Interface.AXI (axi_light, AXIPred) where++import Language.Embedded.VHDL (Mode(..))+import Language.Embedded.Hardware.Command.CMD+import Language.Embedded.Hardware.Command.Frontend+import Language.Embedded.Hardware.Interface+import Language.Embedded.Hardware.Expression.Frontend+import Language.Embedded.Hardware.Expression.Represent+import Language.Embedded.Hardware.Expression.Represent.Bit (Bits, Bit, bitFromInteger, ni)++import Control.Monad.Identity (Identity)+import Control.Monad.Operational.Higher hiding (when)+import Data.Constraint (Constraint)+import Data.Typeable+import Data.Int+import Data.Word+import Data.Bits ()+import Data.Ix (Ix)++import GHC.TypeLits+import qualified GHC.Exts as GHC (Constraint)++import Prelude hiding (not, and, or, div, null)+import qualified Prelude as P++--------------------------------------------------------------------------------+-- * AXI-light Controller.+--------------------------------------------------------------------------------+-- todo : we make a slight simplification and assume that components which we+--        connect to AXI-lite has a signature of+--          "input -> input -> .. -> input -> output -> ()"+--        this can easily be fixed by inspecting the modes given by the+--        signature.+--------------------------------------------------------------------------------++-- | Short-hand for programs.+type Prog instr exp pred = Program instr (Param2 exp pred)++-- | Short-hand for constraints.+type AXIPred instr exp pred = (+       SignalCMD      :<: instr+     , ArrayCMD       :<: instr+     , VariableCMD    :<: instr+     , ConditionalCMD :<: instr+     , StructuralCMD  :<: instr+     , LoopCMD        :<: instr+     , ComponentCMD   :<: instr+     , VHDLCMD        :<: instr+--+     , Expr    exp+     , Rel     exp+     , Factor  exp+     , Primary exp+--+     , FreeExp exp+       -- todo: this equality might be bad. It should be enough to+       --       say that 'PredicateExp' holds, and not that it has+       --       to be equal to 'pred'.+     , pred ~ PredicateExp exp+     , pred (Bit)+     , pred (Bits 2)+     , pred (Bits 3)+     , pred (Bits 4)+     , pred (Bits 32)+     , pred (Integer)+     , Num (exp Integer)+     )++--------------------------------------------------------------------------------+-- ** Signature.+--------------------------------------------------------------------------------++axi_light+  :: forall instr exp pred sig . AXIPred instr exp pred+  => Comp instr exp pred Identity sig+  -> Sig  instr exp pred Identity (+          Signal Bit       -- ^ Global clock signal.+       -> Signal Bit       -- ^ Global reset signal.+       -> Signal (Bits 32) -- ^ Write address.+       -> Signal (Bits 3)  -- ^ Write channel protection type.+       -> Signal Bit       -- ^ Write address valid.+       -> Signal Bit       -- ^ Write address ready.+       -> Signal (Bits 32) -- ^ Write data.+       -> Signal (Bits 4)  -- ^ Write strobes.+       -> Signal Bit       -- ^ Write valid.+       -> Signal Bit       -- ^ Write ready.+       -> Signal (Bits 2)  -- ^ Write response.+       -> Signal Bit       -- ^ Write response valid.+       -> Signal Bit       -- ^ Response ready.+       -> Signal (Bits 32) -- ^ Read address.+       -> Signal (Bits 3)  -- ^ Protection type.+       -> Signal Bit       -- ^ Read address valid.+       -> Signal Bit       -- ^ Read address ready.+       -> Signal (Bits 32) -- ^ Read data.+       -> Signal (Bits 2)  -- ^ Read response.+       -> Signal Bit       -- ^ Read valid.+       -> Signal Bit       -- ^ Read ready.    +       -> ()+     )+axi_light comp =+  exactInput  "S_AXI_ACLK"    $ \s_axi_aclk    ->       +  exactInput  "S_AXI_ARESETN" $ \s_axi_aresetn -> +  exactInput  "S_AXI_AWADDR"  $ \s_axi_awaddr  ->+  exactInput  "S_AXI_AWPROT"  $ \s_axi_awprot  ->+  exactInput  "S_AXI_AWVALID" $ \s_axi_awvalid -> +  exactOutput "S_AXI_AWREADY" $ \s_axi_awready ->+  exactInput  "S_AXI_WDATA"   $ \s_axi_wdata   ->+  exactInput  "S_AXI_WSTRB"   $ \s_axi_wstrb   ->+  exactInput  "S_AXI_WVALID"  $ \s_axi_wvalid  ->   +  exactOutput "S_AXI_WREADY"  $ \s_axi_wready  ->   +  exactOutput "S_AXI_BRESP"   $ \s_axi_bresp   ->     +  exactOutput "S_AXI_BVALID"  $ \s_axi_bvalid  ->   +  exactInput  "S_AXI_BREADY"  $ \s_axi_bready  ->   +  exactInput  "S_AXI_ARADDR"  $ \s_axi_araddr  ->+  exactInput  "S_AXI_ARPROT"  $ \s_axi_arprot  ->+  exactInput  "S_AXI_ARVALID" $ \s_axi_arvalid ->   +  exactOutput "S_AXI_ARREADY" $ \s_axi_arready ->+  exactOutput "S_AXI_RDATA"   $ \s_axi_rdata   ->     +  exactOutput "S_AXI_RRESP"   $ \s_axi_rresp   ->     +  exactOutput "S_AXI_RVALID"  $ \s_axi_rvalid  ->+  exactInput  "S_AXI_RREADY"  $ \s_axi_rready  ->   +  ret $ axi_light_impl comp+    s_axi_aclk s_axi_aresetn+    s_axi_awaddr s_axi_awprot s_axi_awvalid s_axi_awready+    s_axi_wdata  s_axi_wstrb  s_axi_wvalid  s_axi_wready+    s_axi_bresp  s_axi_bvalid s_axi_bready+    s_axi_araddr s_axi_arprot s_axi_arvalid s_axi_arready s_axi_rdata+    s_axi_rresp  s_axi_rvalid s_axi_rready     ++--------------------------------------------------------------------------------+-- ** Implementation.+--------------------------------------------------------------------------------++axi_light_impl+  :: forall instr exp pred sig . AXIPred instr exp pred+  -- Component to connect:+  => Comp instr exp pred Identity sig+  -- AXI signals:+  -> Signal Bit       -- ^ Global clock signal.+  -> Signal Bit       -- ^ Global reset signal.+  -> Signal (Bits 32) -- ^ Write address.+  -> Signal (Bits 3)  -- ^ Write channel protection type.+  -> Signal Bit       -- ^ Write address valid.+  -> Signal Bit       -- ^ Write address ready.+  -> Signal (Bits 32) -- ^ Write data.+  -> Signal (Bits 4)  -- ^ Write strobes.+  -> Signal Bit       -- ^ Write valid.+  -> Signal Bit       -- ^ Write ready.+  -> Signal (Bits 2)  -- ^ Write response.+  -> Signal Bit       -- ^ Write response valid.+  -> Signal Bit       -- ^ Response ready.+  -> Signal (Bits 32) -- ^ Read address.+  -> Signal (Bits 3)  -- ^ Protection type.+  -> Signal Bit       -- ^ Read address valid.+  -> Signal Bit       -- ^ Read address ready.+  -> Signal (Bits 32) -- ^ Read data.+  -> Signal (Bits 2)  -- ^ Read response.+  -> Signal Bit       -- ^ Read valid.+  -> Signal Bit       -- ^ Read ready.    +  -> Prog instr exp pred ()+axi_light_impl comp+    s_axi_aclk   s_axi_aresetn+    s_axi_awaddr s_axi_awprot s_axi_awvalid s_axi_awready+    s_axi_wdata  s_axi_wstrb  s_axi_wvalid  s_axi_wready+    s_axi_bresp  s_axi_bvalid s_axi_bready+    s_axi_araddr s_axi_arprot s_axi_arvalid s_axi_arready s_axi_rdata+    s_axi_rresp  s_axi_rvalid s_axi_rready+  = do+       ----------------------------------------+       -- AXI Light signals.+       --+       awaddr  <- signal "axi_awaddr"  :: Prog instr exp pred (Signal (Bits 32))+       awready <- signal "axi_awready" :: Prog instr exp pred (Signal (Bit))+       wready  <- signal "axi_wready"  :: Prog instr exp pred (Signal (Bit))+       bresp   <- signal "axi_bresp"   :: Prog instr exp pred (Signal (Bits 2))+       bvalid  <- signal "axi_bvalid"  :: Prog instr exp pred (Signal (Bit))+       araddr  <- signal "axi_araddr"  :: Prog instr exp pred (Signal (Bits 32))+       arready <- signal "axi_arready" :: Prog instr exp pred (Signal (Bit))+       rdata   <- signal "axi_rdata"   :: Prog instr exp pred (Signal (Bits 32))+       rresp   <- signal "axi_rresp"   :: Prog instr exp pred (Signal (Bits 2))+       rvalid  <- signal "axi_rvalid"  :: Prog instr exp pred (Signal (Bit))++       ----------------------------------------+       -- Signals for user logic registers.+       --+       reg_rden  <- signal "slv_reg_rden" :: Prog instr exp pred (Signal (Bit))+       reg_wren  <- signal "slv_reg_wren" :: Prog instr exp pred (Signal (Bit))+       reg_out   <- signal "reg_data_out" :: Prog instr exp pred (Signal (Bits 32))+       reg_index <- signal "byte_index"   :: Prog instr exp pred (Signal (Integer))+       registers <- declareRegisters (signatureOf comp)++       ----------------------------------------+       -- Short-hands for ...+       --+       -- > reset all input registers.+       let mReset  = resetInputs  (signatureOf comp) registers+       -- > reload all input registers.+       let mReload = reloadInputs (signatureOf comp) registers+       -- > fetch the names of all input registers.+       let mInputs = identInputs  (signatureOf comp) registers+       -- > write to output.+       let mWrite :: Prog instr exp pred ()+           mWrite = loadOutputs araddr reg_out+             (signatureOf comp)+             (registers)+       -- > read from input.+       let mRead :: Prog instr exp pred ()+           mRead = loadInputs awaddr reg_wren s_axi_wdata s_axi_wstrb+             (signatureOf comp)+             (registers)+       +       ----------------------------------------+       -- I/O Connections.+       --+       s_axi_awready <=- awready+       s_axi_wready  <=- wready+       s_axi_bresp   <=- bresp+       s_axi_bvalid  <=- bvalid+       s_axi_arready <=- arready+       s_axi_rdata   <=- rdata+       s_axi_rresp   <=- rresp+       s_axi_rvalid  <=- rvalid++       ----------------------------------------+       -- Mem. mapped register select and write+       -- logic generation.+       --+       u_wr  <- unsafeFreezeSignal wready+       u_wv  <- unsafeFreezeSignal s_axi_wvalid+       u_awr <- unsafeFreezeSignal awready+       u_awv <- unsafeFreezeSignal s_axi_awvalid+       concurrentSetSignal reg_wren+         (u_wr `and` u_wv `and` u_awr `and` u_awv)++       ----------------------------------------+       -- Mem. mapped register select and read+       -- logic generation.+       --+       u_arr <- unsafeFreezeSignal arready+       u_arv <- unsafeFreezeSignal s_axi_arvalid+       u_rv  <- unsafeFreezeSignal rvalid+       concurrentSetSignal reg_rden+         (u_arr `and` u_arv `and` not u_rv)++       ----------------------------------------+       -- AXI_AWREADY generation.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           (do awready <== low)+           (do rdy <- getSignal awready+               awv <- getSignal s_axi_awvalid+               wv  <- getSignal s_axi_wvalid+               iff (isLow rdy `and` isHigh awv `and` isHigh wv)+                 (do awready <== high)+                 (do awready <== low)))+           +       ----------------------------------------+       -- AXI_AWADDR latching.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           (do awaddr <== zeroes)+           (do rdy <- getSignal awready+               awv <- getSignal s_axi_awvalid+               wv  <- getSignal s_axi_wvalid+               when (isLow  rdy `and` isHigh awv `and` isHigh wv)+                 (awaddr <=- s_axi_awaddr)))++       ----------------------------------------+       -- AXI_WREADY generation.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           (do wready <== low)+           (do rdy <- getSignal awready+               awv <- getSignal s_axi_awvalid+               wv  <- getSignal s_axi_wvalid+               iff (isLow  rdy `and` isHigh awv `and` isHigh wv)+                 (wready <== high)+                 (wready <== low)))++       ----------------------------------------+       -- Slave register logic.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           mReset+           mRead)+       +       ----------------------------------------+       -- Write response logic.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           (do bvalid <== low+               bresp  <== zeroes)+           (do awr <- getSignal awready+               awv <- getSignal s_axi_awvalid+               wr  <- getSignal wready+               wv  <- getSignal s_axi_wvalid+               bv  <- getSignal bvalid+               br  <- getSignal s_axi_bready+               ifE ((isHigh awr `and` isHigh awv+                                `and` isHigh wr+                                `and` isHigh wv+                                `and` isLow bv),+                     do bvalid <== high+                        bresp  <== zeroes)+                   ((isHigh br  `and` isHigh bv),+                     do bvalid <== low)))++       ----------------------------------------+       -- AXI_AWREADY generation.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           (do arready <== low+               araddr  <== ones)+           (do arr <- getSignal arready+               arv <- getSignal s_axi_arvalid+               iff (isLow arr `and` isHigh arv)+                 (do arready <== high+                     araddr  <=- s_axi_araddr)+                 (do arready <== low)))++       ----------------------------------------+       -- AXI_ARVALID generation.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           (do rvalid <== low+               rresp  <== zeroes)+           (do arr <- getSignal arready+               arv <- getSignal s_axi_arvalid+               rv  <- getSignal rvalid+               rr  <- getSignal s_axi_rready+               ifE ((isHigh arr `and` isHigh arv),+                     do rvalid <== high+                        rresp  <== zeroes)+                   ((isHigh rv  `and` isHigh rr),+                     do rvalid <== low)))++       ----------------------------------------+       -- Memory mapped rigister select and+       -- read logic generaiton.+       --+       process (araddr .: s_axi_aresetn .: reg_rden .: mInputs) (do+         mWrite)++       ----------------------------------------+       -- Output register of memory read data.+       --+       process (s_axi_aclk .: []) (do+         whenRising s_axi_aclk s_axi_aresetn+           (do rdata <== zeroes)+           (do rden <- getSignal reg_rden+               when (isHigh rden)+                 (do rdata <=- reg_out)))++       ----------------------------------------+       -- User logic.+       --+       portmap comp registers+       --+       -- The end.+       ----------------------------------------+  where+    -- Application-specific design signals.+    addr_lsb, addr_bits :: Integer+    addr_lsb  = 2+    addr_bits = 2 + 1+      --addr_lsb + (widthOf comp)++--------------------------------------------------------------------------------+-- ** Helpers.+--------------------------------------------------------------------------------++-- | Declare the registers which will be used by our AXI-lite slave to store+--   values received from the master and, once filled, as input for the comp.+declareRegisters :: forall instr (exp :: * -> *) pred m a . AXIPred instr exp pred+  => Sig  instr exp pred Identity a+  -> Prog instr exp pred (Argument pred a)+declareRegisters (Ret _) = return Nil+declareRegisters (SSig _ _ sf) =+  do s <- newSignal+     a <- declareRegisters (sf s)+     return (ASig s a)+declareRegisters (SArr _ _ l af) =+  do s <- newArray (litE l)+     a <- declareRegisters (af s)+     return (AArr s a)++--------------------------------------------------------------------------------++-- | Reset the input registers.+resetInputs :: forall instr (exp :: * -> *) pred m a . AXIPred instr exp pred+  => Sig  instr exp pred Identity a+  -> Argument pred a+  -> Prog instr exp pred ()+resetInputs (Ret _)           (Nil)        = return ()+resetInputs (SSig _ Out   sf) (ASig s arg) = resetInputs (sf s) arg+resetInputs (SArr _ Out _ af) (AArr a arg) = resetInputs (af a) arg+resetInputs (SSig _ In    sf) (ASig s arg) =+  do setSignal s (litE reset)+     resetInputs (sf s) arg+resetInputs (SArr _ In  _ af) (AArr a arg) =+  do resetArray a (litE reset)+     resetInputs (af a) arg++--------------------------------------------------------------------------------++-- | Reset the input registers to their previous values.+reloadInputs :: forall instr (exp :: * -> *) pred m a . AXIPred instr exp pred+  => Sig  instr exp pred Identity a+  -> Argument pred a+  -> Prog instr exp pred ()+reloadInputs (Ret _)           (Nil)        = return ()+reloadInputs (SSig _ Out   sf) (ASig s arg) = reloadInputs (sf s) arg+reloadInputs (SArr _ Out _ af) (AArr a arg) = reloadInputs (af a) arg+reloadInputs (SSig _ In    sf) (ASig s arg) =+  do sv <- unsafeFreezeSignal s+     setSignal s sv+     reloadInputs (sf s) arg+reloadInputs (SArr _ In  l af) (AArr a arg) =+  do copyArray (a, litE 0) (a, litE 0) (litE l)+     reloadInputs (af a) arg++--------------------------------------------------------------------------------++-- | ...+loadInputs :: forall instr (exp :: * -> *) pred a . AXIPred instr exp pred+  => Signal   (Bits 32) -- ^ Address.+  -> Signal   (Bit)     -- ^ Ready.+  -> Signal   (Bits 32) -- ^ Input.+  -> Signal   (Bits 4)  -- ^ Protected bits.+  -> Sig instr exp pred Identity a+  -> Argument pred a+  -> Prog instr exp pred ()+loadInputs waddr rwren wdata wren sig arg =+  do loc   <- getBits waddr addr_lsb addr_msb+     ready <- getSignal rwren+     when (isHigh ready) $+       switched loc+         (cases 0 sig arg)+         (reloadInputs sig arg)+  where+    cases :: Integer+          -> Sig instr exp pred Identity b+          -> Argument pred b+          -> [When Integer (Prog instr exp pred)]+    cases ix (Ret _)         (Nil)        = []+    cases ix (SArr _ _ l af) (AArr a arg) = error "axi-todo: loading arrays."+    cases ix (SSig _ Out sf) (ASig s arg) = cases (ix+1) (sf s) arg+    cases ix (SSig _ In  sf) (ASig s arg) =+      is (ix) (loadInputSignal wdata wren s) : cases (ix+1) (sf s) arg++    addr_lsb, addr_msb :: exp Integer+    addr_lsb = litE 2+    addr_msb = litE 3++loadInputSignal :: forall instr (exp :: * -> *) pred a .+     (AXIPred instr exp pred, pred a, Sized a)+  => Signal (Bits 32)+  -> Signal (Bits 4)+  -> Signal a+  -> Prog instr exp pred ()+loadInputSignal wdata wren reg = for 0 size $ \byte_index ->+  do bit <- getBit wren byte_index+     when (isHigh bit) $+       copyBits (reg, byte_index*8) (wdata, byte_index*8) (litE 7)+  where+    size :: exp Integer+    size = litE $ (P.div (bits reg) 8) - 1+-- todo: I assume that `a` has a type \width\ that is some multiple of eight,+--       hence the hard-coded seven when copying.++--------------------------------------------------------------------------------++-- | ...+loadOutputs :: forall instr (exp :: * -> *) pred a . AXIPred instr exp pred+  => Signal (Bits 32) -- ^ Address.+  -> Signal (Bits 32) -- ^ Output.+  -> Sig instr exp pred Identity a+  -> Argument pred a+  -> Prog instr exp pred ()+loadOutputs araddr rout sig arg =+  do loc <- getBits araddr addr_lsb addr_msb+     switched loc+       (cases 0 sig arg)+       (setSignal rout (litE reset))+  where+    cases :: Integer+          -> Sig instr exp pred Identity b+          -> Argument pred b+          -> [When Integer (Prog instr exp pred)]+    cases ix (Ret _) (Nil) = []+    cases ix (SArr _ _ l af) (AArr a arg) = error "axi-todo: loading arrays."+    cases ix (SSig _ Out sf) (ASig s arg) = cases (ix+1) (sf s) arg+    cases ix (SSig _ In  sf) (ASig s arg) =+      is (ix) (loadOutputSignal rout s) : cases (ix+1) (sf s) arg++    addr_lsb, addr_msb :: exp Integer+    addr_lsb = litE 2+    addr_msb = litE 3++loadOutputSignal :: forall instr (exp :: * -> *) pred a .+     (AXIPred instr exp pred, pred a, PrimType a, Integral a)+  => Signal (Bits 32)+  -> Signal a+  -> Prog instr exp pred ()+loadOutputSignal rout reg =+  do r <- unsafeFreezeSignal reg+     setSignal rout (toBits r :: exp (Bits 32))++--------------------------------------------------------------------------------++identInputs :: forall instr (exp :: * -> *) pred m a .+     Sig instr exp pred m a+  -> Argument pred a+  -> [Ident]+identInputs (Ret _) (Nil) = []+identInputs (SSig _ In sf)   (ASig s arg) = toIdent s : identInputs (sf s) arg+identInputs (SSig _ _  sf)   (ASig s arg) = identInputs (sf s) arg+identInputs (SArr _ In _ af) (AArr a arg) = toIdent a : identInputs (af a) arg+identInputs (SArr _ _  _ af) (AArr a arg) = identInputs (af a) arg++--------------------------------------------------------------------------------++signatureOf :: Comp instr exp pred m a -> Sig instr exp pred m a+signatureOf (Component _ sig) = sig++widthOf :: Comp instr exp pred m a -> Integer+widthOf = go . signatureOf+  where+    go :: Sig instr exp pred m b -> Integer+    go (Ret _)        = 0+    go (SSig _ _ f)   = 1 + go (f dummy)+--  go (SArr _ _ l g) = l + go (g dummy)++dummy :: a+dummy = error "todo: evaluated dummy"++high, low :: Expr exp => exp Bit+high = true+low  = false++isHigh, isLow :: (Expr exp, Rel exp) => exp Bit -> exp Bit+isHigh e = e `eq` high+isLow  e = e `eq` low++zeroes :: (Primary exp, Typeable n, KnownNat n) => exp (Bits n)+zeroes = value 0++ones :: forall exp n. (Primary exp, Typeable n, KnownNat n) => exp (Bits n)+ones = value $ bitFromInteger (read (replicate size '1') :: Integer)+  where size = fromIntegral (ni (Proxy::Proxy n)) - 1++--------------------------------------------------------------------------------+-- Program stubs.+--------------------------------------------------------------------------------+{-+loadInputs wdata wren tmp i (SSig _ In sf) (ASig s arg) =+    When (Is i) cases : loadInputs wdata wren tmp (i+1) (sf s) arg+  where+    size :: Integer+    size = bits s++    loadBit :: Prog instr exp pred ()+    loadBit = do+      wb <- getBit wren (0 :: exp Integer)+      undefined+      when (isHigh wb) $+        do bit <- getBit wdata (0 :: exp Integer)+           setBit s (0 :: exp Integer) bit++    loadBits :: Integer -> Integer -> Prog instr exp pred ()+    loadBits ix len = do+      wb <- getBit wren (value ix)+      undefined+      when (isHigh wb) $+        copyBits (s, value $ ix*8) (wdata, value $ ix*8) (value $ len-1)++    cases :: Prog instr exp pred ()+    cases | size == 1 = loadBit+          | otherwise = sequence_ $ map (uncurry loadBits) $ zip [0..] $ chunk size+loadInputs wdata wren tmp i (SArr _ Out l af) (AArr a arg) =+    loadInputs wdata wren tmp (i+(Prelude.toInteger l)) (af a) arg+loadInputs wdata wren tmp i (SArr _ In l af) (AArr (a :: Array i b) arg)+    let cs = map (\ix -> When (Is $ i+ix) $ cases ix) [0..l'-1]+     in cs ++ loadInputs wdata wren tmp (i+l') (af a) arg+  where+    l', size :: Integer+    l'   = Prelude.toInteger l    +    size = bits a++    loadBit :: Integer -> Prog instr exp pred ()+    loadBit ax = error "axi-todo: loadBit for array."++    loadBits :: Integer -> Integer -> Integer -> Prog instr exp pred ()+    loadBits ax ix len = do+      wb <- getBit wren (value ix)+      when (isHigh wb) $+        copyVBits (tmp, value $ ix*8) (wdata, value $ ix*8) (value $ len-1)++    cases :: Integer -> Prog instr exp pred ()+    cases ax | size == 1 = loadBit ax+             | otherwise = do+      sequence_ $ map (uncurry $ loadBits ax) $ zip [0..] $ chunk size+      val :: exp (Bits 32) <- unsafeFreezeVariable tmp+      let ix = litE (fromInteger ax) :: exp i+      let b  = fromBits val          :: exp b+      undefined --setArray a ix b+-}+{-+loadOutputs o i (Ret _) (Nil) = []+loadOutputs o i (SSig _ Out sf) (ASig s arg) =+  let p = setSignal o . toBits =<< unsafeFreezeSignal s+   in When (Is i) p : loadOutputs o (i+1) (sf s) arg+loadOutputs o i (SSig _ _ sf) (ASig s arg) =+  loadOutputs o (i+1) (sf s) arg+loadOutputs o i (SArr _ Out l af) (AArr a arg) =+  let f ix = When (Is ix) (setSignal o . toBits =<< getArray a (value ix))+   in map f [i..i+l-1] ++ loadOutputs o (i+l) (af a) arg+loadOutputs o i (SArr _ _ l af) (AArr a arg) =+  loadOutputs o (i+l) (af a) arg++chunk :: Integer -> [Integer]+chunk i | i >  8 = 8 : chunk (i - 8)+        | i <= 8 = [i]+-}+--------------------------------------------------------------------------------+
src/Language/Embedded/VHDL/Monad/Type.hs view
@@ -9,7 +9,7 @@   , unconstrainedArray, constrainedArray   -- utility.   , typeName, typeRange, typeWidth-  , isBit, isBits, isSigned, isUnsigned, isInteger+  , isBit, isBits, isSigned, isUnsigned, isInteger, isFloating   ) where  import Language.VHDL@@ -159,5 +159,8 @@  isInteger :: Type -> Bool isInteger t = "integer" == typeName t++isFloating :: Type -> Bool+isFloating t = "float" == typeName t  --------------------------------------------------------------------------------