add model for storing het file structure

main
josch 13 years ago
parent c778f0c282
commit c321bf2084

@ -0,0 +1,11 @@
package de.unibremen.informatik.hets.model;
public class Actuals extends Spec {
public Actuals(String cont, String anno) {
super(cont, anno);
}
public String toString() {
return content + "\n";
}
}

@ -0,0 +1,7 @@
package de.unibremen.informatik.hets.model;
public class Basicspec extends Spec {
public Basicspec(String cont, String anno) {
super(cont, anno);
}
}

@ -0,0 +1,42 @@
package de.unibremen.informatik.hets.model;
import java.util.ArrayList;
public class HetFile {
private String libname;
private ArrayList<SpecDefn> specdefns;
public HetFile(String name) {
libname = name;
specdefns = new ArrayList<SpecDefn>();
}
public void add(SpecDefn specdefn) {
specdefns.add(specdefn);
}
public String toString() {
StringBuilder builder = new StringBuilder();
builder.append("library ");
builder.append(libname);
builder.append("\n\n");
String logic = "";
for (SpecDefn specdefn : specdefns) {
if (logic != specdefn.getLogic()) {
logic = specdefn.getLogic();
builder.append("logic ");
builder.append(logic);
builder.append("\n\n");
}
builder.append(specdefn.toString());
builder.append("\n");
}
return builder.toString();
}
}

@ -0,0 +1,156 @@
package de.unibremen.informatik.hets.model;
import java.util.ArrayList;
import java.io.InputStream;
import java.io.IOException;
import de.unibremen.informatik.hets.model.HetFile;
import de.unibremen.informatik.hets.model.PPXMLParserException;
import de.unibremen.informatik.hets.common.xml.Dom;
import de.unibremen.informatik.hets.common.lang.StringUtils;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
import org.w3c.dom.Node;
import org.xml.sax.SAXException;
import javax.xml.parsers.DocumentBuilderFactory;
import javax.xml.parsers.ParserConfigurationException;
public class PPXMLParser {
static {
}
public PPXMLParser() {
super();
}
private static String getrange(String hetfile, String range) throws PPXMLParserException {
int minus = range.indexOf('-');
int fromdot, todot;
int fromline, fromcolumn;
int toline, tocolumn;
String from, to;
try {
from = range.substring(0, minus);
to = range.substring(minus+1);
} catch (IndexOutOfBoundsException e) {
throw new PPXMLParserException(e);
}
fromdot = from.indexOf('.');
todot = to.indexOf('.');
if (fromdot == -1 || todot == -1) {
throw new PPXMLParserException();
}
try {
fromline = Integer.parseInt(from.substring(0, fromdot));
fromcolumn = Integer.parseInt(from.substring(fromdot+1));
toline = Integer.parseInt(to.substring(0, todot));
tocolumn = Integer.parseInt(to.substring(todot+1));
} catch (NumberFormatException e) {
throw new PPXMLParserException(e);
} catch (IndexOutOfBoundsException e) {
throw new PPXMLParserException(e);
}
try {
return StringUtils.getSlice(hetfile, fromline, fromcolumn, toline, tocolumn);
} catch (java.io.IOException e) {
throw new PPXMLParserException(e);
}
}
private static Spec parsespec(String hetfile, Element spec) throws PPXMLParserException {
spec = Dom.getFirstChildElement(spec);
if (spec == null) {
throw new PPXMLParserException("<spec> block doesnt have a child");
}
if (spec.getTagName() == "Union") {
Union un = new Union();
ArrayList<Element> speclist = Dom.getChildElements(spec);
for (Element s : speclist) {
un.add(parsespec(hetfile, s));
}
return un;
} else {
return parsespecspec(hetfile, spec);
}
}
private static Spec parsespecspec(String hetfile, Element spec) throws PPXMLParserException {
Element left = Dom.getFirstChildElement(spec);
String annotation = "";
if (left != null && left.getTagName() == "Left") {
annotation = Dom.getTextContent(Dom.getFirstChildElement(left));
}
if (spec.getTagName() == "Basicspec") {
return new Basicspec(getrange(hetfile, spec.getAttribute("range")), annotation);
} else if (spec.getTagName() == "Actuals") {
return new Actuals(spec.getAttribute("name"), annotation);
} else {
throw new PPXMLParserException();
}
}
public static HetFile parse(InputStream ppxml, String hetfile) throws PPXMLParserException {
Document document;
try {
document = DocumentBuilderFactory.newInstance().newDocumentBuilder().parse(ppxml);
} catch (ParserConfigurationException e) {
throw new PPXMLParserException(e);
} catch (org.xml.sax.SAXException e) {
throw new PPXMLParserException(e);
} catch (IOException e) {
throw new PPXMLParserException(e);
}
Node root = document.getDocumentElement();
HetFile het = new HetFile(((Element)root).getAttribute("name"));
ArrayList<Element> list = Dom.getChildElements(root);
String currentlogic = "";
for (Element item : list) {
if (item.getNodeName() == "Logic") {
currentlogic = ((Element)item).getAttribute("name");
} else if (item.getNodeName() == "SpecDefn") {
if (currentlogic == "") {
throw new PPXMLParserException();
}
SpecDefn specdefn = new SpecDefn(((Element)item).getAttribute("name"), currentlogic);
Element child = Dom.getFirstChildElement(item);
if (child.getTagName() == "Basicspec") {
specdefn.add(parsespecspec(hetfile, child));
} else if (child.getTagName() == "Extension") {
ArrayList<Element> speclist = Dom.getChildElements(child);
for (Element spec : speclist) {
specdefn.add(parsespec(hetfile, spec));
}
}
het.add(specdefn);
}
}
return het;
}
}

@ -0,0 +1,15 @@
package de.unibremen.informatik.hets.model;
public class PPXMLParserException extends Exception {
public PPXMLParserException(Throwable cause) {
super(cause);
}
public PPXMLParserException() {
super();
}
public PPXMLParserException(String message) {
super(message);
}
}

@ -0,0 +1,29 @@
package de.unibremen.informatik.hets.model;
public class Spec {
protected String annotation;
protected String content;
public Spec(String cont, String anno) {
content = cont;
annotation = anno;
}
public Spec(String cont) {
content = cont;
annotation = null;
}
public Spec() {
content = null;
annotation = null;
}
public String toString() {
return content;
}
public String getAnnotation() {
return annotation;
}
}

@ -0,0 +1,59 @@
package de.unibremen.informatik.hets.model;
import java.util.ArrayList;
import java.util.Iterator;
public class SpecDefn {
private ArrayList<Spec> specs;
private String name;
private String logic;
public SpecDefn(String n, String l) {
name = n;
logic = l;
specs = new ArrayList<Spec>();
}
public void add(Spec spec) {
specs.add(spec);
}
public String getLogic() {
return logic;
}
public String toString() {
StringBuilder builder = new StringBuilder();
builder.append("spec ");
builder.append(name);
builder.append(" =");
Iterator<Spec> it = specs.iterator();
for (;;) {
Spec spec = it.next();
String annotation = spec.getAnnotation();
if (annotation != null) {
builder.append(" ");
builder.append(spec.getAnnotation());
}
if (!(spec instanceof Union)) {
builder.append("\n");
}
builder.append(spec.toString());
if (it.hasNext()) {
builder.append("then");
} else {
break;
}
}
builder.append("end");
builder.append("\n");
return builder.toString();
}
}

@ -0,0 +1,46 @@
package de.unibremen.informatik.hets.model;
import java.util.ArrayList;
import java.util.Iterator;
public class Union extends Spec {
private ArrayList<Spec> specs;
public Union() {
specs = new ArrayList<Spec>();
}
public void add(Spec spec) {
if (spec instanceof Union) {
return;
} else {
specs.add(spec);
}
}
public String toString() {
StringBuilder builder = new StringBuilder();
Iterator<Spec> it = specs.iterator();
for (;;) {
Spec spec = it.next();
String annotation = spec.getAnnotation();
if (annotation != null) {
builder.append(" ");
builder.append(spec.getAnnotation());
}
builder.append("\n");
builder.append(spec.toString());
if (it.hasNext()) {
builder.append("and");
} else {
break;
}
}
return builder.toString();
}
}
Loading…
Cancel
Save