{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-} -- | Symantic for 'IO'. module Language.Symantic.Compiling.IO where import Control.Monad (liftM, liftM2) import Data.Proxy import Data.Text (Text) import Data.Type.Equality ((:~:)(Refl)) import qualified System.IO as IO import Language.Symantic.Parsing import Language.Symantic.Typing import Language.Symantic.Compiling.Term import Language.Symantic.Interpreting import Language.Symantic.Transforming.Trans -- * Class 'Sym_IO' class Sym_IO term where io_hClose :: term IO.Handle -> term (IO ()) io_openFile :: term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle) default io_hClose :: Trans t term => t term IO.Handle -> t term (IO ()) default io_openFile :: Trans t term => t term IO.FilePath -> t term IO.IOMode -> t term (IO IO.Handle) io_hClose = trans_map1 io_hClose io_openFile = trans_map2 io_openFile type instance Sym_of_Iface (Proxy IO) = Sym_IO type instance Consts_of_Iface (Proxy IO) = Proxy IO ': Consts_imported_by IO type instance Consts_imported_by IO = [ Proxy IO.Handle , Proxy IO.IOMode , Proxy Applicative , Proxy Functor , Proxy Monad ] type instance Consts_imported_by IO.Handle = '[ Proxy Eq ] type instance Consts_imported_by IO.IOMode = [ Proxy Enum , Proxy Eq , Proxy Ord ] instance Sym_IO HostI where io_hClose = liftM IO.hClose io_openFile = liftM2 IO.openFile instance Sym_IO TextI where io_hClose = textI1 "IO.hClose" io_openFile = textI2 "IO.openFile" instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where io_hClose = dupI1 (Proxy @Sym_IO) io_hClose io_openFile = dupI2 (Proxy @Sym_IO) io_openFile instance ( Read_TypeNameR Text cs rs , Inj_Const cs IO ) => Read_TypeNameR Text cs (Proxy IO ': rs) where read_typenameR _cs "IO" k = k (ty @IO) read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k instance ( Read_TypeNameR Text cs rs , Inj_Const cs IO.Handle ) => Read_TypeNameR Text cs (Proxy IO.Handle ': rs) where read_typenameR _cs "IO.Handle" k = k (ty @IO.Handle) read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k instance ( Read_TypeNameR Text cs rs , Inj_Const cs IO.IOMode ) => Read_TypeNameR Text cs (Proxy IO.IOMode ': rs) where read_typenameR _cs "IO.Mode" k = k (ty @IO.IOMode) read_typenameR _rs raw k = read_typenameR (Proxy @rs) raw k instance Show_Const cs => Show_Const (Proxy IO ': cs) where show_const ConstZ{} = "IO" show_const (ConstS c) = show_const c instance Show_Const cs => Show_Const (Proxy IO.Handle ': cs) where show_const ConstZ{} = "IO.Handle" show_const (ConstS c) = show_const c instance Show_Const cs => Show_Const (Proxy IO.IOMode ': cs) where show_const ConstZ{} = "IO.IOMode" show_const (ConstS c) = show_const c instance -- Proj_ConC IO ( Proj_Const cs IO , Proj_Consts cs (Consts_imported_by IO) ) => Proj_ConC cs (Proxy IO) where proj_conC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_const c) (SKiType `SKiArrow` SKiType) , Just Refl <- proj_const c (Proxy::Proxy IO) = case () of _ | Just Refl <- proj_const q (Proxy::Proxy Applicative) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Functor) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Monad) -> Just Con _ -> Nothing proj_conC _c _q = Nothing instance -- Proj_ConC IO.Handle ( Proj_Const cs IO.Handle , Proj_Consts cs (Consts_imported_by IO.Handle) ) => Proj_ConC cs (Proxy IO.Handle) where proj_conC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_const c) SKiType , Just Refl <- proj_const c (Proxy::Proxy IO.Handle) = case () of _ | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con _ -> Nothing proj_conC _c _q = Nothing instance -- Proj_ConC IO.IOMode ( Proj_Const cs IO.IOMode , Proj_Consts cs (Consts_imported_by IO.IOMode) ) => Proj_ConC cs (Proxy IO.IOMode) where proj_conC _ (TyConst q :$ TyConst c) | Just Refl <- eq_skind (kind_of_const c) SKiType , Just Refl <- proj_const c (Proxy::Proxy IO.IOMode) = case () of _ | Just Refl <- proj_const q (Proxy::Proxy Enum) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Eq) -> Just Con | Just Refl <- proj_const q (Proxy::Proxy Ord) -> Just Con _ -> Nothing proj_conC _c _q = Nothing data instance TokenT meta (ts::[*]) (Proxy IO) = Token_Term_IO_hClose (EToken meta ts) | Token_Term_IO_openFile (EToken meta ts) deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IO)) deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO)) instance -- CompileI ( Inj_Const (Consts_of_Ifaces is) IO , Inj_Const (Consts_of_Ifaces is) IO.Handle , Inj_Const (Consts_of_Ifaces is) [] , Inj_Const (Consts_of_Ifaces is) Char , Inj_Const (Consts_of_Ifaces is) IO.IOMode , Inj_Const (Consts_of_Ifaces is) (->) , Inj_Const (Consts_of_Ifaces is) () , Compile is ) => CompileI is (Proxy IO) where compileI tok ctx k = case tok of Token_Term_IO_hClose tok_h -> -- hClose :: Handle -> IO () compileO tok_h ctx $ \ty_h (TermO h) -> check_type (At Nothing (ty @IO.Handle)) (At (Just tok_h) ty_h) $ \Refl -> k (ty @IO :$ ty @()) $ TermO $ io_hClose . h Token_Term_IO_openFile tok_fp -> -- openFile :: FilePath -> IOMode -> IO Handle compileO tok_fp ctx $ \ty_fp (TermO fp) -> check_type (At Nothing tyFilePath) (At (Just tok_fp) ty_fp) $ \Refl -> k (ty @IO.IOMode ~> ty @IO :$ ty @IO.Handle) $ TermO $ \c -> lam $ io_openFile (fp c) where tyFilePath = ty @[] :$ ty @Char