Move classes into separate files

Source/Core/Visitors/VarDeclOnceStandardVisitor.cs

@@ -0,0 +1,21 @@
+namespace Microsoft.Boogie;
+
+/// <summary>
+/// VarDeclOnceStandardVisitor is like StandardVisitor, except
+///   -- it does not visit a variable's declaration when visiting an `IdentifierExpr`, and
+///   -- it visits the `where` clause (if any) when visiting a `TypedIdent`.
+/// </summary>
+public abstract class VarDeclOnceStandardVisitor : StandardVisitor
+{
+  public override Expr VisitIdentifierExpr(IdentifierExpr node) {
+    return node;
+  }
+
+  public override TypedIdent VisitTypedIdent(TypedIdent node) {
+    node = base.VisitTypedIdent(node);
+    if (node.WhereExpr != null) {
+      node.WhereExpr = (Expr) Visit(node.WhereExpr);
+    }
+    return node;
+  }
+}

Source/Core/Visitors/Visitor.cs

@@ -0,0 +1,40 @@
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+[ContractClass(typeof(VisitorContracts))]
+/// <summary>
+/// Base for all classes that process the Absy using the visitor pattern.
+/// </summary>
+public abstract class Visitor
+{
+  /// <summary>
+  /// Switches on node.NodeType to call a visitor method that has been specialized for node.
+  /// </summary>
+  /// <param name="a">The Absy node to be visited.</param>
+  /// <returns> Returns null if node is null. Otherwise returns an updated node (possibly a different object).</returns>
+  public abstract Absy /*!*/ Visit(Absy /*!*/ node);
+
+  /// <summary>
+  /// Transfers the state from one visitor to another. This enables separate visitor instances to cooperative process a single IR.
+  /// </summary>
+  public virtual void TransferStateTo(Visitor targetVisitor)
+  {
+  }
+
+  public virtual IList<Expr> VisitExprSeq(IList<Expr> list)
+  {
+    Contract.Requires(list != null);
+    Contract.Ensures(Contract.Result<IList<Expr>>() != null);
+    lock (list)
+    {
+      for (int i = 0, n = list.Count; i < n; i++)
+      {
+        list[i] = (Expr) this.Visit(cce.NonNull(list[i]));
+      }
+    }
+
+    return list;
+  }
+}

Source/Core/Visitors/VisitorContracts.cs

@@ -0,0 +1,15 @@
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Boogie;
+
+[ContractClassFor(typeof(Visitor))]
+abstract class VisitorContracts : Visitor
+{
+  public override Absy Visit(Absy node)
+  {
+    Contract.Requires(node != null);
+    Contract.Ensures(Contract.Result<Absy>() != null);
+
+    throw new System.NotImplementedException();
+  }
+}