{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
-- | 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 qualified Data.Text as Text
import qualified Data.Traversable as Traversable
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (zipWith)

import Language.Symantic.Parsing
import Language.Symantic.Parsing.Grammar
import Language.Symantic.Typing
import Language.Symantic.Compiling.Term
import Language.Symantic.Compiling.Lambda
import Language.Symantic.Interpreting
import Language.Symantic.Transforming.Trans

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

infixr 5 .:

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 Show
 , Proxy Traversable
 ]

instance Sym_List HostI where
	list_empty     = return []
	list_singleton = liftM return
	(.:)           = liftM2 (:)
	list           = Traversable.sequence
	zipWith        = liftM3 List.zipWith
instance Sym_List TextI where
	list_empty = TextI $ \_p _v -> "[]"
	list_singleton a = textI_infix ":" op a list_empty
		where op = infixR 5
	(.:) = textI_infix ":" (infixR 5)
	list l = TextI $ \_po v ->
		"[" <> Text.intercalate ", " ((\(TextI a) -> a op v) Functor.<$> l) <> "]"
		where op = (infixN0, L)
	zipWith = textI3 "zipWith"
instance (Sym_List r1, Sym_List r2) => Sym_List (DupI r1 r2) where
	list_empty = dupI0 (Proxy @Sym_List) list_empty
	list_singleton = dupI1 (Proxy @Sym_List) list_singleton
	(.:) = dupI2 (Proxy @Sym_List) (.:)
	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 (Proxy @Sym_List) zipWith

instance
 ( Read_TypeNameR Type_Name cs rs
 , Inj_Const cs []
 ) => Read_TypeNameR Type_Name cs (Proxy [] ': rs) where
	read_typenameR _cs (Type_Name "[]") k = k (ty @[])
	read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
instance Show_Const cs => Show_Const (Proxy [] ': cs) where
	show_const ConstZ{} = "[]"
	show_const (ConstS c) = show_const c
instance Show_Const cs => Show_Const (Proxy String ': cs) where
	show_const ConstZ{} = "String"
	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 @[])
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
		   | Just Refl <- proj_const q (Proxy @Foldable)    -> Just Con
		   | Just Refl <- proj_const q (Proxy @Functor)     -> Just Con
		   | Just Refl <- proj_const q (Proxy @Monad)       -> Just Con
		   | Just Refl <- proj_const q (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 @[])
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy @Eq)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy @Monoid) -> Just Con
		   | Just Refl <- proj_const q (Proxy @Show)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		   | Just Refl <- proj_const q (Proxy @Ord)
		   , Just Con  <- proj_con (t :$ a) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy [])
 = Token_Term_List_empty     (EToken meta '[Proxy Token_Type])
 | Token_Term_List_cons      (EToken meta ts) (EToken meta ts)
 | Token_Term_List_singleton (EToken meta ts)
 | Token_Term_List_list      (EToken meta '[Proxy Token_Type]) [EToken meta ts]
 | Token_Term_List_zipWith   (EToken meta ts)
deriving instance (Eq meta, Eq_Token meta ts) => Eq (TokenT meta ts (Proxy []))
deriving instance (Show meta, Show_Token meta ts) => Show (TokenT meta ts (Proxy []))
instance -- CompileI
 ( Read_TypeName Type_Name (Consts_of_Ifaces is)
 , Inj_Const (Consts_of_Ifaces is) []
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Compile is
 ) => CompileI is (Proxy []) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy [])
	 -> CompileT meta ctx ret is ls (Proxy [] ': rs)
	compileI tok ctx k =
		case tok of
		 Token_Term_List_empty tok_ty_a ->
			-- [] :: [a]
			compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			k (ty @[] :$ ty_a) $ TermO $
				Fun.const list_empty
		 Token_Term_List_singleton tok_a ->
			-- [a] :: [a]
			compileO tok_a ctx $ \ty_a (TermO a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_a) $ kind_of ty_a) $ \Refl ->
			k (ty @[] :$ ty_a) $ TermO $
			 \c -> list_singleton (a c)
		 Token_Term_List_cons tok_a tok_as ->
			compileO tok_a ctx $ \ty_a (TermO a) ->
			compileO tok_as ctx $ \ty_as (TermO as) ->
			check_type1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
			check_type (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl ->
			k ty_as $ TermO $
			 \c -> a c .: as c
		 Token_Term_List_list tok_ty_a tok_as ->
			compile_type tok_ty_a $ \(ty_a::Type (Consts_of_Ifaces is) a) ->
			check_kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			go (At (Just tok_ty_a) ty_a) [] tok_as
			where
			go :: At meta '[Proxy Token_Type] (Type (Consts_of_Ifaces is) ty_a)
			   -> [TermO ctx ty_a is '[] is]
			   -> [EToken meta is]
			   -> Either (Error_Term meta is) ret
			go ty_a as [] =
				k (ty @[] :$ unAt ty_a) $ TermO $
				 \c -> list $ (\(TermO a) -> a c)
					 Functor.<$> List.reverse as
			go ty_a as (tok_x:tok_xs) =
				compileO tok_x ctx $ \ty_x x ->
				check_type_is ty_a (At (Just tok_x) ty_x) $ \Refl ->
				go ty_a (x:as) tok_xs
		 Token_Term_List_zipWith tok_a2b2c ->
			-- zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
			compileO tok_a2b2c ctx $ \ty_a2b2c (TermO a2b2c) ->
			check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
			check_type2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c_b2c) $ \Refl ty_a2b2c_b2c_b ty_a2b2c_b2c_c ->
			k ( ty @[] :$ ty_a2b2c_a
			 ~> ty @[] :$ ty_a2b2c_b2c_b
			 ~> ty @[] :$ ty_a2b2c_b2c_c ) $ TermO $
			 \c -> lam $ lam . zipWith (a2b2c c)
instance -- TokenizeT
 Inj_Token meta ts [] =>
 TokenizeT meta ts (Proxy []) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ (Term_Name "[]",) $ Term_ProTok
			 { term_protok = \meta -> ProTokPi $ \a ->
				ProTok $ inj_etoken meta $ Token_Term_List_empty a
			 , term_fixity = infixN5
			 }
		 , tokenize2 ":" (infixR 5) Token_Term_List_cons
		 , tokenize1 "zipWith" infixN0 Token_Term_List_zipWith
		 ]
	 }
instance
 ( App g
 , Gram_Rule g
 , Gram_Lexer g
 , Gram_Term ts meta g
 , Inj_Token meta ts (->)
 , Inj_Token meta ts []
 ) => Gram_Term_AtomsT meta ts (Proxy []) g where
	term_atomsT _t =
	 [ rule "term_list" $
		ProTok <$> between (symbol "[") (symbol "]") listG
	 , rule "term_list_empty" $
		metaG $
		(\meta -> ProTokPi $ \a -> ProTok $ inj_etoken meta $ Token_Term_List_empty a)
		 <$ symbol "["
		 <* symbol "]"
	 ]
		where
		listG :: CF g (EToken meta ts)
		listG = rule "list" $
			metaG $
			(\a mb meta -> inj_etoken meta $ case mb of
			 Just b  -> Token_Term_List_cons a b
			 Nothing -> Token_Term_List_singleton a)
			 <$> termG
			 <*> option Nothing (Just <$ symbol "," <*> listG)