]> Git — Sourcephile - haskell/symantic.git/blob - symantic/Language/Symantic/Typing/Constant.hs
Backtrack (try) the grammar only when necessary to get better error messages.
[haskell/symantic.git] / symantic / Language / Symantic / Typing / Constant.hs
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE TypeInType #-}
4 module Language.Symantic.Typing.Constant where
5
6 import qualified Data.Kind as Kind
7 import qualified Data.Map.Strict as Map
8 import qualified Data.MonoTraversable as MT
9 import qualified Data.Sequences as Seqs
10 import Data.NonNull (NonNull)
11 import Data.Proxy
12 import Data.Text (Text)
13 import Data.Type.Equality
14 import qualified System.IO as IO
15
16 import Language.Symantic.Helper.Data.Type.List
17 import Language.Symantic.Helper.Data.Type.Peano
18 import Language.Symantic.Typing.Kind
19
20 -- * Type 'TyConst'
21 -- | A /type constant/,
22 -- indexed at the Haskell type and term level amongst a list of them.
23 -- When used, @c@ is actually wrapped within a 'Proxy'
24 -- to be able to handle constants of different 'Kind's.
25 data TyConst (cs::[Kind.Type]) (c::k) where
26 TyConstZ :: SKind k -> TyConst (Proxy c ': cs) (c::k)
27 TyConstS :: TyConst cs c -> TyConst (not_c ': cs) c
28 infixr 5 `TyConstS`
29
30 eq_Kind_TyConst :: TyConst cs (x::kx) -> TyConst cs (y::ky) -> Maybe (kx:~:ky)
31 eq_Kind_TyConst x y = eq_skind (kind_of_TyConst x) (kind_of_TyConst y)
32
33 instance TestEquality (TyConst cs) where
34 testEquality TyConstZ{} TyConstZ{} = Just Refl
35 testEquality (TyConstS x) (TyConstS y) = testEquality x y
36 testEquality _ _ = Nothing
37
38 kind_of_TyConst :: TyConst cs (h::k) -> SKind k
39 kind_of_TyConst (TyConstZ ki) = ki
40 kind_of_TyConst (TyConstS c) = kind_of_TyConst c
41
42 -- * Type 'Inj_TyConst'
43 -- | Convenient type synonym wrapping 'Inj_ConstP'
44 -- applied on the correct 'Index'.
45 type Inj_TyConst cs c = Inj_ConstP (Index cs (Proxy c)) cs c
46
47 -- | Inject a given /type constant/ @c@ into a list of them,
48 -- by returning a proof that 'Proxy'@ c@ is in @cs@.
49 inj_TyConst :: forall cs c. Inj_TyConst cs c => TyConst cs c
50 inj_TyConst = inj_TyConstP (Proxy @(Index cs (Proxy c)))
51
52 -- ** Class 'Inj_ConstP'
53 class Inj_ConstP p cs c where
54 inj_TyConstP :: Proxy p -> TyConst cs c
55 {- NOTE: using this commented instance fails very badly due to GHC-8.0.1's bug #12933
56 which makes it fail to calculate the right kind,
57 it seems to wrongly reuse the kind of the first use (sic)…
58 instance IKind k => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
59 inj_TyConstP _ = TyConstZ kind
60 -}
61 instance
62 ( IKindP (Ty_of_Type k)
63 , Type_of_Ty (Ty_of_Type k) ~ k
64 ) => Inj_ConstP Zero (Proxy c ': cs) (c::k) where
65 inj_TyConstP _ = TyConstZ (kindP (Proxy :: Proxy (Ty_of_Type k)))
66 instance Inj_ConstP p cs c => Inj_ConstP (Succ p) (not_c ': cs) c where
67 inj_TyConstP _p = TyConstS (inj_TyConstP (Proxy @p))
68
69 -- * Class 'Proj_TyConst'
70 -- | Convenient type synonym wrapping 'Proj_TyConstP'
71 -- applied on the correct 'Index'.
72 type Proj_TyConst cs c = Proj_TyConstP (Index cs (Proxy c)) cs c
73
74 -- | Project a 'TyConst' onto a Haskell type level /type constant/ @c@,
75 -- returning a proof that the 'TyConst' indexes @c@ iif. it's the case.
76 proj_TyConst :: forall cs k (c::k) (u::k).
77 Proj_TyConst cs c => TyConst cs u -> Proxy c -> Maybe (c :~: u)
78 proj_TyConst = proj_TyConstP (Proxy @(Index cs (Proxy c)))
79
80 (=?) :: forall cs c u. Proj_TyConst cs c => TyConst cs u -> Proxy c -> Maybe (c :~: u)
81 (=?) = proj_TyConstP (Proxy @(Index cs (Proxy c)))
82
83 -- ** Type 'Proj_TyConstP'
84 class Proj_TyConstP p cs c where
85 proj_TyConstP :: Proxy p -> TyConst cs u -> Proxy c -> Maybe (c :~: u)
86 instance Proj_TyConstP Zero (Proxy c ': cs) c where
87 proj_TyConstP _p TyConstZ{} _c = Just Refl
88 proj_TyConstP _p TyConstS{} _c = Nothing
89 instance Proj_TyConstP p cs c => Proj_TyConstP (Succ p) (not_c ': cs) c where
90 proj_TyConstP _p TyConstZ{} _c = Nothing
91 proj_TyConstP _p (TyConstS u) c = proj_TyConstP (Proxy @p) u c
92
93 -- ** Type 'Proj_TyConsts'
94 type Proj_TyConsts cs cs_to_proj
95 = Concat_Constraints (Proj_TyConstsR cs cs_to_proj)
96
97 -- *** Type family 'Proj_TyConstsR'
98 type family Proj_TyConstsR cs cs_to_proj where
99 Proj_TyConstsR cs '[] = '[]
100 Proj_TyConstsR cs (Proxy x ': xs) = Proj_TyConst cs x ': Proj_TyConstsR cs xs
101
102 -- * Class 'Show_TyConst'
103 class Show_TyConst cs where
104 show_TyConst :: TyConst cs c -> String
105
106 -- deriving instance Show (TyConst cs c)
107 instance Show_TyConst cs => Show (TyConst cs c) where
108 show = show_TyConst
109 instance Show_TyConst '[] where
110 show_TyConst = error "Show_TyConst unreachable pattern"
111
112 -- TODO: move each of these to a dedicated module.
113 instance Show_TyConst cs => Show_TyConst (Proxy Bounded ': cs) where
114 show_TyConst TyConstZ{} = "Bounded"
115 show_TyConst (TyConstS c) = show_TyConst c
116 instance Show_TyConst cs => Show_TyConst (Proxy Enum ': cs) where
117 show_TyConst TyConstZ{} = "Enum"
118 show_TyConst (TyConstS c) = show_TyConst c
119 instance Show_TyConst cs => Show_TyConst (Proxy Fractional ': cs) where
120 show_TyConst TyConstZ{} = "Fractional"
121 show_TyConst (TyConstS c) = show_TyConst c
122 instance Show_TyConst cs => Show_TyConst (Proxy Real ': cs) where
123 show_TyConst TyConstZ{} = "Real"
124 show_TyConst (TyConstS c) = show_TyConst c
125
126 -- * Type 'Constants'
127 -- | Usual 'TyConst's.
128 type Constants = Terms ++ Constraints
129
130 -- ** Type 'Terms'
131 -- | Usual 'TyConst's of /terms constructors/.
132 type Terms =
133 [ Proxy ()
134 , Proxy (,)
135 , Proxy (->)
136 , Proxy []
137 , Proxy Bool
138 , Proxy Char
139 , Proxy Either
140 , Proxy Int
141 , Proxy Integer
142 , Proxy Integral
143 , Proxy IO
144 , Proxy IO.Handle
145 , Proxy IO.IOMode
146 , Proxy Map.Map
147 , Proxy Maybe
148 , Proxy NonNull
149 , Proxy Text
150 ]
151
152 -- ** Type 'Constraints'
153 -- | Usual 'TyConst's of /type constraint constructors/.
154 type Constraints =
155 [ Proxy Applicative
156 , Proxy Bounded
157 , Proxy Enum
158 , Proxy Eq
159 , Proxy Foldable
160 , Proxy Functor
161 , Proxy Monad
162 , Proxy Monoid
163 , Proxy MT.MonoFoldable
164 , Proxy MT.MonoFunctor
165 , Proxy Num
166 , Proxy Ord
167 , Proxy Real
168 , Proxy Seqs.IsSequence
169 , Proxy Seqs.SemiSequence
170 , Proxy Show
171 , Proxy Traversable
172 ]