62419f4 · Idris-dev · git.iko.soy

src/Idris/REPL.hs+4−2

compare with master

unifiedsplit

@@ -1518,7 +1518,8 @@ loadInputs inputs toline -- furthest line to read in input source files

1518

1519idrisMain :: [Opt] -> Idris ()

1520idrisMain opts =

1521+ do mapM_ setWidth (opt getConsoleWidth opts)

1521− do let inputs = opt getFile opts

1522+ let inputs = opt getFile opts

1522 let quiet = Quiet `elem` opts

1523 let quiet = Quiet `elem` opts

1523 let nobanner = NoBanner `elem` opts

1524 let nobanner = NoBanner `elem` opts

1524 let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

1525 let idesl = Idemode `elem` opts || IdemodeSocket `elem` opts

@@ -1533,6 +1534,7 @@ idrisMain opts =

1533 let optimise = case opt getOptLevel opts of

1534 let optimise = case opt getOptLevel opts of

1534 [] -> 2

1535 [] -> 2

1535 xs -> last xs

1536 xs -> last xs

1537+

1536 setOptLevel optimise

1538 setOptLevel optimise

1537 let outty = case opt getOutputTy opts of

1539 let outty = case opt getOutputTy opts of

1538 [] -> if Interface `elem` opts then

1540 [] -> if Interface `elem` opts then

@@ -1555,7 +1557,7 @@ idrisMain opts =

1555 putIState (i { default_total = True })

1557 putIState (i { default_total = True })

1556 setColourise $ not quiet && last (True : opt getColour opts)

1558 setColourise $ not quiet && last (True : opt getColour opts)

1557

1559

1558− when (not runrepl) $ mapM_ setWidth (opt getConsoleWidth opts)

1560+

1559

1561

1560 mapM_ addLangExt (opt getLanguageExt opts)

1562 mapM_ addLangExt (opt getLanguageExt opts)

1561 setREPL runrepl

1563 setREPL runrepl

test/basic006/run+3−2

@@ -1,5 +1,6 @@

1#!/usr/bin/env bash

2+

2−idris $@ test020.idr -o test020

3+idris --consolewidth 80 $@ test020.idr -o test020

3−idris $@ test020a.idr --check --nocolor

4+idris --consolewidth 80 $@ test020a.idr --check --nocolor

4./test020

5./test020

5rm -f test020 *.ibc

6rm -f test020 *.ibc

test/basic009/run+6−3

@@ -1,5 +1,8 @@

1#!/usr/bin/env bash

2+

2−idris $@ Main.idr --nocolour --check && echo MAIN-PASS

3+idris --consolewidth 80 $@ Main.idr --nocolour --check && echo MAIN-PASS

3−idris $@ Faulty.idr --nocolour --check && echo FAULTY-PASS

4+idris --consolewidth 80 $@ Faulty.idr --nocolour --check && echo FAULTY-PASS

4−idris $@ Multiple.idr --nocolour --check && echo MULTIPLE-PASS

5+idris --consolewidth 80 $@ Multiple.idr --nocolour --check && echo MULTIPLE-PASS

6+

7+

