20e0bf4 · Idris-dev · git.iko.soy

idris.cabal+1

compare with master

unifiedsplit

@@ -477,6 +477,7 @@ Library

477 , Idris.IdrisDoc

478 , Idris.Imports

479 , Idris.Inliner

480+ , Idris.Output

480 , Idris.Parser

481 , Idris.Parser

481 , Idris.ParseHelpers

482 , Idris.ParseHelpers

482 , Idris.ParseOps

483 , 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/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+5

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

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+2

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

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+17−142

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

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

1666 = do mf <- match' f f'

1540 = do mf <- match' f f'

1667 ms <- zipWithM matchArg args args'

1541 ms <- zipWithM matchArg args args'

1668 return (mf ++ concat ms)

1542 return (mf ++ concat ms)

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

1670−-- | otherwise = Nothing

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

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

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

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

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

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

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

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

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

1678 || tm == Placeholder)

1550 || tm == Placeholder)

1679 = return [(n, tm)]

1551 = return [(n, tm)]

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

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

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

1554+ where dropNS (NS n _) = n

1555+ dropNS n = n

1681 match (PRef _ n) tm

1556 match (PRef _ n) tm

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

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

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

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

src/Idris/AbsSyntaxTree.hs+29−30

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

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

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

93

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

95−-- without typechecking).

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

97−-- and syntax macros.

98−

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

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

100data IState = IState {

95data IState = IState {

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

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

@@ -134,6 +129,7 @@ data IState = IState {

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

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

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

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

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

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

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

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

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

138 errSpan :: Maybe FC,

134 errSpan :: Maybe FC,

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

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

@@ -225,7 +221,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

225 emptyContext emptyContext emptyContext emptyContext

221 emptyContext emptyContext emptyContext emptyContext

226 emptyContext emptyContext

222 emptyContext emptyContext

227 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

223 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

228− [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

224+ [] [] Nothing [] Nothing [] [] Nothing [] Hidden False [] Nothing [] [] RawOutput

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

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

230 AutomaticWidth

226 AutomaticWidth

231

227

@@ -1070,13 +1066,13 @@ consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist

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

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

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

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

1072consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

1068consoleDecorate ist AnnKeyword = colouriseKeyword (idris_colourTheme ist)

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

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

1074− theme = idris_colourTheme ist

1070+ theme = idris_colourTheme ist

1075− in case () of

1071+ in case () of

1076− _ | isDConName n ctxt -> colouriseData theme

1072+ _ | isDConName n ctxt -> colouriseData theme

1077− _ | isFnName n ctxt -> colouriseFun theme

1073+ _ | isFnName n ctxt -> colouriseFun theme

1078− _ | isTConName n ctxt -> colouriseType theme

1074+ _ | isTConName n ctxt -> colouriseType theme

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

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

1080consoleDecorate ist (AnnFC _) = id

1076consoleDecorate ist (AnnFC _) = id

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

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

1082 where colour BoldText = IdrisColour Nothing True False True False

1078 where colour BoldText = IdrisColour Nothing True False True False

@@ -1191,16 +1187,16 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1191

1187

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1200 prettySe p bnd (PEq _ l r) =

1196 prettySe p bnd (PEq _ l r) =

1201 bracket p 2 . align . group $

1197 bracket p 2 . align . group $

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

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

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

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

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

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

1205 bracket p 2 $

1201 bracket p 2 $

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

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

@@ -1212,28 +1208,28 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1212 map (prettySe 10 bnd) elts

1208 map (prettySe 10 bnd) elts

1213 where ann = case pun of

1209 where ann = case pun of

1214 TypeOrTerm -> id

1210 TypeOrTerm -> id

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

1211+ IsType -> annName pairTy

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

1212+ IsTerm -> annName pairCon

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

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

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

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

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

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

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

1216+ annName sigmaTy lparen <>

1221 bindingOf n False <+>

1217 bindingOf n False <+>

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

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

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

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

1224− annotate (AnnName sigmaTy Nothing Nothing) rparen

1220+ annName sigmaTy rparen

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

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

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

1222+ annName sigmaTy lparen <>

1227 prettySe 10 bnd l <+>

1223 prettySe 10 bnd l <+>

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

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

1229 prettySe 10 bnd r <>

1225 prettySe 10 bnd r <>

1230− annotate (AnnName sigmaTy Nothing Nothing) rparen

1226+ annName sigmaTy rparen

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

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

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

1228+ annName existsCon lparen <>

1233 prettySe 10 bnd l <+>

1229 prettySe 10 bnd l <+>

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

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

1235 prettySe 10 bnd r <>

1231 prettySe 10 bnd r <>

1236− annotate (AnnName existsCon Nothing Nothing) rparen

1232+ annName existsCon rparen

1237 prettySe p bnd (PAlternative a as) =

1233 prettySe p bnd (PAlternative a as) =

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

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

1239 where

1235 where

@@ -1270,6 +1266,9 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

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

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

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

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

1272

1268

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

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

1271+

1273 basename :: Name -> Name

1272 basename :: Name -> Name

1274 basename (NS n _) = basename n

1273 basename (NS n _) = basename n

1275 basename n = n

1274 basename n = n

@@ -1335,7 +1334,7 @@ prettyName :: Bool -- ^^ whether to show namespaces

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

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

1336 -> Doc OutputAnnotation

1335 -> Doc OutputAnnotation

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

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

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

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

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

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

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

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

1341 | otherwise = strName n

1340 | 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+20−7

@@ -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.

@@ -49,10 +60,10 @@ genClauses fc n xs given

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

57 -- suggests)

68 -- suggests)

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

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

@@ -60,10 +71,10 @@ genClauses fc n xs given

60 _ -> repeat (pexp Placeholder)

71 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

72 let tryclauses = mkClauses parg all_args

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

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

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

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

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

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

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

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

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

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

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

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

68 return new

79 return new

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

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

@@ -74,9 +85,11 @@ genClauses fc n xs given

74 lhsApp (PClause _ _ l _ _ _) = l

85 lhsApp (PClause _ _ l _ _ _) = l

75 lhsApp (PWith _ _ l _ _ _) = l

86 lhsApp (PWith _ _ l _ _ _) = l

76

87

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

89+ -- (xs)

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

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

78− Right _ -> False

91+ Right ms -> False

79− Left miss -> True) xs

92+ Left miss -> True) xs

