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 = textI_app2 "intersperse"
  52         cons        = textI_app2 "cons"
  53         snoc        = textI_app2 "snoc"
  54         reverse     = textI_app1 "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 Const_from Text cs => Const_from Text (Proxy SemiSequence ': cs) where
  62         const_from "SemiSequence" k = k (ConstZ kind)
  63         const_from s k = const_from s $ k . ConstS
  64 instance Show_Const cs => Show_Const (Proxy SemiSequence ': cs) where
  65         show_const ConstZ{} = "SemiSequence"
  66         show_const (ConstS c) = show_const c
  67
  68 instance -- Proj_ConC
  69  ( Proj_Const cs SemiSequence
  70  , Proj_Consts cs (Consts_imported_by SemiSequence)
  71  ) => Proj_ConC cs (Proxy SemiSequence) where
  72         proj_conC _ (TyConst q :$ s)
  73          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
  74          , Just Refl <- proj_const q (Proxy::Proxy SemiSequence)
  75          = case s of
  76                  TyConst c
  77                   | Just Refl <- eq_skind (kind_of_const c) SKiType ->
  78                         case () of
  79                          _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
  80                          _ -> Nothing
  81                  TyConst c :$ _o
  82                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
  83                         case () of
  84                          _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
  85                          _ -> Nothing
  86                  _ -> Nothing
  87         proj_conC _c _q = Nothing
  88 data instance TokenT meta (ts::[*]) (Proxy SemiSequence)
  89  = Token_Term_SemiSequence_intersperse (EToken meta ts) (EToken meta ts)
  90  | Token_Term_SemiSequence_cons        (EToken meta ts) (EToken meta ts)
  91  | Token_Term_SemiSequence_snoc        (EToken meta ts) (EToken meta ts)
  92  | Token_Term_SemiSequence_reverse     (EToken meta ts)
  93 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy SemiSequence))
  94 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy SemiSequence))
  95 instance -- CompileI
  96  ( Inj_Const (Consts_of_Ifaces is) SemiSequence
  97  , Proj_Con  (Consts_of_Ifaces is)
  98  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
  99  , Compile is
 100  ) => CompileI is (Proxy SemiSequence) where
 101         compileI
 102          :: forall meta ctx ret ls rs.
 103          TokenT meta is (Proxy SemiSequence)
 104          -> CompileT meta ctx ret is ls (Proxy SemiSequence ': rs)
 105         compileI tok ctx k =
 106                 case tok of
 107                  Token_Term_SemiSequence_intersperse tok_e tok_s ->
 108                         e2s2s_from tok_e tok_s intersperse
 109                  Token_Term_SemiSequence_cons tok_e tok_s ->
 110                         e2s2s_from tok_e tok_s cons
 111                  Token_Term_SemiSequence_snoc tok_s tok_e ->
 112                         e2s2s_from tok_s tok_e (Prelude.flip snoc)
 113                  Token_Term_SemiSequence_reverse tok_s ->
 114                         -- reverse :: SemiSequence s => s -> s
 115                         compileO tok_s ctx $ \ty_s (TermO s) ->
 116                         check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
 117                         k ty_s $ TermO $
 118                          \c -> reverse (s c)
 119                 where
 120                 e2s2s_from tok_e tok_s
 121                  (f::forall term s.
 122                          (Sym_SemiSequence term, SemiSequence s)
 123                          => term (MT.Element s) -> term s -> term s) =
 124                  -- intersperse :: SemiSequence s => MT.Element s -> s -> s
 125                  -- cons        :: SemiSequence s => MT.Element s -> s -> s
 126                  -- snoc        :: SemiSequence s => s -> MT.Element s -> s
 127                         compileO tok_e ctx $ \ty_e (TermO e) ->
 128                         compileO tok_s ctx $ \ty_s (TermO s) ->
 129                         check_con (At (Just tok_s) (ty @SemiSequence :$ ty_s)) $ \Con ->
 130                         check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 131                         check_type (At Nothing ty_s_e) (At (Just tok_e) ty_e) $ \Refl ->
 132                         k ty_s $ TermO $
 133                          \c -> f (e c) (s c)
 134
 135 -- * Class 'Sym_IsSequence'
 136 class Sym_IsSequence term where
 137         filter :: IsSequence s => term (MT.Element s -> Bool) -> term s -> term s
 138         default filter :: (Trans t term, IsSequence s) => t term (MT.Element s -> Bool) -> t term s -> t term s
 139         filter  = trans_map2 filter
 140
 141 type instance Sym_of_Iface (Proxy IsSequence) = Sym_IsSequence
 142 type instance Consts_of_Iface (Proxy IsSequence) = Proxy IsSequence ': Consts_imported_by IsSequence
 143 type instance Consts_imported_by IsSequence =
 144  [ Proxy IsSequence
 145  , Proxy (->)
 146  , Proxy []
 147  , Proxy Text
 148  , Proxy Bool
 149  ]
 150
 151 instance Sym_IsSequence HostI where
 152         filter  = liftM2 Seqs.filter
 153 instance Sym_IsSequence TextI where
 154         filter  = textI_app2 "filter"
 155 instance (Sym_IsSequence r1, Sym_IsSequence r2) => Sym_IsSequence (DupI r1 r2) where
 156         filter  = dupI2 (Proxy @Sym_IsSequence) filter
 157
 158 instance Const_from Text cs => Const_from Text (Proxy IsSequence ': cs) where
 159         const_from "IsSequence" k = k (ConstZ kind)
 160         const_from s k = const_from s $ k . ConstS
 161 instance Show_Const cs => Show_Const (Proxy IsSequence ': cs) where
 162         show_const ConstZ{} = "IsSequence"
 163         show_const (ConstS c) = show_const c
 164
 165 instance -- Proj_ConC
 166  ( Proj_Const cs IsSequence
 167  , Proj_Consts cs (Consts_imported_by IsSequence)
 168  ) => Proj_ConC cs (Proxy IsSequence) where
 169         proj_conC _ (TyConst q :$ s)
 170          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 171          , Just Refl <- proj_const q (Proxy::Proxy IsSequence)
 172          = case s of
 173                  TyConst c
 174                   | Just Refl <- eq_skind (kind_of_const c) SKiType ->
 175                         case () of
 176                          _ | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
 177                          _ -> Nothing
 178                  TyConst c :$ _o
 179                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) ->
 180                         case () of
 181                          _ | Just Refl <- proj_const c (Proxy::Proxy []) -> Just Con
 182                          _ -> Nothing
 183                  _ -> Nothing
 184         proj_conC _c _q = Nothing
 185 data instance TokenT meta (ts::[*]) (Proxy IsSequence)
 186  = Token_Term_IsSequence_filter (EToken meta ts) (EToken meta ts)
 187 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IsSequence))
 188 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IsSequence))
 189 instance -- CompileI
 190  ( Inj_Const (Consts_of_Ifaces is) IsSequence
 191  , Inj_Const (Consts_of_Ifaces is) (->)
 192  , Inj_Const (Consts_of_Ifaces is) Bool
 193  , Proj_Con  (Consts_of_Ifaces is)
 194  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 195  , Compile is
 196  ) => CompileI is (Proxy IsSequence) where
 197         compileI
 198          :: forall meta ctx ret ls rs.
 199          TokenT meta is (Proxy IsSequence)
 200          -> CompileT meta ctx ret is ls (Proxy IsSequence ': rs)
 201         compileI tok ctx k =
 202                 case tok of
 203                  Token_Term_IsSequence_filter tok_e2Bool tok_s ->
 204                         -- filter :: IsSequence s => (MT.Element s -> Bool) -> s -> s
 205                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 206                         compileO tok_s      ctx $ \ty_s      (TermO s) ->
 207                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 208                         check_type
 209                          (At Nothing (ty @Bool))
 210                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 211                         check_con (At (Just tok_s) (ty @IsSequence :$ ty_s)) $ \Con ->
 212                         check_fam (At (Just tok_s) Fam_MonoElement) (ty_s `TypesS` TypesZ) $ \ty_s_e ->
 213                         check_type
 214                          (At Nothing ty_s_e)
 215                          (At (Just tok_e2Bool) ty_e2Bool_e) $ \Refl ->
 216                         k ty_s $ TermO $
 217                          \c -> filter (e2Bool c) (s c)