{-# 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 RetroClash.Clock
import RetroClash.Utils
import Data.Maybe (isJust)

data VGASync dom = VGASync
    { forall (dom :: Domain). VGASync dom -> "HSYNC" ::: Signal dom Bit
vgaHSync :: "HSYNC" ::: Signal dom Bit
    , forall (dom :: Domain). VGASync dom -> "HSYNC" ::: Signal dom Bit
vgaVSync :: "VSYNC" ::: Signal dom Bit
    , forall (dom :: Domain). VGASync dom -> "DE" ::: Signal dom Bool
vgaDE :: "DE" ::: Signal dom Bool
    }

data VGAOut dom r g b = VGAOut
    { forall (dom :: Domain) (r :: Nat) (g :: Nat) (b :: Nat).
VGAOut dom r g b -> VGASync dom
vgaSync  :: VGASync dom
    , forall (dom :: Domain) (r :: Nat) (g :: Nat) (b :: Nat).
VGAOut dom r g b -> "RED" ::: Signal dom (Unsigned r)
vgaR     :: "RED" ::: Signal dom (Unsigned r)
    , forall (dom :: Domain) (r :: Nat) (g :: Nat) (b :: Nat).
VGAOut dom r g b -> "GREEN" ::: Signal dom (Unsigned g)
vgaG     :: "GREEN" ::: Signal dom (Unsigned g)
    , forall (dom :: Domain) (r :: Nat) (g :: Nat) (b :: Nat).
VGAOut dom r g b -> "BLUE" ::: Signal dom (Unsigned b)
vgaB     :: "BLUE" ::: Signal dom (Unsigned b)
    }

data VGADriver dom w h = VGADriver
    { forall (dom :: Domain) (w :: Nat) (h :: Nat).
VGADriver dom w h -> VGASync dom
vgaSync :: VGASync dom
    , forall (dom :: Domain) (w :: Nat) (h :: Nat).
VGADriver dom w h -> Signal dom (Maybe (Index w))
vgaX :: Signal dom (Maybe (Index w))
    , forall (dom :: Domain) (w :: Nat) (h :: Nat).
VGADriver dom w h -> Signal dom (Maybe (Index h))
vgaY :: Signal dom (Maybe (Index h))
    }

data VGATiming (visible :: Nat) = forall front pulse back. VGATiming
    { forall (visible :: Nat). 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
    { forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> VGATiming w
vgaHorizTiming :: VGATiming w
    , forall (ps :: Nat) (w :: Nat) (h :: Nat).
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 (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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
Int -> VGATimings ps w h -> ShowS
showsPrec :: Int -> VGATimings ps w h -> ShowS
$cshow :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> String
show :: VGATimings ps w h -> String
$cshowList :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
[VGATimings ps w h] -> ShowS
showList :: [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 (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
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
Int -> VGAState visible front pulse back -> ShowS
showsPrec :: Int -> VGAState visible front pulse back -> ShowS
$cshow :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
VGAState visible front pulse back -> String
show :: VGAState visible front pulse back -> String
$cshowList :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
[VGAState visible front pulse back] -> ShowS
showList :: [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 (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
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
$cfrom :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat) (back :: Nat)
       x.
VGAState visible front pulse back
-> Rep (VGAState visible front pulse back) x
from :: forall 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
to :: forall x.
Rep (VGAState visible front pulse back) x
-> VGAState visible front pulse back
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 (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
forall a.
(HasCallStack => String -> a)
-> (a -> Bool) -> (a -> a) -> (a -> ()) -> NFDataX a
$cdeepErrorX :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
HasCallStack =>
String -> VGAState visible front pulse back
deepErrorX :: HasCallStack => String -> VGAState visible front pulse back
$chasUndefined :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
VGAState visible front pulse back -> Bool
hasUndefined :: VGAState visible front pulse back -> Bool
$censureSpine :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
VGAState visible front pulse back
-> VGAState visible front pulse back
ensureSpine :: VGAState visible front pulse back
-> VGAState visible front pulse back
$crnfX :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
VGAState visible front pulse back -> ()
rnfX :: VGAState visible front pulse back -> ()
NFDataX)

visible :: VGAState visible front pulse back -> Maybe (Index visible)
visible :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
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 :: forall (visible :: Nat) (front :: Nat) (pulse :: Nat)
       (back :: Nat).
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 :: forall (back :: Nat) (visible :: Nat) (front :: Nat)
       (pulse :: Nat).
KnownNat back =>
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 :: 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
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 :: forall (visible :: Nat).
KnownNat visible =>
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 :: forall (n :: Nat) (m :: Nat) a.
(KnownNat n, KnownNat m) =>
(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 :: forall (dom :: Domain) (w :: Nat) (h :: Nat) (ps :: Nat).
(HiddenClockResetEnable dom, KnownNat w, KnownNat h,
 DomainPeriod dom ~ ps) =>
VGATimings ps w h -> VGADriver dom w h
vgaDriver VGATimings{VGATiming w
VGATiming h
$sel:vgaHorizTiming:VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> VGATiming w
$sel:vgaVertTiming:VGATimings :: forall (ps :: Nat) (w :: Nat) (h :: Nat).
VGATimings ps w h -> VGATiming h
vgaHorizTiming :: VGATiming w
vgaVertTiming :: VGATiming h
..} = 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{ $sel:vgaSync:VGADriver :: VGASync dom
vgaSync = VGASync{"DE" ::: Signal dom Bool
"HSYNC" ::: Signal dom Bit
$sel:vgaHSync:VGASync :: "HSYNC" ::: Signal dom Bit
$sel:vgaVSync:VGASync :: "HSYNC" ::: Signal dom Bit
$sel:vgaDE:VGASync :: "DE" ::: Signal dom Bool
vgaHSync :: "HSYNC" ::: Signal dom Bit
vgaVSync :: "HSYNC" ::: Signal dom Bit
vgaDE :: "DE" ::: Signal dom Bool
..}, Signal dom (Maybe (Index w))
Signal dom (Maybe (Index h))
$sel:vgaX:VGADriver :: Signal dom (Maybe (Index w))
$sel:vgaY:VGADriver :: Signal dom (Maybe (Index h))
vgaX :: Signal dom (Maybe (Index w))
vgaY :: Signal dom (Maybe (Index h))
.. }
      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 :: Domain) 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
-> ("DE" ::: Signal dom Bool)
-> Signal dom (VGAState h front pulse back)
-> Signal dom (VGAState h front pulse back)
forall (dom :: Domain) 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) "DE" ::: 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 :: "HSYNC" ::: 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)
-> "HSYNC" ::: 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 :: "DE" ::: 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)
-> "DE" ::: 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 :: "HSYNC" ::: 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)
-> "HSYNC" ::: 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 :: "DE" ::: Signal dom Bool
vgaDE = Maybe (Index w) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Index w) -> Bool)
-> Signal dom (Maybe (Index w)) -> "DE" ::: Signal dom Bool
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Signal dom (Maybe (Index w))
vgaX ("DE" ::: Signal dom Bool)
-> ("DE" ::: Signal dom Bool) -> "DE" ::: 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)) -> "DE" ::: 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 :: forall (dom :: Domain) (r :: Nat) (g :: Nat) (b :: Nat).
(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 :: VGASync dom
vgaSync@VGASync{"DE" ::: Signal dom Bool
"VSYNC" ::: Signal dom Bit
$sel:vgaHSync:VGASync :: forall (dom :: Domain). VGASync dom -> "HSYNC" ::: Signal dom Bit
$sel:vgaVSync:VGASync :: forall (dom :: Domain). VGASync dom -> "HSYNC" ::: Signal dom Bit
$sel:vgaDE:VGASync :: forall (dom :: Domain). VGASync dom -> "DE" ::: Signal dom Bool
vgaHSync :: "VSYNC" ::: Signal dom Bit
vgaVSync :: "VSYNC" ::: Signal dom Bit
vgaDE :: "DE" ::: Signal dom Bool
..} Signal dom (Unsigned r, Unsigned g, Unsigned b)
rgb = VGAOut{"RED" ::: Signal dom (Unsigned r)
"GREEN" ::: Signal dom (Unsigned g)
"BLUE" ::: Signal dom (Unsigned b)
VGASync dom
$sel:vgaSync:VGAOut :: VGASync dom
$sel:vgaR:VGAOut :: "RED" ::: Signal dom (Unsigned r)
$sel:vgaG:VGAOut :: "GREEN" ::: Signal dom (Unsigned g)
$sel:vgaB:VGAOut :: "BLUE" ::: Signal dom (Unsigned b)
vgaSync :: VGASync dom
vgaR :: "RED" ::: Signal dom (Unsigned r)
vgaG :: "GREEN" ::: Signal dom (Unsigned g)
vgaB :: "BLUE" ::: Signal dom (Unsigned b)
..}
  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 :: Domain).
