Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
sarah.grebing
ProofScriptParser
Commits
b08c1ba4
Commit
b08c1ba4
authored
Sep 12, 2017
by
Sarah Grebing
Browse files
Some changes to handle ambigous commands
parent
40e5a455
Pipeline
#13557
failed with stage
in 2 minutes and 31 seconds
Changes
6
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
lang/src/main/java/edu/kit/iti/formal/psdbg/parser/TransformAst.java
View file @
b08c1ba4
...
...
@@ -41,6 +41,10 @@ import java.util.Map;
* @version 1 (27.04.17)
*/
public
class
TransformAst
implements
ScriptLanguageVisitor
<
Object
>
{
/**
* Start Index for positional arguments for command calls
*/
public
static
final
int
KEY_START_INDEX_PARAMETER
=
2
;
private
List
<
ProofScript
>
scripts
=
new
ArrayList
<>(
10
);
...
...
@@ -380,7 +384,9 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
@Override
public
Object
visitParameters
(
ScriptLanguageParser
.
ParametersContext
ctx
)
{
Parameters
params
=
new
Parameters
();
int
i
=
1
;
int
i
=
KEY_START_INDEX_PARAMETER
;
for
(
ScriptLanguageParser
.
ParameterContext
pc
:
ctx
.
parameter
())
{
Expression
expr
=
(
Expression
)
pc
.
expr
.
accept
(
this
);
Variable
key
=
pc
.
pname
!=
null
?
new
Variable
(
pc
.
pname
)
:
new
Variable
(
"#"
+
(
i
++));
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/InterpreterBuilder.java
View file @
b08c1ba4
...
...
@@ -51,7 +51,7 @@ public class InterpreterBuilder {
@Getter
private
ScopeLogger
logger
;
@Getter
private
DefaultLookup
lookup
=
new
DefaultLookup
(
psh
,
pmh
,
pm
r
,
pm
c
);
private
DefaultLookup
lookup
=
new
DefaultLookup
(
psh
,
pmh
,
pm
c
,
pm
r
);
private
KeyInterpreter
interpreter
=
new
KeyInterpreter
(
lookup
);
@Getter
...
...
rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptCommandBuilder.java
View file @
b08c1ba4
...
...
@@ -21,7 +21,7 @@ import java.util.HashMap;
import
java.util.Map
;
/**
* This class handle the call of key's proof script commands, e.g. select or auto;
* This class handle
s
the call of key's proof script commands, e.g. select or auto;
*
* @author Alexander Weigl
* @version 1 (21.05.17)
...
...
@@ -56,7 +56,6 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
KeyData
kd
=
expandedNode
.
getData
();
Map
<
String
,
String
>
map
=
new
HashMap
<>();
params
.
asMap
().
forEach
((
k
,
v
)
->
map
.
put
(
k
.
getIdentifier
(),
v
.
getData
().
toString
()));
//System.out.println(map);
try
{
EngineState
estate
=
new
EngineState
(
kd
.
getProof
());
estate
.
setGoal
(
kd
.
getNode
());
...
...
rt-key/src/test/resources/edu/kit/iti/formal/psdbg/interpreter/contraposition/cutTest.kps
View file @
b08c1ba4
script cutTest(){
cases{
case match `==>?X -> ?Y`:
cut `p`;
//cases{
// case match `==>?X -> ?Y`:
//auto steps=100;
//cut formula=`?X`[];
}
//
}
//cut #2=`p`;
//auto steps=100;
}
\ No newline at end of file
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/Interpreter.java
View file @
b08c1ba4
...
...
@@ -34,7 +34,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
//TODO later also include information about source line for each state (for debugging purposes and rewind purposes)
private
Stack
<
State
<
T
>>
stateStack
=
new
Stack
<>();
//We now need thet stack of listeners to handle try statements scuh that listnersa re only informed if a try was sucessfull
private
Stack
<
List
<
Visitor
>>
entryListenerStack
=
new
Stack
<>();
private
Stack
<
List
<
Visitor
>>
exitListenerStack
=
new
Stack
<>();
...
...
@@ -517,10 +517,12 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
try
{
functionLookup
.
callCommand
(
this
,
call
,
params
);
}
catch
(
RuntimeException
e
)
{
System
.
err
.
println
(
"Call command not applicable"
);
throw
e
;
//TODO handling of error state for each visit
State
<
T
>
newErrorState
=
newState
(
null
,
null
);
newErrorState
.
setErrorState
(
true
);
pushState
(
newErrorState
);
//
State<T> newErrorState = newState(null, null);
//
newErrorState.setErrorState(true);
//
pushState(newErrorState);
}
g
.
exitScope
();
exitScope
(
call
);
...
...
rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/DefaultLookup.java
View file @
b08c1ba4
...
...
@@ -53,18 +53,9 @@ public class DefaultLookup implements CommandLookup {
if
(
b
.
handles
(
callStatement
))
{
foundHandlers
.
add
(
b
);
found
=
b
;
/*if (found == null) {
found = b;
} else {
found = b; //CUTCommand
System.out.println(b.getClass());
System.out.println(found.getClass());
if (callStatement.getCommand().equals("cut")) {
System.out.println("Cut Case");
}
//throw new IllegalStateException("Call on line" + callStatement + " is ambigue.");
}*/
}
else
{
//if a proof macro contains a "-" character, the proof script language does not support this.
// Therefore we have to check for both versions
if
(
mayBeEscapedMacro
)
{
String
command
=
callStatement
.
getCommand
();
callStatement
.
setCommand
(
command
.
replace
(
"_"
,
"-"
));
...
...
@@ -75,13 +66,9 @@ public class DefaultLookup implements CommandLookup {
}
}
}
if
(
foundHandlers
.
size
()
==
1
)
return
foundHandlers
.
get
(
0
);
if
(
foundHandlers
.
size
()
>
1
)
{
return
foundHandlers
.
get
(
0
);
}
else
{
if
(
foundHandlers
.
size
()
>=
1
)
return
foundHandlers
.
get
(
0
);
throw
new
NoCallHandlerException
(
callStatement
);
}
}
@Override
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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