blob: 461e1ee8bb25eb75e19d1c5149fa303017fd5d4f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
//-----------------------------------------------------------------------------
//
// Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
using System;
using System.Linq;
using System.Collections.Generic;
using System.Collections.ObjectModel;
using System.Text;
using System.Diagnostics.Contracts;
using System.Globalization;
namespace Microsoft.Boogie
{
public class SExpr
{
static readonly SExpr[] EmptyArgs = new SExpr[0];
public readonly string Name;
public SExpr[] Arguments
{
get
{
Contract.Ensures(Contract.Result<SExpr[]>() != null);
Contract.Ensures(Contract.ForAll(Contract.Result<SExpr[]>(), expr => expr != null));
return this.arguments;
}
}
public SExpr this[int idx]
{
get
{
return Arguments[idx];
}
}
public int ArgCount
{
get { return arguments.Length; }
}
public bool IsId
{
get { return Arguments.Length == 0; }
}
private readonly SExpr[] arguments;
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(this.Name != null);
Contract.Invariant(this.arguments != null);
Contract.Invariant(Contract.ForAll(this.arguments, arg => arg != null));
}
public SExpr(string name, params SExpr[] args)
: this(name, (IEnumerable<SExpr>)args)
{
Contract.Requires(name != null);
Contract.Requires(args != null);
Contract.Requires(Contract.ForAll(args, x => x != null));
}
public SExpr(string name, IEnumerable<SExpr> args)
{
Contract.Requires(name != null);
Contract.Requires(args != null);
// We don't want to evaluate args twice!
// Contract.Requires(Contract.ForAll(args, x => x != null));
Name = name;
arguments = args.ToArray();
}
public SExpr(string name)
: this(name, EmptyArgs)
{
Contract.Requires(name != null);
}
#region pretty-printing
void WriteTo(StringBuilder sb)
{
Contract.Requires(sb != null);
if (Arguments.Length > 0) sb.Append('(');
if (Name.Any(Char.IsWhiteSpace))
sb.Append("\"").Append(Name).Append("\"");
else
sb.Append(Name);
foreach (var a in Arguments) {
sb.Append(' ');
a.WriteTo(sb);
}
if (Arguments.Length > 0) sb.Append(')');
}
public override string ToString()
{
var sb = new StringBuilder();
this.WriteTo(sb);
return sb.ToString();
}
#endregion
}
}
|
