Language/Symantic/Compiling/NonNull.hs

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