fd0bbc2 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

@@ -23,6 +23,7 @@ New in 0.9.17:

23* Added FFI_Export type which allows Idris functions to be exportoed and

24 called from foreign code

25* Instances can now have documentation strings.

26+* Type providers can have documentation strings.

26

27

27New in 0.9.16:

28New in 0.9.16:

28--------------

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

idris.cabal+4

@@ -615,6 +615,10 @@ Extra-source-files:

615 test/docs001/input

616 test/docs001/*.idr

617 test/docs001/expected

618+ test/docs002/run

619+ test/docs002/input

620+ test/docs002/*.idr

621+ test/docs002/expected

618

622

619

623

620

624

src/Idris/AbsSyntaxTree.hs+1−1

@@ -618,7 +618,7 @@ data PDecl' t

618 | PSyntax FC Syntax -- ^ Syntax definition

619 | PMutual FC [PDecl' t] -- ^ Mutual block

620 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

621− | PProvider SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

621+ | PProvider (Docstring (Either Err PTerm)) SyntaxInfo FC (ProvideWhat' t) Name -- ^ Type provider. The first t is the type, the second is the term

622 | PTransform FC Bool t t -- ^ Source-to-source transformation rule. If

623 -- bool is True, lhs and rhs must be convertible

624 deriving Functor

src/Idris/DeepSeq.hs+2−2

@@ -165,8 +165,8 @@ instance (NFData t) => NFData (PDecl' t) where

165 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

166 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

167 rnf (PDirective x1) = ()

168− rnf (PProvider x1 x2 x3 x4)

168+ rnf (PProvider x1 x2 x3 x4 x5)

169− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

169+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

170 rnf (PTransform x1 x2 x3 x4)

171 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

172

src/Idris/Elab/Provider.hs+8−5

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

52import Util.Pretty(pretty, text)

53

54-- | Elaborate a type provider

55−elabProvider :: ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

55+elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> ProvideWhat -> Name -> Idris ()

56−elabProvider info syn fc what n

56+elabProvider doc info syn fc what n

57 = do i <- getIState

58 -- Ensure that the experimental extension is enabled

59 unless (TypeProviders `elem` idris_language_extensions i) $

@@ -93,12 +93,16 @@ elabProvider info syn fc what n

93 Provide tm

94 | ProvTerm ty _ <- what ->

95 do -- Finally add a top-level definition of the provided term

96− elabType info syn emptyDocstring [] fc [] n ty

96+ elabType info syn doc [] fc [] n ty

97 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

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

99 | ProvPostulate _ <- what ->

100 do -- Add the postulate

101+ elabPostulate

102+ info syn

103+ (fmap (const (Left $ Msg "")) .

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

104+ parseDocstring $ T.pack "Provided postulate")

105+ fc [] n (delab i tm)

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

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

103 | otherwise ->

107 | otherwise ->

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

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

@@ -120,4 +124,3 @@ elabProvider info syn fc what n

120 case converts ctxt [] (providerOf tp) prov of

124 case converts ctxt [] (providerOf tp) prov of

121 OK _ -> True

125 OK _ -> True

122 _ -> False

126 _ -> False

123−

src/Idris/ElabDecls.hs+2−2

@@ -249,10 +249,10 @@ elabDecl' _ info (PDSL n dsl)

249 addIBC (IBCDSL n)

250elabDecl' what info (PDirective i)

251 | what /= EDefns = i

252−elabDecl' what info (PProvider syn fc provWhat n)

252+elabDecl' what info (PProvider doc syn fc provWhat n)

253 | what /= EDefns

254 = do iLOG $ "Elaborating type provider " ++ show n

255− elabProvider info syn fc provWhat n

255+ elabProvider doc info syn fc provWhat n

256elabDecl' what info (PTransform fc safety old new)

257 = do elabTransform info fc safety old new

258 return ()

src/Idris/IBC.hs+9−6

@@ -1282,11 +1282,13 @@ instance (Binary t) => Binary (PDecl' t) where

1282 put x1

1283 put x2

1284 PDirective x1 -> error "Cannot serialize PDirective"

1285− PProvider x1 x2 x3 x4 -> do putWord8 15

1285+ PProvider x1 x2 x3 x4 x5 ->

1286+ do putWord8 15

1286− put x1

1287+ put x1

1287− put x2

1288+ put x2

1288− put x3

1289+ put x3

1289− put x4

1290+ put x4

1291+ put x5

1290 PTransform x1 x2 x3 x4 -> do putWord8 16

1292 PTransform x1 x2 x3 x4 -> do putWord8 16

1291 put x1

1293 put x1

1292 put x2

1294 put x2

@@ -1381,7 +1383,8 @@ instance (Binary t) => Binary (PDecl' t) where

1381 x2 <- get

1383 x2 <- get

1382 x3 <- get

1384 x3 <- get

1383 x4 <- get

1385 x4 <- get

1386+ x5 <- get

1384− return (PProvider x1 x2 x3 x4)

1387+ return (PProvider x1 x2 x3 x4 x5)

1385 16 -> do x1 <- get

1388 16 -> do x1 <- get

1386 x2 <- get

1389 x2 <- get

1387 x3 <- get

1390 x3 <- get

src/Idris/Parser.hs+19−14

@@ -1108,25 +1108,30 @@ totality

1108{- | Parses a type provider

1109

1110@

1111−Provider ::= '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1111+Provider ::= DocComment_t? '%' 'provide' Provider_What? '(' FnName TypeSig ')' 'with' Expr;

1112ProviderWhat ::= 'proof' | 'term' | 'type' | 'postulate'

1113@

1114 -}

1115provider :: SyntaxInfo -> IdrisParser [PDecl]

1116+provider syn = do doc <- try (do (doc, _) <- docstring syn

1117+ lchar '%'

1116−provider syn = do try (lchar '%' *> reserved "provide");

1118+ reserved "provide"

1119+ return doc)

1117− provideTerm <|> providePostulate

1120+ provideTerm doc <|> providePostulate doc

1118 <?> "type provider"

1121 <?> "type provider"

1122+ where provideTerm doc =

1119− where provideTerm = do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1123+ do lchar '('; n <- fnName; lchar ':'; t <- typeExpr syn; lchar ')'

1120− fc <- getFC

1124+ fc <- getFC

1121− reserved "with"

1125+ reserved "with"

1122− e <- expr syn <?> "provider expression"

1126+ e <- expr syn <?> "provider expression"

1123− return [PProvider syn fc (ProvTerm t e) n]

1127+ return [PProvider doc syn fc (ProvTerm t e) n]

1128+ providePostulate doc =

1124− providePostulate = do reserved "postulate"

1129+ do reserved "postulate"

1125− n <- fnName

1130+ n <- fnName

1126− fc <- getFC

1131+ fc <- getFC

1127− reserved "with"

1132+ reserved "with"

1128− e <- expr syn <?> "provider expression"

1133+ e <- expr syn <?> "provider expression"

1129− return [PProvider syn fc (ProvPostulate e) n]

1134+ return [PProvider doc syn fc (ProvPostulate e) n]

1130

1135

1131{- | Parses a transform

1136{- | Parses a transform

1132

1137

test/docs002/docs002.idrnew file+16

@@ -0,0 +1,16 @@

1+module Main

2+

3+-- Simple test case for type provider documentation.

4+

5+import Providers

6+

7+%language TypeProviders

8+

9+getType : Int -> IO (Provider Type)

10+getType 0 = return (Provide Int)

11+getType _ = return (Provide Bool)

12+

13+||| Some documentation

14+%provide (T1 : Type) with getType 0

15+||| Some other documentation

16+%provide (T2 : Type) with getType 1

test/docs002/expectednew file+8

@@ -0,0 +1,8 @@

1+Type checking ./docs002.idr

2+*docs002> T1 : Type

3+ Some documentation

4+

5+*docs002> T2 : Type

6+ Some other documentation

7+

8+*docs002> Bye bye

test/docs002/inputnew file+2

@@ -0,0 +1,2 @@

1+:doc T1

2+:doc T2

test/docs002/runnew file+3

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

1+#!/usr/bin/env bash

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

3+rm *.ibc