{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=12 #-}
-- | Symantic for 'Map'.
module Language.Symantic.Lib.Map where
-import Control.Monad (liftM, liftM2, liftM3)
import Data.Map.Strict (Map)
+import Data.MonoTraversable (MonoFunctor)
import qualified Data.Map.Strict as Map
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
-import Prelude hiding (either)
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
+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)
-- * Class 'Sym_Map'
+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_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 :: (Trans t term, Ord k) => t term [(k, a)] -> t term (Map k a)
- default map_mapWithKey :: Trans t term => t term (k -> a -> b) -> t term (Map k a) -> t term (Map k b)
- default map_lookup :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Maybe a)
- default map_keys :: Trans t term => t term (Map k a) -> t term [k]
- default map_member :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term Bool
- default map_insert :: (Trans t term, Ord k) => t term k -> t term a -> t term (Map k a) -> t term (Map k a)
- default map_delete :: (Trans t term, Ord k) => t term k -> t term (Map k a) -> t term (Map k a)
- default map_difference :: (Trans t term, Ord k) => t term (Map k a) -> t term (Map k b) -> t term (Map k a)
- default map_foldrWithKey :: Trans t term => t term (k -> a -> b -> b) -> t term b -> t term (Map k a) -> t 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 = trans_map1 map_fromList
- map_mapWithKey = trans_map2 map_mapWithKey
- map_lookup = trans_map2 map_lookup
- map_keys = trans_map1 map_keys
- map_member = trans_map2 map_member
- map_insert = trans_map3 map_insert
- map_delete = trans_map2 map_delete
- map_difference = trans_map2 map_difference
- map_foldrWithKey = trans_map3 map_foldrWithKey
+ 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
-type instance Sym_of_Iface (Proxy Map) = Sym_Map
-type instance TyConsts_of_Iface (Proxy Map) = Proxy Map ': TyConsts_imported_by Map
-type instance TyConsts_imported_by Map =
- [ Proxy (->)
- , Proxy []
- , Proxy (,)
- , Proxy Bool
- , Proxy Eq
- , Proxy Foldable
- , Proxy Functor
- , Proxy Maybe
- , Proxy Monad
- , Proxy Monoid
- , Proxy Ord
- , Proxy Traversable
- , Proxy Show
- ]
+-- Interpreting
+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 HostI where
- map_fromList = liftM Map.fromList
- map_mapWithKey = liftM2 Map.mapWithKey
- map_lookup = liftM2 Map.lookup
- map_keys = liftM Map.keys
- map_member = liftM2 Map.member
- map_insert = liftM3 Map.insert
- map_delete = liftM2 Map.delete
- map_difference = liftM2 Map.difference
- map_foldrWithKey = liftM3 Map.foldrWithKey
-instance Sym_Map TextI where
- map_fromList = textI1 "Map.fromList"
- map_mapWithKey = textI2 "Map.mapWithKey"
- map_lookup = textI2 "Map.lookup"
- map_keys = textI1 "Map.keys"
- map_member = textI2 "Map.member"
- map_insert = textI3 "Map.insert"
- map_delete = textI2 "Map.delete"
- map_difference = textI2 "Map.difference"
- map_foldrWithKey = textI3 "Map.foldrWithKey"
-instance (Sym_Map r1, Sym_Map r2) => Sym_Map (DupI r1 r2) where
- map_fromList = dupI1 (Proxy @Sym_Map) map_fromList
- map_mapWithKey = dupI2 (Proxy @Sym_Map) map_mapWithKey
- map_lookup = dupI2 (Proxy @Sym_Map) map_lookup
- map_keys = dupI1 (Proxy @Sym_Map) map_keys
- map_member = dupI2 (Proxy @Sym_Map) map_member
- map_insert = dupI3 (Proxy @Sym_Map) map_insert
- map_delete = dupI2 (Proxy @Sym_Map) map_delete
- map_difference = dupI2 (Proxy @Sym_Map) map_difference
- map_foldrWithKey = dupI3 (Proxy @Sym_Map) map_foldrWithKey
+-- Transforming
+instance (Sym_Map term, Sym_Lambda term) => Sym_Map (BetaT term)
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs Map
- ) => Read_TyNameR TyName cs (Proxy Map ': rs) where
- read_TyNameR _cs (TyName "Map") k = k (ty @Map)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance Show_TyConst cs => Show_TyConst (Proxy Map ': cs) where
- show_TyConst TyConstZ{} = "Map"
- show_TyConst (TyConstS c) = show_TyConst c
-
-instance -- Proj_TyConC
- ( Proj_TyConst cs Map
- , Proj_TyConsts cs (TyConsts_imported_by Map)
- , Proj_TyCon cs
- , Inj_TyConst cs Ord
- ) => Proj_TyConC cs (Proxy Map) where
- proj_TyConC _ (TyConst q :$ (TyConst c :$ _k))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Map)
+-- Typing
+instance FixityOf Map
+instance ClassInstancesFor Map where
+ proveConstraintFor _ (TyApp _ (TyConst _ _ q) (TyApp _ c _k))
+ | Just HRefl <- proj_ConstKiTy @_ @Map c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Foldable) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
+ _ | 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
- proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ k :$ a))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @Map)
+ proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ (TyApp _ c k) a))
+ | Just HRefl <- proj_ConstKiTy @_ @Map c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Eq)
- , Just TyCon <- proj_TyCon (t :$ k)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord)
- , Just TyCon <- proj_TyCon (t :$ k)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monoid)
- , Just TyCon <- proj_TyCon (ty @Ord :$ k) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Show)
- , Just TyCon <- proj_TyCon (t :$ k)
- , Just TyCon <- proj_TyCon (t :$ a) -> Just TyCon
+ _ | 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
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy Map)
- = Token_Term_Map_fromList (EToken meta ts)
- | Token_Term_Map_mapWithKey (EToken meta ts)
- | Token_Term_Map_lookup (EToken meta ts) (EToken meta ts)
- | Token_Term_Map_keys (EToken meta ts)
- | Token_Term_Map_member (EToken meta ts) (EToken meta ts)
- | Token_Term_Map_insert (EToken meta ts) (EToken meta ts)
- | Token_Term_Map_delete (EToken meta ts) (EToken meta ts)
- | Token_Term_Map_difference (EToken meta ts) (EToken meta ts)
- | Token_Term_Map_foldrWithKey (EToken meta ts)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy Map))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy Map))
-instance -- CompileI
- ( Inj_TyConst (TyConsts_of_Ifaces is) Map
- , Inj_TyConst (TyConsts_of_Ifaces is) (->)
- , Inj_TyConst (TyConsts_of_Ifaces is) Bool
- , Inj_TyConst (TyConsts_of_Ifaces is) Ord
- , Inj_TyConst (TyConsts_of_Ifaces is) Maybe
- , Inj_TyConst (TyConsts_of_Ifaces is) []
- , Inj_TyConst (TyConsts_of_Ifaces is) (,)
- , Proj_TyCon (TyConsts_of_Ifaces is)
- , Compile is
- ) => CompileI is (Proxy Map) where
- compileI tok ctx k =
- case tok of
- Token_Term_Map_fromList tok_l ->
- -- fromList :: Ord k => [(k, a)] -> Map k a
- compileO tok_l ctx $ \ty_l (TermO l) ->
- check_TyEq1 (ty @[]) (At (Just tok_l) ty_l) $ \Refl ty_l_t2 ->
- check_TyEq2 (ty @(,)) (At (Just tok_l) ty_l_t2) $ \Refl ty_k ty_a ->
- check_TyCon (At (Just tok_l) (ty @Ord :$ ty_k)) $ \TyCon ->
- k ((ty @Map :$ ty_k) :$ ty_a) $ TermO $
- \c -> map_fromList (l c)
- Token_Term_Map_mapWithKey tok_k2a2b ->
- -- map_mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
- compileO tok_k2a2b ctx $ \ty_k2a2b (TermO k2a2b) ->
- check_TyEq2 (ty @(->)) (At (Just tok_k2a2b) ty_k2a2b) $ \Refl ty_k ty_a2b ->
- check_TyEq2 (ty @(->)) (At (Just tok_k2a2b) ty_a2b) $ \Refl ty_a ty_b ->
- k ((ty @Map :$ ty_k) :$ ty_a ~> (ty @Map :$ ty_k) :$ ty_b) $ TermO $
- \c -> lam $ map_mapWithKey (k2a2b c)
- Token_Term_Map_lookup tok_k tok_m ->
- -- lookup :: Ord k => k -> Map k a -> Maybe a
- compileO tok_k ctx $ \ty_k (TermO k_) ->
- compileO tok_m ctx $ \ty_m (TermO m) ->
- check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a ->
- check_TyEq
- (At (Just tok_k) ty_k)
- (At (Just tok_m) ty_m_k) $ \Refl ->
- check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
- k (ty @Maybe :$ ty_m_a) $ TermO $
- \c -> map_lookup (k_ c) (m c)
- Token_Term_Map_keys tok_m ->
- -- keys :: Map k a -> [k]
- compileO tok_m ctx $ \ty_m (TermO m) ->
- check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k _ty_m_a ->
- k (ty @[] :$ ty_m_k) $ TermO $
- \c -> map_keys (m c)
- Token_Term_Map_member tok_k tok_m ->
- -- member :: Ord k => k -> Map k a -> Bool
- compileO tok_k ctx $ \ty_k (TermO k_) ->
- compileO tok_m ctx $ \ty_m (TermO m) ->
- check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k _ty_m_a ->
- check_TyEq
- (At (Just tok_k) ty_k)
- (At (Just tok_m) ty_m_k) $ \Refl ->
- check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
- k (ty @Bool) $ TermO $
- \c -> map_member (k_ c) (m c)
- Token_Term_Map_insert tok_k tok_a ->
- -- insert :: Ord k => k -> a -> Map k a -> Map k a
- compileO tok_k ctx $ \ty_k (TermO k_) ->
- compileO tok_a ctx $ \ty_a (TermO a) ->
- check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
- k ((ty @Map :$ ty_k) :$ ty_a ~> (ty @Map :$ ty_k) :$ ty_a) $ TermO $
- \c -> lam $ map_insert (k_ c) (a c)
- Token_Term_Map_delete tok_k tok_m ->
- -- delete :: Ord k => k -> Map k a -> Map k a
- compileO tok_k ctx $ \ty_k (TermO k_) ->
- compileO tok_m ctx $ \ty_m (TermO m) ->
- check_TyEq2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a ->
- check_TyEq
- (At (Just tok_k) ty_k)
- (At (Just tok_m) ty_m_k) $ \Refl ->
- check_TyCon (At (Just tok_k) (ty @Ord :$ ty_k)) $ \TyCon ->
- k (((ty @Map) :$ ty_k) :$ ty_m_a) $ TermO $
- \c -> map_delete (k_ c) (m c)
- Token_Term_Map_difference tok_ma tok_mb ->
- -- difference :: Ord k => Map k a -> Map k b -> Map k a
- compileO tok_ma ctx $ \ty_ma (TermO ma) ->
- compileO tok_mb ctx $ \ty_mb (TermO mb) ->
- check_TyEq2 (ty @Map) (At (Just tok_ma) ty_ma) $ \Refl ty_ma_k ty_ma_a ->
- check_TyEq2 (ty @Map) (At (Just tok_mb) ty_mb) $ \Refl ty_mb_k _ty_mb_b ->
- check_TyEq
- (At (Just tok_ma) ty_ma_k)
- (At (Just tok_mb) ty_mb_k) $ \Refl ->
- check_TyCon (At (Just tok_ma) (ty @Ord :$ ty_ma_k)) $ \TyCon ->
- k ((ty @Map :$ ty_ma_k) :$ ty_ma_a) $ TermO $
- \c -> map_difference (ma c) (mb c)
- Token_Term_Map_foldrWithKey tok_f ->
- -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
- compileO tok_f ctx $ \ty_f (TermO f) ->
- check_TyEq2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_k ty_fabb ->
- check_TyEq2 (ty @(->)) (At (Just tok_f) ty_fabb) $ \Refl ty_a ty_fbb ->
- check_TyEq2 (ty @(->)) (At (Just tok_f) ty_fbb) $ \Refl ty_b ty_b' ->
- check_TyEq
- (At (Just tok_f) ty_b)
- (At (Just tok_f) ty_b') $ \Refl ->
- k (ty_b ~> (ty @Map :$ ty_k) :$ ty_a ~> ty_b) $ TermO $
- \c -> lam $ \b -> lam $ \m -> map_foldrWithKey (f c) b m
-instance -- TokenizeT
- Inj_Token meta ts Map =>
- TokenizeT meta ts (Proxy Map) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod [Mod_Name "Map"]
- [ tokenize1 "fromList" infixN5 Token_Term_Map_fromList
- , tokenize1 "mapWithKey" infixN5 Token_Term_Map_mapWithKey
- , tokenize2 "lookup" infixN5 Token_Term_Map_lookup
- , tokenize1 "keys" infixN5 Token_Term_Map_keys
- , tokenize2 "member" infixN5 Token_Term_Map_member
- , tokenize2 "insert" infixN5 Token_Term_Map_insert
- , tokenize2 "delete" infixN5 Token_Term_Map_delete
- , tokenize2 "difference" infixN5 Token_Term_Map_difference
- , tokenize1 "foldrWithKey" infixN5 Token_Term_Map_foldrWithKey
- ]
- }
-instance Gram_Term_AtomsT meta ts (Proxy Map) g
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor Map where
+ expandFamFor _c _len f (TyApp _ (TyApp _ c _k) a `TypesS` TypesZ)
+ | Just HRefl <- proj_ConstKi @_ @Element f
+ , Just HRefl <- proj_ConstKiTy @_ @Map c
+ = Just a
+ expandFamFor _c _len _fam _as = Nothing
+
+-- Compiling
+instance Gram_Term_AtomsFor src ss g Map
+instance (Source src, Inj_Sym 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
+ ]
+
+-- ** 'Type's
+tyMap :: Source src => Inj_Len 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 => Inj_Len vs => Inj_Kind (K k) =>
+ Type src (a ': Proxy k ': vs) k
+k1 = tyVar "k" $ VarS varZ
+
+k2 :: Source src => Inj_Len vs => Inj_Kind (K k) =>
+ Type src (a ': b ': Proxy k ': vs) k
+k2 = tyVar "k" $ VarS $ VarS varZ
+
+-- ** 'Term's
+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
sourcephile / git / haskell / symantic.git / blobdiff