-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Spine
-- Copyright   :  (c) 2010 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Rewrite:
-- automatic transformation system for point-free programs
-- 
-- Representation of spines for generic programming a la SYB revolutions.
--
-----------------------------------------------------------------------------

module Data.Spine where

import Data.Type
import Data.Pf
import {-# SOURCE #-} Data.Equal

import Data.Monoid hiding (Any)
import Control.Monad.State

import Generics.Pointless.Functors hiding (rep)
import Generics.Pointless.Combinators

-- * A spine representation for data values à la SYB revolutions

data Typed a = Type a :| a

data Spine a where
    As :: a -> Con -> Spine a
    Ap :: Spine (a -> b) -> Typed a -> Spine b

data Fixity = Prefix | Infix deriving Eq

data Con = Con {name :: String, fixity :: Fixity}

scon n = Con {name = show n, fixity = Prefix}
pcon s = Con {name = s, fixity = Prefix}
icon s = Con {name = s, fixity = Infix}

-- | Converting from a spine to a value
fromSpine :: Spine a -> a
fromSpine (c `As` _) = c
fromSpine (Ap f (_ :| a)) = (fromSpine f) a

showlst :: Type a -> [a] -> String
showlst a l = "[" ++ showlst' a l
showlst' :: Type a -> [a] -> String
showlst' a [] = "]"
showlst' a (x:xs) = gshow a x ++ "," ++ showlst' a xs

-- | Converting from a value to a spine
toSpine :: Type a -> a -> Spine a
toSpine TypeRep Any = Any `As` (pcon "Any")
toSpine TypeRep (Var s) = Var s `As` (pcon $ showL ["Var",show s])
toSpine TypeRep (Id a) = Id `As` (pcon "Id")
    `Ap` (TypeRep :| a)
toSpine TypeRep Int = Int `As` (pcon "Int")
toSpine TypeRep Bool = Bool `As` (pcon "Bool")
toSpine TypeRep Char = Char `As` (pcon "Char")
toSpine TypeRep One = One `As` (pcon "One")
toSpine TypeRep (Either a b) = Either `As` (pcon "Either")
    `Ap` (TypeRep :| a)
    `Ap` (TypeRep :| b)
toSpine TypeRep (Prod a b) = Prod `As` (pcon "Prod")
    `Ap` (TypeRep :| a)
    `Ap` (TypeRep :| b)
toSpine TypeRep (Fun a b) = Fun `As` (pcon "Fun")
    `Ap` (TypeRep :| a)
    `Ap` (TypeRep :| b)
toSpine TypeRep (Lns a b) = Lns `As` (pcon "Lns")
    `Ap` (TypeRep :| a)
    `Ap` (TypeRep :| b)
toSpine TypeRep (Data s fctr) = Data s `As` (pcon $ "Data " ++ show s)
    `Ap` (FctrRep :| fctr)
toSpine TypeRep (NewData s fctr) = NewData s `As` (pcon $ "NewData " ++ show s)
    `Ap` (FctrRep :| fctr)
toSpine TypeRep (List a) = List `As` (pcon "List")
    `Ap` (TypeRep :| a)
toSpine TypeRep Dynamic = Dynamic `As` (pcon "Dynamic")
toSpine TypeRep (Pf a) = Pf `As` (pcon "Pf")
    `Ap` (TypeRep :| a)
toSpine TypeRep TP = TP `As` (pcon "TP")
toSpine TypeRep (TU a) = TU `As` (pcon "TU")
    `Ap` (TypeRep :| a)
toSpine FctrRep I = I `As` (pcon "I")
toSpine FctrRep L = L `As` (pcon "L")
toSpine FctrRep (K c) = K `As` (pcon "K")
    `Ap` (TypeRep :| c)
toSpine FctrRep (f :*!: g) = (:*!:) `As` (icon ":*!:")
    `Ap` (FctrRep :| f)
    `Ap` (FctrRep :| g)
toSpine FctrRep (f :+!: g) = (:+!:) `As` (icon ":+!:")
    `Ap` (FctrRep :| f)
    `Ap` (FctrRep :| g)
toSpine FctrRep (f :@!: g) = (:@!:) `As` (icon ":@!:")
    `Ap` (FctrRep :| f)
    `Ap` (FctrRep :| g)
toSpine FctrRep AnyF = AnyF `As` (pcon "AnyF")

toSpine Any x = x `As` (pcon "Any ")
toSpine (Var s) x = x `As` (pcon $ showL ["Var",show s])
toSpine (Id a) x = x `As` (pcon $ showL ["Id",gshow a x])
toSpine Int n = n `As` (scon n)
toSpine Bool n = n `As` (scon n)
toSpine Char n = n `As` (scon n)
toSpine One x = x `As` (pcon "(_L::One)")
toSpine (Either a _) (Left x) = Left `As` (pcon "Left")
    `Ap` (a :| x)
toSpine (Either _ b) (Right y) = Right `As` (pcon "Right")
    `Ap` (b :| y)
toSpine (Prod a b) (x,y) = (,) `As` (icon ",")
    `Ap` (a :| x)
    `Ap` (b :| y)
toSpine (Fun a b) f = f `As` (pcon "Fun")
toSpine (Lns c a) l = l `As` (pcon "Lns")
toSpine (a@(Data s fctr)) v = inn `As` (pcon $ "inn" ++ s)
    `Ap` ((rep fctr a) :| out v)
toSpine (a@(NewData s fctr)) v = inn `As` (pcon $ "Inn" ++ s)
    `Ap` ((rep fctr a) :| out v)
toSpine (List Char) str = str `As` (pcon $ show str)
toSpine (List a) l = l `As` (pcon $ showlst a l)
toSpine Dynamic (Dyn t x) = Dyn t `As` (pcon "Dyn")
    `Ap` (t :| x)
toSpine TP x = x `As` (pcon "TP")
toSpine (TU a) x = x `As` (pcon "TQ")

toSpine (Pf (Fun c b)) (COMPF fctr a f g) = COMPF `As` (pcon "compf")
    `Ap` (FctrRep :| fctr)
    `Ap` (TypeRep :| a)
    `Ap` ((Pf (Fun (rep fctr a) b)) :| f)
    `Ap` ((Pf (Fun c (rep fctr a))) :| g)
toSpine (Pf (Lns c b)) (COMPF_LNS fctr a f g) = COMPF_LNS `As` (pcon "compf_lns")
    `Ap` (FctrRep :| fctr)
    `Ap` (TypeRep :| a)
    `Ap` ((Pf (Lns (rep fctr a) b)) :| f)
    `Ap` ((Pf (Lns c (rep fctr a))) :| g)
toSpine (Pf _) BOT = BOT `As` (pcon "_L")
toSpine (Pf _) TOP = TOP `As` (pcon "T")
toSpine (Pf (Fun _ _)) (FUN s f) = (FUN s f) `As` (pcon s)
toSpine (Pf (Fun a c)) (CONV e@(Left _) f) = CONV e `As` (pcon "lconv")
    `Ap` (Pf (Fun c a) :| f)
toSpine (Pf (Fun a c)) (CONV e@(Right _) f) = CONV e `As` (pcon "rconv")
    `Ap` (Pf (Fun c a) :| f)
toSpine (Pf (Lns a c)) (CONV_LNS e@(Left _) f) = CONV_LNS e `As` (pcon "lconv")
    `Ap` (Pf (Lns c a) :| f)
toSpine (Pf (Lns a c)) (CONV_LNS e@(Right _) f) = CONV_LNS e `As` (pcon "rconv")
    `Ap` (Pf (Lns c a) :| f)
toSpine (Pf (Lns c a)) (LNS s l) = (LNS s l) `As` (pcon s)
toSpine (Pf (Fun a b)) (PROTECT f) = PROTECT `As` (pcon "protect")
    `Ap` (Pf (Fun a b) :| f)
toSpine (Pf (Lns a b)) (PROTECT_LNS f) = PROTECT_LNS `As` (pcon "protect_lns")
    `Ap` (Pf (Lns a b) :| f)
toSpine (Pf _) (VAR s) = VAR s `As` (pcon s)

toSpine (Pf (Fun a b)) (PNT vb) = PNT `As` (pcon "pnt")
    `Ap` (b :| vb)
toSpine (Pf (Fun _ _)) BANG = BANG `As` (pcon "bang")
toSpine (Pf (Fun a c)) (COMP b f g) = COMP `As` (icon ".")
    `Ap` (TypeRep :| b)
    `Ap` (Pf (Fun b c) :| f)
    `Ap` (Pf (Fun a b) :| g)
toSpine (Pf (Fun _ _)) FST = FST `As` (pcon "fst")
toSpine (Pf (Fun _ _)) SND = SND `As` (pcon "snd")
toSpine (Pf (Fun a (Prod b c))) (SPLIT f g) = SPLIT `As` (icon "/\\")
    `Ap` (Pf (Fun a b) :| f)
    `Ap` (Pf (Fun a c) :| g)
toSpine (Pf (Fun (Prod a b) (Prod c d))) (PROD f g) = PROD `As` (icon "><")
    `Ap` (Pf (Fun a c) :| f)
    `Ap` (Pf (Fun b d) :| g)
toSpine (Pf (Fun _ _)) INL = INL `As` (pcon "inl")
toSpine (Pf (Fun _ _)) INR = INR `As` (pcon "inr")
toSpine (Pf (Fun (Either a b) c)) (EITHER f g) = EITHER `As` (icon "\\/")
    `Ap` (Pf (Fun a c) :| f)
    `Ap` (Pf (Fun b c) :| g)
toSpine (Pf (Fun (Either a b) (Either c d))) (SUM f g) = SUM `As` (icon "-|-")
    `Ap` (Pf (Fun a c) :| f)
    `Ap` (Pf (Fun b d) :| g)
toSpine (Pf _) (MKDYN a) = MKDYN `As` (pcon "mkDyn")
    `Ap` (TypeRep :| a)
toSpine (Pf _) (UNDYN a) = UNDYN `As` (pcon "unDyn")
    `Ap` (TypeRep :| a)
toSpine (Pf _) (CAST a) = CAST `As` (pcon "cast")
    `Ap` (TypeRep :| a)

toSpine (Pf func) ZERO = aux func
   where aux :: Monoid y => Type (x -> y) -> Spine (Pf (x -> y))
         aux t@(Fun _ (Data "List" fctr)) = ZERO `As` pcon "nil"
         aux (Fun _ Int) = ZERO `As` pcon "const 0"
         aux _ = ZERO `As` pcon "mempty"
toSpine (Pf func) PLUS = PLUS `As` pcon "mappend"
toSpine (Pf func) (FOLD) = (FOLD `As` pcon "fold")
   
toSpine (Pf (Fun _ _)) ID = ID `As` (pcon "id") 
toSpine (Pf (Fun _ _)) SWAP = SWAP `As` (pcon "swap") 
toSpine (Pf (Fun _ _)) COSWAP = COSWAP `As` (pcon "coswap") 
toSpine (Pf (Fun _ _)) DISTL = DISTL `As` (pcon "distl")
toSpine (Pf (Fun _ _)) UNDISTL = UNDISTL `As` (pcon "undistl")
toSpine (Pf (Fun _ _)) DISTR = DISTR `As` (pcon "distr") 
toSpine (Pf (Fun _ _)) UNDISTR = UNDISTR `As` (pcon "undistr") 
toSpine (Pf (Fun _ _)) ASSOCL = ASSOCL `As` (pcon "assocl") 
toSpine (Pf (Fun _ _)) ASSOCR = ASSOCR `As` (pcon "assocr") 
toSpine (Pf (Fun _ _)) COASSOCL = COASSOCL `As` (pcon "coassocl")
toSpine (Pf (Fun _ _)) COASSOCR = COASSOCR `As` (pcon "coassocr") 

toSpine (Pf (Fun _ (List a))) INN = INN `As` (pcon $ "innList")
toSpine (Pf (Fun (List a) _)) OUT = OUT `As` (pcon $ "outList")
toSpine (Pf (Fun _ a@(dataName -> Just s))) INN = INN `As` (pcon $ "inn" ++ s)
toSpine (Pf (Fun a@(dataName -> Just s) _)) OUT = OUT `As` (pcon $ "out" ++ s)
toSpine (Pf (Fun _ _)) (FMAP fctr (Fun a c) f) = FMAP `As` (pcon "fmap")
    `Ap` (FctrRep :| fctr)
    `Ap` (TypeRep :| Fun a c)
    `Ap` (Pf (Fun a c) :| f)
toSpine (Pf (Fun _ _)) (FZIP fctr t f) = FZIP `As` (pcon "fzip")
    `Ap` (FctrRep :| fctr)
    `Ap` (TypeRep :| t)
    `Ap` (Pf t :| f)
toSpine (Pf (Fun a b@(dataNameFctr -> Just (s,fctr)))) (ANA f) = ANA `As` (pcon $ "ana" ++ s)
    `Ap` (Pf (Fun a (rep fctr a)) :| f)
toSpine (Pf (Fun a@(dataNameFctr -> Just (s,fctr)) b)) (CATA f) = CATA `As` (pcon $ "cata" ++ s)
    `Ap` (Pf (Fun (rep fctr b) b) :| f)
toSpine (Pf (Fun a@(dataNameFctr -> Just (s,fctr)) c)) (PARA f) = PARA `As` (pcon $ "para" ++ s)
    `Ap` (Pf (Fun (rep fctr (Prod c a)) c) :| f)

toSpine (Pf _) WRAP = WRAP `As` (pcon "wrap")
toSpine (Pf (Fun (List a) (List b))) (MAP f) = MAP `As` (pcon "map")
    `Ap` (Pf (Fun a b) :| f)
toSpine (Pf _) LHEAD = LHEAD `As` (pcon "lhead")
toSpine (Pf _) LTAIL = LTAIL `As` (pcon "ltail")
toSpine (Pf _) LENGTH = LENGTH `As` (pcon "length")
toSpine (Pf _) ONE = ONE `As` (pcon "one")

toSpine (Pf (Fun c a)) (GET l) = GET `As` (pcon "get")
    `Ap` (Pf (Lns c a) :| l)
toSpine (Pf (Fun (Prod a c) _)) (PUT l) = PUT `As` (pcon "put")
    `Ap` (Pf (Lns c a) :| l)
toSpine (Pf (Fun a c)) (CREATE l) = CREATE `As` (pcon "create")
    `Ap` (Pf (Lns c a) :| l)

toSpine (Pf (Lns c a)) (COMP_LNS b f g) = COMP_LNS `As` (icon ".< ")
    `Ap` (TypeRep :| b)
    `Ap` (Pf (Lns b a) :| f)
    `Ap` (Pf (Lns c b) :| g)
toSpine (Pf (Lns (Prod a b) _)) (FST_LNS f) = FST_LNS `As` (pcon "fst_lns")
    `Ap` (Pf (Fun a b) :| f)
toSpine (Pf (Lns (Prod a b) _)) (SND_LNS f) = SND_LNS `As` (pcon "snd_lns")
    `Ap` (Pf (Fun b a) :| f)
toSpine (Pf (Lns (Prod c d) (Prod a b))) (PROD_LNS f g) = PROD_LNS `As` (icon "><<")
    `Ap` (Pf (Lns c a) :| f)
    `Ap` (Pf (Lns d b) :| g)
toSpine (Pf (Lns (Either a b) c)) (EITHER_LNS x f g) = EITHER_LNS `As` (icon "\\/<")
    `Ap` (Pf (Fun c (Either One One)) :| x)
    `Ap` (Pf (Lns a c) :| f)
    `Ap` (Pf (Lns b c) :| g)
toSpine (Pf (Lns (Either c d) (Either a b))) (SUM_LNS f g) = SUM_LNS `As` (icon "-|-<")
    `Ap` (Pf (Lns c a) :| f)
    `Ap` (Pf (Lns d b) :| g)
toSpine (Pf (Lns (Either c d) (Either a b))) (SUMW_LNS x y f g) = SUMW_LNS `As` (pcon "sum_lns")
    `Ap` (Pf (Fun (Prod a d) c) :| x)
    `Ap` (Pf (Fun (Prod b c) d) :| y)
    `Ap` (Pf (Lns c a) :| f)
    `Ap` (Pf (Lns d b) :| g)
toSpine (Pf (Lns c One)) (BANG_LNS f) = BANG_LNS `As` (pcon "(!<)")
    `Ap` (Pf (Fun One c) :| f)
toSpine (Pf (Lns c (Prod One _))) (BANGL_LNS) = BANGL_LNS `As` (pcon "bangl")
toSpine (Pf (Lns c (Prod _ One))) (BANGR_LNS) = BANGR_LNS `As` (pcon "bangr")

toSpine (Pf (Lns _ _)) ID_LNS = ID_LNS `As` (pcon "id_lns")
toSpine (Pf (Lns _ _)) SWAP_LNS = SWAP_LNS `As` (pcon "swap_lns")
toSpine (Pf (Lns _ _)) COSWAP_LNS = COSWAP_LNS `As` (pcon "coswap_lns")
toSpine (Pf (Lns _ _)) DISTL_LNS = DISTL_LNS `As` (pcon "distl_lns")
toSpine (Pf (Lns _ _)) UNDISTL_LNS = UNDISTL_LNS `As` (pcon "undistl_lns")
toSpine (Pf (Lns _ _)) DISTR_LNS = DISTR_LNS `As` (pcon "distr_lns")
toSpine (Pf (Lns _ _)) UNDISTR_LNS = UNDISTR_LNS `As` (pcon "undistr_lns")
toSpine (Pf (Lns _ _)) ASSOCL_LNS = ASSOCL_LNS `As` (pcon "assocl_lns")
toSpine (Pf (Lns _ _)) ASSOCR_LNS = ASSOCR_LNS `As` (pcon "assocr_lns")
toSpine (Pf (Lns _ _)) COASSOCL_LNS = COASSOCL_LNS `As` (pcon "coassocl_lns")
toSpine (Pf (Lns _ _)) COASSOCR_LNS = COASSOCR_LNS `As` (pcon "coassocr_lns")

toSpine (Pf (Lns _ a@(dataName -> Just s))) INN_LNS = INN_LNS `As` (pcon $ "inn" ++ s ++ "_lns")
toSpine (Pf (Lns a@(dataName -> Just s) _)) OUT_LNS = OUT_LNS `As` (pcon $ "out" ++ s ++ "_lns")
toSpine (Pf (Lns _ _)) (FMAP_LNS fctr (Fun c a) (f)) = FMAP_LNS `As` (pcon "fmap_lns")
    `Ap` (FctrRep :| fctr)
    `Ap` (TypeRep :| Fun c a)
    `Ap` (Pf (Lns c a) :| f)
toSpine (Pf (Lns a b@(dataNameFctr -> Just (s,fctr)))) (ANA_LNS f) = ANA_LNS `As` (pcon $ "ana" ++ s ++ "_lns")
    `Ap` (Pf (Lns a (rep fctr a)) :| f)
toSpine (Pf (Lns a@(dataNameFctr -> Just (s,fctr)) b)) (CATA_LNS f) = CATA_LNS `As` (pcon $ "cata" ++ s ++ "_lns")
    `Ap` (Pf (Lns (rep fctr b) b) :| f)
toSpine (Pf (Lns (List a) (List b))) (MAP_LNS f) = MAP_LNS `As` (pcon "map_lns")
    `Ap` (Pf (Lns a b) :| f)
toSpine (Pf (Lns (List a) _)) (LENGTH_LNS v) = LENGTH_LNS `As` (pcon "length_lns")
    `Ap` (a :| v)
toSpine (Pf (Lns _ _)) FILTER_LEFT_LNS = FILTER_LEFT_LNS `As` (pcon "filter_left_lns")
toSpine (Pf (Lns _ _)) FILTER_RIGHT_LNS = FILTER_RIGHT_LNS `As` (pcon "filter_right_lns")
toSpine (Pf (Lns _ _)) CAT_LNS = CAT_LNS `As` (pcon "cat_lns")
toSpine (Pf (Lns _ _)) CONCAT_LNS = CONCAT_LNS `As` (pcon "concat_lns")
toSpine (Pf (Lns _ _)) SUMN_LNS = SUMN_LNS `As` (pcon "sumn_lns")
toSpine (Pf (Lns _ _)) PLUSN_LNS = PLUSN_LNS `As` (pcon "plus_lns")

toSpine (Pf _) (APPLY t f) = APPLY `As` (pcon "apT")
    `Ap` (TypeRep :| t)
    `Ap` (Pf TP :| f)
toSpine (Pf _) (MKT t f) = MKT `As` (pcon "mkT")
    `Ap` (TypeRep :| t)
    `Ap` (Pf (Fun t t) :| f)
toSpine (Pf _) NOP = NOP `As` pcon "nop"
toSpine (Pf _) (SEQ f g) = (SEQ `As` pcon "seq")
    `Ap` (Pf TP :| f)
    `Ap` (Pf TP :| g)
toSpine (Pf _) (EXTT f t g)  = EXTT `As` (pcon "extT")
    `Ap` (Pf TP :| f)
    `Ap` (TypeRep :| t)
    `Ap` (Pf (Fun t t) :| g)
toSpine (Pf _) (ALL f) = (ALL `As` pcon "gmapT") `Ap` (Pf TP :| f)
toSpine (Pf _) (EVERYWHERE f) = (EVERYWHERE `As` pcon "everywhere") `Ap` (Pf TP :| f)
toSpine (Pf _) (EVERYWHERE' f) = (EVERYWHERE' `As` pcon "everywhere'") `Ap` (Pf TP :| f)

toSpine (Pf (Fun _ r)) (APPLYQ t f) = APPLYQ `As` (pcon "apQ")
    `Ap` (TypeRep :| t)
    `Ap` (Pf (TU r) :| f)
toSpine (Pf (TU r)) (MKQ t f) = MKQ `As` (pcon "mkQ")
    `Ap` (TypeRep :| t)
    `Ap` (Pf (Fun t r) :| f)
toSpine (Pf _) EMPTYQ = EMPTYQ `As` pcon "emptyQ"
toSpine (Pf r) (UNION f g) = (UNION `As` icon "`union`") `Ap` (Pf r :| f) `Ap` (Pf r :| g)
toSpine (Pf (TU r)) (EXTQ f t g) = EXTQ `As` (pcon "extQ")
    `Ap` (Pf (TU r) :| f)
    `Ap` (TypeRep :| t)
    `Ap` (Pf (Fun t r) :| g)
toSpine (Pf r) (GMAPQ f) = (GMAPQ `As` pcon "gmapQ") `Ap` (Pf r :| f)
toSpine (Pf r) (EVERYTHING f) = (EVERYTHING `As` pcon "everything") `Ap` (Pf r :| f)

toSpine (Pf r) SELF = SELF `As` pcon "self"
toSpine (Pf r) ATT = ATT `As` pcon "att"
toSpine (Pf r) CHILD = CHILD `As` pcon "child"
toSpine (Pf r) ATTRIBUTE = ATTRIBUTE `As` pcon "attribute"
toSpine (Pf r) DESCENDANT = DESCENDANT `As` pcon "desc"
toSpine (Pf r) DESCSELF = DESCSELF `As` pcon "descself"
toSpine (Pf r) (NAME s) = NAME s `As` (pcon $ showL["name",show s])
toSpine (Pf r) (f :/: g) = (:/:) `As` (icon "/")
    `Ap` (Pf (TU (List Dynamic)) :| f)
    `Ap` (Pf r :| g)
toSpine (Pf (TU s)) (SEQQ (q :: Pf (Q r)) f) = let r = typeof::Type r in (SEQQ `As` pcon "seqQ") `Ap` (Pf (TU r) :| q) `Ap` (Pf (Fun r s) :| f)
toSpine (Pf _) (f :?: p) =  (((:?:) `As` Con {name="?", fixity=Infix}) `Ap` (Pf (TU (List Dynamic)) :| f)) `Ap` (Pf (TU Bool) :| p)
toSpine (Pf _) NONEMPTY = NONEMPTY `As` Con {name = "nonempty", fixity = Prefix}
toSpine (Pf (TU (Prod a b))) (f :/\: g) = (((:/\:) `As` Con {name ="/\\", fixity=Infix}) `Ap` (Pf (TU a) :| f)) `Ap` (Pf (TU b) :| g)

toSpine (Pf (Fun Any Any)) e = e `As` (pcon "<anyfunc>")
toSpine (Pf (Lns Any Any)) e = e `As` (pcon "<anylens>")

toSpine (Pf t) f = error $ "toSpine undefined for " ++ show t
toSpine TypeRep t = error $ "toSpine TypeRep"

instance Show (Type a) where
    show Any = "Any"
    show (Var s) = showL["Var",show s]
    show (Id x) = showL ["Id",show x]
    show Int = "Int"
    show Bool = "Bool"
    show Char = "Char"
    show One = "One"
    show (Either x y) = showL ["Either",show x,show y]
    show (Prod x y) = showL ["Prod",show x,show y]
    show (Fun x y) = showL ["Fun",show x,show y]
    show (Lns x y) = showL ["Lns",show x,show y]
    show (List a) = "[" ++ show a ++ "]"
    show (Data s f) = s
    show (NewData s f) = s

    show (Pf a) = showL ["Pf",show a]
    show (Dynamic) = "Dynamic"
    show TP = "TP"
    show (TU a) = showL ["TU",show a]

showData :: Type a -> String
showData (Data s fctr) = s ++ " = " ++ show fctr
showData (NewData s fctr) = "New" ++ s ++ " = " ++ show fctr
  
instance Show Dynamic where
    show (Dyn t v) = showL ["Dynamic",gshow t v]

instance Show DynType where
    show (DynT t) = showL ["DynT",show t]

instance Show DynFctr where
    show (DynF f) = showL ["DynF",show f]

instance Show (Fctr f) where
  show I = "Id"
  show (K t) = showL ["K",show t]
  show L = "L"
  show (f:*!:g) = showL [show f,":*:",show g]
  show (f:+!:g) = showL [show f,":+:",show g]
  show (f:@!:g) = showL [show f,":@:",show g]
  show AnyF = "AnyF"

instance Typeable a => Show (Pf a) where
    show = gshow typeof

gshow :: Type a -> a -> String
gshow (isNat -> Just Eq) (Nat n) = showL ["Nat",show n]
gshow Dynamic (Dyn t x) = gshow t x
gshow (Pf t) f@(COMP _ _ _) = "(" ++ showComp (Pf t) f ++ ")"
gshow (Pf t) f@(COMP_LNS _ _ _) = "(" ++ showComp (Pf t) f ++ ")"
gshow t x = showSpine (toSpine t x)
   where showSpine :: Spine a -> String
         showSpine (Ap f@(Ap (_ `As` c) (a :| x)) (b :| y))
            | fixity c == Infix = showL [gshow a x,name c,gshow b y]
				| otherwise = showL [showSpine f,gshow b y]
         showSpine (_ `As` c) = name c
         showSpine (Ap f (t :| a)) = showL [showSpine f,gshow t a]

showComp :: Type a -> a -> String
showComp (Pf (Fun a c)) (COMP b f g) = showComp (Pf $ Fun b c) f ++ " . " ++ showComp (Pf $ Fun a b) g
showComp (Pf (Lns a c)) (COMP_LNS b f g) = showComp (Pf $ Lns b c) f ++ " .< " ++ showComp (Pf $ Lns a b) g
showComp t f = gshow t f