{-# LANGUAGE ExistentialQuantification, GADTs, EmptyDataDecls,
    MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

module Language.Grammars.Grammar where

import Language.AbstractSyntax.TTTAS
import Data.HList

import Control.Applicative
import Unsafe.Coerce


-------------------------------------------
-- GRAMMAR REPRESENTATION
-------------------------------------------

data TL
data FL a


data Grammar a  
  = forall env . Grammar  (Ref a env)  
                          (GramEnv env env)

type GramEnv = Env (Productions TL)

newtype Productions l a env 
  = PS {unPS :: [Prod l a env]}

data Prod l a env where
      Star      ::  Prod l (a->b) env -> Prod l a      env ->  Prod l b  env
      FlipStar  ::  Prod l a      env -> Prod l (a->b) env ->  Prod l b  env
      Sym       ::  Symbol a t env                         ->  Prod l a  env
      Pure      ::  a                                      ->  Prod l a  env

      Fix       ::  Productions (FL a) a env               ->  Prod l      a  env
      Var       ::                                             Prod (FL a) a  env 

-- I tried with HOAS, but it is more restrictive
--      Fix       ::  (forall s. Prod a s -> Productions a s)  -> Prod a env 

type DTerm = String

data TTerm
data TNonT
data TAttT

data Symbol a t env where
  Term    :: String    ->  Symbol  DTerm    TTerm   env

  Nont    :: Ref a env ->  Symbol  a        TNonT   env
  -- attributed terminals
  TermInt   ::             Symbol  Int      TAttT   env
  TermChar  ::             Symbol  Char     TAttT   env
  TermVarid ::             Symbol  String   TAttT   env
  TermConid ::             Symbol  String   TAttT   env
  TermOp    ::             Symbol  String   TAttT   env 
  --- TODO: the rest of EnumValToken


getRefNT :: Symbol a TNonT env -> Ref a env
getRefNT (Nont ref) = ref


pairEq :: Maybe (Equal a b) -> Maybe (Equal (a,t) (b,t))
pairEq (Just Eq) = Just Eq
pairEq Nothing   = Nothing

matchSym  ::  Symbol a t1 env -> Symbol b t2 env 
          ->  Maybe (Equal (a,t1) (b,t2))
matchSym (Nont x)   (Nont y)             = pairEq $ match x y
matchSym (Term x)   (Term y) | x == y    = Just Eq
matchSym TermInt    TermInt              = Just Eq
matchSym TermVarid  TermVarid            = Just Eq
matchSym TermConid  TermConid            = Just Eq
matchSym TermOp     TermOp               = Just Eq
matchSym _          _                    = Nothing


int   ::  Symbol Int     TAttT  env
char  ::  Symbol Char    TAttT  env
var   ::  Symbol String  TAttT  env
con   ::  Symbol String  TAttT  env
op    ::  Symbol String  TAttT  env

int   =  TermInt
char  =  TermChar
var   =  TermVarid
con   =  TermConid
op    =  TermOp


------------------------
-- APPLICATIVE INTERFACE


newtype ListProd l env a = PP { unPP :: [ Prod l a env ] }


prod :: ListProd l env a -> Productions l a env
prod (PP ps) = PS ps

sym  ::  Symbol a  t  env -> ListProd l env a
sym  s = PP [ Sym $ s ]

nt :: Symbol a  TNonT  env -> ListProd l env a
nt s = sym s

ntPrd :: Symbol a  TNonT  env -> ListProd l env a
ntPrd s =  id <$> nt s
 

tr ::  String -> ListProd l env DTerm
tr s = PP [ Sym $ Term s ]


varPrd   ::  ListProd (FL a) env a
varPrd    = PP [ Var ]
fixPrd  ::  ListProd (FL a) env a -> ListProd l env a
fixPrd p  = PP [ (Fix . prod) p ]


instance Functor (ListProd l env) where
 fmap f (PP p) = PP [ Star (Pure f) p' | p' <- p ]

instance Applicative (ListProd l env) where
 pure f = PP [ Pure f ]
 
 (PP f) <*> (PP g) = PP [ Star f' g' | f' <- f, g' <- g ]

instance Alternative (ListProd l env) where
 empty = PP []
 
 (PP f) <|> (PP g) = PP (f ++ g)

 some p = fixPrd (one <|> more)
     where  one  = (:[]) <$> toFL p 
            more = (:)   <$> toFL p <*> varPrd


 many p = fixPrd (none <|> more) 
     where  none = pure [] 
            more = (:)   <$> toFL p <*> varPrd

toFL :: ListProd l env a -> ListProd (FL b) env a
toFL (PP p) = PP $ map prodToFL p

prodToFL :: Prod l a env -> Prod (FL b) a env
prodToFL (Star      f  g)  = Star      (prodToFL f) (prodToFL g)
prodToFL (FlipStar  f  g)  = FlipStar  (prodToFL f) (prodToFL g)
prodToFL (Sym       s)     = Sym s
prodToFL (Pure      a)     = Pure a
prodToFL (Fix       f)     = Fix f
prodToFL Var               = unsafeCoerce Var -- the other option is to add an error here


pSome :: ListProd (FL [a]) env a -> ListProd l env [a]
pSome p = fixPrd (one <|> more)
     where  one  = (:[]) <$> p 
            more = (:)   <$> p <*> varPrd

pMany :: ListProd (FL [a]) env a -> ListProd l env [a]
pMany p = fixPrd (none <|> more)
     where  none = pure [] 
            more = (:)   <$> p <*> varPrd


------------------------
-- IDIOMS

-- | The  `Ii` is to be pronounced as @stop@
data Ii = Ii 

-- | The function `iI` is to be pronounced as @start@
iI ::Idiomatic  l env (a -> a) g => g
iI = idiomatic (pure id)

class Idiomatic l env f g  | g -> f l env  where
    idiomatic :: ListProd l env f -> g

instance  Idiomatic l env x  (Ii -> ListProd l env x) where
    idiomatic ix Ii = ix
instance  Idiomatic l env f g  => Idiomatic  l env (a -> f) (ListProd l env a -> g) where
    idiomatic isf is = idiomatic (isf <*> is)

instance Idiomatic l env f g => Idiomatic l env ((a -> b) -> f)  ((a -> b) -> g) where
    idiomatic isf f = idiomatic (isf <*> (pure f))

instance (Idiomatic  l env f g) 
       => Idiomatic  l env f (String -> g) where
    idiomatic isf str = idiomatic (isf <* (tr str))


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


newtype  LSPair nt a t env = LSPair { symLSPair :: (Symbol a t env) }  

labelLSPair :: LSPair nt a t env -> nt
labelLSPair _ = undefined

infixr 6 ^= 
(^=) :: nt -> Symbol a t env -> LSPair nt a t env
(^=) _ = LSPair

infixr 6 <=>

class LabelSymbol t v v' | t v -> v' where 
 (<=>) :: label -> Symbol v t env -> ListProd l env (LVPair label v')


instance LabelSymbol TAttT v (Record HNil -> v) where
 l <=> v =  (\x -> l .=. (\(Record HNil) -> x)) <$> (PP [ Sym v ])

instance LabelSymbol TNonT v v where
 l <=> v =  (l .=.) <$> (PP [ Sym v ])

instance LabelSymbol TTerm v v where -- only to have all the instances
 l <=> v =  (l .=.) <$> (PP [ Sym v ])



-------------------------------------------------------------------------------
-- Show instances for the Grammars
-- Just for debugging purposes

instance Show (Grammar a) where
 show (Grammar r prods) = show r ++ "\n" ++ show prods

instance ShowEnv (Env (Productions l) env env') => Show (Env (Productions l) env env') where
 show env = showEnv 0 env

class ShowEnv a where
    showEnv :: Int -> a -> String

instance ShowEnv (Env (Productions l) env env') where
    showEnv _ (Empty)         = "\n"
    showEnv n (Ext nts nont)  = show n ++ "->" ++ show nont ++ "\n" ++ showEnv (n+1) nts
 
instance Show (Productions l a env) where
 show (PS prods) = show prods

instance Show (Prod l a env) where
 show (Star pf pa)      = "(" ++ show pf ++ "<*>" ++ show pa ++ ")"
 show (FlipStar pa pf)  = "(" ++ show pa ++ "<**>" ++ show pf  ++ ")"
 show (Sym s)           = show s 
 show (Pure _)          = "pure"
 show (Fix f)           = "fix " ++ show f
 show Var               = "var"

instance Show (Symbol a t env) where
 show (Term s)    = show s
 show (Nont r)    = show r
 show (TermInt)   = "int"
 show (TermChar)  = "char"
 show (TermVarid) = "var"
 show (TermConid) = "con"
 show (TermOp)    = "op"

instance Show (Ref a env) where
 show Zero     = "0"
 show (Suc r)  = show  $ (1::Int) + ((read . show) r)