17a2a48 · Idris-dev · git.iko.soy

.travis.yml+4−1

compare with master

unifiedsplit

@@ -1,3 +1,4 @@

1+dist: trusty

1sudo: false

2sudo: false

2

3

3language: c

4language: c

@@ -153,7 +154,9 @@ script:

153 - echo -en 'travis_fold:end:script.tests\\r'

154 - echo -en 'travis_fold:end:script.tests\\r'

154###

155###

155 - echo 'Benchmarks...' && echo -en 'travis_fold:start:script.benchmarks\\r'

156 - echo 'Benchmarks...' && echo -en 'travis_fold:start:script.benchmarks\\r'

157+ - if [[ "$TESTS" == "test_c" ]]; then

156− - cd benchmarks && ./build.pl && ./run.pl && cd ..

158+ cd benchmarks && ./build.pl && ./run.pl && cd ..;

159+ fi

157 - echo -en 'travis_fold:end:script.benchmarks\\r'

160 - echo -en 'travis_fold:end:script.benchmarks\\r'

158###

161###

159# EOF

162# EOF

CHANGELOG.md+9−2

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

1+# New in 1.0.1

2+

1## Library Updates

3## Library Updates

2

4

5++ Added `Text.Lexer` and `Text.Parser` to `contrib`. These are small libraries

6+ for implementing total lexical analysers and parsers.

7+

8++ Added utility functions to `Data.SortedMap` and `Data.SortedSet` (`contrib`),

9+ most notably `merge`, merging two maps by their `Semigroup` op (`<+>`)

10+

3+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size

11+ `Prelude.WellFounded` now contains an interface `Sized a` that defines a size

4 mapping from `a` to natural numbers. For example, there is an implementation

12 mapping from `a` to natural numbers. For example, there is an implementation

5 `Sized (List a)` where `size = length`.

13 `Sized (List a)` where `size = length`.

@@ -15,8 +23,7 @@

15+ New JavaScript code generator that uses an higher level intermediate

23+ New JavaScript code generator that uses an higher level intermediate

16 representation.

24 representation.

17

25

18−+ Various optimizations of the novel JavaScript code generator to make

26++ Various optimizations of the new JavaScript code generator.

19− its results fast.

20

27

21+ Names are now annotated with their representations over the IDE

28+ Names are now annotated with their representations over the IDE

22 protocol, which allows IDEs to provide commands that work on special

29 protocol, which allows IDEs to provide commands that work on special

appveyor.yml+1−1

@@ -1,7 +1,7 @@

1version: 1.0.{build}

2init:

3- ps: >-

4− choco install cabal

4+ choco install cabal --no-progress

5

6 mkdir C:\ghc

7

libs/contrib/Data/SortedMap.idr+52−1

@@ -1,6 +1,6 @@

1module Data.SortedMap

2

3−-- TODO: write merge and split

3+-- TODO: write split

4

5private

6data Tree : Nat -> (k : Type) -> Type -> Ord k -> Type where

@@ -214,6 +214,10 @@ insert k v (M _ t) =

214 Left t' => (M _ t')

215 Right t' => (M _ t')

216

217+export

218+insertFrom : Foldable f => f (k, v) -> SortedMap k v -> SortedMap k v

219+insertFrom = flip $ foldl $ flip $ uncurry insert

220+

217export

221export

218delete : k -> SortedMap k v -> SortedMap k v

222delete : k -> SortedMap k v -> SortedMap k v

219delete _ Empty = Empty

223delete _ Empty = Empty

@@ -235,6 +239,16 @@ toList : SortedMap k v -> List (k, v)

235toList Empty = []

239toList Empty = []

236toList (M _ t) = treeToList t

240toList (M _ t) = treeToList t

237

241

242+||| Gets the keys of the map.

243+export

244+keys : SortedMap k v -> List k

245+keys = map fst . toList

246+

247+||| Gets the values of the map. Could contain duplicates.

248+export

249+values : SortedMap k v -> List v

250+values = map snd . toList

251+

238treeMap : (a -> b) -> Tree n k a o -> Tree n k b o

252treeMap : (a -> b) -> Tree n k a o -> Tree n k b o

239treeMap f (Leaf k v) = Leaf k (f v)

253treeMap f (Leaf k v) = Leaf k (f v)

240treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)

254treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)

@@ -245,3 +259,40 @@ export

245implementation Functor (SortedMap k) where

259implementation Functor (SortedMap k) where

246 map _ Empty = Empty

260 map _ Empty = Empty

247 map f (M n t) = M _ (treeMap f t)

261 map f (M n t) = M _ (treeMap f t)

262+

263+||| Merge two maps. When encountering duplicate keys, using a function to combine the values.

264+||| Uses the ordering of the first map given.

265+export

266+mergeWith : (v -> v -> v) -> SortedMap k v -> SortedMap k v -> SortedMap k v

267+mergeWith f x y = insertFrom inserted x where

268+ inserted : List (k, v)

269+ inserted = do

270+ (k, v) <- toList y

271+ let v' = (maybe id f $ lookup k x) v

272+ pure (k, v')

273+

274+||| Merge two maps using the Semigroup (and by extension, Monoid) operation.

275+||| Uses mergeWith internally, so the ordering of the left map is kept.

276+export

277+merge : Semigroup v => SortedMap k v -> SortedMap k v -> SortedMap k v

278+merge = mergeWith (<+>)

279+

280+||| Left-biased merge, also keeps the ordering specified by the left map.

281+export

282+mergeLeft : SortedMap k v -> SortedMap k v -> SortedMap k v

283+mergeLeft = mergeWith const

284+

285+-- TODO: is this the right variant of merge to use for this? I think it is, but

286+-- I could also see the advantages of using `mergeLeft`. The current approach is

287+-- strictly more powerful I believe, because `mergeLeft` can be emulated with

288+-- the `First` monoid. However, this does require more code to do the same

289+-- thing.

290+export

291+Semigroup v => Semigroup (SortedMap k v) where

292+ (<+>) = merge

293+

294+||| For `neutral <+> y`, y is rebuilt in `Ord k`, so this is not a "strict" Monoid.

295+||| However, semantically, it should be equal.

296+export

297+(Ord k, Semigroup v) => Monoid (SortedMap k v) where

298+ neutral = empty

libs/contrib/Data/SortedSet.idr+4

@@ -60,3 +60,7 @@ Ord k => Semigroup (SortedSet k) where

60export

61Ord k => Monoid (SortedSet k) where

62 neutral = empty

63+

64+export

65+keySet : SortedMap k v -> SortedSet k

66+keySet = SetWrapper . map (const ())

libs/contrib/Text/Lexer.idrnew file+238

@@ -0,0 +1,238 @@

1+module Text.Lexer

2+

3+%default total

4+

5+||| A language of token recognisers.

6+||| The `consumes` flag is True is the recogniser is guaranteed to consume

7+||| at least one character

8+export

9+data Recognise : (consumes : Bool) -> Type where

10+ Empty : Recognise False

11+ Fail : Recognise c

12+ Pred : (Char -> Bool) -> Recognise True

13+ SeqEat : Recognise True -> Inf (Recognise e) -> Recognise True

14+ SeqEmpty : Recognise e1 -> Recognise e2 -> Recognise (e1 || e2)

15+ Alt : Recognise e1 -> Recognise e2 -> Recognise (e1 && e2)

16+

17+||| A token recogniser. Guaranteed to consume at least one character.

18+public export

19+Lexer : Type

20+Lexer = Recognise True

21+

22+public export

23+inf : Bool -> Type -> Type

24+inf True t = Inf t

25+inf False t = t

26+

27+||| Sequence two recognisers. If either consumes a character, the sequence

28+||| is guaranteed to consume a character.

29+export %inline

30+(<+>) : {c1 : Bool} ->

31+ Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)

