symantic-lib/Language/Symantic/Lib/Map.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Map'.
   4 module Language.Symantic.Lib.Map where
   5
   6 import Data.Bool
   7 import Data.Eq (Eq)
   8 import Data.Foldable (Foldable)
   9 import Data.Function (($))
  10 import Data.Functor (Functor)
  11 import Data.Map.Strict (Map)
  12 import Data.Maybe (Maybe(..))
  13 import Data.MonoTraversable (MonoFunctor)
  14 import Data.Monoid (Monoid)
  15 import Data.Ord (Ord)
  16 import Data.Traversable (Traversable)
  17 import Text.Show (Show)
  18 import qualified Data.Map.Strict as Map
  19
  20 import Language.Symantic
  21 import Language.Symantic.Lib.Bool (tyBool)
  22 import Language.Symantic.Lib.Function (a0, b1)
  23 import Language.Symantic.Lib.List (tyList)
  24 import Language.Symantic.Lib.Maybe (tyMaybe)
  25 import Language.Symantic.Lib.MonoFunctor (Element)
  26 import Language.Symantic.Lib.Ord (tyOrd)
  27 import Language.Symantic.Lib.Tuple2 (tyTuple2)
  28
  29 -- * Class 'Sym_Map'
  30 type instance Sym Map = Sym_Map
  31 class Sym_Map term where
  32         map_fromList     :: Ord k => term [(k, a)] -> term (Map k a)
  33         map_mapWithKey   :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
  34         map_lookup       :: Ord k => term k -> term (Map k a) -> term (Maybe a)
  35         map_keys         :: term (Map k a) -> term [k]
  36         map_member       :: Ord k => term k -> term (Map k a) -> term Bool
  37         map_insert       :: Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
  38         map_delete       :: Ord k => term k -> term (Map k a) -> term (Map k a)
  39         map_difference   :: Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
  40         map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
  41
  42         default map_fromList     :: Sym_Map (UnT term) => Trans term => Ord k => term [(k, a)] -> term (Map k a)
  43         default map_mapWithKey   :: Sym_Map (UnT term) => Trans term          => term (k -> a -> b) -> term (Map k a) -> term (Map k b)
  44         default map_lookup       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Maybe a)
  45         default map_keys         :: Sym_Map (UnT term) => Trans term          => term (Map k a) -> term [k]
  46         default map_member       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term Bool
  47         default map_insert       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
  48         default map_delete       :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Map k a)
  49         default map_difference   :: Sym_Map (UnT term) => Trans term => Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
  50         default map_foldrWithKey :: Sym_Map (UnT term) => Trans term          => term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
  51
  52         map_fromList     = trans1 map_fromList
  53         map_mapWithKey   = trans2 map_mapWithKey
  54         map_lookup       = trans2 map_lookup
  55         map_keys         = trans1 map_keys
  56         map_member       = trans2 map_member
  57         map_insert       = trans3 map_insert
  58         map_delete       = trans2 map_delete
  59         map_difference   = trans2 map_difference
  60         map_foldrWithKey = trans3 map_foldrWithKey
  61
  62 -- Interpreting
  63 instance Sym_Map Eval where
  64         map_fromList     = eval1 Map.fromList
  65         map_mapWithKey   = eval2 Map.mapWithKey
  66         map_lookup       = eval2 Map.lookup
  67         map_keys         = eval1 Map.keys
  68         map_member       = eval2 Map.member
  69         map_insert       = eval3 Map.insert
  70         map_delete       = eval2 Map.delete
  71         map_difference   = eval2 Map.difference
  72         map_foldrWithKey = eval3 Map.foldrWithKey
  73 instance Sym_Map View where
  74         map_fromList     = view1 "Map.fromList"
  75         map_mapWithKey   = view2 "Map.mapWithKey"
  76         map_lookup       = view2 "Map.lookup"
  77         map_keys         = view1 "Map.keys"
  78         map_member       = view2 "Map.member"
  79         map_insert       = view3 "Map.insert"
  80         map_delete       = view2 "Map.delete"
  81         map_difference   = view2 "Map.difference"
  82         map_foldrWithKey = view3 "Map.foldrWithKey"
  83 instance (Sym_Map r1, Sym_Map r2) => Sym_Map (Dup r1 r2) where
  84         map_fromList     = dup1 @Sym_Map map_fromList
  85         map_mapWithKey   = dup2 @Sym_Map map_mapWithKey
  86         map_lookup       = dup2 @Sym_Map map_lookup
  87         map_keys         = dup1 @Sym_Map map_keys
  88         map_member       = dup2 @Sym_Map map_member
  89         map_insert       = dup3 @Sym_Map map_insert
  90         map_delete       = dup2 @Sym_Map map_delete
  91         map_difference   = dup2 @Sym_Map map_difference
  92         map_foldrWithKey = dup3 @Sym_Map map_foldrWithKey
  93
  94 -- Transforming
  95 instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)
  96
  97 -- Typing
  98 instance NameTyOf Map where
  99         nameTyOf _c = ["Map"] `Mod` "Map"
 100 instance FixityOf Map
 101 instance ClassInstancesFor Map where
 102         proveConstraintFor _ (TyConst _ _ q :$ m:@_k)
 103          | Just HRefl <- proj_ConstKiTy @_ @Map m
 104          = case () of
 105                  _ | Just Refl <- proj_Const @Functor     q -> Just Dict
 106                    | Just Refl <- proj_Const @Foldable    q -> Just Dict
 107                    | Just Refl <- proj_Const @Traversable q -> Just Dict
 108                  _ -> Nothing
 109         proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@k:@a)
 110          | Just HRefl <- proj_ConstKiTy @_ @Map m
 111          = case () of
 112                  _ | Just Refl <- proj_Const @Eq q
 113                    , Just Dict <- proveConstraint (tq`tyApp`k)
 114                    , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 115                    | Just Refl <- proj_Const @Ord q
 116                    , Just Dict <- proveConstraint (tq`tyApp`k)
 117                    , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 118                    | Just Refl <- proj_Const @Monoid q
 119                    , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict
 120                    | Just Refl <- proj_Const @Show q
 121                    , Just Dict <- proveConstraint (tq`tyApp`k)
 122                    , Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
 123                    | Just Refl <- proj_Const @MonoFunctor q -> Just Dict
 124                  _ -> Nothing
 125         proveConstraintFor _c _q = Nothing
 126 instance TypeInstancesFor Map where
 127         expandFamFor _c _len f (m:@_k:@a `TypesS` TypesZ)
 128          | Just HRefl <- proj_ConstKi @_ @Element f
 129          , Just HRefl <- proj_ConstKiTy @_ @Map m
 130          = Just a
 131         expandFamFor _c _len _fam _as = Nothing
 132
 133 -- Compiling
 134 instance Gram_Term_AtomsFor src ss g Map
 135 instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
 136         moduleFor = ["Map"] `moduleWhere`
 137          [ "delete"       := teMap_delete
 138          , "difference"   := teMap_difference
 139          , "foldrWithKey" := teMap_foldrWithKey
 140          , "fromList"     := teMap_fromList
 141          , "insert"       := teMap_insert
 142          , "keys"         := teMap_keys
 143          , "lookup"       := teMap_lookup
 144          , "mapWithKey"   := teMap_mapWithKey
 145          , "member"       := teMap_member
 146          ]
 147
 148 -- ** 'Type's
 149 tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
 150 tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a
 151
 152 k1 :: Source src => LenInj vs => KindInj (K k) =>
 153      Type src (a ': Proxy k ': vs) k
 154 k1 = tyVar "k" $ VarS varZ
 155
 156 k2 :: Source src => LenInj vs => KindInj (K k) =>
 157      Type src (a ': b ': Proxy k ': vs) k
 158 k2 = tyVar "k" $ VarS $ VarS varZ
 159
 160 -- ** 'Term's
 161 teMap_delete :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Map k a))
 162 teMap_delete = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam2 map_delete
 163
 164 teMap_insert :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> a -> Map k a -> Map k a))
 165 teMap_insert = Term (tyOrd k1) (k1 ~> a0 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam3 map_insert
 166
 167 teMap_difference :: TermDef Map '[Proxy a, Proxy b, Proxy k] (Ord k #> (Map k a -> Map k b -> Map k a))
 168 teMap_difference = Term (tyOrd k2) (tyMap k2 a0 ~> tyMap k2 b1 ~> tyMap k2 a0) $ teSym @Map $ lam2 map_difference
 169
 170 teMap_fromList :: TermDef Map '[Proxy a, Proxy k] (Ord k #> ([(k, a)] -> Map k a))
 171 teMap_fromList = Term (tyOrd k1) (tyList (tyTuple2 k1 a0) ~> tyMap k1 a0) $ teSym @Map $ lam1 map_fromList
 172
 173 teMap_lookup :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Maybe a))
 174 teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $ lam2 map_lookup
 175
 176 teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))
 177 teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member
 178
 179 teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))
 180 teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey
 181
 182 teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))
 183 teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey
 184
 185 teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))
 186 teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys