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
e3881ad8
Commit
e3881ad8
authored
Jan 29, 2018
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Now with nested Cases
parent
a7a05d05
Pipeline
#17493
canceled with stages
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
36 additions
and
19 deletions
+36
-19
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
...ormal/psdbg/gui/controller/InteractiveModeController.java
+36
-19
No files found.
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java
View file @
e3881ad8
...
...
@@ -9,6 +9,7 @@ import de.uka.ilkd.key.logic.SequentFormula;
import
de.uka.ilkd.key.macros.scripts.EngineState
;
import
de.uka.ilkd.key.macros.scripts.RuleCommand
;
import
de.uka.ilkd.key.macros.scripts.ScriptException
;
import
de.uka.ilkd.key.pp.LogicPrinter
;
import
de.uka.ilkd.key.proof.Goal
;
import
de.uka.ilkd.key.proof.Node
;
import
de.uka.ilkd.key.proof.Proof
;
...
...
@@ -147,8 +148,11 @@ public class InteractiveModeController {
SequentFormula
seqForm
=
tap
.
getPio
().
sequentFormula
();
//transform term to parsable string representation
Sequent
seq
=
g
.
sequent
();
String
sfTerm
=
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
Utils
.
toPrettyTerm
(
seqForm
.
formula
());
String
onTerm
=
edu
.
kit
.
iti
.
formal
.
psdbg
.
termmatcher
.
Utils
.
toPrettyTerm
(
tap
.
getPio
().
subTerm
());
String
sfTerm
=
LogicPrinter
.
quickPrintTerm
(
seqForm
.
formula
(),
keYServices
,
false
,
false
);
String
onTerm
=
LogicPrinter
.
quickPrintTerm
(
tap
.
getPio
().
subTerm
(),
keYServices
,
false
,
false
);
//String sfTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(seqForm.formula());
// String onTerm = edu.kit.iti.formal.psdbg.termmatcher.Utils.toPrettyTerm(tap.getPio().subTerm());
//check whether more than one possibility for match
//Matchings matches = MatcherFacade.matches(term, seq, true, keYServices);
...
...
@@ -191,8 +195,8 @@ public class InteractiveModeController {
applyRule
(
call
,
g
);
// Insert into the right cases
Node
currentNode
=
g
.
node
();
cases
.
get
(
findRoot
(
currentNode
)).
add
(
call
);
//
Node currentNode = g.node();
//
cases.get(findRoot(currentNode)).add(call);
// How to Play this on the Proof?
// How to Build a new StatePointer? Is it still possible?
...
...
@@ -245,18 +249,6 @@ public class InteractiveModeController {
return
pp
.
toString
();
}
private
String
format
(
String
branchingLabel
)
{
System
.
out
.
println
(
"branchingLabel = "
+
branchingLabel
);
String
newLabel
=
branchingLabel
;
if
(
branchingLabel
.
endsWith
(
"$$"
))
{
newLabel
=
branchingLabel
.
substring
(
0
,
branchingLabel
.
length
()
-
2
);
newLabel
+=
".*"
;
System
.
out
.
println
(
"newLabel = "
+
newLabel
);
}
return
newLabel
;
}
private
void
applyRule
(
CallStatement
call
,
Goal
g
)
throws
ScriptCommandNotApplicableException
{
savepointslist
.
add
(
g
.
node
());
savepointsstatement
.
add
(
call
);
...
...
@@ -297,13 +289,27 @@ public class InteractiveModeController {
AbstractUserInterfaceControl
uiControl
=
new
DefaultUserInterfaceControl
();
c
.
execute
(
uiControl
,
cc
,
estate
);
ImmutableList
<
Goal
>
ngoals
=
g
.
proof
().
getSubtreeGoals
(
g
.
n
ode
());
ImmutableList
<
Goal
>
ngoals
=
g
.
proof
().
getSubtreeGoals
(
expandedNode
.
getData
().
getN
ode
());
goals
.
remove
(
expandedNode
);
GoalNode
<
KeyData
>
last
=
null
;
for
(
Goal
newGoalNode
:
ngoals
)
{
KeyData
kdn
=
new
KeyData
(
kd
,
newGoalNode
.
node
());
/* currentProof.getSubtreeGoals(currentProof.root()).forEach(goal -> {
cases.put(goal.node(), new Statements());
});*/
if
(
ngoals
.
size
()
>
1
)
{
for
(
Goal
newGoalNode
:
ngoals
)
{
KeyData
kdn
=
new
KeyData
(
kd
,
newGoalNode
.
node
());
goals
.
add
(
last
=
new
GoalNode
<>(
expandedNode
,
kdn
,
kdn
.
getNode
().
isClosed
()));
cases
.
put
(
last
.
getData
().
getNode
(),
new
Statements
());
}
}
else
{
KeyData
kdn
=
new
KeyData
(
kd
,
ngoals
.
get
(
0
).
node
());
goals
.
add
(
last
=
new
GoalNode
<>(
expandedNode
,
kdn
,
kdn
.
getNode
().
isClosed
()));
Node
currentNode
=
last
.
getData
().
getNode
();
cases
.
get
(
findRoot
(
currentNode
)).
add
(
call
);
}
if
(
last
!=
null
)
model
.
setSelectedGoalNodeToShow
(
last
);
...
...
@@ -319,6 +325,17 @@ public class InteractiveModeController {
}
private
String
format
(
String
branchingLabel
)
{
// System.out.println("branchingLabel = " + branchingLabel);
String
newLabel
=
branchingLabel
;
if
(
branchingLabel
.
endsWith
(
"$$"
))
{
newLabel
=
branchingLabel
.
substring
(
0
,
branchingLabel
.
length
()
-
2
);
newLabel
+=
".*"
;
// System.out.println("newLabel = " + newLabel);
}
return
newLabel
;
}
public
boolean
isActivated
()
{
return
activated
.
get
();
}
...
...
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