32+(<+>) {c1 = False} = SeqEmpty

33+(<+>) {c1 = True} = SeqEat

34+

35+||| Alternative recognisers. If both consume, the combination is guaranteed

36+||| to consumer a character.

37+export

38+(<|>) : Recognise c1 -> Recognise c2 -> Recognise (c1 && c2)

39+(<|>) = Alt

40+

41+||| Recognise a specific character

42+export

43+is : Char -> Lexer

44+is x = Pred (==x)

45+

46+||| Recognise anything but the given character

47+export

48+isNot : Char -> Lexer

49+isNot x = Pred (/=x)

50+

51+||| Recognise a sequence of at least one sub-lexers

52+export

53+some : Lexer -> Lexer

54+some l = l <+> (some l <|> Empty)

55+

56+||| Recognise a sequence of at zero or more sub-lexers. This is not

57+||| guaranteed to consume input

58+export

59+many : Lexer -> Recognise False

60+many l = some l <|> Empty

61+

62+||| Recognise any character

63+export

64+any : Lexer

65+any = Pred (const True)

66+

67+||| Recognise no input (doesn't consume any input)

68+export

69+empty : Recognise False

70+empty = Empty

71+

72+||| Recognise a character that matches a predicate

73+export

74+pred : (Char -> Bool) -> Lexer

75+pred = Pred

76+

77+||| Recognise any of the characters in the given string

78+export

79+oneOf : String -> Lexer

80+oneOf cs = pred (\x => x `elem` unpack cs)

81+

82+data StrLen : Type where

83+ MkStrLen : String -> Nat -> StrLen

84+

85+getString : StrLen -> String

86+getString (MkStrLen str n) = str

87+

88+strIndex : StrLen -> Nat -> Maybe Char

89+strIndex (MkStrLen str len) i

90+ = if i >= len then Nothing

91+ else Just (assert_total (prim__strIndex str (cast i)))

92+

93+mkStr : String -> StrLen

94+mkStr str = MkStrLen str (length str)

95+

96+strTail : Nat -> StrLen -> StrLen

97+strTail start (MkStrLen str len)

98+ = MkStrLen (substr start len str) (minus len start)

99+

100+-- If the string is recognised, returns the index at which the token

101+-- ends

102+scan : Recognise c -> Nat -> StrLen -> Maybe Nat

103+scan Empty idx str = pure idx

104+scan Fail idx str = Nothing

105+scan (Pred f) idx str

106+ = do c <- strIndex str idx

107+ if f c

108+ then Just (idx + 1)

109+ else Nothing

110+scan (SeqEat r1 r2) idx str

111+ = do idx' <- scan r1 idx str

112+ -- TODO: Can we prove totality instead by showing idx has increased?

113+ assert_total (scan r2 idx' str)

114+scan (SeqEmpty r1 r2) idx str

115+ = do idx' <- scan r1 idx str

116+ scan r2 idx' str

117+scan (Alt r1 r2) idx str

118+ = case scan r1 idx str of

119+ Nothing => scan r2 idx str

120+ Just idx => Just idx

121+

122+takeToken : Lexer -> StrLen -> Maybe (String, StrLen)

123+takeToken lex str

124+ = do i <- scan lex 0 str -- i must be > 0 if successful

125+ pure (substr 0 i (getString str), strTail i str)

126+

127+||| Recognise a digit 0-9

128+export

129+digits : Lexer

130+digits = some (Pred isDigit)

131+

132+||| Recognise a specific string

133+export

134+exact : String -> Lexer

135+exact str with (unpack str)

136+ exact str | [] = Fail -- Not allowed, Lexer has to consume

137+ exact str | (x :: xs)

138+ = foldl SeqEmpty (is x) (map is xs)

139+

140+||| Recognise a whitespace character

141+export

142+space : Lexer

143+space = some (pred isSpace)

144+

145+||| Recognise a non-alphanumeric, non-whitespace character

146+export

147+symbol : Lexer

148+symbol = some (pred (\x => not (isAlphaNum x) && not (isSpace x)))

149+

150+strChar : Lexer

151+strChar = (is '\\' <+> any) <|> isNot '"'

152+

153+||| Recognise a string literal, including escaped characters.

154+||| (Note: doesn't yet handle escape sequences such as \123)

155+export

156+stringLit : Lexer

157+stringLit = is '"' <+> many strChar <+> is '"'

158+

159+||| Recognise a character literal, including escaped characters.

160+||| (Note: doesn't yet handle escape sequences such as \123)

161+export

162+charLit : Lexer

163+charLit = is '\'' <+> strChar <+> is '\''

164+

165+||| Recognise an integer literal (possibly with a '-' prefix)

166+export

167+intLit : Lexer

168+intLit = (is '-' <|> Empty) <+> digits

169+

170+||| A mapping from lexers to the tokens they produce.

171+||| This is a list of pairs `(Lexer, String -> tokenType)`

172+||| For each Lexer in the list, if a substring in the input matches, run

173+||| the associated function to produce a token of type `tokenType`

174+public export

175+TokenMap : (tokenType : Type) -> Type

176+TokenMap tokenType = List (Lexer, String -> tokenType)

177+

178+||| A token, and the line and column where it was in the input

179+public export

180+record TokenData a where

181+ constructor MkToken

182+ line : Int

183+ col : Int

184+ tok : a

185+

186+fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)

187+fspanEnd k p "" = (k, "")

188+fspanEnd k p xxs

189+ = assert_total $

190+ let x = prim__strHead xxs

191+ xs = prim__strTail xxs in

192+ if p x then fspanEnd (S k) p xs

193+ else (k, xxs)

194+

195+-- Faster version of 'span' from the prelude (avoids unpacking)

196+export

197+fspan : (Char -> Bool) -> String -> (String, String)

198+fspan p xs

199+ = let (end, rest) = fspanEnd 0 p xs in

200+ (substr 0 end xs, rest)

201+

202+tokenise : (line : Int) -> (col : Int) ->

203+ List (TokenData a) -> TokenMap a ->

204+ StrLen -> (List (TokenData a), (Int, Int, StrLen))

205+tokenise line col acc tmap str

206+ = case getFirstToken tmap str of

207+ Just (tok, line', col', rest) =>

208+ -- assert total because getFirstToken must consume something

209+ assert_total (tokenise line' col' (tok :: acc) tmap rest)

210+ Nothing => (reverse acc, (line, col, str))

211+ where

212+ countNLs : List Char -> Nat

213+ countNLs str = List.length (filter (== '\n') str)

214+

215+ getCols : String -> Int -> Int

216+ getCols x c

217+ = case fspan (/= '\n') (reverse x) of

218+ (incol, "") => c + cast (length incol)

219+ (incol, _) => cast (length incol)

220+

221+ getFirstToken : TokenMap a -> StrLen -> Maybe (TokenData a, Int, Int, StrLen)

222+ getFirstToken [] str = Nothing

223+ getFirstToken ((lex, fn) :: ts) str

224+ = case takeToken lex str of

225+ Just (tok, rest) => Just (MkToken line col (fn tok),

226+ line + cast (countNLs (unpack tok)),

227+ getCols tok col, rest)

228+ Nothing => getFirstToken ts str

229+

230+||| Given a mapping from lexers to token generating functions (the

231+||| TokenMap a) and an input string, return a list of recognised tokens,

232+||| and the line, column, and remainder of the input at the first point in the

233+||| string where there are no recognised tokens.

234+export

235+lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))

236+lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in

237+ (ts, (l, c, getString str'))

238+

libs/contrib/Text/Parser.idrnew file+229

@@ -0,0 +1,229 @@

1+module Text.Parser

2+

3+%default total

4+

5+-- TODO: Add some primitives for helping with error messages.

6+-- e.g. perhaps set a string to state what we're currently trying to

7+-- parse, or to say what the next expected token is in words

8+

9+||| Description of a language's grammar. The `tok` parameter is the type

10+||| of tokens, and the `consumes` flag is True if the language is guaranteed

11+||| to be non-empty - that is, successfully parsing the language is guaranteed

12+||| to consume some input.

13+export

14+data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where

15+ Empty : (val : ty) -> Grammar tok False ty

16+ Terminal : (tok -> Maybe a) -> Grammar tok True a

17+ NextIs : (tok -> Bool) -> Grammar tok False tok

18+ EOF : Grammar tok False ()

19+

20+ Fail : String -> Grammar tok c ty

21+ Commit : Grammar tok False ()

22+

23+ SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->

24+ Grammar tok True b

25+ SeqEmpty : {c1, c2 : Bool} ->

26+ Grammar tok c1 a -> (a -> Grammar tok c2 b) ->

27+ Grammar tok (c1 || c2) b

28+ Alt : {c1, c2 : Bool} ->

29+ Grammar tok c1 ty -> Grammar tok c2 ty ->

30+ Grammar tok (c1 && c2) ty

31+

32+public export

33+inf : Bool -> Type -> Type

34+inf True t = Inf t

35+inf False t = t

36+

37+||| Sequence two grammars. If either consumes some input, the sequence is

38+||| guaranteed to consume some input. If the first one consumes input, the

39+||| second is allowed to be recursive (because it means some input has been

40+||| consumed and therefore the input is smaller)

41+export %inline

42+(>>=) : {c1 : Bool} ->

43+ Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->

44+ Grammar tok (c1 || c2) b

45+(>>=) {c1 = False} = SeqEmpty

46+(>>=) {c1 = True} = SeqEat

47+

48+||| Give two alternative grammars. If both consume, the combination is

49+||| guaranteed to consume.

50+export

51+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->

52+ Grammar tok (c1 && c2) ty

53+(<|>) = Alt

54+

55+export

56+pure : (val : ty) -> Grammar tok False ty

57+pure = Empty

58+

59+||| Check whether the next token satisfies a predicate

60+export

61+nextIs : (tok -> Bool) -> Grammar tok False tok

62+nextIs = NextIs

63+

64+||| Look at the next token in the input

65+export

66+peek : Grammar tok False tok

67+peek = nextIs (const True)

68+

69+||| Succeeds if running the predicate on the next token returns Just x,

70+||| returning x. Otherwise fails.

71+export

72+terminal : (tok -> Maybe a) -> Grammar tok True a

73+terminal = Terminal

74+

75+||| Always fail with a message

76+export

77+fail : String -> Grammar tok c ty

78+fail = Fail

79+

80+||| Succeed if the input is empty

81+export

82+eof : Grammar tok False ()

83+eof = EOF

84+

85+||| Commit to an alternative; if the current branch of an alternative

86+||| fails to parse, no more branches will be tried

87+export

88+commit : Grammar tok False ()

89+commit = Commit

90+

91+data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where

92+ Failure : {xs : List tok} ->

93+ (committed : Bool) ->

94+ (err : String) -> (rest : List tok) -> ParseResult xs c ty

95+ EmptyRes : (committed : Bool) ->

96+ (val : ty) -> (more : List tok) -> ParseResult more False ty

97+ NonEmptyRes : (committed : Bool) ->

98+ (val : ty) -> (more : List tok) ->

99+ ParseResult (x :: xs ++ more) c ty

100+

101+weakenRes : {whatever, c : Bool} -> {xs : List tok} ->

102+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty

103+weakenRes (Failure com msg ts) = Failure com msg ts

104+weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs

105+weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs

106+weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more

107+

108+shorter : (more : List tok) -> .(ys : List tok) ->

109+ LTE (S (length more)) (S (length (ys ++ more)))

110+shorter more [] = lteRefl

111+shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))

112+

113+doParse : {c : Bool} ->

114+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->

115+ ParseResult xs c ty

116+doParse com xs act with (smallerAcc xs)

117+ doParse com xs (Empty val) | sml = EmptyRes com val xs

118+ doParse com [] (Fail str) | sml = Failure com str []

119+ doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)

