e16c068 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Documentation for primitives

Allow primitive types to be entered into :doc. Also add their documentation to IDESlave annotations. This stops :doc String from throwing an error. Fixes #1207.

commite16c068d817646c6a1d2e23a5ad4feb097addfe7 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 7 May 2014, 10:54 (12 years ago) parent755b5b3

8 files changed+77−9

compare with master

unifiedsplit

CHANGELOG+1 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Core/TT.hs+38 src/Idris/Docs.hs+16−1 src/Idris/IdeSlave.hs+1−1 src/Idris/Parser.hs+5−1 src/Idris/REPL.hs+12−4 src/Idris/REPLParser.hs+2−1

CHANGELOG+1

@@ -6,6 +6,7 @@ New in 0.9.13:

66* Command line option -e (or --eval) to evaluate expressions without loading the

77 REPL. This is useful for writing more portable tests.

88* Many more of the basic functions and datatypes are documented.

9+* Primitive types such as Int and String are documented

910* Removed javascript lib in favor of idris-hackers/iQuery

1011* Specify codegen for :compile REPL command (e.g. :compile javascript program.js)

1112* Remove :info REPL command, subsume and enhance its functionality in the :doc command

src/Idris/AbsSyntaxTree.hs+2−1

@@ -286,7 +286,7 @@ data Command = Quit

286286 | Help

287287 | Eval PTerm

288288 | Check PTerm

289− | DocStr Name

289+ | DocStr (Either Name Const)

290290 | TotCheck Name

291291 | Reload

292292 | Load FilePath

@@ -1536,6 +1536,7 @@ showTmImpls :: PTerm -> String

15361536showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

15371537

15381538

1539+

15391540instance Sized PTerm where

15401541 size (PQuote rawTerm) = size rawTerm

15411542 size (PRef fc name) = size name

src/Idris/Core/TT.hs+38

@@ -27,6 +27,7 @@ import Control.Monad.Trans.Error (Error(..))

2727import Debug.Trace

2828import qualified Data.Map.Strict as Map

2929import Data.Char

30+import Numeric (showIntAtBase)

3031import qualified Data.Text as T

3132import Data.List

3233import Data.Maybe (listToMaybe)

@@ -542,6 +543,43 @@ constIsType (B32V _) = False

542543constIsType (B64V _) = False

543544constIsType _ = True

544545

546+-- | Get the docstring for a Const

547+constDocs :: Const -> String

548+constDocs c@(AType (ATInt ITBig)) = "Arbitrary-precision integers"

549+constDocs c@(AType (ATInt ITNative)) = "Fixed-precision integers of undefined size"

550+constDocs c@(AType (ATInt ITChar)) = "Characters in some unspecified encoding"

551+constDocs c@(AType ATFloat) = "Double-precision floating-point numbers"

552+constDocs StrType = "Strings in some unspecified encoding"

553+constDocs PtrType = "Foreign pointers"

554+constDocs ManagedPtrType = "Managed pointers"

555+constDocs BufferType = "Copy-on-write buffers"

556+constDocs c@(AType (ATInt (ITFixed IT8))) = "Eight bits (unsigned)"

557+constDocs c@(AType (ATInt (ITFixed IT16))) = "Sixteen bits (unsigned)"

558+constDocs c@(AType (ATInt (ITFixed IT32))) = "Thirty-two bits (unsigned)"

559+constDocs c@(AType (ATInt (ITFixed IT64))) = "Sixty-four bits (unsigned)"

560+constDocs c@(AType (ATInt (ITVec IT8 16))) = "Vectors of sixteen eight-bit values"

561+constDocs c@(AType (ATInt (ITVec IT16 8))) = "Vectors of eight sixteen-bit values"

562+constDocs c@(AType (ATInt (ITVec IT32 4))) = "Vectors of four thirty-two-bit values"

563+constDocs c@(AType (ATInt (ITVec IT64 2))) = "Vectors of two sixty-four-bit values"

564+constDocs (Fl f) = "A float"

565+constDocs (I i) = "A fixed-precision integer"

566+constDocs (BI i) = "An arbitrary-precision integer"

567+constDocs (Str s) = "A string of length " ++ show (length s)

568+constDocs (Ch c) = "A character"

569+constDocs (B8 w) = "The eight-bit value 0x" ++

570+ showIntAtBase 16 intToDigit w ""

571+constDocs (B16 w) = "The sixteen-bit value 0x" ++

572+ showIntAtBase 16 intToDigit w ""

573+constDocs (B32 w) = "The thirty-two-bit value 0x" ++

574+ showIntAtBase 16 intToDigit w ""

575+constDocs (B64 w) = "The sixty-four-bit value 0x" ++

576+ showIntAtBase 16 intToDigit w ""

577+constDocs (B8V v) = "A vector of eight-bit values"

578+constDocs (B16V v) = "A vector of sixteen-bit values"

579+constDocs (B32V v) = "A vector of thirty-two-bit values"

580+constDocs (B64V v) = "A vector of sixty-four-bit values"

