{-# 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)
	 = Just $ 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)
	 = Just $ 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"