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 Data.NonNull (NonNull)
  10 import Data.Proxy
  11 import Data.Sequences (IsSequence, SemiSequence)
  12 import Data.Type.Equality ((:~:)(Refl))
  13 import Prelude hiding (head, init, last, tail)
  14 import qualified Data.MonoTraversable as MT
  15 import qualified Data.NonNull as NonNull
  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 (TyFam_MonoElement(..))
  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 (Proxy NonNull)
  56 type instance TyConsts_imported_by (Proxy 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 @Sym_NonNull fromNullable
  91         toNullable   = dupI1 @Sym_NonNull toNullable
  92         ncons        = dupI2 @Sym_NonNull ncons
  93         nuncons      = dupI1 @Sym_NonNull nuncons
  94         head         = dupI1 @Sym_NonNull head
  95         last         = dupI1 @Sym_NonNull last
  96         tail         = dupI1 @Sym_NonNull tail
  97         init         = dupI1 @Sym_NonNull init
  98         nfilter      = dupI2 @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 -- Proj_TyFamC 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
 120 instance -- Proj_TyConC
 121  ( Proj_TyConst cs NonNull
 122  , Proj_TyConsts cs (TyConsts_imported_by (Proxy NonNull))
 123  , Proj_TyCon cs
 124  ) => Proj_TyConC cs (Proxy NonNull) where
 125         proj_TyConC _ (t@(TyConst q) :$ (TyConst c :$ o))
 126          | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 127          , Just Refl <- proj_TyConst c (Proxy @NonNull)
 128          = case () of
 129                  _ | Just Refl <- proj_TyConst q (Proxy @Eq)
 130                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 131                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFoldable)
 132                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 133                    | Just Refl <- proj_TyConst q (Proxy @MT.MonoFunctor)
 134                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 135                    | Just Refl <- proj_TyConst q (Proxy @Ord)
 136                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 137                    | Just Refl <- proj_TyConst q (Proxy @SemiSequence)
 138                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 139                    | Just Refl <- proj_TyConst q (Proxy @Show)
 140                    , Just TyCon  <- proj_TyCon (t :$ o) -> Just TyCon
 141                  _ -> Nothing
 142         proj_TyConC _c _q = Nothing
 143 data instance TokenT meta (ts::[*]) (Proxy NonNull)
 144  = Token_Term_NonNull_fromNullable (EToken meta ts)
 145  | Token_Term_NonNull_toNullable   (EToken meta ts)
 146  | Token_Term_NonNull_ncons        (EToken meta ts) (EToken meta ts)
 147  | Token_Term_NonNull_nuncons      (EToken meta ts)
 148  | Token_Term_NonNull_head         (EToken meta ts)
 149  | Token_Term_NonNull_last         (EToken meta ts)
 150  | Token_Term_NonNull_tail         (EToken meta ts)
 151  | Token_Term_NonNull_init         (EToken meta ts)
 152  | Token_Term_NonNull_nfilter      (EToken meta ts) (EToken meta ts)
 153 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy NonNull))
 154 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy NonNull))
 155
 156 instance -- CompileI
 157  ( Inj_TyConst cs NonNull
 158  , Inj_TyConst cs (->)
 159  , Inj_TyConst cs (,)
 160  , Inj_TyConst cs Bool
 161  , Inj_TyConst cs Maybe
 162  , Inj_TyConst cs MonoFoldable
 163  , Inj_TyConst cs IsSequence
 164  , Inj_TyConst cs SemiSequence
 165  , Proj_TyCon  cs
 166  , Proj_TyFam  cs TyFam_MonoElement
 167  , Compile cs is
 168  ) => CompileI cs is (Proxy NonNull) where
 169         compileI
 170          :: forall meta ctx ret ls rs.
 171          TokenT meta is (Proxy NonNull)
 172          -> CompileT meta ctx ret cs is ls (Proxy NonNull ': rs)
 173         compileI tok ctx k =
 174                 case tok of
 175                  Token_Term_NonNull_fromNullable tok_o ->
 176                         -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
 177                         compileO tok_o ctx $ \ty_o (TermO o) ->
 178                         check_TyCon (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
 179                         k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ TermO $
 180                          \c -> fromNullable (o c)
 181                  Token_Term_NonNull_toNullable tok_n ->
 182                         -- toNullable :: MonoFoldable o => NonNull o -> o
 183                         compileO tok_n ctx $ \ty_n (TermO n) ->
 184                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 185                         check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
 186                         k ty_o $ TermO $
 187                          \c -> toNullable (n c)
 188                  Token_Term_NonNull_ncons tok_e tok_s ->
 189                         -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
 190                         compileO tok_e ctx $ \ty_e (TermO e) ->
 191                         compileO tok_s ctx $ \ty_s (TermO s) ->
 192                         check_TyCon (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \TyCon ->
 193                         check_TyFam (At (Just tok_s) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 194                         check_TyEq (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
 195                         k (ty @NonNull :$ ty_s) $ TermO $
 196                          \c -> ncons (e c) (s c)
 197                  Token_Term_NonNull_nuncons tok_n ->
 198                         -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
 199                         compileO tok_n ctx $ \ty_n (TermO n) ->
 200                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 201                         check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
 202                         check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 203                         check_TyEq
 204                          (At Nothing ty_s_e)
 205                          (At (Just tok_n) ty_s_e) $ \Refl ->
 206                         k (ty @(,) :$ ty_s_e :$ (ty @Maybe :$ (ty @NonNull :$ ty_s))) $ TermO $
 207                          \c -> nuncons (n c)
 208                  Token_Term_NonNull_head tok_n -> n2e_from tok_n head
 209                  Token_Term_NonNull_last tok_n -> n2e_from tok_n last
 210                  Token_Term_NonNull_tail tok_n -> n2s_from tok_n tail
 211                  Token_Term_NonNull_init tok_n -> n2s_from tok_n init
 212                  Token_Term_NonNull_nfilter tok_e2Bool tok_n ->
 213                         -- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
 214                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 215                         compileO tok_n      ctx $ \ty_n      (TermO s) ->
 216                         check_TyEq2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 217                         check_TyEq
 218                          (At Nothing (ty @Bool))
 219                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 220                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 221                         check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
 222                         check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 223                         check_TyEq
 224                          (At Nothing ty_s_e)
 225                          (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
 226                         k ty_s $ TermO $
 227                          \c -> nfilter (e2Bool c) (s c)
 228                 where
 229                 n2e_from tok_n
 230                  (f::forall term o.
 231                          (Sym_NonNull term, MonoFoldable o)
 232                          => term (NonNull o) -> term (MT.Element o)) =
 233                  -- head :: MonoFoldable o => NonNull o -> MT.Element o
 234                  -- last :: MonoFoldable o => NonNull o -> MT.Element o
 235                         compileO tok_n ctx $ \ty_n (TermO n) ->
 236                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 237                         check_TyCon (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \TyCon ->
 238                         check_TyFam (At (Just tok_n) TyFam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 239                         k ty_o_e $ TermO $
 240                          \c -> f (n c)
 241                 n2s_from tok_n
 242                  (f::forall term s.
 243                          (Sym_NonNull term, IsSequence s)
 244                          => term (NonNull s) -> term s) =
 245                  -- tail :: IsSequence s => NonNull s -> s
 246                  -- init :: IsSequence s => NonNull s -> s
 247                         compileO tok_n ctx $ \ty_n (TermO n) ->
 248                         check_TyEq1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 249                         check_TyCon (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \TyCon ->
 250                         k ty_s $ TermO $
 251                          \c -> f (n c)
 252 instance -- TokenizeT
 253  Inj_Token meta ts NonNull =>
 254  TokenizeT meta ts (Proxy NonNull) where
 255         tokenizeT _t = mempty
 256          { tokenizers_infix = tokenizeTMod []
 257                  [ tokenize1 "fromNullable" infixN5 Token_Term_NonNull_fromNullable
 258                  , tokenize1 "toNullable"   infixN5 Token_Term_NonNull_toNullable
 259                  , tokenize2 "ncons"        infixN5 Token_Term_NonNull_ncons
 260                  , tokenize1 "nuncons"      infixN5 Token_Term_NonNull_nuncons
 261                  , tokenize1 "head"         infixN5 Token_Term_NonNull_head
 262                  , tokenize1 "last"         infixN5 Token_Term_NonNull_last
 263                  , tokenize1 "tail"         infixN5 Token_Term_NonNull_tail
 264                  , tokenize1 "init"         infixN5 Token_Term_NonNull_init
 265                  , tokenize2 "nfilter"      infixN5 Token_Term_NonNull_nfilter
 266                  ]
 267          }
 268 instance Gram_Term_AtomsT meta ts (Proxy NonNull) g