author  blanchet 
Sun, 01 May 2011 18:37:24 +0200  
changeset 42539  f6ba908b8b27 
parent 42531  a462dbaa584f 
child 42541  8938507b2054 
permissions  rwrr 
40114  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML 
38027  2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
3 
Author: Claire Quigley, Cambridge University Computer Laboratory 

36392  4 
Author: Jasmin Blanchette, TU Muenchen 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

5 

39495
bb4fb9ffe2d1
added new "Metis_Reconstruct" module, temporarily empty
blanchet
parents:
39494
diff
changeset

6 
Proof reconstruction for Sledgehammer. 
33310  7 
*) 
8 

40068  9 
signature SLEDGEHAMMER_ATP_RECONSTRUCT = 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

10 
sig 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

11 
type 'a proof = 'a ATP_Proof.proof 
38988  12 
type locality = Sledgehammer_Filter.locality 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

13 
type type_system = Sledgehammer_ATP_Translate.type_system 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

14 
type minimize_command = string list > string 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

15 
type metis_params = 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

16 
string * type_system * minimize_command * string proof 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

17 
* (string * locality) list vector * thm * int 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

18 
type isar_params = 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

19 
string Symtab.table * bool * int * Proof.context * int list list 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

20 
type text_result = string * (string * locality) list 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

21 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

22 
val repair_conjecture_shape_and_fact_names : 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

23 
string > int list list > (string * locality) list vector 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

24 
> int list list * (string * locality) list vector 
42451
a75fcd103cbb
automatically remove offending facts when faced with an unsound proof  instead of using the highly inefficient "full_types" option
blanchet
parents:
42449
diff
changeset

25 
val used_facts_in_atp_proof : 
a75fcd103cbb
automatically remove offending facts when faced with an unsound proof  instead of using the highly inefficient "full_types" option
blanchet
parents:
42449
diff
changeset

26 
(string * locality) list vector > string proof > (string * locality) list 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

27 
val is_unsound_proof : 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

28 
int list list > (string * locality) list vector > string proof > bool 
41151
d58157bb1ae7
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
blanchet
parents:
41146
diff
changeset

29 
val apply_on_subgoal : string > int > int > string 
40060
5ef6747aa619
first step in adding support for an SMT backend to Sledgehammer
blanchet
parents:
39953
diff
changeset

30 
val command_call : string > string list > string 
40064
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40060
diff
changeset

31 
val try_command_line : string > string > string 
db8413d82c3b
got rid of duplicate functionality ("run_smt_solver_somehow");
blanchet
parents:
40060
diff
changeset

32 
val minimize_line : ('a list > string) > 'a list > string 
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

33 
val split_used_facts : 
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

34 
(string * locality) list 
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

35 
> (string * locality) list * (string * locality) list 
41742
11e862c68b40
automatically minimize Z3asanATP proofs (cf. CVC3 and Yices)
blanchet
parents:
41203
diff
changeset

36 
val metis_proof_text : metis_params > text_result 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

37 
val isar_proof_text : isar_params > metis_params > text_result 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

38 
val proof_text : bool > isar_params > metis_params > text_result 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

39 
end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

40 

40068  41 
structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

42 
struct 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

43 

38028  44 
open ATP_Problem 
39452  45 
open ATP_Proof 
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset

46 
open Metis_Translate 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

47 
open Sledgehammer_Util 
38988  48 
open Sledgehammer_Filter 
40074  49 
open Sledgehammer_ATP_Translate 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

50 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

51 
type minimize_command = string list > string 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

52 
type metis_params = 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

53 
string * type_system * minimize_command * string proof 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

54 
* (string * locality) list vector * thm * int 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

55 
type isar_params = 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

56 
string Symtab.table * bool * int * Proof.context * int list list 
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

57 
type text_result = string * (string * locality) list 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

58 

39500  59 
fun is_head_digit s = Char.isDigit (String.sub (s, 0)) 
60 
val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) 

61 

62 
fun find_first_in_list_vector vec key = 

63 
Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key 

64 
 (_, value) => value) NONE vec 

65 

39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

66 

39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

67 
(** SPASS's Flotter hack **) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

68 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

69 
(* This is a hack required for keeping track of facts after they have been 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

70 
clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

71 
part of this hack. *) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

72 

cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

73 
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

74 

cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

75 
fun extract_clause_sequence output = 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

76 
let 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

77 
val tokens_of = String.tokens (not o Char.isAlphaNum) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

78 
fun extract_num ("clause" :: (ss as _ :: _)) = 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

79 
Int.fromString (List.last ss) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

80 
 extract_num _ = NONE 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

81 
in output > split_lines > map_filter (extract_num o tokens_of) end 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

82 

cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

83 
val parse_clause_formula_pair = 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

84 
$$ "("  scan_integer  $$ "," 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

85 
 (Symbol.scan_id ::: Scan.repeat ($$ ","  Symbol.scan_id))  $$ ")" 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

86 
 Scan.option ($$ ",") 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

87 
val parse_clause_formula_relation = 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

88 
Scan.this_string set_ClauseFormulaRelationN  $$ "(" 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

89 
 Scan.repeat parse_clause_formula_pair 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

90 
val extract_clause_formula_relation = 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

91 
Substring.full #> Substring.position set_ClauseFormulaRelationN 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

92 
#> snd #> Substring.position "." #> fst #> Substring.string 
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40204
diff
changeset

93 
#> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

94 
#> fst 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

95 

42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

96 
val unprefix_fact_number = space_implode "_" o tl o space_explode "_" 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

97 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

98 
fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names = 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

99 
if String.isSubstring set_ClauseFormulaRelationN output then 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

100 
let 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

101 
val j0 = hd (hd conjecture_shape) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

102 
val seq = extract_clause_sequence output 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

103 
val name_map = extract_clause_formula_relation output 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

104 
fun renumber_conjecture j = 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

105 
conjecture_prefix ^ string_of_int (j  j0) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

106 
> AList.find (fn (s, ss) => member (op =) ss s) name_map 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

107 
> map (fn s => find_index (curry (op =) s) seq + 1) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

108 
fun names_for_number j = 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

109 
j > AList.lookup (op =) name_map > these 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

110 
> map_filter (try (unascii_of o unprefix_fact_number 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

111 
o unprefix fact_prefix)) 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

112 
> map (fn name => 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

113 
(name, name > find_first_in_list_vector fact_names > the) 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

114 
handle Option.Option => 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

115 
error ("No such fact: " ^ quote name ^ ".")) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

116 
in 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

117 
(conjecture_shape > map (maps renumber_conjecture), 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

118 
seq > map names_for_number > Vector.fromList) 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

119 
end 
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

120 
else 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

121 
(conjecture_shape, fact_names) 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

122 

42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

123 
val vampire_step_prefix = "f" (* grrr... *) 
41203
1393514094d7
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (proof tptp)
blanchet
parents:
41151
diff
changeset

124 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

125 
fun resolve_fact fact_names ((_, SOME s)) = 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

126 
(case try (unprefix fact_prefix) s of 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

127 
SOME s' => 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

128 
let val s' = s' > unprefix_fact_number > unascii_of in 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

129 
case find_first_in_list_vector fact_names s' of 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

130 
SOME x => [(s', x)] 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

131 
 NONE => [] 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

132 
end 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

133 
 NONE => []) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

134 
 resolve_fact fact_names (num, NONE) = 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

135 
case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

136 
SOME j => 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

137 
if j > 0 andalso j <= Vector.length fact_names then 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

138 
Vector.sub (fact_names, j  1) 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

139 
else 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

140 
[] 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

141 
 NONE => [] 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

142 

42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

143 
fun resolve_conjecture conjecture_shape (num, s_opt) = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

144 
let 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

145 
val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

146 
SOME s => Int.fromString s > the_default ~1 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

147 
 NONE => case Int.fromString num of 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

148 
SOME j => find_index (exists (curry (op =) j)) 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

149 
conjecture_shape 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

150 
 NONE => ~1 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

151 
in if k >= 0 then [k] else [] end 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

152 

494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

153 
fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

154 
fun is_conjecture conjecture_shape = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

155 
not o null o resolve_conjecture conjecture_shape 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

156 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

157 
fun add_fact fact_names (Inference (name, _, [])) = 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

158 
append (resolve_fact fact_names name) 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

159 
 add_fact _ _ = I 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

160 

42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

161 
fun used_facts_in_atp_proof fact_names atp_proof = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

162 
if null atp_proof then Vector.foldl (op @) [] fact_names 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

163 
else fold (add_fact fact_names) atp_proof [] 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

164 

494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

165 
fun is_conjecture_referred_to_in_proof conjecture_shape = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

166 
exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

167 
 _ => false) 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

168 

494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

169 
fun is_unsound_proof conjecture_shape fact_names = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

170 
(not o is_conjecture_referred_to_in_proof conjecture_shape) andf 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

171 
forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

172 

494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

173 
(** Softcore proof reconstruction: Metis oneliner **) 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

174 

494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

175 
fun string_for_label (s, num) = s ^ string_of_int num 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

176 

494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

177 
fun set_settings "" = "" 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

178 
 set_settings settings = "using [[" ^ settings ^ "]] " 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

179 
fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by " 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

180 
 apply_on_subgoal settings 1 _ = set_settings settings ^ "apply " 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

181 
 apply_on_subgoal settings i n = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

182 
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

183 
fun command_call name [] = name 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

184 
 command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

185 
fun try_command_line banner command = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

186 
banner ^ ": " ^ Markup.markup Markup.sendback command ^ "." 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

187 
fun using_labels [] = "" 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

188 
 using_labels ls = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

189 
"using " ^ space_implode " " (map string_for_label ls) ^ " " 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

190 
fun metis_name type_sys = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

191 
if type_system_types_dangerous_types type_sys then "metisFT" else "metis" 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

192 
fun metis_call type_sys ss = command_call (metis_name type_sys) ss 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

193 
fun metis_command type_sys i n (ls, ss) = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

194 
using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

195 
fun metis_line banner type_sys i n ss = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

196 
try_command_line banner (metis_command type_sys i n ([], ss)) 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

197 
fun minimize_line _ [] = "" 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

198 
 minimize_line minimize_command ss = 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

199 
case minimize_command ss of 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

200 
"" => "" 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

201 
 command => 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

202 
"\nTo minimize the number of lemmas, try this: " ^ 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

203 
Markup.markup Markup.sendback command ^ "." 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

204 

40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

205 
val split_used_facts = 
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

206 
List.partition (curry (op =) Chained o snd) 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

207 
#> pairself (sort_distinct (string_ord o pairself fst)) 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

208 

42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

209 
fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names, 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

210 
goal, i) = 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

211 
let 
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

212 
val (chained_lemmas, other_lemmas) = 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

213 
split_used_facts (used_facts_in_atp_proof fact_names atp_proof) 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

214 
val n = Logic.count_prems (prop_of goal) 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

215 
in 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

216 
(metis_line banner type_sys i n (map fst other_lemmas) ^ 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

217 
minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

218 
other_lemmas @ chained_lemmas) 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

219 
end 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

220 

1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

221 
(** Hardcore proof reconstruction: structured Isar proofs **) 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

222 

38014  223 
(* Simple simplifications to ensure that sort annotations don't leave a trail of 
224 
spurious "True"s. *) 

225 
fun s_not @{const False} = @{const True} 

226 
 s_not @{const True} = @{const False} 

227 
 s_not (@{const Not} $ t) = t 

228 
 s_not t = @{const Not} $ t 

229 
fun s_conj (@{const True}, t2) = t2 

230 
 s_conj (t1, @{const True}) = t1 

231 
 s_conj p = HOLogic.mk_conj p 

232 
fun s_disj (@{const False}, t2) = t2 

233 
 s_disj (t1, @{const False}) = t1 

234 
 s_disj p = HOLogic.mk_disj p 

235 
fun s_imp (@{const True}, t2) = t2 

236 
 s_imp (t1, @{const False}) = s_not t1 

237 
 s_imp p = HOLogic.mk_imp p 

238 
fun s_iff (@{const True}, t2) = t2 

239 
 s_iff (t1, @{const True}) = t1 

240 
 s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 

241 

39425  242 
fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t 
243 
fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t 

244 

39452  245 
fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) = 
246 
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t') 

