summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-06-11 16:45:21 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-06-11 16:45:21 -0700
commit84cd85ffd3c722278eb22d0bf402caf0f717a150 (patch)
treed990fd3227548f40cd99d81d2d285775c49c6ed1
parentf83bee27aa1b0de0659f39d7fcd27121ecbef755 (diff)
Dafny: allow types to be qualified with the name of the module that declares them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member)
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg25
-rw-r--r--Source/Dafny/DafnyAst.cs11
-rw-r--r--Source/Dafny/Parser.cs176
-rw-r--r--Source/Dafny/RefinementTransformer.cs2
-rw-r--r--Source/Dafny/Resolver.cs35
-rw-r--r--Source/Dafny/Scanner.cs30
-rw-r--r--Source/Dafny/Translator.cs2
-rw-r--r--Test/dafny0/Answer23
-rw-r--r--Test/dafny0/Modules0.dfy28
-rw-r--r--Test/dafny0/Modules1.dfy20
10 files changed, 239 insertions, 113 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 02685fd1..195495aa 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -507,6 +507,7 @@ TypeAndToken<out IToken/*!*/ tok, out Type/*!*/ ty>
ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
= (. Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ IToken moduleName = null;
List<Type/*!*/>/*!*/ gt;
.)
( "object" (. tok = t; ty = new ObjectType(); .)
@@ -521,7 +522,10 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty>
ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
.)
| Ident<out tok> (. gt = new List<Type/*!*/>(); .)
- [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
+ [ (. moduleName = tok; .)
+ "." Ident<out tok>
+ ]
+ [ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt, moduleName); .)
)
.
GenericInstantiation<.List<Type/*!*/>/*!*/ gt.>
@@ -765,8 +769,23 @@ Rhs<out AssignmentRhs r, Expression receiverForInitCall>
| "." Ident<out x>
"(" (. args = new List<Expression/*!*/>(); .)
[ Expressions<args> ]
- ")" (. initCall = new CallStmt(x, new List<Expression>(),
- receiverForInitCall, x.val, args); .)
+ ")" (. initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args); .)
+ | "(" (. var udf = ty as UserDefinedType;
+ if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {
+ // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as
+ // the name of the constructor that's being invoked.
+ x = udf.tok;
+ ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);
+ } else {
+ SemErr(t, "expected '.'");
+ x = null;
+ }
+ args = new List<Expression/*!*/>(); .)
+ [ Expressions<args> ]
+ ")" (. if (x != null) {
+ initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
+ }
+ .)
]
(. if (ee != null) {
r = new TypeRhs(newToken, ty, ee);
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index fd58835c..95110629 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -54,7 +54,7 @@ namespace Microsoft.Dafny {
List<Type/*!*/> typeArgs = new List<Type/*!*/>();
typeArgs.Add(arg);
- UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs);
+ UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs, null);
if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);
for (int d = 0; d < dims; d++) {
@@ -393,7 +393,8 @@ namespace Microsoft.Dafny {
Contract.Invariant(cce.NonNullElements(TypeArgs));
}
- public readonly IToken tok;
+ public readonly IToken ModuleName; // may be null
+ public readonly IToken tok; // token of the Name
public readonly string Name;
[Rep]
public readonly List<Type/*!*/>/*!*/ TypeArgs;
@@ -411,10 +412,11 @@ namespace Microsoft.Dafny {
public TopLevelDecl ResolvedClass; // filled in by resolution, if Name denotes a class/datatype and TypeArgs match the type parameters of that class/datatype
public TypeParameter ResolvedParam; // filled in by resolution, if Name denotes an enclosing type parameter and TypeArgs is the empty list
- public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs) {
+ public UserDefinedType(IToken/*!*/ tok, string/*!*/ name, [Captured] List<Type/*!*/>/*!*/ typeArgs, IToken moduleName) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
+ this.ModuleName = moduleName;
this.tok = tok;
this.Name = name;
this.TypeArgs = typeArgs;
@@ -480,6 +482,9 @@ namespace Microsoft.Dafny {
Contract.Ensures(Contract.Result<string>() != null);
string s = Name;
+ if (ModuleName != null) {
+ s = ModuleName.val + "." + s;
+ }
if (TypeArgs.Count != 0) {
string sep = "<";
foreach (Type t in TypeArgs) {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index f3ac7f54..52bbc90c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -405,7 +405,7 @@ bool IsAttribute() {
}
if (la.kind == 19) {
FieldDecl(mmod, mm);
- } else if (la.kind == 43 || la.kind == 44) {
+ } else if (la.kind == 44 || la.kind == 45) {
FunctionDecl(mmod, out f);
mm.Add(f);
} else if (la.kind == 24 || la.kind == 25) {
@@ -470,7 +470,7 @@ bool IsAttribute() {
IToken bodyEnd = Token.NoToken;
bool signatureOmitted = false;
- if (la.kind == 43) {
+ if (la.kind == 44) {
Get();
if (la.kind == 24) {
Get();
@@ -494,7 +494,7 @@ bool IsAttribute() {
signatureOmitted = true;
openParen = Token.NoToken;
} else SynErr(117);
- } else if (la.kind == 44) {
+ } else if (la.kind == 45) {
Get();
isPredicate = true;
if (la.kind == 24) {
@@ -885,7 +885,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void FrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null;
Expression(out e);
- if (la.kind == 47) {
+ if (la.kind == 48) {
Get();
Ident(out id);
fieldName = id.val;
@@ -934,6 +934,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void ReferenceType(out IToken/*!*/ tok, out Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/
+ IToken moduleName = null;
List<Type/*!*/>/*!*/ gt;
if (la.kind == 42) {
@@ -955,10 +956,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
} else if (la.kind == 1) {
Ident(out tok);
gt = new List<Type/*!*/>();
+ if (la.kind == 43) {
+ moduleName = tok;
+ Get();
+ Ident(out tok);
+ }
if (la.kind == 22) {
GenericInstantiation(gt);
}
- ty = new UserDefinedType(tok, tok.val, gt);
+ ty = new UserDefinedType(tok, tok.val, gt, moduleName);
} else SynErr(131);
}
@@ -972,7 +978,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (!(la.kind == 0 || la.kind == 18)) {SynErr(133); Get();}
Expect(18);
reqs.Add(e);
- } else if (la.kind == 45) {
+ } else if (la.kind == 46) {
Get();
if (StartOf(11)) {
PossiblyWildFrameExpression(out fe);
@@ -1010,7 +1016,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void PossiblyWildFrameExpression(out FrameExpression/*!*/ fe) {
Contract.Ensures(Contract.ValueAtReturn(out fe) != null); fe = dummyFrameExpr;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
fe = new FrameExpression(new WildcardExpr(t), null);
} else if (StartOf(9)) {
@@ -1021,7 +1027,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void PossiblyWildExpression(out Expression/*!*/ e) {
Contract.Ensures(Contract.ValueAtReturn(out e)!=null);
e = dummyExpr;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
e = new WildcardExpr(t);
} else if (StartOf(9)) {
@@ -1086,7 +1092,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
ParallelStmt(out s);
break;
}
- case 48: {
+ case 49: {
Get();
x = t;
Ident(out id);
@@ -1095,14 +1101,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s.Labels = new LList<Label>(new Label(x, id.val), s.Labels);
break;
}
- case 49: {
+ case 50: {
Get();
x = t; breakCount = 1; label = null;
if (la.kind == 1) {
Ident(out id);
label = id.val;
- } else if (la.kind == 18 || la.kind == 49) {
- while (la.kind == 49) {
+ } else if (la.kind == 18 || la.kind == 50) {
+ while (la.kind == 50) {
Get();
breakCount++;
}
@@ -1112,7 +1118,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount);
break;
}
- case 50: {
+ case 51: {
ReturnStmt(out s);
break;
}
@@ -1192,14 +1198,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(18);
rhss.Add(new ExprRhs(e, attrs));
- } else if (la.kind == 20 || la.kind == 51 || la.kind == 52) {
+ } else if (la.kind == 20 || la.kind == 52 || la.kind == 53) {
lhss.Add(e); lhs0 = e;
while (la.kind == 20) {
Get();
Lhs(out e);
lhss.Add(e);
}
- if (la.kind == 51) {
+ if (la.kind == 52) {
Get();
x = t;
Rhs(out r, lhs0);
@@ -1209,7 +1215,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Rhs(out r, lhs0);
rhss.Add(r);
}
- } else if (la.kind == 52) {
+ } else if (la.kind == 53) {
Get();
x = t;
Expression(out suchThat);
@@ -1248,8 +1254,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
LocalIdentTypeOptional(out d, isGhost);
lhss.Add(d);
}
- if (la.kind == 51 || la.kind == 52) {
- if (la.kind == 51) {
+ if (la.kind == 52 || la.kind == 53) {
+ if (la.kind == 52) {
Get();
assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
@@ -1446,7 +1452,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<AssignmentRhs> rhss = null;
AssignmentRhs r;
- Expect(50);
+ Expect(51);
returnTok = t;
if (StartOf(14)) {
Rhs(out r, null);
@@ -1470,19 +1476,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
r = null; // to please compiler
Attributes attrs = null;
- if (la.kind == 53) {
+ if (la.kind == 54) {
Get();
newToken = t;
TypeAndToken(out x, out ty);
- if (la.kind == 54 || la.kind == 56) {
- if (la.kind == 54) {
+ if (la.kind == 33 || la.kind == 43 || la.kind == 55) {
+ if (la.kind == 55) {
Get();
ee = new List<Expression>();
Expressions(ee);
- Expect(55);
+ Expect(56);
UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
- } else {
+ } else if (la.kind == 43) {
Get();
Ident(out x);
Expect(33);
@@ -1491,8 +1497,28 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expressions(args);
}
Expect(34);
- initCall = new CallStmt(x, new List<Expression>(),
- receiverForInitCall, x.val, args);
+ initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
+ } else {
+ Get();
+ var udf = ty as UserDefinedType;
+ if (udf != null && udf.ModuleName != null && udf.TypeArgs.Count == 0) {
+ // The parsed name had the form "A.B", so treat "A" as the name of the type and "B" as
+ // the name of the constructor that's being invoked.
+ x = udf.tok;
+ ty = new UserDefinedType(udf.ModuleName, udf.ModuleName.val, new List<Type>(), null);
+ } else {
+ SemErr(t, "expected '.'");
+ x = null;
+ }
+ args = new List<Expression/*!*/>();
+ if (StartOf(9)) {
+ Expressions(args);
+ }
+ Expect(34);
+ if (x != null) {
+ initCall = new CallStmt(x, new List<Expression>(), receiverForInitCall, x.val, args);
+ }
+
}
}
if (ee != null) {
@@ -1506,7 +1532,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
Expression(out e);
r = new ExprRhs(new UnaryExpr(x, UnaryExpr.Opcode.SetChoose, e));
- } else if (la.kind == 46) {
+ } else if (la.kind == 47) {
Get();
r = new HavocRhs(t);
} else if (StartOf(9)) {
@@ -1524,13 +1550,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (la.kind == 1) {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 54 || la.kind == 56) {
+ while (la.kind == 43 || la.kind == 55) {
Suffix(ref e);
}
} else if (StartOf(15)) {
ConstAtomExpression(out e);
Suffix(ref e);
- while (la.kind == 54 || la.kind == 56) {
+ while (la.kind == 43 || la.kind == 55) {
Suffix(ref e);
}
} else SynErr(152);
@@ -1550,7 +1576,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Guard(out Expression e) {
Expression/*!*/ ee; e = null;
Expect(33);
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
e = null;
} else if (StartOf(9)) {
@@ -1971,7 +1997,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 46 || la.kind == 89 || la.kind == 90) {
+ while (la.kind == 47 || la.kind == 89 || la.kind == 90) {
MulOp(out x, out op);
UnaryExpression(out e1);
e0 = new BinaryExpr(x, op, e0, e1);
@@ -2012,12 +2038,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
case 1: {
DottedIdentifiersAndFunction(out e);
- while (la.kind == 54 || la.kind == 56) {
+ while (la.kind == 43 || la.kind == 55) {
Suffix(ref e);
}
break;
}
- case 6: case 54: {
+ case 6: case 55: {
DisplayExpr(out e);
break;
}
@@ -2031,7 +2057,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
case 2: case 17: case 33: case 92: case 93: case 94: case 95: case 96: case 97: case 98: {
ConstAtomExpression(out e);
- while (la.kind == 54 || la.kind == 56) {
+ while (la.kind == 43 || la.kind == 55) {
Suffix(ref e);
}
break;
@@ -2042,7 +2068,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- if (la.kind == 46) {
+ if (la.kind == 47) {
Get();
x = t; op = BinaryExpr.Opcode.Mul;
} else if (la.kind == 89) {
@@ -2123,7 +2149,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
IdentTypeOptional(out d);
letVars.Add(d);
}
- Expect(51);
+ Expect(52);
Expression(out e);
letRHSs.Add(e);
while (la.kind == 20) {
@@ -2147,7 +2173,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Ident(out id);
idents.Add(id);
- while (la.kind == 56) {
+ while (la.kind == 43) {
Get();
Ident(out id);
idents.Add(id);
@@ -2169,7 +2195,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<Expression> multipleIndices = null;
bool func = false;
- if (la.kind == 56) {
+ if (la.kind == 43) {
Get();
Ident(out id);
if (la.kind == 33) {
@@ -2182,7 +2208,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new FunctionCallExpr(id, id.val, e, openParen, args);
}
if (!func) { e = new ExprDotName(id, e, id.val); }
- } else if (la.kind == 54) {
+ } else if (la.kind == 55) {
Get();
x = t;
if (StartOf(9)) {
@@ -2195,11 +2221,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression(out ee);
e1 = ee;
}
- } else if (la.kind == 51) {
+ } else if (la.kind == 52) {
Get();
Expression(out ee);
e1 = ee;
- } else if (la.kind == 20 || la.kind == 55) {
+ } else if (la.kind == 20 || la.kind == 56) {
while (la.kind == 20) {
Get();
Expression(out ee);
@@ -2241,7 +2267,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
- Expect(55);
+ Expect(56);
} else SynErr(173);
}
@@ -2258,14 +2284,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
e = new SetDisplayExpr(x, elements);
Expect(7);
- } else if (la.kind == 54) {
+ } else if (la.kind == 55) {
Get();
x = t; elements = new List<Expression/*!*/>();
if (StartOf(9)) {
Expressions(elements);
}
e = new SeqDisplayExpr(x, elements);
- Expect(55);
+ Expect(56);
} else SynErr(174);
}
@@ -2303,14 +2329,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expect(41);
x = t;
- if (la.kind == 54) {
+ if (la.kind == 55) {
Get();
elements = new List<ExpressionPair/*!*/>();
if (StartOf(9)) {
MapLiteralExpressions(out elements);
}
e = new MapDisplayExpr(x, elements);
- Expect(55);
+ Expect(56);
} else if (la.kind == 1) {
BoundVar/*!*/ bv;
List<BoundVar/*!*/> bvars = new List<BoundVar/*!*/>();
@@ -2422,13 +2448,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression/*!*/ d, r;
elements = new List<ExpressionPair/*!*/>();
Expression(out d);
- Expect(51);
+ Expect(52);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
while (la.kind == 20) {
Get();
Expression(out d);
- Expect(51);
+ Expect(52);
Expression(out r);
elements.Add(new ExpressionPair(d,r));
}
@@ -2584,27 +2610,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
static readonly bool[,]/*!*/ set = {
- {T,T,T,x, x,x,T,x, T,x,x,x, T,x,T,T, x,T,T,T, x,x,x,x, T,T,x,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,T,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, 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,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,x,x,x, x,x,x,x, T,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,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},
- {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,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},
+ {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,x,x, x,x,T,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, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,T,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, T,T,T,T, x,x,x,T, x,T,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, x,x,x,T, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {T,x,x,x, x,x,T,T, T,T,x,x, T,T,T,T, x,x,x,T, x,T,T,x, T,T,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, 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, T,T,T,x, x,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, 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, T,T,T,x, x,x,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x, x,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, 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,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, 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,x,x, x,x,T,x, x,x,T,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
- {x,T,T,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,T,x, x,x,x,x, x,T,T,x, x,T,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, 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, 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, x,T,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, 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,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,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,T,T, x,x,x,T, x,x,x,T, x,x,x,T, T,T,x,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, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, 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,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, T,x,x,T, T,T,x,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,x,T, x,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, T,x,x,T, T,T,T,T, T,T,T,x, x,T,T,T, T,x,x,x, x}
};
} // end Parser
@@ -2672,20 +2698,20 @@ public class Errors {
case 40: s = "\"seq\" expected"; break;
case 41: s = "\"map\" expected"; break;
case 42: s = "\"object\" expected"; break;
- case 43: s = "\"function\" expected"; break;
- case 44: s = "\"predicate\" expected"; break;
- case 45: s = "\"reads\" expected"; break;
- case 46: s = "\"*\" expected"; break;
- case 47: s = "\"`\" expected"; break;
- case 48: s = "\"label\" expected"; break;
- case 49: s = "\"break\" expected"; break;
- case 50: s = "\"return\" expected"; break;
- case 51: s = "\":=\" expected"; break;
- case 52: s = "\":|\" expected"; break;
- case 53: s = "\"new\" expected"; break;
- case 54: s = "\"[\" expected"; break;
- case 55: s = "\"]\" expected"; break;
- case 56: s = "\".\" expected"; break;
+ case 43: s = "\".\" expected"; break;
+ case 44: s = "\"function\" expected"; break;
+ case 45: s = "\"predicate\" expected"; break;
+ case 46: s = "\"reads\" expected"; break;
+ case 47: s = "\"*\" expected"; break;
+ case 48: s = "\"`\" expected"; break;
+ case 49: s = "\"label\" expected"; break;
+ case 50: s = "\"break\" expected"; break;
+ case 51: s = "\"return\" expected"; break;
+ case 52: s = "\":=\" expected"; break;
+ case 53: s = "\":|\" expected"; break;
+ case 54: s = "\"new\" expected"; break;
+ case 55: s = "\"[\" expected"; break;
+ case 56: s = "\"]\" expected"; break;
case 57: s = "\"choose\" expected"; break;
case 58: s = "\"if\" expected"; break;
case 59: s = "\"else\" expected"; break;
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs
index 5c607804..ba3cae19 100644
--- a/Source/Dafny/RefinementTransformer.cs
+++ b/Source/Dafny/RefinementTransformer.cs
@@ -198,7 +198,7 @@ namespace Microsoft.Dafny {
return new MapType(CloneType(tt.Domain), CloneType(tt.Range));
} else if (t is UserDefinedType) {
var tt = (UserDefinedType)t;
- return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType));
+ return new UserDefinedType(Tok(tt.tok), tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.ModuleName == null ? null : Tok(tt.ModuleName));
} else if (t is InferredTypeProxy) {
return new InferredTypeProxy();
} else {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 23cf892e..6cf215d6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -937,7 +937,7 @@ namespace Microsoft.Dafny {
Error(t.tok, "sorry, cannot instantiate type parameter with a subrange type");
}
}
- TypeParameter tp = allTypeParameters.Find(t.Name);
+ TypeParameter tp = t.ModuleName == null ? allTypeParameters.Find(t.Name) : null;
if (tp != null) {
if (t.TypeArgs.Count == 0) {
t.ResolvedParam = tp;
@@ -945,11 +945,32 @@ namespace Microsoft.Dafny {
Error(t.tok, "Type parameter expects no type arguments: {0}", t.Name);
}
} 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;
- if (!classes.TryGetValue(t.Name, out d)) {
+ 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;
+ }
+ }
+ Error(t.ModuleName, "Undeclared module name: {0} (did you forget a module import?)", t.ModuleName.val);
+ DONE_WITH_QUALIFIED_NAME: ;
+ } else if (!classes.TryGetValue(t.Name, out d)) {
Error(t.tok, "Undeclared top-level type or type parameter: {0} (did you forget a module import?)", t.Name);
+ }
+
+ if (d == null) {
+ // error has been reported above
} else if (d is AmbiguousTopLevelDecl) {
- Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1}", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());
+ Error(t.tok, "The name {0} ambiguously refers to a type in one of the modules {1} (try qualifying the type name with the module name)", t.Name, ((AmbiguousTopLevelDecl)d).ModuleNames());
} else if (d is ArbitraryTypeDecl) {
t.ResolvedParam = ((ArbitraryTypeDecl)d).TheType; // resolve like a type parameter
} else {
@@ -973,7 +994,7 @@ namespace Microsoft.Dafny {
Contract.Assert(d.TypeArgs.Count <= defaultTypeArguments.Count);
// automatically supply a prefix of the arguments from defaultTypeArguments
for (int i = 0; i < d.TypeArgs.Count; i++) {
- var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List<Type>());
+ var typeArg = new UserDefinedType(t.tok, defaultTypeArguments[i].Name, new List<Type>(), null);
typeArg.ResolvedParam = defaultTypeArguments[i]; // resolve "typeArg" here
t.TypeArgs.Add(typeArg);
}
@@ -2339,7 +2360,7 @@ namespace Microsoft.Dafny {
}
if (!callsConstructor && rr.EType is UserDefinedType) {
var udt = (UserDefinedType)rr.EType;
- var cl = (ClassDecl)udt.ResolvedClass; // cast is guarantted by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test
+ var cl = (ClassDecl)udt.ResolvedClass; // cast is guaranteed by the call to rr.EType.IsRefType above, together with the "rr.EType is UserDefinedType" test
if (cl.HasConstructor) {
Error(stmt, "when allocating an object of type '{0}', one of its constructor methods must be called", cl.Name);
}
@@ -2595,7 +2616,7 @@ namespace Microsoft.Dafny {
dtv.InferredTypeArgs.Add(t);
subst.Add(dt.TypeArgs[i], t);
}
- expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt);
+ expr.Type = new UserDefinedType(dtv.tok, dtv.DatatypeName, gt, null);
ResolveType(expr.tok, expr.Type, null, true);
DatatypeCtor ctor;
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 2f9ac694..2388716b 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -514,13 +514,13 @@ public class Scanner {
case "seq": t.kind = 40; break;
case "map": t.kind = 41; break;
case "object": t.kind = 42; break;
- case "function": t.kind = 43; break;
- case "predicate": t.kind = 44; break;
- case "reads": t.kind = 45; break;
- case "label": t.kind = 48; break;
- case "break": t.kind = 49; break;
- case "return": t.kind = 50; break;
- case "new": t.kind = 53; break;
+ case "function": t.kind = 44; break;
+ case "predicate": t.kind = 45; break;
+ case "reads": t.kind = 46; break;
+ case "label": t.kind = 49; break;
+ case "break": t.kind = 50; break;
+ case "return": t.kind = 51; break;
+ case "new": t.kind = 54; break;
case "choose": t.kind = 57; break;
case "if": t.kind = 58; break;
case "else": t.kind = 59; break;
@@ -658,17 +658,17 @@ public class Scanner {
case 23:
{t.kind = 34; break;}
case 24:
- {t.kind = 46; break;}
- case 25:
{t.kind = 47; break;}
+ case 25:
+ {t.kind = 48; break;}
case 26:
- {t.kind = 51; break;}
- case 27:
{t.kind = 52; break;}
+ case 27:
+ {t.kind = 53; break;}
case 28:
- {t.kind = 54; break;}
- case 29:
{t.kind = 55; break;}
+ case 29:
+ {t.kind = 56; break;}
case 30:
{t.kind = 61; break;}
case 31:
@@ -747,9 +747,9 @@ public class Scanner {
if (ch == '=') {AddCh(); goto case 41;}
else {t.kind = 23; break;}
case 61:
- recEnd = pos; recKind = 56;
+ recEnd = pos; recKind = 43;
if (ch == '.') {AddCh(); goto case 65;}
- else {t.kind = 56; break;}
+ else {t.kind = 43; break;}
case 62:
recEnd = pos; recKind = 83;
if (ch == '=') {AddCh(); goto case 42;}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 07583edd..2325734f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -666,7 +666,7 @@ namespace Microsoft.Dafny {
// create and resolve datatype value
var r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);
r.Ctor = mc.Ctor;
- r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);
+ r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/, null);
Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
substMap.Add(formal, r);
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c451cc62..be41fbf8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -712,13 +712,13 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA
Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M
-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
+Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)
-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M
+Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)
Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
@@ -730,13 +730,20 @@ Modules0.dfy(250,15): Error: unresolved identifier: X
Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X
Modules0.dfy(294,16): Error: member R does not exist in class B
Modules0.dfy(294,6): Error: expected method call, found expression
+Modules0.dfy(317,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
+Modules0.dfy(321,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
+Modules0.dfy(322,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
+Modules0.dfy(323,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
+Modules0.dfy(324,17): Error: Undeclared class name Edon in module Q_Imp
+Modules0.dfy(326,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
+Modules0.dfy(327,30): Error: member Create does not exist in class Klassy
Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts
Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts
Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts
Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts
Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context
Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context
-30 resolution/type errors detected in Modules0.dfy
+37 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(74,16): Error: assertion violation
@@ -758,7 +765,7 @@ Modules1.dfy(58,3): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 19 verified, 5 errors
+Dafny program verifier finished with 22 verified, 5 errors
-------------------- BadFunction.dfy --------------------
BadFunction.dfy(6,3): Error: failure to decrease termination measure
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index b171a9c9..cc66c3c1 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -301,3 +301,31 @@ module Local imports NonLocalA, NonLocalB {
method Q() { }
}
}
+
+// ------ qualified type names ----------------------------------
+
+module Q_Imp {
+ class Node { }
+ datatype List<T> = Nil | Cons(T, List);
+ class Klassy {
+ method Init()
+ }
+}
+
+module Q_M imports Q_Imp {
+ method MyMethod(root: Q_Imp.Node, S: set<Node>)
+ requires root in S; // error: the element type of S does not agree with the type of root
+ {
+ var i := new Q_Imp.Node;
+ var j := new Node;
+ assert i != j; // error: i and j have different types
+ var k: LongLostModule.Node; // error: undeclared module
+ var l: Wazzup.WazzupA; // error: undeclared module (it has not been imported)
+ var m: Q_Imp.Edon; // error: undeclared class in module Q_Imp
+ var n: Q_Imp.List;
+ var o := new Q_Imp.List; // error: not a class declared in module Q_Imp
+ var p := new Q_Imp.Klassy.Create(); // error: Create is not a method
+ var q := new Q_Imp.Klassy.Init();
+ }
+ class Node { }
+}
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 5e2d0fff..e8a88749 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -89,3 +89,23 @@ module B_Visibility imports A_Visibility {
}
}
}
+
+// ------ qualified type names ----------------------------------
+
+module Q_Imp {
+ class Node { }
+ class Klassy {
+ method Init()
+ }
+}
+
+module Q_M imports Q_Imp {
+ method MyMethod(root: Q_Imp.Node, S: set<Q_Imp.Node>)
+ requires root in S;
+ {
+ var i := new Q_Imp.Node;
+ var j := new Node;
+ assert i != j; // fine
+ var q := new Q_Imp.Klassy.Init();
+ }
+}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 11:11:29 +0000