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

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

import Language.Symantic.Type
import Language.Symantic.Trans.Common
import Language.Symantic.Expr.Common
import Language.Symantic.Expr.Lambda
-- import Language.Symantic.Expr.Bool
import Language.Symantic.Expr.List
import Language.Symantic.Expr.Tuple

-- * Class 'Sym_Map_Lam'
-- | Symantic.
class Sym_Map repr where
	map_from_list :: Ord k => repr [(k, a)] -> repr (Map k a)
	
	default map_from_list :: (Trans t repr, Ord k) => t repr [(k, a)] -> t repr (Map k a)
	map_from_list = trans_map1 map_from_list
-- | Symantic.
class Sym_Map_Lam lam repr where
	map_map
	 :: repr (Lambda lam a b)
	 -> repr (Map k a)
	 -> repr (Map k b)
	
	default map_map
	 :: Trans t repr
	 => t repr (Lambda lam a b)
	 -> t repr (Map k a)
	 -> t repr (Map k b)
	map_map = trans_map2 map_map

-- | 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)
		 :: Type_Root_of_Expr ex (Map Var0 Var0)))
		 (Exists_Type ty)

-- | Parse 'map_from_list'.
map_from_list_from
 :: forall root lam ty ty_root ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map lam root)
 , ty_root ~ Type_of_Expr root
 , Expr_from ast root
 , Lift_Type   Type_List      ty_root
 , Unlift_Type Type_List      ty_root
 , Lift_Type   Type_Map       ty_root
 , Lift_Type   Type_Tuple2    ty_root
 , Unlift_Type Type_Tuple2    ty_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 lam root) hs ret
map_from_list_from ast_l ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_l ctx $
	 \(ty_l::Type_Root_of_Expr root 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 'map_map'.
map_map_from
 :: forall root lam ty ty_root ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_Map lam root)
 , ty_root ~ Type_of_Expr root
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   (Type_Fun lam) ty_root
 , Unlift_Type (Type_Fun lam) ty_root
 , Lift_Type   Type_Map       ty_root
 , Unlift_Type Type_Map       ty_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 lam root) hs ret
map_map_from ast_f ast_m ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::Type_Root_of_Expr root h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_m ctx $
	 \(ty_m::Type_Root_of_Expr root h_m) (Forall_Repr_with_Context m) ->
	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
	 :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
	check_type_map ex ast ty_m $ \(Type_Type2 Proxy ty_m_k ty_m_a) ->
	check_eq_type ex ast ty_f_a ty_m_a $ \Refl ->
	check_constraint_type ex (Proxy::Proxy Ord) ast ty_m_k $ \Dict ->
	k (type_map ty_m_k ty_f_b) $ Forall_Repr_with_Context $
	 \c -> map_map (f c) (m c)

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