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
7 import Control.Monad (liftM, liftM2)
8 import Data.Monoid ((<>))
10 import qualified Data.Tuple as Tuple
11 import Data.Type.Equality ((:~:)(Refl))
12 import Prelude hiding (fst, snd)
14 import Language.Symantic.Parsing
15 import Language.Symantic.Typing
16 import Language.Symantic.Compiling
17 import Language.Symantic.Interpreting
18 import Language.Symantic.Transforming
20 -- * Class 'Sym_Tuple2'
21 class Sym_Tuple2 term where
22 tuple2 :: term a -> term b -> term (a, b)
23 fst :: term (a, b) -> term a
24 snd :: term (a, b) -> term b
26 default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
27 default fst :: Trans t term => t term (a, b) -> t term a
28 default snd :: Trans t term => t term (a, b) -> t term b
30 tuple2 = trans_map2 tuple2
34 type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
35 type instance Consts_of_Iface (Proxy (,)) = Proxy (,) ': Consts_imported_by (,)
36 type instance Consts_imported_by (,) =
49 instance Sym_Tuple2 HostI where
53 instance Sym_Tuple2 TextI where
54 tuple2 (TextI a) (TextI b) =
56 "(" <> a (op, L) v <> ", " <> b (op, R) v <> ")"
60 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
61 tuple2 = dupI2 (Proxy @Sym_Tuple2) tuple2
62 fst = dupI1 (Proxy @Sym_Tuple2) fst
63 snd = dupI1 (Proxy @Sym_Tuple2) snd
66 ( Read_TypeNameR Type_Name cs rs
68 ) => Read_TypeNameR Type_Name cs (Proxy (,) ': rs) where
69 read_typenameR _cs (Type_Name "(,)") k = k (ty @(,))
70 read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
71 instance Show_Const cs => Show_Const (Proxy (,) ': cs) where
72 show_const ConstZ{} = "(,)"
73 show_const (ConstS c) = show_const c
77 , Proj_Consts cs (Consts_imported_by (,))
80 ) => Proj_ConC cs (Proxy (,)) where
81 proj_conC _ (TyConst q :$ (TyConst c :$ a))
82 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
83 , Just Refl <- proj_const c (Proxy @(,))
85 _ | Just Refl <- proj_const q (Proxy @Applicative)
86 , Just Con <- proj_con (ty @Monoid :$ a) -> Just Con
87 | Just Refl <- proj_const q (Proxy @Functor) -> Just Con
88 | Just Refl <- proj_const q (Proxy @Foldable) -> Just Con
89 | Just Refl <- proj_const q (Proxy @Monad)
90 , Just Con <- proj_con (ty @Monoid :$ a) -> Just Con
91 | Just Refl <- proj_const q (Proxy @Traversable) -> Just Con
93 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
94 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
95 , Just Refl <- proj_const c (Proxy @(,))
97 _ | Just Refl <- proj_const q (Proxy @Bounded)
98 , Just Con <- proj_con (t :$ a)
99 , Just Con <- proj_con (t :$ b) -> Just Con
100 | Just Refl <- proj_const q (Proxy @Eq)
101 , Just Con <- proj_con (t :$ a)
102 , Just Con <- proj_con (t :$ b) -> Just Con
103 | Just Refl <- proj_const q (Proxy @Monoid)
104 , Just Con <- proj_con (t :$ a)
105 , Just Con <- proj_con (t :$ b) -> Just Con
106 | Just Refl <- proj_const q (Proxy @Ord)
107 , Just Con <- proj_con (t :$ a)
108 , Just Con <- proj_con (t :$ b) -> Just Con
109 | Just Refl <- proj_const q (Proxy @Show)
110 , Just Con <- proj_con (t :$ a)
111 , Just Con <- proj_con (t :$ b) -> Just Con
113 proj_conC _c _q = Nothing
114 data instance TokenT meta (ts::[*]) (Proxy (,))
115 = Token_Term_Tuple2 (EToken meta ts) (EToken meta ts)
116 | Token_Term_Tuple2_fst (EToken meta ts)
117 | Token_Term_Tuple2_snd (EToken meta ts)
118 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy (,)))
119 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy (,)))
121 ( Inj_Const (Consts_of_Ifaces is) (,)
123 ) => CompileI is (Proxy (,)) where
126 Token_Term_Tuple2 tok_a tok_b ->
127 -- (,) :: a -> b -> (a, b)
128 compileO tok_a ctx $ \ty_a (TermO a) ->
129 compileO tok_b ctx $ \ty_b (TermO b) ->
130 k (ty @(,) :$ ty_a :$ ty_b) $ TermO $
131 \c -> tuple2 (a c) (b c)
132 Token_Term_Tuple2_fst tok_ab ->
133 -- fst :: (a, b) -> a
134 compileO tok_ab ctx $ \ty_ab (TermO ab) ->
135 check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
138 Token_Term_Tuple2_snd tok_ab ->
139 -- snd :: (a, b) -> b
140 compileO tok_ab ctx $ \ty_ab (TermO ab) ->
141 check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
144 instance -- TokenizeT
145 Inj_Token meta ts (,) =>
146 TokenizeT meta ts (Proxy (,)) where
147 tokenizeT _t = mempty
148 { tokenizers_infix = tokenizeTMod []
149 [ tokenize1 "fst" infixN5 Token_Term_Tuple2_fst
150 , tokenize1 "snd" infixN5 Token_Term_Tuple2_snd
153 instance -- Gram_Term_AtomsT
158 , Gram_Term ts meta g
159 , Inj_Token meta ts (->)
160 , Inj_Token meta ts (,)
161 ) => Gram_Term_AtomsT meta ts (Proxy (,)) g where
163 [ rule "term_tuple2" $
165 (\a b meta -> ProTok $ inj_etoken meta $ Token_Term_Tuple2 a b)
169 , rule "term_tuple2" $
171 (\meta -> ProTokLam $ \a -> ProTokLam $ \b -> ProTok $ inj_etoken meta $ Token_Term_Tuple2 a b)