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