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

git.iko.soy/Idris-dev

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

commit124f0e4d9b4769989adc877d0df8b1be9e513b14 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 17 Dec 2011, 15:10 (15 years ago) parentd9834c1 0f7b6d5

5 files changed+59−49

compare with master

unifiedsplit

Makefile−2 lib/prelude.idr+31−4 samples/interp.idr+1−1 src/Main.hs+23−17 test/test004/test004.idr+4−25

Makefile−2

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

11install: .PHONY

22 cabal install

3− make -C lib recheck

54pinstall: .PHONY

65 cabal configure --enable-executable-profiling

76 cabal install --enable-executable-profiling

8− make -C lib check

108build: .PHONY

119 cabal build

lib/prelude.idr+31−4

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

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

153153 return (FHandle h); };

154154

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+

155165do_fclose : Ptr -> IO ();

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

157167

158−fclose : File -> IO ();

159−fclose (FHandle h) = do_fclose h;

168+closeFile : File -> IO ();

169+closeFile (FHandle h) = do_fclose h;

160170

161171do_fread : Ptr -> IO String;

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

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

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

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

179189

180−

181−

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

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+ }

182209

samples/interp.idr+1−1

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

7777test = interp [] eProg 2 2;

7878

7979testFac : Int;

80−testFac = interp [] eFac 5;

80+testFac = interp [] eFac 4;

8181

8282main : IO ();

8383main = do { print testFac;

src/Main.hs+23−17

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

3030-- on with the REPL.

3131

3232data Opt = Filename String

33− | Version

33+ | Ver

34+ | Usage

3435 | NoPrelude

3536 | NoREPL

3637 | OLogging Int

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

4849 do let inputs = opt getFile opts

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

5051 let output = opt getOutput opts

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

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

5154 setREPL runrepl

5255 mapM_ makeOption opts

5356 elabPrims

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

6164 [] -> return ()

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

6366 when runrepl $ repl ist inputs

67+ ok <- noErrors

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

6469 where

6570 makeOption (OLogging i) = setLogLevel i

6671 makeOption TypeCase = setTypeCase True

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

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

7984opt = mapMaybe

8085

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

82− exitWith (ExitFailure 1)

86+usage = do putStrLn usagemsg

87+ exitWith ExitSuccess

88+

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

90+ exitWith ExitSuccess

8391

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

8593parseArgs [] = return []

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

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

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

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

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

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

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

93103

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−

108104ver = showVersion version

109105

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

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

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

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

115111

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 @@

11module 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−

243dumpFile : String -> IO ();

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

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

265 while (do { x <- feof h;

276 return (not x); })

287 (do { l <- fread h;

298 putStr l; });

30− fclose h; };

9+ closeFile h; };

3110

3211main : IO ();

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

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

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

35− fclose h;

14+ closeFile h;

3615 putStrLn "Reading testfile";

3716 f <- readFile "testfile";

3817 putStrLn f;