Language/Symantic/Compiling/MonoFunctor.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 Rank2Types #-}
  10 {-# LANGUAGE ScopedTypeVariables #-}
  11 {-# LANGUAGE TypeFamilies #-}
  12 {-# LANGUAGE TypeOperators #-}
  13 {-# LANGUAGE UndecidableInstances #-}
  14 {-# OPTIONS_GHC -fno-warn-orphans #-}
  15 {-# OPTIONS_GHC -fconstraint-solver-iterations=7 #-}
  16 -- | Symantic for 'MonoFunctor'.
  17 module Language.Symantic.Compiling.MonoFunctor where
  18
  19 import Control.Monad (liftM2)
  20 import Data.Map.Strict (Map)
  21 import Data.MonoTraversable (MonoFunctor)
  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 import GHC.Exts (Constraint)
  28 import qualified System.IO as IO
  29
  30 import Language.Symantic.Typing
  31 import Language.Symantic.Compiling.Term
  32 import Language.Symantic.Interpreting
  33 import Language.Symantic.Transforming.Trans
  34 import Language.Symantic.Lib.Data.Type.List hiding (Map)
  35
  36 -- * Class 'Sym_MonoFunctor'
  37 class Sym_MonoFunctor term where
  38         omap :: MonoFunctor o => term (MT.Element o -> MT.Element o) -> term o -> term o
  39         default omap :: (Trans t term, MonoFunctor o)
  40          => t term (MT.Element o -> MT.Element o) -> t term o -> t term o
  41         omap = trans_map2 omap
  42
  43 type instance Sym_of_Iface (Proxy MonoFunctor) = Sym_MonoFunctor
  44 type instance Consts_of_Iface (Proxy MonoFunctor) = Proxy MonoFunctor ': Consts_imported_by MonoFunctor
  45 type instance Consts_imported_by MonoFunctor =
  46  [ Proxy (->)
  47  , Proxy (,)
  48  , Proxy []
  49  , Proxy Either
  50  , Proxy IO
  51  , Proxy Maybe
  52  , Proxy String
  53  , Proxy Text
  54  ] ++ Consts_imported_by IO
  55
  56 instance Sym_MonoFunctor HostI where
  57         omap = liftM2 MT.omap
  58 instance Sym_MonoFunctor TextI where
  59         omap = textI_app2 "omap"
  60 instance (Sym_MonoFunctor r1, Sym_MonoFunctor r2) => Sym_MonoFunctor (DupI r1 r2) where
  61         omap = dupI2 sym_MonoFunctor omap
  62
  63 instance Const_from Text cs => Const_from Text (Proxy MonoFunctor ': cs) where
  64         const_from "MonoFunctor" k = k (ConstZ kind)
  65         const_from s k = const_from s $ k . ConstS
  66 instance Show_Const cs => Show_Const (Proxy MonoFunctor ': cs) where
  67         show_const ConstZ{} = "MonoFunctor"
  68         show_const (ConstS c) = show_const c
  69
  70 -- * Type 'Fam_MonoElement'
  71 data Fam_MonoElement
  72 type instance Fam Fam_MonoElement h = MT.Element h
  73 instance -- Constraint
  74  Proj_FamC cs Fam_MonoElement (Proxy (c::Constraint))
  75 instance -- k -> Constraint
  76  Proj_FamC cs Fam_MonoElement (Proxy (c::k -> Constraint))
  77 instance -- ()
  78  Proj_FamC cs Fam_MonoElement (Proxy ())
  79 instance -- Bool
  80  Proj_FamC cs Fam_MonoElement (Proxy Bool)
  81 instance -- Char
  82  Proj_FamC cs Fam_MonoElement (Proxy Char)
  83 instance -- String
  84  ( Proj_Const cs String
  85  , Inj_Const cs (Fam Fam_MonoElement String)
  86  ) => Proj_FamC cs Fam_MonoElement (Proxy String) where
  87         proj_famC _c _fam (TyConst c)
  88          | Just Refl <- eq_skind (kind_of_const c) SKiType
  89          , Just Refl <- proj_const c (Proxy::Proxy String)
  90          = Just $ Just (TyConst inj_const::Type cs (Fam Fam_MonoElement String))
  91         proj_famC _c _fam _ty = Nothing
  92 instance -- Text
  93  ( Proj_Const cs Text
  94  , Inj_Const cs (Fam Fam_MonoElement Text)
  95  ) => Proj_FamC cs Fam_MonoElement (Proxy Text) where
  96         proj_famC _c _fam (TyConst c)
  97          | Just Refl <- eq_skind (kind_of_const c) SKiType
  98          , Just Refl <- proj_const c (Proxy::Proxy Text)
  99          = Just $ Just (TyConst inj_const::Type cs (Fam Fam_MonoElement Text))
 100         proj_famC _c _fam _ty = Nothing
 101 instance -- []
 102  ( Proj_Const cs []
 103  ) => Proj_FamC cs Fam_MonoElement (Proxy []) where
 104         proj_famC _c _fam (TyConst c :$ ty_a)
 105          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 106          , Just Refl <- proj_const c (Proxy::Proxy [])
 107          = Just $ Just ty_a
 108         proj_famC _c _fam _ty = Nothing
 109 instance -- IO
 110  ( Proj_Const cs IO
 111  ) => Proj_FamC cs Fam_MonoElement (Proxy IO) where
 112         proj_famC _c _fam (TyConst c :$ ty_a)
 113          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 114          , Just Refl <- proj_const c (Proxy::Proxy IO)
 115          = Just $ Just ty_a
 116         proj_famC _c _fam _ty = Nothing
 117 instance -- IO.Handle
 118  Proj_FamC cs Fam_MonoElement (Proxy IO.Handle)
 119 instance -- IO.IOMode
 120  Proj_FamC cs Fam_MonoElement (Proxy IO.IOMode)
 121 instance -- Maybe
 122  ( Proj_Const cs Maybe
 123  ) => Proj_FamC cs Fam_MonoElement (Proxy Maybe) where
 124         proj_famC _c _fam (TyConst c :$ ty_a)
 125          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 126          , Just Refl <- proj_const c (Proxy::Proxy Maybe)
 127          = Just $ Just ty_a
 128         proj_famC _c _fam _ty = Nothing
 129 instance -- (->)
 130  ( Proj_Const cs (->)
 131  ) => Proj_FamC cs Fam_MonoElement (Proxy (->)) where
 132         proj_famC _c _fam (TyConst c :$ _ty_r :$ ty_a)
 133          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 134          , Just Refl <- proj_const c (Proxy::Proxy (->))
 135          = Just $ Just ty_a
 136         proj_famC _c _fam _ty = Nothing
 137 instance -- (,)
 138  ( Proj_Const cs (,)
 139  ) => Proj_FamC cs Fam_MonoElement (Proxy (,)) where
 140         proj_famC _c _fam (TyConst c :$ _ty_a :$ ty_b)
 141          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 142          , Just Refl <- proj_const c (Proxy::Proxy (,))
 143          = Just $ Just ty_b
 144         proj_famC _c _fam _ty = Nothing
 145 instance -- Either
 146  ( Proj_Const cs Either
 147  ) => Proj_FamC cs Fam_MonoElement (Proxy Either) where
 148         proj_famC _c _fam (TyConst c :$ _ty_l :$ ty_r)
 149          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 150          , Just Refl <- proj_const c (Proxy::Proxy Either)
 151          = Just $ Just ty_r
 152         proj_famC _c _fam _ty = Nothing
 153 instance -- Map
 154  ( Proj_Const cs Map
 155  ) => Proj_FamC cs Fam_MonoElement (Proxy Map) where
 156         proj_famC _c _fam (TyConst c :$ _ty_k :$ ty_a)
 157          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 158          , Just Refl <- proj_const c (Proxy::Proxy Map)
 159          = Just $ Just ty_a
 160         proj_famC _c _fam _ty = Nothing
 161
 162 instance -- Proj_ConC
 163  ( Proj_Const cs MonoFunctor
 164  , Proj_Consts cs (Consts_imported_by MonoFunctor)
 165  ) => Proj_ConC cs (Proxy MonoFunctor) where
 166         proj_conC _ (TyConst q :$ ty)
 167          | Just Refl <- eq_skind (kind_of_const q) (SKiType `SKiArrow` SKiConstraint)
 168          , Just Refl <- proj_const q (Proxy::Proxy MonoFunctor)
 169          = case ty of
 170                  TyConst c
 171                   | Just Refl <- proj_const c (Proxy::Proxy String) -> Just Con
 172                   | Just Refl <- proj_const c (Proxy::Proxy Text)   -> Just Con
 173                  TyConst c :$ _a
 174                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
 175                   -> case () of
 176                          _ | Just Refl <- proj_const c (Proxy::Proxy [])    -> Just Con
 177                            | Just Refl <- proj_const c (Proxy::Proxy IO)    -> Just Con
 178                            | Just Refl <- proj_const c (Proxy::Proxy Maybe) -> Just Con
 179                          _ -> Nothing
 180                  TyConst c :$ _a :$ _b
 181                   | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType `SKiArrow` SKiType)
 182                   -> case () of
 183                          _ | Just Refl <- proj_const c (Proxy::Proxy (->))   -> Just Con
 184                            | Just Refl <- proj_const c (Proxy::Proxy (,))    -> Just Con
 185                            | Just Refl <- proj_const c (Proxy::Proxy Either) -> Just Con
 186                          _ -> Nothing
 187                  _ -> Nothing
 188         proj_conC _c _q = Nothing
 189 instance -- Term_fromI
 190  ( AST ast
 191  , Lexem ast ~ LamVarName
 192  , Inj_Const (Consts_of_Ifaces is) MonoFunctor
 193  , Inj_Const (Consts_of_Ifaces is) (->)
 194  , Proj_Con  (Consts_of_Ifaces is)
 195  , Proj_Fam  (Consts_of_Ifaces is) Fam_MonoElement
 196  , Term_from is ast
 197  ) => Term_fromI is (Proxy MonoFunctor) ast where
 198         term_fromI ast ctx k =
 199                 case ast_lexem ast of
 200                  "omap" -> omap_from
 201                  _ -> Left $ Error_Term_unsupported
 202                 where
 203                 omap_from =
 204                  -- omap :: (Element mono -> Element mono) -> mono -> mono
 205                         from_ast2 ast $ \ast_f ast_m as ->
 206                         term_from ast_f ctx $ \ty_f (TermLC f) ->
 207                         term_from ast_m ctx $ \ty_m (TermLC m) ->
 208                         check_type2 tyFun ast_f ty_f $ \Refl ty_f_a ty_f_b ->
 209                         check_type (At (Just ast_f) ty_f_a) (At (Just ast_f) ty_f_b) $ \Refl ->
 210                         check_constraint (At (Just ast_f) (tyMonoFunctor :$ ty_m)) $ \Con ->
 211                         check_family (Proxy::Proxy Fam_MonoElement) (At (Just ast) ty_m) $ \ty_m_ele ->
 212                         check_type (At Nothing ty_m_ele) (At (Just ast_f) ty_f_a) $ \Refl ->
 213                         k as ty_m $ TermLC $
 214                          \c -> omap (f c) (m c)
 215
 216 -- | The 'MonoFunctor' 'Type'
 217 tyMonoFunctor :: Inj_Const cs MonoFunctor => Type cs MonoFunctor
 218 tyMonoFunctor = TyConst inj_const
 219
 220 sym_MonoFunctor :: Proxy Sym_MonoFunctor
 221 sym_MonoFunctor = Proxy
 222
 223 syMonoFunctor :: IsString a => [Syntax a] -> Syntax a
 224 syMonoFunctor = Syntax "MonoFunctor"