247 
 negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = 

248 
Const (@{const_name All}, T) $ Abs (s, T', negate_term t') 

249 
 negate_term (@{const HOL.implies} $ t1 $ t2) = 

250 
@{const HOL.conj} $ t1 $ negate_term t2 

251 
 negate_term (@{const HOL.conj} $ t1 $ t2) = 

252 
@{const HOL.disj} $ negate_term t1 $ negate_term t2 

253 
 negate_term (@{const HOL.disj} $ t1 $ t2) = 

254 
@{const HOL.conj} $ negate_term t1 $ negate_term t2 

255 
 negate_term (@{const Not} $ t) = t 

256 
 negate_term t = @{const Not} $ t 

39368  257 

39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

258 
val indent_size = 2 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

259 
val no_label = ("", ~1) 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

260 

1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

261 
val raw_prefix = "X" 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

262 
val assum_prefix = "A" 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

263 
val have_prefix = "F" 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

264 

39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

265 
fun raw_label_for_name conjecture_shape name = 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

266 
case resolve_conjecture conjecture_shape name of 
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

267 
[j] => (conjecture_prefix, j) 
39455  268 
 _ => case Int.fromString (fst name) of 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

269 
SOME j => (raw_prefix, j) 
39455  270 
 NONE => (raw_prefix ^ fst name, 0) 
39453
1740a2d6bef9
use the same TSTP/Vampire/SPASS parser for oneliners as for Isar proofs
blanchet
parents:
39452
diff
changeset

271 

21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

272 
(**** INTERPRETATION OF TSTP SYNTAX TREES ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

273 

37991  274 
exception FO_TERM of string fo_term list 
42531
a462dbaa584f
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet
parents:
42526
diff
changeset

275 
exception FORMULA of (string, string, string fo_term) formula list 
37991  276 
exception SAME of unit 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

277 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

278 
(* Type variables are given the basic sort "HOL.type". Some will later be 
37991  279 
constrained by information from type literals, or by type inference. *) 
280 
fun type_from_fo_term tfrees (u as ATerm (a, us)) = 

281 
let val Ts = map (type_from_fo_term tfrees) us in 

38748  282 
case strip_prefix_and_unascii type_const_prefix a of 
37991  283 
SOME b => Type (invert_const b, Ts) 
284 
 NONE => 

285 
if not (null us) then 

286 
raise FO_TERM [u] (* only "tconst"s have type arguments *) 

38748  287 
else case strip_prefix_and_unascii tfree_prefix a of 
37991  288 
SOME b => 
289 
let val s = "'" ^ b in 

290 
TFree (s, AList.lookup (op =) tfrees s > the_default HOLogic.typeS) 

291 
end 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

292 
 NONE => 
38748  293 
case strip_prefix_and_unascii tvar_prefix a of 
37991  294 
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

295 
 NONE => 
37991  296 
(* Variable from the ATP, say "X1" *) 
297 
Type_Infer.param 0 (a, HOLogic.typeS) 

298 
end 

21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

299 

38014  300 
(* Type class literal applied to a type. Returns triple of polarity, class, 
301 
type. *) 

302 
fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) = 

38748  303 
case (strip_prefix_and_unascii class_prefix a, 
38014  304 
map (type_from_fo_term tfrees) us) of 
305 
(SOME b, [T]) => (pos, b, T) 

306 
 _ => raise FO_TERM [u] 

307 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

308 
(** Accumulate type constraints in a formula: negative type literals **) 
38014  309 
fun add_var (key, z) = Vartab.map_default (key, []) (cons z) 
310 
fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) 

311 
 add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) 

312 
 add_type_constraint _ = I 

313 

38490  314 
fun repair_atp_variable_name f s = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

315 
let 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

316 
fun subscript_name s n = s ^ nat_subscript n 
38488  317 
val s = String.map f s 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

318 
in 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

319 
case space_explode "_" s of 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

320 
[_] => (case take_suffix Char.isDigit (String.explode s) of 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

321 
(cs1 as _ :: _, cs2 as _ :: _) => 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

322 
subscript_name (String.implode cs1) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

323 
(the (Int.fromString (String.implode cs2))) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

324 
 (_, _) => s) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

325 
 [s1, s2] => (case Int.fromString s2 of 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

326 
SOME n => subscript_name s1 n 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

327 
 NONE => s) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

328 
 _ => s 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

329 
end 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

330 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

331 
(* Firstorder translation. No types are known for variables. "HOLogic.typeT" 
38014  332 
should allow them to be inferred. *) 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

333 
fun raw_term_from_pred thy type_sys tfrees = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

334 
let 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

335 
fun aux opt_T extra_us u = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

336 
case u of 
42539
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42531
diff
changeset

337 
ATerm (a, us) => 
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42531
diff
changeset

338 
if a = boolify_name then 
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42531
diff
changeset

339 
aux (SOME @{typ bool}) [] (hd us) 
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42531
diff
changeset

340 
else if a = explicit_app_name then 
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42531
diff
changeset

341 
aux opt_T (nth us 1 :: extra_us) (hd us) 
f6ba908b8b27
generate typing for "hBOOL" in "Many_Typed" mode + tuning
blanchet
parents:
42531
diff
changeset

342 
else if a = type_tag_name then 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

343 
case us of 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

344 
[typ_u, term_u] => 
37991  345 
aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u 
346 
 _ => raise FO_TERM us 

38748  347 
else case strip_prefix_and_unascii const_prefix a of 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

348 
SOME "equal" => 
39106  349 
let val ts = map (aux NONE []) us in 
350 
if length ts = 2 andalso hd ts aconv List.last ts then 

351 
(* Vampire is keen on producing these. *) 

352 
@{const True} 

353 
else 

354 
list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts) 

355 
end 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

356 
 SOME b => 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

357 
let 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

358 
val (c, mangled_us) = b > unmangled_const >> invert_const 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

359 
val num_ty_args = num_atp_type_args thy type_sys c 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

360 
val (type_us, term_us) = chop num_ty_args us >> append mangled_us 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

