]> Git — Sourcephile - haskell/symantic.git/blob - symantic-lib/Language/Symantic/Lib/IO.hs
Clarification : Megaparsec integration.
[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 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