]> Git — Sourcephile - haskell/symantic.git/blob - Language/Symantic/Compiling/Tuple2.hs
Add tests for Compiling.
[haskell/symantic.git] / Language / Symantic / Compiling / Tuple2.hs
1 {-# LANGUAGE DataKinds #-}
2 {-# LANGUAGE DefaultSignatures #-}
3 {-# LANGUAGE FlexibleContexts #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE MultiParamTypeClasses #-}
6 {-# LANGUAGE OverloadedStrings #-}
7 {-# LANGUAGE Rank2Types #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE TypeFamilies #-}
10 {-# LANGUAGE TypeOperators #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# OPTIONS_GHC -fno-warn-orphans #-}
13 {-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-}
14 -- | Symantic for @(,)@.
15 module Language.Symantic.Compiling.Tuple2 where
16
17 import Control.Monad (liftM, liftM2)
18 import Data.Monoid ((<>))
19 import Data.Proxy
20 import Data.String (IsString)
21 import Data.Text (Text)
22 import qualified Data.Tuple as Tuple
23 import Data.Type.Equality ((:~:)(Refl))
24 import Prelude hiding (fst, snd)
25
26 import Language.Symantic.Typing
27 import Language.Symantic.Compiling.Term
28 import Language.Symantic.Compiling.Monoid (tyMonoid)
29 import Language.Symantic.Interpreting
30 import Language.Symantic.Transforming.Trans
31
32 -- * Class 'Sym_Tuple2'
33 class Sym_Tuple2 term where
34 tuple2 :: term a -> term b -> term (a, b)
35 fst :: term (a, b) -> term a
36 snd :: term (a, b) -> term b
37
38 default tuple2 :: Trans t term => t term a -> t term b -> t term (a, b)
39 default fst :: Trans t term => t term (a, b) -> t term a
40 default snd :: Trans t term => t term (a, b) -> t term b
41
42 tuple2 = trans_map2 tuple2
43 fst = trans_map1 fst
44 snd = trans_map1 snd
45
46 type instance Sym_of_Iface (Proxy (,)) = Sym_Tuple2
47 type instance Consts_of_Iface (Proxy (,)) = Proxy (,) ': Consts_imported_by (,)
48 type instance Consts_imported_by (,) =
49 [ Proxy Applicative
50 , Proxy Bounded
51 , Proxy Eq
52 , Proxy Foldable
53 , Proxy Functor
54 , Proxy Monad
55 , Proxy Monoid
56 , Proxy Ord
57 , Proxy Traversable
58 ]
59
60 instance Sym_Tuple2 HostI where
61 tuple2 = liftM2 (,)
62 fst = liftM Tuple.fst
63 snd = liftM Tuple.snd
64 instance Sym_Tuple2 TextI where
65 tuple2 (TextI a) (TextI b) =
66 TextI $ \_p v ->
67 let p' = precedence_Toplevel in
68 "(" <> a p' v <> ", " <> b p' v <> ")"
69 fst = textI_app1 "fst"
70 snd = textI_app1 "snd"
71 instance (Sym_Tuple2 r1, Sym_Tuple2 r2) => Sym_Tuple2 (DupI r1 r2) where
72 tuple2 = dupI2 sym_Tuple2 tuple2
73 fst = dupI1 sym_Tuple2 fst
74 snd = dupI1 sym_Tuple2 snd
75
76 instance Const_from Text cs => Const_from Text (Proxy (,) ': cs) where
77 const_from "(,)" k = k (ConstZ kind)
78 const_from s k = const_from s $ k . ConstS
79 instance Show_Const cs => Show_Const (Proxy (,) ': cs) where
80 show_const ConstZ{} = "(,)"
81 show_const (ConstS c) = show_const c
82
83 instance -- Proj_ConC
84 ( Proj_Const cs (,)
85 , Proj_Consts cs (Consts_imported_by (,))
86 , Proj_Con cs
87 , Inj_Const cs Monoid
88 ) => Proj_ConC cs (Proxy (,)) where
89 proj_conC _ (TyConst q :$ (TyConst c :$ a))
90 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
91 , Just Refl <- proj_const c (Proxy::Proxy (,))
92 = Just $ case () of
93 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative)
94 , Just Con <- proj_con (tyMonoid :$ a) -> Just Con
95 | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con
96 | Just Refl <- proj_const q (Proxy::Proxy Foldable) -> Just Con
97 | Just Refl <- proj_const q (Proxy::Proxy Monad)
98 , Just Con <- proj_con (tyMonoid :$ a) -> Just Con
99 | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
100 _ -> Nothing
101 proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a :$ b))
102 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
103 , Just Refl <- proj_const c (Proxy::Proxy (,))
104 = Just $ case () of
105 _ | Just Refl <- proj_const q (Proxy::Proxy Bounded)
106 , Just Con <- proj_con (t :$ a)
107 , Just Con <- proj_con (t :$ b) -> Just Con
108 | Just Refl <- proj_const q (Proxy::Proxy Eq)
109 , Just Con <- proj_con (t :$ a)
110 , Just Con <- proj_con (t :$ b) -> Just Con
111 | Just Refl <- proj_const q (Proxy::Proxy Monoid)
112 , Just Con <- proj_con (t :$ a)
113 , Just Con <- proj_con (t :$ b) -> Just Con
114 | Just Refl <- proj_const q (Proxy::Proxy Ord)
115 , Just Con <- proj_con (t :$ a)
116 , Just Con <- proj_con (t :$ b) -> Just Con
117 _ -> Nothing
118 proj_conC _c _q = Nothing
119 instance -- Term_fromI
120 ( AST ast
121 , Lexem ast ~ LamVarName
122 , Inj_Const (Consts_of_Ifaces is) (,)
123 , Term_from is ast
124 ) => Term_fromI is (Proxy (,)) ast where
125 term_fromI ast ctx k =
126 case ast_lexem ast of
127 "(,)" -> tuple2_from
128 "fst" -> fst_from
129 "snd" -> snd_from
130 _ -> Left $ Error_Term_unsupported
131 where
132 tuple2_from =
133 -- (,) :: a -> b -> (a, b)
134 from_ast2 ast $ \ast_a ast_b as ->
135 term_from ast_a ctx $ \ty_a (TermLC a) ->
136 term_from ast_b ctx $ \ty_b (TermLC b) ->
137 k as (tyTuple2 :$ ty_a :$ ty_b) $ TermLC $
138 \c -> tuple2 (a c) (b c)
139 fst_from =
140 -- fst :: (a, b) -> a
141 from_ast1 ast $ \ast_ab as ->
142 term_from ast_ab ctx $ \ty_ab (TermLC ab) ->
143 check_type2 tyTuple2 ast_ab ty_ab $ \Refl ty_a _ty_b ->
144 k as ty_a $ TermLC $
145 \c -> fst (ab c)
146 snd_from =
147 -- snd :: (a, b) -> b
148 from_ast1 ast $ \ast_ab as ->
149 term_from ast_ab ctx $ \ty_ab (TermLC ab) ->
150 check_type2 tyTuple2 ast_ab ty_ab $ \Refl _ty_a ty_b ->
151 k as ty_b $ TermLC $
152 \c -> snd (ab c)
153
154 -- | The '(,)' 'Type'
155 tyTuple2 :: Inj_Const cs (,) => Type cs (,)
156 tyTuple2 = TyConst inj_const
157
158 sym_Tuple2 :: Proxy Sym_Tuple2
159 sym_Tuple2 = Proxy
160
161 syTuple2 :: IsString a => [Syntax a] -> Syntax a
162 syTuple2 = Syntax "(,)"