7fe42e0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2470 from benjamin-hodgson/2460_multipleFields

7fe42e0Niklas Larsson11 years ago

docs/tutorial/typesfuns.rst+17−15

compare with master

unifiedsplit

@@ -349,7 +349,7 @@ following:

349 $ idris vbroken.idr --check

350 vbroken.idr:9:23:When elaborating right hand side of Vect.++:

351 When elaborating an application of constructor Vect.:::

352− Type mismatch between

352+ Type mismatch between

353 Vect (k + k) a (Type of xs ++ xs)

354 and

355 Vect (plus k m) a (Expected type)

@@ -442,7 +442,7 @@ names, ``n`` and ``a``, which are not declared explicitly. These are

442Implicit arguments, given in braces ``{}`` in the type declaration,

443are not given in applications of ``index``; their values can be

444inferred from the types of the ``Fin n`` and ``Vect n a``

445−arguments. Any name beginning with a lower case letter which appears

445+arguments. Any name beginning with a lower case letter which appears

446as a parameter or index in a

447type declaration, but which is otherwise unbound, will be automatically

448bound as an implicit argument. Implicit arguments can still be given

@@ -1017,26 +1017,28 @@ example, we can represent a person's name and age in a record:

1017

1018 record Person where

1019 constructor MkPerson

1020− name : String

1020+ firstName, middleName, lastName : String

1021 age : Int

1022

1023 fred : Person

1024− fred = MkPerson "Fred" 30

1024+ fred = MkPerson "Fred" "Joe" "Bloggs" 30

1025

1026Records can have *parameters*, which are listed between the record

1027name and the ``where`` keyword, and *fields*, which are in an indented

1028−block following the `where` keyword (here, ``name`` and ``age``). The

1028+block following the `where` keyword (here, ``firstName``, ``middleName``,

1029+``lastName``, and ``age``). You can declare multiple fields on a single

1030+line, provided that they have the same type. The constructor name is

1029−constructor name is provided after the ``constructor`` keyword. The

1031+provided after the ``constructor`` keyword. The field names can be used to

1030−field names can be used to access the field values:

1032+access the field values:

1031

1033

1032::

1034::

1033

1035

1034− *record> name fred

1036+ *record> firstName fred

1035 "Fred" : String

1037 "Fred" : String

1036 *record> age fred

1038 *record> age fred

1037 30 : Int

1039 30 : Int

1038− *record> :t name

1040+ *record> :t firstName

1039− name : Person -> String

1041+ firstName : Person -> String

1040

1042

1041We can also use the field names to update a record (or, more

1043We can also use the field names to update a record (or, more

1042precisely, produce a copy of the record with the given fields

1044precisely, produce a copy of the record with the given fields

@@ -1044,10 +1046,10 @@ updated):

1044

1046

1045.. code-block:: bash

1047.. code-block:: bash

1046

1048

1047− *record> record { name = "Jim" } fred

1049+ *record> record { firstName = "Jim" } fred

1048− MkPerson "Jim" 30 : Person

1050+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person

1049− *record> record { name = "Jim", age = 20 } fred

1051+ *record> record { firstName = "Jim", age = 20 } fred

1050− MkPerson "Jim" 20 : Person

1052+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person

1051

1053

1052The syntax ``record { field = val, ... }`` generates a function which

1054The syntax ``record { field = val, ... }`` generates a function which

1053updates the given fields in a record.

1055updates the given fields in a record.

@@ -1074,7 +1076,7 @@ length because it will not affect the type of the record:

1074::

1076::

1075

1077

1076 *record> addStudent fred (ClassInfo [] "CS")

1078 *record> addStudent fred (ClassInfo [] "CS")

1077− ClassInfo [MkPerson "Fred" 30] "CS" : Class

1079+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class

1078

1080

1079Nested record update

1081Nested record update

1080--------------------

1082--------------------

src/Idris/ParseData.hs+18−17

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

87 let constructorDoc' = annotate syn ist constructorDoc

89− fields <- many . indented $ field syn

89+ fields <- many . indented $ fieldLine syn

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

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