Language/Symantic/Compiling/Sequences.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'Sequences'.
   4 module Language.Symantic.Compiling.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.Term
  18 import Language.Symantic.Compiling.MonoFunctor (Fam_MonoElement(..))
  19 import Language.Symantic.Interpreting
  20 import Language.Symantic.Transforming.Trans
  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 Consts_of_Iface (Proxy SemiSequence) = Proxy SemiSequence ': Consts_imported_by SemiSequence
  39 type instance Consts_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 (Proxy @Sym_SemiSequence) intersperse
  57         cons        = dupI2 (Proxy @Sym_SemiSequence) cons
  58         snoc        = dupI2 (Proxy @Sym_SemiSequence) snoc
  59         reverse     = dupI1 (Proxy @Sym_SemiSequence) reverse
  60
  61 instance
  62  ( Read_TypeNameR Text cs rs
  63  , Inj_Const cs SemiSequence
  64  ) => Read_TypeNameR Text cs (Proxy SemiSequence ': rs) where
  65         read_typenameR _cs "SemiSequence" k = k (ty @SemiSequence)
  66         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  67 instance Show_Const cs => Show_Const (Proxy SemiSequence ': cs) where
  68         show_const ConstZ{} = "SemiSequence"
  69         show_const (ConstS c) = show_const c
  70
  71 instance -- Proj_ConC
  72  ( Proj_Const cs SemiSequence
  73  , Proj_Consts cs (Consts_imported_by SemiSequence)
  74  ) => Proj_ConC cs (Proxy SemiSequence) where
  75         proj_conC _ (TyConst q :$ s)
  76          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
  77          , Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
  78          = case s of
  79                  TyConst c
  80                   | Just Refl <- eq_skind (kind_of_const c) SKiType ->
  81                         case () of
  82                          _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
  83                          _ -> Nothing
  84                  TyConst c :$ _o
  85                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
  86                         case () of
  87                          _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
  88                          _ -> Nothing
  89                  _ -> Nothing
  90         proj_conC _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_Const (Consts_of_Ifaces is) SemiSequence
 100  , Proj_Con  (Consts_of_Ifaces is)
 101  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 102  , Compile is
 103  ) => CompileI is (Proxy SemiSequence) where
 104         compileI
 105          :: forall meta ctx ret ls rs.
 106          TokenT meta is (Proxy SemiSequence)
 107          -> CompileT meta ctx ret 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_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
 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_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
 133                         check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 134                         check_type (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
 138 -- * Class 'Sym_IsSequence'
 139 class Sym_IsSequence term where
 140         filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
 141         default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
 142         filter  = trans_map2 filter
 143
 144 type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
 145 type instance Consts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': Consts_imported_by IsSequence
 146 type instance Consts_imported_by IsSequence =
 147  [ Proxy IsSequence
 148  , Proxy (->)
 149  , Proxy []
 150  , Proxy Text
 151  , Proxy Bool
 152  ]
 153
 154 instance Sym_IsSequence HostI where
 155         filter  = liftM2 Seqs.filter
 156 instance Sym_IsSequence TextI where
 157         filter  = textI2 "filter"
 158 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
 159         filter  = dupI2 (Proxy @Sym_IsSequence) filter
 160
 161 instance
 162  ( Read_TypeNameR Text cs rs
 163  , Inj_Const cs IsSequence
 164  ) => Read_TypeNameR Text cs (Proxy IsSequence ': rs) where
 165         read_typenameR _cs "IsSequence" k = k (ty @IsSequence)
 166         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
 167 instance Show_Const cs => Show_Const (Proxy IsSequence ': cs) where
 168         show_const ConstZ{} = "IsSequence"
 169         show_const (ConstS c) = show_const c
 170
 171 instance -- Proj_ConC
 172  ( Proj_Const cs IsSequence
 173  , Proj_Consts cs (Consts_imported_by IsSequence)
 174  ) => Proj_ConC cs (Proxy IsSequence) where
 175         proj_conC _ (TyConst q :$ s)
 176          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 177          , Just Refl <- proj_const q (Proxy::Proxy IsSequence)
 178          = case s of
 179                  TyConst c
 180                   | Just Refl <- eq_skind (kind_of_const c) SKiType ->
 181                         case () of
 182                          _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
 183                          _ -> Nothing
 184                  TyConst c :$ _o
 185                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
 186                         case () of
 187                          _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
 188                          _ -> Nothing
 189                  _ -> Nothing
 190         proj_conC _c _q = Nothing
 191 data instance TokenT meta (ts::[*]) (Proxy IsSequence)
 192  = Token_Term_IsSequence_filter (EToken meta ts) (EToken meta ts)
 193 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IsSequence))
 194 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IsSequence))
 195 instance -- CompileI
 196  ( Inj_Const (Consts_of_Ifaces is) IsSequence
 197  , Inj_Const (Consts_of_Ifaces is) (->)
 198  , Inj_Const (Consts_of_Ifaces is) Bool
 199  , Proj_Con  (Consts_of_Ifaces is)
 200  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 201  , Compile is
 202  ) => CompileI is (Proxy IsSequence) where
 203         compileI
 204          :: forall meta ctx ret ls rs.
 205          TokenT meta is (Proxy IsSequence)
 206          -> CompileT meta ctx ret is ls (Proxy IsSequence ': rs)
 207         compileI tok ctx k =
 208                 case tok of
 209                  Token_Term_IsSequence_filter tok_e2Bool tok_s ->
 210                         -- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
 211                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 212                         compileO tok_s      ctx $ \ty_s      (TermO s) ->
 213                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 214                         check_type
 215                          (At Nothing (ty @Bool))
 216                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 217                         check_con (At (Just tok_s) (ty @IsSequence :$ ty_s)) $ \Con ->
 218                         check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 219                         check_type
 220                          (At Nothing ty_s_e)
 221                          (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
 222                         k ty_s $ TermO $
 223                          \c -> filter (e2Bool c) (s c)