f2bada8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3818 from jdevuyst/master

[Issue 3774] Have :exec print the value of IO _ expressions

commitf2bada80fb8c97c8583723585486e9ad2e9a88c2 authorNiklas Larsson <metaniklas@gmail.com> dateWed 24 May 2017, 11:48 (9 years ago) parentd176fb3 1f273b9

7 files changed+32−9

compare with master

unifiedsplit

src/Idris/Elab/Value.hs+5−2 test/README.md−6 test/TestData.hs+2−1 test/interactive014/expected+7 test/interactive014/input+5 test/interactive014/interactive014.idr+10 test/interactive014/run+3

src/Idris/Elab/Value.hs+5−2

@@ -123,13 +123,16 @@ elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

123123 else Checked tm

124124 | otherwise = Unchecked

125125

126−-- | Try running the term directly (as IO ()), then printing it as an Integer

127−-- (as a default numeric tye), then printing it as any Showable thing

126+-- | Try running the term directly (as IO ()) or with >>= printLn appended

127+-- (for other IO _), then printing it as an Integer (as a default numeric

128+-- type), then printing it as any Showable thing

128129elabExec :: FC -> PTerm -> PTerm

129130elabExec fc tm = runtm (PAlternative [] FirstSuccess

130131 [printtm (PApp fc (PRef fc [] (sUN "the"))

131132 [pexp (PConstant NoFC (AType (ATInt ITBig))), pexp tm]),

132133 tm,

134+ PApp fc (PRef fc [] (sUN ">>="))

135+ [pexp tm, pexp (PRef fc [] (sUN "printLn"))],

133136 printtm tm

134137 ])

135138 where

test/README.md−6

@@ -124,12 +124,6 @@ and somewhat self-explanatory.

124124 stack test --test-arguments="--pattern foo042 --accept"

125125 ```

1261268. Check the content of `expected`. Maybe the test didn't do what you thought it would. Fix and go back to 7 until it's ok.

127−9. Add under `Extra-source-files` in `idris.cabal` the patterns that match the folder's content. If you forget this, your test will fail in Travis CI. With the previous example, it should be at least:

128− ```

129− test/foo042/run

130− test/foo042/expected

131− test/foo042/*.idr

132− ```

133127

134128### Specifying compatible backends

135129

test/TestData.hs+2−1

@@ -153,7 +153,8 @@ testFamiliesData = [

153153 ( 10, ANY ),

154154 ( 11, ANY ),

155155 ( 12, ANY ),

156− ( 13, ANY )]),

156+ ( 13, ANY ),

157+ ( 14, C_CG )]),

157158 ("interfaces", "Interfaces",

158159 [ ( 1, ANY ),

159160 ( 2, ANY ),

test/interactive014/expectednew file+7

@@ -0,0 +1,7 @@

1+aa

2+bb

3+123

4+cc

5+"dd"

6+456

7+"xyz"

test/interactive014/inputnew file+5

@@ -0,0 +1,5 @@

1+:exec voidIO

2+:exec intIO

3+:exec stringIO

4+:exec 456

5+:exec "xyz"

test/interactive014/interactive014.idrnew file+10

@@ -0,0 +1,10 @@

1+voidIO : IO ()

2+voidIO = do putStrLn "aa"

4+intIO : IO Int

5+intIO = do putStrLn "bb"

6+ pure 123

8+stringIO : IO String

9+stringIO = do putStrLn "cc"

10+ pure "dd"

test/interactive014/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --quiet --port none interactive014.idr < input

3+rm -f *.ibc