Language/Symantic/Expr/Map.hs

   1 {-# LANGUAGE DefaultSignatures #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE OverloadedStrings #-}
   6 {-# LANGUAGE ScopedTypeVariables #-}
   7 {-# LANGUAGE TypeFamilies #-}
   8 {-# OPTIONS_GHC -fno-warn-orphans #-}
   9 -- | Expression for 'Map'.
  10 module Language.Symantic.Expr.Map where
  11
  12 import Control.Monad
  13 import Data.Map.Strict (Map)
  14 import qualified Data.Map.Strict as Map
  15 import Data.Proxy (Proxy(..))
  16 import Data.Type.Equality ((:~:)(Refl))
  17
  18 import Language.Symantic.Type
  19 import Language.Symantic.Repr
  20 import Language.Symantic.Expr.Root
  21 import Language.Symantic.Expr.Error
  22 import Language.Symantic.Expr.From
  23 import Language.Symantic.Expr.Lambda
  24 import Language.Symantic.Expr.List
  25 import Language.Symantic.Expr.Tuple
  26 import Language.Symantic.Trans.Common
  27
  28 -- * Class 'Sym_Map_Lam'
  29 -- | Symantic.
  30 class Sym_Map repr where
  31         map_from_list :: Ord k => repr [(k, a)] -> repr (Map k a)
  32         mapWithKey :: repr (k -> a -> b) -> repr (Map k a) -> repr (Map k b)
  33         map_lookup :: Ord k => repr k -> repr (Map k a) -> repr (Maybe a)
  34         map_keys :: repr (Map k a) -> repr [k]
  35         map_member :: Ord k => repr k -> repr (Map k a) -> repr Bool
  36         map_insert :: Ord k => repr k -> repr a -> repr (Map k a) -> repr (Map k a)
  37         map_delete :: Ord k => repr k -> repr (Map k a) -> repr (Map k a)
  38         map_difference :: Ord k => repr (Map k a) -> repr (Map k b) -> repr (Map k a)
  39         map_foldrWithKey :: repr (k -> a -> b -> b) -> repr b -> repr (Map k a) -> repr b
  40
  41         default map_from_list :: (Trans t repr, Ord k) => t repr [(k, a)] -> t repr (Map k a)
  42         default mapWithKey :: Trans t repr => t repr (k -> a -> b) -> t repr (Map k a) -> t repr (Map k b)
  43         default map_lookup :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Maybe a)
  44         default map_keys :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr [k]
  45         default map_member :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr Bool
  46         default map_insert :: (Trans t repr, Ord k) => t repr k -> t repr a -> t repr (Map k a) -> t repr (Map k a)
  47         default map_delete :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Map k a)
  48         default map_difference :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr (Map k b) -> t repr (Map k a)
  49         default map_foldrWithKey :: Trans t repr => t repr (k -> a -> b -> b) -> t repr b -> t repr (Map k a) -> t repr b
  50
  51         map_from_list    = trans_map1 map_from_list
  52         mapWithKey       = trans_map2 mapWithKey
  53         map_lookup       = trans_map2 map_lookup
  54         map_keys         = trans_map1 map_keys
  55         map_member       = trans_map2 map_member
  56         map_insert       = trans_map3 map_insert
  57         map_delete       = trans_map2 map_delete
  58         map_difference   = trans_map2 map_difference
  59         map_foldrWithKey = trans_map3 map_foldrWithKey
  60 instance Sym_Map Repr_Host where
  61         map_from_list    = liftM  Map.fromList
  62         mapWithKey       = liftM2 Map.mapWithKey
  63         map_lookup       = liftM2 Map.lookup
  64         map_keys         = liftM  Map.keys
  65         map_member       = liftM2 Map.member
  66         map_insert       = liftM3 Map.insert
  67         map_delete       = liftM2 Map.delete
  68         map_difference   = liftM2 Map.difference
  69         map_foldrWithKey = liftM3 Map.foldrWithKey
  70 instance Sym_Map Repr_Text where
  71         map_from_list    = repr_text_app1 "map_from_list"
  72         mapWithKey       = repr_text_app2 "mapWithKey"
  73         map_lookup       = repr_text_app2 "map_lookup"
  74         map_keys         = repr_text_app1 "map_keys"
  75         map_member       = repr_text_app2 "map_member"
  76         map_insert       = repr_text_app3 "map_insert"
  77         map_delete       = repr_text_app2 "map_delete"
  78         map_difference   = repr_text_app2 "map_difference"
  79         map_foldrWithKey = repr_text_app3 "map_foldrWithKey"
  80 instance
  81  ( Sym_Map r1
  82  , Sym_Map r2
  83  ) => Sym_Map (Dup r1 r2) where
  84         map_from_list (l1 `Dup` l2) =
  85                 map_from_list l1 `Dup` map_from_list l2
  86         mapWithKey (f1 `Dup` f2) (m1 `Dup` m2) =
  87                 mapWithKey f1 m1 `Dup` mapWithKey f2 m2
  88         map_lookup (k1 `Dup` k2) (m1 `Dup` m2) =
  89                 map_lookup k1 m1 `Dup` map_lookup k2 m2
  90         map_keys (m1 `Dup` m2) =
  91                 map_keys m1 `Dup` map_keys m2
  92         map_member (k1 `Dup` k2) (m1 `Dup` m2) =
  93                 map_member k1 m1 `Dup` map_member k2 m2
  94         map_insert (k1 `Dup` k2) (a1 `Dup` a2) (m1 `Dup` m2) =
  95                 map_insert k1 a1 m1 `Dup` map_insert k2 a2 m2
  96         map_delete (k1 `Dup` k2) (m1 `Dup` m2) =
  97                 map_delete k1 m1 `Dup` map_delete k2 m2
  98         map_difference (ma1 `Dup` ma2) (mb1 `Dup` mb2) =
  99                 map_difference ma1 mb1 `Dup` map_difference ma2 mb2
 100         map_foldrWithKey (f1 `Dup` f2) (b1 `Dup` b2) (m1 `Dup` m2) =
 101                 map_foldrWithKey f1 b1 m1 `Dup` map_foldrWithKey f2 b2 m2
 102
 103 -- | Parsing utility to check that the given type is a 'Type_List'
 104 -- or raise 'Error_Expr_Type_mismatch'.
 105 check_type_map
 106  :: forall ast ex root ty h ret.
 107  ( root ~ Root_of_Expr ex
 108  , ty ~ Type_Root_of_Expr ex
 109  , Lift_Type   Type_Map (Type_of_Expr root)
 110  , Unlift_Type Type_Map (Type_of_Expr root)
 111  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 112                    (Error_of_Expr ast root)
 113  )
 114  => Proxy ex -> ast -> ty h
 115  -> (Type_Map ty h -> Either (Error_of_Expr ast root) ret)
 116  -> Either (Error_of_Expr ast root) ret
 117 check_type_map ex ast ty k =
 118         case unlift_type $ unType_Root ty of
 119          Just ty_l -> k ty_l
 120          Nothing -> Left $
 121                 error_expr ex $
 122                 Error_Expr_Type_mismatch ast
 123                  (Exists_Type (type_map (type_var0 SZero) (type_var0 $ SSucc SZero)
 124                  :: ty (Map Var0 Var0)))
 125                  (Exists_Type ty)
 126
 127 -- | Parse 'map_from_list'.
 128 map_from_list_from
 129  :: forall root ty ast hs ret.
 130  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 131  , Expr_from ast root
 132  , Lift_Type   Type_List   (Type_of_Expr root)
 133  , Unlift_Type Type_List   (Type_of_Expr root)
 134  , Lift_Type   Type_Map    (Type_of_Expr root)
 135  , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 136  , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 137  , Constraint_Type Ord ty
 138  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 139                    (Error_of_Expr ast root)
 140  , Root_of_Expr root ~ root
 141  ) => ast
 142  -> Expr_From ast (Expr_Map root) hs ret
 143 map_from_list_from ast_l ex ast ctx k =
 144         expr_from (Proxy::Proxy root) ast_l ctx $
 145          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 146         check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_t) ->
 147         check_type_tuple2 ex ast ty_l_t $ \(Type_Type2 Proxy ty_k ty_a) ->
 148         check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 149         k (type_map ty_k ty_a) $ Forall_Repr_with_Context $
 150          \c -> map_from_list (l c)
 151
 152 -- | Parse 'mapWithKey'.
 153 mapWithKey_from
 154  :: forall root ty ast hs ret.
 155  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 156  , Eq_Type ty
 157  , Expr_from ast root
 158  , Lift_Type   Type_Fun (Type_of_Expr root)
 159  , Unlift_Type Type_Fun (Type_of_Expr root)
 160  , Lift_Type   Type_Map (Type_of_Expr root)
 161  , Unlift_Type Type_Map (Type_of_Expr root)
 162  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 163                    (Error_of_Expr ast root)
 164  , Root_of_Expr root ~ root
 165  ) => ast -> ast
 166  -> Expr_From ast (Expr_Map root) hs ret
 167 mapWithKey_from ast_f ast_m ex ast ctx k =
 168  -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
 169         expr_from (Proxy::Proxy root) ast_f ctx $
 170          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 171         expr_from (Proxy::Proxy root) ast_m ctx $
 172          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 173         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_k ty_f_a2b
 174          :: Type_Fun ty h_f) ->
 175         check_type_fun ex ast ty_f_a2b $ \(Type_Type2 Proxy ty_f_a ty_f_b
 176          :: Type_Fun ty h_f_a2b) ->
 177         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
 178         check_eq_type ex ast ty_f_k ty_m_k $ \Refl ->
 179         check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
 180         k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
 181          \c -> mapWithKey (f c) (m c)
 182
 183 -- | Parse 'map_lookup'.
 184 map_lookup_from
 185  :: forall root ty ast hs ret.
 186  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 187  , Eq_Type ty
 188  , Expr_from ast root
 189  , Lift_Type   Type_Map   (Type_of_Expr root)
 190  , Unlift_Type Type_Map   (Type_of_Expr root)
 191  , Lift_Type   Type_Maybe (Type_of_Expr root)
 192  , Constraint_Type Ord ty
 193  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 194                    (Error_of_Expr ast root)
 195  , Root_of_Expr root ~ root
 196  ) => ast -> ast
 197  -> Expr_From ast (Expr_Map root) hs ret
 198 map_lookup_from ast_k ast_m ex ast ctx k =
 199  -- lookup :: Ord k => k -> Map k a -> Maybe a
 200         expr_from (Proxy::Proxy root) ast_k ctx $
 201          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 202         expr_from (Proxy::Proxy root) ast_m ctx $
 203          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 204         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
 205         check_eq_type ex ast ty_k ty_m_k $ \Refl ->
 206         check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 207         k (type_maybe ty_m_a) $ Forall_Repr_with_Context $
 208          \c -> map_lookup (key c) (m c)
 209
 210 -- | Parse 'map_keys'.
 211 map_keys_from
 212  :: forall root ty ast hs ret.
 213  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 214  , Eq_Type ty
 215  , Expr_from ast root
 216  , Lift_Type   Type_Map  (Type_of_Expr root)
 217  , Unlift_Type Type_Map  (Type_of_Expr root)
 218  , Lift_Type   Type_List (Type_of_Expr root)
 219  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 220                    (Error_of_Expr ast root)
 221  , Root_of_Expr root ~ root
 222  ) => ast
 223  -> Expr_From ast (Expr_Map root) hs ret
 224 map_keys_from ast_m ex ast ctx k =
 225  -- keys :: Map k a -> [k]
 226         expr_from (Proxy::Proxy root) ast_m ctx $
 227          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 228         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
 229         k (type_list ty_m_k) $ Forall_Repr_with_Context $
 230          \c -> map_keys (m c)
 231
 232 -- | Parse 'map_member'.
 233 map_member_from
 234  :: forall root ty ast hs ret.
 235  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 236  , Eq_Type ty
 237  , Expr_from ast root
 238  , Constraint_Type Ord ty
 239  , Lift_Type   Type_Map  (Type_of_Expr root)
 240  , Unlift_Type Type_Map  (Type_of_Expr root)
 241  , Lift_Type   Type_Bool (Type_of_Expr root)
 242  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 243                    (Error_of_Expr ast root)
 244  , Root_of_Expr root ~ root
 245  ) => ast -> ast
 246  -> Expr_From ast (Expr_Map root) hs ret
 247 map_member_from ast_k ast_m ex ast ctx k =
 248  -- member :: Ord k => k -> Map k a -> Bool
 249         expr_from (Proxy::Proxy root) ast_k ctx $
 250          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 251         expr_from (Proxy::Proxy root) ast_m ctx $
 252          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 253         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
 254         check_eq_type ex ast ty_k ty_m_k $ \Refl ->
 255         check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 256         k type_bool $ Forall_Repr_with_Context $
 257          \c -> map_member (key c) (m c)
 258
 259 -- | Parse 'map_insert'.
 260 map_insert_from
 261  :: forall root ty ast hs ret.
 262  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 263  , Eq_Type ty
 264  , Expr_from ast root
 265  , Constraint_Type Ord ty
 266  , Lift_Type   Type_Map (Type_of_Expr root)
 267  , Unlift_Type Type_Map (Type_of_Expr root)
 268  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 269                    (Error_of_Expr ast root)
 270  , Root_of_Expr root ~ root
 271  ) => ast -> ast -> ast
 272  -> Expr_From ast (Expr_Map root) hs ret
 273 map_insert_from ast_k ast_a ast_m ex ast ctx k =
 274  -- insert :: Ord k => k -> a -> Map k a -> Map k a
 275         expr_from (Proxy::Proxy root) ast_k ctx $
 276          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 277         expr_from (Proxy::Proxy root) ast_a ctx $
 278          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 279         expr_from (Proxy::Proxy root) ast_m ctx $
 280          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 281         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
 282         check_eq_type ex ast ty_k ty_m_k $ \Refl ->
 283         check_eq_type ex ast ty_a ty_m_a $ \Refl ->
 284         check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 285         k ty_m $ Forall_Repr_with_Context $
 286          \c -> map_insert (key c) (a c) (m c)
 287
 288 -- | Parse 'map_delete'.
 289 map_delete_from
 290  :: forall root ty ast hs ret.
 291  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 292  , Eq_Type ty
 293  , Expr_from ast root
 294  , Lift_Type   Type_Map (Type_of_Expr root)
 295  , Unlift_Type Type_Map (Type_of_Expr root)
 296  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 297                    (Error_of_Expr ast root)
 298  , Constraint_Type Ord ty
 299  , Root_of_Expr root ~ root
 300  ) => ast -> ast
 301  -> Expr_From ast (Expr_Map root) hs ret
 302 map_delete_from ast_k ast_m ex ast ctx k =
 303  -- delete :: Ord k => k -> Map k a -> Map k a
 304         expr_from (Proxy::Proxy root) ast_k ctx $
 305          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 306         expr_from (Proxy::Proxy root) ast_m ctx $
 307          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 308         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
 309         check_eq_type ex ast ty_k ty_m_k $ \Refl ->
 310         check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 311         k ty_m $ Forall_Repr_with_Context $
 312          \c -> map_delete (key c) (m c)
 313
 314 -- | Parse 'map_difference'.
 315 map_difference_from
 316  :: forall root ty ast hs ret.
 317  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 318  , Eq_Type ty
 319  , Expr_from ast root
 320  , Lift_Type   Type_Map (Type_of_Expr root)
 321  , Unlift_Type Type_Map (Type_of_Expr root)
 322  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 323                    (Error_of_Expr ast root)
 324  , Constraint_Type Ord ty
 325  , Root_of_Expr root ~ root
 326  ) => ast -> ast
 327  -> Expr_From ast (Expr_Map root) hs ret
 328 map_difference_from ast_ma ast_mb ex ast ctx k =
 329  -- difference :: Ord k => Map k a -> Map k b -> Map k a
 330         expr_from (Proxy::Proxy root) ast_ma ctx $
 331          \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
 332         expr_from (Proxy::Proxy root) ast_mb ctx $
 333          \(ty_mb::ty h_mb) (Forall_Repr_with_Context mb) ->
 334         check_type_map ex ast ty_ma $ \(Type_Type2 Proxy ty_ma_k _ty_ma_a) ->
 335         check_type_map ex ast ty_mb $ \(Type_Type2 Proxy ty_mb_k _ty_mb_b) ->
 336         check_eq_type ex ast ty_ma_k ty_mb_k $ \Refl ->
 337         check_constraint_type ex (Proxy::Proxy Ord) ast ty_ma_k $ \Dict ->
 338         k ty_ma $ Forall_Repr_with_Context $
 339          \c -> map_difference (ma c) (mb c)
 340
 341 -- | Parse 'map_foldrWithKey'.
 342 map_foldrWithKey_from
 343  :: forall root ty ast hs ret.
 344  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 345  , Eq_Type ty
 346  , Expr_from ast root
 347  , Lift_Type   Type_Fun (Type_of_Expr root)
 348  , Unlift_Type Type_Fun (Type_of_Expr root)
 349  , Lift_Type   Type_Map (Type_of_Expr root)
 350  , Unlift_Type Type_Map (Type_of_Expr root)
 351  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 352                    (Error_of_Expr ast root)
 353  , Constraint_Type Ord ty
 354  , Root_of_Expr root ~ root
 355  ) => ast -> ast -> ast
 356  -> Expr_From ast (Expr_Map root) hs ret
 357 map_foldrWithKey_from ast_f ast_b ast_m ex ast ctx k =
 358  -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
 359         expr_from (Proxy::Proxy root) ast_f ctx $
 360          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 361         expr_from (Proxy::Proxy root) ast_b ctx $
 362          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 363         expr_from (Proxy::Proxy root) ast_m ctx $
 364          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 365         check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_k ty_f_a2b2b) ->
 366         check_type_fun ex ast ty_f_a2b2b $ \(Type_Type2 Proxy ty_f_a ty_f_b2b) ->
 367         check_type_fun ex ast ty_f_b2b $ \(Type_Type2 Proxy ty_f_b ty_f_b') ->
 368         check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
 369         check_eq_type ex ast ty_f_k ty_m_k $ \Refl ->
 370         check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
 371         check_eq_type ex ast ty_b ty_f_b $ \Refl ->
 372         check_eq_type ex ast ty_f_b ty_f_b' $ \Refl ->
 373         check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
 374         k ty_b $ Forall_Repr_with_Context $
 375          \c -> map_foldrWithKey (f c) (b c) (m c)
 376
 377 -- * Type 'Expr_Map'
 378 -- | Expression.
 379 data Expr_Map (root:: *)
 380 type instance Root_of_Expr      (Expr_Map root)      = root
 381 type instance Type_of_Expr      (Expr_Map root)      = Type_Map
 382 type instance Sym_of_Expr       (Expr_Map root) repr = (Sym_Map repr)
 383 type instance Error_of_Expr ast (Expr_Map root)      = No_Error_Expr