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 (Proxy IO)        = Sym_IO
  16 type instance Sym (Proxy IO.Handle) = Sym_IO_Handle
  17 type instance Sym (Proxy 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 FixityOf IO
  56 instance ClassInstancesFor IO where
  57         proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
  58          | Just HRefl <- proj_ConstKiTy @_ @IO z
  59          = case () of
  60                  _ | Just Refl <- proj_Const @Applicative q -> Just Dict
  61                    | Just Refl <- proj_Const @Functor     q -> Just Dict
  62                    | Just Refl <- proj_Const @Monad       q -> Just Dict
  63                  _ -> Nothing
  64         proveConstraintFor _ (TyApp _ q (TyApp _ z _a))
  65          | Just HRefl <- proj_ConstKiTy @_ @IO z
  66          = case () of
  67                  _ | Just Refl <- proj_ConstTy @MT.MonoFunctor q -> Just Dict
  68                  _ -> Nothing
  69         proveConstraintFor _c _q = Nothing
  70 instance ClassInstancesFor IO.Handle where
  71         proveConstraintFor _ (TyApp _ q z)
  72          | Just HRefl <- proj_ConstKiTy @_ @IO.Handle z
  73          = case () of
  74                  _ | Just Refl <- proj_ConstTy @Eq q -> Just Dict
  75                  _ -> Nothing
  76         proveConstraintFor _c _q = Nothing
  77 instance ClassInstancesFor IO.IOMode where
  78         proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
  79          | Just HRefl <- proj_ConstKiTy @_ @IO.IOMode c
  80          = case () of
  81                  _ | Just Refl <- proj_Const @Enum q -> Just Dict
  82                    | Just Refl <- proj_Const @Eq   q -> Just Dict
  83                    | Just Refl <- proj_Const @Ord  q -> Just Dict
  84                  _ -> Nothing
  85         proveConstraintFor _c _q = Nothing
  86 instance TypeInstancesFor IO where
  87         expandFamFor _c _len f (TyApp _ z a `TypesS` TypesZ)
  88          | Just HRefl <- proj_ConstKi @_ @Element f
  89          , Just HRefl <- proj_ConstKiTy @_ @IO z
  90          = Just a
  91         expandFamFor _c _len _fam _as = Nothing
  92 instance TypeInstancesFor IO.Handle
  93 instance TypeInstancesFor IO.IOMode
  94
  95 -- Compiling
  96 instance ModuleFor src ss IO
  97 instance (Source src, Inj_Sym ss IO.Handle) => ModuleFor src ss IO.Handle where
  98         moduleFor _s = ["IO"] `moduleWhere`
  99          [ "hClose"   := teIO_hClose
 100          , "openFile" := teIO_openFile
 101          ]
 102 instance ModuleFor src ss IO.IOMode
 103 instance Gram_Term_AtomsFor src ss g IO
 104 instance Gram_Term_AtomsFor src ss g IO.Handle
 105 instance Gram_Term_AtomsFor src ss g IO.IOMode
 106
 107 -- ** 'Type's
 108 tyIO :: Source src => Type src vs a -> Type src vs (IO a)
 109 tyIO a = tyConstLen @(K IO) @IO (lenVars a) `tyApp` a
 110
 111 tyIO_Handle :: Source src => Inj_Len vs => Type src vs IO.Handle
 112 tyIO_Handle = tyConst @(K IO.Handle) @IO.Handle
 113
 114 tyIO_Mode :: Source src => Inj_Len vs => Type src vs IO.IOMode
 115 tyIO_Mode = tyConst @(K IO.IOMode) @IO.IOMode
 116
 117 tyFilePath :: Source src => Inj_Len vs => Type src vs FilePath
 118 tyFilePath = tyString
 119
 120 -- ** 'Term's
 121 teIO_hClose :: TermDef IO.Handle '[] (IO.Handle -> IO ())
 122 teIO_hClose = Term noConstraint (tyIO_Handle ~> tyIO tyUnit) $ teSym @IO.Handle $ lam1 io_hClose
 123
 124 teIO_openFile :: TermDef IO.Handle '[] (FilePath -> IO.IOMode -> IO (IO.Handle))
 125 teIO_openFile = Term noConstraint (tyFilePath ~> tyIO_Mode ~> tyIO tyIO_Handle) $ teSym @IO.Handle $ lam2 io_openFile