Support all option types in the project file

Source/DafnyCore.Test/DafnyProjectTest.cs

@@ -10,7 +10,7 @@ public class DafnyProjectTest {
  Uri = new Uri(randomFileName, UriKind.Absolute),
  Includes = new[] { "a", "a2" },
  Excludes = new[] { "b", "b2" },
- Options = new Dictionary<string, object>() {
+ Options = new Dictionary<string, string>() {
  { "c", "d" },
  { "e", "f" }
  }
@@ -20,21 +20,21 @@ public class DafnyProjectTest {
  Uri = new Uri(randomFileName, UriKind.Absolute),
  Includes = new[] { "a2", "a" },
  Excludes = new[] { "b2", "b" },
- Options = new Dictionary<string, object>() {
+ Options = new Dictionary<string, string>() {
  { "e", "f" },
  { "c", "d" },
  }
  };
 
  Assert.Equal(first, second);
 
- first.Options.Add("k", new[] { 1, 2, 3 });
- second.Options.Add("k", new[] { 1, 2, 3 });
+ first.Options.Add("k", "1, 2, 3");
+ second.Options.Add("k", "1, 2, 3");
 
  Assert.Equal(first, second);
 
- first.Options.Add("m", new[] { 1, 2, 3 });
- second.Options.Add("m", new[] { 3, 2, 1 });
+ first.Options.Add("m", "1, 2, 3");
+ second.Options.Add("m", "3, 2, 1");
  Assert.NotEqual(first, second);
  }
 }

Source/DafnyCore/DooFile.cs

@@ -1,18 +1,13 @@
 using System;
 using System.Collections.Generic;
 using System.CommandLine;
-using System.CommandLine.Binding;
-using System.Configuration;
 using System.IO;
 using System.IO.Compression;
 using System.Linq;
 using System.Text;
-using System.Threading;
+using DafnyCore.Generic;
 using Microsoft.Dafny;
-using Microsoft.Dafny.Auditor;
 using Tomlyn;
-using Tomlyn.Model;
-using Type = System.Type;
 
 namespace DafnyCore; 
 
@@ -137,7 +132,7 @@ public class ManifestData {
 
  object libraryValue = null;
  if (Manifest.Options.TryGetValue(option.Name, out var manifestValue)) {
- if (!DafnyProject.TryGetValueFromToml(Console.Out, null,
+ if (!TomlUtil.TryGetValueFromToml(Console.Out, null,
  option.Name, option.ValueType, manifestValue, out libraryValue)) {
  return false;
  }

Source/DafnyCore/Generic/TomlUtil.cs

@@ -0,0 +1,70 @@
+using System;
+using System.Collections.Generic;
+using System.IO;
+using System.Linq;
+using Tomlyn.Model;
+
+namespace DafnyCore.Generic; 
+
+public static class TomlUtil {
+
+ public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, Type type, object tomlValue, out object value) {
+ if (tomlValue == null) {
+ value = null;
+ return false;
+ }
+
+ if (type.IsAssignableFrom(typeof(List<string>))) {
+ return TryGetListValueFromToml<string>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
+ }
+ if (type.IsAssignableFrom(typeof(List<FileInfo>))) {
+ return TryGetListValueFromToml<FileInfo>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
+ }
+
+ if (tomlValue is string tomlString) {
+ if (type == typeof(FileInfo)) {
+ // Need to make sure relative paths are interpreted relative to the source of the value,
+ // not the current directory.
+ var fullPath = sourceDir != null ? Path.GetFullPath(tomlString, sourceDir) : tomlString;
+ value = new FileInfo(fullPath);
+ return true;
+ }
+
+ if (typeof(Enum).IsAssignableFrom(type)) {
+ try {
+ value = Enum.Parse(type, tomlString);
+ return true;
+ } catch (ArgumentException) {
+ value = null;
+ return false;
+ }
+ }
+ }
+
+ if (!type.IsInstanceOfType(tomlValue)) {
+ if (type == typeof(string)) {
+ value = tomlValue.ToString();
+ return true;
+ }
+ errorWriter.WriteLine(
+ $"Error: property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'");
+ value = null;
+ return false;
+ }
+
+ value = tomlValue;
+ return true;
+ }
+
+ private static bool TryGetListValueFromToml<T>(TextWriter errorWriter, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) {
+ var success = true;
+ value = tomlValue.Select((e, i) => {
+ if (TryGetValueFromToml(errorWriter, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) {
+ return (T)elementValue;
+ }
+ success = false;
+ return default(T);
+ }).ToList();
+ return success;
+ }
+}

Source/DafnyCore/Options/DafnyProject.cs

@@ -10,7 +10,6 @@
 using DafnyCore.Options;
 using Microsoft.Extensions.FileSystemGlobbing;
 using Tomlyn;
-using Tomlyn.Model;
 
 namespace Microsoft.Dafny; 
 
@@ -23,7 +22,7 @@ public class DafnyProject : IEquatable<DafnyProject> {
  public Uri Uri { get; set; }
  public string[] Includes { get; set; }
  public string[] Excludes { get; set; }
- public Dictionary<string, object> Options { get; set; }
+ public Dictionary<string, string> Options { get; set; }
  public bool UsesProjectFile => Path.GetFileName(Uri.LocalPath) == FileName;
 
  public static async Task<DafnyProject> Open(IFileSystem fileSystem, Uri uri, TextWriter outputWriter, TextWriter errorWriter) {
@@ -140,57 +139,16 @@ public class DafnyProject : IEquatable<DafnyProject> {
  return false;
  }
 
- return TryGetValueFromToml(errorWriter, Path.GetDirectoryName(Uri.LocalPath), option.Name, option.ValueType, tomlValue, out value);
- }
-
- public static bool TryGetValueFromToml(TextWriter errorWriter, string sourceDir, string tomlPath, System.Type type, object tomlValue, out object value) {
- if (tomlValue == null) {
- value = null;
- return false;
- }
-
- if (type.IsAssignableFrom(typeof(List<string>))) {
- return TryGetListValueFromToml<string>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
- }
- if (type.IsAssignableFrom(typeof(List<FileInfo>))) {
- return TryGetListValueFromToml<FileInfo>(errorWriter, sourceDir, tomlPath, (TomlArray)tomlValue, out value);
- }
-
- if (type == typeof(FileInfo) && tomlValue is string tomlString) {
- // Need to make sure relative paths are interpreted relative to the source of the value,
- // not the current directory.
- var fullPath = sourceDir != null ? Path.GetFullPath(tomlString, sourceDir) : tomlString;
- value = new FileInfo(fullPath);
- return true;
- }
-
- if (!type.IsInstanceOfType(tomlValue)) {
- if (type == typeof(string)) {
- value = tomlValue.ToString();
- return true;
- }
- errorWriter.WriteLine(
- $"Error: property '{tomlPath}' is of type '{tomlValue.GetType()}' but should be of type '{type}'");
+ var parseResult = option.Parse(new[] { option.Aliases.First(), tomlValue });
+ if (parseResult.Errors.Any()) {
  value = null;
  return false;
  }
 
- value = tomlValue;
+ value = parseResult.GetValueForOption(option);
  return true;
  }
 
- private static bool TryGetListValueFromToml<T>(TextWriter errorWriter, string sourceDir, string tomlPath, TomlArray tomlValue, out object value) {
- var success = true;
- value = tomlValue.Select((e, i) => {
- if (TryGetValueFromToml(errorWriter, sourceDir, $"{tomlPath}[{i}]", typeof(T), e, out var elementValue)) {
- return (T)elementValue;
- }
- success = false;
- return default(T);
- }).ToList();
- return success;
- }
-
  public bool Equals(DafnyProject other) {
  if (ReferenceEquals(null, other)) {
  return false;
@@ -200,13 +158,13 @@ public class DafnyProject : IEquatable<DafnyProject> {
  return true;
  }
 
- var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
- var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, object>>();
+ var orderedOptions = Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, string>>();
+ var otherOrderedOptions = other.Options?.OrderBy(kv => kv.Key) ?? Enumerable.Empty<KeyValuePair<string, string>>();
 
  return Equals(Uri, other.Uri) &&
  NullableSetEqual(Includes?.ToHashSet(), other.Includes) &&
  NullableSetEqual(Excludes?.ToHashSet(), other.Excludes) &&
- orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer<KeyValuePair<string, object>>(
+ orderedOptions.SequenceEqual(otherOrderedOptions, new LambdaEqualityComparer<KeyValuePair<string, string>>(
  (kv1, kv2) => kv1.Key == kv2.Key && GenericEquals(kv1.Value, kv2.Value),
  kv => kv.GetHashCode()));
  }

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -1,4 +1,5 @@
 using System.IO;
+using System.Linq;
 using System.Threading.Tasks;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
 using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
@@ -67,6 +68,7 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest {
  public async Task ProjectFileOverridesOptions() {
  await SetUp(options => {
  options.Set(Function.FunctionSyntaxOption, "3");
+ options.Set(CommonOptionBag.QuantifierSyntax, QuantifierSyntaxOptions.Version3);
  options.Set(CommonOptionBag.WarnShadowing, true);
  });
  var source = @"
@@ -77,13 +79,18 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest {
  }
 }
 
+function Zoo(): set<(int,int)> {
+ set x: int | 0 <= x < 5, y | 0 <= y < 6 :: (x,y)
+}
+
 ghost function Bar(): int { 3 }".TrimStart();
 
  var projectFileSource = @"
 includes = [""**/*.dfy""]
 
 [options]
 warn-shadowing = false
+quantifier-syntax = 4
 function-syntax = 4";
 
  var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
@@ -94,7 +101,9 @@ public class ProjectFilesTest : ClientBasedLanguageServerTest {
  Assert.Single(diagnostics1); // Stops after parsing
 
  await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource);
- await CreateAndOpenTestDocument(source, Path.Combine(directory, "source.dfy"));
+ var sourceFile = await CreateAndOpenTestDocument(source, Path.Combine(directory, "source.dfy"));
+ var diagnostics2 = await GetLastDiagnostics(sourceFile, CancellationToken);
+ Assert.Empty(diagnostics2.Where(d => d.Severity == DiagnosticSeverity.Error));
  await AssertNoDiagnosticsAreComing(CancellationToken);
  }