361 
(* Extra args from "hAPP" come after any arguments given directly to 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

362 
the constant. *) 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

363 
val term_ts = map (aux NONE []) term_us 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

364 
val extra_ts = map (aux NONE []) extra_us 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

365 
val T = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

366 
case opt_T of 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

367 
SOME T => map fastype_of term_ts > T 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

368 
 NONE => 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

369 
if num_type_args thy c = length type_us then 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

370 
Sign.const_instance thy (c, 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

371 
map (type_from_fo_term tfrees) type_us) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

372 
else 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

373 
HOLogic.typeT 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

374 
in list_comb (Const (c, T), term_ts @ extra_ts) end 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

375 
 NONE => (* a free or schematic variable *) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

376 
let 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

377 
val ts = map (aux NONE []) (us @ extra_us) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

378 
val T = map fastype_of ts > HOLogic.typeT 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

379 
val t = 
38748  380 
case strip_prefix_and_unascii fixed_var_prefix a of 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

381 
SOME b => Free (b, T) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

382 
 NONE => 
38748  383 
case strip_prefix_and_unascii schematic_var_prefix a of 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

384 
SOME b => Var ((b, 0), T) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

385 
 NONE => 
39452  386 
if is_atp_variable a then 
38490  387 
Var ((repair_atp_variable_name Char.toLower a, 0), T) 
38017
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset

388 
else 
38488  389 
(* Skolem constants? *) 
38490  390 
Var ((repair_atp_variable_name Char.toUpper a, 0), T) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

391 
in list_comb (t, ts) end 
38014  392 
in aux (SOME HOLogic.boolT) [] end 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

393 

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

394 
fun term_from_pred thy type_sys tfrees pos (u as ATerm (s, _)) = 
38014  395 
if String.isPrefix class_prefix s then 
396 
add_type_constraint (type_constraint_from_term pos tfrees u) 

397 
#> pair @{const True} 

398 
else 

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

399 
pair (raw_term_from_pred thy type_sys tfrees u) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

400 

36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

401 
val combinator_table = 
39953
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39710
diff
changeset

402 
[(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39710
diff
changeset

403 
(@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39710
diff
changeset

404 
(@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39710
diff
changeset

405 
(@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), 
aa54f347e5e2
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
blanchet
parents:
39710
diff
changeset

406 
(@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})] 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

407 

8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

408 
fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2)) 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

409 
 uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t') 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

410 
 uncombine_term (t as Const (x as (s, _))) = 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

411 
(case AList.lookup (op =) combinator_table s of 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

412 
SOME thm => thm > prop_of > specialize_type @{theory} x 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

413 
> Logic.dest_equals > snd 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

414 
 NONE => t) 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

415 
 uncombine_term t = t 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

416 

37991  417 
(* Update schematic type variables with detected sort constraints. It's not 
418 
totally clear when this code is necessary. *) 

38014  419 
fun repair_tvar_sorts (t, tvar_tab) = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

420 
let 
37991  421 
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) 
422 
 do_type (TVar (xi, s)) = 

423 
TVar (xi, the_default s (Vartab.lookup tvar_tab xi)) 

424 
 do_type (TFree z) = TFree z 

425 
fun do_term (Const (a, T)) = Const (a, do_type T) 

426 
 do_term (Free (a, T)) = Free (a, do_type T) 

427 
 do_term (Var (xi, T)) = Var (xi, do_type T) 

428 
 do_term (t as Bound _) = t 

429 
 do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) 

430 
 do_term (t1 $ t2) = do_term t1 $ do_term t2 

431 
in t > not (Vartab.is_empty tvar_tab) ? do_term end 

432 

39425  433 
fun quantify_over_var quant_of var_s t = 
434 
let 

435 
val vars = [] > Term.add_vars t > filter (fn ((s, _), _) => s = var_s) 

436 
> map Var 

437 
in fold_rev quant_of vars t end 

37991  438 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

439 
(* Interpret an ATP formula as a HOL term, extracting sort constraints as they 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

440 
appear in the formula. *) 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

441 
fun prop_from_formula thy type_sys tfrees phi = 
38014  442 
let 
443 
fun do_formula pos phi = 

