1 | /* This file is part of the project "Hilbert II" - 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 | } |