| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
| |
Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we
print tokens, we need to decrement the column number. This was done for resolver
errors, but not for verification or parsing errors. In addition, parsing errors
were inconsistent with resolution errors case-wise.
Unfortunately, the fix affects the output of many tests.
|
|
|
|
| |
a module import.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Although
convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported. This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior. For auto-declare, identifiers could be used in the program
without having a declaration. For fill-in parameters, the implicitly declared
type parameters remain anonymous.
|
|
|
|
|
|
|
| |
so use the new name resolution machinery that handles modules and type parameters
Included some inadvertently left-out test cases in dafny0/Modules0.dfy
Fixed comparable-types tests
|
|
|
|
|
|
|
|
|
|
| |
class are now
automatically static, and fields are no longer allowed to be declared there. Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module. The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.
|
| |
|
|
|
|
| |
now created by the parser into the system module.
|
| |
|
| |
|
|
|