{-# 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 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.Type.Equality ((:~:)(Refl))
import Prelude hiding (head, init, last, tail)

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

-- * 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 NonNull
type instance TyConsts_imported_by 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 -- 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 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)
	 -> CompileT 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)
			compileO tok_o ctx $ \ty_o (TermO o) ->
			check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
			k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ TermO $
			 \c -> fromNullable (o c)
		 Token_Term_NonNull_toNullable tok_n ->
			-- toNullable :: MonoFoldable o => NonNull o -> o
			compileO tok_n ctx $ \ty_n (TermO 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 $ TermO $
			 \c -> toNullable (n c)
		 Token_Term_NonNull_ncons tok_e tok_s ->
			-- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
			compileO tok_e ctx $ \ty_e (TermO e) ->
			compileO tok_s ctx $ \ty_s (TermO 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) $ TermO $
			 \c -> ncons (e c) (s c)
		 Token_Term_NonNull_nuncons tok_n ->
			-- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
			compileO tok_n ctx $ \ty_n (TermO 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))) $ TermO $
			 \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
			compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
			compileO tok_n      ctx $ \ty_n      (TermO 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 $ TermO $
			 \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
			compileO tok_n ctx $ \ty_n (TermO 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 $ TermO $
			 \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
			compileO tok_n ctx $ \ty_n (TermO 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 $ TermO $
			 \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