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)
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
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
instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)
instance NameTyOf NonNull where
nameTyOf _c = ["NonNull"] `Mod` "NonNull"
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
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
]
tyNonNull :: Source src => Type src vs a -> Type src vs (NonNull a)
tyNonNull a = tyConstLen @(K NonNull) @NonNull (lenVars a) `tyApp` a
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