Update docs and tests.

docs/source/reference/records.rst

@@ -10,8 +10,7 @@ tighter than function application.
 Lexical structure
 -----------------
 
-* ``.foo`` is a valid name, which stands for record fields (new ``Name``
-  constructor ``RF "foo"``)
+* ``.foo`` is a valid lexeme, which stands for postfix application of ``foo``
 
 * ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced
   identifier: ``DotSepIdent ["baz", "bar", "Foo"]``
@@ -32,14 +31,11 @@ Expressions binding tighter than application (``simpleExpr``), such as variables
 
 .. code-block:: idris
 
-    simpleExpr ::= (.field)+               -- parses as PRecordProjection
-                 | simplerExpr (.field)+   -- parses as PRecordFieldAccess
+    simpleExpr ::= (.field)+               -- parses as PPostfixAppPartial
+                 | simplerExpr (.field)+   -- parses as PPostfixApp
                  | simplerExpr             -- (parses as whatever it used to)
 
-* ``(.foo)`` is a name, so you can use it to e.g. define a function called
-  ``.foo`` (see ``.squared`` below)
-
-* ``(.foo.bar)`` is a parenthesised expression
+* ``(.foo.bar)`` is a valid parenthesised expression
 
 Desugaring rules
 ----------------
@@ -50,19 +46,6 @@ Desugaring rules
 * ``(simpleExpr .field1 .field2 .field3)`` desugars to ``((.field .field2
   .field3) simpleExpr)``
 
-Record elaboration
-------------------
-
-* there is a new pragma ``%undotted_record_projections``, which is ``on`` by
-  default
-
-* for every field ``f`` of a record ``R``, we get:
-
-  * projection ``f`` in namespace ``R`` (exactly like now), unless
-    ``%undotted_record_projections`` is ``off``
-
-  * projection ``.f`` in namespace ``R`` with the same definition
-
 Example code
 ------------
 
@@ -74,33 +57,18 @@ Example code
       y : Double
 
 This record creates two projections:
-* ``.x : Point -> Double``
-* ``.y : Point -> Double``
-
-Because ``%undotted_record_projections`` are ``on`` by default, we also get:
 * ``x : Point -> Double``
 * ``y : Point -> Double``
 
-To prevent cluttering the ordinary global name space with short identifiers, we can do this:
+We add another record:
 
 .. code-block:: idris
 
-    %undotted_record_projections off
-
     record Rect where
       constructor MkRect
       topLeft : Point
       bottomRight : Point
 
-For ``Rect``, we don't get the undotted projections:
-
-.. code-block:: idris
-
-    Main> :t topLeft
-    (interactive):1:4--1:11:Undefined name topLeft
-    Main> :t .topLeft
-    \{rec:0} => .topLeft rec : ?_ -> Point
-
 Let's define some constants:
 
 .. code-block:: idris
@@ -114,20 +82,13 @@ Let's define some constants:
         (MkPoint 1.1 2.5)
         (MkPoint 4.3 6.3)
 
-User-defined projections work, too. (Should they?)
-
-.. code-block:: idris
-
-    (.squared) : Double -> Double
-    (.squared) x = x * x
-
 Finally, the examples:
 
 .. code-block:: idris
 
     main : IO ()
     main = do
-      -- desugars to (.x pt)
+      -- desugars to (x pt)
       -- prints 4.2
       printLn $ pt.x
 
@@ -153,7 +114,7 @@ Finally, the examples:
       -- prints [1.0, 3.0]
       printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
 
-      -- .topLeft.y desugars to (\x => .y (.topLeft x))
+      -- .topLeft.y desugars to (\x => y (topLeft x))
       -- prints [2.5, 2.5]
       printLn $ map (.topLeft.y) [rect, rect]
 

docs/source/tutorial/typesfuns.rst

@@ -1002,12 +1002,6 @@ We can use prefix field projections, like in Haskell:
     *Record> :t firstName
     firstName : Person -> String
 
