git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2470 from benjamin-hodgson/2460_multipleFields

Multiple record fields on one line (#2460)

commit7fe42e06de633d40773cc1f94b333e485d052eb6 authorNiklas Larsson <metaniklas@gmail.com> dateThu 30 Jul 2015, 00:26 (11 years ago) parentaf79c58f25976d
6 files changed+60−32
compare with master
unifiedsplit
docs/tutorial/typesfuns.rst+17−15 src/Idris/ParseData.hs+18−17 src/Idris/ParseHelpers.hs+5 test/records004/expected+3 test/records004/records004.idr+13 test/records004/run+4
docs/tutorial/typesfuns.rst+17−15
@@ -349,7 +349,7 @@ following:
349349 $ idris vbroken.idr --check
350350 vbroken.idr:9:23:When elaborating right hand side of Vect.++:
351351 When elaborating an application of constructor Vect.:::
352− Type mismatch between
352+ Type mismatch between
353353 Vect (k + k) a (Type of xs ++ xs)
354354 and
355355 Vect (plus k m) a (Expected type)
@@ -442,7 +442,7 @@ names, ``n`` and ``a``, which are not declared explicitly. These are
442442Implicit arguments, given in braces ``{}`` in the type declaration,
443443are not given in applications of ``index``; their values can be
444444inferred 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
446446as a parameter or index in a
447447type declaration, but which is otherwise unbound, will be automatically
448448bound 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:
10171017
10181018 record Person where
10191019 constructor MkPerson
1020− name : String
1020+ firstName, middleName, lastName : String
10211021 age : Int
10221022
10231023 fred : Person
1024− fred = MkPerson "Fred" 30
1024+ fred = MkPerson "Fred" "Joe" "Bloggs" 30
10251025
10261026Records can have *parameters*, which are listed between the record
10271027name and the ``where`` keyword, and *fields*, which are in an indented
1028−block following the `where` keyword (here, ``name`` and ``age``). The
1029−constructor name is provided after the ``constructor`` keyword. The
1030−field names can be used to access the field values:
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
1031+provided after the ``constructor`` keyword. The field names can be used to
1032+access the field values:
10311033
10321034::
10331035
1034− *record> name fred
1036+ *record> firstName fred
10351037 "Fred" : String
10361038 *record> age fred
10371039 30 : Int
1038− *record> :t name
1039− name : Person -> String
1040+ *record> :t firstName
1041+ firstName : Person -> String
10401042
10411043We can also use the field names to update a record (or, more
10421044precisely, produce a copy of the record with the given fields
@@ -1044,10 +1046,10 @@ updated):
10441046
10451047.. code-block:: bash
10461048
1047− *record> record { name = "Jim" } fred
1048− MkPerson "Jim" 30 : Person
1049− *record> record { name = "Jim", age = 20 } fred
1050− MkPerson "Jim" 20 : Person
1049+ *record> record { firstName = "Jim" } fred
1050+ MkPerson "Jim" "Joe" "Bloggs" 30 : Person
1051+ *record> record { firstName = "Jim", age = 20 } fred
1052+ MkPerson "Jim" "Joe" "Bloggs" 20 : Person
10511053
10521054The syntax ``record { field = val, ... }`` generates a function which
10531055updates the given fields in a record.
@@ -1074,7 +1076,7 @@ length because it will not affect the type of the record:
10741076::
10751077
10761078 *record> addStudent fred (ClassInfo [] "CS")
1077− ClassInfo [MkPerson "Fred" 30] "CS" : Class
1079+ ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
10781080
10791081Nested record update
10801082--------------------
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
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