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