80

93

81

94

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

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

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+3−1

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

src/Idris/ElabTerm.hs+1

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

7import Idris.Delaborate

8import Idris.Error

9import Idris.ProofSearch

10+import Idris.Output (pshow)

10

11

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

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

12import Idris.Core.TT

13import 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+7−3

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

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

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

28import Idris.Inliner

29import Idris.CaseSplit

30import Idris.DeepSeq

31+import Idris.Output

31

32

32import Paths_idris

33import Paths_idris

33import Version_idris (gitHash)

34import Version_idris (gitHash)

@@ -321,8 +322,6 @@ ideslaveProcess fn (HNF t) = process stdout fn (HNF t)

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

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

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

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

323

324

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

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

326ideslaveProcess fn Execute = do process stdout fn Execute

325ideslaveProcess fn Execute = do process stdout fn Execute

327 iPrintResult ""

326 iPrintResult ""

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

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

@@ -534,7 +533,7 @@ process h fn (Check (PRef _ n))

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

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

535 putGoal imp ist bnd g

534 putGoal imp ist bnd g

536 = text "--------------------------------------" <$>

535 = text "--------------------------------------" <$>

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

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

538 align (tPretty bnd ist g)

537 align (tPretty bnd ist g)

539

538

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

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

@@ -893,17 +892,19 @@ process h fn (TestInline t)

893 c <- colourise

892 c <- colourise

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

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

895process h fn Execute

894process h fn Execute

895+ = do ist <- getIState

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

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

897 (PApp fc

898 (PRef fc (sUN "run__IO"))

899 [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

900−-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

901 (tmpn, tmph) <- runIO tempfile

900 (tmpn, tmph) <- runIO tempfile

902 runIO $ hClose tmph

901 runIO $ hClose tmph

903 t <- codegen

902 t <- codegen

904 compile t tmpn m

903 compile t tmpn m

904+ case idris_outputmode ist of

905− runIO $ system tmpn

905+ RawOutput -> do runIO $ system tmpn

906− return ()

906+ return ()

907+ IdeSlave n -> do runIO . hPutStrLn h $ IdeSlave.convSExp "run-program" tmpn n

907 where fc = fileFC "main"

908 where fc = fileFC "main"

908process h fn (Compile codegen f)

909process h fn (Compile codegen f)

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

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

@@ -1163,30 +1164,32 @@ loadInputs h inputs

1163 let ninputs = zip [1..] inputs

1164 let ninputs = zip [1..] inputs

1164 ifiles <- mapWhileOK (\(num, input) ->

1165 ifiles <- mapWhileOK (\(num, input) ->

1165 do putIState ist

1166 do putIState ist

1166− v <- verbose

1167− -- when v $ iputStrLn $ "(" ++ show num ++ "/" ++

1168− -- show (length inputs) ++

1169− -- ") " ++ input

1170 modTree <- buildTree

1167 modTree <- buildTree

1171 (map snd (take (num-1) ninputs))

1168 (map snd (take (num-1) ninputs))

1172 input

1169 input

1173 let ifiles = getModuleFiles modTree

1170 let ifiles = getModuleFiles modTree

1174 iLOG ("MODULE TREE : " ++ show modTree)

1171 iLOG ("MODULE TREE : " ++ show modTree)

1175 iLOG ("RELOAD: " ++ show ifiles)

1172 iLOG ("RELOAD: " ++ show ifiles)

1176− when (not (all ibc ifiles) || loadCode) $ tryLoad ifiles

1173+ when (not (all ibc ifiles) || loadCode) $

1174+ tryLoad False (filter (not . ibc) ifiles)

1177 -- return the files that need rechecking

1175 -- return the files that need rechecking

1178− return (if (all ibc ifiles) then ifiles else []))

1176+ return ifiles)

1179 ninputs

1177 ninputs

1180 inew <- getIState

1178 inew <- getIState

1181− -- to check everything worked consistently (in particular, will catch

1179+ let tidata = idris_tyinfodata inew

1182− -- if the ibc version is out of date) if we weren't loading per

1180+ let lineapps = idris_lineapps inew

1183− -- module

1181+ let patdefs = idris_patdefs inew

1182+ -- If it worked, load the whole thing from all the ibcs together

1184 case errSpan inew of

1183 case errSpan inew of

1185 Nothing ->

1184 Nothing ->

1186− do putIState ist

1185+ do putIState (ist { idris_tyinfodata = tidata })

1187− when (not loadCode) $ tryLoad $ nub (concat ifiles)

1186+ ibcfiles <- mapM findNewIBC (nub (concat ifiles))

1187+ tryLoad True (mapMaybe id ibcfiles)

1188 _ -> return ()

1189− putIState inew)

1189+ ist <- getIState

1190+ putIState (ist { idris_tyinfodata = tidata,

1191+ idris_lineapps = lineapps,

1192+ idris_patdefs = patdefs }))

