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

-- import qualified Data.List as List
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (maybe)

import Language.Symantic.Type
import Language.Symantic.Repr.Dup
import Language.Symantic.Trans.Common
import Language.Symantic.Expr.Common
import Language.Symantic.Expr.Lambda
import Language.Symantic.Expr.Bool

-- * Class 'Sym_List_Lam'
-- | Symantic.
class Sym_List repr where
	list_empty :: repr [a]
	list_cons  :: repr a -> repr [a] -> repr [a]
	
	default list_empty :: Trans t repr => t repr [a]
	default list_cons  :: Trans t repr => t repr a -> t repr [a] -> t repr [a]
	list_empty = trans_lift list_empty
	list_cons  = trans_map2 list_cons
-- | Symantic requiring a 'Lambda'.
class Sym_List_Lam lam repr where
	list_filter
	 :: repr (Lambda lam a Bool)
	 -> repr [a]
	 -> repr [a]
	
	default list_filter
	 :: Trans t repr
	 => t repr (Lambda lam a Bool)
	 -> t repr [a]
	 -> t repr [a]
	list_filter = trans_map2 list_filter

instance -- Sym_List Dup
 ( Sym_List r1
 , Sym_List r2
 ) => Sym_List (Dup r1 r2) where
	list_empty = list_empty `Dup` list_empty
	list_cons (a1 `Dup` a2) (l1 `Dup` l2) = list_cons a1 l1 `Dup` list_cons a2 l2
instance -- Sym_List_Lam Dup
 ( Sym_List_Lam lam r1
 , Sym_List_Lam lam r2
 ) => Sym_List_Lam lam (Dup r1 r2) where
	list_filter (f1 `Dup` f2) (l1 `Dup` l2) =
		list_filter f1 l1 `Dup` list_filter f2 l2

-- * Type 'Expr_List'
-- | Expression.
data Expr_List (lam:: * -> *) (root:: *)
type instance Root_of_Expr      (Expr_List lam root)      = root
type instance Type_of_Expr      (Expr_List lam root)      = Type_List
type instance Sym_of_Expr       (Expr_List lam root) repr = (Sym_List repr, Sym_List_Lam lam repr)
type instance Error_of_Expr ast (Expr_List lam root)      = No_Error_Expr

-- | Parsing utility to check that the given type is a 'Type_List'
-- or raise 'Error_Expr_Type_mismatch'.
check_type_list
 :: forall ast ex root ty h ret.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , Type_Lift   Type_List (Type_of_Expr root)
 , Type_Unlift Type_List (Type_of_Expr root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 )
 => Proxy ex -> ast -> ty h
 -> (Type_List ty h -> Either (Error_of_Expr ast root) ret)
 -> Either (Error_of_Expr ast root) ret
check_type_list ex ast ty k =
	case type_unlift $ unType_Root ty of
	 Just ty_l -> k ty_l
	 Nothing -> Left $
		error_expr ex $
		Error_Expr_Type_mismatch ast
		 (Exists_Type (type_list $ type_var SZero
		 :: Type_Root_of_Expr ex [Zero]))
		 (Exists_Type ty)

-- | Parse 'list_empty'.
list_empty_from
 :: forall root lam ty ty_root ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 , ty_root ~ Type_Root_of_Expr root
 , Type_from ast ty_root
 , Type_Root_Lift Type_List ty_root
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 , Root_of_Expr root ~ root
 ) => ast
 -> Expr_From ast (Expr_List lam root) hs ret
list_empty_from ast_ty_a ex ast _ctx k =
	case type_from (Proxy::Proxy ty_root)
	 ast_ty_a (Right . Exists_Type) of
	 Left err -> Left $ error_expr ex $ Error_Expr_Type err ast
	 Right (Exists_Type ty_a) ->
		k (type_list ty_a) $ Forall_Repr_with_Context $
			const list_empty

-- | Parse 'list_cons'.
list_cons_from
 :: forall root lam ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 , Type_Eq (Type_Root_of_Expr root)
 , Expr_from ast root
 , Type_Lift   Type_List (Type_of_Expr root)
 , Type_Unlift Type_List (Type_of_Expr root)
 , Error_Expr_Lift (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_List lam root) hs ret
list_cons_from ast_a ast_l ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_a ctx $
	 \(ty_a::Type_Root_of_Expr root h_a) (Forall_Repr_with_Context a) ->
	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_List ty_l_a) ->
	check_type_eq ex ast ty_a ty_l_a $ \Refl ->
	k (type_list ty_a) $ Forall_Repr_with_Context $
		\c -> list_cons (a c) (l c)

-- | Parse 'list_filter'.
list_filter_from
 :: forall root lam ty ty_root ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List lam root)
 , ty_root ~ Type_of_Expr root
 , Type_Eq (Type_Root_of_Expr root)
 , Expr_from ast root
 , Type_Lift   Type_Bool      ty_root
 , Type_Lift   (Type_Fun lam) ty_root
 , Type_Unlift (Type_Fun lam) ty_root
 , Type_Lift   Type_List      ty_root
 , Type_Unlift Type_List      ty_root
 , Error_Expr_Lift (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_List lam root) hs ret
list_filter_from ast_f ast_l 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_l ctx $
	 \(ty_l::Type_Root_of_Expr root h_l) (Forall_Repr_with_Context l) ->
	check_type_fun ex ast ty_f $ \(ty_f_a `Type_Fun` ty_f_b
	 :: Type_Fun lam (Type_Root_of_Expr root) h_f) ->
	check_type_eq ex ast type_bool ty_f_b $ \Refl ->
	check_type_list ex ast ty_l $ \(Type_List ty_l_a) ->
	check_type_eq ex ast ty_f_a ty_l_a $ \Refl ->
	k ty_l $ Forall_Repr_with_Context $
	 \c -> list_filter (f c) (l c)

-- ** Type 'Expr_Lambda_List_Bool'
-- | Convenient alias.
type Expr_Lambda_List_Bool lam
 =   Expr_Root (Expr_Alt (Expr_Lambda lam)
                         (Expr_Alt (Expr_List lam)
                                    Expr_Bool))

-- | Convenient alias around 'expr_from'.
expr_lambda_list_bool_from
 :: forall lam ast root.
 ( Expr_from ast (Expr_Lambda_List_Bool lam)
 , root ~ Expr_Lambda_List_Bool lam
 ) => Proxy lam
 -> ast
 -> Either (Error_of_Expr ast root)
           (Exists_Type_and_Repr (Type_Root_of_Expr root)
                                 (Forall_Repr root))
expr_lambda_list_bool_from _lam ast =
	expr_from (Proxy::Proxy root) ast
	 Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
		Right $ Exists_Type_and_Repr ty $
			Forall_Repr $ repr Context_Empty