{-# 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)