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 (Sym_Map r1, Sym_Map r2) => Sym_Map (Repr_Dup r1 r2) where
  81         map_from_list    = repr_dup1 sym_Map map_from_list
  82         mapWithKey       = repr_dup2 sym_Map mapWithKey
  83         map_lookup       = repr_dup2 sym_Map map_lookup
  84         map_keys         = repr_dup1 sym_Map map_keys
  85         map_member       = repr_dup2 sym_Map map_member
  86         map_insert       = repr_dup3 sym_Map map_insert
  87         map_delete       = repr_dup2 sym_Map map_delete
  88         map_difference   = repr_dup2 sym_Map map_difference
  89         map_foldrWithKey = repr_dup3 sym_Map map_foldrWithKey
  90
  91 sym_Map :: Proxy Sym_Map
  92 sym_Map = Proxy
  93
  94 -- | Parsing utility to check that the given type is a 'Type_List'
  95 -- or raise 'Error_Expr_Type_mismatch'.
  96 check_type_map
  97  :: forall ast ex root ty h ret.
  98  ( root ~ Root_of_Expr ex
  99  , ty ~ Type_Root_of_Expr ex
 100  , Type0_Lift   Type_Map (Type_of_Expr root)
 101  , Type0_Unlift Type_Map (Type_of_Expr root)
 102  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 103                    (Error_of_Expr ast root)
 104  )
 105  => Proxy ex -> ast -> ty h
 106  -> (Type_Map ty h -> Either (Error_of_Expr ast root) ret)
 107  -> Either (Error_of_Expr ast root) ret
 108 check_type_map ex ast ty k =
 109         case type0_unlift $ unType_Root ty of
 110          Just ty_l -> k ty_l
 111          Nothing -> Left $
 112                 error_expr ex $
 113                 Error_Expr_Type_mismatch ast
 114                  (Exists_Type0 (type_map (type_var0 SZero) (type_var0 $ SSucc SZero)
 115                  :: ty (Map Var0 Var0)))
 116                  (Exists_Type0 ty)
 117
 118 -- | Parse 'map_from_list'.
 119 map_from_list_from
 120  :: forall root ty ast hs ret.
 121  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 122  , Expr_From ast root
 123  , Type0_Lift   Type_List   (Type_of_Expr root)
 124  , Type0_Unlift Type_List   (Type_of_Expr root)
 125  , Type0_Lift   Type_Map    (Type_of_Expr root)
 126  , Type0_Lift   Type_Tuple2 (Type_of_Expr root)
 127  , Type0_Unlift Type_Tuple2 (Type_of_Expr root)
 128  , Type0_Constraint Ord ty
 129  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 130                    (Error_of_Expr ast root)
 131  , Root_of_Expr root ~ root
 132  ) => ast
 133  -> ExprFrom ast (Expr_Map root) hs ret
 134 map_from_list_from ast_l ex ast ctx k =
 135         expr_from (Proxy::Proxy root) ast_l ctx $
 136          \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
 137         check_type_list ex ast ty_l $ \(Type1 _ ty_l_t) ->
 138         check_type_tuple2 ex ast ty_l_t $ \(Type2 Proxy ty_k ty_a) ->
 139         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 140         k (type_map ty_k ty_a) $ Forall_Repr_with_Context $
 141          \c -> map_from_list (l c)
 142
 143 -- | Parse 'mapWithKey'.
 144 mapWithKey_from
 145  :: forall root ty ast hs ret.
 146  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 147  , Type0_Eq ty
 148  , Expr_From ast root
 149  , Type0_Lift   Type_Fun (Type_of_Expr root)
 150  , Type0_Unlift Type_Fun (Type_of_Expr root)
 151  , Type0_Lift   Type_Map (Type_of_Expr root)
 152  , Type0_Unlift Type_Map (Type_of_Expr root)
 153  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 154                    (Error_of_Expr ast root)
 155  , Root_of_Expr root ~ root
 156  ) => ast -> ast
 157  -> ExprFrom ast (Expr_Map root) hs ret
 158 mapWithKey_from ast_f ast_m ex ast ctx k =
 159  -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
 160         expr_from (Proxy::Proxy root) ast_f ctx $
 161          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 162         expr_from (Proxy::Proxy root) ast_m ctx $
 163          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 164         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_k ty_f_a2b
 165          :: Type_Fun ty h_f) ->
 166         check_type_fun ex ast ty_f_a2b $ \(Type2 Proxy ty_f_a ty_f_b
 167          :: Type_Fun ty h_f_a2b) ->
 168         check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
 169         check_type0_eq ex ast ty_f_k ty_m_k $ \Refl ->
 170         check_type0_eq ex ast ty_f_a ty_m_a $ \Refl ->
 171         k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
 172          \c -> mapWithKey (f c) (m c)
 173
 174 -- | Parse 'map_lookup'.
 175 map_lookup_from
 176  :: forall root ty ast hs ret.
 177  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 178  , Type0_Eq ty
 179  , Expr_From ast root
 180  , Type0_Lift   Type_Map   (Type_of_Expr root)
 181  , Type0_Unlift Type_Map   (Type_of_Expr root)
 182  , Type0_Lift   Type_Maybe (Type_of_Expr root)
 183  , Type0_Constraint Ord ty
 184  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 185                    (Error_of_Expr ast root)
 186  , Root_of_Expr root ~ root
 187  ) => ast -> ast
 188  -> ExprFrom ast (Expr_Map root) hs ret
 189 map_lookup_from ast_k ast_m ex ast ctx k =
 190  -- lookup :: Ord k => k -> Map k a -> Maybe a
 191         expr_from (Proxy::Proxy root) ast_k ctx $
 192          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 193         expr_from (Proxy::Proxy root) ast_m ctx $
 194          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 195         check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
 196         check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
 197         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 198         k (type_maybe ty_m_a) $ Forall_Repr_with_Context $
 199          \c -> map_lookup (key c) (m c)
 200
 201 -- | Parse 'map_keys'.
 202 map_keys_from
 203  :: forall root ty ast hs ret.
 204  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 205  , Type0_Eq ty
 206  , Expr_From ast root
 207  , Type0_Lift   Type_Map  (Type_of_Expr root)
 208  , Type0_Unlift Type_Map  (Type_of_Expr root)
 209  , Type0_Lift   Type_List (Type_of_Expr root)
 210  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 211                    (Error_of_Expr ast root)
 212  , Root_of_Expr root ~ root
 213  ) => ast
 214  -> ExprFrom ast (Expr_Map root) hs ret
 215 map_keys_from ast_m ex ast ctx k =
 216  -- keys :: Map k a -> [k]
 217         expr_from (Proxy::Proxy root) ast_m ctx $
 218          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 219         check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k _ty_m_a) ->
 220         k (type_list ty_m_k) $ Forall_Repr_with_Context $
 221          \c -> map_keys (m c)
 222
 223 -- | Parse 'map_member'.
 224 map_member_from
 225  :: forall root ty ast hs ret.
 226  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 227  , Type0_Eq ty
 228  , Expr_From ast root
 229  , Type0_Constraint Ord ty
 230  , Type0_Lift   Type_Map  (Type_of_Expr root)
 231  , Type0_Unlift Type_Map  (Type_of_Expr root)
 232  , Type0_Lift   Type_Bool (Type_of_Expr root)
 233  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 234                    (Error_of_Expr ast root)
 235  , Root_of_Expr root ~ root
 236  ) => ast -> ast
 237  -> ExprFrom ast (Expr_Map root) hs ret
 238 map_member_from ast_k ast_m ex ast ctx k =
 239  -- member :: Ord k => k -> Map k a -> Bool
 240         expr_from (Proxy::Proxy root) ast_k ctx $
 241          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 242         expr_from (Proxy::Proxy root) ast_m ctx $
 243          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 244         check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k _ty_m_a) ->
 245         check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
 246         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 247         k type_bool $ Forall_Repr_with_Context $
 248          \c -> map_member (key c) (m c)
 249
 250 -- | Parse 'map_insert'.
 251 map_insert_from
 252  :: forall root ty ast hs ret.
 253  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 254  , Type0_Eq ty
 255  , Expr_From ast root
 256  , Type0_Constraint Ord ty
 257  , Type0_Lift   Type_Map (Type_of_Expr root)
 258  , Type0_Unlift Type_Map (Type_of_Expr root)
 259  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 260                    (Error_of_Expr ast root)
 261  , Root_of_Expr root ~ root
 262  ) => ast -> ast -> ast
 263  -> ExprFrom ast (Expr_Map root) hs ret
 264 map_insert_from ast_k ast_a ast_m ex ast ctx k =
 265  -- insert :: Ord k => k -> a -> Map k a -> Map k a
 266         expr_from (Proxy::Proxy root) ast_k ctx $
 267          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 268         expr_from (Proxy::Proxy root) ast_a ctx $
 269          \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
 270         expr_from (Proxy::Proxy root) ast_m ctx $
 271          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 272         check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
 273         check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
 274         check_type0_eq ex ast ty_a ty_m_a $ \Refl ->
 275         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 276         k ty_m $ Forall_Repr_with_Context $
 277          \c -> map_insert (key c) (a c) (m c)
 278
 279 -- | Parse 'map_delete'.
 280 map_delete_from
 281  :: forall root ty ast hs ret.
 282  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 283  , Type0_Eq ty
 284  , Expr_From ast root
 285  , Type0_Lift   Type_Map (Type_of_Expr root)
 286  , Type0_Unlift Type_Map (Type_of_Expr root)
 287  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 288                    (Error_of_Expr ast root)
 289  , Type0_Constraint Ord ty
 290  , Root_of_Expr root ~ root
 291  ) => ast -> ast
 292  -> ExprFrom ast (Expr_Map root) hs ret
 293 map_delete_from ast_k ast_m ex ast ctx k =
 294  -- delete :: Ord k => k -> Map k a -> Map k a
 295         expr_from (Proxy::Proxy root) ast_k ctx $
 296          \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
 297         expr_from (Proxy::Proxy root) ast_m ctx $
 298          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 299         check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k _ty_m_a) ->
 300         check_type0_eq ex ast ty_k ty_m_k $ \Refl ->
 301         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
 302         k ty_m $ Forall_Repr_with_Context $
 303          \c -> map_delete (key c) (m c)
 304
 305 -- | Parse 'map_difference'.
 306 map_difference_from
 307  :: forall root ty ast hs ret.
 308  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 309  , Type0_Eq ty
 310  , Expr_From ast root
 311  , Type0_Lift   Type_Map (Type_of_Expr root)
 312  , Type0_Unlift Type_Map (Type_of_Expr root)
 313  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 314                    (Error_of_Expr ast root)
 315  , Type0_Constraint Ord ty
 316  , Root_of_Expr root ~ root
 317  ) => ast -> ast
 318  -> ExprFrom ast (Expr_Map root) hs ret
 319 map_difference_from ast_ma ast_mb ex ast ctx k =
 320  -- difference :: Ord k => Map k a -> Map k b -> Map k a
 321         expr_from (Proxy::Proxy root) ast_ma ctx $
 322          \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
 323         expr_from (Proxy::Proxy root) ast_mb ctx $
 324          \(ty_mb::ty h_mb) (Forall_Repr_with_Context mb) ->
 325         check_type_map ex ast ty_ma $ \(Type2 Proxy ty_ma_k _ty_ma_a) ->
 326         check_type_map ex ast ty_mb $ \(Type2 Proxy ty_mb_k _ty_mb_b) ->
 327         check_type0_eq ex ast ty_ma_k ty_mb_k $ \Refl ->
 328         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_ma_k $ \Dict ->
 329         k ty_ma $ Forall_Repr_with_Context $
 330          \c -> map_difference (ma c) (mb c)
 331
 332 -- | Parse 'map_foldrWithKey'.
 333 map_foldrWithKey_from
 334  :: forall root ty ast hs ret.
 335  ( ty ~ Type_Root_of_Expr (Expr_Map root)
 336  , Type0_Eq ty
 337  , Expr_From ast root
 338  , Type0_Lift   Type_Fun (Type_of_Expr root)
 339  , Type0_Unlift Type_Fun (Type_of_Expr root)
 340  , Type0_Lift   Type_Map (Type_of_Expr root)
 341  , Type0_Unlift Type_Map (Type_of_Expr root)
 342  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 343                    (Error_of_Expr ast root)
 344  , Type0_Constraint Ord ty
 345  , Root_of_Expr root ~ root
 346  ) => ast -> ast -> ast
 347  -> ExprFrom ast (Expr_Map root) hs ret
 348 map_foldrWithKey_from ast_f ast_b ast_m ex ast ctx k =
 349  -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
 350         expr_from (Proxy::Proxy root) ast_f ctx $
 351          \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
 352         expr_from (Proxy::Proxy root) ast_b ctx $
 353          \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
 354         expr_from (Proxy::Proxy root) ast_m ctx $
 355          \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
 356         check_type_fun ex ast ty_f $ \(Type2 Proxy ty_f_k ty_f_a2b2b) ->
 357         check_type_fun ex ast ty_f_a2b2b $ \(Type2 Proxy ty_f_a ty_f_b2b) ->
 358         check_type_fun ex ast ty_f_b2b $ \(Type2 Proxy ty_f_b ty_f_b') ->
 359         check_type_map ex ast ty_m $ \(Type2 Proxy ty_m_k ty_m_a) ->
 360         check_type0_eq ex ast ty_f_k ty_m_k $ \Refl ->
 361         check_type0_eq ex ast ty_f_a ty_m_a $ \Refl ->
 362         check_type0_eq ex ast ty_b ty_f_b $ \Refl ->
 363         check_type0_eq ex ast ty_f_b ty_f_b' $ \Refl ->
 364         check_type0_constraint ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
 365         k ty_b $ Forall_Repr_with_Context $
 366          \c -> map_foldrWithKey (f c) (b c) (m c)
 367
 368 -- * Type 'Expr_Map'
 369 -- | Expression.
 370 data Expr_Map (root:: *)
 371 type instance Root_of_Expr      (Expr_Map root)      = root
 372 type instance Type_of_Expr      (Expr_Map root)      = Type_Map
 373 type instance Sym_of_Expr       (Expr_Map root) repr = Sym_Map repr
 374 type instance Error_of_Expr ast (Expr_Map root)      = No_Error_Expr