git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1511 from tac-tics/basic-repl-test

Add test for basic REPL commands

commit99fe3e8f332b005439df9261933be5f1ca0799bf authorDavid Christiansen <david@davidchristiansen.dk> dateThu 11 Sep 2014, 16:56 (12 years ago) parent52407a9e0f815a
5 files changed+66
compare with master
unifiedsplit
idris.cabal+4 test/interactive005/expected+33 test/interactive005/input+21 test/interactive005/interactive005.idr+3 test/interactive005/run+5
idris.cabal+4
@@ -391,6 +391,10 @@ Extra-source-files:
391391 test/interactive004/input
392392 test/interactive004/*.idr
393393 test/interactive004/expected
394+ test/interactive005/run
395+ test/interactive005/input
396+ test/interactive005/*.idr
397+ test/interactive005/expected
394398
395399 test/io001/run
396400 test/io001/*.idr
test/interactive005/expectednew file+33
@@ -0,0 +1,33 @@
1+Type checking ./interactive005.idr
2+3 : Nat
3+Hello, World
4+main : IO ()
5+ This is a docstring
6+
7+Main.main is Total
8+Hello, World
9+Prelude.Basics.id : a -> a
10+Prelude.Basics.id : {a : Type} -> (__pi_arg : a) -> a
11+Prelude.Basics.id : a -> a
12+
13+ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY
14+ EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
15+ IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
16+ PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE
17+ LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
18+ CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
19+ SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR
20+ BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
21+ WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE
22+ OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
23+ IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
24+
25+main : IO ()
26+ This
27+ is a
28+ docstring
29+
30+main : IO ()
31+ This is a docstring
32+
33+Nat2 : Type
test/interactive005/inputnew file+21
@@ -0,0 +1,21 @@
1+the Nat (1 + 2)
2+:exec
3+:c bytecode hello.bytecode
4+:c c hello
5+:doc main
6+:reload
7+:load interactive005.idr
8+:total main
9+:exec
10+:t id
11+:set showimplicits
12+:t id
13+:unset showimplicits
14+:t id
15+:warranty
16+:consolewidth 10
17+:doc main
18+:consolewidth infinite
19+:doc main
20+:let data Nat2 = Zero | Succ Nat2
21+:t Nat2
test/interactive005/interactive005.idrnew file+3
@@ -0,0 +1,3 @@
1+||| This is a docstring
2+main : IO ()
3+main = putStrLn "Hello, World"
test/interactive005/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+idris --quiet interactive005.idr < input
3+rm -f *.ibc
4+rm -f hello.bytecode
5+rm -f hello