-
Notifications
You must be signed in to change notification settings - Fork 258
/
DafnyExecutableBackend.cs
51 lines (39 loc) · 1.84 KB
/
DafnyExecutableBackend.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
using System;
using System.Collections.Generic;
using System.Collections.ObjectModel;
using System.Diagnostics;
using System.Diagnostics.Contracts;
using System.IO;
using System.Linq;
using Dafny;
namespace Microsoft.Dafny.Compilers;
public abstract class DafnyExecutableBackend : ExecutableBackend {
protected virtual bool PreventShadowing => true;
protected virtual bool CanEmitUncompilableCode => true;
protected DafnyWrittenCodeGenerator DafnyCodeGenerator;
protected DafnyExecutableBackend(DafnyOptions options) : base(options) {
}
protected override SinglePassCodeGenerator CreateCodeGenerator() {
// becomes this.compiler
return new DafnyCodeGenerator(Options, Reporter, PreventShadowing, CanEmitUncompilableCode);
}
protected abstract DafnyWrittenCodeGenerator CreateDafnyWrittenCompiler();
public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<string> otherFileNames) {
base.OnPreCompile(reporter, otherFileNames);
DafnyCodeGenerator = CreateDafnyWrittenCompiler();
}
public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
ProcessTranslationRecords(dafnyProgram, dafnyProgramName, output);
CheckInstantiationReplaceableModules(dafnyProgram);
ProcessOuterModules(dafnyProgram);
((DafnyCodeGenerator)codeGenerator).Start();
codeGenerator.Compile(dafnyProgram, new ConcreteSyntaxTree());
var dast = ((DafnyCodeGenerator)codeGenerator).Build();
var o = DafnyCodeGenerator.Compile((Sequence<DAST.Module>)Sequence<DAST.Module>.FromArray(dast.ToArray()));
output.Write(o.ToVerbatimString(false));
}
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree output) {
var o = DafnyCodeGenerator.EmitCallToMain(mainMethod.FullSanitizedName);
output.Write(o.ToVerbatimString(false));
}
}