summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Binaries/DafnyPrelude.bpl56
-rw-r--r--Source/Dafny/Resolver.cs75
-rw-r--r--Source/Dafny/Translator.cs48
-rw-r--r--Test/dafny0/AdvancedLHS.dfy1
-rw-r--r--Test/dafny0/Array.dfy35
5 files changed, 117 insertions, 98 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index e11acf26..37b972d0 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -131,6 +131,8 @@ function MultiSet#Union<T>(MultiSet T, MultiSet T): MultiSet T;
// union-ing is the sum of the contents
axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Union(a,b)[o] }
MultiSet#Union(a,b)[o] == a[o] + b[o]);
+axiom (forall<T> a: MultiSet T, b: MultiSet T :: { MultiSet#Union(a,b) }
+ MultiSet#Union(a,b) == MultiSet#Union(b,a));
// two containment axioms
axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), a[y] }
@@ -140,9 +142,8 @@ axiom (forall<T> a, b: MultiSet T, y: T :: { MultiSet#Union(a, b), b[y] }
// symmetry axiom
axiom (forall<T> a, b: MultiSet T :: { MultiSet#Union(a, b) }
- MultiSet#Disjoint(a, b) ==>
- MultiSet#Difference(MultiSet#Union(a, b), a) == b &&
- MultiSet#Difference(MultiSet#Union(a, b), b) == a);
+ MultiSet#Difference(MultiSet#Union(a, b), a) == b &&
+ MultiSet#Difference(MultiSet#Union(a, b), b) == a);
function MultiSet#Intersection<T>(MultiSet T, MultiSet T): MultiSet T;
axiom (forall<T> a: MultiSet T, b: MultiSet T, o: T :: { MultiSet#Intersection(a,b)[o] }
@@ -183,9 +184,17 @@ axiom (forall<T> s: Set T, a: T :: { MultiSet#FromSet(s)[a] }
(MultiSet#FromSet(s)[a] == 0 <==> !s[a]) &&
(MultiSet#FromSet(s)[a] == 1 <==> s[a]));
-// conversion to a multiset. each element in the original set has duplicity 1.
+// conversion to a multiset, from a sequence.
function MultiSet#FromSeq<T>(Seq T): MultiSet T;
-// no axioms yet.
+axiom (forall<T> s: Seq T, v: T ::
+ { MultiSet#FromSeq(Seq#Build(s, v)) }
+ MultiSet#FromSeq(Seq#Build(s, v)) == MultiSet#UnionOne(MultiSet#FromSeq(s), v)
+ );
+axiom (MultiSet#FromSeq(Seq#Empty(): Seq BoxType) == MultiSet#Empty());
+axiom (forall<T> a: Seq T, b: Seq T ::
+ { MultiSet#FromSeq(Seq#Append(a, b)) }
+ MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(a), MultiSet#FromSeq(b)) &&
+ MultiSet#FromSeq(Seq#Append(a, b)) == MultiSet#Union(MultiSet#FromSeq(b), MultiSet#FromSeq(a)));
// ---------------------------------------------------------------
// -- Axiomatization of sequences --------------------------------
@@ -203,9 +212,12 @@ axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#E
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): 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#Build<T>(s: Seq T, val: T): Seq T;
+axiom (forall<T> s: Seq T, v: T :: { Seq#Length(Seq#Build(s,v)) }
+ Seq#Length(Seq#Build(s,v)) == 1 + Seq#Length(s));
+axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Index(Seq#Build(s,v), i) }
+ (i == Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == v) &&
+ (i != Seq#Length(s) ==> Seq#Index(Seq#Build(s,v), i) == Seq#Index(s, i)));
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)) }
@@ -216,10 +228,6 @@ axiom (forall<T> t: T :: { Seq#Index(Seq#Singleton(t), 0) } Seq#Index(Seq#Single
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)) &&
(Seq#Length(s0) <= n ==> Seq#Index(Seq#Append(s0,s1), n) == Seq#Index(s1, n - Seq#Length(s0))));
-axiom (forall<T> s: Seq T, i: int, v: T, len: int, n: int :: { Seq#Index(Seq#Build(s,i,v,len),n) }
- 0 <= n && n < len ==>
- (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): Seq T;
axiom (forall<T> s: Seq T, i: int, v: T :: { Seq#Length(Seq#Update(s,i,v)) }
@@ -240,16 +248,11 @@ axiom (forall<T> s0: Seq T, s1: Seq T, x: T ::
{ Seq#Contains(Seq#Append(s0, s1), x) }
Seq#Contains(Seq#Append(s0, s1), x) <==>
Seq#Contains(s0, x) || Seq#Contains(s1, x));
-axiom (forall<T> i: int, v: T, len: int, x: T ::
- { Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) }
- 0 <= i && i < len ==>
- (Seq#Contains(Seq#Build(Seq#Empty(), i, v, len), x) <==> x == v));
-axiom (forall<T> s: Seq T, i0: int, v0: T, len0: int, i1: int, v1: T, len1: int, x: T ::
- { Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) }
- 0 <= i0 && i0 < len0 && len0 <= i1 && i1 < len1 ==>
- (Seq#Contains(Seq#Build(Seq#Build(s, i0, v0, len0), i1, v1, len1), x) <==>
- v1 == x ||
- Seq#Contains(Seq#Build(s, i0, v0, len0), x)));
+
+axiom (forall<T> s: Seq T, v: T, x: T ::
+ { Seq#Contains(Seq#Build(s, v), x) }
+ Seq#Contains(Seq#Build(s, v), x) <==> (v == x || Seq#Contains(s, x)));
+
axiom (forall<T> s: Seq T, n: int, x: T ::
{ Seq#Contains(Seq#Take(s, n), x) }
Seq#Contains(Seq#Take(s, n), x) <==>
@@ -299,6 +302,11 @@ axiom (forall<T> s, t: Seq T ::
Seq#Take(Seq#Append(s, t), Seq#Length(s)) == s &&
Seq#Drop(Seq#Append(s, t), Seq#Length(s)) == t);
+function Seq#FromArray(h: HeapType, a: ref): Seq BoxType;
+axiom (forall h: HeapType, a: ref :: { Seq#Length(Seq#FromArray(h,a)) } Seq#Length(Seq#FromArray(h, a)) == array.Length(a));
+axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType }
+ (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
+
// ---------------------------------------------------------------
// -- Boxing and unboxing ----------------------------------------
// ---------------------------------------------------------------
@@ -328,6 +336,7 @@ const unique class.int: ClassName;
const unique class.bool: ClassName;
const unique class.set: ClassName;
const unique class.seq: ClassName;
+const unique class.multiset: ClassName;
function /*{:never_pattern true}*/ dtype(ref): ClassName;
function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;
@@ -435,6 +444,9 @@ axiom (forall r: ref, h: HeapType ::
// -- Arrays -----------------------------------------------------
// ---------------------------------------------------------------
+function array.Length(a: ref): int;
+axiom (forall o: ref :: 0 <= array.Length(o));
+
procedure UpdateArrayRange(arr: ref, low: int, high: int, rhs: BoxType);
modifies $Heap;
ensures $HeapSucc(old($Heap), $Heap);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 2b3128ae..1321a987 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1304,15 +1304,14 @@ namespace Microsoft.Dafny {
// LHS is fine, provided the "sequence" is really an array
if (lhsResolvedSuccessfully) {
Contract.Assert(slhs.Seq.Type != null);
- Type elementType = new InferredTypeProxy();
- if (!UnifyTypes(slhs.Seq.Type, builtIns.ArrayType(1, elementType))) {
+ if (!UnifyTypes(slhs.Seq.Type, builtIns.ArrayType(1, new InferredTypeProxy()))) {
Error(slhs.Seq, "LHS of array assignment must denote an array element (found {0})", slhs.Seq.Type);
}
if (specContextOnly) {
Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
}
- if (!slhs.SelectOne && !(s.Rhs is ExprRhs)) {
- Error(stmt, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");
+ if (!slhs.SelectOne) {
+ Error(stmt, "cannot assign to multiple array elements (try a foreach).");
}
}
@@ -1328,43 +1327,43 @@ namespace Microsoft.Dafny {
s.IsGhost = lvalueIsGhost;
Type lhsType = s.Lhs.Type;
if (lhs is SeqSelectExpr && !((SeqSelectExpr)lhs).SelectOne) {
- Contract.Assert(lhsType.IsArrayType);
- lhsType = UserDefinedType.ArrayElementType(lhsType);
- }
- if (s.Rhs is ExprRhs) {
- ExprRhs rr = (ExprRhs)s.Rhs;
- ResolveExpression(rr.Expr, true);
- if (!lvalueIsGhost) {
- CheckIsNonGhost(rr.Expr);
- }
- Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(lhsType, rr.Expr.Type)) {
- Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);
- }
- } else if (s.Rhs is TypeRhs) {
- TypeRhs rr = (TypeRhs)s.Rhs;
- Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, method);
- if (!lvalueIsGhost) {
- if (rr.ArrayDimensions != null) {
- foreach (var dim in rr.ArrayDimensions) {
- CheckIsNonGhost(dim);
- }
+ Error(stmt, "cannot assign to multiple array elements (try a foreach).");
+ //lhsType = UserDefinedType.ArrayElementType(lhsType);
+ } else {
+ if (s.Rhs is ExprRhs) {
+ ExprRhs rr = (ExprRhs)s.Rhs;
+ ResolveExpression(rr.Expr, true);
+ if (!lvalueIsGhost) {
+ CheckIsNonGhost(rr.Expr);
}
- if (rr.InitCall != null) {
- foreach (var arg in rr.InitCall.Args) {
- CheckIsNonGhost(arg);
+ Contract.Assert(rr.Expr.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(lhsType, rr.Expr.Type)) {
+ Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, lhsType);
+ }
+ } else if (s.Rhs is TypeRhs) {
+ TypeRhs rr = (TypeRhs)s.Rhs;
+ Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, method);
+ if (!lvalueIsGhost) {
+ if (rr.ArrayDimensions != null) {
+ foreach (var dim in rr.ArrayDimensions) {
+ CheckIsNonGhost(dim);
+ }
+ }
+ if (rr.InitCall != null) {
+ foreach (var arg in rr.InitCall.Args) {
+ CheckIsNonGhost(arg);
+ }
}
}
+ if (!UnifyTypes(lhsType, t)) {
+ Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);
+ }
+ } else if (s.Rhs is HavocRhs) {
+ // nothing else to do
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS
}
- if (!UnifyTypes(lhsType, t)) {
- Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, lhsType);
- }
- } else if (s.Rhs is HavocRhs) {
- // nothing else to do
- } else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected RHS
}
-
} else if (stmt is VarDecl) {
VarDecl s = (VarDecl)stmt;
if (s.OptionalType != null) {
@@ -2340,7 +2339,7 @@ namespace Microsoft.Dafny {
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- ResolveSeqSelectExpr(e, twoState, false);
+ ResolveSeqSelectExpr(e, twoState, true);
} else if (expr is MultiSelectExpr) {
MultiSelectExpr e = (MultiSelectExpr)expr;
@@ -3554,7 +3553,7 @@ namespace Microsoft.Dafny {
if (e.SelectOne) {
e.Type = elementType;
} else {
- e.Type = e.Seq.Type;
+ e.Type = new SeqType(elementType);
}
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index dacbf143..60a40f57 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -44,6 +44,7 @@ namespace Microsoft.Dafny {
public readonly Bpl.Type TickType;
private readonly Bpl.TypeSynonymDecl setTypeCtor;
private readonly Bpl.TypeSynonymDecl multiSetTypeCtor;
+ public readonly Bpl.Function ArrayLength;
private readonly Bpl.TypeCtorDecl seqTypeCtor;
readonly Bpl.TypeCtorDecl fieldName;
public readonly Bpl.Type HeapType;
@@ -60,6 +61,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(TickType != null);
Contract.Invariant(setTypeCtor != null);
Contract.Invariant(multiSetTypeCtor != null);
+ Contract.Invariant(ArrayLength != null);
Contract.Invariant(seqTypeCtor != null);
Contract.Invariant(fieldName != null);
Contract.Invariant(HeapType != null);
@@ -111,7 +113,7 @@ namespace Microsoft.Dafny {
}
public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
- Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
+ Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField) {
@@ -136,6 +138,7 @@ namespace Microsoft.Dafny {
this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new Bpl.TypeSeq());
this.setTypeCtor = setTypeCtor;
this.multiSetTypeCtor = multiSetTypeCtor;
+ this.ArrayLength = arrayLength;
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
this.HeapType = heap.TypedIdent.Type;
@@ -158,6 +161,7 @@ namespace Microsoft.Dafny {
Bpl.TypeCtorDecl refType = null;
Bpl.TypeSynonymDecl setTypeCtor = null;
Bpl.TypeSynonymDecl multiSetTypeCtor = null;
+ Bpl.Function arrayLength = null;
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
@@ -167,7 +171,7 @@ namespace Microsoft.Dafny {
Bpl.TypeCtorDecl tickType = null;
Bpl.GlobalVariable heap = null;
Bpl.Constant allocField = null;
- foreach (Bpl.Declaration d in prog.TopLevelDeclarations) {
+ foreach (var d in prog.TopLevelDeclarations) {
if (d is Bpl.TypeCtorDecl) {
Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;
if (dt.Name == "Seq") {
@@ -205,6 +209,10 @@ namespace Microsoft.Dafny {
if (v.Name == "$Heap") {
heap = v;
}
+ } else if (d is Bpl.Function) {
+ var f = (Bpl.Function)d;
+ if (f.Name == "array.Length")
+ arrayLength = f;
}
}
if (seqTypeCtor == null) {
@@ -213,6 +221,8 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Set");
} else if (multiSetTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet");
+ } else if (arrayLength == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of function array.Length");
} else if (fieldNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
@@ -233,7 +243,7 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
} else {
return new PredefinedDecls(refType, boxType, tickType,
- setTypeCtor, multiSetTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
+ setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
allocField);
}
return null;
@@ -506,7 +516,8 @@ namespace Microsoft.Dafny {
sink.TopLevelDeclarations.Add(fc);
} else {
Bpl.Function ff = GetReadonlyField(f);
- sink.TopLevelDeclarations.Add(ff);
+ if (ff != predef.ArrayLength)
+ sink.TopLevelDeclarations.Add(ff);
}
AddAllocationAxiom(f);
@@ -1656,7 +1667,7 @@ namespace Microsoft.Dafny {
}
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
- bool isSequence = e.Seq.Type is SeqType;
+ //bool isSequence = e.Seq.Type is SeqType;
Bpl.Expr total = CanCallAssumption(e.Seq, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
Bpl.Expr e0 = null;
@@ -2396,7 +2407,7 @@ namespace Microsoft.Dafny {
if (a == null) {
return null;
}
- Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too.
+ Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : (ct is SeqType ? "class.seq" : "class.multiset"), predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too.
return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
} else {
UserDefinedType ct = (UserDefinedType)type;
@@ -2448,6 +2459,10 @@ namespace Microsoft.Dafny {
if (fieldFunctions.TryGetValue(f, out ff)) {
Contract.Assert(ff != null);
} else {
+ if (f.EnclosingClass is ArrayClassDecl && f.Name == "Length") { // link directly to the function in the prelude.
+ fieldFunctions.Add(f, predef.ArrayLength);
+ return predef.ArrayLength;
+ }
// function f(Ref): ty;
Bpl.Type ty = TrType(f.Type);
Bpl.VariableSeq args = new Bpl.VariableSeq();
@@ -4680,7 +4695,7 @@ namespace Microsoft.Dafny {
}
return s;
- } else if (expr is MultiSetDisplayExpr) { //^^^ todo: add multiset to BuiltinFunction
+ } else if (expr is MultiSetDisplayExpr) {
MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEmpty, predef.BoxType);
foreach (Expression ee in e.Elements) {
@@ -4694,8 +4709,8 @@ namespace Microsoft.Dafny {
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
int i = 0;
foreach (Expression ee in e.Elements) {
- Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));
- s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, Bpl.Expr.Literal(i), ss, Bpl.Expr.Literal(i+1));
+ Bpl.Expr elt = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));
+ s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqBuild, predef.BoxType, s, elt);
i++;
}
return s;
@@ -4711,14 +4726,13 @@ namespace Microsoft.Dafny {
result = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(translator.GetReadonlyField(e.Field)), new Bpl.ExprSeq(obj));
}
return CondApplyUnbox(expr.tok, result, e.Field.Type, cce.NonNull(expr.Type));
-
+
} else if (expr is SeqSelectExpr) {
SeqSelectExpr e = (SeqSelectExpr)expr;
Bpl.Expr seq = TrExpr(e.Seq);
Type elmtType;
Contract.Assert(e.Seq.Type != null); // the expression has been successfully resolved
if (e.Seq.Type.IsArrayType) {
- Contract.Assert(e.SelectOne); // resolution enforces that a non-unit array selections is allowed only as an assignment LHS
elmtType = UserDefinedType.ArrayElementType(e.Seq.Type);
} else {
elmtType = ((SeqType)e.Seq.Type).Arg;
@@ -4740,13 +4754,16 @@ namespace Microsoft.Dafny {
}
return x;
} else {
+ if (e.Seq.Type.IsArrayType) {
+ seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqFromArray, elType, HeapExpr, seq);
+ }
if (e1 != null) {
seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqTake, elType, seq, e1);
}
if (e0 != null) {
seq = translator.FunctionCall(expr.tok, BuiltinFunction.SeqDrop, elType, seq, e0);
}
- // if e0 == null && e1 == null, then we have the identity operation seq[..];
+ // if e0 == null && e1 == null, then we have the identity operation seq[..] == seq;
return seq;
}
@@ -5489,6 +5506,7 @@ namespace Microsoft.Dafny {
SeqTake,
SeqEqual,
SeqSameUntil,
+ SeqFromArray,
IndexField,
MultiIndexField,
@@ -5627,7 +5645,7 @@ namespace Microsoft.Dafny {
return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Seq#Empty", resultType, args), resultType);
}
case BuiltinFunction.SeqBuild:
- Contract.Assert(args.Length == 4);
+ Contract.Assert(args.Length == 2);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Seq#Build", predef.SeqType(tok, typeInstantiation), args);
case BuiltinFunction.SeqAppend:
@@ -5662,6 +5680,10 @@ namespace Microsoft.Dafny {
Contract.Assert(args.Length == 3);
Contract.Assert(typeInstantiation == null);
return FunctionCall(tok, "Seq#SameUntil", Bpl.Type.Bool, args);
+ case BuiltinFunction.SeqFromArray:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "Seq#FromArray", typeInstantiation, args);
case BuiltinFunction.IndexField:
Contract.Assert(args.Length == 1);
diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy
index cc07cbb5..f1fc7d48 100644
--- a/Test/dafny0/AdvancedLHS.dfy
+++ b/Test/dafny0/AdvancedLHS.dfy
@@ -34,7 +34,6 @@ class C {
if (a != null && 10 <= a.Length) {
a[2] := new C;
- a[4..8] := null;
a[3] := *;
}
if (b != null && 10 <= b.Length0 && 20 <= b.Length1) {
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 5f366d10..1a18be6d 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -72,30 +72,17 @@ class A {
}
method Q() {
- var y := new object[100];
- y[5] := null;
- y[0..] := null;
- y[..83] := null;
- y[0..y.Length] := null;
- }
-
- method R() {
- var y := new int[100];
- y[55] := 80;
- y[10..] := 25;
- y[..83] := 30;
- y[50..60] := 35;
- y[55] := 90;
-
- assert y[54] == 35;
- assert y[55] == 90;
- assert y[83] == 25;
- assert y[8] == 30;
- assert y[90] + y[91] + y[0] + 20 == y.Length;
- assert y[93] == 24; // error (it's 25)
-
- y[..] := 4; // assign to all elements.
- assert forall i :: 0 <= i < y.Length ==> y[i] == 4;
+ var a := new int[5];
+ y[0],y[1],y[2],y[3],y[4] := 0,1,2,3,4;
+
+ assert [1,2,3,4] == y[1..];
+ assert [1,2,3,4] == y[1.. y.Length];
+ assert [1] == y[1..2];
+ assert [0,1] == y[..2];
+ assert [0,1] == y[0..2];
+ assert forall i :: 0 <= i <= y.Length ==> [] == y[i..i];
+ assert [0,1,2,3,4] == y[..];
+ assert forall i :: 0 <= i < y.Length ==> y[i] == i;
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 16:57:17 +0000