diff options
| author |  tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-20 22:29:44 +0000 |
| commit | b617dda87871573b826dada4af73fc48dce94f15 (patch) | |
| tree | 453088d59b99376c0b14035e76463a4561d6ec1c /Source/Core/OOLongUtil.cs | |
| parent | 0d77cf304b9bd2b2152fe1a733e4533536c883c0 (diff) | |
Boogie: Renaming core sources in preparation for port commit
Diffstat (limited to 'Source/Core/OOLongUtil.cs')
| -rw-r--r-- | Source/Core/OOLongUtil.cs | 174 |
1 files changed, 174 insertions, 0 deletions
diff --git a/Source/Core/OOLongUtil.cs b/Source/Core/OOLongUtil.cs new file mode 100644 index 00000000..e87666f3 --- /dev/null +++ b/Source/Core/OOLongUtil.cs @@ -0,0 +1,174 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections.Generic;
+using System.IO;
+using Microsoft.Contracts;
+
+namespace Boogie.Util {
+ public class TeeWriter : TextWriter {
+ readonly TextWriter! a;
+ readonly TextWriter! b;
+
+ public TeeWriter(TextWriter! a, TextWriter! b) {
+ this.a = a;
+ this.b = b;
+ }
+
+ public override System.Text.Encoding Encoding {
+ get {
+ return a.Encoding;
+ }
+ }
+
+ public override void Close() {
+ a.Close();
+ b.Close();
+ }
+
+ public override void Flush() {
+ a.Flush();
+ b.Flush();
+ }
+
+ [Pure]
+ public override string! ToString() {
+ return "<TeeWriter: " + a.ToString() + ", " + b.ToString() + ">";
+ }
+
+ public override void Write(char ch) {
+ a.Write(ch);
+ b.Write(ch);
+ }
+
+ public override void Write(string s) {
+ a.Write(s);
+ b.Write(s);
+ }
+ }
+
+ /// <summary>
+ /// A LineReader is a class that allows further subclasses to just override the ReadLine() method.
+ /// It simply reads from the given "reader".
+ /// </summary>
+ public class LineReader : TextReader {
+ [Rep] readonly TextReader! reader;
+ string readAhead;
+ int readAheadConsumed;
+ invariant readAhead == null || (0 <= readAheadConsumed && readAheadConsumed < readAhead.Length);
+
+ public LineReader([Captured] TextReader! reader) {
+ this.reader = reader;
+ }
+ public override void Close() {
+ expose (this) {
+ reader.Close();
+ }
+ }
+ public override int Read() {
+ expose (this) {
+ while (readAhead == null) {
+ readAhead = reader.ReadLine();
+ if (readAhead == null) {
+ // we're at EOF
+ return -1;
+ } else if (readAhead.Length > 0) {
+ readAheadConsumed = 0;
+ break;
+ }
+ }
+ int res = readAhead[readAheadConsumed++];
+ if (readAheadConsumed == readAhead.Length) {
+ readAhead = null;
+ }
+ return res;
+ }
+ }
+ public override int Read(char[]! buffer, int index, int count) {
+ int n = 0;
+ for (; n < count; n++) {
+ int ch = Read();
+ if (ch == -1) {
+ break;
+ }
+ buffer[index + n] = (char)ch;
+ }
+ return n;
+ }
+ public override string ReadLine() {
+ string res;
+ if (readAhead != null) {
+ expose (this) {
+ res = readAhead.Substring(readAheadConsumed);
+ readAhead = null;
+ }
+ } else {
+ res = reader.ReadLine();
+ }
+ return res;
+ }
+ }
+
+ public class IfdefReader : LineReader {
+ [Rep] readonly List<string!>! defines;
+ [Rep] readonly List<bool>! readState = new List<bool>();
+ int ignoreCutoff = 0; // 0 means we're not ignoring
+ invariant 0 <= ignoreCutoff && ignoreCutoff <= readState.Count;
+
+ public IfdefReader([Captured] TextReader! reader, [Captured] List<string!>! defines) {
+ base(reader);
+ this.defines = defines;
+ }
+
+ public override string ReadLine() {
+ while (true) {
+ string s = base.ReadLine();
+ if (s == null) {
+ return s;
+ }
+ string t = s.Trim();
+ if (t.StartsWith("#if")) {
+ string arg = t.Substring(3).TrimStart();
+ bool sense = true;
+ while (t.StartsWith("!")) {
+ sense = !sense;
+ t = t.Substring(1).TrimStart();
+ }
+ // push "true", since we're in a "then" branch
+ readState.Add(true);
+ if (ignoreCutoff == 0 && defines.Contains(arg) != sense) {
+ ignoreCutoff = readState.Count; // start ignoring
+ }
+ } else if (t == "#else") {
+ if (readState.Count == 0 || !readState[readState.Count-1]) {
+ return s; // malformed input; return the read line as if it were not special
+ }
+ // change the "true" to a "false" on top of the state, since we're now going into the "else" branch
+ readState[readState.Count-1] = false;
+ if (ignoreCutoff == 0) {
+ // the "then" branch had been included, so we'll ignore the "else" branch
+ ignoreCutoff = readState.Count;
+ } else if (ignoreCutoff == readState.Count) {
+ // we had ignored the "then" branch, so we'll include the "else" branch
+ ignoreCutoff = 0;
+ }
+ } else if (t == "#endif") {
+ if (readState.Count == 0) {
+ return s; // malformed input; return the read line as if it were not special
+ }
+ if (ignoreCutoff == readState.Count) {
+ // we had ignored the branch that ends here; so, now we start including again
+ ignoreCutoff = 0;
+ }
+ // pop
+ readState.RemoveAt(readState.Count-1);
+ } else if (ignoreCutoff == 0) {
+ return s;
+ }
+ }
+ }
+ }
+}
|