blob: e11be0e569d45b1a867d603b6ef4152f016d3b4f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive IO: simple bindings to Haskell types and functions
------------------------------------------------------------------------
module IO.Primitive where
open import Codata.Musical.Costring
open import Data.Char.Base
open import Data.String.Base
open import Foreign.Haskell
------------------------------------------------------------------------
-- The IO monad
open import Agda.Builtin.IO public using (IO)
infixl 1 _>>=_
postulate
return : ∀ {a} {A : Set a} → A → IO A
_>>=_ : ∀ {a b} {A : Set a} {B : Set b} → IO A → (A → IO B) → IO B
{-# COMPILE GHC return = \_ _ -> return #-}
{-# COMPILE GHC _>>=_ = \_ _ _ _ -> (>>=) #-}
{-# COMPILE UHC return = \_ _ x -> UHC.Agda.Builtins.primReturn x #-}
{-# COMPILE UHC _>>=_ = \_ _ _ _ x y -> UHC.Agda.Builtins.primBind x y #-}
------------------------------------------------------------------------
-- Simple lazy IO
-- Note that the functions below produce commands which, when
-- executed, may raise exceptions.
-- Note also that the semantics of these functions depends on the
-- version of the Haskell base library. If the version is 4.2.0.0 (or
-- later?), then the functions use the character encoding specified by
-- the locale. For older versions of the library (going back to at
-- least version 3) the functions use ISO-8859-1.
{-# FOREIGN GHC import qualified Data.Text #-}
{-# FOREIGN GHC import qualified Data.Text.IO #-}
{-# FOREIGN GHC import qualified System.IO #-}
{-# FOREIGN GHC import qualified Control.Exception #-}
postulate
getContents : IO Costring
readFile : String → IO Costring
writeFile : String → Costring → IO Unit
appendFile : String → Costring → IO Unit
putStr : Costring → IO Unit
putStrLn : Costring → IO Unit
-- Reads a finite file. Raises an exception if the file path refers
-- to a non-physical file (like "/dev/zero").
readFiniteFile : String → IO String
{-# FOREIGN GHC
readFiniteFile :: Data.Text.Text -> IO Data.Text.Text
readFiniteFile f = do
h <- System.IO.openFile (Data.Text.unpack f) System.IO.ReadMode
Control.Exception.bracketOnError (return ()) (\_ -> System.IO.hClose h)
(\_ -> System.IO.hFileSize h)
Data.Text.IO.hGetContents h
fromColist :: MAlonzo.Code.Codata.Musical.Colist.AgdaColist a -> [a]
fromColist MAlonzo.Code.Codata.Musical.Colist.Nil = []
fromColist (MAlonzo.Code.Codata.Musical.Colist.Cons x xs) =
x : fromColist (MAlonzo.RTE.flat xs)
toColist :: [a] -> MAlonzo.Code.Codata.Musical.Colist.AgdaColist a
toColist [] = MAlonzo.Code.Codata.Musical.Colist.Nil
toColist (x : xs) =
MAlonzo.Code.Codata.Musical.Colist.Cons x (MAlonzo.RTE.Sharp (toColist xs))
#-}
{-# COMPILE GHC getContents = fmap toColist getContents #-}
{-# COMPILE GHC readFile = fmap toColist . readFile . Data.Text.unpack #-}
{-# COMPILE GHC writeFile = \x -> writeFile (Data.Text.unpack x) . fromColist #-}
{-# COMPILE GHC appendFile = \x -> appendFile (Data.Text.unpack x) . fromColist #-}
{-# COMPILE GHC putStr = putStr . fromColist #-}
{-# COMPILE GHC putStrLn = putStrLn . fromColist #-}
{-# COMPILE GHC readFiniteFile = readFiniteFile #-}
{-# COMPILE UHC getContents = UHC.Agda.Builtins.primGetContents #-}
{-# COMPILE UHC readFile = UHC.Agda.Builtins.primReadFile #-}
{-# COMPILE UHC writeFile = UHC.Agda.Builtins.primWriteFile #-}
{-# COMPILE UHC appendFile = UHC.Agda.Builtins.primAppendFile #-}
{-# COMPILE UHC putStr = UHC.Agda.Builtins.primPutStr #-}
{-# COMPILE UHC putStrLn = UHC.Agda.Builtins.primPutStrLn #-}
{-# COMPILE UHC readFiniteFile = UHC.Agda.Builtins.primReadFiniteFile #-}
|