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