if (src.contentType() == WyalFile.ContentType) {
Path.Entry<WyalFile> source = (Path.Entry<WyalFile>) src;
Path.Entry<WycsFile> target = (Path.Entry<WycsFile>) dst.create(src.id(),WycsFile.ContentType);
generatedFiles.add(target);
WyalFile wf = source.read();
WycsFile wycs = getModuleStub(wf);
target.write(wycs);
}
}
logger.logTimedMessage("Generated stubs for " + count + " source file(s).",
System.currentTimeMillis() - tmpTime, tmpMem - runtime.freeMemory());
// ========================================================================
// Type source files
// ========================================================================
runtime = Runtime.getRuntime();
tmpTime = System.currentTimeMillis();
tmpMem = runtime.freeMemory();
TypePropagation typer = new TypePropagation(this);
for(Pair<Path.Entry<?>,Path.Root> p : delta) {
Path.Entry<?> f = p.first();
if (f.contentType() == WyalFile.ContentType) {
Path.Entry<WyalFile> sf = (Path.Entry<WyalFile>) f;
WyalFile wf = sf.read();
typer.apply(wf);
}
}
logger.logTimedMessage("Typed " + count + " source file(s).",
System.currentTimeMillis() - tmpTime, tmpMem - runtime.freeMemory());
// ========================================================================
// Code Generation
// ========================================================================
runtime = Runtime.getRuntime();
tmpTime = System.currentTimeMillis();
tmpMem = runtime.freeMemory();
CodeGeneration generator = new CodeGeneration(this);
for (Pair<Path.Entry<?>, Path.Root> p : delta) {
Path.Entry<?> src = p.first();
Path.Root dst = p.second();
if (src.contentType() == WyalFile.ContentType) {
Path.Entry<WyalFile> source = (Path.Entry<WyalFile>) src;
Path.Entry<WycsFile> target = (Path.Entry<WycsFile>) dst
.create(src.id(), WycsFile.ContentType);
WyalFile wf = source.read();
WycsFile wycs = generator.generate(wf);
target.write(wycs);
}
}
logger.logTimedMessage("Generated code for " + count + " source file(s).",
System.currentTimeMillis() - tmpTime, tmpMem - runtime.freeMemory());
// ========================================================================
// Pipeline Stages
// ========================================================================
for (Transform<WycsFile> stage : pipeline) {
for (Pair<Path.Entry<?>, Path.Root> p : delta) {
Path.Root dst = p.second();
Path.Entry<WycsFile> df = dst.get(p.first().id(),WycsFile.ContentType);
WycsFile module = df.read();
try {
process(module, stage);
} catch (VerificationCheck.AssertionFailure ex) {
// FIXME: this feels a bit like a hack.
if(debug && ex.original() != null) {
Rewriter rw = ex.rewriter();
PrettyAutomataWriter writer = new PrettyAutomataWriter(System.out,SCHEMA,"Or","And");
writer.write(ex.original());
writer.flush();
System.err.println("\n\n=> (" + rw.getStats() + ")\n");
writer.write(ex.reduction());
writer.flush();
}
syntaxError(ex.getMessage(), module.filename(),
ex.assertion(), ex);
} catch (SmtVerificationCheck.AssertionFailure e) {
syntaxError(e.getMessage(), module.filename(),
e.getAssertion(), e);
}
}
}