examples/GArrowVerilog.hs

   1 {-# LANGUAGE MultiParamTypeClasses, TypeOperators, FunctionalDependencies, TypeFamilies, FlexibleContexts, RankNTypes, GADTs, MultiParamTypeClasses, ScopedTypeVariables, FlexibleInstances, UndecidableInstances #-}
   2 -- {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
   3 module GArrowVerilog where
   4 import Control.GArrow
   5 import Control.Monad.State
   6 import Data.List (intercalate)
   7 import Control.Category
   8 import Control.Monad ((>=>), (<=<))
   9 import Prelude hiding (id, (.))
  10 import Text.PrettyPrint.HughesPJ
  11 import BitSerialHardware
  12 import GArrowPretty
  13
  14
  15 ------------------------------------------------------------------------------
  16 -- Declaration Types (basically (Tree ()))
  17
  18 data DeclType t where
  19   DeclTypeUnit :: DeclType ()
  20   DeclTypeWire :: DeclType Wire
  21   DeclTypePair :: DeclType x -> DeclType y -> DeclType (x,y)
  22
  23 instance Show (DeclType t) where
  24   show DeclTypeUnit       = "()"
  25   show DeclTypeWire       = "Wire"
  26   show (DeclTypePair x y) = case x of
  27                            DeclTypePair _ _ -> "(" ++ show x ++ ")*" ++ show y
  28                            _                ->        show x ++  "*" ++ show y
  29
  30 ------------------------------------------------------------------------------
  31 -- Identifiers
  32
  33 data Id t where
  34   IdUnit    :: Id ()
  35   IdWire    :: String -> Id Wire
  36   IdPair    :: Id x -> Id y -> Id (x,y)
  37
  38 instance Show (Id t) where
  39   show IdUnit       = "()"
  40   show (IdWire n)   = n
  41   show (IdPair x y) = (show x) ++ "," ++ (show y)
  42
  43 id2shape :: Id t -> DeclType t
  44 id2shape  IdUnit    = DeclTypeUnit
  45 id2shape (IdWire _) = DeclTypeWire
  46 id2shape (IdPair x y) = DeclTypePair (id2shape x) (id2shape y)
  47
  48
  49 ------------------------------------------------------------------------------
  50 -- Verilog Writer
  51
  52 class Monad vw => VerilogWriter vw where
  53   declareWire   :: DeclType t -> vw (Id t)
  54   gate          :: String -> [Id Wire] -> vw ()
  55
  56 instance MonadState VState m => VerilogWriter m where
  57   declareWire   DeclTypeUnit      = return IdUnit
  58   declareWire  (DeclTypePair x y) = do ix <- declareWire x ; iy <- declareWire y ; return $ IdPair ix iy
  59   declareWire   DeclTypeWire      = do (VState x decls out) <- get
  60                                        let ids = "wire"++(show x)
  61                                        put $ VState (x+1) ((text "wire" <+> text ids <> semi):decls) out
  62                                        return $ IdWire $ ids
  63   gate name inputs = let output = text name <+> (parens $ hsep $ punctuate comma $ map (text . show) inputs) <> semi
  64                      in do (VState x decls out) <- get
  65                            put $ VState x decls (output:out)
  66
  67
  68 ------------------------------------------------------------------------------
  69 -- Instance of Verilog Writer
  70
  71 data VState = VState Int [Doc] [Doc]
  72
  73 data V vw x y = V
  74    { infer :: DeclType x -> DeclType y
  75    , write :: Id x -> vw (Id y)
  76    }
  77
  78 instance VerilogWriter vw => Category (V vw) where
  79   id    = V { infer = id
  80             , write = return }
  81   g . f = V { infer = infer g . infer f
  82             , write = write g <=< write f }
  83
  84
  85
  86 ------------------------------------------------------------------------------
  87 -- GArrow implementation
  88
  89 instance VerilogWriter vw => GArrow (V vw) (,) () where
  90   ga_cancell     = V { infer = \(DeclTypePair DeclTypeUnit sx) -> sx
  91                      , write = \(IdPair IdUnit x) -> return x }
  92   ga_cancelr     = V { infer = \(DeclTypePair sx DeclTypeUnit) -> sx
  93                      , write = \(IdPair x IdUnit) -> return x }
  94   ga_uncancell   = V { infer = \s -> DeclTypePair DeclTypeUnit s
  95                      , write = \x -> return (IdPair IdUnit x) }
  96   ga_uncancelr   = V { infer = \s -> DeclTypePair s DeclTypeUnit
  97                      , write = \x -> return (IdPair x IdUnit) }
  98   ga_assoc       = V { infer = \(DeclTypePair (DeclTypePair sx sy) sz) -> DeclTypePair sx (DeclTypePair sy sz)
  99                      , write = \(IdPair (IdPair x y) z) -> return $ IdPair x (IdPair y z) }
 100   ga_unassoc     = V { infer = \(DeclTypePair sx (DeclTypePair sy sz)) -> (DeclTypePair (DeclTypePair sx sy) sz)
 101                      , write = \(IdPair x (IdPair y z)) -> return $ IdPair (IdPair x y) z }
 102   ga_first     f = V { infer = \(DeclTypePair sx sz) -> DeclTypePair (infer f sx) sz
 103                      , write = \(IdPair x z) -> do idy <- write f x ; return $ IdPair idy z }
 104   ga_second    f = V { infer = \(DeclTypePair sz sx) -> DeclTypePair sz (infer f sx)
 105                      , write = \(IdPair z x) -> do idy <- write f x ; return $ IdPair z idy }
 106
 107 instance VerilogWriter vw => GArrowDrop (V vw) (,) () where
 108   ga_drop = V { infer = \_ -> DeclTypeUnit
 109               , write = \_ -> return IdUnit }
 110
 111 instance VerilogWriter vw => GArrowCopy (V vw) (,) () where
 112   ga_copy = V { infer = \s -> DeclTypePair s s
 113               , write = \x -> return $ IdPair x x }
 114
 115 instance VerilogWriter vw => GArrowSwap (V vw) (,) () where
 116   ga_swap = V { infer = \(DeclTypePair x y) -> DeclTypePair y x
 117               , write = \(IdPair x y) -> return $ IdPair y x }
 118
 119 instance VerilogWriter vw => GArrowLoop (V vw) (,) () where
 120   ga_loopl f = ga_loopr $ ga_swap >>> f >>> ga_swap
 121   ga_loopr f = V { infer = \x -> let yz = infer f (DeclTypePair x (case yz of (DeclTypePair y z) -> z))
 122                                  in (case yz of (DeclTypePair y z) -> y)
 123                  , write = \idx -> let yz = infer f (DeclTypePair (id2shape idx) (case yz of (DeclTypePair y z) -> z))
 124                                    in case yz of (DeclTypePair y z) -> do idz  <- declareWire z
 125                                                                           idyz <- write f (IdPair idx idz)
 126                                                                           return (case idyz of (IdPair y z) -> y)
 127                  }
 128
 129 gate1 :: VerilogWriter vw => String -> Id Wire -> vw (Id Wire)
 130 gate1 name x =
 131   do out <- declareWire DeclTypeWire
 132      gate name [out,x]
 133      return out
 134
 135 gate2 :: VerilogWriter vw => String -> Id (Wire,Wire) -> vw (Id Wire)
 136 gate2 name (IdPair x y) =
 137   do out <- declareWire DeclTypeWire
 138      gate name [out,x,y]
 139      return out
 140
 141 gate3 :: VerilogWriter vw => String -> Id (Wire,(Wire,Wire)) -> vw (Id Wire)
 142 gate3 name (IdPair x (IdPair y z)) =
 143   do out <- declareWire DeclTypeWire
 144      gate name [out,x,y,z]
 145      return out
 146
 147 instance VerilogWriter vw => BitSerialHardwarePrimitives (V vw) where
 148   high        = V { infer = const DeclTypeWire , write = const $ return $ IdWire "1'b1" }
 149   low         = V { infer = const DeclTypeWire , write = const $ return $ IdWire "1'b0" }
 150   not         = V { infer = const DeclTypeWire , write = gate1 "not" }
 151   xor         = V { infer = const DeclTypeWire , write = gate2 "xor" }
 152   or          = V { infer = const DeclTypeWire , write = gate2 "or" }
 153   and         = V { infer = const DeclTypeWire , write = gate2 "and" }
 154   mux2        = V { infer = const DeclTypeWire , write = gate3 "mux2" }
 155   maj3        = V { infer = const DeclTypeWire , write = gate3 "maj3" }
 156   reg         = V { infer = const DeclTypeWire , write = gate1 "reg" }
 157   loop   vals = undefined
 158   fifo   len  = undefined
 159   probe  id   = undefined
 160   oracle id   = undefined
 161
 162
 163 ------------------------------------------------------------------------------
 164 -- Examples
 165
 166 oscillator :: BitSerialHardwarePrimitives v => v Wire Wire
 167 oscillator = ga_loopl $ ga_first reg >>> xor >>> ga_copy
 168
 169 sample2 :: MonadState VState m => V m Wire Wire
 170 sample2 = oscillator
 171
 172 sample3 :: V (StateT VState IO) Wire Wire
 173 sample3 = sample2
 174
 175 writeModule moduleName verilog =
 176   do (VState _ decls out) <- execStateT (write verilog (IdWire "inputWire")) (VState 0 [] [])
 177      let portNames = [ "inputWire" ]
 178      let ports = map text portNames
 179      let out' = vcat [ text "module" <+> text moduleName <> (parens $ sep $ punctuate comma ports)
 180                      , nest 2 (vcat $ reverse decls)
 181                      , text ""
 182                      , nest 2 (vcat $ reverse out)
 183                      , text "endmodule"
 184                      ]
 185      return out'
 186
 187 main :: IO ()
 188 main = do putStrLn $ renderStyle (style{mode=PageMode, ribbonsPerLine=0.1}) $ pprGArrow oscillator
 189           putStrLn ""
 190           out' <- writeModule "foo" sample3
 191           putStrLn $ renderStyle (style{mode=PageMode, ribbonsPerLine=0.1}) out'
 192
 193 submodule :: V vw inputs outputs -> V vw inputs outputs
 194 submodule = undefined
 195
 196 --main = do putStrLn $ show (DeclTypePair (DeclTypePair DeclTypeWire DeclTypeUnit) (DeclTypePair DeclTypeUnit DeclTypeWire))