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