From 28d4c891be182db6e07638722284c5296bf06e0a Mon Sep 17 00:00:00 2001 From: Daniel Schoepe Date: Mon, 16 Sep 2024 15:56:51 -0700 Subject: [PATCH] Add missing PreResolve plugin hook This hook is described in the [documentation](https://dafny.org/latest/DafnyRef/DafnyRef#sec-plugins) but wasn't actually provided to plugins. --- Source/DafnyCore/Plugins/Rewriter.cs | 8 ++++++++ Source/DafnyCore/Rewriters/PluginRewriter.cs | 4 ++++ 2 files changed, 12 insertions(+) diff --git a/Source/DafnyCore/Plugins/Rewriter.cs b/Source/DafnyCore/Plugins/Rewriter.cs index 973e6c5401f..4a2416ad145 100644 --- a/Source/DafnyCore/Plugins/Rewriter.cs +++ b/Source/DafnyCore/Plugins/Rewriter.cs @@ -32,6 +32,14 @@ public virtual void PostResolve(Program program) { Contract.Requires(program != null); } + /// + /// Override this method to perform changes to the AST of a module before resolution. + /// You can also report warnings and errors using reporter.Error + /// + /// The module before resolution + public virtual void PreResolve(ModuleDefinition module) { + } + /// /// Override this method to obtain the resolved module before the translation pipeline occurs /// after the individual PostResolve on every module diff --git a/Source/DafnyCore/Rewriters/PluginRewriter.cs b/Source/DafnyCore/Rewriters/PluginRewriter.cs index 729a7a9bc01..07b4b6b1c90 100644 --- a/Source/DafnyCore/Rewriters/PluginRewriter.cs +++ b/Source/DafnyCore/Rewriters/PluginRewriter.cs @@ -15,6 +15,10 @@ internal override void PostResolve(Program program) { internalRewriter.PostResolve(program); } + internal override void PreResolve(ModuleDefinition module) { + internalRewriter.PreResolve(module); + } + internal override void PreVerify(ModuleDefinition module) { internalRewriter.PreVerify(module); }