author  blanchet 
Sun, 25 Apr 2010 11:38:46 +0200  
changeset 36393  be73a2b2443b 
parent 36392  c00c57850eb7 
child 36395  e73923451f6f 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML 
33310  2 
Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory 
36392  3 
Author: Jasmin Blanchette, TU Muenchen 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

4 

33310  5 
Transfer of proofs from external provers. 
6 
*) 

7 

35826  8 
signature SLEDGEHAMMER_PROOF_RECONSTRUCT = 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

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

10 
type minimize_command = string list > string 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

11 
type name_pool = Sledgehammer_FOL_Clause.name_pool 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

12 

25492
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25414
diff
changeset

13 
val chained_hint: string 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

14 
val invert_const: string > string 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

15 
val invert_type_const: string > string 
33243  16 
val num_typargs: theory > string > int 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

17 
val make_tvar: string > typ 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

18 
val strip_prefix: string > string > string option 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

19 
val metis_line: int > int > string list > string 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

20 
val metis_proof_text: 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

21 
minimize_command * string * string vector * thm * int 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

22 
> string * string list 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

23 
val isar_proof_text: 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

24 
name_pool option > bool > int > bool > Proof.context 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

25 
> minimize_command * string * string vector * thm * int 
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

26 
> string * string list 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

27 
val proof_text: 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

28 
bool > name_pool option > bool > int > bool > Proof.context 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

29 
> minimize_command * string * string vector * thm * int 
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

30 
> string * string list 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

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

32 

35826  33 
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

35 

35865  36 
open Sledgehammer_FOL_Clause 
37 
open Sledgehammer_Fact_Preprocessor 

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

38 

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

39 
type minimize_command = string list > string 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

40 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

41 
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" 
36392  42 
fun is_head_digit s = Char.isDigit (String.sub (s, 0)) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

43 

b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

44 
fun is_axiom thm_names line_no = line_no <= Vector.length thm_names 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

45 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

46 
fun ugly_name NONE s = s 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

47 
 ugly_name (SOME the_pool) s = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

48 
case Symtab.lookup (snd the_pool) s of 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

49 
SOME s' => s' 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

50 
 NONE => s 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

51 

be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

52 
val trace_path = Path.basic "sledgehammer_proof_trace" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

53 
fun trace_proof_msg f = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

54 
if !trace then File.append (File.tmp_path trace_path) (f ()) else (); 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

55 

be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

56 
val string_of_thm = PrintMode.setmp [] o Display.string_of_thm 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

57 

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

