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

import Data.MonoTraversable (MonoFoldable)
import Data.NonNull (NonNull)
import Data.Sequences (IsSequence, SemiSequence)
import Prelude hiding (head, init, last, tail)
import qualified Data.MonoTraversable as MT
import qualified Data.NonNull as NonNull

import Language.Symantic
import Language.Symantic.Lib.Bool (tyBool)
import Language.Symantic.Lib.Maybe (tyMaybe)
import Language.Symantic.Lib.MonoFoldable (tyMonoFoldable)
import Language.Symantic.Lib.MonoFunctor (Element, famElement, o0, e1)
import Language.Symantic.Lib.Sequences (tySemiSequence, tyIsSequence, s0)
import Language.Symantic.Lib.Tuple2 (tyTuple2)

-- * Class 'Sym_NonNull'
type instance Sym NonNull = 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 :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term o -> term (Maybe (NonNull o))
	default toNullable   :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term o
	default ncons        :: Sym_NonNull (UnT term) => Trans term => SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
	default nuncons      :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
	default head         :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)
	default last         :: Sym_NonNull (UnT term) => Trans term => MonoFoldable o => term (NonNull o) -> term (MT.Element o)
	default tail         :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term s
	default init         :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (NonNull s) -> term s
	default nfilter      :: Sym_NonNull (UnT term) => Trans term => IsSequence s   => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
	fromNullable = trans1 fromNullable
	toNullable   = trans1 toNullable
	ncons        = trans2 ncons
	nuncons      = trans1 nuncons
	head         = trans1 head
	last         = trans1 last
	tail         = trans1 tail
	init         = trans1 init
	nfilter      = trans2 nfilter

-- Interpreting
instance Sym_NonNull Eval where
	fromNullable = eval1 NonNull.fromNullable
	toNullable   = eval1 NonNull.toNullable
	ncons        = eval2 NonNull.ncons
	nuncons      = eval1 NonNull.nuncons
	head         = eval1 NonNull.head
	last         = eval1 NonNull.last
	tail         = eval1 NonNull.tail
	init         = eval1 NonNull.init
	nfilter      = eval2 NonNull.nfilter
instance Sym_NonNull View where
	fromNullable = view1 "fromNullable"
	toNullable   = view1 "toNullable"
	ncons        = view2 "ncons"
	nuncons      = view1 "nuncons"
	head         = view1 "head"
	last         = view1 "last"
	tail         = view1 "tail"
	init         = view1 "init"
	nfilter      = view2 "nfilter"
instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (Dup r1 r2) where
	fromNullable = dup1 @Sym_NonNull fromNullable
	toNullable   = dup1 @Sym_NonNull toNullable
	ncons        = dup2 @Sym_NonNull ncons
	nuncons      = dup1 @Sym_NonNull nuncons
	head         = dup1 @Sym_NonNull head
	last         = dup1 @Sym_NonNull last
	tail         = dup1 @Sym_NonNull tail
	init         = dup1 @Sym_NonNull init
	nfilter      = dup2 @Sym_NonNull nfilter

-- Transforming
instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)

-- Typing
instance FixityOf NonNull
instance TypeInstancesFor NonNull where
	expandFamFor c len f (TyApp _ z o `TypesS` TypesZ)
	 | Just HRefl <- proj_ConstKi @_ @Element f
	 , Just HRefl <- proj_ConstKiTy @_ @NonNull z
	 = expandFamFor c len f (o `TypesS` TypesZ)
	expandFamFor _c _len _fam _as = Nothing
instance ClassInstancesFor NonNull where
	proveConstraintFor _ (TyApp _ tq@(TyConst _ _ q) (TyApp _ c o))
	 | Just HRefl <- proj_ConstKiTy @_ @NonNull c
	 = case () of
		 _ | Just Refl <- proj_Const @Eq q
		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFoldable q
		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
		   | Just Refl <- proj_Const @MT.MonoFunctor q
		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
		   | Just Refl <- proj_Const @Ord q
		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
		   | Just Refl <- proj_Const @SemiSequence q
		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
		   | Just Refl <- proj_Const @Show q
		   , Just Dict <- proveConstraint (tq `tyApp` o) -> Just Dict
		 _ -> Nothing
	proveConstraintFor _c _q = Nothing

-- Compiling
instance Gram_Term_AtomsFor src ss g NonNull
instance (Source src, SymInj ss NonNull) => ModuleFor src ss NonNull where
	moduleFor = ["NonNull"] `moduleWhere`
	 [ "fromNullable" := teNonNull_fromNullable
	 , "toNullable"   := teNonNull_toNullable
	 , "ncons"        := teNonNull_ncons
	 , "nuncons"      := teNonNull_nuncons
	 , "head"         := teNonNull_head
	 , "last"         := teNonNull_last
	 , "tail"         := teNonNull_tail
	 , "init"         := teNonNull_init
	 , "nfilter"      := teNonNull_nfilter
	 ]

-- ** 'Type's
tyNonNull :: Source src => Type src vs a -> Type src vs (NonNull a)
tyNonNull a = tyConstLen @(K NonNull) @NonNull (lenVars a) `tyApp` a

-- ** 'Term's
teNonNull_fromNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (o -> Maybe (NonNull o)))
teNonNull_fromNullable = Term (tyMonoFoldable o0) (o0 ~> tyMaybe (tyNonNull o0)) $ teSym @NonNull $ lam1 fromNullable

teNonNull_toNullable :: TermDef NonNull '[Proxy o] (MonoFoldable o #> (NonNull o -> o))
teNonNull_toNullable = Term (tyMonoFoldable o0) (tyNonNull o0 ~> o0) $ teSym @NonNull $ lam1 toNullable

teNonNull_ncons :: TermDef NonNull '[Proxy s, Proxy e] (SemiSequence s # e #~ MT.Element s #> (e -> s -> NonNull s))
teNonNull_ncons = Term (tySemiSequence s0 # e1 #~ famElement s0) (e1 ~> s0 ~> tyNonNull s0) $ teSym @NonNull $ lam2 ncons

teNonNull_nuncons :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> (NonNull s -> (e, Maybe (NonNull s))))
teNonNull_nuncons = Term (tyIsSequence s0 # e1 #~ famElement s0) (tyNonNull s0 ~> e1 `tyTuple2` tyMaybe (tyNonNull s0)) $ teSym @NonNull $ lam1 nuncons

teNonNull_nfilter :: TermDef NonNull '[Proxy s, Proxy e] (IsSequence s # e #~ MT.Element s #> ((e -> Bool) -> NonNull s -> s))
teNonNull_nfilter = Term (tyIsSequence s0 # e1 #~ famElement s0) ((e1 ~> tyBool) ~> tyNonNull s0 ~> s0) $ teSym @NonNull $ lam2 nfilter

teNonNull_head, teNonNull_last :: TermDef NonNull '[Proxy o, Proxy e] (MonoFoldable o # e #~ MT.Element o #> (NonNull o -> e))
teNonNull_head = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head
teNonNull_last = Term (tyMonoFoldable o0 # e1 #~ famElement o0) (tyNonNull o0 ~> e1) $ teSym @NonNull $ lam1 head

teNonNull_tail, teNonNull_init :: TermDef NonNull '[Proxy s] (IsSequence s #> (NonNull s -> s))
teNonNull_tail = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 tail
teNonNull_init = Term (tyIsSequence s0) (tyNonNull s0 ~> s0) $ teSym @NonNull $ lam1 init