← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/Introduction/Built-in.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/Introduction/Built-in.agda
1
 
 
2
 
 
3
 
module Introduction.Built-in where
4
 
 
5
 
{- Agda supports four built-in types :
6
 
 
7
 
    - integers,
8
 
    - floating point numbers,
9
 
    - characters, and
10
 
    - strings.
11
 
 
12
 
   Note that strings are not defined as lists of characters (as is the case in
13
 
   Haskell).
14
 
 
15
 
   To use the built-in types they first have to be bound to Agda types. The
16
 
   reason for this is that there are no predefined names in Agda.
17
 
-}
18
 
 
19
 
postulate
20
 
  Int    : Set
21
 
  Float  : Set
22
 
  Char   : Set
23
 
  String : Set
24
 
 
25
 
{-# BUILTIN INTEGER Int    #-}
26
 
{-# BUILTIN FLOAT   Float  #-}
27
 
{-# BUILTIN CHAR    Char   #-}
28
 
{-# BUILTIN STRING  String #-}
29
 
 
30
 
pi : Float
31
 
pi = 3.141593
32
 
 
33
 
forAll : Char
34
 
forAll = '∀'
35
 
 
36
 
hello : String
37
 
hello = "Hello World!"
38
 
 
39
 
 
40
 
data Nat : Set where
41
 
  zero : Nat
42
 
  suc  : Nat -> Nat
43
 
 
44
 
{-# BUILTIN NATURAL Nat  #-}
45
 
{-# BUILTIN SUC     suc  #-}
46
 
{-# BUILTIN ZERO    zero #-}
47
 
 
48
 
fortyTwo : Nat
49
 
fortyTwo = 42
50
 
 
51
 
 
52
 
module FloatPlus where  -- We put it in a module to prevent it from clashing with
53
 
                      -- the plus function in the complete list of primitive
54
 
                      -- functions below.
55
 
  primitive
56
 
    primFloatPlus : Float -> Float -> Float
57
 
 
58
 
  twoPi = primFloatPlus pi pi
59
 
 
60
 
 
61
 
data Bool : Set where
62
 
  false : Bool
63
 
  true  : Bool
64
 
 
65
 
{-# BUILTIN BOOL  Bool  #-}
66
 
{-# BUILTIN TRUE  true  #-}
67
 
{-# BUILTIN FALSE false #-}
68
 
 
69
 
module FloatLess where
70
 
 
71
 
  primitive
72
 
    primFloatLess : Float -> Float -> Bool
73
 
 
74
 
 
75
 
data List (A : Set) : Set where
76
 
  nil  : List A
77
 
  _::_ : A -> List A -> List A
78
 
 
79
 
{-# BUILTIN LIST List #-}
80
 
{-# BUILTIN NIL  nil  #-}
81
 
{-# BUILTIN CONS _::_ #-}
82
 
 
83
 
module StringToList where
84
 
 
85
 
  primitive
86
 
    primStringToList : String -> List Char
87
 
 
88
 
 
89
 
primitive
90
 
 
91
 
    -- Integer functions
92
 
  primIntegerPlus     : Int -> Int -> Int
93
 
  primIntegerMinus    : Int -> Int -> Int
94
 
  primIntegerTimes    : Int -> Int -> Int
95
 
  primIntegerDiv      : Int -> Int -> Int  -- partial
96
 
  primIntegerMod      : Int -> Int -> Int  -- partial
97
 
  primIntegerEquality : Int -> Int -> Bool
98
 
  primIntegerLess     : Int -> Int -> Bool
99
 
  primIntegerAbs      : Int -> Nat
100
 
  primNatToInteger    : Nat -> Int
101
 
  primShowInteger     : Int -> String
102
 
 
103
 
    -- Floating point functions
104
 
  primIntegerToFloat : Int -> Float
105
 
  primFloatPlus      : Float -> Float -> Float
106
 
  primFloatMinus     : Float -> Float -> Float
107
 
  primFloatTimes     : Float -> Float -> Float
108
 
  primFloatDiv       : Float -> Float -> Float
109
 
  primFloatLess      : Float -> Float -> Bool
110
 
  primRound          : Float -> Int
111
 
  primFloor          : Float -> Int
112
 
  primCeiling        : Float -> Int
113
 
  primExp            : Float -> Float
114
 
  primLog            : Float -> Float     -- partial
115
 
  primSin            : Float -> Float
116
 
  primShowFloat      : Float -> String
117
 
 
118
 
    -- Character functions
119
 
  primCharEquality : Char -> Char -> Bool
120
 
  primIsLower      : Char -> Bool
121
 
  primIsDigit      : Char -> Bool
122
 
  primIsAlpha      : Char -> Bool
123
 
  primIsSpace      : Char -> Bool
124
 
  primIsAscii      : Char -> Bool
125
 
  primIsLatin1     : Char -> Bool
126
 
  primIsPrint      : Char -> Bool
127
 
  primIsHexDigit   : Char -> Bool
128
 
  primToUpper      : Char -> Char
129
 
  primToLower      : Char -> Char
130
 
  primCharToNat    : Char -> Nat
131
 
  primNatToChar    : Nat  -> Char -- partial
132
 
  primShowChar     : Char -> String
133
 
 
134
 
    -- String functions
135
 
  primStringToList   : String -> List Char
136
 
  primStringFromList : List Char -> String
137
 
  primStringAppend   : String -> String -> String
138
 
  primStringEquality : String -> String -> Bool
139
 
  primShowString     : String -> String