//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation.  All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.IO;
using System.Xml;
using System.Collections.Generic;
using Microsoft.Contracts;
using Cci = System.Compiler;

namespace Microsoft.Boogie
{

  public class XmlSink {
    string! filename;
    [Rep] XmlWriter wr;
    public bool IsOpen {
      get { return wr != null; }
    }
    
    public XmlSink(string! filename) {
      this.filename = filename;
    }
    
    /// <summary>
    /// Returns null on success, in which case the caller should eventually invoke Close.
    /// Returns an error string on failure.
    /// </summary>
    public string Open()
      modifies this.*;
      ensures IsOpen;
    {
      if (wr != null) {
        Close();
      }
      expose (this) {
        XmlWriterSettings settings = new XmlWriterSettings();
        settings.Indent = true;
        wr = XmlWriter.Create(filename, settings);
        wr.WriteStartDocument();
        wr.WriteStartElement("boogie");
        wr.WriteAttributeString("version", CommandLineOptions.VersionNumber);
        wr.WriteAttributeString("commandLine", Environment.CommandLine);
      }
      return null;  // success
    }
    
    public void Close()
      modifies this.*;
    {
      if (wr != null) {
        expose (this) {
          wr.WriteEndDocument();
          wr.Close();
          wr = null;
        }
      }
    }
    
    const string DateTimeFormatString = "u";
    
    public void WriteStartMethod(string! methodName, DateTime startTime)
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteStartElement("method");
        wr.WriteAttributeString("name", methodName);
        wr.WriteAttributeString("startTime", startTime.ToString(DateTimeFormatString));
      }
    }
    
    public void WriteEndMethod(string! outcome, DateTime endTime, TimeSpan elapsed)
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteStartElement("conclusion");
        wr.WriteAttributeString("endTime", endTime.ToString(DateTimeFormatString));
        wr.WriteAttributeString("duration", elapsed.TotalSeconds.ToString());
        wr.WriteAttributeString("outcome", outcome);
        
        wr.WriteEndElement();  // outcome
        wr.WriteEndElement();  // method
      }
    }
    
    public void WriteError(string! message, IToken! errorToken, IToken relatedToken, BlockSeq trace)
      requires IsOpen && (trace == null || Owner.Different(this, trace));
      modifies this.*, errorToken.*, relatedToken.*, trace.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose(this){
        wr.WriteStartElement("error");
        wr.WriteAttributeString("message", message);
        WriteTokenAttributes(errorToken);
        if (relatedToken != null)
        {
          wr.WriteStartElement("related");
          WriteTokenAttributes(relatedToken);
          wr.WriteEndElement();
        }
        if (trace != null)
        {
          wr.WriteStartElement("trace");
          {
            foreach (object bo in trace)
              invariant wr != null;
            {
              assume bo is Block;
              Block b = (Block)bo;
              wr.WriteStartElement("traceNode");
              {
                WriteTokenAttributes(b.tok);
                wr.WriteAttributeString("label", b.Label);
              }
              wr.WriteEndElement();
            }
            wr.WriteEndElement();
          }
        }
        wr.WriteEndElement();
      } 
    }     

    public void WriteError(string! message, Cci.Node! offendingNode, BlockSeq trace)
      requires IsOpen && Owner.Different(this, offendingNode);
      requires trace == null || Owner.Different(this, trace);
      modifies this.*, offendingNode.*, trace.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose(this){
        wr.WriteStartElement("error");
        wr.WriteAttributeString("message", message);
        WriteTokenAttributes(offendingNode);
        if (trace != null)
        {
          wr.WriteStartElement("trace");
          {
            foreach (object bo in trace)
              invariant wr != null;
            {
              assume bo is Block;
              Block b = (Block)bo;
              wr.WriteStartElement("traceNode");
              {
                this.WriteTokenAttributes(b.tok);
                wr.WriteAttributeString("label", b.Label);
              }
              wr.WriteEndElement();
            }
            wr.WriteEndElement();
          }
        }
        wr.WriteEndElement();
      } 
    }

    [Inside]
    private void WriteTokenAttributes(IToken tok) 
      requires wr != null && wr.IsPeerConsistent;
      modifies this.0, wr.*;
    {
      if (tok != null && tok.filename != null)
      {
        wr.WriteAttributeString("file", tok.filename);
        wr.WriteAttributeString("line", tok.line.ToString());
        wr.WriteAttributeString("column", tok.col.ToString());
      }
    }

    [Inside]
    private void WriteTokenAttributes(Cci.Node! node) 
      requires wr != null && wr.IsPeerConsistent;
      modifies this.0, wr.*;
    {
      assert wr != null;
      if (node.SourceContext.Document != null)
      {
        wr.WriteAttributeString("file", node.SourceContext.Document.Name);
        wr.WriteAttributeString("line", node.SourceContext.StartLine.ToString());
        wr.WriteAttributeString("column", node.SourceContext.StartColumn.ToString());
      }
    }
    
    public void WriteStartInference(string! inferenceName)
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteStartElement("inference");
        wr.WriteAttributeString("name", inferenceName);
      }
    }
    
    public void WriteEndInference()
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteEndElement();  // inference
      }
    }
    
    public void WriteContractParaAssignment(string! varName, string val)
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteStartElement("assignment");
        wr.WriteAttributeString("name", varName);
        wr.WriteAttributeString("value", val);
        wr.WriteEndElement();
      }
    }
    
    public void WriteStartFile(string! filename)
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteStartElement("file");
        wr.WriteAttributeString("name", filename);
      }
    }

    public void WriteEndFile()
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteEndElement();
      }
    }
    
    public void WriteFileFragment(string! fragment)
      requires IsOpen;
      modifies this.*;
      ensures IsOpen;
    {
      assert wr != null;
      expose (this) {
        wr.WriteStartElement("fileFragment");
        wr.WriteAttributeString("name", fragment);
        wr.WriteEndElement();
      }
    }
  }
  
  public class XmlFileScope : IDisposable {
    [Peer] [SpecPublic] XmlSink sink;
    
    [Captured]
    public XmlFileScope(XmlSink? sink, string! filename)
      requires sink != null ==> sink.IsOpen;
      modifies sink.*;
    {
      if (sink != null) {
        sink.WriteStartFile(filename);  // invoke this method while "sink" is still peer consistent
        Owner.AssignSame(this, sink);
        this.sink = sink;
      }
    }
    
    public void Dispose()
    {
      if (sink != null) {
        assume sink.IsOpen;
        sink.WriteEndFile();
      }
    }
  }
}