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