summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Cloner.cs2
-rw-r--r--Source/Dafny/Compiler.cs6
-rw-r--r--Source/Dafny/Dafny.atg8
-rw-r--r--Source/Dafny/DafnyAst.cs10
-rw-r--r--Source/Dafny/Parser.cs18
-rw-r--r--Source/Dafny/Printer.cs4
-rw-r--r--Source/Dafny/Resolver.cs23
-rw-r--r--Source/Dafny/Translator.cs16
-rw-r--r--Source/DafnyDriver/DafnyDriver.cs5
9 files changed, 47 insertions, 45 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 0d77ecc6..60e737b1 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -105,7 +105,7 @@ namespace Microsoft.Dafny
if (d is DefaultClassDecl) {
return new DefaultClassDecl(m, mm);
} else {
- return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), new List<IToken> { dd.TraitId });
+ return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitTyp);
}
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index a3312c4a..0e8b886b 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -247,9 +247,9 @@ namespace Microsoft.Dafny {
else if (d is ClassDecl) {
var cl = (ClassDecl)d;
Indent(indent);
- if (cl.Trait != null && cl.Trait is TraitDecl)
+ if (cl.TraitObj != null && cl.TraitObj is TraitDecl)
{
- wr.WriteLine("public class @{0} : @{1}", cl.CompileName, cl.TraitId.val);
+ wr.WriteLine("public class @{0} : @{1}", cl.CompileName, ((UserDefinedType)cl.TraitTyp).tok);
}
else
wr.Write("public class @{0}", cl.CompileName);
@@ -767,7 +767,7 @@ namespace Microsoft.Dafny {
{
Indent(indent);
wr.WriteLine("public {0} @{1};", TypeName(f.Type), f.CompileName);
- wr.Write("{0} @{1}.@{2}", TypeName(f.Type), c.Trait.CompileName, f.CompileName);
+ wr.Write("{0} @{1}.@{2}", TypeName(f.Type), c.TraitObj.CompileName, f.CompileName);
wr.WriteLine(" {");
wr.WriteLine(" get { ");
wr.Write("return this.@{0};", f.CompileName);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 690f8403..5bc8ad5f 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -354,7 +354,7 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
= (. Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
- List<IToken>/*!*/ traitId=null;
+ Type/*!*/ trait = null;
Attributes attrs = null;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
@@ -365,12 +365,12 @@ ClassDecl<ModuleDefinition/*!*/ module, out ClassDecl/*!*/ c>
{ Attribute<ref attrs> }
NoUSIdent<out id>
[ GenericParameters<typeArgs> ]
- ["extends" QualifiedName<out traitId>]
- "{" (. bodyStart = t; .)
+ ["extends" Type<out trait>]
+ "{" (. bodyStart = t; .)
{ ClassMemberDecl<members, true>
}
"}"
- (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);
+ (. c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
.)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 7fa8df76..58666c6a 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1688,8 +1688,8 @@ namespace Microsoft.Dafny {
public class ClassDecl : TopLevelDecl {
public readonly List<MemberDecl> Members;
- public TraitDecl Trait;
- public readonly IToken TraitId;
+ public TraitDecl TraitObj;
+ public readonly Type TraitTyp;
public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -1697,7 +1697,7 @@ namespace Microsoft.Dafny {
}
public ClassDecl(IToken tok, string name, ModuleDefinition module,
- List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, List<IToken> traitId)
+ List<TypeParameter> typeArgs, [Captured] List<MemberDecl> members, Attributes attributes, Type trait)
: base(tok, name, module, typeArgs, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -1705,8 +1705,8 @@ namespace Microsoft.Dafny {
Contract.Requires(cce.NonNullElements(typeArgs));
Contract.Requires(cce.NonNullElements(members));
Members = members;
- if (traitId != null && traitId.Count > 0)
- TraitId = traitId[0]; //there are at most one inheriting trait at the moment
+ if (trait != null)
+ TraitTyp = trait; //there are at most one inheriting trait at the moment
}
public virtual bool IsDefaultClass {
get {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f990f9ff..dd1ff730 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -465,7 +465,7 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Contract.Requires(module != null);
Contract.Ensures(Contract.ValueAtReturn(out c) != null);
IToken/*!*/ id;
- List<IToken>/*!*/ traitId=null;
+ Type/*!*/ trait = null;
Attributes attrs = null;
List<TypeParameter/*!*/> typeArgs = new List<TypeParameter/*!*/>();
List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();
@@ -482,15 +482,15 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
if (la.kind == 31) {
Get();
- QualifiedName(out traitId);
+ Type(out trait);
}
Expect(15);
- bodyStart = t;
+ bodyStart = t;
while (StartOf(2)) {
ClassMemberDecl(members, true);
}
Expect(16);
- c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, traitId);
+ c = new ClassDecl(id, id.val, module, typeArgs, members, attrs, trait);
c.BodyStartTok = bodyStart;
c.BodyEndTok = t;
@@ -837,6 +837,11 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
Expect(47);
}
+ void Type(out Type ty) {
+ Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
+ TypeAndToken(out tok, out ty);
+ }
+
void FieldDecl(MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm) {
Contract.Requires(cce.NonNullElements(mm));
Attributes attrs = null;
@@ -1164,11 +1169,6 @@ bool CloseOptionalBrace(bool usesOptionalBrace) {
}
}
- void Type(out Type ty) {
- Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok;
- TypeAndToken(out tok, out ty);
- }
-
void Expression(out Expression e, bool allowSemi, bool allowLambda) {
Expression e0; IToken endTok;
EquivExpression(out e, allowSemi, allowLambda);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 9e569ef1..36eeb554 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -298,8 +298,8 @@ namespace Microsoft.Dafny {
Contract.Requires(c != null);
Indent(indent);
PrintClassMethodHelper((c is TraitDecl) ? "trait" : "class", c.Attributes, c.Name, c.TypeArgs);
- if (c.TraitId != null) {
- wr.Write(" extends {0}", c.TraitId.val);
+ if (c.TraitTyp != null) {
+ wr.Write(" extends {0}", ((UserDefinedType)(c.TraitTyp)).tok);
}
if (c.Members.Count == 0) {
wr.WriteLine(" { }");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 99045b01..b6b0ab0b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -2657,21 +2657,22 @@ namespace Microsoft.Dafny
currentClass = cl;
// Resolve names of traits extended
- if (cl.TraitId != null) {
- var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == cl.TraitId.val);
+ if (cl.TraitTyp != null && cl.TraitTyp is UserDefinedType)
+ {
+ var trait = classMembers.Keys.FirstOrDefault(traitDecl => traitDecl.CompileName == ((UserDefinedType)(cl.TraitTyp)).FullCompileName);
if (trait == null) {
- Error(cl.TraitId, "unresolved identifier: {0}", cl.TraitId.val);
+ Error(((UserDefinedType)(cl.TraitTyp)).tok, "unresolved identifier: {0}", ((UserDefinedType)(cl.TraitTyp)).tok.val);
} else if (!(trait is TraitDecl)) {
- Error(cl.TraitId, "identifier '{0}' does not denote a trait", cl.TraitId.val);
+ Error(((UserDefinedType)(cl.TraitTyp)).tok, "identifier '{0}' does not denote a trait", ((UserDefinedType)(cl.TraitTyp)).tok.val);
} else {
//disallowing inheritance in multi module case
string clModName = cl.Module.CompileName.Replace("_Compile", string.Empty);
string traitModName = trait.Module.CompileName.Replace("_Compile", string.Empty);
if (clModName != traitModName) {
- Error(cl.TraitId, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",
+ Error(((UserDefinedType)(cl.TraitTyp)).tok, string.Format("class {0} is in a different module than trait {1}. A class may only extend a trait in the same module",
cl.FullName, trait.FullName));
} else {
- cl.Trait = (TraitDecl)trait;
+ cl.TraitObj = (TraitDecl)trait;
}
}
}
@@ -2730,9 +2731,9 @@ namespace Microsoft.Dafny
Contract.Requires(cl != null);
//merging class members with parent members if any
- if (cl.Trait != null) {
+ if (cl.TraitObj != null) {
var clMembers = classMembers[cl];
- var traitMembers = classMembers[cl.Trait];
+ var traitMembers = classMembers[cl.TraitObj];
//merging current class members with the inheriting trait
foreach (KeyValuePair<string, MemberDecl> traitMem in traitMembers) {
MemberDecl clMember;
@@ -2815,7 +2816,7 @@ namespace Microsoft.Dafny
//checking to make sure all body-less methods/functions have been implemented in the child class
if (refinementTransformer == null)
refinementTransformer = new RefinementTransformer(this, AdditionalInformationReporter, null);
- foreach (MemberDecl traitMember in cl.Trait.Members.Where(mem => mem is Function || mem is Method)) {
+ foreach (MemberDecl traitMember in cl.TraitObj.Members.Where(mem => mem is Function || mem is Method)) {
if (traitMember is Function) {
Function traitFunc = (Function)traitMember;
if (traitFunc.Body == null) //we do this check only if trait function body is null
@@ -4021,9 +4022,9 @@ namespace Microsoft.Dafny
}
return successSoFar;
} else if ((bb.ResolvedClass is ClassDecl) && (aa.ResolvedClass is TraitDecl)) {
- return ((ClassDecl)bb.ResolvedClass).Trait.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;
+ return ((ClassDecl)bb.ResolvedClass).TraitObj.FullCompileName == ((TraitDecl)aa.ResolvedClass).FullCompileName;
} else if ((aa.ResolvedClass is ClassDecl) && (bb.ResolvedClass is TraitDecl)) {
- return ((ClassDecl)aa.ResolvedClass).Trait.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;
+ return ((ClassDecl)aa.ResolvedClass).TraitObj.FullCompileName == ((TraitDecl)bb.ResolvedClass).FullCompileName;
} else if (aa.ResolvedParam != null && aa.ResolvedParam == bb.ResolvedParam) {
// type parameters
if (aa.TypeArgs.Count != bb.TypeArgs.Count) {
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 72a9e752..cdf9eb86 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -509,7 +509,7 @@ namespace Microsoft.Dafny {
{
foreach (ModuleDefinition m in program.Modules)
{
- if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).Trait != null) || (d is TraitDecl)))
+ if (m.TopLevelDecls.Any(d => (d is ClassDecl && ((ClassDecl)d).TraitObj != null) || (d is TraitDecl)))
{
//adding const unique NoTraitAtAll: ClassName;
Token tNoTrait = new Token();
@@ -527,12 +527,12 @@ namespace Microsoft.Dafny {
if (d is ClassDecl)
{
var c = (ClassDecl)d;
- if (c is ClassDecl && c.Trait != null)
+ if (c is ClassDecl && c.TraitObj != null)
{
//this adds: axiom TraitParent(class.A) == class.J; Where A extends J
- Bpl.TypedIdent trait_id = new Bpl.TypedIdent(c.Trait.tok, string.Format("class.{0}", c.Trait.FullSanitizedName), predef.ClassNameType);
- Bpl.Constant trait = new Bpl.Constant(c.Trait.tok, trait_id, true);
- Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(c.Trait.tok, trait);
+ Bpl.TypedIdent trait_id = new Bpl.TypedIdent(c.TraitObj.tok, string.Format("class.{0}", c.TraitObj.FullSanitizedName), predef.ClassNameType);
+ Bpl.Constant trait = new Bpl.Constant(c.TraitObj.tok, trait_id, true);
+ Bpl.Expr traitId_expr = new Bpl.IdentifierExpr(c.TraitObj.tok, trait);
var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), false);
@@ -542,7 +542,7 @@ namespace Microsoft.Dafny {
sink.AddTopLevelDeclaration(traitParentAxiom);
}
- else if (c is ClassDecl && c.Trait == null)
+ else if (c is ClassDecl && c.TraitObj == null)
{
//this adds: axiom TraitParent(class.B) == NoTraitAtAll; Where B does not extend any traits
Bpl.TypedIdent noTraitAtAll_id = new Bpl.TypedIdent(c.tok, "NoTraitAtAll", predef.ClassNameType);
@@ -1325,14 +1325,14 @@ namespace Microsoft.Dafny {
//this adds: axiom implements$J(class.C);
else if (c is ClassDecl)
{
- if (c.Trait != null)
+ if (c.TraitObj != null)
{
//var dtypeFunc = FunctionCall(c.tok, BuiltinFunction.DynamicType, null, o);
//Bpl.Expr implementsFunc = FunctionCall(t.tok, "implements$" + t.Name, Bpl.Type.Bool, new List<Expr> { dtypeFunc });
var args = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, predef.ClassNameType), true);
var ret_value = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + c.TraitId.val, new List<Variable> { args }, ret_value));
+ var funCall = new Bpl.FunctionCall(new Bpl.Function(c.tok, "implements$" + ((UserDefinedType)(c.TraitTyp)).tok, new List<Variable> { args }, ret_value));
var expr = new Bpl.NAryExpr(c.tok, funCall, new List<Expr> { new Bpl.IdentifierExpr(c.tok, string.Format("class.{0}", c.FullSanitizedName), predef.ClassNameType) });
var implements_axiom = new Bpl.Axiom(c.tok, expr);
sink.AddTopLevelDeclaration(implements_axiom);
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 2bda7cf0..16349ccc 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Dafny
public static int ThreadMain(string[] args)
{
Contract.Requires(cce.NonNullElements(args));
-
+
printer = new DafnyConsolePrinter();
ExecutionEngine.printer = printer;
@@ -51,7 +51,7 @@ namespace Microsoft.Dafny
exitValue = ExitValue.PREPROCESSING_ERROR;
goto END;
}
- //CommandLineOptions.Clo.Files = new List<string> { @"C:\dafny\Test\dafny0\Trait\TraitOverride1.dfy" };
+ //CommandLineOptions.Clo.Files = new List<string> { @"C:\dafny\Test\dafny0\Trait\TraitExtend.dfy" };
if (CommandLineOptions.Clo.Files.Count == 0)
{
@@ -109,6 +109,7 @@ namespace Microsoft.Dafny
// TODO(wuestholz): We should probably add a separate flag for this. This is currently only used by the new testing infrastructure.
return 0;
}
+ //Console.ReadKey();
return (int)exitValue;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 16:58:36 +0000