120+ doParse com xs Commit | sml = EmptyRes True () xs

121+

122+ doParse com [] (Terminal f) | sml = Failure com "End of input" []

123+ doParse com (x :: xs) (Terminal f) | sml

124+ = maybe

125+ (Failure com "Unrecognised token" (x :: xs))

126+ (\a => NonEmptyRes com {xs=[]} a xs)

127+ (f x)

128+ doParse com [] EOF | sml = EmptyRes com () []

129+ doParse com (x :: xs) EOF | sml

130+ = Failure com "Expected end of input" (x :: xs)

131+ doParse com [] (NextIs f) | sml = Failure com "End of input" []

132+ doParse com (x :: xs) (NextIs f) | sml

133+ = if f x

134+ then EmptyRes com x (x :: xs)

135+ else Failure com "Unrecognised token" (x :: xs)

136+ doParse com xs (Alt x y) | sml with (doParse False xs x | sml)

137+ doParse com xs (Alt x y) | sml | Failure com' msg ts

138+ = if com' -- If the alternative had committed, don't try the

139+ -- other branch (and reset commit flag)

140+ then Failure com msg ts

141+ else weakenRes (doParse False xs y | sml)

142+ -- Successfully parsed the first option, so use the outer commit flag

143+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)

144+ = EmptyRes com val xs

145+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)

146+ = NonEmptyRes com val more

147+ doParse com xs (SeqEmpty act next) | (Access morerec)

148+ = case doParse com xs act | Access morerec of

149+ Failure com msg ts => Failure com msg ts

150+ EmptyRes com val xs =>

151+ case doParse com xs (next val) | (Access morerec) of

152+ Failure com' msg ts => Failure com' msg ts

153+ EmptyRes com' val xs => EmptyRes com' val xs

154+ NonEmptyRes com' val more => NonEmptyRes com' val more

155+ NonEmptyRes {x} {xs=ys} com val more =>

156+ case (doParse com more (next val) | morerec _ (shorter more ys)) of

157+ Failure com' msg ts => Failure com' msg ts

158+ EmptyRes com' val _ => NonEmptyRes com' val more

159+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>

160+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in

161+ NonEmptyRes com' val more'

162+ doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)

163+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts

164+ = Failure com' msg ts

165+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)

166+ = case doParse com' more (next val) | morerec _ (shorter more ys) of

167+ Failure com' msg ts => Failure com' msg ts

168+ EmptyRes com' val _ => NonEmptyRes com' val more

169+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>

170+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in

171+ NonEmptyRes com' val more'

172+ -- This next line is not strictly necessary, but it stops the coverage

173+ -- checker taking a really long time and eating lots of memory...

174+ doParse _ _ _ | sml = Failure True "Help the coverage checker!" []

175+

176+public export

177+data ParseError tok = Error String (List tok)

178+

179+||| Parse a list of tokens according to the given grammar. If successful,

180+||| returns a pair of the parse result and the unparsed tokens (the remaining

181+||| input).

182+export

183+parse : (xs : List tok) -> (act : Grammar tok c ty) ->

184+ Either (ParseError tok) (ty, List tok)

185+parse xs act

186+ = case doParse False xs act of

187+ Failure _ msg ts => Left (Error msg ts)

