{-# OPTIONS -fglasgow-exts #-}

module Types where

import Control.Applicative
import Test.QuickCheck

import Representations
import Base
import GFixpoints hiding (Tree, Leaf, Node)

-- PFView instance for the list data type.

instance PFView [a] where
  type PF [a] = Sum Unit (Prod (K a) Id)

  from []       = Inl Unit
  from (x : xs) = Inr (Prod (K x) (Id (xs)))

  to (Inl Unit)                = []
  to (Inr (Prod (K x) (Id r))) = x : r

-- Tree data type definition.

data Tree a = Leaf | Branch a (Tree a) (Tree a)
  deriving (Show, Eq, Ord)

-- PFView instance for the tree data type.

instance PFView (Tree a) where
  type PF (Tree a) = Sum (Prod (K a) (Prod Id Id)) Unit

  to (Inr Unit)                              = Leaf
  to (Inl (Prod (K a) (Prod (Id l) (Id r)))) = Branch a (l) (r)

  from Leaf           = Inr Unit
  from (Branch a l r) = Inl $ Prod (K a) $ Prod (Id l) (Id r)

-- PFView instance for the cardinal direction data type.

data Direction a =
    North
  | NorthEast
  | East
  | SouthEast
  | South
  | SouthWest
  | West
  | NorthWest
--  | Test (Direction a)
  deriving (Eq, Show, Ord)

instance PFView (Direction a) where
  type PF (Direction a) =
--    Sum Unit (Sum Unit (Sum Unit (Sum Unit (Sum Unit (Sum Unit (Sum Unit (Sum Unit Id)))))))
    Sum Unit (Sum Unit (Sum Unit (Sum Unit (Sum Unit (Sum Unit (Sum Unit Unit))))))

  to (Inl Unit) = North     
  to (Inr (Inl Unit)) = NorthEast
  to (Inr (Inr (Inl Unit))) = East
  to (Inr (Inr (Inr (Inl Unit)))) = SouthEast
  to (Inr (Inr (Inr (Inr (Inl Unit))))) = South
  to (Inr (Inr (Inr (Inr (Inr (Inl Unit)))))) = SouthWest
  to (Inr (Inr (Inr (Inr (Inr (Inr (Inl Unit))))))) = West
  to (Inr (Inr (Inr (Inr (Inr (Inr (Inr Unit))))))) = NorthWest
--  to (In (Inr (Inr (Inr (Inr (Inr (Inr (Inr (Inr (Id a)))))))))) = Test (to a)

  from North     = Inl Unit
  from NorthEast = Inr (Inl Unit)
  from East      = Inr (Inr (Inl Unit))
  from SouthEast = Inr (Inr (Inr (Inl Unit)))
  from South     = Inr (Inr (Inr (Inr (Inl Unit))))
  from SouthWest = Inr (Inr (Inr (Inr (Inr (Inl Unit)))))
  from West      = Inr (Inr (Inr (Inr (Inr (Inr (Inl Unit))))))
  from NorthWest = Inr (Inr (Inr (Inr (Inr (Inr (Inr Unit))))))
--  from (Test a)  = In (Inr (Inr (Inr (Inr (Inr (Inr (Inr (Inr (Id (from a))))))))))

-- PFView instance for the recursive identity.

data R a = R (R a)
  deriving (Show, Eq, Ord)

instance PFView (R a) where
  type PF (R a) = Id

  to (Id a) = R a
  from (R a)     = Id (a)

-- balanced to the left
data A = A A | B A | C
 deriving (Show, Eq, Ord)
instance PFView A where
  type PF A = Sum Unit (Sum Id Id)

  to (Inr (Inl (Id x))) = A (x)
  to (Inr (Inr (Id x))) = B (x)
  to (Inl Unit)       = C
  from (A x) = (Inr (Inl (Id x)))
  from (B x) = (Inr (Inr (Id x)))
  from C = (Inl Unit)