{-# LANGUAGE ScopedTypeVariables, NumericUnderscores #-}
{-# LANGUAGE DuplicateRecordFields, RecordWildCards, ApplicativeDo #-}
{-# LANGUAGE ExistentialQuantification, StandaloneDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}
module RetroClash.VGA
( VGASync(..)
, VGADriver(..)
, vgaDriver
, VGAOut(..)
, vgaOut
, VGATiming(..), VGATimings(..)
, vga640x480at60
, vga800x600at60
, vga800x600at72
, vga1024x768at60
) where
import Clash.Prelude
import Clash.Class.HasDomain
import RetroClash.Clock
import RetroClash.Utils
import Data.Maybe (isJust)
data VGASync dom = VGASync
{ VGASync dom -> "HSYNC" ::: Signal dom Bit
vgaHSync :: "HSYNC" ::: Signal dom Bit
, VGASync dom -> "VSYNC" ::: Signal dom Bit
vgaVSync :: "VSYNC" ::: Signal dom Bit
, VGASync dom -> "DE" ::: Signal dom Bool
vgaDE :: "DE" ::: Signal dom Bool
}
data VGAOut dom r g b = VGAOut
{ VGAOut dom r g b -> VGASync dom
vgaSync :: VGASync dom
, VGAOut dom r g b -> "RED" ::: Signal dom (Unsigned r)
vgaR :: "RED" ::: Signal dom (Unsigned r)
, VGAOut dom r g b -> "GREEN" ::: Signal dom (Unsigned g)
vgaG :: "GREEN" ::: Signal dom (Unsigned g)
, VGAOut dom r g b -> "BLUE" ::: Signal dom (Unsigned b)
vgaB :: "BLUE" ::: Signal dom (Unsigned b)
}
type instance HasDomain dom1 (VGAOut dom2 r g b) = DomEq dom1 dom2
type instance TryDomain t (VGAOut dom r g b) = Found dom
data VGADriver dom w h = VGADriver
{ VGADriver dom w h -> VGASync dom
vgaSync :: VGASync dom
, VGADriver dom w h -> Signal dom (Maybe (Index w))
vgaX :: Signal dom (Maybe (Index w))
, VGADriver dom w h -> Signal dom (Maybe (Index h))
vgaY :: Signal dom (Maybe (Index h))
}
data VGATiming (visible :: Nat) = forall front pulse back. VGATiming
{ VGATiming visible -> Polarity
polarity :: Polarity
, ()
preWidth :: SNat front
, ()
pulseWidth :: SNat pulse
, ()
postWidth :: SNat back
}
deriving instance Show (VGATiming vis)
data VGATimings (ps :: Nat) (w :: Nat) (h :: Nat) = VGATimings
{ VGATimings ps w h -> VGATiming w
vgaHorizTiming :: VGATiming w
, VGATimings ps w h -> VGATiming h
vgaVertTiming :: VGATiming h
}
deriving (Int -> VGATimings ps w h -> ShowS
[VGATimings ps w h] -> ShowS
VGATimings ps w h -> String
(Int -> VGATimings ps w h -> ShowS)
-> (VGATimings ps w h -> String)
-> ([VGATimings ps w h] -> ShowS)
-> Show (VGATimings ps w h)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (ps :: Nat) (w :: Nat) (h :: Nat).
Int -> VGATimings ps w h -> ShowS
forall (ps :: Nat) (w :: Nat) (h :: Nat).
[VGATimings ps w h] -> ShowS
forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> String
showList :: [VGATimings ps w h] -> ShowS
$cshowList :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
[VGATimings ps w h] -> ShowS
show :: VGATimings ps w h -> String
$cshow :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> String
showsPrec :: Int -> VGATimings ps w h -> ShowS
$cshowsPrec :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
Int -> VGATimings ps w h -> ShowS
Show)
data VGAState visible front pulse back
= Visible (Index visible)
| FrontPorch (Index front)
| SyncPulse (Index pulse)
| BackPorch (Index back)
deriving (Int -> VGAState visible front pulse back -> ShowS
[VGAState visible front pulse back] -> ShowS
VGAState visible front pulse back -> String
(Int -> VGAState visible front pulse back -> ShowS)
-> (VGAState visible front pulse back -> String)
-> ([VGAState visible front pulse back] -> ShowS)
-> Show (VGAState visible front pulse back)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Int -> VGAState visible front pulse back -> ShowS
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
[VGAState visible front pulse back] -> ShowS
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> String
showList :: [VGAState visible front pulse back] -> ShowS
$cshowList :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
[VGAState visible front pulse back] -> ShowS
show :: VGAState visible front pulse back -> String
$cshow :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> String
showsPrec :: Int -> VGAState visible front pulse back -> ShowS
$cshowsPrec :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Int -> VGAState visible front pulse back -> ShowS
Show, (forall x.
VGAState visible front pulse back
-> Rep (VGAState visible front pulse back) x)
-> (forall x.
Rep (VGAState visible front pulse back) x
-> VGAState visible front pulse back)
-> Generic (VGAState visible front pulse back)
forall x.
Rep (VGAState visible front pulse back) x
-> VGAState visible front pulse back
forall x.
VGAState visible front pulse back
-> Rep (VGAState visible front pulse back) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (visible :: Nat) (front :: Nat) (pulse :: Nat) (back :: Nat)
x.
Rep (VGAState visible front pulse back) x
-> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat) (back :: Nat)
x.
VGAState visible front pulse back
-> Rep (VGAState visible front pulse back) x
$cto :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat) (back :: Nat)
x.
Rep (VGAState visible front pulse back) x
-> VGAState visible front pulse back
$cfrom :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat) (back :: Nat)
x.
VGAState visible front pulse back
-> Rep (VGAState visible front pulse back) x
Generic, HasCallStack => String -> VGAState visible front pulse back
VGAState visible front pulse back -> Bool
VGAState visible front pulse back -> ()
VGAState visible front pulse back
-> VGAState visible front pulse back
(HasCallStack => String -> VGAState visible front pulse back)
-> (VGAState visible front pulse back -> Bool)
-> (VGAState visible front pulse back
-> VGAState visible front pulse back)
-> (VGAState visible front pulse back -> ())
-> NFDataX (VGAState visible front pulse back)
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
HasCallStack =>
String -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> Bool
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> ()
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back
-> VGAState visible front pulse back
rnfX :: VGAState visible front pulse back -> ()
$crnfX :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> ()
ensureSpine :: VGAState visible front pulse back
-> VGAState visible front pulse back
$censureSpine :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back
-> VGAState visible front pulse back
hasUndefined :: VGAState visible front pulse back -> Bool
$chasUndefined :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> Bool
deepErrorX :: String -> VGAState visible front pulse back
$cdeepErrorX :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
HasCallStack =>
String -> VGAState visible front pulse back
NFDataX)
visible :: VGAState visible front pulse back -> Maybe (Index visible)
visible :: VGAState visible front pulse back -> Maybe (Index visible)
visible (Visible Index visible
coord) = Index visible -> Maybe (Index visible)
forall a. a -> Maybe a
Just Index visible
coord
visible VGAState visible front pulse back
_ = Maybe (Index visible)
forall a. Maybe a
Nothing
sync :: VGAState visible front pulse back -> Bool
sync :: VGAState visible front pulse back -> Bool
sync SyncPulse{} = Bool
True
sync VGAState visible front pulse back
_ = Bool
False
end :: (KnownNat back) => VGAState visible front pulse back -> Bool
end :: VGAState visible front pulse back -> Bool
end (BackPorch Index back
cnt) | Index back
cnt Index back -> Index back -> Bool
forall a. Eq a => a -> a -> Bool
== Index back
forall a. Bounded a => a
maxBound = Bool
True
end VGAState visible front pulse back
_ = Bool
False
type Step a = a -> a
data VGACounter visible
= forall front pulse back. (KnownNat front, KnownNat pulse, KnownNat back)
=> VGACounter (Step (VGAState visible front pulse back))
mkVGACounter
:: SNat front -> SNat pulse -> SNat back
-> Step (VGAState visible front pulse back)
-> VGACounter visible
mkVGACounter :: SNat front
-> SNat pulse
-> SNat back
-> Step (VGAState visible front pulse back)
-> VGACounter visible
mkVGACounter SNat front
SNat SNat pulse
SNat SNat back
SNat = Step (VGAState visible front pulse back) -> VGACounter visible
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
(KnownNat front, KnownNat pulse, KnownNat back) =>
Step (VGAState visible front pulse back) -> VGACounter visible
VGACounter
vgaCounter :: (KnownNat visible) => VGATiming visible -> VGACounter visible
vgaCounter :: VGATiming visible -> VGACounter visible
vgaCounter (VGATiming Polarity
_ front :: SNat front
front@SNat front
SNat pulse :: SNat pulse
pulse@SNat pulse
SNat back :: SNat back
back@SNat back
SNat) =
SNat front
-> SNat pulse
-> SNat back
-> Step (VGAState visible front pulse back)
-> VGACounter visible
forall (front :: Nat) (pulse :: Nat) (back :: Nat)
(visible :: Nat).
SNat front
-> SNat pulse
-> SNat back
-> Step (VGAState visible front pulse back)
-> VGACounter visible
mkVGACounter SNat front
front SNat pulse
pulse SNat back
back (Step (VGAState visible front pulse back) -> VGACounter visible)
-> Step (VGAState visible front pulse back) -> VGACounter visible
forall a b. (a -> b) -> a -> b
$ \case
Visible Index visible
cnt -> (Index visible -> VGAState visible front pulse back)
-> (Index front -> VGAState visible front pulse back)
-> Index visible
-> VGAState visible front pulse back
forall (n :: Nat) (m :: Nat) a.
(KnownNat n, KnownNat m) =>
(Index n -> a) -> (Index m -> a) -> Index n -> a
count Index visible -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index visible -> VGAState visible front pulse back
Visible Index front -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index front -> VGAState visible front pulse back
FrontPorch Index visible
cnt
FrontPorch Index front
cnt -> (Index front -> VGAState visible front pulse back)
-> (Index pulse -> VGAState visible front pulse back)
-> Index front
-> VGAState visible front pulse back
forall (n :: Nat) (m :: Nat) a.
(KnownNat n, KnownNat m) =>
(Index n -> a) -> (Index m -> a) -> Index n -> a
count Index front -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index front -> VGAState visible front pulse back
FrontPorch Index pulse -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index pulse -> VGAState visible front pulse back
SyncPulse Index front
cnt
SyncPulse Index pulse
cnt -> (Index pulse -> VGAState visible front pulse back)
-> (Index back -> VGAState visible front pulse back)
-> Index pulse
-> VGAState visible front pulse back
forall (n :: Nat) (m :: Nat) a.
(KnownNat n, KnownNat m) =>
(Index n -> a) -> (Index m -> a) -> Index n -> a
count Index pulse -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index pulse -> VGAState visible front pulse back
SyncPulse Index back -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index back -> VGAState visible front pulse back
BackPorch Index pulse
cnt
BackPorch Index back
cnt -> (Index back -> VGAState visible front pulse back)
-> (Index visible -> VGAState visible front pulse back)
-> Index back
-> VGAState visible front pulse back
forall (n :: Nat) (m :: Nat) a.
(KnownNat n, KnownNat m) =>
(Index n -> a) -> (Index m -> a) -> Index n -> a
count Index back -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index back -> VGAState visible front pulse back
BackPorch Index visible -> VGAState visible front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index visible -> VGAState visible front pulse back
Visible Index back
cnt
where
count :: (KnownNat n, KnownNat m) => (Index n -> a) -> (Index m -> a) -> Index n -> a
count :: (Index n -> a) -> (Index m -> a) -> Index n -> a
count Index n -> a
this Index m -> a
next = a -> (Index n -> a) -> Maybe (Index n) -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Index m -> a
next Index m
0) Index n -> a
this (Maybe (Index n) -> a)
-> (Index n -> Maybe (Index n)) -> Index n -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index n -> Maybe (Index n)
forall a. (Eq a, Enum a, Bounded a) => a -> Maybe a
succIdx
vgaDriver
:: (HiddenClockResetEnable dom, KnownNat w, KnownNat h)
=> (DomainPeriod dom ~ ps)
=> VGATimings ps w h
-> VGADriver dom w h
vgaDriver :: VGATimings ps w h -> VGADriver dom w h
vgaDriver VGATimings{VGATiming w
VGATiming h
vgaVertTiming :: VGATiming h
vgaHorizTiming :: VGATiming w
$sel:vgaVertTiming:VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> VGATiming h
$sel:vgaHorizTiming:VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> VGATiming w
..} = case (VGATiming w -> VGACounter w
forall (visible :: Nat).
KnownNat visible =>
VGATiming visible -> VGACounter visible
vgaCounter VGATiming w
vgaHorizTiming, VGATiming h -> VGACounter h
forall (visible :: Nat).
KnownNat visible =>
VGATiming visible -> VGACounter visible
vgaCounter VGATiming h
vgaVertTiming) of
(VGACounter Step (VGAState w front pulse back)
nextH, VGACounter Step (VGAState h front pulse back)
nextV) -> VGADriver :: forall (dom :: Symbol) (w :: Nat) (h :: Nat).
VGASync dom
-> Signal dom (Maybe (Index w))
-> Signal dom (Maybe (Index h))
-> VGADriver dom w h
VGADriver{ $sel:vgaSync:VGADriver :: VGASync dom
vgaSync = VGASync :: forall (dom :: Symbol).
("HSYNC" ::: Signal dom Bit)
-> ("HSYNC" ::: Signal dom Bit)
-> ("DE" ::: Signal dom Bool)
-> VGASync dom
VGASync{Signal dom Bool
Signal dom Bit
vgaDE :: Signal dom Bool
vgaVSync :: Signal dom Bit
vgaHSync :: Signal dom Bit
$sel:vgaDE:VGASync :: Signal dom Bool
$sel:vgaVSync:VGASync :: Signal dom Bit
$sel:vgaHSync:VGASync :: Signal dom Bit
..}, Signal dom (Maybe (Index w))
Signal dom (Maybe (Index h))
vgaY :: Signal dom (Maybe (Index h))
vgaX :: Signal dom (Maybe (Index w))
$sel:vgaY:VGADriver :: Signal dom (Maybe (Index h))
$sel:vgaX:VGADriver :: Signal dom (Maybe (Index w))
.. }
where
stateH :: Signal dom (VGAState w front pulse back)
stateH = VGAState w front pulse back
-> Signal dom (VGAState w front pulse back)
-> Signal dom (VGAState w front pulse back)
forall (dom :: Symbol) a.
(HiddenClockResetEnable dom, NFDataX a) =>
a -> Signal dom a -> Signal dom a
register (Index w -> VGAState w front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index visible -> VGAState visible front pulse back
Visible Index w
0) (Signal dom (VGAState w front pulse back)
-> Signal dom (VGAState w front pulse back))
-> Signal dom (VGAState w front pulse back)
-> Signal dom (VGAState w front pulse back)
forall a b. (a -> b) -> a -> b
$ Step (VGAState w front pulse back)
nextH Step (VGAState w front pulse back)
-> Signal dom (VGAState w front pulse back)
-> Signal dom (VGAState w front pulse back)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (VGAState w front pulse back)
stateH
stateV :: Signal dom (VGAState h front pulse back)
stateV = VGAState h front pulse back
-> Signal dom Bool
-> Signal dom (VGAState h front pulse back)
-> Signal dom (VGAState h front pulse back)
forall (dom :: Symbol) a.
(HiddenClockResetEnable dom, NFDataX a) =>
a -> Signal dom Bool -> Signal dom a -> Signal dom a
regEn (Index h -> VGAState h front pulse back
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Index visible -> VGAState visible front pulse back
Visible Index h
0) Signal dom Bool
endLine (Signal dom (VGAState h front pulse back)
-> Signal dom (VGAState h front pulse back))
-> Signal dom (VGAState h front pulse back)
-> Signal dom (VGAState h front pulse back)
forall a b. (a -> b) -> a -> b
$ Step (VGAState h front pulse back)
nextV Step (VGAState h front pulse back)
-> Signal dom (VGAState h front pulse back)
-> Signal dom (VGAState h front pulse back)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (VGAState h front pulse back)
stateV
vgaX :: Signal dom (Maybe (Index w))
vgaX = VGAState w front pulse back -> Maybe (Index w)
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> Maybe (Index visible)
visible (VGAState w front pulse back -> Maybe (Index w))
-> Signal dom (VGAState w front pulse back)
-> Signal dom (Maybe (Index w))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (VGAState w front pulse back)
stateH
vgaHSync :: Signal dom Bit
vgaHSync = Polarity -> Bool -> Bit
toActiveDyn (VGATiming w -> Polarity
forall (visible :: Nat). VGATiming visible -> Polarity
polarity VGATiming w
vgaHorizTiming) (Bool -> Bit)
-> (VGAState w front pulse back -> Bool)
-> VGAState w front pulse back
-> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VGAState w front pulse back -> Bool
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> Bool
sync (VGAState w front pulse back -> Bit)
-> Signal dom (VGAState w front pulse back) -> Signal dom Bit
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (VGAState w front pulse back)
stateH
endLine :: Signal dom Bool
endLine = VGAState w front pulse back -> Bool
forall (back :: Nat) (visible :: Nat) (front :: Nat)
(pulse :: Nat).
KnownNat back =>
VGAState visible front pulse back -> Bool
end (VGAState w front pulse back -> Bool)
-> Signal dom (VGAState w front pulse back) -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (VGAState w front pulse back)
stateH
vgaY :: Signal dom (Maybe (Index h))
vgaY = VGAState h front pulse back -> Maybe (Index h)
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> Maybe (Index visible)
visible (VGAState h front pulse back -> Maybe (Index h))
-> Signal dom (VGAState h front pulse back)
-> Signal dom (Maybe (Index h))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (VGAState h front pulse back)
stateV
vgaVSync :: Signal dom Bit
vgaVSync = Polarity -> Bool -> Bit
toActiveDyn (VGATiming h -> Polarity
forall (visible :: Nat). VGATiming visible -> Polarity
polarity VGATiming h
vgaVertTiming) (Bool -> Bit)
-> (VGAState h front pulse back -> Bool)
-> VGAState h front pulse back
-> Bit
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VGAState h front pulse back -> Bool
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
VGAState visible front pulse back -> Bool
sync (VGAState h front pulse back -> Bit)
-> Signal dom (VGAState h front pulse back) -> Signal dom Bit
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (VGAState h front pulse back)
stateV
vgaDE :: Signal dom Bool
vgaDE = Maybe (Index w) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Index w) -> Bool)
-> Signal dom (Maybe (Index w)) -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Maybe (Index w))
vgaX Signal dom Bool -> Signal dom Bool -> Signal dom Bool
forall (f :: Type -> Type).
Applicative f =>
f Bool -> f Bool -> f Bool
.&&. Maybe (Index h) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Index h) -> Bool)
-> Signal dom (Maybe (Index h)) -> Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Maybe (Index h))
vgaY
vgaOut
:: (HiddenClockResetEnable dom, KnownNat r, KnownNat g, KnownNat b)
=> VGASync dom
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> VGAOut dom r g b
vgaOut :: VGASync dom
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> VGAOut dom r g b
vgaOut vgaSync :: VGASync dom
vgaSync@VGASync{"DE" ::: Signal dom Bool
"VSYNC" ::: Signal dom Bit
vgaDE :: "DE" ::: Signal dom Bool
vgaVSync :: "VSYNC" ::: Signal dom Bit
vgaHSync :: "VSYNC" ::: Signal dom Bit
$sel:vgaDE:VGASync :: forall (dom :: Symbol). VGASync dom -> "DE" ::: Signal dom Bool
$sel:vgaVSync:VGASync :: forall (dom :: Symbol). VGASync dom -> "HSYNC" ::: Signal dom Bit
$sel:vgaHSync:VGASync :: forall (dom :: Symbol). VGASync dom -> "HSYNC" ::: Signal dom Bit
..} Signal dom (Unsigned r, Unsigned g, Unsigned b)
rgb = VGAOut :: forall (dom :: Symbol) (r :: Nat) (g :: Nat) (b :: Nat).
VGASync dom
-> ("RED" ::: Signal dom (Unsigned r))
-> ("GREEN" ::: Signal dom (Unsigned g))
-> ("BLUE" ::: Signal dom (Unsigned b))
-> VGAOut dom r g b
VGAOut{"RED" ::: Signal dom (Unsigned r)
"GREEN" ::: Signal dom (Unsigned g)
"BLUE" ::: Signal dom (Unsigned b)
VGASync dom
vgaB :: "BLUE" ::: Signal dom (Unsigned b)
vgaG :: "GREEN" ::: Signal dom (Unsigned g)
vgaR :: "RED" ::: Signal dom (Unsigned r)
vgaSync :: VGASync dom
$sel:vgaB:VGAOut :: "BLUE" ::: Signal dom (Unsigned b)
$sel:vgaG:VGAOut :: "GREEN" ::: Signal dom (Unsigned g)
$sel:vgaR:VGAOut :: "RED" ::: Signal dom (Unsigned r)
$sel:vgaSync:VGAOut :: VGASync dom
..}
where
("RED" ::: Signal dom (Unsigned r)
vgaR, "GREEN" ::: Signal dom (Unsigned g)
vgaG, "BLUE" ::: Signal dom (Unsigned b)
vgaB) = Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Unbundled dom (Unsigned r, Unsigned g, Unsigned b)
forall a (dom :: Symbol).
Bundle a =>
Signal dom a -> Unbundled dom a
unbundle (Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Unbundled dom (Unsigned r, Unsigned g, Unsigned b))
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Unbundled dom (Unsigned r, Unsigned g, Unsigned b)
forall a b. (a -> b) -> a -> b
$ Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
blank Signal dom (Unsigned r, Unsigned g, Unsigned b)
rgb
blank :: Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
blank = ("DE" ::: Signal dom Bool)
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
forall (f :: Type -> Type) a.
Applicative f =>
f Bool -> f a -> f a -> f a
mux (Bool -> Bool
not (Bool -> Bool)
-> ("DE" ::: Signal dom Bool) -> "DE" ::: Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> "DE" ::: Signal dom Bool
vgaDE) ((Unsigned r, Unsigned g, Unsigned b)
-> Signal dom (Unsigned r, Unsigned g, Unsigned b)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Unsigned r
0, Unsigned g
0, Unsigned b
0))
vga640x480at60 :: VGATimings (HzToPeriod 25_175_000) 640 480
vga640x480at60 :: VGATimings (HzToPeriod 25175000) 640 480
vga640x480at60 = VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATiming w -> VGATiming h -> VGATimings ps w h
VGATimings
{ $sel:vgaHorizTiming:VGATimings :: VGATiming 640
vgaHorizTiming = Polarity -> SNat 16 -> SNat 96 -> SNat 48 -> VGATiming 640
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
Low (KnownNat 16 => SNat 16
forall (n :: Nat). KnownNat n => SNat n
SNat @16) (KnownNat 96 => SNat 96
forall (n :: Nat). KnownNat n => SNat n
SNat @96) (KnownNat 48 => SNat 48
forall (n :: Nat). KnownNat n => SNat n
SNat @48)
, $sel:vgaVertTiming:VGATimings :: VGATiming 480
vgaVertTiming = Polarity -> SNat 11 -> SNat 2 -> SNat 31 -> VGATiming 480
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
Low (KnownNat 11 => SNat 11
forall (n :: Nat). KnownNat n => SNat n
SNat @11) (KnownNat 2 => SNat 2
forall (n :: Nat). KnownNat n => SNat n
SNat @2) (KnownNat 31 => SNat 31
forall (n :: Nat). KnownNat n => SNat n
SNat @31)
}
vga800x600at72 :: VGATimings (HzToPeriod 50_000_000) 800 600
vga800x600at72 :: VGATimings (HzToPeriod 50000000) 800 600
vga800x600at72 = VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATiming w -> VGATiming h -> VGATimings ps w h
VGATimings
{ $sel:vgaHorizTiming:VGATimings :: VGATiming 800
vgaHorizTiming = Polarity -> SNat 56 -> SNat 120 -> SNat 64 -> VGATiming 800
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
High (KnownNat 56 => SNat 56
forall (n :: Nat). KnownNat n => SNat n
SNat @56) (KnownNat 120 => SNat 120
forall (n :: Nat). KnownNat n => SNat n
SNat @120) (KnownNat 64 => SNat 64
forall (n :: Nat). KnownNat n => SNat n
SNat @64)
, $sel:vgaVertTiming:VGATimings :: VGATiming 600
vgaVertTiming = Polarity -> SNat 37 -> SNat 6 -> SNat 23 -> VGATiming 600
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
High (KnownNat 37 => SNat 37
forall (n :: Nat). KnownNat n => SNat n
SNat @37) (KnownNat 6 => SNat 6
forall (n :: Nat). KnownNat n => SNat n
SNat @6) (KnownNat 23 => SNat 23
forall (n :: Nat). KnownNat n => SNat n
SNat @23)
}
vga800x600at60 :: VGATimings (HzToPeriod 40_000_000) 800 600
vga800x600at60 :: VGATimings (HzToPeriod 40000000) 800 600
vga800x600at60 = VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATiming w -> VGATiming h -> VGATimings ps w h
VGATimings
{ $sel:vgaHorizTiming:VGATimings :: VGATiming 800
vgaHorizTiming = Polarity -> SNat 40 -> SNat 128 -> SNat 88 -> VGATiming 800
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
High (KnownNat 40 => SNat 40
forall (n :: Nat). KnownNat n => SNat n
SNat @40) (KnownNat 128 => SNat 128
forall (n :: Nat). KnownNat n => SNat n
SNat @128) (KnownNat 88 => SNat 88
forall (n :: Nat). KnownNat n => SNat n
SNat @88)
, $sel:vgaVertTiming:VGATimings :: VGATiming 600
vgaVertTiming = Polarity -> SNat 1 -> SNat 4 -> SNat 23 -> VGATiming 600
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
High (KnownNat 1 => SNat 1
forall (n :: Nat). KnownNat n => SNat n
SNat @1) (KnownNat 4 => SNat 4
forall (n :: Nat). KnownNat n => SNat n
SNat @4) (KnownNat 23 => SNat 23
forall (n :: Nat). KnownNat n => SNat n
SNat @23)
}
vga1024x768at60 :: VGATimings (HzToPeriod 65_000_000) 1024 768
vga1024x768at60 :: VGATimings (HzToPeriod 65000000) 1024 768
vga1024x768at60 = VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATiming w -> VGATiming h -> VGATimings ps w h
VGATimings
{ $sel:vgaHorizTiming:VGATimings :: VGATiming 1024
vgaHorizTiming = Polarity -> SNat 24 -> SNat 136 -> SNat 160 -> VGATiming 1024
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
Low (KnownNat 24 => SNat 24
forall (n :: Nat). KnownNat n => SNat n
SNat @24) (KnownNat 136 => SNat 136
forall (n :: Nat). KnownNat n => SNat n
SNat @136) (KnownNat 160 => SNat 160
forall (n :: Nat). KnownNat n => SNat n
SNat @160)
, $sel:vgaVertTiming:VGATimings :: VGATiming 768
vgaVertTiming = Polarity -> SNat 3 -> SNat 6 -> SNat 29 -> VGATiming 768
forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
(back :: Nat).
Polarity
-> SNat front -> SNat pulse -> SNat back -> VGATiming visible
VGATiming Polarity
Low (KnownNat 3 => SNat 3
forall (n :: Nat). KnownNat n => SNat n
SNat @3) (KnownNat 6 => SNat 6
forall (n :: Nat). KnownNat n => SNat n
SNat @6) (KnownNat 29 => SNat 29
forall (n :: Nat). KnownNat n => SNat n
SNat @29)
}