2316dc9 · Idris-dev · git.iko.soy

Setup.hs+4−4

compare with master

unifiedsplit

@@ -22,12 +22,12 @@ installStdLib pkg local verbosity copy

22 let icmd = ".." </> buildDir local </> "idris" </> "idris"

23 putStrLn $ "Installing libraries in " ++ idir

24 make verbosity

25− [ "-C", "lib", "install"

25+ [ "-C", "support", "install"

26 , "TARGET=" ++ idir

27 , "IDRIS=" ++ icmd

28 ]

29 make verbosity

30− [ "-C", "support", "install"

30+ [ "-C", "lib", "install"

31 , "TARGET=" ++ idir

32 , "IDRIS=" ++ icmd

33 ]

@@ -36,11 +36,11 @@ checkStdLib local verbosity

36 = do let icmd = ".." </> buildDir local </> "idris" </> "idris"

37 putStrLn $ "Building libraries..."

38 make verbosity

39− [ "-C", "lib", "check"

39+ [ "-C", "support", "check"

40 , "IDRIS=" ++ icmd

41 ]

42 make verbosity

43− [ "-C", "support", "check"

43+ [ "-C", "lib", "check"

44 , "IDRIS=" ++ icmd

45 ]

46

src/Idris/AbsSyntax.hs+17−3

@@ -8,6 +8,8 @@ import Core.Evaluate

8import Core.Elaborate hiding (Tactic(..))

9import Core.Typecheck

10

11+import Paths_idris

12+

11import System.Console.Haskeline

13import System.Console.Haskeline

12

14

13import Control.Monad.State

15import Control.Monad.State

@@ -29,11 +31,12 @@ data IOption = IOption { opt_logLevel :: Int,

29 opt_showimp :: Bool,

31 opt_showimp :: Bool,

30 opt_repl :: Bool,

32 opt_repl :: Bool,

31 opt_verbose :: Bool,

33 opt_verbose :: Bool,

32− opt_ibcsubdir :: FilePath

34+ opt_ibcsubdir :: FilePath,

35+ opt_importdirs :: [FilePath]

33 }

36 }

34 deriving (Show, Eq)

37 deriving (Show, Eq)

35

38

36−defaultOpts = IOption 0 False False True False True True ""

39+defaultOpts = IOption 0 False False True False True True "" []

37

40

38-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

41-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

39-- without typechecking).

42-- without typechecking).

@@ -321,12 +324,23 @@ setCoverage t = do i <- get

321setIBCSubDir :: FilePath -> Idris ()

324setIBCSubDir :: FilePath -> Idris ()

322setIBCSubDir fp = do i <- get

325setIBCSubDir fp = do i <- get

323 let opts = idris_options i

326 let opts = idris_options i

324− let opt' = opts { opt_ibcsubdir =fp }

327+ let opt' = opts { opt_ibcsubdir = fp }

325 put (i { idris_options = opt' })

328 put (i { idris_options = opt' })

326

329

327valIBCSubDir :: IState -> Idris FilePath

330valIBCSubDir :: IState -> Idris FilePath

328valIBCSubDir i = return (opt_ibcsubdir (idris_options i))

331valIBCSubDir i = return (opt_ibcsubdir (idris_options i))

329

332

333+setImportDirs :: [FilePath] -> Idris ()

334+setImportDirs fps = do i <- get

335+ let opts = idris_options i

336+ let opt' = opts { opt_importdirs = fps }

337+ put (i { idris_options = opt' })

338+

339+allImportDirs :: IState -> Idris [FilePath]

340+allImportDirs i = do datadir <- liftIO $ getDataDir

341+ let optdirs = opt_importdirs (idris_options i)

342+ return ("." : (optdirs ++ [datadir]))

343+

330impShow :: Idris Bool

344impShow :: Idris Bool

331impShow = do i <- get

345impShow = do i <- get

332 return (opt_showimp (idris_options i))

346 return (opt_showimp (idris_options i))

src/Idris/IBC.hs+3−3

@@ -155,10 +155,10 @@ timestampOlder src ibc = do srct <- getModificationTime src

155

156pImports :: [FilePath] -> Idris ()

157pImports fs

158− = do datadir <- liftIO $ getDataDir

159− mapM_ (\f -> do i <- getIState

158+ = do mapM_ (\f -> do i <- getIState

160 ibcsd <- valIBCSubDir i

159 ibcsd <- valIBCSubDir i

160+ ids <- allImportDirs i

161− fp <- liftIO $ findImport [".", datadir] ibcsd f

161+ fp <- liftIO $ findImport ids ibcsd f

162 if (f `elem` imported i)

163 then iLOG $ "Already read " ++ f

164 else do putIState (i { imported = f : imported i })

src/Idris/Parser.hs+3−3

@@ -57,10 +57,10 @@ lchar = lexeme.char

57

58loadModule :: FilePath -> Idris String

59loadModule f

60− = idrisCatch (do datadir <- liftIO $ getDataDir

61− i <- getIState

60+ = idrisCatch (do i <- getIState

62 ibcsd <- valIBCSubDir i

61 ibcsd <- valIBCSubDir i

62+ ids <- allImportDirs i

63− fp <- liftIO $ findImport [".", datadir] ibcsd f

63+ fp <- liftIO $ findImport ids ibcsd f

64 if (f `elem` imported i)

65 then iLOG $ "Already read " ++ f

66 else do putIState (i { imported = f : imported i })

src/Main.hs+9

@@ -41,6 +41,7 @@ data Opt = Filename String

41 | NoCoverage

42 | Verbose

43 | IBCSubDir String

44+ | ImportDir String

44 deriving Eq

45 deriving Eq

45

46

46main = do xs <- getArgs

47main = do xs <- getArgs

@@ -53,6 +54,7 @@ runIdris opts =

53 let runrepl = not (NoREPL `elem` opts)

54 let runrepl = not (NoREPL `elem` opts)

54 let output = opt getOutput opts

55 let output = opt getOutput opts

55 let ibcsubdir = opt getIBCSubDir opts

56 let ibcsubdir = opt getIBCSubDir opts

57+ let importdirs = opt getImportDir opts

56 when (Ver `elem` opts) $ liftIO showver

58 when (Ver `elem` opts) $ liftIO showver

57 when (Usage `elem` opts) $ liftIO usage

59 when (Usage `elem` opts) $ liftIO usage

58 setREPL runrepl

60 setREPL runrepl

@@ -62,6 +64,7 @@ runIdris opts =

62 case ibcsubdir of

64 case ibcsubdir of

63 [] -> setIBCSubDir ""

65 [] -> setIBCSubDir ""

64 (d:_) -> setIBCSubDir d

66 (d:_) -> setIBCSubDir d

67+ setImportDirs importdirs

65 elabPrims

68 elabPrims

66 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

69 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

67 return ()

70 return ()

@@ -94,6 +97,10 @@ getIBCSubDir :: Opt -> Maybe String

94getIBCSubDir (IBCSubDir str) = Just str

97getIBCSubDir (IBCSubDir str) = Just str

95getIBCSubDir _ = Nothing

98getIBCSubDir _ = Nothing

96

99

100+getImportDir :: Opt -> Maybe String

101+getImportDir (ImportDir str) = Just str

102+getImportDir _ = Nothing

103+

97opt :: (Opt -> Maybe a) -> [Opt] -> [a]

104opt :: (Opt -> Maybe a) -> [Opt] -> [a]

98opt = mapMaybe

105opt = mapMaybe

99

106

@@ -116,6 +123,7 @@ parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

116parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

123parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

117parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)

124parseArgs ("--verbose":ns) = liftM (Verbose : ) (parseArgs ns)

118parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)

125parseArgs ("--ibcsubdir":n:ns) = liftM (IBCSubDir n : ) (parseArgs ns)

126+parseArgs ("-i":n:ns) = liftM (ImportDir n : ) (parseArgs ns)

119parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

127parseArgs (n:ns) = liftM (Filename n : ) (parseArgs ns)

120

128

121ver = showVersion version

129ver = showVersion version

@@ -132,6 +140,7 @@ usagemsg = "Idris version " ++ ver ++ "\n" ++

132 "Options:\n" ++

140 "Options:\n" ++

133 "\t--check Type check only\n" ++

141 "\t--check Type check only\n" ++

134 "\t-o [file] Generate executable\n" ++

142 "\t-o [file] Generate executable\n" ++

143+ "\t-i [dir] Add directory to the list of import paths\n" ++

135 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++

144 "\t--ibcsubdir [dir] Write IBC files into sub directory\n" ++

136 "\t--noprelude Don't import the prelude\n" ++

145 "\t--noprelude Don't import the prelude\n" ++

137 "\t--typeintype Disable universe checking\n" ++

146 "\t--typeintype Disable universe checking\n" ++

support/threads.cnew file+111

@@ -0,0 +1,111 @@

1+#include <closure.h>

2+#include "threads.h"

3+

4+// Threads and locks

5+

6+typedef struct {

7+ pthread_mutex_t m_id;

8+} Mutex;

9+

10+typedef struct {

11+ pthread_t t_id;

12+} Thread;

13+

14+Mutex** ms = NULL;

15+int mutexes = 0;

16+

17+int idris_newLock(int sem)

18+{

19+ pthread_mutex_t m;

20+

21+ pthread_mutex_init(&m, NULL);

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

23+ newm->m_id = m;

24+

25+ // Increase space for the mutexes

26+ if (ms==NULL) {

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

28+ mutexes=1;

29+ } else {

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

31+ mutexes++;

32+ }

33+

34+ ms[mutexes-1] = newm;

35+ return mutexes-1;

36+}

37+

38+void idris_doLock(int lock)

39+{

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

41+}

42+

43+void idris_doUnlock(int lock)

44+{

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

46+}

47+

48+struct threadinfo {

49+ void* proc;

50+ void* result;

51+};

52+

53+void* idris_runThread(void* th_in) {

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

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

56+ th->result = v;

57+ return v;

58+}

59+

60+void idris_doFork(void* proc)

61+{

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

63+ struct threadinfo th;

64+ th.proc = proc;

65+ th.result = NULL;

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

67+}

68+

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

70+{

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

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

73+ struct threadinfo th;

74+ th.proc = proc;

75+ th.result = NULL;

76+

77+ struct timeval tv;

78+ gettimeofday(&tv, NULL);

79+ int tnow, tthen = do_utime();

80+

81+ pthread_create(t, NULL, idris_runThread, &th);

82+// printf("tthen %d\n", tthen);

83+

84+ void* ans;

85+

86+ do

87+ {

88+ // If the answer has been updated, we're done.

89+ if (th.result!=NULL) {

90+ pthread_join(*t, &ans);

91+ return ans;

92+ }

93+ gettimeofday(&tv, NULL);

94+ tnow = idris_utime();

95+ usleep(100);

96+// printf("tnow %d\n", tnow);

97+ }

98+ while(tnow<(tthen+(limit*1000)));

99+ pthread_cancel(*t);

100+ return DO_EVAL(doOnFail,1);

101+}

102+

103+int idris_utime() {

104+ struct timeval tv;

105+ gettimeofday(&tv, NULL);

106+

107+ static int start=0;

108+ if (start==0) { start = tv.tv_sec; }

109+

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

111+}

support/threads.hnew file+12

@@ -0,0 +1,12 @@

1+#ifndef _THREADS_H

2+#define _THREADS_H

3+

4+

5+int idris_newLock(int sem);

6+void idris_doLock(int lock);

7+void idris_doUnlock(int lock);

8+void idris_doFork(void* proc);

9+void* idris_doWithin(int limit, void* proc, void* doOnFail);

10+int idris_utime();

11+

12+#endif