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