{-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=11 #-} -- | 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.String (IsString) import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl)) import Prelude hiding (either) import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Compiling.Bool (tyBool) import Language.Symantic.Compiling.List (tyList) import Language.Symantic.Compiling.Ord (tyOrd) import Language.Symantic.Compiling.Maybe (tyMaybe) import Language.Symantic.Compiling.Tuple2 (tyTuple2) 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 ] 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 = textI_app1 "Map.fromList" map_mapWithKey = textI_app2 "Map.mapWithKey" map_lookup = textI_app2 "Map.lookup" map_keys = textI_app1 "Map.keys" map_member = textI_app2 "Map.member" map_insert = textI_app3 "Map.insert" map_delete = textI_app2 "Map.delete" map_difference = textI_app2 "Map.difference" map_foldrWithKey = textI_app3 "Map.foldrWithKey" instance (Sym_Map r1, Sym_Map r2) => Sym_Map (DupI r1 r2) where map_fromList = dupI1 sym_Map map_fromList map_mapWithKey = dupI2 sym_Map map_mapWithKey map_lookup = dupI2 sym_Map map_lookup map_keys = dupI1 sym_Map map_keys map_member = dupI2 sym_Map map_member map_insert = dupI3 sym_Map map_insert map_delete = dupI2 sym_Map map_delete map_difference = dupI2 sym_Map map_difference map_foldrWithKey = dupI3 sym_Map map_foldrWithKey instance Const_from Text cs => Const_from Text (Proxy Map ': cs) where const_from "Map" k = k (ConstZ kind) const_from s k = const_from s $ k . ConstS 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 (tyOrd :$ k) -> Just Con _ -> Nothing proj_conC _c _q = Nothing instance -- Term_fromI ( AST ast , Lexem ast ~ LamVarName , 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) , Term_from is ast ) => Term_fromI is (Proxy Map) ast where term_fromI ast ctx k = case ast_lexem ast of "Map.fromList" -> map_fromList_from "Map.mapWithKey" -> mapWithKey_from "Map.lookup" -> map_lookup_from "Map.keys" -> map_keys_from "Map.member" -> map_member_from "Map.insert" -> map_insert_from "Map.delete" -> map_delete_from "Map.difference" -> map_difference_from "Map.foldrWithKey" -> map_foldrWithKey_from _ -> Left $ Error_Term_unsupported where map_fromList_from = -- fromList :: Ord k => [(k, a)] -> Map k a from_ast1 ast $ \ast_l as -> term_from ast_l ctx $ \ty_l (TermLC l) -> check_type1 tyList ast_l ty_l $ \Refl ty_l_t2 -> check_type2 tyTuple2 ast_l ty_l_t2 $ \Refl ty_k ty_a -> check_constraint (At (Just ast_l) (tyOrd :$ ty_k)) $ \Con -> k as ((tyMap :$ ty_k) :$ ty_a) $ TermLC $ \c -> map_fromList (l c) mapWithKey_from = -- map_mapWithKey :: (k -> a -> b) -> Map k a -> Map k b from_ast1 ast $ \ast_k2a2b as -> term_from ast_k2a2b ctx $ \ty_k2a2b (TermLC k2a2b) -> check_type2 tyFun ast_k2a2b ty_k2a2b $ \Refl ty_k ty_a2b -> check_type2 tyFun ast_k2a2b ty_a2b $ \Refl ty_a ty_b -> k as ((tyMap :$ ty_k) :$ ty_a ~> (tyMap :$ ty_k) :$ ty_b) $ TermLC $ \c -> lam $ map_mapWithKey (k2a2b c) map_lookup_from = -- lookup :: Ord k => k -> Map k a -> Maybe a from_ast2 ast $ \ast_k ast_m as -> term_from ast_k ctx $ \ty_k (TermLC k_) -> term_from ast_m ctx $ \ty_m (TermLC m) -> check_type2 tyMap ast_m ty_m $ \Refl ty_m_k ty_m_a -> check_type (At (Just ast_k) ty_k) (At (Just ast_m) ty_m_k) $ \Refl -> check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con -> k as (tyMaybe :$ ty_m_a) $ TermLC $ \c -> map_lookup (k_ c) (m c) map_keys_from = -- keys :: Map k a -> [k] from_ast1 ast $ \ast_m as -> term_from ast_m ctx $ \ty_m (TermLC m) -> check_type2 tyMap ast_m ty_m $ \Refl ty_m_k _ty_m_a -> k as (tyList :$ ty_m_k) $ TermLC $ \c -> map_keys (m c) map_member_from = -- member :: Ord k => k -> Map k a -> Bool from_ast2 ast $ \ast_k ast_m as -> term_from ast_k ctx $ \ty_k (TermLC k_) -> term_from ast_m ctx $ \ty_m (TermLC m) -> check_type2 tyMap ast_m ty_m $ \Refl ty_m_k _ty_m_a -> check_type (At (Just ast_k) ty_k) (At (Just ast_m) ty_m_k) $ \Refl -> check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con -> k as tyBool $ TermLC $ \c -> map_member (k_ c) (m c) map_insert_from = -- insert :: Ord k => k -> a -> Map k a -> Map k a from_ast2 ast $ \ast_k ast_a as -> term_from ast_k ctx $ \ty_k (TermLC k_) -> term_from ast_a ctx $ \ty_a (TermLC a) -> check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con -> k as ((tyMap :$ ty_k) :$ ty_a ~> (tyMap :$ ty_k) :$ ty_a) $ TermLC $ \c -> lam $ map_insert (k_ c) (a c) map_delete_from = -- delete :: Ord k => k -> Map k a -> Map k a from_ast2 ast $ \ast_k ast_m as -> term_from ast_k ctx $ \ty_k (TermLC k_) -> term_from ast_m ctx $ \ty_m (TermLC m) -> check_type2 tyMap ast_m ty_m $ \Refl ty_m_k ty_m_a -> check_type (At (Just ast_k) ty_k) (At (Just ast_m) ty_m_k) $ \Refl -> check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con -> k as ((tyMap :$ ty_k) :$ ty_m_a) $ TermLC $ \c -> map_delete (k_ c) (m c) map_difference_from = -- difference :: Ord k => Map k a -> Map k b -> Map k a from_ast2 ast $ \ast_ma ast_mb as -> term_from ast_ma ctx $ \ty_ma (TermLC ma) -> term_from ast_mb ctx $ \ty_mb (TermLC mb) -> check_type2 tyMap ast_ma ty_ma $ \Refl ty_ma_k ty_ma_a -> check_type2 tyMap ast_mb ty_mb $ \Refl ty_mb_k _ty_mb_b -> check_type (At (Just ast_ma) ty_ma_k) (At (Just ast_mb) ty_mb_k) $ \Refl -> check_constraint (At (Just ast_ma) (tyOrd :$ ty_ma_k)) $ \Con -> k as ((tyMap :$ ty_ma_k) :$ ty_ma_a) $ TermLC $ \c -> map_difference (ma c) (mb c) map_foldrWithKey_from = -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b from_ast1 ast $ \ast_f as -> term_from ast_f ctx $ \ty_f (TermLC f) -> check_type2 tyFun ast_f ty_f $ \Refl ty_k ty_fabb -> check_type2 tyFun ast_f ty_fabb $ \Refl ty_a ty_fbb -> check_type2 tyFun ast_f ty_fbb $ \Refl ty_b ty_b' -> check_type (At (Just ast_f) ty_b) (At (Just ast_f) ty_b') $ \Refl -> k as (ty_b ~> (tyMap :$ ty_k) :$ ty_a ~> ty_b) $ TermLC $ \c -> lam $ \b -> lam $ \m -> map_foldrWithKey (f c) b m -- | The 'Map' 'Type' tyMap :: Inj_Const cs Map => Type cs Map tyMap = TyConst inj_const sym_Map :: Proxy Sym_Map sym_Map = Proxy syMap :: IsString a => [Syntax a] -> Syntax a syMap = Syntax "Map"