bfc3c3e · Idris-dev · git.iko.soy

CHANGELOG+3−3

compare with master

unifiedsplit

@@ -5,7 +5,7 @@ New in 0.9.12:

5 type inference.

6* New 'Lazy' type, replacing laziness annotations.

7* JavaScript and Node codegen now understand the %include directive.

8−* Concept up 'null' is now understood in the JavaScript and Node codegen.

8+* Concept of 'null' is now understood in the JavaScript and Node codegen.

9* Lots of performance patches for generated JavaScript.

10* New commands :eval (:e) and :type (:t) in the prover, which either normalise

11 or show the type of expressions.

@@ -17,8 +17,8 @@ New in 0.9.12:

17 ||| @ n the first number (examined by the function)

18 ||| @ m the second number (not examined)

19 plus (n, m : Nat) -> Nat

20−* Allow the auto-solve behavior in the prover to be disabled, for easier debugging

20+* Allow the auto-solve behaviour in the prover to be disabled, for easier

21− of proof automation. Use ":set autosolve" and ":unset autosolve".

21+ debugging of proof automation. Use ":set autosolve" and ":unset autosolve".

22* Updated 'effects' library

23* New :apropos command at REPL to search documentation, names, and types

24* Unification errors are now slightly more informative

README+1−1

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

1−Idris (http://idris-lang.org/) is an experimental functional programming

1+Idris (http://idris-lang.org/) is a general-purpose functional programming

2language with dependent types.

3

4To configure, edit config.mk. The default values should work for most people.

idris.cabal+2−1

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

1Name: idris

2−Version: 0.9.11.2

2+Version: 0.9.12

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

@@ -476,6 +476,7 @@ Library

476 , Idris.IdeSlave

477 , Idris.Imports

478 , Idris.Inliner

479+ , Idris.Output

479 , Idris.Parser

480 , Idris.Parser

480 , Idris.ParseHelpers

481 , Idris.ParseHelpers

481 , Idris.ParseOps

482 , Idris.ParseOps

libs/base/Data/HVect.idr+1

@@ -19,6 +19,7 @@ using (k : Nat, ts : Vect k Type)

19 deleteAt : {us : Vect (S l) Type} -> (i : Fin (S l)) -> HVect us -> HVect (deleteAt i us)

20 deleteAt fZ (x::xs) = xs

21 deleteAt {l = S m} (fS j) (x::xs) = x :: deleteAt j xs

22+ deleteAt {l = Z} (fS j) (x::xs) = absurd j

22 deleteAt _ [] impossible

23 deleteAt _ [] impossible

23

24

24 replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)

25 replaceAt : (i : Fin k) -> t -> HVect ts -> HVect (replaceAt i t ts)

libs/effects/Effect/File.idr+85−14

@@ -1,24 +1,78 @@

1+-- -------------------------------------------------------- [ Effectful FileIO ]

1module Effect.File

2module Effect.File

2

3

3import Effects

4import Effects

4import Control.IOExcept

5import Control.IOExcept

5

6

7+

8+||| A Dependent type to describe File Handles. File handles are

9+||| parameterised with the current state of the file: Closed; Open for

10+||| reading; and Open for writing.

11+|||

12+||| @ m The file mode.

6−data OpenFile : Mode -> Type where

13+data OpenFile : (m : Mode) -> Type where

7 FH : File -> OpenFile m

14 FH : File -> OpenFile m

8

15

9openOK : Mode -> Bool -> Type

16openOK : Mode -> Bool -> Type

10openOK m True = OpenFile m

17openOK m True = OpenFile m

11openOK m False = ()

18openOK m False = ()

12

19

20+-- ------------------------------------------------------------ [ The Protocol ]

21+

22+||| Here the protocol for resource access is defined as an effect.

23+||| The state transitions diagram for the protocol is as follows:

24+|||

25+||| digraph G {

26+|||

27+||| empty; read; write; // States

28+|||

29+||| empty -> read [label="Open R"];

30+||| read -> empty [label="Close"];

31+||| read -> read [label="ReadLine"];

32+||| read -> read [label="EOF"];

33+|||

34+||| empty -> write [label="Open W"];

35+||| write -> empty [label="Close"];

36+||| write -> write [label="WriteLine"];

37+|||

38+||| }

13data FileIO : Effect where

39data FileIO : Effect where

40+ ||| Open a file with the specified mode.

41+ |||

42+ ||| Opening a file successful moves the state from 'empty' to the

43+ ||| specified mode. If not successful the state is still 'empty'.

44+ |||

45+ ||| @ fname The file name to be opened.

46+ ||| @ m The file mode.

47+ Open : (fname: String)

14− Open : String -> (m : Mode) ->

48+ -> (m : Mode)

49+ -> {() ==> {res} if res

50+ then OpenFile m

15− {() ==> {res} if res then OpenFile m else ()} FileIO Bool

51+ else ()} FileIO Bool

52+

53+ ||| Close a file.

54+ |||

55+ ||| Closing a file moves the state from Open to closed.

16− Close : {OpenFile m ==> ()} FileIO ()

56+ Close : {OpenFile m ==> ()} FileIO ()

17−

57+

58+ ||| Read a line from the file.

59+ |||

60+ ||| Only files that are open for reading can be read.

18− ReadLine : {OpenFile Read} FileIO String

61+ ReadLine : {OpenFile Read} FileIO String

62+

63+ ||| Write a line to a file.

64+ |||

65+ ||| Only file that are open for writing can be written to.

19− WriteLine : String -> {OpenFile Write} FileIO ()

66+ WriteLine : String -> {OpenFile Write} FileIO ()

67+

68+ ||| End of file?

69+ |||

70+ ||| Only files open for reading can be tested for EOF

20− EOF : {OpenFile Read} FileIO Bool

71+ EOF : {OpenFile Read} FileIO Bool

21−

72+

73+-- ------------------------------------------------------------ [ The Handlers ]

74+

75+--- An implementation of the resource access protocol for the IO Context.

22instance Handler FileIO IO where

76instance Handler FileIO IO where

23 handle () (Open fname m) k = do h <- openFile fname m

77 handle () (Open fname m) k = do h <- openFile fname m

24 valid <- validFile h

78 valid <- validFile h

@@ -33,30 +87,47 @@ instance Handler FileIO IO where

33 handle (FH h) EOF k = do e <- feof h

87 handle (FH h) EOF k = do e <- feof h

34 k e (FH h)

88 k e (FH h)

35

89

90+-- -------------------------------------------------------------- [ The Effect ]

36FILE_IO : Type -> EFFECT

91FILE_IO : Type -> EFFECT

37FILE_IO t = MkEff t FileIO

92FILE_IO t = MkEff t FileIO

38

93

94+-- ------------------------------------------------------------ [ The Bindings ]

95+--

96+-- Bind the IO context handlers to functions. These functions will run

97+-- in the IO context.

98+--

99+

100+||| Open a file with the specified mode.

101+|||

102+||| @ fname The file name to be opened.

103+||| @ m The file mode.

39open : Handler FileIO e =>

104open : Handler FileIO e =>

105+ (fname : String)

40− String -> (m : Mode) ->

106+ -> (m : Mode)

41− { [FILE_IO ()] ==> [FILE_IO (if result then OpenFile m else ())] } Eff e Bool

107+ -> { [FILE_IO ()] ==> [FILE_IO (if result

108+ then OpenFile m

109+ else ())] } Eff e Bool

42open f m = Open f m

110open f m = Open f m

43

111

112+

113+||| Close a file.

44close : Handler FileIO e =>

114close : Handler FileIO e =>

45 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

115 { [FILE_IO (OpenFile m)] ==> [FILE_IO ()] } Eff e ()

46close = Close

116close = Close

47

117

118+||| Read a line from the file.

48readLine : Handler FileIO e =>

119readLine : Handler FileIO e =>

49 { [FILE_IO (OpenFile Read)] } Eff e String

120 { [FILE_IO (OpenFile Read)] } Eff e String

50readLine = ReadLine

121readLine = ReadLine

51

122

123+||| Write a line to a file.

52writeLine : Handler FileIO e =>

124writeLine : Handler FileIO e =>

53 String -> { [FILE_IO (OpenFile Write)] } Eff e ()

125 String -> { [FILE_IO (OpenFile Write)] } Eff e ()

54writeLine str = WriteLine str

126writeLine str = WriteLine str

55

127

128+||| End of file?

56eof : Handler FileIO e =>

129eof : Handler FileIO e =>

57 { [FILE_IO (OpenFile Read)] } Eff e Bool

130 { [FILE_IO (OpenFile Read)] } Eff e Bool

58eof = EOF

131eof = EOF

59

132

60−

133+-- --------------------------------------------------------------------- [ EOF ]

61−

62−

libs/prelude/Prelude/Applicative.idr+2

@@ -1,6 +1,8 @@

1module Prelude.Applicative

2

3import Builtins

4+import Prelude.Basics

5+import Prelude.Classes

4import Prelude.Functor

6import Prelude.Functor

5

7

6---- Applicative functors/Idioms

8---- Applicative functors/Idioms

libs/prelude/Prelude/Chars.idr+3

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

1module Prelude.Char

2-- Functions operating over Chars

3

4+import Prelude.Bool

5+import Prelude.Classes

6+import Prelude.List

4import Builtins

7import Builtins

5

8

6||| Return the ASCII representation of the character.

9||| Return the ASCII representation of the character.

libs/prelude/Prelude/Fin.idr+11

@@ -2,6 +2,7 @@ module Prelude.Fin

2

3import Prelude.Nat

4import Prelude.Either

5+import Prelude.Uninhabited

5

6

6%default total

7%default total

7

8

@@ -11,6 +12,10 @@ data Fin : (n : Nat) -> Type where

11 fZ : Fin (S k)

12 fZ : Fin (S k)

12 fS : Fin k -> Fin (S k)

13 fS : Fin k -> Fin (S k)

13

14

15+instance Uninhabited (Fin Z) where

16+ uninhabited fZ impossible

17+ uninhabited (fS f) impossible

18+

14fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n

19fSInjective : (m : Fin k) -> (n : Fin k) -> fS m = fS n -> m = n

15fSInjective left _ refl = refl

20fSInjective left _ refl = refl

16

21

@@ -93,6 +98,12 @@ instance MaxBound (Fin (S n)) where

93(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

98(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

94(+) (fS f) f' = fS (f + f')

99(+) (fS f) f' = fS (f + f')

95

100

101+||| Substract two Fins, keeping the bound of the minuend

102+(-) : Fin n -> Fin m -> Fin n

103+fZ - _ = fZ

104+f - fZ = f

105+(fS f) - (fS f') = weaken $ f - f'

106+

96||| Multiply two Fins, extending the bound

107||| Multiply two Fins, extending the bound

97(*) : Fin n -> Fin m -> Fin (n * m)

108(*) : Fin n -> Fin m -> Fin (n * m)

98(*) {n=Z} f f' = FinZElim f

109(*) {n=Z} f f' = FinZElim f

libs/prelude/Prelude/List.idr+8

@@ -422,6 +422,14 @@ split p xs =

422 (chunk, []) => [chunk]

423 (chunk, (c :: rest)) => chunk :: split p (assert_smaller xs rest)

424

425+||| A tuple where the first element is a List of the n first elements and

426+||| the second element is a List of the remaining elements of the list

427+||| It is equivalent to (take n xs, drop n xs)

428+||| @ n the index to split at

429+||| @ xs the list to split in two

430+splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)

431+splitAt n xs = (take n xs, drop n xs)

432+

425partition : (a -> Bool) -> List a -> (List a, List a)

433partition : (a -> Bool) -> List a -> (List a, List a)

426partition p [] = ([], [])

434partition p [] = ([], [])

427partition p (x::xs) =

435partition p (x::xs) =

libs/prelude/Prelude/Nat.idr+4

@@ -6,6 +6,7 @@ import Prelude.Algebra

6import Prelude.Bool

7import Prelude.Cast

8import Prelude.Classes

9+import Prelude.Uninhabited

9

10

10%access public

11%access public

11%default total

12%default total

@@ -20,6 +21,9 @@ import Prelude.Classes

20-- name hints for interactive editing

21-- name hints for interactive editing

21%name Nat k,j,i,n,m

22%name Nat k,j,i,n,m

22

23

24+instance Uninhabited (Z = S n) where

25+ uninhabited refl impossible

26+

23--------------------------------------------------------------------------------

27--------------------------------------------------------------------------------

24-- Syntactic tests

28-- Syntactic tests

25--------------------------------------------------------------------------------

29--------------------------------------------------------------------------------

libs/prelude/Prelude/Uninhabited.idr+2−7

@@ -1,18 +1,13 @@

1module Prelude.Uninhabited

2

3+import Builtins

4+

3||| A canonical proof that some type is empty

5||| A canonical proof that some type is empty

4class Uninhabited t where

6class Uninhabited t where

5 ||| If I have a t, I've had a contradiction

7 ||| If I have a t, I've had a contradiction

6 ||| @ t the uninhabited type

8 ||| @ t the uninhabited type

7 total uninhabited : t -> _|_

9 total uninhabited : t -> _|_

8

10

9−instance Uninhabited (Fin Z) where

10− uninhabited fZ impossible

11− uninhabited (fS f) impossible

12−

13−instance Uninhabited (Z = S n) where

14− uninhabited refl impossible

15−

16||| Use an absurd assumption to discharge a proof obligation

11||| Use an absurd assumption to discharge a proof obligation

17||| @ t some empty type

12||| @ t some empty type

18||| @ a the goal type

13||| @ a the goal type

libs/prelude/Prelude/Vect.idr+10

@@ -7,6 +7,7 @@ import Prelude.List

7import Prelude.Classes

8import Prelude.Nat

9import Prelude.Bool

10+import Prelude.Uninhabited

10

11

11%access public

12%access public

12%default total

13%default total

@@ -71,6 +72,7 @@ index fZ [] impossible

71deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

72deleteAt : Fin (S n) -> Vect (S n) a -> Vect n a

72deleteAt fZ (x::xs) = xs

73deleteAt fZ (x::xs) = xs

73deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

74deleteAt {n = S m} (fS k) (x::xs) = x :: deleteAt k xs

75+deleteAt {n = Z} (fS k) (x::xs) = absurd k

74deleteAt _ [] impossible

76deleteAt _ [] impossible

75

77

76||| Replace an element at a particlar index with another

78||| Replace an element at a particlar index with another

@@ -379,6 +381,14 @@ nub = nubBy (==)

379-- Splitting and breaking lists

381-- Splitting and breaking lists

380--------------------------------------------------------------------------------

382--------------------------------------------------------------------------------

381

383

384+||| A tuple where the first element is a Vect of the n first elements and

385+||| the second element is a Vect of the remaining elements of the original Vect

386+||| It is equivalent to (take n xs, drop n xs)

387+||| @ m the index to split at

388+||| @ xs the Vect to split in two

389+splitAt : {n : Nat} -> (m : Fin (S n)) -> (xs : Vect n a) -> (Vect (cast m) a, Vect (n - cast m) a)

390+splitAt n xs = (take n xs, drop n xs)

391+

382--------------------------------------------------------------------------------

392--------------------------------------------------------------------------------

383-- Predicates

393-- Predicates

384--------------------------------------------------------------------------------

394--------------------------------------------------------------------------------

rts/idris_rts.c+12−3

@@ -37,9 +37,18 @@ VM* init_vm(int stack_size, size_t heap_size,

37 vm->inbox_ptr = vm->inbox;

38 vm->inbox_write = vm->inbox;

39

40+ // The allocation lock must be reentrant. The lock exists to ensure that

41+ // no memory is allocated during the message sending process, but we also

42+ // check the lock in calls to allocate.

43+ // The problem comes when we use requireAlloc to guarantee a chunk of memory

44+ // first: this sets the lock, and since it is not reentrant, we get a deadlock.

45+ pthread_mutexattr_t rec_attr;

46+ pthread_mutexattr_init(&rec_attr);

47+ pthread_mutexattr_settype(&rec_attr, PTHREAD_MUTEX_RECURSIVE);

48+

40 pthread_mutex_init(&(vm->inbox_lock), NULL);

49 pthread_mutex_init(&(vm->inbox_lock), NULL);

41 pthread_mutex_init(&(vm->inbox_block), NULL);

50 pthread_mutex_init(&(vm->inbox_block), NULL);

42− pthread_mutex_init(&(vm->alloc_lock), NULL);

51+ pthread_mutex_init(&(vm->alloc_lock), &rec_attr);

43 pthread_cond_init(&(vm->inbox_waiting), NULL);

52 pthread_cond_init(&(vm->inbox_waiting), NULL);

44

53

45 vm->max_threads = max_threads;

54 vm->max_threads = max_threads;

@@ -72,14 +81,14 @@ void idris_requireAlloc(VM* vm, size_t size) {

72 }

81 }

73

82

74 int lock = vm->processes > 0;

83 int lock = vm->processes > 0;

75− if (lock) { // not message passing

84+ if (lock) { // We only need to lock if we're in concurrent mode

76 pthread_mutex_lock(&vm->alloc_lock);

85 pthread_mutex_lock(&vm->alloc_lock);

77 }

86 }

78}

