← Back to branch summary

~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

Viewing changes to examples/outdated-and-incorrect/fileIO/IO/File.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/outdated-and-incorrect/fileIO/IO/File.agda
1
 
 
2
 
module IO.File where
3
 
 
4
 
open import Base
5
 
open import IO
6
 
 
7
 
{-# IMPORT System.IO #-}
8
 
 
9
 
FilePath = String
10
 
 
11
 
data IOMode : Set where
12
 
  readMode      : IOMode
13
 
  writeMode     : IOMode
14
 
  appendMode    : IOMode
15
 
  readWriteMode : IOMode
16
 
 
17
 
{-# COMPILED_DATA IOMode ReadMode WriteMode AppendMode ReadWriteMode #-}
18
 
 
19
 
canRead : IOMode -> Bool
20
 
canRead readMode      = true
21
 
canRead writeMode     = false
22
 
canRead appendMode    = false
23
 
canRead readWriteMode = true
24
 
 
25
 
canWrite : IOMode -> Bool
26
 
canWrite readMode      = false
27
 
canWrite writeMode     = true
28
 
canWrite appendMode    = true
29
 
canWrite readWriteMode = true
30
 
 
31
 
CanRead : IOMode -> Set
32
 
CanRead m = IsTrue (canRead m)
33
 
 
34
 
CanWrite : IOMode -> Set
35
 
CanWrite m = IsTrue (canWrite m)
36
 
 
37
 
postulate
38
 
  Handle : Set
39
 
 
40
 
private
41
 
 postulate
42
 
  hs-openFile : FilePath -> IOMode -> IO Handle
43
 
  hs-hClose   : Handle -> IO Unit
44
 
 
45
 
  hs-hGetChar : Handle -> IO Char
46
 
  hs-hGetLine : Handle -> IO String
47
 
  hs-hGetContents : Handle -> IO String
48
 
 
49
 
  hs-hPutStr  : Handle -> String -> IO Unit
50
 
 
51
 
{-# COMPILED hs-openFile     openFile #-}
52
 
{-# COMPILED hs-hClose       hClose #-}
53
 
{-# COMPILED hs-hGetChar     hGetChar #-}
54
 
{-# COMPILED hs-hGetLine     hGetLine #-}
55
 
{-# COMPILED hs-hGetContents hGetContents #-}
56
 
{-# COMPILED hs-hPutStr      hPutStr #-}
57
 
 
58
 
Handles = List (Handle × IOMode)
59
 
 
60
 
abstract
61
 
 -- The FileIO monad. Records the list of open handles before and after
62
 
 -- a computation. The open handles after the computation may depend on
63
 
 -- the computed value.
64
 
 data FileIO (A : Set)(hs₁ : Handles)(hs₂ : A -> Handles) : Set where
65
 
   fileIO : IO A -> FileIO A hs₁ hs₂
66
 
 
67
 
private
68
 
 abstract
69
 
  unFileIO : forall {A hs f} -> FileIO A hs f -> IO A
70
 
  unFileIO (fileIO io) = io
71
 
 
72
 
FileIO₋ : Set -> Handles -> Handles -> Set
73
 
FileIO₋ A hs₁ hs₂ = FileIO A hs₁ (\_ -> hs₂)
74
 
 
75
 
abstract
76
 
  openFile : {hs : Handles} -> FilePath -> (m : IOMode) ->
77
 
             FileIO Handle hs (\h -> (h , m) :: hs)
78
 
  openFile file mode = fileIO (hs-openFile file mode)
79
 
 
80
 
infix 30 _∈_
81
 
data _∈_ {A : Set}(x : A) : List A -> Set where
82
 
  hd : forall {xs} -> x ∈ x :: xs
83
 
  tl : forall {y xs} -> x ∈ xs -> x ∈ y :: xs
84
 
 
85
 
delete : {A : Set}{x : A}(xs : List A) -> x ∈ xs -> List A
86
 
delete [] ()
87
 
delete (x :: xs)  hd    = xs
88
 
delete (x :: xs) (tl p) = x :: delete xs p
89
 
 
90
 
abstract
91
 
  hClose : {hs : Handles}{m : IOMode}(h : Handle)(p : (h , m) ∈ hs) ->
92
 
           FileIO₋ Unit hs (delete hs p)
93
 
  hClose h _ = fileIO (hs-hClose h)
94
 
 
95
 
  hGetLine : {hs : Handles}{m : IOMode}{isRead : CanRead m}(h : Handle)
96
 
             (p : (h , m) ∈ hs) -> FileIO₋ String hs hs
97
 
  hGetLine h _ = fileIO (hs-hGetLine h)
98
 
 
99
 
  hGetContents : {hs : Handles}{m : IOMode}{isRead : CanRead m}(h : Handle)
100
 
             (p : (h , m) ∈ hs) -> FileIO₋ String hs (delete hs p)
101
 
  hGetContents h _ = fileIO (hs-hGetContents h)
102
 
 
103
 
abstract
104
 
  -- You can only run file computations that don't leave any open
105
 
  -- handles.
106
 
  runFileIO : {A : Set} -> FileIO₋ A [] [] -> IO A
107
 
  runFileIO (fileIO m) = m
108
 
 
109
 
abstract
110
 
  _>>=_ : forall {A B hs f g} ->
111
 
          FileIO A hs f -> ((x : A) -> FileIO B (f x) g) -> FileIO B hs g
112
 
  fileIO m >>= k = fileIO (bindIO m \x -> unFileIO (k x))
113
 
 
114
 
  return : forall {A hs} -> A -> FileIO₋ A hs hs
115
 
  return x = fileIO (returnIO x)