{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Expression for 'Map'.
module Language.Symantic.Expr.Map where

import Control.Monad
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))

import Language.Symantic.Type
import Language.Symantic.Repr
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Error
import Language.Symantic.Expr.From
import Language.Symantic.Expr.Lambda
import Language.Symantic.Expr.List
import Language.Symantic.Expr.Tuple
import Language.Symantic.Trans.Common

-- * Class 'Sym_Map_Lam'
-- | Symantic.
class Sym_Map repr where
	map_from_list :: Ord k => repr [(k, a)] -> repr (Map k a)
	mapWithKey :: repr (k -> a -> b) -> repr (Map k a) -> repr (Map k b)
	map_lookup :: Ord k => repr k -> repr (Map k a) -> repr (Maybe a)
	map_keys :: repr (Map k a) -> repr [k]
	map_member :: Ord k => repr k -> repr (Map k a) -> repr Bool
	map_insert :: Ord k => repr k -> repr a -> repr (Map k a) -> repr (Map k a)
	map_delete :: Ord k => repr k -> repr (Map k a) -> repr (Map k a)
	map_difference :: Ord k => repr (Map k a) -> repr (Map k b) -> repr (Map k a)
	map_foldrWithKey :: repr (k -> a -> b -> b) -> repr b -> repr (Map k a) -> repr b
	
	default map_from_list :: (Trans t repr, Ord k) => t repr [(k, a)] -> t repr (Map k a)
	default mapWithKey :: Trans t repr => t repr (k -> a -> b) -> t repr (Map k a) -> t repr (Map k b)
	default map_lookup :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Maybe a)
	default map_keys :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr [k]
	default map_member :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr Bool
	default map_insert :: (Trans t repr, Ord k) => t repr k -> t repr a -> t repr (Map k a) -> t repr (Map k a)
	default map_delete :: (Trans t repr, Ord k) => t repr k -> t repr (Map k a) -> t repr (Map k a)
	default map_difference :: (Trans t repr, Ord k) => t repr (Map k a) -> t repr (Map k b) -> t repr (Map k a)
	default map_foldrWithKey :: Trans t repr => t repr (k -> a -> b -> b) -> t repr b -> t repr (Map k a) -> t repr b
	
	map_from_list    = trans_map1 map_from_list
	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
instance Sym_Map Repr_Host where
	map_from_list    = 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 Repr_Text where
	map_from_list    = repr_text_app1 "map_from_list"
	mapWithKey       = repr_text_app2 "mapWithKey"
	map_lookup       = repr_text_app2 "map_lookup"
	map_keys         = repr_text_app1 "map_keys"
	map_member       = repr_text_app2 "map_member"
	map_insert       = repr_text_app3 "map_insert"
	map_delete       = repr_text_app2 "map_delete"
	map_difference   = repr_text_app2 "map_difference"
	map_foldrWithKey = repr_text_app3 "map_foldrWithKey"
instance
 ( Sym_Map r1
 , Sym_Map r2
 ) => Sym_Map (Dup r1 r2) where
	map_from_list (l1 `Dup` l2) =
		map_from_list l1 `Dup` map_from_list l2
	mapWithKey (f1 `Dup` f2) (m1 `Dup` m2) =
		mapWithKey f1 m1 `Dup` mapWithKey f2 m2
	map_lookup (k1 `Dup` k2) (m1 `Dup` m2) =
		map_lookup k1 m1 `Dup` map_lookup k2 m2
	map_keys (m1 `Dup` m2) =
		map_keys m1 `Dup` map_keys m2
	map_member (k1 `Dup` k2) (m1 `Dup` m2) =
		map_member k1 m1 `Dup` map_member k2 m2
	map_insert (k1 `Dup` k2) (a1 `Dup` a2) (m1 `Dup` m2) =
		map_insert k1 a1 m1 `Dup` map_insert k2 a2 m2
	map_delete (k1 `Dup` k2) (m1 `Dup` m2) =
		map_delete k1 m1 `Dup` map_delete k2 m2
	map_difference (ma1 `Dup` ma2) (mb1 `Dup` mb2) =
		map_difference ma1 mb1 `Dup` map_difference ma2 mb2
	map_foldrWithKey (f1 `Dup` f2) (b1 `Dup` b2) (m1 `Dup` m2) =
		map_foldrWithKey f1 b1 m1 `Dup` map_foldrWithKey f2 b2 m2

