343 (* Printing parsed TPTP formulas *) |
343 (* Printing parsed TPTP formulas *) |
344 (*FIXME this is not pretty-printing, just printing*) |
344 (*FIXME this is not pretty-printing, just printing*) |
345 |
345 |
346 fun status_to_string status_value = |
346 fun status_to_string status_value = |
347 case status_value of |
347 case status_value of |
348 Suc => "suc" | Unp => "unp" |
348 Suc => "suc" | Unp => "unp" |
349 | Sap => "sap" | Esa => "esa" |
349 | Sap => "sap" | Esa => "esa" |
350 | Sat => "sat" | Fsa => "fsa" |
350 | Sat => "sat" | Fsa => "fsa" |
351 | Thm => "thm" | Wuc => "wuc" |
351 | Thm => "thm" | Wuc => "wuc" |
352 | Eqv => "eqv" | Tac => "tac" |
352 | Eqv => "eqv" | Tac => "tac" |
353 | Wec => "wec" | Eth => "eth" |
353 | Wec => "wec" | Eth => "eth" |
354 | Tau => "tau" | Wtc => "wtc" |
354 | Tau => "tau" | Wtc => "wtc" |
355 | Wth => "wth" | Cax => "cax" |
355 | Wth => "wth" | Cax => "cax" |
356 | Sca => "sca" | Tca => "tca" |
356 | Sca => "sca" | Tca => "tca" |
357 | Wca => "wca" | Cup => "cup" |
357 | Wca => "wca" | Cup => "cup" |
358 | Csp => "csp" | Ecs => "ecs" |
358 | Csp => "csp" | Ecs => "ecs" |
359 | Csa => "csa" | Cth => "cth" |
359 | Csa => "csa" | Cth => "cth" |
360 | Ceq => "ceq" | Unc => "unc" |
360 | Ceq => "ceq" | Unc => "unc" |
361 | Wcc => "wcc" | Ect => "ect" |
361 | Wcc => "wcc" | Ect => "ect" |
362 | Fun => "fun" | Uns => "uns" |
362 | Fun => "fun" | Uns => "uns" |
363 | Wct => "wct" | Scc => "scc" |
363 | Wct => "wct" | Scc => "scc" |
364 | Uca => "uca" | Noc => "noc" |
364 | Uca => "uca" | Noc => "noc" |
365 |
365 |
366 fun string_of_tptp_term x = |
366 fun string_of_tptp_term x = |
367 case x of |
367 case x of |
368 Term_Func (symbol, tptp_term_list) => |
368 Term_Func (symbol, tptp_term_list) => |
369 "(" ^ string_of_symbol symbol ^ " " ^ |
369 "(" ^ string_of_symbol symbol ^ " " ^ |