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

git.iko.soy/Idris-dev

Merge remote-tracking branch 'refs/remotes/upstream/master' into wip/tactical

commit91649d42ee72e4af373bed24ddffe867218ef131 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 16 May 2015, 19:38 (11 years ago) parentac26e38 4ad2949

11 files changed+36−18

compare with master

unifiedsplit

.travis.yml+1−1 libs/prelude/Prelude.idr+8−4 rts/idris_rts.c−2 src/IRTS/CodegenC.hs+2−1 src/IRTS/System.hs+8−1 src/Idris/Core/Evaluate.hs+9−4 src/Idris/Core/Typecheck.hs+4−1 test/dsl002/test014.idr+2−1 test/effects001/expected+1−1 test/io001/expected−1 test/io001/test004.idr+1−1

.travis.yml+1−1

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

1919 - sudo apt-get install -qq cppcheck

2020 - cabal install alex-3.1.3

2121install:

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

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

2323 - ghc-pkg list

2424before_script:

2525 - cabal sdist

libs/prelude/Prelude.idr+8−4

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

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

353353partial

354354getLine : 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

356362

357363||| Write a single character to stdout

358364partial

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

548554 readFile' h contents =

549555 do x <- feof h

550556 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)

554558 else return contents

rts/idris_rts.c−2

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

509509 size_t n = 0;

510510 ssize_t len;

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

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

513−

514512 if (len <= 0) {

515513 ret = MKSTR(vm, "");

516514 } else {

src/IRTS/CodegenC.hs+2−1

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

7373 comp <- getCC

7474 libFlags <- getLibFlags

7575 incFlags <- getIncFlags

76+ envFlags <- getEnvFlags

7677 let args = [gccDbg dbg] ++

7778 gccFlags iface ++

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

7980 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

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

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

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

8283 [tmpn] ++

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

src/IRTS/System.hs+8−1

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

11{-# LANGUAGE CPP #-}

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

3− getIncFlags,getMvn,getExecutablePom, version) where

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

55import Util.System

6+import Data.List.Split

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

89import Data.Maybe (fromMaybe)

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

1920getCC :: IO String

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

2122

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+

2229mvnCommand :: String

2330#ifdef mingw32_HOST_OS

2431mvnCommand = "mvn.bat"

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

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

10071007 _ -> False

10081008

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

1010−lookupP = lookupP_all False

1010+lookupP = lookupP_all False False

10111011

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

1013−lookupP_all all n ctxt

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

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

1013+lookupP_all all exact n ctxt

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

10151015 p <- case def of

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

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

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

10201020 case snd p of

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

10221022 _ -> 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

10231028

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

10251030lookupDefExact 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

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

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

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

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

9194 | otherwise = do lift $ tfail $ NoSuchVariable n

9295 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

3434syntax reof [h] = Use eof h

3535

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

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

3738

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

3940

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

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

5859 if opened x then

5960 do str <- rreadLine x

60− rputStrLn str

61+ rputStr str

6162 rclose x

6263 else rputStrLn "Error")

6364

test/effects001/expected+1−1

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

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

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

223

3315

44Answer: 99

test/io001/expected−1

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

13133

14144

1515Last line

16−

1716---

test/io001/test004.idr+1−1

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

1313 x <- feof h

1414 return (not x) })

1515 (do { l <- fread h

16− putStrLn l })

16+ putStr l })

1717 closeFile h }

1818

1919main : IO ()