Commit ffb9d946 authored by Alexander Weigl's avatar Alexander Weigl

lookup for proofscript in directories

parent 814a7c3e
Pipeline #10643 passed with stage
in 2 minutes and 4 seconds
...@@ -180,4 +180,4 @@ NOT: 'not'; ...@@ -180,4 +180,4 @@ NOT: 'not';
DIGITS : DIGIT+ ; DIGITS : DIGIT+ ;
fragment DIGIT : [0-9] ; fragment DIGIT : [0-9] ;
ID : [a-zA-Z] [_a-zA-Z0-9]* ; ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' )* ;
\ No newline at end of file \ No newline at end of file
...@@ -73,4 +73,8 @@ public class Value<T> { ...@@ -73,4 +73,8 @@ public class Value<T> {
public String toString() { public String toString() {
return data + ":" + type; return data + ":" + type;
} }
public static Value<String> from(String s) {
return new Value<>(Type.STRING, s);
}
} }
...@@ -2,7 +2,6 @@ package edu.kit.formal.interpreter.funchdl; ...@@ -2,7 +2,6 @@ package edu.kit.formal.interpreter.funchdl;
import edu.kit.formal.interpreter.*; import edu.kit.formal.interpreter.*;
import edu.kit.formal.proofscriptparser.ast.CallStatement; import edu.kit.formal.proofscriptparser.ast.CallStatement;
import edu.kit.formal.proofscriptparser.ast.Parameters;
import lombok.Getter; import lombok.Getter;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
......
package edu.kit.formal.interpreter.funchdl;
import de.uka.ilkd.key.macros.ProofMacro;
import de.uka.ilkd.key.macros.scripts.MacroCommand;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.Value;
import edu.kit.formal.interpreter.VariableAssignment;
import edu.kit.formal.proofscriptparser.ast.CallStatement;
import edu.kit.formal.proofscriptparser.ast.Parameters;
import edu.kit.formal.proofscriptparser.ast.StringLiteral;
import edu.kit.formal.proofscriptparser.ast.Variable;
import lombok.RequiredArgsConstructor;
import java.lang.reflect.Parameter;
import java.util.Map;
/**
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
@RequiredArgsConstructor
public class MacroCommandHandler implements CommandHandler {
private final Map<String, ProofMacro> macros;
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
return macros.containsKey(call.getCommand());
}
@Override
public void evaluate(Interpreter interpreter,
CallStatement call,
VariableAssignment params) {
//ProofMacro m = macros.get(call.getCommand());
Parameters p = new Parameters();
p.put(new Variable("#2"), new StringLiteral(call.getCommand()));
CallStatement macroCall = new CallStatement("macro", p);
macroCall.setRuleContext(call.getRuleContext().get());
//macro proofscript command
interpreter.getFunctionLookup().callCommand(interpreter, call, params);
//TODO change MacroCommand.Parameters to public
}
}
package edu.kit.formal.interpreter.funchdl;
import edu.kit.formal.interpreter.Interpreter;
import edu.kit.formal.interpreter.VariableAssignment;
import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.ast.CallStatement;
import edu.kit.formal.proofscriptparser.ast.ProofScript;
import lombok.Getter;
import lombok.RequiredArgsConstructor;
import java.io.File;
import java.io.IOException;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
/**
* @author Alexander Weigl
* @version 1 (21.05.17)
*/
@RequiredArgsConstructor
public class ProofScriptHandler implements CommandHandler {
private static final String SUFFIX = ".kps";
@Getter
private final Map<String, ProofScript> scripts;
@Getter
private final List<File> searchPath = new ArrayList<>();
public ProofScriptHandler(List<ProofScript> proofScripts) {
scripts = new HashMap<>();
proofScripts.forEach(s -> scripts.put(s.getName(), s));
}
/**
* lib/test.test
*
* @param name
* @return
*/
public ProofScript find(String name) throws IOException {
File f = new File(name.replace('\\', '/'));
String path = f.getParent();
String[] filename = f.getName().split("\\.", 1);
String candidate = path + '/' + filename[0] + SUFFIX;
for (File dir : searchPath) {
File test = new File(dir, candidate);
if (test.exists()) {
addFile(path, filename[0], test);
return scripts.get(name);
}
}
return null;
}
private void addFile(String path, String filename, File test) throws IOException {
List<ProofScript> ps = Facade.getAST(test);
for (ProofScript s : ps) {
String name = s.getName();
String prefix = path.replace('/', '\\') + '\\';
if (name.equals(filename)) {
scripts.put(prefix + name, s);
}
scripts.put(prefix + filename + '.' + name, s);
}
}
@Override
public boolean handles(CallStatement call) throws IllegalArgumentException {
if (scripts.containsKey(call.getCommand()))
return true;
try {
return find(call.getCommand()) != null;
} catch (IOException e) {
e.printStackTrace();
}
return false;
}
@Override
public void evaluate(Interpreter interpreter, CallStatement call, VariableAssignment params) {
ProofScript ps = scripts.get(call.getCommand());
//TODO create new context/introduce signature
ps.accept(interpreter);
}
}
...@@ -4,6 +4,7 @@ import edu.kit.formal.ScopeLogger; ...@@ -4,6 +4,7 @@ import edu.kit.formal.ScopeLogger;
import edu.kit.formal.interpreter.funchdl.BuiltinCommands; import edu.kit.formal.interpreter.funchdl.BuiltinCommands;
import edu.kit.formal.interpreter.funchdl.CommandLookup; import edu.kit.formal.interpreter.funchdl.CommandLookup;
import edu.kit.formal.interpreter.funchdl.DefaultLookup; import edu.kit.formal.interpreter.funchdl.DefaultLookup;
import edu.kit.formal.interpreter.funchdl.ProofScriptHandler;
import edu.kit.formal.proofscriptparser.Facade; import edu.kit.formal.proofscriptparser.Facade;
import edu.kit.formal.proofscriptparser.ast.CallStatement; import edu.kit.formal.proofscriptparser.ast.CallStatement;
import edu.kit.formal.proofscriptparser.ast.ProofScript; import edu.kit.formal.proofscriptparser.ast.ProofScript;
...@@ -11,6 +12,7 @@ import org.antlr.v4.runtime.CharStreams; ...@@ -11,6 +12,7 @@ import org.antlr.v4.runtime.CharStreams;
import org.junit.Assert; import org.junit.Assert;
import org.junit.Test; import org.junit.Test;
import java.io.File;
import java.io.IOException; import java.io.IOException;
import java.io.InputStream; import java.io.InputStream;
import java.util.List; import java.util.List;
...@@ -24,19 +26,22 @@ public class InterpreterTest { ...@@ -24,19 +26,22 @@ public class InterpreterTest {
public Interpreter execute(InputStream is) throws IOException { public Interpreter execute(InputStream is) throws IOException {
List<ProofScript> scripts = Facade.getAST(CharStreams.fromStream(is)); List<ProofScript> scripts = Facade.getAST(CharStreams.fromStream(is));
Interpreter i = new Interpreter(createTestLookup()); Interpreter i = new Interpreter(createTestLookup(scripts));
i.setMatcherApi(new EvaluatorTest.PseudoMatcher()); i.setMatcherApi(new EvaluatorTest.PseudoMatcher());
//i.getEntryListeners().add(new ScopeLogger("scope:")); //i.getEntryListeners().add(new ScopeLogger("scope:"));
i.interpret(scripts, "abc"); i.interpret(scripts, "abc");
return i; return i;
} }
private CommandLookup createTestLookup() { private CommandLookup createTestLookup(List<ProofScript> scripts) {
DefaultLookup defaultLookup = new DefaultLookup(); DefaultLookup defaultLookup = new DefaultLookup();
defaultLookup.getBuilders().add(new BuiltinCommands.PrintCommand()); defaultLookup.getBuilders().add(new BuiltinCommands.PrintCommand());
defaultLookup.getBuilders().add(new BuiltinCommands.SplitCommand()); defaultLookup.getBuilders().add(new BuiltinCommands.SplitCommand());
defaultLookup.getBuilders().add(new AssertionCommand()); defaultLookup.getBuilders().add(new AssertionCommand());
defaultLookup.getBuilders().add(new AssertionEqCommand()); defaultLookup.getBuilders().add(new AssertionEqCommand());
ProofScriptHandler scriptHandler = new ProofScriptHandler(scripts);
scriptHandler.getSearchPath().add(new File("src/test/resources/edu/kit/formal/interpreter/"));
defaultLookup.getBuilders().add(scriptHandler);
return defaultLookup; return defaultLookup;
} }
...@@ -45,7 +50,12 @@ public class InterpreterTest { ...@@ -45,7 +50,12 @@ public class InterpreterTest {
public void testSimple() throws IOException { public void testSimple() throws IOException {
Interpreter i = execute(getClass().getResourceAsStream("simple1.txt")); Interpreter i = execute(getClass().getResourceAsStream("simple1.txt"));
Assert.assertEquals(10, i.getCurrentState().getGoals().size()); Assert.assertEquals(10, i.getCurrentState().getGoals().size());
}
@Test
public void testInclude() throws IOException {
Interpreter i = execute(getClass().getResourceAsStream("includetest.kps"));
} }
private class AssertionEqCommand extends BuiltinCommands.BuiltinCommand { private class AssertionEqCommand extends BuiltinCommands.BuiltinCommand {
......
script A () {
print_state;
lib\test;
lib\test.abc i=2;
}
\ No newline at end of file
script test() {
print_state;
}
script abc(i:int,j:int){j:=1;print_state;}
\ 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