Skip to content

Commit 0365893

Browse files
coscos
committed
Definition @API
Former-commit-id: 74568277b798eab802d3c979ea62a0b8b4de7ecf [formerly 3662144f31eed1f11f7559457bd9518265b42b42] Former-commit-id: 261c87565dc3d9994cd5fe404df2d851c1768a58
1 parent 9d9ceed commit 0365893

5 files changed

Lines changed: 114 additions & 11 deletions

File tree

‎kernel/src/main/java/org/kframework/Definition.java‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
package org.kframework;
2+
3+
import com.google.common.collect.Lists;
4+
import com.google.common.io.Files;
5+
import com.google.inject.util.Providers;
6+
import org.kframework.attributes.Source;
7+
import org.kframework.kompile.Kompile;
8+
import org.kframework.main.GlobalOptions;
9+
import org.kframework.parser.concrete2kore.ParserUtils;
10+
import org.kframework.utils.errorsystem.KExceptionManager;
11+
import org.kframework.utils.file.FileUtil;
12+
13+
import java.io.File;
14+
import java.util.regex.Matcher;
15+
import java.util.regex.Pattern;
16+
17+
@API
18+
public class Definition {
19+
20+
/**
21+
* Parses the text to create a {@link Definition} object.
22+
* The main module of the definition will be last module defined in the text file.
23+
*/
24+
public static org.kframework.definition.Definition from(String definitionText) {
25+
Pattern pattern = Pattern.compile("module ([A-Z_]*)");
26+
Matcher m = pattern.matcher(definitionText);
27+
if(!m.find()) {
28+
throw new RuntimeException("Could not find any module in the definition");
29+
}
30+
String nameOfLastModule = m.group(m.groupCount());
31+
return from(definitionText, nameOfLastModule, Source.apply("generated"));
32+
}
33+
34+
/**
35+
* Parses the text to create a {@link Definition} object.
36+
*/
37+
public static org.kframework.definition.Definition from(String definitionText, String mainModuleName) {
38+
return from(definitionText, mainModuleName, Source.apply("generated"));
39+
}
40+
41+
/**
42+
* Parses the text to create a {@link Definition} object.
43+
*/
44+
public static org.kframework.definition.Definition from(String definitionText, String mainModuleName, Source source) {
45+
File tmpDir = Files.createTempDir();
46+
File tempDir = new File(tmpDir.getAbsolutePath() + File.pathSeparator + "tempDir");
47+
File definitionDir = new File(tmpDir.getAbsolutePath() + File.pathSeparator + "definitionDir");
48+
File workingDir = new File(tmpDir.getAbsolutePath() + File.pathSeparator + "workingDir");
49+
File kompiledDir = new File(tmpDir.getAbsolutePath() + File.pathSeparator + "kompiledDir");
50+
if(!tempDir.mkdir() || !definitionDir.mkdir() || !workingDir.mkdir() || !kompiledDir.mkdir()) {
51+
throw new AssertionError("Could not create one of the temporary directories");
52+
}
53+
GlobalOptions globalOptions = new GlobalOptions();
54+
KExceptionManager kem = new KExceptionManager(globalOptions);
55+
56+
FileUtil fileUtil = new FileUtil(tempDir,
57+
Providers.of(definitionDir),
58+
workingDir,
59+
Providers.of(kompiledDir),
60+
globalOptions,
61+
System.getenv());
62+
ParserUtils parserUtils = new ParserUtils(fileUtil, kem, globalOptions);
63+
64+
org.kframework.definition.Definition definition = parserUtils.loadDefinition(
65+
mainModuleName,
66+
mainModuleName,
67+
definitionText,
68+
source,
69+
workingDir,
70+
Lists.newArrayList(Kompile.BUILTIN_DIRECTORY),
71+
true
72+
);
73+
74+
return definition;
75+
}
76+
}

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55
import com.google.inject.Inject;
66
import com.google.inject.Module;
77
import org.apache.commons.collections15.ListUtils;
8+
import org.kframework.attributes.Source;
89
import org.kframework.kompile.Kompile;
910
import org.kframework.main.FrontEnd;
1011
import org.kframework.main.GlobalOptions;
@@ -82,7 +83,7 @@ protected int run() {
8283
}
8384

