{-# LANGUAGE GADTs
           , TypeFamilies
           , TypeOperators
           , KindSignatures
           , MultiParamTypeClasses
           , EmptyDataDecls
           , FlexibleInstances
           #-}

{- Example by Sjoerd Visscher -}
module XMLRep where

import Generics.MultiRec.Elems.Many

data Node n v = Elt n [Attrs n v] [Node n v] | Text v deriving Show
data Attrs n v = Attr n v deriving Show

data XML :: (* -> *) -> * -> * -> * where
  Node     :: XML (n :|: v :|: Nil) (Node n v)     Zero
  Attrs    :: XML (n :|: v :|: Nil) (Attrs n v)    (Suc Zero)
  NodeList :: XML (n :|: v :|: Nil) [Node n v] (Suc (Suc Zero))
  AttrList :: XML (n :|: v :|: Nil) [Attrs n v] (Suc (Suc (Suc Zero)))
    
data Elt
instance Constructor Elt where
  conName _ = "Elt"

data Text
instance Constructor Text where
  conName _ = "Text"

data Attr
instance Constructor Attr where
  conName _ = "Attr"

type instance PF XML =
      (    C Elt (I (Elem Zero) :*: I (Rec (Suc (Suc (Suc Zero)))) :*: I (Rec (Suc (Suc Zero))))
       :+: C Text (I (Elem (Suc Zero))) 
      ) :>: Zero
  :+: (    C Attr (I (Elem Zero) :*: I (Elem (Suc Zero)))
      ) :>: (Suc Zero)
  :+: (    U 
       :+: (I (Rec Zero) :*: I (Rec (Suc (Suc Zero))))
      ) :>: (Suc (Suc Zero))
  :+: (    U 
       :+: (I (Rec (Suc Zero)) :*: I (Rec (Suc (Suc (Suc Zero)))))
      ) :>: (Suc (Suc (Suc Zero)))

instance Fam XML (n :|: v :|: Nil) where
  from Node (Elt n as ns) = L (Tag (L (C (I (CL (Z n)) :*: I (CR (R0 AttrList as)) :*: I (CR (R0 NodeList ns))))))
  from Node (Text v)      = L (Tag (R (C (I (CL (S (Z v)))))))
  from Attrs (Attr n v)   = R (L (Tag (C (I (CL (Z n)) :*: I (CL (S (Z v)))))))
  from NodeList []        = R (R (L (Tag (L U))))
  from NodeList (n:ns)    = R (R (L (Tag (R (I (CR (R0 Node n)) :*: I (CR (R0 NodeList ns)))))))
  from AttrList []        = R (R (R (Tag (L U))))
  from AttrList (a:as)    = R (R (R (Tag (R (I (CR (R0 Attrs a)) :*: I (CR (R0 AttrList as)))))))
  to Node (L (Tag (L (C (I (CL (Z n)) :*: I (CR (R0 AttrList as)) :*: I (CR (R0 NodeList ns))))))) = Elt n as ns
  to Node (L (Tag (R (C (I (CL (S (Z v))))))))                                                     = Text v
  to Attrs (R (L (Tag (C (I (CL (Z n)) :*: I (CL (S (Z v))))))))                                   = Attr n v
  to NodeList (R (R (L (Tag (L U)))))                                                              = []
  to NodeList (R (R (L (Tag (R (I (CR (R0 Node n)) :*: I (CR (R0 NodeList ns))))))))               = n:ns
  to AttrList (R (R (R (Tag (L U)))))                                                              = []
  to AttrList (R (R (R (Tag (R (I (CR (R0 Attrs a)) :*: I (CR (R0 AttrList as))))))))              = a:as
  

instance El (Proof (XML (n :|: v :|: Nil))) Zero                   where proof = Proof Node
instance El (Proof (XML (n :|: v :|: Nil))) (Suc Zero)             where proof = Proof Attrs
instance El (Proof (XML (n :|: v :|: Nil))) (Suc (Suc Zero))       where proof = Proof NodeList
instance El (Proof (XML (n :|: v :|: Nil))) (Suc (Suc (Suc Zero))) where proof = Proof AttrList

instance EqS (Proof (XML (n :|: v :|: Nil))) where
    eqS (Proof Node)     (Proof Node)     = Just Refl
    eqS (Proof Attrs)    (Proof Attrs)    = Just Refl
    eqS (Proof NodeList) (Proof NodeList) = Just Refl
    eqS (Proof AttrList) (Proof AttrList) = Just Refl
    eqS _                _                = Nothing

instance EqS2 (XML (n :|: v :|: Nil)) where
    eqS2 Node     Node     = Just (Refl, Refl)
    eqS2 Attrs    Attrs    = Just (Refl, Refl)
    eqS2 NodeList NodeList = Just (Refl, Refl)
    eqS2 AttrList AttrList = Just (Refl, Refl)
    eqS2 _        _        = Nothing