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