summaryrefslogtreecommitdiff
path: root/Source/Dafny/Resolver.cs
Commit message (Collapse)AuthorAge
* 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.
* Added ghost let expressions.Gravatar Rustan Leino2014-01-05
|
* Improved the name-clashing situation when substituting to produce printable ↵Gravatar Rustan Leino2014-01-03
| | | | AdditionalInformation for forall-statement ensures clauses.
* MergeGravatar Rustan Leino2014-01-03
|\
| * Make ModuleDefinition inherit from TopLevelDecl instead of just DeclarationGravatar Bryan Parno2014-01-03
| |
* | Allow "match" expressions anywhereGravatar Rustan Leino2014-01-03
|/
* Hover text for inferred postconditions of 'forall' statements (the one for ↵Gravatar Rustan Leino2013-12-30
| | | | calls leaves something to be desired)
* MergeGravatar Rustan Leino2013-12-30
|\
* | Added proper parsing for StmtExpr's in all contexts.Gravatar Rustan Leino2013-12-30
| | | | | | | | | | | | Adjusted printer accordingly. Fixed bug in Substituter for CalcStmt in StmtExpr's. Always show terminating semi-colon in hover-text for default decreases clauses.
| * Changed the iterator class hover text back to the iterator name (which is ↵Gravatar Rustan Leino2013-12-20
|/ | | | consistent with everything else), not the "iterator" keyword
* Hover text for default decreases clauses of loops.Gravatar Rustan Leino2013-12-20
| | | | Collected various routines used to create resolved Dafny expressions into the Expression class.
* Moved the hover text of iterator classes to the "iterator" keyword itself ↵Gravatar Rustan Leino2013-12-19
| | | | (since it is long and there may be other things hanging off the iterator name)
* MergeGravatar Rustan Leino2013-12-19
|\
* | Added an .EndTok for every statement. (Note, in some places, especially in ↵Gravatar Rustan Leino2013-12-19
| | | | | | | | | | | | | | VarDecl statements, there's often no good .EndTok information.) Used the .EndTok in CaptureState information. In other words, move the blue dots in the IDE to after the statement just executed. Removed /*!*/ comments in some parts of the source code -- CodeContracts reveal this information.
| * Compute default decreases clauses in Resolver instead of in the Translator.Gravatar Rustan Leino2013-12-19
|/ | | | Make this information available as AdditionalInformation, that is, as hover text in the IDE.
* MergeGravatar Bryan Parno2013-12-13
|\
| * Produce "tail recursive" hover text in the IDE only for methods that are ↵Gravatar Rustan Leino2013-12-13
| | | | | | | | recursive
* | Added support for opaque function definitions, indicated via the {:opaque} ↵Gravatar Bryan Parno2013-12-13
|/ | | | | | | | attribute. Dafny cannot see the body of opaque function foo() unless you call the (automatically generated) lemma reveal_foo(). This can be helpful in preventing Dafny from spending unnecessary time thinking about the body of a function.
* Refactored the calling of rewritersGravatar Rustan Leino2013-12-11
|
* Fixed bug reported as discussion:472216 on dafny.codeplex.comGravatar Rustan Leino2013-12-09
|
* Allow calls to side-effect-free ghost methods from expressionsGravatar Rustan Leino2013-08-06
|
* 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 hover text ("additional information") in places where co-predicates ↵Gravatar Rustan Leino2013-08-04
| | | | provide syntactic shorthands
* Allow co-predicates to be wrapped inside bounded existential quantifiersGravatar Rustan Leino2013-08-04
|
* Added hover text ("additional information") in places where co-methods ↵Gravatar Rustan Leino2013-08-04
| | | | provide syntactic shorthands
* Disallow call-graph clusters that mix co-methods / prefix methods with other ↵Gravatar Rustan Leino2013-08-04
| | | | | | things. Disallow call-graph clusters that mix co-predicates / prefix predicates with other things.
* Set up call-graph to keep track of edges between functions and methods. (To ↵Gravatar Rustan Leino2013-08-04
| | | | be done: replace InMethodContext with a Function/Method-Height in translator.)
* Introduced keywords "lemma" (like a "ghost method", but not allowed to have ↵Gravatar Rustan Leino2013-08-02
| | | | a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
* MergeGravatar Nadia Polikarpova2013-07-31
|\
* | Allowing dangling hints in calculations.Gravatar Nadia Polikarpova2013-07-31
| |
| * Minor changeGravatar wuestholz2013-07-30
|/
* Added "co-recursive call" to drop boxGravatar Rustan Leino2013-07-30
|
* Simplified the guardedness checking algorithmGravatar Rustan Leino2013-07-30
|
* Co-recursion, now sounder than ever!Gravatar Rustan Leino2013-07-30
| | | | | | - prefix equality is destructive - co-methods are not allowed to have out-parameters - in an SCC with both co-recursive and recursive calls, the latter are allowed only in non-destructive contexts
* Allow field names to be sequences of digits (this is nice, for example, to ↵Gravatar Rustan Leino2013-07-24
| | | | define a Tuple with fields .0 and .1)
* DafnyExtension: Added support for collecting additional information during ↵Gravatar wuestholz2013-07-15
| | | | resolution and displaying it.
* Datatypes with ghost fields (that is, with constructors with ghost ↵Gravatar Rustan Leino2013-07-09
| | | | | | parameters) do not support equality, since the ghost fields will be erased during compilation. Allow any equalities to be passed in for ghost parameters.
* Fixed bugs reported as Issue 20.Gravatar Rustan Leino2013-07-04
| | | | | | For the first one, co-recursive calls are allowed only immediately inside co-constructors (which previously wasn't checked properly). For the second one, a resolution error had caused a crash in Dafny. Also, tightened up requirement about equality, since equality on non-codatatypes can also be destructive (if the type contains a co-datatype value).
* Fixed soundness bug with co-recursive calls: co-recursive calls may now no ↵Gravatar Rustan Leino2013-06-29
| | | | longer to to functions with ensures clauses
* Fixed unsoundness (and also allowed other, sound cases) in the admissability ↵Gravatar Rustan Leino2013-06-28
| | | | checks for co-recursive calls
* Fixed some Code Contract type errorsGravatar Rustan Leino2013-06-25
|
* Fixed a problem where changes to a substMap were not being undone, curing ↵Gravatar Rustan Leino2013-06-20
| | | | | | Issue 15 on dafny.codeplex.com. Also fixed some code that make an optimization possible.
* 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 bug, where prefix predicate was not included in CheckTypeInference visitorGravatar Rustan Leino2013-05-21
|
* Refactored some resolution stages to make use of VisitorsGravatar Rustan Leino2013-04-02
|
* Moved resolution of BinaryExpr.ResolveOp until the CheckTypeInference phase, ↵Gravatar Rustan Leino2013-04-01
| | | | | | | where more type information is known Refactored ConcreteUpdateStatement to no longer inherit from ConcreteSyntaxStatement. Fixed numerous places where some recursive checks did not reach.
* 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
|
* Type-inference support for cardinality operatorGravatar Rustan Leino2013-03-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 08:29:46 +0000