{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# OPTIONS_GHC -fconstraint-solver-iterations=5 #-}
-- | Symantic for 'IO'.
module Language.Symantic.Lib.IO where
-import Control.Monad (liftM, liftM2)
-import Data.MonoTraversable (MonoFunctor)
-import Data.Proxy
-import Data.Type.Equality ((:~:)(Refl))
+import qualified Data.MonoTraversable as MT
import qualified System.IO as IO
-import Language.Symantic.Parsing
-import Language.Symantic.Typing
-import Language.Symantic.Compiling
-import Language.Symantic.Interpreting
-import Language.Symantic.Transforming
-import Language.Symantic.Lib.Lambda
-import Language.Symantic.Lib.MonoFunctor (TyFam_MonoElement(..))
+import Language.Symantic
+import Language.Symantic.Lib.Char (tyString)
+import Language.Symantic.Lib.MonoFunctor (Element)
+import Language.Symantic.Lib.Unit (tyUnit)
-- * Class 'Sym_IO'
-class Sym_IO term where
+type instance Sym IO = Sym_IO
+type instance Sym IO.Handle = Sym_IO_Handle
+type instance Sym IO.IOMode = Sym_IO_Mode
+class Sym_IO (term:: * -> *)
+class Sym_IO_Handle (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)
+ default io_hClose :: Sym_IO_Handle (UnT term) => Trans term => term IO.Handle -> term (IO ())
+ default io_openFile :: Sym_IO_Handle (UnT term) => Trans term => term IO.FilePath -> term IO.IOMode -> term (IO IO.Handle)
- io_hClose = trans_map1 io_hClose
- io_openFile = trans_map2 io_openFile
-class Sym_IO_Handle (term:: * -> *)
-class Sym_IO_IOMode (term:: * -> *)
+ io_hClose = trans1 io_hClose
+ io_openFile = trans2 io_openFile
+class Sym_IO_Mode (term:: * -> *)
-type instance Sym_of_Iface (Proxy IO) = Sym_IO
-type instance Sym_of_Iface (Proxy IO.Handle) = Sym_IO_Handle
-type instance Sym_of_Iface (Proxy IO.IOMode) = Sym_IO_IOMode
-type instance TyConsts_of_Iface (Proxy IO) = Proxy IO ': TyConsts_imported_by (Proxy IO)
-type instance TyConsts_of_Iface (Proxy IO.Handle) = Proxy IO.Handle ': TyConsts_imported_by (Proxy IO.Handle)
-type instance TyConsts_of_Iface (Proxy IO.IOMode) = Proxy IO.IOMode ': TyConsts_imported_by (Proxy IO.IOMode)
-type instance TyConsts_imported_by (Proxy IO) =
- [ Proxy IO.Handle
- , Proxy IO.IOMode
- , Proxy Applicative
- , Proxy Functor
- , Proxy Monad
- , Proxy MonoFunctor
- ]
-type instance TyConsts_imported_by (Proxy IO.Handle) =
- '[ Proxy Eq
- ]
-type instance TyConsts_imported_by (Proxy IO.IOMode) =
- [ Proxy Enum
- , Proxy Eq
- , Proxy Ord
- ]
+-- Interpreting
+instance Sym_IO Eval
+instance Sym_IO_Handle Eval where
+ io_hClose = eval1 IO.hClose
+ io_openFile = eval2 IO.openFile
+instance Sym_IO_Mode Eval
-instance Sym_IO HostI where
- io_hClose = liftM IO.hClose
- io_openFile = liftM2 IO.openFile
-instance Sym_IO_Handle HostI
-instance Sym_IO_IOMode HostI
-instance Sym_IO TextI where
- io_hClose = textI1 "IO.hClose"
- io_openFile = textI2 "IO.openFile"
-instance Sym_IO_Handle TextI
-instance Sym_IO_IOMode TextI
-instance (Sym_IO r1, Sym_IO r2) => Sym_IO (DupI r1 r2) where
- io_hClose = dupI1 @Sym_IO io_hClose
- io_openFile = dupI2 @Sym_IO io_openFile
-instance Sym_IO_Handle (DupI r1 r2)
-instance Sym_IO_IOMode (DupI r1 r2)
+instance Sym_IO View
+instance Sym_IO_Handle View where
+ io_hClose = view1 "IO.hClose"
+ io_openFile = view2 "IO.openFile"
+instance Sym_IO_Mode View
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs IO
- ) => Read_TyNameR TyName cs (Proxy IO ': rs) where
- read_TyNameR _cs (TyName "IO") k = k (ty @IO)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs IO.Handle
- ) => Read_TyNameR TyName cs (Proxy IO.Handle ': rs) where
- read_TyNameR _cs (TyName "IO.Handle") k = k (ty @IO.Handle)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
-instance
- ( Read_TyNameR TyName cs rs
- , Inj_TyConst cs IO.IOMode
- ) => Read_TyNameR TyName cs (Proxy IO.IOMode ': rs) where
- read_TyNameR _cs (TyName "IO.Mode") k = k (ty @IO.IOMode)
- read_TyNameR _rs raw k = read_TyNameR (Proxy @rs) raw k
+instance Sym_IO (Dup r1 r2)
+instance (Sym_IO_Handle r1, Sym_IO_Handle r2) => Sym_IO_Handle (Dup r1 r2) where
+ io_hClose = dup1 @Sym_IO_Handle io_hClose
+ io_openFile = dup2 @Sym_IO_Handle io_openFile
+instance Sym_IO_Mode (Dup r1 r2)
-instance Show_TyConst cs => Show_TyConst (Proxy IO ': cs) where
- show_TyConst TyConstZ{} = "IO"
- show_TyConst (TyConstS c) = show_TyConst c
-instance Show_TyConst cs => Show_TyConst (Proxy IO.Handle ': cs) where
- show_TyConst TyConstZ{} = "IO.Handle"
- show_TyConst (TyConstS c) = show_TyConst c
-instance Show_TyConst cs => Show_TyConst (Proxy IO.IOMode ': cs) where
- show_TyConst TyConstZ{} = "IO.IOMode"
- show_TyConst (TyConstS c) = show_TyConst c
+-- Transforming
+instance (Sym_IO term, Sym_Lambda term) => Sym_IO (BetaT term)
+instance (Sym_IO_Handle term, Sym_Lambda term) => Sym_IO_Handle (BetaT term)
+instance (Sym_IO_Mode term, Sym_Lambda term) => Sym_IO_Mode (BetaT term)
-instance -- Proj_TyFamC TyFam_MonoElement IO
- ( Proj_TyConst cs IO
- ) => Proj_TyFamC cs TyFam_MonoElement IO where
- proj_TyFamC _c _fam ((TyConst c :$ ty_a) `TypesS` TypesZ)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @IO)
- = Just ty_a
- proj_TyFamC _c _fam _ty = Nothing
-instance -- Proj_TyFamC TyFam_MonoElement IO.Handle
- Proj_TyFamC cs TyFam_MonoElement IO.Handle
-instance -- Proj_TyFamC TyFam_MonoElement IO.IOMode
- Proj_TyFamC cs TyFam_MonoElement IO.IOMode
-
-instance -- Proj_TyConC IO
- ( Proj_TyConst cs IO
- , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO))
- ) => Proj_TyConC cs (Proxy IO) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @IO)
+-- Typing
+instance NameTyOf IO where
+ nameTyOf _c = ["IO"] `Mod` "IO"
+instance NameTyOf IO.Handle where
+ nameTyOf _c = ["IO"] `Mod` "Handle"
+instance NameTyOf IO.IOMode where
+ nameTyOf _c = ["IO"] `Mod` "IOMode"
+instance FixityOf IO
+instance ClassInstancesFor IO where
+ proveConstraintFor _ (TyApp _ (TyConst _ _ q) z)
+ | Just HRefl <- proj_ConstKiTy @_ @IO z
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Applicative) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Functor) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Monad) -> Just TyCon
+ _ | Just Refl <- proj_Const @Applicative q -> Just Dict
+ | Just Refl <- proj_Const @Functor q -> Just Dict
+ | Just Refl <- proj_Const @Monad q -> Just Dict
_ -> Nothing
- proj_TyConC _ (TyConst q :$ (TyConst c :$ _a))
- | Just Refl <- eq_skind (kind_of_TyConst c) (SKiType `SKiArrow` SKiType)
- , Just Refl <- proj_TyConst c (Proxy @IO)
+ proveConstraintFor _ (TyApp _ q (TyApp _ z _a))
+ | Just HRefl <- proj_ConstKiTy @_ @IO z
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @MonoFunctor) -> Just TyCon
+ _ | Just Refl <- proj_ConstTy @MT.MonoFunctor q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-instance -- Proj_TyConC IO.Handle
- ( Proj_TyConst cs IO.Handle
- , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO.Handle))
- ) => Proj_TyConC cs (Proxy IO.Handle) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
- , Just Refl <- proj_TyConst c (Proxy @IO.Handle)
+ proveConstraintFor _c _q = Nothing
+instance ClassInstancesFor IO.Handle where
+ proveConstraintFor _ (TyApp _ q z)
+ | Just HRefl <- proj_ConstKiTy @_ @IO.Handle z
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
+ _ | Just Refl <- proj_ConstTy @Eq q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-instance -- Proj_TyConC IO.IOMode
- ( Proj_TyConst cs IO.IOMode
- , Proj_TyConsts cs (TyConsts_imported_by (Proxy IO.IOMode))
- ) => Proj_TyConC cs (Proxy IO.IOMode) where
- proj_TyConC _ (TyConst q :$ TyConst c)
- | Just Refl <- eq_skind (kind_of_TyConst c) SKiType
- , Just Refl <- proj_TyConst c (Proxy @IO.IOMode)
+ proveConstraintFor _c _q = Nothing
+instance ClassInstancesFor IO.IOMode where
+ proveConstraintFor _ (TyApp _ (TyConst _ _ q) c)
+ | Just HRefl <- proj_ConstKiTy @_ @IO.IOMode c
= case () of
- _ | Just Refl <- proj_TyConst q (Proxy @Enum) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Eq) -> Just TyCon
- | Just Refl <- proj_TyConst q (Proxy @Ord) -> Just TyCon
+ _ | Just Refl <- proj_Const @Enum q -> Just Dict
+ | Just Refl <- proj_Const @Eq q -> Just Dict
+ | Just Refl <- proj_Const @Ord q -> Just Dict
_ -> Nothing
- proj_TyConC _c _q = Nothing
-data instance TokenT meta (ts::[*]) (Proxy IO)
- = Token_Term_IO_hClose (EToken meta ts)
- | Token_Term_IO_openFile (EToken meta ts)
-data instance TokenT meta (ts::[*]) (Proxy IO.Handle)
-data instance TokenT meta (ts::[*]) (Proxy IO.IOMode)
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IO))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO))
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IO.Handle))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.Handle))
-deriving instance Eq_Token meta ts => Eq (TokenT meta ts (Proxy IO.IOMode))
-deriving instance Show_Token meta ts => Show (TokenT meta ts (Proxy IO.IOMode))
+ proveConstraintFor _c _q = Nothing
+instance TypeInstancesFor IO where
+ expandFamFor _c _len f (TyApp _ z a `TypesS` TypesZ)
+ | Just HRefl <- proj_ConstKi @_ @Element f
+ , Just HRefl <- proj_ConstKiTy @_ @IO z
+ = Just a
+ expandFamFor _c _len _fam _as = Nothing
+instance TypeInstancesFor IO.Handle
+instance TypeInstancesFor IO.IOMode
+
+-- Compiling
+instance ModuleFor src ss IO
+instance (Source src, SymInj ss IO.Handle) => ModuleFor src ss IO.Handle where
+ moduleFor = ["IO"] `moduleWhere`
+ [ "hClose" := teIO_hClose
+ , "openFile" := teIO_openFile
+ ]
+instance ModuleFor src ss IO.IOMode
+instance Gram_Term_AtomsFor src ss g IO
+instance Gram_Term_AtomsFor src ss g IO.Handle
+instance Gram_Term_AtomsFor src ss g IO.IOMode
+
+-- ** 'Type's
+tyIO :: Source src => Type src vs a -> Type src vs (IO a)
+tyIO a = tyConstLen @(K IO) @IO (lenVars a) `tyApp` a
+
+tyIO_Handle :: Source src => LenInj vs => Type src vs IO.Handle
+tyIO_Handle = tyConst @(K IO.Handle) @IO.Handle
+
+tyIO_Mode :: Source src => LenInj vs => Type src vs IO.IOMode
+tyIO_Mode = tyConst @(K IO.IOMode) @IO.IOMode
+
+tyFilePath :: Source src => LenInj vs => Type src vs FilePath
+tyFilePath = tyString
+
+-- ** 'Term's
+teIO_hClose :: TermDef IO.Handle '[] (() #> (IO.Handle -> IO ()))
+teIO_hClose = Term noConstraint (tyIO_Handle ~> tyIO tyUnit) $ teSym @IO.Handle $ lam1 io_hClose
-instance -- CompileI IO
- ( Inj_TyConst cs IO
- , Inj_TyConst cs IO.Handle
- , Inj_TyConst cs []
- , Inj_TyConst cs Char
- , Inj_TyConst cs IO.IOMode
- , Inj_TyConst cs (->)
- , Inj_TyConst cs ()
- , Compile cs is
- ) => CompileI cs 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_TyEq
- (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_TyEq
- (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
-instance CompileI cs is (Proxy IO.Handle) where
- compileI tok _ctx _k = case tok of _ -> undefined
-instance CompileI cs is (Proxy IO.IOMode) where
- compileI tok _ctx _k = case tok of _ -> undefined
-instance -- TokenizeT IO
- Inj_Token meta ts IO =>
- TokenizeT meta ts (Proxy IO) where
- tokenizeT _t = mempty
- { tokenizers_infix = tokenizeTMod [Mod_Name "IO"]
- [ tokenize1 "hClose" infixN5 Token_Term_IO_hClose
- , tokenize1 "openFile" infixN5 Token_Term_IO_openFile
- ]
- }
-instance TokenizeT meta ts (Proxy IO.Handle)
-instance TokenizeT meta ts (Proxy IO.IOMode)
-instance Gram_Term_AtomsT meta ts (Proxy IO) g
-instance Gram_Term_AtomsT meta ts (Proxy IO.Handle) g
-instance Gram_Term_AtomsT meta ts (Proxy IO.IOMode) g
+teIO_openFile :: TermDef IO.Handle '[] (() #> (FilePath -> IO.IOMode -> IO (IO.Handle)))
+teIO_openFile = Term noConstraint (tyFilePath ~> tyIO_Mode ~> tyIO tyIO_Handle) $ teSym @IO.Handle $ lam2 io_openFile
sourcephile / git / haskell / symantic.git / blobdiff