author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47055  16e2633f3b4b 
child 47606  06dde48a1503 
permissions  rwrr 
46321  1 
(* Title: HOL/TPTP/atp_theory_export.ML 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

2 
Author: Jasmin Blanchette, TU Muenchen 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

3 
Copyright 2011 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

4 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

5 
Export Isabelle theories as firstorder TPTP inferences, exploiting 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

6 
Sledgehammer's translation. 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

7 
*) 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

8 

46321  9 
signature ATP_THEORY_EXPORT = 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

10 
sig 
45305  11 
type atp_format = ATP_Problem.atp_format 
12 

43494
13eefebbc4cb
make sure that enough type information is generated  because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents:
43479
diff
changeset

13 
val theorems_mentioned_in_proof_term : 
13eefebbc4cb
make sure that enough type information is generated  because the exported "lemma"s are also used as "conjecture", we can't optimize type information based on polarity
blanchet
parents:
43479
diff
changeset

14 
string list option > thm > string list 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

15 
val generate_tptp_graph_file_for_theory : 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

16 
Proof.context > theory > string > unit 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

17 
val generate_tptp_inference_file_for_theory : 
45305  18 
Proof.context > theory > atp_format > string > string > unit 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

19 
end; 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

20 

46321  21 
structure ATP_Theory_Export : ATP_THEORY_EXPORT = 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

22 
struct 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

23 

43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

24 
open ATP_Problem 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

25 
open ATP_Proof 
46320  26 
open ATP_Problem_Generate 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

27 
open ATP_Systems 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

28 

43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

29 
val fact_name_of = prefix fact_prefix o ascii_of 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

30 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

31 
fun facts_of thy = 
46734  32 
let val ctxt = Proof_Context.init_global thy in 
33 
Sledgehammer_Filter.all_facts ctxt false 

34 
Symtab.empty true [] [] 

35 
(Sledgehammer_Filter.clasimpset_rule_table_of ctxt) 

36 
> filter (curry (op =) @{typ bool} o fastype_of 

37 
o Object_Logic.atomize_term thy o prop_of o snd) 

38 
end 

42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

39 

43468
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset

40 
(* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few 
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset

41 
fixes that seem to be missing over there; or maybe the two code portions are 
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset

42 
not doing the same? *) 
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset

43 
fun fold_body_thms thm_name all_names f = 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

44 
let 
43468
c768f7adb711
fixed silly ATP exporter bug: if the proof of lemma A relies on B and C, and the proof of B relies on C, return {B, C}, not {B}, as the set of dependencies
blanchet
parents:
43400
diff
changeset

45 
fun app n (PBody {thms, ...}) = 
43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

46 
thms > fold (fn (_, (name, prop, body)) => fn x => 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

47 
let 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

48 
val body' = Future.join body 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

49 
val n' = 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

50 
n + (if name = "" orelse 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

51 
(is_some all_names andalso 
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset

52 
not (member (op =) (the all_names) name)) orelse 
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset

53 
(* uncommon case where the proved theorem occurs twice 
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset

54 
(e.g., "Transitive_Closure.trancl_into_trancl") *) 
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset

55 
n = 1 andalso name = thm_name then 
43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

56 
0 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

57 
else 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

58 
1) 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

59 
val x' = x > n' <= 1 ? app n' body' 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

60 
in (x' > n = 1 ? f (name, prop, body')) end) 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

61 
in fold (app 0) end 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

62 

43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

63 
fun theorems_mentioned_in_proof_term all_names thm = 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

64 
let 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

65 
fun collect (s, _, _) = if s <> "" then insert (op =) s else I 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

66 
val names = 
43498
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset

67 
[] > fold_body_thms (Thm.get_name_hint thm) all_names collect 
75caf7e4302e
peel off two or more layers in exceptional cases where the proof term refers to the proved theorems twice with the same name (e.g., "Transitive_Closure.trancl_into_trancl")
blanchet
parents:
43494
diff
changeset

68 
[Thm.proof_body_of thm] 
43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

69 
> map fact_name_of 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

70 
in names end 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

71 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

72 
fun interesting_const_names ctxt = 
43276  73 
let val thy = Proof_Context.theory_of ctxt in 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

74 
Sledgehammer_Filter.const_names_in_fact thy 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

