Language/Symantic/Compiling/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.Compiling.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.Text (Text)
  15 import Data.Type.Equality ((:~:)(Refl))
  16 import Prelude hiding (head, init, last, tail)
  17
  18 import Language.Symantic.Parsing
  19 import Language.Symantic.Typing
  20 import Language.Symantic.Compiling.Term
  21 import Language.Symantic.Compiling.MonoFunctor
  22 import Language.Symantic.Interpreting
  23 import Language.Symantic.Transforming.Trans
  24
  25 -- * Class 'Sym_NonNull'
  26 class Sym_NonNull term where
  27         fromNullable :: MonoFoldable o => term o -> term (Maybe (NonNull o))
  28         toNullable :: MonoFoldable o => term (NonNull o) -> term o
  29         ncons :: SemiSequence s => term (MT.Element s) -> term s -> term (NonNull s)
  30         nuncons :: IsSequence s => term (NonNull s) -> term (MT.Element s, Maybe (NonNull s))
  31         head :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  32         last :: MonoFoldable o => term (NonNull o) -> term (MT.Element o)
  33         tail :: IsSequence s => term (NonNull s) -> term s
  34         init :: IsSequence s => term (NonNull s) -> term s
  35         nfilter :: IsSequence s => term (MT.Element s -> Bool) -> term (NonNull s) -> term s
  36         default fromNullable :: (Trans t term, MonoFoldable o) => t term o -> t term (Maybe (NonNull o))
  37         default toNullable :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term o
  38         default ncons :: (Trans t term, SemiSequence s) => t term (MT.Element s) -> t term s -> t term (NonNull s)
  39         default nuncons :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term (MT.Element s, Maybe (NonNull s))
  40         default head :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
  41         default last :: (Trans t term, MonoFoldable o) => t term (NonNull o) -> t term (MT.Element o)
  42         default tail :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
  43         default init :: (Trans t term, IsSequence s) => t term (NonNull s) -> t term s
  44         default nfilter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term (NonNull s) -> t term s
  45         fromNullable = trans_map1 fromNullable
  46         toNullable   = trans_map1 toNullable
  47         ncons        = trans_map2 ncons
  48         nuncons      = trans_map1 nuncons
  49         head         = trans_map1 head
  50         last         = trans_map1 last
  51         tail         = trans_map1 tail
  52         init         = trans_map1 init
  53         nfilter      = trans_map2 nfilter
  54
  55 type instance Sym_of_Iface (Proxy NonNull) = Sym_NonNull
  56 type instance Consts_of_Iface (Proxy NonNull) = Proxy NonNull ': Consts_imported_by NonNull
  57 type instance Consts_imported_by NonNull =
  58  [ Proxy (->)
  59  , Proxy (,)
  60  , Proxy Eq
  61  , Proxy Maybe
  62  , Proxy Ord
  63  , Proxy MT.MonoFoldable
  64  , Proxy MT.MonoFunctor
  65  , Proxy IsSequence
  66  , Proxy SemiSequence
  67  , Proxy Show
  68  ]
  69
  70 instance Sym_NonNull HostI where
  71         fromNullable = liftM  NonNull.fromNullable
  72         toNullable   = liftM  NonNull.toNullable
  73         ncons        = liftM2 NonNull.ncons
  74         nuncons      = liftM  NonNull.nuncons
  75         head         = liftM  NonNull.head
  76         last         = liftM  NonNull.last
  77         tail         = liftM  NonNull.tail
  78         init         = liftM  NonNull.init
  79         nfilter      = liftM2 NonNull.nfilter
  80 instance Sym_NonNull TextI where
  81         fromNullable = textI1 "fromNullable"
  82         toNullable   = textI1 "toNullable"
  83         ncons        = textI2 "ncons"
  84         nuncons      = textI1 "nuncons"
  85         head         = textI1 "head"
  86         last         = textI1 "last"
  87         tail         = textI1 "tail"
  88         init         = textI1 "init"
  89         nfilter      = textI2 "nfilter"
  90 instance (Sym_NonNull r1, Sym_NonNull r2) => Sym_NonNull (DupI r1 r2) where
  91         fromNullable = dupI1 (Proxy @Sym_NonNull) fromNullable
  92         toNullable   = dupI1 (Proxy @Sym_NonNull) toNullable
  93         ncons        = dupI2 (Proxy @Sym_NonNull) ncons
  94         nuncons      = dupI1 (Proxy @Sym_NonNull) nuncons
  95         head         = dupI1 (Proxy @Sym_NonNull) head
  96         last         = dupI1 (Proxy @Sym_NonNull) last
  97         tail         = dupI1 (Proxy @Sym_NonNull) tail
  98         init         = dupI1 (Proxy @Sym_NonNull) init
  99         nfilter      = dupI2 (Proxy @Sym_NonNull) nfilter
 100
 101 instance
 102  ( Read_TypeNameR Text cs rs
 103  , Inj_Const cs NonNull
 104  ) => Read_TypeNameR Text cs (Proxy NonNull ': rs) where
 105         read_typenameR _cs "NonNull" k = k (ty @NonNull)
 106         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
 107 instance Show_Const cs => Show_Const (Proxy NonNull ': cs) where
 108         show_const ConstZ{} = "NonNull"
 109         show_const (ConstS c) = show_const c
 110
 111 instance -- Fam_MonoElement
 112  ( Proj_Const cs NonNull
 113  , Proj_Fam cs Fam_MonoElement
 114  ) => Proj_FamC cs Fam_MonoElement NonNull where
 115         proj_famC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
 116          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 117          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
 118          = proj_fam Fam_MonoElement (ty_o `TypesS` TypesZ)
 119         proj_famC _c _fam _ty = Nothing
 120 instance -- Proj_ConC
 121  ( Proj_Const cs NonNull
 122  , Proj_Consts cs (Consts_imported_by NonNull)
 123  , Proj_Con cs
 124  ) => Proj_ConC cs (Proxy NonNull) where
 125         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ o))
 126          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 127          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
 128          = case () of
 129                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 130                    , Just Con  <- proj_con (t :$ o) -> Just Con
 131                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFoldable)
 132                    , Just Con  <- proj_con (t :$ o) -> Just Con
 133                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFunctor)
 134                    , Just Con  <- proj_con (t :$ o) -> Just Con
 135                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 136                    , Just Con  <- proj_con (t :$ o) -> Just Con
 137                    | Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
 138                    , Just Con  <- proj_con (t :$ o) -> Just Con
 139                    | Just Refl <- proj_const q (Proxy::Proxy Show)
 140                    , Just Con  <- proj_con (t :$ o) -> Just Con
 141                  _ -> Nothing
 142         proj_conC _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 instance -- CompileI
 156  ( Inj_Const (Consts_of_Ifaces is) NonNull
 157  , Inj_Const (Consts_of_Ifaces is) (->)
 158  , Inj_Const (Consts_of_Ifaces is) (,)
 159  , Inj_Const (Consts_of_Ifaces is) Bool
 160  , Inj_Const (Consts_of_Ifaces is) Maybe
 161  , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 162  , Inj_Const (Consts_of_Ifaces is) IsSequence
 163  , Inj_Const (Consts_of_Ifaces is) SemiSequence
 164  , Proj_Con  (Consts_of_Ifaces is)
 165  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 166  , Compile is
 167  ) => CompileI is (Proxy NonNull) where
 168         compileI
 169          :: forall meta ctx ret ls rs.
 170          TokenT meta is (Proxy NonNull)
 171          -> CompileT meta ctx ret is ls (Proxy NonNull ': rs)
 172         compileI tok ctx k =
 173                 case tok of
 174                  Token_Term_NonNull_fromNullable tok_o ->
 175                         -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
 176                         compileO tok_o ctx $ \ty_o (TermO o) ->
 177                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 178                         k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ TermO $
 179                          \c -> fromNullable (o c)
 180                  Token_Term_NonNull_toNullable tok_n ->
 181                         -- toNullable :: MonoFoldable o => NonNull o -> o
 182                         compileO tok_n ctx $ \ty_n (TermO n) ->
 183                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 184                         check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 185                         k ty_o $ TermO $
 186                          \c -> toNullable (n c)
 187                  Token_Term_NonNull_ncons tok_e tok_s ->
 188                         -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
 189                         compileO tok_e ctx $ \ty_e (TermO e) ->
 190                         compileO tok_s ctx $ \ty_s (TermO s) ->
 191                         check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
 192                         check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 193                         check_type (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
 194                         k (ty @NonNull :$ ty_s) $ TermO $
 195                          \c -> ncons (e c) (s c)
 196                  Token_Term_NonNull_nuncons tok_n ->
 197                         -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
 198                         compileO tok_n ctx $ \ty_n (TermO n) ->
 199                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 200                         check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
 201                         check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 202                         check_type
 203                          (At Nothing ty_s_e)
 204                          (At (Just tok_n) ty_s_e) $ \Refl ->
 205                         k (ty @(,) :$ ty_s_e :$ (ty @Maybe :$ (ty @NonNull :$ ty_s))) $ TermO $
 206                          \c -> nuncons (n c)
 207                  Token_Term_NonNull_head tok_n -> n2e_from tok_n head
 208                  Token_Term_NonNull_last tok_n -> n2e_from tok_n last
 209                  Token_Term_NonNull_tail tok_n -> n2s_from tok_n tail
 210                  Token_Term_NonNull_init tok_n -> n2s_from tok_n init
 211                  Token_Term_NonNull_nfilter tok_e2Bool tok_n ->
 212                         -- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
 213                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 214                         compileO tok_n      ctx $ \ty_n      (TermO s) ->
 215                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 216                         check_type
 217                          (At Nothing (ty @Bool))
 218                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 219                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 220                         check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
 221                         check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 222                         check_type
 223                          (At Nothing ty_s_e)
 224                          (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
 225                         k ty_s $ TermO $
 226                          \c -> nfilter (e2Bool c) (s c)
 227                 where
 228                 n2e_from tok_n
 229                  (f::forall term o.
 230                          (Sym_NonNull term, MonoFoldable o)
 231                          => term (NonNull o) -> term (MT.Element o)) =
 232                  -- head :: MonoFoldable o => NonNull o -> MT.Element o
 233                  -- last :: MonoFoldable o => NonNull o -> MT.Element o
 234                         compileO tok_n ctx $ \ty_n (TermO n) ->
 235                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 236                         check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 237                         check_fam (At (Just tok_n) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 238                         k ty_o_e $ TermO $
 239                          \c -> f (n c)
 240                 n2s_from tok_n
 241                  (f::forall term s.
 242                          (Sym_NonNull term, IsSequence s)
 243                          => term (NonNull s) -> term s) =
 244                  -- tail :: IsSequence s => NonNull s -> s
 245                  -- init :: IsSequence s => NonNull s -> s
 246                         compileO tok_n ctx $ \ty_n (TermO n) ->
 247                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 248                         check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
 249                         k ty_s $ TermO $
 250                          \c -> f (n c)
 251                 {-
 252                  "ncons"        -> ncons_from
 253                  "nuncons"      -> nuncons_from
 254                  "head"         -> n2e_from head
 255                  "last"         -> n2e_from last
 256                  "tail"         -> n2s_from tail
 257                  "init"         -> n2s_from init
 258                  "nfilter"      -> nfilter_from
 259                  _ -> Left $ Error_Term_unsupported
 260                 where
 261                 fromNullable_from =
 262                 toNullable_from =
 263                 ncons_from =
 264                 nuncons_from =
 265                 nfilter_from =
 266                 -}