c0acdc5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' into lambdastyle

c0acdc5johnny-john12 years ago

CONTRIBUTING.md+23−6

compare with master

unifiedsplit

@@ -15,7 +15,7 @@ Here are a few guidelines that we would like contributors to follow so that we c

15 * [Debian](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Debian)

16 * [Windows](https://github.com/idris-lang/Idris-dev/wiki/Idris-on-Windows)

18−# Issue Reporting

18+## Issue Reporting

20Before you report an issue, or wish to add cool functionality please try and check to see if there are existing [issues](https://github.com/idris-lang/Idris-dev/issues) and [pull requests](https://github.com/idris-lang/Idris-dev/pulls).

21We do not want you wasting your time, duplicating somebody's work!

@@ -25,6 +25,25 @@ We do not want you wasting your time, duplicating somebody's work!

25A basic rule when contributing to Idris is the **campsite rule**: leave the codebase in better condition than you found it.

26Please clean up any messes that you find, and don't leave behind new messes for the next contributor.

28+## Contributing to the default libraries.

29+

30+`Idris` ships with a set of packages in `libs/` that is provided as a default library.

31+These packages should not be seen as the *standard* as when working with dependent types we do not necessarily know how best to work with dependent types.

32+These packages offer functionality that can be built on top of when constructing `Idris` programs.

33+

34+One major point to make is that everything in prelude will be imported automatically, unless given

35+the `--noprelude` option.

36+A central idea within the `Idris` Community is that what counts as `Idris` is: **the compiler plus the Standard Prelude**.

37+Other libraries (base, effects, etc) are still part of the distribution, but not necessarily standard.

38+

39+As `Idris` is still being developed we are open to suggestions and changes that make improvements to these default packages.

40+Major changes to the library (or `Idris` itself) should ideally be discussed first through the projects official channels of communication i.e. the mailing list, github wiki, or IRC, or as a [Dragon Egg](https://github.com/idris-lang/Idris-dev/wiki/Feature-proposals).

41+Developers then seeking to add content to `Idris`s prelude and default library, should do so through a PR where more discussion's and refinements can be made.

42+

43+We do not want you wasting your time nor duplicating somebody's work!

44+

45+Of note: developers should be prepared to wait until their PR has been discussed and authorized prior to the PRs inclusion.

46+

28## Making Changes

47## Making Changes

30Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).

49Idris developers and hackers try to adhere to something similar to the [successful git branching model](http://nvie.com/posts/a-successful-git-branching-model/).

@@ -88,11 +107,11 @@ $ git diff --check

88 line separating the summary from the body is critical (unless you omit

107 line separating the summary from the body is critical (unless you omit

89 the body entirely); tools like rebase can get confused if you run the

108 the body entirely); tools like rebase can get confused if you run the

90 two together.

109 two together.

91−

110+

92 Further paragraphs come after blank lines.

111 Further paragraphs come after blank lines.

93−

112+

94 - Bullet points are okay, too

113 - Bullet points are okay, too

95−

114+

96 - Typically a hyphen or asterisk is used for the bullet, preceded by a

115 - Typically a hyphen or asterisk is used for the bullet, preceded by a

97 single space, with blank lines in between, but conventions vary here

116 single space, with blank lines in between, but conventions vary here

117

@@ -137,5 +156,3 @@ To help increase the chance of your pull request being accepted:

137

156

138

157

139Adapted from the most excellent contributing files from the [Puppet project](https://github.com/puppetlabs/puppet) and [Factroy Girl Rails](https://github.com/thoughtbot/factory_girl_rails/blob/master/CONTRIBUTING.md)

158Adapted from the most excellent contributing files from the [Puppet project](https://github.com/puppetlabs/puppet) and [Factroy Girl Rails](https://github.com/thoughtbot/factory_girl_rails/blob/master/CONTRIBUTING.md)

140−

141−

libs/prelude/Prelude/Algebra.idr+54−2

@@ -123,7 +123,7 @@ class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

123||| + Inverse for `<+>`:

124||| forall a, a <+> inverse a == neutral

125||| forall a, inverse a <+> a == neutral

126−||| + Associativity of `<*>a:

126+||| + Associativity of `<*>`:

127||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

128||| + Neutral for `<*>`:

129||| forall a, a <*> unity == a

@@ -264,9 +264,61 @@ class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a w

264

265class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }

266

267+-- Fields.

268+||| Sets equipped with two binary operations, both associative and commutative

269+||| supplied with a neutral element, with

270+||| distributivity laws relating the two operations. Must satisfy the following

271+||| laws:

272+|||

273+||| + Associativity of `<+>`:

274+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

275+||| + Commutativity of `<+>`:

276+||| forall a b, a <+> b == b <+> a

277+||| + Neutral for `<+>`:

278+||| forall a, a <+> neutral == a

279+||| forall a, neutral <+> a == a

280+||| + Inverse for `<+>`:

281+||| forall a, a <+> inverse a == neutral

282+||| forall a, inverse a <+> a == neutral

283+||| + Associativity of `<*>`:

284+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c

285+||| + Unity for `<*>`:

286+||| forall a, a <*> unity == a

287+||| forall a, unity <*> a == a

288+||| + InverseM of `<*>`:

289+||| forall a, a <*> inverseM a == unity

290+||| forall a, inverseM a <*> a == unity

291+||| + Distributivity of `<*>` and `<->`:

292+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)

293+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)

294+class RingWithUnity a => Field a where

295+ inverseM : a -> a

296+

297+class (VerifiedRing a, Field a) => VerifiedField a where

298+ total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity

299+ total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity

300+

301+-- vector spaces.

302+||| A Vector Space over a Field can be considered as an additive Abeliean Group

303+||| of Vectors adjoined to the Field structure by distributivity laws relating

304+||| the two operations. Such that we satisfy the following laws:

305+|||

306+||| + Unity for `<*>`:

307+||| forall a, a <*> unity == a

308+||| forall a, unity <*> a == a

309+||| + Distributivity of `<*>` and `<+>`:

310+||| forall a x y, a <*> (x <+> y) == (a <*> x) <+> (a <*> y)

311+||| forall a b x, (a <+> b) <*> x == (a <*> x) <+> (b <*> x)

312+class (Field a, AbelianGroup a) => VectorSpace a a where {}

313+

314+class (VerifiedField a, VerifiedAbelianGroup a, VectorSpace a a) => VerifiedVectorSpace a a where

315+ total vectorspaceScalarUnityIsUnityL : (l : a) -> l <*> unity = l

316+ total vectorspaceScalarUnityIsUnityR : (r : a) -> unity <*> r = r

317+ total vectorspaceScalarIsDistributiveWRTVectorAddition : (s : a) -> (x, y : a) -> s <*> (x <+> y) = (s <*> x) <+> (s <*> y)

318+ total vectorspaceScalarIsDistributiveWRTFieldAddition : (s, t : a) -> (x : a) -> (s <+> t) <*> x = (s <*> x) <+> (t <*> x)

319+

267

320

268-- XXX todo:

321-- XXX todo:

269−-- Fields and vector spaces.

270-- Structures where "abs" make sense.

322-- Structures where "abs" make sense.

271-- Euclidean domains, etc.

323-- Euclidean domains, etc.

272-- Where to put fromInteger and fromRational?

324-- Where to put fromInteger and fromRational?

libs/prelude/Prelude/List.idr+67−2

@@ -157,7 +157,7 @@ drop Z xs = xs

157drop (S n) [] = []

158drop (S n) (x::xs) = drop n xs

159

160−||| Take the longest prefix of a list such that all elements satsify some

160+||| Take the longest prefix of a list such that all elements satisfy some

161||| Boolean predicate.

162|||

163||| @ p the predicate

@@ -165,7 +165,7 @@ takeWhile : (p : a -> Bool) -> List a -> List a

165takeWhile p [] = []

166takeWhile p (x::xs) = if p x then x :: takeWhile p xs else []

167

168−||| Remove the longest prefix of a list such that all removed elements satsify some

168+||| Remove the longest prefix of a list such that all removed elements satisfy some

169||| Boolean predicate.

170|||

171||| @ p the predicate

@@ -340,6 +340,9 @@ reverse = reverse' []

340 reverse' acc (x::xs) = reverse' (x::acc) xs

341

342||| Insert some separator between the elements of a list.

343+|||

344+||| > intersperse ',' (unpack "abcde") == unpack "a,b,c,d,e"

345+|||

343intersperse : a -> List a -> List a

346intersperse : a -> List a -> List a

344intersperse sep [] = []

347intersperse sep [] = []

345intersperse sep (x::xs) = x :: intersperse' sep xs

348intersperse sep (x::xs) = x :: intersperse' sep xs

@@ -468,6 +471,10 @@ elemIndices = elemIndicesBy (==)

468-- Filters

471-- Filters

469--------------------------------------------------------------------------------

472--------------------------------------------------------------------------------

470

473

474+||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,

475+|||

476+||| > filter (<3) [0..5] == [0,1,2]

477+|||

471filter : (a -> Bool) -> List a -> List a

478filter : (a -> Bool) -> List a -> List a

472filter p [] = []

479filter p [] = []

473filter p (x::xs) =

480filter p (x::xs) =

@@ -476,6 +483,7 @@ filter p (x::xs) =

476 else

483 else

477 filter p xs

484 filter p xs

478

485

486+||| The nubBy function behaves just like nub, except it uses a user-supplied equality predicate instead of the overloaded == function.

479nubBy : (a -> a -> Bool) -> List a -> List a

487nubBy : (a -> a -> Bool) -> List a -> List a

480nubBy = nubBy' []

488nubBy = nubBy' []

481 where

489 where

@@ -487,22 +495,40 @@ nubBy = nubBy' []

487 else

495 else

488 x :: nubBy' (x::acc) p xs

496 x :: nubBy' (x::acc) p xs

489

497

498+||| O(n^2). The nub function removes duplicate elements from a list. In particular, it keeps only the first occurrence of each element. It is a special case of nubBy, which allows the programmer to supply their own equality test.

499+|||

500+||| > nub (the (List _) [1,2,1,3]) == [1,2,3]

501+|||

490nub : Eq a => List a -> List a

502nub : Eq a => List a -> List a

491nub = nubBy (==)

503nub = nubBy (==)

492

504

505+||| The deleteBy function behaves like delete, but takes a user-supplied equality predicate.

493deleteBy : (a -> a -> Bool) -> a -> List a -> List a

506deleteBy : (a -> a -> Bool) -> a -> List a -> List a

494deleteBy _ _ [] = []

507deleteBy _ _ [] = []

495deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys

508deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys

496

509

510+||| delete x removes the first occurrence of x from its list argument. For example,

511+|||

512+||| > delete 'a' (unpack "banana") == unpack "bnana"

513+|||

514+||| It is a special case of deleteBy, which allows the programmer to supply their own equality test.

497delete : (Eq a) => a -> List a -> List a

515delete : (Eq a) => a -> List a -> List a

498delete = deleteBy (==)

516delete = deleteBy (==)

499

517

518+||| The \\ function is list difference (non-associative). In the result of xs \\ ys, the first occurrence of each element of ys in turn (if any) has been removed from xs, e.g.,

519+|||

520+||| > (([1,2] ++ [2,3]) \\ [1,2]) == [2,3]

521+|||

500(\\) : (Eq a) => List a -> List a -> List a

522(\\) : (Eq a) => List a -> List a -> List a

501(\\) = foldl (flip delete)

523(\\) = foldl (flip delete)

502

524

503unionBy : (a -> a -> Bool) -> List a -> List a -> List a

525unionBy : (a -> a -> Bool) -> List a -> List a -> List a

504unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

526unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

505

527

528+||| The union function returns the list union of the two lists. For example,

529+|||

530+||| > union (unpack "dog") (unpack "cow") == unpack "dogcw"

531+|||

506union : (Eq a) => List a -> List a -> List a

532union : (Eq a) => List a -> List a -> List a

507union = unionBy (==)

533union = unionBy (==)

508

534

@@ -512,6 +538,9 @@ union = unionBy (==)

512

538

513||| Given a list and a predicate, returns a pair consisting of the longest

539||| Given a list and a predicate, returns a pair consisting of the longest

514||| prefix of the list that satisfies a predicate and the rest of the list.

540||| prefix of the list that satisfies a predicate and the rest of the list.

541+|||

542+||| > span (<3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])

543+|||

515span : (a -> Bool) -> List a -> (List a, List a)

544span : (a -> Bool) -> List a -> (List a, List a)

516span p [] = ([], [])

545span p [] = ([], [])

517span p (x::xs) =

546span p (x::xs) =

@@ -521,9 +550,18 @@ span p (x::xs) =

521 else

550 else

522 ([], x::xs)

551 ([], x::xs)

523

552

553+||| Given a list and a predicate, returns a pair consisting of the longest

554+||| prefix of the list that does not satisfy a predicate and the rest of the list.

555+|||

556+||| > break (>=3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])

557+|||

524break : (a -> Bool) -> List a -> (List a, List a)

558break : (a -> Bool) -> List a -> (List a, List a)

525break p = span (not . p)

559break p = span (not . p)

526

560

561+||| Split on any elements that satisfy the given predicate.

562+|||

563+||| > split (<2) [2,0,3,1,4] == [[2], [3], [4]]

564+|||

527split : (a -> Bool) -> List a -> List (List a)

565split : (a -> Bool) -> List a -> List (List a)

528split p xs =

566split p xs =

529 case break p xs of

567 case break p xs of

@@ -538,6 +576,10 @@ split p xs =

538splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)

576splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)

539splitAt n xs = (take n xs, drop n xs)

577splitAt n xs = (take n xs, drop n xs)

540

578

579+||| The partition function takes a predicate a list and returns the pair of lists of elements which do and do not satisfy the predicate, respectively; e.g.,

580+|||

581+||| > partition (<3) [0..5] == (the (List Integer) [0,1,2], the (List Integer) [3,4,5])

582+|||

541partition : (a -> Bool) -> List a -> (List a, List a)

583partition : (a -> Bool) -> List a -> (List a, List a)

542partition p [] = ([], [])

584partition p [] = ([], [])

543partition p (x::xs) =

585partition p (x::xs) =

@@ -547,19 +589,35 @@ partition p (x::xs) =

547 else

589 else

548 (lefts, x::rights)

590 (lefts, x::rights)

549

591

592+||| The inits function returns all initial segments of the argument, shortest first. For example,

593+|||

594+||| > inits [1,2,3] == [[],[1],[1,2],[1,2,3]]

595+|||

550inits : List a -> List (List a)

596inits : List a -> List (List a)

551inits xs = [] :: case xs of

597inits xs = [] :: case xs of

552 [] => []

598 [] => []

553 x :: xs' => map (x ::) (inits xs')

599 x :: xs' => map (x ::) (inits xs')

554

600

601+||| The tails function returns all final segments of the argument, longest first. For example,

602+|||

603+||| > tails [1,2,3] == [[1,2,3], [2,3], [3], []]

604+|||

555tails : List a -> List (List a)

605tails : List a -> List (List a)

556tails xs = xs :: case xs of

606tails xs = xs :: case xs of

557 [] => []

607 [] => []

558 _ :: xs' => tails xs'

608 _ :: xs' => tails xs'

559

609

610+||| Split on the given element.

611+|||

612+||| > splitOn 0 [1,0,2,0,0,3] == [[1],[2],[],[3]]

613+|||

560splitOn : Eq a => a -> List a -> List (List a)

614splitOn : Eq a => a -> List a -> List (List a)

561splitOn a = split (== a)

615splitOn a = split (== a)

562

616

617+||| Replaces all occurences of the first argument with the second argument in a list.

618+|||

619+||| > replaceOn '-' ',' (unpack "1-2-3") == unpack "1,2,3"

620+|||

563replaceOn : Eq a => a -> a -> List a -> List a

621replaceOn : Eq a => a -> a -> List a -> List a

564replaceOn a b l = map (\c => if c == a then b else c) l

622replaceOn a b l = map (\c => if c == a then b else c) l

565

623

@@ -576,15 +634,22 @@ isPrefixOfBy p (x::xs) (y::ys) =

576 else

634 else

577 False

635 False

578

636

637+||| The isPrefixOf function takes two lists and returns True iff the first list is a prefix of the second.

579isPrefixOf : Eq a => List a -> List a -> Bool

638isPrefixOf : Eq a => List a -> List a -> Bool

580isPrefixOf = isPrefixOfBy (==)

639isPrefixOf = isPrefixOfBy (==)

581

640

582isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool

641isSuffixOfBy : (a -> a -> Bool) -> List a -> List a -> Bool

583isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

642isSuffixOfBy p left right = isPrefixOfBy p (reverse left) (reverse right)

584

643

644+||| The isSuffixOf function takes two lists and returns True iff the first list is a suffix of the second.

585isSuffixOf : Eq a => List a -> List a -> Bool

645isSuffixOf : Eq a => List a -> List a -> Bool

586isSuffixOf = isSuffixOfBy (==)

646isSuffixOf = isSuffixOfBy (==)

587

647

648+||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.

649+|||

650+||| > isInfixOf "Idris" "I really like Idris." == True

651+||| > isInfixOf "Ial" "I really like Idris." == False

652+|||

588isInfixOf : Eq a => List a -> List a -> Bool

653isInfixOf : Eq a => List a -> List a -> Bool

589isInfixOf n h = any (isPrefixOf n) (tails h)

654isInfixOf n h = any (isPrefixOf n) (tails h)

590

655

libs/prelude/Prelude/Vect.idr+15

@@ -205,16 +205,31 @@ zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

205zipWith f [] [] = []

206zipWith f (x::xs) (y::ys) = f x y :: zipWith f xs ys

207

208+||| Combine three equal-length vectors into a vector with some function

209+zipWith3 : (a -> b -> c -> d) -> Vect n a -> Vect n b -> Vect n c -> Vect n d

210+zipWith3 f [] [] [] = []

211+zipWith3 f (x::xs) (y::ys) (z::zs) = f x y z :: zipWith3 f xs ys zs

212+

208||| Combine two equal-length vectors pairwise

213||| Combine two equal-length vectors pairwise

209zip : Vect n a -> Vect n b -> Vect n (a, b)

214zip : Vect n a -> Vect n b -> Vect n (a, b)

210zip = zipWith (\x,y => (x,y))

215zip = zipWith (\x,y => (x,y))

211

216

217+||| Combine three equal-length vectors elementwise into a vector of tuples

218+zip3 : Vect n a -> Vect n b -> Vect n c -> Vect n (a, b, c)

219+zip3 = zipWith3 (\x,y,z => (x,y,z))

220+

212||| Convert a vector of pairs to a pair of vectors

221||| Convert a vector of pairs to a pair of vectors

213unzip : Vect n (a, b) -> (Vect n a, Vect n b)

222unzip : Vect n (a, b) -> (Vect n a, Vect n b)

214unzip [] = ([], [])

223unzip [] = ([], [])

215unzip ((l, r)::xs) with (unzip xs)

224unzip ((l, r)::xs) with (unzip xs)

216 | (lefts, rights) = (l::lefts, r::rights)

225 | (lefts, rights) = (l::lefts, r::rights)

217

226

227+||| Convert a vector of three-tuples to a triplet of vectors

228+unzip3 : Vect n (a, b, c) -> (Vect n a, Vect n b, Vect n c)

229+unzip3 [] = ([], [], [])

230+unzip3 ((l,c,r)::xs) with (unzip3 xs)

231+ | (lefts, centers, rights) = (l::lefts, c::centers, r::rights)

232+

218--------------------------------------------------------------------------------

233--------------------------------------------------------------------------------

219-- Equality

234-- Equality

220--------------------------------------------------------------------------------

235--------------------------------------------------------------------------------

rts/idris_rts.c+2−1

@@ -346,10 +346,11 @@ void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i

346}

347

348VAL idris_castIntStr(VM* vm, VAL i) {

349+ int x = (int) GETINT(i);

349 Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);

350 Closure* cl = allocate(vm, sizeof(Closure) + sizeof(char)*16, 0);

350 SETTY(cl, STRING);

351 SETTY(cl, STRING);

351 cl -> info.str = (char*)cl + sizeof(Closure);

352 cl -> info.str = (char*)cl + sizeof(Closure);

352− sprintf(cl -> info.str, "%d", (int)(GETINT(i)));

353+ sprintf(cl -> info.str, "%d", x);

353 return cl;

354 return cl;

354}

355}

355

356

support/Makefiledeleted−15

@@ -1,15 +0,0 @@

1−OBJS = network.o testidr.o

2−HDRS = network.h testidr.h

3−

4−CFLAGS = `epic -includedirs`

5−

6−LIBTARGET = libidris.a

7−

8−check: $(OBJS)

9− ar -r $(LIBTARGET) $(OBJS)

10−

11−install: check

12− install $(LIBTARGET) $(TARGET)

13− install $(HDRS) $(TARGET)

14−

15−.PHONY: check install

support/network.cdeleted−260

@@ -1,260 +0,0 @@

1−#include <stdio.h>

2−#include <sys/types.h>

3−#include <sys/socket.h>

4−#include <netinet/in.h>

5−#include <arpa/inet.h>

6−#include <unistd.h>

7−#include <string.h>

8−#include <fcntl.h>

9−#include <errno.h>

10−#include <closure.h>

11−

12−#include "network.h"

13−

14−int isReadable(int sd, int timeOut) { // milliseconds

15− fd_set socketReadSet;

16− FD_ZERO(&socketReadSet);

17− FD_SET(sd,&socketReadSet);

18− struct timeval tv;

19− if (timeOut) {

20− tv.tv_sec = timeOut / 1000;

21− tv.tv_usec = (timeOut % 1000) * 1000;

22− } else {

23− tv.tv_sec = 0;

24− tv.tv_usec = 0;

25− } // if

26− if (select(sd+1,&socketReadSet,0,0,&tv) == -1) {

27− printf("READ ERROR!\n");

28− return 0;

29− } // if

30− return FD_ISSET(sd,&socketReadSet) != 0;

31−} /* isReadable */

32−

33−void* net_UDP_clientSocket(char* server, int port) {

34− srand(12345); //time(NULL));

35−

36− Connection* con = (Connection*)EMALLOC(sizeof(Connection));

37− int s;

38− struct sockaddr_in si_me, si_other;

39−

40− if ((s=socket(AF_INET, SOCK_DGRAM, 0))==-1) {

41− printf("FAIL 1\n");

42− return NULL;

43− }

44−

45− memset((char *) &si_other, 0, sizeof(si_other));

46− si_other.sin_family = AF_INET;

47− si_other.sin_port = htons(port);

48−

49− if (inet_aton(server, &si_other.sin_addr)==0) {

50− printf("FAIL 2\n");

51− return NULL;

52− }

53−

54− // Bind, so we can receive replies.

55− si_me.sin_family = AF_INET;

56− si_me.sin_port = htons(0);

57− si_me.sin_addr.s_addr = htonl(INADDR_ANY);

58−

59− if (bind(s, (struct sockaddr*)&si_me, sizeof(si_me))<0) {

60− return NULL;

61− }

62−

63− con->sock = s;

64− con->addr = si_other;

65−

66−// printf("Opened client socket %d\n", s);

67− return con;

68−}

69−

70−void* net_UDP_serverSocket(int port) {

71− srand(time(NULL));

72−

73− Connection* con = (Connection*)EMALLOC(sizeof(Connection));

74− int s;

75− struct sockaddr_in si_me;

76−

77− if ((s=socket(AF_INET, SOCK_DGRAM, 0))==-1) {

78− return NULL;

79− }

80−

81− memset((char *) &si_me, 0, sizeof(si_me));

82− si_me.sin_family = AF_INET;

83− si_me.sin_port = htons(port);

84− si_me.sin_addr.s_addr = htonl(INADDR_ANY);

85− if (bind(s, (struct sockaddr*)&si_me, sizeof(si_me))==-1) {

86− return NULL;

87− }

88−

89− con->sock = s;

90− con->addr = si_me;

91−

92−// printf("Opened server socket %d\n", s);

93− return con;

94−}

95−

96−int net_sendUDP(void* conn, char* server, int port, char* stuff) {

97−// printf("Socket is %d\n", conn);

98− if (0) { //rand()%50000 == 0) {

99− printf("DROP\n");

100− return 0;

101− }

102−

103−

104− Connection* c = (Connection*)conn;

105− int s = c->sock;

106− struct sockaddr_in other = c->addr;

107− memset((char *) &other, 0, sizeof(other));

108− other.sin_family = AF_INET;

109− other.sin_port = htons(port);

110− if (inet_aton(server, &other.sin_addr)==0) {

111− printf("FAIL 3\n");

112− return -1;

113− }

114−

115− if (sendto(s, stuff, strlen(stuff), 0, (struct sockaddr*)&other,

116− sizeof(other))==-1) {

117− printf("Send FAIL\n");

118− return -1;

119− }

120−// printf("Send WIN, to %s %d %d\n", inet_ntoa(other.sin_addr),

121−// ntohs(other.sin_port), port);

122− return 0;

123−}

124−

125−void* net_recvUDP(void* conn) {

126− struct sockaddr_in other;

127− Connection* c = (Connection*)conn;

128− int s = c->sock;

129− socklen_t slen = sizeof(other);

130− struct sockaddr_in me = c->addr;

131−

132− // TMP HACK: 512 should be enough for the purposes of this experiment...

133− // Do it properly some time.

134− char* buf = (char*)EMALLOC(512*sizeof(char));

135−

136−// printf("Waiting to receive\n");

137−

138− int error;

139−// while (!isReadable(s,100)) printf(".");

140−

141− if (!isReadable(s, 1000)) {

142− printf("Nothing\n");

143− return NULL;

144− }

145−

146− if (recvfrom(s, buf, 512, 0, (struct sockaddr *)&other, &slen)==-1) {

147− printf("Nothing\n");

148− return NULL;

149− }

150−

151−/* printf("Received %s from %s:UDP%u\n",

152− buf,inet_ntoa(other.sin_addr),

153− ntohs(other.sin_port));

154−*/

155− // return a structure with the received value, and where it came from.

156− Recv* r = (Recv*)EMALLOC(sizeof(Recv));

157− r->buf = buf;

158− r->server = inet_ntoa(other.sin_addr);

159− r->port = ntohs(other.sin_port);

160−

161− return (void*)r;

162−}

163−

164−char* get_recvBuf(void* recv) {

165− return ((Recv*)recv)->buf;

166−}

167−

168−char* get_recvServer(void* recv) {

169− return ((Recv*)recv)->server;

170−}

171−

172−int get_recvPort(void* recv) {

173− return ((Recv*)recv)->port;

174−}

175−

176−int nullPtr(void *ptr) {

177− return ptr==NULL;

178−}

179−

180−// Just to see if the idris FFI is working, and happily talking to .o files...

181−int netTest(char* strTest, int num) {

182− int i;

183− for(i=0;i<num;++i) {

184− printf("%s\n",strTest);

185− }

186−

187− return i;

188−}

189−

190−void net_sendRaw(void* conn, char* server, int port, VAL pkt)

191−{

192− int seq = GETINT(PROJECT(pkt, 0));

193− VAL ty = PROJECT(pkt, 1);

194− int pty;

195−

196− switch(TAG(ty)) {

197− case 0:

198− pty = 0;

199− break;

200− case 1:

201− pty = 1;

202− break;

203− case 2:

204− pty = TAG(PROJECT(ty,0)) + 2;

205− }

206−

207− char* buf = (char*)EMALLOC(512*sizeof(char));

208− sprintf(buf, "%d %d", seq, pty);

209−

210− net_sendUDP(conn, server, port, buf);

211−}

212−

213−VAL net_recvRaw(void* conn)

214−{

215− int seq, pty;

216−

217− void* dat = net_recvUDP(conn);

218− if (dat==NULL) {

219− return CONSTRUCTOR(1,0,NULL); // Nothing

220− }

221− else {

222− char* recvBuf = get_recvBuf(dat);

223−

224− sscanf(recvBuf, "%d %d", &seq, &pty);

225− VAL ptyc = NULL;

226− if (pty<2) {

227− ptyc = CONSTRUCTOR(pty,0,NULL);

228− } else {

229− ptyc = CONSTRUCTOR1(2, CONSTRUCTOR(pty-2,0,NULL));

230− }

231− VAL pkt = CONSTRUCTOR2(0, MKINT(seq), ptyc);

232− printf("Received %d %d\n", seq, pty);

233−

234− VAL recvpkt = CONSTRUCTOR3(0, pkt, MKSTR(get_recvServer(dat)),

235− MKINT(get_recvPort(dat)));

236−

237− return CONSTRUCTOR1(0, recvpkt); // Just pkt

238− }

239−

240−}

241−

242−void dumpPkt(VAL pkt)

243−{

244− int seq = GETINT(PROJECT(pkt, 0));

245− VAL ty = PROJECT(pkt, 1);

246− int pty;

247−

248− switch(TAG(ty)) {

249− case 0:

250− pty = 0;

251− break;

252− case 1:

253− pty = 1;

254− break;

255− case 2:

256− pty = TAG(PROJECT(ty,0)) + 2;

257− }

258−

259− printf("%d %d\n", seq, pty);

260−}

support/network.hdeleted−36

@@ -1,36 +0,0 @@

1−#include <stdio.h>

2−#include <sys/types.h>

3−#include <sys/socket.h>

4−#include <netinet/in.h>

5−#include <arpa/inet.h>

6−#include <unistd.h>

7−#include <string.h>

8−#include <closure.h>

9−

10−typedef struct {

11− int sock;

12− struct sockaddr_in addr;

13−} Connection;

14−

15−typedef struct {

16− unsigned port;

17− char* buf;

18− char* server;

19−} Recv;

20−

21−int netTest(char* strTest, int num);

22−void* net_UDP_serverSocket(int port);

23−void* net_UDP_clientSocket(char* server, int port);

24−

25−int nullPtr(void *ptr);

26−

27−int net_sendUDP(void* conn, char* server, int port, char* stuff);

28−void* net_recvUDP(void* conn);

29−

30−char* get_recvBuf(void* recv);

31−char* get_recvServer(void* recv);

32−int get_recvPort(void* recv);

33−

34−void net_sendRaw(void* conn, char* server, int port, VAL pkt);

35−VAL net_recvRaw(void* conn);

36−void dumpPkt(VAL pkt);

support/testidr.cdeleted−6

@@ -1,6 +0,0 @@

1−#include "testidr.h"

2−#include <stdio.h>

3−

4−void testIdr() {

5− printf("Hello Idris support library!\n");

6−}

support/testidr.hdeleted−7

@@ -1,7 +0,0 @@

1−#ifndef __TESTIDR_H

2−#define __TESTIDR_H

3−

4−void testIdr();

5−

6−#endif

7−

support/threads.cdeleted−116

@@ -1,116 +0,0 @@

1−#include <closure.h>

2−#include "threads.h"

3−

4−// Threads and locks

5−

6−typedef struct {

7− pthread_mutex_t m_id;

8−} IdrisMutex;

9−

10−typedef struct {

11− pthread_t t_id;

12−} IdrisThread;

13−

14−IdrisMutex** idris_ms = NULL;

15−int idris_mutexes = 0;

16−

17−int idris_newLock()

18−{

19− pthread_mutex_t m;

20−

21− pthread_mutex_init(&m, NULL);

22− IdrisMutex* newm = EMALLOC(sizeof(IdrisMutex));

23− newm->m_id = m;

24−

25− // Increase space for the mutexes

26− if (idris_ms==NULL) {

27− idris_ms = (IdrisMutex**)EMALLOC(sizeof(IdrisMutex*));

28− idris_mutexes=1;

29− } else {

30− idris_ms = (IdrisMutex**)(EREALLOC(idris_ms, sizeof(IdrisMutex*)*(idris_mutexes+1)));

31− idris_mutexes++;

32− }

33−

34− idris_ms[idris_mutexes-1] = newm;

35− return idris_mutexes-1;

36−}

37−

38−void idris_doLock(int lock)

39−{

40− pthread_mutex_lock(&(idris_ms[lock]->m_id));

41−}

42−

43−void idris_doUnlock(int lock)

44−{

45− pthread_mutex_unlock(&(idris_ms[lock]->m_id));

46−}

47−

48−struct idris_threadinfo {

49− void* proc;

50− void* result;

51−};

52−

53−void* idris_runThread(void* th_in) {

54− printf("IN THREAD\n");

55− struct idris_threadinfo* th = (struct idris_threadinfo*)th_in;

56− printf("using %d\n", th_in);

57− void* v = DO_EVAL(th_in, 1);

58− th->result = v;

59− return v;

60−}

61−

62−void idris_doFork(void* proc)

63−{

64− printf("FORKING!\n");

65− pthread_t* t = malloc(sizeof(pthread_t));

66− struct idris_threadinfo th;

67− printf("in %d\n", proc);

68− th.proc = proc;

69− th.result = NULL;

70− pthread_create(t, NULL, idris_runThread, proc);

71− printf("FORKED!\n");

72−}

73−

74−void* idris_doWithin(int limit, void* proc, void* doOnFail)

75−{

76− pthread_t* t = EMALLOC(sizeof(pthread_t));

77−// printf("CREATING THREAD %d\n", t);

78− struct idris_threadinfo th;

79− th.proc = proc;

80− th.result = NULL;

81−

82− struct timeval tv;

83− gettimeofday(&tv, NULL);

84− int tnow, tthen = do_utime();

85−

86− pthread_create(t, NULL, idris_runThread, &th);

87−// printf("tthen %d\n", tthen);

88−

89− void* ans;

90−

91− do

92− {

93− // If the answer has been updated, we're done.

94− if (th.result!=NULL) {

95− pthread_join(*t, &ans);

96− return ans;

97− }

98− gettimeofday(&tv, NULL);

99− tnow = idris_utime();

100− usleep(100);

101−// printf("tnow %d\n", tnow);

102− }

103− while(tnow<(tthen+(limit*1000)));

104− pthread_cancel(*t);

105− return DO_EVAL(doOnFail,1);

106−}

107−

108−int idris_utime() {

109− struct timeval tv;

110− gettimeofday(&tv, NULL);

111−

112− static int start=0;

113− if (start==0) { start = tv.tv_sec; }

114−

115− return 1000000*(tv.tv_sec - start)+tv.tv_usec;

116−}

support/threads.hdeleted−11

@@ -1,11 +0,0 @@

1−#ifndef _THREADS_H

2−#define _THREADS_H

3−

4−int idris_newLock();

5−void idris_doLock(int lock);

6−void idris_doUnlock(int lock);

7−void idris_doFork(void* proc);

8−void* idris_doWithin(int limit, void* proc, void* doOnFail);

9−int idris_utime();

10−

11−#endif