Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
sarah.grebing
ProofScriptParser
Commits
880c6ea1
Commit
880c6ea1
authored
Aug 30, 2017
by
Sarah Grebing
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
changes to paths
parent
165768de
Pipeline
#13224
failed with stage
in 13 seconds
Changes
8
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
8 changed files
with
60 additions
and
15 deletions
+60
-15
lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4
.../antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4
+4
-4
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
...in/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
+1
-1
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java
.../java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java
+4
-4
pom.xml
pom.xml
+1
-1
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
...ava/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
+5
-2
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java
...va/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java
+10
-3
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/help.html
...du/kit/iti/formal/psdbg/examples/contraposition/help.html
+3
-0
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
...u/kit/iti/formal/psdbg/examples/contraposition/script.kps
+32
-0
No files found.
lang/src/main/antlr4/edu/kit/iti/formal/psdbg/parser/ScriptLanguage.g4
View file @
880c6ea1
...
...
@@ -107,18 +107,18 @@ repeatStmt
casesStmt
: CASES INDENT
casesList*
(DEFAULT COLON? INDENT
(DEFAULT COLON? INDENT
?
defList=stmtList
DEDENT)?
DEDENT
?
)?
DEDENT
;
casesList
:
CASE
(TRY | expression | closesExpression) COLON? INDENT stmtList DEDENT
: (TRY |
CASE (
expression | closesExpression)
)
COLON? INDENT
?
stmtList DEDENT
?
;
closesExpression
: CLOSES closesScript=
scriptCommand
: CLOSES
INDENT
closesScript=
stmtList DEDENT
;
forEachStmt
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
View file @
880c6ea1
...
...
@@ -328,7 +328,7 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
ClosesCase
closesCase
=
new
ClosesCase
();
closesCase
.
setClosedStmt
(
true
);
closesCase
.
setRuleContext
(
ctx
);
closesCase
.
setClosesScript
((
Call
Statement
)
ctx
.
closesExpression
().
closesScript
.
accept
(
this
));
closesCase
.
setClosesScript
((
Statement
s
)
ctx
.
closesExpression
().
closesScript
.
accept
(
this
));
closesCase
.
setBody
((
Statements
)
ctx
.
stmtList
().
accept
(
this
));
return
closesCase
;
...
...
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/ClosesCase.java
View file @
880c6ea1
...
...
@@ -16,7 +16,7 @@ public class ClosesCase extends CaseStatement {
/**
* Script that should be executed and shown whether case can be closed
*/
private
Call
Statement
closesScript
;
private
Statement
s
closesScript
;
/**
* A close subscript() {bodyscript} expression
...
...
@@ -24,7 +24,7 @@ public class ClosesCase extends CaseStatement {
* @param closesScript the script that is exectued in order to determine whether goal would clos. This proof is pruned afterwards
* @param body the actual script that is then executed when closesscript was successful and pruned
*/
public
ClosesCase
(
Call
Statement
closesScript
,
Statements
body
)
{
public
ClosesCase
(
Statement
s
closesScript
,
Statements
body
)
{
this
.
body
=
body
;
this
.
closesScript
=
closesScript
;
}
...
...
@@ -41,8 +41,8 @@ public class ClosesCase extends CaseStatement {
* {@inheritDoc}
*/
@Override
public
try
Case
copy
()
{
return
new
tryCase
(
body
.
copy
());
public
Closes
Case
copy
()
{
return
new
ClosesCase
(
closesScript
.
copy
(),
body
.
copy
());
}
}
pom.xml
View file @
880c6ea1
...
...
@@ -57,7 +57,7 @@
<module>
rt
</module>
<module>
rt-key
</module>
<module>
ui
</module>
<module>
DockFX
</module>
<module>
lib/
DockFX
</module>
<module>
lint
</module>
<module>
keydeps
</module>
<module>
matcher
</module>
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java
View file @
880c6ea1
...
...
@@ -39,8 +39,11 @@ public class ProofScriptDebugger extends Application {
Locale
.
setDefault
(
Locale
.
ENGLISH
);
try
{
FXMLLoader
fxmlLoader
=
new
FXMLLoader
(
getClass
().
getResource
(
"controller/DebuggerMain.fxml"
));
// FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource(
// "controller/DebuggerMain.fxml"));
FXMLLoader
fxmlLoader
=
new
FXMLLoader
(
getClass
().
getResource
(
"/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml"
));
//"/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml"));
Parent
root
=
fxmlLoader
.
load
();
//DebuggerMain controller = fxmlLoader.<DebuggerMain>getController();
Scene
scene
=
new
Scene
(
root
);
...
...
ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java
View file @
880c6ea1
package
edu.kit.iti.formal.psdbg.gui.controls
;
import
edu.kit.iti.formal.psdbg.examples.Examples
;
import
edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain
;
import
javafx.event.ActionEvent
;
import
javafx.scene.layout.AnchorPane
;
...
...
@@ -21,13 +22,19 @@ public class WelcomePane extends AnchorPane {
public
void
loadContraPosition
(
ActionEvent
event
)
{
proofScriptDebugger
.
getWelcomePaneDock
().
close
();
proofScriptDebugger
.
showActiveInspector
(
null
);
proofScriptDebugger
.
openScript
(
new
File
(
"src/test/resources/edu/kit/formal/psdb/interpreter/contraposition/w_branching.kps"
)
Examples
.
loadExamples
().
forEach
(
example
->
{
if
(
example
.
getName
().
equals
(
"Contraposition"
))
example
.
open
(
proofScriptDebugger
);
});
/* proofScriptDebugger.openScript(
new File("")
);
proofScriptDebugger.openKeyFile(
new File("src/test/resources/edu/kit/formal/psdb/interpreter/contraposition/contraposition.key"));
*/
}
public
void
loadJavaTest
(
ActionEvent
event
)
{
...
...
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/help.html
View file @
880c6ea1
<html>
<body>
<h1>
Contraposition
</h1>
<p>
To load a script it needs to be called in the main script.
For example to load the script cpwob() type
<i>
cpwob;
</i>
in the body of the script
<i>
main()
</i></p>
</body>
</html>
\ No newline at end of file
ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
View file @
880c6ea1
...
...
@@ -16,4 +16,36 @@ script cpwob () {
replace_known_left occ='2';
concrete_impl_1;
close;
}
script cpwb () {
impRight;
impLeft;
cases{
case match `==> p`:{
auto;
}
default:{
auto;
}
}
}
script cpClosable(){
impRight;
impRight;
cases{
case try:{
notLeft;
notRight;
replace_known_left occ='2';
concrete_impl_1;
close;
}
default:{
auto;
}
}
}
\ No newline at end of file
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