diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 79 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 23 |
2 files changed, 63 insertions, 39 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 646b16f1..a358e3c0 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -20,14 +20,14 @@ const null: ref; type Set T = [T]bool;
-function Set#Empty<T>() returns (Set T);
+function Set#Empty<T>(): Set T;
axiom (forall<T> o: T :: { Set#Empty()[o] } !Set#Empty()[o]);
-function Set#Singleton<T>(T) returns (Set T);
+function Set#Singleton<T>(T): Set T;
axiom (forall<T> r: T :: { Set#Singleton(r) } Set#Singleton(r)[r]);
axiom (forall<T> r: T, o: T :: { Set#Singleton(r)[o] } Set#Singleton(r)[o] <==> r == o);
-function Set#UnionOne<T>(Set T, T) returns (Set T);
+function Set#UnionOne<T>(Set T, T): Set T;
axiom (forall<T> a: Set T, x: T, o: T :: { Set#UnionOne(a,x)[o] }
Set#UnionOne(a,x)[o] <==> o == x || a[o]);
axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) }
@@ -35,7 +35,7 @@ axiom (forall<T> a: Set T, x: T :: { Set#UnionOne(a, x) } axiom (forall<T> a: Set T, x: T, y: T :: { Set#UnionOne(a, x), a[y] }
a[y] ==> Set#UnionOne(a, x)[y]);
-function Set#Union<T>(Set T, Set T) returns (Set T);
+function Set#Union<T>(Set T, Set T): Set T;
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Union(a,b)[o] }
Set#Union(a,b)[o] <==> a[o] || b[o]);
axiom (forall<T> a, b: Set T, y: T :: { Set#Union(a, b), a[y] }
@@ -47,7 +47,7 @@ axiom (forall<T> a, b: Set T :: { Set#Union(a, b) } Set#Difference(Set#Union(a, b), a) == b &&
Set#Difference(Set#Union(a, b), b) == a);
-function Set#Intersection<T>(Set T, Set T) returns (Set T);
+function Set#Intersection<T>(Set T, Set T): Set T;
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }
Set#Intersection(a,b)[o] <==> a[o] && b[o]);
@@ -60,27 +60,27 @@ axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) } axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }
Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));
-function Set#Difference<T>(Set T, Set T) returns (Set T);
+function Set#Difference<T>(Set T, Set T): Set T;
axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }
Set#Difference(a,b)[o] <==> a[o] && !b[o]);
axiom (forall<T> a, b: Set T, y: T :: { Set#Difference(a, b), b[y] }
b[y] ==> !Set#Difference(a, b)[y] );
-function Set#Subset<T>(Set T, Set T) returns (bool);
+function Set#Subset<T>(Set T, Set T): bool;
axiom(forall<T> a: Set T, b: Set T :: { Set#Subset(a,b) }
Set#Subset(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] ==> b[o]));
-function Set#Equal<T>(Set T, Set T) returns (bool);
+function Set#Equal<T>(Set T, Set T): bool;
axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) }
Set#Equal(a,b) <==> (forall o: T :: {a[o]} {b[o]} a[o] <==> b[o]));
axiom(forall<T> a: Set T, b: Set T :: { Set#Equal(a,b) } // extensionality axiom for sets
Set#Equal(a,b) ==> a == b);
-function Set#Disjoint<T>(Set T, Set T) returns (bool);
+function Set#Disjoint<T>(Set T, Set T): bool;
axiom (forall<T> a: Set T, b: Set T :: { Set#Disjoint(a,b) }
Set#Disjoint(a,b) <==> (forall o: T :: {a[o]} {b[o]} !a[o] || !b[o]));
-function Set#Choose<T>(Set T, TickType) returns (T);
+function Set#Choose<T>(Set T, TickType): T;
axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) }
a != Set#Empty() ==> a[Set#Choose(a, tick)]);
@@ -90,25 +90,25 @@ axiom (forall<T> a: Set T, tick: TickType :: { Set#Choose(a, tick) } type Seq T;
-function Seq#Length<T>(Seq T) returns (int);
+function Seq#Length<T>(Seq T): int;
axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
-function Seq#Empty<T>() returns (Seq T);
+function Seq#Empty<T>(): Seq T;
axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());
-function Seq#Singleton<T>(T) returns (Seq T);
+function Seq#Singleton<T>(T): Seq T;
axiom (forall<T> t: T :: { Seq#Length(Seq#Singleton(t)) } Seq#Length(Seq#Singleton(t)) == 1);
-function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int) returns (Seq T);
+function Seq#Build<T>(s: Seq T, index: int, val: T, newLength: int): Seq T;
axiom (forall<T> s: Seq T, i: int, v: T, len: int :: { Seq#Length(Seq#Build(s,i,v,len)) }
0 <= len ==> Seq#Length(Seq#Build(s,i,v,len)) == len);
-function Seq#Append<T>(Seq T, Seq T) returns (Seq T);
+function Seq#Append<T>(Seq T, Seq T): Seq T;
axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }
Seq#Length(Seq#Append(s0,s1)) == Seq#Length(s0) + Seq#Length(s1));
-function Seq#Index<T>(Seq T, int) returns (T);
+function Seq#Index<T>(Seq T, int): T;
axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Singleton(t), 0) == t);
axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#Index(Seq#Append(s0,s1), n) }
(n < Seq#Length(s0) ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s0, n)) &&
@@ -118,7 +118,7 @@ axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Bui (i == n ==> Seq#Index(Seq#Build(s,i,v,len),n) == v) &&
(i != n ==> Seq#Index(Seq#Build(s,i,v,len),n) == Seq#Index(s,n)));
-function Seq#Update<T>(Seq T, int, T) returns (Seq T);
+function Seq#Update<T>(Seq T, int, T): Seq T;
axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }
0 <= i && i < Seq#Length(s) ==> Seq#Length(Seq#Update(s,i,v)) == Seq#Length(s));
axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v),n) }
@@ -126,7 +126,7 @@ axiom (forall<T> s: Seq T, i: int, v: T, n: int :: { Seq#Index(Seq#Update(s,i,v) (i == n ==> Seq#Index(Seq#Update(s,i,v),n) == v) &&
(i != n ==> Seq#Index(Seq#Update(s,i,v),n) == Seq#Index(s,n)));
-function Seq#Contains<T>(Seq T, T) returns (bool);
+function Seq#Contains<T>(Seq T, T): bool;
axiom (forall<T> s: Seq T, x: T :: { Seq#Contains(s,x) }
Seq#Contains(s,x) <==>
(exists i: int :: { Seq#Index(s,i) } 0 <= i && i < Seq#Length(s) && Seq#Index(s,i) == x));
@@ -153,22 +153,22 @@ axiom (forall<T> s: Seq T, n: int, x: T :: (exists i: int :: { Seq#Index(s, i) }
0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
-function Seq#Equal<T>(Seq T, Seq T) returns (bool);
+function Seq#Equal<T>(Seq T, Seq T): bool;
axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Equal(s0,s1) }
Seq#Equal(s0,s1) <==>
Seq#Length(s0) == Seq#Length(s1) &&
(forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
0 <= j && j < Seq#Length(s0) ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
-axiom(forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences
+axiom (forall<T> a: Seq T, b: Seq T :: { Seq#Equal(a,b) } // extensionality axiom for sequences
Seq#Equal(a,b) ==> a == b);
-function Seq#SameUntil<T>(Seq T, Seq T, int) returns (bool);
+function Seq#SameUntil<T>(Seq T, Seq T, int): bool;
axiom (forall<T> s0: Seq T, s1: Seq T, n: int :: { Seq#SameUntil(s0,s1,n) }
Seq#SameUntil(s0,s1,n) <==>
(forall j: int :: { Seq#Index(s0,j) } { Seq#Index(s1,j) }
0 <= j && j < n ==> Seq#Index(s0,j) == Seq#Index(s1,j)));
-function Seq#Take<T>(s: Seq T, howMany: int) returns (Seq T);
+function Seq#Take<T>(s: Seq T, howMany: int): Seq T;
axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Take(s,n)) }
0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Take(s,n)) == n) &&
@@ -177,7 +177,7 @@ axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Take(s,n), j) } {:w 0 <= j && j < n && j < Seq#Length(s) ==>
Seq#Index(Seq#Take(s,n), j) == Seq#Index(s, j));
-function Seq#Drop<T>(s: Seq T, howMany: int) returns (Seq T);
+function Seq#Drop<T>(s: Seq T, howMany: int): Seq T;
axiom (forall<T> s: Seq T, n: int :: { Seq#Length(Seq#Drop(s,n)) }
0 <= n ==>
(n <= Seq#Length(s) ==> Seq#Length(Seq#Drop(s,n)) == Seq#Length(s) - n) &&
@@ -197,8 +197,8 @@ axiom (forall<T> s, t: Seq T :: type BoxType;
-function $Box<T>(T) returns (BoxType);
-function $Unbox<T>(BoxType) returns (T);
+function $Box<T>(T): BoxType;
+function $Unbox<T>(BoxType): T;
axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);
axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);
@@ -206,7 +206,10 @@ axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b); axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);
axiom (forall b: BoxType :: { $Unbox(b): DatatypeType } $Box($Unbox(b): DatatypeType) == b);
-// note: an axiom like this for bool would not be sound
+// Note: an axiom like this for bool would not be sound; instead, we do:
+function $IsCanonicalBoolBox(BoxType): bool;
+axiom $IsCanonicalBoolBox($Box(false)) && $IsCanonicalBoolBox($Box(true));
+axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box($Unbox(b): bool) == b);
// ---------------------------------------------------------------
// -- Encoding of type names -------------------------------------
@@ -218,12 +221,12 @@ const unique class.bool: ClassName; const unique class.set: ClassName;
const unique class.seq: ClassName;
-function /*{:never_pattern true}*/ dtype(ref) returns (ClassName);
-function /*{:never_pattern true}*/ TypeParams(ref, int) returns (ClassName);
+function /*{:never_pattern true}*/ dtype(ref): ClassName;
+function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;
-function TypeTuple(a: ClassName, b: ClassName) returns (ClassName);
-function TypeTupleCar(ClassName) returns (ClassName);
-function TypeTupleCdr(ClassName) returns (ClassName);
+function TypeTuple(a: ClassName, b: ClassName): ClassName;
+function TypeTupleCar(ClassName): ClassName;
+function TypeTupleCdr(ClassName): ClassName;
// TypeTuple is injective in both arguments:
axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
TypeTupleCar(TypeTuple(a,b)) == a &&
@@ -235,13 +238,13 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) } type DatatypeType;
-function /*{:never_pattern true}*/ DtType(DatatypeType) returns (ClassName); // the analog of dtype for datatype values
-function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int) returns (ClassName); // the analog of TypeParams
+function /*{:never_pattern true}*/ DtType(DatatypeType): ClassName; // the analog of dtype for datatype values
+function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int): ClassName; // the analog of TypeParams
type DtCtorId;
-function DatatypeCtorId(DatatypeType) returns (DtCtorId);
+function DatatypeCtorId(DatatypeType): DtCtorId;
-function DtRank(DatatypeType) returns (int);
+function DtRank(DatatypeType): int;
// ---------------------------------------------------------------
// -- Axiom contexts ---------------------------------------------
@@ -274,7 +277,7 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } MultiIndexField_Inverse1(MultiIndexField(f,i)) == i);
-function DeclType<T>(Field T) returns (ClassName);
+function DeclType<T>(Field T): ClassName;
// ---------------------------------------------------------------
// -- Allocatedness ----------------------------------------------
@@ -339,10 +342,10 @@ type HeapType = <alpha>[ref,Field alpha]alpha; function {:inline true} read<alpha>(H:HeapType, r:ref, f:Field alpha): alpha { H[r, f] }
function {:inline true} update<alpha>(H:HeapType, r:ref, f:Field alpha, v:alpha): HeapType { H[r,f := v] }
-function $IsGoodHeap(HeapType) returns (bool);
+function $IsGoodHeap(HeapType): bool;
var $Heap: HeapType where $IsGoodHeap($Heap);
-function $HeapSucc(HeapType, HeapType) returns (bool);
+function $HeapSucc(HeapType, HeapType): bool;
axiom (forall<alpha> h: HeapType, r: ref, f: Field alpha, x: alpha :: { update(h, r, f, x) }
$HeapSucc(h, update(h, r, f, x)));
axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 253a1f9b..67559aee 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3676,11 +3676,15 @@ namespace Microsoft.Dafny { Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);
Bpl.Expr unbox = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? xSubI : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), xSubI);
+ Bpl.Expr c = GetBoolBoxCondition(xSubI, st.Arg);
Bpl.Expr wh = GetWhereClause(tok, unbox, st.Arg, etran);
if (wh != null) {
+ c = BplAnd(c, wh);
+ }
+ if (c != Bpl.Expr.True) {
Bpl.Expr range = InSeqRange(tok, i, x, true, null, false);
Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubI));
- return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.Imp(range, wh));
+ return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.Imp(range, c));
}
} else if (type.IsRefType) {
@@ -3706,6 +3710,18 @@ namespace Microsoft.Dafny { return null;
}
+ Bpl.Expr GetBoolBoxCondition(Expr box, Type type) {
+ Contract.Requires(box != null);
+ Contract.Requires(type != null);
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ if (type is BoolType) {
+ return FunctionCall(box.tok, BuiltinFunction.IsCanonicalBoolBox, null, box);
+ } else {
+ return Bpl.Expr.True;
+ }
+ }
+
void TrAssignment(IToken tok, Expression lhs, AssignmentRhs rhs, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals,
ExpressionTranslator etran)
{
@@ -4826,6 +4842,7 @@ namespace Microsoft.Dafny { Box,
Unbox,
+ IsCanonicalBoolBox,
IsGoodHeap,
HeapSucc,
@@ -4957,6 +4974,10 @@ namespace Microsoft.Dafny { Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation != null);
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "$Unbox", typeInstantiation, args), typeInstantiation);
+ case BuiltinFunction.IsCanonicalBoolBox:
+ Contract.Assert(args.Length == 1);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "$IsCanonicalBoolBox", Bpl.Type.Bool, args);
case BuiltinFunction.IsGoodHeap:
Contract.Assert(args.Length == 1);
|