37991  444 
case phi of 
38014  445 
AQuant (_, [], phi) => do_formula pos phi 
42526  446 
 AQuant (q, (s, _) :: xs, phi') => 
38014  447 
do_formula pos (AQuant (q, xs, phi')) 
42526  448 
(* FIXME: TFF *) 
39425  449 
#>> quantify_over_var (case q of 
450 
AForall => forall_of 

451 
 AExists => exists_of) 

42526  452 
(repair_atp_variable_name Char.toLower s) 
38014  453 
 AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not 
37991  454 
 AConn (c, [phi1, phi2]) => 
38014  455 
do_formula (pos > c = AImplies ? not) phi1 
456 
##>> do_formula pos phi2 

457 
#>> (case c of 

458 
AAnd => s_conj 

459 
 AOr => s_disj 

460 
 AImplies => s_imp 

38038  461 
 AIf => s_imp o swap 
462 
 AIff => s_iff 

40069  463 
 ANotIff => s_not o s_iff 
464 
 _ => raise Fail "unexpected connective") 

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

465 
 AAtom tm => term_from_pred thy type_sys tfrees pos tm 
37991  466 
 _ => raise FORMULA [phi] 
38014  467 
in repair_tvar_sorts (do_formula true phi Vartab.empty) end 
37991  468 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

469 
fun check_formula ctxt = 
39288  470 
Type.constraint HOLogic.boolT 
42361  471 
#> Syntax.check_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

472 

72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

473 

72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

474 
(**** Translation of TSTP files to Isar Proofs ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

475 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

476 
fun unvarify_term (Var ((s, 0), T)) = Free (s, T) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

477 
 unvarify_term t = raise TERM ("unvarify_term: nonVar", [t]) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

478 

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

479 
fun decode_line type_sys tfrees (Definition (name, phi1, phi2)) ctxt = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

480 
let 
42361  481 
val thy = Proof_Context.theory_of ctxt 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

482 
val t1 = prop_from_formula thy type_sys tfrees phi1 
36551  483 
val vars = snd (strip_comb t1) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

484 
val frees = map unvarify_term vars 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

485 
val unvarify_args = subst_atomic (vars ~~ frees) 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

486 
val t2 = prop_from_formula thy type_sys tfrees phi2 
36551  487 
val (t1, t2) = 
488 
HOLogic.eq_const HOLogic.typeT $ t1 $ t2 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

489 
> unvarify_args > uncombine_term > check_formula ctxt 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

490 
> HOLogic.dest_eq 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

491 
in 
39368  492 
(Definition (name, t1, t2), 
36551  493 
fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

494 
end 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

495 
 decode_line type_sys tfrees (Inference (name, u, deps)) ctxt = 
36551  496 
let 
42361  497 
val thy = Proof_Context.theory_of ctxt 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

498 
val t = u > prop_from_formula thy type_sys tfrees 
37998  499 
> uncombine_term > check_formula ctxt 
36551  500 
in 
39368  501 
(Inference (name, t, deps), 
36551  502 
fold Variable.declare_term (OldTerm.term_frees t) ctxt) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

503 
end 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

504 
fun decode_lines ctxt type_sys tfrees lines = 
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

505 
fst (fold_map (decode_line type_sys tfrees) lines ctxt) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

506 

38035  507 
fun is_same_inference _ (Definition _) = false 
508 
 is_same_inference t (Inference (_, t', _)) = t aconv t' 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

509 

c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

510 
(* No "real" literals means only type information (tfree_tcs, clsrel, or 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

511 
clsarity). *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

512 
val is_only_type_information = curry (op aconv) HOLogic.true_const 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

513 

39373  514 
fun replace_one_dependency (old, new) dep = 
39452  515 
if is_same_step (dep, old) then new else [dep] 
39373  516 
fun replace_dependencies_in_line _ (line as Definition _) = line 
517 
 replace_dependencies_in_line p (Inference (name, t, deps)) = 

518 
Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) 

21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

519 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

520 
(* Discard facts; consolidate adjacent lines that prove the same formula, since 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

521 
they differ only in type information.*) 
36551  522 
fun add_line _ _ (line as Definition _) lines = line :: lines 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

523 
 add_line conjecture_shape fact_names (Inference (name, t, [])) lines = 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

524 
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

525 
definitions. *) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

526 
if is_fact fact_names name then 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

527 
(* Facts are not proof lines. *) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

528 
if is_only_type_information t then 
39373  529 
map (replace_dependencies_in_line (name, [])) lines 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

530 
(* Is there a repetition? If so, replace later line by earlier one. *) 
38035  531 
else case take_prefix (not o is_same_inference t) lines of 
39373  532 
(_, []) => lines (* no repetition of proof line *) 
39368  533 
 (pre, Inference (name', _, _) :: post) => 
39373  534 
pre @ map (replace_dependencies_in_line (name', [name])) post 
40069  535 
 _ => raise Fail "unexpected inference" 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

536 
else if is_conjecture conjecture_shape name then 
39368  537 
Inference (name, negate_term t, []) :: lines 
36551  538 
else 
39373  539 
map (replace_dependencies_in_line (name, [])) lines 
39368  540 
 add_line _ _ (Inference (name, t, deps)) lines = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

541 
(* Type information will be deleted later; skip repetition test. *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

542 
if is_only_type_information t then 
39368  543 
Inference (name, t, deps) :: lines 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

544 
(* Is there a repetition? If so, replace later line by earlier one. *) 
38035  545 
else case take_prefix (not o is_same_inference t) lines of 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

546 
(* FIXME: Doesn't this code risk conflating proofs involving different 
38035  547 
types? *) 
39368  548 
(_, []) => Inference (name, t, deps) :: lines 
549 
 (pre, Inference (name', t', _) :: post) => 

550 
Inference (name, t', deps) :: 

39373  551 
pre @ map (replace_dependencies_in_line (name', [name])) post 
40069  552 
 _ => raise Fail "unexpected inference" 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

553 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

554 
(* Recursively delete empty lines (type information) from the proof. *) 
39368  555 
fun add_nontrivial_line (Inference (name, t, [])) lines = 
39373  556 
if is_only_type_information t then delete_dependency name lines 
39368  557 
else Inference (name, t, []) :: lines 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

558 
 add_nontrivial_line line lines = line :: lines 
39373  559 
and delete_dependency name lines = 
560 
fold_rev add_nontrivial_line 

561 
(map (replace_dependencies_in_line (name, [])) lines) [] 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

562 

37323  563 
(* ATPs sometimes reuse free variable names in the strangest ways. Removing 
564 
offending lines often does the trick. *) 

36560
45c1870f234f
fixed definition of "bad frees" so that it actually works
blanchet
parents:
36559
diff
changeset

565 
fun is_bad_free frees (Free x) = not (member (op =) frees x) 
45c1870f234f
fixed definition of "bad frees" so that it actually works
blanchet
parents:
36559
diff
changeset

566 
 is_bad_free _ _ = false 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

567 

39368  568 
fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) = 
39373  569 
(j, line :: map (replace_dependencies_in_line (name, [])) lines) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

570 
 add_desired_line isar_shrink_factor conjecture_shape fact_names frees 
39368  571 
(Inference (name, t, deps)) (j, lines) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

572 
(j + 1, 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

573 
if is_fact fact_names name orelse 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

574 
is_conjecture conjecture_shape name orelse 
39373  575 
(* the last line must be kept *) 
576 
j = 0 orelse 

36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

577 
(not (is_only_type_information t) andalso 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

578 
null (Term.add_tvars t []) andalso 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

579 
not (exists_subterm (is_bad_free frees) t) andalso 
39373  580 
length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso 
581 
(* kill next to last line, which usually results in a trivial step *) 

582 
j <> 1) then 

39368  583 
Inference (name, t, deps) :: lines (* keep line *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

584 
else 
39373  585 
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

586 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

587 
(** Isar proof construction and manipulation **) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

588 

c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

589 
fun merge_fact_sets (ls1, ss1) (ls2, ss2) = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

590 
(union (op =) ls1 ls2, union (op =) ss1 ss2) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

591 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

592 
type label = string * int 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

593 
type facts = label list * string list 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

594 

39452  595 
datatype isar_qualifier = Show  Then  Moreover  Ultimately 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

596 

39452  597 
datatype isar_step = 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

598 
Fix of (string * typ) list  
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

599 
Let of term * term  
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

600 
Assume of label * term  
39452  601 
Have of isar_qualifier list * label * term * byline 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

602 
and byline = 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

603 
ByMetis of facts  
39452  604 
CaseSplit of isar_step list list * facts 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

605 

36574  606 
fun smart_case_split [] facts = ByMetis facts 
607 
 smart_case_split proofs facts = CaseSplit (proofs, facts) 

608 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

609 
fun add_fact_from_dependency conjecture_shape fact_names name = 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

610 
if is_fact fact_names name then 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

611 
apsnd (union (op =) (map fst (resolve_fact fact_names name))) 
36475
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

612 
else 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

613 
apfst (insert (op =) (raw_label_for_name conjecture_shape name)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

614 

39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

615 
fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) 
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

616 
 step_for_line conjecture_shape _ _ (Inference (name, t, [])) = 
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

617 
Assume (raw_label_for_name conjecture_shape name, t) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

618 
 step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) = 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

619 
Have (if j = 1 then [Show] else [], 
39425  620 
raw_label_for_name conjecture_shape name, 
621 
fold_rev forall_of (map Var (Term.add_vars t [])) t, 

40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

622 
ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names) 
39373  623 
deps ([], []))) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

624 

39454  625 
fun repair_name "$true" = "c_True" 
626 
 repair_name "$false" = "c_False" 

627 
 repair_name "$$e" = "c_equal" (* seen in Vampire proofs *) 

628 
 repair_name "equal" = "c_equal" (* needed by SPASS? *) 

629 
 repair_name s = 

630 
if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then 

631 
"c_equal" (* seen in Vampire proofs *) 

632 
else 

633 
s 

634 

42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

635 
fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

636 
atp_proof conjecture_shape fact_names params frees = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

637 
let 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

638 
val lines = 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

639 
atp_proof 
39454  640 
> nasty_atp_proof pool 
641 
> map_term_names_in_atp_proof repair_name 

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

642 
> decode_lines ctxt type_sys tfrees 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

643 
> rpair [] > fold_rev (add_line conjecture_shape fact_names) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

644 
> rpair [] > fold_rev add_nontrivial_line 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

645 
> rpair (0, []) > fold_rev (add_desired_line isar_shrink_factor 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

646 
conjecture_shape fact_names frees) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

647 
> snd 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

648 
in 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

649 
(if null params then [] else [Fix params]) @ 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40114
diff
changeset

650 
map2 (step_for_line conjecture_shape fact_names) (length lines downto 1) 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

651 
lines 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

652 
end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

653 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

654 
(* When redirecting proofs, we keep information about the labels seen so far in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

655 
the "backpatches" data structure. The first component indicates which facts 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

656 
should be associated with forthcoming proof steps. The second component is a 
37322
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

657 
pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should 
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

658 
become assumptions and "drop_ls" are the labels that should be dropped in a 
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

659 
case split. *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

660 
type backpatches = (label * facts) list * (label list * label list) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

661 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

662 
fun used_labels_of_step (Have (_, _, _, by)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

663 
(case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

664 
ByMetis (ls, _) => ls 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

665 
 CaseSplit (proofs, (ls, _)) => 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

666 
fold (union (op =) o used_labels_of) proofs ls) 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

667 
 used_labels_of_step _ = [] 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

668 
and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

669 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

670 
fun new_labels_of_step (Fix _) = [] 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

671 
 new_labels_of_step (Let _) = [] 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

672 
 new_labels_of_step (Assume (l, _)) = [l] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

673 
 new_labels_of_step (Have (_, l, _, _)) = [l] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

674 
val new_labels_of = maps new_labels_of_step 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

675 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

676 
val join_proofs = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

677 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

678 
fun aux _ [] = NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

679 
 aux proof_tail (proofs as (proof1 :: _)) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

680 
if exists null proofs then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

681 
NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

682 
else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

683 
aux (hd proof1 :: proof_tail) (map tl proofs) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

684 
else case hd proof1 of 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

685 
Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

686 
if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

687 
 _ => false) (tl proofs) andalso 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

688 
not (exists (member (op =) (maps new_labels_of proofs)) 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

689 
(used_labels_of proof_tail)) then 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

690 
SOME (l, t, map rev proofs, proof_tail) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

691 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

692 
NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

693 
 _ => NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

694 
in aux [] o map rev end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

695 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

696 
fun case_split_qualifiers proofs = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

697 
case length proofs of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

698 
0 => [] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

699 
 1 => [Then] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

700 
 _ => [Ultimately] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

701 

39372
2fd8a9a7080d
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
blanchet
parents:
39370
diff
changeset

702 
fun redirect_proof hyp_ts concl_t proof = 
33310  703 
let 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

704 
(* The first pass outputs those steps that are independent of the negated 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

705 
conjecture. The second pass flips the proof by contradiction to obtain a 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

706 
direct proof, introducing case splits when an inference depends on 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

707 
several facts that depend on the negated conjecture. *) 
39372
2fd8a9a7080d
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
blanchet
parents:
39370
diff
changeset

708 
val concl_l = (conjecture_prefix, length hyp_ts) 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

709 
fun first_pass ([], contra) = ([], contra) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

710 
 first_pass ((step as Fix _) :: proof, contra) = 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

711 
first_pass (proof, contra) >> cons step 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

712 
 first_pass ((step as Let _) :: proof, contra) = 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

713 
first_pass (proof, contra) >> cons step 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

714 
 first_pass ((step as Assume (l as (_, j), _)) :: proof, contra) = 
39372
2fd8a9a7080d
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
blanchet
parents:
39370
diff
changeset

715 
if l = concl_l then first_pass (proof, contra > cons step) 
2fd8a9a7080d
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
blanchet
parents:
39370
diff
changeset

716 
else first_pass (proof, contra) >> cons (Assume (l, nth hyp_ts j)) 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

717 
 first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = 
39372
2fd8a9a7080d
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
blanchet
parents:
39370
diff
changeset

718 
let val step = Have (qs, l, t, ByMetis (ls, ss)) in 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

719 
if exists (member (op =) (fst contra)) ls then 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

720 
first_pass (proof, contra >> cons l > cons step) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

721 
else 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

722 
first_pass (proof, contra) >> cons step 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

723 
end 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

724 
 first_pass _ = raise Fail "malformed proof" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

725 
val (proof_top, (contra_ls, contra_proof)) = 
39372
2fd8a9a7080d
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
blanchet
parents:
39370
diff
changeset

726 
first_pass (proof, ([concl_l], [])) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

727 
val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

728 
fun backpatch_labels patches ls = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

729 
fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

730 
fun second_pass end_qs ([], assums, patches) = 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

731 
([Have (end_qs, no_label, concl_t, 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

732 
ByMetis (backpatch_labels patches (map snd assums)))], patches) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

733 
 second_pass end_qs (Assume (l, t) :: proof, assums, patches) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

734 
second_pass end_qs (proof, (t, l) :: assums, patches) 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

735 
 second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums, 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

736 
patches) = 
39373  737 
(if member (op =) (snd (snd patches)) l andalso 
738 
not (member (op =) (fst (snd patches)) l) andalso 

739 
not (AList.defined (op =) (fst patches) l) then 

740 
second_pass end_qs (proof, assums, patches > apsnd (append ls)) 

741 
else case List.partition (member (op =) contra_ls) ls of 

742 
([contra_l], co_ls) => 

743 
if member (op =) qs Show then 

744 
second_pass end_qs (proof, assums, 

745 
patches >> cons (contra_l, (co_ls, ss))) 

746 
else 

747 
second_pass end_qs 

748 
(proof, assums, 

749 
patches >> cons (contra_l, (l :: co_ls, ss))) 

750 
>> cons (if member (op =) (fst (snd patches)) l then 

751 
Assume (l, negate_term t) 

752 
else 

753 
Have (qs, l, negate_term t, 

754 
ByMetis (backpatch_label patches l))) 

755 
 (contra_ls as _ :: _, co_ls) => 

756 
let 

757 
val proofs = 

758 
map_filter 

759 
(fn l => 

760 
if l = concl_l then 

761 
NONE 

762 
else 

763 
let 

764 
val drop_ls = filter (curry (op <>) l) contra_ls 

765 
in 

766 
second_pass [] 

767 
(proof, assums, 

768 
patches > apfst (insert (op =) l) 

769 
> apsnd (union (op =) drop_ls)) 

770 
> fst > SOME 

771 
end) contra_ls 

772 
val (assumes, facts) = 

773 
if member (op =) (fst (snd patches)) l then 

774 
([Assume (l, negate_term t)], (l :: co_ls, ss)) 

775 
else 

776 
([], (co_ls, ss)) 

777 
in 

778 
(case join_proofs proofs of 

779 
SOME (l, t, proofs, proof_tail) => 

780 
Have (case_split_qualifiers proofs @ 

781 
(if null proof_tail then end_qs else []), l, t, 

782 
smart_case_split proofs facts) :: proof_tail 

783 
 NONE => 

784 
[Have (case_split_qualifiers proofs @ end_qs, no_label, 

785 
concl_t, smart_case_split proofs facts)], 

786 
patches) 

787 
>> append assumes 

788 
end 

789 
 _ => raise Fail "malformed proof") 

36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

790 
 second_pass _ _ = raise Fail "malformed proof" 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

791 
val proof_bottom = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

792 
second_pass [Show] (contra_proof, [], ([], ([], []))) > fst 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

793 
in proof_top @ proof_bottom end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

794 

38490  795 
(* FIXME: Still needed? Probably not. *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

796 
val kill_duplicate_assumptions_in_proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

797 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

798 
fun relabel_facts subst = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

799 
apfst (map (fn l => AList.lookup (op =) subst l > the_default l)) 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

800 
fun do_step (step as Assume (l, t)) (proof, subst, assums) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

801 
(case AList.lookup (op aconv) assums t of 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

802 
SOME l' => (proof, (l, l') :: subst, assums) 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

803 
 NONE => (step :: proof, subst, (t, l) :: assums)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

804 
 do_step (Have (qs, l, t, by)) (proof, subst, assums) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

805 
(Have (qs, l, t, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

806 
case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

807 
ByMetis facts => ByMetis (relabel_facts subst facts) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

808 
 CaseSplit (proofs, facts) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

809 
CaseSplit (map do_proof proofs, relabel_facts subst facts)) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

810 
proof, subst, assums) 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

811 
 do_step step (proof, subst, assums) = (step :: proof, subst, assums) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

812 
and do_proof proof = fold do_step proof ([], [], []) > #1 > rev 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

813 
in do_proof end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

814 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

815 
val then_chain_proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

816 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

817 
fun aux _ [] = [] 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

818 
 aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

819 
 aux l' (Have (qs, l, t, by) :: proof) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

820 
(case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

821 
ByMetis (ls, ss) => 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

822 
Have (if member (op =) ls l' then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

823 
(Then :: qs, l, t, 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

824 
ByMetis (filter_out (curry (op =) l') ls, ss)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

825 
else 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

826 
(qs, l, t, ByMetis (ls, ss))) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

827 
 CaseSplit (proofs, facts) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

828 
Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

829 
aux l proof 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

830 
 aux _ (step :: proof) = step :: aux no_label proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

831 
in aux no_label end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

832 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

833 
fun kill_useless_labels_in_proof proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

834 
let 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

835 
val used_ls = used_labels_of proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

836 
fun do_label l = if member (op =) used_ls l then l else no_label 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

837 
fun do_step (Assume (l, t)) = Assume (do_label l, t) 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

838 
 do_step (Have (qs, l, t, by)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

839 
Have (qs, do_label l, t, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

840 
case by of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

841 
CaseSplit (proofs, facts) => 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

842 
CaseSplit (map (map do_step) proofs, facts) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

843 
 _ => by) 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

844 
 do_step step = step 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

845 
in map do_step proof end 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

846 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

847 
fun prefix_for_depth n = replicate_string (n + 1) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

848 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

849 
val relabel_proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

850 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

851 
fun aux _ _ _ [] = [] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

852 
 aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

853 
if l = no_label then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

854 
Assume (l, t) :: aux subst depth (next_assum, next_fact) proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

855 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

856 
let val l' = (prefix_for_depth depth assum_prefix, next_assum) in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

857 
Assume (l', t) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

858 
aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

859 
end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

860 
 aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

861 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

862 
val (l', subst, next_fact) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

863 
if l = no_label then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

864 
(l, subst, next_fact) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

865 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

866 
let 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41742
diff
changeset

867 
val l' = (prefix_for_depth depth have_prefix, next_fact) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

868 
in (l', (l, l') :: subst, next_fact + 1) end 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

869 
val relabel_facts = 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

870 
apfst (maps (the_list o AList.lookup (op =) subst)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

871 
val by = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

872 
case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

873 
ByMetis facts => ByMetis (relabel_facts facts) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

874 
 CaseSplit (proofs, facts) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

875 
CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

876 
relabel_facts facts) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

877 
in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

878 
Have (qs, l', t, by) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

879 
aux subst depth (next_assum, next_fact) proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

880 
end 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

881 
 aux subst depth nextp (step :: proof) = 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

882 
step :: aux subst depth nextp proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

883 
in aux [] 0 (1, 1) end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

884 

41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

885 
fun string_for_proof ctxt0 type_sys i n = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

886 
let 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39115
diff
changeset

887 
val ctxt = ctxt0 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39115
diff
changeset

888 
> Config.put show_free_types false 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39115
diff
changeset

889 
> Config.put show_types true 
37319
42268dc7d6c4
show types in Isar proofs, but not for free variables;
blanchet
parents:
37172
diff
changeset

890 
fun fix_print_mode f x = 
39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39115
diff
changeset

891 
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) 
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
39115
diff
changeset

892 
(print_mode_value ())) f x 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

893 
fun do_indent ind = replicate_string (ind * indent_size) " " 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

894 
fun do_free (s, T) = 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

895 
maybe_quote s ^ " :: " ^ 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

896 
maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

897 
fun do_label l = if l = no_label then "" else string_for_label l ^ ": " 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

898 
fun do_have qs = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

899 
(if member (op =) qs Moreover then "moreover " else "") ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

900 
(if member (op =) qs Ultimately then "ultimately " else "") ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

901 
(if member (op =) qs Then then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

902 
if member (op =) qs Show then "thus" else "hence" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

903 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

904 
if member (op =) qs Show then "show" else "have") 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

905 
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

906 
fun do_facts (ls, ss) = 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

907 
metis_command type_sys 1 1 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

908 
(ls > sort_distinct (prod_ord string_ord int_ord), 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

909 
ss > sort_distinct string_ord) 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

910 
and do_step ind (Fix xs) = 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

911 
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

912 
 do_step ind (Let (t1, t2)) = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

913 
do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

914 
 do_step ind (Assume (l, t)) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

915 
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

916 
 do_step ind (Have (qs, l, t, ByMetis facts)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

917 
do_indent ind ^ do_have qs ^ " " ^ 
36479  918 
do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

919 
 do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

920 
space_implode (do_indent ind ^ "moreover\n") 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

921 
(map (do_block ind) proofs) ^ 
36479  922 
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

923 
do_facts facts ^ "\n" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

924 
and do_steps prefix suffix ind steps = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

925 
let val s = implode (map (do_step ind) steps) in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

926 
replicate_string (ind * indent_size  size prefix) " " ^ prefix ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

927 
String.extract (s, ind * indent_size, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

928 
SOME (size s  ind * indent_size  1)) ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

929 
suffix ^ "\n" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

930 
end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

931 
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

932 
(* Onestep proofs are pointless; better use the Metis oneliner 
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

933 
directly. *) 
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

934 
and do_proof [Have (_, _, _, ByMetis _)] = "" 
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

935 
 do_proof proof = 
36480
1e01a7162435
polish Isar proofs: don't mention facts twice, and don't show oneliner "structured" proofs
blanchet
parents:
36479
diff
changeset

936 
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ 
39452  937 
do_indent 0 ^ "proof \n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ 
938 
(if n <> 1 then "next" else "qed") 

36488
32c92af68ec9
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
blanchet
parents:
36486
diff
changeset

939 
in do_proof end 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

940 

37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

941 
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

942 
(metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

943 
let 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

944 
val (params, hyp_ts, concl_t) = strip_subgoal goal i 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

945 
val frees = fold Term.add_frees (concl_t :: hyp_ts) [] 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

946 
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

947 
val n = Logic.count_prems (prop_of goal) 
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

948 
val (one_line_proof, lemma_names) = metis_proof_text metis_params 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

949 
fun isar_proof_for () = 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

950 
case isar_proof_from_atp_proof pool ctxt type_sys tfrees 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

951 
isar_shrink_factor atp_proof conjecture_shape fact_names params 
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

952 
frees 
39372
2fd8a9a7080d
first step in generalizing to nonnumeric proof step names (e.g. remote Vampire 0.6)
blanchet
parents:
39370
diff
changeset

953 
> redirect_proof hyp_ts concl_t 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

954 
> kill_duplicate_assumptions_in_proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

955 
> then_chain_proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

956 
> kill_useless_labels_in_proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

957 
> relabel_proof 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
40723
diff
changeset

958 
> string_for_proof ctxt type_sys i n of 
38599  959 
"" => "\nNo structured proof available." 
960 
 proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof 

35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

961 
val isar_proof = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

962 
if debug then 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

963 
isar_proof_for () 
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

964 
else 
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

965 
try isar_proof_for () 
38599  966 
> the_default "\nWarning: The Isar proof construction failed." 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

967 
in (one_line_proof ^ isar_proof, lemma_names) end 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

968 

40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

969 
fun proof_text isar_proof isar_params metis_params = 
36557  970 
(if isar_proof then isar_proof_text isar_params else metis_proof_text) 
40723
a82badd0e6ef
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
blanchet
parents:
40627
diff
changeset

971 
metis_params 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

972 

31038  973 
end; 