{-# 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 Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (either)
import qualified Data.Map.Strict as Map

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.Lib.MonoFunctor (TyFam_MonoElement(..))

-- * 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 TyConsts_of_Iface (Proxy Map) = Proxy Map ': TyConsts_imported_by (Proxy Map)
type instance TyConsts_imported_by (Proxy Map) =
 [ Proxy (->)
 , Proxy []
 , Proxy (,)
 , Proxy Bool
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Maybe
 , Proxy Monad
 , Proxy MonoFunctor
 , 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 @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
 ( 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_TyFamC TyFam_MonoElement
 ( Proj_TyConst cs Map
 ) => Proj_TyFamC cs TyFam_MonoElement Map where
	proj_TyFamC _c _fam ((TyConst c :$ _ty_k :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @Map)
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing

instance -- Proj_TyConC
 ( Proj_TyConst cs Map
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy 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)
	 = 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
		 _ -> 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)
	 = 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_TyConst q (Proxy @MonoFunctor) -> Just TyCon
		 _ -> 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 cs Map
 , Inj_TyConst cs (->)
 , Inj_TyConst cs Bool
 , Inj_TyConst cs Ord
 , Inj_TyConst cs Maybe
 , Inj_TyConst cs []
 , Inj_TyConst cs (,)
 , Proj_TyCon  cs
 , Compile cs is
 ) => CompileI cs 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 ->
			-- 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