git.iko.soy/Idris-dev
on master help sign in
Documentation improvements in library
commit17e042b520a25774ef1aed2f75c7f8e7227dd257 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 3 Oct 2014, 18:14 (12 years ago) parenta5a63fc
7 files changed+136−71
compare with master
unifiedsplit
libs/base/Data/List.idr+9−1 libs/base/Data/Vect/Quantifiers.idr+24−2 libs/base/Data/ZZ.idr+18−9 libs/base/Language/Reflection.idr+11−9 libs/base/Network/Socket.idr+51−37 libs/prelude/Builtins.idr+15−13 libs/prelude/Prelude.idr+8
libs/base/Data/List.idr+9−1
@@ -2,9 +2,17 @@ module Data.List
22
33%access public
44
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 })`
68data 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`
712 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)`
816 There : Elem x xs -> Elem x (y :: xs)
917
1018instance Uninhabited (Elem {a} x []) where
libs/base/Data/Vect/Quantifiers.idr+24−2
@@ -1,9 +1,15 @@
11module Data.Vect.Quantifiers
22
3+||| A proof that some element of a vector satisfies some property
4+|||
5+||| @ P the property to be satsified
36data Any : (P : a -> Type) -> Vect n a -> Type where
7+ ||| A proof that the satisfying element is the first one in the `Vect`
48 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`
510 There : {P : a -> Type} -> {xs : Vect n a} -> Any P xs -> Any P (x :: xs)
611
12+||| No element of an empty vector satisfies any property
713anyNilAbsurd : {P : a -> Type} -> Any P Nil -> _|_
814anyNilAbsurd (Here _) impossible
915anyNilAbsurd (There _) impossible
@@ -15,7 +21,13 @@ anyElim : {xs : Vect n a} -> {P : a -> Type} -> (Any P xs -> b) -> (P x -> b) ->
1521anyElim _ f (Here p) = f p
1622anyElim f _ (There p) = f p
1723
18−any : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
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
30+any : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (Any P xs)
1931any _ Nil = No anyNilAbsurd
2032any p (x::xs) with (p x)
2133 | Yes prf = Yes (Here prf)
@@ -24,10 +36,14 @@ any p (x::xs) with (p x)
2436 Yes prf' => Yes (There prf')
2537 No prf' => No (anyElim prf' prf)
2638
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`.
2741data All : (P : a -> Type) -> Vect n a -> Type where
2842 Nil : {P : a -> Type} -> All P Nil
2943 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
3044
45+||| If there does not exist an element that satifies the property, then it is
46+||| the case that all elements do not satisfy.
3147negAnyAll : {P : a -> Type} -> {xs : Vect n a} -> Not (Any P xs) -> All (\x => Not (P x)) xs
3248negAnyAll {xs=Nil} _ = Nil
3349negAnyAll {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 :
4056notAllThere _ Nil impossible
4157notAllThere np (_ :: ps) = np ps
4258
43−all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
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
65+all : {P : a -> Type} -> (dec : (x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
4466all _ Nil = Yes Nil
4567all d (x::xs) with (d x)
4668 | No prf = No (notAllHere prf)
libs/base/Data/ZZ.idr+18−9
@@ -7,14 +7,18 @@ import Data.Sign
77%access public
88
99
10−||| An integer is either a positive nat or the negated successor of a nat.
11−||| Zero is arbitrarily chosen to be positive.
10+||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
11+|||
12+||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
13+||| to be positive.
14+|||
1215data ZZ = Pos Nat | NegS Nat
1316
1417instance Signed ZZ where
1518 sign (Pos _) = Plus
1619 sign (NegS _) = Minus
1720
21+||| Take the absolute value of a `ZZ`
1822absZ : ZZ -> Nat
1923absZ (Pos n) = n
2024absZ (NegS n) = S n
@@ -23,28 +27,32 @@ instance Show ZZ where
2327 show (Pos n) = show n
2428 show (NegS n) = "-" ++ show (S n)
2529
26−negZ : ZZ -> ZZ
27−negZ (Pos Z) = Pos Z
28−negZ (Pos (S n)) = NegS n
29−negZ (NegS n) = Pos (S n)
30+instance Neg ZZ where
31+ negate (Pos Z) = Pos Z
32+ negate (Pos (S n)) = NegS n
33+ negate (NegS n) = Pos (S n)
3034
3135negNat : Nat -> ZZ
3236negNat Z = Pos Z
3337negNat (S n) = NegS n
3438
39+
40+||| Construct a `ZZ` as the difference of two `Nat`s
3541minusNatZ : Nat -> Nat -> ZZ
3642minusNatZ n Z = Pos n
3743minusNatZ Z (S m) = NegS m
3844minusNatZ (S n) (S m) = minusNatZ n m
3945
46+||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`.
4047plusZ : ZZ -> ZZ -> ZZ
4148plusZ (Pos n) (Pos m) = Pos (n + m)
4249plusZ (NegS n) (NegS m) = NegS (S (n + m))
4350plusZ (Pos n) (NegS m) = minusNatZ n (S m)
4451plusZ (NegS n) (Pos m) = minusNatZ m (S n)
4552
53+||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
4654subZ : ZZ -> ZZ -> ZZ
47−subZ n m = plusZ n (negZ m)
55+subZ n m = plusZ n (negate m)
4856
4957instance Eq ZZ where
5058 (Pos n) == (Pos m) = n == m
@@ -58,13 +66,14 @@ instance Ord ZZ where
5866 compare (Pos _) (NegS _) = GT
5967 compare (NegS _) (Pos _) = LT
6068
61−
69+||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`.
6270multZ : ZZ -> ZZ -> ZZ
6371multZ (Pos n) (Pos m) = Pos $ n * m
6472multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
6573multZ (NegS n) (Pos m) = negNat $ (S n) * m
6674multZ (Pos n) (NegS m) = negNat $ n * (S m)
6775
76+||| Convert an `Integer` to an inductive representation.
6877fromInt : Integer -> ZZ
6978fromInt n = if n < 0
7079 then NegS $ fromInteger {a=Nat} ((-n) - 1)
@@ -100,7 +109,7 @@ natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
100109 -> n * m = x -> (Pos n) * (Pos m) = Pos x
101110natMultZMult n m x h = cong h
102111
103−doubleNegElim : (z : ZZ) -> negZ (negZ z) = z
112+doubleNegElim : (z : ZZ) -> negate (negate z) = z
104113doubleNegElim (Pos Z) = Refl
105114doubleNegElim (Pos (S n)) = Refl
106115doubleNegElim (NegS Z) = Refl
libs/base/Language/Reflection.idr+11−9
@@ -79,20 +79,22 @@ reflectConstant = toConst
7979
8080
8181||| Types of named references
82−data NameType = Bound
83− -- ^ reference which is just bound, e.g. by intro
84− | Ref
85− -- ^ reference to a variable
86− | DCon Int Int
87− -- ^ constructor with tag and number
88− | TCon Int Int
89− -- ^ type constructor with tag and number
82+data NameType =
83+ ||| A reference which is just bound, e.g. by intro
84+ Bound |
85+ ||| A reference to a de Bruijn-indexed variable
86+ Ref |
87+ ||| Data constructor with tag and number
88+ DCon Int Int |
89+ ||| Type constructor with tag and number
90+ TCon Int Int
91+
9092%name NameType nt, nt'
9193
9294||| Types annotations for bound variables in different
9395||| binding contexts
9496data Binder a = Lam a
95− | Pi a a
97+ | Pi a a
9698 | Let a a
9799 | NLet a a
98100 | Hole a
libs/base/Network/Socket.idr+51−37
@@ -4,8 +4,8 @@
44module IdrisNet.Socket
55
66%include C "idris_net.h"
7−%include C "sys/types.h"
8−%include C "sys/socket.h"
7+%include C "sys/types.h"
8+%include C "sys/socket.h"
99%include C "netdb.h"
1010
1111%access public
@@ -16,12 +16,17 @@ ByteLength = Int
1616class ToCode a where
1717 toCode : a -> Int
1818
19−-- Socket Families.
20−-- The ones that people might actually use. We're not going to need US Government
21−-- proprietary ones...
22−data SocketFamily = AF_UNSPEC -- Unspecified
23− | AF_INET -- IP / UDP etc. IPv4
24− | AF_INET6 -- IP / UDP etc. IPv6
19+||| Socket Families
20+|||
21+||| The ones that people might actually use. We're not going to need US
22+||| Government proprietary ones.
23+data SocketFamily =
24+ ||| Unspecified
25+ AF_UNSPEC |
26+ ||| IP / UDP etc. IPv4
27+ AF_INET |
28+ ||| IP / UDP etc. IPv6
29+ AF_INET6
2530
2631instance Show SocketFamily where
2732 show AF_UNSPEC = "AF_UNSPEC"
@@ -36,11 +41,16 @@ instance ToCode SocketFamily where
3641getSocketFamily : Int -> Maybe SocketFamily
3742getSocketFamily i = Prelude.List.lookup i [(0, AF_UNSPEC), (2, AF_INET), (10, AF_INET6)]
3843
39−-- Socket Types.
40−data SocketType = NotASocket -- Not a socket, used in certain operations
41− | Stream -- TCP
42− | Datagram -- UDP
43− | RawSocket -- Raw sockets. A guy can dream.
44+||| Socket Types.
45+data SocketType =
46+ ||| Not a socket, used in certain operations
47+ NotASocket |
48+ ||| TCP
49+ Stream |
50+ ||| UDP
51+ Datagram |
52+ ||| Raw sockets
53+ RawSocket
4454
4555instance Show SocketType where
4656 show NotASocket = "Not a socket"
@@ -60,15 +70,17 @@ data RecvfromStructPtr = RFPtr Ptr
6070data BufPtr = BPtr Ptr
6171data SockaddrPtr = SAPtr Ptr
6272
63−-- Protocol Number. Generally good enough to just set it to 0.
73+||| Protocol Number.
74+|||
75+||| Generally good enough to just set it to 0.
6476ProtocolNumber : Type
6577ProtocolNumber = Int
6678
67−-- SocketError: Error thrown by a socket operation
79+||| SocketError: Error thrown by a socket operation
6880SocketError : Type
6981SocketError = Int
7082
71−-- SocketDescriptor: Native C Socket Descriptor
83+||| SocketDescriptor: Native C Socket Descriptor
7284SocketDescriptor : Type
7385SocketDescriptor = Int
7486
@@ -86,7 +98,7 @@ instance Show SocketAddress where
8698Port : Type
8799Port = Int
88100
89−-- Backlog used within listen() call -- number of incoming calls
101+||| Backlog used within listen() call -- number of incoming calls
90102BACKLOG : Int
91103BACKLOG = 20
92104
@@ -109,7 +121,7 @@ record UDPAddrInfo : Type where
109121 (remote_port : Port) ->
110122 UDPAddrInfo
111123
112−-- Frees a given pointer
124+||| Frees a given pointer
113125public
114126sock_free : BufPtr -> IO ()
115127sock_free (BPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
@@ -118,12 +130,14 @@ public
118130sockaddr_free : SockaddrPtr -> IO ()
119131sockaddr_free (SAPtr ptr) = mkForeign (FFun "idrnet_free" [FPtr] FUnit) ptr
120132
121−-- Allocates an amount of memory given by the ByteLength parameter.
122−-- Used to allocate a mutable pointer to be given to the Recv functions.
133+||| Allocates an amount of memory given by the ByteLength parameter.
134+|||
135+||| Used to allocate a mutable pointer to be given to the Recv functions.
123136public
124137sock_alloc : ByteLength -> IO BufPtr
125138sock_alloc bl = map BPtr $ mkForeign (FFun "idrnet_malloc" [FInt] FPtr) bl
126139
140+||| The metadata about a socket
127141record Socket : Type where
128142 MkSocket : (descriptor : SocketDescriptor) ->
129143 (family : SocketFamily) ->
@@ -131,20 +145,21 @@ record Socket : Type where
131145 (protocolNumber : ProtocolNumber) ->
132146 Socket
133147
148+||| Get the C error number
134149getErrno : IO Int
135150getErrno = mkForeign (FFun "idrnet_errno" [] FInt)
136151
137−-- Creates a UNIX socket with the given family, socket type and protocol number.
138−-- Returns either a socket or an error.
152+||| Creates a UNIX socket with the given family, socket type and protocol
153+||| number. Returns either a socket or an error.
139154socket : SocketFamily -> SocketType -> ProtocolNumber -> IO (Either SocketError Socket)
140155socket sf st pn = do
141156 socket_res <- mkForeign (FFun "socket" [FInt, FInt, FInt] FInt) (toCode sf) (toCode st) pn
142157 if socket_res == -1 then -- error
143158 map Left getErrno
144− else
159+ else
145160 return $ Right (MkSocket socket_res sf st pn)
146161
147−
162+||| Close a socket
148163close : Socket -> IO ()
149164close sock = mkForeign (FFun "close" [FInt] FUnit) (descriptor sock)
150165
@@ -153,18 +168,18 @@ saString : (Maybe SocketAddress) -> String
153168saString (Just sa) = show sa
154169saString Nothing = ""
155170
156−-- Binds a socket to the given socket address and port.
157−-- Returns 0 on success, an error code otherwise.
171+||| Binds a socket to the given socket address and port.
172+||| Returns 0 on success, an error code otherwise.
158173bind : Socket -> (Maybe SocketAddress) -> Port -> IO Int
159174bind 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)
161176 (descriptor sock) (toCode $ family sock) (toCode $ socketType sock) (saString addr) port)
162177 if bind_res == (-1) then -- error
163178 getErrno
164179 else return 0 -- Success
165180
166−-- Connects to a given address and port.
167−-- Returns 0 on success, and an error number on error.
181+||| Connects to a given address and port.
182+||| Returns 0 on success, and an error number on error.
168183connect : Socket -> SocketAddress -> Port -> IO Int
169184connect sock addr port = do
170185 conn_res <- (mkForeign (FFun "idrnet_connect" [FInt, FInt, FInt, FString, FInt] FInt)
@@ -173,7 +188,7 @@ connect sock addr port = do
173188 getErrno
174189 else return 0
175190
176−-- Listens on a bound socket.
191+||| Listens on a bound socket.
177192listen : Socket -> IO Int
178193listen sock = do
179194 listen_res <- mkForeign (FFun "listen" [FInt, FInt] FInt) (descriptor sock) BACKLOG
@@ -181,7 +196,7 @@ listen sock = do
181196 getErrno
182197 else return 0
183198
184−-- Parses a textual representation of an IPv4 address into a SocketAddress
199+||| Parses a textual representation of an IPv4 address into a SocketAddress
185200parseIPv4 : String -> SocketAddress
186201parseIPv4 str = case splitted of
187202 (i1 :: i2 :: i3 :: i4 :: _) => IPv4Addr i1 i2 i3 i4
@@ -194,7 +209,7 @@ parseIPv4 str = case splitted of
194209 splitted = map toInt (Prelude.Strings.split (\c => c == '.') str)
195210
196211
197−-- Retrieves a socket address from a sockaddr pointer
212+||| Retrieves a socket address from a sockaddr pointer
198213getSockAddr : SockaddrPtr -> IO SocketAddress
199214getSockAddr (SAPtr ptr) = do
200215 addr_family_int <- mkForeign (FFun "idrnet_sockaddr_family" [FPtr] FInt) ptr
@@ -256,13 +271,13 @@ recv sock len = do
256271 return $ Right (payload, recv_res)
257272
258273
259−-- Sends the data in a given memory location
274+||| Sends the data in a given memory location
260275sendBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
261276sendBuf sock (BPtr ptr) len = do
262277 send_res <- mkForeign (FFun "idrnet_send_buf" [FInt, FPtr, FInt] FInt) (descriptor sock) ptr len
263278 if send_res == (-1) then
264279 map Left getErrno
265− else
280+ else
266281 return $ Right send_res
267282
268283recvBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError ByteLength)
@@ -313,7 +328,7 @@ recvFrom sock bl = do
313328 recv_ptr <- mkForeign (FFun "idrnet_recvfrom" [FInt, FInt] FPtr)
314329 (descriptor sock) bl
315330 let recv_ptr' = RFPtr recv_ptr
316− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
331+ if !(nullPtr recv_ptr) then
317332 map Left getErrno
318333 else do
319334 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -332,7 +347,7 @@ recvFromBuf : Socket -> BufPtr -> ByteLength -> IO (Either SocketError (UDPAddrI
332347recvFromBuf sock (BPtr ptr) bl = do
333348 recv_ptr <- mkForeign (FFun "idrnet_recvfrom_buf" [FInt, FPtr, FInt] FPtr) (descriptor sock) ptr bl
334349 let recv_ptr' = RFPtr recv_ptr
335− if !(nullPtr recv_ptr) then -- ! notation = monadic bind shortcut, not "not"
350+ if !(nullPtr recv_ptr) then
336351 map Left getErrno
337352 else do
338353 result <- mkForeign (FFun "idrnet_get_recvfrom_res" [FPtr] FInt) recv_ptr
@@ -345,5 +360,4 @@ recvFromBuf sock (BPtr ptr) bl = do
345360 freeRecvfromStruct recv_ptr'
346361 return $ Right (MkUDPAddrInfo addr port, result + 1)
347362
348−
349363
libs/prelude/Builtins.idr+15−13
@@ -5,11 +5,10 @@
55
66||| The canonical single-element type, also known as the trivially
77||| true proposition.
8−%elim
9− data Unit =
10− ||| The trivial constructor for `()`.
11− MkUnit
12−
8+%elim data Unit =
9+ ||| The trivial constructor for `()`.
10+ MkUnit
11+
1312||| The non-dependent pair type, also known as conjunction.
1413||| @A the type of the left elements in the pair
1514||| @B the type of the left elements in the pair
@@ -18,10 +17,15 @@ data Pair : (A : Type) -> (B : Type) -> Type where
1817 ||| @a the left element of the pair
1918 ||| @b the right element of the pair
2019 MkPair : {A, B : Type} -> (a : A) -> (b : B) -> Pair A B
21−
22−||| Dependent pairs, in their internal representation
23−||| @ a the type of the witness
24−||| @ P the type of the proof
20+
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+|||
28+||| @ a the type of the witness @ P the type of the proof
2529data Sigma : (a : Type) -> (P : a -> Type) -> Type where
2630 MkSigma : .{P : a -> Type} -> (x : a) -> (pf : P x) -> Sigma a P
2731
@@ -43,7 +47,6 @@ infix 5 ~=~
4347(~=~) : (x : a) -> (y : b) -> Type
4448(~=~) x y = (=) _ _ x y
4549
46−-- ------------------------------------------------------ [ For rewrite tactic ]
4750||| Perform substitution in a term according to some equality.
4851|||
4952||| This is used by the `rewrite` tactic and term.
@@ -95,7 +98,7 @@ namespace Ownership
9598 ||| A read-only version of a unique value
9699 data Borrowed : UniqueType -> NullType where
97100 Read : {a : UniqueType} -> a -> Borrowed a
98−
101+
99102 ||| Make a read-only version of a unique value, which can be passed to another
100103 ||| function without the unique value being consumed.
101104 implicit
@@ -104,7 +107,7 @@ namespace Ownership
104107
105108par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type
106109 -- is better in any case?
107−par (Delay x) = x
110+par (Delay x) = x
108111
109112malloc : Int -> a -> a
110113malloc size x = x -- compiled specially
@@ -135,4 +138,3 @@ believe_me x = prim__believe_me _ _ x
135138public %assert_total
136139really_believe_me : a -> b
137140really_believe_me x = prim__believe_me _ _ x
138−
libs/prelude/Prelude.idr+8
@@ -494,6 +494,7 @@ getChar = map cast $ mkForeign (FFun "getchar" [] FInt)
494494
495495---- some basic file handling
496496
497+||| A file handle
497498abstract
498499data File = FHandle Ptr
499500
@@ -592,6 +593,7 @@ partial
592593do_feof : Ptr -> IO Int
593594do_feof h = mkForeign (FFun "fileEOF" [FPtr] FInt) h
594595
596+||| Check if a file handle has reached the end
595597feof : File -> IO Bool
596598feof (FHandle h) = do eof <- do_feof h
597599 return (not (eof == 0))
@@ -608,6 +610,7 @@ fpoll : File -> IO Bool
608610fpoll (FHandle h) = do p <- mkForeign (FFun "fpoll" [FPtr] FInt) h
609611 return (p > 0)
610612
613+||| Check if a foreign pointer is null
611614partial
612615nullPtr : Ptr -> IO Bool
613616nullPtr p = do ok <- mkForeign (FFun "isNull" [FPtr] FInt) p
@@ -630,6 +633,10 @@ validFile : File -> IO Bool
630633validFile (FHandle h) = do x <- nullPtr h
631634 return (not x)
632635
636+||| Loop while some test is true
637+|||
638+||| @ test the condition of the loop
639+||| @ body the loop body
633640partial -- obviously
634641while : (test : IO Bool) -> (body : IO ()) -> IO ()
635642while t b = do v <- t
@@ -637,6 +644,7 @@ while t b = do v <- t
637644 while t b
638645 else return ()
639646
647+||| Read the contents of a file into a string
640648partial -- no error checking!
641649readFile : String -> IO String
642650readFile fn = do h <- openFile fn Read