{-# 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 qualified Data.MonoTraversable as MT
+import qualified Data.NonNull as NonNull
-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
+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 :: (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
+ 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
-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
- ]
+-- 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
-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
+-- Transforming
+instance (Sym_NonNull term, Sym_Lambda term) => Sym_NonNull (BetaT term)
-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)
+-- 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_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
+ _ | 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
- 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
+ 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
sourcephile / git / haskell / symantic.git / blobdiff