summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
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-16 20:33:07 +0000