diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:12:36 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 22:12:36 -0700 |
| commit | 487c6e48d305d57994b801440d4b62f1a4bfdd06 (patch) | |
| tree | b9fbca7af347050072d6505f44a9ae3ccdf7d3a1 | |
| parent | e5f9a4cbf74f7794ad13b2a5bd831fd54c20629c (diff) | |
Factor out some AST visiting code
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 54 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 32 |
2 files changed, 56 insertions, 30 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index ffd6df63..89bba760 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -7725,6 +7725,33 @@ namespace Microsoft.Dafny { public void Visit(IEnumerable<MaybeFreeExpression> exprs) {
exprs.Iter(Visit);
}
+ public void Visit(IEnumerable<FrameExpression> exprs) {
+ exprs.Iter(Visit);
+ }
+ public void Visit(ICallable decl) {
+ if (decl is Function) {
+ Visit((Function)decl);
+ } else if (decl is Method) {
+ Visit((Method)decl);
+ }
+ //FIXME More?
+ }
+ public void Visit(Method method) {
+ Visit(method.Ens);
+ Visit(method.Req);
+ Visit(method.Mod.Expressions);
+ Visit(method.Decreases.Expressions);
+ if (method.Body != null) { Visit(method.Body); }
+ //FIXME More?
+ }
+ public void Visit(Function function) {
+ Visit(function.Ens);
+ Visit(function.Req);
+ Visit(function.Reads);
+ Visit(function.Decreases.Expressions);
+ if (function.Body != null) { Visit(function.Body); }
+ //FIXME More?
+ }
protected virtual void VisitOneExpr(Expression expr) {
Contract.Requires(expr != null);
// by default, do nothing
@@ -7771,6 +7798,33 @@ namespace Microsoft.Dafny { public void Visit(IEnumerable<MaybeFreeExpression> exprs, State st) {
exprs.Iter(e => Visit(e, st));
}
+ public void Visit(IEnumerable<FrameExpression> exprs, State st) {
+ exprs.Iter(e => Visit(e, st));
+ }
+ public void Visit(ICallable decl, State st) {
+ if (decl is Function) {
+ Visit((Function)decl, st);
+ } else if (decl is Method) {
+ Visit((Method)decl, st);
+ }
+ //FIXME More?
+ }
+ public void Visit(Method method, State st) {
+ Visit(method.Ens, st);
+ Visit(method.Req, st);
+ Visit(method.Mod.Expressions, st);
+ Visit(method.Decreases.Expressions, st);
+ if (method.Body != null) { Visit(method.Body, st); }
+ //FIXME More?
+ }
+ public void Visit(Function function, State st) {
+ Visit(function.Ens, st);
+ Visit(function.Req, st);
+ Visit(function.Reads, st);
+ Visit(function.Decreases.Expressions, st);
+ if (function.Body != null) { Visit(function.Body, st); }
+ //FIXME More?
+ }
/// <summary>
/// Visit one expression proper. This method is invoked before it is invoked on the
/// sub-parts (sub-expressions and sub-statements). A return value of "true" says to
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 83f49a12..230d9349 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -47,21 +47,7 @@ namespace Microsoft.Dafny var finder = new Triggers.QuantifierCollector(reporter);
foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
- 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);
- }
- }
+ finder.Visit(decl, null);
}
var triggersCollector = new Triggers.TriggersCollector();
@@ -80,21 +66,7 @@ namespace Microsoft.Dafny 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;
- 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;
- splitter.Visit(method.Ens);
- splitter.Visit(method.Req);
- if (method.Body != null) {
- splitter.Visit(method.Body);
- }
- }
+ splitter.Visit(decl);
}
}
}
|