Merge branch 'revert-projections' into master

docs/source/reference/index.rst

@@ -18,6 +18,6 @@ This is a placeholder, to get set up with readthedocs.
 
    packages
    envvars
-   postfixprojs
+   records
    literate
    overloadedlit

docs/source/reference/postfixprojs.rst

@@ -1,196 +0,0 @@
-Postfix projections
-===================
-
-.. role:: idris(code)
-    :language: idris
-
-Postfix projections are syntactic forms that represent postfix application,
-such as ``person.name``. They were originally motivated by the need of dot syntax
-to access fields of records, and generalised also for non-record use cases later.
-
-The more advanced features require ``%language PostfixProjections``,
-at least until it's clear whether they should be present in the language.
-
-Lexical structure
------------------
-
-* ``.foo`` starting with lowercase ``f``, single identifier, and no space after dot,
-  is a valid lexeme, which stands for postfix application of ``foo``
-
-* ``Foo.Bar.baz`` with uppercase ``F`` and ``B`` is one lexeme: a namespaced
-  identifier.
-
-* ``Foo.Bar.baz.boo`` is two lexemes: ``Foo.Bar.baz`` and ``.boo``.
-
-* ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``,
-  ``.bar``, ``.baz``
-
-* ``.foo.bar.baz`` is three lexemes: ``.foo``, ``.bar``, ``.baz``
-
-* ``foo . bar``, as well as ``foo. bar`` is three lexemes: ``foo``, ``.``, ``bar``,
-  and represents function composition as usual
-
-* Beware that ``True.not`` is lexed as "name ``not`` in module ``True``".
-  If you want the postfix application of ``not`` to constructor ``True``,
-  you have to write ``(True).not``.
-
-* Spaces *before* dots are optional; spaces *after* dots are forbidden
-  in postfix projections: ``foo. bar`` is parsed as function composition.
-
-* All module names must start with an uppercase letter.
-
-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 postfix dot syntax has been inserted in ``simpleExpr``.
-
-.. code-block:: idris
-
-    postfixProj ::= .ident        -- identifiers need not be bracketed
-                  | .(expr)       -- arbitrary expression in brackets
-
-    simpleExpr ::= simplerExpr postfixProj+   -- postfix projection
-                 | (postfixProj+ simpleExpr+) -- section of postfix projection
-                 | simplerExpr                -- (parses as whatever it used to)
-
-Desugaring rules
-----------------
-
-* Postfix projections:
-  ``simpleExpr .proj1 .proj2 .proj3`` desugars to ``(proj3 (proj2 (proj1 simpleExpr))``
-
-* Sections of postfix projections:
-  ``(.proj1 .proj2 .proj3 arg1 arg2)`` desugars to ``(\x => x.proj1.proj2.proj3 arg1 arg2)``
-
-Examples of desugaring:
-
-* ``foo.bar`` desugars as ``bar foo``
-* ``True.not`` is a single lexeme: qualified name
-* ``(True).not`` desugars as ``not True``
-* ``(True).(not . not)`` desugars as ``(not . not) True``
-* ``(not True).(not . not)`` desugars as ``(not . not) (not True)``
-* ``(checkFile fileName).runState initialState`` desugars as ``runState (checkFile fileName) initialState``
-* ``(MkPoint 3 4).x`` desugars as ``x (MkPoint 3 4)``
-
-Examples of desugaring sections:
-
-* bare ``.foo`` is invalid syntax (e.g. in ``f $ .foo``)
-* ``(.foo)`` desugars as ``(\x => x.foo)``, i.e. ``(\x => foo x)``
-* ``(.foo.bar m n)`` desugars as ``(\x => bar (foo x) m n)``
-
-Example code
-------------
-
-.. code-block:: idris
-
-    record Point where
-      constructor MkPoint
-      x : Double
-      y : Double
-
-This record creates two projections:
-
-* ``x : Point -> Double``
-* ``y : Point -> Double``
-
-We add another record:
-
-.. code-block:: idris
-
-    record Rect where
-      constructor MkRect
-      topLeft : Point
-      bottomRight : Point
-
-Let's define some constants:
-
-.. code-block:: idris
-
-    pt : Point
-    pt = MkPoint 4.2 6.6
-
-    rect : Rect
-    rect =
-      MkRect
-        (MkPoint 1.1 2.5)
-        (MkPoint 4.3 6.3)
-
-    squared : Num a => a -> a
-    squared x = x * x
-
-Finally, some examples:
-
-.. code-block:: idris
-
-    main : IO ()
-    main = do
-      -- desugars to (x pt)
-      -- prints 4.2
-      printLn $ pt.x
-
-      -- prints 4.2, too
-      -- maybe we want to make this a parse error?
-      printLn $ pt .x
-
-      -- prints 10.8
-      printLn $ pt.x + pt.y
-
-      -- works fine with namespacing
-      -- both print 4.2
-      printLn $ Main.pt.x
-      printLn $ (Main.pt).x
-
-      -- the LHS can be an arbitrary expression
-      -- prints 4.2
-      printLn $ (MkPoint pt.y pt.x).y
-
-      -- the RHS can be an arbitrary expression, too
-      -- prints 17.64
-      printLn $ (MkPoint pt.y pt.x).(squared . y)
-
-      -- user-defined function
-      -- prints 17.64
-      printLn $ pt.x.squared
-
-      -- prints [1.0, 3.0]
-      printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
-
-      -- .topLeft.y desugars to (\x => y (topLeft x))
-      -- prints [2.5, 2.5]
-      printLn $ map (.topLeft.y) [rect, rect]
-
-      -- desugars to (.topLeft.x rect + .bottomRight.y rect)
-      -- prints 7.4
-      printLn $ rect.topLeft.x + rect.bottomRight.y
-
-      -- complex projections
-      -- prints 7.4
-      printLn $ rect.(x . topLeft) + rect.(y . bottomRight)
-
-      -- haskell-style projections
-      printLn $ Main.Point.x pt
-      printLn $ Point.x pt
-      printLn $ (x) pt
-      printLn $ x pt
-
-      -- record update syntax uses dots now
-      -- prints 3.0
-      printLn $ (record { topLeft.x = 3 } rect).topLeft.x
-
-      -- but for compatibility, we support the old syntax, too
-      printLn $ (record { topLeft->x = 3 } rect).topLeft.x
-
-      -- prints 2.1
-      printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
-      printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
-
-Parses but does not typecheck:
-
-.. code-block:: idris
-
-  -- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
-  -- maybe we should disallow spaces before dots?
-  --
-  printLn $ map .x [MkPoint 1 2, MkPoint 3 4]

docs/source/reference/records.rst

@@ -0,0 +1,195 @@
+Dot syntax for records
+======================
+
+.. role:: idris(code)
+    :language: idris
+
+Long story short, ``.field`` is a postfix projection operator that binds
+tighter than function application.
+
+Lexical structure
+-----------------
+
+* ``.foo`` is a valid name, which stands for record fields (new ``Name``
+  constructor ``RF "foo"``)
+
+* ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced
+  identifier: ``DotSepIdent ["baz", "bar", "Foo"]``
+
+* ``foo.bar.baz`` starting 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``.
+
+* All module names must start with an uppercase letter.
+
+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.
+
+.. code-block:: idris
+
+    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
+
+Desugaring rules
+----------------
+
+* ``(.field1 .field2 .field3)`` desugars to ``(\x => .field3 (.field2 (.field1
+  x)))``
+
+* ``(simpleExpr .field1 .field2 .field3)`` desugars to ``((.field .field2
+  .field3) simpleExpr)``
+
+Record elaboration
+------------------
+
+* there is a new pragma ``%prefix_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
+    ``%prefix_record_projections`` is ``off``
+
+  * projection ``.f`` in namespace ``R`` with the same definition
+
+Example code
+------------
+
+.. code-block:: idris
+
+    record Point where
+      constructor MkPoint
+      x : Double
+      y : Double
+
+This record creates two projections:
+* ``.x : Point -> Double``
+* ``.y : Point -> Double``
+
+Because ``%prefix_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:
+
+.. code-block:: idris
+
+    %prefix_record_projections off
+
+    record Rect where
+      constructor MkRect
+      topLeft : Point
+      bottomRight : Point
+
+For ``Rect``, we don't get the prefix 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
+
+    pt : Point
+    pt = MkPoint 4.2 6.6
+
+    rect : Rect
+    rect =
+      MkRect
+        (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)
+      -- prints 4.2
+      printLn $ pt.x
+
+      -- prints 4.2, too
+      -- maybe we want to make this a parse error?
+      printLn $ pt .x
+
+      -- prints 10.8
+      printLn $ pt.x + pt.y
+
+      -- works fine with namespacing
+      -- prints 4.2
+      printLn $ (Main.pt).x
+
+      -- the LHS can be an arbitrary expression
+      -- prints 4.2
+      printLn $ (MkPoint pt.y pt.x).y
+
+      -- user-defined projection
+      -- prints 17.64
+      printLn $ pt.x.squared
+
+      -- prints [1.0, 3.0]
+      printLn $ map (.x) [MkPoint 1 2, MkPoint 3 4]
+
+      -- .topLeft.y desugars to (\x => .y (.topLeft x))
+      -- prints [2.5, 2.5]
+      printLn $ map (.topLeft.y) [rect, rect]
+
+      -- desugars to (.topLeft.x rect + .bottomRight.y rect)
+      -- prints 7.4
+      printLn $ rect.topLeft.x + rect.bottomRight.y
+
+      -- qualified names work, too
+      -- all these print 4.2
+      printLn $ Main.Point.(.x) pt
+      printLn $ Point.(.x) pt
+      printLn $ (.x) pt
+      printLn $ .x pt
+
+      -- haskell-style projections work, too
+      printLn $ Main.Point.x pt
+      printLn $ Point.x pt
+      printLn $ (x) pt
+      printLn $ x pt
+
+      -- record update syntax uses dots now
+      -- prints 3.0
+      printLn $ (record { topLeft.x = 3 } rect).topLeft.x
+
+      -- but for compatibility, we support the old syntax, too
+      printLn $ (record { topLeft->x = 3 } rect).topLeft.x
+
+      -- prints 2.1
+      printLn $ (record { topLeft.x $= (+1) } rect).topLeft.x
+      printLn $ (record { topLeft->x $= (+1) } rect).topLeft.x
+
+Parses but does not typecheck:
+
+.. code-block:: idris
+
+  -- parses as: map.x [MkPoint 1 2, MkPoint 3 4]
+  -- maybe we should disallow spaces before dots?
+  --
+  printLn $ map .x [MkPoint 1 2, MkPoint 3 4]

docs/source/tutorial/typesfuns.rst

@@ -988,8 +988,8 @@ type. The field names can be used to access the field values:
     "Fred" : String
     *Record> fred.age
     30 : Int
-    *Record> :t firstName
+    *Record> :t (.firstName)
-    firstName : Person -> String
+    Main.Person.(.firstName) : Person -> String
 
 We can use prefix field projections, like in Haskell:
 
@@ -999,6 +999,14 @@ We can use prefix field projections, like in Haskell:
     "Fred" : String
     *Record> age fred
     30 : Int
+    *Record> :t firstName
+    firstName : Person -> String
+
+Prefix field projections can be disabled per record definition
+using pragma ``%prefix_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 ``%prefix_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

libs/base/Language/Reflection/TT.idr

@@ -64,6 +64,7 @@ data Name = UN String -- user defined name
           | MN String Int -- machine generated name
           | NS Namespace Name -- name in a namespace
           | DN String Name -- a name and how to display it
+          | RF String -- record field name
 
 export
 Show Name where
@@ -71,6 +72,7 @@ Show Name where
   show (UN x) = x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (DN str y) = str
+  show (RF n) = "." ++ n
 
 public export
 data Count = M0 | M1 | MW

src/Compiler/ES/ES.idr

@@ -92,6 +92,7 @@ jsName (UN n) = keywordSafe $ jsIdent n
 jsName (MN n i) = jsIdent n ++ "_" ++ show i
 jsName (PV n d) = "pat__" ++ jsName n
 jsName (DN _ n) = jsName n
+jsName (RF n) = "rf__" ++ jsIdent n
 jsName (Nested (i, x) n) = "n__" ++ show i ++ "_" ++ show x ++ "_" ++ jsName n
 jsName (CaseBlock x y) = "case__" ++ jsIdent x ++ "_" ++ show y
 jsName (WithBlock x y) = "with__" ++ jsIdent x ++ "_" ++ show y

src/Compiler/Scheme/Common.idr

@@ -36,6 +36,7 @@ schName (UN n) = schString n
 schName (MN n i) = schString n ++ "-" ++ show i
 schName (PV n d) = "pat--" ++ schName n
 schName (DN _ n) = schName n
+schName (RF n) = "rf--" ++ schString n
 schName (Nested (i, x) n) = "n--" ++ show i ++ "-" ++ show x ++ "-" ++ schName n
 schName (CaseBlock x y) = "case--" ++ schString x ++ "-" ++ show y
 schName (WithBlock x y) = "with--" ++ schString x ++ "-" ++ show y

src/Core/Binary.idr

@@ -31,7 +31,7 @@ import Data.Buffer
 -- TTC files can only be compatible if the version number is the same
 export
 ttcVersion : Int
-ttcVersion = 41
+ttcVersion = 42
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Context.idr

@@ -361,7 +361,7 @@ initCtxtS : Int -> Core Context
 initCtxtS s
     = do arr <- coreLift $ newArray s
          aref <- newRef Arr arr
-         pure (MkContext 0 0 empty empty aref 0 empty [partialEvalNS] False False empty)
+         pure $ MkContext 0 0 empty empty aref 0 empty [partialEvalNS] False False empty
 
 export
 initCtxt : Core Context
@@ -1299,6 +1299,8 @@ visibleInAny nss n vis = any (\ns => visibleIn ns n vis) nss
 reducibleIn : Namespace -> Name -> Visibility -> Bool
 reducibleIn nspace (NS ns (UN n)) Export = isParentOf ns nspace
 reducibleIn nspace (NS ns (UN n)) Private = isParentOf ns nspace
+reducibleIn nspace (NS ns (RF n)) Export = isParentOf ns nspace
+reducibleIn nspace (NS ns (RF n)) Private = isParentOf ns nspace
 reducibleIn nspace n _ = True
 
 export
@@ -1806,6 +1808,9 @@ inCurrentNS n@(MN _ _)
 inCurrentNS n@(DN _ _)
     = do defs <- get Ctxt
          pure (NS (currentNS defs) n)
+inCurrentNS n@(RF _)
+    = do defs <- get Ctxt
+         pure (NS (currentNS defs) n)
 inCurrentNS n = pure n
 
 export
@@ -2012,6 +2017,12 @@ setUnboundImplicits a
     = do defs <- get Ctxt
          put Ctxt (record { options->elabDirectives->unboundImplicits = a } defs)
 
+export
+setPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
+setPrefixRecordProjections b = do
+  defs <- get Ctxt
+  put Ctxt (record { options->elabDirectives->prefixRecordProjections = b } defs)
+
 export
 setDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
                            TotalReq -> Core ()
@@ -2047,6 +2058,11 @@ isUnboundImplicits
     = do defs <- get Ctxt
          pure (unboundImplicits (elabDirectives (options defs)))
 
+export
+isPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Core Bool
+isPrefixRecordProjections =
+  prefixRecordProjections . elabDirectives . options <$> get Ctxt
+
 export
 getDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
                            Core TotalReq

src/Core/Name.idr

@@ -19,6 +19,7 @@ data Name : Type where
      MN : String -> Int -> Name -- machine generated name
      PV : Name -> Int -> Name -- pattern variable name; int is the resolved function id
      DN : String -> Name -> Name -- a name and how to display it
+     RF : String -> Name  -- record field name
      Nested : (Int, Int) -> Name -> Name -- nested function name
      CaseBlock : String -> Int -> Name -- case block nested in (resolved) name
      WithBlock : String -> Int -> Name -- with block nested in (resolved) name
@@ -57,6 +58,7 @@ userNameRoot : Name -> Maybe String
 userNameRoot (NS _ n) = userNameRoot n
 userNameRoot (UN n) = Just n
 userNameRoot (DN _ n) = userNameRoot n
+userNameRoot (RF n) = Just ("." ++ n)  -- TMP HACK
 userNameRoot _ = Nothing
 
 export
@@ -74,6 +76,7 @@ nameRoot (UN n) = n
 nameRoot (MN n _) = n
 nameRoot (PV n _) = nameRoot n
 nameRoot (DN _ n) = nameRoot n
+nameRoot (RF n) = n
 nameRoot (Nested _ inner) = nameRoot inner
 nameRoot (CaseBlock n _) = "$" ++ show n
 nameRoot (WithBlock n _) = "$" ++ show n
@@ -93,11 +96,13 @@ dropAllNS n = n
 
 export
 Show Name where
+  show (NS ns n@(RF _)) = show ns ++ ".(" ++ show n ++ ")"
   show (NS ns n) = show ns ++ "." ++ show n
   show (UN x) = x
   show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
   show (PV n d) = "{P:" ++ show n ++ ":" ++ show d ++ "}"
   show (DN str n) = str
+  show (RF n) = "." ++ n
   show (Nested (outer, idx) inner)
       = show outer ++ ":" ++ show idx ++ ":" ++ show inner
   show (CaseBlock outer i) = "case block in " ++ outer
@@ -106,11 +111,13 @@ Show Name where
 
 export
 Pretty Name where
+  pretty (NS ns n@(RF _)) = pretty ns <+> dot <+> parens (pretty n)
   pretty (NS ns n) = pretty ns <+> dot <+> pretty n
   pretty (UN x) = pretty x
   pretty (MN x y) = braces (pretty x <+> colon <+> pretty y)
   pretty (PV n d) = braces (pretty 'P' <+> colon <+> pretty n <+> colon <+> pretty d)
   pretty (DN str _) = pretty str
+  pretty (RF n) = "." <+> pretty n
   pretty (Nested (outer, idx) inner) = pretty outer <+> colon <+> pretty idx <+> colon <+> pretty inner
   pretty (CaseBlock outer _) = reflow "case block in" <++> pretty outer
   pretty (WithBlock outer _) = reflow "with block in" <++> pretty outer
@@ -123,6 +130,7 @@ Eq Name where
     (==) (MN x y) (MN x' y') = y == y' && x == x'
     (==) (PV x y) (PV x' y') = x == x' && y == y'
     (==) (DN _ n) (DN _ n') = n == n'
+    (==) (RF n) (RF n') = n == n'
     (==) (Nested x y) (Nested x' y') = x == x' && y == y'
     (==) (CaseBlock x y) (CaseBlock x' y') = y == y' && x == x'
     (==) (WithBlock x y) (WithBlock x' y') = y == y' && x == x'
@@ -135,10 +143,11 @@ nameTag (UN _) = 1
 nameTag (MN _ _) = 2
 nameTag (PV _ _) = 3
 nameTag (DN _ _) = 4
-nameTag (Nested _ _) = 5
+nameTag (RF _) = 5
-nameTag (CaseBlock _ _) = 6
+nameTag (Nested _ _) = 6
-nameTag (WithBlock _ _) = 7
+nameTag (CaseBlock _ _) = 7
-nameTag (Resolved _) = 8
+nameTag (WithBlock _ _) = 8
+nameTag (Resolved _) = 9
 
 export
 Ord Name where
@@ -161,6 +170,7 @@ Ord Name where
                GT => GT
                LT => LT
     compare (DN _ n) (DN _ n') = compare n n'
+    compare (RF n) (RF n') = compare n n'
     compare (Nested x y) (Nested x' y')
         = case compare y y' of
                EQ => compare x x'
@@ -206,6 +216,9 @@ nameEq (DN x t) (DN y t') with (decEq x y)
     nameEq (DN y t) (DN y t) | (Yes Refl) | (Just Refl) = Just Refl
     nameEq (DN y t) (DN y t') | (Yes Refl) | Nothing = Nothing
   nameEq (DN x t) (DN y t') | (No p) = Nothing
+nameEq (RF x) (RF y) with (decEq x y)
+  nameEq (RF y) (RF y) | (Yes Refl) = Just Refl
+  nameEq (RF x) (RF y) | (No contra) = Nothing
 nameEq (Nested x y) (Nested x' y') with (decEq x x')
   nameEq (Nested x y) (Nested x' y') | (No p) = Nothing
   nameEq (Nested x y) (Nested x y') | (Yes Refl) with (nameEq y y')

src/Core/Options.idr

@@ -98,13 +98,11 @@ public export
 data LangExt
      = ElabReflection
      | Borrowing -- not yet implemented
-     | PostfixProjections
 
 export
 Eq LangExt where
   ElabReflection == ElabReflection = True
   Borrowing == Borrowing = True
-  PostfixProjections == PostfixProjections = True
   _ == _ = False
 
 -- Other options relevant to the current session (so not to be saved in a TTC)
@@ -116,6 +114,11 @@ record ElabDirectives where
   totality : TotalReq
   ambigLimit : Nat
   autoImplicitLimit : Nat
+  --
+  -- produce traditional (prefix) record projections,
+  -- in addition to postfix (dot) projections
+  -- default: yes
+  prefixRecordProjections : Bool
 
 public export
 record Session where
@@ -182,7 +185,7 @@ defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 50
+defaultElab = MkElabDirectives True True CoveringOnly 3 50 True
 
 export
 defaults : Options

src/Core/Reflect.idr

@@ -272,6 +272,9 @@ Reify Name where
                  => do str' <- reify defs !(evalClosure defs str)
                        n' <- reify defs !(evalClosure defs n)
                        pure (DN str' n')
+             (NS _ (UN "RF"), [str])
+                 => do str' <- reify defs !(evalClosure defs str)
+                       pure (RF str')
              _ => cantReify val "Name"
   reify defs val = cantReify val "Name"
 
@@ -292,6 +295,9 @@ Reflect Name where
       = do str' <- reflect fc defs lhs env str
            n' <- reflect fc defs lhs env n
            appCon fc defs (reflectiontt "DN") [str', n']
+  reflect fc defs lhs env (RF x)
+      = do x' <- reflect fc defs lhs env x
+           appCon fc defs (reflectiontt "RF") [x']
   reflect fc defs lhs env (Resolved i)
       = case !(full (gamma defs) (Resolved i)) of
              Resolved _ => cantReflect fc "Name"

src/Core/TTC.idr

@@ -47,9 +47,10 @@ TTC Name where
   toBuf b (MN x y) = do tag 2; toBuf b x; toBuf b y
   toBuf b (PV x y) = do tag 3; toBuf b x; toBuf b y
   toBuf b (DN x y) = do tag 4; toBuf b x; toBuf b y
-  toBuf b (Nested x y) = do tag 5; toBuf b x; toBuf b y
+  toBuf b (RF x) = do tag 5; toBuf b x
-  toBuf b (CaseBlock x y) = do tag 6; toBuf b x; toBuf b y
+  toBuf b (Nested x y) = do tag 6; toBuf b x; toBuf b y
-  toBuf b (WithBlock x y) = do tag 7; toBuf b x; toBuf b y
+  toBuf b (CaseBlock x y) = do tag 7; toBuf b x; toBuf b y
+  toBuf b (WithBlock x y) = do tag 8; toBuf b x; toBuf b y
   toBuf b (Resolved x)
       = throw (InternalError ("Can't write resolved name " ++ show x))
 
@@ -70,12 +71,14 @@ TTC Name where
                      y <- fromBuf b
                      pure (DN x y)
              5 => do x <- fromBuf b
-                     y <- fromBuf b
+                     pure (RF x)
-                     pure (Nested x y)
              6 => do x <- fromBuf b
                      y <- fromBuf b
-                     pure (CaseBlock x y)
+                     pure (Nested x y)
              7 => do x <- fromBuf b
+                     y <- fromBuf b
+                     pure (CaseBlock x y)
+             8 => do x <- fromBuf b
                      y <- fromBuf b
                      pure (WithBlock x y)
              _ => corrupt "Name"

src/Core/UnifyState.idr

@@ -125,6 +125,7 @@ genMVName : {auto c : Ref Ctxt Defs} ->
             Name -> Core Name
 genMVName (UN str) = genName str
 genMVName (MN str _) = genName str
+genMVName (RF str) = genName str
 genMVName n
     = do ust <- get UST
          put UST (record { nextName $= (+1) } ust)

src/Idris/Desugar.idr

@@ -351,43 +351,12 @@ mutual
                 desugarB side ps (PApp fc (PApp fc (PRef fc (UN "rangeFromThen")) start) n)
   desugarB side ps (PUnifyLog fc lvl tm)
       = pure $ IUnifyLog fc lvl !(desugarB side ps tm)
-
+  desugarB side ps (PPostfixApp fc rec projs)
-  desugarB side ps (PPostfixProjs fc rec projs)
+      = desugarB side ps $ foldl (\x, proj => PApp fc (PRef fc proj) x) rec projs
-      = do
+  desugarB side ps (PPostfixAppPartial fc projs)
-        let isPRef = \case
+      = desugarB side ps $
-              PRef _ _ => True
-              _ => False
-        defs <- get Ctxt
-        when (not (isExtension PostfixProjections defs) && not (all isPRef projs)) $
-          throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")
-
-        desugarB side ps $ foldl (\x, proj => PApp fc proj x) rec projs
-
-  desugarB side ps (PPostfixProjsSection fc projs args)
-      = do
-        let isPRef = \case
-              PRef _ _ => True
-              _ => False
-        defs <- get Ctxt
-
-        when (not (isExtension PostfixProjections defs)) $ do
-          when (not (all isPRef projs)) $
-            throw (GenericMsg fc "complex postfix projections require %language PostfixProjections")
-
-          case args of
-            [] => pure ()
-            _  => throw $ GenericMsg fc "postfix projection sections require %language PostfixProjections"
-
-        desugarB side ps $
           PLam fc top Explicit (PRef fc (MN "paRoot" 0)) (PImplicit fc) $
-            foldl
+            foldl (\r, proj => PApp fc (PRef fc proj) r) (PRef fc (MN "paRoot" 0)) projs
-              (\r, arg => PApp fc r arg)
-              (foldl
-                (\r, proj => PApp fc proj r)
-                (PRef fc (MN "paRoot" 0))
-                projs)
-              args
-
   desugarB side ps (PWithUnambigNames fc ns rhs)
       = IWithUnambigNames fc ns <$> desugarB side ps rhs
 
@@ -857,6 +826,8 @@ mutual
              UnboundImplicits a => do
                setUnboundImplicits a
                pure [IPragma (\nest, env => setUnboundImplicits a)]
+             PrefixRecordProjections b => do
+               pure [IPragma (\nest, env => setPrefixRecordProjections b)]
              AmbigDepth n => pure [IPragma (\nest, env => setAmbigLimit n)]
              AutoImplicitDepth n => pure [IPragma (\nest, env => setAutoImplicitLimit n)]
              PairNames ty f s => pure [IPragma (\nest, env => setPair fc ty f s)]

src/Idris/Parser.idr

@@ -241,10 +241,9 @@ mutual
            (op, e) <- pure b.val
            pure (PSectionL (boundToFC fname (mergeBounds s b)) op e)
     <|> do  -- (.y.z)  -- section of projection (chain)
-           b <- bounds (MkPair <$> (some $ postfixApp fname indents) <*> (many $ simpleExpr fname indents))
+           b <- bounds $ some postfixProj
-           (projs, args) <- pure b.val
            symbol ")"
-           pure $ PPostfixProjsSection (boundToFC fname b) projs args
+           pure $ PPostfixAppPartial (boundToFC fname b) b.val
       -- unit type/value
     <|> do b <- bounds (continueWith indents ")")
            pure (PUnit (boundToFC fname (mergeBounds s b)))
@@ -340,22 +339,24 @@ mutual
      <|> do end <- bounds (continueWith indents ")")
             pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
 
-  postfixApp : FileName -> IndentInfo -> Rule PTerm
+  postfixProjection : FileName -> IndentInfo -> Rule PTerm
-  postfixApp fname indents
+  postfixProjection fname indents
-    = do di <- bounds dotIdent
+    = do di <- bounds postfixProj
          pure $ PRef (boundToFC fname di) di.val
-    <|> (symbol ".(" *> commit *> expr pdef fname indents <* symbol ")")
 
   simpleExpr : FileName -> IndentInfo -> Rule PTerm
   simpleExpr fname indents
     = do  -- x.y.z
           b <- bounds (do root <- simplerExpr fname indents
-                          projs <- many $ postfixApp fname indents
+                          projs <- many postfixProj
                           pure (root, projs))
           (root, projs) <- pure b.val
           pure $ case projs of
             [] => root
-            _  => PPostfixProjs (boundToFC fname b) root projs
+            _  => PPostfixApp (boundToFC fname b) root projs
+    <|> do
+          b <- bounds (some postfixProj)
+          pure $ PPostfixAppPartial (boundToFC fname b) b.val
 
   simplerExpr : FileName -> IndentInfo -> Rule PTerm
   simplerExpr fname indents
@@ -631,12 +632,13 @@ mutual
     where
       fieldName : Name -> String
       fieldName (UN s) = s
+      fieldName (RF s) = s
       fieldName _ = "_impossible"
 
       -- this allows the dotted syntax .field
       -- but also the arrowed syntax ->field for compatibility with Idris 1
       recFieldCompat : Rule Name
-      recFieldCompat = dotIdent <|> (symbol "->" *> name)
+      recFieldCompat = postfixProj <|> (symbol "->" *> name)
 
   rewrite_ : FileName -> IndentInfo -> Rule PTerm
   rewrite_ fname indents
@@ -932,7 +934,6 @@ onoff
 extension : Rule LangExt
 extension
     = (exactIdent "ElabReflection" *> pure ElabReflection)
-  <|> (exactIdent "PostfixProjections" *> pure PostfixProjections)
   <|> (exactIdent "Borrowing" *> pure Borrowing)
 
 totalityOpt : Rule TotalReq
@@ -964,6 +965,10 @@ directive fname indents
          b <- onoff
          atEnd indents
          pure (UnboundImplicits b)
+  <|> do pragma "prefix_record_projections"
+         b <- onoff
+         atEnd indents
+         pure (PrefixRecordProjections b)
   <|> do pragma "ambiguity_depth"
          lvl <- intLit
          atEnd indents

src/Idris/Pretty.idr

@@ -277,10 +277,10 @@ mutual
       go d (PRangeStream _ start (Just next)) =
         brackets (go startPrec start <+> comma <++> go startPrec next <++> pretty "..")
       go d (PUnifyLog _ lvl tm) = go d tm
-      go d (PPostfixProjs fc rec fields) =
+      go d (PPostfixApp fc rec fields) =
-        parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (go startPrec <$> fields)
+        parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (map pretty fields)
-      go d (PPostfixProjsSection fc fields args) =
+      go d (PPostfixAppPartial fc fields) =
-        parens (dot <+> concatWith (surround dot) (go startPrec <$> fields) <+> fillSep (go appPrec <$> args))
+        parens (dot <+> concatWith (surround dot) (map pretty fields))
       go d (PWithUnambigNames fc ns rhs) = parenthesise (d > appPrec) $ group $ with_ <++> pretty ns <+> line <+> go startPrec rhs
 
 export

src/Idris/Syntax.idr

@@ -93,10 +93,10 @@ mutual
        PRange : FC -> PTerm -> Maybe PTerm -> PTerm -> PTerm
        -- A stream range [x,y..]
        PRangeStream : FC -> PTerm -> Maybe PTerm -> PTerm
-       -- r.x.y, equivalent to (y (x r))
+       -- r.x.y
-       PPostfixProjs : FC -> PTerm -> List PTerm -> PTerm
+       PPostfixApp : FC -> PTerm -> List Name -> PTerm
-       -- (.x.y p q), equivalent to (\r => r.x.y p q)
+       -- .x.y
-       PPostfixProjsSection : FC -> List PTerm -> List PTerm -> PTerm
+       PPostfixAppPartial : FC -> List Name -> PTerm
 
        -- Debugging
        PUnifyLog : FC -> LogLevel -> PTerm -> PTerm
@@ -150,8 +150,8 @@ mutual
   getPTermLoc (PRewrite fc _ _) = fc
   getPTermLoc (PRange fc _ _ _) = fc
   getPTermLoc (PRangeStream fc _ _) = fc
-  getPTermLoc (PPostfixProjs fc _ _) = fc
+  getPTermLoc (PPostfixApp fc _ _) = fc
-  getPTermLoc (PPostfixProjsSection fc _ _) = fc
+  getPTermLoc (PPostfixAppPartial fc _) = fc
   getPTermLoc (PUnifyLog fc _ _) = fc
   getPTermLoc (PWithUnambigNames fc _ _) = fc
 
@@ -237,6 +237,7 @@ mutual
        Overloadable : Name -> Directive
        Extension : LangExt -> Directive
        DefaultTotality : TotalReq -> Directive
+       PrefixRecordProjections : Bool -> Directive
        AutoImplicitDepth : Nat -> Directive
 
   public export
@@ -602,13 +603,10 @@ mutual
     showPrec d (PRangeStream _ start (Just next))
         = "[" ++ showPrec d start ++ ", " ++ showPrec d next ++ " .. ]"
     showPrec d (PUnifyLog _ _ tm) = showPrec d tm
-    showPrec d (PPostfixProjs fc rec fields)
+    showPrec d (PPostfixApp fc rec fields)
         = showPrec d rec ++ concatMap (\n => "." ++ show n) fields
-    showPrec d (PPostfixProjsSection fc fields args)
+    showPrec d (PPostfixAppPartial fc fields)
-        = "("
+        = concatMap (\n => "." ++ show n) fields
-            ++ concatMap (\n => "." ++ show n) fields
-            ++ concatMap (\x => " " ++ showPrec App x) args
-            ++ ")"
     showPrec d (PWithUnambigNames fc ns rhs)
         = "with " ++ show ns ++ " " ++ showPrec d rhs
 
@@ -906,12 +904,11 @@ mapPTermM f = goPTerm where
     goPTerm (PUnifyLog fc k x) =
       PUnifyLog fc k <$> goPTerm x
       >>= f
-    goPTerm (PPostfixProjs fc rec fields) =
+    goPTerm (PPostfixApp fc rec fields) =
-      PPostfixProjs fc <$> goPTerm rec <*> pure fields
+      PPostfixApp fc <$> goPTerm rec <*> pure fields
-      >>= f
-    goPTerm (PPostfixProjsSection fc fields args) =
-      PPostfixProjsSection fc fields <$> goPTerms args
       >>= f
+    goPTerm (PPostfixAppPartial fc fields) =
+      f (PPostfixAppPartial fc fields)
     goPTerm (PWithUnambigNames fc ns rhs) =
       PWithUnambigNames fc ns <$> goPTerm rhs
       >>= f

src/Parser/Rule/Source.idr

@@ -96,8 +96,8 @@ aDotIdent = terminal "Expected dot+identifier"
 
 
 export
-dotIdent : Rule Name
+postfixProj : Rule Name
-dotIdent = UN <$> aDotIdent
+postfixProj = RF <$> aDotIdent
 
 export
 symbol : String -> Rule ()
@@ -215,12 +215,12 @@ name = opNonNS <|> do
       else pure $ mkNamespacedName ns x
 
   opNonNS : Rule Name
-  opNonNS = symbol "(" *> operator <* symbol ")"
+  opNonNS = symbol "(" *> (operator <|> postfixProj) <* symbol ")"
 
   opNS : Namespace -> Rule Name
   opNS ns = do
     symbol ".("
-    n <- operator
+    n <- (operator <|> postfixProj)
     symbol ")"
     pure (NS ns n)
 

src/TTImp/ProcessRecord.idr

@@ -47,16 +47,21 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
          defs <- get Ctxt
          Just conty <- lookupTyExact conName (gamma defs)
              | Nothing => throw (InternalError ("Adding " ++ show tn ++ "failed"))
+
          -- Go into new namespace, if there is one, for getters
          case newns of
               Nothing =>
-                      elabGetters conName 0 [] [] conty -- make projections
+                   do elabGetters conName 0 [] RF [] conty -- make postfix projections
+                      when !isPrefixRecordProjections $
+                        elabGetters conName 0 [] UN [] conty -- make prefix projections
               Just ns =>
                    do let cns = currentNS defs
                       let nns = nestedNS defs
                       extendNS (mkNamespace ns)
                       newns <- getNS
-                      elabGetters conName 0 [] [] conty -- make projections
+                      elabGetters conName 0 [] RF [] conty -- make postfix projections
+                      when !isPrefixRecordProjections $
+                        elabGetters conName 0 [] UN [] conty -- make prefix projections
                       defs <- get Ctxt
                       -- Record that the current namespace is allowed to look
                       -- at private names in the nested namespace
@@ -122,17 +127,18 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
                   List (Name, RawImp) -> -- names to update in types
                     -- (for dependent records, where a field's type may depend
                     -- on an earlier projection)
+                  (mkProjName : String -> Name) ->
                   Env Term vs -> Term vs ->
                   Core ()
-    elabGetters con done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
+    elabGetters con done upds mkProjName tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
         = if (n `elem` map fst params) || (n `elem` vars)
              then elabGetters con
                               (if imp == Explicit && not (n `elem` vars)
                                   then S done else done)
-                              upds (b :: tyenv) sc
+                              upds mkProjName (b :: tyenv) sc
              else
                 do let fldNameStr = nameRoot n
-                   projNameNS <- inCurrentNS (UN fldNameStr)
+                   projNameNS <- inCurrentNS (mkProjName fldNameStr)
 
                    ty <- unelab tyenv ty_chk
                    let ty' = substNames vars upds ty
@@ -173,9 +179,9 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
                    elabGetters con
                                (if imp == Explicit
                                    then S done else done)
-                               upds' (b :: tyenv) sc
+                               upds' mkProjName (b :: tyenv) sc
 
-    elabGetters con done upds _ _ = pure ()
+    elabGetters con done upds _ _ _ = pure ()
 
 export
 processRecord : {vars : _} ->

src/TTImp/TTImp.idr

@@ -561,6 +561,7 @@ definedInBlock ns decls =
            UN _ => NS ns n
            MN _ _ => NS ns n
            DN _ _ => NS ns n
+           RF _ => NS ns n
            _ => n
 
     defName : Namespace -> ImpDecl -> List Name
@@ -576,11 +577,25 @@ definedInBlock ns decls =
         fldns' : Namespace
         fldns' = maybe ns (\ f => ns <.> mkNamespace f) fldns
 
+        toRF : Name -> Name
+        toRF (UN n) = RF n
+        toRF n = n
+
         fnsUN : List Name
         fnsUN = map getFieldName flds
 
+        fnsRF : List Name
+        fnsRF = map toRF fnsUN
+
+        -- Depending on %prefix_record_projections,
+        -- the record may or may not produce prefix projections (fnsUN).
+        --
+        -- However, since definedInBlock is pure, we can't check that flag
+        -- (and it would also be wrong if %prefix_record_projections appears
+        -- inside the parameter block)
+        -- so let's just declare all of them and some may go unused.
         all : List Name
-        all = expandNS ns n :: map (expandNS fldns') fnsUN
+        all = expandNS ns n :: map (expandNS fldns') (fnsRF ++ fnsUN)
 
     defName _ _ = []
 

tests/ideMode/ideMode001/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:239} : (Main.Vect n[0] a[1])) -> ({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

tests/ideMode/ideMode003/expected

@@ -2,13 +2,13 @@
 000038(:write-string "1/1: Building LocType (LocType.idr)" 1)
 0000ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 23) (:end 7 24)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "a")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 38) (:end 7 40)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:258} a)")))))) 1)
+0000df(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 35) (:end 7 37)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect {k:295} a)")))))) 1)
-0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:259}_[]")))))) 1)
+0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 9) (:end 7 10)) ((:name "x") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "?{_:296}_[]")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:258}_[] ?{_:259}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 14) (:end 7 16)) ((:name "xs") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{k:295}_[] ?{_:296}_[])")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:260}_[] ?{_:259}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 20)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:297}_[] ?{_:296}_[])")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 6 18)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1)
-0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:249}_[] ?{_:248}_[])")))))) 1)
+0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 13)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:286}_[] ?{_:285}_[])")))))) 1)
-0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:239} : (Main.Vect n[0] a[1])) -> ({arg:240} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
+0001eb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 7)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Types.Nat} -> {0 a : Type} -> {0 n : Prelude.Types.Nat} -> ({arg:276} : (Main.Vect n[0] a[1])) -> ({arg:277} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.Num.+ Prelude.Types.Nat Prelude.Types.Num implementation at Prelude/Types.idr:57:1--64:7 n[2] m[4]) a[3]))))))")))))) 1)
 0000cc(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 5 48)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)
 0000d9(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 41)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Types.Nat")))))) 1)

