Language/Symantic/Type/IO.hs

   1 {-# LANGUAGE FlexibleContexts #-}
   2 {-# LANGUAGE FlexibleInstances #-}
   3 {-# LANGUAGE MultiParamTypeClasses #-}
   4 {-# LANGUAGE PatternSynonyms #-}
   5 {-# LANGUAGE TypeFamilies #-}
   6 {-# OPTIONS_GHC -fno-warn-orphans #-}
   7 module Language.Symantic.Type.IO where
   8
   9 import qualified Data.MonoTraversable as MT
  10 import Data.Proxy
  11 import Data.Type.Equality ((:~:)(Refl))
  12 import qualified System.IO as IO
  13
  14 import Language.Symantic.Type.Root
  15 import Language.Symantic.Type.Type0
  16 import Language.Symantic.Type.Type1
  17
  18 -- * Type 'Type_IO'
  19 -- | The list type.
  20 type Type_IO          = Type_Type1 (Proxy IO)
  21 type Type_IO_Handle   = Type_Type0 (Proxy IO.Handle)
  22 type Type_IO_FilePath = Type_Type0 (Proxy IO.FilePath)
  23 type Type_IO_Mode     = Type_Type0 (Proxy IO.IOMode)
  24
  25 pattern Type_IO :: root a -> Type_IO root (IO a)
  26 pattern Type_IO a = Type_Type1 Proxy a
  27
  28 instance Constraint_Type Eq (Type_IO root)
  29 instance Constraint_Type Ord (Type_IO root)
  30 instance Constraint_Type Monoid (Type_IO root)
  31 instance Constraint_Type Num (Type_IO root)
  32 instance Constraint_Type Integral (Type_IO root)
  33 instance Constraint_Type MT.MonoFunctor (Type_IO root) where
  34         constraint_type _c Type_Type1{} = Just Dict
  35 instance Constraint_Type1 Functor (Type_IO root) where
  36         constraint_type1 _c Type_Type1{} = Just Dict
  37 instance Constraint_Type1 Applicative (Type_IO root) where
  38         constraint_type1 _c Type_Type1{} = Just Dict
  39 instance Constraint_Type1 Monad (Type_IO root) where
  40         constraint_type1 _c Type_Type1{} = Just Dict
  41 instance -- Eq_Type
  42  Eq_Type root =>
  43  Eq_Type (Type_IO root) where
  44         eq_type (Type_Type1 _px1 a1) (Type_Type1 _px2 a2)
  45          | Just Refl <- a1 `eq_type` a2
  46          = Just Refl
  47         eq_type _ _ = Nothing
  48 instance -- Eq_Type1
  49  Eq_Type1 (Type_IO root) where
  50         eq_type1 Type_Type1{} Type_Type1{}
  51          = Just Refl
  52 instance -- String_from_Type
  53  String_from_Type root =>
  54  String_from_Type (Type_IO root) where
  55         string_from_type (Type_Type1 _f a) =
  56                 "[" ++ string_from_type a ++ "]"
  57
  58 -- | Inject 'Type_IO' within a root type.
  59 type_io :: Lift_Type_Root Type_IO root => root h_a -> root (IO h_a)
  60 type_io = type_type1
  61
  62 -- | Inject 'Type_IO_Handle' within a root type.
  63 type_io_handle
  64  :: Lift_Type_Root Type_IO_Handle root
  65  => root IO.Handle
  66 type_io_handle = lift_type_root $ Type_Type0 (Proxy::Proxy IO.Handle)
  67
  68 -- | Inject 'Type_IO_FilePath' within a root type.
  69 type_io_filepath
  70  :: Lift_Type_Root Type_IO_FilePath root
  71  => root IO.FilePath
  72 type_io_filepath = lift_type_root $ Type_Type0 (Proxy::Proxy IO.FilePath)
  73
  74 -- | Inject 'Type_IO_Mode' within a root type.
  75 type_io_mode
  76  :: Lift_Type_Root Type_IO_Mode root
  77  => root IO.IOMode
  78 type_io_mode = lift_type_root $ Type_Type0 (Proxy::Proxy IO.IOMode)