git.iko.soy/Idris-dev
on master help sign in
Docs for new record syntax
0afd6f2David Raymond Christiansen
docs/reference/documenting.rst+5−5
compare with master
unifiedsplit
@@ -127,9 +127,9 @@ italics correctly). A comprehensive set of examples is given below.
127 ||| @ rest the remaining work
127 ||| @ rest the remaining work
128 Later : (rest : Partial a) -> Partial a
128 Later : (rest : Partial a) -> Partial a
129
129
130− ||| We can document records just like normal data
130+ ||| We can document records, including their fields and constructors
131− record Yummy : Type where
131+ record Yummy where
132−
133 ||| Make a yummy
132 ||| Make a yummy
133+ constructor MkYummy
134− ||| @ food what to eat
134+ ||| What to eat
135− MkYummy : (food : String) -> Yummy
135+ food : String
docs/reference/ffi.rst+6−5
@@ -70,21 +70,22 @@ call:
70
70
71.. code-block:: idris
71.. code-block:: idris
72
72
73− record FFI : Type where
73+ record FFI where
74+ constructor MkFFI
74− MkFFI : (ffi_types : Type -> Type) ->
75+ ffi_types : Type -> Type
75− (ffi_fn : Type) -> FFI
76+ ffi_fn : Type
76
77
77For C, this is:
78For C, this is:
78
79
79.. code-block:: idris
80.. code-block:: idris
80
81
81− -- Supported C integer types
82+ ||| Supported C integer types
82 data C_IntTypes : Type -> Type where
83 data C_IntTypes : Type -> Type where
83 C_IntChar : C_IntTypes Char
84 C_IntChar : C_IntTypes Char
84 C_IntNative : C_IntTypes Int
85 C_IntNative : C_IntTypes Int
85 ... -- more integer types
86 ... -- more integer types
86
87
87− -- Supported C foreign types
88+ ||| Supported C foreign types
88 data C_Types : Type -> Type where
89 data C_Types : Type -> Type where
89 C_Str : C_Types String
90 C_Str : C_Types String
90 C_Float : C_Types Float
91 C_Float : C_Types Float
docs/tutorial/typesfuns.rst+46−17
@@ -979,18 +979,19 @@ example, we can represent a person's name and age in a record:
979
979
980.. code-block:: idris
980.. code-block:: idris
981
981
982− record Person : Type where
982+ record Person where
983+ constructor MkPerson
983− MkPerson : (name : String) ->
984+ name : String
984− (age : Int) -> Person
985+ age : Int
985
986
986 fred : Person
987 fred : Person
987 fred = MkPerson "Fred" 30
988 fred = MkPerson "Fred" 30
988
989
989−Record declarations are like ``data`` declarations, except that they
990+Records can have *parameters*, which are listed between the record
990−are introduced by the ``record`` keyword, and can only have one
991+name and the ``where`` keyword, and *fields*, which are in an indented
991−constructor. The names of the binders in the constructor type
992+block following the `where` keyword (here, ``name`` and ``age``). The
992−(``name`` and ``age``) here are the field names, which we can use to
993+constructor name is provided after the ``constructor`` keyword. The
993−access the field values:
994+field names can be used to access the field values:
994
995
995::
996::
996
997
@@ -1002,7 +1003,8 @@ access the field values:
1002 name : Person -> String
1003 name : Person -> String
1003
1004
1004We can also use the field names to update a record (or, more
1005We can also use the field names to update a record (or, more
1005−precisely, produce a new record with the given fields updated).
1006+precisely, produce a copy of the record with the given fields
1007+updated):
1006
1008
1007.. code-block:: bash
1009.. code-block:: bash
1008
1010
@@ -1016,15 +1018,14 @@ updates the given fields in a record.
1016
1018
1017Records, and fields within records, can have dependent types. Updates
1019Records, and fields within records, can have dependent types. Updates
1018are allowed to change the type of a field, provided that the result is
1020are allowed to change the type of a field, provided that the result is
1019−well-typed, and the result does not affect the type of the record as a
1021+well-typed.
1020−whole. For example:
1021
1022
1022.. code-block:: idris
1023.. code-block:: idris
1023
1024
1024− record Class : Type where
1025+ record Class where
1026+ constructor ClassInfo
1025− ClassInfo : (students : Vect n Person) ->
1027+ students : Vect n Person
1026− (className : String) ->
1028+ className : String
1027− Class
1028
1029
1029It is safe to update the ``students`` field to a vector of a different
1030It is safe to update the ``students`` field to a vector of a different
1030length because it will not affect the type of the record:
1031length because it will not affect the type of the record:
@@ -1037,8 +1038,7 @@ length because it will not affect the type of the record:
1037::
1038::
1038
1039
1039 *record> addStudent fred (ClassInfo [] "CS")
1040 *record> addStudent fred (ClassInfo [] "CS")
1040− ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
1041+ ClassInfo [MkPerson "Fred" 30] "CS" : Class
1041− : Class
1042
1042
1043Nested record update
1043Nested record update
1044--------------------
1044--------------------
@@ -1060,3 +1060,32 @@ can also be accessed with the following syntax:
1060.. code-block:: idris
1060.. code-block:: idris
1061
1061
1062 record { a->b->c } x
1062 record { a->b->c } x
1063+
1064+Parameters and Fields
1065+---------------------
1066+
1067+Records can have *parameters*, which are not subject to field
1068+updates. The parameters appear as arguments to the resulting type, and
1069+are written following the record type name. For example, a pair type
1070+could be defined as follows:
1071+
1072+.. code-block:: idris
1073+
1074+ record Prod a b where
1075+ constructor Times
1076+ fst : a
1077+ snd : b
1078+
1079+The parameters to a record type need not be types. For example, we can
1080+restrict the size of classes using a ``Nat`` parameter to the
1081+``Class`` record:
1082+
1083+.. code-block:: idris
1084+
1085+ record SizedClass (size : Nat) where
1086+ constructor SizedClassInfo
1087+ students : Vect size Person
1088+ className : String
1089+
1090+Note that it is no longer possible to write ``addStudent`` for this
1091+type, as that would change the size of the class.
src/Idris/Elab/Record.hs+2−1
@@ -32,8 +32,9 @@ import Data.Maybe
32import Data.List
32import Data.List
33import Control.Monad
33import Control.Monad
34
34
35+-- | Elaborate a record declaration
35elabRecord :: ElabInfo ->
36elabRecord :: ElabInfo ->
36− (Docstring (Either Err PTerm)) ->
37+ (Docstring (Either Err PTerm)) -> -- ^ The documentation for the whole declaration
37 SyntaxInfo ->
38 SyntaxInfo ->
38 FC ->
39 FC ->
39 DataOpts ->
40 DataOpts ->