symantic-lib/Language/Symantic/Lib/NonNull.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
   4 -- | Symantic for 'NonNull'.
   5 module Language.Symantic.Lib.NonNull where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.MonoTraversable (MonoFoldable)
   9 import qualified Data.MonoTraversable as MT
  10 import Data.NonNull (NonNull)
  11 import qualified Data.NonNull as NonNull
  12 import Data.Proxy
  13 import Data.Sequences (IsSequence, SemiSequence)
  14 import Data.Type.Equality ((:~:)(Refl))
  15 import Prelude hiding (head, init, last, tail)
  16
  17 import Language.Symantic.Parsing
  18 import Language.Symantic.Typing
  19 import Language.Symantic.Compiling
  20 import Language.Symantic.Interpreting
  21 import Language.Symantic.Transforming
  22 import Language.Symantic.Lib.MonoFunctor
  23
  24 -- * Class 'Sym_NonNull'
  25 class Sym_NonNull term where
  26         fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
  27         toNullable :: MonoFoldable o => term (NonNull o) -> term o
  28         ncons :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
  29         nuncons :: IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
  30         head :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  31         last :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  32         tail :: IsSequence s => term (NonNull s) -> term s
  33         init :: IsSequence s => term (NonNull s) -> term s
  34         nfilter :: IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
  35         default fromNullable :: (Trans t term, MonoFoldable o) => t term o -> t term (Maybe (NonNull o))
  36         default toNullable :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term o
  37         default ncons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term (NonNull s)
  38         default nuncons :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term (MT.Element s, Maybe (NonNull s))
  39         default head :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
  40         default last :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
  41         default tail :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
  42         default init :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
  43         default nfilter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term (NonNull s) -> t term s
  44         fromNullable = trans_map1 fromNullable
  45         toNullable   = trans_map1 toNullable
  46         ncons        = trans_map2 ncons
  47         nuncons      = trans_map1 nuncons
  48         head         = trans_map1 head
  49         last         = trans_map1 last
  50         tail         = trans_map1 tail
  51         init         = trans_map1 init
  52         nfilter      = trans_map2 nfilter
  53
  54 type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
  55 type instance TyConsts_of_Iface (Proxy NonNull) = Proxy NonNull ': TyConsts_imported_by NonNull
  56 type instance TyConsts_imported_by NonNull =
  57  [ Proxy (->)
  58  , Proxy (,)
  59  , Proxy Eq
  60  , Proxy Maybe
  61  , Proxy Ord
  62  , Proxy MT.MonoFoldable
  63  , Proxy MT.MonoFunctor
  64  , Proxy IsSequence
  65  , Proxy SemiSequence
  66  , Proxy Show
  67  ]
  68
  69 instance Sym_NonNull HostI where
  70         fromNullable = liftM  NonNull.fromNullable
  71         toNullable   = liftM  NonNull.toNullable
  72         ncons        = liftM2 NonNull.ncons
  73         nuncons      = liftM  NonNull.nuncons
  74         head         = liftM  NonNull.head
  75         last         = liftM  NonNull.last
  76         tail         = liftM  NonNull.tail
  77         init         = liftM  NonNull.init
  78         nfilter      = liftM2 NonNull.nfilter
  79 instance Sym_NonNull TextI where
  80         fromNullable = textI1 "fromNullable"
  81         toNullable   = textI1 "toNullable"
  82         ncons        = textI2 "ncons"
  83         nuncons      = textI1 "nuncons"
  84         head         = textI1 "head"
  85         last         = textI1 "last"
  86         tail         = textI1 "tail"
  87         init         = textI1 "init"
  88         nfilter      = textI2 "nfilter"
  89 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
  90         fromNullable = dupI1 (Proxy @Sym_NonNull) fromNullable
  91         toNullable   = dupI1 (Proxy @Sym_NonNull) toNullable
  92         ncons        = dupI2 (Proxy @Sym_NonNull) ncons
  93         nuncons      = dupI1 (Proxy @Sym_NonNull) nuncons
  94         head         = dupI1 (Proxy @Sym_NonNull) head
  95         last         = dupI1 (Proxy @Sym_NonNull) last
  96         tail         = dupI1 (Proxy @Sym_NonNull) tail
  97         init         = dupI1 (Proxy @Sym_NonNull) init
  98         nfilter      = dupI2 (Proxy @Sym_NonNull) nfilter
  99
 100 instance
 101  ( Read_TyNameR TyName cs rs
 102  , Inj_TyConst cs NonNull
 103  ) => Read_TyNameR TyName cs (Proxy NonNull ': rs) where
 104         read_TyNameR _cs (TyName "NonNull") k = k (ty @NonNull)
 105         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
 106 instance Show_TyConst cs => Show_TyConst (Proxy NonNull ': cs) where
 107         show_TyConst TyConstZ{} = "NonNull"
 108         show_TyConst (TyConstS c) = show_TyConst c
 109
 110 instance -- TyFam_MonoElement
 111  ( Proj_TyConst cs NonNull
 112  , Proj_TyFam cs TyFam_MonoElement
 113  ) => Proj_TyFamC cs TyFam_MonoElement NonNull where
 114         proj_TyFamC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
 115          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 116          , Just Refl <- proj_TyConst c (Proxy @NonNull)
 117          = proj_TyFam TyFam_MonoElement (ty_o `TypesS` TypesZ)
 118         proj_TyFamC _c _fam _ty = Nothing
 119 instance -- Proj_TyConC
 120  ( Proj_TyConst cs NonNull
 121  , Proj_TyConsts cs (TyConsts_imported_by NonNull)
 122  , Proj_TyCon cs
 123  ) => Proj_TyConC cs (Proxy NonNull) where
 124         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ o))
 125          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 126          , Just Refl <- proj_TyConst c (Proxy @NonNull)
 127          = case () of
 128                  _ | Just Refl <- proj_TyConst q (Proxy @Eq)
 129                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 130                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable)
 131                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 132                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)
 133                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 134                    | Just Refl <- proj_TyConst q (Proxy @Ord)
 135                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 136                    | Just Refl <- proj_TyConst q (Proxy @SemiSequence)
 137                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 138                    | Just Refl <- proj_TyConst q (Proxy @Show)
 139                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 140                  _ -> Nothing
 141         proj_TyConC _c _q = Nothing
 142 data instance TokenT meta (ts::[*]) (Proxy NonNull)
 143  = Token_Term_NonNull_fromNullable (EToken meta ts)
 144  | Token_Term_NonNull_toNullable   (EToken meta ts)
 145  | Token_Term_NonNull_ncons        (EToken meta ts) (EToken meta ts)
 146  | Token_Term_NonNull_nuncons      (EToken meta ts)
 147  | Token_Term_NonNull_head         (EToken meta ts)
 148  | Token_Term_NonNull_last         (EToken meta ts)
 149  | Token_Term_NonNull_tail         (EToken meta ts)
 150  | Token_Term_NonNull_init         (EToken meta ts)
 151  | Token_Term_NonNull_nfilter      (EToken meta ts) (EToken meta ts)
 152 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy NonNull))
 153 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy NonNull))
 154 instance -- CompileI
 155  ( Inj_TyConst (TyConsts_of_Ifaces is) NonNull
 156  , Inj_TyConst (TyConsts_of_Ifaces is) (->)
 157  , Inj_TyConst (TyConsts_of_Ifaces is) (,)
 158  , Inj_TyConst (TyConsts_of_Ifaces is) Bool
 159  , Inj_TyConst (TyConsts_of_Ifaces is) Maybe
 160  , Inj_TyConst (TyConsts_of_Ifaces is) MonoFoldable
 161  , Inj_TyConst (TyConsts_of_Ifaces is) IsSequence
 162  , Inj_TyConst (TyConsts_of_Ifaces is) SemiSequence
 163  , Proj_TyCon  (TyConsts_of_Ifaces is)
 164  , Proj_TyFam  (TyConsts_of_Ifaces is) TyFam_MonoElement
 165  , Compile is
 166  ) => CompileI is (Proxy NonNull) where
 167         compileI
 168          :: forall meta ctx ret ls rs.
 169          TokenT meta is (Proxy NonNull)
 170          -> CompileT meta ctx ret is ls (Proxy NonNull ': rs)
 171         compileI tok ctx k =
 172                 case tok of
 173                  Token_Term_NonNull_fromNullable tok_o ->
 174                         -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
 175                         compileO tok_o ctx $ \ty_o (TermO o) ->
 176                         check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
 177                         k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ TermO $
 178                          \c -> fromNullable (o c)
 179                  Token_Term_NonNull_toNullable tok_n ->
 180                         -- toNullable :: MonoFoldable o => NonNull o -> o
 181                         compileO tok_n ctx $ \ty_n (TermO n) ->
 182                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 183                         check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
 184                         k ty_o $ TermO $
 185                          \c -> toNullable (n c)
 186                  Token_Term_NonNull_ncons tok_e tok_s ->
 187                         -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
 188                         compileO tok_e ctx $ \ty_e (TermO e) ->
 189                         compileO tok_s ctx $ \ty_s (TermO s) ->
 190                         check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
 191                         check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 192                         check_TyEq (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
 193                         k (ty @NonNull :$ ty_s) $ TermO $
 194                          \c -> ncons (e c) (s c)
 195                  Token_Term_NonNull_nuncons tok_n ->
 196                         -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
 197                         compileO tok_n ctx $ \ty_n (TermO n) ->
 198                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 199                         check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
 200                         check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 201                         check_TyEq
 202                          (At Nothing ty_s_e)
 203                          (At (Just tok_n) ty_s_e) $ \Refl ->
 204                         k (ty @(,) :$ ty_s_e :$ (ty @Maybe :$ (ty @NonNull :$ ty_s))) $ TermO $
 205                          \c -> nuncons (n c)
 206                  Token_Term_NonNull_head tok_n -> n2e_from tok_n head
 207                  Token_Term_NonNull_last tok_n -> n2e_from tok_n last
 208                  Token_Term_NonNull_tail tok_n -> n2s_from tok_n tail
 209                  Token_Term_NonNull_init tok_n -> n2s_from tok_n init
 210                  Token_Term_NonNull_nfilter tok_e2Bool tok_n ->
 211                         -- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
 212                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 213                         compileO tok_n      ctx $ \ty_n      (TermO s) ->
 214                         check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 215                         check_TyEq
 216                          (At Nothing (ty @Bool))
 217                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 218                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 219                         check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
 220                         check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 221                         check_TyEq
 222                          (At Nothing ty_s_e)
 223                          (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
 224                         k ty_s $ TermO $
 225                          \c -> nfilter (e2Bool c) (s c)
 226                 where
 227                 n2e_from tok_n
 228                  (f::forall term o.
 229                          (Sym_NonNull term, MonoFoldable o)
 230                          => term (NonNull o) -> term (MT.Element o)) =
 231                  -- head :: MonoFoldable o => NonNull o -> MT.Element o
 232                  -- last :: MonoFoldable o => NonNull o -> MT.Element o
 233                         compileO tok_n ctx $ \ty_n (TermO n) ->
 234                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 235                         check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
 236                         check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 237                         k ty_o_e $ TermO $
 238                          \c -> f (n c)
 239                 n2s_from tok_n
 240                  (f::forall term s.
 241                          (Sym_NonNull term, IsSequence s)
 242                          => term (NonNull s) -> term s) =
 243                  -- tail :: IsSequence s => NonNull s -> s
 244                  -- init :: IsSequence s => NonNull s -> s
 245                         compileO tok_n ctx $ \ty_n (TermO n) ->
 246                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 247                         check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
 248                         k ty_s $ TermO $
 249                          \c -> f (n c)
 250 instance -- TokenizeT
 251  Inj_Token meta ts NonNull =>
 252  TokenizeT meta ts (Proxy NonNull) where
 253         tokenizeT _t = mempty
 254          { tokenizers_infix = tokenizeTMod []
 255                  [ tokenize1 "fromNullable" infixN5 Token_Term_NonNull_fromNullable
 256                  , tokenize1 "toNullable"   infixN5 Token_Term_NonNull_toNullable
 257                  , tokenize2 "ncons"        infixN5 Token_Term_NonNull_ncons
 258                  , tokenize1 "nuncons"      infixN5 Token_Term_NonNull_nuncons
 259                  , tokenize1 "head"         infixN5 Token_Term_NonNull_head
 260                  , tokenize1 "last"         infixN5 Token_Term_NonNull_last
 261                  , tokenize1 "tail"         infixN5 Token_Term_NonNull_tail
 262                  , tokenize1 "init"         infixN5 Token_Term_NonNull_init
 263                  , tokenize2 "nfilter"      infixN5 Token_Term_NonNull_nfilter
 264                  ]
 265          }
 266 instance Gram_Term_AtomsT meta ts (Proxy NonNull) g