Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix type inference bug in data rank comparison when one side can be a TypeVar | Dan Rosén | 2014-08-19 |
| | |||
* | Consider lambdas literals + create literal axioms when an argument is a function | Dan Rosén | 2014-08-18 |
| | |||
* | Add Monads as a module example and implementation of some simple monads | Dan Rosén | 2014-08-15 |
| | |||
* | Refactor resolver, and really allow reads to take fields of type A -> set<obj> | Dan Rosén | 2014-08-15 |
| | | | | twoState and codeContext is moved to a new class ResolveOpts | ||
* | Add the VectorUpdate example | Dan Rosén | 2014-08-14 |
| | |||
* | Make arrow types not look like reference types for the resolver | Dan Rosén | 2014-08-14 |
| | |||
* | Reword error message for type error in lambda requires clause | Dan Rosén | 2014-08-14 |
| | |||
* | Add lambda compilation example, and remove some unused files from the tests | Dan Rosén | 2014-08-13 |
| | |||
* | Re-included lost calls to CheckEqualityTypes_Type | leino | 2014-08-13 |
| | | | | Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate) | ||
* | Merge | leino | 2014-08-13 |
|\ | |||
* | | Check for proper use of equality-supporting types also in local variables ↵ | leino | 2014-08-13 |
| | | | | | | | | and forall statements, and more expressions | ||
| * | Rewrote two tests to make triggering better (while waiting for better ↵ | Rustan Leino | 2014-08-12 |
| | | | | | | | | automatic triggering support in either Dafny or Boogie) | ||
| * | Compile lambda functions and apply expressions, and change let expr compilation | Dan Rosén | 2014-08-12 |
| | | |||
| * | Merge | Dan Rosén | 2014-08-11 |
| |\ | |/ |/| | |||
| * | Add higher-order-functions and some other goodies | Dan Rosén | 2014-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 | ||
* | | Merge | leino | 2014-08-05 |
|\ \ | |||
* | | | Resolved further merge issues | leino | 2014-08-05 |
| | | | |||
| * | | Tests for non-terminating computations. Already passing. | Nada Amin | 2014-08-05 |
| | | | |||
* | | | Merge | leino | 2014-08-02 |
|\| | | |||
* | | | Fixed bug Issue 37: expand type synonyms in more (hopefully all) places in ↵ | leino | 2014-08-02 |
| | | | | | | | | | | | | the resolver and translator | ||
| * | | added one more test case | Reza Ahmadi | 2014-07-31 |
| | | | |||
| * | | combined few tests | Reza Ahmadi | 2014-07-31 |
| | | | |||
| * | | combined two tests | Reza Ahmadi | 2014-07-31 |
| | | | |||
| * | | Merge | Reza Ahmadi | 2014-07-31 |
| |\ \ | |||
| | * | | Changed test case to not use '/doNotUseParallelism' anymore. | wuestholz | 2014-07-31 |
| | |/ | |||
* | / | Test file whitespace delta | leino | 2014-07-23 |
| |/ |/| | |||
| * | added one more test. | Reza Ahmadi | 2014-07-20 |
| | | |||
| * | - fixed a bug in inheriting members from a trait | Reza Ahmadi | 2014-07-20 |
| | | | | | | | | | | | | | | => ResolvedClass in userdefinedtypes used to be null-> fixed - checking only bodyless methods and functions to make sure they have been implemented in the child class - added one more test | ||
| * | fixed one .expect file. now all 11 tests related to Traits pass. | Reza Ahmadi | 2014-07-20 |
| | | |||
| * | - fixed an issue regarding including ghost functions in the compiled interface | Reza Ahmadi | 2014-07-20 |
| | | | | | | | | - added one more test | ||
| * | added trait feature: | Reza Ahmadi | 2014-07-18 |
|/ | | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods | ||
* | An attempt at making dafny4/NumberRepresentations.dfy run faster and more ↵ | Rustan Leino | 2014-07-15 |
| | | | | predictably | ||
* | Renamed "arbitrary type" to "opaque type" | Rustan Leino | 2014-07-15 |
| | |||
* | Allow an arbitrary-type to take type parameters | Rustan Leino | 2014-07-15 |
| | |||
* | Added more tests. | wuestholz | 2014-07-15 |
| | |||
* | Another variation of GenericSort, this time instantiating with "int" | Rustan Leino | 2014-07-14 |
| | |||
* | Merge | Rustan Leino | 2014-07-14 |
|\ | |||
* | | Support for type synonyms in refinements | Rustan Leino | 2014-07-14 |
| | | | | | | | | Started allowing arbitrary types to have type parameters | ||
| * | Added a test. | wuestholz | 2014-07-13 |
|/ | |||
* | Merge | Rustan Leino | 2014-07-11 |
|\ | |||
* | | Added type synonyms. (No support yet for these in refinements.) | Rustan Leino | 2014-07-11 |
| | | |||
| * | Check that type arguments to map display expressions are fully resolved | Dan Rosén | 2014-07-11 |
|/ | | | | Also add a test case for the different display expressions. | ||
* | Make reveal axioms from opaque functions quantify over layers | Dan Rosén | 2014-07-10 |
| | |||
* | Added more tests for the more advanced verification result caching. | wuestholz | 2014-07-10 |
| | |||
* | Merge | Rustan Leino | 2014-07-09 |
|\ | |||
* | | Improved AnalyzeList encoding in a way that performs way better. | Rustan Leino | 2014-07-09 |
| | | | | | | | | Cleaned up file to use some improved Dafny constructs. | ||
* | | Include an explicit trigger to make NumberRepresentations.dfy behave more ↵ | Rustan Leino | 2014-07-09 |
| | | | | | | | | consistently. (There is a future opportunity to heuristically figure out such triggers.) | ||
| * | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 |
|/ | |||
* | Further resolved merge conflicts | Rustan Leino | 2014-07-08 |
| | |||
* | Merge | Rustan Leino | 2014-07-08 |
|\ |