{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
{-# OPTIONS -fallow-overlapping-instances #-}

import Data.Generics
import Control.Monad.Reader
import Data.Maybe
import Data.Tree


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

-- Terms with typed variables

class Term ( t :: ( * -> * ) -> * -> * ) ( h :: * -> * ) ( a :: * )

-- t ... the term constructor
-- h ... the type constructor for variable spots
-- a ... the type of the term


-- Spots-- either values or maybies or maybe references or ...

data Spot h a = Spot (h a)
instance Term Spot h a


-- Integer constants

data IntC (h :: * -> *) a = IntC Int
instance Term IntC v Int


-- Pairs

data Pair tx ty ax ay ( h :: * -> * ) a = Pair (tx h ax) (ty h ay)
instance (Term tx v ax, Term ty v ay) => Term (Pair tx ty ax ay) v (ax,ay)


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

-- Typeable and Data instances

spotTc :: TyCon
spotTc =  mkTyCon "Spot"

instance Typeable1 h => Typeable1 (Spot h)
 where
  typeOf1 _ = mkTyConApp spotTc [ typeOf1 (undefined :: h ()) ]

spotCon  :: Constr
spotCon  =  mkConstr spotType "Spot" [] Prefix
spotType :: DataType
spotType =  mkDataType "Spot" [spotCon]

instance (Data (h a), Typeable1 h, Data a) => Data (Spot h a)
 where
   dataCast1 f = gcast1 f -- THIS IS CRUCIAL!
   toConstr _ = spotCon
   dataTypeOf _ = spotType
   gfoldl k z (Spot x) = z Spot `k` x
   gunfold k z con =
      case constrIndex con of
        1 -> k (z Spot)

intCTc :: TyCon
intCTc =  mkTyCon "IntC"

instance Typeable1 h => Typeable1 (IntC h)
 where
  typeOf1 _ = mkTyConApp intCTc [ typeOf1 (undefined :: h ()) ]

intCCon  :: Constr
intCCon  =  mkConstr intCType "IntC" [] Prefix
intCType :: DataType
intCType =  mkDataType "IntC" [intCCon]

instance (Data (h a), Typeable1 h, Data a) => Data (IntC h a)
 where
   dataCast1 f = gcast1 f
   toConstr _ = intCCon
   dataTypeOf _ = intCType
   gfoldl k z (IntC x) = z IntC `k` x
   gunfold k z con =
      case constrIndex con of
        1 -> k (z IntC)

pairTc :: TyCon
pairTc =  mkTyCon "Pair"

instance Typeable1 h => Typeable1 (Pair tx ty ax ay h)
 where
  typeOf1 _ = mkTyConApp intCTc [ typeOf1 (undefined :: h ()) ]

pairCon  :: Constr
pairCon  =  mkConstr pairType "Pair" [] Prefix
pairType :: DataType
pairType =  mkDataType "Pair" [pairCon]

instance ( Data (h a)
         , Typeable1 h
         , Data a
         , Data (tx h ax)
         , Data (ty h ay)
         , Typeable1 (Pair tx ty ax ay h)
         )
           => Data (Pair tx ty ax ay h a)
 where
   dataCast1 f = gcast1 f
   toConstr _ = pairCon
   dataTypeOf _ = pairType
   gfoldl k z (Pair x y) = z Pair `k` x `k` y
   gunfold k z con =
      case constrIndex con of
        1 -> k (k (z Pair))


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

-- The Id type constructor

newtype Id x = Id x deriving (Typeable, Data)


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

-- An operation replacing Maybies by Ids

force :: ( Data (t Maybe a)
         , Data (t Id a)
         , Term t Maybe a
         , Term t Id a
         ) => t Maybe a -> t Id a
force = fromJust . tree2data . data2tree


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

-- Special trealisation of Data

data2tree :: Data a => a -> Tree Constr
data2tree = gdefault `ext1Q` atSpot
  where
    atSpot (Spot (Just x)) = data2tree (Spot (Id x))
    gdefault x = Node (toConstr x) (gmapQ data2tree x)


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

-- Trivial de-trealization to Data

tree2data :: Data a => Tree Constr -> Maybe a
tree2data = gdefault
  where
    gdefault (Node con ts) = kids $ fromConstr con
      where
        kids x = snd (gmapAccumM perkid ts x)
        perkid ts = const (tail ts, tree2data (head ts)) 


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

-- Our type checker for terms; perhaps use GADTs if you like

assureTerm :: Term t v a => t v a -> t v a
assureTerm = id


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

-- Sample terms

t1 = assureTerm (Spot (Just (1 :: Int))) :: Spot Maybe Int
t2 = assureTerm (IntC 1 :: IntC Maybe Int)
t3 = assureTerm (Pair t1 t2) :: Pair Spot IntC Int Int Maybe (Int, Int)


-- Test run

main = do
           putStrLn $ gshow t1
           putStrLn $ gshow t2
           putStrLn $ gshow t3
           putStrLn $ gshow (force t1)
           putStrLn $ gshow (force t2)
           putStrLn $ gshow (force t3)