91649d4 · Idris-dev · git.iko.soy

.travis.yml+1−1

compare with master

unifiedsplit

@@ -19,7 +19,7 @@ before_install:

19 - sudo apt-get install -qq cppcheck

20 - cabal install alex-3.1.3

21install:

22− - cabal install -f FFI --enable-tests --dependencies-only

22+ - cabal install -f FFI --enable-tests --dependencies-only --max-backjumps=-1

23 - ghc-pkg list

24before_script:

25 - cabal sdist

libs/prelude/Prelude.idr+8−4

@@ -352,7 +352,13 @@ printLn x = putStrLn (show x)

352||| Read one line of input from stdin, without the trailing newline

353partial

354getLine : IO' ffi String

355−getLine = prim_read

355+getLine = do x <- prim_read

356+ return (reverse (trimNL (reverse x)))

357+ where trimNL : String -> String

358+ trimNL str with (strM str)

359+ trimNL "" | StrNil = ""

360+ trimNL (strCons '\n' xs) | StrCons _ _ = xs

361+ trimNL (strCons x xs) | StrCons _ _ = strCons x xs

356

362

357||| Write a single character to stdout

363||| Write a single character to stdout

358partial

364partial

@@ -548,7 +554,5 @@ readFile fn = do h <- openFile fn Read

548 readFile' h contents =

554 readFile' h contents =

549 do x <- feof h

555 do x <- feof h

550 if not x then do l <- fread h

556 if not x then do l <- fread h

551− case contents of

552− "" => readFile' h l

553− _ => readFile' h (contents ++ "\n" ++ l)

557+ readFile' h (contents ++ l)

554 else return contents

558 else return contents

rts/idris_rts.c−2

@@ -509,8 +509,6 @@ VAL idris_readStr(VM* vm, FILE* h) {

509 size_t n = 0;

510 ssize_t len;

511 len = getline(&buffer, &n, h);

512− strtok(buffer, "\n");

513−

514 if (len <= 0) {

512 if (len <= 0) {

515 ret = MKSTR(vm, "");

513 ret = MKSTR(vm, "");

516 } else {

514 } else {

src/IRTS/CodegenC.hs+2−1

@@ -73,11 +73,12 @@ codegenC' defs out exec incs objs libs flags exports iface dbg

73 comp <- getCC

74 libFlags <- getLibFlags

75 incFlags <- getIncFlags

76+ envFlags <- getEnvFlags

76 let args = [gccDbg dbg] ++

77 let args = [gccDbg dbg] ++

77 gccFlags iface ++

78 gccFlags iface ++

78 -- # Any flags defined here which alter the RTS API must also be added to config.mk

79 -- # Any flags defined here which alter the RTS API must also be added to config.mk

79 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

80 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

80− "-I."] ++ objs ++ ["-x", "c"] ++

81+ "-I."] ++ objs ++ ["-x", "c"] ++ envFlags ++

81 (if (exec == Executable) then [] else ["-c"]) ++

82 (if (exec == Executable) then [] else ["-c"]) ++

82 [tmpn] ++

83 [tmpn] ++

83 (if not iface then concatMap words libFlags else []) ++

84 (if not iface then concatMap words libFlags else []) ++

src/IRTS/System.hs+8−1

@@ -1,8 +1,9 @@

1{-# LANGUAGE CPP #-}

2module IRTS.System(getDataFileName, getDataDir, getTargetDir,getCC,getLibFlags,getIdrisLibDir,

3− getIncFlags,getMvn,getExecutablePom, version) where

3+ getIncFlags, getEnvFlags, getMvn,getExecutablePom, version) where

4

5import Util.System

6+import Data.List.Split

6

7

7import Control.Applicative ((<$>))

8import Control.Applicative ((<$>))

8import Data.Maybe (fromMaybe)

9import Data.Maybe (fromMaybe)

@@ -19,6 +20,12 @@ import Paths_idris

19getCC :: IO String

20getCC :: IO String

20getCC = fromMaybe "gcc" <$> environment "IDRIS_CC"

21getCC = fromMaybe "gcc" <$> environment "IDRIS_CC"

21

22

23+getEnvFlags :: IO [String]

24+getEnvFlags = do flags <- environment "IDRIS_CFLAGS"

25+ case flags of

26+ Nothing -> return $ []

27+ Just s -> return $ splitOn " " s

28+

22mvnCommand :: String

29mvnCommand :: String

23#ifdef mingw32_HOST_OS

30#ifdef mingw32_HOST_OS

24mvnCommand = "mvn.bat"

31mvnCommand = "mvn.bat"

src/Idris/Core/Evaluate.hs+9−4

@@ -1007,11 +1007,11 @@ isTCDict n ctxt

1007 _ -> False

1008

1009lookupP :: Name -> Context -> [Term]

1010−lookupP = lookupP_all False

1010+lookupP = lookupP_all False False

1011

1012−lookupP_all :: Bool -> Name -> Context -> [Term]

1012+lookupP_all :: Bool -> Bool -> Name -> Context -> [Term]

1013−lookupP_all all n ctxt

1013+lookupP_all all exact n ctxt

1014− = do (n', def) <- lookupCtxtName n (definitions ctxt)

1014+ = do (n', def) <- names

1015 p <- case def of

1016 (Function ty tm, a, _, _) -> return (P Ref n' ty, a)

1017 (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)

@@ -1020,6 +1020,11 @@ lookupP_all all n ctxt

1020 case snd p of

1021 Hidden -> if all then return (fst p) else []

1022 _ -> return (fst p)

1023+ where

1024+ names = let ns = lookupCtxtName n (definitions ctxt) in

1025+ if exact

1026+ then filter (\ (n', d) -> n' == n) ns

1027+ else ns

1023

1028

1024lookupDefExact :: Name -> Context -> Maybe Def

1029lookupDefExact :: Name -> Context -> Maybe Def

1025lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

1030lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

src/Idris/Core/Typecheck.hs+4−1

@@ -86,7 +86,10 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

86 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

87 -- If we're elaborating, we don't want the private names; if we're

88 -- checking an already elaborated term, we do

89− | [P nt n' ty] <- lookupP_all (not holes) n ctxt

89+ | [P nt n' ty] <- lookupP_all (not holes) False n ctxt

90+ = return (P nt n' ty, ty)

91+ -- If the names are ambiguous, require it to be fully qualified

92+ | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

90 = return (P nt n' ty, ty)

93 = return (P nt n' ty, ty)

91 | otherwise = do lift $ tfail $ NoSuchVariable n

94 | otherwise = do lift $ tfail $ NoSuchVariable n

92 chk u env ap@(RApp f RType) | not holes

95 chk u env ap@(RApp f RType) | not holes

test/dsl002/test014.idr+2−1

@@ -34,6 +34,7 @@ syntax rreadLine [h] = Use readLine h

34syntax reof [h] = Use eof h

35

36syntax rputStrLn [s] = Lift (putStrLn s)

37+syntax rputStr [s] = Lift (putStr s)

37

38

38syntax "if" "opened" [f] "then" [e] "else" [t] = Check f t e

39syntax "if" "opened" [f] "then" [e] "else" [t] = Check f t e

39

40

@@ -57,7 +58,7 @@ readH : String -> RES ()

57readH fn = res (do let x = open fn Reading

58readH fn = res (do let x = open fn Reading

58 if opened x then

59 if opened x then

59 do str <- rreadLine x

60 do str <- rreadLine x

60− rputStrLn str

61+ rputStr str

61 rclose x

62 rclose x

62 else rputStrLn "Error")

63 else rputStrLn "Error")

63

64

test/effects001/expected+1−1

@@ -1,4 +1,4 @@

1−["HELLO!!!", "WORLD!!!", ""]

1+["HELLO!!!\n", "WORLD!!!\n", ""]

23

315

4Answer: 99

test/io001/expected−1

@@ -13,5 +13,4 @@ World!

133

144

15Last line

16−

17---

16---

test/io001/test004.idr+1−1

@@ -13,7 +13,7 @@ dumpFile fn = do { h <- openFile fn Read

13 x <- feof h

14 return (not x) })

15 (do { l <- fread h

16− putStrLn l })

16+ putStr l })

17 closeFile h }

18

19main : IO ()