{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-- | Symantic for 'Sequences'.
module Language.Symantic.Compiling.Sequences where

import Control.Monad (liftM, liftM2)
import qualified Data.MonoTraversable as MT
import Data.Proxy
import Data.Sequences (SemiSequence, IsSequence)
import qualified Data.Sequences as Seqs
import Data.String (IsString)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (filter, reverse)

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

-- * Class 'Sym_SemiSequence'
class Sym_SemiSequence term where
	intersperse :: SemiSequence s => term (MT.Element s) -> term s -> term s
	cons :: SemiSequence s => term (MT.Element s) -> term s -> term s
	snoc :: SemiSequence s => term s -> term (MT.Element s) -> term s
	reverse :: SemiSequence s => term s -> term s
	default intersperse :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
	default cons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term s
	default snoc :: (Trans t term, SemiSequence s) => t term s -> t term (MT.Element s) -> t term s
	default reverse :: (Trans t term, SemiSequence s) => t term s -> t term s
	intersperse = trans_map2 cons
	cons        = trans_map2 cons
	snoc        = trans_map2 snoc
	reverse     = trans_map1 reverse

type instance Sym_of_Iface (Proxy SemiSequence) = Sym_SemiSequence
type instance Consts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': Consts_imported_by SemiSequence
type instance Consts_imported_by SemiSequence =
 [ Proxy SemiSequence
 , Proxy []
 , Proxy Text
 ]

instance Sym_SemiSequence HostI where
	intersperse = liftM2 Seqs.intersperse
	cons        = liftM2 Seqs.cons
	snoc        = liftM2 Seqs.snoc
	reverse     = liftM  Seqs.reverse
instance Sym_SemiSequence TextI where
	intersperse = textI_app2 "intersperse"
	cons        = textI_app2 "cons"
	snoc        = textI_app2 "snoc"
	reverse     = textI_app1 "reverse"
instance (Sym_SemiSequence r1, Sym_SemiSequence r2) => Sym_SemiSequence (DupI r1 r2) where
	intersperse = dupI2 sym_SemiSequence intersperse
	cons        = dupI2 sym_SemiSequence cons
	snoc        = dupI2 sym_SemiSequence snoc
	reverse     = dupI1 sym_SemiSequence reverse

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

instance -- Proj_ConC
 ( Proj_Const cs SemiSequence
 , Proj_Consts cs (Consts_imported_by SemiSequence)
 ) => Proj_ConC cs (Proxy SemiSequence) where
	proj_conC _ (TyConst q :$ s)
	 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_const c) SKiType ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
			 _ -> Nothing
		 TyConst c :$ _o
		  | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
			 _ -> Nothing
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) SemiSequence
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 , Term_from is ast
 ) => Term_fromI is (Proxy SemiSequence) ast where
	term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy SemiSequence ': rs)
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "intersperse" -> e2s2s_from intersperse
		 "cons"        -> e2s2s_from cons
		 "snoc"        -> snoc_from
		 "reverse"     -> reverse_from
		 _ -> Left $ Error_Term_unsupported
		where
		e2s2s_from
		 (f::forall term s.
			 (Sym_SemiSequence term, SemiSequence s)
			 => term (MT.Element s) -> term s -> term s) =
		 -- intersperse :: SemiSequence s => MT.Element s -> s -> s
		 -- cons        :: SemiSequence s => MT.Element s -> s -> s
			from_ast2 ast $ \ast_e ast_s as ->
			term_from ast_e ctx $ \ty_e (TermLC e) ->
			term_from ast_s ctx $ \ty_s (TermLC s) ->
			check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
			check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (At Nothing ty_s_e) (At (Just ast_e) ty_e) $ \Refl ->
			k as ty_s $ TermLC $
			 \c -> f (e c) (s c)
		snoc_from =
		 -- snoc :: SemiSequence s => s -> MT.Element s -> s
			from_ast2 ast $ \ast_s ast_e as ->
			term_from ast_s ctx $ \ty_s (TermLC s) ->
			term_from ast_e ctx $ \ty_e (TermLC e) ->
			check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
			check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (At Nothing ty_s_e) (At (Just ast_e) ty_e) $ \Refl ->
			k as ty_s $ TermLC $
			 \c -> snoc (s c) (e c)
		reverse_from =
		 -- reverse :: SemiSequence s => s -> s
			from_ast1 ast $ \ast_s as ->
			term_from ast_s ctx $ \ty_s (TermLC s) ->
			check_constraint (At (Just ast_s) (tySemiSequence :$ ty_s)) $ \Con ->
			k as ty_s $ TermLC $
			 \c -> reverse (s c)

