Language/Symantic/Lib/MonoFoldable.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
   4 -- | Symantic for 'MonoFoldable'.
   5 module Language.Symantic.Lib.MonoFoldable where
   6
   7 import Control.Monad (liftM, liftM2, liftM3)
   8 import Data.MonoTraversable (MonoFoldable)
   9 import qualified Data.MonoTraversable as MT
  10 import Data.Proxy
  11 import Data.Text (Text)
  12 import Data.Type.Equality ((:~:)(Refl))
  13
  14 import Language.Symantic.Parsing
  15 import Language.Symantic.Parsing.Grammar
  16 import Language.Symantic.Typing
  17 import Language.Symantic.Compiling
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  20 import Language.Symantic.Lib.MonoFunctor
  21
  22 -- * Class 'Sym_MonoFoldable'
  23 class Sym_MonoFunctor term => Sym_MonoFoldable term where
  24         ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m
  25         ofoldr   :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
  26         ofoldl'  :: MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
  27         olength  :: MonoFoldable o => term o -> term Int
  28         onull    :: MonoFoldable o => term o -> term Bool
  29         oall     :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
  30         oany     :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
  31         otoList  :: MonoFoldable o => term o -> term [MT.Element o]
  32         default ofoldMap :: (Trans t term, MonoFoldable o, Monoid m)
  33          => t term (MT.Element o -> m) -> t term o -> t term m
  34         default ofoldr :: (Trans t term, MonoFoldable o)
  35          => t term (MT.Element o -> b -> b) -> t term b -> t term o -> t term b
  36         default ofoldl' :: (Trans t term, MonoFoldable o)
  37          => t term (b -> MT.Element o -> b) -> t term b -> t term o -> t term b
  38         default olength :: (Trans t term, MonoFoldable o) => t term o -> t term Int
  39         default onull   :: (Trans t term, MonoFoldable o) => t term o -> t term Bool
  40         default oall    :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
  41         default oany    :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
  42         default otoList :: (Trans t term, MonoFoldable o) => t term o -> t term [MT.Element o]
  43         ofoldMap = trans_map2 ofoldMap
  44         ofoldr   = trans_map3 ofoldr
  45         ofoldl'  = trans_map3 ofoldl'
  46         olength  = trans_map1 olength
  47         onull    = trans_map1 onull
  48         oall     = trans_map2 oall
  49         oany     = trans_map2 oany
  50         otoList  = trans_map1 otoList
  51
  52 type instance Sym_of_Iface (Proxy MonoFoldable) = Sym_MonoFoldable
  53 type instance Consts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': Consts_imported_by MonoFoldable
  54 type instance Consts_imported_by MonoFoldable =
  55  [ Proxy (->)
  56  , Proxy (,)
  57  , Proxy []
  58  , Proxy Bool
  59  , Proxy Either
  60  , Proxy Int
  61  , Proxy Maybe
  62  , Proxy Monoid
  63  , Proxy Text
  64  ]
  65
  66 instance Sym_MonoFoldable HostI where
  67         ofoldMap = liftM2 MT.ofoldMap
  68         ofoldr   = liftM3 MT.ofoldr
  69         ofoldl'  = liftM3 MT.ofoldl'
  70         olength  = liftM  MT.olength
  71         onull    = liftM  MT.onull
  72         oall     = liftM2 MT.oall
  73         oany     = liftM2 MT.oany
  74         otoList  = liftM  MT.otoList
  75 instance Sym_MonoFoldable TextI where
  76         ofoldMap = textI2 "ofoldMap"
  77         ofoldr   = textI3 "ofoldr"
  78         ofoldl'  = textI3 "ofoldl'"
  79         olength  = textI1 "olength"
  80         onull    = textI1 "onull"
  81         oall     = textI2 "oall"
  82         oany     = textI2 "oany"
  83         otoList  = textI1 "otoList"
  84 instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (DupI r1 r2) where
  85         ofoldMap = dupI2 (Proxy @Sym_MonoFoldable) ofoldMap
  86         ofoldr   = dupI3 (Proxy @Sym_MonoFoldable) ofoldr
  87         ofoldl'  = dupI3 (Proxy @Sym_MonoFoldable) ofoldl'
  88         olength  = dupI1 (Proxy @Sym_MonoFoldable) olength
  89         onull    = dupI1 (Proxy @Sym_MonoFoldable) onull
  90         oall     = dupI2 (Proxy @Sym_MonoFoldable) oall
  91         oany     = dupI2 (Proxy @Sym_MonoFoldable) oany
  92         otoList  = dupI1 (Proxy @Sym_MonoFoldable) otoList
  93
  94 instance
  95  ( Read_TypeNameR Type_Name cs rs
  96  , Inj_Const cs MonoFoldable
  97  ) => Read_TypeNameR Type_Name cs (Proxy MonoFoldable ': rs) where
  98         read_typenameR _cs (Type_Name "MonoFoldable") k = k (ty @MonoFoldable)
  99         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
 100 instance Show_Const cs => Show_Const (Proxy MonoFoldable ': cs) where
 101         show_const ConstZ{} = "MonoFoldable"
 102         show_const (ConstS c) = show_const c
 103
 104 instance -- Proj_ConC
 105  ( Proj_Const cs MonoFoldable
 106  , Proj_Consts cs (Consts_imported_by MonoFoldable)
 107  ) => Proj_ConC cs (Proxy MonoFoldable) where
 108         proj_conC _ (TyConst q :$ typ)
 109          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 110          , Just Refl <- proj_const q (Proxy @MonoFoldable)
 111          = case typ of
 112                  TyConst c
 113                   | Just Refl <- proj_const c (Proxy @Text) -> Just Con
 114                  TyConst c :$ _a
 115                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 116                   -> case () of
 117                          _ | Just Refl <- proj_const c (Proxy @[])    -> Just Con
 118                            | Just Refl <- proj_const c (Proxy @Maybe) -> Just Con
 119                          _ -> Nothing
 120                  TyConst c :$ _a :$ _b
 121                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 122                   -> case () of
 123                          _ | Just Refl <- proj_const c (Proxy @(,))    -> Just Con
 124                            | Just Refl <- proj_const c (Proxy @Either) -> Just Con
 125                          _ -> Nothing
 126                  _ -> Nothing
 127         proj_conC _c _q = Nothing
 128 data instance TokenT meta (ts::[*]) (Proxy MonoFoldable)
 129  = Token_Term_MonoFoldable_ofoldMap (EToken meta ts) (EToken meta ts)
 130  | Token_Term_MonoFoldable_ofoldr   (EToken meta ts) (EToken meta ts) (EToken meta ts)
 131  | Token_Term_MonoFoldable_ofoldl'  (EToken meta ts) (EToken meta ts) (EToken meta ts)
 132  | Token_Term_MonoFoldable_olength  (EToken meta ts)
 133  | Token_Term_MonoFoldable_onull    (EToken meta ts)
 134  | Token_Term_MonoFoldable_oall     (EToken meta ts) (EToken meta ts)
 135  | Token_Term_MonoFoldable_oany     (EToken meta ts) (EToken meta ts)
 136  | Token_Term_MonoFoldable_otoList  (EToken meta ts)
 137 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFoldable))
 138 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFoldable))
 139 instance -- CompileI
 140  ( Inj_Const (Consts_of_Ifaces is) MonoFoldable
 141  , Inj_Const (Consts_of_Ifaces is) (->)
 142  , Inj_Const (Consts_of_Ifaces is) []
 143  , Inj_Const (Consts_of_Ifaces is) Monoid
 144  , Inj_Const (Consts_of_Ifaces is) Bool
 145  , Inj_Const (Consts_of_Ifaces is) Int
 146  , Proj_Con  (Consts_of_Ifaces is)
 147  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 148  , Compile is
 149  ) => CompileI is (Proxy MonoFoldable) where
 150         compileI
 151          :: forall meta ctx ret ls rs.
 152          TokenT meta is (Proxy MonoFoldable)
 153          -> CompileT meta ctx ret is ls (Proxy MonoFoldable ': rs)
 154         compileI tok ctx k =
 155                 case tok of
 156                  Token_Term_MonoFoldable_ofoldMap tok_f tok_o ->
 157                         -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
 158                         compileO tok_f ctx $ \ty_f (TermO f) ->
 159                         compileO tok_o ctx $ \ty_o (TermO o) ->
 160                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_m ->
 161                         check_con (At (Just tok_f) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 162                         check_con (At (Just tok_f) (ty @Monoid :$ ty_m)) $ \Con ->
 163                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 164                         check_type
 165                          (At Nothing ty_o_e)
 166                          (At (Just tok_f) ty_f_a) $ \Refl ->
 167                         k ty_m $ TermO $
 168                          \c -> ofoldMap (f c) (o c)
 169                  Token_Term_MonoFoldable_ofoldr tok_e2b2b tok_b tok_o ->
 170                         ofoldr_from tok_e2b2b tok_b tok_o ofoldr
 171                  Token_Term_MonoFoldable_ofoldl' tok_b2e2b tok_b tok_o ->
 172                         ofoldl_from tok_b2e2b tok_b tok_o ofoldl'
 173                  Token_Term_MonoFoldable_olength tok_o -> o2ty_from tok_o olength
 174                  Token_Term_MonoFoldable_onull   tok_o -> o2ty_from tok_o onull
 175                  Token_Term_MonoFoldable_oall tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oall
 176                  Token_Term_MonoFoldable_oany tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oany
 177                  Token_Term_MonoFoldable_otoList tok_o ->
 178                  -- otoList :: MonoFoldable o => o -> [MT.Element o]
 179                         compileO tok_o ctx $ \ty_o (TermO o) ->
 180                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 181                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 182                         k (ty @[] :$ ty_o_e) $ TermO $
 183                          \c -> otoList (o c)
 184                 where
 185                 ofoldr_from tok_e2b2b tok_b tok_o
 186                  (fold::forall term o b.
 187                          (Sym_MonoFoldable term, MonoFoldable o)
 188                          => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
 189                  -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
 190                         compileO tok_e2b2b ctx $ \ty_e2b2b (TermO e2b2b) ->
 191                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 192                         compileO tok_o     ctx $ \ty_o     (TermO o) ->
 193                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b) $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
 194                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b_b2b) $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
 195                         check_type
 196                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 197                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
 198                         check_type
 199                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 200                          (At (Just tok_b) ty_b) $ \Refl ->
 201                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 202                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 203                         check_type
 204                          (At (Just tok_e2b2b) ty_e2b2b_e)
 205                          (At (Just tok_o) ty_o_e) $ \Refl ->
 206                         k ty_b $ TermO $
 207                          \c -> fold (e2b2b c) (b c) (o c)
 208                 ofoldl_from tok_b2e2b tok_b tok_o
 209                  (fold::forall term o b.
 210                          (Sym_MonoFoldable term, MonoFoldable o)
 211                          => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
 212                         -- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
 213                         compileO tok_b2e2b ctx $ \ty_b2e2b (TermO b2e2b) ->
 214                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 215                         compileO tok_o     ctx $ \ty_o     (TermO o) ->
 216                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b) $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
 217                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b_a2b) $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
 218                         check_type
 219                          (At (Just tok_b2e2b) ty_b2e2b_b)
 220                          (At (Just tok_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
 221                         check_type
 222                          (At (Just tok_b2e2b) ty_b2e2b_b)
 223                          (At (Just tok_b) ty_b) $ \Refl ->
 224                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 225                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 226                         check_type
 227                          (At (Just tok_b2e2b) ty_b2e2b_a2b_e)
 228                          (At (Just tok_o) ty_o_e) $ \Refl ->
 229                         k ty_b $ TermO $
 230                          \c -> fold (b2e2b c) (b c) (o c)
 231                 o2ty_from
 232                  :: forall typ. Inj_Const (Consts_of_Ifaces is) typ
 233                  => EToken meta is
 234                  -> (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term typ)
 235                  -> Either (Error_Term meta is) ret
 236                 o2ty_from tok_o f =
 237                         -- olength :: MonoFoldable o => o -> Int
 238                         -- onull   :: MonoFoldable o => o -> Bool
 239                         compileO tok_o ctx $ \ty_o (TermO o) ->
 240                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 241                         k (TyConst inj_const::Type (Consts_of_Ifaces is) typ) $ TermO $
 242                          \c -> f (o c)
 243                 oalloany_from
 244                  tok_e2Bool tok_o
 245                  (g::forall term o.
 246                          (Sym_MonoFoldable term, MonoFoldable o)
 247                          => term (MT.Element o -> Bool) -> term o -> term Bool) =
 248                  -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 249                  -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 250                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 251                         compileO tok_o ctx $ \ty_o (TermO o) ->
 252                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 253                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 254                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 255                         check_type
 256                          (At (Just tok_e2Bool) ty_e2Bool_e)
 257                          (At (Just tok_o) ty_o_e) $ \Refl ->
 258                         check_type
 259                          (At Nothing (ty @Bool))
 260                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 261                         k (ty @Bool) $ TermO $
 262                          \c -> g (e2Bool c) (o c)
 263 instance -- TokenizeT
 264  Inj_Token meta ts MonoFoldable =>
 265  TokenizeT meta ts (Proxy MonoFoldable) where
 266         tokenizeT _t = mempty
 267          { tokenizers_infix = tokenizeTMod []
 268                  [ tokenize2 "ofoldMap" infixN5 Token_Term_MonoFoldable_ofoldMap
 269                  , tokenize3 "ofoldr"   infixN5 Token_Term_MonoFoldable_ofoldr
 270                  , tokenize3 "ofoldl'"  infixN5 Token_Term_MonoFoldable_ofoldl'
 271                  , tokenize1 "olength"  infixN5 Token_Term_MonoFoldable_olength
 272                  , tokenize1 "onull"    infixN5 Token_Term_MonoFoldable_onull
 273                  , tokenize2 "oall"     infixN5 Token_Term_MonoFoldable_oall
 274                  , tokenize2 "oany"     infixN5 Token_Term_MonoFoldable_oany
 275                  , tokenize1 "otoList"  infixN5 Token_Term_MonoFoldable_otoList
 276                  ]
 277          }
 278 instance Gram_Term_AtomsT meta ts (Proxy MonoFoldable) g