Commit a02f781f authored by Sarah Grebing's avatar Sarah Grebing

First attempt for new Case-Handling (still containing a bug)

parent 5c62d788
Pipeline #12198 failed with stage
in 1 minute and 39 seconds
......@@ -25,7 +25,7 @@ import java.util.logging.Logger;
*
* @author S.Grebing
*/
public class Interpreter<T> extends DefaultASTVisitor<Void>
public class Interpreter<T> extends DefaultASTVisitor<Object>
implements ScopeObservable {
private static final int MAX_ITERATIONS = 5;
@Getter
......@@ -79,7 +79,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
* @return
*/
@Override
public Void visit(ProofScript proofScript) {
public Object visit(ProofScript proofScript) {
enterScope(proofScript);
//add vars
visit(proofScript.getSignature());
......@@ -95,7 +95,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
* @return
*/
@Override
public Void visit(AssignmentStatement assignmentStatement) {
public Object visit(AssignmentStatement assignmentStatement) {
enterScope(assignmentStatement);
GoalNode<T> node = getSelectedNode();
......@@ -152,26 +152,92 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
return null;
}
@Override
public Object visit(IsClosableCase isClosableCase) {
State<T> currentStateToMatch = peekState();
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
enterScope(isClosableCase);
//executebody
exitScope(isClosableCase);
return false;
}
@Override
public Object visit(SimpleCaseStatement simpleCaseStatement) {
Expression matchExpression = simpleCaseStatement.getGuard();
State<T> currentStateToMatch = peekState();
GoalNode<T> selectedGoal = currentStateToMatch.getSelectedGoalNode();
VariableAssignment va = evaluateMatchInGoal(matchExpression, selectedGoal);
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;
*/
}
/**
* @param casesStatement
* @return
*/
@Override
public Void visit(CasesStatement casesStatement) {
public Object visit(CasesStatement casesStatement) {
enterScope(casesStatement);
State<T> beforeCases = peekState();
List<GoalNode<T>> allGoalsBeforeCases = beforeCases.getGoals();
//global List after all Case Statements
List<GoalNode<T>> goalsAfterCases = new ArrayList<>();
//copy the list of goal nodes for keeping track of goals
Set<GoalNode<T>> remainingGoalsSet = new HashSet<>(allGoalsBeforeCases);
//TODO
//handle cases
List<CaseStatement> cases = casesStatement.getCases();
for (CaseStatement aCase : cases) {
for (GoalNode<T> goalBeforeCase : allGoalsBeforeCases) {
State<T> createdState = newState(goalBeforeCase);//to allow the case to retrieve goal
for (CaseStatement aCase : cases) {
boolean result = (boolean) aCase.accept(this);
if (result) {
//remove goal from set for default
remainingGoalsSet.remove(goalBeforeCase);
//case statement matched and was executed
break;
}
}
//remove state from stack
State<T> stateAfterCase = popState();
if (stateAfterCase.getGoals() != null) {
goalsAfterCases.addAll(stateAfterCase.getGoals());
}
}
//===========================================================================================//
/* for (CaseStatement aCase : cases) {
if (aCase.isClosedStmt) {
System.out.println("IsClosableStmt not implemented yet");
} else {
......@@ -183,7 +249,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
}
}
}
}*/
//for all remaining goals execute default
if (!remainingGoalsSet.isEmpty()) {
......@@ -227,14 +293,11 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
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;
}
......@@ -244,7 +307,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
*
* @param matchExpression
* @param goal
* @return null, if match was false, return teh first Assignment when match was true
* @return null, if match was false, return the first Assignment when match was true
*/
private VariableAssignment evaluateMatchInGoal(Expression matchExpression, GoalNode<T> goal) {
enterScope(matchExpression);
......@@ -308,16 +371,6 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
return s;
}
/**
* @param caseStatement
* @return
*/
/* @Override
public Void visit(CaseStatement caseStatement) {
enterScope(caseStatement);
exitScope(caseStatement);
return null;
}*/
/**
* Visiting a call statement results in:
......@@ -332,7 +385,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
* @return
*/
@Override
public Void visit(CallStatement call) {
public Object visit(CallStatement call) {
enterScope(call);
//neuer VarScope
//enter new variable scope
......@@ -357,7 +410,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
}
@Override
public Void visit(TheOnlyStatement theOnly) {
public Object visit(TheOnlyStatement theOnly) {
List<GoalNode<T>> goals = getCurrentState().getGoals();
if (goals.size() > 1) {
throw new IllegalArgumentException(
......@@ -381,7 +434,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
* @return
*/
@Override
public Void visit(ForeachStatement foreach) {
public Object visit(ForeachStatement foreach) {
enterScope(foreach);
List<GoalNode<T>> allGoals = getCurrentGoals();
List<GoalNode<T>> goalsAfterForeach = new ArrayList<>();
......@@ -399,7 +452,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
}
@Override
public Void visit(RepeatStatement repeatStatement) {
public Object visit(RepeatStatement repeatStatement) {
enterScope(repeatStatement);
int counter = 0;
boolean b = false;
......@@ -419,7 +472,7 @@ public class Interpreter<T> extends DefaultASTVisitor<Void>
}
@Override
public Void visit(Signature signature) {
public Object visit(Signature signature) {
exitScope(signature);
GoalNode<T> node = getSelectedNode();
node.enterScope();
......
......@@ -152,6 +152,11 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
return createBinaryExpression(ctx, ctx.expression(), findOperator(ctx.op.getText()));
}
@Override
public Object visitExprSubs(ScriptLanguageParser.ExprSubsContext ctx) {
return null;
}
private Operator findOperator(String n) {
return findOperator(n, 2);
}
......@@ -215,6 +220,12 @@ public class TransformAst implements ScriptLanguageVisitor<Object> {
}
//TODO implement
@Override
public Object visitSubstExpression(ScriptLanguageParser.SubstExpressionContext ctx) {
return null;
}
@Override
public Object visitLiteralID(ScriptLanguageParser.LiteralIDContext ctx) {
return new Variable(ctx.ID().getSymbol());
......
......@@ -4,5 +4,260 @@
<meta content="">
<style></style>
</head>
<body>Test</body>
<body>
<h1>Language Constructs</h1>
<h2>Proof Commands</h2>
All KeY rules can be used as proof command.
<!--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,
settings changes and macro invocations. They are notated in linear
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).
Syntax of proof scripts
-----------------------
Proof commands start with an identifier followed by optional
arguments:
command argName="argument" "argument without name" ;
Every command is terminated with a semicolon. There are named
arguments in the form argName="argument" and unnamed argument without
name. Single '...'and double quotes "..." can both be used. If
"argument" is an identifier itself, the quotes can optionally be
dropped, like in
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
applied to the root of a fresh proof obligation (no rule applications,
prune steps). The open the context menu (sequent or proof tree),
choose "Strategy macros" and then "Run proof script ...". In the file
dialog that appears, choose the script file to load. The script is
automatically applied. You can follow the process in a logging window.
2. From within key input files:
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<----------
\predicates {a; b;}
\problem { a & b -> a }
\proofScript "
rule 'impRight';
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
-------------------
This list of available script commands is subject to change and to
extension. If you write your own script commands (s. below), please
add an explanation to this list here. The list is sorted alphabetically.
-- auto ------------------
Apply the automatic KeY strategy on the current goal. Optinally you
can specify the number of steps to run.
Examples:
auto steps=30000;
# run at most 30000 steps automatically.
-- cut -------------------
Performs a cut and thus splits the sequent into two goals. The unnamed
argument is the formula to cut with
Examples:
cut "value1 = value2";
-- exit ------------------
Terminate the script prematurely at that point. Used mainly for debug
purposes.
Examples:
exit;
-- instantiate -----------
Quantifier instantiation is a task that often occurs. Instead of
specifying the entire formula, it suffices here to name the variable
that is to be instantiated. If that is not unique, the number of the
occurrence of that quantified variable can be specified as well.
Examples:
instantiate var="x" occ="3" with="42"
# Instantiate the third instantiateable formula whose bound
# variable is called "x" with the value 42
instantiate formula="\forall int x; f(x) = 42" with="23"
# The quantified formula can also be specified if wanted.
# This here for the antecedent.
instantiate formula="\exists int x; f(x) = 42" with="23"
# Existentially quantified variables can be instantiated if they
# occur on the succedent side.
instantiate hide var=x value="x_0"
# instantiate x and hide the quantified formula
-- leave -----------------
Mark the currently active goal as non-interactive (the orange hand
symbol in the GUI). It is then excluded from further analysis by
scripts. This is good for debugging unfinished proof scripts.
-- macro -----------------
Invoke a macro on the current goal. The names of available macros
include:
autopilot full autopilot
autopilot-prep preparation only autopilot
split-prop propositional expansion w/ splits
nosplit-prop propositional expansion w/o splits
simp-upd update simplification
simp-heap heap simplification
Examples:
macro autopilot-prep;
(Future version may drop the macro keyword and allow macro invocations
directly.)
-- rule ------------------
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"'
-- script ----------------
Invoke another script which resides in an external file.
Example:
script '/path/to/other/file.script';
-- select ----------------
Unlike most other commands, this command does not change the proof but
chooses the goal on which the next step operates. Currently you can
specify a formula. The goal is chosen such that the formula appears
(toplevel) on the sequent (antecedent or succedent). You can limit the
search to antecedent or succedent.
Examples:
select formula="{ x:=1 }y < x";
# search for the formula anywhere
select succedent formula="wellFormed(someHeap)";
# search only the succedent for the formula
-- smt -------------------
Invoke an external SMT solver. That solver must be adequately
configured outside the script mechanism. By default, Z3 is invoked,
but that can be chosen.
Examples:
smt;
# invoke Z3
smt solver="Z3,yices";
# a comma separated list of solvers can be specified.
-- tryclose --------------
Unlike other commands this command operates on ALL open goals and
effectively applies the "try provable goals below" macro to all of
them. A number of steps can optionally be given.
Examples:
tryclose;
tryclose steps=2000;
# spend 2000 steps on each open goal
Write your on proof commands
----------------------------
to be done.
Contact Mattias, if you are interested.
-->
</body>
</html>
\ No newline at end of file
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