-- | Parsing utility to check that the given type is a 'Type_List'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_map
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Lift_Type   Type_Map (Type_of_Expr root)
 , Unlift_Type Type_Map (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty h
 -> (Type_Map ty h -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type_map ex ast ty k =
	case unlift_type $ unType_Root ty of
	 Just ty_l -> k ty_l
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type (type_map (type_var0 SZero) (type_var0 $ SSucc SZero)
		 :: ty (Map Var0 Var0)))
		 (Exists_Type ty)

-- | Parse 'map_from_list'.
map_from_list_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Expr_from ast root
 , Lift_Type   Type_List   (Type_of_Expr root)
 , Unlift_Type Type_List   (Type_of_Expr root)
 , Lift_Type   Type_Map    (Type_of_Expr root)
 , Lift_Type   Type_Tuple2 (Type_of_Expr root)
 , Unlift_Type Type_Tuple2 (Type_of_Expr root)
 , Constraint_Type Ord ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> Expr_From ast (Expr_Map root) hs ret
map_from_list_from ast_l ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_l ctx $
	 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
	check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_t) ->
	check_type_tuple2 ex ast ty_l_t $ \(Type_Type2 Proxy ty_k ty_a) ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
	k (type_map ty_k ty_a) $ Forall_Repr_with_Context $
	 \c -> map_from_list (l c)

-- | Parse 'mapWithKey'.
mapWithKey_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Fun (Type_of_Expr root)
 , Unlift_Type Type_Fun (Type_of_Expr root)
 , Lift_Type   Type_Map (Type_of_Expr root)
 , Unlift_Type Type_Map (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> Expr_From ast (Expr_Map root) hs ret
mapWithKey_from ast_f ast_m ex ast ctx k =
 -- mapWithKey :: (k -> a -> b) -> Map k a -> Map k b
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_k ty_f_a2b
	 :: Type_Fun ty h_f) ->
	check_type_fun ex ast ty_f_a2b $ \(Type_Type2 Proxy ty_f_a ty_f_b
	 :: Type_Fun ty h_f_a2b) ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
	check_eq_type ex ast ty_f_k ty_m_k $ \Refl ->
	check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
	k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
	 \c -> mapWithKey (f c) (m c)

-- | Parse 'map_lookup'.
map_lookup_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Map   (Type_of_Expr root)
 , Unlift_Type Type_Map   (Type_of_Expr root)
 , Lift_Type   Type_Maybe (Type_of_Expr root)
 , Constraint_Type Ord ty
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> Expr_From ast (Expr_Map root) hs ret
map_lookup_from ast_k ast_m ex ast ctx k =
 -- lookup :: Ord k => k -> Map k a -> Maybe a
	expr_from (Proxy::Proxy root) ast_k ctx $
	 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
	check_eq_type ex ast ty_k ty_m_k $ \Refl ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
	k (type_maybe ty_m_a) $ Forall_Repr_with_Context $
	 \c -> map_lookup (key c) (m c)

