{-# 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 qualified Data.List as List
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)
	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 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
	mapWithKey       = trans_map2 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
	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"
	mapWithKey       = textI_app2 "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
	mapWithKey       = dupI2 sym_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
		 "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 ->
			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 ((tyMap :$ ty_k) :$ ty_a) $ TermLC $
			 \c -> map_fromList (l c)
		mapWithKey_from =
		 -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_k2a2b] ->
				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 ((tyMap :$ ty_k) :$ ty_a ~> (tyMap :$ ty_k) :$ ty_b) $ TermLC $
				 \c -> lam $ mapWithKey (k2a2b c)
			 [ast_k2a2b, ast_m] ->
				term_from ast_k2a2b ctx $ \ty_k2a2b (TermLC k2a2b) ->
				term_from ast_m     ctx $ \ty_m     (TermLC m) ->
				check_type2 tyFun ast_k2a2b ty_k2a2b $ \Refl ty_k ty_a2b ->
				check_type2 tyFun ast_k2a2b ty_a2b $ \Refl ty_a ty_b ->
				check_type2 tyMap ast_m ty_m $ \Refl ty_m_k ty_m_a ->
				check_type (At (Just ast_k2a2b) ty_k) (At (Just ast_m) ty_m_k) $ \Refl ->
				check_type (At (Just ast_k2a2b) ty_a) (At (Just ast_m) ty_m_a) $ \Refl ->
				k ((tyMap :$ ty_k) :$ ty_b) $ TermLC $
				 \c -> mapWithKey (k2a2b c) (m c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2
		map_lookup_from =
		 -- lookup :: Ord k => k -> Map k a -> Maybe a
			from_ast2 ast $ \ast_k ast_m ->
			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 (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 ->
			term_from ast_m ctx $ \ty_m (TermLC m) ->
			check_type2 tyMap ast_m ty_m $ \Refl ty_m_k _ty_m_a ->
			k (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 ->
			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 tyBool $ TermLC $
			 \c -> map_member (k_ c) (m c)
		map_insert_from =
		 -- insert :: Ord k => k -> a -> Map k a -> Map k a
			case ast_nodes ast of
			 l | List.length l < 2 -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 2
			 [ast_k, ast_a] ->
				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 ((tyMap :$ ty_k) :$ ty_a ~> (tyMap :$ ty_k) :$ ty_a) $ TermLC $
				 \c -> lam $ map_insert (k_ c) (a c)
			 [ast_k, ast_a, ast_m] ->
				term_from ast_k ctx $ \ty_k (TermLC k_) ->
				term_from ast_a ctx $ \ty_a (TermLC a) ->
				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_type (At (Just ast_a) ty_a) (At (Just ast_m) ty_m_a) $ \Refl ->
				check_constraint (At (Just ast_k) (tyOrd :$ ty_k)) $ \Con ->
				k ((tyMap :$ ty_k) :$ ty_a) $ TermLC $
				 \c -> map_insert (k_ c) (a c) (m c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 3
		map_delete_from =
		 -- delete :: Ord k => k -> Map k a -> Map k a
			from_ast2 ast $ \ast_k ast_m ->
			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 ((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 ->
			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 ((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
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_f] ->
				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 (ty_b ~> (tyMap :$ ty_k) :$ ty_a ~> ty_b) $ TermLC $
				 \c -> lam $ \b -> lam $ \m -> map_foldrWithKey (f c) b m
			 [ast_f, ast_b] ->
				term_from ast_f ctx $ \ty_f (TermLC f) ->
				term_from ast_b ctx $ \ty_b (TermLC b) ->
				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 ->
				check_type (At (Just ast_f) ty_b') (At (Just ast_f) ty_b'') $ \Refl ->
				k ((tyMap :$ ty_k) :$ ty_a ~> ty_b) $ TermLC $
				 \c -> lam $ map_foldrWithKey (f c) (b c)
			 [ast_f, ast_b, ast_m] ->
				term_from ast_f ctx $ \ty_f (TermLC f) ->
				term_from ast_b ctx $ \ty_b (TermLC b) ->
				term_from ast_m ctx $ \ty_m (TermLC m) ->
				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 ->
				check_type (At (Just ast_f) ty_b') (At (Just ast_f) ty_b'') $ \Refl ->
				check_type2 tyMap ast_m ty_m $ \Refl ty_m_k ty_m_a ->
				check_type (At (Just ast_f) ty_k) (At (Just ast_m) ty_m_k) $ \Refl ->
				check_type (At (Just ast_f) ty_a) (At (Just ast_m) ty_m_a) $ \Refl ->
				k ty_b $ TermLC $
				 \c -> map_foldrWithKey (f c) (b c) (m c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 3

-- | 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"