]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Lib/List.hs
Fix Lib.Text.
[haskell/symantic.git] / Language / Symantic / Lib / List.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
4 -- | Symantic for '[]'.
5 module Language.Symantic.Lib.List where
6
7 import Control.Monad (liftM, liftM2, liftM3)
8 import qualified Data.Foldable as Foldable
9 import qualified Data.Function as Fun
10 import qualified Data.Functor as Functor
11 import qualified Data.List as List
12 import Data.Monoid ((<>))
13 import Data.Proxy
14 import qualified Data.Text as Text
15 import qualified Data.Traversable as Traversable
16 import Data.Type.Equality ((:~:)(Refl))
17 import Prelude hiding (zipWith)
18
19 import Language.Symantic.Parsing
20 import Language.Symantic.Parsing.Grammar
21 import Language.Symantic.Typing
22 import Language.Symantic.Compiling
23 import Language.Symantic.Interpreting
24 import Language.Symantic.Transforming.Trans
25 import Language.Symantic.Lib.Lambda
26
27 -- * Class 'Sym_List'
28 class Sym_List term where
29 list_empty :: term [a]
30 list_singleton :: term a -> term [a]
31 (.:) :: term a -> term [a] -> term [a]
32 list :: [term a] -> term [a]
33 zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
34
35 default list_empty :: Trans t term => t term [a]
36 default list_singleton :: Trans t term => t term a -> t term [a]
37 default (.:) :: Trans t term => t term a -> t term [a] -> t term [a]
38 default list :: Trans t term => [t term a] -> t term [a]
39 default zipWith :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
40
41 list_empty = trans_lift list_empty
42 list_singleton = trans_map1 list_singleton
43 (.:) = trans_map2 (.:)
44 list l = trans_lift (list (trans_apply Functor.<$> l))
45 zipWith = trans_map3 zipWith
46
47 infixr 5 .:
48
49 type instance Sym_of_Iface (Proxy []) = Sym_List
50 type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
51 type instance Consts_imported_by [] =
52 [ Proxy Applicative
53 , Proxy Bool
54 , Proxy Eq
55 , Proxy Foldable
56 , Proxy Functor
57 , Proxy Monad
58 , Proxy Monoid
59 , Proxy Ord
60 , Proxy Show
61 , Proxy Traversable
62 ]
63
64 instance Sym_List HostI where
65 list_empty = return []
66 list_singleton = liftM return
67 (.:) = liftM2 (:)
68 list = Traversable.sequence
69 zipWith = liftM3 List.zipWith
70 instance Sym_List TextI where
71 list_empty = TextI $ \_p _v -> "[]"
72 list_singleton a = textI_infix ":" op a list_empty
73 where op = infixR 5
74 (.:) = textI_infix ":" (infixR 5)
75 list l = TextI $ \_po v ->
76 "[" <> Text.intercalate ", " ((\(TextI a) -> a op v) Functor.<$> l) <> "]"
77 where op = (infixN0, L)
78 zipWith = textI3 "zipWith"
79 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
80 list_empty = dupI0 (Proxy @Sym_List) list_empty
81 list_singleton = dupI1 (Proxy @Sym_List) list_singleton
82 (.:) = dupI2 (Proxy @Sym_List) (.:)
83 list l =
84 let (l1, l2) =
85 Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
86 (x1:xs1, x2:xs2)) ([], []) l in
87 list l1 `DupI` list l2
88 zipWith = dupI3 (Proxy @Sym_List) zipWith
89
90 instance
91 ( Read_TypeNameR Type_Name cs rs
92 , Inj_Const cs []
93 ) => Read_TypeNameR Type_Name cs (Proxy [] ': rs) where
94 read_typenameR _cs (Type_Name "[]") k = k (ty @[])
95 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
96 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
97 show_const ConstZ{} = "[]"
98 show_const (ConstS c) = show_const c
99 instance Show_Const cs => Show_Const (Proxy String ': cs) where
100 show_const ConstZ{} = "String"
101 show_const (ConstS c) = show_const c
102
103 instance -- Proj_ConC
104 ( Proj_Const cs []
105 , Proj_Consts cs (Consts_imported_by [])
106 , Proj_Con cs
107 ) => Proj_ConC cs (Proxy []) where
108 proj_conC _ (TyConst q :$ TyConst c)
109 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
110 , Just Refl <- proj_const c (Proxy @[])
111 = case () of
112 _ | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
113 | Just Refl <- proj_const q (Proxy @Foldable) -> Just Con
114 | Just Refl <- proj_const q (Proxy @Functor) -> Just Con
115 | Just Refl <- proj_const q (Proxy @Monad) -> Just Con
116 | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
117 _ -> Nothing
118 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
119 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
120 , Just Refl <- proj_const c (Proxy @[])
121 = case () of
122 _ | Just Refl <- proj_const q (Proxy @Eq)
123 , Just Con <- proj_con (t :$ a) -> Just Con
124 | Just Refl <- proj_const q (Proxy @Monoid) -> Just Con
125 | Just Refl <- proj_const q (Proxy @Show)
126 , Just Con <- proj_con (t :$ a) -> Just Con
127 | Just Refl <- proj_const q (Proxy @Ord)
128 , Just Con <- proj_con (t :$ a) -> Just Con
129 _ -> Nothing
130 proj_conC _c _q = Nothing
131 data instance TokenT meta (ts::[*]) (Proxy [])
132 = Token_Term_List_empty (EToken meta '[Proxy Token_Type])
133 | Token_Term_List_cons (EToken meta ts) (EToken meta ts)
134 | Token_Term_List_singleton (EToken meta ts)
135 | Token_Term_List_list (EToken meta '[Proxy Token_Type]) [EToken meta ts]
136 | Token_Term_List_zipWith (EToken meta ts)
137 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
138 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
139 instance -- CompileI
140 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
141 , Inj_Const (Consts_of_Ifaces is) []
142 , Inj_Const (Consts_of_Ifaces is) (->)
143 , Compile is
144 ) => CompileI is (Proxy []) where
145 compileI
146 :: forall meta ctx ret ls rs.
147 TokenT meta is (Proxy [])
148 -> CompileT meta ctx ret is ls (Proxy [] ': rs)
149 compileI tok ctx k =
150 case tok of
151 Token_Term_List_empty tok_ty_a ->
152 -- [] :: [a]
153 compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
154 check_kind
155 (At Nothing SKiType)
156 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
157 k (ty @[] :$ ty_a) $ TermO $
158 Fun.const list_empty
159 Token_Term_List_singleton tok_a ->
160 -- [a] :: [a]
161 compileO tok_a ctx $ \ty_a (TermO a) ->
162 check_kind
163 (At Nothing SKiType)
164 (At (Just tok_a) $ kind_of ty_a) $ \Refl ->
165 k (ty @[] :$ ty_a) $ TermO $
166 \c -> list_singleton (a c)
167 Token_Term_List_cons tok_a tok_as ->
168 compileO tok_a ctx $ \ty_a (TermO a) ->
169 compileO tok_as ctx $ \ty_as (TermO as) ->
170 check_type1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
171 check_type (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl ->
172 k ty_as $ TermO $
173 \c -> a c .: as c
174 Token_Term_List_list tok_ty_a tok_as ->
175 compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
176 check_kind
177 (At Nothing SKiType)
178 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
179 go (At (Just tok_ty_a) ty_a) [] tok_as
180 where
181 go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
182 -> [TermO ctx ty_a is '[] is]
183 -> [EToken meta is]
184 -> Either (Error_Term meta is) ret
185 go ty_a as [] =
186 k (ty @[] :$ unAt ty_a) $ TermO $
187 \c -> list $ (\(TermO a) -> a c)
188 Functor.<$> List.reverse as
189 go ty_a as (tok_x:tok_xs) =
190 compileO tok_x ctx $ \ty_x x ->
191 check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
192 go ty_a (x:as) tok_xs
193 Token_Term_List_zipWith tok_a2b2c ->
194 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
195 compileO tok_a2b2c ctx $ \ty_a2b2c (TermO a2b2c) ->
196 check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
197 check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
198 k ( ty @[] :$ ty_a2b2c_a
199 ~> ty @[] :$ ty_a2b2c_b2c_b
200 ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermO $
201 \c -> lam $ lam . zipWith (a2b2c c)
202 instance -- TokenizeT
203 Inj_Token meta ts [] =>
204 TokenizeT meta ts (Proxy []) where
205 tokenizeT _t = mempty
206 { tokenizers_infix = tokenizeTMod []
207 [ (Term_Name "[]",) $ Term_ProTok
208 { term_protok = \meta -> ProTokPi $ \a ->
209 ProTok $ inj_etoken meta $ Token_Term_List_empty a
210 , term_fixity = infixN5
211 }
212 , tokenize2 ":" (infixR 5) Token_Term_List_cons
213 , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith
214 ]
215 }
216 instance
217 ( App g
218 , Gram_Rule g
219 , Gram_Lexer g
220 , Gram_Term ts meta g
221 , Inj_Token meta ts (->)
222 , Inj_Token meta ts []
223 ) => Gram_Term_AtomsT meta ts (Proxy []) g where
224 term_atomsT _t =
225 [ rule "term_list" $
226 ProTok <$> between (symbol "[") (symbol "]") listG
227 , rule "term_list_empty" $
228 metaG $
229 (\meta -> ProTokPi $ \a -> ProTok $ inj_etoken meta $ Token_Term_List_empty a)
230 <$ symbol "["
231 <* symbol "]"
232 ]
233 where
234 listG :: CF g (EToken meta ts)
235 listG = rule "list" $
236 metaG $
237 (\a mb meta -> inj_etoken meta $ case mb of
238 Just b -> Token_Term_List_cons a b
239 Nothing -> Token_Term_List_singleton a)
240 <$> termG
241 <*> option Nothing (Just <$ symbol "," <*> listG)