fd0bbc2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1996 from adamse/type-provider-docs

Type provider docs

commitfd0bbc2f9735350434f38e012e1d3aceba2563fa authorDavid Christiansen <david@davidchristiansen.dk> dateSun 15 Mar 2015, 12:16 (12 years ago) parentd1d6a7e 774e2fe

12 files changed+75−30

compare with master

unifiedsplit

CHANGELOG+1 idris.cabal+4 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/DeepSeq.hs+2−2 src/Idris/Elab/Provider.hs+8−5 src/Idris/ElabDecls.hs+2−2 src/Idris/IBC.hs+9−6 src/Idris/Parser.hs+19−14 test/docs002/docs002.idr+16 test/docs002/expected+8 test/docs002/input+2 test/docs002/run+3

CHANGELOG+1

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

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

2424 called from foreign code

2525* Instances can now have documentation strings.

26+* Type providers can have documentation strings.

2627

2728New in 0.9.16:

2829--------------

idris.cabal+4

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

615615 test/docs001/input

616616 test/docs001/*.idr

617617 test/docs001/expected

618+ test/docs002/run

619+ test/docs002/input

620+ test/docs002/*.idr

621+ test/docs002/expected

618622

619623

620624

src/Idris/AbsSyntaxTree.hs+1−1

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

618618 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

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

624624 deriving Functor

src/Idris/DeepSeq.hs+2−2

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

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

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

167167 rnf (PDirective x1) = ()

168− rnf (PProvider x1 x2 x3 x4)

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

168+ rnf (PProvider x1 x2 x3 x4 x5)

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

170170 rnf (PTransform x1 x2 x3 x4)

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

172172

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

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

5252import Util.Pretty(pretty, text)

5353

5454-- | Elaborate a type provider

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

56−elabProvider info syn fc what n

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

56+elabProvider doc info syn fc what n

5757 = do i <- getIState

5858 -- Ensure that the experimental extension is enabled

5959 unless (TypeProviders `elem` idris_language_extensions i) $

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

9393 Provide tm

9494 | ProvTerm ty _ <- what ->

9595 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

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

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

9999 | ProvPostulate _ <- what ->

100100 do -- Add the postulate

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

101+ elabPostulate

102+ info syn

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

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

105+ fc [] n (delab i tm)

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

103107 | otherwise ->

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

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

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

121125 OK _ -> True

122126 _ -> False

123−

src/Idris/ElabDecls.hs+2−2

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

249249 addIBC (IBCDSL n)

250250elabDecl' what info (PDirective i)

251251 | what /= EDefns = i

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

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

253253 | what /= EDefns

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

255− elabProvider info syn fc provWhat n

255+ elabProvider doc info syn fc provWhat n

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

257257 = do elabTransform info fc safety old new

258258 return ()

src/Idris/IBC.hs+9−6

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

12821282 put x1

12831283 put x2

12841284 PDirective x1 -> error "Cannot serialize PDirective"

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

1286− put x1

1287− put x2

1288− put x3

1289− put x4

1285+ PProvider x1 x2 x3 x4 x5 ->

1286+ do putWord8 15

1287+ put x1

1288+ put x2

1289+ put x3

1290+ put x4

1291+ put x5

12901292 PTransform x1 x2 x3 x4 -> do putWord8 16

12911293 put x1

12921294 put x2

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

13811383 x2 <- get

13821384 x3 <- get

13831385 x4 <- get

1384− return (PProvider x1 x2 x3 x4)

1386+ x5 <- get

1387+ return (PProvider x1 x2 x3 x4 x5)

13851388 16 -> do x1 <- get

13861389 x2 <- get

13871390 x3 <- get

src/Idris/Parser.hs+19−14

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

11081108{- | Parses a type provider

11091109

11101110@

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

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

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

11131113@

11141114 -}

11151115provider :: SyntaxInfo -> IdrisParser [PDecl]

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

1117− provideTerm <|> providePostulate

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

1117+ lchar '%'

1118+ reserved "provide"

1119+ return doc)

1120+ provideTerm doc <|> providePostulate doc

11181121 <?> "type provider"

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

1120− fc <- getFC

1121− reserved "with"

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

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

1124− providePostulate = do reserved "postulate"

1125− n <- fnName

1126− fc <- getFC

1127− reserved "with"

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

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

1122+ where provideTerm doc =

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

1124+ fc <- getFC

1125+ reserved "with"

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

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

1128+ providePostulate doc =

1129+ do reserved "postulate"

1130+ n <- fnName

1131+ fc <- getFC

1132+ reserved "with"

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

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

11301135

11311136{- | Parses a transform

11321137

test/docs002/docs002.idrnew file+16

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

1+module Main

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

5+import Providers

7+%language TypeProviders

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

5+*docs002> T2 : Type

6+ Some other documentation

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