124f0e4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:edwinb/MiniIdris

124f0e4Edwin Brady15 years ago

Makefile−2

compare with master

unifiedsplit

@@ -1,11 +1,9 @@

1install: .PHONY

2 cabal install

3− make -C lib recheck

5pinstall: .PHONY

4pinstall: .PHONY

6 cabal configure --enable-executable-profiling

5 cabal configure --enable-executable-profiling

7 cabal install --enable-executable-profiling

6 cabal install --enable-executable-profiling

8− make -C lib check

10build: .PHONY

8build: .PHONY

11 cabal build

9 cabal build

lib/prelude.idr+31−4

@@ -152,11 +152,21 @@ fopen : String -> String -> IO File;

152fopen f m = do { h <- do_fopen f m;

153 return (FHandle h); };

154

155+data Mode = Read | Write | ReadWrite;

156+

157+openFile : String -> Mode -> IO File;

158+openFile f m = fopen f (modeStr m) where {

159+ modeStr : Mode -> String;

160+ modeStr Read = "r";

161+ modeStr Write = "w";

162+ modeStr ReadWrite = "r+";

163+}

164+

155do_fclose : Ptr -> IO ();

165do_fclose : Ptr -> IO ();

156do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;

166do_fclose h = mkForeign (FFun "fileClose" [FPtr] FUnit) h;

157

167

158−fclose : File -> IO ();

168+closeFile : File -> IO ();

159−fclose (FHandle h) = do_fclose h;

169+closeFile (FHandle h) = do_fclose h;

160

170

161do_fread : Ptr -> IO String;

171do_fread : Ptr -> IO String;

162do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;

172do_fread h = mkForeign (FFun "freadStr" [FPtr] FString) h;

@@ -177,6 +187,23 @@ feof : File -> IO Bool;

177feof (FHandle h) = do { eof <- do_feof h;

187feof (FHandle h) = do { eof <- do_feof h;

178 return (not (eof == 0)); };

188 return (not (eof == 0)); };

179

189

180−

190+while : |(test : IO Bool) -> |(body : IO ()) -> IO ();

181−

191+while t b = do { v <- t;

192+ if v then (do { b; while t b; }) else return (); };

193+

194+readFile : String -> IO String;

195+readFile fn = do { h <- openFile fn Read;

196+ c <- readFile' h "";

197+ closeFile h;

198+ return c;

199+ }

200+ where {

201+ readFile' : File -> String -> IO String;

202+ readFile' h contents =

203+ do { x <- feof h;

204+ if (not x) then (do { l <- fread h;

205+ readFile' h (contents ++ l);

206+ })

207+ else (return contents); };

208+ }

182

209

samples/interp.idr+1−1

@@ -77,7 +77,7 @@ test : Int;

77test = interp [] eProg 2 2;

79testFac : Int;

80−testFac = interp [] eFac 5;

80+testFac = interp [] eFac 4;

82main : IO ();

83main = do { print testFac;

src/Main.hs+23−17

@@ -30,7 +30,8 @@ import Paths_idris

30-- on with the REPL.

32data Opt = Filename String

33− | Version

33+ | Ver

34+ | Usage

34 | NoPrelude

35 | NoPrelude

35 | NoREPL

36 | NoREPL

36 | OLogging Int

37 | OLogging Int

@@ -48,6 +49,8 @@ runIdris opts =

48 do let inputs = opt getFile opts

49 do let inputs = opt getFile opts

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

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

50 let output = opt getOutput opts

51 let output = opt getOutput opts

52+ when (Ver `elem` opts) $ lift showver

53+ when (Usage `elem` opts) $ lift usage

51 setREPL runrepl

54 setREPL runrepl

52 mapM_ makeOption opts

55 mapM_ makeOption opts

53 elabPrims

56 elabPrims

@@ -61,6 +64,8 @@ runIdris opts =

61 [] -> return ()

64 [] -> return ()

62 (o:_) -> process (Compile o)

65 (o:_) -> process (Compile o)

63 when runrepl $ repl ist inputs

66 when runrepl $ repl ist inputs

67+ ok <- noErrors

68+ when (not ok) $ lift (exitWith (ExitFailure 1))

64 where

69 where

65 makeOption (OLogging i) = setLogLevel i

70 makeOption (OLogging i) = setLogLevel i

66 makeOption TypeCase = setTypeCase True

71 makeOption TypeCase = setTypeCase True

@@ -78,8 +83,11 @@ getOutput _ = Nothing

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

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

79opt = mapMaybe

84opt = mapMaybe

81−usage = do putStrLn "You're doing it wrong"

86+usage = do putStrLn usagemsg

82− exitWith (ExitFailure 1)

87+ exitWith ExitSuccess

88+

89+showver = do putStrLn $ "Idris version " ++ ver

90+ exitWith ExitSuccess

84parseArgs :: [String] -> IO [Opt]

92parseArgs :: [String] -> IO [Opt]

85parseArgs [] = return []

93parseArgs [] = return []

@@ -89,22 +97,10 @@ parseArgs ("--check":ns) = liftM (NoREPL : ) (parseArgs ns)

89parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)

