Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
89dee988
Commit
89dee988
authored
May 01, 2017
by
Alexander Weigl
Browse files
Documentation
parent
679d8b10
Changes
32
Hide whitespace changes
Inline
Side-by-side
src/main/java/edu/kit/formal/proofscriptparser/ASTChanger.java
View file @
89dee988
...
...
@@ -19,8 +19,8 @@ public class ASTChanger extends DefaultASTVisitor<ASTNode> {
}
@Override
public
AssignmentStatement
visit
(
AssignmentStatement
assign
)
{
assign
.
setRhs
((
Variable
)
assign
.
getRhs
().
accept
(
this
));
assign
.
setLhs
((
Expression
)
assign
.
getLhs
().
accept
(
this
));
assign
.
setRhs
((
Expression
)
assign
.
getRhs
().
accept
(
this
));
assign
.
setLhs
((
Variable
)
assign
.
getLhs
().
accept
(
this
));
return
assign
;
}
...
...
src/main/java/edu/kit/formal/proofscriptparser/PrettyPrinter.java
View file @
89dee988
package
edu.kit.formal.proofscriptparser
;
import
edu.kit.formal.proofscriptparser.ast.*
;
import
lombok.Getter
;
import
lombok.Setter
;
import
java.util.Iterator
;
import
java.util.Map
;
/**
* Pretty printer for ASTs.
*
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
public
class
PrettyPrinter
extends
DefaultASTVisitor
<
Void
>
{
private
static
final
int
MAX_WIDTH
=
80
;
@Getter
@Setter
private
int
maxWidth
=
80
;
@Getter
@Setter
private
boolean
unicode
=
true
;
private
final
StringBuilder
s
=
new
StringBuilder
();
private
int
indentation
=
0
;
@Override
public
String
toString
()
{
@Override
public
String
toString
()
{
return
s
.
toString
();
}
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
@Override
public
Void
visit
(
ProofScript
proofScript
)
{
s
.
append
(
"script"
);
s
.
append
(
proofScript
.
getName
());
s
.
append
(
" ("
);
...
...
@@ -31,7 +44,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
null
;
}
@Override
public
Void
visit
(
Signature
sig
)
{
@Override
public
Void
visit
(
Signature
sig
)
{
Iterator
<
Map
.
Entry
<
Variable
,
Type
>>
iter
=
sig
.
entrySet
().
iterator
();
while
(
iter
.
hasNext
())
{
Map
.
Entry
<
Variable
,
Type
>
next
=
iter
.
next
();
...
...
@@ -43,7 +57,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
null
;
}
@Override
public
Void
visit
(
AssignmentStatement
assign
)
{
@Override
public
Void
visit
(
AssignmentStatement
assign
)
{
assign
.
getRhs
().
accept
(
this
);
s
.
append
(
" := "
);
assign
.
getLhs
().
accept
(
this
);
...
...
@@ -51,7 +66,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
null
;
}
@Override
public
Void
visit
(
BinaryExpression
e
)
{
@Override
public
Void
visit
(
BinaryExpression
e
)
{
boolean
left
=
e
.
getPrecedence
()
<
e
.
getLeft
().
getPrecedence
();
boolean
right
=
e
.
getPrecedence
()
<
e
.
getRight
().
getPrecedence
();
...
...
@@ -75,7 +91,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
super
.
visit
(
e
);
}
@Override
public
Void
visit
(
MatchExpression
match
)
{
@Override
public
Void
visit
(
MatchExpression
match
)
{
s
.
append
(
"match "
);
String
prefix
=
getWhitespacePrefix
();
if
(
match
.
getTerm
()
!=
null
)
{
...
...
@@ -84,10 +101,9 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
if
(!
match
.
getSignature
().
isEmpty
())
{
if
(
getCurrentLineLength
()
>
MAX_WIDTH
)
{
if
(
getCurrentLineLength
()
>
maxWidth
)
{
s
.
append
(
"\n"
).
append
(
prefix
);
}
else
{
}
else
{
s
.
append
(
" "
);
}
...
...
@@ -99,7 +115,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
null
;
}
@Override
public
Void
visit
(
CasesStatement
casesStatement
)
{
@Override
public
Void
visit
(
CasesStatement
casesStatement
)
{
s
.
append
(
"cases {"
);
incrementIndent
();
nl
();
...
...
@@ -130,7 +147,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
nl
();
}
@Override
public
Void
visit
(
CaseStatement
caseStatement
)
{
@Override
public
Void
visit
(
CaseStatement
caseStatement
)
{
s
.
append
(
"case "
);
caseStatement
.
getGuard
().
accept
(
this
);
s
.
append
(
" {"
);
...
...
@@ -140,34 +158,40 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
super
.
visit
(
caseStatement
);
}
@Override
public
Void
visit
(
CallStatement
call
)
{
@Override
public
Void
visit
(
CallStatement
call
)
{
s
.
append
(
call
.
getCommand
()).
append
(
' '
);
call
.
getParameters
().
accept
(
this
);
s
.
append
(
";"
);
return
null
;
}
@Override
public
Void
visit
(
TermLiteral
termLiteral
)
{
@Override
public
Void
visit
(
TermLiteral
termLiteral
)
{
s
.
append
(
String
.
format
(
"`%s`"
,
termLiteral
.
getText
()));
return
super
.
visit
(
termLiteral
);
}
@Override
public
Void
visit
(
StringLiteral
stringLiteral
)
{
@Override
public
Void
visit
(
StringLiteral
stringLiteral
)
{
s
.
append
(
String
.
format
(
"\"%s\""
,
stringLiteral
.
getText
()));
return
super
.
visit
(
stringLiteral
);
}
@Override
public
Void
visit
(
Variable
variable
)
{
@Override
public
Void
visit
(
Variable
variable
)
{
s
.
append
(
variable
.
getIdentifier
());
return
super
.
visit
(
variable
);
}
@Override
public
Void
visit
(
BooleanLiteral
bool
)
{
@Override
public
Void
visit
(
BooleanLiteral
bool
)
{
s
.
append
(
bool
.
isValue
());
return
super
.
visit
(
bool
);
}
@Override
public
Void
visit
(
Statements
statements
)
{
@Override
public
Void
visit
(
Statements
statements
)
{
if
(
statements
.
size
()
==
0
)
return
null
;
incrementIndent
();
...
...
@@ -179,12 +203,14 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
super
.
visit
(
statements
);
}
@Override
public
Void
visit
(
IntegerLiteral
integer
)
{
@Override
public
Void
visit
(
IntegerLiteral
integer
)
{
s
.
append
(
integer
.
getValue
().
toString
());
return
null
;
}
@Override
public
Void
visit
(
TheOnlyStatement
theOnly
)
{
@Override
public
Void
visit
(
TheOnlyStatement
theOnly
)
{
s
.
append
(
"theonly {"
);
theOnly
.
getBody
().
accept
(
this
);
cl
();
...
...
@@ -192,7 +218,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
null
;
}
@Override
public
Void
visit
(
ForeachStatement
foreach
)
{
@Override
public
Void
visit
(
ForeachStatement
foreach
)
{
s
.
append
(
"foreach {"
);
foreach
.
getBody
().
accept
(
this
);
cl
();
...
...
@@ -200,7 +227,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
null
;
}
@Override
public
Void
visit
(
RepeatStatement
repeat
)
{
@Override
public
Void
visit
(
RepeatStatement
repeat
)
{
s
.
append
(
"repeat"
);
s
.
append
(
"{"
);
repeat
.
getBody
().
accept
(
this
);
...
...
@@ -210,7 +238,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
}
@Override
public
Void
visit
(
Parameters
parameters
)
{
@Override
public
Void
visit
(
Parameters
parameters
)
{
int
nl
=
getLastNewline
();
String
indention
=
getWhitespacePrefix
();
Iterator
<
Map
.
Entry
<
Variable
,
Expression
>>
iter
=
parameters
.
entrySet
().
iterator
();
...
...
@@ -222,10 +251,9 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
entry
.
getValue
().
accept
(
this
);
if
(
iter
.
hasNext
())
{
int
currentLineLength
=
getCurrentLineLength
();
if
(
currentLineLength
>
MAX_WIDTH
)
{
if
(
currentLineLength
>
maxWidth
)
{
s
.
append
(
"\n"
).
append
(
indention
);
}
else
{
}
else
{
s
.
append
(
" "
);
}
}
...
...
@@ -233,7 +261,8 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
return
null
;
}
@Override
public
Void
visit
(
UnaryExpression
e
)
{
@Override
public
Void
visit
(
UnaryExpression
e
)
{
s
.
append
(
unicode
?
e
.
getOperator
().
unicode
()
:
e
.
getOperator
().
symbol
());
if
(
e
.
getPrecedence
()
<
e
.
getExpression
().
getPrecedence
())
s
.
append
(
"("
);
...
...
@@ -277,22 +306,4 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
//endregion
/**
* Flag for indicating, that the unicode operation symbols should be used.
*
* @return
*/
public
boolean
isUnicode
()
{
return
unicode
;
}
/**
* @param unicode
* @return
* @see #isUnicode()
*/
public
PrettyPrinter
setUnicode
(
boolean
unicode
)
{
this
.
unicode
=
unicode
;
return
this
;
}
}
src/main/java/edu/kit/formal/proofscriptparser/TransformAst.java
View file @
89dee988
...
...
@@ -75,8 +75,8 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
public
Object
visitAssignment
(
ScriptLanguageParser
.
AssignmentContext
ctx
)
{
AssignmentStatement
assign
=
new
AssignmentStatement
();
assign
.
setRuleContext
(
ctx
);
assign
.
set
R
hs
(
new
Variable
(
ctx
.
variable
));
assign
.
set
L
hs
((
Expression
)
ctx
.
expression
().
accept
(
this
));
assign
.
set
L
hs
(
new
Variable
(
ctx
.
variable
));
assign
.
set
R
hs
((
Expression
)
ctx
.
expression
().
accept
(
this
));
return
assign
;
}
...
...
@@ -159,7 +159,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override
public
Object
visitExprLineOperators
(
ScriptLanguageParser
.
ExprLineOperatorsContext
ctx
)
{
return
createBinaryExpression
(
ctx
,
ctx
.
expression
(),
findOperator
(
ctx
.
op
.
getText
()));
return
createBinaryExpression
(
ctx
,
ctx
.
expression
(),
findOperator
(
ctx
.
op
.
getText
()));
}
...
...
src/main/java/edu/kit/formal/proofscriptparser/Visitable.java
View file @
89dee988
package
edu.kit.formal.proofscriptparser
;
/**
* An interface for all classes that can be visited by {@link Visitor}.
*
* @author Alexander Weigl
* @version 1 (27.04.17)
*/
...
...
src/main/java/edu/kit/formal/proofscriptparser/ast/ASTNode.java
View file @
89dee988
package
edu.kit.formal.proofscriptparser.ast
;
import
com.sun.xml.internal.ws.wsdl.writer.document.OpenAtts
;
import
edu.kit.formal.proofscriptparser.Visitable
;
import
edu.kit.formal.proofscriptparser.Visitor
;
import
lombok.Data
;
import
org.antlr.v4.runtime.ParserRuleContext
;
import
java.util.Optional
;
...
...
@@ -10,19 +12,20 @@ import java.util.Optional;
* @author Alexander Weigl
* @version 1 (27.04.17)
*/
public
abstract
class
ASTNode
<
T
extends
ParserRuleContext
>
implements
Visitable
,
Cloneable
{
private
Optional
<
T
>
ruleContext
;
private
Position
startPosition
=
new
Position
();
private
Position
endPosition
=
new
Position
();
public
abstract
class
ASTNode
<
T
extends
ParserRuleContext
>
implements
Visitable
,
Cloneable
{
protected
T
ruleContext
;
protected
Position
startPosition
=
new
Position
();
protected
Position
endPosition
=
new
Position
();
public
void
setRuleContext
(
T
c
)
{
startPosition
=
Position
.
from
(
c
.
getStart
());
endPosition
=
Position
.
from
(
c
.
getStop
());
ruleContext
=
Optional
.
of
(
c
)
;
ruleContext
=
c
;
}
public
Optional
<
T
>
getRuleContext
()
{
return
ruleContext
;
return
Optional
.
of
(
ruleContext
)
;
}
public
Position
getStartPosition
()
{
...
...
@@ -47,6 +50,12 @@ public abstract class ASTNode<T extends ParserRuleContext> implements Visitable,
*/
public
abstract
<
T
>
T
accept
(
Visitor
<
T
>
visitor
);
@Override
public
abstract
ASTNode
<
T
>
clone
();
/**
* Deep copy of the AST hierarchy.
*
* @return a fresh substree of the AST that is equal to this.
*/
@Override
public
abstract
ASTNode
<
T
>
clone
();
}
src/main/java/edu/kit/formal/proofscriptparser/ast/AssignmentStatement.java
View file @
89dee988
...
...
@@ -5,38 +5,41 @@ import edu.kit.formal.proofscriptparser.Visitor;
import
lombok.*
;
/**
* An {@link AssignmentStatement} encapsulate the assigned variable
* {@link AssignmentStatement#getLhs()} and an expression {@link AssignmentStatement#getRhs()}.
*
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
@Data
@ToString
(
includeFieldNames
=
true
)
@NoArgsConstructor
@RequiredArgsConstructor
()
@AllArgsConstructor
@Data
@ToString
(
includeFieldNames
=
true
)
@NoArgsConstructor
@RequiredArgsConstructor
()
@AllArgsConstructor
public
class
AssignmentStatement
extends
Statement
<
ScriptLanguageParser
.
AssignmentContext
>
{
@NonNull
private
Variable
rhs
;
@NonNull
private
Expression
lhs
;
@NonNull
private
Variable
lhs
;
@NonNull
private
Expression
rhs
;
private
Type
type
;
@Override
public
<
T
>
T
accept
(
Visitor
<
T
>
visitor
)
{
@Override
public
<
T
>
T
accept
(
Visitor
<
T
>
visitor
)
{
return
visitor
.
visit
(
this
);
}
@Override
public
AssignmentStatement
clone
()
{
return
new
AssignmentStatement
(
rhs
.
clone
(),
lhs
.
clone
());
}
public
void
setRhs
(
Variable
rhs
)
{
this
.
rhs
=
rhs
;
}
public
Variable
getRhs
()
{
return
rhs
;
}
public
void
setLhs
(
Expression
lhs
)
{
this
.
lhs
=
lhs
;
@Override
public
AssignmentStatement
clone
()
{
return
new
AssignmentStatement
(
lhs
.
clone
(),
rhs
.
clone
(),
type
);
}
public
Expression
getLhs
()
{
return
lhs
;
/**
* Returns true, iff this assignment declares the assigned variable.
*/
public
boolean
isDeclaration
()
{
return
type
!=
null
;
}
}
src/main/java/edu/kit/formal/proofscriptparser/ast/BinaryExpression.java
View file @
89dee988
...
...
@@ -28,13 +28,18 @@ public class BinaryExpression extends Expression<ParserRuleContext> {
return
visitor
.
visit
(
this
);
}
/**
* {@inheritDoc}
*/
@Override
public
BinaryExpression
clone
()
{
BinaryExpression
be
=
new
BinaryExpression
(
left
.
clone
(),
operator
,
right
.
clone
());
return
be
;
}
/**
* {@inheritDoc}
*/
@Override
public
Type
getType
(
Signature
signature
)
throws
NotWelldefinedException
{
if
(
operator
.
arity
()
!=
2
)
...
...
@@ -46,6 +51,9 @@ public class BinaryExpression extends Expression<ParserRuleContext> {
return
operator
.
returnType
();
}
/**
* {@inheritDoc}
*/
@Override
public
int
getPrecedence
()
{
return
operator
.
precedence
();
...
...
src/main/java/edu/kit/formal/proofscriptparser/ast/BooleanLiteral.java
View file @
89dee988
...
...
@@ -8,6 +8,10 @@ import org.antlr.v4.runtime.Token;
import
java.util.Optional
;
/**
* Represents a boolean literal (ie. {@link #FALSE} or {@link #TRUE}).
* <p>
* Instantiating can be useful for setting a custom {@link #setToken(Token)} and position.
*
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
...
...
@@ -22,27 +26,32 @@ public class BooleanLiteral extends Literal {
public
BooleanLiteral
(
boolean
value
,
Token
token
)
{
this
.
value
=
value
;
if
(
token
!=
null
)
this
.
token
=
Optional
.
of
(
token
);
else
this
.
token
=
Optional
.
empty
();
this
.
token
=
token
;
}
BooleanLiteral
(
boolean
b
)
{
this
(
b
,
null
);
}
/**
* {@inheritDoc}
*/
@Override
public
<
T
>
T
accept
(
Visitor
<
T
>
visitor
)
{
return
visitor
.
visit
(
this
);
}
/**
* {@inheritDoc}
*/
@Override
public
BooleanLiteral
clone
()
{
return
new
BooleanLiteral
(
value
,
token
.
orElse
(
null
)
);
return
new
BooleanLiteral
(
value
,
token
);
}
/**
* {@inheritDoc}
*/
@Override
public
Type
getType
(
Signature
signature
)
throws
NotWelldefinedException
{
return
Type
.
BOOL
;
...
...
src/main/java/edu/kit/formal/proofscriptparser/ast/CallStatement.java
View file @
89dee988
...
...
@@ -5,6 +5,8 @@ import edu.kit.formal.proofscriptparser.Visitor;
import
lombok.*
;
/**
* A call to a subroutine or atomic function.
*
* @author Alexander Weigl
* @version 1 (28.04.17)
*/
...
...
@@ -13,14 +15,30 @@ import lombok.*;
@RequiredArgsConstructor
@AllArgsConstructor
public
class
CallStatement
extends
Statement
<
ScriptLanguageParser
.
ScriptCommandContext
>
{
@NonNull
private
String
command
;
/**
* The name of the command.
*/
@NonNull
private
String
command
;
/**
* The list of parameters.
*/
private
Parameters
parameters
=
new
Parameters
();
@Override
public
<
T
>
T
accept
(
Visitor
<
T
>
visitor
)
{
/**
* {@inheritDoc}
*/
@Override
public
<
T
>
T
accept
(
Visitor
<
T
>
visitor
)
{
return
visitor
.
visit
(
this
);
}
@Override
public
CallStatement
clone
()
{
/**
* {@inheritDoc}
*/
@Override
public
CallStatement
clone
()
{
return
new
CallStatement
(
command
,
parameters
.
clone
());
}
}
src/main/java/edu/kit/formal/proofscriptparser/ast/CaseStatement.java
View file @
89dee988
...
...
@@ -2,6 +2,7 @@ package edu.kit.formal.proofscriptparser.ast;
import
edu.kit.formal.proofscriptparser.ScriptLanguageParser
;
import
edu.kit.formal.proofscriptparser.Visitor
;
import
lombok.AllArgsConstructor
;
import
lombok.Data
;
import
lombok.NoArgsConstructor
;
...
...
@@ -11,21 +12,21 @@ import lombok.NoArgsConstructor;
*/
@Data
@NoArgsConstructor
@AllArgsConstructor
public
class
CaseStatement
extends
Statement
<
ScriptLanguageParser
.
CasesListContext
>
{
private
Expression
guard
;
private
Statements
body
;
public
CaseStatement
(
Expression
guard
,
Statements
body
)
{
this
.
guard
=
guard
;
this
.
body
=
body
;
}
/**
* {@inheritDoc}
*/
@Override
public
<
T
>
T
accept
(
Visitor
<
T
>
visitor
)
{
return
visitor
.
visit
(
this
);
}
/**
* {@inheritDoc}
*/
@Override
public
CaseStatement
clone
()
{
return
new
CaseStatement
(
guard
.
clone
(),
body
.
clone
());
}
...
...
src/main/java/edu/kit/formal/proofscriptparser/ast/CasesStatement.java
View file @
89dee988
...
...
@@ -3,6 +3,7 @@ package edu.kit.formal.proofscriptparser.ast;
import
edu.kit.formal.proofscriptparser.ScriptLanguageParser
;
import
edu.kit.formal.proofscriptparser.Visitor
;
import
lombok.Data
;
import
lombok.NonNull
;
import
java.util.ArrayList
;
import
java.util.List
;
...
...
@@ -13,26 +14,19 @@ import java.util.List;
*/
@Data
public
class
CasesStatement
extends
Statement
<
ScriptLanguageParser
.
CasesListContext
>
{
private
List
<
CaseStatement
>
cases
=
new
ArrayList
<>();
private
Statements
defaultCase
=
new
Statements
();
public
List
<
CaseStatement
>
getCases
()
{
return
cases
;
}
public
Statements
getDefaultCase
()
{
return
defaultCase
;
}
public
CasesStatement
setDefaultCase
(
Statements
defaultCase
)
{
this
.
defaultCase
=
defaultCase
;
return
this
;
}
@NonNull
private
final
List
<
CaseStatement
>
cases
=
new
ArrayList
<>();