/usr/share/agda-stdlib/IO/Primitive.agda is in agda-stdlib 0.7-2.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 | ------------------------------------------------------------------------
-- The Agda standard library
--
-- Primitive IO: simple bindings to Haskell types and functions
------------------------------------------------------------------------
module IO.Primitive where
open import Data.Char
open import Data.String
open import Foreign.Haskell
------------------------------------------------------------------------
-- The IO monad
postulate
IO : ∀ {ℓ} → Set ℓ → Set ℓ
{-# IMPORT IO.FFI #-}
{-# COMPILED_TYPE IO IO.FFI.AgdaIO #-}
{-# BUILTIN IO 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
{-# COMPILED return (\_ _ -> return) #-}
{-# COMPILED _>>=_ (\_ _ _ _ -> (>>=)) #-}
------------------------------------------------------------------------
-- 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.
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
{-# COMPILED getContents getContents #-}
{-# COMPILED readFile readFile #-}
{-# COMPILED writeFile writeFile #-}
{-# COMPILED appendFile appendFile #-}
{-# COMPILED putStr putStr #-}
{-# COMPILED putStrLn putStrLn #-}
{-# COMPILED readFiniteFile IO.FFI.readFiniteFile #-}
|