{-# 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 NameTyOf NonNull where
        nameTyOf _c = ["NonNull"] `Mod` "NonNull"
instance FixityOf NonNull
instance TypeInstancesFor NonNull where
        expandFamFor c len f (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 _ (tq@(TyConst _ _ q) :$ 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