58 
(**** PARSING OF TSTP FORMAT ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

59 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

60 
(* Syntax trees, either term list or formulae *) 
36392  61 
datatype stree = SInt of int  SBranch of string * stree list; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

62 

36392  63 
fun atom x = SBranch (x, []) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

64 

36392  65 
fun scons (x, y) = SBranch ("cons", [x, y]) 
66 
val slist_of = List.foldl scons (atom "nil") 

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

67 

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

68 
(*Strings enclosed in single quotes, e.g. filenames*) 
36392  69 
val parse_quoted = $$ "'"  Scan.repeat (~$$ "'")  $$ "'" >> implode; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

70 

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

71 
(*Integer constants, typically proof line numbers*) 
36392  72 
val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

73 

36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36293
diff
changeset

74 
(* needed for SPASS's output format *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

75 
fun repair_bool_literal "true" = "c_True" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

76 
 repair_bool_literal "false" = "c_False" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

77 
fun repair_name pool "equal" = "c_equal" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

78 
 repair_name pool s = ugly_name pool s 
36392  79 
(* Generalized firstorder terms, which include file names, numbers, etc. *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

80 
(* The "x" argument is not strictly necessary, but without it Poly/ML loops 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

81 
forever at compile time. *) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

82 
fun parse_term pool x = 
36392  83 
(parse_quoted >> atom 
84 
 parse_integer >> SInt 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

85 
 $$ "$"  Symbol.scan_id >> (atom o repair_bool_literal) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

86 
 (Symbol.scan_id >> repair_name pool) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

87 
 Scan.optional ($$ "("  parse_terms pool  $$ ")") [] >> SBranch 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

88 
 $$ "("  parse_term pool  $$ ")" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

89 
 $$ "["  Scan.optional (parse_terms pool) []  $$ "]" >> slist_of) x 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

90 
and parse_terms pool x = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

91 
(parse_term pool ::: Scan.repeat ($$ ","  parse_term pool)) x 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

92 

36392  93 
fun negate_stree t = SBranch ("c_Not", [t]) 
94 
fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]); 

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

95 

36392  96 
(* Apply equal or notequal to a term. *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

97 
fun repair_predicate_term (t, NONE) = t 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

98 
 repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

99 
 repair_predicate_term (t1, SOME (SOME _, t2)) = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

100 
negate_stree (equate_strees t1 t2) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

101 
fun parse_predicate_term pool = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

102 
parse_term pool  Scan.option (Scan.option ($$ "!")  $$ "=" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

103 
 parse_term pool) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

105 
(*Literals can involve negation, = and !=.*) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

106 
fun parse_literal pool x = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

107 
($$ "~"  parse_literal pool >> negate_stree  parse_predicate_term pool) x 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

108 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

109 
fun parse_literals pool = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

110 
parse_literal pool ::: Scan.repeat ($$ ""  parse_literal pool) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

111 

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

112 
(*Clause: a list of literals separated by the disjunction sign*) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

113 
fun parse_clause pool = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

114 
$$ "("  parse_literals pool  $$ ")"  Scan.single (parse_literal pool) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

115 

36392  116 
fun ints_of_stree (SInt n) = cons n 
117 
 ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts 

118 
val parse_tstp_annotations = 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

119 
Scan.optional ($$ ","  parse_term NONE 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

120 
 Scan.option ($$ ","  parse_terms NONE) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

121 
>> (fn source => ints_of_stree source [])) [] 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

122 

b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

123 
(* <cnf_annotated> ::= cnf(<name>, <formula_role>, <cnf_formula> <annotations>). 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

124 
The <name> could be an identifier, but we assume integers. *) 
36392  125 
fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

126 
fun parse_tstp_line pool = 
36392  127 
(Scan.this_string "cnf"  $$ "(")  parse_integer  $$ "," 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

128 
 Symbol.scan_id  $$ ","  parse_clause pool  parse_tstp_annotations 
36392  129 
 $$ ")"  $$ "." 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

130 
>> retuple_tstp_line 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

131 

b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

132 
(**** PARSING OF SPASS OUTPUT ****) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

133 

36392  134 
(* SPASS returns clause references of the form "x.y". We ignore "y", whose role 
135 
is not clear anyway. *) 

136 
val parse_dot_name = parse_integer  $$ "."  parse_integer 

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

137 

36392  138 
val parse_spass_annotations = 
139 
Scan.optional ($$ ":"  Scan.repeat (parse_dot_name 

140 
 Scan.option ($$ ","))) [] 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

141 

36392  142 
(* It is not clear why some literals are followed by sequences of stars. We 
143 
ignore them. *) 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

144 
fun parse_starred_predicate_term pool = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

145 
parse_predicate_term pool  Scan.repeat ($$ "*"  $$ " ") 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

146 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

147 
fun parse_horn_clause pool = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

148 
Scan.repeat (parse_starred_predicate_term pool)  $$ ""  $$ ">" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

149 
 Scan.repeat (parse_starred_predicate_term pool) 
36392  150 
>> (fn ([], []) => [atom "c_False"] 
151 
 (clauses1, clauses2) => map negate_stree clauses1 @ clauses2) 

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

152 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

153 
(* Syntax: <name>[0:<inference><annotations>]  
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

154 
<cnf_formulas> > <cnf_formulas>. *) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

155 
fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

156 
fun parse_spass_proof_line pool = 
36392  157 
parse_integer  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 
158 
 parse_spass_annotations  $$ "]"  $$ ""  $$ "" 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

159 
 parse_horn_clause pool  $$ "." 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

160 
>> retuple_spass_proof_line 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

161 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

162 
fun parse_proof_line pool = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

163 
fst o (parse_tstp_line pool  parse_spass_proof_line pool) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

164 

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

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

166 

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

167 
exception STREE of stree; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

168 

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

169 
(*If string s has the prefix s1, return the result of deleting it.*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

170 
fun strip_prefix s1 s = 
31038  171 
if String.isPrefix s1 s 
35865  172 
then SOME (undo_ascii_of (String.extract (s, size s1, NONE))) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

174 

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

175 
(*Invert the table of translations between Isabelle and ATPs*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

176 
val type_const_trans_table_inv = 
35865  177 
Symtab.make (map swap (Symtab.dest type_const_trans_table)); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

178 

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

179 
fun invert_type_const c = 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

180 
case Symtab.lookup type_const_trans_table_inv c of 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

181 
SOME c' => c' 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

182 
 NONE => c; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

183 

36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

184 
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS); 
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

185 
fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

186 
fun make_var (b,T) = Var((b,0),T); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

187 

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

188 
(*Type variables are given the basic sort, HOL.type. Some will later be constrained 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

189 
by information from type literals, or by type inference.*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

190 
fun type_of_stree t = 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

191 
case t of 
36392  192 
SInt _ => raise STREE t 
193 
 SBranch (a,ts) => 

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

194 
let val Ts = map type_of_stree ts 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

195 
in 
35865  196 
case strip_prefix tconst_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

197 
SOME b => Type(invert_type_const b, Ts) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

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

199 
if not (null ts) then raise STREE t (*only tconsts have type arguments*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

200 
else 
35865  201 
case strip_prefix tfree_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

202 
SOME b => TFree("'" ^ b, HOLogic.typeS) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

203 
 NONE => 
35865  204 
case strip_prefix tvar_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

205 
SOME b => make_tvar b 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

206 
 NONE => make_tparam a (* Variable from the ATP, say "X1" *) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

208 

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

209 
(*Invert the table of translations between Isabelle and ATPs*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

210 
val const_trans_table_inv = 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

211 
Symtab.update ("fequal", "op =") 
35865  212 
(Symtab.make (map swap (Symtab.dest const_trans_table))); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

213 

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

214 
fun invert_const c = 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

215 
case Symtab.lookup const_trans_table_inv c of 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

216 
SOME c' => c' 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

217 
 NONE => c; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

218 

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

219 
(*The number of type arguments of a constant, zero if it's monomorphic*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

220 
fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s)); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

221 

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

222 
(*Generates a constant, given its type arguments*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

223 
fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts)); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

224 

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

225 
(*Firstorder translation. No types are known for variables. HOLogic.typeT should allow 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

226 
them to be inferred.*) 
22428  227 
fun term_of_stree args thy t = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

228 
case t of 
36392  229 
SInt _ => raise STREE t 
230 
 SBranch ("hBOOL", [t]) => term_of_stree [] thy t (*ignore hBOOL*) 

231 
 SBranch ("hAPP", [t, u]) => term_of_stree (u::args) thy t 

232 
 SBranch (a, ts) => 

35865  233 
case strip_prefix const_prefix a of 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

234 
SOME "equal" => 
35865  235 
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

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

237 
let val c = invert_const b 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

238 
val nterms = length ts  num_typargs thy c 
22428  239 
val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args) 
240 
(*Extra args from hAPP come AFTER any arguments given directly to the 

241 
constant.*) 

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

242 
val Ts = List.map type_of_stree (List.drop(ts,nterms)) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

243 
in list_comb(const_of thy (c, Ts), us) end 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

244 
 NONE => (*a variable, not a constant*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

245 
let val T = HOLogic.typeT 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

246 
val opr = (*a Free variable is typically a Skolem function*) 
35865  247 
case strip_prefix fixed_var_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

248 
SOME b => Free(b,T) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

249 
 NONE => 
35865  250 
case strip_prefix schematic_var_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

251 
SOME b => make_var (b,T) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

252 
 NONE => make_var (a,T) (* Variable from the ATP, say "X1" *) 
23519  253 
in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

254 

36392  255 
(* Type class literal applied to a type. Returns triple of polarity, class, 
256 
type. *) 

257 
fun constraint_of_stree pol (SBranch ("c_Not", [t])) = 

258 
constraint_of_stree (not pol) t 

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

259 
 constraint_of_stree pol t = case t of 
36392  260 
SInt _ => raise STREE t 
261 
 SBranch (a, ts) => 

35865  262 
(case (strip_prefix class_prefix a, map type_of_stree ts) of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

263 
(SOME b, [T]) => (pol, b, T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

264 
 _ => raise STREE t); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

265 

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

266 
(** Accumulate type constraints in a clause: negative type literals **) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

267 

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

268 
fun addix (key,z) = Vartab.map_default (key,[]) (cons z); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

269 

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

270 
fun add_constraint ((false, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

271 
 add_constraint ((false, cl, TVar(ix,_)), vt) = addix (ix,cl) vt 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

272 
 add_constraint (_, vt) = vt; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

273 

36392  274 
(* Final treatment of the list of "real" literals from a clause. *) 
275 
fun finish [] = 

276 
(* No "real" literals means only type information. *) 

277 
HOLogic.true_const 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

278 
 finish lits = 
36392  279 
case filter_out (curry (op =) HOLogic.false_const) lits of 
280 
[] => HOLogic.false_const 

281 
 xs => foldr1 HOLogic.mk_disj (rev xs); 

22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

282 

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

283 
(*Accumulate sort constraints in vt, with "real" literals in lits.*) 
32994  284 
fun lits_of_strees _ (vt, lits) [] = (vt, finish lits) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

285 
 lits_of_strees ctxt (vt, lits) (t::ts) = 
22012
adf68479ae1b
Proof.context now sent to watcher and used in type inference step of proof reconstruction
paulson
parents:
21999
diff
changeset

286 
lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

287 
handle STREE _ => 
22428  288 
lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

289 

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

290 
(*Update TVars/TFrees with detected sort constraints.*) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

292 
let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) 
33035  293 
 tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) 
294 
 tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1))) 

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

295 
fun tmsubst (Const (a, T)) = Const (a, tysubst T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

296 
 tmsubst (Free (a, T)) = Free (a, tysubst T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

297 
 tmsubst (Var (xi, T)) = Var (xi, tysubst T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

298 
 tmsubst (t as Bound _) = t 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

299 
 tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

300 
 tmsubst (t $ u) = tmsubst t $ tmsubst u; 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

301 
in not (Vartab.is_empty vt) ? tmsubst end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

302 

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

303 
(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints. 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

304 
vt0 holds the initial sort constraints, from the conjecture clauses.*) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

305 
fun clause_of_strees ctxt vt ts = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

306 
let val (vt, dt) = lits_of_strees ctxt (vt, []) ts in 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

307 
dt > repair_sorts vt > TypeInfer.constrain HOLogic.boolT 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

308 
> Syntax.check_term ctxt 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

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

310 

29268  311 
fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

312 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

313 
fun decode_proof_step vt0 (name, ts, deps) ctxt = 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

314 
let val cl = clause_of_strees ctxt vt0 ts in 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

315 
((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

317 

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

318 
(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

319 

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

320 
fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

321 
 add_tfree_constraint (_, vt) = vt; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

322 

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

323 
fun tfree_constraints_of_clauses vt [] = vt 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

324 
 tfree_constraints_of_clauses vt ([lit]::tss) = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

325 
(tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

326 
handle STREE _ => (*not a positive type constraint: ignore*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

327 
tfree_constraints_of_clauses vt tss) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

328 
 tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

329 

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

330 

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

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

332 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

333 
fun decode_proof_steps ctxt tuples = 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

334 
let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

335 
#1 (fold_map (decode_proof_step vt0) tuples ctxt) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

337 

23519  338 
(** Finding a matching assumption. The literals may be permuted, and variable names 
36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

339 
may disagree. We must try all combinations of literals (quadratic!) and 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

340 
match the variable names consistently. **) 
23519  341 

35865  342 
fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t)) = 
23519  343 
strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t)) 
344 
 strip_alls_aux _ t = t; 

345 

346 
val strip_alls = strip_alls_aux 0; 

347 

36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

348 
exception MATCH_LITERAL of unit 
22012
adf68479ae1b
Proof.context now sent to watcher and used in type inference step of proof reconstruction
paulson
parents:
21999
diff
changeset

349 

36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

350 
(* Remark 1: Ignore types. They are not to be trusted. 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

351 
Remark 2: Ignore order of arguments for equality. SPASS sometimes swaps 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

352 
them for no apparent reason. *) 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

353 
fun match_literal (Const (@{const_name "op ="}, _) $ t1 $ u1) 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

354 
(Const (@{const_name "op ="}, _) $ t2 $ u2) env = 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

355 
(env > match_literal t1 t2 > match_literal u1 u2 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

356 
handle MATCH_LITERAL () => 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

357 
env > match_literal t1 u2 > match_literal u1 t2) 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

358 
 match_literal (t1 $ u1) (t2 $ u2) env = 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

359 
env > match_literal t1 t2 > match_literal u1 u2 
31038  360 
 match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env = 
36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

361 
match_literal t1 t2 env 
31038  362 
 match_literal (Bound i1) (Bound i2) env = 
36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

363 
if i1=i2 then env else raise MATCH_LITERAL () 
31038  364 
 match_literal (Const(a1,_)) (Const(a2,_)) env = 
36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

365 
if a1=a2 then env else raise MATCH_LITERAL () 
31038  366 
 match_literal (Free(a1,_)) (Free(a2,_)) env = 
36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

367 
if a1=a2 then env else raise MATCH_LITERAL () 
23519  368 
 match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env 
36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

369 
 match_literal _ _ _ = raise MATCH_LITERAL () 
23519  370 

36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

371 
(* Checking that all variable associations are unique. The list "env" contains 
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

372 
no repetitions, but does it contain say (x, y) and (y, y)? *) 
31038  373 
fun good env = 
23519  374 
let val (xs,ys) = ListPair.unzip env 
375 
in not (has_duplicates (op=) xs orelse has_duplicates (op=) ys) end; 

376 

377 
(*Match one list of literals against another, ignoring types and the order of 

378 
literals. Sorting is unreliable because we don't have types or variable names.*) 

379 
fun matches_aux _ [] [] = true 

380 
 matches_aux env (lit::lits) ts = 

381 
let fun match1 us [] = false 

382 
 match1 us (t::ts) = 

383 
let val env' = match_literal lit t env 

31038  384 
in (good env' andalso matches_aux env' lits (us@ts)) orelse 
385 
match1 (t::us) ts 

23519  386 
end 
36293
e6db3ba0b61d
handle SPASS's equality predicate correctly in Isar proof reconstruction
blanchet
parents:
36291
diff
changeset

387 
handle MATCH_LITERAL () => match1 (t::us) ts 
31038  388 
in match1 [] ts end; 
23519  389 

390 
(*Is this length test useful?*) 

31038  391 
fun matches (lits1,lits2) = 
392 
length lits1 = length lits2 andalso 

23519  393 
matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2); 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

394 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

395 
fun permuted_clause t = 
24958  396 
let val lits = HOLogic.disjuncts t 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

397 
fun perm [] = NONE 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

398 
 perm (ctm::ctms) = 
24958  399 
if matches (lits, HOLogic.disjuncts (HOLogic.dest_Trueprop (strip_alls ctm))) 
23519  400 
then SOME ctm else perm ctms 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

401 
in perm end; 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

402 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

403 
(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

404 
ATP may have their literals reordered.*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

405 
fun isar_proof_body ctxt sorts ctms = 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

406 
let 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

407 
val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n") 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

408 
val string_of_term = 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

409 
PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN) 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

410 
(print_mode_value ())) 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

411 
(Syntax.string_of_term ctxt) 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

412 
fun have_or_show "show" _ = " show \"" 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

413 
 have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \"" 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

414 
fun do_line _ (lname, t, []) = 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

415 
(* No depedencies: it's a conjecture clause, with no proof. *) 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

416 
(case permuted_clause t ctms of 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

417 
SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

418 
 NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body", 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

419 
[t])) 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

420 
 do_line have (lname, t, deps) = 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

421 
have_or_show have lname ^ 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

422 
string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^ 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

423 
"\"\n by (metis " ^ space_implode " " deps ^ ")\n" 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

424 
fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)] 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

425 
 do_lines ((lname, t, deps) :: lines) = 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

426 
do_line "have" (lname, t, deps) :: do_lines lines 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

427 
in setmp_CRITICAL show_sorts sorts do_lines end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

428 

35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

429 
fun unequal t (_, t', _) = not (t aconv t'); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

430 

22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

431 
(*No "real" literals means only type information*) 
23519  432 
fun eq_types t = t aconv HOLogic.true_const; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

433 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22728
diff
changeset

434 
fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

435 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

436 
fun replace_deps (old:int, new) (lno, t, deps) = 
33042  437 
(lno, t, List.foldl (uncurry (union (op =))) [] (map (replace_dep (old, new)) deps)); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

438 

22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

439 
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

440 
only in type information.*) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

441 
fun add_proof_line thm_names (lno, t, []) lines = 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

442 
(* No dependencies: axiom or conjecture clause *) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

443 
if is_axiom thm_names lno then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

444 
(* Axioms are not proof lines *) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

445 
if eq_types t then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

446 
(* Must be clsrel/clsarity: type information, so delete refs to it *) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

447 
map (replace_deps (lno, [])) lines 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

448 
else 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

449 
(case take_prefix (unequal t) lines of 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

450 
(_,[]) => lines (*no repetition of proof line*) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

451 
 (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

452 
pre @ map (replace_deps (lno', [lno])) post) 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

453 
else 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

454 
(lno, t, []) :: lines 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

455 
 add_proof_line _ (lno, t, deps) lines = 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

456 
if eq_types t then (lno, t, deps) :: lines 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

457 
(*Type information will be deleted later; skip repetition test.*) 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

458 
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*) 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

459 
case take_prefix (unequal t) lines of 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

460 
(_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*) 
32994  461 
 (pre, (lno', t', _) :: post) => 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

462 
(lno, t', deps) :: (*repetition: replace later line by earlier one*) 
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

463 
(pre @ map (replace_deps (lno', [lno])) post); 
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

464 

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

465 
(*Recursively delete empty lines (type information) from the proof.*) 
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

466 
fun add_nonnull_prfline ((lno, t, []), lines) = (*no dependencies, so a conjecture clause*) 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

467 
if eq_types t (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

468 
then delete_dep lno lines 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

469 
else (lno, t, []) :: lines 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

470 
 add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines 
30190  471 
and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines); 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

472 

35865  473 
fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22728
diff
changeset

474 
 bad_free _ = false; 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22728
diff
changeset

475 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

476 
(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies. 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

477 
To further compress proofs, setting modulus:=n deletes every nth line, and nlines 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

478 
counts the number of proof lines processed so far. 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

479 
Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline" 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

480 
phase may delete some dependencies, hence this phase comes later.*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

481 
fun add_wanted_prfline ctxt _ ((lno, t, []), (nlines, lines)) = 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

482 
(nlines, (lno, t, []) :: lines) (*conjecture clauses must be kept*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

483 
 add_wanted_prfline ctxt modulus ((lno, t, deps), (nlines, lines)) = 
29272  484 
if eq_types t orelse not (null (Term.add_tvars t [])) orelse 
29268  485 
exists_subterm bad_free t orelse 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

486 
(not (null lines) andalso (*final line can't be deleted for these reasons*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

487 
(length deps < 2 orelse nlines mod modulus <> 0)) 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

488 
then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*) 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

489 
else (nlines+1, (lno, t, deps) :: lines); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

490 

21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

491 
(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

492 
fun stringify_deps thm_names deps_map [] = [] 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

493 
 stringify_deps thm_names deps_map ((lno, t, deps) :: lines) = 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

494 
if is_axiom thm_names lno then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

495 
(Vector.sub(thm_names,lno1), t, []) :: stringify_deps thm_names deps_map lines 
21979
80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

496 
else let val lname = Int.toString (length deps_map) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

497 
fun fix lno = if is_axiom thm_names lno 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

498 
then SOME(Vector.sub(thm_names,lno1)) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

499 
else AList.lookup (op =) deps_map lno; 
32952  500 
in (lname, t, map_filter fix (distinct (op=) deps)) :: 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

501 
stringify_deps thm_names ((lno,lname)::deps_map) lines 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

503 

36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

504 
fun isar_proof_start i = 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

505 
(if i = 1 then "" else "prefer " ^ string_of_int i ^ "\n") ^ 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

506 
"proof (neg_clausify)\n"; 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

507 
fun isar_fixes [] = "" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

508 
 isar_fixes ts = " fix " ^ space_implode " " ts ^ "\n"; 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

509 
fun isar_proof_end 1 = "qed" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

510 
 isar_proof_end _ = "next" 
21979
80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

511 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

512 
fun isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal i = 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

513 
let 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

514 
val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n") 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

515 
val tuples = map (parse_proof_line pool o explode) cnfs 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

516 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

517 
Int.toString (length tuples) ^ " tuples extracted\n") 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

518 
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

519 
val raw_lines = 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

520 
fold_rev (add_proof_line thm_names) (decode_proof_steps ctxt tuples) [] 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

521 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

522 
Int.toString (length raw_lines) ^ " raw_lines extracted\n") 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

523 
val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

524 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

525 
Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

526 
val (_, lines) = List.foldr (add_wanted_prfline ctxt modulus) (0,[]) nonnull_lines 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

527 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

528 
Int.toString (length lines) ^ " lines extracted\n") 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

529 
val (ccls, fixes) = neg_conjecture_clauses ctxt goal i 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

530 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

531 
Int.toString (length ccls) ^ " conjecture clauses\n") 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

532 
val ccls = map forall_intr_vars ccls 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

533 
val _ = app (fn th => trace_proof_msg 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

534 
(fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

535 
val body = isar_proof_body ctxt sorts (map prop_of ccls) 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

536 
(stringify_deps thm_names [] lines) 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

537 
val n = Logic.count_prems (prop_of goal) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

538 
val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: finishing\n") 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

539 
in 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

540 
isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^ 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

541 
isar_proof_end n ^ "\n" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

542 
end 
36288  543 
handle STREE _ => raise Fail "Cannot parse ATP output"; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

544 

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

545 

33310  546 
(* === EXTRACTING LEMMAS === *) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

547 
(* A list consisting of the first number in each line is returned. 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

548 
TPTP: Interesting lines have the form "cnf(108, axiom, ...)", where the 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

549 
number (108) is extracted. 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

550 
DFG: Lines have the form "108[0:Inp] ...", where the first number (108) is 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

551 
extracted. *) 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36293
diff
changeset

552 
fun get_step_nums proof = 
35865  553 
let 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

554 
val toks = String.tokens (not o is_ident_char) 
35865  555 
fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

556 
 inputno ("cnf" :: ntok :: "negated_conjecture" :: _) = 
35865  557 
Int.fromString ntok 
36392  558 
(* SPASS's output format *) 
559 
 inputno (ntok :: "0" :: "Inp" :: _) = Int.fromString ntok 

35865  560 
 inputno _ = NONE 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36293
diff
changeset

561 
in map_filter (inputno o toks) (split_lines proof) end 
33310  562 

563 
(*Used to label theorems chained into the sledgehammer call*) 

564 
val chained_hint = "CHAINED"; 

35865  565 
val kill_chained = filter_out (curry (op =) chained_hint) 
566 

36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

567 
fun apply_command _ 1 = "by " 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

568 
 apply_command 1 _ = "apply " 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

569 
 apply_command i _ = "prefer " ^ string_of_int i ^ " apply " 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

570 
fun metis_command i n [] = 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

571 
apply_command i n ^ "metis" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

572 
 metis_command i n xs = 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

573 
apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

574 
fun metis_line i n xs = 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

575 
"Try this command: " ^ 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

576 
Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

577 
fun minimize_line _ [] = "" 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

578 
 minimize_line minimize_command facts = 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

579 
case minimize_command facts of 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

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

581 
 command => 
36065  582 
"To minimize the number of lemmas, try this command: " ^ 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

583 
Markup.markup Markup.sendback command ^ ".\n" 
31840
beeaa1ed1f47
check if conjectures have been used in proof
immler@in.tum.de
parents:
31479
diff
changeset

584 

36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

585 
fun metis_proof_text (minimize_command, proof, thm_names, goal, i) = 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

586 
let 
36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36225
diff
changeset

587 
val lemmas = 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36293
diff
changeset

588 
proof > get_step_nums 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

589 
> filter (is_axiom thm_names) 
36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36225
diff
changeset

590 
> map (fn i => Vector.sub (thm_names, i  1)) 
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36225
diff
changeset

591 
> filter (fn x => x <> "??.unknown") 
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36225
diff
changeset

592 
> sort_distinct string_ord 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

593 
val n = Logic.count_prems (prop_of goal) 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

594 
val xs = kill_chained lemmas 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

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

596 
(metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

597 
end 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
30874
diff
changeset

598 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

599 
val is_proof_line = String.isPrefix "cnf(" orf String.isSubstring "" 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

600 

b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

601 
fun do_space c = if Char.isSpace c then "" else str c 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

602 

b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

603 
fun strip_spaces_in_list [] = "" 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

604 
 strip_spaces_in_list [c1] = do_space c1 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

605 
 strip_spaces_in_list [c1, c2] = do_space c1 ^ do_space c2 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

606 
 strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

607 
if Char.isSpace c1 then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

608 
strip_spaces_in_list (c2 :: c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

609 
else if Char.isSpace c2 then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

610 
if Char.isSpace c3 then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

611 
strip_spaces_in_list (c1 :: c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

612 
else 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

613 
str c1 ^ 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

614 
(if is_ident_char c1 andalso is_ident_char c3 then " " else "") ^ 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

615 
strip_spaces_in_list (c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

616 
else 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

617 
str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

618 

b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

619 
val strip_spaces = strip_spaces_in_list o String.explode 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

620 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

621 
fun isar_proof_text pool debug modulus sorts ctxt 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

622 
(minimize_command, proof, thm_names, goal, i) = 
33310  623 
let 
36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36293
diff
changeset

624 
val cnfs = proof > split_lines > map strip_spaces > filter is_proof_line 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

625 
val (one_line_proof, lemma_names) = 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

626 
metis_proof_text (minimize_command, proof, thm_names, goal, i) 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

627 
val tokens = String.tokens (fn c => c = #" ") one_line_proof 
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

628 
fun isar_proof_for () = 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

629 
case isar_proof_from_atp_proof pool modulus sorts ctxt cnfs thm_names goal 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

630 
i of 
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

631 
"" => "" 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

632 
 isar_proof => 
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

633 
"\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

634 
val isar_proof = 
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

635 
if member (op =) tokens chained_hint then 
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

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

637 
else if debug then 
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

638 
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

639 
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

640 
try isar_proof_for () 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

641 
> the_default "Warning: The Isar proof construction failed.\n" 
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

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

643 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

644 
fun proof_text isar_proof pool debug modulus sorts ctxt = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

645 
if isar_proof then isar_proof_text pool debug modulus sorts ctxt 
36288  646 
else metis_proof_text 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

647 

31038  648 
end; 