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