import qualified Data.Text as Text
import Language.Symantic.Grammar hiding (char, any)
-import qualified Language.Symantic.Grammar as Gram
+import qualified Language.Symantic.Grammar as G
import Language.Symantic
import Language.Symantic.Lib.List (tyList)
instance (Sym_Char term, Sym_Lambda term) => Sym_Char (BetaT term)
-- Typing
+instance NameTyOf Char where
+ nameTyOf _c = ["Char"] `Mod` "Char"
instance ClassInstancesFor Char where
proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
| Just HRefl <- proj_ConstKiTy @_ @Char z
, Gram_Alt g
, Gram_Rule g
, Gram_Comment g
- , Inj_Sym ss Char
+ , SymInj ss Char
) => Gram_Term_AtomsFor src ss g Char where
g_term_atomsFor =
[ rule "teChar" $
- lexeme $ g_source $
+ lexeme $ source $
(\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c)
<$> between tickG tickG (
- cf_of_Terminal (Gram.any `but` tickG) <+>
+ cfOf (G.any `but` tickG) <+>
'\'' <$ string "\\'"
)
]
where
tickG :: Gram_Terminal g' => g' Char
- tickG = Gram.char '\''
-instance (Source src, Inj_Sym ss Char) => ModuleFor src ss Char where
+ tickG = G.char '\''
+instance (Source src, SymInj ss Char) => ModuleFor src ss Char where
moduleFor = ["Char"] `moduleWhere`
[ "toLower" := teChar_toLower
, "toUpper" := teChar_toUpper
]
-- ** 'Type's
-tyChar :: Source src => Inj_Len vs => Type src vs Char
+tyChar :: Source src => LenInj vs => Type src vs Char
tyChar = tyConst @(K Char) @Char
-tyString :: Source src => Inj_Len vs => Type src vs String
+tyString :: Source src => LenInj vs => Type src vs String
tyString = tyList tyChar
-- ** 'Term's
-teChar :: Source src => Inj_Sym ss Char => Char -> Term src ss ts '[] (() #> Char)
+teChar :: Source src => SymInj ss Char => Char -> Term src ss ts '[] (() #> Char)
teChar b = Term noConstraint tyChar $ teSym @Char $ char b
teChar_toUpper, teChar_toLower :: TermDef Char '[] (() #> (Char -> Char))