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