From 10a8896ae40fd918abbb8caa616ac6ee0876ac1d Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 29 May 2015 16:29:15 -0700 Subject: Add an infinite set collection type. --- Source/Dafny/RefinementTransformer.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'Source/Dafny/RefinementTransformer.cs') diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index d819652d..05146b7d 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -452,7 +452,8 @@ namespace Microsoft.Dafny } else if (prev is ObjectType) { return next is ObjectType; } else if (prev is SetType) { - return next is SetType && ResolvedTypesAreTheSame(((SetType)prev).Arg, ((SetType)next).Arg); + return next is SetType && ((SetType)prev).Finite == ((SetType)next).Finite && + ResolvedTypesAreTheSame(((SetType)prev).Arg, ((SetType)next).Arg); } else if (prev is MultiSetType) { return next is MultiSetType && ResolvedTypesAreTheSame(((MultiSetType)prev).Arg, ((MultiSetType)next).Arg); } else if (prev is MapType) { -- cgit v1.2.3 From 85d4456ccf1e1d8c456dffa012d3f3d724f50a4a Mon Sep 17 00:00:00 2001 From: Michael Lowell Roberts Date: Thu, 2 Jul 2015 15:00:52 -0700 Subject: multiple changes... - fix for requirement inheritance in refinement. - minimimally viable implementation of exclusive refinement feature. --- Source/Dafny/Cloner.cs | 11 +- Source/Dafny/Dafny.atg | 5 +- Source/Dafny/DafnyAst.cs | 119 ++++- Source/Dafny/Makefile | 4 +- Source/Dafny/Parser.cs | 962 +++++++++++++++++----------------- Source/Dafny/RefinementTransformer.cs | 9 + Source/Dafny/Resolver.cs | 71 ++- Source/Dafny/Scanner.cs | 198 +++---- Source/Dafny/Translator.cs | 4 +- 9 files changed, 768 insertions(+), 615 deletions(-) (limited to 'Source/Dafny/RefinementTransformer.cs') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index e313ffac..6e64c7ec 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -17,12 +17,15 @@ namespace Microsoft.Dafny if (m is DefaultModuleDecl) { nw = new DefaultModuleDecl(); } else { - nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.RefinementBaseName, m.Module, CloneAttributes(m.Attributes), true); + nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.IsExclusiveRefinement, m.RefinementBaseName, m.Module, CloneAttributes(m.Attributes), true); } foreach (var d in m.TopLevelDecls) { nw.TopLevelDecls.Add(CloneDeclaration(d, nw)); } - nw.RefinementBase = m.RefinementBase; + if (null != m.RefinementBase) { + nw.RefinementBase = m.RefinementBase; + } + nw.ClonedFrom = m; nw.Height = m.Height; return nw; } @@ -33,7 +36,7 @@ namespace Microsoft.Dafny if (d is OpaqueTypeDecl) { var dd = (OpaqueTypeDecl)d; - return new OpaqueTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), CloneAttributes(dd.Attributes)); + return new OpaqueTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), CloneAttributes(dd.Attributes), d); } else if (d is TypeSynonymDecl) { var dd = (TypeSynonymDecl)d; var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); @@ -138,7 +141,7 @@ namespace Microsoft.Dafny } public TypeParameter CloneTypeParam(TypeParameter tp) { - return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport); + return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport, tp); } public MemberDecl CloneMember(MemberDecl member) { diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 5d4a4321..7b51fb5e 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -542,6 +542,7 @@ SubModuleDecl ModuleDecl sm; submodule = null; // appease compiler bool isAbstract = false; + bool isExclusively = false; bool opened = false; .) ( [ "abstract" (. isAbstract = true; .) ] @@ -549,7 +550,9 @@ SubModuleDecl { Attribute } NoUSIdent - [ "refines" QualifiedModuleName ] (. module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); .) + [ "exclusively" "refines" QualifiedModuleName (. isExclusively = true; .) + | "refines" QualifiedModuleName (. isExclusively = false; .) ] + (. module = new ModuleDefinition(id, id.val, isAbstract, false, isExclusively, idRefined == null ? null : idRefined, parent, attrs, false, this); .) "{" (. module.BodyStartTok = t; .) { SubModuleDecl (. module.TopLevelDecls.Add(sm); .) | ClassDecl (. module.TopLevelDecls.Add(c); .) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 712cb00a..134fb4c1 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -86,7 +86,7 @@ namespace Microsoft.Dafny { public class BuiltIns { - public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, null, true); + public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, /*isExclusiveRefinement:*/ false, null, null, null, true); readonly Dictionary arrayTypeDecls = new Dictionary(); readonly Dictionary arrowTypeDecls = new Dictionary(); readonly Dictionary tupleTypeDecls = new Dictionary(); @@ -1486,6 +1486,8 @@ namespace Microsoft.Dafny { IToken INamedRegion.BodyEndTok { get { return BodyEndTok; } } string INamedRegion.Name { get { return Name; } } string compileName; + private readonly Declaration clonedFrom; + public virtual string CompileName { get { if (compileName == null) { @@ -1496,12 +1498,19 @@ namespace Microsoft.Dafny { } public Attributes Attributes; // readonly, except during class merging in the refinement transformations - public Declaration(IToken tok, string name, Attributes attributes) { + public Declaration(IToken tok, string name, Attributes attributes, Declaration clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); this.tok = tok; this.Name = name; this.Attributes = attributes; + this.clonedFrom = clonedFrom; + } + + public Declaration ClonedFrom { + get { + return this.clonedFrom; + } } [Pure] @@ -1513,12 +1522,10 @@ namespace Microsoft.Dafny { internal FreshIdGenerator IdGenerator = new FreshIdGenerator(); } - public class OpaqueType_AsParameter : TypeParameter - { + public class OpaqueType_AsParameter : TypeParameter { public readonly List TypeArgs; public OpaqueType_AsParameter(IToken tok, string name, EqualitySupportValue equalitySupport, List typeArgs) - : base(tok, name, equalitySupport) - { + : base(tok, name, equalitySupport) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(typeArgs != null); @@ -1566,8 +1573,8 @@ namespace Microsoft.Dafny { } public int PositionalIndex; // which type parameter this is (ie. in C, S is 0, T is 1 and U is 2). - public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified) - : base(tok, name, null) { + public TypeParameter(IToken tok, string name, EqualitySupportValue equalitySupport = EqualitySupportValue.Unspecified, Declaration clonedFrom = null) + : base(tok, name, null, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); EqualitySupport = equalitySupport; @@ -1642,7 +1649,7 @@ namespace Microsoft.Dafny { } public class ModuleSignature { - + private ModuleDefinition exclusiveRefinement = null; public readonly Dictionary TopLevels = new Dictionary(); public readonly Dictionary> Ctors = new Dictionary>(); public readonly Dictionary StaticMembers = new Dictionary(); @@ -1663,6 +1670,25 @@ namespace Microsoft.Dafny { return false; } } + + public ModuleDefinition ExclusiveRefinement { + get { + if (null == exclusiveRefinement) { + return ModuleDef == null ? null : ModuleDef.ExclusiveRefinement; + } else { + return exclusiveRefinement; + } + } + + set { + if (null == ExclusiveRefinement) { + exclusiveRefinement = null; + } else { + throw new InvalidOperationException("An exclusive refinement relationship cannot be amended."); + } + } + } + } public class ModuleDefinition : INamedRegion @@ -1678,22 +1704,64 @@ namespace Microsoft.Dafny { public readonly Attributes Attributes; public readonly List RefinementBaseName; // null if no refinement base public ModuleDecl RefinementBaseRoot; // filled in early during resolution, corresponds to RefinementBaseName[0] - public ModuleDefinition RefinementBase; // filled in during resolution (null if no refinement base) + public List Includes; public readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that public readonly Graph CallGraph = new Graph(); // filled in during resolution public int Height; // height in the topological sorting of modules; filled in during resolution public readonly bool IsAbstract; + public readonly bool IsExclusiveRefinement; public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface) private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled. + + private ModuleDefinition exclusiveRefinement; + + public ModuleDefinition ExclusiveRefinement { + get { return exclusiveRefinement; } + set { + if (null == exclusiveRefinement) { + if (!value.IsExclusiveRefinement) { + throw new ArgumentException( + string.Format("Exclusive refinement of {0} with 'new' module {0} is disallowed.", + Name, + value.Name)); + } + // todo: validate state of `value`. + exclusiveRefinement = value; + } else { + throw new InvalidOperationException(string.Format("Exclusive refinement of {0} has already been established {1}; cannot reestabilish as {2}.", Name, exclusiveRefinement.Name, value.Name)); + } + } + } + + public int ExclusiveRefinementCount { get; set; } + + private ModuleDefinition refinementBase; // filled in during resolution via RefinementBase property (null if no refinement base yet or at all). + + public ModuleDefinition RefinementBase { + get { + return refinementBase; + } + + set { + // the refinementBase member may only be changed once. + if (null != refinementBase) { + throw new InvalidOperationException(string.Format("This module ({0}) already has a refinement base ({1}).", Name, refinementBase.Name)); + } + refinementBase = value; + } + } + + public ModuleDefinition ClonedFrom { get; set; } + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(cce.NonNullElements(TopLevelDecls)); Contract.Invariant(CallGraph != null); } - public ModuleDefinition(IToken tok, string name, bool isAbstract, bool isFacade, List refinementBase, ModuleDefinition parent, Attributes attributes, bool isBuiltinName) + public ModuleDefinition(IToken tok, string name, bool isAbstract, bool isFacade, bool isExclusiveRefinement, List refinementBase, ModuleDefinition parent, Attributes attributes, bool isBuiltinName, Parser parser = null) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -1704,8 +1772,9 @@ namespace Microsoft.Dafny { RefinementBaseName = refinementBase; IsAbstract = isAbstract; IsFacade = isFacade; + IsExclusiveRefinement = isExclusiveRefinement; RefinementBaseRoot = null; - RefinementBase = null; + this.refinementBase = null; Includes = new List(); IsBuiltinName = isBuiltinName; } @@ -1844,7 +1913,9 @@ namespace Microsoft.Dafny { } public class DefaultModuleDecl : ModuleDefinition { - public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, null, true) { + public DefaultModuleDecl() + : base(Token.NoToken, "_module", false, false, /*isExclusiveRefinement:*/ false, null, null, null, true) + { } public override bool IsDefaultModule { get { @@ -1862,8 +1933,8 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(TypeArgs)); } - public TopLevelDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, Attributes attributes) - : base(tok, name, attributes) { + public TopLevelDecl(IToken tok, string name, ModuleDefinition module, List typeArgs, Attributes attributes, Declaration clonedFrom = null) + : base(tok, name, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); @@ -2116,7 +2187,7 @@ namespace Microsoft.Dafny { public List Destructors = new List(); // contents filled in during resolution; includes both implicit (not mentionable in source) and explicit destructors public DatatypeCtor(IToken tok, string name, [Captured] List formals, Attributes attributes) - : base(tok, name, attributes) { + : base(tok, name, attributes, null) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(formals)); @@ -2326,7 +2397,7 @@ namespace Microsoft.Dafny { public TopLevelDecl EnclosingClass; // filled in during resolution public MemberDecl RefinementBase; // filled in during the pre-resolution refinement transformation; null if the member is new here public MemberDecl(IToken tok, string name, bool hasStaticKeyword, bool isGhost, Attributes attributes) - : base(tok, name, attributes) { + : base(tok, name, attributes, null) { Contract.Requires(tok != null); Contract.Requires(name != null); HasStaticKeyword = hasStaticKeyword; @@ -2463,8 +2534,8 @@ namespace Microsoft.Dafny { Contract.Invariant(TheType != null && Name == TheType.Name); } - public OpaqueTypeDecl(IToken tok, string name, ModuleDefinition module, TypeParameter.EqualitySupportValue equalitySupport, List typeArgs, Attributes attributes) - : base(tok, name, module, typeArgs, attributes) { + public OpaqueTypeDecl(IToken tok, string name, ModuleDefinition module, TypeParameter.EqualitySupportValue equalitySupport, List typeArgs, Attributes attributes, Declaration clonedFrom = null) + : base(tok, name, module, typeArgs, attributes, clonedFrom) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -3063,7 +3134,7 @@ namespace Microsoft.Dafny { prefixPredCall.TypeArgumentSubstitutions = new Dictionary(); var old_to_new = new Dictionary(); for (int i = 0; i < this.TypeArgs.Count; i++) { - old_to_new[this.TypeArgs[i]] = this.PrefixPredicate.TypeArgs[i]; + old_to_new[this.TypeArgs[i]] = this.PrefixPredicate.TypeArgs[i]; } foreach (var p in fexp.TypeArgumentSubstitutions) { prefixPredCall.TypeArgumentSubstitutions[old_to_new[p.Key]] = p.Value; @@ -5578,8 +5649,8 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(Arguments)); Contract.Invariant(cce.NonNullElements(InferredTypeArgs)); Contract.Invariant( - Ctor == null || - InferredTypeArgs.Count == Ctor.EnclosingDatatype.TypeArgs.Count); + Ctor == null || + InferredTypeArgs.Count == Ctor.EnclosingDatatype.TypeArgs.Count); } public DatatypeValue(IToken tok, string datatypeName, string memberName, [Captured] List arguments) @@ -6009,10 +6080,10 @@ namespace Microsoft.Dafny { Function == null || TypeArgumentSubstitutions == null || Contract.ForAll( Function.TypeArgs, - a => TypeArgumentSubstitutions.ContainsKey(a)) && + a => TypeArgumentSubstitutions.ContainsKey(a)) && Contract.ForAll( TypeArgumentSubstitutions.Keys, - a => Function.TypeArgs.Contains(a) || Function.EnclosingClass.TypeArgs.Contains(a))); + a => Function.TypeArgs.Contains(a) || Function.EnclosingClass.TypeArgs.Contains(a))); } public Function Function; // filled in by resolution diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile index 4c01c780..e8c0f5e0 100644 --- a/Source/Dafny/Makefile +++ b/Source/Dafny/Makefile @@ -4,8 +4,8 @@ # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to # point to whatever directory you install that into. # ############################################################################### -COCO_EXE_DIR = ..\..\..\boogiepartners\CocoRdownload -FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified +COCO_EXE_DIR = ..\..\..\boogie-partners\CocoRdownload +FRAME_DIR = ..\..\..\boogie-partners\CocoR\Modified COCO = $(COCO_EXE_DIR)\Coco.exe # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index c4047819..a90e650a 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -72,10 +72,10 @@ public class Parser { public const int _star = 56; public const int _notIn = 57; public const int _ellipsis = 58; - public const int maxT = 137; + public const int maxT = 138; - const bool T = true; - const bool x = false; + const bool _T = true; + const bool _x = false; const int minErrDist = 2; public Scanner/*!*/ scanner; @@ -540,42 +540,42 @@ bool IsType(ref IToken pt) { } while (StartOf(1)) { switch (la.kind) { - case 60: case 61: case 63: { + case 60: case 61: case 64: { SubModuleDecl(defaultModule, out submodule); defaultModule.TopLevelDecls.Add(submodule); break; } - case 68: { + case 69: { ClassDecl(defaultModule, out c); defaultModule.TopLevelDecls.Add(c); break; } - case 74: case 75: { + case 75: case 76: { DatatypeDecl(defaultModule, out dt); defaultModule.TopLevelDecls.Add(dt); break; } - case 77: { + case 78: { NewtypeDecl(defaultModule, out td); defaultModule.TopLevelDecls.Add(td); break; } - case 78: { + case 79: { OtherTypeDecl(defaultModule, out td); defaultModule.TopLevelDecls.Add(td); break; } - case 79: { + case 80: { IteratorDecl(defaultModule, out iter); defaultModule.TopLevelDecls.Add(iter); break; } - case 70: { + case 71: { TraitDecl(defaultModule, out trait); defaultModule.TopLevelDecls.Add(trait); break; } - case 37: case 38: case 39: case 40: case 41: case 71: case 72: case 73: case 76: case 82: case 83: case 84: case 85: { + case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { ClassMemberDecl(membersDefaultClass, false, !DafnyOptions.O.AllowGlobals); break; } @@ -606,6 +606,7 @@ bool IsType(ref IToken pt) { ModuleDecl sm; submodule = null; // appease compiler bool isAbstract = false; + bool isExclusively = false; bool opened = false; if (la.kind == 60 || la.kind == 61) { @@ -618,51 +619,59 @@ bool IsType(ref IToken pt) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 62) { - Get(); - QualifiedModuleName(out idRefined); + if (la.kind == 62 || la.kind == 63) { + if (la.kind == 62) { + Get(); + Expect(63); + QualifiedModuleName(out idRefined); + isExclusively = true; + } else { + Get(); + QualifiedModuleName(out idRefined); + isExclusively = false; + } } - module = new ModuleDefinition(id, id.val, isAbstract, false, idRefined == null ? null : idRefined, parent, attrs, false); + module = new ModuleDefinition(id, id.val, isAbstract, false, isExclusively, idRefined == null ? null : idRefined, parent, attrs, false, this); Expect(45); module.BodyStartTok = t; while (StartOf(1)) { switch (la.kind) { - case 60: case 61: case 63: { + case 60: case 61: case 64: { SubModuleDecl(module, out sm); module.TopLevelDecls.Add(sm); break; } - case 68: { + case 69: { ClassDecl(module, out c); module.TopLevelDecls.Add(c); break; } - case 70: { + case 71: { TraitDecl(module, out trait); module.TopLevelDecls.Add(trait); break; } - case 74: case 75: { + case 75: case 76: { DatatypeDecl(module, out dt); module.TopLevelDecls.Add(dt); break; } - case 77: { + case 78: { NewtypeDecl(module, out td); module.TopLevelDecls.Add(td); break; } - case 78: { + case 79: { OtherTypeDecl(module, out td); module.TopLevelDecls.Add(td); break; } - case 79: { + case 80: { IteratorDecl(module, out iter); module.TopLevelDecls.Add(iter); break; } - case 37: case 38: case 39: case 40: case 41: case 71: case 72: case 73: case 76: case 82: case 83: case 84: case 85: { + case 37: case 38: case 39: case 40: case 41: case 72: case 73: case 74: case 77: case 83: case 84: case 85: case 86: { ClassMemberDecl(namedModuleDefaultClassMembers, false, !DafnyOptions.O.AllowGlobals); break; } @@ -672,22 +681,22 @@ bool IsType(ref IToken pt) { module.BodyEndTok = t; module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); submodule = new LiteralModuleDecl(module, parent); - } else if (la.kind == 63) { + } else if (la.kind == 64) { Get(); - if (la.kind == 64) { + if (la.kind == 65) { Get(); opened = true; } NoUSIdent(out id); - if (la.kind == 65 || la.kind == 66) { - if (la.kind == 65) { + if (la.kind == 66 || la.kind == 67) { + if (la.kind == 66) { Get(); QualifiedModuleName(out idPath); submodule = new AliasModuleDecl(idPath, id, parent, opened); } else { Get(); QualifiedModuleName(out idPath); - if (la.kind == 67) { + if (la.kind == 68) { Get(); QualifiedModuleName(out idAssignment); } @@ -695,7 +704,7 @@ bool IsType(ref IToken pt) { } } if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(138); Get();} + while (!(la.kind == 0 || la.kind == 27)) {SynErr(139); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a sub-module declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -705,7 +714,7 @@ bool IsType(ref IToken pt) { submodule = new AliasModuleDecl(idPath, id, parent, opened); } - } else SynErr(139); + } else SynErr(140); } void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { @@ -719,8 +728,8 @@ bool IsType(ref IToken pt) { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 68)) {SynErr(140); Get();} - Expect(68); + while (!(la.kind == 0 || la.kind == 69)) {SynErr(141); Get();} + Expect(69); while (la.kind == 45) { Attribute(ref attrs); } @@ -728,7 +737,7 @@ bool IsType(ref IToken pt) { if (la.kind == 51) { GenericParameters(typeArgs); } - if (la.kind == 69) { + if (la.kind == 70) { Get(); Type(out trait); traits.Add(trait); @@ -760,13 +769,13 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; - while (!(la.kind == 0 || la.kind == 74 || la.kind == 75)) {SynErr(141); Get();} - if (la.kind == 74) { + while (!(la.kind == 0 || la.kind == 75 || la.kind == 76)) {SynErr(142); Get();} + if (la.kind == 75) { Get(); - } else if (la.kind == 75) { + } else if (la.kind == 76) { Get(); co = true; - } else SynErr(142); + } else SynErr(143); while (la.kind == 45) { Attribute(ref attrs); } @@ -774,7 +783,7 @@ bool IsType(ref IToken pt) { if (la.kind == 51) { GenericParameters(typeArgs); } - Expect(65); + Expect(66); bodyStart = t; DatatypeMemberDecl(ctors); while (la.kind == 23) { @@ -782,7 +791,7 @@ bool IsType(ref IToken pt) { DatatypeMemberDecl(ctors); } if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(143); Get();} + while (!(la.kind == 0 || la.kind == 27)) {SynErr(144); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate a (co)datatype declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -803,12 +812,12 @@ bool IsType(ref IToken pt) { Type baseType = null; Expression wh; - Expect(77); + Expect(78); while (la.kind == 45) { Attribute(ref attrs); } NoUSIdent(out id); - Expect(65); + Expect(66); if (IsIdentColonOrBar()) { NoUSIdent(out bvId); if (la.kind == 21) { @@ -822,7 +831,7 @@ bool IsType(ref IToken pt) { } else if (StartOf(3)) { Type(out baseType); td = new NewtypeDecl(theVerifyThisFile ? id : new IncludeToken(id), id.val, module, baseType, attrs); - } else SynErr(144); + } else SynErr(145); } void OtherTypeDecl(ModuleDefinition module, out TopLevelDecl td) { @@ -833,7 +842,7 @@ bool IsType(ref IToken pt) { td = null; Type ty; - Expect(78); + Expect(79); while (la.kind == 45) { Attribute(ref attrs); } @@ -850,18 +859,18 @@ bool IsType(ref IToken pt) { if (la.kind == 51) { GenericParameters(typeArgs); } - if (la.kind == 65) { + if (la.kind == 66) { Get(); Type(out ty); td = new TypeSynonymDecl(id, id.val, typeArgs, module, ty, attrs); } - } else SynErr(145); + } else SynErr(146); if (td == null) { td = new OpaqueTypeDecl(id, id.val, module, eqSupport, typeArgs, attrs); } if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(146); Get();} + while (!(la.kind == 0 || la.kind == 27)) {SynErr(147); Get();} Get(); errors.Warning(t, "the semi-colon that used to terminate an opaque-type declaration has been deprecated; in the new syntax, just leave off the semi-colon"); } @@ -890,8 +899,8 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 79)) {SynErr(147); Get();} - Expect(79); + while (!(la.kind == 0 || la.kind == 80)) {SynErr(148); Get();} + Expect(80); while (la.kind == 45) { Attribute(ref attrs); } @@ -901,8 +910,8 @@ bool IsType(ref IToken pt) { GenericParameters(typeArgs); } Formals(true, true, ins); - if (la.kind == 80 || la.kind == 81) { - if (la.kind == 80) { + if (la.kind == 81 || la.kind == 82) { + if (la.kind == 81) { Get(); } else { Get(); @@ -913,7 +922,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(148); + } else SynErr(149); while (StartOf(5)) { IteratorSpec(reads, mod, decreases, req, ens, yieldReq, yieldEns, ref readsAttrs, ref modAttrs, ref decrAttrs); } @@ -940,8 +949,8 @@ bool IsType(ref IToken pt) { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 70)) {SynErr(149); Get();} - Expect(70); + while (!(la.kind == 0 || la.kind == 71)) {SynErr(150); Get();} + Expect(71); while (la.kind == 45) { Attribute(ref attrs); } @@ -968,11 +977,11 @@ bool IsType(ref IToken pt) { MemberModifiers mmod = new MemberModifiers(); IToken staticToken = null, protectedToken = null; - while (la.kind == 71 || la.kind == 72 || la.kind == 73) { - if (la.kind == 71) { + while (la.kind == 72 || la.kind == 73 || la.kind == 74) { + if (la.kind == 72) { Get(); mmod.IsGhost = true; - } else if (la.kind == 72) { + } else if (la.kind == 73) { Get(); mmod.IsStatic = true; staticToken = t; } else { @@ -980,7 +989,7 @@ bool IsType(ref IToken pt) { mmod.IsProtected = true; protectedToken = t; } } - if (la.kind == 76) { + if (la.kind == 77) { if (moduleLevelDecl) { SemErr(la, "fields are not allowed to be declared at the module level; instead, wrap the field in a 'class' declaration"); mmod.IsStatic = false; @@ -1008,7 +1017,7 @@ bool IsType(ref IToken pt) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(150); + } else SynErr(151); } void Attribute(ref Attributes attrs) { @@ -1093,8 +1102,8 @@ bool IsType(ref IToken pt) { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 76)) {SynErr(151); Get();} - Expect(76); + while (!(la.kind == 0 || la.kind == 77)) {SynErr(152); Get();} + Expect(77); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } while (la.kind == 45) { @@ -1131,7 +1140,7 @@ bool IsType(ref IToken pt) { if (la.kind == 37) { Get(); - if (la.kind == 82) { + if (la.kind == 83) { Get(); isFunctionMethod = true; } @@ -1151,11 +1160,11 @@ bool IsType(ref IToken pt) { } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(152); + } else SynErr(153); } else if (la.kind == 38) { Get(); isPredicate = true; - if (la.kind == 82) { + if (la.kind == 83) { Get(); isFunctionMethod = true; } @@ -1182,7 +1191,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(153); + } else SynErr(154); } else if (la.kind == 39) { Get(); Expect(38); @@ -1205,7 +1214,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(154); + } else SynErr(155); } else if (la.kind == 41) { Get(); isCoPredicate = true; @@ -1227,8 +1236,8 @@ bool IsType(ref IToken pt) { } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(155); - } else SynErr(156); + } else SynErr(156); + } else SynErr(157); decreases = isIndPredicate || isCoPredicate ? null : new List(); while (StartOf(9)) { FunctionSpec(reqs, reads, ens, decreases); @@ -1287,9 +1296,9 @@ bool IsType(ref IToken pt) { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(StartOf(10))) {SynErr(157); Get();} + while (!(StartOf(10))) {SynErr(158); Get();} switch (la.kind) { - case 82: { + case 83: { Get(); break; } @@ -1298,12 +1307,12 @@ bool IsType(ref IToken pt) { isLemma = true; break; } - case 83: { + case 84: { Get(); isCoLemma = true; break; } - case 84: { + case 85: { Get(); isCoLemma = true; errors.Warning(t, "the 'comethod' keyword has been deprecated; it has been renamed to 'colemma'"); @@ -1316,7 +1325,7 @@ bool IsType(ref IToken pt) { isIndLemma = true; break; } - case 85: { + case 86: { Get(); if (allowConstructor) { isConstructor = true; @@ -1326,7 +1335,7 @@ bool IsType(ref IToken pt) { break; } - default: SynErr(158); break; + default: SynErr(159); break; } keywordToken = t; if (isLemma) { @@ -1369,7 +1378,7 @@ bool IsType(ref IToken pt) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins); - if (la.kind == 81) { + if (la.kind == 82) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs); @@ -1377,7 +1386,7 @@ bool IsType(ref IToken pt) { } else if (la.kind == 58) { Get(); signatureEllipsis = t; - } else SynErr(159); + } else SynErr(160); while (StartOf(11)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } @@ -1450,14 +1459,14 @@ bool IsType(ref IToken pt) { } else if (la.kind == 2) { Get(); id = t; - } else SynErr(160); + } else SynErr(161); Expect(21); Type(out ty); } void OldSemi() { if (la.kind == 27) { - while (!(la.kind == 0 || la.kind == 27)) {SynErr(161); Get();} + while (!(la.kind == 0 || la.kind == 27)) {SynErr(162); Get();} Get(); } } @@ -1480,7 +1489,7 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out id)!=null); Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); isGhost = false; - if (la.kind == 71) { + if (la.kind == 72) { Get(); if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } } @@ -1532,7 +1541,7 @@ bool IsType(ref IToken pt) { Contract.Ensures(Contract.ValueAtReturn(out ty)!=null); Contract.Ensures(Contract.ValueAtReturn(out identName)!=null); string name = null; id = Token.NoToken; ty = new BoolType()/*dummy*/; isGhost = false; - if (la.kind == 71) { + if (la.kind == 72) { Get(); isGhost = true; } @@ -1554,7 +1563,7 @@ bool IsType(ref IToken pt) { id = t; name = id.val; Expect(21); Type(out ty); - } else SynErr(162); + } else SynErr(163); if (name != null) { identName = name; } else { @@ -1742,7 +1751,7 @@ bool IsType(ref IToken pt) { ty = new UserDefinedType(e.tok, e); break; } - default: SynErr(163); break; + default: SynErr(164); break; } if (la.kind == 29) { Type t2; @@ -1763,7 +1772,7 @@ bool IsType(ref IToken pt) { void Formals(bool incoming, bool allowGhostKeyword, List formals) { Contract.Requires(cce.NonNullElements(formals)); IToken id; Type ty; bool isGhost; Expect(49); - if (la.kind == 1 || la.kind == 71) { + if (la.kind == 1 || la.kind == 72) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); while (la.kind == 22) { @@ -1781,7 +1790,7 @@ List/*!*/ yieldReq, List/*!* ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { Expression/*!*/ e; FrameExpression/*!*/ fe; bool isFree = false; bool isYield = false; Attributes ensAttrs = null; - while (!(StartOf(13))) {SynErr(164); Get();} + while (!(StartOf(13))) {SynErr(165); Get();} if (la.kind == 43) { Get(); while (IsAttribute()) { @@ -1809,13 +1818,13 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } OldSemi(); } else if (StartOf(14)) { - if (la.kind == 86) { + if (la.kind == 87) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); } - if (la.kind == 88) { + if (la.kind == 89) { Get(); isYield = true; } @@ -1829,7 +1838,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { req.Add(new MaybeFreeExpression(e, isFree)); } - } else if (la.kind == 87) { + } else if (la.kind == 88) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1842,7 +1851,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); } - } else SynErr(165); + } else SynErr(166); } else if (la.kind == 35) { Get(); while (IsAttribute()) { @@ -1850,7 +1859,7 @@ ref Attributes readsAttrs, ref Attributes modAttrs, ref Attributes decrAttrs) { } DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(166); + } else SynErr(167); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -1872,7 +1881,7 @@ List/*!*/ 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(167); Get();} + while (!(StartOf(16))) {SynErr(168); Get();} if (la.kind == 42) { Get(); while (IsAttribute()) { @@ -1886,8 +1895,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod.Add(fe); } OldSemi(); - } else if (la.kind == 44 || la.kind == 86 || la.kind == 87) { - if (la.kind == 86) { + } else if (la.kind == 44 || la.kind == 87 || la.kind == 88) { + if (la.kind == 87) { Get(); isFree = true; errors.Warning(t, "the 'free' keyword is soon to be deprecated"); @@ -1898,7 +1907,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false, false); OldSemi(); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 87) { + } else if (la.kind == 88) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); @@ -1906,7 +1915,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out e, false, false); OldSemi(); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(168); + } else SynErr(169); } else if (la.kind == 35) { Get(); while (IsAttribute()) { @@ -1914,7 +1923,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } DecreasesList(decreases, true, false); OldSemi(); - } else SynErr(169); + } else SynErr(170); } void FrameExpression(out FrameExpression fe, bool allowSemi, bool allowLambda) { @@ -1927,18 +1936,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(7)) { Expression(out e, allowSemi, allowLambda); feTok = e.tok; - if (la.kind == 89) { + if (la.kind == 90) { Get(); Ident(out id); fieldName = id.val; feTok = id; } fe = new FrameExpression(feTok, e, fieldName); - } else if (la.kind == 89) { + } else if (la.kind == 90) { Get(); Ident(out id); fieldName = id.val; fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); - } else SynErr(170); + } else SynErr(171); } void DecreasesList(List decreases, bool allowWildcard, bool allowLambda) { @@ -1993,7 +2002,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - while (!(StartOf(17))) {SynErr(171); Get();} + while (!(StartOf(17))) {SynErr(172); Get();} if (la.kind == 44) { Get(); Expression(out e, false, false); @@ -2009,7 +2018,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo reads.Add(fe); } OldSemi(); - } else if (la.kind == 87) { + } else if (la.kind == 88) { Get(); Expression(out e, false, false); OldSemi(); @@ -2023,7 +2032,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DecreasesList(decreases, false, false); OldSemi(); - } else SynErr(172); + } else SynErr(173); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -2042,7 +2051,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(t, new WildcardExpr(t), null); } else if (StartOf(18)) { FrameExpression(out fe, allowSemi, false); - } else SynErr(173); + } else SynErr(174); } void PossiblyWildExpression(out Expression e, bool allowLambda) { @@ -2053,7 +2062,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t); } else if (StartOf(7)) { Expression(out e, false, allowLambda); - } else SynErr(174); + } else SynErr(175); } void Stmt(List/*!*/ ss) { @@ -2070,14 +2079,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(19))) {SynErr(175); Get();} + while (!(StartOf(19))) {SynErr(176); Get();} switch (la.kind) { case 45: { BlockStmt(out bs, out bodyStart, out bodyEnd); s = bs; break; } - case 100: { + case 101: { AssertStmt(out s); break; } @@ -2085,31 +2094,31 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssumeStmt(out s); break; } - case 101: { + case 102: { PrintStmt(out s); break; } - case 1: case 2: case 3: case 4: case 8: case 10: case 19: case 20: case 23: case 49: case 130: case 131: case 132: case 133: case 134: case 135: { + case 1: case 2: case 3: case 4: case 8: case 10: case 19: case 20: case 23: case 49: case 131: case 132: case 133: case 134: case 135: case 136: { UpdateStmt(out s); break; } - case 71: case 76: { + case 72: case 77: { VarDeclStatement(out s); break; } - case 97: { + case 98: { IfStmt(out s); break; } - case 98: { + case 99: { WhileStmt(out s); break; } - case 99: { + case 100: { MatchStmt(out s); break; } - case 102: case 103: { + case 103: case 104: { ForallStmt(out s); break; } @@ -2117,11 +2126,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo CalcStmt(out s); break; } - case 104: { + case 105: { ModifyStmt(out s); break; } - case 90: { + case 91: { Get(); x = t; NoUSIdent(out id); @@ -2130,24 +2139,24 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo s.Labels = new LList