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 FixityOf Map
  89 instance ClassInstancesFor Map where
  90         proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))
  91          | Just HRefl <- proj_ConstKiTy @_ @Map c
  92          = case () of
  93                  _ | Just Refl <- proj_Const @Functor     q -> Just Dict
  94                    | Just Refl <- proj_Const @Foldable    q -> Just Dict
  95                    | Just Refl <- proj_Const @Traversable q -> Just Dict
  96                  _ -> Nothing
  97         proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c k) a))
  98          | Just HRefl <- proj_ConstKiTy @_ @Map c
  99          = case () of
 100                  _ | Just Refl <- proj_Const @Eq q
 101                    , Just Dict <- proveConstraint (tq `tyApp` k)
 102                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
 103                    | Just Refl <- proj_Const @Ord q
 104                    , Just Dict <- proveConstraint (tq `tyApp` k)
 105                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
 106                    | Just Refl <- proj_Const @Monoid q
 107                    , Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict
 108                    | Just Refl <- proj_Const @Show q
 109                    , Just Dict <- proveConstraint (tq `tyApp` k)
 110                    , Just Dict <- proveConstraint (tq `tyApp` a) -> Just Dict
 111                    | Just Refl <- proj_Const @MonoFunctor q -> Just Dict
 112                  _ -> Nothing
 113         proveConstraintFor _c _q = Nothing
 114 instance TypeInstancesFor Map where
 115         expandFamFor _c _len f (TyApp _ (TyApp _ c _k) a `TypesS` TypesZ)
 116          | Just HRefl <- proj_ConstKi @_ @Element f
 117          , Just HRefl <- proj_ConstKiTy @_ @Map c
 118          = Just a
 119         expandFamFor _c _len _fam _as = Nothing
 120
 121 -- Compiling
 122 instance Gram_Term_AtomsFor src ss g Map
 123 instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
 124         moduleFor = ["Map"] `moduleWhere`
 125          [ "delete"       := teMap_delete
 126          , "difference"   := teMap_difference
 127          , "foldrWithKey" := teMap_foldrWithKey
 128          , "fromList"     := teMap_fromList
 129          , "insert"       := teMap_insert
 130          , "keys"         := teMap_keys
 131          , "lookup"       := teMap_lookup
 132          , "mapWithKey"   := teMap_mapWithKey
 133          , "member"       := teMap_member
 134          ]
 135
 136 -- ** 'Type's
 137 tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
 138 tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a
 139
 140 k1 :: Source src => LenInj vs => KindInj (K k) =>
 141      Type src (a ': Proxy k ': vs) k
 142 k1 = tyVar "k" $ VarS varZ
 143
 144 k2 :: Source src => LenInj vs => KindInj (K k) =>
 145      Type src (a ': b ': Proxy k ': vs) k
 146 k2 = tyVar "k" $ VarS $ VarS varZ
 147
 148 -- ** 'Term's
 149 teMap_delete :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Map k a))
 150 teMap_delete = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam2 map_delete
 151
 152 teMap_insert :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> a -> Map k a -> Map k a))
 153 teMap_insert = Term (tyOrd k1) (k1 ~> a0 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam3 map_insert
 154
 155 teMap_difference :: TermDef Map '[Proxy a, Proxy b, Proxy k] (Ord k #> (Map k a -> Map k b -> Map k a))
 156 teMap_difference = Term (tyOrd k2) (tyMap k2 a0 ~> tyMap k2 b1 ~> tyMap k2 a0) $ teSym @Map $ lam2 map_difference
 157
 158 teMap_fromList :: TermDef Map '[Proxy a, Proxy k] (Ord k #> ([(k, a)] -> Map k a))
 159 teMap_fromList = Term (tyOrd k1) (tyList (tyTuple2 k1 a0) ~> tyMap k1 a0) $ teSym @Map $ lam1 map_fromList
 160
 161 teMap_lookup :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Maybe a))
 162 teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $ lam2 map_lookup
 163
 164 teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))
 165 teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member
 166
 167 teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))
 168 teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey
 169
 170 teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))
 171 teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey
 172
 173 teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))
 174 teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys