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

   1 {-# LANGUAGE UndecidableInstances #-}
   2 {-# OPTIONS_GHC -fno-warn-orphans #-}
   3 -- | Symantic for 'IO'.
   4 module Language.Symantic.Lib.IO where
   5
   6 import Control.Applicative (Applicative)
   7 import Control.Monad (Monad)
   8 import Data.Eq (Eq)
   9 import Data.Function (($))
  10 import Data.Functor (Functor)
  11 import Data.Maybe (Maybe(..))
  12 import Data.Ord (Ord)
  13 import Prelude (Enum)
  14 import System.IO (IO, FilePath)
  15 import qualified Data.MonoTraversable as MT
  16 import qualified System.IO as IO
  17
  18 import Language.Symantic
  19 import Language.Symantic.Lib.Char (tyString)
  20 import Language.Symantic.Lib.MonoFunctor (Element)
  21 import Language.Symantic.Lib.Unit (tyUnit)
  22
  23 -- * Class 'Sym_IO'
  24 type instance Sym IO        = Sym_IO
  25 type instance Sym IO.Handle = Sym_IO_Handle
  26 type instance Sym IO.IOMode = Sym_IO_Mode
  27 class Sym_IO (term:: * -> *)
  28 class Sym_IO_Handle (term:: * -> *) where
  29         io_hClose   :: term IO.Handle -> term (IO ())
  30         io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
  31
  32         default io_hClose   :: Sym_IO_Handle (UnT term) => Trans term => term IO.Handle -> term (IO ())
  33         default io_openFile :: Sym_IO_Handle (UnT term) => Trans term => term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
  34
  35         io_hClose   = trans1 io_hClose
  36         io_openFile = trans2 io_openFile
  37 class Sym_IO_Mode (term:: * -> *)
  38
  39 -- Interpreting
  40 instance Sym_IO Eval
  41 instance Sym_IO_Handle Eval where
  42         io_hClose   = eval1 IO.hClose
  43         io_openFile = eval2 IO.openFile
  44 instance Sym_IO_Mode Eval
  45
  46 instance Sym_IO View
  47 instance Sym_IO_Handle View where
  48         io_hClose   = view1 "IO.hClose"
  49         io_openFile = view2 "IO.openFile"
  50 instance Sym_IO_Mode View
  51
  52 instance Sym_IO (Dup r1 r2)
  53 instance (Sym_IO_Handle r1, Sym_IO_Handle r2) => Sym_IO_Handle (Dup r1 r2) where
  54         io_hClose   = dup1 @Sym_IO_Handle io_hClose
  55         io_openFile = dup2 @Sym_IO_Handle io_openFile
  56 instance Sym_IO_Mode (Dup r1 r2)
  57
  58 -- Transforming
  59 instance (Sym_IO term, Sym_Lambda term) => Sym_IO (BetaT term)
  60 instance (Sym_IO_Handle term, Sym_Lambda term) => Sym_IO_Handle (BetaT term)
  61 instance (Sym_IO_Mode term, Sym_Lambda term) => Sym_IO_Mode (BetaT term)
  62
  63 -- Typing
  64 instance NameTyOf IO where
  65         nameTyOf _c = ["IO"] `Mod` "IO"
  66 instance NameTyOf IO.Handle where
  67         nameTyOf _c = ["IO"] `Mod` "Handle"
  68 instance NameTyOf IO.IOMode where
  69         nameTyOf _c = ["IO"] `Mod` "IOMode"
  70 instance FixityOf IO
  71 instance ClassInstancesFor IO where
  72         proveConstraintFor _ (TyConst _ _ q :$ z)
  73          | Just HRefl <- proj_ConstKiTy @_ @IO z
  74          = case () of
  75                  _ | Just Refl <- proj_Const @Applicative q -> Just Dict
  76                    | Just Refl <- proj_Const @Functor     q -> Just Dict
  77                    | Just Refl <- proj_Const @Monad       q -> Just Dict
  78                  _ -> Nothing
  79         proveConstraintFor _ (TyConst _ _ q :$ z:@_a)
  80          | Just HRefl <- proj_ConstKiTy @_ @IO z
  81          = case () of
  82                  _ | Just Refl <- proj_Const @MT.MonoFunctor q -> Just Dict
  83                  _ -> Nothing
  84         proveConstraintFor _c _q = Nothing
  85 instance ClassInstancesFor IO.Handle where
  86         proveConstraintFor _ (TyConst _ _ q :$ z)
  87          | Just HRefl <- proj_ConstKiTy @_ @IO.Handle z
  88          = case () of
  89                  _ | Just Refl <- proj_Const @Eq q -> Just Dict
  90                  _ -> Nothing
  91         proveConstraintFor _c _q = Nothing
  92 instance ClassInstancesFor IO.IOMode where
  93         proveConstraintFor _ (TyConst _ _ q :$ c)
  94          | Just HRefl <- proj_ConstKiTy @_ @IO.IOMode c
  95          = case () of
  96                  _ | Just Refl <- proj_Const @Enum q -> Just Dict
  97                    | Just Refl <- proj_Const @Eq   q -> Just Dict
  98                    | Just Refl <- proj_Const @Ord  q -> Just Dict
  99                  _ -> Nothing
 100         proveConstraintFor _c _q = Nothing
 101 instance TypeInstancesFor IO where
 102         expandFamFor _c _len f (z:@a `TypesS` TypesZ)
 103          | Just HRefl <- proj_ConstKi @_ @Element f
 104          , Just HRefl <- proj_ConstKiTy @_ @IO z
 105          = Just a
 106         expandFamFor _c _len _fam _as = Nothing
 107 instance TypeInstancesFor IO.Handle
 108 instance TypeInstancesFor IO.IOMode
 109
 110 -- Compiling
 111 instance ModuleFor src ss IO
 112 instance (Source src, SymInj ss IO.Handle) => ModuleFor src ss IO.Handle where
 113         moduleFor = ["IO"] `moduleWhere`
 114          [ "hClose"   := teIO_hClose
 115          , "openFile" := teIO_openFile
 116          ]
 117 instance ModuleFor src ss IO.IOMode
 118 instance Gram_Term_AtomsFor src ss g IO
 119 instance Gram_Term_AtomsFor src ss g IO.Handle
 120 instance Gram_Term_AtomsFor src ss g IO.IOMode
 121
 122 -- ** 'Type's
 123 tyIO :: Source src => Type src vs a -> Type src vs (IO a)
 124 tyIO a = tyConstLen @(K IO) @IO (lenVars a) `tyApp` a
 125
 126 tyIO_Handle :: Source src => LenInj vs => Type src vs IO.Handle
 127 tyIO_Handle = tyConst @(K IO.Handle) @IO.Handle
 128
 129 tyIO_Mode :: Source src => LenInj vs => Type src vs IO.IOMode
 130 tyIO_Mode = tyConst @(K IO.IOMode) @IO.IOMode
 131
 132 tyFilePath :: Source src => LenInj vs => Type src vs FilePath
 133 tyFilePath = tyString
 134
 135 -- ** 'Term's
 136 teIO_hClose :: TermDef IO.Handle '[] (() #> (IO.Handle -> IO ()))
 137 teIO_hClose = Term noConstraint (tyIO_Handle ~> tyIO tyUnit) $ teSym @IO.Handle $ lam1 io_hClose
 138
 139 teIO_openFile :: TermDef IO.Handle '[] (() #> (FilePath -> IO.IOMode -> IO (IO.Handle)))
 140 teIO_openFile = Term noConstraint (tyFilePath ~> tyIO_Mode ~> tyIO tyIO_Handle) $ teSym @IO.Handle $ lam2 io_openFile