{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
-- | Symantic for '[]'.
module Language.Symantic.Compiling.List where

import Control.Monad (liftM, liftM2, liftM3)
import qualified Data.Foldable as Foldable
import qualified Data.Function as Fun
import qualified Data.Functor as Functor
import qualified Data.List as List
import Data.Monoid ((<>))
import Data.Proxy
import Data.String (IsString)
import Data.Text (Text)
import qualified Data.Text as Text
import qualified Data.Traversable as Traversable
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (filter, reverse, zipWith)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Bool (tyBool)
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

-- * Class 'Sym_List'
class Sym_List term where
	list_empty :: term [a]
	list_cons  :: term a -> term [a] -> term [a]
	list       :: [term a] -> term [a]
	filter     :: term (a -> Bool) -> term [a] -> term [a]
	zipWith    :: term (a -> b -> c) -> term [a] -> term [b] -> term [c]
	reverse    :: term [a] -> term [a]
	
	default list_empty :: Trans t term => t term [a]
	default list_cons  :: Trans t term => t term a -> t term [a] -> t term [a]
	default list       :: Trans t term => [t term a] -> t term [a]
	default filter     :: Trans t term => t term (a -> Bool) -> t term [a] -> t term [a]
	default zipWith    :: Trans t term => t term (a -> b -> c) -> t term [a] -> t term [b] -> t term [c]
	default reverse    :: Trans t term => t term [a] -> t term [a]
	
	list_empty = trans_lift list_empty
	list_cons  = trans_map2 list_cons
	list l     = trans_lift (list (trans_apply Functor.<$> l))
	filter     = trans_map2 filter
	zipWith    = trans_map3 zipWith
	reverse    = trans_map1 reverse

type instance Sym_of_Iface (Proxy []) = Sym_List
type instance Consts_of_Iface (Proxy []) = Proxy [] ': Consts_imported_by []
type instance Consts_imported_by [] =
 [ Proxy Applicative
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Ord
 , Proxy Traversable
 ]

instance Sym_List HostI where
	list_empty   = return []
	list_cons    = liftM2 (:)
	list         = Traversable.sequence
	filter  = liftM2 List.filter
	zipWith = liftM3 List.zipWith
	reverse = liftM  List.reverse
instance Sym_List TextI where
	list_empty = TextI $ \_p _v -> "[]"
	list_cons (TextI x) (TextI xs) =
		TextI $ \p v ->
			let p' = Precedence 5 in
			paren p p' $ x p' v <> ":" <> xs p' v
	list l = TextI $ \_p v ->
		let p' = precedence_Toplevel in
		"[" <> Text.intercalate ", " ((\(TextI a) -> a p' v) Functor.<$> l) <> "]"
	filter  = textI_app2 "filter"
	zipWith = textI_app3 "zipWith"
	reverse = textI_app1 "reverse"
instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
	list_empty = dupI0 sym_List list_empty
	list_cons  = dupI2 sym_List list_cons
	list l =
		let (l1, l2) =
			Foldable.foldr (\(x1 `DupI` x2) (xs1, xs2) ->
				(x1:xs1, x2:xs2)) ([], []) l in
		list l1 `DupI` list l2
	filter  = dupI2 sym_List filter
	zipWith = dupI3 sym_List zipWith
	reverse = dupI1 sym_List reverse

instance Const_from Text cs => Const_from Text (Proxy [] ': cs) where
	const_from "[]" k = k (ConstZ kind)
	const_from s k = const_from s $ k . ConstS
instance Show_Const cs => Show_Const (Proxy [] ': cs) where
	show_const ConstZ{} = "[]"
	show_const (ConstS c) = show_const c

instance -- Proj_ConC
 ( Proj_Const cs []
 , Proj_Consts cs (Consts_imported_by [])
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy []) where
	proj_conC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy [])
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Foldable)    -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monad)       -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Traversable) -> Just Con
		 _ -> Nothing
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy [])
	 = Just $ case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Monoid)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Const_from (Lexem ast) (Consts_of_Ifaces is)
 , Inj_Const (Consts_of_Ifaces is) []
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Term_from is ast
 ) => Term_fromI is (Proxy []) ast where
	term_fromI :: forall ctx ls rs ret. Term_fromT ast ctx ret is ls (Proxy [] ': rs)
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "[]"      -> list_empty_from
		 ":"       -> list_cons_from
		 "list"    -> list_from
		 "filter"  -> filter_from
		 "zipWith" -> zipWith_from
		 "reverse" -> reverse_from
		 _ -> Left $ Error_Term_unsupported
		where
		list_empty_from =
		 -- [] :: [a]
			from_ast1 ast $ \ast_ty_a ->
			either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
			type_from ast_ty_a $ \ty_a -> Right $
			check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
			k (tyList :$ ty_a) $ TermLC $
				Fun.const list_empty
		list_cons_from =
		 -- (:) :: a -> [a] -> [a]
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_a] ->
				term_from ast_a ctx $ \ty_a (TermLC a) ->
				k (tyList :$ ty_a ~> tyList :$ ty_a) $ TermLC $
				 \c -> lam $ list_cons (a c)
			 [ast_a, ast_la] ->
				term_from ast_a  ctx $ \ty_a  (TermLC a) ->
				term_from ast_la ctx $ \ty_la (TermLC la) ->
				check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
				check_type (At (Just ast_a) ty_a) (At (Just ast_la) ty_la_a) $ \Refl ->
				k ty_la $ TermLC $
				 \c -> list_cons (a c) (la c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2
		list_from =
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 ast_ty_a:ast_as ->
				either (Left . Error_Term_Typing . At (Just ast)) Fun.id $
				type_from ast_ty_a $ \ty_a -> Right $
				check_kind ast SKiType (At (Just ast_ty_a) ty_a) $ \Refl ->
				go ty_a [] ast_as
			where
			go :: Type (Consts_of_Ifaces is) ty_a
			   -> [TermLC ctx ty_a is '[] is]
			   -> [ast]
			   -> Either (Error_Term is ast) ret
			go ty_a as [] =
				k (tyList :$ ty_a) $ TermLC $
				 \c -> list $ (\(TermLC a) -> a c)
					 Functor.<$> List.reverse as
			go ty_a as (ast_x:ast_xs) =
				term_from ast_x ctx $ \ty_x x ->
				check_type (At (Just ast) ty_a) (At (Just ast_x) ty_x) $ \Refl ->
				go ty_a (x:as) ast_xs
		filter_from =
		 -- filter :: (a -> Bool) -> [a] -> [a]
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_a2Bool] ->
				term_from ast_a2Bool ctx $ \ty_a2Bool (TermLC a2Bool) ->
				check_type2 tyFun ast_a2Bool ty_a2Bool $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
				check_type (At Nothing tyBool) (At (Just ast_a2Bool) ty_a2Bool_Bool) $ \Refl ->
				k (tyList :$ ty_a2Bool_a ~> tyList :$ ty_a2Bool_a) $ TermLC $
				 \c -> lam $ filter (a2Bool c)
			 [ast_a2Bool, ast_la] ->
				term_from ast_a2Bool ctx $ \ty_a2Bool (TermLC a2Bool) ->
				term_from ast_la     ctx $ \ty_la     (TermLC la) ->
				check_type2 tyFun ast_a2Bool ty_a2Bool $ \Refl ty_a2Bool_a ty_a2Bool_Bool ->
				check_type (At Nothing tyBool) (At (Just ast_a2Bool) ty_a2Bool_Bool) $ \Refl ->
				check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
				check_type (At (Just ast_a2Bool) ty_a2Bool_a) (At (Just ast_la) ty_la_a) $ \Refl ->
				k (tyList :$ ty_a2Bool_a) $ TermLC $
				 \c -> filter (a2Bool c) (la c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 2
		zipWith_from =
		 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
			case ast_nodes ast of
			 [] -> Left $ Error_Term_Syntax $
				Error_Syntax_more_arguments_needed $ At (Just ast) 1
			 [ast_a2b2c] ->
				term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
				check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
				check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
				k ( tyList :$ ty_a2b2c_a
				 ~> tyList :$ ty_a2b2c_b2c_b
				 ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $
				 \c -> lam $ lam . zipWith (a2b2c c)
			 [ast_a2b2c, ast_la] ->
				term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
				term_from ast_la    ctx $ \ty_la    (TermLC la) ->
				check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
				check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
				check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
				check_type (At (Just ast_a2b2c) ty_a2b2c_a) (At (Just ast_la) ty_la_a) $ \Refl ->
				k ( tyList :$ ty_a2b2c_b2c_b
				 ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $
				 \c -> lam $ zipWith (a2b2c c) (la c)
			 [ast_a2b2c, ast_la, ast_lb] ->
				term_from ast_a2b2c ctx $ \ty_a2b2c (TermLC a2b2c) ->
				term_from ast_la    ctx $ \ty_la    (TermLC la) ->
				term_from ast_lb    ctx $ \ty_lb    (TermLC lb) ->
				check_type2 tyFun ast_a2b2c ty_a2b2c $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
				check_type2 tyFun ast_a2b2c ty_a2b2c_b2c $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
				check_type1 tyList ast_la ty_la $ \Refl ty_la_a ->
				check_type (At (Just ast_a2b2c) ty_a2b2c_a) (At (Just ast_la) ty_la_a) $ \Refl ->
				check_type1 tyList ast_lb ty_lb $ \Refl ty_lb_b ->
				check_type (At (Just ast_a2b2c) ty_a2b2c_b2c_b) (At (Just ast_lb) ty_lb_b) $ \Refl ->
				k (tyList :$ ty_a2b2c_b2c_c) $ TermLC $
				 \c -> zipWith (a2b2c c) (la c) (lb c)
			 _ -> Left $ Error_Term_Syntax $
				Error_Syntax_too_many_arguments $ At (Just ast) 3
		reverse_from =
		 -- reverse :: [a] -> [a]
			from_ast1 ast $ \ast_la ->
			term_from ast_la ctx $ \ty_la (TermLC la) ->
			check_type1 tyList ast_la ty_la $ \Refl _ty_la_a ->
			k ty_la $ TermLC $
			 \c -> reverse (la c)

-- | The '[]' 'Type'
tyList :: Inj_Const cs [] => Type cs []
tyList = TyConst inj_const

sym_List :: Proxy Sym_List
sym_List = Proxy

syList :: IsString a => [Syntax a] -> Syntax a
syList = Syntax "List"