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