Commit 01ac913d authored by Sarah Grebing's avatar Sarah Grebing

interim

parent e0c77460
Pipeline #19502 failed with stages
in 4 minutes and 25 seconds
...@@ -113,7 +113,12 @@ public class ValueInjector { ...@@ -113,7 +113,12 @@ public class ValueInjector {
if (s.getTerm() != null) { if (s.getTerm() != null) {
return s.getTerm(); return s.getTerm();
} else { } else {
TermConverter converter = new TermConverter(node); NamespaceSet nss = null;
if(s.getNs() !=null) {
nss = s.getNs();
}
TermConverter converter = new TermConverter(node, nss);
Term t = converter.convert(s.getTermRepr()); Term t = converter.convert(s.getTermRepr());
s.setTerm(t); s.setTerm(t);
return t; return t;
...@@ -127,6 +132,12 @@ public class ValueInjector { ...@@ -127,6 +132,12 @@ public class ValueInjector {
private final static DefaultTermParser PARSER = new DefaultTermParser(); private final static DefaultTermParser PARSER = new DefaultTermParser();
private NamespaceSet additionalNamespace; private NamespaceSet additionalNamespace;
public TermConverter(Node node, NamespaceSet additionalNamespace) {
this.node = node;
this.additionalNamespace = additionalNamespace;
}
@Override @Override
public Term convert(String string) throws ParserException { public Term convert(String string) throws ParserException {
StringReader reader = new StringReader(string); StringReader reader = new StringReader(string);
...@@ -147,6 +158,7 @@ public class ValueInjector { ...@@ -147,6 +158,7 @@ public class ValueInjector {
} }
Term formula = PARSER.parse(reader, null, services, ns, node.proof().abbreviations()); Term formula = PARSER.parse(reader, null, services, ns, node.proof().abbreviations());
return formula; return formula;
} }
} }
...@@ -273,7 +285,6 @@ public class ValueInjector { ...@@ -273,7 +285,6 @@ public class ValueInjector {
/** /**
* Registers the given converter for the specified class. * Registers the given converter for the specified class.
* *
* @param clazz a class
* @param conv a converter for the given class * @param conv a converter for the given class
* @param <T> an arbitrary type * @param <T> an arbitrary type
*/ */
......
...@@ -37,6 +37,7 @@ public class KeyEvaluator extends Evaluator<KeyData> { ...@@ -37,6 +37,7 @@ public class KeyEvaluator extends Evaluator<KeyData> {
TermValue data = ((TermValue) term.getData()).copy(); TermValue data = ((TermValue) term.getData()).copy();
nss.getSignature().forEach((v,s) -> { nss.getSignature().forEach((v,s) -> {
Sort sort = asKeySort(s, getGoal().getData().getGoal()); Sort sort = asKeySort(s, getGoal().getData().getGoal());
QuantifiableVariable gf;
data.getNs().variables().add(new LogicVariable(new Name(v.getIdentifier()), sort)); data.getNs().variables().add(new LogicVariable(new Name(v.getIdentifier()), sort));
}); });
return new Value(term.getType(), data); return new Value(term.getType(), data);
......
...@@ -44,10 +44,15 @@ public class TermValue { ...@@ -44,10 +44,15 @@ public class TermValue {
public TermValue copy() { public TermValue copy() {
TermValue tv = new TermValue(); TermValue tv = new TermValue();
tv.keySort = keySort; tv.keySort = keySort;
tv.termRepr=termRepr; tv.termRepr=termRepr;
tv.term=term; tv.term=term;
tv.ns = ns.copy(); if(ns !=null) {
tv.ns = ns.copy();
} else {
tv.ns=new NamespaceSet();
}
return tv; return tv;
} }
} }
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