From ac659e1ffa8d3f664daaa9f5394e007ca75cb3d1 Mon Sep 17 00:00:00 2001 From: chrishaw Date: Tue, 9 Dec 2014 14:36:12 -0800 Subject: Add nativeType attribute for newtype declarations. Change Compiler.cs to 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 --- Binaries/DafnyRuntime.cs | 129 +++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 119 insertions(+), 10 deletions(-) (limited to 'Binaries') diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 661666ef..a1d9037d 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -437,8 +437,11 @@ namespace Dafny public static Sequence FromString(string s) { return new Sequence(s.ToCharArray()); } - public BigInteger Length { - get { return new BigInteger(elmts.Length); } + public int Length { + get { return elmts.Length; } + } + public long LongLength { + get { return elmts.LongLength; } } public T[] Elements { get { @@ -451,14 +454,32 @@ namespace Dafny return st.Elements; } } + public T Select(ulong index) { + return elmts[index]; + } + public T Select(long index) { + return elmts[index]; + } + public T Select(uint index) { + return elmts[index]; + } + public T Select(int index) { + return elmts[index]; + } public T Select(BigInteger index) { return elmts[(int)index]; } - public Sequence Update(BigInteger index, T t) { + public Sequence Update(long index, T t) { T[] a = (T[])elmts.Clone(); - a[(int)index] = t; + a[index] = t; return new Sequence(a); } + public Sequence Update(ulong index, T t) { + return Update((long)index, t); + } + public Sequence Update(BigInteger index, T t) { + return Update((long)index, t); + } public bool Equals(Sequence other) { int n = elmts.Length; return n == other.elmts.Length && EqualUntil(other, n); @@ -519,22 +540,34 @@ namespace Dafny } return false; } - public Sequence Take(BigInteger n) { - int m = (int)n; - if (elmts.Length == m) + public Sequence Take(long m) { + if (elmts.LongLength == m) return this; T[] a = new T[m]; System.Array.Copy(elmts, a, m); return new Sequence(a); } - public Sequence Drop(BigInteger n) { - if (n.IsZero) + public Sequence Take(ulong n) { + return Take((long)n); + } + public Sequence Take(BigInteger n) { + return Take((long)n); + } + public Sequence Drop(long m) { + if (m == 0) return this; - int m = (int)n; T[] a = new T[elmts.Length - m]; System.Array.Copy(elmts, m, a, 0, elmts.Length - m); return new Sequence(a); } + public Sequence Drop(ulong n) { + return Drop((long)n); + } + public Sequence Drop(BigInteger n) { + if (n.IsZero) + return this; + return Drop((long)n); + } } public struct Pair { @@ -604,6 +637,50 @@ namespace Dafny } // pre: b != 0 // post: result == a/b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) + public static sbyte EuclideanDivision_sbyte(sbyte a, sbyte b) { + return (sbyte)EuclideanDivision(a, b); + } + public static short EuclideanDivision_short(short a, short b) { + return (short)EuclideanDivision(a, b); + } + public static int EuclideanDivision_int(int a, int b) { + if (0 <= a) { + if (0 <= b) { + // +a +b: a/b + return (int)(((uint)(a)) / ((uint)(b))); + } else { + // +a -b: -(a/(-b)) + return -((int)(((uint)(a)) / ((uint)(unchecked(-b))))); + } + } else { + if (0 <= b) { + // -a +b: -((-a-1)/b) - 1 + return -((int)(((uint)(-(a + 1))) / ((uint)(b)))) - 1; + } else { + // -a -b: ((-a-1)/(-b)) + 1 + return ((int)(((uint)(-(a + 1))) / ((uint)(unchecked(-b))))) + 1; + } + } + } + public static long EuclideanDivision_long(long a, long b) { + if (0 <= a) { + if (0 <= b) { + // +a +b: a/b + return (long)(((ulong)(a)) / ((ulong)(b))); + } else { + // +a -b: -(a/(-b)) + return -((long)(((ulong)(a)) / ((ulong)(unchecked(-b))))); + } + } else { + if (0 <= b) { + // -a +b: -((-a-1)/b) - 1 + return -((long)(((ulong)(-(a + 1))) / ((ulong)(b)))) - 1; + } else { + // -a -b: ((-a-1)/(-b)) + 1 + return ((long)(((ulong)(-(a + 1))) / ((ulong)(unchecked(-b))))) + 1; + } + } + } public static BigInteger EuclideanDivision(BigInteger a, BigInteger b) { if (0 <= a.Sign) { if (0 <= b.Sign) { @@ -625,6 +702,38 @@ namespace Dafny } // pre: b != 0 // post: result == a%b, as defined by Euclidean Division (http://en.wikipedia.org/wiki/Modulo_operation) + public static sbyte EuclideanModulus_sbyte(sbyte a, sbyte b) { + return (sbyte)EuclideanModulus(a, b); + } + public static short EuclideanModulus_short(short a, short b) { + return (short)EuclideanModulus(a, b); + } + public static int EuclideanModulus_int(int a, int b) { + uint bp = (0 <= b) ? (uint)b : (uint)(unchecked(-b)); + if (0 <= a) { + // +a: a % b' + return (int)(((uint)a) % bp); + } else { + // c = ((-a) % b') + // -a: b' - c if c > 0 + // -a: 0 if c == 0 + uint c = ((uint)(unchecked(-a))) % bp; + return (int)(c == 0 ? c : bp - c); + } + } + public static long EuclideanModulus_long(long a, long b) { + ulong bp = (0 <= b) ? (ulong)b : (ulong)(unchecked(-b)); + if (0 <= a) { + // +a: a % b' + return (long)(((ulong)a) % bp); + } else { + // c = ((-a) % b') + // -a: b' - c if c > 0 + // -a: 0 if c == 0 + ulong c = ((ulong)(unchecked(-a))) % bp; + return (long)(c == 0 ? c : bp - c); + } + } public static BigInteger EuclideanModulus(BigInteger a, BigInteger b) { var bp = BigInteger.Abs(b); if (0 <= a.Sign) { -- cgit v1.2.3