{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=12 #-}
-- | Symantic for '[]'.
module Language.Symantic.Lib.List where

import Control.Monad (liftM, liftM2, liftM3)
import Data.Monoid ((<>))
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (zipWith)
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 qualified Data.MonoTraversable as MT
import qualified Data.Sequences as Seqs
import qualified Data.Text as Text
import qualified Data.Traversable as Traversable

import Language.Symantic.Parsing
import Language.Symantic.Typing
import Language.Symantic.Compiling
import Language.Symantic.Interpreting
import Language.Symantic.Transforming
import Language.Symantic.Lib.Lambda
import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement)

-- * Class 'Sym_List'
class Sym_List term where
	list_empty     :: term [a]
	list_singleton :: term a -> term [a]
	(.:)           :: term a -> term [a] -> term [a]; infixr 5 .:
	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

type instance Sym_of_Iface (Proxy []) = Sym_List
type instance TyConsts_of_Iface (Proxy []) = Proxy [] ': TyConsts_imported_by (Proxy [])
type instance TyConsts_imported_by (Proxy []) =
 [ Proxy Applicative
 , Proxy Bool
 , Proxy Eq
 , Proxy Foldable
 , Proxy Functor
 , Proxy Monad
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy Monoid
 , Proxy Ord
 , Proxy Seqs.IsSequence
 , Proxy Seqs.SemiSequence
 , 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 @Sym_List list_empty
	list_singleton = dupI1 @Sym_List list_singleton
	(.:)           = dupI2 @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 @Sym_List zipWith

instance
 ( Read_TyNameR TyName cs rs
 , Inj_TyConst cs []
 ) => Read_TyNameR TyName cs (Proxy [] ': rs) where
	read_TyNameR _cs (TyName "[]") k = k (ty @[])
	read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
instance Show_TyConst cs => Show_TyConst (Proxy [] ': cs) where
	show_TyConst TyConstZ{} = "[]"
	show_TyConst (TyConstS c) = show_TyConst c
instance Show_TyConst cs => Show_TyConst (Proxy String ': cs) where
	show_TyConst TyConstZ{} = "String"
	show_TyConst (TyConstS c) = show_TyConst c

instance -- Proj_TyFamC TyFam_MonoElement
 ( Proj_TyConst cs []
 ) => Proj_TyFamC cs TyFam_MonoElement [] where
	proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @[])
	 = Just ty_a
	proj_TyFamC _c _fam _ty = Nothing

instance -- Proj_TyConC
 ( Proj_TyConst cs []
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy []))
 , Proj_TyCon cs
 ) => Proj_TyConC cs (Proxy []) where
	proj_TyConC _ (TyConst q :$ TyConst c)
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @[])
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Foldable)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Traversable) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ a))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @[])
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Monoid) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)
		   , Just TyCon  <- proj_TyCon (t :$ a) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable)   -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)    -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Seqs.IsSequence)   -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Seqs.SemiSequence) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _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_TyName TyName cs
 , Inj_TyConst        cs []
 , Inj_TyConst        cs (->)
 , Compile cs is
 ) => CompileI cs is (Proxy []) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy [])
	 -> Compiler meta ctx ret cs 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 cs a) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_ty_a) $ kind_of ty_a) $ \Refl ->
			k (ty @[] :$ ty_a) $ Term $
				Fun.const list_empty
		 Token_Term_List_singleton tok_a ->
			-- [a] :: [a]
			compile tok_a ctx $ \ty_a (Term a) ->
			check_Kind
			 (At Nothing SKiType)
			 (At (Just tok_a) $ kind_of ty_a) $ \Refl ->
			k (ty @[] :$ ty_a) $ Term $
			 \c -> list_singleton (a c)
		 Token_Term_List_cons tok_a tok_as ->
			compile tok_a ctx $ \ty_a (Term a) ->
			compile tok_as ctx $ \ty_as (Term as) ->
			check_TyEq1 (ty @[]) (At (Just tok_as) ty_as) $ \Refl ty_as_a ->
			check_TyEq (At (Just tok_a) ty_a) (At (Just tok_as) ty_as_a) $ \Refl ->
			k ty_as $ Term $
			 \c -> a c .: as c
		 Token_Term_List_list tok_ty_a tok_as ->
			compile_Type tok_ty_a $ \(ty_a::Type cs 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 cs ty_a)
			   -> [Term ctx ty_a is '[] is]
			   -> [EToken meta is]
			   -> Either (Error_Term meta cs is) ret
			go ty_a as [] =
				k (ty @[] :$ unAt ty_a) $ Term $
				 \c -> list $ (\(Term a) -> a c)
					 Functor.<$> List.reverse as
			go ty_a as (tok_x:tok_xs) =
				compile 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]
			compile tok_a2b2c ctx $ \ty_a2b2c (Term a2b2c) ->
			check_TyEq2 (ty @(->)) (At (Just tok_a2b2c) ty_a2b2c) $ \Refl ty_a2b2c_a ty_a2b2c_b2c ->
			check_TyEq2 (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 ) $ Term $
			 \c -> lam $ lam . zipWith (a2b2c c)
instance -- TokenizeT
 Inj_Token meta ts [] =>
 TokenizeT meta ts (Proxy []) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ (TeName "[]",) $ ProTok_Term
			 { protok_term = \meta -> ProTokPi $ \a ->
				ProTok $ inj_EToken meta $ Token_Term_List_empty a
			 , protok_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
	gs_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)
			 <$> g_term
			 <*> option Nothing (Just <$ symbol "," <*> listG)