]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Tuple2.hs
Add compileWithTyCtx.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Tuple2.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 {-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-}
4 -- | Symantic for @(,)@.
5 module Language.Symantic.Lib.Tuple2 where
6
7 import Control.Monad (liftM, liftM2)
8 import Data.Monoid ((<>))
9 import Data.Proxy
10 import Data.Type.Equality ((:~:)(Refl))
11 import Prelude hiding (fst, snd)
12 import qualified Data.Tuple as Tuple
13 import qualified Data.MonoTraversable as MT
14
15 import Language.Symantic.Parsing
16 import Language.Symantic.Typing
17 import Language.Symantic.Compiling
18 import Language.Symantic.Interpreting
19 import Language.Symantic.Transforming
20 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)
21
22 -- * Class 'Sym_Tuple2'
23 class Sym_Tuple2 term where
24 tuple2 :: term a -> term b -> term (a, b)
25 fst :: term (a, b) -> term a
26 snd :: term (a, b) -> term b
27
28 default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
29 default fst :: Trans t term => t term (a, b) -> t term a
30 default snd :: Trans t term => t term (a, b) -> t term b
31
32 tuple2 = trans_map2 tuple2
33 fst = trans_map1 fst
34 snd = trans_map1 snd
35
36 type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
37 type instance TyConsts_of_Iface (Proxy (,)) = Proxy (,) ': TyConsts_imported_by (Proxy (,))
38 type instance TyConsts_imported_by (Proxy (,)) =
39 [ Proxy Applicative
40 , Proxy Bounded
41 , Proxy Eq
42 , Proxy Foldable
43 , Proxy Functor
44 , Proxy Monad
45 , Proxy MT.MonoFoldable
46 , Proxy MT.MonoFunctor
47 , Proxy Monoid
48 , Proxy Ord
49 , Proxy Show
50 , Proxy Traversable
51 ]
52
53 instance Sym_Tuple2 HostI where
54 tuple2 = liftM2 (,)
55 fst = liftM Tuple.fst
56 snd = liftM Tuple.snd
57 instance Sym_Tuple2 TextI where
58 tuple2 (TextI a) (TextI b) =
59 TextI $ \_po v ->
60 "(" <> a (op, L) v <> ", " <> b (op, R) v <> ")"
61 where op = infixN 0
62 fst = textI1 "fst"
63 snd = textI1 "snd"
64 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
65 tuple2 = dupI2 @Sym_Tuple2 tuple2
66 fst = dupI1 @Sym_Tuple2 fst
67 snd = dupI1 @Sym_Tuple2 snd
68
69 instance
70 ( Read_TyNameR TyName cs rs
71 , Inj_TyConst cs (,)
72 ) => Read_TyNameR TyName cs (Proxy (,) ': rs) where
73 read_TyNameR _cs (TyName "(,)") k = k (ty @(,))
74 read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
75 instance Show_TyConst cs => Show_TyConst (Proxy (,) ': cs) where
76 show_TyConst TyConstZ{} = "(,)"
77 show_TyConst (TyConstS c) = show_TyConst c
78
79 instance -- Proj_TyFamC TyFam_MonoElement
80 ( Proj_TyConst cs (,)
81 ) => Proj_TyFamC cs TyFam_MonoElement (,) where
82 proj_TyFamC _c _fam ((TyConst c :$ _ty_a :$ ty_b) `TypesS` TypesZ)
83 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
84 , Just Refl <- proj_TyConst c (Proxy @(,))
85 = Just ty_b
86 proj_TyFamC _c _fam _ty = Nothing
87
88 instance -- Proj_TyConC
89 ( Proj_TyConst cs (,)
90 , Proj_TyConsts cs (TyConsts_imported_by (Proxy (,)))
91 , Proj_TyCon cs
92 , Inj_TyConst cs Monoid
93 ) => Proj_TyConC cs (Proxy (,)) where
94 proj_TyConC _ (TyConst q :$ (TyConst c :$ a))
95 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
96 , Just Refl <- proj_TyConst c (Proxy @(,))
97 = case () of
98 _ | Just Refl <- proj_TyConst q (Proxy @Applicative)
99 , Just TyCon <- proj_TyCon (ty @Monoid :$ a) -> Just TyCon
100 | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
101 | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
102 | Just Refl <- proj_TyConst q (Proxy @Monad)
103 , Just TyCon <- proj_TyCon (ty @Monoid :$ a) -> Just TyCon
104 | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
105 _ -> Nothing
106 proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
107 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
108 , Just Refl <- proj_TyConst c (Proxy @(,))
109 = case () of
110 _ | Just Refl <- proj_TyConst q (Proxy @Bounded)
111 , Just TyCon <- proj_TyCon (t :$ a)
112 , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
113 | Just Refl <- proj_TyConst q (Proxy @Eq)
114 , Just TyCon <- proj_TyCon (t :$ a)
115 , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
116 | Just Refl <- proj_TyConst q (Proxy @Monoid)
117 , Just TyCon <- proj_TyCon (t :$ a)
118 , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
119 | Just Refl <- proj_TyConst q (Proxy @Ord)
120 , Just TyCon <- proj_TyCon (t :$ a)
121 , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
122 | Just Refl <- proj_TyConst q (Proxy @Show)
123 , Just TyCon <- proj_TyCon (t :$ a)
124 , Just TyCon <- proj_TyCon (t :$ b) -> Just TyCon
125 | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable) -> Just TyCon
126 | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor) -> Just TyCon
127 _ -> Nothing
128 proj_TyConC _c _q = Nothing
129 data instance TokenT meta (ts::[*]) (Proxy (,))
130 = Token_Term_Tuple2 (EToken meta ts) (EToken meta ts)
131 | Token_Term_Tuple2_fst (EToken meta ts)
132 | Token_Term_Tuple2_snd (EToken meta ts)
133 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy (,)))
134 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy (,)))
135
136 instance -- CompileI
137 ( Inj_TyConst cs (,)
138 , Compile cs is
139 ) => CompileI cs is (Proxy (,)) where
140 compileI tok ctx k =
141 case tok of
142 Token_Term_Tuple2 tok_a tok_b ->
143 -- (,) :: a -> b -> (a, b)
144 compile tok_a ctx $ \ty_a (Term a) ->
145 compile tok_b ctx $ \ty_b (Term b) ->
146 k (ty @(,) :$ ty_a :$ ty_b) $ Term $
147 \c -> tuple2 (a c) (b c)
148 Token_Term_Tuple2_fst tok_ab ->
149 -- fst :: (a, b) -> a
150 compile tok_ab ctx $ \ty_ab (Term ab) ->
151 check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
152 k ty_a $ Term $
153 \c -> fst (ab c)
154 Token_Term_Tuple2_snd tok_ab ->
155 -- snd :: (a, b) -> b
156 compile tok_ab ctx $ \ty_ab (Term ab) ->
157 check_TyEq2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
158 k ty_b $ Term $
159 \c -> snd (ab c)
160 instance -- TokenizeT
161 Inj_Token meta ts (,) =>
162 TokenizeT meta ts (Proxy (,)) where
163 tokenizeT _t = mempty
164 { tokenizers_infix = tokenizeTMod []
165 [ tokenize1 "fst" infixN5 Token_Term_Tuple2_fst
166 , tokenize1 "snd" infixN5 Token_Term_Tuple2_snd
167 ]
168 }
169 instance -- Gram_Term_AtomsT
170 ( Alt g
171 , Gram_Rule g
172 , Gram_Lexer g
173 , Gram_Meta meta g
174 , Gram_Term ts meta g
175 , Inj_Token meta ts (->)
176 , Inj_Token meta ts (,)
177 ) => Gram_Term_AtomsT meta ts (Proxy (,)) g where
178 gs_term_atomsT _t =
179 [ rule "term_tuple2" $
180 metaG $ parens $
181 (\a b meta -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
182 <$> g_term
183 <* symbol ","
184 <*> g_term
185 , rule "term_tuple2" $
186 metaG $
187 (\meta -> ProTokLam $ \a -> ProTokLam $ \b -> ProTok $ inj_EToken meta $ Token_Term_Tuple2 a b)
188 <$ symbol "(,)"
189 ]