Language/Symantic/Compiling/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.Compiling.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.Term
  17 import Language.Symantic.Compiling.MonoFunctor
  18 import Language.Symantic.Interpreting
  19 import Language.Symantic.Transforming.Trans
  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 Consts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': Consts_imported_by MonoFoldable
  53 type instance Consts_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 (Proxy @Sym_MonoFoldable) ofoldMap
  85         ofoldr   = dupI3 (Proxy @Sym_MonoFoldable) ofoldr
  86         ofoldl'  = dupI3 (Proxy @Sym_MonoFoldable) ofoldl'
  87         olength  = dupI1 (Proxy @Sym_MonoFoldable) olength
  88         onull    = dupI1 (Proxy @Sym_MonoFoldable) onull
  89         oall     = dupI2 (Proxy @Sym_MonoFoldable) oall
  90         oany     = dupI2 (Proxy @Sym_MonoFoldable) oany
  91         otoList  = dupI1 (Proxy @Sym_MonoFoldable) otoList
  92
  93 instance Const_from Text cs => Const_from Text (Proxy MonoFoldable ': cs) where
  94         const_from "MonoFoldable" k = k (ConstZ kind)
  95         const_from s k = const_from s $ k . ConstS
  96 instance Show_Const cs => Show_Const (Proxy MonoFoldable ': cs) where
  97         show_const ConstZ{} = "MonoFoldable"
  98         show_const (ConstS c) = show_const c
  99
 100 instance -- Proj_ConC
 101  ( Proj_Const cs MonoFoldable
 102  , Proj_Consts cs (Consts_imported_by MonoFoldable)
 103  ) => Proj_ConC cs (Proxy MonoFoldable) where
 104         proj_conC _ (TyConst q :$ typ)
 105          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 106          , Just Refl <- proj_const q (Proxy::Proxy MonoFoldable)
 107          = case typ of
 108                  TyConst c
 109                   | Just Refl <- proj_const c (Proxy::Proxy Text) -> Just Con
 110                  TyConst c :$ _a
 111                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 112                   -> case () of
 113                          _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
 114                            | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
 115                          _ -> Nothing
 116                  TyConst c :$ _a :$ _b
 117                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 118                   -> case () of
 119                          _ | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
 120                            | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
 121                          _ -> Nothing
 122                  _ -> Nothing
 123         proj_conC _c _q = Nothing
 124 data instance TokenT meta (ts::[*]) (Proxy MonoFoldable)
 125  = Token_Term_MonoFoldable_ofoldMap (EToken meta ts) (EToken meta ts)
 126  | Token_Term_MonoFoldable_ofoldr   (EToken meta ts) (EToken meta ts) (EToken meta ts)
 127  | Token_Term_MonoFoldable_ofoldl'  (EToken meta ts) (EToken meta ts) (EToken meta ts)
 128  | Token_Term_MonoFoldable_olength  (EToken meta ts)
 129  | Token_Term_MonoFoldable_onull    (EToken meta ts)
 130  | Token_Term_MonoFoldable_oall     (EToken meta ts) (EToken meta ts)
 131  | Token_Term_MonoFoldable_oany     (EToken meta ts) (EToken meta ts)
 132  | Token_Term_MonoFoldable_otoList  (EToken meta ts)
 133 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy MonoFoldable))
 134 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy MonoFoldable))
 135 instance -- CompileI
 136  ( Inj_Const (Consts_of_Ifaces is) MonoFoldable
 137  , Inj_Const (Consts_of_Ifaces is) (->)
 138  , Inj_Const (Consts_of_Ifaces is) []
 139  , Inj_Const (Consts_of_Ifaces is) Monoid
 140  , Inj_Const (Consts_of_Ifaces is) Bool
 141  , Inj_Const (Consts_of_Ifaces is) Int
 142  , Proj_Con  (Consts_of_Ifaces is)
 143  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 144  , Compile is
 145  ) => CompileI is (Proxy MonoFoldable) where
 146         compileI
 147          :: forall meta ctx ret ls rs.
 148          TokenT meta is (Proxy MonoFoldable)
 149          -> CompileT meta ctx ret is ls (Proxy MonoFoldable ': rs)
 150         compileI tok ctx k =
 151                 case tok of
 152                  Token_Term_MonoFoldable_ofoldMap tok_f tok_o ->
 153                         -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
 154                         compileO tok_f ctx $ \ty_f (TermO f) ->
 155                         compileO tok_o ctx $ \ty_o (TermO o) ->
 156                         check_type2 (ty @(->)) (At (Just tok_f) ty_f) $ \Refl ty_f_a ty_m ->
 157                         check_con (At (Just tok_f) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 158                         check_con (At (Just tok_f) (ty @Monoid :$ ty_m)) $ \Con ->
 159                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 160                         check_type
 161                          (At Nothing ty_o_e)
 162                          (At (Just tok_f) ty_f_a) $ \Refl ->
 163                         k ty_m $ TermO $
 164                          \c -> ofoldMap (f c) (o c)
 165                  Token_Term_MonoFoldable_ofoldr tok_e2b2b tok_b tok_o ->
 166                         ofoldr_from tok_e2b2b tok_b tok_o ofoldr
 167                  Token_Term_MonoFoldable_ofoldl' tok_b2e2b tok_b tok_o ->
 168                         ofoldl_from tok_b2e2b tok_b tok_o ofoldl'
 169                  Token_Term_MonoFoldable_olength tok_o -> o2ty_from tok_o olength
 170                  Token_Term_MonoFoldable_onull   tok_o -> o2ty_from tok_o onull
 171                  Token_Term_MonoFoldable_oall tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oall
 172                  Token_Term_MonoFoldable_oany tok_e2Bool tok_o -> oalloany_from tok_e2Bool tok_o oany
 173                  Token_Term_MonoFoldable_otoList tok_o ->
 174                  -- otoList :: MonoFoldable o => o -> [MT.Element o]
 175                         compileO tok_o ctx $ \ty_o (TermO o) ->
 176                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 177                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 178                         k (ty @[] :$ ty_o_e) $ TermO $
 179                          \c -> otoList (o c)
 180                 where
 181                 ofoldr_from tok_e2b2b tok_b tok_o
 182                  (fold::forall term o b.
 183                          (Sym_MonoFoldable term, MonoFoldable o)
 184                          => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
 185                  -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
 186                         compileO tok_e2b2b ctx $ \ty_e2b2b (TermO e2b2b) ->
 187                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 188                         compileO tok_o     ctx $ \ty_o     (TermO o) ->
 189                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b) $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
 190                         check_type2 (ty @(->)) (At (Just tok_e2b2b) ty_e2b2b_b2b) $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
 191                         check_type
 192                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 193                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
 194                         check_type
 195                          (At (Just tok_e2b2b) ty_e2b2b_b2b_b0)
 196                          (At (Just tok_b) ty_b) $ \Refl ->
 197                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 198                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 199                         check_type
 200                          (At (Just tok_e2b2b) ty_e2b2b_e)
 201                          (At (Just tok_o) ty_o_e) $ \Refl ->
 202                         k ty_b $ TermO $
 203                          \c -> fold (e2b2b c) (b c) (o c)
 204                 ofoldl_from tok_b2e2b tok_b tok_o
 205                  (fold::forall term o b.
 206                          (Sym_MonoFoldable term, MonoFoldable o)
 207                          => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
 208                         -- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
 209                         compileO tok_b2e2b ctx $ \ty_b2e2b (TermO b2e2b) ->
 210                         compileO tok_b     ctx $ \ty_b     (TermO b) ->
 211                         compileO tok_o     ctx $ \ty_o     (TermO o) ->
 212                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b) $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
 213                         check_type2 (ty @(->)) (At (Just tok_b2e2b) ty_b2e2b_a2b) $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
 214                         check_type
 215                          (At (Just tok_b2e2b) ty_b2e2b_b)
 216                          (At (Just tok_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
 217                         check_type
 218                          (At (Just tok_b2e2b) ty_b2e2b_b)
 219                          (At (Just tok_b) ty_b) $ \Refl ->
 220                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 221                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 222                         check_type
 223                          (At (Just tok_b2e2b) ty_b2e2b_a2b_e)
 224                          (At (Just tok_o) ty_o_e) $ \Refl ->
 225                         k ty_b $ TermO $
 226                          \c -> fold (b2e2b c) (b c) (o c)
 227                 o2ty_from
 228                  :: forall typ. Inj_Const (Consts_of_Ifaces is) typ
 229                  => EToken meta is
 230                  -> (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term typ)
 231                  -> Either (Error_Term meta is) ret
 232                 o2ty_from tok_o f =
 233                         -- olength :: MonoFoldable o => o -> Int
 234                         -- onull   :: MonoFoldable o => o -> Bool
 235                         compileO tok_o ctx $ \ty_o (TermO o) ->
 236                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 237                         k (TyConst inj_const::Type (Consts_of_Ifaces is) typ) $ TermO $
 238                          \c -> f (o c)
 239                 oalloany_from
 240                  tok_e2Bool tok_o
 241                  (g::forall term o.
 242                          (Sym_MonoFoldable term, MonoFoldable o)
 243                          => term (MT.Element o -> Bool) -> term o -> term Bool) =
 244                  -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 245                  -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 246                         compileO tok_e2Bool ctx $ \ty_e2Bool (TermO e2Bool) ->
 247                         compileO tok_o ctx $ \ty_o (TermO o) ->
 248                         check_type2 (ty @(->)) (At (Just tok_e2Bool) ty_e2Bool) $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 249                         check_con (At (Just tok_o) (ty @MonoFoldable :$ ty_o)) $ \Con ->
 250                         check_fam (At (Just tok_o) Fam_MonoElement) (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 251                         check_type
 252                          (At (Just tok_e2Bool) ty_e2Bool_e)
 253                          (At (Just tok_o) ty_o_e) $ \Refl ->
 254                         check_type
 255                          (At Nothing (ty @Bool))
 256                          (At (Just tok_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 257                         k (ty @Bool) $ TermO $
 258                          \c -> g (e2Bool c) (o c)