]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/Map.hs
Support GHC-8.4.3.
[haskell/symantic.git] / symantic-lib / Language / Symantic / Lib / Map.hs
1 {-# LANGUAGE UndecidableInstances #-}
2 {-# OPTIONS_GHC -fno-warn-orphans #-}
3 -- | Symantic for 'Map'.
4 module Language.Symantic.Lib.Map where
5
6 import Data.Bool
7 import Data.Eq (Eq)
8 import Data.Foldable (Foldable)
9 import Data.Function (($))
10 import Data.Functor (Functor)
11 import Data.Map.Strict (Map)
12 import Data.Maybe (Maybe(..))
13 import Data.MonoTraversable (MonoFunctor)
14 import Data.Monoid (Monoid)
15 import Data.Ord (Ord)
16 import Data.Traversable (Traversable)
17 import Text.Show (Show)
18 import qualified Data.Map.Strict as Map
19
20 import Language.Symantic
21 import Language.Symantic.Lib.Bool (tyBool)
22 import Language.Symantic.Lib.Function (a0, b1)
23 import Language.Symantic.Lib.List (tyList)
24 import Language.Symantic.Lib.Maybe (tyMaybe)
25 import Language.Symantic.Lib.MonoFunctor (Element)
26 import Language.Symantic.Lib.Ord (tyOrd)
27 import Language.Symantic.Lib.Tuple2 (tyTuple2)
28
29 -- * Class 'Sym_Map'
30 type instance Sym Map = Sym_Map
31 class Sym_Map term where
32 map_fromList :: Ord k => term [(k, a)] -> term (Map k a)
33 map_mapWithKey :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
34 map_lookup :: Ord k => term k -> term (Map k a) -> term (Maybe a)
35 map_keys :: term (Map k a) -> term [k]
36 map_member :: Ord k => term k -> term (Map k a) -> term Bool
37 map_insert :: Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
38 map_delete :: Ord k => term k -> term (Map k a) -> term (Map k a)
39 map_difference :: Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
40 map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
41
42 default map_fromList :: Sym_Map (UnT term) => Trans term => Ord k => term [(k, a)] -> term (Map k a)
43 default map_mapWithKey :: Sym_Map (UnT term) => Trans term => term (k -> a -> b) -> term (Map k a) -> term (Map k b)
44 default map_lookup :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Maybe a)
45 default map_keys :: Sym_Map (UnT term) => Trans term => term (Map k a) -> term [k]
46 default map_member :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term Bool
47 default map_insert :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
48 default map_delete :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Map k a)
49 default map_difference :: Sym_Map (UnT term) => Trans term => Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
50 default map_foldrWithKey :: Sym_Map (UnT term) => Trans term => term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
51
52 map_fromList = trans1 map_fromList
53 map_mapWithKey = trans2 map_mapWithKey
54 map_lookup = trans2 map_lookup
55 map_keys = trans1 map_keys
56 map_member = trans2 map_member
57 map_insert = trans3 map_insert
58 map_delete = trans2 map_delete
59 map_difference = trans2 map_difference
60 map_foldrWithKey = trans3 map_foldrWithKey
61
62 -- Interpreting
63 instance Sym_Map Eval where
64 map_fromList = eval1 Map.fromList
65 map_mapWithKey = eval2 Map.mapWithKey
66 map_lookup = eval2 Map.lookup
67 map_keys = eval1 Map.keys
68 map_member = eval2 Map.member
69 map_insert = eval3 Map.insert
70 map_delete = eval2 Map.delete
71 map_difference = eval2 Map.difference
72 map_foldrWithKey = eval3 Map.foldrWithKey
73 instance Sym_Map View where
74 map_fromList = view1 "Map.fromList"
75 map_mapWithKey = view2 "Map.mapWithKey"
76 map_lookup = view2 "Map.lookup"
77 map_keys = view1 "Map.keys"
78 map_member = view2 "Map.member"
79 map_insert = view3 "Map.insert"
80 map_delete = view2 "Map.delete"
81 map_difference = view2 "Map.difference"
82 map_foldrWithKey = view3 "Map.foldrWithKey"
83 instance (Sym_Map r1, Sym_Map r2) => Sym_Map (Dup r1 r2) where
84 map_fromList = dup1 @Sym_Map map_fromList
85 map_mapWithKey = dup2 @Sym_Map map_mapWithKey
86 map_lookup = dup2 @Sym_Map map_lookup
87 map_keys = dup1 @Sym_Map map_keys
88 map_member = dup2 @Sym_Map map_member
89 map_insert = dup3 @Sym_Map map_insert
90 map_delete = dup2 @Sym_Map map_delete
91 map_difference = dup2 @Sym_Map map_difference
92 map_foldrWithKey = dup3 @Sym_Map map_foldrWithKey
93
94 -- Transforming
95 instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)
96
97 -- Typing
98 instance NameTyOf Map where
99 nameTyOf _c = ["Map"] `Mod` "Map"
100 instance FixityOf Map
101 instance ClassInstancesFor Map where
102 proveConstraintFor _ (TyConst _ _ q :$ m:@_k)
103 | Just HRefl <- proj_ConstKiTy @_ @Map m
104 = case () of
105 _ | Just Refl <- proj_Const @Functor q -> Just Dict
106 | Just Refl <- proj_Const @Foldable q -> Just Dict
107 | Just Refl <- proj_Const @Traversable q -> Just Dict
108 _ -> Nothing
109 proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@k:@a)
110 | Just HRefl <- proj_ConstKiTy @_ @Map m
111 = case () of
112 _ | Just Refl <- proj_Const @Eq q
113 , Just Dict <- proveConstraint (tq`tyApp`k)
114 , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
115 | Just Refl <- proj_Const @Ord q
116 , Just Dict <- proveConstraint (tq`tyApp`k)
117 , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
118 | Just Refl <- proj_Const @Monoid q
119 , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict
120 | Just Refl <- proj_Const @Show q
121 , Just Dict <- proveConstraint (tq`tyApp`k)
122 , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
123 | Just Refl <- proj_Const @MonoFunctor q -> Just Dict
124 _ -> Nothing
125 proveConstraintFor _c _q = Nothing
126 instance TypeInstancesFor Map where
127 expandFamFor _c _len f (m:@_k:@a `TypesS` TypesZ)
128 | Just HRefl <- proj_ConstKi @_ @Element f
129 , Just HRefl <- proj_ConstKiTy @_ @Map m
130 = Just a
131 expandFamFor _c _len _fam _as = Nothing
132
133 -- Compiling
134 instance Gram_Term_AtomsFor src ss g Map
135 instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
136 moduleFor = ["Map"] `moduleWhere`
137 [ "delete" := teMap_delete
138 , "difference" := teMap_difference
139 , "foldrWithKey" := teMap_foldrWithKey
140 , "fromList" := teMap_fromList
141 , "insert" := teMap_insert
142 , "keys" := teMap_keys
143 , "lookup" := teMap_lookup
144 , "mapWithKey" := teMap_mapWithKey
145 , "member" := teMap_member
146 ]
147
148 -- ** 'Type's
149 tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
150 tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a
151
152 k1 :: Source src => LenInj vs => KindInj (K k) =>
153 Type src (a ': Proxy k ': vs) k
154 k1 = tyVar "k" $ VarS varZ
155
156 k2 :: Source src => LenInj vs => KindInj (K k) =>
157 Type src (a ': b ': Proxy k ': vs) k
158 k2 = tyVar "k" $ VarS $ VarS varZ
159
160 -- ** 'Term's
161 teMap_delete :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Map k a))
162 teMap_delete = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam2 map_delete
163
164 teMap_insert :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> a -> Map k a -> Map k a))
165 teMap_insert = Term (tyOrd k1) (k1 ~> a0 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam3 map_insert
166
167 teMap_difference :: TermDef Map '[Proxy a, Proxy b, Proxy k] (Ord k #> (Map k a -> Map k b -> Map k a))
168 teMap_difference = Term (tyOrd k2) (tyMap k2 a0 ~> tyMap k2 b1 ~> tyMap k2 a0) $ teSym @Map $ lam2 map_difference
169
170 teMap_fromList :: TermDef Map '[Proxy a, Proxy k] (Ord k #> ([(k, a)] -> Map k a))
171 teMap_fromList = Term (tyOrd k1) (tyList (tyTuple2 k1 a0) ~> tyMap k1 a0) $ teSym @Map $ lam1 map_fromList
172
173 teMap_lookup :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Maybe a))
174 teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $ lam2 map_lookup
175
176 teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))
177 teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member
178
179 teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))
180 teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey
181
182 teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))
183 teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey
184
185 teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))
186 teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys