b0e1ecf · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -28,6 +28,8 @@ New in 0.9.15:

28 documentation lookups, and with semantic highlighting for IDEs.

29* Fenced code blocks in docs defined with the "example" attribute are rendered

30 as code examples.

31+* Fenced code blocks declared to be Idris code that fail to parse or type check now

32+ provide error messages to IDE clients.

31* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

33* EXPERIMENTAL support for partial evaluation (Scrapping your Inefficient

32 Engine style)

34 Engine style)

33

35

idris.cabal+1−1

@@ -692,7 +692,7 @@ Library

692 , ansi-terminal < 0.7

693 , ansi-wl-pprint < 0.7

694 , base64-bytestring < 1.1

695− , binary < 0.8

695+ , binary >= 0.7 && < 0.8

696 , blaze-html >= 0.6.1.3 && < 0.8

697 , blaze-markup >= 0.5.2.1 && < 0.7.0.0

698 , bytestring < 0.11

libs/prelude/Prelude/List.idr+71−35

@@ -341,13 +341,15 @@ reverse = reverse' []

341

342||| Insert some separator between the elements of a list.

343|||

344−||| > intersperse ',' (unpack "abcde") == unpack "a,b,c,d,e"

344+||| ````idris example

345+||| with List (intersperse ',' ['a', 'b', 'c', 'd', 'e'])

346+||| ````

345|||

347|||

346intersperse : a -> List a -> List a

348intersperse : a -> List a -> List a

347intersperse sep [] = []

349intersperse sep [] = []

348intersperse sep (x::xs) = x :: intersperse' sep xs

350intersperse sep (x::xs) = x :: intersperse' sep xs

349 where

351 where

350−-- intersperse' : a -> List a -> List a

352+ intersperse' : a -> List a -> List a

351 intersperse' sep [] = []

353 intersperse' sep [] = []

352 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys

354 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys

353

355

@@ -356,13 +358,15 @@ intercalate sep l = concat $ intersperse sep l

356

358

357||| Transposes rows and columns of a list of lists.

359||| Transposes rows and columns of a list of lists.

358|||

360|||

361+||| ```idris example

359−||| > transpose [[1, 2], [3, 4]] = [[1, 3], [2, 4]]

362+||| with List transpose [[1, 2], [3, 4]]

363+||| ```

360|||

364|||

361||| This also works for non square scenarios, thus

365||| This also works for non square scenarios, thus

362||| involution does not always hold:

366||| involution does not always hold:

363|||

367|||

364−||| > transpose [[], [1, 2]] = [[1], [2]]

368+||| transpose [[], [1, 2]] = [[1], [2]]

365−||| > transpose (transpose [[], [1, 2]]) = [[1, 2]]

369+||| transpose (transpose [[], [1, 2]]) = [[1, 2]]

366|||

370|||

367||| TODO: Solution which satisfies the totality checker?

371||| TODO: Solution which satisfies the totality checker?

368%assert_total

372%assert_total

@@ -473,7 +477,9 @@ elemIndices = elemIndicesBy (==)

473

477

474||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,

478||| filter, applied to a predicate and a list, returns the list of those elements that satisfy the predicate; e.g.,

475|||

479|||

480+||| ````idris example

476−||| > filter (<3) [0..5] == [0,1,2]

481+||| filter (< 3) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))]

482+||| ````

477|||

483|||

478filter : (a -> Bool) -> List a -> List a

484filter : (a -> Bool) -> List a -> List a

479filter p [] = []

485filter p [] = []

@@ -495,10 +501,14 @@ nubBy = nubBy' []

495 else

501 else

496 x :: nubBy' (x::acc) p xs

502 x :: nubBy' (x::acc) p xs

497

503

504+||| O(n^2). The nub function removes duplicate elements from a list. In

498−||| O(n^2). The nub function removes duplicate elements from a list. In particular, it keeps only the first occurrence of each element. It is a special case of nubBy, which allows the programmer to supply their own equality test.

505+||| particular, it keeps only the first occurrence of each element. It is a

499−|||

506+||| special case of nubBy, which allows the programmer to supply their own

500−||| > nub (the (List _) [1,2,1,3]) == [1,2,3]

507+||| equality test.

501|||

508|||

509+||| ```idris example

510+||| nub (the (List _) [1,2,1,3])

511+||| ```

502nub : Eq a => List a -> List a

512nub : Eq a => List a -> List a

503nub = nubBy (==)

513nub = nubBy (==)

504

514

@@ -507,18 +517,25 @@ deleteBy : (a -> a -> Bool) -> a -> List a -> List a

507deleteBy _ _ [] = []

517deleteBy _ _ [] = []

508deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys

518deleteBy eq x (y::ys) = if x `eq` y then ys else y :: deleteBy eq x ys

509

519

510−||| delete x removes the first occurrence of x from its list argument. For example,

520+||| `delete x` removes the first occurrence of `x` from its list argument. For

521+||| example,

511|||

522|||

512−||| > delete 'a' (unpack "banana") == unpack "bnana"

523+|||````idris example

524+|||delete 'a' ['b', 'a', 'n', 'a', 'n', 'a']

525+|||````

513|||

526|||

514−||| It is a special case of deleteBy, which allows the programmer to supply their own equality test.

527+||| It is a special case of deleteBy, which allows the programmer to supply

528+||| their own equality test.

515delete : (Eq a) => a -> List a -> List a

529delete : (Eq a) => a -> List a -> List a

516delete = deleteBy (==)

530delete = deleteBy (==)

517

531

518−||| The \\ function is list difference (non-associative). In the result of xs \\ ys, the first occurrence of each element of ys in turn (if any) has been removed from xs, e.g.,

532+||| The `\\` function is list difference (non-associative). In the result of

519−|||

533+||| `xs \\ ys`, the first occurrence of each element of ys in turn (if any) has

520−||| > (([1,2] ++ [2,3]) \\ [1,2]) == [2,3]

534+||| been removed from `xs`, e.g.,

521|||

535|||

536+||| ```idris example

537+||| (([1,2] ++ [2,3]) \\ [1,2])

538+||| ```

522(\\) : (Eq a) => List a -> List a -> List a

539(\\) : (Eq a) => List a -> List a -> List a

523(\\) = foldl (flip delete)

540(\\) = foldl (flip delete)

524

541

@@ -527,7 +544,9 @@ unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

527

544

528||| The union function returns the list union of the two lists. For example,

545||| The union function returns the list union of the two lists. For example,

529|||

546|||

530−||| > union (unpack "dog") (unpack "cow") == unpack "dogcw"

547+||| ```idris example

548+||| union ['d', 'o', 'g'] ['c', 'o', 'w']

549+||| ```

531|||

550|||

532union : (Eq a) => List a -> List a -> List a

551union : (Eq a) => List a -> List a -> List a

533union = unionBy (==)

552union = unionBy (==)

@@ -539,8 +558,9 @@ union = unionBy (==)

539||| Given a list and a predicate, returns a pair consisting of the longest

558||| Given a list and a predicate, returns a pair consisting of the longest

540||| prefix of the list that satisfies a predicate and the rest of the list.

559||| prefix of the list that satisfies a predicate and the rest of the list.

541|||

560|||

561+||| ```idris example

542−||| > span (<3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])

562+||| span (<3) [1,2,3,2,1]

543−|||

563+||| ```

544span : (a -> Bool) -> List a -> (List a, List a)

564span : (a -> Bool) -> List a -> (List a, List a)

545span p [] = ([], [])

565span p [] = ([], [])

546span p (x::xs) =

566span p (x::xs) =

@@ -551,17 +571,20 @@ span p (x::xs) =

551 ([], x::xs)

571 ([], x::xs)

552

572

553||| Given a list and a predicate, returns a pair consisting of the longest

573||| Given a list and a predicate, returns a pair consisting of the longest

554−||| prefix of the list that does not satisfy a predicate and the rest of the list.

574+||| prefix of the list that does not satisfy a predicate and the rest of the

555−|||

575+||| list.

556−||| > break (>=3) [1,2,3,2,1] == the ((List _, List _)) ([1, 2], [3, 2, 1])

557|||

576|||

577+||| ```idris example

578+||| break (>=3) [1,2,3,2,1]

579+||| ```

558break : (a -> Bool) -> List a -> (List a, List a)

580break : (a -> Bool) -> List a -> (List a, List a)

559break p = span (not . p)

581break p = span (not . p)

560

582

561||| Split on any elements that satisfy the given predicate.

583||| Split on any elements that satisfy the given predicate.

562|||

584|||

585+||| ```idris example

563−||| > split (<2) [2,0,3,1,4] == [[2], [3], [4]]

586+||| split (<2) [2,0,3,1,4]

564−|||

587+||| ```

565split : (a -> Bool) -> List a -> List (List a)

588split : (a -> Bool) -> List a -> List (List a)

566split p xs =

589split p xs =

567 case break p xs of

590 case break p xs of

@@ -578,8 +601,9 @@ splitAt n xs = (take n xs, drop n xs)

578

601

579||| The partition function takes a predicate a list and returns the pair of lists of elements which do and do not satisfy the predicate, respectively; e.g.,

602||| The partition function takes a predicate a list and returns the pair of lists of elements which do and do not satisfy the predicate, respectively; e.g.,

580|||

603|||

604+||| ```idris example

581−||| > partition (<3) [0..5] == (the (List Integer) [0,1,2], the (List Integer) [3,4,5])

605+||| partition (<3) [0, 1, 2, 3, 4, 5]

582−|||

606+||| ```

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

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

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

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

585partition p (x::xs) =

609partition p (x::xs) =

@@ -589,19 +613,23 @@ partition p (x::xs) =

589 else

613 else

590 (lefts, x::rights)

614 (lefts, x::rights)

591

615

592−||| The inits function returns all initial segments of the argument, shortest first. For example,

616+||| The inits function returns all initial segments of the argument, shortest

593−|||

617+||| first. For example,

594−||| > inits [1,2,3] == [[],[1],[1,2],[1,2,3]]

595|||

618|||

619+||| ```idris example

620+||| inits [1,2,3]

621+||| ```

596inits : List a -> List (List a)

622inits : List a -> List (List a)

597inits xs = [] :: case xs of

623inits xs = [] :: case xs of

598 [] => []

624 [] => []

599 x :: xs' => map (x ::) (inits xs')

625 x :: xs' => map (x ::) (inits xs')

600

626

601−||| The tails function returns all final segments of the argument, longest first. For example,

627+||| The tails function returns all final segments of the argument, longest

602−|||

628+||| first. For example,

603−||| > tails [1,2,3] == [[1,2,3], [2,3], [3], []]

604|||

629|||

630+||| ```idris example

631+||| tails [1,2,3] == [[1,2,3], [2,3], [3], []]

632+|||```

605tails : List a -> List (List a)

633tails : List a -> List (List a)

606tails xs = xs :: case xs of

634tails xs = xs :: case xs of

607 [] => []

635 [] => []

@@ -609,14 +637,18 @@ tails xs = xs :: case xs of

609

637

610||| Split on the given element.

638||| Split on the given element.

611|||

639|||

640+||| ```idris example

612−||| > splitOn 0 [1,0,2,0,0,3] == [[1],[2],[],[3]]

641+||| splitOn 0 [1,0,2,0,0,3]

642+||| ```

613|||

643|||

614splitOn : Eq a => a -> List a -> List (List a)

644splitOn : Eq a => a -> List a -> List (List a)

615splitOn a = split (== a)

645splitOn a = split (== a)

616

646

617||| Replaces all occurences of the first argument with the second argument in a list.

647||| Replaces all occurences of the first argument with the second argument in a list.

618|||

648|||

649+||| ```idris example

619−||| > replaceOn '-' ',' (unpack "1-2-3") == unpack "1,2,3"

650+||| replaceOn '-' ',' ['1', '-', '2', '-', '3']

651+||| ```

620|||

652|||

621replaceOn : Eq a => a -> a -> List a -> List a

653replaceOn : Eq a => a -> a -> List a -> List a

622replaceOn a b l = map (\c => if c == a then b else c) l

654replaceOn a b l = map (\c => if c == a then b else c) l

@@ -647,8 +679,12 @@ isSuffixOf = isSuffixOfBy (==)

647

679

648||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.

680||| The isInfixOf function takes two lists and returns True iff the first list is contained, wholly and intact, anywhere within the second.

649|||

681|||

650−||| > isInfixOf "Idris" "I really like Idris." == True

682+||| ```idris example

651−||| > isInfixOf "Ial" "I really like Idris." == False

683+||| isInfixOf ['b','c'] ['a', 'b', 'c', 'd']

684+||| ```

685+||| ```idris example

686+||| isInfixOf ['b','d'] ['a', 'b', 'c', 'd']

687+||| ```

652|||

688|||

653isInfixOf : Eq a => List a -> List a -> Bool

689isInfixOf : Eq a => List a -> List a -> Bool

654isInfixOf n h = any (isPrefixOf n) (tails h)

690isInfixOf n h = any (isPrefixOf n) (tails h)

src/Idris/AbsSyntax.hs+1−1

@@ -286,7 +286,7 @@ addCoercion :: Name -> Idris ()

286addCoercion n = do i <- getIState

287 putIState $ i { idris_coercions = nub $ n : idris_coercions i }

288

289−addDocStr :: Name -> Docstring (Maybe Term) -> [(Name, Docstring (Maybe Term))] -> Idris ()

289+addDocStr :: Name -> Docstring DocTerm -> [(Name, Docstring DocTerm)] -> Idris ()

290addDocStr n doc args

291 = do i <- getIState

292 putIState $ i { idris_docstrings = addDef n (doc, args) (idris_docstrings i) }

src/Idris/AbsSyntaxTree.hs+16−15

@@ -158,7 +158,7 @@ data IState = IState {

158 idris_flags :: Ctxt [FnOpt],

159 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

160 idris_calledgraph :: Ctxt [Name],

161− idris_docstrings :: Ctxt (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]),

161+ idris_docstrings :: Ctxt (Docstring DocTerm, [(Name, Docstring DocTerm)]),

162 idris_tyinfodata :: Ctxt TIData,

163 idris_fninfo :: Ctxt FnInfo,

164 idris_transforms :: Ctxt [(Term, Term)],

@@ -536,19 +536,19 @@ type ProvideWhat = ProvideWhat' PTerm

536-- datatypes and typeclasses.

537data PDecl' t

538 = PFix FC Fixity [String] -- ^ Fixity declaration

539− | PTy (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

539+ | PTy (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC FnOpts Name t -- ^ Type declaration

540− | PPostulate (Docstring (Maybe PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

540+ | PPostulate (Docstring (Either Err PTerm)) SyntaxInfo FC FnOpts Name t -- ^ Postulate

541 | PClauses FC FnOpts Name [PClause' t] -- ^ Pattern clause

542 | PCAF FC Name t -- ^ Top level constant

543− | PData (Docstring (Maybe PTerm)) [(Name, Docstring (Maybe PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

543+ | PData (Docstring (Either Err PTerm)) [(Name, Docstring (Either Err PTerm))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

544 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

545 | PNamespace String [PDecl' t] -- ^ New namespace

546− | PRecord (Docstring (Maybe PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Maybe PTerm)) Name t -- ^ Record declaration

546+ | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC Name t DataOpts (Docstring (Either Err PTerm)) Name t -- ^ Record declaration

547− | PClass (Docstring (Maybe PTerm)) SyntaxInfo FC

547+ | PClass (Docstring (Either Err PTerm)) SyntaxInfo FC

548 [t] -- constraints

549 Name

550 [(Name, t)] -- parameters

551− [(Name, Docstring (Maybe PTerm))] -- parameter docstrings

551+ [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

552 [PDecl' t] -- declarations

553 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

554 -- class name, parameters, method declarations

@@ -599,7 +599,7 @@ deriving instance NFData PClause'

599-- | Data declaration

600data PData' t = PDatadecl { d_name :: Name, -- ^ The name of the datatype

601 d_tcon :: t, -- ^ Type constructor

602− d_cons :: [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, t, FC, [Name])] -- ^ Constructors

602+ d_cons :: [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, t, FC, [Name])] -- ^ Constructors

603 }

604 -- ^ Data declaration

605 | PLaterdecl { d_name :: Name, d_tcon :: t }

@@ -1079,7 +1079,7 @@ unitTy = sUN "Unit"

1079unitCon = sUN "MkUnit"

1080

1081-- TODO: elaborate the code samples in the docstring

1082−falseDoc = fmap (const Nothing) . parseDocstring . T.pack $

1082+falseDoc = fmap (const $ Msg "") . parseDocstring . T.pack $

1083 "The empty type, also known as the trivially false proposition." ++

1084 "\n\n" ++

1085 "Use `void` or `absurd` to prove anything if you have a variable " ++

@@ -1091,7 +1091,7 @@ pairCon = sUN "MkPair"

1091

1092eqTy = sUN "="

1093eqCon = sUN "Refl"

1094−eqDoc = fmap (const Nothing) . parseDocstring . T.pack $

1094+eqDoc = fmap (const (Left $ Msg "")) . parseDocstring . T.pack $

1095 "The propositional equality type. A proof that `x` = `y`." ++

1096 "\n\n" ++

1097 "To use such a proof, pattern-match on it, and the two equal things will " ++

@@ -1114,14 +1114,14 @@ eqDecl = PDatadecl eqTy (piBindp impl [(n "A", PType), (n "B", PType)]

1114 pexp (PRef bi (n "x")),

1115 pexp (PRef bi (n "x"))])), bi, [])]

1116 where n a = sUN a

1117− reflDoc = annotCode (const Nothing) . parseDocstring . T.pack $

1117+ reflDoc = annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $

1118 "A proof that `x` in fact equals `x`. To construct this, you must have already " ++

1119 "shown that both sides are in fact equal."

1120− reflParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type at which the equality is proven"),

1120+ reflParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type at which the equality is proven"),

1121− (n "x", annotCode (const Nothing) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]

1121+ (n "x", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the element shown to be equal to itself.")]

1122

1123−eqParamDoc = [(n "A", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the left side of the equality"),

1123+eqParamDoc = [(n "A", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the left side of the equality"),

1124− (n "B", annotCode (const Nothing) . parseDocstring . T.pack $ "the type of the right side of the equality")

1124+ (n "B", annotCode (const (Left $ Msg "")) . parseDocstring . T.pack $ "the type of the right side of the equality")

1125 ]

1126 where n a = sUN a

1127

@@ -1188,6 +1188,7 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1188 colour ItalicText = IdrisColour Nothing True False False True

1189consoleDecorate ist (AnnTerm _ _) = id

1190consoleDecorate ist (AnnSearchResult _) = id

1191+consoleDecorate ist (AnnErr _) = id

1191

1192

1192isPostulateName :: Name -> IState -> Bool

1193isPostulateName :: Name -> IState -> Bool

1193isPostulateName n ist = S.member n (idris_postulates ist)

1194isPostulateName n ist = S.member n (idris_postulates ist)

src/Idris/Core/Binary.hs+171−1

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

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

2+

1{-| Binary instances for the core datatypes -}

3{-| Binary instances for the core datatypes -}

2module Idris.Core.Binary where

4module Idris.Core.Binary where

3

5

@@ -7,6 +9,169 @@ import qualified Data.Text as T

7

9

8import Idris.Core.TT

10import Idris.Core.TT

9

11

12+instance Binary ErrorReportPart where

13+ put (TextPart msg) = do putWord8 0 ; put msg

14+ put (NamePart n) = do putWord8 1 ; put n

15+ put (TermPart t) = do putWord8 2 ; put t

16+ put (SubReport ps) = do putWord8 3 ; put ps

17+

18+ get = do i <- getWord8

19+ case i of

20+ 0 -> fmap TextPart get

21+ 1 -> fmap NamePart get

22+ 2 -> fmap TermPart get

23+ 3 -> fmap SubReport get

24+ _ -> error "Corrupted binary data for ErrorReportPart"

25+

26+instance Binary a => Binary (Err' a) where

27+ put (Msg str) = do putWord8 0

28+ put str

29+ put (InternalMsg str) = do putWord8 1

30+ put str

31+ put (CantUnify x y z e ctxt i) = do putWord8 2

32+ put x

33+ put y

34+ put z

35+ put e

36+ put ctxt

37+ put i

38+ put (InfiniteUnify n t ctxt) = do putWord8 3

39+ put n

40+ put t

41+ put ctxt

42+ put (CantConvert x y ctxt) = do putWord8 4

43+ put x

44+ put y

45+ put ctxt

46+ put (CantSolveGoal x ctxt) = do putWord8 5

47+ put x

48+ put ctxt

49+ put (UnifyScope n1 n2 x ctxt) = do putWord8 6

50+ put n1

51+ put n2

52+ put x

53+ put ctxt

54+ put (CantInferType str) = do putWord8 7

55+ put str

56+ put (NonFunctionType t1 t2) = do putWord8 8

57+ put t1

58+ put t2

59+ put (NotEquality t1 t2) = do putWord8 9

60+ put t1

61+ put t2

62+ put (TooManyArguments n) = do putWord8 10

63+ put n

64+ put (CantIntroduce t) = do putWord8 11

65+ put t

66+ put (NoSuchVariable n) = do putWord8 12

67+ put n

68+ put (NoTypeDecl n) = do putWord8 13

69+ put n

70+ put (NotInjective x y z) = do putWord8 14

71+ put x

72+ put y

73+ put z

74+ put (CantResolve t) = do putWord8 15

75+ put t

76+ put (CantResolveAlts ns) = do putWord8 16

77+ put ns

78+ put (IncompleteTerm t) = do putWord8 17

79+ put t

80+ put UniverseError = putWord8 18

81+ put (UniqueError u n) = do putWord8 19

82+ put u

83+ put n

84+ put (UniqueKindError u n) = do putWord8 20

85+ put u

86+ put n

87+ put ProgramLineComment = putWord8 21

88+ put (Inaccessible n) = do putWord8 22

89+ put n

90+ put (NonCollapsiblePostulate n) = do putWord8 23

91+ put n

92+ put (AlreadyDefined n) = do putWord8 24

93+ put n

94+ put (ProofSearchFail e) = do putWord8 25

95+ put e

96+ put (NoRewriting t) = do putWord8 26

97+ put t

98+ put (At fc e) = do putWord8 27

99+ put fc

100+ put e

101+ put (Elaborating str n e) = do putWord8 28

102+ put str

103+ put n

104+ put e

105+ put (ElaboratingArg n1 n2 ns e) = do putWord8 29

106+ put n1

107+ put n2

108+ put ns

109+ put e

110+ put (ProviderError str) = do putWord8 30

111+ put str

112+ put (LoadingFailed str e) = do putWord8 31

113+ put str

114+ put e

115+ put (ReflectionError parts e) = do putWord8 32

116+ put parts

117+ put e

118+ put (ReflectionFailed str e) = do putWord8 33

119+ put str

120+ put e

121+

122+ get = do i <- getWord8

123+ case i of

124+ 0 -> fmap Msg get

125+ 1 -> fmap InternalMsg get

126+ 2 -> do x <- get ; y <- get ; z <- get ; e <- get ; ctxt <- get ; i <- get

127+ return $ CantUnify x y z e ctxt i

128+ 3 -> do x <- get ; y <- get ; z <- get

129+ return $ InfiniteUnify x y z

130+ 4 -> do x <- get ; y <- get ; z <- get

131+ return $ CantConvert x y z

132+ 5 -> do x <- get ; y <- get

133+ return $ CantSolveGoal x y

134+ 6 -> do w <- get ; x <- get ; y <- get ; z <- get

135+ return $ UnifyScope w x y z

136+ 7 -> fmap CantInferType get

137+ 8 -> do x <- get ; y <- get

138+ return $ NonFunctionType x y

139+ 9 -> do x <- get ; y <- get

140+ return $ NotEquality x y

141+ 10 -> fmap TooManyArguments get

142+ 11 -> fmap CantIntroduce get

143+ 12 -> fmap NoSuchVariable get

144+ 13 -> fmap NoTypeDecl get

145+ 14 -> do x <- get ; y <- get ; z <- get

146+ return $ NotInjective x y z

147+ 15 -> fmap CantResolve get

148+ 16 -> fmap CantResolveAlts get

149+ 17 -> fmap IncompleteTerm get

150+ 18 -> return UniverseError

151+ 19 -> do x <- get ; y <- get

152+ return $ UniqueError x y

153+ 20 -> do x <- get ; y <- get

154+ return $ UniqueKindError x y

155+ 21 -> return ProgramLineComment

156+ 22 -> fmap Inaccessible get

157+ 23 -> fmap NonCollapsiblePostulate get

158+ 24 -> fmap AlreadyDefined get

159+ 25 -> fmap ProofSearchFail get

160+ 26 -> fmap NoRewriting get

161+ 27 -> do x <- get ; y <- get

162+ return $ At x y

163+ 28 -> do x <- get ; y <- get ; z <- get

164+ return $ Elaborating x y z

165+ 29 -> do w <- get ; x <- get ; y <- get ; z <- get

166+ return $ ElaboratingArg w x y z

167+ 30 -> fmap ProviderError get

168+ 31 -> do x <- get ; y <- get

169+ return $ LoadingFailed x y

170+ 32 -> do x <- get ; y <- get

171+ return $ ReflectionError x y

172+ 33 -> do x <- get ; y <- get

173+ return $ ReflectionFailed x y

174+ _ -> error "Corrupted binary data for Err'"

10----- Generated by 'derive'

175----- Generated by 'derive'

11

176

12instance Binary FC where

177instance Binary FC where

@@ -145,6 +310,7 @@ instance Binary Const where

145 B64V x1 -> putWord8 24 >> put x1

310 B64V x1 -> putWord8 24 >> put x1

146 BufferType -> putWord8 25

311 BufferType -> putWord8 25

147 ManagedPtrType -> putWord8 26

312 ManagedPtrType -> putWord8 26

313+ VoidType -> putWord8 27

148 get

314 get

149 = do i <- getWord8

315 = do i <- getWord8

150 case i of

316 case i of

@@ -187,7 +353,7 @@ instance Binary Const where

187 24 -> fmap B64V get

353 24 -> fmap B64V get

188 25 -> return BufferType

354 25 -> return BufferType

189 26 -> return ManagedPtrType

355 26 -> return ManagedPtrType

190−

356+ 27 -> return VoidType

191 _ -> error "Corrupted binary data for Const"

357 _ -> error "Corrupted binary data for Const"

192

358

193

359

@@ -208,6 +374,8 @@ instance Binary Raw where

208 put x1

374 put x1

209 RForce x1 -> do putWord8 5

375 RForce x1 -> do putWord8 5

210 put x1

376 put x1

377+ RUType x1 -> do putWord8 6

378+ put x1

211 get

379 get

212 = do i <- getWord8

380 = do i <- getWord8

213 case i of

381 case i of

@@ -225,6 +393,8 @@ instance Binary Raw where

225 return (RConstant x1)

393 return (RConstant x1)

226 5 -> do x1 <- get

394 5 -> do x1 <- get

227 return (RForce x1)

395 return (RForce x1)

396+ 6 -> do x1 <- get

397+ return (RUType x1)

228 _ -> error "Corrupted binary data for Raw"

398 _ -> error "Corrupted binary data for Raw"

229

399

230

400

src/Idris/Core/TT.hs+2−1

@@ -103,6 +103,7 @@ data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe String) (Maybe St

103 | AnnTextFmt TextFormatting

104 | AnnTerm [(Name, Bool)] (TT Name) -- ^ pprint bound vars, original term

105 | AnnSearchResult Ordering -- ^ more general, isomorphic, or more specific

106+ | AnnErr Err

106

107

107-- | Used for error reflection

108-- | Used for error reflection

108data ErrorReportPart = TextPart String

109data ErrorReportPart = TextPart String

@@ -117,7 +118,7 @@ data ErrorReportPart = TextPart String

117

118

118-- | Idris errors. Used as exceptions in the compiler, but reported to users

119-- | Idris errors. Used as exceptions in the compiler, but reported to users

119-- if they reach the top level.

120-- if they reach the top level.

120−data Err' t

121+data Err' t

121 = Msg String

122 = Msg String

122 | InternalMsg String

123 | InternalMsg String

123 | CantUnify Bool t t (Err' t) [(Name, t)] Int

124 | CantUnify Bool t t (Err' t) [(Name, t)] Int

src/Idris/Delaborate.hs+6−4

@@ -9,7 +9,7 @@ import Util.Pretty

9import Idris.AbsSyntax

10import Idris.Core.TT

11import Idris.Core.Evaluate

12−import Idris.Docstrings (overview, renderDocstring)

12+import Idris.Docstrings (overview, renderDocstring, renderDocTerm)

13import Idris.ErrReverse

14

15import Data.List (intersperse, nub)

@@ -435,12 +435,14 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

435 _ | otherwise -> annot

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

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

438− let o = overview (fst docs)

438+ let o = overview (fst docs)

439+ norm = normaliseAll (tt_ctxt ist) []

439 -- TODO make width configurable

440 -- TODO make width configurable

440 -- Issue #1588 on the Issue Tracker

441 -- Issue #1588 on the Issue Tracker

441 -- https://github.com/idris-lang/Idris-dev/issues/1588

442 -- https://github.com/idris-lang/Idris-dev/issues/1588

442− out = displayS . renderPretty 1.0 50 $

443+ out = displayS . renderPretty 1.0 50 $

443− renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) o

444+ renderDocstring (renderDocTerm (pprintDelab ist)

445+ norm) o

444 return (out "")

446 return (out "")

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

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

446 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

448 getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

src/Idris/Docs.hs+12−12

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

6import Idris.Delaborate

7import Idris.Core.TT

8import Idris.Core.Evaluate

9−import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring)

9+import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm)

10

11import Util.Pretty

12

@@ -18,31 +18,31 @@ import qualified Data.Text as T

18--

19-- Issue #1573 on the Issue tracker.

20-- https://github.com/idris-lang/Idris-dev/issues/1573

21−data FunDoc = FD Name (Docstring (Maybe Term))

21+data FunDoc = FD Name (Docstring DocTerm)

22− [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs

22+ [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))] -- args: name, ty, implicit, docs

23 PTerm -- function type

24 (Maybe Fixity)

25− deriving Show

26

25

27data Docs = FunDoc FunDoc

26data Docs = FunDoc FunDoc

28 | DataDoc FunDoc -- type constructor docs

27 | DataDoc FunDoc -- type constructor docs

29 [FunDoc] -- data constructor docs

28 [FunDoc] -- data constructor docs

30− | ClassDoc Name (Docstring (Maybe Term))-- class docs

29+ | ClassDoc Name (Docstring DocTerm)-- class docs

31 [FunDoc] -- method docs

30 [FunDoc] -- method docs

32− [(Name, Maybe (Docstring (Maybe Term)))] -- parameters and their docstrings

31+ [(Name, Maybe (Docstring DocTerm))] -- parameters and their docstrings

33 [PTerm] -- instances

32 [PTerm] -- instances

34 [PTerm] -- superclasses

33 [PTerm] -- superclasses

35− deriving Show

36

34

35+showDoc ist d

37−showDoc ist d | nullDocstring d = empty

36+ | nullDocstring d = empty

37+ | otherwise = text " -- " <>

38− | otherwise = text " -- " <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) d

38+ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d

39

40pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

41pprintFD ist (FD n doc args ty f)

42 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>

43 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

44 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

45− renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc <$>

45+ renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>

46 maybe empty (\f -> text (show f) <> line) f <>

47 let argshow = showArgs args [] in

48 if not (null argshow)

@@ -84,7 +84,7 @@ pprintDocs ist (ClassDoc n doc meths params instances superclasses)

84 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

85 if nullDocstring doc

86 then empty

87− else line <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc)

87+ else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

88 <> line <$>

89 nest 4 (text "Parameters:" <$> prettyParameters)

90 <> line <$>

@@ -187,7 +187,7 @@ docFun n

187 funName (UN n) = str n

188 funName (NS n _) = funName n

189

190−getPArgNames :: PTerm -> [(Name, Docstring (Maybe Term))] -> [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))]

190+getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]

191getPArgNames (PPi plicity name ty body) ds =

192 (name, ty, plicity, lookup name ds) : getPArgNames body ds

193getPArgNames _ _ = []

src/Idris/Docstrings.hs+79−39

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

1{-# LANGUAGE DeriveFunctor, ScopedTypeVariables #-}

2−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

3

4-- | Wrapper around Markdown library

5module Idris.Docstrings (

6 Docstring(..), Block(..), Inline(..), parseDocstring, renderDocstring, emptyDocstring, nullDocstring, noDocs,

7− overview, containsText, renderHtml, annotCode

7+ overview, containsText, renderHtml, annotCode, DocTerm(..), renderDocTerm, checkDocstring

8 ) where

9

10import qualified Cheapskate as C

@@ -13,7 +13,7 @@ import Cheapskate.Html (renderDoc)

13

14import Util.Pretty

15

16−import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term)

16+import Idris.Core.TT (OutputAnnotation(..), TextFormatting(..), Name, Term, Err)

17

18import qualified Data.Text as T

19import qualified Data.Foldable as F

@@ -25,6 +25,22 @@ import Control.DeepSeq (NFData(..))

25

26import Text.Blaze.Html (Html)

27

28+-- | The various kinds of code samples that can be embedded in docs

29+data DocTerm = Unchecked

30+ | Checked Term

31+ | Example Term

32+ | Failing Err

33+ deriving Show

34+

35+-- | Render a term in the documentation

36+renderDocTerm :: (Term -> Doc OutputAnnotation) -> (Term -> Term) -> DocTerm -> String -> Doc OutputAnnotation

37+renderDocTerm pp norm Unchecked src = text src

38+renderDocTerm pp norm (Checked tm) src = pp tm

39+renderDocTerm pp norm (Example tm) src = align $

40+ text ">" <+> align (pp tm) <$>

41+ pp (norm tm)

42+renderDocTerm pp norm (Failing err) src = annotate (AnnErr err) $ text src

43+

28-- | Representation of Idris's inline documentation. The type paramter

44-- | Representation of Idris's inline documentation. The type paramter

29-- represents the type of terms that are associated with code blocks.

45-- represents the type of terms that are associated with code blocks.

30data Docstring a = DocString CT.Options (Blocks a)

46data Docstring a = DocString CT.Options (Blocks a)

@@ -58,6 +74,37 @@ data Inline a = Str T.Text

58type Inlines a = S.Seq (Inline a)

74type Inlines a = S.Seq (Inline a)

59

75

60

76

77+-- | Run some kind of processing step over code in a Docstring. The code

78+-- processor gets the language and annotations as parameters, along with the

79+-- source and the original annotation.

80+checkDocstring :: forall a b. (String -> [String] -> String -> a -> b) -> Docstring a -> Docstring b

81+checkDocstring f (DocString opts blocks) = DocString opts (fmap (checkBlock f) blocks)

82+ where checkBlock :: (String -> [String] -> String -> a -> b) -> Block a -> Block b

83+ checkBlock f (Para inlines) = Para (fmap (checkInline f) inlines)

84+ checkBlock f (Header i inlines) = Header i (fmap (checkInline f) inlines)

85+ checkBlock f (Blockquote bs) = Blockquote (fmap (checkBlock f) bs)

86+ checkBlock f (List b t blocks) = List b t (fmap (fmap (checkBlock f)) blocks)

87+ checkBlock f (CodeBlock attrs src tm) = CodeBlock attrs src

88+ (f (T.unpack $ CT.codeLang attrs)

89+ (words . T.unpack $ CT.codeInfo attrs)

90+ (T.unpack src)

91+ tm)

92+ checkBlock f (HtmlBlock src) = HtmlBlock src

93+ checkBlock f HRule = HRule

94+

95+ checkInline :: (String -> [String] -> String -> a -> b) -> Inline a -> Inline b

96+ checkInline f (Str txt) = Str txt

97+ checkInline f Space = Space

98+ checkInline f SoftBreak = SoftBreak

99+ checkInline f LineBreak = LineBreak

100+ checkInline f (Emph is) = Emph (fmap (checkInline f) is)

101+ checkInline f (Strong is) = Strong (fmap (checkInline f) is)

102+ checkInline f (Code src x) = Code src (f "" [] (T.unpack src) x)

103+ checkInline f (Link is url title) = Link (fmap (checkInline f) is) url title

104+ checkInline f (Image is url title) = Image (fmap (checkInline f) is) url title

105+ checkInline f (Entity txt) = Entity txt

106+ checkInline f (RawHtml src) = RawHtml src

107+

61-- | Construct a docstring from a Text that contains Markdown-formatted docs

108-- | Construct a docstring from a Text that contains Markdown-formatted docs

62parseDocstring :: T.Text -> Docstring ()

109parseDocstring :: T.Text -> Docstring ()

63parseDocstring = toDocstring . C.markdown options

110parseDocstring = toDocstring . C.markdown options

@@ -94,60 +141,53 @@ options = CT.Options { CT.sanitize = True

94 }

141 }

95

142

96-- | Convert a docstring to be shown by the pretty-printer

143-- | Convert a docstring to be shown by the pretty-printer

97−renderDocstring :: (a -> Doc OutputAnnotation) -> (a -> a) -> Docstring (Maybe a) -> Doc OutputAnnotation

144+renderDocstring :: (a -> String -> Doc OutputAnnotation) -> Docstring a -> Doc OutputAnnotation

98−renderDocstring pp norm (DocString _ blocks) = renderBlocks pp norm blocks

145+renderDocstring pp (DocString _ blocks) = renderBlocks pp blocks

99

146

100-- | Construct a docstring consisting of the first block-level element of the

147-- | Construct a docstring consisting of the first block-level element of the

101-- argument docstring, for use in summaries.

148-- argument docstring, for use in summaries.

102overview :: Docstring a -> Docstring a

149overview :: Docstring a -> Docstring a

103overview (DocString opts blocks) = DocString opts (S.take 1 blocks)

150overview (DocString opts blocks) = DocString opts (S.take 1 blocks)

104

151

105−renderBlocks :: (a -> Doc OutputAnnotation) -> (a -> a)

152+renderBlocks :: (a -> String -> Doc OutputAnnotation)

106− -> Blocks (Maybe a) -> Doc OutputAnnotation

153+ -> Blocks a -> Doc OutputAnnotation

107−renderBlocks pp norm blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

154+renderBlocks pp blocks | S.length blocks > 1 = F.foldr1 (\b1 b2 -> b1 <> line <> line <> b2) $

108− fmap (renderBlock pp norm) blocks

155+ fmap (renderBlock pp) blocks

109− | S.length blocks == 1 = renderBlock pp norm (S.index blocks 0)

156+ | S.length blocks == 1 = renderBlock pp (S.index blocks 0)

110 | otherwise = empty

157 | otherwise = empty

111

158

112−renderBlock :: (a -> Doc OutputAnnotation) -> (a -> a)

159+renderBlock :: (a -> String -> Doc OutputAnnotation)

113− -> Block (Maybe a) -> Doc OutputAnnotation

160+ -> Block a -> Doc OutputAnnotation

114−renderBlock pp norm (Para inlines) = renderInlines pp inlines

161+renderBlock pp (Para inlines) = renderInlines pp inlines

115−renderBlock pp norm (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))

162+renderBlock pp (Header lvl inlines) = renderInlines pp inlines <+> parens (text (show lvl))

116−renderBlock pp norm (Blockquote blocks) = indent 8 $ renderBlocks pp norm blocks

163+renderBlock pp (Blockquote blocks) = indent 8 $ renderBlocks pp blocks

117−renderBlock pp norm (List b ty blockss) = renderList pp norm b ty blockss

164+renderBlock pp (List b ty blockss) = renderList pp b ty blockss

118−renderBlock pp norm (CodeBlock attr src Nothing) = indent 8 $ text (T.unpack src)

165+renderBlock pp (CodeBlock attr src tm) = indent 4 $ pp tm (T.unpack src)

119−renderBlock pp norm (CodeBlock attr src (Just tm))

120− | isExample attr = indent 4 $

121− text ">" <+> align (group (pp tm)) <$>

122− align (group (pp (norm tm)))

123− | otherwise = indent 4 $ pp tm

124− where isExample (CT.CodeAttr lang info) = T.pack "example" `elem` lang : T.words info

125−renderBlock pp norm (HtmlBlock txt) = text "<html block>" -- TODO

166+renderBlock pp (HtmlBlock txt) = text "<html block>" -- TODO

126−renderBlock pp norm HRule = text "----------------------"

167+renderBlock pp HRule = text "----------------------"

127−

168+

128−renderList :: (a -> Doc OutputAnnotation) -> (a -> a)

169+renderList :: (a -> String -> Doc OutputAnnotation)

129− -> Bool -> CT.ListType -> [Blocks (Maybe a)] -> Doc OutputAnnotation

170+ -> Bool -> CT.ListType -> [Blocks a] -> Doc OutputAnnotation

130−renderList pp norm b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks pp norm) blockss

171+renderList pp b (CT.Bullet c) blockss = vsep $ map (hang 4 . (char c <+>) . renderBlocks pp) blockss

131−renderList pp norm b (CT.Numbered nw i) blockss =

172+renderList pp b (CT.Numbered nw i) blockss =

132 vsep $

173 vsep $

133 zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)

174 zipWith3 (\n p txt -> hang 4 $ text (show n) <> p <+> txt)

134− [i..] (repeat punc) (map (renderBlocks pp norm) blockss)

175+ [i..] (repeat punc) (map (renderBlocks pp) blockss)

135 where punc = case nw of

176 where punc = case nw of

136 CT.PeriodFollowing -> char '.'

177 CT.PeriodFollowing -> char '.'

137 CT.ParenFollowing -> char '('

178 CT.ParenFollowing -> char '('

138

179

139−renderInlines :: (a -> Doc OutputAnnotation) -> Inlines (Maybe a) -> Doc OutputAnnotation

180+renderInlines :: (a -> String -> Doc OutputAnnotation) -> Inlines a -> Doc OutputAnnotation

140renderInlines pp = F.foldr (<>) empty . fmap (renderInline pp)

181renderInlines pp = F.foldr (<>) empty . fmap (renderInline pp)

141

182

142−renderInline :: (a -> Doc OutputAnnotation) -> Inline (Maybe a) -> Doc OutputAnnotation

183+renderInline :: (a -> String -> Doc OutputAnnotation) -> Inline a -> Doc OutputAnnotation

143renderInline pp (Str s) = text $ T.unpack s

184renderInline pp (Str s) = text $ T.unpack s

144renderInline pp Space = softline

185renderInline pp Space = softline

145renderInline pp SoftBreak = softline

186renderInline pp SoftBreak = softline

146renderInline pp LineBreak = line

187renderInline pp LineBreak = line

147renderInline pp (Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines pp txt

188renderInline pp (Emph txt) = annotate (AnnTextFmt ItalicText) $ renderInlines pp txt

148renderInline pp (Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines pp txt

189renderInline pp (Strong txt) = annotate (AnnTextFmt BoldText) $ renderInlines pp txt

149−renderInline pp (Code txt Nothing) = text $ T.unpack txt

190+renderInline pp (Code txt tm) = pp tm $ T.unpack txt

150−renderInline pp (Code txt (Just tm)) = pp tm

151renderInline pp (Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines pp body) <+>

191renderInline pp (Link body url title) = annotate (AnnTextFmt UnderlineText) (renderInlines pp body) <+>

152 parens (text $ T.unpack url)

192 parens (text $ T.unpack url)

153renderInline pp (Image body url title) = text "<image>" -- TODO

193renderInline pp (Image body url title) = text "<image>" -- TODO

@@ -193,13 +233,13 @@ containsText str (DocString _ blocks) = F.any (blockContains (T.toLower str)) bl

193 inlineContains str (RawHtml txt) = T.isInfixOf str (T.toLower txt)

233 inlineContains str (RawHtml txt) = T.isInfixOf str (T.toLower txt)

194

234

195

235

196−renderHtml :: Docstring (Maybe Term) -> Html

236+renderHtml :: Docstring DocTerm -> Html

197renderHtml = renderDoc . fromDocstring

237renderHtml = renderDoc . fromDocstring

198 where

238 where

199− fromDocstring :: Docstring (Maybe Term) -> CT.Doc

239+ fromDocstring :: Docstring DocTerm -> CT.Doc

200 fromDocstring (DocString opts blocks) = CT.Doc opts (fmap fromBlock blocks)

240 fromDocstring (DocString opts blocks) = CT.Doc opts (fmap fromBlock blocks)

201

241

202− fromBlock :: Block (Maybe Term) -> CT.Block

242+ fromBlock :: Block DocTerm -> CT.Block

203 fromBlock (Para inlines) = CT.Para (fmap fromInline inlines)

243 fromBlock (Para inlines) = CT.Para (fmap fromInline inlines)

204 fromBlock (Header i inlines) = CT.Header i (fmap fromInline inlines)

244 fromBlock (Header i inlines) = CT.Header i (fmap fromInline inlines)

205 fromBlock (Blockquote blocks) = CT.Blockquote (fmap fromBlock blocks)

245 fromBlock (Blockquote blocks) = CT.Blockquote (fmap fromBlock blocks)

@@ -208,7 +248,7 @@ renderHtml = renderDoc . fromDocstring

208 fromBlock (HtmlBlock src) = CT.HtmlBlock src

248 fromBlock (HtmlBlock src) = CT.HtmlBlock src

209 fromBlock HRule = CT.HRule

249 fromBlock HRule = CT.HRule

210

250

211− fromInline :: Inline (Maybe Term) -> CT.Inline

251+ fromInline :: Inline DocTerm -> CT.Inline

212 fromInline (Str t) = CT.Str t

252 fromInline (Str t) = CT.Str t

213 fromInline Space = CT.Space

253 fromInline Space = CT.Space

214 fromInline SoftBreak = CT.SoftBreak

254 fromInline SoftBreak = CT.SoftBreak

src/Idris/Elab/Class.hs+2−2

@@ -52,9 +52,9 @@ import Util.Pretty(pretty, text)

52

53data MArgTy = IA | EA | CA deriving Show

54

55−elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->

55+elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

56 FC -> [PTerm] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring (Maybe PTerm))] -> [PDecl] -> Idris ()

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [PDecl] -> Idris ()

58elabClass info syn_in doc fc constraints tn ps pDocs ds

59 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

60 let tty = pibind ps PType

src/Idris/Elab/Clause.hs+1−1

@@ -30,7 +30,7 @@ import Idris.Core.Execute

30import Idris.Core.Typecheck

31import Idris.Core.CaseTree

32

33−import Idris.Docstrings

33+import Idris.Docstrings hiding (Unchecked)

34import Util.Pretty hiding ((<$>))

35

36import Prelude hiding (id, (.))

src/Idris/Elab/Data.hs+8−8

@@ -50,7 +50,7 @@ import Data.List.Split (splitOn)

50

51import Util.Pretty(pretty, text)

52

53−elabData :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm)-> [(Name, Docstring (Maybe PTerm))] -> FC -> DataOpts -> PData -> Idris ()

53+elabData :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] -> FC -> DataOpts -> PData -> Idris ()

54elabData info syn doc argDocs fc opts (PLaterdecl n t_in)

55 = do let codata = Codata `elem` opts

56 iLOG (show (fc, doc))

@@ -78,7 +78,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

78 cons <- mapM (elabCon cnameinfo syn n codata (getRetTy cty)) dcons

79 ttag <- getName

80 i <- getIState

81− let as = map (const Nothing) (getArgTys cty)

81+ let as = map (const (Left (Msg ""))) (getArgTys cty)

82 let params = findParams (map snd cons)

83 logLvl 2 $ "Parameters : " ++ show params

84 -- TI contains information about mutually declared types - this will

@@ -206,7 +206,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

206

207elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

208 Type -> -- for kind checking

209− (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) ->

209+ (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) ->

210 Idris (Name, Type)

211elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

212 = do checkUndefined fc n

@@ -279,7 +279,7 @@ type EliminatorState = StateT (Map.Map String Int) Idris

279-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

280-- rename to caseFun to match updated intend

281elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

282− [(Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name])] ->

282+ [(Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])] ->

283 ElabInfo -> EliminatorState ()

284elabCaseFun ind paramPos n ty cons info = do

285 elimLog $ "Elaborating case function"

@@ -298,7 +298,7 @@ elabCaseFun ind paramPos n ty cons info = do

298 let motiveConstr = [(motiveName, expl, motive)]

299 let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))

300 let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))

301− let eliminatorTyDecl = PTy (fmap (const Nothing) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

301+ let eliminatorTyDecl = PTy (fmap (const (Left $ Msg "")) . parseDocstring . T.pack $ show n) [] defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy

302 let clauseConsElimArgs = map getPiName consTerms

303 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

304 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

@@ -448,7 +448,7 @@ elabCaseFun ind paramPos n ty cons info = do

448 splitArgPms _ = ([],[])

449

450

451− implicitIndexes :: (Docstring (Maybe PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

451+ implicitIndexes :: (Docstring (Either Err PTerm), Name, PTerm, FC, [Name]) -> EliminatorState [(Name, Plicity, PTerm)]

452 implicitIndexes (cns@(doc, cnm, ty, fc, fs)) = do

453 i <- State.lift getIState

454 implargs' <- case lookupCtxt cnm (idris_implicits i) of

@@ -463,7 +463,7 @@ elabCaseFun ind paramPos n ty cons info = do

463 in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs

464 _ -> return implargs

465

466− extractConsTerm :: (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

466+ extractConsTerm :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm

467 extractConsTerm (doc, argDocs, cnm, ty, fc, fs) generalParameters = do

468 let cons' = replaceParams paramPos generalParameters ty

469 let (args, resTy) = splitPi cons'

@@ -499,7 +499,7 @@ elabCaseFun ind paramPos n ty cons info = do

499 convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)

500 convertImplPi _ = Nothing

501

502− generateEliminatorClauses :: (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

502+ generateEliminatorClauses :: (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name]) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause

503 generateEliminatorClauses (doc, _, cnm, ty, fc, fs) cnsElim generalArgs generalParameters = do

504 let cons' = replaceParams paramPos generalParameters ty

505 let (args, resTy) = splitPi cons'

src/Idris/Elab/Provider.hs+1−1

@@ -98,7 +98,7 @@ elabProvider info syn fc what n

98 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

99 | ProvPostulate _ <- what ->

100 do -- Add the postulate

101− elabPostulate info syn (fmap (const Nothing) . parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

101+ elabPostulate info syn (fmap (const (Left $ Msg "")) . parseDocstring $ T.pack "Provided postulate") fc [] n (delab i tm)

102 logLvl 3 $ "Elaborated provided postulate " ++ show n

103 | otherwise ->

104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

src/Idris/Elab/Record.hs+2−2

@@ -50,8 +50,8 @@ import Data.List.Split (splitOn)

50

51import Util.Pretty(pretty, text)

52

53−elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> FC -> Name ->

53+elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> Name ->

54− PTerm -> DataOpts -> Docstring (Maybe PTerm) -> Name -> PTerm -> Idris ()

54+ PTerm -> DataOpts -> Docstring (Either Err PTerm) -> Name -> PTerm -> Idris ()

55elabRecord info syn doc fc tyn ty opts cdoc cn cty_in

56 = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])

57 -- TODO think: something more in info?

src/Idris/Elab/Type.hs+3−3

@@ -114,12 +114,12 @@ buildType info syn fc opts n ty' = do

114 param_pos i ns t = []

115

116-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

117−elabType :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm)-> [(Name, Docstring (Maybe PTerm))] ->

117+elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] ->

118 FC -> FnOpts -> Name -> PTerm -> Idris Type

119elabType = elabType' False

120

121elabType' :: Bool -> -- normalise it

122− ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) -> [(Name, Docstring (Maybe PTerm))] ->

122+ ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

123 FC -> FnOpts -> Name -> PTerm -> Idris Type

124elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

125 n = liftname info n_in in -}

@@ -207,7 +207,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

207 , ns4 == map txt ["Reflection","Language"] = True

208 tyIsHandler _ = False

209

210−elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Maybe PTerm) ->

210+elabPostulate :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

211 FC -> FnOpts -> Name -> PTerm -> Idris ()

212elabPostulate info syn doc fc opts n ty = do

213 elabType info syn doc [] fc opts n ty

src/Idris/Elab/Value.hs+21−8

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

1{-# LANGUAGE PatternGuards #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

2module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where

3module Idris.Elab.Value(elabVal, elabValBind, elabDocTerms) where

3

4

4import Idris.AbsSyntax

5import Idris.AbsSyntax

@@ -22,7 +23,7 @@ import Idris.Elab.Utils

22

23

23import Idris.Core.TT

24import Idris.Core.TT

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

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

25−import Idris.Core.Evaluate

26+import Idris.Core.Evaluate hiding (Unchecked)

26import Idris.Core.Execute

27import Idris.Core.Execute

27import Idris.Core.Typecheck

28import Idris.Core.Typecheck

28import Idris.Core.CaseTree

29import Idris.Core.CaseTree

@@ -88,11 +89,23 @@ elabVal info aspat tm_in

88

89

90

91

91−elabDocTerms :: ElabInfo -> Docstring (Maybe PTerm) -> Idris (Docstring (Maybe Term))

92+elabDocTerms :: ElabInfo -> Docstring (Either Err PTerm) -> Idris (Docstring DocTerm)

92−elabDocTerms info str = Traversable.mapM decorate str

93+elabDocTerms info str = do typechecked <- Traversable.mapM decorate str

94+ return $ checkDocstring mkDocTerm typechecked

93− where decorate Nothing = return Nothing

95+ where decorate (Left err) = return (Left err)

94− decorate (Just pt) = fmap (fmap fst) (tryElabVal info ERHS pt)

96+ decorate (Right pt) = fmap (fmap fst) (tryElabVal info ERHS pt)

97+

95− tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Maybe (Term, Type))

98+ tryElabVal :: ElabInfo -> ElabMode -> PTerm -> Idris (Either Err (Term, Type))

96 tryElabVal info aspat tm_in

99 tryElabVal info aspat tm_in

97− = idrisCatch (fmap Just $ elabVal info aspat tm_in)

100+ = idrisCatch (fmap Right $ elabVal info aspat tm_in)

98− (const $ return Nothing)

101+ (return . Left)

102+

103+ mkDocTerm :: String -> [String] -> String -> Either Err Term -> DocTerm

104+ mkDocTerm lang attrs src (Left err)

105+ | map toLower lang == "idris" = Failing err

106+ | otherwise = Unchecked

107+ mkDocTerm lang attrs src (Right tm)

108+ | map toLower lang == "idris" = if "example" `elem` map (map toLower) attrs

109+ then Example tm

110+ else Checked tm

111+ | otherwise = Unchecked

src/Idris/ElabDecls.hs+1−1

@@ -38,7 +38,7 @@ import Idris.Core.Execute

38import Idris.Core.Typecheck

39import Idris.Core.CaseTree

40

41−import Idris.Docstrings

41+import Idris.Docstrings hiding (Unchecked)

42

43import Prelude hiding (id, (.))

44import Control.Category

src/Idris/IBC.hs+17−3

@@ -32,7 +32,7 @@ import Codec.Compression.Zlib (compress)

32import Util.Zlib (decompressEither)

33

34ibcVersion :: Word8

35−ibcVersion = 83

35+ibcVersion = 84

36

37data IBCFile = IBCFile { ver :: Word8,

38 sourcefile :: FilePath,

@@ -61,7 +61,7 @@ data IBCFile = IBCFile { ver :: Word8,

61 ibc_fninfo :: [(Name, FnInfo)],

62 ibc_cg :: [(Name, CGInfo)],

63 ibc_defs :: [(Name, Def)],

64− ibc_docstrings :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))],

64+ ibc_docstrings :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))],

65 ibc_transforms :: [(Name, (Term, Term))],

66 ibc_errRev :: [(Term, Term)],

67 ibc_coercions :: [Name],

@@ -459,7 +459,7 @@ pDefs syms ds

459 update (Proj t i) = Proj (update t) i

460 update t = t

461

462−pDocs :: [(Name, (Docstring (Maybe Term), [(Name, Docstring (Maybe Term))]))] -> Idris ()

462+pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris ()

463pDocs ds = mapM_ (\ (n, a) -> addDocStr n (fst a) (snd a)) ds

464

465pAccess :: [(Name, Accessibility)] -> Idris ()

@@ -538,6 +538,20 @@ instance Binary CT.Options where

538 x4 <- get

539 return (CT.Options x1 x2 x3 x4)

540

541+instance Binary D.DocTerm where

542+ put D.Unchecked = putWord8 0

543+ put (D.Checked t) = putWord8 1 >> put t

544+ put (D.Example t) = putWord8 2 >> put t

545+ put (D.Failing e) = putWord8 3 >> put e

546+

547+ get = do i <- getWord8

548+ case i of

549+ 0 -> return D.Unchecked

550+ 1 -> fmap D.Checked get

551+ 2 -> fmap D.Example get

552+ 3 -> fmap D.Failing get

553+ _ -> error "Corrupted binary data for DocTerm"

554+

541instance Binary a => Binary (D.Block a) where

555instance Binary a => Binary (D.Block a) where

542 put (D.Para lines) = do putWord8 0 ; put lines

556 put (D.Para lines) = do putWord8 0 ; put lines

543 put (D.Header i lines) = do putWord8 1 ; put i ; put lines

557 put (D.Header i lines) = do putWord8 1 ; put i ; put lines

src/Idris/IdeSlave.hs+13

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

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

2+

1{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

3{-# LANGUAGE FlexibleInstances, IncoherentInstances, PatternGuards #-}

2

4

3module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch, getLen, getNChar) where

5module Idris.IdeSlave(parseMessage, convSExp, IdeSlaveCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideSlaveEpoch, getLen, getNChar) where

@@ -151,6 +153,7 @@ instance SExpable OutputAnnotation where

151 EQ -> "isomorphic"

153 EQ -> "isomorphic"

152 LT -> "more general than searched type"

154 LT -> "more general than searched type"

153 GT -> "more specific than searched type"

155 GT -> "more specific than searched type"

156+ toSExp (AnnErr e) = toSExp [(SymbolAtom "error", StringAtom (encodeErr e))]

154

157

155encodeTerm :: [(Name, Bool)] -> Term -> String

158encodeTerm :: [(Name, Bool)] -> Term -> String

156encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

159encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $

@@ -159,6 +162,12 @@ encodeTerm bnd tm = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encod

159decodeTerm :: String -> ([(Name, Bool)], Term)

162decodeTerm :: String -> ([(Name, Bool)], Term)

160decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

163decodeTerm = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

161

164

165+encodeErr :: Err -> String

166+encodeErr e = UTF8.toString . Base64.encode . Lazy.toStrict . Binary.encode $ e

167+

168+decodeErr :: String -> Err

169+decodeErr = Binary.decode . Lazy.fromStrict . Base64.decodeLenient . UTF8.fromString

170+

162instance SExpable FC where

171instance SExpable FC where

163 toSExp (FC f (sl, sc) (el, ec)) =

172 toSExp (FC f (sl, sc) (el, ec)) =

164 toSExp ((SymbolAtom "filename", StringAtom f),

173 toSExp ((SymbolAtom "filename", StringAtom f),

@@ -219,6 +228,8 @@ data IdeSlaveCommand = REPLCompletions String

219 | TermShowImplicits [(Name, Bool)] Term

228 | TermShowImplicits [(Name, Bool)] Term

220 | TermNoImplicits [(Name, Bool)] Term

229 | TermNoImplicits [(Name, Bool)] Term

221 | PrintDef String

230 | PrintDef String

231+ | ErrString Err

232+ | ErrPPrint Err

222

233

223sexpToCommand :: SExp -> Maybe IdeSlaveCommand

234sexpToCommand :: SExp -> Maybe IdeSlaveCommand

224sexpToCommand (SexpList (x:[])) = sexpToCommand x

235sexpToCommand (SexpList (x:[])) = sexpToCommand x

@@ -262,6 +273,8 @@ sexpToCommand (SexpList [SymbolAtom "show-term-implicits", StringAtom encoded])

262sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

273sexpToCommand (SexpList [SymbolAtom "hide-term-implicits", StringAtom encoded]) = let (bnd, tm) = decodeTerm encoded in

263 Just (TermNoImplicits bnd tm)

274 Just (TermNoImplicits bnd tm)

264sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)

275sexpToCommand (SexpList [SymbolAtom "print-definition", StringAtom name]) = Just (PrintDef name)

276+sexpToCommand (SexpList [SymbolAtom "error-string", StringAtom encoded]) = Just . ErrString . decodeErr $ encoded

277+sexpToCommand (SexpList [SymbolAtom "error-pprint", StringAtom encoded]) = Just . ErrPPrint . decodeErr $ encoded

265sexpToCommand _ = Nothing

278sexpToCommand _ = Nothing

266

279

267parseMessage :: String -> Either Err (SExp, Integer)

280parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/Output.hs+6−3

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

1−{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

1+{-# OPTIONS_GHC -fwarn-incomplete-patterns -Werror #-}

2

3module Idris.Output where

4

@@ -177,12 +177,13 @@ printUndefinedNames ns = text "Undefined " <> names <> text "."

177

178

179prettyDocumentedIst :: IState

180− -> (Name, PTerm, Maybe (Docstring (Maybe Term)))

180+ -> (Name, PTerm, Maybe (Docstring DocTerm))

181 -> Doc OutputAnnotation

182prettyDocumentedIst ist (name, ty, docs) =

183 prettyName True True [] name <+> colon <+> align (prettyIst ist ty) <$>

184− fromMaybe empty (fmap (\d -> renderDocstring ppTm (normaliseAll (tt_ctxt ist) []) d <> line) docs)

184+ fromMaybe empty (fmap (\d -> renderDocstring (renderDocTerm ppTm norm) d <> line) docs)

185 where ppTm = pprintDelab ist

186+ norm = normaliseAll (tt_ctxt ist) []

186

187

188

188renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

189renderExternal :: OutputFmt -> Int -> Doc OutputAnnotation -> Idris String

@@ -220,6 +221,7 @@ renderExternal fmt width doc

220 decorate HTMLOutput (AnnTextFmt _) = id -- TODO

221 decorate HTMLOutput (AnnTextFmt _) = id -- TODO

221 decorate HTMLOutput (AnnTerm _ _) = id

222 decorate HTMLOutput (AnnTerm _ _) = id

222 decorate HTMLOutput (AnnSearchResult _) = id

223 decorate HTMLOutput (AnnSearchResult _) = id

224+ decorate HTMLOutput (AnnErr _) = id

223

225

224 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

226 decorate LaTeXOutput (AnnName _ (Just TypeOutput) _ _) =

225 latex "IdrisType"

227 latex "IdrisType"

@@ -242,6 +244,7 @@ renderExternal fmt width doc

242 decorate LaTeXOutput (AnnTextFmt _) = id -- TODO

244 decorate LaTeXOutput (AnnTextFmt _) = id -- TODO

243 decorate LaTeXOutput (AnnTerm _ _) = id

245 decorate LaTeXOutput (AnnTerm _ _) = id

244 decorate LaTeXOutput (AnnSearchResult _) = id

246 decorate LaTeXOutput (AnnSearchResult _) = id

247+ decorate LaTeXOutput (AnnErr _) = id

245

248

246 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

249 tag cls docs str = "<span class=\""++cls++"\""++title++">" ++ str ++ "</span>"

247 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

250 where title = maybe "" (\d->" title=\"" ++ d ++ "\"") docs

src/Idris/ParseData.hs+3−3

@@ -4,7 +4,7 @@ module Idris.ParseData where

4import Prelude hiding (pi)

5

6import Text.Trifecta.Delta

7−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

7+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

8import Text.Parser.LookAhead

9import Text.Parser.Expression

10import qualified Text.Parser.Token as Tok

@@ -172,7 +172,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

172{- | Parses a type constructor declaration

173 Constructor ::= DocComment? FnName TypeSig;

174-}

175−constructor :: SyntaxInfo -> IdrisParser (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, PTerm, FC, [Name])

175+constructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, PTerm, FC, [Name])

176constructor syn

177 = do (doc, argDocs) <- option noDocs docComment

178 cn_in <- fnName; fc <- getFC

@@ -191,7 +191,7 @@ constructor syn

191{- | Parses a constructor for simple discriminated union data types

192 SimpleConstructor ::= FnName SimpleExpr* DocComment?

193-}

194−simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Maybe PTerm), [(Name, Docstring (Maybe PTerm))], Name, [PTerm], FC, [Name])

194+simpleConstructor :: SyntaxInfo -> IdrisParser (Docstring (Either Err PTerm), [(Name, Docstring (Either Err PTerm))], Name, [PTerm], FC, [Name])

195simpleConstructor syn

196 = do (doc, _) <- option noDocs (try docComment)

197 ist <- get

src/Idris/ParseExpr.hs+4−4

@@ -5,7 +5,7 @@ module Idris.ParseExpr where

5import Prelude hiding (pi)

6

7import Text.Trifecta.Delta

8−import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

8+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace, Err)

9import Text.Parser.LookAhead

10import Text.Parser.Expression

11import qualified Text.Parser.Token as Tok

@@ -53,11 +53,11 @@ fullExpr syn = do x <- expr syn

53 i <- get

54 return $ debindApp syn (desugar syn i x)

55

56−tryFullExpr :: SyntaxInfo -> IState -> String -> Maybe PTerm

56+tryFullExpr :: SyntaxInfo -> IState -> String -> Either Err PTerm

57tryFullExpr syn st input =

58 case runparser (fullExpr syn) st "" input of

59− Success tm -> Just tm

59+ Success tm -> Right tm

60− _ -> Nothing

60+ Failure e -> Left (Msg (show e))

61

62{- | Parses an expression

63@

src/Idris/Parser.hs+1−1

@@ -37,7 +37,7 @@ import Idris.ParseOps

37import Idris.ParseExpr

38import Idris.ParseData

39

40−import Idris.Docstrings

40+import Idris.Docstrings hiding (Unchecked)

41

42import Paths_idris

43

src/Idris/REPL.hs+13−1

@@ -485,7 +485,19 @@ runIdeSlaveCommand h id orig fn mods (IdeSlave.PrintDef name) =

485 [] -> Left ("Didn't understand name '" ++ s ++ "'")

486 [n] -> Right $ sUN n

487 (n:ns) -> Right $ sNS (sUN n) ns

488−

488+runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrString e) =

489+ do ist <- getIState

490+ let out = displayS . renderPretty 1.0 60 $ pprintErr ist e

491+ msg = (IdeSlave.SymbolAtom "ok", IdeSlave.StringAtom $ out "")

492+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

493+runIdeSlaveCommand h id orig fn modes (IdeSlave.ErrPPrint e) =

494+ do ist <- getIState

495+ let (out, spans) =

496+ displaySpans .

497+ renderPretty 0.9 80 .

498+ fmap (fancifyAnnots ist) $ pprintErr ist e

499+ msg = (IdeSlave.SymbolAtom "ok", out, spans)

500+ runIO . hPutStrLn h $ IdeSlave.convSExp "return" msg id

489

501

490-- | Show a term for IDESlave with the specified implicitness

502-- | Show a term for IDESlave with the specified implicitness

491ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

503ideSlaveForceTermImplicits :: Handle -> Integer -> [(Name, Bool)] -> Bool -> Term -> Idris ()

test/interactive005/input+3

@@ -1,12 +1,15 @@

1+:consolewidth 80

1the Nat (1 + 2)

2the Nat (1 + 2)

2:exec

3:exec

3:c bytecode hello.bytecode

4:c bytecode hello.bytecode

4:c c hello

5:c c hello

5:doc main

6:doc main

6:reload

7:reload

8+:consolewidth 80

7:load interactive005.idr

9:load interactive005.idr

8:total main

10:total main

9:exec

11:exec

12+:consolewidth 80

10:t id

13:t id

11:set showimplicits

14:set showimplicits

12:t id

15:t id

test/interactive005/run+1−1

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

1#!/usr/bin/env bash

2−idris --quiet interactive005.idr < input

2+idris --nocolour --quiet interactive005.idr < input

3rm -f *.ibc

4rm -f hello.bytecode

5rm -f hello