symantic-lib/Language/Symantic/Lib/IO.hs

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
   4 -- | Symantic for 'IO'.
   5 module Language.Symantic.Lib.IO where
   6
   7 import Control.Monad (liftM, liftM2)
   8 import Data.MonoTraversable (MonoFunctor)
   9 import Data.Proxy
  10 import Data.Type.Equality ((:~:)(Refl))
  11 import qualified System.IO as IO
  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.Lambda
  19 import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
  20
  21 -- * Class 'Sym_IO'
  22 class Sym_IO term where
  23         io_hClose   :: term IO.Handle -> term (IO ())
  24         io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
  25
  26         default io_hClose   :: Trans t term => t term IO.Handle -> t term (IO ())
  27         default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle)
  28
  29         io_hClose   = trans_map1 io_hClose
  30         io_openFile = trans_map2 io_openFile
  31 class Sym_IO_Handle (term:: * -> *)
  32 class Sym_IO_IOMode (term:: * -> *)
  33
  34 type instance Sym_of_Iface      (Proxy IO)        = Sym_IO
  35 type instance Sym_of_Iface      (Proxy IO.Handle) = Sym_IO_Handle
  36 type instance Sym_of_Iface      (Proxy IO.IOMode) = Sym_IO_IOMode
  37 type instance TyConsts_of_Iface (Proxy IO)        = Proxy IO ': TyConsts_imported_by (Proxy IO)
  38 type instance TyConsts_of_Iface (Proxy IO.Handle) = Proxy IO.Handle ': TyConsts_imported_by (Proxy IO.Handle)
  39 type instance TyConsts_of_Iface (Proxy IO.IOMode) = Proxy IO.IOMode ': TyConsts_imported_by (Proxy IO.IOMode)
  40 type instance TyConsts_imported_by (Proxy IO) =
  41  [ Proxy IO.Handle
  42  , Proxy IO.IOMode
  43  , Proxy Applicative
  44  , Proxy Functor
  45  , Proxy Monad
  46  , Proxy MonoFunctor
  47  ]
  48 type instance TyConsts_imported_by (Proxy IO.Handle) =
  49  '[ Proxy Eq
  50  ]
  51 type instance TyConsts_imported_by (Proxy IO.IOMode) =
  52  [ Proxy Enum
  53  , Proxy Eq
  54  , Proxy Ord
  55  ]
  56
  57 instance Sym_IO HostI where
  58         io_hClose   = liftM IO.hClose
  59         io_openFile = liftM2 IO.openFile
  60 instance Sym_IO_Handle HostI
  61 instance Sym_IO_IOMode HostI
  62 instance Sym_IO TextI where
  63         io_hClose   = textI1 "IO.hClose"
  64         io_openFile = textI2 "IO.openFile"
  65 instance Sym_IO_Handle TextI
  66 instance Sym_IO_IOMode TextI
  67 instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
  68         io_hClose   = dupI1 @Sym_IO io_hClose
  69         io_openFile = dupI2 @Sym_IO io_openFile
  70 instance Sym_IO_Handle (DupI r1 r2)
  71 instance Sym_IO_IOMode (DupI r1 r2)
  72
  73 instance
  74  ( Read_TyNameR TyName cs rs
  75  , Inj_TyConst cs IO
  76  ) => Read_TyNameR TyName cs (Proxy IO ': rs) where
  77         read_TyNameR _cs (TyName "IO") k = k (ty @IO)
  78         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  79 instance
  80  ( Read_TyNameR TyName cs rs
  81  , Inj_TyConst cs IO.Handle
  82  ) => Read_TyNameR TyName cs (Proxy IO.Handle ': rs) where
  83         read_TyNameR _cs (TyName "IO.Handle") k = k (ty @IO.Handle)
  84         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  85 instance
  86  ( Read_TyNameR TyName cs rs
  87  , Inj_TyConst cs IO.IOMode
  88  ) => Read_TyNameR TyName cs (Proxy IO.IOMode ': rs) where
  89         read_TyNameR _cs (TyName "IO.Mode") k = k (ty @IO.IOMode)
  90         read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
  91
  92 instance Show_TyConst cs => Show_TyConst (Proxy IO ': cs) where
  93         show_TyConst TyConstZ{} = "IO"
  94         show_TyConst (TyConstS c) = show_TyConst c
  95 instance Show_TyConst cs => Show_TyConst (Proxy IO.Handle ': cs) where
  96         show_TyConst TyConstZ{} = "IO.Handle"
  97         show_TyConst (TyConstS c) = show_TyConst c
  98 instance Show_TyConst cs => Show_TyConst (Proxy IO.IOMode ': cs) where
  99         show_TyConst TyConstZ{} = "IO.IOMode"
 100         show_TyConst (TyConstS c) = show_TyConst c
 101
 102 instance -- Proj_TyFamC TyFam_MonoElement IO
 103  ( Proj_TyConst cs IO
 104  ) => Proj_TyFamC cs TyFam_MonoElement IO where
 105         proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
 106          | Just Refl <- eq_SKind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 107          , Just Refl <- proj_TyConst c (Proxy @IO)
 108          = Just ty_a
 109         proj_TyFamC _c _fam _ty = Nothing
 110 instance -- Proj_TyFamC TyFam_MonoElement IO.Handle
 111  Proj_TyFamC cs TyFam_MonoElement IO.Handle
 112 instance -- Proj_TyFamC TyFam_MonoElement IO.IOMode
 113  Proj_TyFamC cs TyFam_MonoElement IO.IOMode
 114
 115 instance -- Proj_TyConC IO
 116  ( Proj_TyConst cs IO
 117  , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO))
 118  ) => Proj_TyConC cs (Proxy IO) where
 119         proj_TyConC _ (TyConst q :$ TyConst c)
 120          | Just Refl <- eq_SKind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 121          , Just Refl <- proj_TyConst c (Proxy @IO)
 122          = case () of
 123                  _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
 124                    | Just Refl <- proj_TyConst q (Proxy @Functor)     -> Just TyCon
 125                    | Just Refl <- proj_TyConst q (Proxy @Monad)       -> Just TyCon
 126                  _ -> Nothing
 127         proj_TyConC _ (TyConst q :$ (TyConst c :$ _a))
 128          | Just Refl <- eq_SKind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
 129          , Just Refl <- proj_TyConst c (Proxy @IO)
 130          = case () of
 131                  _ | Just Refl <- proj_TyConst q (Proxy @MonoFunctor) -> Just TyCon
 132                  _ -> Nothing
 133         proj_TyConC _c _q = Nothing
 134 instance -- Proj_TyConC IO.Handle
 135  ( Proj_TyConst cs IO.Handle
 136  , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO.Handle))
 137  ) => Proj_TyConC cs (Proxy IO.Handle) where
 138         proj_TyConC _ (TyConst q :$ TyConst c)
 139          | Just Refl <- eq_SKind (kind_of_TyConst c) SKiType
 140          , Just Refl <- proj_TyConst c (Proxy @IO.Handle)
 141          = case () of
 142                  _ | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
 143                  _ -> Nothing
 144         proj_TyConC _c _q = Nothing
 145 instance -- Proj_TyConC IO.IOMode
 146  ( Proj_TyConst cs IO.IOMode
 147  , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO.IOMode))
 148  ) => Proj_TyConC cs (Proxy IO.IOMode) where
 149         proj_TyConC _ (TyConst q :$ TyConst c)
 150          | Just Refl <- eq_SKind (kind_of_TyConst c) SKiType
 151          , Just Refl <- proj_TyConst c (Proxy @IO.IOMode)
 152          = case () of
 153                  _ | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
 154                    | Just Refl <- proj_TyConst q (Proxy @Eq)   -> Just TyCon
 155                    | Just Refl <- proj_TyConst q (Proxy @Ord)  -> Just TyCon
 156                  _ -> Nothing
 157         proj_TyConC _c _q = Nothing
 158 data instance TokenT meta (ts::[*]) (Proxy IO)
 159  = Token_Term_IO_hClose   (EToken meta ts)
 160  | Token_Term_IO_openFile (EToken meta ts)
 161 data instance TokenT meta (ts::[*]) (Proxy IO.Handle)
 162 data instance TokenT meta (ts::[*]) (Proxy IO.IOMode)
 163 deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO))
 164 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO))
 165 deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO.Handle))
 166 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.Handle))
 167 deriving instance Eq_Token   meta ts => Eq   (TokenT meta ts (Proxy IO.IOMode))
 168 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.IOMode))
 169
 170 instance -- CompileI IO
 171  ( Inj_TyConst cs IO
 172  , Inj_TyConst cs IO.Handle
 173  , Inj_TyConst cs []
 174  , Inj_TyConst cs Char
 175  , Inj_TyConst cs IO.IOMode
 176  , Inj_TyConst cs (->)
 177  , Inj_TyConst cs ()
 178  , Compile cs is
 179  ) => CompileI cs is (Proxy IO) where
 180         compileI tok ctx k =
 181                 case tok of
 182                  Token_Term_IO_hClose tok_h ->
 183                         -- hClose :: Handle -> IO ()
 184                         compile tok_h ctx $ \ty_h (Term h) ->
 185                         check_TyEq
 186                          (At Nothing (ty @IO.Handle))
 187                          (At (Just tok_h) ty_h) $ \Refl ->
 188                         k (ty @IO :$ ty @()) $ Term $
 189                                 io_hClose . h
 190                  Token_Term_IO_openFile tok_fp ->
 191                         -- openFile :: FilePath -> IOMode -> IO Handle
 192                         compile tok_fp ctx $ \ty_fp (Term fp) ->
 193                         check_TyEq
 194                          (At Nothing tyFilePath)
 195                          (At (Just tok_fp) ty_fp) $ \Refl ->
 196                         k (ty @IO.IOMode ~> ty @IO :$ ty @IO.Handle) $ Term $
 197                          \c -> lam $ io_openFile (fp c)
 198                 where tyFilePath = ty @[] :$ ty @Char
 199 instance CompileI cs is (Proxy IO.Handle) where
 200         compileI tok _ctx _k = case tok of _ -> undefined
 201 instance CompileI cs is (Proxy IO.IOMode) where
 202         compileI tok _ctx _k = case tok of _ -> undefined
 203 instance -- TokenizeT IO
 204  Inj_Token meta ts IO =>
 205  TokenizeT meta ts (Proxy IO) where
 206         tokenizeT _t = mempty
 207          { tokenizers_infix = tokenizeTMod [Mod_Name "IO"]
 208                  [ tokenize1 "hClose"   infixN5 Token_Term_IO_hClose
 209                  , tokenize1 "openFile" infixN5 Token_Term_IO_openFile
 210                  ]
 211          }
 212 instance TokenizeT meta ts (Proxy IO.Handle)
 213 instance TokenizeT meta ts (Proxy IO.IOMode)
 214 instance Gram_Term_AtomsT meta ts (Proxy IO) g
 215 instance Gram_Term_AtomsT meta ts (Proxy IO.Handle) g
 216 instance Gram_Term_AtomsT meta ts (Proxy IO.IOMode) g