author  blanchet 
Mon, 04 Apr 2011 18:53:35 +0200  
changeset 42227  662b50b7126f 
parent 42180  a6c141925a8a 
child 42232  5f2a555b15d6 
permissions  rwrr 
40114  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

2 
Author: Fabian Immler, TU Muenchen 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

3 
Author: Makarius 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

4 
Author: Jasmin Blanchette, TU Muenchen 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

5 

39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39452
diff
changeset

6 
Translation of HOL to FOL for Sledgehammer. 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

7 
*) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

8 

40068  9 
signature SLEDGEHAMMER_ATP_TRANSLATE = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

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

11 
type 'a fo_term = 'a ATP_Problem.fo_term 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

12 
type 'a problem = 'a ATP_Problem.problem 
40114  13 
type translated_formula 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

14 

41134  15 
datatype type_system = 
16 
Tags of bool  

17 
Preds of bool  

18 
Const_Args  

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

19 
Mangled  
41134  20 
No_Types 
21 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

22 
val precise_overloaded_args : bool Unsynchronized.ref 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

23 
val fact_prefix : string 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

24 
val conjecture_prefix : string 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

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

26 
val num_atp_type_args : theory > type_system > string > int 
41088  27 
val translate_atp_fact : 
41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

28 
Proof.context > bool > (string * 'a) * thm 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

29 
> translated_formula option * ((string * 'a) * thm) 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

30 
val unmangled_const : string > string * string fo_term list 
40059
6ad9081665db
use consistent terminology in Sledgehammer: "prover = ATP or SMT solver or ..."
blanchet
parents:
39975
diff
changeset

31 
val prepare_atp_problem : 
41134  32 
Proof.context > bool > bool > type_system > bool > term list > term 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

33 
> (translated_formula option * ((string * 'a) * thm)) list 
38818
61cf050f8b2e
improve SPASS hack, when a clause comes from several facts
blanchet
parents:
38752
diff
changeset

34 
> string problem * string Symtab.table * int * (string * 'a) list vector 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

35 
val atp_problem_weights : string problem > (string * real) list 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

36 
end; 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

37 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

38 
structure Sledgehammer_ATP_Translate : SLEDGEHAMMER_ATP_TRANSLATE = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

39 
struct 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

40 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

41 
open ATP_Problem 
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39452
diff
changeset

42 
open Metis_Translate 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

43 
open Sledgehammer_Util 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

44 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

45 
(* FIXME: Remove references once appropriate defaults have been determined 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

46 
empirically. *) 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

47 
val precise_overloaded_args = Unsynchronized.ref false 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

48 

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

49 
val fact_prefix = "fact_" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

50 
val conjecture_prefix = "conj_" 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

51 
val helper_prefix = "help_" 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

52 
val class_rel_clause_prefix = "clrel_"; 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

53 
val arity_clause_prefix = "arity_" 
39975
7c50d5ca5c04
avoid generating several formulas with the same name ("tfrees")
blanchet
parents:
39954
diff
changeset

54 
val tfree_prefix = "tfree_" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

55 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

56 
(* Freshness almost guaranteed! *) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

57 
val sledgehammer_weak_prefix = "Sledgehammer:" 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

58 

40114  59 
type translated_formula = 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

60 
{name: string, 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

61 
kind: kind, 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

62 
combformula: (name, combterm) formula, 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

63 
ctypes_sorts: typ list} 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

64 

41134  65 
datatype type_system = 
66 
Tags of bool  

67 
Preds of bool  

68 
Const_Args  

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

69 
Mangled  
41134  70 
No_Types 
71 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

72 
fun types_dangerous_types (Tags _) = true 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

73 
 types_dangerous_types (Preds _) = true 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

74 
 types_dangerous_types _ = false 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

75 

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

76 
(* This is an approximation. If it returns "true" for a constant that isn't 
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

77 
overloaded (i.e., that has one uniform definition), needless clutter is 
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

78 
generated; if it returns "false" for an overloaded constant, the ATP gets a 
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

79 
license to do unsound reasoning if the type system is "overloaded_args". *) 
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

80 
fun is_overloaded thy s = 
41748
657712cc8847
fix handling of "fequal" in generated ATP problems  the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)
blanchet
parents:
41726
diff
changeset

81 
not (s = @{const_name HOL.eq}) andalso 
657712cc8847
fix handling of "fequal" in generated ATP problems  the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)
blanchet
parents:
41726
diff
changeset

82 
not (s = @{const_name Metis.fequal}) andalso 
657712cc8847
fix handling of "fequal" in generated ATP problems  the bug was visible if "explicit_apply" was on and "singleton_conv" is one of the facts being translated, as it resulted in an arity error in the ATP (e.g., E)
blanchet
parents:
41726
diff
changeset

83 
(not (!precise_overloaded_args) orelse s = @{const_name finite} orelse 
41147
0e1903273712
fix translation of higherorder equality ("fequal") if "precise_overloaded_args" is "true"
blanchet
parents:
41145
diff
changeset

84 
length (Defs.specifications_of (Theory.defs_of thy) s) > 1) 
41136
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

85 

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

86 
fun needs_type_args thy type_sys s = 
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

87 
case type_sys of 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

88 
Tags full_types => not full_types andalso is_overloaded thy s 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

89 
 Preds _ => is_overloaded thy s (* FIXME: could be more precise *) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

90 
 Const_Args => is_overloaded thy s 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

92 
 No_Types => false 
30bedf58b177
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
blanchet
parents:
41134
diff
changeset

93 

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

94 
datatype type_arg_policy = No_Type_Args  Explicit_Type_Args  Mangled_Types 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

95 

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

96 
fun type_arg_policy thy type_sys s = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

97 
if needs_type_args thy type_sys s then 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

98 
if type_sys = Mangled then Mangled_Types else Explicit_Type_Args 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

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

101 

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

102 
fun num_atp_type_args thy type_sys s = 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

103 
if type_arg_policy thy type_sys s = Explicit_Type_Args then 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

104 
num_type_args thy s 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

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

107 

41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

108 
fun atp_type_literals_for_types type_sys Ts = 
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

109 
if type_sys = No_Types then [] else type_literals_for_types Ts 
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

110 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

111 
fun mk_anot phi = AConn (ANot, [phi]) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

112 
fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2]) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

113 
fun mk_ahorn [] phi = phi 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

114 
 mk_ahorn (phi :: phis) psi = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

115 
AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi]) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

116 

41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

117 
fun close_universally phi = 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

118 
let 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

119 
fun term_vars bounds (ATerm (name as (s, _), tms)) = 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

120 
(is_atp_variable s andalso not (member (op =) bounds name)) 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

121 
? insert (op =) name 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

122 
#> fold (term_vars bounds) tms 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

123 
fun formula_vars bounds (AQuant (_, xs, phi)) = 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

124 
formula_vars (xs @ bounds) phi 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

125 
 formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

126 
 formula_vars bounds (AAtom tm) = term_vars bounds tm 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

127 
in 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

128 
case formula_vars [] phi [] of [] => phi  xs => AQuant (AForall, xs, phi) 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

129 
end 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

130 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

131 
fun combformula_for_prop thy eq_as_iff = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

132 
let 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

133 
fun do_term bs t ts = 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

134 
combterm_from_term thy bs (Envir.eta_contract t) 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

135 
>> AAtom > union (op =) ts 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

136 
fun do_quant bs q s T t' = 
38518
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

137 
let val s = Name.variant (map fst bs) s in 
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

138 
do_formula ((s, T) :: bs) t' 
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

139 
#>> (fn phi => AQuant (q, [`make_bound_var s], phi)) 
54727b44e277
handle bound name conflicts gracefully in FOF translation
blanchet
parents:
38496
diff
changeset

140 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

141 
and do_conn bs c t1 t2 = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

142 
do_formula bs t1 ##>> do_formula bs t2 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

143 
#>> (fn (phi1, phi2) => AConn (c, [phi1, phi2])) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

144 
and do_formula bs t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

145 
case t of 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

146 
@{const Not} $ t1 => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

147 
do_formula bs t1 #>> (fn phi => AConn (ANot, [phi])) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

148 
 Const (@{const_name All}, _) $ Abs (s, T, t') => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

149 
do_quant bs AForall s T t' 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

150 
 Const (@{const_name Ex}, _) $ Abs (s, T, t') => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

151 
do_quant bs AExists s T t' 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

152 
 @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd t1 t2 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

153 
 @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr t1 t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

154 
 @{const HOL.implies} $ t1 $ t2 => do_conn bs AImplies t1 t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

155 
 Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 => 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

156 
if eq_as_iff then do_conn bs AIff t1 t2 else do_term bs t 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

157 
 _ => do_term bs t 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

158 
in do_formula [] end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

159 

38618  160 
val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

161 

41491  162 
fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

163 
fun conceal_bounds Ts t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

164 
subst_bounds (map (Free o apfst concealed_bound_name) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

165 
(0 upto length Ts  1 ~~ Ts), t) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

166 
fun reveal_bounds Ts = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

167 
subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

168 
(0 upto length Ts  1 ~~ Ts)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

169 

38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

170 
(* Removes the lambdas from an equation of the form "t = (%x. u)". 
39890  171 
(Cf. "extensionalize_theorem" in "Meson_Clausify".) *) 
38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

172 
fun extensionalize_term t = 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

173 
let 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

174 
fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t' 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

175 
 aux j (t as Const (s, Type (_, [Type (_, [_, T']), 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

176 
Type (_, [_, res_T])])) 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

177 
$ t2 $ Abs (var_s, var_T, t')) = 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

178 
if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then 
38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

179 
let val var_t = Var ((var_s, j), var_T) in 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

180 
Const (s, T' > T' > res_T) 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

181 
$ betapply (t2, var_t) $ subst_bound (var_t, t') 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

182 
> aux (j + 1) 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

183 
end 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

184 
else 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

185 
t 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

186 
 aux _ t = t 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

187 
in aux (maxidx_of_term t + 1) t end 
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

188 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

189 
fun introduce_combinators_in_term ctxt kind t = 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

190 
let val thy = ProofContext.theory_of ctxt in 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

191 
if Meson.is_fol_term thy t then 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

192 
t 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

193 
else 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

194 
let 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

195 
fun aux Ts t = 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

196 
case t of 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

197 
@{const Not} $ t1 => @{const Not} $ aux Ts t1 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

198 
 (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

199 
t0 $ Abs (s, T, aux (T :: Ts) t') 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

200 
 (t0 as Const (@{const_name All}, _)) $ t1 => 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

201 
aux Ts (t0 $ eta_expand Ts t1 1) 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

202 
 (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

203 
t0 $ Abs (s, T, aux (T :: Ts) t') 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

204 
 (t0 as Const (@{const_name Ex}, _)) $ t1 => 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

205 
aux Ts (t0 $ eta_expand Ts t1 1) 
38795
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

206 
 (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
848be46708dc
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
haftmann
parents:
38786
diff
changeset

207 
 (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
38786
e46e7a9cb622
formerly unnamed infix impliciation now named HOL.implies
haftmann
parents:
38752
diff
changeset

208 
 (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2 
38864
4abe644fcea5
formerly unnamed infix equality now named HOL.eq
haftmann
parents:
38829
diff
changeset

209 
 (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _]))) 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

210 
$ t1 $ t2 => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

211 
t0 $ aux Ts t1 $ aux Ts t2 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

212 
 _ => if not (exists_subterm (fn Abs _ => true  _ => false) t) then 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

213 
t 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

214 
else 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

215 
t > conceal_bounds Ts 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

216 
> Envir.eta_contract 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

217 
> cterm_of thy 
39890  218 
> Meson_Clausify.introduce_combinators_in_cterm 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

219 
> prop_of > Logic.dest_equals > snd 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

220 
> reveal_bounds Ts 
39370
f8292d3020db
use same hack as in "Async_Manager" to work around Proof General bug
blanchet
parents:
39005
diff
changeset

221 
val (t, ctxt') = Variable.import_terms true [t] ctxt >> the_single 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

222 
in t > aux [] > singleton (Variable.export_terms ctxt' ctxt) end 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

223 
handle THM _ => 
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

224 
(* A type variable of sort "{}" will make abstraction fail. *) 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

225 
if kind = Conjecture then HOLogic.false_const 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

226 
else HOLogic.true_const 
38491
f7e51d981a9f
invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms;
blanchet
parents:
38282
diff
changeset

227 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

228 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

229 
(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

230 
same in Sledgehammer to prevent the discovery of unreplable proofs. *) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

231 
fun freeze_term t = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

232 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

233 
fun aux (t $ u) = aux t $ aux u 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

234 
 aux (Abs (s, T, t)) = Abs (s, T, aux t) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

235 
 aux (Var ((s, i), T)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

236 
Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

237 
 aux t = t 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

238 
in t > exists_subterm is_Var t ? aux end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

239 

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

240 
(* making fact and conjecture formulas *) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

241 
fun make_formula ctxt eq_as_iff presimp name kind t = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

242 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

243 
val thy = ProofContext.theory_of ctxt 
38608
01ed56c46259
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
blanchet
parents:
38606
diff
changeset

244 
val t = t > Envir.beta_eta_contract 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

245 
> transform_elim_term 
41211
1e2e16bc0077
no need to do a superduper atomization if Metis fails afterwards anyway
blanchet
parents:
41199
diff
changeset

246 
> Object_Logic.atomize_term thy 
38652
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

247 
val need_trueprop = (fastype_of t = HOLogic.boolT) 
e063be321438
perform etaexpansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38618
diff
changeset

248 
val t = t > need_trueprop ? HOLogic.mk_Trueprop 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

249 
> extensionalize_term 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

250 
> presimp ? presimplify_term thy 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

251 
> perhaps (try (HOLogic.dest_Trueprop)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

252 
> introduce_combinators_in_term ctxt kind 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

253 
> kind <> Axiom ? freeze_term 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

254 
val (combformula, ctypes_sorts) = combformula_for_prop thy eq_as_iff t [] 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

255 
in 
38752
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

256 
{name = name, combformula = combformula, kind = kind, 
6628adcae4a7
consider "locality" when assigning weights to facts
blanchet
parents:
38748
diff
changeset

257 
ctypes_sorts = ctypes_sorts} 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

258 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

259 

41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

260 
fun make_fact ctxt keep_trivial eq_as_iff presimp ((name, _), th) = 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

261 
case (keep_trivial, 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

262 
make_formula ctxt eq_as_iff presimp name Axiom (prop_of th)) of 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

263 
(false, {combformula = AAtom (CombConst (("c_True", _), _, _)), ...}) => 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

264 
NONE 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

265 
 (_, formula) => SOME formula 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

266 
fun make_conjecture ctxt ts = 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

267 
let val last = length ts  1 in 
41491  268 
map2 (fn j => make_formula ctxt true true (string_of_int j) 
38613
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

269 
(if j = last then Conjecture else Hypothesis)) 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

270 
(0 upto last) ts 
4ca2cae2653f
use "hypothesis" rather than "conjecture" for hypotheses in TPTP format;
blanchet
parents:
38610
diff
changeset

271 
end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

272 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

273 
(** Helper facts **) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

274 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

275 
fun fold_formula f (AQuant (_, _, phi)) = fold_formula f phi 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

276 
 fold_formula f (AConn (_, phis)) = fold (fold_formula f) phis 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

277 
 fold_formula f (AAtom tm) = f tm 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

278 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

279 
fun count_term (ATerm ((s, _), tms)) = 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

280 
(if is_atp_variable s then I 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

281 
else Symtab.map_entry s (Integer.add 1)) 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

282 
#> fold count_term tms 
41406  283 
fun count_formula x = fold_formula count_term x 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

284 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

285 
val init_counters = 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

286 
metis_helpers > map fst > sort_distinct string_ord > map (rpair 0) 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

287 
> Symtab.make 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

288 

41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

289 
fun get_helper_facts ctxt explicit_forall type_sys formulas = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

290 
let 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

291 
val no_dangerous_types = types_dangerous_types type_sys 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

292 
val ct = init_counters > fold count_formula formulas 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

293 
fun is_used s = the (Symtab.lookup ct s) > 0 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

294 
fun dub c needs_full_types (th, j) = 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

295 
((c ^ "_" ^ string_of_int j ^ (if needs_full_types then "ft" else ""), 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

296 
false), th) 
41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

297 
fun make_facts eq_as_iff = map_filter (make_fact ctxt false eq_as_iff false) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

298 
in 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

299 
(metis_helpers 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

300 
> filter (is_used o fst) 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

301 
> maps (fn (c, (needs_full_types, ths)) => 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

302 
if needs_full_types andalso not no_dangerous_types then 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

303 
[] 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

304 
else 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

305 
ths ~~ (1 upto length ths) 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

306 
> map (dub c needs_full_types) 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

307 
> make_facts (not needs_full_types)), 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

308 
if type_sys = Tags false then 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

309 
let 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

310 
fun var s = ATerm (`I s, []) 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

311 
fun tag tm = ATerm (`I type_tag_name, [var "X", tm]) 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

312 
in 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

313 
[Fof (helper_prefix ^ ascii_of "ti_ti", Axiom, 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

314 
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")])) 
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

315 
> explicit_forall ? close_universally, NONE)] 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

316 
end 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

317 
else 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

318 
[]) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

319 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

320 

41990
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

321 
fun translate_atp_fact ctxt keep_trivial = 
7f2793d51efc
add option to function to keep trivial ATP formulas, needed for some experiments
blanchet
parents:
41770
diff
changeset

322 
`(make_fact ctxt keep_trivial true true) 
39004
f1b465f889b5
translate the axioms to FOF once and for all ATPs
blanchet
parents:
39003
diff
changeset

323 

41134  324 
fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

325 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

326 
val thy = ProofContext.theory_of ctxt 
41091
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

327 
val fact_ts = map (prop_of o snd o snd) rich_facts 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

328 
val (facts, fact_names) = 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

329 
rich_facts 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

330 
> map_filter (fn (NONE, _) => NONE 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

331 
 (SOME fact, (name, _)) => SOME (fact, name)) 
0afdf5cde874
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet
parents:
41088
diff
changeset

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

333 
(* Remove existing facts from the conjecture, as this can dramatically 
39005  334 
boost an ATP's performance (for some reason). *) 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

335 
val hyp_ts = hyp_ts > filter_out (member (op aconv) fact_ts) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

336 
val goal_t = Logic.list_implies (hyp_ts, concl_t) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

337 
val subs = tfree_classes_of_terms [goal_t] 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

338 
val supers = tvar_classes_of_terms fact_ts 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

339 
val tycons = type_consts_of_terms thy (goal_t :: fact_ts) 
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

340 
(* TFrees in the conjecture; TVars in the facts *) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

341 
val conjs = make_conjecture ctxt (hyp_ts @ [concl_t]) 
41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

342 
val (supers', arity_clauses) = 
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

343 
if type_sys = No_Types then ([], []) 
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

344 
else make_arity_clauses thy tycons supers 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

345 
val class_rel_clauses = make_class_rel_clauses thy subs supers' 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

346 
in 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

347 
(fact_names > map single, (conjs, facts, class_rel_clauses, arity_clauses)) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

348 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

349 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

350 
fun tag_with_type ty t = ATerm (`I type_tag_name, [ty, t]) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

351 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

352 
fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

353 
 fo_term_for_combtyp (CombTFree name) = ATerm (name, []) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

354 
 fo_term_for_combtyp (CombType (name, tys)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

355 
ATerm (name, map fo_term_for_combtyp tys) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

356 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

357 
fun fo_literal_for_type_literal (TyLitVar (class, name)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

358 
(true, ATerm (class, [ATerm (name, [])])) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

359 
 fo_literal_for_type_literal (TyLitFree (class, name)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

360 
(true, ATerm (class, [ATerm (name, [])])) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

361 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

362 
fun formula_for_fo_literal (pos, t) = AAtom t > not pos ? mk_anot 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

363 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

364 
(* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

365 
considered dangerous because their "exhaust" properties can easily lead to 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

366 
unsound ATP proofs. The checks below are an (unsound) approximation of 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

367 
finiteness. *) 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

368 

eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

369 
fun is_dtyp_dangerous _ (Datatype_Aux.DtTFree _) = true 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

370 
 is_dtyp_dangerous ctxt (Datatype_Aux.DtType (s, Us)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

371 
is_type_constr_dangerous ctxt s andalso forall (is_dtyp_dangerous ctxt) Us 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

372 
 is_dtyp_dangerous _ (Datatype_Aux.DtRec _) = false 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

373 
and is_type_dangerous ctxt (Type (s, Ts)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

374 
is_type_constr_dangerous ctxt s andalso forall (is_type_dangerous ctxt) Ts 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

375 
 is_type_dangerous _ _ = false 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

376 
and is_type_constr_dangerous ctxt s = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

377 
let val thy = ProofContext.theory_of ctxt in 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

378 
case Datatype_Data.get_info thy s of 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

379 
SOME {descr, ...} => 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

380 
forall (fn (_, (_, _, constrs)) => 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

381 
forall (forall (is_dtyp_dangerous ctxt) o snd) constrs) descr 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

382 
 NONE => 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

383 
case Typedef.get_info ctxt s of 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

384 
({rep_type, ...}, _) :: _ => is_type_dangerous ctxt rep_type 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

385 
 [] => true 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

386 
end 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

387 

eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

388 
fun is_combtyp_dangerous ctxt (CombType ((s, _), tys)) = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

389 
(case strip_prefix_and_unascii type_const_prefix s of 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

390 
SOME s' => forall (is_combtyp_dangerous ctxt) tys andalso 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

391 
is_type_constr_dangerous ctxt (invert_const s') 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

392 
 NONE => false) 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

393 
 is_combtyp_dangerous _ _ = false 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

394 

eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

395 
fun should_tag_with_type ctxt (Tags full_types) ty = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

396 
full_types orelse is_combtyp_dangerous ctxt ty 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

397 
 should_tag_with_type _ _ _ = false 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

398 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

399 
val fname_table = 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

400 
[("c_False", (0, ("c_fFalse", @{const_name Metis.fFalse}))), 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

401 
("c_True", (0, ("c_fTrue", @{const_name Metis.fTrue}))), 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

402 
("c_Not", (1, ("c_fNot", @{const_name Metis.fNot}))), 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

403 
("c_conj", (2, ("c_fconj", @{const_name Metis.fconj}))), 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

404 
("c_disj", (2, ("c_fdisj", @{const_name Metis.fdisj}))), 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

405 
("c_implies", (2, ("c_fimplies", @{const_name Metis.fimplies}))), 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

406 
("equal", (2, ("c_fequal", @{const_name Metis.fequal})))] 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

407 

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

408 
(* We are crossing our fingers that it doesn't clash with anything else. *) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

410 

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

411 
fun mangled_combtyp f (CombTFree name) = f name 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

412 
 mangled_combtyp f (CombType (name, tys)) = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

413 
"(" ^ commas (map (mangled_combtyp f) tys) ^ ")" ^ f name 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

414 
 mangled_combtyp _ _ = raise Fail "impossible schematic type variable" 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

415 

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

416 
fun mangled_type_suffix f g tys = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

417 
fold_rev (curry (op ^) o g o prefix mangled_type_sep o mangled_combtyp f) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

419 

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

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

421 
Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

422 

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

423 
fun parse_mangled_type x = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

424 
($$ "("  Scan.optional parse_mangled_types []  $$ ")" 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

425 
 parse_mangled_ident >> (ATerm o swap) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

426 
 parse_mangled_ident >> (ATerm o rpair [])) x 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

427 
and parse_mangled_types x = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

428 
(parse_mangled_type ::: Scan.repeat ($$ ","  parse_mangled_type)) x 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

429 

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

430 
fun unmangled_type s = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

431 
s > suffix ")" > raw_explode 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

432 
> Scan.finite Symbol.stopper 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

433 
(Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^ 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

434 
quote s)) parse_mangled_type)) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

436 
> tap (fn u => PolyML.makestring u > warning) (*###*) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

437 

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

438 
fun unmangled_const s = 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

439 
let val ss = space_explode mangled_type_sep s in 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

440 
(hd ss, map unmangled_type (tl ss)) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

442 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

443 
fun fo_term_for_combterm ctxt type_sys = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

444 
let 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

445 
val thy = ProofContext.theory_of ctxt 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

446 
fun aux top_level u = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

447 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

448 
val (head, args) = strip_combterm_comb u 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

449 
val (x, ty_args) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

450 
case head of 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

451 
CombConst (name as (s, s'), _, ty_args) => 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

452 
(case AList.lookup (op =) fname_table s of 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

453 
SOME (n, fname) => 
41150
54b3c9c05664
make sure firstorder occurrences of "False" and "True" are handled correctly  this broke when adding proper support for higherorder occurrences
blanchet
parents:
41149
diff
changeset

454 
(if top_level andalso length args = n then 
54b3c9c05664
make sure firstorder occurrences of "False" and "True" are handled correctly  this broke when adding proper support for higherorder occurrences
blanchet
parents:
41149
diff
changeset

455 
case s of 
54b3c9c05664
make sure firstorder occurrences of "False" and "True" are handled correctly  this broke when adding proper support for higherorder occurrences
blanchet
parents:
41149
diff
changeset

456 
"c_False" => ("$false", s') 
54b3c9c05664
make sure firstorder occurrences of "False" and "True" are handled correctly  this broke when adding proper support for higherorder occurrences
blanchet
parents:
41149
diff
changeset

457 
 "c_True" => ("$true", s') 
54b3c9c05664
make sure firstorder occurrences of "False" and "True" are handled correctly  this broke when adding proper support for higherorder occurrences
blanchet
parents:
41149
diff
changeset

458 
 _ => name 
54b3c9c05664
make sure firstorder occurrences of "False" and "True" are handled correctly  this broke when adding proper support for higherorder occurrences
blanchet
parents:
41149
diff
changeset

459 
else 
54b3c9c05664
make sure firstorder occurrences of "False" and "True" are handled correctly  this broke when adding proper support for higherorder occurrences
blanchet
parents:
41149
diff
changeset

460 
fname, []) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

461 
 NONE => 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

462 
case strip_prefix_and_unascii const_prefix s of 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

463 
NONE => (name, ty_args) 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

464 
 SOME s'' => 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

465 
let val s'' = invert_const s'' in 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

466 
case type_arg_policy thy type_sys s'' of 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

467 
No_Type_Args => (name, []) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

468 
 Explicit_Type_Args => (name, ty_args) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

470 
((s ^ mangled_type_suffix fst ascii_of ty_args, 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

471 
s' ^ mangled_type_suffix snd I ty_args), []) 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

472 
end) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

473 
 CombVar (name, _) => (name, []) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

474 
 CombApp _ => raise Fail "impossible \"CombApp\"" 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

475 
val t = 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

476 
ATerm (x, map fo_term_for_combtyp ty_args @ map (aux false) args) 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

477 
val ty = combtyp_of u 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

478 
in 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

479 
t > (if should_tag_with_type ctxt type_sys ty then 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

480 
tag_with_type (fo_term_for_combtyp ty) 
41134  481 
else 
482 
I) 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

483 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

484 
in aux true end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

485 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

486 
fun formula_for_combformula ctxt type_sys = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

487 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

488 
fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

489 
 aux (AConn (c, phis)) = AConn (c, map aux phis) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

490 
 aux (AAtom tm) = AAtom (fo_term_for_combterm ctxt type_sys tm) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

491 
in aux end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

492 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

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

494 
({combformula, ctypes_sorts, ...} : translated_formula) = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

495 
mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal) 
41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

496 
(atp_type_literals_for_types type_sys ctypes_sorts)) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

497 
(formula_for_combformula ctxt type_sys combformula) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

498 

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

499 
(* Each fact is given a unique fact number to avoid name clashes (e.g., because 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

500 
of monomorphization). The TPTP explicitly forbids name clashes, and some of 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

501 
the remote provers might care. *) 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

502 
fun problem_line_for_fact ctxt prefix type_sys 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

503 
(j, formula as {name, kind, ...}) = 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

504 
Fof (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind, 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

505 
formula_for_fact ctxt type_sys formula, NONE) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

506 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

507 
fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass, 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

508 
superclass, ...}) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

509 
let val ty_arg = ATerm (("T", "T"), []) in 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

510 
Fof (class_rel_clause_prefix ^ ascii_of name, Axiom, 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

511 
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])), 
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

512 
AAtom (ATerm (superclass, [ty_arg]))]), NONE) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

513 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

514 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

515 
fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

516 
(true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

517 
 fo_literal_for_arity_literal (TVarLit (c, sort)) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

518 
(false, ATerm (c, [ATerm (sort, [])])) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

519 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

520 
fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits, 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

521 
...}) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

522 
Fof (arity_clause_prefix ^ ascii_of name, Axiom, 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

523 
mk_ahorn (map (formula_for_fo_literal o apfst not 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

524 
o fo_literal_for_arity_literal) premLits) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

525 
(formula_for_fo_literal 
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

526 
(fo_literal_for_arity_literal conclLit)), NONE) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

527 

41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

528 
fun problem_line_for_conjecture ctxt type_sys 
40114  529 
({name, kind, combformula, ...} : translated_formula) = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

530 
Fof (conjecture_prefix ^ name, kind, 
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

531 
formula_for_combformula ctxt type_sys combformula, NONE) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

532 

41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

533 
fun free_type_literals_for_conjecture type_sys 
40114  534 
({ctypes_sorts, ...} : translated_formula) = 
41137
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

535 
ctypes_sorts > atp_type_literals_for_types type_sys 
8b634031b2a5
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
blanchet
parents:
41136
diff
changeset

536 
> map fo_literal_for_type_literal 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

537 

39975
7c50d5ca5c04
avoid generating several formulas with the same name ("tfrees")
blanchet
parents:
39954
diff
changeset

538 
fun problem_line_for_free_type j lit = 
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

539 
Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit, 
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

540 
NONE) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

541 
fun problem_lines_for_free_types type_sys conjs = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

542 
let 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

543 
val litss = map (free_type_literals_for_conjecture type_sys) conjs 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

544 
val lits = fold (union (op =)) litss [] 
39975
7c50d5ca5c04
avoid generating several formulas with the same name ("tfrees")
blanchet
parents:
39954
diff
changeset

545 
in map2 problem_line_for_free_type (0 upto length lits  1) lits end 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

546 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

547 
(** "hBOOL" and "hAPP" **) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

548 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

549 
type const_info = {min_arity: int, max_arity: int, sub_level: bool} 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

550 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

551 
fun consider_term top_level (ATerm ((s, _), ts)) = 
39452  552 
(if is_atp_variable s then 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

553 
I 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

554 
else 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

555 
let val n = length ts in 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

556 
Symtab.map_default 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

557 
(s, {min_arity = n, max_arity = 0, sub_level = false}) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

558 
(fn {min_arity, max_arity, sub_level} => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

559 
{min_arity = Int.min (n, min_arity), 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

560 
max_arity = Int.max (n, max_arity), 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

561 
sub_level = sub_level orelse not top_level}) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

562 
end) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

563 
#> fold (consider_term (top_level andalso s = type_tag_name)) ts 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

564 
fun consider_formula (AQuant (_, _, phi)) = consider_formula phi 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

565 
 consider_formula (AConn (_, phis)) = fold consider_formula phis 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

566 
 consider_formula (AAtom tm) = consider_term true tm 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

567 

41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

568 
fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

569 
fun consider_problem problem = fold (fold consider_problem_line o snd) problem 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

570 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

571 
(* needed for helper facts if the problem otherwise does not involve equality *) 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

572 
val equal_entry = ("equal", {min_arity = 2, max_arity = 2, sub_level = false}) 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

573 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

574 
fun const_table_for_problem explicit_apply problem = 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

575 
if explicit_apply then 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

576 
NONE 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

577 
else 
41147
0e1903273712
fix translation of higherorder equality ("fequal") if "precise_overloaded_args" is "true"
blanchet
parents:
41145
diff
changeset

578 
SOME (Symtab.empty > Symtab.default equal_entry > consider_problem problem) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

579 

41134  580 
fun min_arity_of thy type_sys NONE s = 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

581 
(if s = "equal" orelse s = type_tag_name orelse 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

582 
String.isPrefix type_const_prefix s orelse 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

583 
String.isPrefix class_prefix s then 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

584 
16383 (* large number *) 
38748  585 
else case strip_prefix_and_unascii const_prefix s of 
42227
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

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

587 
s' > unmangled_const > fst > invert_const 
662b50b7126f
if "monomorphize" is enabled, mangle the type information in the names by default
blanchet
parents:
42180
diff
changeset

588 
> num_atp_type_args thy type_sys 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

589 
 NONE => 0) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

590 
 min_arity_of _ _ (SOME the_const_tab) s = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

591 
case Symtab.lookup the_const_tab s of 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

592 
SOME ({min_arity, ...} : const_info) => min_arity 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

593 
 NONE => 0 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

594 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

595 
fun full_type_of (ATerm ((s, _), [ty, _])) = 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

596 
if s = type_tag_name then SOME ty else NONE 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

597 
 full_type_of _ = NONE 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

598 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

599 
fun list_hAPP_rev _ t1 [] = t1 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

600 
 list_hAPP_rev NONE t1 (t2 :: ts2) = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

601 
ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2]) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

602 
 list_hAPP_rev (SOME ty) t1 (t2 :: ts2) = 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

603 
case full_type_of t2 of 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

604 
SOME ty2 => 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

605 
let val ty' = ATerm (`make_fixed_type_const @{type_name fun}, 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

606 
[ty2, ty]) in 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

607 
ATerm (`I "hAPP", 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

608 
[tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

609 
end 
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

610 
 NONE => list_hAPP_rev NONE t1 (t2 :: ts2) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

611 

41134  612 
fun repair_applications_in_term thy type_sys const_tab = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

613 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

614 
fun aux opt_ty (ATerm (name as (s, _), ts)) = 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

615 
if s = type_tag_name then 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

616 
case ts of 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

617 
[t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

618 
 _ => raise Fail "malformed type tag" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

619 
else 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

620 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

621 
val ts = map (aux NONE) ts 
41134  622 
val (ts1, ts2) = chop (min_arity_of thy type_sys const_tab s) ts 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

623 
in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

624 
in aux NONE end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

625 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

626 
fun boolify t = ATerm (`I "hBOOL", [t]) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

627 

319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

628 
(* True if the constant ever appears outside of the toplevel position in 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

629 
literals, or if it appears with different arities (e.g., because of different 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

630 
type instantiations). If false, the constant always receives all of its 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

631 
arguments and is used as a predicate. *) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

632 
fun is_predicate NONE s = 
38589
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38518
diff
changeset

633 
s = "equal" orelse s = "$false" orelse s = "$true" orelse 
b03f8fe043ec
added "max_relevant_per_iter" option to Sledgehammer
blanchet
parents:
38518
diff
changeset

634 
String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

635 
 is_predicate (SOME the_const_tab) s = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

636 
case Symtab.lookup the_const_tab s of 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

637 
SOME {min_arity, max_arity, sub_level} => 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

638 
not sub_level andalso min_arity = max_arity 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

639 
 NONE => false 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

640 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

641 
fun repair_predicates_in_term pred_const_tab (t as ATerm ((s, _), ts)) = 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

642 
if s = type_tag_name then 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

643 
case ts of 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

644 
[_, t' as ATerm ((s', _), _)] => 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

645 
if is_predicate pred_const_tab s' then t' else boolify t 
41138
eb80538166b6
implemented partiallytyped "tags" type encoding
blanchet
parents:
41137
diff
changeset

646 
 _ => raise Fail "malformed type tag" 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

647 
else 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

648 
t > not (is_predicate pred_const_tab s) ? boolify 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

649 

41134  650 
fun repair_formula thy explicit_forall type_sys const_tab = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

651 
let 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

652 
val pred_const_tab = case type_sys of Tags _ => NONE  _ => const_tab 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

653 
fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

654 
 aux (AConn (c, phis)) = AConn (c, map aux phis) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

655 
 aux (AAtom tm) = 
41134  656 
AAtom (tm > repair_applications_in_term thy type_sys const_tab 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

657 
> repair_predicates_in_term pred_const_tab) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

658 
in aux #> explicit_forall ? close_universally end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

659 

41134  660 
fun repair_problem_line thy explicit_forall type_sys const_tab 
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

661 
(Fof (ident, kind, phi, source)) = 
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

662 
Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi, 
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

663 
source) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

664 
fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

665 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

666 
fun dest_Fof (Fof z) = z 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

667 

41157  668 
val factsN = "Relevant facts" 
669 
val class_relsN = "Class relationships" 

670 
val aritiesN = "Arity declarations" 

671 
val helpersN = "Helper facts" 

672 
val conjsN = "Conjectures" 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

673 
val free_typesN = "Type variables" 
41157  674 

675 
fun offset_of_heading_in_problem _ [] j = j 

676 
 offset_of_heading_in_problem needle ((heading, lines) :: problem) j = 

677 
if heading = needle then j 

678 
else offset_of_heading_in_problem needle problem (j + length lines) 

679 

41134  680 
fun prepare_atp_problem ctxt readable_names explicit_forall type_sys 
40204
da97d75e20e6
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer  but keep "Axiom" in the lowerlevel "ATP_Problem" module
blanchet
parents:
40145
diff
changeset

681 
explicit_apply hyp_ts concl_t facts = 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

682 
let 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

683 
val thy = ProofContext.theory_of ctxt 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

684 
val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = 
41134  685 
translate_formulas ctxt type_sys hyp_ts concl_t facts 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

686 
(* Reordering these might or might not confuse the proof reconstruction 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

687 
code or the SPASS Flotter hack. *) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

688 
val problem = 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

689 
[(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys) 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

690 
(0 upto length facts  1 ~~ facts)), 
41157  691 
(class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), 
692 
(aritiesN, map problem_line_for_arity_clause arity_clauses), 

693 
(helpersN, []), 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

694 
(conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

695 
(free_typesN, problem_lines_for_free_types type_sys conjs)] 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

696 
val const_tab = const_table_for_problem explicit_apply problem 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

697 
val problem = 
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

698 
problem > repair_problem thy explicit_forall type_sys const_tab 
41157  699 
val helper_lines = 
41145
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

700 
get_helper_facts ctxt explicit_forall type_sys 
a5ee3b8e5a90
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
blanchet
parents:
41140
diff
changeset

701 
(maps (map (#3 o dest_Fof) o snd) problem) 
42180
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

702 
>> map (pair 0 
a6c141925a8a
added monomorphization option to Sledgehammer ATPs  this looks promising but is still off by default
blanchet
parents:
41990
diff
changeset

703 
#> problem_line_for_fact ctxt helper_prefix type_sys 
41157  704 
#> repair_problem_line thy explicit_forall type_sys const_tab) 
705 
> op @ 

41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

706 
val (problem, pool) = 
41157  707 
problem > AList.update (op =) (helpersN, helper_lines) 
41140
9c68004b8c9d
added Sledgehammer support for higherorder propositional reasoning
blanchet
parents:
41138
diff
changeset

708 
> nice_atp_problem readable_names 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

709 
in 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

710 
(problem, 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

711 
case pool of SOME the_pool => snd the_pool  NONE => Symtab.empty, 
41157  712 
offset_of_heading_in_problem conjsN problem 0, 
713 
fact_names > Vector.fromList) 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

714 
end 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

715 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

716 
(* FUDGE *) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

717 
val conj_weight = 0.0 
41770  718 
val hyp_weight = 0.1 
719 
val fact_min_weight = 0.2 

41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

720 
val fact_max_weight = 1.0 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

721 

a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

722 
fun add_term_weights weight (ATerm (s, tms)) = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

723 
(not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

724 
#> fold (add_term_weights weight) tms 
41769
eb2e39555f98
extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs
blanchet
parents:
41748
diff
changeset

725 
fun add_problem_line_weights weight (Fof (_, _, phi, _)) = 
41384  726 
fold_formula (add_term_weights weight) phi 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

727 

a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

728 
fun add_conjectures_weights [] = I 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

729 
 add_conjectures_weights conjs = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

730 
let val (hyps, conj) = split_last conjs in 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

731 
add_problem_line_weights conj_weight conj 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

732 
#> fold (add_problem_line_weights hyp_weight) hyps 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

733 
end 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

734 

a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

735 
fun add_facts_weights facts = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

736 
let 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

737 
val num_facts = length facts 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

738 
fun weight_of j = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

739 
fact_min_weight + (fact_max_weight  fact_min_weight) * Real.fromInt j 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

740 
/ Real.fromInt num_facts 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

741 
in 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

742 
map weight_of (0 upto num_facts  1) ~~ facts 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

743 
> fold (uncurry add_problem_line_weights) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

744 
end 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

745 

a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

746 
(* Weights are from 0.0 (most important) to 1.0 (least important). *) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

747 
fun atp_problem_weights problem = 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

748 
Symtab.empty 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

749 
> add_conjectures_weights (these (AList.lookup (op =) problem conjsN)) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

750 
> add_facts_weights (these (AList.lookup (op =) problem factsN)) 
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

751 
> Symtab.dest 
41726  752 
> sort (prod_ord Real.compare string_ord o pairself swap) 
41313
a96ac4d180b7
optionally supply constant weights to E  turned off by default until properly parameterized
blanchet
parents:
41211
diff
changeset

753 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
diff
changeset

754 
end; 