75 
(Sledgehammer_Provers.is_built_in_const_for_prover ctxt eN) 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

76 
end 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

77 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

78 
fun generate_tptp_graph_file_for_theory ctxt thy file_name = 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

79 
let 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

80 
val path = file_name > Path.explode 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

81 
val _ = File.write path "" 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

82 
val axioms = Theory.all_axioms_of thy > map fst 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

83 
fun do_thm thm = 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

84 
let 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

85 
val name = Thm.get_name_hint thm 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

86 
val s = 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

87 
"[" ^ Thm.legacy_get_kind thm ^ "] " ^ 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

88 
(if member (op =) axioms name then "A" else "T") ^ " " ^ 
43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

89 
prefix fact_prefix (ascii_of name) ^ ": " ^ 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

90 
commas (theorems_mentioned_in_proof_term NONE thm) ^ "; " ^ 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

91 
commas (map (prefix const_prefix o ascii_of) 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

92 
(interesting_const_names ctxt (Thm.prop_of thm))) ^ " \n" 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

93 
in File.append path s end 
43245  94 
val thms = facts_of thy > map snd 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

95 
val _ = map do_thm thms 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

96 
in () end 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

97 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

98 
fun inference_term [] = NONE 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

99 
 inference_term ss = 
43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

100 
ATerm ("inference", 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

101 
[ATerm ("isabelle", []), 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

102 
ATerm (tptp_empty_list, []), 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

103 
ATerm (tptp_empty_list, map (fn s => ATerm (s, [])) ss)]) 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

104 
> SOME 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

105 
fun inference infers ident = 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

106 
these (AList.lookup (op =) infers ident) > inference_term 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

107 
fun add_inferences_to_problem_line infers 
46406  108 
(Formula (ident, Axiom, phi, NONE, tms)) = 
109 
Formula (ident, Lemma, phi, inference infers ident, tms) 

42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

110 
 add_inferences_to_problem_line _ line = line 
43996  111 
fun add_inferences_to_problem infers = 
112 
map (apsnd (map (add_inferences_to_problem_line infers))) 

42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

113 

43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

114 
fun ident_of_problem_line (Decl (ident, _, _)) = ident 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

115 
 ident_of_problem_line (Formula (ident, _, _, _, _)) = ident 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

116 

45305  117 
fun run_some_atp ctxt format problem = 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

118 
let 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

119 
val thy = Proof_Context.theory_of ctxt 
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47038
diff
changeset

120 
val prob_file = File.tmp_path (Path.explode "prob") 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

121 
val atp = case format of DFG _ => spass_newN  _ => eN 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

122 
val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

123 
val ord = effective_term_order ctxt atp 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

124 
val _ = problem > lines_for_atp_problem format ord (K []) 
46442
1e07620d724c
added possibility of generating KBO weights to DFG problems
blanchet
parents:
46409
diff
changeset

125 
> File.write_list prob_file 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

126 
val command = 
47055
16e2633f3b4b
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
blanchet
parents:
47038
diff
changeset

127 
File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^ 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

128 
" " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^ 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

129 
File.shell_path prob_file 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

130 
in 
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43828
diff
changeset

131 
TimeLimit.timeLimit (seconds 0.3) Isabelle_System.bash_output command 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

132 
> fst 
47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

133 
> extract_tstplike_proof_and_outcome false true proof_delims known_failures 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

134 
> snd 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

135 
end 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

136 
handle TimeLimit.TimeOut => SOME TimedOut 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

137 

a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

138 
val likely_tautology_prefixes = 
43569
b342cd125533
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
blanchet
parents:
43566
diff
changeset

139 
[@{theory HOL}, @{theory Meson}, @{theory ATP}, @{theory Metis}] 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

140 
> map (fact_name_of o Context.theory_name) 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

141 

45305  142 
fun is_problem_line_tautology ctxt format (Formula (ident, _, phi, _, _)) = 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

143 
exists (fn prefix => String.isPrefix prefix ident) 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

144 
likely_tautology_prefixes andalso 
45305  145 
is_none (run_some_atp ctxt format 
46406  146 
[(factsN, [Formula (ident, Conjecture, phi, NONE, [])])]) 
45305  147 
 is_problem_line_tautology _ _ _ = false 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

148 

43499  149 
fun order_facts ord = sort (ord o pairself ident_of_problem_line) 
150 
fun order_problem_facts _ [] = [] 

