Language/Symantic/Compiling/Map.hs

   1 {-# LANGUAGE DataKinds #-}
   2 {-# LANGUAGE DefaultSignatures #-}
   3 {-# LANGUAGE FlexibleContexts #-}
   4 {-# LANGUAGE FlexibleInstances #-}
   5 {-# LANGUAGE MultiParamTypeClasses #-}
   6 {-# LANGUAGE OverloadedStrings #-}
   7 {-# LANGUAGE Rank2Types #-}
   8 {-# LANGUAGE ScopedTypeVariables #-}
   9 {-# LANGUAGE TypeFamilies #-}
  10 {-# LANGUAGE TypeOperators #-}
  11 {-# LANGUAGE UndecidableInstances #-}
  12 {-# OPTIONS_GHC -fno-warn-orphans #-}
  13 {-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-}
  14 -- | Symantic for 'Map'.
  15 module Language.Symantic.Compiling.Map where
  16
  17 import Control.Monad (liftM, liftM2, liftM3)
  18 import Data.Map.Strict (Map)
  19 import qualified Data.Map.Strict as Map
  20 import Data.Proxy
  21 import Data.String (IsString)
  22 import Data.Text (Text)
  23 import Data.Type.Equality ((:~:)(Refl))
  24 import Prelude hiding (either)
  25
  26 import Language.Symantic.Typing
  27 import Language.Symantic.Compiling.Term
  28 import Language.Symantic.Compiling.Bool (tyBool)
  29 import Language.Symantic.Compiling.List (tyList)
  30 import Language.Symantic.Compiling.Ord (tyOrd)
  31 import Language.Symantic.Compiling.Maybe (tyMaybe)
  32 import Language.Symantic.Compiling.Tuple2 (tyTuple2)
  33 import Language.Symantic.Interpreting
  34 import Language.Symantic.Transforming.Trans
  35
  36 -- * Class 'Sym_Map'
  37 class Sym_Map term where
  38         map_fromList :: Ord k => term [(k, a)] -> term (Map k a)
  39         map_mapWithKey :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
  40         map_lookup :: Ord k => term k -> term (Map k a) -> term (Maybe a)
  41         map_keys :: term (Map k a) -> term [k]
  42         map_member :: Ord k => term k -> term (Map k a) -> term Bool
  43         map_insert :: Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
  44         map_delete :: Ord k => term k -> term (Map k a) -> term (Map k a)
  45         map_difference :: Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
  46         map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
  47
  48         default map_fromList :: (Trans t term, Ord k) => t term [(k, a)] -> t term (Map k a)
  49         default map_mapWithKey :: Trans t term => t term (k -> a -> b) -> t term (Map k a) -> t term (Map k b)
  50         default map_lookup :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Maybe a)
  51         default map_keys :: Trans t term => t term (Map k a) -> t term [k]
  52         default map_member :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term Bool
  53         default map_insert :: (Trans t term, Ord k) => t term k -> t term a -> t term (Map k a) -> t term (Map k a)
  54         default map_delete :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Map k a)
  55         default map_difference :: (Trans t term, Ord k) => t term (Map k a) -> t term (Map k b) -> t term (Map k a)
  56         default map_foldrWithKey :: Trans t term => t term (k -> a -> b -> b) -> t term b -> t term (Map k a) -> t term b
  57
  58         map_fromList     = trans_map1 map_fromList
  59         map_mapWithKey   = trans_map2 map_mapWithKey
  60         map_lookup       = trans_map2 map_lookup
  61         map_keys         = trans_map1 map_keys
  62         map_member       = trans_map2 map_member
  63         map_insert       = trans_map3 map_insert
  64         map_delete       = trans_map2 map_delete
  65         map_difference   = trans_map2 map_difference
  66         map_foldrWithKey = trans_map3 map_foldrWithKey
  67
  68 type instance Sym_of_Iface (Proxy Map) = Sym_Map
  69 type instance Consts_of_Iface (Proxy Map) = Proxy Map ': Consts_imported_by Map
  70 type instance Consts_imported_by Map =
  71  [ Proxy (->)
  72  , Proxy []
  73  , Proxy (,)
  74  , Proxy Bool
  75  , Proxy Eq
  76  , Proxy Foldable
  77  , Proxy Functor
  78  , Proxy Maybe
  79  , Proxy Monad
  80  , Proxy Monoid
  81  , Proxy Ord
  82  , Proxy Traversable
  83  ]
  84
  85 instance Sym_Map HostI where
  86         map_fromList     = liftM  Map.fromList
  87         map_mapWithKey   = liftM2 Map.mapWithKey
  88         map_lookup       = liftM2 Map.lookup
  89         map_keys         = liftM  Map.keys
  90         map_member       = liftM2 Map.member
  91         map_insert       = liftM3 Map.insert
  92         map_delete       = liftM2 Map.delete
  93         map_difference   = liftM2 Map.difference
  94         map_foldrWithKey = liftM3 Map.foldrWithKey
  95 instance Sym_Map TextI where
  96         map_fromList     = textI_app1 "Map.fromList"
  97         map_mapWithKey   = textI_app2 "Map.mapWithKey"
  98         map_lookup       = textI_app2 "Map.lookup"
  99         map_keys         = textI_app1 "Map.keys"
 100         map_member       = textI_app2 "Map.member"
 101         map_insert       = textI_app3 "Map.insert"
 102         map_delete       = textI_app2 "Map.delete"
 103         map_difference   = textI_app2 "Map.difference"
 104         map_foldrWithKey = textI_app3 "Map.foldrWithKey"
 105 instance (Sym_Map r1, Sym_Map r2) => Sym_Map (DupI r1 r2) where
 106         map_fromList     = dupI1 sym_Map map_fromList
 107         map_mapWithKey   = dupI2 sym_Map map_mapWithKey
 108         map_lookup       = dupI2 sym_Map map_lookup
 109         map_keys         = dupI1 sym_Map map_keys
 110         map_member       = dupI2 sym_Map map_member
 111         map_insert       = dupI3 sym_Map map_insert
 112         map_delete       = dupI2 sym_Map map_delete
 113         map_difference   = dupI2 sym_Map map_difference
 114         map_foldrWithKey = dupI3 sym_Map map_foldrWithKey
 115
 116 instance Const_from Text cs => Const_from Text (Proxy Map ': cs) where
 117         const_from "Map" k = k (ConstZ kind)
 118         const_from s k = const_from s $ k . ConstS
 119 instance Show_Const cs => Show_Const (Proxy Map ': cs) where
 120         show_const ConstZ{} = "Map"
 121         show_const (ConstS c) = show_const c
 122
 123 instance -- Proj_ConC
 124  ( Proj_Const cs Map
 125  , Proj_Consts cs (Consts_imported_by Map)
 126  , Proj_Con cs
 127  , Inj_Const cs Ord
 128  ) => Proj_ConC cs (Proxy Map) where
 129         proj_conC _ (TyConst q :$ (TyConst c :$ _k))
 130          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 131          , Just Refl <- proj_const c (Proxy::Proxy Map)
 132          = case () of
 133                  _ | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
 134                    | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
 135                    | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
 136                  _ -> Nothing
 137         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ k :$ a))
 138          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 139          , Just Refl <- proj_const c (Proxy::Proxy Map)
 140          = case () of
 141                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 142                    , Just Con  <- proj_con (t :$ k)
 143                    , Just Con  <- proj_con (t :$ a) -> Just Con
 144                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 145                    , Just Con  <- proj_con (t :$ k)
 146                    , Just Con  <- proj_con (t :$ a) -> Just Con
 147                    | Just Refl <- proj_const q (Proxy::Proxy Monoid)
 148                    , Just Con  <- proj_con (tyOrd :$ k) -> Just Con
 149                  _ -> Nothing
 150         proj_conC _c _q = Nothing
 151 instance -- Term_fromI
 152  ( AST ast
 153  , Lexem ast ~ LamVarName
 154  , Inj_Const (Consts_of_Ifaces is) Map
 155  , Inj_Const (Consts_of_Ifaces is) (->)
 156  , Inj_Const (Consts_of_Ifaces is) Bool
 157  , Inj_Const (Consts_of_Ifaces is) Ord
 158  , Inj_Const (Consts_of_Ifaces is) Maybe
 159  , Inj_Const (Consts_of_Ifaces is) []
 160  , Inj_Const (Consts_of_Ifaces is) (,)
 161  , Proj_Con  (Consts_of_Ifaces is)
 162  , Term_from is ast
 163  ) => Term_fromI is (Proxy Map) ast where
 164         term_fromI ast ctx k =
 165                 case ast_lexem ast of
 166                  "Map.fromList"     -> map_fromList_from
 167                  "Map.mapWithKey"   -> mapWithKey_from
 168                  "Map.lookup"       -> map_lookup_from
 169                  "Map.keys"         -> map_keys_from
 170                  "Map.member"       -> map_member_from
 171                  "Map.insert"       -> map_insert_from
 172                  "Map.delete"       -> map_delete_from
 173                  "Map.difference"   -> map_difference_from
 174                  "Map.foldrWithKey" -> map_foldrWithKey_from
 175                  _ -> Left $ Error_Term_unsupported
 176                 where
 177                 map_fromList_from =
 178                  -- fromList :: Ord k => [(k, a)] -> Map k a
 179                         from_ast1 ast $ \ast_l as ->
 180                         term_from ast_l ctx $ \ty_l (TermLC l) ->
 181                         check_type1 tyList ast_l ty_l $ \Refl ty_l_t2 ->
 182                         check_type2 tyTuple2 ast_l ty_l_t2 $ \Refl ty_k ty_a ->
 183                         check_constraint (At (Just ast_l) (tyOrd :$ ty_k)) $ \Con ->
 184                         k as ((tyMap :$ ty_k) :$ ty_a) $ TermLC $
 185                          \c -> map_fromList (l c)
 186                 mapWithKey_from =
 187                  -- map_mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
 188                         from_ast1 ast $ \ast_k2a2b as ->
 189                         term_from ast_k2a2b ctx $ \ty_k2a2b (TermLC k2a2b) ->
 190                         check_type2 tyFun ast_k2a2b ty_k2a2b $ \Refl ty_k ty_a2b ->
 191                         check_type2 tyFun ast_k2a2b ty_a2b $ \Refl ty_a ty_b ->
 192                         k as ((tyMap :$ ty_k) :$ ty_a ~> (tyMap :$ ty_k) :$ ty_b) $ TermLC $
 193                          \c -> lam $ map_mapWithKey (k2a2b c)
 194                 map_lookup_from =
 195                  -- lookup :: Ord k => k -> Map k a -> Maybe a
 196                         from_ast2 ast $ \ast_k ast_m as ->
 197                         term_from ast_k ctx $ \ty_k (TermLC k_) ->
 198                         term_from ast_m ctx $ \ty_m (TermLC m) ->
 199                         check_type2 tyMap ast_m ty_m $ \Refl ty_m_k ty_m_a ->
 200                         check_type (At (Just ast_k) ty_k) (At (Just ast_m) ty_m_k) $ \Refl ->
 201                         check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con ->
 202                         k as (tyMaybe :$ ty_m_a) $ TermLC $
 203                          \c -> map_lookup (k_ c) (m c)
 204                 map_keys_from =
 205                  -- keys :: Map k a -> [k]
 206                         from_ast1 ast $ \ast_m as ->
 207                         term_from ast_m ctx $ \ty_m (TermLC m) ->
 208                         check_type2 tyMap ast_m ty_m $ \Refl ty_m_k _ty_m_a ->
 209                         k as (tyList :$ ty_m_k) $ TermLC $
 210                          \c -> map_keys (m c)
 211                 map_member_from =
 212                  -- member :: Ord k => k -> Map k a -> Bool
 213                         from_ast2 ast $ \ast_k ast_m as ->
 214                         term_from ast_k ctx $ \ty_k (TermLC k_) ->
 215                         term_from ast_m ctx $ \ty_m (TermLC m) ->
 216                         check_type2 tyMap ast_m ty_m $ \Refl ty_m_k _ty_m_a ->
 217                         check_type (At (Just ast_k) ty_k) (At (Just ast_m) ty_m_k) $ \Refl ->
 218                         check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con ->
 219                         k as tyBool $ TermLC $
 220                          \c -> map_member (k_ c) (m c)
 221                 map_insert_from =
 222                  -- insert :: Ord k => k -> a -> Map k a -> Map k a
 223                         from_ast2 ast $ \ast_k ast_a as ->
 224                         term_from ast_k ctx $ \ty_k (TermLC k_) ->
 225                         term_from ast_a ctx $ \ty_a (TermLC a) ->
 226                         check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con ->
 227                         k as ((tyMap :$ ty_k) :$ ty_a ~> (tyMap :$ ty_k) :$ ty_a) $ TermLC $
 228                          \c -> lam $ map_insert (k_ c) (a c)
 229                 map_delete_from =
 230                  -- delete :: Ord k => k -> Map k a -> Map k a
 231                         from_ast2 ast $ \ast_k ast_m as ->
 232                         term_from ast_k ctx $ \ty_k (TermLC k_) ->
 233                         term_from ast_m ctx $ \ty_m (TermLC m) ->
 234                         check_type2 tyMap ast_m ty_m $ \Refl ty_m_k ty_m_a ->
 235                         check_type (At (Just ast_k) ty_k) (At (Just ast_m) ty_m_k) $ \Refl ->
 236                         check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con ->
 237                         k as ((tyMap :$ ty_k) :$ ty_m_a) $ TermLC $
 238                          \c -> map_delete (k_ c) (m c)
 239                 map_difference_from =
 240                  -- difference :: Ord k => Map k a -> Map k b -> Map k a
 241                         from_ast2 ast $ \ast_ma ast_mb as ->
 242                         term_from ast_ma ctx $ \ty_ma (TermLC ma) ->
 243                         term_from ast_mb ctx $ \ty_mb (TermLC mb) ->
 244                         check_type2 tyMap ast_ma ty_ma $ \Refl ty_ma_k ty_ma_a ->
 245                         check_type2 tyMap ast_mb ty_mb $ \Refl ty_mb_k _ty_mb_b ->
 246                         check_type (At (Just ast_ma) ty_ma_k) (At (Just ast_mb) ty_mb_k) $ \Refl ->
 247                         check_constraint (At (Just ast_ma) (tyOrd :$ ty_ma_k)) $ \Con ->
 248                         k as ((tyMap :$ ty_ma_k) :$ ty_ma_a) $ TermLC $
 249                          \c -> map_difference (ma c) (mb c)
 250                 map_foldrWithKey_from =
 251                  -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
 252                         from_ast1 ast $ \ast_f as ->
 253                         term_from ast_f ctx $ \ty_f (TermLC f) ->
 254                         check_type2 tyFun ast_f ty_f $ \Refl ty_k ty_fabb ->
 255                         check_type2 tyFun ast_f ty_fabb $ \Refl ty_a ty_fbb ->
 256                         check_type2 tyFun ast_f ty_fbb $ \Refl ty_b ty_b' ->
 257                         check_type (At (Just ast_f) ty_b) (At (Just ast_f) ty_b') $ \Refl ->
 258                         k as (ty_b ~> (tyMap :$ ty_k) :$ ty_a ~> ty_b) $ TermLC $
 259                          \c -> lam $ \b -> lam $ \m -> map_foldrWithKey (f c) b m
 260
 261 -- | The 'Map' 'Type'
 262 tyMap :: Inj_Const cs Map => Type cs Map
 263 tyMap = TyConst inj_const
 264
 265 sym_Map :: Proxy Sym_Map
 266 sym_Map = Proxy
 267
 268 syMap :: IsString a => [Syntax a] -> Syntax a
 269 syMap = Syntax "Map"