Bundle a =>
Signal dom a -> Unbundled dom a
forall (dom :: Domain).
Signal dom (Unsigned r, Unsigned g, Unsigned b)
-> Unbundled dom (Unsigned r, Unsigned g, Unsigned b)
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 a. a -> Signal dom a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (Unsigned r
0, Unsigned g
0, Unsigned b
0))

-- | VGA 640*480@60Hz, 25.175 MHz pixel clock
vga640x480at60 :: VGATimings (HzToPeriod 25_175_000) 640 480
vga640x480at60 :: VGATimings (HzToPeriod 25175000) 640 480
vga640x480at60 = 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 (forall (n :: Nat). KnownNat n => SNat n
SNat @16) (forall (n :: Nat). KnownNat n => SNat n
SNat @96) (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 (forall (n :: Nat). KnownNat n => SNat n
SNat @11) (forall (n :: Nat). KnownNat n => SNat n
SNat @2)  (forall (n :: Nat). KnownNat n => SNat n
SNat @31)
    }

-- | VGA 800x600@72Hz, 50 MHz pixel clock
vga800x600at72 :: VGATimings (HzToPeriod 50_000_000) 800 600
vga800x600at72 :: VGATimings (HzToPeriod 50000000) 800 600
vga800x600at72 = 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 (forall (n :: Nat). KnownNat n => SNat n
SNat @56) (forall (n :: Nat). KnownNat n => SNat n
SNat @120) (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 (forall (n :: Nat). KnownNat n => SNat n
SNat @37) (forall (n :: Nat). KnownNat n => SNat n
SNat @6)   (forall (n :: Nat). KnownNat n => SNat n
SNat @23)
    }

