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

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

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

-- * 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 TyConsts_of_Iface (Proxy NonNull) = Proxy NonNull ': TyConsts_imported_by (Proxy NonNull)
type instance TyConsts_imported_by (Proxy NonNull) =
 [ Proxy (->)
 , Proxy (,)
 , Proxy Eq
 , Proxy Maybe
 , Proxy Ord
 , Proxy MT.MonoFoldable
 , Proxy MT.MonoFunctor
 , Proxy IsSequence
 , Proxy SemiSequence
 , Proxy Show
 ]

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 = textI1 "fromNullable"
	toNullable   = textI1 "toNullable"
	ncons        = textI2 "ncons"
	nuncons      = textI1 "nuncons"
	head         = textI1 "head"
	last         = textI1 "last"
	tail         = textI1 "tail"
	init         = textI1 "init"
	nfilter      = textI2 "nfilter"
instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
	fromNullable = dupI1 @Sym_NonNull fromNullable
	toNullable   = dupI1 @Sym_NonNull toNullable
	ncons        = dupI2 @Sym_NonNull ncons
	nuncons      = dupI1 @Sym_NonNull nuncons
	head         = dupI1 @Sym_NonNull head
	last         = dupI1 @Sym_NonNull last
	tail         = dupI1 @Sym_NonNull tail
	init         = dupI1 @Sym_NonNull init
	nfilter      = dupI2 @Sym_NonNull nfilter

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

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

instance -- Proj_TyConC
 ( Proj_TyConst cs NonNull
 , Proj_TyConsts cs (TyConsts_imported_by (Proxy NonNull))
 , Proj_TyCon cs
 ) => Proj_TyConC cs (Proxy NonNull) where
	proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ o))
	 | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
	 , Just Refl <- proj_TyConst c (Proxy @NonNull)
	 = case () of
		 _ | Just Refl <- proj_TyConst q (Proxy @Eq)
		   , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable)
		   , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)
		   , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Ord)
		   , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @SemiSequence)
		   , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
		   | Just Refl <- proj_TyConst q (Proxy @Show)
		   , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
		 _ -> Nothing
	proj_TyConC _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 -- CompileI
 ( Inj_TyConst cs NonNull
 , Inj_TyConst cs (->)
 , Inj_TyConst cs (,)
 , Inj_TyConst cs Bool
 , Inj_TyConst cs Maybe
 , Inj_TyConst cs MonoFoldable
 , Inj_TyConst cs IsSequence
 , Inj_TyConst cs SemiSequence
 , Proj_TyCon  cs
 , Proj_TyFam  cs TyFam_MonoElement
 , Compile cs is
 ) => CompileI cs is (Proxy NonNull) where
	compileI
	 :: forall meta ctx ret ls rs.
	 TokenT meta is (Proxy NonNull)
	 -> Compiler meta ctx ret cs is ls (Proxy NonNull ': rs)
	compileI tok ctx k =
		case tok of
		 Token_Term_NonNull_fromNullable tok_o ->
			-- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
			compile tok_o ctx $ \ty_o (Term o) ->
			check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ Term $
			 \c -> fromNullable (o c)
		 Token_Term_NonNull_toNullable tok_n ->
			-- toNullable :: MonoFoldable o => NonNull o -> o
			compile tok_n ctx $ \ty_n (Term n) ->
			check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
			check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			k ty_o $ Term $
			 \c -> toNullable (n c)
		 Token_Term_NonNull_ncons tok_e tok_s ->
			-- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
			compile tok_e ctx $ \ty_e (Term e) ->
			compile tok_s ctx $ \ty_s (Term s) ->
			check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
			check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_TyEq (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
			k (ty @NonNull :$ ty_s) $ Term $
			 \c -> ncons (e c) (s c)
		 Token_Term_NonNull_nuncons tok_n ->
			-- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
			compile tok_n ctx $ \ty_n (Term n) ->
			check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
			check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
			check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_TyEq
			 (At Nothing ty_s_e)
			 (At (Just tok_n) ty_s_e) $ \Refl ->
			k (ty @(,) :$ ty_s_e :$ (ty @Maybe :$ (ty @NonNull :$ ty_s))) $ Term $
			 \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
			compile tok_e2Bool ctx $ \ty_e2Bool (Term e2Bool) ->
			compile tok_n      ctx $ \ty_n      (Term s) ->
			check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
			check_TyEq
			 (At Nothing (ty @Bool))
			 (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
			check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
			check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
			check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
			check_TyEq
			 (At Nothing ty_s_e)
			 (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
			k ty_s $ Term $
			 \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
			compile tok_n ctx $ \ty_n (Term n) ->
			check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
			check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
			k ty_o_e $ Term $
			 \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
			compile tok_n ctx $ \ty_n (Term n) ->
			check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
			check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
			k ty_s $ Term $
			 \c -> f (n c)
instance -- TokenizeT
 Inj_Token meta ts NonNull =>
 TokenizeT meta ts (Proxy NonNull) where
	tokenizeT _t = mempty
	 { tokenizers_infix = tokenizeTMod []
		 [ tokenize1 "fromNullable" infixN5 Token_Term_NonNull_fromNullable
		 , tokenize1 "toNullable"   infixN5 Token_Term_NonNull_toNullable
		 , tokenize2 "ncons"        infixN5 Token_Term_NonNull_ncons
		 , tokenize1 "nuncons"      infixN5 Token_Term_NonNull_nuncons
		 , tokenize1 "head"         infixN5 Token_Term_NonNull_head
		 , tokenize1 "last"         infixN5 Token_Term_NonNull_last
		 , tokenize1 "tail"         infixN5 Token_Term_NonNull_tail
		 , tokenize1 "init"         infixN5 Token_Term_NonNull_init
		 , tokenize2 "nfilter"      infixN5 Token_Term_NonNull_nfilter
		 ]
	 }
instance Gram_Term_AtomsT meta ts (Proxy NonNull) g