From 474402019659b954371e46891f0e6ac8679dd574 Mon Sep 17 00:00:00 2001 From: Jason Koenig Date: Tue, 26 Jun 2012 17:06:33 -0700 Subject: Dafny: Implemented abstract modules --- Binaries/DafnyPrelude.bpl | 7 + Source/Dafny/Compiler.cs | 8 +- Source/Dafny/Dafny.atg | 55 +- Source/Dafny/DafnyAst.cs | 136 ++-- Source/Dafny/DafnyMain.cs | 2 +- Source/Dafny/DafnyPipeline.csproj | 1 + Source/Dafny/Parser.cs | 845 +++++++++++----------- Source/Dafny/Printer.cs | 18 +- Source/Dafny/RefinementTransformer.cs | 61 +- Source/Dafny/Resolver.cs | 768 +++++++++++++++----- Source/Dafny/Rewriter.cs | 8 +- Source/Dafny/Scanner.cs | 96 +-- Source/Dafny/Translator.cs | 61 +- Source/Dafny/Util.cs | 20 + Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs | 3 +- 15 files changed, 1295 insertions(+), 794 deletions(-) create mode 100644 Source/Dafny/Util.cs diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index fef8fe1f..53d0b471 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -500,6 +500,13 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) } function DeclType(Field T): ClassName; +type NameFamily; +function DeclName(Field T): NameFamily; +function FieldOfDecl(ClassName, NameFamily): Field alpha; +axiom (forall cl : ClassName, nm: NameFamily :: + {FieldOfDecl(cl, nm): Field T} + DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm); + // --------------------------------------------------------------- // -- Allocatedness ---------------------------------------------- // --------------------------------------------------------------- diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index e72c04dd..7f48e551 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny { ReadRuntimeSystem(); CompileBuiltIns(program.BuiltIns); - foreach (ModuleDecl m in program.Modules) { + foreach (ModuleDefinition m in program.Modules) { if (m.IsGhost) { // the purpose of a ghost module is to skip compilation continue; @@ -91,7 +91,7 @@ namespace Microsoft.Dafny { wr.WriteLine(" { }"); CompileDatatypeConstructors(dt, indent); CompileDatatypeStruct(dt, indent); - } else { + } else if (d is ClassDecl) { ClassDecl cl = (ClassDecl)d; Indent(indent); wr.Write("public class @{0}", cl.CompileName); @@ -101,7 +101,9 @@ namespace Microsoft.Dafny { wr.WriteLine(" {"); CompileClassMembers(cl, indent+IndentAmount); Indent(indent); wr.WriteLine("}"); - } + } else if (d is ModuleDecl) { + // nop + } else { Contract.Assert(false); } } if (!m.IsDefaultModule) { wr.WriteLine("}} // end of namespace {0}", m.CompileName); diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 4b76f9b4..ca8f934e 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -71,7 +71,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, Contract.Requires(filename != null); Contract.Requires(module != null); Contract.Requires(errors != null); - ModuleDecl oldModule = theModule; + var oldModule = theModule; theModule = module; BuiltIns oldBuiltIns = builtIns; theBuiltIns = builtIns; @@ -132,9 +132,9 @@ PRODUCTIONS Dafny = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; List membersDefaultClass = new List(); - SubModuleDecl submodule; + ModuleDecl submodule; // to support multiple files, create a default module only if theModule is null - DefaultModuleDecl defaultModule = theModule as DefaultModuleDecl; + DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef; // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl) Contract.Assert(defaultModule != null); bool isGhost; @@ -163,23 +163,22 @@ Dafny } .) EOF . -SubModuleDecl +SubModuleDecl = (. ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; Attributes attrs = null; IToken/*!*/ id; List namedModuleDefaultClassMembers = new List();; - IToken idRefined = null; - List theImports = new List(); + List idRefined = null, idPath = null; bool isGhost = false; - ModuleDecl module; - SubModuleDecl sm; + ModuleDefinition module; + ModuleDecl sm; + submodule = null; // appease compiler .) - "module" - { Attribute } - NoUSIdent (. .) - [ "refines" Ident ] - [ "imports" Idents ] (. module = new ModuleDecl(id, id.val, isOverallModuleGhost, idRefined == null ? null : idRefined.val, theImports, attrs); - parent.Dependencies.Add(module); .) - "{" (. module.BodyStartTok = t; .) + "module" + { Attribute } + NoUSIdent + (( + [ "refines" QualifiedName ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); .) + "{" (. module.BodyStartTok = t; .) { (. isGhost = false; .) [ "ghost" (. isGhost = true; .) ] ( SubModuleDecl (. module.TopLevelDecls.Add(sm); .) @@ -194,10 +193,22 @@ SubModuleDecl ";" (.submodule = new AbstractModuleDecl(idPath, id, parent); .) + ) . -ClassDecl +QualifiedName<.out List ids.> += (. IToken id; ids = new List(); .) + Ident (. ids.Add(id); .) + { "." Ident (. ids.Add(id); .) + } + . + +ClassDecl = (. Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ id; @@ -235,7 +246,7 @@ ClassMemberDecl<.List/*!*/ mm, bool isAlreadyGhost, bool allowC | MethodDecl (. mm.Add(m); .) ) . -DatatypeDecl +DatatypeDecl = (. Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out dt)!=null); IToken/*!*/ id; @@ -291,7 +302,7 @@ FieldDecl<.MemberModifiers mmod, List/*!*/ mm.> } SYNC ";" . -ArbitraryTypeDecl +ArbitraryTypeDecl = (. IToken/*!*/ id; Attributes attrs = null; .) @@ -1629,12 +1640,6 @@ AttributeArg ) . /*------------------------------------------------------------------------*/ -Idents<.List/*!*/ ids.> -= (. IToken/*!*/ id; .) - Ident (. ids.Add(id.val); .) - { "," Ident (. ids.Add(id.val); .) - } - . Ident = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .) ident (. x = t; .) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index dc012b32..19bb8b72 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -19,24 +19,27 @@ namespace Microsoft.Dafny { } public readonly string Name; - public List/*!*/ Modules; // filled in during resolution. + public List/*!*/ Modules; // filled in during resolution. // Resolution essentially flattens the module heirarchy, for // purposes of translation and compilation. public readonly ModuleDecl DefaultModule; + public readonly ModuleDefinition DefaultModuleDef; public readonly BuiltIns BuiltIns; public Program(string name, [Captured] ModuleDecl module, [Captured] BuiltIns builtIns) { Contract.Requires(name != null); Contract.Requires(module != null); + Contract.Requires(module is LiteralModuleDecl); Name = name; DefaultModule = module; + DefaultModuleDef = (DefaultModuleDecl)((LiteralModuleDecl)module).ModuleDef; BuiltIns = builtIns; - Modules = new List(); + Modules = new List(); } } public class BuiltIns { - public readonly ModuleDecl SystemModule = new ModuleDecl(Token.NoToken, "_System", false, null, new List(), null); + public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null); Dictionary arrayTypeDecls = new Dictionary(); public BuiltIns() { @@ -734,46 +737,100 @@ namespace Microsoft.Dafny { } } - public class SubModuleDecl : TopLevelDecl { - public readonly ModuleDecl SubModule; - public SubModuleDecl(ModuleDecl submodule, ModuleDecl parent) - : base(submodule.tok, submodule.Name, parent, new List(), submodule.Attributes) { - SubModule = submodule; + // Represents a submodule declartion at module level scope + abstract public class ModuleDecl : TopLevelDecl + { + public ModuleSignature Signature; // filled in by resolution, in topological order. + public int Height; + public ModuleDecl(IToken tok, string name, ModuleDefinition parent) + : base(tok, name, parent, new List(), null) { + Height = -1; + Signature = null; + } + } + // Represents module X { ... } + public class LiteralModuleDecl : ModuleDecl + { + public readonly ModuleDefinition ModuleDef; + public LiteralModuleDecl(ModuleDefinition module, ModuleDefinition parent) + : base(module.tok, module.Name, parent) { + ModuleDef = module; } } - public class ModuleDecl : Declaration { - public readonly string RefinementBaseName; // null if no refinement base - public ModuleDecl RefinementBase; // filled in during resolution (null if no refinement base) - public readonly List/*!*/ ImportNames; // contains no duplicates - public readonly List/*!*/ Dependencies; // filled in during parsing. contains submodules dependencies. - public readonly List/*!*/ Imports = new List(); // filled in during resolution, contains no duplicates + // Represents "module name = path;", where name is a identifier and path is a possibly qualified name. + public class AliasModuleDecl : ModuleDecl + { + public ModuleDecl ModuleReference; // should refer to another declaration somewhere. NOTE: cyclicity is possible, and should + // be detected and warned. + public readonly List Path; // generated by the parser, this is looked up + public ModuleDecl Root; // the moduleDecl that Path[0] refers to. + public AliasModuleDecl(List path, IToken name, ModuleDefinition parent) + : base(name, name.val, parent) { + Contract.Requires(path != null && path.Count > 0); + Path = path; + ModuleReference = null; + } + } + // Represents "module name as path;", where name is a identifier and path is a possibly qualified name. + public class AbstractModuleDecl : ModuleDecl + { + public ModuleDecl Root; + public readonly List Path; + public AbstractModuleDecl(List path, IToken name, ModuleDefinition parent) + : base(name, name.val, parent) { + Path = path; + Root = null; + } + } + + public class ModuleSignature { + + public readonly Dictionary TopLevels = new Dictionary(); + public readonly Dictionary> Ctors = new Dictionary>(); + public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e. + // it is abstract). Otherwise, it points to that definition. + public ModuleSignature() {} + + public bool FindSubmodule(string name, out ModuleSignature pp) { + TopLevelDecl top; + pp = null; + if (TopLevels.TryGetValue(name, out top)) { + if (top is ModuleDecl) { + pp = ((ModuleDecl)top).Signature; + return true; + } else return false; + } else return false; + } + + + } + public class ModuleDefinition : Declaration { + 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 readonly List TopLevelDecls = new List(); // filled in by the parser; readonly after that + public Resolver.ModuleBindings Bindings; 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 IsGhost; + public readonly bool IsAbstract; // True iff this module represents an abstract interface [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(cce.NonNullElements(ImportNames)); Contract.Invariant(cce.NonNullElements(TopLevelDecls)); Contract.Invariant(CallGraph != null); } - public ModuleDecl(IToken tok, string name, bool isGhost, string refinementBase, [Captured] List/*!*/ imports, Attributes attributes) + public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List refinementBase, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); - Contract.Requires(cce.NonNullElements(imports)); RefinementBaseName = refinementBase; - // set "ImportNames" to "imports" minus any duplicates - ImportNames = new List(); - Dependencies = new List(); - foreach (var nm in imports) { - if (!ImportNames.Contains(nm)) { - ImportNames.Add(nm); - } - } IsGhost = isGhost; + IsAbstract = isAbstract; + RefinementBaseRoot = null; + RefinementBase = null; } public virtual bool IsDefaultModule { get { @@ -784,20 +841,15 @@ namespace Microsoft.Dafny { new public string CompileName { get { if (compileName == null) { - compileName = NonglobalVariable.CompilerizeName(Name) + "_" + Height.ToString(); + compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name); } return compileName; } } - public string UniqueName { - get { - return Name + "_" + Height.ToString(); - } - } } - public class DefaultModuleDecl : ModuleDecl { - public DefaultModuleDecl() : base(Token.NoToken, "_default", false, null, new List(), null) { + public class DefaultModuleDecl : ModuleDefinition { + public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null) { } public override bool IsDefaultModule { get { @@ -807,7 +859,7 @@ namespace Microsoft.Dafny { } public abstract class TopLevelDecl : Declaration, TypeParameter.ParentType { - public readonly ModuleDecl Module; + public readonly ModuleDefinition Module; public readonly List/*!*/ TypeArgs; [ContractInvariantMethod] void ObjectInvariant() { @@ -815,7 +867,7 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(TypeArgs)); } - public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, Attributes attributes) + public TopLevelDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs, Attributes attributes) : base(tok, name, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -845,7 +897,7 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(Members)); } - public ClassDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, + public ClassDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ members, Attributes attributes) : base(tok, name, module, typeArgs, attributes) { Contract.Requires(tok != null); @@ -865,7 +917,7 @@ namespace Microsoft.Dafny { } public class DefaultClassDecl : ClassDecl { - public DefaultClassDecl(ModuleDecl/*!*/ module, [Captured] List/*!*/ members) + public DefaultClassDecl(ModuleDefinition/*!*/ module, [Captured] List/*!*/ members) : base(Token.NoToken, "_default", module, new List(), members, null) { Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(members)); @@ -879,7 +931,7 @@ namespace Microsoft.Dafny { public class ArrayClassDecl : ClassDecl { public readonly int Dims; - public ArrayClassDecl(int dims, ModuleDecl module) + public ArrayClassDecl(int dims, ModuleDefinition module) : base(Token.NoToken, BuiltIns.ArrayClassName(dims), module, new List(new TypeParameter[]{new TypeParameter(Token.NoToken, "arg")}), new List(), null) @@ -899,7 +951,7 @@ namespace Microsoft.Dafny { Contract.Invariant(1 <= Ctors.Count); } - public DatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, + public DatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ ctors, Attributes attributes) : base(tok, name, module, typeArgs, attributes) { Contract.Requires(tok != null); @@ -917,7 +969,7 @@ namespace Microsoft.Dafny { public DatatypeCtor DefaultCtor; // set during resolution public bool[] TypeParametersUsedInConstructionByDefaultCtor; // set during resolution; has same length as - public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, + public IndDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ ctors, Attributes attributes) : base(tok, name, module, typeArgs, ctors, attributes) { Contract.Requires(tok != null); @@ -931,7 +983,7 @@ namespace Microsoft.Dafny { public class CoDatatypeDecl : DatatypeDecl { - public CoDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, List/*!*/ typeArgs, + public CoDatatypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, List/*!*/ typeArgs, [Captured] List/*!*/ ctors, Attributes attributes) : base(tok, name, module, typeArgs, ctors, attributes) { Contract.Requires(tok != null); @@ -1075,7 +1127,7 @@ namespace Microsoft.Dafny { Contract.Invariant(TheType != null && Name == TheType.Name); } - public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDecl/*!*/ module, Attributes attributes) + public ArbitraryTypeDecl(IToken/*!*/ tok, string/*!*/ name, ModuleDefinition/*!*/ module, Attributes attributes) : base(tok, name, module, new List(), attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); diff --git a/Source/Dafny/DafnyMain.cs b/Source/Dafny/DafnyMain.cs index 90c2de44..6091e522 100644 --- a/Source/Dafny/DafnyMain.cs +++ b/Source/Dafny/DafnyMain.cs @@ -20,7 +20,7 @@ namespace Microsoft.Dafny { Contract.Requires(programName != null); Contract.Requires(fileNames != null); program = null; - ModuleDecl module = new DefaultModuleDecl(); + ModuleDecl module = new LiteralModuleDecl(new DefaultModuleDecl(), null); BuiltIns builtIns = new BuiltIns(); foreach (string dafnyFileName in fileNames){ Contract.Assert(dafnyFileName != null); diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index cf2b51eb..14ff3348 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -151,6 +151,7 @@ + diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 3f58c1db..931970ca 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -91,7 +91,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, ModuleDecl module, Contract.Requires(filename != null); Contract.Requires(module != null); Contract.Requires(errors != null); - ModuleDecl oldModule = theModule; + var oldModule = theModule; theModule = module; BuiltIns oldBuiltIns = builtIns; theBuiltIns = builtIns; @@ -182,9 +182,9 @@ bool IsAttribute() { void Dafny() { ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; List membersDefaultClass = new List(); - SubModuleDecl submodule; + ModuleDecl submodule; // to support multiple files, create a default module only if theModule is null - DefaultModuleDecl defaultModule = theModule as DefaultModuleDecl; + DefaultModuleDecl defaultModule = (DefaultModuleDecl)((LiteralModuleDecl)theModule).ModuleDef; // theModule should be a DefaultModuleDecl (actually, the singular DefaultModuleDecl) Contract.Assert(defaultModule != null); bool isGhost; @@ -198,15 +198,15 @@ bool IsAttribute() { if (la.kind == 9) { SubModuleDecl(defaultModule, isGhost, out submodule); defaultModule.TopLevelDecls.Add(submodule); - } else if (la.kind == 12) { + } else if (la.kind == 15) { if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } ClassDecl(defaultModule, out c); defaultModule.TopLevelDecls.Add(c); - } else if (la.kind == 14 || la.kind == 15) { + } else if (la.kind == 17 || la.kind == 18) { if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } DatatypeDecl(defaultModule, out dt); defaultModule.TopLevelDecls.Add(dt); - } else if (la.kind == 21) { + } else if (la.kind == 22) { if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } ArbitraryTypeDecl(defaultModule, out at); defaultModule.TopLevelDecls.Add(at); @@ -224,66 +224,72 @@ bool IsAttribute() { Expect(0); } - void SubModuleDecl(ModuleDecl parent, bool isOverallModuleGhost, out SubModuleDecl submodule) { + void SubModuleDecl(ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl submodule) { ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt; ArbitraryTypeDecl at; Attributes attrs = null; IToken/*!*/ id; List namedModuleDefaultClassMembers = new List();; - IToken idRefined = null; - List theImports = new List(); + List idRefined = null, idPath = null; bool isGhost = false; - ModuleDecl module; - SubModuleDecl sm; + ModuleDefinition module; + ModuleDecl sm; + submodule = null; // appease compiler Expect(9); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - - if (la.kind == 10) { - Get(); - Ident(out idRefined); - } - if (la.kind == 11) { - Get(); - Idents(theImports); - } - module = new ModuleDecl(id, id.val, isOverallModuleGhost, idRefined == null ? null : idRefined.val, theImports, attrs); - parent.Dependencies.Add(module); - Expect(6); - module.BodyStartTok = t; - while (StartOf(1)) { - isGhost = false; - if (la.kind == 8) { + if (la.kind == 6 || la.kind == 10) { + if (la.kind == 10) { Get(); - isGhost = true; + QualifiedName(out idRefined); } - if (la.kind == 9) { - SubModuleDecl(module, isGhost, out sm); - module.TopLevelDecls.Add(sm); - } else if (la.kind == 12) { - if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } - ClassDecl(module, out c); - module.TopLevelDecls.Add(c); - } else if (la.kind == 14 || la.kind == 15) { - if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } - DatatypeDecl(module, out dt); - module.TopLevelDecls.Add(dt); - } else if (la.kind == 21) { - if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } - ArbitraryTypeDecl(module, out at); - module.TopLevelDecls.Add(at); - } else if (StartOf(2)) { - ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false); - } else SynErr(109); - } - Expect(7); - module.BodyEndTok = t; - module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); - submodule = new SubModuleDecl(module, parent); + module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); + Expect(6); + module.BodyStartTok = t; + while (StartOf(1)) { + isGhost = false; + if (la.kind == 8) { + Get(); + isGhost = true; + } + if (la.kind == 9) { + SubModuleDecl(module, isGhost, out sm); + module.TopLevelDecls.Add(sm); + } else if (la.kind == 15) { + if (isGhost) { SemErr(t, "a class is not allowed to be declared as 'ghost'"); } + ClassDecl(module, out c); + module.TopLevelDecls.Add(c); + } else if (la.kind == 17 || la.kind == 18) { + if (isGhost) { SemErr(t, "a datatype/codatatype is not allowed to be declared as 'ghost'"); } + DatatypeDecl(module, out dt); + module.TopLevelDecls.Add(dt); + } else if (la.kind == 22) { + if (isGhost) { SemErr(t, "a type is not allowed to be declared as 'ghost'"); } + ArbitraryTypeDecl(module, out at); + module.TopLevelDecls.Add(at); + } else if (StartOf(2)) { + ClassMemberDecl(namedModuleDefaultClassMembers, isGhost, false); + } else SynErr(109); + } + Expect(7); + module.BodyEndTok = t; + module.TopLevelDecls.Add(new DefaultClassDecl(module, namedModuleDefaultClassMembers)); + submodule = new LiteralModuleDecl(module, parent); + } else if (la.kind == 11) { + Get(); + QualifiedName(out idPath); + Expect(12); + submodule = new AliasModuleDecl(idPath, id, parent); + } else if (la.kind == 13) { + Get(); + QualifiedName(out idPath); + Expect(12); + submodule = new AbstractModuleDecl(idPath, id, parent); + } else SynErr(110); } - void ClassDecl(ModuleDecl/*!*/ module, out ClassDecl/*!*/ c) { + void ClassDecl(ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c) { Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out c) != null); IToken/*!*/ id; @@ -292,13 +298,13 @@ bool IsAttribute() { List members = new List(); IToken bodyStart; - while (!(la.kind == 0 || la.kind == 12)) {SynErr(110); Get();} - Expect(12); + while (!(la.kind == 0 || la.kind == 15)) {SynErr(111); Get();} + Expect(15); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 22) { + if (la.kind == 23) { GenericParameters(typeArgs); } Expect(6); @@ -313,7 +319,7 @@ bool IsAttribute() { } - void DatatypeDecl(ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt) { + void DatatypeDecl(ModuleDefinition/*!*/ module, out DatatypeDecl/*!*/ dt) { Contract.Requires(module != null); Contract.Ensures(Contract.ValueAtReturn(out dt)!=null); IToken/*!*/ id; @@ -323,29 +329,29 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; // dummy assignment bool co = false; - while (!(la.kind == 0 || la.kind == 14 || la.kind == 15)) {SynErr(111); Get();} - if (la.kind == 14) { + while (!(la.kind == 0 || la.kind == 17 || la.kind == 18)) {SynErr(112); Get();} + if (la.kind == 17) { Get(); - } else if (la.kind == 15) { + } else if (la.kind == 18) { Get(); co = true; - } else SynErr(112); + } else SynErr(113); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 22) { + if (la.kind == 23) { GenericParameters(typeArgs); } - Expect(16); + Expect(11); bodyStart = t; DatatypeMemberDecl(ctors); - while (la.kind == 17) { + while (la.kind == 19) { Get(); DatatypeMemberDecl(ctors); } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(113); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(114); Get();} + Expect(12); if (co) { dt = new CoDatatypeDecl(id, id.val, module, typeArgs, ctors, attrs); } else { @@ -356,18 +362,18 @@ bool IsAttribute() { } - void ArbitraryTypeDecl(ModuleDecl/*!*/ module, out ArbitraryTypeDecl at) { + void ArbitraryTypeDecl(ModuleDefinition/*!*/ module, out ArbitraryTypeDecl at) { IToken/*!*/ id; Attributes attrs = null; - Expect(21); + Expect(22); while (la.kind == 6) { Attribute(ref attrs); } NoUSIdent(out id); at = new ArbitraryTypeDecl(id, id.val, module, attrs); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(114); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(115); Get();} + Expect(12); } void ClassMemberDecl(List/*!*/ mm, bool isAlreadyGhost, bool allowConstructors) { @@ -377,7 +383,7 @@ bool IsAttribute() { MemberModifiers mmod = new MemberModifiers(); mmod.IsGhost = isAlreadyGhost; - while (la.kind == 8 || la.kind == 13) { + while (la.kind == 8 || la.kind == 16) { if (la.kind == 8) { Get(); mmod.IsGhost = true; @@ -386,15 +392,15 @@ bool IsAttribute() { mmod.IsStatic = true; } } - if (la.kind == 19) { + if (la.kind == 20) { FieldDecl(mmod, mm); } else if (la.kind == 44 || la.kind == 45) { FunctionDecl(mmod, out f); mm.Add(f); - } else if (la.kind == 24 || la.kind == 25) { + } else if (la.kind == 25 || la.kind == 26) { MethodDecl(mmod, allowConstructors, out m); mm.Add(m); - } else SynErr(115); + } else SynErr(116); } void Attribute(ref Attributes attrs) { @@ -413,35 +419,35 @@ bool IsAttribute() { } - void Ident(out IToken/*!*/ x) { - Contract.Ensures(Contract.ValueAtReturn(out x) != null); - Expect(1); - x = t; - } - - void Idents(List/*!*/ ids) { - IToken/*!*/ id; + void QualifiedName(out List ids) { + IToken id; ids = new List(); Ident(out id); - ids.Add(id.val); - while (la.kind == 20) { + ids.Add(id); + while (la.kind == 14) { Get(); Ident(out id); - ids.Add(id.val); + ids.Add(id); } } + void Ident(out IToken/*!*/ x) { + Contract.Ensures(Contract.ValueAtReturn(out x) != null); + Expect(1); + x = t; + } + void GenericParameters(List/*!*/ typeArgs) { Contract.Requires(cce.NonNullElements(typeArgs)); IToken/*!*/ id; - Expect(22); + Expect(23); NoUSIdent(out id); typeArgs.Add(new TypeParameter(id, id.val)); - while (la.kind == 20) { + while (la.kind == 21) { Get(); NoUSIdent(out id); typeArgs.Add(new TypeParameter(id, id.val)); } - Expect(23); + Expect(24); } void FieldDecl(MemberModifiers mmod, List/*!*/ mm) { @@ -449,8 +455,8 @@ bool IsAttribute() { Attributes attrs = null; IToken/*!*/ id; Type/*!*/ ty; - while (!(la.kind == 0 || la.kind == 19)) {SynErr(116); Get();} - Expect(19); + while (!(la.kind == 0 || la.kind == 20)) {SynErr(117); Get();} + Expect(20); if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); } while (la.kind == 6) { @@ -458,13 +464,13 @@ bool IsAttribute() { } IdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); - while (la.kind == 20) { + while (la.kind == 21) { Get(); IdentType(out id, out ty); mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(117); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(118); Get();} + Expect(12); } void FunctionDecl(MemberModifiers mmod, out Function/*!*/ f) { @@ -488,7 +494,7 @@ bool IsAttribute() { if (la.kind == 44) { Get(); - if (la.kind == 24) { + if (la.kind == 25) { Get(); isFunctionMethod = true; } @@ -498,22 +504,22 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 22 || la.kind == 33) { - if (la.kind == 22) { + if (la.kind == 23 || la.kind == 34) { + if (la.kind == 23) { GenericParameters(typeArgs); } Formals(true, isFunctionMethod, formals, out openParen); Expect(5); Type(out returnType); - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(118); + } else SynErr(119); } else if (la.kind == 45) { Get(); isPredicate = true; - if (la.kind == 24) { + if (la.kind == 25) { Get(); isFunctionMethod = true; } @@ -524,22 +530,22 @@ bool IsAttribute() { } NoUSIdent(out id); if (StartOf(3)) { - if (la.kind == 22) { + if (la.kind == 23) { GenericParameters(typeArgs); } - if (la.kind == 33) { + if (la.kind == 34) { Formals(true, isFunctionMethod, formals, out openParen); if (la.kind == 5) { Get(); SemErr(t, "predicates do not have an explicitly declared return type; it is always bool"); } } - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(119); - } else SynErr(120); + } else SynErr(120); + } else SynErr(121); while (StartOf(4)) { FunctionSpec(reqs, reads, ens, decreases); } @@ -578,10 +584,10 @@ bool IsAttribute() { IToken bodyStart = Token.NoToken; IToken bodyEnd = Token.NoToken; - while (!(la.kind == 0 || la.kind == 24 || la.kind == 25)) {SynErr(121); Get();} - if (la.kind == 24) { + while (!(la.kind == 0 || la.kind == 25 || la.kind == 26)) {SynErr(122); Get();} + if (la.kind == 25) { Get(); - } else if (la.kind == 25) { + } else if (la.kind == 26) { Get(); if (allowConstructor) { isConstructor = true; @@ -589,7 +595,7 @@ bool IsAttribute() { SemErr(t, "constructors are only allowed in classes"); } - } else SynErr(122); + } else SynErr(123); if (isConstructor) { if (mmod.IsGhost) { SemErr(t, "constructors cannot be declared 'ghost'"); @@ -603,20 +609,20 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 22 || la.kind == 33) { - if (la.kind == 22) { + if (la.kind == 23 || la.kind == 34) { + if (la.kind == 23) { GenericParameters(typeArgs); } Formals(true, !mmod.IsGhost, ins, out openParen); - if (la.kind == 26) { + if (la.kind == 27) { Get(); if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } Formals(false, !mmod.IsGhost, outs, out openParen); } - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); signatureOmitted = true; openParen = Token.NoToken; - } else SynErr(123); + } else SynErr(124); while (StartOf(5)) { MethodSpec(req, mod, ens, dec, ref decAttrs, ref modAttrs); } @@ -645,7 +651,7 @@ bool IsAttribute() { Attribute(ref attrs); } NoUSIdent(out id); - if (la.kind == 33) { + if (la.kind == 34) { FormalsOptionalIds(formals); } ctors.Add(new DatatypeCtor(id, id.val, formals, attrs)); @@ -653,17 +659,17 @@ bool IsAttribute() { void FormalsOptionalIds(List/*!*/ formals) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; string/*!*/ name; bool isGhost; - Expect(33); + Expect(34); if (StartOf(6)) { TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); - while (la.kind == 20) { + while (la.kind == 21) { Get(); TypeIdentOptional(out id, out name, out ty, out isGhost); formals.Add(new Formal(id, name, ty, true, isGhost)); } } - Expect(34); + Expect(35); } void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) { @@ -747,22 +753,22 @@ bool IsAttribute() { List/*!*/ gt; switch (la.kind) { - case 35: { + case 36: { Get(); tok = t; break; } - case 36: { + case 37: { Get(); tok = t; ty = new NatType(); break; } - case 37: { + case 38: { Get(); tok = t; ty = new IntType(); break; } - case 38: { + case 39: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -773,7 +779,7 @@ bool IsAttribute() { break; } - case 39: { + case 40: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -784,7 +790,7 @@ bool IsAttribute() { break; } - case 40: { + case 41: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -795,7 +801,7 @@ bool IsAttribute() { break; } - case 41: { + case 42: { Get(); tok = t; gt = new List(); GenericInstantiation(gt); @@ -806,28 +812,28 @@ bool IsAttribute() { break; } - case 1: case 3: case 42: { + case 1: case 3: case 43: { ReferenceType(out tok, out ty); break; } - default: SynErr(124); break; + default: SynErr(125); break; } } void Formals(bool incoming, bool allowGhostKeyword, List/*!*/ formals, out IToken openParen) { Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id; Type/*!*/ ty; bool isGhost; - Expect(33); + Expect(34); openParen = t; if (la.kind == 1 || la.kind == 8) { GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); - while (la.kind == 20) { + while (la.kind == 21) { Get(); GIdentType(allowGhostKeyword, out id, out ty, out isGhost); formals.Add(new Formal(id, id.val, ty, incoming, isGhost)); } } - Expect(34); + Expect(35); } void MethodSpec(List/*!*/ req, List/*!*/ mod, List/*!*/ ens, @@ -835,8 +841,8 @@ 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(7))) {SynErr(125); Get();} - if (la.kind == 28) { + while (!(StartOf(7))) {SynErr(126); Get();} + if (la.kind == 29) { Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -844,44 +850,44 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(8)) { FrameExpression(out fe); mod.Add(fe); - while (la.kind == 20) { + while (la.kind == 21) { Get(); FrameExpression(out fe); mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(126); Get();} - Expect(18); - } else if (la.kind == 29 || la.kind == 30 || la.kind == 31) { - if (la.kind == 29) { + while (!(la.kind == 0 || la.kind == 12)) {SynErr(127); Get();} + Expect(12); + } else if (la.kind == 30 || la.kind == 31 || la.kind == 32) { + if (la.kind == 30) { Get(); isFree = true; } - if (la.kind == 30) { + if (la.kind == 31) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(127); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(128); Get();} + Expect(12); req.Add(new MaybeFreeExpression(e, isFree)); - } else if (la.kind == 31) { + } else if (la.kind == 32) { Get(); while (IsAttribute()) { Attribute(ref ensAttrs); } Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(128); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(129); Get();} + Expect(12); ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); - } else SynErr(129); - } else if (la.kind == 32) { + } else SynErr(130); + } else if (la.kind == 33) { Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(130); Get();} - Expect(18); - } else SynErr(131); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(131); Get();} + Expect(12); + } else SynErr(132); } void BlockStmt(out BlockStmt/*!*/ block, out IToken bodyStart, out IToken bodyEnd) { @@ -922,7 +928,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo decreases.Add(e); } - while (la.kind == 20) { + while (la.kind == 21) { Get(); PossiblyWildExpression(out e); if (!allowWildcard && e is WildcardExpr) { @@ -936,15 +942,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void GenericInstantiation(List/*!*/ gt) { Contract.Requires(cce.NonNullElements(gt)); Type/*!*/ ty; - Expect(22); + Expect(23); Type(out ty); gt.Add(ty); - while (la.kind == 20) { + while (la.kind == 21) { Get(); Type(out ty); gt.Add(ty); } - Expect(23); + Expect(24); } void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) { @@ -953,7 +959,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken moduleName = null; List/*!*/ gt; - if (la.kind == 42) { + if (la.kind == 43) { Get(); tok = t; ty = new ObjectType(); } else if (la.kind == 3) { @@ -972,53 +978,53 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 1) { Ident(out tok); gt = new List(); - if (la.kind == 43) { + if (la.kind == 14) { moduleName = tok; Get(); Ident(out tok); } - if (la.kind == 22) { + if (la.kind == 23) { GenericInstantiation(gt); } ty = new UserDefinedType(tok, tok.val, gt, moduleName); - } else SynErr(132); + } else SynErr(133); } void FunctionSpec(List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List/*!*/ decreases) { Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases)); Expression/*!*/ e; FrameExpression/*!*/ fe; - if (la.kind == 30) { - while (!(la.kind == 0 || la.kind == 30)) {SynErr(133); Get();} + if (la.kind == 31) { + while (!(la.kind == 0 || la.kind == 31)) {SynErr(134); Get();} Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(134); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(135); Get();} + Expect(12); reqs.Add(e); } else if (la.kind == 46) { Get(); if (StartOf(10)) { PossiblyWildFrameExpression(out fe); reads.Add(fe); - while (la.kind == 20) { + while (la.kind == 21) { Get(); PossiblyWildFrameExpression(out fe); reads.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(135); Get();} - Expect(18); - } else if (la.kind == 31) { + while (!(la.kind == 0 || la.kind == 12)) {SynErr(136); Get();} + Expect(12); + } else if (la.kind == 32) { Get(); Expression(out e); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(136); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(137); Get();} + Expect(12); ens.Add(e); - } else if (la.kind == 32) { + } else if (la.kind == 33) { Get(); DecreasesList(decreases, false); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(137); Get();} - Expect(18); - } else SynErr(138); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(138); Get();} + Expect(12); + } else SynErr(139); } void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) { @@ -1037,7 +1043,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo fe = new FrameExpression(new WildcardExpr(t), null); } else if (StartOf(8)) { FrameExpression(out fe); - } else SynErr(139); + } else SynErr(140); } void PossiblyWildExpression(out Expression/*!*/ e) { @@ -1048,7 +1054,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new WildcardExpr(t); } else if (StartOf(8)) { Expression(out e); - } else SynErr(140); + } else SynErr(141); } void Stmt(List/*!*/ ss) { @@ -1065,7 +1071,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken bodyStart, bodyEnd; int breakCount; - while (!(StartOf(11))) {SynErr(141); Get();} + while (!(StartOf(11))) {SynErr(142); Get();} switch (la.kind) { case 6: { BlockStmt(out bs, out bodyStart, out bodyEnd); @@ -1084,11 +1090,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo PrintStmt(out s); break; } - case 1: case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: { + case 1: case 2: case 19: case 34: case 92: case 93: case 94: case 95: case 96: case 97: case 98: { UpdateStmt(out s); break; } - case 8: case 19: { + case 8: case 20: { VarDeclStatement(out s); break; } @@ -1123,14 +1129,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) { NoUSIdent(out id); label = id.val; - } else if (la.kind == 18 || la.kind == 50) { + } else if (la.kind == 12 || la.kind == 50) { while (la.kind == 50) { Get(); breakCount++; } - } else SynErr(142); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(143); Get();} - Expect(18); + } else SynErr(143); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(144); Get();} + Expect(12); s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); break; } @@ -1138,13 +1144,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo ReturnStmt(out s); break; } - case 27: { + case 28: { Get(); s = new SkeletonStatement(t); - Expect(18); + Expect(12); break; } - default: SynErr(144); break; + default: SynErr(145); break; } } @@ -1159,10 +1165,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } if (StartOf(8)) { Expression(out e); - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); - } else SynErr(145); - Expect(18); + } else SynErr(146); + Expect(12); if (e == null) { s = new SkeletonStatement(new AssertStmt(x, new LiteralExpr(x, true), attrs), true, false); } else { @@ -1176,7 +1182,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(54); x = t; Expression(out e); - Expect(18); + Expect(12); s = new AssumeStmt(x, e); } @@ -1188,12 +1194,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; AttributeArg(out arg); args.Add(arg); - while (la.kind == 20) { + while (la.kind == 21) { Get(); AttributeArg(out arg); args.Add(arg); } - Expect(18); + Expect(12); s = new PrintStmt(x, args); } @@ -1209,15 +1215,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Lhs(out e); x = e.tok; - if (la.kind == 6 || la.kind == 18) { + if (la.kind == 6 || la.kind == 12) { while (la.kind == 6) { Attribute(ref attrs); } - Expect(18); + Expect(12); rhss.Add(new ExprRhs(e, attrs)); - } else if (la.kind == 20 || la.kind == 52 || la.kind == 53) { + } else if (la.kind == 21 || la.kind == 52 || la.kind == 53) { lhss.Add(e); lhs0 = e; - while (la.kind == 20) { + while (la.kind == 21) { Get(); Lhs(out e); lhss.Add(e); @@ -1227,7 +1233,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; Rhs(out r, lhs0); rhss.Add(r); - while (la.kind == 20) { + while (la.kind == 21) { Get(); Rhs(out r, lhs0); rhss.Add(r); @@ -1240,12 +1246,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo suchThatAssume = t; } Expression(out suchThat); - } else SynErr(146); - Expect(18); + } else SynErr(147); + Expect(12); } else if (la.kind == 5) { Get(); SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); - } else SynErr(147); + } else SynErr(148); if (suchThat != null) { s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume); } else { @@ -1267,11 +1273,11 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); isGhost = true; x = t; } - Expect(19); + Expect(20); if (!isGhost) { x = t; } LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); - while (la.kind == 20) { + while (la.kind == 21) { Get(); LocalIdentTypeOptional(out d, isGhost); lhss.Add(d); @@ -1285,7 +1291,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0); rhss.Add(r); - while (la.kind == 20) { + while (la.kind == 21) { Get(); Rhs(out r, lhs0); rhss.Add(r); @@ -1300,7 +1306,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out suchThat); } } - Expect(18); + Expect(12); ConcreteUpdateStatement update; if (suchThat != null) { var ies = new List(); @@ -1334,8 +1340,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(59); x = t; - if (la.kind == 27 || la.kind == 33) { - if (la.kind == 33) { + if (la.kind == 28 || la.kind == 34) { + if (la.kind == 34) { Guard(out guard); } else { Get(); @@ -1350,7 +1356,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) { BlockStmt(out bs, out bodyStart, out bodyEnd); els = bs; - } else SynErr(148); + } else SynErr(149); } if (guardOmitted) { ifStmt = new SkeletonStatement(new IfStmt(x, guard, thn, els), true, false); @@ -1361,7 +1367,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 6) { AlternativeBlock(out alternatives); ifStmt = new AlternativeStmt(x, alternatives); - } else SynErr(149); + } else SynErr(150); } void WhileStmt(out Statement/*!*/ stmt) { @@ -1379,8 +1385,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(63); x = t; - if (la.kind == 27 || la.kind == 33) { - if (la.kind == 33) { + if (la.kind == 28 || la.kind == 34) { + if (la.kind == 34) { Guard(out guard); Contract.Assume(guard == null || cce.Owner.None(guard)); } else { @@ -1390,10 +1396,10 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs); if (la.kind == 6) { BlockStmt(out body, out bodyStart, out bodyEnd); - } else if (la.kind == 27) { + } else if (la.kind == 28) { Get(); bodyOmitted = true; - } else SynErr(150); + } else SynErr(151); if (guardOmitted || bodyOmitted) { if (decreases.Count != 0) { SemErr(decreases[0].tok, "'decreases' clauses are not allowed on refining loops"); @@ -1414,7 +1420,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo LoopSpec(out invariants, out decreases, out mod, ref decAttrs, ref modAttrs); AlternativeBlock(out alternatives); stmt = new AlternativeLoopStmt(x, invariants, new Specification(decreases, decAttrs), new Specification(mod, modAttrs), alternatives); - } else SynErr(151); + } else SynErr(152); } void MatchStmt(out Statement/*!*/ s) { @@ -1447,7 +1453,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(68); x = t; - Expect(33); + Expect(34); if (la.kind == 1) { List bvarsX; Attributes attrsX; Expression rangeX; QuantifierDomain(out bvarsX, out attrsX, out rangeX); @@ -1457,16 +1463,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (bvars == null) { bvars = new List(); } if (range == null) { range = new LiteralExpr(x, true); } - Expect(34); - while (la.kind == 29 || la.kind == 31) { + Expect(35); + while (la.kind == 30 || la.kind == 32) { isFree = false; - if (la.kind == 29) { + if (la.kind == 30) { Get(); isFree = true; } - Expect(31); + Expect(32); Expression(out e); - Expect(18); + Expect(12); ens.Add(new MaybeFreeExpression(e, isFree)); } BlockStmt(out block, out bodyStart, out bodyEnd); @@ -1483,13 +1489,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(13)) { Rhs(out r, null); rhss = new List(); rhss.Add(r); - while (la.kind == 20) { + while (la.kind == 21) { Get(); Rhs(out r, null); rhss.Add(r); } } - Expect(18); + Expect(12); s = new ReturnStmt(returnTok, rhss); } @@ -1506,7 +1512,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); newToken = t; TypeAndToken(out x, out ty); - if (la.kind == 33 || la.kind == 43 || la.kind == 56) { + if (la.kind == 14 || la.kind == 34 || la.kind == 56) { if (la.kind == 56) { Get(); ee = new List(); @@ -1514,15 +1520,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(57); UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true); - } else if (la.kind == 43) { + } else if (la.kind == 14) { Get(); Ident(out x); - Expect(33); + Expect(34); args = new List(); if (StartOf(8)) { Expressions(args); } - Expect(34); + Expect(35); initCall = new CallStmt(x, new List(), receiverForInitCall, x.val, args); } else { Get(); @@ -1540,7 +1546,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(8)) { Expressions(args); } - Expect(34); + Expect(35); if (x != null) { initCall = new CallStmt(x, new List(), receiverForInitCall, x.val, args); } @@ -1564,7 +1570,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) { Expression(out e); r = new ExprRhs(e); - } else SynErr(152); + } else SynErr(153); while (la.kind == 6) { Attribute(ref attrs); } @@ -1576,23 +1582,23 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 1) { DottedIdentifiersAndFunction(out e); - while (la.kind == 43 || la.kind == 56) { + while (la.kind == 14 || la.kind == 56) { Suffix(ref e); } } else if (StartOf(14)) { ConstAtomExpression(out e); Suffix(ref e); - while (la.kind == 43 || la.kind == 56) { + while (la.kind == 14 || la.kind == 56) { Suffix(ref e); } - } else SynErr(153); + } else SynErr(154); } void Expressions(List/*!*/ args) { Contract.Requires(cce.NonNullElements(args)); Expression/*!*/ e; Expression(out e); args.Add(e); - while (la.kind == 20) { + while (la.kind == 21) { Get(); Expression(out e); args.Add(e); @@ -1601,15 +1607,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void Guard(out Expression e) { Expression/*!*/ ee; e = null; - Expect(33); + Expect(34); if (la.kind == 47) { Get(); e = null; } else if (StartOf(8)) { Expression(out ee); e = ee; - } else SynErr(154); - Expect(34); + } else SynErr(155); + Expect(35); } void AlternativeBlock(out List alternatives) { @@ -1641,22 +1647,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo mod = null; while (StartOf(15)) { - if (la.kind == 29 || la.kind == 64) { + if (la.kind == 30 || la.kind == 64) { Invariant(out invariant); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(155); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(156); Get();} + Expect(12); invariants.Add(invariant); - } else if (la.kind == 32) { - while (!(la.kind == 0 || la.kind == 32)) {SynErr(156); Get();} + } else if (la.kind == 33) { + while (!(la.kind == 0 || la.kind == 33)) {SynErr(157); Get();} Get(); while (IsAttribute()) { Attribute(ref decAttrs); } DecreasesList(decreases, true); - while (!(la.kind == 0 || la.kind == 18)) {SynErr(157); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(158); Get();} + Expect(12); } else { - while (!(la.kind == 0 || la.kind == 28)) {SynErr(158); Get();} + while (!(la.kind == 0 || la.kind == 29)) {SynErr(159); Get();} Get(); while (IsAttribute()) { Attribute(ref modAttrs); @@ -1665,22 +1671,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(8)) { FrameExpression(out fe); mod.Add(fe); - while (la.kind == 20) { + while (la.kind == 21) { Get(); FrameExpression(out fe); mod.Add(fe); } } - while (!(la.kind == 0 || la.kind == 18)) {SynErr(159); Get();} - Expect(18); + while (!(la.kind == 0 || la.kind == 12)) {SynErr(160); Get();} + Expect(12); } } } void Invariant(out MaybeFreeExpression/*!*/ invariant) { bool isFree = false; Expression/*!*/ e; List ids = new List(); invariant = null; Attributes attrs = null; - while (!(la.kind == 0 || la.kind == 29 || la.kind == 64)) {SynErr(160); Get();} - if (la.kind == 29) { + while (!(la.kind == 0 || la.kind == 30 || la.kind == 64)) {SynErr(161); Get();} + if (la.kind == 30) { Get(); isFree = true; } @@ -1702,16 +1708,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(61); x = t; Ident(out id); - if (la.kind == 33) { + if (la.kind == 34) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); - while (la.kind == 20) { + while (la.kind == 21) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); } - Expect(34); + Expect(35); } Expect(62); while (StartOf(9)) { @@ -1728,7 +1734,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (StartOf(8)) { Expression(out e); arg = new Attributes.Argument(t, e); - } else SynErr(161); + } else SynErr(162); } void QuantifierDomain(out List bvars, out Attributes attrs, out Expression range) { @@ -1739,7 +1745,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); bvars.Add(bv); - while (la.kind == 20) { + while (la.kind == 21) { Get(); IdentTypeOptional(out bv); bvars.Add(bv); @@ -1747,7 +1753,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo while (la.kind == 6) { Attribute(ref attrs); } - if (la.kind == 17) { + if (la.kind == 19) { Get(); Expression(out range); } @@ -1780,7 +1786,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 70) { Get(); - } else SynErr(162); + } else SynErr(163); } void LogicalExpression(out Expression/*!*/ e0) { @@ -1818,7 +1824,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 72) { Get(); - } else SynErr(163); + } else SynErr(164); } void RelationalExpression(out Expression/*!*/ e) { @@ -1916,7 +1922,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 74) { Get(); - } else SynErr(164); + } else SynErr(165); } void OrOp() { @@ -1924,7 +1930,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 76) { Get(); - } else SynErr(165); + } else SynErr(166); } void Term(out Expression/*!*/ e0) { @@ -1948,12 +1954,12 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Eq; break; } - case 22: { + case 23: { Get(); x = t; op = BinaryExpr.Opcode.Lt; break; } - case 23: { + case 24: { Get(); x = t; op = BinaryExpr.Opcode.Gt; break; @@ -2016,7 +2022,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Ge; break; } - default: SynErr(166); break; + default: SynErr(167); break; } } @@ -2038,7 +2044,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 88) { Get(); x = t; op = BinaryExpr.Opcode.Sub; - } else SynErr(167); + } else SynErr(168); } void UnaryExpression(out Expression/*!*/ e) { @@ -2058,13 +2064,13 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo e = new UnaryExpr(x, UnaryExpr.Opcode.Not, e); break; } - case 19: case 38: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: { + case 20: case 39: case 54: case 59: case 65: case 66: case 101: case 102: case 103: case 104: { EndlessExpression(out e); break; } case 1: { DottedIdentifiersAndFunction(out e); - while (la.kind == 43 || la.kind == 56) { + while (la.kind == 14 || la.kind == 56) { Suffix(ref e); } break; @@ -2073,22 +2079,22 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo DisplayExpr(out e); break; } - case 39: { + case 40: { MultiSetExpr(out e); break; } - case 41: { + case 42: { MapExpr(out e); break; } - case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: { + case 2: case 19: case 34: case 92: case 93: case 94: case 95: case 96: case 97: case 98: { ConstAtomExpression(out e); - while (la.kind == 43 || la.kind == 56) { + while (la.kind == 14 || la.kind == 56) { Suffix(ref e); } break; } - default: SynErr(168); break; + default: SynErr(169); break; } } @@ -2103,7 +2109,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 90) { Get(); x = t; op = BinaryExpr.Opcode.Mod; - } else SynErr(169); + } else SynErr(170); } void NegOp() { @@ -2111,7 +2117,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 91) { Get(); - } else SynErr(170); + } else SynErr(171); } void EndlessExpression(out Expression e) { @@ -2141,7 +2147,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo QuantifierGuts(out e); break; } - case 38: { + case 39: { ComprehensionExpr(out e); break; } @@ -2149,7 +2155,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); x = t; Expression(out e0); - Expect(18); + Expect(12); Expression(out e1); e = new AssertExpr(x, e0, e1); break; @@ -2158,19 +2164,19 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); x = t; Expression(out e0); - Expect(18); + Expect(12); Expression(out e1); e = new AssumeExpr(x, e0, e1); break; } - case 19: { + case 20: { Get(); x = t; letVars = new List(); letRHSs = new List(); IdentTypeOptional(out d); letVars.Add(d); - while (la.kind == 20) { + while (la.kind == 21) { Get(); IdentTypeOptional(out d); letVars.Add(d); @@ -2178,17 +2184,17 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(52); Expression(out e); letRHSs.Add(e); - while (la.kind == 20) { + while (la.kind == 21) { Get(); Expression(out e); letRHSs.Add(e); } - Expect(18); + Expect(12); Expression(out e); e = new LetExpr(x, letVars, letRHSs, e); break; } - default: SynErr(171); break; + default: SynErr(172); break; } } @@ -2199,18 +2205,18 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id); idents.Add(id); - while (la.kind == 43) { + while (la.kind == 14) { Get(); Ident(out id); idents.Add(id); } - if (la.kind == 33) { + if (la.kind == 34) { Get(); openParen = t; args = new List(); if (StartOf(8)) { Expressions(args); } - Expect(34); + Expect(35); } e = new IdentifierSequence(idents, openParen, args); } @@ -2221,16 +2227,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List multipleIndices = null; bool func = false; - if (la.kind == 43) { + if (la.kind == 14) { Get(); Ident(out id); - if (la.kind == 33) { + if (la.kind == 34) { Get(); IToken openParen = t; args = new List(); func = true; if (StartOf(8)) { Expressions(args); } - Expect(34); + Expect(35); e = new FunctionCallExpr(id, id.val, e, openParen, args); } if (!func) { e = new ExprDotName(id, e, id.val); } @@ -2251,8 +2257,8 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); Expression(out ee); e1 = ee; - } else if (la.kind == 20 || la.kind == 57) { - while (la.kind == 20) { + } else if (la.kind == 21 || la.kind == 57) { + while (la.kind == 21) { Get(); Expression(out ee); if (multipleIndices == null) { @@ -2262,7 +2268,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo multipleIndices.Add(ee); } - } else SynErr(172); + } else SynErr(173); } else if (la.kind == 100) { Get(); anyDots = true; @@ -2270,7 +2276,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression(out ee); e1 = ee; } - } else SynErr(173); + } else SynErr(174); if (multipleIndices != null) { e = new MultiSelectExpr(x, e, multipleIndices); // make sure an array class with this dimensionality exists @@ -2294,7 +2300,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } Expect(57); - } else SynErr(174); + } else SynErr(175); } void DisplayExpr(out Expression e) { @@ -2318,7 +2324,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new SeqDisplayExpr(x, elements); Expect(57); - } else SynErr(175); + } else SynErr(176); } void MultiSetExpr(out Expression e) { @@ -2326,7 +2332,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IToken/*!*/ x = null; List/*!*/ elements; e = dummyExpr; - Expect(39); + Expect(40); x = t; if (la.kind == 6) { Get(); @@ -2336,15 +2342,15 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } e = new MultiSetDisplayExpr(x, elements); Expect(7); - } else if (la.kind == 33) { + } else if (la.kind == 34) { Get(); x = t; elements = new List(); Expression(out e); e = new MultiSetFormingExpr(x, e); - Expect(34); + Expect(35); } else if (StartOf(18)) { SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); - } else SynErr(176); + } else SynErr(177); } void MapExpr(out Expression e) { @@ -2353,7 +2359,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo List/*!*/ elements; e = dummyExpr; - Expect(41); + Expect(42); x = t; if (la.kind == 56) { Get(); @@ -2371,14 +2377,14 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo IdentTypeOptional(out bv); bvars.Add(bv); - Expect(17); + Expect(19); Expression(out range); QSep(); Expression(out body); e = new MapComprehension(x, bvars, range, body); } else if (StartOf(18)) { SemErr("map must be followed by literal in brackets or comprehension."); - } else SynErr(177); + } else SynErr(178); } void ConstAtomExpression(out Expression/*!*/ e) { @@ -2415,47 +2421,47 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 96: { Get(); x = t; - Expect(33); - Expression(out e); Expect(34); + Expression(out e); + Expect(35); e = new FreshExpr(x, e); break; } case 97: { Get(); x = t; - Expect(33); - Expression(out e); Expect(34); + Expression(out e); + Expect(35); e = new AllocatedExpr(x, e); break; } case 98: { Get(); x = t; - Expect(33); - Expression(out e); Expect(34); + Expression(out e); + Expect(35); e = new OldExpr(x, e); break; } - case 17: { + case 19: { Get(); x = t; Expression(out e); e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); - Expect(17); + Expect(19); break; } - case 33: { + case 34: { Get(); x = t; Expression(out e); e = new ParensExpression(x, e); - Expect(34); + Expect(35); break; } - default: SynErr(178); break; + default: SynErr(179); break; } } @@ -2477,7 +2483,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(52); Expression(out r); elements.Add(new ExpressionPair(d,r)); - while (la.kind == 20) { + while (la.kind == 21) { Get(); Expression(out d); Expect(52); @@ -2491,7 +2497,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 106) { Get(); - } else SynErr(179); + } else SynErr(180); } void MatchExpression(out Expression/*!*/ e) { @@ -2522,7 +2528,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else if (la.kind == 103 || la.kind == 104) { Exists(); x = t; - } else SynErr(180); + } else SynErr(181); QuantifierDomain(out bvars, out attrs, out range); QSep(); Expression(out body); @@ -2542,16 +2548,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression/*!*/ range; Expression body = null; - Expect(38); + Expect(39); x = t; IdentTypeOptional(out bv); bvars.Add(bv); - while (la.kind == 20) { + while (la.kind == 21) { Get(); IdentTypeOptional(out bv); bvars.Add(bv); } - Expect(17); + Expect(19); Expression(out range); if (la.kind == 105 || la.kind == 106) { QSep(); @@ -2571,16 +2577,16 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(61); x = t; Ident(out id); - if (la.kind == 33) { + if (la.kind == 34) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); - while (la.kind == 20) { + while (la.kind == 21) { Get(); IdentTypeOptional(out bv); arguments.Add(bv); } - Expect(34); + Expect(35); } Expect(62); Expression(out body); @@ -2592,7 +2598,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 102) { Get(); - } else SynErr(181); + } else SynErr(182); } void Exists() { @@ -2600,7 +2606,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Get(); } else if (la.kind == 104) { Get(); - } else SynErr(182); + } else SynErr(183); } void AttributeBody(ref Attributes attrs) { @@ -2614,7 +2620,7 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (StartOf(19)) { AttributeArg(out aArg); aArgs.Add(aArg); - while (la.kind == 20) { + while (la.kind == 21) { Get(); AttributeArg(out aArg); aArgs.Add(aArg); @@ -2636,26 +2642,26 @@ List/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } static readonly bool[,]/*!*/ set = { - {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}, - {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, - {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}, - {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}, - {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, + {T,T,T,x, x,x,T,x, T,x,x,x, T,x,x,T, x,T,T,T, T,x,x,x, x,T,T,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, + {x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, + {x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, T,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, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, + {T,x,x,x, x,x,T,T, T,T,x,x, x,x,x,T, T,T,T,x, T,x,T,T, x,T,T,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, 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,T,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,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,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, + {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,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,T,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}, + {x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, + {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}, + {T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,T,x, x,x,x,T, x,x,x,T, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, + {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, + {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,T, x,x,x,x, x,x,T,T, T,x,T,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}, + {x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x}, + {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, - {x,x,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,T,T,x, T,x,T,T, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x}, - {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x} + {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,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x}, + {x,x,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,T,x,T, T,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, T,x,x,x, x,T,x,x, T,T,T,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,T, T,x,x,x, x,T,T,x, x}, + {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, T,x,x,T, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x} }; } // end Parser @@ -2691,39 +2697,39 @@ public class Errors { case 8: s = "\"ghost\" expected"; break; case 9: s = "\"module\" expected"; break; case 10: s = "\"refines\" expected"; break; - case 11: s = "\"imports\" expected"; break; - case 12: s = "\"class\" expected"; break; - case 13: s = "\"static\" expected"; break; - case 14: s = "\"datatype\" expected"; break; - case 15: s = "\"codatatype\" expected"; break; - case 16: s = "\"=\" expected"; break; - case 17: s = "\"|\" expected"; break; - case 18: s = "\";\" expected"; break; - case 19: s = "\"var\" expected"; break; - case 20: s = "\",\" expected"; break; - case 21: s = "\"type\" expected"; break; - case 22: s = "\"<\" expected"; break; - case 23: s = "\">\" expected"; break; - case 24: s = "\"method\" expected"; break; - case 25: s = "\"constructor\" expected"; break; - case 26: s = "\"returns\" expected"; break; - case 27: s = "\"...\" expected"; break; - case 28: s = "\"modifies\" expected"; break; - case 29: s = "\"free\" expected"; break; - case 30: s = "\"requires\" expected"; break; - case 31: s = "\"ensures\" expected"; break; - case 32: s = "\"decreases\" expected"; break; - case 33: s = "\"(\" expected"; break; - case 34: s = "\")\" expected"; break; - case 35: s = "\"bool\" expected"; break; - case 36: s = "\"nat\" expected"; break; - case 37: s = "\"int\" expected"; break; - case 38: s = "\"set\" expected"; break; - case 39: s = "\"multiset\" expected"; break; - case 40: s = "\"seq\" expected"; break; - case 41: s = "\"map\" expected"; break; - case 42: s = "\"object\" expected"; break; - case 43: s = "\".\" expected"; break; + case 11: s = "\"=\" expected"; break; + case 12: s = "\";\" expected"; break; + case 13: s = "\"as\" expected"; break; + case 14: s = "\".\" expected"; break; + case 15: s = "\"class\" expected"; break; + case 16: s = "\"static\" expected"; break; + case 17: s = "\"datatype\" expected"; break; + case 18: s = "\"codatatype\" expected"; break; + case 19: s = "\"|\" expected"; break; + case 20: s = "\"var\" expected"; break; + case 21: s = "\",\" expected"; break; + case 22: s = "\"type\" expected"; break; + case 23: s = "\"<\" expected"; break; + case 24: s = "\">\" expected"; break; + case 25: s = "\"method\" expected"; break; + case 26: s = "\"constructor\" expected"; break; + case 27: s = "\"returns\" expected"; break; + case 28: s = "\"...\" expected"; break; + case 29: s = "\"modifies\" expected"; break; + case 30: s = "\"free\" expected"; break; + case 31: s = "\"requires\" expected"; break; + case 32: s = "\"ensures\" expected"; break; + case 33: s = "\"decreases\" expected"; break; + case 34: s = "\"(\" expected"; break; + case 35: s = "\")\" expected"; break; + case 36: s = "\"bool\" expected"; break; + case 37: s = "\"nat\" expected"; break; + case 38: s = "\"int\" expected"; break; + case 39: s = "\"set\" expected"; break; + case 40: s = "\"multiset\" expected"; break; + case 41: s = "\"seq\" expected"; break; + case 42: s = "\"map\" expected"; break; + case 43: s = "\"object\" expected"; break; case 44: s = "\"function\" expected"; break; case 45: s = "\"predicate\" expected"; break; case 46: s = "\"reads\" expected"; break; @@ -2790,79 +2796,80 @@ public class Errors { case 107: s = "??? expected"; break; case 108: s = "invalid Dafny"; break; case 109: s = "invalid SubModuleDecl"; break; - case 110: s = "this symbol not expected in ClassDecl"; break; - case 111: s = "this symbol not expected in DatatypeDecl"; break; - case 112: s = "invalid DatatypeDecl"; break; - case 113: s = "this symbol not expected in DatatypeDecl"; break; - case 114: s = "this symbol not expected in ArbitraryTypeDecl"; break; - case 115: s = "invalid ClassMemberDecl"; break; - case 116: s = "this symbol not expected in FieldDecl"; break; + case 110: s = "invalid SubModuleDecl"; break; + case 111: s = "this symbol not expected in ClassDecl"; break; + case 112: s = "this symbol not expected in DatatypeDecl"; break; + case 113: s = "invalid DatatypeDecl"; break; + case 114: s = "this symbol not expected in DatatypeDecl"; break; + case 115: s = "this symbol not expected in ArbitraryTypeDecl"; break; + case 116: s = "invalid ClassMemberDecl"; break; case 117: s = "this symbol not expected in FieldDecl"; break; - case 118: s = "invalid FunctionDecl"; break; + case 118: s = "this symbol not expected in FieldDecl"; break; case 119: s = "invalid FunctionDecl"; break; case 120: s = "invalid FunctionDecl"; break; - case 121: s = "this symbol not expected in MethodDecl"; break; - case 122: s = "invalid MethodDecl"; break; + case 121: s = "invalid FunctionDecl"; break; + case 122: s = "this symbol not expected in MethodDecl"; break; case 123: s = "invalid MethodDecl"; break; - case 124: s = "invalid TypeAndToken"; break; - case 125: s = "this symbol not expected in MethodSpec"; break; + case 124: s = "invalid MethodDecl"; break; + case 125: s = "invalid TypeAndToken"; break; case 126: s = "this symbol not expected in MethodSpec"; break; case 127: s = "this symbol not expected in MethodSpec"; break; case 128: s = "this symbol not expected in MethodSpec"; break; - case 129: s = "invalid MethodSpec"; break; - case 130: s = "this symbol not expected in MethodSpec"; break; - case 131: s = "invalid MethodSpec"; break; - case 132: s = "invalid ReferenceType"; break; - case 133: s = "this symbol not expected in FunctionSpec"; break; + case 129: s = "this symbol not expected in MethodSpec"; break; + case 130: s = "invalid MethodSpec"; break; + case 131: s = "this symbol not expected in MethodSpec"; break; + case 132: s = "invalid MethodSpec"; break; + case 133: s = "invalid ReferenceType"; break; case 134: s = "this symbol not expected in FunctionSpec"; break; case 135: s = "this symbol not expected in FunctionSpec"; break; case 136: s = "this symbol not expected in FunctionSpec"; break; case 137: s = "this symbol not expected in FunctionSpec"; break; - case 138: s = "invalid FunctionSpec"; break; - case 139: s = "invalid PossiblyWildFrameExpression"; break; - case 140: s = "invalid PossiblyWildExpression"; break; - case 141: s = "this symbol not expected in OneStmt"; break; - case 142: s = "invalid OneStmt"; break; - case 143: s = "this symbol not expected in OneStmt"; break; - case 144: s = "invalid OneStmt"; break; - case 145: s = "invalid AssertStmt"; break; - case 146: s = "invalid UpdateStmt"; break; + case 138: s = "this symbol not expected in FunctionSpec"; break; + case 139: s = "invalid FunctionSpec"; break; + case 140: s = "invalid PossiblyWildFrameExpression"; break; + case 141: s = "invalid PossiblyWildExpression"; break; + case 142: s = "this symbol not expected in OneStmt"; break; + case 143: s = "invalid OneStmt"; break; + case 144: s = "this symbol not expected in OneStmt"; break; + case 145: s = "invalid OneStmt"; break; + case 146: s = "invalid AssertStmt"; break; case 147: s = "invalid UpdateStmt"; break; - case 148: s = "invalid IfStmt"; break; + case 148: s = "invalid UpdateStmt"; break; case 149: s = "invalid IfStmt"; break; - case 150: s = "invalid WhileStmt"; break; + case 150: s = "invalid IfStmt"; break; case 151: s = "invalid WhileStmt"; break; - case 152: s = "invalid Rhs"; break; - case 153: s = "invalid Lhs"; break; - case 154: s = "invalid Guard"; break; - case 155: s = "this symbol not expected in LoopSpec"; break; + case 152: s = "invalid WhileStmt"; break; + case 153: s = "invalid Rhs"; break; + case 154: s = "invalid Lhs"; break; + case 155: s = "invalid Guard"; break; case 156: s = "this symbol not expected in LoopSpec"; break; case 157: s = "this symbol not expected in LoopSpec"; break; case 158: s = "this symbol not expected in LoopSpec"; break; case 159: s = "this symbol not expected in LoopSpec"; break; - case 160: s = "this symbol not expected in Invariant"; break; - case 161: s = "invalid AttributeArg"; break; - case 162: s = "invalid EquivOp"; break; - case 163: s = "invalid ImpliesOp"; break; - case 164: s = "invalid AndOp"; break; - case 165: s = "invalid OrOp"; break; - case 166: s = "invalid RelOp"; break; - case 167: s = "invalid AddOp"; break; - case 168: s = "invalid UnaryExpression"; break; - case 169: s = "invalid MulOp"; break; - case 170: s = "invalid NegOp"; break; - case 171: s = "invalid EndlessExpression"; break; - case 172: s = "invalid Suffix"; break; + case 160: s = "this symbol not expected in LoopSpec"; break; + case 161: s = "this symbol not expected in Invariant"; break; + case 162: s = "invalid AttributeArg"; break; + case 163: s = "invalid EquivOp"; break; + case 164: s = "invalid ImpliesOp"; break; + case 165: s = "invalid AndOp"; break; + case 166: s = "invalid OrOp"; break; + case 167: s = "invalid RelOp"; break; + case 168: s = "invalid AddOp"; break; + case 169: s = "invalid UnaryExpression"; break; + case 170: s = "invalid MulOp"; break; + case 171: s = "invalid NegOp"; break; + case 172: s = "invalid EndlessExpression"; break; case 173: s = "invalid Suffix"; break; case 174: s = "invalid Suffix"; break; - case 175: s = "invalid DisplayExpr"; break; - case 176: s = "invalid MultiSetExpr"; break; - case 177: s = "invalid MapExpr"; break; - case 178: s = "invalid ConstAtomExpression"; break; - case 179: s = "invalid QSep"; break; - case 180: s = "invalid QuantifierGuts"; break; - case 181: s = "invalid Forall"; break; - case 182: s = "invalid Exists"; break; + case 175: s = "invalid Suffix"; break; + case 176: s = "invalid DisplayExpr"; break; + case 177: s = "invalid MultiSetExpr"; break; + case 178: s = "invalid MapExpr"; break; + case 179: s = "invalid ConstAtomExpression"; break; + case 180: s = "invalid QSep"; break; + case 181: s = "invalid QuantifierGuts"; break; + case 182: s = "invalid Forall"; break; + case 183: s = "invalid Exists"; break; default: s = "error " + n; break; } diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index fb46ba4b..36883203 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -32,7 +32,7 @@ namespace Microsoft.Dafny { wr.WriteLine("// " + Bpl.CommandLineOptions.Clo.Environment); } wr.WriteLine("// {0}", prog.Name); - foreach (ModuleDecl module in prog.Modules) { + foreach (ModuleDefinition module in prog.Modules) { wr.WriteLine(); if (module.IsDefaultModule) { PrintTopLevelDecls(module.TopLevelDecls, 0); @@ -43,13 +43,6 @@ namespace Microsoft.Dafny { if (module.RefinementBaseName != null) { wr.Write("refines {0} ", module.RefinementBaseName); } - if (module.ImportNames.Count != 0) { - string sep = "imports "; - foreach (string imp in module.ImportNames) { - wr.Write("{0}{1}", sep, imp); - sep = ", "; - } - } if (module.TopLevelDecls.Count == 0) { wr.WriteLine(" { }"); } else { @@ -144,14 +137,7 @@ namespace Microsoft.Dafny { wr.Write(" {0}", name); if (typeArgs.Count != 0) { - wr.Write("<"); - string sep = ""; - foreach (TypeParameter tp in typeArgs) { - Contract.Assert(tp != null); - wr.Write("{0}{1}", sep, tp.Name); - sep = ", "; - } - wr.Write(">"); + wr.Write("<" + Util.Comma(", ", typeArgs, tp => tp.Name) + ">"); } } diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 51b22443..180aecbd 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -21,8 +21,8 @@ using IToken = Microsoft.Boogie.IToken; namespace Microsoft.Dafny { public class RefinementToken : TokenWrapper { - public readonly ModuleDecl InheritingModule; - public RefinementToken(IToken tok, ModuleDecl m) + public readonly ModuleDefinition InheritingModule; + public RefinementToken(IToken tok, ModuleDefinition m) : base(tok) { Contract.Requires(tok != null); @@ -30,7 +30,7 @@ namespace Microsoft.Dafny { this.InheritingModule = m; } - public static bool IsInherited(IToken tok, ModuleDecl m) { + public static bool IsInherited(IToken tok, ModuleDefinition m) { while (tok is NestedToken) { var n = (NestedToken)tok; // check Outer @@ -58,29 +58,16 @@ namespace Microsoft.Dafny { this.reporter = reporter; } - private ModuleDecl moduleUnderConstruction; // non-null for the duration of Construct calls + private ModuleDefinition moduleUnderConstruction; // non-null for the duration of Construct calls - public void Construct(ModuleDecl m) { + public void Construct(ModuleDefinition m) { Contract.Requires(m != null); Contract.Requires(m.RefinementBase != null); Contract.Assert(moduleUnderConstruction == null); moduleUnderConstruction = m; var prev = m.RefinementBase; - - // Include the imports of the base. Note, prev is itself NOT added as an import - // of m; instead, the contents from prev is merged directly into m. - // (Here, we change the import declarations. But edges for these imports will - // not be added to the importGraph of the calling resolver. However, the refines - // clause gave rise to an edge in the importGraph, so the transitive import edges - // are represented in the importGraph.) - foreach (var im in prev.Imports) { - if (!m.ImportNames.Contains(im.Name)) { - m.ImportNames.Add(im.Name); - m.Imports.Add(im); - } - } - + // Create a simple name-to-decl dictionary. Ignore any duplicates at this time. var declaredNames = new Dictionary(); for (int i = 0; i < m.TopLevelDecls.Count; i++) { @@ -91,15 +78,26 @@ namespace Microsoft.Dafny { } // Merge the declarations of prev into the declarations of m - foreach (var d in prev.TopLevelDecls) { int index; if (!declaredNames.TryGetValue(d.Name, out index)) { m.TopLevelDecls.Add(CloneDeclaration(d, m)); } else { var nw = m.TopLevelDecls[index]; - if (d is ArbitraryTypeDecl) { + if (d is ModuleDecl) { + if (!(nw is ModuleDecl)) { + reporter.Error(nw, "a module ({0}) must refine another module", nw.Name); + } + if (d is AliasModuleDecl || d is LiteralModuleDecl) { + reporter.Error(nw, "a module ({0}) can only refine abstract modules", nw.Name); + } + } else if (d is ArbitraryTypeDecl) { // this is allowed to be refined by any type declaration, so just keep the new one + // of course, the new thing has to be a type. Everything is a type except for a module + // declaration + if (nw is ModuleDecl) { + reporter.Error(nw, "a module ({0}) must refine another module", nw.Name); + } } else if (nw is ArbitraryTypeDecl) { reporter.Error(nw, "an arbitrary type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name); } else if (nw is DatatypeDecl) { @@ -129,7 +127,8 @@ namespace Microsoft.Dafny { // -------------------------------------------------- Cloning --------------------------------------------------------------- - TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDecl m) { + // Clone a toplevel, specifying that its parent module should be m (i.e. it will be added to m.TopLevelDecls). + TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) { Contract.Requires(d != null); Contract.Requires(m != null); @@ -154,6 +153,22 @@ namespace Microsoft.Dafny { var mm = dd.Members.ConvertAll(CloneMember); var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null); return cl; + } else if (d is ModuleDecl) { + if (d is LiteralModuleDecl) { + return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef,m); + } else if (d is AliasModuleDecl) { + var a = (AliasModuleDecl)d; + var alias = new AliasModuleDecl(a.Path, a.tok, m); + alias.ModuleReference = a.ModuleReference; + alias.Signature = a.Signature; + return alias; + } else if (d is AbstractModuleDecl) { + var a = (AbstractModuleDecl)d; + return new AbstractModuleDecl(a.Path, a.tok, m); + } else { + Contract.Assert(false); // unexpected declaration + return null; // to please compiler + } } else { Contract.Assert(false); // unexpected declaration return null; // to please compiler @@ -1120,7 +1135,7 @@ namespace Microsoft.Dafny { // ---------------------- additional methods ----------------------------------------------------------------------------- - public static bool ContainsChange(Expression expr, ModuleDecl m) { + public static bool ContainsChange(Expression expr, ModuleDefinition m) { Contract.Requires(expr != null); Contract.Requires(m != null); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 22a0a299..63f2f9e9 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -65,13 +65,13 @@ namespace Microsoft.Dafny { //Dictionary/*!*/ classes; // can map to AmbiguousTopLevelDecl //Dictionary importedNames; // the imported modules, as a map. - ModuleNameInformation moduleInfo = null; + ModuleSignature moduleInfo = null; class AmbiguousTopLevelDecl : TopLevelDecl // only used with "classes" { readonly TopLevelDecl A; readonly TopLevelDecl B; - public AmbiguousTopLevelDecl(ModuleDecl m, TopLevelDecl a, TopLevelDecl b) + public AmbiguousTopLevelDecl(ModuleDefinition m, TopLevelDecl a, TopLevelDecl b) : base(a.tok, a.Name + "/" + b.Name, m, new List(), null) { A = a; B = b; @@ -96,8 +96,7 @@ namespace Microsoft.Dafny { readonly Dictionary/*!*/>/*!*/ classMembers = new Dictionary/*!*/>(); readonly Dictionary/*!*/>/*!*/ datatypeMembers = new Dictionary/*!*/>(); readonly Dictionary/*!*/>/*!*/ datatypeCtors = new Dictionary/*!*/>(); - readonly Graph/*!*/ importGraph = new Graph(); - private ModuleNameInformation[] moduleNameInfo; + readonly Graph/*!*/ dependencies = new Graph(); public Resolver(Program prog) { Contract.Requires(prog != null); builtIns = prog.BuiltIns; @@ -106,66 +105,109 @@ namespace Microsoft.Dafny { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(builtIns != null); - Contract.Invariant(cce.NonNullElements(importGraph)); + Contract.Invariant(cce.NonNullElements(dependencies)); Contract.Invariant(cce.NonNullDictionaryAndValues(classMembers) && Contract.ForAll(classMembers.Values, v => cce.NonNullDictionaryAndValues(v))); Contract.Invariant(cce.NonNullDictionaryAndValues(datatypeCtors) && Contract.ForAll(datatypeCtors.Values, v => cce.NonNullDictionaryAndValues(v))); } public void ResolveProgram(Program prog) { Contract.Requires(prog != null); - - BindModuleNames(prog.DefaultModule, new ModuleBindings(null), prog.Modules, importGraph); - + var bindings = new ModuleBindings(null); + var b = BindModuleNames(prog.DefaultModuleDef, bindings); + bindings.BindName("_module", prog.DefaultModule , b); + if (ErrorCount > 0) { return; } // if there were errors, then the implict ModuleBindings data structure invariant + // is violated, so Processing dependencies will not succeed. + ProcessDependencies(prog.DefaultModule, b, dependencies); // check for cycles in the import graph - List cycle = importGraph.TryFindCycle(); + List cycle = dependencies.TryFindCycle(); if (cycle != null) { - string cy = ""; - string sep = ""; - foreach (ModuleDecl m in cycle) { - cy = m.Name + sep + cy; - sep = " -> "; - } - Error(cycle[0], "import graph contains a cycle (note: parent modules implicitly depend on submodules): {0}", cy); - return; // give up on trying to resolve anything else + var cy = Util.Comma(" -> ", cycle, m => m.Name); + Error(cycle[0], "module definition contains a cycle (note: parent modules implicitly depend on submodules): {0}", cy); } + if (ErrorCount > 0) { return; } // give up on trying to resolve anything else // fill in module heights - List mm = importGraph.TopologicallySortedComponents(); - Contract.Assert(mm.Count == prog.Modules.Count); // follows from the fact that there are no cycles + List sortedDecls = dependencies.TopologicallySortedComponents(); int h = 0; - foreach (ModuleDecl m in mm) { + foreach (ModuleDecl m in sortedDecls) { m.Height = h; + if (m is LiteralModuleDecl) { + var mdef = ((LiteralModuleDecl)m).ModuleDef; + mdef.Height = h; + prog.Modules.Add(mdef); + } h++; } + var mm = prog.Modules; // register top-level declarations - Rewriter rewriter = new AutoContractsRewriter(); - var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule.TopLevelDecls); - moduleNameInfo = new ModuleNameInformation[h]; - foreach (var m in mm) { - rewriter.PreResolve(m); - if (m.RefinementBase != null) { - var transformer = new RefinementTransformer(this); - transformer.Construct(m); - } - moduleNameInfo[m.Height] = RegisterTopLevelDecls(m.TopLevelDecls); - // set up environment - moduleInfo = ModuleNameInformation.Merge(m, systemNameInfo, moduleNameInfo); - /* - classes = info.Classes; - importedNames = info.ImportedNames; - allDatatypeCtors = info.Ctors; - */ - // resolve - var datatypeDependencies = new Graph(); - ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies); - ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies); - // tear down - // give rewriter a chance to do processing - rewriter.PostResolve(m); + + //Rewriter rewriter = new AutoContractsRewriter(); + var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule); + foreach (var decl in sortedDecls) { + if (decl is LiteralModuleDecl) { + // The declaration is a literal module, so it has members and such that we need + // to resolve. First we do refinement transformation. Then we construct the signature + // of the module. This is the public, externally visible signature. Then we add in + // everything that the system defines, as well as any "import" (i.e. "opened" modules) + // directives (currently not supported, but this is where we would do it.) This signature, + // which is only used while resolving the members of the module is stored in the (basically) + // global variable moduleInfo. Then the signatures of the module members are resolved, followed + // by the bodies. + var literalDecl = (LiteralModuleDecl)decl; + var m = (literalDecl).ModuleDef; + //rewriter.PreResolve(m); + if (m.RefinementBaseRoot != null) { + ModuleSignature sig; + if (ResolvePath(m.RefinementBaseRoot, m.RefinementBaseName, out sig)) { + if (sig.ModuleDef != null) { + m.RefinementBase = sig.ModuleDef; + var transformer = new RefinementTransformer(this); + transformer.Construct(m); + } else { + Error(m.RefinementBaseName[0], "module ({0}) named as refinement base is not a literal module or reference to a literal module", Util.Comma(".", m.RefinementBaseName, x => x.val)); + } + } else { + Error(m.RefinementBaseName[0], "module ({0}) named as refinement base does not exist", Util.Comma(".", m.RefinementBaseName, x => x.val)); + } + } + literalDecl.Signature = RegisterTopLevelDecls(m); + // set up environment + moduleInfo = MergeSignature(literalDecl.Signature, systemNameInfo); + // resolve + var datatypeDependencies = new Graph(); + ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies); + ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies); + // give rewriter a chance to do processing + //rewriter.PostResolve(m); + } else if (decl is AliasModuleDecl) { + var alias = (AliasModuleDecl)decl; + // resolve the path + ModuleSignature p; + if (ResolvePath(alias.Root, alias.Path, out p)) { + alias.Signature = p; + } else { + alias.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature + } + } else if (decl is AbstractModuleDecl) { + var abs = (AbstractModuleDecl)decl; + ModuleSignature p; ModuleDefinition mod; + if (ResolvePath(abs.Root, abs.Path, out p)) { + abs.Signature = MakeAbstractSignature(p, abs.Name, abs.Height, out mod); + moduleInfo = MergeSignature(abs.Signature, systemNameInfo); + // resolve + var datatypeDependencies = new Graph(); + ResolveTopLevelDecls_Signatures(mod.TopLevelDecls, datatypeDependencies); + ResolveTopLevelDecls_Meat(mod.TopLevelDecls, datatypeDependencies); + prog.Modules.Add(mod); + } else { + abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature + } + } else { Contract.Assert(false); } + Contract.Assert(decl.Signature != null); } // compute IsRecursive bit for mutually recursive functions - foreach (ModuleDecl m in mm) { + foreach (ModuleDefinition m in mm) { foreach (TopLevelDecl decl in m.TopLevelDecls) { ClassDecl cl = decl as ClassDecl; if (cl != null) { @@ -182,152 +224,153 @@ namespace Microsoft.Dafny { } } } + } - private class ModuleBindings { + + public class ModuleBindings { private ModuleBindings parent; private Dictionary modules; + private Dictionary bindings; public ModuleBindings(ModuleBindings p) { parent = p; - modules = new Dictionary(); + modules = new Dictionary(); + bindings = new Dictionary(); } - public bool BindName(string name, ModuleDecl subModule) { + public bool BindName(string name, ModuleDecl subModule, ModuleBindings b) { if (modules.ContainsKey(name)) { return false; } else { modules.Add(name, subModule); + bindings.Add(name, b); return true; } } - public bool TryLookup(string name, out ModuleDecl m) { - if (modules.TryGetValue(name, out m)) + public bool TryLookup(IToken name, out ModuleDecl m) { + Contract.Requires(name != null); + if (modules.TryGetValue(name.val, out m)) { return true; - else if (parent != null) { + } else if (parent != null) { return parent.TryLookup(name, out m); } else return false; } + public IEnumerable ModuleList { + get { return modules.Values; } + } + public ModuleBindings SubBindings(string name) { + ModuleBindings v = null; + bindings.TryGetValue(name, out v); + return v; + } } - private void BindModuleNames(ModuleDecl moduleDecl, ModuleBindings parentBindings, List globalModuleList, Graph importGraph) { - // a dictionary of submodules at the current scope. - var modules = new Dictionary(); - var moduleList = new List(); + private ModuleBindings BindModuleNames(ModuleDefinition moduleDecl, ModuleBindings parentBindings) { var bindings = new ModuleBindings(parentBindings); + foreach (var tld in moduleDecl.TopLevelDecls) { - var submodule = tld as SubModuleDecl; - if (submodule != null) { - var name = submodule.SubModule.Name; - if (!bindings.BindName(name, submodule.SubModule)) { - Error(submodule.Module, "Duplicate module name: {0}", name); - } else { - moduleList.Add(submodule.SubModule); + if (tld is LiteralModuleDecl) { + var subdecl = (LiteralModuleDecl)tld; + var subBindings = BindModuleNames(subdecl.ModuleDef, bindings); + subdecl.ModuleDef.Bindings = subBindings; + if (!bindings.BindName(subdecl.Name, subdecl, subBindings)) { + Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name); } - } - } - - // resolve refines and imports - foreach (var m in moduleList) { - importGraph.AddVertex(m); - if (m.RefinementBaseName != null) { - ModuleDecl other; - if (!bindings.TryLookup(m.RefinementBaseName, out other)) { - Error(m, "module {0} named as refinement base does not exist", m.RefinementBaseName); - } else if (other == m) { - Error(m, "module cannot refine itself: {0}", m.RefinementBaseName); - } else { - Contract.Assert(other != null); // follows from postcondition of TryGetValue - importGraph.AddEdge(m, other); - m.RefinementBase = other; + } else if (tld is AbstractModuleDecl) { + var subdecl = (AbstractModuleDecl)tld; + if (!bindings.BindName(subdecl.Name, subdecl, null)) { + Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name); } - } - foreach (string imp in m.ImportNames) { - ModuleDecl other; - if (!bindings.TryLookup(imp, out other)) { - Error(m, "module {0} named among imports does not exist", imp); - } else if (other == m) { - Error(m, "module must not import itself: {0}", imp); - } else { - Contract.Assert(other != null); // follows from postcondition of TryGetValue - importGraph.AddEdge(m, other); - m.Imports.Add(other); + } else if (tld is AliasModuleDecl) { + var subdecl = (AliasModuleDecl)tld; + if (!bindings.BindName(subdecl.Name, subdecl, null)) { + Error(subdecl.Module, "Duplicate module name: {0}", subdecl.Name); } } - foreach (var dep in m.Dependencies) { - importGraph.AddEdge(m, dep); - } - } - foreach (var m in moduleList) { - BindModuleNames(m, bindings, globalModuleList, importGraph); } - globalModuleList.AddRange(moduleList); + return bindings; } - public class ModuleNameInformation - { - public readonly Dictionary Classes = new Dictionary(); - public readonly Dictionary ImportedNames = new Dictionary(); - public readonly Dictionary> Ctors = new Dictionary>(); - - public static ModuleNameInformation Merge(ModuleDecl m, ModuleNameInformation system, ModuleNameInformation[] modules) { - var info = new ModuleNameInformation(); - // add the system-declared information, among which we know there are no duplicates - foreach (var kv in system.Classes) { - info.Classes.Add(kv.Key, kv.Value); - } - foreach (var kv in system.Ctors) { - info.Ctors.Add(kv.Key, kv.Value); - } - // for each imported module, add its information, noting any duplicates - foreach (var im in m.Imports) { - Contract.Assume(0 <= im.Height && im.Height < m.Height); - var import = modules[im.Height]; - info.ImportedNames.Add(im.Name, im); - // classes: - foreach (var kv in import.Classes) { - TopLevelDecl d; - if (info.Classes.TryGetValue(kv.Key, out d)) { - info.Classes[kv.Key] = new AmbiguousTopLevelDecl(m, d, kv.Value); - } else { - info.Classes.Add(kv.Key, kv.Value); - } - } - // constructors: - foreach (var kv in import.Ctors) { - Tuple pair; - if (info.Ctors.TryGetValue(kv.Key, out pair)) { - // mark it as a duplicate - info.Ctors[kv.Key] = new Tuple(pair.Item1, true); - } else { - // add new - info.Ctors.Add(kv.Key, kv.Value); - } - } + private void ProcessDependenciesDefinition(ModuleDecl decl, ModuleDefinition m, ModuleBindings bindings, Graph dependencies) { + if (m.RefinementBaseName != null) { + ModuleDecl other; + if (!bindings.TryLookup(m.RefinementBaseName[0], out other)) { + Error(m, "module {0} named as refinement base does not exist", m.RefinementBaseName[0].val); + } else if (other is LiteralModuleDecl && ((LiteralModuleDecl)other).ModuleDef == m) { + Error(m, "module cannot refine itself: {0}", m.RefinementBaseName[0].val); + } else { + Contract.Assert(other != null); // follows from postcondition of TryGetValue + dependencies.AddEdge(decl, other); + m.RefinementBaseRoot = other; } - // finally, for the module itself, let its information override whatever is imported - foreach (var kv in modules[m.Height].Classes) { - info.Classes[kv.Key] = kv.Value; + } + foreach (var toplevel in m.TopLevelDecls) { + if (toplevel is ModuleDecl) { + var d = (ModuleDecl)toplevel; + dependencies.AddEdge(decl, d); + var subbindings = bindings.SubBindings(d.Name); + ProcessDependencies(d, subbindings ?? bindings, dependencies); } - foreach (var kv in modules[m.Height].Ctors) { - info.Ctors[kv.Key] = kv.Value; + } + } + private void ProcessDependencies(ModuleDecl moduleDecl, ModuleBindings bindings, Graph dependencies) { + // resolve refines and imports + if (moduleDecl is LiteralModuleDecl) { + ProcessDependenciesDefinition(moduleDecl, ((LiteralModuleDecl)moduleDecl).ModuleDef, bindings, dependencies); + } else if (moduleDecl is AliasModuleDecl) { + var alias = moduleDecl as AliasModuleDecl; + ModuleDecl root; + if (!bindings.TryLookup(alias.Path[0], out root)) + Error(alias.tok, "module {0} does not exist", Util.Comma(".", alias.Path, x => x.val)); + else { + dependencies.AddEdge(moduleDecl, root); + alias.Root = root; + } + } else if (moduleDecl is AbstractModuleDecl) { + var abs = moduleDecl as AbstractModuleDecl; + ModuleDecl root; + if (!bindings.TryLookup(abs.Path[0], out root)) + Error(abs.tok, "module {0} does not exist", Util.Comma(".", abs.Path, x => x.val)); + else { + dependencies.AddEdge(moduleDecl, root); + abs.Root = root; } - return info; } } - ModuleNameInformation RegisterTopLevelDecls(List declarations) { - Contract.Requires(declarations != null); - var info = new ModuleNameInformation(); + public static ModuleSignature MergeSignature(ModuleSignature m, ModuleSignature system) { + var info = new ModuleSignature(); + // add the system-declared information, among which we know there are no duplicates + foreach (var kv in system.TopLevels) { + info.TopLevels.Add(kv.Key, kv.Value); + } + foreach (var kv in system.Ctors) { + info.Ctors.Add(kv.Key, kv.Value); + } + // add for the module itself + foreach (var kv in m.TopLevels) { + info.TopLevels[kv.Key] = kv.Value; + } + foreach (var kv in m.Ctors) { + info.Ctors[kv.Key] = kv.Value; + } + return info; + } + ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) { + Contract.Requires(moduleDef != null); + var sig = new ModuleSignature(); + sig.ModuleDef = moduleDef; + List declarations = moduleDef.TopLevelDecls; foreach (TopLevelDecl d in declarations) { Contract.Assert(d != null); - // register the class/datatype name - if (info.Classes.ContainsKey(d.Name)) { + // register the class/datatype/module name + if (sig.TopLevels.ContainsKey(d.Name)) { Error(d, "Duplicate name of top-level declaration: {0}", d.Name); } else { - info.Classes.Add(d.Name, d); + sig.TopLevels.Add(d.Name, d); } - if (d is SubModuleDecl) { - // do Nothing + if (d is ModuleDecl) { + // nothing to do } else if (d is ArbitraryTypeDecl) { // nothing more to register @@ -378,12 +421,12 @@ namespace Microsoft.Dafny { // also register the constructor name globally Tuple pair; - if (info.Ctors.TryGetValue(ctor.Name, out pair)) { + if (sig.Ctors.TryGetValue(ctor.Name, out pair)) { // mark it as a duplicate - info.Ctors[ctor.Name] = new Tuple(pair.Item1, true); + sig.Ctors[ctor.Name] = new Tuple(pair.Item1, true); } else { // add new - info.Ctors.Add(ctor.Name, new Tuple(ctor, false)); + sig.Ctors.Add(ctor.Name, new Tuple(ctor, false)); } } } @@ -405,9 +448,331 @@ namespace Microsoft.Dafny { } } } - return info; + return sig; + } + + private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, out ModuleDefinition mod) { + mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null); + mod.Height = Height; + foreach (var kv in p.TopLevels) { + mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod)); + } + return RegisterTopLevelDecls(mod); + } + TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) { + Contract.Requires(d != null); + Contract.Requires(m != null); + + if (d is ArbitraryTypeDecl) { + var dd = (ArbitraryTypeDecl)d; + return new ArbitraryTypeDecl(dd.tok, dd.Name, m, null); + } else if (d is IndDatatypeDecl) { + var dd = (IndDatatypeDecl)d; + var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); + var ctors = dd.Ctors.ConvertAll(CloneCtor); + var dt = new IndDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null); + return dt; + } else if (d is CoDatatypeDecl) { + var dd = (CoDatatypeDecl)d; + var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); + var ctors = dd.Ctors.ConvertAll(CloneCtor); + var dt = new CoDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null); + return dt; + } else if (d is ClassDecl) { + var dd = (ClassDecl)d; + var tps = dd.TypeArgs.ConvertAll(CloneTypeParam); + var mm = dd.Members.ConvertAll(CloneMember); + var cl = new ClassDecl(dd.tok, dd.Name, m, tps, mm, null); + return cl; + } else if (d is ModuleDecl) { + if (d is LiteralModuleDecl) { + return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m); + } else if (d is AliasModuleDecl) { + var a = (AliasModuleDecl)d; + var alias = new AliasModuleDecl(a.Path, a.tok, m); + alias.ModuleReference = a.ModuleReference; + alias.Signature = a.Signature; + return alias; + } + Contract.Assert(false); // unexpected declaration + return null; // to please compiler + } else { + Contract.Assert(false); // unexpected declaration + return null; // to please compiler + } + } + MemberDecl CloneMember(MemberDecl member) { + if (member is Field) { + var f = (Field)member; + return new Field(f.tok, f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null); + } else if (member is Function) { + var f = (Function)member; + return CloneFunction(f.tok, f, f.IsGhost); + } else { + var m = (Method)member; + return CloneMethod(m); + } + } + TypeParameter CloneTypeParam(TypeParameter tp) { + return new TypeParameter(tp.tok, tp.Name); + } + + DatatypeCtor CloneCtor(DatatypeCtor ct) { + return new DatatypeCtor(ct.tok, ct.Name, ct.Formals.ConvertAll(CloneFormal), null); + } + Formal CloneFormal(Formal formal) { + return new Formal(formal.tok, formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost); + } + Type CloneType(Type t) { + if (t is BasicType) { + return t; + } else if (t is SetType) { + var tt = (SetType)t; + return new SetType(CloneType(tt.Arg)); + } else if (t is SeqType) { + var tt = (SeqType)t; + return new SeqType(CloneType(tt.Arg)); + } else if (t is MultiSetType) { + var tt = (MultiSetType)t; + return new MultiSetType(CloneType(tt.Arg)); + } else if (t is MapType) { + var tt = (MapType)t; + return new MapType(CloneType(tt.Domain), CloneType(tt.Range)); + } else if (t is UserDefinedType) { + var tt = (UserDefinedType)t; + return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : tt.ModuleName); + } else if (t is InferredTypeProxy) { + return new InferredTypeProxy(); + } else { + Contract.Assert(false); // unexpected type (e.g., no other type proxies are expected at this time) + return null; // to please compiler + } + } + Function CloneFunction(IToken tok, Function f, bool isGhost) { + + var tps = f.TypeArgs.ConvertAll(CloneTypeParam); + var formals = f.Formals.ConvertAll(CloneFormal); + var req = f.Req.ConvertAll(CloneExpr); + var reads = f.Reads.ConvertAll(CloneFrameExpr); + var decreases = CloneSpecExpr(f.Decreases); + + var ens = f.Ens.ConvertAll(CloneExpr); + + Expression body = CloneExpr(f.Body); + + if (f is Predicate) { + return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, + req, reads, ens, decreases, body, false, null, false); + } else { + return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType), + req, reads, ens, decreases, body, null, false); + } + } + Method CloneMethod(Method m) { + Contract.Requires(m != null); + + var tps = m.TypeArgs.ConvertAll(CloneTypeParam); + var ins = m.Ins.ConvertAll(CloneFormal); + var req = m.Req.ConvertAll(CloneMayBeFreeExpr); + var mod = CloneSpecFrameExpr(m.Mod); + var decreases = CloneSpecExpr(m.Decreases); + + var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr); + + if (m is Constructor) { + return new Constructor(m.tok, m.Name, tps, ins, + req, mod, ens, decreases, null, null, false); + } else { + return new Method(m.tok, m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal), + req, mod, ens, decreases, null, null, false); + } + } + Specification CloneSpecExpr(Specification spec) { + var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr); + return new Specification(ee, null); + } + Specification CloneSpecFrameExpr(Specification frame) { + var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr); + return new Specification(ee, null); + } + FrameExpression CloneFrameExpr(FrameExpression frame) { + return new FrameExpression(CloneExpr(frame.E), frame.FieldName); + } + MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) { + return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree); + } + BoundVar CloneBoundVar(BoundVar bv) { + return new BoundVar((bv.tok), bv.Name, CloneType(bv.Type)); + } + Expression CloneExpr(Expression expr) { + if (expr == null) { + return null; + } else if (expr is LiteralExpr) { + var e = (LiteralExpr)expr; + if (e.Value == null) { + return new LiteralExpr((e.tok)); + } else if (e.Value is bool) { + return new LiteralExpr((e.tok), (bool)e.Value); + } else { + return new LiteralExpr((e.tok), (BigInteger)e.Value); + } + + } else if (expr is ThisExpr) { + if (expr is ImplicitThisExpr) { + return new ImplicitThisExpr((expr.tok)); + } else { + return new ThisExpr((expr.tok)); + } + + } else if (expr is IdentifierExpr) { + var e = (IdentifierExpr)expr; + return new IdentifierExpr((e.tok), e.Name); + + } else if (expr is DatatypeValue) { + var e = (DatatypeValue)expr; + return new DatatypeValue((e.tok), e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr)); + + } else if (expr is DisplayExpression) { + DisplayExpression e = (DisplayExpression)expr; + if (expr is SetDisplayExpr) { + return new SetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr)); + } else if (expr is MultiSetDisplayExpr) { + return new MultiSetDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr)); + } else { + Contract.Assert(expr is SeqDisplayExpr); + return new SeqDisplayExpr((e.tok), e.Elements.ConvertAll(CloneExpr)); + } + + } else if (expr is MapDisplayExpr) { + MapDisplayExpr e = (MapDisplayExpr)expr; + List pp = new List(); + foreach (ExpressionPair p in e.Elements) { + pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B))); + } + return new MapDisplayExpr((expr.tok), pp); + } else if (expr is ExprDotName) { + var e = (ExprDotName)expr; + return new ExprDotName((e.tok), CloneExpr(e.Obj), e.SuffixName); + + } else if (expr is FieldSelectExpr) { + var e = (FieldSelectExpr)expr; + return new FieldSelectExpr((e.tok), CloneExpr(e.Obj), e.FieldName); + + } else if (expr is SeqSelectExpr) { + var e = (SeqSelectExpr)expr; + return new SeqSelectExpr((e.tok), e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1)); + + } else if (expr is MultiSelectExpr) { + var e = (MultiSelectExpr)expr; + return new MultiSelectExpr((e.tok), CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr)); + + } else if (expr is SeqUpdateExpr) { + var e = (SeqUpdateExpr)expr; + return new SeqUpdateExpr((e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value)); + + } else if (expr is FunctionCallExpr) { + var e = (FunctionCallExpr)expr; + return new FunctionCallExpr((e.tok), e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr)); + + } else if (expr is OldExpr) { + var e = (OldExpr)expr; + return new OldExpr((e.tok), CloneExpr(e.E)); + + } else if (expr is MultiSetFormingExpr) { + var e = (MultiSetFormingExpr)expr; + return new MultiSetFormingExpr((e.tok), CloneExpr(e.E)); + + } else if (expr is FreshExpr) { + var e = (FreshExpr)expr; + return new FreshExpr((e.tok), CloneExpr(e.E)); + + } else if (expr is AllocatedExpr) { + var e = (AllocatedExpr)expr; + return new AllocatedExpr((e.tok), CloneExpr(e.E)); + + } else if (expr is UnaryExpr) { + var e = (UnaryExpr)expr; + return new UnaryExpr((e.tok), e.Op, CloneExpr(e.E)); + + } else if (expr is BinaryExpr) { + var e = (BinaryExpr)expr; + return new BinaryExpr((e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1)); + + } else if (expr is ChainingExpression) { + var e = (ChainingExpression)expr; + return CloneExpr(e.E); // just clone the desugaring, since it's already available + + } else if (expr is LetExpr) { + var e = (LetExpr)expr; + return new LetExpr((e.tok), e.Vars.ConvertAll(CloneBoundVar), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body)); + + } else if (expr is ComprehensionExpr) { + var e = (ComprehensionExpr)expr; + var tk = (e.tok); + var bvs = e.BoundVars.ConvertAll(CloneBoundVar); + var range = CloneExpr(e.Range); + var term = CloneExpr(e.Term); + if (e is ForallExpr) { + return new ForallExpr(tk, bvs, range, term, null); + } else if (e is ExistsExpr) { + return new ExistsExpr(tk, bvs, range, term, null); + } else if (e is MapComprehension) { + return new MapComprehension(tk, bvs, range, term); + } else { + Contract.Assert(e is SetComprehension); + return new SetComprehension(tk, bvs, range, term); + } + + } else if (expr is WildcardExpr) { + return new WildcardExpr((expr.tok)); + + } else if (expr is PredicateExpr) { + var e = (PredicateExpr)expr; + if (e is AssertExpr) { + return new AssertExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body)); + } else { + Contract.Assert(e is AssumeExpr); + return new AssumeExpr((e.tok), CloneExpr(e.Guard), CloneExpr(e.Body)); + } + + } else if (expr is ITEExpr) { + var e = (ITEExpr)expr; + return new ITEExpr((e.tok), CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els)); + + } else if (expr is ParensExpression) { + var e = (ParensExpression)expr; + return CloneExpr(e.E); // skip the parentheses in the clone + + } else if (expr is IdentifierSequence) { + var e = (IdentifierSequence)expr; + var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr); + return new IdentifierSequence(e.Tokens.ConvertAll(tk => (tk)), e.OpenParen == null ? null : (e.OpenParen), aa); + + } else if (expr is MatchExpr) { + var e = (MatchExpr)expr; + return new MatchExpr((e.tok), CloneExpr(e.Source), + e.Cases.ConvertAll(c => new MatchCaseExpr((c.tok), c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body)))); + + } else { + Contract.Assert(false); throw new cce.UnreachableException(); // unexpected expression + } } + private bool ResolvePath(ModuleDecl root, List Path, out ModuleSignature p) { + p = root.Signature; + int i = 1; + while (i < Path.Count) { + ModuleSignature pp; + if (p.FindSubmodule(Path[i].val, out pp)) { + p = pp; + i++; + } else { + Error(Path[i], "module {0} does not exist", Path[i].val); + break; + } + } + return i == Path.Count; + } public void ResolveTopLevelDecls_Signatures(List/*!*/ declarations, Graph/*!*/ datatypeDependencies) { Contract.Requires(declarations != null); Contract.Requires(datatypeDependencies != null); // more expensive check: Contract.Requires(cce.NonNullElements(datatypeDependencies)); @@ -419,7 +784,7 @@ namespace Microsoft.Dafny { // nothing to do } else if (d is ClassDecl) { ResolveClassMemberTypes((ClassDecl)d); - } else if (d is SubModuleDecl) { + } else if (d is ModuleDecl) { // TODO: what goes here? } else { ResolveCtorTypes((DatatypeDecl)d, datatypeDependencies); @@ -999,23 +1364,15 @@ namespace Microsoft.Dafny { } else if (t.ResolvedClass == null) { // this test is because 'array' is already resolved; TODO: an alternative would be to pre-populate 'classes' with built-in references types like 'array' (and perhaps in the future 'string') TopLevelDecl d = null; if (t.ModuleName != null) { - foreach (var imp in currentClass.Module.Imports) { - if (imp.Name == t.ModuleName.val) { - // now search among the types declared in module "imp" - foreach (var tld in imp.TopLevelDecls) { // this search is slow, but oh well - if (tld.Name == t.Name) { - // found the class - d = tld; - goto DONE_WITH_QUALIFIED_NAME; - } - } - Error(t.tok, "Undeclared class name {0} in module {1}", t.Name, t.ModuleName.val); - goto DONE_WITH_QUALIFIED_NAME; + ModuleDecl m; + if (currentClass.Module.Bindings.TryLookup(t.ModuleName, out m)) { + if (!m.Signature.TopLevels.TryGetValue(t.Name, out d)) { + Error(t.tok, "The name does not exist in the given module"); } + } else { + Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val); } - Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val); - DONE_WITH_QUALIFIED_NAME: ; - } else if (!moduleInfo.Classes.TryGetValue(t.Name, out d)) { + } else if (!moduleInfo.TopLevels.TryGetValue(t.Name, out d)) { Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name); } @@ -2234,13 +2591,14 @@ namespace Microsoft.Dafny { // Resolution termination check if (method.EnclosingClass != null && callee.EnclosingClass != null) { - ModuleDecl callerModule = method.EnclosingClass.Module; - ModuleDecl calleeModule = callee.EnclosingClass.Module; + ModuleDefinition callerModule = method.EnclosingClass.Module; + ModuleDefinition calleeModule = callee.EnclosingClass.Module; if (callerModule == calleeModule) { // intra-module call; this is allowed; add edge in module's call graph callerModule.CallGraph.AddEdge(method, callee); } else { - Contract.Assert(importGraph.Reaches(callerModule, calleeModule)); + //Contract.Assert(dependencies.Reaches(callerModule, calleeModule)); + // } } } @@ -2674,7 +3032,7 @@ namespace Microsoft.Dafny { } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; TopLevelDecl d; - if (!moduleInfo.Classes.TryGetValue(dtv.DatatypeName, out d)) { + if (!moduleInfo.TopLevels.TryGetValue(dtv.DatatypeName, out d)) { Error(expr.tok, "Undeclared datatype: {0}", dtv.DatatypeName); } else if (d is AmbiguousTopLevelDecl) { Error(expr.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", dtv.DatatypeName, ((AmbiguousTopLevelDecl)d).ModuleNames()); @@ -2952,7 +3310,7 @@ namespace Microsoft.Dafny { case BinaryExpr.Opcode.Eq: case BinaryExpr.Opcode.Neq: - if (!CouldPossiblyBeSameType(e.E0.Type, e.E1.Type)) { + if (!ComparableTypes(e.E0.Type, e.E1.Type)) { if (!UnifyTypes(e.E0.Type, e.E1.Type)) { Error(expr, "arguments must have the same type (got {0} and {1})", e.E0.Type, e.E1.Type); } @@ -3347,6 +3705,31 @@ namespace Microsoft.Dafny { } } + private bool ComparableTypes(Type A, Type B) { + if (A.IsArrayType && B.IsArrayType) { + Type a = UserDefinedType.ArrayElementType(A); + Type b = UserDefinedType.ArrayElementType(B); + return CouldPossiblyBeSameType(a, b); + } else + if (A is UserDefinedType && B is UserDefinedType) { + UserDefinedType a = (UserDefinedType)A; + UserDefinedType b = (UserDefinedType)B; + if (a.ResolvedClass != null && b.ResolvedClass != null && a.ResolvedClass.Name == b.ResolvedClass.Name) { + if (a.TypeArgs.Count != b.TypeArgs.Count) { + return false; // this probably doesn't happen if the classes are the same. + } + for (int i = 0; i < a.TypeArgs.Count; i++) { + if (!CouldPossiblyBeSameType(a.TypeArgs[i], b.TypeArgs[i])) + return false; + } + // all parameters could be the same + return true; + } + // either we don't know what class it is yet, or the classes mismatch + return false; + } + return false; + } private bool CouldPossiblyBeSameType(Type A, Type B) { if (A.IsTypeParameter || B.IsTypeParameter) { return true; @@ -3541,8 +3924,8 @@ namespace Microsoft.Dafny { // Resolution termination check if (currentFunction != null && currentFunction.EnclosingClass != null && function.EnclosingClass != null) { - ModuleDecl callerModule = currentFunction.EnclosingClass.Module; - ModuleDecl calleeModule = function.EnclosingClass.Module; + ModuleDefinition callerModule = currentFunction.EnclosingClass.Module; + ModuleDefinition calleeModule = function.EnclosingClass.Module; if (callerModule == calleeModule) { // intra-module call; this is allowed; add edge in module's call graph callerModule.CallGraph.AddEdge(currentFunction, function); @@ -3550,7 +3933,7 @@ namespace Microsoft.Dafny { currentFunction.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere) } } else { - Contract.Assert(importGraph.Reaches(callerModule, calleeModule)); + //Contract.Assert(dependencies.Reaches(callerModule, calleeModule)); } } } @@ -3578,7 +3961,6 @@ namespace Microsoft.Dafny { Tuple pair; Dictionary members; MemberDecl member; - ModuleDecl module; var id = e.Tokens[0]; if (scope.Find(id.val) != null) { // ----- root is a local variable, parameter, or bound variable @@ -3586,7 +3968,7 @@ namespace Microsoft.Dafny { ResolveExpression(r, twoState); r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call); - } else if (moduleInfo.Classes.TryGetValue(id.val, out decl)) { + } else if (moduleInfo.TopLevels.TryGetValue(id.val, out decl)) { if (decl is AmbiguousTopLevelDecl) { Error(id, "The name {0} ambiguously refers to a type in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames()); } else if (e.Tokens.Count == 1 && e.Arguments == null) { @@ -3602,13 +3984,12 @@ namespace Microsoft.Dafny { var cd = (ClassDecl)decl; r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, allowMethodCall, out call); - } else if (decl is SubModuleDecl) { + } else if (decl is ModuleDecl) { // ----- root is a submodule - module = ((SubModuleDecl)decl).SubModule; if (!(1 < e.Tokens.Count)) { - Error(e.tok, "module {0} is not an expression", module.Name); + Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name); } - call = ResolveIdentifierSequenceModuleScope(e, 1, moduleNameInfo[module.Height], twoState, allowMethodCall); + call = ResolveIdentifierSequenceModuleScope(e, 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall); } else { // ----- root is a datatype var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl @@ -3634,11 +4015,6 @@ namespace Microsoft.Dafny { } } - } else if (moduleInfo.ImportedNames.TryGetValue(id.val, out module)) { - if (e.Tokens.Count <= 1) { - Error(e.tok, "module {0} is not an expression", module.Name); - } - call = ResolveIdentifierSequenceModuleScope(e, 1, moduleNameInfo[module.Height], twoState, allowMethodCall); } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) { // ----- field, function, or method Expression receiver; @@ -3671,7 +4047,7 @@ namespace Microsoft.Dafny { return call; } - CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleNameInformation info, bool twoState, bool allowMethodCall) { + CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature info, bool twoState, bool allowMethodCall) { // Look up "id" as follows: // - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type) // (if two imported types have the same name, an error message is produced here) @@ -3682,9 +4058,8 @@ namespace Microsoft.Dafny { CallRhs call = null; TopLevelDecl decl; - ModuleDecl module; var id = e.Tokens[p]; - if (info.Classes.TryGetValue(id.val, out decl)) { + if (info.TopLevels.TryGetValue(id.val, out decl)) { if (decl is AmbiguousTopLevelDecl) { Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames()); } else if (decl is ClassDecl) { @@ -3692,13 +4067,12 @@ namespace Microsoft.Dafny { var cd = (ClassDecl)decl; r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, p + 1, twoState, allowMethodCall, out call); - } else if (decl is SubModuleDecl) { + } else if (decl is ModuleDecl) { // ----- root is a submodule - module = ((SubModuleDecl)decl).SubModule; if (!(p + 1 < e.Tokens.Count)) { - Error(e.tok, "module {0} is not an expression", module.Name); + Error(e.tok, "module {0} cannot be used here", ((ModuleDecl)decl).Name); } - call = ResolveIdentifierSequenceModuleScope(e, p+1, moduleNameInfo[module.Height], twoState, allowMethodCall); + call = ResolveIdentifierSequenceModuleScope(e, p + 1, ((ModuleDecl)decl).Signature, twoState, allowMethodCall); } else { // ----- root is a datatype var dt = (DatatypeDecl)decl; // otherwise, unexpected TopLevelDecl @@ -4513,7 +4887,7 @@ namespace Microsoft.Dafny { class CoCallResolution { - readonly ModuleDecl currentModule; + readonly ModuleDefinition currentModule; readonly Function currentFunction; readonly bool dealsWithCodatatypes; diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 26ec496e..45e4f50c 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -6,8 +6,8 @@ namespace Microsoft.Dafny { public interface Rewriter { - void PreResolve(ModuleDecl m); - void PostResolve(ModuleDecl m); + void PreResolve(ModuleDefinition m); + void PostResolve(ModuleDefinition m); } /// @@ -50,7 +50,7 @@ namespace Microsoft.Dafny /// public class AutoContractsRewriter : Rewriter { - public void PreResolve(ModuleDecl m) { + public void PreResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { bool sayYes = true; if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) { @@ -101,7 +101,7 @@ namespace Microsoft.Dafny } } - public void PostResolve(ModuleDecl m) { + public void PostResolve(ModuleDefinition m) { foreach (var d in m.TopLevelDecls) { bool sayYes = true; if (d is ClassDecl && Attributes.ContainsBool(d.Attributes, "autocontracts", ref sayYes) && sayYes) { diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index d35fc22f..307fa321 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -262,12 +262,12 @@ public class Scanner { start[123] = 10; start[125] = 11; start[61] = 57; - start[124] = 58; start[59] = 19; + start[46] = 58; + start[124] = 59; start[44] = 20; - start[60] = 59; - start[62] = 60; - start[46] = 61; + start[60] = 60; + start[62] = 61; start[40] = 22; start[41] = 23; start[42] = 24; @@ -491,29 +491,29 @@ public class Scanner { case "ghost": t.kind = 8; break; case "module": t.kind = 9; break; case "refines": t.kind = 10; break; - case "imports": t.kind = 11; break; - case "class": t.kind = 12; break; - case "static": t.kind = 13; break; - case "datatype": t.kind = 14; break; - case "codatatype": t.kind = 15; break; - case "var": t.kind = 19; break; - case "type": t.kind = 21; break; - case "method": t.kind = 24; break; - case "constructor": t.kind = 25; break; - case "returns": t.kind = 26; break; - case "modifies": t.kind = 28; break; - case "free": t.kind = 29; break; - case "requires": t.kind = 30; break; - case "ensures": t.kind = 31; break; - case "decreases": t.kind = 32; break; - case "bool": t.kind = 35; break; - case "nat": t.kind = 36; break; - case "int": t.kind = 37; break; - case "set": t.kind = 38; break; - case "multiset": t.kind = 39; break; - case "seq": t.kind = 40; break; - case "map": t.kind = 41; break; - case "object": t.kind = 42; break; + case "as": t.kind = 13; break; + case "class": t.kind = 15; break; + case "static": t.kind = 16; break; + case "datatype": t.kind = 17; break; + case "codatatype": t.kind = 18; break; + case "var": t.kind = 20; break; + case "type": t.kind = 22; break; + case "method": t.kind = 25; break; + case "constructor": t.kind = 26; break; + case "returns": t.kind = 27; break; + case "modifies": t.kind = 29; break; + case "free": t.kind = 30; break; + case "requires": t.kind = 31; break; + case "ensures": t.kind = 32; break; + case "decreases": t.kind = 33; break; + case "bool": t.kind = 36; break; + case "nat": t.kind = 37; break; + case "int": t.kind = 38; break; + case "set": t.kind = 39; break; + case "multiset": t.kind = 40; break; + case "seq": t.kind = 41; break; + case "map": t.kind = 42; break; + case "object": t.kind = 43; break; case "function": t.kind = 44; break; case "predicate": t.kind = 45; break; case "reads": t.kind = 46; break; @@ -648,15 +648,15 @@ public class Scanner { else if (ch >= '0' && ch <= '9') {AddCh(); goto case 18;} else {t.kind = 3; break;} case 19: - {t.kind = 18; break;} + {t.kind = 12; break;} case 20: - {t.kind = 20; break;} + {t.kind = 21; break;} case 21: - {t.kind = 27; break;} + {t.kind = 28; break;} case 22: - {t.kind = 33; break;} - case 23: {t.kind = 34; break;} + case 23: + {t.kind = 35; break;} case 24: {t.kind = 47; break;} case 25: @@ -730,26 +730,26 @@ public class Scanner { else if (ch == ':') {AddCh(); goto case 54;} else {t.kind = 5; break;} case 57: - recEnd = pos; recKind = 16; + recEnd = pos; recKind = 11; if (ch == '>') {AddCh(); goto case 30;} else if (ch == '=') {AddCh(); goto case 63;} - else {t.kind = 16; break;} + else {t.kind = 11; break;} case 58: - recEnd = pos; recKind = 17; - if (ch == '|') {AddCh(); goto case 39;} - else {t.kind = 17; break;} + recEnd = pos; recKind = 14; + if (ch == '.') {AddCh(); goto case 64;} + else {t.kind = 14; break;} case 59: - recEnd = pos; recKind = 22; - if (ch == '=') {AddCh(); goto case 64;} - else {t.kind = 22; break;} + recEnd = pos; recKind = 19; + if (ch == '|') {AddCh(); goto case 39;} + else {t.kind = 19; break;} case 60: recEnd = pos; recKind = 23; - if (ch == '=') {AddCh(); goto case 41;} + if (ch == '=') {AddCh(); goto case 65;} else {t.kind = 23; break;} case 61: - recEnd = pos; recKind = 43; - if (ch == '.') {AddCh(); goto case 65;} - else {t.kind = 43; break;} + recEnd = pos; recKind = 24; + if (ch == '=') {AddCh(); goto case 41;} + else {t.kind = 24; break;} case 62: recEnd = pos; recKind = 83; if (ch == '=') {AddCh(); goto case 42;} @@ -760,13 +760,13 @@ public class Scanner { if (ch == '>') {AddCh(); goto case 34;} else {t.kind = 77; break;} case 64: - recEnd = pos; recKind = 78; - if (ch == '=') {AddCh(); goto case 31;} - else {t.kind = 78; break;} - case 65: recEnd = pos; recKind = 100; if (ch == '.') {AddCh(); goto case 21;} else {t.kind = 100; break;} + case 65: + recEnd = pos; recKind = 78; + if (ch == '=') {AddCh(); goto case 31;} + else {t.kind = 78; break;} } t.val = new String(tval, 0, tlen); diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index cb154729..7a841a3b 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -26,6 +26,7 @@ namespace Microsoft.Dafny { readonly Dictionary/*!*/ classes = new Dictionary(); readonly Dictionary/*!*/ fields = new Dictionary(); readonly Dictionary/*!*/ fieldFunctions = new Dictionary(); + readonly Dictionary fieldConstants = new Dictionary(); [ContractInvariantMethod] void ObjectInvariant() @@ -52,6 +53,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type HeapType; public readonly string HeapVarName; public readonly Bpl.Type ClassNameType; + public readonly Bpl.Type NameFamilyType; public readonly Bpl.Type DatatypeType; public readonly Bpl.Type DtCtorId; public readonly Bpl.Expr Null; @@ -70,6 +72,7 @@ namespace Microsoft.Dafny { Contract.Invariant(HeapType != null); Contract.Invariant(HeapVarName != null); Contract.Invariant(ClassNameType != null); + Contract.Invariant(NameFamilyType != null); Contract.Invariant(DatatypeType != null); Contract.Invariant(DtCtorId != null); Contract.Invariant(Null != null); @@ -125,7 +128,7 @@ namespace Microsoft.Dafny { public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType, Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType, - Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, + Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType, Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId, Bpl.Constant allocField, Bpl.Constant classDotArray) { #region Non-null preconditions on parameters @@ -157,6 +160,7 @@ namespace Microsoft.Dafny { this.HeapType = heap.TypedIdent.Type; this.HeapVarName = heap.Name; this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq()); + this.NameFamilyType = new Bpl.CtorType(Token.NoToken, nameFamilyType, new Bpl.TypeSeq()); this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq()); this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq()); this.allocField = allocField; @@ -179,6 +183,7 @@ namespace Microsoft.Dafny { Bpl.TypeCtorDecl seqTypeCtor = null; Bpl.TypeCtorDecl fieldNameType = null; Bpl.TypeCtorDecl classNameType = null; + Bpl.TypeCtorDecl nameFamilyType = null; Bpl.TypeCtorDecl datatypeType = null; Bpl.TypeCtorDecl dtCtorId = null; Bpl.TypeCtorDecl boxType = null; @@ -202,6 +207,8 @@ namespace Microsoft.Dafny { dtCtorId = dt; } else if (dt.Name == "ref") { refType = dt; + } else if (dt.Name == "NameFamily") { + nameFamilyType = dt; } else if (dt.Name == "BoxType") { boxType = dt; } else if (dt.Name == "TickType") { @@ -249,6 +256,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type Field"); } else if (classNameType == null) { Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName"); + } else if (nameFamilyType == null) { + Console.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily"); } else if (datatypeType == null) { Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType"); } else if (dtCtorId == null) { @@ -267,7 +276,7 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of class._System.array"); } else { return new PredefinedDecls(refType, boxType, tickType, - setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId, + setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, nameFamilyType, datatypeType, dtCtorId, allocField, classDotArray); } return null; @@ -325,19 +334,22 @@ namespace Microsoft.Dafny { AddClassMembers((ClassDecl)d); } } - foreach (ModuleDecl m in program.Modules) { + foreach (ModuleDefinition m in program.Modules) { foreach (TopLevelDecl d in m.TopLevelDecls) { if (d is ArbitraryTypeDecl) { // nothing to do--this is treated just like a type parameter } else if (d is DatatypeDecl) { AddDatatype((DatatypeDecl)d); - } else if (d is SubModuleDecl) { + } else if (d is ModuleDecl) { // submodules have already been added as a top level module, ignore this. } else { AddClassMembers((ClassDecl)d); } } } + foreach(var c in fieldConstants.Values) { + sink.TopLevelDeclarations.Add(c); + } return sink; } @@ -813,7 +825,7 @@ namespace Microsoft.Dafny { } // mh < ModuleContextHeight || (mh == ModuleContextHeight && (fh <= FunctionContextHeight || InMethodContext)) - ModuleDecl mod = f.EnclosingClass.Module; + ModuleDefinition mod = f.EnclosingClass.Module; var activateForeign = Bpl.Expr.Lt(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()); var activateIntra = Bpl.Expr.And( @@ -1019,7 +1031,7 @@ namespace Microsoft.Dafny { return Bpl.Expr.And(lower, upper); } - ModuleDecl currentModule = null; // the name of the module whose members are currently being translated + ModuleDefinition currentModule = null; // the name of the module whose members are currently being translated Method currentMethod = null; // the method whose implementation is currently being translated int loopHeapVarCount = 0; int otherTmpVarCount = 0; @@ -1556,7 +1568,7 @@ namespace Microsoft.Dafny { // the procedure itself Bpl.RequiresSeq req = new Bpl.RequiresSeq(); // free requires mh == ModuleContextHeight && fh == FunctionContextHeight; - ModuleDecl mod = f.EnclosingClass.Module; + ModuleDefinition mod = f.EnclosingClass.Module; Bpl.Expr context = Bpl.Expr.And( Bpl.Expr.Eq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()), Bpl.Expr.Eq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())); @@ -2374,7 +2386,7 @@ namespace Microsoft.Dafny { if (options.Decr != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes) { // check that the decreases measure goes down - ModuleDecl module = cce.NonNull(e.Function.EnclosingClass).Module; + ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module; if (module == cce.NonNull(options.Decr.EnclosingClass).Module) { if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(options.Decr)) { bool contextDecrInferred, calleeDecrInferred; @@ -2792,12 +2804,26 @@ namespace Microsoft.Dafny { if (classes.TryGetValue(cl, out cc)) { Contract.Assert(cc != null); } else { - cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullCompileName, predef.ClassNameType), true); + cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullCompileName, predef.ClassNameType), !cl.Module.IsAbstract); classes.Add(cl, cc); } return cc; } + Bpl.Constant GetFieldNameFamily(string n) { + Contract.Requires(n != null); + Contract.Requires(predef != null); + Contract.Ensures(Contract.Result() != null); + Bpl.Constant cc; + if (fieldConstants.TryGetValue(n, out cc)) { + Contract.Assert(cc != null); + } else { + cc = new Bpl.Constant(Token.NoToken, new Bpl.TypedIdent(Token.NoToken, "field$" + n, predef.NameFamilyType), true); + fieldConstants.Add(n, cc); + } + return cc; + } + Bpl.Expr GetTypeExpr(IToken tok, Type type) { Contract.Requires(tok != null); @@ -2857,13 +2883,13 @@ namespace Microsoft.Dafny { if (fields.TryGetValue(f, out fc)) { Contract.Assert(fc != null); } else { - // const unique f: Field ty; + // const f: Field ty; Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type)); - fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullCompileName, ty), true); + fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullCompileName, ty), false); fields.Add(f, fc); - // axiom FDim(f) == 0 && DeclType(f) == C; + // axiom FDim(f) == 0 && FieldOfDecl(C, name) == f; Bpl.Expr fdim = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FDim, ty, Bpl.Expr.Ident(fc)), Bpl.Expr.Literal(0)); - Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass)))); + Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FieldOfDecl, ty, new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))), new Bpl.IdentifierExpr(f.tok, GetFieldNameFamily(f.Name))), Bpl.Expr.Ident(fc)); Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fdim, declType)); sink.TopLevelDeclarations.Add(ax); } @@ -4387,7 +4413,7 @@ namespace Microsoft.Dafny { CheckFrameSubset(tok, method.Mod.Expressions, receiver, substMap, etran, builder, "call may violate context's modifies clause", null); // Check termination - ModuleDecl module = method.EnclosingClass.Module; + ModuleDefinition module = method.EnclosingClass.Module; if (module == currentModule) { if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(currentMethod)) { bool contextDecrInferred, calleeDecrInferred; @@ -5707,7 +5733,7 @@ namespace Microsoft.Dafny { } string nm = FunctionName(e.Function, 1 + offsetToUse); if (this.applyLimited_CurrentFunction != null && e.Function.IsRecursive) { - ModuleDecl module = cce.NonNull(e.Function.EnclosingClass).Module; + ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module; if (module == cce.NonNull(applyLimited_CurrentFunction.EnclosingClass).Module) { if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(applyLimited_CurrentFunction)) { nm = FunctionName(e.Function, 0 + offsetToUse); @@ -6525,6 +6551,7 @@ namespace Microsoft.Dafny { DtTypeParams, // type parameters of datatype TypeTuple, DeclType, + FieldOfDecl, FDim, // field dimension (0 - named, 1 or more - indexed) DatatypeCtorId, @@ -6763,6 +6790,10 @@ namespace Microsoft.Dafny { Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation != null); return FunctionCall(tok, "DeclType", predef.ClassNameType, args); + case BuiltinFunction.FieldOfDecl: + Contract.Assert(args.Length == 2); + Contract.Assert(typeInstantiation != null); + return FunctionCall(tok, "FieldOfDecl", predef.FieldName(tok, typeInstantiation) , args); case BuiltinFunction.FDim: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation != null); diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs new file mode 100644 index 00000000..e057727a --- /dev/null +++ b/Source/Dafny/Util.cs @@ -0,0 +1,20 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace Microsoft.Dafny { + class Util + { + public delegate string ToString(T t); + public static string Comma(string comma, List l, ToString f) { + string res = ""; + string c = ""; + foreach(var t in l) { + res += c + f(t); + c = comma; + } + return res; + } + } +} diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs index 4244e817..627353bf 100644 --- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs +++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs @@ -19,7 +19,7 @@ namespace Demo this.MarkReservedWords( // NOTE: these keywords must also appear once more below "class", "ghost", "static", "var", "method", "constructor", "datatype", "codatatype", "type", "assert", "assume", "new", "this", "object", "refines", - "module", "imports", + "module", "imports", "as", "if", "then", "else", "while", "invariant", "break", "label", "return", "parallel", "havoc", "print", "returns", "requires", "ensures", "modifies", "reads", "decreases", @@ -277,6 +277,7 @@ namespace Demo | "refines" | "module" | "imports" + | "as" | "if" | "then" | "else" -- cgit v1.2.3