{-# LANGUAGE AllowAmbiguousTypes     #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}

module Language.Parser.Ptera.Syntax.SafeGrammar (
    T,

    Grammar (..),
    TokensTag,
    RulesTag,
    RuleExprType,
    GrammarToken (..),
    fixGrammar,

    StartPoint,
    Terminal,
    NonTerminal,
    HasRuleExprField (..),
    MemberInitials (..),
    Rules (..),
    genStartPoint,

    RuleExpr (..),
    Alt (..),
    Expr (..),
    ruleExpr,
    (<^>),
    (<:>),
    eps,
    var,
    varA,
    tok,
    TokensMember (..),
    tokA,
) where

import           Language.Parser.Ptera.Prelude

import qualified Data.HashMap.Strict                  as HashMap
import qualified Language.Parser.Ptera.Data.HEnum     as HEnum
import qualified Language.Parser.Ptera.Data.HFList    as HFList
import qualified Language.Parser.Ptera.Syntax.Grammar as SyntaxGrammar
import           Prelude                              (String)
import qualified Type.Membership                      as Membership


type T = Grammar

type Grammar
    :: ([Type] -> Type -> Type) -> Type -> Type -> Type -> [Symbol]
    -> Type
newtype Grammar action rules tokens elem initials = UnsafeGrammar
    {
        forall (action :: [*] -> * -> *) rules tokens elem
       (initials :: [Symbol]).
Grammar action rules tokens elem initials
-> FixedGrammar
     StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action
unsafeGrammar :: SyntaxGrammar.FixedGrammar
            StartPoint
            NonTerminal
            Terminal
            elem
            StringLit
            (Maybe ())
            action
    }

type family TokensTag (tokens :: Type) :: [Symbol]
type family RulesTag (rules :: Type) :: [Symbol]
type family RuleExprType (rules :: Type) :: Type -> Type

class GrammarToken tokens elem where
    tokenToTerminal :: Proxy tokens -> elem -> HEnum.T (TokensTag tokens)

class KnownSymbol v => HasRuleExprField rules v where
    type RuleExprReturnType rules v :: Type

    getExprField :: rules -> proxy v -> RuleExprType rules (RuleExprReturnType rules v)

    nonTerminalName :: rules -> proxy v -> String
    nonTerminalName rules
_ proxy v
p = forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> StringLit
symbolVal proxy v
p

type GrammarMForFixGrammar elem action = SyntaxGrammar.GrammarT
    StartPoint
    NonTerminal
    Terminal
    elem
    StringLit
    (Maybe ())
    action
    Identity

fixGrammar
    :: forall initials action rules tokens elem
    .  MemberInitials rules initials
    => Rules rules => RuleExprType rules ~ RuleExpr action rules tokens elem
    => rules -> Grammar action rules tokens elem initials
fixGrammar :: forall (initials :: [Symbol]) (action :: [*] -> * -> *) rules
       tokens elem.
(MemberInitials rules initials, Rules rules,
 RuleExprType rules ~ RuleExpr action rules tokens elem) =>
rules -> Grammar action rules tokens elem initials
fixGrammar rules
ruleDefs = forall (action :: [*] -> * -> *) rules tokens elem
       (initials :: [Symbol]).
FixedGrammar
  StartPoint StartPoint StartPoint elem StringLit (Maybe ()) action
-> Grammar action rules tokens elem initials
UnsafeGrammar do
    forall a. Identity a -> a
runIdentity do
        forall {k1} {k2} (m :: * -> *) start nonTerminal terminal
       (elem :: k1) varDoc altDoc (action :: [k1] -> k2 -> *).
Monad m =>
GrammarT start nonTerminal terminal elem varDoc altDoc action m ()
-> m (FixedGrammar
        start nonTerminal terminal elem varDoc altDoc action)
SyntaxGrammar.fixGrammarT do
            forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]).
Applicative m =>
HFList f xs
-> (forall (x :: k). Membership xs x -> f x -> m ()) -> m ()
HFList.hforMWithIndex
                forall rules (initials :: [Symbol]).
MemberInitials rules initials =>
T (DictF (HasRuleExprField rules)) initials
memberInitials
                forall (v :: Symbol).
Membership initials v
-> DictF (HasRuleExprField rules) v
-> GrammarT
     StartPoint
     StartPoint
     StartPoint
     elem
     StringLit
     (Maybe ())
     action
     Identity
     ()
fixInitial
            forall {k} (m :: * -> *) (f :: k -> *) (xs :: [k]).
