001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.gui.se.pane;
017
018 import java.awt.Color;
019 import java.awt.Container;
020 import java.awt.Font;
021 import java.awt.event.ActionEvent;
022 import java.awt.event.ComponentAdapter;
023 import java.awt.event.ComponentEvent;
024 import java.awt.event.MouseAdapter;
025 import java.awt.event.MouseEvent;
026 import java.io.ByteArrayOutputStream;
027 import java.io.File;
028 import java.io.IOException;
029 import java.io.UnsupportedEncodingException;
030 import java.util.List;
031 import java.util.Stack;
032
033 import javax.swing.AbstractAction;
034 import javax.swing.JFrame;
035 import javax.swing.JMenu;
036 import javax.swing.JMenuBar;
037 import javax.swing.JMenuItem;
038 import javax.swing.JOptionPane;
039 import javax.swing.JScrollPane;
040 import javax.swing.JSplitPane;
041 import javax.swing.JViewport;
042 import javax.xml.parsers.ParserConfigurationException;
043
044 import org.qedeq.base.io.IoUtility;
045 import org.qedeq.base.io.ResourceLoaderUtility;
046 import org.qedeq.base.io.StringOutput;
047 import org.qedeq.base.io.TextInput;
048 import org.qedeq.base.io.TextOutput;
049 import org.qedeq.base.trace.Trace;
050 import org.qedeq.base.utility.StringUtility;
051 import org.qedeq.base.utility.YodaUtility;
052 import org.qedeq.gui.se.element.CPTextArea;
053 import org.qedeq.kernel.bo.KernelContext;
054 import org.qedeq.kernel.bo.module.InternalKernelServices;
055 import org.qedeq.kernel.bo.module.KernelQedeqBo;
056 import org.qedeq.kernel.bo.module.ModuleLabels;
057 import org.qedeq.kernel.bo.parser.MathParser;
058 import org.qedeq.kernel.bo.parser.ParserException;
059 import org.qedeq.kernel.bo.parser.Term;
060 import org.qedeq.kernel.bo.service.DefaultKernelQedeqBo;
061 import org.qedeq.kernel.bo.service.Element2LatexImpl;
062 import org.qedeq.kernel.bo.service.Element2Utf8Impl;
063 import org.qedeq.kernel.bo.service.unicode.Qedeq2UnicodeVisitor;
064 import org.qedeq.kernel.se.base.list.Element;
065 import org.qedeq.kernel.se.base.module.Proposition;
066 import org.qedeq.kernel.se.common.DefaultModuleAddress;
067 import org.qedeq.kernel.se.common.ModuleContext;
068 import org.qedeq.kernel.se.common.ModuleDataException;
069 import org.qedeq.kernel.se.common.SourceFileExceptionList;
070 import org.qedeq.kernel.se.dto.module.AddVo;
071 import org.qedeq.kernel.se.dto.module.ConclusionVo;
072 import org.qedeq.kernel.se.dto.module.ConditionalProofVo;
073 import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
074 import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
075 import org.qedeq.kernel.se.dto.module.FormalProofVo;
076 import org.qedeq.kernel.se.dto.module.FormulaVo;
077 import org.qedeq.kernel.se.dto.module.HypothesisVo;
078 import org.qedeq.kernel.se.dto.module.ModusPonensVo;
079 import org.qedeq.kernel.se.dto.module.NodeVo;
080 import org.qedeq.kernel.se.dto.module.PropositionVo;
081 import org.qedeq.kernel.se.dto.module.SubstPredVo;
082 import org.qedeq.kernel.se.visitor.QedeqNumbers;
083 import org.qedeq.kernel.xml.dao.Qedeq2Xml;
084 import org.qedeq.kernel.xml.handler.parser.LoadXmlOperatorListUtility;
085 import org.qedeq.kernel.xml.parser.BasicParser;
086 import org.xml.sax.SAXException;
087
088
089 /**
090 * Transform text proof into QEDEQ proof.
091 *
092 * @author Michael Meyling
093 */
094 public class ProofParserPane extends JFrame {
095
096 /** This is the default proposition id. */
097 private static final String UNKNOWN_PROPOSITION_ID = "proposition:unknown";
098
099 /** This class. */
100 private static final Class CLASS = ProofParserPane.class;
101
102 /** Source to parse. */
103 private CPTextArea source = new CPTextArea(true);
104
105 /** Parse QEDEQ result. */
106 private CPTextArea resultQedeqField = new CPTextArea(false);
107
108 /** Parse text result. */
109 private CPTextArea resultTextField = new CPTextArea(false);
110
111 /** Error messages. */
112 private CPTextArea error = new CPTextArea(false);
113
114 /** Make source scrollable. */
115 private JScrollPane sourceScroller = new JScrollPane();
116
117 /** Split between source and result. */
118 private JSplitPane splitPane1 = new JSplitPane(JSplitPane.VERTICAL_SPLIT);
119
120 /** Split between source and result right. */
121 private JSplitPane splitPane2 = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT);
122
123 /** Menu for copy and paste. */
124 private JMenuBar menu = new JMenuBar();
125
126 /** List of {@link org.qedeq.kernel.parser.Operator}s. */
127 private final List operators;
128
129 /** Error position within source file. */
130 private int errorPosition = -1;
131
132 /** Split between previous split and error pane. */
133 private JSplitPane globalPane;
134
135 /** File that contains operator definitions. */
136 private final File resourceFile;
137
138 /** Use this parser. */
139 private final MathParser parser;
140
141 /** Resulting proposition. */
142 private PropositionVo proposition;
143
144
145 public ProofParserPane(final String name, final MathParser parser, final String title,
146 final String resourceName, final String sample) throws SourceFileExceptionList {
147 // LATER mime 20080131: hard coded window, change to FormLayout
148 super(title);
149 this.parser = parser;
150 source.setText(sample);
151 final String resourceDirectoryName = "config";
152 try {
153 resourceFile = ResourceLoaderUtility.getResourceFile(
154 KernelContext.getInstance().getConfig().getBasisDirectory(), resourceDirectoryName,
155 resourceName).getCanonicalFile();
156 } catch (final IOException e) { // should not occur
157 throw new RuntimeException(e);
158 }
159 // LATER mime 20100906: change name and loading mechanism (don't use source directory for file!!!)
160 try {
161 operators = LoadXmlOperatorListUtility.getOperatorList(
162 (InternalKernelServices) YodaUtility.getFieldValue(KernelContext.getInstance(), "services"),
163 resourceFile);
164 } catch (NoSuchFieldException e) { // programming error
165 throw new RuntimeException(e);
166 }
167 setupView(name);
168 updateView();
169 }
170
171 /**
172 * Assembles the GUI components of the panel.
173 *
174 * @param name Name of transformation source.
175 */
176 private final void setupView(final String name) {
177 final Container pane = getContentPane();
178
179 source.setDragEnabled(true);
180 source.setFont(new Font("monospaced", Font.PLAIN, pane.getFont().getSize()));
181 source.setAutoscrolls(true);
182 source.setCaretPosition(0);
183 source.setEditable(true);
184 source.getCaret().setVisible(false);
185 source.setLineWrap(false);
186 source.setWrapStyleWord(true);
187 source.setFocusable(true);
188
189 resultTextField.setFont(new Font("monospaced", Font.PLAIN, pane.getFont().getSize()));
190 resultTextField.setAutoscrolls(true);
191 resultTextField.setCaretPosition(0);
192 resultTextField.setEditable(false);
193 resultTextField.getCaret().setVisible(false);
194 resultTextField.setFocusable(true);
195
196 resultQedeqField.setFont(new Font("monospaced", Font.PLAIN, pane.getFont().getSize()));
197 resultQedeqField.setAutoscrolls(true);
198 resultQedeqField.setCaretPosition(0);
199 resultQedeqField.setEditable(false);
200 resultQedeqField.getCaret().setVisible(false);
201 resultQedeqField.setFocusable(true);
202
203 error.setFont(new Font("monospaced", Font.PLAIN, pane.getFont().getSize()));
204 error.setForeground(Color.RED);
205 error.setAutoscrolls(true);
206 error.setCaretPosition(0);
207 error.setEditable(false);
208 error.getCaret().setVisible(false);
209 error.setFocusable(true);
210 error.addMouseListener(new MouseAdapter() {
211 public void mouseClicked(final MouseEvent e) {
212 updateView();
213 }
214
215 });
216
217 final JViewport qedeqPort = sourceScroller.getViewport();
218 qedeqPort.add(source);
219
220 final JScrollPane resultTextScroller = new JScrollPane();
221 final JViewport resultTextPort = resultTextScroller.getViewport();
222 resultTextPort.add(resultTextField);
223
224 final JScrollPane resultQedeqScroller = new JScrollPane();
225 final JViewport resultQedeqPort = resultQedeqScroller.getViewport();
226 resultQedeqPort.add(resultQedeqField);
227
228 final JScrollPane errorScroller = new JScrollPane();
229 final JViewport errorPort = errorScroller.getViewport();
230 errorPort.add(error);
231
232 splitPane2.setLeftComponent(sourceScroller);
233 splitPane2.setRightComponent(resultTextScroller);
234 splitPane2.setResizeWeight(0.5);
235 splitPane2.setOneTouchExpandable(true);
236
237 splitPane1.setTopComponent(splitPane2);
238 splitPane1.setBottomComponent(resultQedeqScroller);
239 splitPane1.setResizeWeight(0);
240 splitPane1.setOneTouchExpandable(true);
241
242 error.setText("");
243
244 globalPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT);
245 globalPane.setTopComponent(splitPane1);
246 globalPane.setBottomComponent(errorScroller);
247 globalPane.setResizeWeight(1);
248 globalPane.setOneTouchExpandable(true);
249
250 pane.add(globalPane);
251
252 addComponentListener(new ComponentAdapter() {
253 public void componentHidden(final ComponentEvent e) {
254 Trace.trace(CLASS, this, "componentHidden", e);
255 }
256 public void componentShown(final ComponentEvent e) {
257 Trace.trace(CLASS, this, "componentShown", e);
258 }
259 });
260
261 menu.removeAll();
262
263 /*
264 final JMenu fileMenu = new JMenu("File");
265 fileMenu.setMnemonic('F');
266 {
267 final JMenuItem transform = new JMenuItem("Load");
268 transform.setMnemonic('L');
269 transform.addActionListener(new AbstractAction() {
270 public final void actionPerformed(final ActionEvent action) {
271 }
272 });
273 fileMenu.add(transform);
274 }
275 menu.add(fileMenu);
276 setJMenuBar(menu);
277 */
278 final JMenu transformMenu = new JMenu("Transform");
279 transformMenu.setMnemonic('T');
280 {
281 final JMenuItem transform = new JMenuItem(name + " to QEDEQ");
282 transform.setMnemonic('Q');
283 transform.addActionListener(new AbstractAction() {
284 public final void actionPerformed(final ActionEvent action) {
285 try {
286 setProposition(source.getText());
287 resultQedeqField.setText(getQedeqXml(proposition));
288 resultTextField.setText(getUtf8(proposition));
289 } catch (ModuleDataException e) {
290 error.setText(error.getText() + e + "\n");
291 Trace.fatal(CLASS, this, "setupView$transform", "Problem during parsing", e);
292 }
293 updateView();
294 }
295 });
296 transformMenu.add(transform);
297 }
298 menu.add(transformMenu);
299
300 final JMenu helpMenu = new JMenu("Help");
301 helpMenu.setMnemonic('H');
302 {
303 final JMenuItem about = new JMenuItem("About");
304 about.setMnemonic('A');
305 about.addActionListener(new AbstractAction() {
306 public final void actionPerformed(final ActionEvent action) {
307 JOptionPane.showMessageDialog(ProofParserPane.this,
308 "This dialog enables to transform textual input into the QEDEQ format.\n"
309 + "The operators and their QEDEQ counterparts are defined int the file:\n"
310 + resourceFile,
311 "About", JOptionPane.INFORMATION_MESSAGE);
312 }
313 });
314 helpMenu.add(about);
315 }
316 menu.add(helpMenu);
317
318 setJMenuBar(menu);
319 setSize(1000, 800);
320 }
321
322 private Element getElement(final String text) {
323 if (text == null || text.trim().length() == 0) {
324 return null;
325 }
326 Element[] elements = new Element[0];
327 try {
328 elements = BasicParser.createElements(text);
329 } catch (final ParserConfigurationException e1) {
330 Trace.fatal(CLASS, "setupView$actionPerformed",
331 "Parser configuration error", e1);
332 return null;
333 } catch (final SAXException e1) {
334 // ignore
335 }
336 if (elements.length == 0) {
337 return null;
338 }
339 return elements[0];
340 }
341
342 /**
343 * Set line wrap.
344 *
345 * @param wrap Line wrap?
346 */
347 public void setLineWrap(final boolean wrap) {
348 source.setLineWrap(wrap);
349 }
350
351 /**
352 * Get line wrap.
353 *
354 * @return Line wrap?
355 */
356 public boolean getLineWrap() {
357 return source.getLineWrap();
358 }
359
360 /**
361 * Update from model.
362 */
363 public synchronized void updateView() {
364 final String method = "updateView()";
365 Trace.begin(CLASS, this, method);
366
367 splitPane2.setDividerLocation(0.35);
368 if (errorPosition >= 0) {
369 // reserve 3 text lines for error description
370 globalPane.setDividerLocation(globalPane.getHeight()
371 - globalPane.getDividerSize()
372 - error.getFontMetrics(error.getFont()).getHeight() * 3 - 4);
373 } else {
374 error.setText("");
375 globalPane.setDividerLocation(this.getHeight());
376 }
377 this.repaint();
378 }
379
380 private void setProposition(final String text) {
381 proposition = new PropositionVo();
382 error.setText("");
383 final StringBuffer buffer = new StringBuffer(text);
384 final TextInput input = new TextInput(buffer);
385 parser.setParameters(input, operators);
386 errorPosition = -1;
387 try {
388 proposition = new PropositionVo();
389 final FormalProofVo fp = new FormalProofVo();
390 proposition.addFormalProof(fp);
391 FormalProofLineListVo proof = new FormalProofLineListVo();
392 fp.setFormalProofLineList(proof);
393 Stack proofStack = new Stack();
394 Term term = null;
395 do {
396 final String line = input.getLine().trim();
397 if (line.toLowerCase().endsWith("hypothesis")) {
398 final ConditionalProofVo conditional = new ConditionalProofVo();
399 input.skipWhiteSpace();
400 input.read();
401 String label = input.readLetterDigitString();
402 input.skipWhiteSpace();
403 input.readString(1); // should be ")"
404 final HypothesisVo hypothesis = new HypothesisVo();
405 final FormulaVo formula = new FormulaVo();
406 term = parser.readTerm();
407 if (term != null) {
408 formula.setElement(getElement(term.getQedeqXml()));
409 }
410 hypothesis.setFormula(formula);
411 hypothesis.setLabel(label);
412 conditional.setHypothesis(hypothesis);
413 proof.add(conditional);
414 proofStack.push(proof);
415 proofStack.push(conditional);
416 proof = new FormalProofLineListVo();
417 conditional.setFormalProofLineList(proof);
418 input.skipToEndOfLine();
419 } else if (line.toLowerCase().endsWith("conclusion")) {
420 input.skipWhiteSpace();
421 input.read();
422 String label = input.readLetterDigitString();
423 input.skipWhiteSpace();
424 input.readString(1); // should be ")"
425 final ConclusionVo conclusion = new ConclusionVo();
426 final FormulaVo formula = new FormulaVo();
427 term = parser.readTerm();
428 if (term != null) {
429 formula.setElement(getElement(term.getQedeqXml()));
430 }
431 conclusion.setFormula(formula);
432 conclusion.setLabel(label);
433 final ConditionalProofVo conditional = (ConditionalProofVo) proofStack.pop();
434 conditional.setConclusion(conclusion);
435 proof = (FormalProofLineListVo) proofStack.pop();
436 input.skipToEndOfLine();
437 } else if (line.startsWith("(") && Character.isDigit(line.charAt(1))) {
438 // we assume a common proof line
439 input.skipWhiteSpace();
440 input.read();
441 final String label = input.readLetterDigitString();
442 input.skipWhiteSpace();
443 input.readString(1); // should be ")"
444 final FormalProofLineVo l = new FormalProofLineVo();
445 final FormulaVo formula = new FormulaVo();
446 term = parser.readTerm();
447 if (term != null) {
448 formula.setElement(getElement(term.getQedeqXml()));
449 }
450 l.setFormula(formula);
451 l.setLabel(label);
452 // remember position
453 final int mark = input.getPosition();
454 String reason = "";
455 try {
456 reason = input.readStringTilWhitespace().toLowerCase();
457 } catch (RuntimeException e) {
458 // ignore
459 }
460 System.out.println("reason = " + reason);
461 if ("add".equals(reason)) {
462 final AddVo add = new AddVo();
463 add.setReference(input.readStringTilWhitespace());
464 l.setReason(add);
465 } else if ("mp".equals(reason)) {
466 final ModusPonensVo mp = new ModusPonensVo();
467 String ref1 = input.readStringTilWhitespace();
468 String ref2 = "";
469 if (ref1.endsWith(",")) {
470 ref1 = ref1.substring(0, ref1.length() - 1);
471 } else {
472 if (ref1.indexOf(",") >= 0) {
473 ref2 = ref1.substring(ref1.indexOf(",") + 1);
474 ref1 = ref1.substring(0, ref1.indexOf(","));
475 }
476 }
477 mp.setReference1(ref1);
478 if (ref2.length() == 0) {
479 ref2 = input.readStringTilWhitespace();
480 }
481 mp.setReference2(ref2);
482 l.setReason(mp);
483 } else if ("subpred".equals(reason)) {
484 final SubstPredVo subpred = new SubstPredVo();
485 term = parser.readTerm();
486 if (term != null) {
487 subpred.setPredicateVariable(getElement(term.getQedeqXml()));
488 }
489 term = parser.readTerm();
490 if (term != null) {
491 subpred.setSubstituteFormula(getElement(term.getQedeqXml()));
492 }
493 subpred.setReference(input.readStringTilWhitespace());
494 l.setReason(subpred);
495 input.setPosition(mark);
496 } else {
497 // spool back
498 input.setPosition(mark);
499 }
500 proof.add(l);
501 input.skipToEndOfLine();
502 } else {
503 final FormulaVo formula = new FormulaVo();
504 term = parser.readTerm();
505 if (term != null) {
506 formula.setElement(getElement(term.getQedeqXml()));
507 proposition.setFormula(formula);
508 }
509 input.skipToEndOfLine();
510 }
511 // term = parser.readTerm();
512 // if (term != null) {
513 // out.append(term.getQedeqXml()).append("\n");
514 // System.out.println(term.getQedeqXml());
515 // }
516 } while (!input.isEmpty() && !parser.eof());
517 } catch (ParserException e) {
518 e.printStackTrace(System.out);
519 final StringBuffer result = new StringBuffer();
520 errorPosition = input.getPosition();
521 result.append(input.getRow() + ":" + input.getColumn() + ":" + "\n");
522 result.append(e.getMessage() + "\n");
523 result.append(input.getLine().replace('\t', ' ').replace('\015', ' ') + "\n");
524 final StringBuffer pointer = StringUtility.getSpaces(input.getColumn());
525 pointer.append('^');
526 result.append(pointer);
527 System.out.println(result.toString());
528 error.setText(result.toString());
529 } catch (Exception e) {
530 e.printStackTrace(System.out);
531 final StringBuffer result = new StringBuffer();
532 errorPosition = input.getPosition();
533 result.append(input.getRow() + ":" + input.getColumn() + ":" + "\n");
534 result.append(e.getMessage() + "\n");
535 result.append(input.getLine().replace('\t', ' ').replace('\015', ' ') + "\n");
536 final StringBuffer pointer = StringUtility.getSpaces(input.getColumn());
537 pointer.append('^');
538 result.append(pointer);
539 System.out.println(result.toString());
540 error.setText(result.toString());
541 }
542 IoUtility.close(input); // to satisfy checkstyle
543 }
544
545 private String getQedeqXml(final Proposition proposition) throws ModuleDataException {
546 final KernelQedeqBo prop = new DefaultKernelQedeqBo(null, DefaultModuleAddress.MEMORY);
547 final ByteArrayOutputStream outputStream = new ByteArrayOutputStream();
548 final TextOutput output = new TextOutput("out", outputStream, "UTF-8");
549 output.pushLevel();
550 output.pushLevel();
551 output.pushLevel();
552 output.pushLevel();
553 final Qedeq2Xml visitor = new Qedeq2Xml(null, prop, output);
554 final NodeVo node = new NodeVo();
555 node.setId(UNKNOWN_PROPOSITION_ID);
556 node.setNodeType(proposition);
557 visitor.getTraverser().accept(node);
558 try {
559 return outputStream.toString("UTF-8");
560 } catch (UnsupportedEncodingException e) {
561 // should never happen
562 throw new RuntimeException(e);
563 }
564 }
565
566 private String getUtf8(final Proposition proposition) throws ModuleDataException {
567 final DefaultKernelQedeqBo prop = new DefaultKernelQedeqBo(null, DefaultModuleAddress.MEMORY);
568 prop.setLabels(new ModuleLabels());
569 final NodeVo node = new NodeVo();
570 node.setId(UNKNOWN_PROPOSITION_ID);
571 node.setNodeType(proposition);
572 prop.getLabels().addNode(new ModuleContext(DefaultModuleAddress.MEMORY), node, prop,
573 new QedeqNumbers(0, 0));
574 final StringOutput output = new StringOutput();
575 final Qedeq2UnicodeVisitor visitor = new Qedeq2UnicodeVisitor(null, prop, true, 120, false,
576 false) {
577 protected String getUtf8(final Element element) {
578 if (element == null) {
579 return "";
580 }
581 ModuleLabels labels = new ModuleLabels();
582 Element2LatexImpl converter = new Element2LatexImpl(labels);
583 Element2Utf8Impl textConverter = new Element2Utf8Impl(converter);
584 return textConverter.getUtf8(element);
585 }
586
587 protected String[] getUtf8(final Element element, final int max) {
588 if (element == null) {
589 return new String[] {""};
590 }
591 ModuleLabels labels = new ModuleLabels();
592 Element2LatexImpl converter = new Element2LatexImpl(labels);
593 Element2Utf8Impl textConverter = new Element2Utf8Impl(converter);
594 return textConverter.getUtf8(element, 0);
595 }
596
597 };
598 visitor.setParameters(output, "en");
599 visitor.getTraverser().accept(node);
600 return output.toString();
601 }
602
603 }
|