tests/idris2/record004/Main.idr

@@ -6,14 +6,34 @@ record Point where
   y : Double
 
 -- a record creates two projections:
+--
+-- .x : Point -> Double
+-- .y : Point -> Double
+--
+-- because %prefix_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
+%prefix_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 prefix 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
 
@@ -23,25 +43,46 @@ rect =
     (MkPoint 1.1 2.5)
     (MkPoint 4.3 6.3)
 
--- Foo.bar.baz with uppercase F is one lexeme: DotSepIdent ["baz", "bar", "Foo"]
+-- New lexical structure:
+--
+-- Foo.bar.baz with uppercase F is one lexeme: NSIdent ["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 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
+--
+-- 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.
 
-add : Num a => a -> a -> a
+-- user-defined projections work, too (should they?)
-add x y = x + y
+(.squared) : Double -> Double
+(.squared) x = x * x
 
-oopFoldl : List a -> b -> (b -> a -> b) -> b
-oopFoldl xs z f = foldl f z xs
 
-bad : Double
+-- #649: Forced patterns remain unaffected by postfix projections.
-bad = 
+test649 : (x, y : Bool) -> x = y -> Bool
-  rect.x.topLeft        -- should not throw errors
+test649 .(x) x Refl = x
-  + rect.(x . topLeft)  -- disallowed without %language PostfixProjections
 
-bad2 : Double
-bad2 = (.oopFoldl 0 (+))  -- disallowed without %language PostfixProjections
 
-%language PostfixProjections
+-- #441: Locals do not shadow record projections.
--- from now on, we can use complex projections
+test441 : (Point -> Double) -> (Point -> Double) -> Point -> Double
+test441 x y pt = pt.x + pt.y
+  -- no ambiguity errors: the locals "x" and "y" are not considered in pt.x and pt.y

tests/idris2/record004/expected

@@ -1,23 +1,10 @@
 1/1: Building Main (Main.idr)
-Error: complex postfix projections require %language PostfixProjections
-
-Main.idr:41:5--41:23
-    |
- 41 |   + rect.(x . topLeft)  -- disallowed without %language PostfixProjections
-    |     ^^^^^^^^^^^^^^^^^^
-
-Error: postfix projection sections require %language PostfixProjections
-
-Main.idr:44:9--44:24
-    |
- 44 | bad2 = (.oopFoldl 0 (+))  -- disallowed without %language PostfixProjections
-    |         ^^^^^^^^^^^^^^^
-
 Main> 4.2
 Main> 4.2
 Main> 10.8
 Main> 4.2
 Main> 4.2
+Main> 17.64
 Main> [1.1, 4.2]
 Main> Error: When unifying (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
 Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
@@ -28,14 +15,11 @@ Mismatch between: (?a -> ?b) -> ?f ?a -> ?f ?b and Point.
    | ^^^
 
 Main> [2.5, 2.5]
-Main> 8.1
-Main> [8.1, 8.1]
-Main> 6
-Main> [6, 15]
 Main> 7.4
-Main> 7.4
+Main> 4.2
-Main> 7.4
+Main> 4.2
-Main> MkPoint 1.1 2.5
+Main> 4.2
+Main> 4.2
 Main> 4.2
 Main> 4.2
 Main> 4.2

tests/idris2/record004/input

@@ -3,17 +3,15 @@ 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.add 7
-map (.topLeft.x.add 7) [rect, rect]
-[1,2,3].oopFoldl 0 $ \x, y => x + y
-map (.oopFoldl 0 (+)) [[1,2,3],[4,5,6]]
 rect.topLeft.x + rect.bottomRight.y
-rect.(x . topLeft) + rect.(y . bottomRight)
+Main.Point.(.x) pt
-x rect.topLeft + y rect.bottomRight
+Point.(.x) pt
-rect.(Rect.topLeft)
+(.x) pt
+.x pt
 Main.Point.x pt
 Point.x pt
 (x) pt

tests/idris2/reflection004/refdecl.idr

@@ -16,7 +16,7 @@ mkPoint n
     = let type = "Point" ++ show n ++ "D" in
       IRecord emptyFC Public
       (MkRecord emptyFC (NS (MkNS ["Main"]) (UN type)) [] (NS (MkNS ["Main"]) (UN ("Mk" ++ type)))
-        (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (UN axis) `(Double)) (axes n)))
+        (toList $ map (\axis => MkIField emptyFC MW ExplicitArg (RF axis) `(Double)) (axes n)))
 
 logDecls : TTImp -> Elab (Int -> Int)
 logDecls v