Applicative m =>
HFList f xs
-> (forall (x :: k). Membership xs x -> f x -> m ()) -> m ()
HFList.hforMWithIndex
                forall rules.
Rules rules =>
T (DictF (HasRuleExprField rules)) (RulesTag rules)
generateRules
                forall (v :: Symbol).
Membership (RulesTag rules) v
-> DictF (HasRuleExprField rules) v
-> GrammarT
     StartPoint
     StartPoint
     StartPoint
     elem
     StringLit
     (Maybe ())
     action
     Identity
     ()
fixRule
    where
        fixInitial
            :: Membership.Membership initials v
            -> HFList.DictF (HasRuleExprField rules) v
            -> GrammarMForFixGrammar elem action ()
        fixInitial :: forall (v :: Symbol).
Membership initials v
-> DictF (HasRuleExprField rules) v
-> GrammarT
     StartPoint
     StartPoint
     StartPoint
     elem
     StringLit
     (Maybe ())
     action
     Identity
     ()
fixInitial Membership initials v
m DictF (HasRuleExprField rules) v
HFList.DictF = do
            let sn :: StartPoint
sn = forall {k} (initials :: [k]) (v :: k).
Membership initials v -> StartPoint
genStartPoint Membership initials v
m
            let vn :: StartPoint
vn = StringLit -> StartPoint
getNewV do forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> StringLit
symbolVal Membership initials v
m
            forall {k1} {k2} start (m :: * -> *) nonTerminal terminal
       (elem :: k1) varDoc altDoc (action :: [k1] -> k2 -> *).
(Enum start, Monad m) =>
start
-> nonTerminal
-> GrammarT
     start nonTerminal terminal elem varDoc altDoc action m ()
SyntaxGrammar.initialT StartPoint
sn StartPoint
vn

        fixRule
            :: forall v
            .  Membership.Membership (RulesTag rules) v
            -> HFList.DictF (HasRuleExprField rules) v
            -> GrammarMForFixGrammar elem action ()
        fixRule :: forall (v :: Symbol).
Membership (RulesTag rules) v
-> DictF (HasRuleExprField rules) v
-> GrammarT
     StartPoint
     StartPoint
     StartPoint
     elem
     StringLit
     (Maybe ())
     action
     Identity
     ()
fixRule Membership (RulesTag rules) v
m DictF (HasRuleExprField rules) v
HFList.DictF = do
            let vn :: StartPoint
vn = StringLit -> StartPoint
getNewV do forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> StringLit
symbolVal Membership (RulesTag rules) v
m
            let d :: StringLit
d = forall rules (v :: Symbol) (proxy :: Symbol -> *).
HasRuleExprField rules v =>
rules -> proxy v -> StringLit
nonTerminalName rules
ruleDefs Membership (RulesTag rules) v
m
            forall {k1} {k2} nonTerminal (m :: * -> *) varDoc terminal
       (elem :: k1) altDoc (action :: [k1] -> k2 -> *) start.
(Enum nonTerminal, Monad m) =>
nonTerminal
-> varDoc
-> RuleExpr nonTerminal terminal elem altDoc action
-> GrammarT
     start nonTerminal terminal elem varDoc altDoc action m ()
SyntaxGrammar.ruleT StartPoint
vn StringLit
d do
                forall a.
RuleExpr action rules tokens elem a
-> RuleExpr StartPoint StartPoint elem (Maybe ()) action
fixRuleExpr do forall rules (v :: Symbol) (proxy :: Symbol -> *).
HasRuleExprField rules v =>
rules -> proxy v -> RuleExprType rules (RuleExprReturnType rules v)
getExprField rules
ruleDefs Membership (RulesTag rules) v
m

        fixRuleExpr :: RuleExpr action rules tokens elem a
            -> SyntaxGrammar.RuleExpr NonTerminal Terminal elem (Maybe ()) action
        fixRuleExpr :: forall a.
RuleExpr action rules tokens elem a
-> RuleExpr StartPoint StartPoint elem (Maybe ()) action
fixRuleExpr = \case
            RuleExpr [Alt action rules tokens elem a]
alts -> forall {k} {k1} nonTerminal terminal (elem :: k) altDoc
       (action :: [k] -> k1 -> *) (a :: k1).
[Alt nonTerminal terminal elem altDoc action a]
-> RuleExpr nonTerminal terminal elem altDoc action
SyntaxGrammar.RuleExpr
                [ forall a.
Alt action rules tokens elem a
-> Alt StartPoint StartPoint elem (Maybe ()) action a
fixAlt Alt action rules tokens elem a
origAlt | Alt action rules tokens elem a
origAlt <- [Alt action rules tokens elem a]
alts ]

        fixAlt :: Alt action rules tokens elem a
            -> SyntaxGrammar.Alt NonTerminal Terminal elem (Maybe ()) action a
        fixAlt :: forall a.
