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 TyConsts_of_Iface (Proxy []) = Proxy [] ': TyConsts_imported_by []
50 type instance TyConsts_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_TyNameR TyName cs rs
92 ) => Read_TyNameR TyName cs (Proxy [] ': rs) where
93 read_TyNameR _cs (TyName "[]") k = k (ty @[])
94 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
95 instance Show_TyConst cs => Show_TyConst (Proxy [] ': cs) where
96 show_TyConst TyConstZ{} = "[]"
97 show_TyConst (TyConstS c) = show_TyConst c
98 instance Show_TyConst cs => Show_TyConst (Proxy String ': cs) where
99 show_TyConst TyConstZ{} = "String"
100 show_TyConst (TyConstS c) = show_TyConst c
102 instance -- Proj_TyConC
104 , Proj_TyConsts cs (TyConsts_imported_by [])
106 ) => Proj_TyConC cs (Proxy []) where
107 proj_TyConC _ (TyConst q :$ TyConst c)
108 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
109 , Just Refl <- proj_TyConst c (Proxy @[])
111 _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
112 | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
113 | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
114 | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
115 | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
117 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
118 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
119 , Just Refl <- proj_TyConst c (Proxy @[])
121 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
122 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
123 | Just Refl <- proj_TyConst q (Proxy @Monoid) -> Just TyCon
124 | Just Refl <- proj_TyConst q (Proxy @Show)
125 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
126 | Just Refl <- proj_TyConst q (Proxy @Ord)
127 , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
129 proj_TyConC _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_TyName TyName (TyConsts_of_Ifaces is)
140 , Inj_TyConst (TyConsts_of_Ifaces is) []
141 , Inj_TyConst (TyConsts_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 (TyConsts_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_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
170 check_TyEq (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 (TyConsts_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 (TyConsts_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_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
196 check_TyEq2 (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)