6d7a6aa · Idris-dev · git.iko.soy

lib/Prelude.idr+1−1

compare with master

unifiedsplit

@@ -158,7 +158,7 @@ ceiling x = prim__floatCeil x

158

159---- Ranges

160

161−partial

161+%assert_total

162count : (Ord a, Num a) => a -> a -> a -> List a

163count a inc b = if a <= b then a :: count (a + inc) inc b

164 else []

src/Core/CoreParser.hs+28−4

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

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

2

3−module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName, idrisDef,

3+module Core.CoreParser(parseTerm, parseFile, parseDef, pTerm, iName,

4− maybeWithNS) where

4+ idrisLexer, maybeWithNS) where

5

6import Core.TT

7

@@ -11,6 +11,7 @@ import Text.ParserCombinators.Parsec.Language

11import qualified Text.ParserCombinators.Parsec.Token as PTok

12

13import Control.Monad.State

14+import Data.Char

14import Debug.Trace

15import Debug.Trace

15

16

16type TokenParser a = PTok.TokenParser a

17type TokenParser a = PTok.TokenParser a

@@ -36,8 +37,31 @@ iOpStart = oneOf ":!#$%&*+./<=>?@\\^|-~"

36iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

37iOpLetter = oneOf ":!#$%&*+./<=>?@\\^|-~"

37-- <|> letter

38-- <|> letter

38

39

39−lexer :: TokenParser a

40+idrisLexer :: TokenParser a

40−lexer = PTok.makeTokenParser idrisDef

41+idrisLexer = (PTok.makeTokenParser idrisDef) { PTok.whiteSpace = lexWS }

42+

43+lexer = idrisLexer

44+

45+lexWS = skipMany (simpleSpace <|> oneLineComment <|> multiLineComment <?> "")

46+ where

47+

48+ simpleSpace = skipMany1 (satisfy isSpace)

49+ oneLineComment = do try (string ("--"))

50+ satisfy (/= '|')

51+ skipMany (satisfy (/= '\n'))

52+ return ()

53+ multiLineComment = do try (string "{-")

54+ satisfy (/= '|')

55+ inCommentMulti

56+

57+ inCommentMulti

58+ = do{ try (string "-}") ; return () }

59+ <|> do{ multiLineComment ; inCommentMulti }

60+ <|> do{ skipMany1 (noneOf startEnd) ; inCommentMulti }

61+ <|> do{ oneOf startEnd ; inCommentMulti }

62+ <?> "end of comment"

63+ where

64+ startEnd = "-}{"

41

65

42whiteSpace= PTok.whiteSpace lexer

66whiteSpace= PTok.whiteSpace lexer

43lexeme = PTok.lexeme lexer

67lexeme = PTok.lexeme lexer

src/IRTS/LParser.hs+1−1

@@ -26,7 +26,7 @@ type TokenParser a = PTok.TokenParser a

26type LParser = GenParser Char ()

27

28lexer :: TokenParser ()

29−lexer = PTok.makeTokenParser idrisDef

29+lexer = idrisLexer

30

31whiteSpace= PTok.whiteSpace lexer

32lexeme = PTok.lexeme lexer

src/Idris/AbsSyntax.hs+1−3

@@ -701,10 +701,8 @@ implicitise syn ignore ist tm

701 pibind using (n:ns) sc

702 = case lookup n using of

703 Just ty -> PPi (Imp False Dynamic) n ty (pibind using ns sc)

704− Nothing -> if (implicitable n)

705− then PPi (Imp False Dynamic) n Placeholder

704+ Nothing -> PPi (Imp False Dynamic) n Placeholder

706 (pibind using ns sc)

705 (pibind using ns sc)

707− else pibind using ns sc

708

706

709-- Add implicit arguments in function calls

707-- Add implicit arguments in function calls

710addImplPat :: IState -> PTerm -> PTerm

708addImplPat :: IState -> PTerm -> PTerm

src/Idris/Parser.hs+1−1

@@ -35,7 +35,7 @@ type TokenParser a = PTok.TokenParser a

35type IParser = GenParser Char IState

36

37lexer :: TokenParser IState

38−lexer = PTok.makeTokenParser idrisDef

38+lexer = idrisLexer

39

40whiteSpace = PTok.whiteSpace lexer

41lexeme = PTok.lexeme lexer

src/Pkg/PParser.hs+1−1

@@ -18,7 +18,7 @@ type TokenParser a = PTok.TokenParser a

18type PParser = GenParser Char PkgDesc

19

20lexer :: TokenParser PkgDesc

21−lexer = PTok.makeTokenParser idrisDef

21+lexer = idrisLexer

22

23whiteSpace= PTok.whiteSpace lexer

24lexeme = PTok.lexeme lexer