{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=12 #-} -- | Symantic for 'Map'. module Language.Symantic.Compiling.Map where import Control.Monad (liftM, liftM2, liftM3) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Proxy import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (either) import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class '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 :: (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 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 type instance Sym_of_Iface (Proxy Map) = Sym_Map type instance Consts_of_Iface (Proxy Map) = Proxy Map ': Consts_imported_by Map type instance Consts_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 ] 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 instance ( Read_TypeNameR Text cs rs , Inj_Const cs Map ) => Read_TypeNameR Text cs (Proxy Map ': rs) where read_typenameR _cs "Map" k = k (ty @Map) read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k instance Show_Const cs => Show_Const (Proxy Map ': cs) where show_const ConstZ{} = "Map" show_const (ConstS c) = show_const c instance -- Proj_ConC ( Proj_Const cs Map , Proj_Consts cs (Consts_imported_by Map) , Proj_Con cs , Inj_Const cs Ord ) => Proj_ConC cs (Proxy Map) where proj_conC _ (TyConst q :$ (TyConst c :$ _k)) | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) , Just Refl <- proj_const c (Proxy::Proxy Map) = case () of _ | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Foldable) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con _ -> Nothing proj_conC _ (t@(TyConst q) :$ (TyConst c :$ k :$ a)) | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType) , Just Refl <- proj_const c (Proxy::Proxy Map) = case () of _ | Just Refl <- proj_const q (Proxy::Proxy Eq) , Just Con <- proj_con (t :$ k) , Just Con <- proj_con (t :$ a) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Ord) , Just Con <- proj_con (t :$ k) , Just Con <- proj_con (t :$ a) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Monoid) , Just Con <- proj_con (ty @Ord :$ k) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Show) , Just Con <- proj_con (t :$ k) , Just Con <- proj_con (t :$ a) -> Just Con _ -> Nothing proj_conC _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_Const (Consts_of_Ifaces is) Map , Inj_Const (Consts_of_Ifaces is) (->) , Inj_Const (Consts_of_Ifaces is) Bool , Inj_Const (Consts_of_Ifaces is) Ord , Inj_Const (Consts_of_Ifaces is) Maybe , Inj_Const (Consts_of_Ifaces is) [] , Inj_Const (Consts_of_Ifaces is) (,) , Proj_Con (Consts_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_type1 (ty @[]) (At (Just tok_l) ty_l) $ \Refl ty_l_t2 -> check_type2 (ty @(,)) (At (Just tok_l) ty_l_t2) $ \Refl ty_k ty_a -> check_con (At (Just tok_l) (ty @Ord :$ ty_k)) $ \Con -> 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_type2 (ty @(->)) (At (Just tok_k2a2b) ty_k2a2b) $ \Refl ty_k ty_a2b -> check_type2 (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_type2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a -> check_type (At (Just tok_k) ty_k) (At (Just tok_m) ty_m_k) $ \Refl -> check_con (At (Just tok_k) (ty @Ord :$ ty_k)) $ \Con -> 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_type2 (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_type2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k _ty_m_a -> check_type (At (Just tok_k) ty_k) (At (Just tok_m) ty_m_k) $ \Refl -> check_con (At (Just tok_k) (ty @Ord :$ ty_k)) $ \Con -> 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_con (At (Just tok_k) (ty @Ord :$ ty_k)) $ \Con -> 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_type2 (ty @Map) (At (Just tok_m) ty_m) $ \Refl ty_m_k ty_m_a -> check_type (At (Just tok_k) ty_k) (At (Just tok_m) ty_m_k) $ \Refl -> check_con (At (Just tok_k) (ty @Ord :$ ty_k)) $ \Con -> 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_type2 (ty @Map) (At (Just tok_ma) ty_ma) $ \Refl ty_ma_k ty_ma_a -> check_type2 (ty @Map) (At (Just tok_mb) ty_mb) $ \Refl ty_mb_k _ty_mb_b -> check_type (At (Just tok_ma) ty_ma_k) (At (Just tok_mb) ty_mb_k) $ \Refl -> check_con (At (Just tok_ma) (ty @Ord :$ ty_ma_k)) $ \Con -> 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_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_k ty_fabb -> check_type2 (ty @(->)) (At (Just tok_f) ty_fabb) $ \Refl ty_a ty_fbb -> check_type2 (ty @(->)) (At (Just tok_f) ty_fbb) $ \Refl ty_b ty_b' -> check_type (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