-- | Symantic for 'Char'.
module Language.Symantic.Lib.Char where
-import Control.Monad (liftM)
import qualified Data.Char as Char
-import Data.Proxy
import qualified Data.Text as Text
-import Data.Type.Equality ((:~:)(Refl))
-import Language.Symantic.Parsing hiding (char)
-import qualified Language.Symantic.Grammar as Gram
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+import Language.Symantic.Grammar hiding (char, any)
+import qualified Language.Symantic.Grammar as G
+import Language.Symantic
+import Language.Symantic.Lib.List (tyList)
-- * Class 'Sym_Char'
+type instance Sym Char = Sym_Char
class Sym_Char term where
char :: Char -> term Char
char_toUpper :: term Char -> term Char
char_toLower :: term Char -> term Char
- default char :: Trans t term => Char -> t term Char
- default char_toUpper :: Trans t term => t term Char -> t term Char
- default char_toLower :: Trans t term => t term Char -> t term Char
+ default char :: Sym_Char (UnT term) => Trans term => Char -> term Char
+ default char_toUpper :: Sym_Char (UnT term) => Trans term => term Char -> term Char
+ default char_toLower :: Sym_Char (UnT term) => Trans term => term Char -> term Char
- char = trans_lift . char
- char_toUpper = trans_map1 char_toUpper
- char_toLower = trans_map1 char_toLower
+ char = trans . char
+ char_toUpper = trans1 char_toUpper
+ char_toLower = trans1 char_toLower
-type instance Sym_of_Iface (Proxy Char) = Sym_Char
-type instance TyConsts_of_Iface (Proxy Char) = Proxy Char ': TyConsts_imported_by Char
-type instance TyConsts_imported_by Char =
- [ Proxy Bounded
- , Proxy Enum
- , Proxy Eq
- , Proxy Ord
- , Proxy Show
- ]
-
-instance Sym_Char HostI where
- char = HostI
- char_toUpper = liftM Char.toUpper
- char_toLower = liftM Char.toLower
-instance Sym_Char TextI where
- char a = TextI $ \_p _v ->
+-- Interpreting
+instance Sym_Char Eval where
+ char = Eval
+ char_toUpper = eval1 Char.toUpper
+ char_toLower = eval1 Char.toLower
+instance Sym_Char View where
+ char a = View $ \_p _v ->
Text.pack (show a)
- char_toUpper = textI1 "Char.toUpper"
- char_toLower = textI1 "Char.toLower"
-instance (Sym_Char r1, Sym_Char r2) => Sym_Char (DupI r1 r2) where
- char x = char x `DupI` char x
- char_toUpper = dupI1 @Sym_Char char_toUpper
- char_toLower = dupI1 @Sym_Char char_toLower
+ char_toUpper = view1 "Char.toUpper"
+ char_toLower = view1 "Char.toLower"
+instance (Sym_Char r1, Sym_Char r2) => Sym_Char (Dup r1 r2) where
+ char x = char x `Dup` char x
+ char_toUpper = dup1 @Sym_Char char_toUpper
+ char_toLower = dup1 @Sym_Char char_toLower
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Char
- ) => Read_TyNameR TyName cs (Proxy Char ': rs) where
- read_TyNameR _cs (TyName "Char") k = k (ty @Char)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Char ': cs) where
- show_TyConst TyConstZ{} = "Char"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Transforming
+instance (Sym_Char term, Sym_Lambda term) => Sym_Char (BetaT term)
-instance -- Proj_TyConC
- ( Proj_TyConst cs Char
- , Proj_TyConsts cs (TyConsts_imported_by Char)
- ) => Proj_TyConC cs (Proxy Char) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
- , Just Refl <- proj_TyConst c (Proxy @Char)
+-- 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
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Bounded) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show) -> Just TyCon
+ _ | Just Refl <- proj_Const @Bounded q -> Just Dict
+ | Just Refl <- proj_Const @Enum q -> Just Dict
+ | Just Refl <- proj_Const @Eq q -> Just Dict
+ | Just Refl <- proj_Const @Ord q -> Just Dict
+ | Just Refl <- proj_Const @Show q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy Char)
- = Token_Term_Char Char
- | Token_Term_Char_toUpper
- | Token_Term_Char_toLower
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Char))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Char))
-instance -- CompileI
- ( Inj_TyConst cs Char
- , Inj_TyConst cs (->)
- ) => CompileI cs is (Proxy Char) where
- compileI tok _ctx k =
- case tok of
- Token_Term_Char c -> k (ty @Char) $ TermO $ \_c -> char c
- Token_Term_Char_toUpper -> from_op char_toUpper
- Token_Term_Char_toLower -> from_op char_toLower
- where
- from_op (op::forall term. Sym_Char term => term Char -> term Char) =
- k (ty @Char ~> ty @Char) $ TermO $ \_c -> lam op
-instance -- TokenizeT
- Inj_Token meta ts Char =>
- TokenizeT meta ts (Proxy Char) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod [Mod_Name "Char"]
- [ tokenize0 "toLower" infixN5 Token_Term_Char_toLower
- , tokenize0 "toUpper" infixN5 Token_Term_Char_toUpper
- ]
- }
-instance -- Gram_Term_AtomsT
- ( Alt g
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Char
+
+-- Compiling
+instance
+ ( Gram_Source src g
+ , Gram_Alt g
, Gram_Rule g
- , Gram_Lexer g
- , Gram_Meta meta g
- , Inj_Token meta ts Char
- ) => Gram_Term_AtomsT meta ts (Proxy Char) g where
- gs_term_atomsT _t =
- [ rule "term_char" $
- lexeme $ metaG $
- (\c meta -> ProTok $ inj_EToken meta $ Token_Term_Char c)
- <$> Gram.between tickG tickG (
- Gram.cf_of_Terminal (Gram.any `Gram.but` tickG) Gram.<+>
- '\'' <$ Gram.string "\\'"
+ , Gram_Comment g
+ , SymInj ss Char
+ ) => Gram_Term_AtomsFor src ss g Char where
+ g_term_atomsFor =
+ [ rule "teChar" $
+ lexeme $ source $
+ (\c src -> BinTree0 $ Token_Term $ TermAVT $ (`setSource` src) $ teChar c)
+ <$> between tickG tickG (
+ cfOf (G.any `but` tickG) <+>
+ '\'' <$ string "\\'"
)
]
where
tickG :: Gram_Terminal g' => g' Char
- tickG = Gram.char '\''
+ 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 => LenInj vs => Type src vs Char
+tyChar = tyConst @(K Char) @Char
+
+tyString :: Source src => LenInj vs => Type src vs String
+tyString = tyList tyChar
+
+-- ** 'Term's
+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))
+teChar_toUpper = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toUpper
+teChar_toLower = Term noConstraint (tyChar ~> tyChar) $ teSym @Char $ lam1 char_toLower
sourcephile / git / haskell / symantic.git / blobdiff