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