Language/Symantic/Expr/Map.hs

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