# HG changeset patch # User sultana # Date 1392825422 0 # Node ID eb291b215c730bb858e7d3967c29898151ce6d89 # Parent c67c27f0ea9460fbb5404e1ace1b1e0ae3be458c cleaned code used to produce a proof-graph; diff -r c67c27f0ea94 -r eb291b215c73 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Wed Feb 19 15:57:02 2014 +0000 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Wed Feb 19 15:57:02 2014 +0000 @@ -525,38 +525,12 @@ | string_of_tptp_type (Subtype (symbol1, symbol2)) = string_of_symbol symbol1 ^ " << " ^ string_of_symbol symbol2 - -(*FIXME clean up this code!*) +(*FIXME formatting details haven't been fully worked out -- don't use this function for anything serious in its current form!*) (*TODO Add subscripting*) (*infix symbols, including \subset, \cup, \cap*) fun latex_of_tptp_term x = -((*writeln ("term=" ^ PolyML.makestring x);*) case x of -(* - Term_Func (Uninterpreted "subset", [tptp_t1, tptp_t2]) => - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Uninterpreted "union", [tptp_t1, tptp_t2]) => - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" -*) -(* - Term_Func (Interpreted_Logic Apply, [Term_Func (Interpreted_Logic Apply, [Uninterpreted "subset", tptp_t1]), tptp_t2]) => - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Interpreted_Logic Apply, [Term_Func (Interpreted_Logic Apply, [Uninterpreted "union", tptp_t1]), tptp_t2]) => - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" -*) -(* - Term_Func (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "subset", []), - tptp_t1])]), tptp_t2]) => - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" - | Term_Func (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "union", []), - tptp_t1])]), tptp_t2]) => - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" - - |*) Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) => + Term_Func (Interpreted_Logic Equals, [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")" | Term_Func (Interpreted_Logic NEquals, [tptp_t1, tptp_t2]) => "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")" @@ -576,11 +550,8 @@ | Term_Conditional (tptp_formula, tptp_term1, tptp_term2) => "" (*FIXME*) | Term_Num (_, str) => str | Term_Distinct_Object str => str (*FIXME*) -) + and latex_of_symbol (Uninterpreted str) = -(* if str = "union" then "\\\\cup" - else if str = "subset" then "\\\\subset" - else*) if str = "emptyset" then "\\\\emptyset" else "\\\\mathrm{" ^ str ^ "}" | latex_of_symbol (Interpreted_ExtraLogic interpreted_symbol) = latex_of_interpreted_symbol interpreted_symbol @@ -654,100 +625,48 @@ NONE => latex_of_symbol symbol | SOME tptp_type => latex_of_symbol symbol ^ " : " ^ latex_of_tptp_type tptp_type) - | latex_of_tptp_atom (THF_Atom_term tptp_term) = latex_of_tptp_term tptp_term + | latex_of_tptp_atom (THF_Atom_term tptp_term) = latex_of_tptp_term tptp_term | latex_of_tptp_atom (THF_Atom_conn_term symbol) = latex_of_symbol symbol -(* -and latex_of_tptp_formula (Pred (symbol, tptp_term_list)) = - "(" ^ latex_of_symbol symbol ^ - space_implode " " (map latex_of_tptp_term tptp_term_list) ^ ")" - | latex_of_tptp_formula (Fmla (symbol, tptp_formula_list)) = - "(" ^ latex_of_symbol symbol ^ - space_implode " " (map latex_of_tptp_formula tptp_formula_list) ^ ")" -*) -(* -and latex_of_tptp_formula (Pred (Uninterpreted "subset", [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" - | latex_of_tptp_formula (Pred (Uninterpreted "union", [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" -*) -and (*latex_of_tptp_formula ( - Pred (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "subset", []), - tptp_t1])]), tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_term tptp_t2 ^ ")" - | latex_of_tptp_formula (Pred (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, - [Term_Func (Interpreted_ExtraLogic Apply, [Term_Func (Uninterpreted "union", []), - tptp_t1])]), tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_term tptp_t2 ^ ")" - - |*) latex_of_tptp_formula (Pred (Interpreted_Logic Equals, [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")" - | latex_of_tptp_formula (Pred (Interpreted_Logic NEquals, [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")" - | latex_of_tptp_formula (Pred (Interpreted_Logic Or, [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")" - | latex_of_tptp_formula (Pred (Interpreted_Logic And, [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")" - | latex_of_tptp_formula (Pred (Interpreted_Logic Iff, [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" - | latex_of_tptp_formula (Pred (Interpreted_Logic If, [tptp_t1, tptp_t2])) = - "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" +and latex_of_tptp_formula (Pred (Interpreted_Logic Equals, [tptp_t1, tptp_t2])) = + "(" ^ latex_of_tptp_term tptp_t1 ^ " = " ^ latex_of_tptp_term tptp_t2 ^ ")" + | latex_of_tptp_formula (Pred (Interpreted_Logic NEquals, [tptp_t1, tptp_t2])) = + "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\neq " ^ latex_of_tptp_term tptp_t2 ^ ")" + | latex_of_tptp_formula (Pred (Interpreted_Logic Or, [tptp_t1, tptp_t2])) = + "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\vee " ^ latex_of_tptp_term tptp_t2 ^ ")" + | latex_of_tptp_formula (Pred (Interpreted_Logic And, [tptp_t1, tptp_t2])) = + "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\wedge " ^ latex_of_tptp_term tptp_t2 ^ ")" + | latex_of_tptp_formula (Pred (Interpreted_Logic Iff, [tptp_t1, tptp_t2])) = + "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" + | latex_of_tptp_formula (Pred (Interpreted_Logic If, [tptp_t1, tptp_t2])) = + "(" ^ latex_of_tptp_term tptp_t1 ^ " \\\\longrightarrow " ^ latex_of_tptp_term tptp_t2 ^ ")" | latex_of_tptp_formula (x as (Pred (symbol, tptp_term_list))) = -((*writeln ("fmla=" ^ PolyML.makestring x);*) - (*"(" ^*) latex_of_symbol symbol ^ - space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list) (*^ ")"*) -) + latex_of_symbol symbol ^ + space_implode "\\\\, " (map latex_of_tptp_term tptp_term_list) -(* - | latex_of_tptp_formula (Fmla (Uninterpreted "subset", [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")" - | latex_of_tptp_formula (Fmla (Uninterpreted "union", [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")" -*) + | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")" + + | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")" -(* - | latex_of_tptp_formula ( - Fmla (Interpreted_ExtraLogic Apply, - [Fmla (Interpreted_ExtraLogic Apply, - [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Uninterpreted "subset", []), - tptp_t1])]), tptp_t2])) = - "(" ^ latex_of_tptp_formula tptp_t1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_t2 ^ ")" - | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, - [Fmla (Interpreted_ExtraLogic Apply, - [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Uninterpreted "union", []), - tptp_t1])]), tptp_t2])) = - "(" ^ latex_of_tptp_formula tptp_t1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_t2 ^ ")" -*) - - | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "union", []))), tptp_f1]), tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\cup " ^ latex_of_tptp_formula tptp_f2 ^ ")" - - | latex_of_tptp_formula (Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "subset", []))), tptp_f1]), tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\subset " ^ latex_of_tptp_formula tptp_f2 ^ ")" - - - | latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " = " ^ latex_of_tptp_formula tptp_f2 ^ ")" - | latex_of_tptp_formula (Fmla (Interpreted_Logic NEquals, [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\neq " ^ latex_of_tptp_formula tptp_f2 ^ ")" - | latex_of_tptp_formula (Fmla (Interpreted_Logic Or, [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\vee " ^ latex_of_tptp_formula tptp_f2 ^ ")" - | latex_of_tptp_formula (Fmla (Interpreted_Logic And, [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\wedge " ^ latex_of_tptp_formula tptp_f2 ^ ")" - | latex_of_tptp_formula (Fmla (Interpreted_Logic Iff, [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")" - | latex_of_tptp_formula (Fmla (Interpreted_Logic If, [tptp_f1, tptp_f2])) = - "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")" + | latex_of_tptp_formula (Fmla (Interpreted_Logic Equals, [tptp_f1, tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " = " ^ latex_of_tptp_formula tptp_f2 ^ ")" + | latex_of_tptp_formula (Fmla (Interpreted_Logic NEquals, [tptp_f1, tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\neq " ^ latex_of_tptp_formula tptp_f2 ^ ")" + | latex_of_tptp_formula (Fmla (Interpreted_Logic Or, [tptp_f1, tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\vee " ^ latex_of_tptp_formula tptp_f2 ^ ")" + | latex_of_tptp_formula (Fmla (Interpreted_Logic And, [tptp_f1, tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\wedge " ^ latex_of_tptp_formula tptp_f2 ^ ")" + | latex_of_tptp_formula (Fmla (Interpreted_Logic Iff, [tptp_f1, tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longleftrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")" + | latex_of_tptp_formula (Fmla (Interpreted_Logic If, [tptp_f1, tptp_f2])) = + "(" ^ latex_of_tptp_formula tptp_f1 ^ " \\\\longrightarrow " ^ latex_of_tptp_formula tptp_f2 ^ ")" | latex_of_tptp_formula (x as (Fmla (symbol, tptp_formula_list))) = -(writeln ("fmla=" ^ PolyML.makestring x); - (*"(" ^*) latex_of_symbol symbol ^ - space_implode "\\\\, " (map latex_of_tptp_formula tptp_formula_list) (*^ ")"*) -) + latex_of_symbol symbol ^ + space_implode "\\\\, " (map latex_of_tptp_formula tptp_formula_list) | latex_of_tptp_formula (Sequent (tptp_formula_list1, tptp_formula_list2)) = "" (*FIXME*) | latex_of_tptp_formula (Quant (quantifier, varlist, tptp_formula)) = diff -r c67c27f0ea94 -r eb291b215c73 src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Wed Feb 19 15:57:02 2014 +0000 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_to_dot.ML Wed Feb 19 15:57:02 2014 +0000 @@ -30,7 +30,8 @@ (*Draw shapes and write the AF ID inside.*) | IDs -(*FIXME this kind of configurability isn't very user-friendly.*) +(*FIXME this kind of configurability isn't very user-friendly. + Ideally we'd accept a parameter from the tptp_graph script.*) (*Determine the require output style form the TPTP_GRAPH environment variable. Shapes is the default style.*) val required_style = @@ -78,7 +79,6 @@ | Role_Negated_Conjecture => "invhouse" | Role_Plain => "circle" - fun have_role_shape role = (the_role_shape role; true) handle NO_ROLE_SHAPE => false @@ -91,10 +91,11 @@ case lang of CNF => "dotted" | FOF => "dashed" - | THF => "" (* "filled" *) + | THF => "" (*NOTE could use "filled" to contrast with first-order languages*) | _ => raise NO_LANG_STYLE -(*Does the formula just consist of "$false"?*) +(*Check if the formula just consists of "$false"? + which we interpret to be the last line of the proof.*) fun is_last_line CNF (Pred (Interpreted_Logic False, [])) = true | is_last_line THF (Atom (THF_Atom_term (Term_Func (Interpreted_Logic False, [])))) = true @@ -142,13 +143,13 @@ (*FIXME add opts to label arcs etc*) fun write_proof_dot input_file output_file = let - (*rankdir=\"LR\";\n*) + (*NOTE sometimes useful to include: rankdir=\"LR\";\n*) val defaults = "graph[nodesep=3];\n" ^ "node[fixedsize=true];\n" ^ "node[width=0.5];\n" ^ "node[shape=plaintext];\n" ^ - (* "node[fillcolor=lightgray];\n" ^ *) + (*NOTE sometimes useful to include: "node[fillcolor=lightgray];\n" ^ *) "node[fontsize=50];\n" in TPTP_Parser.parse_file input_file