Re-introduce %prefix_record_projections.

docs/source/reference/records.rst

@@ -53,13 +53,13 @@ Desugaring rules
 Record elaboration
 ------------------
 
-* there is a new pragma ``%undotted_record_projections``, which is ``on`` by
+* 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
-    ``%undotted_record_projections`` is ``off``
+    ``%prefix_record_projections`` is ``off``
 
   * projection ``.f`` in namespace ``R`` with the same definition
 
@@ -77,7 +77,7 @@ This record creates two projections:
 * ``.x : Point -> Double``
 * ``.y : Point -> Double``
 
-Because ``%undotted_record_projections`` are ``on`` by default, we also get:
+Because ``%prefix_record_projections`` are ``on`` by default, we also get:
 * ``x : Point -> Double``
 * ``y : Point -> Double``
 
@@ -85,14 +85,14 @@ To prevent cluttering the ordinary global name space with short identifiers, we
 
 .. code-block:: idris
 
-    %undotted_record_projections off
+    %prefix_record_projections off
 
     record Rect where
       constructor MkRect
       topLeft : Point
       bottomRight : Point
 
-For ``Rect``, we don't get the undotted projections:
+For ``Rect``, we don't get the prefix projections:
 
 .. code-block:: idris
 

docs/source/tutorial/typesfuns.rst

@@ -1003,10 +1003,10 @@ We can use prefix field projections, like in Haskell:
     firstName : Person -> String
 
 Prefix field projections can be disabled per record definition
-using pragma ``%undotted_record_projections off``, which makes
+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 ``%undotted_record_projections on``.
+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

src/Core/Context.idr

@@ -362,7 +362,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
@@ -2097,10 +2097,10 @@ setUnboundImplicits a
          put Ctxt (record { options->elabDirectives->unboundImplicits = a } defs)
 
 export
-setUndottedRecordProjections : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
-setUndottedRecordProjections b = do
+setPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Bool -> Core ()
+setPrefixRecordProjections b = do
   defs <- get Ctxt
-  put Ctxt (record { options->elabDirectives->undottedRecordProjections = b } defs)
+  put Ctxt (record { options->elabDirectives->prefixRecordProjections = b } defs)
 
 export
 setDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->
@@ -2138,9 +2138,9 @@ isUnboundImplicits
          pure (unboundImplicits (elabDirectives (options defs)))
 
 export
-isUndottedRecordProjections : {auto c : Ref Ctxt Defs} -> Core Bool
-isUndottedRecordProjections =
-  undottedRecordProjections . elabDirectives . options <$> get Ctxt
+isPrefixRecordProjections : {auto c : Ref Ctxt Defs} -> Core Bool
+isPrefixRecordProjections =
+  prefixRecordProjections . elabDirectives . options <$> get Ctxt
 
 export
 getDefaultTotalityOption : {auto c : Ref Ctxt Defs} ->

src/Core/Options.idr

@@ -113,8 +113,12 @@ record ElabDirectives where
   unboundImplicits : Bool
   totality : TotalReq
   ambigLimit : Nat
-  undottedRecordProjections : Bool
   autoImplicitLimit : Nat
+  --
+  -- produce traditional (prefix) record projections,
+  -- in addition to postfix (dot) projections
+  -- default: yes
+  prefixRecordProjections : Bool
 
 public export
 record Session where
@@ -181,7 +185,7 @@ defaultSession = MkSessionOpts False False False Chez [] defaultLogLevel
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 True 50
+defaultElab = MkElabDirectives True True CoveringOnly 3 50 True
 
 export
 defaults : Options

src/Idris/Desugar.idr

@@ -825,8 +825,8 @@ mutual
              UnboundImplicits a => do
                setUnboundImplicits a
                pure [IPragma (\nest, env => setUnboundImplicits a)]
-             UndottedRecordProjections b => do
-               pure [IPragma (\nest, env => setUndottedRecordProjections b)]
+             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

@@ -979,10 +979,10 @@ directive fname indents
          b <- onoff
          atEnd indents
          pure (UnboundImplicits b)
-  <|> do pragma "undotted_record_projections"
+  <|> do pragma "prefix_record_projections"
          b <- onoff
          atEnd indents
-         pure (UndottedRecordProjections b)
+         pure (PrefixRecordProjections b)
   <|> do pragma "ambiguity_depth"
          lvl <- intLit
          atEnd indents

src/Idris/Syntax.idr

@@ -237,7 +237,7 @@ mutual
        Overloadable : Name -> Directive
        Extension : LangExt -> Directive
        DefaultTotality : TotalReq -> Directive
-       UndottedRecordProjections : Bool -> Directive
+       PrefixRecordProjections : Bool -> Directive
        AutoImplicitDepth : Nat -> Directive
 
   public export

src/TTImp/ProcessRecord.idr

@@ -46,19 +46,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"))
-         addUndotted <- isUndottedRecordProjections
+
          -- Go into new namespace, if there is one, for getters
          case newns of
               Nothing =>
                    do elabGetters conName 0 [] RF [] conty -- make postfix projections
-                      elabGetters conName 0 [] UN [] conty -- make prefix 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 [] RF [] conty -- make postfix projections
-                      elabGetters conName 0 [] UN [] conty -- make prefix 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

src/TTImp/TTImp.idr

@@ -576,11 +576,11 @@ definedInBlock ns decls =
         fnsRF : List Name
         fnsRF = map toRF fnsUN
 
-        -- Depending on %undotted_record_projections,
-        -- the record may or may not produce undotted projections (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 %undotted_record_projections appears
+        -- (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

tests/idris2/record004/Main.idr

@@ -10,13 +10,13 @@ record Point where
 -- .x : Point -> Double
 -- .y : Point -> Double
 --
--- because %undotted_record_projections are on by default, we also get:
+-- 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
-%undotted_record_projections off
+%prefix_record_projections off
 
 record Rect where
   constructor MkRect
@@ -26,7 +26,7 @@ record Rect where
 -- .topLeft : Rect -> Point
 -- .bottomRight : Rect -> Point
 --
--- For Rect, we don't get the undotted projections:
+-- For Rect, we don't get the prefix projections:
 --
 -- Main> :t topLeft
 -- (interactive):1:4--1:11:Undefined name topLeft