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