Eight.idr

module Main

import Derive.Eq
import Derive.Prelude
import Data.Refined

%language ElabReflection
%default total

public export
data Color = R | G | Y | B
%runElab derive "Color" [Show,Eq,Ord]

public export
data Value = V1 | V2 | V3 | V4
%runElab derive "Value" [Show,Eq,Ord]

public export
data Card : Type where
  J : Color -> Card -- Joker
  C : Color -> Value -> Card
 -- C2 : Card

public export
record Game where
  constructor GM
  top : Card 

data Valid : (top, next : Card) -> Type where
  VJ  : Valid t        (J c)
  VJC : Valid (J c)    (C c v)
  VCC : Valid (C c v1) (C c v2)
  VCV : Valid (C c1 v) (C c2 v)

play : (g : Game) -> (c : Card) -> (0 prf : Valid g.top c) -> Game
play g c prf = GM c

validGame : Game
validGame = play (GM (C R V1)) (C R V2) VCC


-- An illegal move: top is C R V1, next is C G V2,
-- but there is no proof of type Valid (C R V1) (C G V2)
--badGame : Game
--badGame = play (GM (C R V1)) (C G V2) VCC


main : IO ()
main = putStrLn "Hello from Idris2!"