{-# 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