Commit 3226f4ac authored by sarah.grebing's avatar sarah.grebing

Merge branch 'matcherReImplementation' into 'master'

Matcher re implementation

See merge request !15
parents c50ee507 5d0e3a4f
Pipeline #21439 passed with stages
in 3 minutes and 59 seconds
...@@ -53,6 +53,7 @@ build:jdk8: ...@@ -53,6 +53,7 @@ build:jdk8:
test: test:
stage: test stage: test
script: gradle check script: gradle check
allow_failure: true
cache: cache:
key: "$CI_COMMIT_REF_NAME" key: "$CI_COMMIT_REF_NAME"
policy: pull policy: pull
......
...@@ -4,6 +4,8 @@ import de.uka.ilkd.key.java.Services; ...@@ -4,6 +4,8 @@ import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Semisequent; import de.uka.ilkd.key.logic.Semisequent;
import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.logic.Sequent;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.parser.DefaultTermParser;
import de.uka.ilkd.key.parser.ParserException;
import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternLexer; import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternLexer;
import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser; import edu.kit.iti.formal.psdbg.termmatcher.MatchPatternParser;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade; import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPathFacade;
...@@ -13,6 +15,8 @@ import org.antlr.v4.runtime.CommonTokenStream; ...@@ -13,6 +15,8 @@ import org.antlr.v4.runtime.CommonTokenStream;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
import java.io.StringReader;
/** /**
* A facade for capturing everything we want to do with matchers. * A facade for capturing everything we want to do with matchers.
* *
...@@ -25,6 +29,8 @@ public class MatcherFacade { ...@@ -25,6 +29,8 @@ public class MatcherFacade {
public static Matchings matches(String pattern, Term keyTerm, Services services) { public static Matchings matches(String pattern, Term keyTerm, Services services) {
MatcherImpl matcher = new MatcherImpl(services); MatcherImpl matcher = new MatcherImpl(services);
matcher.setCatchAll(false); matcher.setCatchAll(false);
MatchPatternParser mpp = getParser(pattern); MatchPatternParser mpp = getParser(pattern);
MatchPatternParser.TermPatternContext ctx = mpp.termPattern(); MatchPatternParser.TermPatternContext ctx = mpp.termPattern();
return matcher.accept(ctx, MatchPathFacade.createRoot(keyTerm)); return matcher.accept(ctx, MatchPathFacade.createRoot(keyTerm));
......
...@@ -3,5 +3,5 @@ description = '' ...@@ -3,5 +3,5 @@ description = ''
dependencies { dependencies {
compile project(':rt') compile project(':rt')
compile project(':keydeps') compile project(':keydeps')
compile project(':matcher') // compile project(':matcher')
} }
...@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.interpreter; ...@@ -2,7 +2,6 @@ package edu.kit.iti.formal.psdbg.interpreter;
import de.uka.ilkd.key.api.KeYApi; import de.uka.ilkd.key.api.KeYApi;
import de.uka.ilkd.key.api.ProofApi; import de.uka.ilkd.key.api.ProofApi;
import de.uka.ilkd.key.api.ScriptApi;
import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
...@@ -14,6 +13,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; ...@@ -14,6 +13,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.interpreter.funchdl.*; import edu.kit.iti.formal.psdbg.interpreter.funchdl.*;
import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher;
import edu.kit.iti.formal.psdbg.parser.Facade; import edu.kit.iti.formal.psdbg.parser.Facade;
import edu.kit.iti.formal.psdbg.parser.Visitor; import edu.kit.iti.formal.psdbg.parser.Visitor;
import edu.kit.iti.formal.psdbg.parser.ast.CallStatement; import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
......
...@@ -13,6 +13,7 @@ import de.uka.ilkd.key.speclang.Contract; ...@@ -13,6 +13,7 @@ import de.uka.ilkd.key.speclang.Contract;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import javafx.beans.binding.BooleanBinding; import javafx.beans.binding.BooleanBinding;
import javafx.beans.property.SimpleBooleanProperty;
import javafx.beans.property.SimpleObjectProperty; import javafx.beans.property.SimpleObjectProperty;
import javafx.concurrent.Task; import javafx.concurrent.Task;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
...@@ -33,6 +34,19 @@ import java.util.stream.Collectors; ...@@ -33,6 +34,19 @@ import java.util.stream.Collectors;
public class KeYProofFacade { public class KeYProofFacade {
private static final Logger LOGGER = LogManager.getLogger(KeYProofFacade.class); private static final Logger LOGGER = LogManager.getLogger(KeYProofFacade.class);
public boolean isLoading() {
return loading.get();
}
public SimpleBooleanProperty loadingProperty() {
return loading;
}
public void setLoading(boolean loading) {
this.loading.set(loading);
}
private SimpleBooleanProperty loading = new SimpleBooleanProperty(false);
/** /**
* Current Proof * Current Proof
*/ */
...@@ -87,6 +101,7 @@ public class KeYProofFacade { ...@@ -87,6 +101,7 @@ public class KeYProofFacade {
Task<ProofApi> task = new Task<ProofApi>() { Task<ProofApi> task = new Task<ProofApi>() {
@Override @Override
protected ProofApi call() throws Exception { protected ProofApi call() throws Exception {
setLoading(true);
ProofApi pa = loadKeyFile(keYFile); ProofApi pa = loadKeyFile(keYFile);
return pa; return pa;
} }
...@@ -97,6 +112,7 @@ public class KeYProofFacade { ...@@ -97,6 +112,7 @@ public class KeYProofFacade {
environment.set(getValue().getEnv()); environment.set(getValue().getEnv());
proof.set(getValue().getProof()); proof.set(getValue().getProof());
contract.set(null); contract.set(null);
setLoading(false);
} }
}; };
...@@ -111,16 +127,20 @@ public class KeYProofFacade { ...@@ -111,16 +127,20 @@ public class KeYProofFacade {
* @throws ProblemLoaderException * @throws ProblemLoaderException
*/ */
ProofApi loadKeyFile(File keYFile) throws ProblemLoaderException { ProofApi loadKeyFile(File keYFile) throws ProblemLoaderException {
setLoading(true);
ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile); ProofManagementApi pma = KeYApi.loadFromKeyFile(keYFile);
ProofApi pa = pma.getLoadedProof(); ProofApi pa = pma.getLoadedProof();
setLoading(false);
return pa; return pa;
} }
public ProofApi loadKeyFileSync(File keyFile) throws ProblemLoaderException { public ProofApi loadKeyFileSync(File keyFile) throws ProblemLoaderException {
setLoading(true);
ProofApi pa = loadKeyFile(keyFile); ProofApi pa = loadKeyFile(keyFile);
environment.set(pa.getEnv()); environment.set(pa.getEnv());
proof.set(pa.getProof()); proof.set(pa.getProof());
contract.set(null); contract.set(null);
setLoading(false);
return pa; return pa;
} }
......
...@@ -99,7 +99,6 @@ public class KeyInterpreter extends Interpreter<KeyData> { ...@@ -99,7 +99,6 @@ public class KeyInterpreter extends Interpreter<KeyData> {
logger.debug(String.format("Beginning of suspicion execution of %s", statements)); logger.debug(String.format("Beginning of suspicion execution of %s", statements));
GoalNode<KeyData> goalNode = getSelectedNode(); GoalNode<KeyData> goalNode = getSelectedNode();
pushState(new State<>(goalNode.deepCopy())); // copy for later prove pushState(new State<>(goalNode.deepCopy())); // copy for later prove
List<Visitor> backupExitListener = getExitListeners(), List<Visitor> backupExitListener = getExitListeners(),
backupEntryListener = getEntryListeners(); backupEntryListener = getEntryListeners();
try { try {
......
...@@ -89,7 +89,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> { ...@@ -89,7 +89,7 @@ public class ProofScriptCommandBuilder implements CommandHandler<KeyData> {
Iterator<Node> nodeIterator = start.leavesIterator(); Iterator<Node> nodeIterator = start.leavesIterator();
while (nodeIterator.hasNext()) { while (nodeIterator.hasNext()) {
Node n = nodeIterator.next(); Node n = nodeIterator.next();
LOGGER.error(n.isClosed()); LOGGER.error("Node "+ n.serialNr()+" was closed "+ n.isClosed());
} }
} else { } else {
......
package edu.kit.iti.formal.psdbg.interpreter.functions; package edu.kit.iti.formal.psdbg.interpreter.functions;
import edu.kit.iti.formal.psdbg.interpreter.Evaluator; import edu.kit.iti.formal.psdbg.interpreter.Evaluator;
import edu.kit.iti.formal.psdbg.interpreter.KeYMatcher; import edu.kit.iti.formal.psdbg.interpreter.matcher.KeYMatcher;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment; import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException; import edu.kit.iti.formal.psdbg.parser.NotWelldefinedException;
......
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import java.lang.annotation.Retention;
import java.lang.annotation.RetentionPolicy;
@Retention(RetentionPolicy.RUNTIME)
public @interface DispatchOn {
Class<?> value();
}
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import java.util.*;
@Deprecated
public class EmptyMatch implements Matchings {
public static EmptyMatch INSTANCE = new EmptyMatch();
// public static Matching EMPTY_MATCH_INSTANCE = new Matching();
private EmptyMatch() {
}
@Override
public boolean isNoMatch() {
return false;
}
@Override
public boolean isEmpty() {
return true;
}
@Override
public void add(String binder, MatchPath term) {
//throw new IllegalStateException();
}
@Override
public void add(Match singleton) {
throw new IllegalStateException();
}
@Override
public void addAll(Collection<Match> matchings) {
throw new IllegalStateException();
}
@Override
public Collection<Match> getMatchings() {
ArrayList<Match> l = new ArrayList<Match>();
l.add(new Match());
return l;
}
@Override
public Matchings reduceConform(Matchings other) {
return other;
}
@Override
public String toString() {
return "{{}}";
}
}
package edu.kit.iti.formal.psdbg.interpreter; package edu.kit.iti.formal.psdbg.interpreter.matcher;
import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.Name; import de.uka.ilkd.key.logic.Name;
import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.LogicVariable;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.logic.op.SchemaVariable;
import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.pp.LogicPrinter;
import de.uka.ilkd.key.proof.ApplyStrategy; import de.uka.ilkd.key.proof.ApplyStrategy;
...@@ -12,6 +14,7 @@ import de.uka.ilkd.key.proof.init.Profile; ...@@ -12,6 +14,7 @@ import de.uka.ilkd.key.proof.init.Profile;
import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.NoPosTacletApp;
import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.Taclet;
import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.TacletApp;
import edu.kit.iti.formal.psdbg.interpreter.MatcherApi;
import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode; import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
import edu.kit.iti.formal.psdbg.interpreter.data.KeyData; import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
import edu.kit.iti.formal.psdbg.interpreter.data.SortType; import edu.kit.iti.formal.psdbg.interpreter.data.SortType;
...@@ -20,9 +23,6 @@ import edu.kit.iti.formal.psdbg.parser.ast.Signature; ...@@ -20,9 +23,6 @@ import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import edu.kit.iti.formal.psdbg.parser.data.Value; import edu.kit.iti.formal.psdbg.parser.data.Value;
import edu.kit.iti.formal.psdbg.parser.types.SimpleType; import edu.kit.iti.formal.psdbg.parser.types.SimpleType;
import edu.kit.iti.formal.psdbg.parser.types.TermType; import edu.kit.iti.formal.psdbg.parser.types.TermType;
import edu.kit.iti.formal.psdbg.termmatcher.MatcherFacade;
import edu.kit.iti.formal.psdbg.termmatcher.Matchings;
import edu.kit.iti.formal.psdbg.termmatcher.mp.MatchPath;
import lombok.Getter; import lombok.Getter;
import org.apache.logging.log4j.LogManager; import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger; import org.apache.logging.log4j.Logger;
...@@ -170,25 +170,24 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -170,25 +170,24 @@ public class KeYMatcher implements MatcherApi<KeyData> {
} }
@Override @Override
public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, public List<VariableAssignment> matchSeq(GoalNode<KeyData> currentState, String pattern, Signature sig) {
String data, KeyMatcherFacade kmf = new KeyMatcherFacade(currentState.getData().getEnv(), currentState.getData().getNode().sequent());
Signature sig) { //System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + pattern);
//System.out.println("State that will be matched " + currentState.getData().getNode().sequent() + " with pattern " + data);
//System.out.println("Signature " + sig.toString()); //System.out.println("Signature " + sig.toString());
Matchings m = kmf.matches(pattern, sig);
Matchings m = MatcherFacade.matches(data, if (m.isNoMatch()) {
currentState.getData().getNode().sequent(), false, currentState.getData().getProof().getServices());
if (m.isEmpty()) {
LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent()); LOGGER.debug("currentState has no match= " + currentState.getData().getNode().sequent());
return Collections.emptyList(); return Collections.emptyList();
} else { } else {
Map<String, MatchPath> firstMatch = m.first(); Match firstMatch = m.getMatchings().iterator().next() ;
VariableAssignment va = new VariableAssignment(null); VariableAssignment va = new VariableAssignment(null);
for (String s : firstMatch.keySet()) { for (String s : firstMatch.keySet()) {
MatchPath matchPath = firstMatch.get(s); MatchPath matchPath = firstMatch.get(s);
if (!s.equals("EMPTY_MATCH")) { //if (!s.equals("EMPTY_MATCH")) {
Term matched = (Term) matchPath.getUnit(); Term matched;
try {
matched = (Term) matchPath.getUnit();
if (s.startsWith("?")) { if (s.startsWith("?")) {
s = s.replaceFirst("\\?", ""); s = s.replaceFirst("\\?", "");
...@@ -197,8 +196,23 @@ public class KeYMatcher implements MatcherApi<KeyData> { ...@@ -197,8 +196,23 @@ public class KeYMatcher implements MatcherApi<KeyData> {
Value<String> value = toValueTerm(currentState.getData(), matched); Value<String> value = toValueTerm(currentState.getData(), matched);
va.declare(s, value.getType()); va.declare(s, value.getType());
va.assign(s, value); va.assign(s, value);
//LOGGER.info("Variables to match " + s + " : " + value);
} catch (ClassCastException e){
LogicVariable var = (LogicVariable) matchPath.getUnit();
String reprTerm = var.name().toString();
Value<String> value = new Value<>(
new TermType(new SortType(var.sort())),
reprTerm);
if (s.startsWith("?")) {
s = s.replaceFirst("\\?", "");
}
va.declare(s, value.getType());
va.assign(s, value);
} }
//LOGGER.info("Variables to match " + s + " : " + value);
//}
} }
List<VariableAssignment> retList = new LinkedList(); List<VariableAssignment> retList = new LinkedList();
LOGGER.info("Matched Variables " + va.toString()); LOGGER.info("Matched Variables " + va.toString());
......
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import de.uka.ilkd.key.control.KeYEnvironment;
import de.uka.ilkd.key.java.Services;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.AbstractSortedOperator;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import de.uka.ilkd.key.logic.sort.Sort;
import de.uka.ilkd.key.macros.scripts.ScriptException;
import de.uka.ilkd.key.parser.DefaultTermParser;
import de.uka.ilkd.key.parser.ParserException;
import edu.kit.iti.formal.psdbg.parser.ast.Operator;
import edu.kit.iti.formal.psdbg.parser.ast.Signature;
import lombok.Builder;
import org.apache.logging.log4j.LogManager;
import org.apache.logging.log4j.Logger;
import org.key_project.util.collection.ImmutableArray;
import java.io.Reader;
import java.io.StringReader;
import java.util.ArrayList;
import java.util.List;
import java.util.function.Function;
@Builder
public class KeyMatcherFacade {
private static Logger logger = LogManager.getLogger(KeyMatcherFacade.class);
private final DefaultTermParser dtp = new DefaultTermParser();
private final KeYEnvironment environment;
private final Sequent sequent;
public Matchings matches(String pattern, Signature sig) {
if(pattern.contains("==>")) {
return matchesSequent(pattern, sig);
} else {
return matchesTerm(pattern, sig);
}
}
private Matchings matchesTerm(String pattern, Signature sig) {
List<Term> positions = new ArrayList<>();
for (String patternTerm : hasToplevelComma(pattern)) {
try {
Term t = dtp.parse(createReader(patternTerm), null, environment.getServices(), environment.getServices().getNamespaces(), null, true);
positions.add(t);
} catch (ParserException e) {
e.printStackTrace();
}
}
KeyTermMatcher keyTermMatcher = new KeyTermMatcher();
return keyTermMatcher.matchesToplevel(sequent, positions);
}
static List<String> hasToplevelComma(String pattern) {
ArrayList<String> rt = new ArrayList<>();
char[] c = pattern.toCharArray();
int level = 0;
int lastPosition = 0;
for (int i = 0; i < c.length; i++) {
if(c[i]==',' && level==0){
rt.add(pattern.substring(lastPosition, i));
lastPosition=i;
}
if(c[i]=='(' || c[i]=='{')
level++;
if(c[i]==')' || c[i]=='}')
level--;
}
if(rt.isEmpty())
rt.add(pattern);
return rt;
}
private Matchings matchesSequent(String pattern, Signature sig) {
Sequent seq = null;
try {
seq = dtp.parseSeq(createReader(pattern), environment.getServices(), environment.getServices().getNamespaces(), null,true);
} catch (ParserException e) {
e.printStackTrace();
}
KeyTermMatcher keyTermMatcher = new KeyTermMatcher();
return keyTermMatcher.matchesSequent(sequent, seq);
}
private Reader createReader(String pattern) {
StringReader sr = new StringReader(pattern);
return sr;
}
}
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import de.uka.ilkd.key.logic.Term;
import de.uka.ilkd.key.logic.op.Operator;
import de.uka.ilkd.key.logic.op.SchemaVariable;
import javax.xml.validation.Schema;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.HashMap;
import java.util.Map;
public abstract class KeyTermBaseVisitor<T,S> {
private Map<Class<?>, TermAcceptor<T,S>> dispatchMap = new HashMap<>();
public KeyTermBaseVisitor() {
populateMap();
}
protected void populateMap() {
Class me = getClass();
for (Method m: me.getMethods()) {
DispatchOn anno = m.getAnnotation(DispatchOn.class);
if(anno!=null){
dispatchMap.put(anno.value(),
(term,arg) -> (T) m.invoke(this, term,arg));
}
}
}
public T visit(Term term, S arg) {
Class<? extends Operator> opClazz = term.op().getClass();
T ret;
if(!dispatchMap.containsKey(opClazz)) {
ret = defaultVisit(term, arg);
}else {
try {
ret = dispatchMap.get(opClazz).visit(term, arg);
} catch (InvocationTargetException | IllegalAccessException e) {
throw new RuntimeException(e);
}
}
// System.out.format(" match: %s :: %s :: %s%n", term, arg, ret);
return ret;
}
protected T defaultVisit(Term term, S arg) {
throw new RuntimeException("Visiting of " +term.getClass() + " not handled by visitor: "
+ getClass().getSimpleName());
}
interface TermAcceptor<T, S> {
T visit(Term term, S arg) throws InvocationTargetException, IllegalAccessException;
}
}
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import java.util.TreeMap;
public class Match extends TreeMap<String, MatchPath> {
public Match() {
}
public Match(Match h1) {
super(h1);
}
public static Match singleton(String binder, MatchPath path) {
Match m = new Match();
m.put(binder, path);
return m;
}
public static Match empty() {
Match m = new Match();
return m;
}
}
package edu.kit.iti.formal.psdbg.interpreter.matcher;
import de.uka.ilkd.key.logic.*;
import de.uka.ilkd.key.logic.op.QuantifiableVariable;
import lombok.Data;
import lombok.EqualsAndHashCode;
/**
* @author Alexander Weigl
* @version 1 (24.08.17)
*/
@Data
@EqualsAndHashCode(of = {"unit"})
public abstract class MatchPath<T, P> {
public static final int SEQUENT_FORMULA_ROOT = -1;
public static final int POSITION_ANTECEDENT = -2;
public static final int POSITION_SUCCEDENT = -3;
private final MatchPath<? extends P, ?> parent;
private final T unit;
private final int posInParent;
private MatchPath(MatchPath<? extends P, ?> parent, T unit, int pos) {
posInParent = pos;
this.unit = unit;
this.parent = parent;
}
public abstract PosInOccurrence pio();
public Sequent getSequent() {
if (getParent() != null)
return getParent().getSequent();
return null;
}
public SequentFormula getSequentFormula() {
if (getParent() != null)
return getParent().getSequentFormula();
return null;
}
public abstract int depth();
public String toString() {
return unit.toString();
}
public static final class MPQuantifiableVariable extends MatchPath<QuantifiableVariable, Object> {
public MPQuantifiableVariable(MatchPath<? extends Object, ?> parent, QuantifiableVariable unit, int pos) {
super(parent, unit, pos);