Alt action rules tokens elem a
-> Alt StartPoint StartPoint elem (Maybe ()) action a
fixAlt (UnsafeAlt Alt StringLit StartPoint elem (Maybe ()) action a
origAlt) = case Alt StringLit StartPoint elem (Maybe ()) action a
origAlt of
            SyntaxGrammar.Alt Expr StringLit StartPoint elem us
e Maybe ()
h action us a
act -> forall {k} {k1} nonTerminal terminal (elem :: k) (us :: [k]) altDoc
       (action :: [k] -> k1 -> *) (a :: k1).
Expr nonTerminal terminal elem us
-> altDoc
-> action us a
-> Alt nonTerminal terminal elem altDoc action a
SyntaxGrammar.Alt
                do forall (us :: [*]).
Expr StringLit StartPoint elem us
-> Expr StartPoint StartPoint elem us
fixExpr Expr StringLit StartPoint elem us
e
                do Maybe ()
h
                do action us a
act

        fixExpr :: SyntaxGrammar.Expr IntermNonTerminal Terminal elem us
            -> SyntaxGrammar.Expr NonTerminal Terminal elem us
        fixExpr :: forall (us :: [*]).
Expr StringLit StartPoint elem us
-> Expr StartPoint StartPoint elem us
fixExpr = forall {k} (xs :: [k]) (f :: k -> *) (g :: k -> *).
(forall (x :: k). Membership xs x -> f x -> g x)
-> HFList f xs -> HFList g xs
HFList.hmapWithIndex
            do \Membership us x
_ Unit StringLit StartPoint elem x
u1 -> forall u.
Unit StringLit StartPoint elem u
-> Unit StartPoint StartPoint elem u
fixUnit Unit StringLit StartPoint elem x
u1

        fixUnit :: SyntaxGrammar.Unit IntermNonTerminal Terminal elem u
            -> SyntaxGrammar.Unit NonTerminal Terminal elem u
        fixUnit :: forall u.
Unit StringLit StartPoint elem u
-> Unit StartPoint StartPoint elem u
fixUnit Unit StringLit StartPoint elem u
u = case Unit StringLit StartPoint elem u
u of
            SyntaxGrammar.UnitToken StartPoint
t ->
                forall {k} terminal nonTerminal (elem :: k).
terminal -> Unit nonTerminal terminal elem elem
SyntaxGrammar.UnitToken StartPoint
t
            SyntaxGrammar.UnitVar StringLit
v ->
                forall {k} nonTerminal terminal (elem :: k) (u :: k).
nonTerminal -> Unit nonTerminal terminal elem u
SyntaxGrammar.UnitVar do StringLit -> StartPoint
getNewV StringLit
v

        rulesTag :: HashMap StringLit StartPoint
rulesTag = forall rules.
Rules rules =>
Proxy# rules -> HashMap StringLit StartPoint
genRulesTagMap do forall {k} (a :: k). Proxy# a
proxy# @rules

        getNewV :: StringLit -> StartPoint
getNewV StringLit
v = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup StringLit
v HashMap StringLit StartPoint
rulesTag of
            Just StartPoint
newV ->
                StartPoint
newV
            Maybe StartPoint
Nothing ->
                forall a. HasCallStack => StringLit -> a
error StringLit
"unreachable: rulesTag must include v."

type StartPoint = Int
type Terminal = Int
type NonTerminal = Int
type IntermNonTerminal = String


class MemberInitials rules initials where
    memberInitials :: HFList.T (HFList.DictF (HasRuleExprField rules)) initials

class Rules rules where
    generateRules :: HFList.T (HFList.DictF (HasRuleExprField rules)) (RulesTag rules)


genStartPoint :: forall initials v. Membership.Membership initials v -> StartPoint
genStartPoint :: forall {k} (initials :: [k]) (v :: k).
Membership initials v -> StartPoint
genStartPoint Membership initials v
m = forall {k} (initials :: [k]) (v :: k).
Membership initials v -> StartPoint
Membership.getMemberId Membership initials v
m

genRulesTagMap :: forall rules.
    Rules rules => Proxy# rules -> HashMap.HashMap IntermNonTerminal NonTerminal
