summaryrefslogtreecommitdiff
path: root/Binaries/DafnyRuntime.cs
Commit message (Collapse)AuthorAge
* Fix for soundness bug discovered in SeqFromArray.Gravatar Michael Lowell Roberts2015-09-17
|
* fix for comparison error in prelude when using /optimize.Gravatar Michael Lowell Roberts2015-08-31
|
* Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
|
* added -optimize option to compiler.Gravatar Michael Lowell Roberts2015-06-12
|
* HashCode for Set/MultiSet/Map should be independent of the order of theGravatar qunyanm2015-04-17
| | | | elements.
* Change GetHashCode for Set, MultiSet and MapGravatar qunyanm2015-04-16
|
* Fix issue #68. Change GetHashCode implementation for Sequence.Gravatar qunyanm2015-04-14
|
* Add LongLength methods to Set/Map in DafnyRuntime.csGravatar chrishaw2015-03-17
|
* Fix issue #60Gravatar qunyanm2015-03-06
|
* Optimization to nativeType: have EuclideanModulus_sbyte and ↵Gravatar chrishaw2014-12-11
| | | | EuclideanModulus_short call EuclideanModulus_int, not the BigInteger EuclideanModulus. (Same for EuclideanDivision.)
* Optimization to nativeType: have EuclideanDivision_sbyte and ↵Gravatar chrishaw2014-12-09
| | | | EuclideanDivision_short call EuclideanDivision_int, not the BigInteger EuclideanDivision. (Same for EuclideanModulus.)
* Add nativeType attribute for newtype declarations. Change Compiler.cs to ↵Gravatar chrishaw2014-12-09
| | | | | | | | | | | | | | | | | | | | | | | | use native C# representation of small integer newtypes. Examples: newtype{:nativeType "byte"} byte = i:int | 0 <= i < 0x100 newtype{:nativeType "sbyte"} sbyte = i:int | -0x80 <= i < 0x80 newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000 newtype{:nativeType "short"} int16 = i:int | -0x8000 <= i < 0x8000 newtype{:nativeType "uint"} uint32 = i:int | 0 <= i < 0x100000000 newtype{:nativeType "int"} int32 = i:int | -0x80000000 <= i < 0x80000000 newtype{:nativeType "ulong"} uint64 = i:int | 0 <= i < 0x10000000000000000 newtype{:nativeType "long"} int64 = i:int | -0x8000000000000000 <= i < 0x8000000000000000 newtype month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise BigInteger newtype{:nativeType} month = i:int | 0 <= i < 12 // same as {:nativeType true} newtype{:nativeType true} month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise error newtype{:nativeType false} month = i:int | 0 <= i < 12 // use BigInteger newtype{:nativeType "uint"} month = i:int | 0 <= i < 12 // use C# uint type if possible, otherwise error newtype{:nativeType} even20 = i:int | 0 <= i < 20 && (i % 2 == 0) // nativeTypes need not be contiguous newtype{:nativeType} even10 = i:even20 | i < 10 // nativeTypes can inherit constraints from other nativeTypes
* 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.
* Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
|
* Implemented missing routine in runtime system (real-to-int conversion)Gravatar leino2014-07-21
|
* Compile realsGravatar Rustan Leino2014-04-13
|
* 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
|/
* 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
* Fixed some build/migration issuesGravatar Rustan Leino2012-10-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 00:14:50 +0000