87}

79

88

80void idris_doneAlloc(VM* vm) {

89void idris_doneAlloc(VM* vm) {

81 int lock = vm->processes > 0;

90 int lock = vm->processes > 0;

82− if (lock) { // not message passing

91+ if (lock) { // We only need to lock if we're in concurrent mode

83 pthread_mutex_unlock(&vm->alloc_lock);

92 pthread_mutex_unlock(&vm->alloc_lock);

84 }

93 }

85}

94}

src/IRTS/CodegenC.hs+26−10

@@ -20,16 +20,32 @@ import System.Directory

20import System.FilePath ((</>), (<.>))

21import Control.Monad

22

23+codegenC :: CodeGenerator

24+codegenC ci = codegenC' (simpleDecls ci)

25+ (outputFile ci)

26+ (outputType ci)

27+ (includes ci)

28+ (concatMap mkObj (compileObjs ci))

29+ (concatMap mkLib (compileLibs ci) ++

30+ concatMap incdir (importDirs ci))

31+ (concatMap mkFlag (compilerFlags ci))

32+ (debugLevel ci)

33+

34+ where mkObj f = f ++ " "

35+ mkLib l = "-l" ++ l ++ " "

36+ mkFlag l = l ++ " "

37+ incdir i = "-I" ++ i ++ " "

38+

23−codegenC :: [(Name, SDecl)] ->

39+codegenC' :: [(Name, SDecl)] ->

24− String -> -- output file name

40+ String -> -- output file name

25− OutputType -> -- generate executable if True, only .o if False

41+ OutputType -> -- generate executable if True, only .o if False

26− [FilePath] -> -- include files

42+ [FilePath] -> -- include files

27− String -> -- extra object files

43+ String -> -- extra object files

28− String -> -- extra compiler flags (libraries)

44+ String -> -- extra compiler flags (libraries)

29− String -> -- extra compiler flags (anything)

45+ String -> -- extra compiler flags (anything)

30− DbgLevel ->

46+ DbgLevel ->

31− IO ()

47+ IO ()

32−codegenC defs out exec incs objs libs flags dbg

48+codegenC' defs out exec incs objs libs flags dbg

33 = do -- print defs

49 = do -- print defs

34 let bc = map toBC defs

50 let bc = map toBC defs

35 let h = concatMap toDecl (map fst bc)

51 let h = concatMap toDecl (map fst bc)

src/IRTS/CodegenCommon.hs+25

@@ -2,8 +2,11 @@ module IRTS.CodegenCommon where

2

3import Idris.Core.TT

4import IRTS.Simplified

5+import IRTS.Defunctionalise

6+import IRTS.Lang

5

7

6import Control.Exception

8import Control.Exception

9+import Data.Word

7import System.Environment

10import System.Environment

8

11

9data DbgLevel = NONE | DEBUG | TRACE deriving Eq

12data DbgLevel = NONE | DEBUG | TRACE deriving Eq

@@ -13,3 +16,25 @@ environment :: String -> IO (Maybe String)

13environment x = Control.Exception.catch (do e <- getEnv x

16environment x = Control.Exception.catch (do e <- getEnv x

14 return (Just e))

17 return (Just e))

15 (\y-> do return (y::SomeException); return Nothing)

18 (\y-> do return (y::SomeException); return Nothing)

19+

20+-- Everything which might be needed in a code generator - a CG can choose which

21+-- level of Decls to generate code from (simplified, defunctionalised or merely

22+-- lambda lifted) and has access to the list of object files, libraries, etc.

23+

24+data CodegenInfo = CodegenInfo { outputFile :: String,

25+ outputType :: OutputType,

26+ targetTriple :: String,

27+ targetCPU :: String,

28+ optimisation :: Word,

29+ includes :: [FilePath],

30+ importDirs :: [FilePath],

31+ compileObjs :: [String],

32+ compileLibs :: [String],

33+ compilerFlags :: [String],

34+ debugLevel :: DbgLevel,

35+ simpleDecls :: [(Name, SDecl)],

36+ defunDecls :: [(Name, DDecl)],

37+ liftDecls :: [(Name, LDecl)]

38+ }

39+

40+type CodeGenerator = CodegenInfo -> IO ()

src/IRTS/CodegenJava.hs+13−8

@@ -34,14 +34,19 @@ import System.Process

34

35-----------------------------------------------------------------------

36-- Main function

37+codegenJava :: CodeGenerator

38+codegenJava cg = codegenJava' [] (simpleDecls cg) (outputFile cg)

39+ (includes cg) (compileLibs cg)

40+ (outputType cg)

41+

37−codegenJava :: [(Name, SExp)] -> -- initialization of globals

42+codegenJava' :: [(Name, SExp)] -> -- initialization of globals

38− [(Name, SDecl)] -> -- decls

43+ [(Name, SDecl)] -> -- decls

39− FilePath -> -- output file name

44+ FilePath -> -- output file name

40− [String] -> -- headers

45+ [String] -> -- headers

41− [String] -> -- libs

46+ [String] -> -- libs

42− OutputType ->

47+ OutputType ->

43− IO ()

48+ IO ()

44−codegenJava globalInit defs out hdrs libs exec =

