summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
...
* | Shorter wait-for-idle time in the Dafny IDEGravatar leino2014-09-29
| |
| * DafnyExtension: Made it not log the pretty-printed program.Gravatar wuestholz2014-09-28
| |
| * DafnyExtension: minor change due to change in BoogieGravatar wuestholz2014-09-28
| |
| * Did more refactoring.Gravatar wuestholz2014-09-23
| |
| * Did more refactoring.Gravatar wuestholz2014-09-23
| |
| * Did some refactoring.Gravatar wuestholz2014-09-23
| |
| * DafnyExtension: minor changeGravatar wuestholz2014-09-22
|/
* Fixed crash after parse errorGravatar Rustan Leino2014-09-11
|
* Print system module (in a comment) with /rprint.Gravatar leino2014-09-09
| | | | Cleaner printing of .reads and .requires members of the built-in arrow "classes".
* Bounds discovery now takes newtype constraints into consideration.Gravatar leino2014-08-28
|
* Disallow parentheses-less declarations of predicates and co-predicates, ↵Gravatar leino2014-08-27
| | | | along with a backward-compatibility warning message if such declarations are attempted
* Merge, and refactored bit in Cloner into class ClonerButDropMethodBodies.Gravatar leino2014-08-27
|\
* | 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.
* | Various resolution fixes and improvementsGravatar leino2014-08-26
| | | | | | | | | | Added IsGoodHeap antecedent in (exists heap ...) in newtype Is axioms. Added IDE tool tips in newtype constraints.
* | Refactoring: renamed DerivedTypeDecl to NewtypeDeclGravatar leino2014-08-26
| |
* | Changed syntax of newtypeGravatar leino2014-08-26
| |
* | Fixed scoping to allow a datatype to have a constructor with the same name.Gravatar leino2014-08-26
| | | | | | | | Allow conversions to qualify type with module names.
* | Implemented arbitrary numeric conversions (but name resolution still needs ↵Gravatar leino2014-08-25
| | | | | | | | work when module names are involved)
* | Fixed bugs in previous check-inGravatar leino2014-08-25
| | | | | | | | Made up for inadequacy in reasoning machinery (supplying Int(Real(i)) == i axiom)
* | Check that result of newtype operations satisfy the newtype constraintGravatar leino2014-08-25
| |
* | Allow $Heap to occur in constraints (even though it isn't actually used)Gravatar leino2014-08-25
| |
| * changed $implements function argument type to ClassNameType (from Ty)Gravatar Reza Ahmadi2014-08-24
| |
* | Define $Is and $IsAlloc predicates for newtypes.Gravatar leino2014-08-24
| |
| * - generating TraitParent axiomsGravatar Reza Ahmadi2014-08-24
| | | | | | | | - $Is and $IsAlloc is no longer generated for a trait
* | Cycle detection among newtypes. Start of well-formedness check for newtypes.Gravatar leino2014-08-24
| |
| * MergeGravatar Dan Rosén2014-08-22
| |\ | |/ |/|
* | Type check and pretty print newtype constraintsGravatar leino2014-08-22
| |
* | Added .Trunc field to real-based typesGravatar leino2014-08-21
| | | | | | | | Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer
* | Changed syntax of derived types to "newtype"Gravatar leino2014-08-21
| | | | | | | | Added parsing of constraints (beyond parsing is yet to come)
* | 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.
| * Remove the cloner inside the ResolverGravatar Dan Rosén2014-08-21
| |
* | MergeGravatar leino2014-08-20
|\ \
* | | Start of derived types (aka "new types")Gravatar leino2014-08-20
| |/ |/| | | | | Fixed bug in type checking for integer division.
| * MergeGravatar Rustan Leino2014-08-19
| |\ | |/ |/|
| * Change behavior of 'decreases *', which can be applied to loops and methods. ↵Gravatar Rustan Leino2014-08-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now, loops that may possibly do an infinite number of iterations (that is, loops marked with 'decreases *') and calls to methods marked with 'decreases *' are allowed only in methods that themselves are marked with 'decreases *'. As before, ghost loops and ghost methods are not allowed to be marked with 'decreases *'. Previously, 'decreases *' was allowed on a method only if the method was tail recursive; this is no longer so. Note, however, that if the method is not tail recursive and engages in infinite recursion, then it will eventually run out of stack space. Previously, a 'decreases *' was not inherited in a refining module; this is no longer so. That is, 'decreases *' is now inherited. To refine a possibly non-terminating method or loop, the refining version simply provides a decreases clause that does not mention '*'. Note that if the refined method is not recursive, it still needs to have _some_ decreases clause in order not to inherit the 'decreases *' from the refined method, but the expression stated in the decreases clause can be arbitrary (for example, one can write 'decreases true' or 'decreases 7' or 'decreases x' for some 'x' in scope). Note, in the new design, a method needs to be declared with 'decreases *' if it may recurse forever _or_ if it contains a possibly infinite loop. Note that the absence of 'decreases *' on a loop does not mean the loop will terminate, but it does mean that the loop will iterate a finite number of times (the subtle distinction here is that a loop without a 'decreases *' is allowed to contain a nested loop that has a 'decreases *' -- provided the enclosing method is also declared with 'decreases *', as previously mentioned).
* | Handle underscores in lambda bound variable lists properlyGravatar Dan Rosén2014-08-19
|/ | | | + add a test case with lambdas that don't get their types fully specified
* Fix type inference bug in data rank comparison when one side can be a TypeVarGravatar Dan Rosén2014-08-19
|
* Consider lambdas literals + create literal axioms when an argument is a functionGravatar Dan Rosén2014-08-18
|
* Fix type equality for UserDefinedTypesGravatar Dan Rosén2014-08-15
|
* Refactor resolver, and really allow reads to take fields of type A -> set<obj>Gravatar Dan Rosén2014-08-15
| | | | twoState and codeContext is moved to a new class ResolveOpts
* Fix a performance issue regarding requires for top level function handlesGravatar Dan Rosén2014-08-14
|
* Make arrow types not look like reference types for the resolverGravatar Dan Rosén2014-08-14
|
* Optimise ApplyExpr to FunctionCallExpr when possible in translatorGravatar Dan Rosén2014-08-14
|
* Generate function handle requires for functions without a bodyGravatar Dan Rosén2014-08-14
|
* Reword error message for type error in lambda requires clauseGravatar Dan Rosén2014-08-14
|
* Fix bug in type substitution for type variablesGravatar Dan Rosén2014-08-14
|
* Allow reads to take fields of type A -> set<object>Gravatar Dan Rosén2014-08-14
|
* Refactor: Change ApplyExpr's Receiver to FunctionGravatar Dan Rosén2014-08-14
|
* Re-included lost calls to CheckEqualityTypes_TypeGravatar leino2014-08-13
| | | | Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate)
* MergeGravatar leino2014-08-13
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 04:37:00 +0000