151 
 order_problem_facts ord ((heading, lines) :: problem) = 

152 
if heading = factsN then (heading, order_facts ord lines) :: problem 

153 
else (heading, lines) :: order_problem_facts ord problem 

154 

45305  155 
(* A fairly random selection of types used for monomorphizing. *) 
156 
val ground_types = 

157 
[@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, 

158 
@{typ unit}] 

159 

160 
fun ground_type_for_tvar _ [] tvar = 

161 
raise TYPE ("ground_type_for_sorts", [TVar tvar], []) 

162 
 ground_type_for_tvar thy (T :: Ts) tvar = 

163 
if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T 

164 
else ground_type_for_tvar thy Ts tvar 

165 

166 
fun monomorphize_term ctxt t = 

167 
let val thy = Proof_Context.theory_of ctxt in 

168 
t > map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) 

169 
handle TYPE _ => @{prop True} 

170 
end 

171 

172 
fun generate_tptp_inference_file_for_theory ctxt thy format type_enc file_name = 

42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

173 
let 
46301  174 
val type_enc = type_enc > type_enc_from_string Strict 
45305  175 
> adjust_type_enc format 
176 
val mono = polymorphism_of_type_enc type_enc <> Polymorphic 

42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

177 
val path = file_name > Path.explode 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

178 
val _ = File.write path "" 
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset

179 
val facts = facts_of thy 
45551  180 
val atp_problem = 
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset

181 
facts 
45305  182 
> map (fn ((_, loc), th) => 
183 
((Thm.get_name_hint th, loc), 

184 
th > prop_of > mono ? monomorphize_term ctxt)) 

46365  185 
> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false 
46409
d4754183ccce
made option available to users (mostly for experiments)
blanchet
parents:
46406
diff
changeset

186 
false true [] @{prop False} 
45551  187 
> #1 
43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

188 
val atp_problem = 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

189 
atp_problem 
45305  190 
> map (apsnd (filter_out (is_problem_line_tautology ctxt format))) 
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset

191 
val all_names = facts > map (Thm.get_name_hint o snd) 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

192 
val infers = 
43576
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset

193 
facts > map (fn (_, th) => 
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset

194 
(fact_name_of (Thm.get_name_hint th), 
ebeda6275027
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical
blanchet
parents:
43572
diff
changeset

195 
theorems_mentioned_in_proof_term (SOME all_names) th)) 
43479
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

196 
val all_atp_problem_names = 
5af1abc13c1f
only refer to facts found in TPTP file  e.g. facts that simplify to true are excluded
blanchet
parents:
43468
diff
changeset

197 
atp_problem > maps (map ident_of_problem_line o snd) 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

198 
val infers = 
43499  199 
infers > filter (member (op =) all_atp_problem_names o fst) 
200 
> map (apsnd (filter (member (op =) all_atp_problem_names))) 

201 
val ordered_names = 

202 
String_Graph.empty 

203 
> fold (String_Graph.new_node o rpair ()) all_atp_problem_names 

204 
> fold (fn (to, froms) => 

43566
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

205 
fold (fn from => String_Graph.add_edge (from, to)) froms) 
a818d5a34cca
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
blanchet
parents:
43499
diff
changeset

206 
infers 
43499  207 
> String_Graph.topological_order 
208 
val order_tab = 

209 
Symtab.empty 

210 
> fold (Symtab.insert (op =)) 

211 
(ordered_names ~~ (1 upto length ordered_names)) 

212 
val name_ord = int_ord o pairself (the o Symtab.lookup order_tab) 

213 
val atp_problem = 

45305  214 
atp_problem 
215 
> (case format of DFG _ => I  _ => add_inferences_to_problem infers) 

216 
> order_problem_facts name_ord 

47038
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

217 
val ord = effective_term_order ctxt eN (* dummy *) 
2409b484e1cc
continued implementation of term ordering attributes
blanchet
parents:
46734
diff
changeset

218 
val ss = lines_for_atp_problem format ord (K []) atp_problem 
42602
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

219 
val _ = app (File.append path) ss 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

220 
in () end 
a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

221 

a2db47fa015e
added TPTP exporter facility  useful to do experiments with machine learning
blanchet
parents:
diff
changeset

222 
end; 