{-# LANGUAGE ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses
  , DeriveGeneric, DeriveAnyClass, TypeFamilies, FlexibleContexts
  , StandaloneDeriving, OverloadedStrings, DeriveDataTypeable #-}
{-|
  Module      : Text.ANTLR.Grammar
  Description : Grammar data types and API for parsing algorithms
  Copyright   : (c) Karl Cronburg, 2018
  License     : BSD3
  Maintainer  : karl@cs.tufts.edu
  Stability   : experimental
  Portability : POSIX

-}
module Text.ANTLR.Grammar
  ( -- * Data types
    Grammar(..)
  , ProdElem(..), ProdElems
  , Production(..), ProdRHS(..), StateFncn(..)
  , Predicate(..), Mutator(..), Ref(..)
  -- * Basic setter / getter functions:
  , getRHS, getLHS, getDataType
  , isSem, isAction
  , sameNTs, sameTs
  , isNT, isT, isEps, getNTs, getTs, getEps
  , prodsFor, getProds
  , validGrammar, hasAllNonTerms, hasAllTerms, startIsNonTerm
  , symbols, defaultGrammar
  ) where
import Prelude hiding (pi)
import Data.List (nub, sort)

import System.IO.Unsafe (unsafePerformIO)
import qualified Debug.Trace as D
import Data.Data (Data(..), Typeable(..))
import Language.Haskell.TH.Lift (Lift(..))

import qualified Text.ANTLR.Set as S
import Text.ANTLR.Set
  ( Set(..), empty, fromList, member, union
  , Hashable(..), Generic(..)
  )

import Text.ANTLR.Pretty

uPIO :: IO a -> a
uPIO = unsafePerformIO

----------------------------------------------------------------
-- When we *Show* production elements, they should contain source location
-- information, but when we *compare* them, we should ignore the source info.

-- | Something is "Ref" if it can be symbolized by some symbol in a set of
--   symbols. Symbols are typically Strings, an enum data type, or some other
--   Eq-able (best if finite) set of things.
class Ref v where
  -- | One symbol type for every value type v.
  type Sym v :: *
  -- | Compute (or extract) the symbol for some concrete value.
  getSymbol :: v -> Sym v

compareSymbols :: (Ref ref, Eq (Sym ref)) => ref -> ref -> Bool
compareSymbols a b = getSymbol a == getSymbol b

-- | Nonterminals can be symbolized (for now the types are equivalent, i.e.
--   nt == Sym nt)
sameNTs :: forall nt. (Ref nt, Eq (Sym nt)) => nt -> nt -> Bool
sameNTs = compareSymbols

-- | Terminals can be symbolized (in the current implementation, the input
--   terminal type to a parser is @(t == 'Text.ANTLR.Lex.Tokenizer.Token' n v)@ and the terminal symbol type is
--   @(ts == 'Sym t' == n)@ where @n@ is defined as the name of a token @('Text.ANTLR.Lex.Tokenizer.Token' n v)@.
sameTs :: forall t. (Ref t, Eq (Sym t)) => t -> t -> Bool
sameTs = compareSymbols

instance Ref String where
  type Sym String = String
  getSymbol = id

instance Ref (String, b) where
  type Sym (String, b) = String
  getSymbol = fst

-- | Grammar ProdElems
--   
--   > nts == Non Terminal Symbol (type)
--   > ts == Terminal Symbol (type)
--
--   Production elements are only used in the grammar data structure and parser,
--   therefore these types (nt and ts) are __not__ necessarily equivalent to the
--   terminal types seen by the tokenizer (nonterminals are special because no one
--   sees them until after parsing). Also pushing @(ts = Sym t)@ up to the top of
--   data constructors gets rid of a lot of unnecessary standalone deriving
--   instances. Standalone deriving instances in this case are a programming
--   anti-pattern for allowing you to improperly parametrize your types. In this
--   case a 'ProdElem' cares about the __terminal symbol type__, not the __terminal
--   token type__. In fact it's redundant to say *terminal token* because all
--   tokens are terminals in the grammar. A token is by definition a tokenized
--   __value__ with a __named__ terminal symbol, which is in fact exactly what the
--   'Text.ANTLR.Lex.Tokenizer.Token' type looks like in 'Text.ANTLR.Lex.Tokenizer': @'Text.ANTLR.Lex.Tokenizer.Token' n v@ (name and
--   value). So wherever I see an @n@ type variable in the tokenizer, this is
--   equivalent to @('Sym' t)@ in the parser. And wherever I see a @('Text.ANTLR.Lex.Tokenizer.Token' n v)@ in the
--   tokenizer, this gets passed into the parser as @t@:
--
--   @
--     n           == 'Sym' t
--     ('Text.ANTLR.Lex.Tokenizer.Token' n v) == t
--   @
--
data ProdElem nts ts =
    NT nts -- ^ Nonterminal production element
  | T  ts  -- ^ Terminal production element
  | Eps    -- ^ Empty string production element
  deriving (Eq, Ord, Generic, Hashable, Show, Data, Lift)

instance (Prettify nts, Prettify ts) => Prettify (ProdElem nts ts) where
  prettify (NT nts) = prettify nts
  prettify (T  ts)  = prettify  ts
  prettify Eps      = pStr "ε"

-- | Is the 'ProdElem' a nonterminal?
isNT (NT _) = True
isNT _      = False

-- | Is the 'ProdElem' a terminal?
isT (T _) = True
isT _     = False

-- | Is the 'ProdElem' an epsilon?
isEps Eps = True
isEps _   = False

-- | Get just the nonterminals from a list
getNTs = map (\(NT nt) -> nt) . filter isNT
-- | Get just the terminals from a list
getTs  = map (\(T t) -> t) . filter isT
-- | Get just the epsilons from a list (umm...)
getEps = map (\Eps -> Eps) . filter isEps

-- | Zero or more production elements
type ProdElems nts ts = [ProdElem nts ts]

-- | A function to run when a production rule fires, operating some state @s@.
data StateFncn s =
    Pass                    -- ^ No predicate or mutator
  | Sem    (Predicate ())   -- ^ Semantic predicate
  | Action (Mutator ())     -- ^ Mutator, ProdElems is always empty in this one
  deriving (Eq, Ord, Generic, Hashable, Show, Data, Lift)

instance Prettify (StateFncn s) where
  prettify Pass       = return ()
  prettify (Sem p)    = prettify p
  prettify (Action a) = prettify a

-- | Right-hand side of a single production rule
data ProdRHS s nts ts = Prod (StateFncn s) (ProdElems nts ts)
  deriving (Eq, Ord, Generic, Hashable, Show, Data, Lift)

instance (Prettify s, Prettify nts, Prettify ts) => Prettify (ProdRHS s nts ts) where
  prettify (Prod sf ps) = do
    prettify sf
    prettify ps

-- | Is this 'ProdRHS' a semantic predicate?
isSem (Prod (Sem _) _) = True
isSem _ = False

-- | Is this 'ProdRHS' a mutator?
isAction (Prod (Action _) _) = True
isAction _ = False

-- | Get just the production elements from a bunch of production rules
getProds = map (\(Prod _ ss) -> ss)

-- | A single production rule with some datatype dt annotating what gets produced when this production rule fires.
data Production s nts ts dt = Production nts (ProdRHS s nts ts) (Maybe dt)
  deriving (Eq, Ord, Generic, Hashable, Data, Lift)

instance (Prettify s, Prettify nts, Prettify ts, Prettify dt) => Prettify (Production s nts ts dt) where
  prettify (Production nts (Prod sf ps) dt) = do
    len <- pCount nts
    -- Put the indentation level after the nonterminal, or just incr by 2 if
    -- lazy...
    incrIndent (len + 4)
    pStr " -> "
    prettify sf
    prettify ps
    prettify dt
    incrIndent (-4)

instance (Show s, Show nts, Show ts, Show dt) => Show (Production s nts ts dt) where
  show (Production nts rhs dt) = show nts ++ " -> " ++ show rhs ++ " (" ++ show dt ++ ")"

-- | Inline get 'ProdRHS' of a 'Production'
getRHS :: Production s nts ts dt -> ProdRHS s nts ts
getRHS (Production lhs rhs dt) = rhs

-- | Inline get the nonterminal symbol naming a 'Production'
getLHS :: Production s nts ts dt -> nts
getLHS (Production lhs rhs dt) = lhs

getDataType :: Production s nts t dt -> Maybe dt
getDataType (Production lhs rhs dt) = dt

-- | Get only the productions for the given nonterminal symbol nts:
prodsFor :: forall s nts ts dt. (Eq nts) => Grammar s nts ts dt -> nts -> [Production s nts ts dt]
prodsFor g nts = let
    matchesNT :: Production s nts t dt -> Bool
    matchesNT (Production nts' _ _) = nts' == nts
  in filter matchesNT (ps g)

-- TODO: boiler plate auto deriving for "named" of a user defined type?

-- | Predicates and Mutators act over some state. The String
--   identifiers should eventually correspond to source-level
--   e.g. location / allocation site information, i.e. two
--   predicates or mutators are equivalent iff they were
--   constructed from the same production rule.
data Predicate p = Predicate String p
  deriving (Data)

instance (Data s, Typeable s) => Lift (Predicate s)
instance (Data s, Typeable s) => Lift (Mutator s)

instance Eq (Predicate s) where
  Predicate p1 _ == Predicate p2 _ = p1 == p2

instance Ord (Predicate s) where
  Predicate p1 _ `compare` Predicate p2 _ = p1 `compare` p2

instance Show (Predicate s) where
  show (Predicate p1 _) = "π(" ++ show p1 ++ ")"

instance Hashable (Predicate s) where
  hashWithSalt salt (Predicate p1 _) = salt `hashWithSalt` p1

instance Prettify (Predicate s) where
  prettify (Predicate n _) = pStr' n

instance Prettify (Mutator s) where
  prettify (Mutator n _) = pStr' n

-- | Function for mutating the state of the parser when a certain
--   production rule fires.
data Mutator   s = Mutator String ()
  deriving (Data)

instance Eq (Mutator s) where
  Mutator m1 _ == Mutator m2 _ = m1 == m2

instance Ord (Mutator s) where
  Mutator m1 _ `compare` Mutator m2 _ = m1 `compare` m2

instance Show (Mutator s) where
  show (Mutator m1 _) = "µ(" ++ show m1 ++ ")"

instance Hashable (Mutator s) where
  hashWithSalt salt (Mutator m1 _) = salt `hashWithSalt` m1

-- | Core representation of a grammar, as used by the parsing algorithms.
data Grammar s nts ts dt = G
  { ns  :: Set nts
  , ts  :: Set ts
  , ps  :: [Production s nts ts dt]
  , s0  :: nts
  , _πs :: Set (Predicate s)
  , _μs :: Set (Mutator   s)
  } deriving (Show, Lift)

instance (Eq s, Eq nts, Eq ts, Eq dt, Hashable nts, Hashable ts, Prettify s, Prettify nts, Prettify ts)
  => Eq (Grammar s nts ts dt) where
  g1 == g2 = ns g1 == ns g2
          && ts g1 == ts g2
          && eqLists (nub $ ps g1) (nub $ ps g2)
          && s0 g1 == s0 g2
          && _πs g1 == _πs g2
          && _μs g1 == _μs g2

eqLists [] [] = True
eqLists [] vs = False
eqLists vs [] = False
eqLists (v1:vs) vs2 = eqLists vs (filter (/= v1) vs2)

instance (Prettify s, Prettify nts, Prettify ts, Prettify dt, Hashable ts, Eq ts, Hashable nts, Eq nts, Ord ts, Ord nts, Ord dt)
  => Prettify (Grammar s nts ts dt) where
  prettify G {ns = ns, ts = ts, ps = ps, s0 = s0, _πs = _πs, _μs = _μs} = do
    pLine "Grammar:"
    pStr "{ "
    incrIndent 2
    pStr  "  ns = "      ; prettify ns; pLine ""
    pStr  ", ts = "      ; prettify ts; pLine ""
    pStr  ", ps = "      ; pListLines $ sort ps; pLine ""
    pStr  ", s0 = "      ; prettify s0; pLine ""
    pStr  ", _πs = "     ; prettify _πs ; pLine ""
    pStr  ", _μs = "     ; prettify _μs ; pLine ""
    incrIndent (-2)
    pStr "}"

-- | All possible production elements of a given grammar.
symbols
  :: (Ord nts, Ord ts, Hashable s, Hashable nts, Hashable ts)
  => Grammar s nts ts dt -> Set (ProdElem nts ts)
symbols g = S.insert Eps $ S.map NT (ns g) `union` S.map T (ts g)

-- | The empty grammar - accepts nothing, with one starting nonterminal
--   and nowhere to go.
defaultGrammar
  :: forall s nts ts dt. (Ord ts, Hashable ts, Hashable nts, Eq nts)
  => nts -> Grammar s nts ts dt
defaultGrammar start = G
  { ns  = S.singleton start
  , ts  = empty
  , ps  = []
  , _πs = empty
  , _μs = empty
  , s0  = start
  }

-- | Does the given grammar make any sense?
validGrammar
  :: forall s nts ts dt.
  (Eq nts, Ord nts, Eq ts, Ord ts, Hashable nts, Hashable ts)
  => Grammar s nts ts dt -> Bool
validGrammar g =
     hasAllNonTerms g
  && hasAllTerms g
  && startIsNonTerm g
--  && distinctTermsNonTerms g

-- | All nonterminals in production rules can be found in the nonterminals list.
hasAllNonTerms
  :: (Eq nts, Ord nts, Hashable nts, Hashable ts)
  => Grammar s nts ts dt -> Bool
hasAllNonTerms g =
  ns g == (fromList . getNTs . concat . getProds . map getRHS $ ps g)

-- | All terminals in production rules can be found in the terminal list.
hasAllTerms
  :: (Eq ts, Ord ts, Hashable nts, Hashable ts)
  => Grammar s nts ts dt -> Bool
hasAllTerms g =
  ts g == (fromList . getTs . concat . getProds . map getRHS $ ps g)

-- | The starting symbol is a valid nonterminal.
startIsNonTerm
  :: (Ord nts, Hashable nts)
  => Grammar s nts ts dt -> Bool
startIsNonTerm g = s0 g `member` ns g

--distinctTermsNonTerms g =
--  (ns g `intersection` ts g) == empty