forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
LibraryBackend.cs
92 lines (69 loc) · 3.16 KB
/
LibraryBackend.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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
using System;
using System.Collections.Generic;
using System.Collections.ObjectModel;
using System.IO;
using System.IO.Compression;
using System.Linq;
using DafnyCore;
namespace Microsoft.Dafny.Compilers;
public class LibraryBackend : ExecutableBackend {
public LibraryBackend(DafnyOptions options) : base(options) {
}
public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { };
public override string TargetName => "Dafny Library (.doo)";
public override bool IsStable => false;
public override string TargetExtension => "doo";
public override string TargetId => "lib";
public override string TargetBaseDir(string dafnyProgramName) =>
$"{Path.GetFileNameWithoutExtension(dafnyProgramName)}-lib";
public override bool TextualTargetIsExecutable => false;
public override bool SupportsInMemoryCompilation => false;
public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
Feature.LegacyCLI,
Feature.RuntimeCoverageReport
};
// Necessary since Compiler is null
public override string ModuleSeparator => ".";
protected override SinglePassCompiler CreateCompiler() {
return null;
}
public override void OnPostCompile() {
// Not calling base.OnPostCompile() since it references `compiler`
}
public override string PublicIdProtect(string name) {
throw new NotSupportedException();
}
public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
if (!Options.UsingNewCli) {
throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.LegacyCLI);
}
var disallowedAssumptions = dafnyProgram.Assumptions(null)
.Where(a => !a.desc.allowedInLibraries);
foreach (var assumption in disallowedAssumptions) {
var message = assumption.desc.issue.Replace("{", "{{").Replace("}", "}}");
Reporter.Error(MessageSource.Compiler, assumption.tok, message, message);
}
var dooFile = new DooFile(dafnyProgram);
dooFile.Write(output);
}
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree callToMainTree) {
// No-op
}
private string DooFilePath(string dafnyProgramName) {
return Path.GetFullPath(Path.ChangeExtension(dafnyProgramName, ".doo"));
}
public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string targetFilename,
ReadOnlyCollection<string> otherFileNames, bool runAfterCompile, TextWriter outputWriter, out object compilationResult) {
var targetDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
var dooPath = DooFilePath(dafnyProgramName);
File.Delete(dooPath);
ZipFile.CreateFromDirectory(targetDirectory, dooPath);
compilationResult = null;
return true;
}
public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string targetFilename,
ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter, TextWriter errorWriter) {
var dooPath = DooFilePath(dafnyProgramName);
return RunTargetDafnyProgram(dooPath, outputWriter, errorWriter, true);
}
}