]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/Char.hs
Use more TypeApplications.
[haskell/symantic.git] / Language / Symantic / Lib / Char.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Char'.
4 module Language.Symantic.Lib.Char where
5
6 import Control.Monad (liftM)
7 import qualified Data.Char as Char
8 import Data.Proxy
9 import qualified Data.Text as Text
10 import Data.Type.Equality ((:~:)(Refl))
11
12 import Language.Symantic.Parsing
13 import Language.Symantic.Parsing.Grammar hiding (char)
14 import qualified Language.Symantic.Parsing.Grammar as Gram
15 import Language.Symantic.Typing
16 import Language.Symantic.Compiling
17 import Language.Symantic.Interpreting
18 import Language.Symantic.Transforming.Trans
19 import Language.Symantic.Lib.Lambda
20
21 -- * Class 'Sym_Char'
22 class Sym_Char term where
23 char :: Char -> term Char
24 char_toUpper :: term Char -> term Char
25 char_toLower :: term Char -> term Char
26
27 default char :: Trans t term => Char -> t term Char
28 default char_toUpper :: Trans t term => t term Char -> t term Char
29 default char_toLower :: Trans t term => t term Char -> t term Char
30
31 char = trans_lift . char
32 char_toUpper = trans_map1 char_toUpper
33 char_toLower = trans_map1 char_toLower
34
35 type instance Sym_of_Iface (Proxy Char) = Sym_Char
36 type instance Consts_of_Iface (Proxy Char) = Proxy Char ': Consts_imported_by Char
37 type instance Consts_imported_by Char =
38 [ Proxy Bounded
39 , Proxy Enum
40 , Proxy Eq
41 , Proxy Ord
42 , Proxy Show
43 ]
44
45 instance Sym_Char HostI where
46 char = HostI
47 char_toUpper = liftM Char.toUpper
48 char_toLower = liftM Char.toLower
49 instance Sym_Char TextI where
50 char a = TextI $ \_p _v ->
51 Text.pack (show a)
52 char_toUpper = textI1 "Char.toUpper"
53 char_toLower = textI1 "Char.toLower"
54 instance (Sym_Char r1, Sym_Char r2) => Sym_Char (DupI r1 r2) where
55 char x = char x `DupI` char x
56 char_toUpper = dupI1 (Proxy @Sym_Char) char_toUpper
57 char_toLower = dupI1 (Proxy @Sym_Char) char_toLower
58
59 instance
60 ( Read_TypeNameR Type_Name cs rs
61 , Inj_Const cs Char
62 ) => Read_TypeNameR Type_Name cs (Proxy Char ': rs) where
63 read_typenameR _cs (Type_Name "Char") k = k (ty @Char)
64 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
65 instance Show_Const cs => Show_Const (Proxy Char ': cs) where
66 show_const ConstZ{} = "Char"
67 show_const (ConstS c) = show_const c
68
69 instance -- Proj_ConC
70 ( Proj_Const cs Char
71 , Proj_Consts cs (Consts_imported_by Char)
72 ) => Proj_ConC cs (Proxy Char) where
73 proj_conC _ (TyConst q :$ TyConst c)
74 | Just Refl <- eq_skind (kind_of_const c) SKiType
75 , Just Refl <- proj_const c (Proxy @Char)
76 = case () of
77 _ | Just Refl <- proj_const q (Proxy @Bounded) -> Just Con
78 | Just Refl <- proj_const q (Proxy @Enum) -> Just Con
79 | Just Refl <- proj_const q (Proxy @Eq) -> Just Con
80 | Just Refl <- proj_const q (Proxy @Ord) -> Just Con
81 | Just Refl <- proj_const q (Proxy @Show) -> Just Con
82 _ -> Nothing
83 proj_conC _c _q = Nothing
84 data instance TokenT meta (ts::[*]) (Proxy Char)
85 = Token_Term_Char Char
86 | Token_Term_Char_toUpper
87 | Token_Term_Char_toLower
88 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Char))
89 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Char))
90 instance -- CompileI
91 ( Inj_Const (Consts_of_Ifaces is) Char
92 , Inj_Const (Consts_of_Ifaces is) (->)
93 ) => CompileI is (Proxy Char) where
94 compileI tok _ctx k =
95 case tok of
96 Token_Term_Char c -> k (ty @Char) $ TermO $ \_c -> char c
97 Token_Term_Char_toUpper -> from_op char_toUpper
98 Token_Term_Char_toLower -> from_op char_toLower
99 where
100 from_op (op::forall term. Sym_Char term => term Char -> term Char) =
101 k (ty @Char ~> ty @Char) $ TermO $ \_c -> lam op
102 instance -- TokenizeT
103 Inj_Token meta ts Char =>
104 TokenizeT meta ts (Proxy Char) where
105 tokenizeT _t = mempty
106 { tokenizers_infix = tokenizeTMod [Mod_Name "Char"]
107 [ tokenize0 "toLower" infixN5 Token_Term_Char_toLower
108 , tokenize0 "toUpper" infixN5 Token_Term_Char_toUpper
109 ]
110 }
111 instance -- Gram_Term_AtomsT
112 ( Alt g
113 , Gram_Rule g
114 , Gram_Lexer g
115 , Gram_Meta meta g
116 , Inj_Token meta ts Char
117 ) => Gram_Term_AtomsT meta ts (Proxy Char) g where
118 term_atomsT _t =
119 [ rule "term_char" $
120 lexeme $ metaG $
121 (\c meta -> ProTok $ inj_etoken meta $ Token_Term_Char c)
122 <$> Gram.between tickG tickG (
123 Gram.cf_of_term (Gram.any `Gram.but` tickG) Gram.<+>
124 '\'' <$ Gram.string "\\'"
125 )
126 ]
127 where
128 tickG :: Gram_Terminal g' => g' Char
129 tickG = Gram.char '\''