Language/Symantic/Compiling/MonoFoldable.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE DefaultSignatures #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE InstanceSigs #-}
   7 {-# LANGUAGE MultiParamTypeClasses #-}
   8 {-# LANGUAGE OverloadedStrings #-}
   9 {-# LANGUAGE PolyKinds #-}
  10 {-# LANGUAGE Rank2Types #-}
  11 {-# LANGUAGE ScopedTypeVariables #-}
  12 {-# LANGUAGE TypeFamilies #-}
  13 {-# LANGUAGE TypeOperators #-}
  14 {-# LANGUAGE UndecidableInstances #-}
  15 {-# OPTIONS_GHC -fno-warn-orphans #-}
  16 {-# OPTIONS_GHC -fconstraint-solver-iterations=9 #-}
  17 -- | Symantic for 'MonoFoldable'.
  18 module Language.Symantic.Compiling.MonoFoldable where
  19
  20 import Control.Monad (liftM, liftM2, liftM3)
  21 import Data.MonoTraversable (MonoFoldable)
  22 import qualified Data.MonoTraversable as MT
  23 import Data.Proxy
  24 import Data.String (IsString)
  25 import Data.Text (Text)
  26 import Data.Type.Equality ((:~:)(Refl))
  27
  28 import Language.Symantic.Typing
  29 import Language.Symantic.Compiling.Term
  30 import Language.Symantic.Compiling.Bool (tyBool)
  31 import Language.Symantic.Compiling.List (tyList)
  32 import Language.Symantic.Compiling.MonoFunctor
  33 import Language.Symantic.Compiling.Monoid (tyMonoid)
  34 import Language.Symantic.Interpreting
  35 import Language.Symantic.Transforming.Trans
  36
  37 -- * Class 'Sym_MonoFoldable'
  38 class Sym_MonoFoldable term where
  39         ofoldMap :: (MonoFoldable o, Monoid m) => term (MT.Element o -> m) -> term o -> term m
  40         ofoldr :: MonoFoldable o => term (MT.Element o -> b -> b) -> term b -> term o -> term b
  41         ofoldl' :: MonoFoldable o => term (b -> MT.Element o -> b) -> term b -> term o -> term b
  42         olength :: MonoFoldable o => term o -> term Int
  43         onull :: MonoFoldable o => term o -> term Bool
  44         oall :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
  45         oany :: MonoFoldable o => term (MT.Element o -> Bool) -> term o -> term Bool
  46         otoList :: MonoFoldable o => term o -> term [MT.Element o]
  47         default ofoldMap :: (Trans t term, MonoFoldable o, Monoid m)
  48          => t term (MT.Element o -> m) -> t term o -> t term m
  49         default ofoldr :: (Trans t term, MonoFoldable o)
  50          => t term (MT.Element o -> b -> b) -> t term b -> t term o -> t term b
  51         default ofoldl' :: (Trans t term, MonoFoldable o)
  52          => t term (b -> MT.Element o -> b) -> t term b -> t term o -> t term b
  53         default olength :: (Trans t term, MonoFoldable o) => t term o -> t term Int
  54         default onull :: (Trans t term, MonoFoldable o) => t term o -> t term Bool
  55         default oall :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
  56         default oany :: (Trans t term, MonoFoldable o) => t term (MT.Element o -> Bool) -> t term o -> t term Bool
  57         default otoList :: (Trans t term, MonoFoldable o) => t term o -> t term [MT.Element o]
  58         ofoldMap = trans_map2 ofoldMap
  59         ofoldr   = trans_map3 ofoldr
  60         ofoldl'  = trans_map3 ofoldl'
  61         olength  = trans_map1 olength
  62         onull    = trans_map1 onull
  63         oall     = trans_map2 oall
  64         oany     = trans_map2 oany
  65         otoList  = trans_map1 otoList
  66
  67 type instance Sym_of_Iface (Proxy MonoFoldable) = Sym_MonoFoldable
  68 type instance Consts_of_Iface (Proxy MonoFoldable) = Proxy MonoFoldable ': Consts_imported_by MonoFoldable
  69 type instance Consts_imported_by MonoFoldable =
  70  [ Proxy (->)
  71  , Proxy (,)
  72  , Proxy []
  73  , Proxy Bool
  74  , Proxy Either
  75  , Proxy Int
  76  , Proxy Maybe
  77  , Proxy Monoid
  78  , Proxy String
  79  , Proxy Text
  80  ]
  81
  82 instance Sym_MonoFoldable HostI where
  83         ofoldMap = liftM2 MT.ofoldMap
  84         ofoldr   = liftM3 MT.ofoldr
  85         ofoldl'  = liftM3 MT.ofoldl'
  86         olength  = liftM  MT.olength
  87         onull    = liftM  MT.onull
  88         oall     = liftM2 MT.oall
  89         oany     = liftM2 MT.oany
  90         otoList  = liftM  MT.otoList
  91 instance Sym_MonoFoldable TextI where
  92         ofoldMap = textI_app2 "ofoldMap"
  93         ofoldr   = textI_app3 "ofoldr"
  94         ofoldl'  = textI_app3 "ofoldl'"
  95         olength  = textI_app1 "olength"
  96         onull    = textI_app1 "onull"
  97         oall     = textI_app2 "oall"
  98         oany     = textI_app2 "oany"
  99         otoList  = textI_app1 "otoList"
 100 instance (Sym_MonoFoldable r1, Sym_MonoFoldable r2) => Sym_MonoFoldable (DupI r1 r2) where
 101         ofoldMap = dupI2 sym_MonoFoldable ofoldMap
 102         ofoldr   = dupI3 sym_MonoFoldable ofoldr
 103         ofoldl'  = dupI3 sym_MonoFoldable ofoldl'
 104         olength  = dupI1 sym_MonoFoldable olength
 105         onull    = dupI1 sym_MonoFoldable onull
 106         oall     = dupI2 sym_MonoFoldable oall
 107         oany     = dupI2 sym_MonoFoldable oany
 108         otoList  = dupI1 sym_MonoFoldable otoList
 109
 110 instance Const_from Text cs => Const_from Text (Proxy MonoFoldable ': cs) where
 111         const_from "MonoFoldable" k = k (ConstZ kind)
 112         const_from s k = const_from s $ k . ConstS
 113 instance Show_Const cs => Show_Const (Proxy MonoFoldable ': cs) where
 114         show_const ConstZ{} = "MonoFoldable"
 115         show_const (ConstS c) = show_const c
 116
 117 instance -- Proj_ConC
 118  ( Proj_Const cs MonoFoldable
 119  , Proj_Consts cs (Consts_imported_by MonoFoldable)
 120  ) => Proj_ConC cs (Proxy MonoFoldable) where
 121         proj_conC _ (TyConst q :$ ty)
 122          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 123          , Just Refl <- proj_const q (Proxy::Proxy MonoFoldable)
 124          = case ty of
 125                  TyConst c
 126                   | Just Refl <- proj_const c (Proxy::Proxy String) -> Just Con
 127                   | Just Refl <- proj_const c (Proxy::Proxy Text)   -> Just Con
 128                  TyConst c :$ _a
 129                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 130                   -> case () of
 131                          _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
 132                            | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
 133                          _ -> Nothing
 134                  TyConst c :$ _a :$ _b
 135                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 136                   -> case () of
 137                          _ | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
 138                            | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
 139                          _ -> Nothing
 140                  _ -> Nothing
 141         proj_conC _c _q = Nothing
 142 instance -- Term_fromI
 143  ( AST ast
 144  , Lexem ast ~ LamVarName
 145  , Inj_Const (Consts_of_Ifaces is) MonoFoldable
 146  , Inj_Const (Consts_of_Ifaces is) (->)
 147  , Inj_Const (Consts_of_Ifaces is) []
 148  , Inj_Const (Consts_of_Ifaces is) Monoid
 149  , Inj_Const (Consts_of_Ifaces is) Bool
 150  , Inj_Const (Consts_of_Ifaces is) Int
 151  , Proj_Con  (Consts_of_Ifaces is)
 152  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 153  , Term_from is ast
 154  ) => Term_fromI is (Proxy MonoFoldable) ast where
 155         term_fromI :: forall ctx ls rs ret. Term_fromIT ast ctx ret is ls (Proxy MonoFoldable ': rs)
 156         term_fromI ast ctx k =
 157                 case ast_lexem ast of
 158                  "ofoldMap" -> ofoldMap_from
 159                  "ofoldr"   -> ofoldr_from ofoldr
 160                  "ofoldl'"  -> ofoldl_from ofoldl'
 161                  "olength"  -> o2ty_from olength
 162                  "onull"    -> o2ty_from onull
 163                  "oall"     -> oalloany_from oall
 164                  "oany"     -> oalloany_from oany
 165                  "otoList"  -> otoList_from
 166                  _ -> Left $ Error_Term_unsupported
 167                 where
 168                 ofoldMap_from =
 169                  -- ofoldMap :: Monoid m => (Element o -> m) -> o -> m
 170                         from_ast2 ast $ \ast_f ast_o as ->
 171                         term_from ast_f ctx $ \ty_f (TermLC f) ->
 172                         term_from ast_o ctx $ \ty_o (TermLC o) ->
 173                         check_type2 tyFun ast_f ty_f $ \Refl ty_f_a ty_m ->
 174                         check_constraint (At (Just ast_f) (tyMonoFoldable :$ ty_o)) $ \Con ->
 175                         check_constraint (At (Just ast_f) (tyMonoid :$ ty_m)) $ \Con ->
 176                         check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 177                         check_type (At Nothing ty_o_e) (At (Just ast_f) ty_f_a) $ \Refl ->
 178                         k as ty_m $ TermLC $
 179                          \c -> ofoldMap (f c) (o c)
 180                 ofoldr_from
 181                  (fold::forall term o b.
 182                          (Sym_MonoFoldable term, MonoFoldable o)
 183                          => term (MT.Element o -> b -> b) -> term b -> term o -> term b) =
 184                  -- ofoldr :: MonoFoldable o => (MT.Element o -> b -> b) -> b -> o -> b
 185                         from_ast3 ast $ \ast_e2b2b ast_b ast_o as ->
 186                         term_from ast_e2b2b ctx $ \ty_e2b2b (TermLC e2b2b) ->
 187                         term_from ast_b     ctx $ \ty_b     (TermLC b) ->
 188                         term_from ast_o     ctx $ \ty_o     (TermLC o) ->
 189                         check_type2 tyFun ast_e2b2b ty_e2b2b $ \Refl ty_e2b2b_e ty_e2b2b_b2b ->
 190                         check_type2 tyFun ast_e2b2b ty_e2b2b_b2b $ \Refl ty_e2b2b_b2b_b0 ty_e2b2b_b2b_b1 ->
 191                         check_type (At (Just ast_e2b2b) ty_e2b2b_b2b_b0) (At (Just ast_e2b2b) ty_e2b2b_b2b_b1) $ \Refl ->
 192                         check_type (At (Just ast_e2b2b) ty_e2b2b_b2b_b0) (At (Just ast_b) ty_b) $ \Refl ->
 193                         check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
 194                         check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 195                         check_type (At (Just ast_e2b2b) ty_e2b2b_e) (At (Just ast_o) ty_o_e) $ \Refl ->
 196                         k as ty_b $ TermLC $
 197                          \c -> fold (e2b2b c) (b c) (o c)
 198                 ofoldl_from
 199                  (fold::forall term o b.
 200                          (Sym_MonoFoldable term, MonoFoldable o)
 201                          => term (b -> MT.Element o -> b) -> term b -> term o -> term b) =
 202                  -- ofoldl' :: MonoFoldable o => (b -> MT.Element o -> b) -> b -> o -> b
 203                         from_ast3 ast $ \ast_b2e2b ast_b ast_o as ->
 204                         term_from ast_b2e2b ctx $ \ty_b2e2b (TermLC b2e2b) ->
 205                         term_from ast_b     ctx $ \ty_b     (TermLC b) ->
 206                         term_from ast_o     ctx $ \ty_o     (TermLC o) ->
 207                         check_type2 tyFun ast_b2e2b ty_b2e2b $ \Refl ty_b2e2b_b ty_b2e2b_a2b ->
 208                         check_type2 tyFun ast_b2e2b ty_b2e2b_a2b $ \Refl ty_b2e2b_a2b_e ty_b2e2b_a2b_b ->
 209                         check_type (At (Just ast_b2e2b) ty_b2e2b_b) (At (Just ast_b2e2b) ty_b2e2b_a2b_b) $ \Refl ->
 210                         check_type (At (Just ast_b2e2b) ty_b2e2b_b) (At (Just ast_b) ty_b) $ \Refl ->
 211                         check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
 212                         check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 213                         check_type (At (Just ast_b2e2b) ty_b2e2b_a2b_e) (At (Just ast_o) ty_o_e) $ \Refl ->
 214                         k as ty_b $ TermLC $
 215                          \c -> fold (b2e2b c) (b c) (o c)
 216                 o2ty_from
 217                  :: forall ty. Inj_Const (Consts_of_Ifaces is) ty
 218                  => (forall term o. (Sym_MonoFoldable term, MonoFoldable o) => term o -> term ty)
 219                  -> Either (Error_Term is ast) ret
 220                 o2ty_from f =
 221                  -- length :: MonoFoldable o => o -> Int
 222                  -- null   :: MonoFoldable o => o -> Bool
 223                         from_ast1 ast $ \ast_o as ->
 224                         term_from ast_o ctx $ \ty_o (TermLC o) ->
 225                         check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
 226                         k as (TyConst inj_const::Type (Consts_of_Ifaces is) ty) $ TermLC $
 227                          \c -> f (o c)
 228                 oalloany_from
 229                  (g::forall term o.
 230                          (Sym_MonoFoldable term, MonoFoldable o)
 231                          => term (MT.Element o -> Bool) -> term o -> term Bool) =
 232                  -- all :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 233                  -- any :: MonoFoldable o => (MT.Element o -> Bool) -> o -> Bool
 234                         from_ast2 ast $ \ast_e2Bool ast_o as ->
 235                         term_from ast_e2Bool ctx $ \ty_e2Bool (TermLC e2Bool) ->
 236                         term_from ast_o ctx $ \ty_o (TermLC o) ->
 237                         check_type2 tyFun ast_e2Bool ty_e2Bool $ \Refl ty_e2Bool_e ty_e2Bool_Bool ->
 238                         check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
 239                         check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 240                         check_type (At (Just ast_e2Bool) ty_e2Bool_e) (At (Just ast_o) ty_o_e) $ \Refl ->
 241                         check_type (At Nothing tyBool) (At (Just ast_e2Bool) ty_e2Bool_Bool) $ \Refl ->
 242                         k as tyBool $ TermLC $
 243                          \c -> g (e2Bool c) (o c)
 244                 otoList_from =
 245                  -- otoList :: MonoFoldable o => o -> [MT.Element o]
 246                         from_ast1 ast $ \ast_o as ->
 247                         term_from ast_o ctx $ \ty_o (TermLC o) ->
 248                         check_constraint (At (Just ast_o) (tyMonoFoldable :$ ty_o)) $ \Con ->
 249                         check_family ast Fam_MonoElement (ty_o `TypesS` TypesZ) $ \ty_o_e ->
 250                         k as (tyList :$ ty_o_e) $ TermLC $
 251                          \c -> otoList (o c)
 252
 253 -- | The 'MonoFoldable' 'Type'
 254 tyMonoFoldable :: Inj_Const cs MonoFoldable => Type cs MonoFoldable
 255 tyMonoFoldable = TyConst inj_const
 256
 257 sym_MonoFoldable :: Proxy Sym_MonoFoldable
 258 sym_MonoFoldable = Proxy
 259
 260 syMonoFoldable :: IsString a => [Syntax a] -> Syntax a
 261 syMonoFoldable = Syntax "MonoFoldable"