summaryrefslogtreecommitdiff
path: root/Source/Dafny/Compiler.cs
Commit message (Collapse)AuthorAge
* Added initial support for dirty while statements.Gravatar chmaria2014-11-01
|
* Comparisons and well-founded order of charGravatar leino2014-10-21
|
* Add char literals.Gravatar leino2014-10-20
| | | | Disallow backslash from being part of identifier names.
* Added types "char" and "string" (the latter being a synonym for "seq<char>").Gravatar leino2014-10-20
| | | | | | Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes.
* Refactored ArrowType's to be resolved with other types. ArrowTypeDecl's are ↵Gravatar leino2014-08-27
| | | | now created by the parser into the system module.
* Refactoring: renamed DerivedTypeDecl to NewtypeDeclGravatar leino2014-08-26
|
* Implemented arbitrary numeric conversions (but name resolution still needs ↵Gravatar leino2014-08-25
| | | | work when module names are involved)
* Support for non-constrained derived types ("new types").Gravatar leino2014-08-21
| | | | | Arbitrary conversion from int/real to derived types not yet supported. Changed rules about numeric type conversions to allow conversions from any numeric type.
* Start of derived types (aka "new types")Gravatar leino2014-08-20
| | | | Fixed bug in type checking for integer division.
* Refactor: Change ApplyExpr's Receiver to FunctionGravatar Dan Rosén2014-08-14
|
* Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
|
* MergeGravatar Dan Rosén2014-08-11
|\
* | Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter
| * MergeGravatar leino2014-08-02
| |\
| * | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵Gravatar leino2014-08-02
|/ / | | | | | | the resolver and translator
| * - fixed an issue regarding including ghost functions in the compiled interfaceGravatar Reza Ahmadi2014-07-20
| | | | | | | | - added one more test
| * added trait feature:Gravatar Reza Ahmadi2014-07-18
|/ | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* Renamed "arbitrary type" to "opaque type"Gravatar Rustan Leino2014-07-15
|
* Added type synonyms. (No support yet for these in refinements.)Gravatar Rustan Leino2014-07-11
|
* Implemented compilation of the int<->real conversions, and changed the ↵Gravatar Rustan Leino2014-07-08
| | | | | | resolution and verification implementations of these. Changed FreshExpr to be a UnaryExpr, and also introduced the UnaryOpExpr subclass.
* Added tuples and tuple types. Syntax is the expected one, namely parentheses ↵Gravatar Rustan Leino2014-06-27
| | | | around a comma-delimited list of expressions or types. Unit and the unit type are denoted ().
* Added support for 'dirty' forall statements.Gravatar chmaria2014-06-03
| | | | | | | | | | | One can now write forall statements without bodies (but with ensures clauses) as follows: forall s | s in S ensures s < 0; where S is set<int>. The ensures clauses are assumed but not checked.
* Fixed bug in resolution, where type proxies involved in equality tests did ↵Gravatar Rustan Leino2014-05-07
| | | | | | not get assigned. (Issue #35) Fixed Main detection--a method "Main" with type parameters cannot be a program entry point.
* DafnyExtension: Made it display the compilation output in the VS output pane.Gravatar wuestholz2014-04-21
|
* Compile realsGravatar Rustan Leino2014-04-13
|
* MergeGravatar Rustan Leino2014-04-04
|\
* | Added "modify Frame { Body }" statement.Gravatar Rustan Leino2014-04-04
| |
* | Added "modify" statement.Gravatar Rustan Leino2014-04-03
| | | | | | | | In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
| * Basic support for datatype-update syntatic sugarGravatar Bryan Parno2014-04-03
|/
* Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵Gravatar Rustan Leino2014-03-17
| | | | to VarDeclStmt.Locals
* AST refactoring:Gravatar Rustan Leino2014-03-17
| | | | | Changed VarDecl to no longer inherit from Statement. Removed ConcreteSyntaxStatement and changed VarDeclStmt's superclass be Statement.
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
|
* Compile to .exe only if the Main method has no user-defined preconditions.Gravatar Rustan Leino2014-01-31
| | | | If Main is already declared as static, don't produce a second static Main.
* Fix minor issue in compilation of main methods.Gravatar wuestholz2014-01-17
|
* MergeGravatar Rustan Leino2014-01-08
|\
* | Allow left-hand sides of a let expression to be patterns (like in the case ↵Gravatar Rustan Leino2014-01-08
| | | | | | | | | | | | | | of a match expression). Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator. Fixed compilation of match expressions, to allow them anywhere.
| * Compile assign-such-that for all integers, not just ones where a bound is foundGravatar Rustan Leino2014-01-06
|/
* More thoroughly check for nested assume statements during compilationGravatar Rustan Leino2014-01-05
|
* Added ghost let expressions.Gravatar Rustan Leino2014-01-05
|
* Add support for the :axiom attribute for ghost methods.Gravatar Bryan Parno2013-12-13
| | | | | | This suppresses compiler errors for ghost methods and functions without bodies. Also changed the parser to complain about bodyless methods and functions without bodies if /noCheating:1 is specified.
* Use full name of type in compilation errorGravatar Rustan Leino2013-11-18
|
* Let compiler complain about body-less functions and methods, even if these ↵Gravatar Rustan Leino2013-11-14
| | | | are ghost
* Merged PredicateExpr and CalcExpr into a single StmtExprGravatar Rustan Leino2013-08-06
| | | | In that process, added a SubstStmt method (and entourage) for substituting into statements
* Added support for more fine-grained generation of unique names.Gravatar wuestholz2013-07-31
| | | | | Creation of unique names is now deferred until translation to Boogie or C#. For Boogie names are unique within a Dafny class member.
* Fixed compilation bug where C# keywords were not being escapedGravatar Rustan Leino2013-06-25
|
* Allow more tail calls, on account of considering non-loop aggregate ↵Gravatar Rustan Leino2013-05-21
| | | | statements with only ghost sub-statements to be ghost
* Fixed compilation of assign-such-that for the multi-variable case where some ↵Gravatar Rustan Leino2013-03-29
| | | | bounds are infinite
* The "choose" statement, hacky and specialized as it was, is now gone. Use ↵Gravatar Rustan Leino2013-03-27
| | | | the assign-such-that statement instead. For example: x :| x in S;
* Replaced SuperSetBoundedPool by SubSetBoundedPool, which is much more useful ↵Gravatar Rustan Leino2013-03-27
| | | | | | in compiling assign-such-that statements Added run-time support for printing sets, multisets, maps, and sequences
* Compilation of (many common) assign-such-that statements.Gravatar Rustan Leino2013-03-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 02:25:32 +0000