-- vim: expandtab: ts=2: sw=2: autoindent:
module Type where

import Data.SparseBIT
import Monad
import Test.QuickCheck

data Type = Ts [Type] | Bool | Nat | Color | Maybe Type | List Type
  deriving (Eq,Show)

instance Expand Type where
  t *. u  | null (expand t)  = u
          | null (expand u)  = t
          | otherwise        = Ts [t,u]

  unit = Ts []

  expand (Ts [])      =   []
  expand (Ts (x:xs))  =   case expand x of
                            [] -> expand (Ts xs)
                            ts -> [foldr (*.) unit (t:xs) | t <- ts]
  expand Bool         =   [unit,unit]
  expand Nat          =   [unit,Nat]
  expand Color        =   [unit,unit,unit]
  expand (Maybe a)    =   [unit,a]
  expand (List a)     =   [unit,a *. List a]

instance Arbitrary Type where
  arbitrary = tygen

{-
instance CoArbitrary Type where
  coarbitrary (Ts ts)    = variant 0 . coarbitrary ts
  coarbitrary Bool       = variant 1
  coarbitrary Nat        = variant 2
  coarbitrary Color      = variant 3
  coarbitrary (Maybe t)  = variant 4 . coarbitrary t
  coarbitrary (List t)   = variant 5 . coarbitrary t
-}
tygen = sized tygen'

tygen' 0        = oneof $ map return [Bool,Nat,Color,Ts []]
tygen' n | n>0  = oneof [liftM Ts ts, liftM Maybe t, liftM List t]
                where
                  ts  =  liftM2 (:) t $ liftM2 (:) t $
                         resize (n `div` 3) arbitrary
                  t   =  tygen' (n `div` 3)






f         = Bs [I unit, O unit] Bool
t         = Bs [O unit, I unit] Bool
n         = \a -> Bs [I unit, O a] (Maybe a)
j x       = Bs [O unit, x] (Maybe (typeof x))
z         = Bs [I unit, O Nat] Nat
s x       = Bs [O unit, x] Nat
nil       = \a -> Bs [I unit, O (List a)] (List a)
cons x y  = Bs [O unit, x .** y] (List (typeof x))
wc        = \a -> I a

r         = Bs [I unit, O unit, O unit] Color
g         = Bs [O unit, I unit, O unit] Color
b         = Bs [O unit, O unit, I unit] Color

b1 = n (Nat *. List Bool)
b2 = j (wc Nat         .** nil Bool)
b3 = j (z              .** wc (List Bool))
b4 = j (s z            .** cons f (wc (List Bool)))
b5 = j (s (wc Nat)     .** cons t (wc (List Bool)))
b6 = j (s (s (wc Nat)) .** cons f (wc (List Bool)))

p1 = f .** f .** f
p2 = f .** f .** t
p3 = f .** t .** f -- 2nd t
p4 = f .** t .** t -- 2nd t
p5 = t .** f .** f
p6 = t .** f .** t
p7 = t .** t .** f -- 2nd t
p8 = t .** t .** t -- 2nd t
p9 = wc Bool .** f .** wc Bool