{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE EmptyDataDecls        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE FlexibleInstances     #-}

module Tests where

import Test.QuickCheck
import Data.List (group, sort)

import Generics.MultiRec.Base
import Generics.MultiRec.Constructor

import AST

import IndexEq
import ConNames
import GArbitrary
import GSize

-- | The data type Logic is the abstract syntax for the domain
--   of logic expressions.
data Logic = Nor Logic Logic -- Nor
           | T               -- true
           | F               -- false
  deriving (Show, Eq, Ord)

data LAST :: * -> * where
  Logic :: LAST Logic

data Nor
instance Constructor Nor  where conName _ = "Nor"
data T
instance Constructor T    where conName _ = "T"
data F
instance Constructor F    where conName _ = "F"

type instance PF LAST = 
   (  C Nor (I Logic :*: I Logic) 
  :+: C T   (K ())                
  :+: C F   (K ())                
   )
  
instance Ix LAST Logic where

  from_ (Nor l r)  = (L     (C (I (I0 l) :*: I (I0 r))))
  from_ T          = (R (L  (C (K ()))))
  from_ F          = (R (R  (C (K ()))))

  to_ ((L    (C (I (I0 l) :*: I (I0 r)))))   = (Nor l r)
  to_ ((R (L (C (K ())))))                   = T
  to_ ((R (R (C (K ())))))                   = F
  
  index = Logic
  
----------------------------------------------------------------------------

data Choice = A1 | A2 | A3 | A4
  deriving (Show, Eq, Ord)

data CAST :: * -> * where
  Choice :: CAST Choice

data A1
instance Constructor A1  where conName _ = "A1"
data A2
instance Constructor A2  where conName _ = "A2"
data A3
instance Constructor A3  where conName _ = "A3"
data A4
instance Constructor A4  where conName _ = "A4"

type instance PF CAST = 
   (  C A1   (K ())
  :+: C A2   (K ())
  :+: C A3   (K ())
  :+: C A4   (K ())
   )
  
instance Ix CAST Choice where

  from_ A1 = (L       (C (K ())))
  from_ A2 = (R (L    (C (K ()))))
  from_ A3 = (R (R (L (C (K ())))))
  from_ A4 = (R (R (R (C (K ())))))

  to_ (L       (C (K ())))   = A1
  to_ (R (L    (C (K ()))))  = A2
  to_ (R (R (L (C (K ()))))) = A3
  to_ (R (R (R (C (K ()))))) = A4
  
  index = Choice

----------------------------------------------------------------------------
-- Testing ConNames

realConNames :: forall s ix . (Ix s ix, ConNames (PF s)) => s ix -> [String]
realConNames s = conNames (undefined :: PF s s I0 ix)

testConNamesLogic  = realConNames (undefined :: LAST Logic)
testConNamesExpr   = realConNames (undefined :: AST Expr)
testConNamesChoice = realConNames (undefined :: CAST Choice)

----------------------------------------------------------------------------
-- Testing Arbitrary

logicFrequenceTable = [("Nor",1),("T",3),("F",3)]

testLogic :: Gen Logic
testLogic = (garbitrary :: LAST Logic -> FrequencyTable -> Gen Logic) undefined logicFrequenceTable

exprFrequenceTable = [("Const",10)
                     ,("Add",5)
                     ,("Mul",5)
                     ,("EVar",10)
                     ,("Let",5)
                     ,(":=",5)
                     ,("Seq",1)
                     ]

testExpr :: Gen Expr 
testExpr = (garbitrary :: AST Expr -> FrequencyTable -> Gen Expr) Expr exprFrequenceTable

choiceFrequenceTable = [("A1",3),("A2",4),("A3",1),("A4",2)]

testChoice :: IO [(Choice, Int)]
testChoice = fmap (\[a,b,c,d] -> [(A1,a),(A2,b),(A3,c),(A4,d)]) .
             fmap (map length . group . sort . concat) .
             sequence . take 909 . repeat $
             sample' (garbitrary Choice choiceFrequenceTable)

instance GArbitrary (K Var) AST where
    harbitrary ft ix r = return . oneof . map (return . K . V) $ ["x", "y", "z"]

----------------------------------------------------------------------------
-- Testing size

example = Let (V "x" := Mul (Const 6) (Const 9))
              (Add (EVar (V "x")) (EVar (V "y")))

testSize = gsize Expr example

instance GSize (K Var) where
    hsize ix x f = one

----------------------------------------------------------------------------
-- Testing sizedArbitrary

four = Succ $ Succ $ Succ $ Succ $ Zero

ten = Succ $ Succ $ Succ $ Succ $ Succ $ Succ $ Succ $ Succ $ Succ $ Succ $ Zero

testSizedExpr = (sizedArbitrary :: AST Expr -> Nat -> FrequencyTable -> Gen Expr) Expr ten exprFrequenceTable

-----------------------------------------------------------------------------

instance Eq_ LAST where
  eq_ Logic Logic = Just Refl

instance Eq_ AST where
  eq_ Expr Expr  =  Just Refl
  eq_ Decl Decl  =  Just Refl
  eq_ Var Var    =  Just Refl
  eq_ _ _        =  Nothing