author  blanchet 
Sun, 01 May 2011 22:36:58 +0200  
changeset 42593  f9d7f1331a00 
parent 42589  9f7c48463645 
child 42595  13c7194a896a 
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 = 
42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

16 
string * minimize_command * string proof * int 
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 = 
42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

19 
Proof.context * bool * type_system * int * string Symtab.table 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

20 
* int list list 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

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

22 

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

23 
val repair_conjecture_shape_and_fact_names : 
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42579
diff
changeset

24 
string > int list list > int > (string * locality) list vector 
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42579
diff
changeset

25 
> int list list * int * (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

26 
val used_facts_in_atp_proof : 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

27 
int > (string * locality) list vector > string proof 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

29 
val is_unsound_proof : 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

30 
int list list > int > (string * locality) list vector > string proof 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

31 
> 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

32 
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

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

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

35 
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

36 
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

37 
(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

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

39 
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

40 
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

41 
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

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

43 

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

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

46 

38028  47 
open ATP_Problem 
39452  48 
open ATP_Proof 
42579
2552c09b1a72
implement the new ATP type system in Sledgehammer
blanchet
parents:
42570
diff
changeset

49 
open ATP_Systems 
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39493
diff
changeset

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

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

54 

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

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

56 
type metis_params = 
42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

57 
string * minimize_command * string proof * int 
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

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

59 
type isar_params = 
42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

60 
Proof.context * bool * type_system * int * string Symtab.table 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

61 
* int list list 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

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

63 

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

66 

67 
fun find_first_in_list_vector vec key = 

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

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

70 

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

71 

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

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

73 

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

74 
(* 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

75 
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

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

77 

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

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

79 

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

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

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

82 
val tokens_of = String.tokens (not o Char.isAlphaNum) 
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42579
diff
changeset

83 
fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss) 
39493
cb2208f2c07d
move SPASS's Flotter hack to "Sledgehammer_Reconstruct"
blanchet
parents:
39455
diff
changeset

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

85 
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

86 

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

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

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

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

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

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

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

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

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

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

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

97 
#> 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

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

99 

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

100 
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

101 

42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42579
diff
changeset

102 
fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_offset 
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42579
diff
changeset

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

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

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

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

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

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

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

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

111 
> 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

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

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

114 
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

115 
> 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

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

117 
> 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

118 
(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

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

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

121 
in 
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42579
diff
changeset

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

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

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

125 
else 
42587
4fbb1de05169
fixed SPASS fact offset calculation and report unexpected unsound proofs with socalled sound encodings
blanchet
parents:
42579
diff
changeset

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

127 

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

128 
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

129 

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

130 
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

131 
(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

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

133 
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

134 
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

135 
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

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

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

138 
 NONE => []) 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

139 
 resolve_fact facts_offset 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

140 
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

141 
SOME j => 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

142 
let val j = j  facts_offset in 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

143 
if j > 0 andalso j <= Vector.length fact_names then 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

144 
Vector.sub (fact_names, j  1) 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

145 
else 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

146 
[] 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

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

149 

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

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

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

152 
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

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

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

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

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

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

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

159 

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

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

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

163 

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

164 
fun add_fact facts_offset fact_names (Inference (name, _, [])) = 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

165 
append (resolve_fact facts_offset fact_names name) 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

167 

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

169 
if null atp_proof then Vector.foldl (op @) [] fact_names 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

171 

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

172 
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

173 
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

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

175 

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

176 
fun is_unsound_proof conjecture_shape facts_offset fact_names = 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

177 
not o is_conjecture_referred_to_in_proof conjecture_shape andf 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

178 
forall (is_global_locality o snd) 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

179 
o used_facts_in_atp_proof facts_offset fact_names 
42449
494e4ac5b0f8
detect some unsound proofs before showing them to the user
blanchet
parents:
42361
diff
changeset

180 

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

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

182 

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

183 
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

184 

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

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

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

187 
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

188 
 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

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

190 
"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

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

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

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

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

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

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

197 
"using " ^ space_implode " " (map string_for_label ls) ^ " " 
42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

198 
fun metis_name full_types = if full_types then "metisFT" else "metis" 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

199 
fun metis_call full_types ss = command_call "metis" ss 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

200 
fun metis_command full_types i n (ls, ss) = 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

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

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

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

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

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

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

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

208 
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

209 

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

210 
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

211 
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

212 
#> 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

213 

42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

214 
fun metis_proof_text (banner, minimize_command, atp_proof, facts_offset, 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

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

216 
let 
42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

217 
val (chained, extra) = 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

218 
atp_proof > used_facts_in_atp_proof facts_offset fact_names 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

220 
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

221 
in 
42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

222 
(try_command_line banner (metis_command false i n ([], map fst extra)) ^ 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

223 
minimize_line minimize_command (map fst (extra @ chained)), 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

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

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

226 

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

227 
(** 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

228 

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

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

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

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

234 
 s_not t = @{const Not} $ t 

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

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

237 
 s_conj p = HOLogic.mk_conj p 

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

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

240 
 s_disj p = HOLogic.mk_disj p 

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

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

243 
 s_imp p = HOLogic.mk_imp p 

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

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

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

247 

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

250 

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

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

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

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

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

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

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

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

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

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

262 
 negate_term t = @{const Not} $ t 

39368  263 

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

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

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

266 

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

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

268 
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

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

270 

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

271 
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

272 
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

273 
[j] => (conjecture_prefix, j) 
39455  274 
 _ => 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

275 
SOME j => (raw_prefix, j) 
39455  276 
 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

277 

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

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

279 

37991  280 
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

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

283 

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

284 
(* Type variables are given the basic sort "HOL.type". Some will later be 
37991  285 
constrained by information from type literals, or by type inference. *) 
42563  286 
fun typ_from_fo_term tfrees (u as ATerm (a, us)) = 
287 
let val Ts = map (typ_from_fo_term tfrees) us in 

38748  288 
case strip_prefix_and_unascii type_const_prefix a of 
37991  289 
SOME b => Type (invert_const b, Ts) 
290 
 NONE => 

291 
if not (null us) then 

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

38748  293 
else case strip_prefix_and_unascii tfree_prefix a of 
37991  294 
SOME b => 
295 
let val s = "'" ^ b in 

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

297 
end 

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

298 
 NONE => 
38748  299 
case strip_prefix_and_unascii tvar_prefix a of 
37991  300 
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

301 
 NONE => 
37991  302 
(* Variable from the ATP, say "X1" *) 
303 
Type_Infer.param 0 (a, HOLogic.typeS) 

304 
end 

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

305 

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

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

38748  309 
case (strip_prefix_and_unascii class_prefix a, 
42563  310 
map (typ_from_fo_term tfrees) us) of 
38014  311 
(SOME b, [T]) => (pos, b, T) 
312 
 _ => raise FO_TERM [u] 

313 

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

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

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

318 
 add_type_constraint _ = I 

319 

38490  320 
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

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

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

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

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

326 
[_] => (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

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

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

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

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

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

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

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

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

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

336 

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

337 
(* Firstorder translation. No types are known for variables. "HOLogic.typeT" 
38014  338 
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

339 
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

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

341 
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

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

343 
ATerm (a, us) => 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42587
diff
changeset

344 
if String.isPrefix tff_type_prefix a then 
42551
cd99d6d3027a
reconstruct TFF type predicates correctly for ToFoF
blanchet
parents:
42549
diff
changeset

345 
@{const True} (* ignore TFF type information *) 
38748  346 
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

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

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

351 
@{const True} 

352 
else 

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

354 
end 

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

355 
 SOME b => 
42549
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

356 
let val (b, mangled_us) = b > unmangled_const >> invert_const in 
42589
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42587
diff
changeset

357 
if b = type_tag_name then 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42587
diff
changeset

358 
case mangled_us @ us of 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42587
diff
changeset

359 
[typ_u, term_u] => 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42587
diff
changeset

360 
aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42587
diff
changeset

361 
 _ => raise FO_TERM us 
9f7c48463645
restructured type systems some more  the old naming schemes had "argshg diff less" and "tagshg diff less" as equivalent and didn't support a monomorphic version of "tags"
blanchet
parents:
42587
diff
changeset

362 
else if b = predicator_base then 
42549
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

363 
aux (SOME @{typ bool}) [] (hd us) 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

364 
else if b = explicit_app_base then 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

365 
aux opt_T (nth us 1 :: extra_us) (hd us) 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

366 
else if b = type_pred_base then 
42551
cd99d6d3027a
reconstruct TFF type predicates correctly for ToFoF
blanchet
parents:
42549
diff
changeset

367 
@{const True} (* ignore type predicates *) 
42549
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

368 
else 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

369 
let 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

370 
val num_ty_args = num_atp_type_args thy type_sys b 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

371 
val (type_us, term_us) = 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

372 
chop num_ty_args us >> append mangled_us 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

373 
(* Extra args from "hAPP" come after any arguments given 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

374 
directly to the constant. *) 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

375 
val term_ts = map (aux NONE []) term_us 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

376 
val extra_ts = map (aux NONE []) extra_us 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

377 
val T = 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

378 
case opt_T of 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

379 
SOME T => map fastype_of term_ts > T 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

380 
 NONE => 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

381 
if num_type_args thy b = length type_us then 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

382 
Sign.const_instance thy 
42563  383 
(b, map (typ_from_fo_term tfrees) type_us) 
42549
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

384 
else 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

385 
HOLogic.typeT 
42570
77f94ac04f32
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
blanchet
parents:
42568
diff
changeset

386 
val b = unproxify_const b 
42549
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

387 
in list_comb (Const (b, T), term_ts @ extra_ts) end 
b9754f26c7bc
handle special constants correctly in Isar proof reconstruction code, especially type predicates
blanchet
parents:
42544
diff
changeset

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

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

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

391 
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

392 
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

393 
val t = 
38748  394 
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

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

396 
 NONE => 
38748  397 
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

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

399 
 NONE => 
39452  400 
if is_atp_variable a then 
38490  401 
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

402 
else 
38488  403 
(* Skolem constants? *) 
38490  404 
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

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

407 

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

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

411 
#> pair @{const True} 

412 
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

413 
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

414 

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

415 
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

416 
[(@{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

417 
(@{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

418 
(@{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

419 
(@{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

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

421 

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

422 
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

423 
 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

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

425 
(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

426 
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

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

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

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

430 

37991  431 
(* Update schematic type variables with detected sort constraints. It's not 
42563  432 
totally clear whether this code is necessary. *) 
38014  433 
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

434 
let 
37991  435 
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) 
436 
 do_type (TVar (xi, s)) = 

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

438 
 do_type (TFree z) = TFree z 

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

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

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

442 
 do_term (t as Bound _) = t 

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

444 
 do_term (t1 $ t2) = do_term t1 $ do_term t2 

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

446 

39425  447 
fun quantify_over_var quant_of var_s t = 
448 
let 

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

450 
> map Var 

451 
in fold_rev quant_of vars t end 

37991  452 

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

453 
(* 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

454 
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

455 
fun prop_from_formula thy type_sys tfrees phi = 
38014  456 
let 
457 
fun do_formula pos phi = 

37991  458 
case phi of 
38014  459 
AQuant (_, [], phi) => do_formula pos phi 
42526  460 
 AQuant (q, (s, _) :: xs, phi') => 
38014  461 
do_formula pos (AQuant (q, xs, phi')) 
42526  462 
(* FIXME: TFF *) 
39425  463 
#>> quantify_over_var (case q of 
464 
AForall => forall_of 

465 
 AExists => exists_of) 

42526  466 
(repair_atp_variable_name Char.toLower s) 
38014  467 
 AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not 
37991  468 
 AConn (c, [phi1, phi2]) => 
38014  469 
do_formula (pos > c = AImplies ? not) phi1 
470 
##>> do_formula pos phi2 

471 
#>> (case c of 

472 
AAnd => s_conj 

473 
 AOr => s_disj 

474 
 AImplies => s_imp 

38038  475 
 AIf => s_imp o swap 
476 
 AIff => s_iff 

40069  477 
 ANotIff => s_not o s_iff 
478 
 _ => 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

479 
 AAtom tm => term_from_pred thy type_sys tfrees pos tm 
37991  480 
 _ => raise FORMULA [phi] 
38014  481 
in repair_tvar_sorts (do_formula true phi Vartab.empty) end 
37991  482 

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

483 
fun check_formula ctxt = 
39288  484 
Type.constraint HOLogic.boolT 
42361  485 
#> 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

486 

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

487 

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

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

489 

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

490 
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

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

492 

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

493 
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

494 
let 
42361  495 
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

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

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

499 
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

500 
val t2 = prop_from_formula thy type_sys tfrees phi2 
36551  501 
val (t1, t2) = 
502 
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

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

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

505 
in 
39368  506 
(Definition (name, t1, t2), 
36551  507 
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

508 
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

509 
 decode_line type_sys tfrees (Inference (name, u, deps)) ctxt = 
36551  510 
let 
42361  511 
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

512 
val t = u > prop_from_formula thy type_sys tfrees 
37998  513 
> uncombine_term > check_formula ctxt 
36551  514 
in 
39368  515 
(Inference (name, t, deps), 
36551  516 
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

517 
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

518 
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

519 
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

520 

38035  521 
fun is_same_inference _ (Definition _) = false 
522 
 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

523 

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

524 
(* 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

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

526 
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

527 

39373  528 
fun replace_one_dependency (old, new) dep = 
39452  529 
if is_same_step (dep, old) then new else [dep] 
39373  530 
fun replace_dependencies_in_line _ (line as Definition _) = line 
531 
 replace_dependencies_in_line p (Inference (name, t, deps)) = 

532 
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

533 

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

534 
(* 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

535 
they differ only in type information.*) 
36551  536 
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

537 
 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

538 
(* 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

539 
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

540 
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

541 
(* Facts are not proof lines. *) 
36486
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 
39373  543 
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

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 
39373  546 
(_, []) => lines (* no repetition of proof line *) 
39368  547 
 (pre, Inference (name', _, _) :: post) => 
39373  548 
pre @ map (replace_dependencies_in_line (name', [name])) post 
40069  549 
 _ => raise Fail "unexpected inference" 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39368
diff
changeset

550 
else if is_conjecture conjecture_shape name then 
39368  551 
Inference (name, negate_term t, []) :: lines 
36551  552 
else 
39373  553 
map (replace_dependencies_in_line (name, [])) lines 
39368  554 
 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

555 
(* 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

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

558 
(* Is there a repetition? If so, replace later line by earlier one. *) 
38035  559 
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

560 
(* FIXME: Doesn't this code risk conflating proofs involving different 
38035  561 
types? *) 
39368  562 
(_, []) => Inference (name, t, deps) :: lines 
563 
 (pre, Inference (name', t', _) :: post) => 

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

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

567 

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

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

572 
 add_nontrivial_line line lines = line :: lines 
39373  573 
and delete_dependency name lines = 
574 
fold_rev add_nontrivial_line 

575 
(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

576 

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

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

579 
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

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

581 

39368  582 
fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) = 
39373  583 
(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

584 
 add_desired_line isar_shrink_factor conjecture_shape fact_names frees 
39368  585 
(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

586 
(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

587 
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

588 
is_conjecture conjecture_shape name orelse 
39373  589 
(* the last line must be kept *) 
590 
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

591 
(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

592 
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

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

596 
j <> 1) then 

39368  597 
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

598 
else 
39373  599 
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

600 

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

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

602 

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

603 
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

604 
(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

605 

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

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

607 
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

608 

39452  609 
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

610 

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

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

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

614 
Assume of label * term  
39452  615 
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

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

617 
ByMetis of facts  
39452  618 
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

619 

36574  620 
fun smart_case_split [] facts = ByMetis facts 
621 
 smart_case_split proofs facts = CaseSplit (proofs, facts) 

622 

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

623 
fun add_fact_from_dependency conjecture_shape facts_offset fact_names 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

624 
if is_fact fact_names name then 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

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

627 
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

628 

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

629 
fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

631 
Assume (raw_label_for_name conjecture_shape name, t) 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

632 
 step_for_line conjecture_shape facts_offset fact_names j 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

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

42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

637 
ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

640 

39454  641 
fun repair_name "$true" = "c_True" 
642 
 repair_name "$false" = "c_False" 

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

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

645 
 repair_name s = 

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

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

648 
else 

649 
s 

650 

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

651 
fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

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

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

655 
atp_proof 
39454  656 
> nasty_atp_proof pool 
657 
> 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

658 
> 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

659 
> 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

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

661 
> 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

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

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

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

665 
(if null params then [] else [Fix params]) @ 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

666 
map2 (step_for_line conjecture_shape facts_offset fact_names) 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

668 
end 
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 
(* 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

671 
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

672 
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

673 
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

674 
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

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

676 
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

677 

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

678 
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

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

680 
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

681 
 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

682 
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

683 
 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

684 
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

685 

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

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

687 
 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

688 
 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

689 
 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

690 
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

691 

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

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

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

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

695 
 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

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

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

698 
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

699 
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

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

701 
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

702 
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

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

704 
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

705 
(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

706 
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

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

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

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

710 
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

711 

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

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

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

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

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

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

717 

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

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

720 
(* 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

721 
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

722 
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

723 
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

724 
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

725 
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

726 
 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

727 
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

728 
 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

729 
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

730 
 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

731 
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

732 
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

733 
 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

734 
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

735 
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

736 
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

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

738 
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

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

740 
 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

741 
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

742 
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

743 
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

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

745 
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

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

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

748 
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

749 
 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

750 
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

751 
 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

752 
patches) = 
39373  753 
(if member (op =) (snd (snd patches)) l andalso 
754 
not (member (op =) (fst (snd patches)) l) andalso 

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

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

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

758 
([contra_l], co_ls) => 

759 
if member (op =) qs Show then 

760 
second_pass end_qs (proof, assums, 

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

762 
else 

763 
second_pass end_qs 

764 
(proof, assums, 

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

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

767 
Assume (l, negate_term t) 

768 
else 

769 
Have (qs, l, negate_term t, 

770 
ByMetis (backpatch_label patches l))) 

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

772 
let 

773 
val proofs = 

774 
map_filter 

775 
(fn l => 

776 
if l = concl_l then 

777 
NONE 

778 
else 

779 
let 

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

781 
in 

782 
second_pass [] 

783 
(proof, assums, 

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

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

786 
> fst > SOME 

787 
end) contra_ls 

788 
val (assumes, facts) = 

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

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

791 
else 

792 
([], (co_ls, ss)) 

793 
in 

794 
(case join_proofs proofs of 

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

796 
Have (case_split_qualifiers proofs @ 

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

798 
smart_case_split proofs facts) :: proof_tail 

799 
 NONE => 

800 
[Have (case_split_qualifiers proofs @ end_qs, no_label, 

801 
concl_t, smart_case_split proofs facts)], 

802 
patches) 

803 
>> append assumes 

804 
end 

805 
 _ => raise Fail "malformed proof") 

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

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

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

808 
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

809 
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

810 

38490  811 
(* 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

812 
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

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

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

815 
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

816 
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

817 
(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

818 
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

819 
 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

820 
 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

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

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

823 
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

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

825 
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

826 
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

827 
 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

828 
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

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

830 

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

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

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

833 
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

834 
 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

835 
 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

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

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

838 
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

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

840 
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

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

842 
(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

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

844 
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

845 
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

846 
 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

847 
in aux no_label end 
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 
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

850 
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

851 
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

852 
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

853 
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

854 
 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

855 
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

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

857 
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

858 
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

859 
 _ => 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

860 
 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

861 
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

862 

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

863 
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

864 

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

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

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

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

868 
 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

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

870 
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

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

872 
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

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

874 
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

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

876 
 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

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

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

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

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

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

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

883 
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

884 
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

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

886 
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

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

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

889 
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

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

891 
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

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

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

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

895 
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

896 
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

897 
 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

898 
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

899 
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

900 

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

901 
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

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

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

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

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

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

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

908 
(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

909 
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

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

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

912 
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

913 
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

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

915 
(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

916 
(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

917 
(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

918 
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

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

920 
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

921 
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

922 
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

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

924 
(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

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

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

927 
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

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

929 
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

930 
 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

931 
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

932 
 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

933 
do_indent ind ^ do_have qs ^ " " ^ 
36479  934 
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

935 
 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

936 
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

937 
(map (do_block ind) proofs) ^ 
36479  938 
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

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

940 
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

941 
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

942 
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

943 
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

944 
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

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

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

947 
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

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

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

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

951 
 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

952 
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ 
39452  953 
do_indent 0 ^ "proof \n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ 
954 
(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

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

956 

42593
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

957 
fun isar_proof_text (ctxt, debug, type_sys, isar_shrink_factor, pool, 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

958 
conjecture_shape) 
f9d7f1331a00
use "metis", not "metisFT", to reconstruct proofs found in fullytyped mode  "metisFT" is just too slow...
blanchet
parents:
42589
diff
changeset

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

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

961 
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

962 
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

963 
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

964 
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

965 
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

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

967 
case isar_proof_from_atp_proof pool ctxt type_sys tfrees 
42541
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

968 
isar_shrink_factor atp_proof conjecture_shape facts_offset 
8938507b2054
move type declarations to the front, for TFFcompliance
blanchet
parents:
42539
diff
changeset

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

970 
> 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

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

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

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

974 
> 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

975 
> string_for_proof ctxt type_sys i n of 
42554  976 
"" => "\nNo structured proof available (proof too short)." 
38599  977 
 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

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

979 
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

980 
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

981 
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

982 
try isar_proof_for () 
38599  983 
> 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

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

985 

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

986 
fun proof_text isar_proof isar_params metis_params = 
36557  987 
(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

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

989 

31038  990 
end; 