diff options
| author |  leino <unknown> | 2014-10-20 17:08:46 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-20 17:08:46 -0700 |
| commit | 82edb1b179916ee61655ab7e425a17ab5145fac8 (patch) | |
| tree | d921e9e5a05a5eafbf04e77800a06b73bfed6c6f /Source/Dafny/Util.cs | |
| parent | 963c6622a33dcff4875dbd44be1702cb979c917c (diff) | |
Added types "char" and "string" (the latter being a synonym for "seq<char>").
Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.
Diffstat (limited to 'Source/Dafny/Util.cs')
| -rw-r--r-- | Source/Dafny/Util.cs | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/Source/Dafny/Util.cs b/Source/Dafny/Util.cs index 61004ddd..d2377a76 100644 --- a/Source/Dafny/Util.cs +++ b/Source/Dafny/Util.cs @@ -2,6 +2,7 @@ using System.Collections.Generic;
using System.Linq;
using System.Text;
+using System.Diagnostics.Contracts;
using Microsoft.Boogie;
@@ -66,5 +67,99 @@ namespace Microsoft.Dafny { return res;
}
+ /// <summary>
+ /// For "S" returns S and false.
+ /// For @"S" return S and true.
+ /// Assumes that s has one of these forms.
+ /// </summary>
+ public static string RemoveParsedStringQuotes(string s, out bool isVerbatimString) {
+ Contract.Requires(s != null);
+ var len = s.Length;
+ if (s[0] == '@') {
+ isVerbatimString = true;
+ return s.Substring(2, len - 3);
+ } else {
+ isVerbatimString = false;
+ return s.Substring(1, len - 2);
+ }
+ }
+ /// <summary>
+ /// Replaced any escaped characters in s by the actual character that the escaping represents.
+ /// Assumes s to be a well-parsed string.
+ /// </summary>
+ public static string RemoveEscaping(string s, bool isVerbatimString) {
+ Contract.Requires(s != null);
+ var sb = new StringBuilder();
+ UnescapedCharacters(s, isVerbatimString).Iter(ch => sb.Append(ch));
+ return sb.ToString();
+ }
+ /// <summary>
+ /// Returns the characters of the well-parsed string p, replacing any
+ /// escaped characters by the actual characters.
+ /// </summary>
+ public static IEnumerable<char> UnescapedCharacters(string p, bool isVerbatimString) {
+ Contract.Requires(p != null);
+ if (isVerbatimString) {
+ var skipNext = false;
+ foreach (var ch in p) {
+ if (skipNext) {
+ skipNext = false;
+ } else {
+ yield return ch;
+ if (ch == '"') {
+ skipNext = true;
+ }
+ }
+ }
+ } else {
+ var i = 0;
+ while (i < p.Length) {
+ char special = ' '; // ' ' indicates not special
+ if (p[i] == '\\') {
+ switch (p[i + 1]) {
+ case '\'': special = '\''; break;
+ case '\"': special = '\"'; break;
+ case '\\': special = '\\'; break;
+ case '\0': special = '\0'; break;
+ case 'n': special = '\n'; break;
+ case 'r': special = '\r'; break;
+ case 't': special = '\t'; break;
+ case 'u':
+ int ch = HexValue(p[i + 1]);
+ ch = 16 * ch + HexValue(p[i + 2]);
+ ch = 16 * ch + HexValue(p[i + 3]);
+ ch = 16 * ch + HexValue(p[i + 4]);
+ yield return (char)ch;
+ i += 5;
+ continue;
+ default:
+ break;
+ }
+ }
+ if (special != ' ') {
+ yield return special;
+ i += 2;
+ } else {
+ yield return p[i];
+ i++;
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// Converts a hexadecimal digit to an integer.
+ /// Assumes ch does represent a hexadecimal digit; alphabetic digits can be in either case.
+ /// </summary>
+ public static int HexValue(char ch) {
+ if ('a' <= ch && ch <= 'f') {
+ return ch - 'a' + 10;
+ } else if ('A' <= ch && ch <= 'F') {
+ return ch - 'A' + 10;
+ } else {
+ return ch - '0';
+ }
+ }
+
}
}
|