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