summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-08-20 20:21:47 -0700
committerGravatar leino <unknown>2014-08-20 20:21:47 -0700
commit61d55705cdf6a710f1a21ddb2ae2caaa314ca7f6 (patch)
treeeb71616351742e3e1e5b56b334065df860a904af
parent3b51d9251d78bd3de763c951102677eecd764984 (diff)
Start of derived types (aka "new types")
Fixed bug in type checking for integer division.
Diffstat
-rw-r--r--Source/Dafny/Cloner.cs3
-rw-r--r--Source/Dafny/Compiler.cs8
-rw-r--r--Source/Dafny/Dafny.atg8
-rw-r--r--Source/Dafny/DafnyAst.cs61
-rw-r--r--Source/Dafny/Parser.cs796
-rw-r--r--Source/Dafny/Printer.cs8
-rw-r--r--Source/Dafny/RefinementTransformer.cs7
-rw-r--r--Source/Dafny/Resolver.cs49
-rw-r--r--Source/Dafny/Scanner.cs82
-rw-r--r--Source/Dafny/Translator.cs26
-rw-r--r--Test/dafny0/DerivedTypesResolution.dfy27
-rw-r--r--Test/dafny0/DerivedTypesResolution.dfy.expect3
-rw-r--r--Test/dafny0/ResolutionErrors.dfy9
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect15
14 files changed, 627 insertions, 475 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index f4315041..8174f5aa 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -34,6 +34,9 @@ namespace Microsoft.Dafny
var dd = (TypeSynonymDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
return new TypeSynonymDecl(Tok(dd.tok), dd.Name, tps, m, CloneType(dd.Rhs), CloneAttributes(dd.Attributes));
+ } else if (d is DerivedTypeDecl) {
+ var dd = (DerivedTypeDecl)d;
+ return new DerivedTypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes));
} else if (d is TupleTypeDecl) {
var dd = (TupleTypeDecl)d;
return new TupleTypeDecl(dd.Dims, dd.Module);
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 0ea3d4a3..bba99355 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -117,6 +117,8 @@ namespace Microsoft.Dafny {
Error("Opaque type ('{0}') cannot be compiled", at.FullName);
} else if (d is TypeSynonymDecl) {
// do nothing, just bypass type synonyms in the compiler
+ } else if (d is DerivedTypeDecl) {
+ // do nothing, just bypass derived types in the compiler
} else if (d is DatatypeDecl) {
var dt = (DatatypeDecl)d;
Indent(indent);
@@ -968,6 +970,8 @@ namespace Microsoft.Dafny {
return "BigInteger";
} else if (type is RealType) {
return "Dafny.BigRational";
+ } else if (type.AsDerivedType != null) {
+ return TypeName(type.AsDerivedType.BaseType);
} else if (type is ObjectType) {
return "object";
} else if (type.IsArrayType) {
@@ -1058,6 +1062,8 @@ namespace Microsoft.Dafny {
return "BigInteger.Zero";
} else if (type is RealType) {
return "Dafny.BigRational.ZERO";
+ } else if (type.AsDerivedType != null) {
+ return DefaultValue(type.AsDerivedType.BaseType);
} else if (type.IsRefType) {
return string.Format("({0})null", TypeName(type));
} else if (type.IsDatatype) {
@@ -1068,7 +1074,7 @@ namespace Microsoft.Dafny {
}
return string.Format("new {0}()", s);
} else if (type.IsTypeParameter) {
- UserDefinedType udt = (UserDefinedType)type;
+ var udt = (UserDefinedType)type;
return "default(@" + udt.FullCompileName + ")";
} else if (type is SetType) {
return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index a9473202..e136a3de 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -462,7 +462,13 @@ OtherTypeDecl<ModuleDefinition/*!*/ module, out TopLevelDecl td>
|
[ GenericParameters<typeArgs> ]
[ "="
- Type<out ty> (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)
+ ( "new"
+ Type<out ty> (. if (typeArgs.Count != 0) {
+ SemErr(typeArgs[0].tok, "a derived type is not allowed type arguments");
+ }
+ td = new DerivedTypeDecl(id, id.val, module, ty, attrs); .)
+ | Type<out ty> (. td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); .)
+ )
]
) (. if (td == null) {
td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 08d05fab..005dbc44 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -364,6 +364,12 @@ namespace Microsoft.Dafny {
public bool IsSubrangeType {
get { return NormalizeExpand() is NatType; }
}
+ public bool IsNumericBased {
+ get {
+ var t = NormalizeExpand();
+ return t.IsIntegerType || t.IsRealType || t.AsDerivedType != null;
+ }
+ }
public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } }
public SetType AsSetType { get { return NormalizeExpand() as SetType; } }
@@ -395,6 +401,12 @@ namespace Microsoft.Dafny {
return udt == null ? null : udt.ResolvedClass as ArrayClassDecl;
}
}
+ public DerivedTypeDecl AsDerivedType {
+ get {
+ var udt = NormalizeExpand() as UserDefinedType;
+ return udt == null ? null : udt.ResolvedClass as DerivedTypeDecl;
+ }
+ }
public TypeSynonymDecl AsTypeSynonym {
get {
var udt = this as UserDefinedType; // note, it is important to use 'this' here, not 'this.NormalizeExpand()'
@@ -405,6 +417,16 @@ namespace Microsoft.Dafny {
}
}
}
+ public RedirectingTypeDecl AsRedirectingType {
+ get {
+ var udt = this as UserDefinedType; // Note, it is important to use 'this' here, not 'this.NormalizeExpand()'. This property getter is intended to be used during resolution.
+ if (udt == null) {
+ return null;
+ } else {
+ return (RedirectingTypeDecl)(udt.ResolvedClass as TypeSynonymDecl) ?? udt.ResolvedClass as DerivedTypeDecl;
+ }
+ }
+ }
public bool IsDatatype {
get {
return AsDatatype != null;
@@ -966,7 +988,7 @@ namespace Microsoft.Dafny {
public override bool SupportsEquality {
get {
- if (ResolvedClass is ClassDecl) {
+ if (ResolvedClass is ClassDecl || ResolvedClass is DerivedTypeDecl) {
return true;
} else if (ResolvedClass is CoDatatypeDecl) {
return false;
@@ -1114,16 +1136,16 @@ namespace Microsoft.Dafny {
}
/// <summary>
- /// This proxy stands for either:
- /// int or real or set or multiset or seq
- /// if AllowSeq, or:
- /// int or real or set or multiset
- /// if !AllowSeq.
+ /// This proxy can stand for any numeric type.
+ /// In addition, if AllowSeq, then it can stand for a seq.
+ /// In addition, if AllowSetVarieties, it can stand for a set or multiset.
/// </summary>
public class OperationTypeProxy : RestrictedTypeProxy {
public readonly bool AllowSeq;
- public OperationTypeProxy(bool allowSeq) {
+ public readonly bool AllowSetVarieties;
+ public OperationTypeProxy(bool allowSeq, bool allowSetVarieties) {
AllowSeq = allowSeq;
+ AllowSetVarieties = allowSetVarieties;
}
public override int OrderID {
get {
@@ -2113,7 +2135,28 @@ namespace Microsoft.Dafny {
}
}
- public class TypeSynonymDecl : TopLevelDecl
+ public interface RedirectingTypeDecl
+ {
+ IToken Tok { get; }
+ string Name { get; }
+ }
+
+ public class DerivedTypeDecl : TopLevelDecl, RedirectingTypeDecl
+ {
+ public readonly Type BaseType;
+ public DerivedTypeDecl(IToken tok, string name, ModuleDefinition module, Type baseType, Attributes attributes)
+ : base(tok, name, module, new List<TypeParameter>(), attributes) {
+ Contract.Requires(tok != null);
+ Contract.Requires(name != null);
+ Contract.Requires(module != null);
+ Contract.Requires(baseType != null);
+ BaseType = baseType;
+ }
+ IToken RedirectingTypeDecl.Tok { get { return tok; } }
+ string RedirectingTypeDecl.Name { get { return Name; } }
+ }
+
+ public class TypeSynonymDecl : TopLevelDecl, RedirectingTypeDecl
{
public readonly Type Rhs;
public TypeSynonymDecl(IToken tok, string name, List<TypeParameter> typeArgs, ModuleDefinition module, Type rhs, Attributes attributes)
@@ -2140,6 +2183,8 @@ namespace Microsoft.Dafny {
return Resolver.SubstType(Rhs, subst);
}
}
+ IToken RedirectingTypeDecl.Tok { get { return tok; } }
+ string RedirectingTypeDecl.Name { get { return Name; } }
}
[ContractClass(typeof(IVariableContracts))]
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 1a8e0e3c..3eff2f87 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -307,7 +307,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
defaultModule.TopLevelDecls.Add(td);
break;
}
- case 40: {
+ case 41: {
IteratorDecl(defaultModule, out iter);
defaultModule.TopLevelDecls.Add(iter);
break;
@@ -317,7 +317,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
defaultModule.TopLevelDecls.Add(trait);
break;
}
- case 31: case 32: case 36: case 46: case 47: case 48: case 49: case 50: case 66: case 67: case 68: {
+ case 31: case 32: case 36: case 47: case 48: case 49: case 50: case 51: case 67: case 68: case 69: {
ClassMemberDecl(membersDefaultClass, false);
break;
}
@@ -394,12 +394,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
module.TopLevelDecls.Add(td);
break;
}
- case 40: {
+ case 41: {
IteratorDecl(module, out iter);
module.TopLevelDecls.Add(iter);
break;
}
- case 31: case 32: case 36: case 46: case 47: case 48: case 49: case 50: case 66: case 67: case 68: {
+ case 31: case 32: case 36: case 47: case 48: case 49: case 50: case 51: case 67: case 68: case 69: {
ClassMemberDecl(namedModuleDefaultClassMembers, false);
break;
}
@@ -460,7 +460,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
if (la.kind == 29) {
@@ -500,7 +500,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
Expect(25);
@@ -542,25 +542,34 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Expect(39);
Expect(16);
eqSupport = TypeParameter.EqualitySupportValue.Required;
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
} else if (StartOf(3)) {
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
if (la.kind == 25) {
Get();
- Type(out ty);
- td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs);
+ if (la.kind == 40) {
+ Get();
+ Type(out ty);
+ if (typeArgs.Count != 0) {
+ SemErr(typeArgs[0].tok, "a derived type is not allowed type arguments");
+ }
+ td = new DerivedTypeDecl(id, id.val, module, ty, attrs);
+ } else if (StartOf(4)) {
+ Type(out ty);
+ td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs);
+ } else SynErr(136);
}
- } else SynErr(136);
+ } else SynErr(137);
if (td == null) {
td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs);
}
if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(137); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(138); Get();}
Get();
}
}
@@ -589,19 +598,19 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(la.kind == 0 || la.kind == 40)) {SynErr(138); Get();}
- Expect(40);
+ while (!(la.kind == 0 || la.kind == 41)) {SynErr(139); Get();}
+ Expect(41);
while (la.kind == 13) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 15 || la.kind == 44) {
- if (la.kind == 44) {
+ if (la.kind == 15 || la.kind == 45) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
Formals(true, true, ins, out openParen);
- if (la.kind == 41 || la.kind == 42) {
- if (la.kind == 41) {
+ if (la.kind == 42 || la.kind == 43) {
+ if (la.kind == 42) {
Get();
} else {
Get();
@@ -609,11 +618,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
Formals(false, true, outs, out openParen);
}
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(139);
- while (StartOf(4)) {
+ } else SynErr(140);
+ while (StartOf(5)) {
IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs);
}
if (la.kind == 13) {
@@ -639,13 +648,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
IToken bodyStart;
- while (!(la.kind == 0 || la.kind == 30)) {SynErr(140); Get();}
+ while (!(la.kind == 0 || la.kind == 30)) {SynErr(141); Get();}
Expect(30);
while (la.kind == 13) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
Expect(13);
@@ -677,13 +686,13 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
if (la.kind == 36) {
FieldDecl(mmod, mm);
- } else if (la.kind == 66 || la.kind == 67 || la.kind == 68) {
+ } else if (la.kind == 67 || la.kind == 68 || la.kind == 69) {
FunctionDecl(mmod, out f);
mm.Add(f);
- } else if (StartOf(5)) {
+ } else if (StartOf(6)) {
MethodDecl(mmod, allowConstructors, out m);
mm.Add(m);
- } else SynErr(141);
+ } else SynErr(142);
}
void Attribute(ref Attributes attrs) {
@@ -706,7 +715,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken id; IToken idPrime; ids = new List<IToken>();
Ident(out id);
ids.Add(id);
- while (la.kind == 65) {
+ while (la.kind == 66) {
IdentOrDigitsSuffix(out id, out idPrime);
ids.Add(id);
if (idPrime != null) { ids.Add(idPrime); }
@@ -725,7 +734,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
x = Token.NoToken;
y = null;
- Expect(65);
+ Expect(66);
if (la.kind == 1) {
Get();
x = t;
@@ -759,7 +768,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
} else if (la.kind == 11) {
Get();
x = t;
- } else SynErr(142);
+ } else SynErr(143);
}
void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {
@@ -767,7 +776,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken/*!*/ id;
TypeParameter.EqualitySupportValue eqSupport;
- Expect(44);
+ Expect(45);
NoUSIdent(out id);
eqSupport = TypeParameter.EqualitySupportValue.Unspecified;
if (la.kind == 15) {
@@ -789,7 +798,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
typeArgs.Add(new TypeParameter(id, id.val, eqSupport));
}
- Expect(45);
+ Expect(46);
}
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
@@ -797,7 +806,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attributes attrs = null;
IToken/*!*/ id; Type/*!*/ ty;
- while (!(la.kind == 0 || la.kind == 36)) {SynErr(143); Get();}
+ while (!(la.kind == 0 || la.kind == 36)) {SynErr(144); Get();}
Expect(36);
if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
@@ -811,7 +820,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
FIdentType(out id, out ty);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(144); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(145); Get();}
Expect(8);
}
@@ -834,9 +843,9 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken bodyEnd = Token.NoToken;
IToken signatureEllipsis = null;
- if (la.kind == 66) {
+ if (la.kind == 67) {
Get();
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
isFunctionMethod = true;
}
@@ -846,22 +855,22 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (la.kind == 15 || la.kind == 44) {
- if (la.kind == 44) {
+ if (la.kind == 15 || la.kind == 45) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
Formals(true, isFunctionMethod, formals, out openParen);
Expect(7);
Type(out returnType);
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(145);
- } else if (la.kind == 67) {
+ } else SynErr(146);
+ } else if (la.kind == 68) {
Get();
isPredicate = true;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
isFunctionMethod = true;
}
@@ -871,8 +880,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (StartOf(6)) {
- if (la.kind == 44) {
+ if (StartOf(7)) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
if (la.kind == 15) {
@@ -882,12 +891,12 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
SemErr(t, "predicates do not have an explicitly declared return type; it is always bool");
}
}
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(146);
- } else if (la.kind == 68) {
+ } else SynErr(147);
+ } else if (la.kind == 69) {
Get();
isCoPredicate = true;
if (mmod.IsGhost) { SemErr(t, "copredicates cannot be declared 'ghost' (they are ghost by default)"); }
@@ -896,8 +905,8 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Attribute(ref attrs);
}
NoUSIdent(out id);
- if (StartOf(6)) {
- if (la.kind == 44) {
+ if (StartOf(7)) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
if (la.kind == 15) {
@@ -907,14 +916,14 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
SemErr(t, "copredicates do not have an explicitly declared return type; it is always bool");
}
}
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
signatureEllipsis = t;
openParen = Token.NoToken;
- } else SynErr(147);
- } else SynErr(148);
+ } else SynErr(148);
+ } else SynErr(149);
decreases = isCoPredicate ? null : new List<Expression/*!*/>();
- while (StartOf(7)) {
+ while (StartOf(8)) {
FunctionSpec(reqs, reads, ens, decreases);
}
if (la.kind == 13) {
@@ -963,21 +972,21 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
IToken bodyStart = Token.NoToken;
IToken bodyEnd = Token.NoToken;
- while (!(StartOf(8))) {SynErr(149); Get();}
- if (la.kind == 46) {
+ while (!(StartOf(9))) {SynErr(150); Get();}
+ if (la.kind == 47) {
Get();
- } else if (la.kind == 47) {
+ } else if (la.kind == 48) {
Get();
isLemma = true;
- } else if (la.kind == 48) {
+ } else if (la.kind == 49) {
Get();
isCoLemma = true;
- } else if (la.kind == 49) {
+ } else if (la.kind == 50) {
Get();
isCoLemma = true;
errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'");
- } else if (la.kind == 50) {
+ } else if (la.kind == 51) {
Get();
if (allowConstructor) {
isConstructor = true;
@@ -985,7 +994,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
SemErr(t, "constructors are only allowed in classes");
}
- } else SynErr(150);
+ } else SynErr(151);
keywordToken = t;
if (isLemma) {
if (mmod.IsGhost) {
@@ -1018,21 +1027,21 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
}
- if (la.kind == 15 || la.kind == 44) {
- if (la.kind == 44) {
+ if (la.kind == 15 || la.kind == 45) {
+ if (la.kind == 45) {
GenericParameters(typeArgs);
}
Formals(true, !mmod.IsGhost, ins, out openParen);
- if (la.kind == 42) {
+ if (la.kind == 43) {
Get();
if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); }
Formals(false, !mmod.IsGhost, outs, out openParen);
}
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
signatureEllipsis = t; openParen = Token.NoToken;
- } else SynErr(151);
- while (StartOf(9)) {
+ } else SynErr(152);
+ while (StartOf(10)) {
MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs);
}
if (la.kind == 13) {
@@ -1084,7 +1093,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {
Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost;
Expect(15);
- if (StartOf(10)) {
+ if (StartOf(11)) {
TypeIdentOptional(out id, out name, out ty, out isGhost);
formals.Add(new Formal(id, name, ty, true, isGhost));
while (la.kind == 37) {
@@ -1105,7 +1114,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
} else if (la.kind == 2) {
Get();
id = t;
- } else SynErr(152);
+ } else SynErr(153);
Expect(7);
Type(out ty);
}
@@ -1175,7 +1184,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Get();
isGhost = true;
}
- if (StartOf(11)) {
+ if (StartOf(4)) {
TypeAndToken(out id, out ty);
if (la.kind == 7) {
Get();
@@ -1193,7 +1202,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
id = t; name = id.val;
Expect(7);
Type(out ty);
- } else SynErr(153);
+ } else SynErr(154);
if (name != null) {
identName = name;
} else {
@@ -1208,30 +1217,30 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
List<Type> gt = null;
switch (la.kind) {
- case 56: {
+ case 57: {
Get();
tok = t;
break;
}
- case 57: {
+ case 58: {
Get();
tok = t; ty = new NatType();
break;
}
- case 58: {
+ case 59: {
Get();
tok = t; ty = new IntType();
break;
}
- case 59: {
+ case 60: {
Get();
tok = t; ty = new RealType();
break;
}
- case 60: {
+ case 61: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1241,10 +1250,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 61: {
+ case 62: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1254,10 +1263,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 62: {
+ case 63: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericInstantiation(gt);
}
if (gt.Count > 1) {
@@ -1267,10 +1276,10 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 63: {
+ case 64: {
Get();
tok = t; gt = new List<Type/*!*/>();
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericInstantiation(gt);
}
if (gt.Count == 0) {
@@ -1287,7 +1296,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
case 15: {
Get();
tok = t; gt = new List<Type>();
- if (StartOf(11)) {
+ if (StartOf(4)) {
Type(out ty);
gt.Add(ty);
while (la.kind == 37) {
@@ -1308,11 +1317,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
break;
}
- case 1: case 5: case 64: {
+ case 1: case 5: case 65: {
ReferenceType(out tok, out ty);
break;
}
- default: SynErr(154); break;
+ default: SynErr(155); break;
}
if (la.kind == 10) {
Type t2;
@@ -1348,7 +1357,7 @@ List<MaybeFreeExpression/*!*/>/*!*/ yieldReq, List<MaybeFreeExpression/*!*/>/*!*
ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null;
- while (!(StartOf(12))) {SynErr(155); Get();}
+ while (!(StartOf(12))) {SynErr(156); Get();}
if (la.kind == 11) {
Get();
while (IsAttribute()) {
@@ -1363,9 +1372,9 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(156); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(157); Get();}
Expect(8);
- } else if (la.kind == 51) {
+ } else if (la.kind == 52) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1379,21 +1388,21 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(157); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(158); Get();}
Expect(8);
} else if (StartOf(14)) {
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
isFree = true;
}
- if (la.kind == 55) {
+ if (la.kind == 56) {
Get();
isYield = true;
}
if (la.kind == 12) {
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(158); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(159); Get();}
Expect(8);
if (isYield) {
yieldReq.Add(new MaybeFreeExpression(e, isFree));
@@ -1401,13 +1410,13 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
req.Add(new MaybeFreeExpression(e, isFree));
}
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(159); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(160); Get();}
Expect(8);
if (isYield) {
yieldEns.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
@@ -1415,16 +1424,16 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) {
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
}
- } else SynErr(160);
- } else if (la.kind == 54) {
+ } else SynErr(161);
+ } else if (la.kind == 55) {
Get();
while (IsAttribute()) {
Attribute(ref decrAttrs);
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(161); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(162); Get();}
Expect(8);
- } else SynErr(162);
+ } else SynErr(163);
}
void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {
@@ -1446,8 +1455,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; Attributes ensAttrs = null;
- while (!(StartOf(16))) {SynErr(163); Get();}
- if (la.kind == 51) {
+ while (!(StartOf(16))) {SynErr(164); Get();}
+ if (la.kind == 52) {
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -1461,38 +1470,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(164); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(165); Get();}
Expect(8);
- } else if (la.kind == 12 || la.kind == 52 || la.kind == 53) {
- if (la.kind == 52) {
+ } else if (la.kind == 12 || la.kind == 53 || la.kind == 54) {
+ if (la.kind == 53) {
Get();
isFree = true;
}
if (la.kind == 12) {
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(165); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(166); Get();}
Expect(8);
req.Add(new MaybeFreeExpression(e, isFree));
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
while (IsAttribute()) {
Attribute(ref ensAttrs);
}
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(166); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(167); Get();}
Expect(8);
ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs));
- } else SynErr(167);
- } else if (la.kind == 54) {
+ } else SynErr(168);
+ } else if (la.kind == 55) {
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(168); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(169); Get();}
Expect(8);
- } else SynErr(169);
+ } else SynErr(170);
}
void FrameExpression(out FrameExpression/*!*/ fe) {
@@ -1505,18 +1514,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (StartOf(17)) {
Expression(out e, false, false);
feTok = e.tok;
- if (la.kind == 69) {
+ if (la.kind == 70) {
Get();
Ident(out id);
fieldName = id.val; feTok = id;
}
fe = new FrameExpression(feTok, e, fieldName);
- } else if (la.kind == 69) {
+ } else if (la.kind == 70) {
Get();
Ident(out id);
fieldName = id.val;
fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName);
- } else SynErr(170);
+ } else SynErr(171);
}
void Expression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -1556,7 +1565,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void GenericInstantiation(List<Type/*!*/>/*!*/ gt) {
Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty;
- Expect(44);
+ Expect(45);
Type(out ty);
gt.Add(ty);
while (la.kind == 37) {
@@ -1564,7 +1573,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Type(out ty);
gt.Add(ty);
}
- Expect(45);
+ Expect(46);
}
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
@@ -1573,13 +1582,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Type> gt;
List<IToken> path;
- if (la.kind == 64) {
+ if (la.kind == 65) {
Get();
tok = t; ty = new ObjectType();
} else if (la.kind == 5) {
Get();
tok = t; gt = new List<Type>();
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericInstantiation(gt);
}
int dims = tok.val.Length == 5 ? 1 : int.Parse(tok.val.Substring(5));
@@ -1589,16 +1598,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out tok);
gt = new List<Type>();
path = new List<IToken>();
- while (la.kind == 65) {
+ while (la.kind == 66) {
path.Add(tok);
Get();
Ident(out tok);
}
- if (la.kind == 44) {
+ if (la.kind == 45) {
GenericInstantiation(gt);
}
ty = new UserDefinedType(tok, tok.val, gt, path);
- } else SynErr(171);
+ } else SynErr(172);
}
void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/> decreases) {
@@ -1607,10 +1616,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Contract.Requires(decreases == null || cce.NonNullElements(decreases));
Expression/*!*/ e; FrameExpression/*!*/ fe;
if (la.kind == 12) {
- while (!(la.kind == 0 || la.kind == 12)) {SynErr(172); Get();}
+ while (!(la.kind == 0 || la.kind == 12)) {SynErr(173); Get();}
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(173); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(174); Get();}
Expect(8);
reqs.Add(e);
} else if (la.kind == 11) {
@@ -1624,15 +1633,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
reads.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(174); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(175); Get();}
Expect(8);
- } else if (la.kind == 53) {
+ } else if (la.kind == 54) {
Get();
Expression(out e, false, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(175); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(176); Get();}
Expect(8);
ens.Add(e);
- } else if (la.kind == 54) {
+ } else if (la.kind == 55) {
Get();
if (decreases == null) {
SemErr(t, "'decreases' clauses are meaningless for copredicates, so they are not allowed");
@@ -1640,9 +1649,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
DecreasesList(decreases, false);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(176); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(177); Get();}
Expect(8);
- } else SynErr(177);
+ } else SynErr(178);
}
void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {
@@ -1661,7 +1670,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
fe = new FrameExpression(t, new WildcardExpr(t), null);
} else if (StartOf(13)) {
FrameExpression(out fe);
- } else SynErr(178);
+ } else SynErr(179);
}
void LambdaSpec(out Expression req, List<FrameExpression> reads) {
@@ -1693,7 +1702,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new WildcardExpr(t);
} else if (StartOf(17)) {
Expression(out e, false, false);
- } else SynErr(179);
+ } else SynErr(180);
}
void Stmt(List<Statement/*!*/>/*!*/ ss) {
@@ -1710,7 +1719,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken bodyStart, bodyEnd;
int breakCount;
- while (!(StartOf(19))) {SynErr(180); Get();}
+ while (!(StartOf(19))) {SynErr(181); Get();}
switch (la.kind) {
case 13: {
BlockStmt(out bs, out bodyStart, out bodyEnd);
@@ -1721,7 +1730,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
AssertStmt(out s);
break;
}
- case 76: {
+ case 77: {
AssumeStmt(out s);
break;
}
@@ -1729,7 +1738,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
PrintStmt(out s);
break;
}
- case 1: case 2: case 3: case 4: case 15: case 35: case 58: case 59: case 116: case 117: case 118: case 119: case 120: case 121: {
+ case 1: case 2: case 3: case 4: case 15: case 35: case 59: case 60: case 116: case 117: case 118: case 119: case 120: case 121: {
UpdateStmt(out s);
break;
}
@@ -1761,7 +1770,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ModifyStmt(out s);
break;
}
- case 70: {
+ case 71: {
Get();
x = t;
NoUSIdent(out id);
@@ -1770,32 +1779,32 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 71: {
+ case 72: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
NoUSIdent(out id);
label = id.val;
- } else if (la.kind == 8 || la.kind == 71) {
- while (la.kind == 71) {
+ } else if (la.kind == 8 || la.kind == 72) {
+ while (la.kind == 72) {
Get();
breakCount++;
}
- } else SynErr(181);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(182); Get();}
+ } else SynErr(182);
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(183); Get();}
Expect(8);
s = label != null ? new BreakStmt(x, t, label) : new BreakStmt(x, t, breakCount);
break;
}
- case 55: case 74: {
+ case 56: case 75: {
ReturnStmt(out s);
break;
}
- case 43: {
+ case 44: {
SkeletonStmt(out s);
break;
}
- default: SynErr(183); break;
+ default: SynErr(184); break;
}
}
@@ -1811,10 +1820,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
if (StartOf(17)) {
Expression(out e, false, true);
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
dotdotdot = t;
- } else SynErr(184);
+ } else SynErr(185);
Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssertStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1829,17 +1838,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression e = dummyExpr; Attributes attrs = null;
IToken dotdotdot = null;
- Expect(76);
+ Expect(77);
x = t;
while (IsAttribute()) {
Attribute(ref attrs);
}
if (StartOf(17)) {
Expression(out e, false, true);
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
dotdotdot = t;
- } else SynErr(185);
+ } else SynErr(186);
Expect(8);
if (dotdotdot != null) {
s = new SkeletonStatement(new AssumeStmt(x, t, new LiteralExpr(x, true), attrs), dotdotdot, null);
@@ -1884,14 +1893,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(8);
endTok = t; rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 37 || la.kind == 73 || la.kind == 75) {
+ } else if (la.kind == 37 || la.kind == 74 || la.kind == 76) {
lhss.Add(e); lhs0 = e;
while (la.kind == 37) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 73) {
+ if (la.kind == 74) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1901,21 +1910,21 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 75) {
+ } else if (la.kind == 76) {
Get();
x = t;
- if (la.kind == 76) {
+ if (la.kind == 77) {
Get();
suchThatAssume = t;
}
Expression(out suchThat, false, true);
- } else SynErr(186);
+ } else SynErr(187);
Expect(8);
endTok = t;
} else if (la.kind == 7) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
- } else SynErr(187);
+ } else SynErr(188);
if (suchThat != null) {
s = new AssignSuchThatStmt(x, endTok, lhss, suchThat, suchThatAssume);
} else {
@@ -1958,8 +1967,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d); d.Attributes = attrs; attrs = null;
}
- if (la.kind == 73 || la.kind == 75) {
- if (la.kind == 73) {
+ if (la.kind == 74 || la.kind == 76) {
+ if (la.kind == 74) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1974,7 +1983,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else {
Get();
assignTok = t;
- if (la.kind == 76) {
+ if (la.kind == 77) {
Get();
suchThatAssume = t;
}
@@ -2036,7 +2045,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 13) {
BlockStmt(out bs, out bodyStart, out bodyEnd);
els = bs; endTok = bs.EndTok;
- } else SynErr(188);
+ } else SynErr(189);
}
if (guardEllipsis != null) {
ifStmt = new SkeletonStatement(new IfStmt(x, endTok, guard, thn, els), guardEllipsis, null);
@@ -2044,7 +2053,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ifStmt = new IfStmt(x, endTok, guard, thn, els);
}
- } else SynErr(189);
+ } else SynErr(190);
}
void WhileStmt(out Statement/*!*/ stmt) {
@@ -2078,10 +2087,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 13) {
BlockStmt(out body, out bodyStart, out bodyEnd);
endTok = body.EndTok;
- } else if (la.kind == 43) {
+ } else if (la.kind == 44) {
Get();
bodyEllipsis = t; endTok = t;
- } else SynErr(190);
+ } else SynErr(191);
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
@@ -2097,7 +2106,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
- } else SynErr(191);
+ } else SynErr(192);
}
void MatchStmt(out Statement/*!*/ s) {
@@ -2121,7 +2130,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(14);
} else if (StartOf(22)) {
if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
- } else SynErr(192);
+ } else SynErr(193);
s = new MatchStmt(x, t, e, cases, usesOptionalBrace);
}
@@ -2147,7 +2156,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
errors.Warning(t, "the 'parallel' keyword has been deprecated; the comprehension statement now uses the keyword 'forall' (and the parentheses around the bound variables are now optional)");
- } else SynErr(193);
+ } else SynErr(194);
if (la.kind == 15) {
Get();
usesOptionalParen = true;
@@ -2165,14 +2174,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(16);
} else if (StartOf(23)) {
if (usesOptionalParen) { SemErr(t, "expecting close parenthesis"); }
- } else SynErr(194);
- while (la.kind == 52 || la.kind == 53) {
+ } else SynErr(195);
+ while (la.kind == 53 || la.kind == 54) {
isFree = false;
- if (la.kind == 52) {
+ if (la.kind == 53) {
Get();
isFree = true;
}
- Expect(53);
+ Expect(54);
Expression(out e, false, true);
ens.Add(new MaybeFreeExpression(e, isFree));
Expect(8);
@@ -2281,10 +2290,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 13) {
BlockStmt(out body, out bodyStart, out endTok);
} else if (la.kind == 8) {
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(195); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(196); Get();}
Get();
endTok = t;
- } else SynErr(196);
+ } else SynErr(197);
s = new ModifyStmt(tok, endTok, mod, attrs, body);
if (ellipsisToken != null) {
s = new SkeletonStatement(s, ellipsisToken, null);
@@ -2298,13 +2307,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
AssignmentRhs r;
bool isYield = false;
- if (la.kind == 74) {
+ if (la.kind == 75) {
Get();
returnTok = t;
- } else if (la.kind == 55) {
+ } else if (la.kind == 56) {
Get();
returnTok = t; isYield = true;
- } else SynErr(197);
+ } else SynErr(198);
if (StartOf(26)) {
Rhs(out r, null);
rhss = new List<AssignmentRhs>(); rhss.Add(r);
@@ -2328,9 +2337,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Expression> exprs = null;
IToken tok, dotdotdot, whereTok;
Expression e;
- Expect(43);
+ Expect(44);
dotdotdot = t;
- if (la.kind == 72) {
+ if (la.kind == 73) {
Get();
names = new List<IToken>(); exprs = new List<Expression>(); whereTok = t;
Ident(out tok);
@@ -2340,7 +2349,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out tok);
names.Add(tok);
}
- Expect(73);
+ Expect(74);
Expression(out e, false, true);
exprs.Add(e);
while (la.kind == 37) {
@@ -2367,11 +2376,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = dummyRhs; // to please compiler
Attributes attrs = null;
- if (la.kind == 77) {
+ if (la.kind == 40) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 15 || la.kind == 65 || la.kind == 78) {
+ if (la.kind == 15 || la.kind == 66 || la.kind == 78) {
if (la.kind == 78) {
Get();
ee = new List<Expression>();
@@ -2381,7 +2390,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else {
x = null; args = new List<Expression/*!*/>();
- if (la.kind == 65) {
+ if (la.kind == 66) {
Get();
Ident(out x);
}
@@ -2406,7 +2415,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(17)) {
Expression(out e, false, true);
r = new ExprRhs(e);
- } else SynErr(198);
+ } else SynErr(199);
while (la.kind == 13) {
Attribute(ref attrs);
}
@@ -2418,17 +2427,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e, false, false);
- while (la.kind == 65 || la.kind == 78) {
+ while (la.kind == 66 || la.kind == 78) {
Suffix(ref e);
}
ApplySuffix(ref e);
} else if (StartOf(27)) {
ConstAtomExpression(out e, false, false);
Suffix(ref e);
- while (la.kind == 65 || la.kind == 78) {
+ while (la.kind == 66 || la.kind == 78) {
Suffix(ref e);
}
- } else SynErr(199);
+ } else SynErr(200);
}
void Expressions(List<Expression/*!*/>/*!*/ args) {
@@ -2477,7 +2486,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(17)) {
Expression(out ee, true, true);
e = ee;
- } else SynErr(200);
+ } else SynErr(201);
}
void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod, ref Attributes decAttrs, ref Attributes modAttrs) {
@@ -2488,22 +2497,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod = null;
while (StartOf(28)) {
- if (la.kind == 52 || la.kind == 84) {
+ if (la.kind == 53 || la.kind == 84) {
Invariant(out invariant);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(201); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(202); Get();}
Expect(8);
invariants.Add(invariant);
- } else if (la.kind == 54) {
- while (!(la.kind == 0 || la.kind == 54)) {SynErr(202); Get();}
+ } else if (la.kind == 55) {
+ while (!(la.kind == 0 || la.kind == 55)) {SynErr(203); Get();}
Get();
while (IsAttribute()) {
Attribute(ref decAttrs);
}
DecreasesList(decreases, true);
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(203); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(204); Get();}
Expect(8);
} else {
- while (!(la.kind == 0 || la.kind == 51)) {SynErr(204); Get();}
+ while (!(la.kind == 0 || la.kind == 52)) {SynErr(205); Get();}
Get();
while (IsAttribute()) {
Attribute(ref modAttrs);
@@ -2518,7 +2527,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
mod.Add(fe);
}
}
- while (!(la.kind == 0 || la.kind == 8)) {SynErr(205); Get();}
+ while (!(la.kind == 0 || la.kind == 8)) {SynErr(206); Get();}
Expect(8);
}
}
@@ -2526,8 +2535,8 @@ 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 == 52 || la.kind == 84)) {SynErr(206); Get();}
- if (la.kind == 52) {
+ while (!(la.kind == 0 || la.kind == 53 || la.kind == 84)) {SynErr(207); Get();}
+ if (la.kind == 53) {
Get();
isFree = true;
}
@@ -2575,7 +2584,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (StartOf(17)) {
Expression(out e, allowSemi, true);
arg = new Attributes.Argument(t, e);
- } else SynErr(207);
+ } else SynErr(208);
}
void QuantifierDomain(out List<BoundVar> bvars, out Attributes attrs, out Expression range) {
@@ -2617,12 +2626,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
break;
}
- case 44: {
+ case 45: {
Get();
x = t; binOp = BinaryExpr.Opcode.Lt;
break;
}
- case 45: {
+ case 46: {
Get();
x = t; binOp = BinaryExpr.Opcode.Gt;
break;
@@ -2672,7 +2681,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
- default: SynErr(208); break;
+ default: SynErr(209); break;
}
if (k == null) {
op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
@@ -2709,7 +2718,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 100) {
Get();
- } else SynErr(209);
+ } else SynErr(210);
}
void ImpliesOp() {
@@ -2717,7 +2726,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 102) {
Get();
- } else SynErr(210);
+ } else SynErr(211);
}
void ExpliesOp() {
@@ -2725,7 +2734,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 104) {
Get();
- } else SynErr(211);
+ } else SynErr(212);
}
void EquivExpression(out Expression e0, bool allowSemi, bool allowLambda) {
@@ -2910,7 +2919,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 106) {
Get();
- } else SynErr(212);
+ } else SynErr(213);
}
void OrOp() {
@@ -2918,7 +2927,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 108) {
Get();
- } else SynErr(213);
+ } else SynErr(214);
}
void Term(out Expression e0, bool allowSemi, bool allowLambda) {
@@ -2949,12 +2958,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
break;
}
- case 44: {
+ case 45: {
Get();
x = t; op = BinaryExpr.Opcode.Lt;
break;
}
- case 45: {
+ case 46: {
Get();
x = t; op = BinaryExpr.Opcode.Gt;
break;
@@ -3023,7 +3032,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- default: SynErr(214); break;
+ default: SynErr(215); break;
}
}
@@ -3045,7 +3054,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 112) {
Get();
x = t; op = BinaryExpr.Opcode.Sub;
- } else SynErr(215);
+ } else SynErr(216);
}
void UnaryExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3065,13 +3074,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new UnaryOpExpr(x, UnaryOpExpr.Opcode.Not, e);
break;
}
- case 31: case 36: case 60: case 70: case 76: case 80: case 85: case 86: case 88: case 91: case 124: case 125: case 126: {
+ case 31: case 36: case 61: case 71: case 77: case 80: case 85: case 86: case 88: case 91: case 124: case 125: case 126: {
EndlessExpression(out e, allowSemi, allowLambda);
break;
}
case 1: {
DottedIdentifiersAndFunction(out e, allowSemi, allowLambda);
- while (la.kind == 65 || la.kind == 78) {
+ while (la.kind == 66 || la.kind == 78) {
Suffix(ref e);
}
ApplySuffix(ref e);
@@ -3079,41 +3088,41 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
case 13: case 78: {
DisplayExpr(out e);
- while (la.kind == 65 || la.kind == 78) {
+ while (la.kind == 66 || la.kind == 78) {
Suffix(ref e);
}
break;
}
- case 61: {
+ case 62: {
MultiSetExpr(out e);
- while (la.kind == 65 || la.kind == 78) {
+ while (la.kind == 66 || la.kind == 78) {
Suffix(ref e);
}
break;
}
- case 63: {
+ case 64: {
Get();
x = t;
if (la.kind == 78) {
MapDisplayExpr(x, out e);
- while (la.kind == 65 || la.kind == 78) {
+ while (la.kind == 66 || la.kind == 78) {
Suffix(ref e);
}
} else if (la.kind == 1) {
MapComprehensionExpr(x, out e, allowSemi);
} else if (StartOf(32)) {
SemErr("map must be followed by literal in brackets or comprehension.");
- } else SynErr(216);
+ } else SynErr(217);
break;
}
- case 2: case 3: case 4: case 15: case 35: case 58: case 59: case 116: case 117: case 118: case 119: case 120: case 121: {
+ case 2: case 3: case 4: case 15: case 35: case 59: case 60: case 116: case 117: case 118: case 119: case 120: case 121: {
ConstAtomExpression(out e, allowSemi, allowLambda);
- while (la.kind == 65 || la.kind == 78) {
+ while (la.kind == 66 || la.kind == 78) {
Suffix(ref e);
}
break;
}
- default: SynErr(217); break;
+ default: SynErr(218); break;
}
}
@@ -3128,7 +3137,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 114) {
Get();
x = t; op = BinaryExpr.Opcode.Mod;
- } else SynErr(218);
+ } else SynErr(219);
}
void NegOp() {
@@ -3136,7 +3145,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 115) {
Get();
- } else SynErr(219);
+ } else SynErr(220);
}
void EndlessExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3165,11 +3174,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
QuantifierGuts(out e, allowSemi, allowLambda);
break;
}
- case 60: {
+ case 61: {
ComprehensionExpr(out e, allowSemi, allowLambda);
break;
}
- case 76: case 86: case 91: {
+ case 77: case 86: case 91: {
StmtInExpr(out s);
Expression(out e, allowSemi, allowLambda);
e = new StmtExpr(s.Tok, s, e);
@@ -3179,11 +3188,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LetExpr(out e, allowSemi, allowLambda);
break;
}
- case 70: {
+ case 71: {
NamedExpr(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(220); break;
+ default: SynErr(221); break;
}
}
@@ -3196,7 +3205,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
idents.Add(id);
- while (la.kind == 65) {
+ while (la.kind == 66) {
IdentOrDigitsSuffix(out id, out idPrime);
idents.Add(id);
if (idPrime != null) { idents.Add(idPrime); id = idPrime; }
@@ -3253,7 +3262,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 65) {
+ if (la.kind == 66) {
IdentOrDigitsSuffix(out id, out x);
if (x != null) {
// process id as a Suffix in its own right
@@ -3293,7 +3302,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out ee, true, true);
e1 = ee;
}
- } else if (la.kind == 73) {
+ } else if (la.kind == 74) {
Get();
Expression(out ee, true, true);
e1 = ee;
@@ -3324,7 +3333,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
multipleIndices.Add(ee);
}
- } else SynErr(221);
+ } else SynErr(222);
} else if (la.kind == 123) {
Get();
anyDots = true;
@@ -3332,7 +3341,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out ee, true, true);
e1 = ee;
}
- } else SynErr(222);
+ } else SynErr(223);
if (multipleIndices != null) {
e = new MultiSelectExpr(x, e, multipleIndices);
// make sure an array class with this dimensionality exists
@@ -3373,7 +3382,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(79);
- } else SynErr(223);
+ } else SynErr(224);
ApplySuffix(ref e);
}
@@ -3410,7 +3419,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SeqDisplayExpr(x, elements);
Expect(79);
- } else SynErr(224);
+ } else SynErr(225);
}
void MultiSetExpr(out Expression e) {
@@ -3418,7 +3427,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IToken/*!*/ x = null; List<Expression/*!*/>/*!*/ elements;
e = dummyExpr;
- Expect(61);
+ Expect(62);
x = t;
if (la.kind == 13) {
Get();
@@ -3436,7 +3445,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(16);
} else if (StartOf(32)) {
SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses.");
- } else SynErr(225);
+ } else SynErr(226);
}
void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {
@@ -3533,8 +3542,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(35);
break;
}
- case 58: case 59: {
- if (la.kind == 58) {
+ case 59: case 60: {
+ if (la.kind == 59) {
Get();
x = t; toType = new IntType();
} else {
@@ -3551,7 +3560,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ParensExpression(out e, allowSemi, allowLambda);
break;
}
- default: SynErr(226); break;
+ default: SynErr(227); break;
}
}
@@ -3576,7 +3585,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
n = BigInteger.Zero;
}
- } else SynErr(227);
+ } else SynErr(228);
}
void Dec(out Basetypes.BigDec d) {
@@ -3684,7 +3693,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 10) {
Get();
oneShot = true;
- } else SynErr(228);
+ } else SynErr(229);
}
void OptTypedExpr(out Expression e, out Type tt, bool allowSemi) {
@@ -3700,13 +3709,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d, true, true);
- Expect(73);
+ Expect(74);
Expression(out r, true, true);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 37) {
Get();
Expression(out d, true, true);
- Expect(73);
+ Expect(74);
Expression(out r, true, true);
elements.Add(new ExpressionPair(d,r));
}
@@ -3717,7 +3726,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 128) {
Get();
- } else SynErr(229);
+ } else SynErr(230);
}
void MatchExpression(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3740,7 +3749,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(14);
} else if (StartOf(32)) {
if (usesOptionalBrace) { SemErr(t, "expecting close curly brace"); }
- } else SynErr(230);
+ } else SynErr(231);
e = new MatchExpr(x, e, cases, usesOptionalBrace);
}
@@ -3758,7 +3767,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 125 || la.kind == 126) {
Exists();
x = t;
- } else SynErr(231);
+ } else SynErr(232);
QuantifierDomain(out bvars, out attrs, out range);
QSep();
Expression(out body, allowSemi, allowLambda);
@@ -3778,7 +3787,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression range;
Expression body = null;
- Expect(60);
+ Expect(61);
x = t;
IdentTypeOptional(out bv);
bvars.Add(bv);
@@ -3802,11 +3811,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s = dummyStmt;
if (la.kind == 86) {
AssertStmt(out s);
- } else if (la.kind == 76) {
+ } else if (la.kind == 77) {
AssumeStmt(out s);
} else if (la.kind == 91) {
CalcStmt(out s);
- } else SynErr(232);
+ } else SynErr(233);
}
void LetExpr(out Expression e, bool allowSemi, bool allowLambda) {
@@ -3835,9 +3844,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
letLHSs.Add(pat);
}
- if (la.kind == 73) {
+ if (la.kind == 74) {
Get();
- } else if (la.kind == 75) {
+ } else if (la.kind == 76) {
Get();
exact = false;
foreach (var lhs in letLHSs) {
@@ -3846,7 +3855,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- } else SynErr(233);
+ } else SynErr(234);
Expression(out e, false, true);
letRHSs.Add(e);
while (la.kind == 37) {
@@ -3864,7 +3873,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = dummyExpr;
Expression expr;
- Expect(70);
+ Expect(71);
x = t;
NoUSIdent(out d);
Expect(7);
@@ -3897,7 +3906,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out bv);
pat = new CasePattern(bv.tok, bv);
- } else SynErr(234);
+ } else SynErr(235);
}
void CaseExpression(out MatchCaseExpr c, bool allowSemi, bool allowLambda) {
@@ -3930,7 +3939,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 124) {
Get();
- } else SynErr(235);
+ } else SynErr(236);
}
void Exists() {
@@ -3938,7 +3947,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
} else if (la.kind == 126) {
Get();
- } else SynErr(236);
+ } else SynErr(237);
}
void AttributeBody(ref Attributes attrs) {
@@ -3974,40 +3983,40 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,T, T,x,x,x, T,x,x,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,T,T,T, T,x,x,x, T,x,x,T, x,x,T,T, T,T,T,T, T,T,T,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,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, 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, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,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,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,T, T,x,x,x, T,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,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},
- {T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,x,x,x, T,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, x,x,x},
- {T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, T,x,x,x, T,x,T,T, T,T,T,x, x,T,T,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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},
- {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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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, 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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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,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,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, 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,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,T, 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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
- {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,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,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
- {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
- {T,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,x,x,T, 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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
- {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
- {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
- {x,T,T,T, T,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,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,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,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
- {x,T,T,T, T,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,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,T,x,T, x,x,T,T, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, T,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,x, x,x,x,x, x,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,x,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,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,T,T,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,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
- {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
- {x,x,T,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, 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,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, 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,T, T,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},
+ {T,T,T,T, T,x,x,x, T,x,x,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,T, x,T,T,T, T,x,x,x, x,T,x,x, T,x,x,T, T,T,T,T, T,T,T,T, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,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, 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, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, x,T,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,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,x,x,x, T,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,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},
+ {T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, T,T,x,T, x,T,x,x, T,x,T,T, T,T,T,x, T,x,T,x, x,T,x,x, x,T,x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, 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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,x,x},
+ {T,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, T,T,x,T, x,x,x,x, T,x,T,T, T,T,T,x, T,x,T,x, x,T,x,x, x,T,x,T, T,T,T,T, x,x,T,T, 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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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,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},
+ {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,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,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, 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,T,T,x, x,T,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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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, 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,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T, T,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, 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,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,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,x,x,T, 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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
+ {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, 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,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T, T,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {T,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,x,x,T, 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, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,T,T,T, T,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,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,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,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x},
+ {x,T,T,T, T,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,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,T,x, T,x,x,T, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,T,x,x, T,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,x, x,x,x,x, x,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,x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,T,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,T,T,T, T,x,x,x, x,x,x,x, x,T,x,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x},
+ {x,x,T,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, 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,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, 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, T,T,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, 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,x, x,x,x,x, x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,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,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,T,T,T, T,T,T,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,T,T,T, T,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,T,x,T, x,x,x,T, T,T,x,x, x,x,x,T, T,T,T,T, x,x,T,T, x,x,x,x, x,T,x,x, x,T,T,T, x,T,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,T, x,x,x,T, T,x,x},
- {x,T,T,T, T,x,T,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T,T, T,T,x,T, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,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,T,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,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,T,T,T, T,x,x,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, T,T,x,T, x,x,x,x, T,T,T,x, x,x,x,x, T,T,T,T, T,x,x,T, T,x,x,x, x,x,T,x, x,x,T,T, T,x,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,T,T, x,x,x,T, T,x,x},
+ {x,T,T,T, T,x,T,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, 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,T, T,T,T,x, T,x,x,x, x,x,x,T, x,x,x,x, x,T,T,x, T,x,x,x, x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,T, T,T,x,x, T,T,T,x, x,x,x}
};
} // end Parser
@@ -4072,44 +4081,44 @@ public class Errors {
case 37: s = "\",\" expected"; break;
case 38: s = "\"type\" expected"; break;
case 39: s = "\"==\" expected"; break;
- case 40: s = "\"iterator\" expected"; break;
- case 41: s = "\"yields\" expected"; break;
- case 42: s = "\"returns\" expected"; break;
- case 43: s = "\"...\" expected"; break;
- case 44: s = "\"<\" expected"; break;
- case 45: s = "\">\" expected"; break;
- case 46: s = "\"method\" expected"; break;
- case 47: s = "\"lemma\" expected"; break;
- case 48: s = "\"colemma\" expected"; break;
- case 49: s = "\"comethod\" expected"; break;
- case 50: s = "\"constructor\" expected"; break;
- case 51: s = "\"modifies\" expected"; break;
- case 52: s = "\"free\" expected"; break;
- case 53: s = "\"ensures\" expected"; break;
- case 54: s = "\"decreases\" expected"; break;
- case 55: s = "\"yield\" expected"; break;
- case 56: s = "\"bool\" expected"; break;
- case 57: s = "\"nat\" expected"; break;
- case 58: s = "\"int\" expected"; break;
- case 59: s = "\"real\" expected"; break;
- case 60: s = "\"set\" expected"; break;
- case 61: s = "\"multiset\" expected"; break;
- case 62: s = "\"seq\" expected"; break;
- case 63: s = "\"map\" expected"; break;
- case 64: s = "\"object\" expected"; break;
- case 65: s = "\".\" expected"; break;
- case 66: s = "\"function\" expected"; break;
- case 67: s = "\"predicate\" expected"; break;
- case 68: s = "\"copredicate\" expected"; break;
- case 69: s = "\"`\" expected"; break;
- case 70: s = "\"label\" expected"; break;
- case 71: s = "\"break\" expected"; break;
- case 72: s = "\"where\" expected"; break;
- case 73: s = "\":=\" expected"; break;
- case 74: s = "\"return\" expected"; break;
- case 75: s = "\":|\" expected"; break;
- case 76: s = "\"assume\" expected"; break;
- case 77: s = "\"new\" expected"; break;
+ case 40: s = "\"new\" expected"; break;
+ case 41: s = "\"iterator\" expected"; break;
+ case 42: s = "\"yields\" expected"; break;
+ case 43: s = "\"returns\" expected"; break;
+ case 44: s = "\"...\" expected"; break;
+ case 45: s = "\"<\" expected"; break;
+ case 46: s = "\">\" expected"; break;
+ case 47: s = "\"method\" expected"; break;
+ case 48: s = "\"lemma\" expected"; break;
+ case 49: s = "\"colemma\" expected"; break;
+ case 50: s = "\"comethod\" expected"; break;
+ case 51: s = "\"constructor\" expected"; break;
+ case 52: s = "\"modifies\" expected"; break;
+ case 53: s = "\"free\" expected"; break;
+ case 54: s = "\"ensures\" expected"; break;
+ case 55: s = "\"decreases\" expected"; break;
+ case 56: s = "\"yield\" expected"; break;
+ case 57: s = "\"bool\" expected"; break;
+ case 58: s = "\"nat\" expected"; break;
+ case 59: s = "\"int\" expected"; break;
+ case 60: s = "\"real\" expected"; break;
+ case 61: s = "\"set\" expected"; break;
+ case 62: s = "\"multiset\" expected"; break;
+ case 63: s = "\"seq\" expected"; break;
+ case 64: s = "\"map\" expected"; break;
+ case 65: s = "\"object\" expected"; break;
+ case 66: s = "\".\" expected"; break;
+ case 67: s = "\"function\" expected"; break;
+ case 68: s = "\"predicate\" expected"; break;
+ case 69: s = "\"copredicate\" expected"; break;
+ case 70: s = "\"`\" expected"; break;
+ case 71: s = "\"label\" expected"; break;
+ case 72: s = "\"break\" expected"; break;
+ case 73: s = "\"where\" expected"; break;
+ case 74: s = "\":=\" expected"; break;
+ case 75: s = "\"return\" expected"; break;
+ case 76: s = "\":|\" expected"; break;
+ case 77: s = "\"assume\" expected"; break;
case 78: s = "\"[\" expected"; break;
case 79: s = "\"]\" expected"; break;
case 80: s = "\"if\" expected"; break;
@@ -4169,106 +4178,107 @@ public class Errors {
case 134: s = "invalid DatatypeDecl"; break;
case 135: s = "this symbol not expected in DatatypeDecl"; break;
case 136: s = "invalid OtherTypeDecl"; break;
- case 137: s = "this symbol not expected in OtherTypeDecl"; break;
- case 138: s = "this symbol not expected in IteratorDecl"; break;
- case 139: s = "invalid IteratorDecl"; break;
- case 140: s = "this symbol not expected in TraitDecl"; break;
- case 141: s = "invalid ClassMemberDecl"; break;
- case 142: s = "invalid IdentOrDigitsSuffix"; break;
- case 143: s = "this symbol not expected in FieldDecl"; break;
+ case 137: s = "invalid OtherTypeDecl"; break;
+ case 138: s = "this symbol not expected in OtherTypeDecl"; break;
+ case 139: s = "this symbol not expected in IteratorDecl"; break;
+ case 140: s = "invalid IteratorDecl"; break;
+ case 141: s = "this symbol not expected in TraitDecl"; break;
+ case 142: s = "invalid ClassMemberDecl"; break;
+ case 143: s = "invalid IdentOrDigitsSuffix"; break;
case 144: s = "this symbol not expected in FieldDecl"; break;
- case 145: s = "invalid FunctionDecl"; break;
+ case 145: s = "this symbol not expected in FieldDecl"; break;
case 146: s = "invalid FunctionDecl"; break;
case 147: s = "invalid FunctionDecl"; break;
case 148: s = "invalid FunctionDecl"; break;
- case 149: s = "this symbol not expected in MethodDecl"; break;
- case 150: s = "invalid MethodDecl"; break;
+ case 149: s = "invalid FunctionDecl"; break;
+ case 150: s = "this symbol not expected in MethodDecl"; break;
case 151: s = "invalid MethodDecl"; break;
- case 152: s = "invalid FIdentType"; break;
- case 153: s = "invalid TypeIdentOptional"; break;
- case 154: s = "invalid TypeAndToken"; break;
- case 155: s = "this symbol not expected in IteratorSpec"; break;
+ case 152: s = "invalid MethodDecl"; break;
+ case 153: s = "invalid FIdentType"; break;
+ case 154: s = "invalid TypeIdentOptional"; break;
+ case 155: s = "invalid TypeAndToken"; break;
case 156: s = "this symbol not expected in IteratorSpec"; break;
case 157: s = "this symbol not expected in IteratorSpec"; break;
case 158: s = "this symbol not expected in IteratorSpec"; break;
case 159: s = "this symbol not expected in IteratorSpec"; break;
- case 160: s = "invalid IteratorSpec"; break;
- case 161: s = "this symbol not expected in IteratorSpec"; break;
- case 162: s = "invalid IteratorSpec"; break;
- case 163: s = "this symbol not expected in MethodSpec"; break;
+ case 160: s = "this symbol not expected in IteratorSpec"; break;
+ case 161: s = "invalid IteratorSpec"; break;
+ case 162: s = "this symbol not expected in IteratorSpec"; break;
+ case 163: s = "invalid IteratorSpec"; break;
case 164: s = "this symbol not expected in MethodSpec"; break;
case 165: s = "this symbol not expected in MethodSpec"; break;
case 166: s = "this symbol not expected in MethodSpec"; break;
- case 167: s = "invalid MethodSpec"; break;
- case 168: s = "this symbol not expected in MethodSpec"; break;
- case 169: s = "invalid MethodSpec"; break;
- case 170: s = "invalid FrameExpression"; break;
- case 171: s = "invalid ReferenceType"; break;
- case 172: s = "this symbol not expected in FunctionSpec"; break;
+ case 167: s = "this symbol not expected in MethodSpec"; break;
+ case 168: s = "invalid MethodSpec"; break;
+ case 169: s = "this symbol not expected in MethodSpec"; break;
+ case 170: s = "invalid MethodSpec"; break;
+ case 171: s = "invalid FrameExpression"; break;
+ case 172: s = "invalid ReferenceType"; break;
case 173: s = "this symbol not expected in FunctionSpec"; break;
case 174: s = "this symbol not expected in FunctionSpec"; break;
case 175: s = "this symbol not expected in FunctionSpec"; break;
case 176: s = "this symbol not expected in FunctionSpec"; break;
- case 177: s = "invalid FunctionSpec"; break;
- case 178: s = "invalid PossiblyWildFrameExpression"; break;
- case 179: s = "invalid PossiblyWildExpression"; break;
- case 180: s = "this symbol not expected in OneStmt"; break;
- case 181: s = "invalid OneStmt"; break;
- case 182: s = "this symbol not expected in OneStmt"; break;
- case 183: s = "invalid OneStmt"; break;
- case 184: s = "invalid AssertStmt"; break;
- case 185: s = "invalid AssumeStmt"; break;
- case 186: s = "invalid UpdateStmt"; break;
+ case 177: s = "this symbol not expected in FunctionSpec"; break;
+ case 178: s = "invalid FunctionSpec"; break;
+ case 179: s = "invalid PossiblyWildFrameExpression"; break;
+ case 180: s = "invalid PossiblyWildExpression"; break;
+ case 181: s = "this symbol not expected in OneStmt"; break;
+ case 182: s = "invalid OneStmt"; break;
+ case 183: s = "this symbol not expected in OneStmt"; break;
+ case 184: s = "invalid OneStmt"; break;
+ case 185: s = "invalid AssertStmt"; break;
+ case 186: s = "invalid AssumeStmt"; break;
case 187: s = "invalid UpdateStmt"; break;
- case 188: s = "invalid IfStmt"; break;
+ case 188: s = "invalid UpdateStmt"; break;
case 189: s = "invalid IfStmt"; break;
- case 190: s = "invalid WhileStmt"; break;
+ case 190: s = "invalid IfStmt"; break;
case 191: s = "invalid WhileStmt"; break;
- case 192: s = "invalid MatchStmt"; break;
- case 193: s = "invalid ForallStmt"; break;
+ case 192: s = "invalid WhileStmt"; break;
+ case 193: s = "invalid MatchStmt"; break;
case 194: s = "invalid ForallStmt"; break;
- case 195: s = "this symbol not expected in ModifyStmt"; break;
- case 196: s = "invalid ModifyStmt"; break;
- case 197: s = "invalid ReturnStmt"; break;
- case 198: s = "invalid Rhs"; break;
- case 199: s = "invalid Lhs"; break;
- case 200: s = "invalid Guard"; break;
- case 201: s = "this symbol not expected in LoopSpec"; break;
+ case 195: s = "invalid ForallStmt"; break;
+ case 196: s = "this symbol not expected in ModifyStmt"; break;
+ case 197: s = "invalid ModifyStmt"; break;
+ case 198: s = "invalid ReturnStmt"; break;
+ case 199: s = "invalid Rhs"; break;
+ case 200: s = "invalid Lhs"; break;
+ case 201: s = "invalid Guard"; break;
case 202: s = "this symbol not expected in LoopSpec"; break;
case 203: s = "this symbol not expected in LoopSpec"; break;
case 204: s = "this symbol not expected in LoopSpec"; break;
case 205: s = "this symbol not expected in LoopSpec"; break;
- case 206: s = "this symbol not expected in Invariant"; break;
- case 207: s = "invalid AttributeArg"; break;
- case 208: s = "invalid CalcOp"; break;
- case 209: s = "invalid EquivOp"; break;
- case 210: s = "invalid ImpliesOp"; break;
- case 211: s = "invalid ExpliesOp"; break;
- case 212: s = "invalid AndOp"; break;
- case 213: s = "invalid OrOp"; break;
- case 214: s = "invalid RelOp"; break;
- case 215: s = "invalid AddOp"; break;
- case 216: s = "invalid UnaryExpression"; break;
+ case 206: s = "this symbol not expected in LoopSpec"; break;
+ case 207: s = "this symbol not expected in Invariant"; break;
+ case 208: s = "invalid AttributeArg"; break;
+ case 209: s = "invalid CalcOp"; break;
+ case 210: s = "invalid EquivOp"; break;
+ case 211: s = "invalid ImpliesOp"; break;
+ case 212: s = "invalid ExpliesOp"; break;
+ case 213: s = "invalid AndOp"; break;
+ case 214: s = "invalid OrOp"; break;
+ case 215: s = "invalid RelOp"; break;
+ case 216: s = "invalid AddOp"; break;
case 217: s = "invalid UnaryExpression"; break;
- case 218: s = "invalid MulOp"; break;
- case 219: s = "invalid NegOp"; break;
- case 220: s = "invalid EndlessExpression"; break;
- case 221: s = "invalid Suffix"; break;
+ case 218: s = "invalid UnaryExpression"; break;
+ case 219: s = "invalid MulOp"; break;
+ case 220: s = "invalid NegOp"; break;
+ case 221: s = "invalid EndlessExpression"; break;
case 222: s = "invalid Suffix"; break;
case 223: s = "invalid Suffix"; break;
- case 224: s = "invalid DisplayExpr"; break;
- case 225: s = "invalid MultiSetExpr"; break;
- case 226: s = "invalid ConstAtomExpression"; break;
- case 227: s = "invalid Nat"; break;
- case 228: s = "invalid LambdaArrow"; break;
- case 229: s = "invalid QSep"; break;
- case 230: s = "invalid MatchExpression"; break;
- case 231: s = "invalid QuantifierGuts"; break;
- case 232: s = "invalid StmtInExpr"; break;
- case 233: s = "invalid LetExpr"; break;
- case 234: s = "invalid CasePattern"; break;
- case 235: s = "invalid Forall"; break;
- case 236: s = "invalid Exists"; break;
+ case 224: s = "invalid Suffix"; break;
+ case 225: s = "invalid DisplayExpr"; break;
+ case 226: s = "invalid MultiSetExpr"; break;
+ case 227: s = "invalid ConstAtomExpression"; break;
+ case 228: s = "invalid Nat"; break;
+ case 229: s = "invalid LambdaArrow"; break;
+ case 230: s = "invalid QSep"; break;
+ case 231: s = "invalid MatchExpression"; break;
+ case 232: s = "invalid QuantifierGuts"; break;
+ case 233: s = "invalid StmtInExpr"; break;
+ case 234: s = "invalid LetExpr"; break;
+ case 235: s = "invalid CasePattern"; break;
+ case 236: s = "invalid Forall"; break;
+ case 237: s = "invalid Exists"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index bfbc9644..459cbcef 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -140,6 +140,14 @@ namespace Microsoft.Dafny {
PrintClassMethodHelper("type", at.Attributes, at.Name, new List<TypeParameter>());
wr.Write(EqualitySupportSuffix(at.EqualitySupport));
wr.WriteLine();
+ } else if (d is DerivedTypeDecl) {
+ var dd = (DerivedTypeDecl)d;
+ if (i++ != 0) { wr.WriteLine(); }
+ Indent(indent);
+ PrintClassMethodHelper("type", dd.Attributes, dd.Name, new List<TypeParameter>());
+ wr.Write(" = new ");
+ PrintType(dd.BaseType);
+ wr.WriteLine();
} else if (d is TypeSynonymDecl) {
var syn = (TypeSynonymDecl)d;
if (i++ != 0) { wr.WriteLine(); }
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index a7989cba..88d3fd24 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -159,10 +159,15 @@ namespace Microsoft.Dafny
}
} else if (dDemandsEqualitySupport) {
if (nw is ClassDecl) {
- // fine, as long as "nw" does not take any type parameters
+ // fine, as long as "nw" takes the right number of type parameters
if (nw.TypeArgs.Count != d.TypeArgs.Count) {
reporter.Error(nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count);
}
+ } else if (nw is DerivedTypeDecl) {
+ // fine, as long as "nw" does not take any type parameters
+ if (nw.TypeArgs.Count != 0) {
+ reporter.Error(nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a derived type, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s");
+ }
} else if (nw is CoDatatypeDecl) {
reporter.Error(nw, "a type declaration that requires equality support cannot be replaced by a codatatype");
} else {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 172f63ad..52bc87ac 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -788,6 +788,8 @@ namespace Microsoft.Dafny
// nothing more to register
} else if (d is TypeSynonymDecl) {
// nothing more to register
+ } else if (d is DerivedTypeDecl) {
+ // nothing more to register
} else if (d is IteratorDecl) {
var iter = (IteratorDecl)d;
@@ -1447,7 +1449,7 @@ namespace Microsoft.Dafny
Contract.Requires(datatypeDependencies != null);
Contract.Requires(codatatypeDependencies != null);
- var typeSynonymDependencies = new Graph<TypeSynonymDecl>();
+ var typeRedirectionDependencies = new Graph<RedirectingTypeDecl>();
foreach (TopLevelDecl d in declarations) {
Contract.Assert(d != null);
allTypeParameters.PushMarker();
@@ -1458,9 +1460,18 @@ namespace Microsoft.Dafny
var syn = (TypeSynonymDecl)d;
ResolveType(syn.tok, syn.Rhs, ResolveTypeOptionEnum.AllowPrefix, syn.TypeArgs);
syn.Rhs.ForeachTypeComponent(ty => {
- var s = ty.AsTypeSynonym;
+ var s = ty.AsRedirectingType;
if (s != null) {
- typeSynonymDependencies.AddEdge(syn, s);
+ typeRedirectionDependencies.AddEdge(syn, s);
+ }
+ });
+ } else if (d is DerivedTypeDecl) {
+ var dd = (DerivedTypeDecl)d;
+ ResolveType(dd.tok, dd.BaseType, ResolveTypeOptionEnum.DontInfer, null);
+ dd.BaseType.ForeachTypeComponent(ty => {
+ var s = ty.AsRedirectingType;
+ if (s != null) {
+ typeRedirectionDependencies.AddEdge(dd, s);
}
});
} else if (d is IteratorDecl) {
@@ -1496,11 +1507,11 @@ namespace Microsoft.Dafny
}
// perform acyclicity test on type synonyms
- var cycle = typeSynonymDependencies.TryFindCycle();
+ var cycle = typeRedirectionDependencies.TryFindCycle();
if (cycle != null) {
Contract.Assert(cycle.Count != 0);
var erste = cycle[0];
- Error(erste.tok, "Cycle among type synonyms: {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name);
+ Error(erste.Tok, "Cycle among redirecting types (derived types, type synonyms): {0} -> {1}", Util.Comma(" -> ", cycle, syn => syn.Name), erste.Name);
}
}
@@ -1531,6 +1542,12 @@ namespace Microsoft.Dafny
} else if (d is ClassDecl) {
var cl = (ClassDecl)d;
ResolveClassMemberBodies(cl);
+ } else if (d is DerivedTypeDecl) {
+ var dd = (DerivedTypeDecl)d;
+ // this check can be done only after it has been determined that the redirected types do not involve cycles
+ if (!dd.BaseType.IsNumericBased) {
+ Error(dd.tok, "derived types must be based on some numeric type (got {0})", dd.BaseType);
+ }
}
allTypeParameters.PopMarker();
}
@@ -4265,8 +4282,8 @@ namespace Microsoft.Dafny
}
} else if (proxy is OperationTypeProxy) {
- OperationTypeProxy opProxy = (OperationTypeProxy)proxy;
- if (t is IntType || t is RealType || t is SetType || t is MultiSetType || (opProxy.AllowSeq && t is SeqType)) {
+ var opProxy = (OperationTypeProxy)proxy;
+ if (t.IsNumericBased || (opProxy.AllowSetVarieties && (t is SetType || t is MultiSetType)) || (opProxy.AllowSeq && t is SeqType)) {
// this is the expected case
} else {
return false;
@@ -4361,10 +4378,11 @@ namespace Microsoft.Dafny
a.T = b;
return UnifyTypes(((CollectionTypeProxy)a).Arg, ((CollectionTypeProxy)b).Arg);
} else if (b is OperationTypeProxy) {
- if (((OperationTypeProxy)b).AllowSeq) {
+ var proxy = (OperationTypeProxy)b;
+ if (proxy.AllowSeq && proxy.AllowSetVarieties) {
b.T = a; // a is a stronger constraint than b
} else {
- // a says set<T>,seq<T> and b says int,set; the intersection is set<T>
+ // a says set<T>,seq<T> and b says numeric,set; the intersection is set<T>
a.T = new SetType(((CollectionTypeProxy)a).Arg);
b.T = a.T;
}
@@ -6692,8 +6710,8 @@ namespace Microsoft.Dafny
expr.Type = Type.Bool;
} else {
bool err = false;
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true))) {
- Error(expr, "arguments to {0} must be int or real or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(true, true))) {
+ Error(expr, "arguments to {0} must be of a numeric type or a collection type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
err = true;
}
if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
@@ -6729,8 +6747,8 @@ namespace Microsoft.Dafny
expr.Type = Type.Bool;
} else {
bool err = false;
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {
- Error(expr, "arguments to {0} must be int or real or a set (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false, true))) {
+ Error(expr, "arguments to {0} must be of a numeric type or set type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
err = true;
}
if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
@@ -6755,9 +6773,8 @@ namespace Microsoft.Dafny
break;
case BinaryExpr.Opcode.Div:
- if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false))) {
- // TODO: this should disallow OperationTypeProxy types except for int and real
- Error(expr, "first argument to {0} must be of type int or real (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
+ if (!UnifyTypes(e.E0.Type, new OperationTypeProxy(false, false))) {
+ Error(expr, "first argument to {0} must be of numeric type (instead got {1})", BinaryExpr.OpcodeString(e.Op), e.E0.Type);
}
if (!UnifyTypes(e.E1.Type, e.E0.Type)) {
Error(expr, "arguments to {0} must have the same type (got {1} and {2})", BinaryExpr.OpcodeString(e.Op), e.E0.Type, e.E1.Type);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 30e4071c..a54fe778 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -510,37 +510,37 @@ public class Scanner {
case "codatatype": t.kind = 34; break;
case "var": t.kind = 36; break;
case "type": t.kind = 38; break;
- case "iterator": t.kind = 40; break;
- case "yields": t.kind = 41; break;
- case "returns": t.kind = 42; break;
- case "method": t.kind = 46; break;
- case "lemma": t.kind = 47; break;
- case "colemma": t.kind = 48; break;
- case "comethod": t.kind = 49; break;
- case "constructor": t.kind = 50; break;
- case "modifies": t.kind = 51; break;
- case "free": t.kind = 52; break;
- case "ensures": t.kind = 53; break;
- case "decreases": t.kind = 54; break;
- case "yield": t.kind = 55; break;
- case "bool": t.kind = 56; break;
- case "nat": t.kind = 57; break;
- case "int": t.kind = 58; break;
- case "real": t.kind = 59; break;
- case "set": t.kind = 60; break;
- case "multiset": t.kind = 61; break;
- case "seq": t.kind = 62; break;
- case "map": t.kind = 63; break;
- case "object": t.kind = 64; break;
- case "function": t.kind = 66; break;
- case "predicate": t.kind = 67; break;
- case "copredicate": t.kind = 68; break;
- case "label": t.kind = 70; break;
- case "break": t.kind = 71; break;
- case "where": t.kind = 72; break;
- case "return": t.kind = 74; break;
- case "assume": t.kind = 76; break;
- case "new": t.kind = 77; break;
+ case "new": t.kind = 40; break;
+ case "iterator": t.kind = 41; break;
+ case "yields": t.kind = 42; break;
+ case "returns": t.kind = 43; break;
+ case "method": t.kind = 47; break;
+ case "lemma": t.kind = 48; break;
+ case "colemma": t.kind = 49; break;
+ case "comethod": t.kind = 50; break;
+ case "constructor": t.kind = 51; break;
+ case "modifies": t.kind = 52; break;
+ case "free": t.kind = 53; break;
+ case "ensures": t.kind = 54; break;
+ case "decreases": t.kind = 55; break;
+ case "yield": t.kind = 56; break;
+ case "bool": t.kind = 57; break;
+ case "nat": t.kind = 58; break;
+ case "int": t.kind = 59; break;
+ case "real": t.kind = 60; break;
+ case "set": t.kind = 61; break;
+ case "multiset": t.kind = 62; break;
+ case "seq": t.kind = 63; break;
+ case "map": t.kind = 64; break;
+ case "object": t.kind = 65; break;
+ case "function": t.kind = 67; break;
+ case "predicate": t.kind = 68; break;
+ case "copredicate": t.kind = 69; break;
+ case "label": t.kind = 71; break;
+ case "break": t.kind = 72; break;
+ case "where": t.kind = 73; break;
+ case "return": t.kind = 75; break;
+ case "assume": t.kind = 77; break;
case "if": t.kind = 80; break;
case "else": t.kind = 81; break;
case "case": t.kind = 82; break;
@@ -714,13 +714,13 @@ public class Scanner {
case 33:
{t.kind = 37; break;}
case 34:
- {t.kind = 43; break;}
+ {t.kind = 44; break;}
case 35:
- {t.kind = 69; break;}
+ {t.kind = 70; break;}
case 36:
- {t.kind = 73; break;}
+ {t.kind = 74; break;}
case 37:
- {t.kind = 75; break;}
+ {t.kind = 76; break;}
case 38:
{t.kind = 78; break;}
case 39:
@@ -799,17 +799,17 @@ public class Scanner {
if (ch == '|') {AddCh(); goto case 54;}
else {t.kind = 35; break;}
case 69:
- recEnd = pos; recKind = 65;
+ recEnd = pos; recKind = 66;
if (ch == '.') {AddCh(); goto case 73;}
- else {t.kind = 65; break;}
+ else {t.kind = 66; break;}
case 70:
- recEnd = pos; recKind = 44;
+ recEnd = pos; recKind = 45;
if (ch == '=') {AddCh(); goto case 74;}
- else {t.kind = 44; break;}
+ else {t.kind = 45; break;}
case 71:
- recEnd = pos; recKind = 45;
+ recEnd = pos; recKind = 46;
if (ch == '=') {AddCh(); goto case 41;}
- else {t.kind = 45; break;}
+ else {t.kind = 46; break;}
case 72:
recEnd = pos; recKind = 39;
if (ch == '>') {AddCh(); goto case 48;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 3688ed3f..de160637 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -368,6 +368,8 @@ namespace Microsoft.Dafny {
currentDeclaration = d;
if (d is OpaqueTypeDecl) {
AddTypeDecl((OpaqueTypeDecl)d);
+ } else if (d is DerivedTypeDecl) {
+ AddTypeDecl((DerivedTypeDecl)d);
} else if (d is DatatypeDecl) {
AddDatatype((DatatypeDecl)d);
} else {
@@ -379,6 +381,8 @@ namespace Microsoft.Dafny {
currentDeclaration = d;
if (d is OpaqueTypeDecl) {
AddTypeDecl((OpaqueTypeDecl)d);
+ } else if (d is DerivedTypeDecl) {
+ AddTypeDecl((DerivedTypeDecl)d);
} else if (d is TypeSynonymDecl) {
// do nothing, just bypass type synonyms in the translation
} else if (d is DatatypeDecl) {
@@ -443,20 +447,30 @@ namespace Microsoft.Dafny {
void AddTypeDecl(OpaqueTypeDecl td) {
Contract.Requires(td != null);
- string nm = nameTypeParam(td.TheType);
+ AddTypeDecl_Aux(td.tok, nameTypeParam(td.TheType), td.TypeArgs);
+ }
+ void AddTypeDecl(DerivedTypeDecl dd) {
+ Contract.Requires(dd != null);
+ AddTypeDecl_Aux(dd.tok, dd.FullName, new List<TypeParameter>());
+ }
+ void AddTypeDecl_Aux(IToken tok, string nm, List<TypeParameter> typeArgs) {
+ Contract.Requires(tok != null);
+ Contract.Requires(nm != null);
+ Contract.Requires(typeArgs != null);
+
if (abstractTypes.Contains(nm)) {
// nothing to do; has already been added
return;
}
- if (td.TypeArgs.Count == 0) {
+ if (typeArgs.Count == 0) {
sink.TopLevelDeclarations.Add(
- new Bpl.Constant(td.tok,
- new TypedIdent(td.tok, nm, predef.Ty), false /* not unique */));
+ new Bpl.Constant(tok,
+ new TypedIdent(tok, nm, predef.Ty), false /* not unique */));
} else {
// Note, the function produced is NOT necessarily injective, because the type may be replaced
// in a refinement module in such a way that the type arguments do not matter.
- var args = new List<Bpl.Variable>(td.TypeArgs.ConvertAll(a => (Bpl.Variable)BplFormalVar(null, predef.Ty, true)));
- var func = new Bpl.Function(td.tok, nm, args, BplFormalVar(null, predef.Ty, false));
+ var args = new List<Bpl.Variable>(typeArgs.ConvertAll(a => (Bpl.Variable)BplFormalVar(null, predef.Ty, true)));
+ var func = new Bpl.Function(tok, nm, args, BplFormalVar(null, predef.Ty, false));
sink.TopLevelDeclarations.Add(func);
}
abstractTypes.Add(nm);
diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy
new file mode 100644
index 00000000..0c242db9
--- /dev/null
+++ b/Test/dafny0/DerivedTypesResolution.dfy
@@ -0,0 +1,27 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+module Cycle {
+ type MySynonym = MyNewType // error: a cycle
+ type MyNewType = new MyIntegerType_WellSupposedly
+ type MyIntegerType_WellSupposedly = MySynonym
+}
+
+module MustBeNumeric {
+ datatype List<T> = Nil | Cons(T, List)
+ type NewDatatype = new List<int> // error: base type must be numeric based
+}
+
+module Goodies {
+ type int32 = new int
+ type posReal = new real
+ type int8 = new int32
+
+ method M()
+ {
+ var k8 := new int8[100];
+ var s: set<int32>;
+ var x: posReal;
+ var y: posReal;
+ }
+}
diff --git a/Test/dafny0/DerivedTypesResolution.dfy.expect b/Test/dafny0/DerivedTypesResolution.dfy.expect
new file mode 100644
index 00000000..09b41101
--- /dev/null
+++ b/Test/dafny0/DerivedTypesResolution.dfy.expect
@@ -0,0 +1,3 @@
+DerivedTypesResolution.dfy(5,7): Error: Cycle among redirecting types (derived types, type synonyms): MySynonym -> MyIntegerType_WellSupposedly -> MyNewType -> MySynonym
+DerivedTypesResolution.dfy(12,7): Error: derived types must be based on some numeric type (got List<int>)
+2 resolution/type errors detected in DerivedTypesResolution.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 50628438..e0c37e2a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1101,7 +1101,7 @@ method TraitSynonym()
var x := new JJ; // error: new cannot be applied to a trait
}
-// ----- set comprehensions where the term type is finite ----
+// ----- set comprehensions where the term type is finite -----
module ObjectSetComprehensions {
// allowed in non-ghost context:
@@ -1114,3 +1114,10 @@ module ObjectSetComprehensions {
method D() { var x := set o : object | true :: o; }
}
+
+// ------ regression test for type checking of integer division -----
+
+method IntegerDivision(s: set<bool>)
+{
+ var t := s / s; // error: / cannot be used with sets
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index ac44375d..b6ebe5dc 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -60,12 +60,12 @@ ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: Bad
ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
-ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A
-ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A
-ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1000,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> A
+ResolutionErrors.dfy(1003,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1007,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A
ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
-ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A
-ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A
+ResolutionErrors.dfy(1019,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A
+ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (derived types, type synonyms): A -> B -> A
ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
@@ -142,7 +142,7 @@ ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specificat
ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool)
+ResolutionErrors.dfy(365,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)
ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int)
@@ -175,4 +175,5 @@ ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from
ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)
ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
-177 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
+178 resolution/type errors detected in ResolutionErrors.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:44:31 +0000