188+ EmptyRes _ val rest => pure (val, rest)

189+ NonEmptyRes _ val rest => pure (val, rest)

190+

191+||| Parse one or more things

192+export

193+some : Grammar tok True a ->

194+ Grammar tok True (List a)

195+some p = do x <- p

196+ (do xs <- some p

197+ pure (x :: xs)) <|> pure [x]

198+

199+||| Parse zero or more things (may match the empty input)

200+export

201+many : Grammar tok True a ->

202+ Grammar tok False (List a)

203+many p = some p

204+ <|> pure []

205+

206+||| Parse one or more things, separated by another thing

207+export

208+sepBy1 : Grammar tok True () -> Grammar tok True a ->

209+ Grammar tok True (List a)

210+sepBy1 sep p = do x <- p

211+ (do sep

212+ xs <- sepBy1 sep p

213+ pure (x :: xs)) <|> pure [x]

214+

215+||| Parse zero or more things, separated by another thing. May

216+||| match the empty input.

217+export

218+sepBy : Grammar tok True () -> Grammar tok True a ->

219+ Grammar tok False (List a)

220+sepBy sep p = sepBy1 sep p <|> pure []

221+

222+||| Optionally parse a thing, with a default value if the grammar doesn't

223+||| match. May match the empty input.

224+export

225+optional : Grammar tok True a -> (ifNothing : a) ->

226+ Grammar tok False a

227+optional p def = p <|> pure def

228+

229+

libs/contrib/contrib.ipkg+2

@@ -30,4 +30,6 @@ modules = CFFI, CFFI.Types, CFFI.Memory,

30

31 System.Concurrency.Process,

32

33+ Text.Lexer, Text.Parser,

34+

33 Data.Fin.Extra

35 Data.Fin.Extra

libs/prelude/Prelude/Cast.idr+1−1

@@ -7,7 +7,7 @@ import public Builtins

7

8||| Interface for transforming an instance of a data type to another type.

9interface Cast from to where

10− ||| Perform a cast operation.

10+ ||| Perform a (potentially lossy!) cast operation.

11 |||

12 ||| @orig The original type.

13 cast : (orig : from) -> to

libs/prelude/Prelude/Nat.idr+2−5

@@ -191,13 +191,10 @@ maximum Z m = m

191maximum (S n) Z = S n

192maximum (S n) (S m) = S (maximum n m)

193

194−||| Tail recursive cast Nat to Int

194+||| Cast Nat to Int

195||| Note that this can overflow

196toIntNat : Nat -> Int

197−toIntNat n = toIntNat' n 0 where

197+toIntNat n = prim__truncBigInt_Int (toIntegerNat n)

198− toIntNat' : Nat -> Int -> Int

199− toIntNat' Z x = x

200− toIntNat' (S n) x = toIntNat' n (x + 1)

201

198

202(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat

199(-) : (m : Nat) -> (n : Nat) -> {auto smaller : LTE n m} -> Nat

203(-) m n {smaller} = minus m n

200(-) m n {smaller} = minus m n

rts/idris_gc.c+1−1

@@ -24,7 +24,7 @@ VAL copy(VM* vm, VAL x) {

24 cl = MKFLOATc(vm, x->info.f);

25 break;

26 case CT_STRING:

27− cl = MKSTRc(vm, x->info.str);

27+ cl = MKSTRclen(vm, x->info.str.str, x->info.str.len);

28 break;

29 case CT_STROFFSET:

30 cl = MKSTROFFc(vm, x->info.str_offset);

rts/idris_gmp.h+2

@@ -7,6 +7,8 @@

7#include "mini-gmp.h"

8#endif

9

10+#include "idris_rts.h"

11+

10// Set memory allocation functions

12// Set memory allocation functions

11void init_gmpalloc(void);

13void init_gmpalloc(void);

12

14

rts/idris_main.c+1

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

3#include "idris_rts.h"

4#include "idris_stats.h"

5

6+void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);

6#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)

7#if defined(WIN32) || defined(__WIN32) || defined(__WIN32__)

7#include <Windows.h>

8#include <Windows.h>

8int win32_get_argv_utf8(int *argc_ptr, char ***argv_ptr)

9int win32_get_argv_utf8(int *argc_ptr, char ***argv_ptr)

rts/idris_rts.c+86−42

@@ -285,19 +285,27 @@ VAL MKSTR(VM* vm, const char* str) {

285 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +

286 sizeof(char)*len, 0);

287 SETTY(cl, CT_STRING);

288− cl -> info.str = (char*)cl + sizeof(Closure);

288+ cl->info.str.str = (char*)cl + sizeof(Closure);

289 if (str == NULL) {

290− cl->info.str = NULL;

290+ cl->info.str.str = NULL;

291 } else {

292− strcpy(cl -> info.str, str);

292+ strcpy(cl->info.str.str, str);

293 }

294+ cl->info.str.len = len > 0 ? len : 0;

294 return cl;

295 return cl;

295}

296}

296

297

297char* GETSTROFF(VAL stroff) {

298char* GETSTROFF(VAL stroff) {

298 // Assume STROFF

299 // Assume STROFF

299 StrOffset* root = stroff->info.str_offset;

300 StrOffset* root = stroff->info.str_offset;

300− return (root->str->info.str + root->offset);

301+ return (root->str->info.str.str + root->offset);

302+}

303+

304+size_t GETSTROFFLEN(VAL stroff) {

305+ // Assume STROFF

306+ // we're working in char* here so no worries about utf8 char length

307+ StrOffset* root = stroff->info.str_offset;

308+ return (root->str->info.str.len - root->offset);

301}

309}

302

310

303VAL MKCDATA(VM* vm, CHeapItem * item) {

311VAL MKCDATA(VM* vm, CHeapItem * item) {

@@ -342,12 +350,26 @@ VAL MKFLOATc(VM* vm, double val) {

342}

350}

343

351

344VAL MKSTRc(VM* vm, char* str) {

352VAL MKSTRc(VM* vm, char* str) {

353+ int len = strlen(str);

354+

355+ Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +

356+ sizeof(char)*len+1, 1);

357+ SETTY(cl, CT_STRING);

358+ cl -> info.str.str = (char*)cl + sizeof(Closure);

359+

360+ strcpy(cl->info.str.str, str);

361+ cl->info.str.len = len;

362+ return cl;

363+}

364+

365+VAL MKSTRclen(VM* vm, char* str, int len) {

345 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +

366 Closure* cl = allocate(sizeof(Closure) + // Type) + sizeof(char*) +

346− sizeof(char)*strlen(str)+1, 1);

367+ sizeof(char)*len+1, 1);

347 SETTY(cl, CT_STRING);

368 SETTY(cl, CT_STRING);

348− cl -> info.str = (char*)cl + sizeof(Closure);

369+ cl -> info.str.str = (char*)cl + sizeof(Closure);

349

370

350− strcpy(cl -> info.str, str);

371+ strcpy(cl->info.str.str, str);

372+ cl->info.str.len = len;

351 return cl;

373 return cl;

352}

374}

353

375

@@ -397,6 +419,13 @@ VAL MKB64(VM* vm, uint64_t bits64) {

397 return cl;

419 return cl;

398}

420}

399

421

422+void idris_trace(VM* vm, const char* func, int line) {

423+ printf("At %s:%d\n", func, line);

424+ dumpStack(vm);

425+ puts("");

426+ fflush(stdout);

427+}

428+