1190 (\e -> do i <- getIState

1193 (\e -> do i <- getIState

1191 case e of

1194 case e of

1192 At f _ -> do setErrSpan f

1195 At f _ -> do setErrSpan f

@@ -1195,15 +1198,43 @@ loadInputs h inputs

1195 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1198 _ -> do setErrSpan emptyFC -- FIXME! Propagate it

1196 iputStrLn (pshow i e))

1199 iputStrLn (pshow i e))

1197 where -- load all files, stop if any fail

1200 where -- load all files, stop if any fail

1198− tryLoad :: [IFileType] -> Idris ()

1201+ tryLoad :: Bool -> [IFileType] -> Idris ()

1199− tryLoad [] = return ()

1202+ tryLoad keepstate [] = return ()

1203+ tryLoad keepstate (f : fs)

1204+ = do ist <- getIState

1200− tryLoad (f : fs) = do loadFromIFile h f

1205+ loadFromIFile h f

1206+ inew <- getIState

1207+ -- FIXME: Save these in IBC to avoid this hack! Need to

1208+ -- preserve it all from source inputs

1209+ let tidata = idris_tyinfodata inew

1210+ let lineapps = idris_lineapps inew

1211+ let patdefs = idris_patdefs inew

1201− ok <- noErrors

1212+ ok <- noErrors

1213+ when ok $ do when (not keepstate) $ putIState ist

1214+ ist <- getIState

1215+ putIState (ist { idris_tyinfodata = tidata,

1216+ idris_lineapps = lineapps,

1217+ idris_patdefs = patdefs })

1202− when ok $ tryLoad fs

1218+ tryLoad keepstate fs

1203

1219

1204 ibc (IBC _ _) = True

1220 ibc (IBC _ _) = True

1205 ibc _ = False

1221 ibc _ = False

1206

1222

1223+ findNewIBC :: IFileType -> Idris (Maybe IFileType)

1224+ findNewIBC i@(IBC _ _) = return (Just i)

1225+ findNewIBC s@(IDR f) = do ist <- get

1226+ ibcsd <- valIBCSubDir ist

1227+ let ibc = ibcPathNoFallback ibcsd f

1228+ ok <- runIO $ doesFileExist ibc

1229+ if ok then return (Just (IBC ibc s))

1230+ else return Nothing

1231+ findNewIBC s@(LIDR f) = do ist <- get

1232+ ibcsd <- valIBCSubDir ist

1233+ let ibc = ibcPathNoFallback ibcsd f

1234+ ok <- runIO $ doesFileExist ibc

1235+ if ok then return (Just (IBC ibc s))

1236+ else return Nothing

1237+

1207 -- Like mapM, but give up when there's an error

1238 -- Like mapM, but give up when there's an error

1208 mapWhileOK f [] = return []

1239 mapWhileOK f [] = return []

1209 mapWhileOK f (x : xs) = do x' <- f x

1240 mapWhileOK f (x : xs) = do x' <- f x

src/Pkg/Package.hs+1

@@ -23,6 +23,7 @@ import Idris.Parser (loadModule)

23import Idris.Delaborate (pshow)

24import Idris.AbsSyntax

25import Idris.IdrisDoc

26+import Idris.Output

26

27

27import IRTS.System

28import IRTS.System

28

29

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