49+codegenJava' globalInit defs out hdrs libs exec =

45 withTgtDir exec out (codegenJava' exec)

50 withTgtDir exec out (codegenJava' exec)

46 where

51 where

47 codegenJava' :: OutputType -> FilePath -> IO ()

52 codegenJava' :: OutputType -> FilePath -> IO ()

src/IRTS/CodegenJavaScript.hs+11−3

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

1{-# LANGUAGE PatternGuards #-}

2

3−module IRTS.CodegenJavaScript (codegenJavaScript, JSTarget(..)) where

3+module IRTS.CodegenJavaScript (codegenJavaScript, codegenNode, JSTarget(..)) where

4

5import Idris.AbsSyntax hiding (TypeCase)

6import IRTS.Bytecode

@@ -1389,14 +1389,22 @@ getGlobalCons js = foldJS match (++) [] js

1389getIncludes :: [FilePath] -> IO [String]

1390getIncludes = mapM readFile

1391

1392−codegenJavaScript

1392+codegenJavaScript :: CodeGenerator

1393+codegenJavaScript ci = codegenJS_all JavaScript (simpleDecls ci)

1394+ (includes ci) (outputFile ci) (outputType ci)

1395+

1396+codegenNode :: CodeGenerator

1397+codegenNode ci = codegenJS_all Node (simpleDecls ci)

1398+ (includes ci) (outputFile ci) (outputType ci)

1399+

1400+codegenJS_all

1393 :: JSTarget

1401 :: JSTarget

1394 -> [(Name, SDecl)]

1402 -> [(Name, SDecl)]

1395 -> [FilePath]

1403 -> [FilePath]

1396 -> FilePath

1404 -> FilePath

1397 -> OutputType

1405 -> OutputType

1398 -> IO ()

1406 -> IO ()

1399−codegenJavaScript target definitions includes filename outputType = do

1407+codegenJS_all target definitions includes filename outputType = do

1400 let (header, rt) = case target of

1408 let (header, rt) = case target of

1401 Node ->

1409 Node ->

1402 ("#!/usr/bin/env node\n", "-node")

1410 ("#!/usr/bin/env node\n", "-node")

src/IRTS/CodegenLLVM.hs+13−8

@@ -58,14 +58,19 @@ import Debug.Trace

58

59data Target = Target { triple :: String, dataLayout :: DataLayout }

60

61+codegenLLVM :: CodeGenerator

62+codegenLLVM ci = codegenLLVM' (simpleDecls ci) (targetTriple ci)

63+ (targetCPU ci) (optimisation ci)

64+ (outputFile ci) (outputType ci)

65+

61−codegenLLVM :: [(TT.Name, SDecl)] ->

66+codegenLLVM' :: [(TT.Name, SDecl)] ->

62− String -> -- target triple

67+ String -> -- target triple

63− String -> -- target CPU

68+ String -> -- target CPU

64− Word -> -- Optimization degree

69+ Word -> -- Optimization degree

65− FilePath -> -- output file name

70+ FilePath -> -- output file name

66− OutputType ->

71+ OutputType ->

67− IO ()

72+ IO ()

68−codegenLLVM defs triple cpu optimize file outty = withContext $ \context -> do

73+codegenLLVM' defs triple cpu optimize file outty = withContext $ \context -> do

69 initializeAllTargets

74 initializeAllTargets

70 (target, _) <- failInIO $ lookupTarget Nothing triple

75 (target, _) <- failInIO $ lookupTarget Nothing triple

71 withTargetOptions $ \options ->

76 withTargetOptions $ \options ->

src/IRTS/Compiler.hs+14−23

@@ -71,25 +71,22 @@ compile codegen f tm

71 case dumpDefun of

72 Nothing -> return ()

73 Just f -> runIO $ writeFile f (dumpDefuns defuns)

74− triple <- targetTriple

74+ triple <- Idris.AbsSyntax.targetTriple

75− cpu <- targetCPU

75+ cpu <- Idris.AbsSyntax.targetCPU

76− optimize <- optLevel

76+ optimise <- optLevel

77 iLOG "Building output"

78+

78 case checked of

79 case checked of

80+ OK c -> do let cginfo = CodegenInfo f outty triple cpu optimise

81+ hdrs impdirs objs libs flags

82+ NONE c (toAlist defuns)

83+ tagged

79− OK c -> runIO $ case codegen of

84+ runIO $ case codegen of

80− ViaC ->

81− codegenC c f outty hdrs

85+ ViaC -> codegenC cginfo

82− (concatMap mkObj objs)

83− (concatMap mkLib libs)

84− (concatMap mkFlag flags ++

85− concatMap incdir impdirs) NONE

86− ViaJava ->

86+ ViaJava -> codegenJava cginfo

87− codegenJava [] c f hdrs libs outty

88− ViaJavaScript ->

87+ ViaJavaScript -> codegenJavaScript cginfo

89− codegenJavaScript JavaScript c hdrs f outty

90− ViaNode ->

88+ ViaNode -> codegenNode cginfo

91− codegenJavaScript Node c hdrs f outty

92− ViaLLVM -> codegenLLVM c triple cpu optimize f outty

89+ ViaLLVM -> codegenLLVM cginfo

93 Bytecode -> dumpBC c f

90 Bytecode -> dumpBC c f

94 Error e -> ierror e

91 Error e -> ierror e

95 where checkMVs = do i <- getIState

92 where checkMVs = do i <- getIState

@@ -99,12 +96,6 @@ compile codegen f tm

99 inDir d h = do let f = d </> h

96 inDir d h = do let f = d </> h

100 ex <- doesFileExist f

97 ex <- doesFileExist f

101 if ex then return f else return h

98 if ex then return f else return h

102− mkObj f = f ++ " "

103− mkLib l = "-l" ++ l ++ " "

104− mkFlag l = l ++ " "

105−

106− incdir i = "-I" ++ i ++ " "

107−

108

99

109irMain :: TT Name -> Idris LDecl

100irMain :: TT Name -> Idris LDecl

110irMain tm = do i <- ir tm

101irMain tm = do i <- ir tm

src/Idris/AbsSyntax.hs+29−145

@@ -88,6 +88,10 @@ addDyLib libs = do i <- getIState

88addHdr :: Codegen -> String -> Idris ()

89addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }

90

91+addImported :: FilePath -> Idris ()

92+addImported f = do i <- getIState

93+ putIState $ i { idris_imported = nub $ f : idris_imported i }

94+

91addLangExt :: LanguageExt -> Idris ()

95addLangExt :: LanguageExt -> Idris ()

92addLangExt TypeProviders = do i <- getIState

96addLangExt TypeProviders = do i <- getIState

93 putIState $ i {

97 putIState $ i {

@@ -357,6 +361,9 @@ addNameIdx' i n

357getHdrs :: Codegen -> Idris [String]

361getHdrs :: Codegen -> Idris [String]

358getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

362getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)

359

363

364+getImported :: Idris [FilePath]

365+getImported = do i <- getIState; return (idris_imported i)

366+

360setErrSpan :: FC -> Idris ()

367setErrSpan :: FC -> Idris ()

361setErrSpan x = do i <- getIState;

368setErrSpan x = do i <- getIState;

362 case (errSpan i) of

369 case (errSpan i) of

@@ -490,6 +497,12 @@ getUndefined :: Idris [Name]

490getUndefined = do i <- getIState

497getUndefined = do i <- getIState

491 return (map fst (idris_metavars i) \\ primDefs)

498 return (map fst (idris_metavars i) \\ primDefs)

492

499

500+isMetavarName :: Name -> IState -> Bool

501+isMetavarName n ist

502+ = case lookupNames n (tt_ctxt ist) of

503+ (t:_) -> isJust $ lookup t (idris_metavars ist)

504+ _ -> False

505+

493getWidth :: Idris ConsoleWidth

506getWidth :: Idris ConsoleWidth

494getWidth = fmap idris_consolewidth getIState

507getWidth = fmap idris_consolewidth getIState

495

508

@@ -505,155 +518,16 @@ renderWidth = do iw <- getWidth

505 AutomaticWidth -> runIO getScreenWidth

518 AutomaticWidth -> runIO getScreenWidth

506

519

507

520

508−iRender :: Doc a -> Idris (SimpleDoc a)

509−iRender d = do w <- getWidth

510− ist <- getIState

511− let ideSlave = case idris_outputmode ist of

512− IdeSlave _ -> True

513− _ -> False

514− case w of

515− InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

516− ColsWide n -> return $

517− if n < 1

518− then renderPretty 1.0 1000000000 d

519− else renderPretty 0.8 n d

520− AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d

521− | otherwise -> do width <- runIO getScreenWidth

522− return $ renderPretty 0.8 width d

523−

524−ihPrintResult :: Handle -> String -> Idris ()

525−ihPrintResult h s = do i <- getIState

526− case idris_outputmode i of

527− RawOutput -> case s of

528− "" -> return ()

529− s -> runIO $ hPutStrLn h s

530− IdeSlave n ->

531− let good = SexpList [SymbolAtom "ok", toSExp s] in

532− runIO $ hPutStrLn h $ convSExp "return" good n

533−

534−-- | Write a pretty-printed term to the console with semantic coloring

535−consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

536−consoleDisplayAnnotated h output = do ist <- getIState

537− rendered <- iRender $ output

538− runIO . hPutStrLn h .

539− displayDecorated (consoleDecorate ist) $

540− rendered

541−

542−

543−-- | Write pretty-printed output to IDESlave with semantic annotations

544−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

545−ideSlaveReturnAnnotated n h out = do ist <- getIState

546− (str, spans) <- fmap displaySpans .

547− iRender .

548− fmap (fancifyAnnots ist) $

549− out

550− let good = [SymbolAtom "ok", toSExp str, toSExp spans]

551− runIO . hPutStrLn h $ convSExp "return" good n

552−

553−ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

554−ihPrintTermWithType h tm ty = do ist <- getIState

555− let output = tm <+> colon <+> ty

556− case idris_outputmode ist of

557− RawOutput -> consoleDisplayAnnotated h output

558− IdeSlave n -> ideSlaveReturnAnnotated n h output

559−

560−-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

561−ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

562−ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

563−ihPrintFunTypes h bnd n overloads = do imp <- impShow

564− ist <- getIState

565− let output = vsep (map (uncurry (ppOverload imp)) overloads)

566− case idris_outputmode ist of

567− RawOutput -> consoleDisplayAnnotated h output

568− IdeSlave n -> ideSlaveReturnAnnotated n h output

569− where fullName n = prettyName True bnd n

570− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)

571−

572−ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

573−ihRenderResult h d = do ist <- getIState

574− case idris_outputmode ist of

575− RawOutput -> consoleDisplayAnnotated h d

576− IdeSlave n -> ideSlaveReturnAnnotated n h d

577−

578−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

579−fancifyAnnots ist annot@(AnnName n _ _) =

580− do let ctxt = tt_ctxt ist

581− case () of

582− _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing

583− _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing

584− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing

585− _ | otherwise -> annot

586−fancifyAnnots _ annot = annot

587

521

588type1Doc :: Doc OutputAnnotation

522type1Doc :: Doc OutputAnnotation

589type1Doc = (annotate AnnConstType $ text "Type 1")

523type1Doc = (annotate AnnConstType $ text "Type 1")

590

524

591−-- | Show an error with semantic highlighting

592−ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

593−ihRenderError h e = do ist <- getIState

594− case idris_outputmode ist of

595− RawOutput -> consoleDisplayAnnotated h e

596− IdeSlave n -> do

597− (str, spans) <- fmap displaySpans .

598− iRender .

599− fmap (fancifyAnnots ist) $

600− e

601− let good = [SymbolAtom "error", toSExp str, toSExp spans]

602− runIO . hPutStrLn h $ convSExp "return" good n

603−

604−ihPrintError :: Handle -> String -> Idris ()

605−ihPrintError h s = do i <- getIState

606− case idris_outputmode i of

607− RawOutput -> case s of

608− "" -> return ()

609− s -> runIO $ hPutStrLn h s

610− IdeSlave n ->

611− let good = SexpList [SymbolAtom "error", toSExp s] in

612− runIO . hPutStrLn h $ convSExp "return" good n

613−

614−ihputStrLn :: Handle -> String -> Idris ()

615−ihputStrLn h s = do i <- getIState

616− case idris_outputmode i of

617− RawOutput -> runIO $ hPutStrLn h s

618− IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

619−

620−iputStrLn = ihputStrLn stdout

621−iPrintError = ihPrintError stdout

622−iPrintResult = ihPrintResult stdout

623−iWarn = ihWarn stdout

624−

625−ideslavePutSExp :: SExpable a => String -> a -> Idris ()

626−ideslavePutSExp cmd info = do i <- getIState

627− case idris_outputmode i of

628− IdeSlave n -> runIO . putStrLn $ convSExp cmd info n

629− _ -> return ()

630−

631−-- this needs some typing magic and more structured output towards emacs

632−iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

633−iputGoal g = do i <- getIState

634− case idris_outputmode i of

635− RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

636− IdeSlave n -> runIO . putStrLn $

637− convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

638

525

639isetPrompt :: String -> Idris ()

526isetPrompt :: String -> Idris ()

640isetPrompt p = do i <- getIState

527isetPrompt p = do i <- getIState

641 case idris_outputmode i of

528 case idris_outputmode i of

642 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

529 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n

643

530

644−ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

645−ihWarn h fc err = do i <- getIState

646− case idris_outputmode i of

647− RawOutput ->

648− do err' <- iRender . fmap (fancifyAnnots i) $

649− text (show fc) <> colon <//> err

650− runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

651− IdeSlave n ->

652− do err' <- iRender . fmap (fancifyAnnots i) $ err

653− let (str, spans) = displaySpans err'

654− runIO . hPutStrLn h $

655− convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

656−

657setLogLevel :: Int -> Idris ()

531setLogLevel :: Int -> Idris ()

658setLogLevel l = do i <- getIState

532setLogLevel l = do i <- getIState

659 let opts = idris_options i

533 let opts = idris_options i

@@ -1701,8 +1575,6 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1701 = do mf <- match' f f'

1575 = do mf <- match' f f'

1702 ms <- zipWithM matchArg args args'

1576 ms <- zipWithM matchArg args args'

1703 return (mf ++ concat ms)

1577 return (mf ++ concat ms)

1704−-- match (PRef _ n) (PRef _ n') | n == n' = return []

1705−-- | otherwise = Nothing

1706 match (PRef f n) (PApp _ x []) = match (PRef f n) x

1578 match (PRef f n) (PApp _ x []) = match (PRef f n) x

1707 match (PPatvar f n) xr = match (PRef f n) xr

1579 match (PPatvar f n) xr = match (PRef f n) xr

1708 match xr (PPatvar f n) = match xr (PRef f n)

1580 match xr (PPatvar f n) = match xr (PRef f n)

@@ -1712,7 +1584,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1712 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

1584 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))

1713 || tm == Placeholder)

