← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/epic/Prelude/IO.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:
test/epic/Prelude/IO.agda
1
 
module Prelude.IO where
2
 
 
3
 
open import Prelude.Bool
4
 
open import Prelude.Char
5
 
open import Prelude.Nat
6
 
open import Prelude.String
7
 
open import Prelude.Unit
8
 
open import Prelude.Vec
9
 
open import Prelude.Float
10
 
 
11
 
postulate
12
 
  IO : Set → Set
13
 
 
14
 
{-# COMPILED_TYPE IO IO #-}
15
 
 
16
 
infixl 1 _>>=_
17
 
 
18
 
postulate
19
 
  return  : ∀ {A} → A → IO A
20
 
  _>>=_   : ∀ {A B} → IO A → (A → IO B) → IO B
21
 
  numArgs : Nat
22
 
  getArg  : Nat -> String
23
 
 
24
 
args : Vec String numArgs
25
 
args = buildArgs numArgs
26
 
  where
27
 
    buildArgs : (n : Nat) -> Vec String n
28
 
    buildArgs Z     = []
29
 
    buildArgs (S n) = snoc (buildArgs n) (getArg n)
30
 
 
31
 
{-# COMPILED_EPIC return (u1 : Unit, a : Any) -> Any = ioreturn(a) #-}
32
 
{-# COMPILED_EPIC _>>=_ (u1 : Unit, u2 : Unit, x : Any, f : Any) -> Any = iobind(x,f) #-}
33
 
{-# COMPILED_EPIC numArgs () -> BigInt = foreign BigInt "numArgsBig" () #-}
34
 
{-# COMPILED_EPIC getArg  (n : BigInt) -> Any = foreign Any "getArgBig" (n : BigInt) #-} 
35
 
 
36
 
postulate
37
 
  natToString : Nat -> String
38
 
  readNat    : IO Nat
39
 
  readStr    : IO String
40
 
  putStr     : String -> IO Unit
41
 
  printChar  : Char   -> IO Unit
42
 
 
43
 
 
44
 
putStrLn   : String -> IO Unit
45
 
putStrLn s = putStr s >>= \_ -> putStr "\n"
46
 
 
47
 
printFloat : Float  -> IO Unit
48
 
printFloat f = putStr (floatToString f)
49
 
 
50
 
printNat : Nat -> IO Unit
51
 
printNat n = putStr (natToString n)
52
 
 
53
 
printBool : Bool -> IO Unit
54
 
printBool true = putStr "true"
55
 
printBool false = putStr "false"
56
 
 
57
 
{-# COMPILED_EPIC natToString (n : Any) -> String = bigToStr(n) #-}
58
 
{-# COMPILED_EPIC readNat (u : Unit) -> Any = strToBig(readStr(u)) #-}
59
 
 
60
 
{-# COMPILED_EPIC putStr (a : String, u : Unit) -> Unit = foreign Int "wputStr" (a : String); primUnit #-}
61
 
{-# COMPILED_EPIC readStr (u : Unit) -> Data = readStr(u) #-}
62
 
{-# COMPILED_EPIC printChar (c : Int, u : Unit) -> Unit = printChar(c) #-}
63
 
 
64
 
infixr 2 _<$>_
65
 
_<$>_ : {A B : Set}(f : A -> B)(m : IO A) -> IO B
66
 
f <$> x = x >>= λ y -> return (f y)
67
 
 
68
 
infixr 0 bind
69
 
bind : ∀ {A B} → IO A → (A → IO B) → IO B
70
 
bind m f = m >>= f
71
 
 
72
 
infixr 0 then
73
 
then : ∀ {A B} -> IO A -> IO B -> IO B
74
 
then m f = m >>= λ _ -> f
75
 
 
76
 
syntax bind e (\ x -> f) = x <- e , f
77
 
syntax then e f          = e ,, f
 
 
b'\\ No newline at end of file'