5rm -f *.ibc B/*.ibc

8rm -f *.ibc B/*.ibc

test/docs001/expected+1−1

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

1Type checking ./docs001.idr

2−[?1049h[1;29r[m(B[4l[?7h[H[2J[29;1H[r[?1049l >Type class C

2+Type class C

3 class

4

5Parameters:

test/docs001/run+1−1

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

1#!/usr/bin/env bash

2−idris --nobanner --nocolor --consolewidth 80 docs001.idr < input

2+idris --quiet --nocolor --consolewidth 80 docs001.idr < input

3rm *.ibc

test/docs002/run+1−1

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

1#!/usr/bin/env bash

2−idris --nobanner --nocolor docs002.idr < input

2+idris --consolewidth 80 --nobanner --nocolor docs002.idr < input

3rm *.ibc

test/error003/expected+2−1

@@ -1,2 +1,3 @@

1+ErrorReflection.idr:68:5:

1−ErrorReflection.idr:68:5:When elaborating right hand side of bad:

2+When elaborating right hand side of bad:

2DSL type error: (t(503) => t'(504)) doesn't match ()

3DSL type error: (t(503) => t'(504)) doesn't match ()

test/error003/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ ErrorReflection.idr --nocolour --check

2+idris --consolewidth 80 $@ ErrorReflection.idr --nocolour --check

3rm -f *.ibc

test/error004/expected+6−3

@@ -1,6 +1,9 @@

1+FunErrTest.idr:35:10:

1−FunErrTest.idr:35:10:When elaborating right hand side of badCadr1:

2+When elaborating right hand side of badCadr1:

2When elaborating argument cons1 to function FunErrTest.cadr:

3When elaborating argument cons1 to function FunErrTest.cadr:

3 Could not prove that [] has at least two elements.

4 Could not prove that [] has at least two elements.

5+FunErrTest.idr:38:10:

4−FunErrTest.idr:38:10:When elaborating right hand side of badCadr2:

6+When elaborating right hand side of badCadr2:

5When elaborating argument cons2 to function FunErrTest.cadr:

7When elaborating argument cons2 to function FunErrTest.cadr:

6− Could not prove that tail [(fromInteger 1)] has at least two elements.

8+ Could not prove that tail [(fromInteger 1)] has at least two

9+ elements.

test/error004/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ FunErrTest.idr --nocolour --check

2+idris --consolewidth 80 $@ FunErrTest.idr --nocolour --check

3rm -f *.ibc

test/error005/expected+2−1

@@ -13,7 +13,8 @@ When elaborating argument prf to function Data.Fin.fromInteger:

13error005.idr:23:24:When elaborating right hand side of b0rken:

14When elaborating argument prf to function Data.Fin.fromInteger:

15 When using n as a literal for a Fin 3

16− Could not show that n is less than 3 because n is a bound variable instead of a constant Integer

16+ Could not show that n is less than 3 because n is a bound

17+ variable instead of a constant Integer

17error005.idr:28:1:When elaborating right hand side of x:

18error005.idr:28:1:When elaborating right hand side of x:

18When elaborating argument prf to function Data.Fin.fromInteger:

19When elaborating argument prf to function Data.Fin.fromInteger:

19 When using 5 as a literal for a Fin 4

20 When using 5 as a literal for a Fin 4

test/error005/run+1−1

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

1#!/usr/bin/env bash

2−idris $@ --check --nocolour error005.idr

2+idris --consolewidth 80 $@ --check --nocolour error005.idr

3rm -f *.ibc

test/ffi002/run+1−1

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

1#!/usr/bin/env bash

2−idris --quiet test023.idr -o test023

2+idris --consolewidth 80 --quiet test023.idr -o test023

3rm -f test023 *.ibc

test/literate001/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ test003a.lidr --check

2+idris --consolewidth 80 $@ test003a.lidr --check

3−idris $@ test003.lidr -o test003

3+idris --consolewidth 80 $@ test003.lidr -o test003

4./test003

5rm -f test003 test003.ibc Lit.ibc

test/proof002/expected+2−1

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

1+Reflect.idr:208:38:

1−Reflect.idr:208:38:When elaborating right hand side of testReflect1:

2+When elaborating right hand side of testReflect1:

2When elaborating an application of function Reflect.getJust:

3When elaborating an application of function Reflect.getJust:

3 Can't unify

4 Can't unify

4 IsJust (Just x1) (Type of ItIsJust)

5 IsJust (Just x1) (Type of ItIsJust)

test/proof002/run+2−2

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

1#!/usr/bin/env bash

2−idris $@ test030.idr --check --nocolour

2+idris --consolewidth 80 $@ test030.idr --check --nocolour

3−idris $@ test030a.idr --check --nocolour

3+idris --consolewidth 80 $@ test030a.idr --check --nocolour

4rm -f *.ibc

test/proof007/expected+2−1

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

1+DefaultArgUnknownName.idr:9:6:

1−DefaultArgUnknownName.idr:9:6:When elaborating right hand side of test:

2+When elaborating right hand side of test:

2When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3When elaborating argument [95marg[0m to function [92mDefaultArgUnknownName.funWithBadDefArg[0m:

3 No such variable sadgjhsag

4 No such variable sadgjhsag

test/proof007/run+1−1

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

1#!/usr/bin/env bash

2−idris --check $@ DefaultArgUnknownName.idr

2+idris --consolewidth 80 --check $@ DefaultArgUnknownName.idr

3rm -f *.ibc