IndexedGames.idr

module IndexedGames

import Data.List
import Data.Vect
import Data.Nat

infixr 6 >>>>
infixr 6 >>>
infixr 5 &&&&
infixr 5 &&&
infixl 5 \\
infixl 5 //

interface Optic o where
  lens   : (s -> a) -> (s -> b -> t) -> o s t a b
  (>>>>) : o s t a b -> o a b p q -> o s t p q
  (&&&&) : o s1 t1 a1 b1 -> o s2 t2 a2 b2 -> o (s1, s2) (t1, t2) (a1, a2) (b1, b2)
  (++++) : o s1 t a1 b -> o s2 t a2 b -> o (Either s1 s2) t (Either a1 a2) b

-- The `List` data type in Haskell
data TypeList : (ts : List Type) -> Type where
  Nil : TypeList []
  (::) : t -> TypeList ts -> TypeList (t :: ts)

-- Concatenation on TypeList
(++) : TypeList xs -> TypeList ys -> TypeList (xs ++ ys)
(++) [] y = y
(++) (x :: z) y = x :: (z ++ y)

record OpenGame (o, c : Type -> Type -> Type -> Type -> Type)
                (a, b : List Type)
                (x, s, y, r : Type) where
  constructor MkGame
  play : TypeList a -> o x s y r
  eval : TypeList a -> c x s y r -> TypeList b

-- How to split a type list into two TypeList, I think its `UnAppend` in haskell
split : {xs, ys : _} -> TypeList (xs ++ ys) -> (TypeList xs, TypeList ys)
split {xs = []} x = ([], x)
split {xs = (x'::xs)} (x :: ys) =
  let (xs', ys') = split ys in (x :: xs', ys')

-- How to merge two typelists I think it's `:++:` in Haskell
combine : TypeList xs -> TypeList ys -> TypeList (xs ++ ys)
combine [] y = y
combine (x :: z) y = x :: combine z y

interface (Optic o) => Context c o where
  cmap : o s1 t1 s2 t2 -> o a1 b1 a2 b2 -> c s1 t1 a2 b2 -> c s2 t2 a1 b1
  (//) : o s1 t1 a1 b1 -> c (s1, s2) (t1, t2) (a1, a2) (b1, b2) -> c s2 t2 a2 b2
  (\\) : o s2 t2 a2 b2 -> c (s1, s2) (t1, t2) (a1, a2) (b1, b2) -> c s1 t1 a1 b1

identity : Optic o => o s t s t
identity = lens id (flip const)

(>>>) : {a, b, a', b' : List Type} ->
        Optic o => (ctx : Context c o) =>
        OpenGame o c a b x s y r ->
        OpenGame o c a' b' y r z q ->
        OpenGame o c (a ++ a') (b ++ b') x s z q
(>>>) (MkGame p1 e1) (MkGame p2 e2) =
  MkGame
      (\args => let (x1, x2) = split args in p1 x1 >>>> p2 x2)
      (\args, body => let (x1, x2) = split args in combine (e1 x1 (cmap @{ctx} identity (p2 x2) body))
                                                           (e2 x2 (cmap (p1 x1) identity body)))

(&&&) : Optic o => (ctx : Context c o) =>
        {a, a', b, b' : List Type} ->
        OpenGame o c a b x s y r ->
        OpenGame o c a' b' x' s' y' r' ->
        OpenGame o c (a ++ a') (b ++ b') (x, x') (s, s') (y, y') (r, r')
(&&&) (MkGame p1 e1) (MkGame p2 e2) = MkGame
    (\args => let (x1, x2) = split args in p1 x1 &&&& p2 x2)
    (\args, body =>
        let (x1, x2) = split args in
            combine (e1 x1 ((\\) @{ctx} (p2 x2) body))
                    (e2 x2 ((//) @{ctx} (p1 x1) body)))

-- Given a number `n` repeat the type list `n` times
0
CatRepeat : Nat -> List Type -> List Type
CatRepeat Z ls = []
CatRepeat (S n) ls = ls ++ CatRepeat n ls

-- How to map optics
omap : Optic o =>
                  (s -> s') ->
                  (x' -> x) ->
                  (y -> y') ->
                  (r' -> r) ->
                  o x s y r -> o x' s' y' r'
omap g g1 g2 g3 optic =
  let post : o y r y' r' = lens g2 (const g3)
      pre : o x' s' x s = lens g1 (const g) in
      pre >>>> (optic >>>> post)

-- How to map games
gmap : Optic o => (ctx : Context c o) =>
       (s -> s') ->
       (x' -> x) ->
       (y -> y') ->
       (r' -> r) ->
       OpenGame o c a b x s y r ->
       OpenGame o c a b x' s' y' r'
gmap f1 f2 f3 f4 (MkGame p e) =
      MkGame (\t => omap f1 f2 f3 f4 (p t))
             (\t, b => e t (cmap @{ctx}(lens f2 (\_ => f1)) (lens f3 (\_ => f4)) b))
-- The optic `o x s y r` is isomorphic to the optic `o [x] [s] [y] [r]`
pureVectIso : Optic o => o x s y r -> o (Vect 1 x) (Vect 1 s) (Vect 1 y) (Vect 1 r)
pureVectIso = omap pure head pure head

-- Chop the head of a vector and return it alons with the tail
chop : Vect (S n) a -> (a, Vect n a)
chop (x :: xs) = (x, xs)

-- Recouple the separated head to the tail
couple : (a, Vect n a) -> Vect (S n) a
couple (x, y) = x :: y

-- Couple a game contains heads with a game containing tails
gameSucc : Optic o =>
           o x s y r ->
           o (Vect (len) x) (Vect (len) s) (Vect (len) y) (Vect (len) r) ->
           o (Vect ((S len)) x) (Vect ((S len)) s) (Vect ((S len)) y) (Vect ((S len)) r)
gameSucc optic opticSucc =
  omap couple chop couple chop (optic &&&& opticSucc)

-- The population operator works on a list of games containing at least one game.
-- It merges this of games into a single game with the boundaries correcly matched
-- with `CatRepeat`
0
population : (opt : Optic o) => (ctx : Context c o) => {n : Nat} ->
             Vect (S n) (OpenGame o c a b x s y r) ->
             OpenGame o c (CatRepeat (S n) a) (CatRepeat (S n) b)
                 (Vect (S n) x) (Vect (S n) s) (Vect (S n) y) (Vect (S n) r)
population [game] =
  let g' : OpenGame o c a b (Vect 1 x) (Vect 1 s) (Vect 1 y) (Vect 1 r)
         = gmap pure Vect.head pure Vect.head game
      in rewrite appendNilRightNeutral a in
         rewrite appendNilRightNeutral b in g'

population (g1 :: g2 :: gs) =
  let rec@(MkGame rPlay rEval)= population (g2 :: gs) in
      MkGame
         (\x =>
               let (x1, x2) = split x
                   playedRec = play rec x2
                   played = play g1 x1
               in
                   gameSucc played playedRec)
         (\x, body =>
           let (x1, x2) = split x
               g' = gmap couple chop couple chop (g1 &&& rec)
               gs = gameSucc @{opt} (play g1 x1) (play rec x2)
            in eval g' x body
         )