-
Notifications
You must be signed in to change notification settings - Fork 22
/
FocusCommand.java
126 lines (101 loc) · 4.56 KB
/
FocusCommand.java
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
package de.uka.ilkd.key.macros.scripts;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.macros.scripts.meta.Option;
import de.uka.ilkd.key.proof.Goal;
import de.uka.ilkd.key.rule.FindTaclet;
import de.uka.ilkd.key.rule.PosTacletApp;
import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp;
import de.uka.ilkd.key.rule.inst.SVInstantiations;
import org.key_project.util.collection.ImmutableList;
import java.util.Iterator;
import java.util.Set;
/**
* Hide all formulas that are not selected Parameter: * The sequent with those formulas that should
* not be hidden Created by sarah on 1/12/17.
*/
public class FocusCommand extends AbstractCommand<FocusCommand.Parameters> {
public FocusCommand() {
super(Parameters.class);
}
static class Parameters {
@Option("#2")
public Sequent toKeep;
}
@Override
public void execute(Parameters s) throws ScriptException, InterruptedException {
if (s == null) {
throw new ScriptException("Missing 'sequent' argument for focus");
}
Sequent toKeep = s.toKeep;
// toKeep = parseSequent(sequentString, getGoalFromCurrentState());
hideAll(toKeep);
}
@Override
public String getName() {
return "focus";
}
/*
* private Goal getGoalFromCurrentState() { Object fixedGoal = stateMap.get(GOAL_KEY); if
* (fixedGoal instanceof Node) { Node fixed = (Node) fixedGoal; //case node is already modified
* by focus, the child has to be returned if (!fixed.leaf()) { assert fixed.childrenCount() ==
* 1; fixed = fixed.child(0); } Goal g = state.getGoal(proof.openGoals(), fixed); return g; }
* return null; }
*/
/**
* Hide all formulas of the sequent that are not on focus sequent
*
* @param toKeep sequent containing formulas to keep
* @throws ScriptException if no goal is currently open
*/
private void hideAll(Sequent toKeep) throws ScriptException {
Goal goal = state.getFirstOpenAutomaticGoal();
assert goal != null : "not null by contract of the method";
// The formulas to keep in the antecedent
ImmutableList<Term> keepAnte = toKeep.antecedent().asList().map(SequentFormula::formula);
ImmutableList<SequentFormula> ante = goal.sequent().antecedent().asList();
for (SequentFormula seqFormula : ante) {
// This means "!keepAnte.contains(seqFormula.formula)" but with equality mod renaming!
if (!keepAnte.exists(it -> it.equalsModRenaming(seqFormula.formula()))) {
Taclet tac = getHideTaclet("left");
makeTacletApp(goal, seqFormula, tac, true);
}
}
ImmutableList<Term> keepSucc = toKeep.succedent().asList().map(SequentFormula::formula);
ImmutableList<SequentFormula> succ = goal.sequent().succedent().asList();
for (SequentFormula seqFormula : succ) {
if (!keepSucc.exists(it -> it.equalsModRenaming(seqFormula.formula()))) {
Taclet tac = getHideTaclet("right");
makeTacletApp(goal, seqFormula, tac, false);
}
}
}
// determine where formula in sequent and apply either hide_left or hide_right
private Taclet getHideTaclet(String pos) {
String ruleName = "hide_" + pos;
return proof.getEnv().getInitConfigForEnvironment().lookupActiveTaclet(new Name(ruleName));
}
/**
* Make tacletApp for one sequent formula to hide on the sequent
*
* @param g the goal on which this hide rule should be applied to
* @param toHide the sequent formula to hide
* @param tac the taclet top apply (either hide_left or hide_right)
* @param antec whether the formula is in the antecedent
*/
private void makeTacletApp(Goal g, SequentFormula toHide, Taclet tac, boolean antec) {
// hide rules only applicable to top-level terms/sequent formulas
PosInTerm pit = PosInTerm.getTopLevel();
PosInOccurrence pio = new PosInOccurrence(toHide, pit, antec);
Set<SchemaVariable> svs = tac.collectSchemaVars();
assert svs.size() == 1;
Iterator<SchemaVariable> iter = svs.iterator();
SchemaVariable sv = (SchemaVariable) iter.next();
SVInstantiations inst = SVInstantiations.EMPTY_SVINSTANTIATIONS;
TacletApp app =
PosTacletApp.createPosTacletApp((FindTaclet) tac, inst, pio, proof.getServices());
app = app.addCheckedInstantiation(sv, toHide.formula(), proof.getServices(), true);
g.apply(app);
}
}