author | paulson |
Mon, 28 Aug 2006 18:18:31 +0200 | |
changeset 20423 | 593053389701 |
parent 18443 | a1d53af4c4c7 |
permissions | -rw-r--r-- |
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15688
diff
changeset
|
1 |
(* ID: $Id$ |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15688
diff
changeset
|
2 |
Author: Claire Quigley |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15688
diff
changeset
|
3 |
Copyright 2004 University of Cambridge |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15688
diff
changeset
|
4 |
*) |
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15688
diff
changeset
|
5 |
|
15642 | 6 |
(* Parsing functions *) |
7 |
||
8 |
(* Auxiliary functions *) |
|
9 |
||
15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15642
diff
changeset
|
10 |
structure Recon_Parse = |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15642
diff
changeset
|
11 |
struct |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15642
diff
changeset
|
12 |
|
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
13 |
open ReconTranslateProof; |
15642 | 14 |
|
15 |
exception NOPARSE_WORD |
|
16 |
exception NOPARSE_NUM |
|
17 |
fun to_upper s = String.translate (Char.toString o Char.toUpper) s; |
|
18 |
||
19 |
fun string2int s = |
|
16804 | 20 |
(case Int.fromString s of SOME i => i |
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
21 |
| NONE => error "string -> int failed"); |
16804 | 22 |
|
15642 | 23 |
|
24 |
(* Parser combinators *) |
|
25 |
||
26 |
exception Noparse; |
|
27 |
||
15688 | 28 |
fun (parser1 ++ parser2) input = |
15642 | 29 |
let |
30 |
val (result1, rest1) = parser1 input |
|
31 |
val (result2, rest2) = parser2 rest1 |
|
32 |
in |
|
33 |
((result1, result2), rest2) |
|
34 |
end; |
|
35 |
||
36 |
fun many parser input = |
|
37 |
let (* Tree * token list*) |
|
38 |
val (result, next) = parser input |
|
39 |
val (results, rest) = many parser next |
|
40 |
in |
|
41 |
((result::results), rest) |
|
42 |
end |
|
43 |
handle Noparse => ([], input) |
|
44 |
| NOPARSE_WORD => ([], input) |
|
45 |
| NOPARSE_NUM => ([], input); |
|
46 |
||
47 |
||
48 |
||
15688 | 49 |
fun (parser >> treatment) input = |
15642 | 50 |
let |
51 |
val (result, rest) = parser input |
|
52 |
in |
|
53 |
(treatment result, rest) |
|
54 |
end; |
|
55 |
||
15688 | 56 |
fun (parser1 || parser2) input = parser1 input |
15642 | 57 |
handle Noparse => parser2 input; |
58 |
||
59 |
infixr 8 ++; infixr 7 >>; infixr 6 ||; |
|
60 |
||
61 |
fun some p [] = raise Noparse |
|
62 |
| some p (h::t) = if p h then (h, t) else raise Noparse; |
|
63 |
||
64 |
fun a tok = some (fn item => item = tok); |
|
65 |
||
66 |
fun finished input = if input = [] then (0, input) else raise Noparse; |
|
67 |
||
68 |
||
69 |
(* Parsing the output from gandalf *) |
|
70 |
datatype token = Word of string |
|
71 |
| Number of int |
|
72 |
| Other of string |
|
73 |
||
74 |
||
75 |
exception NOCUT |
|
76 |
fun remove_prefix [] l = l |
|
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17484
diff
changeset
|
77 |
| remove_prefix (h::t) [] = error "can't remove prefix" |
15642 | 78 |
| remove_prefix (h::t) (h'::t') = remove_prefix t t' |
79 |
fun ccut t [] = raise NOCUT |
|
80 |
| ccut t s = |
|
18443 | 81 |
if is_prefix (op =) t s then ([], remove_prefix t s) else |
15642 | 82 |
let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end |
83 |
fun cut t s = |
|
84 |
let |
|
85 |
val t' = explode t |
|
86 |
val s' = explode s |
|
87 |
val (a, b) = ccut t' s' |
|
88 |
in |
|
89 |
(implode a, implode b) |
|
90 |
end |
|
91 |
||
92 |
fun cut_exists t s |
|
93 |
= let val (a, b) = cut t s in true end handle NOCUT => false |
|
94 |
||
95 |
fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end |
|
96 |
fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end |
|
97 |
||
98 |
||
15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15642
diff
changeset
|
99 |
fun kill_lines 0 = Library.I |
15642 | 100 |
| kill_lines n = kill_lines (n - 1) o snd o cut_after "\n"; |
101 |
||
16478 | 102 |
|
15642 | 103 |
fun several p = many (some p) |
16840 | 104 |
fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "") |
15642 | 105 |
|
106 |
fun lower_letter s = ("a" <= s) andalso (s <= "z") |
|
107 |
fun upper_letter s = ("A" <= s) andalso (s <= "Z") |
|
108 |
fun digit s = ("0" <= s) andalso (s <= "9") |
|
109 |
fun letter s = lower_letter s orelse upper_letter s |
|
110 |
fun alpha s = letter s orelse (s = "_") |
|
111 |
fun alphanum s = alpha s orelse digit s |
|
112 |
fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t") |
|
113 |
(* FIX this is stopping it picking up numbers *) |
|
114 |
val word = (some alpha ++ several alphanum) >> (Word o collect) |
|
115 |
val number = |
|
116 |
(some digit ++ several digit) >> (Number o string2int o collect) |
|
117 |
val other = some (K true) >> Other |
|
118 |
||
119 |
val token = (word || number || other) ++ several space >> fst |
|
120 |
val tokens = (several space ++ many token) >> snd |
|
121 |
val alltokens = (tokens ++ finished) >> fst |
|
122 |
||
123 |
(* val lex = fst ( alltokens ( (map str) explode))*) |
|
124 |
fun lex s = alltokens (explode s) |
|
125 |
||
16478 | 126 |
|
127 |
(************************************************************) |
|
128 |
||
129 |
(**************************************************) |
|
130 |
(* Code to parse SPASS proofs *) |
|
131 |
(**************************************************) |
|
132 |
||
15642 | 133 |
datatype Tree = Leaf of string |
134 |
| Branch of Tree * Tree |
|
135 |
||
136 |
||
137 |
fun number ((Number n)::rest) = (n, rest) |
|
138 |
| number _ = raise NOPARSE_NUM |
|
139 |
fun word ((Word w)::rest) = (w, rest) |
|
140 |
| word _ = raise NOPARSE_WORD |
|
141 |
||
142 |
fun other_char ( (Other p)::rest) = (p, rest) |
|
143 |
| other_char _ =raise NOPARSE_WORD |
|
144 |
||
145 |
val number_list = |
|
146 |
(number ++ many number) |
|
147 |
>> (fn (a, b) => (a::b)) |
|
148 |
||
149 |
val term_num = |
|
150 |
(number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c)) |
|
151 |
||
16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset
|
152 |
|
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset
|
153 |
val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd) |
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset
|
154 |
>> (fn (a, b) => (a::b))) |
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset
|
155 |
|
15642 | 156 |
val axiom = (a (Word "Inp")) |
157 |
>> (fn (_) => Axiom) |
|
158 |
||
159 |
||
160 |
val binary = (a (Word "Res")) ++ (a (Other ":")) |
|
161 |
++ term_num ++ (a (Other ",")) |
|
162 |
++ term_num |
|
163 |
>> (fn (_, (_, (c, (_, e)))) => Binary (c, e)) |
|
164 |
||
165 |
||
166 |
||
167 |
val factor = (a (Word "Fac")) ++ (a (Other ":")) |
|
168 |
++ term_num ++ (a (Other ",")) |
|
169 |
++ term_num |
|
170 |
>> (fn (_, (_, (c, (_, e)))) => Factor ((fst c), (snd c),(snd e))) |
|
171 |
||
172 |
val para = (a (Word "SPm")) ++ (a (Other ":")) |
|
173 |
++ term_num ++ (a (Other ",")) |
|
174 |
++ term_num |
|
175 |
>> (fn (_, (_, (c, (_, e)))) => Para (c, e)) |
|
176 |
||
16357 | 177 |
val super_l = (a (Word "SpL")) ++ (a (Other ":")) |
178 |
++ term_num ++ (a (Other ",")) |
|
179 |
++ term_num |
|
180 |
>> (fn (_, (_, (c, (_, e)))) => Super_l (c, e)) |
|
181 |
||
182 |
||
183 |
val super_r = (a (Word "SpR")) ++ (a (Other ":")) |
|
184 |
++ term_num ++ (a (Other ",")) |
|
185 |
++ term_num |
|
186 |
>> (fn (_, (_, (c, (_, e)))) => Super_r (c, e)) |
|
187 |
||
188 |
||
189 |
val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num |
|
190 |
>> (fn (_, (_, c)) => Obvious ((fst c),(snd c))) |
|
191 |
||
15642 | 192 |
val rewrite = (a (Word "Rew")) ++ (a (Other ":")) |
16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset
|
193 |
++ term_num_list |
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset
|
194 |
>> (fn (_, (_, (c))) => Rewrite (c)) |
15642 | 195 |
|
196 |
||
197 |
val mrr = (a (Word "MRR")) ++ (a (Other ":")) |
|
198 |
++ term_num ++ (a (Other ",")) |
|
199 |
++ term_num |
|
200 |
>> (fn (_, (_, (c, (_, e)))) => MRR (c, e)) |
|
201 |
||
16357 | 202 |
val ssi = (a (Word "SSi")) ++ (a (Other ":")) |
203 |
++ term_num ++ (a (Other ",")) |
|
204 |
++ term_num |
|
205 |
>> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e)) |
|
206 |
||
207 |
val unc = (a (Word "UnC")) ++ (a (Other ":")) |
|
208 |
++ term_num ++ (a (Other ",")) |
|
209 |
++ term_num |
|
210 |
>> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e)) |
|
211 |
||
212 |
||
15642 | 213 |
|
214 |
val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num |
|
215 |
>> (fn (_, (_, c)) => Obvious ((fst c),(snd c))) |
|
16357 | 216 |
|
217 |
val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num |
|
218 |
>> (fn (_, (_, c)) => EqualRes ((fst c),(snd c))) |
|
219 |
||
220 |
val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num |
|
221 |
>> (fn (_, (_, c)) => Condense ((fst c),(snd c))) |
|
222 |
||
15642 | 223 |
(* |
224 |
val hyper = a (Word "hyper") |
|
225 |
++ many ((a (Other ",") ++ number) >> snd) |
|
226 |
>> (Hyper o snd) |
|
227 |
*) |
|
228 |
(* val method = axiom ||binary || factor || para || hyper*) |
|
229 |
||
16357 | 230 |
val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con |
231 |
||
15642 | 232 |
val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num |
233 |
>> (fn (_, (_, a)) => Binary_s a) |
|
234 |
val factor_s = a (Word "factor_s") |
|
235 |
>> (fn _ => Factor_s ()) |
|
236 |
val demod_s = a (Word "demod") |
|
237 |
++ (many ((a (Other ",") ++ term_num) >> snd)) |
|
238 |
>> (fn (_, a) => Demod_s a) |
|
239 |
||
240 |
val hyper_s = a (Word "hyper_s") |
|
241 |
++ many ((a (Other ",") ++ number) >> snd) |
|
242 |
>> (Hyper_s o snd) |
|
243 |
val simp_method = binary_s || factor_s || demod_s || hyper_s |
|
244 |
val simp = a (Other ",") ++ simp_method >> snd |
|
245 |
val simps = many simp |
|
246 |
||
247 |
||
248 |
val justification = |
|
249 |
a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]") |
|
250 |
>> (fn (_,(_, (_,(b, _)))) => b) |
|
251 |
||
252 |
||
253 |
exception NOTERM |
|
254 |
||
255 |
(* FIX - should change the stars and pluses to many rather than explicit patterns *) |
|
256 |
||
16953 | 257 |
fun trim_prefix a b = |
258 |
let val n = String.size a |
|
259 |
in String.substring (b, n, (size b) - n) end; |
|
260 |
||
261 |
||
15642 | 262 |
(* FIX - add the other things later *) |
16953 | 263 |
fun remove_typeinfo x = |
264 |
if String.isPrefix ResClause.fixed_var_prefix x |
|
265 |
then trim_prefix ResClause.fixed_var_prefix x |
|
266 |
else if String.isPrefix ResClause.schematic_var_prefix x |
|
267 |
then trim_prefix ResClause.schematic_var_prefix x |
|
268 |
else if String.isPrefix ResClause.const_prefix x |
|
269 |
then trim_prefix ResClause.const_prefix x |
|
270 |
else if String.isPrefix ResClause.tfree_prefix x |
|
271 |
then "" |
|
272 |
else if String.isPrefix ResClause.tvar_prefix x |
|
273 |
then "" |
|
274 |
else if String.isPrefix ResClause.tconst_prefix x |
|
275 |
then "" |
|
276 |
else x; |
|
15642 | 277 |
|
278 |
fun term input = ( ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) => (a@b)) |
|
279 |
) input |
|
280 |
||
281 |
(* pterms are terms from the rhs of the -> in the spass proof. *) |
|
282 |
(* they should have a "~" in front of them so that they match with *) |
|
283 |
(* positive terms in the meta-clause *) |
|
284 |
(* nterm are terms from the lhs of the spass proof, and shouldn't *) |
|
285 |
(* "~"s added word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) => (a^" "^b)) *) |
|
286 |
||
287 |
and pterm input = ( |
|
288 |
peqterm >> (fn (a) => a) |
|
289 |
||
290 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+") |
|
291 |
>> (fn (a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b)) |
|
292 |
||
293 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+") |
|
294 |
>> (fn ( a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b)) |
|
295 |
||
296 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") |
|
297 |
>> (fn ( a, (_,(b, (_,(_,_))))) => ("~"^" "^(remove_typeinfo a)^" "^b)) |
|
298 |
||
299 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") |
|
300 |
>> (fn (a, (_,(b, (_,_)))) => ("~"^" "^(remove_typeinfo a)^" "^b)) |
|
301 |
||
302 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") |
|
303 |
>> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b)) |
|
304 |
||
16357 | 305 |
|| word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w)) |
306 |
||
307 |
|| word >> (fn w => "~"^" "^(remove_typeinfo w))) input |
|
15642 | 308 |
|
309 |
and nterm input = |
|
310 |
||
311 |
( |
|
312 |
neqterm >> (fn (a) => a) |
|
313 |
||
314 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+") |
|
315 |
>> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b)) |
|
316 |
||
317 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+") |
|
318 |
>> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b)) |
|
319 |
||
320 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") |
|
321 |
>> (fn ( a, (_,(b, (_,(_,_))))) => ((remove_typeinfo a)^" "^b)) |
|
322 |
||
323 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") |
|
324 |
>> (fn ( a, (_,(b, (_,_)))) => ((remove_typeinfo a)^" "^b)) |
|
325 |
||
326 |
|| word ++ a (Other "(") ++ arglist ++ a (Other ")") |
|
327 |
>> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b)) |
|
328 |
||
16357 | 329 |
|| word ++ a (Other "*") >> (fn (w,b) => (remove_typeinfo w)) |
330 |
|| word >> (fn w => (remove_typeinfo w)) |
|
331 |
) input |
|
15642 | 332 |
|
333 |
||
334 |
and peqterm input =( |
|
335 |
||
336 |
a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
337 |
++ a (Other "*") ++ a (Other "*") ++ a (Other "+") |
|
338 |
>> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b)) |
|
339 |
||
340 |
|| a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
341 |
++ a (Other "*") ++ a (Other "+") |
|
342 |
>> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b)) |
|
343 |
||
344 |
|| a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
345 |
++ a (Other "*") ++ a (Other "*") |
|
346 |
>> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b)) |
|
347 |
||
348 |
|| a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
349 |
++ a (Other "*") |
|
350 |
>> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b)) |
|
351 |
||
352 |
||
353 |
||a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
354 |
>> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input |
|
355 |
||
356 |
||
357 |
||
358 |
and neqterm input =( |
|
359 |
||
360 |
a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
361 |
++ a (Other "*") ++ a (Other "*") ++ a (Other "+") |
|
362 |
>> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b)) |
|
363 |
||
364 |
|| a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
365 |
++ a (Other "*") ++ a (Other "+") |
|
366 |
>> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b)) |
|
367 |
||
368 |
|| a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
369 |
++ a (Other "*") ++ a (Other "*") |
|
370 |
>> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b)) |
|
371 |
||
372 |
|| a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
373 |
++ a (Other "*") |
|
374 |
>> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b)) |
|
375 |
||
376 |
||
377 |
||a (Word "equal") ++ a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") |
|
378 |
>> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input |
|
379 |
||
380 |
||
381 |
||
382 |
and ptermlist input = (many pterm |
|
383 |
>> (fn (a) => (a))) input |
|
384 |
||
385 |
and ntermlist input = (many nterm |
|
386 |
>> (fn (a) => (a))) input |
|
387 |
||
388 |
(*and arglist input = ( nterm >> (fn (a) => (a)) |
|
389 |
|| nterm ++ many (a (Other ",") ++ nterm >> snd) |
|
17306 | 390 |
>> (fn (a, b) => (a^" "^(space_implode " " b)))) input*) |
15642 | 391 |
|
392 |
and arglist input = ( nterm ++ many (a (Other ",") ++ nterm >> snd) |
|
17306 | 393 |
>> (fn (a, b) => (a^" "^(space_implode " " b))) |
15642 | 394 |
|| nterm >> (fn (a) => (a)))input |
395 |
||
396 |
val clause = term |
|
397 |
||
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15789
diff
changeset
|
398 |
(* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15789
diff
changeset
|
399 |
val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15789
diff
changeset
|
400 |
a (Other "|") ++ clause ++ a (Other ".") |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15789
diff
changeset
|
401 |
>> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c))) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15789
diff
changeset
|
402 |
|
15642 | 403 |
val lines = many line |
404 |
val alllines = (lines ++ finished) >> fst |
|
405 |
||
406 |
val parse = fst o alllines |
|
407 |
||
15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15642
diff
changeset
|
408 |
end; |