Combinations.idr

data Alignment
  = LeftAligned
  | CenterAligned
  | RightAligned

data FontLevel
  = DisplayTitle
  | BodyText

data Variant
  = Plain
  | Highlighted
  | Inverse

data Swatch
  = PrimaryColor
  | SecondaryColor

data InteractiveState
  = Regular
  | Hovered
  | Pressed
  | Disabled

data ValidBackground : Swatch -> InteractiveState -> Type where
  PrimaryRegular : (swatch : Swatch) ->
                   {auto isPrimaryColor : swatch=PrimaryColor} ->
                   (interactiveState : InteractiveState) ->
                   {auto isRegular : interactiveState=Regular} ->
                   ValidBackground PrimaryColor Regular

data ValidShape : Type where
  ValidBackgroundShape : {a : Swatch} -> {b : InteractiveState} -> ValidShape

data Shape : Type where
  BackgroundShape : (swatch : Swatch) ->
                    (interactiveState : InteractiveState) ->
                    {auto validBackground : ValidBackground swatch interactiveState} ->
                    Shape
--
-- validShapes : Shape a -> a

notPrimaryHovered : ValidBackground PrimaryColor Hovered -> Void
notPrimaryHovered (PrimaryRegular _ _) impossible

notPrimaryPressed : ValidBackground PrimaryColor Pressed -> Void
notPrimaryPressed (PrimaryRegular _ _) impossible

notPrimaryDisabled : ValidBackground PrimaryColor Disabled -> Void
notPrimaryDisabled (PrimaryRegular _ _) impossible

noSecondary : ValidBackground SecondaryColor interactiveState -> Void
noSecondary (PrimaryRegular _ _) impossible

validBackground : (swatch : Swatch) ->
                  (interactiveState : InteractiveState) ->
                  Dec (ValidBackground swatch interactiveState)
validBackground PrimaryColor Regular = Yes (PrimaryRegular PrimaryColor Regular)
validBackground PrimaryColor Hovered = No notPrimaryHovered
validBackground PrimaryColor Pressed = No notPrimaryPressed
validBackground PrimaryColor Disabled = No notPrimaryDisabled
validBackground SecondaryColor interactiveState = No noSecondary

background : (swatch : Swatch) ->
             (interactiveState : InteractiveState) ->
             Shape
background swatch interactiveState with (validBackground swatch interactiveState)
  background PrimaryColor Regular | (Yes (PrimaryRegular x y)) = BackgroundShape PrimaryColor Regular
  background swatch interactiveState | (No contra) = ?background_rhs_rhs_2