# HG changeset patch # User sultana # Date 1392825422 0 # Node ID 37c1abaf4876b339ff55ce2b4e76d3537cc98611 # Parent 5a9ef44731332141ec4d6035ab2fc31e2cec6e8e behaviour of tptp_graph now depends on an envir variable to indicate whether to produce proof graph containing formulas or not; tuned; diff -r 5a9ef4473133 -r 37c1abaf4876 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 @@ -22,37 +22,57 @@ open TPTP_Syntax +datatype style = + (*Only draw shapes. No formulas or edge labels.*) + Shapes + (*Don't draw shapes. Only write formulas (as nodes) and inference names (as edge labels)*) + | Formulas + +(*Determine the require output style form the TPTP_GRAPH environment variable. + Shapes is the default style.*) +val required_style = + if getenv "TPTP_GRAPH" = "formulas" then + Formulas + else Shapes + (*Draw an arc between two nodes*) fun dot_arc reverse (src, label) target = - "\"" ^ (if reverse then target else src) ^ - "\" -> \"" ^ (if reverse then src else target) ^ - "\" " ^ (case label of - NONE => "" - | SOME label => "[label=\"" ^ label ^ "\"];") ^ "\n" + let + val edge_label = + if required_style = Shapes then "" + else + case label of + NONE => "" + | SOME label => "[label=\"" ^ label ^ "\"];" + in + "\"" ^ (if reverse then target else src) ^ + "\" -> \"" ^ (if reverse then src else target) ^ + "\" " ^ edge_label ^ "\n" + end (*Node shapes indicate the role of the related clauses.*) exception NO_ROLE_SHAPE fun the_role_shape role = - case role of - Role_Axiom => "triangle" - | Role_Hypothesis => "invtrapezium" - | Role_Definition => "invtriangle" (*NOTE this is not standard wrt IDV*) - | Role_Assumption => "trapezium" (*NOTE this is not standard wrt IDV*) - | Role_Lemma => "hexagon" - | Role_Theorem => "star" (*NOTE this is not standard wrt IDV*) + if role = Role_Fi_Domain orelse + role = Role_Fi_Functors orelse + role = Role_Fi_Predicates orelse + role = Role_Type orelse + role = Role_Unknown then + raise NO_ROLE_SHAPE + else if required_style = Formulas then "plaintext" + else + case role of + Role_Axiom => "triangle" + | Role_Hypothesis => "invtrapezium" + | Role_Definition => "invtriangle" (*NOTE this is not standard wrt IDV*) + | Role_Assumption => "trapezium" (*NOTE this is not standard wrt IDV*) + | Role_Lemma => "hexagon" + | Role_Theorem => "star" (*NOTE this is not standard wrt IDV*) - (*FIXME add a parameter to switch the behaviour described below.*) - (*NOTE can change the next three to plaintext to avoid clutter if - the inference's conclusion formula is also being displayed.*) - | Role_Conjecture => (* "plaintext" *) "house" - | Role_Negated_Conjecture => (* "plaintext" *) "invhouse" - | Role_Plain => "plaintext" (* "circle" *) (*could also use none*) + | Role_Conjecture => "house" + | Role_Negated_Conjecture => "invhouse" + | Role_Plain => "circle" - | Role_Fi_Domain => raise NO_ROLE_SHAPE - | Role_Fi_Functors => raise NO_ROLE_SHAPE - | Role_Fi_Predicates => raise NO_ROLE_SHAPE - | Role_Type => raise NO_ROLE_SHAPE - | Role_Unknown => raise NO_ROLE_SHAPE fun have_role_shape role = (the_role_shape role; true) @@ -76,34 +96,41 @@ | is_last_line _ _ = false fun tptp_dot_node with_label reverse_arrows - (Annotated_Formula (_, lang, n, role, fmla_tptp, annot)) = - (*don't expect to find 'Include' in proofs*) - if have_role_shape role andalso role <> Role_Definition then - "\"" ^ n ^ - "\" [shape=\"" ^ - (if is_last_line lang fmla_tptp then "doublecircle" - else the_role_shape role) ^ - "\", style=\"" ^ the_lang_style lang ^ - (if role = Role_Definition then "\"];\n" else - (* "\", label=\"$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\"];\n") ^ *) -(*FIXME add a parameter to switch to using the following code, which lowers, centers, and horizontally-bounds the label. - (this is useful if you want to keep the shapes but also show formulas)*) - "\", label=\"\\\\begin{minipage}{10cm}\\\\vspace{21mm}\\\\centering$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\\\\end{minipage}\"];\n") ^ - (case TPTP_Proof.extract_source_info annot of - SOME (TPTP_Proof.Inference (rule, _, pinfos)) => - let - fun parent_id (TPTP_Proof.Parent n) = n - | parent_id (TPTP_Proof.ParentWithDetails (n, _)) = n - val parent_ids = map parent_id pinfos - in - map - (dot_arc reverse_arrows - (n, if with_label then SOME rule else NONE)) - parent_ids - |> implode - end - | _ => "") - else "" + (Annotated_Formula (_, lang, n, role, fmla_tptp, annot)) = + let + val node_label = + if required_style = Formulas then + "\", label=\"$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\"];\n" + (*FIXME add a parameter to switch to using the following code, which lowers, centers, and horizontally-bounds the label. + (this is useful if you want to keep the shapes but also show formulas)*) + (* "\", label=\"\\\\begin{minipage}{10cm}\\\\vspace{21mm}\\\\centering$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\\\\end{minipage}\"];\n") ^*) + else + "\", label=\"\"];\n" + in + (*don't expect to find 'Include' in proofs*) + if have_role_shape role andalso role <> Role_Definition then + "\"" ^ n ^ + "\" [shape=\"" ^ + (if is_last_line lang fmla_tptp then "doublecircle" + else the_role_shape role) ^ + "\", style=\"" ^ the_lang_style lang ^ + node_label ^ + (case TPTP_Proof.extract_source_info annot of + SOME (TPTP_Proof.Inference (rule, _, pinfos)) => + let + fun parent_id (TPTP_Proof.Parent n) = n + | parent_id (TPTP_Proof.ParentWithDetails (n, _)) = n + val parent_ids = map parent_id pinfos + in + map + (dot_arc reverse_arrows + (n, if with_label then SOME rule else NONE)) + parent_ids + |> implode + end + | _ => "") + else "" + end (*FIXME add opts to label arcs etc*) fun write_proof_dot input_file output_file =