-Prefix field projections can be disabled per record definition
-using pragma ``%undotted_record_projections off``, which makes
-all subsequently defined records generate only dotted projections.
-This pragma has effect until the end of the module
-or until the closest occurrence of ``%undotted_record_projections on``.
-
 We can also use the field names to update a record (or, more
 precisely, produce a copy of the record with the given fields
 updated):

tests/idris2/record004/Main.idr

@@ -6,34 +6,14 @@ record Point where
   y : Double
 
 -- a record creates two projections:
---
--- .x : Point -> Double
--- .y : Point -> Double
---
--- because %undotted_record_projections are on by default, we also get:
---
 -- x : Point -> Double
 -- y : Point -> Double
 
--- to prevent cluttering the ordinary name space with short identifiers
-%undotted_record_projections off
-
 record Rect where
   constructor MkRect
   topLeft : Point
   bottomRight : Point
 
--- .topLeft : Rect -> Point
--- .bottomRight : Rect -> Point
---
--- For Rect, we don't get the undotted projections:
---
--- Main> :t topLeft
--- (interactive):1:4--1:11:Undefined name topLeft
--- Main> :t .topLeft
--- \{rec:0} => .topLeft rec : ?_ -> Point
-
-
 pt : Point
 pt = MkPoint 4.2 6.6
 
@@ -43,35 +23,8 @@ rect =
     (MkPoint 1.1 2.5)
     (MkPoint 4.3 6.3)
 
--- New lexical structure:
---
--- Foo.bar.baz with uppercase F is one lexeme: NSIdent ["baz", "bar", "Foo"]
+-- Foo.bar.baz with uppercase F is one lexeme: DotSepIdent ["baz", "bar", "Foo"]
 -- foo.bar.baz with lowercase f is three lexemes: foo, .bar, .baz
 -- .foo.bar.baz is three lexemes: .foo, .bar, .baz
 --
 -- If you want Constructor.field, you have to write (Constructor).field.
---
--- New syntax of simpleExpr:
---
--- Expressions binding tighter than application (simpleExpr),
--- such as variables or parenthesised expressions,
--- have been renamed to simplerExpr,
--- and an extra layer of syntax has been inserted.
--- 
---   simpleExpr ::= (.field)+               -- parses as PRecordProjection
---                | simplerExpr (.field)+   -- parses as PRecordFieldAccess
---                | simplerExpr             -- (parses as whatever it used to)
---
--- (.foo) is a name, so you can use it to e.g. define a function called .foo (see .squared below)
--- (.foo.bar) is a parenthesised expression
---
--- New desugaring rules
---
--- (.field1 .field2 .field3) desugars to (\x => .field3 (.field2 (.field1 x)))
--- (simpleExpr .field1 .field2 .field3) desugars to ((.field .field2 .field3) simpleExpr).
---
--- There are more details such as namespacing; see below.
-
--- user-defined projections work, too (should they?)
-(.squared) : Double -> Double
-(.squared) x = x * x

tests/idris2/record004/expected

@@ -4,7 +4,6 @@ Main> 4.2
 Main> 10.8
 Main> 4.2
 Main> 4.2
-Main> 17.64
 Main> [1.1, 4.2]
 Main> (interactive):1:1--1:4:When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point
 Mismatch between:
@@ -21,10 +20,6 @@ Main> 4.2
 Main> 4.2
 Main> 4.2
 Main> 4.2
-Main> 4.2
-Main> 4.2
-Main> 4.2
-Main> 4.2
 Main> 3.0
 Main> 2.1
 Main> 3.0

tests/idris2/record004/input

@@ -3,15 +3,10 @@ pt .x
 pt.x + pt.y
 (Main.pt).x
 (MkPoint pt.y pt.x).y
-pt.x.squared
 map (.x) [MkPoint 1.1 2.5, MkPoint 4.2 6.3]
 map .x [MkPoint 1 2, MkPoint 3 4]
 map (.topLeft.y) [rect, rect]
 rect.topLeft.x + rect.bottomRight.y
-Main.Point.(.x) pt
-Point.(.x) pt
-(.x) pt
-.x pt
 Main.Point.x pt
 Point.x pt
 (x) pt