Docs for new record syntax

docs/reference/documenting.rst

@@ -127,9 +127,9 @@ italics correctly). A comprehensive set of examples is given below.
       ||| @ rest the remaining work
       Later : (rest : Partial a) -> Partial a
 
-    ||| We can document records just like normal data
+    ||| We can document records, including their fields and constructors
-    record Yummy : Type where
+    record Yummy where
-
       ||| Make a yummy
-      ||| @ food what to eat
+      constructor MkYummy
-      MkYummy : (food : String) -> Yummy
+      ||| What to eat
+      food : String

docs/reference/ffi.rst

@@ -70,21 +70,22 @@ call:
 
 .. code-block:: idris
 
-    record FFI : Type where
+    record FFI where
-         MkFFI : (ffi_types : Type -> Type) ->
+         constructor MkFFI
-                 (ffi_fn : Type) -> FFI
+         ffi_types : Type -> Type
+         ffi_fn : Type
 
 For C, this is:
 
 .. code-block:: idris
 
-    -- Supported C integer types
+    ||| Supported C integer types
     data C_IntTypes : Type -> Type where
          C_IntChar   : C_IntTypes Char
          C_IntNative : C_IntTypes Int
          ... -- more integer types
 
-    -- Supported C foreign types
+    ||| Supported C foreign types
     data C_Types : Type -> Type where
          C_Str   : C_Types String
          C_Float : C_Types Float

docs/tutorial/typesfuns.rst

@@ -979,18 +979,19 @@ example, we can represent a person's name and age in a record:
 
 .. code-block:: idris
 
-    record Person : Type where
+    record Person where
-        MkPerson : (name : String) ->
+        constructor MkPerson
-                   (age : Int) -> Person
+        name : String
+        age : Int
 
     fred : Person
     fred = MkPerson "Fred" 30
 
-Record declarations are like ``data`` declarations, except that they
+Records can have *parameters*, which are listed between the record
-are introduced by the ``record`` keyword, and can only have one
+name and the ``where`` keyword, and *fields*, which are in an indented
-constructor.  The names of the binders in the constructor type
+block following the `where` keyword (here, ``name`` and ``age``). The
-(``name`` and ``age``) here are the field names, which we can use to
+constructor name is provided after the ``constructor`` keyword. The
-access the field values:
+field names can be used to access the field values:
 
 ::
 
@@ -1002,7 +1003,8 @@ access the field values:
     name : Person -> String
 
 We can also use the field names to update a record (or, more
-precisely, produce a new record with the given fields updated).
+precisely, produce a copy of the record with the given fields
+updated):
 
 .. code-block:: bash
 
@@ -1016,15 +1018,14 @@ updates the given fields in a record.
 
 Records, and fields within records, can have dependent types. Updates
 are allowed to change the type of a field, provided that the result is
-well-typed, and the result does not affect the type of the record as a
+well-typed.
-whole. For example:
 
 .. code-block:: idris
 
-    record Class : Type where
+    record Class where
-        ClassInfo : (students : Vect n Person) ->
+        constructor ClassInfo
-                    (className : String) ->
+        students : Vect n Person
-                    Class
+        className : String
 
 It is safe to update the ``students`` field to a vector of a different
 length 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:
 ::
 
     *record> addStudent fred (ClassInfo [] "CS")
-    ClassInfo (prelude.vect.:: (MkPerson "Fred" 30) (prelude.vect.Nil)) "CS"
+    ClassInfo [MkPerson "Fred" 30] "CS" : Class
-      : Class
 
 Nested record update
 --------------------
@@ -1060,3 +1060,32 @@ can also be accessed with the following syntax:
 .. code-block:: idris
 
     record { a->b->c } x
+
+Parameters and Fields
+---------------------
+
+Records can have *parameters*, which are not subject to field
+updates. The parameters appear as arguments to the resulting type, and
+are written following the record type name. For example, a pair type
+could be defined as follows:
+
+.. code-block:: idris
+
+    record Prod a b where
+        constructor Times
+        fst : a
+        snd : b
+
+The parameters to a record type need not be types. For example, we can
+restrict the size of classes using a ``Nat`` parameter to the
+``Class`` record:
+
+.. code-block:: idris
+
+    record SizedClass (size : Nat) where
+        constructor SizedClassInfo
+        students : Vect size Person
+        className : String
+
+Note that it is no longer possible to write ``addStudent`` for this
+type, as that would change the size of the class.

src/Idris/Elab/Record.hs

@@ -32,8 +32,9 @@ import Data.Maybe
 import Data.List
 import Control.Monad
 
+-- | Elaborate a record declaration
 elabRecord ::  ElabInfo ->
-              (Docstring (Either Err PTerm)) ->
+              (Docstring (Either Err PTerm)) -> -- ^ The documentation for the whole declaration
               SyntaxInfo ->
               FC ->
               DataOpts ->