diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 10:51:44 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 10:51:44 -0700 |
| commit | 674e30357980e1192ac532f4bd16c529cedc7fdc (patch) | |
| tree | 583d3eca7e0d40bb4753f25d4dbb3069e3dea9b5 /Source/Dafny/Rewriter.cs | |
| parent | 8a0df70ffb8d57d1bd210ce2e1c9522ba0967365 (diff) | |
Draft out a more advanced version of trigger generation
This new version will include a cleaner pipeline, and trigger splitting.
Diffstat (limited to 'Source/Dafny/Rewriter.cs')
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 46 |
1 files changed, 40 insertions, 6 deletions
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index cb71b80d..4e274189 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -39,22 +39,56 @@ namespace Microsoft.Dafny }
public class TriggerGeneratingRewriter : IRewriter {
+ Triggers.QuantifierCollectionsFinder finder;
+
internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {
Contract.Requires(reporter != null);
+ this.finder = new Triggers.QuantifierCollectionsFinder(reporter);
+ }
+
+ internal override void PostResolve(ModuleDefinition m) {
+ foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { //CLEMENT
+ if (decl is Function) {
+ var function = (Function)decl;
+ finder.Visit(function.Ens, null);
+ finder.Visit(function.Req, null);
+ if (function.Body != null) {
+ finder.Visit(function.Body, null);
+ }
+ } else if (decl is Method) {
+ var method = (Method)decl;
+ finder.Visit(method.Ens, null);
+ finder.Visit(method.Req, null);
+ if (method.Body != null) {
+ finder.Visit(method.Body, null);
+ }
+ }
+ }
+ }
+ }
+
+ internal class QuantifierSplittingRewriter : IRewriter {
+ internal QuantifierSplittingRewriter(ErrorReporter reporter) : base(reporter) {
+ Contract.Requires(reporter != null);
}
internal override void PostResolve(ModuleDefinition m) {
+ var splitter = new Triggers.QuantifierSplitter();
foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
if (decl is Function) {
var function = (Function)decl;
- //TriggerGenerator.AddTriggers(function.Ens, Resolver);
- //TriggerGenerator.AddTriggers(function.Req, Resolver);
- //TriggerGenerator.AddTriggers(function.Body, Resolver);
+ splitter.Visit(function.Ens);
+ splitter.Visit(function.Req);
+ if (function.Body != null) {
+ splitter.Visit(function.Body);
+ }
} else if (decl is Method) {
var method = (Method)decl;
- //TriggerGenerator.AddTriggers(method.Ens, Resolver);
- //TriggerGenerator.AddTriggers(method.Req, Resolver);
- //TriggerGenerator.AddTriggers(method.Body, Resolver);
+ splitter.Visit(method.Ens);
+ splitter.Visit(method.Req);
+ if (method.Body != null) {
+ splitter.Visit(method.Body);
+ }
}
}
}
|