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 = textI_app1 "fromNullable"
  82         toNullable   = textI_app1 "toNullable"
  83         ncons        = textI_app2 "ncons"
  84         nuncons      = textI_app1 "nuncons"
  85         head         = textI_app1 "head"
  86         last         = textI_app1 "last"
  87         tail         = textI_app1 "tail"
  88         init         = textI_app1 "init"
  89         nfilter      = textI_app2 "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 Const_from Text cs => Const_from Text (Proxy NonNull ': cs) where
 102         const_from "NonNull" k = k (ConstZ kind)
 103         const_from s k = const_from s $ k . ConstS
 104 instance Show_Const cs => Show_Const (Proxy NonNull ': cs) where
 105         show_const ConstZ{} = "NonNull"
 106         show_const (ConstS c) = show_const c
 107
 108 instance -- Fam_MonoElement
 109  ( Proj_Const cs NonNull
 110  , Proj_Fam cs Fam_MonoElement
 111  ) => Proj_FamC cs Fam_MonoElement NonNull where
 112         proj_famC _c _fam ((TyConst c :$ ty_o) `TypesS` TypesZ)
 113          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 114          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
 115          = proj_fam Fam_MonoElement (ty_o `TypesS` TypesZ)
 116         proj_famC _c _fam _ty = Nothing
 117 instance -- Proj_ConC
 118  ( Proj_Const cs NonNull
 119  , Proj_Consts cs (Consts_imported_by NonNull)
 120  , Proj_Con cs
 121  ) => Proj_ConC cs (Proxy NonNull) where
 122         proj_conC _ (t@(TyConst q) :$ (TyConst c :$ o))
 123          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 124          , Just Refl <- proj_const c (Proxy::Proxy NonNull)
 125          = case () of
 126                  _ | Just Refl <- proj_const q (Proxy::Proxy Eq)
 127                    , Just Con  <- proj_con (t :$ o) -> Just Con
 128                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFoldable)
 129                    , Just Con  <- proj_con (t :$ o) -> Just Con
 130                    | Just Refl <- proj_const q (Proxy::Proxy MT.MonoFunctor)
 131                    , Just Con  <- proj_con (t :$ o) -> Just Con
 132                    | Just Refl <- proj_const q (Proxy::Proxy Ord)
 133                    , Just Con  <- proj_con (t :$ o) -> Just Con
 134                    | Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
 135                    , Just Con  <- proj_con (t :$ o) -> Just Con
 136                    | Just Refl <- proj_const q (Proxy::Proxy Show)
 137                    , Just Con  <- proj_con (t :$ o) -> Just Con
 138                  _ -> Nothing
 139         proj_conC _c _q = Nothing
 140 data instance TokenT meta (ts::[*]) (Proxy NonNull)
 141  = Token_Term_NonNull_fromNullable (EToken meta ts)
 142  | Token_Term_NonNull_toNullable   (EToken meta ts)
 143  | Token_Term_NonNull_ncons        (EToken meta ts) (EToken meta ts)
 144  | Token_Term_NonNull_nuncons      (EToken meta ts)
 145  | Token_Term_NonNull_head         (EToken meta ts)
 146  | Token_Term_NonNull_last         (EToken meta ts)
 147  | Token_Term_NonNull_tail         (EToken meta ts)
 148  | Token_Term_NonNull_init         (EToken meta ts)
 149  | Token_Term_NonNull_nfilter      (EToken meta ts) (EToken meta ts)
 150 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy NonNull))
 151 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy NonNull))
 152 instance -- Term_fromI
 153  ( Inj_Const (Consts_of_Ifaces is) NonNull
 154  , Inj_Const (Consts_of_Ifaces is) (->)
 155  , Inj_Const (Consts_of_Ifaces is) (,)
 156  , Inj_Const (Consts_of_Ifaces is) Bool
 157  , Inj_Const (Consts_of_Ifaces is) Maybe
 158  , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 159  , Inj_Const (Consts_of_Ifaces is) IsSequence
 160  , Inj_Const (Consts_of_Ifaces is) SemiSequence
 161  , Proj_Con  (Consts_of_Ifaces is)
 162  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 163  , Term_from is
 164  ) => Term_fromI is (Proxy NonNull) where
 165         term_fromI
 166          :: forall meta ctx ret ls rs.
 167          TokenT meta is (Proxy NonNull)
 168          -> Term_fromT meta ctx ret is ls (Proxy NonNull ': rs)
 169         term_fromI tok ctx k =
 170                 case tok of
 171                  Token_Term_NonNull_fromNullable tok_o ->
 172                         -- fromNullable :: MonoFoldable o => o -> Maybe (NonNull o)
 173                         term_from tok_o ctx $ \ty_o (TermLC o) ->
 174                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 175                         k (ty @Maybe :$ (ty @NonNull :$ ty_o)) $ TermLC $
 176                          \c -> fromNullable (o c)
 177                  Token_Term_NonNull_toNullable tok_n ->
 178                         -- toNullable :: MonoFoldable o => NonNull o -> o
 179                         term_from tok_n ctx $ \ty_n (TermLC n) ->
 180                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 181                         check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 182                         k ty_o $ TermLC $
 183                          \c -> toNullable (n c)
 184                  Token_Term_NonNull_ncons tok_e tok_s ->
 185                         -- ncons :: SemiSequence s => MT.Element s -> s -> NonNull s
 186                         term_from tok_e ctx $ \ty_e (TermLC e) ->
 187                         term_from tok_s ctx $ \ty_s (TermLC s) ->
 188                         check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
 189                         check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 190                         check_type (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
 191                         k (ty @NonNull :$ ty_s) $ TermLC $
 192                          \c -> ncons (e c) (s c)
 193                  Token_Term_NonNull_nuncons tok_n ->
 194                         -- nuncons :: IsSequence s => NonNull s -> (MT.Element s, Maybe (NonNull s))
 195                         term_from tok_n ctx $ \ty_n (TermLC n) ->
 196                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 197                         check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
 198                         check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 199                         check_type
 200                          (At Nothing ty_s_e)
 201                          (At (Just tok_n) ty_s_e) $ \Refl ->
 202                         k (ty @(,) :$ ty_s_e :$ (ty @Maybe :$ (ty @NonNull :$ ty_s))) $ TermLC $
 203                          \c -> nuncons (n c)
 204                  Token_Term_NonNull_head tok_n -> n2e_from tok_n head
 205                  Token_Term_NonNull_last tok_n -> n2e_from tok_n last
 206                  Token_Term_NonNull_tail tok_n -> n2s_from tok_n tail
 207                  Token_Term_NonNull_init tok_n -> n2s_from tok_n init
 208                  Token_Term_NonNull_nfilter tok_e2Bool tok_n ->
 209                         -- filter :: IsSequence s => (MT.Element s -> Bool) -> NonNull s -> s
 210                         term_from tok_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
 211                         term_from tok_n      ctx $ \ty_n      (TermLC s) ->
 212                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 213                         check_type
 214                          (At Nothing (ty @Bool))
 215                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 216                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 217                         check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
 218                         check_fam (At (Just tok_n) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 219                         check_type
 220                          (At Nothing ty_s_e)
 221                          (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
 222                         k ty_s $ TermLC $
 223                          \c -> nfilter (e2Bool c) (s c)
 224                 where
 225                 n2e_from tok_n
 226                  (f::forall term o.
 227                          (Sym_NonNull term, MonoFoldable o)
 228                          => term (NonNull o) -> term (MT.Element o)) =
 229                  -- head :: MonoFoldable o => NonNull o -> MT.Element o
 230                  -- last :: MonoFoldable o => NonNull o -> MT.Element o
 231                         term_from tok_n ctx $ \ty_n (TermLC n) ->
 232                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_o ->
 233                         check_con (At (Just tok_n) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 234                         check_fam (At (Just tok_n) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 235                         k ty_o_e $ TermLC $
 236                          \c -> f (n c)
 237                 n2s_from tok_n
 238                  (f::forall term s.
 239                          (Sym_NonNull term, IsSequence s)
 240                          => term (NonNull s) -> term s) =
 241                  -- tail :: IsSequence s => NonNull s -> s
 242                  -- init :: IsSequence s => NonNull s -> s
 243                         term_from tok_n ctx $ \ty_n (TermLC n) ->
 244                         check_type1 (ty @NonNull) (At (Just tok_n) ty_n) $ \Refl ty_s ->
 245                         check_con (At (Just tok_n) (ty @IsSequence :$ ty_s)) $ \Con ->
 246                         k ty_s $ TermLC $
 247                          \c -> f (n c)
 248                 {-
 249                  "ncons"        -> ncons_from
 250                  "nuncons"      -> nuncons_from
 251                  "head"         -> n2e_from head
 252                  "last"         -> n2e_from last
 253                  "tail"         -> n2s_from tail
 254                  "init"         -> n2s_from init
 255                  "nfilter"      -> nfilter_from
 256                  _ -> Left $ Error_Term_unsupported
 257                 where
 258                 fromNullable_from =
 259                 toNullable_from =
 260                 ncons_from =
 261                 nuncons_from =
 262                 nfilter_from =
 263                 -}