8485
List<org.kframework.kil.Module> modules = parser.slurp(prelude + FileUtil.load(options.mainDefinitionFile()),
85-
options.mainDefinitionFile(),
86+
Source.apply(options.mainDefinitionFile().getAbsolutePath()),
8687
options.mainDefinitionFile().getParentFile(),
8788
ListUtils.union(options.includes.stream()
8889
.map(files::resolveWorkingDirectory).collect(Collectors.toList()),

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -230,7 +230,7 @@ public Module parseModule(CompiledDefinition definition, File definitionFile, bo
230230
java.util.Set<Module> modules = parser.loadModules(
231231
mutable(definition.getParsedDefinition().modules()),
232232
"require " + StringUtil.enquoteCString(definitionFile.getPath()),
233-
definitionFile,
233+
Source.apply(definitionFile.getAbsolutePath()),
234234
definitionFile.getParentFile(),
235235
Lists.newArrayList(BUILTIN_DIRECTORY),
236236
dropQuote);

‎kernel/src/main/java/org/kframework/parser/concrete2kore/ParserUtils.java‎

Lines changed: 18 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -112,16 +112,12 @@ public static Module parseMainModuleOuterSyntax(String definitionText, Source so
112112

113113
public List<org.kframework.kil.Module> slurp(
114114
String definitionText,
115-
File source,
115+
Source source,
116116
File currentDirectory,
117117
List<File> lookupDirectories) {
118-
List<DefinitionItem> items = Outer.parse(Source.apply(source.getPath()), definitionText, null);
118+
List<DefinitionItem> items = Outer.parse(source, definitionText, null);
119119
if (options.verbose) {
120-
try {
121-
System.out.println("Importing: " + source.getCanonicalPath());
122-
} catch (IOException e) {
123-
System.out.println("Importing: " + source.getAbsolutePath());
124-
}
120+
System.out.println("Importing: " + source);
125121
}
126122
List<org.kframework.kil.Module> results = new ArrayList<>();
127123

@@ -148,7 +144,7 @@ else if (di instanceof Require) {
148144

149145
if (definitionFile.isPresent()) {
150146
results.addAll(slurp(files.loadFromWorkingDirectory(definitionFile.get().getPath()),
151-
definitionFile.get(),
147+
Source.apply(definitionFile.get().getAbsolutePath()),
152148
definitionFile.get().getParentFile(),
153149
lookupDirectories));
154150
}
@@ -163,7 +159,7 @@ else if (di instanceof Require) {
163159
public Set<Module> loadModules(
164160
Set<Module> previousModules,
165161
String definitionText,
166-
File source,
162+
Source source,
167163
File currentDirectory,
168164
List<File> lookupDirectories,
169165
boolean dropQuote) {
@@ -196,6 +192,19 @@ public org.kframework.definition.Definition loadDefinition(
196192
File currentDirectory,
197193
List<File> lookupDirectories,
198194
boolean dropQuote) {
195+
return loadDefinition(mainModuleName, syntaxModuleName, definitionText,
196+
Source.apply(source.getAbsolutePath()),
197+
currentDirectory, lookupDirectories, dropQuote);
198+
}
199+
200+
public org.kframework.definition.Definition loadDefinition(
201+
String mainModuleName,
202+
String syntaxModuleName,
203+
String definitionText,
204+
Source source,
205+
File currentDirectory,
206+
List<File> lookupDirectories,
207+
boolean dropQuote) {
199208
Set<Module> modules = loadModules(new HashSet<>(), definitionText, source, currentDirectory, lookupDirectories, dropQuote);
200209
Optional<Module> opt = modules.stream().filter(m -> m.name().equals(mainModuleName)).findFirst();
201210
if (!opt.isPresent()) {

‎kernel/src/test/java/org/kframework/DefinitionTest.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
package org.kframework;
2+
3+
import org.junit.Test;
4+
import org.kframework.definition.Module;
5+
6+
import static org.junit.Assert.*;
7+
import static org.kframework.Collections.*;
8+
import static org.kframework.kore.KORE.*;
9+
10+
public class DefinitionTest {
11+
@Test
12+
public void testFrom() throws Exception {
13+
org.kframework.definition.Definition actual = Definition.from("module X endmodule");
14+
Module mod = Module.apply("X", Set());
15+
assertEquals(org.kframework.definition.Definition.apply(mod, Set(mod), Att()), actual);
16+
}
17+
}

0 commit comments

Comments
 (0)