-- | The 'SemiSequence' 'Type'
tySemiSequence :: Inj_Const cs SemiSequence => Type cs SemiSequence
tySemiSequence = TyConst inj_const

sym_SemiSequence :: Proxy Sym_SemiSequence
sym_SemiSequence = Proxy

sySemiSequence :: IsString a => [Syntax a] -> Syntax a
sySemiSequence = Syntax "SemiSequence"

-- * Class 'Sym_IsSequence'
class Sym_IsSequence term where
	filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
	default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
	filter  = trans_map2 filter

type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
type instance Consts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': Consts_imported_by IsSequence
type instance Consts_imported_by IsSequence =
 [ Proxy IsSequence
 , Proxy (->)
 , Proxy []
 , Proxy Text
 , Proxy Bool
 ]

instance Sym_IsSequence HostI where
	filter  = liftM2 Seqs.filter
instance Sym_IsSequence TextI where
	filter  = textI_app2 "filter"
instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
	filter  = dupI2 sym_IsSequence filter

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

instance -- Proj_ConC
 ( Proj_Const cs IsSequence
 , Proj_Consts cs (Consts_imported_by IsSequence)
 ) => Proj_ConC cs (Proxy IsSequence) where
	proj_conC _ (TyConst q :$ s)
	 | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
	 , Just Refl <- proj_const q (Proxy::Proxy IsSequence)
	 = case s of
		 TyConst c
		  | Just Refl <- eq_skind (kind_of_const c) SKiType ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
			 _ -> Nothing
		 TyConst c :$ _o
		  | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
			case () of
			 _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
			 _ -> Nothing
		 _ -> Nothing
	proj_conC _c _q = Nothing
instance -- Term_fromI
 ( AST ast
 , Lexem ast ~ LamVarName
 , Inj_Const (Consts_of_Ifaces is) IsSequence
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 , Term_from is ast
 ) => Term_fromI is (Proxy IsSequence) ast where
	term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy IsSequence ': rs)
	term_fromI ast ctx k =
		case ast_lexem ast of
		 "filter" -> filter_from
		 _ -> Left $ Error_Term_unsupported
		where
		filter_from =
		 -- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
			from_ast2 ast $ \ast_e2Bool ast_s as ->
			term_from ast_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
			term_from ast_s      ctx $ \ty_s      (TermLC s) ->
			check_type2 tyFun ast_e2Bool ty_e2Bool $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_type (At Nothing tyBool) (At (Just ast_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			check_constraint (At (Just ast_s) (tyIsSequence :$ ty_s)) $ \Con ->
			check_family ast Fam_MonoElement (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (At Nothing ty_s_e) (At (Just ast_e2Bool) ty_e2Bool_e) $ \Refl ->
			k as ty_s $ TermLC $
			 \c -> filter (e2Bool c) (s c)

-- | The 'IsSequence' 'Type'
tyIsSequence :: Inj_Const cs IsSequence => Type cs IsSequence
tyIsSequence = TyConst inj_const

sym_IsSequence :: Proxy Sym_IsSequence
sym_IsSequence = Proxy

syIsSequence :: IsString a => [Syntax a] -> Syntax a
syIsSequence = Syntax "IsSequence"