400void dumpStack(VM* vm) {

429void dumpStack(VM* vm) {

401 int i = 0;

430 int i = 0;

402 VAL* root;

431 VAL* root;

@@ -404,7 +433,8 @@ void dumpStack(VM* vm) {

404 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {

433 for (root = vm->valstack; root < vm->valstack_top; ++root, ++i) {

405 printf("%d: ", i);

434 printf("%d: ", i);

406 dumpVal(*root);

435 dumpVal(*root);

407− if (*root >= (VAL)(vm->heap.heap) && *root < (VAL)(vm->heap.end)) { printf("OK"); }

436+ if (*root >= (VAL)(vm->heap.heap) && *root < (VAL)(vm->heap.end)) { printf(" OK"); }

437+ if (root == vm->valstack_base) { printf(" <--- base"); }

408 printf("\n");

438 printf("\n");

409 }

439 }

410 printf("RET: ");

440 printf("RET: ");

@@ -428,7 +458,7 @@ void dumpVal(VAL v) {

428 printf("] ");

458 printf("] ");

429 break;

459 break;

430 case CT_STRING:

460 case CT_STRING:

431− printf("STR[%s]", v->info.str);

461+ printf("STR[%s]", v->info.str.str);

432 break;

462 break;

433 case CT_FWD:

463 case CT_FWD:

434 printf("CT_FWD ");

464 printf("CT_FWD ");

@@ -490,8 +520,9 @@ VAL idris_castIntStr(VM* vm, VAL i) {

490 int x = (int) GETINT(i);

520 int x = (int) GETINT(i);

491 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);

521 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*16, 0);

492 SETTY(cl, CT_STRING);

522 SETTY(cl, CT_STRING);

493− cl -> info.str = (char*)cl + sizeof(Closure);

523+ cl->info.str.str = (char*)cl + sizeof(Closure);

494− sprintf(cl -> info.str, "%d", x);

524+ sprintf(cl->info.str.str, "%d", x);

525+ cl->info.str.len = strlen(cl->info.str.str);

495 return cl;

526 return cl;

496}

527}

497

528

@@ -503,32 +534,33 @@ VAL idris_castBitsStr(VM* vm, VAL i) {

503 case CT_BITS8:

534 case CT_BITS8:

504 // max length 8 bit unsigned int str 3 chars (256)

535 // max length 8 bit unsigned int str 3 chars (256)

505 cl = allocate(sizeof(Closure) + sizeof(char)*4, 0);

536 cl = allocate(sizeof(Closure) + sizeof(char)*4, 0);

506− cl->info.str = (char*)cl + sizeof(Closure);

537+ cl->info.str.str = (char*)cl + sizeof(Closure);

507− sprintf(cl->info.str, "%" PRIu8, (uint8_t)i->info.bits8);

538+ sprintf(cl->info.str.str, "%" PRIu8, (uint8_t)i->info.bits8);

508 break;

539 break;

509 case CT_BITS16:

540 case CT_BITS16:

510 // max length 16 bit unsigned int str 5 chars (65,535)

541 // max length 16 bit unsigned int str 5 chars (65,535)

511 cl = allocate(sizeof(Closure) + sizeof(char)*6, 0);

542 cl = allocate(sizeof(Closure) + sizeof(char)*6, 0);

512− cl->info.str = (char*)cl + sizeof(Closure);

543+ cl->info.str.str = (char*)cl + sizeof(Closure);

513− sprintf(cl->info.str, "%" PRIu16, (uint16_t)i->info.bits16);

544+ sprintf(cl->info.str.str, "%" PRIu16, (uint16_t)i->info.bits16);

514 break;

545 break;

515 case CT_BITS32:

546 case CT_BITS32:

516 // max length 32 bit unsigned int str 10 chars (4,294,967,295)

547 // max length 32 bit unsigned int str 10 chars (4,294,967,295)

517 cl = allocate(sizeof(Closure) + sizeof(char)*11, 0);

548 cl = allocate(sizeof(Closure) + sizeof(char)*11, 0);

518− cl->info.str = (char*)cl + sizeof(Closure);

549+ cl->info.str.str = (char*)cl + sizeof(Closure);

519− sprintf(cl->info.str, "%" PRIu32, (uint32_t)i->info.bits32);

550+ sprintf(cl->info.str.str, "%" PRIu32, (uint32_t)i->info.bits32);

520 break;

551 break;

521 case CT_BITS64:

552 case CT_BITS64:

522 // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615)

553 // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615)

523 cl = allocate(sizeof(Closure) + sizeof(char)*21, 0);

554 cl = allocate(sizeof(Closure) + sizeof(char)*21, 0);

524− cl->info.str = (char*)cl + sizeof(Closure);

555+ cl->info.str.str = (char*)cl + sizeof(Closure);

525− sprintf(cl->info.str, "%" PRIu64, (uint64_t)i->info.bits64);

556+ sprintf(cl->info.str.str, "%" PRIu64, (uint64_t)i->info.bits64);

526 break;

557 break;

527 default:

558 default:

528 fprintf(stderr, "Fatal Error: ClosureType %d, not an integer type", ty);

559 fprintf(stderr, "Fatal Error: ClosureType %d, not an integer type", ty);

529 exit(EXIT_FAILURE);

560 exit(EXIT_FAILURE);

530 }

561 }

531

562

563+ cl->info.str.len = strlen(cl->info.str.str);

532 SETTY(cl, CT_STRING);

564 SETTY(cl, CT_STRING);

533 return cl;

565 return cl;

534}

566}

@@ -545,8 +577,10 @@ VAL idris_castStrInt(VM* vm, VAL i) {

545VAL idris_castFloatStr(VM* vm, VAL i) {

577VAL idris_castFloatStr(VM* vm, VAL i) {

546 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);

578 Closure* cl = allocate(sizeof(Closure) + sizeof(char)*32, 0);

547 SETTY(cl, CT_STRING);

579 SETTY(cl, CT_STRING);

548− cl -> info.str = (char*)cl + sizeof(Closure);

580+ cl->info.str.str = (char*)cl + sizeof(Closure);

549− snprintf(cl -> info.str, 32, "%.16g", GETFLOAT(i));

581+ snprintf(cl->info.str.str, 32, "%.16g", GETFLOAT(i));

582+

583+ cl->info.str.len = strlen(cl->info.str.str);

550 return cl;

584 return cl;

551}

585}

552

586

@@ -559,11 +593,13 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {

559 char *ls = GETSTR(l);

593 char *ls = GETSTR(l);

560 // dumpVal(l);

594 // dumpVal(l);

561 // printf("\n");

595 // printf("\n");

562− Closure* cl = allocate(sizeof(Closure) + strlen(ls) + strlen(rs) + 1, 0);

596+ Closure* cl = allocate(sizeof(Closure) + GETSTRLEN(l) + GETSTRLEN(r) + 1, 0);

563 SETTY(cl, CT_STRING);

597 SETTY(cl, CT_STRING);

564− cl -> info.str = (char*)cl + sizeof(Closure);

598+ cl->info.str.str = (char*)cl + sizeof(Closure);

565− strcpy(cl -> info.str, ls);

599+ strcpy(cl->info.str.str, ls);

566− strcat(cl -> info.str, rs);

600+ strcat(cl->info.str.str, rs);

601+

602+ cl->info.str.len = GETSTRLEN(l) + GETSTRLEN(r);

567 return cl;

603 return cl;

568}

604}

569

605

