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

import qualified Data.Function as Fun
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(Refl))

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

-- * Class 'Sym_List_Lam'
-- | Symantic.
class Sym_List repr where
	list_empty :: repr [a]
	list_cons :: repr a -> repr [a] -> repr [a]
	list :: [repr a] -> repr [a]
	list_filter :: repr (a -> Bool) -> repr [a] -> repr [a]
	list_zipWith :: repr (a -> b -> c) -> repr [a] -> repr [b] -> repr [c]
	list_reverse :: 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]
	default list         :: Trans t repr => [t repr a] -> t repr [a]
	default list_filter  :: Trans t repr => t repr (a -> Bool) -> t repr [a] -> t repr [a]
	default list_zipWith :: Trans t repr => t repr (a -> b -> c) -> t repr [a] -> t repr [b] -> t repr [c]
	default list_reverse :: Trans t repr => t repr [a] -> t repr [a]
	
	list_empty   = trans_lift list_empty
	list_cons    = trans_map2 list_cons
	list l       = trans_lift $ list (trans_apply Prelude.<$> l)
	list_filter  = trans_map2 list_filter
	list_zipWith = trans_map3 list_zipWith
	list_reverse = trans_map1 list_reverse

-- * Type 'Expr_List'
-- | Expression.
data Expr_List (root:: *)
type instance Root_of_Expr      (Expr_List root)      = root
type instance Type_of_Expr      (Expr_List root)      = Type_List
type instance Sym_of_Expr       (Expr_List root) repr = (Sym_List repr)
type instance Error_of_Expr ast (Expr_List 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
 , Lift_Type   Type_List (Type_of_Expr root)
 , Unlift_Type Type_List (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_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 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_list $ type_var0 SZero
		 :: ty [Var0]))
		 (Exists_Type ty)

-- | Parse 'list_empty'.
list_empty_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List root)
 , Type_from ast ty
 , 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_List root) hs ret
list_empty_from ast_ty_a ex ast _ctx k =
	either (\err -> Left $ error_expr ex $ Error_Expr_Type err ast) Fun.id $
	type_from (Proxy::Proxy ty) ast_ty_a $ \ty_a -> Right $
	k (type_list ty_a) $ Forall_Repr_with_Context $
		Fun.const list_empty

-- | Parse 'list_cons'.
list_cons_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_List (Type_of_Expr root)
 , Unlift_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 -> ast
 -> Expr_From ast (Expr_List root) hs ret
list_cons_from ast_a ast_l ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_a ctx $
	 \(ty_a::ty h_a) (Forall_Repr_with_Context a) ->
	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_a) ->
	check_eq_type 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'.
list_from
 :: forall root ex ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List root)
 , ex ~ Expr_List root
 , Eq_Type ty
 , Type_from ast ty
 , Expr_from ast root
 , Lift_Type   Type_List (Type_of_Expr root)
 , Unlift_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 -> [ast]
 -> Expr_From ast ex hs ret
list_from ast_ty_a ast_as =
	case type_from (Proxy::Proxy ty)
	 ast_ty_a (Right . Exists_Type) of
	 Left err -> \ex ast _ctx _k -> Left $ error_expr ex $ Error_Expr_Type err ast
	 Right (Exists_Type ty_a) -> go ty_a [] ast_as
	where
	go :: ty ty_a
	   -> [Forall_Repr_with_Context root hs ty_a]
	   -> [ast]
	   -> Expr_From ast (Expr_List root) hs ret
	go ty_a as [] _ex _ast _ctx k =
		k (type_list ty_a) $ Forall_Repr_with_Context $
		 \c -> list ((\(Forall_Repr_with_Context a) -> a c) Prelude.<$> reverse as)
	go ty_a as (ast_x:ast_xs) ex ast ctx k =
		expr_from (Proxy::Proxy root) ast_x ctx $
		 \(ty_x::ty h_x) x ->
		check_eq_type ex ast ty_a ty_x $ \Refl ->
		go ty_a (x:as) ast_xs ex ast ctx k

-- | Parse 'list_filter'.
list_filter_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_Bool (Type_of_Expr root)
 , Lift_Type   Type_Fun  (Type_of_Expr root)
 , Unlift_Type Type_Fun  (Type_of_Expr root)
 , Lift_Type   Type_List (Type_of_Expr root)
 , Unlift_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 -> ast
 -> Expr_From ast (Expr_List root) hs ret
list_filter_from ast_f ast_l ex ast ctx k =
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_l ctx $
	 \(ty_l::ty h_l) (Forall_Repr_with_Context l) ->
	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b
	 :: Type_Fun ty h_f) ->
	check_eq_type ex ast type_bool ty_f_b $ \Refl ->
	check_type_list ex ast ty_l $ \(Type_Type1 _ ty_l_a) ->
	check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
	k ty_l $ Forall_Repr_with_Context $
	 \c -> list_filter (f c) (l c)

-- | Parse 'list_zipWith'.
list_zipWith_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List 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_List (Type_of_Expr root)
 , Unlift_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 -> ast -> ast
 -> Expr_From ast (Expr_List root) hs ret
list_zipWith_from ast_f ast_la ast_lb ex ast ctx k =
 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
	expr_from (Proxy::Proxy root) ast_f ctx $
	 \(ty_f::ty h_f) (Forall_Repr_with_Context f) ->
	expr_from (Proxy::Proxy root) ast_la ctx $
	 \(ty_la::ty h_la) (Forall_Repr_with_Context la) ->
	expr_from (Proxy::Proxy root) ast_lb ctx $
	 \(ty_lb::ty h_lb) (Forall_Repr_with_Context lb) ->
	check_type_fun ex ast ty_f $ \(Type_Type2 Proxy ty_f_a ty_f_b2c
	 :: Type_Fun ty h_f) ->
	check_type_fun ex ast ty_f_b2c $ \(Type_Type2 Proxy ty_f_b ty_f_c
	 :: Type_Fun ty h_f_b2c) ->
	check_type_list ex ast ty_la $ \(Type_Type1 _ ty_l_a) ->
	check_type_list ex ast ty_lb $ \(Type_Type1 _ ty_l_b) ->
	check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
	check_eq_type ex ast ty_f_b ty_l_b $ \Refl ->
	check_eq_type ex ast ty_f_a ty_l_a $ \Refl ->
	k (type_list ty_f_c) $ Forall_Repr_with_Context $
	 \c -> list_zipWith (f c) (la c) (lb c)

-- | Parse 'list_reverse'.
list_reverse_from
 :: forall root ty ast hs ret.
 ( ty ~ Type_Root_of_Expr (Expr_List root)
 , Eq_Type ty
 , Expr_from ast root
 , Lift_Type   Type_List (Type_of_Expr root)
 , Unlift_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_List root) hs ret
list_reverse_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_a) ->
	k ty_l $ Forall_Repr_with_Context $
	 \c -> list_reverse (l c)