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