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
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 ((<>))
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)
19 import Language.Symantic.Parsing
20 import Language.Symantic.Typing
21 import Language.Symantic.Compiling
22 import Language.Symantic.Interpreting
23 import Language.Symantic.Transforming
24 import Language.Symantic.Lib.Lambda
27 class Sym_List term where
28 list_empty :: term [a]
29 list_singleton :: term a -> term [a]
30 (.:) :: term a -> term [a] -> term [a]
31 list :: [term a] -> term [a]
32 zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
34 default list_empty :: Trans t term => t term [a]
35 default list_singleton :: Trans t term => t term a -> t term [a]
36 default (.:) :: Trans t term => t term a -> t term [a] -> t term [a]
37 default list :: Trans t term => [t term a] -> t term [a]
38 default zipWith :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
40 list_empty = trans_lift list_empty
41 list_singleton = trans_map1 list_singleton
42 (.:) = trans_map2 (.:)
43 list l = trans_lift (list (trans_apply Functor.<$> l))
44 zipWith = trans_map3 zipWith
48 type instance Sym_of_Iface (Proxy []) = Sym_List
49 type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
50 type instance Consts_imported_by [] =
63 instance Sym_List HostI where
64 list_empty = return []
65 list_singleton = liftM return
67 list = Traversable.sequence
68 zipWith = liftM3 List.zipWith
69 instance Sym_List TextI where
70 list_empty = TextI $ \_p _v -> "[]"
71 list_singleton a = textI_infix ":" op a list_empty
73 (.:) = textI_infix ":" (infixR 5)
74 list l = TextI $ \_po v ->
75 "[" <> Text.intercalate ", " ((\(TextI a) -> a op v) Functor.<$> l) <> "]"
76 where op = (infixN0, L)
77 zipWith = textI3 "zipWith"
78 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
79 list_empty = dupI0 (Proxy @Sym_List) list_empty
80 list_singleton = dupI1 (Proxy @Sym_List) list_singleton
81 (.:) = dupI2 (Proxy @Sym_List) (.:)
84 Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
85 (x1:xs1, x2:xs2)) ([], []) l in
86 list l1 `DupI` list l2
87 zipWith = dupI3 (Proxy @Sym_List) zipWith
90 ( Read_TypeNameR Type_Name cs rs
92 ) => Read_TypeNameR Type_Name cs (Proxy [] ': rs) where
93 read_typenameR _cs (Type_Name "[]") k = k (ty @[])
94 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
95 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
96 show_const ConstZ{} = "[]"
97 show_const (ConstS c) = show_const c
98 instance Show_Const cs => Show_Const (Proxy String ': cs) where
99 show_const ConstZ{} = "String"
100 show_const (ConstS c) = show_const c
102 instance -- Proj_ConC
104 , Proj_Consts cs (Consts_imported_by [])
106 ) => Proj_ConC cs (Proxy []) where
107 proj_conC _ (TyConst q :$ TyConst c)
108 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
109 , Just Refl <- proj_const c (Proxy @[])
111 _ | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
112 | Just Refl <- proj_const q (Proxy @Foldable) -> Just Con
113 | Just Refl <- proj_const q (Proxy @Functor) -> Just Con
114 | Just Refl <- proj_const q (Proxy @Monad) -> Just Con
115 | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
117 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
118 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
119 , Just Refl <- proj_const c (Proxy @[])
121 _ | Just Refl <- proj_const q (Proxy @Eq)
122 , Just Con <- proj_con (t :$ a) -> Just Con
123 | Just Refl <- proj_const q (Proxy @Monoid) -> Just Con
124 | Just Refl <- proj_const q (Proxy @Show)
125 , Just Con <- proj_con (t :$ a) -> Just Con
126 | Just Refl <- proj_const q (Proxy @Ord)
127 , Just Con <- proj_con (t :$ a) -> Just Con
129 proj_conC _c _q = Nothing
130 data instance TokenT meta (ts::[*]) (Proxy [])
131 = Token_Term_List_empty (EToken meta '[Proxy Token_Type])
132 | Token_Term_List_cons (EToken meta ts) (EToken meta ts)
133 | Token_Term_List_singleton (EToken meta ts)
134 | Token_Term_List_list (EToken meta '[Proxy Token_Type]) [EToken meta ts]
135 | Token_Term_List_zipWith (EToken meta ts)
136 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
137 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
139 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
140 , Inj_Const (Consts_of_Ifaces is) []
141 , Inj_Const (Consts_of_Ifaces is) (->)
143 ) => CompileI is (Proxy []) where
145 :: forall meta ctx ret ls rs.
146 TokenT meta is (Proxy [])
147 -> CompileT meta ctx ret is ls (Proxy [] ': rs)
150 Token_Term_List_empty tok_ty_a ->
152 compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
155 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
156 k (ty @[] :$ ty_a) $ TermO $
158 Token_Term_List_singleton tok_a ->
160 compileO tok_a ctx $ \ty_a (TermO a) ->
163 (At (Just tok_a) $ kind_of ty_a) $ \Refl ->
164 k (ty @[] :$ ty_a) $ TermO $
165 \c -> list_singleton (a c)
166 Token_Term_List_cons tok_a tok_as ->
167 compileO tok_a ctx $ \ty_a (TermO a) ->
168 compileO tok_as ctx $ \ty_as (TermO as) ->
169 check_type1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
170 check_type (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl ->
173 Token_Term_List_list tok_ty_a tok_as ->
174 compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
177 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
178 go (At (Just tok_ty_a) ty_a) [] tok_as
180 go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
181 -> [TermO ctx ty_a is '[] is]
183 -> Either (Error_Term meta is) ret
185 k (ty @[] :$ unAt ty_a) $ TermO $
186 \c -> list $ (\(TermO a) -> a c)
187 Functor.<$> List.reverse as
188 go ty_a as (tok_x:tok_xs) =
189 compileO tok_x ctx $ \ty_x x ->
190 check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
191 go ty_a (x:as) tok_xs
192 Token_Term_List_zipWith tok_a2b2c ->
193 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
194 compileO tok_a2b2c ctx $ \ty_a2b2c (TermO a2b2c) ->
195 check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
196 check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
197 k ( ty @[] :$ ty_a2b2c_a
198 ~> ty @[] :$ ty_a2b2c_b2c_b
199 ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermO $
200 \c -> lam $ lam . zipWith (a2b2c c)
201 instance -- TokenizeT
202 Inj_Token meta ts [] =>
203 TokenizeT meta ts (Proxy []) where
204 tokenizeT _t = mempty
205 { tokenizers_infix = tokenizeTMod []
206 [ (Term_Name "[]",) $ Term_ProTok
207 { term_protok = \meta -> ProTokPi $ \a ->
208 ProTok $ inj_etoken meta $ Token_Term_List_empty a
209 , term_fixity = infixN5
211 , tokenize2 ":" (infixR 5) Token_Term_List_cons
212 , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith
219 , Gram_Term ts meta g
220 , Inj_Token meta ts (->)
221 , Inj_Token meta ts []
222 ) => Gram_Term_AtomsT meta ts (Proxy []) g where
225 ProTok <$> between (symbol "[") (symbol "]") listG
226 , rule "term_list_empty" $
228 (\meta -> ProTokPi $ \a -> ProTok $ inj_etoken meta $ Token_Term_List_empty a)
233 listG :: CF g (EToken meta ts)
234 listG = rule "list" $
236 (\a mb meta -> inj_etoken meta $ case mb of
237 Just b -> Token_Term_List_cons a b
238 Nothing -> Token_Term_List_singleton a)
240 <*> option Nothing (Just <$ symbol "," <*> listG)