66 | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) |
66 | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) |
67 |
67 |
68 fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) |
68 fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) |
69 | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) |
69 | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) |
70 |
70 |
71 fun is_True_prop t = t aconv @{prop True} |
|
72 |
|
73 fun add_line_pass1 (line as (name, role, t, rule, [])) lines = |
71 fun add_line_pass1 (line as (name, role, t, rule, [])) lines = |
74 (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or |
72 (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or |
75 definitions. *) |
73 definitions. *) |
76 if role = Conjecture orelse role = Negated_Conjecture then line :: lines |
74 if role = Conjecture orelse role = Negated_Conjecture then line :: lines |
77 else if is_True_prop t then map (replace_dependencies_in_line (name, [])) lines |
75 else if t aconv @{prop True} then map (replace_dependencies_in_line (name, [])) lines |
78 else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines |
76 else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then line :: lines |
79 else if role = Axiom then lines (* axioms (facts) need no proof lines *) |
77 else if role = Axiom then lines (* axioms (facts) need no proof lines *) |
80 else map (replace_dependencies_in_line (name, [])) lines |
78 else map (replace_dependencies_in_line (name, [])) lines |
81 | add_line_pass1 line lines = line :: lines |
79 | add_line_pass1 line lines = line :: lines |
82 |
80 |
83 fun add_lines_pass2 res _ [] = rev res |
81 fun add_lines_pass2 res _ [] = rev res |
84 | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) = |
82 | add_lines_pass2 res prev_t ((line as (name, role, t, rule, deps)) :: lines) = |
85 let |
83 let |
86 val is_last_line = null lines |
84 fun looks_boring () = |
87 |
85 t aconv @{prop True} orelse t aconv @{prop False} orelse t aconv prev_t orelse |
88 fun looks_interesting () = |
86 length deps < 2 |
89 not (is_True_prop t) andalso not (t aconv prev_t) andalso null (Term.add_tvars t []) andalso |
|
90 length deps >= 2 andalso not (can the_single lines) |
|
91 |
87 |
92 fun is_skolemizing_line (_, _, _, rule', deps') = |
88 fun is_skolemizing_line (_, _, _, rule', deps') = |
93 is_skolemize_rule rule' andalso member (op =) deps' name |
89 is_skolemize_rule rule' andalso member (op =) deps' name |
94 fun is_before_skolemize_rule () = exists is_skolemizing_line lines |
90 fun is_before_skolemize_rule () = exists is_skolemizing_line lines |
95 in |
91 in |
96 if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse |
92 if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse |
97 is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse |
93 is_datatype_rule rule orelse null lines orelse not (looks_boring ()) orelse |
98 is_before_skolemize_rule () then |
94 is_before_skolemize_rule () then |
99 add_lines_pass2 (line :: res) t lines |
95 add_lines_pass2 (line :: res) t lines |
100 else |
96 else |
101 add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines) |
97 add_lines_pass2 res t (map (replace_dependencies_in_line (name, deps)) lines) |
102 end |
98 end |