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

git.iko.soy/Idris-dev

Change comment rules

Comments cannot begin '{-|' or '--|'. This is now reserved for documentation comments, which will be part of the syntax to support documentation at the REPL.

commit6d7a6aaca28b2f7b6ebe75cbb63e21f285626995 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 Nov 2012, 13:05 (14 years ago) parent2bbea5b

6 files changed+33−11

compare with master

unifiedsplit

lib/Prelude.idr+1−1 src/Core/CoreParser.hs+28−4 src/IRTS/LParser.hs+1−1 src/Idris/AbsSyntax.hs+1−3 src/Idris/Parser.hs+1−1 src/Pkg/PParser.hs+1−1

lib/Prelude.idr+1−1

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

158158

159159---- Ranges

160160

161−partial

161+%assert_total

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

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

164164 else []

src/Core/CoreParser.hs+28−4

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

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

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

4− maybeWithNS) where

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

4+ idrisLexer, maybeWithNS) where

66import Core.TT

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

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

1212

1313import Control.Monad.State

14+import Data.Char

1415import Debug.Trace

1516

1617type TokenParser a = PTok.TokenParser a

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

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

3738-- <|> letter

3839

39−lexer :: TokenParser a

40−lexer = PTok.makeTokenParser idrisDef

40+idrisLexer :: TokenParser a

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 = "-}{"

4165

4266whiteSpace= PTok.whiteSpace lexer

4367lexeme = PTok.lexeme lexer

src/IRTS/LParser.hs+1−1

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

2626type LParser = GenParser Char ()

2727

2828lexer :: TokenParser ()

29−lexer = PTok.makeTokenParser idrisDef

29+lexer = idrisLexer

3030

3131whiteSpace= PTok.whiteSpace lexer

3232lexeme = PTok.lexeme lexer

src/Idris/AbsSyntax.hs+1−3

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

701701 pibind using (n:ns) sc

702702 = case lookup n using of

703703 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

706705 (pibind using ns sc)

707− else pibind using ns sc

708706

709707-- Add implicit arguments in function calls

710708addImplPat :: IState -> PTerm -> PTerm

src/Idris/Parser.hs+1−1

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

3535type IParser = GenParser Char IState

3636

3737lexer :: TokenParser IState

38−lexer = PTok.makeTokenParser idrisDef

38+lexer = idrisLexer

3939

4040whiteSpace = PTok.whiteSpace lexer

4141lexeme = PTok.lexeme lexer

src/Pkg/PParser.hs+1−1

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

1818type PParser = GenParser Char PkgDesc

1919

2020lexer :: TokenParser PkgDesc

21−lexer = PTok.makeTokenParser idrisDef

21+lexer = idrisLexer

2222

2323whiteSpace= PTok.whiteSpace lexer

2424lexeme = PTok.lexeme lexer