Skip to content
Snippets Groups Projects
Commit 64544706 authored by Sebastian Krings's avatar Sebastian Krings
Browse files

remove structparser

parent aa1db326
Branches
Tags
No related merge requests found
Showing
with 0 additions and 1949 deletions
<?xml version="1.0" encoding="UTF-8"?>
<classpath>
<classpathentry kind="src" path="src"/>
<classpathentry kind="src" path="src_generated"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/J2SE-1.5"/>
<classpathentry kind="con" path="org.eclipse.jdt.junit.JUNIT_CONTAINER/3"/>
<classpathentry kind="output" path="bin"/>
</classpath>
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>de.be4.eventb.structparser</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.eclipse.jdt.core.javabuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.eclipse.jdt.core.javanature</nature>
</natures>
</projectDescription>
#Fri Jul 11 11:55:00 CEST 2008
eclipse.preferences.version=1
encoding/<project>=UTF-8
#Mon Jun 15 15:00:47 CEST 2009
eclipse.preferences.version=1
org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
org.eclipse.jdt.core.compiler.codegen.targetPlatform=1.5
org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
org.eclipse.jdt.core.compiler.compliance=1.5
org.eclipse.jdt.core.compiler.debug.lineNumber=generate
org.eclipse.jdt.core.compiler.debug.localVariable=generate
org.eclipse.jdt.core.compiler.debug.sourceFile=generate
org.eclipse.jdt.core.compiler.problem.assertIdentifier=error
org.eclipse.jdt.core.compiler.problem.enumIdentifier=error
org.eclipse.jdt.core.compiler.source=1.5
Package de.be4.eventb.core.parser;
/*******************************************************************
* Helpers *
*******************************************************************/
Helpers
underscore = '_';
at = '@';
lf = 10;
cr = 13;
space = ' ';
slash = '/';
comment_start = slash slash;
multi_comment_start = slash '*';
multi_comment_end = '*' slash;
small_letter = ['a'..'z'];
capital_letter = ['A' .. 'Z'];
letter = small_letter | capital_letter;
digit = ['0' .. '9'] ;
line_break = [lf + cr];
layout_char = [[[[0 .. 32] - line_break] + [127..160]] + [[8206 .. 8207] + [8232 .. 8233]]];
all_chars = [0 .. 0xffff];
all_formula_chars = [[[[all_chars - layout_char] - line_break] - at] - slash];
unicode_letter =
[0x0041..0x005a] | [0x0061..0x007a] | [0x00aa..0x00aa] | [0x00b5..0x00b5] |
[0x00ba..0x00ba] | [0x00c0..0x00d6] | [0x00d8..0x00f6] | [0x00f8..0x01f5] |
[0x01fa..0x0217] | [0x0250..0x02a8] | [0x02b0..0x02b8] | [0x02bb..0x02c1] |
[0x02d0..0x02d1] | [0x02e0..0x02e4] | [0x037a..0x037a] | [0x0386..0x0386] |
[0x0388..0x038a] | [0x038c..0x038c] | [0x038e..0x03a1] | [0x03a3..0x03ce] |
[0x03d0..0x03d6] | [0x03da..0x03da] | [0x03dc..0x03dc] | [0x03de..0x03de] |
[0x03e0..0x03e0] | [0x03e2..0x03f3] | [0x0401..0x040c] | [0x040e..0x044f] |
[0x0451..0x045c] | [0x045e..0x0481] | [0x0490..0x04c4] | [0x04c7..0x04c8] |
[0x04cb..0x04cc] | [0x04d0..0x04eb] | [0x04ee..0x04f5] | [0x04f8..0x04f9] |
[0x0531..0x0556] | [0x0559..0x0559] | [0x0561..0x0587] | [0x05d0..0x05ea] |
[0x05f0..0x05f2] | [0x0621..0x063a] | [0x0640..0x064a] | [0x0671..0x06b7] |
[0x06ba..0x06be] | [0x06c0..0x06ce] | [0x06d0..0x06d3] | [0x06d5..0x06d5] |
[0x06e5..0x06e6] | [0x0905..0x0939] | [0x093d..0x093d] | [0x0958..0x0961] |
[0x0985..0x098c] | [0x098f..0x0990] | [0x0993..0x09a8] | [0x09aa..0x09b0] |
[0x09b2..0x09b2] | [0x09b6..0x09b9] | [0x09dc..0x09dd] | [0x09df..0x09e1] |
[0x09f0..0x09f1] | [0x0a05..0x0a0a] | [0x0a0f..0x0a10] | [0x0a13..0x0a28] |
[0x0a2a..0x0a30] | [0x0a32..0x0a33] | [0x0a35..0x0a36] | [0x0a38..0x0a39] |
[0x0a59..0x0a5c] | [0x0a5e..0x0a5e] | [0x0a72..0x0a74] | [0x0a85..0x0a8b] |
[0x0a8d..0x0a8d] | [0x0a8f..0x0a91] | [0x0a93..0x0aa8] | [0x0aaa..0x0ab0] |
[0x0ab2..0x0ab3] | [0x0ab5..0x0ab9] | [0x0abd..0x0abd] | [0x0ae0..0x0ae0] |
[0x0b05..0x0b0c] | [0x0b0f..0x0b10] | [0x0b13..0x0b28] | [0x0b2a..0x0b30] |
[0x0b32..0x0b33] | [0x0b36..0x0b39] | [0x0b3d..0x0b3d] | [0x0b5c..0x0b5d] |
[0x0b5f..0x0b61] | [0x0b85..0x0b8a] | [0x0b8e..0x0b90] | [0x0b92..0x0b95] |
[0x0b99..0x0b9a] | [0x0b9c..0x0b9c] | [0x0b9e..0x0b9f] | [0x0ba3..0x0ba4] |
[0x0ba8..0x0baa] | [0x0bae..0x0bb5] | [0x0bb7..0x0bb9] | [0x0c05..0x0c0c] |
[0x0c0e..0x0c10] | [0x0c12..0x0c28] | [0x0c2a..0x0c33] | [0x0c35..0x0c39] |
[0x0c60..0x0c61] | [0x0c85..0x0c8c] | [0x0c8e..0x0c90] | [0x0c92..0x0ca8] |
[0x0caa..0x0cb3] | [0x0cb5..0x0cb9] | [0x0cde..0x0cde] | [0x0ce0..0x0ce1] |
[0x0d05..0x0d0c] | [0x0d0e..0x0d10] | [0x0d12..0x0d28] | [0x0d2a..0x0d39] |
[0x0d60..0x0d61] | [0x0e01..0x0e2e] | [0x0e30..0x0e30] | [0x0e32..0x0e33] |
[0x0e40..0x0e46] | [0x0e81..0x0e82] | [0x0e84..0x0e84] | [0x0e87..0x0e88] |
[0x0e8a..0x0e8a] | [0x0e8d..0x0e8d] | [0x0e94..0x0e97] | [0x0e99..0x0e9f] |
[0x0ea1..0x0ea3] | [0x0ea5..0x0ea5] | [0x0ea7..0x0ea7] | [0x0eaa..0x0eab] |
[0x0ead..0x0eae] | [0x0eb0..0x0eb0] | [0x0eb2..0x0eb3] | [0x0ebd..0x0ebd] |
[0x0ec0..0x0ec4] | [0x0ec6..0x0ec6] | [0x0edc..0x0edd] | [0x0f40..0x0f47] |
[0x0f49..0x0f69] | [0x10a0..0x10c5] | [0x10d0..0x10f6] | [0x1100..0x1159] |
[0x115f..0x11a2] | [0x11a8..0x11f9] | [0x1e00..0x1e9b] | [0x1ea0..0x1ef9] |
[0x1f00..0x1f15] | [0x1f18..0x1f1d] | [0x1f20..0x1f45] | [0x1f48..0x1f4d] |
[0x1f50..0x1f57] | [0x1f59..0x1f59] | [0x1f5b..0x1f5b] | [0x1f5d..0x1f5d] |
[0x1f5f..0x1f7d] | [0x1f80..0x1fb4] | [0x1fb6..0x1fbc] | [0x1fbe..0x1fbe] |
[0x1fc2..0x1fc4] | [0x1fc6..0x1fcc] | [0x1fd0..0x1fd3] | [0x1fd6..0x1fdb] |
[0x1fe0..0x1fec] | [0x1ff2..0x1ff4] | [0x1ff6..0x1ffc] | [0x207f..0x207f] |
[0x2102..0x2102] | [0x2107..0x2107] | [0x210a..0x2113] | [0x2115..0x2115] |
[0x2118..0x211d] | [0x2124..0x2124] | [0x2126..0x2126] | [0x2128..0x2128] |
[0x212a..0x2131] | [0x2133..0x2138] | [0x3005..0x3005] | [0x3031..0x3035] |
[0x3041..0x3094] | [0x309b..0x309e] | [0x30a1..0x30fa] | [0x30fc..0x30fe] |
[0x3105..0x312c] | [0x3131..0x318e] | [0x4e00..0x9fa5] | [0xac00..0xd7a3] |
[0xf900..0xfa2d] | [0xfb00..0xfb06] | [0xfb13..0xfb17] | [0xfb1f..0xfb28] |
[0xfb2a..0xfb36] | [0xfb38..0xfb3c] | [0xfb3e..0xfb3e] | [0xfb40..0xfb41] |
[0xfb43..0xfb44] | [0xfb46..0xfbb1] | [0xfbd3..0xfd3d] | [0xfd50..0xfd8f] |
[0xfd92..0xfdc7] | [0xfdf0..0xfdfb] | [0xfe70..0xfe72] | [0xfe74..0xfe74] |
[0xfe76..0xfefc] | [0xff21..0xff3a] | [0xff41..0xff5a] | [0xff66..0xffbe] |
[0xffc2..0xffc7] | [0xffca..0xffcf] | [0xffd2..0xffd7] | [0xffda..0xffdc];
unicode_digit =
[0x0030..0x0039] | [0x0660..0x0669] | [0x06f0..0x06f9] | [0x0966..0x096f] |
[0x09e6..0x09ef] | [0x0a66..0x0a6f] | [0x0ae6..0x0aef] | [0x0b66..0x0b6f] |
[0x0be7..0x0bef] | [0x0c66..0x0c6f] | [0x0ce6..0x0cef] | [0x0d66..0x0d6f] |
[0x0e50..0x0e59] | [0x0ed0..0x0ed9] | [0x0f20..0x0f29] | [0xff10..0xff19];
tick = 39;
identifier = unicode_letter (unicode_letter | unicode_digit | underscore)* tick?;
label = [all_chars - layout_char]+ tick?;
/*******************************************************************
* States *
*******************************************************************/
States
normal,
formula,
label,
comment,
multi_comment;
/*******************************************************************
* Tokens *
*******************************************************************/
Tokens
// single line comments
{normal -> comment, formula -> normal} comment_start = comment_start space*;
{comment} comment = [all_chars - line_break]*;
{comment -> normal} comment_end = line_break;
// multiline comments: a lot of it is handle in the lexer
{normal -> multi_comment, formula -> multi_comment} multi_comment_start = multi_comment_start space*;
{multi_comment} multi_comment_body = [all_chars - ['*' + '/']]*;
{multi_comment} star = '*';
{multi_comment, formula} slash = slash;
{multi_comment} multi_comment_end = multi_comment_end; // return to state 'normal' is done in Lexer
{normal -> label, formula -> normal} at = at;
{normal} comma = ',';
{normal -> formula} colon = ':';
{normal} equal = '=';
{normal, formula -> normal} ordinary = 'ordinary';
{normal, formula -> normal} convergent = 'convergent';
{normal, formula -> normal} anticipated = 'anticipated';
// structural keywords
{normal, formula -> normal} machine = 'machine' ;
{normal, formula -> normal} refines = 'refines' ;
{normal, formula -> normal} sees = 'sees' ;
{normal, formula -> normal} variables = 'variables' ;
{normal, formula -> normal} invariants = 'invariants' ;
{normal, formula -> normal} theorem = 'theorem' ;
{normal, formula -> normal} events = 'events' ;
{normal -> formula, formula -> normal} variant = 'variant' ;
{normal, formula -> normal} end = 'end' ;
{normal, formula -> normal} context = 'context' ;
{normal, formula -> normal} extends = 'extends' ;
{normal, formula -> normal} sets = 'sets' ;
{normal, formula -> normal} constants = 'constants' ;
{normal, formula -> normal} axioms = 'axioms' ;
{normal, formula -> normal} event = 'event' ;
{normal, formula -> normal} any = 'any' ;
{normal, formula -> normal} where = 'where' | 'when' ;
{normal, formula -> normal} with = 'with' ;
{normal, formula -> normal} then = 'then' | 'begin';
{normal} identifier_literal = identifier;
{label} label = label;
{normal, label -> formula, formula} white_space = line_break | layout_char+;
{formula} formula = all_formula_chars+ ;
/*******************************************************************
* Ignored Tokens *
*******************************************************************/
Ignored Tokens
white_space,
comment_start,
comment_end,
multi_comment_start,
multi_comment_body, // this is converted to comment by the lexer
multi_comment_end;
/*******************************************************************
* Productions *
*******************************************************************/
Productions
parse_unit {-> parse_unit} =
{machine} [parse_unit]:P.machine {-> parse_unit.parse_unit} |
{context} [parse_unit]:P.context {-> parse_unit.parse_unit} ;
/*
Structure of a machine file
*/
machine {-> parse_unit} =
T.machine [name]:identifier_literal
[comment]:comment*
[refines]:refines_clause?
[sees]:sees_clause?
[variables]:variables_clause?
[invariants]:invariants_clause?
[variant]:variant_clause?
[events]:events_clause?
end {-> New parse_unit.machine([comment], name, [refines.identifier_literal], [sees.identifier_literal], [variables.variable], [invariants.invariant], variant.variant, [events.event])};
refines_clause {-> identifier_literal*} = T.refines [first]:identifier_literal [rest]:refines_clause_tail* {-> [first, rest.identifier_literal]} ;
refines_clause_tail {-> identifier_literal} = [name]:identifier_literal {-> name};
sees_clause {-> identifier_literal*} = T.sees [first]:identifier_literal [rest]:sees_clause_tail* {-> [first, rest.identifier_literal]} ;
sees_clause_tail {-> identifier_literal} = [name]:identifier_literal {-> name};
variables_clause {-> variable*} = [token]:T.variables [variables]:variable_list {-> [variables.variable]} ;
variable_list {-> variable*} =
{single} [identifier]:identifier_literal [comment]:comment* {-> [New variable([comment], identifier)]} |
{multi} [rest]:variable_list [identifier]:identifier_literal [comment]:comment* {-> [rest.variable, New variable([comment], identifier)]} ;
invariants_clause {-> invariant*} = T.invariants [first]:invariant [rest]:invariants_tail* {-> [first.invariant, rest.invariant]} ;
invariants_tail {-> invariant} = [invariant]:invariant {-> invariant.invariant} ;
invariant {-> invariant} =
[label]:P.label [predicate]:formula [comment]:comment* {-> New invariant([comment], label.label, predicate)} |
{derived} theorem [label]:P.label [predicate]:formula [comment]:comment* {-> New invariant.derived([comment], label.label, predicate)} ;
variant_clause {-> P.variant} = T.variant [expression]:formula [comment]:comment* {-> New variant([comment], expression)} ;
events_clause {-> P.event*} = T.events [first]:P.event [rest]:events_tail* {-> [first.event, rest.event]} ;
events_tail {-> P.event} = [event]:P.event {-> event.event} ;
event {-> P.event} =
[convergence]:convergence?
T.event [name]:identifier_literal
[comment]:comment*
[refinement]:event_refinement?
[parameters]:event_any?
[guards]:event_where?
[witnesses]:event_with?
[actions]:event_then?
end {-> New event([comment], name, convergence.convergence, refinement.event_refinement, [parameters.parameter], [guards.guard], [witnesses.witness], [actions.action])} ;
convergence {-> convergence} =
{ordinary} ordinary {-> New convergence.ordinary()} |
{convergent} convergent {-> New convergence.convergent()} |
{anticipated} anticipated {-> New convergence.anticipated()} ;
event_refinement {-> event_refinement} =
{refines} [names]:event_refines {-> New event_refinement.refines([names.identifier_literal])} |
{extended} extends [name]:identifier_literal {-> New event_refinement.extended(name)} ;
event_refines {-> identifier_literal*} = refines [first]:identifier_literal [rest]:event_refines_tail* {-> [first, rest.identifier_literal]} ;
event_refines_tail {-> identifier_literal} = [refines]:identifier_literal {-> refines};
event_any {-> parameter*} = any [first]:parameter [rest]:event_any_tail* {-> [first.parameter, rest.parameter]};
event_any_tail {-> parameter} = [parameter]:parameter {-> parameter.parameter};
parameter {-> parameter} =[name]:identifier_literal [comment]:comment* {-> New parameter([comment], name)};
event_where {-> guard*} = where [first]:guard [rest]:event_where_tail* {-> [first.guard, rest.guard]};
event_where_tail {-> guard} = [guard]:guard {-> guard.guard};
guard {-> guard} =
[label]:P.label [predicate]:formula [comment]:comment* {-> New guard([comment], label.label, predicate)} |
{derived} theorem [label]:P.label [predicate]:formula [comment]:comment* {-> New guard.derived([comment], label.label, predicate)};
event_with {-> witness*} = with [first]:witness [rest]:event_with_tail* {-> [first.witness, rest.witness]};
event_with_tail {-> witness} = [witness]:witness {-> witness.witness};
witness {-> witness} = [label]:P.label [predicate]:formula [comment]:comment* {-> New witness([comment], label.label, predicate)};
event_then {-> action*} = then [first]:action [rest]:event_then_tail* {-> [first.action, rest.action]};
event_then_tail {-> action} = [action]:action {-> action.action};
action {-> action} = [label]:P.label [action]:formula [comment]:comment* {-> New action([comment], label.label, action)} ;
/*
Structure of a context file
*/
context {-> parse_unit} =
T.context [name]:identifier_literal
[comment]:comment*
[extends]:extends_clause?
[sets]:sets_clause?
[constants]:constants_clause?
[axioms]:axioms_clause?
end {-> New parse_unit.context([comment], name, [extends.identifier_literal], [sets.carrier_set], [constants.constant], [axioms.axiom])} ;
extends_clause {-> identifier_literal*} = T.extends [first]:identifier_literal [rest]:extends_clause_tail* {-> [first, rest.identifier_literal]} ;
extends_clause_tail {-> identifier_literal} = [name]:identifier_literal {-> name};
sets_clause {-> carrier_set*} = T.sets [first]:set [rest]:sets_clause_tail* {-> [first.carrier_set, rest.carrier_set]} ;
sets_clause_tail {-> carrier_set} = [set]:set {-> set.carrier_set};
set {-> carrier_set} = [name]:identifier_literal [comment]:comment* {-> New carrier_set([comment], name)};
constants_clause {-> constant*} = constants [first]:constant [rest]:constants_clause_tail* {-> [first.constant, rest.constant]} ;
constants_clause_tail {-> constant} = [constant]:constant {-> constant.constant};
constant {-> constant} = [name]:identifier_literal [comment]:comment* {-> New constant([comment], name)};
axioms_clause {-> axiom*} = T.axioms [first]:axiom [rest]:axioms_clause_tail* {-> [first.axiom, rest.axiom]} ;
axioms_clause_tail {-> axiom} = [axiom]:axiom {-> axiom.axiom} ;
axiom {-> axiom} =
[label]:P.label [predicate]:formula [comment]:comment* {-> New axiom([comment], label.label, predicate)} |
{derived} theorem [label]:P.label [predicate]:formula [comment]:comment* {-> New axiom.derived([comment], label.label, predicate)} ;
label {-> label} = at [identifier]:T.label {-> identifier};
/*******************************************************************
* Abstract Syntax Tree *
*******************************************************************/
Abstract Syntax Tree
parse_unit =
{machine}
[comments]:comment*
[name]:identifier_literal
[refines_names]:identifier_literal*
[seen_names]:identifier_literal*
[variables]:variable*
[invariants]:invariant*
[variant]:P.variant?
[events]:P.event* |
{context}
[comments]:comment*
[name]:identifier_literal
[extends_names]:identifier_literal*
[sets]:carrier_set*
[constants]:constant*
[axioms]:axiom*;
variable = [comments]:comment* [name]:identifier_literal;
variant = [comments]:comment* [expression]:formula ;
invariant =
[comments]:comment* [name]:label [predicate]:formula |
{derived} [comments]:comment* [name]:label [predicate]:formula ;
carrier_set = [comments]:comment* [name]:identifier_literal;
constant = [comments]:comment* [name]:identifier_literal;
axiom =
[comments]:comment* [name]:label [predicate]:formula |
{derived} [comments]:comment* [name]:label [predicate]:formula ;
event =
[comments]:comment*
[name]:identifier_literal
[convergence]:convergence?
[refinement]:event_refinement?
[parameters]:parameter*
[guards]:guard*
[witnesses]:witness*
[actions]:action* ;
convergence = {ordinary} | {convergent} | {anticipated} ;
event_refinement =
{refines} [names]:identifier_literal* |
{extended} [name]:identifier_literal ;
parameter = [comments]:comment* [name]:identifier_literal;
guard =
[comments]:comment* [name]:label [predicate]:formula |
{derived} [comments]:comment* [name]:label [predicate]:formula;
witness = [comments]:comment* [name]:label [predicate]:formula ;
action = [comments]:comment* [name]:label [action]:formula ;
<?xml version="1.0"?>
<project name="EventBParser" default="sablecc-parser" basedir=".">
<property name="enable_debug" value="true"/>
<property name="dir.src" location="src" />
<property name="dir.src_test" location="src_test" />
<property name="dir.src_generated" location="src_generated" />
<property name="dir.temp" location="temp" />
<property name="dir.temp.src" location="${dir.temp}\src" />
<property name="dir.temp.classes" location="${dir.temp}\classes" />
<property name="dir.release" location="release"/>
<property name="file.release.jar" location="${dir.release}\EventBParser.jar" />
<taskdef name="sablecc" classname="org.sablecc.ant.taskdef.Sablecc" classpath="lib/ext/sablecc-anttask.jar" />
<target name="init">
<mkdir dir="${dir.temp.classes}" />
<mkdir dir="${dir.temp.src}" />
<mkdir dir="${dir.release}" />
</target>
<target name="clean">
<delete >
<fileset dir="${dir.src_generated}">
<include name="**/*" />
</fileset>
</delete>
</target>
<target name="sablecc-parser" depends="clean">
<echo message="Regenerating EventBParser sources..." />
<java jar="lib/ext/sablecc.jar" fork="true" failonerror="true">
<arg value="-d"/>
<arg value="src_generated"/>
<arg value="${basedir}/EventBParser.sablecc"/>
</java>
</target>
<target name="compile" depends="init,sablecc-parser" description="">
<copy todir="${dir.temp.src}">
<fileset dir="src"/>
<fileset dir="src_generated"/>
</copy>
<javac srcdir="${dir.temp.src}" destdir="${dir.temp.classes}" includeAntRuntime="false" target="1.5" source="1.5"/>
<copy file="src_generated/de/be4/eventb/core/parser/lexer/lexer.dat" todir="${dir.temp.classes}/de/be4/eventb/core/parser/lexer" />
<copy file="src_generated/de/be4/eventb/core/parser/parser/parser.dat" todir="${dir.temp.classes}/de/be4/eventb/core/parser/parser" />
</target>
<target name="jar" depends="init,compile" description="">
<tstamp>
<format property="TODAY" pattern="yyyy-MM-dd HH:mm:ss" />
</tstamp>
<jar basedir="${dir.temp.classes}" destfile="${file.release.jar}" >
<manifest>
<attribute name="Built-By" value="${user.name}"/>
<attribute name="Built-On" value="${TODAY}"/>
<attribute name="Main-Class" value="de.be4.eventb.core.parser.EventBParser"/>
</manifest>
</jar>
<delete dir="${dir.temp.classes}" />
</target>
<target name="dist" depends="jar" >
<delete dir="${dir.temp}" />
</target>
<target name="release" depends="clean,dist"/>
</project>
package de.be4.eventb.core.parser;
@SuppressWarnings("serial")
public class BException extends Exception {
private final Exception ex;
public BException(final Exception e) {
ex = e;
}
@Override
public Exception getCause() {
return ex;
}
@Override
public String getMessage() {
return ex.getMessage();
}
@Override
public StackTraceElement[] getStackTrace() {
return ex.getStackTrace();
}
}
package de.be4.eventb.core.parser;
import de.be4.eventb.core.parser.node.Node;
@SuppressWarnings("serial")
public class CheckException extends Exception {
private final Entry[] entries;
public CheckException(final Entry[] entries) {
super();
this.entries = entries;
}
public CheckException(final Entry entry) {
this(new Entry[] { entry });
}
public Entry[] getEntries() {
return entries;
}
@Override
public String getMessage() {
final StringBuilder buffer = new StringBuilder('[');
for (int i = 0; i < entries.length; i++) {
buffer.append(entries[i].message);
if (i < entries.length - 1) {
buffer.append(", ");
}
}
buffer.append(']');
return buffer.toString();
}
public static class Entry {
public final Node node;
public final String message;
public Entry(final Node node, final String message) {
this.node = node;
this.message = message;
}
}
}
package de.be4.eventb.core.parser;
import java.io.IOException;
import java.io.PushbackReader;
import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
import de.be4.eventb.core.parser.lexer.Lexer;
import de.be4.eventb.core.parser.lexer.LexerException;
import de.be4.eventb.core.parser.node.EOF;
import de.be4.eventb.core.parser.node.TColon;
import de.be4.eventb.core.parser.node.TComment;
import de.be4.eventb.core.parser.node.TEnd;
import de.be4.eventb.core.parser.node.TEvent;
import de.be4.eventb.core.parser.node.TFormula;
import de.be4.eventb.core.parser.node.TMultiCommentEnd;
import de.be4.eventb.core.parser.node.TMultiCommentStart;
import de.be4.eventb.core.parser.node.TVariant;
import de.be4.eventb.core.parser.node.TWhiteSpace;
import de.be4.eventb.core.parser.node.Token;
public class EventBLexer extends Lexer {
private boolean debugOutput = false;
private TMultiCommentStart commentStart = null;
private StringBuilder commentBuffer = null;
private TFormula string = null;
private List<Token> stringBuffer;
private static String[] clauseErrorMessages = {
"'machine' is only allowed at the beginning of a file",
"Variable declarations are only allowed before invariant declarations",
"Invariant declarations are only allowed after variables and before the variant",
"The variant is only allowed after invariants and before events",
"The events clause is only allowed at the end",
"'context' is only allowed at the beginning of a file",
"Set declarations are only allowed before the constants declarations",
"Constants declarations are only allowed after sets and before axioms",
"The axioms clause is only allowed at the end" };
private static List<String> clausesOrder = new LinkedList<String>();
private int lastClauseIndex;
private boolean inEvent;
private static String[] eventClauseErrorMessages = {
"Parameter declarations (any) are only allowed at the beginning of an event",
"Guards (where) are only allowed after parameters and before witnesses",
"Witnesses (with) are only allowed after guards and before actions",
"Actions (then) are only allowed at the end of an event" };
private static List<String> eventClausesOrder = new LinkedList<String>();
private int lastEventClauseIndex;
static {
clausesOrder.add("TMachine");
clausesOrder.add("TVariables");
clausesOrder.add("TInvariants");
clausesOrder.add("TVariant");
clausesOrder.add("TEvents");
clausesOrder.add("TContext");
clausesOrder.add("TSets");
clausesOrder.add("TConstants");
clausesOrder.add("TAxioms");
eventClausesOrder.add("TAny");
eventClausesOrder.add("TWhere");
eventClausesOrder.add("TWith");
eventClausesOrder.add("TThen");
}
public EventBLexer(final PushbackReader in) {
super(in);
lastClauseIndex = 0;
lastEventClauseIndex = 0;
inEvent = false;
}
@Override
protected void filter() throws LexerException, IOException {
checkClauseOrders();
collectString();
collectMultiLineComment();
if (token != null) {
if (debugOutput && !(token instanceof TWhiteSpace)
&& !(token instanceof EOF)) {
System.out.print(token.getClass().getSimpleName() + "('"
+ token.getText() + "') ");
}
}
}
private void checkClauseOrders() throws LexerException {
if (token != null) {
// entering event?
if (!inEvent && token instanceof TEvent) {
inEvent = true;
lastEventClauseIndex = 0;
return;
}
// leaving event?
else if (inEvent && token instanceof TEnd) {
inEvent = false;
return;
}
final String className = token.getClass().getSimpleName();
// check machine/context clauses' order
if (!inEvent && clausesOrder.contains(className)) {
final int nextIndex = clausesOrder.indexOf(className);
if (nextIndex < lastClauseIndex) {
throwClausesOrderException(clauseErrorMessages[nextIndex]);
}
lastClauseIndex = nextIndex;
return;
}
// check order within an event
if (inEvent && eventClausesOrder.contains(className)) {
final int nextIndex = eventClausesOrder.indexOf(className);
if (nextIndex < lastEventClauseIndex) {
throwClausesOrderException(eventClauseErrorMessages[nextIndex]);
}
lastEventClauseIndex = nextIndex;
return;
}
}
}
private void throwClausesOrderException(final String message)
throws LexerException {
throw new EventBLexerException(token, message, token.getText()
.toString(), token.getLine(), token.getPos());
}
private void collectMultiLineComment() throws LexerException {
if (state.equals(State.MULTI_COMMENT)) {
if (token instanceof EOF) {
// make sure we don't loose this token, needed for error message
// tokenList.add(token);
throw new LexerException("Comment not closed");
}
/*
* Starting a new multiline comment, so first token is
* TMultiCommentStart
*/
if (commentStart == null) {
commentStart = (TMultiCommentStart) token;
commentBuffer = new StringBuilder();
token = null;
} else {
// end of comment reached?
if (token instanceof TMultiCommentEnd) {
token = new TComment(commentBuffer.toString(), commentStart
.getLine(), commentStart.getPos());
commentStart = null;
commentBuffer = null;
state = State.NORMAL;
} else {
commentBuffer.append(token.getText());
token = null;
}
}
}
}
private void collectString() throws LexerException {
if (state.equals(State.FORMULA)) {
// we are entering state STRING
if (string == null) {
beginStringToken();
}
// we have already been in state STRING
else {
stringBuffer.add(token);
token = null;
}
}
// we just left state STRING
else if (string != null) {
endStringToken();
}
}
private void endStringToken() throws LexerException {
try {
/*
* Push back current token. We are going to insert our own string
* token into the token stream just before the current token. Reset
* state so that unread token can be recognized again in next lexer
* step.
*/
unread(token);
state = State.NORMAL;
// create text for string token
string.setText(createString());
} catch (final IOException e) {
throw new LexerException("IOException occured: "
+ e.getLocalizedMessage());
}
token = string;
string = null;
stringBuffer = null;
}
private void beginStringToken() throws LexerException {
// expected before actual string begins
if (token instanceof TColon || token instanceof TWhiteSpace
|| token instanceof TVariant) {
return;
}
if (!(token instanceof TFormula)) {
// make sure we don't loose this token, needed for error
// message
// tokenList.add(token);
throw new LexerException("Unexpected token '"
+ token.getClass().getSimpleName().substring(1) + "'");
}
string = (TFormula) token;
stringBuffer = new ArrayList<Token>();
stringBuffer.add(token);
token = null;
}
private String createString() throws IOException {
// push back not wanted whitespaces at end
int endPos = stringBuffer.size() - 1;
while (stringBuffer.get(endPos) instanceof TWhiteSpace) {
unread(stringBuffer.get(endPos));
endPos--;
}
// create actual string text
final StringBuilder builder = new StringBuilder();
for (int i = 0; i <= endPos; i++) {
builder.append(stringBuffer.get(i).getText());
}
return builder.toString();
}
public void setDebugOutput(final boolean debugOutput) {
this.debugOutput = debugOutput;
}
}
package de.be4.eventb.core.parser;
import de.be4.eventb.core.parser.lexer.LexerException;
import de.be4.eventb.core.parser.node.Token;
@SuppressWarnings("serial")
public class EventBLexerException extends LexerException {
private final Token lastToken;
private final String lastText;
private final int lastLine;
private final int lastPos;
public EventBLexerException(final Token lastToken, final String message,
final String lastText, final int lastLine, final int lastPos) {
super(message);
this.lastToken = lastToken;
this.lastText = lastText;
this.lastLine = lastLine;
this.lastPos = lastPos;
}
public String getLastText() {
return lastText;
}
public int getLastLine() {
return lastLine;
}
public int getLastPos() {
return lastPos;
}
public Token getLastToken() {
return lastToken;
}
@Override
public String toString() {
final StringBuilder buffer = new StringBuilder(super.toString());
buffer.append(" (");
buffer.append(lastLine);
buffer.append(" / ");
buffer.append(lastPos);
buffer.append(": ");
buffer.append("'");
buffer.append(lastToken != null ? lastToken.getText()
: "[token unknown]");
buffer.append("', '");
buffer.append(lastText);
buffer.append("')");
return buffer.toString();
}
}
package de.be4.eventb.core.parser;
import de.be4.eventb.core.parser.node.Node;
import de.be4.eventb.core.parser.node.Token;
import de.hhu.stups.sablecc.patch.SourcecodeRange;
@SuppressWarnings("serial")
public class EventBParseException extends RuntimeException {
private final Token token;
private final SourcecodeRange range;
public EventBParseException(final Token token, final SourcecodeRange range,
final String message) {
super(message);
this.token = token;
this.range = range;
}
public EventBParseException(final Token token, final String message) {
this(token, null, message);
}
/**
* {@link Token} which caused the parse exception. May be <code>null</code>
* if no special token was affected.
*
* @return
*/
public Token getToken() {
return token;
}
/**
* Returns the {@link SourcecodeRange} which is causing this exception. Will
* be <code>null</code> in case of a real lexing or parsing exception cause
* sourcecode ranges for the {@link Node}s of the AST have not yet been
* evaluated then.
*
* @return
*/
public SourcecodeRange getRange() {
return range;
}
}
package de.be4.eventb.core.parser;
import java.io.File;
import java.io.FileInputStream;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.PushbackReader;
import java.io.Reader;
import java.io.StringReader;
import java.util.List;
import java.util.Map;
import de.be4.eventb.core.parser.analysis.ASTDisplay;
import de.be4.eventb.core.parser.analysis.ASTPrinter;
import de.be4.eventb.core.parser.lexer.LexerException;
import de.be4.eventb.core.parser.node.Start;
import de.be4.eventb.core.parser.node.TComment;
import de.be4.eventb.core.parser.node.Token;
import de.be4.eventb.core.parser.parser.Parser;
import de.be4.eventb.core.parser.parser.ParserException;
import de.hhu.stups.sablecc.patch.IParser;
import de.hhu.stups.sablecc.patch.IToken;
import de.hhu.stups.sablecc.patch.ITokenListContainer;
import de.hhu.stups.sablecc.patch.PositionedNode;
import de.hhu.stups.sablecc.patch.SourcePositions;
import de.hhu.stups.sablecc.patch.SourcecodeRange;
public class EventBParser {
public static final String MSG_COMMENT_PLACEMENT = "Comment can only be place behind the element they belong to. Please move the comment to an appropriate place!";
private static final String CLI_SWITCH_VERBOSE = "-v";
private static final String CLI_SWITCH_TIME = "-time";
private static final String CLI_SWITCH_AST = "-ast";
private static final String CLI_SWITCH_UI = "-ui";
private SourcePositions sourcePositions;
public static void main(final String[] args) {
if (args.length < 1) {
System.err.println("usage: BParser [options] <BMachine file>");
System.err.println();
System.err.println("Available options are:");
System.err.println(CLI_SWITCH_VERBOSE
+ "\t\tVerbose output during lexing and parsing");
System.err.println(CLI_SWITCH_TIME
+ "\t\tOutput time used for complete parsing process.");
System.err.println(CLI_SWITCH_AST
+ "\t\tPrint AST on standard output.");
System.err.println(CLI_SWITCH_UI + "\t\tShow AST as Swing UI.");
System.exit(-1);
}
try {
final long start = System.currentTimeMillis();
final EventBParser parser = new EventBParser();
final Start tree = parser.parseFile(
new File(args[args.length - 1]), isCliSwitchSet(args,
CLI_SWITCH_VERBOSE));
final long end = System.currentTimeMillis();
System.out.println();
if (isCliSwitchSet(args, CLI_SWITCH_TIME)) {
System.out.println("Time for parsing: " + (end - start) + "ms");
}
if (isCliSwitchSet(args, CLI_SWITCH_AST)) {
System.out.println("AST:");
tree.apply(new ASTPrinter());
}
if (isCliSwitchSet(args, CLI_SWITCH_UI)) {
tree.apply(new ASTDisplay());
}
} catch (final IOException e) {
System.err.println();
System.err.println("Error reading input file: "
+ e.getLocalizedMessage());
System.exit(-2);
} catch (final BException e) {
System.err.println();
System.err.println("Error parsing input file: "
+ e.getLocalizedMessage());
System.exit(-3);
}
}
/**
* Parses the input file.
*
* @see #parse(String, boolean)
* @param machine
* @param verbose
* @return
* @throws IOException
* @throws BException
*/
public Start parseFile(final File machine, final boolean verbose)
throws IOException, BException {
final InputStreamReader inputStreamReader = new InputStreamReader(
new FileInputStream(machine));
final StringBuilder builder = new StringBuilder();
final char[] buffer = new char[1024];
int read;
while ((read = inputStreamReader.read(buffer)) >= 0) {
builder.append(String.valueOf(buffer, 0, read));
}
return parse(builder.toString(), verbose);
}
/**
* Parses the input string.
*
* @param input
* the {@link String} to be parsed
* @param debugOutput
* output debug messages on standard out?
* @return the root node of the AST
* @throws BException
* <p>
* The {@link BException} class stores the actual exception as
* delegate and forwards all method calls to it. So it is save
* for tools to just use this exception if they want to extract
* an error message. If the tools needs to extract additional
* information, such as a sourcecode position or involved tokens
* respectively nodes, it needs to retrieve the delegate
* exception. The {@link BException} class offers a
* {@link BException#getCause()} method for this, which returns
* the delegate exception.
* </p>
* <p>
* Internal exceptions:
* <ul>
* <li> {@link PreParseException}: This exception contains errors
* that occur during the preparsing. If possible it supplies a
* token, where the error occured.</li>
* <li> {@link EventBLexerException}: If any error occurs in the
* generated or customized lexer a {@link LexerException} is
* thrown. Usually the lexer classes just throw a
* {@link LexerException}. But this class unfortunately does not
* contain any explicit information about the sourcecode
* position where the error occured. Using aspect-oriented
* programming we intercept the throwing of these exceptions to
* replace them by our own exception. In our own exception we
* provide the sourcecode position of the last characters that
* were read from the input.</li>
* <li> {@link EventBParseException}: This exception is thrown in
* two situations. On the one hand if the parser throws a
* {@link ParseException} we convert it into a
* {@link EventBParseException}. On the other hand it can be
* thrown if any error is found during the AST transformations
* after the parser has finished. We try to provide a token if a
* single token is involved in the error. Otherwise a
* {@link SourcecodeRange} is provided, which can be used to
* retrieve detailed position information from the
* {@link SourcePositions} (s. {@link #getSourcePositions()}).</li>
* <li> {@link CheckException}: If any problem occurs while
* performing semantic checks, a {@link CheckException} is
* thrown. We provide one or more nodes that are involved in the
* problem. For example, if we find dublicate machine clauses,
* we will list all occurances in the exception.</li>
* </ul>
* </p>
*/
public Start parse(final String input, final boolean debugOutput)
throws BException {
final Reader reader = new StringReader(input);
try {
/*
* Main parser
*/
final EventBLexer lexer = new EventBLexer(new PushbackReader(
reader, 99));
lexer.setDebugOutput(debugOutput);
Parser parser = new Parser(lexer);
final Start rootNode = parser.parse();
final List<IToken> tokenList = ((ITokenListContainer) lexer)
.getTokenList();
/*
* Retrieving sourcecode positions which were found by ParserAspect
*/
final Map<PositionedNode, SourcecodeRange> positions = ((IParser) parser)
.getMapping();
sourcePositions = new SourcePositions(tokenList, positions);
parser = null;
return rootNode;
} catch (final LexerException e) {
/*
* Actually it's supposed to be a EventBLexerException because the
* aspect 'LexerAspect' replaces any LexerException to provide
* sourcecode position information in the BLexerException.
*/
throw new BException(e);
} catch (final ParserException e) {
throw new BException(createEventBParseException(e));
} catch (final EventBParseException e) {
throw new BException(e);
} catch (final IOException e) {
// shouldn't happen and if, we cannot handle it
throw new BException(e);
}
}
private EventBParseException createEventBParseException(
final ParserException e) {
final Token token = e.getToken();
String message = e.getMessage();
final boolean expectingFound = message.indexOf("expecting") >= 0;
/*
* Special error message for misplaced comments.
*/
if (expectingFound && token instanceof TComment) {
message = MSG_COMMENT_PLACEMENT;
}
/*
* Replace some token names...
*/
message = message.replaceFirst(" at", " @");
return new EventBParseException(token, message);
}
private static boolean isCliSwitchSet(final String[] args,
final String cliSwitch) {
for (int i = 0; i < args.length; i++) {
if (cliSwitch.equals(args[i])) {
return true;
}
}
return false;
}
public SourcePositions getSourcePositions() {
return sourcePositions;
}
}
package de.be4.eventb.core.parser;
import java.util.List;
import de.be4.eventb.core.parser.node.AContextParseUnit;
import de.be4.eventb.core.parser.node.AMachineParseUnit;
import de.be4.eventb.core.parser.node.PParseUnit;
import de.be4.eventb.core.parser.node.Start;
import de.be4.eventb.core.parser.node.TIdentifierLiteral;
public class Utils {
public static String getIdentifierAsString(
final List<TIdentifierLiteral> idElements) {
final StringBuilder idName = new StringBuilder();
for (final TIdentifierLiteral e : idElements) {
idName.append(e.getText());
idName.append('.');
}
if (idElements.size() > 0) {
idName.deleteCharAt(idName.length() - 1);
}
return idName.toString().trim();
}
public static boolean isCompleteMachine(final Start rootNode) {
if (isMachine(rootNode) || isContext(rootNode)) {
return true;
}
return false;
}
public static boolean isMachine(final Start rootNode) {
final PParseUnit parseUnit = rootNode.getPParseUnit();
if (parseUnit instanceof AMachineParseUnit) {
return true;
}
return false;
}
public static boolean isContext(final Start rootNode) {
final PParseUnit parseUnit = rootNode.getPParseUnit();
if (parseUnit instanceof AContextParseUnit) {
return true;
}
return false;
}
}
package de.be4.eventb.core.parser.analysis;
/*
* NOTES
* AST Walker which creates graphical tree
*/
import java.awt.event.WindowAdapter;
import java.awt.event.WindowEvent;
import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Stack;
import javax.swing.JFrame;
import javax.swing.JScrollPane;
import javax.swing.JTree;
import javax.swing.tree.DefaultMutableTreeNode;
import javax.swing.tree.TreeModel;
import javax.swing.tree.TreePath;
import de.be4.eventb.core.parser.node.EOF;
import de.be4.eventb.core.parser.node.Node;
import de.be4.eventb.core.parser.node.Start;
import de.be4.eventb.core.parser.node.Token;
public class ASTDisplay extends DepthFirstAdapter {
private final Stack parents = new Stack();
@Override
public void outStart(final Start node) {
final JFrame frame = new JFrame("AST Displayer");
final JTree tree = new JTree((DefaultMutableTreeNode) parents.pop());
final JScrollPane pane = new JScrollPane(tree);
expandAll(tree);
/* window listener so the program will die */
frame.addWindowListener(new WindowAdapter() {
@Override
public void windowClosing(final WindowEvent e) {
System.exit(0);
}
});
frame.setSize(300, 400);
frame.getContentPane().add(pane);
frame.setVisible(true);
}
/*
* As we come across non terminals, push them onto the stack
*/
@Override
public void defaultIn(final Node node) {
final DefaultMutableTreeNode thisNode = new DefaultMutableTreeNode(node
.getClass().getSimpleName());
parents.push(thisNode);
}
/*
* As we leave a non terminal, it's parent is the node before it on the
* stack, so we pop it off and add it to that node
*/
@Override
public void defaultOut(final Node node) {
final DefaultMutableTreeNode thisNode = (DefaultMutableTreeNode) parents
.pop();
((DefaultMutableTreeNode) parents.peek()).add(thisNode);
}
/*
* Terminals - our parent is always on the top of the stack, so we add
* ourselves to it
*/
@Override
public void defaultCase(final Node node) {
final DefaultMutableTreeNode thisNode = new DefaultMutableTreeNode(
((Token) node).getText());
((DefaultMutableTreeNode) parents.peek()).add(thisNode);
}
@Override
public void caseEOF(final EOF node) {
}
/*
* we want to see the whole tree. These functions expand it for us, they are
* written by Christian Kaufhold and taken from the comp.lang.jave.help
* newsgroup
*/
public static void expandAll(final JTree tree) {
final Object root = tree.getModel().getRoot();
if (root != null) {
expandAll(tree, new TreePath(root));
}
}
public static void expandAll(final JTree tree, final TreePath path) {
for (final Iterator i = extremalPaths(tree.getModel(), path,
new HashSet()).iterator(); i.hasNext();) {
tree.expandPath((TreePath) i.next());
}
}
/**
* The "extremal paths" of the tree model's subtree starting at path. The
* extremal paths are those paths that a) are non-leaves and b) have only
* leaf children, if any. It suffices to know these to know all non-leaf
* paths in the subtree, and those are the ones that matter for expansion
* (since the concept of expan- sion only applies to non-leaves). The
* extremal paths of a leaves is an empty collection. This method uses the
* usual collection filling idiom, i.e. clear and then fill the collection
* that it is given, and for convenience return it. The extremal paths are
* stored in the order in which they appear in pre-order in the tree model.
*/
public static Collection extremalPaths(final TreeModel data,
final TreePath path, final Collection result) {
result.clear();
if (data.isLeaf(path.getLastPathComponent())) {
return result; // should really be forbidden (?)
}
extremalPathsImpl(data, path, result);
return result;
}
private static void extremalPathsImpl(final TreeModel data,
final TreePath path, final Collection result) {
final Object node = path.getLastPathComponent();
boolean hasNonLeafChildren = false;
final int count = data.getChildCount(node);
for (int i = 0; i < count; i++) {
if (!data.isLeaf(data.getChild(node, i))) {
hasNonLeafChildren = true;
}
}
if (!hasNonLeafChildren) {
result.add(path);
} else {
for (int i = 0; i < count; i++) {
final Object child = data.getChild(node, i);
if (!data.isLeaf(child)) {
extremalPathsImpl(data, path.pathByAddingChild(child),
result);
}
}
}
}
}
package de.be4.eventb.core.parser.analysis;
/* -*- jde -*- ASTPrinter.java.in */
import java.util.Stack;
import de.be4.eventb.core.parser.node.EOF;
import de.be4.eventb.core.parser.node.Node;
import de.be4.eventb.core.parser.node.Start;
import de.be4.eventb.core.parser.node.Token;
/**
* Text display of the AST, with (optionally) color output.
*
* To print the AST we do a reverse depth first traversal. We do this because it
* is easier to know which element is the last child in any node. This makes it
* easier to do nice indenting.
*
* @author Roger Keays <rogerk@ieee.org> 7/9/2001
*/
public class ASTPrinter extends ReversedDepthFirstAdapter {
// ---Constants------------------------------------------------
public static char ESC = 27;
// Text attributes
public static final int NORMAL = 0;
public static final int BOLD = 1;
public static final int UNDERSCORE = 4;
public static final int BLINK = 5;
public static final int REVERSE = 7;
public static final int CONCEALED = 8;
// Foreground colors
public static final int FG_BLACK = 30;
public static final int FG_RED = 31;
public static final int FG_GREEN = 32;
public static final int FG_YELLOW = 33;
public static final int FG_BLUE = 34;
public static final int FG_MAGENTA = 35;
public static final int FG_CYAN = 36;
public static final int FG_WHITE = 37;
// Background colors
public static final int BG_BLACK = 40;
public static final int BG_RED = 41;
public static final int BG_GREEN = 42;
public static final int BG_YELLOW = 43;
public static final int BG_BLUE = 44;
public static final int BG_MAGENTA = 45;
public static final int BG_CYAN = 46;
public static final int BG_WHITE = 47;
// variables. We use a stack to push on indent tokens...
private String indent = "", output = "";
private boolean last = false;
private final Stack indentchar = new Stack();
private boolean color = false;
/*
* The last node we visit. It prints out the entire text that we have built.
*/
@Override
public void outStart(final Start node) {
System.out.println(treeColor() + "\n >"
+ output.substring(3, output.length()) + "\n" + resetColor());
}
/*
* As we visit each non-terminal node push on the indent we need for this
* node. The next node we visit will always be the last child of this node.
*/
@Override
public void defaultIn(final Node node) {
if (last) {
indentchar.push("`");
} else {
indentchar.push("|");
}
indent = indent + " ";
last = true;
}
/*
* As we leave a non-terminal node, we pull off the indent character and
* prepend this nodes line to the output text.
*/
@Override
public void defaultOut(final Node node) {
// replace the current indent with the one from the stack
indent = indent.substring(0, indent.length() - 3);
indent = indent.substring(0, indent.length() - 1)
+ (String) indentchar.pop();
// prepend this line to the output.
output = indent
+ "- "
+ setColor(BOLD, FG_CYAN, BG_BLACK)
+ node.getClass().getName().substring(
node.getClass().getName().lastIndexOf('.') + 1)
+ treeColor() + "\n" + output;
// replace any ` with a |
indent = indent.substring(0, indent.length() - 1) + '|';
}
/*
* When we visit a terminals we just print it out. We always set last to
* false after this because the next node we visit will never be the last
* sibling.
*/
@Override
public void defaultCase(final Node node) {
// last sibling has a ` instead of a |
if (last) {
indent = indent.substring(0, indent.length() - 1) + '`';
}
// prepend this line to the output
output = indent + "- " + setColor(BOLD, FG_GREEN, BG_BLACK)
+ ((Token) node).getText() + treeColor() + "\n" + output;
// replace any ` with a |
indent = indent.substring(0, indent.length() - 1) + '|';
last = false;
}
@Override
public void caseEOF(final EOF node) {
last = false;
}
/*
* A method to change the color codes. This only works on color-enabled
* terminals. In Windows/MS-DOS you need to load the ansi.sys driver from
* config.sys or c:\winnt\system32\config.nt (NT/win2k). ANSI.sys only works
* under Win2k in DOS mode. In UNIX, you need an ansi-enabled terminal...
*/
public String setColor(final int style, final int fgColor, final int bgColor) {
if (color) {
return ESC + "[" + style + ";" + fgColor + ";" + bgColor + "m";
} else {
return "";
}
}
public String resetColor() {
return setColor(NORMAL, FG_WHITE, BG_BLACK);
}
public String treeColor() {
return setColor(NORMAL, FG_YELLOW, BG_BLACK);
}
/*
* Not everyone wants color. It is disabled by default
*/
public void setColor(final boolean b) {
color = b;
}
}
package de.be4.eventb.parser;
import junit.framework.TestCase;
import de.be4.eventb.core.parser.BException;
import de.be4.eventb.core.parser.EventBParser;
import de.be4.eventb.core.parser.node.Start;
public class AbstractTest extends TestCase {
protected Start parseInput(final String input, final boolean debugOutput)
throws BException {
if (debugOutput) {
System.out.println();
System.out.println();
}
final EventBParser parser = new EventBParser();
final Start rootNode = parser.parse(input, debugOutput);
return rootNode;
}
public void testNoTest() throws Exception {
}
}
package de.be4.eventb.parser;
import java.util.Enumeration;
import junit.framework.TestSuite;
import junit.runner.ClassPathTestCollector;
import junit.runner.TestCollector;
/**
* All tests on the classpath.
*/
public class AllTestsSuite extends TestSuite {
/**
* Returns a TestSuite containing all tests on the classpath.
*
* @return a TestSuite containing all tests on the classpath.
* @throws ClassNotFoundException
*/
@SuppressWarnings("unchecked")
public static TestSuite suite() throws ClassNotFoundException {
final TestSuite suite = new TestSuite();
final Enumeration enumer = collectTestClasses();
while (enumer.hasMoreElements()) {
final Class klass = Class.forName((String) enumer.nextElement());
if (klass != null) {
suite.addTestSuite(klass);
}
}
return suite;
}
/**
* Returns qualified class names of classes on the classpath, whos name ends
* with "Test".
*
* @return qualified class names of classes on the classpath, whos name ends
* with "Test".
*/
@SuppressWarnings("unchecked")
private static Enumeration collectTestClasses() {
final TestCollector collector = new ClassPathTestCollector() {
@Override
public boolean isTestClass(final String classFileName) {
if (classFileName.endsWith("Test.class")) {
return true;
} else {
return false;
}
}
};
return collector.collectTests();
}
}
package de.be4.eventb.parser;
import java.util.LinkedList;
import java.util.StringTokenizer;
import de.be4.eventb.core.parser.BException;
import de.be4.eventb.core.parser.EventBParseException;
import de.be4.eventb.core.parser.EventBParser;
import de.be4.eventb.core.parser.node.AAction;
import de.be4.eventb.core.parser.node.AEvent;
import de.be4.eventb.core.parser.node.AInvariant;
import de.be4.eventb.core.parser.node.AMachineParseUnit;
import de.be4.eventb.core.parser.node.AVariable;
import de.be4.eventb.core.parser.node.PAction;
import de.be4.eventb.core.parser.node.PInvariant;
import de.be4.eventb.core.parser.node.PVariable;
import de.be4.eventb.core.parser.node.Start;
import de.be4.eventb.core.parser.node.TComment;
public class CommentTest extends AbstractTest {
public void testCommentPredicates1() throws Exception {
final Start rootNode = parseInput(
"machine CommentPredicates1 invariants\n @inv1 asdf //MyComment\nend",
false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<PInvariant> invariants = parseUnit.getInvariants();
final AInvariant invariant = (AInvariant) invariants.get(0);
// correct comment content?
assertEquals("MyComment", invariant.getComments().get(0).getText());
}
public void testCommentPredicates2() throws Exception {
final Start rootNode = parseInput(
"machine CommentPredicates2 invariants\n @inv0 asdf\n @inv1 asdf\n//MyComment\nend",
false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<PInvariant> invariants = parseUnit.getInvariants();
assertEquals(2, invariants.size());
AInvariant invariant = (AInvariant) invariants.get(0);
assertEquals(0, invariant.getComments().size());
assertEquals("inv0", invariant.getName().getText());
assertEquals("asdf", invariant.getPredicate().getText());
// correct comment content, i.e., is whitespace in the beginning
// omitted?
invariant = (AInvariant) invariants.get(1);
final LinkedList<TComment> comments = invariant.getComments();
assertEquals(1, comments.size());
assertEquals("MyComment", comments.get(0).getText());
assertEquals("inv1", invariant.getName().getText());
assertEquals("asdf", invariant.getPredicate().getText());
}
public void testInvariantsAndMultiComments() throws BException {
final String input = "machine InvariantsAndMultiComments invariants\n"
+ "@inv1 1=1\n" + "@inv2 2=2\n" + "/*inv2\ncomment*/\n" + "end";
final Start rootNode = parseInput(input, false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<PInvariant> invariants = parseUnit.getInvariants();
assertEquals(2, invariants.size());
AInvariant invariant = (AInvariant) invariants.get(0);
assertEquals(0, invariant.getComments().size());
assertEquals("inv1", invariant.getName().getText());
assertEquals("1=1", invariant.getPredicate().getText());
invariant = (AInvariant) invariants.get(1);
final LinkedList<TComment> comments = invariant.getComments();
assertEquals(1, comments.size());
assertEquals("inv2\ncomment", comments.get(0).getText());
assertEquals("inv2", invariant.getName().getText());
assertEquals("2=2", invariant.getPredicate().getText());
}
public void testMultiLineComment() throws Exception {
final Start rootNode = parseInput(
"machine MultiLineComment invariants @inv1 asdf\n/* First line\n Second line*/\nend",
false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<PInvariant> invariants = parseUnit.getInvariants();
final AInvariant invariant = (AInvariant) invariants.get(0);
// correct comment content?
final LinkedList<TComment> comments = invariant.getComments();
assertEquals(1, comments.size());
final StringTokenizer tokenizer = new StringTokenizer(comments.get(0)
.getText(), "\n\r");
assertEquals(2, tokenizer.countTokens());
assertEquals("First line", tokenizer.nextToken());
assertEquals(" Second line", tokenizer.nextToken());
// correct invariant label?
assertEquals("inv1", invariant.getName().getText());
// correct string representation for predicate?
assertEquals("asdf", invariant.getPredicate().getText());
}
public void testCommentVariables1() throws Exception {
final Start rootNode = parseInput(
"machine CommentVariables1 variables\n" + "varA"
+ "//varA comment\n" + " varB\n" + "varC\n"
+ "/*varC\ncomment*/" + "end", false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<PVariable> variables = parseUnit.getVariables();
assertEquals(3, variables.size());
AVariable variable = (AVariable) variables.get(0);
assertEquals("varA", variable.getName().getText());
assertEquals("varA comment", variable.getComments().get(0).getText());
variable = (AVariable) variables.get(1);
assertEquals("varB", variable.getName().getText());
assertEquals(0, variable.getComments().size());
variable = (AVariable) variables.get(2);
assertEquals("varC", variable.getName().getText());
final LinkedList<TComment> comments = variable.getComments();
assertNotNull(comments);
assertEquals(1, comments.size());
final StringTokenizer tokenizer = new StringTokenizer(comments.get(0)
.getText(), "\n\r");
assertEquals(2, tokenizer.countTokens());
assertEquals("varC", tokenizer.nextToken());
assertEquals("comment", tokenizer.nextToken());
}
public void testMultiLineMachineComment() throws Exception {
final Start rootNode = parseInput("machine MultiLineMachineComment"
+ "/*\n" + " comment\n" + " in multiple\n" + " lines\n"
+ "*/\n" + " end", false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final String comments = parseUnit.getComments().get(0).getText();
final StringTokenizer tokenizer = new StringTokenizer(comments, "\n\r");
assertEquals(3, tokenizer.countTokens());
assertEquals(" comment", tokenizer.nextToken());
assertEquals(" in multiple", tokenizer.nextToken());
assertEquals(" lines", tokenizer.nextToken());
}
public void testAtSignInComment() throws Exception {
final Start rootNode = parseInput(
"machine AtSignInComment\nevents\nevent testEvent\nthen\n@act1 skip\n@act2 skip\n// MyComment@act2\nend\nend",
false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final AEvent event = (AEvent) parseUnit.getEvents().get(0);
final LinkedList<PAction> actions = event.getActions();
AAction labeledAction = (AAction) actions.get(0);
assertEquals("act1", labeledAction.getName().getText());
assertEquals("skip", labeledAction.getAction().getText());
assertEquals(0, labeledAction.getComments().size());
labeledAction = (AAction) actions.get(1);
assertEquals("act2", labeledAction.getName().getText());
assertEquals("skip", labeledAction.getAction().getText());
assertNotNull(labeledAction.getComments());
assertEquals("MyComment@act2", labeledAction.getComments().get(0)
.getText());
}
public void testMultipleComments1() throws Exception {
final Start rootNode = parseInput("machine MultipleComments1"
+ "// line1\n" + "/* line2\nline3*/" + "// line4\n" + "\nend",
false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<TComment> comments = parseUnit.getComments();
assertEquals(3, comments.size());
assertEquals("line1", comments.get(0).getText());
assertEquals("line2\nline3", comments.get(1).getText());
assertEquals("line4", comments.get(2).getText());
}
public void testMultipleComments2() throws Exception {
final Start rootNode = parseInput(
"machine MultipleComments2" + "/* line1*/\n"
+ "/* line2\nline3*/" + "// line4\n" + "\nend", false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<TComment> comments = parseUnit.getComments();
assertEquals(3, comments.size());
assertEquals("line1", comments.get(0).getText());
assertEquals("line2\nline3", comments.get(1).getText());
assertEquals("line4", comments.get(2).getText());
}
public void testCommentAtBeginErrorMessage() {
try {
parseInput(
"/* Comment before machine header */\nmachine CommentAtBeginErrorMessage end",
false);
fail("Expecting exception here");
} catch (final BException e) {
final Exception cause = e.getCause();
assertTrue(cause instanceof EventBParseException);
assertTrue(((EventBParseException) cause).getToken() instanceof TComment);
assertEquals(EventBParser.MSG_COMMENT_PLACEMENT, cause
.getLocalizedMessage());
}
}
public void testMisplacedCommentMessage() {
try {
parseInput(
"machine MisplacedCommentMessage refines X\n/* Comment before machine header */\n variant 5\nend",
false);
fail("Expecting exception here");
} catch (final BException e) {
final Exception cause = e.getCause();
assertTrue("Unexpected cause: " + e.getCause() + " - "
+ e.getLocalizedMessage(),
cause instanceof EventBParseException);
assertTrue(
"Unexpected token: "
+ ((EventBParseException) cause).getToken()
.getClass().getSimpleName() + " - "
+ e.getLocalizedMessage(),
((EventBParseException) cause).getToken() instanceof TComment);
assertEquals("Unexpected message: " + e.getLocalizedMessage()
+ " - " + e.getLocalizedMessage(),
EventBParser.MSG_COMMENT_PLACEMENT, cause
.getLocalizedMessage());
}
}
}
package de.be4.eventb.parser;
import java.util.LinkedList;
import de.be4.eventb.core.parser.BException;
import de.be4.eventb.core.parser.node.AInvariant;
import de.be4.eventb.core.parser.node.AMachineParseUnit;
import de.be4.eventb.core.parser.node.AVariant;
import de.be4.eventb.core.parser.node.PInvariant;
import de.be4.eventb.core.parser.node.Start;
public class LexerTest extends AbstractTest {
public void testStringLabeledElements() throws BException {
final Start rootNode = parseInput(
"machine Test invariants \n\t@inv1 asdf \n fdsa \n\t@inv2 qwer: \t rewq \nend",
false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final LinkedList<PInvariant> invariants = parseUnit.getInvariants();
AInvariant invariant = (AInvariant) invariants.get(0);
// correct invariant label?
assertEquals("inv1", invariant.getName().getText());
// correct string representation for predicate?
assertEquals("asdf \n fdsa", invariant.getPredicate().getText());
invariant = (AInvariant) invariants.get(1);
// correct invariant label?
assertEquals("inv2", invariant.getName().getText());
// correct string representation for predicate?
assertEquals("qwer: \t rewq", invariant.getPredicate().getText());
}
public void testStringVariant() throws BException {
final Start rootNode = parseInput("machine Test\nvariant y-x\nend",
false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) rootNode
.getPParseUnit();
final AVariant variantClause = (AVariant) parseUnit.getVariant();
assertEquals("y-x", variantClause.getExpression().getText());
}
}
package de.be4.eventb.parser;
import java.util.LinkedList;
import de.be4.eventb.core.parser.EventBParser;
import de.be4.eventb.core.parser.node.AMachineParseUnit;
import de.be4.eventb.core.parser.node.PVariable;
import de.be4.eventb.core.parser.node.Start;
import de.hhu.stups.sablecc.patch.PositionedNode;
public class SourcePositionsTest extends AbstractTest {
EventBParser parser = new EventBParser();
@Override
protected void setUp() throws Exception {
parser = new EventBParser();
}
@Override
protected void tearDown() throws Exception {
parser = null;
}
public void testGetEndLine() throws Exception {
final Start root = parser.parse(
"machine\nTestMachine\n\nvariables\nx\n\nend", false);
final AMachineParseUnit parseUnit = (AMachineParseUnit) root
.getPParseUnit();
assertEquals(7, ((PositionedNode) parseUnit).getEndPos().getLine());
final LinkedList<PVariable> variables = parseUnit.getVariables();
assertEquals(5, ((PositionedNode) variables.get(0)).getEndPos()
.getLine());
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment