]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/List.hs
Add Compiling.Show.
[haskell/symantic.git] / Language / Symantic / Compiling / 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.Compiling.List where
6
7 import Control.Monad (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 Data.Text (Text)
15 import qualified Data.Text as Text
16 import qualified Data.Traversable as Traversable
17 import Data.Type.Equality ((:~:)(Refl))
18 import Prelude hiding (zipWith)
19
20 import Language.Symantic.Parsing
21 import Language.Symantic.Typing
22 import Language.Symantic.Compiling.Term
23 import Language.Symantic.Interpreting
24 import Language.Symantic.Transforming.Trans
25
26 -- * Class 'Sym_List'
27 class Sym_List term where
28 list_empty :: term [a]
29 zipWith :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
30 list :: [term a] -> term [a]
31
32 default list_empty :: Trans t term => t term [a]
33 default zipWith :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
34 default list :: Trans t term => [t term a] -> t term [a]
35
36 list_empty = trans_lift list_empty
37 zipWith = trans_map3 zipWith
38 list l = trans_lift (list (trans_apply Functor.<$> l))
39
40 type instance Sym_of_Iface (Proxy []) = Sym_List
41 type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
42 type instance Consts_imported_by [] =
43 [ Proxy Applicative
44 , Proxy Bool
45 , Proxy Eq
46 , Proxy Foldable
47 , Proxy Functor
48 , Proxy Monad
49 , Proxy Monoid
50 , Proxy Ord
51 , Proxy Show
52 , Proxy Traversable
53 ]
54
55 instance Sym_List HostI where
56 list_empty = return []
57 list = Traversable.sequence
58 zipWith = liftM3 List.zipWith
59 instance Sym_List TextI where
60 list_empty = TextI $ \_p _v -> "[]"
61 list l = TextI $ \_p v ->
62 let p' = precedence_Toplevel in
63 "[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
64 zipWith = textI_app3 "zipWith"
65 instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
66 list_empty = dupI0 (Proxy @Sym_List) list_empty
67 list l =
68 let (l1, l2) =
69 Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
70 (x1:xs1, x2:xs2)) ([], []) l in
71 list l1 `DupI` list l2
72 zipWith = dupI3 (Proxy @Sym_List) zipWith
73
74 instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
75 const_from "[]" k = k (ConstZ kind)
76 const_from s k = const_from s $ k . ConstS
77 instance Show_Const cs => Show_Const (Proxy [] ': cs) where
78 show_const ConstZ{} = "[]"
79 show_const (ConstS c) = show_const c
80 instance Const_from String cs => Const_from String (Proxy String ': cs) where
81 const_from "String" k = k (ConstZ kind)
82 const_from s k = const_from s $ k . ConstS
83 instance Show_Const cs => Show_Const (Proxy String ': cs) where
84 show_const ConstZ{} = "String"
85 show_const (ConstS c) = show_const c
86
87 instance -- Proj_ConC
88 ( Proj_Const cs []
89 , Proj_Consts cs (Consts_imported_by [])
90 , Proj_Con cs
91 ) => Proj_ConC cs (Proxy []) where
92 proj_conC _ (TyConst q :$ TyConst c)
93 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
94 , Just Refl <- proj_const c (Proxy::Proxy [])
95 = case () of
96 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
97 | Just Refl <- proj_const q (Proxy::Proxy Foldable) -> Just Con
98 | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con
99 | Just Refl <- proj_const q (Proxy::Proxy Monad) -> Just Con
100 | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
101 _ -> Nothing
102 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
103 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
104 , Just Refl <- proj_const c (Proxy::Proxy [])
105 = case () of
106 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
107 , Just Con <- proj_con (t :$ a) -> Just Con
108 | Just Refl <- proj_const q (Proxy::Proxy Monoid) -> Just Con
109 | Just Refl <- proj_const q (Proxy::Proxy Show)
110 , Just Con <- proj_con (t :$ a) -> Just Con
111 | Just Refl <- proj_const q (Proxy::Proxy Ord)
112 , Just Con <- proj_con (t :$ a) -> Just Con
113 _ -> Nothing
114 proj_conC _c _q = Nothing
115 data instance TokenT meta (ts::[*]) (Proxy [])
116 = Token_Term_List_empty (EToken meta '[Proxy Token_Type])
117 | Token_Term_List_list (EToken meta '[Proxy Token_Type]) [EToken meta ts]
118 | Token_Term_List_zipWith (EToken meta ts)
119 deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
120 deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
121 instance -- Term_fromI
122 ( Const_from Name_LamVar (Consts_of_Ifaces is)
123 , Inj_Const (Consts_of_Ifaces is) []
124 , Inj_Const (Consts_of_Ifaces is) (->)
125 , Term_from is
126 ) => Term_fromI is (Proxy []) where
127 term_fromI
128 :: forall meta ctx ret ls rs.
129 TokenT meta is (Proxy [])
130 -> Term_fromT meta ctx ret is ls (Proxy [] ': rs)
131 term_fromI tok ctx k =
132 case tok of
133 Token_Term_List_empty tok_ty_a ->
134 -- [] :: [a]
135 type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
136 check_kind
137 (At Nothing SKiType)
138 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
139 k (ty @[] :$ ty_a) $ TermLC $
140 Fun.const list_empty
141 Token_Term_List_list tok_ty_a tok_as ->
142 type_from tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
143 check_kind
144 (At Nothing SKiType)
145 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
146 go (At (Just tok_ty_a) ty_a) [] tok_as
147 where
148 go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
149 -> [TermLC ctx ty_a is '[] is]
150 -> [EToken meta is]
151 -> Either (Error_Term meta is) ret
152 go ty_a as [] =
153 k (ty @[] :$ unAt ty_a) $ TermLC $
154 \c -> list $ (\(TermLC a) -> a c)
155 Functor.<$> List.reverse as
156 go ty_a as (tok_x:tok_xs) =
157 term_from tok_x ctx $ \ty_x x ->
158 check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
159 go ty_a (x:as) tok_xs
160 Token_Term_List_zipWith tok_a2b2c ->
161 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
162 term_from tok_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
163 check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
164 check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
165 k ( ty @[] :$ ty_a2b2c_a
166 ~> ty @[] :$ ty_a2b2c_b2c_b
167 ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermLC $
168 \c -> lam $ lam . zipWith (a2b2c c)