View Javadoc

1   /* This file is part of the project "Hilbert II" - http://www.qedeq.org" target="alexandria_uri">http://www.qedeq.org
2    *
3    * Copyright 2000-2014,  Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10   * This program is distributed in the hope that it will be useful,
11   * but WITHOUT ANY WARRANTY; without even the implied warranty of
12   * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13   * GNU General Public License for more details.
14   */
15  
16  package org.qedeq.kernel.xml.handler.module;
17  
18  import org.qedeq.kernel.se.base.module.Reason;
19  import org.qedeq.kernel.se.dto.module.FormalProofLineListVo;
20  import org.qedeq.kernel.se.dto.module.FormalProofLineVo;
21  import org.qedeq.kernel.xml.common.XmlSyntaxException;
22  import org.qedeq.kernel.xml.handler.common.AbstractSimpleHandler;
23  import org.qedeq.kernel.xml.handler.common.SimpleAttributes;
24  
25  
26  /**
27   * Parse formal proof lines.
28   *
29   * @author  Michael Meyling
30   */
31  public class FormalProofLineListHandler extends AbstractSimpleHandler {
32  
33      /** Value object with list of all module imports. */
34      private FormalProofLineListVo list;
35  
36      /** Handler for proposition formula. */
37      private final FormulaHandler formulaHandler;
38  
39      /** Handler for Modus Ponens usage. */
40      private final ModusPonensHandler modusPonensHandler;
41  
42      /** Handler for Addition usage. */
43      private final AddHandler addHandler;
44  
45      /** Handler for Rename Subject Variable usage. */
46      private final RenameHandler renameHandler;
47  
48      /** Handler for Substitution Predicate Variable usage. */
49      private final SubstPredvarHandler substPredvarHandler;
50  
51      /** Handler for Substitution Free Variable usage. */
52      private final SubstFreevarHandler substFreevarHandler;
53  
54      /** Handler for Substitution Function Variable usage. */
55      private final SubstFuncvarHandler substFuncvarHandler;
56  
57      /** Handler for Existential Generalization usage. */
58      private final ExistentialHandler existentialHandler;
59  
60      /** Handler for Universal Generalization usage. */
61      private final UniversalHandler universalHandler;
62  
63      /** Handler for Universal Generalization usage. */
64      private final ConditionalProofHandler conditionalProofHandler;
65  
66      /** Label for a single module. */
67      private String label;
68  
69      /** Reason for proof line. */
70      private Reason reason;
71  
72  
73      /**
74       * Handles list of imports.
75       *
76       * @param   handler Parent handler.
77       */
78      public FormalProofLineListHandler(final AbstractSimpleHandler handler) {
79          super(handler, "LINES");
80          formulaHandler = new FormulaHandler(this);
81          modusPonensHandler = new ModusPonensHandler(this);
82          addHandler = new AddHandler(this);
83          substPredvarHandler = new SubstPredvarHandler(this);
84          renameHandler = new RenameHandler(this);
85          substFreevarHandler = new SubstFreevarHandler(this);
86          substFuncvarHandler = new SubstFuncvarHandler(this);
87          existentialHandler = new ExistentialHandler(this);
88          universalHandler = new UniversalHandler(this);
89          conditionalProofHandler = new ConditionalProofHandler(this);
90      }
91  
92      public final void init() {
93          list = null;
94          reason = null;
95          label = null;
96      }
97  
98      /**
99       * Get parsed result.
100      *
101      * @return  Location list.
102      */
103     public final FormalProofLineListVo getFormalProofLineList() {
104         return list;
105     }
106 
107     public final void startElement(final String name, final SimpleAttributes attributes)
108             throws XmlSyntaxException {
109         if (getStartTag().equals(name)) {
110             list = new FormalProofLineListVo();
111         } else if ("L".equals(name)) {
112             label = attributes.getString("label");
113             reason = null;
114         } else if (formulaHandler.getStartTag().equals(name)) {
115             changeHandler(formulaHandler, name, attributes);
116         } else if (modusPonensHandler.getStartTag().equals(name)) {
117             changeHandler(modusPonensHandler, name, attributes);
118         } else if (addHandler.getStartTag().equals(name)) {
119             changeHandler(addHandler, name, attributes);
120         } else if (substPredvarHandler.getStartTag().equals(name)) {
121             changeHandler(substPredvarHandler, name, attributes);
122         } else if (renameHandler.getStartTag().equals(name)) {
123             changeHandler(renameHandler, name, attributes);
124         } else if (substFreevarHandler.getStartTag().equals(name)) {
125             changeHandler(substFreevarHandler, name, attributes);
126         } else if (substFuncvarHandler.getStartTag().equals(name)) {
127             changeHandler(substFuncvarHandler, name, attributes);
128         } else if (existentialHandler.getStartTag().equals(name)) {
129             changeHandler(existentialHandler, name, attributes);
130         } else if (universalHandler.getStartTag().equals(name)) {
131             changeHandler(universalHandler, name, attributes);
132         } else if (conditionalProofHandler.getStartTag().equals(name)) {
133             changeHandler(conditionalProofHandler, name, attributes);
134         } else {
135             throw XmlSyntaxException.createUnexpectedTagException(name);
136         }
137     }
138 
139     public final void endElement(final String name) throws XmlSyntaxException {
140         if (getStartTag().equals(name)) {
141             // nothing to do
142         } else if (formulaHandler.getStartTag().equals(name)) {
143             // nothing to do
144         } else if ("L".equals(name)) {
145             list.add(new FormalProofLineVo(label, formulaHandler.getFormula(), reason));
146         } else if (modusPonensHandler.getStartTag().equals(name)) {
147             reason = modusPonensHandler.getModusPonensVo();
148         } else if (addHandler.getStartTag().equals(name)) {
149             reason = addHandler.getAddVo();
150         } else if (substPredvarHandler.getStartTag().equals(name)) {
151             reason = substPredvarHandler.getSubstPredVo();
152         } else if (renameHandler.getStartTag().equals(name)) {
153             reason = renameHandler.getRenameVo();
154         } else if (substFreevarHandler.getStartTag().equals(name)) {
155             reason = substFreevarHandler.getSubstFreeVo();
156         } else if (substFuncvarHandler.getStartTag().equals(name)) {
157             reason = substFuncvarHandler.getSubstFuncVo();
158         } else if (existentialHandler.getStartTag().equals(name)) {
159             reason = existentialHandler.getExistentialVo();
160         } else if (universalHandler.getStartTag().equals(name)) {
161             reason = universalHandler.getUniversalVo();
162         } else if (conditionalProofHandler.getStartTag().equals(name)) {
163             list.add(conditionalProofHandler.getConditionalProofVo());
164         } else {
165             throw XmlSyntaxException.createUnexpectedTagException(name);
166         }
167     }
168 }