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