f979614 · Idris-dev · git.iko.soy

CHANGELOG+1

compare with master

unifiedsplit

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

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

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

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

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

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

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

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

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

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

12* 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

286 | Help

287 | Eval PTerm

288 | Check PTerm

289− | DocStr Name

289+ | DocStr (Either Name Const)

290 | TotCheck Name

291 | Reload

292 | Load FilePath

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

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

1537

1538

1539+

1539instance Sized PTerm where

1540instance Sized PTerm where

1540 size (PQuote rawTerm) = size rawTerm

1541 size (PQuote rawTerm) = size rawTerm

1541 size (PRef fc name) = size name

1542 size (PRef fc name) = size name

src/Idris/Core/TT.hs+38

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

27import Debug.Trace

28import qualified Data.Map.Strict as Map

29import Data.Char

30+import Numeric (showIntAtBase)

30import qualified Data.Text as T

31import qualified Data.Text as T

31import Data.List

32import Data.List

32import Data.Maybe (listToMaybe)

33import Data.Maybe (listToMaybe)

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

542constIsType (B64V _) = False

543constIsType (B64V _) = False

543constIsType _ = True

544constIsType _ = True

544

545

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+

545data Raw = Var Name

583data Raw = Var Name

546 | RBind Name (Binder Raw) Raw

584 | RBind Name (Binder Raw) Raw

547 | RApp Raw Raw

585 | RApp Raw Raw

src/Idris/Docs.hs+16−1

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

1{-# LANGUAGE PatternGuards #-}

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

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

3

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

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

180getPArgNames (PPi plicity name ty body) ds =

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

182getPArgNames _ _ = []

183+

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

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

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

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

188+ nest 4 (line <> text str)

189+

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

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

192+ t (Str _) = PConstant StrType

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

194+ t _ = PType

195+

196+

197+

src/Idris/IdeSlave.hs+1−1

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

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

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

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

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

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

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

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

117 (SymbolAtom "type", StringAtom ty),

src/Idris/Parser.hs+5−1

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

47import Idris.Core.TT

48import Idris.Core.Evaluate

49

50−import Control.Applicative

50+import Control.Applicative hiding (Const)

51import Control.Monad

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

53import Control.Monad.State.Strict

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

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

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

1088

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

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

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

1092+

1089{- | Parses a tactic from input -}

1093{- | Parses a tactic from input -}

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

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

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

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

src/Idris/REPL.hs+12−4

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

276 [n] -> Right $ sUN n

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

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

279+ case parseConst orig name of

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

281+ Failure _ ->

279− case splitName name of

282+ case splitName name of

280− Left err -> iPrintError err

283+ Left err -> iPrintError err

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

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

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

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

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

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

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

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

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

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

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

627 (prettyIst ist (delab ist ty))

630 (prettyIst ist (delab ist ty))

628

631

629−process h fn (DocStr n)

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

630 = do ist <- getIState

633 = do ist <- getIState

631 case lookupCtxtName n (idris_docstrings ist) of

634 case lookupCtxtName n (idris_docstrings ist) of

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

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

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

634 ihRenderResult h (vsep toShow)

637 ihRenderResult h (vsep toShow)

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

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

636 return $ pprintDocs ist doc

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

637process h fn Universes

645process h fn Universes

638 = do i <- getIState

646 = do i <- getIState

639 let cs = idris_constraints i

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

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

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

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

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

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

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

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

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

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

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

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

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

test/reg018/run+1

@@ -3,3 +3,4 @@ idris $@ reg018a.idr --check

3idris $@ reg018b.idr --check

4idris $@ reg018c.idr --check

5idris $@ reg018d.idr --check

6+rm *.ibc