97parseArgs ("-o":n:ns) = liftM (\x -> NoREPL : Output n : x) (parseArgs ns)

90parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

98parseArgs ("--typecase":ns) = liftM (TypeCase : ) (parseArgs ns)

91parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

99parseArgs ("--typeintype":ns) = liftM (TypeInType : ) (parseArgs ns)

100+parseArgs ("--help":ns) = liftM (Usage : ) (parseArgs ns)

101+parseArgs ("--version":ns) = liftM (Ver : ) (parseArgs ns)

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

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

103

94−{-

95−main'

96− = do f <- readFile "test.mi"

97− case parseFile f of

98− Left err -> print err

99− Right defs -> do

100− print defs

101− case checkProgram emptyContext defs of

102− OK ctxt -> do print (toAlist ctxt)

103− runShell (initState ctxt)

104− return ()

105− err -> print err

106− -}

107−

108ver = showVersion version

104ver = showVersion version

109

105

110banner = " ____ __ _ \n" ++

106banner = " ____ __ _ \n" ++

@@ -113,3 +109,13 @@ banner = " ____ __ _ \n" ++

113 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

109 " _/ // /_/ / / / (__ ) http://www.idris-lang.org/ \n" ++

114 " /___/\\__,_/_/ /_/____/ Type :? for help \n"

110 " /___/\\__,_/_/ /_/____/ Type :? for help \n"

115

111

112+usagemsg = "Idris version " ++ ver ++ "\n" ++

113+ "--------------" ++ map (\x -> '-') ver ++ "\n" ++

114+ "Usage: idris [input file] [options]\n" ++

115+ "Options:\n" ++

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

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

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

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

120+ "\t--log [level] Set debugging log level\n"

121+

test/test004/test004.idr+4−25

@@ -1,38 +1,17 @@

1module main;

3−while : |(test : IO Bool) -> |(body : IO ()) -> IO ();

4−while t b = do { v <- t;

5− if v then (do { b; while t b; }) else return (); };

6−

7−

8−readFile : String -> IO String;

9−readFile fn = do { h <- fopen fn "r";

10− c <- readFile' h "";

11− fclose h;

12− return c;

13− }

14− where {

15− readFile' : File -> String -> IO String;

16− readFile' h contents =

17− do { x <- feof h;

18− if (not x) then (do { l <- fread h;

19− readFile' h (contents ++ l);

20− })

21− else (return contents); };

22− }

23−

24dumpFile : String -> IO ();

3dumpFile : String -> IO ();

25−dumpFile fn = do { h <- fopen fn "r";

4+dumpFile fn = do { h <- openFile fn Read;

26 while (do { x <- feof h;

5 while (do { x <- feof h;

27 return (not x); })

6 return (not x); })

28 (do { l <- fread h;

7 (do { l <- fread h;

29 putStr l; });

8 putStr l; });

30− fclose h; };

9+ closeFile h; };

32main : IO ();

11main : IO ();

33−main = do { h <- fopen "testfile" "w";

12+main = do { h <- openFile "testfile" Write;

34 fwrite h "Hello!\nWorld!\n";

13 fwrite h "Hello!\nWorld!\n";

35− fclose h;

14+ closeFile h;

36 putStrLn "Reading testfile";

15 putStrLn "Reading testfile";

37 f <- readFile "testfile";

16 f <- readFile "testfile";

38 putStrLn f;

17 putStrLn f;