f1e8a4d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Multiple record fields on one line (#2460)

You can now write this: ``` record Person where constructor MkPerson name, surname, middleName : String ``` - which is equivalent to: ``` record Person where constructor MkPerson name : String surname : String middleName : String ``` I changed the parser a little and added a test for the new functionality.

commitf1e8a4dcc936ae5bc0951edea152f7a941e52489 authorBenjamin Hodgson <benjamin.hodgson@huddle.com> dateSun 26 Jul 2015, 16:16 (11 years ago) parentffb7946

5 files changed+43−17

compare with master

unifiedsplit

src/Idris/ParseData.hs+18−17 src/Idris/ParseHelpers.hs+5 test/records004/expected+3 test/records004/records004.idr+13 test/records004/run+4

src/Idris/ParseData.hs+18−17

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

8686

8787 let constructorDoc' = annotate syn ist constructorDoc

8888

89− fields <- many . indented $ field syn

89+ fields <- many . indented $ fieldLine syn

9090

91− return (fields, constructorName, constructorDoc')

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

9292 where

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

94− field syn = do doc <- optional docComment

95− c <- optional $ lchar '{'

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

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

98− <|> (do symbol "_"

99− return Nothing)

100− lchar ':'

101− t <- typeExpr (allowImp syn)

102− p <- endPlicity c

103− ist <- get

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

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

106− Nothing -> Nothing

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

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

94+ fieldLine syn = do

95+ doc <- optional docComment

96+ c <- optional $ lchar '{'

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

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

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

100+ ns <- commaSeparated oneName

101+ lchar ':'

102+ t <- typeExpr (allowImp syn)

103+ p <- endPlicity c

104+ ist <- get

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

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

107+ Nothing -> Nothing

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

108109

109110 constructor :: IdrisParser (Name, FC)

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

src/Idris/ParseHelpers.hs+5

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

434434bindList b [] sc = sc

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

436436

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+

437442{- * Layout helpers -}

438443

439444-- | 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

3+record Person where

4+ constructor MkPerson

5+ firstName, middleName, lastName : String

7+fred : Person

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

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