Skip to content

Commit bbdac8c

Browse files
bmmooredwightguth
bmmoore
authored and
dwightguth
committed
* Tree Viewer * Fix error catching and parser fallback Now uses a better entry point for the textual kore parser, and correctly catches exceptions to try both formats. * Generate node labels more efficiently. Now it won't call ToKast on higher nodes before checking that all the children's text individually fits within the size limit. This is enough to make the loading time for ~200Kb files pretty quick. * Fix ktree pom/maven setup This changes the pom.xml to depend on the RV versions of K packages, which required a small code change, and moves the source files to src/main/java/
1 parent 097e611 commit bbdac8c

4 files changed

Lines changed: 253 additions & 0 deletions

File tree

‎ktree/pom.xml‎

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
<?xml version="1.0" encoding="UTF-8" standalone="yes"?>
2+
<!-- Copyright (c) 2014-2015 K Team. All Rights Reserved. -->
3+
<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
4+
5+
<modelVersion>4.0.0</modelVersion>
6+
<parent>
7+
<groupId>com.runtimeverification.k</groupId>
8+
<artifactId>parent</artifactId>
9+
<version>1.0-SNAPSHOT</version>
10+
</parent>
11+
<artifactId>ktree</artifactId>
12+
<packaging>jar</packaging>
13+
14+
<name>K Framework KTree</name>
15+
16+
<dependencies>
17+
<dependency>
18+
<groupId>com.runtimeverification.k</groupId>
19+
<artifactId>kore</artifactId>
20+
<version>${project.version}</version>
21+
</dependency>
22+
<dependency>
23+
<groupId>com.runtimeverification.k</groupId>
24+
<artifactId>kernel</artifactId>
25+
<version>${project.version}</version>
26+
</dependency>
27+
</dependencies>
28+
</project>

‎ktree/src/main/java/org/kframework/ktree/KTreePanel.java‎

Lines changed: 135 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,135 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework.ktree;
3+
4+
import org.kframework.kore.AbstractKTransformer;
5+
import org.kframework.kore.InjectedKLabel;
6+
import org.kframework.kore.K;
7+
import org.kframework.kore.KApply;
8+
import org.kframework.kore.KAs;
9+
import org.kframework.kore.KRewrite;
10+
import org.kframework.kore.KSequence;
11+
import org.kframework.kore.KToken;
12+
import org.kframework.kore.KVariable;
13+
import org.kframework.unparser.ToKast;
14+
15+
import javax.swing.*;
16+
import javax.swing.tree.DefaultMutableTreeNode;
17+
import javax.swing.tree.DefaultTreeModel;
18+
import javax.swing.tree.TreeSelectionModel;
19+
import java.awt.*;
20+
21+
/**
22+
* Display a K term as a tree
23+
*/
24+
class KTreePanel extends JPanel {
25+
private JTree tree;
26+
27+
KTreePanel() {
28+
super(new GridLayout(1,0));
29+
30+
tree = new JTree(new DefaultMutableTreeNode("No term loaded"));
31+
tree.getSelectionModel().setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION);
32+
33+
add(tree);
34+
JScrollPane treeView = new JScrollPane(tree);
35+
treeView.setMinimumSize(new Dimension(100,100));
36+
treeView.setPreferredSize(new Dimension(500,300));
37+
38+
add(treeView);
39+
}
40+
41+
public void setTerm(K term) {
42+
DefaultMutableTreeNode top = new BuildNodes().apply(term);
43+
tree.setModel(new DefaultTreeModel(top));
44+
}
45+
46+
private class BuildNodes extends AbstractKTransformer<DefaultMutableTreeNode> {
47+
48+
@Override
49+
public DefaultMutableTreeNode apply(KApply k) {
50+
boolean childrenAllSmall = true;
51+
DefaultMutableTreeNode node = new DefaultMutableTreeNode(k.klabel().name());
52+
for (K child : k.asIterable()) {
53+
DefaultMutableTreeNode c = apply(child);
54+
if (childrenAllSmall) {
55+
childrenAllSmall = c.isLeaf();
56+
}
57+
node.add(c);
58+
}
59+
if (childrenAllSmall) {
60+
String text = ToKast.apply(k);
61+
if (text.length() < 80) {
62+
return new DefaultMutableTreeNode(text);
63+
}
64+
}
65+
return node;
66+
}
67+
68+
@Override
69+
public DefaultMutableTreeNode apply(KRewrite k) {
70+
DefaultMutableTreeNode node = new DefaultMutableTreeNode("=>");
71+
DefaultMutableTreeNode l = apply(k.left());
72+
DefaultMutableTreeNode r = apply(k.right());
73+
if (l.isLeaf() && r.isLeaf()) {
74+
String text = ToKast.apply(k);
75+
if (text.length() < 80) {
76+
node.setUserObject(text);
77+
return node;
78+
}
79+
}
80+
node.add(l);
81+
node.add(r);
82+
return node;
83+
}
84+
85+
@Override
86+
public DefaultMutableTreeNode apply(KToken k) {
87+
return new DefaultMutableTreeNode("#token{"+k.s()+"}");
88+
}
89+
90+
@Override
91+
public DefaultMutableTreeNode apply(KVariable k) {
92+
return new DefaultMutableTreeNode(k.name());
93+
}
94+
95+
@Override
96+
public DefaultMutableTreeNode apply(KSequence k) {
97+
boolean childrenAllSmall = true;
98+
DefaultMutableTreeNode node = new DefaultMutableTreeNode("~>");
99+
for (K child: k.asIterable()) {
100+
DefaultMutableTreeNode c = apply(child);
101+
if (childrenAllSmall) {
102+
childrenAllSmall = c.isLeaf();
103+
}
104+
node.add(c);
105+
}
106+
if (childrenAllSmall) {
107+
String text = ToKast.apply(k);
108+
if (text.length() < 80) {
109+
return new DefaultMutableTreeNode(text);
110+
}
111+
}
112+
return node;
113+
}
114+
115+
public DefaultMutableTreeNode apply(KAs k) {
116+
DefaultMutableTreeNode pattern = apply(k.pattern());
117+
DefaultMutableTreeNode alias = apply(k.alias());
118+
if (pattern.isLeaf() && alias.isLeaf()) {
119+
String text = ToKast.apply(k);
120+
if (text.length() < 80) {
121+
return new DefaultMutableTreeNode(text);
122+
}
123+
}
124+
DefaultMutableTreeNode node = new DefaultMutableTreeNode("#as");
125+
node.add(pattern);
126+
node.add(alias);
127+
return node;
128+
}
129+
130+
@Override
131+
public DefaultMutableTreeNode apply(InjectedKLabel k) {
132+
return new DefaultMutableTreeNode(k.klabel().name());
133+
}
134+
}
135+
}

‎ktree/src/main/java/org/kframework/ktree/KTreeViewer.java‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
// Copyright (c) 2015 K Team. All Rights Reserved.
2+
package org.kframework.ktree;
3+
4+
import org.apache.commons.io.FileUtils;
5+
import org.kframework.attributes.Source;
6+
import org.kframework.kore.K;
7+
import org.kframework.parser.binary.BinaryParser;
8+
import org.kframework.parser.kore.KoreParser;
9+
import org.kframework.utils.errorsystem.KEMException;
10+
11+
import javax.swing.*;
12+
import java.io.File;
13+
import java.io.IOException;
14+
import java.nio.channels.FileChannel;
15+
import java.nio.file.StandardOpenOption;
16+
17+
/**
18+
* A simple application for displaying kore files in a Swing TreeView.
19+
* Can load binary or textual kore format.
20+
* The file is parsed on the Swing thread, so the UI hangs while loading.
21+
*/
22+
public class KTreeViewer {
23+
/**
24+
* This needs to be invoked from the event dispatch thread.
25+
*/
26+
private static void createAndShowGUI() {
27+
JFrame frame = new JFrame("KTree");
28+
frame.setDefaultCloseOperation(WindowConstants.EXIT_ON_CLOSE);
29+
30+
final KTreePanel tree = new KTreePanel();
31+
32+
JMenuItem openMenu = new JMenuItem("Open File...");
33+
openMenu.addActionListener(actionEvent -> {
34+
JFileChooser chooser = new JFileChooser();
35+
int returnVal = chooser.showOpenDialog(frame);
36+
if (returnVal == JFileChooser.APPROVE_OPTION) {
37+
try {
38+
K newTerm = loadFile(chooser.getSelectedFile());
39+
assert newTerm != null;
40+
tree.setTerm(newTerm);
41+
} catch (IOException e) {
42+
String message;
43+
if (e.getCause() != null) {
44+
message = "cause:"+e.getCause().getMessage();
45+
} else {
46+
message = e.getMessage();
47+
}
48+
JOptionPane.showMessageDialog(frame,
49+
"Error opening file: "+message,
50+
"Error",
51+
JOptionPane.ERROR_MESSAGE);
52+
}
53+
}
54+
});
55+
56+
JMenuBar menuBar = new JMenuBar();
57+
menuBar.add(openMenu);
58+
frame.setJMenuBar(menuBar);
59+
frame.add(tree);
60+
61+
frame.pack();
62+
frame.setVisible(true);
63+
}
64+
65+
/**
66+
* Tries to parse a term from the given file, as either binary or textual kore.
67+
*
68+
* We don't seem to have good error returns, nor access to the KExceptionGroup
69+
* chosen for a KEMException, so it's hard to give a good message when neither
70+
* parser worked, or figure out which might have been closer to parsing the file.
71+
*/
72+
private static K loadFile(File file) throws IOException {
73+
try {
74+
try {
75+
return KoreParser.parse(FileUtils.readFileToString(file),
76+
new Source(file.getName()));
77+
} catch (KEMException e) {
78+
FileChannel input = FileChannel.open(file.toPath(), StandardOpenOption.READ);
79+
return BinaryParser.parse(input.map(FileChannel.MapMode.READ_ONLY, 0, input.size()));
80+
}
81+
} catch (KEMException e) {
82+
throw new IOException("Parse Error", e);
83+
}
84+
}
85+
86+
public static void main(String[] args) throws IOException {
87+
javax.swing.SwingUtilities.invokeLater(KTreeViewer::createAndShowGUI);
88+
}
89+
}

‎pom.xml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
<modules>
1616
<module>kore</module>
1717
<module>kernel</module>
18+
<module>ktree</module>
1819
<module>k-distribution</module>
1920
<module>coq-backend</module>
2021
<module>API</module>

0 commit comments

Comments
 (0)