{-# 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 Data.NonNull (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 (TyFam_MonoElement(..)) -- * Class '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 type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull type instance TyConsts_of_Iface (Proxy NonNull) = Proxy NonNull ': TyConsts_imported_by (Proxy NonNull) type instance TyConsts_imported_by (Proxy NonNull) = [ Proxy (->) , Proxy (,) , Proxy Eq , Proxy Maybe , Proxy Ord , Proxy MT.MonoFoldable , Proxy MT.MonoFunctor , Proxy IsSequence , Proxy SemiSequence , Proxy Show ] 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 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 -- Proj_TyFamC 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 (Proxy 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) = 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 _ -> 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) -> Compiler 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) compile tok_o ctx $ \ty_o (Term o) -> check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon -> k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ Term $ \c -> fromNullable (o c) Token_Term_NonNull_toNullable tok_n -> -- toNullable :: MonoFoldable o => NonNull o -> o compile tok_n ctx $ \ty_n (Term 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 $ Term $ \c -> toNullable (n c) Token_Term_NonNull_ncons tok_e tok_s -> -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s compile tok_e ctx $ \ty_e (Term e) -> compile tok_s ctx $ \ty_s (Term 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) $ Term $ \c -> ncons (e c) (s c) Token_Term_NonNull_nuncons tok_n -> -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s)) compile tok_n ctx $ \ty_n (Term 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))) $ Term $ \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 compile tok_e2Bool ctx $ \ty_e2Bool (Term e2Bool) -> compile tok_n ctx $ \ty_n (Term 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 $ Term $ \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 compile tok_n ctx $ \ty_n (Term 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 $ Term $ \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 compile tok_n ctx $ \ty_n (Term 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 $ Term $ \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