← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda-stdlib/wily

« back to all changes in this revision

Viewing changes to src/IO.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2013-05-27 19:29:25 UTC
  • mfrom: (8.1.1 experimental)
  • Revision ID: package-import@ubuntu.com-20130527192925-q2tadfousmn0xeav
Tags: 0.7-2
Upload to unstable 

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/IO.agda
4
4
-- IO
5
5
------------------------------------------------------------------------
6
6
 
7
 
{-# OPTIONS --no-termination-check #-}
8
 
 
9
7
module IO where
10
8
 
11
9
open import Coinduction
39
37
 
40
38
abstract
41
39
 
 
40
  {-# NO_TERMINATION_CHECK #-}
 
41
 
42
42
  run : ∀ {a} {A : Set a} → IO A → Prim.IO A
43
43
  run (lift m)   = m
44
44
  run (return x) = Prim.return x
73
73
------------------------------------------------------------------------
74
74
-- Simple lazy IO
75
75
 
 
76
-- Note that the functions below produce commands which, when
 
77
-- executed, may raise exceptions.
 
78
 
 
79
-- Note also that the semantics of these functions depends on the
 
80
-- version of the Haskell base library. If the version is 4.2.0.0 (or
 
81
-- later?), then the functions use the character encoding specified by
 
82
-- the locale. For older versions of the library (going back to at
 
83
-- least version 3) the functions use ISO-8859-1.
76
84
 
77
85
getContents : IO Costring
78
86
getContents = lift Prim.getContents
85
88
readFile : String → IO Costring
86
89
readFile f = lift (Prim.readFile f)
87
90
 
 
91
-- Reads a finite file. Raises an exception if the file path refers to
 
92
-- a non-physical file (like "/dev/zero").
 
93
 
 
94
readFiniteFile : String → IO String
 
95
readFiniteFile f = lift (Prim.readFiniteFile f)
 
96
 
88
97
writeFile∞ : String → Costring → IO ⊤
89
98
writeFile∞ f s =
90
99
  ♯ lift (Prim.writeFile f s) >>