Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
a9b4922a
Commit
a9b4922a
authored
Aug 09, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Tried to make interpreter independent from keydata
parent
b193e370
Pipeline
#12697
failed with stage
in 1 minute and 31 seconds
Changes
14
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
14 changed files
with
45 additions
and
77 deletions
+45
-77
src/main/java/edu/kit/formal/interpreter/Execute.java
src/main/java/edu/kit/formal/interpreter/Execute.java
+10
-11
src/main/java/edu/kit/formal/interpreter/Interpreter.java
src/main/java/edu/kit/formal/interpreter/Interpreter.java
+2
-39
src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java
...n/java/edu/kit/formal/interpreter/InterpreterBuilder.java
+1
-1
src/main/java/edu/kit/formal/interpreter/KeYMatcher.java
src/main/java/edu/kit/formal/interpreter/KeYMatcher.java
+2
-1
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
+1
-1
src/main/java/edu/kit/formal/interpreter/data/GoalNode.java
src/main/java/edu/kit/formal/interpreter/data/GoalNode.java
+5
-2
src/main/java/edu/kit/formal/interpreter/data/KeyData.java
src/main/java/edu/kit/formal/interpreter/data/KeyData.java
+5
-1
src/main/java/edu/kit/formal/interpreter/funchdl/BuiltinCommands.java
...a/edu/kit/formal/interpreter/funchdl/BuiltinCommands.java
+1
-1
src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java
...formal/interpreter/funchdl/ProofScriptCommandBuilder.java
+1
-1
src/main/java/edu/kit/formal/interpreter/funchdl/RuleCommandHandler.java
...du/kit/formal/interpreter/funchdl/RuleCommandHandler.java
+1
-1
src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java
src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java
+2
-2
src/test/java/edu/kit/formal/interpreter/InterpreterTest.java
...test/java/edu/kit/formal/interpreter/InterpreterTest.java
+10
-12
src/test/java/edu/kit/formal/interpreter/KeyMatcherDerivableTest.java
...a/edu/kit/formal/interpreter/KeyMatcherDerivableTest.java
+2
-1
src/test/java/edu/kit/formal/interpreter/MatchEvaluatorTest.java
...t/java/edu/kit/formal/interpreter/MatchEvaluatorTest.java
+2
-3
No files found.
src/main/java/edu/kit/formal/interpreter/Execute.java
View file @
a9b4922a
...
...
@@ -33,6 +33,15 @@ public class Execute {
execute
.
run
();
}
public
static
Options
argparse
()
{
Options
options
=
new
Options
();
options
.
addOption
(
"h"
,
"--help"
,
false
,
"print help text"
);
options
.
addOption
(
"p"
,
"--script-path"
,
true
,
"include folder for scripts"
);
options
.
addOption
(
"l"
,
"--linter"
,
false
,
"run linter before execute"
);
options
.
addOption
(
"s"
,
"--script"
,
true
,
"script sourceName"
);
return
options
;
}
public
Interpreter
<
KeyData
>
run
()
{
try
{
ProofManagementApi
pma
=
KeYApi
.
loadFromKeyFile
(
new
File
(
keyFiles
.
get
(
0
)));
...
...
@@ -49,7 +58,7 @@ public class Execute {
Interpreter
<
KeyData
>
inter
=
interpreterBuilder
.
build
();
KeyData
keyData
=
new
KeyData
(
root
.
getProofNode
(),
pa
.
getEnv
(),
pa
.
getProof
());
inter
.
newState
(
new
GoalNode
<>(
null
,
keyData
));
inter
.
newState
(
new
GoalNode
<>(
null
,
keyData
,
keyData
.
isClosedNode
()
));
inter
.
interpret
(
ast
.
get
(
0
));
return
inter
;
}
catch
(
ProblemLoaderException
|
IOException
e
)
{
...
...
@@ -67,14 +76,4 @@ public class Execute {
if
(
cli
.
getOptionValue
(
'p'
)
!=
null
)
interpreterBuilder
.
scriptSearchPath
(
new
File
(
cli
.
getOptionValue
(
'p'
)));
}
public
static
Options
argparse
()
{
Options
options
=
new
Options
();
options
.
addOption
(
"h"
,
"--help"
,
false
,
"print help text"
);
options
.
addOption
(
"p"
,
"--script-path"
,
true
,
"include folder for scripts"
);
options
.
addOption
(
"l"
,
"--linter"
,
false
,
"run linter before execute"
);
options
.
addOption
(
"s"
,
"--script"
,
true
,
"script sourceName"
);
return
options
;
}
}
src/main/java/edu/kit/formal/interpreter/Interpreter.java
View file @
a9b4922a
...
...
@@ -198,30 +198,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
if
(
va
!=
null
)
{
enterScope
(
simpleCaseStatement
);
executeBody
(
simpleCaseStatement
.
getBody
(),
selectedGoal
,
va
);
// executeCase(simpleCaseStatement.getBody(), )
exitScope
(
simpleCaseStatement
);
return
true
;
}
else
{
return
false
;
}
/* Map<GoalNode<T>, VariableAssignment> matchedGoals =
matchGoal(remainingGoalsSet, (SimpleCaseStatement) aCase);
if (matchedGoals != null) {
remainingGoalsSet.removeAll(matchedGoals.keySet());
goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
}
HashMap<GoalNode<T>, VariableAssignment> matchedGoals = new HashMap<>();
Expression matchExpression = aCase.getGuard();
for (GoalNode<T> goal : allGoalsBeforeCases) {
VariableAssignment va = evaluateMatchInGoal(matchExpression, goal);
if (va != null) {
matchedGoals.put(goal, va);
}
}
return matchedGoals;
*/
}
...
...
@@ -265,20 +246,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
}
//===========================================================================================//
/* for (CaseStatement aCase : cases) {
if (aCase.isClosedStmt) {
System.out.println("IsClosableStmt not implemented yet");
} else {
Map<GoalNode<T>, VariableAssignment> matchedGoals =
matchGoal(remainingGoalsSet, (SimpleCaseStatement) aCase);
if (matchedGoals != null) {
remainingGoalsSet.removeAll(matchedGoals.keySet());
goalsAfterCases.addAll(executeCase(aCase.getBody(), matchedGoals));
}
}
}*/
//for all remaining goals execute default
if
(!
remainingGoalsSet
.
isEmpty
())
{
...
...
@@ -297,13 +264,9 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
State
<
T
>
newStateAfterCases
;
if
(!
goalsAfterCases
.
isEmpty
())
{
//goalsAfterCases.forEach(node -> node.exitScope());
Stream
<
GoalNode
<
T
>>
goalNodeStream
=
goalsAfterCases
.
stream
().
filter
(
tGoalNode
->
!(
(
KeyData
)
tGoalNode
.
getData
()).
getNode
()
.
isClosed
());
Stream
<
GoalNode
<
T
>>
goalNodeStream
=
goalsAfterCases
.
stream
().
filter
(
tGoalNode
->
!(
tGoalNode
.
isClosed
())
)
;
List
<
GoalNode
<
T
>>
openGoalListAfterCases
=
goalNodeStream
.
collect
(
Collectors
.
toList
());
/*if (goalsAfterCases.size() == 1) {
newStateAfterCases = new State<T>(goalsAfterCases, 0);
} else {
// newStateAfterCases = new State<T>(goalsAfterCases, null);
}*/
if
(
openGoalListAfterCases
.
size
()
==
1
)
{
newStateAfterCases
=
new
State
<
T
>(
openGoalListAfterCases
,
0
);
}
else
{
...
...
src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java
View file @
a9b4922a
...
...
@@ -191,7 +191,7 @@ public class InterpreterBuilder {
final
ProofApi
pa
=
new
ProofApi
(
proof
,
keyEnvironment
);
final
ProjectedNode
root
=
pa
.
getFirstOpenGoal
();
final
KeyData
keyData
=
new
KeyData
(
root
.
getProofNode
(),
pa
.
getEnv
(),
pa
.
getProof
());
final
GoalNode
<
KeyData
>
startGoal
=
new
GoalNode
<>(
null
,
keyData
);
final
GoalNode
<
KeyData
>
startGoal
=
new
GoalNode
<>(
null
,
keyData
,
keyData
.
isClosedNode
()
);
return
startState
(
startGoal
);
}
...
...
src/main/java/edu/kit/formal/interpreter/KeYMatcher.java
View file @
a9b4922a
...
...
@@ -75,7 +75,8 @@ public class KeYMatcher implements MatcherApi<KeyData> {
boolean
isDerivable
=
proof
.
getSubtreeGoals
(
toShow
.
node
()).
size
()
==
0
;
if
(
isDerivable
)
{
GoalNode
<
KeyData
>
newGoalNode
=
new
GoalNode
<
KeyData
>(
kd
,
new
KeyData
(
kd
.
getData
(),
goalList
.
head
()));
KeyData
kdataNew
=
new
KeyData
(
kd
.
getData
(),
goalList
.
head
());
GoalNode
<
KeyData
>
newGoalNode
=
new
GoalNode
<
KeyData
>(
kd
,
kdataNew
,
kdataNew
.
isClosedNode
());
return
newGoalNode
;
}
else
{
proof
.
pruneProof
(
kd
.
getData
().
getNode
(),
false
);
...
...
src/main/java/edu/kit/formal/interpreter/KeYProofFacade.java
View file @
a9b4922a
...
...
@@ -153,7 +153,7 @@ public class KeYProofFacade {
public
Collection
<
GoalNode
<
KeyData
>>
getPseudoGoals
()
{
KeyData
data
=
new
KeyData
(
proof
.
get
().
root
(),
getEnvironment
(),
getProof
());
return
Collections
.
singleton
(
new
GoalNode
<>(
null
,
data
));
return
Collections
.
singleton
(
new
GoalNode
<>(
null
,
data
,
data
.
getNode
().
isClosed
()
));
}
//endregion
}
...
...
src/main/java/edu/kit/formal/interpreter/data/GoalNode.java
View file @
a9b4922a
...
...
@@ -21,13 +21,16 @@ public class GoalNode<T> {
@Getter
private
T
data
;
@Getter
private
boolean
isClosed
;
/**
* This conctructur will be replaced with concrete one that uses projectedNode
*
* @param parent
* @param data
*/
public
GoalNode
(
GoalNode
<
T
>
parent
,
T
data
)
{
public
GoalNode
(
GoalNode
<
T
>
parent
,
T
data
,
boolean
isClosed
)
{
//BUG: Hier muesste deepcopy der assignments passieren
this
.
assignments
=
new
VariableAssignment
(
parent
==
null
?
null
:
parent
.
deepCopyAssignments
());
this
.
parent
=
parent
;
...
...
@@ -105,7 +108,7 @@ public class GoalNode<T> {
public
GoalNode
<
T
>
deepCopy
()
{
//TODO method does nothing helpful atm
return
new
GoalNode
<
T
>(
parent
,
data
);
return
new
GoalNode
<
T
>(
parent
,
data
,
isClosed
);
}
public
VariableAssignment
enterScope
(
VariableAssignment
va
)
{
...
...
src/main/java/edu/kit/formal/interpreter/data/KeyData.java
View file @
a9b4922a
...
...
@@ -34,6 +34,7 @@ public class KeyData {
programStatementsLabel
,
nameLabel
;
private
Goal
goal
;
private
boolean
closedNode
;
public
KeyData
(
KeyData
data
,
Goal
node
)
{
env
=
data
.
env
;
...
...
@@ -42,6 +43,7 @@ public class KeyData {
this
.
proof
=
data
.
proof
;
this
.
goal
=
node
;
this
.
node
=
goal
.
node
();
closedNode
=
this
.
node
.
isClosed
();
}
...
...
@@ -49,11 +51,13 @@ public class KeyData {
goal
=
g
;
env
=
environment
;
this
.
proof
=
proof
;
closedNode
=
proof
.
closed
();
}
public
KeyData
(
Node
root
,
KeYEnvironment
environment
,
Proof
proof
)
{
this
(
proof
.
getGoal
(
root
),
environment
,
proof
);
node
=
root
;
closedNode
=
root
.
isClosed
();
}
public
KeyData
(
KeyData
kd
,
Node
node
)
{
...
...
@@ -74,7 +78,7 @@ public class KeyData {
/**
* Create Label for goalview according to function that is passed.
* The following fu
c
ntions can be given:
* The following fun
c
tions can be given:
* <ul>
* <li>@see #Method getRuleLabel()</li>
* <li>@see #Method getBranchingLabel()</li>
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/BuiltinCommands.java
View file @
a9b4922a
...
...
@@ -61,7 +61,7 @@ public abstract class BuiltinCommands {
State
<
String
>
state
=
new
State
<>(
s
.
getGoals
(),
null
);
state
.
getGoals
().
remove
(
s
.
getSelectedGoalNode
());
for
(
char
i
=
0
;
i
<
num
;
i
++)
{
state
.
getGoals
().
add
(
new
GoalNode
<>(
g
,
g
.
getData
()
+
"."
+
(
char
)
(
'a'
+
i
)));
state
.
getGoals
().
add
(
new
GoalNode
<>(
g
,
g
.
getData
()
+
"."
+
(
char
)
(
'a'
+
i
)
,
g
.
isClosed
()
));
}
interpreter
.
pushState
(
state
);
}
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @
a9b4922a
...
...
@@ -60,7 +60,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
state
.
getGoals
().
remove
(
expandedNode
);
for
(
Goal
g
:
ngoals
)
{
KeyData
kdn
=
new
KeyData
(
kd
,
g
.
node
());
state
.
getGoals
().
add
(
new
GoalNode
<>(
expandedNode
,
kdn
));
state
.
getGoals
().
add
(
new
GoalNode
<>(
expandedNode
,
kdn
,
kdn
.
isClosedNode
()
));
}
}
catch
(
Exception
e
)
{
throw
new
RuntimeException
(
e
);
...
...
src/main/java/edu/kit/formal/interpreter/funchdl/RuleCommandHandler.java
View file @
a9b4922a
...
...
@@ -66,7 +66,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
state
.
getGoals
().
remove
(
expandedNode
);
for
(
Goal
g
:
ngoals
)
{
KeyData
kdn
=
new
KeyData
(
kd
,
g
.
node
());
state
.
getGoals
().
add
(
new
GoalNode
<>(
expandedNode
,
kdn
));
state
.
getGoals
().
add
(
new
GoalNode
<>(
expandedNode
,
kdn
,
kdn
.
getNode
().
isClosed
()
));
}
}
catch
(
Exception
e
)
{
if
(
e
.
getClass
().
equals
(
ScriptException
.
class
))
{
...
...
src/test/java/edu/kit/formal/interpreter/EvaluatorTest.java
View file @
a9b4922a
...
...
@@ -35,13 +35,13 @@ public class EvaluatorTest {
@Before
public
void
setup
()
{
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
null
,
"pa"
);
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
null
,
"pa"
,
false
);
parent
.
getAssignments
()
.
declare
(
"a"
,
Type
.
INT
)
.
declare
(
"b"
,
Type
.
INT
)
.
assign
(
"a"
,
Value
.
from
(
1
))
.
assign
(
"b"
,
Value
.
from
(
1
));
GoalNode
<
String
>
selected
=
new
GoalNode
<>(
parent
,
"selg"
);
GoalNode
<
String
>
selected
=
new
GoalNode
<>(
parent
,
"selg"
,
false
);
eval
=
new
Evaluator
(
selected
.
getAssignments
(),
selected
);
eval
.
setMatcher
(
new
PseudoMatcher
());
}
...
...
src/test/java/edu/kit/formal/interpreter/InterpreterTest.java
View file @
a9b4922a
...
...
@@ -28,12 +28,21 @@ import java.util.Map;
*/
public
class
InterpreterTest
{
private
static
<
T
>
T
get
(
Map
<
Variable
,
T
>
m
,
String
...
keys
)
{
for
(
String
k
:
keys
)
{
if
(
m
.
containsKey
(
new
Variable
(
k
)))
{
return
m
.
get
(
new
Variable
(
k
));
}
}
return
null
;
}
public
Interpreter
<
String
>
execute
(
InputStream
is
)
throws
IOException
{
List
<
ProofScript
>
scripts
=
Facade
.
getAST
(
CharStreams
.
fromStream
(
is
));
Interpreter
<
String
>
i
=
new
Interpreter
<>(
createTestLookup
(
scripts
));
i
.
setMatcherApi
(
new
PseudoMatcher
());
//i.getEntryListeners().add(new ScopeLogger("scope:"));
i
.
newState
(
new
GoalNode
<>(
null
,
"abc"
));
i
.
newState
(
new
GoalNode
<>(
null
,
"abc"
,
false
));
i
.
interpret
(
scripts
.
get
(
0
));
return
i
;
}
...
...
@@ -50,7 +59,6 @@ public class InterpreterTest {
return
defaultLookup
;
}
@Test
public
void
testSimple
()
throws
IOException
{
Interpreter
<
String
>
i
=
execute
(
getClass
().
getResourceAsStream
(
"simple1.txt"
));
...
...
@@ -87,7 +95,6 @@ public class InterpreterTest {
}
}
private
class
AssertionCommand
extends
BuiltinCommands
.
BuiltinCommand
{
public
AssertionCommand
()
{
...
...
@@ -105,13 +112,4 @@ public class InterpreterTest {
Assert
.
assertTrue
(
msg
.
getData
(),
exp
.
getData
());
}
}
private
static
<
T
>
T
get
(
Map
<
Variable
,
T
>
m
,
String
...
keys
)
{
for
(
String
k
:
keys
)
{
if
(
m
.
containsKey
(
new
Variable
(
k
)))
{
return
m
.
get
(
new
Variable
(
k
));
}
}
return
null
;
}
}
src/test/java/edu/kit/formal/interpreter/KeyMatcherDerivableTest.java
View file @
a9b4922a
...
...
@@ -22,7 +22,8 @@ public class KeyMatcherDerivableTest {
Proof
proof
=
f
.
getProof
();
Goal
g
=
proof
.
getGoal
(
proof
.
root
());
GoalNode
<
KeyData
>
gn
=
new
GoalNode
<>(
null
,
new
KeyData
(
g
,
f
.
getEnvironment
(),
proof
));
KeyData
newKeYData
=
new
KeyData
(
g
,
f
.
getEnvironment
(),
proof
);
GoalNode
<
KeyData
>
gn
=
new
GoalNode
<>(
null
,
newKeYData
,
newKeYData
.
isClosedNode
());
Term
termQ
=
new
TermBuilder
(
f
.
getEnvironment
().
getServices
().
getTermFactory
(),
f
.
getEnvironment
().
getServices
()).
parseTerm
(
"q"
);
System
.
out
.
println
(
termQ
);
...
...
src/test/java/edu/kit/formal/interpreter/MatchEvaluatorTest.java
View file @
a9b4922a
...
...
@@ -3,7 +3,6 @@ package edu.kit.formal.interpreter;
import
edu.kit.formal.interpreter.data.GoalNode
;
import
edu.kit.formal.interpreter.data.Value
;
import
edu.kit.formal.interpreter.data.VariableAssignment
;
import
edu.kit.formal.interpreter.dbg.Debugger
;
import
edu.kit.formal.interpreter.dbg.PseudoMatcher
;
import
edu.kit.formal.proofscriptparser.ast.Type
;
import
edu.kit.formal.proofscriptparser.ast.Variable
;
...
...
@@ -23,13 +22,13 @@ public class MatchEvaluatorTest {
@Before
public
void
setup
()
{
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
null
,
"pa"
);
GoalNode
<
String
>
parent
=
new
GoalNode
<>(
null
,
"pa"
,
false
);
parent
.
declareVariable
(
new
Variable
(
"a"
),
Type
.
INT
);
parent
.
declareVariable
(
new
Variable
(
"b"
),
Type
.
INT
);
VariableAssignment
va
=
parent
.
getAssignments
();
va
.
assign
(
new
Variable
(
"a"
),
Value
.
from
(
1
));
va
.
assign
(
new
Variable
(
"b"
),
Value
.
from
(
1
));
GoalNode
selected
=
new
GoalNode
(
parent
,
"selg"
);
GoalNode
selected
=
new
GoalNode
(
parent
,
"selg"
,
false
);
mEval
=
new
MatchEvaluator
(
va
,
selected
,
new
PseudoMatcher
());
}
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment