]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Tuple2.hs
Clarify names, and add commentaries (bis).
[haskell/symantic.git] / Language / Symantic / Compiling / 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.Compiling.Tuple2 where
6
7 import Control.Monad (liftM, liftM2)
8 import Data.Monoid ((<>))
9 import Data.Proxy
10 import Data.Text (Text)
11 import qualified Data.Tuple as Tuple
12 import Data.Type.Equality ((:~:)(Refl))
13 import Prelude hiding (fst, snd)
14
15 import Language.Symantic.Parsing
16 import Language.Symantic.Typing
17 import Language.Symantic.Compiling.Term
18 import Language.Symantic.Interpreting
19 import Language.Symantic.Transforming.Trans
20
21 -- * Class 'Sym_Tuple2'
22 class Sym_Tuple2 term where
23 tuple2 :: term a -> term b -> term (a, b)
24 fst :: term (a, b) -> term a
25 snd :: term (a, b) -> term b
26
27 default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
28 default fst :: Trans t term => t term (a, b) -> t term a
29 default snd :: Trans t term => t term (a, b) -> t term b
30
31 tuple2 = trans_map2 tuple2
32 fst = trans_map1 fst
33 snd = trans_map1 snd
34
35 type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
36 type instance Consts_of_Iface (Proxy (,)) = Proxy (,) ': Consts_imported_by (,)
37 type instance Consts_imported_by (,) =
38 [ Proxy Applicative
39 , Proxy Bounded
40 , Proxy Eq
41 , Proxy Foldable
42 , Proxy Functor
43 , Proxy Monad
44 , Proxy Monoid
45 , Proxy Ord
46 , Proxy Show
47 , Proxy Traversable
48 ]
49
50 instance Sym_Tuple2 HostI where
51 tuple2 = liftM2 (,)
52 fst = liftM Tuple.fst
53 snd = liftM Tuple.snd
54 instance Sym_Tuple2 TextI where
55 tuple2 (TextI a) (TextI b) =
56 TextI $ \_p v ->
57 let p' = precedence_Toplevel in
58 "(" <> a p' v <> ", " <> b p' v <> ")"
59 fst = textI_app1 "fst"
60 snd = textI_app1 "snd"
61 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
62 tuple2 = dupI2 (Proxy @Sym_Tuple2) tuple2
63 fst = dupI1 (Proxy @Sym_Tuple2) fst
64 snd = dupI1 (Proxy @Sym_Tuple2) snd
65
66 instance Const_from Text cs => Const_from Text (Proxy (,) ': cs) where
67 const_from "(,)" k = k (ConstZ kind)
68 const_from s k = const_from s $ k . ConstS
69 instance Show_Const cs => Show_Const (Proxy (,) ': cs) where
70 show_const ConstZ{} = "(,)"
71 show_const (ConstS c) = show_const c
72
73 instance -- Proj_ConC
74 ( Proj_Const cs (,)
75 , Proj_Consts cs (Consts_imported_by (,))
76 , Proj_Con cs
77 , Inj_Const cs Monoid
78 ) => Proj_ConC cs (Proxy (,)) where
79 proj_conC _ (TyConst q :$ (TyConst c :$ a))
80 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
81 , Just Refl <- proj_const c (Proxy::Proxy (,))
82 = case () of
83 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative)
84 , Just Con <- proj_con (ty @Monoid :$ a) -> Just Con
85 | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con
86 | Just Refl <- proj_const q (Proxy::Proxy Foldable) -> Just Con
87 | Just Refl <- proj_const q (Proxy::Proxy Monad)
88 , Just Con <- proj_con (ty @Monoid :$ a) -> Just Con
89 | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
90 _ -> Nothing
91 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
92 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
93 , Just Refl <- proj_const c (Proxy::Proxy (,))
94 = case () of
95 _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)
96 , Just Con <- proj_con (t :$ a)
97 , Just Con <- proj_con (t :$ b) -> Just Con
98 | Just Refl <- proj_const q (Proxy::Proxy Eq)
99 , Just Con <- proj_con (t :$ a)
100 , Just Con <- proj_con (t :$ b) -> Just Con
101 | Just Refl <- proj_const q (Proxy::Proxy Monoid)
102 , Just Con <- proj_con (t :$ a)
103 , Just Con <- proj_con (t :$ b) -> Just Con
104 | Just Refl <- proj_const q (Proxy::Proxy Ord)
105 , Just Con <- proj_con (t :$ a)
106 , Just Con <- proj_con (t :$ b) -> Just Con
107 | Just Refl <- proj_const q (Proxy::Proxy Show)
108 , Just Con <- proj_con (t :$ a)
109 , Just Con <- proj_con (t :$ b) -> Just Con
110 _ -> Nothing
111 proj_conC _c _q = Nothing
112 data instance TokenT meta (ts::[*]) (Proxy (,))
113 = Token_Term_Tuple2 (EToken meta ts) (EToken meta ts)
114 | Token_Term_Tuple2_fst (EToken meta ts)
115 | Token_Term_Tuple2_snd (EToken meta ts)
116 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy (,)))
117 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy (,)))
118 instance -- CompileI
119 ( Inj_Const (Consts_of_Ifaces is) (,)
120 , Compile is
121 ) => CompileI is (Proxy (,)) where
122 compileI tok ctx k =
123 case tok of
124 Token_Term_Tuple2 tok_a tok_b ->
125 -- (,) :: a -> b -> (a, b)
126 compileO tok_a ctx $ \ty_a (TermO a) ->
127 compileO tok_b ctx $ \ty_b (TermO b) ->
128 k (ty @(,) :$ ty_a :$ ty_b) $ TermO $
129 \c -> tuple2 (a c) (b c)
130 Token_Term_Tuple2_fst tok_ab ->
131 -- fst :: (a, b) -> a
132 compileO tok_ab ctx $ \ty_ab (TermO ab) ->
133 check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl ty_a _ty_b ->
134 k ty_a $ TermO $
135 \c -> fst (ab c)
136 Token_Term_Tuple2_snd tok_ab ->
137 -- snd :: (a, b) -> b
138 compileO tok_ab ctx $ \ty_ab (TermO ab) ->
139 check_type2 (ty @(,)) (At (Just tok_ab) ty_ab) $ \Refl _ty_a ty_b ->
140 k ty_b $ TermO $
141 \c -> snd (ab c)