{-  Copyright 2010 Dominique Devriese

    This file is part of the grammar-combinators library.

    The grammar-combinators library is free software: you can
    redistribute it and/or modify it under the terms of the GNU
    Lesser General Public License as published by the Free
    Software Foundation, either version 3 of the License, or (at
    your option) any later version.

    Foobar is distributed in the hope that it will be useful, but
    WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General
    Public License along with Foobar. If not, see
    <http://www.gnu.org/licenses/>.
-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE RankNTypes #-}

module Text.GrammarCombinators.Test.TestUPT where

import Text.GrammarCombinators.Base
import Text.GrammarCombinators.Parser.RecursiveDescent
import Text.GrammarCombinators.Transform.UnfoldRecursion
import Text.GrammarCombinators.Transform.FoldLoops
import Text.GrammarCombinators.Transform.FilterDies
import Text.GrammarCombinators.Parser.Packrat
import Text.GrammarCombinators.Parser.Parsec
import Text.GrammarCombinators.Utils.PrintGrammar
import Text.GrammarCombinators.Transform.UniformPaull

data SP
data S
data E
data T

data ETNDom ix where
  SP :: ETNDom SP
  S :: ETNDom S
  E :: ETNDom E
  T :: ETNDom T

instance El ETNDom SP where proof = SP
instance El ETNDom S where proof = S
instance El ETNDom E where proof = E
instance El ETNDom T where proof = T

instance FoldFam ETNDom where
  foldFam f n = f SP $ f S $ f E $ f T n

instance ShowFam ETNDom where
  showIdx SP = "SP"
  showIdx S = "S"
  showIdx E = "E"
  showIdx T = "T"

instance EqFam ETNDom where
  overrideIdx f SP v SP = v
  overrideIdx f S v S = v
  overrideIdx f E v E = v
  overrideIdx f T v T = v
  overrideIdx f _ v idx = f idx

instance MemoFam ETNDom where
  data Memo ETNDom v = MemoETNDom (v SP) (v S) (v E) (v T)
  toMemo f = MemoETNDom (f SP) (f S) (f E) (f T)
  fromMemo (MemoETNDom v _ _ _) SP = v 
  fromMemo (MemoETNDom _ v _ _) S = v 
  fromMemo (MemoETNDom _ _ v _) E = v 
  fromMemo (MemoETNDom _ _ _ v) T = v 

instance Domain ETNDom

type PFETN =  I S :>: SP :+:        -- SP -> S #
              I E :>: S :+:         -- S -> E
              (I E :*: I T) :>: E :+: -- E -> E - T
              I T :>: E :+:         -- E -> T
              I E :>: T :+:         -- T -> ( E ) 
              U :>: T                 -- T -> n

type instance PF ETNDom = PFETN

data family ETNCalcV ix
data instance ETNCalcV SP = ETNVSP Int deriving (Show)
data instance ETNCalcV S = ETNVS Int deriving (Show)
data instance ETNCalcV E = ETNVE Int deriving (Show)
data instance ETNCalcV T = ETNVT Int deriving (Show)

unETNVS :: ETNCalcV S -> Int
unETNVS (ETNVS t) = t
unETNVE :: ETNCalcV E -> Int
unETNVE (ETNVE e) = e
unETNVT :: ETNCalcV T -> Int
unETNVT (ETNVT t) = t

calcETN :: Processor ETNDom ETNCalcV
calcETN = calcETN'
calcETN' :: forall ix. ETNDom ix -> PFETN ETNCalcV ix -> ETNCalcV ix
calcETN' SP (L (Tag (I s))) = ETNVSP $ unETNVS s 
calcETN' S (R (L (Tag (I e)))) = ETNVS $ unETNVE e
calcETN' E (R (R (L (Tag (I e :*: I t))))) = ETNVE $ unETNVE e - unETNVT t
calcETN' E (R (R (R (L (Tag (I t)))))) = ETNVE $ unETNVT t
calcETN' T (R (R (R (R (L (Tag (I e))))))) = ETNVT $ unETNVE e
calcETN' T (R (R (R (R (R (Tag U)))))) = ETNVT 1

calcGrammarETN :: ProcessingContextFreeGrammar ETNDom Char ETNCalcV
calcGrammarETN = applyProcessor grammarETN calcETN

grammarETN :: ContextFreeGrammar ETNDom Char
grammarETN SP = epsilon (L . Tag . I) >>>
                ref S >>>* token '#'
grammarETN S = epsilon (R . L . Tag . I) >>> ref E
grammarETN E =   epsilon (\e t -> R $ R $ L $ Tag $ I e :*: I t) >>>
                 ref E >>>* token '-' >>> ref T
             ||| epsilon (R . R . R . L . Tag . I) >>> ref T
grammarETN T =   epsilon (R . R . R . R . L . Tag . I) >>>*
                 token '(' >>> ref E >>>* token ')'
             ||| epsilon (R $ R $ R $ R $ R $ Tag U) >>>*
                 token 'n'

test1 = "(n)-((n-n-n)-n-n)-(n-(n-n-n)-n)#"
testgr :: ProcessingExtendedContextFreeGrammar (UPDomain ETNDom) Char (UPValue ETNCalcV)
testgr = transformUniformPaull calcGrammarETN
testg :: GContextFreeGrammar (FoldLoopsDomain (UPDomain ETNDom)) Char (FoldLoopsValue (UPValue ETNCalcV)) (FoldLoopsResultValue (UPValue ETNCalcV) (UPValue ETNCalcV))
testg = foldLoops testgr
testgp :: ProcessingContextFreeGrammar (FoldLoopsDomain (UPDomain ETNDom)) Char (FoldLoopsValue (UPValue ETNCalcV)) 
testgp = foldAndProcessLoops testgr
testidx :: FoldLoopsDomain (UPDomain ETNDom) (FLBaseIx (UPBaseIx SP))
testidx = FLBase $ UPBase SP
depth = 30
printG = putStr $ printGrammar grammarETN 
printTG = putStr $ printGrammar $ filterDiesE testgr 
prTest1 = parsePackrat testgp testidx test1
rdTest1 = parseRecDec testgp testidx test1
psTest1 = parseParsec testgp testidx "test1" test1