git.iko.soy/Idris-dev
on master help sign in
Documentation improvements in library
17e042bDavid Raymond Christiansen
libs/base/Data/List.idr+9−1
compare with master
unifiedsplit
@@ -2,9 +2,17 @@ module Data.List
2
2
3%access public
3%access public
4
4
5−||| A proof that some element is found in a list
5+||| A proof that some element is found in a list.
6+|||
7+||| Example: `the (Elem "bar" ["foo", "bar", "baz"]) (tactics { search })`
6data Elem : a -> List a -> Type where
8data Elem : a -> List a -> Type where
9+ ||| A proof that the element is at the front of the list.
10+ |||
11+ ||| Example: `the (Elem "a" ["a", "b"]) Here`
7 Here : Elem x (x :: xs)
12 Here : Elem x (x :: xs)
13+ ||| A proof that the element is after the front of the list
14+ |||
15+ ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
8 There : Elem x xs -> Elem x (y :: xs)
16 There : Elem x xs -> Elem x (y :: xs)
9
17
10instance Uninhabited (Elem {a} x []) where
18instance Uninhabited (Elem {a} x []) where
libs/base/Data/Vect/Quantifiers.idr+24−2
@@ -1,9 +1,15 @@
1module Data.Vect.Quantifiers
1module Data.Vect.Quantifiers
2
2
3+||| A proof that some element of a vector satisfies some property
4+|||
5+||| @ P the property to be satsified
3data Any : (P : a -> Type) -> Vect n a -> Type where
6data Any : (P : a -> Type) -> Vect n a -> Type where
7+ ||| A proof that the satisfying element is the first one in the `Vect`
4 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
8 Here : {P : a -> Type} -> {xs : Vect n a} -> P x -> Any P (x :: xs)
9+ ||| A proof that the satsifying element is in the tail of the `Vect`
5 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
10 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
6
11
12+||| No element of an empty vector satisfies any property
7anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
13anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
8anyNilAbsurd (Here _) impossible
14anyNilAbsurd (Here _) impossible
9anyNilAbsurd (There _) impossible
15anyNilAbsurd (There _) impossible
@@ -15,7 +21,13 @@ anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) ->
15anyElim _ f (Here p) = f p
21anyElim _ f (Here p) = f p
16anyElim f _ (There p) = f p
22anyElim f _ (There p) = f p
17
23
24+||| Given a decision procedure for a property, determine if an element of a
25+||| vector satisfies it.
26+|||
27+||| @ P the property to be satisfied
28+||| @ dec the decision procedure
29+||| @ xs the vector to examine
18−any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
30+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
19any _ Nil = No anyNilAbsurd
31any _ Nil = No anyNilAbsurd
20any p (x::xs) with (p x)
32any p (x::xs) with (p x)
21 | Yes prf = Yes (Here prf)
33 | Yes prf = Yes (Here prf)
@@ -24,10 +36,14 @@ any p (x::xs) with (p x)
24 Yes prf' => Yes (There prf')
36 Yes prf' => Yes (There prf')
25 No prf' => No (anyElim prf' prf)
37 No prf' => No (anyElim prf' prf)
26
38
39+||| A proof that all elements of a vector satisfy a property. It is a list of
40+||| proofs, corresponding element-wise to the `Vect`.
27data All : (P : a -> Type) -> Vect n a -> Type where
41data All : (P : a -> Type) -> Vect n a -> Type where
28 Nil : {P : a -> Type} -> All P Nil
42 Nil : {P : a -> Type} -> All P Nil
29 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
43 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
30
44
45+||| If there does not exist an element that satifies the property, then it is
46+||| the case that all elements do not satisfy.
31negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
47negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
32negAnyAll {xs=Nil} _ = Nil
48negAnyAll {xs=Nil} _ = Nil
33negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
49negAnyAll {xs=(x::xs)} f = (\x => f (Here x)) :: negAnyAll (\x => f (There x))
@@ -40,7 +56,13 @@ notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :
40notAllThere _ Nil impossible
56notAllThere _ Nil impossible
41notAllThere np (_ :: ps) = np ps
57notAllThere np (_ :: ps) = np ps
42
58
59+||| Given a decision procedure for a property, decide whether all elements of
60+||| a vector satisfy it.
61+|||
62+||| @ P the property
63+||| @ dec the decision procedure
64+||| @ xs the vector to examine
43−all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
65+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
44all _ Nil = Yes Nil
66all _ Nil = Yes Nil
45all d (x::xs) with (d x)
67all d (x::xs) with (d x)
46 | No prf = No (notAllHere prf)
68 | No prf = No (notAllHere prf)
libs/base/Data/ZZ.idr+18−9
@@ -7,14 +7,18 @@ import Data.Sign
7%access public
7%access public
8
8
9
9
10−||| An integer is either a positive nat or the negated successor of a nat.
10+||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
11+|||
11−||| Zero is arbitrarily chosen to be positive.
12+||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
13+||| to be positive.
14+|||
12data ZZ = Pos Nat | NegS Nat
15data ZZ = Pos Nat | NegS Nat
13
16
14instance Signed ZZ where
17instance Signed ZZ where
15 sign (Pos _) = Plus
18 sign (Pos _) = Plus
16 sign (NegS _) = Minus
19 sign (NegS _) = Minus
17
20
21+||| Take the absolute value of a `ZZ`
18absZ : ZZ -> Nat
22absZ : ZZ -> Nat
19absZ (Pos n) = n
23absZ (Pos n) = n
20absZ (NegS n) = S n
24absZ (NegS n) = S n
@@ -23,28 +27,32 @@ instance Show ZZ where
23 show (Pos n) = show n
27 show (Pos n) = show n
24 show (NegS n) = "-" ++ show (S n)
28 show (NegS n) = "-" ++ show (S n)
25
29
26−negZ : ZZ -> ZZ
30+instance Neg ZZ where
27−negZ (Pos Z) = Pos Z
31+ negate (Pos Z) = Pos Z
28−negZ (Pos (S n)) = NegS n
32+ negate (Pos (S n)) = NegS n
29−negZ (NegS n) = Pos (S n)
33+ negate (NegS n) = Pos (S n)
30
34
31negNat : Nat -> ZZ
35negNat : Nat -> ZZ
32negNat Z = Pos Z
36negNat Z = Pos Z
33negNat (S n) = NegS n
37negNat (S n) = NegS n
34
38
39+
40+||| Construct a `ZZ` as the difference of two `Nat`s
35minusNatZ : Nat -> Nat -> ZZ
41minusNatZ : Nat -> Nat -> ZZ
36minusNatZ n Z = Pos n
42minusNatZ n Z = Pos n
37minusNatZ Z (S m) = NegS m
43minusNatZ Z (S m) = NegS m
38minusNatZ (S n) (S m) = minusNatZ n m
44minusNatZ (S n) (S m) = minusNatZ n m
39
45
46+||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`.
40plusZ : ZZ -> ZZ -> ZZ
47plusZ : ZZ -> ZZ -> ZZ
41plusZ (Pos n) (Pos m) = Pos (n + m)
48plusZ (Pos n) (Pos m) = Pos (n + m)
42plusZ (NegS n) (NegS m) = NegS (S (n + m))
49plusZ (NegS n) (NegS m) = NegS (S (n + m))
43plusZ (Pos n) (NegS m) = minusNatZ n (S m)
50plusZ (Pos n) (NegS m) = minusNatZ n (S m)
44plusZ (NegS n) (Pos m) = minusNatZ m (S n)
51plusZ (NegS n) (Pos m) = minusNatZ m (S n)
45
52
53+||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
46subZ : ZZ -> ZZ -> ZZ
54subZ : ZZ -> ZZ -> ZZ
47−subZ n m = plusZ n (negZ m)
55+subZ n m = plusZ n (negate m)
48
56
49instance Eq ZZ where
57instance Eq ZZ where
50 (Pos n) == (Pos m) = n == m
58 (Pos n) == (Pos m) = n == m
@@ -58,13 +66,14 @@ instance Ord ZZ where
58 compare (Pos _) (NegS _) = GT
66 compare (Pos _) (NegS _) = GT
59 compare (NegS _) (Pos _) = LT
67 compare (NegS _) (Pos _) = LT
60
68
61−
69+||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`.
62multZ : ZZ -> ZZ -> ZZ
70multZ : ZZ -> ZZ -> ZZ
63multZ (Pos n) (Pos m) = Pos $ n * m
71multZ (Pos n) (Pos m) = Pos $ n * m
64multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
72multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
65multZ (NegS n) (Pos m) = negNat $ (S n) * m
73multZ (NegS n) (Pos m) = negNat $ (S n) * m
66multZ (Pos n) (NegS m) = negNat $ n * (S m)
74multZ (Pos n) (NegS m) = negNat $ n * (S m)
67
75
76+||| Convert an `Integer` to an inductive representation.
68fromInt : Integer -> ZZ
77fromInt : Integer -> ZZ
69fromInt n = if n < 0
78fromInt n = if n < 0
70 then NegS $ fromInteger {a=Nat} ((-n) - 1)
79 then NegS $ fromInteger {a=Nat} ((-n) - 1)
@@ -100,7 +109,7 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100 -> n * m = x -> (Pos n) * (Pos m) = Pos x
109 -> n * m = x -> (Pos n) * (Pos m) = Pos x
101natMultZMult n m x h = cong h
110natMultZMult n m x h = cong h
102
111
103−doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
112+doubleNegElim : (z : ZZ) -> negate (negate z) = z
104doubleNegElim (Pos Z) = Refl
113doubleNegElim (Pos Z) = Refl
105doubleNegElim (Pos (S n)) = Refl
114doubleNegElim (Pos (S n)) = Refl
106doubleNegElim (NegS Z) = Refl
115doubleNegElim (NegS Z) = Refl
libs/base/Language/Reflection.idr+11−9
@@ -79,20 +79,22 @@ reflectConstant = toConst
79
79
80
80
81||| Types of named references
81||| Types of named references
82−data NameType = Bound
82+data NameType =
83− -- ^ reference which is just bound, e.g. by intro
83+ ||| A reference which is just bound, e.g. by intro
84− | Ref
84+ Bound |
85− -- ^ reference to a variable
85+ ||| A reference to a de Bruijn-indexed variable
86+ Ref |
87+ ||| Data constructor with tag and number
86− | DCon Int Int
88+ DCon Int Int |
87− -- ^ constructor with tag and number
89+ ||| Type constructor with tag and number
88− | TCon Int Int
90+ TCon Int Int
89− -- ^ type constructor with tag and number
91+
90%name NameType nt, nt'
92%name NameType nt, nt'
91
93
92||| Types annotations for bound variables in different
94||| Types annotations for bound variables in different
93||| binding contexts
95||| binding contexts
94data Binder a = Lam a
96data Binder a = Lam a
95− | Pi a a
97+ | Pi a a
96 | Let a a
98 | Let a a
97 | NLet a a
99 | NLet a a
98 | Hole a
100 | Hole a
libs/base/Network/Socket.idr+51−37
@@ -4,8 +4,8 @@
4module IdrisNet.Socket
4module IdrisNet.Socket
5
5
6%include C "idris_net.h"
6%include C "idris_net.h"
7−%include C "sys/types.h"
7+%include C "sys/types.h"
8−%include C "sys/socket.h"
8+%include C "sys/socket.h"
9%include C "netdb.h"
9%include C "netdb.h"
10
10
11%access public
11%access public
@@ -16,12 +16,17 @@ ByteLength = Int
16class ToCode a where
16class ToCode a where
17 toCode : a -> Int
17 toCode : a -> Int
18
18
19−-- Socket Families.
19+||| Socket Families
20+|||
20−-- The ones that people might actually use. We're not going to need US Government
21+||| The ones that people might actually use. We're not going to need US
21−-- proprietary ones...
22+||| Government proprietary ones.
22−data SocketFamily = AF_UNSPEC -- Unspecified
23+data SocketFamily =
24+ ||| Unspecified
25+ AF_UNSPEC |
26+ ||| IP / UDP etc. IPv4
23− | AF_INET -- IP / UDP etc. IPv4
27+ AF_INET |
28+ ||| IP / UDP etc. IPv6
24− | AF_INET6 -- IP / UDP etc. IPv6
29+ AF_INET6
25
30
26instance Show SocketFamily where
31instance Show SocketFamily where
27 show AF_UNSPEC = "AF_UNSPEC"
32 show AF_UNSPEC = "AF_UNSPEC"
@@ -36,11 +41,16 @@ instance ToCode SocketFamily where
36getSocketFamily : Int -> Maybe SocketFamily
41getSocketFamily : Int -> Maybe SocketFamily
37getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
42getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
38
43
39−-- Socket Types.
44+||| Socket Types.
45+data SocketType =
40−data SocketType = NotASocket -- Not a socket, used in certain operations
46+ ||| Not a socket, used in certain operations
47+ NotASocket |
41− | Stream -- TCP
48+ ||| TCP
49+ Stream |
42− | Datagram -- UDP
50+ ||| UDP
51+ Datagram |
43− | RawSocket -- Raw sockets. A guy can dream.
52+ ||| Raw sockets
53+ RawSocket
44
54
45instance Show SocketType where
55instance Show SocketType where
46 show NotASocket = "Not a socket"
56 show NotASocket = "Not a socket"
@@ -60,15 +70,17 @@ data RecvfromStructPtr = RFPtr Ptr
60data BufPtr = BPtr Ptr
70data BufPtr = BPtr Ptr
61data SockaddrPtr = SAPtr Ptr
71data SockaddrPtr = SAPtr Ptr
62
72
73+||| Protocol Number.
74+|||
63−-- Protocol Number. Generally good enough to just set it to 0.
75+||| Generally good enough to just set it to 0.
64ProtocolNumber : Type
76ProtocolNumber : Type
65ProtocolNumber = Int
77ProtocolNumber = Int
66
78
67−-- SocketError: Error thrown by a socket operation
79+||| SocketError: Error thrown by a socket operation
68SocketError : Type
80SocketError : Type
69SocketError = Int
81SocketError = Int
70
82
71−-- SocketDescriptor: Native C Socket Descriptor
83+||| SocketDescriptor: Native C Socket Descriptor
72SocketDescriptor : Type
84SocketDescriptor : Type
73SocketDescriptor = Int
85SocketDescriptor = Int
74
86
@@ -86,7 +98,7 @@ instance Show SocketAddress where
86Port : Type
98Port : Type
87Port = Int
99Port = Int
88
100
89−-- Backlog used within listen() call -- number of incoming calls
101+||| Backlog used within listen() call -- number of incoming calls
90BACKLOG : Int
102BACKLOG : Int
91BACKLOG = 20
103BACKLOG = 20
92
104
@@ -109,7 +121,7 @@ record UDPAddrInfo : Type where
109 (remote_port : Port) ->
121 (remote_port : Port) ->
110 UDPAddrInfo
122 UDPAddrInfo
111
123
112−-- Frees a given pointer
124+||| Frees a given pointer
113public
125public
114sock_free : BufPtr -> IO ()
126sock_free : BufPtr -> IO ()
115sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
127sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
@@ -118,12 +130,14 @@ public
118sockaddr_free : SockaddrPtr -> IO ()
130sockaddr_free : SockaddrPtr -> IO ()
119sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
131sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
120
132
121−-- Allocates an amount of memory given by the ByteLength parameter.
133+||| Allocates an amount of memory given by the ByteLength parameter.
134+|||
122−-- Used to allocate a mutable pointer to be given to the Recv functions.
135+||| Used to allocate a mutable pointer to be given to the Recv functions.
123public
136public
124sock_alloc : ByteLength -> IO BufPtr
137sock_alloc : ByteLength -> IO BufPtr
125sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
138sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
126
139
140+||| The metadata about a socket
127record Socket : Type where
141record Socket : Type where
128 MkSocket : (descriptor : SocketDescriptor) ->
142 MkSocket : (descriptor : SocketDescriptor) ->
129 (family : SocketFamily) ->
143 (family : SocketFamily) ->
@@ -131,20 +145,21 @@ record Socket : Type where
131 (protocolNumber : ProtocolNumber) ->
145 (protocolNumber : ProtocolNumber) ->
132 Socket
146 Socket
133
147
148+||| Get the C error number
134getErrno : IO Int
149getErrno : IO Int
135getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
150getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
136
151
137−-- Creates a UNIX socket with the given family, socket type and protocol number.
152+||| Creates a UNIX socket with the given family, socket type and protocol
138−-- Returns either a socket or an error.
153+||| number. Returns either a socket or an error.
139socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
140socket sf st pn = do
155socket sf st pn = do
141 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
156 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
142 if socket_res == -1 then -- error
157 if socket_res == -1 then -- error
143 map Left getErrno
158 map Left getErrno
144− else
159+ else
145 return $ Right (MkSocket socket_res sf st pn)
160 return $ Right (MkSocket socket_res sf st pn)
146
161
147−
162+||| Close a socket
148close : Socket -> IO ()
163close : Socket -> IO ()
149close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
164close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
150
165
@@ -153,18 +168,18 @@ saString : (Maybe SocketAddress) -> String
153saString (Just sa) = show sa
168saString (Just sa) = show sa
154saString Nothing = ""
169saString Nothing = ""
155
170
156−-- Binds a socket to the given socket address and port.
171+||| Binds a socket to the given socket address and port.
157−-- Returns 0 on success, an error code otherwise.
172+||| Returns 0 on success, an error code otherwise.
158bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
159bind sock addr port = do
174bind sock addr port = do
160− bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
175+ bind_res <- (mkForeign (FFun "idrnet_bind" [FInt, FInt, FInt, FString, FInt] FInt)
161 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
176 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
162 if bind_res == (-1) then -- error
177 if bind_res == (-1) then -- error
163 getErrno
178 getErrno
164 else return 0 -- Success
179 else return 0 -- Success
165
180
166−-- Connects to a given address and port.
181+||| Connects to a given address and port.
167−-- Returns 0 on success, and an error number on error.
182+||| Returns 0 on success, and an error number on error.
168connect : Socket -> SocketAddress -> Port -> IO Int
183connect : Socket -> SocketAddress -> Port -> IO Int
169connect sock addr port = do
184connect sock addr port = do
170 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
185 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
@@ -173,7 +188,7 @@ connect sock addr port = do
173 getErrno
188 getErrno
174 else return 0
189 else return 0
175
190
176−-- Listens on a bound socket.
191+||| Listens on a bound socket.
177listen : Socket -> IO Int
192listen : Socket -> IO Int
178listen sock = do
193listen sock = do
179 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
194 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
@@ -181,7 +196,7 @@ listen sock = do
181 getErrno
196 getErrno
182 else return 0
197 else return 0
183
198
184−-- Parses a textual representation of an IPv4 address into a SocketAddress
199+||| Parses a textual representation of an IPv4 address into a SocketAddress
185parseIPv4 : String -> SocketAddress
200parseIPv4 : String -> SocketAddress
186parseIPv4 str = case splitted of
201parseIPv4 str = case splitted of
187 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
202 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
@@ -194,7 +209,7 @@ parseIPv4 str = case splitted of
194 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
209 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
195
210
196
211
197−-- Retrieves a socket address from a sockaddr pointer
212+||| Retrieves a socket address from a sockaddr pointer
198getSockAddr : SockaddrPtr -> IO SocketAddress
213getSockAddr : SockaddrPtr -> IO SocketAddress
199getSockAddr (SAPtr ptr) = do
214getSockAddr (SAPtr ptr) = do
200 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
215 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
@@ -256,13 +271,13 @@ recv sock len = do
256 return $ Right (payload, recv_res)
271 return $ Right (payload, recv_res)
257
272
258
273
259−-- Sends the data in a given memory location
274+||| Sends the data in a given memory location
260sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
275sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
261sendBuf sock (BPtr ptr) len = do
276sendBuf sock (BPtr ptr) len = do
262 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
277 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
263 if send_res == (-1) then
278 if send_res == (-1) then
264 map Left getErrno
279 map Left getErrno
265− else
280+ else
266 return $ Right send_res
281 return $ Right send_res
267
282
268recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
283recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
@@ -313,7 +328,7 @@ recvFrom sock bl = do
313 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
328 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
314 (descriptor sock) bl
329 (descriptor sock) bl
315 let recv_ptr' = RFPtr recv_ptr
330 let recv_ptr' = RFPtr recv_ptr
316− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
331+ if !(nullPtr recv_ptr) then
317 map Left getErrno
332 map Left getErrno
318 else do
333 else do
319 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
334 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -332,7 +347,7 @@ recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrI
332recvFromBuf sock (BPtr ptr) bl = do
347recvFromBuf sock (BPtr ptr) bl = do
333 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
348 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
334 let recv_ptr' = RFPtr recv_ptr
349 let recv_ptr' = RFPtr recv_ptr
335− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
350+ if !(nullPtr recv_ptr) then
336 map Left getErrno
351 map Left getErrno
337 else do
352 else do
338 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
353 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -345,5 +360,4 @@ recvFromBuf sock (BPtr ptr) bl = do
345 freeRecvfromStruct recv_ptr'
360 freeRecvfromStruct recv_ptr'
346 return $ Right (MkUDPAddrInfo addr port, result + 1)
361 return $ Right (MkUDPAddrInfo addr port, result + 1)
347
362
348−
349
363
libs/prelude/Builtins.idr+15−13
@@ -5,11 +5,10 @@
5
5
6||| The canonical single-element type, also known as the trivially
6||| The canonical single-element type, also known as the trivially
7||| true proposition.
7||| true proposition.
8−%elim
9− data Unit =
8+%elim data Unit =
10− ||| The trivial constructor for `()`.
9+ ||| The trivial constructor for `()`.
11− MkUnit
10+ MkUnit
12−
11+
13||| The non-dependent pair type, also known as conjunction.
12||| The non-dependent pair type, also known as conjunction.
14||| @A the type of the left elements in the pair
13||| @A the type of the left elements in the pair
15||| @B the type of the left elements in the pair
14||| @B the type of the left elements in the pair
@@ -18,10 +17,15 @@ data Pair : (A : Type) -> (B : Type) -> Type where
18 ||| @a the left element of the pair
17 ||| @a the left element of the pair
19 ||| @b the right element of the pair
18 ||| @b the right element of the pair
20 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
19 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
21−
20+
22−||| Dependent pairs, in their internal representation
21+||| Dependent pairs
22+|||
23+||| Dependent pairs represent existential quantification - they consist of a
24+||| witness for the existential claim and a proof that the property holds for
25+||| it. Another way to see dependent pairs is as just data - for instance, the
26+||| length of a vector paired with that vector.
27+|||
23−||| @ a the type of the witness
28+||| @ a the type of the witness @ P the type of the proof
24−||| @ P the type of the proof
25data Sigma : (a : Type) -> (P : a -> Type) -> Type where
29data Sigma : (a : Type) -> (P : a -> Type) -> Type where
26 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
30 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
27
31
@@ -43,7 +47,6 @@ infix 5 ~=~
43(~=~) : (x : a) -> (y : b) -> Type
47(~=~) : (x : a) -> (y : b) -> Type
44(~=~) x y = (=) _ _ x y
48(~=~) x y = (=) _ _ x y
45
49
46−-- ------------------------------------------------------ [ For rewrite tactic ]
47||| Perform substitution in a term according to some equality.
50||| Perform substitution in a term according to some equality.
48|||
51|||
49||| This is used by the `rewrite` tactic and term.
52||| This is used by the `rewrite` tactic and term.
@@ -95,7 +98,7 @@ namespace Ownership
95 ||| A read-only version of a unique value
98 ||| A read-only version of a unique value
96 data Borrowed : UniqueType -> NullType where
99 data Borrowed : UniqueType -> NullType where
97 Read : {a : UniqueType} -> a -> Borrowed a
100 Read : {a : UniqueType} -> a -> Borrowed a
98−
101+
99 ||| Make a read-only version of a unique value, which can be passed to another
102 ||| Make a read-only version of a unique value, which can be passed to another
100 ||| function without the unique value being consumed.
103 ||| function without the unique value being consumed.
101 implicit
104 implicit
@@ -104,7 +107,7 @@ namespace Ownership
104
107
105par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
108par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
106 -- is better in any case?
109 -- is better in any case?
107−par (Delay x) = x
110+par (Delay x) = x
108
111
109malloc : Int -> a -> a
112malloc : Int -> a -> a
110malloc size x = x -- compiled specially
113malloc size x = x -- compiled specially
@@ -135,4 +138,3 @@ believe_me x = prim__believe_me _ _ x
135public %assert_total
138public %assert_total
136really_believe_me : a -> b
139really_believe_me : a -> b
137really_believe_me x = prim__believe_me _ _ x
140really_believe_me x = prim__believe_me _ _ x
138−
libs/prelude/Prelude.idr+8
@@ -494,6 +494,7 @@ getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
494
494
495---- some basic file handling
495---- some basic file handling
496
496
497+||| A file handle
497abstract
498abstract
498data File = FHandle Ptr
499data File = FHandle Ptr
499
500
@@ -592,6 +593,7 @@ partial
592do_feof : Ptr -> IO Int
593do_feof : Ptr -> IO Int
593do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
594do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
594
595
596+||| Check if a file handle has reached the end
595feof : File -> IO Bool
597feof : File -> IO Bool
596feof (FHandle h) = do eof <- do_feof h
598feof (FHandle h) = do eof <- do_feof h
597 return (not (eof == 0))
599 return (not (eof == 0))
@@ -608,6 +610,7 @@ fpoll : File -> IO Bool
608fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
610fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
609 return (p > 0)
611 return (p > 0)
610
612
613+||| Check if a foreign pointer is null
611partial
614partial
612nullPtr : Ptr -> IO Bool
615nullPtr : Ptr -> IO Bool
613nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
616nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
@@ -630,6 +633,10 @@ validFile : File -> IO Bool
630validFile (FHandle h) = do x <- nullPtr h
633validFile (FHandle h) = do x <- nullPtr h
631 return (not x)
634 return (not x)
632
635
636+||| Loop while some test is true
637+|||
638+||| @ test the condition of the loop
639+||| @ body the loop body
633partial -- obviously
640partial -- obviously
634while : (test : IO Bool) -> (body : IO ()) -> IO ()
641while : (test : IO Bool) -> (body : IO ()) -> IO ()
635while t b = do v <- t
642while t b = do v <- t
@@ -637,6 +644,7 @@ while t b = do v <- t
637 while t b
644 while t b
638 else return ()
645 else return ()
639
646
647+||| Read the contents of a file into a string
640partial -- no error checking!
648partial -- no error checking!
641readFile : String -> IO String
649readFile : String -> IO String
642readFile fn = do h <- openFile fn Read
650readFile fn = do h <- openFile fn Read