diff options
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 56 |
1 files changed, 27 insertions, 29 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 220b5561..fcd6e637 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -1672,8 +1672,6 @@ namespace Microsoft.Dafny { // ...
// }
if (s.Cases.Count != 0) {
- var sourceType = (UserDefinedType)s.Source.Type;
-
SpillLetVariableDecls(s.Source, indent);
string source = "_source" + tmpVarCount;
tmpVarCount++;
@@ -1683,6 +1681,7 @@ namespace Microsoft.Dafny { wr.WriteLine(";");
int i = 0;
+ var sourceType = (UserDefinedType)s.Source.Type.NormalizeExpand();
foreach (MatchCaseStmt mc in s.Cases) {
MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, s.Cases.Count, indent);
TrStmtList(mc.Body, indent);
@@ -1956,7 +1955,7 @@ namespace Microsoft.Dafny { if (tp.ArrayDimensions == null) {
wr.Write("new {0}()", TypeName(tp.EType));
} else {
- if (tp.EType is IntType || tp.EType.IsTypeParameter) {
+ if (tp.EType.IsIntegerType || tp.EType.IsTypeParameter) {
// Because the default constructor for BigInteger does not generate a valid BigInteger, we have
// to excplicitly initialize the elements of an integer array. This is all done in a helper routine.
wr.Write("Dafny.Helpers.InitNewArray{0}<{1}>", tp.ArrayDimensions.Count, TypeName(tp.EType));
@@ -2138,24 +2137,24 @@ namespace Microsoft.Dafny { wr.Write(enclosingMethod != null && enclosingMethod.IsTailRecursive ? "_this" : "this");
} else if (expr is IdentifierExpr) {
- IdentifierExpr e = (IdentifierExpr)expr;
+ var e = (IdentifierExpr)expr;
wr.Write("@" + e.Var.CompileName);
} else if (expr is SetDisplayExpr) {
- SetDisplayExpr e = (SetDisplayExpr)expr;
- Type elType = cce.NonNull((SetType)e.Type).Arg;
+ var e = (SetDisplayExpr)expr;
+ var elType = e.Type.AsSetType.Arg;
wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));
TrExprList(e.Elements);
} else if (expr is MultiSetDisplayExpr) {
- MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
- Type elType = cce.NonNull((MultiSetType)e.Type).Arg;
+ var e = (MultiSetDisplayExpr)expr;
+ var elType = e.Type.AsMultiSetType.Arg;
wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));
TrExprList(e.Elements);
} else if (expr is SeqDisplayExpr) {
- SeqDisplayExpr e = (SeqDisplayExpr)expr;
- Type elType = cce.NonNull((SeqType)e.Type).Arg;
+ var e = (SeqDisplayExpr)expr;
+ var elType = e.Type.AsSeqType.Arg;
wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
TrExprList(e.Elements);
@@ -2210,11 +2209,12 @@ namespace Microsoft.Dafny { }
}
} else if (expr is MultiSetFormingExpr) {
- MultiSetFormingExpr e = (MultiSetFormingExpr)expr;
- wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(((CollectionType)e.E.Type).Arg));
- if (e.E.Type is SeqType) {
+ var e = (MultiSetFormingExpr)expr;
+ wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(e.E.Type.AsCollectionType.Arg));
+ var eeType = e.E.Type.NormalizeExpand();
+ if (eeType is SeqType) {
TrParenExpr(".FromSeq", e.E);
- } else if (e.E.Type is SetType) {
+ } else if (eeType is SetType) {
TrParenExpr(".FromSet", e.E);
} else {
Contract.Assert(false); throw new cce.UnreachableException();
@@ -2334,7 +2334,7 @@ namespace Microsoft.Dafny { TrParenExpr(e.E);
break;
case UnaryOpExpr.Opcode.Cardinality:
- if (cce.NonNull(e.E.Type).IsArrayType) {
+ if (e.E.Type.IsArrayType) {
wr.Write("new BigInteger(");
TrParenExpr(e.E);
wr.Write(".Length)");
@@ -2350,11 +2350,11 @@ namespace Microsoft.Dafny { } else if (expr is ConversionExpr) {
var e = (ConversionExpr)expr;
if (e.ToType is IntType) {
- Contract.Assert(e.E.Type is RealType);
+ Contract.Assert(e.E.Type.IsRealType);
TrParenExpr(e.E);
wr.Write(".ToBigInteger()");
} else if (e.ToType is RealType) {
- Contract.Assert(e.E.Type is IntType);
+ Contract.Assert(e.E.Type.IsIntegerType);
wr.Write("new Dafny.BigRational(");
TrExpr(e.E);
wr.Write(", BigInteger.One)");
@@ -2379,10 +2379,9 @@ namespace Microsoft.Dafny { opString = "&&"; break;
case BinaryExpr.ResolvedOpcode.EqCommon: {
- Type t = cce.NonNull(e.E0.Type);
- if (t.IsDatatype || t.IsTypeParameter) {
+ if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) {
callString = "Equals";
- } else if (t.IsRefType) {
+ } else if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
@@ -2393,11 +2392,10 @@ namespace Microsoft.Dafny { break;
}
case BinaryExpr.ResolvedOpcode.NeqCommon: {
- Type t = cce.NonNull(e.E0.Type);
- if (t.IsDatatype || t.IsTypeParameter) {
+ if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) {
preOpString = "!";
callString = "Equals";
- } else if (t.IsRefType) {
+ } else if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
// For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
// type parameter.
@@ -2423,7 +2421,7 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.Mul:
opString = "*"; break;
case BinaryExpr.ResolvedOpcode.Div:
- if (expr.Type is IntType) {
+ if (expr.Type.IsIntegerType) {
wr.Write("Dafny.Helpers.EuclideanDivision(");
TrParenExpr(e.E0);
wr.Write(", ");
@@ -2434,7 +2432,7 @@ namespace Microsoft.Dafny { }
break;
case BinaryExpr.ResolvedOpcode.Mod:
- if (expr.Type is IntType) {
+ if (expr.Type.IsIntegerType) {
wr.Write("Dafny.Helpers.EuclideanModulus(");
TrParenExpr(e.E0);
wr.Write(", ");
@@ -2589,7 +2587,7 @@ namespace Microsoft.Dafny { wr.Write("throw new System.Exception();");
} else {
int i = 0;
- var sourceType = (UserDefinedType)e.Source.Type;
+ var sourceType = (UserDefinedType)e.Source.Type.NormalizeExpand();
foreach (MatchCaseExpr mc in e.Cases) {
MatchCasePrelude(source, sourceType, cce.NonNull(mc.Ctor), mc.Arguments, i, e.Cases.Count, 0);
wr.Write("return ");
@@ -2672,7 +2670,7 @@ namespace Microsoft.Dafny { // return Dafny.Set<G>.FromCollection(_coll);
// })()
Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
- var typeName = TypeName(((SetType)e.Type).Arg);
+ var typeName = TypeName(e.Type.AsSetType.Arg);
wr.Write("((Dafny.Helpers.ComprehensionDelegate<{0}>)delegate() {{ ", typeName);
wr.Write("var _coll = new System.Collections.Generic.List<{0}>(); ", typeName);
var n = e.BoundVars.Count;
@@ -2741,8 +2739,8 @@ namespace Microsoft.Dafny { // return Dafny.Map<U, V>.FromElements(_coll);
// })()
Contract.Assert(e.Bounds != null); // the resolver would have insisted on finding bounds
- var domtypeName = TypeName(((MapType)e.Type).Domain);
- var rantypeName = TypeName(((MapType)e.Type).Range);
+ var domtypeName = TypeName(e.Type.AsMapType.Domain);
+ var rantypeName = TypeName(e.Type.AsMapType.Range);
wr.Write("((Dafny.Helpers.MapComprehensionDelegate<{0},{1}>)delegate() {{ ", domtypeName, rantypeName);
wr.Write("var _coll = new System.Collections.Generic.List<Dafny.Pair<{0},{1}>>(); ", domtypeName, rantypeName);
var n = e.BoundVars.Count;
|