-- | VGA 800x600@60Hz, 40 MHz pixel clock
vga800x600at60 :: VGATimings (HzToPeriod 40_000_000) 800 600
vga800x600at60 :: VGATimings (HzToPeriod 40000000) 800 600
vga800x600at60 = 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 (forall (n :: Nat). KnownNat n => SNat n
SNat @40) (forall (n :: Nat). KnownNat n => SNat n
SNat @128) (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 (forall (n :: Nat). KnownNat n => SNat n
SNat @1)  (forall (n :: Nat). KnownNat n => SNat n
SNat @4)   (forall (n :: Nat). KnownNat n => SNat n
SNat @23)
    }

-- | VGA 1024*768@60Hz, 65 MHz pixel clock
vga1024x768at60 :: VGATimings (HzToPeriod 65_000_000) 1024 768
vga1024x768at60 :: VGATimings (HzToPeriod 65000000) 1024 768
vga1024x768at60 = 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 (forall (n :: Nat). KnownNat n => SNat n
SNat @24) (forall (n :: Nat). KnownNat n => SNat n
SNat @136) (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 (forall (n :: Nat). KnownNat n => SNat n
SNat @3)  (forall (n :: Nat). KnownNat n => SNat n
SNat @6)   (forall (n :: Nat). KnownNat n => SNat n
SNat @29)
    }