6633483 · Idris-dev · git.iko.soy

lib/io.idr+2−1

compare with master

unifiedsplit

@@ -41,6 +41,7 @@ data Foreign : Set -> Set where

41 Foreign (ForeignTy xs t)

42

43mkForeign : Foreign x -> x

44+mkLazyForeign : Foreign x -> x

44−-- mkForeign compiled as primitive

45+-- mkForeign and mkLazyForeign compiled as primitives

45

46

47

lib/system.idr+3

@@ -25,3 +25,6 @@ getEnv x = mkForeign (FFun "getenv" [FString] FString) x

25exit : Int -> IO ()

26exit code = mkForeign (FFun "exit" [FInt] FUnit) code

27

28+usleep : Int -> IO ()

29+usleep i = mkForeign (FFun "usleep" [FInt] FUnit) i

30+

src/Idris/Compiler.hs+9−5

@@ -21,7 +21,7 @@ import Paths_idris

21import Epic.Epic hiding (Term, Type, Name, fn, compile)

22import qualified Epic.Epic as E

23

24−primDefs = [UN "mkForeign", UN "FalseElim"]

24+primDefs = [UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]

25

26compile :: FilePath -> Term -> Idris ()

27compile f tm

@@ -102,7 +102,9 @@ instance ToEpic (TT Name) where

102 epic tm = epic' [] tm where

103 epic' env tm@(App f a)

104 | (P _ (UN "mkForeign") _, args) <- unApply tm

105− = doForeign args

105+ = doForeign False args

106+ | (P _ (UN "mkLazyForeign") _, args) <- unApply tm

107+ = doForeign True args

106 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm

108 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm

107 = do arg' <- epic' env arg

109 = do arg' <- epic' env arg

108 return $ lazy_ arg'

110 return $ lazy_ arg'

@@ -155,15 +157,17 @@ instance ToEpic (TT Name) where

155 buildApp env (e @@ x') xs

157 buildApp env (e @@ x') xs

156

158

157

159

158−doForeign :: [TT Name] -> Idris E.Term

160+doForeign :: Bool -> [TT Name] -> Idris E.Term

159−doForeign (_ : fgn : args)

161+doForeign lazy (_ : fgn : args)

160 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

162 | (_, (Constant (Str fgnName) : fgnArgTys : ret : [])) <- unApply fgn

161 = let tys = getFTypes fgnArgTys

163 = let tys = getFTypes fgnArgTys

162 rty = mkEty' ret in

164 rty = mkEty' ret in

163 do args' <- mapM epic args

165 do args' <- mapM epic args

164 -- wrap it in a prim__IO

166 -- wrap it in a prim__IO

165 -- return $ con_ 0 @@ impossible @@

167 -- return $ con_ 0 @@ impossible @@

168+ if lazy

169+ then return $ lazy_ $ foreignL_ rty fgnName (zip args' tys)

166− return $ lazy_ $ foreign_ rty fgnName (zip args' tys)

170+ else return $ lazy_ $ foreign_ rty fgnName (zip args' tys)

167 | otherwise = fail "Badly formed foreign function call"

171 | otherwise = fail "Badly formed foreign function call"

168

172

169getFTypes :: TT Name -> [E.Type]

173getFTypes :: TT Name -> [E.Type]

support/Makefile+2−2

@@ -1,5 +1,5 @@

1−OBJS = network.o testidr.o

1+OBJS = network.o threads.o testidr.o

2−HDRS = network.h testidr.h

2+HDRS = network.h threads.h testidr.h

3

4CFLAGS = `epic -includedirs`

5

support/threads.c+27−22

@@ -5,72 +5,77 @@

5

6typedef struct {

7 pthread_mutex_t m_id;

8−} Mutex;

8+} IdrisMutex;

9

10typedef struct {

11 pthread_t t_id;

12−} Thread;

12+} IdrisThread;

13

14−Mutex** ms = NULL;

14+IdrisMutex** idris_ms = NULL;

15−int mutexes = 0;

15+int idris_mutexes = 0;

16

17−int idris_newLock(int sem)

17+int idris_newLock()

18{

19 pthread_mutex_t m;

20

21 pthread_mutex_init(&m, NULL);

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

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

23 newm->m_id = m;

24

25 // Increase space for the mutexes

26− if (ms==NULL) {

26+ if (idris_ms==NULL) {

27− ms = (Mutex**)EMALLOC(sizeof(Mutex*));

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

28− mutexes=1;

28+ idris_mutexes=1;

29 } else {

30− ms = (Mutex**)(EREALLOC(ms, sizeof(Mutex*)*(mutexes+1)));

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

31− mutexes++;

31+ idris_mutexes++;

32 }

33

34− ms[mutexes-1] = newm;

34+ idris_ms[idris_mutexes-1] = newm;

35− return mutexes-1;

35+ return idris_mutexes-1;

36}

37

38void idris_doLock(int lock)

39{

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

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

41}

42

43void idris_doUnlock(int lock)

44{

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

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

46}

47

48−struct threadinfo {

48+struct idris_threadinfo {

49 void* proc;

50 void* result;

51};

52

53void* idris_runThread(void* th_in) {

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

54− struct threadinfo* th = (struct threadinfo*)th_in;

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

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

55− void* v = DO_EVAL(th->proc, 1);

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

56 th->result = v;

58 th->result = v;

57 return v;

59 return v;

58}

60}

59

61

60void idris_doFork(void* proc)

62void idris_doFork(void* proc)

61{

63{

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

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

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

63− struct threadinfo th;

66+ struct idris_threadinfo th;

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

64 th.proc = proc;

68 th.proc = proc;

65 th.result = NULL;

69 th.result = NULL;

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

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

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

67}

72}

68

73

69void* idris_doWithin(int limit, void* proc, void* doOnFail)

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

70{

75{

71 pthread_t* t = EMALLOC(sizeof(pthread_t));

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

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

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

73− struct threadinfo th;

78+ struct idris_threadinfo th;

74 th.proc = proc;

79 th.proc = proc;

75 th.result = NULL;

80 th.result = NULL;

76

81

support/threads.h+1−2

@@ -1,8 +1,7 @@

1#ifndef _THREADS_H

2#define _THREADS_H

3

4−

5−int idris_newLock(int sem);

4+int idris_newLock();

6void idris_doLock(int lock);

5void idris_doLock(int lock);

7void idris_doUnlock(int lock);

6void idris_doUnlock(int lock);

8void idris_doFork(void* proc);

7void idris_doFork(void* proc);