{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fconstraint-solver-iterations=8 #-}
-- | Symantic for 'NonNull'.
module Language.Symantic.Compiling.NonNull where

import Control.Monad (liftM, liftM2)
import Data.MonoTraversable (MonoFoldable)
import qualified Data.MonoTraversable as MT
import Data.NonNull (NonNull)
import qualified Data.NonNull as NonNull
import Data.Proxy
import Data.Sequences (IsSequence, SemiSequence)
import Data.Text (Text)
import Data.Type.Equality ((:~:)(Refl))
import Prelude hiding (head, init, last, tail)

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

-- * Class 'Sym_NonNull'
class Sym_NonNull term where
	fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
	toNullable :: MonoFoldable o => term (NonNull o) -> term o
	ncons :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
	nuncons :: IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
	head :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
	last :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
	tail :: IsSequence s => term (NonNull s) -> term s
	init :: IsSequence s => term (NonNull s) -> term s
	nfilter :: IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
	default fromNullable :: (Trans t term, MonoFoldable o) => t term o -> t term (Maybe (NonNull o))
	default toNullable :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term o
	default ncons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term (NonNull s)
	default nuncons :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term (MT.Element s, Maybe (NonNull s))
	default head :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
	default last :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
	default tail :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
	default init :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
	default nfilter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term (NonNull s) -> t term s
	fromNullable = trans_map1 fromNullable
	toNullable   = trans_map1 toNullable
	ncons        = trans_map2 ncons
	nuncons      = trans_map1 nuncons
	head         = trans_map1 head
	last         = trans_map1 last
	tail         = trans_map1 tail
	init         = trans_map1 init
	nfilter      = trans_map2 nfilter

type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
type instance Consts_of_Iface (Proxy NonNull) = Proxy NonNull ': Consts_imported_by NonNull
type instance Consts_imported_by NonNull =
 [ Proxy (->)
 , Proxy (,)
 , Proxy Eq
 , Proxy Maybe
 , Proxy Ord
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy IsSequence
 , Proxy SemiSequence
 ]

instance Sym_NonNull HostI where
	fromNullable = liftM  NonNull.fromNullable
	toNullable   = liftM  NonNull.toNullable
	ncons        = liftM2 NonNull.ncons
	nuncons      = liftM  NonNull.nuncons
	head         = liftM  NonNull.head
	last         = liftM  NonNull.last
	tail         = liftM  NonNull.tail
	init         = liftM  NonNull.init
	nfilter      = liftM2 NonNull.nfilter
instance Sym_NonNull TextI where
	fromNullable = textI_app1 "fromNullable"
	toNullable   = textI_app1 "toNullable"
	ncons        = textI_app2 "ncons"
	nuncons      = textI_app1 "nuncons"
	head         = textI_app1 "head"
	last         = textI_app1 "last"
	tail         = textI_app1 "tail"
	init         = textI_app1 "init"
	nfilter      = textI_app2 "nfilter"
instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
	fromNullable = dupI1 (Proxy @Sym_NonNull) fromNullable
	toNullable   = dupI1 (Proxy @Sym_NonNull) toNullable
	ncons        = dupI2 (Proxy @Sym_NonNull) ncons
	nuncons      = dupI1 (Proxy @Sym_NonNull) nuncons
	head         = dupI1 (Proxy @Sym_NonNull) head
	last         = dupI1 (Proxy @Sym_NonNull) last
	tail         = dupI1 (Proxy @Sym_NonNull) tail
	init         = dupI1 (Proxy @Sym_NonNull) init
	nfilter      = dupI2 (Proxy @Sym_NonNull) nfilter

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

instance -- Fam_MonoElement
 ( Proj_Const cs NonNull
 , Proj_Fam cs Fam_MonoElement
 ) => Proj_FamC cs Fam_MonoElement NonNull where
	proj_famC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy NonNull)
	 = proj_fam Fam_MonoElement (ty_o `TypesS` TypesZ)
	proj_famC _c _fam _ty = Nothing
instance -- Proj_ConC
 ( Proj_Const cs NonNull
 , Proj_Consts cs (Consts_imported_by NonNull)
 , Proj_Con cs
 ) => Proj_ConC cs (Proxy NonNull) where
	proj_conC _ (t@(TyConst q) :$ (TyConst c :$ o))
	 | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_const c (Proxy::Proxy NonNull)
	 = case () of
		 _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFoldable)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFunctor)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy Ord)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		   | Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
		   , Just Con  <- proj_con (t :$ o) -> Just Con
		 _ -> Nothing
	proj_conC _c _q = Nothing