581+constDocs prim = "Undocumented"

582+

545583data Raw = Var Name

546584 | RBind Name (Binder Raw) Raw

547585 | RApp Raw Raw

src/Idris/Docs.hs+16−1

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

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs (pprintDocs, getDocs, FunDoc(..), Docs (..)) where

2+module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), Docs (..)) where

44import Idris.AbsSyntax

55import Idris.AbsSyntaxTree

@@ -179,3 +179,18 @@ getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Do

179179getPArgNames (PPi plicity name ty body) ds =

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

181181getPArgNames _ _ = []

182+

183+pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation

184+pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>

185+ pprintPTerm (ppOptionIst ist) [] [] [] (PConstant c) <+> colon <+>

186+ pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>

187+ nest 4 (line <> text str)

188+

189+ where t (Fl _) = PConstant $ AType ATFloat

190+ t (BI _) = PConstant $ AType (ATInt ITBig)

191+ t (Str _) = PConstant StrType

192+ t (Ch c) = PConstant $ AType (ATInt ITChar)

193+ t _ = PType

194+

195+

196+

src/Idris/IdeSlave.hs+1−1

@@ -111,7 +111,7 @@ instance SExpable OutputAnnotation where

111111 toSExp (AnnConst c) = toSExp [(SymbolAtom "decor",

112112 SymbolAtom (if constIsType c then "type" else "data")),

113113 (SymbolAtom "type", StringAtom (constTy c)),

114− (SymbolAtom "doc-overview", StringAtom "Primitive"),

114+ (SymbolAtom "doc-overview", StringAtom (constDocs c)),

115115 (SymbolAtom "name", StringAtom (show c))]

116116 toSExp (AnnData ty doc) = toSExp [(SymbolAtom "decor", SymbolAtom "data"),

117117 (SymbolAtom "type", StringAtom ty),

src/Idris/Parser.hs+5−1

@@ -47,7 +47,7 @@ import qualified Util.Pretty as P

4747import Idris.Core.TT

4848import Idris.Core.Evaluate

4949

50−import Control.Applicative

50+import Control.Applicative hiding (Const)

5151import Control.Monad

5252import Control.Monad.Error (throwError, catchError)

5353import Control.Monad.State.Strict

@@ -1086,6 +1086,10 @@ transform syn = do try (lchar '%' *> reserved "transform")

10861086parseExpr :: IState -> String -> Result PTerm

10871087parseExpr st = runparser (fullExpr defaultSyntax) st "(input)"

10881088

1089+{- | Parses a constant form input -}

1090+parseConst :: IState -> String -> Result Const

1091+parseConst st = runparser constant st "(input)"

1092+

10891093{- | Parses a tactic from input -}

10901094parseTactic :: IState -> String -> Result PTactic

10911095parseTactic st = runparser (fullTactic defaultSyntax) st "(input)"

src/Idris/REPL.hs+12−4

@@ -276,9 +276,12 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.TypeOf name) =

276276 [n] -> Right $ sUN n

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

278278runIdeSlaveCommand id orig fn mods (IdeSlave.DocsFor name) =

279− case splitName name of

280− Left err -> iPrintError err

281− Right n -> process stdout "(ideslave)" (DocStr n)

279+ case parseConst orig name of

280+ Success c -> process stdout "(ideslave)" (DocStr (Right c))

281+ Failure _ ->

282+ case splitName name of

283+ Left err -> iPrintError err

284+ Right n -> process stdout "(ideslave)" (DocStr (Left n))

282285runIdeSlaveCommand id orig fn mods (IdeSlave.CaseSplit line name) =

283286 process stdout fn (CaseSplitAt False line (sUN name))

284287runIdeSlaveCommand id orig fn mods (IdeSlave.AddClause line name) =

@@ -626,7 +629,7 @@ process h fn (Check t)

626629 _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))

627630 (prettyIst ist (delab ist ty))

628631

629−process h fn (DocStr n)

632+process h fn (DocStr (Left n))

630633 = do ist <- getIState

631634 case lookupCtxtName n (idris_docstrings ist) of

632635 [] -> iPrintError $ "No documentation for " ++ show n

@@ -634,6 +637,11 @@ process h fn (DocStr n)

634637 ihRenderResult h (vsep toShow)

635638 where showDoc ist (n, d) = do doc <- getDocs n

636639 return $ pprintDocs ist doc

640+

641+process h fn (DocStr (Right c))

642+ = do ist <- getIState

643+ ihRenderResult h $ pprintConstDocs ist c (constDocs c)

644+

637645process h fn Universes

638646 = do i <- getIState

639647 let cs = idris_constraints i

src/Idris/REPLParser.hs+2−1

@@ -53,7 +53,8 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

5353 <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

5454 <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

5555 <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

56− <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr n))

56+ <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))

57+ <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))

5758 <|> try (do cmd ["d", "def"]; some (P.char ' ') ; n <- P.fnName; eof; return (Defn n))

5859 <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

5960 <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))