f1e8a4d · Idris-dev · git.iko.soy

src/Idris/ParseData.hs+18−17

compare with master

unifiedsplit

@@ -86,25 +86,26 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do

86

87 let constructorDoc' = annotate syn ist constructorDoc

88

89− fields <- many . indented $ field syn

89+ fields <- many . indented $ fieldLine syn

90

91− return (fields, constructorName, constructorDoc')

91+ return (concat fields, constructorName, constructorDoc')

92 where

93− field :: SyntaxInfo -> IdrisParser ((Maybe (Name, FC)), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))

93+ fieldLine :: SyntaxInfo -> IdrisParser [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]

94+ fieldLine syn = do

94− field syn = do doc <- optional docComment

95+ doc <- optional docComment

95− c <- optional $ lchar '{'

96+ c <- optional $ lchar '{'

96− n <- (do (n, nfc) <- fnName

97+ let oneName = (do (n, nfc) <- fnName

97− return $ Just (expandNS syn n, nfc))

98+ return $ Just (expandNS syn n, nfc))

98− <|> (do symbol "_"

99− return Nothing)

99+ <|> (symbol "_" >> return Nothing)

100+ ns <- commaSeparated oneName

100− lchar ':'

101+ lchar ':'

101− t <- typeExpr (allowImp syn)

102+ t <- typeExpr (allowImp syn)

102− p <- endPlicity c

103+ p <- endPlicity c

103− ist <- get

104+ ist <- get

104− let doc' = case doc of -- Temp: Throws away any possible arg docs

105+ let doc' = case doc of -- Temp: Throws away any possible arg docs

105− Just (d,_) -> Just $ annotate syn ist d

106+ Just (d,_) -> Just $ annotate syn ist d

106− Nothing -> Nothing

107+ Nothing -> Nothing

107− return (n, p, t, doc')

108+ return $ map (\n -> (n, p, t, doc')) ns

108

109

109 constructor :: IdrisParser (Name, FC)

110 constructor :: IdrisParser (Name, FC)

110 constructor = (reservedHL "constructor") *> fnName

111 constructor = (reservedHL "constructor") *> fnName

src/Idris/ParseHelpers.hs+5

@@ -434,6 +434,11 @@ bindList :: (Name -> FC -> PTerm -> PTerm -> PTerm) -> [(Name, FC, PTerm)] -> PT

434bindList b [] sc = sc

435bindList b ((n, fc, t):bs) sc = b n fc t (bindList b bs sc)

436

437+{- | @commaSeparated p@ parses one or more occurences of `p`,

438+ separated by commas and optional whitespace. -}

439+commaSeparated :: MonadicParsing m => m a -> m [a]

440+commaSeparated p = p `sepBy1` (spaces >> char ',' >> spaces)

441+

437{- * Layout helpers -}

442{- * Layout helpers -}

438

443

439-- | Push indentation to stack

444-- | Push indentation to stack

test/records004/expectednew file+3

@@ -0,0 +1,3 @@

1+"Fred"

2+"Joe"

3+"Bloggs"

test/records004/records004.idrnew file+13

@@ -0,0 +1,13 @@

1+-- Test for multiple field declarations on one line with the same type

2+

3+record Person where

4+ constructor MkPerson

5+ firstName, middleName, lastName : String

6+

7+fred : Person

8+fred = MkPerson "Fred" "Joe" "Bloggs"

9+

10+main : IO ()

11+main = do printLn (firstName fred)

12+ printLn (middleName fred)

13+ printLn (lastName fred)

test/records004/runnew file+4

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

1+#!/usr/bin/env bash

2+idris $@ records004.idr -o records004

3+./records004

4+rm -f records004 *.ibc