Commit b193e370 authored by Sarah Grebing's avatar Sarah Grebing
Browse files

Extra Exception for not applicable script commands and some adaptations for...

Extra Exception for not applicable script commands and some adaptations for readme (based on Mattias Readme)
parent e237f563
Pipeline #12560 failed with stage
in 1 minute and 33 seconds
...@@ -8,7 +8,11 @@ start ...@@ -8,7 +8,11 @@ start
: (script)* : (script)*
; ;
script: SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT; script
: SCRIPT name=ID '(' signature=argList? ')' INDENT body=stmtList DEDENT
;
argList argList
: varDecl (',' varDecl)* : varDecl (',' varDecl)*
; ;
...@@ -110,7 +114,7 @@ casesStmt ...@@ -110,7 +114,7 @@ casesStmt
casesList casesList
// : simpleCase // : simpleCase
// | closableCase // | closableCase
: CASE (MATCH ISCLOSED | expression) COLON? INDENT stmtList DEDENT : CASE (ISCLOSED | expression) COLON? INDENT stmtList DEDENT
; ;
/*simpleCase /*simpleCase
: CASE expression COLON? INDENT stmtList DEDENT : CASE expression COLON? INDENT stmtList DEDENT
......
...@@ -9,6 +9,7 @@ import de.uka.ilkd.key.proof.Goal; ...@@ -9,6 +9,7 @@ import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.Proof;
import edu.kit.formal.interpreter.data.*; import edu.kit.formal.interpreter.data.*;
import edu.kit.formal.interpreter.exceptions.InterpreterRuntimeException; import edu.kit.formal.interpreter.exceptions.InterpreterRuntimeException;
import edu.kit.formal.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.interpreter.funchdl.CommandLookup;
import edu.kit.formal.proofscriptparser.DefaultASTVisitor; import edu.kit.formal.proofscriptparser.DefaultASTVisitor;
import edu.kit.formal.proofscriptparser.Visitor; import edu.kit.formal.proofscriptparser.Visitor;
...@@ -179,12 +180,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -179,12 +180,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
System.out.println("IsClosable was not successful, rolling back proof"); System.out.println("IsClosable was not successful, rolling back proof");
Proof currentKeYproof = ((KeyData) selectedGoalNode.getData()).getProof(); Proof currentKeYproof = ((KeyData) selectedGoalNode.getData()).getProof();
ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode()); ImmutableList<Goal> subtreeGoals = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
//subtreeGoals.forEach(goal -> System.out.println(goal.node().serialNr()));
//System.out.println(subtreeGoals);
currentKeYproof.pruneProof(((KeyData) selectedGoalCopy.getData()).getNode()); currentKeYproof.pruneProof(((KeyData) selectedGoalCopy.getData()).getNode());
//ImmutableList<Goal> subtreeGoals1 = currentKeYproof.getSubtreeGoals(((KeyData) selectedGoalNode.getData()).getNode());
//subtreeGoals1.forEach(goal -> System.out.println(goal.node().serialNr()));
popState(); popState();
pushState(currentStateToMatchCopy); pushState(currentStateToMatchCopy);
} }
...@@ -433,7 +429,14 @@ public class Interpreter<T> extends DefaultASTVisitor<Object> ...@@ -433,7 +429,14 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
VariableAssignment params = evaluateParameters(call.getParameters()); VariableAssignment params = evaluateParameters(call.getParameters());
GoalNode<T> g = getSelectedNode(); GoalNode<T> g = getSelectedNode();
g.enterScope(); g.enterScope();
functionLookup.callCommand(this, call, params); try {
functionLookup.callCommand(this, call, params);
} catch (ScriptCommandNotApplicableException e) {
//TODO handling of error state for each visit
State<T> newErrorState = newState(null, null);
newErrorState.setErrorState(true);
pushState(newErrorState);
}
g.exitScope(); g.exitScope();
exitScope(call); exitScope(call);
return null; return null;
......
...@@ -31,6 +31,7 @@ public class State<T> { ...@@ -31,6 +31,7 @@ public class State<T> {
private GoalNode<T> selectedGoalNode; private GoalNode<T> selectedGoalNode;
@Getter @Getter
@Setter
private boolean errorState; private boolean errorState;
......
package edu.kit.formal.interpreter.exceptions;
import de.uka.ilkd.key.macros.scripts.RuleCommand;
import java.util.Map;
/**
* Exception for not applicable Rules
*/
public class ScriptCommandNotApplicableException extends RuntimeException {
public ScriptCommandNotApplicableException(Exception e) {
super(e);
}
public ScriptCommandNotApplicableException(Exception e, RuleCommand c) {
System.out.println("Call " + c.getName() + " was not applicable");
}
public ScriptCommandNotApplicableException(Exception e, RuleCommand c, Map<String, String> params) {
StringBuffer sb = new StringBuffer();
sb.append("Call " + c.getName() + " with parameters ");
for (String s : params.keySet()) {
sb.append(params.get(s));
}
sb.append(" was not applicable");
System.out.println(sb.toString());
}
}
...@@ -4,6 +4,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; ...@@ -4,6 +4,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl;
import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
import de.uka.ilkd.key.macros.scripts.EngineState; import de.uka.ilkd.key.macros.scripts.EngineState;
import de.uka.ilkd.key.macros.scripts.RuleCommand; import de.uka.ilkd.key.macros.scripts.RuleCommand;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.Rule;
import edu.kit.formal.interpreter.Interpreter; import edu.kit.formal.interpreter.Interpreter;
...@@ -11,6 +12,7 @@ import edu.kit.formal.interpreter.data.GoalNode; ...@@ -11,6 +12,7 @@ import edu.kit.formal.interpreter.data.GoalNode;
import edu.kit.formal.interpreter.data.KeyData; import edu.kit.formal.interpreter.data.KeyData;
import edu.kit.formal.interpreter.data.State; import edu.kit.formal.interpreter.data.State;
import edu.kit.formal.interpreter.data.VariableAssignment; import edu.kit.formal.interpreter.data.VariableAssignment;
import edu.kit.formal.interpreter.exceptions.ScriptCommandNotApplicableException;
import edu.kit.formal.proofscriptparser.ast.CallStatement; import edu.kit.formal.proofscriptparser.ast.CallStatement;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
...@@ -40,7 +42,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -40,7 +42,7 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
@Override @Override
public void evaluate(Interpreter<KeyData> interpreter, public void evaluate(Interpreter<KeyData> interpreter,
CallStatement call, CallStatement call,
VariableAssignment params) { VariableAssignment params) throws IllegalStateException, RuntimeException, ScriptCommandNotApplicableException {
if (!rules.containsKey(call.getCommand())) { if (!rules.containsKey(call.getCommand())) {
throw new IllegalStateException(); throw new IllegalStateException();
} }
...@@ -67,7 +69,12 @@ public class RuleCommandHandler implements CommandHandler<KeyData> { ...@@ -67,7 +69,12 @@ public class RuleCommandHandler implements CommandHandler<KeyData> {
state.getGoals().add(new GoalNode<>(expandedNode, kdn)); state.getGoals().add(new GoalNode<>(expandedNode, kdn));
} }
} catch (Exception e) { } catch (Exception e) {
throw new RuntimeException(e); if (e.getClass().equals(ScriptException.class)) {
throw new ScriptCommandNotApplicableException(e, c, map);
} else {
throw new RuntimeException(e);
}
} }
} }
......
...@@ -6,130 +6,80 @@ ...@@ -6,130 +6,80 @@
</head> </head>
<body> <body>
<h1>Language Constructs</h1> <h1>Language Constructs</h1>
<h2>Proof Commands</h2> This description is an adapted version of the README for script commands in KeY by Mattias Ulbrich.
<h3>KeY Rules</h3>
All KeY rules can be used as proof command.
The following command structure is used to apply single KeY rules onto a selected goal node.
<br> <br>
RULENAME
<!--Apply a single rule onto the current sequent. As unnamed argument add
the name of the taclet to be applied. If the taclet matches only once
on the entire sequent, the rule is applied. If it matches more than
once you need to specify more. In that case you can first specify the
sequence formula and then the number of the occurrence in the formula
or the specific subterm via the 'on' keyword.
If a rule has schema variables which must be instantiated manually,
such instantiations can be provided as arguments. A schema variable
named sv can be instantiated by setting the argument sv="..." or by
setting inst_sv="..." (the latter works also for conflict cases like
inst_occ="...").
Examples:
rule andRight;
# if there is only one matching spot on the sequent
rule eqSymm formula="a=b";
# changes sequent "a=b ==> c=d" to "b=a ==> c=d"
# "rule eqSymm;" alone would have been ambiguous.
rule eqSymm formula="a=b->c=d" occ=2;
# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
# occurrence number needed since there are
# two possible applications on the formula
rule eqSymm formula="a=b->c=d" on="c=d";
# changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
# same as above, but using the option to specify a
# subterm instead of an occurrence number.
rule cut cutFormula="x > y";
# almost the same as 'cut "x>y"'
-->
<!--A rule command has the following syntax:<br>
RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")?
<br>with:
<ul>
<li>TERM</li>
<li>TOP_LEVEL_FORMULA</li>
</ul>
FROM MATTIAS:
Making interactive persistent using proof scripts
=================================================
Mattias Ulbrich <ulbrich@kit.edu>, 2015
Experimental feature: Proof scripts are currently only visible in the
GUI if KeY is launched with the --experimental option. Concrete syntax
is subject to change.
Every KeY user knows the pain of manually redoing an interactive proof
over and over again even though only a tiny bit of the program or
specification have changed. NOW you can use proof scripts which will
alleviate your worries with repeating proofs.
Proof scripts are textual representations of rule applications, Proof scripts are textual representations of rule applications,
settings changes and macro invocations. They are notated in linear settings changes and macro invocations.
order. The target of a script command is usually the first open goal
in the proof tree, i.e., the first reached when traversing the proof
tree (not necessarily the first in the "Goal" pane in the GUI).
<h2>Proof Commands</h2>
Syntax of proof scripts
-----------------------
Proof commands start with an identifier followed by optional Proof commands start with an identifier followed by optional
arguments: arguments:
<br>
command argName="argument" "argument without name" ; command argName="argument" "argument without name" ;
<br>
Every command is terminated with a semicolon. There are named Every command is terminated with a semicolon. There are named
arguments in the form argName="argument" and unnamed argument without arguments in the form argName="argument" and unnamed argument without
name. Single '...'and double quotes "..." can both be used. If name. Single '...'and double quotes "..." can both be used.
"argument" is an identifier itself, the quotes can optionally be <br>
dropped, like in Single-line comments are start with //.
rule andRight ;
The character # begins a comment which extends to the end of the
line. Currently, there are no multi-line comments in proof scripts.
Proof scripts are case sensitive.
How can scripts be loaded
-------------------------
1. In the GUI:
Open a proof obligation. Currently proof scripts work only reliably if <h3>KeY Rules</h3>
applied to the root of a fresh proof obligation (no rule applications, All KeY rules can be used as proof command.
prune steps). The open the context menu (sequent or proof tree), The following command structure is used to apply single KeY rules onto the sequent of a selected goal node.
choose "Strategy macros" and then "Run proof script ...". In the file If no argument is following the proof command the taclet corresponding to this command has to match at most once on the
dialog that appears, choose the script file to load. The script is sequent.
automatically applied. You can follow the process in a logging window. If more terms or formulas to which a proof command is applicable exist, arguments have to be
given that indicate the where to apply the rule to.
<br>
A rule command has the following syntax:<br>
RULENAME (on="TERM")? (formula="TOP_LEVEL_FORMULA")? (occ="OCCURENCE_IN_SEQUENT")? (inst_="TERM")? (maxSteps=INT)
<br>with:
<ul>
<li>TERM: specific sub-term</li>
<li>TOP_LEVEL_FORMULA: specific top level formula</li>
<li>OCCURENCE_IN_SEQUENT: Number of occurence in the sequent</li>
<li>maxSteps: the number of steps KEY should at most use until it terminateds teh proof search</li>
</ul>
2. From within key input files: If a rule has schema variables which must be instantiated manually,
such instantiations can be provided as arguments. A schema variable
named sv can be instantiated by setting the argument sv="..." or by
setting inst_sv="..." (the latter works also for conflict cases like
inst_occ="...").
At the very end of key files *INSTEAD* of a \proof object, you can now
attach a proof script directly in double quotes following the keyword
\proofScript. An very simple example reads:
----------8<---------- <h4>Examples</h4>
\predicates {a; b;} <ul>
\problem { a & b -> a } <li>andRight;</li>
<br>
Applicable iff there is only one matching spot on the sequent
<li>eqSymm formula="a=b";</li>
<br>
This command changes the sequent "a=b ==> c=d" to "b=a ==> c=d"
Using only "eqSymm;" alone would have been ambiguous.
<li>eqSymm formula="a=b->c=d" occ=2;</li>
<br>
This command changes sequent "a=b->c=d ==>" to "a=b->d=c ==>".
The occurrence number is needed since there are two possible applications on the formula
<li>eqSymm formula="a=b->c=d" on="c=d";</li>
<br>
This command changes the sequent "a=b->c=d ==>" to "a=b->d=c ==>".
It is simialr to the example above, but here the option to specify a
subterm instead of an occurrence number is used.
<li>cut cutFormula="x > y";</li>
<br>
This command is almost the same as 'cut "x>y"'
\proofScript " </ul>
rule 'impRight'; <h3>Macro-Commands</h3>
rule 'andLeft';
rule 'close';"
----------8<----------
Since the script is no enclosed in "...", only single quotes '...' can <!--
be used in the script. You can also load a script from an external
file by writing
\proofScript "script 'some_filename.script';"
Commands in scripts Commands in scripts
......
...@@ -2,7 +2,7 @@ script t1(){ ...@@ -2,7 +2,7 @@ script t1(){
impRight; impRight;
impLeft; impLeft;
cases{ cases{
case match isCloseable:{ case isCloseable:{
impRight; //should not close proof impRight; //should not close proof
} }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment