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.Parsing.Grammar
  14 import Language.Symantic.Typing
  15 import Language.Symantic.Compiling
  16 import Language.Symantic.Interpreting
  17 import Language.Symantic.Transforming.Trans
  18 import Language.Symantic.Lib.Lambda
  19
  20 -- * Class 'Sym_IO'
  21 class Sym_IO term where
  22         io_hClose   :: term IO.Handle -> term (IO ())
  23         io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
  24
  25         default io_hClose   :: Trans t term => t term IO.Handle -> t term (IO ())
  26         default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle)
  27
  28         io_hClose   = trans_map1 io_hClose
  29         io_openFile = trans_map2 io_openFile
  30
  31 type instance Sym_of_Iface (Proxy IO) = Sym_IO
  32 type instance Consts_of_Iface (Proxy IO) = Proxy IO ': Consts_imported_by IO
  33 type instance Consts_imported_by IO =
  34  [ Proxy IO.Handle
  35  , Proxy IO.IOMode
  36  , Proxy Applicative
  37  , Proxy Functor
  38  , Proxy Monad
  39  ]
  40 type instance Consts_imported_by IO.Handle =
  41  '[ Proxy Eq
  42  ]
  43 type instance Consts_imported_by IO.IOMode =
  44  [ Proxy Enum
  45  , Proxy Eq
  46  , Proxy Ord
  47  ]
  48
  49 instance Sym_IO HostI where
  50         io_hClose   = liftM IO.hClose
  51         io_openFile = liftM2 IO.openFile
  52 instance Sym_IO TextI where
  53         io_hClose   = textI1 "IO.hClose"
  54         io_openFile = textI2 "IO.openFile"
  55 instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
  56         io_hClose   = dupI1 (Proxy @Sym_IO) io_hClose
  57         io_openFile = dupI2 (Proxy @Sym_IO) io_openFile
  58
  59 instance
  60  ( Read_TypeNameR Type_Name cs rs
  61  , Inj_Const cs IO
  62  ) => Read_TypeNameR Type_Name cs (Proxy IO ': rs) where
  63         read_typenameR _cs (Type_Name "IO") k = k (ty @IO)
  64         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  65 instance
  66  ( Read_TypeNameR Type_Name cs rs
  67  , Inj_Const cs IO.Handle
  68  ) => Read_TypeNameR Type_Name cs (Proxy IO.Handle ': rs) where
  69         read_typenameR _cs (Type_Name "IO.Handle") k = k (ty @IO.Handle)
  70         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  71 instance
  72  ( Read_TypeNameR Type_Name cs rs
  73  , Inj_Const cs IO.IOMode
  74  ) => Read_TypeNameR Type_Name cs (Proxy IO.IOMode ': rs) where
  75         read_typenameR _cs (Type_Name "IO.Mode") k = k (ty @IO.IOMode)
  76         read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k
  77
  78 instance Show_Const cs => Show_Const (Proxy IO ': cs) where
  79         show_const ConstZ{} = "IO"
  80         show_const (ConstS c) = show_const c
  81 instance Show_Const cs => Show_Const (Proxy IO.Handle ': cs) where
  82         show_const ConstZ{} = "IO.Handle"
  83         show_const (ConstS c) = show_const c
  84 instance Show_Const cs => Show_Const (Proxy IO.IOMode ': cs) where
  85         show_const ConstZ{} = "IO.IOMode"
  86         show_const (ConstS c) = show_const c
  87
  88 instance -- Proj_ConC IO
  89  ( Proj_Const cs IO
  90  , Proj_Consts cs (Consts_imported_by IO)
  91  ) => Proj_ConC cs (Proxy IO) where
  92         proj_conC _ (TyConst q :$ TyConst c)
  93          | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType)
  94          , Just Refl <- proj_const c (Proxy @IO)
  95          = case () of
  96                  _ | Just Refl <- proj_const q (Proxy @Applicative) -> Just Con
  97                    | Just Refl <- proj_const q (Proxy @Functor)     -> Just Con
  98                    | Just Refl <- proj_const q (Proxy @Monad)       -> Just Con
  99                  _ -> Nothing
 100         proj_conC _c _q = Nothing
 101 instance -- Proj_ConC IO.Handle
 102  ( Proj_Const cs IO.Handle
 103  , Proj_Consts cs (Consts_imported_by IO.Handle)
 104  ) => Proj_ConC cs (Proxy IO.Handle) where
 105         proj_conC _ (TyConst q :$ TyConst c)
 106          | Just Refl <- eq_skind (kind_of_const c) SKiType
 107          , Just Refl <- proj_const c (Proxy @IO.Handle)
 108          = case () of
 109                  _ | Just Refl <- proj_const q (Proxy @Eq) -> Just Con
 110                  _ -> Nothing
 111         proj_conC _c _q = Nothing
 112 instance -- Proj_ConC IO.IOMode
 113  ( Proj_Const cs IO.IOMode
 114  , Proj_Consts cs (Consts_imported_by IO.IOMode)
 115  ) => Proj_ConC cs (Proxy IO.IOMode) where
 116         proj_conC _ (TyConst q :$ TyConst c)
 117          | Just Refl <- eq_skind (kind_of_const c) SKiType
 118          , Just Refl <- proj_const c (Proxy @IO.IOMode)
 119          = case () of
 120                  _ | Just Refl <- proj_const q (Proxy @Enum) -> Just Con
 121                    | Just Refl <- proj_const q (Proxy @Eq)   -> Just Con
 122                    | Just Refl <- proj_const q (Proxy @Ord)  -> Just Con
 123                  _ -> Nothing
 124         proj_conC _c _q = Nothing
 125 data instance TokenT meta (ts::[*]) (Proxy IO)
 126  = Token_Term_IO_hClose   (EToken meta ts)
 127  | Token_Term_IO_openFile (EToken meta ts)
 128 deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IO))
 129 deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO))
 130 instance -- CompileI
 131  ( Inj_Const (Consts_of_Ifaces is) IO
 132  , Inj_Const (Consts_of_Ifaces is) IO.Handle
 133  , Inj_Const (Consts_of_Ifaces is) []
 134  , Inj_Const (Consts_of_Ifaces is) Char
 135  , Inj_Const (Consts_of_Ifaces is) IO.IOMode
 136  , Inj_Const (Consts_of_Ifaces is) (->)
 137  , Inj_Const (Consts_of_Ifaces is) ()
 138  , Compile is
 139  ) => CompileI is (Proxy IO) where
 140         compileI tok ctx k =
 141                 case tok of
 142                  Token_Term_IO_hClose tok_h ->
 143                         -- hClose :: Handle -> IO ()
 144                         compileO tok_h ctx $ \ty_h (TermO h) ->
 145                         check_type
 146                          (At Nothing (ty @IO.Handle))
 147                          (At (Just tok_h) ty_h) $ \Refl ->
 148                         k (ty @IO :$ ty @()) $ TermO $
 149                                 io_hClose . h
 150                  Token_Term_IO_openFile tok_fp ->
 151                         -- openFile :: FilePath -> IOMode -> IO Handle
 152                         compileO tok_fp ctx $ \ty_fp (TermO fp) ->
 153                         check_type
 154                          (At Nothing tyFilePath)
 155                          (At (Just tok_fp) ty_fp) $ \Refl ->
 156                         k (ty @IO.IOMode ~> ty @IO :$ ty @IO.Handle) $ TermO $
 157                          \c -> lam $ io_openFile (fp c)
 158                 where tyFilePath = ty @[] :$ ty @Char
 159 instance -- TokenizeT
 160  Inj_Token meta ts IO =>
 161  TokenizeT meta ts (Proxy IO) where
 162         tokenizeT _t = mempty
 163          { tokenizers_infix = tokenizeTMod [Mod_Name "IO"]
 164                  [ tokenize1 "hClose"   infixN5 Token_Term_IO_hClose
 165                  , tokenize1 "openFile" infixN5 Token_Term_IO_openFile
 166                  ]
 167          }
 168 instance Gram_Term_AtomsT meta ts (Proxy IO) g