genRulesTagMap :: forall rules.
Rules rules =>
Proxy# rules -> HashMap StringLit StartPoint
genRulesTagMap Proxy# rules
_ = forall {k} r (xs :: [k]) (f :: k -> *).
r
-> (forall (x :: k). r -> Membership xs x -> f x -> r)
-> HFList f xs
-> r
HFList.hfoldlWithIndex forall k v. HashMap k v
HashMap.empty forall (v :: Symbol).
HashMap StringLit StartPoint
-> Membership (RulesTag rules) v
-> DictF (HasRuleExprField rules) v
-> HashMap StringLit StartPoint
go forall rules.
Rules rules =>
T (DictF (HasRuleExprField rules)) (RulesTag rules)
generateRules where
    go :: forall v
        .  HashMap.HashMap IntermNonTerminal NonTerminal
        -> Membership.Membership (RulesTag rules) v
        -> HFList.DictF (HasRuleExprField rules) v
        -> HashMap.HashMap IntermNonTerminal NonTerminal
    go :: forall (v :: Symbol).
HashMap StringLit StartPoint
-> Membership (RulesTag rules) v
-> DictF (HasRuleExprField rules) v
-> HashMap StringLit StartPoint
go HashMap StringLit StartPoint
vMap Membership (RulesTag rules) v
m DictF (HasRuleExprField rules) v
HFList.DictF = forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
HashMap.insert
        do forall (n :: Symbol). KnownSymbol n => Proxy# n -> StringLit
symbolVal' do forall {k} (a :: k). Proxy# a
proxy# @v
        do forall {k} (initials :: [k]) (v :: k).
Membership initials v -> StartPoint
Membership.getMemberId Membership (RulesTag rules) v
m
        do HashMap StringLit StartPoint
vMap

type RuleExpr :: ([Type] -> Type -> Type) -> Type -> Type -> Type -> Type -> Type
newtype RuleExpr action rules tokens elem a = RuleExpr
    { forall (action :: [*] -> * -> *) rules tokens elem a.
RuleExpr action rules tokens elem a
-> [Alt action rules tokens elem a]
unRuleExpr :: [Alt action rules tokens elem a]
    }

type Alt :: ([Type] -> Type -> Type) -> Type -> Type -> Type -> Type -> Type
newtype Alt action rules tokens elem a = UnsafeAlt
    { forall (action :: [*] -> * -> *) rules tokens elem a.
Alt action rules tokens elem a
-> Alt StringLit StartPoint elem (Maybe ()) action a
unsafeAlt
        :: SyntaxGrammar.Alt IntermNonTerminal Terminal elem (Maybe ()) action a
    }

type Expr :: Type -> Type -> Type -> [Type] -> Type
newtype Expr rules tokens elem us = UnsafeExpr
    { forall rules tokens elem (us :: [*]).
Expr rules tokens elem us -> Expr StringLit StartPoint elem us
unsafeExpr :: SyntaxGrammar.Expr IntermNonTerminal Terminal elem us
    }

class TokensMember tokens t where
    tokensMembership :: Proxy# '(tokens, t) -> Membership.Membership (TokensTag tokens) t

ruleExpr :: [Alt action rules tokens elem a] -> RuleExpr action rules tokens elem a
ruleExpr :: forall (action :: [*] -> * -> *) rules tokens elem a.
[Alt action rules tokens elem a]
-> RuleExpr action rules tokens elem a
ruleExpr [Alt action rules tokens elem a]
alts = forall (action :: [*] -> * -> *) rules tokens elem a.
[Alt action rules tokens elem a]
-> RuleExpr action rules tokens elem a
RuleExpr [Alt action rules tokens elem a]
alts

(<:>)
    :: Expr rules tokens elem us -> action us a
    -> Alt action rules tokens elem a
UnsafeExpr Expr StringLit StartPoint elem us
e <:> :: forall rules tokens elem (us :: [*]) (action :: [*] -> * -> *) a.
Expr rules tokens elem us
-> action us a -> Alt action rules tokens elem a
<:> action us a
act = forall (action :: [*] -> * -> *) rules tokens elem a.
Alt StringLit StartPoint elem (Maybe ()) action a
-> Alt action rules tokens elem a
UnsafeAlt do forall {k} {k1} nonTerminal terminal (elem :: k) (us :: [k]) altDoc
       (action :: [k] -> k1 -> *) (a :: k1).
Expr nonTerminal terminal elem us
-> altDoc
-> action us a
-> Alt nonTerminal terminal elem altDoc action a
SyntaxGrammar.Alt Expr StringLit StartPoint elem us
e forall a. Maybe a
Nothing action us a
act

infixl 4 <:>

