diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/Absy.cs | 87 | ||||
| -rw-r--r-- | Source/Core/AbsyType.cs | 1 | ||||
| -rw-r--r-- | Source/Core/BoogiePL.atg | 6 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 6 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasurePremisses.cs | 1 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 1 |
6 files changed, 35 insertions, 67 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 2a654298..6b0fcdb3 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3209,6 +3209,12 @@ namespace Microsoft.Boogie { // Generic Sequences
//---------------------------------------------------------------------
+ public static class ListFactory {
+ public static List<T> MakeList<T>(params T[]/*!*/ args) {
+ return new List<T>(args);
+ }
+ }
+
public sealed class VariableSeq : List<Variable> {
public VariableSeq(params Variable[]/*!*/ args)
: base(args) {
@@ -3256,15 +3262,6 @@ namespace Microsoft.Boogie { : base(varSeq) {
Contract.Requires(varSeq != null);
}
- public List<Type/*!*/>/*!*/ ToList() {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<Type>>()));
- List<Type/*!*/>/*!*/ res = new List<Type/*!*/>(Count);
- foreach (Type/*!*/ t in this) {
- Contract.Assert(t != null);
- res.Add(t);
- }
- return res;
- }
public void Emit(TokenTextWriter stream, string separator) {
Contract.Requires(separator != null);
Contract.Requires(stream != null);
@@ -3310,15 +3307,6 @@ namespace Microsoft.Boogie { v.Emit(stream);
}
}
- public List<TypeVariable/*!*/>/*!*/ ToList() {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<TypeVariable>>()));
- List<TypeVariable/*!*/>/*!*/ res = new List<TypeVariable/*!*/>(Count);
- foreach (TypeVariable/*!*/ var in this) {
- Contract.Assert(var != null);
- res.Add(var);
- }
- return res;
- }
}
public sealed class IdentifierExprSeq : List<IdentifierExpr> {
@@ -3417,26 +3405,6 @@ namespace Microsoft.Boogie { n[s.Count + i] = t[i];
return new ExprSeq(n);
}
- public void Emit(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- string sep = "";
- foreach (Expr/*!*/ e in this) {
- Contract.Assert(e != null);
- stream.Write(sep);
- sep = ", ";
- e.Emit(stream);
- }
- }
- public TypeSeq/*!*/ ToTypeSeq {
- get {
- Contract.Ensures(Contract.Result<TypeSeq>() != null);
-
- TypeSeq res = new TypeSeq();
- foreach (Expr e in this)
- res.Add(cce.NonNull(e).Type);
- return res;
- }
- }
}
public sealed class StringSeq : List<String> {
@@ -3444,16 +3412,6 @@ namespace Microsoft.Boogie { : base(args) {
Contract.Requires(args != null);
}
- public void Emit(TokenTextWriter stream) {
- Contract.Requires(stream != null);
- string sep = "";
- foreach (string/*!*/ s in this) {
- Contract.Assert(s != null);
- stream.Write(sep);
- sep = ", ";
- stream.Write(s);
- }
- }
}
public sealed class BlockSeq : List<Block> {
@@ -3483,22 +3441,29 @@ namespace Microsoft.Boogie { d.Emit(stream, 0);
}
}
- }
- public sealed class DeclarationSeq : List<Declaration> {
- public void Emit(TokenTextWriter stream) {
+
+ public static void Emit(this StringSeq ss, TokenTextWriter stream) {
Contract.Requires(stream != null);
- bool first = true;
- foreach (Declaration d in this) {
- if (d == null)
- continue;
- if (first) {
- first = false;
- } else {
- stream.WriteLine();
- }
- d.Emit(stream, 0);
+ string sep = "";
+ foreach (string/*!*/ s in ss) {
+ Contract.Assert(s != null);
+ stream.Write(sep);
+ sep = ", ";
+ stream.Write(s);
}
}
+
+ public static void Emit(this ExprSeq ts, TokenTextWriter stream) {
+ Contract.Requires(stream != null);
+ string sep = "";
+ foreach (Expr/*!*/ e in ts) {
+ Contract.Assert(e != null);
+ stream.Write(sep);
+ sep = ", ";
+ e.Emit(stream);
+ }
+ }
+
}
#endregion
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 944bbe08..fe2b9a4c 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -11,6 +11,7 @@ namespace Microsoft.Boogie { using System;
using System.Collections;
using System.Diagnostics;
+ using System.Linq;
using System.Collections.Generic;
using Microsoft.Boogie.AbstractInterpretation;
using System.Diagnostics.Contracts;
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 6b064669..219cb3e6 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -160,7 +160,7 @@ PRODUCTIONS /*------------------------------------------------------------------------*/
BoogiePL
= (. VariableSeq/*!*/ vs;
- DeclarationSeq/*!*/ ds;
+ List<Declaration>/*!*/ ds;
Axiom/*!*/ ax;
List<Declaration/*!*/>/*!*/ ts;
Procedure/*!*/ pr;
@@ -439,9 +439,9 @@ OrderSpec<.out bool ChildrenComplete, out List<ConstantParent/*!*/> Parents.> .
/*------------------------------------------------------------------------*/
-Function<out DeclarationSeq/*!*/ ds>
+Function<out List<Declaration>/*!*/ ds>
= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- ds = new DeclarationSeq(); IToken/*!*/ z;
+ ds = new List<Declaration>(); IToken/*!*/ z;
IToken/*!*/ typeParamTok;
var typeParams = new TypeVariableSeq();
var arguments = new VariableSeq();
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index f6347b37..ed5b88ae 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -208,7 +208,7 @@ private class BvBounds : Expr { void BoogiePL() {
VariableSeq/*!*/ vs;
- DeclarationSeq/*!*/ ds;
+ List<Declaration>/*!*/ ds;
Axiom/*!*/ ax;
List<Declaration/*!*/>/*!*/ ts;
Procedure/*!*/ pr;
@@ -320,9 +320,9 @@ private class BvBounds : Expr { Expect(8);
}
- void Function(out DeclarationSeq/*!*/ ds) {
+ void Function(out List<Declaration>/*!*/ ds) {
Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- ds = new DeclarationSeq(); IToken/*!*/ z;
+ ds = new List<Declaration>(); IToken/*!*/ z;
IToken/*!*/ typeParamTok;
var typeParams = new TypeVariableSeq();
var arguments = new VariableSeq();
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index c28d9b4c..d887a70f 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -8,6 +8,7 @@ using System.Text; using System.IO;
using System.Collections;
using System.Collections.Generic;
+using System.Linq;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 1dd1cac9..67280bea 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -9,6 +9,7 @@ using System.IO; using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
+using System.Linq;
using Microsoft.Basetypes;
// Some visitor skeletons for the VCExpression AST
|