{-# 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=8 #-}
-- | Symantic for '[]'.
module Language.Symantic.Compiling.List where

import Control.Monad (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 (zipWith)

import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

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

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 Bool
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy Monoid
 , Proxy Ord
 , Proxy Traversable
 ]

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

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 [])
	 = 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 [])
	 = 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
		   | 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) (->)
 , Term_from is ast
 ) => Term_fromI is (Proxy []) ast where
	term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy [] ': rs)
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "[]"      -> list_empty_from
		 "list"    -> list_from
		 "zipWith" -> zipWith_from
		 _ -> Left $ Error_Term_unsupported
		where
		list_empty_from =
		 -- [] :: [a]
			from_ast1 ast $ \ast_ty_a 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 ->
			k as (tyList :$ ty_a) $ TermLC $
				Fun.const list_empty
		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
		zipWith_from =
		 -- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
			from_ast1 ast $ \ast_a2b2c as ->
			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 as ( tyList :$ ty_a2b2c_a
			 ~> tyList :$ ty_a2b2c_b2c_b
			 ~> tyList :$ ty_a2b2c_b2c_c ) $ TermLC $
			 \c -> lam $ lam . zipWith (a2b2c 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"