diff --git a/src/main/java/jhilbert/JHilbertException.java b/src/main/java/jhilbert/JHilbertException.java index 39b5a74..17fb7c8 100644 --- a/src/main/java/jhilbert/JHilbertException.java +++ b/src/main/java/jhilbert/JHilbertException.java @@ -52,4 +52,19 @@ public JHilbertException(final String message, final Throwable cause) { super(message, cause); } + public boolean messageMatches(String expectedError) { + if (expectedError.equals(getMessage())) { + return true; + } + else if (getCause() instanceof JHilbertException) { + return ((JHilbertException) getCause()).messageMatches(expectedError); + } + else if (null != getCause()) { + return expectedError.equals(getCause().getMessage()); + } + else { + return false; + } + } + } diff --git a/src/main/java/jhilbert/Main.java b/src/main/java/jhilbert/Main.java index 2a8f573..54f8fb8 100644 --- a/src/main/java/jhilbert/Main.java +++ b/src/main/java/jhilbert/Main.java @@ -40,6 +40,7 @@ See the commit logs ("git log") for a list of individual contributions. import jhilbert.scanners.ScannerFactory; import jhilbert.scanners.TokenFeed; import jhilbert.scanners.WikiInputStream; +import jhilbert.scanners.impl.WikiStreamTokenFeed; import org.apache.log4j.BasicConfigurator; import org.apache.log4j.ConsoleAppender; @@ -186,23 +187,22 @@ public static void main(String... args) throws Exception { } private static void processWikiFile(String inputFileName) - throws IOException, ScannerException, CommandException { + throws IOException, JHilbertException { if (isInterface(inputFileName)) { logger.info("Processing interface " + inputFileName); - final Module mainInterface = DataFactory.getInstance().createModule(inputFileName); - final TokenFeed tokenFeed = ScannerFactory - .getInstance().createTokenFeed(WikiInputStream.create(inputFileName)); - CommandFactory.getInstance().processCommands(mainInterface, tokenFeed); + WikiInputStream wiki = WikiInputStream.create(inputFileName); + final Module mainInterface = DataFactory.getInstance(). + createInterface(inputFileName); + process(wiki, mainInterface); logger.info("File processed successfully"); } else if (isProofModule(inputFileName)) { logger.info("Processing proof module " + inputFileName); - final Module mainModule = DataFactory.getInstance().createModule(""); - final TokenFeed tokenFeed = ScannerFactory - .getInstance().createTokenFeed(WikiInputStream.create(inputFileName)); - CommandFactory.getInstance().processCommands(mainModule, tokenFeed); + WikiInputStream wiki = WikiInputStream.create(inputFileName); + final Module mainModule = DataFactory.getInstance().createProofModule(); + process(wiki, mainModule); logger.info("File processed successfully"); } else { @@ -211,6 +211,37 @@ else if (isProofModule(inputFileName)) { } } + static void process(WikiInputStream wiki, final Module module) + throws JHilbertException { + String expectedError; + if (wiki.expectedErrors().size() > 1) { + throw new JHilbertException("can only expect one error per file currently"); + } + else if (wiki.expectedErrors().size() == 1) { + expectedError = wiki.expectedErrors().get(0); + } + else { + expectedError = null; + } + + final WikiStreamTokenFeed tokenFeed = new WikiStreamTokenFeed(wiki); + try { + CommandFactory.getInstance().processCommands(module, tokenFeed); + } + catch (JHilbertException e) { + if (expectedError != null) { + if (!e.messageMatches(expectedError) + && !tokenFeed.hasRejection(expectedError)) { + throw new JHilbertException("expected error:\n " + expectedError + + "\nbut got:\n " + e.getMessage()); + } + } + else { + throw e; + } + } + } + public static boolean isProofModule(String fileName) { return fileName.contains("Main/") || fileName.contains("User module/"); @@ -224,7 +255,7 @@ public static boolean isInterface(String fileName) { private static void processProofModule(String inputFileName) throws ScannerException, FileNotFoundException, CommandException { logger.info("Processing file " + inputFileName); - final Module mainModule = DataFactory.getInstance().createModule(""); + final Module mainModule = DataFactory.getInstance().createProofModule(); final TokenFeed tokenFeed = ScannerFactory .getInstance().createTokenFeed(new FileInputStream(inputFileName)); CommandFactory.getInstance().processCommands(mainModule, tokenFeed); diff --git a/src/main/java/jhilbert/data/DataFactory.java b/src/main/java/jhilbert/data/DataFactory.java index e3f11af..5e44dba 100644 --- a/src/main/java/jhilbert/data/DataFactory.java +++ b/src/main/java/jhilbert/data/DataFactory.java @@ -64,6 +64,17 @@ public final Module createModule(String name) { } } + public final Module createProofModule() { + return createModule(""); + } + + public final Module createInterface(String name) { + if (name == null || "".equals(name)) { + throw new IllegalArgumentException("must give a name to an interface"); + } + return createModule(name); + } + /** * Creates a new {@link Module} with the specified name and revision * number. diff --git a/src/main/java/jhilbert/data/impl/NamespaceImpl.java b/src/main/java/jhilbert/data/impl/NamespaceImpl.java index 7c9109b..290593d 100644 --- a/src/main/java/jhilbert/data/impl/NamespaceImpl.java +++ b/src/main/java/jhilbert/data/impl/NamespaceImpl.java @@ -118,7 +118,7 @@ public void registerObject(final Name o) throws DataException { if (registry.containsKey(name)) { logger.error("Name " + name + " already registered in this namespace"); logger.debug("Previously registered object: " + registry.get(name)); - throw new DataException("Name already registered"); + throw new DataException("Name " + name + " already registered"); } registry.put(name, obj); obj.setNamespace(this); diff --git a/src/main/java/jhilbert/data/impl/StatementImpl.java b/src/main/java/jhilbert/data/impl/StatementImpl.java index 9ea64f7..8ebdd54 100644 --- a/src/main/java/jhilbert/data/impl/StatementImpl.java +++ b/src/main/java/jhilbert/data/impl/StatementImpl.java @@ -55,6 +55,7 @@ final class StatementImpl extends SymbolImpl implements Statement, Serializable /** * Logger for this class. */ + @SuppressWarnings("unused") private static final Logger logger = Logger.getLogger(StatementImpl.class); /** diff --git a/src/main/java/jhilbert/scanners/WikiInputStream.java b/src/main/java/jhilbert/scanners/WikiInputStream.java index ae4e28c..68622f9 100644 --- a/src/main/java/jhilbert/scanners/WikiInputStream.java +++ b/src/main/java/jhilbert/scanners/WikiInputStream.java @@ -29,39 +29,107 @@ See the commit logs ("git log") for a list of individual contributions. import java.io.FileInputStream; import java.io.IOException; import java.io.InputStream; +import java.io.StringWriter; +import java.io.Writer; +import java.util.ArrayList; +import java.util.List; import java.util.regex.Matcher; import java.util.regex.Pattern; public class WikiInputStream extends InputStream { - // This class contains only static methods + private InputStream delegate; + private Writer buffer; + private String contents; + private ArrayList expectedErrors; + private WikiInputStream() { + this.buffer = new StringWriter(); + expectedErrors = new ArrayList(); + } + + private void finishWriting() throws IOException { + buffer.flush(); + contents = buffer.toString(); + delegate = new ByteArrayInputStream(contents.getBytes("UTF-8")); + buffer = null; + } + + private String getContents() { + return contents; } @Override public int read() throws IOException { - throw new RuntimeException("This class contains only static methods"); + return delegate.read(); + } + + @Override + public void close() throws IOException { + delegate.close(); + } + + @Override + public int read(byte[] arg0, int arg1, int arg2) throws IOException { + return delegate.read(arg0, arg1, arg2); } - public static InputStream create(String inputFileName) throws IOException { + @Override + public int read(byte[] b) throws IOException { + return delegate.read(b); + } + + public static WikiInputStream create(String inputFileName) throws IOException { return create(new FileInputStream(inputFileName)); } - public static InputStream create(InputStream inputStream) throws IOException { - return new ByteArrayInputStream(read(inputStream).getBytes("UTF-8")); + public static WikiInputStream create(InputStream inputStream) throws IOException { + WikiInputStream wiki = new WikiInputStream(); + wiki.readWikiText(inputStream); + wiki.finishWriting(); + return wiki; } - static String read(InputStream inputStream) throws IOException { - Pattern PATTERN = Pattern.compile(".*?", Pattern.DOTALL); - CharSequence contents = readFile(inputStream); - final StringBuilder jhText = new StringBuilder(); - final Matcher matcher = PATTERN.matcher(contents); + private void readWikiText(InputStream input) throws IOException { + Pattern START_OR_END = Pattern.compile("(|)"); + CharSequence contents = readFile(input); + final Matcher matcher = START_OR_END.matcher(contents); + int startTag = -1; + int startOfNonJh = 0; while(matcher.find()) { - final String match = matcher.group(); - jhText.append('\n'); - jhText.append(match, 4, match.length() - 5); // strip tags + final int matchStart = matcher.start(); + final int matchEnd = matcher.end(); + final CharSequence matched = contents.subSequence(matchStart, matchEnd); + if ("".equals(matched)) { + if (startTag != -1) { + throw new RuntimeException( + "Found tag inside tag" + ); + } + startTag = matchStart + matched.length(); + findExpectedErrors(contents.subSequence(startOfNonJh, matchStart)); + } + else { + if (startTag == -1) { + throw new RuntimeException( + "Found tag without matching tag"); + } + buffer.append('\n'); + buffer.append(contents.subSequence(startTag, matchStart)); + startTag = -1; + startOfNonJh = matchStart + matched.length(); + } } - return jhText.toString(); + if (startTag != -1) { + throw new RuntimeException( + "Missing tag" + ); + } + findExpectedErrors(contents.subSequence(startOfNonJh, contents.length())); + } + + static String read(String input) throws IOException { + return create(new ByteArrayInputStream(input.getBytes("UTF-8"))).getContents(); } private static CharSequence readFile(InputStream inputStream) throws IOException { @@ -74,4 +142,17 @@ private static CharSequence readFile(InputStream inputStream) throws IOException return contents.toString("UTF-8"); } + private void findExpectedErrors(CharSequence wikiText) { + Pattern EXPECTED_ERRORS = Pattern.compile( + "\\{\\{\\s*error expected\\s*[|]\\s*([^|}]+)\\s*\\}\\}"); + Matcher matcher = EXPECTED_ERRORS.matcher(wikiText); + while (matcher.find()) { + expectedErrors.add(matcher.group(1)); + } + } + + public List expectedErrors() { + return expectedErrors; + } + } diff --git a/src/main/java/jhilbert/scanners/impl/StreamTokenFeed.java b/src/main/java/jhilbert/scanners/impl/StreamTokenFeed.java index 3786547..17c1824 100644 --- a/src/main/java/jhilbert/scanners/impl/StreamTokenFeed.java +++ b/src/main/java/jhilbert/scanners/impl/StreamTokenFeed.java @@ -34,7 +34,7 @@ See the commit logs ("git log") for a list of individual contributions. /** * A token feed for stream I/O. */ -final class StreamTokenFeed extends AbstractTokenFeed { +class StreamTokenFeed extends AbstractTokenFeed { /** * Logger for this class. diff --git a/src/main/java/jhilbert/scanners/impl/WikiStreamTokenFeed.java b/src/main/java/jhilbert/scanners/impl/WikiStreamTokenFeed.java new file mode 100644 index 0000000..5fe4df6 --- /dev/null +++ b/src/main/java/jhilbert/scanners/impl/WikiStreamTokenFeed.java @@ -0,0 +1,54 @@ +/* + JHilbert, a verifier for collaborative theorem proving + + Copyright © 2008, 2009, 2011 The JHilbert Authors + See the AUTHORS file for the list of JHilbert authors. + See the commit logs ("git log") for a list of individual contributions. + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + + You may contact the author on this Wiki page: + http://www.wikiproofs.de/w/index.php?title=User_talk:GrafZahl +*/ + +package jhilbert.scanners.impl; + +import java.io.InputStream; +import java.util.ArrayList; +import java.util.List; + +import jhilbert.scanners.ScannerException; + +/** + * A token feed for stream I/O. + */ +public class WikiStreamTokenFeed extends StreamTokenFeed { + + List rejections = new ArrayList(); + + public WikiStreamTokenFeed(final InputStream in) throws ScannerException { + super(in); + } + + public @Override void reject(final String msg) { + rejections.add(msg); + super.reject(msg); + } + + public boolean hasRejection(String message) { + System.out.println(rejections); + return rejections.contains(message); + } + +} diff --git a/src/main/java/jhilbert/storage/Storage.java b/src/main/java/jhilbert/storage/Storage.java index b1c77f7..195f567 100644 --- a/src/main/java/jhilbert/storage/Storage.java +++ b/src/main/java/jhilbert/storage/Storage.java @@ -40,7 +40,7 @@ public abstract class Storage { /** * Instance. */ - private static final Storage instance; + private static Storage instance; /** * Choose instance. @@ -73,6 +73,10 @@ public static Storage getInstance() { return instance; } + public static void setInstance(Storage storage) { + instance = storage; + } + /** * Module cache. */ diff --git a/src/main/java/jhilbert/storage/hashstore/Storage.java b/src/main/java/jhilbert/storage/hashstore/Storage.java index 0013f74..a23cd25 100644 --- a/src/main/java/jhilbert/storage/hashstore/Storage.java +++ b/src/main/java/jhilbert/storage/hashstore/Storage.java @@ -73,6 +73,7 @@ public final class Storage extends jhilbert.storage.Storage { /** * Digest charset. */ + @SuppressWarnings("unused") private static final Charset HASHER_CHARSET = Charset.forName("UTF-8"); /** diff --git a/src/main/java/jhilbert/storage/mediawiki/Storage.java b/src/main/java/jhilbert/storage/mediawiki/Storage.java index a546e58..9fdd670 100644 --- a/src/main/java/jhilbert/storage/mediawiki/Storage.java +++ b/src/main/java/jhilbert/storage/mediawiki/Storage.java @@ -140,7 +140,6 @@ private RevisionHandler handleRequest(final String req) throws StorageException assert (!"".equals(locator)): "Proof module supplied"; assert (revision >= 0): "Invalid version number supplied"; try { - final String urlEncodedLocator = URLEncoder.encode(locator, ENCODING); final RevisionHandler handler = handleRequest("revids=" + revision + "&prop=revisions&rvprop=content"); if (!locator.equals(handler.getPageTitle())) throw new StorageException("Supplied revision " + revision + " does not match supplied title " + locator); diff --git a/src/main/java/jhilbert/storage/wiki/Storage.java b/src/main/java/jhilbert/storage/wiki/Storage.java index c11bc50..cebdc90 100644 --- a/src/main/java/jhilbert/storage/wiki/Storage.java +++ b/src/main/java/jhilbert/storage/wiki/Storage.java @@ -119,6 +119,8 @@ public final class Storage extends jhilbert.storage.Storage { */ public static String fileName(String jhilbertName) { String[] parts = jhilbertName.split(":"); + if (parts.length != 2) + throw new RuntimeException("Filename must contain exactly one colon: " + jhilbertName); String namespace = parts[0]; String underscoredName = parts[1]; diff --git a/src/test/java/jhilbert/AppTest.java b/src/test/java/jhilbert/AppTest.java index fac53f7..35ed5f1 100644 --- a/src/test/java/jhilbert/AppTest.java +++ b/src/test/java/jhilbert/AppTest.java @@ -129,16 +129,22 @@ public void testDefineTerm() throws Exception { } public void testAbbreviation() throws Exception { - Kind formula = dataFactory.createKind("formula", mainModule.getKindNamespace()); - dataFactory.createFunctor("!", formula, Arrays.asList(formula), mainModule.getFunctorNamespace()); + Kind formula = dataFactory.createKind("formula", mainModule.getKindNamespace()); + dataFactory.createFunctor("!", formula, Arrays.asList(formula), mainModule.getFunctorNamespace()); dataFactory.createFunctor("->", formula, Arrays.asList(formula, formula), mainModule.getFunctorNamespace()); process("var (formula p q)"); - process("def ((| p q) ((! p) -> q))"); + process("def ((| p q) ((! p) -> q))"); - Definition or = (Definition) mainModule.getFunctorNamespace().getObjectByString("|"); - assertEquals("|", or.getNameString()); - assertEquals("(-> (! (?1)) (?0))", or.getDefiniens().toString()); + Definition or = (Definition) mainModule.getFunctorNamespace().getObjectByString("|"); + assertEquals("|", or.getNameString()); + + // The definiens is something like "(-> (! (?1)) (?0))" but the + // numbers do not seem to be completely consistent from run to run. + String definiens = or.getDefiniens().toString(); + assertTrue("unexpected definiens " + definiens, + definiens.matches( + "\\(-> \\(! \\(\\?[0-9]+\\)\\) \\(\\?[0-9]+\\)\\)")); } public void testDefineStatement() throws Exception { diff --git a/src/test/java/jhilbert/MainTest.java b/src/test/java/jhilbert/MainTest.java index 0f87bd5..6fb0c12 100644 --- a/src/test/java/jhilbert/MainTest.java +++ b/src/test/java/jhilbert/MainTest.java @@ -24,6 +24,15 @@ See the commit logs ("git log") for a list of individual contributions. package jhilbert; +import java.io.ByteArrayInputStream; +import java.io.IOException; +import java.io.UnsupportedEncodingException; + +import jhilbert.data.DataFactory; +import jhilbert.data.Module; +import jhilbert.scanners.WikiInputStream; +import jhilbert.storage.MemoryStorage; +import jhilbert.storage.Storage; import junit.framework.TestCase; import static jhilbert.Main.isInterface; import static jhilbert.Main.isProofModule; @@ -44,4 +53,113 @@ public void testIsModule() throws Exception { assertTrue(isProofModule("User module/J/o/e/Joe\u001cSandbox")); } + private void process(String wikiText) throws IOException, + UnsupportedEncodingException, JHilbertException { + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + wikiText.getBytes("UTF-8"))); + final Module interfaceModule = DataFactory.getInstance(). + createInterface("foo.jhi"); + Main.process(wiki, interfaceModule); + } + + public void testExpectNoErrorsAndGetNone() throws Exception { + process("\nkind (formula)\n\n"); + } + + public void testExpectNoErrorsAndGetOne() throws Exception { + try { + process("\nkind ness and peace\n\n"); + fail(); + } + catch (JHilbertException e) { + assertEquals(" kind ness Feed error: Expected beginning of LISP s-expression", + e.getMessage()); + } + } + + public void testExpectErrorAndGetIt() throws Exception { + process("{{error expected|Kind not found}}\n" + + "\nterm (formula (true))\n\n"); + } + + // Need to follow causes recursively, as long as they are JHilbertExceptions + public void testExpectErrorNested() throws Exception { + MemoryStorage storage = new MemoryStorage(); + storage.store("Interface:logic", + "kind (formula)" + + "var (formula p q)" + + "term (formula (→ formula formula))" + + "stmt (AntecedentIntroduction () () (p → (q → p)))" + ); + Storage.setInstance(storage); + + // Hmm, do we want + // {{error expected|Proof does not verify: Consequent does not match proof result}} + // to work too? + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + ("{{error expected|Consequent does not match proof result}}\n" + + "\n" + + "import (LOGIC Interface:logic () ())" + + "var (formula r s)\n" + + "thm (invalid () () ((r → s) → r) (\n" + + " r s AntecedentIntroduction\n" + + "))\n" + + "\n").getBytes("UTF-8"))); + final Module module = DataFactory.getInstance().createProofModule(); + Main.process(wiki, module); + } + + /* Errors have two wordings. One goes in the exception. One is passed + to reject, which is what is shown to the user (in the case of --wiki, + both are currently shown but that might be overkill). */ + public void testWordingFromReject() throws Exception { + MemoryStorage storage = new MemoryStorage(); + storage.store("Interface:logic", + "kind (formula)" + + "var (formula p q)" + + "term (formula (→ formula formula))" + + "stmt (AntecedentIntroduction () () (p → (q → p)))" + ); + Storage.setInstance(storage); + + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + ("{{error expected|Consequent of theorem does not match proof result}}\n" + + "\n" + + "import (LOGIC Interface:logic () ())" + + "var (formula r s)\n" + + "thm (invalid () () ((r → s) → r) (\n" + + " r s AntecedentIntroduction\n" + + "))\n" + + "\n").getBytes("UTF-8"))); + final Module module = DataFactory.getInstance().createProofModule(); + Main.process(wiki, module); + } + + public void testExpectErrorAndGetAnother() throws Exception { + try { + process("{{error expected|howzzzat}}\n" + + "\nterm (formula (true))\n\n"); + fail(); + } + catch (JHilbertException e) { + assertEquals("expected error:\n" + + " howzzzat\n" + + "but got:\n" + + " term ( formula Kind not found: (cause unknown)", + e.getMessage()); + } + } + + public void testExpectMultipleErrors() throws Exception { + try { + process("{{error expected|boring file}}\n" + + "{{error expected|too much in one file}}\n"); + fail(); + } + catch (JHilbertException e) { + assertEquals("can only expect one error per file currently", + e.getMessage()); + } + } + } diff --git a/src/test/java/jhilbert/scanners/WikiInputStreamTest.java b/src/test/java/jhilbert/scanners/WikiInputStreamTest.java index 534c973..2d3a533 100644 --- a/src/test/java/jhilbert/scanners/WikiInputStreamTest.java +++ b/src/test/java/jhilbert/scanners/WikiInputStreamTest.java @@ -31,13 +31,111 @@ See the commit logs ("git log") for a list of individual contributions. public class WikiInputStreamTest extends TestCase { public void testPageWithoutJh() throws Exception { - assertEquals("", WikiInputStream.read(new ByteArrayInputStream( - "This is some [[wikitext]] {{and a template}}.".getBytes("UTF-8")))); + assertEquals("", WikiInputStream.read( + "This is some [[wikitext]] {{and a template}}.")); } public void testFindJhSections() throws Exception { - assertEquals("\nvar (\nformula p)", WikiInputStream.read(new ByteArrayInputStream( - "Non-jhilbert var ( and then formula p)".getBytes("UTF-8")))); + assertEquals("\nvar (\nformula p)", WikiInputStream.read( + "Non-jhilbert var ( and then formula p)")); + } + + public void testOpenJhNoCloseJh() throws Exception { + try { + WikiInputStream.read("thm ("); + fail(); + } + catch (Exception expected) { + assertEquals("Missing tag", expected.getMessage()); + } + } + + public void testCloseJhBeforeJh() throws Exception { + try { + WikiInputStream.read(""); + fail(); + } + catch (Exception expected) { + assertEquals("Found tag without matching tag", + expected.getMessage()); + } + } + + public void testCloseJhWhenAlreadyClosed() throws Exception { + try { + WikiInputStream.read(""); + fail(); + } + catch (Exception expected) { + assertEquals("Found tag without matching tag", + expected.getMessage()); + } + } + + public void testOpenJhWhenAlreadyOpen() throws Exception { + try { + WikiInputStream.read("\n\n\n"); + fail(); + } + catch (Exception expected) { + assertEquals("Found tag inside tag", expected.getMessage()); + } + } + + public void testNoErrorsExpected() throws Exception { + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + "Hi, I'm a page.\n\n\n".getBytes("UTF-8"))); + assertEquals(0, wiki.expectedErrors().size()); + } + + public void testErrorExpectedBeforeFirstStartTag() throws Exception { + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + "{{error expected|it's broke}}\n\n\n" + .getBytes("UTF-8"))); + assertEquals(1, wiki.expectedErrors().size()); + assertEquals("it's broke", wiki.expectedErrors().get(0)); + } + + public void testTwoExpectedErrors() throws Exception { + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + ("{{error expected|it's heavy}}\n" + + "{{error expected|it's ugly}}\n") + .getBytes("UTF-8"))); + assertEquals(2, wiki.expectedErrors().size()); + assertEquals("it's heavy", wiki.expectedErrors().get(0)); + assertEquals("it's ugly", wiki.expectedErrors().get(1)); + } + + public void testErrorExpectedBetweenTags() throws Exception { + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + ("\n" + + "\n" + + "Foo. {{error expected|syntax error}}\n" + + "\n" + + "the bad syntax\n" + + "\n") + .getBytes("UTF-8"))); + assertEquals(1, wiki.expectedErrors().size()); + assertEquals("syntax error", wiki.expectedErrors().get(0)); + } + + public void testDoNotRecognizeErrorExpectedInJh() throws Exception { + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + ("\n" + + "# We would add {{error expected|foo}} if this were really bad\n" + + "\n") + .getBytes("UTF-8"))); + assertEquals(0, wiki.expectedErrors().size()); + } + + public void testErrorExpectedAfterLastCloseTag() throws Exception { + WikiInputStream wiki = WikiInputStream.create(new ByteArrayInputStream( + ("\n" + + "\n" + + "{{error expected|it's broke}}\n\n") + .getBytes("UTF-8"))); + assertEquals(1, wiki.expectedErrors().size()); + assertEquals("it's broke", wiki.expectedErrors().get(0)); } } diff --git a/src/test/java/jhilbert/storage/MemoryStorage.java b/src/test/java/jhilbert/storage/MemoryStorage.java new file mode 100644 index 0000000..f74c57e --- /dev/null +++ b/src/test/java/jhilbert/storage/MemoryStorage.java @@ -0,0 +1,120 @@ +/* + JHilbert, a verifier for collaborative theorem proving + + Copyright © 2008, 2009, 2011 The JHilbert Authors + See the AUTHORS file for the list of JHilbert authors. + See the commit logs ("git log") for a list of individual contributions. + + This program is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + This program is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with this program. If not, see . + + You may contact the author on this Wiki page: + http://www.wikiproofs.de/w/index.php?title=User_talk:GrafZahl +*/ + +package jhilbert.storage; + +import java.io.ByteArrayInputStream; +import java.io.IOException; +import java.io.InputStream; +import java.util.HashMap; +import java.util.Map; + +import jhilbert.commands.CommandException; +import jhilbert.commands.CommandFactory; +import jhilbert.data.DataException; +import jhilbert.data.DataFactory; +import jhilbert.data.Module; +import jhilbert.scanners.ScannerException; +import jhilbert.scanners.ScannerFactory; +import jhilbert.scanners.TokenFeed; + +import org.apache.log4j.Logger; + +/** + * In memory {@link Storage} implementation. This is for tests, so they can + * set up interfaces and import them without having to write files. + */ +public final class MemoryStorage extends jhilbert.storage.Storage { + + /** + * Logger for this class. + */ + private static final Logger logger = Logger.getLogger(Storage.class); + + // default constructed + + Map storedInterfaces = new HashMap(); + + public @Override boolean isVersioned() { + return false; + } + + protected @Override String getCanonicalName(final String locator) { + return locator; + } + + public void store(final String locator, final String contents) { + storedInterfaces.put(locator, contents); + } + + protected synchronized @Override Module retrieveModule(final String locator, final long revision) + throws StorageException { + assert (locator != null): "Supplied locator is null"; + assert (!"".equals(locator)): "No storage for a proof module"; + if (revision != -1) { + logger.error("Memory based storage does not support versioning"); + logger.debug("Supplied locator: " + locator); + logger.debug("Supplied version number: " + revision); + throw new StorageException("File based storage does not support versioning"); + } + Module interfaceModule; + try { + interfaceModule = DataFactory.getInstance().createInterface(locator, revision); + } catch (DataException e) { + final AssertionError err = new AssertionError("Bad revision number. This cannot happen"); + err.initCause(e); + throw err; + } + try { + final InputStream interfaceFile = new ByteArrayInputStream( + storedInterfaces.get(locator).getBytes("UTF-8")); + final TokenFeed tokenFeed = ScannerFactory.getInstance() + .createTokenFeed(interfaceFile); + CommandFactory.getInstance().processCommands(interfaceModule, tokenFeed); + } catch (ScannerException e) { + logger.error("Scanner error while scanning interface " + locator, e); + logger.debug("Scanner context: " + e.getScanner().getContextString()); + throw new StorageException("Scanner error while scanning interface", e); + } catch (CommandException e) { + logger.error("Command failed to execute while loading interface " + locator, e); + throw new StorageException("Command failed to execute while loading interface", e); + } catch (IOException e) { + throw new RuntimeException(e); + } + return interfaceModule; + } + + protected @Override void storeModule(final Module module, final String locator, long version) { + throw new UnsupportedOperationException("Storing not supported in this implementation"); + } + + protected @Override void eraseModule(final String locator, final long version) { + throw new UnsupportedOperationException("Erasing not supportted in this implementation"); + } + + protected @Override long getCurrentRevision(final String locator) { + return -1; + } + +} diff --git a/src/test/java/jhilbert/storage/wiki/StorageTest.java b/src/test/java/jhilbert/storage/wiki/StorageTest.java index 8112dff..13eaf01 100644 --- a/src/test/java/jhilbert/storage/wiki/StorageTest.java +++ b/src/test/java/jhilbert/storage/wiki/StorageTest.java @@ -50,8 +50,32 @@ public void testUserModule() throws Exception { Storage.fileName("User_module:Joe/Sandbox")); } - public void testMultibyte() throws Exception { + public void testMultibyteBoringCase() throws Exception { assertEquals("Interface/Z/e/r/Zermelo–Fra", Storage.fileName("Interface:Zermelo–Fra")); } + + public void testMultibyteInterestingCase() throws Exception { + // Haven't verified this against what mediawiki/levitation actually do. + assertEquals("Interface/ε/.20/c/ε conjecture", + Storage.fileName("Interface:ε_conjecture")); + } + +// public void testMultibyteSurrogatePairs() throws Exception { +// // Haven't verified this against what mediawiki/levitation actually do. +// assertEquals("Interface/𝔸/-/c/𝔸-completeness", +// Storage.fileName("Interface:𝔸-completeness")); +// } + + public void testNoColon() throws Exception { + try { + Storage.fileName("Interface/T/h/e/Theory One"); + fail(); + } + catch (Exception error) { + assertEquals( + "Filename must contain exactly one colon: Interface/T/h/e/Theory One", + error.getMessage()); + } + } }