← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring

« back to all changes in this revision

Viewing changes to src/IO/Primitive.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-04-10 10:30:20 UTC
  • mfrom: (2.1.7 experimental)
  • Revision ID: package-import@ubuntu.com-20130410103020-bcspfz3whyy5iafu
Tags: 0.7-1
* [6d52289] Imported Upstream version 0.7
* [54104d0] Update Depends and Build-Depends for this version, compatible
  with Agda 2.3.2
* [b3ddce4] No need for the .install file to be executable (thanks lintian)
* [a9a6cb7] Standards-Version → 3.9.4, no changes required

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/IO/Primitive.agda
6
6
 
7
7
module IO.Primitive where
8
8
 
 
9
open import Data.Char
9
10
open import Data.String
10
 
open import Data.Char
11
11
open import Foreign.Haskell
12
12
 
13
13
------------------------------------------------------------------------
32
32
------------------------------------------------------------------------
33
33
-- Simple lazy IO
34
34
 
 
35
-- Note that the functions below produce commands which, when
 
36
-- executed, may raise exceptions.
 
37
 
 
38
-- Note also that the semantics of these functions depends on the
 
39
-- version of the Haskell base library. If the version is 4.2.0.0 (or
 
40
-- later?), then the functions use the character encoding specified by
 
41
-- the locale. For older versions of the library (going back to at
 
42
-- least version 3) the functions use ISO-8859-1.
35
43
 
36
44
postulate
37
45
  getContents : IO Costring
46
49
  putStr      : Costring → IO Unit
47
50
  putStrLn    : Costring → IO Unit
48
51
 
49
 
{-# COMPILED getContents getContents #-}
50
 
{-# COMPILED readFile    readFile    #-}
51
 
{-# COMPILED writeFile   writeFile   #-}
52
 
{-# COMPILED appendFile  appendFile  #-}
53
 
{-# COMPILED putStr      putStr      #-}
54
 
{-# COMPILED putStrLn    putStrLn    #-}
 
52
  -- Reads a finite file. Raises an exception if the file path refers
 
53
  -- to a non-physical file (like "/dev/zero").
 
54
 
 
55
  readFiniteFile : String → IO String
 
56
 
 
57
{-# COMPILED getContents    getContents           #-}
 
58
{-# COMPILED readFile       readFile              #-}
 
59
{-# COMPILED writeFile      writeFile             #-}
 
60
{-# COMPILED appendFile     appendFile            #-}
 
61
{-# COMPILED putStr         putStr                #-}
 
62
{-# COMPILED putStrLn       putStrLn              #-}
 
63
{-# COMPILED readFiniteFile IO.FFI.readFiniteFile #-}