RM updates re grammar (#1089)

Co-authored-by: davidcok <[email protected]>

Author: davidcok

RELEASE.txt

@@ -6,12 +6,9 @@ This is the procedure for generating a new Dafny release.
 1) In an up-to-date repository, with the master branch checked out
    and up-to-date (e.g., git pull upstream)
    cd to the repo root (i.e., dafny, which contains Source, Binaries, etc.)
-   create and checkout a new branch: e.g. git checkout -b release
 
 2) Select a version number (descriptor) $VER (e.g., "3.0.0-alpha")
-   Edit it into Source/version.cs
-   Also edit the release name into .github/workflows/release-downloads.yml
-   for the 'ver' variable for Windows
+   Edit it into Source/version.cs. Push/merge that change to the master branch.
 
 3) Run 'Scripts/package.py "$VER"' (in a Linux or Mac system)
    Warnings about missing fonts can be ignored.
@@ -24,7 +21,10 @@ This is the procedure for generating a new Dafny release.
 
 6) Push the Publish button.
 
-7) Commit the modified files, such as Source/version.cs,
+7) Edit the release name into .github/workflows/release-downloads.yml
+   for the 'ver' variable for Windows
+
+   Commit the modified files, such as
    .github/workflows/release-downloads,yml, docs/DafnyRef/DafnyRef.pdf,
    possibly docs/DafnyRef/Options.txt
 

Scripts/quicktest.out

@@ -10,31 +10,16 @@ Dafny program verifier finished with 0 verified, 1 error
 Compiling on C#
 
 Dafny program verifier finished with 0 verified, 0 errors
-Running...
-
 (42, 131)
 Compiling to Javascript
 
 Dafny program verifier finished with 0 verified, 0 errors
-Running...
-
 (42, 131)
 Compiling to Java
 
 Dafny program verifier finished with 0 verified, 0 errors
-Compiled program written to c-java/c.java
-Additional code written to c-java/_System/nat.java
-Additional code written to c-java/_System/__default.java
-Additional code written to c-java/dafny/Tuple0.java
-Running...
-
 (42, 131)
 Compiling to Go
 
 Dafny program verifier finished with 0 verified, 0 errors
-Compiled program written to c-go/src/c.go
-Additional code written to c-go/src/dafny/dafny.go
-Additional code written to c-go/src/System_/System_.go
-Running...
-
 (42, 131)

Scripts/quicktest.sh

@@ -10,11 +10,11 @@ $DIR/dafny /compile:0 a.dfy
 echo Should fail
 $DIR/dafny /compile:0 -useBaseNameForFileName b.dfy
 echo Compiling on C#
-$DIR/dafny /compile:3 /compileTarget:cs c.dfy
+$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:cs c.dfy
 echo Compiling to Javascript
-$DIR/dafny /compile:3 /compileTarget:js c.dfy
+$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:js c.dfy
 echo Compiling to Java
-$DIR/dafny /compile:3 /compileTarget:java c.dfy
+$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:java c.dfy
 echo Compiling to Go
-$DIR/dafny /compile:3 /compileTarget:go c.dfy
+$DIR/dafny /compile:3 /compileVerbose:0 /compileTarget:go c.dfy
 rm -rf a.dfy b.dfy c.dfy c-go c-java c

Source/Dafny/Dafny.atg

@@ -1030,7 +1030,8 @@ ModuleExport<ModuleDefinition parent, out ModuleDecl submodule>
   .
 
 /*------------------------------------------------------------------------*/
-// TODO - this is somewhat a hack because it relies on TypeNameOrCtorSuffix
+// Note - before the "." only Type names are permitted (no 'digits'), but name resolution sorts that
+// out, since the parser does not know (without adding lookahead) when it has seen the last dot
 // matching any permitted member name
 
 ExportSignature<bool opaque, out ExportSignature exsig>

docs/DafnyRef/DafnyRef.md

@@ -54,32 +54,8 @@ user understand how to do proofs with Dafny.
 <!--PDF NEWPAGE-->
 {% include_relative UserGuide.md %}
 
-# 25. TODO
 
--- const, static const
-
--- declarations
-
--- inference of array sizes
-
--- witness, ghost witness clauses
-
--- customizable error messages
-
--- opaque types
-
--- traits, object
-
--- non-null types
-
--- abstemious functions
-
--- labels (for program locations)
-
--- updates to shared destructors
-
--- labelled assertion statements, labelled preconditions
 
 {% include_relative SyntaxTests.md %}
 
-# 27. References
+# 26. References

docs/DafnyRef/Expressions.md

@@ -501,12 +501,12 @@ TODO: what about multi-dimensional arrays
 
 ## 20.17. Object Allocation
 ````grammar
-ObjectAllocation_ = "new" Type [ "." ( Ident | digits ) ]
+ObjectAllocation_ = "new" Type [ "." TypeNameOrCtorSuffix ]
                                [ "(" [ Expressions ] ")" ]
 ````
 
 This allocated a new object of a class type as explained
-in section [Class Types](#sec-class-types)].
+in section [Class Types](#sec-class-types).
 
 ## 20.18. Havoc Right-Hand-Side
 ````grammar

docs/DafnyRef/Grammar.md

@@ -470,8 +470,11 @@ MethodFunctionName = NoUSIdentOrDigits
 LabelName = NoUSIdentOrDigits
 AttributeName = NoUSIdent
 ExportId = NoUSIdentOrDigits
+TypeNameOrCtorSuffix = NoUSIdentOrDigits
 ````
 
+Some parsing constexts
+
 ### 2.6.3. Qualified Names
 ```grammar
 QualifiedModuleName = ModuleName { "." ModuleName }

docs/DafnyRef/Modules.md

@@ -294,7 +294,7 @@ ModuleExport =
   | "extends"  ExportId { "," ExportId }
   }
 
-ExportSignature = IdentOrDigits [ "." IdentOrDigits ]
+ExportSignature = TypeNameOrCtorSuffix [ "." TypeNameOrCtorSuffix ]
 ````
 
 In some programming languages, keywords such as `public`, `private`, and `protected`

docs/DafnyRef/Refinement.md

@@ -62,7 +62,7 @@ Typically this is the presence of a `...` token.
 
 A refining export set declaration begins with the syntax
 ````grammar
-"export" Ident "..."
+"export" Ident ellipsis
 ````
 but otherwise contains the same `provides`, `reveals` and `extends` sections,
 with the ellipsis indicating that it is a refining declaration.

docs/DafnyRef/Statements.md

@@ -607,7 +607,9 @@ VarDeclStatement =
   )
   ";"
 
-CasePatternLocal = "(" CasePattern { "," CasePattern } ")"  // TODO
+CasePatternLocal = ( [ Ident ] "(" CasePatternLocsl { "," CasePatternLocal } ")"
+                   | LocalIdentTypeOptional
+                   )
 ````
 
 A ``VarDeclStatement`` is used to declare one or more local variables in