symantic-lib/Language/Symantic/Lib/Map.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=12 #-}
   4 -- | Symantic for 'Map'.
   5 module Language.Symantic.Lib.Map where
   6
   7 import Control.Monad (liftM, liftM2, liftM3)
   8 import Data.Map.Strict (Map)
   9 import Data.MonoTraversable (MonoFunctor)
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import Prelude hiding (either)
  13 import qualified Data.Map.Strict as Map
  14
  15 import Language.Symantic.Parsing
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming
  20 import Language.Symantic.Lib.Lambda
  21 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
  22
  23 -- * Class '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
  35         default map_fromList :: (Trans t term, Ord k) => t term [(k, a)] -> t term (Map k a)
  36         default map_mapWithKey :: Trans t term => t term (k -> a -> b) -> t term (Map k a) -> t term (Map k b)
  37         default map_lookup :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Maybe a)
  38         default map_keys :: Trans t term => t term (Map k a) -> t term [k]
  39         default map_member :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term Bool
  40         default map_insert :: (Trans t term, Ord k) => t term k -> t term a -> t term (Map k a) -> t term (Map k a)
  41         default map_delete :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Map k a)
  42         default map_difference :: (Trans t term, Ord k) => t term (Map k a) -> t term (Map k b) -> t term (Map k a)
  43         default map_foldrWithKey :: Trans t term => t term (k -> a -> b -> b) -> t term b -> t term (Map k a) -> t term b
  44
  45         map_fromList     = trans_map1 map_fromList
  46         map_mapWithKey   = trans_map2 map_mapWithKey
  47         map_lookup       = trans_map2 map_lookup
  48         map_keys         = trans_map1 map_keys
  49         map_member       = trans_map2 map_member
  50         map_insert       = trans_map3 map_insert
  51         map_delete       = trans_map2 map_delete
  52         map_difference   = trans_map2 map_difference
  53         map_foldrWithKey = trans_map3 map_foldrWithKey
  54
  55 type instance Sym_of_Iface (Proxy Map) = Sym_Map
  56 type instance TyConsts_of_Iface (Proxy Map) = Proxy Map ': TyConsts_imported_by (Proxy Map)
  57 type instance TyConsts_imported_by (Proxy Map) =
  58  [ Proxy (->)
  59  , Proxy []
  60  , Proxy (,)
  61  , Proxy Bool
  62  , Proxy Eq
  63  , Proxy Foldable
  64  , Proxy Functor
  65  , Proxy Maybe
  66  , Proxy Monad
  67  , Proxy MonoFunctor
  68  , Proxy Monoid
  69  , Proxy Ord
  70  , Proxy Traversable
  71  , Proxy Show
  72  ]
  73
  74 instance Sym_Map HostI where
  75         map_fromList     = liftM  Map.fromList
  76         map_mapWithKey   = liftM2 Map.mapWithKey
  77         map_lookup       = liftM2 Map.lookup
  78         map_keys         = liftM  Map.keys
  79         map_member       = liftM2 Map.member
  80         map_insert       = liftM3 Map.insert
  81         map_delete       = liftM2 Map.delete
  82         map_difference   = liftM2 Map.difference
  83         map_foldrWithKey = liftM3 Map.foldrWithKey
  84 instance Sym_Map TextI where
  85         map_fromList     = textI1 "Map.fromList"
  86         map_mapWithKey   = textI2 "Map.mapWithKey"
  87         map_lookup       = textI2 "Map.lookup"
  88         map_keys         = textI1 "Map.keys"
  89         map_member       = textI2 "Map.member"
  90         map_insert       = textI3 "Map.insert"
  91         map_delete       = textI2 "Map.delete"
  92         map_difference   = textI2 "Map.difference"
  93         map_foldrWithKey = textI3 "Map.foldrWithKey"
  94 instance (Sym_Map r1, Sym_Map r2) => Sym_Map (DupI r1 r2) where
  95         map_fromList     = dupI1 @Sym_Map map_fromList
  96         map_mapWithKey   = dupI2 @Sym_Map map_mapWithKey
  97         map_lookup       = dupI2 @Sym_Map map_lookup
  98         map_keys         = dupI1 @Sym_Map map_keys
  99         map_member       = dupI2 @Sym_Map map_member
 100         map_insert       = dupI3 @Sym_Map map_insert
 101         map_delete       = dupI2 @Sym_Map map_delete
 102         map_difference   = dupI2 @Sym_Map map_difference
 103         map_foldrWithKey = dupI3 @Sym_Map map_foldrWithKey
 104
 105 instance
 106  ( Read_TyNameR TyName cs rs
 107  , Inj_TyConst cs Map
 108  ) => Read_TyNameR TyName cs (Proxy Map ': rs) where
 109         read_TyNameR _cs (TyName "Map") k = k (ty @Map)
 110         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 111 instance Show_TyConst cs => Show_TyConst (Proxy Map ': cs) where
 112         show_TyConst TyConstZ{} = "Map"
 113         show_TyConst (TyConstS c) = show_TyConst c
 114
 115 instance -- Proj_TyFamC TyFam_MonoElement
 116  ( Proj_TyConst cs Map
 117  ) => Proj_TyFamC cs TyFam_MonoElement Map where
 118         proj_TyFamC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
 119          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 120          , Just Refl <- proj_TyConst c (Proxy @Map)
 121          = Just ty_a
 122         proj_TyFamC _c _fam _ty = Nothing
 123
 124 instance -- Proj_TyConC
 125  ( Proj_TyConst cs Map
 126  , Proj_TyConsts cs (TyConsts_imported_by (Proxy Map))
 127  , Proj_TyCon cs
 128  , Inj_TyConst cs Ord
 129  ) => Proj_TyConC cs (Proxy Map) where
 130         proj_TyConC _ (TyConst q :$ (TyConst c :$ _k))
 131          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 132          , Just Refl <- proj_TyConst c (Proxy @Map)
 133          = case () of
 134                  _ | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
 135                    | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
 136                    | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
 137                  _ -> Nothing
 138         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ k :$ a))
 139          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 140          , Just Refl <- proj_TyConst c (Proxy @Map)
 141          = case () of
 142                  _ | Just Refl <- proj_TyConst q (Proxy @Eq)
 143                    , Just TyCon  <- proj_TyCon (t :$ k)
 144                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 145                    | Just Refl <- proj_TyConst q (Proxy @Ord)
 146                    , Just TyCon  <- proj_TyCon (t :$ k)
 147                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 148                    | Just Refl <- proj_TyConst q (Proxy @Monoid)
 149                    , Just TyCon  <- proj_TyCon (ty @Ord :$ k) -> Just TyCon
 150                    | Just Refl <- proj_TyConst q (Proxy @Show)
 151                    , Just TyCon  <- proj_TyCon (t :$ k)
 152                    , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
 153                    | Just Refl <- proj_TyConst q (Proxy @MonoFunctor) -> Just TyCon
 154                  _ -> Nothing
 155         proj_TyConC _c _q = Nothing
 156 data instance TokenT meta (ts::[*]) (Proxy Map)
 157  = Token_Term_Map_fromList     (EToken meta ts)
 158  | Token_Term_Map_mapWithKey   (EToken meta ts)
 159  | Token_Term_Map_lookup       (EToken meta ts) (EToken meta ts)
 160  | Token_Term_Map_keys         (EToken meta ts)
 161  | Token_Term_Map_member       (EToken meta ts) (EToken meta ts)
 162  | Token_Term_Map_insert       (EToken meta ts) (EToken meta ts)
 163  | Token_Term_Map_delete       (EToken meta ts) (EToken meta ts)
 164  | Token_Term_Map_difference   (EToken meta ts) (EToken meta ts)
 165  | Token_Term_Map_foldrWithKey (EToken meta ts)
 166 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Map))
 167 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Map))
 168
 169 instance -- CompileI
 170  ( Inj_TyConst cs Map
 171  , Inj_TyConst cs (->)
 172  , Inj_TyConst cs Bool
 173  , Inj_TyConst cs Ord
 174  , Inj_TyConst cs Maybe
 175  , Inj_TyConst cs []
 176  , Inj_TyConst cs (,)
 177  , Proj_TyCon  cs
 178  , Compile cs is
 179  ) => CompileI cs is (Proxy Map) where
 180         compileI tok ctx k =
 181                 case tok of
 182                  Token_Term_Map_fromList tok_l ->
 183                         -- fromList :: Ord k => [(k, a)] -> Map k a
 184                         compile tok_l ctx $ \ty_l (Term l) ->
 185                         check_TyEq1 (ty @[]) (At (Just tok_l) ty_l) $ \Refl ty_l_t2 ->
 186                         check_TyEq2 (ty @(,)) (At (Just tok_l) ty_l_t2) $ \Refl ty_k ty_a ->
 187                         check_TyCon (At (Just tok_l) (ty @Ord :$ ty_k)) $ \TyCon ->
 188                         k ((ty @Map :$ ty_k) :$ ty_a) $ Term $
 189                          \c -> map_fromList (l c)
 190                  Token_Term_Map_mapWithKey tok_k2a2b ->
 191                         -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
 192                         compile tok_k2a2b ctx $ \ty_k2a2b (Term k2a2b) ->
 193                         check_TyEq2 (ty @(->)) (At (Just tok_k2a2b) ty_k2a2b) $ \Refl ty_k ty_a2b ->
 194                         check_TyEq2 (ty @(->)) (At (Just tok_k2a2b) ty_a2b) $ \Refl ty_a ty_b ->
 195                         k ((ty @Map :$ ty_k) :$ ty_a ~> (ty @Map :$ ty_k) :$ ty_b) $ Term $
 196                          \c -> lam $ map_mapWithKey (k2a2b c)
 197                  Token_Term_Map_lookup tok_k tok_m ->
 198                         -- lookup :: Ord k => k -> Map k a -> Maybe a
 199                         compile tok_k ctx $ \ty_k (Term k_) ->
 200                         compile tok_m ctx $ \ty_m (Term m) ->
 201                         check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a ->
 202                         check_TyEq
 203                          (At (Just tok_k) ty_k)
 204                          (At (Just tok_m) ty_m_k) $ \Refl ->
 205                         check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
 206                         k (ty @Maybe :$ ty_m_a) $ Term $
 207                          \c -> map_lookup (k_ c) (m c)
 208                  Token_Term_Map_keys tok_m ->
 209                         -- keys :: Map k a -> [k]
 210                         compile tok_m ctx $ \ty_m (Term m) ->
 211                         check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k _ty_m_a ->
 212                         k (ty @[] :$ ty_m_k) $ Term $
 213                          \c -> map_keys (m c)
 214                  Token_Term_Map_member tok_k tok_m ->
 215                         -- member :: Ord k => k -> Map k a -> Bool
 216                         compile tok_k ctx $ \ty_k (Term k_) ->
 217                         compile tok_m ctx $ \ty_m (Term m) ->
 218                         check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k _ty_m_a ->
 219                         check_TyEq
 220                          (At (Just tok_k) ty_k)
 221                          (At (Just tok_m) ty_m_k) $ \Refl ->
 222                         check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
 223                         k (ty @Bool) $ Term $
 224                          \c -> map_member (k_ c) (m c)
 225                  Token_Term_Map_insert tok_k tok_a ->
 226                         -- insert :: Ord k => k -> a -> Map k a -> Map k a
 227                         compile tok_k ctx $ \ty_k (Term k_) ->
 228                         compile tok_a ctx $ \ty_a (Term a) ->
 229                         check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
 230                         k ((ty @Map :$ ty_k) :$ ty_a ~> (ty @Map :$ ty_k) :$ ty_a) $ Term $
 231                          \c -> lam $ map_insert (k_ c) (a c)
 232                  Token_Term_Map_delete tok_k tok_m ->
 233                         -- delete :: Ord k => k -> Map k a -> Map k a
 234                         compile tok_k ctx $ \ty_k (Term k_) ->
 235                         compile tok_m ctx $ \ty_m (Term m) ->
 236                         check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a ->
 237                         check_TyEq
 238                          (At (Just tok_k) ty_k)
 239                          (At (Just tok_m) ty_m_k) $ \Refl ->
 240                         check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
 241                         k (((ty @Map) :$ ty_k) :$ ty_m_a) $ Term $
 242                          \c -> map_delete (k_ c) (m c)
 243                  Token_Term_Map_difference tok_ma tok_mb ->
 244                         -- difference :: Ord k => Map k a -> Map k b -> Map k a
 245                         compile tok_ma ctx $ \ty_ma (Term ma) ->
 246                         compile tok_mb ctx $ \ty_mb (Term mb) ->
 247                         check_TyEq2 (ty @Map) (At (Just tok_ma) ty_ma) $ \Refl ty_ma_k ty_ma_a ->
 248                         check_TyEq2 (ty @Map) (At (Just tok_mb) ty_mb) $ \Refl ty_mb_k _ty_mb_b ->
 249                         check_TyEq
 250                          (At (Just tok_ma) ty_ma_k)
 251                          (At (Just tok_mb) ty_mb_k) $ \Refl ->
 252                         check_TyCon (At (Just tok_ma) (ty @Ord :$ ty_ma_k)) $ \TyCon ->
 253                         k ((ty @Map :$ ty_ma_k) :$ ty_ma_a) $ Term $
 254                          \c -> map_difference (ma c) (mb c)
 255                  Token_Term_Map_foldrWithKey tok_f ->
 256                         -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
 257                         compile tok_f ctx $ \ty_f (Term f) ->
 258                         check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_k ty_fabb ->
 259                         check_TyEq2 (ty @(->)) (At (Just tok_f) ty_fabb) $ \Refl ty_a ty_fbb ->
 260                         check_TyEq2 (ty @(->)) (At (Just tok_f) ty_fbb) $ \Refl ty_b ty_b' ->
 261                         check_TyEq
 262                          (At (Just tok_f) ty_b)
 263                          (At (Just tok_f) ty_b') $ \Refl ->
 264                         k (ty_b ~> (ty @Map :$ ty_k) :$ ty_a ~> ty_b) $ Term $
 265                          \c -> lam $ \b -> lam $ \m -> map_foldrWithKey (f c) b m
 266 instance -- TokenizeT
 267  Inj_Token meta ts Map =>
 268  TokenizeT meta ts (Proxy Map) where
 269         tokenizeT _t = mempty
 270          { tokenizers_infix = tokenizeTMod [Mod_Name "Map"]
 271                  [ tokenize1 "fromList"     infixN5 Token_Term_Map_fromList
 272                  , tokenize1 "mapWithKey"   infixN5 Token_Term_Map_mapWithKey
 273                  , tokenize2 "lookup"       infixN5 Token_Term_Map_lookup
 274                  , tokenize1 "keys"         infixN5 Token_Term_Map_keys
 275                  , tokenize2 "member"       infixN5 Token_Term_Map_member
 276                  , tokenize2 "insert"       infixN5 Token_Term_Map_insert
 277                  , tokenize2 "delete"       infixN5 Token_Term_Map_delete
 278                  , tokenize2 "difference"   infixN5 Token_Term_Map_difference
 279                  , tokenize1 "foldrWithKey" infixN5 Token_Term_Map_foldrWithKey
 280                  ]
 281          }
 282 instance Gram_Term_AtomsT meta ts (Proxy Map) g