From 9373ad40d67f494609ef55d2c202d698421c9393 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 10 Aug 2012 18:16:32 -0700 Subject: Dafny: internal renaming --- Dafny/Compiler.cs | 80 +++++++++++++++++++++++++++---------------------------- 1 file changed, 40 insertions(+), 40 deletions(-) (limited to 'Dafny/Compiler.cs') diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 57623068..18721cf3 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -1160,11 +1160,11 @@ namespace Microsoft.Dafny { var ind = indent + i * IndentAmount; var bound = s.Bounds[i]; var bv = s.BoundVars[i]; - if (bound is QuantifierExpr.BoolBoundedPool) { + if (bound is ComprehensionExpr.BoolBoundedPool) { Indent(ind); wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName); - } else if (bound is QuantifierExpr.IntBoundedPool) { - var b = (QuantifierExpr.IntBoundedPool)bound; + } else if (bound is ComprehensionExpr.IntBoundedPool) { + var b = (ComprehensionExpr.IntBoundedPool)bound; SpillLetVariableDecls(b.LowerBound, ind); SpillLetVariableDecls(b.UpperBound, ind); Indent(ind); @@ -1173,22 +1173,22 @@ namespace Microsoft.Dafny { wr.Write("; @{0} < ", bv.CompileName); TrExpr(b.UpperBound); wr.Write("; @{0}++) {{ ", bv.CompileName); - } else if (bound is QuantifierExpr.SetBoundedPool) { - var b = (QuantifierExpr.SetBoundedPool)bound; + } else if (bound is ComprehensionExpr.SetBoundedPool) { + var b = (ComprehensionExpr.SetBoundedPool)bound; SpillLetVariableDecls(b.Set, ind); Indent(ind); wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Set); wr.Write(").Elements) { "); - } else if (bound is QuantifierExpr.SeqBoundedPool) { - var b = (QuantifierExpr.SeqBoundedPool)bound; + } else if (bound is ComprehensionExpr.SeqBoundedPool) { + var b = (ComprehensionExpr.SeqBoundedPool)bound; SpillLetVariableDecls(b.Seq, ind); Indent(ind); wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Seq); wr.Write(").UniqueElements) { "); - } else if (bound is QuantifierExpr.DatatypeBoundedPool) { - var b = (QuantifierExpr.DatatypeBoundedPool)bound; + } else if (bound is ComprehensionExpr.DatatypeBoundedPool) { + var b = (ComprehensionExpr.DatatypeBoundedPool)bound; wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type)); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type @@ -2053,32 +2053,32 @@ namespace Microsoft.Dafny { var bound = e.Bounds[i]; var bv = e.BoundVars[i]; // emit: Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body) - if (bound is QuantifierExpr.BoolBoundedPool) { + if (bound is ComprehensionExpr.BoolBoundedPool) { wr.Write("Dafny.Helpers.QuantBool("); - } else if (bound is QuantifierExpr.IntBoundedPool) { - var b = (QuantifierExpr.IntBoundedPool)bound; + } else if (bound is ComprehensionExpr.IntBoundedPool) { + var b = (ComprehensionExpr.IntBoundedPool)bound; wr.Write("Dafny.Helpers.QuantInt("); TrExpr(b.LowerBound); wr.Write(", "); TrExpr(b.UpperBound); wr.Write(", "); - } else if (bound is QuantifierExpr.SetBoundedPool) { - var b = (QuantifierExpr.SetBoundedPool)bound; + } else if (bound is ComprehensionExpr.SetBoundedPool) { + var b = (ComprehensionExpr.SetBoundedPool)bound; wr.Write("Dafny.Helpers.QuantSet("); TrExpr(b.Set); wr.Write(", "); - } else if (bound is QuantifierExpr.MapBoundedPool) { - var b = (QuantifierExpr.MapBoundedPool)bound; + } else if (bound is ComprehensionExpr.MapBoundedPool) { + var b = (ComprehensionExpr.MapBoundedPool)bound; wr.Write("Dafny.Helpers.QuantMap("); TrExpr(b.Map); wr.Write(", "); - } else if (bound is QuantifierExpr.SeqBoundedPool) { - var b = (QuantifierExpr.SeqBoundedPool)bound; + } else if (bound is ComprehensionExpr.SeqBoundedPool) { + var b = (ComprehensionExpr.SeqBoundedPool)bound; wr.Write("Dafny.Helpers.QuantSeq("); TrExpr(b.Seq); wr.Write(", "); - } else if (bound is QuantifierExpr.DatatypeBoundedPool) { - var b = (QuantifierExpr.DatatypeBoundedPool)bound; + } else if (bound is ComprehensionExpr.DatatypeBoundedPool) { + var b = (ComprehensionExpr.DatatypeBoundedPool)bound; wr.Write("Dafny.Helpers.QuantDatatype("); wr.Write("{0}.AllSingletonConstructors, ", DtName(b.Decl)); @@ -2120,32 +2120,32 @@ namespace Microsoft.Dafny { for (int i = 0; i < n; i++) { var bound = e.Bounds[i]; var bv = e.BoundVars[i]; - if (bound is QuantifierExpr.BoolBoundedPool) { + if (bound is ComprehensionExpr.BoolBoundedPool) { wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName); - } else if (bound is QuantifierExpr.IntBoundedPool) { - var b = (QuantifierExpr.IntBoundedPool)bound; + } else if (bound is ComprehensionExpr.IntBoundedPool) { + var b = (ComprehensionExpr.IntBoundedPool)bound; wr.Write("for (var @{0} = ", bv.CompileName); TrExpr(b.LowerBound); wr.Write("; @{0} < ", bv.CompileName); TrExpr(b.UpperBound); wr.Write("; @{0}++) {{ ", bv.CompileName); - } else if (bound is QuantifierExpr.SetBoundedPool) { - var b = (QuantifierExpr.SetBoundedPool)bound; + } else if (bound is ComprehensionExpr.SetBoundedPool) { + var b = (ComprehensionExpr.SetBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Set); wr.Write(").Elements) { "); - } else if (bound is QuantifierExpr.MapBoundedPool) { - var b = (QuantifierExpr.MapBoundedPool)bound; + } else if (bound is ComprehensionExpr.MapBoundedPool) { + var b = (ComprehensionExpr.MapBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Map); wr.Write(").Domain) { "); - } else if (bound is QuantifierExpr.SeqBoundedPool) { - var b = (QuantifierExpr.SeqBoundedPool)bound; + } else if (bound is ComprehensionExpr.SeqBoundedPool) { + var b = (ComprehensionExpr.SeqBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Seq); wr.Write(").Elements) { "); - } else if (bound is QuantifierExpr.DatatypeBoundedPool) { - var b = (QuantifierExpr.DatatypeBoundedPool)bound; + } else if (bound is ComprehensionExpr.DatatypeBoundedPool) { + var b = (ComprehensionExpr.DatatypeBoundedPool)bound; wr.Write("foreach (var @{0} in {1}.AllSingletonConstructors) {{", bv.CompileName, TypeName(bv.Type)); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type @@ -2189,27 +2189,27 @@ namespace Microsoft.Dafny { Contract.Assert(e.Bounds.Count == n && n == 1); var bound = e.Bounds[0]; var bv = e.BoundVars[0]; - if (bound is QuantifierExpr.BoolBoundedPool) { + if (bound is ComprehensionExpr.BoolBoundedPool) { wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName); - } else if (bound is QuantifierExpr.IntBoundedPool) { - var b = (QuantifierExpr.IntBoundedPool)bound; + } else if (bound is ComprehensionExpr.IntBoundedPool) { + var b = (ComprehensionExpr.IntBoundedPool)bound; wr.Write("for (var @{0} = ", bv.CompileName); TrExpr(b.LowerBound); wr.Write("; @{0} < ", bv.CompileName); TrExpr(b.UpperBound); wr.Write("; @{0}++) {{ ", bv.CompileName); - } else if (bound is QuantifierExpr.SetBoundedPool) { - var b = (QuantifierExpr.SetBoundedPool)bound; + } else if (bound is ComprehensionExpr.SetBoundedPool) { + var b = (ComprehensionExpr.SetBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Set); wr.Write(").Elements) { "); - } else if (bound is QuantifierExpr.MapBoundedPool) { - var b = (QuantifierExpr.MapBoundedPool)bound; + } else if (bound is ComprehensionExpr.MapBoundedPool) { + var b = (ComprehensionExpr.MapBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Map); wr.Write(").Domain) { "); - } else if (bound is QuantifierExpr.SeqBoundedPool) { - var b = (QuantifierExpr.SeqBoundedPool)bound; + } else if (bound is ComprehensionExpr.SeqBoundedPool) { + var b = (ComprehensionExpr.SeqBoundedPool)bound; wr.Write("foreach (var @{0} in (", bv.CompileName); TrExpr(b.Seq); wr.Write(").Elements) { "); -- cgit v1.2.3