module Language.Symantic.Lib.Map where
import Data.Map.Strict (Map)
import Data.MonoTraversable (MonoFunctor)
import qualified Data.Map.Strict as Map
import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Function (a0, b1)
import Language.Symantic.Lib.List (tyList)
import Language.Symantic.Lib.Maybe (tyMaybe)
import Language.Symantic.Lib.MonoFunctor (Element)
import Language.Symantic.Lib.Ord (tyOrd)
import Language.Symantic.Lib.Tuple2 (tyTuple2)
type instance Sym Map = Sym_Map
class Sym_Map term where
map_fromList :: Ord k => term [(k, a)] -> term (Map k a)
map_mapWithKey :: term (k -> a -> b) -> term (Map k a) -> term (Map k b)
map_lookup :: Ord k => term k -> term (Map k a) -> term (Maybe a)
map_keys :: term (Map k a) -> term [k]
map_member :: Ord k => term k -> term (Map k a) -> term Bool
map_insert :: Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
map_delete :: Ord k => term k -> term (Map k a) -> term (Map k a)
map_difference :: Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
map_foldrWithKey :: term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
default map_fromList :: Sym_Map (UnT term) => Trans term => Ord k => term [(k, a)] -> term (Map k a)
default map_mapWithKey :: Sym_Map (UnT term) => Trans term => term (k -> a -> b) -> term (Map k a) -> term (Map k b)
default map_lookup :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Maybe a)
default map_keys :: Sym_Map (UnT term) => Trans term => term (Map k a) -> term [k]
default map_member :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term Bool
default map_insert :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term a -> term (Map k a) -> term (Map k a)
default map_delete :: Sym_Map (UnT term) => Trans term => Ord k => term k -> term (Map k a) -> term (Map k a)
default map_difference :: Sym_Map (UnT term) => Trans term => Ord k => term (Map k a) -> term (Map k b) -> term (Map k a)
default map_foldrWithKey :: Sym_Map (UnT term) => Trans term => term (k -> a -> b -> b) -> term b -> term (Map k a) -> term b
map_fromList = trans1 map_fromList
map_mapWithKey = trans2 map_mapWithKey
map_lookup = trans2 map_lookup
map_keys = trans1 map_keys
map_member = trans2 map_member
map_insert = trans3 map_insert
map_delete = trans2 map_delete
map_difference = trans2 map_difference
map_foldrWithKey = trans3 map_foldrWithKey
instance Sym_Map Eval where
map_fromList = eval1 Map.fromList
map_mapWithKey = eval2 Map.mapWithKey
map_lookup = eval2 Map.lookup
map_keys = eval1 Map.keys
map_member = eval2 Map.member
map_insert = eval3 Map.insert
map_delete = eval2 Map.delete
map_difference = eval2 Map.difference
map_foldrWithKey = eval3 Map.foldrWithKey
instance Sym_Map View where
map_fromList = view1 "Map.fromList"
map_mapWithKey = view2 "Map.mapWithKey"
map_lookup = view2 "Map.lookup"
map_keys = view1 "Map.keys"
map_member = view2 "Map.member"
map_insert = view3 "Map.insert"
map_delete = view2 "Map.delete"
map_difference = view2 "Map.difference"
map_foldrWithKey = view3 "Map.foldrWithKey"
instance (Sym_Map r1, Sym_Map r2) => Sym_Map (Dup r1 r2) where
map_fromList = dup1 @Sym_Map map_fromList
map_mapWithKey = dup2 @Sym_Map map_mapWithKey
map_lookup = dup2 @Sym_Map map_lookup
map_keys = dup1 @Sym_Map map_keys
map_member = dup2 @Sym_Map map_member
map_insert = dup3 @Sym_Map map_insert
map_delete = dup2 @Sym_Map map_delete
map_difference = dup2 @Sym_Map map_difference
map_foldrWithKey = dup3 @Sym_Map map_foldrWithKey
instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)
instance NameTyOf Map where
nameTyOf _c = ["Map"] `Mod` "Map"
instance FixityOf Map
instance ClassInstancesFor Map where
proveConstraintFor _ (TyConst _ _ q :$ m:@_k)
| Just HRefl <- proj_ConstKiTy @_ @Map m
= case () of
_ | Just Refl <- proj_Const @Functor q -> Just Dict
| Just Refl <- proj_Const @Foldable q -> Just Dict
| Just Refl <- proj_Const @Traversable q -> Just Dict
_ -> Nothing
proveConstraintFor _ (tq@(TyConst _ _ q) :$ m:@k:@a)
| Just HRefl <- proj_ConstKiTy @_ @Map m
= case () of
_ | Just Refl <- proj_Const @Eq q
, Just Dict <- proveConstraint (tq`tyApp`k)
, Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @Ord q
, Just Dict <- proveConstraint (tq`tyApp`k)
, Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @Monoid q
, Just Dict <- proveConstraint (tyConstLen @(K Ord) @Ord (lenVars k) `tyApp` k) -> Just Dict
| Just Refl <- proj_Const @Show q
, Just Dict <- proveConstraint (tq`tyApp`k)
, Just Dict <- proveConstraint (tq`tyApp`a) -> Just Dict
| Just Refl <- proj_Const @MonoFunctor q -> Just Dict
_ -> Nothing
proveConstraintFor _c _q = Nothing
instance TypeInstancesFor Map where
expandFamFor _c _len f (m:@_k:@a `TypesS` TypesZ)
| Just HRefl <- proj_ConstKi @_ @Element f
, Just HRefl <- proj_ConstKiTy @_ @Map m
= Just a
expandFamFor _c _len _fam _as = Nothing
instance Gram_Term_AtomsFor src ss g Map
instance (Source src, SymInj ss Map) => ModuleFor src ss Map where
moduleFor = ["Map"] `moduleWhere`
[ "delete" := teMap_delete
, "difference" := teMap_difference
, "foldrWithKey" := teMap_foldrWithKey
, "fromList" := teMap_fromList
, "insert" := teMap_insert
, "keys" := teMap_keys
, "lookup" := teMap_lookup
, "mapWithKey" := teMap_mapWithKey
, "member" := teMap_member
]
tyMap :: Source src => LenInj vs => Type src vs k -> Type src vs a -> Type src vs (Map k a)
tyMap k a = tyConst @(K Map) @Map `tyApp` k `tyApp` a
k1 :: Source src => LenInj vs => KindInj (K k) =>
Type src (a ': Proxy k ': vs) k
k1 = tyVar "k" $ VarS varZ
k2 :: Source src => LenInj vs => KindInj (K k) =>
Type src (a ': b ': Proxy k ': vs) k
k2 = tyVar "k" $ VarS $ VarS varZ
teMap_delete :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Map k a))
teMap_delete = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam2 map_delete
teMap_insert :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> a -> Map k a -> Map k a))
teMap_insert = Term (tyOrd k1) (k1 ~> a0 ~> tyMap k1 a0 ~> tyMap k1 a0) $ teSym @Map $ lam3 map_insert
teMap_difference :: TermDef Map '[Proxy a, Proxy b, Proxy k] (Ord k #> (Map k a -> Map k b -> Map k a))
teMap_difference = Term (tyOrd k2) (tyMap k2 a0 ~> tyMap k2 b1 ~> tyMap k2 a0) $ teSym @Map $ lam2 map_difference
teMap_fromList :: TermDef Map '[Proxy a, Proxy k] (Ord k #> ([(k, a)] -> Map k a))
teMap_fromList = Term (tyOrd k1) (tyList (tyTuple2 k1 a0) ~> tyMap k1 a0) $ teSym @Map $ lam1 map_fromList
teMap_lookup :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Maybe a))
teMap_lookup = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyMaybe a0) $ teSym @Map $ lam2 map_lookup
teMap_member :: TermDef Map '[Proxy a, Proxy k] (Ord k #> (k -> Map k a -> Bool))
teMap_member = Term (tyOrd k1) (k1 ~> tyMap k1 a0 ~> tyBool) $ teSym @Map $ lam2 map_member
teMap_foldrWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b -> b) -> b -> Map k a -> b))
teMap_foldrWithKey = Term noConstraint ((k2 ~> a0 ~> b1 ~> b1) ~> b1 ~> tyMap k2 a0 ~> b1) $ teSym @Map $ lam3 map_foldrWithKey
teMap_mapWithKey :: TermDef Map '[Proxy a, Proxy b, Proxy k] (() #> ((k -> a -> b) -> Map k a -> Map k b))
teMap_mapWithKey = Term noConstraint ((k2 ~> a0 ~> b1) ~> tyMap k2 a0 ~> tyMap k2 b1) $ teSym @Map $ lam2 map_mapWithKey
teMap_keys :: TermDef Map '[Proxy a, Proxy k] (() #> (Map k a -> [k]))
teMap_keys = Term noConstraint (tyMap k1 a0 ~> tyList k1) $ teSym @Map $ lam1 map_keys