@@ -670,21 +706,26 @@ VAL idris_strTail(VM* vm, VAL str) {

670VAL idris_strCons(VM* vm, VAL x, VAL xs) {

706VAL idris_strCons(VM* vm, VAL x, VAL xs) {

671 char *xstr = GETSTR(xs);

707 char *xstr = GETSTR(xs);

672 int xval = GETINT(x);

708 int xval = GETINT(x);

709+ int xlen = GETSTRLEN(xs);

710+

673 if ((xval & 0x80) == 0) { // ASCII char

711 if ((xval & 0x80) == 0) { // ASCII char

674 Closure* cl = allocate(sizeof(Closure) +

712 Closure* cl = allocate(sizeof(Closure) +

675− strlen(xstr) + 2, 0);

713+ xlen + 2, 0);

676 SETTY(cl, CT_STRING);

714 SETTY(cl, CT_STRING);

677− cl -> info.str = (char*)cl + sizeof(Closure);

715+ cl->info.str.str = (char*)cl + sizeof(Closure);

678− cl -> info.str[0] = (char)(GETINT(x));

716+ cl->info.str.str[0] = (char)(GETINT(x));

679− strcpy(cl -> info.str+1, xstr);

717+ strcpy(cl->info.str.str+1, xstr);

718+ cl->info.str.len = xlen + 1;

680 return cl;

719 return cl;

681 } else {

720 } else {

682 char *init = idris_utf8_fromChar(xval);

721 char *init = idris_utf8_fromChar(xval);

722+ int newlen = strlen(init) + xlen;

683− Closure* cl = allocate(sizeof(Closure) + strlen(init) + strlen(xstr) + 1, 0);

723+ Closure* cl = allocate(sizeof(Closure) + newlen + 1, 0);

684 SETTY(cl, CT_STRING);

724 SETTY(cl, CT_STRING);

685− cl -> info.str = (char*)cl + sizeof(Closure);

725+ cl->info.str.str = (char*)cl + sizeof(Closure);

686− strcpy(cl -> info.str, init);

726+ strcpy(cl->info.str.str, init);

687− strcat(cl -> info.str, xstr);

727+ strcat(cl->info.str.str, xstr);

728+ cl->info.str.len = newlen;

688 free(init);

729 free(init);

689 return cl;

730 return cl;

690 }

731 }

@@ -701,7 +742,7 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {

701 char* str_val = GETSTR(str);

742 char* str_val = GETSTR(str);

702

743

703 // If the substring is a suffix, use idris_strShift to avoid reallocating

744 // If the substring is a suffix, use idris_strShift to avoid reallocating

704− if (offset_val + length_val >= strlen(str_val)) {

745+ if (offset_val + length_val >= GETSTRLEN(str)) {

705 return idris_strShift(vm, str, offset_val);

746 return idris_strShift(vm, str, offset_val);

706 }

747 }

707 else {

748 else {

@@ -709,20 +750,23 @@ VAL idris_substr(VM* vm, VAL offset, VAL length, VAL str) {

709 char *end = idris_utf8_advance(start, length_val);

750 char *end = idris_utf8_advance(start, length_val);

710 Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);

751 Closure* newstr = allocate(sizeof(Closure) + (end - start) +1, 0);

711 SETTY(newstr, CT_STRING);

752 SETTY(newstr, CT_STRING);

712− newstr -> info.str = (char*)newstr + sizeof(Closure);

753+ newstr->info.str.str = (char*)newstr + sizeof(Closure);

713− memcpy(newstr -> info.str, start, end - start);

754+ memcpy(newstr->info.str.str, start, end - start);

714− *(newstr -> info.str + (end - start) + 1) = '\0';

755+ *(newstr->info.str.str + (end - start) + 1) = '\0';

756+ newstr->info.str.len = strlen(newstr->info.str.str);

715 return newstr;

757 return newstr;

716 }

758 }

717}

759}

718

760

719VAL idris_strRev(VM* vm, VAL str) {

761VAL idris_strRev(VM* vm, VAL str) {

720 char *xstr = GETSTR(str);

762 char *xstr = GETSTR(str);

763+ int xlen = GETSTRLEN(str);

764+

721− Closure* cl = allocate(sizeof(Closure) +

765+ Closure* cl = allocate(sizeof(Closure) + xlen + 1, 0);

722− strlen(xstr) + 1, 0);

723 SETTY(cl, CT_STRING);

766 SETTY(cl, CT_STRING);

724− cl->info.str = (char*)cl + sizeof(Closure);

767+ cl->info.str.str = (char*)cl + sizeof(Closure);

768+ cl->info.str.len = xlen;

725− idris_utf8_rev(xstr, cl->info.str);

769+ idris_utf8_rev(xstr, cl->info.str.str);

726 return cl;

770 return cl;

727}

771}

728

772

@@ -832,7 +876,7 @@ VAL doCopyTo(VM* vm, VAL x) {

832 cl = MKFLOATc(vm, x->info.f);

876 cl = MKFLOATc(vm, x->info.f);

833 break;

877 break;

834 case CT_STRING:

878 case CT_STRING:

835− cl = MKSTRc(vm, x->info.str);

879+ cl = MKSTRc(vm, x->info.str.str);

836 break;

880 break;

837 case CT_BIGINT:

881 case CT_BIGINT:

838 cl = MKBIGMc(vm, x->info.ptr);

882 cl = MKBIGMc(vm, x->info.ptr);

rts/idris_rts.h+20−3

@@ -42,6 +42,11 @@ typedef struct {

42 size_t offset;

43} StrOffset;

44

45+typedef struct {

46+ char* str;

47+ size_t len; // Cached strlen (we do 'strlen' a lot)

48+} String;

49+

45// A foreign pointer, managed by the idris GC

50// A foreign pointer, managed by the idris GC

46typedef struct {

51typedef struct {

47 size_t size;

52 size_t size;

@@ -59,7 +64,7 @@ typedef struct Closure {

59 con c;

64 con c;

60 int i;

65 int i;

61 double f;

66 double f;

62− char* str;

67+ String str;

63 StrOffset* str_offset;

68 StrOffset* str_offset;

64 void* ptr;

69 void* ptr;

65 uint8_t bits8;

70 uint8_t bits8;

@@ -182,7 +187,8 @@ typedef void(*func)(VM*, VAL*);

182#define ALIGN(__p, __alignment) ((__p + __alignment - 1) & ~(__alignment - 1))

187#define ALIGN(__p, __alignment) ((__p + __alignment - 1) & ~(__alignment - 1))

183

188

184// Retrieving values

189// Retrieving values

185−#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str) : GETSTROFF(x))

190+#define GETSTR(x) (ISSTR(x) ? (((VAL)(x))->info.str.str) : GETSTROFF(x))

191+#define GETSTRLEN(x) (ISSTR(x) ? (((VAL)(x))->info.str.len) : GETSTROFFLEN(x))

186#define GETPTR(x) (((VAL)(x))->info.ptr)

192#define GETPTR(x) (((VAL)(x))->info.ptr)

187#define GETMPTR(x) (((VAL)(x))->info.mptr->data)

193#define GETMPTR(x) (((VAL)(x))->info.mptr->data)

188#define GETFLOAT(x) (((VAL)(x))->info.f)

194#define GETFLOAT(x) (((VAL)(x))->info.f)

@@ -229,7 +235,15 @@ typedef intptr_t i_int;

229

235

230// Stack management

236// Stack management

231

237

238+#ifdef IDRIS_TRACE

239+#define TRACE idris_trace(vm, __FUNCTION__, __LINE__);

240+#else

241+#define TRACE

242+#endif

243+

232−#define INITFRAME VAL* myoldbase

244+#define INITFRAME TRACE\

245+ VAL* myoldbase

246+

233#define REBASE vm->valstack_base = oldbase

247#define REBASE vm->valstack_base = oldbase

234#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \

248#define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \

235 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); }

249 else { memset(vm->valstack_top, 0, (x)*sizeof(VAL)); }

@@ -255,11 +269,13 @@ VAL MKCDATA(VM* vm, CHeapItem * item);

255VAL MKFLOATc(VM* vm, double val);

269VAL MKFLOATc(VM* vm, double val);

256VAL MKSTROFFc(VM* vm, StrOffset* off);

270VAL MKSTROFFc(VM* vm, StrOffset* off);

257VAL MKSTRc(VM* vm, char* str);

271VAL MKSTRc(VM* vm, char* str);

272+VAL MKSTRclen(VM* vm, char* str, int len);

258VAL MKPTRc(VM* vm, void* ptr);

273VAL MKPTRc(VM* vm, void* ptr);

259VAL MKMPTRc(VM* vm, void* ptr, size_t size);

274VAL MKMPTRc(VM* vm, void* ptr, size_t size);

260VAL MKCDATAc(VM* vm, CHeapItem * item);

275VAL MKCDATAc(VM* vm, CHeapItem * item);

261

276

262char* GETSTROFF(VAL stroff);

277char* GETSTROFF(VAL stroff);

278+size_t GETSTROFFLEN(VAL stroff);

263

279

264// #define SETTAG(x, a) (x)->info.c.tag = (a)

280// #define SETTAG(x, a) (x)->info.c.tag = (a)

265#define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a))

281#define SETARG(x, i, a) ((x)->info.c.args)[i] = ((VAL)(a))

@@ -340,6 +356,7 @@ VM* idris_getSender(Msg* msg);

340int idris_getChannel(Msg* msg);

356int idris_getChannel(Msg* msg);

341void idris_freeMsg(Msg* msg);

357void idris_freeMsg(Msg* msg);

342

358

359+void idris_trace(VM* vm, const char* func, int line);

343void dumpVal(VAL r);

360void dumpVal(VAL r);

344void dumpStack(VM* vm);

361void dumpStack(VM* vm);

345

362

src/IRTS/CodegenC.hs+18−18

@@ -151,29 +151,29 @@ showCStr s = '"' : foldr ((++) . showChar) "\"" s

151 -- Note: we need the double quotes around the codes because otherwise

152 -- "\n3" would get encoded as "\x0a3", which is incorrect.

153 -- Instead, we opt for "\x0a""3" and let the C compiler deal with it.

154− | ord c < 0x10 = "\"\"\\x0" ++ showHex (ord c) "\"\""

155− | ord c < 0x20 = "\"\"\\x" ++ showHex (ord c) "\"\""

154+ | ord c < 0x20 = showUTF8 (ord c)

156 | ord c < 0x7f = [c] -- 0x7f = \DEL

155 | ord c < 0x7f = [c] -- 0x7f = \DEL

157 | otherwise = showHexes (utf8bytes (ord c))

156 | otherwise = showHexes (utf8bytes (ord c))

158

157

158+ showUTF8 c = "\"\"\\x" ++ pad (showHex c "") ++ "\"\""

159+ showHexes = foldr ((++) . showUTF8) ""

160+

159 utf8bytes :: Int -> [Int]

161 utf8bytes :: Int -> [Int]

160− utf8bytes x = let (h : bytes) = split [] x in

162+ utf8bytes x

161− headHex h (length bytes) : map toHex bytes

163+ | x <= 0x7f = [x]

164+ | x <= 0x7ff = let (y : ys) = split [] 2 x in (y .|. 0xc0) : map (.|. 0x80) ys

165+ | x <= 0xffff = let (y : ys) = split [] 3 x in (y .|. 0xe0) : map (.|. 0x80) ys

166+ | x <= 0x10ffff = let (y : ys) = split [] 4 x in (y .|. 0xf0) : map (.|. 0x80) ys

167+ | otherwise = error $ "Invalid Unicode code point U+" ++ showHex x ""

162 where

168 where

163− split acc 0 = acc

169+ split acc 1 x = x : acc

164− split acc x = let xbits = x .&. 0x3f

170+ split acc i x = split (x .&. 0x3f : acc) (i - 1) (shiftR x 6)

165− xrest = shiftR x 6 in

171+

166− split (xbits : acc) xrest

172+ pad :: String -> String

167−

173+ pad s = case length s of

168− headHex h 1 = h + 0xc0

174+ 1 -> "0" ++ s

169− headHex h 2 = h + 0xe0

175+ 2 -> s

170− headHex h 3 = h + 0xf0

176+ _ -> error $ "Can't happen: String of invalid length " ++ show s

171− headHex h n = error "Can't happen: Invalid UTF8 character"

172−

173− toHex i = i + 0x80

174−

175− showHexes = foldr ((++) . showUTF8) ""

176− showUTF8 c = "\"\"\\x" ++ showHex c "\"\""

177

178bcc :: Int -> BC -> String

179bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"

src/IRTS/JavaScript/AST.hs+8−19

@@ -99,35 +99,24 @@ data JsExpr

99

100translateChar :: Char -> String

101translateChar ch

102− | '\a' <- ch = "\\u0007"

103 | '\b' <- ch = "\\b"

102 | '\b' <- ch = "\\b"

104 | '\f' <- ch = "\\f"

103 | '\f' <- ch = "\\f"

105 | '\n' <- ch = "\\n"

104 | '\n' <- ch = "\\n"

106 | '\r' <- ch = "\\r"

105 | '\r' <- ch = "\\r"

107 | '\t' <- ch = "\\t"

106 | '\t' <- ch = "\\t"

108 | '\v' <- ch = "\\v"

107 | '\v' <- ch = "\\v"

109− | '\SO' <- ch = "\\u000E"

110− | '\DEL' <- ch = "\\u007F"

111 | '\\' <- ch = "\\\\"

108 | '\\' <- ch = "\\\\"

112 | '\"' <- ch = "\\\""

109 | '\"' <- ch = "\\\""

113 | '\'' <- ch = "\\\'"

110 | '\'' <- ch = "\\\'"

111+ | ord ch < 0x20 = "\\x" ++ pad 2 (showHex (ord ch) "")

112+ | ord ch < 0x7f = [ch] -- 0x7f '\DEL'

114− | ch `elem` asciiTab = "\\u" ++ fill (showHex (ord ch) "")

113+ | ord ch <= 0xff = "\\x" ++ pad 2 (showHex (ord ch) "")

115− | ord ch > 255 = "\\u" ++ fill (showHex (ord ch) "")

114+ | ord ch <= 0xffff = "\\u" ++ pad 4 (showHex (ord ch) "")

116− | otherwise = [ch]

115+ | ord ch <= 0x10ffff = "\\u{" ++ showHex (ord ch) "}"

116+ | otherwise = error $ "Invalid Unicode code point U+" ++ showHex (ord ch) ""

117 where

118− fill :: String -> String

118+ pad :: Int -> String -> String

119− fill s = case length s of

119+ pad n s = replicate (n - length s) '0' ++ s

120− 1 -> "000" ++ s

121− 2 -> "00" ++ s

122− 3 -> "0" ++ s

123− _ -> s

124−

125− asciiTab =

126− ['\NUL', '\SOH', '\STX', '\ETX', '\EOT', '\ENQ', '\ACK', '\BEL',

127− '\BS', '\HT', '\LF', '\VT', '\FF', '\CR', '\SO', '\SI',

128− '\DLE', '\DC1', '\DC2', '\DC3', '\DC4', '\NAK', '\SYN', '\ETB',

129− '\CAN', '\EM', '\SUB', '\ESC', '\FS', '\GS', '\RS', '\US']

130−

131

120

132indent :: Text -> Text

121indent :: Text -> Text

133indent x =

122indent x =

src/IRTS/JavaScript/PrimOp.hs+10−3

@@ -28,7 +28,7 @@ import IRTS.Lang

28data JsPrimTy = PTBool | PTAny deriving (Eq, Ord)

29

30type PrimF = [JsExpr] -> JsExpr

31−type PrimDec = (Bool, JsPrimTy, PrimF)

31+type PrimDec = (Bool, JsPrimTy, PrimF) -- the bool indicates if bigint library is used or not

32

33deriving instance Ord PrimFn

34

@@ -177,15 +177,22 @@ primDB =

177 , item (LZExt (ITFixed IT16) ITNative) False PTAny $ head

178 , item (LZExt (ITFixed IT32) ITNative) False PTAny $ head

179 , item (LZExt ITNative ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"

180+ , item (LZExt (ITFixed IT8) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"

181+ , item (LZExt (ITFixed IT16) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"

182+ , item (LZExt (ITFixed IT32) ITBig) True PTAny $ JsForeign "new $JSRTS.jsbn.BigInteger(''+%0)"

183+ , item (LZExt (ITFixed IT64) ITBig) True PTAny $ head

180 , item (LTrunc ITBig ITNative) True PTAny $ JsForeign "%0.intValue()|0"

184 , item (LTrunc ITBig ITNative) True PTAny $ JsForeign "%0.intValue()|0"

185+ , item (LTrunc ITBig (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"

186+ , item (LTrunc ITBig (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"

187+ , item (LTrunc ITBig (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"

188+ , item (LTrunc ITBig (ITFixed IT64)) True PTAny $

189+ \[x] -> JsForeign "%0.and(new $JSRTS.jsbn.BigInteger(%1))" [x, JsStr $ show 0xFFFFFFFFFFFFFFFF]

181 , item (LTrunc (ITFixed IT16) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"

190 , item (LTrunc (ITFixed IT16) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"

182 , item (LTrunc (ITFixed IT32) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"

191 , item (LTrunc (ITFixed IT32) (ITFixed IT8)) False PTAny $ JsForeign "%0 & 0xFF"

183 , item (LTrunc (ITFixed IT64) (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"

192 , item (LTrunc (ITFixed IT64) (ITFixed IT8)) True PTAny $ JsForeign "%0.intValue() & 0xFF"

184 , item (LTrunc (ITFixed IT32) (ITFixed IT16)) False PTAny $ JsForeign "%0 & 0xFFFF"

193 , item (LTrunc (ITFixed IT32) (ITFixed IT16)) False PTAny $ JsForeign "%0 & 0xFFFF"

185 , item (LTrunc (ITFixed IT64) (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"

194 , item (LTrunc (ITFixed IT64) (ITFixed IT16)) True PTAny $ JsForeign "%0.intValue() & 0xFFFF"

186 , item (LTrunc (ITFixed IT64) (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"

195 , item (LTrunc (ITFixed IT64) (ITFixed IT32)) True PTAny $ JsForeign "%0.intValue() & 0xFFFFFFFF"

187− , item (LTrunc ITBig (ITFixed IT64)) True PTAny $

188− \[x] -> JsForeign "%0.and(new $JSRTS.jsbn.BigInteger(%1))" [x, JsStr $ show 0xFFFFFFFFFFFFFFFF]

189 , item LStrConcat False PTAny $ binop "+"

196 , item LStrConcat False PTAny $ binop "+"

190 , item LStrLt False PTBool $ binop "<"

197 , item LStrLt False PTBool $ binop "<"

191 , item LStrEq False PTBool $ binop "=="

198 , item LStrEq False PTBool $ binop "=="

src/Idris/Interactive.hs+5−7

@@ -111,7 +111,7 @@ addMissing :: FilePath -> Bool -> Int -> Name -> Idris ()

111addMissing fn updatefile l n

112 = do src <- runIO $ readSource fn

113 let (before, tyline : later) = splitAt (l-1) (lines src)

114− let indent = getIndent 0 (show n) tyline

114+ let indent = getIndent tyline

115 i <- getIState

116 cl <- getInternalApp fn l

117 let n' = getAppName cl

@@ -124,9 +124,9 @@ addMissing fn updatefile l n

124 if updatefile

125 then do let fb = fn ++ "~"

126 runIO $ writeSource fb (unlines (before ++ nonblank)

127− ++ extras ++

127+ ++ extras

128− (if null extras then ""

128+ ++ (if null extras then "" else "\n")

129− else "\n" ++ unlines rest))

129+ ++ unlines rest)

130 runIO $ copyFile fb fn

131 else iPrintResult extras

132 where showPat = show . stripNS

@@ -155,9 +155,7 @@ addMissing fn updatefile l n

155 "\n" ++ rest))

156 showNew nm i _ [] = return ""

157

158− getIndent i n [] = 0

158+ getIndent s = length (takeWhile isSpace s)

159− getIndent i n xs | take (length n) xs == n = i

160− getIndent i n (x : xs) = getIndent (i + 1) n xs

161

159

162

160

163makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

161makeWith :: FilePath -> Bool -> Int -> Name -> Idris ()

stack-shell.nix+1−1

@@ -2,7 +2,7 @@ with (import <nixpkgs> {});

2

3let

4 # MUST match resolver in stack.yaml

5− resolver = haskell.packages.lts-8_06.ghc;

5+ resolver = haskell.packages.lts-8_18.ghc;

6

7 native_libs = [

8 libffi

stack.yaml+1−1

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

1−resolver: lts-8.06

1+resolver: lts-8.18

2

3packages:

4 - location: .

test/TestData.hs+3−1

@@ -155,7 +155,9 @@ testFamiliesData = [

155 ( 11, ANY ),

156 ( 12, ANY ),

157 ( 13, ANY ),

158− ( 14, C_CG )]),

158+ ( 14, C_CG ),

159+ ( 15, ANY ),

160+ ( 16, ANY )]),

159 ("interfaces", "Interfaces",

161 ("interfaces", "Interfaces",

160 [ ( 1, ANY ),

162 [ ( 1, ANY ),

161 ( 2, ANY ),

163 ( 2, ANY ),

test/interactive015/expectednew file+6

@@ -0,0 +1,6 @@

1+test (Just x) = ?Nothing_rhs_1

2+

3+test : Maybe a -> Bool

4+test Nothing = False

5+test (Just x) = ?Nothing_rhs_1

6+

test/interactive015/inputnew file+2

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

1+:addmissing 3 Nothing

2+:addmissing! 3 Nothing

test/interactive015/runnew file+8

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

1+#!/usr/bin/env bash

2+

3+cp src/interactive015.idr .

4+${IDRIS:-idris} "$@" --quiet --port none interactive015.idr < input

5+

6+cat interactive015.idr

7+

8+rm -f *.ibc interactive015.idr

test/interactive015/src/interactive015.idrnew file+4

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

1+

2+test : Maybe a -> Bool

3+test Nothing = False

4+

test/interactive016/expectednew file+7

@@ -0,0 +1,7 @@

1+

2+test : Maybe a -> Bool

3+test Nothing = False

4+test (Just x) = True

5+

6+other : Int

7+other = 3

test/interactive016/inputnew file+2

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

1+:addmissing 3 Nothing

2+:addmissing! 3 Nothing

test/interactive016/runnew file+8

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

1+#!/usr/bin/env bash

2+

3+cp src/interactive016.idr .

4+${IDRIS:-idris} "$@" --quiet --port none interactive016.idr < input

5+

6+cat interactive016.idr

7+

8+rm -f *.ibc interactive016.idr

test/interactive016/src/interactive016.idrnew file+7

@@ -0,0 +1,7 @@

1+

2+test : Maybe a -> Bool

3+test Nothing = False

4+test (Just x) = True

5+

6+other : Int

7+other = 3