1c8c27e · Idris-dev · git.iko.soy

CHANGELOG+1

@@ -22,6 +22,7 @@ New in 0.9.15:

22* New REPL command :pprint pretty-prints a definition or term with LaTeX or HTML highlighting

23* Naming of data and type constructors is made consistent across the standard library (see #1516)

24* Terms in `code blocks` inside of documentation strings are now parsed and type checked. If this succeeds, they are rendered in full color in documentation lookups, and with semantic highlighting for IDEs.

25+* Fenced code blocks in docs defined with the "example" attribute are rendered as code examples.

25

26

26New in 0.9.14:

27New in 0.9.14:

27--------------

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

idris.cabal+3

@@ -302,6 +302,9 @@ Extra-source-files:

302 test/basic010/run

303 test/basic010/*.idr

304 test/basic010/expected

305+ test/basic011/run

306+ test/basic011/*.idr

307+ test/basic011/expected

305

308

306 test/buffer001-disabled/*.idr

309 test/buffer001-disabled/*.idr

307 test/buffer001-disabled/run

310 test/buffer001-disabled/run

libs/base/Data/Hash.idrnew file+85

@@ -0,0 +1,85 @@

1+module Data.Hash

2+

3+%access public

4+%default total

5+

6+{- A general purpose Hashing library (not cryptographic)

7+

8+ The core hash is djb2, which is very fast but does not have the best distribution

9+ Source: http://www.cse.yorku.ca/~oz/hash.html

10+

11+ The salted version and the magic salt are copied from Haskell's bloomfilter library

12+ Source: https://hackage.haskell.org/package/bloomfilter-2.0.0.0/docs/src/Data-BloomFilter-Hash.html#Hashable

13+-}

14+

15+||| A type that can be hashed

16+class Hashable a where

17+ saltedHash64 : a -> Bits64 -> Bits64 -- value to hash, salt, hash

18+

19+||| Computes a non cryptographic hash

20+hash : Hashable a => a -> Bits64

21+hash x = saltedHash64 x 0x16fc397cf62f64d3

22+

23+||| Given a user provided salt, computes a non cryptographic hash.

24+||| This version is meant to mitigate hash-flooding DoS attacks.

25+saltedHash : Hashable a => Bits64 -> a -> Bits64

26+saltedHash salt x = saltedHash64 x salt

27+

28+

29+||| Nth byte of a Bits64

30+private

31+byte : Bits64 -> Bits64 -> Bits64

32+byte n w = prim__lshrB64 (prim__andB64 mask w) offset

33+ where offset = 8*n

34+ mask = prim__shlB64 0xff (the Bits64 offset)

35+

36+||| Modulo of an integer, downsized to a Bits64

37+private

38+mod64 : Integer -> Bits64

39+mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)

40+

41+instance Hashable Bits64 where

42+ saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)

43+ salt

44+ [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto

45+

46+instance Hashable Integer where

47+ saltedHash64 i = saltedHash64 (mod64 i)

48+

49+instance Hashable () where

50+ saltedHash64 _ salt = salt

51+

52+instance Hashable Bool where

53+ saltedHash64 True = saltedHash64 (the Bits64 1)

54+ saltedHash64 False = saltedHash64 (the Bits64 0)

55+

56+instance Hashable Int where

57+ saltedHash64 w = saltedHash64 (prim__zextInt_B64 w)

58+

59+instance Hashable Char where

60+ saltedHash64 w = saltedHash64 (the Int (cast w))

61+

62+instance Hashable Bits8 where

63+ saltedHash64 w = saltedHash64 (prim__zextB8_B64 w)

64+

65+instance Hashable Bits16 where

66+ saltedHash64 w = saltedHash64 (prim__zextB16_B64 w)

67+

68+instance Hashable Bits32 where

69+ saltedHash64 w = saltedHash64 (prim__zextB32_B64 w)

70+

71+instance Hashable a => Hashable (Maybe a) where

72+ saltedHash64 Nothing salt = salt

73+ saltedHash64 (Just k) salt = saltedHash64 k salt

74+

75+instance (Hashable a, Hashable b) => Hashable (a, b) where

76+ saltedHash64 (a,b) salt = saltedHash64 b (saltedHash64 a salt)

77+

78+instance Hashable a => Hashable (List a) where

79+ saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l

80+

81+instance Hashable a => Hashable (Vect n a) where

82+ saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l

83+

84+instance Hashable String where

85+ saltedHash64 s = saltedHash64 (unpack s)

libs/base/base.ipkg+1−1

@@ -24,7 +24,7 @@ modules = System,

24 Data.Vect, Data.HVect, Data.Vect.Quantifiers,

25 Data.Floats, Data.Complex, Data.Heap, Data.Fun,

26 Data.Rel, Data.Buffer, Data.Erased,

27− Data.List,

27+ Data.List, Data.Hash,

28

29 Control.Isomorphism, Control.Isomorphism.Primitives,

30 Control.Monad.Identity,

libs/prelude/Builtins.idr−6

@@ -109,12 +109,6 @@ par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type

109 -- is better in any case?

110par (Delay x) = x

111

112−malloc : Int -> a -> a

113−malloc size x = x -- compiled specially

114−

115−trace_malloc : a -> a

116−trace_malloc x = x -- compiled specially

117−

118||| Assert to the totality checker than y is always structurally smaller than

112||| Assert to the totality checker than y is always structurally smaller than

119||| x (which is typically a pattern argument)

113||| x (which is typically a pattern argument)

120||| @ x the larger value (typically a pattern argument)

114||| @ x the larger value (typically a pattern argument)

libs/prelude/Prelude/Vect.idr+43

@@ -111,6 +111,31 @@ drop : (n : Nat) -> Vect (n + m) a -> Vect m a

111drop Z xs = xs

112drop (S k) (x :: xs) = drop k xs

113

114+||| Take the longest prefix of a Vect such that all elements satisfy some

115+||| Boolean predicate.

116+|||

117+||| @ p the predicate

118+takeWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)

119+takeWhile p [] = (_ ** [])

120+takeWhile p (x::xs) =

121+ let (len ** ys) = takeWhile p xs

122+ in if p x then

123+ (S len ** x :: ys)

124+ else

125+ (_ ** [])

126+

127+||| Remove the longest prefix of a Vect such that all removed elements satisfy some

128+||| Boolean predicate.

129+|||

130+||| @ p the predicate

131+dropWhile : (p : a -> Bool) -> Vect n a -> (q ** Vect q a)

132+dropWhile p [] = (_ ** [])

133+dropWhile p (x::xs) =

134+ if p x then

135+ dropWhile p xs

136+ else

137+ (_ ** x::xs)

138+

114--------------------------------------------------------------------------------

139--------------------------------------------------------------------------------

115-- Transformations

140-- Transformations

116--------------------------------------------------------------------------------

141--------------------------------------------------------------------------------

@@ -401,6 +426,15 @@ nubBy = nubBy' []

401nub : Eq a => Vect n a -> (p ** Vect p a)

426nub : Eq a => Vect n a -> (p ** Vect p a)

402nub = nubBy (==)

427nub = nubBy (==)

403

428

429+deleteBy : (a -> a -> Bool) -> a -> Vect n a -> (p ** Vect p a)

430+deleteBy _ _ [] = (_ ** [])

431+deleteBy eq x (y::ys) =

432+ let (len ** zs) = deleteBy eq x ys

433+ in if x `eq` y then (_ ** ys) else (S len ** y ::zs)

434+

435+delete : (Eq a) => a -> Vect n a -> (p ** Vect p a)

436+delete = deleteBy (==)

437+

404--------------------------------------------------------------------------------

438--------------------------------------------------------------------------------

405-- Splitting and breaking lists

439-- Splitting and breaking lists

406--------------------------------------------------------------------------------

440--------------------------------------------------------------------------------

@@ -413,6 +447,15 @@ nub = nubBy (==)

413splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)

447splitAt : (n : Nat) -> (xs : Vect (n + m) a) -> (Vect n a, Vect m a)

414splitAt n xs = (take n xs, drop n xs)

448splitAt n xs = (take n xs, drop n xs)

415

449

450+partition : (a -> Bool) -> Vect n a -> ((p ** Vect p a), (q ** Vect q a))

451+partition p [] = ((_ ** []), (_ ** []))

452+partition p (x::xs) =

453+ let ((leftLen ** lefts), (rightLen ** rights)) = partition p xs in

454+ if p x then

455+ ((S leftLen ** x::lefts), (rightLen ** rights))

456+ else

457+ ((leftLen ** lefts), (S rightLen ** x::rights))

458+

416--------------------------------------------------------------------------------

459--------------------------------------------------------------------------------

417-- Predicates

460-- Predicates

418--------------------------------------------------------------------------------

461--------------------------------------------------------------------------------

src/Idris/Delaborate.hs+1−1

@@ -441,7 +441,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

441 -- Issue #1588 on the Issue Tracker

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

443 out = displayS . renderPretty 1.0 50 $

444− renderDocstring (pprintDelab ist) o

444+ renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) o

445 return (out "")

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

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

src/Idris/Docs.hs+3−3

@@ -35,14 +35,14 @@ data Docs = FunDoc FunDoc

35 deriving Show

36

37showDoc ist d | nullDocstring d = empty

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

38+ | otherwise = text " -- " <> renderDocstring (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) doc <$>

45+ renderDocstring (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) doc)

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

88 <> line <$>

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

90 <> line <$>

src/Idris/Docstrings.hs+28−20

@@ -94,36 +94,44 @@ options = CT.Options { CT.sanitize = True

94 }

95

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

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

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

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

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

99

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

101-- argument docstring, for use in summaries.

102overview :: Docstring a -> Docstring a

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

104

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

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

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

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

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

107− fmap (renderBlock pp) blocks

108+ fmap (renderBlock pp norm) blocks

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

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

109 | otherwise = empty

110 | otherwise = empty

110

111

111−renderBlock :: (a -> Doc OutputAnnotation) -> Block (Maybe a) -> Doc OutputAnnotation

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

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

112−renderBlock pp (Para inlines) = renderInlines pp inlines

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

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

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

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

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

115−renderBlock pp (List b ty blockss) = renderList pp b ty blockss

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

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

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

117−renderBlock pp (CodeBlock attr src (Just tm)) = indent 8 $ pp tm

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

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

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

119−renderBlock pp HRule = text "----------------------"

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

120−

127+

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

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

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

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

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

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

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

124 vsep $

132 vsep $

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

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

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

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

127 where punc = case nw of

135 where punc = case nw of

128 CT.PeriodFollowing -> char '.'

136 CT.PeriodFollowing -> char '.'

129 CT.ParenFollowing -> char '('

137 CT.ParenFollowing -> char '('

src/Idris/Output.hs+2−2

@@ -3,7 +3,7 @@

3module Idris.Output where

4

5import Idris.Core.TT

6−import Idris.Core.Evaluate (isDConName, isTConName, isFnName)

6+import Idris.Core.Evaluate (isDConName, isTConName, isFnName, normaliseAll)

7

8import Idris.AbsSyntax

9import Idris.Delaborate

@@ -181,7 +181,7 @@ prettyDocumentedIst :: IState

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 d <> line) docs)

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

185 where ppTm = pprintDelab ist

186

187

test/Makefile+1−1

@@ -11,7 +11,7 @@ test_java:

11 @perl ./runtest.pl without --codegen Java

12

13test_js:

14− @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 buffer001 --codegen node

14+ @perl ./runtest.pl without sugar004 reg029 reg052 io001 dsl002 io003 effects001 effects002 buffer001 basic011 --codegen node

15

16test_llvm:

17 @perl ./runtest.pl without primitives003 sugar004 io003 buffer001 --codegen llvm

test/basic011/basic011.idrnew file+16

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

1+module Main

2+

3+import Data.Hash

4+

5+main : IO ()

6+main = do print $ hash (the Bits8 3)

7+ print $ hash (the (List Bits8) [3])

8+ print $ hash "hello world"

9+ print $ hash 'a'

10+ print $ hash (the Bits8 3)

11+ print $ hash (the Bits16 3)

12+ print $ hash (the Bits32 3)

13+ print $ hash (the Bits64 3)

14+ print $ hash (the Int 3)

15+ print $ hash (the Integer 3)

16+

test/basic011/expectednew file+10

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

1+6EA049D797FA18D6

2+6EA049D797FA18D6

3+FDA01C93B78A192F

4+AD85270E93646134

5+6EA049D797FA18D6

6+6EA049D797FA18D6

7+6EA049D797FA18D6

8+6EA049D797FA18D6

9+6EA049D797FA18D6

10+6EA049D797FA18D6

test/basic011/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ basic011.idr -o basic011

3+./basic011

4+rm -f basic011 *.ibc