diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-21 19:16:05 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-21 19:16:05 -0700 |
| commit | b0d1f6cc6a6d4f0ea1c64ae6de053061f4697375 (patch) | |
| tree | f8bba784923413c213a6085125beb5baf5dbc13b | |
| parent | fbb49d063841042511bf29c48892ef82e42853a1 (diff) | |
Dafny: Since it's no longer true that all types support equality at run-time (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation.
| -rw-r--r-- | Source/Dafny/Dafny.atg | 17 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 151 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 571 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 456 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 130 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b4.dfy | 2 | ||||
| -rw-r--r-- | Test/VSI-Benchmarks/b8.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 4 | ||||
| -rw-r--r-- | Test/dafny1/Celebrity.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny1/UltraFilter.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny2/MajorityVote.dfy | 12 | ||||
| -rw-r--r-- | Test/vstte2012/BreadthFirstSearch.dfy | 2 |
15 files changed, 916 insertions, 447 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 66756b0c..3000d348 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -290,10 +290,13 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.> ArbitraryTypeDecl<ModuleDecl/*!*/ module, out ArbitraryTypeDecl at>
= (. IToken/*!*/ id;
Attributes attrs = null;
+ var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
.)
"type"
{ Attribute<ref attrs> }
- Ident<out id> (. at = new ArbitraryTypeDecl(id, id.val, module, attrs); .)
+ Ident<out id>
+ [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
+ ] (. at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs); .)
SYNC ";"
.
GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost>
@@ -356,10 +359,16 @@ TypeIdentOptional<out IToken/*!*/ id, out string/*!*/ identName, out Type/*!*/ t /*------------------------------------------------------------------------*/
GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
= (. Contract.Requires(cce.NonNullElements(typeArgs));
- IToken/*!*/ id; .)
+ IToken/*!*/ id;
+ TypeParameter.EqualitySupportValue eqSupport;
+ .)
"<"
- Ident<out id> (. typeArgs.Add(new TypeParameter(id, id.val)); .)
- { "," Ident<out id> (. typeArgs.Add(new TypeParameter(id, id.val)); .)
+ Ident<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
+ ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
+ { "," Ident<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ [ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
+ ] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
}
">"
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 5e6ad5c3..6da3138c 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -269,8 +269,18 @@ namespace Microsoft.Dafny { }
public bool IsTypeParameter {
get {
+ return AsTypeParameter != null;
+ }
+ }
+ public TypeParameter AsTypeParameter {
+ get {
UserDefinedType ct = this as UserDefinedType;
- return ct != null && ct.ResolvedParam != null;
+ return ct == null ? null : ct.ResolvedParam;
+ }
+ }
+ public virtual bool SupportsEquality {
+ get {
+ return true;
}
}
}
@@ -318,16 +328,20 @@ namespace Microsoft.Dafny { public abstract class CollectionType : NonProxyType
{
- public readonly Type Arg;
+ public readonly Type Arg; // denotes the Domain type for a Map
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Arg != null);
}
-
public CollectionType(Type arg) {
Contract.Requires(arg != null);
this.Arg = arg;
}
+ public override bool SupportsEquality {
+ get {
+ return Arg.SupportsEquality;
+ }
+ }
}
public class SetType : CollectionType {
@@ -369,12 +383,14 @@ namespace Microsoft.Dafny { }
public class MapType : CollectionType
{
- public Type Domain, Range;
+ public Type Range;
public MapType(Type domain, Type range) : base(domain) {
Contract.Requires(domain != null && range != null);
- Domain = domain;
Range = range;
}
+ public Type Domain {
+ get { return Arg; }
+ }
[Pure]
public override string ToString() {
Contract.Ensures(Contract.Result<string>() != null);
@@ -515,6 +531,23 @@ namespace Microsoft.Dafny { }
return s;
}
+
+ public override bool SupportsEquality {
+ get {
+ if (ResolvedClass is ClassDecl) {
+ return true;
+ } else if (ResolvedClass is CoDatatypeDecl) {
+ return false;
+ } else if (ResolvedClass is IndDatatypeDecl) {
+ // TODO
+ return true;
+ } else if (ResolvedParam != null) {
+ return ResolvedParam.MustSupportEquality;
+ }
+ Contract.Assume(false); // the SupportsEquality getter requires the Type to have been successfully resolved
+ return true;
+ }
+ }
}
public abstract class TypeProxy : Type {
@@ -529,6 +562,15 @@ namespace Microsoft.Dafny { Contract.Assume(T == null || cce.IsPeerConsistent(T));
return T == null ? "?" : T.ToString();
}
+ public override bool SupportsEquality {
+ get {
+ if (T != null) {
+ return T.SupportsEquality;
+ } else {
+ return base.SupportsEquality;
+ }
+ }
+ }
}
public abstract class UnrestrictedTypeProxy : TypeProxy {
@@ -589,17 +631,6 @@ namespace Microsoft.Dafny { }
/// <summary>
- /// This proxy stands for object or any class/array type or a set/sequence of object or a class/array type.
- /// </summary>
- public class ObjectsTypeProxy : RestrictedTypeProxy {
- public override int OrderID {
- get {
- return 2;
- }
- }
- }
-
- /// <summary>
/// This proxy stands for:
/// set(Arg) or seq(Arg) or map(Arg, Range)
/// </summary>
@@ -616,7 +647,7 @@ namespace Microsoft.Dafny { }
public override int OrderID {
get {
- return 3;
+ return 2;
}
}
}
@@ -635,7 +666,7 @@ namespace Microsoft.Dafny { }
public override int OrderID {
get {
- return 4;
+ return 3;
}
}
}
@@ -658,7 +689,7 @@ namespace Microsoft.Dafny { }
public override int OrderID {
get {
- return 5;
+ return 4;
}
}
}
@@ -723,10 +754,17 @@ namespace Microsoft.Dafny { parent = value;
}
}
- public TypeParameter(IToken tok, string name)
+ public enum EqualitySupportValue { Required, InferredRequired, Unspecified }
+ public EqualitySupportValue EqualitySupport; // the resolver may change this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required)
+ public bool MustSupportEquality {
+ get { return EqualitySupport != EqualitySupportValue.Unspecified; }
+ }
+
+ public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified)
: base(tok, name, null) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
+ EqualitySupport = equalitySupport;
}
}
@@ -953,13 +991,15 @@ namespace Microsoft.Dafny { public abstract class MemberDecl : Declaration {
public readonly bool IsStatic;
+ public readonly bool IsGhost;
public TopLevelDecl EnclosingClass; // filled in during resolution
- public MemberDecl(IToken tok, string name, bool isStatic, Attributes attributes)
+ public MemberDecl(IToken tok, string name, bool isStatic, bool isGhost, Attributes attributes)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
IsStatic = isStatic;
+ IsGhost = isGhost;
}
/// <summary>
/// Returns className+"."+memberName. Available only after resolution.
@@ -983,7 +1023,6 @@ namespace Microsoft.Dafny { }
public class Field : MemberDecl {
- public readonly bool IsGhost;
public readonly bool IsMutable;
public readonly Type Type;
[ContractInvariantMethod]
@@ -999,11 +1038,10 @@ namespace Microsoft.Dafny { }
public Field(IToken tok, string name, bool isGhost, bool isMutable, Type type, Attributes attributes)
- : base(tok, name, false, attributes) {
+ : base(tok, name, false, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(type != null);
- IsGhost = isGhost;
IsMutable = isMutable;
Type = type;
}
@@ -1043,17 +1081,23 @@ namespace Microsoft.Dafny { public class ArbitraryTypeDecl : TopLevelDecl, TypeParameter.ParentType
{
public readonly TypeParameter TheType;
+ public TypeParameter.EqualitySupportValue EqualitySupport {
+ get { return TheType.EqualitySupport; }
+ }
+ public bool MustSupportEquality {
+ get { return TheType.MustSupportEquality; }
+ }
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(TheType != null && Name == TheType.Name);
}
- public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes)
+ public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, TypeParameter.EqualitySupportValue equalitySupport, Attributes attributes)
: base(tok, name, module, new List<TypeParameter>(), attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(module != null);
- TheType = new TypeParameter(tok, name);
+ TheType = new TypeParameter(tok, name, equalitySupport);
}
}
@@ -1274,7 +1318,6 @@ namespace Microsoft.Dafny { }
public class Function : MemberDecl, TypeParameter.ParentType {
- public readonly bool IsGhost; // functions are "ghost" by default; a non-ghost function is called a "function method"
public bool IsRecursive; // filled in during resolution
public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;
public readonly IToken OpenParen; // can be null (for predicates), if there are no formals
@@ -1297,11 +1340,14 @@ namespace Microsoft.Dafny { Contract.Invariant(Decreases != null);
}
+ /// <summary>
+ /// Note, functions are "ghost" by default; a non-ghost function is called a "function method".
+ /// </summary>
public Function(IToken tok, string name, bool isStatic, bool isGhost,
List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals, Type resultType,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
Expression body, Attributes attributes, bool signatureOmitted)
- : base(tok, name, isStatic, attributes) {
+ : base(tok, name, isStatic, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -1312,7 +1358,6 @@ namespace Microsoft.Dafny { Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
- this.IsGhost = isGhost;
this.TypeArgs = typeArgs;
this.OpenParen = openParen;
this.Formals = formals;
@@ -1341,7 +1386,6 @@ namespace Microsoft.Dafny { public class Method : MemberDecl, TypeParameter.ParentType
{
- public readonly bool IsGhost;
public readonly bool SignatureIsOmitted;
public readonly List<TypeParameter/*!*/>/*!*/ TypeArgs;
public readonly List<Formal/*!*/>/*!*/ Ins;
@@ -1372,7 +1416,7 @@ namespace Microsoft.Dafny { [Captured] Specification<Expression>/*!*/ decreases,
[Captured] BlockStmt body,
Attributes attributes, bool signatureOmitted)
- : base(tok, name, isStatic, attributes) {
+ : base(tok, name, isStatic, isGhost, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
@@ -1382,7 +1426,6 @@ namespace Microsoft.Dafny { Contract.Requires(mod != null);
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(decreases != null);
- this.IsGhost = isGhost;
this.TypeArgs = typeArgs;
this.Ins = ins;
this.Outs = outs;
@@ -1640,6 +1683,18 @@ namespace Microsoft.Dafny { Attributes = attrs;
}
public abstract bool CanAffectPreviouslyKnownExpressions { get; }
+ /// <summary>
+ /// Returns the non-null subexpressions of the AssignmentRhs.
+ /// </summary>
+ public virtual IEnumerable<Expression> SubExpressions {
+ get { yield break; }
+ }
+ /// <summary>
+ /// Returns the non-null sub-statements of the AssignmentRhs.
+ /// </summary>
+ public virtual IEnumerable<Statement> SubStatements{
+ get { yield break; }
+ }
}
public class ExprRhs : AssignmentRhs
@@ -1657,6 +1712,11 @@ namespace Microsoft.Dafny { Expr = expr;
}
public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Expr;
+ }
+ }
}
public class TypeRhs : AssignmentRhs
@@ -1705,6 +1765,23 @@ namespace Microsoft.Dafny { return false;
}
}
+
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ if (ArrayDimensions != null) {
+ foreach (var e in ArrayDimensions) {
+ yield return e;
+ }
+ }
+ }
+ }
+ public override IEnumerable<Statement> SubStatements {
+ get {
+ if (InitCall != null) {
+ yield return InitCall;
+ }
+ }
+ }
}
public class CallRhs : AssignmentRhs
@@ -1744,6 +1821,14 @@ namespace Microsoft.Dafny { return false;
}
}
+ public override IEnumerable<Expression> SubExpressions {
+ get {
+ yield return Receiver;
+ foreach (var e in Args) {
+ yield return e;
+ }
+ }
+ }
}
public class HavocRhs : AssignmentRhs {
@@ -1980,6 +2065,7 @@ namespace Microsoft.Dafny { public Expression/*!*/ Receiver;
public readonly string/*!*/ MethodName;
public readonly List<Expression/*!*/>/*!*/ Args;
+ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // create, initialized, and used by resolution (could be deleted once all of resolution is done)
public Method Method; // filled in by resolution
public CallStmt(IToken tok, List<Expression/*!*/>/*!*/ lhs, Expression/*!*/ receiver,
@@ -2785,6 +2871,7 @@ namespace Microsoft.Dafny { public readonly Expression/*!*/ Receiver;
public readonly IToken OpenParen; // can be null if Args.Count == 0
public readonly List<Expression/*!*/>/*!*/ Args;
+ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutions; // create, initialized, and used by resolution (could be deleted once all of resolution is done)
public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }
public CoCallResolution CoCall = CoCallResolution.No; // indicates whether or not the call is a co-recursive call; filled in by resolution
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 26b98833..0c1920a6 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -315,7 +315,7 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Expect(6);
@@ -351,7 +351,7 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Expect(16);
@@ -376,13 +376,20 @@ bool IsAttribute() { void ArbitraryTypeDecl(ModuleDecl/*!*/ module, out ArbitraryTypeDecl at) {
IToken/*!*/ id;
Attributes attrs = null;
+ var eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
Expect(21);
while (la.kind == 6) {
Attribute(ref attrs);
}
Ident(out id);
- at = new ArbitraryTypeDecl(id, id.val, module, attrs);
+ if (la.kind == 22) {
+ Get();
+ Expect(23);
+ Expect(24);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ at = new ArbitraryTypeDecl(id, id.val, module, eqSupport, attrs);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();}
Expect(18);
}
@@ -405,10 +412,10 @@ bool IsAttribute() { }
if (la.kind == 19) {
FieldDecl(mmod, mm);
- } else if (la.kind == 44 || la.kind == 45) {
+ } else if (la.kind == 45 || la.kind == 46) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (la.kind == 24 || la.kind == 25) {
+ } else if (la.kind == 27 || la.kind == 28) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
} else SynErr(114);
@@ -416,16 +423,32 @@ bool IsAttribute() { void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
Contract.Requires(cce.NonNullElements(typeArgs));
- IToken/*!*/ id;
- Expect(22);
+ IToken/*!*/ id;
+ TypeParameter.EqualitySupportValue eqSupport;
+
+ Expect(25);
Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
+ eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
+ if (la.kind == 22) {
+ Get();
+ Expect(23);
+ Expect(24);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
while (la.kind == 20) {
Get();
Ident(out id);
- typeArgs.Add(new TypeParameter(id, id.val));
+ eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
+ if (la.kind == 22) {
+ Get();
+ Expect(23);
+ Expect(24);
+ eqSupport = TypeParameter.EqualitySupportValue.Required;
+ }
+ typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
}
- Expect(23);
+ Expect(26);
}
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
@@ -470,9 +493,9 @@ bool IsAttribute() { IToken bodyEnd = Token.NoToken;
bool signatureOmitted = false;
- if (la.kind == 44) {
+ if (la.kind == 45) {
Get();
- if (la.kind == 24) {
+ if (la.kind == 27) {
Get();
isFunctionMethod = true;
}
@@ -482,22 +505,22 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22 || la.kind == 33) {
- if (la.kind == 22) {
+ if (la.kind == 22 || la.kind == 25) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals, out openParen);
Expect(5);
Type(out returnType);
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
} else SynErr(117);
- } else if (la.kind == 45) {
+ } else if (la.kind == 46) {
Get();
isPredicate = true;
- if (la.kind == 24) {
+ if (la.kind == 27) {
Get();
isFunctionMethod = true;
}
@@ -508,17 +531,17 @@ bool IsAttribute() { }
Ident(out id);
if (StartOf(4)) {
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
- if (la.kind == 33) {
+ if (la.kind == 22) {
Formals(true, isFunctionMethod, formals, out openParen);
if (la.kind == 5) {
Get();
SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
}
}
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
signatureOmitted = true;
openParen = Token.NoToken;
@@ -562,10 +585,10 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(120); Get();}
- if (la.kind == 24) {
+ while (!(la.kind == 0 || la.kind == 27 || la.kind == 28)) {SynErr(120); Get();}
+ if (la.kind == 27) {
Get();
- } else if (la.kind == 25) {
+ } else if (la.kind == 28) {
Get();
if (allowConstructor) {
isConstructor = true;
@@ -587,17 +610,17 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 22 || la.kind == 33) {
- if (la.kind == 22) {
+ if (la.kind == 22 || la.kind == 25) {
+ if (la.kind == 25) {
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins, out openParen);
- if (la.kind == 26) {
+ if (la.kind == 29) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs, out openParen);
}
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
signatureOmitted = true; openParen = Token.NoToken;
} else SynErr(122);
@@ -629,7 +652,7 @@ bool IsAttribute() { Attribute(ref attrs);
}
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
FormalsOptionalIds(formals);
}
ctors.Add(new DatatypeCtor(id, id.val, formals, attrs));
@@ -637,7 +660,7 @@ bool IsAttribute() { void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
- Expect(33);
+ Expect(22);
if (StartOf(7)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
@@ -647,7 +670,7 @@ bool IsAttribute() { formals.Add(new Formal(id, name, ty, true, isGhost));
}
}
- Expect(34);
+ Expect(24);
}
void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
@@ -731,22 +754,22 @@ bool IsAttribute() { List<Type/*!*/>/*!*/ gt;
switch (la.kind) {
- case 35: {
+ case 36: {
Get();
tok = t;
break;
}
- case 36: {
+ case 37: {
Get();
tok = t; ty = new NatType();
break;
}
- case 37: {
+ case 38: {
Get();
tok = t; ty = new IntType();
break;
}
- case 38: {
+ case 39: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -757,7 +780,7 @@ bool IsAttribute() { break;
}
- case 39: {
+ case 40: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -768,7 +791,7 @@ bool IsAttribute() { break;
}
- case 40: {
+ case 41: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -779,7 +802,7 @@ bool IsAttribute() { break;
}
- case 41: {
+ case 42: {
Get();
tok = t; gt = new List<Type/*!*/>();
GenericInstantiation(gt);
@@ -790,7 +813,7 @@ bool IsAttribute() { break;
}
- case 1: case 3: case 42: {
+ case 1: case 3: case 43: {
ReferenceType(out tok, out ty);
break;
}
@@ -800,7 +823,7 @@ bool IsAttribute() { void Formals(bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost;
- Expect(33);
+ Expect(22);
openParen = t;
if (la.kind == 1 || la.kind == 8) {
GIdentType(allowGhostKeyword, out id, out ty, out isGhost);
@@ -811,7 +834,7 @@ bool IsAttribute() { formals.Add(new Formal(id, id.val, ty, incoming, isGhost));
}
}
- Expect(34);
+ Expect(24);
}
void MethodSpec(List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/*!*/ mod, List<MaybeFreeExpression/*!*/>/*!*/ ens,
@@ -820,7 +843,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
while (!(StartOf(8))) {SynErr(124); Get();}
- if (la.kind == 28) {
+ if (la.kind == 31) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -836,18 +859,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
while (!(la.kind == 0 || la.kind == 18)) {SynErr(125); Get();}
Expect(18);
- } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {
- if (la.kind == 29) {
+ } else if (la.kind == 32 || la.kind == 33 || la.kind == 34) {
+ if (la.kind == 32) {
Get();
isFree = true;
}
- if (la.kind == 30) {
+ if (la.kind == 33) {
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();}
Expect(18);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
@@ -857,7 +880,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(18);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
} else SynErr(128);
- } else if (la.kind == 32) {
+ } else if (la.kind == 35) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
@@ -885,7 +908,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
- if (la.kind == 48) {
+ if (la.kind == 49) {
Get();
Ident(out id);
fieldName = id.val;
@@ -920,7 +943,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
- Expect(22);
+ Expect(25);
Type(out ty);
gt.Add(ty);
while (la.kind == 20) {
@@ -928,7 +951,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Type(out ty);
gt.Add(ty);
}
- Expect(23);
+ Expect(26);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -937,7 +960,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken moduleName = null;
List<Type/*!*/>/*!*/ gt;
- if (la.kind == 42) {
+ if (la.kind == 43) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 3) {
@@ -956,12 +979,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 1) {
Ident(out tok);
gt = new List<Type/*!*/>();
- if (la.kind == 43) {
+ if (la.kind == 44) {
moduleName = tok;
Get();
Ident(out tok);
}
- if (la.kind == 22) {
+ if (la.kind == 25) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, moduleName);
@@ -971,14 +994,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {
Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
- if (la.kind == 30) {
- while (!(la.kind == 0 || la.kind == 30)) {SynErr(132); Get();}
+ if (la.kind == 33) {
+ while (!(la.kind == 0 || la.kind == 33)) {SynErr(132); Get();}
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();}
Expect(18);
reqs.Add(e);
- } else if (la.kind == 46) {
+ } else if (la.kind == 47) {
Get();
if (StartOf(11)) {
PossiblyWildFrameExpression(out fe);
@@ -991,13 +1014,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();}
Expect(18);
- } else if (la.kind == 31) {
+ } else if (la.kind == 34) {
Get();
Expression(out e);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();}
Expect(18);
ens.Add(e);
- } else if (la.kind == 32) {
+ } else if (la.kind == 35) {
Get();
DecreasesList(decreases, false);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();}
@@ -1016,7 +1039,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(9)) {
@@ -1027,7 +1050,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(9)) {
@@ -1056,19 +1079,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = bs;
break;
}
- case 66: {
+ case 67: {
AssertStmt(out s);
break;
}
- case 54: {
+ case 55: {
AssumeStmt(out s);
break;
}
- case 67: {
+ case 68: {
PrintStmt(out s);
break;
}
- case 1: case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
+ case 1: case 2: case 17: case 22: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
UpdateStmt(out s);
break;
}
@@ -1076,23 +1099,23 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo VarDeclStatement(out s);
break;
}
- case 59: {
+ case 60: {
IfStmt(out s);
break;
}
- case 63: {
+ case 64: {
WhileStmt(out s);
break;
}
- case 65: {
+ case 66: {
MatchStmt(out s);
break;
}
- case 68: {
+ case 69: {
ParallelStmt(out s);
break;
}
- case 49: {
+ case 50: {
Get();
x = t;
Ident(out id);
@@ -1101,14 +1124,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 50: {
+ case 51: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- } else if (la.kind == 18 || la.kind == 50) {
- while (la.kind == 50) {
+ } else if (la.kind == 18 || la.kind == 51) {
+ while (la.kind == 51) {
Get();
breakCount++;
}
@@ -1118,11 +1141,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 51: {
+ case 52: {
ReturnStmt(out s);
break;
}
- case 27: {
+ case 30: {
Get();
s = new SkeletonStatement(t);
Expect(18);
@@ -1136,14 +1159,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
Expression/*!*/ e = null; Attributes attrs = null;
- Expect(66);
+ Expect(67);
x = t; s = null;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(9)) {
Expression(out e);
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
} else SynErr(144);
Expect(18);
@@ -1157,7 +1180,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void AssumeStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e;
- Expect(54);
+ Expect(55);
x = t;
Expression(out e);
Expect(18);
@@ -1168,7 +1191,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
List<Attributes.Argument/*!*/> args = new List<Attributes.Argument/*!*/>();
- Expect(67);
+ Expect(68);
x = t;
AttributeArg(out arg);
args.Add(arg);
@@ -1199,14 +1222,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
Expect(18);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 20 || la.kind == 52 || la.kind == 53) {
+ } else if (la.kind == 20 || la.kind == 53 || la.kind == 54) {
lhss.Add(e); lhs0 = e;
while (la.kind == 20) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1216,10 +1239,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
x = t;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
suchThatAssume = t;
}
@@ -1260,8 +1283,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 52 || la.kind == 53) {
- if (la.kind == 52) {
+ if (la.kind == 53 || la.kind == 54) {
+ if (la.kind == 53) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1277,7 +1300,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else {
Get();
assignTok = t;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
suchThatAssume = t;
}
@@ -1316,19 +1339,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
ifStmt = dummyStmt; // to please the compiler
- Expect(59);
+ Expect(60);
x = t;
- if (la.kind == 27 || la.kind == 33) {
- if (la.kind == 33) {
+ if (la.kind == 22 || la.kind == 30) {
+ if (la.kind == 22) {
Guard(out guard);
} else {
Get();
guardOmitted = true;
}
BlockStmt(out thn, out bodyStart, out bodyEnd);
- if (la.kind == 60) {
+ if (la.kind == 61) {
Get();
- if (la.kind == 59) {
+ if (la.kind == 60) {
IfStmt(out s);
els = s;
} else if (la.kind == 6) {
@@ -1361,10 +1384,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
- Expect(63);
+ Expect(64);
x = t;
- if (la.kind == 27 || la.kind == 33) {
- if (la.kind == 33) {
+ if (la.kind == 22 || la.kind == 30) {
+ if (la.kind == 22) {
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
} else {
@@ -1374,7 +1397,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs);
if (la.kind == 6) {
BlockStmt(out body, out bodyStart, out bodyEnd);
- } else if (la.kind == 27) {
+ } else if (la.kind == 30) {
Get();
bodyOmitted = true;
} else SynErr(149);
@@ -1402,11 +1425,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x; Expression/*!*/ e; MatchCaseStmt/*!*/ c;
List<MatchCaseStmt/*!*/> cases = new List<MatchCaseStmt/*!*/>();
- Expect(65);
+ Expect(66);
x = t;
Expression(out e);
Expect(6);
- while (la.kind == 61) {
+ while (la.kind == 62) {
CaseStatement(out c);
cases.Add(c);
}
@@ -1426,9 +1449,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BlockStmt/*!*/ block;
IToken bodyStart, bodyEnd;
- Expect(68);
+ Expect(69);
x = t;
- Expect(33);
+ Expect(22);
if (la.kind == 1) {
List<BoundVar/*!*/> bvarsX; Attributes attrsX; Expression rangeX;
QuantifierDomain(out bvarsX, out attrsX, out rangeX);
@@ -1438,14 +1461,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (bvars == null) { bvars = new List<BoundVar>(); }
if (range == null) { range = new LiteralExpr(x, true); }
- Expect(34);
- while (la.kind == 29 || la.kind == 31) {
+ Expect(24);
+ while (la.kind == 32 || la.kind == 34) {
isFree = false;
- if (la.kind == 29) {
+ if (la.kind == 32) {
Get();
isFree = true;
}
- Expect(31);
+ Expect(34);
Expression(out e);
Expect(18);
ens.Add(new MaybeFreeExpression(e, isFree));
@@ -1459,7 +1482,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(51);
+ Expect(52);
returnTok = t;
if (StartOf(14)) {
Rhs(out r, null);
@@ -1483,27 +1506,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = null; // to please compiler
Attributes attrs = null;
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 33 || la.kind == 43 || la.kind == 56) {
- if (la.kind == 56) {
+ if (la.kind == 22 || la.kind == 44 || la.kind == 57) {
+ if (la.kind == 57) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(57);
+ Expect(58);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
Ident(out x);
- Expect(33);
+ Expect(22);
args = new List<Expression/*!*/>();
if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
} else {
Get();
@@ -1521,7 +1544,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
if (x != null) {
initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
}
@@ -1534,12 +1557,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo r = new TypeRhs(newToken, ty, initCall);
}
- } else if (la.kind == 58) {
+ } else if (la.kind == 59) {
Get();
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 47) {
+ } else if (la.kind == 48) {
Get();
r = new HavocRhs(t);
} else if (StartOf(9)) {
@@ -1557,13 +1580,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
} else if (StartOf(15)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
} else SynErr(152);
@@ -1582,15 +1605,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
- Expect(33);
- if (la.kind == 47) {
+ Expect(22);
+ if (la.kind == 48) {
Get();
e = null;
} else if (StartOf(9)) {
Expression(out ee);
e = ee;
} else SynErr(153);
- Expect(34);
+ Expect(24);
}
void AlternativeBlock(out List<GuardedAlternative> alternatives) {
@@ -1600,11 +1623,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Statement> body;
Expect(6);
- while (la.kind == 61) {
+ while (la.kind == 62) {
Get();
x = t;
Expression(out e);
- Expect(62);
+ Expect(63);
body = new List<Statement>();
while (StartOf(10)) {
Stmt(body);
@@ -1622,13 +1645,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null;
while (StartOf(16)) {
- if (la.kind == 29 || la.kind == 64) {
+ if (la.kind == 32 || la.kind == 65) {
Invariant(out invariant);
while (!(la.kind == 0 || la.kind == 18)) {SynErr(154); Get();}
Expect(18);
invariants.Add(invariant);
- } else if (la.kind == 32) {
- while (!(la.kind == 0 || la.kind == 32)) {SynErr(155); Get();}
+ } else if (la.kind == 35) {
+ while (!(la.kind == 0 || la.kind == 35)) {SynErr(155); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
@@ -1637,7 +1660,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (!(la.kind == 0 || la.kind == 18)) {SynErr(156); Get();}
Expect(18);
} else {
- while (!(la.kind == 0 || la.kind == 28)) {SynErr(157); Get();}
+ while (!(la.kind == 0 || la.kind == 31)) {SynErr(157); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1660,12 +1683,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Invariant(out MaybeFreeExpression/*!*/ invariant) {
bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null;
- while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(159); Get();}
- if (la.kind == 29) {
+ while (!(la.kind == 0 || la.kind == 32 || la.kind == 65)) {SynErr(159); Get();}
+ if (la.kind == 32) {
Get();
isFree = true;
}
- Expect(64);
+ Expect(65);
while (IsAttribute()) {
Attribute(ref attrs);
}
@@ -1680,10 +1703,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
List<Statement/*!*/> body = new List<Statement/*!*/>();
- Expect(61);
+ Expect(62);
x = t;
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -1692,9 +1715,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(34);
+ Expect(24);
}
- Expect(62);
+ Expect(63);
while (StartOf(10)) {
Stmt(body);
}
@@ -1737,7 +1760,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 69 || la.kind == 70) {
+ while (la.kind == 70 || la.kind == 71) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -1748,7 +1771,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 71 || la.kind == 72) {
+ if (la.kind == 72 || la.kind == 73) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -1757,9 +1780,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
- } else if (la.kind == 70) {
+ } else if (la.kind == 71) {
Get();
} else SynErr(161);
}
@@ -1768,12 +1791,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(17)) {
- if (la.kind == 73 || la.kind == 74) {
+ if (la.kind == 74 || la.kind == 75) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 73 || la.kind == 74) {
+ while (la.kind == 74 || la.kind == 75) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1784,7 +1807,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 75 || la.kind == 76) {
+ while (la.kind == 76 || la.kind == 77) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1795,9 +1818,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void ImpliesOp() {
- if (la.kind == 71) {
+ if (la.kind == 72) {
Get();
- } else if (la.kind == 72) {
+ } else if (la.kind == 73) {
Get();
} else SynErr(162);
}
@@ -1893,17 +1916,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 73) {
+ if (la.kind == 74) {
Get();
- } else if (la.kind == 74) {
+ } else if (la.kind == 75) {
Get();
} else SynErr(163);
}
void OrOp() {
- if (la.kind == 75) {
+ if (la.kind == 76) {
Get();
- } else if (la.kind == 76) {
+ } else if (la.kind == 77) {
Get();
} else SynErr(164);
}
@@ -1924,17 +1947,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken y;
switch (la.kind) {
- case 77: {
+ case 23: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
break;
}
- case 22: {
+ case 25: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 23: {
+ case 26: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
@@ -2004,7 +2027,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 47 || la.kind == 89 || la.kind == 90) {
+ while (la.kind == 48 || la.kind == 89 || la.kind == 90) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2039,32 +2062,32 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e);
break;
}
- case 19: case 38: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: {
+ case 19: case 39: case 55: case 60: case 66: case 67: case 101: case 102: case 103: case 104: {
EndlessExpression(out e);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
break;
}
- case 6: case 56: {
+ case 6: case 57: {
DisplayExpr(out e);
break;
}
- case 39: {
+ case 40: {
MultiSetExpr(out e);
break;
}
- case 41: {
+ case 42: {
MapExpr(out e);
break;
}
- case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
+ case 2: case 17: case 22: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
ConstAtomExpression(out e);
- while (la.kind == 43 || la.kind == 56) {
+ while (la.kind == 44 || la.kind == 57) {
Suffix(ref e);
}
break;
@@ -2075,7 +2098,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
} else if (la.kind == 89) {
@@ -2103,18 +2126,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<BoundVar> letVars; List<Expression> letRHSs;
switch (la.kind) {
- case 59: {
+ case 60: {
Get();
x = t;
Expression(out e);
Expect(99);
Expression(out e0);
- Expect(60);
+ Expect(61);
Expression(out e1);
e = new ITEExpr(x, e, e0, e1);
break;
}
- case 65: {
+ case 66: {
MatchExpression(out e);
break;
}
@@ -2122,11 +2145,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo QuantifierGuts(out e);
break;
}
- case 38: {
+ case 39: {
ComprehensionExpr(out e);
break;
}
- case 66: {
+ case 67: {
Get();
x = t;
Expression(out e0);
@@ -2135,7 +2158,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new AssertExpr(x, e0, e1);
break;
}
- case 54: {
+ case 55: {
Get();
x = t;
Expression(out e0);
@@ -2156,7 +2179,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(52);
+ Expect(53);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 20) {
@@ -2180,18 +2203,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id);
idents.Add(id);
- while (la.kind == 43) {
+ while (la.kind == 44) {
Get();
Ident(out id);
idents.Add(id);
}
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
openParen = t; args = new List<Expression>();
if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
}
e = new IdentifierSequence(idents, openParen, args);
}
@@ -2202,20 +2225,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
IToken openParen = t; args = new List<Expression/*!*/>(); func = true;
if (StartOf(9)) {
Expressions(args);
}
- Expect(34);
+ Expect(24);
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
x = t;
if (StartOf(9)) {
@@ -2228,11 +2251,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 52) {
+ } else if (la.kind == 53) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 20 || la.kind == 57) {
+ } else if (la.kind == 20 || la.kind == 58) {
while (la.kind == 20) {
Get();
Expression(out ee);
@@ -2274,7 +2297,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- Expect(57);
+ Expect(58);
} else SynErr(173);
}
@@ -2291,14 +2314,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 56) {
+ } else if (la.kind == 57) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(9)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(57);
+ Expect(58);
} else SynErr(174);
}
@@ -2307,7 +2330,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(39);
+ Expect(40);
x = t;
if (la.kind == 6) {
Get();
@@ -2317,12 +2340,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
e = new MultiSetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 33) {
+ } else if (la.kind == 22) {
Get();
x = t; elements = new List<Expression/*!*/>();
Expression(out e);
e = new MultiSetFormingExpr(x, e);
- Expect(34);
+ Expect(24);
} else if (StartOf(19)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
} else SynErr(175);
@@ -2334,16 +2357,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List<ExpressionPair/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(41);
+ Expect(42);
x = t;
- if (la.kind == 56) {
+ if (la.kind == 57) {
Get();
elements = new List<ExpressionPair/*!*/>();
if (StartOf(9)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(x, elements);
- Expect(57);
+ Expect(58);
} else if (la.kind == 1) {
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2396,27 +2419,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 96: {
Get();
x = t;
- Expect(33);
+ Expect(22);
Expression(out e);
- Expect(34);
+ Expect(24);
e = new FreshExpr(x, e);
break;
}
case 97: {
Get();
x = t;
- Expect(33);
+ Expect(22);
Expression(out e);
- Expect(34);
+ Expect(24);
e = new AllocatedExpr(x, e);
break;
}
case 98: {
Get();
x = t;
- Expect(33);
+ Expect(22);
Expression(out e);
- Expect(34);
+ Expect(24);
e = new OldExpr(x, e);
break;
}
@@ -2428,12 +2451,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(17);
break;
}
- case 33: {
+ case 22: {
Get();
x = t;
Expression(out e);
e = new ParensExpression(x, e);
- Expect(34);
+ Expect(24);
break;
}
default: SynErr(177); break;
@@ -2455,13 +2478,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d);
- Expect(52);
+ Expect(53);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 20) {
Get();
Expression(out d);
- Expect(52);
+ Expect(53);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
}
@@ -2479,10 +2502,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; MatchCaseExpr/*!*/ c;
List<MatchCaseExpr/*!*/> cases = new List<MatchCaseExpr/*!*/>();
- Expect(65);
+ Expect(66);
x = t;
Expression(out e);
- while (la.kind == 61) {
+ while (la.kind == 62) {
CaseExpression(out c);
cases.Add(c);
}
@@ -2523,7 +2546,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ range;
Expression body = null;
- Expect(38);
+ Expect(39);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -2549,10 +2572,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo BoundVar/*!*/ bv;
Expression/*!*/ body;
- Expect(61);
+ Expect(62);
x = t;
Ident(out id);
- if (la.kind == 33) {
+ if (la.kind == 22) {
Get();
IdentTypeOptional(out bv);
arguments.Add(bv);
@@ -2561,9 +2584,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv);
arguments.Add(bv);
}
- Expect(34);
+ Expect(24);
}
- Expect(62);
+ Expect(63);
Expression(out body);
c = new MatchCaseExpr(x, id.val, arguments, body);
}
@@ -2617,27 +2640,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
- {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
+ {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,T,x, x,x,x,T, T,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, x,T,x,T, T,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,T, x,x,x,x, T,x,x,x, T,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,x,x, x,x,x,T, T,T,x,T, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x},
+ {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,x, x,T,T,T, x,x,x,x, x,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x},
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,x,x, T,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
};
} // end Parser
@@ -2684,62 +2707,62 @@ public class Errors { case 19: s = "\"var\" expected"; break;
case 20: s = "\",\" expected"; break;
case 21: s = "\"type\" expected"; break;
- case 22: s = "\"<\" expected"; break;
- case 23: s = "\">\" expected"; break;
- case 24: s = "\"method\" expected"; break;
- case 25: s = "\"constructor\" expected"; break;
- case 26: s = "\"returns\" expected"; break;
- case 27: s = "\"...\" expected"; break;
- case 28: s = "\"modifies\" expected"; break;
- case 29: s = "\"free\" expected"; break;
- case 30: s = "\"requires\" expected"; break;
- case 31: s = "\"ensures\" expected"; break;
- case 32: s = "\"decreases\" expected"; break;
- case 33: s = "\"(\" expected"; break;
- case 34: s = "\")\" expected"; break;
- case 35: s = "\"bool\" expected"; break;
- case 36: s = "\"nat\" expected"; break;
- case 37: s = "\"int\" expected"; break;
- case 38: s = "\"set\" expected"; break;
- case 39: s = "\"multiset\" expected"; break;
- case 40: s = "\"seq\" expected"; break;
- case 41: s = "\"map\" expected"; break;
- case 42: s = "\"object\" expected"; break;
- case 43: s = "\".\" expected"; break;
- case 44: s = "\"function\" expected"; break;
- case 45: s = "\"predicate\" expected"; break;
- case 46: s = "\"reads\" expected"; break;
- case 47: s = "\"*\" expected"; break;
- case 48: s = "\"`\" expected"; break;
- case 49: s = "\"label\" expected"; break;
- case 50: s = "\"break\" expected"; break;
- case 51: s = "\"return\" expected"; break;
- case 52: s = "\":=\" expected"; break;
- case 53: s = "\":|\" expected"; break;
- case 54: s = "\"assume\" expected"; break;
- case 55: s = "\"new\" expected"; break;
- case 56: s = "\"[\" expected"; break;
- case 57: s = "\"]\" expected"; break;
- case 58: s = "\"choose\" expected"; break;
- case 59: s = "\"if\" expected"; break;
- case 60: s = "\"else\" expected"; break;
- case 61: s = "\"case\" expected"; break;
- case 62: s = "\"=>\" expected"; break;
- case 63: s = "\"while\" expected"; break;
- case 64: s = "\"invariant\" expected"; break;
- case 65: s = "\"match\" expected"; break;
- case 66: s = "\"assert\" expected"; break;
- case 67: s = "\"print\" expected"; break;
- case 68: s = "\"parallel\" expected"; break;
- case 69: s = "\"<==>\" expected"; break;
- case 70: s = "\"\\u21d4\" expected"; break;
- case 71: s = "\"==>\" expected"; break;
- case 72: s = "\"\\u21d2\" expected"; break;
- case 73: s = "\"&&\" expected"; break;
- case 74: s = "\"\\u2227\" expected"; break;
- case 75: s = "\"||\" expected"; break;
- case 76: s = "\"\\u2228\" expected"; break;
- case 77: s = "\"==\" expected"; break;
+ case 22: s = "\"(\" expected"; break;
+ case 23: s = "\"==\" expected"; break;
+ case 24: s = "\")\" expected"; break;
+ case 25: s = "\"<\" expected"; break;
+ case 26: s = "\">\" expected"; break;
+ case 27: s = "\"method\" expected"; break;
+ case 28: s = "\"constructor\" expected"; break;
+ case 29: s = "\"returns\" expected"; break;
+ case 30: s = "\"...\" expected"; break;
+ case 31: s = "\"modifies\" expected"; break;
+ case 32: s = "\"free\" expected"; break;
+ case 33: s = "\"requires\" expected"; break;
+ case 34: s = "\"ensures\" expected"; break;
+ case 35: s = "\"decreases\" expected"; break;
+ case 36: s = "\"bool\" expected"; break;
+ case 37: s = "\"nat\" expected"; break;
+ case 38: s = "\"int\" expected"; break;
+ case 39: s = "\"set\" expected"; break;
+ case 40: s = "\"multiset\" expected"; break;
+ case 41: s = "\"seq\" expected"; break;
+ case 42: s = "\"map\" expected"; break;
+ case 43: s = "\"object\" expected"; break;
+ case 44: s = "\".\" expected"; break;
+ case 45: s = "\"function\" expected"; break;
+ case 46: s = "\"predicate\" expected"; break;
+ case 47: s = "\"reads\" expected"; break;
+ case 48: s = "\"*\" expected"; break;
+ case 49: s = "\"`\" expected"; break;
+ case 50: s = "\"label\" expected"; break;
+ case 51: s = "\"break\" expected"; break;
+ case 52: s = "\"return\" expected"; break;
+ case 53: s = "\":=\" expected"; break;
+ case 54: s = "\":|\" expected"; break;
+ case 55: s = "\"assume\" expected"; break;
+ case 56: s = "\"new\" expected"; break;
+ case 57: s = "\"[\" expected"; break;
+ case 58: s = "\"]\" expected"; break;
+ case 59: s = "\"choose\" expected"; break;
+ case 60: s = "\"if\" expected"; break;
+ case 61: s = "\"else\" expected"; break;
+ case 62: s = "\"case\" expected"; break;
+ case 63: s = "\"=>\" expected"; break;
+ case 64: s = "\"while\" expected"; break;
+ case 65: s = "\"invariant\" expected"; break;
+ case 66: s = "\"match\" expected"; break;
+ case 67: s = "\"assert\" expected"; break;
+ case 68: s = "\"print\" expected"; break;
+ case 69: s = "\"parallel\" expected"; break;
+ case 70: s = "\"<==>\" expected"; break;
+ case 71: s = "\"\\u21d4\" expected"; break;
+ case 72: s = "\"==>\" expected"; break;
+ case 73: s = "\"\\u21d2\" expected"; break;
+ case 74: s = "\"&&\" expected"; break;
+ case 75: s = "\"\\u2227\" expected"; break;
+ case 76: s = "\"||\" expected"; break;
+ case 77: s = "\"\\u2228\" expected"; break;
case 78: s = "\"<=\" expected"; break;
case 79: s = "\">=\" expected"; break;
case 80: s = "\"!=\" expected"; break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index fb46ba4b..498546c3 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -71,6 +71,9 @@ namespace Microsoft.Dafny { if (i++ != 0) { wr.WriteLine(); }
Indent(indent);
PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());
+ if (at.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {
+ wr.Write("(==)");
+ }
wr.WriteLine(";");
} else if (d is DatatypeDecl) {
if (i++ != 0) { wr.WriteLine(); }
@@ -149,6 +152,9 @@ namespace Microsoft.Dafny { foreach (TypeParameter tp in typeArgs) {
Contract.Assert(tp != null);
wr.Write("{0}{1}", sep, tp.Name);
+ if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Required) {
+ wr.Write("(==)");
+ }
sep = ", ";
}
wr.Write(">");
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 56006a7f..b7866bfd 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -135,7 +135,7 @@ namespace Microsoft.Dafny { if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
- return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, null);
+ return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, null);
} else if (d is IndDatatypeDecl) {
var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
@@ -165,7 +165,7 @@ namespace Microsoft.Dafny { }
TypeParameter CloneTypeParam(TypeParameter tp) {
- return new TypeParameter(Tok(tp.tok), tp.Name);
+ return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport);
}
MemberDecl CloneMember(MemberDecl member) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index f0990aa0..74e401a7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -426,9 +426,391 @@ namespace Microsoft.Dafny { }
}
}
+ // Inferred required equality support for datatypes and for Function and Method signatures
+ // First, do datatypes until a fixpoint is reached
+ bool inferredSomething;
+ do {
+ inferredSomething = false;
+ foreach (var d in declarations) {
+ if (d is DatatypeDecl) {
+ var dt = (DatatypeDecl)d;
+ foreach (var tp in dt.TypeArgs) {
+ if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
+ // here's our chance to infer the need for equality support
+ foreach (var ctor in dt.Ctors) {
+ foreach (var arg in ctor.Formals) {
+ if (InferRequiredEqualitySupport(tp, arg.Type)) {
+ tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
+ inferredSomething = true;
+ goto DONE_DT; // break out of the doubly-nested loop
+ }
+ }
+ }
+ DONE_DT: ;
+ }
+ }
+ }
+ }
+ } while (inferredSomething);
+ // Now do it for Function and Method signatures
+ foreach (var d in declarations) {
+ if (d is ClassDecl) {
+ var cl = (ClassDecl)d;
+ foreach (var member in cl.Members) {
+ if (!member.IsGhost) {
+ if (member is Function) {
+ var f = (Function)member;
+ foreach (var tp in f.TypeArgs) {
+ if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
+ // here's our chance to infer the need for equality support
+ if (InferRequiredEqualitySupport(tp, f.ResultType)) {
+ tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
+ } else {
+ foreach (var p in f.Formals) {
+ if (InferRequiredEqualitySupport(tp, p.Type)) {
+ tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
+ break;
+ }
+ }
+ }
+ }
+ }
+ } else if (member is Method) {
+ var m = (Method)member;
+ foreach (var tp in m.TypeArgs) {
+ if (tp.EqualitySupport == TypeParameter.EqualitySupportValue.Unspecified) {
+ // here's our chance to infer the need for equality support
+ foreach (var p in m.Ins) {
+ if (InferRequiredEqualitySupport(tp, p.Type)) {
+ tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
+ goto DONE;
+ }
+ }
+ foreach (var p in m.Outs) {
+ if (InferRequiredEqualitySupport(tp, p.Type)) {
+ tp.EqualitySupport = TypeParameter.EqualitySupportValue.InferredRequired;
+ goto DONE;
+ }
+ }
+ DONE: ;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ // Check that all == and != operators in non-ghost contexts are applied to equality-supporting types.
+ // Note that this check can only be done after determining which expressions are ghosts.
+ foreach (var d in declarations) {
+ if (d is ClassDecl) {
+ var cl = (ClassDecl)d;
+ foreach (var member in cl.Members) {
+ if (!member.IsGhost) {
+ if (member is Field) {
+ var f = (Field)member;
+ CheckEqualityTypes_Type(f.tok, f.Type);
+ } else if (member is Function) {
+ var f = (Function)member;
+ foreach (var p in f.Formals) {
+ if (!p.IsGhost) {
+ CheckEqualityTypes_Type(p.tok, p.Type);
+ }
+ }
+ CheckEqualityTypes_Type(f.tok, f.ResultType);
+ if (f.Body != null) {
+ CheckEqualityTypes(f.Body);
+ }
+ } else if (member is Method) {
+ var m = (Method)member;
+ foreach (var p in m.Ins) {
+ if (!p.IsGhost) {
+ CheckEqualityTypes_Type(p.tok, p.Type);
+ }
+ }
+ foreach (var p in m.Outs) {
+ if (!p.IsGhost) {
+ CheckEqualityTypes_Type(p.tok, p.Type);
+ }
+ }
+ if (m.Body != null) {
+ CheckEqualityTypes_Stmt(m.Body);
+ }
+ }
+ }
+ }
+ } else if (d is DatatypeDecl) {
+ var dt = (DatatypeDecl)d;
+ foreach (var ctor in dt.Ctors) {
+ foreach (var p in ctor.Formals) {
+ if (!p.IsGhost) {
+ CheckEqualityTypes_Type(p.tok, p.Type);
+ }
+ }
+ }
+ }
+ }
}
}
+ void CheckEqualityTypes_Stmt(Statement stmt) {
+ Contract.Requires(stmt != null);
+ if (stmt.IsGhost) {
+ return;
+ } else if (stmt is PrintStmt) {
+ var s = (PrintStmt)stmt;
+ foreach (var arg in s.Args) {
+ if (arg.E != null) {
+ CheckEqualityTypes(arg.E);
+ }
+ }
+ } else if (stmt is BreakStmt) {
+ } else if (stmt is ReturnStmt) {
+ var s = (ReturnStmt)stmt;
+ if (s.rhss != null) {
+ s.rhss.Iter(CheckEqualityTypes_Rhs);
+ }
+ } else if (stmt is AssignStmt) {
+ AssignStmt s = (AssignStmt)stmt;
+ CheckEqualityTypes(s.Lhs);
+ CheckEqualityTypes_Rhs(s.Rhs);
+ } else if (stmt is VarDecl) {
+ var s = (VarDecl)stmt;
+ s.SubStatements.Iter(CheckEqualityTypes_Stmt);
+ } else if (stmt is CallStmt) {
+ var s = (CallStmt)stmt;
+ CheckEqualityTypes(s.Receiver);
+ s.Args.Iter(CheckEqualityTypes);
+ s.Lhs.Iter(CheckEqualityTypes);
+
+ Contract.Assert(s.Method.TypeArgs.Count <= s.TypeArgumentSubstitutions.Count);
+ var i = 0;
+ foreach (var formalTypeArg in s.Method.TypeArgs) {
+ var actualTypeArg = s.TypeArgumentSubstitutions[formalTypeArg];
+ if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {
+ Error(s.Tok, "type parameter {0} ({1}) passed to method {2} must support equality (got {3}){4}", i, formalTypeArg.Name, s.Method.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));
+ }
+ i++;
+ }
+ } else if (stmt is BlockStmt) {
+ var s = (BlockStmt)stmt;
+ s.Body.Iter(CheckEqualityTypes_Stmt);
+ } else if (stmt is IfStmt) {
+ var s = (IfStmt)stmt;
+ if (s.Guard != null) {
+ CheckEqualityTypes(s.Guard);
+ }
+ s.SubStatements.Iter(CheckEqualityTypes_Stmt);
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ foreach (var alt in s.Alternatives) {
+ CheckEqualityTypes(alt.Guard);
+ alt.Body.Iter(CheckEqualityTypes_Stmt);
+ }
+ } else if (stmt is WhileStmt) {
+ var s = (WhileStmt)stmt;
+ if (s.Guard != null) {
+ CheckEqualityTypes(s.Guard);
+ }
+ CheckEqualityTypes_Stmt(s.Body);
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ foreach (var alt in s.Alternatives) {
+ CheckEqualityTypes(alt.Guard);
+ alt.Body.Iter(CheckEqualityTypes_Stmt);
+ }
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ CheckEqualityTypes(s.Range);
+ CheckEqualityTypes_Stmt(s.Body);
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ CheckEqualityTypes(s.Source);
+ foreach (MatchCaseStmt mc in s.Cases) {
+ mc.Body.Iter(CheckEqualityTypes_Stmt);
+ }
+ } else if (stmt is ConcreteSyntaxStatement) {
+ var s = (ConcreteSyntaxStatement)stmt;
+ s.ResolvedStatements.Iter(CheckEqualityTypes_Stmt);
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
+ }
+ }
+
+ void CheckEqualityTypes_Rhs(AssignmentRhs rhs) {
+ Contract.Requires(rhs != null);
+ rhs.SubExpressions.Iter(CheckEqualityTypes);
+ rhs.SubStatements.Iter(CheckEqualityTypes_Stmt);
+ }
+
+ void CheckEqualityTypes(Expression expr) {
+ Contract.Requires(expr != null);
+ if (expr is BinaryExpr) {
+ var e = (BinaryExpr)expr;
+ var t0 = e.E0.Type.Normalize();
+ var t1 = e.E1.Type.Normalize();
+ switch (e.Op) {
+ case BinaryExpr.Opcode.Eq:
+ case BinaryExpr.Opcode.Neq:
+ if (!t0.SupportsEquality) {
+ Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
+ } else if (!t1.SupportsEquality) {
+ Error(e.E1, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
+ }
+ break;
+ default:
+ switch (e.ResolvedOp) {
+ // Note, all operations on sets, multisets, and maps are guaranteed to work because of restrictions placed on how
+ // these types are instantiated. (Except: This guarantee does not apply to equality on maps, because the Range type
+ // of maps is not restricted, only the Domain type. However, the equality operator is checked above.)
+ case BinaryExpr.ResolvedOpcode.InSeq:
+ case BinaryExpr.ResolvedOpcode.NotInSeq:
+ case BinaryExpr.ResolvedOpcode.Prefix:
+ case BinaryExpr.ResolvedOpcode.ProperPrefix:
+ if (!t1.SupportsEquality) {
+ Error(e.E1, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t1, TypeEqualityErrorMessageHint(t1));
+ } else if (!t0.SupportsEquality) {
+ if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InSet || e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSeq) {
+ Error(e.E0, "{0} can only be applied to expressions of types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
+ } else {
+ Error(e.E0, "{0} can only be applied to expressions of sequence types that support equality (got {1}){2}", BinaryExpr.OpcodeString(e.Op), t0, TypeEqualityErrorMessageHint(t0));
+ }
+ }
+ break;
+ default:
+ break;
+ }
+ break;
+ }
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ foreach (var bv in e.BoundVars) {
+ CheckEqualityTypes_Type(bv.tok, bv.Type);
+ }
+ } else if (expr is LetExpr) {
+ var e = (LetExpr)expr;
+ foreach (var bv in e.Vars) {
+ CheckEqualityTypes_Type(bv.tok, bv.Type);
+ }
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ Contract.Assert(e.Function.TypeArgs.Count <= e.TypeArgumentSubstitutions.Count);
+ var i = 0;
+ foreach (var formalTypeArg in e.Function.TypeArgs) {
+ var actualTypeArg = e.TypeArgumentSubstitutions[formalTypeArg];
+ if (formalTypeArg.MustSupportEquality && !actualTypeArg.SupportsEquality) {
+ Error(e.tok, "type parameter {0} ({1}) passed to function {2} must support equality (got {3}){4}", i, formalTypeArg.Name, e.Function.Name, actualTypeArg, TypeEqualityErrorMessageHint(actualTypeArg));
+ }
+ i++;
+ }
+ }
+
+ foreach (var ee in expr.SubExpressions) {
+ CheckEqualityTypes(ee);
+ }
+ }
+
+ void CheckEqualityTypes_Type(IToken tok, Type type) {
+ Contract.Requires(tok != null);
+ Contract.Requires(type != null);
+ type = type.Normalize();
+ if (type is BasicType) {
+ // fine
+ } else if (type is SetType) {
+ var argType = ((SetType)type).Arg;
+ if (!argType.SupportsEquality) {
+ Error(tok, "set argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
+ }
+ CheckEqualityTypes_Type(tok, argType);
+
+ } else if (type is MultiSetType) {
+ var argType = ((MultiSetType)type).Arg;
+ if (!argType.SupportsEquality) {
+ Error(tok, "multiset argument type must support equality (got {0}){1}", argType, TypeEqualityErrorMessageHint(argType));
+ }
+ CheckEqualityTypes_Type(tok, argType);
+
+ } else if (type is MapType) {
+ var mt = (MapType)type;
+ if (!mt.Domain.SupportsEquality) {
+ Error(tok, "map domain type must support equality (got {0}){1}", mt.Domain, TypeEqualityErrorMessageHint(mt.Domain));
+ }
+ CheckEqualityTypes_Type(tok, mt.Domain);
+ CheckEqualityTypes_Type(tok, mt.Range);
+
+ } else if (type is SeqType) {
+ Type argType = ((SeqType)type).Arg;
+ CheckEqualityTypes_Type(tok, argType);
+
+ } else if (type is UserDefinedType) {
+ var udt = (UserDefinedType)type;
+ if (udt.ResolvedClass != null) {
+ Contract.Assert(udt.ResolvedClass.TypeArgs.Count == udt.TypeArgs.Count);
+ var i = 0;
+ foreach (var argType in udt.TypeArgs) {
+ var formalTypeArg = udt.ResolvedClass.TypeArgs[i];
+ if (formalTypeArg.MustSupportEquality && !argType.SupportsEquality) {
+ Error(tok, "type parameter {0} ({1}) passed to type {2} must support equality (got {3}){4}", i, formalTypeArg.Name, udt.ResolvedClass.Name, argType, TypeEqualityErrorMessageHint(argType));
+ }
+ CheckEqualityTypes_Type(tok, argType);
+ i++;
+ }
+ } else {
+ Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments
+ }
+
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
+ }
+ }
+
+ string TypeEqualityErrorMessageHint(Type argType) {
+ Contract.Requires(argType != null);
+ var tp = argType.AsTypeParameter;
+ if (tp != null) {
+ return string.Format(" (perhaps try declaring type parameter '{0}' on line {1} as '{0}(==)', which says it can only be instantiated with a type that supports equality)", tp.Name, tp.tok.line);
+ }
+ return "";
+ }
+
+ bool InferRequiredEqualitySupport(TypeParameter tp, Type type) {
+ Contract.Requires(tp != null);
+ Contract.Requires(type != null);
+
+ type = type.Normalize();
+ if (type is BasicType) {
+ } else if (type is SetType) {
+ var st = (SetType)type;
+ return st.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, st.Arg);
+ } else if (type is MultiSetType) {
+ var ms = (MultiSetType)type;
+ return ms.Arg.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, ms.Arg);
+ } else if (type is MapType) {
+ var mt = (MapType)type;
+ return mt.Domain.AsTypeParameter == tp || InferRequiredEqualitySupport(tp, mt.Domain) || InferRequiredEqualitySupport(tp, mt.Range);
+ } else if (type is SeqType) {
+ var sq = (SeqType)type;
+ return InferRequiredEqualitySupport(tp, sq.Arg);
+ } else if (type is UserDefinedType) {
+ var udt = (UserDefinedType)type;
+ if (udt.ResolvedClass != null) {
+ var i = 0;
+ foreach (var argType in udt.TypeArgs) {
+ var formalTypeArg = udt.ResolvedClass.TypeArgs[i];
+ if ((formalTypeArg.MustSupportEquality && argType.AsTypeParameter == tp) || InferRequiredEqualitySupport(tp, argType)) {
+ return true;
+ }
+ i++;
+ }
+ } else {
+ Contract.Assert(udt.TypeArgs.Count == 0); // TypeParameters have no type arguments
+ }
+ } else {
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type
+ }
+ return false;
+ }
+
ClassDecl currentClass;
Function currentFunction;
readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
@@ -1133,7 +1515,7 @@ namespace Microsoft.Dafny { // In the remaining cases, proxy is a restricted proxy and t is a non-proxy
} else if (proxy is DatatypeProxy) {
- if (t.IsDatatype) {
+ if (t.IsIndDatatype) {
// all is fine, proxy can be redirected to t
} else {
return false;
@@ -1146,14 +1528,6 @@ namespace Microsoft.Dafny { return false;
}
- } else if (proxy is ObjectsTypeProxy) {
- if (t is ObjectType || UserDefinedType.DenotesClass(t) != null) {
- // all is good
- } else if (t is CollectionType) {
- proxy.T = new CollectionTypeProxy(new ObjectTypeProxy());
- return UnifyTypes(proxy.T, t);
- }
-
} else if (proxy is CollectionTypeProxy) {
CollectionTypeProxy collProxy = (CollectionTypeProxy)proxy;
if (t is CollectionType) {
@@ -1235,10 +1609,6 @@ namespace Microsoft.Dafny { // all is fine
a.T = b;
return true;
- } else if (b is ObjectsTypeProxy) {
- // unify a and b by redirecting b to a, since a gives the stronger requirement
- b.T = a;
- return true;
} else if (b is IndexableTypeProxy) {
// the intersection of ObjectTypeProxy and IndexableTypeProxy is an array type
a.T = builtIns.ArrayType(1, ((IndexableTypeProxy)b).Arg);
@@ -1248,37 +1618,6 @@ namespace Microsoft.Dafny { return false;
}
- } else if (a is ObjectsTypeProxy) {
- if (b is ObjectsTypeProxy) {
- // fine
- a.T = b;
- return true;
- } else if (b is CollectionTypeProxy) {
- // fine provided b's collection-element-type can be unified with object or a class type
- a.T = b;
- return UnifyTypes(((CollectionTypeProxy)b).Arg, new ObjectTypeProxy());
- } else if (b is OperationTypeProxy) {
- // fine; restrict a to sets of object/class, and restrict b to set/seq of object/class
- if (((OperationTypeProxy)b).AllowSeq) {
- a.T = new CollectionTypeProxy(new ObjectTypeProxy());
- b.T = a.T;
- } else {
- a.T = new SetType(new ObjectTypeProxy());
- b.T = a.T;
- }
- return true;
- } else if (b is IndexableTypeProxy) {
- IndexableTypeProxy pb = (IndexableTypeProxy)b;
- // the intersection of ObjectsTypeProxy and IndexableTypeProxy is
- // EITHER a sequence of ObjectTypeProxy OR an array of anything OR map of ObjectTypeProxy in either domain or range.
- // TODO: here, only the first of the three cases is supported
- b.T = new SeqType(pb.Arg);
- a.T = b.T;
- return UnifyTypes(pb.Arg, new ObjectTypeProxy());
- } else {
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected restricted-proxy type
- }
-
} else if (a is CollectionTypeProxy) {
if (b is CollectionTypeProxy) {
a.T = b;
@@ -2122,22 +2461,22 @@ namespace Microsoft.Dafny { UserDefinedType ctype = (UserDefinedType)nptype; // TODO: get rid of this statement, make this code handle any non-proxy type
#endif
// build the type substitution map
- Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ s.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
for (int i = 0; i < ctype.TypeArgs.Count; i++) {
- subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
+ s.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
}
foreach (TypeParameter p in callee.TypeArgs) {
- subst.Add(p, new ParamTypeProxy(p));
+ s.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));
}
// type check the arguments
for (int i = 0; i < callee.Ins.Count; i++) {
- Type st = SubstType(callee.Ins[i].Type, subst);
+ Type st = SubstType(callee.Ins[i].Type, s.TypeArgumentSubstitutions);
if (!UnifyTypes(cce.NonNull(s.Args[i].Type), st)) {
Error(s, "incorrect type of method in-parameter {0} (expected {1}, got {2})", i, st, s.Args[i].Type);
}
}
for (int i = 0; i < callee.Outs.Count; i++) {
- Type st = SubstType(callee.Outs[i].Type, subst);
+ Type st = SubstType(callee.Outs[i].Type, s.TypeArgumentSubstitutions);
var lhs = s.Lhs[i];
if (!UnifyTypes(cce.NonNull(lhs.Type), st)) {
Error(s, "incorrect type of method out-parameter {0} (expected {1}, got {2})", i, st, lhs.Type);
@@ -2925,12 +3264,12 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Le:
case BinaryExpr.Opcode.Add:
{
- if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsDatatype) {
+ if (e.Op == BinaryExpr.Opcode.Lt && e.E0.Type.IsIndDatatype) {
if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
expr.Type = Type.Bool;
- } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsDatatype) {
+ } else if (e.Op == BinaryExpr.Opcode.Lt && e.E1.Type.IsIndDatatype) {
if (!UnifyTypes(e.E0.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E0.Type);
}
@@ -2959,7 +3298,7 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Gt:
case BinaryExpr.Opcode.Ge:
{
- if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsDatatype) {
+ if (e.Op == BinaryExpr.Opcode.Gt && e.E0.Type.IsIndDatatype) {
if (!UnifyTypes(e.E1.Type, new DatatypeProxy())) {
Error(expr, "arguments to rank comparison must be datatypes (instead of {0})", e.E1.Type);
}
@@ -3467,24 +3806,24 @@ namespace Microsoft.Dafny { }
}
// build the type substitution map
- Dictionary<TypeParameter, Type> subst = new Dictionary<TypeParameter, Type>();
+ e.TypeArgumentSubstitutions = new Dictionary<TypeParameter, Type>();
for (int i = 0; i < ctype.TypeArgs.Count; i++) {
- subst.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
+ e.TypeArgumentSubstitutions.Add(cce.NonNull(ctype.ResolvedClass).TypeArgs[i], ctype.TypeArgs[i]);
}
foreach (TypeParameter p in function.TypeArgs) {
- subst.Add(p, new ParamTypeProxy(p));
+ e.TypeArgumentSubstitutions.Add(p, new ParamTypeProxy(p));
}
// type check the arguments
for (int i = 0; i < function.Formals.Count; i++) {
Expression farg = e.Args[i];
ResolveExpression(farg, twoState);
Contract.Assert(farg.Type != null); // follows from postcondition of ResolveExpression
- Type s = SubstType(function.Formals[i].Type, subst);
+ Type s = SubstType(function.Formals[i].Type, e.TypeArgumentSubstitutions);
if (!UnifyTypes(farg.Type, s)) {
Error(e, "incorrect type of function argument {0} (expected {1}, got {2})", i, s, farg.Type);
}
}
- e.Type = SubstType(function.ResultType, subst);
+ e.Type = SubstType(function.ResultType, e.TypeArgumentSubstitutions);
}
// Resolution termination check
@@ -4112,6 +4451,7 @@ namespace Microsoft.Dafny { Contract.Assert(e.Seq.Type != null); // follows from postcondition of ResolveExpression
Type elementType = new InferredTypeProxy();
Type domainType = new InferredTypeProxy();
+
IndexableTypeProxy expectedType = new IndexableTypeProxy(elementType, domainType);
if (!UnifyTypes(e.Seq.Type, expectedType)) {
Error(e, "sequence/array/map selection requires a sequence, array or map (got {0})", e.Seq.Type);
@@ -4197,7 +4537,7 @@ namespace Microsoft.Dafny { return BinaryExpr.ResolvedOpcode.Disjoint;
}
case BinaryExpr.Opcode.Lt:
- if (operandType.IsDatatype || operandType is DatatypeProxy) {
+ if (operandType.IsIndDatatype || operandType is DatatypeProxy) {
return BinaryExpr.ResolvedOpcode.RankLt;
} else if (operandType is SetType) {
return BinaryExpr.ResolvedOpcode.ProperSubset;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index d35fc22f..7cb302fa 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -265,11 +265,11 @@ public class Scanner { start[124] = 58;
start[59] = 19;
start[44] = 20;
+ start[40] = 21;
+ start[41] = 22;
start[60] = 59;
start[62] = 60;
start[46] = 61;
- start[40] = 22;
- start[41] = 23;
start[42] = 24;
start[96] = 25;
start[91] = 28;
@@ -498,40 +498,40 @@ public class Scanner { case "codatatype": t.kind = 15; break;
case "var": t.kind = 19; break;
case "type": t.kind = 21; break;
- case "method": t.kind = 24; break;
- case "constructor": t.kind = 25; break;
- case "returns": t.kind = 26; break;
- case "modifies": t.kind = 28; break;
- case "free": t.kind = 29; break;
- case "requires": t.kind = 30; break;
- case "ensures": t.kind = 31; break;
- case "decreases": t.kind = 32; break;
- case "bool": t.kind = 35; break;
- case "nat": t.kind = 36; break;
- case "int": t.kind = 37; break;
- case "set": t.kind = 38; break;
- case "multiset": t.kind = 39; break;
- case "seq": t.kind = 40; break;
- case "map": t.kind = 41; break;
- case "object": t.kind = 42; break;
- case "function": t.kind = 44; break;
- case "predicate": t.kind = 45; break;
- case "reads": t.kind = 46; break;
- case "label": t.kind = 49; break;
- case "break": t.kind = 50; break;
- case "return": t.kind = 51; break;
- case "assume": t.kind = 54; break;
- case "new": t.kind = 55; break;
- case "choose": t.kind = 58; break;
- case "if": t.kind = 59; break;
- case "else": t.kind = 60; break;
- case "case": t.kind = 61; break;
- case "while": t.kind = 63; break;
- case "invariant": t.kind = 64; break;
- case "match": t.kind = 65; break;
- case "assert": t.kind = 66; break;
- case "print": t.kind = 67; break;
- case "parallel": t.kind = 68; break;
+ case "method": t.kind = 27; break;
+ case "constructor": t.kind = 28; break;
+ case "returns": t.kind = 29; break;
+ case "modifies": t.kind = 31; break;
+ case "free": t.kind = 32; break;
+ case "requires": t.kind = 33; break;
+ case "ensures": t.kind = 34; break;
+ case "decreases": t.kind = 35; break;
+ case "bool": t.kind = 36; break;
+ case "nat": t.kind = 37; break;
+ case "int": t.kind = 38; break;
+ case "set": t.kind = 39; break;
+ case "multiset": t.kind = 40; break;
+ case "seq": t.kind = 41; break;
+ case "map": t.kind = 42; break;
+ case "object": t.kind = 43; break;
+ case "function": t.kind = 45; break;
+ case "predicate": t.kind = 46; break;
+ case "reads": t.kind = 47; break;
+ case "label": t.kind = 50; break;
+ case "break": t.kind = 51; break;
+ case "return": t.kind = 52; break;
+ case "assume": t.kind = 55; break;
+ case "new": t.kind = 56; break;
+ case "choose": t.kind = 59; break;
+ case "if": t.kind = 60; break;
+ case "else": t.kind = 61; break;
+ case "case": t.kind = 62; break;
+ case "while": t.kind = 64; break;
+ case "invariant": t.kind = 65; break;
+ case "match": t.kind = 66; break;
+ case "assert": t.kind = 67; break;
+ case "print": t.kind = 68; break;
+ case "parallel": t.kind = 69; break;
case "in": t.kind = 82; break;
case "false": t.kind = 92; break;
case "true": t.kind = 93; break;
@@ -652,47 +652,47 @@ public class Scanner { case 20:
{t.kind = 20; break;}
case 21:
- {t.kind = 27; break;}
+ {t.kind = 22; break;}
case 22:
- {t.kind = 33; break;}
+ {t.kind = 24; break;}
case 23:
- {t.kind = 34; break;}
+ {t.kind = 30; break;}
case 24:
- {t.kind = 47; break;}
- case 25:
{t.kind = 48; break;}
+ case 25:
+ {t.kind = 49; break;}
case 26:
- {t.kind = 52; break;}
- case 27:
{t.kind = 53; break;}
+ case 27:
+ {t.kind = 54; break;}
case 28:
- {t.kind = 56; break;}
- case 29:
{t.kind = 57; break;}
+ case 29:
+ {t.kind = 58; break;}
case 30:
- {t.kind = 62; break;}
+ {t.kind = 63; break;}
case 31:
if (ch == '>') {AddCh(); goto case 32;}
else {goto case 0;}
case 32:
- {t.kind = 69; break;}
- case 33:
{t.kind = 70; break;}
- case 34:
+ case 33:
{t.kind = 71; break;}
- case 35:
+ case 34:
{t.kind = 72; break;}
+ case 35:
+ {t.kind = 73; break;}
case 36:
if (ch == '&') {AddCh(); goto case 37;}
else {goto case 0;}
case 37:
- {t.kind = 73; break;}
- case 38:
{t.kind = 74; break;}
- case 39:
+ case 38:
{t.kind = 75; break;}
- case 40:
+ case 39:
{t.kind = 76; break;}
+ case 40:
+ {t.kind = 77; break;}
case 41:
{t.kind = 79; break;}
case 42:
@@ -731,41 +731,41 @@ public class Scanner { else {t.kind = 5; break;}
case 57:
recEnd = pos; recKind = 16;
- if (ch == '>') {AddCh(); goto case 30;}
- else if (ch == '=') {AddCh(); goto case 63;}
+ if (ch == '=') {AddCh(); goto case 63;}
+ else if (ch == '>') {AddCh(); goto case 30;}
else {t.kind = 16; break;}
case 58:
recEnd = pos; recKind = 17;
if (ch == '|') {AddCh(); goto case 39;}
else {t.kind = 17; break;}
case 59:
- recEnd = pos; recKind = 22;
+ recEnd = pos; recKind = 25;
if (ch == '=') {AddCh(); goto case 64;}
- else {t.kind = 22; break;}
+ else {t.kind = 25; break;}
case 60:
- recEnd = pos; recKind = 23;
+ recEnd = pos; recKind = 26;
if (ch == '=') {AddCh(); goto case 41;}
- else {t.kind = 23; break;}
+ else {t.kind = 26; break;}
case 61:
- recEnd = pos; recKind = 43;
+ recEnd = pos; recKind = 44;
if (ch == '.') {AddCh(); goto case 65;}
- else {t.kind = 43; break;}
+ else {t.kind = 44; break;}
case 62:
recEnd = pos; recKind = 83;
if (ch == '=') {AddCh(); goto case 42;}
else if (ch == '!') {AddCh(); goto case 43;}
else {t.kind = 83; break;}
case 63:
- recEnd = pos; recKind = 77;
+ recEnd = pos; recKind = 23;
if (ch == '>') {AddCh(); goto case 34;}
- else {t.kind = 77; break;}
+ else {t.kind = 23; break;}
case 64:
recEnd = pos; recKind = 78;
if (ch == '=') {AddCh(); goto case 31;}
else {t.kind = 78; break;}
case 65:
recEnd = pos; recKind = 100;
- if (ch == '.') {AddCh(); goto case 21;}
+ if (ch == '.') {AddCh(); goto case 23;}
else {t.kind = 100; break;}
}
diff --git a/Test/VSI-Benchmarks/b4.dfy b/Test/VSI-Benchmarks/b4.dfy index b70ff4d0..76e1ffa7 100644 --- a/Test/VSI-Benchmarks/b4.dfy +++ b/Test/VSI-Benchmarks/b4.dfy @@ -14,7 +14,7 @@ // that the specification can use mathematical sequences while the
// implementation uses a linked list.
-class Map<Key,Value> {
+class Map<Key(==),Value> {
ghost var Keys: seq<Key>;
ghost var Values: seq<Value>;
ghost var Repr: set<object>;
diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy index 383bccfd..2149df25 100644 --- a/Test/VSI-Benchmarks/b8.dfy +++ b/Test/VSI-Benchmarks/b8.dfy @@ -250,7 +250,7 @@ class WriterStream { -class Map<Key,Value> {
+class Map<Key(==),Value> {
var keys: seq<Key>;
var values: seq<Value>;
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index e8b618d7..40df1135 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -294,7 +294,7 @@ method QuantifierRange1<T>(a: seq<T>, x: T, y: T, N: int) assert x != y;
}
-method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int)
+method QuantifierRange2<T(==)>(a: seq<T>, x: T, y: T, N: int)
requires 0 <= N && N <= |a|;
requires exists k | 0 <= k && k < N :: a[k] == y;
ensures forall k | 0 <= k && k < N :: a[k] == y; // error
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index d6804661..cb9b5660 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -1,11 +1,11 @@ -class C<U> {
+class C<U(==)> {
method M<T>(x: T, u: U) returns (y: T)
ensures x == y && u == u;
{
y := x;
}
- function method F<X>(x: X, u: U): bool
+ function method F<X(==)>(x: X, u: U): bool
{
x == x && u == u
}
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 21b895aa..4c761671 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -10,7 +10,7 @@ static function IsCelebrity<Person>(c: Person, people: set<Person>): bool }
method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
- requires (exists c :: IsCelebrity(c, people));
+ requires exists c :: IsCelebrity(c, people);
ensures r == c;
{
var cc; assume cc == c; // this line essentially converts ghost c to non-ghost cc
diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy index c8419890..c78d5e81 100644 --- a/Test/dafny1/UltraFilter.dfy +++ b/Test/dafny1/UltraFilter.dfy @@ -1,6 +1,6 @@ // ultra filter
-class UltraFilter<G> {
+class UltraFilter<G(==)> {
static function IsFilter(f: set<set<G>>, S: set<G>): bool
{
(forall A, B :: A in f && A <= B ==> B in f) &&
diff --git a/Test/dafny2/MajorityVote.dfy b/Test/dafny2/MajorityVote.dfy index a7512486..af67ee92 100644 --- a/Test/dafny2/MajorityVote.dfy +++ b/Test/dafny2/MajorityVote.dfy @@ -31,6 +31,10 @@ // choice, if there is such a choice, and then passes in that choice as the ghost parameter K
// to the main algorithm. Neat, huh?
+// Language comment:
+// The "(==)" that sits after some type parameters in this program says that the actual
+// type argument must support equality.
+
// Advanced remark:
// There is a subtle situation in the verification of DetermineElection. Suppose the type
// parameter Candidate denotes some type whose instances depend on which object are
@@ -47,7 +51,7 @@ // to the Count function. Alternatively, one could have added the antecedent "c in a" or
// "old(allocated(c))" to the "forall c" quantification in the postcondition of DetermineElection.
-function method Count<T>(a: seq<T>, s: int, t: int, x: T): int
+function method Count<T(==)>(a: seq<T>, s: int, t: int, x: T): int
requires 0 <= s <= t <= |a|;
ensures Count(a, s, t, x) == 0 || x in a;
{
@@ -57,7 +61,7 @@ function method Count<T>(a: seq<T>, s: int, t: int, x: T): int // Here is the first version of the algorithm, the one that assumes there is a majority choice.
-method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
+method FindWinner<Candidate(==)>(a: seq<Candidate>, ghost K: Candidate) returns (k: Candidate)
requires 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
ensures k == K; // find K
{
@@ -93,7 +97,7 @@ method FindWinner<Candidate>(a: seq<Candidate>, ghost K: Candidate) returns (k: // Here is the second version of the program, the one that also computes whether or not
// there is a majority choice.
-method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
+method DetermineElection<Candidate(==)>(a: seq<Candidate>) returns (hasWinner: bool, cand: Candidate)
ensures hasWinner ==> 2 * Count(a, 0, |a|, cand) > |a|;
ensures !hasWinner ==> forall c :: 2 * Count(a, 0, |a|, c) <= |a|;
{
@@ -107,7 +111,7 @@ method DetermineElection<Candidate>(a: seq<Candidate>) returns (hasWinner: bool, // antecedent "hasWinner ==>" and the two checks for no-more-votes that may result in a "return"
// statement.
-method SearchForWinner<Candidate>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
+method SearchForWinner<Candidate(==)>(a: seq<Candidate>, ghost hasWinner: bool, ghost K: Candidate) returns (k: Candidate)
requires hasWinner ==> 2 * Count(a, 0, |a|, K) > |a|; // K has a (strict) majority of the votes
ensures hasWinner ==> k == K; // find K
{
diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy index 5153b053..4373136b 100644 --- a/Test/vstte2012/BreadthFirstSearch.dfy +++ b/Test/vstte2012/BreadthFirstSearch.dfy @@ -1,4 +1,4 @@ -class BreadthFirstSearch<Vertex>
+class BreadthFirstSearch<Vertex(==)>
{
// The following function is left uninterpreted (for the purpose of the
// verification problem, it can be thought of as a parameter to the class)
|