diff --git a/Source/DafnyCore/AST/Function.cs b/Source/DafnyCore/AST/Function.cs index fc61b373b76..88abe4b2159 100644 --- a/Source/DafnyCore/AST/Function.cs +++ b/Source/DafnyCore/AST/Function.cs @@ -7,7 +7,7 @@ namespace Microsoft.Dafny; -public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFormat { +public class Function : MemberDecl, TypeParameter.ParentType, ICallable, ICanFormat, IHasDocstring { public override string WhatKind => "function"; public string GetFunctionDeclarationKeywords(DafnyOptions options) { @@ -437,4 +437,23 @@ public void Resolve(Resolver resolver) { resolver.Options.WarnShadowing = warnShadowingOption; // restore the original warnShadowing value } + + protected override string GetTriviaContainingDocstring() { + if (Body == null) { + if (EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + if (StartToken.LeadingTrivia.Trim() != "") { + return StartToken.LeadingTrivia; + } + } else if (Body.StartToken.Prev.Prev is var tokenWhereTrailingIsDocstring && + tokenWhereTrailingIsDocstring.TrailingTrivia.Trim() != "") { + return tokenWhereTrailingIsDocstring.TrailingTrivia; + } else if (StartToken is var tokenWhereLeadingIsDocstring && + tokenWhereLeadingIsDocstring.LeadingTrivia.Trim() != "") { + return tokenWhereLeadingIsDocstring.LeadingTrivia; + } + return null; + } } diff --git a/Source/DafnyCore/AST/Grammar/TriviaFormatterHelper.cs b/Source/DafnyCore/AST/Grammar/TriviaFormatterHelper.cs index e0af977e535..57d4bb9bf01 100644 --- a/Source/DafnyCore/AST/Grammar/TriviaFormatterHelper.cs +++ b/Source/DafnyCore/AST/Grammar/TriviaFormatterHelper.cs @@ -12,11 +12,11 @@ public static bool EndsWithNewline(string s) { return EndsWithNewlineRegex.IsMatch(s); } - private static readonly string AnyNewline = @"\r?\n|\r(?!\n)"; + public static readonly string AnyNewline = @"\r?\n|\r(?!\n)"; private static readonly string NoCommentDelimiter = @"(?:(?!/\*|\*/)[\s\S])*"; - private static readonly string MultilineCommentContent = + public static readonly string MultilineCommentContent = $@"(?:{NoCommentDelimiter}(?:(?'Open'/\*)|(?'-Open'\*/)))*{NoCommentDelimiter}"; public static readonly Regex NewlineRegex = diff --git a/Source/DafnyCore/AST/IteratorDecl.cs b/Source/DafnyCore/AST/IteratorDecl.cs index cd8e021f810..604addc95c8 100644 --- a/Source/DafnyCore/AST/IteratorDecl.cs +++ b/Source/DafnyCore/AST/IteratorDecl.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny; -public class IteratorDecl : ClassDecl, IMethodCodeContext { +public class IteratorDecl : ClassDecl, IMethodCodeContext, IHasDocstring { public override string WhatKind { get { return "iterator"; } } public readonly List Ins; public readonly List Outs; @@ -480,4 +480,20 @@ public void Resolve(Resolver resolver) { Members.Add(moveNext); } } + + + protected override string GetTriviaContainingDocstring() { + IToken lastClosingParenthesis = null; + foreach (var token in OwnedTokens) { + if (token.val == ")") { + lastClosingParenthesis = token; + } + } + + if (lastClosingParenthesis != null && lastClosingParenthesis.TrailingTrivia.Trim() != "") { + return lastClosingParenthesis.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } diff --git a/Source/DafnyCore/AST/MemberDecls.cs b/Source/DafnyCore/AST/MemberDecls.cs index 11854c015e7..95669f87091 100644 --- a/Source/DafnyCore/AST/MemberDecls.cs +++ b/Source/DafnyCore/AST/MemberDecls.cs @@ -93,7 +93,7 @@ public virtual string FullSanitizedName { public virtual IEnumerable SubExpressions => Enumerable.Empty(); } -public class Field : MemberDecl, ICanFormat { +public class Field : MemberDecl, ICanFormat, IHasDocstring { public override string WhatKind => "field"; public readonly bool IsMutable; // says whether or not the field can ever change values public readonly bool IsUserMutable; // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable) @@ -173,6 +173,14 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return true; } + + protected override string GetTriviaContainingDocstring() { + if (EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } public class SpecialFunction : Function, ICallable { diff --git a/Source/DafnyCore/AST/Method.cs b/Source/DafnyCore/AST/Method.cs index fdb21a25487..0dda3b0b8e4 100644 --- a/Source/DafnyCore/AST/Method.cs +++ b/Source/DafnyCore/AST/Method.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; -public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext, ICanFormat { +public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext, ICanFormat, IHasDocstring { public override IEnumerable Children => new Node[] { Body, Decreases }. Where(x => x != null).Concat(Ins).Concat(Outs).Concat(TypeArgs). Concat(Req).Concat(Ens).Concat(Mod.Expressions); @@ -336,4 +336,19 @@ public void Resolve(Resolver resolver) { resolver.currentMethod = null; } } + + protected override string GetTriviaContainingDocstring() { + IToken lastClosingParenthesis = null; + foreach (var token in OwnedTokens) { + if (token.val == ")") { + lastClosingParenthesis = token; + } + } + + if (lastClosingParenthesis != null && lastClosingParenthesis.TrailingTrivia.Trim() != "") { + return lastClosingParenthesis.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index 13f144c7c81..ca5f0e1b65e 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/Source/DafnyCore/AST/TopLevelDeclarations.cs @@ -345,7 +345,7 @@ public static Dictionary SubstitutionMap(List(); + foreach (var token in tokens) { + if (token.val == "{") { + candidate = token.Prev; + if (candidate.TrailingTrivia.Trim() != "") { + return candidate.TrailingTrivia; + } + } + } + + if (candidate == null && EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } // Represents module X { ... } public class LiteralModuleDecl : ModuleDecl, ICanFormat { @@ -587,6 +608,14 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return true; } + + protected override string GetTriviaContainingDocstring() { + if (Tok.TrailingTrivia.Trim() != "") { + return Tok.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } public class ExportSignature : TokenNode, IHasUsages { @@ -1349,7 +1378,7 @@ public override IEnumerable Assumptions() { } } -public class ClassDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICanFormat { +public class ClassDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICanFormat, IHasDocstring { public override string WhatKind { get { return "class"; } } public override bool CanBeRevealed() { return true; } [FilledInDuringResolution] public bool HasConstructor; // filled in (early) during resolution; true iff there exists a member that is a Constructor @@ -1472,6 +1501,24 @@ public virtual bool SetIndent(int indentBefore, TokenNewIndentCollector formatte return true; } + + protected override string GetTriviaContainingDocstring() { + IToken candidate = null; + foreach (var token in OwnedTokens) { + if (token.val == "{") { + candidate = token.Prev; + if (candidate.TrailingTrivia.Trim() != "") { + return candidate.TrailingTrivia; + } + } + } + + if (candidate == null && EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } public class DefaultClassDecl : ClassDecl { @@ -1524,7 +1571,7 @@ public ArrowTypeDecl(List tps, Function req, Function reads, Modu } } -public abstract class DatatypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICallable, ICanFormat { +public abstract class DatatypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, ICallable, ICanFormat, IHasDocstring { public override bool CanBeRevealed() { return true; } public readonly List Ctors; @@ -1682,6 +1729,16 @@ public bool SetIndent(int indent, TokenNewIndentCollector formatter) { return true; } + + protected override string GetTriviaContainingDocstring() { + foreach (var token in OwnedTokens) { + if (token.val == "=" && token.TrailingTrivia.Trim() != "") { + return token.TrailingTrivia; + } + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } public class IndDatatypeDecl : DatatypeDecl { @@ -1772,7 +1829,7 @@ public Type CreateType(List typeArgs) { } } -public class DatatypeCtor : Declaration, TypeParameter.ParentType { +public class DatatypeCtor : Declaration, TypeParameter.ParentType, IHasDocstring { public readonly bool IsGhost; public readonly List Formals; [ContractInvariantMethod] @@ -1808,6 +1865,14 @@ public string FullName { return "#" + EnclosingDatatype.FullName + "." + Name; } } + + protected override string GetTriviaContainingDocstring() { + if (EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } /// @@ -1880,6 +1945,7 @@ public CallableWrapper(ICallable callable, bool isGhostContext) protected ICallable cwInner => (ICallable)inner; public IToken Tok => cwInner.Tok; + public string WhatKind => cwInner.WhatKind; public string NameRelativeToModule => cwInner.NameRelativeToModule; public Specification Decreases => cwInner.Decreases; @@ -1903,6 +1969,10 @@ public class DontUseICallable : ICallable { public string FullSanitizedName { get { throw new cce.UnreachableException(); } } public bool AllowsNontermination { get { throw new cce.UnreachableException(); } } public IToken Tok { get { throw new cce.UnreachableException(); } } + public string GetDocstring(DafnyOptions options) { + throw new cce.UnreachableException(); + } + public string NameRelativeToModule { get { throw new cce.UnreachableException(); } } public Specification Decreases { get { throw new cce.UnreachableException(); } } public bool InferredDecreases { @@ -1939,7 +2009,7 @@ public NoContext(ModuleDefinition module) { public bool AllowsAllocation => true; } -public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat { +public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl, ICanFormat, IHasDocstring { public override string WhatKind { get { return "opaque type"; } } public override bool CanBeRevealed() { return true; } public readonly TypeParameter.TypeParameterCharacteristics Characteristics; @@ -2020,6 +2090,25 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { return true; } + + protected override string GetTriviaContainingDocstring() { + IToken openingBlock = null; + foreach (var token in OwnedTokens) { + if (token.val == "{") { + openingBlock = token; + } + } + + if (openingBlock != null && openingBlock.Prev.TrailingTrivia.Trim() != "") { + return openingBlock.Prev.TrailingTrivia; + } + + if (openingBlock == null && EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } public interface RedirectingTypeDecl : ICallable { @@ -2091,7 +2180,7 @@ public interface RevealableTypeDecl { TypeDeclSynonymInfo SynonymInfo { get; set; } } -public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, RedirectingTypeDecl { +public class NewtypeDecl : TopLevelDeclWithMembers, RevealableTypeDecl, RedirectingTypeDecl, IHasDocstring { public override string WhatKind { get { return "newtype"; } } public override bool CanBeRevealed() { return true; } public Type BaseType { get; set; } // null when refining @@ -2177,9 +2266,27 @@ public override bool IsEssentiallyEmpty() { // A "newtype" is not considered "essentially empty", because it always has a parent type to be resolved. return false; } + + protected override string GetTriviaContainingDocstring() { + IToken candidate = null; + foreach (var token in OwnedTokens) { + if (token.val == "{") { + candidate = token.Prev; + if (candidate.TrailingTrivia.Trim() != "") { + return candidate.TrailingTrivia; + } + } + } + + if (candidate == null && EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } -public abstract class TypeSynonymDeclBase : TopLevelDecl, RedirectingTypeDecl { +public abstract class TypeSynonymDeclBase : TopLevelDecl, RedirectingTypeDecl, IHasDocstring { public override string WhatKind { get { return "type synonym"; } } public TypeParameter.TypeParameterCharacteristics Characteristics; // the resolver may change the .EqualitySupport component of this value from Unspecified to InferredRequired (for some signatures that may immediately imply that equality support is required) public bool SupportsEquality { @@ -2273,6 +2380,27 @@ public override bool IsEssentiallyEmpty() { // A synonym/subset type is not considered "essentially empty", because it always has a parent type to be resolved. return false; } + + + + protected override string GetTriviaContainingDocstring() { + IToken openingBlock = null; + foreach (var token in OwnedTokens) { + if (token.val == "{") { + openingBlock = token; + } + } + + if (openingBlock != null && openingBlock.Prev.TrailingTrivia.Trim() != "") { + return openingBlock.Prev.TrailingTrivia; + } + + if (openingBlock == null && EndToken.TrailingTrivia.Trim() != "") { + return EndToken.TrailingTrivia; + } + + return GetTriviaContainingDocstringFromStartTokenOrNull(); + } } public class TypeSynonymDecl : TypeSynonymDeclBase, RevealableTypeDecl { diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index e66c98a474d..62066e48160 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -314,6 +314,7 @@ public enum IncludesModes { public IncludesModes PrintIncludesMode = IncludesModes.None; public int OptimizeResolution = 2; public bool IncludeRuntime = true; + public bool UseJavadocLikeDocstringRewriter = false; public bool DisableScopes = false; public int Allocated = 4; public bool UseStdin = false; @@ -326,7 +327,8 @@ public enum IncludesModes { public static string DefaultZ3Version = "4.12.1"; - public static readonly ReadOnlyCollection DefaultPlugins = new(new[] { SinglePassCompiler.Plugin }); + public static readonly ReadOnlyCollection DefaultPlugins = + new(new[] { SinglePassCompiler.Plugin, InternalDocstringRewritersPluginConfiguration.Plugin }); private IList cliPluginCache; public IList Plugins => cliPluginCache ??= ComputePlugins(); public List AdditionalPlugins = new(); diff --git a/Source/DafnyCore/Generic/Node.cs b/Source/DafnyCore/Generic/Node.cs index 61b32011a8f..5f5df7026aa 100644 --- a/Source/DafnyCore/Generic/Node.cs +++ b/Source/DafnyCore/Generic/Node.cs @@ -3,11 +3,13 @@ using System.Diagnostics; using System.Diagnostics.Contracts; using System.Linq; +using System.Text.RegularExpressions; using Microsoft.Boogie; using Microsoft.Dafny.Auditor; namespace Microsoft.Dafny; + public interface INode { RangeToken RangeToken { get; } @@ -21,6 +23,11 @@ public interface ICanFormat : INode { bool SetIndent(int indentBefore, TokenNewIndentCollector formatter); } +// A node that can have a docstring attached to it +public interface IHasDocstring : INode { + string GetDocstring(DafnyOptions options); +} + public abstract class Node : INode { public abstract IToken Tok { get; } @@ -107,6 +114,9 @@ public ISet Visit(Func beforeChildren = null, Action aft protected IReadOnlyList OwnedTokensCache; + private static readonly Regex StartDocstringExtractor = + new Regex($@"/\*\*(?{TriviaFormatterHelper.MultilineCommentContent})\*/"); + /// /// A token is owned by a node if it was used to parse this node, /// but is not owned by any of this Node's children @@ -164,6 +174,103 @@ public IEnumerable OwnedTokens { } public abstract RangeToken RangeToken { get; set; } + + // Docstring from start token is extracted only if using "/** ... */" syntax, and only the last one is considered + protected string GetTriviaContainingDocstringFromStartTokenOrNull() { + var matches = StartDocstringExtractor.Matches(StartToken.LeadingTrivia); + if (matches.Count > 0) { + return matches[^1].Value; + } + + if (StartToken.Prev.val is "|" or "{") { + matches = StartDocstringExtractor.Matches(StartToken.Prev.TrailingTrivia); + if (matches.Count > 0) { + return matches[^1].Value; + } + } + return null; + } + + // Applies plugin-defined docstring filters + public string GetDocstring(DafnyOptions options) { + var plugins = options.Plugins; + string trivia = GetTriviaContainingDocstring(); + if (string.IsNullOrEmpty(trivia)) { + return null; + } + + var rawDocstring = ExtractDocstring(trivia); + foreach (var plugin in plugins) { + foreach (var docstringRewriter in plugin.GetDocstringRewriters(options)) { + rawDocstring = docstringRewriter.RewriteDocstring(rawDocstring) ?? rawDocstring; + } + } + + return rawDocstring; + } + + private string ExtractDocstring(string trivia) { + var extraction = new Regex( + $@"(?(?[ \t]*)/\*(?{TriviaFormatterHelper.MultilineCommentContent})\*/)" + + $@"|(?// ?(?[^\r\n]*?)[ \t]*(?:{TriviaFormatterHelper.AnyNewline}|$))"); + var rawDocstring = new List() { }; + var matches = extraction.Matches(trivia); + for (var i = 0; i < matches.Count; i++) { + var match = matches[i]; + if (match.Groups["multiline"].Success) { + // For each line except the first, + // we need to remove the indentation on every line. + // The length of removed indentation is maximum the space before the first "/*" + 3 characters + // Additionally, if there is a "* " or a " *" or a " * ", we remove it as well + // provided it always started with a star. + var indentation = match.Groups["indentation"].Value; + var multilineContent = match.Groups["multilinecontent"].Value; + var newlineRegex = new Regex(TriviaFormatterHelper.AnyNewline); + var contentLines = newlineRegex.Split(multilineContent); + var starRegex = new Regex(@"^[ \t]*\*\ ?(?.*)$"); + var wasNeverInterrupted = true; + var localDocstring = ""; + for (var j = 0; j < contentLines.Length; j++) { + if (j != 0) { + localDocstring += "\n"; + } + var contentLine = contentLines[j]; + var lineMatch = starRegex.Match(contentLine); + if (lineMatch.Success && wasNeverInterrupted) { + localDocstring += lineMatch.Groups["remaining"].Value; + } else { + if (j == 0) { + localDocstring += contentLine.TrimStart(); + } else { + wasNeverInterrupted = false; + if (contentLine.StartsWith(indentation)) { + var trimmedIndentation = + contentLine.Substring(0, Math.Min(indentation.Length + 3, contentLine.Length)).TrimStart(); + var remaining = (contentLine.Length >= indentation.Length + 3 + ? contentLine.Substring(indentation.Length + 3) + : ""); + localDocstring += trimmedIndentation + remaining; + } else { + localDocstring += contentLine.Trim(); + } + } + } + } + + localDocstring = localDocstring.Trim(); + rawDocstring.Add(localDocstring); + } else if (match.Groups["singleline"].Success) { + rawDocstring.Add(match.Groups["singlelinecontent"].Value); + } + } + + return string.Join("\n", rawDocstring); + } + + // Unfiltered version that only returns the trivia containing the docstring + protected virtual string GetTriviaContainingDocstring() { + return null; + } } public abstract class TokenNode : Node { diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index a6d1edef795..79d9e9f7c29 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -164,6 +164,10 @@ Note that quantifier variable domains (<- ) are available in both syntax public static readonly Option IncludeRuntimeOption = new("--include-runtime", "Include the Dafny runtime as source in the target language."); + public static readonly Option UseJavadocLikeDocstringRewriterOption = new("--javadoclike-docstring-plugin", + "Rewrite docstrings using a simple Javadoc-to-markdown converter" + ); + public enum TestAssumptionsMode { None, Externs @@ -197,6 +201,8 @@ static CommonOptionBag() { } }); DafnyOptions.RegisterLegacyBinding(IncludeRuntimeOption, (options, value) => { options.IncludeRuntime = value; }); + DafnyOptions.RegisterLegacyBinding(UseJavadocLikeDocstringRewriterOption, + (options, value) => { options.UseJavadocLikeDocstringRewriter = value; }); DafnyOptions.RegisterLegacyBinding(WarnShadowing, (options, value) => { options.WarnShadowing = value; }); DafnyOptions.RegisterLegacyBinding(WarnMissingConstructorParenthesis, (options, value) => { options.DisallowConstructorCaseWithoutParentheses = value; }); diff --git a/Source/DafnyCore/Plugin.cs b/Source/DafnyCore/Plugin.cs index 639c13dcccd..01912774a9a 100644 --- a/Source/DafnyCore/Plugin.cs +++ b/Source/DafnyCore/Plugin.cs @@ -1,4 +1,5 @@ using System; +using System.Collections; using System.Collections.Generic; using System.Linq; using System.Reflection; @@ -10,6 +11,7 @@ namespace Microsoft.Dafny; public interface Plugin { public IEnumerable GetCompilers(DafnyOptions options); public IEnumerable GetRewriters(ErrorReporter reporter); + public IEnumerable GetDocstringRewriters(DafnyOptions options); } record ErrorPlugin(string AssemblyAndArgument, Exception Exception) : Plugin { @@ -21,6 +23,10 @@ public IEnumerable GetRewriters(ErrorReporter reporter) { return new[] { new ErrorRewriter(reporter, this) }; } + public IEnumerable GetDocstringRewriters(DafnyOptions options) { + return Enumerable.Empty(); + } + class ErrorRewriter : IRewriter { private readonly ErrorPlugin errorPlugin; @@ -49,6 +55,10 @@ public IEnumerable GetCompilers(DafnyOptions options) { public IEnumerable GetRewriters(ErrorReporter reporter) { return Configuration.GetRewriters(reporter).Select(rewriter => new PluginRewriter(reporter, rewriter)); } + + public IEnumerable GetDocstringRewriters(DafnyOptions options) { + return Configuration.GetDocstringRewriters(options); + } } /// diff --git a/Source/DafnyCore/Plugins/DocstringRewriter.cs b/Source/DafnyCore/Plugins/DocstringRewriter.cs new file mode 100644 index 00000000000..030800428b1 --- /dev/null +++ b/Source/DafnyCore/Plugins/DocstringRewriter.cs @@ -0,0 +1,19 @@ +namespace Microsoft.Dafny.Plugins; + +public abstract class DocstringRewriter { + /// Retrieves the content of what Dafny believes is the Docstring + /// and filters it. Note that the default rendering in VSCode is Markdown, + /// so since it's the major IDE that Dafny supports, you probably want to + /// have your docstring converter converts parts of the code to Markdown + /// As an example: + /// ``` + /// function Test(i: int): int + /// // Returns the number of + /// // numbers smaller than i + /// { ... } + /// ``` + /// The argument docstring will contain "Returns the number of\nnumbers smaller than i" + public virtual string RewriteDocstring(string extractedDocString) { + return extractedDocString; + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Plugins/PluginConfiguration.cs b/Source/DafnyCore/Plugins/PluginConfiguration.cs index e24fa499d13..1b1b2a3fb71 100644 --- a/Source/DafnyCore/Plugins/PluginConfiguration.cs +++ b/Source/DafnyCore/Plugins/PluginConfiguration.cs @@ -39,4 +39,13 @@ public virtual Rewriter[] GetRewriters(ErrorReporter errorReporter) { public virtual IExecutableBackend[] GetCompilers(DafnyOptions options) { return Array.Empty(); } -} + + /// + /// Override this method to provide docstring converters + /// + /// + /// A list of docstring converters implemented by this plugin, applied from left to right + public virtual DocstringRewriter[] GetDocstringRewriters(DafnyOptions options) { + return Array.Empty(); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Plugins/Rewriter.cs b/Source/DafnyCore/Plugins/Rewriter.cs index df0a80f1ca6..c382a30d76d 100644 --- a/Source/DafnyCore/Plugins/Rewriter.cs +++ b/Source/DafnyCore/Plugins/Rewriter.cs @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MIT +// SPDX-License-Identifier: MIT using System.Diagnostics.Contracts; namespace Microsoft.Dafny.Plugins { diff --git a/Source/DafnyCore/Rewriters/Rewriter.cs b/Source/DafnyCore/Rewriters/IRewriter.cs similarity index 79% rename from Source/DafnyCore/Rewriters/Rewriter.cs rename to Source/DafnyCore/Rewriters/IRewriter.cs index 9cec54a03f0..527bba5cec9 100644 --- a/Source/DafnyCore/Rewriters/Rewriter.cs +++ b/Source/DafnyCore/Rewriters/IRewriter.cs @@ -5,11 +5,7 @@ namespace Microsoft.Dafny { /// - /// A class that plugins should extend, in order to provide an extra Rewriter to the pipeline. - /// - /// If the plugin defines no PluginConfiguration, then Dafny will instantiate every sub-class - /// of Rewriter from the plugin, providing them with an ErrorReporter in the constructor - /// as the first and only argument. + /// Internal rewriters used in the resolution pipeline /// public abstract class IRewriter { /// @@ -17,20 +13,6 @@ public abstract class IRewriter { /// protected ErrorReporter Reporter; - /// - /// Constructor that accepts an ErrorReporter - /// You can obtain an ErrorReporter two following ways: - /// * Extend a PluginConfiguration class, and override the method GetRewriters(), whose first argument is an ErrorReporter - /// * Have no PluginConfiguration class, and an ErrorReporter will be provided to your class's constructor. - /// - /// Then you can use the protected field "reporter" like the following: - /// - /// reporter.Error(MessageSource.Compiler, token, "[Your plugin] Your error message here"); - /// - /// The token is usually obtained on expressions and statements in the field `tok` - /// If you do not have access to them, use moduleDefinition.GetFirstTopLevelToken() - /// - /// The error reporter. Usually outputs automatically to IDE or command-line protected internal IRewriter(ErrorReporter reporter) { Contract.Requires(reporter != null); this.Reporter = reporter; diff --git a/Source/DafnyCore/Rewriters/InternalDocstringRewritersPluginConfiguration.cs b/Source/DafnyCore/Rewriters/InternalDocstringRewritersPluginConfiguration.cs new file mode 100644 index 00000000000..4c939312550 --- /dev/null +++ b/Source/DafnyCore/Rewriters/InternalDocstringRewritersPluginConfiguration.cs @@ -0,0 +1,19 @@ +using Microsoft.Dafny.Compilers; +using Microsoft.Dafny.Plugins; + +namespace Microsoft.Dafny; + +public class InternalDocstringRewritersPluginConfiguration : Plugins.PluginConfiguration { + public static readonly InternalDocstringRewritersPluginConfiguration Singleton = new(); + public static readonly Plugin Plugin = new ConfiguredPlugin(Singleton); + + public override DocstringRewriter[] GetDocstringRewriters(DafnyOptions options) { + if (options.UseJavadocLikeDocstringRewriter) { + return new DocstringRewriter[] { + new JavadocLikeDocstringRewriter() + }; + } else { + return new DocstringRewriter[] { }; + } + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Rewriters/JavadocLikeDocstringRewriter.cs b/Source/DafnyCore/Rewriters/JavadocLikeDocstringRewriter.cs new file mode 100644 index 00000000000..029919e4d8f --- /dev/null +++ b/Source/DafnyCore/Rewriters/JavadocLikeDocstringRewriter.cs @@ -0,0 +1,56 @@ +using System; +using System.Text.RegularExpressions; + +namespace Microsoft.Dafny; + +// To use it in CLI or Dafny language server, use the option +// --javadoclike-docstring-plugin +// You can also create your own +public class JavadocLikeDocstringRewriter : Plugins.DocstringRewriter { + private const string DocTableStart = "\n| | |\n| --- | --- |"; + + public override string RewriteDocstring(string extractedDocString) { + var detectJavadoc = new Regex(@"(\r?\n|^)\s*(@param|@return)"); + if (!detectJavadoc.Match(extractedDocString).Success) { + return null; + } + var documentation = ""; + + var initialText = new Regex(@"^(?:(?!\r?\n\s*@)[\s\S])*").Match(extractedDocString).Value.Trim(); + documentation += initialText; + + var paramsRanges = new Regex(@"@param\s+(?\w+)\s+(?(?:(?!\n\s*@)[\s\S])*)"); + + var matches = paramsRanges.Matches(extractedDocString); + var tableRows = 0; + for (var i = 0; i < matches.Count; i++) { + var match = matches[i]; + var name = match.Groups["Name"].Value; + var description = EscapeNewlines(match.Groups["Description"].Value); + if (i == 0) { + if (tableRows++ == 0) { + documentation += DocTableStart; + } + documentation += "\n| **Params** | "; + } else { + documentation += "\n| | "; + } + documentation += $"**{name}** - {description} |"; + } + var returnsDoc = new Regex(@"@returns?\s+(?(?:(?!\n\s*@)[\s\S])*)"); + if (returnsDoc.Match(extractedDocString) is { Success: true } matched) { + var description = EscapeNewlines(matched.Groups["Description"].Value); + if (tableRows == 0) { + documentation += DocTableStart; + } + documentation += $"\n| **Returns** | {description} |"; + } + + return documentation; + } + + private static string EscapeNewlines(string content) { + var newlines = new Regex(@"\r?\n"); + return newlines.Replace(content, "
"); + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs index c00fcd8998f..e9641526d04 100644 --- a/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs +++ b/Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs @@ -6,6 +6,7 @@ using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; +using JetBrains.Annotations; using Microsoft.Dafny.LanguageServer.IntegrationTest.Util; using Xunit; using XunitAssertMessages; @@ -37,11 +38,11 @@ private async Task AssertHoverContains(TextDocumentItem documentItem, Position h Assert.Null(hover); return; } - AssertM.NotNull(hover, $"No hover message found at {hoverPosition}"); + AssertM.NotNull(hover, $"No hover message found at {hoverPosition}, was supposed to display {expectedContent}"); var markup = hover.Contents.MarkupContent; Assert.NotNull(markup); Assert.Equal(MarkupKind.Markdown, markup.Kind); - Assert.True(markup.Value.Contains(expectedContent), $"Could not find {expectedContent} in {markup.Value}"); + Assert.True(markup.Value.Contains(expectedContent), $"Could not find '{expectedContent}'\n in \n'{markup.Value}'"); } /// @@ -52,11 +53,17 @@ private async Task AssertHoverContains(TextDocumentItem documentItem, Position h /// at the place where a user would hover. /// /// - private async Task AssertHover(string sourceWithHovers) { - await SetUp(o => o.ProverOptions.Add("SOLVER=noop")); + /// + private async Task AssertHover(string sourceWithHovers, [CanBeNull] Action modifyOptions = null) { + await SetUp(o => { + o.ProverOptions.Add("SOLVER=noop"); + if (modifyOptions != null) { + modifyOptions(o); + } + }); sourceWithHovers = sourceWithHovers.TrimStart().Replace("\r", ""); // Might not be necessary // Split the source from hovering tasks - var hoverRegex = new Regex(@"\n\s*(?\^)\[(?.*)\](?=\n|$)"); + var hoverRegex = new Regex(@"\n//\s*(?\^)\[(?.*)\](?=\n|$)"); var source = hoverRegex.Replace(sourceWithHovers, ""); var hovers = hoverRegex.Matches(sourceWithHovers); var documentItem = CreateTestDocument(source); @@ -81,7 +88,7 @@ method DoIt() returns (x: int) { method CallDoIt() returns () { var x := DoIt(); - ^[```dafny\nmethod DoIt() returns (x: int)\n```] +// ^[```dafny\nmethod DoIt() returns (x: int)\n```] }"); } @@ -95,9 +102,9 @@ method M(dt: DT) { match dt { case C => case A | B => var x := (y => y)(1); assert x == 1; - ^[```dafny\nx: int\n```] - ^[```dafny\ny: int\n```] - ^[```dafny\ny: int\n```] +// ^[```dafny\nx: int\n```] +// ^[```dafny\ny: int\n```] +// ^[```dafny\ny: int\n```] } } @@ -105,9 +112,9 @@ method M2(dt: DT) { match dt { case C => case _ => var x := (y => y)(1); assert x == 1; - ^[```dafny\nx: int\n```] - ^[```dafny\ny: int\n```] - ^[```dafny\ny: int\n```] +// ^[```dafny\nx: int\n```] +// ^[```dafny\ny: int\n```] +// ^[```dafny\ny: int\n```] } } @@ -115,18 +122,18 @@ function F(dt: DT): int { match dt { case C => 0 case A | B => var x := (y => y)(1); assert x == 1; 0 - ^[```dafny\nx: int\n```] - ^[```dafny\ny: int\n```] - ^[```dafny\ny: int\n```] +// ^[```dafny\nx: int\n```] +// ^[```dafny\ny: int\n```] +// ^[```dafny\ny: int\n```] } } function F2(dt: DT): int { match dt { case C => 0 case _ => var x := (y => y)(1); assert x == 1; 0 - ^[```dafny\nx: int\n```] - ^[```dafny\ny: int\n```] - ^[```dafny\ny: int\n```] +// ^[```dafny\nx: int\n```] +// ^[```dafny\ny: int\n```] +// ^[```dafny\ny: int\n```] } } "); @@ -150,7 +157,7 @@ await AssertHover(@" method DoIt() { var x := new int[0]; var y := x.Length; - ^[```dafny\nconst array.Length: int\n```] +// ^[```dafny\nconst array.Length: int\n```] }"); } @@ -174,7 +181,7 @@ public async Task HoveringInvocationOfUnknownFunctionOrMethodReturnsNull() { await AssertHover(@" method DoIt() returns (x: int) { return GetX(); - ^[null] +// ^[null] }"); } @@ -187,7 +194,7 @@ class Test { method DoIt() { var x := """"; print x; - ^[```dafny\nx: string\n```] +// ^[```dafny\nx: string\n```] } }"); } @@ -201,7 +208,7 @@ class Test { method DoIt() { var x := 1; print this.x; - ^[```dafny\nvar Test.x: int\n```] +// ^[```dafny\nvar Test.x: int\n```] } }"); } @@ -217,7 +224,7 @@ method DoIt() { { var x := ""2""; print x; - ^[```dafny\nx: string\n```] +// ^[```dafny\nx: string\n```] } } }"); @@ -235,7 +242,7 @@ method DoIt() { var x := 2; } print x; - ^[```dafny\nx: string\n```] +// ^[```dafny\nx: string\n```] } }"); } @@ -249,7 +256,7 @@ class A { class B { var a: A; - ^[```dafny\nclass A\n```] +// ^[```dafny\nclass A\n```] constructor() { a := new A(); @@ -269,7 +276,7 @@ class B { constructor() { a := new A(); - ^[```dafny\nclass A\n```] +// ^[```dafny\nclass A\n```] } }"); } @@ -282,7 +289,7 @@ class A { } method DoIt(a: A) {} - ^[```dafny\nclass A\n```]"); +// ^[```dafny\nclass A\n```]"); } [Fact] @@ -290,7 +297,7 @@ public async Task HoveringParentTraitOfUserDefinedTypeReturnsTheParentTrait() { await AssertHover(@" trait Base {} class Sub extends Base {} - ^[```dafny\ntrait Base\n```]"); +// ^[```dafny\ntrait Base\n```]"); } [Fact] @@ -299,7 +306,7 @@ await AssertHover(@" datatype SomeType = SomeType { method AssertEqual(x: int, y: int) { var j:=x == y; - ^[```dafny\nx: int\n```] +// ^[```dafny\nx: int\n```] } }"); } @@ -316,7 +323,7 @@ method AssertEqual(x: int, y: int) { method Main() { var instance: SomeType; instance.AssertEqual(1, 2); - ^[```dafny\nmethod SomeType.AssertEqual(x: int, y: int)\n```] +// ^[```dafny\nmethod SomeType.AssertEqual(x: int, y: int)\n```] }"); } @@ -325,7 +332,7 @@ public async Task HoveringFormalReturnsFormalType() { await AssertHover(@" method f(i: int) { var r := i; - ^[```dafny\ni: int\n```] +// ^[```dafny\ni: int\n```] }"); } @@ -334,7 +341,7 @@ public async Task HoveringDeclarationVariableReturnsInferredVariableType() { await AssertHover(@" method f(i: int) { var r := i; - ^[```dafny\nr: int\n```] +// ^[```dafny\nr: int\n```] }"); } @@ -343,8 +350,8 @@ public async Task HoveringForallBoundVarReturnsBoundVarInferredType() { await AssertHover(@" method f(i: int) { var x:=forall j :: j + i == i + j; - ^[```dafny\nj: int\n```] - ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] }"); } @@ -353,8 +360,8 @@ public async Task HoveringExistsBoundVarReturnsBoundVarInferredType() { await AssertHover(@" method f(i: int) { var x:=exists j :: j + i == i; - ^[```dafny\nj: int\n```] - ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] }"); } @@ -364,8 +371,8 @@ await AssertHover(@" method f(i: int) { var x := {1, 2, 3}; var y := set j | j in x && j < 3; - ^[```dafny\nj: int\n```] - ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] }"); } @@ -374,8 +381,8 @@ public async Task HoveringMapBoundVarReturnsBoundVarInferredType() { await AssertHover(@" method f(i: int) { var m := map j : int | 0 <= j <= i :: j * j; - ^[```dafny\nj: int\n```] - ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] }"); } @@ -384,8 +391,8 @@ public async Task HoveringLambdaBoundVarReturnsBoundVarInferredType() { await AssertHover(@" method f(i: int) { var m := j => j * i; - ^[```dafny\nj: int\n```] - ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] }"); } @@ -394,8 +401,8 @@ public async Task HoveringForAllBoundVarInPredicateReturnsBoundVarInferredType() await AssertHover(@" ghost predicate f(i: int) { forall j :: j + i == i + j - ^[```dafny\nj: int\n```] - ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] +// ^[```dafny\nj: int\n```] }"); } @@ -408,8 +415,8 @@ ensures even(n) <==> n % 2 == 0 if n < 2 then n == 0 else even(n - 2) } by method { var x := n % 2 == 0; - ^[```dafny\nx: bool\n```] - ^[```dafny\nn: nat\n```] +// ^[```dafny\nx: bool\n```] +// ^[```dafny\nn: nat\n```] return x; }"); } @@ -419,8 +426,8 @@ public async Task HoveringLetInReturnsInferredType() { await AssertHover(@" function test(n: nat): nat { var i := n * 2; - ^[```dafny\ni: int\n```] - ^[```dafny\nn: nat\n```] +// ^[```dafny\ni: int\n```] +// ^[```dafny\nn: nat\n```] if i == 4 then 3 else 2 }"); } @@ -430,8 +437,8 @@ public async Task HoveringSpecificationBoundVariableReturnsInferredType() { await AssertHover(@" method returnBiggerThan(n: nat) returns (y: int) requires var y := 100; forall i :: i < n ==> i < y - ^[```dafny\ny: int\n```] - ^[```dafny\ni: int\n```] +// ^[```dafny\ny: int\n```] +// ^[```dafny\ni: int\n```] ensures forall i :: i > y ==> i > n { return n + 2; @@ -442,9 +449,9 @@ method returnBiggerThan(n: nat) returns (y: int) public async Task HoveringResultVarReturnsInferredType() { await AssertHover(@" function f(i: int): (r: int) - ^[```dafny\nr: int\n```] +// ^[```dafny\nr: int\n```] ensures r - i < 10 - ^[```dafny\nr: int\n```] +// ^[```dafny\nr: int\n```] { i + 2 }"); @@ -458,7 +465,7 @@ function f(i: int): Pos { if i <= 3 then Pos(i) else var r := f(i - 2); - ^[```dafny\nr: Pos\n```] +// ^[```dafny\nr: Pos\n```] Pos(r.line + 2) }"); } @@ -468,7 +475,7 @@ public async Task HoverIngResultTypeShouldNotCrash() { await AssertHover(@" datatype Position = Position(Line: nat) function ToRelativeIndependent(): (p: Position) - ^[```dafny\ndatatype Position\n```] +// ^[```dafny\ndatatype Position\n```] { Position(12) } @@ -481,16 +488,154 @@ await AssertHover(@" lemma dummy(e: int) { match e { case _ => var xx := 1; - ^[```dafny\nghost xx: int\n```] +// ^[```dafny\nghost xx: int\n```] } } method test(opt: int) { match(opt) case 1 => var s := 1; - ^[```dafny\ns: int\n```] +// ^[```dafny\ns: int\n```] } "); } + + [Fact] + public async Task HoverShouldDisplayComments() { + await AssertHover(@" +predicate pm() + // No comment for pm +{ true } + +/** Rich comment + * @param k The input + * that is ignored + * @param l The second input that is ignored + * @returns 1 no matter what*/ +function g(k: int, l: int): int { 1 } + +// No comment for pt +twostate predicate pt() { true } + +least predicate pl() + // No comment for pl +{ true } + +// A comment for pg +// That spans two lines +greatest predicate pg() { true } + +/** Returns an integer without guarantee + * @returns The integer + */ +method m() returns (i: int) { i := *; } + +/** The class C. Should be used like this: + * ```dafny + * new C(); + * ``` + */ +class C { + // Unformatted comment + static method m() {} + + // This is the constructor + constructor() {} + + /** Should be the number of x in C */ + var x: int + + const X: int + // The expected number of x +} + +function f(): int + /** Rich comment + * @returns 1 no matter what + */ +{ 1 } + +/** Rich comment for D */ +datatype D = DD(value: int) + +/* D whose value is even */ +type T = x: D | x.value % 2 == 0 witness DD(0) + +/* Even numbers hidden in a newtype */ +newtype Even = x: int | x % 2 == 0 + +/** A useful lemma */ +lemma lem() {} + +/** A useful greatest lemma */ +greatest lemma greatestLemma() {} + +/** A useful least lemma */ +least lemma leastLemma() {} + +/** A useful twostate lemma */ +twostate lemma twostateLemma() {} + +method test(d: D, t: T, e: Even) { +// ^[Rich comment for D] + // ^[D whose value is even] // Not working yet + // ^[Even numbers hidden in a newtype] // Not working yet + var x1 := pm(); +// ^[No comment for pm] + var x2 := pg(); +// ^[A comment for pg\nThat spans two lines] + var x3 := pl(); +// ^[No comment for pl] + var x4 := pt(); +// ^[No comment for pt] + var xg := g(0, 1); +// ^[Rich comment\n@param k The input\n that is ignored\n@param l The second input that is ignored\n@returns 1 no matter what] + C.m(); // TODO + // ^[Unformatted comment] // Does not work yet. + var c: C := new C(); +// ^[The class C. Should be used like this:\n```dafny\nnew C();\n```] + var xc := c.x; +// ^[Should be the number of x in C] + var xx := c.X; +// ^[The expected number of x] + var xf := f(); +// ^[Rich comment\n@returns 1 no matter what] + lem(); +//^[A useful lemma] + greatestLemma(); +//^[A useful greatest lemma] + leastLemma(); +//^[A useful least lemma] + twostateLemma(); +//^[A useful twostate lemma] +}"); + await AssertHover(@" +/** Rich comment + * @param k The input + * that is ignored + * @param l The second input that is ignored + * @returns 1 no matter what*/ +function g(k: int, l: int): int { 1 } + +/** Returns an integer without guarantee + * @returns The integer + */ +method m() returns (i: int) { i := *; } + +function f(): int + /** Rich comment + * @returns 1 no matter what + */ +{ 1 } + +method test() { + var xg := g(0, 1); +// ^[Rich comment\n| | |\n| --- | --- |\n| **Params** | **k** - The input
that is ignored |\n| | **l** - The second input that is ignored |\n| **Returns** | 1 no matter what |] + var i := m(); +// ^[Unformatted comment] // Does not work yet. + var xf := f(); +// ^[Rich comment\n| | |\n| --- | --- |\n| **Returns** | 1 no matter what |] +}", o => o.Set(CommonOptionBag.UseJavadocLikeDocstringRewriterOption, true)); + } } } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs index 467160d923c..9b31223ce29 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs @@ -346,7 +346,8 @@ private static Hover CreateMarkdownHover(string information) { } private string CreateSymbolMarkdown(ILocalizableSymbol symbol, CancellationToken cancellationToken) { - return $"```dafny\n{symbol.GetDetailText(options, cancellationToken)}\n```"; + var docString = symbol.Node is IHasDocstring nodeWithDocstring ? nodeWithDocstring.GetDocstring(options) : ""; + return (docString + $"\n```dafny\n{symbol.GetDetailText(options, cancellationToken)}\n```").TrimStart(); } } } diff --git a/Source/DafnyLanguageServer/Language/Symbols/FieldSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/FieldSymbol.cs index 9ec8511dc7b..857bd56ecb2 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/FieldSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/FieldSymbol.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public class FieldSymbol : MemberSymbol, ILocalizableSymbol { public Field Declaration { get; } - public object Node => Declaration; + public INode Node => Declaration; public FieldSymbol(ISymbol? scope, Field field) : base(scope, field) { Declaration = field; diff --git a/Source/DafnyLanguageServer/Language/Symbols/FunctionSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/FunctionSymbol.cs index 417f0022bca..2c3501ab294 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/FunctionSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/FunctionSymbol.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public class FunctionSymbol : MemberSymbol, ILocalizableSymbol { public Function Declaration { get; } - public object Node => Declaration; + public INode Node => Declaration; public IList Parameters { get; } = new List(); diff --git a/Source/DafnyLanguageServer/Language/Symbols/ILocalizableSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/ILocalizableSymbol.cs index 0a06208186a..f521f41e5fb 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/ILocalizableSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/ILocalizableSymbol.cs @@ -1,5 +1,5 @@ using System.Threading; -using AstNode = System.Object; +using AstNode = Microsoft.Dafny.INode; namespace Microsoft.Dafny.LanguageServer.Language.Symbols { /// diff --git a/Source/DafnyLanguageServer/Language/Symbols/MethodSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/MethodSymbol.cs index f996d08e9a6..c7fe3744c55 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/MethodSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/MethodSymbol.cs @@ -8,7 +8,7 @@ public class MethodSymbol : MemberSymbol, ILocalizableSymbol { /// Gets the method node representing the declaration of this symbol. /// public Method Declaration { get; } - public object Node => Declaration; + public INode Node => Declaration; /// /// Gets the method parameters. diff --git a/Source/DafnyLanguageServer/Language/Symbols/ModuleSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/ModuleSymbol.cs index 710d473883e..71e55841c5c 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/ModuleSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/ModuleSymbol.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public class ModuleSymbol : Symbol, ILocalizableSymbol { public ModuleDefinition Declaration { get; } - public object Node => Declaration; + public INode Node => Declaration; public ISet Declarations { get; } = new HashSet(); diff --git a/Source/DafnyLanguageServer/Language/Symbols/ScopeSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/ScopeSymbol.cs index d99f4933a7f..a7d3720e790 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/ScopeSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/ScopeSymbol.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public class ScopeSymbol : Symbol, ILocalizableSymbol { - public object Node { get; } + public INode Node { get; } public readonly IToken BodyStartToken; public readonly IToken BodyEndToken; public List Symbols { get; } = new(); diff --git a/Source/DafnyLanguageServer/Language/Symbols/TypeWithMembersSymbolBase.cs b/Source/DafnyLanguageServer/Language/Symbols/TypeWithMembersSymbolBase.cs index ee2b8d758fc..4764681d257 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/TypeWithMembersSymbolBase.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/TypeWithMembersSymbolBase.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public abstract class TypeWithMembersSymbolBase : Symbol, ILocalizableSymbol { - public abstract object Node { get; } + public abstract INode Node { get; } public IList Members { get; } = new List(); @@ -16,7 +16,7 @@ protected TypeWithMembersSymbolBase(ISymbol? scope, string name) : base(scope, n public abstract class TypeWithMembersSymbolBase : TypeWithMembersSymbolBase where TNode : TopLevelDeclWithMembers { public TNode Declaration { get; } - public override object Node => Declaration; + public override Node Node => Declaration; protected TypeWithMembersSymbolBase(ISymbol? scope, TNode declaration) : base(scope, declaration.Name) { Declaration = declaration; diff --git a/Source/DafnyLanguageServer/Language/Symbols/ValueTypeSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/ValueTypeSymbol.cs index d1d59a12491..08120b2d894 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/ValueTypeSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/ValueTypeSymbol.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public class ValueTypeSymbol : Symbol, ILocalizableSymbol { public ValuetypeDecl Declaration { get; } - public object Node => Declaration; + public INode Node => Declaration; public IList Members { get; } = new List(); diff --git a/Source/DafnyLanguageServer/Language/Symbols/VariableSymbol.cs b/Source/DafnyLanguageServer/Language/Symbols/VariableSymbol.cs index 694074bbb52..b397124c18e 100644 --- a/Source/DafnyLanguageServer/Language/Symbols/VariableSymbol.cs +++ b/Source/DafnyLanguageServer/Language/Symbols/VariableSymbol.cs @@ -3,7 +3,7 @@ namespace Microsoft.Dafny.LanguageServer.Language.Symbols { public class VariableSymbol : Symbol, ILocalizableSymbol { public IVariable Declaration { get; } - public object Node => Declaration; + public INode Node => Declaration; public VariableSymbol(ISymbol? scope, IVariable variable) : base(scope, variable.Name) { Declaration = variable; diff --git a/Source/DafnyLanguageServer/ServerCommand.cs b/Source/DafnyLanguageServer/ServerCommand.cs index 09399fe9255..35aea9985c7 100644 --- a/Source/DafnyLanguageServer/ServerCommand.cs +++ b/Source/DafnyLanguageServer/ServerCommand.cs @@ -48,6 +48,7 @@ related locations LineVerificationStatus, VerifySnapshots, CommonOptionBag.EnforceDeterminism, + CommonOptionBag.UseJavadocLikeDocstringRewriterOption }.Concat(ICommandSpec.VerificationOptions). Concat(ICommandSpec.ResolverOptions); diff --git a/Source/DafnyPipeline.Test/DocstringTest.cs b/Source/DafnyPipeline.Test/DocstringTest.cs new file mode 100644 index 00000000000..906f1f19c19 --- /dev/null +++ b/Source/DafnyPipeline.Test/DocstringTest.cs @@ -0,0 +1,437 @@ +#nullable enable +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text.RegularExpressions; +using Bpl = Microsoft.Boogie; +using BplParser = Microsoft.Boogie.Parser; +using Microsoft.Dafny; +using Xunit; + +namespace DafnyPipeline.Test { + + // Simple test cases (FormatterWorksFor with only one argument) + // consist of removing all the indentation from the program, + // adding it through the formatter, and checking if we obtain the initial result + // + // Advanced test cases consist of passing the program and its expected result after indentation + // + // Every test is performed with all three newline styles + // Every formatted program is formatted again to verify that it stays the same. + public class DocstringTest { + enum Newlines { + LF, + CR, + CRLF + }; + + private Newlines currentNewlines; + + [Fact] + public void DocstringWorksForFunctions() { + DocstringWorksFor(@" +function Test1(i: int): int + // Test1 computes an int + // It takes an int and adds 1 to it +{ i + 1 } + +function Test2(i: int): int + //Test2 computes an int + //It takes an int and adds 2 to it +{ i + 2 } +// Trailing comment + +// Test3 computes an int +// It takes an int and adds 3 to it +ghost function Test3(i: int): int +{ i + 3 } + +// this is not a docstring but can be used as a TODO +function Test4(i: int): int + // Test4 computes an int + // It takes an int and adds 4 to it +{ i + 4 } + +function Test5(i: int): int + /* Test5 computes an int + * It takes an int and adds 5 to it */ +{ i + 5 } + +function Test6(i: int): int +/** Test6 computes an int + * It takes an int and adds 6 to it */ + +function Test7(i: int): (j: int) + /* Test7 computes an int + It takes an int and adds 7 to it */ +{ i + 7 } + +function Test8(i: int): int + /* Test8 computes an int + It takes an int and adds 8 to it */ +{ i + 8 } + +function Test9(i: int): int /* + Test9 computes an int + It takes an int and adds 9 to it */ +{ i + 9 } + +function Test10(i: int): int + /* Test10 computes an int + It takes an int and adds 10 to it */ +{ i + 10 } + +function Test11(i: int): int + /** Test11 computes an int + * It takes an int and adds 11 to it */ +{ i + 11 } +", Enumerable.Range(1, 9).Select(i => + ($"Test{i}", (string?)$"Test{i} computes an int\nIt takes an int and adds {i} to it") + ).Concat( + new List<(string, string?)>() { + ($"Test10", $"Test10 computes an int\n It takes an int and adds 10 to it"), + ($"Test11", $"Test11 computes an int\n It takes an int and adds 11 to it") + } + ).ToList()); + } + + [Fact] + public void DocstringWorksForPredicate() { + DocstringWorksFor(@" +class X { + static predicate Test1(i: int) + // Test1 checks if an int + // is equal to 1 + { i == 1 } + // Unrelated trailing comment + + // Test2 checks if an int + // is equal to 2 + static predicate Test2(i: int) + { i == 2 } +} +", new List<(string nodeTokenValue, string? expectedDocstring)>() { + ("Test1", "Test1 checks if an int\nis equal to 1"), + ("Test2", "Test2 checks if an int\nis equal to 2")}); + } + + [Fact] + public void DocstringWorksForMethodsAndLemmas() { + DocstringWorksFor(@" +/** ComputeThing prints something to the screen */ +method ComputeThing(i: int) returns (j: int) +{ print i; } +// Unattached comment + +// Unattached comment +lemma ComputeThing2(i: int) returns (j: int) + // ComputeThing2 prints something to the screen + requires i == 2 +{ print i; } + +// Unattached comment +method ComputeThing3(i: int) returns (j: int) + // ComputeThing3 prints something to the screen + +// Unattached comment +method ComputeThing4(i: int) + // ComputeThing4 prints something to the screen + requires i == 2 +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("ComputeThing", "ComputeThing prints something to the screen"), + ("ComputeThing2", "ComputeThing2 prints something to the screen"), + ("ComputeThing3", "ComputeThing3 prints something to the screen"), + ("ComputeThing4", "ComputeThing4 prints something to the screen") + }); + } + [Fact] + public void DocstringWorksForConst() { + DocstringWorksFor(@" +class X { + const x2 := 29 + // The biggest prime number less than 30 + + /** The biggest prime number less than 20 */ + const x1 := 19 + + // Unrelated todo + const x3 := 37 + // The biggest prime number less than 40 +} +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("x1", "The biggest prime number less than 20"), + ("x2", "The biggest prime number less than 30"), + ("x3", "The biggest prime number less than 40")}); + } + + [Fact] + public void DocstringWorksForSubsetType() { + DocstringWorksFor(@" +type Odd = x: int | x % 2 == 1 witness 1 +// Type of numbers that are not divisible by 2 + +/** Type of numbers divisible by 2 */ +type Even = x: int | x % 2 == 1 witness 1 + +// Unrelated comment +type Weird = x: int | x % 2 == x % 3 witness 0 +// Type of numbers whose remainder modulo 2 or 3 is the same + +// Unattached comment +newtype Digit = x: int | 0 <= x < 10 +// A single digit + +/** A hex digit */ +newtype HexDigit = x: int | 0 <= x < 16 + +newtype BinDigit = x: int | 0 <= x < 2 witness 1 +// A binary digit +{ + function flip(): BinDigit { + 1 - this + } +} + +// Unrelated comment +type Weird = x: int | x % 2 == x % 3 witness 0 +// Type of numbers whose remainder modulo 2 or 3 is the same + + +// Unattached comment +type ZeroOrMore = nat +// ZeroOrMore is the same as nat + +/** ZeroOrMore2 is the same as nat */ +type ZeroOrMore2 = nat + +// Unattached comment +type OpaqueType +// OpaqueType has opaque methods so you don't see them +{ +} + +/** OpaqueType2 has opaque methods so you don't see them */ +type OpaqueType2 +{ +} +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("Odd", "Type of numbers that are not divisible by 2"), + ("Even", "Type of numbers divisible by 2"), + ("Weird", "Type of numbers whose remainder modulo 2 or 3 is the same"), + ("Digit", "A single digit"), + ("HexDigit", "A hex digit"), + ("BinDigit", "A binary digit"), + ("ZeroOrMore", "ZeroOrMore is the same as nat"), + ("ZeroOrMore2", "ZeroOrMore2 is the same as nat"), + ("OpaqueType", "OpaqueType has opaque methods so you don't see them"), + ("OpaqueType2", "OpaqueType2 has opaque methods so you don't see them") + }); + } + + [Fact] + public void DocstringWorksForDatatypes() { + DocstringWorksFor(@" +// Unrelated comment +datatype State = + // A typical log message from a process monitoring + | // Unrelated comment + Begin(time: int) + // The beginning of the process + | // Unrelated comment + End(time: int) + // The end of the process + +/** Another typical log message from a process monitoring */ +datatype State2 = + | /** The start of the process */ + Start(time: int) + | /** The finishing state of the process */ + Finish(time: int) + | // Not a docstring + Idle(time: int) +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("State", "A typical log message from a process monitoring"), + ("Begin", "The beginning of the process"), + ("End", "The end of the process"), + ("State2", "Another typical log message from a process monitoring"), + ("Start", "The start of the process"), + ("Finish", "The finishing state of the process"), + ("Idle", null) + }); + } + + + [Fact] + public void DocstringWorksForClassAndTraits() { + DocstringWorksFor(@" +trait X +// A typical base class +{} + +// Unattached comment +trait T1 extends X +// A typical extending trait +{} + +/** A typical extending trait with an even number */ +trait T2 extends X +{} + +// Unrelated comment +class A extends T + // A typical example of a class extending a trait +{} + +/** Another typical example of a class extending a trait */ +class A2 extends T +{} +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("X", "A typical base class"), + ("T1", "A typical extending trait"), + ("T2", "A typical extending trait with an even number"), + ("A", "A typical example of a class extending a trait"), + ("A2", "Another typical example of a class extending a trait") + }); + } + + + [Fact] + public void DocstringWorksForExport() { + DocstringWorksFor(@" +module Test { + /** You only get the signatures of f and g */ + export hidden provides f + provides g + + // Unattached comment + export consistent + // You get the definition of g but not f + provides f + reveals g + + /** You get both the definition of f and g */ + export full provides f + reveals g + + function g(): int { + f() + f() + } + function f(): int { + 1 + } +} +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("hidden", "You only get the signatures of f and g"), + ("consistent", "You get the definition of g but not f"), + ("full", "You get both the definition of f and g") + }); + } + + [Fact] + public void DocstringWorksForModules() { + DocstringWorksFor(@" +// Unattached comment +module A + // A is the most interesting module +{} + +// Unattached comment +module B refines A + // But it can be refined +{} +// Unattached comment + +/** Clearly, modules can be abstract as well */ +abstract module C +{} +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("A", "A is the most interesting module"), + ("B", "But it can be refined"), + ("C", "Clearly, modules can be abstract as well") + }); + } + + [Fact] + public void DocstringWorksForIterators() { + DocstringWorksFor(@" +/** Iter is interesting */ +iterator Iter(x: int) yields (y: int) + requires A: 0 <= x +{ +} + +// Unattached comment +iterator Iter2(x: int) yields (y: int) + // Iter2 is interesting + requires A: 0 <= x +{ +} +", new List<(string nodeTokenValue, string? expectedDocstring)> { + ("Iter", "Iter is interesting"), + ("Iter2", "Iter2 is interesting") + }); + } + + protected Node? FindNode(Node? node, Func nodeFinder) { + if (node == null) { + return node; + } + if (nodeFinder(node)) { + return node; + } else { + foreach (var childNode in node.PreResolveChildren) { + if (FindNode(childNode, nodeFinder) is { } found) { + return found; + } + } + + return null; + } + } + + protected void DocstringWorksFor(string source, string nodeTokenValue, string? expectedDocstring) { + DocstringWorksFor(source, new List<(string nodeTokenValue, string? expectedDocstring)>() { + (nodeTokenValue, expectedDocstring) + }); + } + + protected void DocstringWorksFor(string source, List<(string nodeTokenValue, string? expectedDocstring)> tests) { + var options = DafnyOptions.Create(); + BatchErrorReporter reporter = new BatchErrorReporter(options); + var newlineTypes = Enum.GetValues(typeof(Newlines)); + foreach (Newlines newLinesType in newlineTypes) { + currentNewlines = newLinesType; + // This formatting test will remove all the spaces at the beginning of the line + // and then recompute it. The result should be the same string. + var programString = AdjustNewlines(source); + ModuleDecl module = new LiteralModuleDecl(new DefaultModuleDefinition(), null); + Microsoft.Dafny.Type.ResetScopes(); + BuiltIns builtIns = new BuiltIns(options); + Parser.Parse(programString, "virtual", "virtual", module, builtIns, reporter); + var dafnyProgram = new Program("programName", module, builtIns, reporter); + if (reporter.ErrorCount > 0) { + var error = reporter.AllMessages[ErrorLevel.Error][0]; + Assert.False(true, $"{error.Message}: line {error.Token.line} col {error.Token.col}"); + } + + foreach (var (nodeTokenValue, expectedDocstring) in tests) { + var targetNode = FindNode(dafnyProgram, node => node.Tok.val == nodeTokenValue); + if (targetNode == null) { + Assert.NotNull(targetNode); + } + + var docString = targetNode.GetDocstring(options); + Assert.Equal(expectedDocstring, docString); + } + } + } + + private string AdjustNewlines(string programString) { + return currentNewlines switch { + Newlines.LF => new Regex("\r?\n").Replace(programString, "\n"), + Newlines.CR => new Regex("\r?\n").Replace(programString, "\r"), + _ => new Regex("\r?\n").Replace(programString, "\r\n") + }; + } + } +} diff --git a/docs/dev/news/docstring.feat b/docs/dev/news/docstring.feat new file mode 100644 index 00000000000..67514e4843b --- /dev/null +++ b/docs/dev/news/docstring.feat @@ -0,0 +1,4 @@ +* Added `.GetDocstring(DafnyOptions)` to every AST node +* Plugin support for custom Docstring formatter, +* Activatable plugin to support a subset of Javadoc through `--javadoclike-docstring-plugin` +* Support for displaying docstring in VSCode \ No newline at end of file