eps :: Expr rules tokens elem '[]
eps :: forall rules tokens elem. Expr rules tokens elem '[]
eps = forall rules tokens elem (us :: [*]).
Expr StringLit StartPoint elem us -> Expr rules tokens elem us
UnsafeExpr forall {k} (a :: k -> *). HFList a '[]
HFList.HFNil

(<^>)
    :: Expr rules tokens elem us1 -> Expr rules tokens elem us2
    -> Expr rules tokens elem (HFList.Concat us1 us2)
UnsafeExpr Expr StringLit StartPoint elem us1
e1 <^> :: forall rules tokens elem (us1 :: [*]) (us2 :: [*]).
Expr rules tokens elem us1
-> Expr rules tokens elem us2
-> Expr rules tokens elem (Concat us1 us2)
<^> UnsafeExpr Expr StringLit StartPoint elem us2
e2 = forall rules tokens elem (us :: [*]).
Expr StringLit StartPoint elem us -> Expr rules tokens elem us
UnsafeExpr do forall {k} (f :: k -> *) (xs1 :: [k]) (xs2 :: [k]).
HFList f xs1 -> HFList f xs2 -> HFList f (Concat xs1 xs2)
HFList.hconcat Expr StringLit StartPoint elem us1
e1 Expr StringLit StartPoint elem us2
e2

infixr 5 <^>

var :: KnownSymbol v => proxy v -> Expr rules tokens elem '[RuleExprReturnType rules v]
var :: forall (v :: Symbol) (proxy :: Symbol -> *) rules tokens elem.
KnownSymbol v =>
proxy v -> Expr rules tokens elem '[RuleExprReturnType rules v]
var proxy v
p = forall rules tokens elem (us :: [*]).
Expr StringLit StartPoint elem us -> Expr rules tokens elem us
UnsafeExpr do forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> HFList a xs -> HFList a (x : xs)
HFList.HFCons Unit StringLit StartPoint elem (RuleExprReturnType rules v)
u forall {k} (a :: k -> *). HFList a '[]
HFList.HFNil where
    u :: Unit StringLit StartPoint elem (RuleExprReturnType rules v)
u = forall {k} nonTerminal terminal (elem :: k) (u :: k).
nonTerminal -> Unit nonTerminal terminal elem u
SyntaxGrammar.UnitVar do forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> StringLit
symbolVal proxy v
p

varA :: forall v rules tokens elem.
    KnownSymbol v => Expr rules tokens elem '[RuleExprReturnType rules v]
varA :: forall (v :: Symbol) rules tokens elem.
KnownSymbol v =>
Expr rules tokens elem '[RuleExprReturnType rules v]
varA = forall (v :: Symbol) (proxy :: Symbol -> *) rules tokens elem.
KnownSymbol v =>
proxy v -> Expr rules tokens elem '[RuleExprReturnType rules v]
var do forall {k} (t :: k). Proxy t
Proxy @v

tok :: Membership.Membership (TokensTag tokens) t -> Expr rules tokens elem '[elem]
tok :: forall tokens (t :: Symbol) rules elem.
Membership (TokensTag tokens) t -> Expr rules tokens elem '[elem]
tok Membership (TokensTag tokens) t
p = forall rules tokens elem (us :: [*]).
Expr StringLit StartPoint elem us -> Expr rules tokens elem us
UnsafeExpr do forall {k} (a :: k -> *) (x :: k) (xs :: [k]).
a x -> HFList a xs -> HFList a (x : xs)
HFList.HFCons Unit StringLit StartPoint elem elem
u forall {k} (a :: k -> *). HFList a '[]
HFList.HFNil where
    u :: Unit StringLit StartPoint elem elem
u = forall {k} terminal nonTerminal (elem :: k).
terminal -> Unit nonTerminal terminal elem elem
SyntaxGrammar.UnitToken
        do forall k (as :: [k]). HEnum as -> StartPoint
HEnum.unsafeHEnum do forall {k} (a :: k) (as :: [k]). Membership as a -> HEnum as
HEnum.henum Membership (TokensTag tokens) t
p

tokA :: forall t rules tokens elem.
    TokensMember tokens t => Expr rules tokens elem '[elem]
tokA :: forall (t :: Symbol) rules tokens elem.
TokensMember tokens t =>
Expr rules tokens elem '[elem]
tokA = forall tokens (t :: Symbol) rules elem.
Membership (TokensTag tokens) t -> Expr rules tokens elem '[elem]
tok do forall tokens (t :: Symbol).
TokensMember tokens t =>
Proxy# '(tokens, t) -> Membership (TokensTag tokens) t
tokensMembership do forall {k} (a :: k). Proxy# a
proxy# @'(tokens, t)