From 62d2fa72d5e1816d6cb1239063302808424c6d13 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 19:00:35 +0100 Subject: More refactoring --- Source/Core/Absy.cs | 87 +++++++++++------------------------ Source/Core/AbsyType.cs | 1 + Source/Core/BoogiePL.atg | 6 +-- Source/Core/Parser.cs | 6 +-- Source/VCExpr/TypeErasurePremisses.cs | 1 + 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 MakeList(params T[]/*!*/ args) { + return new List(args); + } + } + public sealed class VariableSeq : List { public VariableSeq(params Variable[]/*!*/ args) : base(args) { @@ -3256,15 +3262,6 @@ namespace Microsoft.Boogie { : base(varSeq) { Contract.Requires(varSeq != null); } - public List/*!*/ ToList() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ res = new List(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/*!*/ ToList() { - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ res = new List(Count); - foreach (TypeVariable/*!*/ var in this) { - Contract.Assert(var != null); - res.Add(var); - } - return res; - } } public sealed class IdentifierExprSeq : List { @@ -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() != null); - - TypeSeq res = new TypeSeq(); - foreach (Expr e in this) - res.Add(cce.NonNull(e).Type); - return res; - } - } } public sealed class StringSeq : List { @@ -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 { @@ -3483,22 +3441,29 @@ namespace Microsoft.Boogie { d.Emit(stream, 0); } } - } - public sealed class DeclarationSeq : List { - 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/*!*/ ds; Axiom/*!*/ ax; List/*!*/ ts; Procedure/*!*/ pr; @@ -439,9 +439,9 @@ OrderSpec<.out bool ChildrenComplete, out List Parents.> . /*------------------------------------------------------------------------*/ -Function +Function/*!*/ ds> = (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); - ds = new DeclarationSeq(); IToken/*!*/ z; + ds = new List(); 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/*!*/ ds; Axiom/*!*/ ax; List/*!*/ ts; Procedure/*!*/ pr; @@ -320,9 +320,9 @@ private class BvBounds : Expr { Expect(8); } - void Function(out DeclarationSeq/*!*/ ds) { + void Function(out List/*!*/ ds) { Contract.Ensures(Contract.ValueAtReturn(out ds) != null); - ds = new DeclarationSeq(); IToken/*!*/ z; + ds = new List(); 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 -- cgit v1.2.3