1585 || tm == Placeholder)

1714 = return [(n, tm)]

1586 = return [(n, tm)]

1587+ -- if one namespace is missing, drop the other

1715− | n == n' = return []

1588+ | n == n' || n == dropNS n' || dropNS n == n' = return []

1589+ where dropNS (NS n _) = n

1590+ dropNS n = n

1716 match (PRef _ n) tm

1591 match (PRef _ n) tm

1717 | not names && (not (isConName n (tt_ctxt i) ||

1592 | not names && (not (isConName n (tt_ctxt i) ||

1718 isFnName n (tt_ctxt i)) || tm == Placeholder)

1593 isFnName n (tt_ctxt i)) || tm == Placeholder)

@@ -1855,6 +1730,12 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1855 mkUniqA arg = do t' <- mkUniq (getTm arg)

1730 mkUniqA arg = do t' <- mkUniq (getTm arg)

1856 return (arg { getTm = t' })

1731 return (arg { getTm = t' })

1857

1732

1733+ -- Initialise the unique name with the environment length (so we're not

1734+ -- looking for too long...)

1735+ initN (UN n) l = UN $ txt (str n ++ show l)

1736+ initN (MN i s) l = MN (i+l) s

1737+ initN n l = n

1738+

1858 -- FIXME: Probably ought to do this for completeness! It's fine as

1739 -- FIXME: Probably ought to do this for completeness! It's fine as

1859 -- long as there are no bindings inside tactics though.

1740 -- long as there are no bindings inside tactics though.

1860 mkUniqT tac = return tac

1741 mkUniqT tac = return tac

@@ -1864,7 +1745,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1864 = do env <- get

1745 = do env <- get

1865 (n', sc') <-

1746 (n', sc') <-

1866 if n `elem` env

1747 if n `elem` env

1867− then do let n' = uniqueName n (env ++ inScope)

1748+ then do let n' = uniqueName (initN n (length env))

1749+ (env ++ inScope)

1868 return (n', shadow n n' sc)

1750 return (n', shadow n n' sc)

1869 else return (n, sc)

1751 else return (n, sc)

1870 put (n' : env)

1752 put (n' : env)

@@ -1875,7 +1757,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1875 = do env <- get

1757 = do env <- get

1876 (n', sc') <-

1758 (n', sc') <-

1877 if n `elem` env

1759 if n `elem` env

1878− then do let n' = uniqueName n (env ++ inScope)

1760+ then do let n' = uniqueName (initN n (length env))

1761+ (env ++ inScope)

1879 return (n', shadow n n' sc)

1762 return (n', shadow n n' sc)

1880 else return (n, sc)

1763 else return (n, sc)

1881 put (n' : env)

1764 put (n' : env)

@@ -1886,7 +1769,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1886 = do env <- get

1769 = do env <- get

1887 (n', sc') <-

1770 (n', sc') <-

1888 if n `elem` env

1771 if n `elem` env

1889− then do let n' = uniqueName n (env ++ inScope)

1772+ then do let n' = uniqueName (initN n (length env))

1773+ (env ++ inScope)

1890 return (n', shadow n n' sc)

1774 return (n', shadow n n' sc)

1891 else return (n, sc)

1775 else return (n, sc)

1892 put (n' : env)

1776 put (n' : env)

src/Idris/AbsSyntaxTree.hs+29−30

@@ -104,11 +104,6 @@ data ConsoleWidth = InfinitelyWide -- ^ Have pretty-printer assume that lines sh

104 | ColsWide Int -- ^ Manually specified - must be positive

105 | AutomaticWidth -- ^ Attempt to determine width, or 80 otherwise

106

107−-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

108−-- without typechecking).

109−-- This will include all the functions and data declarations, plus fixity declarations

110−-- and syntax macros.

111−

112-- | The global state used in the Idris monad

107-- | The global state used in the Idris monad

113data IState = IState {

108data IState = IState {

114 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

109 tt_ctxt :: Context, -- ^ All the currently defined names and their terms

@@ -147,6 +142,7 @@ data IState = IState {

147 idris_libs :: [(Codegen, String)],

142 idris_libs :: [(Codegen, String)],

148 idris_cgflags :: [(Codegen, String)],

143 idris_cgflags :: [(Codegen, String)],

149 idris_hdrs :: [(Codegen, String)],

144 idris_hdrs :: [(Codegen, String)],

145+ idris_imported :: [FilePath], -- ^ Imported ibc file names

150 proof_list :: [(Name, [String])],

146 proof_list :: [(Name, [String])],

151 errSpan :: Maybe FC,

147 errSpan :: Maybe FC,

152 parserWarnings :: [(FC, Err)],

148 parserWarnings :: [(FC, Err)],

@@ -238,7 +234,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

238 emptyContext emptyContext emptyContext emptyContext

234 emptyContext emptyContext emptyContext emptyContext

239 emptyContext emptyContext

235 emptyContext emptyContext

240 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

236 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

241− [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

237+ [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

242 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

238 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

243 AutomaticWidth

239 AutomaticWidth

244

240

@@ -1083,13 +1079,13 @@ consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

1083consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1079consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)

1084consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1080consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)

1085consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1081consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1086−consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist

1082+consoleDecorate ist (AnnName n _ _ _) = let ctxt = tt_ctxt ist

1087− theme = idris_colourTheme ist

1083+ theme = idris_colourTheme ist

1088− in case () of

1084+ in case () of

1089− _ | isDConName n ctxt -> colouriseData theme

1085+ _ | isDConName n ctxt -> colouriseData theme

1090− _ | isFnName n ctxt -> colouriseFun theme

1086+ _ | isFnName n ctxt -> colouriseFun theme

1091− _ | isTConName n ctxt -> colouriseType theme

1087+ _ | isTConName n ctxt -> colouriseType theme

1092− _ | otherwise -> id -- don't colourise unknown names

1088+ _ | otherwise -> id -- don't colourise unknown names

1093consoleDecorate ist (AnnFC _) = id

1089consoleDecorate ist (AnnFC _) = id

1094consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1090consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1095 where colour BoldText = IdrisColour Nothing True False True False

1091 where colour BoldText = IdrisColour Nothing True False True False

@@ -1204,16 +1200,16 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1204

1200

1205 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1201 sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r

1206 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1202 prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1207− prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"

1203+ prettySe p bnd (PRefl _ _) = annName eqCon $ text "refl"

1208 prettySe p bnd (PResolveTC _) = text "resolvetc"

1204 prettySe p bnd (PResolveTC _) = text "resolvetc"

1209− prettySe p bnd (PTrue _ IsType) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1205+ prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1210− prettySe p bnd (PTrue _ IsTerm) = annotate (AnnName unitCon Nothing Nothing) $ text "()"

1206+ prettySe p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

1211 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1207 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1212− prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1208+ prettySe p bnd (PFalse _) = annName falseTy $ text "_|_"

1213 prettySe p bnd (PEq _ l r) =

1209 prettySe p bnd (PEq _ l r) =

1214 bracket p 2 . align . group $

1210 bracket p 2 . align . group $

1215 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1211 prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1216− where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

1212+ where eq = annName eqTy (text "=")

1217 prettySe p bnd (PRewrite _ l r _) =

1213 prettySe p bnd (PRewrite _ l r _) =

1218 bracket p 2 $

1214 bracket p 2 $

1219 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1215 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

@@ -1225,28 +1221,28 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1225 map (prettySe 10 bnd) elts

1221 map (prettySe 10 bnd) elts

1226 where ann = case pun of

1222 where ann = case pun of

1227 TypeOrTerm -> id

1223 TypeOrTerm -> id

1228− IsType -> annotate (AnnName pairTy Nothing Nothing)

1224+ IsType -> annName pairTy

1229− IsTerm -> annotate (AnnName pairCon Nothing Nothing)

1225+ IsTerm -> annName pairCon

1230 prettySe p bnd (PDPair _ TypeOrTerm l t r) =

1226 prettySe p bnd (PDPair _ TypeOrTerm l t r) =

1231 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1227 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1232 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =

1228 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =

1233− annotate (AnnName sigmaTy Nothing Nothing) lparen <>

1229+ annName sigmaTy lparen <>

1234 bindingOf n False <+>

1230 bindingOf n False <+>

1235− annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>

1231+ annName sigmaTy (text "**") <+>

1236 prettySe 10 ((n, False):bnd) r <>

1232 prettySe 10 ((n, False):bnd) r <>

1237− annotate (AnnName sigmaTy Nothing Nothing) rparen

1233+ annName sigmaTy rparen

1238 prettySe p bnd (PDPair _ IsType l t r) =

1234 prettySe p bnd (PDPair _ IsType l t r) =

1239− annotate (AnnName sigmaTy Nothing Nothing) lparen <>

1235+ annName sigmaTy lparen <>

1240 prettySe 10 bnd l <+>

1236 prettySe 10 bnd l <+>

1241− annotate (AnnName sigmaTy Nothing Nothing) (text "**") <+>

1237+ annName sigmaTy (text "**") <+>

1242 prettySe 10 bnd r <>

1238 prettySe 10 bnd r <>

1243− annotate (AnnName sigmaTy Nothing Nothing) rparen

1239+ annName sigmaTy rparen

1244 prettySe p bnd (PDPair _ IsTerm l t r) =

1240 prettySe p bnd (PDPair _ IsTerm l t r) =

1245− annotate (AnnName existsCon Nothing Nothing) lparen <>

1241+ annName existsCon lparen <>

1246 prettySe 10 bnd l <+>

1242 prettySe 10 bnd l <+>

1247− annotate (AnnName existsCon Nothing Nothing) (text "**") <+>

1243+ annName existsCon (text "**") <+>

1248 prettySe 10 bnd r <>

1244 prettySe 10 bnd r <>

1249− annotate (AnnName existsCon Nothing Nothing) rparen

1245+ annName existsCon rparen

1250 prettySe p bnd (PAlternative a as) =

1246 prettySe p bnd (PAlternative a as) =

1251 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1247 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1252 where

1248 where

@@ -1283,6 +1279,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1283 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1279 prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1284 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1280 prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1285

1281

1282+ annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1283+ annName n = annotate (AnnName n Nothing Nothing Nothing)

1284+

1286 basename :: Name -> Name

1285 basename :: Name -> Name

1287 basename (NS n _) = basename n

1286 basename (NS n _) = basename n

1288 basename n = n

1287 basename n = n

@@ -1348,7 +1347,7 @@ prettyName :: Bool -- ^^ whether to show namespaces

1348 -> Name -- ^^ the name to pprint

1347 -> Name -- ^^ the name to pprint

1349 -> Doc OutputAnnotation

1348 -> Doc OutputAnnotation

1350prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))

1349prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))

1351− | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))

1350+ | otherwise = annotate (AnnName n Nothing Nothing Nothing) (text (strName n))

1352 where strName (UN n) = T.unpack n

1351 where strName (UN n) = T.unpack n

1353 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1352 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

1354 | otherwise = strName n

1353 | otherwise = strName n

src/Idris/CaseSplit.hs+1

@@ -14,6 +14,7 @@ import Idris.ElabTerm

14import Idris.Delaborate

15import Idris.Parser

16import Idris.Error

17+import Idris.Output

17

18

18import Idris.Core.TT

19import Idris.Core.TT

19import Idris.Core.Typecheck

20import Idris.Core.Typecheck

src/Idris/Core/TT.hs+8−6

@@ -82,14 +82,16 @@ instance Show FC where

82 | otherwise = show sl ++ ":" ++ show sc ++ "-" ++ show el ++ ":" ++ show ec

83

84-- | Output annotation for pretty-printed name - decides colour

85−data NameOutput = TypeOutput | FunOutput | DataOutput

85+data NameOutput = TypeOutput | FunOutput | DataOutput | MetavarOutput

86

87-- | Text formatting output

88data TextFormatting = BoldText | ItalicText | UnderlineText

89

90-- | Output annotations for pretty-printing

91−data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

91+data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe String)

92+ -- ^^ The name, classification, docs overview, and pretty-printed type

92 | AnnBoundName Name Bool

93 | AnnBoundName Name Bool

94+ -- ^^ The name and whether it is implicit

93 | AnnConstData

95 | AnnConstData

94 | AnnConstType

96 | AnnConstType

95 | AnnKeyword

97 | AnnKeyword

@@ -312,11 +314,11 @@ instance Sized Name where

312 size _ = 1

314 size _ = 1

313

315

314instance Pretty Name OutputAnnotation where

316instance Pretty Name OutputAnnotation where

315− pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')

317+ pretty n@(UN n') = annotate (AnnName n Nothing Nothing Nothing) $ text (T.unpack n')

316− pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un

318+ pretty n@(NS un s) = annotate (AnnName n Nothing Nothing Nothing) . noAnnotate $ pretty un

317− pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $

319+ pretty n@(MN i s) = annotate (AnnName n Nothing Nothing Nothing) $

318 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

320 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

319− pretty n@(SN s) = annotate (AnnName n Nothing Nothing) $ text (show s)

321+ pretty n@(SN s) = annotate (AnnName n Nothing Nothing Nothing) $ text (show s)

320

322

321instance Pretty [Name] OutputAnnotation where

323instance Pretty [Name] OutputAnnotation where

322 pretty = encloseSep empty empty comma . map pretty

324 pretty = encloseSep empty empty comma . map pretty

src/Idris/Coverage.hs+38−11

@@ -9,6 +9,7 @@ import Idris.Core.CaseTree

9import Idris.AbsSyntax

10import Idris.Delaborate

11import Idris.Error

12+import Idris.Output (iputStrLn)

12

13

13import Data.List

14import Data.List

14import Data.Either

15import Data.Either

@@ -17,10 +18,14 @@ import Debug.Trace

17

18

18import Control.Monad.State.Strict

19import Control.Monad.State.Strict

19

20

21+-- Generate a pattern from an 'impossible' LHS. (Need this to eliminate the

22+-- pattern clauses which have been provided explicitly from new clause

23+-- generation.)

24+

20mkPatTm :: PTerm -> Idris Term

25mkPatTm :: PTerm -> Idris Term

21mkPatTm t = do i <- getIState

26mkPatTm t = do i <- getIState

22 let timp = addImpl' True [] [] i t

27 let timp = addImpl' True [] [] i t

23− evalStateT (toTT timp) 0

28+ evalStateT (toTT (mapPT deNS timp)) 0

24 where

29 where

25 toTT (PRef _ n) = do i <- lift getIState

30 toTT (PRef _ n) = do i <- lift getIState

26 case lookupDef n (tt_ctxt i) of

31 case lookupDef n (tt_ctxt i) of

@@ -29,10 +34,16 @@ mkPatTm t = do i <- getIState

29 toTT (PApp _ t args) = do t' <- toTT t

34 toTT (PApp _ t args) = do t' <- toTT t

30 args' <- mapM (toTT . getTm) args

35 args' <- mapM (toTT . getTm) args

31 return $ mkApp t' args'

36 return $ mkApp t' args'

37+ -- For alternatives, pick the first and drop the namespaces. It doesn't

38+ -- really matter which is taken since matching will ignore the namespace.

39+ toTT (PAlternative _ (a : as)) = toTT a

32 toTT _ = do v <- get

40 toTT _ = do v <- get

33 put (v + 1)

41 put (v + 1)

34 return (P Bound (sMN v "imp") Erased)

42 return (P Bound (sMN v "imp") Erased)

35

43

44+ deNS (PRef f (NS n _)) = PRef f n

45+ deNS t = t

46+

36-- Given a list of LHSs, generate a extra clauses which cover the remaining

47-- Given a list of LHSs, generate a extra clauses which cover the remaining

37-- cases. The ones which haven't been provided are marked 'absurd' so that the

48-- cases. The ones which haven't been provided are marked 'absurd' so that the

38-- checker will make sure they can't happen.

49-- checker will make sure they can't happen.

@@ -40,19 +51,24 @@ mkPatTm t = do i <- getIState

40-- This will only work after the given clauses have been typechecked and the

51-- This will only work after the given clauses have been typechecked and the

41-- names are fully explicit!

52-- names are fully explicit!

42

53

43−genClauses :: FC -> Name -> [Term] -> [PClause] -> Idris [PTerm]

54+genClauses :: FC -> Name -> [Term] -> [PTerm] -> Idris [PTerm]

44genClauses fc n xs given

55genClauses fc n xs given

45 = do i <- getIState

56 = do i <- getIState

46− let lhss = map (getLHS i) xs

57+ let lhs_tms = map (\x -> delab' i x True True) xs

58+ -- if a placeholder was given, don't bother generating cases for it

59+ let lhs_tms' = zipWith mergePlaceholders lhs_tms given

60+ let lhss = map pUnApply lhs_tms'

61+

47 let argss = transpose lhss

62 let argss = transpose lhss

48 let all_args = map (genAll i) argss

63 let all_args = map (genAll i) argss

49 logLvl 5 $ "COVERAGE of " ++ show n

64 logLvl 5 $ "COVERAGE of " ++ show n

65+ logLvl 5 $ show lhss

50 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

66 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

51 logLvl 10 $ show argss ++ "\n" ++ show all_args

67 logLvl 10 $ show argss ++ "\n" ++ show all_args

52− logLvl 10 $ "Original: \n" ++

68+ logLvl 1 $ "Original: \n" ++

53 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)

69 showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)

54 -- add an infinite supply of explicit arguments to update the possible

70 -- add an infinite supply of explicit arguments to update the possible

55− -- cases for (the return type may be variadic, or function type, sp

71+ -- cases for (the return type may be variadic, or function type, so

56 -- there may be more case splitting that the idris_implicits record

72 -- there may be more case splitting that the idris_implicits record

57 -- suggests)

73 -- suggests)

58 let parg = case lookupCtxt n (idris_implicits i) of

74 let parg = case lookupCtxt n (idris_implicits i) of

@@ -61,10 +77,10 @@ genClauses fc n xs given

61 _ -> repeat (pexp Placeholder)

77 _ -> repeat (pexp Placeholder)

62 let tryclauses = mkClauses parg all_args

78 let tryclauses = mkClauses parg all_args

63 logLvl 2 $ show (length tryclauses) ++ " initially to check"

79 logLvl 2 $ show (length tryclauses) ++ " initially to check"

64− logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)

80+ logLvl 1 $ showSep "\n" (map (showTm i) tryclauses)

65 let new = filter (noMatch i) (nub tryclauses)

81 let new = filter (noMatch i) (nub tryclauses)

66 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

82 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

67− logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

83+ logLvl 3 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)

68-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

84-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

69 return new

85 return new

70-- return (map (\t -> PClause n t [] PImpossible []) new)

86-- return (map (\t -> PClause n t [] PImpossible []) new)

@@ -72,13 +88,23 @@ genClauses fc n xs given

72 | (f, args) <- unApply term = map (\t -> delab' i t True True) args

88 | (f, args) <- unApply term = map (\t -> delab' i t True True) args

73 | otherwise = []

89 | otherwise = []

74

90

75− lhsApp (PClause _ _ l _ _ _) = l

91+ pUnApply (PApp _ _ args) = map getTm args

76− lhsApp (PWith _ _ l _ _ _) = l

92+ pUnApply _ = []

77

93

94+ -- Return whether the given clause matches none of the input clauses

95+ -- (xs)

78 noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of

96 noMatch i tm = all (\x -> case matchClause i (delab' i x True True) tm of

79− Right _ -> False

97+ Right ms -> False

80− Left miss -> True) xs

98+ Left miss -> True) xs

99+

81

100

101+ mergePlaceholders :: PTerm -> PTerm -> PTerm

102+ mergePlaceholders x Placeholder = Placeholder

103+ mergePlaceholders (PApp fc f args) (PApp fc' f' args')

104+ = PApp fc' f' (zipWith mergePArg args args')

105+ where mergePArg x y = let xtm = mergePlaceholders (getTm x) (getTm y) in

106+ x { getTm = xtm}

107+ mergePlaceholders x _ = x

82

108

83 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]

109 mkClauses :: [PArg] -> [[PTerm]] -> [PTerm]

84 mkClauses parg args

110 mkClauses parg args

@@ -102,6 +128,7 @@ fnub' acc [] = acc

102

128

103-- quick check for constructor equality

129-- quick check for constructor equality

104quickEq :: PTerm -> PTerm -> Bool

130quickEq :: PTerm -> PTerm -> Bool

131+quickEq (PConstant n) (PConstant n') = n == n'

105quickEq (PRef _ n) (PRef _ n') = n == n'

132quickEq (PRef _ n) (PRef _ n') = n == n'

106quickEq (PApp _ t as) (PApp _ t' as')

133quickEq (PApp _ t as) (PApp _ t' as')

107 | length as == length as'

134 | length as == length as'

src/Idris/Delaborate.hs+2−7

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

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pshow, pprintErr) where

2+module Idris.Delaborate (bugaddr, delab, delab', delabMV, delabTy, delabTy', pprintErr) where

3

4-- Convert core TT back into high level syntax, primarily for display

5-- purposes.

@@ -140,11 +140,6 @@ pprintTerm ist = pprintTerm' ist []

140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

141pprintTerm' ist bnd tm = pprintPTerm (opt_showimp (idris_options ist)) bnd [] tm

142

143−pshow :: IState -> Err -> String

144−pshow ist err = displayDecorated (consoleDecorate ist) .

145− renderPretty 1.0 80 .

146− fmap (fancifyAnnots ist) $ pprintErr ist err

147−

148pprintErr :: IState -> Err -> Doc OutputAnnotation

143pprintErr :: IState -> Err -> Doc OutputAnnotation

149pprintErr i err = pprintErr' i (fmap (errReverse i) err)

144pprintErr i err = pprintErr' i (fmap (errReverse i) err)

150

145

@@ -261,7 +256,7 @@ annName :: Name -> Doc OutputAnnotation

261annName n = annName' n (showbasic n)

256annName n = annName' n (showbasic n)

262

257

263annName' :: Name -> String -> Doc OutputAnnotation

258annName' :: Name -> String -> Doc OutputAnnotation

264−annName' n str = annotate (AnnName n Nothing Nothing) (text str)

259+annName' n str = annotate (AnnName n Nothing Nothing Nothing) (text str)

265

260

266showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

261showSc :: IState -> [(Name, Term)] -> Doc OutputAnnotation

267showSc i [] = empty

262showSc i [] = empty

src/Idris/ElabDecls.hs+14−7

@@ -16,6 +16,7 @@ import Idris.Primitives

16import Idris.Inliner

17import Idris.PartialEval

18import Idris.DeepSeq

19+import Idris.Output (iputStrLn, pshow, iWarn)

19import IRTS.Lang

20import IRTS.Lang

20import Paths_idris

21import Paths_idris

21

22

@@ -58,7 +59,8 @@ checkAddDef add toplvl fc [] = return []

58checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

59checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

59 = do ctxt <- getContext

60 = do ctxt <- getContext

60 (t', _) <- recheckC fc [] t

61 (t', _) <- recheckC fc [] t

61− when add $ addDeferred [(n, (i, top, t, toplvl))]

62+ when add $ do addDeferred [(n, (i, top, t, toplvl))]

63+ addIBC (IBCDef n)

62 ns' <- checkAddDef add toplvl fc ns

64 ns' <- checkAddDef add toplvl fc ns

63 return ((n, (i, top, t')) : ns')

65 return ((n, (i, top, t')) : ns')

64-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

66-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

@@ -925,8 +927,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

925 tclift $ tfail $ At fc (NoTypeDecl n)

927 tclift $ tfail $ At fc (NoTypeDecl n)

926 [ty] -> return ty

928 [ty] -> return ty

927 let atys = map snd (getArgTys fty)

929 let atys = map snd (getArgTys fty)

928− pats_in <- mapM (elabClause info opts)

930+ cs_elab <- mapM (elabClause info opts)

929 (zip [0..] cs)

931 (zip [0..] cs)

932+ let (pats_in, cs_full) = unzip cs_elab

933+

930 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

934 logLvl 3 $ "Elaborated patterns:\n" ++ show pats_in

931

935

932 -- if the return type of 'ty' is collapsible, the optimised version should

936 -- if the return type of 'ty' is collapsible, the optimised version should

@@ -1011,7 +1015,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

1011 cov <- coverage

1015 cov <- coverage

1012 pmissing <-

1016 pmissing <-

1013 if cov && not (hasDefault cs)

1017 if cov && not (hasDefault cs)

1014− then do missing <- genClauses fc n (map getLHS pdef) cs

1018+ then do missing <- genClauses fc n (map getLHS pdef) cs_full

1015 -- missing <- genMissing n scargs sc

1019 -- missing <- genMissing n scargs sc

1016 missing' <- filterM (checkPossible info fc True n) missing

1020 missing' <- filterM (checkPossible info fc True n) missing

1017 let clhs = map getLHS pdef

1021 let clhs = map getLHS pdef

@@ -1369,16 +1373,19 @@ propagateParams ps t (PRef fc n)

1369 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1373 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1370propagateParams ps t x = x

1374propagateParams ps t x = x

1371

1375

1376+-- Return the elaborated LHS/RHS, and the original LHS with implicits added

1372elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1377elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

1373− Idris (Either Term (Term, Term))

1378+ Idris (Either Term (Term, Term), PTerm)

1374elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

1379elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

1375 = do let tcgen = Dictionary `elem` opts

1380 = do let tcgen = Dictionary `elem` opts

1381+ i <- get

1382+ let lhs = addImpl i lhs_in

1376 b <- checkPossible info fc tcgen fname lhs_in

1383 b <- checkPossible info fc tcgen fname lhs_in

1377 case b of

1384 case b of

1378 True -> tclift $ tfail (At fc

1385 True -> tclift $ tfail (At fc

1379 (Msg $ show lhs_in ++ " is a valid case"))

1386 (Msg $ show lhs_in ++ " is a valid case"))

1380 False -> do ptm <- mkPatTm lhs_in

1387 False -> do ptm <- mkPatTm lhs_in

1381− return (Left ptm)

1388+ return (Left ptm, lhs)

1382elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1389elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1383 = do let tcgen = Dictionary `elem` opts

1390 = do let tcgen = Dictionary `elem` opts

1384 ctxt <- getContext

1391 ctxt <- getContext

@@ -1519,7 +1526,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1519 when (rev || ErrorReverse `elem` opts) $ do

1526 when (rev || ErrorReverse `elem` opts) $ do

1520 addIBC (IBCErrRev (crhs, clhs))

1527 addIBC (IBCErrRev (crhs, clhs))

1521 addErrRev (crhs, clhs)

1528 addErrRev (crhs, clhs)

1522− return $ Right (clhs, crhs)

1529+ return $ (Right (clhs, crhs), lhs)

1523 where

1530 where

1524 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

1531 pinfo :: ElabInfo -> [(Name, PTerm)] -> [Name] -> Int -> ElabInfo

1525 pinfo info ns ds i

1532 pinfo info ns ds i

@@ -1686,7 +1693,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1686 mapM_ (elabCaseBlock info opts) is

1693 mapM_ (elabCaseBlock info opts) is

1687 logLvl 5 ("Checked RHS " ++ show rhs')

1694 logLvl 5 ("Checked RHS " ++ show rhs')

1688 (crhs, crhsty) <- recheckC fc [] rhs'

1695 (crhs, crhsty) <- recheckC fc [] rhs'

1689− return $ Right (clhs, crhs)

1696+ return $ (Right (clhs, crhs), lhs)

1690 where

1697 where

1691 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

1698 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

1692 getImps _ = []

1699 getImps _ = []

src/Idris/ElabTerm.hs+1

@@ -8,6 +8,7 @@ import Idris.DSL

8import Idris.Delaborate

9import Idris.Error

10import Idris.ProofSearch

11+import Idris.Output (pshow)

11

12

12import Idris.Core.Elaborate hiding (Tactic(..))

13import Idris.Core.Elaborate hiding (Tactic(..))

13import Idris.Core.TT

14import Idris.Core.TT

src/Idris/Error.hs+1

@@ -5,6 +5,7 @@ module Idris.Error where

5import Prelude hiding (catch)

6import Idris.AbsSyntax

7import Idris.Delaborate

8+import Idris.Output

8

9

9import Idris.Core.TT

10import Idris.Core.TT

10import Idris.Core.Typecheck

11import Idris.Core.Typecheck

src/Idris/IBC.hs+12−5

@@ -10,6 +10,7 @@ import Idris.Imports

10import Idris.Error

11import Idris.Delaborate

12import Idris.Docstrings

13+import Idris.Output

13

14

14import qualified Cheapskate.Types as CT

15import qualified Cheapskate.Types as CT

15

16

@@ -75,9 +76,12 @@ initIBC :: IBCFile

75initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

76initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

76

77

77loadIBC :: FilePath -> Idris ()

78loadIBC :: FilePath -> Idris ()

79+loadIBC fp = do imps <- getImported

80+ when (not (fp `elem` imps)) $

78−loadIBC fp = do iLOG $ "Loading ibc " ++ fp

81+ do iLOG $ "Loading ibc " ++ fp

79− ibcf <- runIO $ (bdecode fp :: IO IBCFile)

82+ ibcf <- runIO $ (bdecode fp :: IO IBCFile)

80− process ibcf fp

83+ process ibcf fp

84+ addImported fp

81

85

82bencode :: Binary a => FilePath -> a -> IO ()

86bencode :: Binary a => FilePath -> a -> IO ()

83bencode f d = B.writeFile f (compress (encode d))

87bencode f d = B.writeFile f (compress (encode d))

@@ -396,8 +400,11 @@ pPatdefs ds

396pDefs :: [Name] -> [(Name, Def)] -> Idris ()

400pDefs :: [Name] -> [(Name, Def)] -> Idris ()

397pDefs syms ds

401pDefs syms ds

398 = mapM_ (\ (n, d) ->

402 = mapM_ (\ (n, d) ->

399− do i <- getIState

400− let d' = updateDef d

403+ do let d' = updateDef d

404+ case d' of

405+ TyDecl _ _ -> return ()

406+ _ -> solveDeferred n

407+ i <- getIState

401 logLvl 5 $ "Added " ++ show (n, d')

408 logLvl 5 $ "Added " ++ show (n, d')

402 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

409 putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })) ds

403 where

410 where

src/Idris/IdeSlave.hs+13−8

@@ -74,16 +74,21 @@ instance (SExpable a, SExpable b, SExpable c, SExpable d, SExpable e) =>

74 toSExp (l, m, n, o, p) = SexpList [toSExp l, toSExp m, toSExp n, toSExp o, toSExp p]

75

76instance SExpable NameOutput where

77− toSExp TypeOutput = SymbolAtom "type"

77+ toSExp TypeOutput = SymbolAtom "type"

78− toSExp FunOutput = SymbolAtom "function"

78+ toSExp FunOutput = SymbolAtom "function"

79− toSExp DataOutput = SymbolAtom "data"

79+ toSExp DataOutput = SymbolAtom "data"

80+ toSExp MetavarOutput = SymbolAtom "metavar"

81+

82+maybeProps :: SExpable a => [(String, Maybe a)] -> [(SExp, SExp)]

83+maybeProps [] = []

84+maybeProps ((n, Just p):ps) = (SymbolAtom n, toSExp p) : maybeProps ps

85+maybeProps ((n, Nothing):ps) = maybeProps ps

80

86

81instance SExpable OutputAnnotation where

87instance SExpable OutputAnnotation where

82− toSExp (AnnName n Nothing _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

88+ toSExp (AnnName n ty d t) = toSExp $ [(SymbolAtom "name", StringAtom (show n)),

83− (SymbolAtom "implicit", BoolAtom False)]

89+ (SymbolAtom "implicit", BoolAtom False)] ++

84− toSExp (AnnName n (Just ty) _) = toSExp [(SymbolAtom "name", StringAtom (show n)),

90+ maybeProps [("decor", ty)] ++

85− (SymbolAtom "decor", toSExp ty),

91+ maybeProps [("doc-overview", d), ("type", t)]

86− (SymbolAtom "implicit", BoolAtom False)]

87 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

92 toSExp (AnnBoundName n imp) = toSExp [(SymbolAtom "name", StringAtom (show n)),

88 (SymbolAtom "decor", SymbolAtom "bound"),

93 (SymbolAtom "decor", SymbolAtom "bound"),

89 (SymbolAtom "implicit", BoolAtom imp)]

94 (SymbolAtom "implicit", BoolAtom imp)]

src/Idris/Output.hsnew file+173

@@ -0,0 +1,173 @@

1+module Idris.Output where

2+

3+import Idris.Core.TT

4+import Idris.Core.Evaluate (isDConName, isTConName, isFnName)

5+

6+import Idris.AbsSyntax

7+import Idris.Delaborate

8+import Idris.Docstrings

9+import Idris.IdeSlave

10+

11+import Util.Pretty

12+import Util.ScreenSize (getScreenWidth)

13+

14+import System.IO (stdout, Handle, hPutStrLn)

15+

16+pshow :: IState -> Err -> String

17+pshow ist err = displayDecorated (consoleDecorate ist) .

18+ renderPretty 1.0 80 .

19+ fmap (fancifyAnnots ist) $ pprintErr ist err

20+

21+ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()

22+ihWarn h fc err = do i <- getIState

23+ case idris_outputmode i of

24+ RawOutput ->

25+ do err' <- iRender . fmap (fancifyAnnots i) $

26+ text (show fc) <> colon <//> err

27+ runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'

28+ IdeSlave n ->

29+ do err' <- iRender . fmap (fancifyAnnots i) $ err

30+ let (str, spans) = displaySpans err'

31+ runIO . hPutStrLn h $

32+ convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n

33+

34+iRender :: Doc a -> Idris (SimpleDoc a)

35+iRender d = do w <- getWidth

36+ ist <- getIState

37+ let ideSlave = case idris_outputmode ist of

38+ IdeSlave _ -> True

39+ _ -> False

40+ case w of

41+ InfinitelyWide -> return $ renderPretty 1.0 1000000000 d

42+ ColsWide n -> return $

43+ if n < 1

44+ then renderPretty 1.0 1000000000 d

45+ else renderPretty 0.8 n d

46+ AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d

47+ | otherwise -> do width <- runIO getScreenWidth

48+ return $ renderPretty 0.8 width d

49+

50+ihPrintResult :: Handle -> String -> Idris ()

51+ihPrintResult h s = do i <- getIState

52+ case idris_outputmode i of

53+ RawOutput -> case s of

54+ "" -> return ()

55+ s -> runIO $ hPutStrLn h s

56+ IdeSlave n ->

57+ let good = SexpList [SymbolAtom "ok", toSExp s] in

58+ runIO $ hPutStrLn h $ convSExp "return" good n

59+

60+-- | Write a pretty-printed term to the console with semantic coloring

61+consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()

62+consoleDisplayAnnotated h output = do ist <- getIState

63+ rendered <- iRender $ output

64+ runIO . hPutStrLn h .

65+ displayDecorated (consoleDecorate ist) $

66+ rendered

67+

68+

69+-- | Write pretty-printed output to IDESlave with semantic annotations

70+ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()

71+ideSlaveReturnAnnotated n h out = do ist <- getIState

72+ (str, spans) <- fmap displaySpans .

73+ iRender .

74+ fmap (fancifyAnnots ist) $

75+ out

76+ let good = [SymbolAtom "ok", toSExp str, toSExp spans]

77+ runIO . hPutStrLn h $ convSExp "return" good n

78+

79+ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

80+ihPrintTermWithType h tm ty = do ist <- getIState

81+ let output = tm <+> colon <+> ty

82+ case idris_outputmode ist of

83+ RawOutput -> consoleDisplayAnnotated h output

84+ IdeSlave n -> ideSlaveReturnAnnotated n h output

85+

86+-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

87+ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

88+ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

89+ihPrintFunTypes h bnd n overloads = do imp <- impShow

90+ ist <- getIState

91+ let output = vsep (map (uncurry (ppOverload imp)) overloads)

92+ case idris_outputmode ist of

93+ RawOutput -> consoleDisplayAnnotated h output

94+ IdeSlave n -> ideSlaveReturnAnnotated n h output

95+ where fullName n = prettyName True bnd n

96+ ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)

97+

98+ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

99+ihRenderResult h d = do ist <- getIState

100+ case idris_outputmode ist of

101+ RawOutput -> consoleDisplayAnnotated h d

102+ IdeSlave n -> ideSlaveReturnAnnotated n h d

103+

104+fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation

105+fancifyAnnots ist annot@(AnnName n _ _ _) =

106+ do let ctxt = tt_ctxt ist

107+ docs = docOverview ist n

108+ ty = Just (getTy ist n)

109+ case () of

110+ _ | isDConName n ctxt -> AnnName n (Just DataOutput) docs ty

111+ _ | isFnName n ctxt -> AnnName n (Just FunOutput) docs ty

112+ _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

113+ _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

114+ _ | otherwise -> annot

115+ where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

116+ docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

117+ let o = overview (fst docs)

118+ -- TODO make width configurable

119+ out = displayS . renderPretty 1.0 50 $ renderDocstring o

120+ return (out "")

121+ getTy :: IState -> Name -> String -- fails if name not already extant!

122+ getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] $

123+ delabTy ist n

124+ in (displayS . renderPretty 1.0 50 $ theTy) ""

125+fancifyAnnots _ annot = annot

126+

127+-- | Show an error with semantic highlighting

128+ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()

129+ihRenderError h e = do ist <- getIState

130+ case idris_outputmode ist of

131+ RawOutput -> consoleDisplayAnnotated h e

132+ IdeSlave n -> do

133+ (str, spans) <- fmap displaySpans .

134+ iRender .

135+ fmap (fancifyAnnots ist) $

136+ e

137+ let good = [SymbolAtom "error", toSExp str, toSExp spans]

138+ runIO . hPutStrLn h $ convSExp "return" good n

139+

140+ihPrintError :: Handle -> String -> Idris ()

141+ihPrintError h s = do i <- getIState

142+ case idris_outputmode i of

143+ RawOutput -> case s of

144+ "" -> return ()

145+ s -> runIO $ hPutStrLn h s

146+ IdeSlave n ->

147+ let good = SexpList [SymbolAtom "error", toSExp s] in

148+ runIO . hPutStrLn h $ convSExp "return" good n

149+

150+ihputStrLn :: Handle -> String -> Idris ()

151+ihputStrLn h s = do i <- getIState

152+ case idris_outputmode i of

153+ RawOutput -> runIO $ hPutStrLn h s

154+ IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n

155+

156+iputStrLn = ihputStrLn stdout

157+iPrintError = ihPrintError stdout

158+iPrintResult = ihPrintResult stdout

159+iWarn = ihWarn stdout

160+

161+ideslavePutSExp :: SExpable a => String -> a -> Idris ()

162+ideslavePutSExp cmd info = do i <- getIState

163+ case idris_outputmode i of

164+ IdeSlave n -> runIO . putStrLn $ convSExp cmd info n

165+ _ -> return ()

166+

167+-- this needs some typing magic and more structured output towards emacs

168+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

169+iputGoal g = do i <- getIState

170+ case idris_outputmode i of

171+ RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

172+ IdeSlave n -> runIO . putStrLn $

173+ convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n

src/Idris/ParseHelpers.hs+1

@@ -17,6 +17,7 @@ import Idris.Core.TT

17import Idris.Core.Evaluate

18import Idris.Delaborate (pprintErr)

19import Idris.Docstrings

20+import Idris.Output (ihWarn)

20

21

21import qualified Util.Pretty as Pretty (text)

22import qualified Util.Pretty as Pretty (text)

22

23

src/Idris/ParseOps.hs+6−1

@@ -37,9 +37,14 @@ table fixes

37 [pexp (PApp fc (PRef fc (sUN "fromInteger")) [pexp (PConstant (BI 0))]), pexp x])]]

38 ++ toTable (reverse fixes) ++

39 [[backtick],

40− [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

40+ [binary "$" (\fc x y -> flatten $ PApp fc x [pexp y]) AssocRight],

41 [binary "=" PEq AssocLeft],

42 [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

43+ where

44+ flatten :: PTerm -> PTerm -- flatten application

45+ flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

46+ flatten t = t

47+

43

48

44-- | Calculates table for fixtiy declarations

49-- | Calculates table for fixtiy declarations

45toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

50toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm

src/Idris/Parser.hs+9

@@ -29,6 +29,7 @@ import Idris.Coverage

29import Idris.IBC

30import Idris.Unlit

31import Idris.Providers

32+import Idris.Output

32

33

33import Idris.ParseHelpers

34import Idris.ParseHelpers

34import Idris.ParseOps

35import Idris.ParseOps

@@ -1212,6 +1213,14 @@ loadSource h lidr f

1212 file_in <- runIO $ readFile f

1213 file_in <- runIO $ readFile f

1213 file <- if lidr then tclift $ unlit f file_in else return file_in

1214 file <- if lidr then tclift $ unlit f file_in else return file_in

1214 (mname, imports, pos) <- parseImports f file

1215 (mname, imports, pos) <- parseImports f file

1216+ ids <- allImportDirs

1217+ ibcsd <- valIBCSubDir i

1218+ mapM_ (\f -> do fp <- runIO $ findImport ids ibcsd f

1219+ case fp of

1220+ LIDR fn -> ifail $ "No ibc for " ++ f

1221+ IDR fn -> ifail $ "No ibc for " ++ f

1222+ IBC fn src -> loadIBC fn)

1223+ [fn | (fn, _, _) <- imports]

1215 reportParserWarnings

1224 reportParserWarnings

1216

1225

1217 -- process and check module aliases

1226 -- process and check module aliases

src/Idris/Prover.hs+1

@@ -15,6 +15,7 @@ import Idris.Error

15import Idris.DataOpts

16import Idris.Completion

17import Idris.IdeSlave

18+import Idris.Output

18

19

19import Text.Trifecta.Result(Result(..))

20import Text.Trifecta.Result(Result(..))

20

21

src/Idris/REPL.hs+55−24

@@ -27,6 +27,7 @@ import Idris.Colours hiding (colourise)

27import Idris.Inliner

28import Idris.CaseSplit

29import Idris.DeepSeq

30+import Idris.Output

30

31

31import Paths_idris

32import Paths_idris

32import Version_idris (gitHash)

33import Version_idris (gitHash)

@@ -319,8 +320,6 @@ ideslaveProcess fn (HNF t) = process stdout fn (HNF t)

319--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!

320--ideslaveProcess fn TTShell = process stdout fn TTShell -- need some prove mode!

320ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)

321ideslaveProcess fn (TestInline t) = process stdout fn (TestInline t)

321

322

322−--that most likely does not work, since we need to wrap

323−--input/output of the executed binary...

324ideslaveProcess fn Execute = do process stdout fn Execute

323ideslaveProcess fn Execute = do process stdout fn Execute

325 iPrintResult ""

324 iPrintResult ""

326ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)

325ideslaveProcess fn (Compile codegen f) = do process stdout fn (Compile codegen f)

@@ -532,7 +531,7 @@ process h fn (Check (PRef _ n))

532 putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

531 putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

533 putGoal imp ist bnd g

532 putGoal imp ist bnd g

534 = text "--------------------------------------" <$>

533 = text "--------------------------------------" <$>

535− annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>

534+ annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

536 align (tPretty bnd ist g)

535 align (tPretty bnd ist g)

537

536

538 tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t

537 tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t

@@ -891,17 +890,19 @@ process h fn (TestInline t)

891 c <- colourise

890 c <- colourise

892 iPrintResult (showTm ist (delab ist tm'))

891 iPrintResult (showTm ist (delab ist tm'))

893process h fn Execute

892process h fn Execute

893+ = do ist <- getIState

894− = do (m, _) <- elabVal toplevel False

894+ (m, _) <- elabVal toplevel False

895 (PApp fc

896 (PRef fc (sUN "run__IO"))

897 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

898−-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

899 (tmpn, tmph) <- runIO tempfile

898 (tmpn, tmph) <- runIO tempfile

900 runIO $ hClose tmph

899 runIO $ hClose tmph

901 t <- codegen

900 t <- codegen

902 compile t tmpn m

901 compile t tmpn m

902+ case idris_outputmode ist of

903− runIO $ system tmpn

903+ RawOutput -> do runIO $ system tmpn

904− return ()

904+ return ()

905+ IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n

905 where fc = fileFC "main"

906 where fc = fileFC "main"

906process h fn (Compile codegen f)

907process h fn (Compile codegen f)

907 = do (m, _) <- elabVal toplevel False

908 = do (m, _) <- elabVal toplevel False

@@ -1146,30 +1147,32 @@ loadInputs h inputs

1146 let ninputs = zip [1..] inputs

1147 let ninputs = zip [1..] inputs

1147 ifiles <- mapWhileOK (\(num, input) ->

1148 ifiles <- mapWhileOK (\(num, input) ->

1148 do putIState ist

1149 do putIState ist

1149− v <- verbose

1150− -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++

1151− -- show (length inputs) ++

1152− -- ") " ++ input

1153 modTree <- buildTree

1150 modTree <- buildTree

1154 (map snd (take (num-1) ninputs))

1151 (map snd (take (num-1) ninputs))

1155 input

1152 input

1156 let ifiles = getModuleFiles modTree

1153 let ifiles = getModuleFiles modTree

1157 iLOG ("MODULE TREE : " ++ show modTree)

1154 iLOG ("MODULE TREE : " ++ show modTree)

1158 iLOG ("RELOAD: " ++ show ifiles)

1155 iLOG ("RELOAD: " ++ show ifiles)

1159− when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles

1156+ when (not (all ibc ifiles) || loadCode) $

1157+ tryLoad False (filter (not . ibc) ifiles)

1160 -- return the files that need rechecking

1158 -- return the files that need rechecking

1161− return (if (all ibc ifiles) then ifiles else []))

1159+ return ifiles)

1162 ninputs

1160 ninputs

1163 inew <- getIState

1161 inew <- getIState

1164− -- to check everything worked consistently (in particular, will catch

1162+ let tidata = idris_tyinfodata inew

1165− -- if the ibc version is out of date) if we weren't loading per

1163+ let lineapps = idris_lineapps inew

1166− -- module

1164+ let patdefs = idris_patdefs inew

1165+ -- If it worked, load the whole thing from all the ibcs together

1167 case errSpan inew of

1166 case errSpan inew of

1168 Nothing ->

1167 Nothing ->

1169− do putIState ist

1168+ do putIState (ist { idris_tyinfodata = tidata })

1170− when (not loadCode) $ tryLoad $ nub (concat ifiles)

1169+ ibcfiles <- mapM findNewIBC (nub (concat ifiles))

1170+ tryLoad True (mapMaybe id ibcfiles)

1171 _ -> return ()

1172− putIState inew)

1172+ ist <- getIState

1173+ putIState (ist { idris_tyinfodata = tidata,

1174+ idris_lineapps = lineapps,

1175+ idris_patdefs = patdefs }))

1173 (\e -> do i <- getIState

1176 (\e -> do i <- getIState

1174 case e of

1177 case e of

1175 At f _ -> do setErrSpan f

1178 At f _ -> do setErrSpan f

@@ -1178,15 +1181,43 @@ loadInputs h inputs

1178 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1181 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1179 iputStrLn (pshow i e))

1182 iputStrLn (pshow i e))

1180 where -- load all files, stop if any fail

1183 where -- load all files, stop if any fail

1181− tryLoad :: [IFileType] -> Idris ()

1184+ tryLoad :: Bool -> [IFileType] -> Idris ()

1182− tryLoad [] = return ()

1185+ tryLoad keepstate [] = return ()

1186+ tryLoad keepstate (f : fs)

1187+ = do ist <- getIState

1183− tryLoad (f : fs) = do loadFromIFile h f

1188+ loadFromIFile h f

1189+ inew <- getIState

1190+ -- FIXME: Save these in IBC to avoid this hack! Need to

1191+ -- preserve it all from source inputs

1192+ let tidata = idris_tyinfodata inew

1193+ let lineapps = idris_lineapps inew

1194+ let patdefs = idris_patdefs inew

1184− ok <- noErrors

1195+ ok <- noErrors

1196+ when ok $ do when (not keepstate) $ putIState ist

1197+ ist <- getIState

1198+ putIState (ist { idris_tyinfodata = tidata,

1199+ idris_lineapps = lineapps,

1200+ idris_patdefs = patdefs })

1185− when ok $ tryLoad fs

1201+ tryLoad keepstate fs

1186

1202

1187 ibc (IBC _ _) = True

1203 ibc (IBC _ _) = True

1188 ibc _ = False

1204 ibc _ = False

1189

1205

1206+ findNewIBC :: IFileType -> Idris (Maybe IFileType)

1207+ findNewIBC i@(IBC _ _) = return (Just i)

1208+ findNewIBC s@(IDR f) = do ist <- get

1209+ ibcsd <- valIBCSubDir ist

1210+ let ibc = ibcPathNoFallback ibcsd f

1211+ ok <- runIO $ doesFileExist ibc

1212+ if ok then return (Just (IBC ibc s))

1213+ else return Nothing

1214+ findNewIBC s@(LIDR f) = do ist <- get

1215+ ibcsd <- valIBCSubDir ist

1216+ let ibc = ibcPathNoFallback ibcsd f

1217+ ok <- runIO $ doesFileExist ibc

1218+ if ok then return (Just (IBC ibc s))

1219+ else return Nothing

1220+

1190 -- Like mapM, but give up when there's an error

1221 -- Like mapM, but give up when there's an error

1191 mapWhileOK f [] = return []

1222 mapWhileOK f [] = return []

1192 mapWhileOK f (x : xs) = do x' <- f x

1223 mapWhileOK f (x : xs) = do x' <- f x

src/Pkg/Package.hs+1

@@ -17,6 +17,7 @@ import Data.List.Split(splitOn)

17import Idris.Core.TT

18import Idris.REPL

19import Idris.AbsSyntax

20+import Idris.Output

20

21

21import IRTS.System

22import IRTS.System

22

23

src/Util/LLVMStubs.hs+2−9

@@ -20,12 +20,5 @@ getHostCPUName :: IO String

20getHostCPUName = return ""

21

22

23−codegenLLVM :: [(TT.Name, SDecl)] ->

23+codegenLLVM :: CodeGenerator

24− String -> -- target triple

25− String -> -- target CPU

26− Word -> -- Optimization degree

27− FilePath -> -- output file name

28− OutputType ->

29− IO ()

30−

31−codegenLLVM _ _ _ _ _ _ = fail "This Idris was compiled without the LLVM backend."

24+codegenLLVM _ = fail "This Idris was compiled without the LLVM backend."

test/error004/FunErrTest.idr+1−1

@@ -6,7 +6,6 @@ import Language.Reflection.Utils

6

7%language ErrorReflection

8

9−

10total

9total

11cadr : (xs : List a)

10cadr : (xs : List a)

12 -> {auto cons1 : isCons xs = True}

11 -> {auto cons1 : isCons xs = True}

@@ -14,6 +13,7 @@ cadr : (xs : List a)

14 -> a

13 -> a

15cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

14cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

16cadr (x :: []) {cons1=refl} {cons2=refl} impossible

15cadr (x :: []) {cons1=refl} {cons2=refl} impossible

16+cadr [] {cons1=refl} {cons2=refl} impossible

17

18extractList : TT -> Maybe TT

19extractList (App (App reflCon (App isCons lst)) _) = Just lst