Skip to content

Commit fe1eda9

Browse files
author
Dwight Guth
committed
update kdoc skeleton for new pipeline
Former-commit-id: 7282620b7c2ba3d959df855c247273268cba7f66 [formerly bb3db6b5a1bbcff63a402483e384c94d1e7c1dc1] Former-commit-id: 580199880cf35359b449328f7f796778ef751052
1 parent e8faba8 commit fe1eda9

15 files changed

Lines changed: 156 additions & 199 deletions

File tree

‎coq-backend/src/main/java/org/kframework/backend/coq/CoqBackend.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ public CoqBackend(Stopwatch sw, Context context, KompileOptions options, Provide
3232
}
3333

3434
public void run(Definition definition) {
35-
final String labelFile = FilenameUtils.removeExtension(options.mainDefinitionFile().getName()) + ".labeled_rules";
35+
final String labelFile = FilenameUtils.removeExtension(options.outerParsing.mainDefinitionFile(files).getName()) + ".labeled_rules";
3636
final String langName = definition.getMainModule().toLowerCase();
3737
final String domainFile = langName+"_domains.v";
3838
final String ruleFile = langName+"_rules.v";

‎kernel/src/main/java/org/kframework/backend/latex/LatexBackend.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ public void compile(Definition javaDef) {
5050
String preamble = lf.getPreamble().toString();
5151
latexified += preamble + "\\begin{document}" + endl + lf.getResult() + "\\end{document}" + endl;
5252

53-
File canonicalFile = options.mainDefinitionFile();
53+
File canonicalFile = options.outerParsing.mainDefinitionFile(files);
5454
if(makeDocument) latexFilePath = FilenameUtils.removeExtension(canonicalFile.getName()) + "-doc.tex";
5555
else latexFilePath = FilenameUtils.removeExtension(canonicalFile.getName()) + ".tex";
5656
files.saveToTemp(latexFilePath, latexified);

‎kernel/src/main/java/org/kframework/kdep/KDepFrontEnd.java‎

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
import org.kframework.utils.inject.JCommanderModule;
1818
import org.kframework.utils.inject.JCommanderModule.ExperimentalUsage;
1919
import org.kframework.utils.inject.JCommanderModule.Usage;
20+
import org.kframework.utils.options.OuterParsingOptions;
2021

2122
import java.io.File;
2223
import java.util.ArrayList;
@@ -42,15 +43,15 @@
4243
*/
4344
public class KDepFrontEnd extends FrontEnd {
4445

45-
private final KDepOptions options;
46+
private final OuterParsingOptions options;
4647
private final KExceptionManager kem;
4748
private final Stopwatch sw;
4849
private final FileUtil files;
4950
private final ParserUtils parser;
5051

5152
@Inject
5253
public KDepFrontEnd(
53-
KDepOptions options,
54+
OuterParsingOptions options,
5455
KExceptionManager kem,
5556
GlobalOptions globalOptions,
5657
@Usage String usage,
@@ -63,7 +64,7 @@ public KDepFrontEnd(
6364
this.kem = kem;
6465
this.sw = sw;
6566
this.files = files;
66-
this.parser = new ParserUtils(files, kem, options.global);
67+
this.parser = new ParserUtils(files, kem, globalOptions);
6768
}
6869

6970
public static List<Module> getModules() {
@@ -81,9 +82,9 @@ protected int run() {
8182
prelude = "";
8283
}
8384

84-
List<org.kframework.kil.Module> modules = parser.slurp(prelude + FileUtil.load(options.mainDefinitionFile()),
85-
options.mainDefinitionFile(),
86-
options.mainDefinitionFile().getParentFile(),
85+
List<org.kframework.kil.Module> modules = parser.slurp(prelude + FileUtil.load(options.mainDefinitionFile(files)),
86+
options.mainDefinitionFile(files),
87+
options.mainDefinitionFile(files).getParentFile(),
8788
ListUtils.union(options.includes.stream()
8889
.map(files::resolveWorkingDirectory).collect(Collectors.toList()),
8990
Lists.newArrayList(Kompile.BUILTIN_DIRECTORY)));

‎kernel/src/main/java/org/kframework/kdep/KDepModule.java‎

Lines changed: 8 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,13 @@
55
import com.google.inject.Provides;
66
import com.google.inject.TypeLiteral;
77
import com.google.inject.multibindings.Multibinder;
8-
import org.apache.commons.io.FilenameUtils;
8+
import org.kframework.kdoc.KDocOptions;
99
import org.kframework.main.FrontEnd;
1010
import org.kframework.main.GlobalOptions;
1111
import org.kframework.main.Tool;
12-
import org.kframework.utils.file.DefinitionDir;
13-
import org.kframework.utils.file.KompiledDir;
14-
import org.kframework.utils.file.TempDir;
15-
import org.kframework.utils.file.WorkingDir;
1612
import org.kframework.utils.inject.Options;
17-
18-
import java.io.File;
13+
import org.kframework.utils.inject.OuterParsingModule;
14+
import org.kframework.utils.options.OuterParsingOptions;
1915

2016
/**
2117
* Guice module for kdep tool. Binds the information needed to compute the kompiled directory as well as the options
@@ -28,6 +24,8 @@ protected void configure() {
2824
bind(FrontEnd.class).to(KDepFrontEnd.class);
2925
bind(Tool.class).toInstance(Tool.KDEP);
3026

27+
install(new OuterParsingModule());
28+
3129
Multibinder<Object> optionsBinder = Multibinder.newSetBinder(binder(), Object.class, Options.class);
3230
optionsBinder.addBinding().to(KDepOptions.class);
3331
Multibinder<Class<?>> experimentalOptionsBinder = Multibinder.newSetBinder(binder(), new TypeLiteral<Class<?>>() {}, Options.class);
@@ -38,18 +36,8 @@ GlobalOptions globalOptions(KDepOptions options) {
3836
return options.global;
3937
}
4038

41-
@Provides @DefinitionDir
42-
File definitionDir(@WorkingDir File workingDir, KDepOptions options) {
43-
if (options.directory == null) {
44-
return options.mainDefinitionFile().getParentFile();
45-
}
46-
File f = new File(options.directory);
47-
if (f.isAbsolute()) return f;
48-
return new File(workingDir, options.directory);
49-
}
50-
51-
@Provides @KompiledDir
52-
File kompiledDir(@DefinitionDir File defDir, KDepOptions options, @TempDir File tempDir) {
53-
return new File(defDir, FilenameUtils.removeExtension(options.mainDefinitionFile().getName()) + "-kompiled");
39+
@Provides
40+
OuterParsingOptions outerParsingOptions(KDepOptions options) {
41+
return options.outerParsing;
5442
}
5543
}

‎kernel/src/main/java/org/kframework/kdep/KDepOptions.java‎

Lines changed: 3 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,10 @@
11
// Copyright (c) 2015 K Team. All Rights Reserved.
22
package org.kframework.kdep;
33

4-
import com.beust.jcommander.Parameter;
54
import com.beust.jcommander.ParametersDelegate;
6-
import com.google.inject.Inject;
7-
import com.google.inject.Provider;
85
import org.kframework.main.GlobalOptions;
9-
import org.kframework.utils.errorsystem.KEMException;
10-
import org.kframework.utils.file.FileUtil;
116
import org.kframework.utils.inject.RequestScoped;
12-
13-
import java.io.File;
14-
import java.util.ArrayList;
15-
import java.util.List;
7+
import org.kframework.utils.options.OuterParsingOptions;
168

179
/**
1810
* JCommander options for kdep. Essentially, this should contain all the kompile options needed in order to decide what
@@ -22,38 +14,9 @@
2214
@RequestScoped
2315
public class KDepOptions {
2416

25-
@Parameter(description="<file>")
26-
private List<String> parameters;
27-
28-
private File mainDefinitionFile;
29-
30-
public synchronized File mainDefinitionFile() {
31-
if (mainDefinitionFile == null) {
32-
if (parameters == null || parameters.size() == 0) {
33-
throw KEMException.criticalError("You have to provide exactly one main file in order to compute dependencies.");
34-
}
35-
mainDefinitionFile = files.get().resolveWorkingDirectory(parameters.get(0));
36-
}
37-
return mainDefinitionFile;
38-
}
39-
40-
private transient Provider<FileUtil> files;
41-
42-
@Inject
43-
public void setFiles(Provider<FileUtil> files) {
44-
this.files = files;
45-
}
46-
4717
@ParametersDelegate
4818
public transient GlobalOptions global = new GlobalOptions();
4919

50-
@Parameter(names={"--directory", "-d"}, description="Path to the directory in which the output resides. An output can be either a kompiled K definition or a document which depends on the type of backend. The default is the directory containing the main definition file.")
51-
public String directory;
52-
53-
@Parameter(names="-I", description="Add a directory to the search path for requires statements.", variableArity = true)
54-
public List<String> includes = new ArrayList<>();
55-
56-
@Parameter(names="--no-prelude", description="Do not implicitly require prelude.k.")
57-
public boolean noPrelude = false;
58-
20+
@ParametersDelegate
21+
public OuterParsingOptions outerParsing = new OuterParsingOptions();
5922
}

‎kernel/src/main/java/org/kframework/kdoc/KDocFrontEnd.java‎

Lines changed: 10 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,22 @@
11
// Copyright (c) 2014-2015 K Team. All Rights Reserved.
22
package org.kframework.kdoc;
3-
import java.io.File;
4-
import java.util.ArrayList;
5-
import java.util.List;
63

4+
import com.google.inject.Inject;
5+
import com.google.inject.Module;
6+
import com.google.inject.Provider;
77
import org.kframework.backend.PosterBackend;
8-
import org.kframework.kil.Definition;
98
import org.kframework.main.FrontEnd;
109
import org.kframework.main.GlobalOptions;
1110
import org.kframework.utils.errorsystem.KExceptionManager;
1211
import org.kframework.utils.file.FileUtil;
1312
import org.kframework.utils.file.JarInfo;
14-
import org.kframework.utils.file.KompiledDir;
1513
import org.kframework.utils.inject.CommonModule;
16-
import org.kframework.utils.inject.DefinitionScope;
17-
import org.kframework.utils.inject.Concrete;
1814
import org.kframework.utils.inject.JCommanderModule;
1915
import org.kframework.utils.inject.JCommanderModule.ExperimentalUsage;
2016
import org.kframework.utils.inject.JCommanderModule.Usage;
2117

22-
import com.google.inject.Inject;
23-
import com.google.inject.Module;
24-
import com.google.inject.Provider;
18+
import java.util.ArrayList;
19+
import java.util.List;
2520

2621

2722
public class KDocFrontEnd extends FrontEnd {
@@ -34,39 +29,27 @@ public static List<Module> getModules() {
3429
return modules;
3530
}
3631

32+
private final KDocOptions options;
3733
private final Provider<PosterBackend> backend;
38-
private final Provider<Definition> def;
39-
private final DefinitionScope scope;
40-
private final Provider<File> kompiledDir;
4134

4235
@Inject
4336
public KDocFrontEnd(
37+
KDocOptions options,
4438
KExceptionManager kem,
4539
GlobalOptions globalOptions,
4640
@Usage String usage,
4741
@ExperimentalUsage String experimentalUsage,
4842
JarInfo jarInfo,
49-
Provider<PosterBackend> backend,
50-
@Concrete Provider<Definition> def,
5143
FileUtil files,
52-
DefinitionScope scope,
53-
@KompiledDir Provider<File> kompiledDir) {
44+
Provider<PosterBackend> backend) {
5445
super(kem, globalOptions, usage, experimentalUsage, jarInfo, files);
46+
this.options = options;
5547
this.backend = backend;
56-
this.def = def;
57-
this.scope = scope;
58-
this.kompiledDir = kompiledDir;
5948
}
6049

6150
@Override
6251
protected int run() {
63-
scope.enter(kompiledDir.get());
64-
try {
65-
backend.get().run(def.get());
66-
return 0;
67-
} finally {
68-
scope.exit();
69-
}
52+
return 0;
7053
}
7154

7255
}

‎kernel/src/main/java/org/kframework/kdoc/KDocModule.java‎

Lines changed: 5 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -6,22 +6,15 @@
66
import com.google.inject.TypeLiteral;
77
import com.google.inject.multibindings.MapBinder;
88
import com.google.inject.multibindings.Multibinder;
9-
import org.kframework.backend.Backends;
109
import org.kframework.backend.PosterBackend;
11-
import org.kframework.backend.html.HtmlBackend;
12-
import org.kframework.backend.latex.DocumentationBackend;
13-
import org.kframework.backend.latex.LatexBackend;
14-
import org.kframework.backend.latex.PdfBackend;
15-
import org.kframework.kil.loader.Context;
1610
import org.kframework.main.FrontEnd;
1711
import org.kframework.main.GlobalOptions;
1812
import org.kframework.main.Tool;
1913
import org.kframework.utils.errorsystem.KEMException;
2014
import org.kframework.utils.errorsystem.KExceptionManager;
21-
import org.kframework.utils.inject.DefinitionLoadingModule;
22-
import org.kframework.utils.inject.Main;
2315
import org.kframework.utils.inject.Options;
24-
import org.kframework.utils.options.DefinitionLoadingOptions;
16+
import org.kframework.utils.inject.OuterParsingModule;
17+
import org.kframework.utils.options.OuterParsingOptions;
2518

2619
import java.util.Map;
2720

@@ -32,20 +25,14 @@ protected void configure() {
3225
bind(FrontEnd.class).to(KDocFrontEnd.class);
3326
bind(Tool.class).toInstance(Tool.KDOC);
3427

35-
install(new DefinitionLoadingModule());
36-
37-
bind(Context.class).annotatedWith(Main.class).to(Context.class);
28+
install(new OuterParsingModule());
3829

3930
Multibinder<Object> optionsBinder = Multibinder.newSetBinder(binder(), Object.class, Options.class);
4031
optionsBinder.addBinding().to(KDocOptions.class);
4132
Multibinder.newSetBinder(binder(), new TypeLiteral<Class<?>>() {}, Options.class);
4233

4334
MapBinder<String, PosterBackend> posterBinder = MapBinder.newMapBinder(
4435
binder(), String.class, PosterBackend.class);
45-
posterBinder.addBinding(Backends.PDF).to(PdfBackend.class);
46-
posterBinder.addBinding(Backends.LATEX).to(LatexBackend.class);
47-
posterBinder.addBinding(Backends.DOC).to(DocumentationBackend.class);
48-
posterBinder.addBinding(Backends.HTML).to(HtmlBackend.class);
4936
}
5037

5138
@Provides
@@ -54,8 +41,8 @@ GlobalOptions globalOptions(KDocOptions options) {
5441
}
5542

5643
@Provides
57-
DefinitionLoadingOptions defLoadingOptions(KDocOptions options) {
58-
return options.definitionLoading;
44+
OuterParsingOptions outerParsingOptions(KDocOptions options) {
45+
return options.outerParsing;
5946
}
6047

6148
@Provides

‎kernel/src/main/java/org/kframework/kdoc/KDocOptions.java‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
11
// Copyright (c) 2014-2015 K Team. All Rights Reserved.
22
package org.kframework.kdoc;
33

4+
import com.beust.jcommander.Parameter;
5+
import com.beust.jcommander.ParametersDelegate;
46
import org.kframework.backend.Backends;
57
import org.kframework.main.GlobalOptions;
68
import org.kframework.utils.inject.RequestScoped;
7-
import org.kframework.utils.options.DefinitionLoadingOptions;
8-
9-
import com.beust.jcommander.Parameter;
10-
import com.beust.jcommander.ParametersDelegate;
9+
import org.kframework.utils.options.OuterParsingOptions;
1110

1211
@RequestScoped
1312
public class KDocOptions {
1413

1514
@ParametersDelegate
1615
public transient GlobalOptions global = new GlobalOptions();
1716

18-
@ParametersDelegate
19-
public DefinitionLoadingOptions definitionLoading = new DefinitionLoadingOptions();
20-
2117
@Parameter(names="--format", description="Choose a format. <format> is one of [pdf|latex|html|unparse|doc|unflatten]. Each generates a document from the given K definition.")
2218
public String format = Backends.PDF;
19+
20+
@ParametersDelegate
21+
public OuterParsingOptions outerParsing = new OuterParsingOptions();
22+
2323
}

‎kernel/src/main/java/org/kframework/kompile/Kompile.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -271,15 +271,15 @@ public Module parseModule(CompiledDefinition definition, File definitionFile, bo
271271

272272
public Definition parseDefinition(File definitionFile, String mainModuleName, String mainProgramsModule, boolean dropQuote) {
273273
String prelude = REQUIRE_PRELUDE_K;
274-
if (kompileOptions.noPrelude) {
274+
if (kompileOptions.outerParsing.noPrelude) {
275275
prelude = "";
276276
}
277277
Definition definition = parser.loadDefinition(
278278
mainModuleName,
279279
mainProgramsModule, prelude + FileUtil.load(definitionFile),
280280
definitionFile,
281281
definitionFile.getParentFile(),
282-
ListUtils.union(kompileOptions.includes.stream()
282+
ListUtils.union(kompileOptions.outerParsing.includes.stream()
283283
.map(files::resolveWorkingDirectory).collect(Collectors.toList()),
284284
Lists.newArrayList(BUILTIN_DIRECTORY)),
285285
dropQuote);

‎kernel/src/main/java/org/kframework/kompile/KompileFrontEnd.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -60,14 +60,14 @@ public static List<Module> getModules() {
6060

6161
@Override
6262
public int run() {
63-
if (!options.mainDefinitionFile().exists()) {
63+
if (!options.outerParsing.mainDefinitionFile(files).exists()) {
6464
throw KEMException.criticalError("Definition file doesn't exist: " +
65-
options.mainDefinitionFile().getAbsolutePath());
65+
options.outerParsing.mainDefinitionFile(files).getAbsolutePath());
6666
}
6767

6868
Kompile kompile = new Kompile(options, files, kem, sw);
6969
//TODO(dwightguth): handle start symbols
70-
CompiledDefinition def = kompile.run(options.mainDefinitionFile(), options.mainModule(), options.syntaxModule(), Sorts.K(), koreBackend.get().steps(kompile));
70+
CompiledDefinition def = kompile.run(options.outerParsing.mainDefinitionFile(files), options.mainModule(files), options.syntaxModule(files), Sorts.K(), koreBackend.get().steps(kompile));
7171
loader.saveOrDie(files.resolveKompiled("compiled.bin"), def);
7272
koreBackend.get().accept(def);
7373
loader.saveOrDie(files.resolveKompiled("timestamp"), "");

0 commit comments

Comments
 (0)