-- | Parse 'map_keys'.
map_keys_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Map  (Type_of_Expr root)
 , Unlift_Type Type_Map  (Type_of_Expr root)
 , Lift_Type   Type_List (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> Expr_From ast (Expr_Map root) hs ret
map_keys_from ast_m ex ast ctx k =
 -- keys :: Map k a -> [k]
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
	k (type_list ty_m_k) $ Forall_Repr_with_Context $
	 \c -> map_keys (m c)

-- | Parse 'map_member'.
map_member_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Constraint_Type Ord ty
 , Lift_Type   Type_Map  (Type_of_Expr root)
 , Unlift_Type Type_Map  (Type_of_Expr root)
 , Lift_Type   Type_Bool (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> Expr_From ast (Expr_Map root) hs ret
map_member_from ast_k ast_m ex ast ctx k =
 -- member :: Ord k => k -> Map k a -> Bool
	expr_from (Proxy::Proxy root) ast_k ctx $
	 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
	check_eq_type ex ast ty_k ty_m_k $ \Refl ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
	k type_bool $ Forall_Repr_with_Context $
	 \c -> map_member (key c) (m c)

-- | Parse 'map_insert'.
map_insert_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Constraint_Type Ord ty
 , Lift_Type   Type_Map (Type_of_Expr root)
 , Unlift_Type Type_Map (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast -> ast -> ast
 -> Expr_From ast (Expr_Map root) hs ret
map_insert_from ast_k ast_a ast_m ex ast ctx k =
 -- insert :: Ord k => k -> a -> Map k a -> Map k a
	expr_from (Proxy::Proxy root) ast_k ctx $
	 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
	expr_from (Proxy::Proxy root) ast_a ctx $
	 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
	check_eq_type ex ast ty_k ty_m_k $ \Refl ->
	check_eq_type ex ast ty_a ty_m_a $ \Refl ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
	k ty_m $ Forall_Repr_with_Context $
	 \c -> map_insert (key c) (a c) (m c)

-- | Parse 'map_delete'.
map_delete_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Map (Type_of_Expr root)
 , Unlift_Type Type_Map (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Constraint_Type Ord ty
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> Expr_From ast (Expr_Map root) hs ret
map_delete_from ast_k ast_m ex ast ctx k =
 -- delete :: Ord k => k -> Map k a -> Map k a
	expr_from (Proxy::Proxy root) ast_k ctx $
	 \(ty_k::ty h_k) (Forall_Repr_with_Context key) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k _ty_m_a) ->
	check_eq_type ex ast ty_k ty_m_k $ \Refl ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_k $ \Dict ->
	k ty_m $ Forall_Repr_with_Context $
	 \c -> map_delete (key c) (m c)

-- | Parse 'map_difference'.
map_difference_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Map (Type_of_Expr root)
 , Unlift_Type Type_Map (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Constraint_Type Ord ty
 , Root_of_Expr root ~ root
 ) => ast -> ast
 -> Expr_From ast (Expr_Map root) hs ret
map_difference_from ast_ma ast_mb ex ast ctx k =
 -- difference :: Ord k => Map k a -> Map k b -> Map k a
	expr_from (Proxy::Proxy root) ast_ma ctx $
	 \(ty_ma::ty h_ma) (Forall_Repr_with_Context ma) ->
	expr_from (Proxy::Proxy root) ast_mb ctx $
	 \(ty_mb::ty h_mb) (Forall_Repr_with_Context mb) ->
	check_type_map ex ast ty_ma $ \(Type_Type2 Proxy ty_ma_k _ty_ma_a) ->
	check_type_map ex ast ty_mb $ \(Type_Type2 Proxy ty_mb_k _ty_mb_b) ->
	check_eq_type ex ast ty_ma_k ty_mb_k $ \Refl ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_ma_k $ \Dict ->
	k ty_ma $ Forall_Repr_with_Context $
	 \c -> map_difference (ma c) (mb c)

-- | Parse 'map_foldrWithKey'.
map_foldrWithKey_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Fun (Type_of_Expr root)
 , Unlift_Type Type_Fun (Type_of_Expr root)
 , Lift_Type   Type_Map (Type_of_Expr root)
 , Unlift_Type Type_Map (Type_of_Expr root)
 , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Constraint_Type Ord ty
 , Root_of_Expr root ~ root
 ) => ast -> ast -> ast
 -> Expr_From ast (Expr_Map root) hs ret
map_foldrWithKey_from ast_f ast_b ast_m ex ast ctx k =
 -- foldrWithKey :: (k -> a -> b -> b) -> b -> Map k a -> b
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_b ctx $
	 \(ty_b::ty h_b) (Forall_Repr_with_Context b) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::ty h_m) (Forall_Repr_with_Context m) ->
	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_k ty_f_a2b2b) ->
	check_type_fun ex ast ty_f_a2b2b $ \(Type_Type2 Proxy ty_f_a ty_f_b2b) ->
	check_type_fun ex ast ty_f_b2b $ \(Type_Type2 Proxy ty_f_b ty_f_b') ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
	check_eq_type ex ast ty_f_k ty_m_k $ \Refl ->
	check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
	check_eq_type ex ast ty_b ty_f_b $ \Refl ->
	check_eq_type ex ast ty_f_b ty_f_b' $ \Refl ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
	k ty_b $ Forall_Repr_with_Context $
	 \c -> map_foldrWithKey (f c) (b c) (m c)

-- * Type 'Expr_Map'
-- | Expression.
data Expr_Map (root:: *)
type instance Root_of_Expr      (Expr_Map root)      = root
type instance Type_of_Expr      (Expr_Map root)      = Type_Map
type instance Sym_of_Expr       (Expr_Map root) repr = (Sym_Map repr)
type instance Error_of_Expr ast (Expr_Map root)      = No_Error_Expr