39 | Role_Definition => "invtriangle" (*NOTE this is not standard wrt IDV*) |
39 | Role_Definition => "invtriangle" (*NOTE this is not standard wrt IDV*) |
40 | Role_Assumption => "trapezium" (*NOTE this is not standard wrt IDV*) |
40 | Role_Assumption => "trapezium" (*NOTE this is not standard wrt IDV*) |
41 | Role_Lemma => "hexagon" |
41 | Role_Lemma => "hexagon" |
42 | Role_Theorem => "star" (*NOTE this is not standard wrt IDV*) |
42 | Role_Theorem => "star" (*NOTE this is not standard wrt IDV*) |
43 |
43 |
44 (*NOTE changed the next three to plaintext to avoid clutter, since |
44 (*FIXME add a parameter to switch the behaviour described below.*) |
45 i'm also displaying the inference's conclusion in latex*) |
45 (*NOTE can change the next three to plaintext to avoid clutter if |
46 | Role_Conjecture => "plaintext" (* "house" *) |
46 the inference's conclusion formula is also being displayed.*) |
47 | Role_Negated_Conjecture => "plaintext" (* "invhouse" *) |
47 | Role_Conjecture => (* "plaintext" *) "house" |
|
48 | Role_Negated_Conjecture => (* "plaintext" *) "invhouse" |
48 | Role_Plain => "plaintext" (* "circle" *) (*could also use none*) |
49 | Role_Plain => "plaintext" (* "circle" *) (*could also use none*) |
49 |
50 |
50 | Role_Fi_Domain => raise NO_ROLE_SHAPE |
51 | Role_Fi_Domain => raise NO_ROLE_SHAPE |
51 | Role_Fi_Functors => raise NO_ROLE_SHAPE |
52 | Role_Fi_Functors => raise NO_ROLE_SHAPE |
52 | Role_Fi_Predicates => raise NO_ROLE_SHAPE |
53 | Role_Fi_Predicates => raise NO_ROLE_SHAPE |
82 "\" [shape=\"" ^ |
83 "\" [shape=\"" ^ |
83 (if is_last_line lang fmla_tptp then "doublecircle" |
84 (if is_last_line lang fmla_tptp then "doublecircle" |
84 else the_role_shape role) ^ |
85 else the_role_shape role) ^ |
85 "\", style=\"" ^ the_lang_style lang ^ |
86 "\", style=\"" ^ the_lang_style lang ^ |
86 (if role = Role_Definition then "\"];\n" else |
87 (if role = Role_Definition then "\"];\n" else |
87 "\", label=\"$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\"];\n") ^ |
88 (* "\", label=\"$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\"];\n") ^ *) |
|
89 (*FIXME add a parameter to switch to using the following code, which lowers, centers, and horizontally-bounds the label. |
|
90 (this is useful if you want to keep the shapes but also show formulas)*) |
|
91 "\", label=\"\\\\begin{minipage}{10cm}\\\\vspace{21mm}\\\\centering$" ^ TPTP_Syntax.latex_of_tptp_formula fmla_tptp ^ "$\\\\end{minipage}\"];\n") ^ |
88 (case TPTP_Proof.extract_source_info annot of |
92 (case TPTP_Proof.extract_source_info annot of |
89 SOME (TPTP_Proof.Inference (rule, _, pinfos)) => |
93 SOME (TPTP_Proof.Inference (rule, _, pinfos)) => |
90 let |
94 let |
91 fun parent_id (TPTP_Proof.Parent n) = n |
95 fun parent_id (TPTP_Proof.Parent n) = n |
92 | parent_id (TPTP_Proof.ParentWithDetails (n, _)) = n |
96 | parent_id (TPTP_Proof.ParentWithDetails (n, _)) = n |