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

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