From b46064f688885aad1160648807bc2a49c11e33af Mon Sep 17 00:00:00 2001 From: Matus Tejiscak Date: Sat, 20 Jun 2020 23:49:34 +0200 Subject: [PATCH] Update docs and tests. --- docs/source/reference/records.rst | 53 ++++-------------------------- docs/source/tutorial/typesfuns.rst | 6 ---- tests/idris2/record004/Main.idr | 49 +-------------------------- tests/idris2/record004/expected | 5 --- tests/idris2/record004/input | 5 --- 5 files changed, 8 insertions(+), 110 deletions(-) diff --git a/docs/source/reference/records.rst b/docs/source/reference/records.rst index 8c6799db5..f0cdd78fe 100644 --- a/docs/source/reference/records.rst +++ b/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] diff --git a/docs/source/tutorial/typesfuns.rst b/docs/source/tutorial/typesfuns.rst index a171b7d4b..2d47b8c7c 100644 --- a/docs/source/tutorial/typesfuns.rst +++ b/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): diff --git a/tests/idris2/record004/Main.idr b/tests/idris2/record004/Main.idr index c3585e2f6..9313a8ee1 100644 --- a/tests/idris2/record004/Main.idr +++ b/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 diff --git a/tests/idris2/record004/expected b/tests/idris2/record004/expected index ce5f3be6e..ff7f1d32a 100644 --- a/tests/idris2/record004/expected +++ b/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 diff --git a/tests/idris2/record004/input b/tests/idris2/record004/input index 7f88e92eb..5a00dfbc6 100644 --- a/tests/idris2/record004/input +++ b/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