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

import Control.Monad
import qualified Data.Function as Fun
import qualified Data.List as List
import Data.Monoid
import Data.Proxy (Proxy(..))
import qualified Data.Text as Text
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.Trans.Common

-- * 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
instance Sym_List Repr_Host where
	list_empty   = return []
	list_cons    = liftM2 (:)
	list         = sequence
	list_filter  = liftM2 List.filter
	list_zipWith = liftM3 List.zipWith
	list_reverse = liftM  List.reverse
instance Sym_List Repr_Text where
	list_empty = Repr_Text $ \_p _v ->
		"[]"
	list_cons (Repr_Text x) (Repr_Text xs) =
		Repr_Text $ \p v ->
			let p' = precedence_List_Cons in
			paren p p' $ x p' v <> ":" <> xs p' v
	list l = Repr_Text $ \_p v ->
		let p' = precedence_Toplevel in
		"[" <> Text.intercalate ", " ((\(Repr_Text a) -> a p' v) Prelude.<$> l) <> "]"
	list_filter  = repr_text_app2 "list_filter"
	list_zipWith = repr_text_app3 "list_zipWith"
	list_reverse = repr_text_app1 "list_reverse"
instance
 ( 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
	list l =
		let (l1, l2) =
			foldr (\(x1 `Dup` x2) (xs1, xs2) ->
				(x1:xs1, x2:xs2)) ([], []) l in
		list l1 `Dup` list l2
	list_filter (f1 `Dup` f2) (l1 `Dup` l2) =
		list_filter f1 l1 `Dup` list_filter f2 l2
	list_zipWith (f1 `Dup` f2) (la1 `Dup` la2) (lb1 `Dup` lb2) =
		list_zipWith f1 la1 lb1 `Dup` list_zipWith f2 la2 lb2
	list_reverse (l1 `Dup` l2) =
		list_reverse l1 `Dup` list_reverse l2

-- * 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)