data instance TokenT meta (ts::[*]) (Proxy NonNull)
 = Token_Term_NonNull_fromNullable (EToken meta ts)
 | Token_Term_NonNull_toNullable   (EToken meta ts)
 | Token_Term_NonNull_ncons        (EToken meta ts) (EToken meta ts)
 | Token_Term_NonNull_nuncons      (EToken meta ts)
 | Token_Term_NonNull_head         (EToken meta ts)
 | Token_Term_NonNull_last         (EToken meta ts)
 | Token_Term_NonNull_tail         (EToken meta ts)
 | Token_Term_NonNull_init         (EToken meta ts)
 | Token_Term_NonNull_nfilter      (EToken meta ts) (EToken meta ts)
deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy NonNull))
deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy NonNull))
instance -- Term_fromI
 ( Inj_Const (Consts_of_Ifaces is) NonNull
 , Inj_Const (Consts_of_Ifaces is) (->)
 , Inj_Const (Consts_of_Ifaces is) (,)
 , Inj_Const (Consts_of_Ifaces is) Bool
 , Inj_Const (Consts_of_Ifaces is) Maybe
 , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 , Inj_Const (Consts_of_Ifaces is) IsSequence
 , Inj_Const (Consts_of_Ifaces is) SemiSequence
 , Proj_Con  (Consts_of_Ifaces is)
 , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 , Term_from is
 ) => Term_fromI is (Proxy NonNull) where
	term_fromI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy NonNull)
	 -> Term_fromT meta ctx ret is ls (Proxy NonNull ': rs)
	term_fromI tok ctx k =
		case tok of
		 Token_Term_NonNull_fromNullable tok_o ->
			-- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
			term_from tok_o ctx $ \ty_o (TermLC o) ->
			check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
			k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ TermLC $
			 \c -> fromNullable (o c)
		 Token_Term_NonNull_toNullable tok_n ->
			-- toNullable :: MonoFoldable o => NonNull o -> o
			term_from tok_n ctx $ \ty_n (TermLC n) ->
			check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
			check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
			k ty_o $ TermLC $
			 \c -> toNullable (n c)
		 Token_Term_NonNull_ncons tok_e tok_s ->
			-- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
			term_from tok_e ctx $ \ty_e (TermLC e) ->
			term_from tok_s ctx $ \ty_s (TermLC s) ->
			check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
			check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
			k (ty @NonNull :$ ty_s) $ TermLC $
			 \c -> ncons (e c) (s c)
		 Token_Term_NonNull_nuncons tok_n ->
			-- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
			term_from tok_n ctx $ \ty_n (TermLC n) ->
			check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
			check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
			check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type
			 (At Nothing ty_s_e)
			 (At (Just tok_n) ty_s_e) $ \Refl ->
			k (ty @(,) :$ ty_s_e :$ (ty @Maybe :$ (ty @NonNull :$ ty_s))) $ TermLC $
			 \c -> nuncons (n c)
		 Token_Term_NonNull_head tok_n -> n2e_from tok_n head
		 Token_Term_NonNull_last tok_n -> n2e_from tok_n last
		 Token_Term_NonNull_tail tok_n -> n2s_from tok_n tail
		 Token_Term_NonNull_init tok_n -> n2s_from tok_n init
		 Token_Term_NonNull_nfilter tok_e2Bool tok_n ->
			-- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
			term_from tok_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
			term_from tok_n      ctx $ \ty_n      (TermLC s) ->
			check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_type
			 (At Nothing (ty @Bool))
			 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
			check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
			check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_type
			 (At Nothing ty_s_e)
			 (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
			k ty_s $ TermLC $
			 \c -> nfilter (e2Bool c) (s c)
		where
		n2e_from tok_n
		 (f::forall term o.
			 (Sym_NonNull term, MonoFoldable o)
			 => term (NonNull o) -> term (MT.Element o)) =
		 -- head :: MonoFoldable o => NonNull o -> MT.Element o
		 -- last :: MonoFoldable o => NonNull o -> MT.Element o
			term_from tok_n ctx $ \ty_n (TermLC n) ->
			check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
			check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
			check_fam (At (Just tok_n) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			k ty_o_e $ TermLC $
			 \c -> f (n c)
		n2s_from tok_n
		 (f::forall term s.
			 (Sym_NonNull term, IsSequence s)
			 => term (NonNull s) -> term s) =
		 -- tail :: IsSequence s => NonNull s -> s
		 -- init :: IsSequence s => NonNull s -> s
			term_from tok_n ctx $ \ty_n (TermLC n) ->
			check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
			check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
			k ty_s $ TermLC $
			 \c -> f (n c)
		{-
		 "ncons"        -> ncons_from
		 "nuncons"      -> nuncons_from
		 "head"         -> n2e_from head
		 "last"         -> n2e_from last
		 "tail"         -> n2s_from tail
		 "init"         -> n2s_from init
		 "nfilter"      -> nfilter_from
		 _ -> Left $ Error_Term_unsupported
		where
		fromNullable_from =
		toNullable_from =
		ncons_from =
		nuncons_from =
		nfilter_from =
		-}